Added info to help with extending the tool.

construct-ssm/README.md

@@ -60,4 +60,6 @@ You can instead specify those on the command line instead, e.g.
     CC=clang CXX=clang++ make analyze
 
 # Extending the Tool
-This section provides a description of the 
+This section provides a description of the layout of the tool source and files of interest for extending it as we do not have generated documentation of the API.
+
+If you wish to change how our algorithm utilizes its non-deterministic step function, performs joining, generates invariants, etc., modify the `invgen_post` function in `Predicates/InvGen.hs`. If you wish to modify the step function itself (adding or modifying instruction handling), play around with `transform` and `nd_step` in `Predicates/Transforms.hs`. To extend or modify the basic join-semilattice for symbolic state predicates, manipulate the functions in `Predicates/Lattice.hs`; special handling and join operations for other parts of the state are found in `InvGen.hs` as well. Handling of flag-related expressions can be found in `Predicates/Flags.hs`, with the primary function being `makeFlag`; to add handling for unsupported flag expressions, first uncomment the body of `report_unsupported_flag` and remove the `(top, top)` part. To modify the memory model handling, see `insert_region` and its helpers in `Predicates/Mem.hs`. To modify the data accesses, including the operations that non-deterministically retrieve jump table addresses, see the functions in `Predicates/DataAccess.hs`; the jump table handling is done by `try_read_data_section`. Finally, the files `Z3.hs` and `Predicates/Z3.hs` provide our Z3 interface. If you wish to change how symbolic state predicates are converted to Z3, modify the function `z3mkPred` in `Predicates/Z3.hs`; enclosure problems and the like are also constructed there (`mkCheckEncProblem`, etc.). If you wish to modify how the Z3 expressions themselves are constructed, change the function `z3mkExpr` in `Z3.hs`.

construct-ssm/construct-ssm.cabal

@@ -1,5 +1,5 @@
 name:                construct-ssm
-version:             2.0.0.1
+version:             2.0.0.2
 stability:           research
 -- synopsis:
 -- description:

construct-ssm/src/Elf/ReadMachineCode.hs

@@ -1,5 +1,3 @@
--- http://udis86.sourceforge.net
-
 module Elf.ReadMachineCode where
 
 import X86.Datastructures