From: Patrick Lam Date: Mon, 28 Sep 2015 09:55:28 +0000 (+0200) Subject: fix replacement around macro expansion; add new benchmarks from Stavros Aronis X-Git-Url: http://plrg.eecs.uci.edu/git/?p=satcheck.git;a=commitdiff_plain;h=52b59882a22019190a4f6cb35c65ce1221b4a96e;hp=44e8eabc8f7a0ab23c29037a770463d8a2de7b4a fix replacement around macro expansion; add new benchmarks from Stavros Aronis --- diff --git a/benchmarks/satcheck-precompiled/dekker/dekker-fences.c b/benchmarks/satcheck-precompiled/dekker/dekker-fences.c index c531933..ac796c9 100644 --- a/benchmarks/satcheck-precompiled/dekker/dekker-fences.c +++ b/benchmarks/satcheck-precompiled/dekker/dekker-fences.c @@ -37,9 +37,9 @@ void p0() { _br0 = MC2_branchUsesID(_cond0_m, 1, 2, true); break; } - - else { _br0 = MC2_branchUsesID(_cond0_m, 0, 2, true); MC2_merge(_br0); - } MCID _br1; + else { _br0 = MC2_branchUsesID(_cond0_m, 0, 2, true); MC2_merge(_br0); + } + MCID _br1; MCID _m_cond1_m=MC2_nextOpLoad(MCID_NODEP); int _cond1 = load_32(&turn); MCID _cond1_m = MC2_function_id(2, 1, sizeof(_cond1), _cond1, _m_cond1_m); @@ -57,8 +57,8 @@ void p0() { _br2 = MC2_branchUsesID(_cond2_m, 1, 2, true); break; } - else { _br2 = MC2_branchUsesID(_cond2_m, 0, 2, true); MC2_merge(_br2); - } + else { _br2 = MC2_branchUsesID(_cond2_m, 0, 2, true); MC2_merge(_br2); + } MC2_yield(); } MC2_exitLoop(); @@ -106,8 +106,8 @@ void p1() { _br3 = MC2_branchUsesID(_cond3_m, 1, 2, true); break; } - else { _br3 = MC2_branchUsesID(_cond3_m, 0, 2, true); MC2_merge(_br3); - } + else { _br3 = MC2_branchUsesID(_cond3_m, 0, 2, true); MC2_merge(_br3); + } MCID _br4; MCID _m_cond4_m=MC2_nextOpLoad(MCID_NODEP); int _cond4 = !load_32(&turn); @@ -124,9 +124,9 @@ void p1() { MCID _cond5_m = MC2_function_id(6, 1, sizeof(_cond5), _cond5, _m_cond5_m); if (_cond5) {_br5 = MC2_branchUsesID(_cond5_m, 1, 2, true); - break; -} else { _br5 = MC2_branchUsesID(_cond5_m, 0, 2, true); MC2_merge(_br5); - } MC2_yield(); + break;} + else { _br5 = MC2_branchUsesID(_cond5_m, 0, 2, true); MC2_merge(_br5); + } MC2_yield(); } MC2_exitLoop(); diff --git a/clang/src/add_mc2_annotations.cpp b/clang/src/add_mc2_annotations.cpp index 1b7c926..a2539e5 100644 --- a/clang/src/add_mc2_annotations.cpp +++ b/clang/src/add_mc2_annotations.cpp @@ -1,4 +1,4 @@ -// -*- indent-tabs-mode:nil; -*- +// -*- indent-tabs-mode:nil; c-basic-offset:4; -*- //------------------------------------------------------------------------------ // Add MC2 annotations to C code. // Copyright 2015 Patrick Lam @@ -725,7 +725,8 @@ public: virtual void run(const MatchFinder::MatchResult &Result) { const Stmt * s = Result.Nodes.getNodeAs("s"); - rewrite.InsertText(s->getLocStart(), "MC2_enterLoop();\n", true, true); + rewrite.InsertText(rewrite.getSourceMgr().getExpansionLoc(s->getLocStart()), + "MC2_enterLoop();\n", true, true); // annotate all returns with MC2_exitLoop() // annotate all breaks that aren't further nested with MC2_exitLoop(). @@ -743,7 +744,8 @@ public: // need to find all breaks and returns embedded inside the loop - rewrite.InsertTextAfterToken(s->getLocEnd().getLocWithOffset(1), "\nMC2_exitLoop();\n"); + rewrite.InsertTextAfterToken(rewrite.getSourceMgr().getExpansionLoc(s->getLocEnd().getLocWithOffset(1)), + "\nMC2_exitLoop();\n"); } private: @@ -873,7 +875,8 @@ public: place = op->getLocEnd().getLocWithOffset(1); else place = s->getLocEnd(); - rewrite.InsertText(place.getLocWithOffset(1), nol.str(), true, true); + rewrite.InsertText(rewrite.getSourceMgr().getExpansionLoc(place.getLocWithOffset(1)), + nol.str(), true, true); updateProvisionalName(DeferredUpdates, lhs, mcVar); } @@ -892,13 +895,13 @@ public: // record vars used in conditions class BranchConditionRefactoringHandler : public MatchFinder::MatchCallback { public: - BranchConditionRefactoringHandler(Rewriter &Rewrite, + BranchConditionRefactoringHandler(Rewriter &rewrite, std::set & DeclsInCond, std::map &DeclToMCVar, std::map &ExprToMCVar, std::map &Redirector, std::vector &DeferredUpdates) : - Rewrite(Rewrite), DeclsInCond(DeclsInCond), DeclToMCVar(DeclToMCVar), + rewrite(rewrite), DeclsInCond(DeclsInCond), DeclToMCVar(DeclToMCVar), ExprToMCVar(ExprToMCVar), Redirector(Redirector), DeferredUpdates(DeferredUpdates) {} virtual void run(const MatchFinder::MatchResult &Result) { @@ -920,7 +923,7 @@ public: // e.g. int _cond0 = x == y; std::string SStr; llvm::raw_string_ostream S(SStr); - bc->printPretty(S, nullptr, Rewrite.getLangOpts()); + bc->printPretty(S, nullptr, rewrite.getLangOpts()); const std::string &Str = S.str(); std::stringstream prel; @@ -954,14 +957,15 @@ public: } ExprToMCVar[cond] = condVarEncoded.str(); - Rewrite.InsertText(is->getLocStart(), prel.str(), false, true); + rewrite.InsertText(rewrite.getSourceMgr().getExpansionLoc(is->getLocStart()), + prel.str(), false, true); // rewrite the binary op with the newly-inserted var Expr * RO = bc->getRHS(); // used for location only - int cl = Lexer::MeasureTokenLength(RO->getLocStart(), Rewrite.getSourceMgr(), Rewrite.getLangOpts()); - SourceRange SR(cond->getLocStart(), Rewrite.getSourceMgr().getExpansionLoc(RO->getLocStart()).getLocWithOffset(cl-1)); - Rewrite.ReplaceText(SR, condVar); + int cl = Lexer::MeasureTokenLength(RO->getLocStart(), rewrite.getSourceMgr(), rewrite.getLangOpts()); + SourceRange SR(cond->getLocStart(), rewrite.getSourceMgr().getExpansionLoc(RO->getLocStart()).getLocWithOffset(cl-1)); + rewrite.ReplaceText(SR, condVar); } else { std::string condVar = encodeCond(condCount++); std::stringstream condVarEncoded; @@ -969,7 +973,7 @@ public: std::string SStr; llvm::raw_string_ostream S(SStr); - cond->printPretty(S, nullptr, Rewrite.getLangOpts()); + cond->printPretty(S, nullptr, rewrite.getLangOpts()); const std::string &Str = S.str(); std::stringstream prel; @@ -999,7 +1003,7 @@ public: // rewrite the call op with the newly-inserted var SourceRange SR(cond->getLocStart(), cond->getLocEnd()); Redirector[cond] = is->getLocStart(); - Rewrite.ReplaceText(SR, condVar); + rewrite.ReplaceText(SR, condVar); } std::deque q; @@ -1025,7 +1029,7 @@ public: } private: - Rewriter &Rewrite; + Rewriter &rewrite; std::set & DeclsInCond; std::map &DeclToMCVar; std::map &ExprToMCVar; @@ -1038,7 +1042,7 @@ public: BranchAnnotationHandler(Rewriter &rewrite, std::map & DeclToMCVar, std::map & ExprToMCVar) - : Rewrite(rewrite), + : rewrite(rewrite), DeclToMCVar(DeclToMCVar), ExprToMCVar(ExprToMCVar){} virtual void run(const MatchFinder::MatchResult &Result) { @@ -1065,7 +1069,8 @@ public: std::stringstream brline; brline << "MCID " << brVar << ";\n"; - Rewrite.InsertText(is->getLocStart(), brline.str(), false, true); + rewrite.InsertText(rewrite.getSourceMgr().getExpansionLoc(is->getLocStart()), + brline.str(), false, true); Stmt * ts = is->getThen(), * es = is->getElse(); bool tHasChild = hasChild(ts); @@ -1087,7 +1092,7 @@ public: mergeStmt << "\tMC2_merge(" << brVar << ");\n"; - Rewrite.InsertText(tfl, tlineStart.str(), false, true); + rewrite.InsertText(rewrite.getSourceMgr().getExpansionLoc(tfl), tlineStart.str(), false, true); Stmt * tls = NULL; int extra_else_offset = 0; @@ -1097,13 +1102,13 @@ public: if (!tHasChild || (!isa(tls) && !isa(tls))) { extra_else_offset = 0; - Rewrite.InsertText(tsl.getLocWithOffset(1), mergeStmt.str(), true, true); + rewrite.InsertText(rewrite.getSourceMgr().getExpansionLoc(tsl.getLocWithOffset(1)), + mergeStmt.str(), true, true); } if (tHasChild && !isa(ts)) { - Rewrite.InsertText(tls->getLocStart(), "{", false, true); - SourceLocation tend = Lexer::getLocForEndOfToken(tls->getLocStart(), 0, Rewrite.getSourceMgr(), Rewrite.getLangOpts()); - Rewrite.InsertText(tend.getLocWithOffset(2), "}", true, true); - extra_else_offset++; + rewrite.InsertText(rewrite.getSourceMgr().getFileLoc(tls->getLocStart()), "{", false, true); + SourceLocation tend = Lexer::findLocationAfterToken(tls->getLocEnd(), tok::semi, rewrite.getSourceMgr(), rewrite.getLangOpts(), false); + rewrite.InsertText(tend, "}", true, true); } if (tHasChild && isa(ts)) extra_else_offset++; @@ -1124,22 +1129,23 @@ public: } } else el = es->getLocStart().getLocWithOffset(1); - Rewrite.InsertText(el, eline.str(), false, true); + rewrite.InsertText(rewrite.getSourceMgr().getExpansionLoc(el), eline.str(), false, true); if (eHasChild && !isa(es)) { - Rewrite.InsertText(el, "{", false, true); - Rewrite.InsertText(es->getLocEnd().getLocWithOffset(1), "}", true, true); + rewrite.InsertText(rewrite.getSourceMgr().getExpansionLoc(el), "{", false, true); + rewrite.InsertText(rewrite.getSourceMgr().getExpansionLoc(es->getLocEnd().getLocWithOffset(1)), "}", true, true); } if (!eHasChild || (!isa(els) && !isa(els))) - Rewrite.InsertText(esl.getLocWithOffset(1), mergeStmt.str(), true, true); + rewrite.InsertText(rewrite.getSourceMgr().getExpansionLoc(esl.getLocWithOffset(1)), mergeStmt.str(), true, true); } else { std::stringstream eCompoundLine; eCompoundLine << " else { " << eline.str() << mergeStmt.str() << " }"; - SourceLocation tend = Lexer::getLocForEndOfToken(ts->getLocEnd(), 0, Rewrite.getSourceMgr(), Rewrite.getLangOpts()); - Rewrite.InsertText(tend.getLocWithOffset(extra_else_offset), - eCompoundLine.str(), false, true); + SourceLocation tend = Lexer::findLocationAfterToken(ts->getLocEnd(), tok::semi, rewrite.getSourceMgr(), rewrite.getLangOpts(), false); + if (!tend.isValid()) + tend = Lexer::getLocForEndOfToken(ts->getLocEnd(), 0, rewrite.getSourceMgr(), rewrite.getLangOpts()); + rewrite.InsertText(tend.getLocWithOffset(1), eCompoundLine.str(), false, true); } } private: @@ -1164,7 +1170,7 @@ private: return s; } - Rewriter &Rewrite; + Rewriter &rewrite; std::map &DeclToMCVar; std::map &ExprToMCVar; }; @@ -1208,12 +1214,14 @@ public: std::stringstream brline; brline << "MCID " << mc_rv << ";\n"; - rewrite.InsertText(s->getLocStart(), brline.str(), false, true); + rewrite.InsertText(rewrite.getSourceMgr().getExpansionLoc(s->getLocStart()), + brline.str(), false, true); std::stringstream nol; if (ce->getNumArgs() > 0) nol << ", "; nol << "&" << mc_rv; - rewrite.InsertTextBefore(ce->getRParenLoc(), nol.str()); + rewrite.InsertTextBefore(rewrite.getSourceMgr().getExpansionLoc(ce->getRParenLoc()), + nol.str()); if (s && (ds = dyn_cast(s))) { if (!ds->isSingleDecl()) { @@ -1247,7 +1255,8 @@ public: nol << aa << ", "; if (a->getLocEnd().isValid()) - rewrite.InsertTextBefore(a->getLocStart(), nol.str()); + rewrite.InsertTextBefore(rewrite.getSourceMgr().getExpansionLoc(a->getLocStart()), + nol.str()); } } @@ -1286,7 +1295,8 @@ public: } std::stringstream nol; nol << "*retval = " << mrv << ";\n"; - rewrite.InsertText(rs->getLocStart(), nol.str(), false, true); + rewrite.InsertText(rewrite.getSourceMgr().getExpansionLoc(rs->getLocStart()), + nol.str(), false, true); } private: @@ -1317,7 +1327,8 @@ public: nol << "MCID " << dn << "; "; if (d->getLocStart().isValid()) - rewrite.InsertTextBefore(d->getLocStart(), nol.str()); + rewrite.InsertTextBefore(rewrite.getSourceMgr().getExpansionLoc(d->getLocStart()), + nol.str()); } private: @@ -1346,7 +1357,8 @@ public: std::stringstream nol; nol << "MCID " << encode(p->getName()) << ", "; if (p->getLocStart().isValid()) - rewrite.InsertText(p->getLocStart(), nol.str(), false); + rewrite.InsertText(rewrite.getSourceMgr().getExpansionLoc(p->getLocStart()), + nol.str(), false); if (p->getLocEnd().isValid()) LastParam = p->getLocEnd().getLocWithOffset(p->getName().size()); } @@ -1355,7 +1367,8 @@ public: std::stringstream nol; if (fd->param_size() > 0) nol << ", "; nol << "MCID * retval"; - rewrite.InsertText(LastParam, nol.str(), false); + rewrite.InsertText(rewrite.getSourceMgr().getExpansionLoc(LastParam), + nol.str(), false); } } @@ -1464,7 +1477,7 @@ public: MatcherSanity.matchAST(Context); for (auto & u : DeferredUpdates) { - R.InsertText(u->loc, u->update, true, true); + R.InsertText(R.getSourceMgr().getExpansionLoc(u->loc), u->update, true, true); delete u; } DeferredUpdates.clear(); diff --git a/clang/test/fib_easy_false.c b/clang/test/fib_easy_false.c new file mode 100644 index 0000000..bdee81c --- /dev/null +++ b/clang/test/fib_easy_false.c @@ -0,0 +1,54 @@ +/* Adapted from: https://svn.sosy-lab.org/software/sv-benchmarks/trunk/c/pthread/fib_bench_true-unreach-call.c */ + +#include +#include +#include +#include "libinterface.h" + +/* volatile */ int i, j; + +#define NULL 0 + +void t1(void* arg) { + + int t1, t2; + + t1 = load_32(&i); + t2 = load_32(&j); + store_32(&i, t1 + t2); + + t1 = load_32(&i); + if (t1 >= 3) { + assert(0); + } +} + +void t2(void* arg) { + + int t1, t2; + + t1 = load_32(&j); + t2 = load_32(&i); + store_32(&j, t1 + t2); + + t1 = load_32(&j); + if (t1 >= 3) { + assert(0); + } +} + +int user_main(int argc, char **argv) +{ + thrd_t a, b; + + store_32(&i, 1); + store_32(&j, 1); + + thrd_create(&a, t1, NULL); + thrd_create(&b, t2, NULL); + + thrd_join(a); + thrd_join(b); + + return 0; +} diff --git a/clang/test/fib_easy_true.c b/clang/test/fib_easy_true.c new file mode 100644 index 0000000..7a49e2e --- /dev/null +++ b/clang/test/fib_easy_true.c @@ -0,0 +1,54 @@ +/* Adapted from: https://svn.sosy-lab.org/software/sv-benchmarks/trunk/c/pthread/fib_bench_true-unreach-call.c */ + +#include +#include +#include +#include "libinterface.h" + +/* volatile */ int i, j; + +#define NULL 0 + +void t1(void* arg) { + + int t1, t2; + + t1 = load_32(&i); + t2 = load_32(&j); + store_32(&i, t1 + t2); + + t1 = load_32(&i); + if (t1 > 3) { + assert(0); + } +} + +void t2(void* arg) { + + int t1, t2; + + t1 = load_32(&j); + t2 = load_32(&i); + store_32(&j, t1 + t2); + + t1 = load_32(&j); + if (t1 > 3) { + assert(0); + } +} + +int user_main(int argc, char **argv) +{ + thrd_t a, b; + + store_32(&i, 1); + store_32(&j, 1); + + thrd_create(&a, t1, NULL); + thrd_create(&b, t2, NULL); + + thrd_join(a); + thrd_join(b); + + return 0; +} diff --git a/clang/test/fib_easy_true_if.c b/clang/test/fib_easy_true_if.c new file mode 100644 index 0000000..9fbc761 --- /dev/null +++ b/clang/test/fib_easy_true_if.c @@ -0,0 +1,54 @@ +/* Adapted from: https://svn.sosy-lab.org/software/sv-benchmarks/trunk/c/pthread/fib_bench_true-unreach-call.c */ + +#include +#include +#include +#include "libinterface.h" + +/* volatile */ int i, j; + +#define NULL 0 + +void t1(void* arg) { + + int t1, t2; + + t1 = load_32(&i); + t2 = load_32(&j); + store_32(&i, t1 + t2); + + t1 = load_32(&i); + if (t1 > 3) + assert(0); + else + ; +} + +void t2(void* arg) { + + int t1, t2; + + t1 = load_32(&j); + t2 = load_32(&i); + store_32(&j, t1 + t2); + + t1 = load_32(&j); + if (t1 > 3) + assert(0); +} + +int user_main(int argc, char **argv) +{ + thrd_t a, b; + + store_32(&i, 1); + store_32(&j, 1); + + thrd_create(&a, t1, NULL); + thrd_create(&b, t2, NULL); + + thrd_join(a); + thrd_join(b); + + return 0; +}