[e-acsl] add interval inference for quantifiers

src/plugins/e-acsl/src/analyses/interval.ml

@@ -862,7 +862,65 @@ and infer_term_offset ~logic_env t =
     ignore (infer ~logic_env t);
     infer_term_offset ~logic_env toff
 
-let rec infer_predicate ~logic_env p =
+(* [type_bound_variables] infers an interval associated with each of
+   the provided bounds of a quantified variable, and provides a term
+   accordingly. It could happen that the bounds provided for a quantifier
+   [lv] are bigger than its type. [type_bound_variables] handles such cases
+   and provides smaller bounds whenever possible.
+   Let B be the inferred interval and R the range of [lv.typ]
+   - Case 1: B \subseteq R
+     Example: [\forall unsigned char c; 4 <= c <= 100 ==> 0 <= c <= 255]
+     Return: B
+   - Case 2: B \not\subseteq R and the bounds of B are inferred exactly
+     Example: [\forall unsigned char c; 4 <= c <= 300 ==> 0 <= c <= 255]
+     Return: B \intersect R
+   - Case 3: B \not\subseteq R and the bounds of B are NOT inferred exactly
+     Example: [\let m = n > 0 ? 4 : 341; \forall char u; 1 < u < m ==> u > 0]
+     Return: R with a guard guaranteeing that [lv] does not overflow *)
+let rec infer_bound_variable ~loc ~logic_env (t1, lv, t2) =
+  let get_res = Error.map (fun x -> x) in
+  let i1 = get_res (infer ~logic_env t1) in
+  let i2 = get_res (infer ~logic_env t2) in
+  let i = widen (join i1 i2) in
+  let t1, t2, i =
+    match lv.lv_type with
+    | Ltype _ | Lvar _ | Lreal | Larrow _ ->
+      Error.not_yet "quantification over non-integer type"
+    | Linteger -> t1, t2, i
+    | Ctype ty ->
+      let ity = extended_interv_of_typ ty in
+      if is_included i ity then
+        (* case 1 *)
+        t1, t2, i
+      else if is_singleton_int i1 &&
+              is_singleton_int i2 then
+        begin
+          (* case 2 *)
+          let i = meet i ity in
+          (* We can now update the bounds in the preprocessed form
+             that come from the meet of the two intervals *)
+          let min, max = Misc.finite_min_and_max (extract_ival i) in
+          let t1 = Logic_const.tint ~loc min in
+          let t2 = Logic_const.tint ~loc max in
+          t1, t2, i
+        end else
+        (* case 3 *)
+        let min, max = Misc.finite_min_and_max (extract_ival ity) in
+        let guard_lower = Logic_const.tint ~loc min in
+        let guard_upper = Logic_const.tint ~loc max in
+        let lv_term = Logic_const.tvar ~loc lv in
+        let guard_lower = Logic_const.prel ~loc (Rle, guard_lower, lv_term) in
+        let guard_upper = Logic_const.prel ~loc (Rlt, lv_term, guard_upper) in
+        let guard = Logic_const.pand ~loc (guard_lower, guard_upper) in
+        ignore (infer_predicate ~logic_env guard);
+        Bound_variables.add_guard_for_small_type lv guard;
+        t1, t2, i
+  in
+  ignore (infer ~logic_env t1);
+  ignore (infer ~logic_env t2);
+  Logic_environment.add_let_quantif_binding logic_env lv i, (t1, lv, t2)
+
+and infer_predicate ~logic_env p =
   match Logic_normalizer.get_pred p with
   | PoT_term t -> ignore (infer ~logic_env t)
   | PoT_pred p ->
@@ -896,8 +954,26 @@ let rec infer_predicate ~logic_env p =
       in
       (infer_predicate ~logic_env p)
     | Pforall _
-    | Pexists _ -> ()
-    (* TODO:  *)
+    | Pexists _ ->
+      let guards, goal =
+        Error.retrieve_preprocessing
+          "quantified predicate"
+          Bound_variables.get_preprocessed_quantifier
+          p
+          Printer.pp_predicate
+      in
+      let loc = p.pred_loc in
+      let rec do_analysis guards new_guards logic_env = match guards with
+        | [] -> logic_env, new_guards
+        | guard :: guards ->
+          let  logic_env, new_guard =
+            infer_bound_variable ~loc ~logic_env guard
+          in
+          do_analysis guards (new_guard :: new_guards) logic_env
+      in
+      let logic_env, new_guards = do_analysis guards [] logic_env in
+      Bound_variables.replace p new_guards goal;
+      infer_predicate ~logic_env goal
     | Pseparated tlist ->
       List.iter
         (fun t -> ignore (infer ~logic_env t))

src/plugins/e-acsl/src/analyses/typing.ml

@@ -702,88 +702,33 @@ and type_term_offset ~profile t = match t with
     ignore (type_term ~use_gmp_opt:false ~ctx ~profile t);
     type_term_offset ~profile toff
 
-(* [type_bound_variables] infers an interval associated with each of
-   the provided bounds of a quantified variable, and provides a term
-   accordingly. It could happen that the bounds provided for a quantifier
-   [lv] are bigger than its type. [type_bound_variables] handles such cases
-   and provides smaller bounds whenever possible.
-   Let B be the inferred interval and R the range of [lv.typ]
-   - Case 1: B \subseteq R
-     Example: [\forall unsigned char c; 4 <= c <= 100 ==> 0 <= c <= 255]
-     Return: B
-   - Case 2: B \not\subseteq R and the bounds of B are inferred exactly
-     Example: [\forall unsigned char c; 4 <= c <= 300 ==> 0 <= c <= 255]
-     Return: B \intersect R
-   - Case 3: B \not\subseteq R and the bounds of B are NOT inferred exactly
-     Example: [\let m = n > 0 ? 4 : 341; \forall char u; 1 < u < m ==> u > 0]
-     Return: R with a guard guaranteeing that [lv] does not overflow *)
-and type_bound_variables ~loc ~profile (t1, lv, t2) =
-  let i1 = Interval.get t1 in
-  let i2 = Interval.get t2 in
+and number_ty_bound_variable ~profile (t1, lv, t2) =
+  let i1 = Interval.get_p ~profile t1 in
+  let i2 = Interval.get_p ~profile t2 in
   let i = Interval.(widen (join i1 i2)) in
-  let ctx = match lv.lv_type with
-    | Linteger -> mk_ctx ~use_gmp_opt:true (ty_of_interv ~ctx:Gmpz i)
-    | Ctype ty ->
-      (match Cil.unrollType ty with
-       | TInt(ik, _) | TEnum({ ekind = ik }, _) ->
-         mk_ctx ~use_gmp_opt:true (C_integer ik)
-       | ty ->
-         Options.fatal "unexpected C type %a for quantified variable %a"
-           Printer.pp_typ ty
-           Printer.pp_logic_var lv)
-    | lty ->
-      Options.fatal "unexpected logic type %a for quantified variable %a"
-        Printer.pp_logic_type lty
-        Printer.pp_logic_var lv
-  in
-  let t1, t2, i =
-    match lv.lv_type with
-    | Ltype _ | Lvar _ | Lreal | Larrow _ ->
-      Error.not_yet "quantification over non-integer type"
-    | Linteger -> t1, t2, i
-    | Ctype ty ->
-      let ity = Interval.extended_interv_of_typ ty in
-      if Interval.is_included i ity then
-        (* case 1 *)
-        t1, t2, i
-      else if Interval.is_singleton_int i1 &&
-              Interval.is_singleton_int i2 then
-        begin
-          (* case 2 *)
-          let i = Interval.meet i ity in
-          (* We can now update the bounds in the preprocessed form
-             that come from the meet of the two intervals *)
-          let min, max = Misc.finite_min_and_max (Interval.extract_ival i) in
-          let t1 = Logic_const.tint ~loc min in
-          let t2 = Logic_const.tint ~loc max in
-          t1, t2, i
-        end else
-        (* case 3 *)
-        let min, max = Misc.finite_min_and_max (Interval.extract_ival ity) in
-        let guard_lower = Logic_const.tint ~loc min in
-        let guard_upper = Logic_const.tint ~loc max in
-        let lv_term = Logic_const.tvar ~loc lv in
-        let guard_lower = Logic_const.prel ~loc (Rle, guard_lower, lv_term) in
-        let guard_upper = Logic_const.prel ~loc (Rlt, lv_term, guard_upper) in
-        let guard = Logic_const.pand ~loc (guard_lower, guard_upper) in
-        ignore (type_predicate ~profile guard);
-        Bound_variables.add_guard_for_small_type lv guard;
-        t1, t2, i
-  in
+  match lv.lv_type with
+  | Linteger ->
+    mk_ctx ~use_gmp_opt:true (ty_of_interv ~ctx:Gmpz i)
+  | Ctype ty ->
+    (match Cil.unrollType ty with
+     | TInt(ik, _) | TEnum({ ekind = ik}, _)-> join
+                        (ty_of_interv i)
+                        (mk_ctx ~use_gmp_opt:true (C_integer ik))
+     | ty ->
+       Options.fatal "unexpected C type %a for quantified variable %a"
+         Printer.pp_typ ty
+         Printer.pp_logic_var lv)
+  | lty ->
+    Options.fatal "unexpected logic type %a for quantified variable %a"
+      Printer.pp_logic_type lty
+      Printer.pp_logic_var lv
+
+and type_bound_variables ~profile (t1, lv, t2) =
+  let ctx= number_ty_bound_variable ~profile (t1, lv, t2) in
   (* forcing when typing bounds prevents to generate an extra useless
      GMP variable when --e-acsl-gmp-only *)
-  ignore (type_term ~use_gmp_opt:false ~ctx ~profile t1);
-  ignore (type_term ~use_gmp_opt:false ~ctx ~profile t2);
-  (* if we must generate GMP code, degrade the interval in order to
-     guarantee that [x] will be a GMP when typing the goal *)
-  let _ = match ctx with
-    | C_integer _ -> i
-    (* [ -\infty; +\infty ] *)
-    | Gmpz -> Interval.Ival (Ival.inject_range None None)
-    | C_float _ | Rational | Real | Nan ->
-      Options.fatal "unexpected quantification over %a" D.pretty ctx
-  in
-  (t1, lv, t2)
+  ignore(type_term ~use_gmp_opt:false ~ctx ~profile t1);
+  ignore(type_term ~use_gmp_opt:false ~ctx ~profile t2)
 
 and type_predicate ~profile p =
   let p = Logic_normalizer.get_pred p in
@@ -796,15 +741,12 @@ and type_predicate ~profile p =
       begin
         match li.l_body with
         | LBpred p ->
-          let typed_args =
-            type_args
-              ~use_gmp_opt:true
-              ~profile
-              li.l_profile
-              args
-              li.l_var_info.lv_name
-          in
-          ignore (type_predicate ~profile:typed_args p);
+          List.iter
+            (fun x -> ignore
+                (type_term ~use_gmp_opt: true ~profile x))
+            args;
+          let new_profile = List.map (Interval.get_p ~profile) args in
+          ignore (type_predicate ~profile:new_profile p);
         | LBnone -> ()
         | LBreads _ -> ()
         | LBinductive _ -> ()
@@ -855,12 +797,10 @@ and type_predicate ~profile p =
             p
             Printer.pp_predicate
         in
-        let guards =
-          List.map
-            (fun (t1, x, t2) ->
-               type_bound_variables ~loc:p.pred_loc ~profile (t1, x, t2))
-            guards
-        in Bound_variables.replace p guards goal;
+        List.iter
+          (fun (t1, x, t2) ->
+             type_bound_variables ~profile (t1, x, t2))
+          guards;
         (type_predicate ~profile goal).ty
       end
     | Pseparated tlist ->
@@ -970,7 +910,7 @@ let typing_visitor profile = object
        those errrors are stored in the table and warnings are raised at
        translation time *)
     ignore
-      (try type_named_predicate ~lenv p
+      (try type_named_predicate ~profile p
        with Error.Not_yet _ | Error.Typing_error _  -> ());
     Cil.SkipChildren
 end

src/plugins/e-acsl/src/analyses/typing.mli

@@ -93,6 +93,11 @@ val join: number_ty -> number_ty -> number_ty
     semi-lattice. If one of the argument is {!Other}, the function assumes that
     the other argument is also {!Other}. In this case, the result is [Other]. *)
 
+val number_ty_bound_variable:
+  profile:Interval.profile ->
+  term * logic_var * term ->
+  number_ty
+
 (******************************************************************************)
 (** {2 Typing} *)
 (******************************************************************************)

src/plugins/e-acsl/src/code_generator/loops.ml

@@ -290,9 +290,9 @@ let rec mk_nested_loops ~loc mk_innermost_block kf env lscope_vars =
     Typing.preprocess_term ~use_gmp_opt:false ~logic_env t1;
     Typing.preprocess_term ~use_gmp_opt:false ~logic_env t2;
     let ctx =
-      let ty1 = Typing.get_number_ty ~logic_env t1 in
-      let ty2 = Typing.get_number_ty ~logic_env t2 in
-      Typing.join ty1 ty2
+      Typing.number_ty_bound_variable
+        ~profile:(Interval.Logic_environment.get_profile (Env.Logic_env.get env))
+        (t1, logic_x, t2)
     in
     let t_plus_one ?ty t =
       (* whenever provided, [ty] is known to be the type of the result *)

src/plugins/e-acsl/src/code_generator/quantif.ml

@@ -43,22 +43,23 @@ let predicate_to_exp_ref
    [has_empty_quantif_with_false_negative] partially detects such cases:
    Case 1: an empty quantification was detected for sure, return true.
    Case 2: we don't know, return false. *)
-let rec has_empty_quantif_with_false_negative = function
+let rec has_empty_quantif_with_false_negative ~logic_env = function
   | [] ->
     (* case 2 *)
     false
   | (t1, _, t2) :: guards ->
-    let iv1 = Interval.(extract_ival (get t1)) in
-    let iv2 = Interval.(extract_ival (get t2)) in
+    let iv1 = Interval.(extract_ival (get ~logic_env t1)) in
+    let iv2 = Interval.(extract_ival (get ~logic_env t2)) in
     let lower_bound, _ = Ival.min_and_max iv1 in
     let _, upper_bound = Ival.min_and_max iv2 in
     begin
       match lower_bound, upper_bound with
       | Some lower_bound, Some upper_bound ->
         let res  = lower_bound >= upper_bound in
-        res (* case 1 *) || has_empty_quantif_with_false_negative guards
+        res (* case 1 *) ||
+        has_empty_quantif_with_false_negative guards ~logic_env
       | None, _ | _, None ->
-        has_empty_quantif_with_false_negative guards
+        has_empty_quantif_with_false_negative guards ~logic_env
     end
 
 let () =
@@ -80,7 +81,11 @@ let convert kf env loc ~is_forall quantif =
       quantif
       Printer.pp_predicate
   in
-  match has_empty_quantif_with_false_negative bound_vars, is_forall with
+  match (has_empty_quantif_with_false_negative
+           ~logic_env:(Env.Logic_env.get env)
+           bound_vars),
+        is_forall
+  with
   | true, true ->
     Cil.one ~loc, env
   | true, false ->
@@ -96,14 +101,17 @@ let convert kf env loc ~is_forall quantif =
         else z, o, fun e -> Smart_exp.lnot ~loc:e.eloc e
       in
       (* transform [bound_vars] into [lscope_var list],
-         and update logic scope in the process *)
-      let lvs_guards, env = List.fold_right
-          (fun (t1, lv, t2) (lvs_guards, env) ->
+         and update logic scope and logic environment in the process *)
+      let lvs_guards, env = List.fold_left
+          (fun (lvs_guards, env) (t1, lv, t2) ->
              let lvs = Lvs_quantif (t1, Rle, lv, Rlt, t2) in
              let env = Env.Logic_scope.extend env lvs in
+             let logic_env = Env.Logic_env.get env in
+             let env = Env.Logic_env.add_let_quantif_binding env lv
+                 Interval.(join (get ~logic_env t1) (get ~logic_env t2)) in
              lvs :: lvs_guards, env)
-          bound_vars
           ([], env)
+          bound_vars
       in
       let var_res, res, env =
         (* variable storing the result of the quantifier *)
@@ -157,6 +165,12 @@ let convert kf env loc ~is_forall quantif =
       end_loop.labels <- label :: end_loop.labels;
       end_loop_ref := end_loop;
       let env = Env.add_stmt env end_loop in
+      let
+        env = List.fold_left
+          (fun env _ -> Env.Logic_env.pop env)
+          env
+          lvs_guards
+      in
       res, env
     end