diff --git a/src/plugins/value/engine/analysis.ml b/src/plugins/value/engine/analysis.ml
index d11f2ec4640a155548971d5acf9d85c146c377d1..65ba4b0c285978a9e173e3e5888249989e917ffb 100644
--- a/src/plugins/value/engine/analysis.ml
+++ b/src/plugins/value/engine/analysis.ml
@@ -157,6 +157,7 @@ let reset_analyzer () =
(* Builds the analyzer if needed, and run the analysis. *)
let force_compute () =
Ast.compute ();
+ Value_parameters.configure_precision ();
let kf, lib_entry = Globals.entry_point () in
reset_analyzer ();
let module Analyzer = (val snd !ref_analyzer) in
diff --git a/src/plugins/value/gui_files/register_gui.ml b/src/plugins/value/gui_files/register_gui.ml
index 80d4d7ebce2766f4310fe98fcd23170f348f4543..33fcef5d778f2ff3b7a2ac3df5b96c215369f6e2 100644
--- a/src/plugins/value/gui_files/register_gui.ml
+++ b/src/plugins/value/gui_files/register_gui.ml
@@ -113,16 +113,24 @@ let value_panel pack (main_ui:main_ui) =
GPack.table ~packing:(box#pack ~expand:true ~fill:true) ~columns:2 ()
in
let box_1_1 = GPack.hbox ~packing:(w#attach ~left:1 ~top:1) () in
+ let precision_refresh =
+ let tooltip = Value_parameters.Precision.parameter.Typed_parameter.help in
+ Gtk_helper.on_int ~lower:(-1) ~upper:11 ~tooltip
+ box_1_1 "precision (meta-option)"
+ Value_parameters.Precision.get
+ Value_parameters.Precision.set
+ in
+ let box_1_2 = GPack.hbox ~packing:(w#attach ~left:1 ~top:2) () in
let slevel_refresh =
let tooltip =
Value_parameters.SemanticUnrollingLevel.parameter.Typed_parameter.help
in
Gtk_helper.on_int ~lower:0 ~upper:1000000 ~tooltip
- box_1_1 "slevel"
+ box_1_2 "slevel"
Value_parameters.SemanticUnrollingLevel.get
Value_parameters.SemanticUnrollingLevel.set
in
- let box_1_2 = GPack.hbox ~packing:(w#attach ~left:1 ~top:2) () in
+ let box_1_3 = GPack.hbox ~packing:(w#attach ~left:1 ~top:3) () in
let validator s =
not
(Kernel_function.Set.is_empty
@@ -130,9 +138,9 @@ let value_panel pack (main_ui:main_ui) =
in
let main_refresh = Gtk_helper.on_string
~tooltip:Kernel.MainFunction.parameter.Typed_parameter.help
- ~validator box_1_2 "main" Kernel.MainFunction.get Kernel.MainFunction.set
+ ~validator box_1_3 "main" Kernel.MainFunction.get Kernel.MainFunction.set
in
- let refresh () = slevel_refresh (); main_refresh() in
+ let refresh () = precision_refresh (); slevel_refresh (); main_refresh() in
ignore (run_button#connect#pressed
(fun () ->
main_ui#protect ~cancelable:true
diff --git a/src/plugins/value/value_parameters.ml b/src/plugins/value/value_parameters.ml
index 4c5bb46a70846232a69120259020ab6322920a19..0f8cb4ca773b121746c0af4c6c998912fbb4df51 100644
--- a/src/plugins/value/value_parameters.ml
+++ b/src/plugins/value/value_parameters.ml
@@ -659,7 +659,7 @@ module ILevel =
let () = add_precision_dep ILevel.parameter
let () = ILevel.add_aliases ["-val-ilevel"]
let () = ILevel.add_update_hook (fun _ i -> Ival.set_small_cardinal i)
-let () = ILevel.set_range 4 128
+let () = ILevel.set_range 4 256
let () = Parameter_customize.set_group precision_tuning
module SemanticUnrollingLevel =
@@ -1319,6 +1319,83 @@ module MallocLevel =
end)
let () = MallocLevel.add_aliases ["-val-mlevel"]
+(* -------------------------------------------------------------------------- *)
+(* --- Meta options --- *)
+(* -------------------------------------------------------------------------- *)
+
+module Precision =
+ Int
+ (struct
+ let option_name = "-eva-precision"
+ 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 11 (accurate but potentially slow analysis)."
+ end)
+let () = Precision.set_range (-1) 11
+let () = add_precision_dep Precision.parameter
+
+(* Sets a parameter [P] to [t], unless it has already been set by any other
+ means. *)
+let set (type t) (module P: Parameter_sig.S with type t = t) =
+ let previous = ref (P.get ()) in
+ fun ~default t ->
+ let already_set = P.is_set () && not (P.equal !previous (P.get ())) in
+ if not already_set then begin
+ if default then P.clear () else P.set t;
+ previous := P.get ();
+ end;
+ let str = Typed_parameter.get_value P.parameter in
+ let str = match P.parameter.Typed_parameter.accessor with
+ | Typed_parameter.String _ -> "\'" ^ str ^ "\'"
+ | _ -> str
+ in
+ printf " option %s %sset to %s%s." P.name
+ (if already_set then "already " else "") str
+ (if already_set && not (P.equal t (P.get ())) then " (not modified)"
+ else if P.is_default () then " (default value)" else "")
+
+(* List of configure functions to be called for -eva-precision. *)
+let configures = ref []
+
+(* Binds the parameter [P] to the function [f] that gives the parameter value
+ for a precision n. *)
+let bind (type t) (module P: Parameter_sig.S with type t = t) f =
+ let set = set (module P) in
+ configures := (fun n -> set ~default:(n < 0) (f n)) :: !configures
+
+(* power 0 1 2 3 4 5 6 7 8 9 10 11 *)
+let slevel_power = [| 0; 10; 20; 50; 75; 100; 200; 500; 1000; 2000; 5000; 10000 |]
+let ilevel_power = [| 8; 12; 16; 24; 32; 64; 128; 256; 256; 256; 256; 256 |]
+let plevel_power = [| 10; 20; 40; 70; 100; 150; 200; 300; 500; 700; 1000; 2000 |]
+
+let get array n = if n < 0 then 0 else array.(n)
+
+let () =
+ bind (module MinLoopUnroll) (fun n -> max 0 (n - 4));
+ bind (module SemanticUnrollingLevel) (get slevel_power);
+ bind (module WideningDelay) (fun n -> 1 + n / 2);
+ bind (module ILevel) (get ilevel_power);
+ bind (module ArrayPrecisionLevel) (get plevel_power);
+ bind (module LinearLevel) (fun n -> n * 20);
+ bind (module RmAssert) (fun n -> n > 0);
+ bind (module SymbolicLocsDomain) (fun n -> n > 0);
+ bind (module EqualityDomain) (fun n -> n > 1);
+ bind (module EqualityCall) (fun n -> if n > 2 then "formals" else "none");
+ bind (module GaugesDomain) (fun n -> n > 3);
+ bind (module SplitReturn) (fun n -> if n > 4 then "auto" else "");
+ ()
+
+let set_analysis n =
+ feedback "Option %s %i detected, \
+ automatic configuration of the analysis:" Precision.name n;
+ List.iter ((|>) n) (List.rev !configures)
+
+let configure_precision () =
+ if Precision.is_set () then set_analysis (Precision.get ())
+
(* -------------------------------------------------------------------------- *)
(* --- Freeze parameters. MUST GO LAST --- *)
(* -------------------------------------------------------------------------- *)
diff --git a/src/plugins/value/value_parameters.mli b/src/plugins/value/value_parameters.mli
index 8d1356a799a297539b52ab4f2b5c13cf0618f1f2..1edd3dac575243c6c528a686411f75ac92df9a65 100644
--- a/src/plugins/value/value_parameters.mli
+++ b/src/plugins/value/value_parameters.mli
@@ -149,6 +149,13 @@ module MallocFunctions: Parameter_sig.String_set
module AllocReturnsNull: Parameter_sig.Bool
module MallocLevel: Parameter_sig.Int
+(** Meta-option *)
+module Precision: Parameter_sig.Int
+
+(* Automatically sets some parameters according to the meta-option
+ -eva-precision. *)
+val configure_precision: unit -> unit
+
val parameters_correctness: Typed_parameter.t list
val parameters_tuning: Typed_parameter.t list