diff --git a/src/plugins/value/domains/cvalue/cvalue_domain.ml b/src/plugins/value/domains/cvalue/cvalue_domain.ml
index 3c0579fa6462ea7496f28af5b5ebc819b84f0cec..019f87cc0ee61fa5f2fb0ab04a5b43ce16e56256 100644
--- a/src/plugins/value/domains/cvalue/cvalue_domain.ml
+++ b/src/plugins/value/domains/cvalue/cvalue_domain.ml
@@ -22,15 +22,8 @@
open Eval
-let key = Structure.Key_Domain.create_key "cvalue_domain"
let dkey_card = Value_parameters.register_category "cardinal"
-let extract get = match get key with
- | None -> fun _ -> Cvalue.Model.top
- | Some get -> function
- | `Bottom -> Cvalue.Model.bottom
- | `Value state -> fst (get state)
-
module Model = struct
include Cvalue.Model
@@ -189,7 +182,7 @@ module State = struct
end )
let name = "Cvalue domain"
- let key = key
+ let key = Structure.Key_Domain.create_key "cvalue_domain"
type value = Model.value
type location = Model.location
@@ -549,9 +542,6 @@ end
let () = Db.Value.display := (fun fmt kf -> State.display ~fmt kf)
-let inject cvalue_model = cvalue_model, Locals_scoping.bottom ()
-let project (state, _) = state
-
type prefix = Hptmap.prefix
module Subpart = struct
diff --git a/src/plugins/value/domains/cvalue/cvalue_domain.mli b/src/plugins/value/domains/cvalue/cvalue_domain.mli
index bd1284006ff3f389db475654aee11f3e21604cf4..cf750b4e60f4caad41803517a7d468d98c6b948b 100644
--- a/src/plugins/value/domains/cvalue/cvalue_domain.mli
+++ b/src/plugins/value/domains/cvalue/cvalue_domain.mli
@@ -27,15 +27,6 @@ module State : Abstract_domain.Leaf
and type location = Main_locations.PLoc.location
and type state = Cvalue.Model.t * Locals_scoping.clobbered_set
-val extract :
- (State.t Structure.Key_Domain.key ->
- ('state -> State.t) option) ->
- 'state Eval.or_bottom -> Cvalue.Model.t
-
-val inject : Cvalue.Model.t -> State.t
-val project : State.t -> Cvalue.Model.t
-
-
(** Specific functions for partitioning optimizations. *)
type prefix
diff --git a/src/plugins/value/engine/abstractions.ml b/src/plugins/value/engine/abstractions.ml
index b0aca9a3150d88bd68121a435572fb694852222b..3a52d334d1f27ed177e53edd7c76f29099355316 100644
--- a/src/plugins/value/engine/abstractions.ml
+++ b/src/plugins/value/engine/abstractions.ml
@@ -384,6 +384,18 @@ module Open (Acc: Acc) : S = struct
module Dom = struct
include Acc.Dom
include Structure.Open (Abstract.Domain) (Acc.Dom)
+
+ let get_cvalue = match get Cvalue_domain.State.key with
+ | None -> None
+ | Some get -> Some (fun s -> fst (get s))
+
+ let get_cvalue_or_top = match get Cvalue_domain.State.key with
+ | None -> fun _ -> Cvalue.Model.top
+ | Some get -> fun s -> fst (get s)
+
+ let get_cvalue_or_bottom = function
+ | `Bottom -> Cvalue.Model.bottom
+ | `Value state -> get_cvalue_or_top state
end
end
diff --git a/src/plugins/value/engine/analysis.ml b/src/plugins/value/engine/analysis.ml
index b045bee75c807d965db72fe2bfeef2dd7bda8f65..ee1b5680eeac44e2ad88489209edf6dbbb7fceb6 100644
--- a/src/plugins/value/engine/analysis.ml
+++ b/src/plugins/value/engine/analysis.ml
@@ -133,7 +133,7 @@ let set_current_analyzer config (analyzer: (module Analyzer)) =
let cvalue_initial_state () =
let module A = (val snd !ref_analyzer) in
let _, lib_entry = Globals.entry_point () in
- Cvalue_domain.extract A.Dom.get (A.initial_state ~lib_entry)
+ A.Dom.get_cvalue_or_bottom (A.initial_state ~lib_entry)
(* Builds the Analyzer module corresponding to a given configuration,
and sets it as the current analyzer. *)
diff --git a/src/plugins/value/engine/compute_functions.ml b/src/plugins/value/engine/compute_functions.ml
index 4440415631b5dd90793189134a401c3e655e9dfa..21a9876322a1e7dfe27fdc0a8c9d0dc8803ce778 100644
--- a/src/plugins/value/engine/compute_functions.ml
+++ b/src/plugins/value/engine/compute_functions.ml
@@ -148,11 +148,6 @@ module Make (Abstract: Abstractions.Eva) = struct
let initial_state = Init.initial_state
- let get_cvalue =
- match Abstract.Dom.get Cvalue_domain.State.key with
- | None -> fun _ -> Cvalue.Model.top
- | Some get -> fun state -> Cvalue_domain.project (get state)
-
let get_cval =
match Abstract.Val.get Main_values.CVal.key with
| None -> fun _ -> assert false
@@ -191,7 +186,7 @@ module Make (Abstract: Abstractions.Eva) = struct
then `Spec (Annotations.funspec kf)
else `Def def
in
- let cvalue_state = get_cvalue state in
+ let cvalue_state = Abstract.Dom.get_cvalue_or_top state in
let resulting_states, cacheable = match use_spec with
| `Spec spec ->
Db.Value.Call_Type_Value_Callbacks.apply
@@ -237,9 +232,9 @@ module Make (Abstract: Abstractions.Eva) = struct
in
call_result
| Some (states, i) ->
- let stack_with_call = Value_util.call_stack () in
- Db.Value.Call_Type_Value_Callbacks.apply
- (`Memexec, get_cvalue init_state, stack_with_call);
+ let stack = Value_util.call_stack () in
+ let cvalue = Abstract.Dom.get_cvalue_or_top init_state in
+ Db.Value.Call_Type_Value_Callbacks.apply (`Memexec, cvalue, stack);
(* Evaluate the preconditions of kf, to update the statuses
at this call. *)
let spec = Annotations.funspec call.kf in
@@ -300,7 +295,7 @@ module Make (Abstract: Abstractions.Eva) = struct
in
Locations.Location_Bytes.do_track_garbled_mix true;
let final_state = states >>- join_states in
- let cvalue_state = get_cvalue state in
+ let cvalue_state = Abstract.Dom.get_cvalue_or_top state in
match final_state with
| `Bottom ->
let cs = Value_util.call_stack () in
@@ -329,7 +324,7 @@ module Make (Abstract: Abstractions.Eva) = struct
let store_initial_state kf init_state =
Abstract.Dom.Store.register_initial_state (Value_util.call_stack ()) init_state;
- let cvalue_state = get_cvalue init_state in
+ let cvalue_state = Abstract.Dom.get_cvalue_or_top init_state in
Db.Value.Call_Value_Callbacks.apply (cvalue_state, [kf, Kglobal])
let compute kf init_state =
diff --git a/src/plugins/value/engine/initialization.ml b/src/plugins/value/engine/initialization.ml
index 6f15c07d5d656a644e39895b095726493790376a..fd124a687b6a27f5c823130697fcad9ca2042a7a 100644
--- a/src/plugins/value/engine/initialization.ml
+++ b/src/plugins/value/engine/initialization.ml
@@ -270,15 +270,14 @@ module Make
(* Use the values supplied in [actuals] for the formals of [kf], and
bind them in [state] *)
let add_supplied_main_formals kf actuals state =
- match Domain.get Cvalue_domain.State.key with
- | None ->
- Value_parameters.abort "Function Db.Value.fun_set_args cannot be used \
- without the Cvalue domain"
+ match Domain.get_cvalue with
+ | None -> Value_parameters.abort "Function Db.Value.fun_set_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;
- let cvalue_state = Cvalue_domain.project (get_cvalue state) in
+ 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
Cvalue.Model.add_base (Base.of_varinfo formal) actual state
@@ -287,7 +286,7 @@ module Make
List.fold_left2 add_actual cvalue_state actuals formals
in
let set_domain = Domain.set Cvalue_domain.State.key in
- set_domain (Cvalue_domain.inject cvalue_state) state
+ set_domain (cvalue_state, Locals_scoping.bottom ()) state
let add_main_formals kf state =
match Db.Value.fun_get_args () with
@@ -355,7 +354,7 @@ module Make
let cvalue_state = Db.Value.globals_state () in
if Cvalue.Model.is_reachable cvalue_state
then
- let cvalue_state = Cvalue_domain.inject cvalue_state in
+ let cvalue_state = cvalue_state, Locals_scoping.bottom () in
`Value (Domain.set Cvalue_domain.State.key cvalue_state Domain.top)
else `Bottom
@@ -365,7 +364,7 @@ module Make
else global_state ~lib_entry
let print_initial_cvalue_state state =
- let cvalue_state = Cvalue_domain.extract Domain.get state in
+ let cvalue_state = Domain.get_cvalue_or_bottom state in
(* Do not show variables from the frama-c libc specifications. *)
let print_base base =
try
diff --git a/src/plugins/value/engine/iterator.ml b/src/plugins/value/engine/iterator.ml
index 0e83fb39280cd62436229a5d74a6b8cd5ff5def8..bae4fbcc7b35ec5ec246816cd8ab55f9f6bcfe47 100644
--- a/src/plugins/value/engine/iterator.ml
+++ b/src/plugins/value/engine/iterator.ml
@@ -433,10 +433,8 @@ module Make_Dataflow
edge_info.fireable <- true;
flow
- let get_cvalue = Domain.get Cvalue_domain.State.key
- let gather_cvalues states =
- match get_cvalue with
- | Some get -> List.map (fun s -> Cvalue_domain.project (get s)) states
+ let gather_cvalues states = match Domain.get_cvalue with
+ | Some get -> List.map get states
| None -> []
let call_statement_callbacks (stmt : stmt) (f : flow) : unit =
@@ -633,9 +631,6 @@ module Make_Dataflow
G.iter_edges_e fill graph;
Db.Value.merge_conditions table
- let extract_cvalue (state : state) : 'a =
- Cvalue_domain.extract Domain.get (`Value state)
-
let is_instr s = match s.skind with Instr _ -> true | _ -> false
let states_after_stmt states_before states_after =
@@ -676,7 +671,7 @@ module Make_Dataflow
then VertexTable.memo merged_states v get_smashed_store
else `Bottom
and lift_to_cvalues table =
- StmtTable.map (fun _ s -> extract_cvalue s) (Lazy.force table)
+ StmtTable.map (fun _ s -> Domain.get_cvalue_or_top s) (Lazy.force table)
in
let merged_pre_states = lazy
(StmtTable.map' (fun s (v,_) -> get_merged_states ~all:true s v) automaton.stmt_table)
@@ -691,7 +686,7 @@ module Make_Dataflow
(StmtTable.map (fun _stmt (v,_) ->
let store = get_vertex_store v in
let states = Partition.expanded store in
- List.map (fun x -> extract_cvalue x) states)
+ List.map (fun x -> Domain.get_cvalue_or_top x) states)
automaton.stmt_table)
in
let merged_pre_cvalues = lazy (lift_to_cvalues merged_pre_states)
diff --git a/src/plugins/value/engine/transfer_specification.ml b/src/plugins/value/engine/transfer_specification.ml
index 69171aaeec78721bd2c156951fea6e5d791df366..e15091974e5c8cdc7de19f10e67d858ec9a6babc 100644
--- a/src/plugins/value/engine/transfer_specification.ml
+++ b/src/plugins/value/engine/transfer_specification.ml
@@ -232,11 +232,8 @@ module Make
| Some get -> get
let set_ploc = Location.set Main_locations.PLoc.key
let set_location loc = set_ploc (Main_locations.PLoc.make loc)
- let get_cvalue_state = match Domain.get Cvalue_domain.State.key with
- | None -> fun _ -> Cvalue.Model.top
- | Some get -> fun s -> Cvalue_domain.project (get s)
- let make_env state = Eval_terms.env_assigns (get_cvalue_state state)
+ let make_env state = Eval_terms.env_assigns (Domain.get_cvalue_or_top state)
let is_result = function
| Assigns (term, _)
@@ -299,7 +296,7 @@ module Make
end
in
let check_one_state state =
- let cvalue_state = get_cvalue_state state in
+ let cvalue_state = Domain.get_cvalue_or_top state in
List.iter (check_one_assign cvalue_state) assigns
in
States.iter check_one_state states
diff --git a/src/plugins/value/engine/transfer_stmt.ml b/src/plugins/value/engine/transfer_stmt.ml
index c0f99adcbda13fd6af6563f097ae04be9534acee..514e4ea789c0db62b5c02857c3417d66e9128ee5 100644
--- a/src/plugins/value/engine/transfer_stmt.ml
+++ b/src/plugins/value/engine/transfer_stmt.ml
@@ -559,10 +559,6 @@ module Make (Abstract: Abstractions.Eva) = struct
(* ----------------- show_each and dump_each directives ------------------- *)
- let extract_cvalue = match Domain.get Cvalue_domain.State.key with
- | None -> fun _ -> Cvalue.Model.top
- | Some get -> fun s -> Cvalue_domain.project (get s)
-
(* The product of domains formats the printing of each leaf domains, by
checking their log_category and adding their name before the dump. If the
domain is not a product, this needs to be done here. *)
@@ -609,7 +605,7 @@ module Make (Abstract: Abstractions.Eva) = struct
(* For non scalar expressions, prints the offsetmap of the cvalue domain. *)
let show_offsm =
- match Domain.get Cvalue_domain.State.key, Location.get Main_locations.PLoc.key with
+ match Domain.get_cvalue, Location.get Main_locations.PLoc.key with
| None, _ | _, None ->
fun fmt _ _ -> Format.fprintf fmt "%s" (Unicode.top_string ())
| Some get_cvalue, Some get_ploc ->
@@ -621,9 +617,7 @@ module Make (Abstract: Abstractions.Eva) = struct
let offsm =
fst (Eval.lvaluate ~for_writing:false state lval)
>>- fun (_, loc, _) ->
- let ploc = get_ploc loc
- and cvalue_state = Cvalue_domain.project (get_cvalue state) in
- Eval_op.offsetmap_of_loc ploc cvalue_state
+ Eval_op.offsetmap_of_loc (get_ploc loc) (get_cvalue state)
in
let typ = Cil.typeOf expr in
(Bottom.pretty (Eval_op.pretty_offsetmap typ)) fmt offsm
@@ -707,7 +701,7 @@ module Make (Abstract: Abstractions.Eva) = struct
{Cvalue_transfer.start_call}. *)
let apply_cvalue_callback kf ki_call state =
let stack_with_call = (kf, ki_call) :: Value_util.call_stack () in
- let cvalue_state = extract_cvalue state in
+ 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 (Value_util.call_stack ()) cvalue_state;
let result =
diff --git a/src/plugins/value/gui_files/gui_eval.ml b/src/plugins/value/gui_files/gui_eval.ml
index 2c64ede8741331662b1b3085078c4ba5e77364af..8239f3974fe81a150ebdeaa53a488ec29935eb31 100644
--- a/src/plugins/value/gui_files/gui_eval.ml
+++ b/src/plugins/value/gui_files/gui_eval.ml
@@ -143,11 +143,6 @@ module Make (X: Analysis.S) = struct
module Analysis = X
- let get_cvalue_state =
- match X.Dom.get Cvalue_domain.State.key with
- | None -> fun _ -> Cvalue.Model.top
- | Some get -> fun state -> Cvalue_domain.project (get state)
-
let get_precise_loc =
match X.Loc.get Main_locations.PLoc.key with
| None -> fun _ -> Precise_locs.loc_top
@@ -210,7 +205,7 @@ module Make (X: Analysis.S) = struct
let lval_to_offsetmap state lv =
let loc, alarms = X.eval_lval_to_loc state lv in
let ok = Alarmset.is_empty alarms in
- let state = get_cvalue_state state in
+ let state = X.Dom.get_cvalue_or_top state in
let aux loc (acc_res, acc_ok) =
let res, ok =
match lv with (* catch simplest pattern *)
@@ -273,7 +268,7 @@ module Make (X: Analysis.S) = struct
}
let null_to_offsetmap state (_:unit) =
- let state = get_cvalue_state state in
+ let state = X.Dom.get_cvalue_or_top state in
match Cvalue.Model.find_base_or_default Base.null state with
| `Bottom -> GO_InvalidLoc, false, false
| `Top -> GO_Top, false, false
@@ -335,17 +330,17 @@ module Make (X: Analysis.S) = struct
let env_here kf here callstack =
let pre = pre_kf kf callstack in
- let here = get_cvalue_state here in
+ let here = X.Dom.get_cvalue_or_top here in
let c_labels = Eval_annots.c_labels kf callstack in
Eval_terms.env_annot ~c_labels ~pre ~here ()
let env_pre _kf here _callstack =
- let here = get_cvalue_state here in
+ let here = X.Dom.get_cvalue_or_top here in
Eval_terms.env_pre_f ~pre:here ()
let env_post kf post callstack =
let pre = pre_kf kf callstack in
- let post = get_cvalue_state post in
+ let post = X.Dom.get_cvalue_or_top post in
let result =
if !Db.Value.use_spec_instead_of_definition kf then
None
diff --git a/src/plugins/value/register.ml b/src/plugins/value/register.ml
index 480323cf90b98819280de507bd88acf0b527c9e6..f8617e5ad4eb5c0b021ed543a5102af398231f72 100644
--- a/src/plugins/value/register.ml
+++ b/src/plugins/value/register.ml
@@ -188,6 +188,8 @@ module Eva =
module Transfer = Cvalue_domain.State.Transfer (Eva.Valuation)
+let inject_cvalue state = state, Locals_scoping.bottom ()
+
let bot_value = function
| `Bottom -> Cvalue.V.bottom
| `Value v -> v
@@ -197,7 +199,7 @@ let bot_state = function
| `Value s -> s
let update valuation state =
- bot_state (Transfer.update valuation state >>-: Cvalue_domain.project)
+ bot_state (Transfer.update valuation state >>-: fst)
let rec eval_deps state e =
match e.enode with
@@ -236,7 +238,7 @@ let notify_opt with_alarms alarms =
Extlib.may (fun mode -> Alarmset.notify mode alarms) with_alarms
let eval_expr_with_valuation ?with_alarms deps state expr=
- let state = Cvalue_domain.inject state in
+ let state = inject_cvalue state in
let deps = match deps with
| None -> None
| Some deps ->
@@ -256,7 +258,7 @@ let eval_expr_with_valuation ?with_alarms deps state expr=
module Eval = struct
let eval_expr ?with_alarms state expr =
- let state = Cvalue_domain.inject state in
+ let state = inject_cvalue state in
let eval, alarms = Eva.evaluate ~reduction:false state expr in
notify_opt with_alarms alarms;
bot_value (eval >>-: snd)
@@ -278,7 +280,7 @@ module Eval = struct
let reduce_by_cond state expr positive =
- let state = Cvalue_domain.inject state in
+ let state = inject_cvalue state in
let eval, _alarms =
Eva.reduce state expr positive
in
@@ -289,7 +291,7 @@ module Eval = struct
if not (Cvalue.Model.is_reachable state)
then state, deps, Precise_locs.loc_bottom, (Cil.typeOfLval lval)
else
- let state = Cvalue_domain.inject state in
+ let state = inject_cvalue state in
let deps = match deps with
| None -> None
| Some deps ->
@@ -338,7 +340,7 @@ module Eval = struct
let resolv_func_vinfo ?with_alarms deps state funcexp =
let open Cil_types in
- let state = Cvalue_domain.inject state in
+ let state = inject_cvalue state in
let deps = match funcexp.enode with
| Lval (Var _, NoOffset) -> deps
| Lval (Mem v, _) ->
diff --git a/src/plugins/value/utils/abstract.ml b/src/plugins/value/utils/abstract.ml
index 1ccaa235ba42bb7c456b769b36efdba281386497..e5153a5241bcbd0682795eb13ee79fbe48976499 100644
--- a/src/plugins/value/utils/abstract.ml
+++ b/src/plugins/value/utils/abstract.ml
@@ -86,5 +86,9 @@ module Domain = struct
include Internal
include Structure.External with type t := t
and type 'a key := 'a key
+
+ val get_cvalue: (t -> Cvalue.Model.t) option
+ val get_cvalue_or_top: t -> Cvalue.Model.t
+ val get_cvalue_or_bottom: t Bottom.or_bottom -> Cvalue.Model.t
end
end
diff --git a/src/plugins/value/utils/abstract.mli b/src/plugins/value/utils/abstract.mli
index 258ddf831f82f00bd9af1bf2df6c85b5db0c1c89..3e797f8eddba95cddfa69765f3097ac7a3081ffa 100644
--- a/src/plugins/value/utils/abstract.mli
+++ b/src/plugins/value/utils/abstract.mli
@@ -109,5 +109,10 @@ module Domain : sig
include Internal
include Interface with type t := t
and type 'a key := 'a key
+
+ (** Special accessors for the main cvalue domain. *)
+ val get_cvalue: (t -> Cvalue.Model.t) option
+ val get_cvalue_or_top: t -> Cvalue.Model.t
+ val get_cvalue_or_bottom: t Bottom.or_bottom -> Cvalue.Model.t
end
end