Solidity: SMTChecker throws InternalCompilerError

[elenadimitrova]

Description

InternalCompilerError on SMTChecker compilation of Colony contracts from https://github.com/JoinColony/colonyNetwork/contracts

A couple of examples below

$ solc ./contracts/ColonyTask.sol --allow-paths lib/dappsys/*.sol
Internal compiler error during compilation:
/Users/Elena/Source/solidity/libsolidity/formal/SMTChecker.cpp(1622): Throw in function smt::Expression dev::solidity::SMTChecker::currentValue(const dev::solidity::VariableDeclaration &)
Dynamic exception type: boost::wrapexcept<langutil::InternalCompilerError>
std::exception::what:
[dev::tag_comment*] =

$ solc ./contracts/ColonyNetworkAuction.sol --allow-paths lib/dappsys/*.sol
Internal compiler error during compilation:
/Users/Elena/Source/solidity/libsolidity/formal/SMTChecker.cpp(1622): Throw in function smt::Expression dev::solidity::SMTChecker::currentValue(const dev::solidity::VariableDeclaration &)
Dynamic exception type: boost::wrapexcept<langutil::InternalCompilerError>
std::exception::what:
[dev::tag_comment*] =

And a successful run with a contract that has no imports:

$ solc ./contracts/ColonyNetworkDataTypes.sol --allow-paths lib/dappsys/*.sol
Compiler run successful, no output requested.

Environment

• Compiler version: 0.5.8
• Target EVM version (as per compiler settings): (default)
• Framework/IDE (e.g. Truffle or Remix): truffle compile also errors, originally logged this issue with them https://github.com/trufflesuite/truffle/issues/2132 but upon further analysis it's coming from the compiler.
• EVM execution environment / backend / blockchain client:
• Operating system: OSX

Steps to Reproduce

I am keeping a log of the steps taken so far to enable the SMTChecker on the Colony contracts here https://github.com/JoinColony/colonyNetwork/issues/547

[leonardoalt]

Hi @elenadimitrova , thanks for reporting. It's nice to know that more projects are trying out the SMTChecker.
I ran your example and actually got a different error, I'll need to debug a bit more.

[leonardoalt]

Simplified code that triggers the bug, two files:

// one.sol
library L {
    uint constant one = 1;
    function f() internal pure returns (uint) {
        return one;
    }
}

pragma experimental SMTChecker;

import 'one.sol';

contract C {
    function g(uint x) public pure {
        uint y = L.f();
        assert(x > y);
    }
}

The cause of the bug is that state variables in imported code are not handled properly. If the library and the contract are in the same file it works fine.

[leonardoalt]

I've found multiple bugs in the SMTChecker while fixing this one. Will create separate issues/PRs for each one.

• [x] State vars from another source https://github.com/ethereum/solidity/issues/7162
• [x] Unsupported compound assignment inside branch breaks SSA https://github.com/ethereum/solidity/issues/7163
• [x] Unsupported type as element of returned tuple https://github.com/ethereum/solidity/issues/7164
• [x] StringLiteral type mismatch https://github.com/ethereum/solidity/issues/7165
• [x] Scanner from different source causes ICE when retrieving models https://github.com/ethereum/solidity/issues/7168

[leonardoalt]

After all the bugs above were fixed I ran
solc ./contracts/ColonyTask.sol --allow-paths lib/dappsys/*.sol
and didn't see any more bugs, so closing this one.