backward slicing from memory address about triton HOT 8 CLOSED

Maybe getMemoryAst can work.
eg:
mem = ctx.getMemoryAst(MemoryAccess(y_addr, 4))

from triton.

I think my main problem is that I don't have proper propagation of the expressions. I followed the example given for backward slicing, but it does not seem to create the correct expression, that when solved will produce the correct slice. Is there any way to modify how expressions propagate? And add expressions? I have made that memory access that I want (rsp+0x20) into a symbolic memory but I don't know how to make Triton create an expression out of it.

from triton.

2: 0x000084f7 c74424200500. mov dword [x], 5
3: 0x000084ff c74424240600. mov dword [y], 6
4: 0x00008507 837c242005 cmp dword [x], 5
5: 0x0000850c 7d16 jge 0x8524

When executing the line 5, can you just get the flag registers (sf, of), or maybe just rip and slice from them ?

from triton.

Slicing the rip register from the command in line 5 yields the following result.
[slicing] 0x8776: cmp dword ptr [rsp], 5
[slicing] 0x8776: cmp dword ptr [rsp], 5
[slicing] 0x8776: cmp dword ptr [rsp], 5
[slicing] 0x877a: jge 0x87c1

Where [rsp] is the location of x. Shouldn't this slice return the commands in lines 1 and 2 also?
1: sub rsp, 0xa8
2: mov dword [x], 5
Am I missing something in this logic? Should I combine the slicing of all these registers?

from triton.

Mmmh, it should also slice the line 2 but not the line 1 as we do not keep symbolic memory indexing.

from triton import *

ctx = TritonContext(ARCH.X86_64)

ctx.setConcreteRegisterValue(ctx.registers.rsp, 0x7fffffff)
ctx.setConcreteRegisterValue(ctx.registers.rdi, 0x1fffffff)

code = [
    b"\x48\x81\xec\xa8\x00\x00\x00", # sub rsp, 0xa8
    b"\xc7\x04\x24\x05\x00\x00\x00", # mov dword ptr [rsp], 5
    b"\xc7\x07\x06\x00\x00\x00", # mov dword ptr [rdi], 6
    b"\x83\x3c\x24\x05", # cmp dword ptr [rsp], 5
    b"\x0f\x8d\x1e\x85\x00\x00", # jge 0x8524
]

for op in code:
    i = Instruction(op)
    ctx.processing(i)
    for e in i.getSymbolicExpressions():
        e.setComment(i.getDisassembly())

rip = ctx.getSymbolicRegister(ctx.registers.rip)
for expr in sorted(ctx.sliceExpressions(rip).items()):
    print(expr)

$ python ./test.py
(8, (define-fun ref!8 () (_ BitVec 8) ((_ extract 31 24) (_ bv5 32))) ; mov dword ptr [rsp], 5)
(9, (define-fun ref!9 () (_ BitVec 8) ((_ extract 23 16) (_ bv5 32))) ; mov dword ptr [rsp], 5)
(10, (define-fun ref!10 () (_ BitVec 8) ((_ extract 15 8) (_ bv5 32))) ; mov dword ptr [rsp], 5)
(11, (define-fun ref!11 () (_ BitVec 8) ((_ extract 7 0) (_ bv5 32))) ; mov dword ptr [rsp], 5)
(20, (define-fun ref!20 () (_ BitVec 32) (bvsub (concat ref!8 ref!9 ref!10 ref!11) (_ bv5 32))) ; cmp dword ptr [rsp], 5)
(23, (define-fun ref!23 () (_ BitVec 1) ((_ extract 31 31) (bvand (bvxor (concat ref!8 ref!9 ref!10 ref!11) (_ bv5 32)) (bvxor (concat ref!8 ref!9 ref!10 ref!11) ref!20)))) ; cmp dword ptr [rsp], 5)
(25, (define-fun ref!25 () (_ BitVec 1) ((_ extract 31 31) ref!20)) ; cmp dword ptr [rsp], 5)
(28, (define-fun ref!28 () (_ BitVec 64) (ite (= ref!25 ref!23) (_ bv34108 64) (_ bv30 64))) ; jge 0x853c)

from triton.

Thank you. I seem to get the correct results now after I removed the line: ctx.setMode(MODE.ALIGNED_MEMORY, True). Can you also please explain why you concretized the rdi value?

from triton.

If you are talking about:

ctx.setConcreteRegisterValue(ctx.registers.rsp, 0x7fffffff)
ctx.setConcreteRegisterValue(ctx.registers.rdi, 0x1fffffff)

It's just to provide an initial context. As you have two memory accesses [rsp] and [rdi], it's just to be sure that they do not point on the same memory address.

from triton.

Ok thank you for your help, I may need some more assistance with this but I will open a different thread.

from triton.