From 18cd9ce3b7f478639031b2af3dcb99ff687ae3e8 Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?David=20B=C3=BChler?= <david.buhler@cea.fr>
Date: Fri, 18 Mar 2022 17:27:24 +0100
Subject: [PATCH] [Eva] Multidim: registers a hook to access other domain
states in the join.
---
Makefile | 2 +-
src/plugins/value/domains/multidim_domain.ml | 43 +++++++++++++++++++
src/plugins/value/domains/multidim_domain.mli | 2 +
src/plugins/value/engine/abstractions.ml | 6 ---
src/plugins/value/engine/abstractions.mli | 1 -
5 files changed, 46 insertions(+), 8 deletions(-)
diff --git a/Makefile b/Makefile
index 10816b72815..8d1f4aeae6d 100644
--- a/Makefile
+++ b/Makefile
@@ -881,7 +881,6 @@ PLUGIN_CMO:= partitioning/split_strategy domains/domain_mode self parameters \
domains/hcexprs \
domains/equality/equality domains/equality/equality_domain \
domains/offsm_domain \
- domains/multidim_domain \
domains/symbolic_locs \
domains/sign_domain \
domains/cvalue/warn domains/cvalue/locals_scoping \
@@ -906,6 +905,7 @@ PLUGIN_CMO:= partitioning/split_strategy domains/domain_mode self parameters \
engine/transfer_logic engine/transfer_stmt engine/transfer_specification \
engine/mem_exec engine/iterator engine/initialization \
engine/compute_functions engine/analysis register \
+ domains/multidim_domain \
domains/taint_domain \
$(APRON_CMO) $(NUMERORS_CMO) \
utils/eva_results \
diff --git a/src/plugins/value/domains/multidim_domain.ml b/src/plugins/value/domains/multidim_domain.ml
index 86d3850c471..9ebd380bd81 100644
--- a/src/plugins/value/domains/multidim_domain.ml
+++ b/src/plugins/value/domains/multidim_domain.ml
@@ -849,3 +849,46 @@ struct
end
include Domain
+
+let multidim_top = top
+let better_join _oracle_left _oracle_right a b = join a b
+
+let multidim_hook (module Abstract: Abstractions.S) : (module Abstractions.S) =
+ match Abstract.Dom.get key with
+ | None -> (module Abstract)
+ | Some get_multidim ->
+ let module Eval =
+ Evaluation.Make (Abstract.Val) (Abstract.Loc) (Abstract.Dom)
+ in
+ let module Dom = struct
+ include Abstract.Dom
+
+ let join a b =
+ let r = join (set key multidim_top a) (set key multidim_top b) in
+ let left_oracle = Eval.evaluate a in
+ let right_oracle = Eval.evaluate b in
+ let taint =
+ better_join left_oracle right_oracle (get_multidim a) (get_multidim b)
+ in
+ set key taint r
+ end
+ in
+ (module struct
+ module Val = Abstract.Val
+ module Loc = Abstract.Loc
+ module Dom = Dom
+ end)
+
+(* Registers the domain. *)
+let flag =
+ let name = "multidim"
+ and descr = "Improve the precision over arrays of structures \
+ or multidimensional arrays."
+ and experimental = true
+ and abstraction =
+ Abstractions.{ values = Single (module Main_values.CVal);
+ domain = Domain (module Domain); }
+ in
+ Abstractions.register ~name ~descr ~experimental abstraction
+
+let () = Abstractions.register_hook multidim_hook
diff --git a/src/plugins/value/domains/multidim_domain.mli b/src/plugins/value/domains/multidim_domain.mli
index 3a451e5b12d..a9d0279ec7b 100644
--- a/src/plugins/value/domains/multidim_domain.mli
+++ b/src/plugins/value/domains/multidim_domain.mli
@@ -23,3 +23,5 @@
include Abstract_domain.Leaf
with type value = Cvalue.V.t
and type location = Precise_locs.precise_location
+
+val flag: Abstractions.flag
diff --git a/src/plugins/value/engine/abstractions.ml b/src/plugins/value/engine/abstractions.ml
index 573e734b218..fedceb3f36f 100644
--- a/src/plugins/value/engine/abstractions.ml
+++ b/src/plugins/value/engine/abstractions.ml
@@ -174,12 +174,6 @@ module Config = struct
to a statement."
(module Traces_domain.D)
- let multidim =
- make 2 "multidim" ~experimental:true
- "Improve the precision over arrays of structures or multidimensional \
- arrays."
- (module Multidim_domain)
-
let printer =
make 2 "printer"
"Debug domain, only useful for developers. Prints the transfer functions \
diff --git a/src/plugins/value/engine/abstractions.mli b/src/plugins/value/engine/abstractions.mli
index 4f761517c0d..c8f03be0c01 100644
--- a/src/plugins/value/engine/abstractions.mli
+++ b/src/plugins/value/engine/abstractions.mli
@@ -158,7 +158,6 @@ module Config : sig
val inout: flag
val sign: flag
val traces: flag
- val multidim: flag
val printer: flag
val default: t
--
GitLab