Module type `Sig.BINARY_FORWARD`

include BINARY_BACKWARD

type binary

include BITVECTOR_BACKWARD with type bitvector := binary

type boolean

module Arity : ARITY

val biadd : 
  size:Units.In_bits.t ->
  flags:Flags.Biadd.t ->
  (binary, binary, binary) Arity.ar2

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}$ to $2^{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).

val bisub : 
  size:Units.In_bits.t ->
  flags:Flags.Biadd.t ->
  (binary, binary, binary) Arity.ar2

Bitvector Integer SUBtraction. See biadd for the flag meanings

val bimul : 
  size:Units.In_bits.t ->
  flags:Flags.Bimul.t ->
  (binary, binary, binary) Arity.ar2

Bitvector Integer MULtiplication. See biadd for the flag meanings

val bshl : 
  size:Units.In_bits.t ->
  flags:Flags.Bshl.t ->
  (binary, binary, binary) Arity.ar2

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

val bashr : size:Units.In_bits.t -> (binary, binary, binary) Arity.ar2

Arithmetic shift right: fill with the most significant bit.

val blshr : size:Units.In_bits.t -> (binary, binary, binary) Arity.ar2

Logical shift right: fill with 0.

val beq : size:Units.In_bits.t -> (binary, binary, boolean) Arity.ar2

Bitvector equality

val bisle : size:Units.In_bits.t -> (binary, binary, boolean) Arity.ar2

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.

val biule : size:Units.In_bits.t -> (binary, binary, boolean) Arity.ar2

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

val bconcat : 
  size1:Units.In_bits.t ->
  size2:Units.In_bits.t ->
  (binary, binary, binary) Arity.ar2

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

val bextract : 
  size:Units.In_bits.t ->
  index:Units.In_bits.t ->
  oldsize:Units.In_bits.t ->
  (binary, binary) Arity.ar1

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

val band : size:Units.In_bits.t -> (binary, binary, binary) Arity.ar2

Bitvector bitwise and

val bor : size:Units.In_bits.t -> (binary, binary, binary) Arity.ar2

Bitvector bitwise or

val bxor : size:Units.In_bits.t -> (binary, binary, binary) Arity.ar2

Bitvector bitwise xor

val buext : 
  size:Units.In_bits.t ->
  oldsize:Units.In_bits.t ->
  (binary, binary) Arity.ar1

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

val bsext : 
  size:Units.In_bits.t ->
  oldsize:Units.In_bits.t ->
  (binary, binary) Arity.ar1

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

val bisdiv : size:Units.In_bits.t -> (binary, binary, binary) Arity.ar2

Bitvector signed division (truncate towards 0)

val bismod : size:Units.In_bits.t -> (binary, binary, binary) Arity.ar2

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.

val biudiv : size:Units.In_bits.t -> (binary, binary, binary) Arity.ar2

Bitvector unsigned division (corresponds to euclidian division)

val biumod : size:Units.In_bits.t -> (binary, binary, binary) Arity.ar2

Bitvector unsigned modulo (corresponds to euclidian remainder)

val bofbool : size:Units.In_bits.t -> (boolean, binary) Arity.ar1

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

val valid : size:Units.In_bits.t -> access_type -> (binary, boolean) Arity.ar1

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

val valid_ptr_arith : 
  size:Units.In_bits.t ->
  arith_type ->
  (binary, binary, boolean) Arity.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) Arity.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.

val bindex : size:Units.In_bits.t -> int -> (binary, binary, binary) Arity.ar2

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

val bchoose : size:Units.In_bits.t -> int -> (binary, binary) Arity.ar1

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

val biconst : size:Units.In_bits.t -> Z.t -> binary Arity.ar0

Binary constant with given size and value

val buninit : size:Units.In_bits.t -> binary Arity.ar0

Uninitialized binary value

Module type Sig.BINARY_FORWARD

Module type `Sig.BINARY_FORWARD`