diff --git a/sherrloc b/sherrloc index 1258900..ab96ffe 160000 --- a/sherrloc +++ b/sherrloc @@ -1 +1 @@ -Subproject commit 125890034012022280d595bcb6740795dd38b687 +Subproject commit ab96ffe03bc7a3666b42f993c40a2a0a5d15ca71 diff --git a/src/Preprocessor.java b/src/Preprocessor.java index 321aba5..e986eb3 100644 --- a/src/Preprocessor.java +++ b/src/Preprocessor.java @@ -34,8 +34,7 @@ public static List preprocess(List inputFiles) throws IOExcept for (File builtinFile : Utils.BUILTIN_FILES) { Symbol result; try { - result = Parser.parse(builtinFile, null); //p.parse() - assert result != null; + result = Parser.parse(builtinFile, null); } catch (SyntaxError se) { continue; } @@ -63,13 +62,7 @@ public static List preprocess(List inputFiles) throws IOExcept // add all contracts from inputFiles recursively while (!mentionedFiles.isEmpty()) { File file = mentionedFiles.poll(); - Symbol result; - try { - result = Parser.parse(file, null); //p.parse() - assert result != null; - } catch (SyntaxError se) { - throw se; - } + Symbol result = Parser.parse(file, null); List rootsFiles = (List) result.value; if (rootsFiles == null || rootsFiles.isEmpty()) { diff --git a/src/SCIF.cup b/src/SCIF.cup index 55fc384..6915edb 100644 --- a/src/SCIF.cup +++ b/src/SCIF.cup @@ -61,6 +61,15 @@ parser code {: errorMessages.add(sb.toString()); } + /** + * Records an error that is not a syntax error at the given position in the file being + * parsed, which makes {@link #parse()} fail. + */ + void reportError(int left, int right, String message) { + hasError = true; + errorMessages.add(ErrorFormatter.format(filename, left, right, message)); + } + @Override public void report_error(String message, Object info) { // only used by CUP internals; actual reporting is done in syntax_error hasError = true; @@ -99,35 +108,39 @@ parser code {: parse(inputFile, null); } catch (SyntaxError err) { /* ignore */ + } catch (FileNotFoundException e) { + System.err.println("File not found: " + e.getMessage()); } } - public static Symbol parse(File inputFile, File astFile) throws SyntaxError { - Symbol rtn = null; + /** + * Parses {@code inputFile}, writing the AST to {@code astFile} if it is not null. + * + * @throws SyntaxError if the file has syntax errors or imports a file that does not exist + * @throws FileNotFoundException if {@code inputFile} cannot be read + */ + public static Symbol parse(File inputFile, File astFile) + throws SyntaxError, FileNotFoundException { + filename = inputFile.getAbsolutePath(); + Lexer lexer = new Lexer(new FileReader(inputFile)); + + if (astFile != null) { + PrintStream ps = new PrintStream(new FileOutputStream(astFile)); + System.setErr(ps); + } + + Parser p = new Parser(lexer); + + Symbol rtn; try { - filename = inputFile.getAbsolutePath(); - Lexer lexer = new Lexer(new FileReader(inputFile)); - - if (astFile != null) { - PrintStream ps = new PrintStream(new FileOutputStream(astFile)); - System.setErr(ps); - } - - Parser p = new Parser(lexer); - - try { - rtn = p.parse(); - } catch (SyntaxError se) { - throw se; - } catch (Exception e) { - throw new Error("Unexpected exception from parser"); - } - if (astFile != null) { - System.setErr(System.err); - } - } catch (FileNotFoundException e) { - System.err.println("File not found: " + e.getMessage()); - return null; + rtn = p.parse(); + } catch (SyntaxError se) { + throw se; + } catch (Exception e) { + throw new Error("Unexpected exception from parser"); + } + if (astFile != null) { + System.setErr(System.err); } return rtn; } @@ -227,7 +240,7 @@ nonterminal TrailerExpr trailer; //nonterminal Setmaker setmaker; // nonterminal Setmaker setmaker_sub; // nonterminal ClassDef classdef; -nonterminal Call arglist; +nonterminal List arglist, call_args; nonterminal LabeledType labeledType, maybeLabeledType; nonterminal ast.ClosureType closureType; nonterminal List throwsOpt; @@ -269,7 +282,6 @@ nonterminal List except_types; nonterminal Throw throw_stmt; nonterminal List constructors; nonterminal FunctionDef constructor; -//nonterminal EndorseStatement endorse_stmt; nonterminal EndorseIfStatement endorseIf_stmt; nonterminal Call call_expr; nonterminal Revert revert_stmt; @@ -368,8 +380,14 @@ ipt_stmts ::= ipt_stmt ::= ipt_name:a SEMI {:RESULT = a; :}; ipt_name ::= IMPORT:x STRING_LITERAL:a {: - RESULT = a;//new Import(); - //RESULT.setLoc(new CodeLocation(xleft, xright, filename)); + java.nio.file.Path path = java.nio.file.Paths.get((String) a); + if (!path.isAbsolute()) { + path = java.nio.file.Paths.get(filename).getParent().resolve(path); + } + if (!java.nio.file.Files.isRegularFile(path)) { + parser.reportError(aleft, aright, "imported file not found: " + a); + } + RESULT = a; :}; // //ipt_as_names ::= @@ -666,10 +684,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 +1176,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 +1188,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 +1242,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 +1597,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 +1609,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 +1626,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 +1781,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 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;:}; diff --git a/src/SCIF.java b/src/SCIF.java index d03cc63..f47e28b 100644 --- a/src/SCIF.java +++ b/src/SCIF.java @@ -168,6 +168,9 @@ public Integer call() { } catch (TypeCheckFailure e) { System.out.println(e.getMessage()); return 0; + } catch (java.io.FileNotFoundException e) { + System.out.println("File not found: " + e.getMessage()); + return 1; } catch (Exception e) { System.out.println("Unexpected exception:"); e.printStackTrace(); @@ -218,6 +221,9 @@ public Integer call() { Parser.parse(m_inputFiles[0], astOutputFile); } catch (Parser.SyntaxError e) { /* skip */ + } catch (java.io.FileNotFoundException e) { + System.out.println("File not found: " + e.getMessage()); + return 1; } } else if (m_funcRequest.tokenize) { LexerTest.tokenize(m_inputFiles[0]); diff --git a/src/TypeChecker.java b/src/TypeChecker.java index 6c5e885..bbe16fb 100644 --- a/src/TypeChecker.java +++ b/src/TypeChecker.java @@ -62,7 +62,7 @@ public static boolean regularTypecheck(List roots, if (DEBUG) { System.err.println("regular type-checking using SLC..."); } - if (!runSLC(ntcEnv.programMap(), sherrlocDiagnoser, DEBUG)) { + if (!runSLC(ntcEnv.programMap(), sherrlocDiagnoser, false, DEBUG)) { return false; } } catch (Exception e) { @@ -196,10 +196,7 @@ private static void buildSignatureConstraints(String contractName, VisitEnv env, // "The Code integrity label of contract " + ifNameContract + " may be incorrect")); for (Assumption assumption : contractSym.assumptions()) { - env.addTrustConstraint(new Constraint( - assumption.toInequality(), - assumption.location(), - "Static trust relationship")); + env.assume(assumption.toInequality()); } } else { // TODO: handle the assumptions of other contracts @@ -227,20 +224,20 @@ private static void buildSignatureConstraints(String contractName, VisitEnv env, cons.add(new Constraint( new Inequality(ifCallBeforeLabel, Relation.EQ, ifNameCallBeforeLabel), func.external_pc.location(), - "Integrity requirement to call this method may be incorrect")); + "The external begin label of " + func.funcName + " may be wrong")); } if (ifCallAfterLabel != null) { cons.add(new Constraint( new Inequality(ifCallAfterLabel, Relation.EQ, ifNameCallAfterLabel), func.internal_pc.location(), - "Integrity pc level autoendorsed to when calling this method may be incorrect")); + "The internal begin label of " + func.funcName + " may be wrong")); } if (ifCallLockLabel != null) { cons.add(new Constraint( new Inequality(ifCallLockLabel, Relation.EQ, ifNameCallGammaLabel), func.gamma.location(), - "The final reentrancy lock label may be declared incorrectly")); + "The reentrancy lock label of " + func.funcName + " may be wrong")); } @@ -250,7 +247,7 @@ private static void buildSignatureConstraints(String contractName, VisitEnv env, cons.add(new Constraint( new Inequality(ifReturnLabel, Relation.EQ, ifNameReturnLabel), func.location, - "Integrity label of this method's return value may be incorrect")); + "The label of the return value of " + func.funcName + " may be wrong")); } for (int i = 0; i < func.parameters.size(); ++i) { @@ -262,12 +259,12 @@ private static void buildSignatureConstraints(String contractName, VisitEnv env, if (ifArgLabel != null) { cons.add(new Constraint(new Inequality(ifNameArgLabel, Relation.EQ, ifArgLabel), arg.location, - "Argument " + arg.getName() + " may be labeled incorrectly")); + "The label of parameter " + arg.getName() + " may be wrong")); env.addTrustConstraint( new Constraint(new Inequality(ifNameCallBeforeLabel, ifNameArgLabel), arg.location, - "Argument " + arg.getName() - + " must be no more trusted than caller's integrity")); + "Parameter " + arg.getName() + " cannot be trusted more than the " + + "external begin label of " + func.funcName)); } } @@ -291,7 +288,7 @@ private static boolean ifcTypecheck(ContractFile contractFile, VisitEnv env, if (ifLabel != null && varName != null) { env.cons.add( new Constraint(new Inequality(varName, Relation.EQ, ifLabel), var.location, - "Variable " + var.getName() + " may be labeled incorrectly")); + "The label of field " + var.getName() + " may be wrong")); } } @@ -320,12 +317,14 @@ 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, - true, contractSym, env.rigidAtoms(), env.atomAssumptions()); + SherrlocDiagnoser sherrlocDiagnoser = Utils.createDiagnoser(env.principalSet(), + env.versionNames(), trustCons, cons, + true, contractSym, env.rigidAtoms(), env.assumptions()); boolean result; try { - result = runSLC(env.programMap, sherrlocDiagnoser, DEBUG); + result = runSLC(env.programMap, sherrlocDiagnoser, true, DEBUG); } catch (Exception e) { System.out.println(e.getMessage()); return false; @@ -336,8 +335,13 @@ private static boolean ifcTypecheck(ContractFile contractFile, VisitEnv env, } + /** + * Solves the constraints of {@code sherrlocDiagnoser}, reporting the likely causes of any + * failure for the source files in {@code programMap}, and returns whether they were + * satisfied. The constraints are on labels if {@code ifc}, and on types otherwise. + */ static boolean runSLC(Map> programMap, SherrlocDiagnoser sherrlocDiagnoser, - boolean DEBUG) { + boolean ifc, boolean DEBUG) { // logger.trace("running SLC"); if (sherrlocDiagnoser == null) { // There were no constraints return true; @@ -373,7 +377,7 @@ static boolean runSLC(Map> programMap, SherrlocDiagnose System.out.println("Some other possible places:"); } List s = Utils.SLCEntitiesToStrings(programMap, result.getSuggestions().get(i), - DEBUG); + ifc, DEBUG); if (s != null) { for (String exp: s) { if (!expSet.contains(exp)) { diff --git a/src/ast/AnnAssign.java b/src/ast/AnnAssign.java index 5dcb2f5..18f655c 100644 --- a/src/ast/AnnAssign.java +++ b/src/ast/AnnAssign.java @@ -102,10 +102,10 @@ public ScopeContext genTypeConstraints(NTCEnv env, ScopeContext parent) throws S ScopeContext type = annotation.genTypeConstraints(env, now); ScopeContext tgt = target.genTypeConstraints(env, now); - env.addCons(type.genTypeConstraints(tgt, Relation.EQ, env, location)); + env.addCons(type.genTypeConstraints(tgt, Relation.EQ, env, location, "Variable " + target.id + " has its declared type")); if (value != null) { ScopeContext v = value.genTypeConstraints(env, now); - env.addCons(tgt.genTypeConstraints(v, Relation.LEQ, env, location)); + env.addCons(tgt.genTypeConstraints(v, Relation.LEQ, env, location, "The initial value must have the declared type of " + target.id)); } else if (isFinal) { throw new SemanticException("final variable " + name + " not initialized", location); } @@ -143,56 +143,22 @@ public PathOutcome IFCVisit(VisitEnv env, boolean tail_position) throws Semantic if (annotation.label() != null) { varSym.setLabel(env.toLabel(annotation.label())); } - env.checkEqual(varSym.labelNameSLC(), varSym.labelValueSLC(), location, "Variable " - + varSym.getName() + " may be labeled incorrectly"); + env.checkEqual(varSym.labelNameSLC(), varSym.labelValueSLC(), location, "The label of variable " + + varSym.getName() + " may be wrong"); } // // logger.debug(varSym.getName()); SLCNameVar = varSym.toSHErrLocFmt(); 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()); env.checkFlow(ifNamePc, SLCNameVarLbl, location, - "Integrity of control flow must be trusted to allow this assignment"); + "Control flow must be trusted at the label of " + target.id + " to initialize it"); if (!tail_position) { env.checkFlow(endContext.lambda, beginContext.lambda, location, @@ -201,13 +167,18 @@ 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"); + "The initial value must be trusted at the label of " + target.id); if (varSym.typeSym instanceof typecheck.ClosureTypeSym targetCs) { ClosureCreation.checkFlowInto(value, targetCs, new java.util.HashMap<>(), env, value.location, - "Closure value flowing into the declared variable type must subtype its slot"); + "The closure's labels must be compatible with the declared type of " + target.id); } typecheck.Utils.contextFlow(env, valueOutcome.psi.getNormalPath().c, endContext, value.location); diff --git a/src/ast/Arg.java b/src/ast/Arg.java index 8071700..3e4f206 100644 --- a/src/ast/Arg.java +++ b/src/ast/Arg.java @@ -88,7 +88,7 @@ public ScopeContext genTypeConstraints(NTCEnv env, ScopeContext parent) throws S } ScopeContext type = annotation.genTypeConstraints(env, now); - env.addCons(type.genTypeConstraints(now, Relation.EQ, env, location)); + env.addCons(type.genTypeConstraints(now, Relation.EQ, env, location, "Parameter " + name + " has its declared type")); return now; } @@ -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); } } diff --git a/src/ast/ArrayOperation.java b/src/ast/ArrayOperation.java new file mode 100644 index 0000000..6419996 --- /dev/null +++ b/src/ast/ArrayOperation.java @@ -0,0 +1,179 @@ +package ast; + +import compile.CompileEnv; +import compile.ast.Attr; +import compile.ast.ExternalCall; +import compile.ast.Statement; +import java.util.ArrayList; +import java.util.HashMap; +import java.util.List; +import java.util.Map; +import typecheck.ArrayTypeSym; +import typecheck.BuiltInT; +import typecheck.Context; +import typecheck.ExpOutcome; +import typecheck.NTCEnv; +import typecheck.PathOutcome; +import typecheck.PsiUnit; +import typecheck.ScopeContext; +import typecheck.TypeSym; +import typecheck.Utils; +import typecheck.VarSym; +import typecheck.VisitEnv; +import typecheck.exceptions.SemanticException; +import typecheck.sherrlocUtils.Relation; + +/** + * A built-in operation on an array, written {@code a.op(args)}: {@code push(x)}, {@code pop()} + * or {@code length()}. The parser cannot tell it from a call, so the regular type check + * resolves a {@link Call} to it. + */ +public class ArrayOperation extends Expression { + + private final Expression array; + private final String op; + private final List args; + + /** The operation {@code op} on the array {@code array}, with arguments {@code args}. */ + ArrayOperation(Expression array, String op, List args) { + this.array = array; + this.op = op; + this.args = args; + } + + @Override + public ScopeContext genTypeConstraints(NTCEnv env, ScopeContext parent) + throws SemanticException { + ScopeContext now = new ScopeContext(this, parent); + if (!(array instanceof Name)) { + array.genTypeConstraints(env, now); + } + ArrayTypeSym arrayType = (ArrayTypeSym) array.getVarInfo(env).typeSym; + String elementType = arrayType.valueType.toSHErrLocFmt(); + TypeSym voidType = (TypeSym) env.getSym(BuiltInT.VOID); + switch (op) { + case "pop" -> { + if (!args.isEmpty()) { + throw new SemanticException("pop expects 0 arguments", location); + } + env.addCons(now.genTypeConstraints(voidType.toSHErrLocFmt(), Relation.EQ, env, + location, "pop() returns no value")); + } + case "push" -> { + if (args.size() != 1) { + throw new SemanticException("push expects 1 argument", location); + } + Expression arg = args.get(0); + ScopeContext argContext = arg.genTypeConstraints(env, now); + env.addCons(argContext.genTypeConstraints(elementType, Relation.GEQ, env, + arg.location, "The pushed element must have the array's element type")); + env.addCons(now.genTypeConstraints(voidType.toSHErrLocFmt(), Relation.EQ, env, + location, "push() returns no value")); + } + case "length" -> { + if (!args.isEmpty()) { + throw new SemanticException("length expects 0 arguments", location); + } + TypeSym uintType = (TypeSym) env.getSym(BuiltInT.UINT); + env.addCons(now.genTypeConstraints(uintType.toSHErrLocFmt(), Relation.EQ, env, + location, "length() returns a uint")); + } + default -> throw new SemanticException("type error: unknown array operator", + location); + } + return now; + } + + /** + * {@code push} and {@code pop} modify the array, so the control flow, and the element + * pushed, must be trusted at the array's location. {@code length} is trusted as much as + * the array. + */ + @Override + protected ExpOutcome genFlowConstraints(VisitEnv env, boolean tail_position) + throws SemanticException { + Context beginContext = env.inContext; + Context endContext = new Context(Utils.getLabelNamePc(toSHErrLocFmt()), + Utils.getLabelNameLock(toSHErrLocFmt())); + PathOutcome psi = new PathOutcome(new PsiUnit(endContext)); + List argLabels = new ArrayList<>(); + for (Expression arg : args) { + ExpOutcome ao = arg.genIFConstraints(env, false); + psi.joinExe(ao.psi); + argLabels.add(ao.valueLabelName); + env.inContext = Utils.genNewContextAndConstraints(env, false, + ao.psi.getNormalPath().c, beginContext.lambda, arg.nextPcSHL(), + arg.location); + } + ExpOutcome vo = array.genIFConstraints(env, false); + psi.joinExe(vo.psi); + String ifNamePc = Utils.getLabelNamePc(scopeContext.getSHErrLocName()); + String result = ifNamePc; + if (op.equals("length")) { + result = vo.valueLabelName; + } else { + String arrayLocation = array.genLocationConstraints(env).valueLabelName; + env.checkFlow(ifNamePc, arrayLocation, location, + "Control flow must be trusted at the label of the array to modify it"); + if (op.equals("push")) { + env.checkFlow(argLabels.get(0), arrayLocation, location, + "The pushed element must be trusted at the label of the array"); + } + } + Utils.contextFlow(env, psi.getNormalPath().c, endContext, location); + if (!tail_position) { + env.checkFlow(psi.getNormalPath().c.lambda, beginContext.lambda, location, + Utils.ERROR_MESSAGE_LOCK_IN_NONLAST_OPERATION); + } + return new ExpOutcome(result, psi); + } + + @Override + protected TypeSym staticType(VisitEnv env) { + return env.builtinType(op.equals("length") ? BuiltInT.UINT : BuiltInT.VOID); + } + + @Override + public compile.ast.Expression solidityCodeGen(List result, CompileEnv code) { + List argExps = new ArrayList<>(); + for (Expression arg : args) { + argExps.add(arg.solidityCodeGen(result, code)); + } + compile.ast.Expression target = array.solidityCodeGen(result, code); + if (op.equals("length")) { + return new Attr(target, op); + } + return new ExternalCall(target, op, argExps, null); + } + + @Override + public boolean typeMatch(Expression expression) { + if (!(expression instanceof ArrayOperation o) || !op.equals(o.op) + || !array.typeMatch(o.array) || args.size() != o.args.size()) { + return false; + } + for (int i = 0; i < args.size(); ++i) { + if (!args.get(i).typeMatch(o.args.get(i))) { + return false; + } + } + return true; + } + + @Override + public Map readMap(CompileEnv code) { + Map result = new HashMap<>(); + for (Expression arg : args) { + result.putAll(arg.readMap(code)); + } + return result; + } + + @Override + public List children() { + List rtn = new ArrayList<>(); + rtn.add(array); + rtn.addAll(args); + return rtn; + } +} diff --git a/src/ast/Assert.java b/src/ast/Assert.java index 1e43090..1a29a9d 100644 --- a/src/ast/Assert.java +++ b/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 @@ -50,7 +55,7 @@ public ScopeContext genTypeConstraints(NTCEnv env, ScopeContext parent) throws S ScopeContext now = scopeContext; ScopeContext rtn = null; rtn = test.genTypeConstraints(env, now); - Constraint testCon = rtn.genTypeConstraints(Utils.BuiltinType2ID(BuiltInT.BOOL), Relation.EQ, env, test.location); + Constraint testCon = rtn.genTypeConstraints(Utils.BuiltinType2ID(BuiltInT.BOOL), Relation.EQ, env, test.location, "The asserted condition must be a bool"); env.addCons(testCon); return now; } diff --git a/src/ast/Assign.java b/src/ast/Assign.java index b17d9c0..746487b 100644 --- a/src/ast/Assign.java +++ b/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 assignedNames(List nodes) { + java.util.Set names = new java.util.HashSet<>(); + for (Node node : nodes) { + collectAssignedNames(node, names); + } + return names; + } + + private static void collectAssignedNames(Node node, java.util.Set 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)) { @@ -36,7 +67,7 @@ public ScopeContext genTypeConstraints(NTCEnv env, ScopeContext parent) throws S // // logger.debug(v); // // logger.debug(env); // // logger.debug(location); - env.addCons(tgt.genTypeConstraints(v, Relation.LEQ, env, location)); + env.addCons(tgt.genTypeConstraints(v, Relation.LEQ, env, location, "The assigned value must have the type of the assignment target")); return now; } @@ -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); @@ -72,15 +103,25 @@ public PathOutcome IFCVisit(VisitEnv env, boolean tail_position) throws Semantic // prevContext = valueContext; env.checkFlow(ifNameValue, ifNameTgt, value.location, - "Integrity of the value being assigned must be trusted to allow this assignment"); + "The assigned value must be trusted at the label of the assignment target"); env.checkFlow(ifNamePc, ifNameTgt, value.location, - "Integrity of control flow must be trusted to allow this assignment"); + "Control flow must be trusted at the label of the assignment target"); if (target instanceof Name tgtName && env.getVar(tgtName.id).typeSym instanceof typecheck.ClosureTypeSym targetCs) { ClosureCreation.checkFlowInto(value, targetCs, new java.util.HashMap<>(), env, - value.location, "Closure value flowing into the assignment target must subtype its slot"); + value.location, "The closure's labels must be compatible with the type of the assignment target"); + } + + // 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); diff --git a/src/ast/Atomic.java b/src/ast/Atomic.java index 3bc9db7..9d3f70f 100644 --- a/src/ast/Atomic.java +++ b/src/ast/Atomic.java @@ -20,14 +20,14 @@ public class Atomic extends Statement { - List body; + Block body; List handlers; // ArrayList orelse; // ArrayList finalbody; public Atomic(List body, List handlers) {//, ArrayList orelse, ArrayList 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 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 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 result = body.get(0).solidityCodeGen(code); + Call call = callStmt.call; + List 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 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 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()); + "The atomic block must maintain the reentrancy lock when it throws " + 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> exitVersions = new ArrayList<>(); + exitVersions.add(env.saveVersions()); + java.util.Set 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 children() { List rtn = new ArrayList<>(); - rtn.addAll(body); + rtn.add(body); rtn.addAll(handlers); return rtn; } @@ -318,10 +328,7 @@ public boolean exceptionHandlingFree() { @Override protected Map readMap(CompileEnv code) { - Map result = new HashMap<>(); - for (Statement s: body) { - result.putAll(s.readMap(code)); - } + Map result = new HashMap<>(body.readMap(code)); for (ExceptHandler s: handlers) { result.putAll(s.readMap(code)); } @@ -330,10 +337,7 @@ protected Map readMap(CompileEnv code) { @Override protected Map writeMap(CompileEnv code) { - Map result = new HashMap<>(); - for (Statement s: body) { - result.putAll(s.writeMap(code)); - } + Map result = new HashMap<>(body.writeMap(code)); for (ExceptHandler s: handlers) { result.putAll(s.writeMap(code)); } diff --git a/src/ast/Attribute.java b/src/ast/Attribute.java index 03ff066..155a636 100644 --- a/src/ast/Attribute.java +++ b/src/ast/Attribute.java @@ -37,7 +37,7 @@ public Attribute(Expression v, Name a) { public ScopeContext genTypeConstraints(NTCEnv env, ScopeContext parent) throws SemanticException { VarSym varSym = getVarInfo(env); ScopeContext now = new ScopeContext(this, parent); - env.addCons(now.genTypeConstraints(varSym.typeSym.getName(), Relation.EQ, env, location)); + env.addCons(now.genTypeConstraints(varSym.typeSym.getName(), Relation.EQ, env, location, "Member " + attr.id + " has its declared type")); return now; } @@ -86,39 +86,83 @@ public VarSym getVarInfo(NTCEnv env) throws SemanticException { } @Override - public ExpOutcome genIFConstraints(VisitEnv env, boolean tail_position) throws SemanticException { - //TODO: assuming only one-level attribute access - // to add support to multi-level access - String varName = ((Name) value).id; - // TODO: steph: needs to check instanceof - - VarSym varSym = env.getVar(varName); - if (varSym != null && varSym.typeSym instanceof ClosureTypeSym - && attr.id.equals(Utils.CLOSURE_TARGET_MEMBER)) { - return value.genIFConstraints(env, tail_position); - } - if (!(varSym.typeSym instanceof StructTypeSym structType)) { - //TODO: throw errors: variable not struct -// return null; - throw new RuntimeException("Variable not a struct: " + varName); - } - - //String prevLockName = env.prevContext.lambda; + protected ExpOutcome genFlowConstraints(VisitEnv env, boolean tail_position) throws SemanticException { ExpOutcome vo = value.genIFConstraints(env, tail_position); + TypeSym baseType = value.type(); + if (baseType instanceof ClosureTypeSym && attr.id.equals(Utils.CLOSURE_TARGET_MEMBER)) { + return vo; + } + // A member is trusted at its label and no more than the value it belongs to. String attrValueLabel = vo.valueLabelName; -// String ifAttLabel = structType.getMemberLabel(attr.id); + if (baseType instanceof StructTypeSym structType) { + attrValueLabel = Utils.joinLabels(attrValueLabel, + memberLabel(env, structType.member(attr.id).ifl, attrValueLabel)); + } else if (baseType instanceof ExceptionTypeSym expType) { + // Each principal parameter in the label stands for the principal in that field. + java.util.Map mapping = new java.util.HashMap<>(); + for (VarSym param : expType.parameters()) { + if (param.isPrincipalTyped()) { + mapping.put(param.toSHErrLocFmt(), value instanceof Name n + ? exceptionFieldPrincipal(env, env.getVar(n.id), param.getName()) + : env.curContractSym().any().toSHErrLocFmt()); + } + } + VarSym member = expType.getMemberVarInfo("", attr.id); + attrValueLabel = Utils.joinLabels(attrValueLabel, member.ifl.toSHErrLocFmt(mapping)); + } else { + throw new AssertionError("no member " + attr.id + " in type " + baseType.getName()); + } String ifNameRnt = scopeContext.getSHErrLocName() + ".struct" + location.toString(); -// env.cons.add(new Constraint(new Inequality(ifNameRnt, ifAttLabel), env.hypothesis(), location, -// env.curContractSym().getName(), -// "Integrity of the member")); -// if (!ifAttLabel.equals(attrValueLabel)) { - env.checkEqual(attrValueLabel, ifNameRnt, location, - "Integrity of the index value must be trusted to indicate the attribute"); -// } - + env.checkEqual(attrValueLabel, ifNameRnt, location, + "Member " + attr.id + " is trusted no more than its label and the value it is read from"); return new ExpOutcome(ifNameRnt, vo.psi); } + @Override + public String principalName(VisitEnv env) { + if (value instanceof Name n && env.getCurSym(n.id) instanceof VarSym v + && v.typeSym instanceof ExceptionTypeSym expType) { + for (VarSym param : expType.parameters()) { + if (param.getName().equals(attr.id) && param.isPrincipalTyped()) { + return exceptionFieldPrincipal(env, v, attr.id); + } + } + } + return null; + } + + /** + * The label {@code label} of a struct member, as this contract reads it in a struct value + * labeled {@code structLabel}. A struct declared by another contract labels its members in + * that contract's terms: its {@code this} is trusted only as much as the value, its top and + * bottom principals are this contract's, and any other principal it names is unknown here. + */ + private static String memberLabel(VisitEnv env, Label label, String structLabel) { + String own = env.thisSym().toSHErrLocFmt(); + String namespace = own.substring(0, own.length() - Utils.LABEL_THIS.length()); + java.util.Map mapping = new java.util.HashMap<>(); + for (VarSym p : label.principalSyms()) { + String name = p.toSHErrLocFmt(); + if (name.startsWith(namespace)) { + continue; + } + mapping.put(name, switch (p.getName()) { + case Utils.LABEL_THIS -> structLabel; + case Utils.LABEL_TOP -> env.curContractSym().top().toSHErrLocFmt(); + default -> env.curContractSym().any().toSHErrLocFmt(); + }); + } + return label.toSHErrLocFmt(mapping); + } + + /** + * The principal held by the principal-typed field {@code field} of the caught exception + * {@code exception}, registered in {@code env}. Nothing is known about it. + */ + private static String exceptionFieldPrincipal(VisitEnv env, VarSym exception, String field) { + return env.freshPrincipal(exception.toSHErrLocFmt() + "." + field); + } + @Override public compile.ast.Expression solidityCodeGen(List result, CompileEnv code) { if (isClosureTarget) { @@ -172,4 +216,42 @@ public java.util.Map readMap(CompileEnv code) { public Map writeMap(CompileEnv code) { return value.writeMap(code); } + + @Override + protected TypeSym staticType(VisitEnv env) { + TypeSym base = value.type(); + if (base instanceof ClosureTypeSym && attr.id.equals(Utils.CLOSURE_TARGET_MEMBER)) { + return env.builtinType(BuiltInT.ADDRESS); + } else if (base instanceof StructTypeSym structType) { + return structType.member(attr.id).typeSym; + } else if (base instanceof ExceptionTypeSym expType) { + return expType.getMemberVarInfo("", attr.id).typeSym; + } + throw new AssertionError("no member " + attr.id + " in type " + base.getName()); + } + + @Override + protected ExpOutcome genLocationFlow(VisitEnv env) throws SemanticException { + ExpOutcome bo = value.genLocationConstraints(env); + TypeSym baseType = value.type(); + String location = bo.valueLabelName; + if (baseType instanceof StructTypeSym structType) { + location = Utils.joinLabels(location, + memberLabel(env, structType.member(attr.id).ifl, bo.valueLabelName)); + } else if (baseType instanceof ExceptionTypeSym expType) { + java.util.Map mapping = new java.util.HashMap<>(); + for (VarSym param : expType.parameters()) { + if (param.isPrincipalTyped()) { + mapping.put(param.toSHErrLocFmt(), value instanceof Name n + ? exceptionFieldPrincipal(env, env.getVar(n.id), param.getName()) + : env.curContractSym().any().toSHErrLocFmt()); + } + } + location = Utils.joinLabels(location, + expType.getMemberVarInfo("", attr.id).ifl.toSHErrLocFmt(mapping)); + } else { + throw new SemanticException("member " + attr.id + " cannot be assigned", this.location); + } + return new ExpOutcome(location, bo.psi); + } } diff --git a/src/ast/BinOp.java b/src/ast/BinOp.java index 182a3b4..89ec992 100644 --- a/src/ast/BinOp.java +++ b/src/ast/BinOp.java @@ -36,14 +36,14 @@ public ScopeContext genTypeConstraints(NTCEnv env, ScopeContext parent) throws S ScopeContext r = right.genTypeConstraints(env, now); // // logger.debug("binOp/right:"); // // logger.debug(r.toString()); - env.addCons(now.genTypeConstraints(l, Relation.LEQ, env, location)); - env.addCons(now.genTypeConstraints(r, Relation.LEQ, env, location)); - env.addCons(now.genTypeConstraints(env.getSymName(BuiltInT.UINT), Relation.EQ, env, location)); + env.addCons(now.genTypeConstraints(l, Relation.LEQ, env, location, "The operands of an arithmetic operation must be uint")); + env.addCons(now.genTypeConstraints(r, Relation.LEQ, env, location, "The operands of an arithmetic operation must be uint")); + env.addCons(now.genTypeConstraints(env.getSymName(BuiltInT.UINT), Relation.EQ, env, location, "An arithmetic operation returns a uint")); return now; } @Override - public ExpOutcome genIFConstraints(VisitEnv env, boolean tail_position) throws SemanticException { + protected ExpOutcome genFlowConstraints(VisitEnv env, boolean tail_position) throws SemanticException { Context beginContext = env.inContext; Context endContext = new Context(typecheck.Utils.getLabelNamePc(toSHErrLocFmt()), typecheck.Utils.getLabelNameLock(toSHErrLocFmt())); @@ -60,9 +60,9 @@ public ExpOutcome genIFConstraints(VisitEnv env, boolean tail_position) throws S String ifNameRtn = scopeContext.getSHErrLocName() + "." + "bin" + location.toString(); env.checkFlow(ifNameLeft, ifNameRtn, left.location, - "Integrity of left hand expression doesn't flow to value of this binary operation"); + "The result of an operation is trusted no more than its left operand"); env.checkFlow(ifNameRight, ifNameRtn, right.location, - "Integrity of right hand expression doesn't flow to value of this binary operation"); + "The result of an operation is trusted no more than its right operand"); typecheck.Utils.contextFlow(env, ro.psi.getNormalPath().c, endContext, right.location); // env.outContext = endContext; @@ -110,4 +110,9 @@ public java.util.Map readMap(CompileEnv code) { result.putAll(right.readMap(code)); return result; } + + @Override + protected TypeSym staticType(VisitEnv env) { + return env.builtinType(BuiltInT.UINT); + } } diff --git a/src/ast/Block.java b/src/ast/Block.java new file mode 100644 index 0000000..b228647 --- /dev/null +++ b/src/ast/Block.java @@ -0,0 +1,124 @@ +package ast; + +import compile.CompileEnv; +import compile.ast.Type; +import java.util.ArrayList; +import java.util.Collections; +import java.util.HashMap; +import java.util.List; +import java.util.Map; +import typecheck.NTCEnv; +import typecheck.PathOutcome; +import typecheck.PsiUnit; +import typecheck.ScopeContext; +import typecheck.Utils; +import typecheck.VisitEnv; +import typecheck.exceptions.SemanticException; + +/** + * A sequence of statements executed in order, such as the body of a method or a branch of a + * conditional. A block does not introduce a scope; the construct that contains it decides + * which scopes its statements are in. + */ +public class Block extends Statement { + + private final List statements; + + public Block(List statements) { + this.statements = new ArrayList<>(statements); + } + + /** The statements of this block, in order. */ + public List statements() { + return Collections.unmodifiableList(statements); + } + + /** Whether this block has no statements. */ + public boolean isEmpty() { + return statements.isEmpty(); + } + + /** + * Generates the type constraints of each statement in the scope context {@code parent}, + * and returns the scope context of the last statement, or {@code parent} if there is none. + */ + @Override + public ScopeContext genTypeConstraints(NTCEnv env, ScopeContext parent) + throws SemanticException { + ScopeContext last = parent; + for (Statement s : statements) { + last = s.genTypeConstraints(env, parent); + } + return last; + } + + /** + * Generates the information-flow constraints for this block, which starts in the context + * {@code env.inContext}, and returns every way it can terminate: its exception and return + * paths, and its normal path if it can complete normally. The last statement is in tail + * position if {@code tail_position} is. On return, {@code env.inContext} is the context + * after the last statement that completed normally. + */ + @Override + public PathOutcome IFCVisit(VisitEnv env, boolean tail_position) throws SemanticException { + PathOutcome result = new PathOutcome(); + int index = 0; + for (Statement s : statements) { + ++index; + String prevLambda = env.inContext.lambda; + boolean isTail = index == statements.size() && tail_position; + PathOutcome so = s.IFCVisit(env, isTail); + PsiUnit normal = so.getNormalPath(); + result.join(so.withoutNormalPath()); + if (normal == null) { + return result; + } + env.inContext = Utils.genNewContextAndConstraints(env, isTail, normal.c, prevLambda, + s.nextPcSHL(), s.location()); + } + result.setNormalPath(env.inContext); + return result; + } + + @Override + public List solidityCodeGen(CompileEnv code) { + List result = new ArrayList<>(); + for (Statement s : statements) { + result.addAll(s.solidityCodeGen(code)); + } + return result; + } + + @Override + public List children() { + return new ArrayList<>(statements); + } + + @Override + public boolean exceptionHandlingFree() { + for (Statement s : statements) { + if (!s.exceptionHandlingFree()) { + return false; + } + } + return true; + } + + @Override + protected Map readMap(CompileEnv code) { + Map result = new HashMap<>(); + for (Statement s : statements) { + result.putAll(s.readMap(code)); + } + return result; + } + + @Override + protected Map writeMap(CompileEnv code) { + Map result = new HashMap<>(); + for (Statement s : statements) { + result.putAll(s.writeMap(code)); + } + return result; + } +} diff --git a/src/ast/BoolOp.java b/src/ast/BoolOp.java index c257648..e1e90bc 100644 --- a/src/ast/BoolOp.java +++ b/src/ast/BoolOp.java @@ -29,14 +29,14 @@ public BoolOp(Expression l, BoolOperator x, Expression r) { public ScopeContext genTypeConstraints(NTCEnv env, ScopeContext parent) throws SemanticException { ScopeContext now = new ScopeContext(this, parent); ScopeContext l = left.genTypeConstraints(env, now), r = right.genTypeConstraints(env, now); - env.addCons(now.genTypeConstraints(l, Relation.LEQ, env, location)); - env.addCons(now.genTypeConstraints(r, Relation.LEQ, env, location)); - env.addCons(now.genTypeConstraints(env.getSymName(BuiltInT.BOOL), Relation.EQ, env, location)); + env.addCons(now.genTypeConstraints(l, Relation.LEQ, env, location, "The operands of a boolean operation must be bool")); + env.addCons(now.genTypeConstraints(r, Relation.LEQ, env, location, "The operands of a boolean operation must be bool")); + env.addCons(now.genTypeConstraints(env.getSymName(BuiltInT.BOOL), Relation.EQ, env, location, "A boolean operation returns a bool")); return now; } @Override - public ExpOutcome genIFConstraints(VisitEnv env, boolean tail_position) throws SemanticException { + protected ExpOutcome genFlowConstraints(VisitEnv env, boolean tail_position) throws SemanticException { Context beginContext = env.inContext; Context endContext = new Context(typecheck.Utils.getLabelNamePc(toSHErrLocFmt()), typecheck.Utils.getLabelNameLock(toSHErrLocFmt())); @@ -53,9 +53,9 @@ public ExpOutcome genIFConstraints(VisitEnv env, boolean tail_position) throws S String ifNameRtn = scopeContext.getSHErrLocName() + "." + "bool" + location.toString(); env.checkFlow(ifNameLeft, ifNameRtn, location, - "Integrity of left hand expression doesn't flow to value of this boolean operation"); + "The result of an operation is trusted no more than its left operand"); env.checkFlow(ifNameRight, ifNameRtn, location, - "Integrity of right hand expression doesn't flow to value of this boolean operation"); + "The result of an operation is trusted no more than its right operand"); typecheck.Utils.contextFlow(env, ro.psi.getNormalPath().c, endContext, right.location); // env.outContext = endContext; @@ -103,4 +103,9 @@ public java.util.Map readMap(CompileEnv code) { result.putAll(right.readMap(code)); return result; } + + @Override + protected TypeSym staticType(VisitEnv env) { + return env.builtinType(BuiltInT.BOOL); + } } diff --git a/src/ast/Call.java b/src/ast/Call.java index bcc8ea1..33da6d6 100644 --- a/src/ast/Call.java +++ b/src/ast/Call.java @@ -32,9 +32,16 @@ public class Call extends TrailerExpr { List args; - // store the called func symbol after regular typechecking + /** + * The method this call invokes, as resolved by the regular type check, or null if it + * invokes none. Code generation uses it; the IFC check resolves the callee separately. + */ FuncSym funcSym = null; - private boolean isCast; + /** + * The node this expression resolves to when it is not a call, such as a cast, as determined + * by the regular type check; every later pass is its. Null for a call. + */ + private Expression form = null; boolean builtIn = false, ntced = false; CallSpec callSpec; @@ -45,11 +52,20 @@ ClosureTypeSym.RealLabels realLabels() { return realLabels; } + /** Whether this call invokes a closure, as determined by the regular type check. */ private boolean isClosureInvoke = false; - // Closure's external begin label (lextbef) + /** + * For a closure invocation, the principals in the closure's external begin label (lextbef), + * set by the IFC check. Code generation requires it. + */ private List closurePcExLeaves = null; - /** The invoked closure's declared type, kept for codegen. */ + /** + * For a closure invocation, the invoked closure's declared type with its labels, set by the + * IFC check. Code generation requires it. + */ private ClosureTypeSym closureSym = null; + /** The type of this call's result, once it has been IFC-checked. */ + private TypeSym resultType; public Call() { this.args = new ArrayList<>(); @@ -102,22 +118,25 @@ public ScopeContext genTypeConstraints(NTCEnv env, ScopeContext parent) throws S // a.b(c), a must be a contract or an array extern = true; - if (!(att.value instanceof Name)) { + funcName = att.attr.id; // b + if (att.value instanceof Name n && env.getCurSym(n.id) == null) { + throw new SemanticException("variable not found: " + n.id, att.value.location); + } + // The receiver is a variable, or a member or element of one. + VarSym varSym = att.value.getVarInfo(env); + if (varSym == null) { throw new SemanticException( - "the receiver of a method call must be a variable", att.value.location); + "the receiver of a method call must be a variable, a member, or an element", + att.value.location); } - String varName = ((Name) att.value).id; // a - // System.out.println(varName); - funcName = att.attr.id; // b - Sym s = env.getCurSym(varName); - if (s == null) { - throw new SemanticException("variable not found: " + varName, att.value.location); + if (varSym.typeSym instanceof ArrayTypeSym) { + return resolveTo(new ArrayOperation(att.value, funcName, args), env, parent); } - // logger.debug("var " + varName + ": " + s.getName()); - - if (!(s instanceof VarSym varSym)) { - throw new SemanticException("type error in call (callee must be a variable): ", this.location); + if (!(att.value instanceof Name)) { + att.value.genTypeConstraints(env, now); } + String varName = varSym.getName(); + Sym s; if (varSym.typeSym instanceof InterfaceSym contractSym) { s = contractSym.getFunc(funcName); @@ -126,59 +145,20 @@ public ScopeContext genTypeConstraints(NTCEnv env, ScopeContext parent) throws S location); funcSym = (FuncSym) s; - } else if (varSym.typeSym instanceof ArrayTypeSym arrayTypeSym) { - // TODO: change the hard-code style - // TODO: factor this block out into its own method - TypeSym arrayTSym = arrayTypeSym.valueType; - String arrayTName = arrayTSym.toSHErrLocFmt(); - this.builtIn = true; - if (funcName.equals("pop")) { - // return T - if (!args.isEmpty()) throw new SemanticException("pop expects 0 arguments", - this.location); - env.addCons(now.genTypeConstraints(arrayTName, Relation.EQ, env, location)); - return now; - } else if (funcName.equals("push")) { - // require one T, return void - if (args.size() != 1) throw new SemanticException("push expects 1 argument", - this.location); - Expression arg = args.get(0); - ScopeContext argContext = arg.genTypeConstraints(env, now); - env.addCons(argContext.genTypeConstraints(arrayTName, Relation.GEQ, env, arg.location)); - TypeSym rtnTypeSym = (TypeSym) env.getSym(BuiltInT.VOID); - env.addCons(now.genTypeConstraints(rtnTypeSym.toSHErrLocFmt(), Relation.EQ, env, location)); - return now; - } else if (funcName.equals("length")) { - // return uint - if (!args.isEmpty()) { - throw new SemanticException("length expects 0 arguments", - this.location); - } - TypeSym rtnTypeSym = (TypeSym) env.getSym(BuiltInT.UINT); - env.addCons(now.genTypeConstraints(rtnTypeSym.toSHErrLocFmt(), Relation.EQ, env, location)); - return now; - } else { - throw new SemanticException("type error: unknown array operator", this.location); - } } else if (varSym.typeSym instanceof ClosureTypeSym closureTypeSym) { // c.invoke(args): args must match the still-unbound parameters; the call's type is the closure's return. this.builtIn = true; + this.isClosureInvoke = true; + if (callSpec != null) { + throw unsupportedSpec(); + } if (!funcName.equals("invoke")) { throw new SemanticException("type error: unknown closure operator " + funcName, this.location); } - if (args.size() != closureTypeSym.unboundParams.size()) { - throw new SemanticException( - "invoke argument count does not match the closure", this.location); - } - for (int i = 0; i < args.size(); ++i) { - Expression arg = args.get(i); - ScopeContext argContext = arg.genTypeConstraints(env, now); - env.addCons(argContext.genTypeConstraints( - closureTypeSym.unboundParams.get(i).toSHErrLocFmt(), - Relation.GEQ, env, arg.location)); - } + CallArguments.genTypeConstraints(args, closureTypeSym.unboundParams, + "closure " + varName, env, now, location); env.addCons(now.genTypeConstraints( - closureTypeSym.returnType.toSHErrLocFmt(), Relation.EQ, env, location)); + closureTypeSym.returnType.toSHErrLocFmt(), Relation.EQ, env, location, "Invoking a closure returns the closure's return type")); return now; } else { throw new SemanticException("type error: " + varName + "." + funcName + "() " + varSym.typeSym.toSHErrLocFmt() + (varSym.typeSym instanceof ContractSym), @@ -212,9 +192,10 @@ public ScopeContext genTypeConstraints(NTCEnv env, ScopeContext parent) throws S } if (!(s instanceof FuncSym)) { if (s instanceof InterfaceSym || s instanceof BuiltinTypeSym) { - env.addCons(now.genTypeConstraints(s.getName(), Relation.EQ, env, location)); - isCast = true; - return now; + if (args.size() != 1) { + throw new SemanticException("cast must have one argument", location); + } + return resolveTo(new Cast((Name) value, args.get(0)), env, parent); } throw new SemanticException("contract not found: " + s.getName(), location); @@ -227,26 +208,21 @@ public ScopeContext genTypeConstraints(NTCEnv env, ScopeContext parent) throws S if (env.inConstructor() && !env.superCalled()) throw new SemanticException("cannot call methods before super called in constructor: " + funcName, location); - if (args.size() != funcSym.parameters.size()) - throw new SemanticException("number of arguments does not match the number of parameters of the called method: " + funcName, - location); this.funcSym = funcSym; - if (extern && callSpec != null) { + if (callSpec != null) { + if (!extern) { + throw unsupportedSpec(); + } callSpec.genTypeConstraints(env, now); } - // typecheck arguments - for (int i = 0; i < args.size(); ++i) { - Expression arg = args.get(i); - TypeSym paraInfo = funcSym.parameters.get(i).typeSym; - ScopeContext argContext = arg.genTypeConstraints(env, now); - String typeName = paraInfo.toSHErrLocFmt(); - env.addCons(argContext.genTypeConstraints(typeName, Relation.GEQ, env, arg.location)); - } + CallArguments.genTypeConstraints(args, + funcSym.parameters.stream().map(p -> p.typeSym).toList(), + "method " + funcName, env, now, location); String rtnTypeName = funcSym.returnType.toSHErrLocFmt(); - env.addCons(now.genTypeConstraints(rtnTypeName, Relation.EQ, env, location)); + env.addCons(now.genTypeConstraints(rtnTypeName, Relation.EQ, env, location, "A call returns the return type of method " + funcName)); - for (Map.Entry tl : funcSym.exceptions.entrySet()) { + for (Map.Entry tl : funcSym.exceptions.entrySet()) { if (!parent.isCheckedException(tl.getKey(), extern)) { throw new SemanticException("Unchecked exception: " + tl.getKey().getName(), location); @@ -276,7 +252,18 @@ public ScopeContext genTypeConstraints(NTCEnv env, ScopeContext parent) throws S * operator other than {@code invoke} */ @Override - public ExpOutcome genIFConstraints(VisitEnv env, boolean tail_position) + protected ExpOutcome genFlowConstraints(VisitEnv env, boolean tail_position) + throws SemanticException { + if (form != null) { + return form.genIFConstraints(env, tail_position); + } + ExpOutcome result = callIFConstraints(env, tail_position); + // A call may assign to any field, so fields hold new principals afterwards. + env.havocFields(); + return result; + } + + private ExpOutcome callIFConstraints(VisitEnv env, boolean tail_position) throws SemanticException { //TODO: Assuming value is a Name for now Context beginContext = env.inContext; // (pc, lambda) @@ -284,36 +271,26 @@ public ExpOutcome genIFConstraints(VisitEnv env, boolean tail_position) Utils.getLabelNameLock(toSHErrLocFmt())); Map dependentLabelMapping = new HashMap<>(); - List argValueLabelNames = new ArrayList<>(); - PathOutcome psi = new PathOutcome(new PsiUnit(endContext)); - - // Evaluate arguments from left to right with substituations. - ExpOutcome ao = null; - for (Expression arg : args) { - ao = arg.genIFConstraints(env, false); - psi.joinExe(ao.psi); - argValueLabelNames.add(ao.valueLabelName); - - env.inContext = Utils.genNewContextAndConstraints(env, false, - ao.psi.getNormalPath().c, beginContext.lambda, arg.nextPcSHL(), arg.location); -// env.inContext = new Context( -// Utils.joinLabels(ao.psi.getNormalPath().c.pc, beginContext.pc), -// beginContext.lambda); - } + CallArguments.Evaluated evaluated = CallArguments.evaluate(args, env, psi); String funcName; String ifNamePc; // currentMethod.PC - FuncSym funcSym; + FuncSym calleeSym; String namespace = ""; - Label ifFuncCallPcBefore, ifFuncCallPcAfter, ifFuncGammaLock; + Label ifFuncCallPcBefore, ifFuncGammaLock; ExpOutcome vo = null; - boolean externalCall = false; - InterfaceSym externalContractSym = null; - VarSym externalTargetSym = null; + // The receiver of the call: the contract whose method is called, the label of the + // reference to it, and the principal it holds. An internal call's receiver is this + // contract itself. + InterfaceSym calleeContract; + Callee callee; String ifContRtn = null; + String receiverPrincipal = null; // the principal the receiver holds, if it is a variable + // The principal the callee's sender stands for. + String senderPrincipal; if (!(value instanceof Name)) { if (!(value instanceof Attribute att)) { @@ -323,225 +300,44 @@ public ExpOutcome genIFConstraints(VisitEnv env, boolean tail_position) // case 1: a.b(c) where a is a contract or an array, b is a function and c are the arguments // att = a.b - externalCall = true; - // evaluate a.b vo = att.value.genIFConstraints(env, false); psi.joinExe(vo.psi); ifContRtn = vo.valueLabelName; // a..lbl + receiverPrincipal = att.value.principalName(env); - //TODO: assuming a's depth is 1 - String varName = ((Name) att.value).id; // a funcName = (att.attr).id; // b - VarSym var = env.getVar(varName); - - if (var.typeSym instanceof ArrayTypeSym arrayTypeSym) { - // case 1a: a is an array (terminating branch) - - TypeSym arrayTSym = arrayTypeSym.valueType; - String arrayTName = arrayTSym.toSHErrLocFmt(); - - //TODO: change the hard-code style - if (funcName.equals("pop")) { - // requires pc => integrity of the array var - Utils.contextFlow(env, psi.getNormalPath().c, endContext, location); - ifNamePc = Utils.getLabelNamePc(scopeContext.getSHErrLocName()); - env.checkFlow(ifNamePc, ifContRtn, location, - "Current control flow must be trusted to call this method"); - // pc => l - if (!tail_position) { - env.checkFlow(psi.getNormalPath().c.lambda, beginContext.lambda, location, - Utils.ERROR_MESSAGE_LOCK_IN_NONLAST_OPERATION); - } - return new ExpOutcome(ifNamePc, psi); - } else if (funcName.equals("push")) { - // require pc => integrity of the array var - // require the element => integrity of the array var - Expression arg = args.get(0); - ExpOutcome argOutcome = arg.genIFConstraints(env, false); - psi.join(argOutcome.psi); - String argLabel = argOutcome.valueLabelName; - Utils.contextFlow(env, psi.getNormalPath().c, endContext, location); - ifNamePc = Utils.getLabelNamePc(scopeContext.getSHErrLocName()); - env.checkFlow(ifNamePc, var.ifl.toSHErrLocFmt(), location, - "Current control flow must be trusted to call this method"); - // pc => ? - env.checkFlow(argLabel, var.ifl.toSHErrLocFmt(), location, - "Current control flow must be trusted to call this method"); - if (!tail_position) { - env.checkFlow(psi.getNormalPath().c.lambda, beginContext.lambda, location, - Utils.ERROR_MESSAGE_LOCK_IN_NONLAST_OPERATION); - } - return new ExpOutcome(ifNamePc, psi); - } else if (funcName.equals("length")) { - // return uint the same as - Utils.contextFlow(env, psi.getNormalPath().c, endContext, location); - ifNamePc = Utils.getLabelNamePc(scopeContext.getSHErrLocName()); - if (!tail_position) { - env.checkFlow(psi.getNormalPath().c.lambda, beginContext.lambda, location, - Utils.ERROR_MESSAGE_LOCK_IN_NONLAST_OPERATION); - } - return new ExpOutcome(var.ifl.toSHErrLocFmt(), psi); - } else { - throw new SemanticException("Unrecognized operator", location); - } - } - - if (var.typeSym instanceof ClosureTypeSym cs) { - // case 1b: a is a closure value; a.invoke(args) (terminating branch) + TypeSym receiverType = att.value.type(); + if (receiverType instanceof ClosureTypeSym cs) { + // case 1b: a is a closure value; a.invoke(args) calls the closure's target, with + // the closure's labels, which are already in this contract's terms. if (!funcName.equals("invoke")) { throw new SemanticException( "type error: unknown closure operator " + funcName, location); } - - this.builtIn = true; - this.isClosureInvoke = true; this.closureSym = cs; - cs.registerAtoms(env); - - // lextbef this.closurePcExLeaves = cs.pcEx().principalLeaves(); + cs.registerAtoms(env); ifNamePc = Utils.getLabelNamePc(scopeContext.getSHErrLocName()); - dependentLabelMapping.put(env.curContractSym().invoker().toSHErrLocFmt(), env.thisSym().toSHErrLocFmt()); - - // Each invoke argument naming a principal fills its - // positional binder in the closure's labels. An argument - // for a label-referenced slot must name a principal (the - // dependent-map key rule). - List binders = cs.binderSyms(); - for (int i = 0; i < args.size() && i < binders.size(); i++) { - VarSym binder = binders.get(i); - if (binder == null) { - continue; - } - Expression principalExp = args.get(i); - if (principalExp instanceof Call cast && cast.isCast(env)) { - principalExp = cast.getArgAt(0); - } - VarSym actual = principalExp instanceof Name an ? env.getVar(an.id) : null; - if (actual != null && actual.isPrincipalVar()) { - dependentLabelMapping.put(binder.toSHErrLocFmt(), - actual.toSHErrLocFmt()); - } else if (cs.referencesBinder(binder)) { - throw new SemanticException( - "must use a final address/contract for the " - + Utils.ordNumString(i + 1) - + " invoke argument: the closure's labels depend on it", - args.get(i).location); - } - } - - String pcExStr = cs.pcEx().toSHErrLocFmt(dependentLabelMapping); - // pc_2 dropped - // String pcInStr = cs.pcIn().toSHErrLocFmt(dependentLabelMapping); - String gammaStr = cs.callGamma().toSHErrLocFmt(dependentLabelMapping); - String retStr = cs.endPc().toSHErrLocFmt(dependentLabelMapping); - - for (int i = 0; i < args.size(); i++) { - Expression arg = args.get(i); - String argValue = argValueLabelNames.get(i); - String argLabelStr = cs.getLabelArg(i).toSHErrLocFmt(dependentLabelMapping); - // argValue => paramLabel[i] - env.checkFlow(argValue, argLabelStr, arg.location, "Input to the " - + Utils.ordNumString(i + 1) - + " invoke argument must be trusted enough"); - - // pc => paramLabel[i] - env.checkFlow(ifNamePc, argLabelStr, arg.location, - "Current control flow must be trusted to feed the " - + Utils.ordNumString(i + 1) + "-th invoke argument"); - } - - // Authorization to make the call - - // closureValueLabel => pc_ex - env.checkFlow(ifContRtn, pcExStr, location, - "Closure value must be trusted enough to invoke"); - - // pc => pc_ex - env.checkFlow(ifNamePc, pcExStr, location, - "Current control flow must be trusted to invoke this closure"); - - // pc_2 dropped - // // pc_ex => pc_in ∨ lambda_caller - // env.cons.add(new Constraint( - // new Inequality(pcExStr, - // Utils.joinLabels(pcInStr, beginContext.lambda)), - // env.hypothesis(), location, env.curContractSym().getName(), - // "Invoking this closure does not respect static reentrancy locks")); - - // Post-call Psi — normal path: (pc ⊔ l_nθ_u ⊔ ℓ, gamma). - // B.8 / advisor item (3): the continuation is floored by the - // caller's pc, the believed return label, and the closure's - // value label. pc_ex is an entry requirement (gate premise + - // runtime witness), not a taint source; joining it here would - // nullify callee-declared autoendorsement (any-entry methods - // would taint every caller's continuation to any). - String preCallPc = psi.getNormalPath().c.pc; - String postPcJoin = Utils.joinLabels( - Utils.joinLabels(preCallPc, retStr), - ifContRtn); - PathOutcome expPsi = new PathOutcome(new PsiUnit(new Context( - postPcJoin, gammaStr))); - - // TODO: - // closureValueLabel ⊔ gamma == post-call lambda - env.checkEqual(Utils.joinLabels(ifContRtn, gammaStr), endContext.lambda, location, - "Invoking this closure does not respect static reentrancy locks"); - - if (!tail_position) { - env.checkFlow(psi.getNormalPath().c.lambda, beginContext.lambda, location, - Utils.ERROR_MESSAGE_LOCK_IN_NONLAST_OPERATION); // normal psi.lock => pre-call lamnbda - } - - // Finalize - String ifNameFuncRtnValue = retStr; - psi.joinExe(expPsi); - // contextFlow would route the pc edge into trustCons, which - // createDiagnoser hands to SHErrLoc as ASSUMPTIONS — granting - // the flow instead of checking it (found 2026-07-19; the Ψ - // floor was unenforced for every call). Emit the lock edge on - // the usual assumption channel but the pc floor as a CHECKED - // constraint. - env.checkTrustedBy(psi.getNormalPath().c.lambda, endContext.lambda, location, - "actually maintained lock of final sub-statement must flow to that of parent statement"); - // Emitted component-wise: a join on the left of ≤ can slip - // through the solver unchecked (see IMPLEMENTATION.md, - // string-emission landmines). - env.checkFlow(preCallPc, endContext.pc, location, - "Post-invocation control flow must carry the pre-call control flow"); - env.checkFlow(retStr, endContext.pc, location, - "Post-invocation control flow must carry the closure's return label"); - env.checkFlow(ifContRtn, endContext.pc, location, - "Post-invocation control flow must carry the closure's value label"); - psi.setNormalPath(endContext); - env.checkFlow(psi.getNormalPath().c.pc, ifNameFuncRtnValue, location, "ln_to_t"); - return new ExpOutcome(ifNameFuncRtnValue, psi); + callee = Callee.ofClosure(cs, env.curContractSym().invoker()); + calleeContract = null; + // The closure's target is called with this contract as its invoker. + senderPrincipal = env.thisSym().toSHErrLocFmt(); + } else { + // case 1c: external call + TypeSym conType = receiverType; + namespace = conType.getName(); + env.addSigReq(namespace, conType.getName()); + ifNamePc = Utils.getLabelNamePc(scopeContext.getSHErrLocName()); + calleeContract = env.getContract(conType.getName()); + calleeSym = calleeContract.getFunc(funcName); + if (calleeSym == null) + throw new SemanticException("not found: " + conType.getName() + "." + funcName, location); + callee = Callee.ofMethod(calleeSym, calleeContract); + // The callee's sender is this contract. + senderPrincipal = env.thisSym().toSHErrLocFmt(); } - - // case 1c: external call - // look up funcSym, update dependentLabelMapping, and read labels from funcSym - - externalTargetSym = var; - namespace = var.toSHErrLocFmt(); - TypeSym conType = var.typeSym; - externalContractSym = env.getContract(conType.getName()); - - env.addSigReq(namespace, conType.getName()); - ifNamePc = Utils.getLabelNamePc(scopeContext.getSHErrLocName()); - InterfaceSym contractSym = env.getContract(conType.getName()); - funcSym = contractSym.getFunc(funcName); - if (funcSym == null) - throw new SemanticException("not found: " + conType.getName() + "." + funcName, location); - - dependentLabelMapping.put(funcSym.sender().toSHErrLocFmt(), env.thisSym().toSHErrLocFmt()); - dependentLabelMapping.put(contractSym.any().toSHErrLocFmt(), env.curContractSym().any().toSHErrLocFmt()); - dependentLabelMapping.put(contractSym.invoker().toSHErrLocFmt(), env.curContractSym().invoker().toSHErrLocFmt()); - - ifFuncCallPcBefore = funcSym.externalPc(); - ifFuncCallPcAfter = funcSym.internalPc(); - ifFuncGammaLock = funcSym.callGamma(); } else { // case 2: a(b) - local contract call or type cast funcName = ((Name) value).id; @@ -551,43 +347,35 @@ public ExpOutcome genIFConstraints(VisitEnv env, boolean tail_position) ifNamePc = Utils.getLabelNamePc(scopeContext.getSHErrLocName()); if (!env.containsFunc(funcName)) { - if (env.containsContract(funcName) || Utils.isPrimitiveType(funcName)) { - // case 2a: type cast (terminating branch) - - if (args.size() != 1) { - throw new SemanticException("cast must have one argument", location); - } - - String ifNameArgValue = argValueLabelNames.get(0); - Utils.contextFlow(env, psi.getNormalPath().c, endContext, - args.get(0).location); - // env.outContext = endContext; - if (!tail_position) { - env.checkFlow(psi.getNormalPath().c.lambda, beginContext.lambda, location, - Utils.ERROR_MESSAGE_LOCK_IN_NONLAST_OPERATION); - } - return new ExpOutcome(ifNameArgValue, psi); - } else { - throw new SemanticException("method not found: " + funcName, location); - } + throw new SemanticException("method not found: " + funcName, location); } - // case 2b: local call - - funcSym = env.getFunc(funcName); + // case 2b: internal call, whose receiver is this contract -// dependentLabelMapping.put(funcSym.sender().toSHErrLocFmt(), env.sender().toSHErrLocFmt()); - dependentLabelMapping.put(funcSym.sender().toSHErrLocFmt(), env.inContext.pc); + calleeSym = env.getFunc(funcName); + calleeContract = env.curContractSym(); + callee = Callee.ofMethod(calleeSym, calleeContract); + ifContRtn = env.thisSym().toSHErrLocFmt(); + receiverPrincipal = env.thisSym().toSHErrLocFmt(); + // The callee runs with the current sender, so its demands on the sender are met + // with the authority of the current control flow. + senderPrincipal = env.inContext.pc; + } - ifFuncCallPcBefore = funcSym.externalPc(); - ifFuncCallPcAfter = funcSym.internalPc(); - ifFuncGammaLock = funcSym.callGamma(); + if (calleeContract != null) { + dependentLabelMapping.put(calleeContract.any().toSHErrLocFmt(), + env.curContractSym().any().toSHErrLocFmt()); + dependentLabelMapping.put(calleeContract.invoker().toSHErrLocFmt(), + env.curContractSym().invoker().toSHErrLocFmt()); } + dependentLabelMapping.put(callee.sender(), senderPrincipal); + ifFuncCallPcBefore = callee.externalPc(); + ifFuncGammaLock = callee.gamma(); // build hypothesis for sender and this // make sender equal to this // Inequality senderHypo = new Inequality( -// funcSym.sender().toSHErrLocFmt(), +// calleeSym.sender().toSHErrLocFmt(), // CompareOperator.Eq, // env.curContractSym.toSHErrLocFmt() // ); @@ -595,118 +383,88 @@ public ExpOutcome genIFConstraints(VisitEnv env, boolean tail_position) // ++createdHypoCount; // Evaluate callSpec - if (externalCall && callSpec != null) { + if (callSpec != null) { PathOutcome co = callSpec.genIFConstraints(env, false); psi.joinExe(co); env.inContext = Utils.genNewContextAndConstraints(env, false, co.getNormalPath().c, beginContext.lambda, callSpec.nextPcSHL(), callSpec.location); } - // if external call and the target address is final, make callee.this equal to the target address - if (externalCall) { - if (externalTargetSym.isFinal) { - dependentLabelMapping.put( - externalContractSym.thisSym().toSHErrLocFmt(), - externalTargetSym.toSHErrLocFmt()); - } else { - dependentLabelMapping.put( - externalContractSym.thisSym().toSHErrLocFmt(), - ifContRtn); // XXX is this correct? Seems like this is the label of the contract value. - } + // The callee's labels are instantiated differently in input and output positions. + // Its inputs (argument labels, external pc) are demands it makes of this caller, + // so there the callee's `this` is the callee itself: the principal the receiver + // holds. This contract can meet those demands only with what it trusts itself, + // since it is the top principal here. Its outputs (return label, post-call pc, + // lock label) are promises trusted only as much as the callee, which acts for the + // label of the reference used to call it, so there its `this` becomes that label. + // A principal parameter of the callee names the principal passed for it. If that + // is unknown, the callee's demands are taken to name the most trusted principal and + // its promises the least trusted one. + Map inputMapping = new HashMap<>(dependentLabelMapping); + Map outputMapping = new HashMap<>(dependentLabelMapping); + CallArguments.mapPrincipals(callee.principalParams(), evaluated, + env.curContractSym().top().toSHErrLocFmt(), inputMapping); + CallArguments.mapPrincipals(callee.principalParams(), evaluated, + env.curContractSym().any().toSHErrLocFmt(), outputMapping); + if (callee.thisSym() != null) { + inputMapping.put(callee.thisSym(), receiverPrincipal != null + ? receiverPrincipal : env.thisSym().toSHErrLocFmt()); + outputMapping.put(callee.thisSym(), ifContRtn); } + // Whatever the callee's labels say, its results are trusted no more than the + // reference used to call it. + String calleeTrust = ifContRtn; // Generate constraints on arguments -// System.err.println("Call: " + funcName); + CallArguments.checkFlowInto(args, evaluated, ifNamePc, callee.paramLabels(), + inputMapping, "", env); for (int i = 0; i < args.size(); ++i) { Expression arg = args.get(i); - VarSym argSym = funcSym.parameters.get(i); - if (argSym.isPrincipalVar()) { - - if (arg instanceof Name) { - VarSym valueSym = (VarSym) env.getVar(((Name) arg).id); - if (valueSym.isPrincipalVar()) { -// System.err.println("dependent " + argSym.typeSym + " -> " + valueSym.toSHErrLocFmt()); - dependentLabelMapping.put(argSym.toSHErrLocFmt(), valueSym.toSHErrLocFmt()); - } - } - // TODO: Do we throw exception if arg is not a Name? - } - - // env.prevContext = prevContext = tmp; - String ifNameArgValue = argValueLabelNames.get(i); // argument's label name - Label ifArgLabel = funcSym.getLabelArg(i); // parameter's label - assert ifArgLabel != null : argSym.getName(); - env.checkFlow(ifNameArgValue, ifArgLabel.toSHErrLocFmt(dependentLabelMapping), - arg.location, "Input to the " + Utils.ordNumString(i + 1) - + " argument must be trusted enough"); // arglbl => paramlbl - env.checkFlow(ifNamePc, ifArgLabel.toSHErrLocFmt(dependentLabelMapping), arg.location, - "Current control flow must be trusted to feed the " + Utils.ordNumString(i + 1) - + "-th argument value"); // pc => paramlbl - - if (argSym.typeSym instanceof ClosureTypeSym paramCs) { - ClosureCreation.checkFlowInto(arg, paramCs, dependentLabelMapping, env, arg.location, - "Closure value flowing into the " + Utils.ordNumString(i + 1) + " argument must subtype its slot"); + if (callee.paramTypes().get(i) instanceof ClosureTypeSym paramCs) { + ClosureCreation.checkFlowInto(arg, paramCs, inputMapping, env, arg.location, + "The closure passed as the " + Utils.ordNumString(i + 1) + " argument must be compatible with the type of its parameter"); } } // Generate pre-call and post-call constraints and contexts - if (externalCall) { -// String tem = ((Attribute) value).value.toSHErrLocFmt(); - env.checkFlow(ifContRtn, ifFuncCallPcBefore.toSHErrLocFmt(dependentLabelMapping), - location, "Target contract must be trusted to call this method"); // target address..lbl => pc_ex - } + env.checkFlow(ifContRtn, ifFuncCallPcBefore.toSHErrLocFmt(inputMapping), + location, "The reference used to call this method must be trusted at its external begin label"); // target address..lbl => pc_ex + String postCallLock = attenuate(ifFuncGammaLock.toSHErrLocFmt(outputMapping), calleeTrust); PathOutcome expPsi = new PathOutcome(new PsiUnit(new Context( - Utils.joinLabels(psi.getNormalPath().c.pc, funcSym.endPc().toSHErrLocFmt(dependentLabelMapping)), -// funcSym.getLabelNameCallGamma() - ifFuncGammaLock.toSHErrLocFmt(dependentLabelMapping) - ))); // post-call psi = (current normal path pc ⊔ function return label, gamma) - - for (Entry exp : funcSym.exceptions.entrySet()) { - ExceptionTypeSym curSym = exp.getKey(); - String expLabelName = exp.getValue(); - // pc_2 dropped - // expPsi.set(curSym, new PsiUnit( - // new Context( - // Utils.joinLabels(expLabelName, funcSym.externalPcSLC()), - // Utils.joinLabels(ifFuncGammaLock.toSHErrLocFmt(dependentLabelMapping), - // ifFuncCallPcAfter.toSHErrLocFmt(dependentLabelMapping))), - // true) - // ); // exception-path post-call psi = (function exception-path pc ⊔ pc_ex, - // // gamma ⊔ pc_in) - expPsi.set(curSym, new PsiUnit( + attenuate(Utils.joinLabels(psi.getNormalPath().c.pc, + callee.returnLabel().toSHErrLocFmt(outputMapping)), calleeTrust), + postCallLock + ))); // post-call psi = (current normal path pc ⊔ function end pc, gamma), attenuated + + checkExceptionData(env, callee.exceptions().keySet(), outputMapping); + for (Entry exp : callee.exceptions().entrySet()) { + // exception-path post-call psi = (current pc ⊔ declared exception label, gamma), + // attenuated like the normal path + expPsi.set(exp.getKey(), new PsiUnit( new Context( - Utils.joinLabels(expLabelName, funcSym.externalPcSLC()), - ifFuncGammaLock.toSHErrLocFmt(dependentLabelMapping)), - true) - ); // exception-path post-call psi = (function exception-path pc ⊔ pc_ex, gamma) - // TODO: should pc label get joined by pc_ex, or psi.normal.pc? - //TODO: dependent - //PsiUnit psiUnit = env.psi.get(curSym); - //env.cons.add(new Constraint(new Inequality(Utils.makeJoin(expLabelName, ifNameFuncCallPcAfter), psiUnit.pc), env.hypothesis, location, env.curContractSym.name, - //"Exception " + curSym.name + " is not trusted enough to throw")); + attenuate(Utils.joinLabels(psi.getNormalPath().c.pc, + exp.getValue().toSHErrLocFmt(outputMapping)), calleeTrust), + postCallLock), + true)); } //TODO - env.checkFlow(ifNamePc, ifFuncCallPcBefore.toSHErrLocFmt(dependentLabelMapping), location, - "Current control flow must be trusted to call this method"); // current pc => pc_ex + env.checkFlow(ifNamePc, ifFuncCallPcBefore.toSHErrLocFmt(inputMapping), location, + "Control flow must be trusted at the external begin label of the method called"); // current pc => pc_ex // pc_2 dropped // env.cons.add(new Constraint(new Inequality(ifFuncCallPcBefore.toSHErrLocFmt(dependentLabelMapping), // Utils.joinLabels(ifFuncCallPcAfter.toSHErrLocFmt(dependentLabelMapping), beginContext.lambda)), env.hypothesis(), // location, env.curContractSym().getName(), - // "Calling this function does not respect static reentrancy locks") + // "The method called maintains only its reentrancy lock label, trusted no more than the reference used to call it") // ); // pc_ex => pc_in ⊔ caller's lambda - if (externalCall) { - // target address..lbl ⊔ gamma == post-call lambda - env.checkEqual( - Utils.joinLabels(ifContRtn, ifFuncGammaLock.toSHErrLocFmt(dependentLabelMapping)), - endContext.lambda, location, - "Calling this function does not respect static reentrancy locks"); - } + // callee trust ⊔ gamma == post-call lambda + env.checkEqual(postCallLock, endContext.lambda, location, + "The method called maintains only its reentrancy lock label, trusted no more than the reference used to call it"); if (!tail_position) { // env.cons.add(new Constraint( @@ -724,11 +482,12 @@ public ExpOutcome genIFConstraints(VisitEnv env, boolean tail_position) // Finalize - String ifNameFuncRtnValue = funcSym.rtn.toSHErrLocFmt(dependentLabelMapping); + String ifNameFuncRtnValue = attenuate(callee.returnLabel().toSHErrLocFmt(outputMapping), + calleeTrust); // realLabels - if (funcSym.returnType instanceof ClosureTypeSym retCs) { - this.realLabels = retCs.renderLabels(dependentLabelMapping); + if (callee.returnType() instanceof ClosureTypeSym retCs) { + this.realLabels = retCs.renderLabels(outputMapping); } psi.joinExe(expPsi); @@ -736,10 +495,108 @@ public ExpOutcome genIFConstraints(VisitEnv env, boolean tail_position) psi.setNormalPath(endContext); // post-call pc (normal) => function return label (l_n) env.checkFlow(psi.getNormalPath().c.pc, ifNameFuncRtnValue, location, - "Control flow after this call must be trusted by the function's return value label"); + "The result of a call is trusted no more than control flow after the call"); + resultType = callee.returnType(); return new ExpOutcome(ifNameFuncRtnValue, psi); } + /** + * Checks that the data of each exception in {@code exceptions}, which the callee may throw, is + * trusted at the labels this contract's declaration of that exception gives it, since + * handlers here read it at those labels. The callee's labels are instantiated with + * {@code outputMapping}, with its exception's principal parameters standing for the + * corresponding parameters of this contract's declaration. + */ + private void checkExceptionData(VisitEnv env, java.util.Set exceptions, + Map outputMapping) { + // A handler reads each field at its label joined with the label of the exception's + // path, which is attenuated by the callee's trust, so the data is too. + for (ExceptionTypeSym calleeExp : exceptions) { + ExceptionTypeSym localExp = env.getExp(calleeExp.getName()); + if (localExp == null) { + throw new AssertionError("exception " + calleeExp.getName() + + " of an external call has no local declaration"); + } + Map mapping = new HashMap<>(outputMapping); + for (int i = 0; i < calleeExp.parameters().size(); ++i) { + VarSym calleeParam = calleeExp.parameters().get(i); + if (calleeParam.isPrincipalTyped()) { + mapping.put(calleeParam.toSHErrLocFmt(), env.freshPrincipal( + localExp.parameters().get(i).toSHErrLocFmt())); + } + } + for (int i = 0; i < calleeExp.parameters().size(); ++i) { + VarSym calleeParam = calleeExp.parameters().get(i); + VarSym localParam = localExp.parameters().get(i); + env.checkFlow(calleeParam.ifl.toSHErrLocFmt(mapping), + localParam.ifl.toSHErrLocFmt(), location, + "Data of exception " + calleeExp.getName() + + " from this call must be trusted at its declared label here"); + } + } + } + + /** + * What the call rule needs to know about a callee, whether a method or a closure's target. + * + * @param paramLabels the label of each parameter + * @param principalParams the principal each parameter binds, or null for a parameter that + * binds none + * @param paramTypes the type of each parameter + * @param externalPc the label the caller's control flow must be trusted at + * @param gamma the lock label of the call + * @param returnLabel the label of the result, which is also the end pc + * @param returnType the type of the result + * @param exceptions the exceptions the callee may throw, each with its label + * @param sender the SHErrLoc name of the principal that stands for the caller in the + * callee's labels + * @param thisSym the SHErrLoc name of the callee's {@code this}, or null if its labels are + * already in this contract's terms + */ + private record Callee(List