diff --git a/Makefile b/Makefile
index 0dd665f826204332ab4022ab8055f520d83ff2a7..b99afea518b664558478423dade71ea554e0a325 100644
--- a/Makefile
+++ b/Makefile
@@ -825,6 +825,8 @@ PLUGIN_EXTRA_DIRS:=engine values domains api domains/cvalue domains/apron \
domains/gauges domains/equality legacy partitioning utils gui_files \
api values/numerors domains/numerors
PLUGIN_TESTS_DIRS+=value/traces
+PLUGIN_GENERATED:=$(PLUGIN_DIR)/Eva.mli
+PLUGIN_DISTRIB_EXTERNAL+=gen-api.sh
# Files for the binding to Apron domains. Only available if Apron is available.
ifeq ($(HAS_APRON),yes)
@@ -908,7 +910,7 @@ PLUGIN_CMO:= partitioning/split_strategy domains/domain_mode value_parameters \
domains/taint_domain \
$(APRON_CMO) $(NUMERORS_CMO) \
api/general_requests api/values_request \
- utils/unit_tests
+ utils/unit_tests utils/results
PLUGIN_CMI:= values/abstract_value values/abstract_location \
domains/abstract_domain domains/simpler_domains
PLUGIN_DEPENDENCIES:=Server
@@ -927,8 +929,26 @@ VALUE_TYPES:=$(addprefix src/plugins/value_types/,\
PLUGIN_TYPES_CMO:=$(VALUE_TYPES)
PLUGIN_TYPES_TODOC:=$(addsuffix .mli,$(VALUE_TYPES))
+# Eva API.
+API_MLI := $(addprefix $(PLUGIN_DIR)/, \
+ engine/analysis.mli utils/results.mli \
+ value_parameters.mli utils/eva_annotations.mli \
+ eval.mli domains/cvalue/builtins.mli \
+ legacy/eval_terms.mli utils/value_results.mli utils/unit_tests.mli)
+
+$(PLUGIN_DIR)/Eva.mli: $(PLUGIN_DIR)/gen-api.sh Makefile $(API_MLI)
+ $(PRINT_MAKING) $@
+ $(RM) $@ $@.tmp
+ $< $(API_MLI) > $@.tmp
+ $(CHMOD_RO) $@.tmp
+ $(MV) $@.tmp $@
+
+clean::
+ $(RM) $(PLUGIN_DIR)/Eva.mli
+
$(eval $(call include_generic_plugin_Makefile,$(PLUGIN_NAME)))
+
#########
# Reduc #
#########
diff --git a/doc/developer/advance.tex b/doc/developer/advance.tex
index 508230d7c8c933b49215876099e358da74ff20ed..906403ec31d7d23a95bc4be30992c333c53901f1 100644
--- a/doc/developer/advance.tex
+++ b/doc/developer/advance.tex
@@ -2487,10 +2487,10 @@ following.
~
\begin{ocamlcode}
-!Db.Value.compute();
-Kernel.feedback "%B" (Db.Value.is_computed ()); (* true *)
+Eva.Analysis.compute();
+Kernel.feedback "%B" (Eva.Analysis.is_computed ()); (* true *)
Globals.set_entry_point "f" true;
-Kernel.feedback "%B" (Db.Value.is_computed ()); (* false *)
+Kernel.feedback "%B" (Eva.Analysis.is_computed ()); (* false *)
\end{ocamlcode}
As the value analysis has been automatically reset when setting the entry point,
the above code outputs
@@ -2548,7 +2548,7 @@ let compute_info (kf,vi) = ...
let memoize s =
try Stmt.Hashtbl.find state s
with Not_found -> Stmt.Hashtbl.add state s (compute_info s)
-let run () = ... !Db.Value.compute (); ... memoize some_stmt ...
+let run () = ... Eva.Analysis.compute (); ... memoize some_stmt ...
\end{ocamlcode}
However, if one puts this code inside \framac, it does not work because this
@@ -2570,7 +2570,7 @@ module State =
end)
let compute_info (kf,vi) = ...
let memoize = State.memo compute_info
-let run () = ... !Db.Value.compute (); ... memoize some_stmt ...
+let run () = ... Eva.Analysis.compute (); ... memoize some_stmt ...
\end{ocamlcode}
A quick look on this code shows that the declaration of the state itself is more
complicated (it uses a functor application) but its use is
@@ -2870,14 +2870,14 @@ value analysis has never been computed previously)
\scodeidx{Project}{IOError}
\begin{ocamlcode}
let print_computed () =
- Kernel.feedback "%B" (Db.Value.is_computed ())
+ Kernel.feedback "%B" (Eva.Analysis.is_computed ())
in
print_computed (); (* false *)
let old = Project.current () in
try
let foo = Project.load ~name:"foo" "foo.sav" in
Project.set_current foo;
- !Db.Value.compute ();
+ Eva.Analysis.compute ();
print_computed (); (* true *)
Project.set_current old;
print_computed () (* false *)
@@ -2913,13 +2913,13 @@ The following code is equivalent to the one given in
Example~\ref{ex:set_current}.
\begin{ocamlcode}
let print_computed () =
- Value_parameters.feedback "%B" (Db.Value.is_computed ())
+ Value_parameters.feedback "%B" (Eva.Analysis.is_computed ())
in
print_computed (); (* false *)
try
let foo = Project.load ~name:"foo" "foo.sav" in
Project.on foo
- (fun () -> !Db.Value.compute (); print_computed () (* true *)) ();
+ (fun () -> Eva.Analysis.compute (); print_computed () (* true *)) ();
print_computed () (* false *)
with Project.IOError _ ->
exit 1
diff --git a/doc/developer/check_api/run.oracle b/doc/developer/check_api/run.oracle
index 769847618c69cf2f9ca6f482711374dd559b3953..c5b9bea960a39741875927a46cfaee4c321bb3ec 100644
--- a/doc/developer/check_api/run.oracle
+++ b/doc/developer/check_api/run.oracle
@@ -96,7 +96,7 @@ Logic_utils.expr_to_term/cast:bool -> Cil_types.exp -> Cil_types.term/translates
Journal/(string -> string) Pervasives.refend /Journalization of functions./
Cil.cilVisitor.vstmt/Cil_types.stmt -> Cil_types.stmt Cil.visitAction/Control-flow statement. The default DoChildren action does not create a new statement when the components change. Instead it updates the contents of the original statement. This is done to preserve the sharing with Goto and Case statements that point to the original statement. If you use the ChangeTo action then you should take care of preserving that sharing yourself./
Cil.get_varinfo/Cil.visitor_behavior -> Cil_types.varinfo -> Cil_types.varinfo/retrieve the representative of a given varinfo in the current state of the visitor/
-Db.Value.is_computed/unit -> bool/Return true iff the value analysis has been done./
+Eva.Analysis.is_computed/unit -> bool/Return true iff the value analysis has been done./
Kernel.Unicode/('a -> 'b) -> 'a -> 'bend /Behavior of option "-unicode"./
Design.register_extension/(Design.main_window_extension_points -> unit) -> unit/Register an extension to the main GUI. It will be invoked at initialization time./
Cil_types.global/ | GType of Cil_types.typeinfo * Cil_types.location | GCompTag of Cil_types.compinfo * Cil_types.location | GCompTagDecl of Cil_types.compinfo * Cil_types.location | GEnumTag of Cil_types.enuminfo * Cil_types.location | GEnumTagDecl of Cil_types.enuminfo * Cil_types.location | GVarDecl of Cil_types.varinfo * Cil_types.location | GFunDecl of Cil_types.funspec * Cil_types.varinfo * Cil_types.location | GVar of Cil_types.varinfo * Cil_types.initinfo * Cil_types.location | GFun of Cil_types.fundec * Cil_types.location | GAsm of string * Cil_types.location | GPragma of Cil_types.attribute * Cil_types.location | GText of string | GAnnot of Cil_types.global_annotation * Cil_types.location/The main type for representing global declarations and definitions. A list of these form a CIL file. The order of globals in the file is generally important./
diff --git a/doc/developer/tutorial/viewcfg/src/dump_function_memo_clear_cache.ml b/doc/developer/tutorial/viewcfg/src/dump_function_memo_clear_cache.ml
index 3a83c607bb9f1075517684d443f10c25305c122f..36eb30f11660c19bc89f3524067d71382e014733 100644
--- a/doc/developer/tutorial/viewcfg/src/dump_function_memo_clear_cache.ml
+++ b/doc/developer/tutorial/viewcfg/src/dump_function_memo_clear_cache.ml
@@ -1,5 +1,5 @@
let dump_function fundec fmt =
- if not (Value_is_computed.get ()) && Db.Value.is_computed () then begin
+ if not (Value_is_computed.get ()) && Eva.Analysis.is_computed () then begin
Value_is_computed.set true;
let selection = State_selection.with_dependencies Cfg_graph_state.self in
Project.clear ~selection ();
diff --git a/doc/developer/tutorial/viewcfg/src/print_cfg_vstmt_aux_value.ml b/doc/developer/tutorial/viewcfg/src/print_cfg_vstmt_aux_value.ml
index 04446722a1f84abc19e1553058e7cc6f4ad2a5f8..67038d53098490e5c6d7b14991dac834b5b9e9a9 100644
--- a/doc/developer/tutorial/viewcfg/src/print_cfg_vstmt_aux_value.ml
+++ b/doc/developer/tutorial/viewcfg/src/print_cfg_vstmt_aux_value.ml
@@ -1,6 +1,6 @@
method! vstmt_aux s =
let color =
- if Db.Value.is_computed () then
+ if Eva.Analysis.is_computed () then
let state = Db.Value.get_stmt_state s in
let reachable = Db.Value.is_reachable state in
if reachable then "fillcolor=\"#ccffcc\" style=filled"
diff --git a/doc/training/developer/project.tex b/doc/training/developer/project.tex
index 98e08c503c07304da355bff6274bb29fbcde8398..8af2d2bceb399a059fc13eeb0438d6119316513c 100644
--- a/doc/training/developer/project.tex
+++ b/doc/training/developer/project.tex
@@ -175,7 +175,7 @@ let main () =
~select_annot:false
~select_slice_pragma:false
in
- Project.on p !Db.Value.compute ()
+ Project.on p Eva.Analysis.compute ()
\end{ocamlcode}
\end{itemize}
diff --git a/doc/training/developer/sources/basic_script.ml b/doc/training/developer/sources/basic_script.ml
index a9160149a1cbdab32d79dd1d34a89a53c04ff4b1..fd83c661bb190de5faf19f44fb978f59641aa548 100644
--- a/doc/training/developer/sources/basic_script.ml
+++ b/doc/training/developer/sources/basic_script.ml
@@ -10,7 +10,7 @@ let run f () =
incr nb_entry_points;
Kernel.MainFunction.set f;
Kernel.LibEntry.on ();
- !Db.Value.compute ()
+ Eva.Analysis.compute ()
(*# Main driver function*)
let all_entry_points () =
diff --git a/doc/training/developer/sources/const_violation.ml b/doc/training/developer/sources/const_violation.ml
index e057b7fbf7701f7492ff6aebc14db153cfec0c57..2eadb5524debd6e35c3ca20913df90252636c07a 100644
--- a/doc/training/developer/sources/const_violation.ml
+++ b/doc/training/developer/sources/const_violation.ml
@@ -3,7 +3,7 @@ let run () =
let glob = Globals.Vars.find_from_astinfo "Glob" Cil_types.VGlobal in
let glob_expr = Cil.evar ~loc:Cil_datatype.Location.unknown glob in
let main = Globals.Functions.find_by_name "main" in
- let () = !Db.Value.compute () in
+ let () = Eva.Analysis.compute () in
let init_stmt = Kernel_function.find_first_stmt main in
let init_state = Db.Value.get_stmt_state init_stmt in
let end_stmt = Kernel_function.find_return main in
diff --git a/headers/header_spec.txt b/headers/header_spec.txt
index cb21c86bf52c61ebfa4df23d3f566ad493728ae0..4a1d41dd38f7885727b646bf7f65d7a19b4aed76 100644
--- a/headers/header_spec.txt
+++ b/headers/header_spec.txt
@@ -1316,7 +1316,7 @@ src/plugins/users/users_register.ml: CEA_LGPL_OR_PROPRIETARY
src/plugins/users/users_register.mli: CEA_LGPL_OR_PROPRIETARY
src/plugins/value/.merlin: .ignore
src/plugins/value/Changelog_non_free: .ignore
-src/plugins/value/Eva.mli: CEA_LGPL_OR_PROPRIETARY
+src/plugins/value/Eva.mli: .ignore
src/plugins/value/alarmset.ml: CEA_LGPL_OR_PROPRIETARY
src/plugins/value/alarmset.mli: CEA_LGPL_OR_PROPRIETARY
src/plugins/value/api/general_requests.ml: CEA_LGPL_OR_PROPRIETARY
@@ -1429,6 +1429,7 @@ src/plugins/value/engine/transfer_stmt.ml: CEA_LGPL_OR_PROPRIETARY
src/plugins/value/engine/transfer_stmt.mli: CEA_LGPL_OR_PROPRIETARY
src/plugins/value/eval.ml: CEA_LGPL_OR_PROPRIETARY
src/plugins/value/eval.mli: CEA_LGPL_OR_PROPRIETARY
+src/plugins/value/gen-api.sh: .ignore
src/plugins/value/gui_files/gui_callstacks_filters.ml: CEA_LGPL_OR_PROPRIETARY
src/plugins/value/gui_files/gui_callstacks_filters.mli: CEA_LGPL_OR_PROPRIETARY
src/plugins/value/gui_files/gui_callstacks_manager.ml: CEA_LGPL_OR_PROPRIETARY
@@ -1451,6 +1452,8 @@ src/plugins/value/legacy/function_args.ml: CEA_LGPL_OR_PROPRIETARY
src/plugins/value/legacy/function_args.mli: CEA_LGPL_OR_PROPRIETARY
src/plugins/value/register.ml: CEA_LGPL_OR_PROPRIETARY
src/plugins/value/register.mli: CEA_LGPL_OR_PROPRIETARY
+src/plugins/value/utils/results.ml: CEA_LGPL_OR_PROPRIETARY
+src/plugins/value/utils/results.mli: CEA_LGPL_OR_PROPRIETARY
src/plugins/value/partitioning/auto_loop_unroll.ml: CEA_LGPL_OR_PROPRIETARY
src/plugins/value/partitioning/auto_loop_unroll.mli: CEA_LGPL_OR_PROPRIETARY
src/plugins/value/partitioning/partition.ml: CEA_LGPL_OR_PROPRIETARY
diff --git a/src/plugins/aorai/aorai_eva_analysis.enabled.ml b/src/plugins/aorai/aorai_eva_analysis.enabled.ml
index 8b007c55b15b021ba234a5d76899eb55587c0967..f95b747b5e7e9ce175417d44afa1832b6d2f3f62 100644
--- a/src/plugins/aorai/aorai_eva_analysis.enabled.ml
+++ b/src/plugins/aorai/aorai_eva_analysis.enabled.ml
@@ -25,7 +25,7 @@
let show_aorai_variable state fmt var_name =
let vi = Data_for_aorai.(get_varinfo var_name) in
- let cvalue = !Db.Value.eval_expr state (Cil.evar vi) in
+ let cvalue = Cvalue.Model.find state (Locations.loc_of_varinfo vi) in
try
let i = Ival.project_int (Cvalue.V.project_ival cvalue) in
let state_name = Data_for_aorai.getStateName (Integer.to_int_exn i) in
diff --git a/src/plugins/constant_propagation/api.ml b/src/plugins/constant_propagation/api.ml
index 569d5d24e3aeb69d3dbbf390330390aecc1c60da..be5eb41d5d1c6f1f542cf27a213372c95b6037d5 100644
--- a/src/plugins/constant_propagation/api.ml
+++ b/src/plugins/constant_propagation/api.ml
@@ -131,11 +131,11 @@ class propagate project fnames ~cast_intro = object(self)
| TEnum _) -> ()
| _ -> raise Cannot_expand
end;
- let ki = match self#current_stmt with
+ let stmt = match self#current_stmt with
| None -> raise Cannot_change
- | Some s -> Kstmt s
+ | Some s -> s
in
- let evaled = !Db.Value.access_expr ki expr in
+ let evaled = Eva.Results.(before stmt |> eval_exp expr |> as_cvalue) in
let b, m = Cvalue.V.find_lonely_binding evaled in
let can_replace vi =
(* can replace the current expr by [vi] iff (1) it is a source var, or
@@ -340,7 +340,7 @@ module Result =
let size = 7
let name = "Semantical constant propagation"
let dependencies =
- [ Db.Value.self;
+ [ Eva.Analysis.self;
PropagationParameters.CastIntro.self;
PropagationParameters.Project_name.self ]
end)
@@ -352,7 +352,7 @@ let journalized_get =
let get fnames cast_intro =
Result.memo
(fun _ ->
- !Db.Value.compute ();
+ Eva.Analysis.compute ();
let fresh_project =
FC_file.create_project_from_visitor
(PropagationParameters.Project_name.get ())
diff --git a/src/plugins/dive/build.ml b/src/plugins/dive/build.ml
index 6a08979f28db393ec3fcb6024a20c670f6a89241..b694d6d85ecb58b9256b6e05dcbf66547377dfa3 100644
--- a/src/plugins/dive/build.ml
+++ b/src/plugins/dive/build.ml
@@ -27,7 +27,6 @@ module Graph = Dive_graph
let dkey = Self.register_category "build"
-
(* --- Utility function --- *)
(* Breaks a list at n-th element into two sublists *)
@@ -76,29 +75,24 @@ end
module Eval =
struct
- let to_kf_list kinstr expr =
- let _,set = !Db.Value.expr_to_kernel_function kinstr ~deps:None expr in
- Kernel_function.Hptset.fold (fun kf acc -> kf :: acc) set []
+ open Eva.Results
+
+ let to_kf_list kinstr callee =
+ before_kinstr kinstr |> eval_callee callee |>
+ Result.value ~default:[]
let to_cvalue kinstr lval =
- let state = Db.Value.get_state kinstr in
- let _,cvalue = !Db.Value.eval_lval None state lval in
- cvalue
+ before_kinstr kinstr |> eval_lval lval |> as_cvalue
let to_location kinstr lval =
- let state = Db.Value.get_state kinstr in
- !Db.Value.lval_to_loc_state state lval
+ before_kinstr kinstr |> eval_address lval |> as_location |>
+ Result.value ~default:Locations.loc_bottom
let to_zone kinstr lval =
- !Db.Value.lval_to_zone kinstr lval
+ before_kinstr kinstr |> eval_address lval |> as_zone
let to_callstacks stmt =
- let states = Db.Value.get_stmt_state_callstack ~after:false stmt in
- match states with
- | None -> assert false
- | Some table ->
- let module Table = Value_types.Callstack.Hashtbl in
- Table.fold (fun cs _ acc -> cs :: acc) table []
+ before stmt |> callstacks
let studia_is_direct (_,{Studia.Writes.direct}) = direct
diff --git a/src/plugins/dive/context.ml b/src/plugins/dive/context.ml
index 3b91fbdf9ea2bbd5eb459079d421414f051f59c7..5dc407e377dc58dbfb24efb86459aa1fb28db5a1 100644
--- a/src/plugins/dive/context.ml
+++ b/src/plugins/dive/context.ml
@@ -51,7 +51,7 @@ type t = {
(* --- initialization --- *)
let create () =
- !Db.Value.compute ();
+ Eva.Analysis.compute ();
{
graph = Graph.create ();
vertex_table = Index.create 13;
diff --git a/src/plugins/dive/server_interface.ml b/src/plugins/dive/server_interface.ml
index 93e389396dc826aae8771fb83ef57878bb4d635a..999e07549497bb37b4bf985f2d81397f58f9ba81 100644
--- a/src/plugins/dive/server_interface.ml
+++ b/src/plugins/dive/server_interface.ml
@@ -38,7 +38,7 @@ let get_context =
match !context with
| Some c -> c
| None ->
- if Db.Value.is_computed () then
+ if Eva.Analysis.is_computed () then
let c = Context.create () in
context := Some c;
c
diff --git a/src/plugins/impact/compute_impact.ml b/src/plugins/impact/compute_impact.ml
index 4305f65b876bc2d4292644d27645c2ed8445ad9a..a4579f1fb6fab4ac5556f8da78e9cb40393268e4 100644
--- a/src/plugins/impact/compute_impact.ml
+++ b/src/plugins/impact/compute_impact.ml
@@ -332,8 +332,8 @@ let downward_one_call_node wl (pnode, _ as node) caller_kf pdg =
| Key.SigCallKey(id, key) ->
let stmt = Key.call_from_id id in
- let called_kfs = Db.Value.call_to_kernel_function stmt in
- KFS.iter
+ let called_kfs = Eva.Results.callee stmt in
+ List.iter
(fun called_kf ->
let called_pdg = !Db.Pdg.get called_kf in
let nodes_callee, pdg_ok =
@@ -452,7 +452,7 @@ let all_upward_callers wl kfs =
let pdg_caller = !Db.Pdg.get caller in
List.iter (aux_call (caller, pdg_caller) (kf, pdg_kf)) callsites;
KFS.add caller todo
- ) todo (!Db.Value.callers kf);
+ ) todo (Eva.Results.callsites kf);
)
else todo
in
@@ -536,7 +536,7 @@ let initial_worklist ?(skip=Locations.Zone.bottom) ?(reason=false) nodes kf =
let initial_nodes ~skip kf stmt =
Options.debug ~level:3 "computing initial nodes for %d" stmt.sid;
let pdg = !Db.Pdg.get kf in
- if Db.Value.is_reachable_stmt stmt then
+ if Eva.Results.is_reachable stmt then
try
let all = !Db.Pdg.find_simple_stmt_nodes pdg stmt in
let filter n = match PdgTypes.Node.elem_key n with
diff --git a/src/plugins/impact/register_gui.ml b/src/plugins/impact/register_gui.ml
index 38bba42a81961373ba276d255a81ef2986236755..75e1f7a1487d74eddfa93cee9851ded33f655ccd 100644
--- a/src/plugins/impact/register_gui.ml
+++ b/src/plugins/impact/register_gui.ml
@@ -208,7 +208,7 @@ let impact_statement =
let impact_statement_ui (main_ui:Design.main_window_extension_points) s =
- let val_computed = Db.Value.is_computed () in
+ let val_computed = Eva.Analysis.is_computed () in
ignore (impact_statement (*restriction*)Locations.Zone.top s);
if not val_computed then
main_ui#reset ()
diff --git a/src/plugins/inout/derefs.ml b/src/plugins/inout/derefs.ml
index 19bba4c86cccbfb4e72afb0a15313f0db8239d84..53bf4d9d7fa06d2c3c57adc9c83a48294bd6144e 100644
--- a/src/plugins/inout/derefs.ml
+++ b/src/plugins/inout/derefs.ml
@@ -86,7 +86,7 @@ module Externals =
let get_external =
Externals.memo
(fun kf ->
- !Db.Value.compute ();
+ Eva.Analysis.compute ();
if Kernel_function.is_definition kf then
try
externalize
diff --git a/src/plugins/inout/operational_inputs.ml b/src/plugins/inout/operational_inputs.ml
index 43736a78c9436ab1209a6d1bd9af3bed5476bfe3..85835a4966e9698c6afb0cbfd4cfb3df631d73f7 100644
--- a/src/plugins/inout/operational_inputs.ml
+++ b/src/plugins/inout/operational_inputs.ml
@@ -374,26 +374,18 @@ module Computer(Fenv:Dataflows.FUNCTION_ENV)(X:sig
| AAssert (_, p)
| AInvariant (_, true, p) ->
begin
- let env =
- Eva.Eval_terms.env_annot
- ~pre:X.kf_pre_state
- ~here:(X.stmt_state stmt)
- ()
+ let pre = X.kf_pre_state
+ and here = X.stmt_state stmt in
+ let deps =
+ Eva.Eval_terms.annot_predicate_deps ~pre ~here p.tp_statement
in
- match Eva.Eval_terms.predicate_deps env p.tp_statement with
+ match deps with
| None ->
(* To be sound, we should perform a join with the top zone here.
We do nothing instead because the latter behavior would
directly disable memexec. *)
()
- | Some logic_deps ->
- let p_zone =
- Cil_datatype.Logic_label.Map.fold
- (fun _ -> Zone.join)
- logic_deps
- Zone.bottom
- in
- store_non_terminating_logic_inputs p_zone
+ | Some p_zone -> store_non_terminating_logic_inputs p_zone
end
| _ -> ())
stmt
@@ -807,7 +799,7 @@ end
let get_internal =
Internals.memo
(fun kf ->
- !Db.Value.compute ();
+ Eva.Analysis.compute ();
try Internals.find kf (* The results may have been computed by the call
to Value.compute *)
with
diff --git a/src/plugins/inout/outputs.ml b/src/plugins/inout/outputs.ml
index 1137bece59862b3720436f2da090395382a8cc9e..5976c3b6f0fafc7bcc6e3e495609392e96e47bf7 100644
--- a/src/plugins/inout/outputs.ml
+++ b/src/plugins/inout/outputs.ml
@@ -48,11 +48,10 @@ class virtual do_it_ = object(self)
(* For local initializations, counts the written variable as an output of the
function, even if it is const; thus, [for_writing] is false in this case. *)
method private do_assign ~for_writing lv =
- let state = Db.Value.get_state self#current_kinstr in
- let _deps, bits_loc, _exact =
- !Db.Value.lval_to_zone_with_deps_state state
- ~deps:None ~for_writing lv
- in
+ let access = if for_writing then Write else Read in
+ let bits_loc = Eva.Results.(
+ before_kinstr self#current_kinstr |> eval_address lv |>
+ as_zone ~access) in
self#join bits_loc
method! vinst i =
diff --git a/src/plugins/inout/register.ml b/src/plugins/inout/register.ml
index f8615a255af358297d2005df233cabb149b43e94..00ca70a65a077cf27bdc6ef4ab6a1d6386517c7d 100644
--- a/src/plugins/inout/register.ml
+++ b/src/plugins/inout/register.ml
@@ -49,7 +49,7 @@ let main () =
Inout_parameters.Output.get () && ShouldOutput.get ()
then begin
ShouldOutput.set false;
- !Db.Value.compute ();
+ Eva.Analysis.compute ();
Callgraph.Uses.iter_in_rev_order
(fun kf ->
if Kernel_function.is_definition kf && !Db.Value.is_called kf
diff --git a/src/plugins/loop_analysis/Makefile.in b/src/plugins/loop_analysis/Makefile.in
index 4cb7ceebdc781357e9221147bad002aae4d4c284..a4aee4ac5c07f8d1596462e154ed1f4a874feb59 100644
--- a/src/plugins/loop_analysis/Makefile.in
+++ b/src/plugins/loop_analysis/Makefile.in
@@ -33,6 +33,7 @@ PLUGIN_DISTRIBUTED:=$(PLUGIN_ENABLE)
PLUGIN_NAME:= LoopAnalysis
PLUGIN_CMO:= options region_analysis region_analysis_stmt loop_analysis register
PLUGIN_CMI:= region_analysis_sig
+PLUGIN_DEPENDENCIES:= Eva
PLUGIN_DISTRIB_EXTERNAL:= Makefile.in configure.ac configure test.c test.oracle README.org
PLUGIN_TESTS_DIRS:=loop_analysis
diff --git a/src/plugins/loop_analysis/loop_analysis.ml b/src/plugins/loop_analysis/loop_analysis.ml
index 39a8827dd6a6ccf49727ac1b7cdb7a18c4d32dde..a37f5ec6586e66fc2b74e11a11b627dc6b060d7a 100644
--- a/src/plugins/loop_analysis/loop_analysis.ml
+++ b/src/plugins/loop_analysis/loop_analysis.ml
@@ -340,37 +340,18 @@ module Store(* (B:sig *)
Printer.pp_stmt stmt
let value_min_max stmt vi =
- if (Db.Value.is_computed ()) then
+ if (Eva.Analysis.is_computed ()) then
begin
Options.feedback ~dkey ~once:true
"value analysis computed, trying results";
- if Db.Value.is_reachable_stmt stmt then
- let state = Db.Value.get_stmt_state stmt in
- try
- let loc = Locations.loc_of_varinfo vi in
- let v = Db.Value.find state loc in
- let ival = Cvalue.V.project_ival v in
- let omin, omax = Ival.min_and_max ival in
- omin, omax
- with
- | Not_found ->
- Options.feedback ~dkey "value_min_max: not found: %a@.\
- function: %a, stmt: %a"
- Printer.pp_varinfo vi Kernel_function.pretty
- (Kernel_function.find_englobing_kf stmt) Printer.pp_stmt stmt;
- None, None
- | Cvalue.V.Not_based_on_null ->
- Options.feedback ~dkey "value_min_max: not based on null: %a@.\
- function: %a, stmt: %a"
- Printer.pp_varinfo vi Kernel_function.pretty
- (Kernel_function.find_englobing_kf stmt) Printer.pp_stmt stmt;
- None, None
- else
- begin
+ let value = Eva.Results.(before stmt |> eval_var vi |> as_ival) in
+ match value with
+ | Result.Ok ival -> Ival.min_and_max ival
+ | Error e ->
+ if e = Eva.Results.Bottom then
Options.feedback ~dkey "skipping unreachable stmt (function: %a)"
Kernel_function.pretty (Kernel_function.find_englobing_kf stmt);
- None, None
- end
+ None, None
end
else
begin
@@ -490,7 +471,7 @@ module Store(* (B:sig *)
with Not_found -> ()
end
| c ->
- if (Db.Value.is_computed ()) then
+ if (Eva.Analysis.is_computed ()) then
begin
let min_max_int = value_min_max stmt in
match c with
diff --git a/src/plugins/loop_analysis/tests/loop_analysis/oracle/with_value.res.oracle b/src/plugins/loop_analysis/tests/loop_analysis/oracle/with_value.res.oracle
index f2851d8cb74760ca575b38650701d31b54dcc5f9..b7db69d0c82a6d489540170eed6b3c41a2e97997 100644
--- a/src/plugins/loop_analysis/tests/loop_analysis/oracle/with_value.res.oracle
+++ b/src/plugins/loop_analysis/tests/loop_analysis/oracle/with_value.res.oracle
@@ -433,6 +433,10 @@
with_value.i:26: 5
with_value.i:30: 5
with_value.i:34: 4
+ with_value.i:38: 2147483648
+ with_value.i:42: 2147483649
+ with_value.i:46: 2147483649
+ with_value.i:50: 2147483648
with_value.i:54: 2147483646
with_value.i:58: 2147483647
with_value.i:62: 2147483647
diff --git a/src/plugins/markdown-report/eva_info.ml b/src/plugins/markdown-report/eva_info.ml
index 7c00cc4ae15e0e88f9a093f261341904dcb1994d..b0a59dc172472ee3f611be9e4c075057457e46ba 100644
--- a/src/plugins/markdown-report/eva_info.ml
+++ b/src/plugins/markdown-report/eva_info.ml
@@ -96,7 +96,7 @@ class eva_coverage_vis ~from_entry_point = object(self)
| Block _ | UnspecifiedSequence _ -> Cil.DoChildren
| _ ->
self#incr_total_stmts;
- if Db.Value.is_reachable_stmt s then self#incr_covered_stmts;
+ if Eva.Results.is_reachable s then self#incr_covered_stmts;
Cil.DoChildren
method! vinst i =
@@ -114,7 +114,7 @@ class eva_coverage_vis ~from_entry_point = object(self)
Cil.SkipChildren
| Call(_,{ enode = Lval (Mem _,NoOffset)},_,_) ->
let s = Option.get self#current_stmt in
- let kfs = Db.Value.call_to_kernel_function s in
+ let kfs = Eva.Results.callee s in
let handle_one kf =
let vi = Kernel_function.get_vi kf in
if not (Cil_datatype.Varinfo.Hashtbl.mem calls vi)
@@ -129,7 +129,7 @@ class eva_coverage_vis ~from_entry_point = object(self)
end
end
in
- Kernel_function.Hptset.iter handle_one kfs;
+ List.iter handle_one kfs;
Cil.SkipChildren
| _ -> Cil.SkipChildren (* No need to go further. *)
@@ -187,7 +187,7 @@ open Markdown
let coverage_md_gen () =
let main = Kernel.MainFunction.get () in
- !Db.Value.compute ();
+ Eva.Analysis.compute ();
let vis = new eva_coverage_vis ~from_entry_point:false in
let stats = vis#compute () in
let summary_whole =
diff --git a/src/plugins/metrics/metrics_coverage.ml b/src/plugins/metrics/metrics_coverage.ml
index ead657ccfe1122c0ac7ec88c2823ce2b5f0e9682..fad2d481a43a7c6b40a8e539bbe95b0b9d76a93e 100644
--- a/src/plugins/metrics/metrics_coverage.ml
+++ b/src/plugins/metrics/metrics_coverage.ml
@@ -215,7 +215,7 @@ class coverageByFun = object
method! vstmt s =
total <- total + 1;
- if Db.Value.is_reachable_stmt s then value <- value + 1;
+ if Eva.Results.is_reachable s then value <- value + 1;
Cil.DoChildren
method result = (total, value)
@@ -244,12 +244,12 @@ let compute_coverage_for kf =
with Kernel_function.No_Definition -> ()
let compute_coverage_by_fun () =
- if Db.Value.is_computed () && not (is_computed_by_fun ())
+ if Eva.Analysis.is_computed () && not (is_computed_by_fun ())
then
let libc = Metrics_parameters.Libc.get () in
Globals.Functions.iter
(fun kf ->
- if !Db.Value.is_called kf &&
+ if Eva.Results.is_called kf &&
Metrics_base.consider_function ~libc (Kernel_function.get_vi kf)
then compute_coverage_for kf)
@@ -264,12 +264,12 @@ let compute_syntactic ~libc kf =
let dkey_sem = Metrics_parameters.register_category "semantic-visitor"
let compute_semantic ~libc =
- assert (Db.Value.is_computed ());
+ assert (Eva.Analysis.is_computed ());
let res = ref Varinfo.Set.empty in
(* Just iter on all the functions and consult the appropriate table *)
Globals.Functions.iter
(fun kf ->
- if !Db.Value.is_called kf &&
+ if Eva.Results.is_called kf &&
Metrics_base.consider_function ~libc
(Kernel_function.get_vi kf)
then begin
@@ -360,7 +360,7 @@ class semantic_printer ~libc (cov_metrics : coverage_metrics) = object(self)
(* uses semantic *)
method pp_value_coverage fmt =
- assert (Db.Value.is_computed ());
+ assert (Eva.Analysis.is_computed ());
let all = self#all_funs in
let syntactic = cov_metrics.syntactic
and semantic = cov_metrics.semantic in
@@ -425,7 +425,7 @@ let percent_coverage ~libc cov_metrics =
;;
let compute ~libc =
- assert (Db.Value.is_computed ());
+ assert (Eva.Analysis.is_computed ());
let semantic = compute_semantic ~libc in
let main = fst (Globals.entry_point ()) in
let syntactic, initializers = compute_syntactic ~libc main in
diff --git a/src/plugins/metrics/register.ml b/src/plugins/metrics/register.ml
index 1ab4336a288ce79a1cc5a57321819fddc016c314..2ea7050327a6cdcfb61737a06a89477433d5ee13 100644
--- a/src/plugins/metrics/register.ml
+++ b/src/plugins/metrics/register.ml
@@ -47,8 +47,8 @@ let syntactic ?(libc=Metrics_parameters.Libc.get ()) () =
let () = ValueCoverage.set_output_dependencies [Db.Value.self; Libc.self]
let value ~libc () =
- !Db.Value.compute ();
- if Db.Value.is_computed () then begin
+ Eva.Analysis.compute ();
+ if Eva.Analysis.is_computed () then begin
let cov_metrics = Metrics_coverage.compute ~libc in
let cov_printer = new Metrics_coverage.semantic_printer ~libc cov_metrics in
Metrics_parameters.result "%t" cov_printer#pp_value_coverage;
diff --git a/src/plugins/metrics/register_gui.ml b/src/plugins/metrics/register_gui.ml
index ace660eb586bb41b196a5e55fe44b4344204e7a9..a75dd2ed93332dc3d996871daf9eacf801d58b61 100644
--- a/src/plugins/metrics/register_gui.ml
+++ b/src/plugins/metrics/register_gui.ml
@@ -146,7 +146,7 @@ module CyclomaticMetricsGUI = struct
end
method cyclo_selector (popup_factory:GMenu.menu GMenu.factory) main_ui ~button localizable =
- if button = 3 && Db.Value.is_computed () then
+ if button = 3 && Eva.Analysis.is_computed () then
match localizable with
| PVDecl (Some kf, _,_) ->
let callback1 () =
@@ -214,7 +214,7 @@ module ValueCoverageGUI = struct
begin
match !result with
| None ->
- !Db.Value.compute ();
+ Eva.Analysis.compute ();
result := Some (Metrics_coverage.compute ~libc)
| Some _ -> ()
end;
diff --git a/src/plugins/nonterm/nonterm_run.ml b/src/plugins/nonterm/nonterm_run.ml
index 23d5aa7635938046ba7d24391cc8e6bbdfb613d9..0cbfe74ffb31bddf7cf6a014fc1a8621187b7162 100644
--- a/src/plugins/nonterm/nonterm_run.ml
+++ b/src/plugins/nonterm/nonterm_run.ml
@@ -181,7 +181,7 @@ class unreachable_stmt_visitor kf to_ignore = object
method! vstmt stmt =
if Stmt.Hptset.mem stmt syntactically_reachable &&
- Db.Value.is_reachable_stmt stmt = false &&
+ not (Eva.Results.is_reachable stmt) &&
not (Stmt.Hptset.mem stmt !semantically_considered)
then begin
(* add node and its reachable successors to the considered statements *)
@@ -197,11 +197,10 @@ end
1. SyntacticallyUnreachable is disabled (otherwise it already checks them);
2. No warnings were emitted for the function (otherwise it may be redundant). *)
let check_unreachable_returns kf =
- let st = Db.Value.get_initial_state kf in
- if Db.Value.is_reachable st then begin
+ if Eva.Results.is_called kf then begin
try
let ret_stmt = Kernel_function.find_return kf in
- if not (Db.Value.is_reachable_stmt ret_stmt) then
+ if not (Eva.Results.is_reachable ret_stmt) then
warn_unreachable_statement ret_stmt
with
| Kernel_function.No_Statement -> (* should never happen *)
@@ -221,25 +220,24 @@ let check_unreachable_statements kf ~to_ignore ~dead_code ~warned_kfs =
considered as always terminating"
Kernel_function.pretty kf
else
- let st = Db.Value.get_initial_state kf in
- if Db.Value.is_reachable st then begin
- try
- let vis = new unreachable_stmt_visitor kf to_ignore in
+ if Eva.Results.is_called kf then begin
+ try
+ let vis = new unreachable_stmt_visitor kf to_ignore in
+ ignore (Visitor.visitFramacKf (vis :> Visitor.frama_c_visitor) kf);
+ if dead_code then begin
+ (* compute syntactically unreachable statements *)
+ let vis = new dead_cc_collector kf in
ignore (Visitor.visitFramacKf (vis :> Visitor.frama_c_visitor) kf);
- if dead_code then begin
- (* compute syntactically unreachable statements *)
- let vis = new dead_cc_collector kf in
- ignore (Visitor.visitFramacKf (vis :> Visitor.frama_c_visitor) kf);
- let cc_heads = List.map List.hd vis#get in
- Stmt.Hptset.iter (fun h -> warn_dead_code h) (Stmt.Hptset.of_list cc_heads)
- end
- else if not (Kernel_function.Set.mem kf warned_kfs) then
- check_unreachable_returns kf
- with
- | Kernel_function.No_Statement -> (* should never happen *)
- Self.error "function %a has no return statement, skipping"
- Kernel_function.pretty kf;
- end
+ let cc_heads = List.map List.hd vis#get in
+ Stmt.Hptset.iter (fun h -> warn_dead_code h) (Stmt.Hptset.of_list cc_heads)
+ end
+ else if not (Kernel_function.Set.mem kf warned_kfs) then
+ check_unreachable_returns kf
+ with
+ | Kernel_function.No_Statement -> (* should never happen *)
+ Self.error "function %a has no return statement, skipping"
+ Kernel_function.pretty kf;
+ end
(* To avoid redundant warnings, calls to possibly non-terminating functions
are ignored if:
@@ -281,14 +279,6 @@ class stmt_collector = object
method get_instr_stmts = List.rev !instr_stmts
end
-let get_callstack_state ~after stmt cs =
- match Db.Value.get_stmt_state_callstack ~after stmt with
- | None -> None (* unreachable stmt *)
- | Some table ->
- try
- Some (Value_types.Callstack.Hashtbl.find table cs)
- with Not_found -> None
-
(* collects the list of non-terminating instructions *)
let collect_nonterminating_statements fd nonterm_stacks =
let vis = new stmt_collector in
@@ -309,40 +299,23 @@ let collect_nonterminating_statements fd nonterm_stacks =
| _ ->
let source = fst (Stmt.loc stmt) in
Self.debug ~source "processing stmt:@ %a" Printer.pp_stmt stmt;
- match Db.Value.get_stmt_state_callstack ~after:false stmt with
- | None -> () (* unreachable stmt *)
- | Some before_table ->
- Value_types.Callstack.Hashtbl.iter
- (fun cs before_state ->
- try
- match Db.Value.get_stmt_state_callstack ~after:true stmt with
- | None -> (* no after table => non-terminating statement *)
- add_stack stmt cs
- | Some after_table ->
- let after_state =
- Value_types.Callstack.Hashtbl.find after_table cs
- in
- if Cvalue.Model.is_reachable before_state then
- if not (Cvalue.Model.is_reachable after_state) then add_stack stmt cs
- else if match stmt.skind with Loop _ -> true | _ -> false then begin
- (* special treatment for loops: even if their after state
- is reachable, we must check that at least one outgoing
- edge is reachable *)
- let out_edges = Stmts_graph.get_all_stmt_out_edges stmt in
- let all_out_edges_unreachable =
- List.for_all (fun (_, out_stmt) ->
- match get_callstack_state ~after:false out_stmt cs with
- | None -> true
- | Some state -> not (Cvalue.Model.is_reachable state)
- ) out_edges
- in
- if all_out_edges_unreachable then add_stack stmt cs
- end
- with
- | Not_found ->
- (* in this callstack, the statement is non-terminating *)
- add_stack stmt cs
- ) before_table
+ let process_callstack cs =
+ if Eva.Results.(after stmt |> in_callstack cs |> is_empty) then
+ add_stack stmt cs
+ else if match stmt.skind with Loop _ -> true | _ -> false then begin
+ (* special treatment for loops: even if their after state
+ is reachable, we must check that at least one outgoing
+ edge is reachable *)
+ let out_edges = Stmts_graph.get_all_stmt_out_edges stmt in
+ let all_out_edges_unreachable =
+ List.for_all (fun (_, out_stmt) ->
+ Eva.Results.(before out_stmt |> in_callstack cs |> is_empty)
+ ) out_edges
+ in
+ if all_out_edges_unreachable then add_stack stmt cs
+ end
+ in
+ List.iter process_callstack Eva.Results.(before stmt |> callstacks)
) vis#get_instr_stmts;
!new_nonterm_stmts
@@ -364,7 +337,7 @@ let cmp_callstacks cs1 cs2 =
let run () =
if not (Ast.is_computed ()) then
Self.abort "nonterm requires a computed AST";
- if not (Db.Value.is_computed ()) then
+ if not (Eva.Analysis.is_computed ()) then
Self.abort "nonterm requires a computed value analysis";
Self.debug "Starting analysis...";
let file = Ast.get () in
@@ -398,7 +371,7 @@ let run () =
Self.feedback ~level:2 "Analysis done."
;;
-let run_once, _ = State_builder.apply_once "Nonterm.run" [Db.Value.self] run
+let run_once, _ = State_builder.apply_once "Nonterm.run" [Eva.Analysis.self] run
let main () =
if Enabled.get () then run_once ()
diff --git a/src/plugins/occurrence/register.ml b/src/plugins/occurrence/register.ml
index 8d9d94741ec37ce7bf37449cc19674c8fc73cc66..5e6922a3562dd445f1ea22a8ace1b3468dfeb956 100644
--- a/src/plugins/occurrence/register.ml
+++ b/src/plugins/occurrence/register.ml
@@ -106,8 +106,8 @@ class occurrence = object (self)
method! vlval lv =
let ki = self#current_kinstr in
- if Db.Value.is_accessible ki then begin
- let z = !Db.Value.lval_to_zone ki lv in
+ begin
+ let z = Eva.Results.(before_kinstr ki |> eval_address lv |> as_zone) in
try
Locations.Zone.fold_topset_ok
(fun b _ () ->
@@ -135,7 +135,7 @@ class occurrence = object (self)
Db.yield ();
super#vstmt_aux s
- initializer !Db.Value.compute ()
+ initializer Eva.Analysis.compute ()
end
diff --git a/src/plugins/pdg/build.ml b/src/plugins/pdg/build.ml
index e90ada08bba331ce0f7190093d8c7d5c56d9630f..6606cbf535d5975bc4349e6bcb4776f34b94dbba 100644
--- a/src/plugins/pdg/build.ml
+++ b/src/plugins/pdg/build.ml
@@ -1000,7 +1000,7 @@ let degenerated top kf =
if top then PdgTypes.Pdg.top kf else PdgTypes.Pdg.bottom kf
let compute_pdg kf =
- if not (Db.Value.is_computed ()) then !Db.Value.compute ();
+ if not (Eva.Analysis.is_computed ()) then Eva.Analysis.compute ();
Pdg_parameters.feedback "computing for function %a" Kernel_function.pretty kf;
try
if is_variadic kf then
diff --git a/src/plugins/pdg/register.ml b/src/plugins/pdg/register.ml
index 5add8915f1cf8f77a1573dab0f468e71c1755c6f..0c1ae27625fcf632d968f3e545e48dc454891480 100644
--- a/src/plugins/pdg/register.ml
+++ b/src/plugins/pdg/register.ml
@@ -127,7 +127,7 @@ let compute_for_kf kf =
Kernel_function.Set.mem kf (Pdg_parameters.BuildFct.get ())
let compute () =
- !Db.Value.compute ();
+ Eva.Analysis.compute ();
let do_kf_pdg kf =
if compute_for_kf kf then
let pdg = !Db.Pdg.get kf in
diff --git a/src/plugins/postdominators/compute.ml b/src/plugins/postdominators/compute.ml
index d0b257ac9a65ef5759a2b9b9e935fca9701bde32..08cb906feaae05998b2d14113dc8195620ee6913 100644
--- a/src/plugins/postdominators/compute.ml
+++ b/src/plugins/postdominators/compute.ml
@@ -255,7 +255,7 @@ let () = Db.Main.extend output
include
PostDomDb
(struct
- let is_accessible = Db.Value.is_reachable_stmt
+ let is_accessible = Eva.Results.is_reachable
let dependencies = [ Db.Value.self ]
let name = "value"
let eval_cond stmt _e =
diff --git a/src/plugins/reduc/hyp.ml b/src/plugins/reduc/hyp.ml
index fc4fabf2763c7db2b26efafaf8ff26481de7d763..478be2e40ea72324d85484a651060284bec8d474 100644
--- a/src/plugins/reduc/hyp.ml
+++ b/src/plugins/reduc/hyp.ml
@@ -20,9 +20,9 @@
(* *)
(**************************************************************************)
-let pred_opt_from_expr_state state e =
+let pred_opt_from_expr_state stmt e =
try
- Value2acsl.lval_to_predicate state e
+ Value2acsl.lval_to_predicate stmt e
with
| Cvalue.V.Not_based_on_null ->
Misc.not_implemented ~what:"Value not based on null";
@@ -36,12 +36,11 @@ class hypotheses_visitor (env: Collect.env) = object(self)
method! vstmt_aux stmt =
let kf = Option.get (self#current_kf) in
- let state = Db.Value.get_stmt_state stmt in
if Collect.should_annotate_stmt env stmt then begin
let vars = Collect.get_relevant_vars_stmt env kf stmt in
List.iter
(fun e ->
- let p_opt = pred_opt_from_expr_state state e in
+ let p_opt = pred_opt_from_expr_state stmt e in
Option.iter (Misc.assert_and_validate ~kf stmt) p_opt)
vars
end;
diff --git a/src/plugins/reduc/value2acsl.ml b/src/plugins/reduc/value2acsl.ml
index c91d1ba6992418ffebcea1371b2b587aa9d5ea36..e5201a791ccb73bde0919c6831745d8c63026293 100644
--- a/src/plugins/reduc/value2acsl.ml
+++ b/src/plugins/reduc/value2acsl.ml
@@ -165,15 +165,13 @@ let value_to_predicate_opt ?(loc=Location.unknown) t v =
with
| Not_based_on_null -> (* base_offsets_to_predicate ~loc t m *) None
-let exp_to_predicate ?(loc=Location.unknown) state e =
- let value = !Db.Value.eval_expr ~with_alarms:CilE.warn_none_mode state e in
+let exp_to_predicate ?(loc=Location.unknown) stmt e =
+ let value = Eva.Results.(before stmt |> eval_exp e |> as_ival) in
let te = Logic_utils.expr_to_term ~coerce:false e in
- value_to_predicate_opt ~loc te value
+ Option.bind (Result.to_option value) (ival_to_predicate_opt ~loc te)
-let lval_to_predicate ?(loc=Location.unknown) state lv =
- let value = snd(!Db.Value.eval_lval
- ~with_alarms:CilE.warn_none_mode None state lv)
- in
+let lval_to_predicate ?(loc=Location.unknown) stmt lv =
+ let value = Eva.Results.(before stmt |> eval_lval lv |> as_ival) in
let e = Cil.new_exp ~loc (Lval lv) in
let te = Logic_utils.expr_to_term ~coerce:false e in
- value_to_predicate_opt ~loc te value
+ Option.bind (Result.to_option value) (ival_to_predicate_opt ~loc te)
diff --git a/src/plugins/reduc/value2acsl.mli b/src/plugins/reduc/value2acsl.mli
index 17546299c2191a9c2c5ea076b463904ccd48ed60..e69aca30b89ac9004dd0ffb548e7ec90d547b8a2 100644
--- a/src/plugins/reduc/value2acsl.mli
+++ b/src/plugins/reduc/value2acsl.mli
@@ -27,5 +27,5 @@ open Cil_types
@return None if no such predicate can be created. *)
val value_to_predicate_opt: ?loc:location -> term -> Cvalue.V.t -> predicate option
-val lval_to_predicate: ?loc:location -> Cvalue.Model.t -> lval -> predicate option
-val exp_to_predicate: ?loc:location -> Cvalue.Model.t -> exp -> predicate option
+val lval_to_predicate: ?loc:location -> stmt -> lval -> predicate option
+val exp_to_predicate: ?loc:location -> stmt -> exp -> predicate option
diff --git a/src/plugins/scope/datascope.ml b/src/plugins/scope/datascope.ml
index 26d5806673e8aca286bbdc294cd813dc5c2202cd..0e73269b8718a1fd4af65e9bbfb5d1a7da83a342 100644
--- a/src/plugins/scope/datascope.ml
+++ b/src/plugins/scope/datascope.ml
@@ -80,53 +80,44 @@ module InitSid = struct
Format.fprintf fmt "Lmap = %a@\n" LM.pretty lmap
end
-let get_lval_zones ~for_writing stmt lval =
- let state = Db.Value.get_stmt_state stmt in
- let dpds, zone, exact =
- !Db.Value.lval_to_zone_with_deps_state
- state ~deps:(Some Locations.Zone.bottom) ~for_writing lval
- in
- dpds, exact, zone
+let get_writes stmt lval =
+ Eva.Results.(before stmt |> eval_address lval |> as_zone ~access:Write)
(** Add to [stmt] to [lmap] for all the locations modified by the statement.
* Something to do only for calls and assignments.
* *)
let register_modified_zones lmap stmt =
let register lmap zone = InitSid.add_zone lmap zone stmt in
- let aux_out kf out =
+ let aux_out out kf =
let inout= !Db.Operational_inputs.get_internal_precise ~stmt kf in
Locations.Zone.join out inout.Inout_type.over_outputs
in
match stmt.skind with
| Instr (Set (lval, _, _)) ->
- let _dpds, _, zone =
- get_lval_zones ~for_writing:true stmt lval
- in
+ let zone = get_writes stmt lval in
register lmap zone
| Instr (Local_init(v, i, _)) ->
- let _, _, zone = get_lval_zones ~for_writing:true stmt (Cil.var v) in
+ let zone = get_writes stmt (Cil.var v) in
let lmap_init = register lmap zone in
(match i with
| AssignInit _ -> lmap_init
| ConsInit(f,_,_) ->
let kf = Globals.Functions.get f in
- let out = aux_out kf Locations.Zone.bottom in
+ let out = aux_out Locations.Zone.bottom kf in
register lmap_init out)
| Instr (Call (dst,funcexp,_args,_)) ->
begin
let lmap = match dst with
| None -> lmap
| Some lval ->
- let _dpds, _, zone =
- get_lval_zones ~for_writing:true stmt lval
- in
+ let zone = get_writes stmt lval in
register lmap zone
in
- let _, kfs =
- !Db.Value.expr_to_kernel_function ~deps:None (Kstmt stmt) funcexp
+ let kfs =
+ Eva.Results.(before stmt |> eval_callee funcexp |> default [])
in
let out =
- Kernel_function.Hptset.fold aux_out kfs Locations.Zone.bottom
+ List.fold_left aux_out Locations.Zone.bottom kfs
in
register lmap out
end
@@ -141,7 +132,7 @@ let compute kf =
let f = Kernel_function.get_definition kf in
let do_stmt lmap s =
Cil.CurrentLoc.set (Cil_datatype.Stmt.loc s);
- if Db.Value.is_reachable_stmt s
+ if Eva.Results.is_reachable s
then register_modified_zones lmap s
else lmap
in
@@ -361,7 +352,9 @@ let compute_escaping_zones s1 s2 =
let bases = List.fold_left filter Base.Hptset.empty locals in
if Base.Hptset.is_empty bases
then Locations.Zone.bottom
- else gather_escaping_zones bases (Db.Value.get_stmt_state s1)
+ else
+ let cvalue_state = Eva.Results.(before s1 |> get_cvalue_model) in
+ gather_escaping_zones bases cvalue_state
(* type pair_stmts = stmt * stmt *)
module PairStmts =
@@ -392,7 +385,7 @@ module ModifEdge =
Cil_state_builder.Kernel_function_hashtbl(HashPairStmtsZone)
(struct
let name = "Scope.Datatscope.ModifsEdge"
- let dependencies = [Db.Value.self]
+ let dependencies = [Eva.Analysis.self]
let size = 16
end)
@@ -410,9 +403,7 @@ let is_modified_by_edge kf z s1 s2 =
* @raise Kernel_function.No_Definition if [kf] has no definition
*)
let get_data_scope_at_stmt kf stmt lval =
- let dpds, _, zone = get_lval_zones ~for_writing:false stmt lval in
- (* TODO : is there something to do with 'exact' ? *)
- let zone = Locations.Zone.join dpds zone in
+ let zone = Eva.Results.(before stmt |> lval_deps lval) in
let allstmts, info = compute kf in
let modif_stmts = InitSid.find info zone in
let modifs_edge = is_modified_by_edge kf zone in
@@ -594,7 +585,7 @@ class check_annot_visitor = object(self)
method! vglob_aux g = match g with
| GFun (fdec, _loc) when
- !Db.Value.is_called (Option.get self#current_kf) &&
+ Eva.Results.is_called (Option.get self#current_kf) &&
not (!Db.Value.no_results fdec)
->
Cil.DoChildren
diff --git a/src/plugins/scope/datascope.mli b/src/plugins/scope/datascope.mli
index b34a8589757f06d20c613002c3b5d11828773d93..9b93221fe4f37e443f12a2981aeb04a80965eb44 100644
--- a/src/plugins/scope/datascope.mli
+++ b/src/plugins/scope/datascope.mli
@@ -37,9 +37,3 @@ val rm_asserts : unit -> unit
(** for internal use *)
module R: Plugin.General_services
-
-val get_lval_zones:
- for_writing:bool ->
- Cil_types.stmt ->
- Cil_types.lval ->
- Locations.Zone.t * bool * Locations.Zone.t
diff --git a/src/plugins/scope/defs.ml b/src/plugins/scope/defs.ml
index 565500c763b879c05749244de1dfb148edbbf699..af1e23d78388266822ed34f6e8bbad847c6ef558 100644
--- a/src/plugins/scope/defs.ml
+++ b/src/plugins/scope/defs.ml
@@ -62,10 +62,8 @@ let rec add_callee_nodes z acc nodes =
(fun node acc2 ->
match !Db.Pdg.node_key node with
| PdgIndex.Key.SigCallKey (cid, PdgIndex.Signature.Out out_key) ->
- let callees =
- Db.Value.call_to_kernel_function (PdgIndex.Key.call_from_id cid)
- in
- Kernel_function.Hptset.fold (fun kf (new_nodes, acc) ->
+ let callees = Eva.Results.callee (PdgIndex.Key.call_from_id cid) in
+ List.fold_left (fun (new_nodes, acc) kf ->
let callee_pdg = !Db.Pdg.get kf in
let outputs = match out_key with
| PdgIndex.Signature.OutLoc out ->
@@ -78,8 +76,8 @@ let rec add_callee_nodes z acc nodes =
in
let outputs = List.map fst outputs in
add_list_to_set outputs new_nodes, add_list_to_set outputs acc)
- callees
acc2
+ callees
| _ -> acc2)
nodes
(NSet.empty, acc)
@@ -134,7 +132,7 @@ let rec add_caller_nodes z kf acc (undef, nodes) =
let acc_undef, caller_nodes =
List.fold_left (add_one_call_nodes pdg) (None, NSet.empty) stmts
in add_caller_nodes z kf (NSet.union caller_nodes acc) (acc_undef, caller_nodes)
- in List.fold_left add_one_caller_nodes acc (!Db.Value.callers kf)
+ in List.fold_left add_one_caller_nodes acc (Eva.Results.callsites kf)
let compute_aux kf stmt zone =
debug1 "[Defs.compute] for %a at sid:%d in '%a'@."
@@ -168,9 +166,9 @@ let compute kf stmt lval =
let defs = NSet.fold add_node nodes Stmt.Hptset.empty in
(defs, undef)
in
- !Db.Value.compute ();
- let zone = !Db.Value.lval_to_zone (Kstmt stmt) lval in
- Option.map extract (compute_aux kf stmt zone)
+ Eva.Analysis.compute ();
+ let zone = Eva.Results.(before stmt |> eval_address lval |> as_zone) in
+ compute_aux kf stmt zone |> Option.map extract
(* Variation of the function above. For each PDG node that has been found,
we find whether it directly modifies [zone] through an affectation
@@ -219,8 +217,10 @@ let compute_with_def_type_zone kf stmt zone =
Option.map extract (compute_aux kf stmt zone)
let compute_with_def_type kf stmt lval =
- !Db.Value.compute ();
- let zone = !Db.Value.lval_to_zone (Kstmt stmt) lval in
+ Eva.Analysis.compute ();
+ let zone =
+ Eva.Results.(before stmt |> eval_address lval |> as_zone)
+ in
compute_with_def_type_zone kf stmt zone
(*~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~*)
diff --git a/src/plugins/scope/dpds_gui.ml b/src/plugins/scope/dpds_gui.ml
index d9d87225b1b4a4361133aa4d48040a91fff153fc..b3798da4e558840c00d2d51e005b3c92c503f5b8 100644
--- a/src/plugins/scope/dpds_gui.ml
+++ b/src/plugins/scope/dpds_gui.ml
@@ -114,7 +114,7 @@ struct include State_builder.Ref
(Stmt.Hptset)
(struct
let name = Info.name
- let dependencies = [ Db.Value.self ]
+ let dependencies = [ Eva.Analysis.self ]
let default () = Stmt.Hptset.empty
end)
@@ -137,7 +137,7 @@ struct
(Stmt.Map.Make(Datatype.String.Set))
(struct
let name = Info.name
- let dependencies = [ Db.Value.self ]
+ let dependencies = [ Eva.Analysis.self ]
let default () = Stmt.Map.empty
end)
@@ -222,7 +222,7 @@ module Pscope (* : (DpdCmdSig with type t_in = code_annotation) *) = struct
(Code_annotation)
(struct
let name = "Dpds_gui.Highlighter.Pscope_warn"
- let dependencies = [ Db.Value.self ]
+ let dependencies = [ Eva.Analysis.self ]
end)
let clear () = Pscope.clear(); Pscope_warn.clear()
@@ -323,7 +323,7 @@ module Zones : (DpdCmdSig with type t_in = lval) = struct
(Stmt.Hptset))
(struct
let name = "Dpds_gui.Highlighter.ZonesState"
- let dependencies = [ Db.Value.self ]
+ let dependencies = [ Eva.Analysis.self ]
end)
let set s =
set s;
@@ -392,7 +392,7 @@ module DpdsState =
(Stmt)
(struct
let name = "Dpds_gui.Highlighter.DpdsState"
- let dependencies = [ Db.Value.self ]
+ let dependencies = [ Eva.Analysis.self ]
end)
let reset () =
@@ -469,7 +469,7 @@ let highlighter (buffer:Design.reactive_buffer) localizable ~start ~stop =
with Not_found -> ()
let check_value (main_ui:Design.main_window_extension_points) =
- if Db.Value.is_computed () then true
+ if Eva.Analysis.is_computed () then true
else
let answer = GToolbox.question_box
~title:("Eva Needed")
@@ -478,7 +478,7 @@ let check_value (main_ui:Design.main_window_extension_points) =
^"Do you want to run Eva with its current settings now?")
in
if answer = 1 then
- match main_ui#full_protect ~cancelable:true !Db.Value.compute with
+ match main_ui#full_protect ~cancelable:true Eva.Analysis.compute with
| Some _ ->
main_ui#redisplay (); (* New alarms *)
true
diff --git a/src/plugins/scope/zones.ml b/src/plugins/scope/zones.ml
index 9a9e18e7c26c5060b93725f7bbc5c1ca7964ea13..938b3630758808c5697d4bda0560436832efdff9 100644
--- a/src/plugins/scope/zones.ml
+++ b/src/plugins/scope/zones.ml
@@ -64,6 +64,14 @@ let compute_new_data old_zone l_zone l_dpds exact r_dpds =
(true, zone)
else (false, old_zone)
+let get_lval_zones ~for_writing stmt lval =
+ let state = Db.Value.get_stmt_state stmt in
+ let dpds, zone, exact =
+ !Db.Value.lval_to_zone_with_deps_state
+ state ~deps:(Some Locations.Zone.bottom) ~for_writing lval
+ in
+ dpds, exact, zone
+
(* the call result can be processed like a normal assignment *)
let process_call_res data stmt lvaloption froms =
let data = match lvaloption with
@@ -73,7 +81,7 @@ let process_call_res data stmt lvaloption froms =
let r_dpds = Function_Froms.Memory.collapse_return ret_dpds in
let r_dpds = Function_Froms.Deps.to_zone r_dpds in
let l_dpds, exact, l_zone =
- Datascope.get_lval_zones ~for_writing:true stmt lval in
+ get_lval_zones ~for_writing:true stmt lval in
compute_new_data data l_zone l_dpds exact r_dpds
in data
@@ -144,20 +152,20 @@ let process_one_call data stmt lvaloption froms =
used, data
let process_call data_after stmt lvaloption funcexp args _loc =
- let funcexp_dpds, called_functions =
- !Db.Value.expr_to_kernel_function
- (Kstmt stmt) ~deps:(Some Data.bottom) funcexp
+ let funcexp_dpds = Eva.Results.(before stmt |> expr_deps funcexp)
+ and called_functions =
+ Eva.Results.(before stmt |> eval_callee funcexp |> default [])
in
let used, data =
try
let froms = !Db.From.Callwise.find (Kstmt stmt) in
process_one_call data_after stmt lvaloption froms
with Not_found -> (* don't have callwise (-calldeps option) *)
- let do_call kf acc =
+ let do_call acc kf =
(* notice that we use the same old data for each possible call *)
(process_one_call data_after stmt lvaloption (!Db.From.get kf))::acc
in
- let l = Kernel_function.Hptset.fold do_call called_functions [] in
+ let l = List.fold_left do_call [] called_functions in
(* in l, we have one result for each possible function called *)
List.fold_left
(fun (acc_u,acc_d) (u,d) -> (acc_u || u), Data.merge acc_d d)
@@ -167,10 +175,9 @@ let process_call data_after stmt lvaloption funcexp args _loc =
if used then
let data =
(* no problem of order because parameters are disjoint for sure *)
- Kernel_function.Hptset.fold
- (fun kf data -> process_call_args data kf stmt args)
- called_functions
- data
+ List.fold_left
+ (fun data kf -> process_call_args data kf stmt args)
+ data called_functions
in
let data = Data.merge funcexp_dpds data in
used, data
@@ -213,7 +220,7 @@ module Computer (Param:sig val states : Ctx.t end) = struct
let do_assign stmt lval exp data =
let l_dpds, exact, l_zone =
- Datascope.get_lval_zones ~for_writing:true stmt lval in
+ get_lval_zones ~for_writing:true stmt lval in
let r_dpds = Data.exp_zone stmt exp in
let used, data = compute_new_data data l_zone l_dpds exact r_dpds in
let _ = if used then add_used_stmt stmt in
@@ -299,7 +306,7 @@ let compute_ctrl_info pdg ctrl_part used_stmts =
let compute kf stmt lval =
let f = Kernel_function.get_definition kf in
let dpds, _exact, zone =
- Datascope.get_lval_zones ~for_writing:false stmt lval in
+ get_lval_zones ~for_writing:false stmt lval in
let zone = Data.merge dpds zone in
debug1 "[zones] build for %a before %d in %a@\n"
Data.pretty zone stmt.sid Kernel_function.pretty kf;
diff --git a/src/plugins/security_slicing/components.ml b/src/plugins/security_slicing/components.ml
index af605036f174476ed91396a80eb74727be868928..4db3c3d87d9f68ba386df5c377ea29bd926f9e78 100644
--- a/src/plugins/security_slicing/components.ml
+++ b/src/plugins/security_slicing/components.ml
@@ -398,7 +398,7 @@ module Component = struct
todolist
callsites)
todolist
- (!Db.Value.callers kf)
+ (Eva.Results.callsites kf)
let related_nodes_of_nodes kind result nodes =
let initial_nodes =
@@ -460,7 +460,7 @@ module Component = struct
in
List.fold_left do_call todolist callsites
in
- List.fold_left do_caller todolist (!Db.Value.callers kf)
+ List.fold_left do_caller todolist (Eva.Results.callsites kf)
| _ ->
todolist
in
@@ -502,11 +502,7 @@ module Component = struct
todolist
else
let stmt = Key.call_from_id id in
- let called_kfs =
- Kernel_function.Hptset.elements
- (try Db.Value.call_to_kernel_function stmt
- with Db.Value.Not_a_call -> assert false)
- in
+ let called_kfs = Eva.Results.callee stmt in
let todolist =
List.fold_left
(fun todolist called_kf ->
@@ -629,7 +625,7 @@ module Component = struct
~level:3 "computing initial nodes for %d" stmt.sid;
let pdg = !Db.Pdg.get kf in
let nodes =
- if Db.Value.is_reachable_stmt stmt then
+ if Eva.Results.is_reachable stmt then
try !Db.Pdg.find_simple_stmt_nodes pdg stmt
with Not_found -> assert false
else begin
diff --git a/src/plugins/slicing/api.ml b/src/plugins/slicing/api.ml
index 3ece47ef72315659e3f2c4756382c7912a072c2a..13b39597d7dac0e6acfd53fbd6011bf9679978a6 100644
--- a/src/plugins/slicing/api.ml
+++ b/src/plugins/slicing/api.ml
@@ -413,10 +413,9 @@ module Slice = struct
let get_called_funcs ff stmt =
match stmt.skind with
- | Instr (Call (_,expr_f,_,_)) ->
+ | Instr (Call _) ->
if snd (Fct_slice.get_called_slice ff stmt) then
- Kernel_function.Hptset.elements
- (snd (!Db.Value.expr_to_kernel_function (Kstmt stmt) ~deps:None expr_f))
+ Eva.Results.callee stmt
else
[]
| Instr (Local_init (_, ConsInit (f, _, _), _)) -> [ Globals.Functions.get f ]
diff --git a/src/plugins/slicing/fct_slice.ml b/src/plugins/slicing/fct_slice.ml
index 47d922e5bb064d78c4ae8b3c1baacae9bf839769..22285f900b9f9a04bf5aa331cdbef9bd32c215b2 100644
--- a/src/plugins/slicing/fct_slice.ml
+++ b/src/plugins/slicing/fct_slice.ml
@@ -54,9 +54,7 @@ let exists_fun_callers fpred kf =
then false (* no way to call the initial [kf]. *)
else begin
table := Kernel_function.Set.add kf !table ;
- List.exists
- (fun (kf,_) -> exists_fun_callers kf)
- (!Db.Value.callers kf)
+ List.exists exists_fun_callers (Eva.Results.callers kf)
end
in
exists_fun_callers kf
@@ -146,16 +144,7 @@ end = struct
let indirectly_called_src_functions call_id =
let _, stmt = call_id in
- let funcexp = match stmt.skind with
- | Instr (Call (_,funcexp,_,_)) -> funcexp
- | Instr (Local_init (_, ConsInit (f, _, _), _)) -> Cil.evar f
- | _ -> assert false
- in
- let _, called_functions =
- !Db.Value.expr_to_kernel_function
- (Kstmt stmt) ~deps:(Some Locations.Zone.bottom) funcexp
- in
- Kernel_function.Hptset.elements called_functions
+ Eva.Results.callee stmt
(** [call_id] is a call to [g] in [f].
* we don't want [f] to call [g] anymore, so we have to update [g] [called_by]
@@ -1463,12 +1452,11 @@ let merge_fun_callers get_list get_value merge is_top acc kf =
raise StopMerging (* acceleration when top is reached *)
in
let rec merge_fun_callers kf =
- let merge_fun_caller (kf,_) = merge_fun_callers kf in
let vf = Kernel_function.get_vi kf in
if not (Cil_datatype.Varinfo.Set.mem vf !table) then begin
table := Cil_datatype.Varinfo.Set.add vf !table ;
List.iter (fun x -> merge (get_value x)) (get_list kf) ;
- List.iter merge_fun_caller (!Db.Value.callers kf)
+ List.iter merge_fun_callers (Eva.Results.callers kf)
end
(* else no way to add something, the [kf] contribution is already
accumulated. *)
diff --git a/src/plugins/slicing/printSlice.ml b/src/plugins/slicing/printSlice.ml
index 63986e183ebb85760f6c4a16023d4139946f9927..9c5bd9baed6a1c0a0d18839fdf42c04c818018b5 100644
--- a/src/plugins/slicing/printSlice.ml
+++ b/src/plugins/slicing/printSlice.ml
@@ -204,10 +204,10 @@ module PrintProject = struct
let iter_edges_src_fun f =
let do_kf_calls kf =
let fi = SlicingMacros.get_kf_fi kf in
- let doit (kf_caller,_) =
+ let doit kf_caller =
let fi_caller = SlicingMacros.get_kf_fi kf_caller in
f ((Src fi_caller, Src fi), None)
- in List.iter doit (!Db.Value.callers kf)
+ in List.iter doit (Eva.Results.callers kf)
in
Globals.Functions.iter do_kf_calls
diff --git a/src/plugins/slicing/register.ml b/src/plugins/slicing/register.ml
index 3f32606a217928ce557bfcc06f7d7b5c98c0dbea..4166762d3cc86694daf02f82b23262376cb39f89 100644
--- a/src/plugins/slicing/register.ml
+++ b/src/plugins/slicing/register.ml
@@ -27,7 +27,7 @@ let main () =
(* have to do the value analysis before the selections
* because some functions use its results,
* and the value analysis is not launched automatically. *)
- !Db.Value.compute ();
+ Eva.Analysis.compute ();
let project_name = SlicingParameters.ProjectName.get () in
Api.Project.reset_slicing ();
diff --git a/src/plugins/slicing/register_gui.ml b/src/plugins/slicing/register_gui.ml
index 0650a8a5d7d4ec67b06399f6dc4e4f0420060acc..92251b205bb8a73540f113861d13586c14e7b284 100644
--- a/src/plugins/slicing/register_gui.ml
+++ b/src/plugins/slicing/register_gui.ml
@@ -92,7 +92,7 @@ let msg_help_libraries =
undefined functions."
let check_value_computed (main_ui:Design.main_window_extension_points) =
- if Db.Value.is_computed () then true
+ if Eva.Analysis.is_computed () then true
else
let answer = GToolbox.question_box
~title:("Eva Needed")
@@ -102,7 +102,7 @@ let check_value_computed (main_ui:Design.main_window_extension_points) =
^"Do you want to run Eva with its current settings now?")
in
if answer = 1 then
- match main_ui#full_protect ~cancelable:true !Db.Value.compute with
+ match main_ui#full_protect ~cancelable:true Eva.Analysis.compute with
| Some _ ->
main_ui#redisplay (); (* New alarms *)
true
@@ -116,7 +116,7 @@ let gui_apply_action (main_ui:Design.main_window_extension_points) f x ~info =
let slicing_selector (popup_factory:GMenu.menu GMenu.factory)
(main_ui:Design.main_window_extension_points) ~button localizable =
- if (not (Db.Value.is_computed ()))
+ if (not (Eva.Analysis.is_computed ()))
then
ignore
(popup_factory#add_item "Enable _slicing"
@@ -126,7 +126,7 @@ let slicing_selector (popup_factory:GMenu.menu GMenu.factory)
Enabled.set true;
!update_column `Visibility
in
- if (not (Db.Value.is_computed ())) then begin
+ if (not (Eva.Analysis.is_computed ())) then begin
if check_value_computed main_ui then enable ()
end
else enable ()
@@ -344,7 +344,7 @@ let slicing_selector (popup_factory:GMenu.menu GMenu.factory)
in
let some_kf_from_vi vi =
try let kf = Globals.Functions.get vi in
- if !Db.Value.is_called kf then Some kf else None
+ if Eva.Results.is_called kf then Some kf else None
with Not_found -> None in
let some_kf_from_lv lv =
match lv with
@@ -352,7 +352,7 @@ let slicing_selector (popup_factory:GMenu.menu GMenu.factory)
| _ -> None
in
let some_kf_ki_lv kf stmt lvopt =
- if !Db.Value.is_called kf && Db.Value.is_reachable_stmt stmt
+ if Eva.Results.is_called kf && Eva.Results.is_reachable stmt
then Some (kf, stmt, lvopt) else None
in
begin (* add menu for slicing and scope plug-in *)
@@ -386,7 +386,7 @@ let slicing_highlighter(buffer:Design.reactive_buffer) localizable ~start ~stop=
let highlight () =
let buffer = buffer#buffer in
let ki = Pretty_source.ki_of_localizable localizable in
- if Db.Value.is_accessible ki then
+ if Eva.Results.is_reachable_kinstr ki then
let unused_code_area =
Gtk_helper.make_tag buffer
~name:"slicing_unused" [`STRIKETHROUGH true ]
@@ -443,7 +443,7 @@ let slicing_highlighter(buffer:Design.reactive_buffer) localizable ~start ~stop=
end
in
let tag_stmt kf stmt pb pe =
- assert (Db.Value.is_reachable_stmt stmt) ;
+ assert (Eva.Results.is_reachable stmt) ;
apply_on_one_project_and_merge_slices
kf
pb
@@ -554,7 +554,7 @@ let slicing_panel (main_ui:Design.main_window_extension_points) =
(gui_set_slicing_level main_ui)
in
let refresh () =
- let value_is_computed = Db.Value.is_computed () in
+ let value_is_computed = Eva.Analysis.is_computed () in
let enabled = Enabled.get () in
enabled_button#misc#set_sensitive value_is_computed ;
slice_undef_button#misc#set_sensitive enabled ;
diff --git a/src/plugins/slicing/slicingCmds.ml b/src/plugins/slicing/slicingCmds.ml
index 79b59cc0fd5ac7c7124e56e0f1517303def29d20..8340d52e18cffd804ca5e09c873a6bfa1d634920 100644
--- a/src/plugins/slicing/slicingCmds.ml
+++ b/src/plugins/slicing/slicingCmds.ml
@@ -55,6 +55,10 @@ let apply_all ~propagate_to_callers =
let get_select_kf (fvar, _select) = Globals.Functions.get fvar
+let get_lval_zone ?(access=Locations.Read) stmt lval =
+ let open Eva.Results in
+ before stmt |> eval_address lval |> as_zone ~access
+
(** Utilities for [kinstr]. *)
module Kinstr: sig
val iter_from_func : (stmt -> unit) -> kernel_function -> unit
@@ -71,17 +75,14 @@ struct
* i.e. directly means when [ki] is a call,
it doesn't don't look at the assigns clause of the called function. *)
let get_rw_zone stmt = (* returns [Zone.t read],[Zone.t written] *)
- assert (Db.Value.is_computed ());
+ assert (Eva.Analysis.is_computed ());
let lval_process read_zone stmt lv =
(* returns [read_zone] joined to [Zone.t read] by [lv], [Zone.t written] by [lv] *)
(* The modified locations are [looking_for], those address are
function of [deps]. *)
- let state = Db.Value.get_stmt_state stmt in
- let deps, zloc, _exact =
- !Db.Value.lval_to_zone_with_deps_state
- state ~deps:(Some read_zone) ~for_writing:true lv
- in
- deps, zloc
+ let zloc = get_lval_zone ~access:Locations.Write stmt lv in
+ let deps = Eva.Results.(before stmt |> address_deps lv) in
+ Locations.Zone.join read_zone deps, zloc
in
let call_process lv f args _loc =
(* returns [Zone.t read] by [lv, f, args], [Zone.t written] by [lv] *)
@@ -184,8 +185,8 @@ let select_entry_point_and_some_inputs_outputs set ~mark kf ~return ~outputs ~in
add_to_selection set selection
in if ((Locations.Zone.equal Locations.Zone.bottom outputs) && not return) ||
(try
- let ki = Kernel_function.find_return kf
- in if Db.Value.is_reachable_stmt ki then
+ let stmt = Kernel_function.find_return kf
+ in if Eva.Results.is_reachable stmt then
false
else
begin
@@ -210,8 +211,8 @@ let select_entry_point_and_some_inputs_outputs set ~mark kf ~return ~outputs ~in
(* apply [select ~spare] on each callsite of [kf] and add the returned selection
to [set]. *)
let generic_select_func_calls select_stmt set ~spare kf =
- assert (Db.Value.is_computed ());
- let callers = !Db.Value.callers kf in
+ assert (Eva.Analysis.is_computed ());
+ let callers = Eva.Results.callsites kf in
let select_calls acc (caller, stmts) =
List.fold_left (fun acc s -> select_stmt acc ~spare s caller) acc stmts
in
@@ -245,7 +246,7 @@ let select_func_calls_to set ~spare kf =
let nspare = not spare in
SlicingMarks.mk_user_mark ~data:nspare ~addr:nspare ~ctrl:nspare
in
- assert (Db.Value.is_computed ());
+ assert (Eva.Analysis.is_computed ());
let outputs = !Db.Outputs.get_external kf in
select_entry_point_and_some_inputs_outputs set ~mark kf
~return:true
@@ -308,7 +309,7 @@ let select_stmt_zone set mark zone ~before ki kf =
or after (c.f. boolean [~before]) the statement [ki].
Note: add also a transparent selection on the whole statement. *)
let select_stmt_lval set mark lval_str ~before ki ~eval kf =
- assert (Db.Value.is_computed ());
+ assert (Eva.Analysis.is_computed ());
if Datatype.String.Set.is_empty lval_str
then set
else
@@ -319,11 +320,7 @@ let select_stmt_lval set mark lval_str ~before ki ~eval kf =
let lval =
!Db.Properties.Interp.term_lval_to_lval ~result:None lval_term
in
- let state = Db.Value.get_stmt_state eval in
- let _deps, zone, _exact =
- !Db.Value.lval_to_zone_with_deps_state
- ~deps:None ~for_writing:false state lval
- in
+ let zone = get_lval_zone eval lval in
Locations.Zone.join zone acc)
lval_str
Locations.Zone.bottom
@@ -342,7 +339,7 @@ let select_stmt_lval set mark lval_str ~before ki ~eval kf =
i.e. when [ki_opt] is a call, the selection doesn't look at the assigns clause
of a call. *)
let select_lval_rw set mark ~rd ~wr ~eval kf ki_opt=
- assert (Db.Value.is_computed ());
+ assert (Eva.Analysis.is_computed ());
let zone_option ~for_writing lval_str =
if Datatype.String.Set.is_empty lval_str
then None
@@ -352,11 +349,8 @@ let select_lval_rw set mark ~rd ~wr ~eval kf ki_opt=
(fun lval_str acc ->
let lval_term = !Db.Properties.Interp.term_lval kf lval_str in
let lval = !Db.Properties.Interp.term_lval_to_lval ~result:None lval_term in
- let state = Db.Value.get_stmt_state eval in
- let _deps, zone, _exact =
- !Db.Value.lval_to_zone_with_deps_state
- state ~for_writing ~deps:None lval
- in
+ let access = if for_writing then Locations.Write else Locations.Read in
+ let zone = get_lval_zone ~access eval lval in
Locations.Zone.join zone acc)
lval_str Locations.Zone.bottom
in SlicingParameters.debug ~level:3
@@ -389,7 +383,7 @@ let select_lval_rw set mark ~rd ~wr ~eval kf ki_opt=
| None ->
Globals.Functions.iter
(fun kf ->
- if !Db.Value.is_called kf then
+ if Eva.Results.is_called kf then
if not (!Db.Value.use_spec_instead_of_definition kf)
then (* Called function with source code: just looks at its stmt *)
Kinstr.iter_from_func (select_rw_from_stmt kf) kf
@@ -413,7 +407,7 @@ let select_lval_rw set mark ~rd ~wr ~eval kf ki_opt=
~return:false ~inputs ~outputs:Locations.Zone.bottom
in
- assert (!Db.Value.is_called kf) ; (* otherwise [!Db.Outputs.get_external kf] gives weird results *)
+ assert (Eva.Results.is_called kf) ; (* otherwise [!Db.Outputs.get_external kf] gives weird results *)
select_inter_zone select_wr zone_wr_opt (!Db.Outputs.get_external kf) ;
select_inter_zone select_rd zone_rd_opt (!Db.Inputs.get_external kf)
end
diff --git a/src/plugins/slicing/slicingMacros.ml b/src/plugins/slicing/slicingMacros.ml
index d49a3f596c1632a67974dc3aefcfe1553699c28d..ebb985bc1985e17a25ddb057e273ed32aef42a9c 100644
--- a/src/plugins/slicing/slicingMacros.ml
+++ b/src/plugins/slicing/slicingMacros.ml
@@ -173,12 +173,9 @@ let is_call_stmt stmt =
| Instr (Call _ | Local_init(_, ConsInit _,_)) -> true | _ -> false
let get_called_kf call_stmt = match call_stmt.skind with
- | Instr (Call (_, funcexp,_,_)) ->
- let _funcexp_dpds, called_functions =
- !Db.Value.expr_to_kernel_function ~deps:None (Kstmt call_stmt) funcexp
- in
- (match Kernel_function.Hptset.contains_single_elt called_functions with
- | Some kf -> kf
+ | Instr (Call _) ->
+ (match Eva.Results.callee call_stmt with
+ | [kf] -> kf
| _ -> raise SlicingTypes.PtrCallExpr)
| Instr (Local_init(_, ConsInit (f, _, _), _)) -> Globals.Functions.get f
| _ -> invalid_arg "Not a call statement !"
diff --git a/src/plugins/slicing/slicingProject.ml b/src/plugins/slicing/slicingProject.ml
index 73532548cc680d1e25e1d22b8fa9a079ccb49a9b..010cbdd86d44d86398a97ab5efe9e2f392998268 100644
--- a/src/plugins/slicing/slicingProject.ml
+++ b/src/plugins/slicing/slicingProject.ml
@@ -222,13 +222,13 @@ let apply_appli_crit appli_crit =
match appli_crit with
| T.CaCall fi_to_call ->
let kf_to_call = M.get_fi_kf fi_to_call in
- let add_actions actions (kf_caller,_) =
+ let add_actions actions kf_caller =
let fi_caller = M.get_kf_fi kf_caller in
let mark = SlicingMarks.mk_user_spare in
let action =
SlicingActions.mk_crit_mark_calls fi_caller kf_to_call mark in
action :: actions
- in List.fold_left add_actions [] (!Db.Value.callers kf_to_call)
+ in List.fold_left add_actions [] (Eva.Results.callers kf_to_call)
| _ ->
SlicingParameters.not_yet_implemented
"This slicing criterion on application"
diff --git a/src/plugins/slicing/slicingSelect.ml b/src/plugins/slicing/slicingSelect.ml
index 5775c6ecbe4f45d9c3540775f6a1062325efd5a6..b4b331aabe20174accb29534e0e15179b06d3aec 100644
--- a/src/plugins/slicing/slicingSelect.ml
+++ b/src/plugins/slicing/slicingSelect.ml
@@ -105,7 +105,7 @@ let select_stmt_zone kf ?(select=empty_db_select kf) stmt ~before loc mark =
Locations.Zone.pretty loc
(if before then "before" else "after") stmt.sid
SlicingMarks.pretty_mark mark;
- if not (Db.Value.is_reachable_stmt stmt) then
+ if not (Eva.Results.is_reachable stmt) then
begin
SlicingParameters.feedback
"@[Nothing to select for @[%a@]@ %s unreachable stmt of %a@]"
@@ -194,7 +194,7 @@ let stmt_nodes_to_select pdg stmt =
let select_stmt_computation kf ?(select=empty_db_select kf) stmt mark =
SlicingParameters.debug ~level:1 "[Register.select_stmt_computation] on stmt %d" stmt.sid;
- if not (Db.Value.is_reachable_stmt stmt) then
+ if not (Eva.Results.is_reachable stmt) then
begin
SlicingParameters.feedback
"@[Nothing to select for an unreachable stmt of %a@]"
diff --git a/src/plugins/slicing/slicingState.ml b/src/plugins/slicing/slicingState.ml
index 93a4ad676a17dfd508df128dec7f32b16c2fe1b8..4b9a224a47538ed45941692170d9cea09894a585 100644
--- a/src/plugins/slicing/slicingState.ml
+++ b/src/plugins/slicing/slicingState.ml
@@ -49,7 +49,7 @@ let may_map ~none f = match P.get_option () with
| Some _ -> f ()
let reset_slicing () =
- !Db.Value.compute () ;
+ Eva.Analysis.compute () ;
let initialized = match P.get_option () with | None -> false | Some _ -> true in
if not initialized then
SlicingParameters.feedback ~level:1 "initializing slicing ..."
diff --git a/src/plugins/slicing/slicingTransform.ml b/src/plugins/slicing/slicingTransform.ml
index c27b8a15e3be1be8bb12135b32ffba67d21e6533..9a4723f972394a8c7158259f38c6a7a6d69e01a6 100644
--- a/src/plugins/slicing/slicingTransform.ml
+++ b/src/plugins/slicing/slicingTransform.ml
@@ -234,7 +234,7 @@ module Visibility (SliceName : sig
let annotation_visible ff_opt stmt annot =
SlicingParameters.debug ~current:true ~level:2
"[SlicingTransform.Visibility.annotation_visible] ?";
- Db.Value.is_reachable_stmt stmt &&
+ Eva.Results.is_reachable stmt &&
Alarms.find annot = None && (* Always drop alarms: the alarms table
in the new project is not synchronized *)
match ff_opt with
diff --git a/src/plugins/sparecode/register.ml b/src/plugins/sparecode/register.ml
index a6c985c0dc8ebfa6dc8f75311a28460c62ad48b9..a6a1fa9a5bfab44f202049b1b4c4b67773b30e78 100644
--- a/src/plugins/sparecode/register.ml
+++ b/src/plugins/sparecode/register.ml
@@ -35,7 +35,7 @@ module Result =
(struct
let name = "Sparecode"
let size = 7
- let dependencies = [ Ast.self; Db.Value.self ] (* delayed, see below *)
+ let dependencies = [ Ast.self; Eva.Analysis.self ] (* delayed, see below *)
end)
let () =
diff --git a/src/plugins/sparecode/transform.ml b/src/plugins/sparecode/transform.ml
index ce447c3fb94eecd147f1fd0adf0f111c4854a471..8c9fb9a68f6d4fde5b84a591d0600cfa59161639 100644
--- a/src/plugins/sparecode/transform.ml
+++ b/src/plugins/sparecode/transform.ml
@@ -81,7 +81,7 @@ module BoolInfo = struct
key_visible "label_visible" fm lab_key
let annotation_visible _ stmt annot =
- Db.Value.is_reachable_stmt stmt && Alarms.find annot = None
+ Eva.Results.is_reachable stmt && Alarms.find annot = None
(* Keep annotations on reachable, but not alarms: they can be resynthesized,
and the alarms table is not synchronized in the new project anyway *)
(* TODO: does not seem really coherent with the fact that almost everything
@@ -126,13 +126,11 @@ module BoolInfo = struct
let called_info (project, _fm) call_stmt =
match call_stmt.skind with
| Instr (Call (_, _, _, _) | Local_init(_, ConsInit _, _)) ->
- let called_functions = Db.Value.call_to_kernel_function call_stmt in
+ let called_functions = Eva.Results.callee call_stmt in
let call_info =
- match
- Kernel_function.Hptset.contains_single_elt called_functions
- with
- | None -> None
- | Some kf ->
+ match called_functions with
+ | [] | _ :: _ :: _ -> None
+ | [kf] ->
match Spare_marks.get_marks project kf with
| None ->
if Spare_marks.kf_visible project kf
diff --git a/src/plugins/studia/reads.ml b/src/plugins/studia/reads.ml
index 3685d8cba7b689b4e0ee46f1408db61985065d61..0a432ee23a669275b49c37bbc8324b1974c869c3 100644
--- a/src/plugins/studia/reads.ml
+++ b/src/plugins/studia/reads.ml
@@ -44,15 +44,13 @@ class find_read zlval = object
let deps = match lvopt with
| None -> deps
| Some lv ->
- let dlv, _ =
- !Db.Value.lval_to_loc_with_deps (Kstmt stmt) ~deps:Zone.bottom lv
- in
+ let dlv = Eva.Results.(before stmt |> address_deps lv) in
Zone.join dlv deps
in
let direct = Zone.intersects deps zlval in
(* now determine if the functions called at [stmt] read directly or
indirectly [zlval] *)
- let aux_kf kf effects =
+ let aux_kf effects kf =
let inputs = !Db.Inputs.get_internal kf in
(* TODO: change to this once we can get "full" inputs through Inout.
Currently, non operational inputs disappear, and this function
@@ -68,9 +66,9 @@ class find_read zlval = object
else
effects (* this function pointer does not read [zlval] *)
in
- let kfs = Db.Value.call_to_kernel_function stmt in
+ let kfs = Eva.Results.callee stmt in
let effects =
- Kernel_function.Hptset.fold aux_kf kfs {direct; indirect = false}
+ List.fold_left aux_kf {direct; indirect = false} kfs
in
res <- (stmt, effects) :: res
end
diff --git a/src/plugins/studia/studia_gui.ml b/src/plugins/studia/studia_gui.ml
index 9008db351027fc01dcfd385aba799782e8a4f718..c7b1425c394d7c776424631c55b840ec99640425 100644
--- a/src/plugins/studia/studia_gui.ml
+++ b/src/plugins/studia/studia_gui.ml
@@ -90,7 +90,7 @@ struct
(Stmt.Map.Make(Datatype.String.Set))
(struct
let name = Info.name
- let dependencies = [ Db.Value.self ]
+ let dependencies = [ Eva.Analysis.self ]
let default () = Stmt.Map.empty
end)
@@ -184,7 +184,7 @@ module StudiaState =
(Stmt)
(struct
let name = "Studia.Highlighter.StudiaState"
- let dependencies = [ Db.Value.self ]
+ let dependencies = [ Eva.Analysis.self ]
end)
let reset () =
@@ -226,7 +226,7 @@ let highlighter (buffer:Design.reactive_buffer) localizable ~start ~stop =
with Not_found -> ()
let check_value (main_ui:Design.main_window_extension_points) =
- Db.Value.is_computed () ||
+ Eva.Analysis.is_computed () ||
let answer = GToolbox.question_box
~title:("Eva Needed")
~buttons:[ "Run"; "Cancel" ]
@@ -234,7 +234,7 @@ let check_value (main_ui:Design.main_window_extension_points) =
^"Do you want to run Eva now ?")
in
answer = 1 &&
- match main_ui#full_protect ~cancelable:true !Db.Value.compute with
+ match main_ui#full_protect ~cancelable:true Eva.Analysis.compute with
| Some _ -> true
| None -> false
diff --git a/src/plugins/studia/studia_request.ml b/src/plugins/studia/studia_request.ml
index ff3f94c3d1061bc178020507cb565241d5cb20dc..2e44a1b8e8f0d4c9503225954eefa4578b65d3b9 100644
--- a/src/plugins/studia/studia_request.ml
+++ b/src/plugins/studia/studia_request.ml
@@ -81,7 +81,8 @@ let compute kind zone =
let empty = { direct = []; indirect = []; } in
List.fold_left add empty stmts
-let lval_location kinstr lval = !Db.Value.lval_to_zone kinstr lval
+let lval_location kinstr lval =
+ Eva.Results.(before_kinstr kinstr |> eval_address lval |> as_zone)
let () = Request.register ~package
~kind:`GET ~name:"getReadsLval"
diff --git a/src/plugins/studia/writes.ml b/src/plugins/studia/writes.ml
index fa29b18e974c25b9234fa1e95b11f4f3fd8005aa..dbcbcfc04cea20a2596da29b264f3ea0e4b852ee 100644
--- a/src/plugins/studia/writes.ml
+++ b/src/plugins/studia/writes.ml
@@ -35,7 +35,7 @@ type effects = {
(** Does the functions called at [stmt] modify directly or indirectly [zlval] *)
let effects_of_call stmt zlval effects =
- let aux_kf kf effects =
+ let aux_kf effects kf =
let inout = !Db.Operational_inputs.get_internal_precise ~stmt kf in
let out = inout.Inout_type.over_outputs in
if Zone.intersects out zlval then
@@ -47,8 +47,8 @@ let effects_of_call stmt zlval effects =
else
effects
in
- let kfs = Db.Value.call_to_kernel_function stmt in
- Kernel_function.Hptset.fold aux_kf kfs effects
+ let kfs = Eva.Results.callee stmt in
+ List.fold_left aux_kf effects kfs
class find_write zlval = object (self)
inherit Visitor.frama_c_inplace
@@ -66,8 +66,8 @@ class find_write zlval = object (self)
let direct_write = match lvopt with
| None -> false
| Some lv ->
- let zlv = !Db.Value.lval_to_zone (Kstmt stmt) lv in
- Zone.intersects zlv zlval
+ Eva.Results.(before stmt |> eval_address lv |> as_zone_result) |>
+ Result.fold ~ok:(Zone.intersects zlval) ~error:(fun _ -> false)
in
let effects =
effects_of_call stmt zlval {direct = direct_write; indirect =false}
diff --git a/src/plugins/users/users_register.ml b/src/plugins/users/users_register.ml
index f556af9526d47558f4ee79c364b2a0db5cb08162..a57f90f00f611368777176fdc7dc2fd6c41dc995 100644
--- a/src/plugins/users/users_register.ml
+++ b/src/plugins/users/users_register.ml
@@ -79,7 +79,7 @@ let get kf =
if Users.is_computed () then
find kf
else begin
- if Db.Value.is_computed () then begin
+ if Eva.Analysis.is_computed () then begin
feedback "requiring again the computation of the value analysis";
Project.clear
~selection:(State_selection.with_dependencies Db.Value.self)
@@ -87,7 +87,7 @@ let get kf =
end else
feedback ~level:2 "requiring the computation of the value analysis";
add_value_hook ();
- !Db.Value.compute ();
+ Eva.Analysis.compute ();
find kf
end
diff --git a/src/plugins/value/Eva.mli b/src/plugins/value/Eva.mli
index 74ac173305e0e35d0eecdebbcca95a211bf0a8b4..58006b2c451753ca0a1707acada914bcd5106ac6 100644
--- a/src/plugins/value/Eva.mli
+++ b/src/plugins/value/Eva.mli
@@ -1,38 +1,308 @@
-(**************************************************************************)
-(* *)
-(* This file is part of Frama-C. *)
-(* *)
-(* Copyright (C) 2007-2021 *)
-(* CEA (Commissariat à l'énergie atomique et aux énergies *)
-(* alternatives) *)
-(* *)
-(* you can redistribute it and/or modify it under the terms of the GNU *)
-(* Lesser General Public License as published by the Free Software *)
-(* Foundation, version 2.1. *)
-(* *)
-(* It is distributed in the hope that it will be useful, *)
-(* but WITHOUT ANY WARRANTY; without even the implied warranty of *)
-(* MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the *)
-(* GNU Lesser General Public License for more details. *)
-(* *)
-(* See the GNU Lesser General Public License version 2.1 *)
-(* for more details (enclosed in the file licenses/LGPLv2.1). *)
-(* *)
-(**************************************************************************)
-
-(** Analysis for values and pointers *)
+(** Eva public API.
-module Value_results: sig
- type results
+ The main modules are:
+ - Analysis: run the analysis.
+ - Results: access analysis results, especially the values of expressions
+ and memory locations of lvalues at each program point.
+
+ The following modules allow configuring the Eva analysis:
+ - Value_parameters: change the configuration of the analysis.
+ - Eva_annotations: add local annotations to guide the analysis.
+ - Builtins: register ocaml builtins to be used by the cvalue domain
+ instead of analysing the body of some C functions.
+
+ Other modules are for internal use only. *)
+
+(* This file is generated. Do not edit. *)
+
+module Analysis: sig
+ val compute : unit -> unit
+ (** Computes the Eva analysis, if not already computed, using the entry point
+ of the current project. You may set it with {!Globals.set_entry_point}.
+ @raise Globals.No_such_entry_point if the entry point is incorrect
+ @raise Db.Value.Incorrect_number_of_arguments if some arguments are
+ specified for the entry point using {!Db.Value.fun_set_args}, and
+ an incorrect number of them is given.
+ @plugin development guide *)
+
+ val is_computed : unit -> bool
+ (** Return [true] iff the Eva analysis has been done. *)
+
+ val self : State.t
+ (** Internal state of Eva analysis from projects viewpoint. *)
+end
+
+module Results: sig
+ (** Eva's result API is a work-in-progress interface to allow accessing the
+ analysis results once its completed. It is experimental and is very likely
+ to change in the future. It aims at replacing [Db.Value] but does not
+ completely covers all its usages yet. As for now, this interface has some
+ advantages over Db's :
+
+ - evaluations uses every available domains and not only Cvalue;
+ - the caller may distinguish failure cases when a request is unsucessful;
+ - working with callstacks is easy;
+ - some common shortcuts are provided (e.g. for extracting ival directly);
+ - overall, individual functions are simpler.
+
+ The idea behind this API is that requests must be decomposed in several
+ steps. For instance, to evaluate an expression :
+
+ 1. first, you have to state where you want to evaluate it,
+ 2. optionally, you may specify in which callstack,
+ 3. you choose the expression to evaluate,
+ 4. you require a destination type to evaluate into.
+
+ Usage sketch :
+
+ Eva.Results.(
+ before stmt |> in_callstack cs |>
+ eval_var vi |> as_int |> default 0)
+
+ or equivalently, if you prefer
+
+ Eva.Results.(
+ default O (as_int (eval_var vi (in_callstack cs (before stmt))))
+ *)
+
+
+ type callstack = (Cil_types.kernel_function * Cil_types.kinstr) list
+
+ type request
+
+ type value
+ type address
+ type 'a evaluation
+
+ type error = Bottom | Top | DisabledDomain
+ type 'a result = ('a,error) Result.t
+
+
+ (** Results handling *)
+
+ (** Translates an error to a human readable string. *)
+ val string_of_error : error -> string
+
+ (** Pretty printer for errors. *)
+ val pretty_error : Format.formatter -> error -> unit
+
+ (** Pretty printer for API's results. *)
+ val pretty_result : (Format.formatter -> 'a -> unit) ->
+ Format.formatter -> 'a result -> unit
+
+ (** [default d r] extracts the value of [r] if [r] is Ok,
+ or use the default value [d] otherwise.
+ Equivalent to [Result.value ~default:d r] *)
+ val default : 'a -> 'a result -> 'a
+
+
+ (** Control point selection *)
+
+ (** At the start of the analysis, but after the initialization of globals. *)
+ val at_start : request
+
+ (** At the end of the analysis, after the main function has returned. *)
+ val at_end : unit -> request
+
+ (** At the start of the given function. *)
+ val at_start_of : Cil_types.kernel_function -> request
+
+ (** At the end of the given function.
+ @raises Kernel_function.No_statement if the function has no body. *)
+ val at_end_of : Cil_types.kernel_function -> request
+
+ (** Just before a statement is executed. *)
+ val before : Cil_types.stmt -> request
+
+ (** Just after a statement is executed. *)
+ val after : Cil_types.stmt -> request
+
+ (** Just before a statement or at the start of the analysis. *)
+ val before_kinstr : Cil_types.kinstr -> request
+
+
+ (** Callstack selection *)
+
+ (** Only consider the given callstack.
+ Replaces previous calls to [in_callstack] or [in_callstacks]. *)
+ val in_callstack : callstack -> request -> request
+
+ (** Only consider the callstacks from the given list.
+ Replaces previous calls to [in_callstack] or [in_callstacks]. *)
+ val in_callstacks : callstack list -> request -> request
+
+ (** Only consider callstacks satisfying the given predicate. Several filters
+ can be added. If callstacks are also selected with [in_callstack] or
+ [in_callstacks], only the selected callstacks will be filtered. *)
+ val filter_callstack : (callstack -> bool) -> request -> request
+
+
+ (** Working with callstacks *)
+
+ (** Returns the list of reachable callstacks from the given request.
+ An empty list is returned if the request control point has not been
+ reached by the analysis, or if no information has been saved at this point
+ (for instance with the -eva-no-results option).
+ Use [is_empty request] to distinguish these two cases. *)
+ val callstacks : request -> callstack list
+
+ (** Returns a list of subrequests for each reachable callstack from
+ the given request. *)
+ val by_callstack : request -> (callstack * request) list
+
+
+ (** State requests *)
+
+ (** Returns the list of expressions which have been inferred to be equal to
+ the given expression by the Equality domain. *)
+ val equality_class : Cil_types.exp -> request -> Cil_types.exp list result
+
+ (** Returns the Cvalue state. Error cases are converted into the bottom or top
+ cvalue state accordingly. *)
+ val get_cvalue_model : request -> Cvalue.Model.t
+
+ (** Returns the Cvalue model. *)
+ val get_cvalue_model_result : request -> Cvalue.Model.t result
+
+
+ (** Dependencies *)
+
+ (** Computes (an overapproximation of) the memory zones that must be read to
+ evaluate the given expression, including all adresses computations. *)
+ val expr_deps : Cil_types.exp -> request -> Locations.Zone.t
+
+ (** Computes (an overapproximation of) the memory zones that must be read to
+ evaluate the given lvalue, including the lvalue zone itself. *)
+ val lval_deps : Cil_types.lval -> request -> Locations.Zone.t
+
+ (** Computes (an overapproximation of) the memory zones that must be read to
+ evaluate the given lvalue, excluding the lvalue zone itself. *)
+ val address_deps : Cil_types.lval -> request -> Locations.Zone.t
+
+
+ (** Evaluation *)
+
+ (** Returns (an overapproximation of) the possible values of the variable. *)
+ val eval_var : Cil_types.varinfo -> request -> value evaluation
+
+ (** Returns (an overapproximation of) the possible values of the lvalue. *)
+ val eval_lval : Cil_types.lval -> request -> value evaluation
+
+ (** Returns (an overapproximation of) the possible values of the expression. *)
+ val eval_exp : Cil_types.exp -> request -> value evaluation
+
+
+ (** Returns (an overapproximation of) the possible addresses of the lvalue. *)
+ val eval_address : Cil_types.lval -> request -> address evaluation
+
+
+ (** Returns the kernel functions into which the given expression may evaluate.
+ If the callee expression doesn't always evaluate to a function, those
+ spurious values are ignored. If it always evaluate to a non-function value
+ then the returned list is empty.
+ Raises [Stdlib.Invalid_argument] if the callee expression is not an lvalue
+ without offset.
+ Also see [callee] for a function which applies directly on Call
+ statements. *)
+ val eval_callee : Cil_types.exp -> request -> Kernel_function.t list result
+
+
+ (** Evaluated values conversion *)
+
+ (** In all functions below, if the abstract value inferred by Eva does not fit
+ in the required type, [Error Top] is returned, as Top is the only possible
+ over-approximation of the request. *)
+
+ (** Converts the value into a singleton ocaml int. *)
+ val as_int : value evaluation -> int result
+
+ (** Converts the value into a singleton unbounded integer. *)
+ val as_integer : value evaluation -> Integer.t result
+
+ (** Converts the value into a floating point number. *)
+ val as_float : value evaluation -> float result
+
+ (** Converts the value into a C number abstraction. *)
+ val as_ival : value evaluation -> Ival.t result
+
+ (** Converts the value into a floating point abstraction. *)
+ val as_fval : value evaluation -> Fval.t result
+
+ (** Converts the value into a Cvalue abstraction. Converts error cases
+ into bottom and top values accordingly. *)
+ val as_cvalue : value evaluation -> Cvalue.V.t
+
+ (** Converts the value into a Cvalue abstraction. *)
+ val as_cvalue_result : value evaluation -> Cvalue.V.t result
+
+
+ (** Converts into a C location abstraction. *)
+ val as_location : address evaluation -> Locations.location result
+
+ (** Converts into a Zone. Error cases are converted into bottom or top zones
+ accordingly. *)
+ val as_zone: ?access:Locations.access -> address evaluation ->
+ Locations.Zone.t
+
+ (** Converts into a Zone result. *)
+ val as_zone_result : ?access:Locations.access -> address evaluation ->
+ Locations.Zone.t result
+
+
+ (** Evaluation properties *)
+
+ (** Returns whether the evaluated value is initialized or not. If the value have
+ been evaluated from a Cil expression, it is always initialized. *)
+ val is_initialized : value evaluation -> bool
+
+ (** Returns the set of alarms emitted during the evaluation. *)
+ val alarms : 'a evaluation -> Alarms.t list
+
+
+ (** Reachability *)
+
+ (** Returns true if there are no reachable states for the given request. *)
+ val is_empty : request -> bool
+
+ (** Returns true if an evaluation leads to bottom, i.e. if the given expression
+ or lvalue cannot be evaluated to a valid result for the given request. *)
+ val is_bottom : 'a evaluation -> bool
+
+ (** Returns true if the function has been analyzed. *)
+ val is_called : Cil_types.kernel_function -> bool
+
+ (** Returns true if the statement has been reached by the analysis. *)
+ val is_reachable : Cil_types.stmt -> bool
+
+ (** Returns true if the statement has been reached by the analysis, or if
+ the main function has been analyzed for [Kglobal]. *)
+ val is_reachable_kinstr : Cil_types.kinstr -> bool
+
+
+ (*** Callers / Callees / Callsites *)
+
+ (** Returns the list of inferred callers of the given function. *)
+ val callers : Cil_types.kernel_function -> Cil_types.kernel_function list
+
+ (** Returns the list of inferred callers, and for each of them, the list
+ of callsites (the call statements) inside. *)
+ val callsites : Cil_types.kernel_function ->
+ (Cil_types.kernel_function * Cil_types.stmt list) list
+
+
+ (** Returns the kernel functions called in the given statement.
+ If the callee expression doesn't always evaluate to a function, those
+ spurious values are ignored. If it always evaluate to a non-function value
+ then the returned list is empty.
+ Raises [Stdlib.Invalid_argument] if the statement is not a [Call]
+ instruction or a [Local_init] with [ConsInit] initializer. *)
+ val callee : Cil_types.stmt -> Kernel_function.t list
- val get_results: unit -> results
- val set_results: results -> unit
- val merge: results -> results -> results
- val change_callstacks:
- (Value_types.callstack -> Value_types.callstack) -> results -> results
end
module Value_parameters: sig
+ (** Configuration of the analysis. *)
+
(** Returns the list (name, descr) of currently enabled abstract domains. *)
val enabled_domains: unit -> (string * string) list
@@ -46,36 +316,16 @@ module Value_parameters: sig
val use_global_value_partitioning: Cil_types.varinfo -> unit
end
-module Eval_terms: sig
- (** Evaluation environment, built by [env_annot]. *)
- type eval_env
-
- (** Dependencies needed to evaluate a term or a predicate. *)
- type logic_deps = Locations.Zone.t Cil_datatype.Logic_label.Map.t
-
- type labels_states = Db.Value.state Cil_datatype.Logic_label.Map.t
-
- val env_annot :
- ?c_labels:labels_states -> pre:Db.Value.state -> here:Db.Value.state ->
- unit -> eval_env
-
- (** [predicate_deps env p] computes the logic dependencies needed to evaluate
- [p] in the given evaluation environment [env].
- @return None on either an evaluation error or on unsupported construct. *)
- val predicate_deps: eval_env -> Cil_types.predicate -> logic_deps option
-end
-
-
-module Unit_tests: sig
- (** Runs the unit tests of Eva. *)
- val run: unit -> unit
-end
-
-(** Register special annotations to locally guide the partitioning of states
- performed by an Eva analysis. *)
module Eva_annotations: sig
+ (** Register special annotations to locally guide the Eva analysis:
- (** Annotations tweaking the behavior of the -eva-slevel paramter. *)
+ - slevel annotations: "slevel default", "slevel merge" and "slevel i"
+ - loop unroll annotations: "loop unroll term"
+ - value partitioning annotations: "split term" and "merge term"
+ - subdivision annotations: "subdivide i"
+ *)
+
+ (** Annotations tweaking the behavior of the -eva-slevel parameter. *)
type slevel_annotation =
| SlevelMerge (** Join all states separated by slevel. *)
| SlevelDefault (** Use the limit defined by -eva-slevel. *)
@@ -88,6 +338,7 @@ module Eva_annotations: sig
| UnrollFull (** Unroll amount defined by -eva-default-loop-unroll. *)
type split_kind = Static | Dynamic
+
type split_term =
| Expression of Cil_types.exp
| Predicate of Cil_types.predicate
@@ -99,10 +350,13 @@ module Eva_annotations: sig
| FlowMerge of split_term
(** Merge states separated by a previous split. *)
+ type allocation_kind = By_stack | Fresh | Fresh_weak | Imprecise
+
val get_slevel_annot : Cil_types.stmt -> slevel_annotation option
val get_unroll_annot : Cil_types.stmt -> unroll_annotation list
val get_flow_annot : Cil_types.stmt -> flow_annotation list
val get_subdivision_annot : Cil_types.stmt -> int list
+ val get_allocation: Cil_types.stmt -> allocation_kind
val add_slevel_annot : emitter:Emitter.t ->
Cil_types.stmt -> slevel_annotation -> unit
@@ -114,33 +368,105 @@ module Eva_annotations: sig
Cil_types.stmt -> int -> unit
end
-(** Analysis builtins for the cvalue domain, more efficient than the analysis
- of the C functions. See {builtins.mli} for more details. *)
+module Eval: sig
+ (** Can the results of a function call be cached with memexec? *)
+ type cacheable =
+ | Cacheable (** Functions whose result can be safely cached. *)
+ | NoCache (** Functions whose result should not be cached, but for
+ which the caller can still be cached. Typically,
+ functions printing something during the analysis. *)
+ | NoCacheCallers (** Functions for which neither the call, neither the
+ callers, can be cached. *)
+end
+
module Builtins: sig
+ (** Eva analysis builtins for the cvalue domain, more efficient than their
+ equivalent in C. *)
+
open Cil_types
exception Invalid_nb_of_args of int
exception Outside_builtin_possibilities
+ (* Signature of a builtin: type of the result, and type of the arguments. *)
type builtin_type = unit -> typ * typ list
- type cacheable = Cacheable | NoCache | NoCacheCallers
+
+ (** Can the results of a builtin be cached? See {eval.mli} for more details.*)
+ type cacheable = Eval.cacheable = Cacheable | NoCache | NoCacheCallers
type full_result = {
c_values: (Cvalue.V.t option * Cvalue.Model.t) list;
+ (** A list of results, consisting of:
+ - the value returned (ie. what is after the 'return' C keyword)
+ - the memory state after the function has been executed. *)
c_clobbered: Base.SetLattice.t;
+ (** An over-approximation of the bases in which addresses of local variables
+ might have been written *)
c_from: (Function_Froms.froms * Locations.Zone.t) option;
+ (** If not None, the froms of the function, and its sure outputs;
+ i.e. the dependencies of the result and of each zone written to. *)
}
+ (** The result of a builtin can be given in different forms. *)
type call_result =
| States of Cvalue.Model.t list
+ (** A disjunctive list of post-states at the end of the C function.
+ Can only be used if the C function does not write the address of local
+ variables, does not read other locations than the call arguments, and
+ does not write other locations than the result. *)
| Result of Cvalue.V.t list
+ (** A disjunctive list of resulting values. The specification is used to
+ compute the post-state, in which the result is replaced by the values
+ computed by the builtin. *)
| Full of full_result
+ (** See [full_result] type. *)
+ (** Type of a cvalue builtin, whose arguments are:
+ - the memory state at the beginning of the function call;
+ - the list of arguments of the function call. *)
type builtin = Cvalue.Model.t -> (exp * Cvalue.V.t) list -> call_result
+ (** [register_builtin name ?replace ?typ cacheable f] registers the function [f]
+ as a builtin to be used instead of the C function of name [name].
+ If [replace] is provided, the builtin is also used instead of the C function
+ of name [replace], unless option -eva-builtin-auto is disabled.
+ If [typ] is provided, consistency between the expected [typ] and the type of
+ the C function is checked before using the builtin.
+ The results of the builtin are cached according to [cacheable]. *)
val register_builtin:
- string -> ?replace:string -> ?typ:builtin_type -> cacheable ->
- builtin -> unit
+ string -> ?replace:string -> ?typ:builtin_type -> cacheable -> builtin -> unit
+ (** Has a builtin been registered with the given name? *)
val is_builtin: string -> bool
end
+
+module Eval_terms: sig
+ (** [annot_predicate_deps ~pre ~here p] computes the logic dependencies needed
+ to evaluate the predicate [p] in a code annotation in cvalue state [here],
+ in a function whose pre-state is [pre].
+ Returns None on either an evaluation error or on unsupported construct. *)
+ val annot_predicate_deps:
+ pre:Cvalue.Model.t -> here:Cvalue.Model.t ->
+ Cil_types.predicate -> Locations.Zone.t option
+end
+
+module Value_results: sig
+ type results
+
+ val get_results: unit -> results
+ val set_results: results -> unit
+ val merge: results -> results -> results
+ val change_callstacks:
+ (Value_types.callstack -> Value_types.callstack) -> results -> results
+ (** Change the callstacks for the results for which this is meaningful.
+ For technical reasons, the top of the callstack must currently
+ be preserved. *)
+end
+
+module Unit_tests: sig
+ (** Currently tested by this module:
+ - semantics of sign values. *)
+
+ (** Runs some programmatic tests on Eva. *)
+ val run: unit -> unit
+end
diff --git a/src/plugins/value/api/general_requests.ml b/src/plugins/value/api/general_requests.ml
index 1b226d8e8d271a6d3b5a718d3b81e5c33d6c96e8..8d6e48f7301153d4eb7a85c70cb5e87318c433d1 100644
--- a/src/plugins/value/api/general_requests.ml
+++ b/src/plugins/value/api/general_requests.ml
@@ -57,7 +57,7 @@ let _computation_signal =
()
let is_computed kf =
- Db.Value.is_computed () &&
+ Analysis.is_computed () &&
match kf with
| { fundec = Definition (fundec, _) } ->
Mark_noresults.should_memorize_function fundec
@@ -66,7 +66,7 @@ let is_computed kf =
module CallSite = Data.Jpair (Kernel_ast.Kf) (Kernel_ast.Stmt)
let callers kf =
- let list = !Db.Value.callers kf in
+ let list = Value_results.callers kf in
List.concat (List.map (fun (kf, l) -> List.map (fun s -> kf, s) l) list)
let () = Request.register ~package
diff --git a/src/plugins/value/domains/cvalue/builtins.mli b/src/plugins/value/domains/cvalue/builtins.mli
index 353be4b52e81e4b3ef4ee8c9b868a391d0f7f2e8..ac9751b56a819843af15c3d267555c1966c253f9 100644
--- a/src/plugins/value/domains/cvalue/builtins.mli
+++ b/src/plugins/value/domains/cvalue/builtins.mli
@@ -20,6 +20,7 @@
(* *)
(**************************************************************************)
+[@@@ api_start]
(** Eva analysis builtins for the cvalue domain, more efficient than their
equivalent in C. *)
@@ -78,6 +79,7 @@ val register_builtin:
(** Has a builtin been registered with the given name? *)
val is_builtin: string -> bool
+[@@@ api_end]
(** Prepares the builtins to be used for an analysis. Must be called at the
beginning of each Eva analysis. Warns about builtins of incompatible types,
diff --git a/src/plugins/value/domains/equality/equality.mli b/src/plugins/value/domains/equality/equality.mli
index 87ef746f453b17bf99e21e3dfe59610aa01c1a0c..3e92e268f8a59aa7c7364038d0d3ed9e74f985f5 100644
--- a/src/plugins/value/domains/equality/equality.mli
+++ b/src/plugins/value/domains/equality/equality.mli
@@ -88,6 +88,8 @@ module Equality : sig
val choose: t -> elt
(** Return the representative of the equality. *)
+ val elements: t -> elt list
+ (** Returns the list of all elements of the given set. *)
end
type equality = Equality.t
diff --git a/src/plugins/value/domains/equality/equality_domain.ml b/src/plugins/value/domains/equality/equality_domain.ml
index 9d0299b703635aeb4146832b5564dc7638a6d753..ddf7bae272b9a77f854c3f3adac277e14ade6602 100644
--- a/src/plugins/value/domains/equality/equality_domain.ml
+++ b/src/plugins/value/domains/equality/equality_domain.ml
@@ -123,9 +123,6 @@ module Internal = struct
let log_category = dkey
- type equalities = Equality.Set.t
- let project (t, _, _) = t
-
let pretty fmt (eqs, _, _) = Equality.Set.pretty fmt eqs
let pretty_debug fmt (eqs, deps, modified) =
@@ -170,6 +167,10 @@ end
module Store = Domain_builder.Complete (Internal)
+type t = Internal.t
+let key = Store.key
+let project (t, _, _) = t
+
(* ------------------------- Abstract Domain -------------------------------- *)
diff --git a/src/plugins/value/domains/equality/equality_domain.mli b/src/plugins/value/domains/equality/equality_domain.mli
index 7adbbb6f9e6e6e267581c54e845c2e79271e92e1..b903b6e82d0b3e4a8112ac574d4307bb32bab492 100644
--- a/src/plugins/value/domains/equality/equality_domain.mli
+++ b/src/plugins/value/domains/equality/equality_domain.mli
@@ -31,12 +31,14 @@ type call_init_state =
| ISEmpty (** completely empty state, without impact on Memexec. *)
+type t
+val key: t Abstract_domain.key
+val project: t -> Equality.Set.t
+
module Make (Value : Abstract.Value.External) : sig
include Abstract_domain.Leaf with type value = Value.t
and type location = Precise_locs.precise_location
+ and type state = t
val pretty_debug : Format.formatter -> t -> unit
-
- type equalities
- val project : t -> equalities
end
diff --git a/src/plugins/value/engine/analysis.ml b/src/plugins/value/engine/analysis.ml
index 7fde8c2e3ddfee761223d62b4148c34b596a9994..ada39c5e3fb927d537bc33de14cce090d91f33a9 100644
--- a/src/plugins/value/engine/analysis.ml
+++ b/src/plugins/value/engine/analysis.ml
@@ -28,10 +28,12 @@ module type Results = sig
type value
type location
+ val get_global_state: unit -> state or_bottom
val get_stmt_state : after:bool -> stmt -> state or_bottom
- val get_kinstr_state: after:bool -> kinstr -> state or_bottom
val get_stmt_state_by_callstack:
after:bool -> stmt -> state Value_types.Callstack.Hashtbl.t or_top_or_bottom
+ val get_initial_state:
+ kernel_function -> state or_bottom
val get_initial_state_by_callstack:
kernel_function -> state Value_types.Callstack.Hashtbl.t or_top_or_bottom
@@ -74,13 +76,14 @@ module Make (Abstract: Abstractions.S) = struct
then Abstract.Dom.Store.get_stmt_state ~after stmt
else `Value Abstract.Dom.top
- let get_kinstr_state ~after = function
- | Kglobal -> Abstract.Dom.Store.get_global_state ()
- | Kstmt stmt -> get_stmt_state ~after stmt
+ let get_global_state = Abstract.Dom.Store.get_global_state
let get_stmt_state_by_callstack =
Abstract.Dom.Store.get_stmt_state_by_callstack
+ let get_initial_state =
+ Abstract.Dom.Store.get_initial_state
+
let get_initial_state_by_callstack =
Abstract.Dom.Store.get_initial_state_by_callstack
@@ -216,8 +219,18 @@ let force_compute () =
Analyzer.compute_from_entry_point ~lib_entry kf ;
ComputationState.set Computed
+let is_computed = Db.Value.is_computed
+
+let compute () =
+ (* Nothing to recompute when Value has already been computed. This boolean
+ is automatically cleared when an option of Value changes, because they
+ are registered as dependencies on [Db.Value.self] in {!Value_parameters}.*)
+ if not (is_computed ()) then force_compute ()
+
(* Resets the Analyzer when the current project is changed. *)
let () =
Project.register_after_set_current_hook
~user_only:true (fun _ -> reset_analyzer ());
Project.register_after_global_load_hook reset_analyzer
+
+let self = Db.Value.self
diff --git a/src/plugins/value/engine/analysis.mli b/src/plugins/value/engine/analysis.mli
index 2a6e647e5fc99a01f8172413e7cfa25721fb7b86..7eb2d53ef9b03bc1ace961ebf8be08ed5cd75564 100644
--- a/src/plugins/value/engine/analysis.mli
+++ b/src/plugins/value/engine/analysis.mli
@@ -28,10 +28,12 @@ module type Results = sig
type value
type location
+ val get_global_state: unit -> state or_bottom
val get_stmt_state : after:bool -> stmt -> state or_bottom
- val get_kinstr_state: after:bool -> kinstr -> state or_bottom
val get_stmt_state_by_callstack:
after:bool -> stmt -> state Value_types.Callstack.Hashtbl.t or_top_or_bottom
+ val get_initial_state:
+ kernel_function -> state or_bottom
val get_initial_state_by_callstack:
kernel_function -> state Value_types.Callstack.Hashtbl.t or_top_or_bottom
@@ -86,5 +88,22 @@ val register_computation_hook: ?on:computation_state ->
val force_compute : unit -> unit
(** Perform a full analysis, starting from the [main] function. *)
+[@@@ api_start]
+val compute : unit -> unit
+(** Computes the Eva analysis, if not already computed, using the entry point
+ of the current project. You may set it with {!Globals.set_entry_point}.
+ @raise Globals.No_such_entry_point if the entry point is incorrect
+ @raise Db.Value.Incorrect_number_of_arguments if some arguments are
+ specified for the entry point using {!Db.Value.fun_set_args}, and
+ an incorrect number of them is given.
+ @plugin development guide *)
+
+val is_computed : unit -> bool
+(** Return [true] iff the Eva analysis has been done. *)
+
+val self : State.t
+(** Internal state of Eva analysis from projects viewpoint. *)
+[@@@ api_end]
+
val cvalue_initial_state: unit -> Cvalue.Model.t
(** Return the initial state of the cvalue domain only. *)
diff --git a/src/plugins/value/eval.mli b/src/plugins/value/eval.mli
index 5714172358fc24dfbc4ba07a05c4fe2722fcb2b0..0c7808b6607d3199d63b59b321bb4a686797018f 100644
--- a/src/plugins/value/eval.mli
+++ b/src/plugins/value/eval.mli
@@ -270,15 +270,16 @@ type recursion = {
(** Same withdrawal as the previous field, for bases. *)
}
+[@@@ api_start]
(** Can the results of a function call be cached with memexec? *)
type cacheable =
- | Cacheable (** Functions whose result can be safely cached *)
+ | Cacheable (** Functions whose result can be safely cached. *)
| NoCache (** Functions whose result should not be cached, but for
which the caller can still be cached. Typically,
functions printing something during the analysis. *)
| NoCacheCallers (** Functions for which neither the call, neither the
- callers, can be cached *)
-
+ callers, can be cached. *)
+[@@@ api_end]
(*
Local Variables:
compile-command: "make -C ../../.."
diff --git a/src/plugins/value/gen-api.sh b/src/plugins/value/gen-api.sh
new file mode 100755
index 0000000000000000000000000000000000000000..82ce513c3bd3a9c39edda6e380afd1dab059e8ca
--- /dev/null
+++ b/src/plugins/value/gen-api.sh
@@ -0,0 +1,27 @@
+#!/bin/bash -eu
+
+printf '(** Eva public API.
+
+ The main modules are:
+ - Analysis: run the analysis.
+ - Results: access analysis results, especially the values of expressions
+ and memory locations of lvalues at each program point.
+
+ The following modules allow configuring the Eva analysis:
+ - Value_parameters: change the configuration of the analysis.
+ - Eva_annotations: add local annotations to guide the analysis.
+ - Builtins: register ocaml builtins to be used by the cvalue domain
+ instead of analysing the body of some C functions.
+
+ Other modules are for internal use only. *)\n'
+
+printf '\n(* This file is generated. Do not edit. *)\n'
+
+for i in "$@"
+do
+ file=$(basename $i)
+ module=${file%.*}
+ printf '\nmodule %s: sig\n' ${module^}
+ awk '/\[@@@ api_start\]/{flag=1;next} /\[@@@ api_end\]/{flag=0} flag{ print (NF ? " ":"") $0 }' $i
+ printf 'end\n'
+done
diff --git a/src/plugins/value/gui_files/gui_callstacks_manager.ml b/src/plugins/value/gui_files/gui_callstacks_manager.ml
index 9e78d8d54e60d5f8eeddb05bb9ec872bde95b280..c1473fc0604124127c1ec49e0822624511ba7a95 100644
--- a/src/plugins/value/gui_files/gui_callstacks_manager.ml
+++ b/src/plugins/value/gui_files/gui_callstacks_manager.ml
@@ -903,7 +903,7 @@ let make_widget (main_ui:main_ui) ~packing make_panel =
let tabs =
GPack.notebook ~scrollable:true ~packing:(vpaned#pack ~expand:true) ()
in
- vpaned#misc#set_sensitive (Db.Value.is_computed ());
+ vpaned#misc#set_sensitive (Analysis.is_computed ());
let pack_tab ?lbl w = ignore (tabs#insert_page ?tab_label:lbl w) in
let lbl_pane_default = GPack.hbox () in
let clear_button = new Widget.button ~icon:`CLEAR ~tooltip:"Clear" () in
@@ -1031,7 +1031,7 @@ let make_widget (main_ui:main_ui) ~packing make_panel =
HWidget.iter (fun w _ -> tabs#remove_page (tabs#page_num w)) hash_tabs;
HWidget.clear hash_tabs;
clear_default ();
- vpaned#misc#set_sensitive (Db.Value.is_computed ());
+ vpaned#misc#set_sensitive (Analysis.is_computed ());
in
let display_data_by_callstack loc selection content =
clear_button#set_enabled true;
diff --git a/src/plugins/value/gui_files/gui_eval.ml b/src/plugins/value/gui_files/gui_eval.ml
index 5888b1bbe9b9c204ecae7582dd2e0eed4c86c9c6..05335f728181d7d09eb7bf714a9070cefb4921f6 100644
--- a/src/plugins/value/gui_files/gui_eval.ml
+++ b/src/plugins/value/gui_files/gui_eval.ml
@@ -24,7 +24,7 @@ open Cil_types
open Gui_types
let results_kf_computed kf =
- Db.Value.is_computed () &&
+ Analysis.is_computed () &&
match kf with
| { fundec = Definition (fundec, _) } ->
Mark_noresults.should_memorize_function fundec
diff --git a/src/plugins/value/gui_files/register_gui.ml b/src/plugins/value/gui_files/register_gui.ml
index 3587497948dafbc7d40353138da1651a5b8202c2..e73612e700b95212a5ce4160d64fcef3cd14b9cc 100644
--- a/src/plugins/value/gui_files/register_gui.ml
+++ b/src/plugins/value/gui_files/register_gui.ml
@@ -35,7 +35,7 @@ module UsedVarState =
(struct
let size = 17
let name = "Value.Gui.UsedVarState"
- let dependencies = [ Db.Value.self ]
+ let dependencies = [ Analysis.self ]
(* [!Db.Inputs.self_external; !Db.Outputs.self_external] would be better
dependencies, but this introduces a very problematic recursion between
Value and Inout *)
@@ -67,7 +67,7 @@ let sync_filetree (filetree:Filetree.t) =
try
let vi = Kernel_function.get_vi kf in
let strikethrough =
- Db.Value.is_computed () && not (!Db.Value.is_called kf)
+ Analysis.is_computed () && not (Results.is_called kf)
in
filetree#set_global_attribute ~strikethrough vi
with Not_found -> ());
@@ -75,7 +75,7 @@ let sync_filetree (filetree:Filetree.t) =
(fun vi _ ->
if vi.vsource = true then
filetree#set_global_attribute
- ~strikethrough:(Db.Value.is_computed () && not (used_var vi))
+ ~strikethrough:(Analysis.is_computed () && not (used_var vi))
vi
);
if not (filetree#flat_mode) then
@@ -84,7 +84,7 @@ let sync_filetree (filetree:Filetree.t) =
(* the display name removes the path *)
let globals_state = filetree#get_file_globals file in
filetree#set_file_attribute
- ~strikethrough:(Db.Value.is_computed () &&
+ ~strikethrough:(Analysis.is_computed () &&
List.for_all snd globals_state)
file
)
@@ -96,11 +96,11 @@ let sync_filetree (filetree:Filetree.t) =
()
let hide_unused_function_or_var g =
- !hide_unused () && Db.Value.is_computed () &&
+ !hide_unused () && Analysis.is_computed () &&
(match g with
| GFun ({svar = vi}, _) | GFunDecl (_, vi, _) ->
let kf = Globals.Functions.get vi in
- not (!Db.Value.is_called kf)
+ not (Results.is_called kf)
| GVarDecl (vi, _) | GVar (vi, _, _) ->
not (used_var vi)
| _ -> false
@@ -144,7 +144,7 @@ let value_panel pack (main_ui:main_ui) =
ignore (run_button#connect#pressed
(fun () ->
main_ui#protect ~cancelable:true
- (fun () -> refresh (); !Db.Value.compute (); main_ui#reset ());
+ (fun () -> refresh (); Analysis.compute (); main_ui#reset ());
));
pack box;
"Eva", box#coerce, Some refresh
@@ -156,7 +156,7 @@ let active_highlighter buffer localizable ~start ~stop =
let buffer = buffer#buffer in
(* highlight dead code areas, non-terminating calls, and degeneration
points if Value has run.*)
- if Db.Value.is_computed () then
+ if Analysis.is_computed () then
match localizable with
| PStmt (kf, stmt) -> begin
let degenerate =
@@ -222,7 +222,7 @@ let menu_go_to_fun_definition (main_ui:main_ui) (popup_factory:menu) funs =
List.iter aux funs
let gui_compute_values (main_ui:main_ui) =
- if not (Db.Value.is_computed ())
+ if not (Analysis.is_computed ())
then main_ui#launcher ()
let cleaned_outputs kf s =
@@ -233,7 +233,7 @@ let cleaned_outputs kf s =
let pretty_stmt_info (main_ui:main_ui) kf stmt =
(* Is it an accessible statement ? *)
- if Db.Value.is_reachable_stmt stmt then begin
+ if Results.is_reachable stmt then begin
if Value_results.is_non_terminating_instr stmt then
match stmt.skind with
| Instr (Call (_, _, _, _)
@@ -412,7 +412,7 @@ module Select (Eval: Eval) = struct
(if unfocus <> [] then (kf, unfocus) :: acc_unfocus else acc_unfocus)
in
let focused, unfocused =
- List.fold_left aux_focus ([], []) (!Db.Value.callers kf)
+ List.fold_left aux_focus ([], []) (Results.callsites kf)
in
List.iter (aux menu) focused;
if unfocused <> [] then
@@ -521,7 +521,12 @@ module Select (Eval: Eval) = struct
(* Function pointers *)
(* get the list of functions in the values *)
let e = Value_util.lval_to_exp lv in
- match Eval.Analysis.get_kinstr_state ~after:false ki with
+ let state =
+ match ki with
+ | Kglobal -> Eval.Analysis.get_global_state ()
+ | Kstmt stmt -> Eval.Analysis.get_stmt_state ~after:false stmt
+ in
+ match state with
| `Bottom -> ()
| `Value state ->
let funs, _ = Eval.Analysis.eval_function_exp state e in
@@ -555,7 +560,7 @@ let responses_ref = ref (module No_Response: Responses)
let to_do_on_select (menu:menu) (main_ui:main_ui) ~button selected =
let module Responses = (val !responses_ref) in
- if Db.Value.is_computed () then
+ if Analysis.is_computed () then
if button = 1 then
Responses.left_click_values_computed main_ui selected
else if button = 3 then
diff --git a/src/plugins/value/legacy/eval_terms.ml b/src/plugins/value/legacy/eval_terms.ml
index c36e84a45b30286e18f983451fdff6d6a4171a81..a75bfed0d139992f8f602c3218285215a1101720 100644
--- a/src/plugins/value/legacy/eval_terms.ml
+++ b/src/plugins/value/legacy/eval_terms.ml
@@ -2745,6 +2745,16 @@ and predicate_deps env pred =
try Some (do_eval env pred)
with LogicEvalError _ -> None
+let annot_predicate_deps ~pre ~here predicate =
+ let env = env_annot ~pre ~here () in
+ let logic_deps = predicate_deps env predicate in
+ let join logic_deps =
+ Cil_datatype.Logic_label.Map.fold
+ (fun _ -> Locations.Zone.join)
+ logic_deps
+ Locations.Zone.bottom
+ in
+ Option.map join logic_deps
(* -------------------------------------------------------------------------- *)
(* --- Export --- *)
diff --git a/src/plugins/value/legacy/eval_terms.mli b/src/plugins/value/legacy/eval_terms.mli
index e63e6a531800d52ccbbbfc1ca29564cb2e27ef70..cff8567815ab453e72462ac147747305a2604fb3 100644
--- a/src/plugins/value/legacy/eval_terms.mli
+++ b/src/plugins/value/legacy/eval_terms.mli
@@ -52,14 +52,15 @@ exception LogicEvalError of logic_evaluation_error
type labels_states = Cvalue.Model.t Cil_datatype.Logic_label.Map.t
(** Evaluation environment. Currently available are function Pre and Post, or
- the environment to evaluate an annotation *)
+ the environment to evaluate an annotation. *)
type eval_env
val make_env: Model.t Abstract_domain.logic_environment -> Model.t -> eval_env
val env_pre_f : pre:Model.t -> unit -> eval_env
val env_annot :
- ?c_labels:labels_states -> pre:Model.t -> here:Model.t -> unit -> eval_env
+ ?c_labels:labels_states -> pre:Cvalue.Model.t -> here:Cvalue.Model.t ->
+ unit -> eval_env
val env_post_f :
?c_labels:labels_states -> pre:Model.t -> post:Model.t ->
result:varinfo option -> unit -> eval_env
@@ -71,7 +72,7 @@ val env_only_here: Model.t -> eval_env
val env_current_state: eval_env -> Model.t
(** Dependencies needed to evaluate a term or a predicate *)
-type logic_deps = Zone.t Cil_datatype.Logic_label.Map.t
+type logic_deps = Locations.Zone.t Cil_datatype.Logic_label.Map.t
(** Three modes to handle the alarms when evaluating a logical term. *)
type alarm_mode =
@@ -110,7 +111,22 @@ val eval_tlval_as_zone :
val eval_predicate :
eval_env -> predicate -> predicate_status
-val predicate_deps: eval_env -> predicate -> logic_deps option
+(** [predicate_deps env p] computes the logic dependencies needed to evaluate
+ [p] in the given evaluation environment [env].
+ Returns None on either an evaluation error or on unsupported construct. *)
+val predicate_deps: eval_env -> Cil_types.predicate -> logic_deps option
val reduce_by_predicate :
eval_env -> bool -> predicate -> eval_env
+
+
+
+[@@@ api_start]
+(** [annot_predicate_deps ~pre ~here p] computes the logic dependencies needed
+ to evaluate the predicate [p] in a code annotation in cvalue state [here],
+ in a function whose pre-state is [pre].
+ Returns None on either an evaluation error or on unsupported construct. *)
+val annot_predicate_deps:
+ pre:Cvalue.Model.t -> here:Cvalue.Model.t ->
+ Cil_types.predicate -> Locations.Zone.t option
+[@@@ api_end]
diff --git a/src/plugins/value/register.ml b/src/plugins/value/register.ml
index 2e585515cff0920c414234bc28d18bad920f517f..2db4de10b3a0bc336b41126a07a126c0e2a181ae 100644
--- a/src/plugins/value/register.ml
+++ b/src/plugins/value/register.ml
@@ -23,14 +23,9 @@
open Cil_types
open Locations
-let compute () =
- (* Nothing to recompute when Value has already been computed. This boolean
- is automatically cleared when an option of Value changes, because they
- are registered as dependencies on [Db.Value.self] in {!Value_parameters}.*)
- if not (Db.Value.is_computed ()) then Analysis.force_compute ()
-
-let _self =
- Db.register_compute "Value.compute" [ Db.Value.self ] Db.Value.compute compute
+let [@alert "-deprecated"] _self =
+ Db.register_compute "Value.compute" [ Db.Value.self ] Db.Value.compute
+ Analysis.compute
let () = Value_parameters.ForceValues.set_output_dependencies [Db.Value.self]
diff --git a/src/plugins/value/register.mli b/src/plugins/value/register.mli
index c27dd17263fd3f5deb3581b5ebdd0f6c3b2674f5..0f54ee776453869a4b44e2675c264a5535429fb9 100644
--- a/src/plugins/value/register.mli
+++ b/src/plugins/value/register.mli
@@ -20,6 +20,9 @@
(* *)
(**************************************************************************)
-(** Functions of the Value plugin registered in {!Db}.
+(** Functions of the Value plugin registered in {!Db}. Only three functions
+ are exported. *)
- Nothing is exported. *)
+val eval_deps : Cvalue_domain.State.t -> Cil_types.exp -> Locations.Zone.t
+val eval_deps_lval : Cvalue_domain.State.t -> Cil_types.lval -> Locations.Zone.t
+val eval_deps_addr : Cvalue_domain.State.t -> Cil_types.lval -> Locations.Zone.t
diff --git a/src/plugins/value/utils/eva_annotations.mli b/src/plugins/value/utils/eva_annotations.mli
index df768e5a1fbb96dc022afa594ca4a5ab9d4fc1a7..5b206536c557f1b287c1c7ea9a76d2759642d370 100644
--- a/src/plugins/value/utils/eva_annotations.mli
+++ b/src/plugins/value/utils/eva_annotations.mli
@@ -20,23 +20,28 @@
(* *)
(**************************************************************************)
-(** Registers Eva annotations:
+(* Note: widen hints annotations are still registered in !{widen_hints_ext.ml}. *)
+
+[@@@ api_start]
+(** Register special annotations to locally guide the Eva analysis:
+
- slevel annotations: "slevel default", "slevel merge" and "slevel i"
- loop unroll annotations: "loop unroll term"
- value partitioning annotations: "split term" and "merge term"
- subdivision annotations: "subdivide i"
+*)
- Widen hints annotations are still registered in !{widen_hints_ext.ml}. *)
-
+(** Annotations tweaking the behavior of the -eva-slevel parameter. *)
type slevel_annotation =
- | SlevelMerge
- | SlevelDefault
- | SlevelLocal of int
- | SlevelFull
+ | SlevelMerge (** Join all states separated by slevel. *)
+ | SlevelDefault (** Use the limit defined by -eva-slevel. *)
+ | SlevelLocal of int (** Use the given limit instead of -eva-slevel. *)
+ | SlevelFull (** Remove the limit of number of separated states. *)
+(** Loop unroll annotations. *)
type unroll_annotation =
- | UnrollAmount of Cil_types.term
- | UnrollFull
+ | UnrollAmount of Cil_types.term (** Unroll the n first iterations. *)
+ | UnrollFull (** Unroll amount defined by -eva-default-loop-unroll. *)
type split_kind = Static | Dynamic
@@ -44,9 +49,12 @@ type split_term =
| Expression of Cil_types.exp
| Predicate of Cil_types.predicate
+(** Split/merge annotations for value partitioning. *)
type flow_annotation =
| FlowSplit of split_term * split_kind
+ (** Split states according to a term. *)
| FlowMerge of split_term
+ (** Merge states separated by a previous split. *)
type allocation_kind = By_stack | Fresh | Fresh_weak | Imprecise
@@ -64,3 +72,4 @@ val add_flow_annot : emitter:Emitter.t ->
Cil_types.stmt -> flow_annotation -> unit
val add_subdivision_annot : emitter:Emitter.t ->
Cil_types.stmt -> int -> unit
+[@@@ api_end]
diff --git a/src/plugins/value/utils/results.ml b/src/plugins/value/utils/results.ml
new file mode 100644
index 0000000000000000000000000000000000000000..87a2ee9758f3ede02bd347959d77a58f4da61270
--- /dev/null
+++ b/src/plugins/value/utils/results.ml
@@ -0,0 +1,686 @@
+(**************************************************************************)
+(* *)
+(* This file is part of Frama-C. *)
+(* *)
+(* Copyright (C) 2007-2021 *)
+(* CEA (Commissariat à l'énergie atomique et aux énergies *)
+(* alternatives) *)
+(* *)
+(* you can redistribute it and/or modify it under the terms of the GNU *)
+(* Lesser General Public License as published by the Free Software *)
+(* Foundation, version 2.1. *)
+(* *)
+(* It is distributed in the hope that it will be useful, *)
+(* but WITHOUT ANY WARRANTY; without even the implied warranty of *)
+(* MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the *)
+(* GNU Lesser General Public License for more details. *)
+(* *)
+(* See the GNU Lesser General Public License version 2.1 *)
+(* for more details (enclosed in the file licenses/LGPLv2.1). *)
+(* *)
+(**************************************************************************)
+
+open Bottom.Type
+
+type 'a or_top_bottom = 'a Bottom.Top.or_top_bottom
+
+let (>>>-:) t f = match t with
+ | `Top -> `Top
+ | `Bottom -> `Bottom
+ | `Value t -> `Value (f t)
+
+module Callstack = Value_types.Callstack
+
+type callstack = Callstack.t
+type 'a by_callstack = (callstack * 'a) list
+
+type control_point =
+ | Initial
+ | Start of Cil_types.kernel_function
+ | Before of Cil_types.stmt
+ | After of Cil_types.stmt
+
+type request = {
+ control_point : control_point;
+ selector : callstack list option;
+ filter: (callstack -> bool) list;
+}
+
+type error = Bottom | Top | DisabledDomain
+type 'a result = ('a,error) Result.t
+
+let string_of_error = function
+ | Bottom -> "The computed state is bottom"
+ | Top -> "The computed state is Top"
+ | DisabledDomain -> "The required domain is disabled"
+
+let pretty_error fmt error =
+ Format.pp_print_string fmt (string_of_error error)
+let pretty_result f fmt r =
+ Result.fold ~ok:(f fmt) ~error:(pretty_error fmt) r
+
+
+(* Building requests *)
+
+let make control_point = {
+ control_point;
+ selector = None;
+ filter = [];
+}
+
+let before stmt = make (Before stmt)
+let after stmt = make (After stmt)
+let at_start_of kf = make (Start kf)
+let at_end_of kf = make (After (Kernel_function.find_return kf))
+let at_start = make Initial
+let at_end () = at_end_of (fst (Globals.entry_point ()))
+
+let before_kinstr = function
+ | Cil_types.Kglobal -> at_start
+ | Kstmt stmt -> before stmt
+
+let in_callstacks l req = { req with selector = Some l }
+let in_callstack cs req = { req with selector = Some [cs] }
+let filter_callstack f req = { req with filter = f :: req.filter }
+
+
+(* Manipulating request results *)
+
+type restricted_to_callstack
+type unrestricted_response
+
+module Response =
+struct
+
+ type ('a, 'callstack) t =
+ | Consolidated : 'a -> ('a, unrestricted_response) t
+ | ByCallstack : 'a by_callstack -> ('a, 'callstack) t
+ | Top : ('a, 'callstack) t
+ | Bottom : ('a, 'callstack) t
+
+ let coercion : ('a, restricted_to_callstack) t -> ('a, 'c) t = function
+ | ByCallstack c -> ByCallstack c
+ | Top -> Top
+ | Bottom -> Bottom
+
+ let is_bottom = function
+ | ByCallstack [] | Bottom -> true
+ | _ -> false
+
+ (* Constructors *)
+
+ let consolidated =
+ function
+ | `Bottom -> Bottom
+ | `Value state -> Consolidated state
+
+ let singleton cs =
+ function
+ | `Bottom -> Bottom
+ | `Value state -> ByCallstack [cs,state]
+
+ let by_callstack : request ->
+ [< `Bottom | `Top | `Value of 'a Value_types.Callstack.Hashtbl.t ] ->
+ ('a, restricted_to_callstack) t =
+ fun req table ->
+ match table with
+ | `Top -> Top
+ | `Bottom -> Bottom
+ | `Value table ->
+ (* Filter *)
+ let add cs state acc =
+ if List.for_all (fun filter -> filter cs) req.filter
+ then (cs, state) :: acc
+ else acc
+ in
+ (* Selection *)
+ let l =
+ match req.selector with
+ | None -> Callstack.Hashtbl.fold add table []
+ | Some selector ->
+ let add acc cs =
+ match Callstack.Hashtbl.find_opt table cs with
+ | Some state -> add cs state acc
+ | None -> acc
+ in
+ List.fold_left add [] selector
+ in
+ ByCallstack l
+
+ (* Accessors *)
+
+ let callstacks : ('a, restricted_to_callstack) t -> callstack list = function
+ | Top | Bottom -> [] (* What else to do when Top is given ? *)
+ | ByCallstack l -> List.map fst l
+
+ (* Fold *)
+
+ let fold (f : callstack -> 'a -> 'b -> 'b) (acc : 'b) :
+ ('a, restricted_to_callstack) t -> 'b =
+ function
+ | Top | Bottom -> acc (* What else to do when Top is given ? *)
+ | ByCallstack l -> List.fold_left (fun acc (cs,x) -> f cs x acc) acc l
+
+ (* Map *)
+
+ let map : type c. ('a -> 'b) -> ('a, c) t -> ('b, c) t = fun f -> function
+ | Consolidated v -> Consolidated (f v)
+ | ByCallstack l -> ByCallstack (List.map (fun (cs,x) -> cs,f x) l)
+ | Top -> Top
+ | Bottom -> Bottom
+
+ (* Reduction *)
+
+ let map_reduce : type c. ([`Top | `Bottom] -> 'b) -> ('a -> 'b) ->
+ ('b -> 'b -> 'b) -> ('a, c) t -> 'b =
+ fun default map reduce -> function
+ | Consolidated v -> map v
+ | ByCallstack ((_,h) :: t) ->
+ List.fold_left (fun acc (_,x) -> reduce acc (map x)) (map h) t
+ | ByCallstack [] | Bottom -> default `Bottom
+ | Top -> default `Top
+
+ let default = function
+ | `Bottom -> `Bottom
+ | `Top -> `Top
+
+ let map_join : type c.
+ ('a -> 'b) -> ('b -> 'b -> 'b) -> ('a, c) t -> 'b or_top_bottom =
+ fun map join ->
+ let map' x = `Value (map x) in
+ map_reduce default map' (Bottom.Top.join join)
+
+ let map_join' : type c. ('a -> 'b or_top_bottom) -> ('b -> 'b -> 'b) ->
+ ('a, c) t -> 'b or_top_bottom =
+ fun map join ->
+ map_reduce default map (Bottom.Top.join join)
+end
+
+
+(* Extracting states and values *)
+
+type value
+type address
+
+module Make () =
+struct
+ module A = (val Analysis.current_analyzer ())
+
+ module EvalTypes =
+ struct
+ type valuation = A.Eval.Valuation.t
+ type exp = (valuation * A.Val.t) Eval.evaluated
+ type lval = (valuation * A.Val.t Eval.flagged_value) Eval.evaluated
+ type loc = (valuation * A.Loc.location * Cil_types.typ) Eval.evaluated
+ end
+
+ type ('a,'c) evaluation =
+ | LValue: (EvalTypes.lval, 'c) Response.t -> (value,'c) evaluation
+ | Value: (EvalTypes.exp, 'c) Response.t -> (value,'c) evaluation
+ | Address: (EvalTypes.loc, 'c) Response.t * Cil_types.lval ->
+ (address,'c) evaluation
+
+ let get_by_callstack (req : request) :
+ (_, restricted_to_callstack) Response.t =
+ let open Response in
+ match req.control_point with
+ | Before stmt ->
+ A.get_stmt_state_by_callstack ~after:false stmt |> by_callstack req
+ | After stmt ->
+ A.get_stmt_state_by_callstack ~after:true stmt |> by_callstack req
+ | Initial ->
+ A.get_global_state () |> singleton []
+ | Start kf ->
+ A.get_initial_state_by_callstack kf |> by_callstack req
+
+ let get (req : request) : (_, unrestricted_response) Response.t =
+ if req.filter <> [] || Option.is_some req.selector then
+ Response.coercion @@ get_by_callstack req
+ else
+ let open Response in
+ let state =
+ match req.control_point with
+ | Before stmt -> A.get_stmt_state ~after:false stmt
+ | After stmt -> A.get_stmt_state ~after:true stmt
+ | Start kf -> A.get_initial_state kf
+ | Initial -> A.get_global_state ()
+ in
+ consolidated state
+
+ let convert : 'a or_top_bottom -> 'a result = function
+ | `Top -> Result.error Top
+ | `Bottom -> Result.error Bottom
+ | `Value v -> Result.ok v
+
+ let callstacks req =
+ get_by_callstack req |> Response.callstacks
+
+ let by_callstack req =
+ let f cs _res acc =
+ (cs, in_callstack cs req) :: acc
+ in
+ get_by_callstack req |> Response.fold f []
+
+ let is_reachable req =
+ match get req with
+ | Bottom -> false
+ | _ -> true
+
+ let equality_class exp req =
+ let open Equality in
+ match A.Dom.get Equality_domain.key with
+ | None ->
+ Result.error DisabledDomain
+ | Some extract ->
+ let hce = Hcexprs.HCE.of_exp exp in
+ let extract' state =
+ let equalities = Equality_domain.project (extract state) in
+ try NonTrivial (Set.find hce equalities)
+ with Not_found -> Trivial
+ and reduce e1 e2 =
+ match e1, e2 with
+ | Trivial, _ | _, Trivial -> Trivial
+ | NonTrivial e1, NonTrivial e2 -> Equality.inter e1 e2
+ in
+ let r = match Response.map_join extract' reduce (get req) with
+ | (`Top | `Bottom) as r -> r
+ | `Value Trivial -> `Top
+ | `Value (NonTrivial e) ->
+ let l = Equality.elements e in
+ `Value (List.map Hcexprs.HCE.to_exp l)
+ in
+ convert r
+
+ let get_cvalue_model req =
+ match A.Dom.get_cvalue with
+ | None ->
+ Result.error DisabledDomain
+ | Some extract ->
+ convert (Response.map_join extract Cvalue.Model.join (get req))
+
+ (* Evaluation *)
+
+ let eval_lval lval req =
+ let eval state = A.Eval.copy_lvalue state lval in
+ LValue (Response.map eval (get req))
+
+ let eval_exp exp req =
+ let eval state = A.Eval.evaluate state exp in
+ Value (Response.map eval (get req))
+
+ let eval_address lval req =
+ let eval state = A.Eval.lvaluate ~for_writing:false state lval in
+ Address (Response.map eval (get req), lval)
+
+ let eval_callee exp req =
+ let join = (@)
+ and extract state =
+ let r,_alarms = A.Eval.eval_function_exp exp state in
+ r >>>-: List.map fst
+ in
+ get req |> Response.map_join' extract join |> convert |>
+ Result.map (List.sort_uniq Kernel_function.compare)
+
+
+ (* Conversion *)
+
+ let extract_value :
+ type c. (value, c) evaluation -> (A.Val.t or_bottom, c) Response.t =
+ function
+ | LValue r ->
+ let extract (x, _alarms) = x >>- (fun (_valuation,fv) -> fv.Eval.v) in
+ Response.map extract r
+ | Value r ->
+ let extract (x, _alarms) = x >>-: (fun (_valuation,v) -> v) in
+ Response.map extract r
+
+ let as_cvalue res =
+ match A.Val.get Main_values.CVal.key with
+ | None ->
+ Result.error DisabledDomain
+ | Some get ->
+ let join = Main_values.CVal.join in
+ let extract value =
+ value >>>-: get
+ in
+ extract_value res |> Response.map_join' extract join |> convert
+
+ let extract_loc :
+ type c. (address, c) evaluation ->
+ (A.Loc.location or_bottom, c) Response.t * Cil_types.lval =
+ function
+ | Address (r, lval) ->
+ let extract (x, _alarms) = x >>-: (fun (_valuation,loc,_typ) -> loc) in
+ Response.map extract r, lval
+
+ let as_location res =
+ match A.Loc.get Main_locations.PLoc.key with
+ | None ->
+ Result.error DisabledDomain
+ | Some get ->
+ let join loc1 loc2 =
+ let open Locations in
+ let size = loc1.size
+ and loc = Location_Bits.join loc1.loc loc2.loc in
+ assert (Int_Base.equal loc2.size size);
+ make_loc loc size
+ and extract loc =
+ loc >>>-: get >>>-: Precise_locs.imprecise_location
+ in
+ extract_loc res |> fst |> Response.map_join' extract join |> convert
+
+ let as_zone ~access res =
+ let response_loc, lv = extract_loc res in
+ let is_const_lv = Value_util.is_const_write_invalid (Cil.typeOfLval lv) in
+ (* No write effect if [lv] is const *)
+ if access=Locations.Write && is_const_lv
+ then Result.ok Locations.Zone.bottom
+ else
+ match A.Loc.get Main_locations.PLoc.key with
+ | None ->
+ Result.error DisabledDomain
+ | Some get ->
+ let join = Locations.Zone.join
+ and extract loc =
+ loc >>>-: get >>>-: Precise_locs.enumerate_valid_bits access
+ in
+ response_loc |> Response.map_join' extract join |> convert
+
+ let is_initialized : type c. (value,c) evaluation -> bool =
+ function
+ | LValue r ->
+ let join = (&&)
+ and extract (x, _alarms) =
+ x >>>-: (fun (_valuation,fv) -> fv.Eval.initialized)
+ in
+ begin match Response.map_join' extract join r with
+ | `Bottom | `Top -> false
+ | `Value v -> v
+ end
+ | Value _ -> true (* computed values are always initialized *)
+
+ let alarms : type a c. (a,c) evaluation -> Alarms.t list =
+ fun res ->
+ let extract (_,v) = `Value v in
+ let r = match res with
+ | LValue r ->
+ Response.map_join' extract Alarmset.union r
+ | Value r ->
+ Response.map_join' extract Alarmset.union r
+ | Address (r, _lval) ->
+ Response.map_join' extract Alarmset.union r
+ in
+ match r with
+ | `Bottom | `Top -> []
+ | `Value alarmset ->
+ let add alarm status acc =
+ if status <> Alarmset.True then alarm :: acc else acc
+ in
+ Alarmset.fold add [] alarmset
+
+ let is_bottom : type a c. (a,c) evaluation -> bool = function
+ | LValue r -> Response.is_bottom r
+ | Value r -> Response.is_bottom r
+ | Address (r, _lval) -> Response.is_bottom r
+
+ (* Dependencies *)
+
+ let compute_deps eval_deps arg req =
+ let error = function
+ | Bottom -> Locations.Zone.bottom
+ | Top | DisabledDomain -> Locations.Zone.top
+ in
+ let compute cvalue =
+ eval_deps (cvalue, Locals_scoping.bottom ()) arg
+ in
+ req |> get_cvalue_model |> Result.fold ~error ~ok:compute
+
+ let lval_deps = compute_deps Register.eval_deps_lval
+ let expr_deps = compute_deps Register.eval_deps
+ let address_deps = compute_deps Register.eval_deps_addr
+end
+
+
+(* Working with callstacks *)
+
+let callstacks req =
+ let module E = Make () in
+ E.callstacks req
+
+let by_callstack req =
+ let module E = Make () in
+ E.by_callstack req
+
+
+(* State requests *)
+
+let equality_class exp req =
+ let module E = Make () in
+ E.equality_class exp req
+
+let get_cvalue_model_result req =
+ let module E = Make () in
+ E.get_cvalue_model req
+
+let get_cvalue_model req =
+ match get_cvalue_model_result req with
+ | Ok state -> state
+ | Error Bottom -> Cvalue.Model.bottom
+ | Error (Top | DisabledDomain) -> Cvalue.Model.top
+
+
+(* Depedencies *)
+
+let expr_deps exp req =
+ let module E = Make () in
+ E.expr_deps exp req
+
+let lval_deps lval req =
+ let module E = Make () in
+ E.lval_deps lval req
+
+let address_deps lval req =
+ let module E = Make () in
+ E.address_deps lval req
+
+
+(* Evaluation *)
+
+module type Lvaluation =
+sig
+ include module type of (Make ())
+ val v : (address, unrestricted_response) evaluation
+end
+
+module type Evaluation =
+sig
+ include module type of (Make ())
+ val v : (value, unrestricted_response) evaluation
+end
+
+type 'a evaluation =
+ | Value: (module Evaluation) -> value evaluation
+ | Address: (module Lvaluation) -> address evaluation
+
+let build_eval_lval_and_exp () =
+ let module M = Make () in
+ let build v =
+ (module struct
+ include M
+ let v = v
+ end : Evaluation)
+ in
+ let eval_lval lval req = build @@ M.eval_lval lval req in
+ let eval_exp exp req = build @@ M.eval_exp exp req in
+ eval_lval, eval_exp
+
+let eval_lval lval req = Value ((fst @@ build_eval_lval_and_exp ()) lval req)
+
+let eval_var vi req = eval_lval (Cil.var vi) req
+
+let eval_exp exp req = Value ((snd @@ build_eval_lval_and_exp ()) exp req)
+
+let eval_address lval req =
+ let module M = Make () in
+ let v = M.eval_address lval req in
+ Address
+ (module struct
+ include M
+ let v = v
+ end : Lvaluation)
+
+let eval_callee exp req =
+ (* Check the validity of exp *)
+ begin match exp with
+ | Cil_types.({ enode = Lval (_, NoOffset) }) -> ()
+ | _ ->
+ invalid_arg "The callee must be an lvalue with no offset"
+ end;
+ let module M = Make () in
+ M.eval_callee exp req
+
+let callee stmt =
+ let callee_exp =
+ match stmt.Cil_types.skind with
+ | Instr (Call (_lval, callee_exp, _args, _loc)) ->
+ callee_exp
+ | Instr (Local_init (_vi, ConsInit (f, _, _), _loc)) ->
+ Cil.evar f
+ | _ ->
+ invalid_arg "Can only evaluate the callee on a statement which is a Call"
+ in
+ before stmt |> eval_callee callee_exp |> Result.value ~default:[]
+
+(* Value conversion *)
+
+let as_cvalue_result (Value evaluation) =
+ let module E = (val evaluation : Evaluation) in
+ E.as_cvalue E.v
+
+let as_cvalue evaluation =
+ match as_cvalue_result evaluation with
+ | Ok v -> v
+ | Error Bottom -> Cvalue.V.bottom
+ | Error (Top | DisabledDomain) -> Cvalue.V.top
+
+let as_ival evaluation =
+ try
+ Result.map Cvalue.V.project_ival (as_cvalue_result evaluation)
+ with Cvalue.V.Not_based_on_null ->
+ Result.error Top
+
+let as_fval evaluation =
+ let f ival =
+ if Ival.is_float ival
+ then Result.ok (Ival.project_float ival)
+ else Result.error Top
+ in
+ Result.bind (as_ival evaluation) f
+
+let as_float evaluation =
+ try
+ as_fval evaluation |>
+ Result.map Fval.project_float |>
+ Result.map Fval.F.to_float
+ with Fval.Not_Singleton_Float ->
+ Result.error Top
+
+let as_integer evaluation =
+ try
+ Result.map Ival.project_int (as_ival evaluation)
+ with Ival.Not_Singleton_Int ->
+ Result.error Top
+
+let as_int evaluation =
+ try
+ Result.map Integer.to_int_exn (as_integer evaluation)
+ with Z.Overflow ->
+ Result.error Top
+
+let as_location (Address lvaluation) =
+ let module E = (val lvaluation : Lvaluation) in
+ E.as_location E.v
+
+let as_zone_result ?(access=Locations.Read) (Address lvaluation) =
+ let module E = (val lvaluation : Lvaluation) in
+ E.as_zone ~access E.v
+
+let as_zone ?access address =
+ match as_zone_result ?access address with
+ | Ok zone -> zone
+ | Error Bottom -> Locations.Zone.bottom
+ | Error (Top | DisabledDomain) -> Locations.Zone.top
+
+(* Evaluation properties *)
+
+let is_initialized (Value evaluation) =
+ let module E = (val evaluation : Evaluation) in
+ E.is_initialized E.v
+
+let alarms : type a. a evaluation -> Alarms.t list =
+ function
+ | Value evaluation ->
+ let module E = (val evaluation : Evaluation) in
+ E.alarms E.v
+ | Address lvaluation ->
+ let module L = (val lvaluation : Lvaluation) in
+ L.alarms L.v
+
+(* Reachability *)
+
+let is_empty rq =
+ let module E = Make () in
+ E.callstacks rq = []
+
+let is_bottom : type a. a evaluation -> bool =
+ function
+ | Value evaluation ->
+ let module E = (val evaluation : Evaluation) in
+ E.is_bottom E.v
+ | Address lvaluation ->
+ let module L = (val lvaluation : Lvaluation) in
+ L.is_bottom L.v
+
+let is_called kf =
+ let module M = Make () in
+ M.is_reachable (at_start_of kf)
+
+let is_reachable stmt =
+ let module M = Make () in
+ M.is_reachable (before stmt)
+
+let is_reachable_kinstr kinstr =
+ let module M = Make () in
+ M.is_reachable (before_kinstr kinstr)
+
+
+(* Callers / callsites *)
+
+let callers kf =
+ let f = function
+ | [] | [_] -> None
+ | _ :: (caller,_) :: _-> Some caller
+ in
+ at_start_of kf |> callstacks |>
+ List.filter_map f |> List.sort_uniq Kernel_function.compare
+
+let uniq_sites = List.sort_uniq Cil_datatype.Stmt.compare
+
+let callsites kf =
+ let module Map = Kernel_function.Map in
+ let f acc = function
+ | [] | (_,Cil_types.Kglobal) :: _ -> acc
+ | [(_,Kstmt _)] -> assert false (* End of callstacks should have no callsite *)
+ | (_kf,Kstmt stmt) :: (caller,_) :: _ -> (* kf = _kf *)
+ Map.update caller
+ (fun old -> Some (stmt :: Option.value ~default:[] old)) acc
+ in
+ at_start_of kf |> callstacks |>
+ List.fold_left f Map.empty |> Map.to_seq |> List.of_seq |>
+ List.map (fun (kf,sites) -> kf, uniq_sites sites)
+
+
+(* Result conversion *)
+
+let default default_value result =
+ Result.value ~default:default_value result
diff --git a/src/plugins/value/utils/results.mli b/src/plugins/value/utils/results.mli
new file mode 100644
index 0000000000000000000000000000000000000000..e24441ccb68a3473d768a8129ee28eb45eb12fe0
--- /dev/null
+++ b/src/plugins/value/utils/results.mli
@@ -0,0 +1,289 @@
+(**************************************************************************)
+(* *)
+(* This file is part of Frama-C. *)
+(* *)
+(* Copyright (C) 2007-2021 *)
+(* CEA (Commissariat à l'énergie atomique et aux énergies *)
+(* alternatives) *)
+(* *)
+(* you can redistribute it and/or modify it under the terms of the GNU *)
+(* Lesser General Public License as published by the Free Software *)
+(* Foundation, version 2.1. *)
+(* *)
+(* It is distributed in the hope that it will be useful, *)
+(* but WITHOUT ANY WARRANTY; without even the implied warranty of *)
+(* MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the *)
+(* GNU Lesser General Public License for more details. *)
+(* *)
+(* See the GNU Lesser General Public License version 2.1 *)
+(* for more details (enclosed in the file licenses/LGPLv2.1). *)
+(* *)
+(**************************************************************************)
+
+[@@@ api_start]
+(** Eva's result API is a work-in-progress interface to allow accessing the
+ analysis results once its completed. It is experimental and is very likely
+ to change in the future. It aims at replacing [Db.Value] but does not
+ completely covers all its usages yet. As for now, this interface has some
+ advantages over Db's :
+
+ - evaluations uses every available domains and not only Cvalue;
+ - the caller may distinguish failure cases when a request is unsucessful;
+ - working with callstacks is easy;
+ - some common shortcuts are provided (e.g. for extracting ival directly);
+ - overall, individual functions are simpler.
+
+ The idea behind this API is that requests must be decomposed in several
+ steps. For instance, to evaluate an expression :
+
+ 1. first, you have to state where you want to evaluate it,
+ 2. optionally, you may specify in which callstack,
+ 3. you choose the expression to evaluate,
+ 4. you require a destination type to evaluate into.
+
+ Usage sketch :
+
+ Eva.Results.(
+ before stmt |> in_callstack cs |>
+ eval_var vi |> as_int |> default 0)
+
+ or equivalently, if you prefer
+
+ Eva.Results.(
+ default O (as_int (eval_var vi (in_callstack cs (before stmt))))
+*)
+
+
+type callstack = (Cil_types.kernel_function * Cil_types.kinstr) list
+
+type request
+
+type value
+type address
+type 'a evaluation
+
+type error = Bottom | Top | DisabledDomain
+type 'a result = ('a,error) Result.t
+
+
+(** Results handling *)
+
+(** Translates an error to a human readable string. *)
+val string_of_error : error -> string
+
+(** Pretty printer for errors. *)
+val pretty_error : Format.formatter -> error -> unit
+
+(** Pretty printer for API's results. *)
+val pretty_result : (Format.formatter -> 'a -> unit) ->
+ Format.formatter -> 'a result -> unit
+
+(** [default d r] extracts the value of [r] if [r] is Ok,
+ or use the default value [d] otherwise.
+ Equivalent to [Result.value ~default:d r] *)
+val default : 'a -> 'a result -> 'a
+
+
+(** Control point selection *)
+
+(** At the start of the analysis, but after the initialization of globals. *)
+val at_start : request
+
+(** At the end of the analysis, after the main function has returned. *)
+val at_end : unit -> request
+
+(** At the start of the given function. *)
+val at_start_of : Cil_types.kernel_function -> request
+
+(** At the end of the given function.
+ @raises Kernel_function.No_statement if the function has no body. *)
+val at_end_of : Cil_types.kernel_function -> request
+
+(** Just before a statement is executed. *)
+val before : Cil_types.stmt -> request
+
+(** Just after a statement is executed. *)
+val after : Cil_types.stmt -> request
+
+(** Just before a statement or at the start of the analysis. *)
+val before_kinstr : Cil_types.kinstr -> request
+
+
+(** Callstack selection *)
+
+(** Only consider the given callstack.
+ Replaces previous calls to [in_callstack] or [in_callstacks]. *)
+val in_callstack : callstack -> request -> request
+
+(** Only consider the callstacks from the given list.
+ Replaces previous calls to [in_callstack] or [in_callstacks]. *)
+val in_callstacks : callstack list -> request -> request
+
+(** Only consider callstacks satisfying the given predicate. Several filters
+ can be added. If callstacks are also selected with [in_callstack] or
+ [in_callstacks], only the selected callstacks will be filtered. *)
+val filter_callstack : (callstack -> bool) -> request -> request
+
+
+(** Working with callstacks *)
+
+(** Returns the list of reachable callstacks from the given request.
+ An empty list is returned if the request control point has not been
+ reached by the analysis, or if no information has been saved at this point
+ (for instance with the -eva-no-results option).
+ Use [is_empty request] to distinguish these two cases. *)
+val callstacks : request -> callstack list
+
+(** Returns a list of subrequests for each reachable callstack from
+ the given request. *)
+val by_callstack : request -> (callstack * request) list
+
+
+(** State requests *)
+
+(** Returns the list of expressions which have been inferred to be equal to
+ the given expression by the Equality domain. *)
+val equality_class : Cil_types.exp -> request -> Cil_types.exp list result
+
+(** Returns the Cvalue state. Error cases are converted into the bottom or top
+ cvalue state accordingly. *)
+val get_cvalue_model : request -> Cvalue.Model.t
+
+(** Returns the Cvalue model. *)
+val get_cvalue_model_result : request -> Cvalue.Model.t result
+
+
+(** Dependencies *)
+
+(** Computes (an overapproximation of) the memory zones that must be read to
+ evaluate the given expression, including all adresses computations. *)
+val expr_deps : Cil_types.exp -> request -> Locations.Zone.t
+
+(** Computes (an overapproximation of) the memory zones that must be read to
+ evaluate the given lvalue, including the lvalue zone itself. *)
+val lval_deps : Cil_types.lval -> request -> Locations.Zone.t
+
+(** Computes (an overapproximation of) the memory zones that must be read to
+ evaluate the given lvalue, excluding the lvalue zone itself. *)
+val address_deps : Cil_types.lval -> request -> Locations.Zone.t
+
+
+(** Evaluation *)
+
+(** Returns (an overapproximation of) the possible values of the variable. *)
+val eval_var : Cil_types.varinfo -> request -> value evaluation
+
+(** Returns (an overapproximation of) the possible values of the lvalue. *)
+val eval_lval : Cil_types.lval -> request -> value evaluation
+
+(** Returns (an overapproximation of) the possible values of the expression. *)
+val eval_exp : Cil_types.exp -> request -> value evaluation
+
+
+(** Returns (an overapproximation of) the possible addresses of the lvalue. *)
+val eval_address : Cil_types.lval -> request -> address evaluation
+
+
+(** Returns the kernel functions into which the given expression may evaluate.
+ If the callee expression doesn't always evaluate to a function, those
+ spurious values are ignored. If it always evaluate to a non-function value
+ then the returned list is empty.
+ Raises [Stdlib.Invalid_argument] if the callee expression is not an lvalue
+ without offset.
+ Also see [callee] for a function which applies directly on Call
+ statements. *)
+val eval_callee : Cil_types.exp -> request -> Kernel_function.t list result
+
+
+(** Evaluated values conversion *)
+
+(** In all functions below, if the abstract value inferred by Eva does not fit
+ in the required type, [Error Top] is returned, as Top is the only possible
+ over-approximation of the request. *)
+
+(** Converts the value into a singleton ocaml int. *)
+val as_int : value evaluation -> int result
+
+(** Converts the value into a singleton unbounded integer. *)
+val as_integer : value evaluation -> Integer.t result
+
+(** Converts the value into a floating point number. *)
+val as_float : value evaluation -> float result
+
+(** Converts the value into a C number abstraction. *)
+val as_ival : value evaluation -> Ival.t result
+
+(** Converts the value into a floating point abstraction. *)
+val as_fval : value evaluation -> Fval.t result
+
+(** Converts the value into a Cvalue abstraction. Converts error cases
+ into bottom and top values accordingly. *)
+val as_cvalue : value evaluation -> Cvalue.V.t
+
+(** Converts the value into a Cvalue abstraction. *)
+val as_cvalue_result : value evaluation -> Cvalue.V.t result
+
+
+(** Converts into a C location abstraction. *)
+val as_location : address evaluation -> Locations.location result
+
+(** Converts into a Zone. Error cases are converted into bottom or top zones
+ accordingly. *)
+val as_zone: ?access:Locations.access -> address evaluation ->
+ Locations.Zone.t
+
+(** Converts into a Zone result. *)
+val as_zone_result : ?access:Locations.access -> address evaluation ->
+ Locations.Zone.t result
+
+
+(** Evaluation properties *)
+
+(** Returns whether the evaluated value is initialized or not. If the value have
+ been evaluated from a Cil expression, it is always initialized. *)
+val is_initialized : value evaluation -> bool
+
+(** Returns the set of alarms emitted during the evaluation. *)
+val alarms : 'a evaluation -> Alarms.t list
+
+
+(** Reachability *)
+
+(** Returns true if there are no reachable states for the given request. *)
+val is_empty : request -> bool
+
+(** Returns true if an evaluation leads to bottom, i.e. if the given expression
+ or lvalue cannot be evaluated to a valid result for the given request. *)
+val is_bottom : 'a evaluation -> bool
+
+(** Returns true if the function has been analyzed. *)
+val is_called : Cil_types.kernel_function -> bool
+
+(** Returns true if the statement has been reached by the analysis. *)
+val is_reachable : Cil_types.stmt -> bool
+
+(** Returns true if the statement has been reached by the analysis, or if
+ the main function has been analyzed for [Kglobal]. *)
+val is_reachable_kinstr : Cil_types.kinstr -> bool
+
+
+(*** Callers / Callees / Callsites *)
+
+(** Returns the list of inferred callers of the given function. *)
+val callers : Cil_types.kernel_function -> Cil_types.kernel_function list
+
+(** Returns the list of inferred callers, and for each of them, the list
+ of callsites (the call statements) inside. *)
+val callsites : Cil_types.kernel_function ->
+ (Cil_types.kernel_function * Cil_types.stmt list) list
+
+
+(** Returns the kernel functions called in the given statement.
+ If the callee expression doesn't always evaluate to a function, those
+ spurious values are ignored. If it always evaluate to a non-function value
+ then the returned list is empty.
+ Raises [Stdlib.Invalid_argument] if the statement is not a [Call]
+ instruction or a [Local_init] with [ConsInit] initializer. *)
+val callee : Cil_types.stmt -> Kernel_function.t list
+
+[@@@ api_end]
diff --git a/src/plugins/value/utils/unit_tests.mli b/src/plugins/value/utils/unit_tests.mli
index cf1fae9cef81e5104e4e6cb886c7a5170a7caa51..db0856b3653da1a60e995926306d1ba00e7fdcb2 100644
--- a/src/plugins/value/utils/unit_tests.mli
+++ b/src/plugins/value/utils/unit_tests.mli
@@ -20,8 +20,10 @@
(* *)
(**************************************************************************)
-(** Currently tested by this file:
+[@@@ api_start]
+(** Currently tested by this module:
- semantics of sign values. *)
(** Runs some programmatic tests on Eva. *)
val run: unit -> unit
+[@@@ api_end]
diff --git a/src/plugins/value/utils/value_results.mli b/src/plugins/value/utils/value_results.mli
index 9592d1e753f5eda07466e46e263863f903648115..bcfcd175ca6a8f2eb6fcd2612ffd26fbf34f1e50 100644
--- a/src/plugins/value/utils/value_results.mli
+++ b/src/plugins/value/utils/value_results.mli
@@ -20,22 +20,23 @@
(* *)
(**************************************************************************)
-(** This file will ultimately contain all the results computed by Value
- (which must be moved out of Db.Value), both per stack and globally. *)
-
-
open Cil_types
val is_called: kernel_function -> bool
val mark_kf_as_called: kernel_function -> unit
val add_kf_caller: caller:kernel_function * stmt -> kernel_function -> unit
+val callers: kernel_function -> (kernel_function*stmt list) list
+(** @return the list of callers with their call sites. Each function is
+ present only once in the list. *)
+
val is_non_terminating_instr: stmt -> bool
(** Returns [true] iff there exists executions of the statement that does
not always fail/loop (for function calls). Must be called *only* on
statements that are instructions. *)
(** {2 Results} *)
+[@@@ api_start]
type results
val get_results: unit -> results
@@ -46,6 +47,7 @@ val change_callstacks:
(** Change the callstacks for the results for which this is meaningful.
For technical reasons, the top of the callstack must currently
be preserved. *)
+[@@@ api_end]
(*
Local Variables:
diff --git a/src/plugins/value/value_parameters.mli b/src/plugins/value/value_parameters.mli
index a05cde2a46d6bbdf015865524e5dda608eb4d91d..14c4e47e61ae888414a7e61a743f6f1af796a0dc 100644
--- a/src/plugins/value/value_parameters.mli
+++ b/src/plugins/value/value_parameters.mli
@@ -230,16 +230,21 @@ val register_builtin: string -> unit
(** Registers available domain names for the -eva-domains option. *)
val register_domain: name:string -> descr:string -> unit
-(** Returns the list (name, descr) of currently enabled domains. *)
+[@@@ api_start]
+(** Configuration of the analysis. *)
+
+(** Returns the list (name, descr) of currently enabled abstract domains. *)
val enabled_domains: unit -> (string * string) list
-(** [use_builtin kf b] adds a builtin override for function `kf` to
- builtin `b`. *)
+(** [use_builtin kf name] instructs the analysis to use the builtin [name]
+ to interpret calls to function [kf].
+ Raises [Not_found] if there is no builtin of name [name]. *)
val use_builtin: Cil_types.kernel_function -> string -> unit
-(** [use_global_value_partitioning vi] enable value partitioning on the global
- variable `vi`. *)
+(** [use_global_value_partitioning vi] instructs the analysis to use
+ value partitioning on the global variable [vi]. *)
val use_global_value_partitioning: Cil_types.varinfo -> unit
+[@@@ api_end]
(*
Local Variables:
diff --git a/tests/crowbar/constfold.ml b/tests/crowbar/constfold.ml
index b98c69153c173ba6dd2cbae5cf252e3459196a44..91de9a16715a5ca908c76349ab5a0cc727b47c78 100644
--- a/tests/crowbar/constfold.ml
+++ b/tests/crowbar/constfold.ml
@@ -206,7 +206,7 @@ let run typ expr =
end;
File.prepare_cil_file cil;
Kernel.MainFunction.set "f";
- !Db.Value.compute ();
+ Eva.Analysis.compute ();
let kf = Globals.Functions.find_by_name "f" in
let r = Globals.Vars.find_from_astinfo "result" Cil_types.VGlobal in
let ret = Kernel_function.find_return kf in
diff --git a/tests/misc/bts1201.ml b/tests/misc/bts1201.ml
index 9e3c1b2a3ff07a05ed42787d1bf59decc41dee91..8cb421763f5dc9c46a3c61679a6413b458875578 100644
--- a/tests/misc/bts1201.ml
+++ b/tests/misc/bts1201.ml
@@ -1,7 +1,7 @@
let main () =
- !Db.Value.compute ();
+ Eva.Analysis.compute ();
Globals.set_entry_point "main2" false;
- !Db.Value.compute ();
+ Eva.Analysis.compute ();
;;
let () = Db.Main.extend main
diff --git a/tests/misc/bts1347.ml b/tests/misc/bts1347.ml
index d2319d0f4b81a02e3a66d55474e63ea4e882c3d7..e1336805421fcbd1b834358ed9209b9e67520e53 100644
--- a/tests/misc/bts1347.ml
+++ b/tests/misc/bts1347.ml
@@ -7,7 +7,7 @@ let run () =
(fun kf ->
if not (Cil_builtins.is_builtin (Kernel_function.get_vi kf)) then begin
Globals.set_entry_point (Kernel_function.get_name kf) true;
- !Db.Value.compute();
+ Eva.Analysis.compute();
let hyps =
Alarms.fold
(fun _ kf' s ~rank:_ _ a l ->
diff --git a/tests/misc/ensures.ml b/tests/misc/ensures.ml
index cfe3fc7894196c48711c6dc6031f79ad9ef95d65..a08e28e31b1135d67ab1334b1c307a85b23a855f 100644
--- a/tests/misc/ensures.ml
+++ b/tests/misc/ensures.ml
@@ -2,7 +2,7 @@ open Cil_types
let run () =
Dynamic.Parameter.Bool.set "-eva-context-valid-pointers" true;
- !Db.Value.compute ();
+ Eva.Analysis.compute ();
Globals.Functions.iter
(fun kf ->
let kf_name = Kernel_function.get_name kf in
diff --git a/tests/misc/issue109.ml b/tests/misc/issue109.ml
index 98cc840b15e7d55bbe01e7c1b6083c3bc28c9fbe..fee1af6952d980a7c9c5c14334a6218a2662198b 100644
--- a/tests/misc/issue109.ml
+++ b/tests/misc/issue109.ml
@@ -6,10 +6,10 @@ let ptest_file =
with Not_found -> fun dir file -> dir ^ file
let main () =
- !Db.Value.compute ();
+ Eva.Analysis.compute ();
Dynamic.Parameter.String.set "" "";
Dynamic.Parameter.String.set "" (ptest_file "tests/misc/" "issue109.i");
File.init_from_cmdline ();
- !Db.Value.compute ()
+ Eva.Analysis.compute ()
let main = Db.Main.extend main
diff --git a/tests/misc/log_twice.ml b/tests/misc/log_twice.ml
index df47c2fe750b3d855d4ec067b48b2cf73f36d42c..15145a121857b9156787d96f5cf526a94f4e308d 100644
--- a/tests/misc/log_twice.ml
+++ b/tests/misc/log_twice.ml
@@ -8,9 +8,9 @@ let run () =
~last:false
"default"
in
- !Db.Value.compute ();
+ Eva.Analysis.compute ();
Project.set_current p_default;
- !Db.Value.compute ();
+ Eva.Analysis.compute ();
()
let () = Db.Main.extend run
diff --git a/tests/misc/well_typed_alarm.ml b/tests/misc/well_typed_alarm.ml
index d0e210e9c00fd3896b37b29a623e123ffa54ead4..6c792a3d3ee8155beb6f9ba3c44e698f5d196a33 100644
--- a/tests/misc/well_typed_alarm.ml
+++ b/tests/misc/well_typed_alarm.ml
@@ -1,5 +1,5 @@
let main () =
- !Db.Value.compute();
+ Eva.Analysis.compute();
Filecheck.check_ast "Check alarm";
File.pretty_ast ()
diff --git a/tests/saveload/load_one.ml b/tests/saveload/load_one.ml
index cef2bc0f80bd94c3a90a943c49997a932664cade..9440328dc2d9b58d99c4f9d5b5f338714f08d6fa 100644
--- a/tests/saveload/load_one.ml
+++ b/tests/saveload/load_one.ml
@@ -18,13 +18,13 @@ let main () =
Project.save fp;
Project.remove ~project:p ();
let p = Project.load fp in
- Project.on p (fun () -> !Db.Value.compute (); ignore (sparecode ())) ()
+ Project.on p (fun () -> Eva.Analysis.compute (); ignore (sparecode ())) ()
let () = Db.Main.extend main
(* testing Project.create_by_copy *)
let main2 () =
- !Db.Value.compute ();
+ Eva.Analysis.compute ();
let prj = Project.create_by_copy ~last:false "copy" in
Format.printf "INIT AST@.";
File.pretty_ast ();
diff --git a/tests/slicing/combine.ml b/tests/slicing/combine.ml
index 853545c0c4836b84bb3fddd7c429377db2d93c8b..bbe23a110edfb1fe818977e138123364b920b55c 100644
--- a/tests/slicing/combine.ml
+++ b/tests/slicing/combine.ml
@@ -63,7 +63,7 @@ let main _ =
Cil.visitCilFile infos new_cil_file (* the cil file after slicing *);;
*)
Dynamic.Parameter.Bool.set "-eva-show-progress" true;
- !Db.Value.compute ();
+ Eva.Analysis.compute ();
let all = Cil_datatype.Fundec.Set.empty in
let proj3 = Constant_Propagation.Api.get all ~cast_intro:true in
Project.set_current proj3;
diff --git a/tests/slicing/libSelect.ml b/tests/slicing/libSelect.ml
index 41e55de6abc57f04b210f23b7547f49fa38d0821..309d09278480d329cc4ae0307e2169914d9d6231 100644
--- a/tests/slicing/libSelect.ml
+++ b/tests/slicing/libSelect.ml
@@ -64,7 +64,7 @@ let load_source_file ?entry_point filename =
in
ignore (Db.get_cil_file ());
let kf = Db.find_function_def_by_name entry_point in
- ignore (!Db.Value.compute_entry_point kf ~library);
+ ignore (Eva.Analysis.compute_entry_point kf ~library);
Db.iter_on_functions
(fun kf -> if Db.is_definition kf && Db.Value.is_called kf
then !Db.From.compute kf)
diff --git a/tests/syntax/Refresh_visitor.ml b/tests/syntax/Refresh_visitor.ml
index 9a82d0fd6b4635681d12e70869a6769a7fa6283e..d4075698d6899674174c5738c32b5e3eb3a02685 100644
--- a/tests/syntax/Refresh_visitor.ml
+++ b/tests/syntax/Refresh_visitor.ml
@@ -72,7 +72,7 @@ let main () =
);
Project.on p (fun () ->
Dynamic.Parameter.Bool.set "-eva-show-progress" true;
- !Db.Value.compute ()
+ Eva.Analysis.compute ()
) ();
File.pretty_ast ~prj:p ()
diff --git a/tests/value/oracle_equality/struct2.res.oracle b/tests/value/oracle_equality/struct2.res.oracle
index 848a02fcf02af843f93025e3241dc58bfe59ef05..31007513f85ece3f32c1295e5fbaad5985d2f497 100644
--- a/tests/value/oracle_equality/struct2.res.oracle
+++ b/tests/value/oracle_equality/struct2.res.oracle
@@ -11,20 +11,25 @@
< [scope:rm_asserts] removing 2 assertion(s)
---
> [scope:rm_asserts] removing 1 assertion(s)
-135,137c133,135
+135,137c133,134
< tab3[0..1] ∈ [--..--]
< tab4[0] ∈ {0; 2}
< [1] ∈ {0}
---
> tab3[0] ∈ {0; 1}
> [1] ∈ [--..--]
-> tab4[0..1] ∈ {0}
-140c138,139
+140c137,138
< tab6[0..1] ∈ {0; 2}
---
> tab6[0] ∈ {0}
> [1] ∈ {2}
-211c210
+206,207c204,205
+< s4.e[0].a; s8.b; s7; tab1[0..1]; tab2[0..1]; tab3[0..1]; tab4[0]; tab5[0];
+< tab6[0..1]; p; p2; p3; p4; p5; p6; p7; q; r; s; t; a; b
+---
+> s4.e[0].a; s8.b; s7; tab1[0..1]; tab2[0..1]; tab3[0..1]; tab5[0]; tab6[1];
+> p; p2; p3; p4; p5; p6; p7; q; r; s; t; a; b
+211c209
< [9].a}; s1; s2; s5.e[0].b; s6.b; s8; tabl[0..1]; tab1[0..1];
---
> [9].a}; s1; s2; s5.e[0].b; s6.b; s8; tabl[0..1]; tab1[0];
diff --git a/tests/value/oracle_symblocs/struct2.res.oracle b/tests/value/oracle_symblocs/struct2.res.oracle
index d5341cd37fc34837196ca8c293e4f153c13ae2a0..31bd4583d89f311ca047261d631ffb3fdaed779c 100644
--- a/tests/value/oracle_symblocs/struct2.res.oracle
+++ b/tests/value/oracle_symblocs/struct2.res.oracle
@@ -11,17 +11,21 @@
< [eva:alarm] struct2.i:185: Warning:
98d93
< [scope:rm_asserts] removing 2 assertion(s)
-136,137c131
+136,137d130
< tab4[0] ∈ {0; 2}
< [1] ∈ {0}
----
-> tab4[0..1] ∈ {0}
-140c134,135
+140c133,134
< tab6[0..1] ∈ {0; 2}
---
> tab6[0] ∈ {0}
> [1] ∈ {2}
-211c206
+206,207c200,201
+< s4.e[0].a; s8.b; s7; tab1[0..1]; tab2[0..1]; tab3[0..1]; tab4[0]; tab5[0];
+< tab6[0..1]; p; p2; p3; p4; p5; p6; p7; q; r; s; t; a; b
+---
+> s4.e[0].a; s8.b; s7; tab1[0..1]; tab2[0..1]; tab3[0..1]; tab5[0]; tab6[1];
+> p; p2; p3; p4; p5; p6; p7; q; r; s; t; a; b
+211c205
< [9].a}; s1; s2; s5.e[0].b; s6.b; s8; tabl[0..1]; tab1[0..1];
---
> [9].a}; s1; s2; s5.e[0].b; s6.b; s8; tabl[0..1]; tab1[0];