S906-017 merge AdaCore master with upstream next branch

To get fix for soundness issue OCamlPro#248

Change-Id: I853a3d577919dc360e4839474d8b4daa1a5106fd

Author: kanigsson

extra/test_lib.sh

@@ -27,7 +27,7 @@ ocamlopt -o lib_usage \
   -I `ocamlfind query zarith` \
   -I `ocamlfind query ocplib-simplex` \
   -I `ocamlfind query psmt2-frontend` \
-  -I `ocamlfind query camlzip` \
+  -I `ocamlfind query zip` \
   -I $lib_path \
   nums.cmxa zarith.cmxa ocplibSimplex.cmxa psmt2Frontend.cmxa \
   unix.cmxa str.cmxa zip.cmxa dynlink.cmxa \

sources/alt-ergo-parsers.opam

@@ -14,7 +14,7 @@ depends: [
   "dune" { build }
   "alt-ergo-lib" { = "2.3.0+" }
   "psmt2-frontend" { >= "0.2" }
-  "camlzip"
+  "camlzip" { >= "1.07" }
   "menhir"
 ]
 homepage: "http://alt-ergo.ocamlpro.com/"

sources/lib/reasoners/instances.ml

@@ -69,7 +69,19 @@ end
 
 module Make(X : Theory.S) : S with type tbox = X.t = struct
 
-  module EM = Matching.Make(Ccx.Main)
+  module EM = Matching.Make(struct
+
+      include Ccx.Main
+
+      (* This function from Ccx.Main is wrapped to ensure Fresh explanations
+         will not leak through Ccx during matching, in which case assertions
+         in various places will be raised. *)
+      let term_repr t e ~init_term =
+        try Ccx.Main.term_repr t ~init_term e
+        with Ex.Inconsistent (d, _) as exn ->
+          if Ex.exists_fresh d then e else raise exn
+
+    end)
 
   type tbox = X.t
   type instances = (Expr.gformula * Ex.t) list

sources/lib/reasoners/intervalCalculus.ml

@@ -402,26 +402,33 @@ end
    normalized polys *)
 let generic_find xp env =
   let is_mon = is_alien xp in
+  if debug_fm () then
+    fprintf fmt "generic_find: %a ... " X.print xp;
   try
     if not is_mon then raise Not_found;
-    let i, use = MX.n_find xp env.monomes in i, use, is_mon
+    let i, use = MX.n_find xp env.monomes in
+    if debug_fm () then fprintf fmt "found@.";
+    i, use, is_mon
   with Not_found ->
     (* according to this implem, it means that we can find aliens in polys
        but not in monomes. FIX THIS => an interval of x in monomes and in
        polys may be differents !!! *)
+    if debug_fm () then
+      fprintf fmt "not_found@.";
     let p0 = poly_of xp in
     let p, c = P.separate_constant p0 in
     let p, c0, d = P.normal_form_pos p in
+    if debug_fm() then
+      fprintf fmt "normalized into %a + %a * %a@."
+        Q.print c Q.print d P.print p;
     assert (Q.sign d <> 0 && Q.sign c0 = 0);
     let ty = P.type_info p0 in
     let ip =
       try MP.n_find p env.polynomes with Not_found -> I.undefined ty
     in
-    let ip = if Q.is_one d then ip else I.scale d ip in
-    let ip =
-      if Q.is_zero c then ip
-      else I.add ip (I.point c ty Explanation.empty)
-    in
+    if debug_fm() then
+      fprintf fmt "scaling %a by %a@." I.print ip Q.print d;
+    let ip = I.affine_scale ~const:c ~coef:d ip in
     ip, SX.empty, is_mon
 
 
@@ -515,13 +522,21 @@ module Debug = struct
       fprintf fmt "\t0@.@."
     end
 
-  let tighten_interval_modulo_eq p1 p2 i1 i2 b1 b2 j =
+  let tighten_interval_modulo_eq_begin p1 p2 =
     if debug_fm () then begin
       fprintf fmt "@.[fm] tighten intervals modulo eq: %a = %a@."
         P.print p1 P.print p2;
+    end
+
+  let tighten_interval_modulo_eq_middle p1 p2 i1 i2 j =
+    if debug_fm () then begin
       fprintf fmt "  %a has interval %a@." P.print p1 I.print i1;
       fprintf fmt "  %a has interval %a@." P.print p2 I.print i2;
       fprintf fmt "  intersection is %a@." I.print j;
+    end
+
+  let tighten_interval_modulo_eq_end p1 p2 b1 b2 =
+    if debug_fm () then begin
       if b1 then fprintf fmt "  > improve interval of %a@.@." P.print p1;
       if b2 then fprintf fmt "  > improve interval of %a@.@." P.print p2;
       if not b1 && not b2 then fprintf fmt "  > no improvement@.@."
@@ -1384,12 +1399,14 @@ let tighten_eq_bounds env r1 r2 p1 p2 origin_eq expl =
     | Th_util.CS _ | Th_util.NCS _ -> env
     | Th_util.Subst | Th_util.Other ->
       (* Subst is needed, but is Other needed ?? or is it subsumed ? *)
+      Debug.tighten_interval_modulo_eq_begin p1 p2;
       let i1, us1, is_mon_1 = generic_find r1 env in
       let i2, us2, is_mon_2 = generic_find r2 env in
       let j = I.add_explanation (I.intersect i1 i2) expl in
+      Debug.tighten_interval_modulo_eq_middle p1 p2 i1 i2 j;
       let impr_i1 = I.is_strict_smaller j i1 in
       let impr_i2 = I.is_strict_smaller j i2 in
-      Debug.tighten_interval_modulo_eq p1 p2 i1 i2 impr_i1 impr_i2 j;
+      Debug.tighten_interval_modulo_eq_end p1 p2 impr_i1 impr_i2;
       let env =
         if impr_i1 then generic_add r1 j us1 is_mon_1 env else env
       in

sources/lib/reasoners/intervals.ml

@@ -445,6 +445,23 @@ let exclude =
     let uints1_c = union_intervals {uints1 with ints = l_c} in
     intersect uints1_c uints2
 
+let add_borne b1 b2 =
+  match b1,b2 with
+  | Minfty, Pinfty | Pinfty, Minfty -> assert false
+  | Minfty, _ | _, Minfty -> Minfty
+  | Pinfty, _ | _, Pinfty -> Pinfty
+  | Large (v1, e1), Large (v2, e2) ->
+    Large (Q.add v1 v2, Ex.union e1 e2)
+  | (Large (v1, e1) | Strict (v1, e1)), (Large (v2, e2) | Strict (v2, e2)) ->
+    Strict (Q.add v1 v2, Ex.union e1 e2)
+
+let translate c ((b1, b2) as b) =
+  if Q.(equal zero) c then b
+  else begin
+    let tmp = Large (c, Ex.empty) in
+    (add_borne b1 tmp, add_borne b2 tmp)
+  end
+
 let scale_interval_zero n (b1, b2) =
   assert (Q.sign n = 0);
   Large (Q.zero, explain_borne b1), Large (Q.zero, explain_borne b2)
@@ -463,34 +480,31 @@ let scale_interval_neg n (b1, b2) =
   minus_borne (scale_borne_non_zero (Q.minus n) b2),
   minus_borne (scale_borne_non_zero (Q.minus n) b1)
 
-let scale n uints =
+
+let affine_scale ~const ~coef uints =
   Options.tool_req 4 "TR-Arith-Axiomes scale";
-  if Q.equal n Q.one then uints
+  if Q.equal coef Q.one then
+    { uints with ints = List.map (translate const) uints.ints; }
   else
-    let sgn = Q.sign n in
+    let sgn = Q.sign coef in
     let aux =
       if sgn = 0 then scale_interval_zero
       else if sgn > 0 then scale_interval_pos
       else scale_interval_neg
     in
-    let rl = List.rev_map (aux n) uints.ints in
+    let rl = List.rev_map (fun bornes ->
+        translate const (aux coef bornes)
+      ) uints.ints in
     let l =
-      if uints.is_int then rev_normalize_int_bounds rl uints.expl n
+      if uints.is_int then rev_normalize_int_bounds rl uints.expl coef
       else List.rev rl
     in
     let res = union_intervals { uints with ints = l } in
     assert (res.ints != []);
     res
 
-let add_borne b1 b2 =
-  match b1,b2 with
-  | Minfty, Pinfty | Pinfty, Minfty -> assert false
-  | Minfty, _ | _, Minfty -> Minfty
-  | Pinfty, _ | _, Pinfty -> Pinfty
-  | Large (v1, e1), Large (v2, e2) ->
-    Large (Q.add v1 v2, Ex.union e1 e2)
-  | (Large (v1, e1) | Strict (v1, e1)), (Large (v2, e2) | Strict (v2, e2)) ->
-    Strict (Q.add v1 v2, Ex.union e1 e2)
+let scale coef uints =
+  affine_scale ~const:Q.zero ~coef uints
 
 let add_interval is_int l (b1,b2) =
   List.fold_right

sources/lib/reasoners/intervals.mli

@@ -65,6 +65,13 @@ val add : t -> t -> t
 
 val scale : Numbers.Q.t -> t -> t
 
+val affine_scale : const:Numbers.Q.t -> coef:Numbers.Q.t -> t -> t
+(** Perform an affine transformation on the given bounds.
+    Suposing input bounds (b1, b2), this will return
+    (const + coef * b1, const + coef * b2).
+    This function is useful to avoid the incorrect roundings that
+    can take place when scaling down an integer range. *)
+
 val sub : t -> t -> t
 
 val merge : t -> t -> t

sources/lib/structures/explanation.ml

@@ -94,6 +94,12 @@ let fresh_exp =
     incr r;
     Fresh !r
 
+let exists_fresh t =
+  S.exists (function
+      | Fresh _ -> true
+      | _ -> false
+    ) t
+
 let remove_fresh fe s =
   if S.mem fe s then Some (S.remove fe s)
   else None

sources/lib/structures/explanation.mli

@@ -55,6 +55,9 @@ val fold_atoms : (exp -> 'a -> 'a )  -> t -> 'a -> 'a
 
 val fresh_exp : unit -> exp
 
+val exists_fresh : t -> bool
+(** Does there exists a [Fresh _] exp in an explanation set. *)
+
 val remove_fresh : exp -> t -> t option
 
 val remove : exp -> t -> t