Add docs on symbolic input (#750)

* Change tagline

* Not sure socket support is a gotcha exactly

* initial docs

* Better docs

* Code blocks

* Links to the api docs

* Improve language

* Doc add_symbolic_file in public API

* Rm stray init

docs/api.rst

@@ -14,7 +14,7 @@ Manticore
 ---------
 
 .. autoclass:: manticore.Manticore
-   :members: add_hook, hook, run, terminate, verbosity, locked_context, linux, decree, evm
+   :members: add_hook, hook, run, terminate, verbosity, locked_context, linux, decree, evm, init
 
 State
 -----
@@ -22,6 +22,14 @@ State
 .. autoclass:: manticore.core.state.State
    :members: abandon, constrain, new_symbolic_buffer, new_symbolic_value, solve_n, solve_one, solve_buffer, symbolicate_buffer, invoke_model, generate_testcase
 
+SLinux
+------
+
+Symbolic Linux
+
+.. autoclass:: manticore.platforms.linux.SLinux
+   :members: add_symbolic_file
+
 Cpu
 ---
 

docs/gotchas.rst

@@ -35,9 +35,3 @@ Client code should use the :meth:`~manticore.Manticore.locked_context` API::
 ---------------
 
 The `random` policy, which is the manticore default, is not actually random and is instead deterministically seeded. This means that running the same analysis twice should return the same results (and get stuck in the same places).
-
-
-Symbolic Socket Support
------------------------
-
-The current implementation of the socket family of system calls is very barebones and is deemed to be experimental. All created sockets are assumed to contain 64 bytes of symbolic input.

docs/index.rst

@@ -1,13 +1,16 @@
 Welcome to Manticore's documentation!
 =====================================
 
-Manticore is a prototyping tool for dynamic binary analysis, with support for symbolic execution, taint analysis, and binary instrumentation.
+Manticore is a symbolic execution tool for analysis of binaries and smart contracts.
+
+
 
 .. toctree::
    :maxdepth: 2
    :caption: Contents:
 
    api
+   syminput
    models
    gotchas
 

docs/syminput.rst

@@ -0,0 +1,58 @@
+Symbolic Input
+==============
+
+Manticore allows you to execute programs with symbolic input, which represents a range of possible inputs. You
+can do this in a variety of manners.
+
+Wildcard byte
+-------------
+
+Throughout these various interfaces, the '+' character is defined to designate a byte
+of input as symbolic. This allows the user to make input that mixes symbolic and concrete
+bytes (e.g. known file magic bytes).::
+
+For example: "concretedata++++++++moreconcretedata++++++++++"
+
+Symbolic arguments/environment
+------------------------------
+
+To provide a symbolic argument or environment variable on the command line,
+use the wildcard byte where arguments and environment are specified.::
+
+    $ manticore ./binary +++++ +++++
+    $ manticore ./binary --env VAR1=+++++ --env VAR2=++++++
+
+For API use, use the ``argv`` and ``envp`` arguments to the :meth:`manticore.Manticore.linux` classmethod.::
+
+    Manticore.linux('./binary', ['++++++', '++++++'], dict(VAR1='+++++', VAR2='++++++'))
+
+Symbolic stdin
+--------------
+
+Manticore by default is configured with 256 bytes of symbolic stdin data, after an optional
+concrete data prefix, which can be provided with the ``concrete_start`` kwarg of
+:meth:`manticore.Manticore.linux`.
+
+Symbolic file input
+-------------------
+
+To provide symbolic input from a file, first create the files that will be opened by the
+analyzed program, and fill them with wildcard bytes where you would like symbolic data
+to be.
+
+For command line use, invoke Manticore with the ``--file`` argument.::
+
+    $ manticore ./binary --file my_symbolic_file1.txt --file my_symbolic_file2.txt
+
+For API use, use the :meth:`~manticore.platforms.linux.SLinux.add_symbolic_file` interface to customize the initial
+execution state from an :meth:`~manticore.Manticore.init` hook.::
+
+    @m.init
+    def init(initial_state):
+        initial_state.platform.add_symbolic_file('my_symbolic_file1.txt')
+
+Symbolic sockets
+----------------
+
+Manticore's socket support is experimental! Sockets are configured to contain 64 bytes of
+symbolic input.