Module type Theory.Minimal

The Minimal theory.

include Init
val var : 'a var -> 'a pure

var v is the value of the variable v.

val unk : 'a Value.sort -> 'a pure

unk s an unknown value of sort s.

This term explicitly denotes a term with undefined or unknown value.

val let_ : 'a var -> 'a pure -> 'b pure -> 'b pure

let_ v exp body bind the value of exp to v body.

val ite : bool -> 'a pure -> 'a pure -> 'a pure

ite c x y is x if c evaluates to b1 else y.

include Bool
val b0 : bool

b0 is false aka 0 bit

val b1 : bool

b1 is true aka 1 bit

val inv : bool -> bool

inv x inverts x.

val and_ : bool -> bool -> bool

and_ x y is a conjunction of x and y.

val or_ : bool -> bool -> bool

or_ x y is a disjunction of x and y.

include Bitv
val int : 's Bitv.t Value.sort -> word -> 's bitv

int s x is a bitvector constant x of sort s.

val msb : 's bitv -> bool

msb x is the most significant bit of x.

val lsb : 's bitv -> bool

lsb x is the least significant bit of x.

val neg : 's bitv -> 's bitv

neg x is two-complement unary minus

val not : 's bitv -> 's bitv

not x is one-complement negation.

val add : 's bitv -> 's bitv -> 's bitv

add x y addition modulo 2^'s

val sub : 's bitv -> 's bitv -> 's bitv

sub x y subtraction modulo 2^'s

val mul : 's bitv -> 's bitv -> 's bitv

mul x y multiplication modulo 2^'s

val div : 's bitv -> 's bitv -> 's bitv

div x y unsigned division modulo 2^'s truncating towards 0.

The division by zero is defined to be a vector of all ones of size 's.

val sdiv : 's bitv -> 's bitv -> 's bitv

sdiv x y is signed division of x by y modulo 2^'s,

The signed division operator is defined in terms of the div operator as follows:

                             /
                             | div x y : if not mx /\ not my
                             | neg (div (neg x) y) if mx /\ not my
                 x sdiv y = <
                             | neg (div x (neg y)) if not mx /\ my
                             | div (neg x) (neg y) if mx /\ my
                             \

              where mx = msb x, and my = msb y.
val modulo : 's bitv -> 's bitv -> 's bitv

modulo x y is the remainder of div x y modulo 2^'s.

val smodulo : 's bitv -> 's bitv -> 's bitv

smodulo x y is the signed remainder of div x y modulo 2^'s.

This version of the signed remainder where the sign follows the dividend, and is defined via the % = modulo operation as follows

                           /
                           | x % y : if not mx /\ not my
                           | neg (neg x % y) if mx /\ not my
            x smodulo y = <
                           | neg (x % (neg y)) if not mx /\ my
                           | neg (neg x % neg y) mod m if mx /\ my
                           \

            where mx = msb x  and my = msb y.
val logand : 's bitv -> 's bitv -> 's bitv

logand x y is a bitwise logical and of x and y.

val logor : 's bitv -> 's bitv -> 's bitv

logor x y is a bitwise logical or of x and y.

val logxor : 's bitv -> 's bitv -> 's bitv

logxor x y is a bitwise logical xor of x and y.

val shiftr : bool -> 's bitv -> 'b bitv -> 's bitv

shiftr s x m shifts x right by m bits filling with s.

val shiftl : bool -> 's bitv -> 'b bitv -> 's bitv

shiftl s x m shifts x left by m bits filling with s.

val sle : 'a bitv -> 'a bitv -> bool

sle x y binary predicate for singed less than or equal

val ule : 'a bitv -> 'a bitv -> bool

ule x y binary predicate for unsigned less than or equal

val cast : 'a Bitv.t Value.sort -> bool -> 'b bitv -> 'a bitv

cast s b x casts x to sort s filling with b.

If m = size s - size (sort b) > 0 then m bits b are prepended to the most significant part of the vector.

Otherwise, if m <= 0, i.e., it is a narrowing cast, then the value of b doesn't affect the result of evaluation.

val concat : 'a Bitv.t Value.sort -> 'b bitv list -> 'a bitv

concat s xs concatenates a list of vectors xs.

All vectors are concatenated from left to right (so that the most significant bits of the resulting vector are defined by the first element of the list and so on).

The result of concatenation are then casted to sort s with all extra bits (if any) set to zero.

val append : 'a Bitv.t Value.sort -> 'b bitv -> 'c bitv -> 'a bitv

append s x y appends x and y and casts to s.

Appends x and y so that in the resulting vector the vector x occupies the most significant part and y the least significant part. The resulting vector is then casted to the sort s with extra bits (if any) set to zero.

include Memory
val load : ('a, 'b) mem -> 'a bitv -> 'b bitv

load m k is the value associated with the key k in the memory m.

val store : ('a, 'b) mem -> 'a bitv -> 'b bitv -> ('a, 'b) mem

store m k x a memory m in which the key k is associated with the word x.

include Effect
val perform : 'a Effect.sort -> 'a eff

perform s performs a generic effect of sort s.

val set : 'a var -> 'a pure -> data eff

set v x changes the value stored in v to the value of x.

val jmp : _ bitv -> ctrl eff

jmp dst passes the control to a program located at dst.

val goto : label -> ctrl eff

goto lbl passes the control to a program labeled with lbl.

val seq : 'a eff -> 'a eff -> 'a eff

seq x y performs effect x, after that perform effect y.

val blk : label -> data eff -> ctrl eff -> unit eff

blk lbl data ctrl an optionally labeled sequence of effects.

If lbl is Label.null then the block is unlabeled. If it is not Label.null then the denotations will preserve the label and assume that this blk is referenced from some other blocks.

  • since 2.4.0 the [blk] operator accepts (and welcomes)

Label.null as the label in cases when the block is not really expected to be called from anywhere else.

val repeat : bool -> data eff -> data eff

repeat c data repeats data effects until the condition c holds.

val branch : bool -> 'a eff -> 'a eff -> 'a eff

branch c lhs rhs if c holds then performs lhs else rhs.