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 c5319338dc1f287c873b731db160e89b76609d0e..ac796c973b934cbf0ac3f1ae774a6fdf2fee91dd 100644 (file)
--- 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 1b7c92604e31547ebb3e3ce77746fda8b4df9062..a2539e545c3a98d1e9884429a49e9c00edd2cf44 100644 (file)
--- 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 <prof.lam@gmail.com>
@@ -725,7 +725,8 @@ public:
     virtual void run(const MatchFinder::MatchResult &Result) {
         const Stmt * s = Result.Nodes.getNodeAs<Stmt>("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<const NamedDecl *> & DeclsInCond,
                                       std::map<const NamedDecl *, std::string> &DeclToMCVar,
                                       std::map<const Expr *, std::string> &ExprToMCVar,
                                       std::map<const Expr *, SourceLocation> &Redirector,
                                       std::vector<Update *> &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<const Decl *> q;
@@ -1025,7 +1029,7 @@ public:
     }
 
 private:
-    Rewriter &Rewrite;
+    Rewriter &rewrite;
     std::set<const NamedDecl *> & DeclsInCond;
     std::map<const NamedDecl *, std::string> &DeclToMCVar;
     std::map<const Expr *, std::string> &ExprToMCVar;
@@ -1038,7 +1042,7 @@ public:
     BranchAnnotationHandler(Rewriter &rewrite,
                             std::map<const NamedDecl *, std::string> & DeclToMCVar,
                             std::map<const Expr *, std::string> & 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<ReturnStmt>(tls) && !isa<BreakStmt>(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<CompoundStmt>(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<CompoundStmt>(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<CompoundStmt>(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<ReturnStmt>(els) && !isa<BreakStmt>(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<const NamedDecl *, std::string> &DeclToMCVar;
     std::map<const Expr *, std::string> &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<DeclStmt>(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 (file)
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 <assert.h>
+#include <stdbool.h>
+#include <threads.h>
+#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 (file)
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 <assert.h>
+#include <stdbool.h>
+#include <threads.h>
+#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 (file)
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 <assert.h>
+#include <stdbool.h>
+#include <threads.h>
+#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;
+}