search

microsoft / verisol

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

Inline assembly workaround; fix for the "using for" bug for struct select #243

Closed ellab123 closed 4 years ago

ellab123 commented 4 years ago

With this feature a function that contains an inline assembly is translated into a procedure with no implementation, which generates a non-deterministic result. Related regression test is Assembly1.sol.

This PR also fixes issue #71, see comment from ellab on Jan. 14th inside issue #71; related regression test is UsingInTwoLibraries.sol.

shuvendu-lahiri commented 4 years ago

Proposed fix for #242

ellab123 commented 4 years ago

Because apparently “bytes” type is not treated properly as an array in z[0].

corral.txt: __SolToBoogieTest_out.bpl(129,25): Error: invalid type for argument 0 in map select: int (expected: Ref) 1 type checking errors in __SolToBoogieTest_out.bpl

var M_int_int: [Ref][int]int; var z_Test: [Ref]int; … assert ((M_int_int[z_Test[this]][0]) == (0)); // line 129

I suspect the problem is probably related to the issues #97 and #49.

Ella

From: Shuvendu Lahiri notifications@github.com Sent: Monday, February 24, 2020 1:02 PM To: microsoft/verisol verisol@noreply.github.com Cc: Ella Bounimova ellab@microsoft.com; Author author@noreply.github.com Subject: Re: [microsoft/verisol] Inline assembly workaround: generate a function with no implementation (#243)

@shuvendu-lahiri commented on this pull request.

In Test/regressions/StringToBytes.solhttps://nam06.safelinks.protection.outlook.com/?url=https%3A%2F%2Fgithub.com%2Fmicrosoft%2Fverisol%2Fpull%2F243%23discussion_r383511911&data=02%7C01%7Cellab%40microsoft.com%7Cd109989fa789467744f108d7b96cc4a1%7C72f988bf86f141af91ab2d7cd011db47%7C1%7C0%7C637181749113619331&sdata=D7C%2B%2B1igRFWedyx8uotiYeZX3HMeozvmw1%2F5XfBfDgw%3D&reserved=0:

@@ -30,8 +30,9 @@ contract Test {

     z = foo(bytes(""));           //compiles

     //assert (z == bytes(""));      //solc error

     //assert (z == 0x0);             //solc error

I don't recall why this assert was removed. Do you?

— You are receiving this because you authored the thread. Reply to this email directly, view it on GitHubhttps://nam06.safelinks.protection.outlook.com/?url=https%3A%2F%2Fgithub.com%2Fmicrosoft%2Fverisol%2Fpull%2F243%3Femail_source%3Dnotifications%26email_token%3DADDTNE5WUKRPL2SQWHB76UTREQYT3A5CNFSM4KZKDWI2YY3PNVWWK3TUL52HS4DFWFIHK3DMKJSXC5LFON2FEZLWNFSXPKTDN5WW2ZLOORPWSZGOCWWZMBQ%23pullrequestreview-363697670&data=02%7C01%7Cellab%40microsoft.com%7Cd109989fa789467744f108d7b96cc4a1%7C72f988bf86f141af91ab2d7cd011db47%7C1%7C0%7C637181749113629327&sdata=Zwz%2B0cCgkuPdfqCchH8mFcNfRv6P4TT5jZqArfTl6Q0%3D&reserved=0, or unsubscribehttps://nam06.safelinks.protection.outlook.com/?url=https%3A%2F%2Fgithub.com%2Fnotifications%2Funsubscribe-auth%2FADDTNEZ4ZOA5GKASUTQBZB3REQYT3ANCNFSM4KZKDWIQ&data=02%7C01%7Cellab%40microsoft.com%7Cd109989fa789467744f108d7b96cc4a1%7C72f988bf86f141af91ab2d7cd011db47%7C1%7C0%7C637181749113629327&sdata=Y3RzVS9BzaZqfNLEqlwF8wtbXvRtuocRIyOkcPQ59Qs%3D&reserved=0.