kdrag.theories.bitvec
Theorems about bitvectors. These are theorems about the built in smtlib bitvector types
Module Attributes
Arbitrary length bitvectors. |
Functions
|
|
|
There is a lot of confusion possible with this construct. |
|
|
|
|
|
|
|
Concat out of an array. |
|
Store multiple bytes into an array. |
|
Unpack a bitvector into lanes. |
|
|
|
|
|
|
|
- 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.UnConcat(x: BitVecRef, lane_num: int) list[BitVecRef]
Unpack a bitvector into lanes.
>>> x,y = smt.BitVecs("x y", 32) >>> kd.prove(smt.Concat(UnConcat(x, 4)) == x) |= Concat(Concat(Concat(Extract(31, 24, x), Extract(23, 16, x)), Extract(15, 8, x)), Extract(7, 0, x)) == x >>> kd.prove(UnConcat(smt.Concat(x,y), 2)[0] == x) |= Extract(63, 32, Concat(x, y)) == x
- Parameters:
x (BitVecRef)
lane_num (int)
- Return type:
list[BitVecRef]
- 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
- kdrag.theories.bitvec.vmap(f, n)
>>> x,y = smt.BitVecs("x y", 16) >>> kd.prove(vmap(lambda a: a, 2)(x) == x) |= Concat(Extract(15, 8, x), Extract(7, 0, x)) == x >>> vmap(lambda a,b: a - b, 2)(x, y) Concat(Extract(15, 8, x) - Extract(15, 8, y), Extract(7, 0, x) - Extract(7, 0, y))