From a1e0fdc99b385ec4186edb43e3ad9a8050e1d278 Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?David=20B=C3=BChler?= <david.buhler@cea.fr>
Date: Wed, 27 Feb 2019 14:26:27 +0100
Subject: [PATCH] [Eva] New meta options -eva-fast, -eva-precise and
-eva-power.
Quick configuration of a fast (but imprecise) or precise (but slow) analysis.
---
src/plugins/value/value_parameters.ml | 82 +++++++++++++++++++++++++++
1 file changed, 82 insertions(+)
diff --git a/src/plugins/value/value_parameters.ml b/src/plugins/value/value_parameters.ml
index 7eda5b6c514..b7d58f50470 100644
--- a/src/plugins/value/value_parameters.ml
+++ b/src/plugins/value/value_parameters.ml
@@ -1318,6 +1318,88 @@ module MallocLevel =
end)
let () = MallocLevel.add_aliases ["-val-mlevel"]
+(* -------------------------------------------------------------------------- *)
+(* --- Meta options --- *)
+(* -------------------------------------------------------------------------- *)
+
+let () = Parameter_customize.set_negative_option_name ""
+module Fast =
+ False
+ (struct
+ let option_name = "-eva-fast"
+ let help = "Quick configuration for a fast (but rather imprecise) analysis. \
+ Opposite of (and incompatible with) -eva-precise. \
+ Equivalent to -eva-power 0."
+ end)
+
+let () = Parameter_customize.set_negative_option_name ""
+module Precise =
+ False
+ (struct
+ let option_name = "-eva-precise"
+ let help = "Quick configuration for a precise (but rather slow) analysis. \
+ Opposite of (and incompatible with) -eva-fast. \
+ Equivalent to -eva-power 5."
+ end)
+
+module Power =
+ Int
+ (struct
+ let option_name = "-eva-power"
+ let arg_name = "n"
+ let default = -1
+ let help = "Meta-option that automatically sets up some Eva parameters \
+ for a quick configuration of an analysis, \
+ from 0 (fastest but rather imprecise analysis) \
+ to 10 (accurate but potentially slow analysis)."
+ end)
+let () = Power.set_range (-1) 10
+
+let incompatible_meta_options () =
+ abort "The meta options %s, %s and %s are mutually incompatible."
+ Fast.name Precise.name Power.name
+
+(* Sets a parameter, unless is is already set. *)
+let set (type t) (module P: Parameter_sig.S with type t = t) t =
+ if P.is_set ()
+ then printf " option %s has already been set, and is not modified." P.name
+ else
+ begin
+ P.set t;
+ let str = Typed_parameter.get_value P.parameter in
+ if P.is_default ()
+ then printf " option %s kept at its default value: %s." P.name str
+ else printf " option %s set to %s." P.name str;
+ end
+
+let slevel_power = [| 0; 10; 25; 50; 75; 100; 150; 200; 300; 400; 500; |]
+
+let set_analysis option_name n =
+ if Fast.is_set () && option_name <> Fast.name
+ || Precise.is_set () && option_name <> Precise.name
+ || Power.is_set () && option_name <> Power.name
+ then incompatible_meta_options ();
+ feedback "Option %s detected, \
+ automatic configuration of the analysis:" option_name;
+ set (module (MinLoopUnroll)) (n / 2);
+ set (module (SemanticUnrollingLevel)) (slevel_power.(n));
+ set (module (WideningDelay)) (1 + n / 2);
+ set (module (ILevel)) (8 + 12 * n);
+ set (module (ArrayPrecisionLevel)) (50 * (n+1));
+ set (module (LinearLevel)) (20 * n);
+ set (module (RmAssert)) (n > 0);
+ set (module (SymbolicLocsDomain)) (n > 0);
+ set (module (EqualityDomain)) (n > 1);
+ set (module (EqualityCall)) (if n > 2 then "formals" else "none");
+ set (module (GaugesDomain)) (n > 3);
+ set (module (SplitReturn)) (if n > 4 then "auto" else "");
+ ()
+
+let () =
+ Fast.add_update_hook (fun _ n -> if n then set_analysis Fast.name 0);
+ Precise.add_update_hook (fun _ n -> if n then set_analysis Precise.name 5);
+ Power.add_update_hook (fun _ n -> if n >= 0 then set_analysis Power.name n)
+
(* -------------------------------------------------------------------------- *)
(* --- Freeze parameters. MUST GO LAST --- *)
(* -------------------------------------------------------------------------- *)
--
GitLab