[e-acsl] ensure that terms of the E-ACSL ast are never shared before code...

[e-acsl] ensure that terms of the E-ACSL ast are never shared before code injection. This invariant is required for E-ACSL typing soundness

src/plugins/e-acsl/doc/Changelog

@@ -19,6 +19,8 @@
 #   configure	configure
 ###############################################################################
 
+-* E-ACSL       [2020/01/06] Fix typing bug in presence of variable-length
+	        arrays that may lead to incorrect generated code.
 -* E-ACSL       [2019/12/04] Fix bug with compiler built-ins.
 
 ############################

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

@@ -182,42 +182,37 @@ module Memo: sig
   val clear: unit -> unit
 end = struct
 
-  module H = Hashtbl.Make(struct
-      type t = term
-      (* The comparison over terms is the physical equality. It cannot be the
-         structural one (given by [Cil_datatype.Term.equal]) because the very
-         same term can be used in 2 different contexts which lead to different
-         casts.
-
-         By construction, there are no physically equal terms in the AST
-         built by Cil. Consequently the memoisation should be fully
-         useless. However the translation of E-ACSL guarded quantification
-         generates new terms (see module {!Quantif}) which must be typed. The
-         term corresponding to the bound variable [x] is actually used twice:
-         once in the guard and once for encoding [x+1] when incrementing it. The
-         memoization is only useful here and indeed prevent the generation of
-         one extra variable in some cases. *)
-      let equal (t1:term) t2 = t1 == t2
-      let hash = Cil_datatype.Term.hash
-    end)
-
-  let tbl = H.create 97
+  (* The comparison over terms is the physical equality. It cannot be the
+     structural one (given by [Cil_datatype.Term.equal]) because the very same
+     term can be used in 2 different contexts which lead to different casts.
+
+     By construction (see prepare_ast.ml), there are no physically equal terms
+     in the E-ACSL's generated AST. Consequently the memoisation should be fully
+     useless. However:
+     - type info of many terms are accessed several times
+     - the translation of E-ACSL guarded quantifications generates
+     new terms (see module {!Quantif}) which must be typed. The term
+     corresponding to the bound variable [x] is actually used twice: once in the
+     guard and once for encoding [x+1] when incrementing it. The memoization is
+     only useful here and indeed prevent the generation of one extra variable in
+     some cases. *)
+  let tbl = Misc.Id_term.Hashtbl.create 97
 
   let get t =
-    try H.find tbl t
+    try Misc.Id_term.Hashtbl.find tbl t
     with Not_found ->
       Options.fatal
         "[typing] type of term '%a' was never computed."
         Printer.pp_term t
 
   let memo f t =
-    try H.find tbl t
+    try Misc.Id_term.Hashtbl.find tbl t
     with Not_found ->
       let x = f t in
-      H.add tbl t x;
+      Misc.Id_term.Hashtbl.add tbl t x;
       x
 
-  let clear () = H.clear tbl
+  let clear () = Misc.Id_term.Hashtbl.clear tbl
 
 end
 

src/plugins/e-acsl/src/libraries/misc.ml

@@ -219,6 +219,19 @@ let name_of_binop = function
   | MinusA -> "sub"
   | MinusPP | MinusPI | IndexPI | PlusPI -> assert false
 
+module Id_term =
+  Datatype.Make_with_collections
+    (struct
+      include Cil_datatype.Term
+      let name = "E_ACSL.Id_term"
+      let compare (t1:term) t2 =
+        if t1 == t2 then 0 else Cil_datatype.Term.compare t1 t2
+      let equal (t1:term) t2 = t1 == t2
+      let structural_descr = Structural_descr.t_abstract
+      let rehash = Datatype.identity
+      let mem_project = Datatype.never_any_project
+    end)
+
 (*
 Local Variables:
 compile-command: "make -C ../../../../.."

src/plugins/e-acsl/src/libraries/misc.mli

@@ -102,6 +102,9 @@ val name_of_binop: binop -> string
 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 *)
 
+module Id_term: Datatype.S_with_collections with type t = term
+(** datatype for terms that relies on physical equality *)
+
 (*
 Local Variables:
 compile-command: "make -C ../../../../.."

src/plugins/e-acsl/src/project_initializer/prepare_ast.ml

@@ -69,6 +69,17 @@ class prepare_visitor = object (self)
 
   val mutable has_new_stmt_in_fundec = false
   val mutable has_new_stmt = false
+  val terms = Misc.Id_term.Hashtbl.create 7
+
+  method !vterm _t =
+    Cil.DoChildrenPost
+      (fun t ->
+         if Misc.Id_term.Hashtbl.mem terms t then
+           (* remove term sharing for soundness of E-ACSL typing
+              (see typing.ml) *)
+           { t with term_node = t.term_node }
+         else
+           t)
 
   (* Add align attributes to local variables (required by temporal analysis) *)
   method !vblock _ =

src/plugins/e-acsl/src/project_initializer/prepare_ast.mli

@@ -23,6 +23,7 @@
 (** Prepare AST for E-ACSL generation.
 
     So for this module performs the following tasks:
+    - remove term sharing
     - move declarations of variables declared in the bodies of switch
       statements to upper scopes;
     - store what is necessary to translate in [Keep_status]

src/plugins/e-acsl/tests/memory/vla.c

 /* run.config
-   COMMENT: Check variable-length arrays
+   COMMENT: check variable-length arrays
 */
 
 int LEN = 10;