From 62c6da6137385dda9787f8129efe68d971ff23eb Mon Sep 17 00:00:00 2001
From: Julien Signoles <julien.signoles@cea.fr>
Date: Fri, 26 Apr 2013 07:39:49 +0000
Subject: [PATCH] [E-ACSL] dataflow: fixed bug in detecting variables of
 interest in annotations

---
 src/plugins/e-acsl/TODO                       |  5 +-
 src/plugins/e-acsl/pre_analysis.ml            | 49 ++++++++-----------
 .../tests/e-acsl-runtime/oracle/gen_valid.c   | 10 ++++
 .../tests/e-acsl-runtime/oracle/gen_valid2.c  | 10 ++++
 .../e-acsl-runtime/oracle/valid.1.res.oracle  |  2 +
 .../e-acsl-runtime/oracle/valid.res.oracle    |  2 +
 .../e-acsl/tests/e-acsl-runtime/valid.c       |  3 +-
 7 files changed, 50 insertions(+), 31 deletions(-)

diff --git a/src/plugins/e-acsl/TODO b/src/plugins/e-acsl/TODO
index c7d62398e69..040ac21002e 100644
--- a/src/plugins/e-acsl/TODO
+++ b/src/plugins/e-acsl/TODO
@@ -34,6 +34,9 @@
 - use checked assigns whenever possible in the analysis
   checked property = valid property or property for which code will be generated
 - RTE avec du code GMP
+- ne pas appeler __malloc et __free quand pas nécessaire. Nécessite d'avoir
+  malloc, __malloc, __e_acsl_malloc, __e_acsl__malloc (idem pour free)
+- analysis: optimize it by performing no join over sets anymore
 
 ##############
 # KNOWN BUGS #
@@ -55,8 +58,6 @@
 - \valid (or other memory-model constructs) in ensures of functions without code
 - function pointers 
   (in case of the pointing function has a behavior like in test ptr_init.c)
-- ne pas remplacer tous les appels à malloc/free par des 
-  __e_acsl_malloc/__eacsl_free. Ne le faire uniquement pour ceux monitorer.
 
 #######
 # DOC #
diff --git a/src/plugins/e-acsl/pre_analysis.ml b/src/plugins/e-acsl/pre_analysis.ml
index 2272cd6fbf1..85f7b2bdc74 100644
--- a/src/plugins/e-acsl/pre_analysis.ml
+++ b/src/plugins/e-acsl/pre_analysis.ml
@@ -161,28 +161,31 @@ module rec Transfer
     let ty = Cil.typeOf e in
     is_ptr_or_array ty
 
-  let rec register_term_lval kf varinfos (thost, _) = 
-    let add vi = 
-      if is_ptr_or_array vi.vtype then Varinfo.Set.add vi varinfos 
-      else varinfos
-    in
-    match thost with
+  let rec register_term_lval kf varinfos (thost, _) = match thost with
     | TVar { lv_origin = None } -> varinfos
-    | TVar { lv_origin = Some vi } -> add vi
-    | TResult _ -> add (Misc.result_vi kf)
+    | TVar { lv_origin = Some vi } -> Varinfo.Set.add vi varinfos
+    | TResult _ -> Varinfo.Set.add (Misc.result_vi kf) varinfos
     | TMem t -> register_term kf varinfos t
 
   and register_term kf varinfos term = match term.term_node with
-    | TConst _ | TSizeOf _ | TSizeOfE _ | TSizeOfStr _ | TAlignOf _
-    | TAlignOfE _ | Tnull | Ttype _ ->
-      varinfos
     | TLval tlv | TAddrOf tlv | TStartOf tlv -> 
       register_term_lval kf varinfos tlv
-    | TUnOp(_, t) | TCastE(_, t) | Tlambda(_, t) | Tat(t, _) | Tlet(_, t) ->
+    | TCastE(_, t) | Tat(t, _) | Tlet(_, t) ->
       register_term kf varinfos t
-    | TBinOp(_, t1, t2) | Tif(_, t1, t2) ->
-      let s = register_term kf varinfos t1 in
-      register_term kf s t2
+    | Tif(_, t1, t2) ->
+      let varinfos = register_term kf varinfos t1 in
+      register_term kf varinfos t2
+    | TBinOp((PlusPI | IndexPI | MinusPI), t1, t2) ->
+      (match t1.term_type with
+      | Ctype ty when is_ptr_or_array ty -> register_term kf varinfos t1
+      | _ -> 
+	match t2.term_type with
+	| Ctype ty when is_ptr_or_array ty -> register_term kf varinfos t2
+	| _ -> assert false)
+    | TConst _ | TSizeOf _ | TSizeOfE _ | TSizeOfStr _ | TAlignOf _
+    | TAlignOfE _ | Tnull | Ttype _ | TUnOp _ | TBinOp _ ->
+      varinfos
+    | Tlambda(_, _) -> Error.not_yet "lambda function"
     | Tapp(_, _, _) -> Error.not_yet "function application"
     | TDataCons _ -> Error.not_yet "data constructor"
     | Tbase_addr _ -> Error.not_yet "\\base_addr"
@@ -205,7 +208,7 @@ module rec Transfer
     | Pvalid(_, t) | Pvalid_read(_, t) | Pinitialized(_, t) ->
       (*	Options.feedback "REGISTER %a" Cil.d_term t;*)
       state_ref := register_term kf !state_ref t;
-      Cil.SkipChildren
+      Cil.DoChildren
     | Pallocable _ -> Error.not_yet "\\allocable"
     | Pfreeable _ -> Error.not_yet "\\freeable"
     | Pfresh _ -> Error.not_yet "\\fresh"
@@ -217,17 +220,7 @@ module rec Transfer
     method vterm term = match term.term_node with
     | Tbase_addr(_, t) | Toffset(_, t) | Tblock_length(_, t) ->
       state_ref := register_term kf !state_ref t;
-      Cil.SkipChildren
-    | TBinOp((PlusPI | IndexPI | MinusPI), t1, t2) ->
-      (match t1.term_type with
-      | Ctype ty when is_ptr_or_array ty ->
-	state_ref := register_term kf !state_ref t1
-      | _ -> 
-	match t2.term_type with
-	| Ctype ty when is_ptr_or_array ty ->
-	  state_ref := register_term kf !state_ref t2
-	| _ -> assert false);
-      Cil.SkipChildren
+      Cil.DoChildren
     | TConst _ | TSizeOf _ | TSizeOfStr _ | TAlignOf _  | Tnull | Ttype _ 
     | Tempty_set -> 
       (* no left-value inside inside: skip for efficiency *)
@@ -244,7 +237,7 @@ module rec Transfer
     | TMem t ->
       (* potential RTE *)
       state_ref := register_term kf !state_ref t;
-      Cil.SkipChildren
+      Cil.DoChildren
     | TVar _ | TResult _ -> 
       Cil.SkipChildren
   end
diff --git a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_valid.c b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_valid.c
index 6e1b00a2313..3c3134c100d 100644
--- a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_valid.c
+++ b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_valid.c
@@ -165,6 +165,7 @@ predicate diffSize{L1, L2}(ℤ i) =
 
 */
 int *X;
+int Z;
 /*@ requires \valid(x);
     ensures \valid(\result); */
 int *f(int *x)
@@ -227,6 +228,7 @@ int *__e_acsl_f(int *x)
 
 void e_acsl_global_init(void)
 {
+  __store_block((void *)(& Z),4U);
   __store_block((void *)(& X),4U);
   return;
 }
@@ -460,7 +462,15 @@ int main(void)
     e_acsl_assert(__e_acsl_and_24,(char *)"Assertion",(char *)"main",
                   (char *)"(!\\valid(a) && \\valid(b)) && \\valid(X)",37);
   }
+  /*@ assert \valid(&Z); */
+  {
+    int __e_acsl_valid_19;
+    __e_acsl_valid_19 = __valid((void *)(& Z),sizeof(int));
+    e_acsl_assert(__e_acsl_valid_19,(char *)"Assertion",(char *)"main",
+                  (char *)"\\valid(&Z)",38);
+  }
   __retres = 0;
+  __delete_block((void *)(& Z));
   __delete_block((void *)(& X));
   __delete_block((void *)(& n));
   __delete_block((void *)(& b));
diff --git a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_valid2.c b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_valid2.c
index 6e1b00a2313..3c3134c100d 100644
--- a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_valid2.c
+++ b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_valid2.c
@@ -165,6 +165,7 @@ predicate diffSize{L1, L2}(ℤ i) =
 
 */
 int *X;
+int Z;
 /*@ requires \valid(x);
     ensures \valid(\result); */
 int *f(int *x)
@@ -227,6 +228,7 @@ int *__e_acsl_f(int *x)
 
 void e_acsl_global_init(void)
 {
+  __store_block((void *)(& Z),4U);
   __store_block((void *)(& X),4U);
   return;
 }
@@ -460,7 +462,15 @@ int main(void)
     e_acsl_assert(__e_acsl_and_24,(char *)"Assertion",(char *)"main",
                   (char *)"(!\\valid(a) && \\valid(b)) && \\valid(X)",37);
   }
+  /*@ assert \valid(&Z); */
+  {
+    int __e_acsl_valid_19;
+    __e_acsl_valid_19 = __valid((void *)(& Z),sizeof(int));
+    e_acsl_assert(__e_acsl_valid_19,(char *)"Assertion",(char *)"main",
+                  (char *)"\\valid(&Z)",38);
+  }
   __retres = 0;
+  __delete_block((void *)(& Z));
   __delete_block((void *)(& X));
   __delete_block((void *)(& n));
   __delete_block((void *)(& b));
diff --git a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/valid.1.res.oracle b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/valid.1.res.oracle
index 8a2718b7566..7abc078baee 100644
--- a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/valid.1.res.oracle
+++ b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/valid.1.res.oracle
@@ -27,6 +27,7 @@ tests/e-acsl-runtime/valid.c:25:[e-acsl] warning: E-ACSL construct `\allocate' i
         __fc_heap_status ∈ [--..--]
         __memory_size ∈ [--..--]
         X ∈ {0}
+        Z ∈ {0}
 [value] using specification for function __store_block
 [value] using specification for function __full_init
 tests/e-acsl-runtime/valid.c:27:[value] Assertion got status valid.
@@ -78,6 +79,7 @@ tests/e-acsl-runtime/valid.c:37:[kernel] warning: accessing left-value that cont
 tests/e-acsl-runtime/valid.c:37:[kernel] warning: completely indeterminate value in a.
 tests/e-acsl-runtime/valid.c:37:[value] all evaluations are invalid for function call argument
         (void *)a
+tests/e-acsl-runtime/valid.c:38:[value] Assertion got status valid.
 [kernel] warning: Neither code nor specification for function __clean, generating default assigns from the prototype
 [value] using specification for function __clean
 [value] done for function main
diff --git a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/valid.res.oracle b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/valid.res.oracle
index 8a2718b7566..7abc078baee 100644
--- a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/valid.res.oracle
+++ b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/valid.res.oracle
@@ -27,6 +27,7 @@ tests/e-acsl-runtime/valid.c:25:[e-acsl] warning: E-ACSL construct `\allocate' i
         __fc_heap_status ∈ [--..--]
         __memory_size ∈ [--..--]
         X ∈ {0}
+        Z ∈ {0}
 [value] using specification for function __store_block
 [value] using specification for function __full_init
 tests/e-acsl-runtime/valid.c:27:[value] Assertion got status valid.
@@ -78,6 +79,7 @@ tests/e-acsl-runtime/valid.c:37:[kernel] warning: accessing left-value that cont
 tests/e-acsl-runtime/valid.c:37:[kernel] warning: completely indeterminate value in a.
 tests/e-acsl-runtime/valid.c:37:[value] all evaluations are invalid for function call argument
         (void *)a
+tests/e-acsl-runtime/valid.c:38:[value] Assertion got status valid.
 [kernel] warning: Neither code nor specification for function __clean, generating default assigns from the prototype
 [value] using specification for function __clean
 [value] done for function main
diff --git a/src/plugins/e-acsl/tests/e-acsl-runtime/valid.c b/src/plugins/e-acsl/tests/e-acsl-runtime/valid.c
index 1571c0b8a46..aaea64d15c4 100644
--- a/src/plugins/e-acsl/tests/e-acsl-runtime/valid.c
+++ b/src/plugins/e-acsl/tests/e-acsl-runtime/valid.c
@@ -10,7 +10,7 @@
 extern void *malloc(size_t p);
 extern void free(void* p);
 
-int *X;
+int *X, Z;
 
 /*@ requires \valid(x); 
   @ ensures \valid(\result); */
@@ -35,5 +35,6 @@ int main(void) {
   /*@ assert \valid(a) && \valid(b) && \valid(X); */
   free(a);
   /*@ assert ! \valid(a) && \valid(b) && \valid(X); */
+  /*@ assert \valid(&Z); */
   return 0;
 }
-- 
GitLab