src/App.cpp

 /**
  * @file App.cpp
  * @author Tomas Susovsky <xsusov01@stud.fit.vutbr.cz>
- * @date 2018
+ * @date 2019
  *
  * @details APP class for Tindger program - main function App::run()
  */

src/App.h

 /**
  * @file App.h
  * @author Tomas Susovsky <xsusov01@stud.fit.vutbr.cz>
- * @date 2018
+ * @date 2019
  *
  * @details APP class for Tindger program:
  *  works with input data structure (@see AppParams.h) and dependencies

src/AppParams.h

 /**
  * @file AppParams.cpp
  * @author Tomas Susovsky <xsusov01@stud.fit.vutbr.cz>
- * @date 2018
+ * @date 2019
  *
  * @details Structure to hold parsed program options
  */

src/ArgParser.h

 /**
  * @file ArgParser.cpp
  * @author Tomas Susovsky <xsusov01@stud.fit.vutbr.cz>
- * @date 2018
+ * @date 2019
  *
  * @details Class for parsing CLI arguments to structure AppParams holding fomatted program options
  *          - arg parsing implemented using getopt lib

src/ConfigParser.h

 /**
  * @file ConfigParse.h
  * @author Tomas Susovsky <xsusov01@stud.fit.vutbr.cz>
- * @date 2018
+ * @date 2019
  *
  * @details Simple class for parsing control config data pased in json formatted file to structure used by App
  */

src/Diagnostic.h

 /**
  * @file Diagnostic.h
  * @author Tomas Susovsky <xsusov01@stud.fit.vutbr.cz>
- * @date 2018
+ * @date 2019
  *
  * @details Class for measuring and storing data about App run
  */
 
-
 #ifndef TINDGER_DIAGNOSTIC_H
 #define TINDGER_DIAGNOSTIC_H
 

src/ExtractionPath.h

+/**
+ * @file ExtactionPath.h
+ * @author Tomas Susovsky <xsusov01@stud.fit.vutbr.cz>
+ * @date 2019
+ *
+ * @details Structure for holding information about program path to be analysed.
+*/
+
 #ifndef TINDGER_EXTRACTIONPATHPLAN_H
 #define TINDGER_EXTRACTIONPATHPLAN_H
 

src/README.md

 llvmextractor - module handling LLVM IR input processing
+model - module for LLVM IR model analysis
+smt - module for generating SMT expressions for solving path semantics reachability
 
 App.cpp - main Application class wrapping dependencies and basic workflow of tindger program \
 App.h \

src/llvmextractor/BasicBlockLabeler.cpp

 /**
  * @file BasicBlockLabeler.cpp
  * @author Tomas Susovsky <xsusov01@stud.fit.vutbr.cz>
- * @date 2018
+ * @date 2019
  *
  * @details Class for generating llvm object names and assign them to IR model implementation.
 */

src/llvmextractor/BasicBlockLabeler.h

 /**
  * @file BasicBlockLabeler.h
  * @author Tomas Susovsky <xsusov01@stud.fit.vutbr.cz>
- * @date 2018
+ * @date 2019
  *
  * @details Class for generating llvm object names and assign them to IR model.
  *  The approach used is based on how llvm labels values internally in CFGPrinter for export to text representation.

src/llvmextractor/FunctionSelector.cpp

 /**
  * @file FunctionSelector.cpp
  * @author Tomas Susovsky <xsusov01@stud.fit.vutbr.cz>
- * @date 2018
+ * @date 2019
  *
  * @details Wrapper class for accessing internal objects of LLVM in-memory model on Function level.
  * @see ModuleSelector.h

src/llvmextractor/FunctionSelector.h

 /**
  * @file FunctionSelector.h
  * @author Tomas Susovsky <xsusov01@stud.fit.vutbr.cz>
- * @date 2018
+ * @date 2019
  *
  * @details Wrapper class for accessing internal objects of LLVM in-memory model on Function level.
  * @see ModuleSelector.h

src/llvmextractor/LLVMExtractor.cpp

 /**
  * @file LLVMExtractor.cpp
  * @author Tomas Susovsky <xsusov01@stud.fit.vutbr.cz>
- * @date 2018
+ * @date 2019
  *
  * @details LLVMExtractorInterface default implementation
  * @see LLVMExtractorInterface.h
@@ -24,7 +24,6 @@ namespace tindger {
      */
     std::unique_ptr<LLVMModuleSelectorInterface> LLVMExtractor::extractIRModule(const std::string inputFilename)
     {
-        // todo change APP api to accept already extracted string with LLVM IR CODE
         ErrorOr<std::unique_ptr<MemoryBuffer>> irFileOrError = MemoryBuffer::getFileOrSTDIN(inputFilename);
         if (irFileOrError.getError()) {
             throw LLVMExtractionException("LLVM IR file: " + inputFilename + " could not be parse. Error: " +
@@ -71,15 +70,13 @@ namespace tindger {
             for (const auto &instruction : basicBlock->getInstList()) {
                 std::vector<tindger::Value> operands{};
                 for (const auto &operand : instruction.operands()) {
-                    /* todo auto value = tindgerValueFromLLVMValue(operand.get());  */
                     // use LLVM roled dynamic cast here
                     if (instruction.getOpcode() == llvm::Instruction::Alloca) {
-                        // todo skip on allocas
                         continue;
                     }
 
                     if (instruction.getOpcode() == llvm::Instruction::Br) {
-                        // todo skip on Br -> will be replaced with branch condition assert for correct BB label evaluation
+                        // skip on Br -> will be replaced with branch condition assert for correct BB label evaluation
                         continue;
                     }
 
@@ -106,7 +103,6 @@ namespace tindger {
 
                 std::unique_ptr<tindger::Type> instructionType;
                 if (instruction.getOpcode() == llvm::Instruction::Alloca) {
-                    // todo
                     // for alloca instruction use pointer base class type
                     instructionType = typeConverter.convert(*(instruction.getOperand(0)->getType()));
                 } else {

src/llvmextractor/LLVMExtractor.h

 /**
  * @file LLVMExtractor.h
  * @author Tomas Susovsky <xsusov01@stud.fit.vutbr.cz>
- * @date 2018
+ * @date 2019
  *
  * @details LLVMExtractorInterface default implementation
  * @see LLVMExtractorInterface.h

src/llvmextractor/LLVMExtractorInterface.h

 /**
  * @file LLVMExtractorInterface.h
  * @author Tomas Susovsky <xsusov01@stud.fit.vutbr.cz>
- * @date 2018
+ * @date 2019
  *
  * @details Interface for extracting in-memory model of LLVM IR code
  *          and converting it to simplified and linearized data model
@@ -43,7 +43,8 @@ namespace tindger {
 
         struct LLVMExtractionException : std::runtime_error
         {
-            LLVMExtractionException(const std::string &message) : std::runtime_error("LLVM IR extraction failed: " + message) {}
+            LLVMExtractionException(const std::string &message) : std::runtime_error(
+                    "LLVM IR extraction failed: " + message) {}
         };
     };
 

src/llvmextractor/ModuleSelector.h

 /**
  * @file ModuleSelector.h
  * @author Tomas Susovsky <xsusov01@stud.fit.vutbr.cz>
- * @date 2018
+ * @date 2019
  *
  * @details Wrapper class for accessing internal objects of LLVM in-memory model on Module level.
  * @see llvm/IR/Module.h

src/llvmextractor/PathView.h

 /**
  * @file PathView.h
  * @author Tomas Susovsky <xsusov01@stud.fit.vutbr.cz>
- * @date 2018
+ * @date 2019
  *
  * @details Representation of function execution path for analysis containing list of visited Basic Blocks
  * @see llvm/IR/BasicBlock.h

src/llvmextractor/README.md

+submodule for handling LLVM IR input processing
+
 BasicBlockLabeler.cpp - class for assigning names to LLVM model basic blocks labels and variables names  
 BasicBlockLabeler.h
 FunctionSelector.cpp - wrapper for accessing basic blocks and arguments of LLVM function object

src/llvmextractor/TypeConverter.cpp

 /**
  * @file TypeConverter.cpp
  * @author Tomas Susovsky <xsusov01@stud.fit.vutbr.cz>
- * @date 2018
+ * @date 2019
  *
  * @details Converts LLVM types to tindger type
  */

src/llvmextractor/TypeConverter.h

 /**
  * @file TypeConverter.h
  * @author Tomas Susovsky <xsusov01@stud.fit.vutbr.cz>
- * @date 2018
+ * @date 2019
  *
  * @details Converts LLVM types to tindger type
  */

src/main.cpp

 /**
  * @file main.cpp
  * @author Tomas Susovsky <xsusov01@stud.fit.vutbr.cz>
- * @date 2018
+ * @date 2019
  *
  * @details MAIN function - program entry point:
  *          - parse CLI args
@@ -22,9 +22,9 @@
 namespace di = boost::di;
 
 const char *APP_NAME = "tindger";
-const uint8_t MAJOR_VERSION = 0;
-const uint8_t MINOR_VERSION = 1;
-const uint8_t PATCH_VERSION = 1;
+const uint8_t MAJOR_VERSION = 1;
+const uint8_t MINOR_VERSION = 0;
+const uint8_t PATCH_VERSION = 0;
 
 void printVersion(std::ostream &out)
 {

src/model/AbstractModelFactory.h

 /**
  * @file AbstractModelFactory.h
  * @author Tomas Susovsky <xsusov01@stud.fit.vutbr.cz>
- * @date 2018
+ * @date 2019
  *
  * @details interface for factory class for creating tindger abstract data model
  *  out of extracted data from LLVM in-memory model
@@ -25,7 +25,8 @@ namespace tindger {
         virtual ~AbstractModelFactory() = default;
 
         virtual std::unique_ptr<Model>
-        createModelFromTape(std::vector<Instruction> &tape, std::vector<tindger::Value> &functionArgs, std::vector<tindger::Value> &functionGlobals) const = 0;
+        createModelFromTape(std::vector<Instruction> &tape, std::vector<tindger::Value> &functionArgs,
+                            std::vector<tindger::Value> &functionGlobals) const = 0;
     };
 
 }

src/model/BasicBlock.h

-#ifndef TINDGER_BASICBLOCK_H
-#define TINDGER_BASICBLOCK_H
-
-namespace tindger {
-
-class BasicBlock
-{
-
-};
-
-}
-
-#endif //TINDGER_BASICBLOCK_H

src/model/Context.h

 /**
  * @file Context.h
  * @author Tomas Susovsky <xsusov01@stud.fit.vutbr.cz>
- * @date 2018
+ * @date 2019
  *
  * @details Class storing Context for transducing llvm code to smt-lib code
 */

src/model/Instruction.h

+/**
+ * @file Instruction.h
+ * @author Tomas Susovsky <xsusov01@stud.fit.vutbr.cz>
+ * @date 2019
+ *
+ * @details Class for holding simplified instruction data for analysis.
+*/
+
 #ifndef TINDGER_INSTRUCTION_H
 #define TINDGER_INSTRUCTION_H
 
@@ -7,9 +15,6 @@
 #include "types/Type.h"
 #include "Value.h"
 
-// todo remove llvm dep from model package
-#include <llvm/IR/Instruction.h>
-
 namespace tindger {
 
     class Instruction
@@ -75,7 +80,7 @@ namespace tindger {
 
             return instStr;
         }
-        
+
     private:
         uint32_t pc = 0;
         const uint32_t opcode;

src/model/LLVMInstructionVisitor.cpp

@@ -61,7 +61,7 @@ namespace tindger {
     void LLVMInstructionVisitor::visitUnsupportedInstruction(const llvm::Instruction &instruction)
     {
         std::cerr << "Unsupported instruction #" + std::to_string(instruction.getOpcode()) + " visited " +
-                llvmValuePrinter.valueToString(&instruction) << std::endl;
+                     llvmValuePrinter.valueToString(&instruction) << std::endl;
     }
 
     void LLVMInstructionVisitor::visitBinaryOperator(const llvm::BinaryOperator &instruction)
@@ -292,12 +292,6 @@ namespace tindger {
         const auto stackPointerOffset = context.getStackAllocationOffset();
 
         context.getSmtDriver().addVariableAllocation(allocatedVar, name, stackPointerOffset);
-        /*
-        // todo fix DL obtaining
-        const auto dataLayout = llvm::DataLayout("");
-        const auto allocatedSizeBits = instruction.getAllocationSizeInBits(dataLayout);
-        if (allocatedSizeBits.hasValue() && allocatedSizeBits.getValue() > 0) {
-         */
         const auto allocatedSizeBits = instruction.getAllocatedType()->isPointerTy()
                                        ? context.getSmtDriver().getPtrSize()
                                        : instruction.getAllocatedType()->getScalarSizeInBits();
@@ -385,7 +379,6 @@ namespace tindger {
             callArguments.push_back(arg);
         }
 
-        // todo: disitinguish pure x inpure function call by metadata spec
         context.getSmtDriver().declareFunction(function, function->getName(), callArguments);
 
         if (!instruction.getType()->isVoidTy()) {
@@ -424,11 +417,12 @@ namespace tindger {
         } else {
             // only for simple functions
             const auto returnVarWrite = std::find_if(tape.begin(), tape.end(),
-                                                          [&returnValue](const std::pair<const llvm::Instruction *, uint32_t> &instructionPair) -> bool {
-                                                              return instructionPair.first == returnValue;
-                                                          });
+                                                     [&returnValue](
+                                                             const std::pair<const llvm::Instruction *, uint32_t> &instructionPair) -> bool {
+                                                         return instructionPair.first == returnValue;
+                                                     });
             if (returnVarWrite != tape.end()) {
-                
+
             }
         }
     }

src/model/Model.cpp

-#include "Model.h"
+/**
+ * @file Model.cpp
+ * @author Tomas Susovsky <xsusov01@stud.fit.vutbr.cz>
+ * @date 2019
+ *
+ * @details Class used for modelling which variables needs to be asserted by SMT solver.
+*/
 
+#include "Model.h"
 #include <algorithm>
 #include "model/types/IntegerType.h"
 #include "model/types/VoidType.h"

src/model/Model.h

+/**
+ * @file Model.h
+ * @author Tomas Susovsky <xsusov01@stud.fit.vutbr.cz>
+ * @date 2019
+ *
+ * @details Class used for modelling which variables needs to be asserted by SMT solver.
+*/
 #ifndef TINDGER_MODEL_H
 #define TINDGER_MODEL_H
 

src/model/ModelFactory.cpp

+/**
+ * @file ModelFactory.cpp
+ * @author Tomas Susovsky <xsusov01@stud.fit.vutbr.cz>
+ * @date 2019
+ *
+ * @details Factory class for creating Model objects.
+*/
+
+
 #include "ModelFactory.h"
 
 namespace tindger {

src/model/ModelFactory.h

+/**
+ * @file ModelFactory.h
+ * @author Tomas Susovsky <xsusov01@stud.fit.vutbr.cz>
+ * @date 2019
+ *
+ * @details Factory class for creating Model objects.
+*/
+
 #ifndef TINDGER_MODELFACTORY_H
 #define TINDGER_MODELFACTORY_H
 

src/model/README.md

 types - submodule for supported data types modeling for analysis & SMT generation 
 
-AbstractModelFactory.h \
-BasicBlock.h \
-Context.cpp \
+AbstractModelFactory.h - factory class for creating Model objects interface. \
+Context.cpp - holds variables analysis information through instructions visits and provides visitor access to path's view and SMT API. \
 Context.h \
-Instruction.h \
-LLVMInstructionVisitor.cpp \
+Instruction.h - simplified instruction data representation. \
+LLVMInstructionVisitor.cpp - LLVM::Instruction visitor for instruction analysis, variables preparing and SMT expressions generation requesting. \
 LLVMInstructionVisitor.h \ 
-LLVMValuePrinter.h \ 
-Model.cpp \
+LLVMValuePrinter.h - utility class for converting llvm objects to string. \ 
+Model.cpp - class modelling variables needed to be asserted by SMT solver. \
 Model.h \
-ModelFactory.cpp \
+ModelFactory.cpp - factory class for creating Model objects implementation. \
 ModelFactory.h \
-Value.h \
-VariablesRegistry.cpp \
-VariablesRegistry.h \
+Value.h - class for values to assert in SMT data encapsulation. \
+VariablesRegistry.cpp - class storing information about analyzed code variables and primes names generation. \
+VariablesRegistry.h 

src/model/Value.h

+/**
+ * @file Value.h
+ * @author Tomas Susovsky <xsusov01@stud.fit.vutbr.cz>
+ * @date 2019
+ *
+ * @details DTO class for values to assert in SMT data encapsulation.
+*/
+
 #ifndef TINDGER_VALUE_H
 #define TINDGER_VALUE_H
 
@@ -14,12 +22,14 @@ namespace tindger {
         Value(std::string name, std::unique_ptr<Type> &&type) : type(std::move(type)), name(std::move(name)) {}
 
         Value(std::string name, std::unique_ptr<Type> &&type, uint64_t &&rawData) : type(std::move(type)),
-                                                                                  name(std::move(name)),
-                                                                                  rawData(rawData) {}
+                                                                                    name(std::move(name)),
+                                                                                    rawData(rawData) {}
 
-        Value(const Value &value) : type(value.type->clone()), name(value.name), useCounter(value.useCounter), rawData(value.rawData) {}
+        Value(const Value &value) : type(value.type->clone()), name(value.name), useCounter(value.useCounter),
+                                    rawData(value.rawData) {}
 
-        Value(Value &&value) noexcept : type(std::move(value.type)), name(value.name), useCounter(value.useCounter), rawData(value.rawData) {}
+        Value(Value &&value) noexcept : type(std::move(value.type)), name(value.name), useCounter(value.useCounter),
+                                        rawData(value.rawData) {}
 
         virtual ~Value() = default;
 

src/smt/README.md

 memory - submodule for working with memory model (for SMT solver querying of memory abstraction)
 
-ResultModel.h
-SMTContext.h
-SMTDriver.h
-Sort.h
-Z3Context.h
-Z3Context.cpp
-Z3Driver.cpp
+ResultModel.h - Class for holding results of SMT solver execution and SMT-LIB code. \
+SMTDriver.h - Interface for SMT-solvers API drivers. \
+Sort.h - Structure for SMT data types data. \
+Z3Context.cpp - Context for storing generated expressions and encapsulating z3::context for Z3Driver \
+Z3Context.h \
+Z3Driver.cpp - SMTDriver API implementation for Z3 solver. \
 Z3Driver.h

src/smt/ResultModel.h

+/**
+ * @file ResultModel.h
+ * @author Tomas Susovsky <xsusov01@stud.fit.vutbr.cz>
+ * @date 2019
+ *
+ * @details Class for holding results of SMT solver execution and SMT-LIB code.
+ */
+
 #ifndef TINDGER_RESULTMODEL_H
 #define TINDGER_RESULTMODEL_H
 
@@ -5,43 +13,45 @@
 #include <string>
 #include <ostream>
 
-class ResultModel
-{
-public:
-    ResultModel() = default;
+namespace tindger {
+    class ResultModel
+    {
+    public:
+        ResultModel() = default;
 
-    ResultModel(std::string errorMessage, std::string rawSmt2Code) : errorMessage(errorMessage),
-                                                                     rawSmt2Code(rawSmt2Code) {};
+        ResultModel(std::string errorMessage, std::string rawSmt2Code) : errorMessage(errorMessage),
+                                                                         rawSmt2Code(rawSmt2Code) {};
 
-    virtual ~ResultModel() = default;
+        virtual ~ResultModel() = default;
 
-    void addVar(std::string varName, std::string serializedValue)
-    {
-        varTable[std::move(varName)] = std::move(serializedValue);
-    }
+        void addVar(std::string varName, std::string serializedValue)
+        {
+            varTable[std::move(varName)] = std::move(serializedValue);
+        }
 
-    void print(std::ostream &out, const std::string &prefix = "") const
-    {
-        for (auto varIterator = varTable.begin(); varIterator != varTable.end(); varIterator++) {
-            out << prefix << '"' << varIterator->first << '"' << ": " << varIterator->second
-                << (std::next(varIterator) != varTable.end() ? ", " : "") << std::endl;
+        void print(std::ostream &out, const std::string &prefix = "") const
+        {
+            for (auto varIterator = varTable.begin(); varIterator != varTable.end(); varIterator++) {
+                out << prefix << '"' << varIterator->first << '"' << ": " << varIterator->second
+                    << (std::next(varIterator) != varTable.end() ? ", " : "") << std::endl;
+            }
         }
-    }
 
-    void printError(std::ostream &out, const std::string &prefix = "") const
-    {
-        out << prefix << "\"" << errorMessage << "\"" << std::endl;
-    }
+        void printError(std::ostream &out, const std::string &prefix = "") const
+        {
+            out << prefix << "\"" << errorMessage << "\"" << std::endl;
+        }
 
-    void printSmt2(std::ostream &out) const
-    {
-        out << rawSmt2Code << std::endl;
-    }
-
-private:
-    std::map<std::string, std::string> varTable;
-    std::string errorMessage;
-    std::string rawSmt2Code;
-};
+        void printSmt2(std::ostream &out) const
+        {
+            out << rawSmt2Code << std::endl;
+        }
+
+    private:
+        std::map<std::string, std::string> varTable;
+        std::string errorMessage;
+        std::string rawSmt2Code;
+    };
+}
 
 #endif //TINDGER_RESULTMODEL_H

src/smt/SMTDriver.h

+/**
+ * @file SMTDriver.h
+ * @author Tomas Susovsky <xsusov01@stud.fit.vutbr.cz>
+ * @date 2019
+ *
+ * @details Interface for SMT-solver API.
+ */
+
 #ifndef TINDGER_SMTDRIVER_H
 #define TINDGER_SMTDRIVER_H
 
@@ -8,59 +16,65 @@
 #include "Sort.h"
 #include "model/Model.h"
 
-class SMTDriver
-{
-public:
-    SMTDriver() noexcept = default;
+namespace tindger {
+
+    class SMTDriver
+    {
+    public:
+        SMTDriver() noexcept = default;
+
+        virtual ~SMTDriver() noexcept = default;
 
-    virtual ~SMTDriver() noexcept = default ;
+        virtual ResultModel solve(const tindger::Model &model) = 0;
 
-    virtual ResultModel solve(const tindger::Model &model) = 0;
+        virtual void addArg(std::size_t index, std::string name, tindger::Sort sort) = 0;
 
-    virtual void addArg(std::size_t index, std::string name, tindger::Sort sort) = 0;
+        virtual void addAlias(const llvm::Value *original, const std::string &originalName, const llvm::Value *alias,
+                              const std::string &aliasName) = 0;
 
-    virtual void addAlias(const llvm::Value *original, const std::string &originalName, const llvm::Value *alias,
-                          const std::string &aliasName) = 0;
+        virtual void addExtension(const llvm::Value *from, const std::string &fromName, const llvm::Value *to,
+                                  const std::string &toName, bool isSigned) = 0;
 
-    virtual void addExtension(const llvm::Value *from, const std::string &fromName, const llvm::Value *to,
-                              const std::string &toName, bool isSigned) = 0;
+        virtual void addBinaryOperator(int32_t opcode, const llvm::Value *result, const std::string &resultName,
+                                       const llvm::Value *firstOperand, const std::string &firstOperandName,
+                                       const llvm::Value *secondOperand, const std::string &secondOperandName) = 0;
 
-    virtual void addBinaryOperator(int32_t opcode, const llvm::Value *result, const std::string &resultName,
-                                   const llvm::Value *firstOperand, const std::string &firstOperandName,
-                                   const llvm::Value *secondOperand, const std::string &secondOperandName) = 0;
+        virtual void
+        addPredicate(llvm::CmpInst::Predicate predicate, const llvm::Value *result, const std::string &resultName,
+                     const llvm::Value *firstOperand, const std::string &firstOperandName,
+                     const llvm::Value *secondOperand,
+                     const std::string &secondOperandName) = 0;
 
-    virtual void
-    addPredicate(llvm::CmpInst::Predicate predicate, const llvm::Value *result, const std::string &resultName,
-                 const llvm::Value *firstOperand, const std::string &firstOperandName, const llvm::Value *secondOperand,
-                 const std::string &secondOperandName) = 0;
+        virtual void
+        assertCondition(const llvm::Value *condition, const std::string &conditionVarName, bool evalutaion) = 0;
 
-    virtual void
-    assertCondition(const llvm::Value *condition, const std::string &conditionVarName, bool evalutaion) = 0;
+        virtual void addVariableAllocation(const llvm::Value *allocatedVar, const std::string &name,
+                                           std::size_t stackPointerOffset) = 0;
 
-    virtual void addVariableAllocation(const llvm::Value *allocatedVar, const std::string &name,
-                                       std::size_t stackPointerOffset) = 0;
+        virtual void addStore(const llvm::Value *pointer, const std::string &pointerName, const llvm::Value *value,
+                              const std::string &valueName) = 0;
 
-    virtual void addStore(const llvm::Value *pointer, const std::string &pointerName, const llvm::Value *value,
-                          const std::string &valueName) = 0;
+        virtual void addLoad(const llvm::Value *pointer, const std::string &pointerName, const llvm::Value *result,
+                             const std::string &resultName) = 0;
 
-    virtual void addLoad(const llvm::Value *pointer, const std::string &pointerName, const llvm::Value *result,
-                         const std::string &resultName) = 0;
+        virtual void
+        addGetElementPtr(const llvm::Value *pointer, const std::string &pointerName, const llvm::Value *result,
+                         const std::string &resultName, const std::vector<std::size_t> &indexes) = 0;
 
-    virtual void addGetElementPtr(const llvm::Value *pointer, const std::string &pointerName, const llvm::Value *result,
-                                  const std::string &resultName, const std::vector<std::size_t> &indexes) = 0;
+        virtual void declareFunction(const llvm::Function *function, const std::string &name,
+                                     const std::vector<const llvm::Value *> &args) = 0;
 
-    virtual void declareFunction(const llvm::Function *function, const std::string &name,
-                                 const std::vector<const llvm::Value *> &args) = 0;
+        virtual void
+        addFunctionCall(const llvm::Value *resultVar, const std::string &resultName, const std::string &functionName,
+                        const std::vector<const llvm::Value *> &args) = 0;
 
-    virtual void
-    addFunctionCall(const llvm::Value *resultVar, const std::string &resultName, const std::string &functionName,
-                    const std::vector<const llvm::Value *> &args) = 0;
+        virtual void defineFunction(const llvm::Function *function, const std::string &functionName,
+                                    const std::vector<const llvm::Value *> &args,
+                                    const llvm::Constant &constantReturnValue) = 0;
 
-    virtual void defineFunction(const llvm::Function *function, const std::string &functionName,
-                                const std::vector<const llvm::Value *> &args,
-                                const llvm::Constant &constantReturnValue) = 0;
+        virtual std::size_t getPtrSize() const noexcept = 0;
+    };
 
-    virtual std::size_t getPtrSize() const noexcept = 0;
-};
+}
 
 #endif //TINDGER_SMTDRIVER_H

src/smt/Sort.h

-//
-// Created by xsusov01 on 25.11.18.
-//
+/**
+ * @file Sort.h
+ * @author Tomas Susovsky <xsusov01@stud.fit.vutbr.cz>
+ * @date 2019
+ *
+ * @details Structure for SMT data types data.
+ */
 
 #ifndef TINDGER_SORT_H
 #define TINDGER_SORT_H
 
-#include <map>
-#include <memory>
-
 namespace tindger {
 
     /** sort declared by declare-sort in smt */

src/smt/Z3Context.cpp

+/**
+ * @file Z3Context.cpp
+ * @author Tomas Susovsky <xsusov01@stud.fit.vutbr.cz>
+ * @date 2019
+ *
+ * @details Class for encapsulating z3::context and storing generated expressions for Z3Driver.
+ */
+
 #include "Z3Context.h"
 
-std::string Z3Context::toString()
-{
-    std::stringstream ss;
-    ss << "; expresions:" << std::endl;
-    for (const auto &expr : expressions) {
-        ss << expr.to_string() << std::endl;
-    }
-    ss << "; known addresses:" << std::endl;
-    for (const auto &address : knownAddresses) {
-        ss << address.to_string() << std::endl;
+namespace tindger {
+
+    std::string Z3Context::toString()
+    {
+        std::stringstream ss;
+        ss << "; expresions:" << std::endl;
+        for (const auto &expr : expressions) {
+            ss << expr.to_string() << std::endl;
+        }
+        ss << "; known addresses:" << std::endl;
+        for (const auto &address : knownAddresses) {
+            ss << address.to_string() << std::endl;
+        }
+
+        return ss.str();
     }
 
-    return ss.str();
-}
+    void Z3Context::addExpression(const z3::expr &expr)
+    {
+        expressions.push_back(expr);
+    }
 
-void Z3Context::addExpression(const z3::expr &expr)
-{
-    expressions.push_back(expr);
-}
+    void Z3Context::addExpressionsToSolver(z3::solver &solver)
+    {
+        for (const auto &expr : expressions) {
+            solver.add(expr);
+        }
+    }
 
-void Z3Context::addExpressionsToSolver(z3::solver &solver)
-{
-    for (const auto &expr : expressions) {
-        solver.add(expr);
+    void Z3Context::registerKnownAddress(const std::string &symbolicAddressName)
+    {
+        const auto symbolicAddress = createPointerExpr(symbolicAddressName);
+        knownAddresses.push_back(symbolicAddress);
     }
-}
-
-void Z3Context::registerKnownAddress(const std::string &symbolicAddressName)
-{
-    const auto symbolicAddress = createPointerExpr(symbolicAddressName);
-    knownAddresses.push_back(symbolicAddress);
-}
-
-void Z3Context::mapPointerArgToKnownAddress(const std::string &pointerArgName)
-{
-    const auto argVal = createPointerExpr(pointerArgName);
-    // is nullable
-    const auto nullptrMapping = z3::expr(argVal == getNullptrExpr());
-    z3::expr exclusiveMapping = nullptrMapping;
-    for (const auto &address : knownAddresses) {
-        const auto mappingToKnownAddress = z3::expr(argVal == address);
-        exclusiveMapping = z3::expr(logicalXor(exclusiveMapping, mappingToKnownAddress));
+
+    void Z3Context::mapPointerArgToKnownAddress(const std::string &pointerArgName)
+    {
+        const auto argVal = createPointerExpr(pointerArgName);
+        // is nullable
+        const auto nullptrMapping = z3::expr(argVal == getNullptrExpr());
+        z3::expr exclusiveMapping = nullptrMapping;
+        for (const auto &address : knownAddresses) {
+            const auto mappingToKnownAddress = z3::expr(argVal == address);
+            exclusiveMapping = z3::expr(logicalXor(exclusiveMapping, mappingToKnownAddress));
+        }
     }
+
 }
\ No newline at end of file

src/smt/Z3Context.h

+/**
+ * @file Z3Context.h
+ * @author Tomas Susovsky <xsusov01@stud.fit.vutbr.cz>
+ * @date 2019
+ *
+ * @details Class for encapsulating z3::context and storing generated expressions for Z3Driver.
+ */
+
 #ifndef TINDGER_Z3CONTEXT_H
 #define TINDGER_Z3CONTEXT_H
 
@@ -5,157 +13,160 @@
 #include <vector>
 #include <z3++.h>
 
-class Z3Context
-{
-public:
-    Z3Context(const std::string name, std::size_t ptrSize)
-            : name{name},
-              ptrSize{ptrSize},
-              context(z3::context()),
-              expressions{z3::expr_vector(this->context)},
-              knownAddresses{z3::expr_vector(this->context)} {}
-
-    virtual ~Z3Context() {}
-
-    virtual std::string toString();
-
-    void addExpression(const z3::expr &expr);
-
-    void addExpressionsToSolver(z3::solver &solver);
-
-    void registerKnownAddress(const std::string &symbolicAddressName);
-
-    void mapPointerArgToKnownAddress(const std::string &pointerArgName);
-
-    inline z3::expr createConstant(const std::string &varName, z3::sort &sort)
-    {
-        return context.constant(varName.c_str(), sort);
-    }
-
-    inline z3::expr createBoolExpr(const std::string &varName) noexcept
-    {
-        return context.bool_const(varName.c_str());
-    }
-
-    inline z3::expr createBoolValue(bool value) noexcept
-    {
-        return context.bool_val(value);
-    }
-
-    inline z3::expr createBitvectorExpr(const std::string &varName, unsigned int sizeBits) noexcept
-    {
-        return context.bv_const(varName.c_str(), sizeBits);
-    }
-
-    inline z3::expr createBitvectorOrBollExpr(const std::string &varName, unsigned int sizeBits) noexcept
-    {
-        return sizeBits == 1 ? createBoolExpr(varName) : createBitvectorExpr(varName, sizeBits);
-    }
-
-    inline z3::sort createBoolSort() noexcept
-    {
-        return context.bool_sort();
-    }
-
-    inline z3::sort createBitvectorSort(unsigned int sizeBits) noexcept
-    {
-        return context.bv_sort(sizeBits);
-    }
-
-    inline z3::sort createBitvectorOrBoolSort(unsigned int sizeBits) noexcept
-    {
-        return sizeBits == 1 ? createBoolSort() : createBitvectorSort(sizeBits);
-    }
-
-    inline z3::sort createPointerSort() noexcept
-    {
-        return context.bv_sort(ptrSize);
-    }
-
-    inline z3::sort createArraySort(unsigned int indexSize, z3::sort &elementSort)
-    {
-        const auto indexSort = createBitvectorSort(indexSize);
-        return context.array_sort(indexSort, elementSort);
-    }
-
-    inline z3::expr createBitvectorValue(uint64_t value, unsigned int sizeBits) noexcept
-    {
-        return context.bv_val(value, sizeBits);
-    }
-
-    inline z3::expr createBitvectorOrBoolValue(uint64_t value, unsigned int sizeBits) noexcept
-    {
-        return sizeBits == 1 ? createBoolValue(value) : createBitvectorValue(value, sizeBits);
-    }
-
-    inline z3::expr createPointerExpr(const std::string &pointerName) noexcept
-    {
-        return createBitvectorExpr(pointerName, ptrSize);
-    }
-
-    inline z3::expr getNullptrExpr() noexcept
-    {
-        return context.bv_val(0, ptrSize);
-    }
-
-    inline z3::expr logicalXor(const z3::expr a, const z3::expr b) const
-    {
-        return (a && !b) || (!a && b);
-    }
-
-    inline z3::expr createTrueBitvector()
-    {
-        return createBitvectorValue(1, 1);
-    }
-
-    inline z3::expr createFalseBitvector()
-    {
-        return createBitvectorValue(0, 1);
-    }
-
-    inline z3::expr boolToBitvector(const z3::expr booleanVar)
-    {
-        return z3::ite(booleanVar, createTrueBitvector(), createFalseBitvector());
-    }
-
-    inline z3::ast getNullAst() noexcept
-    {
-        return z3::ast(context);
-    }
-
-    inline z3::func_decl createFunction(const std::string &functionName, z3::sort_vector &domain, z3::sort &returnSort)
-    {
-        return context.function(functionName.c_str(), domain, returnSort);
-    }
-
-    inline z3::expr_vector createExprVector()
-    {
-        return z3::expr_vector(context);
-    }
-
-    inline z3::sort_vector createSortVector()
-    {
-        return z3::sort_vector(context);
-    }
-
-    inline z3::func_decl_vector createFuncDeclVector()
-    {
-        return z3::func_decl_vector(context);
-    }
-
-    inline z3::solver createSolver()
-    {
-        return z3::solver(context);
-    }
-
-private:
-    const std::string name;
-    const std::size_t ptrSize;
-    z3::context context;
-
-    z3::expr_vector expressions;
-    z3::expr_vector knownAddresses;
-};
-
+namespace tindger {
+    class Z3Context
+    {
+    public:
+        Z3Context(const std::string name, std::size_t ptrSize)
+                : name{name},
+                  ptrSize{ptrSize},
+                  context(z3::context()),
+                  expressions{z3::expr_vector(this->context)},
+                  knownAddresses{z3::expr_vector(this->context)} {}
+
+        virtual ~Z3Context() {}
+
+        virtual std::string toString();
+
+        void addExpression(const z3::expr &expr);
+
+        void addExpressionsToSolver(z3::solver &solver);
+
+        void registerKnownAddress(const std::string &symbolicAddressName);
+
+        void mapPointerArgToKnownAddress(const std::string &pointerArgName);
+
+        inline z3::expr createConstant(const std::string &varName, z3::sort &sort)
+        {
+            return context.constant(varName.c_str(), sort);
+        }
+
+        inline z3::expr createBoolExpr(const std::string &varName) noexcept
+        {
+            return context.bool_const(varName.c_str());
+        }
+
+        inline z3::expr createBoolValue(bool value) noexcept
+        {
+            return context.bool_val(value);
+        }
+
+        inline z3::expr createBitvectorExpr(const std::string &varName, unsigned int sizeBits) noexcept
+        {
+            return context.bv_const(varName.c_str(), sizeBits);
+        }
+
+        inline z3::expr createBitvectorOrBollExpr(const std::string &varName, unsigned int sizeBits) noexcept
+        {
+            return sizeBits == 1 ? createBoolExpr(varName) : createBitvectorExpr(varName, sizeBits);
+        }
+
+        inline z3::sort createBoolSort() noexcept
+        {
+            return context.bool_sort();
+        }
+
+        inline z3::sort createBitvectorSort(unsigned int sizeBits) noexcept
+        {
+            return context.bv_sort(sizeBits);
+        }
+
+        inline z3::sort createBitvectorOrBoolSort(unsigned int sizeBits) noexcept
+        {
+            return sizeBits == 1 ? createBoolSort() : createBitvectorSort(sizeBits);
+        }
+
+        inline z3::sort createPointerSort() noexcept
+        {
+            return context.bv_sort(ptrSize);
+        }
+
+        inline z3::sort createArraySort(unsigned int indexSize, z3::sort &elementSort)
+        {
+            const auto indexSort = createBitvectorSort(indexSize);
+            return context.array_sort(indexSort, elementSort);
+        }
+
+        inline z3::expr createBitvectorValue(uint64_t value, unsigned int sizeBits) noexcept
+        {
+            return context.bv_val(value, sizeBits);
+        }
+
+        inline z3::expr createBitvectorOrBoolValue(uint64_t value, unsigned int sizeBits) noexcept
+        {
+            return sizeBits == 1 ? createBoolValue(value) : createBitvectorValue(value, sizeBits);
+        }
+
+        inline z3::expr createPointerExpr(const std::string &pointerName) noexcept
+        {
+            return createBitvectorExpr(pointerName, ptrSize);
+        }
+
+        inline z3::expr getNullptrExpr() noexcept
+        {
+            return context.bv_val(0, ptrSize);
+        }
+
+        inline z3::expr logicalXor(const z3::expr a, const z3::expr b) const
+        {
+            return (a && !b) || (!a && b);
+        }
+
+        inline z3::expr createTrueBitvector()
+        {
+            return createBitvectorValue(1, 1);
+        }
+
+        inline z3::expr createFalseBitvector()
+        {
+            return createBitvectorValue(0, 1);
+        }
+
+        inline z3::expr boolToBitvector(const z3::expr booleanVar)
+        {
+            return z3::ite(booleanVar, createTrueBitvector(), createFalseBitvector());
+        }
+
+        inline z3::ast getNullAst() noexcept
+        {
+            return z3::ast(context);
+        }
+
+        inline z3::func_decl
+        createFunction(const std::string &functionName, z3::sort_vector &domain, z3::sort &returnSort)
+        {
+            return context.function(functionName.c_str(), domain, returnSort);
+        }
+
+        inline z3::expr_vector createExprVector()
+        {
+            return z3::expr_vector(context);
+        }
+
+        inline z3::sort_vector createSortVector()
+        {
+            return z3::sort_vector(context);
+        }
+
+        inline z3::func_decl_vector createFuncDeclVector()
+        {
+            return z3::func_decl_vector(context);
+        }
+
+        inline z3::solver createSolver()
+        {
+            return z3::solver(context);
+        }
+
+    private:
+        const std::string name;
+        const std::size_t ptrSize;
+        z3::context context;
+
+        z3::expr_vector expressions;
+        z3::expr_vector knownAddresses;
+    };
+
+}
 
 #endif //TINDGER_Z3CONTEXT_H

src/smt/memory/AlignedMemoryModel.cpp

@@ -78,7 +78,7 @@ namespace tindger {
                 .append(pointerName)
                 .append("_offset_")
                 .append(std::to_string(byteOffset));
-        
+
         return memoryCellName;
     }
 }
\ No newline at end of file

src/smt/memory/AlignedMemoryModel.h

@@ -55,14 +55,15 @@ namespace tindger {
         }
 
         std::string getMemorySnapshotAliasName() const { return "memory_" + std::to_string(opCounter); }
-        
-        std::string getMemoryCellName(const std::string &memorySnapshotName, const std::string &pointerName, uint32_t byteOffset) const;
+
+        std::string getMemoryCellName(const std::string &memorySnapshotName, const std::string &pointerName,
+                                      uint32_t byteOffset) const;
 
         Z3Context &context;
         z3::expr *memory;
 
         const uint32_t bitsInByte = 8;
-        
+
         uint64_t opCounter = 0;
         z3::sort *ptrSort;
         z3::sort *memoryElementSort;

src/smt/memory/MemoryManagementEngine.h

@@ -13,7 +13,6 @@
 
 namespace tindger {
 
-
     class MemoryManagementEngine
     {
     public:

src/smt/memory/README.md

 submodule for working with memory model (for SMT solver querying of memory abstraction)
 
-AlignedMemoryModel.cpp \
+AlignedMemoryModel.cpp - Memory model interface implementation with array of 8-bit bitvectors \
 AlignedMemoryModel.h \
-MemoryManagementEngine.h
+MemoryManagementEngine.h - Memory model interface