Fixes Issue 69: unsound translation when bounds for quantified variables are...

Fixes Issue 69: unsound translation when bounds for quantified variables are bigger than their types

src/plugins/e-acsl/VERSION

-18.0+dev
+18.0-beta

src/plugins/e-acsl/doc/Changelog

@@ -23,6 +23,7 @@
 Plugin E-ACSL 18.0 (Argon)
 ##########################
 
+-* E-ACSL       [2018/11/13] Fix typing bug for quantified variables.
 -* runtime      [2018/11/13] Fix bug #!2405 about memory initialization
                 in presence of GCC constructors.
 -* E-ACSL       [2018/10/23] Fix bug #2406 about monitoring of variables

src/plugins/e-acsl/interval.ml

@@ -61,6 +61,7 @@ module Env = struct
   let clear () = Logic_var.Hashtbl.clear tbl
   let add = Logic_var.Hashtbl.add tbl
   let remove = Logic_var.Hashtbl.remove tbl
+  let replace = Logic_var.Hashtbl.replace tbl
   let find = Logic_var.Hashtbl.find tbl
 end
 

src/plugins/e-acsl/interval.mli

@@ -66,6 +66,7 @@ module Env: sig
   val clear: unit -> unit
   val add: Cil_types.logic_var -> Ival.t -> unit
   val remove: Cil_types.logic_var -> unit
+  val replace: Cil_types.logic_var -> Ival.t -> unit
 end
 
 (* ************************************************************************** *)

src/plugins/e-acsl/loops.ml

@@ -31,6 +31,10 @@ let translate_named_predicate_ref
   : (kernel_function -> Env.t -> predicate -> Env.t) ref
   = Extlib.mk_fun "translate_named_predicate_ref"
 
+let named_predicate_ref
+  : (kernel_function -> Env.t -> predicate -> exp * Env.t) ref
+  = Extlib.mk_fun "named_predicate_ref"
+
 let term_to_exp_ref
   : (kernel_function -> Env.t -> term -> exp * Env.t) ref
   = Extlib.mk_fun "term_to_exp_ref"
@@ -98,12 +102,74 @@ let preserve_invariant prj env kf stmt = match stmt.skind with
 (**************************** Nested loops ********************************)
 (**************************************************************************)
 
+(* It could happen that the bounds provided for a quantifier [lv] are bigger
+  than its type. [bounds_for_small_type] 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 bounds_for_small_type ~loc (t1, lv, t2) =
+  match lv.lv_type with
+  | Linteger ->
+    t1, t2, None
+  | Ctype ty ->
+    let i1 = Interval.infer t1 in
+    let i2 = Interval.infer t2 in
+    let i =
+      (* Ival.join would NOT be correct here:
+         Eg: (Ival.join [-3..-3] [300..300]) gives {-3, 300}
+             but NOT [-3..300] *)
+      Ival.inject_range (Ival.min_int i1) (Ival.max_int i2)
+    in
+    let ity = Interval.interv_of_typ ty in
+    if Ival.is_included i ity then
+      (* case 1 *)
+      t1, t2, None
+    else if Ival.is_singleton_int i1 && Ival.is_singleton_int i2 then begin
+      (* case 2 *)
+      let i = Ival.meet i ity in
+      (* now we potentially have a better interval for [lv]
+         ==> update the binding *)
+      Interval.Env.replace lv i;
+      (* the smaller bounds *)
+      let min, max = Misc.finite_min_and_max i in
+      let t1 = Logic_const.tint ~loc min in
+      let t2 = Logic_const.tint ~loc max in
+      let ctx = Typing.integer_ty_of_typ ty in
+      (* we are assured that we will not have a GMP,
+        once again because we intersected with [ity] *)
+      Typing.type_term ~use_gmp_opt:false ~ctx t1;
+      Typing.type_term ~use_gmp_opt:false ~ctx t2;
+      t1, t2, None
+    end else
+      (* case 3 *)
+      let min, max = Misc.finite_min_and_max 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 (Rle, lv_term, guard_upper) in
+      let guard = Logic_const.pand ~loc (guard_lower, guard_upper) in
+      t1, t2, Some guard
+  | Ltype _ | Lvar _ | Lreal | Larrow _ ->
+    Options.abort "quantification over non-integer type is not part of E-ACSL"
+
 let rec mk_nested_loops ~loc mk_innermost_block kf env lscope_vars =
   let term_to_exp = !term_to_exp_ref in
   match lscope_vars with
   | [] ->
     mk_innermost_block env
   | Lscope.Lvs_quantif(t1, rel1, logic_x, rel2, t2) :: lscope_vars' ->
+    let t1, t2, guard_for_small_type_opt =
+      bounds_for_small_type ~loc (t1, logic_x, t2)
+    in
     let ctx =
       let ty1 = Typing.get_integer_ty t1 in
       let ty2 = Typing.get_integer_ty t2 in
@@ -198,8 +264,6 @@ let rec mk_nested_loops ~loc mk_innermost_block kf env lscope_vars =
     let guard = block_to_stmt guard_blk in
     (* increment the loop counter [x++];
        previous typing ensures that [x++] fits type [ty] *)
-    (* TODO: should check that it does not overflow in the case of the type
-       of the loop variable is __declared__ too small. *)
     let tlv_one = t_plus_one ~ty:ctx_one tlv in
     let incr, env = term_to_exp kf (Env.push env) tlv_one in
     let next_blk, env = Env.pop_and_get
@@ -208,20 +272,32 @@ let rec mk_nested_loops ~loc mk_innermost_block kf env lscope_vars =
       ~global_clear:false
       Env.Middle
     in
-    (* remove logic binding now that the block is constructed *)
-    let env = Env.Logic_binding.remove env logic_x in
     (* generate the whole loop *)
-    let start = block_to_stmt init_blk in
     let next = block_to_stmt next_blk in
+    let stmts, env = match guard_for_small_type_opt with
+      | None ->
+        guard :: body @ [ next ], env
+      | Some p ->
+        let e, env = !named_predicate_ref kf (Env.push env) p in
+        let stmt, env =
+          Misc.mk_e_acsl_guard ~reverse:true Misc.RTE kf e p, env
+        in
+        let b, env = Env.pop_and_get env stmt ~global_clear:false Env.After in
+        let guard_for_small_type = Cil.mkStmt ~valid_sid:true (Block b) in
+        guard_for_small_type :: guard :: body @ [ next ], env
+    in
+    let start = block_to_stmt init_blk in
     let stmt = mkStmt
       ~valid_sid:true
       (Loop(
         [],
-        mkBlock (guard :: body @ [ next ]),
+        mkBlock stmts,
         loc,
         None,
         Some break_stmt))
     in
+    (* remove logic binding before returning *)
+    let env = Env.Logic_binding.remove env logic_x in
     [ start ;  stmt ], env
   | Lscope.Lvs_let(lv, t) :: lscope_vars' ->
     let ty = Typing.get_typ t in

src/plugins/e-acsl/loops.mli

@@ -62,6 +62,9 @@ val mk_nested_loops:
 val translate_named_predicate_ref:
   (kernel_function -> Env.t -> predicate -> Env.t) ref
 
+val named_predicate_ref:
+  (kernel_function -> Env.t -> predicate -> exp * Env.t) ref
+
 val term_to_exp_ref:
   (kernel_function -> Env.t -> term -> exp * Env.t) ref
 

src/plugins/e-acsl/misc.ml

@@ -311,6 +311,10 @@ let mk_ptr_sizeof typ loc =
   | TPtr (t', _) -> Cil.new_exp ~loc (SizeOf t')
   | _ -> assert false
 
+let finite_min_and_max i = match Ival.min_and_max i with
+  | Some min, Some max -> min, max
+  | None, _ | _, None -> assert false
+
 (*
 Local Variables:
 compile-command: "make"

src/plugins/e-acsl/misc.mli

@@ -124,6 +124,9 @@ val mk_ptr_sizeof: typ -> location -> exp
 (* [mk_ptr_sizeof ptr_typ loc] takes the pointer typ [ptr_typ] that points
    to a [typ] typ and returns [sizeof(typ)]. *)
 
+val finite_min_and_max: Ival.t -> Integer.t * Integer.t
+(* [finite_min_and_max i] takes the finite ival [i] and returns its bounds *)
+
 (*
 Local Variables:
 compile-command: "make"

src/plugins/e-acsl/tests/bts/issue69.c

+/* run.config
+   COMMENT: typing bug of Issue 69
+*/
+
+int main(void) {
+  /*@ assert \forall unsigned char c; 4 <= c <= 300 ==> 0 <= c <= 255; */ ;
+
+  int n = 5;
+  /*@ assert
+        \let m = n > 0 ? 4 : 341;
+        \forall char u; 1 < u < m ==> u > 0; */ ;
+}

src/plugins/e-acsl/tests/bts/oracle/gen_issue69.c

+/* Generated by Frama-C */
+#include "stdio.h"
+#include "stdlib.h"
+int main(void)
+{
+  int __retres;
+  __e_acsl_memory_init((int *)0,(char ***)0,(size_t)8);
+  /*@ assert ∀ unsigned char c; 4 ≤ c ≤ 300 ⇒ 0 ≤ c ≤ 255; */
+  {
+    int __gen_e_acsl_forall;
+    int __gen_e_acsl_c;
+    __gen_e_acsl_forall = 1;
+    __gen_e_acsl_c = (unsigned char)4;
+    while (1) {
+      if (__gen_e_acsl_c <= 255) ; else break;
+      {
+        int __gen_e_acsl_and;
+        if (0 <= __gen_e_acsl_c) __gen_e_acsl_and = __gen_e_acsl_c <= 255;
+        else __gen_e_acsl_and = 0;
+        if (__gen_e_acsl_and) ;
+        else {
+          __gen_e_acsl_forall = 0;
+          goto e_acsl_end_loop1;
+        }
+      }
+      __gen_e_acsl_c ++;
+    }
+    e_acsl_end_loop1: ;
+    __e_acsl_assert(__gen_e_acsl_forall,(char *)"Assertion",(char *)"main",
+                    (char *)"\\forall unsigned char c; 4 <= c <= 300 ==> 0 <= c <= 255",
+                    6);
+  }
+  int n = 5;
+  /*@ assert \let m = n > 0? 4: 341; ∀ char u; 1 < u < m ⇒ u > 0; */
+  {
+    int __gen_e_acsl_m;
+    int __gen_e_acsl_if;
+    int __gen_e_acsl_forall_2;
+    int __gen_e_acsl_u;
+    if (n > 0) __gen_e_acsl_if = 4; else __gen_e_acsl_if = 341;
+    __gen_e_acsl_m = __gen_e_acsl_if;
+    __gen_e_acsl_forall_2 = 1;
+    __gen_e_acsl_u = (char)1 + 1;
+    while (1) {
+      {
+        int __gen_e_acsl_and_2;
+        if (-128 <= __gen_e_acsl_u) __gen_e_acsl_and_2 = __gen_e_acsl_u <= 127;
+        else __gen_e_acsl_and_2 = 0;
+        __e_acsl_assert(__gen_e_acsl_and_2,(char *)"RTE",(char *)"main",
+                        (char *)"-128 <= u <= 127",11);
+      }
+      if (__gen_e_acsl_u < __gen_e_acsl_m) ; else break;
+      if (__gen_e_acsl_u > 0) ;
+      else {
+        __gen_e_acsl_forall_2 = 0;
+        goto e_acsl_end_loop2;
+      }
+      __gen_e_acsl_u ++;
+    }
+    e_acsl_end_loop2: ;
+    __e_acsl_assert(__gen_e_acsl_forall_2,(char *)"Assertion",(char *)"main",
+                    (char *)"\\let m = n > 0? 4: 341;\n\\forall char u; 1 < u < m ==> u > 0",
+                    10);
+  }
+  __retres = 0;
+  return __retres;
+}
+
+

src/plugins/e-acsl/tests/bts/oracle/issue69.res.oracle

+[e-acsl] beginning translation.
+[e-acsl] translation done in project "e-acsl".
+[eva:alarm] tests/bts/issue69.c:10: Warning: assertion got status unknown.

src/plugins/e-acsl/translate.ml

@@ -840,6 +840,7 @@ let named_predicate_to_exp ?name kf env p =
 let () =
   Loops.term_to_exp_ref := term_to_exp;
   Loops.translate_named_predicate_ref := translate_named_predicate;
+  Loops.named_predicate_ref := named_predicate_to_exp;
   Quantif.predicate_to_exp_ref := named_predicate_to_exp;
   At_with_lscope.term_to_exp_ref := term_to_exp;
   At_with_lscope.predicate_to_exp_ref := named_predicate_to_exp;