package bap-core-theory

  1. Overview
  2. Docs

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

OCaml

Innovation. Community. Security.