From 5e400dab79618b14bac103b5819f2fee8b37221b Mon Sep 17 00:00:00 2001 From: Liam Machado Date: Mon, 18 Sep 2017 23:44:51 -0600 Subject: [PATCH 01/13] Added modifies clause generation for Boogie files. --- CMakeLists.txt | 2 + include/smack/BoogieAst.h | 72 +++++--- include/smack/GenModifies.h | 71 ++++++++ include/smack/SmackModuleGenerator.h | 2 + include/smack/SmackRep.h | 1 + lib/smack/GenModifies.cpp | 243 +++++++++++++++++++++++++++ lib/smack/SmackModuleGenerator.cpp | 2 + share/smack/top.py | 2 +- tools/llvm2bpl/llvm2bpl.cpp | 2 + 9 files changed, 376 insertions(+), 21 deletions(-) create mode 100644 include/smack/GenModifies.h create mode 100644 lib/smack/GenModifies.cpp diff --git a/CMakeLists.txt b/CMakeLists.txt index aeec6ef7c..d5df49a4a 100644 --- a/CMakeLists.txt +++ b/CMakeLists.txt @@ -175,6 +175,7 @@ add_library(smackTranslator STATIC include/smack/MemorySafetyChecker.h include/smack/SignedIntegerOverflowChecker.h include/smack/SplitAggregateLoadStore.h + include/smack/GenModifies.h lib/smack/AddTiming.cpp lib/smack/BoogieAst.cpp lib/smack/BplFilePrinter.cpp @@ -195,6 +196,7 @@ add_library(smackTranslator STATIC lib/smack/MemorySafetyChecker.cpp lib/smack/SignedIntegerOverflowChecker.cpp lib/smack/SplitAggregateLoadStore.cpp + lib/smack/GenModifies.cpp ) add_executable(llvm2bpl diff --git a/include/smack/BoogieAst.h b/include/smack/BoogieAst.h index cb8205756..4d6ea83a9 100644 --- a/include/smack/BoogieAst.h +++ b/include/smack/BoogieAst.h @@ -12,6 +12,16 @@ namespace smack { class Expr { public: + enum Kind { + BIN, COND, FUN, BOOL_LIT, INT_LIT, BV_LIT, FP_LIT, STRING_LIT, NEG, NOT, QUANT, SEL, UPD, VAR, CODE + }; +private: + const Kind kind; +protected: + Expr(Kind k) : kind(k) {} +public: + Kind getKind() const { return kind; } + virtual ~Expr() {} virtual void print(std::ostream& os) const = 0; static const Expr* exists(std::string v, std::string t, const Expr* e); @@ -50,8 +60,9 @@ class BinExpr : public Expr { const Expr* lhs; const Expr* rhs; public: - BinExpr(const Binary b, const Expr* l, const Expr* r) : op(b), lhs(l), rhs(r) {} + BinExpr(const Binary b, const Expr* l, const Expr* r) : Expr(BIN), op(b), lhs(l), rhs(r) {} void print(std::ostream& os) const; + static bool classof(const Expr *e) { return e->getKind() == BIN; } }; class CondExpr : public Expr { @@ -60,53 +71,59 @@ class CondExpr : public Expr { const Expr* else_; public: CondExpr(const Expr* c, const Expr* t, const Expr* e) - : cond(c), then(t), else_(e) {} + : Expr(COND), cond(c), then(t), else_(e) {} void print(std::ostream& os) const; + static bool classof(const Expr *e) { return e->getKind() == COND; } }; class FunExpr : public Expr { std::string fun; std::list args; public: - FunExpr(std::string f, std::list xs) : fun(f), args(xs) {} + FunExpr(std::string f, std::list xs) : Expr(FUN), fun(f), args(xs) {} void print(std::ostream& os) const; + static bool classof(const Expr *e) { return e->getKind() == FUN; } + std::list getArgs() const { return args; } }; class BoolLit : public Expr { bool val; public: - BoolLit(bool b) : val(b) {} + BoolLit(bool b) : Expr(BOOL_LIT), val(b) {} void print(std::ostream& os) const; + static bool classof(const Expr *e) { return e->getKind() == BOOL_LIT; } }; class IntLit : public Expr { std::string val; public: - IntLit(std::string v) : val(v) {} - IntLit(unsigned long v) { + IntLit(std::string v) : Expr(INT_LIT), val(v) {} + IntLit(unsigned long v) : Expr(INT_LIT) { std::stringstream s; s << v; val = s.str(); } - IntLit(long v) { + IntLit(long v) : Expr(INT_LIT) { std::stringstream s; s << v; val = s.str(); } void print(std::ostream& os) const; + static bool classof(const Expr *e) { return e->getKind() == INT_LIT; } }; class BvLit : public Expr { std::string val; unsigned width; public: - BvLit(std::string v, unsigned w) : val(v), width(w) {} - BvLit(unsigned long v, unsigned w) : width(w) { + BvLit(std::string v, unsigned w) : Expr(BV_LIT), val(v), width(w) {} + BvLit(unsigned long v, unsigned w) : Expr(BV_LIT), width(w) { std::stringstream s; s << v; val = s.str(); } void print(std::ostream& os) const; + static bool classof(const Expr *e) { return e->getKind() == BV_LIT; } }; class FPLit : public Expr { @@ -116,29 +133,33 @@ class FPLit : public Expr { unsigned sigSize; unsigned expSize; public: - FPLit(bool n, std::string s, std::string e, unsigned ss, unsigned es) : neg(n), sig(s), expo(e), sigSize(ss), expSize(es) {} + FPLit(bool n, std::string s, std::string e, unsigned ss, unsigned es) : Expr(FP_LIT), neg(n), sig(s), expo(e), sigSize(ss), expSize(es) {} void print(std::ostream& os) const; + static bool classof(const Expr *e) { return e->getKind() == FP_LIT; } }; class StringLit : public Expr { std::string val; public: - StringLit(std::string v) : val(v) {} + StringLit(std::string v) : Expr(STRING_LIT), val(v) {} void print(std::ostream& os) const; + static bool classof(const Expr *e) { return e->getKind() == STRING_LIT; } }; class NegExpr : public Expr { const Expr* expr; public: - NegExpr(const Expr* e) : expr(e) {} + NegExpr(const Expr* e) : Expr(NEG), expr(e) {} void print(std::ostream& os) const; + static bool classof(const Expr *e) { return e->getKind() == NEG; } }; class NotExpr : public Expr { const Expr* expr; public: - NotExpr(const Expr* e) : expr(e) {} + NotExpr(const Expr* e) : Expr(NOT), expr(e) {} void print(std::ostream& os) const; + static bool classof(const Expr *e) { return e->getKind() == NOT; } }; class QuantExpr : public Expr { @@ -149,17 +170,19 @@ class QuantExpr : public Expr { std::list< std::pair > vars; const Expr* expr; public: - QuantExpr(Quantifier q, std::list< std::pair > vs, const Expr* e) : quant(q), vars(vs), expr(e) {} + QuantExpr(Quantifier q, std::list< std::pair > vs, const Expr* e) : Expr(QUANT), quant(q), vars(vs), expr(e) {} void print(std::ostream& os) const; + static bool classof(const Expr *e) { return e->getKind() == QUANT; } }; class SelExpr : public Expr { const Expr* base; std::list idxs; public: - SelExpr(const Expr* a, std::list i) : base(a), idxs(i) {} - SelExpr(const Expr* a, const Expr* i) : base(a), idxs(std::list(1, i)) {} + SelExpr(const Expr* a, std::list i) : Expr(SEL), base(a), idxs(i) {} + SelExpr(const Expr* a, const Expr* i) : Expr(SEL), base(a), idxs(std::list(1, i)) {} void print(std::ostream& os) const; + static bool classof(const Expr *e) { return e->getKind() == SEL; } }; class UpdExpr : public Expr { @@ -168,18 +191,20 @@ class UpdExpr : public Expr { const Expr* val; public: UpdExpr(const Expr* a, std::list i, const Expr* v) - : base(a), idxs(i), val(v) {} + : Expr(UPD), base(a), idxs(i), val(v) {} UpdExpr(const Expr* a, const Expr* i, const Expr* v) - : base(a), idxs(std::list(1, i)), val(v) {} + : Expr(UPD), base(a), idxs(std::list(1, i)), val(v) {} void print(std::ostream& os) const; + static bool classof(const Expr *e) { return e->getKind() == UPD; } }; class VarExpr : public Expr { std::string var; public: - VarExpr(std::string v) : var(v) {} + VarExpr(std::string v) : Expr(VAR), var(v) {} std::string name() const { return var; } void print(std::ostream& os) const; + static bool classof(const Expr *e) { return e->getKind() == VAR; } }; class Attr { @@ -254,6 +279,8 @@ class AssignStmt : public Stmt { public: AssignStmt(std::list lhs, std::list rhs) : Stmt(ASSIGN), lhs(lhs), rhs(rhs) {} + std::list getlhs() const { return lhs; } + std::list getrhs() const { return rhs; } void print(std::ostream& os) const; static bool classof(const Stmt* S) { return S->getKind() == ASSIGN; } }; @@ -289,6 +316,10 @@ class CallStmt : public Stmt { std::list rets) : Stmt(CALL), proc(p), attrs(attrs), params(args), returns(rets) {} + std::string getName() const { return proc; } + std::list getAttrs() const { return attrs; } + std::list getParams() const { return params; } + std::list getReturns() const { return returns; } void print(std::ostream& os) const; static bool classof(const Stmt* S) { return S->getKind() == CALL; } }; @@ -486,8 +517,9 @@ class CodeContainer { class CodeExpr : public Expr, public CodeContainer { public: - CodeExpr(DeclarationList ds, BlockList bs) : CodeContainer(ds, bs) {} + CodeExpr(DeclarationList ds, BlockList bs) : Expr(CODE), CodeContainer(ds, bs) {} void print(std::ostream& os) const; + static bool classof(Expr *e) { return e->getKind() == CODE; } }; class ProcDecl : public Decl, public CodeContainer { diff --git a/include/smack/GenModifies.h b/include/smack/GenModifies.h new file mode 100644 index 000000000..0b52a52c8 --- /dev/null +++ b/include/smack/GenModifies.h @@ -0,0 +1,71 @@ +// +// This file is distributed under the MIT License. See LICENSE for details. +// +#ifndef MODS_H +#define MODS_H + +#include "smack/SmackModuleGenerator.h" +#include "smack/BoogieAst.h" +#include "llvm/Support/Regex.h" +#include +#include +#include + +namespace smack { + +using llvm::Regex; + +class GenModifies : public llvm::ModulePass { + +private: + std::stack st; + std::map onStack; + std::map index; + std::map low; + std::map SCCOfProc; + std::map proc; + std::vector> SCCGraph; + std::vector> modVars; + + int maxIndex; + + void initProcMap(Program *program); + void insertModifiesClause(Decl *&decl, Regex &PROC_DECL, const std::set &bplGlobals); + void genSmackCodeModifies(Program *program, const std::set &bplGlobals); + void addNewSCC(const std::string &procName); + void dfs(ProcDecl *curProc); + void genSCCs(Program *program); + void genSCCGraph(Program *program); + void addEdge(const CallStmt *callStmt, int parentSCC); + void addIfGlobalVar(std::string exprName, const std::string &procName); + void calcModifiesOfExprs(const std::list exprs, const std::string &procName); + void calcModifiesOfStmt(const Stmt *stmt, const std::string procName); + void calcModifiesOfSCCs(Program *program); + void propagateModifiesUpGraph(); + void addSmackGlobals(const std::set &bplGlobals); + void addModifies(Program *program); + void genUserCodeModifies(Program *program, const std::set &bplGlobals); + +public: + static char ID; // Pass identification, replacement for typeid + + GenModifies() : llvm::ModulePass(ID), maxIndex(1) { + SCCGraph.push_back(std::set()); + modVars.push_back(std::set()); + } + + virtual bool runOnModule(llvm::Module& m); + + virtual const char *getPassName() const { + return "Modifies clause generation"; + } + + virtual void getAnalysisUsage(llvm::AnalysisUsage& AU) const { + AU.setPreservesAll(); + AU.addRequired(); + } +}; +} + +#endif // MODS_H + diff --git a/include/smack/SmackModuleGenerator.h b/include/smack/SmackModuleGenerator.h index a3156e112..2c9047ced 100644 --- a/include/smack/SmackModuleGenerator.h +++ b/include/smack/SmackModuleGenerator.h @@ -13,6 +13,7 @@ class Program; class SmackModuleGenerator : public llvm::ModulePass { private: Program* program; + std::vector bplGlobals; public: static char ID; // Pass identification, replacement for typeid @@ -24,6 +25,7 @@ class SmackModuleGenerator : public llvm::ModulePass { Program* getProgram() { return program; } + std::vector getBplGlobals() { return bplGlobals; } }; } diff --git a/include/smack/SmackRep.h b/include/smack/SmackRep.h index d0e305ccd..b98668dfc 100644 --- a/include/smack/SmackRep.h +++ b/include/smack/SmackRep.h @@ -157,6 +157,7 @@ class SmackRep { Decl* getInitFuncs(); std::string getPrelude(); const Expr* declareIsExternal(const Expr* e); + std::vector getBplGlobals() { return bplGlobals; } std::list auxiliaryDeclarations() { std::list ds; diff --git a/lib/smack/GenModifies.cpp b/lib/smack/GenModifies.cpp new file mode 100644 index 000000000..90b59f347 --- /dev/null +++ b/lib/smack/GenModifies.cpp @@ -0,0 +1,243 @@ +// +// This file is distributed under the MIT License. See LICENSE for details. +// +#include "smack/GenModifies.h" +#include "llvm/Support/Debug.h" +#include "llvm/Support/GraphWriter.h" +#include +#include +#include + +namespace smack { + +using llvm::errs; +using llvm::dyn_cast; +using llvm::isa; + +char GenModifies::ID = 0; + +void GenModifies::initProcMap(Program *program) { + for (Decl *decl : *program) { + if (ProcDecl *procDecl = dyn_cast(decl)) { + proc[procDecl->getName()] = procDecl; + } + } +} + +void GenModifies::insertModifiesClause(Decl *&decl, Regex &PROC_DECL, const std::set &bplGlobals) { + std::string modStr = "\nmodifies"; + + for (std::string var : bplGlobals) { + modStr += " " + var + ","; + } + + modStr[modStr.size() - 1] = ';'; + modStr.push_back('\n'); + + std::string newStr = PROC_DECL.sub("\\1", decl->getName()) + modStr + PROC_DECL.sub("\\6", decl->getName()); + + decl = Decl::code(newStr, newStr); +} + +void GenModifies::genSmackCodeModifies(Program *program, const std::set &bplGlobals) { + const std::string NAME_REGEX = "[[:alpha:]_.$#'`^\?][[:alnum:]_.$#'`^\?]*"; + Regex PROC_DECL("^([[:space:]]*procedure(.|[[:space:]])*[[:space:]]+(" + NAME_REGEX + ")[[:space:]]*\\((.|[[:space:]])*\\)(.|[[:space:]])*)(\\{(.|[[:space:]])*\\})"); + Regex MOD_CL("modifies[[:space:]]+" + NAME_REGEX + "([[:space:]]*,[[:space:]]*" + NAME_REGEX + ")*;"); + + for (Decl *&decl : *program) { + if (isa(decl)) { + if (!bplGlobals.empty()) { + if (PROC_DECL.match(decl->getName()) && !MOD_CL.match(decl->getName())) { + insertModifiesClause(decl, PROC_DECL, bplGlobals); + } + } + } + } +} + +void GenModifies::addNewSCC(const std::string &procName) { + std::string toAdd; + + do { + toAdd = st.top(); + st.pop(); + + onStack[toAdd] = false; + + SCCOfProc[toAdd] = modVars.size(); + } while (toAdd != procName); + + modVars.push_back(std::set()); + SCCGraph.push_back(std::set()); +} + +void GenModifies::dfs(ProcDecl *procDecl) { + const std::string name = procDecl->getName(); + + st.push(name); + onStack[name] = true; + index[name] = maxIndex; + low[name] = maxIndex++; + + for (Block *block : *procDecl) { + for (const Stmt *stmt : *block) { + if (const CallStmt *callStmt = dyn_cast(stmt)) { + const std::string next = callStmt->getName(); + + if (proc.count(next) && !index[next]) { + dfs(proc[next]); + + low[name] = std::min(low[name], low[next]); + } else if (onStack[next]) { + low[name] = std::min(low[name], index[next]); + } + } + } + } + + if (low[name] == index[name]) { + addNewSCC(name); + } +} + +void GenModifies::genSCCs(Program *program) { + for (Decl *decl : *program) { + if (ProcDecl *procDecl = dyn_cast(decl)) { + if (!index[procDecl->getName()]) { + dfs(procDecl); + } + } + } +} + +void GenModifies::addEdge(const CallStmt *callStmt, int parentSCC) { + int childSCC = SCCOfProc[callStmt->getName()]; + + if (childSCC && childSCC != parentSCC) { + SCCGraph[childSCC].insert(parentSCC); + } +} + +void GenModifies::genSCCGraph(Program *program) { + for (Decl *decl : *program) { + if (ProcDecl *procDecl = dyn_cast(decl)) { + int curSCC = SCCOfProc[procDecl->getName()]; + + for (Block *block : *procDecl) { + for (const Stmt *stmt : *block) { + if (const CallStmt *callStmt = dyn_cast(stmt)) { + addEdge(callStmt, curSCC); + } + } + } + } + } +} + +void GenModifies::addIfGlobalVar(const std::string exprName, const std::string &procName) { + static Regex GLOBAL_VAR("\\$M.[[:digit:]]+"); + if (GLOBAL_VAR.match(exprName)) { + std::string var = GLOBAL_VAR.sub("\\0", exprName); + + modVars[SCCOfProc[procName]].insert(var); + } +} + +void GenModifies::calcModifiesOfExprs(const std::list exprs, const std::string &procName) { + for (auto expr : exprs) { + if (const VarExpr *varExpr = dyn_cast(expr)) { + addIfGlobalVar(varExpr->name(), procName); + } + } +} + +void GenModifies::calcModifiesOfStmt(const Stmt *stmt, const std::string procName) { + if (const AssignStmt* assignStmt = dyn_cast(stmt)) { + calcModifiesOfExprs(assignStmt->getlhs(), procName); + + for (const Expr *expr : assignStmt->getrhs()) { + if (const FunExpr *funExpr = dyn_cast(expr)) { + calcModifiesOfExprs(funExpr->getArgs(), procName); + } + } + } else if (const CallStmt *callStmt = dyn_cast(stmt)) { + for (const std::string retName : callStmt->getReturns()) { + addIfGlobalVar(retName, procName); + } + + calcModifiesOfExprs(callStmt->getParams(), procName); + } +} + +void GenModifies::calcModifiesOfSCCs(Program *program) { + for (Decl *decl : *program) { + if (ProcDecl *procDecl = dyn_cast(decl)) { + for (Block *block : *procDecl) { + for (const Stmt *stmt : *block) { + calcModifiesOfStmt(stmt, procDecl->getName()); + } + } + } + } +} + +void GenModifies::propagateModifiesUpGraph() { + for (size_t child = 1; child < SCCGraph.size(); ++child) { + for (int parent : SCCGraph[child]) { + modVars[parent].insert(modVars[child].begin(), modVars[child].end()); + } + } +} + +void GenModifies::addSmackGlobals(const std::set &bplGlobals) { + for (size_t scc = 0; scc < modVars.size(); ++scc) { + modVars[scc].insert(bplGlobals.begin(), bplGlobals.end()); + } +} + +void GenModifies::addModifies(Program *program) { + for (Decl *decl : *program) { + if (ProcDecl *procDecl = dyn_cast(decl)) { + if (procDecl->begin() != procDecl->end()) { + int index = SCCOfProc[procDecl->getName()]; + + std::list &modList = procDecl->getModifies(); + + modList.insert(modList.end(), modVars[index].begin(), modVars[index].end()); + } + } + } +} + +void GenModifies::genUserCodeModifies(Program *program, const std::set &bplGlobals) { + genSCCs(program); + + calcModifiesOfSCCs(program); + + genSCCGraph(program); + + propagateModifiesUpGraph(); + + addSmackGlobals(bplGlobals); + + addModifies(program); +} + +bool GenModifies::runOnModule(llvm::Module& m) { + SmackModuleGenerator &smackGenerator = getAnalysis(); + Program *program = smackGenerator.getProgram(); + + std::set bplGlobals; + std::vector oldBplGlobals = smackGenerator.getBplGlobals(); + std::copy(oldBplGlobals.begin(), oldBplGlobals.end(), std::inserter(bplGlobals, bplGlobals.end())); + + initProcMap(program); + + genSmackCodeModifies(program, bplGlobals); + + genUserCodeModifies(program, bplGlobals); + + // DEBUG_WITH_TYPE("bpl", errs() << "" << s.str()); + return false; +} +} diff --git a/lib/smack/SmackModuleGenerator.cpp b/lib/smack/SmackModuleGenerator.cpp index 8b6cad53d..1ea48c383 100644 --- a/lib/smack/SmackModuleGenerator.cpp +++ b/lib/smack/SmackModuleGenerator.cpp @@ -88,6 +88,8 @@ void SmackModuleGenerator::generateProgram(llvm::Module& M) { // ... to do below, after memory splitting is determined. } + bplGlobals = rep.getBplGlobals(); + auto ds = rep.auxiliaryDeclarations(); decls.insert(decls.end(), ds.begin(), ds.end()); decls.insert(decls.end(), rep.getInitFuncs()); diff --git a/share/smack/top.py b/share/smack/top.py index 77b462fab..f23a1f9c8 100755 --- a/share/smack/top.py +++ b/share/smack/top.py @@ -512,7 +512,7 @@ def verify_bpl(args): elif args.verifier == 'boogie' or args.modular: command = ["boogie"] command += [args.bpl_file] - command += ["/nologo", "/noinfer", "/doModSetAnalysis"] + #command += ["/nologo", "/noinfer", "/doModSetAnalysis"] command += ["/timeLimit:%s" % args.time_limit] command += ["/errorLimit:%s" % args.max_violations] if not args.modular: diff --git a/tools/llvm2bpl/llvm2bpl.cpp b/tools/llvm2bpl/llvm2bpl.cpp index 61f564be7..0b24c7df1 100644 --- a/tools/llvm2bpl/llvm2bpl.cpp +++ b/tools/llvm2bpl/llvm2bpl.cpp @@ -41,6 +41,7 @@ #include "smack/MemorySafetyChecker.h" #include "smack/SignedIntegerOverflowChecker.h" #include "smack/SplitAggregateLoadStore.h" +#include "smack/GenModifies.h" static llvm::cl::opt InputFilename(llvm::cl::Positional, llvm::cl::desc(""), @@ -227,6 +228,7 @@ int main(int argc, char **argv) { F->keep(); files.push_back(F); pass_manager.add(new smack::SmackModuleGenerator()); + pass_manager.add(new smack::GenModifies()); pass_manager.add(new smack::BplFilePrinter(F->os())); } From 5d6448bcdade5129c3212e490c1c91b88e9c3103 Mon Sep 17 00:00:00 2001 From: Liam Machado Date: Mon, 25 Sep 2017 16:16:34 -0600 Subject: [PATCH 02/13] Fixed some issues with the modifies pass and smack.c causing the memory-safety regtests to fail. The modifies pass was not handling the prelude section of Boogie files. When the --memory-safety option is specified, this prelude section contains a procedure called $global_allocations which modifies some variables. Additionally, the modifies pass only adds modifies clauses to SMACK-generated procedures that do not already have one, which does not cover the $malloc procedure when the --memory-safety option is set. This is directly changed in smack.c. --- include/smack/BoogieAst.h | 1 + include/smack/GenModifies.h | 4 ++- lib/smack/GenModifies.cpp | 49 ++++++++++++++++++++++++---------- share/smack/lib/smack.c | 53 ++++++++++++++++++++++++++++++------- 4 files changed, 83 insertions(+), 24 deletions(-) diff --git a/include/smack/BoogieAst.h b/include/smack/BoogieAst.h index 4d6ea83a9..7bbeea66c 100644 --- a/include/smack/BoogieAst.h +++ b/include/smack/BoogieAst.h @@ -582,6 +582,7 @@ class Program { bool empty() { return decls.empty(); } DeclarationList& getDeclarations() { return decls; } void appendPrelude(std::string s) { prelude += s; } + std::string& getPrelude() { return prelude; } }; std::ostream& operator<<(std::ostream& os, const Expr& e); diff --git a/include/smack/GenModifies.h b/include/smack/GenModifies.h index 0b52a52c8..8d2cfdc5b 100644 --- a/include/smack/GenModifies.h +++ b/include/smack/GenModifies.h @@ -30,7 +30,9 @@ class GenModifies : public llvm::ModulePass { int maxIndex; void initProcMap(Program *program); - void insertModifiesClause(Decl *&decl, Regex &PROC_DECL, const std::set &bplGlobals); + std::string getBplGlobalsModifiesClause(const std::set &bplGlobals); + void fixPrelude(Program *program, const std::string &modClause); + void addModifiesToSmackProcs(Program *program, const std::string &modClause); void genSmackCodeModifies(Program *program, const std::set &bplGlobals); void addNewSCC(const std::string &procName); void dfs(ProcDecl *curProc); diff --git a/lib/smack/GenModifies.cpp b/lib/smack/GenModifies.cpp index 90b59f347..f1d4bd0dd 100644 --- a/lib/smack/GenModifies.cpp +++ b/lib/smack/GenModifies.cpp @@ -24,37 +24,56 @@ void GenModifies::initProcMap(Program *program) { } } -void GenModifies::insertModifiesClause(Decl *&decl, Regex &PROC_DECL, const std::set &bplGlobals) { - std::string modStr = "\nmodifies"; +std::string GenModifies::getBplGlobalsModifiesClause(const std::set &bplGlobals) { + std::string modClause = "\nmodifies"; for (std::string var : bplGlobals) { - modStr += " " + var + ","; + modClause += " " + var + ","; } - modStr[modStr.size() - 1] = ';'; - modStr.push_back('\n'); + modClause[modClause.size() - 1] = ';'; + modClause.push_back('\n'); - std::string newStr = PROC_DECL.sub("\\1", decl->getName()) + modStr + PROC_DECL.sub("\\6", decl->getName()); + return modClause; +} + +void GenModifies::fixPrelude(Program *program, const std::string &modClause) { + std::string searchStr = "procedure $global_allocations()\n"; + + std::string &prelude = program->getPrelude(); + + size_t pos = prelude.find(searchStr) + searchStr.size();; - decl = Decl::code(newStr, newStr); + std::string str1 = prelude.substr(0, pos); + std::string str2 = prelude.substr(pos); + + prelude = str1 + modClause + str2; } -void GenModifies::genSmackCodeModifies(Program *program, const std::set &bplGlobals) { +void GenModifies::addModifiesToSmackProcs(Program *program, const std::string &modClause) { const std::string NAME_REGEX = "[[:alpha:]_.$#'`^\?][[:alnum:]_.$#'`^\?]*"; - Regex PROC_DECL("^([[:space:]]*procedure(.|[[:space:]])*[[:space:]]+(" + NAME_REGEX + ")[[:space:]]*\\((.|[[:space:]])*\\)(.|[[:space:]])*)(\\{(.|[[:space:]])*\\})"); + Regex PROC_DECL("^([[:space:]]*procedure[[:space:]]+[^\\(]*(" + NAME_REGEX + ")[[:space:]]*\\([^\\)]*\\)[^\\{]*)(\\{(.|[[:space:]])*(\\}[[:space:]]*)$)"); Regex MOD_CL("modifies[[:space:]]+" + NAME_REGEX + "([[:space:]]*,[[:space:]]*" + NAME_REGEX + ")*;"); for (Decl *&decl : *program) { if (isa(decl)) { - if (!bplGlobals.empty()) { - if (PROC_DECL.match(decl->getName()) && !MOD_CL.match(decl->getName())) { - insertModifiesClause(decl, PROC_DECL, bplGlobals); - } + if (PROC_DECL.match(decl->getName()) && !MOD_CL.match(decl->getName())) { + std::string newStr = PROC_DECL.sub("\\1", decl->getName()) + modClause + PROC_DECL.sub("\\3", decl->getName()); + + decl = Decl::code(newStr, newStr); } } } } +void GenModifies::genSmackCodeModifies(Program *program, const std::set &bplGlobals) { + std::string modClause = getBplGlobalsModifiesClause(bplGlobals); + + fixPrelude(program, modClause); + + addModifiesToSmackProcs(program, modClause); +} + void GenModifies::addNewSCC(const std::string &procName) { std::string toAdd; @@ -233,7 +252,9 @@ bool GenModifies::runOnModule(llvm::Module& m) { initProcMap(program); - genSmackCodeModifies(program, bplGlobals); + if (!bplGlobals.empty()) { + genSmackCodeModifies(program, bplGlobals); + } genUserCodeModifies(program, bplGlobals); diff --git a/share/smack/lib/smack.c b/share/smack/lib/smack.c index 4345b565c..f9024c1a9 100644 --- a/share/smack/lib/smack.c +++ b/share/smack/lib/smack.c @@ -1584,8 +1584,14 @@ void __SMACK_decls(void) { D("function $base(ref) returns (ref);"); D("var $allocatedCounter: int;\n"); + +#if MEMORY_MODEL_NO_REUSE_IMPLS + D("var $Alloc: [ref] bool;"); + D("function $Size(ref) returns (ref);"); + D("var $CurrAddr:ref;\n"); + D("procedure $malloc(n: ref) returns (p: ref)\n" - "modifies $allocatedCounter;\n" + "modifies $allocatedCounter, $Alloc, $CurrAddr;\n" "{\n" " if ($ne.ref.bool(n, $0.ref)) {\n" " $allocatedCounter := $allocatedCounter + 1;\n" @@ -1593,11 +1599,6 @@ void __SMACK_decls(void) { " call p := $$alloc(n);\n" "}\n"); -#if MEMORY_MODEL_NO_REUSE_IMPLS - D("var $Alloc: [ref] bool;"); - D("function $Size(ref) returns (ref);"); - D("var $CurrAddr:ref;\n"); - D("procedure $galloc(base_addr: ref, size: ref)\n" "{\n" " assume $Size(base_addr) == size;\n" @@ -1638,6 +1639,16 @@ void __SMACK_decls(void) { D("var $Alloc: [ref] bool;"); D("var $Size: [ref] ref;\n"); + D("procedure $malloc(n: ref) returns (p: ref)\n" + "modifies $allocatedCounter, $Alloc, $Size;\n" + "{\n" + " if ($ne.ref.bool(n, $0.ref)) {\n" + " $allocatedCounter := $allocatedCounter + 1;\n" + " }\n" + " call p := $$alloc(n);\n" + "}\n"); + + D("procedure $galloc(base_addr: ref, size: ref);\n" "modifies $Alloc, $Size;\n" "ensures $Size[base_addr] == size;\n" @@ -1672,6 +1683,16 @@ void __SMACK_decls(void) { D("function $Size(ref) returns (ref);"); D("var $CurrAddr:ref;\n"); + D("procedure $malloc(n: ref) returns (p: ref)\n" + "modifies $allocatedCounter, $Alloc, $CurrAddr;\n" + "{\n" + " if ($ne.ref.bool(n, $0.ref)) {\n" + " $allocatedCounter := $allocatedCounter + 1;\n" + " }\n" + " call p := $$alloc(n);\n" + "}\n"); + + D("procedure $galloc(base_addr: ref, size: ref);\n" "modifies $Alloc;\n" "ensures $Size(base_addr) == size;\n" @@ -1701,14 +1722,16 @@ void __SMACK_decls(void) { #endif #else + +#if MEMORY_MODEL_NO_REUSE_IMPLS + D("var $CurrAddr:ref;\n"); + D("procedure $malloc(n: ref) returns (p: ref)\n" + "modifies $allocatedCounter, $CurrAddr;\n" "{\n" " call p := $$alloc(n);\n" "}\n"); -#if MEMORY_MODEL_NO_REUSE_IMPLS - D("var $CurrAddr:ref;\n"); - D("procedure {:inline 1} $$alloc(n: ref) returns (p: ref)\n" "modifies $CurrAddr;\n" "{\n" @@ -1729,6 +1752,12 @@ void __SMACK_decls(void) { D("var $Alloc: [ref] bool;"); D("var $Size: [ref] ref;\n"); + D("procedure $malloc(n: ref) returns (p: ref)\n" + "modifies $allocatedCounter, $Alloc, $Size;\n" + "{\n" + " call p := $$alloc(n);\n" + "}\n"); + D("procedure {:inline 1} $$alloc(n: ref) returns (p: ref);\n" "modifies $Alloc, $Size;\n" "ensures $sle.ref.bool($0.ref, n);\n" @@ -1749,6 +1778,12 @@ void __SMACK_decls(void) { #else // NO_REUSE does not reuse previously-allocated addresses D("var $CurrAddr:ref;\n"); + D("procedure $malloc(n: ref) returns (p: ref)\n" + "modifies $allocatedCounter, $CurrAddr;\n" + "{\n" + " call p := $$alloc(n);\n" + "}\n"); + D("procedure {:inline 1} $$alloc(n: ref) returns (p: ref);\n" "modifies $CurrAddr;\n" "ensures $sle.ref.bool($0.ref, n);\n" From 015de8bc96faf3905c2a7391801a68209108cf45 Mon Sep 17 00:00:00 2001 From: Liam Machado Date: Mon, 25 Sep 2017 18:10:13 -0600 Subject: [PATCH 03/13] Modifies pass was improperly handling prelude section when -memory-safety option is not specified. --- lib/smack/GenModifies.cpp | 11 +++++++---- 1 file changed, 7 insertions(+), 4 deletions(-) diff --git a/lib/smack/GenModifies.cpp b/lib/smack/GenModifies.cpp index f1d4bd0dd..8344d8a4e 100644 --- a/lib/smack/GenModifies.cpp +++ b/lib/smack/GenModifies.cpp @@ -7,6 +7,7 @@ #include #include #include +#include namespace smack { @@ -42,12 +43,14 @@ void GenModifies::fixPrelude(Program *program, const std::string &modClause) { std::string &prelude = program->getPrelude(); - size_t pos = prelude.find(searchStr) + searchStr.size();; + size_t pos = prelude.find(searchStr); - std::string str1 = prelude.substr(0, pos); - std::string str2 = prelude.substr(pos); + if (pos != std::string::npos) { + std::string str1 = prelude.substr(0, pos + searchStr.size()); + std::string str2 = prelude.substr(pos + searchStr.size()); - prelude = str1 + modClause + str2; + prelude = str1 + modClause + str2; + } } void GenModifies::addModifiesToSmackProcs(Program *program, const std::string &modClause) { From 8154002a17a8c023e4f96020d82486f5aa408d19 Mon Sep 17 00:00:00 2001 From: Liam Machado Date: Mon, 25 Sep 2017 18:11:38 -0600 Subject: [PATCH 04/13] $malloc procedure's modifies clause included variables that should not have been there. --- share/smack/lib/smack.c | 6 +++--- 1 file changed, 3 insertions(+), 3 deletions(-) diff --git a/share/smack/lib/smack.c b/share/smack/lib/smack.c index f9024c1a9..7eb711011 100644 --- a/share/smack/lib/smack.c +++ b/share/smack/lib/smack.c @@ -1727,7 +1727,7 @@ void __SMACK_decls(void) { D("var $CurrAddr:ref;\n"); D("procedure $malloc(n: ref) returns (p: ref)\n" - "modifies $allocatedCounter, $CurrAddr;\n" + "modifies $CurrAddr;\n" "{\n" " call p := $$alloc(n);\n" "}\n"); @@ -1753,7 +1753,7 @@ void __SMACK_decls(void) { D("var $Size: [ref] ref;\n"); D("procedure $malloc(n: ref) returns (p: ref)\n" - "modifies $allocatedCounter, $Alloc, $Size;\n" + "modifies $Alloc, $Size;\n" "{\n" " call p := $$alloc(n);\n" "}\n"); @@ -1779,7 +1779,7 @@ void __SMACK_decls(void) { D("var $CurrAddr:ref;\n"); D("procedure $malloc(n: ref) returns (p: ref)\n" - "modifies $allocatedCounter, $CurrAddr;\n" + "modifies $CurrAddr;\n" "{\n" " call p := $$alloc(n);\n" "}\n"); From e3617e06e1df88427d4d392fcc618dec121e9f46 Mon Sep 17 00:00:00 2001 From: Liam Machado Date: Mon, 25 Sep 2017 18:13:48 -0600 Subject: [PATCH 05/13] Removed unnecessary #include header --- lib/smack/GenModifies.cpp | 1 - 1 file changed, 1 deletion(-) diff --git a/lib/smack/GenModifies.cpp b/lib/smack/GenModifies.cpp index 8344d8a4e..03315b597 100644 --- a/lib/smack/GenModifies.cpp +++ b/lib/smack/GenModifies.cpp @@ -7,7 +7,6 @@ #include #include #include -#include namespace smack { From 266e82bbada80f24a69093225bc5db4869f1465d Mon Sep 17 00:00:00 2001 From: Liam Machado Date: Sun, 8 Oct 2017 14:25:55 -0600 Subject: [PATCH 06/13] Changed name of modifies pass from GenModifies to ModAnalysis. --- CMakeLists.txt | 4 ++-- include/smack/GenModifies.h | 10 ++++----- lib/smack/GenModifies.cpp | 42 ++++++++++++++++++------------------- tools/llvm2bpl/llvm2bpl.cpp | 4 ++-- 4 files changed, 30 insertions(+), 30 deletions(-) diff --git a/CMakeLists.txt b/CMakeLists.txt index d5df49a4a..b7ef8a397 100644 --- a/CMakeLists.txt +++ b/CMakeLists.txt @@ -175,7 +175,7 @@ add_library(smackTranslator STATIC include/smack/MemorySafetyChecker.h include/smack/SignedIntegerOverflowChecker.h include/smack/SplitAggregateLoadStore.h - include/smack/GenModifies.h + include/smack/ModAnalysis.h lib/smack/AddTiming.cpp lib/smack/BoogieAst.cpp lib/smack/BplFilePrinter.cpp @@ -196,7 +196,7 @@ add_library(smackTranslator STATIC lib/smack/MemorySafetyChecker.cpp lib/smack/SignedIntegerOverflowChecker.cpp lib/smack/SplitAggregateLoadStore.cpp - lib/smack/GenModifies.cpp + lib/smack/ModAnalysis.cpp ) add_executable(llvm2bpl diff --git a/include/smack/GenModifies.h b/include/smack/GenModifies.h index 8d2cfdc5b..8dd9f8a76 100644 --- a/include/smack/GenModifies.h +++ b/include/smack/GenModifies.h @@ -1,8 +1,8 @@ // // This file is distributed under the MIT License. See LICENSE for details. // -#ifndef MODS_H -#define MODS_H +#ifndef MODANALYSIS_H +#define MODANALYSIS_H #include "smack/SmackModuleGenerator.h" #include "smack/BoogieAst.h" @@ -15,7 +15,7 @@ namespace smack { using llvm::Regex; -class GenModifies : public llvm::ModulePass { +class ModAnalysis : public llvm::ModulePass { private: std::stack st; @@ -51,7 +51,7 @@ class GenModifies : public llvm::ModulePass { public: static char ID; // Pass identification, replacement for typeid - GenModifies() : llvm::ModulePass(ID), maxIndex(1) { + ModAnalysis() : llvm::ModulePass(ID), maxIndex(1) { SCCGraph.push_back(std::set()); modVars.push_back(std::set()); } @@ -69,5 +69,5 @@ class GenModifies : public llvm::ModulePass { }; } -#endif // MODS_H +#endif // MODANALYSIS_H diff --git a/lib/smack/GenModifies.cpp b/lib/smack/GenModifies.cpp index 03315b597..b5ffbbbdf 100644 --- a/lib/smack/GenModifies.cpp +++ b/lib/smack/GenModifies.cpp @@ -1,7 +1,7 @@ // // This file is distributed under the MIT License. See LICENSE for details. // -#include "smack/GenModifies.h" +#include "smack/ModAnalysis.h" #include "llvm/Support/Debug.h" #include "llvm/Support/GraphWriter.h" #include @@ -14,9 +14,9 @@ using llvm::errs; using llvm::dyn_cast; using llvm::isa; -char GenModifies::ID = 0; +char ModAnalysis::ID = 0; -void GenModifies::initProcMap(Program *program) { +void ModAnalysis::initProcMap(Program *program) { for (Decl *decl : *program) { if (ProcDecl *procDecl = dyn_cast(decl)) { proc[procDecl->getName()] = procDecl; @@ -24,7 +24,7 @@ void GenModifies::initProcMap(Program *program) { } } -std::string GenModifies::getBplGlobalsModifiesClause(const std::set &bplGlobals) { +std::string ModAnalysis::getBplGlobalsModifiesClause(const std::set &bplGlobals) { std::string modClause = "\nmodifies"; for (std::string var : bplGlobals) { @@ -37,7 +37,7 @@ std::string GenModifies::getBplGlobalsModifiesClause(const std::set return modClause; } -void GenModifies::fixPrelude(Program *program, const std::string &modClause) { +void ModAnalysis::fixPrelude(Program *program, const std::string &modClause) { std::string searchStr = "procedure $global_allocations()\n"; std::string &prelude = program->getPrelude(); @@ -52,7 +52,7 @@ void GenModifies::fixPrelude(Program *program, const std::string &modClause) { } } -void GenModifies::addModifiesToSmackProcs(Program *program, const std::string &modClause) { +void ModAnalysis::addModifiesToSmackProcs(Program *program, const std::string &modClause) { const std::string NAME_REGEX = "[[:alpha:]_.$#'`^\?][[:alnum:]_.$#'`^\?]*"; Regex PROC_DECL("^([[:space:]]*procedure[[:space:]]+[^\\(]*(" + NAME_REGEX + ")[[:space:]]*\\([^\\)]*\\)[^\\{]*)(\\{(.|[[:space:]])*(\\}[[:space:]]*)$)"); Regex MOD_CL("modifies[[:space:]]+" + NAME_REGEX + "([[:space:]]*,[[:space:]]*" + NAME_REGEX + ")*;"); @@ -68,7 +68,7 @@ void GenModifies::addModifiesToSmackProcs(Program *program, const std::string &m } } -void GenModifies::genSmackCodeModifies(Program *program, const std::set &bplGlobals) { +void ModAnalysis::genSmackCodeModifies(Program *program, const std::set &bplGlobals) { std::string modClause = getBplGlobalsModifiesClause(bplGlobals); fixPrelude(program, modClause); @@ -76,7 +76,7 @@ void GenModifies::genSmackCodeModifies(Program *program, const std::set()); } -void GenModifies::dfs(ProcDecl *procDecl) { +void ModAnalysis::dfs(ProcDecl *procDecl) { const std::string name = procDecl->getName(); st.push(name); @@ -121,7 +121,7 @@ void GenModifies::dfs(ProcDecl *procDecl) { } } -void GenModifies::genSCCs(Program *program) { +void ModAnalysis::genSCCs(Program *program) { for (Decl *decl : *program) { if (ProcDecl *procDecl = dyn_cast(decl)) { if (!index[procDecl->getName()]) { @@ -131,7 +131,7 @@ void GenModifies::genSCCs(Program *program) { } } -void GenModifies::addEdge(const CallStmt *callStmt, int parentSCC) { +void ModAnalysis::addEdge(const CallStmt *callStmt, int parentSCC) { int childSCC = SCCOfProc[callStmt->getName()]; if (childSCC && childSCC != parentSCC) { @@ -139,7 +139,7 @@ void GenModifies::addEdge(const CallStmt *callStmt, int parentSCC) { } } -void GenModifies::genSCCGraph(Program *program) { +void ModAnalysis::genSCCGraph(Program *program) { for (Decl *decl : *program) { if (ProcDecl *procDecl = dyn_cast(decl)) { int curSCC = SCCOfProc[procDecl->getName()]; @@ -155,7 +155,7 @@ void GenModifies::genSCCGraph(Program *program) { } } -void GenModifies::addIfGlobalVar(const std::string exprName, const std::string &procName) { +void ModAnalysis::addIfGlobalVar(const std::string exprName, const std::string &procName) { static Regex GLOBAL_VAR("\\$M.[[:digit:]]+"); if (GLOBAL_VAR.match(exprName)) { std::string var = GLOBAL_VAR.sub("\\0", exprName); @@ -164,7 +164,7 @@ void GenModifies::addIfGlobalVar(const std::string exprName, const std::string & } } -void GenModifies::calcModifiesOfExprs(const std::list exprs, const std::string &procName) { +void ModAnalysis::calcModifiesOfExprs(const std::list exprs, const std::string &procName) { for (auto expr : exprs) { if (const VarExpr *varExpr = dyn_cast(expr)) { addIfGlobalVar(varExpr->name(), procName); @@ -172,7 +172,7 @@ void GenModifies::calcModifiesOfExprs(const std::list exprs, const } } -void GenModifies::calcModifiesOfStmt(const Stmt *stmt, const std::string procName) { +void ModAnalysis::calcModifiesOfStmt(const Stmt *stmt, const std::string procName) { if (const AssignStmt* assignStmt = dyn_cast(stmt)) { calcModifiesOfExprs(assignStmt->getlhs(), procName); @@ -190,7 +190,7 @@ void GenModifies::calcModifiesOfStmt(const Stmt *stmt, const std::string procNam } } -void GenModifies::calcModifiesOfSCCs(Program *program) { +void ModAnalysis::calcModifiesOfSCCs(Program *program) { for (Decl *decl : *program) { if (ProcDecl *procDecl = dyn_cast(decl)) { for (Block *block : *procDecl) { @@ -202,7 +202,7 @@ void GenModifies::calcModifiesOfSCCs(Program *program) { } } -void GenModifies::propagateModifiesUpGraph() { +void ModAnalysis::propagateModifiesUpGraph() { for (size_t child = 1; child < SCCGraph.size(); ++child) { for (int parent : SCCGraph[child]) { modVars[parent].insert(modVars[child].begin(), modVars[child].end()); @@ -210,13 +210,13 @@ void GenModifies::propagateModifiesUpGraph() { } } -void GenModifies::addSmackGlobals(const std::set &bplGlobals) { +void ModAnalysis::addSmackGlobals(const std::set &bplGlobals) { for (size_t scc = 0; scc < modVars.size(); ++scc) { modVars[scc].insert(bplGlobals.begin(), bplGlobals.end()); } } -void GenModifies::addModifies(Program *program) { +void ModAnalysis::addModifies(Program *program) { for (Decl *decl : *program) { if (ProcDecl *procDecl = dyn_cast(decl)) { if (procDecl->begin() != procDecl->end()) { @@ -230,7 +230,7 @@ void GenModifies::addModifies(Program *program) { } } -void GenModifies::genUserCodeModifies(Program *program, const std::set &bplGlobals) { +void ModAnalysis::genUserCodeModifies(Program *program, const std::set &bplGlobals) { genSCCs(program); calcModifiesOfSCCs(program); @@ -244,7 +244,7 @@ void GenModifies::genUserCodeModifies(Program *program, const std::set(); Program *program = smackGenerator.getProgram(); diff --git a/tools/llvm2bpl/llvm2bpl.cpp b/tools/llvm2bpl/llvm2bpl.cpp index 0b24c7df1..a1f130376 100644 --- a/tools/llvm2bpl/llvm2bpl.cpp +++ b/tools/llvm2bpl/llvm2bpl.cpp @@ -41,7 +41,7 @@ #include "smack/MemorySafetyChecker.h" #include "smack/SignedIntegerOverflowChecker.h" #include "smack/SplitAggregateLoadStore.h" -#include "smack/GenModifies.h" +#include "smack/ModAnalysis.h" static llvm::cl::opt InputFilename(llvm::cl::Positional, llvm::cl::desc(""), @@ -228,7 +228,7 @@ int main(int argc, char **argv) { F->keep(); files.push_back(F); pass_manager.add(new smack::SmackModuleGenerator()); - pass_manager.add(new smack::GenModifies()); + pass_manager.add(new smack::ModAnalysis()); pass_manager.add(new smack::BplFilePrinter(F->os())); } From cb81255ae9476fde8d2e4e5c1d3561397d7cacf6 Mon Sep 17 00:00:00 2001 From: Liam Machado Date: Sun, 8 Oct 2017 14:26:51 -0600 Subject: [PATCH 07/13] Removed unnecessary empty lines. --- lib/smack/GenModifies.cpp | 16 ---------------- 1 file changed, 16 deletions(-) diff --git a/lib/smack/GenModifies.cpp b/lib/smack/GenModifies.cpp index b5ffbbbdf..ce08fdd0e 100644 --- a/lib/smack/GenModifies.cpp +++ b/lib/smack/GenModifies.cpp @@ -39,15 +39,12 @@ std::string ModAnalysis::getBplGlobalsModifiesClause(const std::set void ModAnalysis::fixPrelude(Program *program, const std::string &modClause) { std::string searchStr = "procedure $global_allocations()\n"; - std::string &prelude = program->getPrelude(); - size_t pos = prelude.find(searchStr); if (pos != std::string::npos) { std::string str1 = prelude.substr(0, pos + searchStr.size()); std::string str2 = prelude.substr(pos + searchStr.size()); - prelude = str1 + modClause + str2; } } @@ -61,7 +58,6 @@ void ModAnalysis::addModifiesToSmackProcs(Program *program, const std::string &m if (isa(decl)) { if (PROC_DECL.match(decl->getName()) && !MOD_CL.match(decl->getName())) { std::string newStr = PROC_DECL.sub("\\1", decl->getName()) + modClause + PROC_DECL.sub("\\3", decl->getName()); - decl = Decl::code(newStr, newStr); } } @@ -70,9 +66,7 @@ void ModAnalysis::addModifiesToSmackProcs(Program *program, const std::string &m void ModAnalysis::genSmackCodeModifies(Program *program, const std::set &bplGlobals) { std::string modClause = getBplGlobalsModifiesClause(bplGlobals); - fixPrelude(program, modClause); - addModifiesToSmackProcs(program, modClause); } @@ -82,9 +76,7 @@ void ModAnalysis::addNewSCC(const std::string &procName) { do { toAdd = st.top(); st.pop(); - onStack[toAdd] = false; - SCCOfProc[toAdd] = modVars.size(); } while (toAdd != procName); @@ -107,7 +99,6 @@ void ModAnalysis::dfs(ProcDecl *procDecl) { if (proc.count(next) && !index[next]) { dfs(proc[next]); - low[name] = std::min(low[name], low[next]); } else if (onStack[next]) { low[name] = std::min(low[name], index[next]); @@ -221,9 +212,7 @@ void ModAnalysis::addModifies(Program *program) { if (ProcDecl *procDecl = dyn_cast(decl)) { if (procDecl->begin() != procDecl->end()) { int index = SCCOfProc[procDecl->getName()]; - std::list &modList = procDecl->getModifies(); - modList.insert(modList.end(), modVars[index].begin(), modVars[index].end()); } } @@ -232,15 +221,10 @@ void ModAnalysis::addModifies(Program *program) { void ModAnalysis::genUserCodeModifies(Program *program, const std::set &bplGlobals) { genSCCs(program); - calcModifiesOfSCCs(program); - genSCCGraph(program); - propagateModifiesUpGraph(); - addSmackGlobals(bplGlobals); - addModifies(program); } From d9393e9a1d80b407fd8db7a95a97c1e2b5b10083 Mon Sep 17 00:00:00 2001 From: Liam Machado Date: Sun, 8 Oct 2017 14:28:00 -0600 Subject: [PATCH 08/13] Added back in /nologo and /noinfer options to Boogie command. --- share/smack/top.py | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/share/smack/top.py b/share/smack/top.py index f23a1f9c8..d92597b2a 100755 --- a/share/smack/top.py +++ b/share/smack/top.py @@ -512,7 +512,7 @@ def verify_bpl(args): elif args.verifier == 'boogie' or args.modular: command = ["boogie"] command += [args.bpl_file] - #command += ["/nologo", "/noinfer", "/doModSetAnalysis"] + command += ["/nologo", "/noinfer"] command += ["/timeLimit:%s" % args.time_limit] command += ["/errorLimit:%s" % args.max_violations] if not args.modular: From cff3d8b140c09f3a59bb6a86c9f00f87276553ad Mon Sep 17 00:00:00 2001 From: Liam Machado Date: Tue, 10 Oct 2017 12:46:39 -0600 Subject: [PATCH 09/13] Changed name of GenModifies.h/cpp to ModAnalysis.h/cpp --- include/smack/{GenModifies.h => ModAnalysis.h} | 0 lib/smack/{GenModifies.cpp => ModAnalysis.cpp} | 0 2 files changed, 0 insertions(+), 0 deletions(-) rename include/smack/{GenModifies.h => ModAnalysis.h} (100%) rename lib/smack/{GenModifies.cpp => ModAnalysis.cpp} (100%) diff --git a/include/smack/GenModifies.h b/include/smack/ModAnalysis.h similarity index 100% rename from include/smack/GenModifies.h rename to include/smack/ModAnalysis.h diff --git a/lib/smack/GenModifies.cpp b/lib/smack/ModAnalysis.cpp similarity index 100% rename from lib/smack/GenModifies.cpp rename to lib/smack/ModAnalysis.cpp From 432a3cb3a047bc60ad588350d4033cbab84229ed Mon Sep 17 00:00:00 2001 From: Liam Machado Date: Mon, 31 Dec 2018 18:02:13 -0700 Subject: [PATCH 10/13] Changed BoogieAst to be consistent with most recent version --- include/smack/BoogieAst.h | 8 ++++---- 1 file changed, 4 insertions(+), 4 deletions(-) diff --git a/include/smack/BoogieAst.h b/include/smack/BoogieAst.h index ad244c227..bd4775c4b 100644 --- a/include/smack/BoogieAst.h +++ b/include/smack/BoogieAst.h @@ -17,7 +17,7 @@ enum class RModeKind { RNE, RNA, RTP, RTN, RTZ }; class Expr { public: enum Kind { - BIN, COND, FUN, BOOL_LIT, INT_LIT, BV_LIT, FP_LIT, STRING_LIT, NEG, NOT, QUANT, SEL, UPD, VAR, CODE + BIN, COND, FUN, BOOL_LIT, RMODE_LIT, INT_LIT, BV_LIT, FP_LIT, STRING_LIT, NEG, NOT, QUANT, SEL, UPD, VAR, IF_THEN_ELSE, CODE }; private: const Kind kind; @@ -104,7 +104,7 @@ class BoolLit : public Expr { class RModeLit : public Expr { RModeKind val; public: - RModeLit(RModeKind v) : val(v) {} + RModeLit(RModeKind v) : Expr(RMODE_LIT), val(v) {} void print(std::ostream& os) const; }; @@ -184,7 +184,7 @@ class QuantExpr : public Expr { std::list vars; const Expr* expr; public: - QuantExpr(Quantifier q, std::list vs, const Expr* e) : quant(q), vars(vs), expr(e) {} + QuantExpr(Quantifier q, std::list vs, const Expr* e) : Expr(QUANT), quant(q), vars(vs), expr(e) {} void print(std::ostream& os) const; static bool classof(const Expr *e) { return e->getKind() == QUANT; } }; @@ -227,7 +227,7 @@ class IfThenElseExpr : public Expr { const Expr* false_value; public: IfThenElseExpr(const Expr* c, const Expr* t, const Expr* e) - : cond(c), true_value(t), false_value(e) {} + : Expr(IF_THEN_ELSE), cond(c), true_value(t), false_value(e) {} void print(std::ostream& os) const; }; From 591137b8100e75997a7978ef3a17447999f60dbe Mon Sep 17 00:00:00 2001 From: Liam Machado Date: Thu, 18 Jul 2019 13:52:22 -0600 Subject: [PATCH 11/13] Fixed formatting --- include/smack/ModAnalysis.h | 23 ++++++++------ include/smack/SmackModuleGenerator.h | 10 +++--- include/smack/SmackRep.h | 8 ++--- lib/smack/ModAnalysis.cpp | 47 ++++++++++++++++++---------- 4 files changed, 52 insertions(+), 36 deletions(-) diff --git a/include/smack/ModAnalysis.h b/include/smack/ModAnalysis.h index 8dd9f8a76..c0efe77f5 100644 --- a/include/smack/ModAnalysis.h +++ b/include/smack/ModAnalysis.h @@ -4,8 +4,8 @@ #ifndef MODANALYSIS_H #define MODANALYSIS_H -#include "smack/SmackModuleGenerator.h" #include "smack/BoogieAst.h" +#include "smack/SmackModuleGenerator.h" #include "llvm/Support/Regex.h" #include #include @@ -23,30 +23,34 @@ class ModAnalysis : public llvm::ModulePass { std::map index; std::map low; std::map SCCOfProc; - std::map proc; + std::map proc; std::vector> SCCGraph; std::vector> modVars; int maxIndex; void initProcMap(Program *program); - std::string getBplGlobalsModifiesClause(const std::set &bplGlobals); + std::string + getBplGlobalsModifiesClause(const std::set &bplGlobals); void fixPrelude(Program *program, const std::string &modClause); void addModifiesToSmackProcs(Program *program, const std::string &modClause); - void genSmackCodeModifies(Program *program, const std::set &bplGlobals); + void genSmackCodeModifies(Program *program, + const std::set &bplGlobals); void addNewSCC(const std::string &procName); void dfs(ProcDecl *curProc); void genSCCs(Program *program); void genSCCGraph(Program *program); void addEdge(const CallStmt *callStmt, int parentSCC); void addIfGlobalVar(std::string exprName, const std::string &procName); - void calcModifiesOfExprs(const std::list exprs, const std::string &procName); + void calcModifiesOfExprs(const std::list exprs, + const std::string &procName); void calcModifiesOfStmt(const Stmt *stmt, const std::string procName); void calcModifiesOfSCCs(Program *program); void propagateModifiesUpGraph(); void addSmackGlobals(const std::set &bplGlobals); void addModifies(Program *program); - void genUserCodeModifies(Program *program, const std::set &bplGlobals); + void genUserCodeModifies(Program *program, + const std::set &bplGlobals); public: static char ID; // Pass identification, replacement for typeid @@ -56,18 +60,17 @@ class ModAnalysis : public llvm::ModulePass { modVars.push_back(std::set()); } - virtual bool runOnModule(llvm::Module& m); + virtual bool runOnModule(llvm::Module &m); virtual const char *getPassName() const { return "Modifies clause generation"; } - virtual void getAnalysisUsage(llvm::AnalysisUsage& AU) const { + virtual void getAnalysisUsage(llvm::AnalysisUsage &AU) const { AU.setPreservesAll(); AU.addRequired(); - } + } }; } #endif // MODANALYSIS_H - diff --git a/include/smack/SmackModuleGenerator.h b/include/smack/SmackModuleGenerator.h index 484d15cad..fa788c477 100644 --- a/include/smack/SmackModuleGenerator.h +++ b/include/smack/SmackModuleGenerator.h @@ -12,17 +12,17 @@ class Program; class SmackModuleGenerator : public llvm::ModulePass { private: - Program* program; + Program *program; std::vector bplGlobals; public: static char ID; // Pass identification, replacement for typeid SmackModuleGenerator(); - virtual void getAnalysisUsage(llvm::AnalysisUsage& AU) const; - virtual bool runOnModule(llvm::Module& m); - void generateProgram(llvm::Module& m); - Program* getProgram() { return program; } + virtual void getAnalysisUsage(llvm::AnalysisUsage &AU) const; + virtual bool runOnModule(llvm::Module &m); + void generateProgram(llvm::Module &m); + Program *getProgram() { return program; } std::vector getBplGlobals() { return bplGlobals; } }; } diff --git a/include/smack/SmackRep.h b/include/smack/SmackRep.h index 2207487cd..8f5e9698b 100644 --- a/include/smack/SmackRep.h +++ b/include/smack/SmackRep.h @@ -184,10 +184,10 @@ class SmackRep { const Stmt *inverseFPCastAssume(const llvm::StoreInst *si); // used in SmackModuleGenerator - std::list globalDecl(const llvm::GlobalValue* g); - void addInitFunc(const llvm::Function* f); - Decl* getInitFuncs(); - const Expr* declareIsExternal(const Expr* e); + std::list globalDecl(const llvm::GlobalValue *g); + void addInitFunc(const llvm::Function *f); + Decl *getInitFuncs(); + const Expr *declareIsExternal(const Expr *e); std::vector getBplGlobals() { return bplGlobals; } bool isContractExpr(const llvm::Value *V) const; diff --git a/lib/smack/ModAnalysis.cpp b/lib/smack/ModAnalysis.cpp index ce08fdd0e..4645d76e4 100644 --- a/lib/smack/ModAnalysis.cpp +++ b/lib/smack/ModAnalysis.cpp @@ -4,9 +4,9 @@ #include "smack/ModAnalysis.h" #include "llvm/Support/Debug.h" #include "llvm/Support/GraphWriter.h" -#include #include #include +#include namespace smack { @@ -24,7 +24,8 @@ void ModAnalysis::initProcMap(Program *program) { } } -std::string ModAnalysis::getBplGlobalsModifiesClause(const std::set &bplGlobals) { +std::string ModAnalysis::getBplGlobalsModifiesClause( + const std::set &bplGlobals) { std::string modClause = "\nmodifies"; for (std::string var : bplGlobals) { @@ -34,7 +35,7 @@ std::string ModAnalysis::getBplGlobalsModifiesClause(const std::set modClause[modClause.size() - 1] = ';'; modClause.push_back('\n'); - return modClause; + return modClause; } void ModAnalysis::fixPrelude(Program *program, const std::string &modClause) { @@ -49,22 +50,28 @@ void ModAnalysis::fixPrelude(Program *program, const std::string &modClause) { } } -void ModAnalysis::addModifiesToSmackProcs(Program *program, const std::string &modClause) { +void ModAnalysis::addModifiesToSmackProcs(Program *program, + const std::string &modClause) { const std::string NAME_REGEX = "[[:alpha:]_.$#'`^\?][[:alnum:]_.$#'`^\?]*"; - Regex PROC_DECL("^([[:space:]]*procedure[[:space:]]+[^\\(]*(" + NAME_REGEX + ")[[:space:]]*\\([^\\)]*\\)[^\\{]*)(\\{(.|[[:space:]])*(\\}[[:space:]]*)$)"); - Regex MOD_CL("modifies[[:space:]]+" + NAME_REGEX + "([[:space:]]*,[[:space:]]*" + NAME_REGEX + ")*;"); + Regex PROC_DECL("^([[:space:]]*procedure[[:space:]]+[^\\(]*(" + NAME_REGEX + + ")[[:space:]]*\\([^\\)]*\\)[^\\{]*)(\\{(.|[[:space:]])*(\\}[[" + ":space:]]*)$)"); + Regex MOD_CL("modifies[[:space:]]+" + NAME_REGEX + + "([[:space:]]*,[[:space:]]*" + NAME_REGEX + ")*;"); for (Decl *&decl : *program) { if (isa(decl)) { if (PROC_DECL.match(decl->getName()) && !MOD_CL.match(decl->getName())) { - std::string newStr = PROC_DECL.sub("\\1", decl->getName()) + modClause + PROC_DECL.sub("\\3", decl->getName()); + std::string newStr = PROC_DECL.sub("\\1", decl->getName()) + modClause + + PROC_DECL.sub("\\3", decl->getName()); decl = Decl::code(newStr, newStr); } } } } -void ModAnalysis::genSmackCodeModifies(Program *program, const std::set &bplGlobals) { +void ModAnalysis::genSmackCodeModifies( + Program *program, const std::set &bplGlobals) { std::string modClause = getBplGlobalsModifiesClause(bplGlobals); fixPrelude(program, modClause); addModifiesToSmackProcs(program, modClause); @@ -146,16 +153,18 @@ void ModAnalysis::genSCCGraph(Program *program) { } } -void ModAnalysis::addIfGlobalVar(const std::string exprName, const std::string &procName) { +void ModAnalysis::addIfGlobalVar(const std::string exprName, + const std::string &procName) { static Regex GLOBAL_VAR("\\$M.[[:digit:]]+"); if (GLOBAL_VAR.match(exprName)) { - std::string var = GLOBAL_VAR.sub("\\0", exprName); + std::string var = GLOBAL_VAR.sub("\\0", exprName); modVars[SCCOfProc[procName]].insert(var); } } -void ModAnalysis::calcModifiesOfExprs(const std::list exprs, const std::string &procName) { +void ModAnalysis::calcModifiesOfExprs(const std::list exprs, + const std::string &procName) { for (auto expr : exprs) { if (const VarExpr *varExpr = dyn_cast(expr)) { addIfGlobalVar(varExpr->name(), procName); @@ -163,8 +172,9 @@ void ModAnalysis::calcModifiesOfExprs(const std::list exprs, const } } -void ModAnalysis::calcModifiesOfStmt(const Stmt *stmt, const std::string procName) { - if (const AssignStmt* assignStmt = dyn_cast(stmt)) { +void ModAnalysis::calcModifiesOfStmt(const Stmt *stmt, + const std::string procName) { + if (const AssignStmt *assignStmt = dyn_cast(stmt)) { calcModifiesOfExprs(assignStmt->getlhs(), procName); for (const Expr *expr : assignStmt->getrhs()) { @@ -213,13 +223,15 @@ void ModAnalysis::addModifies(Program *program) { if (procDecl->begin() != procDecl->end()) { int index = SCCOfProc[procDecl->getName()]; std::list &modList = procDecl->getModifies(); - modList.insert(modList.end(), modVars[index].begin(), modVars[index].end()); + modList.insert(modList.end(), modVars[index].begin(), + modVars[index].end()); } } } } -void ModAnalysis::genUserCodeModifies(Program *program, const std::set &bplGlobals) { +void ModAnalysis::genUserCodeModifies(Program *program, + const std::set &bplGlobals) { genSCCs(program); calcModifiesOfSCCs(program); genSCCGraph(program); @@ -228,13 +240,14 @@ void ModAnalysis::genUserCodeModifies(Program *program, const std::set(); Program *program = smackGenerator.getProgram(); std::set bplGlobals; std::vector oldBplGlobals = smackGenerator.getBplGlobals(); - std::copy(oldBplGlobals.begin(), oldBplGlobals.end(), std::inserter(bplGlobals, bplGlobals.end())); + std::copy(oldBplGlobals.begin(), oldBplGlobals.end(), + std::inserter(bplGlobals, bplGlobals.end())); initProcMap(program); From 97f7fd10cf7345dcf0fc75c5adf4432179179510 Mon Sep 17 00:00:00 2001 From: Liam Machado Date: Thu, 18 Jul 2019 21:26:35 -0600 Subject: [PATCH 12/13] Fixed method signature --- include/smack/ModAnalysis.h | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/include/smack/ModAnalysis.h b/include/smack/ModAnalysis.h index c0efe77f5..eddc4a12d 100644 --- a/include/smack/ModAnalysis.h +++ b/include/smack/ModAnalysis.h @@ -62,7 +62,7 @@ class ModAnalysis : public llvm::ModulePass { virtual bool runOnModule(llvm::Module &m); - virtual const char *getPassName() const { + virtual StringRef *getPassName() const { return "Modifies clause generation"; } From 4095a647bf90c94cf70ef7307e5588d5cd224dbb Mon Sep 17 00:00:00 2001 From: Liam Machado Date: Thu, 18 Jul 2019 22:00:36 -0600 Subject: [PATCH 13/13] More fixes to method signature --- include/smack/ModAnalysis.h | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/include/smack/ModAnalysis.h b/include/smack/ModAnalysis.h index eddc4a12d..9a62942b0 100644 --- a/include/smack/ModAnalysis.h +++ b/include/smack/ModAnalysis.h @@ -62,7 +62,7 @@ class ModAnalysis : public llvm::ModulePass { virtual bool runOnModule(llvm::Module &m); - virtual StringRef *getPassName() const { + virtual llvm::StringRef getPassName() const { return "Modifies clause generation"; }