Incorrect annotations should not kill parse/compile

[bkushigian]

Describe the bug Having an incorrect annotation bricks parse. In a vacuum I think it makes sense for a compiler to be strict about this sort of thing, but in an ecosystem where the main compiler (solc) is too permissive this means there are tons of libraries that exist that don't follow these conventions. For instance, a client is using the prb-math library which has the following code:

/// @notice Yields the smallest whole number greater than or equal to x.
///
/// @dev This is optimized for fractional value inputs, because for every whole value there are (1e18 - 1) fractional
/// counterparts. See https://en.wikipedia.org/wiki/Floor_and_ceiling_functions.
///
/// Requirements:
/// - x must be less than or equal to `MAX_WHOLE_UD60x18`.
///
/// @param x The UD60x18 number to ceil.
/// @param result The smallest whole number greater than or equal to x, as a UD60x18 number.
/// @custom:smtchecker abstract-function-nondet
function ceil(UD60x18 x) pure returns (UD60x18 result) {
   ...
}

Using Solang to parse this gives an error (note: this example is slightly different than the code I linked above because the source I found is a different version than what is cached in node_modules for me, but they are morally equivalent):

error: tag '@param' no field 'result'
   ┌─ /Users/benku/Certora/gmx-synthetics_all/node_modules/prb-math/contracts/PRBMathUD60x18.sol:52:16
   │
52 │     /// @param result The least integer greater than or equal to x, as an unsigned 60.18-decimal fixed-point number.
   │                ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^

Now I think you actually caught a bug in prb-math's documentation, which is good! But it unfortunately hard-bricks solang's parser, and it is out of our client's control to fix this bug.

Is it possible to make annotation enforcement optional? Probably best to implement solc's behavior by default and then have a --strict_checks flag to enable features that solc should actually do, but I don't know how possible this is?

[seanyoung]

solc is quite strict about doccomments and gives a fatal error when an issue is encountered. However, solc does not detect all problems. Here @return should be used rather than @param since result is a return value.

Do you have any other cases of doccomment failing in solang?

[bkushigian]

Oh good, glad they enforce this.

So far just this and the @custom:... bug I reported. I am running parse_and_resolve on as many projects as I can do I'll let you know if I find anything else

[seanyoung]

Fixed by #1539