kdrag.theories.bitvec

Theorems about bitvectors. These are theorems about the built in smtlib bitvector types

Module Attributes

BitVecN

Arbitrary length bitvectors.

Functions

BVNot(x)

BitVecNConst(name, N)

There is a lot of confusion possible with this construct.

BitVecNVal(x, N)

BitVecSort(N)

PopCount(x)

SelectConcat(a, addr, n[, le])

Concat out of an array.

StoreConcat(a, addr, data[, le])

Store multiple bytes into an array.

fromBV(x)

select_concat(a, addr, n[, le])

toBV(x, N)

kdrag.theories.bitvec.BVNot(x: DatatypeRef) → DatatypeRef
>>> smt.simplify(BVNot(BitVecNVal(1, 3)))
BitVecN(Concat(Unit(0), Concat(Unit(1), Unit(1))))
Parameters:

x (DatatypeRef)

Return type:

DatatypeRef

kdrag.theories.bitvec.BitVecN = BitVecN

Arbitrary length bitvectors. Least significant bit comes first (index 0). Concat is unfortunately reversed compared to bitvector convetions.

Fix via Newtype wrapper? I guess I want overloading anyway

Parameters:

args (ExprRef)

Return type:

DatatypeRef

kdrag.theories.bitvec.BitVecNConst(name: str, N: int) → DatatypeRef

There is a lot of confusion possible with this construct. Maybe it shouldn’t exist.

>>> BitVecNConst("x", 3)
BitVecN(Concat(Unit(x[0]), Concat(Unit(x[1]), Unit(x[2]))))
Parameters:

  • name (str)

  • N (int)

Return type:

DatatypeRef

kdrag.theories.bitvec.BitVecNVal(x: int, N: int) → DatatypeRef
>>> BitVecNVal(6, 3)
BitVecN(Concat(Unit(0), Concat(Unit(1), Unit(1))))
Parameters:

  • x (int)

  • N (int)

Return type:

DatatypeRef

kdrag.theories.bitvec.BitVecSort(N)
>>> BV32 = BitVecSort(32)
>>> BV32.bvadd_comm
|= ForAll([x, y], x + y == y + x)
kdrag.theories.bitvec.PopCount(x: BitVecRef) → ArithRef
>>> smt.simplify(PopCount(smt.BitVecVal(6, 3)))
2
Parameters:

x (BitVecRef)

Return type:

ArithRef

kdrag.theories.bitvec.SelectConcat(a: ArrayRef, addr: BitVecRef | int, n: int, le=True) → BitVecRef

Concat out of an array. n is number of bytes. Flag is for little endian concatenation vs big endian.

>>> x = smt.Const("x", BitVecSort(8))
>>> a = smt.Lambda([x], x)
>>> smt.simplify(SelectConcat(a, 1, 1))
1
>>> smt.simplify(SelectConcat(a, 0, 2))
256
>>> smt.simplify(SelectConcat(a, 0, 2, le=False))
1
Parameters:

  • a (ArrayRef)

  • addr (BitVecRef | int)

  • n (int)

Return type:

BitVecRef

kdrag.theories.bitvec.StoreConcat(a: ArrayRef, addr: BitVecRef | int, data: BitVecRef, le=True) → ArrayRef

Store multiple bytes into an array.

>>> a = smt.Array("a", smt.BitVecSort(8), smt.BitVecSort(8))
>>> smt.simplify(StoreConcat(a, 0, smt.BitVecVal(258, 16)))
Store(Store(a, 0, 2), 1, 1)
>>> smt.simplify(SelectConcat(StoreConcat(a, 6, smt.BitVecVal(258, 16)), 6, 2))
258
Parameters:

  • a (ArrayRef)

  • addr (BitVecRef | int)

  • data (BitVecRef)

Return type:

ArrayRef

kdrag.theories.bitvec.fromBV(x: BitVecRef) → DatatypeRef
>>> fromBV(smt.BitVecVal(6, 3))
BitVecN(Concat(Unit(0), Concat(Unit(1), Unit(1))))
Parameters:

x (BitVecRef)

Return type:

DatatypeRef

kdrag.theories.bitvec.select_concat(a: ArrayRef, addr: BitVecRef | int, n: int, le=True) → BitVecRef
>>> mem = smt.Array("mem", smt.BitVecSort(64), BV8)
>>> smt.simplify(select_concat(mem, 0, 2))
select_16_le(mem, 0)
Parameters:

  • a (ArrayRef)

  • addr (BitVecRef | int)

  • n (int)

Return type:

BitVecRef

kdrag.theories.bitvec.toBV(x: DatatypeRef, N: int) → BitVecRef
>>> smt.simplify(toBV(BitVecNVal(6, 3), 3))
6
Parameters:

  • x (DatatypeRef)

  • N (int)

Return type:

BitVecRef