module type Cfg =sig
..end
module S:Wp.Sigs.Sigma
The memory model used.
module Node:sig
..end
Program point along a trace.
typenode =
Node.t
val node : unit -> node
fresh node
Can be created once with fresh environment, and used several times on different memory states.
module C:sig
..end
Relocatable condition
module P:sig
..end
Relocatable predicate
module T:sig
..end
Relocatable term
module E:sig
..end
Relocatable effect (a predicate that depend on two states).
type
cfg
Structured collection of traces.
val dump_env : name:string -> cfg -> unit
val output_dot : Stdlib.out_channel ->
?checks:P.t Bag.t -> cfg -> unit
val nop : cfg
Structurally, nop
is an empty execution trace.
Hence, nop
actually denotes all possible execution traces.
This is the neutral element of concat
.
Formally: all interpretations I verify nop: | nop |
_I
val add_tmpnode : node -> cfg
Set a node as temporary. Information about its path predicate or sigma can be discarded during compilation
val concat : cfg -> cfg -> cfg
The concatenation is the intersection of all possible collection of traces from each cfg.
concat
is associative, commutative,
has nop
as neutral element.
Formally: | concat g1 g2 |
_I iff | g1 |
_I and | g2 |
_I
val meta : ?stmt:Cil_types.stmt ->
?descr:string -> node -> cfg
Attach meta informations to a node.
Formally, it is equivalent to nop
.
val goto : node -> node -> cfg
Represents all execution traces T
such that, if T
contains node a
,
T
also contains node b
and memory states at a
and b
are equal.
Formally: | goto a b |
_I iff (I(a) iff I(b))
val branch : node ->
C.t ->
node -> node -> cfg
Structurally corresponds to an if-then-else control-flow.
The predicate P
shall reads only memory state at label Here
.
Formally: | branch n P a b |
_I iff ( (I(n) iff (I(a) \/ I(b)))
/\ (I(n) implies (if P(I(n)) then I(a) else I(b))) )
val guard : node ->
C.t -> node -> cfg
Structurally corresponds to an assume control-flow.
The predicate P
shall reads only memory state at label Here
.
Formally: | guard n P a |
_I iff ( (I(n) iff I(a))
/\ (I(n) implies | P |
_I ) )
val guard' : node ->
C.t -> node -> cfg
Same than guard but the condition is negated
val either : node ->
node list -> cfg
Structurally corresponds to an arbitrary choice among the different possible executions.
either
is associative and commutative. either a []
is
very special, since it denotes a cfg with no trace. Technically,
it is equivalent to attaching an assert \false
annotation to node a
.
Formally: | either n [a_1;...;a_n] } |
_I iff ( I(n) iff (I(a_1) \/ ... I(a_n)))
val implies : node ->
(C.t * node) list ->
cfg
implies is the dual of either. Instead of being a non-deterministic choice, it takes the choices that verify its predicate.
Formally: | either n [P_1,a_1;...;P_n,a_n] } |
_I iff ( I(n) iff (I(a_1) \/ ... I(a_n))
/\ I(n) implies | P_k |
_I implies I(a_k)
val effect : node ->
E.t -> node -> cfg
Represents all execution trace T
such that, if T
contains node a
,
then T
also contains b
with the given effect on corresponding
memory states.
Formally: | effect a e b |
_I iff (( I(a) iff I(b) ) /\ | e |
_I )
val assume : P.t -> cfg
Represents execution traces T
such that, if T
contains
every node points in the label-map, then the condition holds over the
corresponding memory states. If the node-map is empty,
the condition must hold over all possible execution path.
Formally: | assume P |
_I iff | P |
_I
val havoc : node ->
effects:node Wp.Sigs.sequence ->
node -> cfg
Inserts an assigns effect between nodes a
and b
, correspondings
to all the written memory chunks accessible in execution paths delimited
by the effects
sequence of nodes.
Formally: | havoc a s b |
_I is verified if there is no path between s.pre and s.path,
otherwise if (I(a) iff I(b) and if I(a) is defined then I(a) and I(b) are equal
for all the chunks that are not in the written domain of an effect that can be found
between s.pre
to s.post
.
Note: the effects are collected in the final control-flow,
when Wp.CfgCompiler.Cfg.compile
is invoked. The portion of the sub-graph in the sequence
shall be concatenated to the cfg
before compiling-it, otherwize it would be
considered empty and havoc
would be a nop (no connection between a and b).
The compilation of cfg control-flow into path predicate is performed by allocating fresh environments with optimized variable allocation. Only the relevant path between the nodes is extracted. Other paths in the cfg are pruned out.
Extract the nodes that are between the start node and the final nodes and returns how to observe a collection of states indexed by nodes. The returned maps gives, for each reachable node, a predicate representing paths that reach the node and the memory state at this node.
Nodes absent from the map are unreachable. Whenever possible,
predicate F.ptrue
is returned for inconditionally accessible
nodes.
~name: identifier used for debugging
val compile : ?name:string ->
?mode:Wp.CfgCompiler.mode ->
node ->
Node.Set.t ->
S.domain Node.Map.t ->
cfg ->
Wp.Lang.F.pred Node.Map.t *
S.t Node.Map.t * Wp.Conditions.sequence