Odr destructors (#341)

* New - Reformat and refactor a bit

* classFromType

* Class.potentiallyInvokeDestructor

* New - potentially invokes destructor of arr member

* Throw - rename

* Throw.potentiallyInvokeDestructor

* Test odr throw

* Test odr destruct in new array

* Test n4778 10.9.2/12

* Test n4778 9.3.1/8

* Be more explicit

* -fno-native-compilation for unit-fail-compilation

* Disable tests.

Because the destructors are implicitly generated even if they should not
be.

* -fno-native-compilation fix

Author: h0nzZik

semantics/cpp/language/common/dynamic.k

@@ -175,6 +175,8 @@ module CPP-DYNAMIC-SYNTAX
      syntax Bool ::= isClassQualId(QualId) [function]
 
      syntax Class ::= classFromScope(Scope) [function]
+                    | classFromType(CPPType) [function]
+                    | classFromSimpleType(CPPSimpleType) [function]
 
      syntax Linkage ::= "ExternalLinkage" | "InternalLinkage" | "NoLinkage"
      syntax Duration ::= "StaticStorage" | "ThreadStorage" | "AutoStorage" | "DynamicStorage"
@@ -286,6 +288,9 @@ module CPP-DYNAMIC
      rule classFromScope(classScope(C::Class, _)) => C
      rule classFromScope(blockScope(C:Class :: _::CId, _, _)) => C
 
+     rule classFromType(T:CPPClassType) => classFromSimpleType(simpleType(T))
+     rule classFromSimpleType(classType(C::Class)) => C
+
      rule enclosesNamespace(N::Namespace, N :: _) => true
      rule enclosesNamespace(N::Namespace, M::Namespace :: _) => enclosesNamespace(N, M)
           requires N =/=K M

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

@@ -32,6 +32,42 @@ module CPP-TRANSLATION-DECL-CLASS-SYNTAX
      syntax Bool ::= isPODLayoutType(CPPType) [function]
      syntax List ::= "Class.getNonStaticDataMembers" "(" ClassInfo ")" [function]
      syntax Map ::= "Class.getDataMembersInitializers" "(" ClassInfo ")" [function]
+
+endmodule
+
+module CPP-TRANSLATION-DECL-CLASS-DESTRUCTOR-SYNTAX
+     imports CPP-TRANSLATION-DECL-CLASS-SYNTAX
+
+     syntax KItem ::= "Class.potentiallyInvokeDestructor" "(" Class ")"
+                    | "Class.invokeDestructor" "(" Class ")"
+
+endmodule
+
+module CPP-TRANSLATION-DECL-CLASS-DESTRUCTOR
+     imports CPP-TRANSLATION-DECL-CLASS-DESTRUCTOR-SYNTAX
+     imports CPP-TRANSLATION-ODR-SYNTAX
+     imports CPP-SYNTAX // DestructorId
+     imports CPP-SYMLOC-SYNTAX // envEntry, SymBase
+     imports C-CONFIGURATION
+
+     // N4296 3.2/3
+     // N4778 6.2/8
+     // <quote>
+     // [...] A destructor for a class is odr-used if it is potentially invoked.
+     // </quote>
+     rule <k> Class.potentiallyInvokeDestructor((_ :: Class(_, X::CId, _)) #as C::Class) => Odr.newUse(Base) ...</k>
+          <curr-tr-tu> Tu::String </curr-tr-tu>
+          <tu-id> Tu </tu-id>
+          <class-id> C </class-id>
+          <cenv>... DestructorId(X) |-> (_::CPPFunctionType |-> envEntry(... base: Base::SymBase)) ...</cenv>
+
+     // N4296 12.4/11
+     // N4778 10.3.6/12
+     // <quote>
+     // A destructor is potentially invoked if it is invoked or as specified in [...]
+     // </quote>
+     rule Class.invokeDestructor(C::Class) => Class.potentiallyInvokeDestructor(C)
+
 endmodule
 
 module CPP-TRANSLATION-DECL-CLASS
@@ -61,6 +97,7 @@ module CPP-TRANSLATION-DECL-CLASS
      imports CPP-TRANSLATION-TYPING-EXPR-SYNTAX
      imports CPP-TYPING-SYNTAX
      imports CPP-TRANSLATION-VALUE-CATEGORY-SYNTAX
+     imports CPP-TRANSLATION-DECL-CLASS-DESTRUCTOR
 
      rule TypeDecl(ElaboratedTypeSpecifier(T:ClassKey, X::CId, NoNNS()) => declareClassName(T, X, true))
 

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

@@ -16,25 +16,36 @@ module CPP-TRANSLATION-EXPR-NEW
      imports CPP-ABSTRACT-SYNTAX
      imports CPP-BITSIZE-SYNTAX
      imports CPP-BUILTIN-SYNTAX
+     imports CPP-DYNAMIC-SYNTAX
+     imports CPP-SYNTAX
      imports CPP-TRANSLATION-DECL-CLASS-SYNTAX
+     imports CPP-TRANSLATION-DECL-CLASS-DESTRUCTOR-SYNTAX
      imports CPP-TRANSLATION-DECL-INITIALIZER-SYNTAX
-     imports CPP-DYNAMIC-SYNTAX
      imports CPP-TRANSLATION-OVERLOADING-SYNTAX
-     imports CPP-SYNTAX
      imports CPP-TRANSLATION-NAME-SYNTAX
      imports CPP-TYPE-MAP-SYNTAX
      imports CPP-TYPING-SYNTAX
 
      context NewExpr(_, _, (HOLE:Expr => reval(HOLE)), _, _) [result(PRVal)]
 
-     rule (.K => lookupAllocationFunction(operatornew, T, IsGlobal)) ~> NewExpr(IsGlobal::Bool, T:CPPType, NoExpression(), _, _)
+     rule (.K => lookupAllocationFunction(operatornew, T, IsGlobal))
+          ~> NewExpr(IsGlobal::Bool, T:CPPType, NoExpression(), _, _)
           requires notBool isCPPArrayType(T)
-     rule (.K => lookupAllocationFunction(operatornew[], getMostDerivedArrayElement(T), IsGlobal)) ~> NewExpr(IsGlobal::Bool, T:CPPType, _:PRVal, _, _)
-     rule (.K => lookupAllocationFunction(operatornew[], getMostDerivedArrayElement(T), IsGlobal)) ~> NewExpr(IsGlobal::Bool, T:CPPArrayType, _, _, _)
 
-     rule lookupAllocationFunction(X::CId, T::CPPType, IsGlobal:Bool) => qualifiedNameLookup(X, GlobalNamespace(), defaultMask)
+     rule (.K => lookupAllocationFunction(operatornew[], getMostDerivedArrayElement(T), IsGlobal))
+          ~> NewExpr(IsGlobal::Bool, T:CPPType, _:PRVal, _, _)
+
+     rule (.K => lookupAllocationFunction(operatornew[], getMostDerivedArrayElement(T), IsGlobal))
+          ~> NewExpr(IsGlobal::Bool, T:CPPArrayType, _, _, _)
+
+     rule lookupAllocationFunction(X::CId, T::CPPType, IsGlobal:Bool)
+          => qualifiedNameLookup(X, GlobalNamespace(), defaultMask)
           requires IsGlobal orBool notBool isCPPClassType(T)
-     rule lookupAllocationFunction(X::CId, t(... st: classType(C::Class)), false) => qualifiedNameLookup(X, C, defaultMask) orIfNotFound qualifiedNameLookup(X, GlobalNamespace(), defaultMask)
+
+     rule lookupAllocationFunction(X::CId, t(... st: classType(C::Class)), false)
+          => qualifiedNameLookup(X, C, defaultMask)
+               orIfNotFound
+             qualifiedNameLookup(X, GlobalNamespace(), defaultMask)
 
      rule (cSet(... id: Q::QualId) #as C:CandidateSet => resolveOverload(C, list(ListItem(pre(newSize(!I), noTrace, type(size_t)) * prv(byteSizeofType(T), noTrace, type(size_t))) P), 
                                              Name(NoNNS(), operatornew[]))
@@ -48,30 +59,101 @@ module CPP-TRANSLATION-EXPR-NEW
           requires getId(Q) ==K operatornew
 
      rule R:PRExpr ~> I:Int ~> NewExpr(_, T:CPPType, Size:PRExpr, Init::Init, _) #as E:Expr
-          => computeNewInit(R, T, Size, E, I, figureInit(le(ExecName(NoNNS(), #NoName(I)), noTrace, t(noQuals, .Set, dynamicArrayType(T, newSize(I)))), t(noQuals, .Set, dynamicArrayType(T, newSize(I))), Init, DirectInit()))
+          => computeNewInit(
+               R, T, Size, E, I,
+               figureInit(
+                 le(ExecName(NoNNS(), #NoName(I)), noTrace, t(noQuals, .Set, dynamicArrayType(T, newSize(I)))),
+                 t(noQuals, .Set, dynamicArrayType(T, newSize(I))),
+                 Init,
+                 DirectInit()
+               )
+             )
+
      rule R:PRExpr ~> I:Int ~> NewExpr(_, T:CPPType, prv(Size:Int, Tr::Trace, SizeT::CPPType), Init::Init, _) #as E:Expr
-          => computeNewInit(R, T, prv(Size, Tr, SizeT), E, I, figureInit(le(ExecName(NoNNS(), #NoName(I)), noTrace, t(noQuals, .Set, arrayType(T, Size))), t(noQuals, .Set, arrayType(T, Size)), Init, DirectInit()))
+          => computeNewInit(
+               R, T, prv(Size, Tr, SizeT), E, I,
+               figureInit(
+                 le(ExecName(NoNNS(), #NoName(I)), noTrace, t(noQuals, .Set, arrayType(T, Size))),
+                 t(noQuals, .Set, arrayType(T, Size)),
+                 Init,
+                 DirectInit()
+               )
+             )
+
      rule R:PRExpr ~> NewExpr(_, T:CPPType, NoExpression(), Init::Init, _) #as E:Expr
-          => computeNewInit(R, T, NoExpression(), E, !I, figureInit(le(ExecName(NoNNS(), #NoName(!I:Int)), noTrace, T), T, Init, DirectInit()))
+          => computeNewInit(
+               R, T, NoExpression(), E, !I,
+               figureInit(
+                 le(ExecName(NoNNS(), #NoName(!I:Int)), noTrace, T),
+                 T,
+                 Init,
+                 DirectInit()
+               )
+            )
 
      syntax Expr ::= computeNewInit(Expr, CPPType, AExpr, Expr, Int, K) [strict(6)]
 
-     rule computeNewInit(R::Expr, T::CPPType, Size:Expr, E::Expr, I::Int, Init:KResult)
-          => pre(NewOp(T, R, Init, Size, I), hasTrace(E), type(pointerType(T)))
-     rule computeNewInit(R::Expr, T::CPPType, NoExpression(), E::Expr, I::Int, Init:KResult)
-          => pre(NewOp(T, R, Init, .K, I), hasTrace(E), type(pointerType(T)))
+     syntax K ::= ExprOrNothing(K) [function]
+     rule ExprOrNothing(E:Expr) => E
+     rule ExprOrNothing(_) => .K [owise]
+
+     rule computeNewInit(R::Expr, T::CPPType, Size::AExpr, E::Expr, I::Int, Init:KResult)
+          => New.potentiallyInvokeDestructor(T)
+          ~> pre(NewOp(T, R, Init, ExprOrNothing(Size), I), hasTrace(E), type(pointerType(T)))
+
+
+     // TODO(jan.tusil) test this with multidimensional arrays
+     //
+     // N4296 5.3.4/19
+     // N4778 7.6.2.4/21
+     // <quote>
+     // If the new-expression creates an array of objects of class type,
+     // the destructor is potentially invoked.
+     // </quote>
+     // <group>
+
+     syntax KItem ::= "New.potentiallyInvokeDestructor" "(" CPPType ")"
+
+     rule New.potentiallyInvokeDestructor(T:CPPArrayType)
+          => #if isCPPClassType(innerType(T)) #then
+               Class.potentiallyInvokeDestructor(classFromType(innerType(T)))
+             #else
+               .K
+             #fi
+
+     rule New.potentiallyInvokeDestructor(T::CPPType) => .K
+          requires notBool isCPPArrayType(T)
+
+     // </group>
+
+     rule getSecondDeleteArg(M::TypeMap, V::PRVal)
+          => #getSecondDeleteArg(M, func(type(void), ptr(type(void))), func(type(void), ptr(type(void)), type(size_t)), V)
 
-     rule getSecondDeleteArg(M::TypeMap, V::PRVal) => #getSecondDeleteArg(M, func(type(void), ptr(type(void))), func(type(void), ptr(type(void)), type(size_t)), V)
      syntax List ::= #getSecondDeleteArg(TypeMap, CPPType, CPPType, PRVal) [function]
      rule #getSecondDeleteArg((T1 |-> _) (T2 |-> _) M::TypeMap, T1::CPPType, T2::CPPType, V::PRVal) => ListItem(V)
      rule #getSecondDeleteArg(...) => .List [owise]
 
      context DeleteExpr(_, _, (HOLE:Expr => reval(HOLE))) [result(PRVal)]
-     rule (.K => lookupAllocationFunction(operatordelete, innerType(type(V)), IsGlobal)) ~> DeleteExpr(IsGlobal::Bool, false, V:PRVal)
+
+     rule (.K => lookupAllocationFunction(operatordelete, innerType(type(V)), IsGlobal))
+          ~> DeleteExpr(IsGlobal::Bool, false, V:PRVal)
           requires isCPPPointerType(type(V)) andBool #fun(InnerT::CPPType => notBool isCPPClassType(InnerT) orBool notBool hasDestructorThat({InnerT}:>CPPClassType, #klabel(`isVirtualDestructor`)))(innerType(type(V)))
-     rule (cSet(Cands::TypeMap, Q::QualId) #as C:CandidateSet => resolveOverload(C, list(ListItem(le(ExecName(NoNNS(), #NoName(!I:Int)), noTrace, type(V))) getSecondDeleteArg(Cands, pre(newSize(!I), noTrace, type(size_t)))), Name(NoNNS(), operatordelete))
-          ~> !I:Int)
+
+     rule (
+            cSet(Cands::TypeMap, Q::QualId) #as C:CandidateSet
+            => resolveOverload(
+                 C,
+                 list(
+                   ListItem(le(ExecName(NoNNS(), #NoName(!I:Int)), noTrace, type(V)))
+                   getSecondDeleteArg(Cands, pre(newSize(!I), noTrace, type(size_t)))
+                 ),
+                 Name(NoNNS(), operatordelete)
+               )
+            ~> !I:Int
+          )
           ~> DeleteExpr(_, false, V::PRVal)
-     rule R:PRExpr ~> I:Int ~> DeleteExpr(IsGlobal::Bool, false, V:PRVal) => pre(DeleteOp(V, R, .K, I), hasTrace(DeleteExpr(IsGlobal, false, V)), type(void))
+
+     rule R:PRExpr ~> I:Int ~> DeleteExpr(IsGlobal::Bool, false, V:PRVal)
+          => pre(DeleteOp(V, R, .K, I), hasTrace(DeleteExpr(IsGlobal, false, V)), type(void))
 
 endmodule

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

@@ -7,13 +7,13 @@ module CPP-TRANSLATION-STMT-TRY
      imports CPP-DYNAMIC-SYNTAX
      imports CPP-SYNTAX
      imports CPP-TYPING-SYNTAX
+     imports CPP-TRANSLATION-DECL-CLASS-DESTRUCTOR-SYNTAX
      imports CPP-TRANSLATION-DECL-DECLARATOR-SYNTAX
      imports CPP-TRANSLATION-DECL-INITIALIZER-SYNTAX
      imports CPP-TRANSLATION-ELABORATOR-SYNTAX
      imports CPP-TRANSLATION-ODR-SYNTAX
      imports CPP-TRANSLATION-TYPING-EXPR-SYNTAX
 
-
      rule (.K => elaborate(Try, listToK(Catch)))
           ~> TryStmt(Try::Stmt, Catch::List)
      rule <k> elaborateDone(Try:K, Catch:K) ~> TryStmt(_, _) => .K ...</k>
@@ -23,30 +23,50 @@ module CPP-TRANSLATION-STMT-TRY
      rule <k> elaborateDone(S:K) ~> TCatchAnyOp(_) => .K ...</k>
           <elab>... .K => CatchAnyOp(S) </elab>
 
-     context evalThrow(HOLE:Expr, _) [result(Val)]
+     context Throw.eval(HOLE:Expr, _) [result(Val)]
 
      rule Throw(E::Expr)
        => Odr.newUse(obj(0, 0, builtinCppSymbol("::std::terminate()")))
-       ~> prepareThrow(E, E)
+       ~> Throw.prepare(E, E)
+
+     syntax Expr ::= "Throw.prepare" "(" AExpr "," K ")"
 
-     syntax Expr ::= prepareThrow(AExpr, K)
-     context prepareThrow(_, HOLE:TypeExpr => typeof(HOLE)) [result(CPPTypeExpr)]
-     context prepareThrow(_, HOLE:CPPTypeExpr)
+     context Throw.prepare(_, HOLE:TypeExpr => typeof(HOLE)) [result(CPPTypeExpr)]
+     context Throw.prepare(_, HOLE:CPPTypeExpr)
              requires notBool isDependentInScope(HOLE) [result(CPPType)]
 
-     rule prepareThrow(_, T:CPPArrayTypeExpr => type(pointerType(innerType(T))))
-     rule prepareThrow(_, T:CPPFunctionTypeExpr => type(pointerType(T)))
-     rule prepareThrow(E::Expr, T:CPPType)
-          => evalThrow(figureInit(le(temp(!I:Int, utype(T)), noTrace, utype(T)), utype(T), E, CopyInit()), E)
-     rule prepareThrow(E::Expr, T:CPPTypeExpr)
-          => prd(prepareThrow(E, T), hasTrace(Throw(E)), type(void), T)
+     rule Throw.prepare(_, T:CPPArrayTypeExpr => type(pointerType(innerType(T))))
+
+     rule Throw.prepare(_, T:CPPFunctionTypeExpr => type(pointerType(T)))
+
+     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)
+
+     rule Throw.prepare(E::Expr, T:CPPTypeExpr)
+          => prd(Throw.prepare(E, T), hasTrace(Throw(E)), type(void), T)
           requires isDependentInScope(T)
-     rule prepareThrow(NoExpression(), NoExpression())
+
+     rule Throw.prepare(NoExpression(), NoExpression())
           => pre(ThrowOp(exceptionObject(type(no-type))), hasTrace(Throw(NoExpression())), type(void))
 
-     syntax Expr ::= evalThrow(Expr, Expr)
+     syntax Expr ::= "Throw.eval" "(" Expr "," Expr ")"
+
+     rule Throw.eval(V:Val, E::Expr) => pre(ThrowOp(V), hasTrace(E), type(void))
+
+     // n4778 13.1/5
+     // <quote>
+     // When the thrown object is a class object, [...].
+     // The destructor is potentially invoked.
+     // </quote>
+     // <group>
+     syntax KItem ::= "Throw.potentiallyInvokeDestructor" "(" CPPType ")"
 
-     rule evalThrow(V:Val, E::Expr) => pre(ThrowOp(V), hasTrace(E), type(void))
+     rule Throw.potentiallyInvokeDestructor(T::CPPType)
+          => #if isCPPClassType(T) #then
+                 Class.potentiallyInvokeDestructor(classFromType(T))
+             #else .K #fi
+     // </group>
 
      rule exceptionObject(T::CPPType) => le(exceptionObject(T), noTrace, T)
           requires Translation()

tests/unit-fail-compilation/Makefile

@@ -35,7 +35,7 @@ cpp-comparison: ${CPP_TEST_COMPARISON}
 
 %.C.kcc.out: %.C
 	@echo -n "Compiling $<... "
-	@../../dist/k++ -Werror -Wfatal-errors $< > $@.tmp 2>&1; ${CHECK_RESULT_COMPILE}
+	@../../dist/k++ -fno-native-compilation -Werror -Wfatal-errors $< > $@.tmp 2>&1; ${CHECK_RESULT_COMPILE}
 
 
 %.cmp: %.kcc.out %.ref

tests/unit-fail-compilation/new26.C.ref

@@ -14,4 +14,4 @@ inline void operator delete (void*) {}
         see C++14 section 18.6.1.1:11 http://rvdoc.org/C++14/18.6.1.1
 
 Translation failed (kcc_config dumped). To repeat, run this command in directory unit-fail-compilation:
-k++ -d -Werror -Wfatal-errors new26.C
+k++ -d -fno-native-compilation -Werror -Wfatal-errors new26.C

tests/unit-fail-compilation/odr-destructor-in-aggregate-initialization.C.disabled

@@ -0,0 +1,20 @@
+/* 
+ * n4778 9.3.1/8
+ * The destructor for each element of class type is potentially invoked
+ * from the context where the aggregate initialization occurs.
+ */
+
+struct A {
+	A(int){}
+	~A();
+};
+
+// An aggregate
+struct B {
+	A a;
+};
+
+int main(){
+	// An aggregate initialization
+	B b{{1}};
+}

tests/unit-fail-compilation/odr-destructor-in-aggregate-initialization.C.ref

@@ -0,0 +1,3 @@
+/tmp/ccgknZkF.o: In function `B::~B()':
+odr-destructor-in-aggregate-initialization.C:(.text._ZN1BD2Ev[_ZN1BD5Ev]+0x14): undefined reference to `A::~A()'
+collect2: error: ld returned 1 exit status

tests/unit-fail-compilation/odr-destructor-in-constructor.C.disabled

@@ -0,0 +1,14 @@
+/* In a non-delegating constructor,
+ * the destructor for each potentially constructed subobject of class type is potentially invoked.
+ */
+
+struct A {
+	~A();
+};
+
+struct B {
+	A a;
+	B(){}
+};
+
+int main(){}

tests/unit-fail-compilation/odr-destructor-in-constructor.C.ref

@@ -0,0 +1,3 @@
+/tmp/cc5l9Z6k.o: In function `B::~B()':
+odr-destructor-in-constructor.C:(.text._ZN1BD2Ev[_ZN1BD5Ev]+0x14): undefined reference to `A::~A()'
+collect2: error: ld returned 1 exit status

tests/unit-fail-compilation/odr-destructor-new-arr.C.disabled

@@ -0,0 +1,8 @@
+struct A {
+  A() { throw 3; }
+  ~A();
+};
+
+int main() {
+	new A[2];
+}

tests/unit-fail-compilation/odr-destructor-new-arr.C.ref

@@ -0,0 +1,3 @@
+/tmp/ccHQ2ZQE.o: In function `main':
+odr-destructor-new-arr.C:(.text+0x6c): undefined reference to `A::~A()'
+collect2: error: ld returned 1 exit status

tests/unit-fail-compilation/odr-destructor-throw.C.disabled

@@ -0,0 +1,7 @@
+struct E {
+  ~E();
+};
+
+int main() {
+	throw E();
+}

tests/unit-fail-compilation/odr-destructor-throw.C.ref

@@ -0,0 +1,3 @@
+/tmp/cc4dM4bV.o: In function `main':
+odr-destructor-throw.C:(.text+0x14): undefined reference to `E::~E()'
+collect2: error: ld returned 1 exit status