From bd2b3be903c2ffc117eb1182597a1c67118e01e1 Mon Sep 17 00:00:00 2001 From: "Joshua A. Bockenek" Date: Sat, 5 Mar 2022 03:30:48 -0500 Subject: [PATCH] Added info to help with extending the tool. --- construct-ssm/README.md | 4 +++- construct-ssm/construct-ssm.cabal | 2 +- construct-ssm/src/Elf/ReadMachineCode.hs | 2 -- 3 files changed, 4 insertions(+), 4 deletions(-) diff --git a/construct-ssm/README.md b/construct-ssm/README.md index 8c1f5921..bdae4561 100644 --- a/construct-ssm/README.md +++ b/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`. diff --git a/construct-ssm/construct-ssm.cabal b/construct-ssm/construct-ssm.cabal index eaac189e..42830f1d 100644 --- a/construct-ssm/construct-ssm.cabal +++ b/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: diff --git a/construct-ssm/src/Elf/ReadMachineCode.hs b/construct-ssm/src/Elf/ReadMachineCode.hs index 11835b27..0e652532 100644 --- a/construct-ssm/src/Elf/ReadMachineCode.hs +++ b/construct-ssm/src/Elf/ReadMachineCode.hs @@ -1,5 +1,3 @@ --- http://udis86.sourceforge.net - module Elf.ReadMachineCode where import X86.Datastructures