Make state Abstract after a CALL to unknown code -- or better yet, analyze what can change

[msooseth]

When executing an equivalence check against

0x5f3560e01c6002600b820660011b61046301601e395f51565b633ce828de81186103fa573461045f57602061003460406103fe565b6040f35b631d1dc1f081186100dd57600254801561045f57803404905060405260405161006160606103fe565b6060511061045f5760035f546020525f5260405f20805460405180820382811161045f57905090508155506003336020525f5260405f20805460405180820182811061045f5790509050815550337fe3d4187f6ca4248660cc0ac8b8056515bac4a8132be2eca31d6d0cc170722a7e60405160605260206060a2005b63961be39181186103fa573461045f574760405260206040f35b63eeb4663481186101305760243610341761045f576004358060a01c61045f57606052602060605160405261012c6080610411565b6080f35b630dca59c181186103fa573461045f57602061014c6060610425565b6060f35b639104c81e81186102405760243610341761045f576004351561045f576004353360405261017e6060610411565b6060511061045f5760043560025480820281158383830414171561045f5790509050471061045f576003336020525f5260405f20805460043580820382811161045f579050905081555060035f546020525f5260405f20805460043580820182811061045f57905090508155505f5f5f5f60043560025480820281158383830414171561045f5790509050335ff11561045f57337f5e5e995ce3133561afceaa51a9a154d5db228cd7525d34df5185582c18d3df0960043560605260206060a2005b63a035b1fe81186103fa573461045f5760025460405260206040f35b637f59e53481186103fa5760443610341761045f576004358060a01c61045f576060526024351561045f57602435336040526102986080610411565b6080511061045f576003336020525f5260405f20805460243580820382811161045f579050905081555060036060516020525f5260405f20805460243580820182811061045f5790509050815550606051337fddf252ad1be2c89b69c2b068fc378daa952ba7f163c4a11628f55a4df523b3ef60243560805260206080a3005b632293448781186103fa5760443610341761045f576004358060a01c61045f576040525f54331861045f57602435471061045f575f5f5f5f6024356040515ff11561045f576040517f357b676c439b9e49b4410f8eb8680bee4223724802d8e3fd422e1756f87b475f60243560605260206060a2005b63ad11c13181186103fa573461045f57476103a96060610425565b60605180820382811161045f579050905060805260206080f35b636904c94d81186103fa573461045f575f5460405260206040f35b633a98ef3981186103fa573461045f5760015460405260206040f35b5f5ffd5b60035f546020525f5260405f2054815250565b60036040516020525f5260405f2054815250565b60015461043260406103fe565b60405180820382811161045f579050905060025480820281158383830414171561045f5790509050815250565b5f80fd00f703de001803fa003801500318038e025c03c303fa

0x6002600b5f3560e01c90810660011b61040101601e929192395f51565b505b5f5ffd5b636904c94d1861001e57346103fd575f5460405260206040f35b637f59e5341861001e573660441134176103fd576004358060a01c6103fd5760243580156103fd57336040528060806100736103b5565b608051106103fd573360035f5260205260405f208054808390039081116103fd5790558160035f5260205260405f2080548083019081106103fd57905560a052337fddf252ad1be2c89b69c2b068fc378daa952ba7f163c4a11628f55a4df523b3ef602060a0a3005b63ad11c1311861001e57346103fd57478060606100f76103c9565b60605190039081116103fd5760805260206080f35b63229344871861001e573660441134176103fd576004358060a01c6103fd575f5433186103fd576024358047106103fd575f5f5f5f84865ff1156103fd576060527f357b676c439b9e49b4410f8eb8680bee4223724802d8e3fd422e1756f87b475f60206060a2005b80639104c81e1861025557503660241134176103fd5760043580156103fd57336040528060606101a36103b5565b606051106103fd576002548015908290808402908104909114909117156103fd5747106103fd573360035f5260205260405f208054808390039081116103fd5790555f5460035f5260205260405f2080548083019081106103fd5790556002548015908290808402908104909114909117156103fd575f905f905f905f90335ff1156103fd57608052337f5e5e995ce3133561afceaa51a9a154d5db228cd7525d34df5185582c18d3df0960206080a2005b63a035b1fe1861001e57346103fd5760025460405260206040f35b80631d1dc1f0186102fc575060025480156103fd5734048060606102926103a2565b606051106103fd575f5460035f5260205260405f208054808390039081116103fd5790553360035f5260205260405f2080548083019081106103fd579055608052337fe3d4187f6ca4248660cc0ac8b8056515bac4a8132be2eca31d6d0cc170722a7e60206080a2005b63961be3911861001e57346103fd574760405260206040f35b633ce828de1861001e57346103fd57604061032e6103a2565b60206040f35b633a98ef391861001e57346103fd5760015460405260206040f35b8063eeb466341861038357503660241134176103fd576004358060a01c6103fd57604052608061037d6103b5565b60206080f35b630dca59c11861001e57346103fd57606061039c6103c9565b60206060f35b905f5460035f5260205260405f20549052565b9060405160035f5260205260405f20549052565b906001548060406103d86103a2565b60405190039081116103fd5760025480159082908093029283041417156103fd579052565b5f80fd034f03340315001c02700175010c00dc003c0022001c

We get:

     - Unexpected Symbolic Arguments to Opcode
       msg: "trying to access a symbolic address that isn't already present in storage"
       opcode: CALL
       program counter: 524
       arguments:
         (SymAddr "caller")

Due to payment transfer, which actually calls the contract, and may execute the receive() function -- which may lead to reentrancy. So the warning is valid. There are two ways to go around this:

• set the state fully Abstract. This is a huge over-approximation, and may lead to a lot of false positives. But it works
• as above, but ONLY set the parts abstract that can actually change, given the current state. This requires the current state being executed with an abstract calldata, checking all observed potential state changes, and making those values abstract. This can be quite refined (down to bits) or quite coarse (entire blocks of memory & state).

I think we should start with (1) and then move slowly towards (2), as time permits.

--

Side-note: due to dynamic jumps, the above code is actually kinda tricky to execute, but the dynamic jump issues have been resolved thanks to #643 and #652 So funnily enough, they are not a problem at all.

[msooseth]

#658 will hopefully "fix" this to the point where we at least approximate with the restriction of "no reentrancy guaranteed". Proper analysis andsetting of (some parts of the) state to symbolic is needed to do this properly. It will also need an explanation as per #666