little memoisation for integer constants

src/plugins/e-acsl/share/e_acsl.h

@@ -8,6 +8,10 @@
 
 // [TODO] ne pas gnrer les typedef si on veut linker avec GMP derrire
 
+// [TODO] utiliser un champ modle de type integer pour modliser
+// l'entier exact correspondant  un mpz_t.
+// Not yet implemented in ACSL.
+
 typedef struct {
   int _mp_alloc;
   int _mp_size;
@@ -20,9 +24,6 @@ typedef __mpz_struct mpz_t[1];
 /* GMP functions */
 /*****************/
 
-// [TODO] utiliser une variable modle de type integer pour modliser
-// l'entier exact correspondant  un mpz_t.
-
 /*@ ensures \valid(x);
   @ assigns *x; */
 extern void mpz_init(mpz_t x);

src/plugins/e-acsl/tests/e-acsl-runtime/oracle/integer_constant.res.oracle

@@ -2,19 +2,11 @@
 [value] Computing initial state
 [value] Initial state computed
 [value] Values of globals at initialization
-PROJECT_FILE:72:[value] Assertion got status valid.
+PROJECT_FILE:73:[value] Assertion got status valid.
 [value] computing for function mpz_init <-main.
         Called from PROJECT_FILE:74.
 PROJECT_FILE:74:[value] Function mpz_init: postcondition got status unknown
 [value] Done for function mpz_init
-[value] computing for function mpz_set_si <-main.
-        Called from PROJECT_FILE:74.
-PROJECT_FILE:74:[value] Function mpz_set_si: precondition got status valid
-[value] Done for function mpz_set_si
-[value] computing for function mpz_init <-main.
-        Called from PROJECT_FILE:75.
-PROJECT_FILE:75:[value] Function mpz_init: postcondition got status unknown
-[value] Done for function mpz_init
 [value] computing for function mpz_set_si <-main.
         Called from PROJECT_FILE:75.
 PROJECT_FILE:75:[value] Function mpz_set_si: precondition got status valid
@@ -26,11 +18,11 @@ PROJECT_FILE:76:[value] Function mpz_cmp: precondition got status valid
 [value] computing for function e_acsl_fail <-main.
         Called from PROJECT_FILE:77.
 [value] computing for function eprintf <-e_acsl_fail <-main.
-        Called from PROJECT_FILE:68.
+        Called from PROJECT_FILE:69.
 [value] Done for function eprintf
 [value] computing for function exit <-e_acsl_fail <-main.
-        Called from PROJECT_FILE:68.
-PROJECT_FILE:68:[value] Function exit: postcondition got status invalid
+        Called from PROJECT_FILE:69.
+PROJECT_FILE:69:[value] Function exit: postcondition got status invalid
 [value] Done for function exit
 [value] Recording results for e_acsl_fail
 [value] Done for function e_acsl_fail
@@ -38,9 +30,6 @@ PROJECT_FILE:68:[value] Function exit: postcondition got status invalid
         Called from PROJECT_FILE:78.
 PROJECT_FILE:78:[value] Function mpz_clear: precondition got status valid
 [value] Done for function mpz_clear
-[value] computing for function mpz_clear <-main.
-        Called from PROJECT_FILE:78.
-[value] Done for function mpz_clear
 PROJECT_FILE:81:[value] Assertion got status valid.
 [value] computing for function mpz_init <-main.
         Called from PROJECT_FILE:83.
@@ -65,10 +54,10 @@ PROJECT_FILE:85:[value] Function mpz_cmp: precondition got status valid
 [value] computing for function e_acsl_fail <-main.
         Called from PROJECT_FILE:86.
 [value] computing for function eprintf <-e_acsl_fail <-main.
-        Called from PROJECT_FILE:68.
+        Called from PROJECT_FILE:69.
 [value] Done for function eprintf
 [value] computing for function exit <-e_acsl_fail <-main.
-        Called from PROJECT_FILE:68.
+        Called from PROJECT_FILE:69.
 [value] Done for function exit
 [value] Recording results for e_acsl_fail
 [value] Done for function e_acsl_fail
@@ -92,7 +81,7 @@ PROJECT_FILE:87:[value] Function mpz_clear: precondition got status valid
 [from] Done for function eprintf
 [from] Computing for function exit <-e_acsl_fail
 [from] Done for function exit
-PROJECT_FILE:68:[from] Non terminating function (no dependencies)
+PROJECT_FILE:69:[from] Non terminating function (no dependencies)
 [from] Done for function e_acsl_fail
 [from] Computing for function mpz_clear
 [from] Done for function mpz_clear
@@ -139,29 +128,26 @@ void e_acsl_fail(char *msg )
 void main(void) 
 {
   /*@ assert (0 ≡ 0); */ ;
-  { mpz_t e_acsl_cst_1 ; mpz_t e_acsl_cst_2 ; int e_acsl_cst_3 ;
+  { mpz_t e_acsl_cst_1 ; int e_acsl_cst_2 ;
     mpz_init((__mpz_struct *)(e_acsl_cst_1));
     mpz_set_si((__mpz_struct *)(e_acsl_cst_1),(long )0);
-    mpz_init((__mpz_struct *)(e_acsl_cst_2));
-    mpz_set_si((__mpz_struct *)(e_acsl_cst_2),(long )0);
-    e_acsl_cst_3 = mpz_cmp((__mpz_struct *)(e_acsl_cst_1),
-                           (__mpz_struct *)(e_acsl_cst_2));
-    if (e_acsl_cst_3 != 0) { e_acsl_fail((char *)"((0 \342\211\241 0))"); }
-    mpz_clear((__mpz_struct *)(e_acsl_cst_2));
+    e_acsl_cst_2 = mpz_cmp((__mpz_struct *)(e_acsl_cst_1),
+                           (__mpz_struct *)(e_acsl_cst_1));
+    if (e_acsl_cst_2 != 0) { e_acsl_fail((char *)"((0 \342\211\241 0))"); }
     mpz_clear((__mpz_struct *)(e_acsl_cst_1));
   }
   
   /*@ assert (0 ≢ 1); */ ;
-  { mpz_t e_acsl_cst_4 ; mpz_t e_acsl_cst_5 ; int e_acsl_cst_6 ;
+  { mpz_t e_acsl_cst_3 ; mpz_t e_acsl_cst_4 ; int e_acsl_cst_5 ;
+    mpz_init((__mpz_struct *)(e_acsl_cst_3));
+    mpz_set_si((__mpz_struct *)(e_acsl_cst_3),(long )0);
     mpz_init((__mpz_struct *)(e_acsl_cst_4));
-    mpz_set_si((__mpz_struct *)(e_acsl_cst_4),(long )0);
-    mpz_init((__mpz_struct *)(e_acsl_cst_5));
-    mpz_set_si((__mpz_struct *)(e_acsl_cst_5),(long )1);
-    e_acsl_cst_6 = mpz_cmp((__mpz_struct *)(e_acsl_cst_4),
-                           (__mpz_struct *)(e_acsl_cst_5));
-    if (e_acsl_cst_6 == 0) { e_acsl_fail((char *)"((0 \342\211\242 1))"); }
-    mpz_clear((__mpz_struct *)(e_acsl_cst_5));
+    mpz_set_si((__mpz_struct *)(e_acsl_cst_4),(long )1);
+    e_acsl_cst_5 = mpz_cmp((__mpz_struct *)(e_acsl_cst_3),
+                           (__mpz_struct *)(e_acsl_cst_4));
+    if (e_acsl_cst_5 == 0) { e_acsl_fail((char *)"((0 \342\211\242 1))"); }
     mpz_clear((__mpz_struct *)(e_acsl_cst_4));
+    mpz_clear((__mpz_struct *)(e_acsl_cst_3));
   }
   
   return;

src/plugins/e-acsl/tests/e-acsl-runtime/oracle/not.res.oracle

@@ -2,7 +2,7 @@
 [value] Computing initial state
 [value] Initial state computed
 [value] Values of globals at initialization
-PROJECT_FILE:74:[value] Assertion got status valid.
+PROJECT_FILE:75:[value] Assertion got status valid.
 [value] Recording results for main
 [value] done for function main
 [dominators] computing for function main

src/plugins/e-acsl/tests/e-acsl-runtime/oracle/string_literal.res.oracle

@@ -2,7 +2,7 @@
 [value] Computing initial state
 [value] Initial state computed
 [value] Values of globals at initialization
-PROJECT_FILE:72:[value] Assertion got status valid.
+PROJECT_FILE:73:[value] Assertion got status valid.
 [value] Recording results for main
 [value] done for function main
 [dominators] computing for function main

src/plugins/e-acsl/tests/e-acsl-runtime/oracle/true.res.oracle

@@ -2,7 +2,7 @@
 [value] Computing initial state
 [value] Initial state computed
 [value] Values of globals at initialization
-PROJECT_FILE:74:[value] Assertion got status valid.
+PROJECT_FILE:75:[value] Assertion got status valid.
 [value] Recording results for main
 [value] done for function main
 [dominators] computing for function main

src/plugins/e-acsl/visit.ml

@@ -38,8 +38,7 @@ let not_yet s =
   Options.not_yet_implemented "construct `%s' is not yet supported" s
 
 (* [TODO] should not generate the type if the user wants to link the resulting
-   program with GMP: use an option for this purpose?
-   [TODO] transform the function to a constant? *)
+   program with GMP: use an option for this purpose? *)
 let e_acsl_header () = GText (Read_header.text ())
 
 (* Build a C conditional doing a runtime assertion check. *)
@@ -103,24 +102,41 @@ end = struct
      Could be a real issue in practice since **many** variables are generated
      for E-ACSL (at least one variable by integer constant). *)
 
+  (* Memoization is local to a stmt: thus it only merges multiple uses of one
+     constant in one stmt. *)
+  module H = Datatype.Int64.Hashtbl
+  let memo_tbl = H.create 7
+
   let var_cpt = ref 0
   let vlist = ref []
 
+  exception Unknown of int64 option
+
   let push is_global typ c =
-    incr var_cpt;
-    let v =
-      makeVarinfo
-	~logic:false
-	~generated:true
-	is_global
-	false (* is a formal? *)
-	("e_acsl_cst_" ^ string_of_int !var_cpt)
-	typ
-    in
-    vlist := (v, c) :: !vlist;
-    v
+    try
+      match c with
+      | None -> raise (Unknown None)
+      | Some (CInt64(n, _, _)) ->
+	(try H.find memo_tbl n
+	 with Not_found -> raise (Unknown (Some n)))
+      | Some (CStr _ | CWStr _ | CChr _ | CReal _ | CEnum _) -> assert false
+    with Unknown n ->
+      incr var_cpt;
+      let v =
+	makeVarinfo
+	  ~logic:false
+	  ~generated:true
+	  is_global
+	  false (* is a formal? *)
+	  ("e_acsl_cst_" ^ string_of_int !var_cpt)
+	  typ
+      in
+      (match n with None -> () | Some n -> H.add memo_tbl n v);
+      vlist := (v, c) :: !vlist;
+      v
 
   let finalize () =
+    H.clear memo_tbl;
     var_cpt := 0;
     let l = !vlist in
     vlist := [];
@@ -168,9 +184,7 @@ let mpz_t_ty = TNamed(mpz_t_torig, [])
 let is_mpz_t ty = Cil_datatype.Typ.equal ty mpz_t_ty
 
 let constant_to_exp is_global = function
-  | CInt64(_n, _, _) as c ->
-    (* [TODO] use memoization in order to create the minimum number of new
-       variables *)
+  | CInt64(_, _, _) as c ->
 (*    Options.debug ~level:3 "new variable for constant %S" (Int64.to_string n);*)
     mpz_t_torig.treferenced <- true;
     let v = New_vars.push is_global mpz_t_ty (Some c) in