Setting symbolic memory with concrete value using SYMBOLIC_STORE and SYMBOLIC_LOAD doesn't concretize the memory

[ek0]

Evening,

I was recently making use of triton::modes::SYMBOLIC_STORE, triton::modes::SYMBOLIC_LOAD with triton::modes::MEMORY_ARRAY as it seemed to be perfect when acting in arbitrary context. Except that when attempting to concretize a previously symbolized memory cell, triton fails to properly reset the isSymbolized state.

Context Configuration

// This code might not be super accurate as I extracted it from another project that wraps all that logic.
triton::Context ctx_(triton::arch::ARCH_X86_64);
ctx_.setMode(triton::modes::AST_OPTIMIZATIONS, true);
ctx_.setMode(triton::modes::CONSTANT_FOLDING, true);
ctx_.setMode(triton::modes::MEMORY_ARRAY, true);
ctx_.SetMode(triton::modes::SYMBOLIZE_LOAD, true);
ctx_.SetMode(triton::modes::SYMBOLIZE_STORE, true);

SymbolizeAllRegisters(ctx_); // Helper function, you can just symbolize the used register in this example.

auto& r = ctx_.getRegister(triton::arch::ID_REG_X86_RSP);
ctx_.setConcreteRegisterValue(r, 0x50000, false); // Arbitrary stack pointer, not relevant to be symbolic.
// Also set RIP to a concrete value
auto& rip = ctx_.getRegister(triton::arch::ID_REG_X86_RIP);
ctx_.setConcreteRegisterValue(rip, 0, false);

Issue

Emulating the following code works perfectly (with opcode in case you need to test):

48 8d 2d 34 12 00 00    lea    rbp,[rip + 0x1234]        # 0x123b
48 8d 64 24 f8          lea    rsp,[rsp - 0x8]
48 89 2c 24             mov    QWORD PTR[rsp],rbp ; Here [rsp] is not symbolized and contains the proper value.

Checking [rsp] value gives me the proper concrete 0x123b value.

However, if [rsp] was written with a symbolic variable before, overwriting said memory cell doesn't concretize the memory. Here is an example ASM snippets that shows the issue:

50                      push rax ; RAX is symbolic here. Unknown value.
48 8D 2D 0F 00 00 00    lea rbp, [rip + 0xf]
48 89 2C 24             mov [rsp], rbp

Results:

EXPECT_FALSE(emulator.IsSymbolic(triton::arch::ID_REG_X86_RBP)); // Test passes, RBP has a concrete value.
EXPECT_FALSE(emulator.IsSymbolic(triton::arch::ID_REG_X86_RSP)); // Test passes, RSP has a concrete value.
EXPECT_FALSE(emulator.IsSymbolic(insn3.operands[0].getConstMemory())); // Test fails. [rsp] is still symbolized, despite having been overwritten.

I'm not sure if this is intended, but it seems that when overwriting memory in the memory array, triton fails to properly set the state of referenced memory to concrete.

Expected Behaviour

[rsp] should have the concrete rbp value.

[ek0]

To elaborate on how the state of the memory cell is checked, here is the underlying code:

bool Emulator::IsSymbolic(const triton::arch::Register& reg) const
{
    return ctx_.isRegisterSymbolized(reg);
}

// Is the specified register symbolic
bool Emulator::IsSymbolic(const triton::arch::register_e reg) const
{
    const triton::arch::Register& r = ctx_.getRegister(reg);
    return IsSymbolic(r);
}

bool Emulator::IsSymbolic(const triton::arch::MemoryAccess& mem) const
{
    return ctx_.isMemorySymbolized(mem);
}

[JonathanSalwan]

Yes, this is because with an array logic, memory cells contain their whole historic of memory accesses.

[JonathanSalwan]

Below, an unit test that can be used to verify this behaviour.

diff --git a/src/testers/unittests/test_symbolic_array.py b/src/testers/unittests/test_symbolic_array.py
index 627da824..52d3ace3 100644
--- a/src/testers/unittests/test_symbolic_array.py
+++ b/src/testers/unittests/test_symbolic_array.py
@@ -199,3 +199,36 @@ class TestSymbolicArray(unittest.TestCase):
 
         x = self.ctx.getMemoryAst(MemoryAccess(0x1000, 4))
         self.assertEqual(x.evaluate(), 0xdeadbeef)
+
+    def test_11(self):
+        code = [
+            (1, b"\x48\xc7\xc0\x00\x10\x00\x00"),   # mov rax, 0x1000
+            (2, b"\x48\xc7\xc3\x32\x00\x00\x00"),   # mov rbx, 0x32
+            (3, b"\x89\x34\x18"),                   # mov dword ptr [rax + rbx], esi
+            (4, b"\x48\xc7\xc3\x64\x00\x00\x00"),   # mov rbx, 0x64
+            (5, b"\x8b\x0c\x18"),                   # mov ecx, dword ptr [rax + rbx]
+        ]
+
+        self.ctx.symbolizeRegister(self.ctx.registers.esi, 's_esi')
+
+        for i, op in code:
+            inst = Instruction(op)
+            self.ctx.processing(inst)
+
+        self.assertFalse(self.ctx.isRegisterSymbolized(self.ctx.registers.ecx))
+
+    def test_12(self):
+        code = [
+            (1, b"\x48\xc7\xc0\x00\x10\x00\x00"),   # mov rax, 0x1000
+            (2, b"\x48\xc7\xc3\x32\x00\x00\x00"),   # mov rbx, 0x32
+            (3, b"\x89\x34\x18"),                   # mov dword ptr [rax + rbx], esi
+            (4, b"\x8b\x0c\x18"),                   # mov ecx, dword ptr [rax + rbx]
+        ]
+
+        self.ctx.symbolizeRegister(self.ctx.registers.esi, 's_esi')
+
+        for i, op in code:
+            inst = Instruction(op)
+            self.ctx.processing(inst)
+
+        self.assertTrue(self.ctx.isRegisterSymbolized(self.ctx.registers.ecx))