From fba762703c35692c65418f0fd9e3c78137f515db Mon Sep 17 00:00:00 2001 From: radl97 Date: Sun, 9 Aug 2020 00:14:08 +0200 Subject: [PATCH 01/47] Remove loop to recursive conversion --- src/LLVM/Automaton/FunctionToCfa.h | 24 ++++++++++++------------ src/LLVM/Automaton/ModuleToAutomata.cpp | 21 +++++++++++---------- 2 files changed, 23 insertions(+), 22 deletions(-) diff --git a/src/LLVM/Automaton/FunctionToCfa.h b/src/LLVM/Automaton/FunctionToCfa.h index 9a4154e0..4ad45d92 100644 --- a/src/LLVM/Automaton/FunctionToCfa.h +++ b/src/LLVM/Automaton/FunctionToCfa.h @@ -114,11 +114,11 @@ class CfaGenInfo return &function->getEntryBlock(); } - if (auto loop = getSourceLoop()) { + /*if (auto loop = getSourceLoop()) { return loop->getHeader(); - } + }*/ - llvm_unreachable("A CFA source can only be a function or a loop!"); + llvm_unreachable("A CFA source can only be a function!"); } // Variables @@ -192,17 +192,17 @@ class GenerationContext const SpecialFunctions& specialFunctions, const LLVMFrontendSettings& settings ) : mSystem(system), mMemoryModel(memoryModel), mTypes(types), - mLoopInfos(loopInfos), mSpecialFunctions(specialFunctions), mSettings(settings) + /*mLoopInfos(loopInfos), */mSpecialFunctions(specialFunctions), mSettings(settings) {} GenerationContext(const GenerationContext&) = delete; GenerationContext& operator=(const GenerationContext&) = delete; - CfaGenInfo& createLoopCfaInfo(Cfa* cfa, llvm::Loop* loop) + /*CfaGenInfo& createLoopCfaInfo(Cfa* cfa, llvm::Loop* loop) { CfaGenInfo& info = mProcedures.try_emplace(loop, *this, cfa, loop).first->second; return info; - } + }*/ CfaGenInfo& createFunctionCfaInfo(Cfa* cfa, llvm::Function* function) { @@ -225,7 +225,7 @@ class GenerationContext } } - CfaGenInfo& getLoopCfa(llvm::Loop* loop) { return getInfoFor(loop); } + //CfaGenInfo& getLoopCfa(llvm::Loop* loop) { return getInfoFor(loop); } CfaGenInfo& getFunctionCfa(llvm::Function* function) { return getInfoFor(function); } llvm::iterator_range::iterator> procedures() @@ -233,10 +233,10 @@ class GenerationContext return llvm::make_range(mProcedures.begin(), mProcedures.end()); } - llvm::LoopInfo* getLoopInfoFor(const llvm::Function* function) + /*llvm::LoopInfo* getLoopInfoFor(const llvm::Function* function) { return mLoopInfos(function); - } + }*/ std::string uniqueName(const llvm::Twine& base = ""); @@ -260,7 +260,7 @@ class GenerationContext AutomataSystem& mSystem; MemoryModel& mMemoryModel; LLVMTypeTranslator& mTypes; - LoopInfoFuncTy mLoopInfos; + //LoopInfoFuncTy mLoopInfos; const SpecialFunctions& mSpecialFunctions; const LLVMFrontendSettings& mSettings; std::unordered_map mProcedures; @@ -382,9 +382,9 @@ class BlocksToCfa : public InstToExpr ); void createExitTransition(const llvm::BasicBlock* target, Location* pred, const ExprPtr& succCondition); - void createCallToLoop( + /*void createCallToLoop( llvm::Loop* loop, const llvm::BasicBlock* source, const llvm::BasicBlock* target, - const ExprPtr& condition, Location* exit); + const ExprPtr& condition, Location* exit);*/ ExprPtr getExitCondition(const llvm::BasicBlock* target, Variable* exitSelector, CfaGenInfo& nestedInfo); size_t getNumUsesInBlocks(const llvm::Instruction* inst) const; diff --git a/src/LLVM/Automaton/ModuleToAutomata.cpp b/src/LLVM/Automaton/ModuleToAutomata.cpp index 7aa65e92..5d3c8686 100644 --- a/src/LLVM/Automaton/ModuleToAutomata.cpp +++ b/src/LLVM/Automaton/ModuleToAutomata.cpp @@ -155,6 +155,7 @@ static bool isErrorBlock(llvm::BasicBlock* bb) return false; } +/* /// If \p bb is part of a loop nested into the CFA represented by \p genInfo, returns this loop. /// Otherwise, this function returns nullptr. static llvm::Loop* getNestedLoopOf(GenerationContext& genCtx, CfaGenInfo& genInfo, const llvm::BasicBlock* bb) @@ -188,7 +189,7 @@ static llvm::Loop* getNestedLoopOf(GenerationContext& genCtx, CfaGenInfo& genInf } llvm_unreachable("A CFA source should either be a function or a loop."); -} +}*/ static gazer::Type& getExitSelectorType(IntRepresentation ints, GazerContext& context) { @@ -292,10 +293,10 @@ void ModuleToCfa::createAutomata() DenseSet visitedBlocks; // Create a CFA for each loop nested in this function - LoopInfo* loopInfo = mGenCtx.getLoopInfoFor(&function); + /*LoopInfo* loopInfo = mGenCtx.getLoopInfoFor(&function);*/ unsigned loopCount = 0; - auto loops = loopInfo->getLoopsInPreorder(); + /*auto loops = loopInfo->getLoopsInPreorder(); for (Loop* loop : loops) { std::string name = getLoopName(loop, loopCount, cfa->getName()); @@ -349,7 +350,7 @@ void ModuleToCfa::createAutomata() } visitedBlocks.insert(loop->getBlocks().begin(), loop->getBlocks().end()); - } + }*/ // Now that all loops in this function have been dealt with, translate the function itself. CfaGenInfo& genInfo = mGenCtx.createFunctionCfaInfo(cfa, &function); @@ -383,14 +384,14 @@ void ModuleToCfa::createAutomata() // For the local variables, we only need to add the values not present in any of the loops. for (BasicBlock& bb : function) { for (Instruction& inst : bb) { - if (auto loop = loopInfo->getLoopFor(&bb)) { + /*if (auto loop = loopInfo->getLoopFor(&bb)) { // If the variable is an output of a loop, add it here as a local variable Variable* output = mGenCtx.getLoopCfa(loop).findOutput(&inst); if (output == nullptr && !hasUsesInBlockRange(&inst, functionBlocks)) { LLVM_DEBUG(llvm::dbgs() << "Not adding " << inst << "\n"); continue; } - } + }*/ if (!inst.getType()->isVoidTy()) { functionVarDecl.createLocal(&inst, mGenCtx.getTypes().get(inst.getType())); @@ -815,14 +816,14 @@ void BlocksToCfa::handleSuccessor(const BasicBlock* succ, const ExprPtr& succCon mMemoryInstHandler.handleBasicBlockEdge(*parent, *succ, phiEp); mCfa->createAssignTransition(exit, to, succCondition, phiAssignments); - } else if (auto loop = getNestedLoopOf(mGenCtx, mGenInfo, succ)) { + } else /*if (auto loop = getNestedLoopOf(mGenCtx, mGenInfo, succ)) { this->createCallToLoop(loop, parent, succ, succCondition, exit); - } else { + } else */{ createExitTransition(succ, exit, succCondition); } } -void BlocksToCfa::createCallToLoop( +/*void BlocksToCfa::createCallToLoop( llvm::Loop* loop, const llvm::BasicBlock* source, const llvm::BasicBlock* target, const ExprPtr& condition, Location* exit) { @@ -893,7 +894,7 @@ void BlocksToCfa::createCallToLoop( createExitTransition(exitBlock, exit, condition); } } -} +}*/ void BlocksToCfa::insertOutputAssignments(CfaGenInfo& callee, std::vector& outputArgs) { From f8e4018555407da5e38417c7df9a27d3bd082880 Mon Sep 17 00:00:00 2001 From: radl97 Date: Sun, 9 Aug 2020 01:38:06 +0200 Subject: [PATCH 02/47] Enable call transitions in CFA (only valid in XCFA) --- src/LLVM/Automaton/AutomatonPasses.cpp | 2 +- test/theta/cfa/Expected/counter.theta | 6 +- tools/gazer-theta/lib/ThetaCfaGenerator.cpp | 136 +++++++++++++------- 3 files changed, 97 insertions(+), 47 deletions(-) diff --git a/src/LLVM/Automaton/AutomatonPasses.cpp b/src/LLVM/Automaton/AutomatonPasses.cpp index 856ea237..411bd201 100644 --- a/src/LLVM/Automaton/AutomatonPasses.cpp +++ b/src/LLVM/Automaton/AutomatonPasses.cpp @@ -95,7 +95,7 @@ bool ModuleToAutomataPass::runOnModule(llvm::Module& module) // translate it to the format of another verifier immediately. // TODO: We should translate automata other than the main in this case. - TransformRecursiveToCyclic(mSystem->getMainAutomaton()); + //TransformRecursiveToCyclic(mSystem->getMainAutomaton()); } return false; diff --git a/test/theta/cfa/Expected/counter.theta b/test/theta/cfa/Expected/counter.theta index 2f6683df..6289b076 100644 --- a/test/theta/cfa/Expected/counter.theta +++ b/test/theta/cfa/Expected/counter.theta @@ -1,5 +1,5 @@ main process __gazer_main_process { - var main_RET_VAL : int + var result : int var main_tmp : int var main_error_phi : int var main___gazer_error_field : int @@ -32,7 +32,7 @@ main process __gazer_main_process { } loc5 -> loc1 { - main_RET_VAL := 0 + result := 0 } loc6 -> loc7 { @@ -46,4 +46,4 @@ main process __gazer_main_process { main___gazer_error_field := main_error_phi } -} \ No newline at end of file +} diff --git a/tools/gazer-theta/lib/ThetaCfaGenerator.cpp b/tools/gazer-theta/lib/ThetaCfaGenerator.cpp index 13a7ff07..7726515d 100644 --- a/tools/gazer-theta/lib/ThetaCfaGenerator.cpp +++ b/tools/gazer-theta/lib/ThetaCfaGenerator.cpp @@ -86,7 +86,10 @@ struct ThetaLocDecl : ThetaAst struct ThetaStmt : ThetaAst { - using VariantTy = std::variant, std::string>; + using callType = std::tuple, + std::optional>; + using VariantTy = std::variant, std::string, callType>; /* implicit */ ThetaStmt(VariantTy content) : mContent(content) @@ -119,6 +122,12 @@ struct ThetaStmt : ThetaAst void print(llvm::raw_ostream& os) const override; VariantTy mContent; + static ThetaStmt Call( + llvm::StringRef name, + llvm::SmallVector vector, + std::optional result) { + return VariantTy{callType{name, vector, result}}; + } }; struct ThetaEdgeDecl : ThetaAst @@ -155,27 +164,60 @@ class ThetaVarDecl : ThetaAst } // end anonymous namespace -void ThetaStmt::print(llvm::raw_ostream& os) const +struct PrintVisitor { - struct PrintVisitor - { - llvm::raw_ostream& mOS; - explicit PrintVisitor(llvm::raw_ostream& os) : mOS(os) {} + llvm::raw_ostream& mOS; + std::function mCanonizeName; - void operator()(const ExprPtr& expr) { - mOS << "assume "; - mOS << theta::printThetaExpr(expr); - } + PrintVisitor(llvm::raw_ostream& os, std::function canonizeName) + : mOS(os), mCanonizeName(canonizeName) + {} - void operator()(const std::pair& assign) { - mOS << assign.first << " := "; - mOS << theta::printThetaExpr(assign.second); - } + explicit PrintVisitor(llvm::raw_ostream& os) + : mOS(os), mCanonizeName([](Variable* v) {return v->getName();}) + {} + + void operator()(const ExprPtr& expr) { + mOS << "assume "; + mOS << theta::printThetaExpr(expr, mCanonizeName); + } - void operator()(const std::string& variable) { - mOS << "havoc " << variable; + void operator()(const std::pair& assign) { + mOS << assign.first << " := "; + mOS << theta::printThetaExpr(assign.second, mCanonizeName); + } + + void operator()(const std::string& variable) { + mOS << "havoc " << variable; + } + + void operator()(const std::tuple, + std::optional>& call) { + auto result = std::get<2>(call); + auto prefix = result.has_value() ? mCanonizeName(result.value()) + llvm::Twine(" := ") : ""; + + mOS << prefix << "call " << std::get<0>(call) << "("; + bool first = true; + for (const auto& param : std::get<1>(call)) { + if (first) { + first = false; + } else { + mOS << ", "; + } + if (auto var = llvm::dyn_cast(param.getValue())) { + mOS << mCanonizeName(&(var->getVariable())); + } else { + llvm_unreachable("parameter should be a variable reference"); + } } - } visitor(os); + mOS << ")"; + } +}; + +void ThetaStmt::print(llvm::raw_ostream& os) const +{ + PrintVisitor visitor(os); std::visit(visitor, mContent); } @@ -235,6 +277,11 @@ void ThetaCfaGenerator::write(llvm::raw_ostream& os, ThetaNameMapping& nameTrace for (auto& variable : main->locals()) { auto name = validName(variable.getName(), isValidVarName); auto type = typeName(variable.getType()); + + // name should be "result" if it is the/an output instead of the original (_RES_VAR) + if (std::find(main->outputs().begin(), main->outputs().end(), variable) != main->outputs().end()) { + name = "result"; + } nameTrace.variables[name] = &variable; vars.try_emplace(&variable, std::make_unique(name, type)); @@ -251,7 +298,7 @@ void ThetaCfaGenerator::write(llvm::raw_ostream& os, ThetaNameMapping& nameTrace // Add locations for (Location* loc : main->nodes()) { ThetaLocDecl::Flag flag = ThetaLocDecl::Loc_State; - if (loc == recursiveToCyclicResult.errorLocation) { + if (loc == nameTrace.errorLocation) { flag = ThetaLocDecl::Loc_Error; } else if (main->getEntry() == loc) { flag = ThetaLocDecl::Loc_Init; @@ -287,7 +334,33 @@ void ThetaCfaGenerator::write(llvm::raw_ostream& os, ThetaNameMapping& nameTrace } } } else if (auto callEdge = dyn_cast(edge)) { - llvm_unreachable("CallTransitions are not supported in theta CFAs!"); + assert(callEdge->getNumOutputs() <= 1 && "calls should have at most one output"); + + llvm::SmallVector inputs; + for (const auto& input : callEdge->inputs()) { + auto lhsName = input.getVariable()->getName(); + + auto rhs = input.getValue(); + static int paramCounter = 0; + // Create a new variable because XCFA needs it. + auto newVarName = "call_param_tmp_" + llvm::Twine(paramCounter++); + + auto variable = main->createLocal(newVarName.str(), rhs->getType()); + auto name = validName(variable->getName(), isValidVarName); + auto type = typeName(variable->getType()); + + nameTrace.variables[name] = variable; + vars.try_emplace(variable, std::make_unique(name, type)); + + // initialize the new variable + stmts.push_back(ThetaStmt::Assign(variable->getName(), rhs)); + inputs.push_back(VariableAssignment(input.getVariable(), variable->getRefExpr())); + } + std::optional result = {}; + if (callEdge->getNumOutputs() == 1) { + result = callEdge->outputs().begin()->getVariable(); + } + stmts.push_back(ThetaStmt::Call(callEdge->getCalledAutomaton()->getName(), inputs, result)); } edges.emplace_back(std::make_unique(source, target, std::move(stmts))); @@ -322,30 +395,7 @@ void ThetaCfaGenerator::write(llvm::raw_ostream& os, ThetaNameMapping& nameTrace os << INDENT << edge->mSource.mName << " -> " << edge->mTarget.mName << " {\n"; for (auto& stmt : edge->mStmts) { os << INDENT2; - struct PrintVisitor - { - llvm::raw_ostream& mOS; - std::function mCanonizeName; - - PrintVisitor(llvm::raw_ostream& os, std::function canonizeName) - : mOS(os), mCanonizeName(canonizeName) - {} - - void operator()(const ExprPtr& expr) { - mOS << "assume "; - mOS << theta::printThetaExpr(expr, mCanonizeName); - } - - void operator()(const std::pair& assign) { - mOS << assign.first << " := "; - mOS << theta::printThetaExpr(assign.second, mCanonizeName); - } - - void operator()(const std::string& variable) { - mOS << "havoc " << variable; - } - } visitor(os, canonizeName); - + PrintVisitor visitor(os, canonizeName); std::visit(visitor, stmt.mContent); os << "\n"; } From cb6b533170c89cf448300233cc7256f729dd3805 Mon Sep 17 00:00:00 2001 From: radl97 Date: Sun, 9 Aug 2020 14:25:49 +0200 Subject: [PATCH 03/47] Rewrite CFA generation to XCFA --- tools/gazer-theta/lib/ThetaCfaGenerator.cpp | 122 ++++++++++++-------- tools/gazer-theta/lib/ThetaCfaGenerator.h | 2 + 2 files changed, 77 insertions(+), 47 deletions(-) diff --git a/tools/gazer-theta/lib/ThetaCfaGenerator.cpp b/tools/gazer-theta/lib/ThetaCfaGenerator.cpp index 7726515d..3ee2f814 100644 --- a/tools/gazer-theta/lib/ThetaCfaGenerator.cpp +++ b/tools/gazer-theta/lib/ThetaCfaGenerator.cpp @@ -152,6 +152,8 @@ class ThetaVarDecl : ThetaAst llvm::StringRef getName() { return mName; } + llvm::StringRef getType() { return mType; } + void print(llvm::raw_ostream& os) const override { os << "var " << mName << " : " << mType; @@ -170,7 +172,7 @@ struct PrintVisitor std::function mCanonizeName; PrintVisitor(llvm::raw_ostream& os, std::function canonizeName) - : mOS(os), mCanonizeName(canonizeName) + : mOS(os), mCanonizeName(std::move(canonizeName)) {} explicit PrintVisitor(llvm::raw_ostream& os) @@ -197,7 +199,8 @@ struct PrintVisitor auto result = std::get<2>(call); auto prefix = result.has_value() ? mCanonizeName(result.value()) + llvm::Twine(" := ") : ""; - mOS << prefix << "call " << std::get<0>(call) << "("; + // TODO main -> xmain temp solution + mOS << prefix << "call x" << std::get<0>(call) << "("; bool first = true; for (const auto& param : std::get<1>(call)) { if (first) { @@ -253,8 +256,32 @@ static std::string typeName(Type& type) void ThetaCfaGenerator::write(llvm::raw_ostream& os, ThetaNameMapping& nameTrace) { - Cfa* main = mSystem.getMainAutomaton(); - auto recursiveToCyclicResult = TransformRecursiveToCyclic(main); + os << "main process main_process {\n"; + for (Cfa& cfa : mSystem) { + writeCFA(os, &cfa, nameTrace); + } + os << "}\n"; +} + +std::string ThetaCfaGenerator::validName(std::string name, std::function isUnique) +{ + name = std::regex_replace(name, std::regex("[^a-zA-Z0-9_]"), "_"); + + if (std::find(ThetaKeywords.begin(), ThetaKeywords.end(), name) != ThetaKeywords.end()) { + name += "_gazer"; + } + + while (!isUnique(name)) { + llvm::Twine nextTry = name + llvm::Twine(mTmpCount++); + name = nextTry.str(); + } + + return name; +} + +void ThetaCfaGenerator::writeCFA(llvm::raw_ostream& os, Cfa* cfa, ThetaNameMapping& nameTrace) { + // this should not be needed, but it does some extra stuff related to error handling + auto recursiveToCyclicResult = TransformRecursiveToCyclic(cfa); nameTrace.errorLocation = recursiveToCyclicResult.errorLocation; nameTrace.errorFieldVariable = recursiveToCyclicResult.errorFieldVariable; @@ -267,42 +294,43 @@ void ThetaCfaGenerator::write(llvm::raw_ostream& os, ThetaNameMapping& nameTrace // Create a closure to test variable names auto isValidVarName = [&vars](const std::string& name) -> bool { - // The variable name should not be present in the variable list. - return std::find_if(vars.begin(), vars.end(), [name](auto& v1) { - return name == v1.second->getName(); - }) == vars.end(); + // The variable name should not be present in the variable list. + return std::find_if(vars.begin(), vars.end(), [name](auto& v1) { + return name == v1.second->getName(); + }) == vars.end(); }; // Add variables - for (auto& variable : main->locals()) { + for (auto& variable : cfa->locals()) { auto name = validName(variable.getName(), isValidVarName); auto type = typeName(variable.getType()); - // name should be "result" if it is the/an output instead of the original (_RES_VAR) - if (std::find(main->outputs().begin(), main->outputs().end(), variable) != main->outputs().end()) { - name = "result"; - } - + //// name should be "result" if it is the output instead of the original (_RES_VAR) + //if (std::find(cfa->outputs().begin(), cfa->outputs().end(), variable) != cfa->outputs().end()) { + // name = "result"; + //} + nameTrace.variables[name] = &variable; vars.try_emplace(&variable, std::make_unique(name, type)); } - for (auto& variable : main->inputs()) { + // inputs are defined elsewhere + for (auto& variable : cfa->inputs()) { auto name = validName(variable.getName(), isValidVarName); auto type = typeName(variable.getType()); - nameTrace.variables[name] = &variable; +// nameTrace.variables[name] = &variable; vars.try_emplace(&variable, std::make_unique(name, type)); } // Add locations - for (Location* loc : main->nodes()) { + for (Location* loc : cfa->nodes()) { ThetaLocDecl::Flag flag = ThetaLocDecl::Loc_State; if (loc == nameTrace.errorLocation) { flag = ThetaLocDecl::Loc_Error; - } else if (main->getEntry() == loc) { + } else if (cfa->getEntry() == loc) { flag = ThetaLocDecl::Loc_Init; - } else if (main->getExit() == loc) { + } else if (cfa->getExit() == loc) { flag = ThetaLocDecl::Loc_Final; } @@ -313,10 +341,10 @@ void ThetaCfaGenerator::write(llvm::raw_ostream& os, ThetaNameMapping& nameTrace } // Add edges - for (Transition* edge : main->edges()) { + for (Transition* edge : cfa->edges()) { ThetaLocDecl& source = *locs[edge->getSource()]; ThetaLocDecl& target = *locs[edge->getTarget()]; - + std::vector stmts; if (edge->getGuard() != BoolLiteralExpr::True(edge->getGuard()->getContext())) { @@ -345,7 +373,7 @@ void ThetaCfaGenerator::write(llvm::raw_ostream& os, ThetaNameMapping& nameTrace // Create a new variable because XCFA needs it. auto newVarName = "call_param_tmp_" + llvm::Twine(paramCounter++); - auto variable = main->createLocal(newVarName.str(), rhs->getType()); + auto variable = cfa->createLocal(newVarName.str(), rhs->getType()); auto name = validName(variable->getName(), isValidVarName); auto type = typeName(variable->getType()); @@ -353,7 +381,7 @@ void ThetaCfaGenerator::write(llvm::raw_ostream& os, ThetaNameMapping& nameTrace vars.try_emplace(variable, std::make_unique(name, type)); // initialize the new variable - stmts.push_back(ThetaStmt::Assign(variable->getName(), rhs)); + stmts.push_back(ThetaStmt::Assign(name, rhs)); inputs.push_back(VariableAssignment(input.getVariable(), variable->getRefExpr())); } std::optional result = {}; @@ -370,22 +398,38 @@ void ThetaCfaGenerator::write(llvm::raw_ostream& os, ThetaNameMapping& nameTrace auto INDENT2 = " "; auto canonizeName = [&vars](Variable* variable) -> std::string { - if (vars.count(variable) == 0) { - return variable->getName(); - } + if (vars.count(variable) == 0) { + return variable->getName(); + } - return vars[variable]->getName(); + return vars[variable]->getName(); }; - os << "main process __gazer_main_process {\n"; - - for (auto& variable : llvm::concat(main->inputs(), main->locals())) { + if (cfa == mSystem.getMainAutomaton()) { + os << "main "; + } + // TODO main -> xmain temp solution + os << "procedure x" << cfa->getName() << "("; + bool first = true; + for (auto& input : cfa->inputs()) { + if (first) { + first = false; + } else { + os << ", "; + } + auto name = vars[&input]->getName(); + auto type = vars[&input]->getType(); + + os << name << " : " << type; + } + os << ") {\n"; + for (auto& variable : cfa->locals()) { os << INDENT; vars[&variable]->print(os); os << "\n"; } - for (Location* loc : main->nodes()) { + for (Location* loc : cfa->nodes()) { os << INDENT; locs[loc]->print(os); os << "\n"; @@ -406,19 +450,3 @@ void ThetaCfaGenerator::write(llvm::raw_ostream& os, ThetaNameMapping& nameTrace os << "}\n"; os.flush(); } - -std::string ThetaCfaGenerator::validName(std::string name, std::function isUnique) -{ - name = std::regex_replace(name, std::regex("[^a-zA-Z0-9_]"), "_"); - - if (std::find(ThetaKeywords.begin(), ThetaKeywords.end(), name) != ThetaKeywords.end()) { - name += "_gazer"; - } - - while (!isUnique(name)) { - llvm::Twine nextTry = name + llvm::Twine(mTmpCount++); - name = nextTry.str(); - } - - return name; -} diff --git a/tools/gazer-theta/lib/ThetaCfaGenerator.h b/tools/gazer-theta/lib/ThetaCfaGenerator.h index 942d93d3..88a8cf76 100644 --- a/tools/gazer-theta/lib/ThetaCfaGenerator.h +++ b/tools/gazer-theta/lib/ThetaCfaGenerator.h @@ -52,6 +52,7 @@ struct ThetaNameMapping llvm::DenseMap inlinedVariables; }; +/// XXX Currently creates an XCFA class ThetaCfaGenerator { public: @@ -63,6 +64,7 @@ class ThetaCfaGenerator private: std::string validName(std::string name, std::function isUnique); + void writeCFA(llvm::raw_ostream& os, Cfa* cfa, ThetaNameMapping& nameTrace); private: AutomataSystem& mSystem; From 383220e484006c2cc944644a4ed781bb3f14ece8 Mon Sep 17 00:00:00 2001 From: radl97 Date: Sun, 9 Aug 2020 14:29:02 +0200 Subject: [PATCH 04/47] Remove trace generation --- tools/gazer-theta/lib/ThetaVerifier.cpp | 5 +++-- 1 file changed, 3 insertions(+), 2 deletions(-) diff --git a/tools/gazer-theta/lib/ThetaVerifier.cpp b/tools/gazer-theta/lib/ThetaVerifier.cpp index 4f646cc1..c2992e9e 100644 --- a/tools/gazer-theta/lib/ThetaVerifier.cpp +++ b/tools/gazer-theta/lib/ThetaVerifier.cpp @@ -192,7 +192,8 @@ auto ThetaVerifierImpl::execute(llvm::StringRef input) -> std::unique_ptr std::unique_ptrparseCex(cex, &failureCode); - return VerificationResult::CreateFail(failureCode, std::move(trace)); + return VerificationResult::CreateFail(failureCode, std::move(trace));*/ } return VerificationResult::CreateInternalError("Theta returned unrecognizable output. Raw output is:\n" + thetaOutput); From 99314370770dafc954f297096ab332ad0d4ec464 Mon Sep 17 00:00:00 2001 From: radl97 Date: Sun, 9 Aug 2020 18:11:19 +0200 Subject: [PATCH 05/47] Add global variables to AutomataSystem --- include/gazer/Automaton/Cfa.h | 8 ++++++++ src/Automaton/Cfa.cpp | 9 +++++++++ 2 files changed, 17 insertions(+) diff --git a/include/gazer/Automaton/Cfa.h b/include/gazer/Automaton/Cfa.h index acc065fa..e0951761 100644 --- a/include/gazer/Automaton/Cfa.h +++ b/include/gazer/Automaton/Cfa.h @@ -345,6 +345,10 @@ class AutomataSystem final AutomataSystem(const AutomataSystem&) = delete; AutomataSystem& operator=(const AutomataSystem&) = delete; + Variable* createGlobal( + std::basic_string, std::allocator> basicString, + Type& type); + public: Cfa* createCfa(std::string name); @@ -370,7 +374,11 @@ class AutomataSystem final private: GazerContext& mContext; std::vector> mAutomata; + std::vector mGlobals; Cfa* mMainAutomaton; +public: + using globals_iterator = decltype(mGlobals.begin()); + llvm::iterator_range globals() { return llvm::make_range(mGlobals.begin(), mGlobals.end()); } }; inline llvm::raw_ostream& operator<<(llvm::raw_ostream& os, const Transition& transition) diff --git a/src/Automaton/Cfa.cpp b/src/Automaton/Cfa.cpp index 6da51e85..81e41056 100644 --- a/src/Automaton/Cfa.cpp +++ b/src/Automaton/Cfa.cpp @@ -341,3 +341,12 @@ void AutomataSystem::setMainAutomaton(Cfa* cfa) assert(&cfa->getParent() == this); mMainAutomaton = cfa; } + +Variable* AutomataSystem::createGlobal( + std::string name, + Type& type) +{ + auto result = mContext.createVariable(name, type); + mGlobals.push_back(result); + return result; +} From 50a129312783c18461e9c37ba1bc4a1f5d8c21dc Mon Sep 17 00:00:00 2001 From: radl97 Date: Sun, 9 Aug 2020 18:14:20 +0200 Subject: [PATCH 06/47] Add EP for global variables --- include/gazer/LLVM/Automaton/ModuleToAutomata.h | 14 ++++++++++++++ src/LLVM/Automaton/ExtensionPoints.cpp | 6 ++++++ 2 files changed, 20 insertions(+) diff --git a/include/gazer/LLVM/Automaton/ModuleToAutomata.h b/include/gazer/LLVM/Automaton/ModuleToAutomata.h index 41349f2a..c56710c1 100644 --- a/include/gazer/LLVM/Automaton/ModuleToAutomata.h +++ b/include/gazer/LLVM/Automaton/ModuleToAutomata.h @@ -115,6 +115,20 @@ class VariableDeclExtensionPoint : public AutomatonInterfaceExtensionPoint void markOutput(ValueOrMemoryObject val, Variable* variable); }; +/// This extension can be used to insert additional global variables at the +/// very beginning of the generation process. +class GlobalVariableDeclExtensionPoint +{ +public: + explicit GlobalVariableDeclExtensionPoint(AutomataSystem& system) + : mSystem(system) + {} + + Variable* createGlobalVar(ValueOrMemoryObject val, Type& type, const std::string& suffix = ""); +private: + AutomataSystem& mSystem; +}; + /// Variable declaration extension point for loops. class LoopVarDeclExtensionPoint : public VariableDeclExtensionPoint { diff --git a/src/LLVM/Automaton/ExtensionPoints.cpp b/src/LLVM/Automaton/ExtensionPoints.cpp index afd26847..86f2ce23 100644 --- a/src/LLVM/Automaton/ExtensionPoints.cpp +++ b/src/LLVM/Automaton/ExtensionPoints.cpp @@ -105,6 +105,12 @@ Variable* VariableDeclExtensionPoint::createInput(ValueOrMemoryObject val, Type& return variable; } +Variable* GlobalVariableDeclExtensionPoint::createGlobalVar(ValueOrMemoryObject val, Type& type, const std::string& suffix) +{ + auto name = val.hasName() ? val.getName() + suffix : "_" + suffix; + return mSystem.createGlobal(name, type); +} + Variable* VariableDeclExtensionPoint::createLocal(ValueOrMemoryObject val, Type& type, const std::string& suffix) { Cfa* cfa = mGenInfo.Automaton; From 8086582f8631ca674a6480a4d788485357be042e Mon Sep 17 00:00:00 2001 From: radl97 Date: Sun, 9 Aug 2020 18:15:57 +0200 Subject: [PATCH 07/47] Add way to declare global variables in MemoryInstructionHandler --- include/gazer/LLVM/Memory/MemoryInstructionHandler.h | 4 ++++ src/LLVM/Automaton/ModuleToAutomata.cpp | 6 ++++++ 2 files changed, 10 insertions(+) diff --git a/include/gazer/LLVM/Memory/MemoryInstructionHandler.h b/include/gazer/LLVM/Memory/MemoryInstructionHandler.h index 41bc97de..0b3805a5 100644 --- a/include/gazer/LLVM/Memory/MemoryInstructionHandler.h +++ b/include/gazer/LLVM/Memory/MemoryInstructionHandler.h @@ -61,6 +61,10 @@ class MemoryInstructionHandler /// Allows the declaration of top-level procedure variables. virtual void declareFunctionVariables(llvm2cfa::VariableDeclExtensionPoint& ep) {} + /// Allows the declaration of global variables. + /// TODO this does not fit the original picture that memory models are per-function... + virtual void declareGlobalVariables(llvm2cfa::GlobalVariableDeclExtensionPoint& ep) {} + /// Allows the declaration of loop-procedure level variables. virtual void declareLoopProcedureVariables( llvm::Loop* loop, llvm2cfa::LoopVarDeclExtensionPoint& ep) {} diff --git a/src/LLVM/Automaton/ModuleToAutomata.cpp b/src/LLVM/Automaton/ModuleToAutomata.cpp index 5d3c8686..396e2472 100644 --- a/src/LLVM/Automaton/ModuleToAutomata.cpp +++ b/src/LLVM/Automaton/ModuleToAutomata.cpp @@ -280,6 +280,7 @@ std::unique_ptr ModuleToCfa::generate( void ModuleToCfa::createAutomata() { + bool firstFunction = true; // Create an automaton for each function definition and set the interfaces. for (llvm::Function& function : mModule.functions()) { if (function.isDeclaration()) { @@ -287,6 +288,11 @@ void ModuleToCfa::createAutomata() } auto& memoryInstHandler = mMemoryModel.getMemoryInstructionHandler(function); + if (firstFunction) { + GlobalVariableDeclExtensionPoint ep(*mSystem); + memoryInstHandler.declareGlobalVariables(ep); + firstFunction = false; + } Cfa* cfa = mSystem->createCfa(function.getName()); LLVM_DEBUG(llvm::dbgs() << "Created CFA " << cfa->getName() << "\n"); From 4b44803ed09b7da94d9647dfd2dd589ddb966c87 Mon Sep 17 00:00:00 2001 From: radl97 Date: Sun, 9 Aug 2020 18:17:30 +0200 Subject: [PATCH 08/47] Add SimpleMemoryModel Handles trivial uses of pointers both in global and local scope. --- include/gazer/LLVM/Memory/MemoryModel.h | 9 + src/LLVM/CMakeLists.txt | 3 +- src/LLVM/Memory/SimpleMemoryModel.cpp | 213 ++++++++++++++++++++++++ 3 files changed, 224 insertions(+), 1 deletion(-) create mode 100644 src/LLVM/Memory/SimpleMemoryModel.cpp diff --git a/include/gazer/LLVM/Memory/MemoryModel.h b/include/gazer/LLVM/Memory/MemoryModel.h index d5b90be0..386719c5 100644 --- a/include/gazer/LLVM/Memory/MemoryModel.h +++ b/include/gazer/LLVM/Memory/MemoryModel.h @@ -65,6 +65,15 @@ std::unique_ptr CreateFlatMemoryModel( std::function dominators ); +//==-----------------------------------------------------------------------==// +// SimpleMemoryModel - a memory model which represents all memory as separate locals or globals. +// Sound when these cannot alias. +std::unique_ptr CreateSimpleMemoryModel( + GazerContext& context, + const LLVMFrontendSettings& settings, + llvm::Module& module +); + class MemoryModelWrapperPass : public llvm::ModulePass { public: diff --git a/src/LLVM/CMakeLists.txt b/src/LLVM/CMakeLists.txt index 8f6ccff2..a69608e0 100644 --- a/src/LLVM/CMakeLists.txt +++ b/src/LLVM/CMakeLists.txt @@ -23,6 +23,7 @@ set(SOURCE_FILES FrontendConfig.cpp Memory/MemoryObject.cpp Memory/FlatMemoryModel.cpp + Memory/SimpleMemoryModel.cpp Memory/HavocMemoryModel.cpp Memory/MemoryModel.cpp Memory/MemorySSA.cpp @@ -32,7 +33,7 @@ set(SOURCE_FILES Automaton/ExtensionPoints.cpp Automaton/ValueOrMemoryObject.cpp Analysis/PDG.cpp -) + Memory/SimpleMemoryModel.cpp) llvm_map_components_to_libnames(GAZER_LLVM_LIBS core irreader transformutils scalaropts ipo) message(STATUS "Using LLVM libraries: ${GAZER_LLVM_LIBS}") diff --git a/src/LLVM/Memory/SimpleMemoryModel.cpp b/src/LLVM/Memory/SimpleMemoryModel.cpp new file mode 100644 index 00000000..44365c0f --- /dev/null +++ b/src/LLVM/Memory/SimpleMemoryModel.cpp @@ -0,0 +1,213 @@ +//==-------------------------------------------------------------*- C++ -*--==// +// +// Copyright 2020 Contributors to the Gazer project +// +// Licensed under the Apache License, Version 2.0 (the "License"); +// you may not use this file except in compliance with the License. +// You may obtain a copy of the License at +// +// http://www.apache.org/licenses/LICENSE-2.0 +// +// Unless required by applicable law or agreed to in writing, software +// distributed under the License is distributed on an "AS IS" BASIS, +// WITHOUT WARRANTIES OR CONDITIONS OF ANY KIND, either express or implied. +// See the License for the specific language governing permissions and +// limitations under the License. +// +//===----------------------------------------------------------------------===// +/// +/// \file This file defines the SimpleMemoryModel class, a memory model which +/// represents all memory as separate locals or globals. +/// Sound when these cannot alias. +/// +//===----------------------------------------------------------------------===// + +#include "gazer/LLVM/Memory/MemoryModel.h" + +#include + +using namespace gazer; + +namespace { + +class SimpleMemoryInstructionHandler : public MemoryInstructionHandler, public MemoryTypeTranslator { + LLVMTypeTranslator types; + llvm::Module& module; +public: + + SimpleMemoryInstructionHandler(GazerContext& context, + const LLVMFrontendSettings& settings, + llvm::Module& module) : + MemoryTypeTranslator(context), types(*this, settings), module(module) { + } + + void declareGlobalVariables(llvm2cfa::GlobalVariableDeclExtensionPoint &ep) override { + for (const auto& val : module.globals()) { + auto var = ep.createGlobalVar(&val, types.get(val.getValueType())); + vars.insert({&val, var}); + } + } + + /// Allows the declaration of top-level procedure variables. + void declareFunctionVariables(llvm2cfa::VariableDeclExtensionPoint& ep) override {} + + // Allocations + //==--------------------------------------------------------------------==// + + llvm::DenseMap vars; + + /// Translates an alloca instruction into an assignable expression. + ExprPtr handleAlloca( + const llvm::AllocaInst& alloc, + llvm2cfa::GenerationStepExtensionPoint& ep) override { + auto var = ep.createAuxiliaryVariable(alloc.getName(), types.get(alloc.getAllocatedType())); + vars.insert({&alloc, var}); + return var->getRefExpr(); + } + + // Pointer value representation + //==--------------------------------------------------------------------==// + // These methods are used to translate various pointer-related values. + // As they are supposed to return expressions without side-effects, these + // do not get access to an extension point. Instead, they receive the + // already-translated operands of their instruction as an input parameter. + + /// Represents a given non-instruction pointer. + ExprPtr handlePointerValue(const llvm::Value* value) override { + llvm_unreachable("Pointers as values are not supported"); + //return ExprBuilder(getContext()).Undef(value->getType()); + } + + /// Represents a pointer casting instruction. + ExprPtr handlePointerCast( + const llvm::CastInst& cast, + const ExprPtr& origPtr) override { + llvm_unreachable("Pointer casts are not supported"); + // maybe this will do? + // return origPtr; + } + + /// Represents a pointer arithmetic instruction. + ExprPtr handleGetElementPtr( + const llvm::GetElementPtrInst& gep, + llvm::ArrayRef ops) override { + llvm_unreachable("GEP (probably lowered from array accesses) are not supported"); + } + + /// Translates constant arrays. + ExprPtr handleConstantDataArray( + const llvm::ConstantDataArray* cda, llvm::ArrayRef> elems) override { + llvm_unreachable("CDA (probably lowered from constant array accesses) are not supported"); + } + + // Memory definitions and uses + //==--------------------------------------------------------------------==// + + /// Translates the given store instruction. + void handleStore( + const llvm::StoreInst& store, + llvm2cfa::GenerationStepExtensionPoint& ep) override { + ep.insertAssignment(vars[store.getPointerOperand()], ep.getAsOperand(store.getValueOperand())); + } + + /// Handles possible memory definitions in the beginning of blocks. + void handleBlock( + const llvm::BasicBlock& bb, llvm2cfa::GenerationStepExtensionPoint& ep) override + {} + + /// Handles possible memory phi-nodes on basic block edges. + void handleBasicBlockEdge( + const llvm::BasicBlock& source, + const llvm::BasicBlock& target, + llvm2cfa::GenerationStepExtensionPoint& ep) override + {} + + /// Returns the value of a load as an assignable expression. + ExprPtr handleLoad( + const llvm::LoadInst& load, + llvm2cfa::GenerationStepExtensionPoint& ep) override { + auto var = vars[load.getPointerOperand()]; + // save the current value of the variable + // TODO this can be done smarter if there is no store after this particular load + auto resultVar = ep.createAuxiliaryVariable("load_" + var->getName(), var->getType()); + ep.insertAssignment(resultVar, var->getRefExpr()); + return resultVar->getRefExpr(); + } + + /// Translates a given call instruction. Clients can assume that the callee + /// function has a definition and a corresponding automaton already exists. + /// The parameters \p inputAssignments and \p outputAssignments will be placed + /// on the resulting automaton call _after_ the regular input/output assignments. + void handleCall( + llvm::CallSite call, + llvm2cfa::GenerationStepExtensionPoint& callerEp, + llvm2cfa::AutomatonInterfaceExtensionPoint& calleeEp, + llvm::SmallVectorImpl& inputAssignments, + llvm::SmallVectorImpl& outputAssignments) override { + + } + + /// If the memory model wishes to handle external calls to unknown functions, it + /// may do so through this method. Note that known memory-related functions such + /// as malloc, memset, memcpy, etc. have their own overridable methods, therefore + /// they should not be handled here. Furthermore, if the call is to a non-void + /// function, the translation process already generates a havoc assignment for + /// it _before_ calling this function. + void handleExternalCall( + llvm::CallSite call, llvm2cfa::GenerationStepExtensionPoint& ep) override {} + + // Memory safety predicates + //==--------------------------------------------------------------------==// + + /// Returns a boolean expression which evaluates to true if a memory access + /// through \p ptr (represented by the expression in \p expr) is valid. + ExprPtr isValidAccess(llvm::Value* ptr, const ExprPtr& expr) override { + // TODO + return ExprBuilder(getContext()).True(); + } + + ~SimpleMemoryInstructionHandler() override = default; + + gazer::Type& handlePointerType(const llvm::PointerType* type) override { + llvm_unreachable("Pointers and arrays are not supported right now"); + } + + /// Translates types of constant arrays and initializers. + gazer::Type& handleArrayType(const llvm::ArrayType* type) override { + llvm_unreachable("Pointers and arrays are not supported right now"); + } +}; + +class SimpleMemoryModel : public MemoryModel { + SimpleMemoryInstructionHandler handler; + +public: + + SimpleMemoryModel( + GazerContext& context, + const LLVMFrontendSettings& settings, + llvm::Module& module) : handler(context, settings, module) {} + + /// Returns the memory instruction translator of this memory model. + MemoryInstructionHandler& getMemoryInstructionHandler(llvm::Function& function) override + { + return handler; + } + + /// Returns the type translator of this memory model. + MemoryTypeTranslator& getMemoryTypeTranslator() override { + return handler; + } + + ~SimpleMemoryModel() override = default; +}; + +} // namespace + +std::unique_ptr gazer::CreateSimpleMemoryModel( + GazerContext& context, + const LLVMFrontendSettings& settings, + llvm::Module& module +) { + return std::make_unique(context, settings, module); +} \ No newline at end of file From 49ab301339ef7bf89d7b17ad2ae3095ffaf1db62 Mon Sep 17 00:00:00 2001 From: radl97 Date: Sun, 9 Aug 2020 18:22:05 +0200 Subject: [PATCH 09/47] Handle global variables when generating XCFA --- tools/gazer-theta/lib/ThetaCfaGenerator.cpp | 84 +++++++++++++++++---- tools/gazer-theta/lib/ThetaCfaGenerator.h | 4 - 2 files changed, 69 insertions(+), 19 deletions(-) diff --git a/tools/gazer-theta/lib/ThetaCfaGenerator.cpp b/tools/gazer-theta/lib/ThetaCfaGenerator.cpp index 3ee2f814..8efbe2d2 100644 --- a/tools/gazer-theta/lib/ThetaCfaGenerator.cpp +++ b/tools/gazer-theta/lib/ThetaCfaGenerator.cpp @@ -254,17 +254,23 @@ static std::string typeName(Type& type) } } -void ThetaCfaGenerator::write(llvm::raw_ostream& os, ThetaNameMapping& nameTrace) +class ThetaCfaProcedureGenerator { - os << "main process main_process {\n"; - for (Cfa& cfa : mSystem) { - writeCFA(os, &cfa, nameTrace); - } - os << "}\n"; -} +public: + ThetaCfaProcedureGenerator(AutomataSystem& system, Cfa* cfa, + const llvm::DenseMap>& globals) + : mSystem(system), cfa(cfa), mGlobals(globals) {} + + void writeCFA(llvm::raw_ostream& os, ThetaNameMapping& nameTrace); +private: + AutomataSystem& mSystem; + Cfa* cfa; + const llvm::DenseMap>& mGlobals; +}; -std::string ThetaCfaGenerator::validName(std::string name, std::function isUnique) +static std::string validName(std::string name, std::function isUnique) { + static int tmpCount = 0; name = std::regex_replace(name, std::regex("[^a-zA-Z0-9_]"), "_"); if (std::find(ThetaKeywords.begin(), ThetaKeywords.end(), name) != ThetaKeywords.end()) { @@ -272,14 +278,14 @@ std::string ThetaCfaGenerator::validName(std::string name, std::function> vars; std::vector> edges; + auto& globals = mGlobals; // Create a closure to test variable names - auto isValidVarName = [&vars](const std::string& name) -> bool { + auto isValidVarName = [&vars, &globals](const std::string& name) -> bool { // The variable name should not be present in the variable list. return std::find_if(vars.begin(), vars.end(), [name](auto& v1) { return name == v1.second->getName(); - }) == vars.end(); + }) == vars.end() && + std::find_if(globals.begin(), globals.end(), [name](auto& v1) { + return name == v1.second->getName(); + }) == globals.end(); }; // Add variables @@ -340,6 +350,14 @@ void ThetaCfaGenerator::writeCFA(llvm::raw_ostream& os, Cfa* cfa, ThetaNameMappi locs.try_emplace(loc, std::make_unique(locName, flag)); } + auto find_var = [&vars, &globals](Variable* var) -> const std::unique_ptr& { + auto it = vars.find(var); + if (it == vars.end()) { + return globals.find(var)->getSecond(); + } + return it->getSecond(); + }; + // Add edges for (Transition* edge : cfa->edges()) { ThetaLocDecl& source = *locs[edge->getSource()]; @@ -353,7 +371,7 @@ void ThetaCfaGenerator::writeCFA(llvm::raw_ostream& os, Cfa* cfa, ThetaNameMappi if (auto assignEdge = dyn_cast(edge)) { for (auto& assignment : *assignEdge) { - auto lhsName = vars[assignment.getVariable()]->getName(); + auto lhsName = find_var(assignment.getVariable())->getName(); // TODO isn't this canonizeName()? if (llvm::isa(assignment.getValue())) { stmts.push_back(ThetaStmt::Havoc(lhsName)); @@ -397,11 +415,15 @@ void ThetaCfaGenerator::writeCFA(llvm::raw_ostream& os, Cfa* cfa, ThetaNameMappi auto INDENT = " "; auto INDENT2 = " "; - auto canonizeName = [&vars](Variable* variable) -> std::string { + auto canonizeName = [&vars, &globals](Variable* variable) -> std::string { + auto it = globals.find(variable); + if (it != globals.end()) { + return it->getSecond()->getName(); + } + if (vars.count(variable) == 0) { return variable->getName(); } - return vars[variable]->getName(); }; @@ -450,3 +472,35 @@ void ThetaCfaGenerator::writeCFA(llvm::raw_ostream& os, Cfa* cfa, ThetaNameMappi os << "}\n"; os.flush(); } + +void ThetaCfaGenerator::write(llvm::raw_ostream& os, ThetaNameMapping& nameTrace) +{ + llvm::DenseMap> mGlobals; + auto& globals = mGlobals; + auto isValidVarName = [&globals](const std::string& name) -> bool { + // The variable name should not be present in the variable list. + return std::find_if(globals.begin(), globals.end(), [name](auto& v1) { + return name == v1.second->getName(); + }) == globals.end(); + }; + + for (auto& globalVar: mSystem.globals()) { + auto name = validName(globalVar->getName(), isValidVarName); + auto type = typeName(globalVar->getType()); + + mGlobals.insert({globalVar, std::make_unique(name, type)}); + } + + os << "main process main_process {\n"; + + for (auto& globalVar : mGlobals) { + os << " "; + globalVar.getSecond()->print(os); + os << "\n"; + } + + for (Cfa& cfa : mSystem) { + ThetaCfaProcedureGenerator(mSystem, &cfa, globals).writeCFA(os, nameTrace); + } + os << "}\n"; +} diff --git a/tools/gazer-theta/lib/ThetaCfaGenerator.h b/tools/gazer-theta/lib/ThetaCfaGenerator.h index 88a8cf76..7881efbd 100644 --- a/tools/gazer-theta/lib/ThetaCfaGenerator.h +++ b/tools/gazer-theta/lib/ThetaCfaGenerator.h @@ -62,10 +62,6 @@ class ThetaCfaGenerator void write(llvm::raw_ostream& os, ThetaNameMapping& names); -private: - std::string validName(std::string name, std::function isUnique); - void writeCFA(llvm::raw_ostream& os, Cfa* cfa, ThetaNameMapping& nameTrace); - private: AutomataSystem& mSystem; CallGraph mCallGraph; From 4077dedee04cfbb7395946c5bbb873e699517ea2 Mon Sep 17 00:00:00 2001 From: radl97 Date: Sun, 9 Aug 2020 18:23:20 +0200 Subject: [PATCH 10/47] Use simple memory model instead of havoc --- src/LLVM/Memory/MemoryModel.cpp | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/src/LLVM/Memory/MemoryModel.cpp b/src/LLVM/Memory/MemoryModel.cpp index 3b52c7d2..980b6796 100644 --- a/src/LLVM/Memory/MemoryModel.cpp +++ b/src/LLVM/Memory/MemoryModel.cpp @@ -56,7 +56,7 @@ bool MemoryModelWrapperPass::runOnModule(llvm::Module& module) break; } case MemoryModelSetting::Havoc: { - mMemoryModel = CreateHavocMemoryModel(mContext); + mMemoryModel = CreateSimpleMemoryModel(mContext, mSettings, module); // CreateHavocMemoryModel(mContext); break; } } From ffcdab5a694725d2312249259566515619c2be60 Mon Sep 17 00:00:00 2001 From: radl97 Date: Mon, 10 Aug 2020 12:56:41 +0200 Subject: [PATCH 11/47] Move CFA generation to separate files --- tools/gazer-theta/CMakeLists.txt | 4 +- tools/gazer-theta/lib/ThetaCfaGenerator.cpp | 448 +----------------- tools/gazer-theta/lib/ThetaCfaGenerator.h | 15 +- .../lib/ThetaCfaProcedureGenerator.cpp | 211 +++++++++ .../lib/ThetaCfaProcedureGenerator.h | 49 ++ tools/gazer-theta/lib/ThetaUtil.cpp | 62 +++ tools/gazer-theta/lib/ThetaUtil.h | 234 +++++++++ 7 files changed, 561 insertions(+), 462 deletions(-) create mode 100644 tools/gazer-theta/lib/ThetaCfaProcedureGenerator.cpp create mode 100644 tools/gazer-theta/lib/ThetaCfaProcedureGenerator.h create mode 100644 tools/gazer-theta/lib/ThetaUtil.cpp create mode 100644 tools/gazer-theta/lib/ThetaUtil.h diff --git a/tools/gazer-theta/CMakeLists.txt b/tools/gazer-theta/CMakeLists.txt index eca621b6..a821ab09 100644 --- a/tools/gazer-theta/CMakeLists.txt +++ b/tools/gazer-theta/CMakeLists.txt @@ -2,7 +2,9 @@ set(LIB_SOURCE_FILES lib/ThetaCfaGenerator.cpp lib/ThetaExpr.cpp lib/ThetaVerifier.cpp - lib/ThetaCfaWriterPass.cpp) + lib/ThetaCfaWriterPass.cpp + lib/ThetaCfaProcedureGenerator.cpp + lib/ThetaUtil.cpp) set(TOOL_SOURCE_FILES gazer-theta.cpp diff --git a/tools/gazer-theta/lib/ThetaCfaGenerator.cpp b/tools/gazer-theta/lib/ThetaCfaGenerator.cpp index 8efbe2d2..7816507e 100644 --- a/tools/gazer-theta/lib/ThetaCfaGenerator.cpp +++ b/tools/gazer-theta/lib/ThetaCfaGenerator.cpp @@ -16,463 +16,17 @@ // //===----------------------------------------------------------------------===// #include "ThetaCfaGenerator.h" -#include "gazer/Core/LiteralExpr.h" #include "gazer/Automaton/CfaTransforms.h" +#include "ThetaCfaProcedureGenerator.h" #include #include -#include -#include - -#include -#include -#include - using namespace gazer; using namespace gazer::theta; using llvm::dyn_cast; -namespace -{ - -constexpr std::array ThetaKeywords = { - "main", "process", "var", "loc", - "assume", "init", "final", "error", - "return", "havoc", "bool", "int", "rat", - "if", "then", "else", "iff", "imply", - "forall", "exists", "or", "and", "not", - "mod", "rem", "true", "false" -}; - -struct ThetaAst -{ - virtual void print(llvm::raw_ostream& os) const = 0; - - virtual ~ThetaAst() = default; -}; - -struct ThetaLocDecl : ThetaAst -{ - enum Flag - { - Loc_State, - Loc_Init, - Loc_Final, - Loc_Error, - }; - - ThetaLocDecl(std::string name, Flag flag = Loc_State) - : mName(name), mFlag(flag) - {} - - void print(llvm::raw_ostream& os) const override - { - switch (mFlag) { - case Loc_Init: os << "init "; break; - case Loc_Final: os << "final "; break; - case Loc_Error: os << "error "; break; - default: - break; - } - - os << "loc " << mName; - } - - std::string mName; - Flag mFlag; -}; - -struct ThetaStmt : ThetaAst -{ - using callType = std::tuple, - std::optional>; - using VariantTy = std::variant, std::string, callType>; - - /* implicit */ ThetaStmt(VariantTy content) - : mContent(content) - {} - - static ThetaStmt Assume(ExprPtr expr) - { - assert(expr->getType().isBoolType()); - - return VariantTy{expr}; - } - - static ThetaStmt Assign(std::string variableName, ExprPtr value) - { - assert(!llvm::isa(value) - && "Cannot assign an undef value to a variable." - "Use ::Havoc() to represent a nondetermistic value assignment." - ); - - std::pair pair = { variableName, value }; - - return VariantTy{pair}; - } - - static ThetaStmt Havoc(std::string variable) - { - return VariantTy{variable}; - } - - void print(llvm::raw_ostream& os) const override; - - VariantTy mContent; - static ThetaStmt Call( - llvm::StringRef name, - llvm::SmallVector vector, - std::optional result) { - return VariantTy{callType{name, vector, result}}; - } -}; - -struct ThetaEdgeDecl : ThetaAst -{ - ThetaEdgeDecl(ThetaLocDecl& source, ThetaLocDecl& target, std::vector stmts) - : mSource(source), mTarget(target), mStmts(std::move(stmts)) - {} - - void print(llvm::raw_ostream& os) const override; - - ThetaLocDecl& mSource; - ThetaLocDecl& mTarget; - std::vector mStmts; -}; - -class ThetaVarDecl : ThetaAst -{ -public: - ThetaVarDecl(std::string name, std::string type) - : mName(name), mType(type) - {} - - llvm::StringRef getName() { return mName; } - - llvm::StringRef getType() { return mType; } - - void print(llvm::raw_ostream& os) const override - { - os << "var " << mName << " : " << mType; - } - -private: - std::string mName; - std::string mType; -}; - -} // end anonymous namespace - -struct PrintVisitor -{ - llvm::raw_ostream& mOS; - std::function mCanonizeName; - - PrintVisitor(llvm::raw_ostream& os, std::function canonizeName) - : mOS(os), mCanonizeName(std::move(canonizeName)) - {} - - explicit PrintVisitor(llvm::raw_ostream& os) - : mOS(os), mCanonizeName([](Variable* v) {return v->getName();}) - {} - - void operator()(const ExprPtr& expr) { - mOS << "assume "; - mOS << theta::printThetaExpr(expr, mCanonizeName); - } - - void operator()(const std::pair& assign) { - mOS << assign.first << " := "; - mOS << theta::printThetaExpr(assign.second, mCanonizeName); - } - - void operator()(const std::string& variable) { - mOS << "havoc " << variable; - } - - void operator()(const std::tuple, - std::optional>& call) { - auto result = std::get<2>(call); - auto prefix = result.has_value() ? mCanonizeName(result.value()) + llvm::Twine(" := ") : ""; - - // TODO main -> xmain temp solution - mOS << prefix << "call x" << std::get<0>(call) << "("; - bool first = true; - for (const auto& param : std::get<1>(call)) { - if (first) { - first = false; - } else { - mOS << ", "; - } - if (auto var = llvm::dyn_cast(param.getValue())) { - mOS << mCanonizeName(&(var->getVariable())); - } else { - llvm_unreachable("parameter should be a variable reference"); - } - } - mOS << ")"; - } -}; - -void ThetaStmt::print(llvm::raw_ostream& os) const -{ - PrintVisitor visitor(os); - - std::visit(visitor, mContent); -} - -void ThetaEdgeDecl::print(llvm::raw_ostream& os) const -{ - os << mSource.mName << " -> " << mTarget.mName << " {\n"; - for (auto& stmt : mStmts) { - os << " "; - stmt.print(os); - os << "\n"; - } - os << "}\n"; -} - -static std::string typeName(Type& type) -{ - switch (type.getTypeID()) { - case Type::IntTypeID: - return "int"; - case Type::RealTypeID: - return "rat"; - case Type::BoolTypeID: - return "bool"; - case Type::ArrayTypeID: { - auto& arrTy = llvm::cast(type); - return "[" + typeName(arrTy.getIndexType()) + "] -> " + typeName(arrTy.getElementType()); - } - default: - llvm_unreachable("Types which are unsupported by theta should have been eliminated earlier!"); - } -} - -class ThetaCfaProcedureGenerator -{ -public: - ThetaCfaProcedureGenerator(AutomataSystem& system, Cfa* cfa, - const llvm::DenseMap>& globals) - : mSystem(system), cfa(cfa), mGlobals(globals) {} - - void writeCFA(llvm::raw_ostream& os, ThetaNameMapping& nameTrace); -private: - AutomataSystem& mSystem; - Cfa* cfa; - const llvm::DenseMap>& mGlobals; -}; - -static std::string validName(std::string name, std::function isUnique) -{ - static int tmpCount = 0; - name = std::regex_replace(name, std::regex("[^a-zA-Z0-9_]"), "_"); - - if (std::find(ThetaKeywords.begin(), ThetaKeywords.end(), name) != ThetaKeywords.end()) { - name += "_gazer"; - } - - while (!isUnique(name)) { - llvm::Twine nextTry = name + llvm::Twine(tmpCount++); - name = nextTry.str(); - } - - return name; -} - -void ThetaCfaProcedureGenerator::writeCFA(llvm::raw_ostream& os, ThetaNameMapping& nameTrace) { - // this should not be needed, but it does some extra stuff related to error handling - auto recursiveToCyclicResult = TransformRecursiveToCyclic(cfa); - - nameTrace.errorLocation = recursiveToCyclicResult.errorLocation; - nameTrace.errorFieldVariable = recursiveToCyclicResult.errorFieldVariable; - nameTrace.inlinedLocations = std::move(recursiveToCyclicResult.inlinedLocations); - nameTrace.inlinedVariables = std::move(recursiveToCyclicResult.inlinedVariables); - - llvm::DenseMap> locs; - llvm::DenseMap> vars; - std::vector> edges; - - auto& globals = mGlobals; - // Create a closure to test variable names - auto isValidVarName = [&vars, &globals](const std::string& name) -> bool { - // The variable name should not be present in the variable list. - return std::find_if(vars.begin(), vars.end(), [name](auto& v1) { - return name == v1.second->getName(); - }) == vars.end() && - std::find_if(globals.begin(), globals.end(), [name](auto& v1) { - return name == v1.second->getName(); - }) == globals.end(); - }; - - // Add variables - for (auto& variable : cfa->locals()) { - auto name = validName(variable.getName(), isValidVarName); - auto type = typeName(variable.getType()); - - //// name should be "result" if it is the output instead of the original (_RES_VAR) - //if (std::find(cfa->outputs().begin(), cfa->outputs().end(), variable) != cfa->outputs().end()) { - // name = "result"; - //} - - nameTrace.variables[name] = &variable; - vars.try_emplace(&variable, std::make_unique(name, type)); - } - - // inputs are defined elsewhere - for (auto& variable : cfa->inputs()) { - auto name = validName(variable.getName(), isValidVarName); - auto type = typeName(variable.getType()); - -// nameTrace.variables[name] = &variable; - vars.try_emplace(&variable, std::make_unique(name, type)); - } - - // Add locations - for (Location* loc : cfa->nodes()) { - ThetaLocDecl::Flag flag = ThetaLocDecl::Loc_State; - if (loc == nameTrace.errorLocation) { - flag = ThetaLocDecl::Loc_Error; - } else if (cfa->getEntry() == loc) { - flag = ThetaLocDecl::Loc_Init; - } else if (cfa->getExit() == loc) { - flag = ThetaLocDecl::Loc_Final; - } - - auto locName = "loc" + std::to_string(loc->getId()); - - nameTrace.locations[locName] = loc; - locs.try_emplace(loc, std::make_unique(locName, flag)); - } - - auto find_var = [&vars, &globals](Variable* var) -> const std::unique_ptr& { - auto it = vars.find(var); - if (it == vars.end()) { - return globals.find(var)->getSecond(); - } - return it->getSecond(); - }; - - // Add edges - for (Transition* edge : cfa->edges()) { - ThetaLocDecl& source = *locs[edge->getSource()]; - ThetaLocDecl& target = *locs[edge->getTarget()]; - - std::vector stmts; - - if (edge->getGuard() != BoolLiteralExpr::True(edge->getGuard()->getContext())) { - stmts.push_back(ThetaStmt::Assume(edge->getGuard())); - } - - if (auto assignEdge = dyn_cast(edge)) { - for (auto& assignment : *assignEdge) { - auto lhsName = find_var(assignment.getVariable())->getName(); // TODO isn't this canonizeName()? - - if (llvm::isa(assignment.getValue())) { - stmts.push_back(ThetaStmt::Havoc(lhsName)); - } else { - stmts.push_back(ThetaStmt::Assign(lhsName, assignment.getValue())); - } - } - } else if (auto callEdge = dyn_cast(edge)) { - assert(callEdge->getNumOutputs() <= 1 && "calls should have at most one output"); - - llvm::SmallVector inputs; - for (const auto& input : callEdge->inputs()) { - auto lhsName = input.getVariable()->getName(); - - auto rhs = input.getValue(); - static int paramCounter = 0; - // Create a new variable because XCFA needs it. - auto newVarName = "call_param_tmp_" + llvm::Twine(paramCounter++); - - auto variable = cfa->createLocal(newVarName.str(), rhs->getType()); - auto name = validName(variable->getName(), isValidVarName); - auto type = typeName(variable->getType()); - - nameTrace.variables[name] = variable; - vars.try_emplace(variable, std::make_unique(name, type)); - - // initialize the new variable - stmts.push_back(ThetaStmt::Assign(name, rhs)); - inputs.push_back(VariableAssignment(input.getVariable(), variable->getRefExpr())); - } - std::optional result = {}; - if (callEdge->getNumOutputs() == 1) { - result = callEdge->outputs().begin()->getVariable(); - } - stmts.push_back(ThetaStmt::Call(callEdge->getCalledAutomaton()->getName(), inputs, result)); - } - - edges.emplace_back(std::make_unique(source, target, std::move(stmts))); - } - - auto INDENT = " "; - auto INDENT2 = " "; - - auto canonizeName = [&vars, &globals](Variable* variable) -> std::string { - auto it = globals.find(variable); - if (it != globals.end()) { - return it->getSecond()->getName(); - } - - if (vars.count(variable) == 0) { - return variable->getName(); - } - return vars[variable]->getName(); - }; - - if (cfa == mSystem.getMainAutomaton()) { - os << "main "; - } - // TODO main -> xmain temp solution - os << "procedure x" << cfa->getName() << "("; - bool first = true; - for (auto& input : cfa->inputs()) { - if (first) { - first = false; - } else { - os << ", "; - } - auto name = vars[&input]->getName(); - auto type = vars[&input]->getType(); - - os << name << " : " << type; - } - os << ") {\n"; - for (auto& variable : cfa->locals()) { - os << INDENT; - vars[&variable]->print(os); - os << "\n"; - } - - for (Location* loc : cfa->nodes()) { - os << INDENT; - locs[loc]->print(os); - os << "\n"; - } - - for (auto& edge : edges) { - os << INDENT << edge->mSource.mName << " -> " << edge->mTarget.mName << " {\n"; - for (auto& stmt : edge->mStmts) { - os << INDENT2; - PrintVisitor visitor(os, canonizeName); - std::visit(visitor, stmt.mContent); - os << "\n"; - } - os << INDENT << "}\n"; - os << "\n"; - } - - os << "}\n"; - os.flush(); -} - void ThetaCfaGenerator::write(llvm::raw_ostream& os, ThetaNameMapping& nameTrace) { llvm::DenseMap> mGlobals; diff --git a/tools/gazer-theta/lib/ThetaCfaGenerator.h b/tools/gazer-theta/lib/ThetaCfaGenerator.h index 7881efbd..726fea6a 100644 --- a/tools/gazer-theta/lib/ThetaCfaGenerator.h +++ b/tools/gazer-theta/lib/ThetaCfaGenerator.h @@ -20,6 +20,7 @@ #include "gazer/Automaton/Cfa.h" #include "gazer/Automaton/CallGraph.h" +#include "ThetaUtil.h" #include @@ -31,10 +32,6 @@ namespace llvm namespace gazer::theta { -std::string printThetaExpr(const ExprPtr& expr); - -std::string printThetaExpr(const ExprPtr& expr, std::function variableNames); - /// \brief Perform pre-processing steps required by theta on the input CFA. /// /// This pass does the following transformations: @@ -42,16 +39,6 @@ std::string printThetaExpr(const ExprPtr& expr, std::function locations; - llvm::StringMap variables; - Location* errorLocation; - Variable* errorFieldVariable; - llvm::DenseMap inlinedLocations; - llvm::DenseMap inlinedVariables; -}; - /// XXX Currently creates an XCFA class ThetaCfaGenerator { diff --git a/tools/gazer-theta/lib/ThetaCfaProcedureGenerator.cpp b/tools/gazer-theta/lib/ThetaCfaProcedureGenerator.cpp new file mode 100644 index 00000000..207d7320 --- /dev/null +++ b/tools/gazer-theta/lib/ThetaCfaProcedureGenerator.cpp @@ -0,0 +1,211 @@ +//==-------------------------------------------------------------*- C++ -*--==// +// +// Copyright 2020 Contributors to the Gazer project +// +// Licensed under the Apache License, Version 2.0 (the "License"); +// you may not use this file except in compliance with the License. +// You may obtain a copy of the License at +// +// http://www.apache.org/licenses/LICENSE-2.0 +// +// Unless required by applicable law or agreed to in writing, software +// distributed under the License is distributed on an "AS IS" BASIS, +// WITHOUT WARRANTIES OR CONDITIONS OF ANY KIND, either express or implied. +// See the License for the specific language governing permissions and +// limitations under the License. +// +//===----------------------------------------------------------------------===// +#include "ThetaCfaProcedureGenerator.h" +#include "gazer/Automaton/CfaTransforms.h" +#include + +using namespace llvm; +using namespace gazer::theta; + +void gazer::ThetaCfaProcedureGenerator::writeCFA(llvm::raw_ostream& os, gazer::theta::ThetaNameMapping& nameTrace) { + // this should not be needed, but it does some extra stuff related to error handling + auto recursiveToCyclicResult = TransformRecursiveToCyclic(cfa); + + nameTrace.errorLocation = recursiveToCyclicResult.errorLocation; + nameTrace.errorFieldVariable = recursiveToCyclicResult.errorFieldVariable; + nameTrace.inlinedLocations = std::move(recursiveToCyclicResult.inlinedLocations); + nameTrace.inlinedVariables = std::move(recursiveToCyclicResult.inlinedVariables); + + llvm::DenseMap> locs; + llvm::DenseMap> vars; + std::vector> edges; + + const auto& globals = mGlobals; + // Create a closure to test variable names + auto isValidVarName = [&vars, &globals](const std::string& name) -> bool { + // The variable name should not be present in the variable list. + return std::find_if(vars.begin(), vars.end(), [name](auto& v1) { + return name == v1.second->getName(); + }) == vars.end() && + std::find_if(globals.begin(), globals.end(), [name](auto& v1) { + return name == v1.second->getName(); + }) == globals.end(); + }; + + // Add variables + for (auto& variable : cfa->locals()) { + auto name = validName(variable.getName(), isValidVarName); + auto type = typeName(variable.getType()); + + //// name should be "result" if it is the output instead of the original (_RES_VAR) + //if (std::find(cfa->outputs().begin(), cfa->outputs().end(), variable) != cfa->outputs().end()) { + // name = "result"; + //} + + nameTrace.variables[name] = &variable; + vars.try_emplace(&variable, std::make_unique(name, type)); + } + + // inputs are defined elsewhere + for (auto& variable : cfa->inputs()) { + auto name = validName(variable.getName(), isValidVarName); + auto type = typeName(variable.getType()); + +// nameTrace.variables[name] = &variable; + vars.try_emplace(&variable, std::make_unique(name, type)); + } + + // Add locations + for (Location* loc : cfa->nodes()) { + ThetaLocDecl::Flag flag = ThetaLocDecl::Loc_State; + if (loc == nameTrace.errorLocation) { + flag = ThetaLocDecl::Loc_Error; + } else if (cfa->getEntry() == loc) { + flag = ThetaLocDecl::Loc_Init; + } else if (cfa->getExit() == loc) { + flag = ThetaLocDecl::Loc_Final; + } + + auto locName = "loc" + std::to_string(loc->getId()); + + nameTrace.locations[locName] = loc; + locs.try_emplace(loc, std::make_unique(locName, flag)); + } + + auto find_var = [&vars, &globals](Variable* var) -> const std::unique_ptr& { + auto it = vars.find(var); + if (it == vars.end()) { + return globals.find(var)->getSecond(); + } + return it->getSecond(); + }; + + // Add edges + for (Transition* edge : cfa->edges()) { + ThetaLocDecl& source = *locs[edge->getSource()]; + ThetaLocDecl& target = *locs[edge->getTarget()]; + + std::vector stmts; + + if (edge->getGuard() != BoolLiteralExpr::True(edge->getGuard()->getContext())) { + stmts.push_back(ThetaStmt::Assume(edge->getGuard())); + } + + if (auto assignEdge = dyn_cast(edge)) { + for (const auto& assignment : *assignEdge) { + auto lhsName = find_var(assignment.getVariable())->getName(); // TODO isn't this canonizeName()? + + if (llvm::isa(assignment.getValue())) { + stmts.push_back(ThetaStmt::Havoc(lhsName)); + } else { + stmts.push_back(ThetaStmt::Assign(lhsName, assignment.getValue())); + } + } + } else if (auto callEdge = dyn_cast(edge)) { + assert(callEdge->getNumOutputs() <= 1 && "calls should have at most one output"); + + llvm::SmallVector inputs; + for (const auto& input : callEdge->inputs()) { + auto lhsName = input.getVariable()->getName(); + + auto rhs = input.getValue(); + static int paramCounter = 0; + // Create a new variable because XCFA needs it. + auto newVarName = "call_param_tmp_" + llvm::Twine(paramCounter++); + + auto variable = cfa->createLocal(newVarName.str(), rhs->getType()); + auto name = validName(variable->getName(), isValidVarName); + auto type = typeName(variable->getType()); + + nameTrace.variables[name] = variable; + vars.try_emplace(variable, std::make_unique(name, type)); + + // initialize the new variable + stmts.push_back(ThetaStmt::Assign(name, rhs)); + inputs.push_back(VariableAssignment(input.getVariable(), variable->getRefExpr())); + } + std::optional result = {}; + if (callEdge->getNumOutputs() == 1) { + result = callEdge->outputs().begin()->getVariable(); + } + stmts.push_back(ThetaStmt::Call(callEdge->getCalledAutomaton()->getName(), inputs, result)); + } + + edges.emplace_back(std::make_unique(source, target, std::move(stmts))); + } + + const auto INDENT = " "; + const auto INDENT2 = " "; + + auto canonizeName = [&vars, &globals](Variable* variable) -> std::string { + auto it = globals.find(variable); + if (it != globals.end()) { + return it->getSecond()->getName(); + } + + if (vars.count(variable) == 0) { + return variable->getName(); + } + return vars[variable]->getName(); + }; + + if (cfa == mSystem.getMainAutomaton()) { + os << "main "; + } + // TODO main -> xmain temp solution + os << "procedure x" << cfa->getName() << "("; + bool first = true; + for (auto& input : cfa->inputs()) { + if (first) { + first = false; + } else { + os << ", "; + } + auto name = vars[&input]->getName(); + auto type = vars[&input]->getType(); + + os << name << " : " << type; + } + os << ") {\n"; + for (auto& variable : cfa->locals()) { + os << INDENT; + vars[&variable]->print(os); + os << "\n"; + } + + for (Location* loc : cfa->nodes()) { + os << INDENT; + locs[loc]->print(os); + os << "\n"; + } + + for (auto& edge : edges) { + os << INDENT << edge->mSource.mName << " -> " << edge->mTarget.mName << " {\n"; + for (auto& stmt : edge->mStmts) { + os << INDENT2; + PrintVisitor visitor(os, canonizeName); + std::visit(visitor, stmt.mContent); + os << "\n"; + } + os << INDENT << "}\n"; + os << "\n"; + } + + os << "}\n"; + os.flush(); +} diff --git a/tools/gazer-theta/lib/ThetaCfaProcedureGenerator.h b/tools/gazer-theta/lib/ThetaCfaProcedureGenerator.h new file mode 100644 index 00000000..50be0378 --- /dev/null +++ b/tools/gazer-theta/lib/ThetaCfaProcedureGenerator.h @@ -0,0 +1,49 @@ +//==-------------------------------------------------------------*- C++ -*--==// +// +// Copyright 2020 Contributors to the Gazer project +// +// Licensed under the Apache License, Version 2.0 (the "License"); +// you may not use this file except in compliance with the License. +// You may obtain a copy of the License at +// +// http://www.apache.org/licenses/LICENSE-2.0 +// +// Unless required by applicable law or agreed to in writing, software +// distributed under the License is distributed on an "AS IS" BASIS, +// WITHOUT WARRANTIES OR CONDITIONS OF ANY KIND, either express or implied. +// See the License for the specific language governing permissions and +// limitations under the License. +// +//===----------------------------------------------------------------------===// +#ifndef GAZER_THETACFAPROCEDUREGENERATOR_H +#define GAZER_THETACFAPROCEDUREGENERATOR_H + +#include "ThetaUtil.h" + +#include +#include +#include + +namespace gazer { + +class ThetaCfaProcedureGenerator +{ +public: + ThetaCfaProcedureGenerator( + AutomataSystem& system, + Cfa* cfa, + const llvm::DenseMap>& globals) + : mSystem(system), cfa(cfa), mGlobals(globals) + {} + + void writeCFA(llvm::raw_ostream& os, gazer::theta::ThetaNameMapping& nameTrace); + +private: + AutomataSystem& mSystem; + Cfa* cfa; + const llvm::DenseMap>& mGlobals; +}; + +} // namespace gazer + +#endif // GAZER_THETACFAPROCEDUREGENERATOR_H diff --git a/tools/gazer-theta/lib/ThetaUtil.cpp b/tools/gazer-theta/lib/ThetaUtil.cpp new file mode 100644 index 00000000..49fdad67 --- /dev/null +++ b/tools/gazer-theta/lib/ThetaUtil.cpp @@ -0,0 +1,62 @@ +//==-------------------------------------------------------------*- C++ -*--==// +// +// Copyright 2020 Contributors to the Gazer project +// +// Licensed under the Apache License, Version 2.0 (the "License"); +// you may not use this file except in compliance with the License. +// You may obtain a copy of the License at +// +// http://www.apache.org/licenses/LICENSE-2.0 +// +// Unless required by applicable law or agreed to in writing, software +// distributed under the License is distributed on an "AS IS" BASIS, +// WITHOUT WARRANTIES OR CONDITIONS OF ANY KIND, either express or implied. +// See the License for the specific language governing permissions and +// limitations under the License. +// +//===----------------------------------------------------------------------===// +#include "ThetaUtil.h" +#include + +void gazer::theta::ThetaStmt::print(llvm::raw_ostream& os) const +{ + PrintVisitor visitor(os); + + std::visit(visitor, mContent); +} + +void gazer::theta::ThetaEdgeDecl::print(llvm::raw_ostream& os) const +{ + os << mSource.mName << " -> " << mTarget.mName << " {\n"; + for (const auto& stmt : mStmts) { + os << " "; + stmt.print(os); + os << "\n"; + } + os << "}\n"; +} + +constexpr std::array ThetaKeywords = { + "main", "process", "var", "loc", + "assume", "init", "final", "error", + "return", "havoc", "bool", "int", "rat", + "if", "then", "else", "iff", "imply", + "forall", "exists", "or", "and", "not", + "mod", "rem", "true", "false" +}; + +std::string gazer::theta::validName(std::string name, std::function isUnique) { + static int tmpCount = 0; + name = std::regex_replace(name, std::regex("[^a-zA-Z0-9_]"), "_"); + + if (std::find(ThetaKeywords.begin(), ThetaKeywords.end(), name) != ThetaKeywords.end()) { + name += "_gazer"; + } + + while (!isUnique(name)) { + llvm::Twine nextTry = name + llvm::Twine(tmpCount++); + name = nextTry.str(); + } + + return name; +} diff --git a/tools/gazer-theta/lib/ThetaUtil.h b/tools/gazer-theta/lib/ThetaUtil.h new file mode 100644 index 00000000..fac01d15 --- /dev/null +++ b/tools/gazer-theta/lib/ThetaUtil.h @@ -0,0 +1,234 @@ +//==-------------------------------------------------------------*- C++ -*--==// +// +// Copyright 2020 Contributors to the Gazer project +// +// Licensed under the Apache License, Version 2.0 (the "License"); +// you may not use this file except in compliance with the License. +// You may obtain a copy of the License at +// +// http://www.apache.org/licenses/LICENSE-2.0 +// +// Unless required by applicable law or agreed to in writing, software +// distributed under the License is distributed on an "AS IS" BASIS, +// WITHOUT WARRANTIES OR CONDITIONS OF ANY KIND, either express or implied. +// See the License for the specific language governing permissions and +// limitations under the License. +// +//===----------------------------------------------------------------------===// +#ifndef GAZER_THETAUTIL_H +#define GAZER_THETAUTIL_H + +#include "gazer/Automaton/Cfa.h" +#include "gazer/Core/LiteralExpr.h" +#include +#include +#include +#include + +namespace gazer::theta { + +std::string printThetaExpr(const ExprPtr& expr); + +std::string printThetaExpr(const ExprPtr& expr, std::function variableNames); + +struct ThetaAst +{ + virtual void print(llvm::raw_ostream& os) const = 0; + + virtual ~ThetaAst() = default; +}; + +struct ThetaLocDecl : ThetaAst +{ + enum Flag + { + Loc_State, + Loc_Init, + Loc_Final, + Loc_Error, + }; + + ThetaLocDecl(std::string name, Flag flag = Loc_State) + : mName(name), mFlag(flag) + {} + + void print(llvm::raw_ostream& os) const override + { + switch (mFlag) { + case Loc_Init: os << "init "; break; + case Loc_Final: os << "final "; break; + case Loc_Error: os << "error "; break; + default: + break; + } + + os << "loc " << mName; + } + + std::string mName; + Flag mFlag; +}; + +struct ThetaStmt : ThetaAst +{ + using callType = std::tuple, + std::optional>; + using VariantTy = std::variant, std::string, callType>; + + /* implicit */ ThetaStmt(VariantTy content) + : mContent(content) + {} + + static ThetaStmt Assume(gazer::ExprPtr expr) + { + assert(expr->getType().isBoolType()); + + return VariantTy{expr}; + } + + static ThetaStmt Assign(std::string variableName, gazer::ExprPtr value) + { + assert(!llvm::isa(value) + && "Cannot assign an undef value to a variable." + "Use ::Havoc() to represent a nondetermistic value assignment." + ); + + std::pair pair = { variableName, value }; + + return VariantTy{pair}; + } + + static ThetaStmt Havoc(std::string variable) + { + return VariantTy{variable}; + } + + void print(llvm::raw_ostream& os) const override; + + VariantTy mContent; + static ThetaStmt Call( + llvm::StringRef name, + llvm::SmallVector vector, + std::optional result) { + return VariantTy{callType{name, vector, result}}; + } +}; + +struct ThetaEdgeDecl : ThetaAst +{ + ThetaEdgeDecl(ThetaLocDecl& source, ThetaLocDecl& target, std::vector stmts) + : mSource(source), mTarget(target), mStmts(std::move(stmts)) + {} + + void print(llvm::raw_ostream& os) const override; + + ThetaLocDecl& mSource; + ThetaLocDecl& mTarget; + std::vector mStmts; +}; + +class ThetaVarDecl : ThetaAst +{ +public: + ThetaVarDecl(std::string name, std::string type) + : mName(name), mType(type) + {} + + llvm::StringRef getName() { return mName; } + + llvm::StringRef getType() { return mType; } + + void print(llvm::raw_ostream& os) const override + { + os << "var " << mName << " : " << mType; + } + +private: + std::string mName; + std::string mType; +}; + +struct PrintVisitor +{ + llvm::raw_ostream& mOS; + std::function mCanonizeName; + + PrintVisitor(llvm::raw_ostream& os, std::function canonizeName) + : mOS(os), mCanonizeName(std::move(canonizeName)) + {} + + explicit PrintVisitor(llvm::raw_ostream& os) + : mOS(os), mCanonizeName([](gazer::Variable* v) {return v->getName();}) + {} + + void operator()(const gazer::ExprPtr& expr) { + mOS << "assume "; + mOS << printThetaExpr(expr, mCanonizeName); + } + + void operator()(const std::pair& assign) { + mOS << assign.first << " := "; + mOS << printThetaExpr(assign.second, mCanonizeName); + } + + void operator()(const std::string& variable) { + mOS << "havoc " << variable; + } + + void operator()(const gazer::theta::ThetaStmt::callType& call) { + auto result = std::get<2>(call); + auto prefix = result.has_value() ? mCanonizeName(result.value()) + llvm::Twine(" := ") : ""; + + // TODO main -> xmain temp solution + mOS << prefix << "call x" << std::get<0>(call) << "("; + bool first = true; + for (const auto& param : std::get<1>(call)) { + if (first) { + first = false; + } else { + mOS << ", "; + } + if (auto var = llvm::dyn_cast(param.getValue())) { + mOS << mCanonizeName(&(var->getVariable())); + } else { + llvm_unreachable("parameter should be a variable reference"); + } + } + mOS << ")"; + } +}; + +std::string validName(std::string name, std::function isUnique); + +static std::string typeName(Type& type) +{ + switch (type.getTypeID()) { + case Type::IntTypeID: + return "int"; + case Type::RealTypeID: + return "rat"; + case Type::BoolTypeID: + return "bool"; + case Type::ArrayTypeID: { + auto& arrTy = llvm::cast(type); + return "[" + typeName(arrTy.getIndexType()) + "] -> " + typeName(arrTy.getElementType()); + } + default: + llvm_unreachable("Types which are unsupported by theta should have been eliminated earlier!"); + } +} + +struct ThetaNameMapping +{ + llvm::StringMap locations; + llvm::StringMap variables; + Location* errorLocation; + Variable* errorFieldVariable; + llvm::DenseMap inlinedLocations; + llvm::DenseMap inlinedVariables; +}; + +} // namespace gazer::theta + +#endif // GAZER_THETAUTIL_H From 712f04ca790f6eb779adc36f155a0f7f06d6da85 Mon Sep 17 00:00:00 2001 From: radl97 Date: Mon, 10 Aug 2020 13:15:06 +0200 Subject: [PATCH 12/47] Rework theta Call stmt --- .../lib/ThetaCfaProcedureGenerator.cpp | 11 +++++------ tools/gazer-theta/lib/ThetaUtil.h | 18 +++++++----------- 2 files changed, 12 insertions(+), 17 deletions(-) diff --git a/tools/gazer-theta/lib/ThetaCfaProcedureGenerator.cpp b/tools/gazer-theta/lib/ThetaCfaProcedureGenerator.cpp index 207d7320..8c69a0ac 100644 --- a/tools/gazer-theta/lib/ThetaCfaProcedureGenerator.cpp +++ b/tools/gazer-theta/lib/ThetaCfaProcedureGenerator.cpp @@ -119,10 +119,9 @@ void gazer::ThetaCfaProcedureGenerator::writeCFA(llvm::raw_ostream& os, gazer::t } else if (auto callEdge = dyn_cast(edge)) { assert(callEdge->getNumOutputs() <= 1 && "calls should have at most one output"); - llvm::SmallVector inputs; + llvm::SmallVector inputs; for (const auto& input : callEdge->inputs()) { - auto lhsName = input.getVariable()->getName(); - + // we do not use the input variable itself, only the value it's assigned to auto rhs = input.getValue(); static int paramCounter = 0; // Create a new variable because XCFA needs it. @@ -137,11 +136,11 @@ void gazer::ThetaCfaProcedureGenerator::writeCFA(llvm::raw_ostream& os, gazer::t // initialize the new variable stmts.push_back(ThetaStmt::Assign(name, rhs)); - inputs.push_back(VariableAssignment(input.getVariable(), variable->getRefExpr())); + inputs.push_back(name); } - std::optional result = {}; + std::optional result = {}; if (callEdge->getNumOutputs() == 1) { - result = callEdge->outputs().begin()->getVariable(); + result = find_var(callEdge->outputs().begin()->getVariable())->getName(); } stmts.push_back(ThetaStmt::Call(callEdge->getCalledAutomaton()->getName(), inputs, result)); } diff --git a/tools/gazer-theta/lib/ThetaUtil.h b/tools/gazer-theta/lib/ThetaUtil.h index fac01d15..9ed1bbdf 100644 --- a/tools/gazer-theta/lib/ThetaUtil.h +++ b/tools/gazer-theta/lib/ThetaUtil.h @@ -71,9 +71,9 @@ struct ThetaLocDecl : ThetaAst struct ThetaStmt : ThetaAst { - using callType = std::tuple, - std::optional>; + using callType = std::tuple, // variables + std::optional>; // return variable using VariantTy = std::variant, std::string, callType>; /* implicit */ ThetaStmt(VariantTy content) @@ -109,8 +109,8 @@ struct ThetaStmt : ThetaAst VariantTy mContent; static ThetaStmt Call( llvm::StringRef name, - llvm::SmallVector vector, - std::optional result) { + llvm::SmallVector vector, + std::optional result) { return VariantTy{callType{name, vector, result}}; } }; @@ -178,7 +178,7 @@ struct PrintVisitor void operator()(const gazer::theta::ThetaStmt::callType& call) { auto result = std::get<2>(call); - auto prefix = result.has_value() ? mCanonizeName(result.value()) + llvm::Twine(" := ") : ""; + auto prefix = result.has_value() ? result.value() + llvm::Twine(" := ") : ""; // TODO main -> xmain temp solution mOS << prefix << "call x" << std::get<0>(call) << "("; @@ -189,11 +189,7 @@ struct PrintVisitor } else { mOS << ", "; } - if (auto var = llvm::dyn_cast(param.getValue())) { - mOS << mCanonizeName(&(var->getVariable())); - } else { - llvm_unreachable("parameter should be a variable reference"); - } + mOS << param; } mOS << ")"; } From f9b2d64ed0e5a195ab7a5751ce509138b0d5aea5 Mon Sep 17 00:00:00 2001 From: radl97 Date: Mon, 10 Aug 2020 14:50:14 +0200 Subject: [PATCH 13/47] Temporary solutions for intrinsics breaking SimpleMemoryModel --- src/LLVM/Memory/SimpleMemoryModel.cpp | 20 ++++++++++++++++---- 1 file changed, 16 insertions(+), 4 deletions(-) diff --git a/src/LLVM/Memory/SimpleMemoryModel.cpp b/src/LLVM/Memory/SimpleMemoryModel.cpp index 44365c0f..4bac1acd 100644 --- a/src/LLVM/Memory/SimpleMemoryModel.cpp +++ b/src/LLVM/Memory/SimpleMemoryModel.cpp @@ -82,9 +82,20 @@ class SimpleMemoryInstructionHandler : public MemoryInstructionHandler, public M ExprPtr handlePointerCast( const llvm::CastInst& cast, const ExprPtr& origPtr) override { - llvm_unreachable("Pointer casts are not supported"); - // maybe this will do? - // return origPtr; + // TODO this is a fake implementation + // mostly for the gazer intrinsics that use pointer casts + // if a real cast would take place, this would make no sense at all. + // probably the intrinsics themselves would brake if tracing would work... + auto& goalType = types.get(cast.getDestTy()); + if (cast.getDestTy()->isPointerTy()) { + return ExprBuilder(getContext()).BvLit8(0); + } + switch(goalType.getTypeID()) { + case gazer::Type::BoolTypeID: return ExprBuilder(getContext()).False(); + case gazer::Type::IntTypeID: return ExprBuilder(getContext()).IntLit(0); + case gazer::Type::BvTypeID: return ExprBuilder(getContext()).BvLit(0, llvm::cast(goalType).getWidth()); + } + llvm_unreachable("Unsupported pointer cast"); } /// Represents a pointer arithmetic instruction. @@ -169,7 +180,8 @@ class SimpleMemoryInstructionHandler : public MemoryInstructionHandler, public M ~SimpleMemoryInstructionHandler() override = default; gazer::Type& handlePointerType(const llvm::PointerType* type) override { - llvm_unreachable("Pointers and arrays are not supported right now"); + // TODO this is a fake implementation, and I'm not quite sure what are the dependencies + return ExprBuilder(getContext()).BvLit8(0)->getType(); } /// Translates types of constant arrays and initializers. From 37c5190008a181b97ef85fcf3a808a1d880739f1 Mon Sep 17 00:00:00 2001 From: rl555 Date: Wed, 12 Aug 2020 18:19:20 +0200 Subject: [PATCH 14/47] Add behaviour for a function as a PoC --- .../AnnotateSpecialFunctions.h | 43 +++++++++ src/LLVM/CMakeLists.txt | 1 + .../AnnotateSpecialFunctions.cpp | 93 +++++++++++++++++++ src/LLVM/LLVMFrontend.cpp | 4 + 4 files changed, 141 insertions(+) create mode 100644 include/gazer/LLVM/Instrumentation/AnnotateSpecialFunctions.h create mode 100644 src/LLVM/Instrumentation/AnnotateSpecialFunctions.cpp diff --git a/include/gazer/LLVM/Instrumentation/AnnotateSpecialFunctions.h b/include/gazer/LLVM/Instrumentation/AnnotateSpecialFunctions.h new file mode 100644 index 00000000..fae48153 --- /dev/null +++ b/include/gazer/LLVM/Instrumentation/AnnotateSpecialFunctions.h @@ -0,0 +1,43 @@ +//==-------------------------------------------------------------*- C++ -*--==// +// +// Copyright 2019 Contributors to the Gazer project +// +// Licensed under the Apache License, Version 2.0 (the "License"); +// you may not use this file except in compliance with the License. +// You may obtain a copy of the License at +// +// http://www.apache.org/licenses/LICENSE-2.0 +// +// Unless required by applicable law or agreed to in writing, software +// distributed under the License is distributed on an "AS IS" BASIS, +// WITHOUT WARRANTIES OR CONDITIONS OF ANY KIND, either express or implied. +// See the License for the specific language governing permissions and +// limitations under the License. +// +//===----------------------------------------------------------------------===// +/// +/// Processes special function behaviours +/// Currently for a given function name, asserts that the function is pure, +/// And transforms as such. +/// +/// Example: +/// %1 := call @FixResult() +/// %2 := load <>* %1 +/// +/// will become something like this: +/// +/// @_FixResult = internal global <> undef +/// %2 := load <>* @_FixResult +/// +//===----------------------------------------------------------------------===// + +#ifndef SRC_LLVM_INSTRUMENTATION_ANNOTATESPECIALFUNCTIONS_H_ +#define SRC_LLVM_INSTRUMENTATION_ANNOTATESPECIALFUNCTIONS_H_ + +#include + +namespace gazer { +llvm::Pass* createAnnotateSpecialFunctionsPass(); +} + +#endif /* SRC_LLVM_INSTRUMENTATION_ANNOTATESPECIALFUNCTIONS_H_ */ diff --git a/src/LLVM/CMakeLists.txt b/src/LLVM/CMakeLists.txt index a69608e0..8bee535e 100644 --- a/src/LLVM/CMakeLists.txt +++ b/src/LLVM/CMakeLists.txt @@ -6,6 +6,7 @@ set(SOURCE_FILES Transform/BackwardSlicer.cpp Transform/Inline.cpp Transform/TransformUtils.cpp + Instrumentation/AnnotateSpecialFunctions.cpp Instrumentation/MarkFunctionEntries.cpp Instrumentation/Check.cpp Instrumentation/DefaultChecks.cpp diff --git a/src/LLVM/Instrumentation/AnnotateSpecialFunctions.cpp b/src/LLVM/Instrumentation/AnnotateSpecialFunctions.cpp new file mode 100644 index 00000000..ca40e98e --- /dev/null +++ b/src/LLVM/Instrumentation/AnnotateSpecialFunctions.cpp @@ -0,0 +1,93 @@ +//==-------------------------------------------------------------*- C++ -*--==// +// +// Copyright 2019 Contributors to the Gazer project +// +// Licensed under the Apache License, Version 2.0 (the "License"); +// you may not use this file except in compliance with the License. +// You may obtain a copy of the License at +// +// http://www.apache.org/licenses/LICENSE-2.0 +// +// Unless required by applicable law or agreed to in writing, software +// distributed under the License is distributed on an "AS IS" BASIS, +// WITHOUT WARRANTIES OR CONDITIONS OF ANY KIND, either express or implied. +// See the License for the specific language governing permissions and +// limitations under the License. +// +//===----------------------------------------------------------------------===// + +#include "gazer/LLVM/Instrumentation/AnnotateSpecialFunctions.h" +#include "llvm/Support/Casting.h" +#include "llvm/IR/Instructions.h" +#include "llvm/IR/Module.h" +//#include "llvm/Support/raw_ostream.h" +#include "llvm/Support/Debug.h" + +using namespace llvm; + +namespace { +class AnnotateSpecialFunctionsPass : public ModulePass { +public: + AnnotateSpecialFunctionsPass() : ModulePass(ID) { + + } + + bool runOnModule(Module& m) override { + bool res = false; + SmallVector toProcess; + for (auto& f : m.functions()) { + for (auto& bb: f) { + for (auto& inst : bb) { + if (auto* callInst = dyn_cast(&inst)) { + toProcess.push_back(callInst); + } + } + } + } + for (auto* callInst : toProcess) { + res |= processInstruction(m, *callInst); + } + return res; + } + +public: + static char ID; + +private: + bool processInstruction(Module& m, CallInst& inst) { + // known function + if (inst.getCalledFunction()->getName().startswith("FixPtr")) { + auto varName = ("gazer." + inst.getCalledFunction()->getName()).str(); + // TODO assert definition is like "type* FixPtr()" + auto resType = inst.getCalledFunction()->getReturnType()->getPointerElementType(); + auto var = m.getOrInsertGlobal(varName, resType, + [&varName, &m, &resType]() -> GlobalVariable* { + return new GlobalVariable(m, resType, false, + GlobalVariable::LinkageTypes::InternalLinkage, + UndefValue::get(resType), + varName); + }); + inst.replaceAllUsesWith(var); + inst.dropAllReferences(); + inst.eraseFromParent(); + return true; + } + // known intrinsics + if (inst.getCalledFunction()->getName().startswith("gazer.") || + inst.getCalledFunction()->getName().startswith("llvm.")) { + return false; + } + llvm::errs() << "WARNING: unknown function " << *(inst.getCalledFunction()) << "\n"; + return false; + } + +}; +} + +char AnnotateSpecialFunctionsPass::ID; + +static RegisterPass X("annot-spec-functions", "annot-spec-functions", false, false); + +llvm::Pass* gazer::createAnnotateSpecialFunctionsPass() { + return new AnnotateSpecialFunctionsPass(); +} diff --git a/src/LLVM/LLVMFrontend.cpp b/src/LLVM/LLVMFrontend.cpp index b3debc1f..5ce1a6f0 100644 --- a/src/LLVM/LLVMFrontend.cpp +++ b/src/LLVM/LLVMFrontend.cpp @@ -17,6 +17,7 @@ //===----------------------------------------------------------------------===// #include "gazer/LLVM/LLVMFrontend.h" #include "gazer/LLVM/Instrumentation/DefaultChecks.h" +#include "gazer/LLVM/Instrumentation/AnnotateSpecialFunctions.h" #include "gazer/LLVM/InstrumentationPasses.h" #include "gazer/LLVM/Transform/Passes.h" #include "gazer/LLVM/Automaton/ModuleToAutomata.h" @@ -155,6 +156,9 @@ void LLVMFrontend::registerVerificationPipeline() // Unify function exit nodes mPassManager.add(llvm::createUnifyFunctionExitNodesPass()); + // Unify function exit nodes + mPassManager.add(gazer::createAnnotateSpecialFunctionsPass()); + // Run assertion lifting. if (mSettings.liftAsserts) { mPassManager.add(new llvm::CallGraphWrapperPass()); From b1b982825c094fd5cfff6b8db7c924b0f24fae35 Mon Sep 17 00:00:00 2001 From: rl555 Date: Wed, 12 Aug 2020 18:22:48 +0200 Subject: [PATCH 15/47] Fix last character not flushed when writing XCFA --- tools/gazer-theta/lib/ThetaCfaGenerator.cpp | 1 + tools/gazer-theta/lib/ThetaCfaProcedureGenerator.cpp | 1 - 2 files changed, 1 insertion(+), 1 deletion(-) diff --git a/tools/gazer-theta/lib/ThetaCfaGenerator.cpp b/tools/gazer-theta/lib/ThetaCfaGenerator.cpp index 7816507e..7ef14914 100644 --- a/tools/gazer-theta/lib/ThetaCfaGenerator.cpp +++ b/tools/gazer-theta/lib/ThetaCfaGenerator.cpp @@ -57,4 +57,5 @@ void ThetaCfaGenerator::write(llvm::raw_ostream& os, ThetaNameMapping& nameTrace ThetaCfaProcedureGenerator(mSystem, &cfa, globals).writeCFA(os, nameTrace); } os << "}\n"; + os.flush(); } diff --git a/tools/gazer-theta/lib/ThetaCfaProcedureGenerator.cpp b/tools/gazer-theta/lib/ThetaCfaProcedureGenerator.cpp index 8c69a0ac..91854ae4 100644 --- a/tools/gazer-theta/lib/ThetaCfaProcedureGenerator.cpp +++ b/tools/gazer-theta/lib/ThetaCfaProcedureGenerator.cpp @@ -206,5 +206,4 @@ void gazer::ThetaCfaProcedureGenerator::writeCFA(llvm::raw_ostream& os, gazer::t } os << "}\n"; - os.flush(); } From 2cd86a29128c24d2efe1d745a32bce90e99f20c1 Mon Sep 17 00:00:00 2001 From: rl555 Date: Wed, 12 Aug 2020 18:24:37 +0200 Subject: [PATCH 16/47] Add test for simple API Contract --- api_contract_test.c | 21 +++++++++++++++++++++ 1 file changed, 21 insertions(+) create mode 100644 api_contract_test.c diff --git a/api_contract_test.c b/api_contract_test.c new file mode 100644 index 00000000..31dfa8a3 --- /dev/null +++ b/api_contract_test.c @@ -0,0 +1,21 @@ +#include +// "FixPtr.*" function has hard-coded property that it returns a constant pointer without side-effects +int* FixPtr_First(void); +int* FixPtr_Second(void); +void undef_call(void); + +int main() { + *FixPtr_First() = 5; + + // another instance is returned from another function call + *FixPtr_Second() = 3; + + int x = *FixPtr_First(); + + assert(x == 5); + + // WARNING: unknown function undef_call(). + // Side-effects might cause unsound verification. + undef_call(); + return 0; +} From c567e688a828d35a23b705bca588572f790b3c7a Mon Sep 17 00:00:00 2001 From: rl555 Date: Tue, 25 Aug 2020 11:18:55 +0200 Subject: [PATCH 17/47] Add Mutex Enter/Exit test --- api_contract_test.c | 10 +- .../SimplifySpecialFunctions.h | 33 +++++ .../SimplifySpecialFunctions.cpp | 122 ++++++++++++++++++ 3 files changed, 164 insertions(+), 1 deletion(-) create mode 100644 include/gazer/LLVM/Instrumentation/SimplifySpecialFunctions.h create mode 100644 src/LLVM/Instrumentation/SimplifySpecialFunctions.cpp diff --git a/api_contract_test.c b/api_contract_test.c index 31dfa8a3..c50605d4 100644 --- a/api_contract_test.c +++ b/api_contract_test.c @@ -4,7 +4,7 @@ int* FixPtr_First(void); int* FixPtr_Second(void); void undef_call(void); -int main() { +int main2() { *FixPtr_First() = 5; // another instance is returned from another function call @@ -19,3 +19,11 @@ int main() { undef_call(); return 0; } + +void Enter1(void) __attribute__((used)); +void Exit1(void) __attribute__((used)); + +int main() { + Enter1(); + Exit1(); +} diff --git a/include/gazer/LLVM/Instrumentation/SimplifySpecialFunctions.h b/include/gazer/LLVM/Instrumentation/SimplifySpecialFunctions.h new file mode 100644 index 00000000..16d764cc --- /dev/null +++ b/include/gazer/LLVM/Instrumentation/SimplifySpecialFunctions.h @@ -0,0 +1,33 @@ +/** + * @file SimplifySpecialFunctions.h + * + * @brief <> + * + * << Write the detailed description of the file here. >> + * + * @author laszlo.radnai + * @date 2020.08.19. + * + * @copyright 2020 thyssenkrupp Components Technology Hungary Ltd. + */ + +#ifndef SRC_LLVM_INSTRUMENTATION_SIMPLIFYSPECIALFUNCTIONS_H_ +#define SRC_LLVM_INSTRUMENTATION_SIMPLIFYSPECIALFUNCTIONS_H_ + +#include + +namespace llvm { +class Pass; +} + +namespace gazer { +/** + * Simplifies special known, but not implemented functions. + * 1) When certain conditions are met for a function, + * replaces function call with a pre-defined value + * @return + */ +llvm::Pass* createSimplifySpecialFunctionsPass(); +} + +#endif /* SRC_LLVM_INSTRUMENTATION_SIMPLIFYSPECIALFUNCTIONS_H_ */ diff --git a/src/LLVM/Instrumentation/SimplifySpecialFunctions.cpp b/src/LLVM/Instrumentation/SimplifySpecialFunctions.cpp new file mode 100644 index 00000000..2b0302b4 --- /dev/null +++ b/src/LLVM/Instrumentation/SimplifySpecialFunctions.cpp @@ -0,0 +1,122 @@ +//==-------------------------------------------------------------*- C++ -*--==// +// +// Copyright 2019 Contributors to the Gazer project +// +// Licensed under the Apache License, Version 2.0 (the "License"); +// you may not use this file except in compliance with the License. +// You may obtain a copy of the License at +// +// http://www.apache.org/licenses/LICENSE-2.0 +// +// Unless required by applicable law or agreed to in writing, software +// distributed under the License is distributed on an "AS IS" BASIS, +// WITHOUT WARRANTIES OR CONDITIONS OF ANY KIND, either express or implied. +// See the License for the specific language governing permissions and +// limitations under the License. +// +//===----------------------------------------------------------------------===// +/// Simplifies special functions +/// If a function: +/// return value is a pointer +/// the return pointer does not alias +/// has no arguments +/// does not access memory, +/// and speculatable +/// it can be replaced with a global variable access. + +#include "gazer/LLVM/Instrumentation/SimplifySpecialFunctions.h" +#include "gazer/LLVM/Instrumentation/AnnotateSpecialFunctions.h" +#include "gazer/LLVM/Instrumentation/Check.h" + +#include "llvm/Pass.h" +#include "llvm/IR/InstIterator.h" +#include "llvm/IR/Module.h" + +using namespace gazer; +using namespace llvm; + +namespace { + +class SimplifySpecialFunctions : public FunctionPass { + static char ID; +public: + + SimplifySpecialFunctions() : FunctionPass(ID) {} + + /// for a specific (function;variableName) pair, returns a unique global variable. + static GlobalVariable* getOrInsertUniqueGlobal(Module& m, + Function* functionDecl, + Type* type, + StringRef variableName) { + auto fullVariableName = ("gazer.global." + functionDecl->getName() + "." + variableName).str(); + auto var = m.getOrInsertGlobal(fullVariableName, type, + [&fullVariableName, &m, &type]() -> GlobalVariable* { + return new GlobalVariable(m, type, false, + GlobalVariable::LinkageTypes::InternalLinkage, + UndefValue::get(type), + fullVariableName); + }); + return static_cast(var); + } + + bool fixPtr(CallInst* inst) { + Function* f = inst->getCalledFunction(); + // has no arguments + if (inst->getFunctionType()->getFunctionNumParams() != 0) { + return false; + } + // returns a pointer + if (!inst->getFunctionType()->getReturnType()->isPointerTy()) { + return false; + } + // the result does not alias (mem region accessible only from this call) + if (!f->returnDoesNotAlias()) { + return false; + } + // the function does not access memory + if (!f->doesNotAccessMemory()) { + return false; + } + // the function is speculatable (~no side-effects) + if (!f->isSpeculatable()) { + return false; + } + auto resType = inst->getFunctionType()->getReturnType()->getPointerElementType(); + auto var = getOrInsertUniqueGlobal(*(f->getParent()), inst->getCalledFunction(), resType, ""); + inst->replaceAllUsesWith(var); + inst->dropAllReferences(); + inst->eraseFromParent(); + return true; + } + + /// Marks the given function's instructions with required + /// pre- and postconditions. + bool runOnFunction(llvm::Function& function) override { + llvm::SmallVector to_process; + for (auto& inst : instructions(function)) { + if (auto* callInst = dyn_cast(&inst)) { + to_process.push_back(callInst); + } + } + bool changed = false; + for (CallInst* callInst : to_process) { + if (fixPtr(callInst)) { + changed = true; + continue; + } + } + return changed; + } + + void getAnalysisUsage(AnalysisUsage &Info) const override { + Info.addRequiredID(getAnnotateSpecialFunctionsID()); + } +}; + +char SimplifySpecialFunctions::ID; + +} + +llvm::Pass* gazer::createSimplifySpecialFunctionsPass() { + return new SimplifySpecialFunctions(); +} From 620efeabe66d1eaedb45511e3883283e3416f182 Mon Sep 17 00:00:00 2001 From: rl555 Date: Tue, 25 Aug 2020 11:25:42 +0200 Subject: [PATCH 18/47] Small fixes --- include/gazer/Automaton/Cfa.h | 2 +- include/gazer/LLVM/Automaton/SpecialFunctions.h | 3 +-- 2 files changed, 2 insertions(+), 3 deletions(-) diff --git a/include/gazer/Automaton/Cfa.h b/include/gazer/Automaton/Cfa.h index e0951761..f058d07c 100644 --- a/include/gazer/Automaton/Cfa.h +++ b/include/gazer/Automaton/Cfa.h @@ -346,7 +346,7 @@ class AutomataSystem final AutomataSystem& operator=(const AutomataSystem&) = delete; Variable* createGlobal( - std::basic_string, std::allocator> basicString, + std::string basicString, Type& type); public: diff --git a/include/gazer/LLVM/Automaton/SpecialFunctions.h b/include/gazer/LLVM/Automaton/SpecialFunctions.h index fdc2f624..6e71211a 100644 --- a/include/gazer/LLVM/Automaton/SpecialFunctions.h +++ b/include/gazer/LLVM/Automaton/SpecialFunctions.h @@ -71,7 +71,6 @@ class SpecialFunctions // Some handlers for common cases public: static void handleAssume(llvm::ImmutableCallSite cs, llvm2cfa::GenerationStepExtensionPoint& ep); - private: llvm::StringMap mHandlers; @@ -79,4 +78,4 @@ class SpecialFunctions } // namespace gazer -#endif \ No newline at end of file +#endif From 9cf5cfc4b3f9a8e37fcc61c0277d56f938d653d7 Mon Sep 17 00:00:00 2001 From: rl555 Date: Tue, 25 Aug 2020 11:26:58 +0200 Subject: [PATCH 19/47] Implement mutex Enter/Exit check --- .../LLVM/Instrumentation/DefaultChecks.h | 6 +- src/LLVM/Instrumentation/DefaultChecks.cpp | 197 ++++++++++++++++++ 2 files changed, 202 insertions(+), 1 deletion(-) diff --git a/include/gazer/LLVM/Instrumentation/DefaultChecks.h b/include/gazer/LLVM/Instrumentation/DefaultChecks.h index fbb07306..a69f7bae 100644 --- a/include/gazer/LLVM/Instrumentation/DefaultChecks.h +++ b/include/gazer/LLVM/Instrumentation/DefaultChecks.h @@ -31,4 +31,8 @@ namespace gazer::checks /// in an over- or underflow. std::unique_ptr createSignedIntegerOverflowCheck(ClangOptions& options); -} // end namespace gazer::checks \ No newline at end of file + /// This check fails if a non-reentrant mutex has bad usage. + /// TODO initialization and clean-up are a problem. + std::unique_ptr createMutexCheck(ClangOptions& options); + +} // end namespace gazer::checks diff --git a/src/LLVM/Instrumentation/DefaultChecks.cpp b/src/LLVM/Instrumentation/DefaultChecks.cpp index ecf678ef..176fbd44 100644 --- a/src/LLVM/Instrumentation/DefaultChecks.cpp +++ b/src/LLVM/Instrumentation/DefaultChecks.cpp @@ -183,6 +183,198 @@ char DivisionByZeroCheck::ID; char AssertionFailCheck::ID; char SignedIntegerOverflowCheck::ID; +class MutexCheck : public Check +{ +public: + static char ID; + + MutexCheck() + : Check(ID) + {} + + // TODO duplicate + /// for a specific (function;variableName) pair, returns a unique global variable. + static GlobalVariable* getOrInsertUniqueGlobal(Module& m, + Function* functionDecl, + Type* type, + StringRef variableName) { + return getOrInsertUniqueGlobal(m, functionDecl->getName(), type, variableName); + } + + static GlobalVariable* getOrInsertUniqueGlobal(Module& m, + llvm::Twine functionName, + Type* type, + StringRef variableName) { + auto fullVariableName = ("gazer.global." + functionName + "." + variableName).str(); + auto var = m.getOrInsertGlobal(fullVariableName, type, + [&fullVariableName, &m, &type]() -> GlobalVariable* { + return new GlobalVariable(m, type, false, + GlobalVariable::LinkageTypes::InternalLinkage, + UndefValue::get(type), + fullVariableName); + }); + return static_cast(var); + } + + bool isMutexEnterFunction(llvm::Function* function) { + return function->getName().startswith("Enter"); + } + + static GlobalVariable* enterLockVariable(llvm::Function* function) { + auto funcSuffix = function->getName().substr(5); + return getOrInsertUniqueGlobal(*(function->getParent()), funcSuffix, + IntegerType::getInt1Ty(function->getContext()), + "locked"); + } + + static GlobalVariable* exitLockVariable(llvm::Function* function) { + auto funcSuffix = function->getName().substr(4); + return getOrInsertUniqueGlobal(*(function->getParent()), funcSuffix, + IntegerType::getInt1Ty(function->getContext()), + "locked"); + } + + static void setLockValue(IRBuilder<>& builder, GlobalVariable* lockVariable, bool locked) { + builder.CreateStore(builder.getInt1(false), lockVariable, locked); + } + + static llvm::Value* unlockedCheck(IRBuilder<>& builder, GlobalVariable* lockVariable) { + auto* lockValue = builder.CreateLoad(IntegerType::getInt1Ty(builder.getContext()), + lockVariable); + return builder.CreateICmpEQ(lockValue, builder.getInt1(false)); + } + + static llvm::Value* lockedCheck(IRBuilder<>& builder, GlobalVariable* lockVariable) { + auto* lockValue = builder.CreateLoad(IntegerType::getInt1Ty(builder.getContext()), + lockVariable); + return builder.CreateICmpEQ(lockValue, builder.getInt1(true)); + } + + static bool isMainFunction(llvm::Function& function) { + return function.getName() == "main"; // TODO LLVMFrontendSettings knows the main function + } + + bool mark(llvm::Function& function) override { + if (isMainFunction(function)) { + + llvm::SmallVector enterFunctions; + // initialize the lock variable + for (llvm::Function& enterFunc: function.getParent()->functions()) { + if (isMutexEnterFunction(&enterFunc)) { + enterFunctions.push_back(&enterFunc); + } + } + + for (llvm::Function* enterFunc : enterFunctions) { + IRBuilder<> irbuilder(function.getContext()); + auto* global = enterLockVariable(enterFunc); + irbuilder.SetInsertPoint(&(function.getEntryBlock()), function.getEntryBlock().begin()); + setLockValue(irbuilder, global, false); + } + + llvm::SmallVector exitBlocks; + // assert that at the end nothing is locked. + for (llvm::BasicBlock& bb : function) { + // exit node; UnreachableInst would be unreachable anyways... + if (llvm::isa(bb.getTerminator())) { + exitBlocks.push_back(&bb); + } + } + for (auto* enterFunc: enterFunctions) { + for (auto* bb : exitBlocks) { + // add check to the last non-terminator instruction + IRBuilder<> builder(function.getContext()); + auto* global = enterLockVariable(enterFunc); + + auto* errorBB = createErrorBlock(function, "err.mutex", bb->getTerminator()); + + // insert check + builder.SetInsertPoint(bb->getTerminator()); + auto* check = unlockedCheck(builder, global); + + // create new block with the old terminator (cloned) + auto * newBB = llvm::BasicBlock::Create(builder.getContext(), "", &function); + auto * clonedTerminator = bb->getTerminator()->clone(); + builder.SetInsertPoint(newBB, newBB->begin()); + builder.Insert(clonedTerminator); + + // replace old terminator with branching on the check + builder.ClearInsertionPoint(); + llvm::ReplaceInstWithInst( + bb->getTerminator(), + builder.CreateCondBr(check, newBB, errorBB) + ); + } + } + } + llvm::SmallVector enters; + llvm::SmallVector exits; + + for (Instruction& inst : instructions(function)) { + if (auto* call = dyn_cast(&inst)) { + if (isMutexEnterFunction(call->getCalledFunction())) { + enters.push_back(call); + } + if (call->getCalledFunction()->getName().startswith("Exit")) { + exits.push_back(call); + } + } + } + + for (CallInst* inst : enters) { + auto* bb = inst->getParent(); + auto* errorBB = createErrorBlock(function, "err.mutex", inst); + auto* global = enterLockVariable(inst->getCalledFunction()); + IRBuilder<> builder(function.getContext()); + auto* newBB = bb->splitBasicBlock(inst, ""); + builder.SetInsertPoint(bb->getTerminator()); + + auto* check = unlockedCheck(builder, global); + + builder.ClearInsertionPoint(); + llvm::ReplaceInstWithInst( + bb->getTerminator(), + builder.CreateCondBr(check, newBB, errorBB) + ); + + builder.SetInsertPoint(inst); + builder.CreateStore(builder.getInt1(true), global); + + inst->dropAllReferences(); + inst->eraseFromParent(); + } + + for (CallInst* inst : exits) { + + auto* bb = inst->getParent(); + auto* errorBB = createErrorBlock(function, "err.mutex", inst); + auto* global = exitLockVariable(inst->getCalledFunction()); + IRBuilder<> builder(function.getContext()); + auto* newBB = bb->splitBasicBlock(inst, ""); + builder.SetInsertPoint(bb->getTerminator()); + + auto* check = lockedCheck(builder, global); + + builder.ClearInsertionPoint(); + llvm::ReplaceInstWithInst( + bb->getTerminator(), + builder.CreateCondBr(check, newBB, errorBB) + ); + + builder.SetInsertPoint(inst); + builder.CreateStore(builder.getInt1(false), global); + + inst->dropAllReferences(); + inst->eraseFromParent(); + } + return true;//!enters.empty() || !exits.empty(); + } + + llvm::StringRef getErrorDescription() const override { return "Bad mutex usage"; } +}; + +char MutexCheck::ID; + } // end anonymous namespace bool SignedIntegerOverflowCheck::isOverflowIntrinsic(llvm::Function* callee, GazerIntrinsic::Overflow* ovrKind) @@ -321,3 +513,8 @@ std::unique_ptr gazer::checks::createSignedIntegerOverflowCheck(ClangOpti options.addSanitizerFlag("signed-integer-overflow"); return std::make_unique(); } + +std::unique_ptr gazer::checks::createMutexCheck(ClangOptions& options) +{ + return std::make_unique(); +} From 670d97765635d117980409238cc3f4a2f0153494 Mon Sep 17 00:00:00 2001 From: rl555 Date: Tue, 25 Aug 2020 11:28:33 +0200 Subject: [PATCH 20/47] Register & add mutex check to defaults --- src/LLVM/FrontendConfig.cpp | 2 ++ 1 file changed, 2 insertions(+) diff --git a/src/LLVM/FrontendConfig.cpp b/src/LLVM/FrontendConfig.cpp index de0ea3b2..a1bd985e 100644 --- a/src/LLVM/FrontendConfig.cpp +++ b/src/LLVM/FrontendConfig.cpp @@ -37,6 +37,7 @@ FrontendConfig::FrontendConfig() registerCheck("assertion-fail", &checks::createAssertionFailCheck); registerCheck("div-by-zero", &checks::createDivisionByZeroCheck); registerCheck("signed-overflow", &checks::createSignedIntegerOverflowCheck); + registerCheck("mutex", &checks::createMutexCheck); } void FrontendConfig::registerCheck(llvm::StringRef name, CheckFactory factory) @@ -83,6 +84,7 @@ void FrontendConfig::createChecks(std::vector>& checks) fragments.push_back("assertion-fail"); fragments.push_back("div-by-zero"); fragments.push_back("signed-overflow"); + fragments.push_back("mutex"); } else if (filter == AllChecksSetting) { // Add all registered checks for (auto& [name, factory] : mFactories) { From 9f34f704b03a5b6a0a042ed9771610caba508c3c Mon Sep 17 00:00:00 2001 From: rl555 Date: Tue, 25 Aug 2020 11:29:53 +0200 Subject: [PATCH 21/47] Rewrite AnnotateSpecialFunctions as analysis pass --- .../AnnotateSpecialFunctions.h | 10 +++- .../AnnotateSpecialFunctions.cpp | 53 ++++++++++++------- 2 files changed, 42 insertions(+), 21 deletions(-) diff --git a/include/gazer/LLVM/Instrumentation/AnnotateSpecialFunctions.h b/include/gazer/LLVM/Instrumentation/AnnotateSpecialFunctions.h index fae48153..9f876dd4 100644 --- a/include/gazer/LLVM/Instrumentation/AnnotateSpecialFunctions.h +++ b/include/gazer/LLVM/Instrumentation/AnnotateSpecialFunctions.h @@ -34,10 +34,16 @@ #ifndef SRC_LLVM_INSTRUMENTATION_ANNOTATESPECIALFUNCTIONS_H_ #define SRC_LLVM_INSTRUMENTATION_ANNOTATESPECIALFUNCTIONS_H_ -#include +namespace llvm { +class Pass; +} namespace gazer { -llvm::Pass* createAnnotateSpecialFunctionsPass(); +/** + * Returns analysis pass which annotates known functions for use in SimplifySpecialFunctions. + * TODO currently known functions are based on name patterns (FixPtr* functions are annotated). + */ +char& getAnnotateSpecialFunctionsID(); } #endif /* SRC_LLVM_INSTRUMENTATION_ANNOTATESPECIALFUNCTIONS_H_ */ diff --git a/src/LLVM/Instrumentation/AnnotateSpecialFunctions.cpp b/src/LLVM/Instrumentation/AnnotateSpecialFunctions.cpp index ca40e98e..745ded8b 100644 --- a/src/LLVM/Instrumentation/AnnotateSpecialFunctions.cpp +++ b/src/LLVM/Instrumentation/AnnotateSpecialFunctions.cpp @@ -19,18 +19,18 @@ #include "gazer/LLVM/Instrumentation/AnnotateSpecialFunctions.h" #include "llvm/Support/Casting.h" #include "llvm/IR/Instructions.h" +#include "llvm/IR/IRBuilder.h" #include "llvm/IR/Module.h" -//#include "llvm/Support/raw_ostream.h" #include "llvm/Support/Debug.h" using namespace llvm; namespace { + +// TODO use this only to mark functions, add a Checks pass that watch for the attributes/marked functions class AnnotateSpecialFunctionsPass : public ModulePass { public: - AnnotateSpecialFunctionsPass() : ModulePass(ID) { - - } + AnnotateSpecialFunctionsPass() : ModulePass(ID) {} bool runOnModule(Module& m) override { bool res = false; @@ -54,22 +54,32 @@ class AnnotateSpecialFunctionsPass : public ModulePass { static char ID; private: + bool processInstruction(Module& m, CallInst& inst) { - // known function + auto enterExitCounterType = Type::getInt32Ty(m.getContext()); + // known API functions if (inst.getCalledFunction()->getName().startswith("FixPtr")) { auto varName = ("gazer." + inst.getCalledFunction()->getName()).str(); - // TODO assert definition is like "type* FixPtr()" - auto resType = inst.getCalledFunction()->getReturnType()->getPointerElementType(); - auto var = m.getOrInsertGlobal(varName, resType, - [&varName, &m, &resType]() -> GlobalVariable* { - return new GlobalVariable(m, resType, false, - GlobalVariable::LinkageTypes::InternalLinkage, - UndefValue::get(resType), - varName); - }); - inst.replaceAllUsesWith(var); - inst.dropAllReferences(); - inst.eraseFromParent(); + + bool ok = true; + if (inst.getNumArgOperands() != 0) { + m.getContext().emitError(&inst, "FixPtr calls must have zero parameters\n"); + ok = false; + // do not return for more checks + } + if (!inst.getFunctionType()->getReturnType()->isPointerTy()) { + m.getContext().emitError(&inst, "FixPtr calls must have pointer return type\n"); + ok = false; + } + if (!ok) { + // no change + return false; + } + + inst.setDoesNotAccessMemory(); + inst.getCalledFunction()->setSpeculatable(); + inst.getCalledFunction()->setDoesNotAccessMemory(); + inst.getCalledFunction()->setReturnDoesNotAlias(); return true; } // known intrinsics @@ -77,7 +87,7 @@ class AnnotateSpecialFunctionsPass : public ModulePass { inst.getCalledFunction()->getName().startswith("llvm.")) { return false; } - llvm::errs() << "WARNING: unknown function " << *(inst.getCalledFunction()) << "\n"; + errs() << "WARNING: unknown function " << *(inst.getCalledFunction()) << "\n"; return false; } @@ -86,8 +96,13 @@ class AnnotateSpecialFunctionsPass : public ModulePass { char AnnotateSpecialFunctionsPass::ID; -static RegisterPass X("annot-spec-functions", "annot-spec-functions", false, false); +char& gazer::getAnnotateSpecialFunctionsID() { + return AnnotateSpecialFunctionsPass::ID; +} +static RegisterPass X("annot-spec-functions", "annot-spec-functions", false, true); +/* llvm::Pass* gazer::createAnnotateSpecialFunctionsPass() { return new AnnotateSpecialFunctionsPass(); } +*/ From 95512a5c08f981608a97cd89bb711d96366623a0 Mon Sep 17 00:00:00 2001 From: rl555 Date: Tue, 25 Aug 2020 11:32:22 +0200 Subject: [PATCH 22/47] Document simplify special functions --- .../Instrumentation/SimplifySpecialFunctions.h | 17 +++++++++++++---- 1 file changed, 13 insertions(+), 4 deletions(-) diff --git a/include/gazer/LLVM/Instrumentation/SimplifySpecialFunctions.h b/include/gazer/LLVM/Instrumentation/SimplifySpecialFunctions.h index 16d764cc..d84629c8 100644 --- a/include/gazer/LLVM/Instrumentation/SimplifySpecialFunctions.h +++ b/include/gazer/LLVM/Instrumentation/SimplifySpecialFunctions.h @@ -1,10 +1,15 @@ /** * @file SimplifySpecialFunctions.h * - * @brief <> + * @brief Contains pass which simplifies functions with special properties * - * << Write the detailed description of the file here. >> + * Simplifies functions with special properties so analysis can take place. + * There are some hard to analyze constructs like pointer handling. + * The goal of this pass is to rewrite the function call to easier constructs. * + * When certain conditions are met for a function, + * replaces function call with access to a global variable + * * @author laszlo.radnai * @date 2020.08.19. * @@ -22,9 +27,13 @@ class Pass; namespace gazer { /** + * Simplifies functions with special properties so analysis can take place. + * There are some hard to analyze constructs like pointer handling. + * The goal of this pass is to rewrite the function call to easier constructs. + * * Simplifies special known, but not implemented functions. - * 1) When certain conditions are met for a function, - * replaces function call with a pre-defined value + * When certain conditions are met for a function, + * replaces function call with access to a global variable * @return */ llvm::Pass* createSimplifySpecialFunctionsPass(); From 4ade7ca53558c565625d412db5ee096f92b42d0f Mon Sep 17 00:00:00 2001 From: rl555 Date: Tue, 25 Aug 2020 11:33:15 +0200 Subject: [PATCH 23/47] Use SimplifySpecialFunctions instead of AnnotateSpecialFunctions --- src/LLVM/LLVMFrontend.cpp | 6 +++--- 1 file changed, 3 insertions(+), 3 deletions(-) diff --git a/src/LLVM/LLVMFrontend.cpp b/src/LLVM/LLVMFrontend.cpp index 5ce1a6f0..1e2ccacb 100644 --- a/src/LLVM/LLVMFrontend.cpp +++ b/src/LLVM/LLVMFrontend.cpp @@ -17,7 +17,7 @@ //===----------------------------------------------------------------------===// #include "gazer/LLVM/LLVMFrontend.h" #include "gazer/LLVM/Instrumentation/DefaultChecks.h" -#include "gazer/LLVM/Instrumentation/AnnotateSpecialFunctions.h" +#include "gazer/LLVM/Instrumentation/SimplifySpecialFunctions.h" #include "gazer/LLVM/InstrumentationPasses.h" #include "gazer/LLVM/Transform/Passes.h" #include "gazer/LLVM/Automaton/ModuleToAutomata.h" @@ -156,8 +156,8 @@ void LLVMFrontend::registerVerificationPipeline() // Unify function exit nodes mPassManager.add(llvm::createUnifyFunctionExitNodesPass()); - // Unify function exit nodes - mPassManager.add(gazer::createAnnotateSpecialFunctionsPass()); + // Simplify special functions + mPassManager.add(gazer::createSimplifySpecialFunctionsPass()); // Run assertion lifting. if (mSettings.liftAsserts) { From 978bf8bca9bf7a149d0810d53ea68fbbd5151368 Mon Sep 17 00:00:00 2001 From: rl555 Date: Tue, 25 Aug 2020 11:34:01 +0200 Subject: [PATCH 24/47] Add memory promotion after mutex check --- src/LLVM/LLVMFrontend.cpp | 3 +++ 1 file changed, 3 insertions(+) diff --git a/src/LLVM/LLVMFrontend.cpp b/src/LLVM/LLVMFrontend.cpp index 1e2ccacb..550035af 100644 --- a/src/LLVM/LLVMFrontend.cpp +++ b/src/LLVM/LLVMFrontend.cpp @@ -146,6 +146,9 @@ void LLVMFrontend::registerVerificationPipeline() mPassManager.add(gazer::createNormalizeVerifierCallsPass()); registerEnabledChecks(); + // mutex check needs a promotion + mPassManager.add(llvm::createPromoteMemoryToRegisterPass()); + // Execute early optimization passes. registerEarlyOptimizations(); From 95192fcbbd1499502ec45d43b6bc22321beee708 Mon Sep 17 00:00:00 2001 From: rl555 Date: Tue, 25 Aug 2020 11:34:53 +0200 Subject: [PATCH 25/47] Add SimplifySpecialFunctions to build --- src/LLVM/CMakeLists.txt | 1 + 1 file changed, 1 insertion(+) diff --git a/src/LLVM/CMakeLists.txt b/src/LLVM/CMakeLists.txt index 8bee535e..5bf684f4 100644 --- a/src/LLVM/CMakeLists.txt +++ b/src/LLVM/CMakeLists.txt @@ -11,6 +11,7 @@ set(SOURCE_FILES Instrumentation/Check.cpp Instrumentation/DefaultChecks.cpp Instrumentation/Intrinsics.cpp + Instrumentation/SimplifySpecialFunctions.cpp Trace/TestHarnessGenerator.cpp Automaton/ModuleToAutomata.cpp Automaton/InstToExpr.cpp From ca179666ecdc79b1e26f055f55f81d58150d6d2d Mon Sep 17 00:00:00 2001 From: rl555 Date: Tue, 25 Aug 2020 11:49:23 +0200 Subject: [PATCH 26/47] Remove solved TODO --- src/LLVM/Instrumentation/AnnotateSpecialFunctions.cpp | 1 - 1 file changed, 1 deletion(-) diff --git a/src/LLVM/Instrumentation/AnnotateSpecialFunctions.cpp b/src/LLVM/Instrumentation/AnnotateSpecialFunctions.cpp index 745ded8b..c1ca0739 100644 --- a/src/LLVM/Instrumentation/AnnotateSpecialFunctions.cpp +++ b/src/LLVM/Instrumentation/AnnotateSpecialFunctions.cpp @@ -27,7 +27,6 @@ using namespace llvm; namespace { -// TODO use this only to mark functions, add a Checks pass that watch for the attributes/marked functions class AnnotateSpecialFunctionsPass : public ModulePass { public: AnnotateSpecialFunctionsPass() : ModulePass(ID) {} From 3e2b08b9d5859d7205e323b37d72b2d79c1b778d Mon Sep 17 00:00:00 2001 From: rl555 Date: Sat, 29 Aug 2020 15:44:00 +0200 Subject: [PATCH 27/47] Add test for generated stubbed methods --- api_contract_test.c | 29 -------------- .../generated/contracts/annotations | 0 .../generated/contracts/ea_stub.xcfa | 39 +++++++++++++++++++ .../SimpleTestCase/generated/contracts/index | 1 + test/rte/SimpleTestCase/run.config | 3 ++ test/rte/SimpleTestCase/src/re_test.c | 7 ++++ 6 files changed, 50 insertions(+), 29 deletions(-) delete mode 100644 api_contract_test.c create mode 100644 test/rte/SimpleTestCase/generated/contracts/annotations create mode 100644 test/rte/SimpleTestCase/generated/contracts/ea_stub.xcfa create mode 100644 test/rte/SimpleTestCase/generated/contracts/index create mode 100644 test/rte/SimpleTestCase/run.config create mode 100644 test/rte/SimpleTestCase/src/re_test.c diff --git a/api_contract_test.c b/api_contract_test.c deleted file mode 100644 index c50605d4..00000000 --- a/api_contract_test.c +++ /dev/null @@ -1,29 +0,0 @@ -#include -// "FixPtr.*" function has hard-coded property that it returns a constant pointer without side-effects -int* FixPtr_First(void); -int* FixPtr_Second(void); -void undef_call(void); - -int main2() { - *FixPtr_First() = 5; - - // another instance is returned from another function call - *FixPtr_Second() = 3; - - int x = *FixPtr_First(); - - assert(x == 5); - - // WARNING: unknown function undef_call(). - // Side-effects might cause unsound verification. - undef_call(); - return 0; -} - -void Enter1(void) __attribute__((used)); -void Exit1(void) __attribute__((used)); - -int main() { - Enter1(); - Exit1(); -} diff --git a/test/rte/SimpleTestCase/generated/contracts/annotations b/test/rte/SimpleTestCase/generated/contracts/annotations new file mode 100644 index 00000000..e69de29b diff --git a/test/rte/SimpleTestCase/generated/contracts/ea_stub.xcfa b/test/rte/SimpleTestCase/generated/contracts/ea_stub.xcfa new file mode 100644 index 00000000..8d006542 --- /dev/null +++ b/test/rte/SimpleTestCase/generated/contracts/ea_stub.xcfa @@ -0,0 +1,39 @@ +main process main_process { + var locked__test : bool + procedure Enter_test() { + init loc L0 + error loc L1 + final loc LE + L0 -> L1 { + assume not locked__test + locked__test := true + } + L0 -> LE { + assume locked__test + } + } + procedure Exit_test() { + init loc L0 + error loc L1 + final loc LE + L0 -> L1 { + assume locked__test + locked__test := false + } + L0 -> LE { + assume locked__test + } + } + procedure ctor_locked__test() { + init loc L0 + final loc L1 + L0 -> L1 { } + } + procedure dtor_locked__test() { + init loc L0 + final loc L1 + error loc LE + L0 -> L1 { assume not locked__test } + L0 -> LE { assume locked__test} + } +} diff --git a/test/rte/SimpleTestCase/generated/contracts/index b/test/rte/SimpleTestCase/generated/contracts/index new file mode 100644 index 00000000..0a765def --- /dev/null +++ b/test/rte/SimpleTestCase/generated/contracts/index @@ -0,0 +1 @@ +re_test ea_stub.xcfa diff --git a/test/rte/SimpleTestCase/run.config b/test/rte/SimpleTestCase/run.config new file mode 100644 index 00000000..8f9c5cd6 --- /dev/null +++ b/test/rte/SimpleTestCase/run.config @@ -0,0 +1,3 @@ +// RUN: %theta-re "%S" | FileCheck "%s" + +// CHECK: Verification FAILED diff --git a/test/rte/SimpleTestCase/src/re_test.c b/test/rte/SimpleTestCase/src/re_test.c new file mode 100644 index 00000000..a0a80868 --- /dev/null +++ b/test/rte/SimpleTestCase/src/re_test.c @@ -0,0 +1,7 @@ +void Enter_test(void); +void Exit_test(void); + +void re_test() { + Enter_test(); + Exit_test(); +} From e02fe2859c04993c3a9df28a955fbc7902ba0e00 Mon Sep 17 00:00:00 2001 From: rl555 Date: Sat, 29 Aug 2020 15:46:25 +0200 Subject: [PATCH 28/47] Update lit config --- test/lit.cfg | 6 ++++-- 1 file changed, 4 insertions(+), 2 deletions(-) diff --git a/test/lit.cfg b/test/lit.cfg index 48212f31..a400e264 100644 --- a/test/lit.cfg +++ b/test/lit.cfg @@ -7,7 +7,7 @@ import pathlib config.name = 'gazer' config.test_format = lit.formats.ShTest() config.test_source_root = os.path.dirname(__file__) -config.suffixes = ['.c', '.ll'] +config.suffixes = ['.c', '.ll', '.config'] config.excludes = [ "errors.c" ] @@ -21,10 +21,12 @@ config.environment['GAZER_TOOLS_DIR'] = gazer_tools_dir config.substitutions.append(('%bmc', gazer_tools_dir + "/gazer-bmc/gazer-bmc")) config.substitutions.append(('%cfa', gazer_tools_dir + "/gazer-cfa/gazer-cfa")) +config.substitutions.append(('%theta', gazer_tools_dir + "/gazer-theta/gazer-theta")) +config.substitutions.append(('%theta-re', gazer_tools_dir + "/gazer-theta/gazer-theta-re")) config.substitutions.append(('%check-cex', os.path.join(os.path.dirname(__file__), "check-cex.sh"))) config.substitutions.append(('%errors', os.path.join(os.path.dirname(__file__), "errors.c"))) config.available_features.add('heap') config.available_features.add('memory.arrays') config.available_features.add('memory.structs') -config.available_features.add('memory.burstall') \ No newline at end of file +config.available_features.add('memory.burstall') From 48ac69c1b8946705dad7fc0ea108da70ad27ccfc Mon Sep 17 00:00:00 2001 From: rl555 Date: Sat, 29 Aug 2020 15:49:52 +0200 Subject: [PATCH 29/47] Add gazer-theta-re --- CMakeLists.txt | 4 +- tools/gazer-theta/CMakeLists.txt | 5 +- tools/gazer-theta/gazer-theta-re.cpp | 269 +++++++++++++++++++++++++++ 3 files changed, 275 insertions(+), 3 deletions(-) create mode 100644 tools/gazer-theta/gazer-theta-re.cpp diff --git a/CMakeLists.txt b/CMakeLists.txt index 73232bc5..d61e6a84 100644 --- a/CMakeLists.txt +++ b/CMakeLists.txt @@ -70,8 +70,8 @@ endif() set(GAZER_CLANG_TEST_COMPILER "clang" CACHE STRING "Clang compiler path for functional tests") add_custom_target(check-functional - COMMAND GAZER_TOOLS_DIR=${CMAKE_BINARY_DIR}/tools lit -v --timeout=60 ${CMAKE_CURRENT_LIST_DIR}/test - DEPENDS gazer-bmc gazer-cfa gazer-theta + COMMAND GAZER_TOOLS_DIR=${CMAKE_BINARY_DIR}/tools lit -v ${CMAKE_CURRENT_LIST_DIR}/test + DEPENDS gazer-bmc gazer-cfa gazer-theta gazer-theta-re ) find_program(CLANG_TIDY NAMES "clang-tidy") diff --git a/tools/gazer-theta/CMakeLists.txt b/tools/gazer-theta/CMakeLists.txt index a821ab09..7c07659e 100644 --- a/tools/gazer-theta/CMakeLists.txt +++ b/tools/gazer-theta/CMakeLists.txt @@ -15,5 +15,8 @@ target_link_libraries(GazerBackendTheta GazerLLVM) add_executable(gazer-theta ${TOOL_SOURCE_FILES}) +add_executable(gazer-theta-re gazer-theta-re.cpp) + # TODO: Boost filesystem should be linked "properly" or dropped altogether -target_link_libraries(gazer-theta GazerBackendTheta -lboost_system -lboost_filesystem) \ No newline at end of file +target_link_libraries(gazer-theta GazerBackendTheta -lboost_system -lboost_filesystem) +target_link_libraries(gazer-theta-re GazerBackendTheta -lboost_system -lboost_regex -lboost_filesystem) diff --git a/tools/gazer-theta/gazer-theta-re.cpp b/tools/gazer-theta/gazer-theta-re.cpp new file mode 100644 index 00000000..5eb858f2 --- /dev/null +++ b/tools/gazer-theta/gazer-theta-re.cpp @@ -0,0 +1,269 @@ +#include "lib/ThetaVerifier.h" +#include "lib/ThetaCfaGenerator.h" + +#include "gazer/LLVM/LLVMFrontend.h" +#include "gazer/Core/GazerContext.h" + +#include +#include +#include +#include + +#include + +#ifndef NDEBUG +#include +#include +#include +#endif + +using namespace gazer; +using namespace llvm; + +namespace +{ + + // Theta environment settings + cl::OptionCategory ThetaEnvironmentCategory("Theta environment settings"); + + cl::opt InputFilename(cl::Positional, cl::desc(""), + cl::cat(ThetaEnvironmentCategory), cl::init("")); + + cl::opt ModelPath("o", + cl::desc("Model output path (will use a unique location if not set)"), + cl::cat(ThetaEnvironmentCategory), + cl::init("") + ); + cl::opt ModelOnly("model-only", + cl::desc("Do not run the verification engine, just write the theta CFA"), + cl::cat(ThetaEnvironmentCategory) + ); + + cl::opt ThetaPath("theta-path", + cl::desc("Full path to the theta-cfa jar file. Defaults to '/theta/theta-cfa-cli.jar'"), + cl::cat(ThetaEnvironmentCategory), + cl::init("") + ); + cl::opt LibPath("lib-path", + cl::desc("Full path to the directory containing the Z3 libraries (libz3.so, libz3java.so) required by theta." + " Defaults to '/theta/lib'"), + cl::cat(ThetaEnvironmentCategory), + cl::init("") + ); + + // Algorithm options + cl::OptionCategory ThetaAlgorithmCategory("Theta algorithm settings"); + + cl::opt Domain("domain", cl::desc("Abstract domain"), cl::init("PRED_CART"), cl::cat(ThetaAlgorithmCategory)); + cl::opt Refinement("refinement", cl::desc("Refinement strategy"), cl::init("SEQ_ITP"), cl::cat(ThetaAlgorithmCategory)); + cl::opt Search("search", cl::desc("Search strategy"), cl::init("BFS"), cl::cat(ThetaAlgorithmCategory)); + cl::opt PrecGranularity("precgranularity", cl::desc("Precision granularity"), cl::init("GLOBAL"), cl::cat(ThetaAlgorithmCategory)); + cl::opt PredSplit("predsplit", cl::desc("Predicate splitting (for predicate abstraction)"), cl::init("WHOLE"), cl::cat(ThetaAlgorithmCategory)); + cl::opt Encoding("encoding", cl::desc("Block encoding"), cl::init("LBE"), cl::cat(ThetaAlgorithmCategory)); + cl::opt MaxEnum("maxenum", cl::desc("Maximal number of explicitly enumerated successors"), cl::init(0), cl::cat(ThetaAlgorithmCategory)); + cl::opt InitPrec("initPrec", cl::desc("Initial precision of abstraction"), cl::init("EMPTY"), cl::cat(ThetaAlgorithmCategory)); + cl::opt PruneStrategy("pruneStrategy", cl::desc("Strategy for pruning after refinement"), cl::init("LAZY"), cl::cat(ThetaAlgorithmCategory)); +} // end anonymous namespace + +namespace gazer +{ + extern cl::OptionCategory ClangFrontendCategory; + extern cl::OptionCategory LLVMFrontendCategory; + extern cl::OptionCategory IrToCfaCategory; + extern cl::OptionCategory TraceCategory; + extern cl::OptionCategory ChecksCategory; +} // end namespace gazer + +static theta::ThetaSettings initSettingsFromCommandLine(); + +std::vector runnables() { + const std::string target_path(InputFilename + "/src/"); + const boost::regex my_filter(".*\\.c"); + + std::vector all_matching_files; + + boost::filesystem::directory_iterator end_itr; // Default ctor yields past-the-end + for (boost::filesystem::directory_iterator i(target_path); i != end_itr; ++i) + { + // Skip if not a file + if (!boost::filesystem::is_regular_file(i->status())) continue; + + if (i->path().extension() != ".c") continue; + + // File matches, store it + + all_matching_files.push_back(i->path().filename().replace_extension("").string()); + } + return std::move(all_matching_files); +} + +using AnnotationMap = std::map>; + +AnnotationMap annotations() { + + std::ifstream ifs(InputFilename + "/generated/contracts/annotations"); + std::string fileData(std::istreambuf_iterator(ifs), + std::istreambuf_iterator()); + std::vector lines; + { + std::string tmp; + while (std::getline(ifs, tmp)) { + lines.push_back(std::move(tmp)); + } + } + AnnotationMap result; + for (const auto& line : lines) { + if (line == "") { + continue; + } + std::vector tokens; + boost::split(tokens, line, boost::is_any_of(" ")); + if (tokens.size() == 0) { + continue; + } + auto& re = tokens[0]; + std::vector annotations(std::next(tokens.begin()), tokens.end()); + result[re] = annotations; + } + return result; +} + +using XcfaMap = std::map>; + +XcfaMap xcfas() { + // find XCFAs + std::ifstream ifs(InputFilename + "/generated/contracts/index"); + std::string fileData(std::istreambuf_iterator(ifs), + std::istreambuf_iterator()); + std::vector lines; + { + std::string tmp; + while (std::getline(ifs, tmp)) { + lines.push_back(std::move(tmp)); + } + } + XcfaMap result; + for (const auto& line : lines) { + if (line == "") { + continue; + } + std::vector tokens; + boost::split(tokens, line, boost::is_any_of(" ")); + if (tokens.size() == 0) { + continue; + } + auto& re = tokens[0]; + std::vector xcfas(std::next(tokens.begin()), tokens.end()); + llvm::errs() << xcfas[0] << "\n"; + result[re] = xcfas; + } + return result; +} + +int main(int argc, char* argv[]) +{ + cl::HideUnrelatedOptions({ + &ClangFrontendCategory, &LLVMFrontendCategory, + &IrToCfaCategory, &TraceCategory, &ChecksCategory, + &ThetaEnvironmentCategory, &ThetaAlgorithmCategory + }); + + cl::SetVersionPrinter(&FrontendConfigWrapper::PrintVersion); + cl::ParseCommandLineOptions(argc, argv); + + #ifndef NDEBUG + llvm::sys::PrintStackTraceOnErrorSignal(argv[0]); + llvm::PrettyStackTraceProgram(argc, argv); + llvm::EnableDebugBuffering = true; + #endif + + // Set up settings + theta::ThetaSettings backendSettings = initSettingsFromCommandLine(); + + if (backendSettings.thetaCfaPath.empty() || backendSettings.thetaLibPath.empty()) { + // Find the current program location + boost::dll::fs::error_code ec; + auto pathToBinary = boost::dll::program_location(ec); + + if (ec) { + llvm::errs() << "ERROR: Could not find the path to this process: " + ec.message(); + return 1; + } + + if (backendSettings.thetaCfaPath.empty()) { + backendSettings.thetaCfaPath = pathToBinary.parent_path().string() + "/theta/theta-cfa-cli.jar"; + } + + if (backendSettings.thetaLibPath.empty()) { + backendSettings.thetaLibPath = pathToBinary.parent_path().string() + "/theta/lib"; + } + } + + auto runnableList = runnables(); + + auto annots = annotations(); + + auto xcfaData = xcfas(); + + // this should be before any LLVM calls (so the destructor is called at an appropriate time) + llvm::llvm_shutdown_obj mShutdown; + + for (auto& runnable : runnableList) { + std::string file = InputFilename + "/src/" + runnable + ".c"; + llvm::errs() << "Runnable " << runnable << " has file " << file << "\n"; + // Find matching annotations + auto it = annots.find(runnable); + if (it != annots.end()) { + for (auto annot : it->second) { + llvm::errs() << "Annotation " << annot << "\n"; + } + } + + // Run the frontend + + backendSettings.xcfaDir = InputFilename + "/generated/contracts/"; + backendSettings.xcfas = std::vector(); + { + auto it = xcfaData.find(runnable); + if (it != xcfaData.end()) { + backendSettings.xcfas = it->second; + } + } + FrontendConfigWrapper config; + + config.getSettings().function = runnable; + + // Force -math-int + config.getSettings().ints = IntRepresentation::Integers; + auto frontend = config.buildFrontend({file}); + if (frontend == nullptr) { + return 1; + } + + frontend->setBackendAlgorithm(new theta::ThetaVerifier(backendSettings)); + frontend->registerVerificationPipeline(); + frontend->run(); + } + return 0; +} + +theta::ThetaSettings initSettingsFromCommandLine() +{ + theta::ThetaSettings settings; + + settings.timeout = 0; // TODO + settings.modelPath = ModelPath; + settings.domain = Domain; + settings.refinement = Refinement; + settings.search = Search; + settings.precGranularity = PrecGranularity; + settings.predSplit = PredSplit; + settings.encoding = Encoding; + settings.maxEnum = std::to_string(MaxEnum); + settings.initPrec = InitPrec; + settings.pruneStrategy = PruneStrategy; + settings.thetaCfaPath = ThetaPath; + settings.thetaLibPath = LibPath; + + return settings; +} From 4202e3b7bb2073c9d22090563504ee31dbe264ad Mon Sep 17 00:00:00 2001 From: rl555 Date: Sat, 29 Aug 2020 15:51:46 +0200 Subject: [PATCH 30/47] Add multiple input files support for Theta --- tools/gazer-theta/lib/ThetaVerifier.cpp | 8 +++++++- tools/gazer-theta/lib/ThetaVerifier.h | 5 +++++ 2 files changed, 12 insertions(+), 1 deletion(-) diff --git a/tools/gazer-theta/lib/ThetaVerifier.cpp b/tools/gazer-theta/lib/ThetaVerifier.cpp index c2992e9e..a0a2a0e9 100644 --- a/tools/gazer-theta/lib/ThetaVerifier.cpp +++ b/tools/gazer-theta/lib/ThetaVerifier.cpp @@ -122,12 +122,18 @@ auto ThetaVerifierImpl::execute(llvm::StringRef input) -> std::unique_ptr args = { "java", javaLibPath, "-jar", thetaPath, - "--model", input, + "--model", inputs, "--domain", mSettings.domain, "--encoding", mSettings.encoding, "--initprec", mSettings.initPrec, diff --git a/tools/gazer-theta/lib/ThetaVerifier.h b/tools/gazer-theta/lib/ThetaVerifier.h index 87c34bd5..678bc70e 100644 --- a/tools/gazer-theta/lib/ThetaVerifier.h +++ b/tools/gazer-theta/lib/ThetaVerifier.h @@ -21,6 +21,8 @@ #include "gazer/Automaton/Cfa.h" #include "gazer/Verifier/VerificationAlgorithm.h" +#include + namespace gazer::theta { @@ -32,6 +34,9 @@ struct ThetaSettings unsigned timeout = 0; std::string modelPath; + std::string xcfaDir; + std::vector xcfas; + // Algorithm settings std::string domain; std::string refinement; From b111c86f5f7d247aeb90306102ab2fed9481930a Mon Sep 17 00:00:00 2001 From: rl555 Date: Sat, 29 Aug 2020 15:52:59 +0200 Subject: [PATCH 31/47] Solve call clashing with keyword --- tools/gazer-theta/lib/ThetaCfaProcedureGenerator.cpp | 3 ++- tools/gazer-theta/lib/ThetaUtil.h | 2 +- 2 files changed, 3 insertions(+), 2 deletions(-) diff --git a/tools/gazer-theta/lib/ThetaCfaProcedureGenerator.cpp b/tools/gazer-theta/lib/ThetaCfaProcedureGenerator.cpp index 91854ae4..80a7b838 100644 --- a/tools/gazer-theta/lib/ThetaCfaProcedureGenerator.cpp +++ b/tools/gazer-theta/lib/ThetaCfaProcedureGenerator.cpp @@ -167,7 +167,8 @@ void gazer::ThetaCfaProcedureGenerator::writeCFA(llvm::raw_ostream& os, gazer::t os << "main "; } // TODO main -> xmain temp solution - os << "procedure x" << cfa->getName() << "("; + std::string cfaName = gazer::theta::validName(cfa->getName(), [](const std::string& x) {return true;}); + os << "procedure " << cfaName << "("; bool first = true; for (auto& input : cfa->inputs()) { if (first) { diff --git a/tools/gazer-theta/lib/ThetaUtil.h b/tools/gazer-theta/lib/ThetaUtil.h index 9ed1bbdf..a54d2401 100644 --- a/tools/gazer-theta/lib/ThetaUtil.h +++ b/tools/gazer-theta/lib/ThetaUtil.h @@ -181,7 +181,7 @@ struct PrintVisitor auto prefix = result.has_value() ? result.value() + llvm::Twine(" := ") : ""; // TODO main -> xmain temp solution - mOS << prefix << "call x" << std::get<0>(call) << "("; + mOS << prefix << "call " << std::get<0>(call) << "("; bool first = true; for (const auto& param : std::get<1>(call)) { if (first) { From 8c6b2ebce66ecbf1c28bc02017cdf63ad749e798 Mon Sep 17 00:00:00 2001 From: rl555 Date: Sat, 29 Aug 2020 15:56:25 +0200 Subject: [PATCH 32/47] Remove mutex check from default checks --- include/gazer/LLVM/Instrumentation/DefaultChecks.h | 2 +- src/LLVM/FrontendConfig.cpp | 1 - src/LLVM/Instrumentation/DefaultChecks.cpp | 2 ++ 3 files changed, 3 insertions(+), 2 deletions(-) diff --git a/include/gazer/LLVM/Instrumentation/DefaultChecks.h b/include/gazer/LLVM/Instrumentation/DefaultChecks.h index a69f7bae..ab613ff4 100644 --- a/include/gazer/LLVM/Instrumentation/DefaultChecks.h +++ b/include/gazer/LLVM/Instrumentation/DefaultChecks.h @@ -32,7 +32,7 @@ namespace gazer::checks std::unique_ptr createSignedIntegerOverflowCheck(ClangOptions& options); /// This check fails if a non-reentrant mutex has bad usage. - /// TODO initialization and clean-up are a problem. + /// Unused std::unique_ptr createMutexCheck(ClangOptions& options); } // end namespace gazer::checks diff --git a/src/LLVM/FrontendConfig.cpp b/src/LLVM/FrontendConfig.cpp index a1bd985e..c1d90e48 100644 --- a/src/LLVM/FrontendConfig.cpp +++ b/src/LLVM/FrontendConfig.cpp @@ -84,7 +84,6 @@ void FrontendConfig::createChecks(std::vector>& checks) fragments.push_back("assertion-fail"); fragments.push_back("div-by-zero"); fragments.push_back("signed-overflow"); - fragments.push_back("mutex"); } else if (filter == AllChecksSetting) { // Add all registered checks for (auto& [name, factory] : mFactories) { diff --git a/src/LLVM/Instrumentation/DefaultChecks.cpp b/src/LLVM/Instrumentation/DefaultChecks.cpp index 176fbd44..68d0ca49 100644 --- a/src/LLVM/Instrumentation/DefaultChecks.cpp +++ b/src/LLVM/Instrumentation/DefaultChecks.cpp @@ -183,6 +183,7 @@ char DivisionByZeroCheck::ID; char AssertionFailCheck::ID; char SignedIntegerOverflowCheck::ID; +/// Unused check for mutex class MutexCheck : public Check { public: @@ -251,6 +252,7 @@ class MutexCheck : public Check } static bool isMainFunction(llvm::Function& function) { + // TODO global ctor/dtor?? return function.getName() == "main"; // TODO LLVMFrontendSettings knows the main function } From 4b9620525559bc4e7221ea1a1c750bd7efd71c79 Mon Sep 17 00:00:00 2001 From: rl555 Date: Sat, 29 Aug 2020 15:57:20 +0200 Subject: [PATCH 33/47] Remove shutdown object from gazer::LLVMFrontend --- include/gazer/LLVM/LLVMFrontend.h | 6 ++++-- 1 file changed, 4 insertions(+), 2 deletions(-) diff --git a/include/gazer/LLVM/LLVMFrontend.h b/include/gazer/LLVM/LLVMFrontend.h index bc4cf85e..7ef349b3 100644 --- a/include/gazer/LLVM/LLVMFrontend.h +++ b/include/gazer/LLVM/LLVMFrontend.h @@ -91,7 +91,9 @@ class FrontendConfigWrapper LLVMFrontendSettings& getSettings() { return config.getSettings(); } private: - llvm::llvm_shutdown_obj mShutdown; // This should be kept as first, will be destroyed last + // We will run LLVM multiple times and use different FrontendConfigWrappers. + // TODO removing this breaks the normal usage. + //llvm::llvm_shutdown_obj mShutdown; public: llvm::LLVMContext llvmContext; GazerContext context; @@ -166,4 +168,4 @@ class LLVMFrontend } -#endif \ No newline at end of file +#endif From 780b5d272ddd43fb7d0aaf31d3521418928f5e14 Mon Sep 17 00:00:00 2001 From: rl555 Date: Sat, 29 Aug 2020 15:59:14 +0200 Subject: [PATCH 34/47] Add support for calling undefined functions Functions that weren't defined were generated a simple CFA or calls were dropped entirely. When multiple inputs are present, some XCFA, Gazer must not drop these calls. CallGraph check for recursion is disabled. --- include/gazer/Automaton/CallGraph.h | 4 +- include/gazer/Automaton/Cfa.h | 2 +- src/Automaton/CallGraph.cpp | 5 +- src/Automaton/Cfa.cpp | 6 +- src/LLVM/Automaton/FunctionToCfa.h | 6 ++ src/LLVM/Automaton/ModuleToAutomata.cpp | 138 +++++++++++++----------- 6 files changed, 90 insertions(+), 71 deletions(-) diff --git a/include/gazer/Automaton/CallGraph.h b/include/gazer/Automaton/CallGraph.h index cc550c50..85631e8d 100644 --- a/include/gazer/Automaton/CallGraph.h +++ b/include/gazer/Automaton/CallGraph.h @@ -48,7 +48,7 @@ class CallGraph void addCall(CallTransition* call, Node* node) { assert(call != nullptr); - assert(node != nullptr); + if (node == nullptr) { return; } mCallsToOthers.emplace_back(call, node); node->mCallsToThis.emplace_back(call); @@ -118,4 +118,4 @@ struct GraphTraits } // end namespace llvm -#endif \ No newline at end of file +#endif diff --git a/include/gazer/Automaton/Cfa.h b/include/gazer/Automaton/Cfa.h index f058d07c..678dbecb 100644 --- a/include/gazer/Automaton/Cfa.h +++ b/include/gazer/Automaton/Cfa.h @@ -350,7 +350,7 @@ class AutomataSystem final Type& type); public: - Cfa* createCfa(std::string name); + Cfa* createCfa(std::string name, bool register_cfa = true); using iterator = boost::indirect_iterator>::iterator>; using const_iterator = boost::indirect_iterator>::const_iterator>; diff --git a/src/Automaton/CallGraph.cpp b/src/Automaton/CallGraph.cpp index 88a3460b..1c863e61 100644 --- a/src/Automaton/CallGraph.cpp +++ b/src/Automaton/CallGraph.cpp @@ -43,7 +43,8 @@ CallGraph::CallGraph(AutomataSystem& system) bool CallGraph::isTailRecursive(Cfa* cfa) { - auto& node = mNodes[cfa]; + return false; + /*auto& node = mNodes[cfa]; bool isRecursive = false; bool isTail = true; @@ -58,7 +59,7 @@ bool CallGraph::isTailRecursive(Cfa* cfa) } } - return isRecursive && isTail; + return isRecursive && isTail;*/ } auto CallGraph::lookupNode(Cfa* cfa) -> Node* diff --git a/src/Automaton/Cfa.cpp b/src/Automaton/Cfa.cpp index 81e41056..e3cf7b64 100644 --- a/src/Automaton/Cfa.cpp +++ b/src/Automaton/Cfa.cpp @@ -315,10 +315,12 @@ AutomataSystem::AutomataSystem(GazerContext &context) : mContext(context) {} -Cfa *AutomataSystem::createCfa(std::string name) +Cfa *AutomataSystem::createCfa(std::string name, bool register_cfa) { Cfa* cfa = new Cfa(mContext, name, *this); - mAutomata.emplace_back(cfa); + if (register_cfa) { + mAutomata.emplace_back(cfa); + } return cfa; } diff --git a/src/LLVM/Automaton/FunctionToCfa.h b/src/LLVM/Automaton/FunctionToCfa.h index 4ad45d92..6629ed75 100644 --- a/src/LLVM/Automaton/FunctionToCfa.h +++ b/src/LLVM/Automaton/FunctionToCfa.h @@ -247,6 +247,12 @@ class GenerationContext CfaToLLVMTrace& getTraceInfo() { return mTraceInfo; } const SpecialFunctions& getSpecialFunctions() const { return mSpecialFunctions; } + bool hasInfoFor(llvm::Function* function) + { + auto it = mProcedures.find(function); + return it != mProcedures.end(); + } + private: CfaGenInfo& getInfoFor(VariantT key) { diff --git a/src/LLVM/Automaton/ModuleToAutomata.cpp b/src/LLVM/Automaton/ModuleToAutomata.cpp index 396e2472..eaa599ad 100644 --- a/src/LLVM/Automaton/ModuleToAutomata.cpp +++ b/src/LLVM/Automaton/ModuleToAutomata.cpp @@ -250,12 +250,14 @@ std::unique_ptr ModuleToCfa::generate( // Encode all loops and functions for (auto& [source, genInfo] : mGenCtx.procedures()) { - LLVM_DEBUG(llvm::dbgs() << "Encoding function CFA " << genInfo.Automaton->getName() << "\n"); + if (!genInfo.getSourceFunction()->isDeclaration()){ + LLVM_DEBUG(llvm::dbgs() << "Encoding function CFA " << genInfo.Automaton->getName() << "\n"); - BlocksToCfa blocksToCfa(mGenCtx, genInfo, *mExprBuilder); + BlocksToCfa blocksToCfa(mGenCtx, genInfo, *mExprBuilder); - // Do the actual encoding. - blocksToCfa.encode(); + // Do the actual encoding. + blocksToCfa.encode(); + } } // CFAs must be connected graphs. Remove unreachable components now. @@ -563,83 +565,91 @@ void BlocksToCfa::encode() bool BlocksToCfa::handleCall(const llvm::CallInst* call, Location** entry, Location* exit, std::vector& previousAssignments) { Function* callee = call->getCalledFunction(); - if (callee == nullptr) { - // We do not support indirect calls yet. - return false; - } + assert(callee != nullptr && "Indirect calls are unsupported"); // Create an extension point to handle the call auto callerEP = this->createExtensionPoint(previousAssignments, entry, &exit); - if (!callee->isDeclaration()) { - CfaGenInfo& calledAutomatonInfo = mGenCtx.getFunctionCfa(callee); - Cfa* calledCfa = calledAutomatonInfo.Automaton; - assert(calledCfa != nullptr && "The callee automaton must exist in a function call!"); - - // Split the current transition here and create a call. - Location* callBegin = mCfa->createLocation(); - Location* callEnd = mCfa->createLocation(); - - mCfa->createAssignTransition(*entry, callBegin, previousAssignments); - previousAssignments.clear(); - - llvm::SmallVector inputs; - llvm::SmallVector outputs; - std::vector additionalAssignments; - - // Insert regular LLVM IR arguments. - llvm::SmallVector arguments; - for (llvm::Argument& arg : callee->args()) { - arguments.push_back(&arg); + if (callee->isDeclaration() && callee->getName() == CheckRegistry::ErrorFunctionName) { + assert(exit->isError() && "The target location of a 'gazer.error_code' call must be an error location!"); + + llvm::Value* arg = call->getArgOperand(0); + ExprPtr errorCodeExpr = operand(arg); + mCfa->addErrorCode(exit, errorCodeExpr); + return true; + } else if (callee->isDeclaration()) { + // Try to handle this value as a special function. + if (mGenCtx.getSpecialFunctions().handle(call, callerEP)) { + return true; } + } - for (size_t i = 0; i < call->getNumArgOperands(); ++i) { - ExprPtr expr = this->operand(call->getArgOperand(i)); - Variable* input = calledAutomatonInfo.findInput(arguments[i]); - assert(input != nullptr && "Function arguments should be present as procedure inputs!"); + if (callee->getName().startswith("gazer.")) { + return true; + } - inputs.emplace_back(input, expr); - } + if (!mGenCtx.hasInfoFor(callee)) { + Cfa* calledCfa = (*entry)->getAutomaton()->getParent().createCfa(callee->getName(), false); + auto& it = mGenCtx.createFunctionCfaInfo(calledCfa, callee); + } - // Insert arguments coming from the memory model. - AutomatonInterfaceExtensionPoint calleeEP(calledAutomatonInfo); + // If there is a declaration or there is no special function to handle, generate a call + CfaGenInfo& calledAutomatonInfo = mGenCtx.getFunctionCfa(callee); + Cfa* calledCfa = calledAutomatonInfo.Automaton; - // FIXME: This const_cast is needed because the memory model interface must - // take a mutable call site as ImmutableCallSite objects cannot be put into - // a map properly. This should be removed as soon as something about that changes. - mMemoryInstHandler.handleCall(const_cast(call), callerEP, calleeEP, inputs, outputs); - if (!callee->getReturnType()->isVoidTy()) { - Variable* variable = getVariable(call); + // Split the current transition here and create a call. + Location* callBegin = mCfa->createLocation(); + Location* callEnd = mCfa->createLocation(); - // Find the return variable of this function. - Variable* retval = mGenCtx.getFunctionCfa(callee).ReturnVariable; - assert(retval != nullptr && "A non-void function must have a return value!"); - - outputs.emplace_back(variable, retval->getRefExpr()); - } + mCfa->createAssignTransition(*entry, callBegin, previousAssignments); + previousAssignments.clear(); + + llvm::SmallVector inputs; + llvm::SmallVector outputs; + std::vector additionalAssignments; - mCfa->createCallTransition(callBegin, callEnd, calledCfa, inputs, outputs); + // Insert regular LLVM IR arguments. + llvm::SmallVector arguments; + for (llvm::Argument& arg : callee->args()) { + arguments.push_back(&arg); + } - // Continue the translation from the end location of the call. - *entry = callEnd; + llvm::errs() << call->getNumArgOperands() << "\n"; + llvm::errs() << callee->getName() << "\n"; + for (size_t i = 0; i < call->getNumArgOperands(); ++i) { + ExprPtr expr = this->operand(call->getArgOperand(i)); + Variable* input = calledAutomatonInfo.findInput(arguments[i]); + assert(input != nullptr && "Function arguments should be present as procedure inputs!"); - // Do not generate an assignment for this call. - return false; + inputs.emplace_back(input, expr); } - - if (callee->getName() == CheckRegistry::ErrorFunctionName) { - assert(exit->isError() && "The target location of a 'gazer.error_code' call must be an error location!"); - - llvm::Value* arg = call->getArgOperand(0); - ExprPtr errorCodeExpr = operand(arg); - mCfa->addErrorCode(exit, errorCodeExpr); - } else { - // Try to handle this value as a special function. - mGenCtx.getSpecialFunctions().handle(call, callerEP); + + // Insert arguments coming from the memory model. + AutomatonInterfaceExtensionPoint calleeEP(calledAutomatonInfo); + + // FIXME: This const_cast is needed because the memory model interface must + // take a mutable call site as ImmutableCallSite objects cannot be put into + // a map properly. This should be removed as soon as something about that changes. + mMemoryInstHandler.handleCall(const_cast(call), callerEP, calleeEP, inputs, outputs); + + if (!callee->getReturnType()->isVoidTy()) { + Variable* variable = getVariable(call); + + // Find the return variable of this function. + Variable* retval = mGenCtx.getFunctionCfa(callee).ReturnVariable; + assert(retval != nullptr && "A non-void function must have a return value!"); + + outputs.emplace_back(variable, retval->getRefExpr()); } - return true; + mCfa->createCallTransition(callBegin, callEnd, calledCfa, inputs, outputs); + + // Continue the translation from the end location of the call. + *entry = callEnd; + + // Do not generate an assignment for this call. + return false; } void BlocksToCfa::handleTerminator(const llvm::BasicBlock* bb, Location* entry, Location* exit) From 09161a8b77e1ea99e569094d9c01f6ff4e66a04e Mon Sep 17 00:00:00 2001 From: rl555 Date: Mon, 31 Aug 2020 18:04:12 +0200 Subject: [PATCH 35/47] Fix test, add more sub testcases --- .../generated/contracts/annotations | 2 ++ .../generated/contracts/ea_stub.xcfa | 14 ++++++++------ .../SimpleTestCase/generated/contracts/index | 8 +++++++- test/rte/SimpleTestCase/run.config | 19 +++++++++++++++++-- test/rte/SimpleTestCase/src/re_fixptr_test.c | 11 +++++++++++ test/rte/SimpleTestCase/src/re_test.c | 7 ------- .../SimpleTestCase/src/re_test_double_enter.c | 9 +++++++++ .../SimpleTestCase/src/re_test_double_exit.c | 8 ++++++++ .../rte/SimpleTestCase/src/re_test_no_enter.c | 6 ++++++ test/rte/SimpleTestCase/src/re_test_no_exit.c | 6 ++++++ test/rte/SimpleTestCase/src/re_test_ok.c | 7 +++++++ .../SimpleTestCase/src/re_test_ok_double.c | 9 +++++++++ .../rte/SimpleTestCase/src/re_test_ok_empty.c | 5 +++++ 13 files changed, 95 insertions(+), 16 deletions(-) create mode 100644 test/rte/SimpleTestCase/src/re_fixptr_test.c delete mode 100644 test/rte/SimpleTestCase/src/re_test.c create mode 100644 test/rte/SimpleTestCase/src/re_test_double_enter.c create mode 100644 test/rte/SimpleTestCase/src/re_test_double_exit.c create mode 100644 test/rte/SimpleTestCase/src/re_test_no_enter.c create mode 100644 test/rte/SimpleTestCase/src/re_test_no_exit.c create mode 100644 test/rte/SimpleTestCase/src/re_test_ok.c create mode 100644 test/rte/SimpleTestCase/src/re_test_ok_double.c create mode 100644 test/rte/SimpleTestCase/src/re_test_ok_empty.c diff --git a/test/rte/SimpleTestCase/generated/contracts/annotations b/test/rte/SimpleTestCase/generated/contracts/annotations index e69de29b..49dfb5dc 100644 --- a/test/rte/SimpleTestCase/generated/contracts/annotations +++ b/test/rte/SimpleTestCase/generated/contracts/annotations @@ -0,0 +1,2 @@ +fixPtr_five re_fixptr_test fixptr +fixPtr_three re_fixptr_test fixptr diff --git a/test/rte/SimpleTestCase/generated/contracts/ea_stub.xcfa b/test/rte/SimpleTestCase/generated/contracts/ea_stub.xcfa index 8d006542..2119a857 100644 --- a/test/rte/SimpleTestCase/generated/contracts/ea_stub.xcfa +++ b/test/rte/SimpleTestCase/generated/contracts/ea_stub.xcfa @@ -2,8 +2,8 @@ main process main_process { var locked__test : bool procedure Enter_test() { init loc L0 - error loc L1 - final loc LE + final loc L1 + error loc LE L0 -> L1 { assume not locked__test locked__test := true @@ -14,20 +14,22 @@ main process main_process { } procedure Exit_test() { init loc L0 - error loc L1 - final loc LE + final loc L1 + error loc LE L0 -> L1 { assume locked__test locked__test := false } L0 -> LE { - assume locked__test + assume not locked__test } } procedure ctor_locked__test() { init loc L0 final loc L1 - L0 -> L1 { } + L0 -> L1 { + locked__test := false + } } procedure dtor_locked__test() { init loc L0 diff --git a/test/rte/SimpleTestCase/generated/contracts/index b/test/rte/SimpleTestCase/generated/contracts/index index 0a765def..9b87ec6c 100644 --- a/test/rte/SimpleTestCase/generated/contracts/index +++ b/test/rte/SimpleTestCase/generated/contracts/index @@ -1 +1,7 @@ -re_test ea_stub.xcfa +re_test_ok ea_stub.xcfa +re_test_ok_empty ea_stub.xcfa +re_test_ok_double ea_stub.xcfa +re_test_no_enter ea_stub.xcfa +re_test_no_exit ea_stub.xcfa +re_test_double_enter ea_stub.xcfa +re_test_double_exit ea_stub.xcfa diff --git a/test/rte/SimpleTestCase/run.config b/test/rte/SimpleTestCase/run.config index 8f9c5cd6..f7893e31 100644 --- a/test/rte/SimpleTestCase/run.config +++ b/test/rte/SimpleTestCase/run.config @@ -1,3 +1,18 @@ -// RUN: %theta-re "%S" | FileCheck "%s" +// RUN: %theta-re "%S" > "%t" && cat "%t" && FileCheck "%s" < "%t" -// CHECK: Verification FAILED +// CHECK: Running re_fixptr_test +// CHECK: Verification SUCCESSFUL. +// CHECK: Running re_test_double_enter +// CHECK: Verification FAILED. +// CHECK: Running re_test_double_exit +// CHECK: Verification FAILED. +// CHECK: Running re_test_no_enter +// CHECK: Verification FAILED. +// CHECK: Running re_test_no_exit +// CHECK: Verification FAILED. +// CHECK: Running re_test_ok +// CHECK: Verification SUCCESSFUL. +// CHECK: Running re_test_ok_double +// CHECK: Verification SUCCESSFUL. +// CHECK: Running re_test_ok_empty +// CHECK: Verification SUCCESSFUL. diff --git a/test/rte/SimpleTestCase/src/re_fixptr_test.c b/test/rte/SimpleTestCase/src/re_fixptr_test.c new file mode 100644 index 00000000..5ffc54a5 --- /dev/null +++ b/test/rte/SimpleTestCase/src/re_fixptr_test.c @@ -0,0 +1,11 @@ +#include + +int* fixPtr_five(void); +int* fixPtr_three(void); + +void re_fixptr_test() { + *fixPtr_five() = 5; + *fixPtr_three() = 3; + assert(*fixPtr_five() == 5); + assert(*fixPtr_three() == 3); +} diff --git a/test/rte/SimpleTestCase/src/re_test.c b/test/rte/SimpleTestCase/src/re_test.c deleted file mode 100644 index a0a80868..00000000 --- a/test/rte/SimpleTestCase/src/re_test.c +++ /dev/null @@ -1,7 +0,0 @@ -void Enter_test(void); -void Exit_test(void); - -void re_test() { - Enter_test(); - Exit_test(); -} diff --git a/test/rte/SimpleTestCase/src/re_test_double_enter.c b/test/rte/SimpleTestCase/src/re_test_double_enter.c new file mode 100644 index 00000000..771aff87 --- /dev/null +++ b/test/rte/SimpleTestCase/src/re_test_double_enter.c @@ -0,0 +1,9 @@ +void Enter_test(void) __attribute__((used)); +void Exit_test(void) __attribute__((used)); + +void re_test_double_enter() { + Enter_test(); + Enter_test(); + Exit_test(); + Exit_test(); +} diff --git a/test/rte/SimpleTestCase/src/re_test_double_exit.c b/test/rte/SimpleTestCase/src/re_test_double_exit.c new file mode 100644 index 00000000..472caa2c --- /dev/null +++ b/test/rte/SimpleTestCase/src/re_test_double_exit.c @@ -0,0 +1,8 @@ +void Enter_test(void) __attribute__((used)); +void Exit_test(void) __attribute__((used)); + +void re_test_double_exit() { + Enter_test(); + Exit_test(); + Exit_test(); +} diff --git a/test/rte/SimpleTestCase/src/re_test_no_enter.c b/test/rte/SimpleTestCase/src/re_test_no_enter.c new file mode 100644 index 00000000..c4160921 --- /dev/null +++ b/test/rte/SimpleTestCase/src/re_test_no_enter.c @@ -0,0 +1,6 @@ +void Enter_test(void) __attribute__((used)); +void Exit_test(void) __attribute__((used)); + +void re_test_no_enter() { + Exit_test(); +} diff --git a/test/rte/SimpleTestCase/src/re_test_no_exit.c b/test/rte/SimpleTestCase/src/re_test_no_exit.c new file mode 100644 index 00000000..1d9de8a4 --- /dev/null +++ b/test/rte/SimpleTestCase/src/re_test_no_exit.c @@ -0,0 +1,6 @@ +void Enter_test(void) __attribute__((used)); +void Exit_test(void) __attribute__((used)); + +void re_test_no_exit() { + Enter_test(); +} diff --git a/test/rte/SimpleTestCase/src/re_test_ok.c b/test/rte/SimpleTestCase/src/re_test_ok.c new file mode 100644 index 00000000..be4fed5e --- /dev/null +++ b/test/rte/SimpleTestCase/src/re_test_ok.c @@ -0,0 +1,7 @@ +void Enter_test(void) __attribute__((used)); +void Exit_test(void) __attribute__((used)); + +void re_test_ok() { + Enter_test(); + Exit_test(); +} diff --git a/test/rte/SimpleTestCase/src/re_test_ok_double.c b/test/rte/SimpleTestCase/src/re_test_ok_double.c new file mode 100644 index 00000000..5e2fa201 --- /dev/null +++ b/test/rte/SimpleTestCase/src/re_test_ok_double.c @@ -0,0 +1,9 @@ +void Enter_test(void) __attribute__((used)); +void Exit_test(void) __attribute__((used)); + +void re_test_ok_double() { + Enter_test(); + Exit_test(); + Enter_test(); + Exit_test(); +} diff --git a/test/rte/SimpleTestCase/src/re_test_ok_empty.c b/test/rte/SimpleTestCase/src/re_test_ok_empty.c new file mode 100644 index 00000000..65346cf7 --- /dev/null +++ b/test/rte/SimpleTestCase/src/re_test_ok_empty.c @@ -0,0 +1,5 @@ +void Enter_test(void) __attribute__((used)); +void Exit_test(void) __attribute__((used)); + +void re_test_ok_empty() { +} From 6345a1bc26e96078e6963b92b82d89b87029f622 Mon Sep 17 00:00:00 2001 From: rl555 Date: Mon, 31 Aug 2020 18:05:23 +0200 Subject: [PATCH 36/47] Remove unneccessary print --- tools/gazer-theta/lib/ThetaVerifier.cpp | 1 - 1 file changed, 1 deletion(-) diff --git a/tools/gazer-theta/lib/ThetaVerifier.cpp b/tools/gazer-theta/lib/ThetaVerifier.cpp index a0a2a0e9..6c8851d4 100644 --- a/tools/gazer-theta/lib/ThetaVerifier.cpp +++ b/tools/gazer-theta/lib/ThetaVerifier.cpp @@ -126,7 +126,6 @@ auto ThetaVerifierImpl::execute(llvm::StringRef input) -> std::unique_ptr args = { "java", From d1e70a45024cac29ae07b6911b332587ed58d9a3 Mon Sep 17 00:00:00 2001 From: rl555 Date: Mon, 31 Aug 2020 18:06:27 +0200 Subject: [PATCH 37/47] Fix driver Provide annotations via a horrible function definition AnnotateSpecialFunctions must use weak reference for it's definition... getline does not work as expected when using the same source for Windows and Linux. Remove unnecessary prints --- tools/gazer-theta/gazer-theta-re.cpp | 51 ++++++++++++++++++++++------ 1 file changed, 40 insertions(+), 11 deletions(-) diff --git a/tools/gazer-theta/gazer-theta-re.cpp b/tools/gazer-theta/gazer-theta-re.cpp index 5eb858f2..d173529a 100644 --- a/tools/gazer-theta/gazer-theta-re.cpp +++ b/tools/gazer-theta/gazer-theta-re.cpp @@ -20,6 +20,19 @@ using namespace gazer; using namespace llvm; +namespace { + std::map> currentAnnotations; +} + +/// used by AnnotateSpecialFunctionsPass (rip) +std::vector getAnnotationsFor(std::string functionName) { + auto it = currentAnnotations.find(functionName); + if (it == currentAnnotations.end()) { + return std::vector(); + } + return it->second; +} + namespace { @@ -76,6 +89,19 @@ namespace gazer static theta::ThetaSettings initSettingsFromCommandLine(); +namespace { + +/// removes leftover newlines, problem on cross-platform installations +int good_getline(std::istream& ifs, std::string& tmp) { + if (!std::getline(ifs, tmp)) { + return 0; + } + if (tmp.size() && tmp[tmp.size()-1] == '\r' ) { + tmp = tmp.substr( 0, tmp.size() - 1 ); + } + return 1; +} + std::vector runnables() { const std::string target_path(InputFilename + "/src/"); const boost::regex my_filter(".*\\.c"); @@ -97,7 +123,8 @@ std::vector runnables() { return std::move(all_matching_files); } -using AnnotationMap = std::map>; +// Runnable -> {Function -> [Annotation]} +using AnnotationMap = std::map>>; AnnotationMap annotations() { @@ -107,7 +134,7 @@ AnnotationMap annotations() { std::vector lines; { std::string tmp; - while (std::getline(ifs, tmp)) { + while (good_getline(ifs, tmp)) { lines.push_back(std::move(tmp)); } } @@ -121,9 +148,11 @@ AnnotationMap annotations() { if (tokens.size() == 0) { continue; } - auto& re = tokens[0]; - std::vector annotations(std::next(tokens.begin()), tokens.end()); - result[re] = annotations; + auto& func = tokens[0]; + auto& re = tokens[1]; + std::vector annotations(tokens.begin()+2, tokens.end()); + result.try_emplace(re); + result[re][func] = annotations; } return result; } @@ -138,7 +167,7 @@ XcfaMap xcfas() { std::vector lines; { std::string tmp; - while (std::getline(ifs, tmp)) { + while (good_getline(ifs, tmp)) { lines.push_back(std::move(tmp)); } } @@ -154,12 +183,13 @@ XcfaMap xcfas() { } auto& re = tokens[0]; std::vector xcfas(std::next(tokens.begin()), tokens.end()); - llvm::errs() << xcfas[0] << "\n"; result[re] = xcfas; } return result; } +} + int main(int argc, char* argv[]) { cl::HideUnrelatedOptions({ @@ -210,13 +240,10 @@ int main(int argc, char* argv[]) for (auto& runnable : runnableList) { std::string file = InputFilename + "/src/" + runnable + ".c"; - llvm::errs() << "Runnable " << runnable << " has file " << file << "\n"; // Find matching annotations auto it = annots.find(runnable); if (it != annots.end()) { - for (auto annot : it->second) { - llvm::errs() << "Annotation " << annot << "\n"; - } + currentAnnotations = it->second; } // Run the frontend @@ -240,6 +267,8 @@ int main(int argc, char* argv[]) return 1; } + llvm::outs() << "Running " << runnable << "\n"; + frontend->setBackendAlgorithm(new theta::ThetaVerifier(backendSettings)); frontend->registerVerificationPipeline(); frontend->run(); From 6451ac37be198a6cedad15df4a690b9fab909b25 Mon Sep 17 00:00:00 2001 From: rl555 Date: Mon, 31 Aug 2020 18:09:50 +0200 Subject: [PATCH 38/47] Remove unnecessary prints --- src/LLVM/Automaton/ModuleToAutomata.cpp | 2 -- 1 file changed, 2 deletions(-) diff --git a/src/LLVM/Automaton/ModuleToAutomata.cpp b/src/LLVM/Automaton/ModuleToAutomata.cpp index eaa599ad..c30fef96 100644 --- a/src/LLVM/Automaton/ModuleToAutomata.cpp +++ b/src/LLVM/Automaton/ModuleToAutomata.cpp @@ -615,8 +615,6 @@ bool BlocksToCfa::handleCall(const llvm::CallInst* call, Location** entry, Locat arguments.push_back(&arg); } - llvm::errs() << call->getNumArgOperands() << "\n"; - llvm::errs() << callee->getName() << "\n"; for (size_t i = 0; i < call->getNumArgOperands(); ++i) { ExprPtr expr = this->operand(call->getArgOperand(i)); Variable* input = calledAutomatonInfo.findInput(arguments[i]); From 5bfd89199c2cb4dfe926d7409c3b355b3c96c7ce Mon Sep 17 00:00:00 2001 From: rl555 Date: Mon, 31 Aug 2020 18:10:24 +0200 Subject: [PATCH 39/47] Move simplify special functions pass --- src/LLVM/LLVMFrontend.cpp | 6 ++---- 1 file changed, 2 insertions(+), 4 deletions(-) diff --git a/src/LLVM/LLVMFrontend.cpp b/src/LLVM/LLVMFrontend.cpp index 550035af..e546dcb0 100644 --- a/src/LLVM/LLVMFrontend.cpp +++ b/src/LLVM/LLVMFrontend.cpp @@ -146,7 +146,8 @@ void LLVMFrontend::registerVerificationPipeline() mPassManager.add(gazer::createNormalizeVerifierCallsPass()); registerEnabledChecks(); - // mutex check needs a promotion + // Simplify special functions + mPassManager.add(gazer::createSimplifySpecialFunctionsPass()); mPassManager.add(llvm::createPromoteMemoryToRegisterPass()); // Execute early optimization passes. @@ -159,9 +160,6 @@ void LLVMFrontend::registerVerificationPipeline() // Unify function exit nodes mPassManager.add(llvm::createUnifyFunctionExitNodesPass()); - // Simplify special functions - mPassManager.add(gazer::createSimplifySpecialFunctionsPass()); - // Run assertion lifting. if (mSettings.liftAsserts) { mPassManager.add(new llvm::CallGraphWrapperPass()); From c04c1da9f63f7eabe85c9d1402c9172799492a03 Mon Sep 17 00:00:00 2001 From: rl555 Date: Mon, 31 Aug 2020 18:11:06 +0200 Subject: [PATCH 40/47] Wire Annotations through file, small fixes AnnotationSpecialFunction uses a horrible function reference to get a list of annotations for a specific functions. Rte tests are stable --- .../AnnotateSpecialFunctions.cpp | 88 ++++++++----------- 1 file changed, 39 insertions(+), 49 deletions(-) diff --git a/src/LLVM/Instrumentation/AnnotateSpecialFunctions.cpp b/src/LLVM/Instrumentation/AnnotateSpecialFunctions.cpp index c1ca0739..b1e56e39 100644 --- a/src/LLVM/Instrumentation/AnnotateSpecialFunctions.cpp +++ b/src/LLVM/Instrumentation/AnnotateSpecialFunctions.cpp @@ -23,73 +23,63 @@ #include "llvm/IR/Module.h" #include "llvm/Support/Debug.h" +#include + using namespace llvm; +// Implemented by gazer-theta-re.cpp :'( +// TODO This is ugly +__attribute__((weak)) std::vector getAnnotationsFor(std::string functionName) { + return {}; +} +//extern std::vector getAnnotationsFor(std::string functionName); + namespace { class AnnotateSpecialFunctionsPass : public ModulePass { + std::unordered_set fixptrs; public: AnnotateSpecialFunctionsPass() : ModulePass(ID) {} - bool runOnModule(Module& m) override { - bool res = false; - SmallVector toProcess; - for (auto& f : m.functions()) { - for (auto& bb: f) { - for (auto& inst : bb) { - if (auto* callInst = dyn_cast(&inst)) { - toProcess.push_back(callInst); - } - } - } + bool runOnModule(llvm::Module& m) override { + for (auto& f: m.functions()) { + processFunction(f); } - for (auto* callInst : toProcess) { - res |= processInstruction(m, *callInst); - } - return res; + return true; } -public: - static char ID; - -private: + bool processFunction(Function& func) { + for (std::string annot : getAnnotationsFor(func.getName())) { + if (annot == "fixptr") { + bool ok = true; + if (func.arg_size() != 0) { + func.getContext().emitError("FixPtr calls must have zero parameters\n"); + ok = false; + // do not return for more checks + } + if (!func.getFunctionType()->getReturnType()->isPointerTy()) { + func.getContext().emitError("FixPtr calls must have pointer return type\n"); + ok = false; + } + if (!ok) { + // no change + return false; + } - bool processInstruction(Module& m, CallInst& inst) { - auto enterExitCounterType = Type::getInt32Ty(m.getContext()); - // known API functions - if (inst.getCalledFunction()->getName().startswith("FixPtr")) { - auto varName = ("gazer." + inst.getCalledFunction()->getName()).str(); + //fixptrs.insert(&func); - bool ok = true; - if (inst.getNumArgOperands() != 0) { - m.getContext().emitError(&inst, "FixPtr calls must have zero parameters\n"); - ok = false; - // do not return for more checks - } - if (!inst.getFunctionType()->getReturnType()->isPointerTy()) { - m.getContext().emitError(&inst, "FixPtr calls must have pointer return type\n"); - ok = false; + func.setSpeculatable(); + func.setDoesNotAccessMemory(); + func.setReturnDoesNotAlias(); + return true; // TODO what happens with multiple annotations on a single call? } - if (!ok) { - // no change - return false; - } - - inst.setDoesNotAccessMemory(); - inst.getCalledFunction()->setSpeculatable(); - inst.getCalledFunction()->setDoesNotAccessMemory(); - inst.getCalledFunction()->setReturnDoesNotAlias(); - return true; } - // known intrinsics - if (inst.getCalledFunction()->getName().startswith("gazer.") || - inst.getCalledFunction()->getName().startswith("llvm.")) { - return false; - } - errs() << "WARNING: unknown function " << *(inst.getCalledFunction()) << "\n"; return false; } +public: + static char ID; + }; } From 19cb98ebded71db40354ed2a2dbd57cf986a976c Mon Sep 17 00:00:00 2001 From: rl555 <68019200+rl555@users.noreply.github.com> Date: Tue, 1 Sep 2020 12:59:39 +0200 Subject: [PATCH 41/47] Add setting udevelopment environment to README.md --- README.md | 42 ++++++++++++++++++++++++++++++++++++++++++ 1 file changed, 42 insertions(+) diff --git a/README.md b/README.md index 6d49b917..97743efc 100644 --- a/README.md +++ b/README.md @@ -107,3 +107,45 @@ $ clang example.c harness.ll -o example_test $ ./example_test [1] 19948 floating point exception (core dumped) ./example_test ``` + +## Development on Windows + +One possibility, devised here, is to install Docker, and use it as a Linux subsystem. + +After installing Docker, one must create an image, that is capable of running the tests. + +- Install docker +- Download gazer project and theta project and LLVM source code (later referred to as `$HOST_THETA_DIR` and `$HOST_GAZER_DIR`, `$HOST_LLVM_DIR`). +- Modify gazer's dockerfile to include `lit` (used in regression tests) and it's necessary components: `psutil` (for handling case-by-case timeouts) +- Modify gazer's dockerfile to use theta project's source code instead of downloading the source. +- Mount Theta and Gazer, LLVM inside Docker. Publish port 8000: + + `docker run -i -t -p 127.0.0.1:8000:8000 --name dev-container --mount type=bind,source="$HOST_THETA_DIR\theta",target=/host/theta --mount type=bind,source="$HOST_LLVM_DIR/theta",target=/host/llvm --mount type=bind,source="C:\Workspaces\Theta-dev\gazer",target=/host/gazer theta-gazer-dev bash` + +- When first running, run LLVM's CMakefile with the proper configuration, and generate Makefiles. This (binding LLVM) is used to be able to import LLVM as a project and use its' sources (and comments) for development. +- When first running, it's a good idea to create scripts capable of handling basic usage: + + ```sh + # build java + cd /host/theta + ./gradlew :theta-xcfa-cli:shadowJar + ``` + + ```sh + # bulid gazer + cd /host/gazer/build + make gazer-theta-re + ``` + + ```sh + # run gazer's regression tests with necessary options + GAZER_TOOLS_DIR=/host/gazer/build/tools + make check-functional + ``` + + ```sh + # run gazer with necessary options. + /host/gazer/build/tools/gazer-theta/gazer-theta-re --inline=off --no-assert-lift --theta-path=/host/theta/subprojects/xcfa-cli/build/libs/theta-xcfa-cli-0.0.1-SNAPSHOT-all.jar --lib-path=/host/theta/lib/ "$@" + ``` + + (TBD) From 346b0792ab2cddcef11f41048efeadcdfea03f8b Mon Sep 17 00:00:00 2001 From: rl555 <68019200+rl555@users.noreply.github.com> Date: Wed, 2 Sep 2020 12:52:38 +0200 Subject: [PATCH 42/47] Update README.md --- README.md | 56 ++++++++++++++++++++++++++++++++++++++++++++++++++----- 1 file changed, 51 insertions(+), 5 deletions(-) diff --git a/README.md b/README.md index 97743efc..5279dc90 100644 --- a/README.md +++ b/README.md @@ -120,23 +120,69 @@ After installing Docker, one must create an image, that is capable of running th - Modify gazer's dockerfile to use theta project's source code instead of downloading the source. - Mount Theta and Gazer, LLVM inside Docker. Publish port 8000: - `docker run -i -t -p 127.0.0.1:8000:8000 --name dev-container --mount type=bind,source="$HOST_THETA_DIR\theta",target=/host/theta --mount type=bind,source="$HOST_LLVM_DIR/theta",target=/host/llvm --mount type=bind,source="C:\Workspaces\Theta-dev\gazer",target=/host/gazer theta-gazer-dev bash` + ```sh + docker run -i -t -p 127.0.0.1:8000:8000 --name dev-container \ + --mount type=bind,source="$HOST_THETA_DIR/theta",target=/host/theta \ + --mount type=bind,source="$HOST_LLVM_DIR/theta",target=/host/llvm \ + --mount type=bind,source="C:\Workspaces\Theta-dev\gazer",target=/host/gazer \ + theta-gazer-dev bash` + ``` + + ```dev.dockerfile + FROM ubuntu:18.04 + + RUN apt-get update && \ + apt-get install -y build-essential git cmake \ + wget sudo vim lsb-release \ + software-properties-common zlib1g-dev \ + openjdk-11-jdk + + # fetch LLVM and other dependencies + RUN wget -O - https://apt.llvm.org/llvm-snapshot.gpg.key | apt-key add - && \ + add-apt-repository "deb http://apt.llvm.org/bionic/ llvm-toolchain-bionic-9 main" && \ + apt-get update && \ + add-apt-repository ppa:mhier/libboost-latest && \ + apt-get update && \ + apt-get install -y clang-9 llvm-9-dev llvm-9-tools llvm-9-runtime libboost1.70-dev && \ + ln -s `which clang-9` /usr/bin/clang && \ + ln -s `which llvm-link-9` /usr/bin/llvm-link && \ + ln -s /usr/lib/llvm-9/build/utils/lit/lit.py /usr/bin/lit && \ + ln -s /usr/lib/llvm-9/bin/FileCheck /usr/bin/FileCheck && \ + + # create a new user `user` with the password `user` and sudo rights + RUN useradd -m user && \ + echo user:user | chpasswd && \ + cp /etc/sudoers /etc/sudoers.bak && \ + echo 'user ALL=(root) NOPASSWD: ALL' >> /etc/sudoers + + USER user + + ENV GAZER_DIR /host/gazer + ENV THETA_DIR /host/theta + + COPY ./build.sh /host/build.sh + COPY ./first-run.sh /host/first-run.sh + + WORKDIR $GAZER_DIR + CMD /bin/bash + ``` - When first running, run LLVM's CMakefile with the proper configuration, and generate Makefiles. This (binding LLVM) is used to be able to import LLVM as a project and use its' sources (and comments) for development. - When first running, it's a good idea to create scripts capable of handling basic usage: + Useful commands/scripts for use inside Docker ```sh - # build java + # build Theta (xcfa only) cd /host/theta ./gradlew :theta-xcfa-cli:shadowJar ``` ```sh - # bulid gazer + # bulid gazer (runnable-entity checker only) cd /host/gazer/build make gazer-theta-re ``` - + ```sh # run gazer's regression tests with necessary options GAZER_TOOLS_DIR=/host/gazer/build/tools @@ -145,7 +191,7 @@ After installing Docker, one must create an image, that is capable of running th ```sh # run gazer with necessary options. - /host/gazer/build/tools/gazer-theta/gazer-theta-re --inline=off --no-assert-lift --theta-path=/host/theta/subprojects/xcfa-cli/build/libs/theta-xcfa-cli-0.0.1-SNAPSHOT-all.jar --lib-path=/host/theta/lib/ "$@" + /host/gazer/build/tools/gazer-theta/gazer-theta-re --theta-path=/host/theta/subprojects/xcfa-cli/build/libs/theta-xcfa-cli-0.0.1-SNAPSHOT-all.jar --lib-path=/host/theta/lib/ "$@" ``` (TBD) From 67c1a023de702d695d3908a5eb07fedab8149db9 Mon Sep 17 00:00:00 2001 From: rl555 <68019200+rl555@users.noreply.github.com> Date: Wed, 2 Sep 2020 14:12:32 +0200 Subject: [PATCH 43/47] Update README.md --- README.md | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/README.md b/README.md index 5279dc90..94768af9 100644 --- a/README.md +++ b/README.md @@ -124,7 +124,7 @@ After installing Docker, one must create an image, that is capable of running th docker run -i -t -p 127.0.0.1:8000:8000 --name dev-container \ --mount type=bind,source="$HOST_THETA_DIR/theta",target=/host/theta \ --mount type=bind,source="$HOST_LLVM_DIR/theta",target=/host/llvm \ - --mount type=bind,source="C:\Workspaces\Theta-dev\gazer",target=/host/gazer \ + --mount type=bind,source="$HOST_GAZER_DIR\gazer",target=/host/gazer \ theta-gazer-dev bash` ``` From fb2984c454b1acdcd990d8ee1f52e63be6d1d309 Mon Sep 17 00:00:00 2001 From: rl555 <68019200+rl555@users.noreply.github.com> Date: Wed, 2 Sep 2020 14:41:52 +0200 Subject: [PATCH 44/47] Update README.md --- README.md | 5 +---- 1 file changed, 1 insertion(+), 4 deletions(-) diff --git a/README.md b/README.md index 94768af9..a46f16d5 100644 --- a/README.md +++ b/README.md @@ -147,7 +147,7 @@ After installing Docker, one must create an image, that is capable of running th ln -s `which clang-9` /usr/bin/clang && \ ln -s `which llvm-link-9` /usr/bin/llvm-link && \ ln -s /usr/lib/llvm-9/build/utils/lit/lit.py /usr/bin/lit && \ - ln -s /usr/lib/llvm-9/bin/FileCheck /usr/bin/FileCheck && \ + ln -s /usr/lib/llvm-9/bin/FileCheck /usr/bin/FileCheck # create a new user `user` with the password `user` and sudo rights RUN useradd -m user && \ @@ -160,9 +160,6 @@ After installing Docker, one must create an image, that is capable of running th ENV GAZER_DIR /host/gazer ENV THETA_DIR /host/theta - COPY ./build.sh /host/build.sh - COPY ./first-run.sh /host/first-run.sh - WORKDIR $GAZER_DIR CMD /bin/bash ``` From 20ee2c477252ea705a6edcb8a0e141529d8009ca Mon Sep 17 00:00:00 2001 From: rl555 <68019200+rl555@users.noreply.github.com> Date: Wed, 2 Sep 2020 14:44:17 +0200 Subject: [PATCH 45/47] Update README.md --- README.md | 5 +++-- 1 file changed, 3 insertions(+), 2 deletions(-) diff --git a/README.md b/README.md index a46f16d5..5d9ecb48 100644 --- a/README.md +++ b/README.md @@ -135,10 +135,11 @@ After installing Docker, one must create an image, that is capable of running th apt-get install -y build-essential git cmake \ wget sudo vim lsb-release \ software-properties-common zlib1g-dev \ - openjdk-11-jdk + openjdk-11-jdk python3-pip # fetch LLVM and other dependencies - RUN wget -O - https://apt.llvm.org/llvm-snapshot.gpg.key | apt-key add - && \ + RUN pip install psutil && \ + wget -O - https://apt.llvm.org/llvm-snapshot.gpg.key | apt-key add - && \ add-apt-repository "deb http://apt.llvm.org/bionic/ llvm-toolchain-bionic-9 main" && \ apt-get update && \ add-apt-repository ppa:mhier/libboost-latest && \ From 764f1382b45759e6ee0cbf6fb6c17d579eca9b6b Mon Sep 17 00:00:00 2001 From: rl555 <68019200+rl555@users.noreply.github.com> Date: Wed, 2 Sep 2020 14:50:36 +0200 Subject: [PATCH 46/47] Update README.md --- README.md | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/README.md b/README.md index 5d9ecb48..4fbf1eb6 100644 --- a/README.md +++ b/README.md @@ -138,7 +138,7 @@ After installing Docker, one must create an image, that is capable of running th openjdk-11-jdk python3-pip # fetch LLVM and other dependencies - RUN pip install psutil && \ + RUN pip3 install psutil && \ wget -O - https://apt.llvm.org/llvm-snapshot.gpg.key | apt-key add - && \ add-apt-repository "deb http://apt.llvm.org/bionic/ llvm-toolchain-bionic-9 main" && \ apt-get update && \ From f10591f6297d8bc47f33e09691216b25e216f6fb Mon Sep 17 00:00:00 2001 From: rl555 Date: Thu, 3 Sep 2020 15:47:13 +0200 Subject: [PATCH 47/47] Add a document listing the changes in the xcfa branch with TODOs --- XCFA-ADDITIONS.md | 242 ++++++++++++++++++++++++++++++++++++++++++++++ 1 file changed, 242 insertions(+) create mode 100644 XCFA-ADDITIONS.md diff --git a/XCFA-ADDITIONS.md b/XCFA-ADDITIONS.md new file mode 100644 index 00000000..b6b609c5 --- /dev/null +++ b/XCFA-ADDITIONS.md @@ -0,0 +1,242 @@ +# Additions in XCFA branch + +`TODO merge with README.md and developer docs after stabilizing branch` + +`TODO add (back?) theta to lit tool for integration tests.` + +**Note:** All new files modify `CMakeLists.txt`, that is not listed unless for a non-trivial modification. + +## `TODO`: remove unnecessary modifications + +Some are annotated in Github. + +- `test/theta/cfa/Expected/counter.theta` + +## Disable loops to recursion transformation + +### What is it? + +Loop handling is important for only a small portion of code (specifically for Gazer's own BMC algorithm). +This is disabled. + +Loops (as a Gazer CFA) might have more than one output, which makes it incompatible with XCFA. + +### List of changed files + +- `FunctionToCfa.h` and `ModuleToAutomata.cpp`: infos are not passed around for loops; + These do *not* contain loop registration (as far as I've seen), only that must be disabled. + Uncomment is needed for BMC to work. + +### Further changes needed for merging with master + +`TODO add flag to disable loop transformations, force-disable loops when generating XCFA, force-enable for BMC. Probably CFA does not need this.` + +## XCFA generation + +### What is it? + +Generate XCFA instead of CFA. Globals are supported (with `Global variables support`) + +Tracing is disabled. + +Also some steps were taken to improve the code related to code generation. + +### List of changed files + +- `tools/gazer-theta` directory: no CFA can be generated as of now. Also contains some code improvements. + +### Further changes needed for merging with master + +`TODO create common code for CFA/XCFA generation, support both CFA and XCFA (CFA generation is missing)` + +`TODO error locations are supported on non-main functions, so global inlining pass is not needed` + +## Global variables support + +### What is it? + +Also added a GlobalVariableExtensionPoint to enable memory models declare global variables. + +### List of changed files + +- `ModuleToAutomata.cpp`: `declareGlobalVariables` is called here before the first function for the very +first memory instruction handler instance. + +- The `AutomataSystem` class in `Cfa.h` is patched to enable adding variables not attached to any CFA (hence, global). + Also added a way to iterate through them. + +### Further changes needed for merging with master + +## Simple memory model for globals and alloca'd locals + +### What is it? + +The simple memory models is a simple memory model asserting that there are no pointer-int casts, global arrays and +various pointer magic. + +There are broken assumptions made in Gazer, as there is no 'global' state assumed, everything is considered local. +Gazer's solution is to pass a memory object, as it is easier to reason about. With global variables handled in Theta, +this is not needed. + +Memory models are handled by-function. This clashes with the original global variable support. + +### List of changed files + +- `src/LLVM/Memory/SimpleMemoryModel.cpp`: Implementation. + +- `src/LLVM/Memory/MemoryModel.cpp`: removed havoc memory model, simple memory model is used instead. + Rework needed. + +### Further changes needed for merging with master + +`TODO memory models are handled by-function. This clashes with global variable support` + +`TODO remove hack that changes "havoc" implementation to simple memory model` + +## Swap function call with an inline LLVM implementation; decoupled analysis and inline implementation + +### What is it? + +Theta has some limitations (CFA or XCFA, whatever), and that limits our scope. Also, there are special knowledge around +some functions: e.g. malloc(n) returns a `dereferencable(n) noalias` pointer, but it's not `speculatable`. +See the LLVM reference for the meaning of these function attributes). + +Some special functions can be transformed in such a way that there is no pointer (magic) involved. + +There are two passes: one analyzing which functions have an implementation applicable to this (set of) transformation(s). + +Functions with `fixptr` (non-LLVM) annotation are transformed as such: + +```C +T* FixPtr(void) +T* variable = FixPtr() + +--- + +T FixPtr.fixptr = undef +T* variable = gazer.FixPtr.fixptr +``` + +Say, the hidden implementation is something trivial like `FixPtr(void) { return FixPtr_global; }`. + +**Note:** Currently there only one function handled; specific to a demo, and it does not have a similar STL function. + +Unknown functions with special signatures (returning or passing a parameter) must be such that + +### List of changed files + +- `src/LLVM/Instrumentation/AnnotateSpecialFunctions.cpp`: Adds in-LLVM annotations from some sources. + +- `src/LLVM/Instrumentation/SimplifySpecialFunctions.cpp`: Transforms the calls. Also this requires the + annotation pass. + +- `src/LLVM/LLVMFrontend.cpp`: Registers the pass to the pipeline. + + +### Further changes needed for merging with master + +`TODO rename passes, as the name clashes with SpecialFunctions interface of Gazer` + +`TODO find a good way to interface with AnnotateSpecialFunctions analysis pass` + +## Demo for non-reentrant mutex usage checks + +### What is it? + +A simple check, unused, may be deleted. + +Calls with the pattern `Enter*` and `Exit*` are transformed to have a check, when transformed to CFA. + +### List of changed files + +- `DefaultChecks.cpp` and some other. + +### Further changes needed for merging with master + +`TODO remove or move to separate file` + +## Support for handling functions without implementation in LLVM + +### What is it? + +Unimplemented functions are handled in a different way than in the original implementation: they were unknown +functions, which might return a value, and, as the implementations are unknown, they are converted havocing variable. + +Now this usage is broken, as they are now used, instead, as a way to include functions unknown to Gazer, but known to +Theta. + +Intrinsics are handled the same way as the original implementation. + +### List of changed files + +- `Callgraph.h` is patched to enable Calls with no nodes attached to the target. + +- The `AutomataSystem` class in `Cfa.h` is patched: createCfa might create a `Cfa` that is not registered to the + `AutomataSystem`. This is done to ensure iterating through CFAs one can be sure there is an implementation. + +- `FunctionToCfa.h` contains data attached to procedures. When a procedure is missing, there was an error. Added +a way to ask whether a function has related (generation) info. + +- `ModuleToAutomata.cpp`: `blocksToCfa` is created only for declared functions. + Unsure if this change is needed for the current implementation (as the generation context's procedures might not + actually contain the given procedures) + +- `BlocksToCfa::handleCall` in `ModuleToAutomata.cpp` is reordered, + `!callee->isDeclaration()` branch handles the new implementation. Original handling must `return true`, + nothing else is needed. (Like for gazer.*) No unrelated changes were made in this function. + +### Further changes needed for merging with master + +`TODO rename hasInfoFor(function)` to `isImplemented(function)`? + +`TODO add comment: only CFAs with implementation are registered; And to Cfa: One might not have an implementation` + +`TODO Gazer must know which functions are implemented at a later stage, as use-cases clash` + +`TODO generation context's procedures need not contain unimplemented procedures` + +## Passing stub XCFA files + +### What is it? + +Strongly coupled `Support for handling functions without implementation in LLVM`. + +The unimplemented functions can be defined in XCFA files in Theta. Not wired to a setting :( + +Merging is done through a recent addition to Theta XCFA. + +### List of changed files + +- `tools/gazer-theta/lib/ThetaVerifier.cpp`: Passing the list of XCFAs (instead of the single XCFA) to Theta. +- `tools/gazer-theta/lib/ThetaVerifier.h`: Adding list of XCFA files to the definition of configuration passed + around for Theta verification. + +### Further changes needed for merging with master + +`TODO wire this to command-line interface to gazer-theta` + +## New driver: gazer-theta-re + +### What is it? + +This is a demo-specific addition, but some parts can be reused, I think. + +Iterates through a list of `.c` files, and runs a modified workflow to it. + +The most important: it tells `AnnotateSpecialFunctions` pass which functions (unknown to Gazer) have special +implementations. Anyway, the way it does this is plain ugly (maybe Linux-specific?), so that one must be fixed. + +### List of changed files + +- `test/lit.cfg`: The directory structure for testing contains a `run.config` file, that must be parsed by `lit`. + Also the binary is linked so the configuration can use it. + +- `tools/gazer-theta/gazer-theta-re.cpp`: implementation + +- `test/rte`: test cases related to the new driver. + +- `tools/gazer-theta/lib/ThetaVerifier.cpp`: Multiple XCFA can be added. + +### Further changes needed for merging with master + +`TODO Merge common code with gazer-theta.cpp` \ No newline at end of file