z3 是微软开发的的高性能约束求解工具。
z3 也是 angr 和 triton 底层的约束求解器。其强大的数学求解能力在CTF解题中被广泛使用，
本文记录/摘录一些常用的z3 Python API，以期能较为充分的运用z3的强大能力。
数据类型
$1, $2 表示第1，2个参数。以此类推
数学类型
函数名 说明 例 Int 定义一个整数符号 x = Int('x')Ints 定义几个整数 符号 x, y = Ints('x y')IntVector 以$1为前缀定义，定义$2个Int x = IntVector('x', 12)IntVal 定义值为$1的一个Int，$1可以是string或整数 a = IntVal(1); b=IntVal('123')Real 定义一个实数 x = Real('x')Reals 同Ints x = Reals('x y')RealVector 同IntVector x = RealVector('x', 12)RealVal 同IntVal x = RealVal('2.718')Q 定义一个有理分数$1/$2 x = Q(5, 8)RatVal 与Q一样，定义一个有理分数$1 / $2，实际Q是调用的RatVal x = RatVal(5, 8)Bool 定义一个布尔类型 p = Bool('p')Bools 同Ints p, q, r = Bools('p q r')BoolVector 同IntVector P = BoolVector('p', 5)BoolVal 同IntVal BoolVal(True)
有限类型
函数名 说明 例 BitVec 定义一个名为$1长度为$2 bit的位向量，如BitVal(‘x’, 32)表示C语言中的int x = BitVec('x', 16)BitVecs 同Ints x, y, z = BitVecs('x y z', 16)BitVecVal 定义值为$1，长度为$2 bit的位向量 v = BitVecVal(122, 8)FPSort 按照$1 bit指数位， $2 bit有效位定义一个浮点类型，如FPSort(8, 24)表示C语言中float，FPSort(11, 53)表示C语言中double，当然z3已经内置了这几种类型：Float16(),Float32(), Float64(), float128() Single = FPSort(8, 24); Double = Float64()FP 定义一个名为$1，类型为$2 的浮点数 x = FP('x', FPSort(8, 24))FPs 同Ints x, y, z = FPs('x y z', FPSort(8, 24))FPVal 定义值为$1，类型为$2的浮点数 f = FPVal(11.11, FPSort(8, 24))String 定义一个名为$1 的字符串 a = String('a')Strings 同Ints a, b, c = Strings('a b c')StringVal 定义一个值为$1 的字符串 a = StringVal('a')
类
数学类型
Int
成员函数
函数名 返回类型 说明 例 as_long python int 把z3的Int转换成python的int IntVal(888).as_long()as_string python string 把z3的Int转换成python的string IntVal(888).as_string()
运算
函数名 返回类型 说明 例 __add__ Int 两个Int相加 Int('x') + Int('y'); Int('x') + 10__sub__ Int 两个Int相减 Int('x') - Int('y'); Int('x') - 10__mul__ Int 两个Int相乘 Int('x') * Int('y'); Int('x') * 10__div__ Int 两个Int相除 Int('x') / Int('y'); Int('x') / 10__mod__ Int 取模运算 Int('x') % Int('y'); Int('x') % 10__neg__ Int 取相反数 -Int('x')__pow__ Int 指数运算 Int('x') ** Int('y'); Int('x') ** 10__eq__ Bool 得到相等的约束 Int('a') == Int('b')__ne__ Bool 得到不等的约束 Int('a') != Int('b')__lt__ Bool 得到小于的约束 Int('a') < Int('b')__le__ Bool 得到小于等于的约束 Int('a') <= Int('b')__gt__ Bool 得到大于的约束 Int('a') > Int('b')__ge__ Bool 得到大于等于的约束 Int('a') >= Int('b')ToReal Real 转换成Real类型 ToReal(Int('x'))Int2BV BitVec 把1 转换成长2 bit的BitVec Int2BV(Int('x'), 32)
Real
成员函数
函数名 返回类型 说明 例 numerator Int 返回该数分数形式的分子 Q(3,5).numerator()numerator_as_long python int 返回该数分数形式的分子 Q(3,5).numerator()denominator Int 返回该数分数形式的分母 RealVal(12.25).denominator()denominator_as_long python int 返回该数分数形式的分母 RealVal("1/77").denominator_as_long()as_fraction python Fraction 得到该数的python Fraction对象 RealVal("1/12").as_fraction()as_decimal python string 得到该数的小数形式并保留$1位小数 RealVal("1/33").as_decimal(3)as_long python int 得到该数的python整数形式，如果该数不为整数则抛异常 同Int as_string pyhton string 同Int 同Int
运算
函数名 返回类型 说明 例 Cbrt Real 开三次方 Cbrt(Real('x'))Sqrt Real 开平方 Sqrt(Real('x'))ToInt Int 转换成Int类型 ToInt(Real('x'))
Bool
成员函数
无
运算
函数名 返回类型 说明 例 Xor Bool 异或表达式 Xor(Bool('p'), Bool('q'))Not Bool 取非表达式 Not(Bool('p'))And Bool 取与表达式 And(Bool('p'), Bool('q'), Bool('w'))Or Bool 取或表达式 Or(Bool('p'), Bool('q'), Bool('w'))Implies Bool 蕴含表达式 Implies(Bool('p'), Bool('q'))
有限类型
BitVec
成员函数
函数名 返回类型 说明 例 size python int 得到BitVec的长度 len = BitVec('x', 12).size()
运算
函数名 返回类型 说明 例 BV2Int Int $1 转换成Int，布尔值$2输入是否有符号 BV2Int(BitVec('a', 8), is_signed=True)Concat BitVec BitVec 类型参数拼接 Concat(BitVec('a', 8),BitVec('b', 8))Extract BitVec 取$3[$2: $1]得到新的 BitVec Extract(6, 2, BitVec('a', 8))RotateLeft BitVec $1 循环左移 $2位 RotateLeft(BitVec('a', 8),2)RotateRight BitVec $1 循环右移 $2位 RotateRight(BitVec('a', 8),2)RepeatBitVec BitVec 重复$2，$1 次RepeatBitVec(2, a) RepeatBitVec(2, BitVec('a', 8))SignExt BitVec 向$2前缀填充$1 位1 SignExt(8, BitVec('a', 32))ZeroExt BitVec 向$2前缀填充$1 位0 ZeroExt(8, BitVec('b', 32))
有符号与无符号运算表
运算 有符号 无符号 加法 + + 减法 – – 乘法 * * 除法 / UDiv 取模 % URem 小于等于 <= ULE 小于 < ULT 大于等于 >= UGE 大于 > UGT 右移运算 >> LShR 左移运算 << <<
FP
成员函数
函数名 返回类型 说明 例 ebits python int 得到浮点数的指数位长度 sbits python int 得到浮点数的有效位长度
运算
z3中定义了5种IEEE舍入规则:
RoundNearestTiesToEven RoundNearestTiesToAway RoundTowardPositive RoundTowardNegative RoundTowardZero Function Alias Description RoundNearestTiesToEven RNE 向偶数舍入 RoundNearestTiesToAway RNA 最近 舍入 RoundTowardPositive RTP 向+∞ 舍入 RoundTowardNegative RTN 向-∞ 舍入 RoundTowardZero RTZ 向0 舍入
C语言默认为RNE
Function Return Types Description Example fpNaN FP 返回 一个值为NaN的FP fpNaN(FPSort(8, 24))fpPlusInfinit FP 返回 一个值为+∞的FP fpPlusInfinity(FPSort(8, 24))fpMinusInfinity FP 返回 一个值为-∞的FP fpMinusInfinity(FPSort(8, 24))fpInfinity FP 返回 一个值为+∞ 或 -∞的FP fpInfinity(FPSort(8, 24), False)fpPlusZero FP 返回一个值为+0.0的FP fpPlusZero(FPSort(8, 24))fpMinusZero FP 返回 一个值为-0.0的FP fpMinusZero(FPSort(8, 24))fpZero FP 返回 一个值为+0.0 或 -0.0的FP fpZero(FPSort(8, 24), False)fpAbs FP 取绝对值 fpAbs(x)fpNeg FP 取相反数 fpAbs(Neg)fpAdd FP 按照$1舍入规则$2 + $3 fpAdd(RNE(), x, y)fpSub FP 按照$1舍入规则$2 – $3 fpSub(RNE(), x, y)fpMul FP 按照$1舍入规则$2 * $3 fpMul(RNE(), x, y)fpDiv FP 按照$1舍入规则$2 / $3 fpDiv(RNE(), x, y)fpRem FP 按照$1舍入规则$2 % $3 fpRem(RNE(), x, y)fpMin FP 返回$1与$2中最小的FP fpMin(x, y)fpMax FP 返回$1与$2最大的FP fpMax(x, y)fpFMA FP 按照$1舍入规则$2 * 3 + $4 fpFMA(RNE(), x, y, z)fpSqrt FP 按照$1 舍入规则对$1开方 fpSqrt(RNE(), x)fpRoundToIntegral Int 按照$1舍入规则对$2取整 fpRoundToIntegral(RNE(), a)fpIsNaN Bool 判断$1是否为NaN fpIsNaN(x)fpIsInf Bool 判断$1是否为Inf fpIsInf(x)fpIsZero Bool 判断$1是否为0 fpIsZero(x)fpIsNormal Bool 当fpIsNaN、fpIsInf、fpIsZero都不成立时为True fpIsNormal(x)fpIsNegative Bool 判断$1是否为负值 fpIsNegative(x)fpIsPositive Bool 判断$1是否为正值 fpIsPositive(x)fpLT Bool $1 < $2 fpLT(a,b)fpLEQ Bool $1 <= $2 fpLEQ(a,b)fpGT Bool $1 > $2 fpGT(a,b)fpGEQ Bool $1 >= $2 fpGEQ(a,b)fpEQ Bool $1 == $2 fpEQ(a,b)fpNEQ Bool $1 != $2 fpNEQ(a,b)fpBVToFP FP 按照IEEE编码把$1转换成$2类型的浮点数 fpBVToFP(BitVecVal(0x41440000, 32), Float32())fpSignedToFP FP 按照$1 舍入规则把$2转换成$3 类型 fpSignedToFP(RNE(), BitVecVal(-5, 32), Float32())fpUnsignedToFP FP 按照$1 舍入规则把$2转换成$3 类型 fpUnsignedToFP(RNE(), BitVecVal(-5, 32), Float32())fpFPToFP FP 按照$1 舍入规则把$2转换成$3 类型 fpFPToFP(RNE(), FPVal(1.0, Float32()), Float64())fpRealToFP FP 按照$1 舍入规则把$2转换成$3 类型 fpRealToFP(RNE(), RealVal(1.5), Float32())fpToIEEEBV BitVec 按照IEEE编码把$1转换成BitVec类型 fpToIEEEBV(FP('x', FPSort(8, 24)))fpToSBV BitVec 按照$1舍入规则把$2转换成有符号BitVec类型 fpToSBV(RNE(), FP('x', FPSort(8, 24)), BitVecSort(32)))fpToUBV BitVec 按照$1舍入规则把$2转换成无符号BitVec类型 fpToUBV(RNE(), FP('x', FPSort(8, 24)), BitVecSort(32)))fpToReal Real 把$1转换成Real类型 fpToReal(x)
String
成员函数
函数名 返回类型 说明 例 at String 返回第$1个位置的值 StringVal('who am i').at(2)__add__ String 拼接 String('a') + String('b')
运算
函数名 返回类型 说明 例 SubSeq String 从$2位置开始在$1中取出长度为$3的字串 SubSeq(s,0,4)PrefixOf Bool 判断$1是否是$2的前缀 PrefixOf("ab", "abc")SuffixOf Bool 判断$1是否是$2的后缀 SuffixOf("bc", "abc")Contains Bool 判断$1是否包含$2 Contains("abc", "bc")Replace String 把$1 中的第一个$2 字符替换成$3 Replace("aaa", "a", "b")IndexOf Int 从$3位置开始在$1中搜索$2，$3默认为0 IndexOf("abcabc", "bc"， 2)LastIndexOf Int 在$1中检索最后出现$2的位置 LastIndexOf("abcdc","dc")Length Int 取长度 Length(StringVal('aaa'))StrToInt Int String转Int StrToInt("1")IntToStr String Int转String IntToStr(IntVal(31))
求解
一般情况下，用Solver创建一个求解器，利用成员函数add添加约束，最后使用成员函数check进行求解，成员函数model()得到求解结果。 例如：
a, b = Reals('a b')
sol = Solver()
sol.add(a + b == 128)
sol.add(a - b == 64)
assert sol.check() == sat
rol = sol.model()
print(f"a = {rol[a]}")
print(f"b = {rol[b]}")
还有一个函数solve则是直接在参数中添加约束。
例如：
a = Int('a')
solve(a > 0, a < 2)
z3 解Base64
from z3 import *
from functools import reduce
enc = "kcGXlcG9ihRqlYy5"
maps = StringVal("3GHIJKLMNOPQRSTUb=cdefghijklmnopWXYZ/12+406789VaqrstuvwxyzABCDEF5")
sol = reduce(Concat, [Int2BV(If(i == '=', 0, IndexOf(maps, i, 0)), 6) for i in enc])
arr = reversed([chr(simplify(Extract(i + 7, i, sol)).as_long()) for i in range(0, sol.size(), 8)])
print("".join(arr))
参考
Z3: z3py Namespace Reference
Z3Py Guide
Z3求解约束器及例题 -SYJ
发表回复