Open liona24 opened 5 months ago
By default the concrete state is zero and there is no symbolic variable. The proper way to do is:
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)
.
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)
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:
This prints the following:
Two questions:
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?