@@ -161,6 +161,10 @@ private class UnsignedMulExpr extends MulExpr {
161161 UnsignedMulExpr ( ) { this .getType ( ) .( IntegralType ) .isUnsigned ( ) }
162162}
163163
164+ private class UnsignedAssignMulExpr extends AssignMulExpr {
165+ UnsignedAssignMulExpr ( ) { this .getType ( ) .( IntegralType ) .isUnsigned ( ) }
166+ }
167+
164168/** Set of expressions which we know how to analyze. */
165169private predicate analyzableExpr ( Expr e ) {
166170 // The type of the expression must be arithmetic. We reuse the logic in
@@ -191,6 +195,8 @@ private predicate analyzableExpr(Expr e) {
191195 or
192196 e instanceof AssignSubExpr
193197 or
198+ e instanceof UnsignedAssignMulExpr
199+ or
194200 e instanceof CrementOperation
195201 or
196202 e instanceof RemExpr
@@ -237,25 +243,27 @@ private predicate defDependsOnDef(
237243 // Definitions with a defining value.
238244 exists ( Expr expr | assignmentDef ( def , v , expr ) | exprDependsOnDef ( expr , srcDef , srcVar ) )
239245 or
240- exists ( AssignAddExpr assignAdd , RangeSsaDefinition nextDef |
246+ exists ( AssignAddExpr assignAdd |
241247 def = assignAdd and
242- assignAdd .getLValue ( ) = nextDef .getAUse ( v )
243- |
244- defDependsOnDef ( nextDef , v , srcDef , srcVar ) or
245- exprDependsOnDef ( assignAdd .getRValue ( ) , srcDef , srcVar )
248+ def .getAVariable ( ) = v and
249+ exprDependsOnDef ( assignAdd .getAnOperand ( ) , srcDef , srcVar )
246250 )
247251 or
248- exists ( AssignSubExpr assignSub , RangeSsaDefinition nextDef |
252+ exists ( AssignSubExpr assignSub |
249253 def = assignSub and
250- assignSub .getLValue ( ) = nextDef .getAUse ( v )
251- |
252- defDependsOnDef ( nextDef , v , srcDef , srcVar ) or
253- exprDependsOnDef ( assignSub .getRValue ( ) , srcDef , srcVar )
254+ def .getAVariable ( ) = v and
255+ exprDependsOnDef ( assignSub .getAnOperand ( ) , srcDef , srcVar )
256+ )
257+ or
258+ exists ( UnsignedAssignMulExpr assignMul |
259+ def = assignMul and
260+ def .getAVariable ( ) = v and
261+ exprDependsOnDef ( assignMul .getAnOperand ( ) , srcDef , srcVar )
254262 )
255263 or
256264 exists ( CrementOperation crem |
257265 def = crem and
258- crem . getOperand ( ) = v . getAnAccess ( ) and
266+ def . getAVariable ( ) = v and
259267 exprDependsOnDef ( crem .getOperand ( ) , srcDef , srcVar )
260268 )
261269 or
@@ -302,6 +310,10 @@ private predicate exprDependsOnDef(Expr e, RangeSsaDefinition srcDef, StackVaria
302310 exprDependsOnDef ( subExpr .getAnOperand ( ) , srcDef , srcVar )
303311 )
304312 or
313+ exists ( UnsignedAssignMulExpr mulExpr | e = mulExpr |
314+ exprDependsOnDef ( mulExpr .getAnOperand ( ) , srcDef , srcVar )
315+ )
316+ or
305317 exists ( CrementOperation crementExpr | e = crementExpr |
306318 exprDependsOnDef ( crementExpr .getOperand ( ) , srcDef , srcVar )
307319 )
@@ -669,6 +681,13 @@ private float getLowerBoundsImpl(Expr expr) {
669681 result = addRoundingDown ( xLow , - yHigh )
670682 )
671683 or
684+ exists ( UnsignedAssignMulExpr mulExpr , float xLow , float yLow |
685+ expr = mulExpr and
686+ xLow = getFullyConvertedLowerBounds ( mulExpr .getLValue ( ) ) and
687+ yLow = getFullyConvertedLowerBounds ( mulExpr .getRValue ( ) ) and
688+ result = xLow * yLow
689+ )
690+ or
672691 exists ( PrefixIncrExpr incrExpr , float xLow |
673692 expr = incrExpr and
674693 xLow = getFullyConvertedLowerBounds ( incrExpr .getOperand ( ) ) and
@@ -853,6 +872,13 @@ private float getUpperBoundsImpl(Expr expr) {
853872 result = addRoundingUp ( xHigh , - yLow )
854873 )
855874 or
875+ exists ( UnsignedAssignMulExpr mulExpr , float xHigh , float yHigh |
876+ expr = mulExpr and
877+ xHigh = getFullyConvertedUpperBounds ( mulExpr .getLValue ( ) ) and
878+ yHigh = getFullyConvertedUpperBounds ( mulExpr .getRValue ( ) ) and
879+ result = xHigh * yHigh
880+ )
881+ or
856882 exists ( PrefixIncrExpr incrExpr , float xHigh |
857883 expr = incrExpr and
858884 xHigh = getFullyConvertedUpperBounds ( incrExpr .getOperand ( ) ) and
@@ -1089,6 +1115,14 @@ private float getDefLowerBoundsImpl(RangeSsaDefinition def, StackVariable v) {
10891115 result = addRoundingDown ( lhsLB , - rhsUB )
10901116 )
10911117 or
1118+ exists ( UnsignedAssignMulExpr assignMul , RangeSsaDefinition nextDef , float lhsLB , float rhsLB |
1119+ def = assignMul and
1120+ assignMul .getLValue ( ) = nextDef .getAUse ( v ) and
1121+ lhsLB = getDefLowerBounds ( nextDef , v ) and
1122+ rhsLB = getFullyConvertedLowerBounds ( assignMul .getRValue ( ) ) and
1123+ result = lhsLB * rhsLB
1124+ )
1125+ or
10921126 exists ( IncrementOperation incr , float newLB |
10931127 def = incr and
10941128 incr .getOperand ( ) = v .getAnAccess ( ) and
@@ -1131,6 +1165,14 @@ private float getDefUpperBoundsImpl(RangeSsaDefinition def, StackVariable v) {
11311165 result = addRoundingUp ( lhsUB , - rhsLB )
11321166 )
11331167 or
1168+ exists ( UnsignedAssignMulExpr assignMul , RangeSsaDefinition nextDef , float lhsUB , float rhsUB |
1169+ def = assignMul and
1170+ assignMul .getLValue ( ) = nextDef .getAUse ( v ) and
1171+ lhsUB = getDefUpperBounds ( nextDef , v ) and
1172+ rhsUB = getFullyConvertedUpperBounds ( assignMul .getRValue ( ) ) and
1173+ result = lhsUB * rhsUB
1174+ )
1175+ or
11341176 exists ( IncrementOperation incr , float newUB |
11351177 def = incr and
11361178 incr .getOperand ( ) = v .getAnAccess ( ) and
0 commit comments