Commit 16011f2c authored by Valentin Perrelle's avatar Valentin Perrelle
Browse files

Merge branch 'feature/eva/api-callbacks' into 'master'

[Eva] Moves cvalue callbacks into the new Eva API

See merge request frama-c/frama-c!3835
parents 09c34e4f 9d306d03
......@@ -856,7 +856,7 @@ endif
PLUGIN_CMO:= partitioning/split_strategy domains/domain_mode self parameters \
utils/eva_audit utils/eva_perf utils/eva_annotations \
utils/eva_dynamic utils/eva_utils utils/red_statuses \
utils/active_behaviors \
utils/cvalue_callbacks utils/active_behaviors \
utils/widen_hints_ext utils/widen \
partitioning/split_return \
partitioning/per_stmt_slevel \
......@@ -937,7 +937,7 @@ PLUGIN_TYPES_TODOC:=$(addsuffix .mli,$(VALUE_TYPES))
API_MLI := $(addprefix $(PLUGIN_DIR)/, \
engine/analysis.mli utils/results.mli \
parameters.mli utils/eva_annotations.mli \
eval.mli domains/cvalue/builtins.mli \
eval.mli domains/cvalue/builtins.mli utils/cvalue_callbacks.mli \
legacy/eval_terms.mli utils/eva_results.mli utils/unit_tests.mli)
$(PLUGIN_DIR)/Eva.mli: $(PLUGIN_DIR)/gen-api.sh Makefile $(API_MLI)
......
......@@ -1507,6 +1507,8 @@ src/plugins/value/utils/active_behaviors.ml: CEA_LGPL_OR_PROPRIETARY
src/plugins/value/utils/active_behaviors.mli: CEA_LGPL_OR_PROPRIETARY
src/plugins/value/utils/backward_formals.ml: CEA_LGPL_OR_PROPRIETARY
src/plugins/value/utils/backward_formals.mli: CEA_LGPL_OR_PROPRIETARY
src/plugins/value/utils/cvalue_callbacks.ml: CEA_LGPL_OR_PROPRIETARY
src/plugins/value/utils/cvalue_callbacks.mli: CEA_LGPL_OR_PROPRIETARY
src/plugins/value/utils/eva_annotations.ml: CEA_LGPL_OR_PROPRIETARY
src/plugins/value/utils/eva_annotations.mli: CEA_LGPL_OR_PROPRIETARY
src/plugins/value/utils/eva_audit.ml: CEA_LGPL_OR_PROPRIETARY
......
......@@ -64,9 +64,9 @@ let record_callwise_dependencies_in_db call_site froms =
Tbl.replace call_site (Function_Froms.join previous froms)
with Not_found -> Tbl.add call_site froms
let call_for_individual_froms (call_type, value_initial_state, call_stack) =
let call_for_individual_froms callstack _kf call_type value_initial_state =
if From_parameters.ForceCallDeps.get () then begin
let current_function, call_site = List.hd call_stack in
let current_function, call_site = List.hd callstack in
let register_from froms =
record_callwise_dependencies_in_db call_site froms;
match !call_froms_stack with
......@@ -151,15 +151,13 @@ let compute_call_from_value_states current_function states =
Callwise_Froms.compute_and_return current_function
let record_for_individual_froms (call_stack, value_res) =
let record_for_individual_froms callstack cur_kf value_res =
if From_parameters.ForceCallDeps.get () then begin
let froms = match value_res with
| Value_types.Normal (states, _after_states)
| Value_types.NormalStore ((states, _after_states), _) ->
let cur_kf, _ = List.hd call_stack in
| Eva.Cvalue_callbacks.Store ({before_stmts}, memexec_counter) ->
let froms =
if Eva.Analysis.save_results cur_kf
then compute_call_from_value_states cur_kf (Lazy.force states)
then compute_call_from_value_states cur_kf (Lazy.force before_stmts)
else Function_Froms.top
in
let pre_state = match !call_froms_stack with
......@@ -168,28 +166,21 @@ let record_for_individual_froms (call_stack, value_res) =
in
if From_parameters.VerifyAssigns.get () then
!Db.Value.verify_assigns_froms cur_kf ~pre:pre_state froms;
(match value_res with
| Value_types.NormalStore (_, memexec_counter) ->
MemExec.replace memexec_counter froms
| _ -> ());
MemExec.replace memexec_counter froms;
froms
| Value_types.Reuse counter ->
| Reuse counter ->
MemExec.find counter
in
end_record call_stack froms
end_record callstack froms
end
(* Register our callbacks inside the value analysis *)
let () = From_parameters.ForceCallDeps.add_update_hook
(fun _bold bnew ->
if bnew then begin
Db.Value.Call_Type_Value_Callbacks.extend_once call_for_individual_froms;
Db.Value.Record_Value_Callbacks_New.extend_once
record_for_individual_froms;
end)
let () =
Eva.Cvalue_callbacks.register_call_hook call_for_individual_froms;
Eva.Cvalue_callbacks.register_call_results_hook record_for_individual_froms
let force_compute_all_calldeps ()=
......
......@@ -587,11 +587,10 @@ module Callwise = struct
let call_inout_stack = ref []
let call_for_callwise_inout (call_type, state, call_stack) =
let (current_function, ki as call_site) = List.hd call_stack in
let call_for_callwise_inout callstack _kf call_type state =
let (current_function, ki as call_site) = List.hd callstack in
let merge_inout inout =
Db.Operational_inputs.Record_Inout_Callbacks.apply
(call_stack, inout);
Db.Operational_inputs.Record_Inout_Callbacks.apply (callstack, inout);
if ki = Kglobal
then merge_call_in_global_tables call_site inout
else
......@@ -698,35 +697,30 @@ module Callwise = struct
in
Computer.end_dataflow ()
let record_for_callwise_inout ((call_stack: Db.Value.callstack), value_res) =
let record_for_callwise_inout callstack kf value_res =
let inout = match value_res with
| Value_types.Normal (states, _after_states)
| Value_types.NormalStore ((states, _after_states), _) ->
let kf, _ = List.hd call_stack in
| Eva.Cvalue_callbacks.Store ({before_stmts}, memexec_counter) ->
let inout =
if Eva.Analysis.save_results kf
then compute_call_from_value_states kf call_stack (Lazy.force states)
then
let cvalue_states = Lazy.force before_stmts in
compute_call_from_value_states kf callstack cvalue_states
else top
in
(match value_res with
| Value_types.NormalStore (_, memexec_counter) ->
MemExec.replace memexec_counter inout
| _ -> ());
MemExec.replace memexec_counter inout;
inout
| Value_types.Reuse counter ->
| Reuse counter ->
MemExec.find counter
in
Db.Operational_inputs.Record_Inout_Callbacks.apply
(call_stack, inout);
end_record call_stack inout
Db.Operational_inputs.Record_Inout_Callbacks.apply (callstack, inout);
end_record callstack inout
(* Register our callbacks inside the value analysis *)
let () =
Db.Value.Record_Value_Callbacks_New.extend_once record_for_callwise_inout;
Db.Value.Call_Type_Value_Callbacks.extend_once call_for_callwise_inout;;
Eva.Cvalue_callbacks.register_call_results_hook record_for_callwise_inout;
Eva.Cvalue_callbacks.register_call_hook call_for_callwise_inout
end
......
......@@ -265,14 +265,12 @@ let apply_builtin (builtin:builtin) call ~pre ~post =
let arguments = compute_arguments call.arguments call.rest in
try
let call_result = builtin pre arguments in
let call_stack = Eva_utils.call_stack () in
let froms =
match call_result with
| Full result -> `Builtin result.c_from
| States _ -> `Builtin None
| Result _ -> `Spec (Annotations.funspec call.kf)
| States _ | Result _ -> `Builtin None
in
Db.Value.Call_Type_Value_Callbacks.apply (froms, pre, call_stack);
Cvalue_callbacks.apply_call_hooks call.callstack call.kf froms pre;
process_result call post call_result
with
| Invalid_nb_of_args n ->
......
......@@ -184,9 +184,8 @@ module Make (Abstract: Abstractions.Eva) = struct
in
call_result
| Some (states, i) ->
let stack = Eva_utils.call_stack () in
let cvalue = Abstract.Dom.get_cvalue_or_top init_state in
Db.Value.Call_Type_Value_Callbacks.apply (`Memexec, cvalue, stack);
Cvalue_callbacks.apply_call_hooks call.callstack call.kf `Memexec cvalue;
(* Evaluate the preconditions of kf, to update the statuses
at this call. *)
let spec = Annotations.funspec call.kf in
......@@ -202,7 +201,8 @@ module Make (Abstract: Abstractions.Eva) = struct
Self.debug ~dkey
"calling Record_Value_New callbacks on saved previous result";
end;
Db.Value.Record_Value_Callbacks_New.apply (stack, Value_types.Reuse i);
let reuse = Cvalue_callbacks.Reuse i in
Cvalue_callbacks.apply_call_results_hooks call.callstack call.kf reuse;
(* call can be cached since it was cached once *)
Transfer.{states; cacheable = Cacheable; builtin=false}
......@@ -234,11 +234,10 @@ module Make (Abstract: Abstractions.Eva) = struct
let compute_using_spec_or_body target kinstr call state =
let global = match kinstr with Kglobal -> true | _ -> false in
let pp = not global && Parameters.ValShowProgress.get () in
let call_stack = Eva_utils.call_stack () in
if pp then
Self.feedback
"@[computing for function %a.@\nCalled from %a.@]"
Value_types.Callstack.pretty_short call_stack
Value_types.Callstack.pretty_short call.callstack
Cil_datatype.Location.pretty (Cil_datatype.Kinstr.loc kinstr);
let cvalue_state = Abstract.Dom.get_cvalue_or_top state in
let compute, kind =
......@@ -248,7 +247,7 @@ module Make (Abstract: Abstractions.Eva) = struct
| `Spec funspec ->
compute_using_spec funspec, `Spec funspec
in
Db.Value.Call_Type_Value_Callbacks.apply (kind, cvalue_state, call_stack);
Cvalue_callbacks.apply_call_hooks call.callstack call.kf kind cvalue_state;
let resulting_states, cacheable = compute kinstr call state in
if pp then
Self.feedback
......@@ -293,8 +292,8 @@ module Make (Abstract: Abstractions.Eva) = struct
let cvalue_state = Abstract.Dom.get_cvalue_or_top state in
match final_state with
| `Bottom ->
let cs = Eva_utils.call_stack () in
Db.Value.Call_Type_Value_Callbacks.apply (`Spec spec, cvalue_state, cs);
let kind = `Spec spec in
Cvalue_callbacks.apply_call_hooks call.callstack call.kf kind cvalue_state;
let cacheable = Eval.Cacheable in
Transfer.{states; cacheable; builtin=true}
| `Value final_state ->
......@@ -352,9 +351,8 @@ module Make (Abstract: Abstractions.Eva) = struct
let compute () =
Eva_utils.push_call_stack kf Kglobal;
store_initial_state kf init_state;
let call =
{ kf; callstack = []; arguments = []; rest = []; return = None; }
in
let callstack = [kf, Kglobal] in
let call = { kf; callstack; arguments = []; rest = []; return = None; } in
let final_result = compute_call Kglobal call None init_state in
let final_states = List.map snd (final_result.Transfer.states) in
let final_state = PowersetDomain.(final_states |> of_list |> join) in
......
......@@ -448,8 +448,8 @@ module Make_Dataflow
(* TODO: apply on all domains. *)
let states = Partitioning.contents f in
let cvalue_states = gather_cvalues states in
Db.Value.Compute_Statement_Callbacks.apply
(stmt, Eva_utils.call_stack (), cvalue_states)
let callstack = Eva_utils.call_stack () in
Cvalue_callbacks.apply_statement_hooks callstack stmt cvalue_states
let update_vertex ?(widening : bool = false) (v : vertex)
(sources : ('branch * flow) list) : bool =
......@@ -723,21 +723,12 @@ module Make_Dataflow
Db.Value.Record_Value_Callbacks.apply
(callstack, merged_pre_cvalues)
end;
if not (Db.Value.Record_Value_Callbacks_New.is_empty ())
then begin
if Parameters.ValShowProgress.get () then
Self.debug ~dkey:dkey_callbacks
"now calling Record_Value_New callbacks";
if Parameters.MemExecAll.get () then
Db.Value.Record_Value_Callbacks_New.apply
(callstack,
Value_types.NormalStore ((merged_pre_cvalues, merged_post_cvalues),
(Mem_exec.new_counter ())))
else
Db.Value.Record_Value_Callbacks_New.apply
(callstack,
Value_types.Normal (merged_pre_cvalues, merged_post_cvalues))
end;
let states =
Cvalue_callbacks.{ before_stmts = merged_pre_cvalues;
after_stmts = merged_post_cvalues }
in
let results = Cvalue_callbacks.Store (states, Mem_exec.new_counter ()) in
Cvalue_callbacks.apply_call_results_hooks callstack kf results;
if not (Db.Value.Record_Value_After_Callbacks.is_empty ())
then begin
if Parameters.ValShowProgress.get () then
......
......@@ -179,7 +179,7 @@ let make_recursion call depth =
let make call =
let is_same_kf (f, _) = Kernel_function.equal f call.kf in
let previous_calls = List.filter is_same_kf call.callstack in
let depth = List.length previous_calls in
let depth = List.length previous_calls - 1 in
if depth > 0
then Some (make_recursion call depth)
else None
......
......@@ -531,9 +531,9 @@ module Make (Abstract: Abstractions.Eva) = struct
(* ------------------------- Make an Eval.call ---------------------------- *)
(* Create an Eval.call *)
let create_call kf args =
let create_call stmt kf args =
let return = Library_functions.get_retres_vi kf in
let callstack = Eva_utils.call_stack () in
let callstack = (kf, Kstmt stmt) :: Eva_utils.call_stack () in
let arguments, rest =
let formals = Kernel_function.get_formals kf in
let rec format_arguments acc args formals = match args, formals with
......@@ -572,12 +572,12 @@ module Make (Abstract: Abstractions.Eva) = struct
let arguments = List.map replace_arg call.arguments in
{ call with arguments; }
let make_call ~subdivnb kf arguments valuation state =
let make_call ~subdivnb stmt kf arguments valuation state =
(* Evaluate the arguments of the call. *)
let determinate = is_determinate kf in
compute_actuals ~subdivnb ~determinate valuation state arguments
>>=: fun (args, valuation) ->
let call = create_call kf args in
let call = create_call stmt kf args in
let recursion = Recursion.make call in
let call = Extlib.opt_fold replace_recursive_call recursion call in
call, recursion, valuation
......@@ -731,9 +731,8 @@ module Make (Abstract: Abstractions.Eva) = struct
let cvalue_state = Domain.get_cvalue_or_top state in
Db.Value.Call_Value_Callbacks.apply (cvalue_state, stack_with_call);
Db.Value.merge_initial_state (Eva_utils.call_stack ()) cvalue_state;
Db.Value.Call_Type_Value_Callbacks.apply
(`Builtin None, cvalue_state, stack_with_call)
let kind = `Builtin None in
Cvalue_callbacks.apply_call_hooks stack_with_call kf kind cvalue_state
(* --------------------- Process the call statement ---------------------- *)
......@@ -756,7 +755,7 @@ module Make (Abstract: Abstractions.Eva) = struct
[(Partition.Key.empty, state)]
else
(* Create the call. *)
let eval, alarms = make_call ~subdivnb kf args valuation state in
let eval, alarms = make_call ~subdivnb stmt kf args valuation state in
Alarmset.emit ki_call alarms;
let states =
let+ call, recursion, valuation = eval in
......
......@@ -238,7 +238,7 @@ type callstack = call_site list
type ('loc, 'value) call = {
kf: kernel_function; (** The called function. *)
callstack: callstack; (** The current callstack
(without this call). *)
(with this call on top). *)
arguments: ('loc, 'value) argument list; (** The arguments of the call. *)
rest: (exp * ('loc, 'value) assigned) list; (** Extra-arguments. *)
return: varinfo option; (** Fake varinfo to store the
......
(**************************************************************************)
(* *)
(* This file is part of Frama-C. *)
(* *)
(* Copyright (C) 2007-2022 *)
(* 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 Cil_types
let dkey = Self.dkey_callbacks
type callstack = (kernel_function * kinstr) list
type state = Cvalue.Model.t
type analysis_kind =
[ `Builtin of Value_types.call_froms
| `Spec of funspec
| `Def
| `Memexec ]
module Call =
Hook.Build
(struct type t = callstack * kernel_function * analysis_kind * state end)
let register_call_hook f =
Call.extend (fun (callstack, kf, kind, state) -> f callstack kf kind state)
let apply_call_hooks callstack kf kind state =
Call.apply (callstack, kf, kind, state);
Db.Value.Call_Type_Value_Callbacks.apply (kind, state, callstack)
type state_by_stmt = (state Cil_datatype.Stmt.Hashtbl.t) Lazy.t
type results = { before_stmts: state_by_stmt; after_stmts: state_by_stmt }
type call_results =
| Store of results * int
| Reuse of int
module Call_Results =
Hook.Build (struct type t = callstack * kernel_function * call_results end)
let register_call_results_hook f =
Call_Results.extend (fun (callstack, kf, results) -> f callstack kf results)
let apply_call_results_hooks callstack kf call_results =
if Parameters.ValShowProgress.get ()
&& not (Call_Results.is_empty ()
&& Db.Value.Record_Value_Callbacks_New.is_empty ())
then Self.debug ~dkey "now calling Call_Results callbacks";
Call_Results.apply (callstack, kf, call_results);
let results =
match call_results with
| Reuse i -> Value_types.Reuse i
| Store ({before_stmts; after_stmts}, i) ->
Value_types.NormalStore ((before_stmts, after_stmts), i)
in
Db.Value.Record_Value_Callbacks_New.apply (callstack, results)
module Statement =
Hook.Build (struct type t = callstack * stmt * state list end)
let register_statement_hook f =
Statement.extend (fun (callstack, stmt, states) -> f callstack stmt states)
let apply_statement_hooks callstack stmt states =
Statement.apply (callstack, stmt, states);
Db.Value.Compute_Statement_Callbacks.apply (stmt, callstack, states)
(**************************************************************************)
(* *)
(* This file is part of Frama-C. *)
(* *)
(* Copyright (C) 2007-2022 *)
(* 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]
(** Register actions to performed during the Eva analysis,
with access to the states of the cvalue domain. *)
type callstack = (Cil_types.kernel_function * Cil_types.kinstr) list
type state = Cvalue.Model.t
type analysis_kind =
[ `Builtin of Value_types.call_froms
| `Spec of Cil_types.funspec
| `Def
| `Memexec ]
(** Registers a function to be applied at the beginning of the analysis of each
function call. Arguments of the callback are the callstack of the call,
the function called, the kind of analysis performed by Eva for this call,
and the cvalue state at the beginning of the call. *)
val register_call_hook:
(callstack -> Cil_types.kernel_function -> analysis_kind -> state -> unit)
-> unit
type state_by_stmt = (state Cil_datatype.Stmt.Hashtbl.t) Lazy.t
type results = { before_stmts: state_by_stmt; after_stmts: state_by_stmt }
(** Results of a function call. *)
type call_results =
| Store of results * int
(** Cvalue states before and after each statement of the given function,
plus a unique integer id for the call. *)
| Reuse of int
(** The results are the same as a previous call with the given integer id,
previously recorded with the [Store] constructor. *)
(** Registers a function to be applied at the end of the analysis of each
function call. Arguments of the callback are the callstack of the call,
the function called and the cvalue states resulting from its analysis. *)
val register_call_results_hook:
(callstack -> Cil_types.kernel_function -> call_results -> unit)
-> unit
[@@@ api_end]
val register_statement_hook:
(callstack -> Cil_types.stmt -> state list -> unit) -> unit
val apply_call_hooks:
callstack -> Cil_types.kernel_function -> analysis_kind -> state -> unit
val apply_call_results_hooks:
callstack -> Cil_types.kernel_function -> call_results -> unit
val apply_statement_hooks:
callstack -> Cil_types.stmt -> state list -> unit
......@@ -228,16 +228,16 @@
[kernel] imprecise.c:114: approximating value to write.
[eva:alarm] imprecise.c:116: Warning: assertion got status unknown.
[eva] Recording results for many_writes
[kernel] imprecise.c:111:
more than 200(300) elements to enumerate. Approximating.
[kernel] imprecise.c:114:
more than 200(300) elements to enumerate. Approximating.
[from] Computing for function many_writes
[kernel] imprecise.c:111:
more than 200(300) dependencies to update. Approximating.
[kernel] imprecise.c:114:
more than 200(300) dependencies to update. Approximating.
[from] Done for function many_writes
[kernel] imprecise.c:111:
more than 200(300) elements to enumerate. Approximating.
[kernel] imprecise.c:114:
more than 200(300) elements to enumerate. Approximating.
[eva] Done for function many_writes
[eva] computing for function overlap <- main.
Called from imprecise.c:151.
......
......@@ -4,11 +4,11 @@
220a223,224
> [kernel] imprecise.c:111:
> more than 200(300) elements to enumerate. Approximating.
229,232d232
< [eva:alarm] imprecise.c:116: Warning: assertion got status unknown.
< [eva] Recording results for many_writes
228a233,234
> [kernel] imprecise.c:114:
> more than 200(300) elements to enumerate. Approximating.
237,240d242
< [kernel] imprecise.c:111:
< more than 200(300) elements to enumerate. Approximating.
234a235,236
> [eva:alarm] imprecise.c:116: Warning: assertion got status unknown.
> [eva] Recording results for many_writes
< [kernel] imprecise.c:114:
< more than 200(300) elements to enumerate. Approximating.
220a221,222
> [kernel] imprecise.c:111:
> more than 200(300) elements to enumerate. Approximating.
229,232d230
< [eva:alarm] imprecise.c:116: Warning: assertion got status unknown.
< [eva] Recording results for many_writes
228a231,232
> [kernel] imprecise.c:114:
> more than 200(300) elements to enumerate. Approximating.
237,240d240
< [kernel] imprecise.c:111:
< more than 200(300) elements to enumerate. Approximating.
234a233,234
> [eva:alarm] imprecise.c:116: Warning: assertion got status unknown.
> [eva] Recording results for many_writes
< [kernel] imprecise.c:114:
< more than 200(300) elements to enumerate. Approximating.
220a221,222
> [kernel] imprecise.c:111:
> more than 200(300) elements to enumerate. Approximating.
229,232d230
< [eva:alarm] imprecise.c:116: Warning: assertion got status unknown.
< [eva] Recording results for many_writes
228a231,232
> [kernel] imprecise.c:114:
> more than 200(300) elements to enumerate. Approximating.
237,240d240
< [kernel] imprecise.c:111:
< more than 200(300) elements to enumerate. Approximating.
234a233,234
> [eva:alarm] imprecise.c:116: Warning: assertion got status unknown.
> [eva] Recording results for many_writes
< [kernel] imprecise.c:114:
< more than 200(300) elements to enumerate. Approximating.
......@@ -6,10 +6,10 @@
x ∈ {0}
[eva] replace_by_show_each.c:23: Frama_C_show_each_2:
[eva] replace_by_show_each.c:25: Frama_C_show_each_1:
[inout] Warning: no assigns clauses for function Frama_C_show_each_1.
Results will be imprecise.
[from] Warning: no assigns clauses for function Frama_C_show_each_1.