Refactor type checking

src/SCIF.cup

@@ -666,10 +666,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));
     :};

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);
         }
     }

src/ast/Assert.java

@@ -35,14 +35,19 @@ public PathOutcome IFCVisit(VisitEnv env, boolean tail_position) throws Semantic
                 VarSym l = env.getVar(left.id), r = env.getVar(right.id);
 //                // logger.debug(l.toString());
 //                // logger.debug(r.toString());
-                Inequality hypo = new Inequality(l.toSHErrLocFmt(), Relation.LEQ,
-                        r.toSHErrLocFmt());
+                Inequality hypo = new Inequality(env.principalName(l), Relation.LEQ,
+                        env.principalName(r));
 
                 env.hypothesis().add(hypo);
             }
 
         }
-        return test.genIFConstraints(env, tail_position).psi;
+        PathOutcome result = test.genIFConstraints(env, tail_position).psi;
+        if (test instanceof ConstantExpr c && c.value == Constant.FALSE) {
+            // An assertion of false always fails, so it never completes normally.
+            return result.withoutNormalPath();
+        }
+        return result;
     }
 
     @Override

src/ast/Assign.java

@@ -16,15 +16,46 @@ public class Assign extends Statement {
 
     Expression target;
     Expression value;
+    /** Whether this assignment is a constructor's initialization of a final field. */
+    private boolean initializesFinalField = false;
 
     public Assign(Expression target, Expression value) {
         this.target = target;
         this.value = value;
     }
 
+    /** The names of the variables assigned by assignments within {@code nodes}. */
+    static java.util.Set<String> assignedNames(List<? extends Node> nodes) {
+        java.util.Set<String> names = new java.util.HashSet<>();
+        for (Node node : nodes) {
+            collectAssignedNames(node, names);
+        }
+        return names;
+    }
+
+    private static void collectAssignedNames(Node node, java.util.Set<String> names) {
+        if (node instanceof Assign a && a.target instanceof Name n) {
+            names.add(n.id);
+        }
+        for (Node child : node.children()) {
+            if (child != null) {
+                collectAssignedNames(child, names);
+            }
+        }
+    }
+
+    /** Marks this assignment as a constructor's initialization of a final field. */
+    void markFinalFieldInit() {
+        initializesFinalField = true;
+    }
+
     @Override
     public ScopeContext genTypeConstraints(NTCEnv env, ScopeContext parent) throws SemanticException {
         ScopeContext now = new ScopeContext(this, parent);
+        if (target instanceof Name n && env.getCurSym(n.id) instanceof VarSym v && v.isFinal
+                && !(initializesFinalField && v.isGlobal())) {
+            throw new SemanticException("cannot assign to final variable " + n.id, location);
+        }
         if (target instanceof Attribute att && att.value.getVarInfo(env) != null
                 && att.value.getVarInfo(env).typeSym instanceof typecheck.ClosureTypeSym
                 && att.attr.id.equals(typecheck.Utils.CLOSURE_TARGET_MEMBER)) {
@@ -58,7 +89,7 @@ public PathOutcome IFCVisit(VisitEnv env, boolean tail_position) throws Semantic
             // env.prevContext = valueContext;
             /*env.cons.add(new Constraint(new Inequality(prevLockName, CompareOperator.Eq, valueContext.lambda), env.hypothesis, value.location, env.curContractSym.name,
                     "Lock should be maintained before execution of this operation"));*/
-            to = target.genIFConstraints(env, false);
+            to = target.genLocationConstraints(env);
             ifNameTgt = to.valueLabelName;
 //            env.inContext = new Context(to.psi.getNormalPath().c.lambda, beginContext.lambda);
             env.inContext = Utils.genNewContextAndConstraints(env, false, to.psi.getNormalPath().c, beginContext.lambda, target.nextPcSHL(), location);
@@ -83,6 +114,16 @@ public PathOutcome IFCVisit(VisitEnv env, boolean tail_position) throws Semantic
                 value.location, "Closure value flowing into the assignment target must subtype its slot");
         }
 
+        // The target names the assigned principal from here on.
+        if (target instanceof Name tgtName && env.getVar(tgtName.id) instanceof VarSym tgtSym
+                && tgtSym.isPrincipalTyped()) {
+            String source = value.principalName(env);
+            String dest = tgtSym.isMutablePrincipal() ? env.newVersion(tgtSym) : tgtSym.toSHErrLocFmt();
+            if (source != null) {
+                env.assumeSamePrincipal(dest, source);
+            }
+        }
+
         typecheck.Utils.contextFlow(env, vo.psi.getNormalPath().c, endContext, value.location);
         // env.outContext = endContext;
 

src/ast/Atomic.java

@@ -247,17 +247,17 @@ public PathOutcome IFCVisit(VisitEnv env, boolean tail_position) throws Semantic
         //env.psi = newPsi;
         PathOutcome psi = new PathOutcome();
         PathOutcome input = new PathOutcome();
+        Map<String, String> versionsBefore = env.saveVersions();
         env.incScopeLayer();
-        PathOutcome so = new PathOutcome(new PsiUnit(beginContext));
-        Utils.genConsStmtsWithException(body, env, so, psi, tail_position);
+        psi.join(Utils.genConsStmtSeq(body, env, tail_position));
         env.decScopeLayer();
         for (ExceptHandler h : handlers) {
-            ExceptionTypeSym expSym = env.getExp(h.name());
+            ExceptionTypeSym expSym = h.exceptionType(env);
             PsiUnit u = psi.psi.get(expSym);
 
             if (u != null) {
                 env.checkFlow(u.c.lambda, beginContext.lambda, location,
-                        "Try clause should maintain locks when throwing exception " + h.name());
+                        "Try clause should maintain locks when throwing exception " + h.type().name());
             /*env.cons.add(new Constraint(new Inequality(u.c.pc, h.), env.hypothesis, location, env.curContractSym.name,
                     "Try clause should maintain locks when throwing exception " + h.name));*/
 
@@ -269,19 +269,34 @@ public PathOutcome IFCVisit(VisitEnv env, boolean tail_position) throws Semantic
         //Context cTry = env.outContext;
 
         //env.psi = oldPsi;
+        // A handler may be entered from any point in the body.
+        List<Map<String, String>> exitVersions = new ArrayList<>();
+        exitVersions.add(env.saveVersions());
+        java.util.Set<String> assignedInBody = ast.Assign.assignedNames(body);
         for (ExceptHandler h : handlers) {
+            env.restoreVersions(versionsBefore);
+            env.havoc(assignedInBody);
             env.incScopeLayer();
             //env.inContext = new Context(h.getHandlerPcLabelName(), beginContext.lambda);
-            ExceptionTypeSym expSym = env.getExp(h.name());
-            PsiUnit expUnit = input.psi.get(expSym);
-            if (expUnit != null) {
+            ExceptionTypeSym expSym = h.exceptionType(env);
+            if (expSym == null) {
+                // Nothing is known about where a failure came from, so a handler for
+                // failures runs with untrusted control flow.
+                env.inContext = new Context(env.curContractSym().any().toSHErrLocFmt(),
+                        beginContext.lambda);
+                PathOutcome ho = h.genConsVisit(env, tail_position);
+                psi.join(ho);
+                exitVersions.add(env.saveVersions());
+            } else if (input.psi.get(expSym) instanceof PsiUnit expUnit) {
                 env.inContext = new Context(expUnit.c.pc, beginContext.lambda);
                 PathOutcome ho = h.genConsVisit(env, tail_position);
                 psi.join(ho);
+                exitVersions.add(env.saveVersions());
             }
             env.decScopeLayer();
             // cTry = new Context(Utils.makeJoin(cTry.pc, env.outContext.outPcName), Utils.makeJoin(cTry.lambda, env.outContext.lockName));
         }
+        env.mergeVersions(exitVersions);
 
         Utils.contextFlow(env, psi.getNormalPath().c, endContext, location);