solc-verify reports mismatched types

[zhao-nan]

Description

When calling solc-verify.py on the example code below, it gives an error message: out/Err.sol.bpl(37,1): Error: mismatched types in assignment command (cannot assign int_arr_type to int_arr_ptr)

pragma solidity >=0.5.0 <0.6.0;

contract Thing {
    string public id;
}

contract otherThing {
    function f(Thing t)
        public view returns(string memory)
    {
        string memory s = t.id();
        return s;
    }
}

The solc compiler does not give any errors or warnings. Therefore, I think this is a bug. I also came across the very similar Error: invalid type for argument 0 in map select: int_arr_type (expected: int_arr_ptr)

Environment

• Compiler version: 0.5.17-develop.2020.6.23+commit.04e0b152.Linux.g++
• Operating system: Ubuntu 18.04

[hajduakos]

Thanks for reporting! To me it seems like this is related to #123, namely not handling strings properly when passed around or returned.

[dddejan]

123 is related to string literals (which are not arrays). The issue here is that the getter function .id() is currently modeled as directly giving the contract member (storage). In reality, for non-value types, the getters will return the corresponding memory version.

[zhao-nan]

Is this likely to be fixed at some point? We're doing a smart contract verification case study. For some parts, solc-verify would be the obvious choice and should work very well (judging from my experience), but at present this bug prevents us from using it.

[hajduakos]

@zhao-nan I will check. I think we need to do some conversion around here https://github.com/SRI-CSL/solidity/blob/7ffe52527eefcc4567ec6cff4ec9d7bfcb9dcb12/libsolidity/boogie/ASTBoogieExpressionConverter.cpp#L1375

[hajduakos]

@zhao-nan was fixed in bc1465b

I'm gonna leave the issue open, because we also have to port this fix to the 0.7 branch

[hajduakos]

Fixed on 0.7 as well. @zhao-nan can you please check and close the issue if it works? I've added your example as Issue147.sol

[zhao-nan]

Everything working now. Great, thanks!