From 17ddef0c2f975efc0f9eea47db632afa0a252e90 Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?David=20B=C3=BChler?= <david.buhler@cea.fr>
Date: Thu, 5 Nov 2020 10:36:16 +0100
Subject: [PATCH] [Eva] Widening thresholds of global variables are independent
of functions.
---
src/plugins/value/utils/widen.ml | 72 ++++++++++++++++----------------
1 file changed, 36 insertions(+), 36 deletions(-)
diff --git a/src/plugins/value/utils/widen.ml b/src/plugins/value/utils/widen.ml
index 26256dfdd10..fd0ba303f42 100644
--- a/src/plugins/value/utils/widen.ml
+++ b/src/plugins/value/utils/widen.ml
@@ -49,6 +49,21 @@ let rec constFoldTermToLogicReal = function
end
| _ -> None
+
+module Global_Static_Hints =
+ State_builder.Ref
+ (Widen_type)
+ (struct
+ let dependencies = [ Ast.self ]
+ let name = "Widen.Global_Static_Hints"
+ let default = Widen_type.default
+ end)
+let () = Ast.add_monotonic_state Global_Static_Hints.self
+
+let update_global_hints new_hints =
+ let hints = Widen_type.join (Global_Static_Hints.get ()) new_hints in
+ Global_Static_Hints.set hints;
+
class pragma_widen_visitor init_widen_hints init_enclosing_loops = object(self)
inherit Visitor.frama_c_inplace
@@ -56,16 +71,16 @@ class pragma_widen_visitor init_widen_hints init_enclosing_loops = object(self)
val enclosing_loops = init_enclosing_loops
method private add_int_thresholds ?base int_thresholds =
- widen_hints :=
- Widen_type.join
- (Widen_type.num_hints None(*see note*) base int_thresholds)
- !widen_hints
+ let new_hints = Widen_type.num_hints None(*see note*) base int_thresholds in
+ if Extlib.may_map Base.is_global ~dft:false base
+ then update_global_hints new_hints
+ else widen_hints := Widen_type.join new_hints !widen_hints
method private add_float_thresholds ?base float_thresholds =
- widen_hints :=
- Widen_type.join
- (Widen_type.float_hints None(*see note*) base float_thresholds)
- !widen_hints
+ let new_hints = Widen_type.float_hints None base float_thresholds in
+ if Extlib.may_map Base.is_global ~dft:false base
+ then update_global_hints new_hints
+ else widen_hints := Widen_type.join new_hints !widen_hints
method private add_var_hints ~stmt hints =
widen_hints := Widen_type.join (Widen_type.var_hints stmt hints) !widen_hints
@@ -385,35 +400,18 @@ class hints_visitor init_widen_hints global = object(self)
Cil.DoChildren
end
-module Global_Static_Hints =
- State_builder.Ref
- (Widen_type)
- (struct
- let dependencies = [ Ast.self ]
- let name = "Widen.Global_Static_Hints"
- let default = Widen_type.default
- end)
-let () = Ast.add_monotonic_state Global_Static_Hints.self
-
-(* Global widen hints, used for all functions *)
-let global_widen_hints () =
- if (not (Global_Static_Hints.is_computed ())) then
- begin
- Value_parameters.debug ~dkey "computing global widen hints";
- let global_widen_hints = ref (Widen_type.default ()) in
- Globals.Functions.iter_on_fundecs (fun fd ->
- let visitor = new hints_visitor global_widen_hints true in
- ignore (Visitor.visitFramacFunction visitor fd)
- );
- Global_Static_Hints.set !global_widen_hints;
- Global_Static_Hints.mark_as_computed ();
- !global_widen_hints
- end
- else
- Global_Static_Hints.get ()
+(* Precompute global widen hints, used for all functions *)
+let compute_global_static_hints () =
+ Value_parameters.debug ~dkey "computing global widen hints";
+ let global_widen_hints = ref (Global_Static_Hints.get ()) in
+ Globals.Functions.iter_on_fundecs (fun fd ->
+ let visitor = new hints_visitor global_widen_hints true in
+ ignore (Visitor.visitFramacFunction visitor fd)
+ );
+ Global_Static_Hints.set !global_widen_hints
let per_function_static_hints fdec =
- let widen_hints = ref (global_widen_hints ()) in
+ let widen_hints = ref Widen_type.empty in
let visitor_pragma = new pragma_widen_visitor widen_hints [] in
ignore (Visitor.visitFramacFunction visitor_pragma fdec);
let visitor_local = new hints_visitor widen_hints false in
@@ -433,6 +431,7 @@ let () = Ast.add_monotonic_state Per_Function_Static_Hints.self
(* parse and precompute global and local static hints *)
let precompute_widen_hints () =
+ compute_global_static_hints ();
Globals.Functions.iter_on_fundecs
(fun fd ->
Per_Function_Static_Hints.replace fd (per_function_static_hints fd))
@@ -549,12 +548,13 @@ module Per_Function_Hints =
let () = Ast.add_monotonic_state Per_Function_Hints.self
let extract_per_function_hints fdec =
+ let global = Global_Static_Hints.get () in
let for_fdec =
try Per_Function_Static_Hints.find fdec
with Not_found -> assert false
in
let dynamic = Dynamic_Hints.get () in
- Widen_type.join for_fdec dynamic
+ Widen_type.join (Widen_type.join global for_fdec) dynamic
let per_function_hints = Per_Function_Hints.memo extract_per_function_hints
--
GitLab