From f0085ed25aed767a177f94692210eebcd3708cf9 Mon Sep 17 00:00:00 2001 From: Geoffrey White <40627776+geoffw0@users.noreply.github.com> Date: Mon, 4 Mar 2019 12:37:43 +0000 Subject: [PATCH 1/4] CPP: Additional test cases. --- .../Critical/NewFree/NewFreeMismatch.expected | 2 ++ .../query-tests/Critical/NewFree/test.cpp | 34 +++++++++++++++++++ 2 files changed, 36 insertions(+) diff --git a/cpp/ql/test/query-tests/Critical/NewFree/NewFreeMismatch.expected b/cpp/ql/test/query-tests/Critical/NewFree/NewFreeMismatch.expected index c5fd0d623a02..ce41889db422 100644 --- a/cpp/ql/test/query-tests/Critical/NewFree/NewFreeMismatch.expected +++ b/cpp/ql/test/query-tests/Critical/NewFree/NewFreeMismatch.expected @@ -12,3 +12,5 @@ | 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 | diff --git a/cpp/ql/test/query-tests/Critical/NewFree/test.cpp b/cpp/ql/test/query-tests/Critical/NewFree/test.cpp index fd5485ca8766..43506d8baf6a 100644 --- a/cpp/ql/test/query-tests/Critical/NewFree/test.cpp +++ b/cpp/ql/test/query-tests/Critical/NewFree/test.cpp @@ -337,3 +337,37 @@ class Test11 char *data; }; + +// --- + +int *z; + +void test12(bool cond) +{ + int *x, *y; + + x = new int(); + delete x; // GOOD + x = (int *)malloc(sizeof(int)); + free(x); // GOOD + + if (cond) + { + y = new int(); + z = new int(); + } else { + y = (int *)malloc(sizeof(int)); + z = (int *)malloc(sizeof(int)); + } + + // ... + + if (cond) + { + delete y; // GOOD [FALSE POSITIVE] + delete z; // GOOD + } else { + free(y); // GOOD [FALSE POSITIVE] + free(z); // GOOD + } +} From df73bb34689780d11c6d5dd02e48f5b1473154e7 Mon Sep 17 00:00:00 2001 From: Geoffrey White <40627776+geoffw0@users.noreply.github.com> Date: Fri, 1 Mar 2019 17:51:53 +0000 Subject: [PATCH 2/4] CPP: Fix performance issue. Also has a small positive effect on correctness. --- cpp/ql/src/Critical/NewDelete.qll | 36 ++++++++++++------- .../Critical/NewFree/NewFreeMismatch.expected | 2 -- .../query-tests/Critical/NewFree/test.cpp | 4 +-- 3 files changed, 25 insertions(+), 17 deletions(-) diff --git a/cpp/ql/src/Critical/NewDelete.qll b/cpp/ql/src/Critical/NewDelete.qll index 05c641c04c32..d8a6dde23859 100644 --- a/cpp/ql/src/Critical/NewDelete.qll +++ b/cpp/ql/src/Critical/NewDelete.qll @@ -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 diff --git a/cpp/ql/test/query-tests/Critical/NewFree/NewFreeMismatch.expected b/cpp/ql/test/query-tests/Critical/NewFree/NewFreeMismatch.expected index ce41889db422..c5fd0d623a02 100644 --- a/cpp/ql/test/query-tests/Critical/NewFree/NewFreeMismatch.expected +++ b/cpp/ql/test/query-tests/Critical/NewFree/NewFreeMismatch.expected @@ -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 | diff --git a/cpp/ql/test/query-tests/Critical/NewFree/test.cpp b/cpp/ql/test/query-tests/Critical/NewFree/test.cpp index 43506d8baf6a..4fe8559d7eb0 100644 --- a/cpp/ql/test/query-tests/Critical/NewFree/test.cpp +++ b/cpp/ql/test/query-tests/Critical/NewFree/test.cpp @@ -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 } } From a9ce2f7a62634337befaab112b98d7decb7d74e6 Mon Sep 17 00:00:00 2001 From: Geoffrey White <40627776+geoffw0@users.noreply.github.com> Date: Mon, 4 Mar 2019 13:13:04 +0000 Subject: [PATCH 3/4] CPP: Simplify out some old optimizations (that make little difference now). --- cpp/ql/src/Critical/NewDelete.qll | 13 ++----------- 1 file changed, 2 insertions(+), 11 deletions(-) diff --git a/cpp/ql/src/Critical/NewDelete.qll b/cpp/ql/src/Critical/NewDelete.qll index d8a6dde23859..71b32d283724 100644 --- a/cpp/ql/src/Critical/NewDelete.qll +++ b/cpp/ql/src/Critical/NewDelete.qll @@ -51,23 +51,14 @@ predicate allocExprOrIndirect(Expr alloc, string kind) { ) } -/** - * 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 - v.getAnAssignedValue() = e and - not e.getValue().toInt() = 0 -} - /** * Holds if `v` is a non-local variable which is assigned with allocations of * type `kind`. */ private cached predicate allocReachesVariable(Variable v, Expr alloc, string kind) { exists(Expr mid | - nonNullGlobalAssignment(v, mid) and + not v instanceof LocalScopeVariable and + v.getAnAssignedValue() = mid and allocReaches0(mid, alloc, kind) ) } From 56fe91d774493d86a494eba71590dbac33b5d4e9 Mon Sep 17 00:00:00 2001 From: Geoffrey White <40627776+geoffw0@users.noreply.github.com> Date: Tue, 5 Mar 2019 08:59:16 +0000 Subject: [PATCH 4/4] CPP: cached -> pragma[nomagic]. --- cpp/ql/src/Critical/NewDelete.qll | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/cpp/ql/src/Critical/NewDelete.qll b/cpp/ql/src/Critical/NewDelete.qll index 71b32d283724..97848e3bbdf2 100644 --- a/cpp/ql/src/Critical/NewDelete.qll +++ b/cpp/ql/src/Critical/NewDelete.qll @@ -55,7 +55,7 @@ predicate allocExprOrIndirect(Expr alloc, string kind) { * Holds if `v` is a non-local variable which is assigned with allocations of * type `kind`. */ -private cached predicate allocReachesVariable(Variable v, Expr alloc, string kind) { +private pragma[nomagic] predicate allocReachesVariable(Variable v, Expr alloc, string kind) { exists(Expr mid | not v instanceof LocalScopeVariable and v.getAnAssignedValue() = mid and