...
 
Commits (11)
/**
* @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()
*/
......
/**
* @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
......
/**
* @file AppParams.cpp
* @author Tomas Susovsky <xsusov01@stud.fit.vutbr.cz>
* @date 2018
* @date 2019
*
* @details Structure to hold parsed program options
*/
......
/**
* @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
......
/**
* @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
*/
......
/**
* @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
......
/**
* @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
......
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 \
......
/**
* @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.
*/
......
/**
* @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.
......
/**
* @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
......
/**
* @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
......
/**
* @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 {
......
/**
* @file LLVMExtractor.h
* @author Tomas Susovsky <xsusov01@stud.fit.vutbr.cz>
* @date 2018
* @date 2019
*
* @details LLVMExtractorInterface default implementation
* @see 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) {}
};
};
......
/**
* @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
......
/**
* @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
......
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
......
/**
* @file TypeConverter.cpp
* @author Tomas Susovsky <xsusov01@stud.fit.vutbr.cz>
* @date 2018
* @date 2019
*
* @details Converts LLVM types to tindger type
*/
......
/**
* @file TypeConverter.h
* @author Tomas Susovsky <xsusov01@stud.fit.vutbr.cz>
* @date 2018
* @date 2019
*
* @details Converts LLVM types to tindger type
*/
......
/**
* @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)
{
......
/**
* @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;
};
}
......
#ifndef TINDGER_BASICBLOCK_H
#define TINDGER_BASICBLOCK_H
namespace tindger {
class BasicBlock
{
};
}
#endif //TINDGER_BASICBLOCK_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
*/
......
/**
* @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;
......
......@@ -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()) {
}
}
}
......
#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"
......
/**
* @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
......
/**
* @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 {
......
/**
* @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
......
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
/**
* @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;
......
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
/**
* @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
/**
* @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
//
// 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 */
......
/**
* @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
/**
* @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
This diff is collapsed.
This diff is collapsed.
......@@ -78,7 +78,7 @@ namespace tindger {
.append(pointerName)
.append("_offset_")
.append(std::to_string(byteOffset));
return memoryCellName;
}
}
\ No newline at end of file
......@@ -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;
......
......@@ -13,7 +13,6 @@
namespace tindger {
class MemoryManagementEngine
{
public:
......
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