From 96fcdf6be4216c24909ba08c33ca9413176c73bf Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?David=20B=C3=BChler?= <david.buhler@cea.fr>
Date: Fri, 21 May 2021 10:41:35 +0200
Subject: [PATCH] [Eva] Change Domain_builder.Complete signature.
This functor automatically builds some abstract domain functions.
It must now be called at the beginning of the abstract domain module, so that
the built functions can be redefined by the domain if needed.
---
src/plugins/value/domains/abstract_domain.mli | 8 +-
.../value/domains/apron/apron_domain.ml | 13 +-
src/plugins/value/domains/domain_builder.ml | 19 +-
src/plugins/value/domains/domain_builder.mli | 17 +-
.../value/domains/gauges/gauges_domain.ml | 8 +-
src/plugins/value/domains/inout_domain.ml | 10 +-
src/plugins/value/domains/multidim_domain.ml | 34 +-
src/plugins/value/domains/octagons.ml | 8 +-
src/plugins/value/domains/offsm_domain.ml | 10 +-
src/plugins/value/domains/simple_memory.ml | 13 +-
src/plugins/value/domains/symbolic_locs.ml | 9 +-
src/plugins/value/domains/taint_domain.ml | 10 +-
src/plugins/value/domains/traces_domain.ml | 352 +++++++++---------
src/plugins/value/utils/abstract.ml | 4 +-
src/plugins/value/utils/abstract.mli | 4 +-
15 files changed, 271 insertions(+), 248 deletions(-)
diff --git a/src/plugins/value/domains/abstract_domain.mli b/src/plugins/value/domains/abstract_domain.mli
index 232f8e12eec..a71352d34ce 100644
--- a/src/plugins/value/domains/abstract_domain.mli
+++ b/src/plugins/value/domains/abstract_domain.mli
@@ -464,12 +464,6 @@ module type S = sig
(** Category for the messages about the domain.
Must be created through {!Value_parameters.register_category}. *)
val log_category : Value_parameters.category
-end
-
-(** Full implementation of domains. Automatically built by
- {!Domain_builder.Complete} from an {!S_with_Structure} domain. *)
-module type Internal = sig
- include S
(** This function is called after the analysis. The argument is the state
computed at the return statement of the main function. The function can
@@ -485,7 +479,7 @@ type 't key = 't Structure.Key_Domain.key
(** Signature for a leaf module of a domain. *)
module type Leaf = sig
- include Internal
+ include S
(** The key identifies the domain and the type [t] of its states. *)
val key: t key
diff --git a/src/plugins/value/domains/apron/apron_domain.ml b/src/plugins/value/domains/apron/apron_domain.ml
index 1f3b2fdede7..3b8321d98f7 100644
--- a/src/plugins/value/domains/apron/apron_domain.ml
+++ b/src/plugins/value/domains/apron/apron_domain.ml
@@ -370,7 +370,7 @@ module Make (Man : Input) = struct
let top = Abstract1.top man empty_env
let make_top env = Abstract1.top man env
- include Datatype.Make_with_collections (
+ module D = Datatype.Make_with_collections (
struct
include Datatype.Undefined
type t = state
@@ -402,6 +402,7 @@ module Make (Man : Input) = struct
let mem_project = Datatype.never_any_project
end )
+ include D
let name = Man.name
@@ -428,6 +429,14 @@ module Make (Man : Input) = struct
let s = Abstract1.meet man s1 s2 in
if Abstract1.is_bottom man s then `Bottom else `Value s
+ include Domain_builder.Complete
+ (struct
+ include D
+ let name = name
+ let top = top
+ let join = join
+ end)
+
let make_eval state =
let env = Abstract1.env state in
fun e ->
@@ -728,7 +737,7 @@ end
let () = Floating_point.set_round_nearest_even ()
let make name (module Man: Input) =
- let module Domain = Domain_builder.Complete (Make (Man)) in
+ let module Domain = Make (Man) in
let descr =
"Binding to the " ^ name ^ " domain of the Apron library. " ^
"See http://apron.cri.ensmp.fr/library for more details."
diff --git a/src/plugins/value/domains/domain_builder.ml b/src/plugins/value/domains/domain_builder.ml
index ac0278cd3d4..0d48207dbda 100644
--- a/src/plugins/value/domains/domain_builder.ml
+++ b/src/plugins/value/domains/domain_builder.ml
@@ -21,14 +21,20 @@
(**************************************************************************)
module type InputDomain = sig
- include Abstract_domain.S
+ include Datatype.S
+ val top: t
+ val join: t -> t -> t
end
-module Complete
- (Domain: InputDomain)
-= struct
+module type LeafDomain = sig
+ type t
+ val post_analysis: t Bottom.or_bottom -> unit
+ module Store: Domain_store.S with type t := t
+ val key: t Abstract_domain.key
+end
+
+module Complete (Domain: InputDomain) = struct
- include Domain
module Store = Domain_store.Make (Domain)
let key: Domain.t Structure.Key_Domain.key =
@@ -140,6 +146,7 @@ module Complete_Minimal
: Datatype.S_with_collections with type t := t)
end
+ include D
include Complete (D)
end
@@ -161,6 +168,7 @@ module Complete_Minimal_with_datatype
: Datatype.S_with_collections with type t := t)
end
+ include D
include Complete (D)
end
@@ -253,6 +261,7 @@ module Complete_Simple_Cvalue (Domain: Simpler_domains.Simple_Cvalue)
let reuse _kf _bases ~current_input:_ ~previous_output = previous_output
end
+ include D
include Complete (D)
end
diff --git a/src/plugins/value/domains/domain_builder.mli b/src/plugins/value/domains/domain_builder.mli
index e27fcc16829..5d76e370494 100644
--- a/src/plugins/value/domains/domain_builder.mli
+++ b/src/plugins/value/domains/domain_builder.mli
@@ -24,14 +24,19 @@
simplified interfaces. *)
module type InputDomain = sig
- include Abstract_domain.S
+ include Datatype.S
+ val top: t
+ val join: t -> t -> t
end
-module Complete
- (Domain: InputDomain)
- : Abstract_domain.Leaf with type state = Domain.state
- and type value = Domain.value
- and type location = Domain.location
+module type LeafDomain = sig
+ type t
+ val post_analysis: t Bottom.or_bottom -> unit
+ module Store: Domain_store.S with type t := t
+ val key: t Abstract_domain.key
+end
+
+module Complete (Domain: InputDomain) : LeafDomain with type t := Domain.t
module Complete_Minimal
(Value: Abstract_value.S)
diff --git a/src/plugins/value/domains/gauges/gauges_domain.ml b/src/plugins/value/domains/gauges/gauges_domain.ml
index f14c28a4ec5..ced00ea1bab 100644
--- a/src/plugins/value/domains/gauges/gauges_domain.ml
+++ b/src/plugins/value/domains/gauges/gauges_domain.ml
@@ -538,6 +538,8 @@ module G = struct
(Datatype.List(Datatype.Pair(Cil_datatype.Stmt)(IterationInfo)))
(struct let module_name = "Values.Gauges_domain.G" end)
+ let name = "gauges"
+
let empty = MV.empty, []
let top (state: t) : t =
let top_iteration_info = function
@@ -1117,7 +1119,7 @@ end
let dkey = Value_parameters.register_category "d-gauges"
-module D_Impl : Abstract_domain.S
+module D : Abstract_domain.Leaf
with type state = G.t
and type value = Cvalue.V.t
and type location = Precise_locs.precise_location
@@ -1128,8 +1130,8 @@ module D_Impl : Abstract_domain.S
type origin
include G
+ include Domain_builder.Complete (struct include G let top = empty end)
- let name = "gauges"
let log_category = dkey
let empty _ = G.empty
@@ -1304,5 +1306,3 @@ module D_Impl : Abstract_domain.S
let top = G.empty (* must not be used, not neutral w.r.t. join (because
join crashes...)!! *)
end
-
-module D = Domain_builder.Complete (D_Impl)
diff --git a/src/plugins/value/domains/inout_domain.ml b/src/plugins/value/domains/inout_domain.ml
index bbcad31558f..3d99d563f6c 100644
--- a/src/plugins/value/domains/inout_domain.ml
+++ b/src/plugins/value/domains/inout_domain.ml
@@ -95,6 +95,8 @@ module LatticeInout = struct
end)
+ let name = "inout"
+
(* Initial abstract at the beginning of the computation: nothing written
or read so far. *)
let empty = {
@@ -204,7 +206,7 @@ module Transfer = struct
end
-module Internal
+module D
(*: Domain_builder.InputDomain
with type state = inout
and type value = Cvalue.V.t
@@ -220,7 +222,8 @@ module Internal
include Abstract_domain.Lattice with type state := state
end)
- let name = "inout"
+ include Domain_builder.Complete (LatticeInout)
+
let log_category = Value_parameters.register_category "d-inout"
let enter_scope _kind _vars state = state
@@ -284,9 +287,6 @@ module Internal
end
-module D = Domain_builder.Complete (Internal)
-
-
(*
Local Variables:
compile-command: "make -C ../../.."
diff --git a/src/plugins/value/domains/multidim_domain.ml b/src/plugins/value/domains/multidim_domain.ml
index fb5764a5151..e9928248897 100644
--- a/src/plugins/value/domains/multidim_domain.ml
+++ b/src/plugins/value/domains/multidim_domain.ml
@@ -231,7 +231,7 @@ struct
end
-module DomainPrototype =
+module DomainLattice =
struct
(* The domain is essentially a map from bases to individual memory abstractions *)
module Initial_Values = struct let v = [[]] end
@@ -241,16 +241,6 @@ struct
(Base.Base) (Memory)
(Hptmap.Comp_unused) (Initial_Values) (Deps)
- type state = t
- type value = Value.t
- type base = Base.t
- type offset = Location.offset
- type memory = Memory.t
- type location = Precise_locs.precise_location
- type mdlocation = Location.t (* should be = to location *)
- type origin
-
-
let name = "multidim"
let log_category = dkey
@@ -295,6 +285,23 @@ struct
in
inter ~cache:Hptmap_sig.NoCache ~symmetric:false ~idempotent:true ~decide
+end
+
+module Domain =
+struct
+
+ include DomainLattice
+ include Domain_builder.Complete (DomainLattice)
+
+ type state = t
+ type value = Value.t
+ type base = Base.t
+ type offset = Location.offset
+ type memory = Memory.t
+ type location = Precise_locs.precise_location
+ type mdlocation = Location.t (* should be = to location *)
+ type origin
+
(* Bases handling *)
@@ -556,7 +563,7 @@ struct
let relate _kf _bases _state = Base.SetLattice.empty
let filter _kf _kind bases state =
- filter (fun elt -> Base.Hptset.mem elt bases) state
+ DomainLattice.filter (fun elt -> Base.Hptset.mem elt bases) state
let reuse _kf bases ~current_input ~previous_output =
let cache = Hptmap_sig.NoCache in
@@ -569,5 +576,4 @@ struct
current_input previous_output
end
-
-include Domain_builder.Complete (DomainPrototype)
+include Domain
diff --git a/src/plugins/value/domains/octagons.ml b/src/plugins/value/domains/octagons.ml
index cdccda505e9..5b0fa411508 100644
--- a/src/plugins/value/domains/octagons.ml
+++ b/src/plugins/value/domains/octagons.ml
@@ -753,6 +753,9 @@ module State = struct
Format.fprintf fmt "@[%a@]" Octagons.pretty octagons
end)
+ let name = "octagon"
+ let log_category = Value_parameters.register_category "d-octagon"
+
let pretty_debug fmt { octagons; intervals; relations } =
Format.fprintf fmt "@[<v> Octagons: %a@; Intervals: %a@; Relations: %a@]"
Octagons.pretty octagons Intervals.pretty intervals
@@ -1034,6 +1037,7 @@ end
module Domain = struct
include State
+ include Domain_builder.Complete (State)
type value = Cvalue.V.t
type location = Precise_locs.precise_location
@@ -1320,8 +1324,6 @@ module Domain = struct
relations = join_rel prev_output.relations current_input.relations;
modified = current_input.modified }
- let name = "octagon"
- let log_category = Value_parameters.register_category "d-octagon"
end
-include Domain_builder.Complete (Domain)
+include Domain
diff --git a/src/plugins/value/domains/offsm_domain.ml b/src/plugins/value/domains/offsm_domain.ml
index 2818f14c91f..7f4e4b4846b 100644
--- a/src/plugins/value/domains/offsm_domain.ml
+++ b/src/plugins/value/domains/offsm_domain.ml
@@ -86,10 +86,12 @@ module Memory = struct
widen wh s1 s2
let narrow x _y = `Value x
+
+ let name = "bitwise"
end
-module Internal : Domain_builder.InputDomain
+module D : Abstract_domain.Leaf
with type state = Memory.t
and type value = offsm_or_top
and type location = Precise_locs.precise_location
@@ -104,7 +106,8 @@ module Internal : Domain_builder.InputDomain
include Abstract_domain.Lattice with type state := state
end)
- let name = "bitwise"
+ include Domain_builder.Complete (Memory)
+
let log_category = dkey
let empty _ = Memory.empty_map
@@ -233,6 +236,3 @@ module Internal : Domain_builder.InputDomain
let evaluate_predicate _ _ _ = Alarmset.Unknown
let reduce_by_predicate _ state _ _ = `Value state
end
-
-
-module D = Domain_builder.Complete (Internal)
diff --git a/src/plugins/value/domains/simple_memory.ml b/src/plugins/value/domains/simple_memory.ml
index b8260e5834d..80c5dbce55e 100644
--- a/src/plugins/value/domains/simple_memory.ml
+++ b/src/plugins/value/domains/simple_memory.ml
@@ -176,7 +176,7 @@ module Make_Memory (Value: Value) = struct
end
-module Make_Internal (Info: sig val name: string end) (Value: Value) = struct
+module Make_Domain (Info: sig val name: string end) (Value: Value) = struct
let table = Hashtbl.create 17
let () =
@@ -186,7 +186,10 @@ module Make_Internal (Info: sig val name: string end) (Value: Value) = struct
try Some (Hashtbl.find table name)
with Not_found -> None
- include Make_Memory (Value)
+ module M = Make_Memory (Value)
+ include M
+
+ include Domain_builder.Complete (M)
let name = Info.name
@@ -344,13 +347,7 @@ module Make_Internal (Info: sig val name: string end) (Value: Value) = struct
merge ~cache ~symmetric:false ~idempotent:true
~decide_both ~decide_left:(Traversing decide_left) ~decide_right:Neutral
current_input previous_output
-end
-
-module Make_Domain (Info: sig val name: string end) (Value: Value) =
-struct
- module M = Make_Internal (Info) (Value)
- include Domain_builder.Complete (M)
let add = M.add
let find = M.find
let remove = M.remove
diff --git a/src/plugins/value/domains/symbolic_locs.ml b/src/plugins/value/domains/symbolic_locs.ml
index 840e4fdbb09..8e49fd93cf7 100644
--- a/src/plugins/value/domains/symbolic_locs.ml
+++ b/src/plugins/value/domains/symbolic_locs.ml
@@ -215,6 +215,8 @@ module Memory = struct
end)
+ let name = "symbolic-locations"
+
let top = {
values = K2V.M.empty;
zones = K2Z.empty;
@@ -454,7 +456,7 @@ module Memory = struct
syntactic_deps = B2K.union into.syntactic_deps t.syntactic_deps }
end
-module Internal : Domain_builder.InputDomain
+module D : Abstract_domain.Leaf
with type state = Memory.t
and type value = V.t
and type location = Precise_locs.precise_location
@@ -469,7 +471,8 @@ module Internal : Domain_builder.InputDomain
include Abstract_domain.Lattice with type state := state
end)
- let name = "symbolic-locations"
+ include Domain_builder.Complete (Memory)
+
let log_category = dkey
let empty _ = Memory.empty_map
@@ -640,5 +643,3 @@ module Internal : Domain_builder.InputDomain
let evaluate_predicate _ _ _ = Alarmset.Unknown
let reduce_by_predicate _ state _ _ = `Value state
end
-
-module D = Domain_builder.Complete (Internal)
diff --git a/src/plugins/value/domains/taint_domain.ml b/src/plugins/value/domains/taint_domain.ml
index 6bf2ad5f6e7..6ac9fe86559 100644
--- a/src/plugins/value/domains/taint_domain.ml
+++ b/src/plugins/value/domains/taint_domain.ml
@@ -106,6 +106,8 @@ module LatticeTaint = struct
end)
+ let name = "taint"
+
(* Initial state at the start of the computation: nothing is tainted yet. *)
let empty = {
locs_data = Zone.bottom;
@@ -329,7 +331,7 @@ module ReuseTaint = struct
end
-module InternalTaint = struct
+module TaintDomain = struct
type state = taint
type value = Cvalue.V.t
type location = Precise_locs.precise_location
@@ -340,6 +342,8 @@ module InternalTaint = struct
include Abstract_domain.Lattice with type state := state
end)
+ include Domain_builder.Complete (LatticeTaint)
+
include (QueriesTaint: Abstract_domain.Queries
with type state := state
and type value := value
@@ -354,7 +358,6 @@ module InternalTaint = struct
include (ReuseTaint: Abstract_domain.Reuse with type t := state)
- let name = "taint"
let log_category = dkey
@@ -415,5 +418,4 @@ module InternalTaint = struct
let leave_loop _ state = state
end
-
-include Domain_builder.Complete (InternalTaint)
+include TaintDomain
diff --git a/src/plugins/value/domains/traces_domain.ml b/src/plugins/value/domains/traces_domain.ml
index e29351acf71..25e01df3368 100644
--- a/src/plugins/value/domains/traces_domain.ml
+++ b/src/plugins/value/domains/traces_domain.ml
@@ -571,6 +571,8 @@ module Traces = struct
end)
+ let name = "traces"
+
let view m =
if m == top then `Top
else `Other m
@@ -844,174 +846,6 @@ let rec complete_graph (graph:Graph.t) =
) graph Graph.empty
-module Internal = struct
- type nonrec state = state
- type value = Cvalue.V.t
- type location = Precise_locs.precise_location
- type origin
-
- include (Traces: sig
- include Datatype.S_with_collections with type t = state
- include Abstract_domain.Lattice with type state := state
- end)
-
- let name = "traces"
- let log_category = Value_parameters.register_category "d-traces"
-
- let assign ki lv e _v _valuation state =
- let trans = Assign (ki, lv.Eval.lval, lv.Eval.ltyp, e) in
- `Value (Traces.add_trans state trans)
-
- let assume stmt e pos _valuation state =
- let trans = Assume (stmt, e, pos) in
- `Value (Traces.add_trans state trans)
-
- let start_call stmt call _recursion _valuation state =
- let kf = call.Eval.kf in
- if Kernel_function.is_definition kf then
- let msg = Format.asprintf "start_call: %s (%b)" (Kernel_function.get_name call.Eval.kf)
- (Kernel_function.is_definition call.Eval.kf) in
- let state = Traces.add_trans state (Msg msg) in
- let formals = List.map (fun arg -> arg.Eval.formal) call.Eval.arguments in
- let state = Traces.add_trans state (EnterScope (kf, formals)) in
- let state = List.fold_left (fun state arg ->
- Traces.add_trans state
- (Assign (Kstmt stmt, Cil.var arg.Eval.formal,
- arg.Eval.formal.Cil_types.vtype,
- arg.Eval.concrete))) state call.Eval.arguments in
- `Value state
- else
- (** enter the scope of the dumb result variable *)
- let var = call.Eval.return in
- let state = match var with
- | Some var -> Traces.add_trans state (EnterScope (kf, [var]))
- | None -> state in
- let exps = List.map (fun arg -> arg.Eval.concrete) call.Eval.arguments in
- let state = Traces.add_trans state
- (CallDeclared (call.Eval.kf, exps, Option.map Cil.var var))
- in `Value {state with call_declared_function = true}
-
- let finalize_call _stmt call _recursion ~pre:_ ~post =
- if post.call_declared_function
- then `Value {post with call_declared_function = false}
- else
- let msg = Format.asprintf "finalize_call: %s" (Kernel_function.get_name call.Eval.kf) in
- let state = Traces.add_trans post (Msg msg) in
- `Value state
-
- let update _valuation state = `Value state
-
- let show_expr _valuation state fmt _expr = Traces.pretty fmt state
-
- (* Memexec *)
- (* This domains infers no relation between variables. *)
- let relate _kf _bases _state = Base.SetLattice.bottom
- (* Do not filter the state: the memexec cache will be applied only on function
- calls for which the entry states are equal. This almost completely
- disable memexec, but is always sound. *)
- let filter _kf _kind _bases state = state
- (* As memexec cache is only applied on equal entry states, the previous
- output state is a correct output for the current input state. *)
- let reuse _kf _bases ~current_input:_ ~previous_output:state = state
-
- let empty () = Traces.empty
- let initialize_variable lv _ ~initialized:_ _ state =
- Traces.add_trans state (Msg(Format.asprintf "initialize variable: %a" Printer.pp_lval lv ))
- let initialize_variable_using_type var_kind varinfo state =
- let kind_str =
- match var_kind with
- | Abstract_domain.Global -> "global"
- | Abstract_domain.Local _ -> "local"
- | Abstract_domain.Formal _ -> "formal"
- | Abstract_domain.Result _ -> "result"
- in
- let msg =
- Format.asprintf "initialize@ %s variable@ using@ type@ %a"
- kind_str Varinfo.pretty varinfo
- in
- Traces.add_trans state (Msg msg)
-
- (* TODO *)
- let logic_assign _assign _location state =
- Traces.add_trans state (Msg "logic assign")
-
- (* Logic *)
- let evaluate_predicate _ _ _ = Alarmset.Unknown
- let reduce_by_predicate _ state _ _ = `Value state
-
- let top_query = `Value (Cvalue.V.top, None), Alarmset.all
-
- let extract_expr ~oracle:_ _context _state _expr = top_query
- let extract_lval ~oracle:_ _context _state _lv _typ _locs = top_query
-
- let backward_location _state _lval _typ loc value =
- `Value (loc, value)
-
- let enter_loop stmt state =
- let state = Traces.add_trans state (Msg "enter_loop") in
- let state = if not (Value_parameters.TracesUnrollLoop.get ())
- then Traces.add_loop stmt state
- else { state with current = UnrollLoop(stmt,state.current) } in
- state
-
- let incr_loop_counter _ state =
- match state.current with
- | Base _ -> assert false
- | UnrollLoop(_,_) -> state
- | OpenLoop(stmt,s,last,_,g,l) ->
- let last = Graph.join last g in
- let last = if Value_parameters.TracesUnifyLoop.get () then
- let s',old_last = Stmt.Hashtbl.find state.all_loop_start stmt in
- let last = Graph.join last old_last in
- assert (Node.equal s s');
- Stmt.Hashtbl.add state.all_loop_start stmt (s,last);
- last
- else last
- in
- let current = OpenLoop(stmt,s,last,s,Graph.empty,l) in
- let state = { state with current } in
- (* Traces.add_trans state (Msg("incr_loop_counter")) *)
- state
-
- let leave_loop stmt' state =
- match state.current with
- | Base _ -> assert false (* absurd: we are in at least a loop *)
- | UnrollLoop(_,l) -> { state with current = l }
- | OpenLoop(stmt,s,last,old_current_node,g,current) ->
- assert (Stmt.equal stmt stmt');
- let state = { state with current } in
- let last = if Value_parameters.TracesUnifyLoop.get () then
- let s',old_last = Stmt.Hashtbl.find state.all_loop_start stmt in
- let last = Graph.join last old_last in
- assert (Node.equal s s');
- Stmt.Hashtbl.add state.all_loop_start stmt (s,last);
- last
- else last
- in
- let state = if Graph.is_empty last then state
- else Traces.add_trans state (Loop(stmt,s,last)) in
- let state = Traces.copy_edges s old_current_node g state in
- Traces.add_trans state (Msg "leave_loop")
-
-
- let enter_scope kind vars state =
- match kind with
- | Abstract_domain.Global ->
- { state with globals = vars @ state.globals }
- | Abstract_domain.Formal kf ->
- if Kernel_function.equal kf (fst (Globals.entry_point ()))
- then { state with main_formals = vars @ state.main_formals }
- else state
- | Abstract_domain.(Local kf | Result kf) ->
- Traces.add_trans state (EnterScope (kf, vars))
-
- let leave_scope kf vars state =
- Traces.add_trans state (LeaveScope (kf, vars))
-
- let reduce_further _state _expr _value = [] (*Nothing intelligent to suggest*)
-
-end
-
let dummy_loc = Location.unknown
let subst_in_full var_mapping =
@@ -1250,15 +1084,179 @@ let project_of_cfg vreturn s =
(* ) () *)
-let output_dot filename state =
- let out = open_out filename in
- Value_parameters.feedback ~dkey:Internal.log_category "@[Output dot produced to %s.@]" filename;
- (** *)
- GraphDot.output_graph out (complete_graph (snd (Traces.get_current state)));
- close_out out
-
module D = struct
- include Domain_builder.Complete (Internal)
+ type nonrec state = state
+ type value = Cvalue.V.t
+ type location = Precise_locs.precise_location
+ type origin
+
+ include (Traces: sig
+ include Datatype.S_with_collections with type t = state
+ include Abstract_domain.Lattice with type state := state
+ end)
+
+ include Domain_builder.Complete (Traces)
+
+ let log_category = Value_parameters.register_category "d-traces"
+
+ let assign ki lv e _v _valuation state =
+ let trans = Assign (ki, lv.Eval.lval, lv.Eval.ltyp, e) in
+ `Value (Traces.add_trans state trans)
+
+ let assume stmt e pos _valuation state =
+ let trans = Assume (stmt, e, pos) in
+ `Value (Traces.add_trans state trans)
+
+ let start_call stmt call _recursion _valuation state =
+ let kf = call.Eval.kf in
+ if Kernel_function.is_definition kf then
+ let msg = Format.asprintf "start_call: %s (%b)" (Kernel_function.get_name call.Eval.kf)
+ (Kernel_function.is_definition call.Eval.kf) in
+ let state = Traces.add_trans state (Msg msg) in
+ let formals = List.map (fun arg -> arg.Eval.formal) call.Eval.arguments in
+ let state = Traces.add_trans state (EnterScope (kf, formals)) in
+ let state = List.fold_left (fun state arg ->
+ Traces.add_trans state
+ (Assign (Kstmt stmt, Cil.var arg.Eval.formal,
+ arg.Eval.formal.Cil_types.vtype,
+ arg.Eval.concrete))) state call.Eval.arguments in
+ `Value state
+ else
+ (** enter the scope of the dumb result variable *)
+ let var = call.Eval.return in
+ let state = match var with
+ | Some var -> Traces.add_trans state (EnterScope (kf, [var]))
+ | None -> state in
+ let exps = List.map (fun arg -> arg.Eval.concrete) call.Eval.arguments in
+ let state = Traces.add_trans state
+ (CallDeclared (call.Eval.kf, exps, Option.map Cil.var var))
+ in `Value {state with call_declared_function = true}
+
+ let finalize_call _stmt call _recursion ~pre:_ ~post =
+ if post.call_declared_function
+ then `Value {post with call_declared_function = false}
+ else
+ let msg = Format.asprintf "finalize_call: %s" (Kernel_function.get_name call.Eval.kf) in
+ let state = Traces.add_trans post (Msg msg) in
+ `Value state
+
+ let update _valuation state = `Value state
+
+ let show_expr _valuation state fmt _expr = Traces.pretty fmt state
+
+ (* Memexec *)
+ (* This domains infers no relation between variables. *)
+ let relate _kf _bases _state = Base.SetLattice.bottom
+ (* Do not filter the state: the memexec cache will be applied only on function
+ calls for which the entry states are equal. This almost completely
+ disable memexec, but is always sound. *)
+ let filter _kf _kind _bases state = state
+ (* As memexec cache is only applied on equal entry states, the previous
+ output state is a correct output for the current input state. *)
+ let reuse _kf _bases ~current_input:_ ~previous_output:state = state
+
+ let empty () = Traces.empty
+ let initialize_variable lv _ ~initialized:_ _ state =
+ Traces.add_trans state (Msg(Format.asprintf "initialize variable: %a" Printer.pp_lval lv ))
+ let initialize_variable_using_type var_kind varinfo state =
+ let kind_str =
+ match var_kind with
+ | Abstract_domain.Global -> "global"
+ | Abstract_domain.Local _ -> "local"
+ | Abstract_domain.Formal _ -> "formal"
+ | Abstract_domain.Result _ -> "result"
+ in
+ let msg =
+ Format.asprintf "initialize@ %s variable@ using@ type@ %a"
+ kind_str Varinfo.pretty varinfo
+ in
+ Traces.add_trans state (Msg msg)
+
+ (* TODO *)
+ let logic_assign _assign _location state =
+ Traces.add_trans state (Msg "logic assign")
+
+ (* Logic *)
+ let evaluate_predicate _ _ _ = Alarmset.Unknown
+ let reduce_by_predicate _ state _ _ = `Value state
+
+ let top_query = `Value (Cvalue.V.top, None), Alarmset.all
+
+ let extract_expr ~oracle:_ _context _state _expr = top_query
+ let extract_lval ~oracle:_ _context _state _lv _typ _locs = top_query
+
+ let backward_location _state _lval _typ loc value =
+ `Value (loc, value)
+
+ let enter_loop stmt state =
+ let state = Traces.add_trans state (Msg "enter_loop") in
+ let state = if not (Value_parameters.TracesUnrollLoop.get ())
+ then Traces.add_loop stmt state
+ else { state with current = UnrollLoop(stmt,state.current) } in
+ state
+
+ let incr_loop_counter _ state =
+ match state.current with
+ | Base _ -> assert false
+ | UnrollLoop(_,_) -> state
+ | OpenLoop(stmt,s,last,_,g,l) ->
+ let last = Graph.join last g in
+ let last = if Value_parameters.TracesUnifyLoop.get () then
+ let s',old_last = Stmt.Hashtbl.find state.all_loop_start stmt in
+ let last = Graph.join last old_last in
+ assert (Node.equal s s');
+ Stmt.Hashtbl.add state.all_loop_start stmt (s,last);
+ last
+ else last
+ in
+ let current = OpenLoop(stmt,s,last,s,Graph.empty,l) in
+ let state = { state with current } in
+ (* Traces.add_trans state (Msg("incr_loop_counter")) *)
+ state
+
+ let leave_loop stmt' state =
+ match state.current with
+ | Base _ -> assert false (* absurd: we are in at least a loop *)
+ | UnrollLoop(_,l) -> { state with current = l }
+ | OpenLoop(stmt,s,last,old_current_node,g,current) ->
+ assert (Stmt.equal stmt stmt');
+ let state = { state with current } in
+ let last = if Value_parameters.TracesUnifyLoop.get () then
+ let s',old_last = Stmt.Hashtbl.find state.all_loop_start stmt in
+ let last = Graph.join last old_last in
+ assert (Node.equal s s');
+ Stmt.Hashtbl.add state.all_loop_start stmt (s,last);
+ last
+ else last
+ in
+ let state = if Graph.is_empty last then state
+ else Traces.add_trans state (Loop(stmt,s,last)) in
+ let state = Traces.copy_edges s old_current_node g state in
+ Traces.add_trans state (Msg "leave_loop")
+
+
+ let enter_scope kind vars state =
+ match kind with
+ | Abstract_domain.Global ->
+ { state with globals = vars @ state.globals }
+ | Abstract_domain.Formal kf ->
+ if Kernel_function.equal kf (fst (Globals.entry_point ()))
+ then { state with main_formals = vars @ state.main_formals }
+ else state
+ | Abstract_domain.(Local kf | Result kf) ->
+ Traces.add_trans state (EnterScope (kf, vars))
+
+ let leave_scope kf vars state =
+ Traces.add_trans state (LeaveScope (kf, vars))
+
+ let reduce_further _state _expr _value = [] (*Nothing intelligent to suggest*)
+
+ let output_dot filename state =
+ let out = open_out filename in
+ Value_parameters.feedback ~dkey:log_category "@[Output dot produced to %s.@]" filename;
+ (** *)
+ GraphDot.output_graph out (complete_graph (snd (Traces.get_current state)));
+ close_out out
let post_analysis state =
let return_stmt = Kernel_function.find_return (fst (Globals.entry_point ())) in
@@ -1267,7 +1265,7 @@ module D = struct
| _ -> assert false in
let header fmt = Format.fprintf fmt "Trace domains:" in
let body = Bottom.pretty Traces.pretty in
- Value_parameters.printf ~dkey:Internal.log_category ~header " @[%a@]" body state;
+ Value_parameters.printf ~dkey:log_category ~header " @[%a@]" body state;
if Value_parameters.TracesProject.get () ||
not (Value_parameters.TracesDot.is_default ()) then
match state with
diff --git a/src/plugins/value/utils/abstract.ml b/src/plugins/value/utils/abstract.ml
index b7158ae6e3f..84c9df46890 100644
--- a/src/plugins/value/utils/abstract.ml
+++ b/src/plugins/value/utils/abstract.ml
@@ -72,13 +72,13 @@ end
module Domain = struct
module D = struct
- type 'a t = (module Abstract_domain.Internal with type state = 'a)
+ type 'a t = (module Abstract_domain.S with type state = 'a)
end
include Structure.Shape (Structure.Key_Domain) (D)
module type Internal = sig
- include Abstract_domain.Internal
+ include Abstract_domain.S
val structure: t structure
end
diff --git a/src/plugins/value/utils/abstract.mli b/src/plugins/value/utils/abstract.mli
index 643159a7b00..5ea4d7e8531 100644
--- a/src/plugins/value/utils/abstract.mli
+++ b/src/plugins/value/utils/abstract.mli
@@ -98,10 +98,10 @@ end
module Domain : sig
include Structure.Shape
with type 'a key = 'a Structure.Key_Domain.key
- and type 'a data = (module Abstract_domain.Internal with type state = 'a)
+ and type 'a data = (module Abstract_domain.S with type state = 'a)
module type Internal = sig
- include Abstract_domain.Internal
+ include Abstract_domain.S
val structure: t structure
end
--
GitLab