[PATCH] D32449: Modifying PthreadLockChecker.cpp to reduce false positives.
This revision was automatically updated to reflect the committed changes.
Closed by commit rL304159: [analyzer] PthreadLockChecker: model failed
pthread_mutex_destroy() calls. (authored by dergachev).
Changed prior to commit:
https://reviews.llvm.org/D32449?vs=99970&id=100615#toc
Repository:
rL LLVM
https://reviews.llvm.org/D32449
Files:
cfe/trunk/lib/StaticAnalyzer/Checkers/PthreadLockChecker.cpp
cfe/trunk/test/Analysis/pthreadlock.c
Index: cfe/trunk/test/Analysis/pthreadlock.c
===
--- cfe/trunk/test/Analysis/pthreadlock.c
+++ cfe/trunk/test/Analysis/pthreadlock.c
@@ -176,6 +176,42 @@
pthread_mutex_unlock(pmtx); // no-warning
}
+void ok23(void) {
+ if (pthread_mutex_destroy(&mtx1) != 0) // no-warning
+pthread_mutex_destroy(&mtx1);// no-warning
+}
+
+void ok24(void) {
+ if (pthread_mutex_destroy(&mtx1) != 0) // no-warning
+pthread_mutex_lock(&mtx1); // no-warning
+}
+
+void ok25(void) {
+ if (pthread_mutex_destroy(&mtx1) != 0) // no-warning
+pthread_mutex_unlock(&mtx1); // no-warning
+}
+
+void ok26(void) {
+ pthread_mutex_unlock(&mtx1); // no-warning
+ if (pthread_mutex_destroy(&mtx1) != 0) // no-warning
+pthread_mutex_lock(&mtx1); // no-warning
+}
+
+void ok27(void) {
+ pthread_mutex_unlock(&mtx1); // no-warning
+ if (pthread_mutex_destroy(&mtx1) != 0) // no-warning
+pthread_mutex_lock(&mtx1); // no-warning
+ else
+pthread_mutex_init(&mtx1, NULL); // no-warning
+}
+
+void ok28(void) {
+ if (pthread_mutex_destroy(&mtx1) != 0) { // no-warning
+pthread_mutex_lock(&mtx1); // no-warning
+pthread_mutex_unlock(&mtx1); // no-warning
+pthread_mutex_destroy(&mtx1); // no-warning
+ }
+}
void
bad1(void)
@@ -392,3 +428,46 @@
pthread_mutex_unlock(&mtx1); // no-warning
pthread_mutex_init(&mtx1, NULL); // expected-warning{{This lock has already been initialized}}
}
+
+void bad27(void) {
+ pthread_mutex_unlock(&mtx1);// no-warning
+ int ret = pthread_mutex_destroy(&mtx1); // no-warning
+ if (ret != 0) // no-warning
+pthread_mutex_lock(&mtx1);// no-warning
+ else
+pthread_mutex_unlock(&mtx1); // expected-warning{{This lock has already been destroyed}}
+}
+
+void bad28(void) {
+ pthread_mutex_unlock(&mtx1);// no-warning
+ int ret = pthread_mutex_destroy(&mtx1); // no-warning
+ if (ret != 0) // no-warning
+pthread_mutex_lock(&mtx1);// no-warning
+ else
+pthread_mutex_lock(&mtx1); // expected-warning{{This lock has already been destroyed}}
+}
+
+void bad29(void) {
+ pthread_mutex_lock(&mtx1); // no-warning
+ pthread_mutex_unlock(&mtx1); // no-warning
+ if (pthread_mutex_destroy(&mtx1) != 0) // no-warning
+pthread_mutex_init(&mtx1, NULL); // expected-warning{{This lock has already been initialized}}
+ else
+pthread_mutex_init(&mtx1, NULL); // no-warning
+}
+
+void bad30(void) {
+ pthread_mutex_lock(&mtx1); // no-warning
+ pthread_mutex_unlock(&mtx1); // no-warning
+ if (pthread_mutex_destroy(&mtx1) != 0) // no-warning
+pthread_mutex_init(&mtx1, NULL); // expected-warning{{This lock has already been initialized}}
+ else
+pthread_mutex_destroy(&mtx1); // expected-warning{{This lock has already been destroyed}}
+}
+
+void bad31(void) {
+ int ret = pthread_mutex_destroy(&mtx1); // no-warning
+ pthread_mutex_lock(&mtx1); // expected-warning{{This lock has already been destroyed}}
+ if (ret != 0)
+pthread_mutex_lock(&mtx1);
+}
Index: cfe/trunk/lib/StaticAnalyzer/Checkers/PthreadLockChecker.cpp
===
--- cfe/trunk/lib/StaticAnalyzer/Checkers/PthreadLockChecker.cpp
+++ cfe/trunk/lib/StaticAnalyzer/Checkers/PthreadLockChecker.cpp
@@ -25,30 +25,49 @@
namespace {
struct LockState {
- enum Kind { Destroyed, Locked, Unlocked } K;
+ enum Kind {
+Destroyed,
+Locked,
+Unlocked,
+UntouchedAndPossiblyDestroyed,
+UnlockedAndPossiblyDestroyed
+ } K;
private:
LockState(Kind K) : K(K) {}
public:
static LockState getLocked() { return LockState(Locked); }
static LockState getUnlocked() { return LockState(Unlocked); }
static LockState getDestroyed() { return LockState(Destroyed); }
+ static LockState getUntouchedAndPossiblyDestroyed() {
+return LockState(UntouchedAndPossiblyDestroyed);
+ }
+ static LockState getUnlockedAndPossiblyDestroyed() {
+return LockState(UnlockedAndPossiblyDestroyed);
+ }
bool operator==(const LockState &X) const {
return K == X.K;
}
bool isLocked() const { return K == Locked; }
bool isUnlocked() const { return K == Unlocked; }
bool isDestroyed() const { return K == Destroyed; }
+ bool isUntouchedAndPossiblyDestroyed() const {
+retu
[PATCH] D32449: Modifying PthreadLockChecker.cpp to reduce false positives.
NoQ accepted this revision. NoQ added a comment. This revision is now accepted and ready to land. I'd commit your patch without the .gitignore change, as it deserves a separate commit and more attention; will have a look at it myself - llvm's and clang's .gitignores have diverged quite a bit. Thanks for taking this up!~ Repository: rL LLVM https://reviews.llvm.org/D32449 ___ cfe-commits mailing list cfe-commits@lists.llvm.org http://lists.llvm.org/cgi-bin/mailman/listinfo/cfe-commits
[PATCH] D32449: Modifying PthreadLockChecker.cpp to reduce false positives.
malhar1995 updated this revision to Diff 99970.
malhar1995 added a comment.
Applied clang-format only to the changed lines in the final code.
Repository:
rL LLVM
https://reviews.llvm.org/D32449
Files:
.gitignore
lib/StaticAnalyzer/Checkers/PthreadLockChecker.cpp
test/Analysis/pthreadlock.c
Index: test/Analysis/pthreadlock.c
===
--- test/Analysis/pthreadlock.c
+++ test/Analysis/pthreadlock.c
@@ -176,6 +176,42 @@
pthread_mutex_unlock(pmtx); // no-warning
}
+void ok23(void) {
+ if (pthread_mutex_destroy(&mtx1) != 0) // no-warning
+pthread_mutex_destroy(&mtx1);// no-warning
+}
+
+void ok24(void) {
+ if (pthread_mutex_destroy(&mtx1) != 0) // no-warning
+pthread_mutex_lock(&mtx1); // no-warning
+}
+
+void ok25(void) {
+ if (pthread_mutex_destroy(&mtx1) != 0) // no-warning
+pthread_mutex_unlock(&mtx1); // no-warning
+}
+
+void ok26(void) {
+ pthread_mutex_unlock(&mtx1); // no-warning
+ if (pthread_mutex_destroy(&mtx1) != 0) // no-warning
+pthread_mutex_lock(&mtx1); // no-warning
+}
+
+void ok27(void) {
+ pthread_mutex_unlock(&mtx1); // no-warning
+ if (pthread_mutex_destroy(&mtx1) != 0) // no-warning
+pthread_mutex_lock(&mtx1); // no-warning
+ else
+pthread_mutex_init(&mtx1, NULL); // no-warning
+}
+
+void ok28(void) {
+ if (pthread_mutex_destroy(&mtx1) != 0) { // no-warning
+pthread_mutex_lock(&mtx1); // no-warning
+pthread_mutex_unlock(&mtx1); // no-warning
+pthread_mutex_destroy(&mtx1); // no-warning
+ }
+}
void
bad1(void)
@@ -392,3 +428,46 @@
pthread_mutex_unlock(&mtx1); // no-warning
pthread_mutex_init(&mtx1, NULL); // expected-warning{{This lock has already been initialized}}
}
+
+void bad27(void) {
+ pthread_mutex_unlock(&mtx1);// no-warning
+ int ret = pthread_mutex_destroy(&mtx1); // no-warning
+ if (ret != 0) // no-warning
+pthread_mutex_lock(&mtx1);// no-warning
+ else
+pthread_mutex_unlock(&mtx1); // expected-warning{{This lock has already been destroyed}}
+}
+
+void bad28(void) {
+ pthread_mutex_unlock(&mtx1);// no-warning
+ int ret = pthread_mutex_destroy(&mtx1); // no-warning
+ if (ret != 0) // no-warning
+pthread_mutex_lock(&mtx1);// no-warning
+ else
+pthread_mutex_lock(&mtx1); // expected-warning{{This lock has already been destroyed}}
+}
+
+void bad29(void) {
+ pthread_mutex_lock(&mtx1); // no-warning
+ pthread_mutex_unlock(&mtx1); // no-warning
+ if (pthread_mutex_destroy(&mtx1) != 0) // no-warning
+pthread_mutex_init(&mtx1, NULL); // expected-warning{{This lock has already been initialized}}
+ else
+pthread_mutex_init(&mtx1, NULL); // no-warning
+}
+
+void bad30(void) {
+ pthread_mutex_lock(&mtx1); // no-warning
+ pthread_mutex_unlock(&mtx1); // no-warning
+ if (pthread_mutex_destroy(&mtx1) != 0) // no-warning
+pthread_mutex_init(&mtx1, NULL); // expected-warning{{This lock has already been initialized}}
+ else
+pthread_mutex_destroy(&mtx1); // expected-warning{{This lock has already been destroyed}}
+}
+
+void bad31(void) {
+ int ret = pthread_mutex_destroy(&mtx1); // no-warning
+ pthread_mutex_lock(&mtx1); // expected-warning{{This lock has already been destroyed}}
+ if (ret != 0)
+pthread_mutex_lock(&mtx1);
+}
Index: lib/StaticAnalyzer/Checkers/PthreadLockChecker.cpp
===
--- lib/StaticAnalyzer/Checkers/PthreadLockChecker.cpp
+++ lib/StaticAnalyzer/Checkers/PthreadLockChecker.cpp
@@ -25,30 +25,49 @@
namespace {
struct LockState {
- enum Kind { Destroyed, Locked, Unlocked } K;
+ enum Kind {
+Destroyed,
+Locked,
+Unlocked,
+UntouchedAndPossiblyDestroyed,
+UnlockedAndPossiblyDestroyed
+ } K;
private:
LockState(Kind K) : K(K) {}
public:
static LockState getLocked() { return LockState(Locked); }
static LockState getUnlocked() { return LockState(Unlocked); }
static LockState getDestroyed() { return LockState(Destroyed); }
+ static LockState getUntouchedAndPossiblyDestroyed() {
+return LockState(UntouchedAndPossiblyDestroyed);
+ }
+ static LockState getUnlockedAndPossiblyDestroyed() {
+return LockState(UnlockedAndPossiblyDestroyed);
+ }
bool operator==(const LockState &X) const {
return K == X.K;
}
bool isLocked() const { return K == Locked; }
bool isUnlocked() const { return K == Unlocked; }
bool isDestroyed() const { return K == Destroyed; }
+ bool isUntouchedAndPossiblyDestroyed() const {
+return K == UntouchedAndPossiblyDestroyed;
+ }
+ bool isUnlockedAndPossiblyDestroyed() const {
+return K == UnlockedAndPossiblyDestroyed;
+ }
void Profile(llvm::FoldingSetNodeID &ID) const {
ID.A
[PATCH] D32449: Modifying PthreadLockChecker.cpp to reduce false positives.
NoQ added a comment.
No-no, all i was trying to say is that there's code in `PthreadLockChecker.cpp`
that you haven't changed, but accidentally reformatted - and this is something
we normally try to avoid. Like, for example, changing `enum LockingSemantics
{...}` from vertical to horizontal - that wasn't your intention, it just
accidentally happened because you auto-reformatted the whole file. I don't mind
these changes, and i didn't mean they introduce any merge conflicts for now,
though they tend to do so in the future for other people working on the same
code, as we have a few downstream users, and magenta guys who are working on
this checker as part of https://reviews.llvm.org/D26342), so most of the time
it's better not to introduce unnecessary changes.
I'm not sure if you can easily revert the style-only changes via `git
clang-format`, but you should be able to find them with the help of `git
reflog` if you made a local commit before running clang-format (even if it was
later discarded or amended), otherwise only manually i guess.
Repository:
rL LLVM
https://reviews.llvm.org/D32449
___
cfe-commits mailing list
cfe-commits@lists.llvm.org
http://lists.llvm.org/cgi-bin/mailman/listinfo/cfe-commits
[PATCH] D32449: Modifying PthreadLockChecker.cpp to reduce false positives.
malhar1995 added a comment. In https://reviews.llvm.org/D32449#761303, @NoQ wrote: > Thanks, this is great! Two more things: > > - You have touched other code, unrelated to your patch, with clang-format; > we're usually trying to avoid that, because it creates merge conflicts out of > nowhere, and because some of that code actually seems formatted by hand > intentionally. It's better to revert these changes; you can use the `git > clang-format` thing to format only actual changes. I did not apply clang-format to any file except for PthreadLockChecker.cpp. Do you think the merge conflict is due to me not applying clang-format to test/Analysis/pthreadlock.c? The only files I changed were .gitignore, PthreadLockChecker.cpp and test/Analysis/pthreadlock.c. Also, when you asked me to revert the changes, did you mean revert the changes made by clang-format? If yes, how do I do that? I apologize for asking such silly questions. The thing is I'm new to all this and I don't really know how to proceed further. > > > - Updating .gitignore sounds like the right thing to do (llvm's .gitignore > already has this), but i guess we'd better make a separate commit for that. Repository: rL LLVM https://reviews.llvm.org/D32449 ___ cfe-commits mailing list cfe-commits@lists.llvm.org http://lists.llvm.org/cgi-bin/mailman/listinfo/cfe-commits
[PATCH] D32449: Modifying PthreadLockChecker.cpp to reduce false positives.
NoQ added a comment. Thanks, this is great! Two more things: - You have touched other code, unrelated to your patch, with clang-format; we're usually trying to avoid that, because it creates merge conflicts out of nowhere, and because some of that code actually seems formatted by hand intentionally. It's better to revert these changes; you can use the `git clang-format` thing to format only actual changes. - Updating .gitignore sounds like the right thing to do (llvm's .gitignore already has this), but i guess we'd better make a separate commit for that. Comment at: lib/StaticAnalyzer/Checkers/PthreadLockChecker.cpp:143-146 +if(lstate->isSchrodingerUntouched()) + state = state->remove(lockR); +else if(lstate->isSchrodingerUnlocked()) + state = state->set(lockR, LockState::getUnlocked()); malhar1995 wrote: > NoQ wrote: > > I think we can be certain that the lock is in one of these states, and > > assert that. > We can be certain that the lock state will be either of the two only if I add > the following statement before returning from this function. > ``` > state = state->remove(lockR); > ``` > If I don't add the above statement, a return value symbol for the region > specified by lockR will still be in DestroyRetVal and it may have an actual > lock state (locked, unlocked or destroyed). Yep, that's a great thing to do. I didn't notice this. Generally, it's great to keep the program state free from stuff that would no longer be necessary. Repository: rL LLVM https://reviews.llvm.org/D32449 ___ cfe-commits mailing list cfe-commits@lists.llvm.org http://lists.llvm.org/cgi-bin/mailman/listinfo/cfe-commits
[PATCH] D32449: Modifying PthreadLockChecker.cpp to reduce false positives.
malhar1995 updated this revision to Diff 99750.
malhar1995 added a comment.
Addressed previous comments (removed Schrodinger from lock state names, changed
method name setAppropriateLockState to resolvePossiblyDestroyedMutex, added an
assert in resolvePossiblyDestroyedMutex, formatted the code using clang-format
and added some test-cases to test/Analysis/pthreadlock.c)
Repository:
rL LLVM
https://reviews.llvm.org/D32449
Files:
.gitignore
lib/StaticAnalyzer/Checkers/PthreadLockChecker.cpp
test/Analysis/pthreadlock.c
Index: test/Analysis/pthreadlock.c
===
--- test/Analysis/pthreadlock.c
+++ test/Analysis/pthreadlock.c
@@ -176,6 +176,49 @@
pthread_mutex_unlock(pmtx); // no-warning
}
+void
+ok23(void) {
+ if(pthread_mutex_destroy(&mtx1) != 0) // no-warning
+ pthread_mutex_destroy(&mtx1); // no-warning
+}
+
+void
+ok24(void) {
+ if(pthread_mutex_destroy(&mtx1) != 0) // no-warning
+ pthread_mutex_lock(&mtx1); // no-warning
+}
+
+void
+ok25(void) {
+ if(pthread_mutex_destroy(&mtx1) != 0) // no-warning
+ pthread_mutex_unlock(&mtx1); // no-warning
+}
+
+void
+ok26(void) {
+ pthread_mutex_unlock(&mtx1); // no-warning
+ if(pthread_mutex_destroy(&mtx1) != 0) // no-warning
+ pthread_mutex_lock(&mtx1); // no-warning
+}
+
+void
+ok27(void) {
+ pthread_mutex_unlock(&mtx1); // no-warning
+ if(pthread_mutex_destroy(&mtx1) != 0) // no-warning
+ pthread_mutex_lock(&mtx1); // no-warning
+ else
+ pthread_mutex_init(&mtx1, NULL); // no-warning
+}
+
+void
+ok28() {
+ if(pthread_mutex_destroy(&mtx1)!=0) { // no-warning
+ pthread_mutex_lock(&mtx1); // no-warning
+ pthread_mutex_unlock(&mtx1); // no-warning
+ pthread_mutex_destroy(&mtx1); // no-warning
+ }
+}
+
void
bad1(void)
@@ -392,3 +435,56 @@
pthread_mutex_unlock(&mtx1); // no-warning
pthread_mutex_init(&mtx1, NULL); // expected-warning{{This lock has already been initialized}}
}
+
+void
+bad27(void)
+{
+ pthread_mutex_unlock(&mtx1); // no-warning
+ int ret = pthread_mutex_destroy(&mtx1); // no-warning
+ if(ret != 0) // no-warning
+ pthread_mutex_lock(&mtx1); // no-warning
+ else
+ pthread_mutex_unlock(&mtx1); // expected-warning{{This lock has already been destroyed}}
+}
+
+void
+bad28(void)
+{
+ pthread_mutex_unlock(&mtx1); // no-warning
+ int ret = pthread_mutex_destroy(&mtx1); // no-warning
+ if(ret != 0) // no-warning
+ pthread_mutex_lock(&mtx1); // no-warning
+ else
+ pthread_mutex_lock(&mtx1); // expected-warning{{This lock has already been destroyed}}
+}
+
+void
+bad29()
+{
+ pthread_mutex_lock(&mtx1); // no-warning
+ pthread_mutex_unlock(&mtx1); // no-warning
+ if(pthread_mutex_destroy(&mtx1) != 0) // no-warning
+ pthread_mutex_init(&mtx1, NULL); // expected-warning{{This lock has already been initialized}}
+ else
+ pthread_mutex_init(&mtx1, NULL); // no-warning
+}
+
+void
+bad30()
+{
+ pthread_mutex_lock(&mtx1); // no-warning
+ pthread_mutex_unlock(&mtx1); // no-warning
+ if(pthread_mutex_destroy(&mtx1) != 0) // no-warning
+ pthread_mutex_init(&mtx1, NULL); // expected-warning{{This lock has already been initialized}}
+ else
+ pthread_mutex_destroy(&mtx1); // expected-warning{{This lock has already been destroyed}}
+}
+
+void
+bad31()
+{
+ int ret = pthread_mutex_destroy(&mtx1); // no-warning
+ pthread_mutex_lock(&mtx1); // expected-warning{{This lock has already been destroyed}}
+ if(ret != 0)
+ pthread_mutex_lock(&mtx1);
+}
Index: lib/StaticAnalyzer/Checkers/PthreadLockChecker.cpp
===
--- lib/StaticAnalyzer/Checkers/PthreadLockChecker.cpp
+++ lib/StaticAnalyzer/Checkers/PthreadLockChecker.cpp
@@ -25,58 +25,79 @@
namespace {
struct LockState {
- enum Kind { Destroyed, Locked, Unlocked } K;
+ enum Kind {
+Destroyed,
+Locked,
+Unlocked,
+UntouchedAndPossiblyDestroyed,
+UnlockedAndPossiblyDestroyed
+ } K;
private:
LockState(Kind K) : K(K) {}
public:
static LockState getLocked() { return LockState(Locked); }
static LockState getUnlocked() { return LockState(Unlocked); }
static LockState getDestroyed() { return LockState(Destroyed); }
-
- bool operator==(const LockState &X) const {
-return K == X.K;
+ static LockState getUntouchedAndPossiblyDestroyed() {
+return LockState(UntouchedAndPossiblyDestroyed);
+ }
+ static LockState getUnlockedAndPossiblyDestroyed() {
+return LockState(UnlockedAndPossiblyDestroyed);
}
+ bool operator==(const LockState &X) const { return K == X.K; }
+
bool isLocked() const { return K == Locked; }
bool isUnlocked() const { return K == Unlocked; }
bool isDestroyed() const { return K == Destroyed; }
-
- void Profile(llvm::FoldingSetNodeID &ID) const {
-ID.AddInteger(K);
+ bool isUntouchedAndPossiblyDestroyed() const {
+return K == UntouchedAndPossiblyDestroyed;
}
+ bool isUnlockedAndPossiblyDestroyed() const {
+return K == UnlockedAndPossiblyDestroyed;
+ }
+
+ void Profile(llvm
[PATCH] D32449: Modifying PthreadLockChecker.cpp to reduce false positives.
malhar1995 added inline comments. Comment at: lib/StaticAnalyzer/Checkers/PthreadLockChecker.cpp:143-146 +if(lstate->isSchrodingerUntouched()) + state = state->remove(lockR); +else if(lstate->isSchrodingerUnlocked()) + state = state->set(lockR, LockState::getUnlocked()); NoQ wrote: > I think we can be certain that the lock is in one of these states, and assert > that. We can be certain that the lock state will be either of the two only if I add the following statement before returning from this function. ``` state = state->remove(lockR); ``` If I don't add the above statement, a return value symbol for the region specified by lockR will still be in DestroyRetVal and it may have an actual lock state (locked, unlocked or destroyed). Repository: rL LLVM https://reviews.llvm.org/D32449 ___ cfe-commits mailing list cfe-commits@lists.llvm.org http://lists.llvm.org/cgi-bin/mailman/listinfo/cfe-commits
[PATCH] D32449: Modifying PthreadLockChecker.cpp to reduce false positives.
malhar1995 marked 2 inline comments as done. malhar1995 added a comment. In https://reviews.llvm.org/D32449#760141, @NoQ wrote: > Thanks! Your code looks very clear now, and it seems correct to me. > > One last thing we definitely should do here would be add regression tests for > the new functionality. I guess you already have your tests, otherwise you > wouldn't know if your code works, so you'd just need to append them to the > patch, somewhere at the bottom of `test/Analysis/pthreadlock.c`, and make > sure that `make -j4 check-clang-analysis` passes. Ideally, we should cover as > many branches as possible. > > A few ideas of what to test (you might have thought about most of them > already, and i expect them to actually work by just looking at what your code > accomplishes): > > - What we can/cannot do with the mutex in the failed-to-be-destroyed state, > depending on the state of the mutex before destruction was attempted. > - What we can/cannot do with the mutex in each of the "Schrodinger" states - > in particular, do we display the double-destroy warning in such cases? > - How return-symbol death races against resolving success of the destroy > operation: what if the programmer first tries to destroy mutex, then uses the > mutex, then checks the return value? > - Are you sure we cannot `assert(lstate)` on line 137? - a test could be > added that would cause such assertion to fail if someone tries to impose it. > > Apart from that, i guess it'd be good to use more informative variable > names in a few places (see inline comments), and fix the formatting, i.e. > spaces and line breaks (should be easy with `clang-format`). Also you > shouldn't add the `.DS_Store` files :) And then we'd accept and commit this > patch. Dear Dr. Artem, Thank you so much for such a detailed review. I'll work on addressing these comments ASAP and reach out to you in case I have any queries. Regards, Malhar Thakkar Repository: rL LLVM https://reviews.llvm.org/D32449 ___ cfe-commits mailing list cfe-commits@lists.llvm.org http://lists.llvm.org/cgi-bin/mailman/listinfo/cfe-commits
[PATCH] D32449: Modifying PthreadLockChecker.cpp to reduce false positives.
NoQ added a comment.
Thanks! Your code looks very clear now, and it seems correct to me.
One last thing we definitely should do here would be add regression tests for
the new functionality. I guess you already have your tests, otherwise you
wouldn't know if your code works, so you'd just need to append them to the
patch, somewhere at the bottom of `test/Analysis/pthreadlock.c`, and make sure
that `make -j4 check-clang-analysis` passes. Ideally, we should cover as many
branches as possible.
A few ideas of what to test (you might have thought about most of them already,
and i expect them to actually work by just looking at what your code
accomplishes):
- What we can/cannot do with the mutex in the failed-to-be-destroyed state,
depending on the state of the mutex before destruction was attempted.
- What we can/cannot do with the mutex in each of the "Schrodinger" states - in
particular, do we display the double-destroy warning in such cases?
- How return-symbol death races against resolving success of the destroy
operation: what if the programmer first tries to destroy mutex, then uses the
mutex, then checks the return value?
- Are you sure we cannot `assert(lstate)` on line 137? - a test could be added
that would cause such assertion to fail if someone tries to impose it.
Apart from that, i guess it'd be good to use more informative variable names in
a few places (see inline comments), and fix the formatting, i.e. spaces and
line breaks (should be easy with `clang-format`). Also you shouldn't add the
`.DS_Store` files :) And then we'd accept and commit this patch.
Comment at: lib/StaticAnalyzer/Checkers/PthreadLockChecker.cpp:28
struct LockState {
- enum Kind { Destroyed, Locked, Unlocked } K;
+ enum Kind { Destroyed, Locked, Unlocked, SchrodingerUntouched,
SchrodingerUnlocked } K;
I still think these names, no matter if a good metaphor or not and no matter
how much i enjoyed them, should be toned down :) Suggesting
`UntouchedAndPossiblyDestroyed` and `UnlockedAndPossiblyDestroyed`.
Comment at: lib/StaticAnalyzer/Checkers/PthreadLockChecker.cpp:77
void reportUseDestroyedBug(CheckerContext &C, const CallExpr *CE) const;
+ ProgramStateRef setAppropriateLockState(ProgramStateRef state, const
MemRegion* lockR, const SymbolRef* sym, bool fromCheckDeadSymbols) const;
};
I suggest renaming to something like "`resolvePossiblyDestroyedMutex()`".
Also, i'm for passing the symbol by value (with `*` dereference at most call
sites) because it's less surprising/confusing to the reader.
I also suggest a comment explaining what the function does. Eg., "When a lock
is destroyed, in some semantics we are not sure if the destroy call has
succeeded or failed, and the lock enters one of the 'possibly destroyed' state.
There is a short time frame for the programmer to check the return value to see
if the lock was successfully destroyed. Before we model the next operation over
that lock, we call this function to see if the return value was checked by now
and set the lock state - either to destroyed state or back to its previous
state."
Comment at: lib/StaticAnalyzer/Checkers/PthreadLockChecker.cpp:81-85
// GDM Entry for tracking lock state.
REGISTER_LIST_WITH_PROGRAMSTATE(LockSet, const MemRegion *)
REGISTER_MAP_WITH_PROGRAMSTATE(LockMap, const MemRegion *, LockState)
+REGISTER_MAP_WITH_PROGRAMSTATE(DestroyRetVal, const MemRegion *, SymbolRef)
Because there's only one comment per three traits, it'd be great to clean this
up a bit together with commenting up your new trait:
```
// A stack of locks for tracking lock-unlock order.
REGISTER_LIST_WITH_PROGRAMSTATE(LockSet, const MemRegion *)
// An entry for tracking lock states.
REGISTER_MAP_WITH_PROGRAMSTATE(LockMap, const MemRegion *, LockState)
// Return values for unresolved destroy calls.
REGISTER_MAP_WITH_PROGRAMSTATE(DestroyRetVal, const MemRegion *, SymbolRef)
```
Comment at: lib/StaticAnalyzer/Checkers/PthreadLockChecker.cpp:143-146
+if(lstate->isSchrodingerUntouched())
+ state = state->remove(lockR);
+else if(lstate->isSchrodingerUnlocked())
+ state = state->set(lockR, LockState::getUnlocked());
I think we can be certain that the lock is in one of these states, and assert
that.
Comment at: lib/StaticAnalyzer/Checkers/PthreadLockChecker.cpp:149-151
+if(lstate->isSchrodingerUntouched() || lstate->isSchrodingerUnlocked()){
+ state = state->set(lockR, LockState::getDestroyed());
+}
Assert the lock state here as well?
Comment at: lib/StaticAnalyzer/Checkers/PthreadLockChecker.cpp:302-308
+ SVal X = State->getSVal(CE, C.getLocationContext());
+ if (X.isUnknownOrUndef()){
+return;
+ }
+
+ DefinedSVal retVal = X.castAs();
+ SymbolRef sym = retVal.getAsSymbol();
--
[PATCH] D32449: Modifying PthreadLockChecker.cpp to reduce false positives.
malhar1995 updated this revision to Diff 99388.
malhar1995 marked an inline comment as done.
malhar1995 added a comment.
Cleaned up the previous patch.
Added checking of LockState before initializing a mutex as well.
Added separate branches of execution for PthreadSemantics and XNUSemantics.
Added assert in case of checkDeadSymbols as existence in DestroyRetVal ensures
existence in LockMap.
Repository:
rL LLVM
https://reviews.llvm.org/D32449
Files:
.DS_Store
lib/.DS_Store
lib/StaticAnalyzer/.DS_Store
lib/StaticAnalyzer/Checkers/.DS_Store
lib/StaticAnalyzer/Checkers/PthreadLockChecker.cpp
test/.DS_Store
test/Analysis/.DS_Store
Index: lib/StaticAnalyzer/Checkers/PthreadLockChecker.cpp
===
--- lib/StaticAnalyzer/Checkers/PthreadLockChecker.cpp
+++ lib/StaticAnalyzer/Checkers/PthreadLockChecker.cpp
@@ -25,30 +25,34 @@
namespace {
struct LockState {
- enum Kind { Destroyed, Locked, Unlocked } K;
+ enum Kind { Destroyed, Locked, Unlocked, SchrodingerUntouched, SchrodingerUnlocked } K;
private:
LockState(Kind K) : K(K) {}
public:
static LockState getLocked() { return LockState(Locked); }
static LockState getUnlocked() { return LockState(Unlocked); }
static LockState getDestroyed() { return LockState(Destroyed); }
+ static LockState getSchrodingerUntouched() { return LockState(SchrodingerUntouched); }
+ static LockState getSchrodingerUnlocked() { return LockState(SchrodingerUnlocked); }
bool operator==(const LockState &X) const {
return K == X.K;
}
bool isLocked() const { return K == Locked; }
bool isUnlocked() const { return K == Unlocked; }
bool isDestroyed() const { return K == Destroyed; }
+ bool isSchrodingerUntouched() const { return K == SchrodingerUntouched; }
+ bool isSchrodingerUnlocked() const { return K == SchrodingerUnlocked; }
void Profile(llvm::FoldingSetNodeID &ID) const {
ID.AddInteger(K);
}
};
-class PthreadLockChecker : public Checker< check::PostStmt > {
+class PthreadLockChecker : public Checker< check::PostStmt, check::DeadSymbols > {
mutable std::unique_ptr BT_doublelock;
mutable std::unique_ptr BT_doubleunlock;
mutable std::unique_ptr BT_destroylock;
@@ -61,21 +65,24 @@
};
public:
void checkPostStmt(const CallExpr *CE, CheckerContext &C) const;
+ void checkDeadSymbols(SymbolReaper &SymReaper, CheckerContext &C) const;
void AcquireLock(CheckerContext &C, const CallExpr *CE, SVal lock,
bool isTryLock, enum LockingSemantics semantics) const;
void ReleaseLock(CheckerContext &C, const CallExpr *CE, SVal lock) const;
- void DestroyLock(CheckerContext &C, const CallExpr *CE, SVal Lock) const;
+ void DestroyLock(CheckerContext &C, const CallExpr *CE, SVal Lock, enum LockingSemantics semantics) const;
void InitLock(CheckerContext &C, const CallExpr *CE, SVal Lock) const;
void reportUseDestroyedBug(CheckerContext &C, const CallExpr *CE) const;
+ ProgramStateRef setAppropriateLockState(ProgramStateRef state, const MemRegion* lockR, const SymbolRef* sym, bool fromCheckDeadSymbols) const;
};
} // end anonymous namespace
// GDM Entry for tracking lock state.
REGISTER_LIST_WITH_PROGRAMSTATE(LockSet, const MemRegion *)
REGISTER_MAP_WITH_PROGRAMSTATE(LockMap, const MemRegion *, LockState)
+REGISTER_MAP_WITH_PROGRAMSTATE(DestroyRetVal, const MemRegion *, SymbolRef)
void PthreadLockChecker::checkPostStmt(const CallExpr *CE,
CheckerContext &C) const {
@@ -113,22 +120,50 @@
FName == "lck_mtx_unlock" ||
FName == "lck_rw_done")
ReleaseLock(C, CE, state->getSVal(CE->getArg(0), LCtx));
- else if (FName == "pthread_mutex_destroy" ||
- FName == "lck_mtx_destroy")
-DestroyLock(C, CE, state->getSVal(CE->getArg(0), LCtx));
+ else if (FName == "pthread_mutex_destroy")
+DestroyLock(C, CE, state->getSVal(CE->getArg(0), LCtx), PthreadSemantics);
+ else if (FName == "lck_mtx_destroy")
+DestroyLock(C, CE, state->getSVal(CE->getArg(0), LCtx), XNUSemantics);
else if (FName == "pthread_mutex_init")
InitLock(C, CE, state->getSVal(CE->getArg(0), LCtx));
}
+ProgramStateRef PthreadLockChecker::setAppropriateLockState(ProgramStateRef state, const MemRegion* lockR, const SymbolRef* sym, bool fromCheckDeadSymbols) const {
+ const LockState* lstate = state->get(lockR);
+ // Existence in DestroyRetVal ensures existence in LockMap.
+ if(fromCheckDeadSymbols)
+assert(lstate);
+ else{
+if(!lstate)
+ return state;
+ }
+ ConstraintManager &CMgr = state->getConstraintManager();
+ ConditionTruthVal retZero = CMgr.isNull(state, *sym);
+ if(retZero.isConstrainedFalse()){
+if(lstate->isSchrodingerUntouched())
+ state = state->remove(lockR);
+else if(lstate->isSchrodingerUnlocked())
+ state = state->set(lockR, LockState::getUnlocked());
+ }
+ else{
+if(lstate->isSchrodingerUntouch
[PATCH] D32449: Modifying PthreadLockChecker.cpp to reduce false positives.
malhar1995 updated this revision to Diff 99179.
malhar1995 added a comment.
Added context.
Also, I removed the inclusion of iostream and also added the repetitive code to
the function setAppropriateLockState.
Currently working on finding various corner cases and invariants.
Repository:
rL LLVM
https://reviews.llvm.org/D32449
Files:
.DS_Store
lib/.DS_Store
lib/StaticAnalyzer/.DS_Store
lib/StaticAnalyzer/Checkers/.DS_Store
lib/StaticAnalyzer/Checkers/PthreadLockChecker.cpp
Index: lib/StaticAnalyzer/Checkers/PthreadLockChecker.cpp
===
--- lib/StaticAnalyzer/Checkers/PthreadLockChecker.cpp
+++ lib/StaticAnalyzer/Checkers/PthreadLockChecker.cpp
@@ -25,30 +25,34 @@
namespace {
struct LockState {
- enum Kind { Destroyed, Locked, Unlocked } K;
+ enum Kind { Destroyed, Locked, Unlocked, SchrodingerLocked, SchrodingerUnlocked } K;
private:
LockState(Kind K) : K(K) {}
public:
static LockState getLocked() { return LockState(Locked); }
static LockState getUnlocked() { return LockState(Unlocked); }
static LockState getDestroyed() { return LockState(Destroyed); }
+ static LockState getSchrodingerLocked() { return LockState(SchrodingerLocked); }
+ static LockState getSchrodingerUnlocked() { return LockState(SchrodingerUnlocked); }
bool operator==(const LockState &X) const {
return K == X.K;
}
bool isLocked() const { return K == Locked; }
bool isUnlocked() const { return K == Unlocked; }
bool isDestroyed() const { return K == Destroyed; }
+ bool isSchrodingerLocked() const { return K == SchrodingerLocked; }
+ bool isSchrodingerUnlocked() const { return K == SchrodingerUnlocked; }
void Profile(llvm::FoldingSetNodeID &ID) const {
ID.AddInteger(K);
}
};
-class PthreadLockChecker : public Checker< check::PostStmt > {
+class PthreadLockChecker : public Checker< check::PostStmt, check::DeadSymbols > {
mutable std::unique_ptr BT_doublelock;
mutable std::unique_ptr BT_doubleunlock;
mutable std::unique_ptr BT_destroylock;
@@ -61,21 +65,24 @@
};
public:
void checkPostStmt(const CallExpr *CE, CheckerContext &C) const;
+ void checkDeadSymbols(SymbolReaper &SymReaper, CheckerContext &C) const;
void AcquireLock(CheckerContext &C, const CallExpr *CE, SVal lock,
bool isTryLock, enum LockingSemantics semantics) const;
void ReleaseLock(CheckerContext &C, const CallExpr *CE, SVal lock) const;
void DestroyLock(CheckerContext &C, const CallExpr *CE, SVal Lock) const;
void InitLock(CheckerContext &C, const CallExpr *CE, SVal Lock) const;
void reportUseDestroyedBug(CheckerContext &C, const CallExpr *CE) const;
+ ProgramStateRef setAppropriateLockState(ProgramStateRef state, const MemRegion* lockR) const;
};
} // end anonymous namespace
// GDM Entry for tracking lock state.
REGISTER_LIST_WITH_PROGRAMSTATE(LockSet, const MemRegion *)
REGISTER_MAP_WITH_PROGRAMSTATE(LockMap, const MemRegion *, LockState)
+REGISTER_MAP_WITH_PROGRAMSTATE(DestroyRetVal, const MemRegion *, SymbolRef)
void PthreadLockChecker::checkPostStmt(const CallExpr *CE,
CheckerContext &C) const {
@@ -120,16 +127,40 @@
InitLock(C, CE, state->getSVal(CE->getArg(0), LCtx));
}
+ProgramStateRef PthreadLockChecker::setAppropriateLockState(ProgramStateRef state, const MemRegion* lockR) const {
+ const SymbolRef* sym = state->get(lockR);
+ if(sym){
+const LockState* lstate = state->get(lockR);
+if(lstate){
+ ConstraintManager &CMgr = state->getConstraintManager();
+ ConditionTruthVal retZero = CMgr.isNull(state, *sym);
+ if(retZero.isConstrainedFalse()){
+if(lstate->isSchrodingerLocked())
+ state = state->set(lockR, LockState::getLocked());
+else if(lstate->isSchrodingerUnlocked())
+ state = state->set(lockR, LockState::getUnlocked());
+ }
+ else{
+if(!lstate || lstate->isSchrodingerLocked() || lstate->isSchrodingerUnlocked())
+ state = state->set(lockR, LockState::getDestroyed());
+ }
+}
+ }
+ return state;
+}
+
void PthreadLockChecker::AcquireLock(CheckerContext &C, const CallExpr *CE,
SVal lock, bool isTryLock,
enum LockingSemantics semantics) const {
const MemRegion *lockR = lock.getAsRegion();
if (!lockR)
-return;
+return;
ProgramStateRef state = C.getState();
+ state = setAppropriateLockState(state, lockR);
+
SVal X = state->getSVal(CE, C.getLocationContext());
if (X.isUnknownOrUndef())
return;
@@ -198,6 +229,8 @@
ProgramStateRef state = C.getState();
+ state = setAppropriateLockState(state, lockR);
+
if (const LockState *LState = state->get(lockR)) {
if (LState->isUnlocked()) {
if (!BT_doubleunlock)
@@ -253,9 +286,32 @@
ProgramStateRef State = C.getState();
+ State = setAppropriateL
[PATCH] D32449: Modifying PthreadLockChecker.cpp to reduce false positives.
zaks.anna added a comment. Thank you for the patch! Could you please re-submit the patch with context? Instructions on how to do that can be found here: http://llvm.org/docs/Phabricator.html Repository: rL LLVM https://reviews.llvm.org/D32449 ___ cfe-commits mailing list cfe-commits@lists.llvm.org http://lists.llvm.org/cgi-bin/mailman/listinfo/cfe-commits
[PATCH] D32449: Modifying PthreadLockChecker.cpp to reduce false positives.
NoQ added a comment.
Thanks for uploading this to phabricator and sorry again that i was lost for a
while.
As we already discussed in the mailing lists, i agree with your point that the
locked-and-possibly-destroyed state should be removed, and we also had a
thought of making it explicit that the patch only applies to posix thread
semantics, not to XNU semantics - in other words, there should appear different
branches of code depending on the lock's semantics.
Could you also upload the patch file with the "context" (eg. `git diff
-U99` would include +/- 99 unchanged lines around the changes in the
patch file, and phabricator would use them fancily to make reviewing easier;
otherwise i don't immediately see which callback you are changing in a
particular spot).
Once the patch would reach completion, it'd need to be cleaned up for
formatting/whitespace; we usually run `clang-format` over our changes with
default settings and it does everything for us.
Comment at: lib/StaticAnalyzer/Checkers/PthreadLockChecker.cpp:21
#include "clang/StaticAnalyzer/Core/PathSensitive/ProgramStateTrait.h"
+#include
You don't need to include `getConstraintManager();
+ ConditionTruthVal retZero = CMgr.isNull(state, *sym);
+ if(retZero.isConstrainedFalse()){
+if(lstate->isSchrodingerLocked())
+ state = state->set(lockR, LockState::getLocked());
+else if(lstate->isSchrodingerUnlocked())
+ state = state->set(lockR, LockState::getUnlocked());
This code gets duplicated multiple times - including the `checkDeadSymbols`
callback as well; can we refactor it into a function?
Comment at: lib/StaticAnalyzer/Checkers/PthreadLockChecker.cpp:154
+ else{
+if(!lstate || lstate->isSchrodingerLocked() ||
lstate->isSchrodingerUnlocked())
+ state = state->set(lockR, LockState::getDestroyed());
I'd like you to consider various corner cases. Note that because we have the
`REGISTER_MAP_WITH_PROGRAMSTATE` privately in this file, only code in this file
can affect the contents of that program state trait. So we have complete
knowledge of what can and cannot be in the program state.
For example, can it be that there's a symbol in the `DestroyRetVal` map, but
`lstate` is not present for the same mutex region in the `LockMap`? Or does the
code ensure that the former implies the latter? If we are sure that some
invariants hold, then we should remove the respective `if ()` and ideally
replace it with an `assert()`.
If you find invariants that always hold, it would be great to write these down
in the comments inside the code.
Repository:
rL LLVM
https://reviews.llvm.org/D32449
___
cfe-commits mailing list
cfe-commits@lists.llvm.org
http://lists.llvm.org/cgi-bin/mailman/listinfo/cfe-commits
[PATCH] D32449: Modifying PthreadLockChecker.cpp to reduce false positives.
NoQ edited reviewers, added: NoQ; removed: dergachev.a. NoQ added a comment. Uhm, i need to do something about this duplicate account. Sorry, I have completely forgotten that the review is already up... Repository: rL LLVM https://reviews.llvm.org/D32449 ___ cfe-commits mailing list cfe-commits@lists.llvm.org http://lists.llvm.org/cgi-bin/mailman/listinfo/cfe-commits
[PATCH] D32449: Modifying PthreadLockChecker.cpp to reduce false positives.
malhar1995 created this revision.
I am currently working on to avoid false positives which currently occur as the
return values of mutex functions like pthread_mutex_destroy() are not taken
into consideration.
The precise description of the bug can be found here:
https://bugs.llvm.org/show_bug.cgi?id=32455
Dr. Devin and Dr. Artem have been guiding me to fix PthreadLockChecker to avoid
such false positives. The patch I'm attaching is not 100% correct and hence I
need your advice to proceed further.
Thank you.
Repository:
rL LLVM
https://reviews.llvm.org/D32449
Files:
lib/.DS_Store
lib/StaticAnalyzer/.DS_Store
lib/StaticAnalyzer/Checkers/PthreadLockChecker.cpp
Index: lib/StaticAnalyzer/Checkers/PthreadLockChecker.cpp
===
--- lib/StaticAnalyzer/Checkers/PthreadLockChecker.cpp
+++ lib/StaticAnalyzer/Checkers/PthreadLockChecker.cpp
@@ -18,6 +18,7 @@
#include "clang/StaticAnalyzer/Core/CheckerManager.h"
#include "clang/StaticAnalyzer/Core/PathSensitive/CheckerContext.h"
#include "clang/StaticAnalyzer/Core/PathSensitive/ProgramStateTrait.h"
+#include
using namespace clang;
using namespace ento;
@@ -25,7 +26,7 @@
namespace {
struct LockState {
- enum Kind { Destroyed, Locked, Unlocked } K;
+ enum Kind { Destroyed, Locked, Unlocked, SchrodingerLocked, SchrodingerUnlocked } K;
private:
LockState(Kind K) : K(K) {}
@@ -34,6 +35,8 @@
static LockState getLocked() { return LockState(Locked); }
static LockState getUnlocked() { return LockState(Unlocked); }
static LockState getDestroyed() { return LockState(Destroyed); }
+ static LockState getSchrodingerLocked() { return LockState(SchrodingerLocked); }
+ static LockState getSchrodingerUnlocked() { return LockState(SchrodingerUnlocked); }
bool operator==(const LockState &X) const {
return K == X.K;
@@ -42,13 +45,15 @@
bool isLocked() const { return K == Locked; }
bool isUnlocked() const { return K == Unlocked; }
bool isDestroyed() const { return K == Destroyed; }
+ bool isSchrodingerLocked() const { return K == SchrodingerLocked; }
+ bool isSchrodingerUnlocked() const { return K == SchrodingerUnlocked; }
void Profile(llvm::FoldingSetNodeID &ID) const {
ID.AddInteger(K);
}
};
-class PthreadLockChecker : public Checker< check::PostStmt > {
+class PthreadLockChecker : public Checker< check::PostStmt, check::DeadSymbols > {
mutable std::unique_ptr BT_doublelock;
mutable std::unique_ptr BT_doubleunlock;
mutable std::unique_ptr BT_destroylock;
@@ -61,6 +66,7 @@
};
public:
void checkPostStmt(const CallExpr *CE, CheckerContext &C) const;
+ void checkDeadSymbols(SymbolReaper &SymReaper, CheckerContext &C) const;
void AcquireLock(CheckerContext &C, const CallExpr *CE, SVal lock,
bool isTryLock, enum LockingSemantics semantics) const;
@@ -76,6 +82,7 @@
REGISTER_LIST_WITH_PROGRAMSTATE(LockSet, const MemRegion *)
REGISTER_MAP_WITH_PROGRAMSTATE(LockMap, const MemRegion *, LockState)
+REGISTER_MAP_WITH_PROGRAMSTATE(DestroyRetVal, const MemRegion *, SymbolRef)
void PthreadLockChecker::checkPostStmt(const CallExpr *CE,
CheckerContext &C) const {
@@ -126,10 +133,30 @@
const MemRegion *lockR = lock.getAsRegion();
if (!lockR)
-return;
+return;
ProgramStateRef state = C.getState();
+ // CHECK THIS
+ const SymbolRef* sym = state->get(lockR);
+ if(sym){
+const LockState* lstate = state->get(lockR);
+if(lstate){
+ ConstraintManager &CMgr = state->getConstraintManager();
+ ConditionTruthVal retZero = CMgr.isNull(state, *sym);
+ if(retZero.isConstrainedFalse()){
+if(lstate->isSchrodingerLocked())
+ state = state->set(lockR, LockState::getLocked());
+else if(lstate->isSchrodingerUnlocked())
+ state = state->set(lockR, LockState::getUnlocked());
+ }
+ else{
+if(!lstate || lstate->isSchrodingerLocked() || lstate->isSchrodingerUnlocked())
+ state = state->set(lockR, LockState::getDestroyed());
+ }
+}
+ }
+
SVal X = state->getSVal(CE, C.getLocationContext());
if (X.isUnknownOrUndef())
return;
@@ -198,6 +225,26 @@
ProgramStateRef state = C.getState();
+ // CHECK THIS
+ const SymbolRef* sym = state->get(lockR);
+ if(sym){
+const LockState* lstate = state->get(lockR);
+if(lstate){
+ ConstraintManager &CMgr = state->getConstraintManager();
+ ConditionTruthVal retZero = CMgr.isNull(state, *sym);
+ if(retZero.isConstrainedFalse()){
+if(lstate->isSchrodingerLocked())
+ state = state->set(lockR, LockState::getLocked());
+else if(lstate->isSchrodingerUnlocked())
+ state = state->set(lockR, LockState::getUnlocked());
+ }
+ else{
+if(!lstate || lstate->isSchrodingerLocked() || lstate->isSchrodingerUnlocked())
+ state = state->set(lockR, LockState::getDest
