Merge pull request #152 from commial/depgraph_z3

Depgraph z3

1 files changed, 22 insertions, 1 deletions

diff --git a/example/symbol_exec/depgraph.py b/example/symbol_exec/depgraph.py
index 802d4fca..5b6f373a 100644
--- a/example/symbol_exec/depgraph.py
+++ b/example/symbol_exec/depgraph.py
@@ -4,6 +4,7 @@ from pdb import pm
 from miasm2.analysis.machine import Machine
 from miasm2.analysis.binary import Container
 from miasm2.analysis.depgraph import DependencyGraph
+from miasm2.expression.expression import ExprMem, ExprId, ExprInt32
 
 parser = ArgumentParser("Dependency grapher")
 parser.add_argument("filename", help="Binary to analyse")
@@ -20,6 +21,9 @@ parser.add_argument("--unfollow-call", help="Stop on call statements",
 		    action="store_true")
 parser.add_argument("--do-not-simplify", help="Do not simplify expressions",
 		    action="store_true")
+parser.add_argument("--rename-args",
+                    help="Rename common arguments (@32[ESP_init] -> Arg1)",
+		    action="store_true")
 args = parser.parse_args()
 
 # Get architecture
@@ -41,6 +45,15 @@ for element in args.element:
 mdis = machine.dis_engine(cont.bin_stream, dont_dis_nulstart_bloc=True)
 ir_arch = machine.ira(mdis.symbol_pool)
 
+# Common argument forms
+init_ctx = {}
+if args.rename_args:
+    if arch == "x86_32":
+        # StdCall example
+        for i in xrange(4):
+            e_mem = ExprMem(ExprId("ESP_init") + ExprInt32(4 * (i + 1)), 32)
+            init_ctx[e_mem] = ExprId("arg%d" % i)
+
 # Disassemble the targeted function
 blocks = mdis.dis_multibloc(int(args.func_addr, 16))
 
@@ -71,7 +84,15 @@ for sol_nb, sol in enumerate(dg.get(current_block.label, elements, line_nb, set(
 	with open(fname, "w") as fdesc:
 		fdesc.write(sol.graph.dot())
 	result = ", ".join("%s: %s" % (k, v)
-			   for k, v in sol.emul().iteritems())
+			   for k, v in sol.emul(ctx=init_ctx).iteritems())
 	print "Solution %d: %s -> %s" % (sol_nb,
 					 result,
 					 fname)
+        if args.implicit:
+            sat = sol.is_satisfiable
+            constraints = ""
+            if sat:
+                constraints = {}
+                for element in sol.constraints:
+                    constraints[element] = hex(sol.constraints[element].as_long())
+            print "\tSatisfiability: %s %s" % (sat, constraints)