Skip to content
Browse files

sl/symheap: redesign the abstract prover from scratch

  • Loading branch information...
1 parent 3a45831 commit 934a26af3b59194683363b017eb63d4df6cb5d23 @kdudka committed May 12, 2012
View
170 sl/symheap.cc
@@ -3021,6 +3021,10 @@ void SymHeapCore::valDestroyTarget(TValId val) {
TSizeRange SymHeapCore::valSizeOfTarget(TValId val) const {
const BaseValue *valData;
d->ents.getEntRO(&valData, val);
+ if (!isPossibleToDeref(valData->code))
+ // no writable target around here
+ return IR::rngFromNum(IR::Int0);
+
if (valData->offRoot < 0)
// we are above the root, so we cannot safely write anything
return IR::rngFromNum(IR::Int0);
@@ -3588,8 +3592,48 @@ void SymHeap::neqOp(ENeqOp op, TValId v1, TValId v2) {
CL_DEBUG("SymHeap::neqOp() refuses to add an extraordinary Neq predicate");
}
+TValId lookThrough(TValSet *pSeen, SymHeap &sh, TValId val) {
+ if (VT_RANGE == sh.valTarget(val))
+ // not supported yet
+ return VAL_INVALID;
+
+ const TOffset off = sh.valOffset(val);
+
+ while (0 < val) {
+ const TValId root = sh.valRoot(val);
+ if (!insertOnce(*pSeen, root))
+ // an already seen root value
+ return VAL_INVALID;
+
+ const EValueTarget code = sh.valTarget(val);
+ if (!isAbstract(code))
+ // a non-abstract object reached
+ break;
+
+ const TValId seg = segPeer(sh, root);
+ if (sh.segMinLength(seg))
+ // non-empty abstract object reached
+ break;
+
+ const EObjKind kind = sh.valTargetKind(seg);
+ if (OK_OBJ_OR_NULL == kind) {
+ // we always end up with VAL_NULL if OK_OBJ_OR_NULL is removed
+ val = VAL_NULL;
+ continue;
+ }
+
+ // jump to next value while taking the 'head' offset into consideration
+ const TValId valNext = nextValFromSeg(sh, seg);
+ const BindingOff &bOff = sh.segBinding(seg);
+ val = sh.valByOffset(valNext, off - bOff.head);
+ }
+
+ return val;
+}
+
bool SymHeap::proveNeq(TValId ref, TValId val) const {
if (SymHeapCore::proveNeq(ref, val))
+ // values are non-equal in non-abstract world
return true;
// having the values always in the same order leads to simpler code
@@ -3599,102 +3643,62 @@ bool SymHeap::proveNeq(TValId ref, TValId val) const {
// we are interested only in abstract objects here, nothing to do...
return false;
- if (isAbstract(this->valTarget(ref))) {
- // both values are abstract
- const TValId root1 = this->valRoot(ref);
- const TValId root2 = this->valRoot(val);
- if (root2 == segPeer(*this, root1)) {
- // one value points at segment and the other points at its peer
- const TOffset off1 = this->valOffset(ref);
- const TOffset off2 = this->valOffset(val);
- return (off1 == off2)
- && (1 < this->segMinLength(root1));
- }
-
- const TMinLen len1 = objMinLength(*this, root1);
- const TMinLen len2 = objMinLength(*this, root2);
- if (!len1 && !len2)
- // both targets are possibly empty, giving up
- return false;
+ TValSet seen;
- if (len1 < len2)
- // move the non-empty segment to left (FIXME: still imprecise)
- swapValues(ref, val);
- }
-
- const EValueTarget refCode = this->valTarget(ref);
- if (VT_RANGE == refCode)
- // not supported yet
+ // try to look through possibly empty abstract objects
+ val = lookThrough(&seen, *const_cast<SymHeap *>(this), val);
+ if (VAL_INVALID == val)
return false;
- const TOffset off = this->valOffset(val);
- EValueTarget code = this->valTarget(val);
- TValSet haveSeen;
-
- while (0 < val && insertOnce(haveSeen, val)) {
- switch (code) {
- case VT_ABSTRACT:
- break;
-
- case VT_ON_STACK:
- case VT_ON_HEAP:
- case VT_STATIC:
- // concrete object reached --> prove done
- return (val != ref);
-
- case VT_INVALID:
- case VT_CUSTOM:
- return SymHeapCore::proveNeq(ref, val);
-
- case VT_RANGE:
- // TODO: improve the reasoning about VT_RANGE values
- // fall through!
-
- case VT_DELETED:
- case VT_LOST:
- return (VAL_NULL == ref);
+ // try to look through possibly empty abstract objects
+ ref = lookThrough(&seen, *const_cast<SymHeap *>(this), ref);
+ if (VAL_INVALID == ref)
+ return false;
- case VT_COMPOSITE:
- CL_BREAK_IF("SymHeap::proveNeq() sees VT_COMPOSITE");
- // fall through!
+ if (SymHeapCore::proveNeq(ref, val))
+ // values are non-equal in non-abstract world
+ return true;
- case VT_UNKNOWN:
- // we can't prove much for unknown values
- return false;
- }
+ // having the values always in the same order leads to simpler code
+ moveKnownValueToLeft(*this, ref, val);
- SymHeap &writable = *const_cast<SymHeap *>(this);
+ const TSizeRange size2 = this->valSizeOfTarget(val);
+ if (size2.lo <= IR::Int0)
+ // oops, we cannot prove the address is safely allocated, giving up
+ return false;
- TValId seg = this->valRoot(val);
- const EObjKind kind = this->valTargetKind(val);
- if (OK_DLS == kind)
- seg = dlSegPeer(writable, seg);
+ const TValId root2 = this->valRoot(val);
+ const TMinLen len2 = objMinLength(*this, root2);
+ if (!len2)
+ // one of the targets is possibly empty, giving up
+ return false;
- if (seg < 0)
- // no valid object here
- return false;
+ if (VAL_NULL == ref)
+ // one of them is VAL_NULL the other one is address of non-empty object
+ return true;
- if (this->segMinLength(seg))
- // non-empty abstract object reached
- return (VAL_NULL == ref)
- || isKnownObject(refCode);
+ const TSizeRange size1 = this->valSizeOfTarget(ref);
+ if (size1.lo <= IR::Int0)
+ // oops, we cannot prove the address is safely allocated, giving up
+ return false;
- // jump to next value while taking the 'head' offset into consideration
- const TValId valNext = nextValFromSeg(writable, seg);
+ const TValId root1 = this->valRoot(ref);
+ const TMinLen len1 = objMinLength(*this, root1);
+ if (!len1)
+ // both targets are possibly empty, giving up
+ return false;
- if (OK_OBJ_OR_NULL == kind) {
- CL_BREAK_IF(VAL_NULL != valNext);
- val = VAL_NULL;
- }
- else {
- const BindingOff &bOff = this->segBinding(seg);
- val = writable.valByOffset(valNext, off - bOff.head);
- }
+ if (!isAbstract(this->valTarget(ref)))
+ // non-empty abstract object vs. concrete object
+ return true;
- code = this->valTarget(val);
- }
+ if (root2 != segPeer(*this, root1))
+ // a pair of non-empty abstract objects
+ return true;
- return false;
+ // one value points at segment and the other points at its peer
+ CL_BREAK_IF(len1 != len2);
+ return (1 < len1);
}
void SymHeap::valDestroyTarget(TValId root) {
View
6 tests/predator-regre/test-0010.err
@@ -4,9 +4,3 @@ test-0010.c:53:5: note: from call of main()
test-0010.c:48:13: warning: memory leak detected while destroying a heap object
test-0010.c:73:27: note: from call of destroy_cyclic_sll()
test-0010.c:53:5: note: from call of main()
-test-0010.c:48:13: warning: memory leak detected while destroying a heap object
-test-0010.c:73:27: note: from call of destroy_cyclic_sll()
-test-0010.c:53:5: note: from call of main()
-test-0010.c:48:13: warning: memory leak detected while destroying a heap object
-test-0010.c:73:27: note: from call of destroy_cyclic_sll()
-test-0010.c:53:5: note: from call of main()
View
6 tests/predator-regre/test-0010.err.oom
@@ -4,9 +4,3 @@ test-0010.c:53:5: note: from call of main()
test-0010.c:48:13: warning: memory leak detected while destroying a heap object
test-0010.c:73:27: note: from call of destroy_cyclic_sll()
test-0010.c:53:5: note: from call of main()
-test-0010.c:48:13: warning: memory leak detected while destroying a heap object
-test-0010.c:73:27: note: from call of destroy_cyclic_sll()
-test-0010.c:53:5: note: from call of main()
-test-0010.c:48:13: warning: memory leak detected while destroying a heap object
-test-0010.c:73:27: note: from call of destroy_cyclic_sll()
-test-0010.c:53:5: note: from call of main()
View
6 tests/predator-regre/test-0010.err.uninit
@@ -4,9 +4,3 @@ test-0010.c:53:5: note: from call of main()
test-0010.c:48:13: warning: memory leak detected while destroying a heap object
test-0010.c:73:27: note: from call of destroy_cyclic_sll()
test-0010.c:53:5: note: from call of main()
-test-0010.c:48:13: warning: memory leak detected while destroying a heap object
-test-0010.c:73:27: note: from call of destroy_cyclic_sll()
-test-0010.c:53:5: note: from call of main()
-test-0010.c:48:13: warning: memory leak detected while destroying a heap object
-test-0010.c:73:27: note: from call of destroy_cyclic_sll()
-test-0010.c:53:5: note: from call of main()
View
3 tests/predator-regre/test-0053.err
@@ -2,7 +2,4 @@ test-0053.c:65:15: note: writing heap graph to '01-cyclic-sll-ready-0000.dot'...
test-0053.c:52:13: warning: memory leak detected while destroying a heap object
test-0053.c:68:27: note: from call of destroy_cyclic_sll()
test-0053.c:57:5: note: from call of main()
-test-0053.c:52:13: warning: memory leak detected while destroying a heap object
-test-0053.c:68:27: note: from call of destroy_cyclic_sll()
-test-0053.c:57:5: note: from call of main()
test-0053.c:71:15: note: writing heap graph to '02-cyclic-sll-gone-0000.dot'...
View
3 tests/predator-regre/test-0053.err.oom
@@ -2,7 +2,4 @@ test-0053.c:65:15: note: writing heap graph to '01-cyclic-sll-ready-0000.dot'...
test-0053.c:52:13: warning: memory leak detected while destroying a heap object
test-0053.c:68:27: note: from call of destroy_cyclic_sll()
test-0053.c:57:5: note: from call of main()
-test-0053.c:52:13: warning: memory leak detected while destroying a heap object
-test-0053.c:68:27: note: from call of destroy_cyclic_sll()
-test-0053.c:57:5: note: from call of main()
test-0053.c:71:15: note: writing heap graph to '02-cyclic-sll-gone-0000.dot'...
View
3 tests/predator-regre/test-0053.err.uninit
@@ -2,7 +2,4 @@ test-0053.c:65:15: note: writing heap graph to '01-cyclic-sll-ready-0000.dot'...
test-0053.c:52:13: warning: memory leak detected while destroying a heap object
test-0053.c:68:27: note: from call of destroy_cyclic_sll()
test-0053.c:57:5: note: from call of main()
-test-0053.c:52:13: warning: memory leak detected while destroying a heap object
-test-0053.c:68:27: note: from call of destroy_cyclic_sll()
-test-0053.c:57:5: note: from call of main()
test-0053.c:71:15: note: writing heap graph to '02-cyclic-sll-gone-0000.dot'...
View
18 tests/predator-regre/test-0184.err.oom
@@ -4,32 +4,20 @@ test-0184.c:5:13: warning: end of function fail() has not been reached
test-0184.c:97:9: note: from call of fail()
test-0184.c:114:19: note: from call of check_seq_next()
test-0184.c:108:5: note: from call of main()
+test-0184.c:92:6: warning: end of function check_seq_next() has not been reached
+test-0184.c:114:19: note: from call of check_seq_next()
+test-0184.c:108:5: note: from call of main()
test-0184.c:119:15: note: writing heap graph to 'test-0184.c-119-0000.dot'...
test-0184.c:119:15: note: writing heap graph to 'test-0184.c-119-0001.dot'...
test-0184.c:119:15: note: writing heap graph to 'test-0184.c-119-0002.dot'...
test-0184.c:119:15: note: writing heap graph to 'test-0184.c-119-0003.dot'...
test-0184.c:119:15: note: writing heap graph to 'test-0184.c-119-0004.dot'...
-test-0184.c:119:15: note: writing heap graph to 'test-0184.c-119-0005.dot'...
-test-0184.c:119:15: note: writing heap graph to 'test-0184.c-119-0006.dot'...
-test-0184.c:119:15: note: writing heap graph to 'test-0184.c-119-0007.dot'...
-test-0184.c:92:6: warning: end of function check_seq_next() has not been reached
-test-0184.c:120:19: note: from call of check_seq_next()
-test-0184.c:108:5: note: from call of main()
-test-0184.c:92:6: warning: end of function check_seq_next() has not been reached
-test-0184.c:120:19: note: from call of check_seq_next()
-test-0184.c:108:5: note: from call of main()
test-0184.c:124:15: note: writing heap graph to 'test-0184.c-124-0000.dot'...
test-0184.c:124:15: note: writing heap graph to 'test-0184.c-124-0001.dot'...
test-0184.c:124:15: note: writing heap graph to 'test-0184.c-124-0002.dot'...
test-0184.c:124:15: note: writing heap graph to 'test-0184.c-124-0003.dot'...
test-0184.c:124:15: note: writing heap graph to 'test-0184.c-124-0004.dot'...
-test-0184.c:124:15: note: writing heap graph to 'test-0184.c-124-0005.dot'...
-test-0184.c:124:15: note: writing heap graph to 'test-0184.c-124-0006.dot'...
-test-0184.c:100:6: warning: end of function check_seq_prev() has not been reached
-test-0184.c:125:19: note: from call of check_seq_prev()
-test-0184.c:108:5: note: from call of main()
test-0184.c:129:15: note: writing heap graph to 'test-0184.c-129-0000.dot'...
test-0184.c:129:15: note: writing heap graph to 'test-0184.c-129-0001.dot'...
test-0184.c:129:15: note: writing heap graph to 'test-0184.c-129-0002.dot'...
test-0184.c:129:15: note: writing heap graph to 'test-0184.c-129-0003.dot'...
-test-0184.c:129:15: note: writing heap graph to 'test-0184.c-129-0004.dot'...
View
18 tests/predator-regre/test-0184.err.uninit
@@ -4,32 +4,20 @@ test-0184.c:5:13: warning: end of function fail() has not been reached
test-0184.c:97:9: note: from call of fail()
test-0184.c:114:19: note: from call of check_seq_next()
test-0184.c:108:5: note: from call of main()
+test-0184.c:92:6: warning: end of function check_seq_next() has not been reached
+test-0184.c:114:19: note: from call of check_seq_next()
+test-0184.c:108:5: note: from call of main()
test-0184.c:119:15: note: writing heap graph to 'test-0184.c-119-0000.dot'...
test-0184.c:119:15: note: writing heap graph to 'test-0184.c-119-0001.dot'...
test-0184.c:119:15: note: writing heap graph to 'test-0184.c-119-0002.dot'...
test-0184.c:119:15: note: writing heap graph to 'test-0184.c-119-0003.dot'...
test-0184.c:119:15: note: writing heap graph to 'test-0184.c-119-0004.dot'...
-test-0184.c:119:15: note: writing heap graph to 'test-0184.c-119-0005.dot'...
-test-0184.c:119:15: note: writing heap graph to 'test-0184.c-119-0006.dot'...
-test-0184.c:119:15: note: writing heap graph to 'test-0184.c-119-0007.dot'...
-test-0184.c:92:6: warning: end of function check_seq_next() has not been reached
-test-0184.c:120:19: note: from call of check_seq_next()
-test-0184.c:108:5: note: from call of main()
-test-0184.c:92:6: warning: end of function check_seq_next() has not been reached
-test-0184.c:120:19: note: from call of check_seq_next()
-test-0184.c:108:5: note: from call of main()
test-0184.c:124:15: note: writing heap graph to 'test-0184.c-124-0000.dot'...
test-0184.c:124:15: note: writing heap graph to 'test-0184.c-124-0001.dot'...
test-0184.c:124:15: note: writing heap graph to 'test-0184.c-124-0002.dot'...
test-0184.c:124:15: note: writing heap graph to 'test-0184.c-124-0003.dot'...
test-0184.c:124:15: note: writing heap graph to 'test-0184.c-124-0004.dot'...
-test-0184.c:124:15: note: writing heap graph to 'test-0184.c-124-0005.dot'...
-test-0184.c:124:15: note: writing heap graph to 'test-0184.c-124-0006.dot'...
-test-0184.c:100:6: warning: end of function check_seq_prev() has not been reached
-test-0184.c:125:19: note: from call of check_seq_prev()
-test-0184.c:108:5: note: from call of main()
test-0184.c:129:15: note: writing heap graph to 'test-0184.c-129-0000.dot'...
test-0184.c:129:15: note: writing heap graph to 'test-0184.c-129-0001.dot'...
test-0184.c:129:15: note: writing heap graph to 'test-0184.c-129-0002.dot'...
test-0184.c:129:15: note: writing heap graph to 'test-0184.c-129-0003.dot'...
-test-0184.c:129:15: note: writing heap graph to 'test-0184.c-129-0004.dot'...

0 comments on commit 934a26a

Please sign in to comment.
Something went wrong with that request. Please try again.