@@ -12,7 +12,7 @@ module BaseSsa {
1212 * targeting local scope variable `v`.
1313 */
1414 private predicate definitionAt (
15- AssignableDefinition def , BasicBlock bb , int i , SsaInput :: SourceVariable v
15+ AssignableDefinition def , BasicBlock bb , int i , SsaImplInput :: SourceVariable v
1616 ) {
1717 bb .getNode ( i ) = def .getExpr ( ) .getControlFlowNode ( ) and
1818 v = def .getTarget ( ) and
@@ -24,7 +24,7 @@ module BaseSsa {
2424 )
2525 }
2626
27- private predicate implicitEntryDef ( Callable c , EntryBasicBlock bb , SsaInput :: SourceVariable v ) {
27+ private predicate entryDef ( Callable c , EntryBasicBlock bb , SsaImplInput :: SourceVariable v ) {
2828 exists ( EntryBasicBlock entry |
2929 c = entry .getEnclosingCallable ( ) and
3030 // In case `c` has multiple bodies, we want each body to get its own implicit
@@ -79,7 +79,7 @@ module BaseSsa {
7979 }
8080 }
8181
82- private module SsaInput implements SsaImplCommon:: InputSig< Location , BasicBlock > {
82+ private module SsaImplInput implements SsaImplCommon:: InputSig< Location , BasicBlock > {
8383 class SourceVariable = SimpleLocalScopeVariable ;
8484
8585 predicate variableWrite ( BasicBlock bb , int i , SourceVariable v , boolean certain ) {
@@ -88,7 +88,7 @@ module BaseSsa {
8888 if def .isCertain ( ) then certain = true else certain = false
8989 )
9090 or
91- implicitEntryDef ( _, bb , v ) and
91+ entryDef ( _, bb , v ) and
9292 i = - 1 and
9393 certain = true
9494 }
@@ -102,7 +102,37 @@ module BaseSsa {
102102 }
103103 }
104104
105- private module SsaImpl = SsaImplCommon:: Make< Location , Cfg , SsaInput > ;
105+ private module SsaImpl = SsaImplCommon:: Make< Location , Cfg , SsaImplInput > ;
106+
107+ private module SsaInput implements SsaImpl:: SsaInputSig {
108+ private import csharp as CS
109+
110+ class Expr = CS:: Expr ;
111+
112+ class Parameter = CS:: Parameter ;
113+
114+ class VariableWrite extends AssignableDefinition {
115+ Expr asExpr ( ) { result = this .getExpr ( ) }
116+
117+ Expr getValue ( ) { result = this .getSource ( ) }
118+
119+ predicate isParameterInit ( Parameter p ) {
120+ this .( ImplicitParameterDefinition ) .getParameter ( ) = p
121+ }
122+ }
123+
124+ predicate explicitWrite ( VariableWrite w , BasicBlock bb , int i , SsaImplInput:: SourceVariable v ) {
125+ definitionAt ( w , bb , i , v )
126+ or
127+ entryDef ( _, bb , v ) and
128+ i = - 1 and
129+ w .isParameterInit ( v )
130+ }
131+ }
132+
133+ module Ssa = SsaImpl:: MakeSsa< SsaInput > ;
134+
135+ import Ssa
106136
107137 class Definition extends SsaImpl:: Definition {
108138 final AssignableRead getARead ( ) {
@@ -113,16 +143,16 @@ module BaseSsa {
113143 }
114144
115145 final AssignableDefinition getDefinition ( ) {
116- exists ( BasicBlock bb , int i , SsaInput :: SourceVariable v |
146+ exists ( BasicBlock bb , int i , SsaImplInput :: SourceVariable v |
117147 this .definesAt ( v , bb , i ) and
118148 definitionAt ( result , bb , i , v )
119149 )
120150 }
121151
122- final predicate isImplicitEntryDefinition ( SsaInput :: SourceVariable v ) {
152+ final predicate isImplicitEntryDefinition ( SsaImplInput :: SourceVariable v ) {
123153 exists ( BasicBlock bb |
124154 this .definesAt ( v , bb , - 1 ) and
125- implicitEntryDef ( _, bb , v )
155+ entryDef ( _, bb , v )
126156 )
127157 }
128158
@@ -139,9 +169,9 @@ module BaseSsa {
139169 override Location getLocation ( ) {
140170 result = this .getDefinition ( ) .getLocation ( )
141171 or
142- exists ( Callable c , BasicBlock bb , SsaInput :: SourceVariable v |
172+ exists ( Callable c , BasicBlock bb , SsaImplInput :: SourceVariable v |
143173 this .definesAt ( v , bb , - 1 ) and
144- implicitEntryDef ( c , bb , v ) and
174+ entryDef ( c , bb , v ) and
145175 result = c .getLocation ( )
146176 )
147177 }
0 commit comments