@@ -32,7 +32,8 @@ private predicate nonConstAddition(Expr add, Expr larg, Expr rarg) {
3232 exists ( AddExpr a | a = add |
3333 larg = a .getLeftOperand ( ) and
3434 rarg = a .getRightOperand ( )
35- ) or
35+ )
36+ or
3637 exists ( AssignAddExpr a | a = add |
3738 larg = a .getDest ( ) and
3839 rarg = a .getRhs ( )
@@ -51,7 +52,8 @@ private predicate nonConstSubtraction(Expr sub, Expr larg, Expr rarg) {
5152 exists ( SubExpr s | s = sub |
5253 larg = s .getLeftOperand ( ) and
5354 rarg = s .getRightOperand ( )
54- ) or
55+ )
56+ or
5557 exists ( AssignSubExpr s | s = sub |
5658 larg = s .getDest ( ) and
5759 rarg = s .getRhs ( )
@@ -67,12 +69,14 @@ private Expr modExpr(Expr arg, int mod) {
6769 arg = rem .getLeftOperand ( ) and
6870 rem .getRightOperand ( ) .( CompileTimeConstantExpr ) .getIntValue ( ) = mod and
6971 mod >= 2
70- ) or
72+ )
73+ or
7174 exists ( CompileTimeConstantExpr c |
72- mod = 2 .pow ( [ 1 .. 30 ] ) and
75+ mod = 2 .pow ( [ 1 .. 30 ] ) and
7376 c .getIntValue ( ) = mod - 1 and
7477 result .( AndBitwiseExpr ) .hasOperands ( arg , c )
75- ) or
78+ )
79+ or
7680 result .( ParExpr ) .getExpr ( ) = modExpr ( arg , mod )
7781}
7882
@@ -88,7 +92,9 @@ private Guard moduloCheck(SsaVariable v, int val, int mod, boolean testIsTrue) {
8892 (
8993 testIsTrue = polarity and val = r
9094 or
91- testIsTrue = polarity .booleanNot ( ) and mod = 2 and val = 1 - r and
95+ testIsTrue = polarity .booleanNot ( ) and
96+ mod = 2 and
97+ val = 1 - r and
9298 ( r = 0 or r = 1 )
9399 )
94100 )
@@ -109,17 +115,22 @@ private predicate moduloGuardedRead(SsaVariable v, SsaReadPosition pos, int val,
109115bindingset [ mask]
110116private predicate andmaskFactor ( int mask , int factor ) {
111117 mask % factor = 0 and
112- factor = 2 .pow ( [ 1 .. 30 ] )
118+ factor = 2 .pow ( [ 1 .. 30 ] )
113119}
114120
115121/** Holds if `e` is evenly divisible by `factor`. */
116122private predicate evenlyDivisibleExpr ( Expr e , int factor ) {
117123 exists ( ConstantIntegerExpr c , int k | k = c .getIntValue ( ) |
118- e .( MulExpr ) .getAnOperand ( ) = c and factor = k .abs ( ) and factor >= 2 or
119- e .( AssignMulExpr ) .getSource ( ) = c and factor = k .abs ( ) and factor >= 2 or
120- e .( LShiftExpr ) .getRightOperand ( ) = c and factor = 2 .pow ( k ) and k > 0 or
121- e .( AssignLShiftExpr ) .getRhs ( ) = c and factor = 2 .pow ( k ) and k > 0 or
122- e .( AndBitwiseExpr ) .getAnOperand ( ) = c and factor = max ( int f | andmaskFactor ( k , f ) ) or
124+ e .( MulExpr ) .getAnOperand ( ) = c and factor = k .abs ( ) and factor >= 2
125+ or
126+ e .( AssignMulExpr ) .getSource ( ) = c and factor = k .abs ( ) and factor >= 2
127+ or
128+ e .( LShiftExpr ) .getRightOperand ( ) = c and factor = 2 .pow ( k ) and k > 0
129+ or
130+ e .( AssignLShiftExpr ) .getRhs ( ) = c and factor = 2 .pow ( k ) and k > 0
131+ or
132+ e .( AndBitwiseExpr ) .getAnOperand ( ) = c and factor = max ( int f | andmaskFactor ( k , f ) )
133+ or
123134 e .( AssignAndExpr ) .getSource ( ) = c and factor = max ( int f | andmaskFactor ( k , f ) )
124135 )
125136}
@@ -134,9 +145,17 @@ private int getId(BasicBlock bb) { idOf(bb, result) }
134145 * Holds if `inp` is an input to `phi` along `edge` and this input has index `r`
135146 * in an arbitrary 1-based numbering of the input edges to `phi`.
136147 */
137- private predicate rankedPhiInput ( SsaPhiNode phi , SsaVariable inp , SsaReadPositionPhiInputEdge edge , int r ) {
148+ private predicate rankedPhiInput (
149+ SsaPhiNode phi , SsaVariable inp , SsaReadPositionPhiInputEdge edge , int r
150+ ) {
138151 edge .phiInput ( phi , inp ) and
139- edge = rank [ r ] ( SsaReadPositionPhiInputEdge e | e .phiInput ( phi , _) | e order by getId ( e .getOrigBlock ( ) ) )
152+ edge = rank [ r ] ( SsaReadPositionPhiInputEdge e |
153+ e .phiInput ( phi , _)
154+ |
155+ e
156+ order by
157+ getId ( e .getOrigBlock ( ) )
158+ )
140159}
141160
142161/**
@@ -154,9 +173,11 @@ private int gcdLim() { result = 128 }
154173 */
155174private int gcd ( int x , int y ) {
156175 result != 1 and
157- result = x .abs ( ) and y = 0 and x in [ - gcdLim ( ) ..gcdLim ( ) ]
176+ result = x .abs ( ) and
177+ y = 0 and
178+ x in [ - gcdLim ( ) .. gcdLim ( ) ]
158179 or
159- result = gcd ( y , x % y ) and y != 0 and x in [ - gcdLim ( ) .. gcdLim ( ) ]
180+ result = gcd ( y , x % y ) and y != 0 and x in [ - gcdLim ( ) .. gcdLim ( ) ]
160181}
161182
162183/**
@@ -167,14 +188,17 @@ private int gcd(int x, int y) {
167188 */
168189bindingset [ val, mod]
169190private int remainder ( int val , int mod ) {
170- mod = 0 and result = val or
191+ mod = 0 and result = val
192+ or
171193 mod > 1 and result = ( ( val % mod ) + mod ) % mod
172194}
173195
174196/**
175197 * Holds if `inp` is an input to `phi` and equals `phi` modulo `mod` along `edge`.
176198 */
177- private predicate phiSelfModulus ( SsaPhiNode phi , SsaVariable inp , SsaReadPositionPhiInputEdge edge , int mod ) {
199+ private predicate phiSelfModulus (
200+ SsaPhiNode phi , SsaVariable inp , SsaReadPositionPhiInputEdge edge , int mod
201+ ) {
178202 exists ( SsaBound phibound , int v , int m |
179203 edge .phiInput ( phi , inp ) and
180204 phibound .getSsa ( ) = phi and
@@ -204,7 +228,7 @@ private predicate phiModulusRankStep(SsaPhiNode phi, Bound b, int val, int mod,
204228 exists ( SsaVariable inp , SsaReadPositionPhiInputEdge edge , int v1 , int m1 |
205229 mod != 1 and
206230 val = remainder ( v1 , mod )
207- |
231+ |
208232 exists ( int v2 , int m2 |
209233 rankedPhiInput ( phi , inp , edge , rix ) and
210234 phiModulusRankStep ( phi , b , v1 , m1 , rix - 1 ) and
@@ -257,36 +281,43 @@ private predicate ssaModulus(SsaVariable v, SsaReadPosition pos, Bound b, int va
257281 */
258282cached
259283predicate exprModulus ( Expr e , Bound b , int val , int mod ) {
260- e = b .getExpr ( val ) and mod = 0 or
261- evenlyDivisibleExpr ( e , mod ) and val = 0 and b instanceof ZeroBound or
284+ e = b .getExpr ( val ) and mod = 0
285+ or
286+ evenlyDivisibleExpr ( e , mod ) and val = 0 and b instanceof ZeroBound
287+ or
262288 exists ( SsaVariable v , SsaReadPositionBlock bb |
263289 ssaModulus ( v , bb , b , val , mod ) and
264290 e = v .getAUse ( ) and
265291 bb .getBlock ( ) = e .getBasicBlock ( )
266- ) or
292+ )
293+ or
267294 exists ( Expr mid , int val0 , int delta |
268295 exprModulus ( mid , b , val0 , mod ) and
269296 valueFlowStep ( e , mid , delta ) and
270297 val = remainder ( val0 + delta , mod )
271- ) or
298+ )
299+ or
272300 exists ( ConditionalExpr cond , int v1 , int v2 , int m1 , int m2 |
273301 cond = e and
274302 condExprBranchModulus ( cond , true , b , v1 , m1 ) and
275303 condExprBranchModulus ( cond , false , b , v2 , m2 ) and
276304 mod = gcd ( gcd ( m1 , m2 ) , v1 - v2 ) and
277305 mod != 1 and
278306 val = remainder ( v1 , mod )
279- ) or
307+ )
308+ or
280309 exists ( Bound b1 , Bound b2 , int v1 , int v2 , int m1 , int m2 |
281310 addModulus ( e , true , b1 , v1 , m1 ) and
282311 addModulus ( e , false , b2 , v2 , m2 ) and
283312 mod = gcd ( m1 , m2 ) and
284313 mod != 1 and
285314 val = remainder ( v1 + v2 , mod )
286- |
287- b = b1 and b2 instanceof ZeroBound or
315+ |
316+ b = b1 and b2 instanceof ZeroBound
317+ or
288318 b = b2 and b1 instanceof ZeroBound
289- ) or
319+ )
320+ or
290321 exists ( int v1 , int v2 , int m1 , int m2 |
291322 subModulus ( e , true , b , v1 , m1 ) and
292323 subModulus ( e , false , any ( ZeroBound zb ) , v2 , m2 ) and
@@ -296,25 +327,24 @@ predicate exprModulus(Expr e, Bound b, int val, int mod) {
296327 )
297328}
298329
299- private predicate condExprBranchModulus ( ConditionalExpr cond , boolean branch , Bound b , int val , int mod ) {
300- exprModulus ( cond .getTrueExpr ( ) , b , val , mod ) and branch = true or
330+ private predicate condExprBranchModulus (
331+ ConditionalExpr cond , boolean branch , Bound b , int val , int mod
332+ ) {
333+ exprModulus ( cond .getTrueExpr ( ) , b , val , mod ) and branch = true
334+ or
301335 exprModulus ( cond .getFalseExpr ( ) , b , val , mod ) and branch = false
302336}
303337
304338private predicate addModulus ( Expr add , boolean isLeft , Bound b , int val , int mod ) {
305- exists ( Expr larg , Expr rarg |
306- nonConstAddition ( add , larg , rarg )
307- |
339+ exists ( Expr larg , Expr rarg | nonConstAddition ( add , larg , rarg ) |
308340 exprModulus ( larg , b , val , mod ) and isLeft = true
309341 or
310342 exprModulus ( rarg , b , val , mod ) and isLeft = false
311343 )
312344}
313345
314346private predicate subModulus ( Expr sub , boolean isLeft , Bound b , int val , int mod ) {
315- exists ( Expr larg , Expr rarg |
316- nonConstSubtraction ( sub , larg , rarg )
317- |
347+ exists ( Expr larg , Expr rarg | nonConstSubtraction ( sub , larg , rarg ) |
318348 exprModulus ( larg , b , val , mod ) and isLeft = true
319349 or
320350 exprModulus ( rarg , b , val , mod ) and isLeft = false
0 commit comments