Use claripy ops from claripy instead of solver

angr · Aug 16, 2024 · 81f0e03 · 81f0e03
1 parent fc321ff
commit 81f0e03
Show file tree

Hide file tree

Showing 4 changed files with 19 additions and 17 deletions.
diff --git a/angr_platforms/ct64/ct64_angr.py b/angr_platforms/ct64/ct64_angr.py
@@ -93,7 +93,7 @@ def state_entry(self, *args, **kwargs):
         return state
 
     def _hard_checker(self, state, addr):
-        crange = state.solver.And(addr >= 0x200, addr < 0x300)
+        crange = claripy.And(addr >= 0x200, addr < 0x300)
         if not state.solver.satisfiable(extra_constraints=(crange,)):
             return None
 
@@ -126,7 +126,7 @@ def hard_checker_wr(self, state):
 
 # output
 def hard_200_rd(state):
-    return state.solver.BVV(0, 16)
+    return claripy.BVV(0, 16)
 
 def hard_200_wr(state, v):
     state.posix.fd[1].write_data(v)

diff --git a/angr_platforms/ct64/ct64_engine.py b/angr_platforms/ct64/ct64_engine.py
@@ -81,7 +81,7 @@ def execute(self, state, successors):
 
         state.regs._ip += self.LEN
         state.memory.store(dest, value)
-        successors.add_successor(state, state.regs._ip, state.solver.true, 'Ijk_Boring')
+        successors.add_successor(state, state.regs._ip, claripy.true, 'Ijk_Boring')
 
     def value(self, state):
         raise NotImplementedError
@@ -171,7 +171,7 @@ class SR(Instruction2):
     NAME = 'SR'
 
     def value(self, state):
-        return state.solver.LShR(state.memory.load(self.rm, size=1), state.memory.load(self.mem, size=1))
+        return claripy.LShR(state.memory.load(self.rm, size=1), state.memory.load(self.mem, size=1))
 
 class SL(Instruction2):
     NAME = 'SL'
@@ -206,7 +206,7 @@ def execute(self, state, successors):
 
         jumpkind = 'Ijk_Exit' if self.NAME == 'HF' and state.solver.is_true(self.imm == successors.addr) else 'Ijk_Boring'
         successors.add_successor(yes_state, self.imm, guard, jumpkind)
-        successors.add_successor(no_state, state.solver.BVV(successors.addr + self.LEN, 16), state.solver.Not(guard), jumpkind)
+        successors.add_successor(no_state, claripy.BVV(successors.addr + self.LEN, 16), claripy.Not(guard), jumpkind)
 
     def condition(self, state):
         raise NotImplementedError
@@ -215,13 +215,13 @@ class JG(InstructionJump):
     NAME = 'JG'
 
     def condition(self, state):
-        return state.solver.UGT(state.memory.load(self.rm, size=1), state.memory.load(self.mem, size=1))
+        return claripy.UGT(state.memory.load(self.rm, size=1), state.memory.load(self.mem, size=1))
 
 class JL(InstructionJump):
     NAME = 'JL'
 
     def condition(self, state):
-        return state.solver.ULT(state.memory.load(self.rm, size=1), state.memory.load(self.mem, size=1))
+        return claripy.ULT(state.memory.load(self.rm, size=1), state.memory.load(self.mem, size=1))
 
 class JQ(InstructionJump):
     NAME = 'JQ'

diff --git a/tests/test_bpf_idea.py b/tests/test_bpf_idea.py
@@ -25,10 +25,10 @@ def test_idea_correct_flag():
     state.memory.store(proj.arch.DATA_BASE, 0x1337, endness='Iend_LE')
     # input variables
     for i in range(0, len(flag), 4):
-        state.memory.store(proj.arch.DATA_BASE + 0x10 + i, state.solver.BVV(ord(flag[i]), 8))
-        state.memory.store(proj.arch.DATA_BASE + 0x10 + i + 1, state.solver.BVV(ord(flag[i+1]), 8))
-        state.memory.store(proj.arch.DATA_BASE + 0x10 + i + 2, state.solver.BVV(ord(flag[i+2]), 8))
-        state.memory.store(proj.arch.DATA_BASE + 0x10 + i + 3, state.solver.BVV(ord(flag[i+3]), 8))
+        state.memory.store(proj.arch.DATA_BASE + 0x10 + i, claripy.BVV(ord(flag[i]), 8))
+        state.memory.store(proj.arch.DATA_BASE + 0x10 + i + 1, claripy.BVV(ord(flag[i+1]), 8))
+        state.memory.store(proj.arch.DATA_BASE + 0x10 + i + 2, claripy.BVV(ord(flag[i+2]), 8))
+        state.memory.store(proj.arch.DATA_BASE + 0x10 + i + 3, claripy.BVV(ord(flag[i+3]), 8))
 
     # Execute until it returns
     simgr.explore(find=(MAX_INSTR_ID * 8,))
@@ -54,10 +54,10 @@ def test_idea_incorrect_flag():
     state.memory.store(proj.arch.DATA_BASE, 0x1337, endness='Iend_LE')
     # input variables
     for i in range(0, len(flag), 4):
-        state.memory.store(proj.arch.DATA_BASE + 0x10 + i, state.solver.BVV(ord(flag[i]), 8))
-        state.memory.store(proj.arch.DATA_BASE + 0x10 + i + 1, state.solver.BVV(ord(flag[i+1]), 8))
-        state.memory.store(proj.arch.DATA_BASE + 0x10 + i + 2, state.solver.BVV(ord(flag[i+2]), 8))
-        state.memory.store(proj.arch.DATA_BASE + 0x10 + i + 3, state.solver.BVV(ord(flag[i+3]), 8))
+        state.memory.store(proj.arch.DATA_BASE + 0x10 + i, claripy.BVV(ord(flag[i]), 8))
+        state.memory.store(proj.arch.DATA_BASE + 0x10 + i + 1, claripy.BVV(ord(flag[i+1]), 8))
+        state.memory.store(proj.arch.DATA_BASE + 0x10 + i + 2, claripy.BVV(ord(flag[i+2]), 8))
+        state.memory.store(proj.arch.DATA_BASE + 0x10 + i + 3, claripy.BVV(ord(flag[i+3]), 8))
 
     # Execute until it returns
     simgr.explore(find=(MAX_INSTR_ID * 8,))

diff --git a/tests/test_riscv.py b/tests/test_riscv.py
@@ -1,6 +1,8 @@
 import os
 
 import angr
+import claripy
+
 from angr_platforms.risc_v import *
 
 
@@ -15,8 +17,8 @@ def test_schoolbook_multiplication():
 
     startState = proj.factory.call_state(targetAddress)
 
-    A = startState.solver.BVS("A",32)
-    B = startState.solver.BVS("B",32)
+    A = claripy.BVS("A",32)
+    B = claripy.BVS("B",32)
     startState.memory.store(startState.regs.a0, A)
     startState.memory.store(startState.regs.a1, B)