KJ-11 Eliminate the rule [runtime-elabExpressions].

Fixed the problems reported by jenkins test.

Author: denis-bogdanas

semantics/api-core.k

@@ -275,12 +275,13 @@ rule [storeCopyDiscard]:
 //@We need to synchronize access to class literals to avoid instantiation of the came .class by multiple threads. This is done by the term temp in <classLiteralsMap>. We cannot use 'Synchronized because it required an objectClousre as argument, and we might not have any objects instantiated at the moment.
 rule [ClassLiteralInstantiate]:
     <k>
-        (. => saveClassLiteral(T, 'NewInstance(
+        (. => saveClassLiteral(T,
+          elab('NewInstance(
                 'None(.KList),,
                 class String2Id("java.lang.Class"),,
                 'ListWrap(toString(T)),,
                 'None(.KList)
-              ))
+          )))
         )
         ~> 'Lit('Class(T:Type))::_
       ...

semantics/elaborate-blocks.k

@@ -1267,17 +1267,6 @@ rule count(Ks:KList) => count(0, Ks)
 rule count(I:Int, K:K,, Ks:KList) => count(I +Int 1, Ks)
 rule count(I:Int, .KList) => I::int
 
-//@ Unwrap elaborated terms in execution phase, so that they could be executed.
-rule [elabRes-ExecutionPhase-discard1]:
-    <k> (elabRes(K:K) => K) ~> KL:KLabel(_) ...</k>
-    <globalPhase> ExecutionPhase </globalPhase>
-when
-    KL =/=KLabel 'elab`(_`)
-
-rule [elabRes-ExecutionPhase-discard2]:
-    <k> elabRes(K:K) => K </k>
-    <globalPhase> ExecutionPhase </globalPhase>
-
 //@\subsection{Elaboration of SuperConstrInv, AltConstrInv}
 
 //@ Desugaring unqualified superclass constructor invocation into a qualified one
@@ -1356,4 +1345,20 @@ rule [getEnclosingClass]:
     <classType> Class </classType>
     <enclosingClass> EnclosingClass:ClassType </enclosingClass>
 
+//@ \subsection{Hacks related to elaboration during execution phase}
+
+//@ Unwrap elaborated terms in execution phase, so that they could be executed.
+rule [elabRes-ExecutionPhase-discard1]:
+    <k> (elabRes(K:K) => K) ~> KL:KLabel(_) ...</k>
+    <globalPhase> ExecutionPhase </globalPhase>
+when
+    KL =/=KLabel 'elab`(_`)
+
+rule [elabRes-ExecutionPhase-discard2]:
+    <k> elabRes(K:K) => K </k>
+    <globalPhase> ExecutionPhase </globalPhase>
+
+//Required for [VarDecWithArrayInitDesugar], [FieldDecWithArrayInitDesugar]
+rule elab(elab(K:K)) => elab(K)
+
 endmodule

semantics/statements.k

@@ -412,7 +412,7 @@ rule [ThrowCheckedTrue]:
     ~> catchBlocks(catchImpl(paramImpl(T:Type, X:Id), CatchS:K),, _)
     => 'Block('ListWrap(
           'LocalVarDec(.K,, T,, 'ListWrap('VarDec(X))),,
-          'ExprStm('Assign(localVar(X)::T,, TV)),,
+          elab('ExprStm('Assign(localVar(X)::T,, TV))),,
           CatchS
         ))
 

semantics/static-init.k

@@ -36,7 +36,7 @@ rule [staticInit]:
       => elab('ListWrap(
         staticInit(BaseClass),,
         'Try(
-            StaticInit,,
+            elabRes(StaticInit),,
 
             //catch clause of 'Try
             'ListWrap(