add partial solves for multiple-styles (#123)

examples/linux/binaries/concrete_solve.py

@@ -0,0 +1,35 @@
+from manticore import Manticore
+
+def fixme():
+  raise Exception("Fill in the blanks!")
+
+# Let's initialize the manticore control object
+m = Manticore('multiple-styles')
+
+# First, let's give it some fake data for the input. Anything the same size as
+# the real flag should work fine!
+m.concrete_data = "infiltrate miami!"
+
+# Now we're going to want to execute a few different hooks and share data, so
+# let's use the m.context dict to keep our solution in
+m.context['solution'] = ''
+
+# Now we want to hook that compare instruction that controls the main loop.
+# Where is it again?
+@m.hook(fixme())
+def solve(state):
+    # Our actual flag should have something to do with AL at this point, let's
+    # just read it out real quick
+    flag_byte = state.cpu.AL - fixme()
+
+    m.context['solution'] += chr(flag_byte)
+
+    # But how can we make the comparison pass? There are a couple solutions here
+    fixme()
+
+# play with these numbers!
+m.verbosity = 0
+m.workers = 1
+
+m.run()
+print m.context['solution']

examples/linux/binaries/symbolic_solve.py

@@ -0,0 +1,38 @@
+from manticore import Manticore
+
+def fixme():
+  raise Exception("Fill in the blanks!")
+
+# Let's initialize the manticore control object
+m = Manticore('multiple-styles')
+
+# Now, we can hook the success state and figure out the flag! `fixme()` here
+# should be an address we'd like to get to
+@m.hook(fixme())
+def solve(state):
+    # Where is the flag in memory? It's probably offset from the base pointer
+    # somehow
+    flag_base = state.cpu.RBP - fixme()
+
+    # We're going to build a solution later
+    solution = ''
+
+    # How big is the flag? We should be able to figure this out from traditional
+    # static analysis
+    for i in xrange(fixme()):
+        # We can get the symbolic flag out
+        symbolic_character = state.cpu.read_int(flag_base + i, 8)
+        # And now we just need to solve for it in z3. How might we do that?
+        # Perhaps `grep -r "def solve" manticore` can help our case
+        concrete_character = fixme()
+        solution += chr(concrete_character)
+
+    # And this should give us a solution, after which we're done!
+    print solution
+    m.terminate()
+
+# play with these numbers!
+m.verbosity = 0
+m.workers = 1
+
+m.run()