Statement blocks

src/SCIF.cup

@@ -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,14 +1169,6 @@ 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)) {

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

@@ -20,14 +20,14 @@
 
 public class Atomic extends Statement {
 
-    List<Statement> body;
+    Block body;
     List<ExceptHandler> handlers;
 
     // ArrayList<Statement> orelse;
     // ArrayList<Statement> finalbody;
     public Atomic(List<Statement> body,
             List<ExceptHandler> handlers) {//, ArrayList<Statement> orelse, ArrayList<Statement> finalbody) {
-        this.body = body;
+        this.body = new Block(body);
         this.handlers = handlers;
         // this.orelse = orelse;
         // this.finalbody = finalbody;
@@ -53,10 +53,7 @@ public ScopeContext genTypeConstraints(NTCEnv env, ScopeContext parent) throws S
 //            now.addException(t, false);
 //        }
 
-        for (Statement s : body) {
-//            assert !now.getSHErrLocName().startsWith("null");
-            tmp = s.genTypeConstraints(env, atomicScope);
-        }
+        body.genTypeConstraints(env, atomicScope);
         env.exitNewScope();
         env.exitAtomic();
 
@@ -107,10 +104,11 @@ public List<compile.ast.Statement> solidityCodeGen(CompileEnv code) {
         readMap = new HashMap<>();
         writeMap = new HashMap<>();
 
-        if (body.size() == 1 && body.get(0) instanceof CallStatement && ((CallStatement) body.get(0)).call.value instanceof Attribute) {
+        List<Statement> stmts = body.statements();
+        if (stmts.size() == 1 && stmts.get(0) instanceof CallStatement callStmt && callStmt.call.value instanceof Attribute) {
             // if it is a single call
-            Call call = ((CallStatement) body.get(0)).call;
-            List<compile.ast.Statement> result = body.get(0).solidityCodeGen(code);
+            Call call = callStmt.call;
+            List<compile.ast.Statement> result = callStmt.solidityCodeGen(code);
             if (result.size() == 1 && result.get(0) instanceof ExternalCall) {
                 ExternalCall externalCall = (ExternalCall) result.get(0);
 //                    LowLevelCall lowLevelCall = new LowLevelCall();
@@ -137,14 +135,11 @@ public List<compile.ast.Statement> solidityCodeGen(CompileEnv code) {
 
         if (lowLevelCall == null) {
             // find out read and written local variables
-            for (Statement s : body) {
-                readMap.putAll(s.readMap(code));
-                writeMap.putAll(s.writeMap(code));
-                // solBody.addAll(s.solidityCodeGen(code));
-            }
+            readMap.putAll(body.readMap(code));
+            writeMap.putAll(body.writeMap(code));
             readMap.putAll(writeMap);
             code.enterNewVarScope();
-            Function newTempFunction = code.makeMethod(body, readMap, writeMap, ScopeType.ATOMIC);
+            Function newTempFunction = code.makeMethod(body.statements(), readMap, writeMap, ScopeType.ATOMIC);
             lowLevelCall = new LowLevelCall(newTempFunction, compile.Utils.THIS_ADDRESS,
                     newTempFunction.funcName(), newTempFunction.argNames().stream().map(name -> new SingleVar(name)).collect(
                     Collectors.toList()));
@@ -247,17 +242,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(body.IFCVisit(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 +264,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.statements());
         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);
 
@@ -306,7 +316,7 @@ public void passScopeContext(ScopeContext parent) {
     @Override
     public List<Node> children() {
         List<Node> rtn = new ArrayList<>();
-        rtn.addAll(body);
+        rtn.add(body);
         rtn.addAll(handlers);
         return rtn;
     }
@@ -318,10 +328,7 @@ public boolean exceptionHandlingFree() {
 
     @Override
     protected Map<String,? extends Type> readMap(CompileEnv code) {
-        Map<String, Type> result = new HashMap<>();
-        for (Statement s: body) {
-            result.putAll(s.readMap(code));
-        }
+        Map<String, Type> result = new HashMap<>(body.readMap(code));
         for (ExceptHandler s: handlers) {
             result.putAll(s.readMap(code));
         }
@@ -330,10 +337,7 @@ protected Map<String,? extends Type> readMap(CompileEnv code) {
 
     @Override
     protected Map<String,? extends Type> writeMap(CompileEnv code) {
-        Map<String, Type> result = new HashMap<>();
-        for (Statement s: body) {
-            result.putAll(s.writeMap(code));
-        }
+        Map<String, Type> result = new HashMap<>(body.writeMap(code));
         for (ExceptHandler s: handlers) {
             result.putAll(s.writeMap(code));
         }