@@ -46,32 +46,20 @@ predicate allocExprOrIndirect(Expr alloc, string kind) {
4646 alloc .( FunctionCall ) .getTarget ( ) = rtn .getEnclosingFunction ( ) and
4747 (
4848 allocExprOrIndirect ( rtn .getExpr ( ) , kind ) or
49- allocReaches ( rtn .getExpr ( ) , _, kind )
49+ allocReaches0 ( rtn .getExpr ( ) , _, kind )
5050 )
5151 )
5252}
5353
5454/**
55- * Holds if `v` is assigned value `e`, and `e` is not known to be `0`.
55+ * Holds if `v` is a non-local variable which is assigned with allocations of
56+ * type `kind`.
5657 */
57- private predicate nonNullGlobalAssignment ( Variable v , Expr e ) {
58- not v instanceof LocalScopeVariable and
59- v .getAnAssignedValue ( ) = e and
60- not e .getValue ( ) .toInt ( ) = 0
61- }
62-
63- /**
64- * Holds if `v` is a non-local variable which is assigned only with allocations of
65- * type `kind` (it may also be assigned with NULL).
66- */
67- private predicate allocReachesVariable ( Variable v , Expr alloc , string kind ) {
58+ private pragma [ nomagic] predicate allocReachesVariable ( Variable v , Expr alloc , string kind ) {
6859 exists ( Expr mid |
69- nonNullGlobalAssignment ( v , mid ) and
70- allocReaches ( mid , alloc , kind )
71- ) and
72- forall ( Expr mid |
73- nonNullGlobalAssignment ( v , mid ) |
74- allocReaches ( mid , _, kind )
60+ not v instanceof LocalScopeVariable and
61+ v .getAnAssignedValue ( ) = mid and
62+ allocReaches0 ( mid , alloc , kind )
7563 )
7664}
7765
@@ -80,22 +68,35 @@ private predicate allocReachesVariable(Variable v, Expr alloc, string kind) {
8068 * result of a previous memory allocation `alloc`. `kind` is a
8169 * string describing the type of that allocation.
8270 */
83- predicate allocReaches ( Expr e , Expr alloc , string kind ) {
71+ private predicate allocReaches0 ( Expr e , Expr alloc , string kind ) {
8472 (
8573 // alloc
8674 allocExprOrIndirect ( alloc , kind ) and
8775 e = alloc
8876 ) or exists ( SsaDefinition def , LocalScopeVariable v |
8977 // alloc via SSA
90- allocReaches ( def .getAnUltimateDefiningValue ( v ) , alloc , kind ) and
78+ allocReaches0 ( def .getAnUltimateDefiningValue ( v ) , alloc , kind ) and
9179 e = def .getAUse ( v )
9280 ) or exists ( Variable v |
93- // alloc via a singly assigned global
81+ // alloc via a global
9482 allocReachesVariable ( v , alloc , kind ) and
9583 e .( VariableAccess ) .getTarget ( ) = v
9684 )
9785}
9886
87+ /**
88+ * Holds if `e` is an expression which may evaluate to the
89+ * result of previous memory allocations `alloc` only of type
90+ * `kind`.
91+ */
92+ predicate allocReaches ( Expr e , Expr alloc , string kind ) {
93+ allocReaches0 ( e , alloc , kind ) and
94+ not exists ( string k2 |
95+ allocReaches0 ( e , _, k2 ) and
96+ kind != k2
97+ )
98+ }
99+
99100/**
100101 * Holds if `free` is a use of free or delete. `freed` is the
101102 * expression that is freed / deleted and `kind` is a string
0 commit comments