Getting compilation error in OS X with test contracts

[nettrino]

Analysis passes for examples 1 and 2 however I am getting the following error in OS X for the leak_unsafe contract as well as a contract I want to test - is this a misconfiguration on my end? Commands are as follows: For test.sol :

./main.native -input examples/test.sol -main OCR2Aggregator -verify_timeout 60 -z3timeout 10000 -solc 0.8.0
[CHECKER] Integer Over/Underflows
[CHECKER] Division-by-zero

Solc.CompilationError
Raised at Stdlib.input_line.scan in file "stdlib.ml", line 450, characters 14-31
Called from Solc.get_json_ast in file "src/util/solc.ml", line 26, characters 19-35

and for leak_unsafe

./main.native -input examples/leak_unsafe.sol -verify_timeout 60 -z3timeout 1000
[CHECKER] Integer Over/Underflows
[CHECKER] Division-by-zero

Solc.CompilationError
Raised at Stdlib.input_line.scan in file "stdlib.ml", line 450, characters 14-31
Called from Solc.get_json_ast in file "src/util/solc.ml", line 26, characters 19-35

Please note that I have installed solc via brew and z3 via opam due to installation problems.

opam list is as follows:

# Packages matching: installed
# Name        # Installed # Synopsis
base-bigarray base
base-threads  base
base-unix     base
batteries     3.5.0       A community-maintained standard library extension
biniou        1.2.1       Binary data format designed for speed, safety, ease of use and backward compatibility as protocols evolve
conf-gmp      4           Virtual package relying on a GMP lib system installation
conf-m4       1           Virtual package relying on m4
conf-python-3 1.0.0       Virtual package relying on Python-3 installation
cppo          1.6.8       Code preprocessor like cpp for OCaml
dune          2.9.3       Fast, portable, and opinionated build system
easy-format   1.3.2       High-level and functional interface to the Format module of the OCaml standard library
num           1.4         The legacy Num library for arbitrary-precision integer and rational arithmetic
ocaml         4.12.0      The OCaml compiler (virtual package)
ocaml-config  2           OCaml Switch Configuration
ocaml-system  4.12.0      The OCaml compiler (system version, from outside of opam)
ocamlbuild    0.14.1      OCamlbuild is a build system with builtin rules to easily build most OCaml projects
ocamlfind     1.9.3       A library manager for OCaml
ocamlgraph    2.0.0       A generic graph library for OCaml
stdlib-shims  0.3.0       Backport some of the new stdlib features to older compiler
yojson        1.7.0       Yojson is an optimized parsing and printing library for the JSON format
z3            4.8.14      Z3 solver
zarith        1.12        Implements arithmetic and logical operations over arbitrary-precision integers

[sunbeomso]

Hi @nettrino. You mentioned you installed solc via brew.

Regarding this issue, please refer to the instructions mentioned in readme (the item "Specify a solc version with -solc"). The solc version that you installed and the solc version that is required to compile test contracts could be different.

Solidity contracts can be written in different versions. Thus, to use VeriSmart and SmarTest on different versions of Solidity, I recommend to obtain different versions of static binaries or build from sources, and do not recommend to install them via brew (it was hard to install different versions of Solidity via package management systems in my experience).

[sunbeomso]

In addition, please note that you ran the verification mode command on leak_unsafe.sol file, but detecting ether-leaking vulnerabilities is only valid in exploit mode in the current public version tool. For the details on -mode option, please refer to the instructions in readme.

[nettrino]

Thank you for the reply - if you see the command above I did specify the -solc option. Also I have attached a test contract (test.sol) using solidity 0.8.0 which is reporting to not passing the compilation phase although it does compile successfuly- does this pass analysis on your end?

Notice that solc --ast-compact-json test.sol works just fine but src/util/solc.ml complains that there is an error. I also tried with a static solc binary of 0.8.0 and its exactly the same behavior.

[sunbeomso]

In any cases, for the contract that you attached, your error message should not be produced if solc is located at proper locations.

Please refer to the instruction in the item "Specify a solc version with -solc" of readme. Also please check out if the version of solc identified by which solc_0.8.0 command is indeed 0.8.0 (the solc version can be checked by the command solc_0.8.0 --version).

On my machine, a following error message, which is different from the error message that you originally mentioned, is produced as the public version tool does not currently support some features in Solidity >= 0.8.0 (I will try to resolve this issue soon):

Failure("trans_yul_stmt : YulIf @ 765")
Raised at Stdlib.failwith in file "stdlib.ml", line 29, characters 17-33
Called from Translator.trans_yul_block.(fun) in file "src/frontend/translator.ml", line 582, characters 10-45
Called from Stdlib__list.fold_left in file "list.ml", line 121, characters 24-34
Called from Translator.trans_statement in file "src/frontend/translator.ml", line 657, characters 29-49
Called from Translator.trans_block.(fun) in file "src/frontend/translator.ml", line 674, characters 19-36
Called from Stdlib__list.fold_left in file "list.ml", line 121, characters 24-34
Called from Translator.trans_contractDefinition.(fun) in file "src/frontend/translator.ml", line 840, characters 58-93
Called from Stdlib__list.fold_left in file "list.ml", line 121, characters 24-34
Called from Translator.trans_contractDefinition in file "src/frontend/translator.ml", line 787, characters 4-1023
Called from Translator.translate.(fun) in file "src/frontend/translator.ml", line 926, characters 14-47
Called from Stdlib__list.fold_left in file "list.ml", line 121, characters 24-34
Called from Translator.run in file "src/frontend/translator.ml", line 930, characters 15-29
Called from Main.main in file "src/main.ml", line 67, characters 27-48
Called from Main in file "src/main.ml", line 93, characters 12-19

[nettrino]

Thanks for looking into this - the version I have is 0.8.0+commit.c7dfd78e.Darwin.appleclang

[sunbeomso]

What is the name of your solc binary file? "solc" or "solc_0.8.0"?

[sunbeomso]

Notice that solc --ast-compact-json test.sol works just fine but src/util/solc.ml complains that there is an error. I also tried with a static solc binary of 0.8.0 and its exactly the same behavior.

Based on your comment in the above, it seems that the name of your solc binary is just "solc" not "solc_0.8.0". If this is the case, you should not provide -solc option for running your test contract. That is, try the following command:

./main.native -input examples/test.sol -main OCR2Aggregator -verify_timeout 60 -z3timeout 10000

As mentioned in readme, the -solc X option is valid only when the binary named solc_X exists at directories (in my machine, /usr/local/bin) for executables:

Note that, in this case, CONTRACT.sol must be compiled with solc v.0.5.11, where the solc binary named solc_0.5.11 should be located at the path identified by which solc_0.5.11. If the -solc option is not explicitly provided, VeriSmart will attempt to compile the source code with solc binary named solc, located at the path identified by which solc.

That is, if the option -solc X is provided, VeriSmart/SmarTest tries to compile a given contract using a compiler named solc_X.

If my answer does not resolve your issue, please let me know. Also, please provide the outputs of the following commands: (1) which solc (2) solc --version (3) which solc_0.8.0 (4) solc_0.8.0 --version

[nettrino]

Thanks for the detailed response. The the solc version is here secondary - I did try with and without the solc flag and the real issue here is related to the error you were seeing as well:

Failure("trans_yul_stmt : YulIf @ 765")
Raised at Stdlib.failwith in file "stdlib.ml", line 29, characters 17-33
Called from Translator.trans_yul_block.(fun) in file "src/frontend/translator.ml", line 582, characters 10-45
Called from Stdlib__list.fold_left in file "list.ml", line 121, characters 24-34
Called from Translator.trans_statement in file "src/frontend/translator.ml", line 657, characters 29-49
Called from Translator.trans_block.(fun) in file "src/frontend/translator.ml", line 674, characters 19-36
Called from Stdlib__list.fold_left in file "list.ml", line 121, characters 24-34
Called from Translator.trans_contractDefinition.(fun) in file "src/frontend/translator.ml", line 840, characters 58-93
Called from Stdlib__list.fold_left in file "list.ml", line 121, characters 24-34
Called from Translator.trans_contractDefinition in file "src/frontend/translator.ml", line 787, characters 4-1023
Called from Translator.translate.(fun) in file "src/frontend/translator.ml", line 926, characters 14-47
Called from Stdlib__list.fold_left in file "list.ml", line 121, characters 24-34
Called from Translator.run in file "src/frontend/translator.ml", line 930, characters 15-29
Called from Main.main in file "src/main.ml", line 67, characters 27-48
Called from Main in file "src/main.ml", line 93, characters 12-19

We can close this issue since it digressed into separate threads and create a separate one just for the above or leave it open until the above is resolved - whatever works best for you!

[sunbeomso]

@nettrino

Thanks for letting me know the situation. I leave the issue open and will let you know if the secondary problem is resolved.