Skip to content
Snippets Groups Projects
Commit ce033d87 authored by Valentin Perrelle's avatar Valentin Perrelle
Browse files

Merge branch 'feature/eva/remove-db-final-step' into 'master' 

[Eva] Finally removes Db.Value.

See merge request frama-c/frama-c!4280
parents 3073aa76 5d0cc350
No related branches found
No related tags found
No related merge requests found
Hide whitespace changes
Inline Side-by-side
Showing
with 92 additions and 434 deletions
src/kernel_services/abstract_interp/cilE.ml deleted 100644 → 0
+ 0
− 46
View file @ 3073aa76
(**************************************************************************)
(* *)
(* This file is part of Frama-C. *)
(* *)
(* Copyright (C) 2007-2023 *)
(* 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). *)
(* *)
(**************************************************************************)
(* ************************************************************************* *)
(* [JS 2011/03/11] All the below stuff manage warnings of the value analysis
plug-in. Refactoring required. *)
(* ************************************************************************* *)
type alarm_behavior = unit -> unit
let a_ignore = Extlib.nop
type warn_mode = {defined_logic: alarm_behavior;
unspecified: alarm_behavior;
others: alarm_behavior;}
let warn_none_mode =
{ defined_logic = a_ignore; unspecified = a_ignore; others = a_ignore; }
(*
Local Variables:
compile-command: "make -C ../../.."
End:
*)
src/kernel_services/abstract_interp/cilE.mli deleted 100644 → 0
+ 0
− 54
View file @ 3073aa76
(**************************************************************************)
(* *)
(* This file is part of Frama-C. *)
(* *)
(* Copyright (C) 2007-2023 *)
(* 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). *)
(* *)
(**************************************************************************)
(** Value analysis alarms *)
(* ************************************************************************* *)
(* [JS 2011/03/11] All the below stuff manage warnings of the value analysis
plug-in. Refactoring required. *)
(* ************************************************************************* *)
type alarm_behavior = unit -> unit
val a_ignore: alarm_behavior
type warn_mode =
{ defined_logic: alarm_behavior
(** operations that raise an error only in the C, not in the logic *);
unspecified: alarm_behavior (** defined but unspecified behaviors *);
others: alarm_behavior (** all the remaining undefined behaviors *);
}
(** An argument of type [warn_mode] can be supplied to some of the access
functions in {!Db.Value} (the interface to the value analysis).
Each field of {!warn_mode} indicates the action to perform
for each category of alarm. These fields are not completely fixed
yet. However, you can use the value {!warn_none_mode} below
when you have to provide an argument of type [warn_mode]. *)
val warn_none_mode : warn_mode
(** Do not emit any message. *)
(*
Local Variables:
compile-command: "make -C ../../.."
End:
*)
src/kernel_services/plugin_entry_points/db.ml
+ 0
− 108
View file @ ce033d87
......@@ -157,114 +157,6 @@ module Derefs = struct
let pretty = Locations.Zone.pretty
end
(* ************************************************************************* *)
(** {2 Values} *)
(* ************************************************************************* *)
module Value = struct
type state = Cvalue.Model.t
type t = Cvalue.V.t
(* This function is responsible for clearing completely Value's state
when the user-supplied initial state or main arguments are changed.
It is set deep inside Value for technical reasons *)
let initial_state_changed = mk_fun "Value.initial_state_changed"
(* Arguments of the root function of the value analysis *)
module ListArgs = Datatype.List(Cvalue.V)
module FunArgs =
State_builder.Option_ref
(ListArgs)
(struct
let name = "Db.Value.fun_args"
let dependencies =
[ Ast.self; Kernel.LibEntry.self; Kernel.MainFunction.self]
end)
let () = Ast.add_monotonic_state FunArgs.self
exception Incorrect_number_of_arguments
let fun_get_args () = FunArgs.get_option ()
let fun_set_args l =
if not (Option.equal ListArgs.equal (Some l) (FunArgs.get_option ())) then
(!initial_state_changed (); FunArgs.set l)
let fun_use_default_args () =
if FunArgs.get_option () <> None then
(!initial_state_changed (); FunArgs.clear ())
(* Initial memory state of the value analysis *)
module VGlobals =
State_builder.Option_ref
(Cvalue.Model)
(struct
let name = "Db.Value.Vglobals"
let dependencies = [Ast.self]
end)
let globals_set_initial_state state =
if not (Option.equal Cvalue.Model.equal
(Some state)
(VGlobals.get_option ()))
then begin
!initial_state_changed ();
VGlobals.set state
end
let globals_use_default_initial_state () =
if VGlobals.get_option () <> None then
(!initial_state_changed (); VGlobals.clear ())
let initial_state_only_globals = mk_fun "Value.initial_state_only_globals"
let globals_state () =
match VGlobals.get_option () with
| Some v -> v
| None -> !initial_state_only_globals ()
let globals_use_supplied_state () = not (VGlobals.get_option () = None)
let dependencies = [ FunArgs.self; VGlobals.self ]
let proxy = State_builder.Proxy.(create "eva_db" Forward dependencies)
let self = State_builder.Proxy.get proxy
let only_self = [ self ]
module Conditions_table =
Cil_state_builder.Stmt_hashtbl
(Datatype.Int)
(struct
let name = "Db.Value.Conditions_table"
let size = 101
let dependencies = only_self
end)
let merge_conditions h =
Cil_datatype.Stmt.Hashtbl.iter
(fun stmt v ->
try
let old = Conditions_table.find stmt in
Conditions_table.replace stmt (old lor v)
with Not_found ->
Conditions_table.add stmt v)
h
let mask_then = 1
let mask_else = 2
let condition_truth_value s =
try
let i = Conditions_table.find s in
((i land mask_then) <> 0, (i land mask_else) <> 0)
with Not_found -> false, false
let compute = mk_fun "Value.compute"
end
(* ************************************************************************* *)
(** {2 Others plugins} *)
(* ************************************************************************* *)
......
src/kernel_services/plugin_entry_points/db.mli
+ 0
− 94
View file @ ce033d87
......@@ -96,100 +96,6 @@ module Toplevel: sig
end
(* ************************************************************************* *)
(** {2 Values} *)
(* ************************************************************************* *)
(** Deprecated module: use the Eva.mli API instead. *)
module Value : sig
type state = Cvalue.Model.t
(** Internal state of the value analysis. *)
type t = Cvalue.V.t
(** Internal representation of a value. *)
val proxy: State_builder.Proxy.t
val self : State.t
(** Internal state of the value analysis from projects viewpoint.
@see <https://frama-c.com/download/frama-c-plugin-development-guide.pdf> Plug-in Development Guide *)
val compute : (unit -> unit) ref
(** Compute the value analysis 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.
@see <https://frama-c.com/download/frama-c-plugin-development-guide.pdf> Plug-in Development Guide *)
val condition_truth_value: stmt -> bool * bool
(** Provided [stmt] is an 'if' construct, [fst (condition_truth_value stmt)]
(resp. snd) is true if and only if the condition of the 'if' has been
evaluated to true (resp. false) at least once during the analysis. *)
(** {4 Arguments of the main function} *)
(** The functions below are related to the arguments that are passed to the
function that is analysed by the value analysis. Specific arguments
are set by [fun_set_args]. Arguments reset to default values when
[fun_use_default_args] is called, when the ast is changed, or
if the options [-libentry] or [-main] are changed. *)
(** Specify the arguments to use. *)
val fun_set_args : t list -> unit
val fun_use_default_args : unit -> unit
(** For this function, the result [None] means that
default values are used for the arguments. *)
val fun_get_args : unit -> t list option
exception Incorrect_number_of_arguments
(** Raised by [Db.Compute] when the arguments set by [fun_set_args]
are not coherent with the prototype of the function (if there are
too few or too many of them) *)
(** {4 Initial state of the analysis} *)
(** The functions below are related to the value of the global variables
when the value analysis is started. If [globals_set_initial_state] has not
been called, the given state is used. A default state (which depends on
the option [-libentry]) is used when [globals_use_default_initial_state]
is called, or when the ast changes. *)
(** Specify the initial state to use. *)
val globals_set_initial_state : state -> unit
val globals_use_default_initial_state : unit -> unit
(** Initial state used by the analysis *)
val globals_state : unit -> state
(** @return [true] if the initial state for globals used by the value
analysis has been supplied by the user (through
[globals_set_initial_state]), or [false] if it is automatically
computed by the value analysis *)
val globals_use_supplied_state : unit -> bool
(**/**)
(** {3 Internal use only} *)
val merge_conditions: int Cil_datatype.Stmt.Hashtbl.t -> unit
val mask_then: int
val mask_else: int
val initial_state_only_globals : (unit -> state) ref
val initial_state_changed: (unit -> unit) ref
end
[@@alert db_deprecated
"Db.Value is deprecated and will be removed in a future version \
of Frama-C. Please use the Eva.mli public API instead."]
(* ************************************************************************* *)
(** {2 Plugins} *)
(* ************************************************************************* *)
......
src/plugins/eva/Eva.mli
+ 20
− 4
View file @ ce033d87
......@@ -42,9 +42,6 @@ module Analysis: sig
(** 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.
@see <https://frama-c.com/download/frama-c-plugin-development-guide.pdf> Plug-in Development Guide *)
val is_computed : unit -> bool
......@@ -116,7 +113,6 @@ module Analysis: sig
end
module Callstack: sig
[@@@ alert "-db_deprecated"]
(** A call is identified by the function called and the call statement *)
type call = Cil_types.kernel_function * Cil_types.stmt
......@@ -803,6 +799,26 @@ module Eva_results: sig
(** Internal temporary API: please do not use it, as it should be removed in a
future version. *)
(** {2 Initial cvalue state} *)
(** Specifies the initial cvalue state to use. *)
val set_initial_state: Cvalue.Model.t -> unit
(** Ignores previous calls to [set_initial_state] above, and uses the default
initial state instead. *)
val use_default_initial_state: unit -> unit
(** Specifies the values of the main function arguments. Beware that the
analysis fails if the number of given values is different from the number
of arguments of the entry point of the analysis. *)
val set_main_args: Cvalue.V.t list -> unit
(** Ignores previous calls to [set_main_args] above, and uses the default
main argument values instead. *)
val use_default_main_args: unit -> unit
(** {2 Results} *)
type results
val get_results: unit -> results
......
src/plugins/eva/alarmset.ml
+ 0
− 28
View file @ ce033d87
......@@ -205,8 +205,6 @@ let for_all test ~default = function
Alarms
------------------------------------------------------------------------ *)
open CilE
let emitter = Eva_utils.emitter
(* Printer that shows additional information about temporaries *)
......@@ -432,32 +430,6 @@ let emit kinstr = function
"All alarms may arise: \
abstract state too imprecise to continue the analysis."
let warn_alarm warn_mode = function
| Alarms.Uninitialized _
| Alarms.Dangling _
-> warn_mode.unspecified ()
| Alarms.Pointer_comparison _
| Alarms.Differing_blocks _
-> warn_mode.defined_logic ()
| Alarms.Division_by_zero _
| Alarms.Overflow _
| Alarms.Float_to_int _
| Alarms.Invalid_shift _
| Alarms.Memory_access _
| Alarms.Index_out_of_bound _
| Alarms.Invalid_pointer _
| Alarms.Is_nan_or_infinite _
| Alarms.Is_nan _
| Alarms.Not_separated _
| Alarms.Overlap _
| Alarms.Function_pointer _
| Alarms.Invalid_bool _
-> warn_mode.others ()
let notify warn_mode alarms =
iter (fun alarm _status -> warn_alarm warn_mode alarm) alarms
(*
Local Variables:
compile-command: "make -C ../../.."
......
src/plugins/eva/alarmset.mli
+ 0
− 4
View file @ ce033d87
......@@ -104,10 +104,6 @@ val fold : (alarm -> status -> 'a -> 'a) -> 'a -> t -> 'a
instruction. *)
val emit: Cil_types.kinstr -> t -> unit
(** Calls the functions registered in the [warn_mode] according to the
set of alarms. *)
val notify: CilE.warn_mode -> t -> unit
val pretty : Format.formatter -> t -> unit
val pretty_status : Format.formatter -> status -> unit
......
src/plugins/eva/dune
+ 2
− 2
View file @ ce033d87
......@@ -40,7 +40,7 @@
(name eva)
(optional)
(public_name frama-c-eva.core)
(flags -open Frama_c_kernel :standard -w -9 -alert -db_deprecated)
(flags -open Frama_c_kernel :standard -w -9)
(libraries frama-c.kernel frama-c-server.core)
(instrumentation (backend landmarks))
(instrumentation (backend bisect_ppx))
......@@ -60,7 +60,7 @@
(name eva_gui)
(optional)
(public_name frama-c-eva.gui)
(flags -open Frama_c_kernel -open Frama_c_gui -open Eva__Private :standard -w -9 -alert -db_deprecated)
(flags -open Frama_c_kernel -open Frama_c_gui -open Eva__Private :standard -w -9)
(libraries eva frama-c.kernel frama-c.gui)
(instrumentation (backend landmarks))))
......
src/plugins/eva/engine/analysis.ml
+ 0
− 10
View file @ ce033d87
......@@ -88,7 +88,6 @@ module type Analyzer = sig
include S
val compute_from_entry_point : kernel_function -> lib_entry:bool -> unit
(* val compute_from_init_state: kernel_function -> Dom.t -> unit *)
val initial_state: lib_entry:bool -> Dom.t or_bottom
end
......@@ -181,14 +180,6 @@ let set_current_analyzer config (analyzer: (module Analyzer)) =
Analyzer_Hook.apply (module (val analyzer): S);
ref_analyzer := (config, analyzer)
let cvalue_initial_state () =
let module A = (val snd !ref_analyzer) in
let module G = (Cvalue_domain.Getters (A.Dom)) in
let _, lib_entry = Globals.entry_point () in
G.get_cvalue_or_bottom (A.initial_state ~lib_entry)
let () = Db.Value.initial_state_only_globals := cvalue_initial_state
(* Builds the Analyzer module corresponding to a given configuration,
and sets it as the current analyzer. *)
let make_analyzer config =
......@@ -238,7 +229,6 @@ let compute =
let name = "Eva.Analysis.compute" in
fst (State_builder.apply_once name [ Self.state ] compute)
let () = Db.Value.compute := compute
let () = Parameters.ForceValues.set_output_dependencies [Self.state]
let main () =
......
src/plugins/eva/engine/analysis.mli
+ 0
− 3
View file @ ce033d87
......@@ -82,9 +82,6 @@ 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.
@see <https://frama-c.com/download/frama-c-plugin-development-guide.pdf> Plug-in Development Guide *)
val is_computed : unit -> bool
......
src/plugins/eva/engine/compute_functions.ml
+ 0
− 2
View file @ ce033d87
......@@ -167,8 +167,6 @@ module Make (Abstract: Abstractions.S_with_evaluation) = struct
include Cvalue_domain.Getters (Abstract.Dom)
let initial_state = Init.initial_state
let get_cval =
match Abstract.Val.get Main_values.CVal.key with
| None -> fun _ -> assert false
......
src/plugins/eva/engine/compute_functions.mli
+ 0
− 3
View file @ ce033d87
......@@ -23,7 +23,6 @@
(** Value analysis of entire functions, using Eva engine. *)
open Cil_types
open Eval
module Make (Abstract: Abstractions.S_with_evaluation)
: sig
......@@ -33,6 +32,4 @@ module Make (Abstract: Abstractions.S_with_evaluation)
(** Compute a call to the main function from the given initial state. *)
val compute_from_init_state: kernel_function -> Abstract.Dom.t -> unit
val initial_state: lib_entry:bool -> Abstract.Dom.t or_bottom
end
src/plugins/eva/engine/initialization.ml
+ 11
− 17
View file @ ce033d87
......@@ -27,7 +27,6 @@ open Eval
module type S = sig
type state
val initial_state : lib_entry:bool -> state or_bottom
val initial_state_with_formals :
lib_entry:bool -> kernel_function -> state or_bottom
val initialize_local_variable:
......@@ -274,12 +273,15 @@ module Make
bind them in [state] *)
let add_supplied_main_formals kf actuals state =
match get_cvalue with
| None -> Self.abort "Function Db.Value.fun_set_args cannot be \
| None -> Self.abort "API function [set_main_args] cannot be \
used without the Cvalue domain"
| Some get_cvalue ->
let formals = Kernel_function.get_formals kf in
if (List.length formals) <> List.length actuals then
raise Db.Value.Incorrect_number_of_arguments;
Self.abort
"Incorrect number of arguments for the main function %a \
provided via the API function [set_main_args]"
Kernel_function.pretty kf;
let cvalue_state = get_cvalue state in
let add_actual state actual formal =
let actual = Eval_op.offsetmap_of_v ~typ:formal.vtype actual in
......@@ -292,7 +294,7 @@ module Make
set_domain (cvalue_state, Locals_scoping.bottom ()) state
let add_main_formals kf state =
match Db.Value.fun_get_args () with
match Eva_results.get_main_args () with
| None -> compute_main_formals kf state
| Some actuals -> add_supplied_main_formals kf actuals state
......@@ -357,19 +359,13 @@ module Make
InitialState.memo (compute_global_state ~lib_entry)
(* The global cvalue state may be supplied by the user. *)
let supplied_state () =
let cvalue_state = Db.Value.globals_state () in
let supplied_state cvalue_state =
if Cvalue.Model.is_reachable cvalue_state
then
let cvalue_state = cvalue_state, Locals_scoping.bottom () in
`Value (Domain.set Cvalue_domain.State.key cvalue_state Domain.top)
else `Bottom
let initial_state ~lib_entry =
if Db.Value.globals_use_supplied_state ()
then supplied_state ()
else global_state ~lib_entry
let print_initial_cvalue_state state =
let cvalue_state = get_cvalue_or_bottom state in
(* Do not show variables from the frama-c libc specifications. *)
......@@ -391,18 +387,16 @@ module Make
let initial_state_with_formals ~lib_entry kf =
let init_state =
if Db.Value.globals_use_supplied_state ()
then begin
match Eva_results.get_initial_state () with
| Some state ->
Self.feedback "Initial state supplied by user";
supplied_state ()
end
else begin
supplied_state state
| None ->
let pp = Parameters.ValShowProgress.get () in
if pp then Self.feedback "Computing initial state";
let state = global_state ~lib_entry in
if pp then Self.feedback "Initial state computed";
state
end
in
let b = Parameters.ResultsAll.get () in
Domain.Store.register_global_state b init_state;
......
src/plugins/eva/engine/initialization.mli
+ 0
− 5
View file @ ce033d87
......@@ -28,11 +28,6 @@ open Lattice_bounds
module type S = sig
type state
(** Compute the initial state for an analysis. The initial state is generated
according to the options of Value governing the shape of this state.
All global variables are bound in the resulting abstract state. *)
val initial_state : lib_entry:bool -> state or_bottom
(** Compute the initial state for an analysis (as in {!initial_state}),
but also bind the formal parameters of the function given as argument. *)
val initial_state_with_formals :
......
src/plugins/eva/engine/iterator.ml
+ 35
− 36
View file @ ce033d87
......@@ -43,6 +43,33 @@ let blocks_share_locals b1 b2 =
| v1 :: _, v2 :: _ -> v1.vid = v2.vid
| _, _ -> false
module Conditions_table =
Cil_state_builder.Stmt_hashtbl
(Datatype.Pair (Datatype.Bool) (Datatype.Bool))
(struct
let name = "Eva.Iterator.Conditions_table"
let size = 101
let dependencies = [ Self.state ]
end)
let condition_truth_value s =
try Conditions_table.find s
with Not_found -> false, false
let record_fireable edge =
match edge.edge_transition with
| Guard (_exp, kind, stmt) ->
let b_then, b_else = condition_truth_value stmt in
let new_status =
match kind with
| Then -> true, b_else
| Else -> b_then, true
in
Conditions_table.replace stmt new_status
| _ -> ()
module Make_Dataflow
(Abstract : Abstractions.S_with_evaluation)
(States : Powerset.S with type state = Abstract.Dom.t)
......@@ -104,10 +131,6 @@ module Make_Dataflow
type tank = Partitioning.tank
type widening = Partitioning.widening
type edge_info = {
mutable fireable : bool (* Does any states survive the transition ? *)
}
(* --- Interpreted automata --- *)
......@@ -171,7 +194,7 @@ module Make_Dataflow
VertexTable.create control_point_count
let w_table : widening VertexTable.t =
VertexTable.create 7
let e_table : (tank * edge_info) EdgeTable.t =
let e_table : tank EdgeTable.t =
EdgeTable.create transition_count
(* Default (Initial) stores on vertex and edges *)
......@@ -179,18 +202,18 @@ module Make_Dataflow
Partitioning.empty_store ~stmt:v.vertex_start_of
let default_vertex_widening (v : vertex) () : widening =
Partitioning.empty_widening ~stmt:v.vertex_start_of
let default_edge_tank () : tank * edge_info =
Partitioning.empty_tank (), { fireable = false }
let default_edge_tank () : tank =
Partitioning.empty_tank ()
(* Get the stores associated to a control point or edge *)
let get_vertex_store (v : vertex) : store =
VertexTable.find_or_add v_table v ~default:(default_vertex_store v)
let get_vertex_widening (v : vertex) : widening =
VertexTable.find_or_add w_table v ~default:(default_vertex_widening v)
let get_edge_data (e : vertex edge) : tank * edge_info =
let get_edge_data (e : vertex edge) : tank =
EdgeTable.find_or_add e_table e ~default:default_edge_tank
let get_succ_tanks (v : vertex) : tank list =
List.map (fun (_,e,_) -> fst (get_edge_data e)) (G.succ_e graph v)
List.map (fun (_,e,_) -> get_edge_data e) (G.succ_e graph v)
module StmtTable = struct
include Cil_datatype.Stmt.Hashtbl
......@@ -422,7 +445,7 @@ module Make_Dataflow
let process_edge (v1,e,v2 : G.edge) : flow =
let {edge_transition=transition; edge_kinstr=kinstr} = e in
let tank,edge_info = get_edge_data e in
let tank = get_edge_data e in
let flow = Partitioning.drain tank in
Db.yield ();
check_signals ();
......@@ -431,7 +454,7 @@ module Make_Dataflow
let flow = Partitioning.transfer (transfer_transition transition) flow in
let flow = process_partitioning_transitions v1 v2 transition flow in
if not (Partitioning.is_empty_flow flow) then
edge_info.fireable <- true;
record_fireable e;
flow
let gather_cvalues states = match get_cvalue with
......@@ -526,7 +549,7 @@ module Make_Dataflow
let reset_component (vertex_list : vertex list) : unit =
let reset_edge (_,e,_) =
let t,_ = get_edge_data e in
let t = get_edge_data e in
Partitioning.reset_tank t
in
let reset_vertex v =
......@@ -611,29 +634,6 @@ module Make_Dataflow
(* --- Results conversion --- *)
let merge_conditions () =
let table = StmtTable.create 5 in
let fill (_,e,_) =
match e.edge_transition with
| Guard (_exp,kind,stmt) ->
let mask = match kind with
| Then -> Db.Value.mask_then
| Else -> Db.Value.mask_else
in
let edge_info = snd (get_edge_data e) in
let old_status =
try StmtTable.find table stmt
with Not_found -> 0
and status =
if edge_info.fireable then mask else 0
in
let new_status = old_status lor status in
StmtTable.replace table stmt new_status;
| _ -> ()
in
G.iter_edges_e fill graph;
Db.Value.merge_conditions table
let is_instr s = match s.skind with Instr _ -> true | _ -> false
let states_after_stmt states_before states_after =
......@@ -693,7 +693,6 @@ module Make_Dataflow
and register_post = Domain.Store.register_state_after_stmt callstack in
StmtTable.iter register_pre (Lazy.force merged_pre_states);
StmtTable.iter register_post (Lazy.force merged_post_states);
merge_conditions ();
end;
let states =
Cvalue_callbacks.{ before_stmts = merged_pre_cvalues;
......
src/plugins/eva/engine/iterator.mli
+ 5
− 0
View file @ ce033d87
......@@ -25,6 +25,11 @@ open Cil_types
(** Mark the analysis as aborted. It will be stopped at the next safe point *)
val signal_abort: unit -> unit
(** Provided [stmt] is an 'if' construct, [fst (condition_truth_value stmt)]
(resp. snd) is true if and only if the condition of the 'if' has been
evaluated to true (resp. false) at least once during the analysis. *)
val condition_truth_value: stmt -> bool * bool
module Computer
(* Abstractions with the evaluator. *)
(Abstract: Abstractions.S_with_evaluation)
......
src/plugins/eva/legacy/TOREMOVE
+ 0
− 5
View file @ ce033d87
**Function_args**: only there to fill Db.Value.add_formals_to_state, itself used
by Inout/Cumulative_analysis. [compute_actual] is now in [Transfer_stmt],
[actualize_formals] is in [Cvalue_transfer]
**Eval_op**: multiple dependencies in Eval_terms and builtins. Must be rewritten
into the corresponding functionality in Cvalue_forward. This requires having
contexts for logic terms, though.
To be moved elsewhere, probably in domains/cvalue or in engine:
eval_annots, eval_terms
src/plugins/eva/legacy/eval_terms.ml
+ 4
− 2
View file @ ce033d87
......@@ -238,8 +238,10 @@ let add_pre = add_logic Logic_const.pre_label
let add_post = add_logic Logic_const.post_label
let add_old = add_logic Logic_const.old_label
(* Init is a bit special, it is constant and always added to the initial state*)
let add_init state =
add_logic Logic_const.init_label (Db.Value.globals_state ()) state
let add_init states =
match Cvalue_results.get_global_state () with
| `Bottom -> states
| `Value state -> add_logic Logic_const.init_label state states
let add_logic_var env lv cvalue =
{ env with logic_vars = LogicVarEnv.add lv cvalue env.logic_vars }
......
src/plugins/eva/parameters.ml
+ 7
− 10
View file @ ce033d87
......@@ -1131,23 +1131,20 @@ let () = StopAtNthAlarm.set_range ~min:0 ~max:max_int
(* -------------------------------------------------------------------------- *)
let () = Parameter_customize.is_invisible ()
module InitialStateChanged =
module CorrectnessChanged =
Int (struct
let option_name = "-eva-new-initial-state"
let default = 0
let arg_name = "n"
let help = ""
end)
(* Changing the user-supplied initial state (or the arguments of main) through
the API of Db.Value does reset the state of Value, but *not* the property
statuses that Value has positioned. Currently, statuses can only depend
on a command-line parameter. We use the dummy one above to force a reset
when needed. *)
let () =
add_correctness_dep InitialStateChanged.parameter;
Db.Value.initial_state_changed :=
(fun () -> InitialStateChanged.set (InitialStateChanged.get () + 1))
let () = add_correctness_dep CorrectnessChanged.parameter
(* Changing the user-supplied initial state (or the arguments of main) through
the API does reset the state of Eva, but *not* the property statuses set by
Eva. Currently, statuses can only depend on command-line parameters.
We use the dummy one above to force a reset when needed. *)
let change_correctness = CorrectnessChanged.incr
(* -------------------------------------------------------------------------- *)
(* --- Eva options --- *)
......
src/plugins/eva/parameters.mli
+ 8
− 1
View file @ ce033d87
......@@ -148,10 +148,17 @@ module Precision: Parameter_sig.Int
-eva-precision. *)
val configure_precision: unit -> unit
(** List of parameters having an impact on the correctness of the analysis. *)
val parameters_correctness: Typed_parameter.t list
(** List of parameters having an impact only on the analysis precision. *)
val parameters_tuning: Typed_parameter.t list
(** This function should be called whenever the correctness of the analysis
is externally changed through the Eva API, to ensure that the property
statuses emitted by Eva are properly reset. *)
val change_correctness: unit -> unit
(** Registers available cvalue builtins for the -eva-builtin option. *)
val register_builtin: string -> unit
......
0% or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment