I'm currently using radare2 in order to construct a simple CFG, each block/node in that graph is composed of one or more assembly instructions, I wish to estimate the value of specific register or stack position as best as I can.
Few examples:
Example 1:
xor rax, rax
inc rax
; Given these instructions, solve(rax) => 1
Example 2:
mov rcx, 3
mov rbx, rcx
mov rax, rbx
; Given the instructions above, solve(rax) => 3
Example 3:
mov rbx, rcx
mov rax, rbx
; Given the instructions above, solve(rax) => Unknown
Example 4:
mov rdx, 1
shl rdx, 2
add rdx, 3
mov [rsp], rdx
; Given the instructions above, solve([rsp]) => 7
I'm looking for a simple Python example to start with, which either takes opcodes directly or and address and evaluates/solve for specific register/stack position.
I've already looked into some symbolic execution examples, which looks like what I need, but I'm pretty new to this so a simple working example would really help.