search

ethereum / solidity

Solidity, the Smart Contract Programming Language
https://soliditylang.org
GNU General Public License v3.0
22.64k stars 5.61k forks source link

SMTChecker: Fix internal compiler error on reporting proved targets #15205

Closed pgebal closed 1 week ago

pgebal commented 1 week ago

Closes https://github.com/ethereum/solidity/issues/15188 Closes https://github.com/ethereum/solidity/issues/15113

We used UniqueErrorLogger for reporting proved targets, which requires pair (error code, source location) to be unique. I replaced that with a regular ErrorLogger.

blishko commented 1 week ago

What would happen if we remove m_uniqueErrorReporter from ModelChecker and just use the ErrorReporter passed from CompilerStack (so we do not have to add another ErrorReporter)? Where would we run into problem with duplicates?

pgebal commented 1 week ago

What would happen if we remove m_uniqueErrorReporter from ModelChecker and just use the ErrorReporter passed from CompilerStack (so we do not have to add another ErrorReporter)? Where would we run into problem with duplicates?

I'll double check that, but I almost sure I've seen CHC reporting some failed targets twice.

blishko commented 1 week ago

I'll double check that, but I almost sure I've seen CHC reporting some failed targets twice.

That's interesting. I would expect the same behaviour for safe and unsafe targets.

cameel commented 1 week ago

The unique reporter was added in #11850 (which was meant to address #11597). See the description:

The SMTChecker generates a lot of redundant "unsupported" warnings, because it visits every contract separately in its own context, with 2 different engines. So for example if a contract that is inherited by 2 contracts has some assembly in it, we're going to see the message "inline assembly unsupported" possibly 6 times: each time a contract is visited, by each engine.

blishko commented 1 week ago

@pgebal, I checked and you were right that in certain situations, we would emit a warning multiple times for the same source code location without UniqueErrorReporter. For example, assertion violation in a parent contract in the presence of inheritance.

There is a possibility to maybe be more efficient in these scenarios. For example, if the assertion can be violated in the context of one contract, we do not need to check it again in the context of another contract. But then one must consider also the case where the assertion is safe in the context of one contract, but can be violated in the context of another contract.

Let's go with your fix now, and we can maybe revisit this later. Can you just remove the unnecessary field in SMTEncoder? Or maybe you can do it the other way around? Only have it in SMTEncoder and not add again in BMC and CHC?

pgebal commented 1 week ago

@pgebal, I checked and you were right that in certain situations, we would emit a warning multiple times for the same source code location without UniqueErrorReporter. For example, assertion violation in a parent contract in the presence of inheritance.

There is a possibility to maybe be more efficient in these scenarios. For example, if the assertion can be violated in the context of one contract, we do not need to check it again in the context of another contract. But then one must consider also the case where the assertion is safe in the context of one contract, but can be violated in the context of another contract.

Let's go with your fix now, and we can maybe revisit this later. Can you just remove the unnecessary field in SMTEncoder? Or maybe you can do it the other way around? Only have it in SMTEncoder and not add again in BMC and CHC?

Actually, we have it only in the SMTEncoder. Sorry for misleading comment I posted earlier. I think the PR is ready for a merge