Module P1.Binary_Forward

Bitvector Integer ADDition. Operaters on bitvectors of size size. The flags represent behavior on overflow:

  • nuw: no unsigned wrap: the operation is partial, i.e. fails if the sum of the two operands (interpreted as unsigned numbers) is not in the 0 to 2^{size}-1 interval.
  • nsw: no signed wrap: the operation is partial, i.e. fails if the sum of the two operands (interpreted as signed numbers) is not in the -2^{size-1} to2^{size-1} - 1 interval.
  • nusw: no unsigned plus signed wrap: the addition of the first operand (interpreted as an unsigned number) and the second one (interpreted as a signed number) fails if its value is not in the 0 to 2^{size}-1 interval. This is useful when doing pointer arithmetic (address (unsigned) + offset (signed))

Note that the simultaneous combination of different flags may be unimplemented (as it never happens in practice).

Bitvector Integer SUBtraction. See biadd for the flag meanings

Bitvector Integer MULtiplication. See biadd for the flag meanings

Bitvector SHift Left, If second argument is larger than size, bshl returns 0.

Arithmetic shift right: fill with the most significant bit.

Logical shift right: fill with 0.

Bitvector equality

Signed comparison between two bitvectors (using less-or-equal <=). Bitvectors are interpreted as integers in [-2^{size-1}..-2^{size-1}-1] using two's complement.

Unsigned comparison between two bitvectors (using less-or-equal <=). Bitvectors are interpreted as positive integers in [0..-2^{size}-1].

Bitvector concatenation: the new bitvector's size is the sum of the sizes of the arguments. The first argument becomes the most significant bits.

Extract a size of a bitvector of total size oldsize, starting at index. Should satisfy index + size <= oldsize.

Bitvector bitwise and

Bitvector bitwise or

Bitvector bitwise xor

Unsingned-extend (pad left with zero) the argument bitvector until it reaches the specified size.

Sign-extend (pad left with topbit) the argument bitvector until it reaches the specified size.

Bitvector signed division (truncate towards 0)

Bitvector signed modulo: should satisfy a = b*(bisdiv a b) + bismod a b, just like C-modulo. This means it can be negative for negative divisions.

Bitvector unsigned division (corresponds to euclidian division)

Bitvector unsigned modulo (corresponds to euclidian remainder)

Turn a boolean into a bitvector of the given size: false is 0 and true is 1.

val valid : size:Units.In_bits.t -> Operator__.Operator_sig.access_type -> (binary, boolean) Sig.Context_Arity_Forward(Context).ar1

Returns true if the access to the pointer in memory is valid.

val valid_ptr_arith : size:Units.In_bits.t -> Operator__.Operator_sig.arith_type -> (binary, binary, boolean) Sig.Context_Arity_Forward(Context).ar2

valid_ptr_arith(ptr,off) where ptr is a pointer (unsigned) and off a signed integer offset returns true if ptr + off (or ptr - off, depending on the arith_type) is in-bound.

val bshift : size:Units.In_bits.t -> offset:int -> max:int option -> (binary, binary) Sig.Context_Arity_Forward(Context).ar1

bshift ptr ~offset returns ptr + offset. If max is not None, limits further pointer arithmetics: one cannot go beyond max. Note: offset and max are in bytes, not in bits.

bindex takes an integer k and two binary values ptr and off. It returns ptr + k*off.

If s is a set, and c is a "choice" (i.e. valuation of conditions), choose an element of set according to choice.

Binary constant with given size and value

Uninitialized binary value