Module Core.EffectSource

Effects are a journal of all statements executed by the domains when computing a post-condition.

They are used to merge two post-conditions that diverged due to a fork-join trajectory in the abstraction DAG.

Effects

Sourcetype effect =
  1. | Effect_empty
  2. | Effect_block of Ast.Stmt.stmt list
  3. | Effect_seq of effect list
  4. | Effect_join of effect * effect
  5. | Effect_meet of effect * effect
Sourceval pp_effect : Stdlib.Format.formatter -> effect -> unit

Print a effect

Sourceval compare_effect : effect -> effect -> int

Compare two effects

Sourceval empty_effect : effect

Empty effect

Sourceval is_empty_effect : effect -> bool

Check whether a effect is empty

Sourceval join_effect : effect -> effect -> effect

Compute the union of two effects

Sourceval meet_effect : effect -> effect -> effect

Compute the intersection of two effects

Sourceval fold_stmt_effect : ('a -> Ast.Stmt.stmt -> 'a) -> 'a -> effect -> 'a

Fold over the statements in the effect

Effect trees

Sourcetype teffect =
  1. | Teffect_empty
  2. | Teffect_node of effect * teffect * teffect

Effects are presented as binary trees. Each node of the tree is associated to a domain in the abstraction and stores the statements executed by the domain when computing a post-condition.

Note that this representation is also useful when we have an abstraction DAG (i.e. when there are shared domains) thanks to the compose (stack) operator:

A x B \___/ | C

is represented as:

o / \ x C / \ A B

Sourceval empty_teffect : teffect

Create an empty effects tree

Sourceval mk_teffect : effect -> teffect -> teffect -> teffect

mk_teffect effect left right creates an effect tree with a root containing effect and having left and right as the two sub-trees

Sourceval pp_teffect : Stdlib.Format.formatter -> teffect -> unit

Print an effects tree

Sourceval compare_teffect : teffect -> teffect -> int

Compare two effects trees

Sourceval is_empty_teffect : teffect -> bool

Check whether an effects tree is empty

Sourceval get_left_teffect : teffect -> teffect

get_left_teffect te returns the left sub-tree of te

Sourceval get_right_teffect : teffect -> teffect

get_right_teffect te returns the right sub-tree of te

Sourceval get_root_effect : teffect -> effect

get_log_stmts te returns the effect at the root node of te

Sourceval set_left_teffect : teffect -> teffect -> teffect

get_left_teffect left te sets left as the left sub-tree of te

Sourceval set_right_teffect : teffect -> teffect -> teffect

get_right_teffect right te sets right as the right sub-tree of te

Sourceval map_left_teffect : (teffect -> teffect) -> teffect -> teffect

map_left_teffect f te is equivalent to set_left_teffect (f (get_left_teffect te)) te

Sourceval map_right_teffect : (teffect -> teffect) -> teffect -> teffect

map_right_teffect f te is equivalent to set_right_teffect (f (get_right_teffect te)) te

Sourceval add_stmt_to_teffect : Ast.Stmt.stmt -> teffect -> teffect

add_stmt_to_teffect stmt teffect adds stmt to the the effects of the root no of te

Sourceval merge_teffect : (effect -> effect) -> (effect -> effect) -> (effect -> effect -> effect) -> teffect -> teffect -> teffect

merge_teffect f1 f2 f te1 te2 combines te1 and te2

Sourceval concat_teffect : old:teffect -> recent:teffect -> teffect

concat_teffect old recent puts effects in old before those in recent

Sourceval meet_teffect : teffect -> teffect -> teffect

merge_teffect te1 te2 computes the effects of two intersected post-states

Sourceval join_teffect : teffect -> teffect -> teffect

merge_teffect te1 te2 computes the effects of two joined post-states

Sourceval fold_stmt_teffect : ('a -> Ast.Stmt.stmt -> 'a) -> 'a -> teffect -> 'a

Fold over the statements in the effects tree

Generic merge

Sourcetype var_effect = {
  1. modified : Ast.Var.VarSet.t;
  2. removed : Ast.Var.VarSet.t;
}

Effect of a statement in terms of modified and removed variables

Sourceval generic_merge : add:(Ast.Var.var -> 'b -> 'a -> 'a) -> find:(Ast.Var.var -> 'a -> 'b) -> remove:(Ast.Var.var -> 'a -> 'a) -> ?custom:(Ast.Stmt.stmt -> var_effect option) -> ('a * effect) -> ('a * effect) -> 'a * 'a

Generic merge operator. generic_merge ~add ~find ~remove ~custom (a1,e1) (a2,e2) applies a generic merge of states a1 and a2:

  • It searches for modified variables in one state's effects, gets their value using find and adds them to the other state using add.
  • It searches for removed variables in one state's effects and remove them from the other state using remove. This function handles common statements (assign,assume,add,remove,fold,expand and rename). Other statements can be handled using the custom function that returns the var_effect of a given statement.
Sourceval enable_effects : unit -> unit
Sourceval disable_effects : unit -> unit
Sourceval are_effects_enabled : unit -> bool
Sourceval set_effects_state : bool -> unit
Sourceval with_effects : (unit -> 'a) -> 'a