few more things

Signed-off-by: degrigis <[email protected]>

docs/docs/advanced.md

@@ -1,14 +1,17 @@
 # 🚀 Advanced Topics
 
 
+# State Plugins
 
 # Memory Model
 
+# Partial Concrete Storage
 
+# Multi-Transactions Execution
 
-# Chain Together Contracts Execution
+# Keccak256
 
+# External Calls
 
 
 
-# State Plugins

docs/docs/core.md

@@ -127,9 +127,32 @@ A state offers many API for its inspection:
 Symbolic execution is the process of progressing SimState(s) and propagating the symbolic variables according to the program's execution.
 Imagine, for instance, that the condition of a `JUMPI` contains a symbolic variable X.
 If the condition checks for `X != 0`, and the constraints over the variable X make it possible for `X != 0` and `X == 0`, greed will create two different State(s), one at the location specified by the JUMPI (adding a constraint of `X != 0` to the state), and one at the fallthrough (adding a constraint of `X == 0`).
-
+To begin symbolic execution you need to instantiate a `Simulation Manager`.
 
 ### Simulation Manager
-The simulation manager is a concept borrowed from angr. It is the starting point for beginning symbolic execution and orchestrates the progression of the SimState(s) according to the specified `Exploration Techniques`.
+The simulation manager is a concept borrowed from angr. It is the starting point for beginning symbolic execution and it is used to orchestrate the progression of the SimState(s) according to the employed `Exploration Techniques`.
+Exploration Techniques are used to specify a strategy to explore the states of the program. For instance, an exploration technique can be the classic BFS, or a DFS, or more complicated strategies such as Directed Search etc...
+
+You can instantiate a simulation manager via the Factory in this way:
+
+```python
+>>> simgr = proj.factory.simgr(entry_state=entry_state)
+```
+
+By default, the employed exploration technique will be B(reath)F(irst)S(earch). You can change this behavior by installing a new exploration technique that follows the `Exploration Technique` object interface. e.g., :
+
+```python
+>>> from greed.exploration_techniques import ExplorationTechnique, DirectedSearch
+>>> directed_search = DirectedSearch(proj.statement_at['0x1e'])
+>>> simgr.use_technique(directed_search)
+```
+
+Finally, to start the exploration:
+
+```python
+>>> simgr.run()
+```
+
+The simulation manager operates using `stashes`. A stash is a "bucket" of SimStates generated by the simulation manager during symbolic execution.
 
 ### Solver 

docs/docs/options.md

@@ -0,0 +1,22 @@
+# 🕹️ Options
+
+greed supports many option to tweak the behavior of symbolic execution.
+These global options should be activated or de-activated before creating an entry state.
+
+| Option Name | Default | Desc |
+|-------------------|----------|----------|
+| options.GREEDY_SHA  | False | calculate the result of the `KECCAK256` whenever the input buffer is fully concrete and has one solution |
+| options.LAZY_SOLVES | False | check_sat() every time a new SimState is generated |
+
+
+
+options.GREEDY_SHA = True
+options.LAZY_SOLVES = False
+options.STATE_INSPECT = False
+options.MAX_SHA_SIZE = 300
+options.OPTIMISTIC_CALL_RESULTS = True
+options.DEFAULT_EXTCODESIZE = True
+options.DEFAULT_CREATE2_RESULT_ADDRESS = True
+options.DEFAULT_CREATE_RESULT_ADDRESS = True
+options.MATH_CONCRETIZE_SYMBOLIC_EXP_EXP = True
+options.MATH_CONCRETIZE_SYMBOLIC_EXP_BASE = True