Skip to content

GitLab

Commit fdda96e4 authored by David Bühler's avatar David Bühler
Browse files

Merge branch 'fix/andre/deprecate-save-load-fun-state' into 'master' 

[Eva] hide experimental and deprecated options

See merge request frama-c/frama-c!2811
parents 099993c3 9b68391b
Expand all Hide whitespace changes
Inline Side-by-side
Makefile
View file @ fdda96e4
......@@ -899,7 +899,6 @@ PLUGIN_CMO:= partitioning/split_strategy domains/domain_mode value_parameters \
domains/cvalue/builtins_watchpoint \
domains/cvalue/builtins_float domains/cvalue/builtins_split \
domains/inout_domain \
utils/state_import \
legacy/eval_terms legacy/eval_annots \
domains/powerset engine/transfer_logic \
domains/cvalue/cvalue_transfer domains/cvalue/cvalue_init \
......
src/plugins/value/engine/compute_functions.ml
View file @ fdda96e4
......@@ -91,12 +91,9 @@ let post_analysis_cleanup ~aborted =
if Value_parameters.JoinResults.get () then
Db.Value.Table_By_Callstack.iter
(fun s _ -> ignore (Db.Value.get_stmt_state s));
if not aborted then begin
if not aborted then
(* Keep memexec results for users that want to resume the analysis *)
Mem_exec.cleanup_results ();
if not (Value_parameters.SaveFunctionState.is_empty ()) then
State_import.save_globals_state ();
end
Mem_exec.cleanup_results ()
let post_analysis () =
(* Garbled mix must be dumped here -- at least before the call to
......
src/plugins/value/register.ml
View file @ fdda96e4
......@@ -138,8 +138,7 @@ let use_spec_instead_of_definition kf =
not (Kernel_function.is_definition kf) ||
Ast_info.is_frama_c_builtin (Kernel_function.get_name kf) ||
Builtins.is_builtin_overridden kf ||
Kernel_function.Set.mem kf (Value_parameters.UsePrototype.get ()) ||
Value_parameters.LoadFunctionState.mem kf
Kernel_function.Set.mem kf (Value_parameters.UsePrototype.get ())
let eval_predicate ~pre ~here p =
let open Eval_terms in
......
src/plugins/value/utils/state_import.ml deleted 100644 → 0
View file @ 099993c3
(**************************************************************************)
(* *)
(* This file is part of Frama-C. *)
(* *)
(* Copyright (C) 2007-2020 *)
(* 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 Cvalue
open Cil_types
let dkey = Value_parameters.register_category "restart"
let base_cache : (int, Base.t) Hashtbl.t = Hashtbl.create 41
let v_cache = V.Hashtbl.create 53
(* Used to identify and remove escaping values from globals *)
exception Possibly_escaping_value
let import_varinfo (vi : varinfo) ~importing_value =
try
if Cil.isFunctionType vi.vtype then
let kf = Globals.Functions.find_by_name vi.vname in
Kernel_function.get_vi kf
else begin
let vi' = Globals.Vars.find_from_astinfo vi.vname VGlobal in
if vi.vstorage = Static then
Value_parameters.warning ~once:true
"loaded state contains static variables;@ AST ordering@ \
cannot be enforced and must be manually checked for soundness@ \
(e.g. ensure that files are processed in the same order)";
vi'
end
with Not_found ->
(* search in the state *)
if importing_value then begin
(* Variable may be an escaping local value *)
Value_parameters.warning "variable `%a' is not global, \
possibly an escaping value; ignoring"
Printer.pp_varinfo vi;
raise Possibly_escaping_value
end else
Value_parameters.abort "global not found: `%a'"
Printer.pp_varinfo vi
let import_validity = function
| Base.Empty | Base.Known _ | Base.Unknown _ | Base.Invalid as v -> v
| Base.Variable { Base.weak; min_alloc; max_alloc; max_allocable } ->
let var = Base.create_variable_validity ~weak ~min_alloc ~max_alloc in
if Integer.equal max_allocable var.Base.max_allocable then
Base.Variable var
else Kernel.abort "Incompatible maximum size for variable %a vs. %a"
Abstract_interp.Int.pretty max_allocable
Abstract_interp.Int.pretty var.Base.max_allocable
let import_base (base : Base.t) ~importing_value =
let make_base = function
| Base.Var (vi, _validity) ->
Base.of_varinfo (import_varinfo vi ~importing_value)
| Base.CLogic_Var (lv, _ty, _validity) ->
(* Value states do not contain logic variables anyway
(except when evaluating ACSL clauses, which is not the case here *)
Value_parameters.fatal "importing logic variables (%a) is unsupported"
Printer.pp_logic_var lv
| Base.Null -> Base.null
| Base.String (_, s) ->
(* TODO: currently, we recreate a new string unrelated to the original
one. This is probably not the good solution *)
let c = match s with
| Base.CSString s -> Const (CStr s)
| Base.CSWstring s -> Const (CWStr s)
in
let e = Cil.new_exp Cil_datatype.Location.unknown c in
Base.of_string_exp e
| Base.Allocated (vi, deallocation, validity) ->
Value_parameters.feedback ~dkey "recreating allocated base for alloc: `%a'"
Printer.pp_varinfo vi;
let new_vi = Value_util.create_new_var vi.vname vi.vtype in
let validity = import_validity validity in
let new_base = Base.register_allocated_var new_vi deallocation validity in
Builtins_malloc.register_malloced_base new_base;
new_base
in
let id = Base.id base in
try
let res = Hashtbl.find base_cache id in
res
with Not_found ->
let base' = make_base base in
Hashtbl.replace base_cache id base';
base'
let import_base_setlattice (sl : Base.SetLattice.t) ~importing_value =
Base.SetLattice.fold (fun base acc ->
let b' = import_base base ~importing_value in
Base.Hptset.add b' acc
) sl Base.Hptset.empty
let import_ival = Ival.rehash
let import_map (m : Cvalue.V.M.t) =
let add base ival m =
let new_base = import_base base ~importing_value:true in
let new_ival = import_ival ival in
Cvalue.V.add new_base new_ival m
in
Cvalue.V.M.fold add m Cvalue.V.bottom
let import_v (v : Cvalue.V.t) =
match v with
| Cvalue.V.Top (sl, o) ->
Value_parameters.warning ~once:true
"importing garbled mix, locations may have changed";
(*let o' = import_origin o in*)
let s = import_base_setlattice sl ~importing_value:true in
Cvalue.V.inject_top_origin o s
| Cvalue.V.Map m ->
import_map m
let import_v_or_uninit (vu : Cvalue.V_Or_Uninitialized.t) =
let find v =
try
let res = V.Hashtbl.find v_cache v in
res
with Not_found ->
let v' = import_v v
in
V.Hashtbl.replace v_cache v v';
v'
in
try
V_Or_Uninitialized.map find vu
with Possibly_escaping_value ->
(* replace variable with ESCAPINGADDR *)
Cvalue.V_Or_Uninitialized.C_init_esc V.bottom
let import_offsetmap (offsetmap : V_Offsetmap.t) =
V_Offsetmap.map_on_values import_v_or_uninit offsetmap
let import_model (state : Model.t) =
match state with
| Model.Bottom -> Model.bottom
| Model.Top -> Model.top
| Model.Map map ->
let add base offsetmap map =
let new_offsetmap = import_offsetmap offsetmap in
let new_base = import_base base ~importing_value:false in
Model.add_base new_base new_offsetmap map
in
Model.fold add map Model.empty_map
(*and import_origin (o : Origin.t) =
(* the "new" origin location is arbitrary, since no guarantees about the
actual location can be given *)
let loc = Origin.LocationSetLattice.currentloc_singleton () in
match o with
| Origin.Misalign_read _ -> Origin.Misalign_read loc
| Origin.Leaf _ -> Origin.Leaf loc
| Origin.Merge _ -> Origin.Merge loc
| Origin.Arith _ -> Origin.Arith loc
| Origin.Well | Origin.Unknown -> o*)
let load_globals_from_file filename : Model.t =
let ic = open_in_bin filename in
let (state : Model.t) = Marshal.from_channel ic in
close_in ic;
Value_parameters.feedback ~dkey "DE-MARSHALLED STATE (before import):@.%a"
Cvalue.Model.pretty state;
import_model state
let save_globals_to_file kf state_with_locals filename =
Value_parameters.feedback "Saving globals state after call to function: %a"
Kernel_function.pretty kf;
let state = Model.filter_base Base.is_global state_with_locals in
Value_parameters.feedback ~dkey "SAVED STATE:@.%a" Model.pretty state;
let oc = open_out_bin filename in
Marshal.to_channel oc state [];
close_out oc
let load_and_merge_function_state state : Model.t =
let (kf, filename) = Value_parameters.get_LoadFunctionState () in
Value_parameters.feedback
"@[<hov 0>Skipping call to %a,@ loading globals state from file:@ %s@]"
Kernel_function.pretty kf filename;
let saved_state = load_globals_from_file filename in
Value_parameters.debug ~dkey "LOADED STATE:@.%a"
Cvalue.Model.pretty saved_state;
(* warn about missing globals in the new AST, and add new globals that were
not present before *)
let saved_map = match saved_state with
| Model.Map m -> m
| _ -> assert false
in
let locals =
Model.filter_base (fun base -> not (Base.is_global base)) state
in
let state_without_locals =
Model.filter_base (fun base -> Base.is_global base) state
in
Value_parameters.debug ~dkey "Merging state with locals: %a@."
Model.pretty locals;
let new_globals =
Model.filter_base
(fun base ->
try
let _ = Model.find_base base saved_state in
false (* previously existing global *)
with
| Not_found ->
Value_parameters.warning "found new global variable `%a'"
Base.pretty base;
true (* new global *)
) state_without_locals
in
let merged_globals_state =
Model.fold (fun new_base offsm acc ->
Model.add_base new_base offsm acc
) saved_map new_globals
in
let map_with_globals = match merged_globals_state with
| Model.Map m -> m
| _ -> Value_parameters.fatal "invalid saved state: %a"
Model.pretty saved_state
in
let merged_globals_and_locals =
Model.fold (fun new_base offsm acc ->
Model.add_base new_base offsm acc
) map_with_globals locals
in
merged_globals_and_locals
let save_globals_state () : unit =
let (kf, filename) = Value_parameters.get_SaveFunctionState () in
let ret_stmt = Kernel_function.find_return kf in
try
let ret_state = Db.Value.get_stmt_state ret_stmt in
match ret_state with
| Model.Top ->
Value_parameters.abort "cannot save state at return statement of %a \
(too imprecise)" Kernel_function.pretty kf
| Model.Bottom ->
Value_parameters.abort "cannot save state at return statement of %a \
(bottom)" Kernel_function.pretty kf
| Model.Map _ -> save_globals_to_file kf ret_state filename
with Not_found ->
if Value_parameters.LoadFunctionState.is_set () then
let (load_kf, _) = Value_parameters.get_LoadFunctionState () in
Value_parameters.abort "could not find saved state for function `%a';@ \
this can happen if it is called from `%a'"
Kernel_function.pretty kf Kernel_function.pretty load_kf;
else
Value_parameters.failure "could not find saved state for function `%a'"
Kernel_function.pretty kf
exception Warn_local_addresses
(* visitor used by frama_c_load_state *)
class locals_visitor = object(_self) inherit Visitor.frama_c_inplace
method! vlval (lhost, _) =
match lhost with
| Var vi ->
if not vi.vglob then raise Warn_local_addresses;
Cil.DoChildren
| Mem _ -> Cil.DoChildren
end
(* Builtin to load a saved analysis state *)
let frama_c_load_state state actuals =
(* Warn if arguments contain pointers to local variables,
in which case the loaded state may be unsound. *)
begin
try
List.iter (fun (exp_arg, arg, _) ->
let vis = new locals_visitor in
if Cil.isPointerType (Cil.typeOf exp_arg) then
ignore (Visitor.visitFramacExpr vis exp_arg);
if Cvalue.V.contains_addresses_of_any_locals arg then
raise Warn_local_addresses
) actuals;
with Warn_local_addresses ->
Value_parameters.warning ~current:true ~once:true
"arguments to loaded function state contain local addresses,@ \
possible unsoundness";
end;
let merged_loaded_state = load_and_merge_function_state state in
{
Value_types.c_values = [None, merged_loaded_state];
c_clobbered = Base.SetLattice.empty;
c_cacheable = Value_types.NoCacheCallers;
c_from = None
}
let () = Builtins.register_builtin "Frama_C_load_state" frama_c_load_state
src/plugins/value/utils/state_import.mli deleted 100644 → 0
View file @ 099993c3
(**************************************************************************)
(* *)
(* This file is part of Frama-C. *)
(* *)
(* Copyright (C) 2007-2020 *)
(* 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). *)
(* *)
(**************************************************************************)
(** Saving/loading of Value states, possibly among different ASTs.
Used by the command-line options defined by
[Value_parameters.SaveFunctionState] and
[Value_parameters.LoadFunctionState].
@since Aluminium-20160501 *)
(** Loads the saved initial global state, and merges it with the given state
(locals plus new globals which were not present in the original AST).
The saved state may come from a different project.
Note that, to ensure soundness of the merge, some constraints must be
respected according to where the merge takes place.
The intended use is to replace costly function calls, in which case
the state of local variables should not be modified by the function. *)
val load_and_merge_function_state: Cvalue.Model.t -> Cvalue.Model.t
(** Saves the final state of globals variables after the return statement of
the function defined via [Value_parameters.SaveFunctionState]. The result
is saved in the file defined by the same option.
The function must have been called exactly once during the value analysis,
otherwise the saved state is unspecified. *)
val save_globals_state: unit -> unit
src/plugins/value/value_parameters.ml
View file @ fdda96e4
......@@ -1041,97 +1041,6 @@ let () = add_precision_dep ArrayPrecisionLevel.parameter
let () = ArrayPrecisionLevel.add_update_hook
(fun _ v -> Offsetmap.set_plevel v)
(* Options SaveFunctionState and LoadFunctionState are related
and mutually dependent for sanity checking.
Also, they depend on BuiltinsOverrides, so they cannot be defined before it. *)
let () = Parameter_customize.set_group initial_context
module SaveFunctionState =
Kernel_function_map
(struct
include Datatype.String
type key = Cil_types.kernel_function
let of_string ~key:_ ~prev:_ file = file
let to_string ~key:_ file = file
end)
(struct
let option_name = "-eva-save-fun-state"
let arg_name = "function:filename"
let help = "Experimental. Save state of function <function> in file <filename>"
let default = Kernel_function.Map.empty
end)
let () = SaveFunctionState.add_aliases ["-val-save-fun-state"]
let () = Parameter_customize.set_group initial_context
module LoadFunctionState =
Kernel_function_map
(struct
include Datatype.String
type key = Cil_types.kernel_function
let of_string ~key:_ ~prev:_ file = file
let to_string ~key:_ file = file
end)
(struct
let option_name = "-eva-load-fun-state"
let arg_name = "function:filename"
let help = "Experimental. Load state of function <function> from file <filename>"
let default = Kernel_function.Map.empty
end)
let () = LoadFunctionState.add_aliases ["-val-load-fun-state"]
let () = add_correctness_dep SaveFunctionState.parameter
let () = add_correctness_dep LoadFunctionState.parameter
(* checks that SaveFunctionState has a unique argument pair, and returns it. *)
let get_SaveFunctionState () =
let is_first = ref true in
let (kf, filename) = SaveFunctionState.fold
(fun (kf, opt_filename) _acc ->
if !is_first then is_first := false
else abort "option `%s' requires a single function:filename pair"
SaveFunctionState.name;
let filename = Extlib.the opt_filename in
kf, filename
) (Kernel_function.dummy (), "")
in
if filename = "" then abort "option `%s' requires a function:filename pair"
SaveFunctionState.name
else kf, filename
(* checks that LoadFunctionState has a unique argument pair, and returns it. *)
let get_LoadFunctionState () =
let is_first = ref true in
let (kf, filename) = LoadFunctionState.fold
(fun (kf, opt_filename) _acc ->
if !is_first then is_first := false
else abort "option `%s' requires a single function:filename pair"
LoadFunctionState.name;
let filename = Extlib.the opt_filename in
kf, filename
) (Kernel_function.dummy (), "")
in
if filename = "" then abort "option `%s' requires a function:filename pair"
LoadFunctionState.name
else kf, filename
(* perform early sanity checks to avoid aborting the analysis only at the end *)
let () = Ast.apply_after_computed (fun _ ->
(* check the function to save returns 'void' *)
if SaveFunctionState.is_set () then begin
let (kf, _) = get_SaveFunctionState () in
if not (Kernel_function.returns_void kf) then
abort "option `%s': function `%a' must return void"
SaveFunctionState.name Kernel_function.pretty kf
end;
if SaveFunctionState.is_set () && LoadFunctionState.is_set () then begin
(* check that if both save and load are set, they do not specify the
same function name (note: cannot compare using function ids) *)
let (save_kf, _) = get_SaveFunctionState () in
let (load_kf, _) = get_LoadFunctionState () in
if Kernel_function.equal save_kf load_kf then
abort "options `%s' and `%s' cannot save/load the same function `%a'"
SaveFunctionState.name LoadFunctionState.name
Kernel_function.pretty save_kf
end;
if LoadFunctionState.is_set () then
let (kf, _) = get_LoadFunctionState () in
BuiltinsOverrides.add (kf, Some "Frama_C_load_state");
)
(* ------------------------------------------------------------------------- *)
(* --- Messages --- *)
(* ------------------------------------------------------------------------- *)
......
src/plugins/value/value_parameters.mli
View file @ fdda96e4
......@@ -91,15 +91,6 @@ module ArrayPrecisionLevel: Parameter_sig.Int
module AllocatedContextValid: Parameter_sig.Bool
module InitializationPaddingGlobals: Parameter_sig.String
module SaveFunctionState:
Parameter_sig.Map with type key = Cil_types.kernel_function
and type value = string
module LoadFunctionState:
Parameter_sig.Map with type key = Cil_types.kernel_function
and type value = string
val get_SaveFunctionState : unit -> Cil_types.kernel_function * string
val get_LoadFunctionState : unit -> Cil_types.kernel_function * string
module Numerors_Real_Size : Parameter_sig.Int
module Numerors_Mode : Parameter_sig.String
......
tests/builtins/Longinit_sequencer.i deleted 100644 → 0
View file @ 099993c3
/* run.config*
EXECNOW: make -s @PTEST_DIR@/@PTEST_NAME@.cmxs
OPT: @EVA_OPTIONS@ -load-module @PTEST_DIR@/@PTEST_NAME@.cmxs -res-file @PTEST_RESULT@
*/
tests/builtins/Longinit_sequencer.ml deleted 100644 → 0
View file @ 099993c3
(* Small script to test long_init*.c files, which require one test to run
before the other. *)
open Kernel
include Plugin.Register
(struct
let name = "long init testing module"
let shortname = "test-long-init"
let help = "utility script for tests"
end)
module Res = String(struct
let option_name = "-res-file"
let help = ""
let arg_name = "file"
let default = "result"
end)
let ok = ref false
let tmpfile () = Res.get () ^ "/Longinit_sequencer.sav"
let () =
at_exit (fun () ->
let tmpfile = tmpfile () in
if Debug.get () >= 1 || not !ok then
result "Keeping temp file %s" tmpfile
else
try Sys.remove tmpfile with Sys_error _ -> ())
let main () =
let tmpfile = tmpfile () in
let fmt = Format.std_formatter in
let display_results state = Format.fprintf fmt "@[%a@]@\n" !Db.Value.display state in
Dynamic.Parameter.String.set "" "tests/builtins/long_init.c";
Dynamic.Parameter.String.set "-eva-save-fun-state" ("init_inner:" ^ tmpfile);
Dynamic.Parameter.String.set "-eva-alloc-builtin" "fresh";
Dynamic.Parameter.Bool.set "-eva-alloc-returns-null" false;
Dynamic.Parameter.String.set "-eva-warn-key" "builtins:override=inactive";
!Db.Value.compute ();
Callgraph.Uses.iter_in_rev_order display_results;
Files.clear ();
Dynamic.Parameter.String.set "" "tests/builtins/long_init2.c";
(* clear and set parameters to the same value to recompute
kernel function IDs *)
Dynamic.Parameter.String.clear "-eva-save-fun-state" ();
Dynamic.Parameter.String.set "-eva-save-fun-state" ("init_outer:" ^ tmpfile);
Dynamic.Parameter.String.set "-eva-load-fun-state" ("init_inner:" ^ tmpfile);
(* set builtins in a different order to force kernel to recompute
kernel function IDs *)
Dynamic.Parameter.String.set "-eva-alloc-builtin" "fresh";
!Db.Value.compute ();
Callgraph.Uses.iter_in_rev_order display_results;
Files.clear ();
Dynamic.Parameter.String.set "" "tests/builtins/long_init3.c";
Dynamic.Parameter.String.clear "-eva-save-fun-state" ();
Dynamic.Parameter.String.clear "-eva-load-fun-state" ();
Dynamic.Parameter.String.set "-eva-load-fun-state" ("init_outer:" ^ tmpfile);
(* set builtins in a different order to force kernel to recompute
kernel function IDs *)
Dynamic.Parameter.String.set "-eva-alloc-builtin" "fresh";
!Db.Value.compute ();
Callgraph.Uses.iter_in_rev_order display_results;
ok:=true (* no error, we can erase the file *)
let () = Db.Main.extend main
tests/builtins/oracle/Longinit_sequencer.res.oracle deleted 100644 → 0
View file @ 099993c3
This diff is collapsed.
Markdown is supported
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