11private import java as J
2+ private import SemanticBound
23private import SemanticCFG
34private import SemanticExpr
4- private import SemanticCFGSpecific
5+ private import SemanticGuard
56private import SemanticSSA
67private import SemanticType
78private import semmle.code.java.dataflow.SSA as SSA
9+ private import semmle.code.java.dataflow.internal.rangeanalysis.SsaReadPositionCommon as SsaRead
10+ private import semmle.code.java.dataflow.Bound as JBound
11+ private import semmle.code.java.controlflow.Guards as JGuards
12+ private import semmle.code.java.controlflow.internal.GuardsLogic as JGuardsLogic
813
914private module Impl {
1015 newtype TExpr =
@@ -23,12 +28,14 @@ private module Impl {
2328module SemanticExprConfig {
2429 private import Impl
2530
31+ class Location = J:: Location ;
32+
2633 class Expr extends TExpr {
2734 string toString ( ) { none ( ) }
2835
29- J :: Location getLocation ( ) { none ( ) }
36+ Location getLocation ( ) { none ( ) }
3037
31- J :: BasicBlock getBasicBlock ( ) { none ( ) }
38+ BasicBlock getBasicBlock ( ) { none ( ) }
3239 }
3340
3441 private class PrimaryExpr extends Expr , TPrimaryExpr {
@@ -38,9 +45,9 @@ module SemanticExprConfig {
3845
3946 override string toString ( ) { result = e .toString ( ) }
4047
41- override J :: Location getLocation ( ) { result = e .getLocation ( ) }
48+ override Location getLocation ( ) { result = e .getLocation ( ) }
4249
43- override J :: BasicBlock getBasicBlock ( ) { result = e .getBasicBlock ( ) }
50+ override BasicBlock getBasicBlock ( ) { result = e .getBasicBlock ( ) }
4451
4552 J:: Expr getExpr ( ) { result = e }
4653 }
@@ -52,9 +59,9 @@ module SemanticExprConfig {
5259
5360 override string toString ( ) { result = "post-update for " + e .toString ( ) }
5461
55- override J :: Location getLocation ( ) { result = e .getLocation ( ) }
62+ override Location getLocation ( ) { result = e .getLocation ( ) }
5663
57- override J :: BasicBlock getBasicBlock ( ) { result = e .getBasicBlock ( ) }
64+ override BasicBlock getBasicBlock ( ) { result = e .getBasicBlock ( ) }
5865
5966 J:: UnaryAssignExpr getExpr ( ) { result = e }
6067 }
@@ -66,9 +73,9 @@ module SemanticExprConfig {
6673
6774 override string toString ( ) { result = "init of " + for .getVariable ( ) .toString ( ) }
6875
69- override J :: Location getLocation ( ) { result = for .getVariable ( ) .getLocation ( ) }
76+ override Location getLocation ( ) { result = for .getVariable ( ) .getLocation ( ) }
7077
71- override J :: BasicBlock getBasicBlock ( ) { result = for .getVariable ( ) .getBasicBlock ( ) }
78+ override BasicBlock getBasicBlock ( ) { result = for .getVariable ( ) .getBasicBlock ( ) }
7279 }
7380
7481 private class ParameterInitExpr extends Expr , TParameterInit {
@@ -79,16 +86,16 @@ module SemanticExprConfig {
7986
8087 override string toString ( ) { result = "param init: " + init .toString ( ) }
8188
82- override J :: Location getLocation ( ) { result = init .getLocation ( ) }
89+ override Location getLocation ( ) { result = init .getLocation ( ) }
8390
84- override J :: BasicBlock getBasicBlock ( ) { result = init .getBasicBlock ( ) }
91+ override BasicBlock getBasicBlock ( ) { result = init .getBasicBlock ( ) }
8592
8693 final J:: Parameter getParameter ( ) { result = param }
8794 }
8895
8996 string exprToString ( Expr e ) { result = e .toString ( ) }
9097
91- J :: Location getExprLocation ( Expr e ) { result = e .getLocation ( ) }
98+ Location getExprLocation ( Expr e ) { result = e .getLocation ( ) }
9299
93100 SemBasicBlock getExprBasicBlock ( Expr e ) { result = getSemanticBasicBlock ( e .getBasicBlock ( ) ) }
94101
@@ -306,6 +313,143 @@ module SemanticExprConfig {
306313 result = getSemanticType ( for .getVariable ( ) .getType ( ) )
307314 )
308315 }
316+
317+ class BasicBlock instanceof J:: BasicBlock {
318+ final string toString ( ) { result = super .toString ( ) }
319+
320+ final Location getLocation ( ) { result = super .getLocation ( ) }
321+ }
322+
323+ predicate bbDominates ( BasicBlock dominator , BasicBlock dominated ) {
324+ dominator .( J:: BasicBlock ) .bbDominates ( dominated .( J:: BasicBlock ) )
325+ }
326+
327+ predicate hasDominanceInformation ( BasicBlock block ) { J:: hasDominanceInformation ( block ) }
328+
329+ class SsaVariable instanceof SSA:: SsaVariable {
330+ final string toString ( ) { result = super .toString ( ) }
331+
332+ final Location getLocation ( ) { result = super .getLocation ( ) }
333+ }
334+
335+ predicate explicitUpdate ( SsaVariable v , SemType type , Expr sourceExpr ) {
336+ exists ( SSA:: SsaExplicitUpdate update | v = update |
337+ type = getSemanticType ( update .getSourceVariable ( ) .getType ( ) ) and
338+ exists ( J:: Expr expr | expr = update .getDefiningExpr ( ) |
339+ (
340+ expr instanceof J:: Assignment or
341+ expr instanceof J:: PreIncExpr or
342+ expr instanceof J:: PreDecExpr
343+ ) and
344+ sourceExpr = getResultExpr ( expr )
345+ or
346+ sourceExpr = getResultExpr ( expr .( J:: LocalVariableDeclExpr ) .getInit ( ) )
347+ or
348+ ( expr instanceof J:: PostIncExpr or expr instanceof J:: PostDecExpr ) and
349+ sourceExpr = TPostUpdateExpr ( expr )
350+ or
351+ exists ( J:: EnhancedForStmt for |
352+ for .getVariable ( ) = expr and
353+ sourceExpr = TEnhancedForInit ( for )
354+ )
355+ )
356+ )
357+ }
358+
359+ predicate phi ( SsaVariable v , SemType type ) {
360+ type = getSemanticType ( v .( SSA:: SsaPhiNode ) .getSourceVariable ( ) .getType ( ) )
361+ }
362+
363+ SsaVariable getAPhiInput ( SsaVariable v ) { result = v .( SSA:: SsaPhiNode ) .getAPhiInput ( ) }
364+
365+ Expr getAUse ( SsaVariable v ) { result = getResultExpr ( v .( SSA:: SsaVariable ) .getAUse ( ) ) }
366+
367+ BasicBlock getSsaVariableBasicBlock ( SsaVariable v ) {
368+ result = v .( SSA:: SsaVariable ) .getBasicBlock ( )
369+ }
370+
371+ class SsaReadPosition instanceof SsaRead:: SsaReadPosition {
372+ final string toString ( ) { result = super .toString ( ) }
373+
374+ Location getLocation ( ) { none ( ) }
375+ }
376+
377+ private class SsaReadPositionBlock extends SsaReadPosition {
378+ SsaRead:: SsaReadPositionBlock block ;
379+
380+ SsaReadPositionBlock ( ) { this = block }
381+
382+ final override Location getLocation ( ) { result = block .getBlock ( ) .getLocation ( ) }
383+ }
384+
385+ private class SsaReadPositionPhiInputEdge extends SsaReadPosition {
386+ SsaRead:: SsaReadPositionPhiInputEdge edge ;
387+
388+ SsaReadPositionPhiInputEdge ( ) { this = edge }
389+
390+ final override Location getLocation ( ) { result = edge .getPhiBlock ( ) .getLocation ( ) }
391+ }
392+
393+ predicate hasReadOfSsaVariable ( SsaReadPosition pos , SsaVariable v ) {
394+ pos .( SsaRead:: SsaReadPosition ) .hasReadOfVar ( v )
395+ }
396+
397+ predicate readBlock ( SsaReadPosition pos , BasicBlock block ) {
398+ block = pos .( SsaRead:: SsaReadPositionBlock ) .getBlock ( )
399+ }
400+
401+ predicate phiInputEdge ( SsaReadPosition pos , BasicBlock origBlock , BasicBlock phiBlock ) {
402+ exists ( SsaRead:: SsaReadPositionPhiInputEdge readBlock | readBlock = pos |
403+ origBlock = readBlock .getOrigBlock ( ) and
404+ phiBlock = readBlock .getPhiBlock ( )
405+ )
406+ }
407+
408+ predicate phiInput ( SsaReadPosition pos , SsaVariable phi , SsaVariable input ) {
409+ pos .( SsaRead:: SsaReadPositionPhiInputEdge ) .phiInput ( phi , input )
410+ }
411+
412+ class Bound instanceof JBound:: Bound {
413+ final string toString ( ) { result = super .toString ( ) }
414+
415+ final Location getLocation ( ) { result = super .getExpr ( ) .getLocation ( ) }
416+ }
417+
418+ predicate zeroBound ( Bound bound ) { bound instanceof JBound:: ZeroBound }
419+
420+ predicate ssaBound ( Bound bound , SsaVariable v ) { v = bound .( JBound:: SsaBound ) .getSsa ( ) }
421+
422+ Expr getBoundExpr ( Bound bound , int delta ) {
423+ result = getResultExpr ( bound .( JBound:: Bound ) .getExpr ( delta ) )
424+ }
425+
426+ class Guard instanceof JGuards:: Guard {
427+ final string toString ( ) { result = super .toString ( ) }
428+
429+ final Location getLocation ( ) { result = super .getLocation ( ) }
430+ }
431+
432+ predicate guard ( Guard guard , BasicBlock block ) { block = guard .( JGuards:: Guard ) .getBasicBlock ( ) }
433+
434+ Expr getGuardAsExpr ( Guard guard ) { result = getResultExpr ( guard .( J:: Expr ) ) }
435+
436+ predicate equalityGuard ( Guard guard , Expr e1 , Expr e2 , boolean polarity ) {
437+ guard .( JGuards:: Guard ) .isEquality ( getJavaExpr ( e1 ) , getJavaExpr ( e2 ) , polarity )
438+ }
439+
440+ predicate guardDirectlyControlsBlock ( Guard guard , BasicBlock controlled , boolean branch ) {
441+ guard .( JGuards:: Guard ) .directlyControls ( controlled , branch )
442+ }
443+
444+ predicate guardHasBranchEdge ( Guard guard , BasicBlock bb1 , BasicBlock bb2 , boolean branch ) {
445+ guard .( JGuards:: Guard ) .hasBranchEdge ( bb1 , bb2 , branch )
446+ }
447+
448+ Guard comparisonGuard ( Expr e ) { result = getJavaExpr ( e ) .( J:: ComparisonExpr ) }
449+
450+ predicate implies_v2 ( Guard g1 , boolean b1 , Guard g2 , boolean b2 ) {
451+ JGuardsLogic:: implies_v2 ( g1 , b1 , g2 , b2 )
452+ }
309453}
310454
311455private import Impl
@@ -314,25 +458,22 @@ SemExpr getSemanticExpr(J::Expr javaExpr) { result = TPrimaryExpr(javaExpr) }
314458
315459J:: Expr getJavaExpr ( SemExpr e ) { e = getSemanticExpr ( result ) }
316460
317- SemExpr getUpdateExpr ( SSA:: SsaExplicitUpdate update ) {
318- exists ( J:: Expr expr | expr = update .getDefiningExpr ( ) |
319- (
320- expr instanceof J:: Assignment or
321- expr instanceof J:: PreIncExpr or
322- expr instanceof J:: PreDecExpr
323- ) and
324- result = getResultExpr ( expr )
325- or
326- result = getResultExpr ( expr .( J:: LocalVariableDeclExpr ) .getInit ( ) )
327- or
328- ( expr instanceof J:: PostIncExpr or expr instanceof J:: PostDecExpr ) and
329- result = TPostUpdateExpr ( expr )
330- or
331- exists ( J:: EnhancedForStmt for |
332- for .getVariable ( ) = expr and
333- result = TEnhancedForInit ( for )
334- )
335- )
336- }
337-
338461SemExpr getEnhancedForInitExpr ( J:: EnhancedForStmt for ) { result = TEnhancedForInit ( for ) }
462+
463+ SemBasicBlock getSemanticBasicBlock ( J:: BasicBlock block ) { result = block }
464+
465+ J:: BasicBlock getJavaBasicBlock ( SemBasicBlock block ) { block = getSemanticBasicBlock ( result ) }
466+
467+ SemSsaVariable getSemanticSsaVariable ( SSA:: SsaVariable v ) { result = v }
468+
469+ SSA:: SsaVariable getJavaSsaVariable ( SemSsaVariable v ) { v = getSemanticSsaVariable ( result ) }
470+
471+ SemSsaReadPosition getSemanticSsaReadPosition ( SsaRead:: SsaReadPosition pos ) { result = pos }
472+
473+ SemBound getSemanticBound ( JBound:: Bound bound ) { result = bound }
474+
475+ JBound:: Bound getJavaBound ( SemBound bound ) { bound = getSemanticBound ( result ) }
476+
477+ SemGuard getSemanticGuard ( JGuards:: Guard guard ) { result = guard }
478+
479+ JGuards:: Guard getJavaGuard ( SemGuard guard ) { guard = getSemanticGuard ( result ) }
0 commit comments