Destruct temporaries (2) (#572)

* createTemporary for bindParams

* Delete local references when they go out of scope

* destruct returned temporary

* Forgotten test.

* fix: forgotten `destructTemporaries`

* Forgotten Makefile

Author: h0nzZik

semantics/common/execution/thread_local.k

@@ -53,6 +53,7 @@ module COMMON-THREAD-LOCAL
             <most-derived-class> .K </most-derived-class>
 
             <constructed-temporaries> .List </constructed-temporaries>
+            <ret-constructed-temporary> .K </ret-constructed-temporary>
 
             // stack of block-control cells
             <block-stack color="violet"> .List </block-stack>

semantics/cpp/language/common/syntax.k

@@ -209,7 +209,7 @@ module CPP-SYNTAX
                    | ExpressionStmt(Expr) [strict(c)]
                    | PRValExpressionStmt(Expr) [strict(c)]
                    | BreakStmt()
-                   | ReturnOp(Expr)
+                   | ReturnOp(init: Expr, obj: K)
                    | IfStmt(Decl, Stmt, Stmt)
                    | IfStmt(Expr, K, K)
                    | WhileStmt(Decl, Stmt)

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

@@ -19,28 +19,30 @@ module CPP-EXECUTION-DECL-DECLARATOR
                     allocObject(bnew(!I:Int, T, Mods, D), T, byteSizeofType(T))
                  #else .K #fi
               ~> addToExecEnv(X, T, bnew(!I:Int, T, Mods, D), false)
-              ~> #if notBool isCPPRefType(T) #then
-                    LCregisterForDestruction(ExecName(NoNNS(), X))
-                 #else .K #fi
+              ~> LCregisterForDestruction(ExecName(NoNNS(), X))
               ~> initializeObjectExec(Init)
-              ~> #if notBool isCPPRefType(T) #then
-                    LCupdateRegisteredForDestruction(size(LC))
-                 #else .K #fi
+              ~> LCupdateRegisteredForDestruction(size(LC))
           ...</k>
           <duration> D::Duration </duration>
           <local-vars> Vars:Set (.Set => SetItem(X)) </local-vars>
           <locally-constructed> LC::List </locally-constructed>
           requires notBool X in Vars andBool X =/=K #NoName
 
-     syntax KItem ::= LCregisterForDestruction(Expr) [strict(1)]
+     syntax KItem ::= LCregisterForDestruction(Expr)
+
+     // This works even if the declared variable is a reference.
+     // The rule for reference rewriting (from dynamic.k)
+     // can not apply, because the reference was not
+     // initialized yet.
+     context LCregisterForDestruction(HOLE:Expr) [result(LV)]
 
      // we register the object for destruction before
      // its initializer runs (but with the `initialized` flag cleared)
      // so that if an exception is thrown in the initializer,
      // the allocated object gets deleted.
      // The `initialized` flag is set later
      // in `LCupdateRegisteredForDestruction()`.
-     rule <k> LCregisterForDestruction(Obj:LVal) => .K ...</k>
+     rule <k> LCregisterForDestruction(Obj:LV) => .K ...</k>
           <locally-constructed> .List =>
                ListItem(lcentry(Obj, false, true, false))
           ...</locally-constructed>

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

@@ -1,4 +1,12 @@
+module CPP-EXECUTION-EXPR-REFERENCE-SYNTAX
+     imports SYMLOC-SORTS
+
+     syntax KItem ::= deleteReference(SymLoc)
+
+endmodule
+
 module CPP-EXECUTION-EXPR-REFERENCE
+     imports CPP-EXECUTION-EXPR-REFERENCE-SYNTAX
      imports C-CONFIGURATION
      imports BOOL
      imports CPP-BITSIZE-SYNTAX
@@ -41,4 +49,7 @@ module CPP-EXECUTION-EXPR-REFERENCE
 
      rule referenceTarget(... loc: Loc::SymLoc) => Loc [owise]
 
+     rule <k> deleteReference(Loc::SymLoc) => .K ...</k>
+     <references> R::Map => R[stripProv(Loc) <- undef] </references>
+
 endmodule

semantics/cpp/language/execution/stmt/block.k

@@ -22,6 +22,7 @@ module CPP-EXECUTION-STMT-BLOCK
      imports CPP-BUILTIN-SYNTAX
      imports CPP-DYNAMIC-SYNTAX
      imports CPP-EXECUTION-ENV-SYNTAX
+     imports CPP-EXECUTION-EXPR-REFERENCE-SYNTAX
      imports CPP-EXECUTION-FULL-EXPRESSION-SYNTAX
      imports CPP-EXECUTION-STMT-BLOCK-SYNTAX
      imports CPP-SYMLOC-SYNTAX
@@ -106,7 +107,7 @@ module CPP-EXECUTION-STMT-BLOCK
 
      rule destructLocal(IsException:Bool,
                lcentry(
-                    lv(Loc::SymLoc, _, _) #as V::LVal,
+                    lv(Loc::SymLoc, _, T::CPPType) #as V::LVal,
                     Initialized:Bool,
                     CanBeVirtual::Bool,
                     IsConstructor:Bool
@@ -119,11 +120,15 @@ module CPP-EXECUTION-STMT-BLOCK
                destruct(V, CanBeVirtual) ~> fullExpression
           #fi
           ~>
-          #if IsConstructor #then
+          #if IsConstructor orBool isCPPRefType(T) #then
                .K
           #else
                deleteObject(base(Loc))
           #fi
+          ~>
+          #if isCPPRefType(T) #then
+               deleteReference(Loc)
+          #else .K #fi
 
      syntax KItem ::= "unfoldBlockStack"
 

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

@@ -15,23 +15,30 @@ module CPP-EXECUTION-STMT-RETURN
      imports CPP-DYNAMIC-SYNTAX
      imports CPP-EXECUTION-ENV-SYNTAX
      imports CPP-EXECUTION-FULL-EXPRESSION-SYNTAX
+     imports CPP-EXECUTION-STMT-BLOCK-SYNTAX
      imports CPP-MEMORY-ALLOC-SYNTAX
      imports CPP-REFERENCE-SYNTAX
      imports CPP-SYNTAX
      imports CPP-TYPING-SYNTAX
 
      // Return (from C++ function)
-     rule <k> ReturnOp(V::Expr) => prepareReturn(getReturnType(T), V) ...</k>
+     rule <k> ReturnOp(V::Expr, Obj::Expr) => prepareReturn(getReturnType(T), V, Obj) ...</k>
           <curr-scope> blockScope(_, Base::SymBase, _) </curr-scope>
           <functions>... Base |-> functionObject(_, T::CPPType, _, _) ...</functions>
 
-     syntax KItem ::= prepareReturn(CPPType, K)
+     syntax KItem ::= prepareReturn(CPPType, K, KItem)
 
-     rule prepareReturn(T::CPPType, Init:KItem)
+     context prepareReturn(_, _, HOLE:Expr) [result(LV)]
+
+     rule <k> prepareReturn(T::CPPType, Init:KItem, Obj:LV)
           => Return'(Init, T)
+          ...</k>
+          <ret-constructed-temporary>
+               .K => lcentry(Obj, false, true, false)
+          </ret-constructed-temporary>
           requires notBool isCPPVoidType(T)
 
-     rule prepareReturn(t(... st: void) #as T::CPPType, V:PRVal) => Return''(V)
+     rule prepareReturn(t(... st: void) #as T::CPPType, V:PRVal, _) => Return''(V)
 
      syntax KItem ::= "Return'" "(" KItem "," CPPType ")" [strict(c; 1)]
 
@@ -66,13 +73,15 @@ module CPP-EXECUTION-STMT-RETURN
      // Return (to C++ function)
      rule <k> return(V:Val) ~> _
               => exitRestrictBlock(.Set)
+              ~> addToCT(LCE)
               ~> sequencePoint
               ~> V
               ~> K
           </k>
           (<function-control>
                <live-va-lists> .Set </live-va-lists>
                <block-stack> .List </block-stack>
+               <ret-constructed-temporary> LCE::KItem  </ret-constructed-temporary>
           ...</function-control> => C)
           <call-stack>
                ListItem(
@@ -86,4 +95,14 @@ module CPP-EXECUTION-STMT-RETURN
                ) => .List
           ...</call-stack>
 
+     syntax KItem ::= addToCT(K)
+
+     rule addToCT(.K) => .K
+
+     rule <k> addToCT(lcentry(Obj::LV, _, _, _)) => .K ...</k>
+          <constructed-temporaries> .List =>
+               ListItem(lcentry(Obj, true, true, false))
+          ...</constructed-temporaries>
+
+
 endmodule

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

@@ -7,6 +7,7 @@ module CPP-EXECUTION-STMT-TRY
      imports CPP-CONVERSION-SYNTAX
      imports CPP-DYNAMIC-SYNTAX
      imports CPP-EXECUTION-ENV-SYNTAX
+     imports CPP-EXECUTION-STMT-BLOCK-SYNTAX
      imports CPP-EXECUTION-TEMPORARY-SYNTAX
      imports CPP-ERROR-SYNTAX
      imports CPP-SETTINGS-SYNTAX
@@ -25,14 +26,21 @@ module CPP-EXECUTION-STMT-TRY
      rule <k> ThrowOp(V:LVal) => throw(V) ...</k>
           <uncaught-exception> _ => true </uncaught-exception>
 
+     rule <k> (.K => destructLocal(true, LCE)) ~> throw(V::LVal) ...</k>
+          <catch-handlers> .List </catch-handlers>
+          <ret-constructed-temporary> lcentry(...) #as LCE::KItem => .K </ret-constructed-temporary>
+          requires canUnwindStack(V)
+
      rule <k> (.K => destructTemporaries(true)) ~> throw(V::LVal) ...</k>
           <catch-handlers> .List </catch-handlers>
+          <ret-constructed-temporary> .K </ret-constructed-temporary>
           <constructed-temporaries> ListItem(_) _ </constructed-temporaries>
           requires canUnwindStack(V)
 
      // if there are still blocks in this function, pop them
      rule <k> (.K => popBlock(true)) ~> throw(V::LVal) ...</k>
           <catch-handlers> .List </catch-handlers>
+          <ret-constructed-temporary> .K </ret-constructed-temporary>
           <constructed-temporaries> .List </constructed-temporaries>
           <block-stack> ListItem(_) _ </block-stack>
           <block-history> ListItem(Num::Int) ...</block-history>
@@ -43,6 +51,7 @@ module CPP-EXECUTION-STMT-TRY
      // if we are at the root of a loop, pop it before popping further blocks
      rule <k> throw(V::LVal) ~> (_ => K) </k>
           <catch-handlers> .List </catch-handlers>
+          <ret-constructed-temporary> .K </ret-constructed-temporary>
           <constructed-temporaries> .List </constructed-temporaries>
           <block-stack> ListItem(_) _ </block-stack>
           <block-history> ListItem(Num::Int) ...</block-history>
@@ -52,6 +61,7 @@ module CPP-EXECUTION-STMT-TRY
      // if there are still functions in the stack trace, pop them
      rule <k> (.K => unwindFunction) ~> throw(V::LVal) ...</k>
           <catch-handlers> .List </catch-handlers>
+          <ret-constructed-temporary> .K </ret-constructed-temporary>
           <constructed-temporaries> .List </constructed-temporaries>
           <block-stack> .List </block-stack>
           <call-stack> ListItem(_) _ </call-stack>
@@ -161,7 +171,8 @@ module CPP-EXECUTION-STMT-TRY
 
      rule <k> catchWithHandler(CatchOp(_, pushBlock(N::Int) ~> declareNonStaticObjectExec(... id: X::CId) #as D:KItem ~> Rest:K), V::LVal)
               ~> tryMark(I::Int)
-              => popBlock(true)
+              => destructTemporaries(true)
+              ~> popBlock(true)
               ~> pushBlock(N)
               ~> setCurrentException(V)
               ~> #if X ==K #NoName #then .K #else D #fi

semantics/cpp/language/execution/temporary.k

@@ -9,6 +9,7 @@ module CPP-EXECUTION-TEMPORARY
      imports C-CONFIGURATION
      imports CPP-DYNAMIC-SYNTAX
      imports CPP-EXECUTION-STMT-BLOCK-SYNTAX
+     imports CPP-REFERENCE-SYNTAX
      imports COMPAT-SYNTAX
 
      // This code works similarly to the code
@@ -21,23 +22,28 @@ module CPP-EXECUTION-TEMPORARY
           ...</k>
           <constructed-temporaries> CT::List </constructed-temporaries>
 
-     syntax KItem ::= CTregisterForDestruction(Expr) [strict(1)]
+     syntax KItem ::= CTregisterForDestruction(Expr)
 
-     rule <k> CTregisterForDestruction(Obj:LVal) => .K ...</k>
+     // see LCregisterForDestruction in declarator.k
+     context CTregisterForDestruction(HOLE:Expr) [result(LV)]
+
+     rule <k> CTregisterForDestruction(Obj:LV) => .K ...</k>
           <constructed-temporaries> .List =>
                ListItem(lcentry(Obj, false, true, false))
           ...</constructed-temporaries>
 
      syntax KItem ::= CTupdateRegisteredForDestruction(Int)
                     | CTupdateRegisteredForDestruction2(idx: Int, entry: KItem)
 
+     syntax LVorRBR ::= LV | ReferenceBindingResult
+
      // `-1 -Int Size` from the end is the index of the newly-added entry
-     rule <k> V:LVal ~> CTupdateRegisteredForDestruction(Size::Int)
+     rule <k> V:LVorRBR ~> CTupdateRegisteredForDestruction(Size::Int)
           => CTupdateRegisteredForDestruction2(-1 -Int Size, CT[-1 -Int Size])
           ~> V
           ...</k>
           <constructed-temporaries> CT::List </constructed-temporaries>
-          requires isEvalVal(V)
+          requires isEvalVal(V) orBool isReferenceBindingResult(V)
 
      rule <k> CTupdateRegisteredForDestruction2(Idx::Int,
                lcentry(Obj::LVal, false, CanBeVirtual::Bool, IsConstructor::Bool)) => .K

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

@@ -692,7 +692,14 @@ module CPP-TRANSLATION-DECL-DECLARATOR
      syntax Stmt ::= getFunDefBody(TemplateInfo, QualId, CPPType, Stmt) [function]
 
      rule getFunDefBody(noTemplate, QX::QualId, T::CPPType, Body::Stmt)
-          => TLabelStmt(funLabel(getId(QX)), #if isDestructorId(getId(QX)) #then ListItem(Destructor()) #else .List #fi ListItem(Body) ListItem(TReturnOp(getDefaultReturnOp(QX, getReturnType(T)))))
+          =>
+          TLabelStmt(funLabel(getId(QX)),
+               #if isDestructorId(getId(QX)) #then ListItem(Destructor()) #else .List #fi
+               ListItem(Body)
+               ListItem(TReturnOp(
+                    getDefaultReturnOp(!I:Int, QX, getReturnType(T)),
+                    temp(!I:Int, type(int))))
+          )
 
      rule getFunDefBody(_, _, _, Body::Stmt) => Body [owise]
 
@@ -707,12 +714,12 @@ module CPP-TRANSLATION-DECL-DECLARATOR
      rule <k> setTrThis(C:Class :: _, methodInfo(... cvQuals: Q::Quals)) => .K ...</k>
           <tr-this> _ => pre(This(), hasTrace(This()), type(pointerType(t(Q::Quals, .Set, classType(C))))) </tr-this>
 
-     syntax Expr ::= getDefaultReturnOp(QualId, CPPType) [function]
+     syntax Expr ::= getDefaultReturnOp(Int, QualId, CPPType) [function]
 
-     rule getDefaultReturnOp(GlobalNamespace() :: Identifier("main"), T::CPPType)
-          => le(temp(!I:Int, type(int)), noTrace, T) :=init prv(0, noTrace, type(int))
+     rule getDefaultReturnOp(I::Int, GlobalNamespace() :: Identifier("main"), T::CPPType)
+          => le(temp(I, type(int)), noTrace, T) :=init prv(0, noTrace, type(int))
 
-     rule getDefaultReturnOp(_, _) => prv(voidVal, noTrace, type(void)) [owise]
+     rule getDefaultReturnOp(_, _, _) => prv(voidVal, noTrace, type(void)) [owise]
 
      syntax KItem ::= dummyBind(List)
 

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

@@ -8,6 +8,7 @@ module CPP-TRANSLATION-EXPR-FUNCTION-CALL
      imports CPP-DYNAMIC-SYNTAX
      imports CPP-TRANSLATION-ELABORATOR-SYNTAX
      imports CPP-TRANSLATION-OVERLOADING-SYNTAX
+     imports CPP-TRANSLATION-TEMPORARY-SYNTAX
      imports CPP-SYNTAX
      imports CPP-TYPING-SYNTAX
 
@@ -38,7 +39,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(), AutoStorage)) bindParams(P, A, DArgs)
+          => ListItem(createTemporary(temp(!I:Int, T), T, 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,