Use declareObject to create a temporary for ref.

Track duration of references.

The temporary to which the reference is bound
persists for the lifetime of the reference.

semantics/cpp/language/common/dynamic.k

@@ -520,7 +520,7 @@ module CPP-DYNAMIC-OTHER-SYNTAX
                      | showSignature(QualId, CPPType) [function]
                      | showQualId(QualId) [function]
 
-     syntax Expr ::= bindReference(Expr, Expr) [strict(c; 2)]
+     syntax Expr ::= bindReference(Expr, Expr, Duration) [strict(c; 2)]
 
      syntax KItem ::= "discard"
 

semantics/cpp/language/translation/decl/declarator.k

@@ -335,7 +335,7 @@ module CPP-TRANSLATION-DECL-DECLARATOR
                requires Constexpr() in S
 
           rule prepareDeclareNonStaticObject(X::CId, T::CPPType, Init::Init, Type::InitType, S::Set)
-               => declareNonStaticObject(X, T, figureInit(le(ExecName(NoNNS(), X), hasTrace(Name(NoNNS(), X)), T), T, Init, Type), Var(Type), AutoStorage, S)
+               => declareNonStaticObject(X, T, figureInit(le(ExecName(NoNNS(), X), hasTrace(Name(NoNNS(), X)), T), T, Init, Type, AutoStorage), Var(Type), AutoStorage, S)
 
           // NoLinkage, StaticStorage, not previously declared
           rule <k> declareObject(NoNamespace(), _, X::CId, _, T::CPPType, Init::Init, Type::DeclarationType, NoLinkage, StaticStorage, Set::Set)
@@ -522,7 +522,7 @@ module CPP-TRANSLATION-DECL-DECLARATOR
      syntax Decl ::= defineObject3(NNSVal, CId, CId, CPPType, DeclarationType, Set, init: Init, type: InitType)
 
      rule defineObject3(N::NNSVal, X::CId, CName::CId, T::CPPType, Type::DeclarationType, S::Set, Init::Init, InitType::InitType)
-          => initializeObject(N, X, T, figureInit(allocateDecl(N :: X, CName, T, S), T, Init, InitType), Type)
+          => initializeObject(N, X, T, figureInit(allocateDecl(N :: X, CName, T, S), T, Init, InitType, StaticStorage), Type)
 
 
      syntax InitType ::= getInitType(DeclarationType) [function]
@@ -546,7 +546,7 @@ module CPP-TRANSLATION-DECL-DECLARATOR
           ~> allocNrObject(Base, T)
           ~> initializeObject(NoNamespace(), X, T, figureInit(
                lv(lnew(Base), noTrace, T),
-               T, Init, Type), Var(Type))
+               T, Init, Type, StaticStorage), Var(Type))
 
      syntax Expr ::= allocateDecl(QualId, CId, CPPType, Set)
 
@@ -803,7 +803,7 @@ module CPP-TRANSLATION-DECL-DECLARATOR
 
      // This part is very similar to bindParams
      rule #computeDefaultArgs(ListItem(T:CPPType) P::List, ListItem(Init::Init) A::List, false)
-          => ListItem(figureInit(le(temp(!I:Int, T), noTrace, T), T, Init, CopyInit())) #computeDefaultArgs(P, A, false)
+          => ListItem(figureInit(le(temp(!I:Int, T), noTrace, T), T, Init, CopyInit(), AutoStorage)) #computeDefaultArgs(P, A, false)
           requires notBool (isCPPRefType(T) andBool isExpr(Init))
            andBool Init =/=K NoInit()
 

semantics/cpp/language/translation/expr/cast.k

@@ -32,7 +32,7 @@ module CPP-TRANSLATION-EXPR-CAST
      rule FunctionalCast(T:CPPType, ListItem(E::Expr)) => ParenthesizedCast(T, E)
 
      rule FunctionalCast(T:CPPType, ListItem(E1::Expr) ListItem(E2::Expr) L::List)
-          => makePRVal(figureInit(le(temp(!I:Int, T), noTrace, T), T, ExpressionList(ListItem(E1) ListItem(E2) L), DirectInit()))
+          => makePRVal(figureInit(le(temp(!I:Int, T), noTrace, T), T, ExpressionList(ListItem(E1) ListItem(E2) L), DirectInit(), AutoStorage))
 
      // @ref n4296 5.2.3:2
      rule FunctionalCast(T:CPPType, .List)
@@ -96,7 +96,7 @@ module CPP-TRANSLATION-EXPR-CAST
 
      // @ref n4800 7.6.1.8:4
      rule convertStatic(T::CPPType, V::Val, Tr::Trace)
-          => tryInit(T, V, figureInit(le(temp(!I:Int, T), Tr, T), T, V, DirectInit())) [owise]
+          => tryInit(T, V, figureInit(le(temp(!I:Int, T), Tr, T), T, V, DirectInit(), AutoStorage)) [owise]
 
      rule tryInit(_, _, V:Val) => V
 

semantics/cpp/language/translation/expr/function-call.k

@@ -38,7 +38,7 @@ module CPP-TRANSLATION-EXPR-FUNCTION-CALL
      syntax List ::= bindParams(List, List, List) [function]
 
      rule bindParams(ListItem(T:CPPType) P::List, ListItem(Init::Init) A::List, ListItem(_) DArgs::List)
-          => ListItem(figureInit(le(temp(!I:Int, T), noTrace, T), T, Init, CopyInit())) bindParams(P, A, DArgs)
+          => ListItem(figureInit(le(temp(!I:Int, T), noTrace, T), T, Init, CopyInit(), AutoStorage)) bindParams(P, A, DArgs)
 
      // ignore implicit object parameter for static function member
      rule bindParams(ListItem(implicitObjectParameter(t(... st: no-type))) P::List,

semantics/cpp/language/translation/expr/new.k

@@ -65,7 +65,8 @@ module CPP-TRANSLATION-EXPR-NEW
                  le(ExecName(NoNNS(), #NoName(I)), noTrace, t(noQuals, .Set, dynamicArrayType(T, newSize(I)))),
                  t(noQuals, .Set, dynamicArrayType(T, newSize(I))),
                  Init,
-                 DirectInit()
+                 DirectInit(),
+                 DynamicStorage
                )
              )
 
@@ -76,7 +77,8 @@ module CPP-TRANSLATION-EXPR-NEW
                  le(ExecName(NoNNS(), #NoName(I)), noTrace, t(noQuals, .Set, arrayType(T, Size))),
                  t(noQuals, .Set, arrayType(T, Size)),
                  Init,
-                 DirectInit()
+                 DirectInit(),
+                 DynamicStorage
                )
              )
 
@@ -87,7 +89,8 @@ module CPP-TRANSLATION-EXPR-NEW
                  le(ExecName(NoNNS(), #NoName(!I:Int)), noTrace, T),
                  T,
                  Init,
-                 DirectInit()
+                 DirectInit(),
+                 DynamicStorage
                )
             )
 

semantics/cpp/language/translation/expr/reference.k

@@ -7,54 +7,55 @@ module CPP-TRANSLATION-EXPR-REFERENCE
      imports CPP-REFERENCE-SYNTAX
      imports CPP-SYNTAX
      imports CPP-TYPING-SYNTAX
+     imports CPP-TRANSLATION-DECL-DECLARATOR-SYNTAX
      imports CPP-TRANSLATION-DECL-INITIALIZER-SYNTAX
 
-     context bindReference(HOLE:Expr, _) [result(LVal)]
+     context bindReference(HOLE:Expr, _, _) [result(LVal)]
 
-     rule bindReference(L:LVal, R:Val) => bindReference2(L, R)
+     rule bindReference(L:LVal, R:Val, D::Duration) => bindReference2(L, R, D)
      requires isCPPRefType(type(L))
 
-     syntax KItem ::= bindReference2(LVal, Val)
+     syntax KItem ::= bindReference2(LVal, Val, Duration)
 
      // @ref n4296 8.5.3:5.1.1
      // @ref n4800 9.3.3:5.1
-     rule bindReference2(V1::LVal, V2::Val)
+     rule bindReference2(V1::LVal, V2::Val, _)
           => bindReference'(V1, V2)
           requires isCPPLVRefType(type(V1))
           andBool notBool isCPPBitfieldType(type(V2))
           andBool isReferenceCompatible(innerType(type(V1)), type(V2))
           andBool cat(V2) ==K lvalue
 
      // @ref n4800 9.3.3:5.3 - converted initializer is NOT a prvalue
-     rule bindReference2(V1::LVal, V2::Val)
+     rule bindReference2(V1::LVal, V2::Val, _)
           => bindReference'(V1, V2)
           requires notBool isCPPBitfieldType(type(V2))
           andBool isReferenceCompatible(innerType(type(V1)), type(V2))
           andBool isValidReferenceType(type(V1))
           andBool cat(V2) ==K xvalue
 
      // @ref n4800 9.3.3:5.3 - converted initializer IS a prvalue
-     rule bindReference2(V1::LVal, V2::Val)
+     rule bindReference2(V1::LVal, V2::Val, D::Duration)
           =>
           bindReferenceToTemporary(
                V1,
-               temp(!I:Int, innerType(type(V1))),
                innerType(type(V1)),
-               V2
+               V2,
+               D
           )
           requires cat(V2) ==K prvalue
           andBool notBool isCPPArrayType(type(V2))
 
 
-     syntax KItem ::= bindReferenceToTemporary(LVal, Expr, CPPType, Val)
+     syntax KItem ::= bindReferenceToTemporary(LVal, CPPType, Val, Duration)
 
-     rule bindReferenceToTemporary(V1::LVal, Temp::Expr, T::CPPType, V2::Val)
+     rule bindReferenceToTemporary(V1::LVal, T::CPPType, V2::Val, D::Duration)
           =>
-          TExpressionStmt(figureInit(le(Temp, noTrace, T), T, V2, CopyInit())) // TODO copy or direct?
+          declareObject(NoNamespace(), NoNamespace(), #NoName(!I:Int), Identifier(""), T, V2, Var(CopyInit()), NoLinkage, D, .Set)
           ~>
-          bindReference'(V1, le(Temp, noTrace, T))
+          bindReference'(V1, Name(NoNNS(), #NoName(!I:Int)))
 
-     syntax Expr ::= "bindReference'" "(" Expr "," Expr ")" [function]
+     syntax Expr ::= "bindReference'" "(" Expr "," Expr ")" [strict(c; 2)]
 
      rule bindReference'(L:LVal, R:Val) => le(bindReferenceExec(L, R), trace(L), type(L))
 

semantics/cpp/language/translation/stmt/return.k

@@ -8,7 +8,7 @@ module CPP-TRANSLATION-STMT-RETURN
 
      context TReturnOp(HOLE:Expr) [result(Val)]
 
-     rule <k> ReturnStmt(I::Init) => TReturnOp(figureInit(le(temp(!I:Int, Ret), noTrace, Ret), Ret, I, CopyInit())) ...</k>
+     rule <k> ReturnStmt(I::Init) => TReturnOp(figureInit(le(temp(!I:Int, Ret), noTrace, Ret), Ret, I, CopyInit(), AutoStorage)) ...</k>
           <curr-function> Base::SymBase </curr-function>
           <functions>... Base |-> functionObject(_, t(_, _, functionType(... returnType: Ret::CPPType)), _, _) ...</functions>
           requires I =/=K NoInit()

semantics/cpp/language/translation/stmt/try.k

@@ -41,7 +41,7 @@ module CPP-TRANSLATION-STMT-TRY
 
      rule Throw.prepare(E::Expr, T:CPPType)
           => Throw.potentiallyInvokeDestructor(T)
-          ~> Throw.eval(figureInit(le(temp(!I:Int, utype(T)), noTrace, utype(T)), utype(T), E, CopyInit()), E)
+          ~> Throw.eval(figureInit(le(temp(!I:Int, utype(T)), noTrace, utype(T)), utype(T), E, CopyInit(), /* will never be used: */ AutoStorage), E)
 
      rule Throw.prepare(NoExpression(), NoExpression())
           => pre(ThrowOp(exceptionObject(type(no-type))), hasTrace(Throw(NoExpression())), type(void))

tests/unit-pass/static-ref.C

@@ -0,0 +1,7 @@
+int main()
+{
+  static const int &i = 42;
+  if (i != 42)
+	return 1;
+}
+