Add examples (#145)

* intermediate example commit
* Added more state_explore examples (w/ new_symbolic_buffer)
* Actually comment out verbosity
* rename
* Add comment mentioning symbolicate_buffer
* Update comments
* Fix issue with limited exploration
* Clear up wording
* Update descriptions
* Remove reference to symbolicate_buffer
* Clean up state_explore.c header
* move .c to src/

examples/script/introduce_symbolic_bytes.py

@@ -0,0 +1,50 @@
+
+import sys
+from manticore import Manticore
+
+'''
+Replaces a variable that controls program flow with a symbolic buffer. This
+in turn explores all possible states under that variable's influence.
+
+Usage:
+
+ $ gcc -static -g src/state_explore.c -o state_explore # -static is optional
+ $ ADDRESS=0x$(objdump -S state_explore | grep -A 1 '((value & 0xff) != 0)' |
+         tail -n 1 | sed 's|^\s*||g' | cut -f1 -d:)
+ $ python ./introduce_symbolic_bytes.py state_explore $ADDRESS
+
+'''
+
+if __name__ == '__main__':
+    if len(sys.argv) < 3:
+        sys.stderr.write("Usage: %s [binary] [address]\n"%(sys.argv[0],))
+        sys.exit(2)
+
+    # Passing a parameter to state_explore binary disables reading the value
+    # from STDIN, and relies on us adding it manually
+    m = Manticore(sys.argv[1], ['anything'])
+
+    # Uncomment to see debug output
+    #m.verbosity = 2
+
+    # Set to the address of the instruction before the first conditional.
+    introduce_at = int(sys.argv[2], 0)
+
+    @m.hook(introduce_at)
+    def introduce_sym(state):
+        # RBP-0xC is the location of the value we're interested in:
+        #
+        #    if ((value & 0xff) != 0) {
+        #  400a08:       8b 45 f4                mov    -0xc(%rbp),%eax
+        #  400a0b:       0f b6 c0                movzbl %al,%eax
+        #  400a0e:       85 c0                   test   %eax,%eax
+        #
+
+        print "introducing symbolic value to {:x}".format(state.cpu.RBP-0xc)
+
+        val = state.new_symbolic_buffer(4)
+        state.cpu.write_bytes(state.cpu.RBP - 0xc, val)
+
+    m.run()
+
+    print 'Analysis finished. See {} for results.'.format(m.workspace)

examples/script/src/state_explore.c

@@ -1,23 +1,30 @@
 #include <stdio.h>
 
 /**
- * Example code for the state abandon example in the Manticore script corpus.
+ * Example code for the state state_control.py and introduce_symbolic_bytes.py
+ * examples.
  *
- * # Compile binary
- * $ gcc -m32 -static -g state_explore.c -o state_explore
- *
- * # Pull out the address of the branch we want to ignore
- * $ ADDRESS=0x$(objdump -S state_explore | grep -A 1 'value == 0x41' | tail -n 1 | sed 's|^\s*||g' | cut -f1 -d:)
- *
- * # Run the analysis
- * $ python state_explore.py state_explore $ADDRESS
+ *  See scripts for more information.
  */
+
+void
+fill_from_stdin(int *value)
+{
+    read(0, value, sizeof *value);
+}
+
 int
 main(int argc, char *argv[])
 {
     int value;
 
-    read(0, &value, sizeof value);
+    /**
+     * If we don't receive any arguments, read value from stdin. If we do 
+     * receive an argument, treat `value` as uninitialized.
+     */
+    if (argc < 2) {
+        fill_from_stdin(&value);
+    }
 
     if ((value & 0xff) != 0) {
         if (value >= 0x40) {

examples/script/state_control.py

@@ -0,0 +1,40 @@
+
+import sys
+from manticore import Manticore
+
+'''
+Demonstrates the ability to guide Manticore's state exploration. In this case,
+abandoning a state we're no longer interested in.
+
+Usage:
+
+ $ gcc -static -g src/state_explore.c -o state_explore # -static is optional
+ $ ADDRESS=0x$(objdump -S state_explore | grep -A 1 'value == 0x41' |
+         tail -n 1 | sed 's|^\s*||g' | cut -f1 -d:)
+ $ python ./state_control.py state_explore $ADDRESS
+
+'''
+
+if __name__ == '__main__':
+    if len(sys.argv) < 3:
+        sys.stderr.write("Usage: %s [binary] [address]\n"%(sys.argv[0],))
+        sys.exit(2)
+
+    m = Manticore(sys.argv[1])
+
+    # Uncomment to see debug output
+    #m.verbosity = 2
+
+    # Set to the address of the conditional at state_explore.c:38, which will be
+    # abandoned. If line 36 of this script is commented out, Manticore will
+    # explore all reachable states.
+    to_abandon = int(sys.argv[2], 0)
+
+    @m.hook(to_abandon)
+    def explore(state):
+        print "Abandoning state at PC: ", hex(state.cpu.PC)
+        state.abandon()
+
+    print "Adding hook to: {:x}".format(to_abandon)
+
+    m.run()

examples/script/state_explore.py

@@ -1,26 +0,0 @@
-
-import sys
-from manticore import Manticore
-
-'''
-Demonstrates guiding Manticore's state exploration. 
-'''
-
-if __name__ == '__main__':
-    if len(sys.argv) < 3:
-        sys.stderr.write("Usage: %s [binary] [address]\n"%(sys.argv[0],))
-        sys.exit(2)
-
-    m = Manticore(sys.argv[1])
-
-    # Set to the address of the conditonal checking for the first complex branch
-    to_abandon = int(sys.argv[2], 0)
-
-    @m.hook(to_abandon)
-    def explore(state):
-        print "Abandoning state at PC: ", hex(state.cpu.PC)
-        state.abandon()
-
-    print "Adding hook to: {:x}".format(to_abandon)
-
-    m.run()