package bap-core-theory

var v is the value of the variable v.

unk s an unknown value of sort s.

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

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

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

b0 is false aka 0 bit

b1 is true aka 1 bit

inv x inverts x.

and_ x y is a conjunction of x and y.

or_ x y is a disjunction of x and y.

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

msb x is the most significant bit of x.

lsb x is the least significant bit of x.

neg x is two-complement unary minus

not x is one-complement negation.

add x y addition modulo 2^'s

sub x y subtraction modulo 2^'s

mul x y multiplication modulo 2^'s

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.

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.

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

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.

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

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

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

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

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

sle x y binary predicate for singed less than or equal

ule x y binary predicate for unsigned less than or equal

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.

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.

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.

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

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

perform s performs a generic effect of sort s.

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

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

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

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

blk lbl data ctrl a labeled sequence of effects.

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

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