diff --git a/src/plugins/eva/Eva.mli b/src/plugins/eva/Eva.mli
index 9a535134ce61730528cc9ed81d7eb2c3fe3c5af9..0adbbd5ebd2178991f430073708a86c7c5f6503d 100644
--- a/src/plugins/eva/Eva.mli
+++ b/src/plugins/eva/Eva.mli
@@ -685,6 +685,18 @@ module Logic_inout: sig
result: Cil_types.varinfo option ->
Cvalue.Model.t -> Cil_types.assigns -> Locations.Zone.t
+ (** Zones of an lvalue term of an assigns clause. *)
+ type tlval_zones = {
+ under: Locations.Zone.t; (** Under-approximation of the memory zone. *)
+ over: Locations.Zone.t; (** Over-approximation of the memory zone. *)
+ deps: Locations.Zone.t; (** Dependencies needed to evaluate the address. *)
+ }
+
+ (** Evaluation of the memory zones and dependencies of an lvalue term from an
+ assigns clause, in the given cvalue state for a read or write access. *)
+ val assigns_tlval_to_zones:
+ Cvalue.Model.t -> Locations.access -> Cil_types.term -> tlval_zones option
+
(** Evaluate the assigns clauses of the given function in its given pre-state,
and compare them with the given froms (computed by the from plugin).
Emits warnings if needed, and sets statuses to the assigns clauses. *)
diff --git a/src/plugins/eva/legacy/eval_terms.ml b/src/plugins/eva/legacy/eval_terms.ml
index 344e7cd9f1a3e3992df5b7fd571a8cbd5f0ce4a9..ce12bb0f25478cd2cd9a23dbb6344017e4d4679c 100644
--- a/src/plugins/eva/legacy/eval_terms.ml
+++ b/src/plugins/eva/legacy/eval_terms.ml
@@ -2773,6 +2773,9 @@ let eval_tlval_as_zone ~alarm_mode access env t =
in
over
+let tlval_deps env t = (eval_term_as_lval ~alarm_mode:Ignore env t).ldeps
+
+
let () =
(* TODO: deprecate loc_to_loc, move loc_to_locs into Value *)
Db.Properties.Interp.loc_to_loc :=
diff --git a/src/plugins/eva/legacy/eval_terms.mli b/src/plugins/eva/legacy/eval_terms.mli
index a8b326ffc3dbb4651441e06591a75a501a4b3130..ff51402c4982af6c308f8e68c4a12a71f48cd19f 100644
--- a/src/plugins/eva/legacy/eval_terms.mli
+++ b/src/plugins/eva/legacy/eval_terms.mli
@@ -116,5 +116,11 @@ val eval_predicate :
Returns None on either an evaluation error or on unsupported construct. *)
val predicate_deps: eval_env -> Cil_types.predicate -> logic_deps option
+(** [tlval_deps env t] computes the logic dependencies needed to evaluate the
+ address of lvalue term [t] in the given evaluation environment [env].
+ @raises LogicEvalError on evaluation errors, unsupported constructs, or
+ if [t] is not an lvalue term. *)
+val tlval_deps: eval_env -> Cil_types.term -> logic_deps
+
val reduce_by_predicate :
eval_env -> bool -> predicate -> eval_env
diff --git a/src/plugins/eva/legacy/logic_inout.ml b/src/plugins/eva/legacy/logic_inout.ml
index a505839980c5e4433fe373fec607fa6fab6682bf..e4b4c543a701109dc90c688a4f202ce58c430887 100644
--- a/src/plugins/eva/legacy/logic_inout.ml
+++ b/src/plugins/eva/legacy/logic_inout.ml
@@ -100,6 +100,24 @@ let assigns_outputs_to_zone ~result state assigns =
| WritesAny -> Locations.Zone.top
| Writes l -> List.fold_left treat_asgn Locations.Zone.bottom l
+type tlval_zones = {
+ under: Locations.Zone.t;
+ over: Locations.Zone.t;
+ deps: Locations.Zone.t;
+}
+
+let assigns_tlval_to_zones state access tlval =
+ let env = Eval_terms.env_post_f ~pre:state ~post:state ~result:None () in
+ let alarm_mode = Eval_terms.Ignore in
+ try
+ let under, over =
+ Eval_terms.eval_tlval_as_zone_under_over ~alarm_mode access env tlval
+ in
+ let deps = join_logic_deps (Eval_terms.tlval_deps env tlval) in
+ Some { under; over; deps; }
+ with Eval_terms.LogicEvalError _ -> None
+
+
(* -------------------------------------------------------------------------- *)
(* --- Verify assigns clauses --- *)
(* -------------------------------------------------------------------------- *)
diff --git a/src/plugins/eva/legacy/logic_inout.mli b/src/plugins/eva/legacy/logic_inout.mli
index 92d6afd81687589a37b2bfbdcadea6bfe67a6cba..7e478d9b4c5cada150d08b830a78cdd701c3e283 100644
--- a/src/plugins/eva/legacy/logic_inout.mli
+++ b/src/plugins/eva/legacy/logic_inout.mli
@@ -50,6 +50,18 @@ val assigns_outputs_to_zone:
result: Cil_types.varinfo option ->
Cvalue.Model.t -> Cil_types.assigns -> Locations.Zone.t
+(** Zones of an lvalue term of an assigns clause. *)
+type tlval_zones = {
+ under: Locations.Zone.t; (** Under-approximation of the memory zone. *)
+ over: Locations.Zone.t; (** Over-approximation of the memory zone. *)
+ deps: Locations.Zone.t; (** Dependencies needed to evaluate the address. *)
+}
+
+(** Evaluation of the memory zones and dependencies of an lvalue term from an
+ assigns clause, in the given cvalue state for a read or write access. *)
+val assigns_tlval_to_zones:
+ Cvalue.Model.t -> Locations.access -> Cil_types.term -> tlval_zones option
+
(** Evaluate the assigns clauses of the given function in its given pre-state,
and compare them with the given froms (computed by the from plugin).
Emits warnings if needed, and sets statuses to the assigns clauses. *)
diff --git a/src/plugins/from/from_compute.ml b/src/plugins/from/from_compute.ml
index 76b7fa9c5d6a08bcc0c6ca452460187c0e9ca830..0805d3aef48555180c59ab2099575d29c51bb89d 100644
--- a/src/plugins/from/from_compute.ml
+++ b/src/plugins/from/from_compute.ml
@@ -52,23 +52,24 @@ let compute_using_prototype_for_state state kf assigns =
Eva.Logic_inout.assigns_inputs_to_zone state (Writes [out, ins])
in
let treat_assign acc (out, ins) =
- try
- let (output_loc_under, output_loc_over, _deps) =
- !Db.Properties.Interp.loc_to_loc_under_over
- ~result:None state out.it_content
- in
+ let output =
+ Eva.Logic_inout.assigns_tlval_to_zones state Write out.it_content
+ in
+ match output with
+ | None ->
+ From_parameters.result
+ ~once:true ~current:true "Unable to extract assigns in %a"
+ Kernel_function.pretty kf;
+ acc
+ | Some output ->
let input_zone = input_zone out ins in
(* assign clauses do not let us specify address
dependencies for now, so we assume it is all data
dependencies *)
- let input_deps =
- Function_Froms.Deps.from_data_deps input_zone
- in
+ let input_deps = Function_Froms.Deps.from_data_deps input_zone in
(* Weak update of the over-approximation of the zones assigned *)
- let acc = Function_Froms.Memory.add_binding_loc ~exact:false
- acc output_loc_over input_deps in
- let output_loc_under_zone = Locations.enumerate_valid_bits_under
- Write output_loc_under in
+ let acc = Function_Froms.Memory.add_binding ~exact:false
+ acc output.over input_deps in
(* Now, perform a strong update on the zones that are guaranteed
to be assigned (under-approximation) AND that do not depend
on themselves.
@@ -78,16 +79,12 @@ let compute_using_prototype_for_state state kf assigns =
zones is an exact operation. *)
let sure_out_zone =
Zone.(if equal top input_zone then bottom
- else diff output_loc_under_zone input_zone)
+ else diff output.under input_zone)
in
let acc = Function_Froms.Memory.add_binding ~exact:true
acc sure_out_zone input_deps in
acc
- with Db.Properties.Interp.No_conversion ->
- From_parameters.result
- ~once:true ~current:true "Unable to extract assigns in %a"
- Kernel_function.pretty kf;
- acc
+
in
let treat_ret_assign acc (out, from) =
let zone_from = input_zone out from in
diff --git a/src/plugins/inout/operational_inputs.ml b/src/plugins/inout/operational_inputs.ml
index 4e5041fc2fd00a15e9b6b265ba1d49571a28a87e..b7ce487c06545613a0caf8f58480220e18ce2d5c 100644
--- a/src/plugins/inout/operational_inputs.ml
+++ b/src/plugins/inout/operational_inputs.ml
@@ -121,41 +121,35 @@ let eval_assigns kf state assigns =
in
let out_term = out.it_content in
let outputs_under, outputs_over, deps =
- try
- if Logic_const.(is_result out_term || is_exit_status out_term)
- then (Zone.bottom, Zone.bottom, Zone.bottom)
- else
- let loc_out_under, loc_out_over, deps =
- !Db.Properties.Interp.loc_to_loc_under_over ~result:None state out_term
- in
- (enumerate_valid_bits_under Write loc_out_under,
- enumerate_valid_bits Write loc_out_over,
- clean_deps deps)
- with Db.Properties.Interp.No_conversion ->
- Inout_parameters.warning ~current:true ~once:true
- "failed to interpret assigns clause '%a'" Printer.pp_term out_term;
- (Zone.bottom, Zone.top, Zone.top)
+ if Logic_const.(is_result out_term || is_exit_status out_term)
+ then (Zone.bottom, Zone.bottom, Zone.bottom)
+ else
+ let output = Eva.Logic_inout.assigns_tlval_to_zones state Write out_term in
+ match output with
+ | Some output -> output.under, output.over, clean_deps output.deps
+ | None ->
+ Inout_parameters.warning ~current:true ~once:true
+ "failed to interpret assigns clause '%a'" Printer.pp_term out_term;
+ (Zone.bottom, Zone.top, Zone.top)
in
(* Compute all inputs as a zone *)
let inputs =
- try
- match froms with
- | FromAny -> Zone.top
- | From l ->
- let aux acc { it_content = from } =
- let _, loc, deps =
- !Db.Properties.Interp.loc_to_loc_under_over ~result:None state from
- in
- let acc = Zone.join (clean_deps deps) acc in
- let z = enumerate_valid_bits Read loc in
- Zone.join z acc
- in
- List.fold_left aux deps l
- with Db.Properties.Interp.No_conversion ->
- Inout_parameters.warning ~current:true ~once:true
- "failed to interpret inputs in assigns clause '%a'"
- Printer.pp_from asgn;
- Zone.top
+ match froms with
+ | FromAny -> Zone.top
+ | From l ->
+ let aux acc { it_content = from } =
+ let inputs = Eva.Logic_inout.assigns_tlval_to_zones state Read from in
+ match inputs with
+ | Some inputs ->
+ let acc = Zone.join (clean_deps inputs.deps) acc in
+ Zone.join inputs.over acc
+ | _ ->
+ Inout_parameters.warning ~current:true ~once:true
+ "failed to interpret inputs in assigns clause '%a'"
+ Printer.pp_from asgn;
+ Zone.top
+ in
+ List.fold_left aux deps l
in
(* Fuse all outputs. An output is sure if it was certainly
overwritten (i.e. is in the left part of an assign clause,
diff --git a/tests/builtins/oracle/imprecise.res.oracle b/tests/builtins/oracle/imprecise.res.oracle
index aac1b7410d2177b68888a0a52de635a1bc3bc49b..c2c904747084df4152760b9eb433b5cb05ddcd3b 100644
--- a/tests/builtins/oracle/imprecise.res.oracle
+++ b/tests/builtins/oracle/imprecise.res.oracle
@@ -365,7 +365,7 @@
[from] Function cast_address:
NO EFFECTS
[from] Function f:
- NULL[100..200] FROM \nothing (and SELF)
+ NO EFFECTS
[from] Function gm_f1:
\result FROM \nothing
[from] Function gm_f2:
@@ -375,7 +375,7 @@
NULL[100..200] FROM NULL[100..200] (and SELF)
p_gm_null FROM \nothing
[from] Function invalid_assigns_imprecise:
- NULL[100..200] FROM \nothing (and SELF)
+ NO EFFECTS
[from] Function many_writes:
NO EFFECTS
[from] Function memset:
@@ -414,7 +414,7 @@
[from] call to Frama_C_dump_each at imprecise.c:78 (by garbled_mix_null):
\result FROM \nothing
[from] call to f at imprecise.c:11 (by invalid_assigns_imprecise):
- NULL[100..200] FROM \nothing (and SELF)
+ NO EFFECTS
[from] call to memset at imprecise.c:51 (by abstract_structs):
v3.[bits 0 to ..] FROM c (and SELF)
\result FROM s
@@ -424,7 +424,7 @@
[from] call to Frama_C_dump_each at imprecise.c:21 (by write_garbled):
\result FROM \nothing
[from] call to invalid_assigns_imprecise at imprecise.c:144 (by main):
- NULL[100..200] FROM \nothing (and SELF)
+ NO EFFECTS
[from] call to write_garbled at imprecise.c:145 (by main):
NULL[100..200] FROM \nothing (and SELF)
[from] call to abstract_structs at imprecise.c:146 (by main):
@@ -902,7 +902,7 @@
[from] Function cast_address:
NO EFFECTS
[from] Function f:
- NULL[100..200] FROM \nothing (and SELF)
+ NO EFFECTS
[from] Function gm_f1:
\result FROM \nothing
[from] Function gm_f2:
@@ -912,7 +912,7 @@
NULL[100..200] FROM NULL[100..200] (and SELF)
p_gm_null FROM \nothing
[from] Function invalid_assigns_imprecise:
- NULL[100..200] FROM \nothing (and SELF)
+ NO EFFECTS
[from] Function many_writes:
NO EFFECTS
[from] Function memset:
@@ -951,7 +951,7 @@
[from] call to Frama_C_dump_each at imprecise.c:78 (by garbled_mix_null):
\result FROM \nothing
[from] call to f at imprecise.c:11 (by invalid_assigns_imprecise):
- NULL[100..200] FROM \nothing (and SELF)
+ NO EFFECTS
[from] call to memset at imprecise.c:51 (by abstract_structs):
v3.[bits 0 to ..] FROM c (and SELF)
\result FROM s
@@ -961,7 +961,7 @@
[from] call to Frama_C_dump_each at imprecise.c:21 (by write_garbled):
\result FROM \nothing
[from] call to invalid_assigns_imprecise at imprecise.c:144 (by main):
- NULL[100..200] FROM \nothing (and SELF)
+ NO EFFECTS
[from] call to write_garbled at imprecise.c:145 (by main):
NULL[100..200] FROM \nothing (and SELF)
[from] call to abstract_structs at imprecise.c:146 (by main):
diff --git a/tests/value/oracle/assigns.res.oracle b/tests/value/oracle/assigns.res.oracle
index 1bdb53cd80638ca67a3459df8cda1068e0b917d8..a845b332c3d8c1a328e54a8b64e3e814a4d309b0 100644
--- a/tests/value/oracle/assigns.res.oracle
+++ b/tests/value/oracle/assigns.res.oracle
@@ -626,12 +626,8 @@
[from] Done for function main2
[from] Computing for function main4
[from] Computing for function f_main4_1 <-main4
-[kernel] assigns.i:104:
- more than 200(1000) dependencies to update. Approximating.
[from] Done for function f_main4_1
[from] Computing for function f_main4_2 <-main4
-[kernel] assigns.i:105:
- more than 200(1000) dependencies to update. Approximating.
[from] Done for function f_main4_2
[from] Done for function main4
[from] Computing for function main