diff --git a/Makefile b/Makefile index 10816b728150b3b64bf166cd2a96c07d24704816..8d1f4aeae6d452f3385c1666246f4f47a385f4aa 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 86d3850c4712da8d6d42c39bdc51b39c34c47c6d..9ebd380bd814cbf8e676eff683dae0b436efeae4 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 3a451e5b12d610e2cf11b89159583f9092fc86f0..a9d0279ec7b2d271d22790313bf8cbe488108f0e 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 573e734b218e6299ef6a2a5be8634f2ca7022264..fedceb3f36ff2cd185349b8eb1b5f5303ce05829 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 4f761517c0d69f6c2605ab9f4ec452f7bd51c7fe..c8f03be0c01f42a72c661500e9e0b3a11e6af28a 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