package bap-core-theory

  1. Overview
  2. Docs

Module Effect.Sort

Effect sorts.

The sort of an effect holds static information that is common to all effects of that sort.

We distinguish two kinds of effects - ctrl effects that affect which instructions will be executed next and data effects that affect only the values in the computer storage.

The unit effect represents an effect that is a mixture of ctrl and data effects.

type +'a t = 'a sort
type data = private
  1. | Data
type ctrl = private
  1. | Ctrl
val data : string -> data t

data kind defines a data effect of the kind.

val ctrl : string -> ctrl t

ctrl kind defines a ctrl effect of the kind.

val top : unit t

top is a set of all possible effects.

This sort indicates that the statement can have any effect.

val bot : 'a t

bot is an empty set of effects.

This sort indicates that the statement doesn't have any observable effects, thus it could be coerced to any other sort.

val both : 'a t -> 'a t -> 'a t

both s1 s2 an effect of both s1 and s2

val (&&) : 'a t -> 'a t -> 'a t

s1 && s2 is both s1 s2.

val union : 'a t list -> 'a t

union [s1;...;sN] is [s1 && ... && sN].

val join : 'a t list -> 'b t list -> unit t

join xs ys is union [union xs; union ys ].

val order : 'a t -> 'b t -> KB.Order.partial

order xs ys orders effects by the order of inclusion.

xs is before ys if ys includes all effects of xs, otherwise.

val rreg : data t

the register read effect.

val wreg : data t

the register write effect.

val rmem : data t

the memory read effect.

val wmem : data t

is the memory write effect.

val barr : data t

the memory barrier effect

val fall : ctrl t

the normal control flow effect

val jump : ctrl t

the jump effect.

val cjmp : ctrl t

the conditional branching effect