crytic / slither

Static Analyzer for Solidity and Vyper
https://blog.trailofbits.com/2018/10/19/slither-a-solidity-static-analysis-framework/
GNU Affero General Public License v3.0
5.23k stars 954 forks source link

[Bug]: Incorrect SSA form with break #2509

Open smonicas opened 1 month ago

smonicas commented 1 month ago

Describe the issue:

The SSA form returns s_3 and p_3 instead of s_2 and p_2 which are correctly returned if the break is removed.

Code example to reproduce the issue:

contract T {
 function a(uint n) public returns(uint,uint){
   uint s = 0;
   uint p = 0;

   for (uint i; i < n; i++) {
     s += i;
     p *= i;
     if (i == 3) { break; }
   }
   return (s, p);
 }
}

Version:

0.10.3

Relevant log output:

Function T.a(uint256)
        Expression: s = 0
        IRs:
            s_1(uint256) := 0(uint256)
        Expression: p = 0
        IRs:
            p_1(uint256) := 0(uint256)
        Expression: i < n
        IRs:
            s_2(uint256) := ϕ(['s_3', 's_1'])
            p_2(uint256) := ϕ(['p_1', 'p_3'])
            i_1(uint256) := ϕ(['i_0', 'i_2'])
            TMP_0(bool) = i_1 < n_1
            CONDITION TMP_0
        Expression: s += i
        IRs:
            s_3(uint256) = s_2 (c)+ i_1
        Expression: p *= i
        IRs:
            p_3(uint256) = p_2 (c)* i_1
        Expression: i == 3
        IRs:
            TMP_1(bool) = i_1 == 3
            CONDITION TMP_1
        Expression: i ++
        IRs:
            TMP_2(uint256) := i_1(uint256)
            i_2(uint256) = i_1 (c)+ 1
        Expression: (s,p)
        IRs:
            RETURN s_3,p_3
0xalpharush commented 1 month ago

Is the CFG and dominator graph correct?