@@ -7,12 +7,21 @@ module BaseSsa {
77 private import AssignableDefinitions
88 private import codeql.ssa.Ssa as SsaImplCommon
99
10+ cached
11+ private module BaseSsaStage {
12+ cached
13+ predicate ref ( ) { any ( ) }
14+
15+ cached
16+ predicate backref ( ) { ( exists ( any ( SsaDefinition def ) .getARead ( ) ) implies any ( ) ) }
17+ }
18+
1019 /**
1120 * Holds if the `i`th node of basic block `bb` is assignable definition `def`,
1221 * targeting local scope variable `v`.
1322 */
1423 private predicate definitionAt (
15- AssignableDefinition def , BasicBlock bb , int i , SsaInput :: SourceVariable v
24+ AssignableDefinition def , BasicBlock bb , int i , SsaImplInput :: SourceVariable v
1625 ) {
1726 bb .getNode ( i ) = def .getExpr ( ) .getControlFlowNode ( ) and
1827 v = def .getTarget ( ) and
@@ -24,7 +33,7 @@ module BaseSsa {
2433 )
2534 }
2635
27- private predicate implicitEntryDef ( Callable c , EntryBasicBlock bb , SsaInput :: SourceVariable v ) {
36+ private predicate entryDef ( Callable c , BasicBlock bb , SsaImplInput :: SourceVariable v ) {
2837 exists ( EntryBasicBlock entry |
2938 c = entry .getEnclosingCallable ( ) and
3039 // In case `c` has multiple bodies, we want each body to get its own implicit
@@ -79,16 +88,17 @@ module BaseSsa {
7988 }
8089 }
8190
82- private module SsaInput implements SsaImplCommon:: InputSig< Location , BasicBlock > {
91+ private module SsaImplInput implements SsaImplCommon:: InputSig< Location , BasicBlock > {
8392 class SourceVariable = SimpleLocalScopeVariable ;
8493
8594 predicate variableWrite ( BasicBlock bb , int i , SourceVariable v , boolean certain ) {
95+ BaseSsaStage:: ref ( ) and
8696 exists ( AssignableDefinition def |
8797 definitionAt ( def , bb , i , v ) and
8898 if def .isCertain ( ) then certain = true else certain = false
8999 )
90100 or
91- implicitEntryDef ( _, bb , v ) and
101+ entryDef ( _, bb , v ) and
92102 i = - 1 and
93103 certain = true
94104 }
@@ -102,54 +112,35 @@ module BaseSsa {
102112 }
103113 }
104114
105- private module SsaImpl = SsaImplCommon:: Make< Location , Cfg , SsaInput > ;
115+ private module SsaImpl = SsaImplCommon:: Make< Location , Cfg , SsaImplInput > ;
106116
107- class Definition extends SsaImpl:: Definition {
108- final AssignableRead getARead ( ) {
109- exists ( BasicBlock bb , int i |
110- SsaImpl:: ssaDefReachesRead ( _, this , bb , i ) and
111- result .getControlFlowNode ( ) = bb .getNode ( i )
112- )
113- }
117+ private module SsaInput implements SsaImpl:: SsaInputSig {
118+ private import csharp as CS
114119
115- final AssignableDefinition getDefinition ( ) {
116- exists ( BasicBlock bb , int i , SsaInput:: SourceVariable v |
117- this .definesAt ( v , bb , i ) and
118- definitionAt ( result , bb , i , v )
119- )
120- }
120+ class Expr = CS:: Expr ;
121121
122- final predicate isImplicitEntryDefinition ( SsaInput:: SourceVariable v ) {
123- exists ( BasicBlock bb |
124- this .definesAt ( v , bb , - 1 ) and
125- implicitEntryDef ( _, bb , v )
126- )
127- }
122+ class Parameter = CS:: Parameter ;
128123
129- private Definition getAPhiInputOrPriorDefinition ( ) {
130- result = this .( PhiNode ) . getAnInput ( ) or
131- SsaImpl :: uncertainWriteDefinitionInput ( this , result )
132- }
124+ class VariableWrite extends AssignableDefinition {
125+ Expr asExpr ( ) { result = this .getExpr ( ) }
126+
127+ Expr getValue ( ) { result = this . getSource ( ) }
133128
134- final Definition getAnUltimateDefinition ( ) {
135- result = this .getAPhiInputOrPriorDefinition * ( ) and
136- not result instanceof PhiNode
129+ predicate isParameterInit ( Parameter p ) {
130+ this .( ImplicitParameterDefinition ) . getParameter ( ) = p
131+ }
137132 }
138133
139- override Location getLocation ( ) {
140- result = this . getDefinition ( ) . getLocation ( )
134+ predicate explicitWrite ( VariableWrite w , BasicBlock bb , int i , SsaImplInput :: SourceVariable v ) {
135+ definitionAt ( w , bb , i , v )
141136 or
142- exists ( Callable c , BasicBlock bb , SsaInput:: SourceVariable v |
143- this .definesAt ( v , bb , - 1 ) and
144- implicitEntryDef ( c , bb , v ) and
145- result = c .getLocation ( )
146- )
137+ entryDef ( _, bb , v ) and
138+ i = - 1 and
139+ w .isParameterInit ( v )
147140 }
148141 }
149142
150- class PhiNode extends SsaImpl:: PhiNode , Definition {
151- override Location getLocation ( ) { result = this .getBasicBlock ( ) .getLocation ( ) }
143+ module Ssa = SsaImpl:: MakeSsa< SsaInput > ;
152144
153- final Definition getAnInput ( ) { SsaImpl:: phiHasInputFromBlock ( this , result , _) }
154- }
145+ import Ssa
155146}
0 commit comments