Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Add support for ABI types #1883

Merged
merged 89 commits into from
Aug 17, 2023
Merged

Add support for ABI types #1883

merged 89 commits into from
Aug 17, 2023

Conversation

iFrostizz
Copy link
Contributor

@iFrostizz iFrostizz commented Jun 2, 2023

Advances towards a fix for: runtimeverification/kontrol#55

ref: https://solidity-fr.readthedocs.io/fr/latest/abi-spec.html#types

  • Refactor
  • bytes<M> support
  • dynamic / fixed length arrays support
  • fixed point (this one is parsed but not supported, Solidity itself has a very limited support for it at the moment)

@iFrostizz iFrostizz self-assigned this Jun 7, 2023
@iFrostizz
Copy link
Contributor Author

iFrostizz commented Aug 17, 2023

Status of this PR:
We first planned to support arrays but got issues to create arbitrary size arrays because existentials are not permitted in decorators in K. I would need help to support those.

   rule  ( CounterTest . testArray ( V0_numbers : uint256[] ) => #abiCallData ( "testArray", #array ( V0_numbers , ?SIZE , ?ARRAY ) , .TypedArgs ) )
      ensures #rangeUInt ( 128 , ?SIZE )
        Location(60,126,60,132)
        60 |        rule  ( CounterTest . testArray ( V0_numbers : uint256[] ) =>
#abiCallData ( "testArray" , #array ( V0_numbers , ?SIZE , ?ARRAY ) ,
.TypedArgs ) )
           .
                                                   ^~~~~~
[Error] Compiler: Cannot encode equations with existential variables to KORE.
 If this is desired, please use #Exists with regular variables.
 Offending variables: [?SIZE, ?ARRAY]

So what was done instead:

  • Support all static bytes1..32 variants
  • Support all static signed ints int8..256 variants

We still need to support:

  • Dynamic arrays
  • Fixed length arrays
  • Two dimensional arrays (including static arrays or dynamic for one dimension)
  • Structs

@rv-jenkins rv-jenkins merged commit 2be4f95 into master Aug 17, 2023
@rv-jenkins rv-jenkins deleted the dynamic-types branch August 17, 2023 14:24
iFrostizz added a commit that referenced this pull request Aug 28, 2023
* add static bytes

* support dynamic arrays

* anticipate fixed point type

* Set Version: 1.0.195

* kevm-pyk/: sync poetry files

* support fixed len array

* bytes equivalent to string

* forgotten import

* merge master

* Set Version: 1.0.202

* back out changes

* Set Version: 1.0.205

* deps/: back out changes

* deps/: back out changes

* Set Version: 1.0.210

* ci passes

* Set Version: 1.0.211

* use macos-13 and format

* start array support

* update kvariable array

* Add signed integer support beyond int256

* Set Version: 1.0.215

* update array exception

* Set Version: 1.0.216

* Set Version: 1.0.217

* Set Version: 1.0.219

* Set Version: 1.0.220

* Set Version: 1.0.242

* deps/: back out changes

* only suppport static types

* filter out dynamic arrays

* only support static type *minus* static arrays

* remove redundant test

* Set Version: 1.0.243

* Set Version: 1.0.244

* remove unused function

* Set Version: 1.0.245

* update uint to bytes

* Set Version: 1.0.246

* Set Version: 1.0.246

* better comparison

* Set Version: 1.0.256

* add range_predicate tests

* Set Version: 1.0.257

* add solc_to_k unit test

* add uint24 variant

* Set Version: 1.0.257

* update int types test

* Set Version: 1.0.261

* back out poetry

* deps/: back out changes

* back out

* Set Version: 1.0.261

* merge master

* add int sort

* update expected kompiled

* update int and new bytes<M> variants

* format

* Set Version: 1.0.262

* update import

* back out

* add SInt variants

* write all min/max SInt variants

* add Word for SInt variants

* make minSInt aliases

* Set Version: 1.0.263

* Set Version: 1.0.263

* update expected output

---------

Co-authored-by: François Guyot <[email protected]>
Co-authored-by: devops <[email protected]>
Co-authored-by: Noah Watson <[email protected]>
Co-authored-by: Noah Watson <[email protected]>
Co-authored-by: Andrei Văcaru <[email protected]>
Co-authored-by: Andrei <[email protected]>
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Projects
None yet
Development

Successfully merging this pull request may close these issues.

Unsuported evm base sort type: int128
5 participants