Frama-C:
Plug-ins:
Libraries:

Frama-C API - Partition

A partition is a collection of states, each identified by a unique key. The keys define the states partition: states with identical keys are joined together, while states with different keys are maintained separate. A key contains the reason for which a state must be kept separate from others, or joined with similar states.

Partitioning actions allow updating the keys or splitting some states to define or change the partition. Actions are applied to flows, in which states with the same key are *not* automatically joined. This allows applying multiple actions before recomputing the partitions. Flows can then be converted into partitions, thus merging states with identical keys.

Flows are used to transfer states from one partition to another. Transfer functions can be applied to flows; keys are maintained through transfer functions, until partitioning actions update them.

Keys and partitions.

type branch =
  1. | Branch of int
    (*

    Junction branch id in the control flow

    *)
  2. | Builtin_result of Frama_c_kernel.Kernel_function.t * Frama_c_kernel.Cil_datatype.Kinstr.t * int
    (*

    Case of a builtin

    *)
  3. | Spec_behavior of Frama_c_kernel.Kernel_function.t * Frama_c_kernel.Cil_datatype.Kinstr.t * int
    (*

    Behavior of a spec

    *)
  4. | Disjunction_case of Frama_c_kernel.Cil_datatype.Stmt.t * int
    (*

    Case of a disjunction in an ACSL annotation

    *)
type key

Partitioning keys attached to states.

type call_return_policy = {
  1. callee_splits : bool;
  2. callee_history : bool;
  3. caller_history : bool;
  4. history_size : int;
}
module Key : sig ... end
type 'state partition

Collection of states, each identified by a unique key.

val empty : 'a partition
val is_empty : 'a partition -> bool
val size : 'a partition -> int
val to_list : 'a partition -> (key * 'a) list
val find : key -> 'a partition -> 'a
val replace : key -> 'a -> 'a partition -> 'a partition
val merge : (key -> 'a option -> 'b option -> 'c option) -> 'a partition -> 'b partition -> 'c partition
val iter : (key -> 'a -> unit) -> 'a partition -> unit
val filter : (key -> 'a -> bool) -> 'a partition -> 'a partition
val map : ('a -> 'a) -> 'a partition -> 'a partition

Partitioning actions.

type rationing

Rationing are used to keep separate the n first states propagated at a point, by creating unique stamp until the limit is reached. Implementation of the option -eva-slevel.

val new_rationing : limit:int -> merge:bool -> rationing

Creates a new rationing, that can be used successively on several flows.

type unroll_limit =
  1. | ExpLimit of Frama_c_kernel.Cil_types.exp
    (*

    Value of the expression for each incoming state. The expression must evaluate to a singleton integer in each state.

    *)
  2. | IntLimit of int
    (*

    Integer limit.

    *)
  3. | AutoUnroll of Eva_automata.loop * int * int
    (*

    AutoUnroll(loop, min, max) requests to find a "good" unrolling limit between min and max for the loop loop.

    *)

The unroll limit of a loop.

type split_kind = Eva_annotations.split_kind =
  1. | Static
  2. | Dynamic

Splits on an expression can be static or dynamic:

  • static splits are processed once: the expression is only evaluated at the split point, and the key is then kept unchanged until a merge.
  • dynamic splits are regularly redone: the expression is re-evaluated, and states are then split or merged accordingly.
type split_monitor

Split monitor: prevents splits from generating too many states.

val new_monitor : limit:int -> kind:split_kind -> term:Eva_annotations.split_term -> split_monitor

Creates a new monitor that allows to split up to limit states according to term evaluation.

type action =
  1. | Enter_loop of unroll_limit * Eva_automata.loop
    (*

    Enters a loop in which the n first iterations will be kept separate: creates an iteration counter at 0 for each states in the flow; states at different iterations will be kept separate, until reaching the unroll_limit. Counters are incremented by the Incr_loop action.

    *)
  2. | Leave_loop
    (*

    Leaves the current loop: removes its iteration counter. States that were kept separate only by this iteration counter will be joined together.

    *)
  3. | Incr_loop
    (*

    Increments the iteration counter of the current loop for all states in the flow. States with different iteration counter are kept separate.

    *)
  4. | Add_branch of int * int
    (*

    Identifies all the states in the flow as coming from the branch identified by the first integer. They will be kept separated from states coming from other branches. The second integer is the maximum number of successive branches kept in the keys: this action also removes the oldest branches from the keys to meet this constraint.

    *)
  5. | Ration of rationing
    (*

    Ensures that the first states encountered are kept separate, by creating a unique ration stamp for each new state until the limit is reached. The same rationing can be used on multiple flows. Applying a new rationing replaces the previous one. If the rationing has been created with merge:true, all the states from each flow receive the same stamp, but states from different flows receive different stamps, until limit states have been tagged.

    *)
  6. | Restrict of Eva_ast.exp * Frama_c_kernel.Z.t list
    (*

    Restrict (exp, list) restricts the rationing according to the evaluation of the expression exp: – for each integer i in list, states in which exp evaluates exactly to the singleton i receive the same unique stamp, and will thus be joined together but kept separate from other states; – all other states are joined together. Previous rationing is erased and replaced by this new stamping. Implementation of the option -eva-split-return.

    *)
  7. | Split of split_monitor
    (*

    If monitor has been built as new_monitor ~limit ~kind ~term then Split monitor tries to separate states such as the term evaluates to a singleton value in each state in the flow. If necessary and possible, splits states into multiple states. States in which the term evaluates to different values will be kept separate. Gives up the split if term evaluates to more than limit values. A same monitor can be used for successive splits on different flows.

    *)
  8. | Merge of Eva_annotations.split_term
    (*

    Forgets the split of an expression: states that were kept separate only by the split of this expression will be joined together.

    *)
  9. | Update_dynamic_splits
    (*

    Updates dynamic splits by evaluating the expression and splitting the states accordingly.

    *)

These actions redefine the partitioning by updating keys or splitting states. They are applied to all the pair (key, state) in a flow.

exception InvalidAction

Flows.

Flows are used to transfer states from one partition to another, by applying transfer functions and partitioning actions. They do not enforce the unicity of keys.