From 6c45c7a3b66a35874ee4386445c0535888e76a81 Mon Sep 17 00:00:00 2001
From: Fonenantsoa Maurica <maurica.fonenantsoa@gmail.com>
Date: Fri, 5 Oct 2018 14:41:20 +0200
Subject: [PATCH] Memory instrumentation moved in Mmodel_translate.
---
src/plugins/e-acsl/Makefile.in | 1 +
src/plugins/e-acsl/misc.ml | 5 +
src/plugins/e-acsl/misc.mli | 4 +
src/plugins/e-acsl/mmodel_translate.ml | 359 ++++++++++++++++++++++++
src/plugins/e-acsl/mmodel_translate.mli | 60 ++++
src/plugins/e-acsl/translate.ml | 356 ++---------------------
6 files changed, 458 insertions(+), 327 deletions(-)
create mode 100644 src/plugins/e-acsl/mmodel_translate.ml
create mode 100644 src/plugins/e-acsl/mmodel_translate.mli
diff --git a/src/plugins/e-acsl/Makefile.in b/src/plugins/e-acsl/Makefile.in
index 13768e6bfbc..935abd3c882 100644
--- a/src/plugins/e-acsl/Makefile.in
+++ b/src/plugins/e-acsl/Makefile.in
@@ -78,6 +78,7 @@ PLUGIN_CMO:= local_config \
loops \
quantif \
at_with_lscope \
+ mmodel_translate \
translate \
temporal \
prepare_ast \
diff --git a/src/plugins/e-acsl/misc.ml b/src/plugins/e-acsl/misc.ml
index 89ff5794ca4..e4971d0f5b5 100644
--- a/src/plugins/e-acsl/misc.ml
+++ b/src/plugins/e-acsl/misc.ml
@@ -306,6 +306,11 @@ let term_has_lv_from_vi t =
type pred_or_term = PoT_pred of predicate | PoT_term of term
+let mk_ptr_sizeof typ loc =
+ match Cil.unrollType typ with
+ | TPtr (t', _) -> Cil.new_exp ~loc (SizeOf t')
+ | _ -> assert false
+
(*
Local Variables:
compile-command: "make"
diff --git a/src/plugins/e-acsl/misc.mli b/src/plugins/e-acsl/misc.mli
index 006fa6d4383..6c61e732290 100644
--- a/src/plugins/e-acsl/misc.mli
+++ b/src/plugins/e-acsl/misc.mli
@@ -120,6 +120,10 @@ val term_has_lv_from_vi: term -> bool
type pred_or_term = PoT_pred of predicate | PoT_term of term
+val mk_ptr_sizeof: typ -> location -> exp
+(* [mk_ptr_sizeof ptr_typ loc] takes the pointer typ [ptr_typ] that points
+ to a [typ] typ and returns [sizeof(typ)]. *)
+
(*
Local Variables:
compile-command: "make"
diff --git a/src/plugins/e-acsl/mmodel_translate.ml b/src/plugins/e-acsl/mmodel_translate.ml
new file mode 100644
index 00000000000..1172ffc3301
--- /dev/null
+++ b/src/plugins/e-acsl/mmodel_translate.ml
@@ -0,0 +1,359 @@
+(**************************************************************************)
+(* *)
+(* 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"
+
+(*****************************************************************************)
+(****************************** Ranges Elimination ***************************)
+(*****************************************************************************)
+
+(* We call Range Elimination the operation through which ranges are
+ substituted by universally quantified logic variables.
+ Example:
+ [\valid(&t[(n-1)..(n+2)][1][0..1])] can be soundly transformed into
+ [\forall integer q1; n-1 <= q1 <= n+2 ==>
+ \forall integer q2; 0 <= q2 <= 1 ==>
+ \valid(&t[q1][1][q2])]
+ However, the substition can be unsound,
+ in which case [Range_elimination_exception] must be raised.
+ Example:
+ [\valid(&t[(0..2)==(0..2) ? 0 : 1])] is equivalent to [\valid(&t[0])]
+ since [==] refers to set equality when applied on ranges.
+ But Range Elimination will give a predicate equivalent to [\valid(&t[1])]
+ since [\forall 0 <= q1,q2 <= 2: q1==q2] is false.
+ Hence [Range_elimination_exception] must be raised. *)
+exception Range_elimination_exception
+
+(* Takes a [toffset] and checks whether it contains an index that is a set *)
+let rec has_set_as_index = function
+ | TNoOffset ->
+ false
+ | TIndex(t, toffset) ->
+ Logic_const.is_set_type t.term_type || has_set_as_index toffset
+ | TModel(_, toffset) | TField(_, toffset) ->
+ has_set_as_index toffset
+
+(* Performs Range Elimination on index [TIndex(term, offset)]. Term part.
+ Raises [Range_elimination_exception] if whether the operation is unsound or
+ if we don't support the construction yet. *)
+let eliminate_ranges_from_index_of_term ~loc t =
+ match t.term_node with
+ | Trange(Some n1, Some n2) ->
+ let name = Env.Varname.get ~scope:Env.Local_block "range" in
+ let lv = Cil_const.make_logic_var_kind name LVQuant Linteger in
+ let tlv = Logic_const.tvar ~loc lv in
+ tlv, (n1, lv, n2)
+ | _ ->
+ raise Range_elimination_exception
+
+(* Performs Range Elimination on index [TIndex(term, offset)]. Offset part.
+ Raises [Range_elimination_exception], through [eliminate_ranges_from_
+ index_of_term], if whether the operation is unsound or
+ if we don't support the construction yet. *)
+let rec eliminate_ranges_from_index_of_toffset ~loc toffset quantifiers =
+ match toffset with
+ | TIndex(t, toffset') ->
+ if Misc.is_range_free t then
+ let toffset', quantifiers' =
+ eliminate_ranges_from_index_of_toffset ~loc toffset' quantifiers
+ in
+ TIndex(t, toffset'), quantifiers'
+ else
+ (* Attempt Range Elimination on [t] *)
+ let t1, quantifiers1 =
+ eliminate_ranges_from_index_of_term ~loc t
+ in
+ let toffset2, quantifiers2 =
+ eliminate_ranges_from_index_of_toffset ~loc toffset' quantifiers
+ in
+ let toffset3 = TIndex(t1, toffset2) in
+ toffset3, quantifiers1 :: quantifiers2
+ | TNoOffset ->
+ toffset, quantifiers
+ | TModel _ ->
+ Error.not_yet "range elimination on TModel"
+ | TField _ ->
+ Error.not_yet "range elimination on TField"
+
+(*****************************************************************************)
+(********************** Calls without Range Elimination **********************)
+(************** \base_addr, \block_length, \offset, \freeable ****************)
+(*****************************************************************************)
+
+(* \base_addr, \block_length, \offset and \freeable *)
+let call ~loc kf name ctx env t =
+ assert (name = "base_addr" || name = "block_length"
+ || name = "offset" || name ="freeable");
+ let term_to_exp = !term_to_exp_ref in
+ let e, env = term_to_exp kf (Env.rte env true) t in
+ let _, res, env =
+ Env.new_var
+ ~loc
+ ~name
+ env
+ None
+ ctx
+ (fun v _ ->
+ let name = Functions.RTL.mk_api_name name in
+ [ Misc.mk_call ~loc ~result:(Cil.var v) name [ e ] ])
+ in
+ res, env
+
+(*****************************************************************************)
+(************************* Calls with Range Elimination **********************)
+(********************** \initialized, \valid, \valid_read ********************)
+(*****************************************************************************)
+
+(* Call to [__e_acsl_<name>] for terms of the form [p + r]
+ when [<name> = valid or initialized or valid_read] and
+ where [p] is an address and [r] a range offset *)
+let call_memory_block ~loc kf name ctx env p r =
+ let n1, n2 = match r.term_node with
+ | Trange(Some n1, Some n2) ->
+ n1, n2
+ | Trange(None, _) | Trange(_, None) ->
+ Options.abort "unbounded ranges are not part of E-ACSL"
+ | _ ->
+ assert false
+ in
+ (* s *)
+ let ty = match Cil.unrollType (Misc.cty p.term_type) with
+ | TPtr(ty, _) | TArray(ty, _, _, _) -> ty
+ | _ -> assert false
+ in
+ let s = Logic_const.term ~loc (TSizeOf ty) Linteger in
+ (* ptr *)
+ let typ_charptr = Cil.charPtrType in
+ let ptr = Logic_const.term
+ ~loc
+ (TBinOp(
+ PlusPI,
+ Logic_utils.mk_cast ~loc ~force:false typ_charptr p,
+ Logic_const.term ~loc (TBinOp(Mult, s, n1)) Linteger))
+ (Ctype typ_charptr)
+ in
+ Typing.type_term ~use_gmp_opt:false ~ctx:Typing.other ptr;
+ let term_to_exp = !term_to_exp_ref in
+ let ptr, env = term_to_exp kf (Env.rte env true) ptr in
+ (* size *)
+ let size = Logic_const.term
+ ~loc
+ (TBinOp(
+ Mult,
+ s,
+ Logic_const.term ~loc (TBinOp(MinusA, n2, n1)) Linteger))
+ Linteger
+ in
+ let ctx_ity = Typing.integer_ty_of_typ ctx in
+ Typing.type_term ~use_gmp_opt:false ~ctx:ctx_ity size;
+ let ity = Typing.get_integer_ty size in
+ if ity = Typing.gmp then Error.not_yet "size of memory area in GMP";
+ let size, env = term_to_exp kf env size in
+ let size = Cil.constFold false size in
+ (* base and base_addr *)
+ let base, _ = Misc.ptr_index ~loc ptr in
+ let base_addr = match base.enode with
+ | AddrOf _ | Const _ -> Cil.zero ~loc
+ | Lval lv | StartOf lv -> Cil.mkAddrOrStartOf ~loc lv
+ | _ -> assert false
+ in
+ (* generating env *)
+ let _, e, env =
+ Env.new_var
+ ~loc
+ ~name
+ env
+ None
+ ctx
+ (fun v _ ->
+ let fname = Functions.RTL.mk_api_name name in
+ let args = match name with
+ | "valid" | "valid_read" -> [ ptr; size; base; base_addr ]
+ | "initialized" -> [ ptr; size ]
+ | _ -> Error.not_yet ("builtin " ^ name)
+ in
+ [ Misc.mk_call ~loc ~result:(Cil.var v) fname args ])
+ in
+ e, env
+
+(* [call_with_ranges] handles ranges in [t] when calling builtin [name].
+ It only supports the following cases for the time being:
+ A: [\builtin(p+r)] where [p] is an address and [r] a range or
+ [\builtin(t[r])] or
+ [\builtin(t[i_1]...[i_n])] where [t] is dynamically allocated
+ and all the indexes are integers,
+ except the last one which is a range
+ The generated code is a SINGLE call to the corresponding E-ACSL builtin
+ B: [\builtin(t[i_1]...[i_n])] where [t] is NOT dynamically allocated
+ and the indexes are integers or ranges
+ The generated code is a SET OF calls to the corresponding E-ACSL builtin
+ C: Any other use of ranges/No range
+ Call [call_default] which performs the translation for
+ range free terms, and raises Not_yet if it ever encouters a range.
+ Example for case:
+ A: [\valid(&t[3..5])]
+ Contiguous locations -> a single call to [__e_acsl_valid]
+ B: [\valid(&t[4][3..5][2])]
+ NON-contiguous locations -> multiple calls (3) to [__e_acsl_valid] *)
+let call_with_ranges ~loc kf name ctx env t call_default =
+ if Misc.is_bitfield_pointers t.term_type then
+ Error.not_yet "bitfield pointer";
+ match t.term_node with
+ | TBinOp((PlusPI | IndexPI), p, ({ term_node = Trange _ } as r)) ->
+ if Misc.is_set_of_ptr_or_array p.term_type then
+ Error.not_yet "arithmetic over set of pointers or arrays"
+ else
+ (* Case A *)
+ call_memory_block ~loc kf name ctx env p r
+ | TAddrOf(TVar lv, TIndex({ term_node = Trange _ } as r, TNoOffset)) ->
+ (* Case A *)
+ assert (Logic_const.is_set_type t.term_type);
+ let lty_noset = Logic_const.type_of_element t.term_type in
+ let p = Logic_const.taddrof ~loc (TVar lv, TNoOffset) lty_noset in
+ call_memory_block ~loc kf name ctx env p r
+ | TAddrOf(TVar ({ lv_type = Ctype (TArray _) } as lv), toffset) ->
+ if has_set_as_index toffset then
+ (* Case B *)
+ try
+ let toffset', quantifiers =
+ eliminate_ranges_from_index_of_toffset ~loc toffset []
+ in
+ let lty_noset =
+ if Logic_const.is_set_type t.term_type then
+ Logic_const.type_of_element t.term_type
+ else
+ t.term_type
+ in
+ let t' = Logic_const.taddrof ~loc (TVar lv, toffset') lty_noset in
+ let p_quantified =
+ (* [loc] prevents a type error with eta-expansion and label *)
+ let loc = Some loc in
+ let call f = f ?loc (Logic_const.here_label, t') in
+ match name with
+ | "valid" -> call Logic_const.pvalid
+ | "initialized" -> call Logic_const.pinitialized
+ | "valid_read" -> call Logic_const.pvalid_read
+ | _ -> Options.fatal "[call_with_ranges] unexpected builtin"
+ in
+ let p_quantified = List.fold_left
+ (fun p (tmin, lv, tmax) ->
+ (* \forall integer tlv; tmin <= tlv <= tmax ==> p *)
+ let tlv = Logic_const.tvar ~loc lv in
+ let lower_bound = Logic_const.prel ~loc (Rle, tmin, tlv) in
+ let upper_bound = Logic_const.prel ~loc (Rle, tlv, tmax) in
+ let bound = Logic_const.pand ~loc (lower_bound, upper_bound) in
+ let bound_imp_p = Logic_const.pimplies ~loc (bound, p) in
+ Logic_const.pforall ~loc ([lv], bound_imp_p))
+ p_quantified
+ quantifiers
+ in
+ Typing.type_named_predicate ~must_clear:true p_quantified;
+ let named_predicate_to_exp = !predicate_to_exp_ref in
+ named_predicate_to_exp kf env p_quantified
+ with Range_elimination_exception ->
+ (* Case C *)
+ call_default ~loc kf name ctx env t
+ else
+ (* Case C *)
+ call_default ~loc kf name ctx env t
+ | _ ->
+ (* Case C *)
+ call_default ~loc kf name ctx env t
+
+(* \initialized *)
+let call_with_size ~loc kf name ctx env t =
+ assert (name = "initialized");
+ let call_for_unsupported_constructs ~loc kf name ctx env t =
+ let term_to_exp = !term_to_exp_ref in
+ let e, env = term_to_exp kf (Env.rte env true) t in
+ let _, res, env =
+ Env.new_var
+ ~loc
+ ~name
+ env
+ None
+ ctx
+ (fun v _ ->
+ let ty = Misc.cty t.term_type in
+ let sizeof = Misc.mk_ptr_sizeof ty loc in
+ let fname = Functions.RTL.mk_api_name name in
+ [ Misc.mk_call ~loc ~result:(Cil.var v) fname [ e; sizeof ] ])
+ in
+ res, env
+ in
+ call_with_ranges
+ ~loc
+ kf
+ name
+ ctx
+ env
+ t
+ call_for_unsupported_constructs
+
+(* \valid and \valid_read *)
+let call_valid ~loc kf name ctx env t =
+ assert (name = "valid" || name = "valid_read");
+ let call_for_unsupported_constructs ~loc kf name ctx env t =
+ let term_to_exp = !term_to_exp_ref in
+ let e, env = term_to_exp kf (Env.rte env true) t in
+ let base, _ = Misc.ptr_index ~loc e in
+ let base_addr = match base.enode with
+ | AddrOf _ | Const _ -> Cil.zero ~loc
+ | Lval lv | StartOf lv -> Cil.mkAddrOrStartOf ~loc lv
+ | _ -> assert false
+ in
+ let _, res, env =
+ Env.new_var
+ ~loc
+ ~name
+ env
+ None
+ ctx
+ (fun v _ ->
+ let ty = Misc.cty t.term_type in
+ let sizeof = Misc.mk_ptr_sizeof ty loc in
+ let fname = Functions.RTL.mk_api_name name in
+ let args = [ e; sizeof; base; base_addr ] in
+ [ Misc.mk_call ~loc ~result:(Cil.var v) fname args ])
+ in
+ res, env
+ in
+ call_with_ranges
+ ~loc
+ kf
+ name
+ ctx
+ env
+ t
+ call_for_unsupported_constructs
\ No newline at end of file
diff --git a/src/plugins/e-acsl/mmodel_translate.mli b/src/plugins/e-acsl/mmodel_translate.mli
new file mode 100644
index 00000000000..eeed2bc1120
--- /dev/null
+++ b/src/plugins/e-acsl/mmodel_translate.mli
@@ -0,0 +1,60 @@
+(**************************************************************************)
+(* *)
+(* 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
+
+(* Create calls to a few memory builtins.
+ Partial support for ranges is provided. *)
+
+val call:
+ loc:location -> kernel_function -> string -> typ -> Env.t -> term ->
+ exp * Env.t
+(* [call ~loc kf name ctx env t] creates a call to the E-ACSL memory builtin
+ identified by [name] which only requires a single argument, namely the
+ pointer under study. The supported builtins are:
+ [base_addr], [block_length], [offset] and [freeable]. *)
+
+val call_with_size:
+ loc:location -> kernel_function -> string -> typ -> Env.t -> term ->
+ exp * Env.t
+(* [call_with_size ~loc kf name ctx env t] creates a call to the E-ACSL memory
+ builtin identified by [name] which requires two arguments, namely
+ the pointer under study and a size in bytes.
+ The only supported builtin is: [initialized].
+ [t] can denote ranges of memory locations. *)
+
+val call_valid:
+ loc:location -> kernel_function -> string -> typ -> Env.t -> term ->
+ exp * Env.t
+(* [call_valid ~loc kf name ctx env t] creates a call to the E-ACSL memory
+ builtin [valid] or [valid_read] according to [name].
+ [t] can denote ranges of memory locations. *)
+
+(**************************************************************************)
+(********************** 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
\ No newline at end of file
diff --git a/src/plugins/e-acsl/translate.ml b/src/plugins/e-acsl/translate.ml
index d77e94913a3..e57580f53f2 100644
--- a/src/plugins/e-acsl/translate.ml
+++ b/src/plugins/e-acsl/translate.ml
@@ -39,78 +39,6 @@ let handle_error f env =
It is [true] iff we are currently visiting \valid. *)
let is_visiting_valid = ref false
-(*****************************************************************************)
-(*************************** Ranges in a few builtins ************************)
-(*****************************************************************************)
-
-(* We call Range Elimination the operation through which ranges are
- substituted by universally quantified logic variables.
- Example:
- [\valid(&t[(n-1)..(n+2)][1][0..1])] can be soundly transformed into
- [\forall integer q1; n-1 <= q1 <= n+2 ==>
- \forall integer q2; 0 <= q2 <= 1 ==>
- \valid(&t[q1][1][q2])]
- However, the substition can be unsound,
- in which case [Range_elimination_exception] must be raised.
- Example:
- [\valid(&t[(0..2)==(0..2) ? 0 : 1])] is equivalent to [\valid(&t[0])]
- since [==] refers to set equality when applied on ranges.
- But Range Elimination will give a predicate equivalent to [\valid(&t[1])]
- since [\forall 0 <= q1,q2 <= 2: q1==q2] is false.
- Hence [Range_elimination_exception] must be raised. *)
-exception Range_elimination_exception
-
-(* Takes a [toffset] and checks whether it contains an index that is a set *)
-let rec has_set_as_index = function
- | TNoOffset ->
- false
- | TIndex(t, toffset) ->
- Logic_const.is_set_type t.term_type || has_set_as_index toffset
- | TModel(_, toffset) | TField(_, toffset) ->
- has_set_as_index toffset
-
-(* Performs Range Elimination on index [TIndex(term, offset)]. Term part.
- Raises [Range_elimination_exception] if whether the operation is unsound or
- if we don't support the construction yet. *)
-let eliminate_ranges_from_index_of_term ~loc t =
- match t.term_node with
- | Trange(Some n1, Some n2) ->
- let name = Env.Varname.get ~scope:Env.Local_block "range" in
- let lv = Cil_const.make_logic_var_kind name LVQuant Linteger in
- let tlv = Logic_const.tvar ~loc lv in
- tlv, (n1, lv, n2)
- | _ ->
- raise Range_elimination_exception
-
-(* Performs Range Elimination on index [TIndex(term, offset)]. Offset part.
- Raises [Range_elimination_exception], through [eliminate_ranges_from_
- index_of_term], if whether the operation is unsound or
- if we don't support the construction yet. *)
-let rec eliminate_ranges_from_index_of_toffset ~loc toffset quantifiers =
- match toffset with
- | TIndex(t, toffset') ->
- if Misc.is_range_free t then
- let toffset', quantifiers' =
- eliminate_ranges_from_index_of_toffset ~loc toffset' quantifiers
- in
- TIndex(t, toffset'), quantifiers'
- else
- (* Attempt Range Elimination on [t] *)
- let t1, quantifiers1 =
- eliminate_ranges_from_index_of_term ~loc t
- in
- let toffset2, quantifiers2 =
- eliminate_ranges_from_index_of_toffset ~loc toffset' quantifiers
- in
- let toffset3 = TIndex(t1, toffset2) in
- toffset3, quantifiers1 :: quantifiers2
- | TNoOffset ->
- toffset, quantifiers
- | TModel _ ->
- Error.not_yet "range elimination on TModel"
- | TField _ ->
- Error.not_yet "range elimination on TField"
-
(* ************************************************************************** *)
(* Transforming terms and predicates into C expressions (if any) *)
(* ************************************************************************** *)
@@ -572,15 +500,21 @@ and context_insensitive_term_to_exp kf env t =
let e, env, is_mpz_string = at_to_exp_no_lscope env (Some t) label e in
e, env, is_mpz_string, ""
| Tbase_addr(BuiltinLabel Here, t) ->
- mmodel_call ~loc kf "base_addr" Cil.voidPtrType env t
+ let name = "base_addr" in
+ let e, env = Mmodel_translate.call ~loc kf name Cil.voidPtrType env t in
+ e, env, false, name
| 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
+ let name = "offset" in
+ let e, env = Mmodel_translate.call ~loc kf name size_t env t in
+ e, env, false, name
| 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
+ let name = "block_length" in
+ let e, env = Mmodel_translate.call ~loc kf name size_t env t in
+ e, env, false, name
| 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 *)
@@ -652,247 +586,6 @@ and comparison_to_exp
| Typing.C_type _ | Typing.Other ->
Cil.mkBinOp ~loc bop e1 e2, env
-(* \base_addr, \block_length and \freeable annotations *)
-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
- ~name
- env
- None
- ctx
- (fun v _ ->
- let name = Functions.RTL.mk_api_name name in
- [ Misc.mk_call ~loc ~result:(Cil.var v) name [ e ] ])
- in
- res, env, false, name
-
-and get_c_term_type = function
- | Ctype ty -> ty
- | _ -> assert false
-
-and mk_ptr_sizeof typ loc =
- match Cil.unrollType typ with
- | TPtr (t', _) -> Cil.new_exp ~loc (SizeOf t')
- | _ -> assert false
-
-(* \valid, \offset and \initialized annotations *)
-and mmodel_call_with_size ~loc kf name ctx env t =
- let call_for_unsupported_constructs ~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
- ~name
- env
- None
- ctx
- (fun v _ ->
- let ty = get_c_term_type t.term_type in
- let sizeof = mk_ptr_sizeof ty loc in
- let fname = Functions.RTL.mk_api_name name in
- [ Misc.mk_call ~loc ~result:(Cil.var v) fname [ e; sizeof ] ])
- in
- res, env
- in
- mmodel_call_with_ranges
- ~loc
- kf
- name
- ctx
- env
- t
- call_for_unsupported_constructs
-
-and mmodel_call_valid ~loc kf name ctx env t =
- let call_for_unsupported_constructs ~loc kf name ctx env t =
- let e, env = term_to_exp kf (Env.rte env true) t in
- let base, _ = Misc.ptr_index ~loc e in
- let base_addr = match base.enode with
- | AddrOf _ | Const _ -> Cil.zero ~loc
- | Lval lv | StartOf lv -> Cil.mkAddrOrStartOf ~loc lv
- | _ -> assert false
- in
- let _, res, env =
- Env.new_var
- ~loc
- ~name
- env
- None
- ctx
- (fun v _ ->
- let ty = get_c_term_type t.term_type in
- let sizeof = mk_ptr_sizeof ty loc in
- let fname = Functions.RTL.mk_api_name name in
- let args = [ e; sizeof; base; base_addr ] in
- [ Misc.mk_call ~loc ~result:(Cil.var v) fname args ])
- in
- res, env
- in
- mmodel_call_with_ranges
- ~loc
- kf
- name
- ctx
- env
- t
- call_for_unsupported_constructs
-
-(* [mmodel_call_with_ranges] handles ranges in [t] when calling builtin [name].
- It only supports the following cases for the time being:
- A: [\builtin(p+r)] where [p] is an address and [r] a range or
- [\builtin(t[r])] or
- [\builtin(t[i_1]...[i_n])] where [t] is dynamically allocated
- and all the indexes are integers,
- except the last one which is a range
- The generated code is a SINGLE call to the corresponding E-ACSL builtin
- B: [\builtin(t[i_1]...[i_n])] where [t] is NOT dynamically allocated
- and the indexes are integers or ranges
- The generated code is a SET OF calls to the corresponding E-ACSL builtin
- C: Any other use of ranges/No range
- Call [mmodel_call_default] which performs the translation for
- range free terms, and raises Not_yet if it ever encouters a range.
- Example for case:
- A: [\valid(&t[3..5])]
- Contiguous locations -> a single call to [__e_acsl_valid]
- B: [\valid(&t[4][3..5][2])]
- NON-contiguous locations -> multiple calls (3) to [__e_acsl_valid] *)
-and mmodel_call_with_ranges ~loc kf name ctx env t mmodel_call_default =
- if Misc.is_bitfield_pointers t.term_type then
- not_yet env "bitfield pointer";
- match t.term_node with
- | TBinOp((PlusPI | IndexPI), p, ({ term_node = Trange _ } as r)) ->
- if Misc.is_set_of_ptr_or_array p.term_type then
- not_yet env "arithmetic over set of pointers or arrays"
- else
- (* Case A *)
- mmodel_call_memory_block ~loc kf name ctx env p r
- | TAddrOf(TVar lv, TIndex({ term_node = Trange _ } as r, TNoOffset)) ->
- (* Case A *)
- assert (Logic_const.is_set_type t.term_type);
- let lty_noset = Logic_const.type_of_element t.term_type in
- let p = Logic_const.taddrof ~loc (TVar lv, TNoOffset) lty_noset in
- mmodel_call_memory_block ~loc kf name ctx env p r
- | TAddrOf(TVar ({ lv_type = Ctype (TArray _) } as lv), toffset) ->
- if has_set_as_index toffset then
- (* Case B *)
- try
- let toffset', quantifiers =
- eliminate_ranges_from_index_of_toffset ~loc toffset []
- in
- let lty_noset =
- if Logic_const.is_set_type t.term_type then
- Logic_const.type_of_element t.term_type
- else
- t.term_type
- in
- let t' = Logic_const.taddrof ~loc (TVar lv, toffset') lty_noset in
- let p_quantified =
- (* [loc] prevents a type error with eta-expansion and label *)
- let loc = Some loc in
- let call f = f ?loc (Logic_const.here_label, t') in
- match name with
- | "valid" -> call Logic_const.pvalid
- | "initialized" -> call Logic_const.pinitialized
- | "valid_read" -> call Logic_const.pvalid_read
- | _ -> Options.fatal "[mmodel_call_with_ranges] unexpected builtin"
- in
- let p_quantified = List.fold_left
- (fun p (tmin, lv, tmax) ->
- (* \forall integer tlv; tmin <= tlv <= tmax ==> p *)
- let tlv = Logic_const.tvar ~loc lv in
- let lower_bound = Logic_const.prel ~loc (Rle, tmin, tlv) in
- let upper_bound = Logic_const.prel ~loc (Rle, tlv, tmax) in
- let bound = Logic_const.pand ~loc (lower_bound, upper_bound) in
- let bound_imp_p = Logic_const.pimplies ~loc (bound, p) in
- Logic_const.pforall ~loc ([lv], bound_imp_p))
- p_quantified
- quantifiers
- in
- Typing.type_named_predicate ~must_clear:true p_quantified;
- named_predicate_to_exp kf env p_quantified
- with Range_elimination_exception ->
- (* Case C *)
- mmodel_call_default ~loc kf name ctx env t
- else
- (* Case C *)
- mmodel_call_default ~loc kf name ctx env t
- | _ ->
- (* Case C *)
- mmodel_call_default ~loc kf name ctx env t
-
-(* Call to [__e_acsl_<name>] for terms of the form [p + r]
- when [<name> = valid or initialized or valid_read] and
- where [p] is an address and [r] a range offset *)
-and mmodel_call_memory_block ~loc kf name ctx env p r =
- let n1, n2 = match r.term_node with
- | Trange(Some n1, Some n2) ->
- n1, n2
- | Trange(None, _) | Trange(_, None) ->
- Options.abort "unbounded ranges are not part of E-ACSL"
- | _ ->
- assert false
- in
- (* s *)
- let ty = match Cil.unrollType (get_c_term_type p.term_type) with
- | TPtr(ty, _) | TArray(ty, _, _, _) -> ty
- | _ -> assert false
- in
- let s = Logic_const.term ~loc (TSizeOf ty) Linteger in
- (* ptr *)
- let typ_charptr = Cil.charPtrType in
- let ptr = Logic_const.term
- ~loc
- (TBinOp(
- PlusPI,
- Logic_utils.mk_cast ~loc ~force:false typ_charptr p,
- Logic_const.term ~loc (TBinOp(Mult, s, n1)) Linteger))
- (Ctype typ_charptr)
- in
- Typing.type_term ~use_gmp_opt:false ~ctx:Typing.other ptr;
- let ptr, env = term_to_exp kf (Env.rte env true) ptr in
- (* size *)
- let size = Logic_const.term
- ~loc
- (TBinOp(
- Mult,
- s,
- Logic_const.term ~loc (TBinOp(MinusA, n2, n1)) Linteger))
- Linteger
- in
- let ctx_ity = Typing.integer_ty_of_typ ctx in
- Typing.type_term ~use_gmp_opt:false ~ctx:ctx_ity size;
- let ity = Typing.get_integer_ty size in
- if ity = Typing.gmp then not_yet env "size of memory area in GMP";
- let size, env = term_to_exp kf env size in
- let size = Cil.constFold false size in
- (* base and base_addr *)
- let base, _ = Misc.ptr_index ~loc ptr in
- let base_addr = match base.enode with
- | AddrOf _ | Const _ -> Cil.zero ~loc
- | Lval lv | StartOf lv -> Cil.mkAddrOrStartOf ~loc lv
- | _ -> assert false
- in
- (* generating env *)
- let _, e, env =
- Env.new_var
- ~loc
- ~name
- env
- None
- ctx
- (fun v _ ->
- let fname = Functions.RTL.mk_api_name name in
- let args = match name with
- | "valid" | "valid_read" -> [ ptr; size; base; base_addr ]
- | "initialized" -> [ ptr; size ]
- | _ -> not_yet env ("builtin " ^ name)
- in
- [ Misc.mk_call ~loc ~result:(Cil.var v) fname args ])
- in
- e, env
-
and at_to_exp_no_lscope env t_opt label e =
let stmt = E_acsl_label.get_stmt (Env.get_visitor env) label in
(* generate a new variable denoting [\at(t',label)].
@@ -1029,15 +722,15 @@ and named_predicate_content_to_exp ?name kf env p =
| (Pvalid(BuiltinLabel Here as llabel, t) as pc) ->
let call_valid t =
let name = match pc with
- | Pvalid _ -> "valid"
- | Pvalid_read _ -> "valid_read"
- | _ -> assert false
+ | Pvalid _ -> "valid"
+ | Pvalid_read _ -> "valid_read"
+ | _ -> assert false
in
- mmodel_call_valid ~loc kf name Cil.intType env t
+ Mmodel_translate.call_valid ~loc kf name Cil.intType env t
in
if !is_visiting_valid then begin
(* we already transformed \valid(t) into \initialized(&t) && \valid(t):
- now convert this right-most valid. *)
+ now convert this right-most valid. *)
is_visiting_valid := false;
call_valid t
end else begin
@@ -1050,7 +743,8 @@ and named_predicate_content_to_exp ?name kf env p =
let p = Logic_const.pand ~loc (init, p) in
is_visiting_valid := true;
named_predicate_to_exp kf env p
- | _ -> call_valid t
+ | _ ->
+ call_valid t
end
| Pvalid _ -> not_yet env "labeled \\valid"
| Pvalid_read _ -> not_yet env "labeled \\valid_read"
@@ -1059,15 +753,21 @@ and named_predicate_content_to_exp ?name kf env p =
(* optimisation when we know that the initialisation is ok *)
| TAddrOf (TResult _, TNoOffset) -> Cil.one ~loc, env
| TAddrOf (TVar { lv_origin = Some vi }, TNoOffset)
- when vi.vformal || vi.vglob || Functions.RTL.is_generated_name vi.vname ->
+ 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)
+ Mmodel_translate.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 in
- res, env
+ Mmodel_translate.call ~loc kf "freeable" Cil.intType env t
| Pfreeable _ -> not_yet env "labeled \\freeable"
| Pfresh _ -> not_yet env "\\fresh"
| Psubtype _ -> Error.untypable "subtyping relation" (* Jessie specific *)
@@ -1141,7 +841,9 @@ let () =
Loops.translate_named_predicate_ref := translate_named_predicate;
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
+ At_with_lscope.predicate_to_exp_ref := named_predicate_to_exp;
+ Mmodel_translate.term_to_exp_ref := term_to_exp;
+ Mmodel_translate.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. *)
--
GitLab