From f37eb27e87a84843d6c928d4153265a15b1ac891 Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?David=20B=C3=BChler?= <david.buhler@cea.fr>
Date: Fri, 21 Jul 2023 17:42:20 +0200
Subject: [PATCH] [Eva] Multidim domain: optimizes the oracle function of the
join.
Caches calls to the oracle by saving the resulting valuation and reusing it
on next calls.
---
.../eva/domains/multidim/multidim_domain.ml | 21 ++++++++++++-------
1 file changed, 14 insertions(+), 7 deletions(-)
diff --git a/src/plugins/eva/domains/multidim/multidim_domain.ml b/src/plugins/eva/domains/multidim/multidim_domain.ml
index 55b457e1695..26d4bab6710 100644
--- a/src/plugins/eva/domains/multidim/multidim_domain.ml
+++ b/src/plugins/eva/domains/multidim/multidim_domain.ml
@@ -918,15 +918,22 @@ let multidim_hook (module Abstract: Abstractions.S) : (module Abstractions.S) =
let join a b =
let r = join (set key Domain.top a) (set key Domain.top b) in
- let oracle state exp = (* TODO: cache results *)
- let v, _alarms = Eval.evaluate state exp in
- match v with
- | `Bottom -> Cvalue.V.top
- | `Value (_valuation,v) -> get_cval v
+ let oracle state =
+ let valuation_ref = ref Eval.Valuation.empty in
+ fun exp ->
+ let valuation = !valuation_ref in
+ let v, _alarms = Eval.evaluate ~valuation state exp in
+ match v with
+ | `Bottom -> Cvalue.V.top
+ | `Value (valuation, v) ->
+ valuation_ref := valuation;
+ get_cval v
in
+ let left_oracle = oracle a
+ and right_oracle = oracle b in
let oracle = function
- | Abstract_memory.Left -> convert_oracle (oracle a)
- | Abstract_memory.Right -> convert_oracle (oracle b)
+ | Abstract_memory.Left -> convert_oracle left_oracle
+ | Abstract_memory.Right -> convert_oracle right_oracle
in
let multidim = Domain.join' ~oracle (get_multidim a) (get_multidim b) in
set key multidim r
--
GitLab