Relax closure calling rule (and fix pop)

src/SCIF.cup

@@ -227,7 +227,7 @@ nonterminal TrailerExpr trailer;
 //nonterminal Setmaker setmaker;
 // nonterminal Setmaker setmaker_sub;
 // nonterminal ClassDef classdef;
-nonterminal Call arglist;
+nonterminal List<Expression> arglist, call_args;
 nonterminal LabeledType labeledType, maybeLabeledType;
 nonterminal ast.ClosureType closureType;
 nonterminal List<LabeledType> throwsOpt;
@@ -269,7 +269,6 @@ nonterminal List<LabeledType> except_types;
 nonterminal Throw throw_stmt;
 nonterminal List<FunctionDef> constructors;
 nonterminal FunctionDef constructor;
-//nonterminal EndorseStatement endorse_stmt;
 nonterminal EndorseIfStatement endorseIf_stmt;
 nonterminal Call call_expr;
 nonterminal Revert revert_stmt;
@@ -666,10 +665,10 @@ plain_var_dec ::=
 //        RESULT.setLoc(new CodeLocation(aleft, aright, filename));
 //
 //    :}
-    type:t NAME:a SEMI {:
+    maybeLabeledType:t NAME:a SEMI {:
         Name name = new Name((String)a);
         name.setLoc(new CodeLocation(aleft, aright, filename));
-        StateVariableDeclaration rnt = new StateVariableDeclaration(name, new LabeledType(t, null), null, false, false, false);
+        StateVariableDeclaration rnt = new StateVariableDeclaration(name, t, null, false, false, false);
         RESULT = rnt;
         RESULT.setLoc(new CodeLocation(aleft, aright, filename));
     :};
@@ -1158,9 +1157,6 @@ stmt ::= assign_stmt:a {: RESULT = a; :}
     | throw_stmt:a {: RESULT = a;:}
     | revert_stmt:a {: RESULT = a;:}
     | emit_stmt:a {: RESULT = a; :}
-//    | endorse_stmt:a {:
-//        RESULT = a;
-//    :}
     | endorseIf_stmt:a {:
         RESULT = a;
     :}
@@ -1173,21 +1169,11 @@ stmt ::= assign_stmt:a {: RESULT = a; :}
     :}
     ;
 
-//endorse_stmt ::=
-//    ENDORSEIF:x LPAR name_list:exprList COMMA ifLabel:from RIGHT_ARROW ifLabel:to RPAR IN suite:s {:
-//        EndorseStatement statement = new EndorseStatement(exprList, from, to, s);
-//        RESULT = statement;
-//        RESULT.setLoc(new CodeLocation(xleft, xright, filename));
-//    :}
-//    ;
-
 emit_stmt ::=
-    EMIT:x call_expr:e SEMI {:
-        if (!(e instanceof Call)) {
-            return null;
-        }
-
-        RESULT = new Emit((Call)e);
+    EMIT:x NAME:n call_args:a SEMI {:
+        Name event = new Name(n);
+        event.setLoc(new CodeLocation(nleft, nright, filename));
+        RESULT = new Emit(event, a);
         RESULT.setLoc(new CodeLocation(xleft, xright, filename));
     :}
     ;
@@ -1237,12 +1223,10 @@ atomic_stmt ::= ATOMIC:x suite:s exceptall_stmts:es {:
         RESULT.setLoc(new CodeLocation(xleft, xright, filename));
     :};
 
-throw_stmt ::= THROW:x call_expr:e SEMI{:
-        if (!(e instanceof Call)) {
-            return null;
-        }
-
-        RESULT = new Throw((Call)e);
+throw_stmt ::= THROW:x NAME:n call_args:a SEMI{:
+        Name exception = new Name(n);
+        exception.setLoc(new CodeLocation(nleft, nright, filename));
+        RESULT = new Throw(exception, a);
         RESULT.setLoc(new CodeLocation(xleft, xright, filename));
     :};
 
@@ -1594,9 +1578,9 @@ call_expr ::= trailer_expr:e  LPAR RPAR transaction_spec:ts{:
         RESULT = c;
         RESULT.setLoc(new CodeLocation(eleft, eright, filename));
     :}
-    | trailer_expr:e LPAR arglist:c RPAR transaction_spec:ts{:
-             c.setValue(e);
-            c.setSpec(ts);
+    | trailer_expr:e LPAR arglist:a RPAR transaction_spec:ts{:
+             Call c = new Call(e, a);
+             c.setSpec(ts);
              RESULT = c;
              RESULT.setLoc(new CodeLocation(eleft, eright, filename));
     :}
@@ -1606,9 +1590,8 @@ call_expr ::= trailer_expr:e  LPAR RPAR transaction_spec:ts{:
           RESULT = c;
           RESULT.setLoc(new CodeLocation(eleft, eright, filename));
       :}
-      | trailer_expr:e LPAR arglist:c RPAR {:
-               c.setValue(e);
-               RESULT = c;
+      | trailer_expr:e LPAR arglist:a RPAR {:
+               RESULT = new Call(e, a);
                RESULT.setLoc(new CodeLocation(eleft, eright, filename));
       :}
     | atom:a LPAR RPAR transaction_spec:ts  {:
@@ -1624,15 +1607,14 @@ call_expr ::= trailer_expr:e  LPAR RPAR transaction_spec:ts{:
         RESULT = c;
         RESULT.setLoc(new CodeLocation(aleft, aright, filename));
     :}
-    | atom:a LPAR arglist:c RPAR transaction_spec:ts  {:
-        c.setValue(a);
+    | atom:a LPAR arglist:l RPAR transaction_spec:ts  {:
+        Call c = new Call(a, l);
         c.setSpec(ts);
         RESULT = c;
         RESULT.setLoc(new CodeLocation(aleft, aright, filename));
     :}
-    | atom:a LPAR arglist:c RPAR {:
-        c.setValue(a);
-        RESULT = c;
+    | atom:a LPAR arglist:l RPAR {:
+        RESULT = new Call(a, l);
         RESULT.setLoc(new CodeLocation(aleft, aright, filename));
     :}
     ;
@@ -1780,17 +1762,17 @@ trailer ::=
     :};
 arglist ::=
     expr:a {:
-        //System.out.println("parsing first arg for arglist");
-        Call rnt = new Call();
-        rnt.addArg(a);
-        RESULT = rnt;
-        RESULT.setLoc(new CodeLocation(aleft, aright, filename));
+        List<Expression> rtn = new ArrayList<>();
+        rtn.add(a);
+        RESULT = rtn;
     :}
     | arglist:list COMMA expr:a {:
-        //System.out.println("parsing one more arg for arglist");
-        list.addArg(a);
+        list.add(a);
         RESULT = list;
     :};
+call_args ::=
+    LPAR RPAR {: RESULT = new ArrayList<>(); :}
+    | LPAR arglist:a RPAR {: RESULT = a; :};
 //exprlist ::=
 //    exprlist_sub:a {:RESULT = a;:}
 //    | exprlist_sub:a COMMA {:RESULT = a;:};

src/TypeChecker.java

@@ -320,8 +320,10 @@ private static boolean ifcTypecheck(ContractFile contractFile, VisitEnv env,
                 for (Constraint c : trustCons) System.err.println("DBGTRUST[" + methodName + "] " + c.toSherrlocFmt(true));
                 for (Sym s : env.principalSet()) System.err.println("DBGCTOR[" + methodName + "] " + s.toSHErrLocFmt());
                 for (String a : env.rigidAtoms()) System.err.println("DBGATOM[" + methodName + "] " + a);
+                for (String v : env.versionNames()) System.err.println("DBGVER[" + methodName + "] " + v);
             }
-            SherrlocDiagnoser sherrlocDiagnoser = Utils.createDiagnoser(env.principalSet(), trustCons, cons,
+            SherrlocDiagnoser sherrlocDiagnoser = Utils.createDiagnoser(env.principalSet(),
+                    env.versionNames(), trustCons, cons,
                     true, contractSym, env.rigidAtoms(), env.atomAssumptions());
             boolean result;
             try {

src/ast/AnnAssign.java

@@ -151,42 +151,8 @@ public PathOutcome IFCVisit(VisitEnv env, boolean tail_position) throws Semantic
         SLCNameVarLbl = varSym.labelNameSLC();
 //        // logger.debug(varSym.typeSym.getName());
 
-        // If the declared variable is a principal (final address/contract), add it to the principal list
-        if ((varSym.isFinal &&
-                (varSym.typeSym instanceof ContractSym || varSym.typeSym.getName().equals(Utils.ADDRESS_TYPE)))
-                // || varSym.typeSym.name().equals(Utils.PRINCIPAL_TYPE)) Invalid to declare a non-global principal
-                ) {
+        if (varSym.isPrincipalTyped()) {
             env.addPrincipal(varSym);
-
-            VarSym equalPrincipal = null;
-            boolean correctInit = true;
-            if (value instanceof Name) { // assigned as another variable
-                // Nothing to check
-                equalPrincipal = env.getVar(((Name) value).id);
-            } else if (value instanceof Call call && call.isCast(env)) { // assigned as another contract
-                // check if it is a cast to a final address variable
-                Expression arg = call.getArgAt(0);
-                if (arg instanceof Name) {
-                    VarSym sym = env.getVar(((Name) arg).id);
-                    if (!sym.isFinal) {
-                        correctInit = false;
-                    } else {
-                        equalPrincipal = sym;
-                    }
-                } else {
-                    correctInit = false;
-                }
-            } else if (!isBuiltIn) {
-                correctInit = false;
-            }
-
-            if (correctInit) {
-                // add equivalence assumption to the trust set
-                env.checkTrustEqual(SLCNameVar, equalPrincipal.toSHErrLocFmt(), location,
-                        "New principal declaration");
-            } else {
-                throw new SemanticException("A final address/Contract must be initialized to another final address/Contract: " + id, location);
-            }
         }
 
         String ifNamePc = Utils.getLabelNamePc(scopeContext.getSHErrLocName());
@@ -201,6 +167,11 @@ public PathOutcome IFCVisit(VisitEnv env, boolean tail_position) throws Semantic
         if (value != null) {
             env.inContext = beginContext;
             ExpOutcome valueOutcome = value.genIFConstraints(env, scopeContext.isContractLevel());
+            // A principal-typed variable starts out naming the principal it is initialized to.
+            String init = varSym.isPrincipalTyped() ? value.principalName(env) : null;
+            if (init != null) {
+                env.assumeSamePrincipal(SLCNameVar, init);
+            }
             env.checkFlow(valueOutcome.valueLabelName, SLCNameVarLbl, value.location,
                     "Integrity of the value being assigned must be trusted to allow this assignment");
 

src/ast/Arg.java

@@ -117,7 +117,7 @@ public void genConsVisit(VisitEnv env, boolean tail_position) throws SemanticExc
         if (annotation.label() != null) {
             varSym.setLabel(env.toLabel(annotation.label()));
         }
-        if (varSym.typeSym instanceof InterfaceSym || varSym.typeSym.getName().equals(Utils.ADDRESS_TYPE)) {
+        if (varSym.isPrincipalTyped()) {
             env.addPrincipal(varSym);
         }
     }