From 7b0eea9f4e1c93af6fda32b2e93a1cd452409143 Mon Sep 17 00:00:00 2001
From: Basile Desloges <basile.desloges@cea.fr>
Date: Tue, 21 Jul 2020 17:29:46 +0200
Subject: [PATCH] [eacsl:codegen] Add support of `\separated` for non-explicit
range
---
.../src/code_generator/memory_translate.ml | 467 ++++++++++--------
.../src/code_generator/memory_translate.mli | 20 +-
.../e-acsl/src/code_generator/translate.ml | 4 +-
3 files changed, 262 insertions(+), 229 deletions(-)
diff --git a/src/plugins/e-acsl/src/code_generator/memory_translate.ml b/src/plugins/e-acsl/src/code_generator/memory_translate.ml
index f06b6096a08..2b496a89f87 100644
--- a/src/plugins/e-acsl/src/code_generator/memory_translate.ml
+++ b/src/plugins/e-acsl/src/code_generator/memory_translate.ml
@@ -247,245 +247,286 @@ let range_to_ptr_and_size ~loc kf env ptr r p =
in
ptr, size, env
-(* Call to [__e_acsl_<name>] for terms of the form [ptr + r]
- when [<name> = valid or initialized or valid_read] and
- where [ptr] is an address and [r] a range offset *)
-let call_memory_block ~loc kf name ctx env ptr r p =
- let ptr, size, env = range_to_ptr_and_size ~loc kf env ptr r p in
- (* base and base_addr *)
- let base, _ = Misc.ptr_index ~loc ptr in
+(* Take a term without range [t] and return a tuple [(ptr, size, env)] where
+ [ptr] is an expression representing the term, [size] is the size of the
+ expression in bytes and [env] is the current environment.
+ [p] is the predicate under test. *)
+let term_to_ptr_and_size ~loc kf env t =
+ let e, env = !term_to_exp_ref kf (Env.rte env true) t in
+ let ty = Misc.cty t.term_type in
+ let sizeof = Misc.mk_ptr_sizeof ty loc in
+ e, sizeof, env
+
+(* Take an expression [e] and return a tuple [(base, base_addr)] where [base]
+ is the address [p] if [e] is of the form [p + i] and [e] otherwise, and
+ [base_addr] is the address [&p] if [e] is of the form [p + i] and 0
+ otherwise. *)
+let exp_to_base_and_baseaddr ~loc e =
+ 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
- (* generating env *)
- let args = match name with
- | "valid" | "valid_read" -> [ ptr; size; base; base_addr ]
- | "initialized" -> [ ptr; size ]
- | _ -> Error.not_yet ("builtin " ^ name)
- in
- Env.rtl_call_to_new_var
- ~loc
- ~name
- env
- kf
- None
- ctx
- name
- args
+ base, base_addr
-(* [call_with_ranges] handles ranges in [t] when calling builtin [name].
- It only supports the following cases for the time being:
- A: [\builtin(ptr+r)] where [ptr] 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 encounters 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 p call_default =
- if Misc.is_bitfield_pointers t.term_type then
- Error.not_yet "bitfield pointer";
- match t.term_node with
- | TBinOp((PlusPI | IndexPI), ptr, ({ term_node = Trange _ } as r)) ->
- if Misc.is_set_of_ptr_or_array ptr.term_type then
- Error.not_yet "arithmetic over set of pointers or arrays"
- else
- (* Case A *)
- call_memory_block ~loc kf name ctx env ptr r p
- | 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 ptr = Logic_const.taddrof ~loc (TVar lv, TNoOffset) lty_noset in
- call_memory_block ~loc kf name ctx env ptr r p
- | 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;
- !predicate_to_exp_ref 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
+(* [fname_to_pred name args] returns the memory predicate corresponding to
+ [name] with the given [args]. *)
+let fname_to_pred ?loc name args =
+ match name, args with
+ | "dangling", [ t ] ->
+ Logic_const.pdangling ?loc (Logic_const.here_label, t)
+ | "valid", [ t ] ->
+ Logic_const.pvalid ?loc (Logic_const.here_label, t)
+ | "valid_read", [ t ] ->
+ Logic_const.pvalid_read ?loc (Logic_const.here_label, t)
+ | "separated", args ->
+ Logic_const.pseparated ?loc args
+ | "initialized", [ t ] ->
+ Logic_const.pinitialized ?loc (Logic_const.here_label, t)
+ | "dangling", _ | "valid", _ | "valid_read", _ | "initialized", _ ->
+ Options.fatal
+ "Mismatch between the function name ('%s') and the number of parameters \
+ (%d)"
+ name
+ (List.length args)
| _ ->
- (* Case C *)
- call_default ~loc kf name ctx env t
+ Options.fatal "Unsupported function '%s'" name
+
+(* [extract_quantifiers ~loc args] iterates over each argument in [args] and if
+ that argument contains a non-explicit range, tries to extract a universal
+ quantifier representing the range and returns an updated argument for this
+ quantifier.
+
+ The cases in the function comments correspond to the cases described in
+ [call_with_tset]. *)
+let extract_quantifiers ~loc args =
+ let args = List.rev args in
+ List.fold_left
+ (fun (args, quantifiers) arg ->
+ let arg, quantifiers =
+ match arg.term_node with
+ | TAddrOf(TVar _, TIndex({ term_node = Trange _ }, TNoOffset)) ->
+ (* Case A: explicit range *)
+ arg, quantifiers
+ | TAddrOf(TVar ({ lv_type = Ctype (TArray _) } as lv), toffset) ->
+ if has_set_as_index toffset then
+ (* Case B: non-explicit range, try to extract quantifiers with
+ range elimination. *)
+ try
+ let toffset', quantifiers' =
+ eliminate_ranges_from_index_of_toffset ~loc toffset quantifiers
+ in
+ let lty_noset =
+ if Logic_const.is_set_type arg.term_type then
+ Logic_const.type_of_element arg.term_type
+ else
+ arg.term_type
+ in
+ let arg' =
+ Logic_const.taddrof ~loc (TVar lv, toffset') lty_noset
+ in
+ arg', quantifiers'
+ with Range_elimination_exception ->
+ (* Case C: range elimination failed *)
+ arg, quantifiers
+ else
+ (* Case C: no range in the offsets *)
+ arg, quantifiers
+ | _ ->
+ (* Case A or C: either explicit range or no range. *)
+ arg, quantifiers
+ in
+ (arg :: args, quantifiers)
+ )
+ ([], [])
+ args
+
-(* \initialized *)
-let call_with_size ~loc kf name ctx env t p =
- 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 ty = Misc.cty t.term_type in
- let sizeof = Misc.mk_ptr_sizeof ty loc in
- Env.rtl_call_to_new_var
+(* [call_with_tset
~loc
- ~name
- env
+ ~arg_from_range
+ ~arg_from_term
+ ~prepend_n_args
kf
- None
- ctx
name
- [ e; sizeof ]
+ ctx
+ env
+ args
+ p]
+ creates a call to the E-ACSL memory builtin identified by [name] with the
+ given tset [args].
+
+ [arg_from_range ~loc kf env rev_args ptr r p] is a function that converts an
+ argument of the form [ptr + r] where [ptr] is an address and [r] a range into
+ a list of arguments that can be passed to a built-in function and add them in
+ reverse order to the [rev_args] parameter list. For instance for the built-in
+ [\initialized(ptr + r)], [ptr + r] will be turned into [[ptr'; size]] where
+ [ptr'] is the address of the start of the range and [size] is the size of the
+ range, and will be returned as [size :: ptr' :: rev_args].
+
+ [arg_from_term ~loc kf env rev_args t p] is a function that converts a term
+ without range argument [t] into a list of arguments that can be passed to a
+ built-in function and add them in reverse order to the [rev_args] parameter
+ list. For instance for the built-in [\valid(t)], [t] will be turned into
+ [[e; size; base; base_addr]] where [e] is the value representing [t], [size]
+ is the size of the memory under study, [base] is the value [ptr] if [t] can
+ be represented by the expression [ptr + i], and [base_addr] if the value
+ [&ptr] if [t] can be represented by the expression [ptr + i]. They will be
+ returned as [base_addr :: base :: size :: e :: rev_args].
+
+ If [prepend_n_args], then the number of arguments in args is prepended to the
+ list of arguments given to the builtin.
+
+ Since each argument in [args] is a tset, it can contains ranges. For now,
+ only the following cases are supported:
+ A: [\builtin(ptr+r)] where [ptr] 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 [arg_from_term] which performs the translation for
+ range free terms, and raises Not_yet if it ever encounters 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_tset ~loc ~arg_from_range ~arg_from_term ?(prepend_n_args=false) kf name ctx env args p =
+ let args, quantifiers = extract_quantifiers ~loc args in
+ match quantifiers with
+ | _ :: _ ->
+ (* Some quantifiers have been extracted from the arguments, we need to build
+ a new predicate with these quantifiers and the updated arguments. *)
+ let p_quantified = fname_to_pred ~loc name args 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
+ (* There's no more quantifiers in the arguments now, we can call back
+ [prediate_to_exp] to translate the predicate as usual *)
+ Typing.type_named_predicate ~must_clear:true p_quantified;
+ !predicate_to_exp_ref kf env p_quantified
+ | [] ->
+ (* No arguments require quantifiers, so we can directly translate the
+ predicate *)
+ let n_args, rev_args, env =
+ List.fold_left
+ (fun (n_args, rev_args, env) t ->
+ let rev_args, env =
+ if Misc.is_bitfield_pointers t.term_type then
+ Error.not_yet "bitfield pointer";
+ match t.term_node with
+ | TBinOp((PlusPI | IndexPI),
+ ptr,
+ ({ term_node = Trange _ } as r)) ->
+ if Misc.is_set_of_ptr_or_array ptr.term_type then
+ Error.not_yet
+ "arithmetic over set of pointers or arrays"
+ else
+ (* Case A *)
+ arg_from_range ~loc kf env rev_args ptr r p
+ | 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 ptr =
+ Logic_const.taddrof ~loc (TVar lv, TNoOffset) lty_noset
+ in
+ arg_from_range ~loc kf env rev_args ptr r p
+ | _ ->
+ (* Case A, B with failed range elimination or C *)
+ arg_from_term ~loc kf env rev_args t p
+ in
+ let n_args = n_args + 1 in
+ n_args, rev_args, env
+ )
+ (0, [], env)
+ args
+ in
+ (* The arguments were built in reverse, reorder them *)
+ let args = List.rev rev_args in
+ let args =
+ if prepend_n_args then
+ Cil.integer ~loc n_args :: args
+ else
+ args
+ in
+ let _, e, env =
+ Env.new_var
+ ~loc
+ ~name
+ env
+ kf
+ None
+ ctx
+ (fun v _ -> [
+ Smart_stmt.rtl_call ~loc ~result:(Cil.var v) name args
+ ])
+ in
+ e, env
+
+(* \initialized and \separated *)
+let call_with_size ~loc kf name ctx env args p =
+ assert (name = "initialized" || name = "separated");
+ let arg_from_term ~loc kf env rev_args t _p =
+ let ptr, size, env = term_to_ptr_and_size ~loc kf env t in
+ size :: ptr :: rev_args, env
in
- call_with_ranges
+ let arg_from_range ~loc kf env rev_args ptr r p =
+ let ptr, size, env = range_to_ptr_and_size ~loc kf env ptr r p in
+ size :: ptr :: rev_args, env
+ in
+ let prepend_n_args = Datatype.String.equal name "separated" in
+ call_with_tset
~loc
+ ~arg_from_term
+ ~arg_from_range
+ ~prepend_n_args
kf
name
ctx
env
- t
+ args
p
- call_for_unsupported_constructs
(* \valid and \valid_read *)
let call_valid ~loc kf name ctx env t p =
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 ty = Misc.cty t.term_type in
- let sizeof = Misc.mk_ptr_sizeof ty loc in
- let args = [ e; sizeof; base; base_addr ] in
- Env.rtl_call_to_new_var
- ~loc
- ~name
- env
- kf
- None
- ctx
- name
- args
+ let arg_from_term ~loc kf env rev_args t _p =
+ let ptr, size, env = term_to_ptr_and_size ~loc kf env t in
+ let base, base_addr = exp_to_base_and_baseaddr ~loc ptr in
+ base_addr :: base :: size :: ptr :: rev_args, env
+ in
+ let arg_from_range ~loc kf env rev_args ptr r p =
+ let ptr, size, env = range_to_ptr_and_size ~loc kf env ptr r p in
+ let base, base_addr = exp_to_base_and_baseaddr ~loc ptr in
+ base_addr :: base :: size :: ptr :: rev_args, env
in
- call_with_ranges
+ let prepend_n_args = false in
+ call_with_tset
~loc
+ ~arg_from_term
+ ~arg_from_range
+ ~prepend_n_args
kf
name
ctx
env
- t
+ [ t ]
p
- call_for_unsupported_constructs
-
-(* \separated *)
-let call_separated ~loc kf ctx env tlist p =
- let term_to_ptr_and_size kf 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 ty = Misc.cty t.term_type in
- let sizeof = Misc.mk_ptr_sizeof ty loc in
- e, sizeof, env
- in
- let n_args, args, env =
- List.fold_left
- (fun (n_args, args, env) t ->
- let ptr, size, env =
- if Misc.is_bitfield_pointers t.term_type then
- Error.not_yet "bitfield pointer in \\separated";
- match t.term_node with
- | TBinOp((PlusPI | IndexPI),
- ptr,
- ({ term_node = Trange _ } as r)) ->
- if Misc.is_set_of_ptr_or_array ptr.term_type then
- Error.not_yet
- "arithmetic over set of pointers or arrays in \\separated"
- else
- range_to_ptr_and_size ~loc kf env ptr r p
- | 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 ptr =
- Logic_const.taddrof ~loc (TVar lv, TNoOffset) lty_noset
- in
- range_to_ptr_and_size ~loc kf env ptr r p
- | TAddrOf(TVar ({ lv_type = Ctype (TArray _) } as _lv), toffset) ->
- if has_set_as_index toffset then
- Error.not_yet "range elimination for \\separated"
- else
- term_to_ptr_and_size kf env t
- | _ ->
- term_to_ptr_and_size kf env t
- in
- let ptr = Cil.mkCast ~force:false ~e:ptr ~newt:Cil.voidPtrType in
- let n_args = n_args + 1 in
- let args = ptr :: size :: args in
- n_args, args, env
- )
- (0, [], env)
- tlist
- in
- let args = (Cil.integer ~loc n_args) :: args in
- let _, e, env =
- Env.new_var
- ~loc
- ~name:"separated"
- env
- kf
- None
- ctx
- (fun v _ -> [
- Constructor.mk_rtl_call ~loc ~result:(Cil.var v) "separated" args
- ])
- in
- e, env
-
-(*
-Local Variables:
-compile-command: "make -C ../.."
-End:
-*)
diff --git a/src/plugins/e-acsl/src/code_generator/memory_translate.mli b/src/plugins/e-acsl/src/code_generator/memory_translate.mli
index 8cf471dea9b..dd64b8322e3 100644
--- a/src/plugins/e-acsl/src/code_generator/memory_translate.mli
+++ b/src/plugins/e-acsl/src/code_generator/memory_translate.mli
@@ -34,13 +34,13 @@ val call:
[base_addr], [block_length], [offset] and [freeable]. *)
val call_with_size:
- loc:location -> kernel_function -> string -> typ -> Env.t -> term ->
+ loc:location -> kernel_function -> string -> typ -> Env.t -> term list ->
predicate -> exp * Env.t
-(* [call_with_size ~loc kf name ctx env t p] 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.
+(* [call_with_size ~loc kf name ctx env tlist p] creates a call to the E-ACSL
+ memory built-in identified by [name] which requires two arguments per term,
+ namely the pointer under study and a size in bytes.
+ The supported built-ins are: [initialized] and [separated].
+ Each term in [tlist] can denote ranges of memory locations.
[p] is the predicate under testing. *)
val call_valid:
@@ -51,14 +51,6 @@ val call_valid:
[t] can denote ranges of memory locations.
[p] is the predicate under testing. *)
-val call_separated:
- loc:location -> kernel_function -> typ -> Env.t -> term list -> predicate ->
- exp * Env.t
-(* [call_separated ~loc kf ctx env tlist p] creates a call to the E-ACSL memory
- builtin [separated].
- Each [term] in [tlist] can denote ranges of memory locations.
- [p] is the predicate under testing. *)
-
(**************************************************************************)
(********************** Forward references ********************************)
(**************************************************************************)
diff --git a/src/plugins/e-acsl/src/code_generator/translate.ml b/src/plugins/e-acsl/src/code_generator/translate.ml
index 9ecf3c89082..860c165a18a 100644
--- a/src/plugins/e-acsl/src/code_generator/translate.ml
+++ b/src/plugins/e-acsl/src/code_generator/translate.ml
@@ -1008,7 +1008,7 @@ and predicate_content_to_exp ?name kf env p =
env
tlist
in
- Memory_translate.call_separated ~loc kf Cil.intType env tlist p
+ Memory_translate.call_with_size ~loc kf "separated" Cil.intType env tlist p
| Pinitialized(BuiltinLabel Here, t) ->
(match t.term_node with
(* optimisation when we know that the initialisation is ok *)
@@ -1024,7 +1024,7 @@ and predicate_content_to_exp ?name kf env p =
"initialized"
Cil.intType
env
- t
+ [ t ]
p)
| Pinitialized _ -> Env.not_yet env "labeled \\initialized"
| Pallocable _ -> Env.not_yet env "\\allocate"
--
GitLab