[C++] Reference binding bug

[h0nzZik]

The following program gets stuck in execution:

int a = 1;
int &b = a;
int main() {
    b--;
}

Top of the K cell:

`ExecName`(`NoNNS`(.KList),`Identifier`(#token("\"b\"","String")))

It is probably a bug in the translation semantics. We use ExecName to refer only to local variables, whereas b is a global variable. However, when we change the type of b from int & to just int, the problem disappears.

[h0nzZik]

When processing resolveUniqueDecl of b, the <references> cell is empty. This probably is not caused by my recent work on rvalue references, f0f054a because the version 11f74ac behaves the same. TODO try an older version of RV-Match.

[h0nzZik]

The reference b should be initialized either statically in compile-time or dynamically in runtime - in our case, statically. Static initialization is implemented by means of the rules

rule <k> initializeObject(... init: Init:Val)
         => runInit(stripInitHolds(Init))
     ...</k>
     requires isStaticInitialization(Init)

from declarator.k and

rule (.K => K) ~> runInit(K:K)
rule K:Val ~> runInit(_) => .K

from elaborator.k.

, which put the initialization expression bindReference(...) on the top of the <k> cell. Unfortunately, the expression has the shape of bindReference(le(lv(...)...), ...), so the rule that fills ` does not match.

That can be fixed by changing a rule in initializer.k:

rule #figureInit(Base:LVal, cppRefType #as DestT::CPPType, _, E:Expr, _, _, _)
     => bindReference(Base /*le(Base, trace(Base), DestT)*/, E)

However, this modification changes the type of the first parameter of bindReference from DestT to type(Base). Is that a problem?

[h0nzZik]

Fixed in #448.