@@ -73,67 +73,29 @@ private int isSource(Expr bufferExpr, Element why) {
7373 )
7474}
7575
76- /**
77- * Holds if `e2` is an expression that is derived from `e1` such that if `e1[n]` is a
78- * well-defined expression for some number `n`, then `e2[n + delta]` is also a well-defined
79- * expression.
80- */
81- private predicate step ( Expr e1 , Expr e2 , int delta ) {
82- getBufferSizeCand0 ( e1 ) and
83- (
84- exists ( Variable bufferVar , Class parentClass , VariableAccess parentPtr , int bufferSize |
85- e1 = parentPtr
86- |
87- bufferVar = e2 .( VariableAccess ) .getTarget ( ) and
88- // buffer is the parentPtr->bufferVar of a 'variable size struct'
89- memberMayBeVarSize ( parentClass , bufferVar ) and
90- parentPtr = e2 .( VariableAccess ) .getQualifier ( ) and
91- parentPtr .getTarget ( ) .getUnspecifiedType ( ) .( PointerType ) .getBaseType ( ) = parentClass and
92- (
93- if exists ( bufferVar .getType ( ) .getSize ( ) )
94- then bufferSize = bufferVar .getType ( ) .getSize ( )
95- else bufferSize = 0
96- ) and
97- delta = bufferSize - parentClass .getSize ( )
98- )
99- or
100- DataFlow:: localExprFlowStep ( e1 , e2 ) and
101- delta = 0
102- )
103- }
104-
105- pragma [ nomagic]
106- private predicate getBufferSizeCand0 ( Expr e ) {
107- exists ( isSource ( e , _) )
108- or
109- exists ( Expr e0 |
110- getBufferSizeCand0 ( e0 ) and
111- step ( e0 , e , _)
112- )
113- }
114-
115- /**
116- * Get the size in bytes of the buffer pointed to by an expression (if this can be determined).
117- *
118- * NOTE: There can be multiple `(result, why)` for a given `bufferExpr`.
119- */
120- private int getBufferSizeCand ( Expr bufferExpr , Element why ) {
121- getBufferSizeCand0 ( bufferExpr ) and
122- (
123- result = isSource ( bufferExpr , why )
124- or
125- exists ( Expr e0 , int delta , int size |
126- size = getBufferSizeCand ( e0 , why ) and
127- step ( e0 , bufferExpr , delta ) and
128- result = size + delta
129- )
130- )
131- }
132-
13376/**
13477 * Get the size in bytes of the buffer pointed to by an expression (if this can be determined).
13578 */
79+ language [ monotonicAggregates]
13680int getBufferSize ( Expr bufferExpr , Element why ) {
137- result = max ( | | getBufferSizeCand ( bufferExpr , _) ) and
138- result = getBufferSizeCand ( bufferExpr , why )
81+ result = isSource ( bufferExpr , why )
82+ or
83+ exists ( Class parentClass , VariableAccess parentPtr , int bufferSize , Variable bufferVar |
84+ bufferVar = bufferExpr .( VariableAccess ) .getTarget ( ) and
85+ // buffer is the parentPtr->bufferVar of a 'variable size struct'
86+ memberMayBeVarSize ( parentClass , bufferVar ) and
87+ why = bufferVar and
88+ parentPtr = bufferExpr .( VariableAccess ) .getQualifier ( ) and
89+ parentPtr .getTarget ( ) .getUnspecifiedType ( ) .( PointerType ) .getBaseType ( ) = parentClass and
90+ result = getBufferSize ( parentPtr , _) + bufferSize - parentClass .getSize ( )
91+ |
92+ if exists ( bufferVar .getType ( ) .getSize ( ) )
93+ then bufferSize = bufferVar .getType ( ) .getSize ( )
94+ else bufferSize = 0
95+ )
96+ or
97+ // dataflow (all sources must be the same size)
98+ result = unique( Expr def | DataFlow:: localExprFlowStep ( def , bufferExpr ) | getBufferSize ( def , _) ) and
99+ // find reason
100+ exists ( Expr def | DataFlow:: localExprFlowStep ( def , bufferExpr ) | exists ( getBufferSize ( def , why ) ) )
139101}
0 commit comments