@@ -11,10 +11,8 @@ public partial class CfgAbstractInterpretation<N,D>
1111 {
1212 /// <summary>
1313 /// Abstract interpretation execution environment.
14- /// The default execution performed is based on a dfs algorithm, with exception that
15- /// branching instructions are handled specifically.
16- /// Thus not all execution paths are applied, but all nodes are visited using dfs like algorithm if they are accessible.
17- /// A node cannot be visited twice.
14+ /// The default execution performed is based on a dfs algorithm with an execution threshold on cyclic transition.
15+ /// This method only works on CFG graph emitted with an Extended or WithDfa mode.
1816 /// </summary>
1917 public class Environment
2018 {
@@ -31,15 +29,15 @@ public class Environment
3129 /// <summary>
3230 /// The DFS Run stack
3331 /// </summary>
34- private Stack < BasicBlock < N , D > > _dfsStack ;
32+ private Stack < BasicBlock < N , D > > _dfsStack ;
3533 /// <summary>
3634 /// Bit Vector to check if metric values have been taken in account for a block index.
3735 /// </summary>
3836 private System . Collections . BitArray _metricUpdated ;
3937 /// <summary>
4038 /// Current Cyclic execution Threshold by block index.
4139 /// </summary>
42- private Dictionary < int , int > _cyclicThreshold ;
40+ private Dictionary < int , int > _cyclicThreshold ;
4341 /// <summary>
4442 /// The Cyclic transition from one block index to another block index
4543 /// </summary>
@@ -143,9 +141,9 @@ void dfs(int a)
143141 if ( _nb == 0 )
144142 { // Block 'b' is not visited yet => traverse it
145143 dfs ( b ) ;
144+ _nb = Visited ( b ) ;
146145 }
147- int _na = Visited ( a ) ;
148- _nb = Visited ( b ) ;
146+ int _na = Visited ( a ) ;
149147 if ( _nb < _na )
150148 { // This mean that the transition from block 'a' to block 'b' leads to a cycle.
151149 _cyclicThreshold [ b ] = _cyclicExecutionThreshold ;
@@ -161,7 +159,7 @@ void dfs(int a)
161159 if ( na == d )
162160 {
163161 do
164- { // Close any block that belongs to a cycle from block 'a' has considered.
162+ { // Close any block that belongs to a cycle from block 'a' as considered.
165163 _N [ _stack . Peek ( ) ] = Int32 . MaxValue ;
166164 } while ( _stack . Count > 0 && _stack . Pop ( ) != a ) ;
167165 }
0 commit comments