CPP: Fix performance issue. Also has a small positive effect on correctness.

This commit is contained in:
Geoffrey White
2019-03-01 17:51:53 +00:00
parent f0085ed25a
commit df73bb3468
3 changed files with 25 additions and 17 deletions

View File

@@ -46,13 +46,14 @@ predicate allocExprOrIndirect(Expr alloc, string kind) {
alloc.(FunctionCall).getTarget() = rtn.getEnclosingFunction() and
(
allocExprOrIndirect(rtn.getExpr(), kind) or
allocReaches(rtn.getExpr(), _, kind)
allocReaches0(rtn.getExpr(), _, kind)
)
)
}
/**
* Holds if `v` is assigned value `e`, and `e` is not known to be `0`.
* Holds if `v` is a global variable assigned value `e`, and `e` is not known
* to be `0`.
*/
private predicate nonNullGlobalAssignment(Variable v, Expr e) {
not v instanceof LocalScopeVariable and
@@ -61,17 +62,13 @@ private predicate nonNullGlobalAssignment(Variable v, Expr e) {
}
/**
* Holds if `v` is a non-local variable which is assigned only with allocations of
* type `kind` (it may also be assigned with NULL).
* Holds if `v` is a non-local variable which is assigned with allocations of
* type `kind`.
*/
private predicate allocReachesVariable(Variable v, Expr alloc, string kind) {
private cached predicate allocReachesVariable(Variable v, Expr alloc, string kind) {
exists(Expr mid |
nonNullGlobalAssignment(v, mid) and
allocReaches(mid, alloc, kind)
) and
forall(Expr mid |
nonNullGlobalAssignment(v, mid) |
allocReaches(mid, _, kind)
allocReaches0(mid, alloc, kind)
)
}
@@ -80,22 +77,35 @@ private predicate allocReachesVariable(Variable v, Expr alloc, string kind) {
* result of a previous memory allocation `alloc`. `kind` is a
* string describing the type of that allocation.
*/
predicate allocReaches(Expr e, Expr alloc, string kind) {
private predicate allocReaches0(Expr e, Expr alloc, string kind) {
(
// alloc
allocExprOrIndirect(alloc, kind) and
e = alloc
) or exists(SsaDefinition def, LocalScopeVariable v |
// alloc via SSA
allocReaches(def.getAnUltimateDefiningValue(v), alloc, kind) and
allocReaches0(def.getAnUltimateDefiningValue(v), alloc, kind) and
e = def.getAUse(v)
) or exists(Variable v |
// alloc via a singly assigned global
// alloc via a global
allocReachesVariable(v, alloc, kind) and
e.(VariableAccess).getTarget() = v
)
}
/**
* Holds if `e` is an expression which may evaluate to the
* result of previous memory allocations `alloc` only of type
* `kind`.
*/
predicate allocReaches(Expr e, Expr alloc, string kind) {
allocReaches0(e, alloc, kind) and
not exists(string k2 |
allocReaches0(e, _, k2) and
kind != k2
)
}
/**
* Holds if `free` is a use of free or delete. `freed` is the
* expression that is freed / deleted and `kind` is a string

View File

@@ -12,5 +12,3 @@
| test.cpp:235:2:235:5 | call to free | There is a new/free mismatch between this free and the corresponding $@. | test.cpp:227:7:227:13 | new | new |
| test.cpp:239:2:239:5 | call to free | There is a new/free mismatch between this free and the corresponding $@. | test.cpp:228:7:228:17 | new[] | new[] |
| test.cpp:272:3:272:6 | call to free | There is a new/free mismatch between this free and the corresponding $@. | test.cpp:265:7:265:13 | new | new |
| test.cpp:367:3:367:10 | delete | There is a malloc/delete mismatch between this delete and the corresponding $@. | test.cpp:359:14:359:19 | call to malloc | malloc |
| test.cpp:370:3:370:6 | call to free | There is a new/free mismatch between this free and the corresponding $@. | test.cpp:356:7:356:15 | new | new |

View File

@@ -364,10 +364,10 @@ void test12(bool cond)
if (cond)
{
delete y; // GOOD [FALSE POSITIVE]
delete y; // GOOD
delete z; // GOOD
} else {
free(y); // GOOD [FALSE POSITIVE]
free(y); // GOOD
free(z); // GOOD
}
}