add MC2_function call for assignments where RHS computed from loads; tweak tests

diff --git a/benchmarks/satcheck-precompiled/linuxlock/linuxlocks.c b/benchmarks/satcheck-precompiled/linuxlock/linuxlocks.c
index db7502555ac3c663b07b881dbb1ac619511147de..366a1639b5406a4ba5bfd040ee0a6497f23c1903 100644 (file)
--- a/benchmarks/satcheck-precompiled/linuxlock/linuxlocks.c
+++ b/benchmarks/satcheck-precompiled/linuxlock/linuxlocks.c
@@ -58,8 +58,8 @@ int user_main(int argc, char **argv)
 {
        thrd_t t1, t2;//, t3, t4;
        mylock = (rwlock_t*)malloc(sizeof(rwlock_t));
-       _fn0 = MC2_function_id(0, 0, sizeof (mylock), (uint64_t)mylock); 
-       MC2_nextOpStoreOffset(_fn0, MC2_OFFSET(rwlock_t *, lock), MCID_NODEP);
+
+       _fn0 = MC2_function_id(0, 0, sizeof (mylock), (uint64_t)mylock);        MC2_nextOpStoreOffset(_fn0, MC2_OFFSET(rwlock_t *, lock), MCID_NODEP);
        store_32(&mylock->lock, 0);
 
        thrd_create(&t1, (thrd_start_t)&a, NULL);

diff --git a/benchmarks/satcheck-precompiled/linuxrwlock/linuxrwlocks.c b/benchmarks/satcheck-precompiled/linuxrwlock/linuxrwlocks.c
index 150b68a5b6f83f005eb4823628f398cc4800e44f..a48768b0b2ef1beffe87176035b1376f5814b668 100644 (file)
--- a/benchmarks/satcheck-precompiled/linuxrwlock/linuxrwlocks.c
+++ b/benchmarks/satcheck-precompiled/linuxrwlock/linuxrwlocks.c
@@ -179,8 +179,8 @@ MC2_exitLoop();
 int user_main(int argc, char **argv)
 {
        mylock = (rwlock_t*)malloc(sizeof(rwlock_t));
-       _fn1 = MC2_function_id(0, 0, sizeof (mylock), (uint64_t)mylock); 
 
+_fn1 = MC2_function_id(0, 0, sizeof (mylock), (uint64_t)mylock); 
        thrd_t t1, t2;
        //, t3, t4;
        MC2_nextOpStoreOffset(_fn1, MC2_OFFSET(rwlock_t *, lock), MCID_NODEP);

diff --git a/benchmarks/satcheck-precompiled/msqueueoffset/ms-queue-simple.c b/benchmarks/satcheck-precompiled/msqueueoffset/ms-queue-simple.c
index e819eb7d1cdda144d0e22b4520d0bfd07dcc3981..44199745b09ca809c38375bf01a03518ac086c88 100644 (file)
--- a/benchmarks/satcheck-precompiled/msqueueoffset/ms-queue-simple.c
+++ b/benchmarks/satcheck-precompiled/msqueueoffset/ms-queue-simple.c
@@ -37,8 +37,8 @@ void init_queue(MCID _mq, queue_t *q, MCID _mnum_threads, int num_threads) {
 void enqueue(MCID _mq, queue_t *q, MCID _mval, unsigned int val) {
        MCID _mtail; struct node *tail;
        MCID _fn1; struct node * node_ptr; node_ptr = (struct node *)malloc(sizeof(struct node));
-       _fn1 = MC2_function_id(0, 1, sizeof (node_ptr), (uint64_t)node_ptr, _fn1); 
-       
+
+       _fn1 = MC2_function_id(0, 0, sizeof (node_ptr), (uint64_t)node_ptr);    
        MC2_nextOpStoreOffset(_fn1, MC2_OFFSET(struct node *, value), _mval);
        store_32(&node_ptr->value, val);
        

diff --git a/clang/src/add_mc2_annotations.cpp b/clang/src/add_mc2_annotations.cpp
index a2539e545c3a98d1e9884429a49e9c00edd2cf44..07246f9cc99f3beaaef2ede15b25649d4f8e2f0a 100644 (file)
--- a/clang/src/add_mc2_annotations.cpp
+++ b/clang/src/add_mc2_annotations.cpp
@@ -774,7 +774,7 @@ public:
     virtual void run(const MatchFinder::MatchResult &Result) {
         BinaryOperator * op = const_cast<BinaryOperator *>(Result.Nodes.getNodeAs<BinaryOperator>("op"));
         const Stmt * s = Result.Nodes.getNodeAs<Stmt>("containingStmt");
-        FindLocalsVisitor flv;
+        FindLocalsVisitor locals, locals_rhs;
 
         const VarDecl * lhs = NULL;
         const Expr * rhs = NULL;
@@ -810,10 +810,11 @@ public:
         }
         std::set<std::string> mcState;
 
+        bool lhsUsedInCond;
+        bool rhsRead = false;
+
         bool lhsTooComplicated = false;
         if (op) {
-            flv.TraverseStmt(op);
-
             DeclRefExpr * vd;
             if ((vd = dyn_cast<DeclRefExpr>(op->getLHS())))
                 lhs = dyn_cast<VarDecl>(vd->getDecl());
@@ -826,21 +827,37 @@ public:
             if (rhs) 
                 rhs = rhs->IgnoreCasts();
         }
-        else if (lhs) {
-            // rhs must be MC-active state, i.e. in declsread
-            // lhs must be subsequently used in (1) store/load or (2) branch condition or (3) other functions and (3a) uses values from other functions or (3b) uses values from loads, stores, or phi functions
-            flv.TraverseStmt(const_cast<Stmt *>(cast<Stmt>(rhs)));
+
+        // rhs must be MC-active state, i.e. in declsread
+        // lhs must be subsequently used in (1) store/load or (2) branch condition or (3) other functions and (3a) uses values from other functions or (3b) uses values from loads, stores, or phi functions
+
+        if (rhs) {
+            locals_rhs.TraverseStmt(const_cast<Stmt *>(cast<Stmt>(rhs)));
+            for (auto & nd : locals_rhs.RetrieveVars()) {
+                if (DeclsRead.find(nd) != DeclsRead.end())
+                    rhsRead = true;
+            }
         }
 
-        if (DeclsInCond.find(lhs) != DeclsInCond.end()) {
-            for (auto & d : flv.RetrieveVars()) {
+        locals.TraverseStmt(const_cast<Stmt *>(cast<Stmt>(rhs)));
+
+        lhsUsedInCond = DeclsInCond.find(lhs) != DeclsInCond.end();
+        if (lhsUsedInCond) {
+            for (auto & d : locals.RetrieveVars()) {
+                if (DeclToMCVar.count(d) > 0)
+                    mcState.insert(DeclToMCVar[d]);
+                else if (DeclsRead.find(d) != DeclsRead.end())
+                    mcState.insert(encode(d->getName().str()));
+            }
+        }
+        if (rhsRead) {
+            for (auto & d : locals_rhs.RetrieveVars()) {
                 if (DeclToMCVar.count(d) > 0)
                     mcState.insert(DeclToMCVar[d]);
                 else if (DeclsRead.find(d) != DeclsRead.end())
                     mcState.insert(encode(d->getName().str()));
             }
         }
-
         if (mcState.size() > 0 || MallocExprs.find(rhs) != MallocExprs.end()) {
             if (lhsTooComplicated)
                 assert(0 && "couldn't find LHS of = operator");
@@ -871,9 +888,9 @@ public:
             }
             nol << "); ";
             SourceLocation place;
-            if (op)
-                place = op->getLocEnd().getLocWithOffset(1);
-            else
+            if (op) {
+                place = Lexer::getLocForEndOfToken(op->getLocEnd(), 0, rewrite.getSourceMgr(), rewrite.getLangOpts()).getLocWithOffset(1);
+            } else
                 place = s->getLocEnd();
             rewrite.InsertText(rewrite.getSourceMgr().getExpansionLoc(place.getLocWithOffset(1)),
                                nol.str(), true, true);
@@ -1487,7 +1504,9 @@ private:
     /* DeclsRead contains all local variables 'x' which:
     * 1) appear in 'x = load_32(...);
     * 2) appear in 'y = store_32(x); */
-    std::set<const NamedDecl *> DeclsRead, DeclsInCond;
+    std::set<const NamedDecl *> DeclsRead;
+    /* DeclsInCond contains all local variables 'x' used in a branch condition or rmw parameter */
+    std::set<const NamedDecl *> DeclsInCond;
     std::map<const NamedDecl *, std::string> DeclToMCVar;
     std::map<const Expr *, std::string> ExprToMCVar;
     std::set<const VarDecl *> DeclsNeedingMC;

diff --git a/clang/test/fib_easy_true.c b/clang/test/fib_easy_true.c
index 7a49e2efa1c10fb9f43a49b30fe9b50ac6f330d1..cad94dd015a90aec9b1f18cb904370912ff2b11c 100644 (file)
--- a/clang/test/fib_easy_true.c
+++ b/clang/test/fib_easy_true.c
@@ -11,11 +11,12 @@
 
 void t1(void* arg) {
 
-  int t1, t2;
+  int t1, t2, sum;
 
   t1 = load_32(&i);
   t2 = load_32(&j);
-  store_32(&i, t1 + t2);
+  sum = t1 + t2;
+  store_32(&i, sum);
 
   t1 = load_32(&i);
   if (t1 > 3) {
@@ -25,14 +26,15 @@ void t1(void* arg) {
 
 void t2(void* arg) {
 
-  int t1, t2;
+  int tt1, tt2, sum;
 
-  t1 = load_32(&j);
-  t2 = load_32(&i);
-  store_32(&j, t1 + t2);
+  tt1 = load_32(&j);
+  tt2 = load_32(&i);
+  sum = tt1 + tt2;
+  store_32(&j, sum);
 
-  t1 = load_32(&j);
-  if (t1 > 3) {
+  tt1 = load_32(&j);
+  if (tt1 > 3) {
     assert(0);
   }
 }