From d76168715a3f33559537d7df57f45cb926500b64 Mon Sep 17 00:00:00 2001
From: Julien Signoles <julien.signoles@cea.fr>
Date: Mon, 6 Jan 2020 11:13:23 +0100
Subject: [PATCH] [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 | 2 +
src/plugins/e-acsl/src/analyses/typing.ml | 43 ++++++++-----------
src/plugins/e-acsl/src/libraries/misc.ml | 13 ++++++
src/plugins/e-acsl/src/libraries/misc.mli | 3 ++
.../src/project_initializer/prepare_ast.ml | 11 +++++
.../src/project_initializer/prepare_ast.mli | 1 +
src/plugins/e-acsl/tests/memory/vla.c | 2 +-
7 files changed, 50 insertions(+), 25 deletions(-)
diff --git a/src/plugins/e-acsl/doc/Changelog b/src/plugins/e-acsl/doc/Changelog
index 78572f83775..0fea8bfb71a 100644
--- a/src/plugins/e-acsl/doc/Changelog
+++ b/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.
############################
diff --git a/src/plugins/e-acsl/src/analyses/typing.ml b/src/plugins/e-acsl/src/analyses/typing.ml
index fd7d0e6b967..b59e1c17593 100644
--- a/src/plugins/e-acsl/src/analyses/typing.ml
+++ b/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
diff --git a/src/plugins/e-acsl/src/libraries/misc.ml b/src/plugins/e-acsl/src/libraries/misc.ml
index 872847c39d4..97b2bea3cfa 100644
--- a/src/plugins/e-acsl/src/libraries/misc.ml
+++ b/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 ../../../../.."
diff --git a/src/plugins/e-acsl/src/libraries/misc.mli b/src/plugins/e-acsl/src/libraries/misc.mli
index 82d10e9d096..a39917f6cc1 100644
--- a/src/plugins/e-acsl/src/libraries/misc.mli
+++ b/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 ../../../../.."
diff --git a/src/plugins/e-acsl/src/project_initializer/prepare_ast.ml b/src/plugins/e-acsl/src/project_initializer/prepare_ast.ml
index d7988858a84..d015c335f8d 100644
--- a/src/plugins/e-acsl/src/project_initializer/prepare_ast.ml
+++ b/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 _ =
diff --git a/src/plugins/e-acsl/src/project_initializer/prepare_ast.mli b/src/plugins/e-acsl/src/project_initializer/prepare_ast.mli
index e3334623601..b23a84d6295 100644
--- a/src/plugins/e-acsl/src/project_initializer/prepare_ast.mli
+++ b/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]
diff --git a/src/plugins/e-acsl/tests/memory/vla.c b/src/plugins/e-acsl/tests/memory/vla.c
index 79b15c3475b..28b41333424 100644
--- a/src/plugins/e-acsl/tests/memory/vla.c
+++ b/src/plugins/e-acsl/tests/memory/vla.c
@@ -1,5 +1,5 @@
/* run.config
- COMMENT: Check variable-length arrays
+ COMMENT: check variable-length arrays
*/
int LEN = 10;
--
GitLab