Module StmtSemantics.Make.Cfg

module Cfg: CfgCompiler.Cfg  with module S = Compiler.M.Sigma

module S: Sigs.Sigma

The memory model used.

module Node: sig .. end

Program point along a trace.

type node = Node.t

val node : unit -> node

fresh node

Relocatable Formulae

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 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 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).

Path-Predicates

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:CfgCompiler.mode ->
       node ->
       Node.Set.t ->
       S.domain Node.Map.t ->
       cfg ->
       Lang.F.pred Node.Map.t * S.t Node.Map.t *
       Conditions.sequence