【Python】测试Claripy操作符与LLVM IR一致性
本帖最后由 lichao 于 2025-9-10 21:30 编辑## 背景
  笔者前段时间在分析iOS系统模块时发现关键算法代码加了一些MCB表达式做BR混淆(以下展示的是模块混淆的一处作为示例)，分析过程中尝试用Angr还原，
在此过程中笔者尝试将该混淆方式还原为OLLVM逻辑并加入到笔者自己研发的SLLVM混淆器。此文正是此过程的一部分有感而发。
```asm
__text:000000018CD955E4 SUB X26, X8, #3
__text:000000018CD955E8 MOV W0, #0x18
__text:000000018CD955EC BLR X26
__text:000000018CD955F0 MOV X8, #0x385FA333FCDBE678
__text:000000018CD95600 ADD X19, X0, X8
__text:000000018CD95604 MOV X8, #0x904EC4DDC4524EA8
__text:000000018CD95614 ADD X9, X0, X8
__text:000000018CD95618 CMP X9, X8
__text:000000018CD9561C CSET W8, NE
__text:000000018CD95620 CSET W9, EQ
__text:000000018CD95624 MOV W2, #0xA4B50D3
__text:000000018CD9562C SUB W10, W2, #6
__text:000000018CD95630 MUL W10, W9, W10
__text:000000018CD95634 SUB W8, W10, W8,LSL#1
__text:000000018CD95638 ADD W21, W8, #6
__text:000000018CD9563C ORR W8, W9, #6
__text:000000018CD95640 ADRL X23, jpt_18CD95678
__text:000000018CD95648 LDRSW X8,
__text:000000018CD9564C ADRP X9, #0x18CD95000
__text:000000018CD95650 ADD X9, X9, #0x618 ; jumptable 000000018CD95678 case 0
__text:000000018CD95654 ADD X8, X8, X9
__text:000000018CD95658 ADRP X9, #off_1C3880B50@PAGE
__text:000000018CD9565C LDR X9, ; unk_1CDDBDEFB
__text:000000018CD95660 SUB X22, X9, #3
__text:000000018CD95664 MOV W27, #0xFFFF5035
__text:000000018CD95668 MOV X20, #0x385FA333FCDBE678
__text:000000018CD95678 BR X8 ; ['0x18cd9567c', '0x18cd95754']
__text:000000018CD9567C MOV X24, X0 ; jumptable 000000018CD95678 case 0
__text:000000018CD95680 MOV X8, #0x4B91BD37674B1CED
__text:000000018CD95690 STP XZR, X8, ; jumptable 000000018CD95678 case 1
__text:000000018CD95694 STR WZR,
__text:000000018CD95698 MOV W0, #0x1000
__text:000000018CD9569C BLR X26
```
  关于OLLVM的基础知识<https://www.0xaa55.com/thread-27509-1-1.html>
## 表达式混淆的研究
### 第一阶段 OLLVM/SUB
  最早出现表达式混淆的是OLLVM项目，它提供了3大混淆方式`控制流伪造(BCF)`,`控制流平坦化(FLA)`,`指令替换(SUB)`至今仍在延续和发展。
其中指令替换其实就是最早的表达式混淆，他是在IR层做指令替换，如：
`a = b + c`替换为`a = b - (-c)`
```ir
%0 = load i32* %a, align 4
%1 = load i32* %b, align 4
%2 = sub i32 0, %1
%3 = sub nsw i32 %0, %2
```
`a = b + c`替换为`r = rand (); a = b + r; a = a + c; a = a - r`
```ir
%0 = load i32* %a, align 4
%1 = load i32* %b, align 4
%2 = add i32 %0, 1107414009
%3 = add i32 %2, %1
%4 = sub nsw i32 %3, 1107414009
```
`a = b & c`替换为`a = (b ^ ~c) & b`
```ir
%0 = load i32* %a, align 4
%1 = load i32* %b, align 4
%2 = xor i32 %1, -1
%3 = xor i32 %0, %2
%4 = and i32 %3, %0
```
`a = b | c`替换为`a = (b & c) | (b ^ c)`
```ir
%0 = load i32* %a, align 4
%1 = load i32* %b, align 4
%2 = and i32 %0, %1
%3 = xor i32 %0, %1
%4 = or i32 %2, %3
```
`a= b ^ c`替换为`a = (~a & b) | (a & ~b)`
```ir
%0 = load i32* %a, align 4
%1 = load i32* %b, align 4
%2 = xor i32 %0, -1
%3 = and i32 %1, %2
%4 = xor i32 %1, -1
%5 = and i32 %0, %4
%6 = or i32 %3, %5
```
### 第二阶段 Z3/MBA
  上述OLLVM/SUB具有一定的灵活性，但是灵活性较低，而且基本上无法干扰IDA等成熟分析工具，此时Z3求解器和符号执行开始流行，加上MBA相关的数学定理以论文形式出现，因此OLLVM/SUB升级为Z3/MBA。
  什么是Z3呢？Z3是Microsoft出品的求解器，用途极广，可以处理科学问题，可以求解方程，可以分析物理受力平衡，可以求解工科线性规划问题，也可以用于计算机中的符号执行，甚至你可以用它求解数独。
  什么是MBA呢？MBA(Mixed Boolean-Arithmetic expressions)，即混合布尔操作和数学运算的表达式，以64位整数x/y举例：`x ^ y == (x + y) - 2*(x & y)`，此类恒等式理论上是无限的，且有办法用Z3无限生成此类数学公式。实际使用时也有2种用法：运算替换和常量替换，人们将表达式提前通过Z3随机生成恒等式并存储，然后应用到增强版OLLVM中。Z3/MBA大大增强了混淆的自由度，如果再经过多层嵌套，其IDA伪代码会显得非常复杂，笔者2024年刚接触OLLVM开发时，也研究过一部分，例如生成如下公式：
```
x y ~x ~y 1
x + ~x == -1 y + ~y == -1
x&y x&~y ~x&y ~x&~y
~x&~y == ~(x|y)
(~x|~y) + (x&y) == -1
(~x&y) + (x|~y) == -1
x|y x|~y ~x|y ~x|~y
~x|~y == ~(x&y)
(~x&~y) + (x|y) == -1
(~x|y) + (x&~y) == -1
x^y x^~y ~x^y
x^y == ~x^~y x^~y == ~x^y
(x^~y) + (x^y) == -1
```
可以用代码：
```python
from z3 import *
from random import randint
N = 8
c =
s = Solver()
for i in range(4): # 取4时求解速度最快
x = randint(1, 0xffffffff)
y = randint(1, 0xffffffff)
s.add(c*x + c*y + c + c*(x&y) + c*(x&~y) + c*(x|y) + c*(x|~y) + c*(x^y) == 0)
sum = Sum()
s.add(And(sum > 0, sum <= 2*N, c != 0))
expr = ["x", "y", "1", "(x&y)", "(x&~y)", "(x|y)", "(x|~y)", "(x^y)"]
for i in range(1000):
r = s.check()
if r != sat:
break
m = s.model()
fs = " + ".join(["{}*{}".format(m], expr) for j in range(N) if m].as_long() != 0])
print("{}: ".format(i+1) + fs + " == 0")
s.add(Not(And( == m] for j in range(N)])))
```
```
1: 1*x + -1*1 + -1*(x|y) + -1*(x|~y) == 0
2: 2*x + -1*y + -4*1 + 1*(x&y) + 1*(x&~y) + -2*(x|y) + -4*(x|~y) + -1*(x^y) == 0
3: 3*x + -1*y + -4*1 + -2*(x|y) + -4*(x|~y) + -1*(x^y) == 0
4: -3*x + -2*y + 1*1 + 5*(x|y) + 1*(x|~y) + -2*(x^y) == 0
5: -1*x + -2*y + 1*1 + -2*(x&y) + -2*(x&~y) + 5*(x|y) + 1*(x|~y) + -2*(x^y) == 0
6: -2*x + -2*y + 1*1 + -1*(x&y) + -1*(x&~y) + 5*(x|y) + 1*(x|~y) + -2*(x^y) == 0
7: 2*x + -2*y + -2*1 + -2*(x&y) + -2*(x&~y) + 2*(x|y) + -2*(x|~y) + -2*(x^y) == 0
8: 1*x + -2*y + -3*1 + -1*(x&y) + 2*(x|y) + -3*(x|~y) + -3*(x^y) == 0
9: 1*x + -2*y + -2*1 + -2*(x&y) + -1*(x&~y) + 3*(x|y) + -2*(x|~y) + -3*(x^y) == 0
10: -2*y + -1*1 + -2*(x&y) + -1*(x&~y) + 4*(x|y) + -1*(x|~y) + -3*(x^y) == 0
...
```
  那么如何对抗呢，其实大部分情况一大坨运算算出来的是个0或1的布尔值，可以直接忽略。另外2020年底出现一款IDA插件`https://gitlab.com/eshard/d810`，它在IDA微代码层处理，可以完美还原MBA表达式。市面上大部分MBA混淆都是此类，有的是把MBA和包括IGV(间接引用)的其他手段混合使用以增强效果，例如`https://github.com/za233/Polaris-Obfuscator`，以下是混淆效果
### 第三阶段 增强表达式
  MCB(Mixed Boolean-Comparison expressions)即混合比较和数学运算的表达式，属于增强表示式的一种，此类表达式的操作包含`比较操作`和数学运算等。笔者遇到的这个iOS系统模块便是MCB表达式，MCB表达式还原显然比MBA难多了，此模块包含如下特点：
* MCB表达式保护BR混淆(IndirectBranch,前面引用帖子里的`间接分支`)，此混淆会将B指令直接跳转改造成BR跳转表间接跳转，保护跳转表的索引和基址。
* MCB表达式保护BLR混淆(IndirectGlobalVariable)，此混淆会把BL指令调用函数地址处理成跳转表间接调用，同样保护跳转表的索引和基址。
* 每个函数中的每个BasicBlock的跳转表的索引和基址计算过程是相关的，如将上一个BasicBlock的一个中间值用作当前BasicBlock计算，这给还原带来较大难度
## “拿来主义”，将混淆思路应用到混淆器
  笔者还是觉得有必要扩展一下逆向的定义：逆向不仅包含把汇编或字节码还原为高级源码的过程，也应该包含将可见逻辑还原成高级逻辑的过程，本例就是一个。
  笔者最终还原了该混淆，且规划将Apple的混淆逻辑，应用到自己的SLLVM混淆器中，笔者在构造难度高于MCB的增强表达式，目前使用Claripy代替Z3。
* 第一步就是确定Claripy操作符和LLVM IR操作符的对应关系和验证是否完美对应，给出如下的对应关系
| Claripy | 含义 | 对应 LLVM IR |
| ---------------------------| ------------ | ------------------------------------- |
|一元 | | |
|`Not(expr)` | 逻辑非(布尔) | `xor i1 %x, true` 或 `icmp eq %x, 0` |
|`~expr`(__invert__) | 按位取反 | `xor iN %x, -1` |
|`-expr`(__neg__) | 取负(算术取反)| `sub iN 0, %x` |
|`Reverse(expr)` | 位反转 | `llvm.bitreverse` |
|二元 | | |
|`expr1 + expr2`(__add__) | 加法 | `add` |
|`expr1 - expr2`(__sub__) | 减法 | `sub` |
|`expr1 * expr2`(__mul__) | 乘法 | `mul` |
|`expr1 / expr2`(__floordiv__)| 有符号除法 | `udiv` |
|`expr1 % expr2`(__mod__) | 有符号取模 | `urem` |
|`expr1 & expr2`(__and__) | 按位与 | `and` |
|`expr1 \| expr2`(__or__) | 按位或 | `or` |
|`expr1 ^ expr2`(__xor__) | 按位异或 | `xor` |
|`LShR(expr, k)` | 逻辑右移 | `lshr` |
|`expr >> k`(__lshift__) | 算术右移 | `ashr` |
|`expr << k`(__rshift__) | 左移 | `shl` |
|`RotateLeft(expr,k)` | 左旋 | `llvm.fshl` |
|`RotateRight(expr,k)` | 右旋 | `llvm.fshr` |
|`Concat(expr1, expr2)` | 拼接 | |
|`==, !=, <, <=, >, >=` | 比较 | `icmp` |
|三元 | | |
|`If(cond, t_expr, f_expr)` | 条件选择 | `select i1 %cond, %t, %f` |
|`ITE(cond, a, b)` | 与 `If` 相同 | `select` |
|`Extract(hi, lo, expr)` | 截取bitfield | `shl+sub+lshr+and`/`sub+shl+lshr` |
验证代码：
```python
import claripy
from claripy import BVS, BVV, Solver
import ctypes
from llvmlite import ir, binding
import random
from unicorn import *
from unicorn.arm64_const import *
triple = "arm64-apple-ios12.0"
# prepare llvm
binding.initialize()
binding.initialize_all_targets()
binding.initialize_all_asmprinters()
target = binding.Target.from_triple(triple)
tm = target.create_target_machine()
# prepare unicorn
code_base, code_size = 0x1000, 0x400
emu = Uc(UC_ARCH_ARM64, UC_MODE_ARM)
emu.mem_map(code_base, code_size)
# prepare claripy
x0 = BVS("x0", 64)
x1 = BVS("x1", 64)
x2 = BVS("x2", 64)
s = Solver()
def test_1op(name):
name_dic = {
"invert": {"claripy": "__invert__", "llvm": "?", "op": '~' },
"neg": {"claripy": "__neg__", "llvm": "?", "op": '-' },
"reverse":{"claripy": "Reverse", "llvm": "?", "op": '(rev)' },
}
op = name_dic["op"]
llvm_op = name_dic["llvm"]
# get machine code from llvm
tm = target.create_target_machine()
module = ir.Module()
module.triple = triple
fty = ir.FunctionType(ir.IntType(64), )
func = ir.Function(module, fty, name=name)
block = func.append_basic_block(name="entry")
builder = ir.IRBuilder(block)
if name == "invert": # ~x == x ^ -1
ret = builder.xor(func.args, ir.Constant(ir.IntType(64), -1))
elif name == "neg": # -x = 0 - x
ret = builder.sub(ir.Constant(ir.IntType(64), 0), func.args)
elif name == "reverse":
bswap_ty = ir.FunctionType(ir.IntType(64), )
bswap = ir.Function(module, bswap_ty, name="llvm.bswap.i64")
ret = builder.call(bswap, ])
else:
ret = getattr(builder, llvm_op)(*func.args)
builder.ret(ret)
mod = binding.parse_assembly(str(module))
mod.verify()
#print(tm.emit_assembly(mod))
engine = binding.create_mcjit_compiler(mod, tm)
func_ptr = engine.get_function_address(name)
bs = ctypes.string_at(func_ptr, 32)
func_bs = bs[:bs.find(b"\xc0\x03\x5f\xd6") + 4]
# init claripy
claripy_op = name_dic["claripy"]
if hasattr(x0, claripy_op):
expr = getattr(x0, claripy_op)()
else:
expr = getattr(claripy, claripy_op)(x0)
# get result
a1 = random.randint(0, 0x7fffffffffffffff)
a2 = random.randint(0x8000000000000000, 0xffffffffffffffff)
for a in :
emu.mem_write(code_base, func_bs)
emu.reg_write(UC_ARM64_REG_X0, a)
emu.reg_write(UC_ARM64_REG_PC, code_base)
emu.emu_start(code_base, code_base + len(func_bs) - 4)
r = emu.reg_read(UC_ARM64_REG_X0)
print(f"llvm: {op}{a} = {r}")
r = s.eval(expr, 1, extra_constraints=)
print(f"claripy: {op}{a} = {r}")
def test_2op(name):
name_dic = {
"add": {"claripy": "__add__", "llvm": "add","op": '+' },
"sub": {"claripy": "__sub__", "llvm": "sub","op": '-' },
"mul": {"claripy": "__mul__", "llvm": "mul","op": '*' },
"div": {"claripy": "__floordiv__", "llvm": "udiv", "op": '/' },
"mod": {"claripy": "__mod__", "llvm": "urem", "op": '%' },
"and": {"claripy": "__and__", "llvm": "and_", "op": '&' },
"or": {"claripy": "__or__", "llvm": "or_","op": '|' },
"xor": {"claripy": "__xor__", "llvm": "xor","op": '^' },
"lsr": {"claripy": "LShR", "llvm": "lshr", "op": '>>' }, # 逻辑右移
"asr": {"claripy": "__rshift__", "llvm": "ashr", "op": '>>s' }, # 算数右移
"lsl": {"claripy": "__lshift__", "llvm": "shl","op": '<<' }, # 逻辑左移
"ror": {"claripy": "RotateRight","llvm": "?", "op": '>>>' },
"rol": {"claripy": "RotateLeft", "llvm": "?", "op": '<<<' },
}
op = name_dic["op"]
llvm_op = name_dic["llvm"]
# get machine code from llvm
tm = target.create_target_machine()
module = ir.Module()
module.triple = triple
fty = ir.FunctionType(ir.IntType(64), )
func = ir.Function(module, fty, name=name)
block = func.append_basic_block(name="entry")
builder = ir.IRBuilder(block)
if name == "ror":
bswap_ty = ir.FunctionType(ir.IntType(64), )
bswap = ir.Function(module, bswap_ty, name="llvm.fshr.i64")
ret = builder.call(bswap, , func.args, func.args])
elif name == "rol":
bswap_ty = ir.FunctionType(ir.IntType(64), )
bswap = ir.Function(module, bswap_ty, name="llvm.fshl.i64")
ret = builder.call(bswap, , func.args, func.args])
else:
ret = getattr(builder, llvm_op)(*func.args)
builder.ret(ret)
mod = binding.parse_assembly(str(module))
mod.verify()
#print(tm.emit_assembly(mod))
engine = binding.create_mcjit_compiler(mod, tm)
func_ptr = engine.get_function_address(name)
bs = ctypes.string_at(func_ptr, 32)
func_bs = bs[:bs.find(b"\xc0\x03\x5f\xd6") + 4]
# init claripy
claripy_op = name_dic["claripy"]
if hasattr(x0, claripy_op):
expr = getattr(x0, claripy_op)(x1)
else:
expr = getattr(claripy, claripy_op)(x0, x1)
# get result
a1 = random.randint(0, 0x7fffffffffffffff)
a2 = random.randint(0x8000000000000000, 0xffffffffffffffff)
b1 = random.randint(0, 0x7fffffff)
b2 = random.randint(0x80000000, 0xffffffff)
if name in ["lsr", "asr", "lsl", "ror", "rol"]:
b1 = random.randint(1, 63)
b2 = random.randint(1, 63)
for a, b in [(a1, b1), (a1, b2), (a2, b1), (a2, b2)]:
emu.mem_write(code_base, func_bs)
emu.reg_write(UC_ARM64_REG_X0, a)
emu.reg_write(UC_ARM64_REG_X1, b)
emu.reg_write(UC_ARM64_REG_PC, code_base)
emu.emu_start(code_base, code_base + len(func_bs) - 4)
r = emu.reg_read(UC_ARM64_REG_X0)
print(f"llvm: {a} {op} {b} = {r}")
r = s.eval(expr, 1, extra_constraints=)
print(f"claripy: {a} {op} {b} = {r}")
def test_3op(name):
name_dic = {
"extract":{"claripy": "?", "llvm": "?", "op": 'extract' },
}
op = name_dic["op"]
llvm_op = name_dic["llvm"]
# get machine code from llvm
tm = target.create_target_machine()
module = ir.Module()
module.triple = triple
fty = ir.FunctionType(ir.IntType(64), )
func = ir.Function(module, fty, name=name)
block = func.append_basic_block(name="entry")
builder = ir.IRBuilder(block)
if name == "extract":
x, lsb, width = func.args
# func1
one = ir.Constant(ir.IntType(64), 1)
mask = builder.sub(builder.shl(one, width), one)
shifted = builder.lshr(x, lsb)
ret = builder.and_(shifted, mask)
# func2
#c_64 = ir.Constant(ir.IntType(64), 64)
#rshift_nbit = builder.sub(c_64, width)
#lshifted = builder.shl(x, builder.sub(rshift_nbit, lsb)) # x << (64 - width - lsb)
#ret = builder.lshr(lshifted, rshift_nbit) # x >> (64 - width)
else:
raise Exception("unimplemented")
builder.ret(ret)
mod = binding.parse_assembly(str(module))
mod.verify()
#print(tm.emit_assembly(mod))
engine = binding.create_mcjit_compiler(mod, tm)
func_ptr = engine.get_function_address(name)
bs = ctypes.string_at(func_ptr, 32)
func_bs = bs[:bs.find(b"\xc0\x03\x5f\xd6") + 4]
# init claripy
a1 = random.randint(0x8fffffffffffffff, 0xffffffffffffffff)
b1 = random.randint(0, 64 - 1) # lsb
c1 = random.randint(1, 64 - b1) # width
if name == "extract":
expr1 = claripy.Extract(b1 + c1 - 1, b1, x0)
expr = claripy.ZeroExt(64 - c1, expr1)
else:
raise Exception("unimplemented")
# get result
for a, b, c in [(a1, b1, c1)]:
emu.mem_write(code_base, func_bs)
emu.reg_write(UC_ARM64_REG_X0, a)
emu.reg_write(UC_ARM64_REG_X1, b)
emu.reg_write(UC_ARM64_REG_X2, c)
emu.reg_write(UC_ARM64_REG_PC, code_base)
emu.emu_start(code_base, code_base + len(func_bs) - 4)
r = emu.reg_read(UC_ARM64_REG_X0)
print(f"llvm: {op}({a}, {b}, {c}) = {r}")
r = s.eval(expr, 1, extra_constraints=)
print(f"claripy: {op}({a}, {b}, {c}) = {r}")
def test_cmp(name):
name_dic = {
"eq": {"claripy": "__eq__", "llvm": "==", "op": '=='},
"ne": {"claripy": "__ne__", "llvm": "!=", "op": '!='},
"slt":{"claripy": "SLT", "llvm": "<", "op": '<s'},
"ult":{"claripy": "ULT", "llvm": "<", "op": '<' },
"sle":{"claripy": "SLE", "llvm": "<=", "op": '<=s' },
"ule":{"claripy": "ULE", "llvm": "<=", "op": '<='},
"sgt":{"claripy": "SGT", "llvm": ">", "op": '>s'},
"ugt":{"claripy": "UGT", "llvm": ">", "op": '>' },
"sge":{"claripy": "SGE", "llvm": ">=", "op": '>=s' },
"ule":{"claripy": "ULE", "llvm": ">=", "op": '>='},
}
op = name_dic["op"]
llvm_op = name_dic["llvm"]
# get machine code from llvm
tm = target.create_target_machine()
module = ir.Module()
module.triple = triple
fty = ir.FunctionType(ir.IntType(64), )
func = ir.Function(module, fty, name=name)
block = func.append_basic_block(name="entry")
builder = ir.IRBuilder(block)
if name.startswith("S"):
cmp = builder.icmp_signed(llvm_op, func.args, func.args)
ret = builder.zext(cmp, ir.IntType(64))
else:
cmp = builder.icmp_unsigned(llvm_op, func.args, func.args)
ret = builder.zext(cmp, ir.IntType(64))
builder.ret(ret)
mod = binding.parse_assembly(str(module))
mod.verify()
#print(tm.emit_assembly(mod))
engine = binding.create_mcjit_compiler(mod, tm)
func_ptr = engine.get_function_address(name)
bs = ctypes.string_at(func_ptr, 32)
func_bs = bs[:bs.find(b"\xc0\x03\x5f\xd6") + 4]
# init claripy
claripy_op = name_dic["claripy"]
cond = getattr(x0, claripy_op)(x1)
expr = claripy.If(cond, BVV(1, 64), BVV(0, 64))
# get result
a1 = random.randint(0, 0x7fffffffffffffff)
a2 = random.randint(0x8000000000000000, 0xffffffffffffffff)
b1 = random.randint(0, 0x7fffffffffffffff)
b2 = random.randint(0x8000000000000000, 0xffffffffffffffff)
if name in ["eq", "ne"]:
b1 = a1
for a, b in [(a1, b1), (a1, b2), (a2, b1), (a2, b2)]:
emu.mem_write(code_base, func_bs)
emu.reg_write(UC_ARM64_REG_X0, a)
emu.reg_write(UC_ARM64_REG_X1, b)
emu.reg_write(UC_ARM64_REG_PC, code_base)
emu.emu_start(code_base, code_base + len(func_bs) - 4)
r = emu.reg_read(UC_ARM64_REG_X0)
print(f"llvm: {a} {op} {b} = {r}")
r = s.eval(expr, 1, extra_constraints=)
print(f"claripy: {a} {op} {b} = {r}")
#test_1op("invert")
#test_1op("neg")
#test_1op("reverse")
#test_2op("add")
#test_2op("sub")
#test_2op("mul")
#test_2op("div")
#test_2op("mod")
#test_2op("and")
#test_2op("or")
#test_2op("lsr")
#test_2op("asr")
#test_2op("lsl")
#test_2op("rol")
#test_3op("extract")
#test_cmp("eq")
#test_cmp("ne")
#test_cmp("slt")
#test_cmp("ult")
#test_cmp("sle")
#test_cmp("ule")
#test_cmp("sgt")
#test_cmp("ugt")
#test_cmp("sge")
#test_cmp("ule")
```
* 第二步，使用Claripy生成定理，并应用到SLLVM
页:
[1]