Module Concrete.Bitvector_InterpSource

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.

Bitvector constant with the given size and value.