search

microsoft / verisol

A formal verifier and analysis tool for Solidity Smart Contracts
Other
245 stars 46 forks source link

Partial support for delete construct (add support for deleting a dynamic array) #110

Closed garbervetsky closed 5 years ago

garbervetsky commented 5 years ago

This addresses #36

garbervetsky commented 5 years ago

Can you please add a regression, or add to the regression that has delete constructs? Also, as I understand this does not handle the full semantics of delete for nested arrays, correct?

There was already a regression DeleteArray.sol that tested delete but doesn't appear to be in the file records.txt. When I added the file I got this solidity version mismatch problem and other issues.

So I uncommented 1 line in DeleteScalar.sol. If I uncomment the next line I got:

assert (keccak256(bytes(s)) == keccak256(bytes(n[1]))); that fails. I just set array.length = 0, this assertion is requiring to clean the array. Does the spec of delete states that the array should be wiped? Do we require to add a formula stating that forall 0<=i< arrays.length => array[i] = 0?
In that case, my fix is incomplete. I can try to fix it.

And. Yes, it doesn't handle the multidimensional arrays.

garbervetsky commented 5 years ago

assert (keccak256(bytes(s)) == keccak256(bytes(n[1]))); that fails. I just set array.length = 0, this assertion is requiring to clean the array. Does the spec of delete states that the array should be wiped?

@shuvendu-lahiri why do you this assertion? An access out of bounds like n[1] should fail after performing delete n. Shouldn't it?

shuvendu-lahiri commented 5 years ago

Let me resolve the merge conflict.

garbervetsky commented 5 years ago

Looks good. Can you (a) merge from master and (b) run the regressions.

I see you already merge. Now I get an error when I try to build: /var/folders/rr/4gnbq4zn2y500zdr3lrmq59r0000gn/T/tmpbaff5cca18bf482c9741894768735f23.exec.cmd: line 2: copy: command not found

/verisol/Sources/SolToBoogie/SolToBoogie.csproj(5,5): Error MSB3073: The command "copy "/verisol/Sources/SolToBoogie//../../Tool/solc.exe" "bin/Debug/netcoreapp2.2/"" exited with code 127. (MSB3073) (SolToBoogie)

There are at least two issues:

Do you really need this in the projects SolToBoogie.csproj and SolToBoogieTest.csproj? 

  <Target Name="PostBuild" AfterTargets="PostBuildEvent">
    <Exec Command="copy &quot;$(ProjectDir)\..\..\Tool\solc.exe&quot; &quot;$(OutDir)&quot;" />
  </Target>

When I remove that from the project I can build SolToBoogie solution and 3 regressions failed.