package codex

  1. Overview
  2. Docs
package codex
Legend:
Page
Library
Module
Module type
Parameter
Class
Class type
Source

Module Concrete.Bitvector_InterpSource

Sourcetype bitvector = Z.t
Sourcetype boolean = bool

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].

Sourceval 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.

Sourceval 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.

Bitvector bitwise and

Bitvector bitwise or

Bitvector bitwise xor

Sourceval 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.

Sourceval 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.

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)

Sourceval 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.

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

Bitvector constant with the given size and value.