From c0828349d8d79e469f450fb1e6b8dd717637c5f0 Mon Sep 17 00:00:00 2001 From: Patrick Lam Date: Sun, 4 Oct 2015 23:17:51 +0200 Subject: [PATCH 1/1] add MC2_function call for assignments where RHS computed from loads; tweak tests --- .../linuxlock/linuxlocks.c | 4 +- .../linuxrwlock/linuxrwlocks.c | 2 +- .../msqueueoffset/ms-queue-simple.c | 4 +- clang/src/add_mc2_annotations.cpp | 47 +++++++++++++------ clang/test/fib_easy_true.c | 18 +++---- 5 files changed, 48 insertions(+), 27 deletions(-) diff --git a/benchmarks/satcheck-precompiled/linuxlock/linuxlocks.c b/benchmarks/satcheck-precompiled/linuxlock/linuxlocks.c index db75025..366a163 100644 --- 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 150b68a..a48768b 100644 --- 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 e819eb7..4419974 100644 --- 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 a2539e5..07246f9 100644 --- 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(Result.Nodes.getNodeAs("op")); const Stmt * s = Result.Nodes.getNodeAs("containingStmt"); - FindLocalsVisitor flv; + FindLocalsVisitor locals, locals_rhs; const VarDecl * lhs = NULL; const Expr * rhs = NULL; @@ -810,10 +810,11 @@ public: } std::set mcState; + bool lhsUsedInCond; + bool rhsRead = false; + bool lhsTooComplicated = false; if (op) { - flv.TraverseStmt(op); - DeclRefExpr * vd; if ((vd = dyn_cast(op->getLHS()))) lhs = dyn_cast(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(cast(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(cast(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(cast(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 DeclsRead, DeclsInCond; + std::set DeclsRead; + /* DeclsInCond contains all local variables 'x' used in a branch condition or rmw parameter */ + std::set DeclsInCond; std::map DeclToMCVar; std::map ExprToMCVar; std::set DeclsNeedingMC; diff --git a/clang/test/fib_easy_true.c b/clang/test/fib_easy_true.c index 7a49e2e..cad94dd 100644 --- 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); } } -- 2.34.1