angr/claripy

How to customize simplification method?

Closed this issue · 2 comments

I'd like to customize the expression simplification method like:

I have an expression <stack_base - 0x38 - (0x17 + (concat_expr1))>, and I'd like to simplify it to the format: <stack_base - (0x4f + concat_expr1)>.

However, after z3's simplification, the expression turns to <0xffffffc8 + stack_base + 0xffffffff*(0x17 + concat_expr1)>.

If there is any way to simplify the expression as I wanted?

There is nothing in angr or claripy which will do this for you automatically. However, you have access to the internals of the ASTs and you can write an optimization pass which traverses and rewrites them based on your desired specifications.

Thanks!