From a81dea06e2f026296df7b045a971fb9f0b287933 Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?David=20B=C3=BChler?= <david.buhler@cea.fr>
Date: Mon, 15 Jul 2019 13:32:48 +0200
Subject: [PATCH] [Eva] Subdivided_evaluation takes the max number of
subdivisions as argument.
The maximal number of subdivisions is a new field of the context record for the
forward evaluation functions, as it is also used when calling the oracle.
---
src/plugins/value/engine/evaluation.ml | 19 ++++++++++++++-----
.../value/engine/subdivided_evaluation.ml | 3 +--
.../value/engine/subdivided_evaluation.mli | 3 ++-
3 files changed, 17 insertions(+), 8 deletions(-)
diff --git a/src/plugins/value/engine/evaluation.ml b/src/plugins/value/engine/evaluation.ml
index f306a61dbef..36e832a57b6 100644
--- a/src/plugins/value/engine/evaluation.ml
+++ b/src/plugins/value/engine/evaluation.ml
@@ -746,6 +746,9 @@ module Make
type context =
{ (* The abstract domain state in which the evaluation takes place. *)
state: Domain.t;
+ (* Maximum number of subdivisions. See {!Subdivided_evaluation} for
+ more details. *)
+ subdivision: int;
(* The remaining fuel: maximum number of nested oracle uses, decremented
at each call to the oracle. *)
remaining_fuel: int;
@@ -1093,7 +1096,8 @@ module Make
fun expr ->
let valuation = !cache in
let context = { context with remaining_fuel } in
- Subdivided_Evaluation.evaluate context valuation expr
+ let subdivnb = context.subdivision in
+ Subdivided_Evaluation.evaluate context valuation ~subdivnb expr
>>=: fun (valuation, value) ->
cache := valuation;
value
@@ -1104,15 +1108,20 @@ module Make
with maximal precision. *)
let root_context state =
let remaining_fuel = root_fuel () in
- { state; remaining_fuel; oracle }
+ let subdivision = Value_parameters.LinearLevel.get () in
+ { state; subdivision; remaining_fuel; oracle }
- (* Context for a fast forward evaluation with minimal precision. *)
+ (* Context for a fast forward evaluation with minimal precision:
+ no subdivisions and no call to the oracle. *)
let low_context state =
let remaining_fuel = no_fuel in
- { state; remaining_fuel; oracle }
+ let subdivision = 0 in
+ { state; subdivision; remaining_fuel; oracle }
let subdivided_forward_eval valuation state expr =
- Subdivided_Evaluation.evaluate (root_context state) valuation expr
+ let context = root_context state in
+ let subdivnb = context.subdivision in
+ Subdivided_Evaluation.evaluate context valuation ~subdivnb expr
(* ------------------------------------------------------------------------
Backward Evaluation
diff --git a/src/plugins/value/engine/subdivided_evaluation.ml b/src/plugins/value/engine/subdivided_evaluation.ml
index ab59086cbb7..b832e789d36 100644
--- a/src/plugins/value/engine/subdivided_evaluation.ml
+++ b/src/plugins/value/engine/subdivided_evaluation.ml
@@ -772,8 +772,7 @@ module Make
in
subdivide_subexpr vars valuation result alarms
- let evaluate context valuation expr =
- let subdivnb = Value_parameters.LinearLevel.get () in
+ let evaluate context valuation ~subdivnb expr =
if subdivnb = 0 || not activated
then Eva.evaluate context valuation expr
else subdivide_evaluation context valuation subdivnb expr
diff --git a/src/plugins/value/engine/subdivided_evaluation.mli b/src/plugins/value/engine/subdivided_evaluation.mli
index 34f7836676c..25ed9703977 100644
--- a/src/plugins/value/engine/subdivided_evaluation.mli
+++ b/src/plugins/value/engine/subdivided_evaluation.mli
@@ -44,7 +44,8 @@ module Make
: sig
val evaluate:
- Eva.context -> Valuation.t -> exp -> (Valuation.t * Value.t) evaluated
+ Eva.context -> Valuation.t -> subdivnb:int ->
+ exp -> (Valuation.t * Value.t) evaluated
val reduce_by_enumeration:
Eva.context -> Valuation.t -> exp -> bool -> Valuation.t or_bottom
--
GitLab