Clean GotoC AST annotations

[giltho]

Following #1469, it looks like a viable solution for supporting alternative backends is to comment the produced Irep to allow for a different interpretation than CBMC.

At the moment, the choice has been made to add a "#comment" named sub to the Irep itself. For example, in the case of Deinit, the assignment statement corresponding to lvalue = Nondet has this name sub. However, comments are usually attached to the location member of the irep.

The reason the comment was attached to the irep itself is simplicity: Stmt::to_irep's job is to call Location::to_irep and StmtBody::to_irep, and then aggregating the results. Therefore, if we want StmtBody::to_irep to produce a comment that is then added to the Location's irep, we need StmtBody::to_irep to return two things, instead of one. That would mean refactoring the function to change every return value, for 1 use case.

This issue aims at discussing the best and cleanest way to handle AST comments in the future.

[tedinski]

This appears to generate irep that looks like this currently:

{
    "id": "code",
    "sub": [
        {
            "id": "symbol",
            "namedSub": {
                "identifier": {
                "id": "_RNvMs2_NtCs2ybv9YpAGK_4core3fmtNtB5_9Arguments6new_v1Cs53OqACNvaXJ_11simple_test::1::var_24"
                },
                "type": {...}
            }
        },
        {
            "id": "side_effect",
            "namedSub": {
                "statement": {
                "id": "nondet"
                },
                "type": {...}
            }
        }
    ],
    "namedSub": {
        "statement": {
            "id": "assign"
        },
        "comment": {
            "id": "deinit"
        },
        "#source_location": {...}
    }
},

[tedinski]

Feedback: It's apparently not emitting the # right now?

The "meaningfulness" of # in CBMC is that there are two notions of equality: an earlier stage full-equality which compares everything on an irep node, and a later stage semantic-equality that ignores anything with # as prefix.

We probably want to keep that # for now, to ensure we don't impact CBMC's solving at all.

[giltho]

Interesting. I am not in control of the string that gets put there, only of the IrepId I choose: https://github.com/model-checking/kani/blob/main/cprover_bindings/src/irep/irep_id.rs#L905

We could maybe use "#annotation"? But I don't know its semantics... https://github.com/model-checking/kani/blob/main/cprover_bindings/src/irep/irep_id.rs#L1553

I think "comment" doesn't have a "#" because it's expected to be used inside of a "#c_location"

[giltho]

@danielsn proposed that we have our own kind of comments, such as #kani_comment or #kani_meta, which we could put anywhere we want on the Ireps Right now, the encoding of uninit adds a comment node (importantly without a hash) on the irep node, which could cause problems in the future.