From d6245ae13831a3b5090925d54a4268ed8c26d5df Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?David=20B=C3=BChler?= <david.buhler@cea.fr>
Date: Fri, 13 May 2022 15:53:02 +0200
Subject: [PATCH] [Eva] Fixes the evaluation engine when a domain oracle
returns Bottom.
When the evaluation of any subexpression leads to Bottom, the evaluation of the
complete expression returns only Bottom with no valuation: thus the valuation
cache is no longer updated.
However, when the evaluation of another expression requested by a domain through
the oracle leads to Bottom, the evaluation of the primary expression may
continue without leading to Bottom (domains are allowed to request the evaluation
of 1/0 at any time, after all).
In this case, we should properly update the cached valuation by binding Bottom
to the expression requested by the domain, in case it should be used again in
the evaluation (for instance if the requested evaluation was a subexpression of
the primary target of the evaluation).
And especially, if subdivided evaluations are enabled, the reference to the
cached valuation must _always_ be reset after the oracle (even when it returns
Bottom), as the cache has been used for successive evaluations with various
hypotheses, and the last one is probably not sound in the general case.
---
src/plugins/value/engine/evaluation.ml | 44 +++++++++++++++++---------
1 file changed, 29 insertions(+), 15 deletions(-)
diff --git a/src/plugins/value/engine/evaluation.ml b/src/plugins/value/engine/evaluation.ml
index 10974ea5bb1..2a7beccec65 100644
--- a/src/plugins/value/engine/evaluation.ml
+++ b/src/plugins/value/engine/evaluation.ml
@@ -114,10 +114,6 @@ type loc_report = {
propagated backward, and that the expression cannot be volatile. *)
let extern_report = { fuel = Infty; reduction = Neither; volatile = false }
-(* Report used when the cache is filled with a dummy value to avoid evaluation
- loops. *)
-let dummy_report = { fuel = Loop; reduction = Neither; volatile = false }
-
let no_fuel = -1
let root_fuel () = Parameters.OracleDepth.get ()
let backward_fuel () = Parameters.ReductionDepth.get ()
@@ -343,12 +339,19 @@ module Make
(* Was the fuel entirely consumed? *)
let fuel_consumed = ref false
- let top_record =
- let flagged_top =
- { v = `Value Value.top; initialized = false; escaping = true }
- in
- { value = flagged_top; origin = None;
- reductness = Dull; val_alarms = Alarmset.all }
+ let bottom_entry val_alarms =
+ let value = { v = `Bottom; initialized = true; escaping = false } in
+ let record = { value; origin = None; reductness = Dull; val_alarms } in
+ let report = { fuel = Infty; reduction = Neither; volatile = false} in
+ record, report
+
+ let top_entry =
+ let v = `Value Value.top in
+ let value = { v; initialized = false; escaping = true } in
+ let val_alarms = Alarmset.all in
+ let record = { value; origin = None; reductness = Dull; val_alarms } in
+ let report = { fuel = Loop; reduction = Neither; volatile = false } in
+ record, report
(* Updates the abstractions stored in the cache for the expression [expr]
with the given record, report and value. [kind] is the type of the
@@ -805,7 +808,7 @@ module Make
(* Fuel not consumed for this new evaluation. *)
fuel_consumed := false;
(* Fill the cache to avoid loops in the use of the oracle. *)
- cache := Cache.add' !cache expr (top_record, dummy_report);
+ cache := Cache.add' !cache expr top_entry;
(* Evaluation of [expr]. *)
let result, alarms = coop_forward_eval context expr in
let value =
@@ -1129,10 +1132,21 @@ module Make
let valuation = !cache in
let context = { context with remaining_fuel } in
let subdivnb = context.subdivision in
- Subdivided_Evaluation.evaluate context valuation ~subdivnb expr
- >>=: fun (valuation, value) ->
- cache := valuation;
- value
+ let eval, alarms =
+ Subdivided_Evaluation.evaluate context valuation ~subdivnb expr
+ in
+ (* Always reset the reference to the cached valuation after a subdivided
+ evaluation (as the multiple evaluations modify the cache). *)
+ match eval with
+ | `Bottom ->
+ (* The evaluation of the expression requested by a domain returns
+ Bottom, but the evaluation of the primary expression may continue.
+ Thus bind Bottom to [expr] in the valuation. *)
+ cache := Cache.add' valuation expr (bottom_entry alarms);
+ `Bottom, alarms
+ | `Value (valuation, value) ->
+ cache := valuation;
+ `Value value, alarms
else
fun _ -> fuel_consumed := true; `Value Value.top, Alarmset.all
--
GitLab