[SMTChecker]: document currently unsupported features

[PaulRBerg]

Page

SMTChecker.

Issue Description

I've recently started using the SMTChecker on a code base that uses many of the modern Solidity features, and I was disappointed to see that many features are not yet supported. To share just a few examples:

warning[7650]: Warning: Assertion checker does not yet support this expression.
   --> src/SablierV2LockupLinear.sol:370:17:
    |
370 |             if (recipient.code.length > 0) {
    |                 ^^^^^^^^^^^^^^

The above is the .code member of the address type.

Then:

warning[8364]: Warning: Assertion checker does not yet implement type type(struct LockupLinear.Stream storage pointer)
   --> src/SablierV2LockupLinear.sol:419:30:
    |
419 |         _streams[streamId] = LockupLinear.Stream({
    |                              ^^^^^^^^^^^^^^^^^^^

Here, I am not sure what is not supported: structs defined in libraries, assignments to mappings, or the Struct({ key: val }) style of initialing structs?

warning[7650]: Warning: Assertion checker does not yet support this expression.
   --> src/SablierV2LockupLinear.sol:419:30:
    |
419 |         _streams[streamId] = LockupLinear.Stream({
    |                          

Ditto.

Documentation Request

Given the above, it would be helpful to add a new section in the SMTChecker documentation page that would outline the list of currently unsupported features of the compiler.

[leonardoalt]

Yea, that makes sense. To clarify the specific examples you gave:

1. recipient.code isn't supported precisely because it's a runtime value, but it does get its own symbolic variable. I'm not sure what kind of properties you'd be able to write about it though.

2. The struct warning looks like it's referring to the type itself which at a quick glance looks like a false positive in warning that. Structs themselves and their constructors are supported (except for recursive structs), but storage references are tricky and many things related to references are unsupported.

[PaulRBerg]

Thanks for the clarifications, Leo.

I'm not sure what kind of properties you'd be able to write about it though

I was not interested in writing any assertions about it - it's moreso a question of user experience, i.e. I was lead to believe that the property verifications are impaired by this warning, so maybe the compiler could add a clarificatory note add at the end of a report with many warnings like this? e.g. something like "in spite of the many warnings above, the verification succeeded" (in the successful case).

The struct warning looks like it's referring to the type itself which at a quick glance looks like a false positive in warning that

Interesting! This is how the struct is defined:

library LockupLinear {
    struct Stream {
        Lockup.Amounts amounts;
        Range range;
        address sender
        bool isCancelable;
        Lockup.Status status;
        IERC20 asset;
    }
}

Is this a bug in the SMTChecker then?

[leonardoalt]

I was not interested in writing any assertions about it - it's moreso a question of user experience, i.e. I was lead to believe that the property verifications are impaired by this warning

That may be the case, but yea the warning is rather general.

, so maybe the compiler could add a clarificatory note add at the end of a report with many warnings like this? e.g. something like "in spite of the many warnings above, the verification succeeded" (in the successful case).

That's great feedback, thanks! We do have an issue that's going to be worked on soon (https://github.com/ethereum/solidity/issues/11703) to first of all group all the "unsupported" messages into a single one, similarly to how it's currently done for unproven targets, with a flag to expand on it if the user is interested. The final information that the verification was successful is also a good idea.

Is this a bug in the SMTChecker then?

Yea it does look like a bug, the struct itself should be supported so the message looks wrong to me.

[PaulRBerg]

group all the "unsupported" messages into a single one

This would be great!

with a flag to expand on it if the user is interested

And this, too.

it does look like a bug, the struct itself should be supported so the message looks wrong to me.

Good, thanks for confirming. I will try to reproduce it and I will open an issue if I succeed.