Unknown exception during compilation for 0.5.12 and 0.5.13

sunbeomso commented 4 years ago

Description

The released versions of solc (0.5.12+commit.7709ece9.Linux.g++ and 0.5.13+commit.5b0b510c.Linux.g++) often produce errors when compiling contracts. The produced error messages are: Unknown exception during compilation.

Indeed, I haven't seen any successful cases for the above two released versions.

I have checked the solc version 0.5.11+commit.22be8592.Linux.g++ successfully compiles several contracts.

Environment

Compiler version: 0.5.12+commit.7709ece9.Linux.g++, 0.5.13+commit.5b0b510c.Linux.g++ where both of them were built from source.
Target EVM version (as per compiler settings): N/A
Framework/IDE (e.g. Truffle or Remix): N/A
EVM execution environment / backend / blockchain client: N/A
Operating system: Ubuntu 18.04.2

Steps to Reproduce

Simply can be reproduced by typing: solc FILENAME

For example, solc 0.5.13 produces the error message above when compiling the contract below: https://etherscan.io/address/0x3a19a99c715a3bddc66c74d68b32f2a85244a5b5#code

Also, solc 0.5.12 generates the error for the contract below: https://etherscan.io/address/0xf44ea500abd7d4fb8b0bc5c42002e0eb58d0eb42#code

axic commented 4 years ago

solc 0.5.13 produces the error message above when compiling the contract below: https://etherscan.io/address/0x3a19a99c715a3bddc66c74d68b32f2a85244a5b5#code

According to etherscan this was verified with 0.5.13. Are you sure it doesn't compile with 0.5.13?

Also, solc 0.5.12 generates the error for the contract below: https://etherscan.io/address/0xf44ea500abd7d4fb8b0bc5c42002e0eb58d0eb42#code

Likewise, etherscan claims to have verified this with 0.5.12

sunbeomso commented 4 years ago

@axic I intentionally provided such examples. Did you get successful results? At least for me, the two solc versions failed. As I mentioned above, I have not observed cases where the two versions successfully compile contracts.

chriseth commented 4 years ago

@SunBeomSo did you build the compiler from source on your system or did you use a binary? Does the error message provide any further details about the internal error? If not, can you re-compile in debug mode (cmake -DCMAKE_BUILD_TYPE=Debug ..) and check with gdb where there exception is thrown? Thanks a lot!

sunbeomso commented 4 years ago

@chriseth

did you build the compiler from source on your system or did you use a binary?

I built from released versions of source code.

Does the error message provide any further details about the internal error?

The entire messages were Unknown exception during compilation. There were no further details.

can you re-compile in debug mode (cmake -DCMAKE_BUILD_TYPE=Debug ..) and check with gdb where there exception is thrown?

I am not familiar with gdb but I would try.

chriseth commented 4 years ago

Thanks!

gdb --args solc filename.sol
catch throw
run
# wait for exception
bt

sunbeomso commented 4 years ago

@chriseth With solc 0.5.13 built from source with debug mode, the command run produces:

[Thread debugging using libthread_db enabled]
Using host libthread_db library "/lib/x86_64-linux-gnu/libthread_db.so.1".

and the command bt produces:

#0  0x00007ffff506fced in __cxa_throw () from /usr/lib/x86_64-linux-gnu/libstdc++.so.6
#1  0x00007ffff78d3b1f in params::validate(param_descrs const&) () from /usr/lib/libz3.so
#2  0x00007ffff690e215 in Z3_fixedpoint_set_params () from /usr/lib/libz3.so
#3  0x00005555559383cc in z3::fixedpoint::set (this=0x55555620a210, p=...) at /usr/include/z3++.h:2397
#4  0x000055555593764d in dev::solidity::smt::Z3CHCInterface::Z3CHCInterface (this=0x55555620a1f0) at /HOME/solidity_0.5.13/libsolidity/formal/Z3CHCInterface.cpp:47
#5  0x00005555558d468f in __gnu_cxx::new_allocator<dev::solidity::smt::Z3CHCInterface>::construct<dev::solidity::smt::Z3CHCInterface> (this=0x7fffffffd297, __p=0x55555620a1f0)
    at /usr/include/c++/7/ext/new_allocator.h:136
#6  0x00005555558d42bf in std::allocator_traits<std::allocator<dev::solidity::smt::Z3CHCInterface> >::construct<dev::solidity::smt::Z3CHCInterface> (__a=..., __p=0x55555620a1f0)
    at /usr/include/c++/7/bits/alloc_traits.h:475
#7  0x00005555558d3bb2 in std::_Sp_counted_ptr_inplace<dev::solidity::smt::Z3CHCInterface, std::allocator<dev::solidity::smt::Z3CHCInterface>, (__gnu_cxx::_Lock_policy)2>::_Sp_counted_ptr_inplace<>(std::allocator<dev::solidity::smt::Z3CHCInterface>) (this=0x55555620a1e0, __a=...) at /usr/include/c++/7/bits/shared_ptr_base.h:526
#8  0x00005555558d326e in std::__shared_count<(__gnu_cxx::_Lock_policy)2>::__shared_count<dev::solidity::smt::Z3CHCInterface, std::allocator<dev::solidity::smt::Z3CHCInterface>>(std::_Sp_make_shared_tag, dev::solidity::smt::Z3CHCInterface*, std::allocator<dev::solidity::smt::Z3CHCInterface> const&) (this=0x7fffffffd3f8, __a=...)
    at /usr/include/c++/7/bits/shared_ptr_base.h:637
#9  0x00005555558d2390 in std::__shared_ptr<dev::solidity::smt::Z3CHCInterface, (__gnu_cxx::_Lock_policy)2>::__shared_ptr<std::allocator<dev::solidity::smt::Z3CHCInterface>>(std::_Sp_make_shared_tag, std::allocator<dev::solidity::smt::Z3CHCInterface> const&) (this=0x7fffffffd3f0, __tag=..., __a=...) at /usr/include/c++/7/bits/shared_ptr_base.h:1295
#10 0x00005555558d13d2 in std::shared_ptr<dev::solidity::smt::Z3CHCInterface>::shared_ptr<std::allocator<dev::solidity::smt::Z3CHCInterface>>(std::_Sp_make_shared_tag, std::allocator<dev::solidity::smt::Z3CHCInterface> const&) (this=0x7fffffffd3f0, __tag=..., __a=...) at /usr/include/c++/7/bits/shared_ptr.h:344
#11 0x00005555558d068b in std::allocate_shared<dev::solidity::smt::Z3CHCInterface, std::allocator<dev::solidity::smt::Z3CHCInterface>>(std::allocator<dev::solidity::smt::Z3CHCInterface> const&) (__a=...) at /usr/include/c++/7/bits/shared_ptr.h:691
#12 0x00005555558cf8b8 in std::make_shared<dev::solidity::smt::Z3CHCInterface> () at /usr/include/c++/7/bits/shared_ptr.h:707
#13 0x00005555558c5f11 in dev::solidity::CHC::CHC (this=0x7fffffffd950, _context=..., _errorReporter=..., _smtlib2Responses=std::map with 0 elements)
    at /HOME/solidity_0.5.13/libsolidity/formal/CHC.cpp:42
#14 0x00005555558e457d in dev::solidity::ModelChecker::ModelChecker (this=0x7fffffffd7c0, _errorReporter=..., _smtlib2Responses=std::map with 0 elements)
    at /HOME/solidity_0.5.13/libsolidity/formal/ModelChecker.cpp:28
#15 0x00005555556a58ac in dev::solidity::CompilerStack::analyze (this=0x55555618d9f0) at /HOME/solidity_0.5.13/libsolidity/interface/CompilerStack.cpp:375
#16 0x00005555556a5d6a in dev::solidity::CompilerStack::parseAndAnalyze (this=0x55555618d9f0) at /HOME/solidity_0.5.13/libsolidity/interface/CompilerStack.cpp:399
#17 0x00005555556a62bd in dev::solidity::CompilerStack::compile (this=0x55555618d9f0) at /HOME/solidity_0.5.13/libsolidity/interface/CompilerStack.cpp:431
#18 0x00005555555b6d3d in dev::solidity::CommandLineInterface::processInput (this=0x7fffffffdfb0) at /HOME/solidity_0.5.13/solc/CommandLineInterface.cpp:966
#19 0x00005555555f9678 in main (argc=2, argv=0x7fffffffe228) at /HOME/solidity_0.5.13/solc/main.cpp:59

where HOME is the home directory.

axic commented 4 years ago

@SunBeomSo what version of z3 are you using? Did you add pragma experimental SMTChecker; into the file?

cc @leonardoalt

sunbeomso commented 4 years ago

@axic

what version of z3 are you using?

ver z3 4.7.1

Did you add pragma experimental SMTChecker; into the file?

No. I didn't make any changes from the original contracts.

cc @leonardoalt

leonardoalt commented 4 years ago

I just compiled the contract with Solidity 0.5.13 and z3 4.8.6 and it works. @axic Even though the SMTChecker wasn't enabled, if solc is linked against a solver, the constructors are still called. It looks like the Z3CHCInterface constructor uses some Z3 options that didn't exist then.

@SunBeomSo could you please try with a newer z3 version? At least 4.8.1

sunbeomso commented 4 years ago

@leonardoalt With z3 4.8.7, I checked that compilations are successful. Thanks.

ethereum / solidity