Install instructions updates (#171)

* Install instructions updates

* Update README.md

* also need pip

* need to update, plus compact a few things

* add -y

* grammar?

* typos

* Add bountysource link

* consistency

* Point users to the examples dir and wiki

I thought these links were cluttering things a bit, and 2 out of 3 of
them aren’t official documentation yet we’re linking to them in the
first line of the README. I updated the wiki to address these directly
in a way I think is more clear.

* link to Z3 releases

* oops, don't know where that came from

* ensure people run the latest pip

* be more explicit

* Add an Issue Template

* be more explicit

* no longer appropriate here

* unnecessary

* add note about 16.04

* move issue template to hidden folder

* Spelling

* be explicit, makes copy/paste easier

.github/ISSUE_TEMPLATE.md

@@ -0,0 +1,28 @@
+### OS / Environment
+<!--- lsb_release -a --->
+
+
+### Python version
+<!--- python --version --->
+
+
+### Dependencies
+<!--- pip freeze --->
+
+
+### Summary of the problem
+
+
+### Step to reproduce the behavior
+
+
+### Expected behavior
+
+
+### Actual behavior
+
+
+### Any relevant logs
+
+
+

README.md

@@ -2,8 +2,9 @@
 
 [![Build Status](https://travis-ci.com/trailofbits/manticore.svg?token=m4YsYkGcyttTxRXGVHMr&branch=master)](https://travis-ci.com/trailofbits/manticore)
 [![Slack Status](https://empireslacking.herokuapp.com/badge.svg)](https://empireslacking.herokuapp.com)
+[![Bountysource](https://img.shields.io/bountysource/team/trailofbits/activity.svg)](https://www.bountysource.com/teams/trailofbits)
 
-Manticore is a prototyping tool for dynamic binary analysis, with support for [symbolic execution](https://gist.github.com/ehennenfent/a5ad9746615d1490c618a88b98769c10#file-2multiple_styles_symbolic_solve-py), [taint analysis](/examples/script/introduce_symbolic_bytes.py), and [binary instrumentation](https://gist.github.com/ehennenfent/a5ad9746615d1490c618a88b98769c10#file-1multiple_styles_concrete_solve-py).
+Manticore is a prototyping tool for dynamic binary analysis, with support for symbolic execution, taint analysis, and binary instrumentation.
 
 ## Features
 
@@ -20,52 +21,67 @@ architectures. It has been primarily used on binaries compiled from C and C++.
 
 ## Requirements
 
-Manticore is supported on Linux and requires Python 2.7, pip 7.1.0, and Z3.
+Manticore is supported on Linux and requires Python 2.7, pip 7.1.0 or higher, and the [Z3 Theorem Prover](https://github.com/Z3Prover/z3/releases). Ubuntu 16.04 is strongly recommended.
 
 ## Quick Start
 
-Install and try Manticore in a few shell commands:
+Install and try Manticore in a few shell commands (see an [asciinema](https://asciinema.org/a/567nko3eh2yzit099s0nq4e8z)):
 
 ```
-# Install system dependency
+# Install system dependencies
-sudo apt-get install z3
+sudo apt-get update && sudo apt-get install z3 python-pip -y
+python -m pip install -U pip
 
-# Install manticore and python dependencies
+# Install manticore and its dependencies
-git clone https://github.com/trailofbits/manticore.git
+git clone https://github.com/trailofbits/manticore.git && cd manticore
-cd manticore
+sudo pip install --no-binary capstone .
-pip install --user --no-binary capstone .
 
-# Some example usage
+# Build the examples
 cd examples/linux
 make
+
+# Use the Manticore CLI
 manticore basic
 cat mcore_*/*1.stdin | ./basic
 cat mcore_*/*2.stdin | ./basic
-cd ../script
-python count_instructions.py ../linux/helloworld # ok if the insn count is different
-```
 
-Here's an asciinema of what it should look like: https://asciinema.org/a/567nko3eh2yzit099s0nq4e8z
+# Use the Manticore API
+cd ../script
+python count_instructions.py ../linux/helloworld
+```
 
 ## Installation
 
-Make sure that Z3 Theorem Prover is installed and available on your path. On Ubuntu, this is as simple as `sudo apt-get install z3`.
+Make sure that Z3 is installed and available on your `PATH`. On Ubuntu, this is as simple as `sudo apt-get install z3`.
-Then download the Manticore source, and `cd` to the project root.
 
-Option 1: Perform a user install.
+Option 1: Perform a user install (requires `~/.local/bin` in your `PATH`).
 
 ```
+echo "PATH=\$PATH:~/.local/bin" >> ~/.profile
+source ~/.profile
+git clone https://github.com/trailofbits/manticore.git && cd manticore
 pip install --user --no-binary capstone .
 ```
 
-Option 2: Use a [virtual environment](https://virtualenvwrapper.readthedocs.io/en/latest/).
+Option 2: Use a virtual environment (requires [virtualenvwrapper](https://virtualenvwrapper.readthedocs.io/en/latest/) or [similar](https://virtualenv.pypa.io/en/stable/)).
 
 ```
+pip install virtualenvwrapper
+echo "source /usr/local/bin/virtualenvwrapper.sh" >> ~/.profile
+source ~/.profile
+git clone https://github.com/trailofbits/manticore.git && cd manticore
 mkvirtualenv manticore
 pip install --no-binary capstone .
 ```
 
-Once installed via either method, the `manticore` CLI tool and its Python API will be available.
+Option 3: Perform a system install.
+
+```
+git clone https://github.com/trailofbits/manticore.git && cd manticore
+sudo pip install --no-binary capstone .
+```
+
+Once installed, the `manticore` CLI tool and its Python API will be available.
 
 ### For developers
 
@@ -91,8 +107,6 @@ nosetests tests/test_armv7cpu.py:Armv7CpuInstructions.test_mov_imm_min
 
 ## Usage
 
-- [Multiple Styles: The Writeup](https://gist.github.com/ehennenfent/a5ad9746615d1490c618a88b98769c10)
-
 ```
 $ manticore ./path/to/binary  # runs, and creates a mcore_* directory with analysis results
 ```
@@ -117,3 +131,5 @@ def hook(state):
 
 m.run()
 ```
+
+See the [examples](examples) directory and the [wiki](https://github.com/trailofbits/manticore/wiki) for further documentation and examples.

examples/linux/basic.c

@@ -1,5 +1,5 @@
-/* Minimal toy example with input output using libc
+/* Minimal toy example with input/output using libc
- * Symbolic values are read from stdin using standar libc calls. 
+ * Symbolic values are read from stdin using standard libc calls. 
  *    
  * Compile with :
  *   $ gcc toy002-libc.c -o toy002-libc
@@ -26,7 +26,7 @@ int main(int argc, char* argv[], char* envp[]){
     }
     else 
     {
-        printf("Message: It is smaller or equal than 0x41\n");
+        printf("Message: It is less than or equal to 0x41\n");
     }
 
 return 0;

examples/script/count_instructions.py

@@ -1,3 +1,4 @@
+#!/usr/bin/env python
 
 import sys
 from manticore import Manticore

examples/script/introduce_symbolic_bytes.py

@@ -1,3 +1,4 @@
+#!/usr/bin/env python
 
 import sys
 from manticore import Manticore, issymbolic

examples/script/lads-baby-re.py

@@ -1,3 +1,5 @@
+#!/usr/bin/env python
+
 import sys
 
 from manticore import Manticore

examples/script/run_simple.py

@@ -1,3 +1,5 @@
+#!/usr/bin/env python
+
 import sys
 from manticore import Manticore
 

examples/script/state_control.py

@@ -1,3 +1,4 @@
+#!/usr/bin/env python
 
 import sys
 from manticore import Manticore