Debugger_utils.Exec_map
A map of execution of a function (symbolic or otherwise).
This is represented in a tree structure, where each node represents a command.
Each command node comes in one of these forms:
Cmd
) - a normal command with one command node as its child.BranchCmd
) - a command with one or more children, with each child identified by a branch case type; this represents a command that has multiple potential outcomes, depending on the program state (e.g. an if/else). Note that this is only interesting in symbolic execution; in concrete execution, they will always have exactly one branch case, thus functioning similarly to normal command nodes.FinalCmd
) - a command with no children; this represents the end of an execution branch, either due to errors, or normal termination (i.e. when returning from the function).These nodes also contain some (configurable) set of information - this usually includes the relevant report ID from the log database, a human-readable representation of the command, and any errors and matches that occurred during executing the command.
The child of a Cmd
node may be Nothing
, as can any child of a BranchCmd
node; this represents that there is a command here in the code, but it hasn't yet been executed. This is to facilitate the debugger's step-by-step behaviour.
A command node may also contain a submap; this embeds another exec map inside this command node, either described in full or referred to by name (see submap
). This is used to, for example, embed the body of a while-loop in the while-loop command itself.
val next_kind_to_yojson :
'c 'bd. ('c -> Yojson.Safe.t) ->
('bd -> Yojson.Safe.t) ->
('c, 'bd) next_kind ->
Yojson.Safe.t
val next_kind_of_yojson :
'c 'bd. (Yojson.Safe.t -> 'c Ppx_deriving_yojson_runtime.error_or) ->
(Yojson.Safe.t -> 'bd Ppx_deriving_yojson_runtime.error_or) ->
Yojson.Safe.t ->
('c, 'bd) next_kind Ppx_deriving_yojson_runtime.error_or
val kind_of_cases : 'a list -> ('a, unit) next_kind
Maps a list of branches to Normal
if empty, or Branch
An exec map / node in an exec map; takes the following type parameters:
'branch_case
: the type that identifies a branch case'cmd_data
: the type of the data attached to each non-Nothing
node'branch_data
: additional data attached to each branch caseval next_to_yojson :
'id 'case 'branch_data. ('id -> Yojson.Safe.t) ->
('case -> Yojson.Safe.t) ->
('branch_data -> Yojson.Safe.t) ->
('id, 'case, 'branch_data) next ->
Yojson.Safe.t
val next_of_yojson :
'id 'case 'branch_data. (Yojson.Safe.t ->
'id Ppx_deriving_yojson_runtime.error_or) ->
(Yojson.Safe.t -> 'case Ppx_deriving_yojson_runtime.error_or) ->
(Yojson.Safe.t -> 'branch_data Ppx_deriving_yojson_runtime.error_or) ->
Yojson.Safe.t ->
('id, 'case, 'branch_data) next Ppx_deriving_yojson_runtime.error_or
val node_to_yojson :
'id 'case 'data 'bdata. ('id -> Yojson.Safe.t) ->
('case -> Yojson.Safe.t) ->
('data -> Yojson.Safe.t) ->
('bdata -> Yojson.Safe.t) ->
('id, 'case, 'data, 'bdata) node ->
Yojson.Safe.t
val node_of_yojson :
'id 'case 'data 'bdata. (Yojson.Safe.t ->
'id Ppx_deriving_yojson_runtime.error_or) ->
(Yojson.Safe.t -> 'case Ppx_deriving_yojson_runtime.error_or) ->
(Yojson.Safe.t -> 'data Ppx_deriving_yojson_runtime.error_or) ->
(Yojson.Safe.t -> 'bdata Ppx_deriving_yojson_runtime.error_or) ->
Yojson.Safe.t ->
('id, 'case, 'data, 'bdata) node Ppx_deriving_yojson_runtime.error_or
type ('id, 'case, 'cmd_data, 'branch_data) entry =
| Node of ('id, 'case, 'cmd_data, 'branch_data) node
| Alias of 'id
val entry_to_yojson :
'id 'case 'cmd_data 'branch_data. ('id -> Yojson.Safe.t) ->
('case -> Yojson.Safe.t) ->
('cmd_data -> Yojson.Safe.t) ->
('branch_data -> Yojson.Safe.t) ->
('id, 'case, 'cmd_data, 'branch_data) entry ->
Yojson.Safe.t
val entry_of_yojson :
'id 'case 'cmd_data 'branch_data. (Yojson.Safe.t ->
'id Ppx_deriving_yojson_runtime.error_or) ->
(Yojson.Safe.t -> 'case Ppx_deriving_yojson_runtime.error_or) ->
(Yojson.Safe.t -> 'cmd_data Ppx_deriving_yojson_runtime.error_or) ->
(Yojson.Safe.t -> 'branch_data Ppx_deriving_yojson_runtime.error_or) ->
Yojson.Safe.t ->
('id, 'case, 'cmd_data, 'branch_data) entry
Ppx_deriving_yojson_runtime.error_or
type ('id, 'branch_case, 'cmd_data, 'branch_data) map = {
mutable root : 'id option;
entries : ('id, ('id, 'branch_case, 'cmd_data, 'branch_data) entry)
Utils.Prelude.Hashtbl.t;
}
val map_to_yojson :
'id 'branch_case 'cmd_data 'branch_data. ('id -> Yojson.Safe.t) ->
('branch_case -> Yojson.Safe.t) ->
('cmd_data -> Yojson.Safe.t) ->
('branch_data -> Yojson.Safe.t) ->
('id, 'branch_case, 'cmd_data, 'branch_data) map ->
Yojson.Safe.t
val map_of_yojson :
'id 'branch_case 'cmd_data 'branch_data. (Yojson.Safe.t ->
'id
Ppx_deriving_yojson_runtime.error_or) ->
(Yojson.Safe.t -> 'branch_case Ppx_deriving_yojson_runtime.error_or) ->
(Yojson.Safe.t -> 'cmd_data Ppx_deriving_yojson_runtime.error_or) ->
(Yojson.Safe.t -> 'branch_data Ppx_deriving_yojson_runtime.error_or) ->
Yojson.Safe.t ->
('id, 'branch_case, 'cmd_data, 'branch_data) map
Ppx_deriving_yojson_runtime.error_or
A command in an exec map
type matching = {
id : Gillian.Logging.Report_id.t;
kind : Engine.Matcher.match_kind;
result : Match_map.match_result;
}
Data about a matching
val matching_to_yojson : matching -> Yojson.Safe.t
val matching_of_yojson :
Yojson.Safe.t ->
matching Ppx_deriving_yojson_runtime.error_or
val submap_to_yojson : 't. ('t -> Yojson.Safe.t) -> 't submap -> Yojson.Safe.t
val submap_of_yojson :
't. (Yojson.Safe.t -> 't Ppx_deriving_yojson_runtime.error_or) ->
Yojson.Safe.t ->
't submap Ppx_deriving_yojson_runtime.error_or
val _ :
(Yojson.Safe.t -> 'a Ppx_deriving_yojson_runtime.error_or) ->
Yojson.Safe.t ->
'a submap Ppx_deriving_yojson_runtime.error_or
val make : unit -> ('a, 'b, 'c, 'd) map
Traverse the map depth-first, giving the path to the first node that matches the given predicate (or None
otherwise)
Exception-raising equivalent to find_path
Gets the node at the given path
Exception-raising equivalent to at_path
module Packaged : sig ... end
An Exec_map to be passed to the debugger frontend and displayed