Merge branch 'feature/thibaut/interval-conditionals' into 'master'

Improve inference for conditionals

See merge request frama-c/frama-c!3570

src/plugins/e-acsl/doc/Changelog

@@ -25,6 +25,7 @@
 Plugin E-ACSL <next-release>
 ############################
 
+- E-ACSL        [2022-19-07] Improve typing precision of variables appearing in comparisons
 -* E-ACSL       [2022-17-06] Fix wrong cast from pointer to integer (frama-c/frama-c#1119)
 
 ##############################

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

@@ -364,6 +364,11 @@ module Logic_env
   type t = { profile : Profile.t;
              let_quantif_bind : Profile.t}
 
+  (* forward reference to meet of intervals *)
+  let ival_meet_ref
+    : (ival -> ival -> ival) ref
+    = ref (fun _i1 _i2 -> Extlib.mk_labeled_fun "ival_meet_ref")
+
   let add env x i =
     { env with let_quantif_bind = Logic_var.Map.add  x i env.let_quantif_bind}
 
@@ -382,6 +387,24 @@ module Logic_env
 
   let get_profile env = env.profile
 
+  let refine env x ival =
+    let update = function
+      | None -> raise Not_found
+      | Some i -> Some (!ival_meet_ref i ival)
+    in
+    let new_lq_bind =
+      try Logic_var.Map.update x update env.let_quantif_bind
+      with Not_found ->
+      match Logic_var.Map.find_opt x env.profile with
+      | Some i ->
+        (* The profile must remain unchanged, so if the variable is bound in
+           the profile, we add the refined interval in the other bindings,
+           which are checked first when finding the interval *)
+        Logic_var.Map.add x (!ival_meet_ref i ival) env.let_quantif_bind
+      | None -> Options.abort "updating a variable not in environment"
+    in
+    {env with let_quantif_bind = new_lq_bind}
+
 end
 
 (* Imperative environment to perform fixpoint algorithm for recursive

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

@@ -76,17 +76,29 @@ module LFProf: Datatype.S_with_collections
     - an association list for variables bound by a let or a quantification *)
 module Logic_env : sig
   type t
-  (* add a new binding for a let or a quantification binder only *)
+
+  (** forward reference to meet of intervals *)
+  val ival_meet_ref : (ival -> ival -> ival) ref
+
+  (** add a new binding for a let or a quantification binder only *)
   val add : t -> logic_var -> ival -> t
-  (* the empty environment *)
+
+  (** the empty environment *)
   val empty : t
-  (* create a new environment from a profile, for function calls *)
+
+  (** create a new environment from a profile, for function calls *)
   val make : Profile.t -> t
-  (* find a logic variable in the environment *)
+
+  (** find a logic variable in the environment *)
   val find : t -> logic_var -> ival
-  (* get the profile of the logic environment, i.e. bindings through function
-     arguments *)
+
+  (** get the profile of the logic environment, i.e. bindings through function
+      arguments *)
   val get_profile : t -> Profile.t
+
+  (** refine the interval of a logic variable: replace an interval with a more
+      precise one *)
+  val refine : t -> logic_var -> ival -> t
 end
 
 

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

@@ -216,6 +216,8 @@ let meet i1 i2 = match i1, i2 with
   | Nan, (Ival _ | Float _ | Rational | Real) ->
     Nan
 
+let () = Logic_env.ival_meet_ref := meet
+
 let is_singleton_int = function
   | Ival iv -> Ival.is_singleton_int iv
   | Float _ | Rational | Real | Nan -> false
@@ -372,7 +374,8 @@ let rec fixpoint ~(infer : force:bool ->
     then
       ival
     else
-      fixpoint ~infer li args_ival t' inferred_ival
+      let assumed_ival = interv_of_typ_containing_interv inferred_ival in
+      fixpoint ~infer li args_ival t' assumed_ival
 
 
 (* Memoization module which retrieves the computed info of some terms *)
@@ -683,8 +686,11 @@ let rec infer ~force ~logic_env t =
       Error.map (fun src -> cast ~src ~dst) src
     | Tif (t1, t2, t3) ->
       ignore (infer ~force ~logic_env t1);
-      let i2 = infer ~force ~logic_env t2 in
-      let i3 = infer ~force ~logic_env t3 in
+      let logic_env_tbranch, logic_env_fbranch =
+        compute_logic_env_if_branches logic_env t1
+      in
+      let i2 = infer ~force ~logic_env:logic_env_tbranch t2 in
+      let i3 = infer ~force ~logic_env:logic_env_fbranch t3 in
       Error.map2 join i2 i3
     | Tat (t, _) ->
       get_res (infer ~force ~logic_env t)
@@ -873,7 +879,6 @@ and infer_term_host ~force ~logic_env thost =
         Printer.pp_typ ty
         Printer.pp_term t
 
-
 and infer_term_offset ~force ~logic_env t =
   match t with
   | TNoOffset -> ()
@@ -883,6 +888,65 @@ and infer_term_offset ~force ~logic_env t =
     ignore (infer ~force ~logic_env t);
     infer_term_offset ~force ~logic_env toff
 
+(* Update the interval of variables when they appear in a comparison of the form
+   [x op t] or [t op x] *)
+and compute_logic_env_if_branches logic_env t =
+  let get_res = Error.map (fun x -> x) in
+  let ival v = infer ~force:false ~logic_env v in
+  let add_ub logic_env x v =
+    let max = Ival.max_int (Error.map extract_ival (ival v)) in
+    Logic_env.refine logic_env x (Ival (Ival.inject_range None max))
+  in
+  let add_lb logic_env x v =
+    let min = Ival.min_int (Error.map extract_ival (ival v)) in
+    Logic_env.refine logic_env x (Ival (Ival.inject_range min None))
+  in
+  let add_eq logic_env x v = Logic_env.refine logic_env x (get_res (ival v)) in
+  let t_branch, f_branch =
+    (* we do not discriminate between strict and weak inequalities. This is
+       slighlty less precise but allow for better reusing of the code in the
+       case of recursive functions, the main advantage in typing
+       conditionals is for recursive functions. *)
+    match t.term_node with
+    | TBinOp(op, {term_node = TLval(TVar x, TNoOffset)}, v) ->
+      begin
+        match op with
+        | Lt | Le ->
+          add_ub logic_env x v,
+          add_lb logic_env x v
+        | Gt | Ge ->
+          add_lb logic_env x v,
+          add_ub logic_env x v
+        | Eq ->
+          add_eq logic_env x v,
+          logic_env
+        | Ne ->
+          logic_env,
+          add_eq logic_env x v
+        | _ -> logic_env, logic_env
+      end
+    | _ -> logic_env, logic_env
+  in
+  match t.term_node with
+  | TBinOp(op, u, {term_node = TLval(TVar y, TNoOffset)}) ->
+    begin
+      match op with
+      | Lt | Le ->
+        add_lb t_branch y u,
+        add_ub f_branch y u
+      | Gt | Ge ->
+        add_ub t_branch y u,
+        add_lb f_branch y u
+      | Eq ->
+        add_eq t_branch y u,
+        logic_env
+      | Ne ->
+        logic_env,
+        add_eq f_branch y u
+      | _ -> t_branch, f_branch
+    end
+  | _ -> t_branch, f_branch
+
 (* [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

src/plugins/e-acsl/tests/arith/oracle/at_on-purely-logic-variables.res.oracle

@@ -55,7 +55,7 @@
   accessing uninitialized left-value.
   assert
   \initialized(__gen_e_acsl_at_6 +
-               (int)((int)((int)(__gen_e_acsl_u_7 - 9) * 32) +
+               (int)((int)((int)(__gen_e_acsl_u_7 - 9) * 26) +
                      (int)(__gen_e_acsl_v_5 - -4)));
 [eva:alarm] at_on-purely-logic-variables.c:44: Warning: 
   assertion got status unknown.

src/plugins/e-acsl/tests/arith/oracle/functions_rec.res.oracle

@@ -3,127 +3,30 @@
 [eva:alarm] functions_rec.c:28: Warning: 
   function __e_acsl_assert, behavior blocking: precondition got status unknown.
 [eva:alarm] functions_rec.c:28: Warning: assertion got status unknown.
+[eva] functions_rec.c:10: Warning: 
+  Using specification of function __gen_e_acsl_f1 for recursive calls.
+  Analysis of function __gen_e_acsl_f1 is thus incomplete and its soundness
+  relies on the written specification.
 [eva:alarm] functions_rec.c:29: Warning: 
   function __e_acsl_assert, behavior blocking: precondition got status unknown.
 [eva:alarm] functions_rec.c:29: Warning: assertion got status unknown.
-[eva:alarm] functions_rec.c:10: Warning: 
-  accessing uninitialized left-value.
-  assert \initialized((__e_acsl_mpz_struct *)__gen_e_acsl_sub);
-[eva:alarm] functions_rec.c:10: Warning: 
-  accessing uninitialized left-value.
-  assert \initialized((__e_acsl_mpz_struct *)__gen_e_acsl_sub_2);
-[eva] functions_rec.c:10: Warning: 
-  Using specification of function __gen_e_acsl_f1_3 for recursive calls.
-  Analysis of function __gen_e_acsl_f1_3 is thus incomplete and its soundness
-  relies on the written specification.
 [eva:alarm] functions_rec.c:30: Warning: 
   function __e_acsl_assert, behavior blocking: precondition got status unknown.
 [eva:alarm] functions_rec.c:30: Warning: assertion got status unknown.
-[eva:alarm] functions_rec.c:13: Warning: 
-  accessing uninitialized left-value.
-  assert \initialized((__e_acsl_mpz_struct *)__gen_e_acsl_sub_3);
-[eva:alarm] functions_rec.c:13: Warning: 
-  accessing uninitialized left-value.
-  assert \initialized((__e_acsl_mpz_struct *)__gen_e_acsl_sub_4);
 [eva] functions_rec.c:13: Warning: 
-  Using specification of function __gen_e_acsl_f2_3 for recursive calls.
-  Analysis of function __gen_e_acsl_f2_3 is thus incomplete and its soundness
+  Using specification of function __gen_e_acsl_f2 for recursive calls.
+  Analysis of function __gen_e_acsl_f2 is thus incomplete and its soundness
   relies on the written specification.
-[eva:alarm] functions_rec.c:13: Warning: 
-  accessing uninitialized left-value.
-  assert \initialized((__e_acsl_mpz_struct *)__gen_e_acsl_sub_5);
 [eva] functions_rec.c:13: Warning: 
-  Using specification of function __gen_e_acsl_f2_3 for recursive calls.
-  Analysis of function __gen_e_acsl_f2_3 is thus incomplete and its soundness
+  Using specification of function __gen_e_acsl_f2 for recursive calls.
+  Analysis of function __gen_e_acsl_f2 is thus incomplete and its soundness
   relies on the written specification.
-[eva:alarm] functions_rec.c:13: Warning: 
-  accessing uninitialized left-value.
-  assert \initialized((__e_acsl_mpz_struct *)__gen_e_acsl_sub_6);
 [eva] functions_rec.c:13: Warning: 
-  Using specification of function __gen_e_acsl_f2_3 for recursive calls.
-  Analysis of function __gen_e_acsl_f2_3 is thus incomplete and its soundness
+  Using specification of function __gen_e_acsl_f2 for recursive calls.
+  Analysis of function __gen_e_acsl_f2 is thus incomplete and its soundness
   relies on the written specification.
+[eva:alarm] functions_rec.c:13: Warning: assertion 'E_ACSL' got status unknown.
 [eva:alarm] functions_rec.c:13: Warning: 
   function __e_acsl_assert, behavior blocking: precondition got status unknown.
 [eva:alarm] functions_rec.c:13: Warning: 
-  division by zero. assert __gen_e_acsl_f2_9 != 0;
-[eva:alarm] functions_rec.c:13: Warning: 
-  signed overflow. assert -2147483648 <= __gen_e_acsl_f2_5 * __gen_e_acsl_f2_7;
-[eva:alarm] functions_rec.c:13: Warning: 
-  signed overflow. assert __gen_e_acsl_f2_5 * __gen_e_acsl_f2_7 <= 2147483647;
-[eva:alarm] functions_rec.c:13: Warning: 
-  signed overflow.
-  assert
-  (int)(__gen_e_acsl_f2_5 * __gen_e_acsl_f2_7) / __gen_e_acsl_f2_9 <=
-  2147483647;
-[eva:alarm] functions_rec.c:13: Warning: 
-  accessing uninitialized left-value.
-  assert \initialized((__e_acsl_mpz_struct *)__gen_e_acsl_sub_7);
-[eva:alarm] functions_rec.c:13: Warning: 
-  accessing uninitialized left-value.
-  assert \initialized((__e_acsl_mpz_struct *)__gen_e_acsl_sub_8);
-[eva:alarm] functions_rec.c:13: Warning: 
-  division by zero. assert __gen_e_acsl_f2_14 != 0;
-[eva:alarm] functions_rec.c:13: Warning: 
-  signed overflow.
-  assert -2147483648 <= __gen_e_acsl_f2_10 * __gen_e_acsl_f2_12;
-[eva:alarm] functions_rec.c:13: Warning: 
-  signed overflow.
-  assert __gen_e_acsl_f2_10 * __gen_e_acsl_f2_12 <= 2147483647;
-[eva:alarm] functions_rec.c:13: Warning: 
-  signed overflow.
-  assert
-  (int)(__gen_e_acsl_f2_10 * __gen_e_acsl_f2_12) / __gen_e_acsl_f2_14 <=
-  2147483647;
-[eva:alarm] functions_rec.c:13: Warning: 
-  division by zero. assert __gen_e_acsl_f2_19 != 0;
-[eva:alarm] functions_rec.c:13: Warning: 
-  signed overflow.
-  assert -2147483648 <= __gen_e_acsl_f2_15 * __gen_e_acsl_f2_17;
-[eva:alarm] functions_rec.c:13: Warning: 
-  signed overflow.
-  assert __gen_e_acsl_f2_15 * __gen_e_acsl_f2_17 <= 2147483647;
-[eva:alarm] functions_rec.c:13: Warning: 
-  signed overflow.
-  assert
-  (int)(__gen_e_acsl_f2_15 * __gen_e_acsl_f2_17) / __gen_e_acsl_f2_19 <=
-  2147483647;
-[eva:alarm] functions_rec.c:32: Warning: 
-  function __e_acsl_assert, behavior blocking: precondition got status unknown.
-[eva:alarm] functions_rec.c:32: Warning: assertion got status unknown.
-[eva:alarm] functions_rec.c:17: Warning: 
-  accessing uninitialized left-value.
-  assert \initialized((__e_acsl_mpz_struct *)__gen_e_acsl_sub_9);
-[eva:alarm] functions_rec.c:17: Warning: 
-  accessing uninitialized left-value.
-  assert \initialized((__e_acsl_mpz_struct *)__gen_e_acsl_sub_10);
-[eva] functions_rec.c:17: Warning: 
-  Using specification of function __gen_e_acsl_f3_3 for recursive calls.
-  Analysis of function __gen_e_acsl_f3_3 is thus incomplete and its soundness
-  relies on the written specification.
-[eva:alarm] functions_rec.c:17: Warning: 
-  accessing uninitialized left-value.
-  assert \initialized((__e_acsl_mpz_struct *)__gen_e_acsl_add_4);
-[eva:alarm] functions_rec.c:34: Warning: assertion got status unknown.
-[eva:alarm] functions_rec.c:20: Warning: 
-  accessing uninitialized left-value.
-  assert \initialized((__e_acsl_mpz_struct *)__gen_e_acsl_add_6);
-[eva:alarm] functions_rec.c:20: Warning: 
-  accessing uninitialized left-value.
-  assert \initialized((__e_acsl_mpz_struct *)__gen_e_acsl_add_7);
-[eva] functions_rec.c:20: Warning: 
-  Using specification of function __gen_e_acsl_f4_3 for recursive calls.
-  Analysis of function __gen_e_acsl_f4_3 is thus incomplete and its soundness
-  relies on the written specification.
-[eva:alarm] functions_rec.c:36: Warning: 
-  function __e_acsl_assert, behavior blocking: precondition got status unknown.
-[eva:alarm] functions_rec.c:36: Warning: assertion got status unknown.
-[eva:alarm] functions_rec.c:38: Warning: 
-  function __e_acsl_assert, behavior blocking: precondition got status unknown.
-[eva:alarm] functions_rec.c:38: Warning: assertion got status unknown.
-[eva:alarm] functions_rec.c:40: Warning: 
-  function __e_acsl_assert_register_mpz: precondition data->values == \null ||
-                                                      \valid(data->values) got status unknown.
-[eva:alarm] functions_rec.c:40: Warning: 
-  function __e_acsl_assert, behavior blocking: precondition got status unknown.
-[eva:alarm] functions_rec.c:40: Warning: assertion got status unknown.
+  accessing uninitialized left-value. assert \initialized(&n);

src/plugins/e-acsl/tests/arith/oracle/gen_at_on-purely-logic-variables.c

@@ -113,7 +113,7 @@ int main(void)
   __e_acsl_memory_init((int *)0,(char ***)0,8UL);
   __gen_e_acsl_at_8 = (long *)malloc(64UL);
   __gen_e_acsl_at_7 = (int *)malloc(12000UL);
-  __gen_e_acsl_at_6 = (long *)malloc(3072UL);
+  __gen_e_acsl_at_6 = (long *)malloc(2496UL);
   __gen_e_acsl_at_5 = (int *)malloc(528UL);
   __gen_e_acsl_at_3 = (int *)malloc(12UL);
   __gen_e_acsl_at_2 = (long *)malloc(8UL);
@@ -182,7 +182,7 @@ int main(void)
           else __gen_e_acsl_if_2 = 3;
           if (__gen_e_acsl_v_2 <= __gen_e_acsl_if_2) ; else break;
         }
-        *(__gen_e_acsl_at_6 + ((__gen_e_acsl_u_2 - 9) * 32 + (__gen_e_acsl_v_2 - -4))) = 
+        *(__gen_e_acsl_at_6 + ((__gen_e_acsl_u_2 - 9) * 26 + (__gen_e_acsl_v_2 - -4))) = 
         (n + (long)__gen_e_acsl_u_2) + __gen_e_acsl_v_2;
         __gen_e_acsl_v_2 ++;
       }
@@ -547,7 +547,7 @@ int main(void)
                                                             __gen_e_acsl_at_6 + (int)(
                                                             (long)((int)(
                                                             (long)((int)(
-                                                            __gen_e_acsl_u_7 - 9L)) * 32L)) + (int)(
+                                                            __gen_e_acsl_u_7 - 9L)) * 26L)) + (int)(
                                                             __gen_e_acsl_v_5 - -4L))),
                                                             sizeof(long),
                                                             (void *)__gen_e_acsl_at_6,
@@ -565,7 +565,7 @@ int main(void)
                                            "sizeof(long)",0,sizeof(long));
             __gen_e_acsl_assert_data_12.blocking = 1;
             __gen_e_acsl_assert_data_12.kind = "RTE";
-            __gen_e_acsl_assert_data_12.pred_txt = "\\valid_read(__gen_e_acsl_at_6 +\n            (int)((int)((int)(__gen_e_acsl_u_7 - 9) * 32) +\n                  (int)(__gen_e_acsl_v_5 - -4)))";
+            __gen_e_acsl_assert_data_12.pred_txt = "\\valid_read(__gen_e_acsl_at_6 +\n            (int)((int)((int)(__gen_e_acsl_u_7 - 9) * 26) +\n                  (int)(__gen_e_acsl_v_5 - -4)))";
             __gen_e_acsl_assert_data_12.file = "at_on-purely-logic-variables.c";
             __gen_e_acsl_assert_data_12.fct = "main";
             __gen_e_acsl_assert_data_12.line = 46;
@@ -576,10 +576,10 @@ int main(void)
             /*@ assert
                 Eva: initialization:
                   \initialized(__gen_e_acsl_at_6 +
-                               (int)((int)((int)(__gen_e_acsl_u_7 - 9) * 32)
+                               (int)((int)((int)(__gen_e_acsl_u_7 - 9) * 26)
                                      + (int)(__gen_e_acsl_v_5 - -4)));
             */
-            if (*(__gen_e_acsl_at_6 + ((__gen_e_acsl_u_7 - 9) * 32 + (
+            if (*(__gen_e_acsl_at_6 + ((__gen_e_acsl_u_7 - 9) * 26 + (
                                        __gen_e_acsl_v_5 - -4))) > 0L) 
               ;
             else {