From c9f1976fa0b56feb5ee1ef003a01fd1df8e4ec40 Mon Sep 17 00:00:00 2001
From: Fonenantsoa Maurica <maurica.fonenantsoa@gmail.com>
Date: Wed, 12 Sep 2018 14:48:25 +0200
Subject: [PATCH] Addresses Julien's review no.1: - No superfluous white space
- No camel case - No unauthorized open - Longic_const.tinteger -> Cil.lone,
Cil.lzero - lscope -> Lscope.t - lscope becomes abstract - 'with non-void
logic scope' -> 'on purely logical variables' - Make lscope be part of env -
Discard all the translation in a new module: At_with_lscope - No extra
variable for size - Cil.(theMachine.typeOfSizeOf) instead of Cil.intType - No
superfluous block for storing_loops - mem_infos -> memory_infos - Prevent GMP
result (actually already done previously) - record for malloc and free -
H_malloc_free = Cil_datatype.Fundec.Hashtbl - dedicated
insert_malloc_and_free_stmts in Visit - Kernel_function.is_entry_point for
testing main function - no visit in term_has_lv_from_vi and
effective_lscope_from_pot - term_has_lv_from_vi moved to Misc - Passing kf to
add_malloc_and_free_stmt instead of fundec - Less @ during the insertion of
free stmts - ty_array -> ty_ptr - Typos - Comments on: - Exported functions
in MLIs - Computation of pre in put_block_at_label - Use of global scope
for Env.Varname.get - Description of mk_storing_loops - New binding in
mk_storing_loops - Description of effective_lscope_from_pred_or_term -
Motivation of the over-approximation on t_size
---
src/plugins/e-acsl/Makefile.in | 3 +-
src/plugins/e-acsl/at_with_lscope.ml | 413 ++++++++++++
src/plugins/e-acsl/at_with_lscope.mli | 67 ++
src/plugins/e-acsl/env.ml | 13 +-
src/plugins/e-acsl/env.mli | 10 +
src/plugins/e-acsl/lscope.ml | 79 +--
src/plugins/e-acsl/lscope.mli | 35 +-
src/plugins/e-acsl/misc.ml | 17 +
src/plugins/e-acsl/misc.mli | 6 +
src/plugins/e-acsl/quantif.ml | 39 +-
src/plugins/e-acsl/quantif.mli | 8 +-
.../full-mmodel-only/at_logic-variables.c | 4 +-
.../oracle/at_logic-variables.res.oracle | 2 +-
.../oracle/gen_at_logic-variables.c | 41 +-
src/plugins/e-acsl/translate.ml | 588 ++++--------------
src/plugins/e-acsl/typing.mli | 3 +-
src/plugins/e-acsl/visit.ml | 89 +--
17 files changed, 788 insertions(+), 629 deletions(-)
create mode 100644 src/plugins/e-acsl/at_with_lscope.ml
create mode 100644 src/plugins/e-acsl/at_with_lscope.mli
diff --git a/src/plugins/e-acsl/Makefile.in b/src/plugins/e-acsl/Makefile.in
index cbf6f25d1a9..adfb3eccf89 100644
--- a/src/plugins/e-acsl/Makefile.in
+++ b/src/plugins/e-acsl/Makefile.in
@@ -69,13 +69,14 @@ PLUGIN_CMO:= local_config \
mmodel_analysis \
exit_points \
label \
+ lscope \
env \
keep_status \
dup_functions \
interval \
typing \
- lscope \
quantif \
+ at_with_lscope \
translate \
temporal \
prepare_ast \
diff --git a/src/plugins/e-acsl/at_with_lscope.ml b/src/plugins/e-acsl/at_with_lscope.ml
new file mode 100644
index 00000000000..66b9987aead
--- /dev/null
+++ b/src/plugins/e-acsl/at_with_lscope.ml
@@ -0,0 +1,413 @@
+(**************************************************************************)
+(* *)
+(* This file is part of Frama-C. *)
+(* *)
+(* Copyright (C) 2007-2018 *)
+(* CEA (Commissariat à l'énergie atomique et aux énergies *)
+(* alternatives) *)
+(* *)
+(* you can redistribute it and/or modify it under the terms of the GNU *)
+(* Lesser General Public License as published by the Free Software *)
+(* Foundation, version 2.1. *)
+(* *)
+(* It is distributed in the hope that it will be useful, *)
+(* but WITHOUT ANY WARRANTY; without even the implied warranty of *)
+(* MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the *)
+(* GNU Lesser General Public License for more details. *)
+(* *)
+(* See the GNU Lesser General Public License version 2.1 *)
+(* for more details (enclosed in the file licenses/LGPLv2.1). *)
+(* *)
+(**************************************************************************)
+
+open Cil_types
+
+(**************************************************************************)
+(********************** Forward references ********************************)
+(**************************************************************************)
+
+let predicate_to_exp_ref
+ : (kernel_function -> Env.t -> predicate -> exp * Env.t) ref
+ = Extlib.mk_fun "named_predicate_to_exp_ref"
+
+let term_to_exp_ref
+ : (kernel_function -> Env.t -> term -> exp * Env.t) ref
+ = Extlib.mk_fun "term_to_exp_ref"
+
+(*****************************************************************************)
+(**************************** Handling memory ********************************)
+(*****************************************************************************)
+
+module H_malloc_free = Cil_datatype.Fundec.Hashtbl
+
+type malloc_and_free_stmts = {
+ mf_malloc : stmt;
+ mf_free : stmt
+}
+
+let tbl_malloc_free : (stmt list * stmt list) H_malloc_free.t =
+ (* The first (resp.second) list is for malloc (resp. free) stmts *)
+ H_malloc_free.create 7
+
+let add_malloc_and_free_stmts kf mf =
+ match kf.fundec with
+ | Definition(fundec, _) ->
+ begin try
+ let malloc_stmts, free_stmts =
+ H_malloc_free.find tbl_malloc_free fundec
+ in
+ H_malloc_free.replace
+ tbl_malloc_free
+ fundec
+ (mf.mf_malloc :: malloc_stmts, mf.mf_free :: free_stmts)
+ with Not_found ->
+ H_malloc_free.add tbl_malloc_free fundec ([mf.mf_malloc], [mf.mf_free])
+ end
+ | Declaration _ ->
+ assert false
+
+let get_malloc_and_free_stmts fundec =
+ try H_malloc_free.find tbl_malloc_free fundec
+ with Not_found -> [], []
+
+(**************************************************************************)
+(*************************** Translation **********************************)
+(**************************************************************************)
+
+(* Make Lvs_quantif(tmin, lv, tmax) correspond to (t_size, t_shifted)
+ where t_size = tmax - tmin + 1 (+1 because the inequalities are large
+ due to previous normalization)
+ and t_shifted = lv - tmin (so that we start indexing at 0) *)
+let rec memory_infos_from_quantifs ~loc kf env lscope res =
+ match Lscope.top lscope with
+ | None ->
+ res, env
+ | Some(lscope_var, lscope') ->
+ match lscope_var with
+ | Lscope.Lvs_quantif(tmin, _, tmax)
+ when (Misc.term_has_lv_from_vi tmin)
+ || (Misc.term_has_lv_from_vi tmax) ->
+ Error.not_yet "\\at with logic variable linked to C variable"
+ | Lscope.Lvs_quantif(tmin, lv, tmax) ->
+ let t_size = Logic_const.term
+ ~loc (TBinOp(MinusA, tmax, tmin)) Linteger
+ in
+ let t_size = Logic_const.term
+ ~loc (TBinOp(PlusA, t_size, Cil.lone ~loc ())) Linteger
+ in
+ let i = Interval.infer t_size in
+ (* The amount of memory we allocate depends on the precision of
+ the interval inference. We need to do this over-approximation
+ because the bounds [tmax] and [tmin] can be terms that are so complex
+ that we cannot precisely determine the precise value of [t_size] *)
+ let t_size = match Ival.min_and_max i with
+ | Some _, Some max ->
+ Logic_const.tint ~loc max
+ | _ ->
+ Error.not_yet
+ ("\\at on purely logical variables and with quantifier that uses " ^
+ "too complex bound " ^
+ "(E-ACSL cannot infer a finite upper bound to it)")
+ in
+ (* Index *)
+ let t_lv = Logic_const.tvar ~loc lv in
+ let t_shifted = Logic_const.term
+ ~loc (TBinOp(MinusA, t_lv, tmin)) Linteger
+ in
+ (* Returning *)
+ let res = (t_size, t_shifted) :: res in
+ memory_infos_from_quantifs ~loc kf env lscope' res
+ | Lscope.Lvs_let(_, t) | Lscope.Lvs_global(_, t)
+ when (Misc.term_has_lv_from_vi t) ->
+ Error.not_yet "\\at with logic variable linked to C variable"
+ | Lscope.Lvs_let _ ->
+ memory_infos_from_quantifs ~loc kf env lscope' res
+ | Lscope.Lvs_formal _ ->
+ Error.not_yet "\\at using formal variable of a logic function"
+ | Lscope.Lvs_global _ ->
+ Error.not_yet "\\at using global logic variable"
+
+let size_from_memory_infos ~loc memory_infos =
+ List.fold_left
+ (fun t_size (t_s, _) ->
+ Logic_const.term ~loc (TBinOp(Mult, t_size, t_s)) Linteger)
+ (Cil.lone ~loc ())
+ memory_infos
+
+(* [mk_storing_loops] creates the nested loops that are used to store the
+ different possible values of [pot].
+ These loops are similar to those generated by [Quantif], with the difference
+ that the aim of the innermost block is to store values,
+ not to check the validity of some (quantified) predicate. *)
+let rec mk_storing_loops ~loc kf env lscope lval pot =
+ let term_to_exp = !term_to_exp_ref in
+ let named_predicate_to_exp = !predicate_to_exp_ref in
+ match Lscope.top lscope with
+ | None ->
+ begin match pot with
+ | Misc.PoT_pred p ->
+ let e, env = named_predicate_to_exp kf (Env.push env) p in
+ let storing_stmt =
+ Cil.mkStmtOneInstr ~valid_sid:true (Set(lval, e, loc))
+ in
+ let block, env = Env.pop_and_get
+ env storing_stmt ~global_clear:true Env.After
+ in
+ block, env
+ | Misc.PoT_term t ->
+ begin match Typing.get_integer_ty t with
+ | Typing.C_type _ | Typing.Other ->
+ let e, env = term_to_exp kf (Env.push env) t in
+ let storing_stmt =
+ Cil.mkStmtOneInstr ~valid_sid:true (Set(lval, e, loc))
+ in
+ let block, env = Env.pop_and_get
+ env storing_stmt ~global_clear:true Env.After
+ in
+ block, env
+ | Typing.Gmp ->
+ Error.not_yet "\\at on purely logical variables and over gmp type"
+ end
+ end
+ | Some(Lscope.Lvs_quantif(tmin, lv, tmax), lscope') ->
+ (* TODO: a refactor with [Quantif] may be possible for this case *)
+ let vi_of_lv = Env.Logic_binding.get env lv in
+ let env = Env.push env in
+ let vi_of_lv, _, env =
+ (* We need to redeclare the lv thus new varinfo needed *)
+ Env.Logic_binding.add ~ty:vi_of_lv.vtype env lv
+ in
+ let t_lv = Logic_const.tvar ~loc lv in
+ (* Guard *)
+ let guard = Logic_const.term
+ ~loc
+ (TBinOp(Le, t_lv, tmax))
+ (Ctype Cil.intType)
+ in
+ Typing.type_term ~use_gmp_opt:false ~ctx:Typing.c_int guard;
+ let guard_exp, env = term_to_exp kf env guard in
+ (* Break *)
+ let break_stmt = Cil.mkStmt ~valid_sid:true (Break guard_exp.eloc) in
+ (* Inner loop *)
+ let loop', env = mk_storing_loops ~loc kf env lscope' lval pot in
+ let loop' = Cil.mkStmt ~valid_sid:true (Block loop') in
+ (* Loop counter *)
+ let plus_one_term = Logic_const.term
+ ~loc
+ (TBinOp(PlusA, t_lv, Cil.lone ~loc ()))
+ Linteger
+ in
+ Typing.type_term ~use_gmp_opt:true plus_one_term;
+ let plus_one_exp, env = term_to_exp kf env plus_one_term in
+ let plus_one_stmt = match Typing.get_integer_ty plus_one_term with
+ | Typing.C_type _ | Typing.Gmp->
+ Gmpz.init_set ~loc (Cil.var vi_of_lv) (Cil.evar vi_of_lv) plus_one_exp
+ | Typing.Other ->
+ assert false
+ in
+ (* If guard is satisfiable then inner loop, else break *)
+ let if_stmt = Cil.mkStmt
+ ~valid_sid:true
+ (If(guard_exp,
+ Cil.mkBlock [loop'; plus_one_stmt],
+ Cil.mkBlock [ break_stmt ],
+ guard_exp.eloc))
+ in
+ let loop = Cil.mkStmt
+ ~valid_sid:true
+ (Loop ([],
+ Cil.mkBlock [ if_stmt ],
+ loc,
+ None,
+ Some break_stmt))
+ in
+ (* Init lv *)
+ let tmin_exp, env = term_to_exp kf env tmin in
+ let set_tmin = match Typing.get_integer_ty plus_one_term with
+ | Typing.C_type _ | Typing.Gmp->
+ Gmpz.init_set ~loc (Cil.var vi_of_lv) (Cil.evar vi_of_lv) tmin_exp
+ | Typing.Other ->
+ assert false
+ in
+ (* The whole block *)
+ let block' = Cil.mkBlock [set_tmin; loop] in
+ let block'_stmt = Cil.mkStmt ~valid_sid:true (Block block') in
+ let block, env = Env.pop_and_get
+ env block'_stmt ~global_clear:true Env.After
+ in
+ block, env
+ | Some(Lscope.Lvs_let(lv, t), lscope') ->
+ let vi_of_lv = Env.Logic_binding.get env lv in
+ let env = Env.push env in
+ let vi_of_lv, exp_of_lv, env =
+ (* We need to redeclare the lv thus new varinfo needed *)
+ Env.Logic_binding.add ~ty:vi_of_lv.vtype env lv
+ in
+ let e, env = term_to_exp kf env t in
+ let let_stmt = Gmpz.init_set
+ ~loc (Cil.var vi_of_lv) exp_of_lv e
+ in
+ let block', env = mk_storing_loops ~loc kf env lscope' lval pot in
+ (* The whole block *)
+ block'.bstmts <- let_stmt :: block'.bstmts;
+ let block'_stmt = Cil.mkStmt ~valid_sid:true (Block block') in
+ let block, env = Env.pop_and_get
+ env block'_stmt ~global_clear:true Env.After
+ in
+ block, env
+ | Some(Lscope.Lvs_formal _, _) ->
+ Error.not_yet "\\at using formal variable of a logic function"
+ | Some(Lscope.Lvs_global _, _) ->
+ Error.not_yet "\\at using global logic variable"
+
+(* Associate to each possible tuple of quantifiers
+ a unique index from the set {n | 0 <= n < n_max}.
+ That index will serve to identify the memory location where the evaluation
+ of the term/predicate is stored for the given tuple of quantifier.
+ The following gives the smallest set of such indexes (hence we use the
+ smallest amount of memory in some respect):
+ To (t_shifted_n, t_shifted_n-1, ..., t_shifted_1)
+ where 0 <= t_shifted_i < beta_i
+ corresponds:
+ sum_from_i_eq_1_to_n(
+ t_shifted_i *
+ mult_from_j_eq_1_to_i-1(beta_j)
+ ) *)
+let rec index_from_mem_infos ~loc memory_infos =
+ match memory_infos with
+ | [] ->
+ Cil.lzero ~loc ()
+ | [(_, t_shifted)] ->
+ t_shifted
+ | (_, t_shifted) :: memory_infos' ->
+ let index' = index_from_mem_infos ~loc memory_infos' in
+ let bi = t_shifted in
+ let rec pi_beta_j memory_infos = match memory_infos with
+ | [] ->
+ Cil.lone ~loc ()
+ | (t_size, _) :: memory_infos' ->
+ let pi_beta_j' = pi_beta_j memory_infos' in
+ Logic_const.term ~loc (TBinOp(Mult, t_size, pi_beta_j')) Linteger
+ in
+ let pi_beta_j = pi_beta_j memory_infos' in
+ let bi_mult_pi_beta_j = Logic_const.term ~loc
+ (TBinOp(Mult, bi, pi_beta_j)) Linteger
+ in
+ Logic_const.term ~loc (TBinOp(PlusA, bi_mult_pi_beta_j, index')) Linteger
+
+let put_block_at_label env block label =
+ let stmt = Label.get_stmt (Env.get_visitor env) label in
+ let env_ref = ref env in
+ let o = object
+ inherit Visitor.frama_c_inplace
+ method !vstmt_aux stmt =
+ assert (!env_ref == env);
+ let pre = match label with
+ (* This was just shamelessly copied from [at_to_exp],
+ with no much understanding... *)
+ | BuiltinLabel(Here | Post) -> true
+ | BuiltinLabel(Old | Pre | LoopEntry | LoopCurrent | Init)
+ | FormalLabel _ | StmtLabel _ -> false
+ in
+ env_ref := Env.extend_stmt_in_place env stmt ~pre block;
+ Cil.ChangeTo stmt
+ end
+ in
+ let bhv = Env.get_behavior env in
+ ignore( Visitor.visitFramacStmt o (Cil.get_stmt bhv stmt));
+ !env_ref
+
+let to_exp ~loc kf env pot label =
+ if not(Options.Full_mmodel.get ()) then
+ Error.not_yet
+ "\\at on purely logical variables but without full memory model";
+ if Options.Gmp_only.get () then
+ Error.not_yet "\\at on purely logical variables and with gmp only";
+ let term_to_exp = !term_to_exp_ref in
+ let memory_infos, env =
+ memory_infos_from_quantifs ~loc kf env (Env.get_lscope env) []
+ in
+ (* Creating the pointer *)
+ let ty = match pot with
+ | Misc.PoT_pred _ ->
+ Cil.intType
+ | Misc.PoT_term t ->
+ begin match Typing.get_integer_ty t with
+ | Typing.C_type _ | Typing.Other ->
+ Typing.get_typ t
+ | Typing.Gmp ->
+ Error.not_yet "\\at on purely logical variables and over gmp type"
+ end
+ in
+ let ty_ptr = TPtr(ty, []) in
+ let name =
+ Env.Varname.get ~scope:Env.Global "at"
+ (* the scope is actually [Function], but we use [Global] here to trick
+ [Env.Varname.get] so that it produces distinct names *)
+ in
+ let vi_at, at_e, env = Env.new_var
+ ~loc
+ ~name
+ ~scope:Env.Function
+ env
+ None
+ ty_ptr
+ (fun _ _ -> [])
+ in
+ (* Size *)
+ let lty_sizeof = Ctype Cil.(theMachine.typeOfSizeOf) in
+ let t_sizeof = Logic_const.term ~loc (TSizeOf ty) lty_sizeof in
+ let t_size = size_from_memory_infos ~loc memory_infos in
+ let t_size = Logic_const.term
+ ~loc (TBinOp(Mult, t_sizeof, t_size)) lty_sizeof
+ in
+ let i = Interval.infer t_size in
+ let malloc_stmt, env = match Typing.ty_of_interv i with
+ | Typing.C_type IInt ->
+ Typing.type_term ~use_gmp_opt:false ~ctx:Typing.c_int t_size;
+ let e_size, env = term_to_exp kf (Env.push env) t_size in
+ let e_size = Cil.constFold false e_size in
+ let malloc_stmt =
+ Misc.mk_call ~loc ~result:(Cil.var vi_at) "malloc" [e_size]
+ in
+ let malloc_block, env = Env.pop_and_get
+ env malloc_stmt ~global_clear:true Env.Before
+ in
+ (* The following assert is because:
+ 1) [t_size is] a product of CONSTANT integers due to
+ the over-approximations performed by [memory_infos_from_quantifs]
+ 2) We are in an [IInt] context
+ Thus [e_size] is simply a C integer CONSTANT *)
+ assert(List.length malloc_block.bstmts = 1);
+ malloc_stmt, env
+ | Typing.C_type _ | Typing.Gmp ->
+ Error.not_yet
+ ("\\at on purely logical variables that needs to allocate "
+ ^ "too much memory (bigger than int_max bytes)")
+ | Typing.Other ->
+ Options.fatal "quantification over non-integer type is not part of E-ACSL"
+ in
+ let mf = {
+ mf_malloc = malloc_stmt;
+ mf_free = Misc.mk_call ~loc "free" [at_e]
+ }
+ in
+ add_malloc_and_free_stmts kf mf;
+ (* Index *)
+ let t_index = index_from_mem_infos ~loc memory_infos in
+ Typing.type_term ~use_gmp_opt:false ~ctx:Typing.c_int t_index;
+ let e_index, env = term_to_exp kf env t_index in
+ let e_index = Cil.constFold false e_index in
+ (* Storing loops *)
+ let e_addr =
+ Cil.new_exp ~loc (BinOp(PlusPI, at_e, e_index, vi_at.vtype))
+ in
+ let lval_at_index = Mem e_addr, NoOffset in
+ let storing_loops, env =
+ mk_storing_loops ~loc kf env (Env.get_lscope env) lval_at_index pot
+ in
+ (* Put at label *)
+ let env = put_block_at_label env storing_loops label in
+ (* Returning *)
+ let e = Cil.new_exp ~loc (Lval lval_at_index) in
+ e, env
\ No newline at end of file
diff --git a/src/plugins/e-acsl/at_with_lscope.mli b/src/plugins/e-acsl/at_with_lscope.mli
new file mode 100644
index 00000000000..394f7688be5
--- /dev/null
+++ b/src/plugins/e-acsl/at_with_lscope.mli
@@ -0,0 +1,67 @@
+(**************************************************************************)
+(* *)
+(* This file is part of Frama-C. *)
+(* *)
+(* Copyright (C) 2007-2018 *)
+(* CEA (Commissariat à l'énergie atomique et aux énergies *)
+(* alternatives) *)
+(* *)
+(* you can redistribute it and/or modify it under the terms of the GNU *)
+(* Lesser General Public License as published by the Free Software *)
+(* Foundation, version 2.1. *)
+(* *)
+(* It is distributed in the hope that it will be useful, *)
+(* but WITHOUT ANY WARRANTY; without even the implied warranty of *)
+(* MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the *)
+(* GNU Lesser General Public License for more details. *)
+(* *)
+(* See the GNU Lesser General Public License version 2.1 *)
+(* for more details (enclosed in the file licenses/LGPLv2.1). *)
+(* *)
+(**************************************************************************)
+
+open Cil_types
+open Cil_datatype
+
+(* Convert \at on terms or predicates in which we can find purely
+ logical variable. *)
+
+(**************************************************************************)
+(********************** Forward references ********************************)
+(**************************************************************************)
+
+val predicate_to_exp_ref:
+ (kernel_function -> Env.t -> predicate -> exp * Env.t) ref
+
+val term_to_exp_ref:
+ (kernel_function -> Env.t -> term -> exp * Env.t) ref
+
+(**************************************************************************)
+(*************************** Translation **********************************)
+(**************************************************************************)
+
+val to_exp:
+ loc:Location.t -> kernel_function -> Env.t ->
+ Misc.pred_or_term -> logic_label -> exp * Env.t
+
+(*****************************************************************************)
+(**************************** Handling memory ********************************)
+(*****************************************************************************)
+
+(* The different possible evaluations of the [\at] under study are
+ stored on a memory location that needs to be alloted then freed.
+ This part is designed for that purpose. *)
+
+type malloc_and_free_stmts = {
+ mf_malloc : stmt;
+ mf_free : stmt
+}
+(* A malloc stmt and its associated free stmt. *)
+
+val add_malloc_and_free_stmts:
+ kernel_function -> malloc_and_free_stmts -> unit
+(* Add a [malloc] and [free] stmts that need to be added to [kf] *)
+
+val get_malloc_and_free_stmts: fundec -> stmt list * stmt list
+(* Get the list of [malloc] and [free] stmts that need to be added
+ to [fundec] *)
\ No newline at end of file
diff --git a/src/plugins/e-acsl/env.ml b/src/plugins/e-acsl/env.ml
index 6cbc310cb12..c9a4554b389 100644
--- a/src/plugins/e-acsl/env.ml
+++ b/src/plugins/e-acsl/env.ml
@@ -51,7 +51,8 @@ type local_env =
rte: bool }
type t =
- { visitor: Visitor.frama_c_visitor;
+ { visitor: Visitor.frama_c_visitor;
+ lscope: Lscope.t;
annotation_kind: Misc.annotation_kind;
new_global_vars: (varinfo * scope) list;
(* generated variables. The scope indicates the level where the variable
@@ -108,7 +109,8 @@ let empty_local_env =
rte = true }
let dummy =
- { visitor = new Visitor.generic_frama_c_visitor (Cil.inplace_visit ());
+ { visitor = new Visitor.generic_frama_c_visitor (Cil.inplace_visit ());
+ lscope = Lscope.empty ();
annotation_kind = Misc.Assertion;
new_global_vars = [];
global_mpz_tbl = empty_mpz_tbl;
@@ -119,7 +121,8 @@ let dummy =
cpt = 0; }
let empty v =
- { visitor = v;
+ { visitor = v;
+ lscope = Lscope.empty ();
annotation_kind = Misc.Assertion;
new_global_vars = [];
global_mpz_tbl = empty_mpz_tbl;
@@ -315,6 +318,10 @@ let current_kf env =
let get_visitor env = env.visitor
let get_behavior env = env.visitor#behavior
+let get_lscope env = env.lscope
+let add_to_lscope env lvs = { env with lscope = Lscope.add env.lscope lvs }
+let reset_lscope env = { env with lscope = Lscope.empty () }
+
let emitter =
Emitter.create
"E_ACSL"
diff --git a/src/plugins/e-acsl/env.mli b/src/plugins/e-acsl/env.mli
index bb32297e32d..3d00f03d9cc 100644
--- a/src/plugins/e-acsl/env.mli
+++ b/src/plugins/e-acsl/env.mli
@@ -116,6 +116,16 @@ val get_behavior: t -> Cil.visitor_behavior
val current_kf: t -> kernel_function option
(** Kernel function currently visited in the new project. *)
+val get_lscope: t -> Lscope.t
+(* Return the logical scope associated to the environment. *)
+
+val add_to_lscope: t -> Lscope.lscope_var -> t
+(* Add a new logical variable with its associated information in the
+ logical scope of the environment. *)
+
+val reset_lscope: t -> t
+(* Return a new environment in which the logical scope has been reset. *)
+
(* ************************************************************************** *)
(** {2 Current annotation kind} *)
(* ************************************************************************** *)
diff --git a/src/plugins/e-acsl/lscope.ml b/src/plugins/e-acsl/lscope.ml
index 24faf9400c2..9bf48d97d35 100644
--- a/src/plugins/e-acsl/lscope.ml
+++ b/src/plugins/e-acsl/lscope.ml
@@ -22,46 +22,55 @@
open Cil_types
-
type lscope_var =
- | LvsLet of logic_var * term
- | LvsQuantif of term * logic_var * term
- | LvsFormal of logic_var * logic_info
- | LvsGlobal of logic_var * term
+ | Lvs_let of logic_var * term
+ | Lvs_quantif of term * logic_var * term
+ | Lvs_formal of logic_var * logic_info
+ | Lvs_global of logic_var * term
+
+type t = lscope_var list
+(* The logic scope is usually small, so a list is fine instead of a Map *)
+
+let empty () = []
-type lscope = lscope_var list
+let is_empty = function [] -> true | _ :: _ -> false
-let add lscope lvs = lvs :: lscope
+let add t lvs = t @ [lvs]
+(* We need to append [lvs], and not prepend it.
+ This is so that the first element of the list is
+ the first that should be translated,
+ the 2nd element the 2nd to be translated and so on. *)
-let rec get_lscope_var lv lscope =
- match lscope with
+let top = function
+ | [] -> None
+ | lvs :: lscope -> Some(lvs, lscope)
+
+let rec get_lscope_var lv t =
+ match t with
| [] ->
None
- | lvs :: lscope' ->
+ | lvs :: t' ->
match lvs with
- | LvsLet(lv', _) | LvsQuantif(_, lv', _)
- | LvsFormal(lv', _) | LvsGlobal(lv', _) ->
- if lv.lv_name = lv'.lv_name then Some lvs
- else get_lscope_var lv lscope'
-
-module H_malloc_free = Hashtbl.Make(struct
- type t = fundec
- let equal (f1:fundec) f2 = Cil_datatype.Fundec.equal f1 f2
- let hash = Cil_datatype.Fundec.hash
-end)
-let tbl_malloc_free : (stmt list * stmt list) H_malloc_free.t =
- (* The first (resp.second) list is for malloc (resp. free) stmts *)
- H_malloc_free.create 7
-
-let add_malloc_and_free_stmt fundec (malloc_stmt, free_stmt) =
- try
- let malloc_stmts, free_stmts = H_malloc_free.find tbl_malloc_free fundec in
- H_malloc_free.add
- tbl_malloc_free
- fundec (malloc_stmt :: malloc_stmts, free_stmt :: free_stmts)
- with Not_found ->
- H_malloc_free.add tbl_malloc_free fundec ([malloc_stmt], [free_stmt])
+ | Lvs_let(lv', _) | Lvs_quantif(_, lv', _)
+ | Lvs_formal(lv', _) | Lvs_global(lv', _) ->
+ if Cil_datatype.Logic_var.equal lv lv' then Some lvs
+ else get_lscope_var lv t'
-let get_malloc_and_free_stmts fundec =
- try H_malloc_free.find tbl_malloc_free fundec
- with Not_found -> [], []
\ No newline at end of file
+let effective_lscope_from_pred_or_term pot potential_lscope =
+ let effective_lscope = ref (empty ()) in
+ let o = object inherit Visitor.frama_c_inplace
+ method !vlogic_var_use lv =
+ begin match get_lscope_var lv potential_lscope with
+ | None -> ()
+ | Some lvs -> effective_lscope := add !effective_lscope lvs
+ end;
+ Cil.DoChildren
+ end
+ in
+ match pot with
+ | Misc.PoT_pred p ->
+ ignore (Visitor.visitFramacPredicate o p);
+ !effective_lscope
+ | Misc.PoT_term t ->
+ ignore (Visitor.visitFramacTerm o t);
+ !effective_lscope
\ No newline at end of file
diff --git a/src/plugins/e-acsl/lscope.mli b/src/plugins/e-acsl/lscope.mli
index 3938c3b8613..0a14ecaf56d 100644
--- a/src/plugins/e-acsl/lscope.mli
+++ b/src/plugins/e-acsl/lscope.mli
@@ -22,18 +22,35 @@
open Cil_types
+(* Handle the logic scope of a term.
+ We define the logic scope of a term [t] to be the set of PURELY logical
+ variables that are visible by [t]. *)
type lscope_var =
- | LvsLet of logic_var * term
- | LvsQuantif of term * logic_var * term
- | LvsFormal of logic_var * logic_info
- | LvsGlobal of logic_var * term
+ | Lvs_let of logic_var * term (* the expression to which the lv is binded *)
+ | Lvs_quantif of term (* min *) * logic_var * term (* max *)
+ | Lvs_formal of logic_var * logic_info (* the logic definition *)
+ | Lvs_global of logic_var * term (* same as Lvs_let *)
-type lscope = lscope_var list (* TODO: maybe a Map is better *)
+type t
-val add: lscope -> lscope_var -> lscope
+val empty: unit -> t
+(* Create an empty logic scope. *)
-val get_lscope_var: logic_var -> lscope -> lscope_var option
+val is_empty: t -> bool
+(* Check whether the given logic scope is empty. *)
-val add_malloc_and_free_stmt: fundec -> stmt * stmt -> unit
-val get_malloc_and_free_stmts: fundec -> stmt list * stmt list
\ No newline at end of file
+val add: t -> lscope_var -> t
+(* Return a new logic scope in which the given [lscope_var] has been added. *)
+
+val get_lscope_var: logic_var -> t -> lscope_var option
+(* Return the [lscope_var] associated to the given logic var, if it exists. *)
+
+val top: t -> (lscope_var * t) option
+(* Return the outermost [lscope_var]. *)
+
+val effective_lscope_from_pred_or_term: Misc.pred_or_term -> t -> t
+(* We define the EFFECTIVE logical scope of a predicate or term [pot],
+ for a given POTENTIAL logical [potential_lscope] scope, to be the set [S] of
+ logical variables from [potential_lscope] that appear in [pot].
+ [effective_lscope_from_pred_or_term pot potential_lscope] computes [S]. *)
\ No newline at end of file
diff --git a/src/plugins/e-acsl/misc.ml b/src/plugins/e-acsl/misc.ml
index 1b48696679d..43f72dd3eef 100644
--- a/src/plugins/e-acsl/misc.ml
+++ b/src/plugins/e-acsl/misc.ml
@@ -290,6 +290,23 @@ let is_bitfield_pointers lty =
else
is_bitfield_pointer lty
+let term_has_lv_from_vi t =
+ let res_ref = ref false in
+ let o = object inherit Visitor.frama_c_inplace
+ method !vlogic_var_use lv =
+ match lv.lv_origin with
+ | None ->
+ Cil.DoChildren
+ | Some _ ->
+ res_ref := true;
+ Cil.SkipChildren
+ end
+ in
+ ignore (Visitor.visitFramacTerm o t);
+ !res_ref
+
+type pred_or_term = PoT_pred of predicate | PoT_term of term
+
(*
Local Variables:
compile-command: "make"
diff --git a/src/plugins/e-acsl/misc.mli b/src/plugins/e-acsl/misc.mli
index 9dbd86e33fb..87c016fdd75 100644
--- a/src/plugins/e-acsl/misc.mli
+++ b/src/plugins/e-acsl/misc.mli
@@ -114,6 +114,12 @@ val is_bitfield_pointers: logic_type -> bool
(* Returns [true] iff the given logic type is a bitfield pointer or a
set of bitfield pointers. *)
+val term_has_lv_from_vi: term -> bool
+(* Return [true] iff the given term contains a variables that originated from
+ a C varinfo, that is a non-purely logical variable. *)
+
+type pred_or_term = PoT_pred of predicate | PoT_term of term
+
(*
Local Variables:
compile-command: "make"
diff --git a/src/plugins/e-acsl/quantif.ml b/src/plugins/e-acsl/quantif.ml
index 7cd77b819f3..d30adecc770 100644
--- a/src/plugins/e-acsl/quantif.ml
+++ b/src/plugins/e-acsl/quantif.ml
@@ -23,14 +23,13 @@
open Cil_types
open Cil
open Cil_datatype
-open Lscope
let predicate_to_exp_ref
- : (kernel_function -> Env.t -> predicate -> lscope -> exp * Env.t) ref
+ : (kernel_function -> Env.t -> predicate -> exp * Env.t) ref
= Extlib.mk_fun "named_predicate_to_exp_ref"
let term_to_exp_ref
- : (kernel_function -> Env.t -> term -> lscope -> exp * Env.t) ref
+ : (kernel_function -> Env.t -> term -> exp * Env.t) ref
= Extlib.mk_fun "term_to_exp_ref"
let compute_quantif_guards quantif bounded_vars hyps =
@@ -111,7 +110,7 @@ let () = Typing.compute_quantif_guards_ref := compute_quantif_guards
module Label_ids =
State_builder.Counter(struct let name = "E_ACSL.Label_ids" end)
-let convert kf env loc is_forall p bounded_vars hyps goal lscope =
+let convert kf env loc is_forall p bounded_vars hyps goal =
(* part depending on the kind of quantifications
(either universal or existential) *)
let init_val, found_val, mk_guard =
@@ -125,11 +124,11 @@ let convert kf env loc is_forall p bounded_vars hyps goal lscope =
(* universal quantification over integers (or a subtype of integer) *)
let guards = compute_quantif_guards p bounded_vars hyps in
(* Update logic scope *)
- let lscope = lscope @ List.map
- (fun (t1, rel1, lv, rel2, t2) ->
- let tone =
- Logic_const.term ~loc (TConst(Integer(Integer.one, None))) Linteger
- in
+ let env = List.fold_left
+ (fun env (t1, rel1, lv, rel2, t2) ->
+ (* The following normalization is done here:
+ all the inequalities are large *)
+ let tone = Cil.lone ~loc () in
let t1 = match rel1 with
| Rle -> t1
| Rlt -> Logic_const.term
@@ -146,7 +145,9 @@ let convert kf env loc is_forall p bounded_vars hyps goal lscope =
Linteger
| Rgt | Rge | Req | Rneq -> assert false
in
- LvsQuantif(t1, lv, t2))
+ let lvs = Lscope.Lvs_quantif(t1, lv, t2) in
+ Env.add_to_lscope env lvs)
+ env
guards
in
let var_res, res, env =
@@ -167,7 +168,7 @@ let convert kf env loc is_forall p bounded_vars hyps goal lscope =
| [] ->
(* innermost loop body: store the result in [res] and go out according
to evaluation of the goal *)
- let test, env = named_predicate_to_exp kf (Env.push env) goal lscope in
+ let test, env = named_predicate_to_exp kf (Env.push env) goal in
let then_block = mkBlock [ mkEmptyStmt ~loc () ] in
let else_block =
(* use a 'goto', not a simple 'break' in order to handle 'forall' with
@@ -195,7 +196,7 @@ let convert kf env loc is_forall p bounded_vars hyps goal lscope =
in
let t_plus_one ?ty t =
(* whenever provided, [ty] is known to be the type of the result *)
- let tone = Logic_const.tinteger ~loc 1 in
+ let tone = Cil.lone ~loc () in
let res = Logic_const.term ~loc (TBinOp(PlusA, t, tone)) Linteger in
Extlib.may
(fun ty ->
@@ -243,7 +244,7 @@ let convert kf env loc is_forall p bounded_vars hyps goal lscope =
(* build the inner loops and loop body *)
let body, env = mk_for_loop env tl in
(* initialize the loop counter to [t1] *)
- let e1, env = term_to_exp kf (Env.push env) t1 lscope in
+ let e1, env = term_to_exp kf (Env.push env) t1 in
let init_blk, env =
Env.pop_and_get
env
@@ -260,7 +261,7 @@ let convert kf env loc is_forall p bounded_vars hyps goal lscope =
(TBinOp(bop2, tlv, { t2 with term_node = t2.term_node } )) Linteger
in
Typing.type_term ~use_gmp_opt:false ~ctx:Typing.c_int guard;
- let guard_exp, env = term_to_exp kf (Env.push env) guard lscope in
+ let guard_exp, env = term_to_exp kf (Env.push env) guard in
let break_stmt = mkStmt ~valid_sid:true (Break guard_exp.eloc) in
let guard_blk, env =
Env.pop_and_get
@@ -279,8 +280,8 @@ let convert kf env loc is_forall p bounded_vars hyps goal lscope =
(* 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 lscope in
- let next_blk, env =
+ let incr, env = term_to_exp kf (Env.push env) tlv_one in
+ let next_blk, env =
Env.pop_and_get
env
(Gmpz.affect ~loc:incr.eloc lv_x x incr)
@@ -313,14 +314,14 @@ let convert kf env loc is_forall p bounded_vars hyps goal lscope =
let env = List.fold_left Env.Logic_binding.remove env bounded_vars in
res, env
-let quantif_to_exp kf env p lscope =
+let quantif_to_exp kf env p =
let loc = p.pred_loc in
match p.pred_content with
| Pforall(bounded_vars, { pred_content = Pimplies(hyps, goal) }) ->
- convert kf env loc true p bounded_vars hyps goal lscope
+ convert kf env loc true p bounded_vars hyps goal
| Pforall _ -> Error.not_yet "unguarded \\forall quantification"
| Pexists(bounded_vars, { pred_content = Pand(hyps, goal) }) ->
- convert kf env loc false p bounded_vars hyps goal lscope
+ convert kf env loc false p bounded_vars hyps goal
| Pexists _ -> Error.not_yet "unguarded \\exists quantification"
| _ -> assert false
diff --git a/src/plugins/e-acsl/quantif.mli b/src/plugins/e-acsl/quantif.mli
index 4da71afc455..6ace647e813 100644
--- a/src/plugins/e-acsl/quantif.mli
+++ b/src/plugins/e-acsl/quantif.mli
@@ -23,11 +23,9 @@
(** Convert quantifiers. *)
open Cil_types
-open Lscope
-
val quantif_to_exp:
- kernel_function -> Env.t -> predicate -> lscope -> exp * Env.t
+ kernel_function -> Env.t -> predicate -> exp * Env.t
(** The given predicate must be a quantification. *)
(* ***********************************************************************)
@@ -35,10 +33,10 @@ val quantif_to_exp:
(* ***********************************************************************)
val predicate_to_exp_ref:
- (kernel_function -> Env.t -> predicate -> lscope -> exp * Env.t) ref
+ (kernel_function -> Env.t -> predicate -> exp * Env.t) ref
val term_to_exp_ref:
- (kernel_function -> Env.t -> term -> lscope -> exp * Env.t) ref
+ (kernel_function -> Env.t -> term -> exp * Env.t) ref
(*
Local Variables:
diff --git a/src/plugins/e-acsl/tests/full-mmodel-only/at_logic-variables.c b/src/plugins/e-acsl/tests/full-mmodel-only/at_logic-variables.c
index 74a898a4446..729f79c6413 100644
--- a/src/plugins/e-acsl/tests/full-mmodel-only/at_logic-variables.c
+++ b/src/plugins/e-acsl/tests/full-mmodel-only/at_logic-variables.c
@@ -39,11 +39,11 @@ int main(void) {
int t[5] = {9, 12, 12, 12, -4};
f(t);
- // Not yets:
+ // Not yet:
/*@ assert
\exists integer j; 2 <= j < 10000000000000000 // too big => not_yet
&& \at(n + j == 11, L); */ ;
- /*@ assert \let i = n; // TODO: lv defined with C var => not_yet
+ /*@ assert \let i = n; // lv defined with C var => not_yet
\at(n + i == 10, L); */ ;
return 0;
diff --git a/src/plugins/e-acsl/tests/full-mmodel-only/oracle/at_logic-variables.res.oracle b/src/plugins/e-acsl/tests/full-mmodel-only/oracle/at_logic-variables.res.oracle
index 8a7eda94e83..3945cc9f064 100644
--- a/src/plugins/e-acsl/tests/full-mmodel-only/oracle/at_logic-variables.res.oracle
+++ b/src/plugins/e-acsl/tests/full-mmodel-only/oracle/at_logic-variables.res.oracle
@@ -1,7 +1,7 @@
[e-acsl] beginning translation.
[e-acsl] tests/full-mmodel-only/at_logic-variables.c:45: Warning:
E-ACSL construct
- `\at with non-void logic scope that needs to allocate too much memory (bigger than int_max bytes)'
+ `\at on purely logical variables that needs to allocate too much memory (bigger than int_max bytes)'
is not yet supported.
Ignoring annotation.
[e-acsl] tests/full-mmodel-only/at_logic-variables.c:47: Warning:
diff --git a/src/plugins/e-acsl/tests/full-mmodel-only/oracle/gen_at_logic-variables.c b/src/plugins/e-acsl/tests/full-mmodel-only/oracle/gen_at_logic-variables.c
index bbf27ae2a63..13565bda997 100644
--- a/src/plugins/e-acsl/tests/full-mmodel-only/oracle/gen_at_logic-variables.c
+++ b/src/plugins/e-acsl/tests/full-mmodel-only/oracle/gen_at_logic-variables.c
@@ -14,10 +14,8 @@ void f(int *t)
/*@ ensures ∀ ℤ n; 1 < n ≤ 3 ⇒ \old(*(t + n) ≡ 12); */
void __gen_e_acsl_f(int *t)
{
- int __gen_e_acsl_size_7;
int *__gen_e_acsl_at_8;
- __gen_e_acsl_size_7 = 8;
- __gen_e_acsl_at_8 = (int *)malloc((size_t)__gen_e_acsl_size_7);
+ __gen_e_acsl_at_8 = (int *)malloc((size_t)8);
{
int __gen_e_acsl_n;
__gen_e_acsl_n = 1 + 1;
@@ -92,35 +90,22 @@ void __e_acsl_globals_init(void)
int main(void)
{
- int *__gen_e_acsl_at_7;
- int __gen_e_acsl_size_6;
int *__gen_e_acsl_at_6;
- int __gen_e_acsl_size_5;
long *__gen_e_acsl_at_5;
- int __gen_e_acsl_size_4;
long *__gen_e_acsl_at_4;
- int __gen_e_acsl_size_3;
int *__gen_e_acsl_at_3;
- int __gen_e_acsl_size_2;
int *__gen_e_acsl_at_2;
- int __gen_e_acsl_size;
int *__gen_e_acsl_at;
int __retres;
int n;
__e_acsl_memory_init((int *)0,(char ***)0,(size_t)8);
__e_acsl_globals_init();
- __gen_e_acsl_size_6 = 1536;
- __gen_e_acsl_at_6 = (int *)malloc((size_t)__gen_e_acsl_size_6);
- __gen_e_acsl_size_5 = 64;
- __gen_e_acsl_at_5 = (long *)malloc((size_t)__gen_e_acsl_size_5);
- __gen_e_acsl_size_4 = 8;
- __gen_e_acsl_at_4 = (long *)malloc((size_t)__gen_e_acsl_size_4);
- __gen_e_acsl_size_3 = 528;
- __gen_e_acsl_at_3 = (int *)malloc((size_t)__gen_e_acsl_size_3);
- __gen_e_acsl_size_2 = 12;
- __gen_e_acsl_at_2 = (int *)malloc((size_t)__gen_e_acsl_size_2);
- __gen_e_acsl_size = 4;
- __gen_e_acsl_at = (int *)malloc((size_t)__gen_e_acsl_size);
+ __gen_e_acsl_at_6 = (int *)malloc((size_t)1536);
+ __gen_e_acsl_at_5 = (long *)malloc((size_t)64);
+ __gen_e_acsl_at_4 = (long *)malloc((size_t)8);
+ __gen_e_acsl_at_3 = (int *)malloc((size_t)528);
+ __gen_e_acsl_at_2 = (int *)malloc((size_t)12);
+ __gen_e_acsl_at = (int *)malloc((size_t)4);
__e_acsl_store_block((void *)(& n),(size_t)4);
__e_acsl_store_block((void *)(& __retres),(size_t)4);
__e_acsl_full_init((void *)(& n));
@@ -180,9 +165,9 @@ int main(void)
}
{
int __gen_e_acsl_k;
- __gen_e_acsl_k = -7;
{
int __gen_e_acsl_u;
+ __gen_e_acsl_k = -7;
__gen_e_acsl_u = 9;
while (1)
if (__gen_e_acsl_u <= 20) {
@@ -453,12 +438,12 @@ int main(void)
/*@ assert \let i = n; \at(n + i ≡ 10,L); */ ;
__e_acsl_full_init((void *)(& __retres));
__retres = 0;
- free((void *)__gen_e_acsl_at_6);
- free((void *)__gen_e_acsl_at_5);
- free((void *)__gen_e_acsl_at_4);
- free((void *)__gen_e_acsl_at_3);
- free((void *)__gen_e_acsl_at_2);
free((void *)__gen_e_acsl_at);
+ free((void *)__gen_e_acsl_at_2);
+ free((void *)__gen_e_acsl_at_3);
+ free((void *)__gen_e_acsl_at_4);
+ free((void *)__gen_e_acsl_at_5);
+ free((void *)__gen_e_acsl_at_6);
__e_acsl_delete_block((void *)(& f));
__e_acsl_delete_block((void *)(& __fc_p_fopen));
__e_acsl_delete_block((void *)(__fc_fopen));
diff --git a/src/plugins/e-acsl/translate.ml b/src/plugins/e-acsl/translate.ml
index 22ef2433c21..0a4d239c911 100644
--- a/src/plugins/e-acsl/translate.ml
+++ b/src/plugins/e-acsl/translate.ml
@@ -23,7 +23,6 @@
module E_acsl_label = Label
open Cil_types
open Cil_datatype
-open Lscope
let dkey = Options.dkey_translation
@@ -112,35 +111,6 @@ let rec eliminate_ranges_from_index_of_toffset ~loc toffset quantifiers =
| TField _ ->
Error.not_yet "range elimination on TField"
-(* ************************************************************************ *)
-(* Managing \at with non-void logic scope *)
-(* ************************************************************************ *)
-
-type pred_or_term = PoTPred of predicate | PoTTerm of term
-
-let effective_lscope_from_pred_or_term pot potential_lscope =
- let o = object(self) inherit Visitor.frama_c_inplace
- val mutable effective_lscope = ([] : lscope)
- method !vlogic_var_use lv =
- begin match Lscope.get_lscope_var lv potential_lscope with
- | None -> ()
- | Some lvs -> effective_lscope <- lvs :: effective_lscope
- end;
- Cil.DoChildren
- method visit pot =
- match pot with
- | PoTPred p ->
- ignore
- (Visitor.visitFramacPredicate (self :> Visitor.frama_c_inplace) p);
- effective_lscope
- | PoTTerm t ->
- ignore
- (Visitor.visitFramacTerm (self :> Visitor.frama_c_inplace) t);
- effective_lscope
- end
- in
- o#visit pot
-
(* ************************************************************************** *)
(* Transforming terms and predicates into C expressions (if any) *)
(* ************************************************************************** *)
@@ -326,7 +296,7 @@ let cast_integer_to_float lty lty_t e =
else
e
-let rec thost_to_host kf env th lscope = match th with
+let rec thost_to_host kf env th = match th with
| TVar { lv_origin = Some v } ->
Var (Cil.get_varinfo (Env.get_behavior env) v), env, v.vname
| TVar ({ lv_origin = None } as logic_v) ->
@@ -339,50 +309,50 @@ let rec thost_to_host kf env th lscope = match th with
| Var v -> Var (Cil.get_varinfo (Env.get_behavior env) v), env, "result"
| _ -> assert false)
| TMem t ->
- let e, env = term_to_exp kf env t lscope in
+ let e, env = term_to_exp kf env t in
Mem e, env, ""
-and toffset_to_offset ?loc kf env toff lscope = match toff with
+and toffset_to_offset ?loc kf env toff = match toff with
| TNoOffset -> NoOffset, env
| TField(f, offset) ->
- let offset, env = toffset_to_offset ?loc kf env offset lscope in
+ let offset, env = toffset_to_offset ?loc kf env offset in
Field(f, offset), env
| TIndex(t, offset) ->
- let e, env = term_to_exp kf env t lscope in
- let offset, env = toffset_to_offset kf env offset lscope in
+ let e, env = term_to_exp kf env t in
+ let offset, env = toffset_to_offset kf env offset in
Index(e, offset), env
| TModel _ -> not_yet env "model"
-and tlval_to_lval kf env (host, offset) lscope =
- let host, env, name = thost_to_host kf env host lscope in
- let offset, env = toffset_to_offset kf env offset lscope in
+and tlval_to_lval kf env (host, offset) =
+ let host, env, name = thost_to_host kf env host in
+ let offset, env = toffset_to_offset kf env offset in
let name = match offset with NoOffset -> name | Field _ | Index _ -> "" in
(host, offset), env, name
(* the returned boolean says that the expression is an mpz_string;
the returned string is the name of the generated variable corresponding to
the term. *)
-and context_insensitive_term_to_exp kf env t (lscope: lscope) =
+and context_insensitive_term_to_exp kf env t =
let loc = t.term_loc in
match t.term_node with
| TConst c ->
let c, is_mpz_string = constant_to_exp ~loc t c in
c, env, is_mpz_string, ""
| TLval lv ->
- let lv, env, name = tlval_to_lval kf env lv lscope in
+ let lv, env, name = tlval_to_lval kf env lv in
Cil.new_exp ~loc (Lval lv), env, false, name
| TSizeOf ty -> Cil.sizeOf ~loc ty, env, false, "sizeof"
| TSizeOfE t ->
- let e, env = term_to_exp kf env t lscope in
+ let e, env = term_to_exp kf env t in
Cil.sizeOf ~loc (Cil.typeOf e), env, false, "sizeof"
| TSizeOfStr s -> Cil.new_exp ~loc (SizeOfStr s), env, false, "sizeofstr"
| TAlignOf ty -> Cil.new_exp ~loc (AlignOf ty), env, false, "alignof"
| TAlignOfE t ->
- let e, env = term_to_exp kf env t lscope in
+ let e, env = term_to_exp kf env t in
Cil.new_exp ~loc (AlignOfE e), env, false, "alignof"
| TUnOp(Neg | BNot as op, t') ->
let ty = Typing.get_typ t in
- let e, env = term_to_exp kf env t' lscope in
+ let e, env = term_to_exp kf env t' in
if Gmpz.is_t ty then
let name, vname = match op with
| Neg -> "__gmpz_neg", "neg"
@@ -409,18 +379,18 @@ and context_insensitive_term_to_exp kf env t (lscope: lscope) =
Typing.type_term ~use_gmp_opt:true ~ctx zero;
let e, env =
comparison_to_exp
- kf ~loc ~name:"not" env Typing.gmp Eq t zero (Some t) lscope
+ kf ~loc ~name:"not" env Typing.gmp Eq t zero (Some t)
in
e, env, false, ""
else begin
assert (Cil.isIntegralType ty);
- let e, env = term_to_exp kf env t lscope in
+ let e, env = term_to_exp kf env t in
Cil.new_exp ~loc (UnOp(LNot, e, Cil.intType)), env, false, ""
end
| TBinOp(PlusA | MinusA | Mult as bop, t1, t2) ->
let ty = Typing.get_typ t in
- let e1, env = term_to_exp kf env t1 lscope in
- let e2, env = term_to_exp kf env t2 lscope in
+ let e1, env = term_to_exp kf env t1 in
+ let e2, env = term_to_exp kf env t2 in
if Gmpz.is_t ty then
let name = name_of_mpz_arith_bop bop in
let mk_stmts _ e = [ Misc.mk_call ~loc name [ e; e1; e2 ] ] in
@@ -439,8 +409,8 @@ and context_insensitive_term_to_exp kf env t (lscope: lscope) =
Cil.new_exp ~loc (BinOp(bop, e1, e2, ty)), env, false, ""
| TBinOp(Div | Mod as bop, t1, t2) ->
let ty = Typing.get_typ t in
- let e1, env = term_to_exp kf env t1 lscope in
- let e2, env = term_to_exp kf env t2 lscope in
+ let e1, env = term_to_exp kf env t1 in
+ let e2, env = term_to_exp kf env t2 in
if Gmpz.is_t ty then
(* TODO: preventing division by zero should not be required anymore.
RTE should do this automatically. *)
@@ -456,7 +426,7 @@ and context_insensitive_term_to_exp kf env t (lscope: lscope) =
let guard, env =
let name = name_of_binop bop ^ "_guard" in
comparison_to_exp
- ~loc kf env Typing.gmp ~e1:e2 ~name Eq t2 zero t lscope
+ ~loc kf env Typing.gmp ~e1:e2 ~name Eq t2 zero t
in
let mk_stmts _v e =
assert (Gmpz.is_t ty);
@@ -488,16 +458,16 @@ and context_insensitive_term_to_exp kf env t (lscope: lscope) =
| TBinOp(Lt | Gt | Le | Ge | Eq | Ne as bop, t1, t2) ->
(* comparison operators *)
let ity = Typing.get_integer_op t in
- let e, env = comparison_to_exp ~loc kf env ity bop t1 t2 (Some t) lscope in
+ let e, env = comparison_to_exp ~loc kf env ity bop t1 t2 (Some t) in
e, env, false, ""
| TBinOp((Shiftlt | Shiftrt), _, _) ->
(* left/right shift *)
not_yet env "left/right shift"
| TBinOp(LOr, t1, t2) ->
(* t1 || t2 <==> if t1 then true else t2 *)
- let e1, env1 = term_to_exp kf (Env.rte env true) t1 lscope in
+ let e1, env1 = term_to_exp kf (Env.rte env true) t1 in
let env' = Env.push env1 in
- let res2 = term_to_exp kf (Env.push env') t2 lscope in
+ let res2 = term_to_exp kf (Env.push env') t2 in
let e, env =
conditional_to_exp
~name:"or" loc (Some t) e1 (Cil.one loc, env') res2
@@ -505,8 +475,8 @@ and context_insensitive_term_to_exp kf env t (lscope: lscope) =
e, env, false, ""
| TBinOp(LAnd, t1, t2) ->
(* t1 && t2 <==> if t1 then t2 else false *)
- let e1, env1 = term_to_exp kf (Env.rte env true) t1 lscope in
- let _, env2 as res2 = term_to_exp kf (Env.push env1) t2 lscope in
+ let e1, env1 = term_to_exp kf (Env.rte env true) t1 in
+ let _, env2 as res2 = term_to_exp kf (Env.push env1) t2 in
let env3 = Env.push env2 in
let e, env =
conditional_to_exp ~name:"and" loc (Some t) e1 res2 (Cil.zero loc, env3)
@@ -526,19 +496,19 @@ and context_insensitive_term_to_exp kf env t (lscope: lscope) =
| Ctype ty -> ty
| _ -> assert false
in
- let e1, env = term_to_exp kf env t1 lscope in
- let e2, env = term_to_exp kf env t2 lscope in
+ let e1, env = term_to_exp kf env t1 in
+ let e2, env = term_to_exp kf env t2 in
Cil.new_exp ~loc (BinOp(bop, e1, e2, ty)), env, false, ""
| TCastE(ty, t') ->
- let e, env = term_to_exp kf env t' lscope in
+ let e, env = term_to_exp kf env t' in
let e, env = add_cast ~loc ~name:"cast" env (Some ty) false (Some t) e in
e, env, false, ""
| TLogic_coerce _ -> assert false (* handle in [term_to_exp] *)
| TAddrOf lv ->
- let lv, env, _ = tlval_to_lval kf env lv lscope in
+ let lv, env, _ = tlval_to_lval kf env lv in
Cil.mkAddrOf ~loc lv, env, false, "addrof"
| TStartOf lv ->
- let lv, env, _ = tlval_to_lval kf env lv lscope in
+ let lv, env, _ = tlval_to_lval kf env lv in
Cil.mkAddrOrStartOf ~loc lv, env, false, "startof"
| Tapp(li, [], args) when Builtins.mem li.l_var_info.lv_name ->
(* E-ACSL built-in function call *)
@@ -547,7 +517,7 @@ and context_insensitive_term_to_exp kf env t (lscope: lscope) =
try
List.fold_left
(fun (l, env) a ->
- let e, env = term_to_exp kf env a lscope in
+ let e, env = term_to_exp kf env a in
e :: l, env)
([], env)
args
@@ -573,38 +543,38 @@ and context_insensitive_term_to_exp kf env t (lscope: lscope) =
| Tlambda _ -> not_yet env "functional"
| TDataCons _ -> not_yet env "constructor"
| Tif(t1, t2, t3) ->
- let e1, env1 = term_to_exp kf (Env.rte env true) t1 lscope in
- let (_, env2 as res2) = term_to_exp kf (Env.push env1) t2 lscope in
- let res3 = term_to_exp kf (Env.push env2) t3 lscope in
+ let e1, env1 = term_to_exp kf (Env.rte env true) t1 in
+ let (_, env2 as res2) = term_to_exp kf (Env.push env1) t2 in
+ let res3 = term_to_exp kf (Env.push env2) t3 in
let e, env = conditional_to_exp loc (Some t) e1 res2 res3 in
e, env, false, ""
| Tat(t, BuiltinLabel Here) ->
- let e, env = term_to_exp kf env t lscope in
+ let e, env = term_to_exp kf env t in
e, env, false, ""
| Tat(t', label) ->
- let effective_lscope =
- effective_lscope_from_pred_or_term (PoTTerm t') lscope
+ let potential_lscope = Env.get_lscope env in
+ let effective_lscope = Lscope.effective_lscope_from_pred_or_term
+ (Misc.PoT_term t') potential_lscope
in
- begin match effective_lscope with
- | [] ->
- let e, env = term_to_exp kf (Env.push env) t' lscope in
- let e, env, is_mpz_string = at_to_exp_no_lscope env (Some t) label e in
- e, env, is_mpz_string, ""
- | _ :: _ ->
- let pot = PoTTerm t' in
- let e, env = at_to_exp_with_lscope ~loc env kf pot lscope label in
- e, env, false, "" (* TODO: GMP not supported yet *)
+ if Lscope.is_empty effective_lscope then begin
+ let e, env = term_to_exp kf (Env.push env) t' in
+ let e, env, is_mpz_string = at_to_exp_no_lscope env (Some t) label e in
+ e, env, is_mpz_string, ""
+ end else begin
+ let pot = Misc.PoT_term t' in
+ let e, env = At_with_lscope.to_exp ~loc kf env pot label in
+ e, env, false, ""
end
| Tbase_addr(BuiltinLabel Here, t) ->
- mmodel_call ~loc kf "base_addr" Cil.voidPtrType env t lscope
+ mmodel_call ~loc kf "base_addr" Cil.voidPtrType env t
| Tbase_addr _ -> not_yet env "labeled \\base_addr"
| Toffset(BuiltinLabel Here, t) ->
let size_t = Cil.theMachine.Cil.typeOfSizeOf in
- mmodel_call ~loc kf "offset" size_t env t lscope
+ mmodel_call ~loc kf "offset" size_t env t
| Toffset _ -> not_yet env "labeled \\offset"
| Tblock_length(BuiltinLabel Here, t) ->
let size_t = Cil.theMachine.Cil.typeOfSizeOf in
- mmodel_call ~loc kf "block_length" size_t env t lscope
+ mmodel_call ~loc kf "block_length" size_t env t
| Tblock_length _ -> not_yet env "labeled \\block_length"
| Tnull -> Cil.mkCast (Cil.zero ~loc) (TPtr(TVoid [], [])), env, false, "null"
| TCoerce _ -> Error.untypable "coercion" (* Jessie specific *)
@@ -618,24 +588,24 @@ and context_insensitive_term_to_exp kf env t (lscope: lscope) =
| Tcomprehension _ -> not_yet env "tset comprehension"
| Trange _ -> not_yet env "range"
| Tlet(li, t) ->
- let lvs = LvsLet(li.l_var_info, Misc.term_of_li li) in
- let lscope = Lscope.add lscope lvs in
- let env = env_of_li li kf env loc lscope in
- let e, env = term_to_exp kf env t lscope in
+ let lvs = Lscope.Lvs_let(li.l_var_info, Misc.term_of_li li) in
+ let env = Env.add_to_lscope env lvs in
+ let env = env_of_li li kf env loc in
+ let e, env = term_to_exp kf env t in
Interval.Env.remove li.l_var_info;
e, env, false, ""
(* Convert an ACSL term into a corresponding C expression (if any) in the given
environment. Also extend this environment in order to include the generating
constructs. *)
-and term_to_exp kf env t lscope =
+and term_to_exp kf env t =
let generate_rte = Env.generate_rte env in
Options.feedback ~dkey ~level:4 "translating term %a (rte? %b)"
Printer.pp_term t generate_rte;
let env = Env.rte env false in
let t = match t.term_node with TLogic_coerce(_, t) -> t | _ -> t in
let e, env, is_mpz_string, name =
- context_insensitive_term_to_exp kf env t lscope
+ context_insensitive_term_to_exp kf env t
in
let env = if generate_rte then translate_rte kf env e else env in
let cast = Typing.get_cast t in
@@ -651,15 +621,15 @@ and term_to_exp kf env t lscope =
(* generate the C code equivalent to [t1 bop t2]. *)
and comparison_to_exp
- ~loc ?e1 kf env ity bop ?(name=name_of_binop bop) t1 t2 t_opt lscope =
+ ~loc ?e1 kf env ity bop ?(name=name_of_binop bop) t1 t2 t_opt =
let e1, env = match e1 with
| None ->
- let e1, env = term_to_exp kf env t1 lscope in
+ let e1, env = term_to_exp kf env t1 in
e1, env
| Some e1 ->
e1, env
in
- let e2, env = term_to_exp kf env t2 lscope in
+ let e2, env = term_to_exp kf env t2 in
match ity with
| Typing.Gmp ->
let _, e, env =
@@ -677,8 +647,8 @@ and comparison_to_exp
Cil.mkBinOp ~loc bop e1 e2, env
(* \base_addr, \block_length and \freeable annotations *)
-and mmodel_call ~loc kf name ctx env t lscope =
- let e, env = term_to_exp kf (Env.rte env true) t lscope in
+and mmodel_call ~loc kf name ctx env t =
+ let e, env = term_to_exp kf (Env.rte env true) t in
let _, res, env =
Env.new_var
~loc
@@ -963,31 +933,11 @@ and at_to_exp_no_lscope env t_opt label e =
ignore( Visitor.visitFramacStmt o (Cil.get_stmt bhv stmt));
res, !env_ref, false
-and put_block_at_label env block label =
- let stmt = E_acsl_label.get_stmt (Env.get_visitor env) label in
- let env_ref = ref env in
- let o = object
- inherit Visitor.frama_c_inplace
- method !vstmt_aux stmt =
- assert (!env_ref == env);
- let pre = match label with
- | BuiltinLabel(Here | Post) -> true
- | BuiltinLabel(Old | Pre | LoopEntry | LoopCurrent | Init)
- | FormalLabel _ | StmtLabel _ -> false
- in
- env_ref := Env.extend_stmt_in_place env stmt ~pre block;
- Cil.ChangeTo stmt
- end
- in
- let bhv = Env.get_behavior env in
- ignore( Visitor.visitFramacStmt o (Cil.get_stmt bhv stmt));
- !env_ref
-
-and env_of_li li kf env loc lscope =
+and env_of_li li kf env loc =
let li_t = Misc.term_of_li li in
let ty = Typing.get_typ li_t in
let vi, vi_e, env = Env.Logic_binding.add ~ty env li.l_var_info in
- let li_e, env = term_to_exp kf env li_t lscope in
+ let li_e, env = term_to_exp kf env li_t in
let stmt = match Typing.get_integer_ty li_t with
| Typing.C_type _ | Typing.Other ->
Cil.mkStmtOneInstr (Set (Cil.var vi, li_e, loc))
@@ -999,7 +949,7 @@ and env_of_li li kf env loc lscope =
(* Convert an ACSL named predicate into a corresponding C expression (if
any) in the given environment. Also extend this environment which includes
the generating constructs. *)
-and named_predicate_content_to_exp ?name kf env p lscope =
+and named_predicate_content_to_exp ?name kf env p =
let loc = p.pred_loc in
match p.pred_content with
| Pfalse -> Cil.zero ~loc, env
@@ -1010,20 +960,20 @@ and named_predicate_content_to_exp ?name kf env p lscope =
| Pvalid_function _ -> not_yet env "\\valid_function"
| Prel(rel, t1, t2) ->
let ity = Typing.get_integer_op_of_predicate p in
- comparison_to_exp ~loc kf env ity (relation_to_binop rel) t1 t2 None lscope
+ comparison_to_exp ~loc kf env ity (relation_to_binop rel) t1 t2 None
| Pand(p1, p2) ->
(* p1 && p2 <==> if p1 then p2 else false *)
- let e1, env1 = named_predicate_to_exp kf (Env.rte env true) p1 lscope in
+ let e1, env1 = named_predicate_to_exp kf (Env.rte env true) p1 in
let _, env2 as res2 =
- named_predicate_to_exp kf (Env.push env1) p2 lscope in
+ named_predicate_to_exp kf (Env.push env1) p2 in
let env3 = Env.push env2 in
let name = match name with None -> "and" | Some n -> n in
conditional_to_exp ~name loc None e1 res2 (Cil.zero loc, env3)
| Por(p1, p2) ->
(* p1 || p2 <==> if p1 then true else p2 *)
- let e1, env1 = named_predicate_to_exp kf (Env.rte env true) p1 lscope in
+ let e1, env1 = named_predicate_to_exp kf (Env.rte env true) p1 in
let env' = Env.push env1 in
- let res2 = named_predicate_to_exp kf (Env.push env') p2 lscope in
+ let res2 = named_predicate_to_exp kf (Env.push env') p2 in
let name = match name with None -> "or" | Some n -> n in
conditional_to_exp ~name loc None e1 (Cil.one loc, env') res2
| Pxor _ -> not_yet env "xor"
@@ -1034,7 +984,6 @@ and named_predicate_content_to_exp ?name kf env p lscope =
kf
env
(Logic_const.por ~loc ((Logic_const.pnot ~loc p1), p2))
- lscope
| Piff(p1, p2) ->
(* (p1 <==> p2) <==> (p1 ==> p2 && p2 ==> p1) *)
named_predicate_to_exp
@@ -1044,40 +993,39 @@ and named_predicate_content_to_exp ?name kf env p lscope =
(Logic_const.pand ~loc
(Logic_const.pimplies ~loc (p1, p2),
Logic_const.pimplies ~loc (p2, p1)))
- lscope
| Pnot p ->
- let e, env = named_predicate_to_exp kf env p lscope in
+ let e, env = named_predicate_to_exp kf env p in
Cil.new_exp ~loc (UnOp(LNot, e, Cil.intType)), env
| Pif(t, p2, p3) ->
- let e1, env1 = term_to_exp kf (Env.rte env true) t lscope in
+ let e1, env1 = term_to_exp kf (Env.rte env true) t in
let (_, env2 as res2) =
- named_predicate_to_exp kf (Env.push env1) p2 lscope in
- let res3 = named_predicate_to_exp kf (Env.push env2) p3 lscope in
+ named_predicate_to_exp kf (Env.push env1) p2 in
+ let res3 = named_predicate_to_exp kf (Env.push env2) p3 in
conditional_to_exp loc None e1 res2 res3
| Plet(li, p) ->
- let lvs = LvsLet(li.l_var_info, Misc.term_of_li li) in
- let lscope = Lscope.add lscope lvs in
- let env = env_of_li li kf env loc lscope in
- let e, env = named_predicate_to_exp kf env p lscope in
+ let lvs = Lscope.Lvs_let(li.l_var_info, Misc.term_of_li li) in
+ let env = Env.add_to_lscope env lvs in
+ let env = env_of_li li kf env loc in
+ let e, env = named_predicate_to_exp kf env p in
Interval.Env.remove li.l_var_info;
e, env
- | Pforall _ | Pexists _ -> Quantif.quantif_to_exp kf env p lscope
+ | Pforall _ | Pexists _ -> Quantif.quantif_to_exp kf env p
| Pat(p, BuiltinLabel Here) ->
- named_predicate_to_exp kf env p lscope
+ named_predicate_to_exp kf env p
| Pat(p', label) ->
- let effective_lscope =
- effective_lscope_from_pred_or_term (PoTPred p') lscope
+ let potential_lscope = Env.get_lscope env in
+ let effective_lscope = Lscope.effective_lscope_from_pred_or_term
+ (Misc.PoT_pred p') potential_lscope
in
- begin match effective_lscope with
- | [] ->
- (* convert [t'] to [e] in a separated local env *)
- let e, env = named_predicate_to_exp kf (Env.push env) p' lscope in
- let e, env, is_string = at_to_exp_no_lscope env None label e in
- assert (not is_string);
- e, env
- | _ :: _ ->
- let pot = PoTPred p' in
- let e, env = at_to_exp_with_lscope ~loc env kf pot lscope label in
+ if Lscope.is_empty effective_lscope then begin
+ (* convert [t'] to [e] in a separated local env *)
+ let e, env = named_predicate_to_exp kf (Env.push env) p' in
+ let e, env, is_string = at_to_exp_no_lscope env None label e in
+ assert (not is_string);
+ e, env
+ end else begin
+ let pot = Misc.PoT_pred p' in
+ let e, env = At_with_lscope.to_exp ~loc kf env pot label in
e, env
end
| Pvalid_read(BuiltinLabel Here as llabel, t) as pc
@@ -1094,7 +1042,7 @@ and named_predicate_content_to_exp ?name kf env p lscope =
(* we already transformed \valid(t) into \initialized(&t) && \valid(t):
now convert this right-most valid. *)
is_visiting_valid := false;
- call_valid t lscope
+ call_valid t
end else begin
match t.term_node, t.term_type with
| TLval tlv, Ctype ty ->
@@ -1104,8 +1052,8 @@ and named_predicate_content_to_exp ?name kf env p lscope =
Typing.type_named_predicate ~must_clear:false init;
let p = Logic_const.pand ~loc (init, p) in
is_visiting_valid := true;
- named_predicate_to_exp kf env p lscope
- | _ -> call_valid t lscope
+ named_predicate_to_exp kf env p
+ | _ -> call_valid t
end
| Pvalid _ -> not_yet env "labeled \\valid"
| Pvalid_read _ -> not_yet env "labeled \\valid_read"
@@ -1117,350 +1065,22 @@ and named_predicate_content_to_exp ?name kf env p lscope =
when vi.vformal || vi.vglob || Functions.RTL.is_generated_name vi.vname ->
Cil.one ~loc, env
| _ ->
- mmodel_call_with_size ~loc kf "initialized" Cil.intType env t lscope)
+ mmodel_call_with_size ~loc kf "initialized" Cil.intType env t)
| Pinitialized _ -> not_yet env "labeled \\initialized"
| Pallocable _ -> not_yet env "\\allocate"
| Pfreeable(BuiltinLabel Here, t) ->
let res, env, _, _ =
- mmodel_call ~loc kf "freeable" Cil.intType env t lscope
+ mmodel_call ~loc kf "freeable" Cil.intType env t
in
res, env
| Pfreeable _ -> not_yet env "labeled \\freeable"
| Pfresh _ -> not_yet env "\\fresh"
| Psubtype _ -> Error.untypable "subtyping relation" (* Jessie specific *)
-and at_to_exp_with_lscope ~loc env kf pot lscope label =
- (* TODO: move this function and everything related to it in a new file
- so that Translate does not become to long *)
- if not(Options.Full_mmodel.get ()) then
- not_yet env "\\at with non-void logic scope but without full memory model";
- if Options.Gmp_only.get () then
- not_yet env "\\at with non-void logic scope and with gmp only";
- let mem_infos, env =
- mem_infos_from_quantifs ~loc kf lscope [] env
- in
- (* Creating the pointer *)
- let ty = match pot with
- | PoTPred _ ->
- Cil.intType
- | PoTTerm t ->
- begin match Typing.get_integer_ty t with
- | Typing.C_type _ | Typing.Other ->
- Typing.get_typ t
- | Typing.Gmp ->
- not_yet env "\\at with non-void logic scope and over gmp type"
- end
- in
- let ty_array = TPtr(ty, []) in
- let name = Env.Varname.get ~scope:Env.Global "at" in
- let vi_at, at_e, env = Env.new_var
- ~loc
- ~name
- ~scope:Env.Function
- env
- None
- ty_array
- (fun _ _ -> [])
- in
- (* Size *)
- let t_sizeof = Logic_const.term ~loc (TSizeOf ty) (Ctype Cil.intType) in
- let t_size = size_from_mem_infos ~loc mem_infos in
- let t_size = Logic_const.term
- ~loc (TBinOp(Mult, t_sizeof, t_size)) Linteger
- in
- let i = Interval.infer t_size in
- begin match Typing.ty_of_interv i with
- | Typing.C_type IInt ->
- Typing.type_term ~use_gmp_opt:false ~ctx:Typing.c_int t_size;
- | Typing.C_type _ | Typing.Gmp ->
- not_yet
- env
- ("\\at with non-void logic scope that needs to allocate too much memory "
- ^ "(bigger than int_max bytes)")
- | Typing.Other ->
- Options.fatal "quantification over non-integer type is not part of E-ACSL"
- end;
- let e_size, env = term_to_exp kf (Env.push env) t_size lscope in
- let e_size = Cil.constFold false e_size in
- let name = Env.Varname.get ~scope:Env.Global "size" in
- let _, e_size, env = Env.new_var
- ~loc
- ~name
- ~scope:Env.Function
- env
- None
- Cil.intType
- (fun vi _ ->
- let instr = Set(Cil.var vi, e_size, loc) in
- let stmt = Cil.mkStmtOneInstr instr in
- [stmt])
- in
- let block_size, env = Env.pop_and_get
- env (Cil.mkEmptyStmt ~loc ()) ~global_clear:true Env.After
- in
- let malloc_block = Cil.mkBlock [
- Cil.mkStmt ~valid_sid:true (Block block_size);
- Misc.mk_call ~loc ~result:(Cil.var vi_at) "malloc" [e_size]
- ]
- in
- let malloc_stmt = Cil.mkStmt ~valid_sid:true (Block malloc_block) in
- let free_stmt = Misc.mk_call ~loc "free" [at_e] in
- begin match kf.fundec with
- | Definition(fundec, _) ->
- Lscope.add_malloc_and_free_stmt fundec (malloc_stmt, free_stmt)
- | Declaration _ ->
- assert false
- end;
- (* Index *)
- let t_index = index_from_mem_infos ~loc mem_infos in
- Typing.type_term ~use_gmp_opt:false ~ctx:Typing.c_int t_index;
- let e_index, env = term_to_exp kf env t_index lscope in
- let e_index = Cil.constFold false e_index in
- (* Storing loops *)
- let e_addr =
- Cil.new_exp ~loc (BinOp(PlusPI, at_e, e_index, vi_at.vtype))
- in
- let lval_at_index = Mem e_addr, NoOffset in
- let storing_loops, env =
- mk_storing_loops ~loc kf env lscope lval_at_index pot
- in
- (* Put at label *)
- let block =
- Cil.mkBlock [ Cil.mkStmt ~valid_sid:true (Block storing_loops) ]
- in
- let env = put_block_at_label env block label in
- (* Returning *)
- let e = Cil.new_exp ~loc (Lval lval_at_index) in
- e, env
-
-and mem_infos_from_quantifs ~loc kf lscope res env =
- (* To LvsQuantif(tmin, lv, tmax) correponds (t_size, t_shifted)
- where t_size = tmax - tmin + 1 (+1 because the inequalities are large
- due to previous normalization)
- and t_shifted = lv - tmin (so that we start indexing at 0) *)
- match lscope with
- | [] ->
- res, env
- | lscope_var :: lscope' ->
- match lscope_var with
- | LvsQuantif(tmin, _, tmax)
- when (term_has_lv_from_vi tmin) || (term_has_lv_from_vi tmax) ->
- not_yet env "\\at with logic variable linked to C variable"
- | LvsQuantif(tmin, lv, tmax) ->
- let t_size = Logic_const.term
- ~loc (TBinOp(MinusA, tmax, tmin)) Linteger
- in
- let t_size = Logic_const.term
- ~loc (TBinOp(PlusA, t_size, Logic_const.tinteger ~loc 1)) Linteger
- in
- let i = Interval.infer t_size in
- let t_size = match Ival.min_and_max i with
- | Some _, Some max ->
- (* We need to get an over-approx of the amount of memory needed.
- We may not write to/read from all of if *)
- Logic_const.tint ~loc max
- | _ ->
- not_yet
- env
- ("\\at with non-void logic scope and with quantifier that uses too "
- ^ "complex bound (e-acsl cannot infer a finite upper bound to it)")
- in
- (* Index *)
- let t_lv = Logic_const.tvar ~loc lv in
- let t_shifted = Logic_const.term
- ~loc (TBinOp(MinusA, t_lv, tmin)) Linteger
- in
- (* Returning *)
- let res = (t_size, t_shifted) :: res in
- mem_infos_from_quantifs ~loc kf lscope' res env
- | LvsLet(_, t) | LvsGlobal(_, t) when (term_has_lv_from_vi t) ->
- not_yet env "\\at with logic variable linked to C variable"
- | LvsLet _ ->
- mem_infos_from_quantifs ~loc kf lscope' res env
- | LvsFormal _ ->
- not_yet env "\\at using formal variable of a logic function"
- | LvsGlobal _ ->
- not_yet env "\\at using global logic variable"
-
-and size_from_mem_infos ~loc mem_infos =
- List.fold_left
- (fun t_size (t_s, _) ->
- Logic_const.term ~loc (TBinOp(Mult, t_size, t_s)) Linteger)
- ( Logic_const.tinteger ~loc 1)
- mem_infos
-
-and index_from_mem_infos ~loc mem_infos =
- (* We want to associate to each possible tuple of quantifiers
- a unique index from the set (n | 0 <= n < n_max).
- That index will serve to identify the memory location where the evaluation
- of the term/predicate is stored for the given tuple of quantifier.
- The following gives the smallest set of such indexes (hence we use the
- smallest amount of memory in some respect):
- To (t_shifted_n, t_shifted_n-1, ..., t_shifted_1)
- where 0 <= t_shifted_i < beta_i
- corresponds:
- sum_from_i_eq_1_to_n(
- t_shifted_i *
- mult_from_j_eq_1_to_i-1(beta_j)
- )
- *)
- match mem_infos with
- | [] ->
- Logic_const.tinteger ~loc 0
- | [(_, t_shifted)] ->
- t_shifted
- | (_, t_shifted) :: mem_infos' ->
- let index' = index_from_mem_infos ~loc mem_infos' in
- let bi = t_shifted in
- let rec pi_beta_j mem_infos = match mem_infos with
- | [] ->
- Logic_const.tinteger ~loc 1
- | (t_size, _) :: mem_infos' ->
- let pi_beta_j' = pi_beta_j mem_infos' in
- Logic_const.term ~loc (TBinOp(Mult, t_size, pi_beta_j')) Linteger
- in
- let pi_beta_j = pi_beta_j mem_infos' in
- let bi_mult_pi_beta_j = Logic_const.term ~loc
- (TBinOp(Mult, bi, pi_beta_j)) Linteger
- in
- Logic_const.term ~loc (TBinOp(PlusA, bi_mult_pi_beta_j, index')) Linteger
-
-and mk_storing_loops ~loc kf env lscope lval pot =
- match lscope with
- | [] ->
- begin match pot with
- | PoTPred p ->
- let e, env = named_predicate_to_exp kf (Env.push env) p lscope in
- let storing_stmt =
- Cil.mkStmtOneInstr ~valid_sid:true (Set(lval, e, loc))
- in
- let block, env = Env.pop_and_get
- env storing_stmt ~global_clear:true Env.After
- in
- block, env
- | PoTTerm t ->
- begin match Typing.get_integer_ty t with
- | Typing.C_type _ | Typing.Other ->
- let e, env = term_to_exp kf (Env.push env) t lscope in
- let storing_stmt =
- Cil.mkStmtOneInstr ~valid_sid:true (Set(lval, e, loc))
- in
- let block, env = Env.pop_and_get
- env storing_stmt ~global_clear:true Env.After
- in
- block, env
- | Typing.Gmp ->
- not_yet env "\\at with non-void logic scope and over gmp type"
- end
- end
- | LvsQuantif(tmin, lv, tmax) :: lscope' ->
- let vi_of_lv = Env.Logic_binding.get env lv in
- let env = Env.push env in
- let vi_of_lv, _, env = Env.Logic_binding.add ~ty:vi_of_lv.vtype env lv in
- let t_lv = Logic_const.tvar ~loc lv in
- (* Guard *)
- let guard = Logic_const.term
- ~loc
- (TBinOp(Le, t_lv, tmax))
- (Ctype Cil.intType)
- in
- Typing.type_term ~use_gmp_opt:false ~ctx:Typing.c_int guard;
- let guard_exp, env =
- term_to_exp kf env guard lscope
- in
- (* Break *)
- let break_stmt = Cil.mkStmt ~valid_sid:true (Break guard_exp.eloc) in
- (* Inner loop *)
- let loop', env = mk_storing_loops ~loc kf env lscope' lval pot in
- let loop' = Cil.mkStmt ~valid_sid:true (Block loop') in
- (* Loop counter *)
- let plus_one_term = Logic_const.term
- ~loc
- (TBinOp(PlusA, t_lv, Logic_const.tinteger ~loc 1))
- Linteger
- in
- Typing.type_term ~use_gmp_opt:true plus_one_term;
- let plus_one_exp, env = term_to_exp kf env plus_one_term lscope in
- let plus_one_stmt = match Typing.get_integer_ty plus_one_term with
- | Typing.C_type _ | Typing.Gmp->
- Gmpz.init_set ~loc (Cil.var vi_of_lv) (Cil.evar vi_of_lv) plus_one_exp
- | Typing.Other ->
- assert false
- in
- (* If guard is satisfiable then inner loop, else break *)
- let if_stmt = Cil.mkStmt
- ~valid_sid:true
- (If(guard_exp,
- Cil.mkBlock [loop'; plus_one_stmt],
- Cil.mkBlock [ break_stmt ],
- guard_exp.eloc))
- in
- let loop = Cil.mkStmt
- ~valid_sid:true
- (Loop ([],
- Cil.mkBlock [ if_stmt ],
- loc,
- None,
- Some break_stmt))
- in
- (* Init lv *)
- let tmin_exp, env = term_to_exp kf env tmin lscope in
- let set_tmin = match Typing.get_integer_ty plus_one_term with
- | Typing.C_type _ | Typing.Gmp->
- Gmpz.init_set ~loc (Cil.var vi_of_lv) (Cil.evar vi_of_lv) tmin_exp
- | Typing.Other ->
- assert false
- in
- (* The whole block *)
- let block, env = Env.pop_and_get
- env (Cil.mkEmptyStmt ~loc ()) ~global_clear:true Env.After
- in
- block.bstmts <- block.bstmts @ [set_tmin; loop];
- block, env
- | LvsLet(lv, t) :: lscope' ->
- let vi_of_lv = Env.Logic_binding.get env lv in
- let env = Env.push env in
- let vi_of_lv, exp_of_lv, env =
- Env.Logic_binding.add ~ty:vi_of_lv.vtype env lv
- in
- let e, env = term_to_exp kf env t lscope in
- let let_stmt = Gmpz.init_set
- ~loc (Cil.var vi_of_lv) exp_of_lv e
- in
- let block', env = mk_storing_loops ~loc kf env lscope' lval pot in
- (* The whole block *)
- let block, env = Env.pop_and_get
- env (Cil.mkEmptyStmt ~loc ()) ~global_clear:true Env.After
- in
- block.bstmts <-
- block.bstmts @ [let_stmt; Cil.mkStmt ~valid_sid:true (Block block')];
- block, env
- | LvsFormal _ :: _ ->
- not_yet env "\\at using formal variable of a logic function"
- | LvsGlobal _ :: _ ->
- not_yet env "\\at using global logic variable"
-
-and term_has_lv_from_vi t =
- let o = object(self) inherit Visitor.frama_c_inplace
- val mutable has_vi = false
- method !vlogic_var_use lv =
- match lv.lv_origin with
- | None ->
- Cil.DoChildren
- | Some _ ->
- has_vi <- true;
- Cil.SkipChildren
- method visit t =
- ignore (Visitor.visitFramacTerm (self :> Visitor.frama_c_inplace) t);
- has_vi
- end
- in
- o#visit t
-
-and named_predicate_to_exp ?name kf ?rte env p lscope =
+and named_predicate_to_exp ?name kf ?rte env p =
let rte = match rte with None -> Env.generate_rte env | Some b -> b in
let env = Env.rte env false in
- let e, env = named_predicate_content_to_exp ?name kf env p lscope in
+ let e, env = named_predicate_content_to_exp ?name kf env p in
let env = if rte then translate_rte kf env e else env in
let cast = Typing.get_cast_of_predicate p in
add_cast
@@ -1505,8 +1125,10 @@ and translate_named_predicate kf env p =
Printer.pp_predicate p;
let rte = Env.generate_rte env in
Typing.type_named_predicate ~must_clear:rte p;
- let e, env = named_predicate_to_exp kf ~rte env p [] in
+ let e, env = named_predicate_to_exp kf ~rte env p in
assert (Typ.equal (Cil.typeOf e) Cil.intType);
+ (* We need to reset the logical scope before translating next predicate *)
+ let env = Env.reset_lscope env in
Env.add_stmt
env
(Misc.mk_e_acsl_guard ~reverse:true (Env.annotation_kind env) kf e p)
@@ -1516,14 +1138,16 @@ let named_predicate_to_exp ?name kf env p =
let () =
Quantif.term_to_exp_ref := term_to_exp;
- Quantif.predicate_to_exp_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
(* This function is used by Guillaume.
However, it is correct to use it only in specific contexts. *)
let predicate_to_exp kf p =
Typing.type_named_predicate ~must_clear:true p;
let empty_env = Env.empty (new Visitor.frama_c_copy Project_skeleton.dummy) in
- let e, _ = named_predicate_to_exp kf empty_env p [] in
+ let e, _ = named_predicate_to_exp kf empty_env p in
assert (Typ.equal (Cil.typeOf e) Cil.intType);
e
@@ -1545,7 +1169,7 @@ let term_to_exp typ t =
let env = Env.push env in
let env = Env.rte env false in
let e, env =
- try term_to_exp (Kernel_function.dummy ()) env t []
+ try term_to_exp (Kernel_function.dummy ()) env t
with Misc.Unregistered_library_function _ -> raise (No_simple_translation t)
in
if not (Env.has_no_new_stmt env) then raise (No_simple_translation t);
diff --git a/src/plugins/e-acsl/typing.mli b/src/plugins/e-acsl/typing.mli
index 25249cc8c19..e8a74d55ae8 100644
--- a/src/plugins/e-acsl/typing.mli
+++ b/src/plugins/e-acsl/typing.mli
@@ -138,7 +138,8 @@ val unsafe_set: term -> ?ctx:integer_ty -> integer_ty -> unit
(*****************************************************************************)
val ty_of_interv: ?ctx:integer_ty -> Ival.t -> integer_ty
-
+(* Compute the smallest type (bigger than [int]) which can contain the whole
+ interval. It is the \theta operator of the JFLA's paper. *)
(******************************************************************************)
(** {2 Internal stuff} *)
diff --git a/src/plugins/e-acsl/visit.ml b/src/plugins/e-acsl/visit.ml
index b28c0142a5c..44a647da785 100644
--- a/src/plugins/e-acsl/visit.ml
+++ b/src/plugins/e-acsl/visit.ml
@@ -456,6 +456,51 @@ you must call function `%s' and `__e_acsl_memory_clean by yourself.@]"
f.slocals <- locals;
f.sbody.blocals <- blocks
+ (* Memory management for \at on purely logical variables:
+ Put [malloc] and [free] stmts at proper locations *)
+ method private insert_malloc_and_free_stmts kf f =
+ let malloc_stmts, free_stmts =
+ At_with_lscope.get_malloc_and_free_stmts f
+ in
+ let fstmts = malloc_stmts @ f.sbody.bstmts in
+ let fstmts =
+ if Kernel_function.is_entry_point kf then begin
+ (* [main] is a special case:
+ [main]'s stmts will be wrapped by things like
+ [memory_clean] and [memory_init afterwards] *)
+ match List.rev fstmts with
+ | [] ->
+ (* Cil normalization: there is always a [return] stmt *)
+ assert false
+ | return :: fsmts' ->
+ let fsmts = return :: free_stmts @ fsmts' in
+ List.rev fsmts
+ end
+ else begin
+ (* The last stmt might not be a [return] but a block ending with
+ a [return] (eg: functions with contract)
+ This could potentially (?) happen in a nested manner: that is
+ a block (ending with a block)^n ending with a [return] *)
+ let rec insert_free_stmts stmts free_stmts =
+ match List.rev stmts with
+ | [] ->
+ assert false
+ | stmt :: stmts' ->
+ begin match stmt.skind with
+ | Return _ ->
+ (List.rev stmts') @ free_stmts @ [stmt]
+ | Block b ->
+ b.bstmts <- insert_free_stmts b.bstmts free_stmts;
+ stmts
+ | _ ->
+ assert false
+ end
+ in
+ insert_free_stmts fstmts free_stmts
+ end
+ in
+ f.sbody.bstmts <- fstmts
+
method !vfunc f =
if generate then begin
Exit_points.generate f;
@@ -467,49 +512,7 @@ you must call function `%s' and `__e_acsl_memory_clean by yourself.@]"
(fun f ->
Exit_points.clear ();
self#add_generated_variables_in_function f;
- (* Memory management for \at with non-void logic scope:
- Put [malloc] and [free] stmts at proper locations *)
- let malloc_stmts, free_stmts = Lscope.get_malloc_and_free_stmts f in
- let fstmts = malloc_stmts @ f.sbody.bstmts in
- let fstmts =
- if f.svar.vname = "main" then begin
- (* [main] is a special case:
- [main]'s stmts will be wrapped by things like
- [memory_clean] and [memory_init afterwards] *)
- match List.rev fstmts with
- | [] ->
- (* Cil normalization: there is always a [return] stmt *)
- assert false
- | [return] ->
- free_stmts @ [return]
- | return :: (stmt :: fstmts) ->
- (List.rev fstmts) @ [stmt] @ free_stmts @ [return]
- end
- else begin
- (* The last stmt might not be a [return] but a block ending with
- a [return] (eg: functions with contract)
- This could potentially (?) happen in a nested manner: that is
- a block (ending with a block)^n ending with a [return] *)
- let rec insert_free_stmts stmts free_stmts =
- match List.rev stmts with
- | [] ->
- assert false
- | stmt :: stmts' ->
- begin match stmt.skind with
- | Return _ ->
- (List.rev stmts') @ free_stmts @ [stmt]
- | Block b ->
- b.bstmts <- insert_free_stmts b.bstmts free_stmts;
- stmts
- | _ ->
- assert false
- end
- in
- insert_free_stmts fstmts free_stmts
- end
- in
- f.sbody.bstmts <- fstmts;
- (* Return *)
+ self#insert_malloc_and_free_stmts kf f;
Options.feedback ~dkey ~level:2 "function %a done."
Kernel_function.pretty kf;
f)
--
GitLab