How to determine if a concrete register value is known?

[liona24]

Hey.

I have experimented with the slicing code and I stumbled over this little issue. Essentially I compute some small slices and try to determine if the analysis could find a concrete register value.

This is the code I have:

from triton import *

CODE = {
        0x993: bytes.fromhex("48 89 45 58"), # mov    %rax,0x58(%rbp)
        0x997: bytes.fromhex("49 0f af c7"), # imul   %r15,%rax
        0x99b: bytes.fromhex("48 8d 78 58"), # lea    0x58(%rax),%rdi
}

ctx = TritonContext()
ctx.setArchitecture(ARCH.X86_64)
ctx.setMode(MODE.ALIGNED_MEMORY, True)
ctx.setAstRepresentationMode(AST_REPRESENTATION.PYTHON)

for pc, opcode in CODE.items():
    insn = Instruction()
    insn.setOpcode(opcode)
    insn.setAddress(pc)

    ctx.processing(insn)

expr = ctx.getSymbolicRegisters().get(REG.X86_64.RDI)
slice = ctx.sliceExpressions(expr)

for (_, v) in sorted(slice.items()):
    print(v.getDisassembly())
    if v.isRegister():
        print(ctx.getSymbolicRegisterValue(v.getOrigin()))
    print("----")

This prints the following:

0x997: imul rax, r15
0
----
0x99b: lea rdi, [rax + 0x58]
88
----

Two questions:

• Is there a proper way to determine if the symbolic value is in fact a known concrete value? It seems the library outputs zero in this case?
• Why does it think rdi is 0x58? It seems it just assumed r15 to be zero for some reason. I was under the impression that everything is symbolic unless explicitly made concrete. Can I somehow make everything symbolic?

[JonathanSalwan]

By default the concrete state is zero and there is no symbolic variable. The proper way to do is:

1. Load concrete memory
2. Init concrete state of registers
3. Symbolize what you want
4. Start processing
5. Get back symbolic expressions
6. Define constraints
7. Request solver

In your example, without concrete state, imul rax, r15 is interpreted as imul 0, 0.

If you want to assign a concrete value to rax you have to do: ctx.setConcreteRegisterValue(ctx.registers.rax, 0xdeadbeef). Then, if you want to symbolize it, you can simply do: ctx.symbolizeRegister(ctx.registers.rax).

[liona24]

Is there an easy way to make everything symbolic? Really the only question I want to answer with my analysis is whether the value can be determined from the previous few instructions and which value it would be (f.e. if there is a mov rax, 123; mov rcx, 123; add rax, rcx or something)