Module `Concrete.Bitvector_Interp`

type bitvector = Z.t

type boolean = bool

val biadd : 
  size:Units.In_bits.t ->
  flags:Flags.Biadd.t ->
  bitvector ->
  bitvector ->
  bitvector

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 ->
  bitvector ->
  bitvector ->
  bitvector

Bitvector Integer SUBtraction. See biadd for the flag meanings

val bimul : 
  size:Units.In_bits.t ->
  flags:Flags.Bimul.t ->
  bitvector ->
  bitvector ->
  bitvector

Bitvector Integer MULtiplication. See biadd for the flag meanings

val bshl : 
  size:Units.In_bits.t ->
  flags:Flags.Bshl.t ->
  bitvector ->
  bitvector ->
  bitvector

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

val bashr : size:Units.In_bits.t -> bitvector -> bitvector -> bitvector

Arithmetic shift right: fill with the most significant bit.

val blshr : size:Units.In_bits.t -> bitvector -> bitvector -> bitvector

Logical shift right: fill with 0.

val beq : size:Units.In_bits.t -> bitvector -> bitvector -> boolean

Bitvector equality

val bisle : size:Units.In_bits.t -> bitvector -> bitvector -> boolean

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 -> bitvector -> bitvector -> boolean

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 ->
  bitvector ->
  bitvector ->
  bitvector

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 ->
  bitvector ->
  bitvector

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 -> bitvector -> bitvector -> bitvector

Bitvector bitwise and

val bor : size:Units.In_bits.t -> bitvector -> bitvector -> bitvector

Bitvector bitwise or

val bxor : size:Units.In_bits.t -> bitvector -> bitvector -> bitvector

Bitvector bitwise xor

val buext : 
  size:Units.In_bits.t ->
  oldsize:Units.In_bits.t ->
  bitvector ->
  bitvector

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 ->
  bitvector ->
  bitvector

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

val bisdiv : size:Units.In_bits.t -> bitvector -> bitvector -> bitvector

Bitvector signed division (truncate towards 0)

val bismod : size:Units.In_bits.t -> bitvector -> bitvector -> bitvector

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 -> bitvector -> bitvector -> bitvector

Bitvector unsigned division (corresponds to euclidian division)

val biumod : size:Units.In_bits.t -> bitvector -> bitvector -> bitvector

Bitvector unsigned modulo (corresponds to euclidian remainder)

val bofbool : size:Units.In_bits.t -> boolean -> bitvector

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

val biconst : size:Units.In_bits.t -> Z.t -> bitvector

Bitvector constant with the given size and value.

Module Concrete.Bitvector_Interp

Module `Concrete.Bitvector_Interp`