diff --git a/ivette/src/dome/renderer/layout/style.css b/ivette/src/dome/renderer/layout/style.css
index a2e0fca13db2095fde266199646103b6c8264367..41dfbcc3254a14b6e4c9ff107da9d50735193f12 100644
--- a/ivette/src/dome/renderer/layout/style.css
+++ b/ivette/src/dome/renderer/layout/style.css
@@ -103,7 +103,6 @@
.dome-xSplitter-block {
display: block;
- overflow: hidden;
position: relative;
width: 100%;
height: 100%;
diff --git a/ivette/src/frama-c/plugins/eva/DomainStates.tsx b/ivette/src/frama-c/plugins/eva/DomainStates.tsx
new file mode 100644
index 0000000000000000000000000000000000000000..dab3218c24ad0398e44e8b525e703ed1508fcf7b
--- /dev/null
+++ b/ivette/src/frama-c/plugins/eva/DomainStates.tsx
@@ -0,0 +1,129 @@
+/* ************************************************************************ */
+/* */
+/* This file is part of Frama-C. */
+/* */
+/* Copyright (C) 2007-2022 */
+/* CEA (Commissariat à l'énergie atomique et aux énergies */
+/* alternatives) */
+/* */
+/* you can redistribute it and/or modify it under the terms of the GNU */
+/* Lesser General Public License as published by the Free Software */
+/* Foundation, version 2.1. */
+/* */
+/* It is distributed in the hope that it will be useful, */
+/* but WITHOUT ANY WARRANTY; without even the implied warranty of */
+/* MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the */
+/* GNU Lesser General Public License for more details. */
+/* */
+/* See the GNU Lesser General Public License version 2.1 */
+/* for more details (enclosed in the file licenses/LGPLv2.1). */
+/* */
+/* ************************************************************************ */
+
+// React & Dome
+import React from 'react';
+import * as Ivette from 'ivette';
+import * as States from 'frama-c/states';
+import { GlobalState, useGlobalState } from 'dome/data/states';
+import * as Eva from 'frama-c/plugins/eva/api/general';
+import * as Boxes from 'dome/layout/boxes';
+import { HSplit } from 'dome/layout/splitters';
+import { Text } from 'frama-c/richtext';
+import { Checkbox, Select } from 'dome/controls/buttons';
+import { Label } from 'dome/controls/labels';
+
+const globalSelectedDomain = new GlobalState("");
+const globalFilter = new GlobalState(true);
+
+export function EvaStates(): JSX.Element {
+ const [selection] = States.useSelection();
+ const selectedLoc = selection?.current;
+ const marker = selectedLoc?.marker;
+ const [domains, setDomains] = React.useState<string[]>([]);
+ const [selected, setSelected] = useGlobalState(globalSelectedDomain);
+ const [stateBefore, setStateBefore] = React.useState("");
+ const [stateAfter, setStateAfter] = React.useState("");
+ const [filter, setFilter] = useGlobalState(globalFilter);
+
+ const requestArg = marker ? [marker, filter] : undefined;
+ const states = States.useRequest(Eva.getStates, requestArg);
+
+ React.useEffect(() => {
+ if (states && states.length > 0) {
+ const names = states.map((d) => d[0]);
+ setDomains(names);
+ if (!names.includes(selected))
+ setSelected(names[0]);
+ const selectedDomain = states.find((d) => d[0] === selected);
+ if (selectedDomain) {
+ setStateBefore(selectedDomain[1]);
+ setStateAfter(selectedDomain[2]);
+ }
+ } else
+ setDomains([]);
+ }, [states, selected, setSelected]);
+
+ if (domains.length === 0)
+ return (<></>);
+
+ function makeOption(name: string): React.ReactNode {
+ return <option value={name}>{name}</option>;
+ }
+ const list = React.Children.toArray(domains.map(makeOption));
+
+ return (
+ <>
+ <Boxes.Hbox className="domain-state-box">
+ <Label>Domain: </Label>
+ <Select
+ title="Select the analysis domain to be shown"
+ value={selected}
+ onChange={(domain) => setSelected(domain ?? "")}
+ >
+ {list}
+ </Select>
+ <Boxes.Filler/>
+ <Checkbox
+ label="Filtered state"
+ title="If enabled, only the part of the states relevant to the
+ selected marker are shown, for domains supporting this feature.
+ For other domains or if disabled, entire domain states are printed.
+ Beware that entire domain states can be very large."
+ value={filter}
+ onChange={setFilter}
+ />
+ </Boxes.Hbox>
+ <Boxes.Scroll>
+ <HSplit
+ settings="ivette.eva.domainStates.beforeAfterSplit"
+ >
+ <div className="domain-state-box">
+ State before the selected statement:
+ <Text className="domain-state" text={stateBefore} />
+ </div>
+ <div className="domain-state-box">
+ State after the selected statement:
+ <Text className="domain-state" text={stateAfter} />
+ </div>
+ </HSplit>
+ </Boxes.Scroll>
+ </>);
+}
+
+function EvaStatesComponent(): JSX.Element {
+ return (
+ <>
+ <Ivette.TitleBar />
+ <EvaStates />
+ </>
+ );
+}
+
+Ivette.registerComponent({
+ id: 'frama-c.plugins.domain_states',
+ group: 'frama-c.plugins',
+ rank: 10,
+ label: 'Eva States',
+ title: 'States of the Eva analysis',
+ children: <EvaStatesComponent />,
+});
diff --git a/ivette/src/frama-c/plugins/eva/api/general/index.ts b/ivette/src/frama-c/plugins/eva/api/general/index.ts
index 55d8b6b7768e3e1717a91f126b192ce459c819bd..3ed2ea6b595d436fd82035130a5f13647d828103 100644
--- a/ivette/src/frama-c/plugins/eva/api/general/index.ts
+++ b/ivette/src/frama-c/plugins/eva/api/general/index.ts
@@ -580,4 +580,30 @@ export const functionStats: State.Array<
functionStatsData
> = functionStats_internal;
+const getStates_internal: Server.GetRequest<
+ [ marker, boolean ],
+ [ string, string, string ][]
+ > = {
+ kind: Server.RqKind.GET,
+ name: 'plugins.eva.general.getStates',
+ input: Json.jTry(
+ Json.jPair(
+ jMarkerSafe,
+ Json.jFail(Json.jBoolean,'Boolean expected'),
+ )),
+ output: Json.jList(
+ Json.jTry(
+ Json.jTriple(
+ Json.jFail(Json.jString,'String expected'),
+ Json.jFail(Json.jString,'String expected'),
+ Json.jFail(Json.jString,'String expected'),
+ ))),
+ signals: [],
+};
+/** Get the domain states about the given marker */
+export const getStates: Server.GetRequest<
+ [ marker, boolean ],
+ [ string, string, string ][]
+ >= getStates_internal;
+
/* ------------------------------------- */
diff --git a/ivette/src/frama-c/plugins/eva/index.tsx b/ivette/src/frama-c/plugins/eva/index.tsx
index 8aeb22bb817b5b6b873944d8b6f18ab43d2c4dff..36b6dc1d5ba54d5aede3104b1b40d767a38c784d 100644
--- a/ivette/src/frama-c/plugins/eva/index.tsx
+++ b/ivette/src/frama-c/plugins/eva/index.tsx
@@ -28,6 +28,7 @@ import * as Ivette from 'ivette';
import { } from 'frama-c/plugins/eva/valuetable';
import { } from './Summary';
import { } from './Coverage';
+import { } from './DomainStates';
import './style.css';
// --------------------------------------------------------------------------
diff --git a/ivette/src/frama-c/plugins/eva/style.css b/ivette/src/frama-c/plugins/eva/style.css
index e4a17e65e23a5e3baf3af13f49d6f319b4c86f35..2d6367d5845267d7a8f76eaca15084b32936e1e0 100644
--- a/ivette/src/frama-c/plugins/eva/style.css
+++ b/ivette/src/frama-c/plugins/eva/style.css
@@ -317,3 +317,20 @@ tr:first-of-type > .eva-table-callsite-box {
}
/* -------------------------------------------------------------------------- */
+/* --- Domains state print --- */
+/* -------------------------------------------------------------------------- */
+
+.domain-state-box {
+ margin: 6px;
+}
+
+.domain-state {
+ cursor: auto;
+ user-select: text;
+ overflow: auto;
+ padding: 6px;
+ margin-top: 6px;
+ background-color: var(--background-report);
+}
+
+/* -------------------------------------------------------------------------- */
diff --git a/src/kernel_services/abstract_interp/locations.ml b/src/kernel_services/abstract_interp/locations.ml
index d330023067eb7aa336fad8020cabdb397368f45c..1a19ba3926ebeb591bac02fb259657b22c9332d1 100644
--- a/src/kernel_services/abstract_interp/locations.ml
+++ b/src/kernel_services/abstract_interp/locations.ml
@@ -476,6 +476,8 @@ module Zone = struct
Base.SetLattice.mem b top_param
| Map m -> M.mem b m
+ let get_bases = get_keys
+
let shape x = x
let fold2_join_heterogeneous ~cache ~empty_left ~empty_right ~both ~join ~empty =
diff --git a/src/kernel_services/abstract_interp/locations.mli b/src/kernel_services/abstract_interp/locations.mli
index e071ac4420fcfa507a7e8c648830a58e0d15bc2a..982221c633d915dfc66a3f6c62ab94c7c76fa2b4 100644
--- a/src/kernel_services/abstract_interp/locations.mli
+++ b/src/kernel_services/abstract_interp/locations.mli
@@ -265,6 +265,10 @@ module Zone : sig
@since Carbon-20101201 *)
+ val get_bases : t -> Base.SetLattice.t
+ (** Returns the bases contained by the given zone. Never fails, but
+ may return [Base.SetLattice.Top]. *)
+
val intersects : t -> t -> bool
(** Assuming that [z1] and [z2] only contain valid bases,
diff --git a/src/plugins/value/api/general_requests.ml b/src/plugins/value/api/general_requests.ml
index 8a6068698cb4dc5568e7d35a761ccc781bc291a9..eb76164294fca8a88a3e39f3c1937a952a9308e1 100644
--- a/src/plugins/value/api/general_requests.ml
+++ b/src/plugins/value/api/general_requests.ml
@@ -261,7 +261,7 @@ let _array =
model
-(* ----- Analysis statistics -------------------------------------------- *)
+(* ----- Analysis statistics ------------------------------------------------ *)
module AlarmCategory = struct
open Server.Data
@@ -470,4 +470,76 @@ let _array =
model
-(**************************************************************************)
+(* ----- Domains states ----------------------------------------------------- *)
+
+let compute_lval_deps request lval =
+ let zone = Results.lval_deps lval request in
+ Locations.Zone.get_bases zone
+
+let compute_expr_deps request expr =
+ let zone = Results.expr_deps expr request in
+ Locations.Zone.get_bases zone
+
+let compute_instr_deps request = function
+ | Set (lval, expr, _) ->
+ Base.SetLattice.join
+ (compute_lval_deps request lval)
+ (compute_expr_deps request expr)
+ | Local_init (vi, AssignInit (SingleInit expr), _) ->
+ Base.SetLattice.join
+ (Base.SetLattice.inject_singleton (Base.of_varinfo vi))
+ (compute_expr_deps request expr)
+ | _ -> Base.SetLattice.empty
+
+let compute_stmt_deps request stmt =
+ match stmt.skind with
+ | Instr (instr) -> compute_instr_deps request instr
+ | If (expr, _, _, _) -> compute_expr_deps request expr
+ | _ -> Base.SetLattice.empty
+
+let compute_marker_deps request = function
+ | Printer_tag.PStmt (_, stmt)
+ | PStmtStart (_, stmt) -> compute_stmt_deps request stmt
+ | PLval (_, _, lval) -> compute_lval_deps request lval
+ | PExp (_, _, expr) -> compute_expr_deps request expr
+ | PVDecl (_, _, vi) -> Base.SetLattice.inject_singleton (Base.of_varinfo vi)
+ | _ -> Base.SetLattice.empty
+
+let get_filtered_state request marker =
+ let bases = compute_marker_deps request marker in
+ match bases with
+ | Base.SetLattice.Top -> Results.print_states request
+ | Base.SetLattice.Set bases ->
+ if Base.Hptset.is_empty bases
+ then []
+ else Results.print_states ~filter:bases request
+
+let get_state filter request marker =
+ if filter
+ then get_filtered_state request marker
+ else Results.print_states request
+
+let get_states (marker, filter) =
+ let kinstr = Printer_tag.ki_of_localizable marker in
+ match kinstr with
+ | Kglobal -> []
+ | Kstmt stmt ->
+ let states_before = get_state filter (Results.before stmt) marker in
+ let states_after = get_state filter (Results.after stmt) marker in
+ match states_before, states_after with
+ | [], _ -> List.map (fun (name, after) -> name, "", after) states_after
+ | _, [] -> List.map (fun (name, before) -> name, before, "") states_before
+ | _, _ ->
+ let join (name, before) (name', after) =
+ assert (name = name');
+ name, before, after
+ in
+ List.rev_map2 join states_before states_after
+
+let () = Request.register ~package
+ ~kind:`GET ~name:"getStates"
+ ~descr:(Markdown.plain "Get the domain states about the given marker")
+ ~input:(module Data.Jpair (Kernel_ast.Marker) (Data.Jbool))
+ ~output:(module Data.Jlist
+ (Data.Jtriple (Data.Jstring) (Data.Jstring) (Data.Jstring)))
+ get_states
diff --git a/src/plugins/value/domains/abstract_domain.mli b/src/plugins/value/domains/abstract_domain.mli
index e8536eb1f6e16c262d723f096cf919917e47eb29..6e36e58388bb196ca4fad8487d8c4a87a3863c2b 100644
--- a/src/plugins/value/domains/abstract_domain.mli
+++ b/src/plugins/value/domains/abstract_domain.mli
@@ -338,19 +338,24 @@ module type Reuse = sig
disables MemExec. *)
val relate: kernel_function -> Base.Hptset.t -> t -> Base.SetLattice.t
- (** [filter kf kind bases states] reduces the state [state] to only keep
+ (** [filter kind bases states] reduces the state [state] to only keep
properties about [bases] — it is a projection on the set of [bases].
It allows reusing an analysis of [kf] from an initial state [pre] to a
final state [post].
- If [kind] is `Pre, [state] is the initial state [pre], and [bases]
- includes all inputs of [kf] and satisfies [relate kf bases state = bases].
- If [kind] is `Post, [state] is the final state [post], and [bases]
+ If [kind] is [`Pre kf], [state] is the initial state of function [kf],
+ and [bases] includes all inputs of [kf] and satisfies
+ [relate kf bases state = bases].
+ If [kind] is [`Post kf], [state] is the final state of [kf], and [bases]
includes all inputs and outputs of [kf].
Afterwards, the two resulting states [reduced_pre] and [reduced_post] are
used as follow: when [kf] should be analyzed with the initial state [s],
if [filter kf `Pre s = reduced_pre], then the analysis is skipped, and
- [reuse kf s reduced_post] is used as its final state instead. *)
- val filter: kernel_function -> [`Pre | `Post] -> Base.Hptset.t -> t -> t
+ [reuse kf s reduced_post] is used as its final state instead.
+ If [kind] is [`Print], the state is reduced before printing it for the
+ end-user. *)
+ val filter:
+ [`Pre of kernel_function | `Post of kernel_function | `Print ] ->
+ Base.Hptset.t -> t -> t
(** [reuse kf bases current_input previous_output] merges the initial state
[current_input] with a final state [previous_output] from a previous
@@ -376,6 +381,10 @@ module type S = sig
type state
include Datatype.S_with_collections with type t = state
+ (* The domain name, shown in some logs and in the GUI. Be sure to redefine a
+ clear and simple name instead of the default one coming from Datatype. *)
+ val name: string
+
(** {3 Lattice Structure } *)
include Lattice with type state := t
diff --git a/src/plugins/value/domains/cvalue/cvalue_domain.ml b/src/plugins/value/domains/cvalue/cvalue_domain.ml
index 77f90be12ff69cc314f8da40cba6f39990e344c1..68d1f194f995758cef798ecbed61fbfd4c22ce52 100644
--- a/src/plugins/value/domains/cvalue/cvalue_domain.ml
+++ b/src/plugins/value/domains/cvalue/cvalue_domain.ml
@@ -181,7 +181,8 @@ module State = struct
let mem_project = Datatype.never_any_project
end )
- let key = Structure.Key_Domain.create_key "cvalue_domain"
+ let name = "cvalue"
+ let key = Structure.Key_Domain.create_key name
type value = Model.value
type location = Model.location
@@ -287,7 +288,7 @@ module State = struct
let relate _kf _bases _state = Base.SetLattice.empty
(* Auxiliary function that keeps only some bases inside a memory state *)
- let filter _kf _kind bases (state, clob) =
+ let filter _kind bases (state, clob) =
Cvalue.Model.filter_by_shape bases state, clob
let reuse _ _ ~current_input:(state, _) ~previous_output:(output, clob) =
diff --git a/src/plugins/value/domains/domain_builder.ml b/src/plugins/value/domains/domain_builder.ml
index 141c643cc703d84b082afa5a7af9e5b6355a0b92..bea7217028e5f618e54498e1c2d54c4bf404fc6e 100644
--- a/src/plugins/value/domains/domain_builder.ml
+++ b/src/plugins/value/domains/domain_builder.ml
@@ -46,7 +46,9 @@ module type LeafDomain = sig
val incr_loop_counter: stmt -> t -> t
val leave_loop: stmt -> t -> t
- val filter: kernel_function -> [`Pre | `Post] -> Base.Hptset.t -> t -> t
+ val filter:
+ [`Pre of kernel_function | `Post of kernel_function | `Print ] ->
+ Base.Hptset.t -> t -> t
val reuse:
kernel_function -> Base.Hptset.t ->
current_input:t -> previous_output:t -> t
@@ -72,7 +74,7 @@ module Complete (Domain: InputDomain) = struct
let incr_loop_counter _stmt state = state
let leave_loop _stmt state = state
- let filter _kf _kind _bases state = state
+ let filter _kind _bases state = state
let reuse _kf _bases ~current_input:_ ~previous_output = previous_output
let show_expr _valuation _state fmt _expr =
@@ -325,6 +327,7 @@ module Restrict
module I = struct let module_name = Domain.name ^ " option" end
include Datatype.Option_with_collections (D) (I)
+ let name = Domain.name
let default = Domain.top, Mode.all
let structure: t Abstract.Domain.structure =
@@ -575,9 +578,9 @@ module Restrict
| None -> Base.SetLattice.empty
| Some (state, _mode) -> Domain.relate kf bases state
- let filter kf kind bases = function
+ let filter kind bases = function
| None -> None
- | Some (state, mode) -> Some (Domain.filter kf kind bases state, mode)
+ | Some (state, mode) -> Some (Domain.filter kind bases state, mode)
let reuse kf bases ~current_input ~previous_output =
match current_input, previous_output with
diff --git a/src/plugins/value/domains/domain_builder.mli b/src/plugins/value/domains/domain_builder.mli
index bf3c05b8f0cc79efed1e2e4ec30131f737bd49df..d4356a571fd6e3ed178c3f7d62037167d36816ae 100644
--- a/src/plugins/value/domains/domain_builder.mli
+++ b/src/plugins/value/domains/domain_builder.mli
@@ -27,6 +27,8 @@ open Cil_types
open Eval
module type InputDomain = sig
+ (* The [name] value from Datatype should be the domain name and will be used
+ in some logs and in the GUI for the end-user. *)
include Datatype.S
val top: t
val join: t -> t -> t
@@ -52,7 +54,9 @@ module type LeafDomain = sig
val incr_loop_counter: stmt -> t -> t
val leave_loop: stmt -> t -> t
- val filter: kernel_function -> [`Pre | `Post] -> Base.Hptset.t -> t -> t
+ val filter:
+ [`Pre of kernel_function | `Post of kernel_function | `Print ] ->
+ Base.Hptset.t -> t -> t
val reuse:
kernel_function -> Base.Hptset.t ->
current_input:t -> previous_output:t -> t
diff --git a/src/plugins/value/domains/domain_product.ml b/src/plugins/value/domains/domain_product.ml
index 550a86f3d45fd987f474e297732ee21553b1f157..52abf820dee9979a0b9b0fc711dfccce911fa939 100644
--- a/src/plugins/value/domains/domain_product.ml
+++ b/src/plugins/value/domains/domain_product.ml
@@ -42,14 +42,15 @@ module Make
}
let () = incr counter
- let name = Left.name ^ "*" ^ Right.name ^
- "(" ^ string_of_int !counter ^ ")"
+ let unique_name = Left.name ^ "*" ^ Right.name ^
+ "(" ^ string_of_int !counter ^ ")"
include Datatype.Pair_with_collections
(Left)
(Right)
- (struct let module_name = name end)
+ (struct let module_name = unique_name end)
type state = t
+ let name = Left.name ^ " * " ^ Right.name
let structure = Abstract.Domain.Node (Left.structure, Right.structure)
@@ -292,8 +293,8 @@ module Make
let relate kf bases (left, right) =
Base.SetLattice.join
(Left.relate kf bases left) (Right.relate kf bases right)
- let filter kf kind bases (left, right) =
- Left.filter kf kind bases left, Right.filter kf kind bases right
+ let filter kind bases (left, right) =
+ Left.filter kind bases left, Right.filter kind bases right
let reuse kf bases ~current_input ~previous_output =
let left_input, right_input = current_input
and left_output, right_output = previous_output in
diff --git a/src/plugins/value/domains/equality/equality_domain.ml b/src/plugins/value/domains/equality/equality_domain.ml
index 44604b43c15df1ff2c12a3940b0d0d745d580dff..542d48cc2ce424ece24b54e1cdfc07a6428bab75 100644
--- a/src/plugins/value/domains/equality/equality_domain.ml
+++ b/src/plugins/value/domains/equality/equality_domain.ml
@@ -121,6 +121,8 @@ module Internal = struct
type state = t
+ let name = "equality"
+
let log_category = dkey
let pretty fmt (eqs, _, _) = Equality.Set.pretty fmt eqs
diff --git a/src/plugins/value/domains/gauges/gauges_domain.ml b/src/plugins/value/domains/gauges/gauges_domain.ml
index 7a91a6af3f8e2dc22c04e88287d12316f2853dd0..829afa083647c8d8e174c8e8c3a1303b840df1c9 100644
--- a/src/plugins/value/domains/gauges/gauges_domain.ml
+++ b/src/plugins/value/domains/gauges/gauges_domain.ml
@@ -532,6 +532,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
diff --git a/src/plugins/value/domains/inout_domain.ml b/src/plugins/value/domains/inout_domain.ml
index 8028b618a1d7e5df61659ebd87c72c7921f8ab96..63af3599eafb50965cc660d38e85473fa0d0a957 100644
--- a/src/plugins/value/domains/inout_domain.ml
+++ b/src/plugins/value/domains/inout_domain.ml
@@ -44,7 +44,7 @@ module LatticeInout = struct
include Datatype.Serializable_undefined
type t = inout
- let name = "Value.Inout.t"
+ let name = "inout"
let reprs = [ {
over_outputs = List.hd Zone.reprs;
diff --git a/src/plugins/value/domains/multidim/multidim_domain.ml b/src/plugins/value/domains/multidim/multidim_domain.ml
index 2f6459d9c5c63631f202e43bf47504a6dfb34690..e1300c7d470e968079b423f3a7a7e5ab2ac2476e 100644
--- a/src/plugins/value/domains/multidim/multidim_domain.ml
+++ b/src/plugins/value/domains/multidim/multidim_domain.ml
@@ -363,6 +363,8 @@ struct
(Datatype.Option (Tracking))
(struct let module_name = "DomainLattice" end)
+ let name = "multidim"
+
type state = t
type value = Value.t
type value_or_uninitialized = Value_or_Uninitialized.t
@@ -885,7 +887,7 @@ struct
let relate _kf _bases _state = Base.SetLattice.empty
- let filter _kf _kind bases (base_map,tracked : t) =
+ let filter _kind bases (base_map,tracked : t) =
BaseMap.filter (fun elt -> Base.Hptset.mem elt bases) base_map,
Option.map (Tracking.inter bases) tracked
diff --git a/src/plugins/value/domains/octagons.ml b/src/plugins/value/domains/octagons.ml
index 757ad4d87ecadaba7e9b0bfe9fa985c413fba7f6..b463daa3ac3b49fe3278cbb5e441cc55547f1616 100644
--- a/src/plugins/value/domains/octagons.ml
+++ b/src/plugins/value/domains/octagons.ml
@@ -701,7 +701,7 @@ module State = struct
type t = state
include Datatype.Serializable_undefined
- let name = "Octagons.State"
+ let name = "octagon"
let structural_descr =
Structural_descr.t_record
[| Octagons.packed_descr;
@@ -1275,7 +1275,7 @@ module Domain = struct
in
Base.Hptset.fold aux bases Base.SetLattice.empty
- let filter _kf _kind bases state =
+ let filter _kind bases state =
if intraprocedural ()
then state
else
diff --git a/src/plugins/value/domains/offsm_domain.ml b/src/plugins/value/domains/offsm_domain.ml
index 66ffd1337c2b6e88dd72b51d5fbc08a9ccea7c64..396598578c7eb76547068d810671bdde1078ab3b 100644
--- a/src/plugins/value/domains/offsm_domain.ml
+++ b/src/plugins/value/domains/offsm_domain.ml
@@ -81,6 +81,8 @@ module Memory = struct
include
Lmap.Make_LOffset(V_Or_Uninitialized)(V_Offsetmap)(Default_offsetmap)
+ let name = "bitwise"
+
let widen kf stmt s1 s2 =
let wh = Widen.getWidenHints kf stmt in
widen wh s1 s2
@@ -197,7 +199,7 @@ module D : Abstract_domain.Leaf
(* Memexec *)
let relate _kf _bases _state = Base.SetLattice.empty
- let filter _kf _kind bases state =
+ let filter _kind bases state =
Memory.filter_by_shape bases state
let reuse _kf bases ~current_input:input ~previous_output:output =
diff --git a/src/plugins/value/domains/printer_domain.ml b/src/plugins/value/domains/printer_domain.ml
index ab4c24f45a6d23b5a03fe815b68502fb7bfd454c..93abea72d3e62b33148dbcc5ede6db82b730a992 100644
--- a/src/plugins/value/domains/printer_domain.ml
+++ b/src/plugins/value/domains/printer_domain.ml
@@ -34,6 +34,7 @@ module Simple : Simpler_domains.Simple_Cvalue = struct
(* In this domain, the states contain nothing. We use [unit] as type formal
the state and we reuse [Datatype.Unit] as a base for our domain. *)
include Datatype.Unit
+ let name = "printer"
(* --- Lattice operators --- *)
diff --git a/src/plugins/value/domains/simple_memory.ml b/src/plugins/value/domains/simple_memory.ml
index 33bae1ed3a01b54fba5d06cbbfcb0fdf77549c77..a0ba820a46fc63cde8dd2449ba2787a536ac2c76 100644
--- a/src/plugins/value/domains/simple_memory.ml
+++ b/src/plugins/value/domains/simple_memory.ml
@@ -47,7 +47,7 @@ module type S = sig
val fold: (Base.t -> value -> 'a -> 'a) -> t -> 'a -> 'a
end
-module Make_Memory (Value: Value) = struct
+module Make_Memory (Info: sig val name: string end) (Value: Value) = struct
module Initial_Values = struct let v = [] end
module Deps = struct let l = [Ast.self] end
@@ -55,8 +55,10 @@ module Make_Memory (Value: Value) = struct
include Hptmap.Make
(Base.Base) (Value) (Hptmap.Comp_unused) (Initial_Values) (Deps)
+ let name = Info.name
+
let cache_name s =
- Hptmap_sig.PersistentCache ("Value." ^ Value.name ^ "." ^ s)
+ Hptmap_sig.PersistentCache ("Value." ^ name ^ "." ^ s)
let disjoint_union =
let cache = cache_name "union" in
@@ -186,7 +188,7 @@ module Make_Domain (Info: sig val name: string end) (Value: Value) = struct
try Some (Hashtbl.find table name)
with Not_found -> None
- module M = Make_Memory (Value)
+ module M = Make_Memory (Info) (Value)
include M
include Domain_builder.Complete (M)
@@ -325,7 +327,7 @@ module Make_Domain (Info: sig val name: string end) (Value: Value) = struct
let relate _kf _bases _state = Base.SetLattice.empty
- let filter _kf _kind bases state =
+ let filter _kind bases state =
M.filter (fun elt -> Base.Hptset.mem elt bases) state
let reuse _kf bases ~current_input ~previous_output =
diff --git a/src/plugins/value/domains/simple_memory.mli b/src/plugins/value/domains/simple_memory.mli
index a194b4fe98797e8aa3438a4109d488bcf1cdb048..bbbd93735a956fa1ca8c9f9b9cb14a30a2d562b4 100644
--- a/src/plugins/value/domains/simple_memory.mli
+++ b/src/plugins/value/domains/simple_memory.mli
@@ -86,7 +86,7 @@ module type S = sig
end
(* Builds a memory from a value abstraction. *)
-module Make_Memory (Value: Value) : sig
+module Make_Memory (Info: sig val name: string end) (Value: Value) : sig
include Datatype.S_with_collections
include S with type t := t
and type value := Value.t
diff --git a/src/plugins/value/domains/symbolic_locs.ml b/src/plugins/value/domains/symbolic_locs.ml
index 0d95237c6476678c6147b3ece9ad12a34fda9616..5ab410de611174dfee0f7a2ec1e9c1b20f128cea 100644
--- a/src/plugins/value/domains/symbolic_locs.ml
+++ b/src/plugins/value/domains/symbolic_locs.ml
@@ -182,7 +182,7 @@ module Memory = struct
include Datatype.Serializable_undefined
type t = memory
- let name = "Value.Symbolic_locs.Memory.t"
+ let name = "symbolic-locations"
let reprs = [ { values = List.hd K2V.M.reprs;
zones = List.hd K2Z.reprs;
@@ -603,7 +603,7 @@ module D : Abstract_domain.Leaf
by itself a variable read or written by f to a variable that is not. *)
let relate _kf _bases _state = Base.SetLattice.empty
- let filter _kf _kind = Memory.filter
+ let filter _kind = Memory.filter
(* Efficient version of [reuse], but the resulting state does not satisfy
the [_check state], as some extra dependenies of keys removed from the
diff --git a/src/plugins/value/domains/taint_domain.ml b/src/plugins/value/domains/taint_domain.ml
index 7d46ca1e8094212d0653b9db9d465f8deb6b053d..f32bc939b956f7adb1b141cb95258b418d0bb4fb 100644
--- a/src/plugins/value/domains/taint_domain.ml
+++ b/src/plugins/value/domains/taint_domain.ml
@@ -75,7 +75,7 @@ module LatticeTaint = struct
type t = taint
- let name = "Value.Taint.t"
+ let name = "taint"
let reprs =
[ { locs_data = List.hd Zone.reprs;
@@ -369,7 +369,7 @@ module TaintDomain = struct
(* MemExec cache. *)
let relate _kf _bases _state = Base.SetLattice.empty
- let filter _kf _kind bases state =
+ let filter _kind bases state =
let filter_base = Zone.filter_base (fun b -> Base.Hptset.mem b bases) in
{ state with locs_data = filter_base state.locs_data;
locs_control = filter_base state.locs_control;
diff --git a/src/plugins/value/domains/traces_domain.ml b/src/plugins/value/domains/traces_domain.ml
index 52e14219be6b7f3d87404deb6e778f55890cc0a2..98cd954008c82b4b7f0fd80fbe920b5bbea07c5c 100644
--- a/src/plugins/value/domains/traces_domain.ml
+++ b/src/plugins/value/domains/traces_domain.ml
@@ -532,7 +532,7 @@ module Traces = struct
include Datatype.Serializable_undefined
type t = state
- let name = "Value.Traces_domain.Traces.state"
+ let name = "traces"
let reprs = [empty]
diff --git a/src/plugins/value/domains/unit_domain.ml b/src/plugins/value/domains/unit_domain.ml
index 5307ef978d60d4ceeaf3a94501935175e8cfabc8..d7f7bb0a24495a638422370353bf576bbfee0e63 100644
--- a/src/plugins/value/domains/unit_domain.ml
+++ b/src/plugins/value/domains/unit_domain.ml
@@ -27,7 +27,7 @@ module Static = struct
include Datatype.Unit
type state = t
- let name = "Unit domain"
+ let name = "unit"
let log_category = log_key
let structure = Abstract.Domain.Unit
diff --git a/src/plugins/value/engine/abstractions.ml b/src/plugins/value/engine/abstractions.ml
index fedceb3f36ff2cd185349b8eb1b5f5303ce05829..c2221af95912657e3c1c5537a18c7ec5d8b94b5e 100644
--- a/src/plugins/value/engine/abstractions.ml
+++ b/src/plugins/value/engine/abstractions.ml
@@ -342,7 +342,6 @@ let add_domain (type v) dname mode (abstraction: v abstraction) (module Acc: Acc
(* Set the name of the domain. *)
let module Domain = struct
include (val domain)
- let name = dname
module Store = struct
include Store
let register_global_state storage state =
diff --git a/src/plugins/value/engine/mem_exec.ml b/src/plugins/value/engine/mem_exec.ml
index ecd7a20c34ac6a793fb64e296ecdde05306f9006..cf8268830c4cdfa967b46f8527067d1a27423d03 100644
--- a/src/plugins/value/engine/mem_exec.ml
+++ b/src/plugins/value/engine/mem_exec.ml
@@ -181,7 +181,7 @@ module Make
| Base.SetLattice.Top -> raise TooImprecise
| Base.SetLattice.Set bases -> bases
in
- let state_input = Domain.filter kf `Pre input_bases input_state in
+ let state_input = Domain.filter (`Pre kf) input_bases input_state in
(* Outputs bases, that is bases that are copy-pasted, also include
input bases. Indeed, those may get reduced during the call. *)
let all_output_bases =
@@ -197,7 +197,7 @@ module Make
Extlib.opt_fold Base.Hptset.add return_base all_output_bases
in
let clear (key,state) =
- key, Domain.filter kf `Post all_output_bases state
+ key, Domain.filter (`Post kf) all_output_bases state
in
let outputs = List.map clear call_result in
let call_number = current_counter () in
@@ -241,7 +241,7 @@ module Make
then ()
else
(* restrict [state] to the inputs of this call *)
- let st_filtered = Domain.filter kf `Pre binputs state in
+ let st_filtered = Domain.filter (`Pre kf) binputs state in
try
let bases, outputs, i = Domain.Hashtbl.find hstates st_filtered in
(* We have found a previous execution, in which the outputs are
diff --git a/src/plugins/value/utils/results.ml b/src/plugins/value/utils/results.ml
index 540bc32142af6c42de9b85c1dbca17bc36ab2504..56935b6b2281b2aaef1ea25d1ccc65ad6624b27c 100644
--- a/src/plugins/value/utils/results.ml
+++ b/src/plugins/value/utils/results.ml
@@ -293,6 +293,26 @@ struct
| Some extract ->
convert (Response.map_join extract Cvalue.Model.join (get req))
+ let print_states ?filter req =
+ let state = Response.map_join (fun x -> x) A.Dom.join (get req) in
+ let print (type s)
+ (key: s Abstract.Domain.key)
+ (module Domain: Abstract_domain.S with type state = s)
+ (state: s) acc =
+ let name = Structure.Key_Domain.name key in
+ let state =
+ match filter with
+ | None -> state
+ | Some bases -> Domain.filter `Print bases state
+ in
+ let str = Format.asprintf "%a" Domain.pretty state in
+ (name, str) :: acc
+ in
+ let polymorphic_fold_fun = A.Dom.{ fold = print } in
+ match state with
+ | `Top | `Bottom -> []
+ | `Value state -> A.Dom.fold polymorphic_fold_fun state []
+
(* Evaluation *)
let eval_lval lval req =
@@ -487,6 +507,10 @@ let get_cvalue_model req =
| Error Bottom -> Cvalue.Model.bottom
| Error (Top | DisabledDomain) -> Cvalue.Model.top
+let print_states ?filter req =
+ let module E = Make () in
+ E.print_states ?filter req
+
(* Depedencies *)
diff --git a/src/plugins/value/utils/results.mli b/src/plugins/value/utils/results.mli
index e6c0678569aa2f5e7077e6780f285ac667560a5f..e18f41a032527bbde86a2c4b4122423e202afb9d 100644
--- a/src/plugins/value/utils/results.mli
+++ b/src/plugins/value/utils/results.mli
@@ -161,6 +161,11 @@ val get_cvalue_model : request -> Cvalue.Model.t
(** Returns the Cvalue model. *)
val get_cvalue_model_result : request -> Cvalue.Model.t result
+(** Returns a textual representation of the internal domain states for the given
+ request. If [filter] is provided, states are filtered on the given bases
+ (for domains that support this feature).
+ Returns a list of pair (name, state) for all available domains. *)
+val print_states: ?filter:Base.Hptset.t -> request -> (string * string) list
(** Dependencies *)
diff --git a/src/plugins/value/utils/structure.ml b/src/plugins/value/utils/structure.ml
index 72cda0e26683743613099657926c9643456bb9f9..40733bca78a1e227aad8b2d39b822b546c94bf83 100644
--- a/src/plugins/value/utils/structure.ml
+++ b/src/plugins/value/utils/structure.ml
@@ -28,6 +28,7 @@ module type Key = sig
val create_key: string -> 'a key
val eq_type : 'a key -> 'b key -> ('a, 'b) eq option
+ val name: 'a key -> string
val print: 'a key Pretty_utils.formatter
val compare: 'a key -> 'b key -> int
val equal: 'a key -> 'b key -> bool
@@ -82,6 +83,7 @@ module Make () = struct
let hash x = x.tag
let tag x = x.tag
+ let name x = x.name
let print fmt x = Format.pp_print_string fmt x.name
end
diff --git a/src/plugins/value/utils/structure.mli b/src/plugins/value/utils/structure.mli
index 792d6a8376e50877c30eb25b760484db5f42b29d..f0c6ed245ddc9a7f9e7e3d8659a8a44e9448fb82 100644
--- a/src/plugins/value/utils/structure.mli
+++ b/src/plugins/value/utils/structure.mli
@@ -34,6 +34,7 @@ module type Key = sig
val create_key: string -> 'a key
val eq_type : 'a key -> 'b key -> ('a, 'b) eq option
+ val name: 'a key -> string
val print: 'a key Pretty_utils.formatter
val compare: 'a key -> 'b key -> int
val equal: 'a key -> 'b key -> bool