From be0cc43cb890369c63ca0bc0fc704c2f9aea25a1 Mon Sep 17 00:00:00 2001
From: Fonenantsoa Maurica <maurica.fonenantsoa@gmail.com>
Date: Tue, 18 Sep 2018 10:40:30 +0200
Subject: [PATCH] Addresses Julien's review no.3: - No superfluous patterns
- Using Cil.charPtrType - call_for_unsupported_constructs as closure given
to mmodel_call_with_ranges - Style: - Indendation - No superfluous
begin..end - Parentheses - Spaces
---
src/plugins/e-acsl/translate.ml | 112 +++++++++++++++-----------------
1 file changed, 51 insertions(+), 61 deletions(-)
diff --git a/src/plugins/e-acsl/translate.ml b/src/plugins/e-acsl/translate.ml
index ad972d9e986..fa284c4c66f 100644
--- a/src/plugins/e-acsl/translate.ml
+++ b/src/plugins/e-acsl/translate.ml
@@ -79,10 +79,6 @@ let eliminate_ranges_from_index_of_term ~loc t =
let lv = Cil_const.make_logic_var_kind name LVQuant Linteger in
let tlv = Logic_const.tvar ~loc lv in
tlv, (n1, lv, n2)
- | TBinOp(PlusA, _, {term_node = Trange _}) ->
- (* t[n + (0..3)] results in a typing error:
- arithmetic conversion between non arithmetic types int and set<ℤ> *)
- assert false
| _ ->
raise Range_elimination_exception
@@ -92,13 +88,6 @@ let eliminate_ranges_from_index_of_term ~loc t =
if we don't support the construction yet. *)
let rec eliminate_ranges_from_index_of_toffset ~loc toffset quantifiers =
match toffset with
- | TIndex(t, TNoOffset) ->
- if Misc.is_range_free t then
- toffset, quantifiers
- else
- (* Attempt Range Elimination on [t] *)
- let t', q = eliminate_ranges_from_index_of_term ~loc t in
- TIndex(t', TNoOffset), q :: quantifiers
| TIndex(t, toffset') ->
if Misc.is_range_free t then
let toffset', quantifiers' =
@@ -668,8 +657,7 @@ and mk_ptr_sizeof typ loc =
(* \valid, \offset and \initialized annotations *)
and mmodel_call_with_size ~loc kf name ctx env t =
- mmodel_call_with_ranges ~loc kf name ctx env t
- begin fun ~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
@@ -685,16 +673,17 @@ and mmodel_call_with_size ~loc kf name ctx env t =
[ Misc.mk_call ~loc ~result:(Cil.var v) fname [ e; sizeof ] ])
in
res, env
- end
+ 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 =
- mmodel_call_with_ranges ~loc kf name ctx env t
- begin fun ~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
+ | Lval lv | StartOf lv -> Cil.mkAddrOrStartOf ~loc lv
| _ -> assert false
in
let _, res, env =
@@ -712,7 +701,9 @@ and mmodel_call_valid ~loc kf name ctx env t =
[ Misc.mk_call ~loc ~result:(Cil.var v) fname args ])
in
res, env
- end
+ 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:
@@ -735,7 +726,7 @@ and mmodel_call_valid ~loc kf name ctx env t =
NON-contiguous locations -> multiple calls (3) to [__e_acsl_valid] *)
and mmodel_call_with_ranges ~loc kf name ctx env t mmodel_call_default =
match t.term_node with
- | TBinOp((PlusPI | IndexPI), p, ({term_node = Trange _} as r)) ->
+ | 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
@@ -747,48 +738,47 @@ and mmodel_call_with_ranges ~loc kf name ctx env t mmodel_call_default =
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) ->
+ | TAddrOf(TVar ({ lv_type = Ctype (TArray _) } as lv), toffset) ->
if has_set_as_index toffset then
- (* Case B *)
- begin 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"
+ (* Case B *)
+ try
+ let toffset', quantifiers =
+ eliminate_ranges_from_index_of_toffset ~loc toffset []
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
- end
+ 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
@@ -815,7 +805,7 @@ and mmodel_call_memory_block ~loc kf name ctx env p r =
in
let s = Logic_const.term ~loc (TSizeOf ty) Linteger in
(* ptr *)
- let typ_charptr = TPtr(TInt(IChar, []), []) in
+ let typ_charptr = Cil.charPtrType in
let ptr = Logic_const.term
~loc
(TBinOp(
@@ -845,7 +835,7 @@ and mmodel_call_memory_block ~loc kf name ctx env p r =
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
+ | Lval lv | StartOf lv -> Cil.mkAddrOrStartOf ~loc lv
| _ -> assert false
in
(* generating env *)
--
GitLab