incorrectly branching into cheatcode call during cse summarization

[ovatman]

When applying cse kontrol produces a #cheatcode_call branch due to a possible misinterpretation of a symoblic variable when applying #checkCall.
To reproduce, perform the following, using kontrol 1.0.25

1. Use the UniswapV2 variant from here; a part of the Pi^2 solidity semantic development project. This file contains multiple contracts.
2. Initialize a foundry project and place the test contract in a separate test directory. In my case all the other contracts reside in a single file under src and the uniswapV2SwapTest was under test
3. forge test and kontrol build
4. We will try to get a summary of the uniswapV2Pair.sync() function so run kontrol prove --match-test 'uniswapV2Pair.sync()' --break-on-calls --cse

Should fail as follows:

  Failure reason:
    Matching failed.
    The following cells failed matching individually (antecedent #Implies consequent):
    K_CELL: #cheatcode_error selector ( "balanceOf(address)" ) #buf ( 32 , C_UNISWAPV2PAIR_ID:Int )
    ~> #cheatcode_return 128 32
    ~> #pc [ CALL ]
    ~> #execute #Implies #halt ~> .K
    ~> CONTINUATION:K

6. After failure, issue kontrol show 'uniswapV2Pair.sync()'

Following is the related part from kcfg

├─ 5
│   k: #checkCall C_UNISWAPV2PAIR_ID:Int 0 ~> #call C_UNISWAPV2PAIR_ID:Int C_UNISWAPV2P ...
│   pc: 2313
│   callDepth: CALLDEPTH_CELL:Int
│   statusCode: STATUSCODE:StatusCode
│   src: src/UniswapV2Swap.sol:290:290
│   method: src%uniswapV2Pair.sync()
┃
┃ (1 step)
┣━━┓
┃  │
┃  ├─ 6
┃  │   k: #cheatcode_call selector ( "balanceOf(address)" ) #buf ( 32 , C_UNISWAPV2PAIR_ID ...
┃  │   pc: 2313
┃  │   callDepth: CALLDEPTH_CELL:Int
┃  │   statusCode: STATUSCODE:StatusCode
┃  │   src: src/UniswapV2Swap.sol:290:290
┃  │   method: src%uniswapV2Pair.sync()
┃  │
┃  │  (1 step)
┃  └─ 8 (stuck, leaf)
┃      k: #cheatcode_error selector ( "balanceOf(address)" ) #buf ( 32 , C_UNISWAPV2PAIR_I ...
┃      pc: 2313
┃      callDepth: CALLDEPTH_CELL:Int
┃      statusCode: CHEATCODE_UNIMPLEMENTED
┃      src: src/UniswapV2Swap.sol:290:290
┃      method: src%uniswapV2Pair.sync()

[PetarMax]

This is strange, because (I think) this means that C_UNISWAPV2PAIR_ID does not have the constraint that it's different from the cheatcode account address. We normally put this constraint in. @ovatman, what is the full configuration you see in node 5?

[ovatman]

@PetarMax I don't have this constraint. Here's the full conf of node 5 (cropping some parts for brevity):

( <generatedTop>
  <foundry>
    <kevm>
      <k>
        #checkCall C_UNISWAPV2PAIR_ID:Int 0
        ~> #call C_UNISWAPV2PAIR_ID:Int C_UNISWAPV2PAIR_TOKEN0_ID:Int C_UNISWAPV2PAIR_TOKEN0_ID:Int 0 0 b"p\xa0\x821" +Bytes #buf ( 32 , C_UNISWAPV2PAIR_ID:Int ) false
        ~> #return 128 32
        ~> #pc [ CALL ]
        ~> #execute
        ~> CONTINUATION:K
      </k>
      ...
      <ethereum>
        <evm>
          <callState>
             ...
            <id>
              C_UNISWAPV2PAIR_ID:Int
            </id>
            <caller>
              CALLER_ID:Int
            </caller>
            <callData>
              b"\xff\xf6\xca\xe9"
            </callData>
            <callValue>
              0
            </callValue>
            <wordStack>
              ( 164 : ( selector ( "balanceOf(address)" ) : ( C_UNISWAPV2PAIR_TOKEN0_ID:Int : ( 3471 : ( 373 : ( selector ( "sync()" ) : .WordStack ) ) ) ) ) )
            </wordStack>
            <localMem>
              b"\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x80\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00p\xa0\x821" +Bytes #buf ( 32 , C_UNISWAPV2PAIR_ID:Int )
            </localMem>
            ...
          </callState>
          <substate>
            <refund>
              0
            </refund>
            <accessedAccounts>
              ACCESSEDACCOUNTS_CELL:Set |Set SetItem ( C_UNISWAPV2PAIR_TOKEN0_ID:Int )
            </accessedAccounts>
            ...
          </substate>
            ...
          </block>
          ...
        </evm>
        <network>
          <accounts>
            ( <account>
              <acctID>
                C_UNISWAPV2PAIR_ID:Int
              </acctID>
              <balance>
                C_UNISWAPV2PAIR_BAL:Int
              </balance>
              <code>
                src%uniswapV2Pair
              </code>
              <storage>
                ( ( 0 |-> C_UNISWAPV2PAIR_TOKEN0_ID:Int )
                ( ( 1 |-> C_UNISWAPV2PAIR_TOKEN1_ID:Int )
                C_UNISWAPV2PAIR_STORAGE:Map ) )
              </storage>
              <nonce>
                C_UNISWAPV2PAIR_NONCE:Int
              </nonce>
              ...
            </account>
            ACCOUNTS_REST:AccountCellMap )
          </accounts>
          ...
        </network>
      </ethereum>
      ...
    </kevm>
    <cheatcodes>
      ...
    </cheatcodes>
    <KEVMTracing>
      ...
    </KEVMTracing>
  </foundry>
  ...
</generatedTop>
#And ( { true #Equals 0 <=Int CALLER_ID:Int }
#And ( { true #Equals 0 <=Int ORIGIN_ID:Int }
#And ( { true #Equals pow24 <Int NUMBER_CELL:Int }
#And ( { true #Equals 0 <=Int C_UNISWAPV2PAIR_ID:Int }
#And ( { true #Equals 0 <=Int C_UNISWAPV2PAIR_BAL:Int }
#And ( { true #Equals NUMBER_CELL:Int <Int pow32 }
#And ( { true #Equals 0 <=Int C_UNISWAPV2PAIR_NONCE:Int }
#And ( { true #Equals 1073741824 <Int TIMESTAMP_CELL:Int }
#And ( { true #Equals TIMESTAMP_CELL:Int <Int 34359738368 }
#And ( { true #Equals 0 <=Int C_UNISWAPV2PAIR_TOKEN0_ID:Int }
#And ( { true #Equals 0 <=Int C_UNISWAPV2PAIR_TOKEN1_ID:Int }
#And ( { true #Equals C_UNISWAPV2PAIR_NONCE:Int <Int maxUInt64 }
#And ( { true #Equals CALLER_ID:Int <Int pow160 }
#And ( { true #Equals ORIGIN_ID:Int <Int pow160 }
#And ( { true #Equals C_UNISWAPV2PAIR_ID:Int <Int pow160 }
#And ( { true #Equals C_UNISWAPV2PAIR_TOKEN0_ID:Int <Int pow160 }
#And ( { true #Equals C_UNISWAPV2PAIR_TOKEN1_ID:Int <Int pow160 }
#And ( { true #Equals C_UNISWAPV2PAIR_BAL:Int <Int pow256 }
#And ( { true #Equals ( notBool 0 in_keys ( C_UNISWAPV2PAIR_STORAGE:Map ) ) }
#And ( { true #Equals ( notBool 1 in_keys ( C_UNISWAPV2PAIR_STORAGE:Map ) ) }
#And ( { true #Equals ( notBool CALLER_ID:Int ==Int 645326474426547203313410069153905908525362434349 ) }
#And ( { true #Equals ( notBool ORIGIN_ID:Int ==Int 645326474426547203313410069153905908525362434349 ) }
#And ( { true #Equals ( notBool C_UNISWAPV2PAIR_ID:Int ==Int 645326474426547203313410069153905908525362434349 ) }
#And ( { true #Equals ( notBool <acctID> C_UNISWAPV2PAIR_ID:Int </acctID> in_keys ( ACCOUNTS_REST:AccountCellMap ) ) }
#And ( { true #Equals ( notBool #range ( 0 < CALLER_ID:Int <= 9 ) ) }
#And ( { true #Equals ( notBool #range ( 0 < ORIGIN_ID:Int <= 9 ) ) }
#And { true #Equals ( notBool #range ( 0 < C_UNISWAPV2PAIR_ID:Int <= 9 ) ) } ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) )

[PetarMax]

Ok, thank you, could you please give me the configuration of node 6 as well?

[PetarMax]

#And ( { true #Equals ( notBool C_UNISWAPV2PAIR_ID:Int ==Int 645326474426547203313410069153905908525362434349 ) }

is there, which should prevent the branching...

[PetarMax]

@palinatolmach When summarising a function, if one of the parameters is an address, I think that we need to assume that it does not equal the cheatcode account address.

[palinatolmach]

Agreed @PetarMax, I'll open an issue and a PR for it later today. Should we do it for an address/contract function parameter, or an address/contract field, or both? Probably both?

[PetarMax]

Both, I think.

[palinatolmach]

Thanks! Opened and assigned myself: #827.