Frama-C:
Plug-ins:
Libraries:

Frama-C API - CfgCompiler

Control Flow Graphs

The semantics of a cfg is a collection of execution traces. We introduce the notion of node which represent a program point. In case of loop unrolling of function inlining, a node generalize the notion of stmt : two distinct nodes may refer to the same instruction at different memory states.

We introduce an interpretation I as a partial mapping from nodes n:node to memory states s:M.sigma, denoted I(n). The notation I(n) seen as a predicate indicates if `n` is in the partial mapping.

Given a cfg, a node can be associated to assumptions to filter interpretation against the memory state at this point.

Effects and predicates are defined wrt some fresh memory states, and can be duplicated at different nodes, each instance being mapped to different memory states.

type mode = [
  1. | `Tree
  2. | `Bool_Backward
  3. | `Bool_Forward
]
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 Frama_c_kernel.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:Frama_c_kernel.Cil_types.stmt -> ?descr:string -> node -> cfg

Attach meta information 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 memory_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: | memory_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 -> memory_effects:node Memory.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 compile is invoked. The portion of the sub-graph in the sequence shall be concatenated to the cfg before compiling-it, otherwise 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 unconditionally accessible nodes.

~name: identifier used for debugging