I am working on a reverse engineering project where I am asked to perform backward slicing on assembly code. for a given assembly code register in a given assembly code function, I would like to detect all instructions inside the assembly function that perform an operation that updates that register. Long story short I represent the operations of these instructions as z3 expressions for example

sub r2 r2 10
add r1 r2 3 

register r1 is represented as (bvadd #x0000000d r2)). however for the case of an ldr instruction like so

ldr r2,[r2, #13]
add r1 r2 3

I want to represent memory as a map that has z3 expressions as keys and values so the ldr instruction should be a z3 expression of the form (z3_ctx.select(mem, i)) only now I want a map not an array in z3

so my question is how can I construct a map in z3 whose keys and values are z3 expressions as I want to represent the load operations from this map as z3 expressions similar to (z3_ctx.select(mem, i)) in case of a z3 array only now the i itself is a z3 expression (bvadd #x0000000d r2)

CodePudding user response：

An SMTLib array from bit-vectors to bit-vectors would work for this just fine. From an API perspective, there's no difference between a map and an array in SMT-solving: You address it using bit-vectors, just like what you wanted to do.

Your message suggests that you're worried you will not be able to "address" the array using a z3 expression? This isn't true. An array from bit-vectors to bit-vectors can be addressed with arbitrary z3 expressions of the right bit-vector type.

If you tried the above an ran into issues, post the code that gave you errors. Otherwise, it should work just fine. (Having said that, this doesn't mean it'll be "performant." Memories are typically soft-spots for solvers from a performance perspective; but that's a whole another topic.)