From 24476f76856acbe81474cbdb8b814be8db63a4d5 Mon Sep 17 00:00:00 2001 From: DavePearce Date: Mon, 8 Sep 2014 14:04:47 +1200 Subject: [PATCH 01/11] WyIL: Changes to first part for #435. This change partly completes the updating of the WyIL bytecode to support multiple requires/ensures clauses. The purpose of this is to enable better error reporting for individual ensures clauses. --- .../wyc/src/wyc/builder/CodeGenerator.java | 45 ++++++++++--------- .../wyil/src/wyil/builders/VcTransformer.java | 27 ++++++----- .../src/wyil/builders/Wyil2WyalBuilder.java | 12 +++-- modules/wyil/src/wyil/io/WyilFilePrinter.java | 8 ++-- modules/wyil/src/wyil/io/WyilFileReader.java | 10 ++--- modules/wyil/src/wyil/io/WyilFileWriter.java | 8 ++-- modules/wyil/src/wyil/lang/WyilFile.java | 24 +++++----- .../src/wyil/transforms/BackPropagation.java | 25 ++++++----- .../wyil/transforms/ConstantPropagation.java | 30 +++++++------ .../transforms/LiveVariablesAnalysis.java | 21 +++++---- .../wyil/transforms/RuntimeAssertions.java | 45 ++++++++++--------- 11 files changed, 137 insertions(+), 118 deletions(-) diff --git a/modules/wyc/src/wyc/builder/CodeGenerator.java b/modules/wyc/src/wyc/builder/CodeGenerator.java index ee53951cbf..4c5992f1d0 100644 --- a/modules/wyc/src/wyc/builder/CodeGenerator.java +++ b/modules/wyc/src/wyc/builder/CodeGenerator.java @@ -449,20 +449,17 @@ private List generate( // Generate pre-condition // ================================================================== - Code.Block precondition = null; + ArrayList requires = new ArrayList(); for (WhileyFile.Parameter p : fd.parameters) { // First, generate and inline any constraints associated with the // type. // Now, map the parameter to its index Code.Block constraint = generate(p.type, p); - if (constraint != null) { - if (precondition == null) { - precondition = new Code.Block(nparams); - } + if (constraint != null) { constraint = shiftBlockExceptionZero(nparams, paramIndex, constraint); - precondition.addAll(constraint); + requires.add(constraint); } environment.allocate(ftype.params().get(paramIndex++),p.name()); } @@ -470,20 +467,25 @@ private List generate( // Resolve pre- and post-condition for (Expr condition : fd.requires) { - if (precondition == null) { - precondition = new Code.Block(nparams); - } + Code.Block block = new Code.Block(nparams); // FIXME: this should be added to RuntimeAssertions String endLab = CodeUtils.freshLabel(); - generateCondition(endLab, condition,environment, precondition, fd); - precondition.add(Codes.Fail("precondition not satisfied"),attributes(condition)); - precondition.add(Codes.Label(endLab)); + generateCondition(endLab, condition, environment, block, fd); + block.add(Codes.Fail("precondition not satisfied"),attributes(condition)); + block.add(Codes.Label(endLab)); + requires.add(block); } // ================================================================== // Generate post-condition // ================================================================== - Code.Block postcondition = generate(fd.ret.toSyntacticType(),fd); + ArrayList ensures = new ArrayList(); + Code.Block retInvariant = generate(fd.ret.toSyntacticType(),fd); + + if(retInvariant != null) { + ensures.add(retInvariant); + } + if (fd.ensures.size() > 0) { Environment postEnv = new Environment(); int root = postEnv.allocate(fd.resolvedType().ret().raw(), "$"); @@ -492,17 +494,18 @@ private List generate( for (WhileyFile.Parameter p : fd.parameters) { postEnv.allocate(ftype.params().get(paramIndex), p.name()); paramIndex++; - } - postcondition = new Code.Block(postEnv.size()); - addDeclaredVariables(root, fd.ret, fd.resolvedType().ret().raw(), - postEnv, postcondition); + } for (Expr condition : fd.ensures) { // FIXME: this should be added to RuntimeAssertions + Code.Block block = new Code.Block(postEnv.size()); + addDeclaredVariables(root, fd.ret, fd.resolvedType().ret().raw(), + postEnv, block); String endLab = CodeUtils.freshLabel(); - generateCondition(endLab, condition, postEnv, postcondition, fd); - postcondition.add(Codes.Fail("postcondition not satisfied"),attributes(condition)); - postcondition.add(Codes.Label(endLab)); + generateCondition(endLab, condition, postEnv, block, fd); + block.add(Codes.Fail("postcondition not satisfied"),attributes(condition)); + block.add(Codes.Label(endLab)); + ensures.add(block); } } @@ -522,7 +525,7 @@ private List generate( List ncases = new ArrayList(); - ncases.add(new WyilFile.Case(body,precondition,postcondition)); + ncases.add(new WyilFile.Case(body,requires,ensures)); ArrayList declarations = new ArrayList(); if (fd instanceof WhileyFile.Function) { diff --git a/modules/wyil/src/wyil/builders/VcTransformer.java b/modules/wyil/src/wyil/builders/VcTransformer.java index b074bc450b..042cb66a60 100644 --- a/modules/wyil/src/wyil/builders/VcTransformer.java +++ b/modules/wyil/src/wyil/builders/VcTransformer.java @@ -380,9 +380,7 @@ protected void transform(Codes.Invoke code, VcBranch branch) Collection attributes = entry.attributes(); int[] code_operands = code.operands(); if (code.target() != Codes.NULL_REG) { - // Need to assume the post-condition holds. - Code.Block postcondition = findPostcondition(code.name, code.type(), - branch.entry()); + // Need to assume the post-condition holds. Expr[] operands = new Expr[code_operands.length]; for (int i = 0; i != code_operands.length; ++i) { operands[i] = branch.read(code_operands[i]); @@ -402,7 +400,10 @@ protected void transform(Codes.Invoke code, VcBranch branch) wycsFile.add(wycsFile.new Function(toIdentifier(code.name), Collections.EMPTY_LIST, from, to, null)); - if (postcondition != null) { + List requires = findPostcondition(code.name, code.type(), + branch.entry()); + + if (requires.size() > 0) { // operands = Arrays.copyOf(operands, operands.length); Expr[] arguments = new Expr[operands.length + 1]; System.arraycopy(operands, 0, arguments, 1, operands.length); @@ -412,11 +413,13 @@ protected void transform(Codes.Invoke code, VcBranch branch) for(int i=0;i!=paramTypes.size();++i) { types[i+1] = paramTypes.get(i); } - types[0] = branch.typeOf(code.target()); - Expr constraint = transformExternalBlock(postcondition, - arguments, types, branch); - // assume the post condition holds - branch.add(constraint); + types[0] = branch.typeOf(code.target()); + for(Code.Block postcondition : requires) { + Expr constraint = transformExternalBlock(postcondition, + arguments, types, branch); + // assume the post condition holds + branch.add(constraint); + } } } } @@ -619,7 +622,7 @@ protected Expr updateHelper(Iterator iter, Expr source, } } - protected Code.Block findPrecondition(NameID name, Type.FunctionOrMethod fun, + protected List findPrecondition(NameID name, Type.FunctionOrMethod fun, SyntacticElement elem) throws Exception { Path.Entry e = builder.project().get(name.module(), WyilFile.ContentType); @@ -639,7 +642,7 @@ protected Code.Block findPrecondition(NameID name, Type.FunctionOrMethod fun, return null; } - protected Code.Block findPostcondition(NameID name, + protected List findPostcondition(NameID name, Type.FunctionOrMethod fun, SyntacticElement elem) throws Exception { Path.Entry e = builder.project().get(name.module(), WyilFile.ContentType); @@ -658,7 +661,7 @@ protected Code.Block findPostcondition(NameID name, return c.postcondition(); } } - return null; + return Collections.EMPTY_LIST; } /** diff --git a/modules/wyil/src/wyil/builders/Wyil2WyalBuilder.java b/modules/wyil/src/wyil/builders/Wyil2WyalBuilder.java index c431e06b30..265cf14224 100644 --- a/modules/wyil/src/wyil/builders/Wyil2WyalBuilder.java +++ b/modules/wyil/src/wyil/builders/Wyil2WyalBuilder.java @@ -159,12 +159,16 @@ protected void transform(WyilFile.Case methodCase, master.write(i, new Expr.Variable("r" + Integer.toString(i)), paramType); } - Code.Block precondition = methodCase.precondition(); + List requires = methodCase.precondition(); - if (precondition != null) { - VcBranch precond = new VcBranch(method, precondition); + if (requires.size() > 0) { + Code.Block block = new Code.Block(fmm.params().size()); + for(Code.Block precondition : requires) { + block.addAll(precondition); + } + VcBranch precond = new VcBranch(method, block); - AssertOrAssumeScope scope = new AssertOrAssumeScope(false, precondition.size(), Collections.EMPTY_LIST); + AssertOrAssumeScope scope = new AssertOrAssumeScope(false, block.size(), Collections.EMPTY_LIST); precond.scopes.add(scope); // FIXME: following seems like a hack --- there must be a more diff --git a/modules/wyil/src/wyil/io/WyilFilePrinter.java b/modules/wyil/src/wyil/io/WyilFilePrinter.java index 2b5045f891..3e764b6635 100755 --- a/modules/wyil/src/wyil/io/WyilFilePrinter.java +++ b/modules/wyil/src/wyil/io/WyilFilePrinter.java @@ -157,15 +157,13 @@ private void write(Case mcase, FunctionOrMethodDeclaration method, PrintWriter o out.print(pts.get(i)); } out.println("):"); - - Code.Block precondition = mcase.precondition(); - if(precondition != null) { + + for(Code.Block precondition : mcase.precondition()) { out.println("requires:"); write(0,precondition,out); } - Code.Block postcondition = mcase.postcondition(); - if(postcondition != null) { + for(Code.Block postcondition : mcase.postcondition()) { out.println("ensures:"); write(0,postcondition,out); } diff --git a/modules/wyil/src/wyil/io/WyilFileReader.java b/modules/wyil/src/wyil/io/WyilFileReader.java index 3fb4b502ce..694628cb41 100644 --- a/modules/wyil/src/wyil/io/WyilFileReader.java +++ b/modules/wyil/src/wyil/io/WyilFileReader.java @@ -456,8 +456,8 @@ private Collection generateModifiers(int modifiers) { private WyilFile.Case readFunctionOrMethodCase(Type.FunctionOrMethod type) throws IOException { - Code.Block precondition = null; - Code.Block postcondition = null; + ArrayList requires = new ArrayList(); + ArrayList ensures = new ArrayList(); Code.Block body = null; int numInputs = type.params().size(); int nBlocks = input.read_uv(); @@ -471,10 +471,10 @@ private WyilFile.Case readFunctionOrMethodCase(Type.FunctionOrMethod type) switch (kind) { case WyilFileWriter.BLOCK_Precondition: - precondition = readCodeBlock(numInputs); + requires.add(readCodeBlock(numInputs)); break; case WyilFileWriter.BLOCK_Postcondition: - postcondition = readCodeBlock(numInputs + 1); + ensures.add(readCodeBlock(numInputs + 1)); break; case WyilFileWriter.BLOCK_Body: body = readCodeBlock(numInputs); @@ -484,7 +484,7 @@ private WyilFile.Case readFunctionOrMethodCase(Type.FunctionOrMethod type) } } - return new WyilFile.Case(body, precondition, postcondition, + return new WyilFile.Case(body, requires, ensures, Collections.EMPTY_LIST); } diff --git a/modules/wyil/src/wyil/io/WyilFileWriter.java b/modules/wyil/src/wyil/io/WyilFileWriter.java index 62cc4f2fb0..9d4ab0e560 100644 --- a/modules/wyil/src/wyil/io/WyilFileWriter.java +++ b/modules/wyil/src/wyil/io/WyilFileWriter.java @@ -432,11 +432,11 @@ private byte[] generateFunctionOrMethodCaseBlock(WyilFile.Case c) throws IOExcep int bodyCount = c.body() == null ? 0 : 1; output.write_uv(preconditionCount + postconditionCount + bodyCount); - if(c.precondition() != null) { - writeBlock(BLOCK_Precondition,c.precondition(),output); + for(Code.Block requires : c.precondition()) { + writeBlock(BLOCK_Precondition,requires,output); } - if(c.postcondition() != null) { - writeBlock(BLOCK_Postcondition,c.postcondition(),output); + for(Code.Block ensures : c.postcondition()) { + writeBlock(BLOCK_Postcondition,ensures,output); } if(c.body() != null) { writeBlock(BLOCK_Body,c.body(),output); diff --git a/modules/wyil/src/wyil/lang/WyilFile.java b/modules/wyil/src/wyil/lang/WyilFile.java index 5f8a3d76c5..f11fe2e367 100755 --- a/modules/wyil/src/wyil/lang/WyilFile.java +++ b/modules/wyil/src/wyil/lang/WyilFile.java @@ -526,40 +526,40 @@ public boolean isMethod() { } public static final class Case extends SyntacticElement.Impl { - private final Code.Block precondition; - private final Code.Block postcondition; + private final ArrayList precondition; + private final ArrayList postcondition; private final Code.Block body; //private final ArrayList locals; public Case(Code.Block body, - Code.Block precondition, - Code.Block postcondition, + List precondition, + List postcondition, Attribute... attributes) { super(attributes); this.body = body; - this.precondition = precondition; - this.postcondition = postcondition; + this.precondition = new ArrayList(precondition); + this.postcondition = new ArrayList(postcondition); } public Case(Code.Block body, - Code.Block precondition, - Code.Block postcondition, + List precondition, + List postcondition, Collection attributes) { super(attributes); this.body = body; - this.precondition = precondition; - this.postcondition = postcondition; + this.precondition = new ArrayList(precondition); + this.postcondition = new ArrayList(postcondition); } public Code.Block body() { return body; } - public Code.Block precondition() { + public List precondition() { return precondition; } - public Code.Block postcondition() { + public List postcondition() { return postcondition; } } diff --git a/modules/wyil/src/wyil/transforms/BackPropagation.java b/modules/wyil/src/wyil/transforms/BackPropagation.java index 7f656193f8..51752e6dbe 100755 --- a/modules/wyil/src/wyil/transforms/BackPropagation.java +++ b/modules/wyil/src/wyil/transforms/BackPropagation.java @@ -147,26 +147,29 @@ protected Env lastStore() { } @Override - protected WyilFile.Case propagate(WyilFile.Case mcase) { + protected WyilFile.Case propagate(WyilFile.Case mcase) { // TODO: back propagate through pre- and post-conditions - + methodCase = mcase; - - Code.Block precondition = mcase.precondition(); - if (precondition != null) { - precondition = propagate(precondition); + + ArrayList requires = new ArrayList( + mcase.precondition()); + for (int i = 0; i != requires.size(); ++i) { + Code.Block tmp = propagate(requires.get(i)); + requires.set(i, tmp); } - Code.Block postcondition = mcase.postcondition(); - if (postcondition != null) { - postcondition = propagate(postcondition); + ArrayList ensures = new ArrayList( + mcase.postcondition()); + for (int i = 0; i != ensures.size(); ++i) { + Code.Block tmp = propagate(ensures.get(i)); + ensures.set(i, tmp); } Code.Block body = mcase.body(); if (body != null) { body = propagate(body); } - return new WyilFile.Case(body, precondition, postcondition, - mcase.attributes()); + return new WyilFile.Case(body, requires, ensures, mcase.attributes()); } protected Code.Block propagate(Code.Block block) { diff --git a/modules/wyil/src/wyil/transforms/ConstantPropagation.java b/modules/wyil/src/wyil/transforms/ConstantPropagation.java index 339a124893..c869e4065a 100755 --- a/modules/wyil/src/wyil/transforms/ConstantPropagation.java +++ b/modules/wyil/src/wyil/transforms/ConstantPropagation.java @@ -94,24 +94,26 @@ public Env initialStore() { } @Override - public WyilFile.Case propagate(WyilFile.Case mcase) { - // TODO: back propagate through pre- and post-conditions - Code.Block precondition = mcase.precondition(); - Code.Block postcondition = mcase.postcondition(); - if (precondition != null) { - precondition = propagate(precondition); + public WyilFile.Case propagate(WyilFile.Case mcase) { + ArrayList requires = new ArrayList( + mcase.precondition()); + for (int i = 0; i != requires.size(); ++i) { + Code.Block tmp = propagate(requires.get(i)); + requires.set(i, tmp); } - if (postcondition != null) { - postcondition = propagate(postcondition); + ArrayList ensures = new ArrayList( + mcase.postcondition()); + for (int i = 0; i != ensures.size(); ++i) { + Code.Block tmp = propagate(ensures.get(i)); + ensures.set(i, tmp); } - + Code.Block body = mcase.body(); - if(body != null) { + if (body != null) { body = propagate(body); - } - - return new WyilFile.Case(body, precondition, postcondition, - mcase.attributes()); + } + + return new WyilFile.Case(body, requires, ensures, mcase.attributes()); } public Code.Block propagate(Code.Block body) { diff --git a/modules/wyil/src/wyil/transforms/LiveVariablesAnalysis.java b/modules/wyil/src/wyil/transforms/LiveVariablesAnalysis.java index b68a12f410..7482c42bf7 100755 --- a/modules/wyil/src/wyil/transforms/LiveVariablesAnalysis.java +++ b/modules/wyil/src/wyil/transforms/LiveVariablesAnalysis.java @@ -136,21 +136,24 @@ public WyilFile.TypeDeclaration propagate(WyilFile.TypeDeclaration type) { @Override public WyilFile.Case propagate(WyilFile.Case mcase) { - Code.Block precondition = mcase.precondition(); - Code.Block postcondition = mcase.postcondition(); - Code.Block body = mcase.body(); - if (precondition != null) { - precondition = propagate(precondition); + ArrayList requires = new ArrayList( + mcase.precondition()); + for (int i = 0; i != requires.size(); ++i) { + Code.Block tmp = propagate(requires.get(i)); + requires.set(i, tmp); } - if (postcondition != null) { - postcondition = propagate(postcondition); + ArrayList ensures = new ArrayList( + mcase.postcondition()); + for (int i = 0; i != ensures.size(); ++i) { + Code.Block tmp = propagate(ensures.get(i)); + ensures.set(i, tmp); } + Code.Block body = mcase.body(); if (body != null) { body = propagate(body); } - return new WyilFile.Case(body, precondition, postcondition, - mcase.attributes()); + return new WyilFile.Case(body, requires, ensures, mcase.attributes()); } public Code.Block propagate(Code.Block body) { diff --git a/modules/wyil/src/wyil/transforms/RuntimeAssertions.java b/modules/wyil/src/wyil/transforms/RuntimeAssertions.java index b27f952f64..e5e705fe78 100644 --- a/modules/wyil/src/wyil/transforms/RuntimeAssertions.java +++ b/modules/wyil/src/wyil/transforms/RuntimeAssertions.java @@ -235,8 +235,10 @@ public Code.Block transform(Code.Block.Entry entry, int freeSlot, */ public Code.Block transform(Codes.Invoke code, int freeSlot, SyntacticElement elem) throws Exception { - Code.Block precondition = findPrecondition(code.name, code.type(), elem); - if (precondition != null) { + + List precondition = findPrecondition(code.name, code.type(), elem); + + if (precondition.size() > 0) { Code.Block blk = new Code.Block(0); List paramTypes = code.type().params(); @@ -248,10 +250,12 @@ public Code.Block transform(Codes.Invoke code, int freeSlot, binding.put(i, code_operands[i]); } - precondition = resource(precondition, - elem.attribute(Attribute.Source.class)); + for(Code.Block requires : precondition) { + requires = resource(requires, + elem.attribute(Attribute.Source.class)); - importExternalAssert(blk, precondition, binding); + importExternalAssert(blk, requires, binding); + } return blk; } @@ -271,23 +275,22 @@ public Code.Block transform(Codes.Return code, int freeSlot, SyntacticElement elem, WyilFile.Case methodCase, WyilFile.FunctionOrMethodDeclaration method) { - if (code.type != Type.T_VOID) { - Code.Block postcondition = methodCase.postcondition(); - if (postcondition != null) { - Code.Block nBlock = new Code.Block(0); - HashMap binding = new HashMap(); - binding.put(0, code.operand); - Type.FunctionOrMethod mtype = method.type(); - int pIndex = 1; - int shadowIndex = methodCase.body().numSlots(); - for (Type p : mtype.params()) { - binding.put(pIndex++, shadowIndex++); - } + if (code.type != Type.T_VOID && methodCase.postcondition().size() > 0) { + Code.Block nBlock = new Code.Block(0); + HashMap binding = new HashMap(); + binding.put(0, code.operand); + Type.FunctionOrMethod mtype = method.type(); + int pIndex = 1; + int shadowIndex = methodCase.body().numSlots(); + for (Type p : mtype.params()) { + binding.put(pIndex++, shadowIndex++); + } + for (Code.Block postcondition : methodCase.postcondition()) { Code.Block block = resource(postcondition, elem.attribute(Attribute.Source.class)); - importExternalAssert(nBlock,block, binding); - return nBlock; + importExternalAssert(nBlock, block, binding); } + return nBlock; } return null; @@ -425,7 +428,7 @@ public Code.Block transform(Codes.BinaryOperator code, int freeSlot, SyntacticEl return null; } - protected Code.Block findPrecondition(NameID name, Type.FunctionOrMethod fun, + protected List findPrecondition(NameID name, Type.FunctionOrMethod fun, SyntacticElement elem) throws Exception { Path.Entry e = builder.project().get(name.module(),WyilFile.ContentType); if(e == null) { @@ -443,7 +446,7 @@ protected Code.Block findPrecondition(NameID name, Type.FunctionOrMethod fun, return c.precondition(); } } - return null; + return Collections.EMPTY_LIST; } private java.util.List attributes(SyntacticElement elem) { From 63fede315692db02ab9d419b37a54291ecebd3ec Mon Sep 17 00:00:00 2001 From: DavePearce Date: Mon, 8 Sep 2014 20:01:40 +1200 Subject: [PATCH 02/11] WyIL: Bug fix for #435. There was a problem related to the construction of postconditions and their input variables. --- modules/wyc/src/wyc/builder/CodeGenerator.java | 10 ++++++---- .../wyil/src/wyil/transforms/RuntimeAssertions.java | 3 ++- 2 files changed, 8 insertions(+), 5 deletions(-) diff --git a/modules/wyc/src/wyc/builder/CodeGenerator.java b/modules/wyc/src/wyc/builder/CodeGenerator.java index 4c5992f1d0..b0a142aa19 100644 --- a/modules/wyc/src/wyc/builder/CodeGenerator.java +++ b/modules/wyc/src/wyc/builder/CodeGenerator.java @@ -495,14 +495,16 @@ private List generate( postEnv.allocate(ftype.params().get(paramIndex), p.name()); paramIndex++; } - + Code.Block template = new Code.Block(postEnv.size()); + addDeclaredVariables(root, fd.ret, fd.resolvedType().ret() + .raw(), postEnv, template); + for (Expr condition : fd.ensures) { // FIXME: this should be added to RuntimeAssertions Code.Block block = new Code.Block(postEnv.size()); - addDeclaredVariables(root, fd.ret, fd.resolvedType().ret().raw(), - postEnv, block); + block.addAll(template); String endLab = CodeUtils.freshLabel(); - generateCondition(endLab, condition, postEnv, block, fd); + generateCondition(endLab, condition, new Environment(postEnv), block, fd); block.add(Codes.Fail("postcondition not satisfied"),attributes(condition)); block.add(Codes.Label(endLab)); ensures.add(block); diff --git a/modules/wyil/src/wyil/transforms/RuntimeAssertions.java b/modules/wyil/src/wyil/transforms/RuntimeAssertions.java index e5e705fe78..4e27b49ee4 100644 --- a/modules/wyil/src/wyil/transforms/RuntimeAssertions.java +++ b/modules/wyil/src/wyil/transforms/RuntimeAssertions.java @@ -285,9 +285,10 @@ public Code.Block transform(Codes.Return code, int freeSlot, for (Type p : mtype.params()) { binding.put(pIndex++, shadowIndex++); } + for (Code.Block postcondition : methodCase.postcondition()) { Code.Block block = resource(postcondition, - elem.attribute(Attribute.Source.class)); + elem.attribute(Attribute.Source.class)); importExternalAssert(nBlock, block, binding); } return nBlock; From fc16f0438be4e64e064f5d45363f51eda8c66789 Mon Sep 17 00:00:00 2001 From: DavePearce Date: Mon, 8 Sep 2014 20:35:47 +1200 Subject: [PATCH 03/11] WyIL: working on figuring last few bugs for #435. --- modules/wyc/src/wyc/builder/CodeGenerator.java | 2 +- modules/wycs/src/wycs/syntax/Expr.java | 8 +++++++- 2 files changed, 8 insertions(+), 2 deletions(-) diff --git a/modules/wyc/src/wyc/builder/CodeGenerator.java b/modules/wyc/src/wyc/builder/CodeGenerator.java index b0a142aa19..5f7a9ada09 100644 --- a/modules/wyc/src/wyc/builder/CodeGenerator.java +++ b/modules/wyc/src/wyc/builder/CodeGenerator.java @@ -1606,7 +1606,7 @@ private int generate(Expr.Lambda expr, Environment environment, Code.Block codes ArrayList modifiers = new ArrayList(); modifiers.add(Modifier.PRIVATE); ArrayList cases = new ArrayList(); - cases.add(new WyilFile.Case(body, null, null, attributes(expr))); + cases.add(new WyilFile.Case(body, Collections.EMPTY_LIST, Collections.EMPTY_LIST, attributes(expr))); WyilFile.FunctionOrMethodDeclaration lambda = new WyilFile.FunctionOrMethodDeclaration( modifiers, name, cfm, cases, attributes(expr)); lambdas.add(lambda); diff --git a/modules/wycs/src/wycs/syntax/Expr.java b/modules/wycs/src/wycs/syntax/Expr.java index 5ff2f4dcb7..0bc044daa8 100644 --- a/modules/wycs/src/wycs/syntax/Expr.java +++ b/modules/wycs/src/wycs/syntax/Expr.java @@ -390,13 +390,19 @@ private Op(int offset) { public Binary(Op op, Expr lhs, Expr rhs, Attribute... attributes) { super(attributes); + if(lhs == null || rhs == null) { + throw new IllegalArgumentException("invalid left or right operand"); + } this.op = op; this.leftOperand = lhs; this.rightOperand = rhs; } - public Binary(Op op, Expr lhs, Expr rhs, Collection attributes) { + public Binary(Op op, Expr lhs, Expr rhs, Collection attributes) { super(attributes); + if(lhs == null || rhs == null) { + throw new IllegalArgumentException("invalid left or right operand"); + } this.op = op; this.leftOperand = lhs; this.rightOperand = rhs; From 1c73faf58e0b49d52ce37fde73bed98ace088cc1 Mon Sep 17 00:00:00 2001 From: DavePearce Date: Tue, 9 Sep 2014 09:20:56 +1200 Subject: [PATCH 04/11] WyIL: Attempting to resolve problems for #435. Specifically, there is some bug which is causing two tests to fail. The bug appears to be related to a block which is imported in RuntimeAssertions representing the precondition of an invocation. For some reason, the inputs for this precondition are set wrong, or something is somehow going wrong. --- modules/wyc/src/wyc/builder/CodeGenerator.java | 7 ++++--- modules/wyil/src/wyil/builders/VcTransformer.java | 6 +++--- modules/wyil/src/wyil/transforms/RuntimeAssertions.java | 8 ++++---- 3 files changed, 11 insertions(+), 10 deletions(-) diff --git a/modules/wyc/src/wyc/builder/CodeGenerator.java b/modules/wyc/src/wyc/builder/CodeGenerator.java index 5f7a9ada09..2ea04dbd5c 100644 --- a/modules/wyc/src/wyc/builder/CodeGenerator.java +++ b/modules/wyc/src/wyc/builder/CodeGenerator.java @@ -495,14 +495,15 @@ private List generate( postEnv.allocate(ftype.params().get(paramIndex), p.name()); paramIndex++; } - Code.Block template = new Code.Block(postEnv.size()); + + int num_inputs = postEnv.size(); + Code.Block template = new Code.Block(num_inputs); addDeclaredVariables(root, fd.ret, fd.resolvedType().ret() .raw(), postEnv, template); for (Expr condition : fd.ensures) { // FIXME: this should be added to RuntimeAssertions - Code.Block block = new Code.Block(postEnv.size()); - block.addAll(template); + Code.Block block = new Code.Block(num_inputs,template); String endLab = CodeUtils.freshLabel(); generateCondition(endLab, condition, new Environment(postEnv), block, fd); block.add(Codes.Fail("postcondition not satisfied"),attributes(condition)); diff --git a/modules/wyil/src/wyil/builders/VcTransformer.java b/modules/wyil/src/wyil/builders/VcTransformer.java index 042cb66a60..92e41b4ac7 100644 --- a/modules/wyil/src/wyil/builders/VcTransformer.java +++ b/modules/wyil/src/wyil/builders/VcTransformer.java @@ -400,10 +400,10 @@ protected void transform(Codes.Invoke code, VcBranch branch) wycsFile.add(wycsFile.new Function(toIdentifier(code.name), Collections.EMPTY_LIST, from, to, null)); - List requires = findPostcondition(code.name, code.type(), + List ensures = findPostcondition(code.name, code.type(), branch.entry()); - if (requires.size() > 0) { + if (ensures.size() > 0) { // operands = Arrays.copyOf(operands, operands.length); Expr[] arguments = new Expr[operands.length + 1]; System.arraycopy(operands, 0, arguments, 1, operands.length); @@ -414,7 +414,7 @@ protected void transform(Codes.Invoke code, VcBranch branch) types[i+1] = paramTypes.get(i); } types[0] = branch.typeOf(code.target()); - for(Code.Block postcondition : requires) { + for(Code.Block postcondition : ensures) { Expr constraint = transformExternalBlock(postcondition, arguments, types, branch); // assume the post condition holds diff --git a/modules/wyil/src/wyil/transforms/RuntimeAssertions.java b/modules/wyil/src/wyil/transforms/RuntimeAssertions.java index 4e27b49ee4..4662d554ea 100644 --- a/modules/wyil/src/wyil/transforms/RuntimeAssertions.java +++ b/modules/wyil/src/wyil/transforms/RuntimeAssertions.java @@ -185,7 +185,7 @@ public WyilFile.Case transform(WyilFile.Case mcase, public int buildShadows(Code.Block body, WyilFile.Case mcase, WyilFile.FunctionOrMethodDeclaration method) { int freeSlot = mcase.body().numSlots(); - if (mcase.postcondition() != null) { + if (mcase.postcondition().size() > 0) { // List params = method.type().params(); for (int i = 0; i != params.size(); ++i) { @@ -196,7 +196,7 @@ public int buildShadows(Code.Block body, WyilFile.Case mcase, } return freeSlot; } - + public Code.Block transform(Code.Block.Entry entry, int freeSlot, WyilFile.Case methodCase, WyilFile.FunctionOrMethodDeclaration method) { Code code = entry.code; @@ -249,14 +249,14 @@ public Code.Block transform(Codes.Invoke code, int freeSlot, for (int i = 0; i != code_operands.length; ++i) { binding.put(i, code_operands[i]); } - + for(Code.Block requires : precondition) { requires = resource(requires, elem.attribute(Attribute.Source.class)); importExternalAssert(blk, requires, binding); } - + return blk; } From c5831ec9ca0fdef97e993c8348fb633c711c34b5 Mon Sep 17 00:00:00 2001 From: DavePearce Date: Tue, 9 Sep 2014 12:46:59 +1200 Subject: [PATCH 05/11] WyIL: Fixed bug in WyiFileWriter #435. The WyilFileWriter was not correctly writing out the number of pre- or post-condition blocks when there was more than one. --- modules/wyil/src/wyil/io/WyilFileWriter.java | 4 +--- modules/wyil/src/wyil/transforms/RuntimeAssertions.java | 2 +- 2 files changed, 2 insertions(+), 4 deletions(-) diff --git a/modules/wyil/src/wyil/io/WyilFileWriter.java b/modules/wyil/src/wyil/io/WyilFileWriter.java index 9d4ab0e560..2326fa715e 100644 --- a/modules/wyil/src/wyil/io/WyilFileWriter.java +++ b/modules/wyil/src/wyil/io/WyilFileWriter.java @@ -427,11 +427,9 @@ private byte[] generateFunctionOrMethodCaseBlock(WyilFile.Case c) throws IOExcep ByteArrayOutputStream bytes = new ByteArrayOutputStream(); BinaryOutputStream output = new BinaryOutputStream(bytes); - int preconditionCount = c.precondition() == null ? 0 : 1; - int postconditionCount = c.postcondition() == null ? 0 : 1; int bodyCount = c.body() == null ? 0 : 1; - output.write_uv(preconditionCount + postconditionCount + bodyCount); + output.write_uv(c.precondition().size() + c.postcondition().size() + bodyCount); for(Code.Block requires : c.precondition()) { writeBlock(BLOCK_Precondition,requires,output); } diff --git a/modules/wyil/src/wyil/transforms/RuntimeAssertions.java b/modules/wyil/src/wyil/transforms/RuntimeAssertions.java index 4662d554ea..adf2257de0 100644 --- a/modules/wyil/src/wyil/transforms/RuntimeAssertions.java +++ b/modules/wyil/src/wyil/transforms/RuntimeAssertions.java @@ -256,7 +256,7 @@ public Code.Block transform(Codes.Invoke code, int freeSlot, importExternalAssert(blk, requires, binding); } - + return blk; } From 291e737cf7f947948dbd4c9123ddb2ac3e2ceb30 Mon Sep 17 00:00:00 2001 From: DavePearce Date: Tue, 9 Sep 2014 13:01:55 +1200 Subject: [PATCH 06/11] WyC: Bug fix for precondition generation #435. There was a minor bug in the way that preconditions were being generated. This was causing issues during verification. --- modules/wyc/src/wyc/builder/CodeGenerator.java | 9 +++++---- modules/wyil/src/wyil/transforms/RuntimeAssertions.java | 4 ++-- 2 files changed, 7 insertions(+), 6 deletions(-) diff --git a/modules/wyc/src/wyc/builder/CodeGenerator.java b/modules/wyc/src/wyc/builder/CodeGenerator.java index 2ea04dbd5c..f37a51dc46 100644 --- a/modules/wyc/src/wyc/builder/CodeGenerator.java +++ b/modules/wyc/src/wyc/builder/CodeGenerator.java @@ -456,9 +456,10 @@ private List generate( // Now, map the parameter to its index Code.Block constraint = generate(p.type, p); - if (constraint != null) { + if (constraint != null) { + constraint = new Code.Block(nparams,constraint); constraint = shiftBlockExceptionZero(nparams, paramIndex, - constraint); + constraint); requires.add(constraint); } environment.allocate(ftype.params().get(paramIndex++),p.name()); @@ -466,7 +467,7 @@ private List generate( // Resolve pre- and post-condition - for (Expr condition : fd.requires) { + for (Expr condition : fd.requires) { Code.Block block = new Code.Block(nparams); // FIXME: this should be added to RuntimeAssertions String endLab = CodeUtils.freshLabel(); @@ -509,7 +510,7 @@ private List generate( block.add(Codes.Fail("postcondition not satisfied"),attributes(condition)); block.add(Codes.Label(endLab)); ensures.add(block); - } + } } // ================================================================== diff --git a/modules/wyil/src/wyil/transforms/RuntimeAssertions.java b/modules/wyil/src/wyil/transforms/RuntimeAssertions.java index adf2257de0..6b3c4db82b 100644 --- a/modules/wyil/src/wyil/transforms/RuntimeAssertions.java +++ b/modules/wyil/src/wyil/transforms/RuntimeAssertions.java @@ -256,7 +256,7 @@ public Code.Block transform(Codes.Invoke code, int freeSlot, importExternalAssert(blk, requires, binding); } - + return blk; } @@ -497,7 +497,7 @@ private java.util.List attributes(SyntacticElement elem) { public void importExternalAssert(Code.Block block, Code.Block external, Map binding) { int freeSlot = block.numSlots(); - + // First, sanity check that all input variables are bound HashMap nbinding = new HashMap(); for (int i = 0; i != external.numInputs(); ++i) { From 0ea91828af80620346bdd6929543fc7eeaf6a02a Mon Sep 17 00:00:00 2001 From: DavePearce Date: Tue, 9 Sep 2014 21:33:06 +1200 Subject: [PATCH 07/11] WyC: Bug fix for Postcondition Generation #435 This is a bug which is confirmed to have existed before, but somehow got through. I'm not quite sure how! --- modules/wyc/src/wyc/builder/CodeGenerator.java | 2 ++ modules/wyil/src/wyil/transforms/RuntimeAssertions.java | 2 +- 2 files changed, 3 insertions(+), 1 deletion(-) diff --git a/modules/wyc/src/wyc/builder/CodeGenerator.java b/modules/wyc/src/wyc/builder/CodeGenerator.java index f37a51dc46..840320c4cd 100644 --- a/modules/wyc/src/wyc/builder/CodeGenerator.java +++ b/modules/wyc/src/wyc/builder/CodeGenerator.java @@ -484,6 +484,8 @@ private List generate( Code.Block retInvariant = generate(fd.ret.toSyntacticType(),fd); if(retInvariant != null) { + retInvariant = shiftBlockExceptionZero(nparams, 0, + retInvariant); ensures.add(retInvariant); } diff --git a/modules/wyil/src/wyil/transforms/RuntimeAssertions.java b/modules/wyil/src/wyil/transforms/RuntimeAssertions.java index 6b3c4db82b..896a3339b8 100644 --- a/modules/wyil/src/wyil/transforms/RuntimeAssertions.java +++ b/modules/wyil/src/wyil/transforms/RuntimeAssertions.java @@ -288,7 +288,7 @@ public Code.Block transform(Codes.Return code, int freeSlot, for (Code.Block postcondition : methodCase.postcondition()) { Code.Block block = resource(postcondition, - elem.attribute(Attribute.Source.class)); + elem.attribute(Attribute.Source.class)); importExternalAssert(nBlock, block, binding); } return nBlock; From a7f4e92c88b448f6e92f652df19b7dde4db7408c Mon Sep 17 00:00:00 2001 From: DavePearce Date: Wed, 10 Sep 2014 10:03:25 +1200 Subject: [PATCH 08/11] WyC: Yet another bug fix for #435; related to #436. This is yet another bug fix related to the incorrect normalisation of type invariants for inclusion into postconditions. The problem is related to the fact that a type invariant has only one input, whereas a postcondition has at least as many inputs as there are parameters. --- modules/wyc/src/wyc/builder/CodeGenerator.java | 7 ++++--- modules/wyil/src/wyil/transforms/RuntimeAssertions.java | 2 +- 2 files changed, 5 insertions(+), 4 deletions(-) diff --git a/modules/wyc/src/wyc/builder/CodeGenerator.java b/modules/wyc/src/wyc/builder/CodeGenerator.java index 840320c4cd..180f1057bf 100644 --- a/modules/wyc/src/wyc/builder/CodeGenerator.java +++ b/modules/wyc/src/wyc/builder/CodeGenerator.java @@ -484,8 +484,9 @@ private List generate( Code.Block retInvariant = generate(fd.ret.toSyntacticType(),fd); if(retInvariant != null) { - retInvariant = shiftBlockExceptionZero(nparams, 0, - retInvariant); + retInvariant = new Code.Block(nparams + 1, retInvariant); + retInvariant = shiftBlockExceptionZero(nparams+1, 0, + retInvariant); ensures.add(retInvariant); } @@ -499,7 +500,7 @@ private List generate( paramIndex++; } - int num_inputs = postEnv.size(); + int num_inputs = postEnv.size(); Code.Block template = new Code.Block(num_inputs); addDeclaredVariables(root, fd.ret, fd.resolvedType().ret() .raw(), postEnv, template); diff --git a/modules/wyil/src/wyil/transforms/RuntimeAssertions.java b/modules/wyil/src/wyil/transforms/RuntimeAssertions.java index 896a3339b8..62c963e712 100644 --- a/modules/wyil/src/wyil/transforms/RuntimeAssertions.java +++ b/modules/wyil/src/wyil/transforms/RuntimeAssertions.java @@ -285,7 +285,7 @@ public Code.Block transform(Codes.Return code, int freeSlot, for (Type p : mtype.params()) { binding.put(pIndex++, shadowIndex++); } - + for (Code.Block postcondition : methodCase.postcondition()) { Code.Block block = resource(postcondition, elem.attribute(Attribute.Source.class)); From 2d9a81543e0f20e29f86e883566551b10b638664 Mon Sep 17 00:00:00 2001 From: DavePearce Date: Thu, 11 Sep 2014 21:42:13 +1200 Subject: [PATCH 09/11] WyC: Uncommented tests which now pass. A number of verification tests now pass as a result of the previous bug fix. I have now gone through and uncommented these. There were about 9 of them, and could be others since I didn't try them all. --- .../wyc/testing/AllValidVerificationTests.java | 18 +++++++++--------- 1 file changed, 9 insertions(+), 9 deletions(-) diff --git a/modules/wyc/src/wyc/testing/AllValidVerificationTests.java b/modules/wyc/src/wyc/testing/AllValidVerificationTests.java index f85341cbdc..5f9714d2f8 100644 --- a/modules/wyc/src/wyc/testing/AllValidVerificationTests.java +++ b/modules/wyc/src/wyc/testing/AllValidVerificationTests.java @@ -573,7 +573,7 @@ public void ConstrainedList_Valid_15() { runTest("ConstrainedList_Valid_15"); } - @Ignore("Issue ???") @Test + @Test public void ConstrainedList_Valid_16() { runTest("ConstrainedList_Valid_16"); } @@ -628,7 +628,7 @@ public void ConstrainedList_Valid_25() { runTest("ConstrainedList_Valid_25"); } - @Ignore("#290") @Test + @Test public void ConstrainedList_Valid_26() { runTest("ConstrainedList_Valid_26"); } @@ -653,7 +653,7 @@ public void ConstrainedList_Valid_6() { runTest("ConstrainedList_Valid_6"); } - @Ignore("#290") @Test + @Test public void ConstrainedList_Valid_7() { runTest("ConstrainedList_Valid_7"); } @@ -663,7 +663,7 @@ public void ConstrainedList_Valid_8() { runTest("ConstrainedList_Valid_8"); } - @Ignore("Timeout") @Test + @Test public void ConstrainedList_Valid_9() { runTest("ConstrainedList_Valid_9"); } @@ -1093,7 +1093,7 @@ public void Function_Valid_12() { runTest("Function_Valid_12"); } - @Ignore("#289") @Test + @Test public void Function_Valid_13() { runTest("Function_Valid_13"); } @@ -1517,7 +1517,7 @@ public void ListAssign_Valid_7() { runTest("ListAssign_Valid_7"); } - @Ignore("Timeout") @Test + @Test public void ListAssign_Valid_8() { runTest("ListAssign_Valid_8"); } @@ -1592,7 +1592,7 @@ public void ListSublist_Valid_1() { runTest("ListSublist_Valid_1"); } - @Ignore("#232") @Test + @Test public void ListSublist_Valid_2() { runTest("ListSublist_Valid_2"); } @@ -1607,7 +1607,7 @@ public void ListSublist_Valid_4() { runTest("ListSublist_Valid_4"); } - @Ignore("#232") @Test + @Test public void ListSublist_Valid_5() { runTest("ListSublist_Valid_5"); } @@ -1910,7 +1910,7 @@ public void RealNeg_Valid_2() { runTest("RealNeg_Valid_2"); } - @Ignore("Issue ???") @Test + @Test public void RealSplit_Valid_1() { runTest("RealSplit_Valid_1"); } From 7eb8d233cc318d899e9b59af9e48c452282a99f9 Mon Sep 17 00:00:00 2001 From: DavePearce Date: Sat, 13 Sep 2014 10:48:55 +1200 Subject: [PATCH 10/11] WyC: Transcribed documentation for CodeGenerator. When the OldCodeGenerator replaced CodeGenerator, a lot of useful documentation was lost in the process. However, I've now gone through and manually recovered this documentation so that it's not lost. In fact, there's some good stuff there!! Also, some simple tweaks which reduced the code in the current CodeGenerator. --- .../wyc/src/wyc/builder/CodeGenerator.java | 807 +++++++++++++++++- 1 file changed, 761 insertions(+), 46 deletions(-) diff --git a/modules/wyc/src/wyc/builder/CodeGenerator.java b/modules/wyc/src/wyc/builder/CodeGenerator.java index 180f1057bf..d4e67bccf6 100644 --- a/modules/wyc/src/wyc/builder/CodeGenerator.java +++ b/modules/wyc/src/wyc/builder/CodeGenerator.java @@ -242,6 +242,10 @@ public Code.Block generate(NameID nid) throws Exception { if(blk == null) { blk = new Code.Block(1); } + // Setup the environment which maps source variables to block + // registers. This is determined by allocating the root variable to + // register 0, and then creating any variables declared in the type + // pattern by from this root. Environment environment = new Environment(); int root = environment.allocate(td.resolvedType.raw()); addDeclaredVariables(root, td.pattern, @@ -439,6 +443,9 @@ public Code.Block generate(SyntacticType t, Context context) throws Exception { private List generate( WhileyFile.FunctionOrMethod fd) throws Exception { Type.FunctionOrMethod ftype = fd.resolvedType().raw(); + + // The environment maintains the mapping from source-level variables to + // the registers in WyIL block(s). Environment environment = new Environment(); // method return type @@ -462,6 +469,7 @@ private List generate( constraint); requires.add(constraint); } + // allocate parameter to register in the current block environment.allocate(ftype.params().get(paramIndex++),p.name()); } @@ -491,6 +499,11 @@ private List generate( } if (fd.ensures.size() > 0) { + // This indicates one or more explicit ensures clauses are given. + // Therefore, we must translate each of these into Wyil bytecodes. + + // First, we need to create an appropriate environment within which + // to translate the post-conditions. Environment postEnv = new Environment(); int root = postEnv.allocate(fd.resolvedType().ret().raw(), "$"); @@ -557,9 +570,15 @@ private List generate( * environment mapping named variables to slots. * * @param stmt - * --- statement to be translated. + * --- Statement to be translated. * @param environment - * --- mapping from variable names to to slot numbers. + * --- Mapping from variable names to to slot block registers. + * @param codes + * --- Code block into which this statement is to be translated. + * @param context + * --- Enclosing context of this statement (i.e. type, constant, + * function or method declaration). The context is used to aid + * with error reporting as it determines the enclosing file. * @return */ private void generate(Stmt stmt, Environment environment, Code.Block codes, Context context) { @@ -618,6 +637,38 @@ private void generate(Stmt stmt, Environment environment, Code.Block codes, Cont } } + /** + * Translate a variable declaration statement into a WyIL block. This only + * has an effect if an initialiser expression is given; otherwise, it's + * effectively a no-op. Consider the following variable declaration: + * + * 
+	 * int v = x + 1
+	 *
+ * + * This might be translated into the following WyIL bytecodes: + * + * 
+	 * const %3 = 1                      
+	 * add %4 = %0, %3                   
+	 * return %4
+	 *
+ * + * Here, we see that variable v is allocated to register 4, + * whilst variable x is allocated to register 0. + * + * @param stmt + * --- Statement to be translated. + * @param environment + * --- Mapping from variable names to block registers. + * @param codes + * --- Code block into which this statement is to be translated. + * @param context + * --- Enclosing context of this statement (i.e. type, constant, + * function or method declaration). The context is used to aid + * with error reporting as it determines the enclosing file. + * @return + */ private void generate(VariableDeclaration s, Environment environment, Code.Block codes, Context context) { // First, we allocate this variable to a given slot in the environment. int root = environment.allocate(s.type.raw()); @@ -639,33 +690,78 @@ private void generate(VariableDeclaration s, Environment environment, Code.Block } } + /** + * Translate an assignment statement into a WyIL block. This must consider + * the different forms of assignment which are permitted in Whiley, + * including: + * + * 
+	 * x = e     // variable assignment
+	 * x,y = e   // tuple assignment
+	 * x.f = e   // field assignment
+	 * x / y = e // rational assignment
+	 * x[i] = e  // index-of assignment
+	 *
+ * + * As an example, consider the following index assignment: + * + * 
+	 * xs[i + 1] = 1
+	 *
+ * + * This might be translated into the following WyIL bytecodes: + * + * 
+	 * const %2 = 1                      
+	 * const %4 = 1                      
+	 * add %5 = %0, %4                   
+	 * update %1[%5] %2       
+	 * const %6 = 0                      
+	 * return %6
+	 *
+ * + * Here, variable i is allocated to register 0, whilst variable + * xs is allocated to register 1. The result of the index + * expression i+1 is stored in the temporary register 5. + * + * @param stmt + * --- Statement to be translated. + * @param environment + * --- Mapping from variable names to block registers. + * @param codes + * --- Code block into which this statement is to be translated. + * @param context + * --- Enclosing context of this statement (i.e. type, constant, + * function or method declaration). The context is used to aid + * with error reporting as it determines the enclosing file. + * @return + */ private void generate(Assign s, Environment environment, Code.Block codes, Context context) { + + // First, we translate the right-hand side expression and assign it to a + // temporary register. + int operand = generate(s.rhs, environment, codes, context); + + // Second, we update the left-hand side of this assignment + // appropriately. if (s.lhs instanceof Expr.AssignedVariable) { Expr.AssignedVariable v = (Expr.AssignedVariable) s.lhs; - int operand = generate(s.rhs, environment, codes, context); - - if (environment.get(v.var) == null) { - environment.put(operand,v.var); - } else { - int target = environment.get(v.var); - codes.add(Codes.Assign(s.rhs.result().raw(), target, operand), - attributes(s)); - } + + // This is the easiest case. Having translated the right-hand side + // expression, we now assign it directly to the register allocated + // for variable on the left-hand side. + int target = environment.get(v.var); + codes.add(Codes.Assign(s.rhs.result().raw(), target, operand), + attributes(s)); } else if(s.lhs instanceof Expr.RationalLVal) { Expr.RationalLVal tg = (Expr.RationalLVal) s.lhs; + // Having translated the right-hand side expression, we now + // destructure it using the numerator and denominator unary + // bytecodes. Expr.AssignedVariable lv = (Expr.AssignedVariable) tg.numerator; Expr.AssignedVariable rv = (Expr.AssignedVariable) tg.denominator; - if (environment.get(lv.var) == null) { - environment.allocate(Type.T_INT,lv.var); - } - if (environment.get(rv.var) == null) { - environment.allocate(Type.T_INT,rv.var); - } - - int operand = generate(s.rhs, environment, codes, context); - codes.add(Codes.UnaryOperator(s.rhs.result() .raw(), environment.get(lv.var), operand, Codes.UnaryOperatorKind.NUMERATOR), attributes(s)); @@ -676,19 +772,11 @@ private void generate(Assign s, Environment environment, Code.Block codes, Conte } else if(s.lhs instanceof Expr.Tuple) { Expr.Tuple tg = (Expr.Tuple) s.lhs; + // Having translated the right-hand side expression, we now + // destructure it using tupleload bytecodes and assign to those + // variables on the left-hand side. ArrayList fields = new ArrayList(tg.fields); - for (int i = 0; i != fields.size(); ++i) { - Expr e = fields.get(i); - if (!(e instanceof Expr.AssignedVariable)) { - WhileyFile.syntaxError(errorMessage(INVALID_TUPLE_LVAL), - context, e); - } - Expr.AssignedVariable v = (Expr.AssignedVariable) e; - if (environment.get(v.var) == null) { - environment.allocate(v.afterType.raw(), v.var); - } - } - int operand = generate(s.rhs, environment, codes, context); + for (int i = 0; i != fields.size(); ++i) { Expr.AssignedVariable v = (Expr.AssignedVariable) fields.get(i); codes.add(Codes.TupleLoad((Type.EffectiveTuple) s.rhs @@ -698,15 +786,17 @@ private void generate(Assign s, Environment environment, Code.Block codes, Conte } else if (s.lhs instanceof Expr.IndexOf || s.lhs instanceof Expr.FieldAccess || s.lhs instanceof Expr.Dereference) { - + + // This is the more complicated case, since the left-hand side + // expression is recursive. However, the WyIL update bytecode comes + // to the rescue here. All we need to do is extract the variable + // being updated and give this to the update bytecode. For example, + // in the expression "x.y.f = e" we have that variable "x" is being + // updated. ArrayList fields = new ArrayList(); ArrayList operands = new ArrayList(); Expr.AssignedVariable lhs = extractLVal(s.lhs, fields, operands, - environment, codes, context); - if (environment.get(lhs.var) == null) { - WhileyFile.syntaxError("unknown variable", - context, lhs); - } + environment, codes, context); int target = environment.get(lhs.var); int rhsRegister = generate(s.rhs, environment, codes, context); @@ -717,6 +807,34 @@ private void generate(Assign s, Environment environment, Code.Block codes, Conte } } + /** + * This function recurses down the left-hand side of an assignment (e.g. + * x[i] = e, x.f = e, etc) with a complex lval. The primary goal is to + * identify the left-most variable which is actually being updated. A + * secondary goal is to collect the sequence of field names being updated, + * and translate any index expressions and store them in temporary + * registers. + * + * @param e + * The LVal being extract from. + * @param fields + * The list of fields being used in the assignment. + * Initially, this is empty and is filled by this method as it + * traverses the lval. + * @param operands + * The list of temporary registers in which evaluated index + * expression are stored. Initially, this is empty and is filled + * by this method as it traverses the lval. + * @param environment + * Mapping from variable names to block registers. + * @param codes + * Code block into which this statement is to be translated. + * @param context + * Enclosing context of this statement (i.e. type, constant, + * function or method declaration). The context is used to aid + * with error reporting as it determines the enclosing file. + * @return + */ private Expr.AssignedVariable extractLVal(Expr e, ArrayList fields, ArrayList operands, Environment environment, Code.Block codes, Context context) { @@ -747,6 +865,21 @@ private Expr.AssignedVariable extractLVal(Expr e, ArrayList fields, } } + /** + * Translate an assert statement into WyIL bytecodes. + * + * @param stmt + * --- Statement to be translated. + * @param environment + * --- Mapping from variable names to block registers. + * @param codes + * --- Code block into which this statement is to be translated. + * @param context + * --- Enclosing context of this statement (i.e. type, constant, + * function or method declaration). The context is used to aid + * with error reporting as it determines the enclosing file. + * @return + */ private void generate(Assert s, Environment environment, Code.Block codes, Context context) { String endLab = CodeUtils.freshLabel(); @@ -756,6 +889,21 @@ private void generate(Assert s, Environment environment, Code.Block codes, codes.add(Codes.Label(endLab)); } + /** + * Translate an assume statement into WyIL bytecodes. + * + * @param stmt + * --- Statement to be translated. + * @param environment + * --- Mapping from variable names to block registers. + * @param codes + * --- Code block into which this statement is to be translated. + * @param context + * --- Enclosing context of this statement (i.e. type, constant, + * function or method declaration). The context is used to aid + * with error reporting as it determines the enclosing file. + * @return + */ private void generate(Assume s, Environment environment, Code.Block codes, Context context) { String endLab = CodeUtils.freshLabel(); @@ -765,6 +913,39 @@ private void generate(Assume s, Environment environment, Code.Block codes, codes.add(Codes.Label(endLab)); } + /** + * Translate a return statement into WyIL bytecodes. In the case that a + * return expression is provided, then this is first translated and stored + * in a temporary register. Consider the following return statement: + * + * 
+	 * return i * 2
+	 *
+ * + * This might be translated into the following WyIL bytecodes: + * + * 
+	 * const %3 = 2                      
+	 * mul %4 = %0, %3                   
+	 * return %4
+	 *
+ * + * Here, we see that variable I is allocated to register 0, + * whilst the result of the expression i * 2 is stored in + * register 4. + * + * @param stmt + * --- Statement to be translated. + * @param environment + * --- Mapping from variable names to block registers. + * @param codes + * --- Code block into which this statement is to be translated. + * @param context + * --- Enclosing context of this statement (i.e. type, constant, + * function or method declaration). The context is used to aid + * with error reporting as it determines the enclosing file. + * @return + */ private void generate(Return s, Environment environment, Code.Block codes, Context context) { @@ -785,17 +966,108 @@ private void generate(Return s, Environment environment, Code.Block codes, } } + /** + * Translate a skip statement into a WyIL nop bytecode. + * + * @param stmt + * --- Statement to be translated. + * @param environment + * --- Mapping from variable names to block registers. + * @param codes + * --- Code block into which this statement is to be translated. + * @param context + * --- Enclosing context of this statement (i.e. type, constant, + * function or method declaration). The context is used to aid + * with error reporting as it determines the enclosing file. + * @return + */ private void generate(Skip s, Environment environment, Code.Block codes, Context context) { codes.add(Codes.Nop, attributes(s)); } + /** + * Translate a debug statement into WyIL bytecodes. The debug expression is + * first translated and stored in a temporary register. Consider the + * following debug statement: + * + * 
+	 * debug "Hello World"
+	 *
+ * + * This might be translated into the following WyIL bytecodes: + * + * 
+	 * const %2 = "Hello World"       
+	 * debug %2
+	 *
+ * + * Here, we see that debug expression is first stored into the temporary + * register 2. + * + * @param stmt + * --- Statement to be translated. + * @param environment + * --- Mapping from variable names to block registers. + * @param codes + * --- Code block into which this statement is to be translated. + * @param context + * --- Enclosing context of this statement (i.e. type, constant, + * function or method declaration). The context is used to aid + * with error reporting as it determines the enclosing file. + * @return + */ private void generate(Debug s, Environment environment, Code.Block codes, Context context) { int operand = generate(s.expr, environment, codes, context); codes.add(Codes.Debug(operand), attributes(s)); } + /** + * Translate an if statement into WyIL bytecodes. This is done by first + * translating the condition into one or more conditional branches. The true + * and false blocks are then translated and marked with labels. Finally, an + * exit label is provided to catch the fall-through case. Consider the + * following if statement: + * + * 
+	 * if x+1 < 2:
+	 *     x = x + 1
+	 * ...
+	 *
+ * + * This might be translated into the following WyIL bytecodes: + * + * 
+	 * const %3 = 1                      
+	 * add %4 = %0, %3                   
+	 * const %5 = 2                      
+	 * ifge %4, %5 goto label0           
+	 * const %7 = 1                      
+	 * add %8 = %0, %7                   
+	 * assign %0 = %8                   
+	 * .label0                                 
+	 *    ...
+	 *
+ * + * Here, we see that result of the condition is stored into temporary + * register 4, which is then used in the comparison. In the case the + * condition is false, control jumps over the true block; otherwise, it + * enters the true block and then (because there is no false block) falls + * through. + * + * @param stmt + * --- Statement to be translated. + * @param environment + * --- Mapping from variable names to block registers. + * @param codes + * --- Code block into which this statement is to be translated. + * @param context + * --- Enclosing context of this statement (i.e. type, constant, + * function or method declaration). The context is used to aid + * with error reporting as it determines the enclosing file. + * @return + */ private void generate(IfElse s, Environment environment, Code.Block codes, Context context) { String falseLab = CodeUtils.freshLabel(); @@ -818,12 +1090,88 @@ private void generate(IfElse s, Environment environment, Code.Block codes, codes.add(Codes.Label(exitLab)); } + /** + * Translate a throw statement into WyIL bytecodes. The throw expression is + * first translated and stored in a temporary register. Consider the + * following throw statement: + * + * 
+	 * throw "Hello World"
+	 *
+ * + * This might be translated into the following WyIL bytecodes: + * + * 
+	 * const %2 = "Hello World"       
+	 * throw %2
+	 *
+ * + * Here, we see that the throw expression is first stored into the temporary + * register 2. + * + * @param stmt + * --- Statement to be translated. + * @param environment + * --- Mapping from variable names to block registers. + * @param codes + * --- Code block into which this statement is to be translated. + * @param context + * --- Enclosing context of this statement (i.e. type, constant, + * function or method declaration). The context is used to aid + * with error reporting as it determines the enclosing file. + * @return + */ private void generate(Throw s, Environment environment, Code.Block codes, Context context) { int operand = generate(s.expr, environment, codes, context); codes.add(Codes.Throw(s.expr.result().raw(), operand), s.attributes()); } + /** + * Translate a break statement into a WyIL unconditional branch bytecode. + * This requires examining the scope stack to determine the correct target + * for the branch. Consider the following use of a break statement: + * + * 
+	 * while x < 10:
+	 *    if x == 0:
+	 *       break
+	 *    x = x + 1     
+	 * ...
+	 *
+ * + * This might be translated into the following WyIL bytecodes: + * + * 
+	 * loop (%0)                               
+	 *     const %3 = 10                     
+	 *     ifge %0, %3 goto label0           
+	 *     const %5 = 0                      
+	 *     ifne %0, %5 goto label1           
+	 *     goto label0                             
+	 *     .label1                                 
+	 *     const %7 = 1                      
+	 *     add %8 = %0, %7                   
+	 *     assign %0 = %8
+	 * .label0                                                        
+	 * ...
+	 *
+ * + * Here, we see that the break statement is translated into the bytecode + * "goto label0", which exits the loop. + * + * @param stmt + * --- Statement to be translated. + * @param environment + * --- Mapping from variable names to block registers. + * @param codes + * --- Code block into which this statement is to be translated. + * @param context + * --- Enclosing context of this statement (i.e. type, constant, + * function or method declaration). The context is used to aid + * with error reporting as it determines the enclosing file. + * @return + */ private void generate(Break s, Environment environment, Code.Block codes, Context context) { BreakScope scope = findEnclosingScope(BreakScope.class); if (scope == null) { @@ -833,6 +1181,60 @@ private void generate(Break s, Environment environment, Code.Block codes, Contex codes.add(Codes.Goto(scope.label)); } + /** + * Translate a switch statement into WyIL bytecodes. This is done by first + * translating the switch expression and storing its result in a temporary + * register. Then, each case is translated in order of appearance. Consider + * the following switch statement: + * + * 
+	 * switch x+1:
+	 *     case 0,1:
+	 *         return x+1
+	 *     case 2:
+	 *         x = x - 1
+	 *     default:
+	 *         x = 0
+	 *
+ * + * This might be translated into the following WyIL bytecodes: + * + * 
+	 *     const %2 = 1                       
+	 *     add %3 = %0, %2  
+	 *     switch %3 0->label1, 1->label1, 2->label2, *->label0
+	 * .label1                                 
+	 *     const %3 = 1                       
+	 *     add %4 = %0, %3                    
+	 *     return %4                          
+	 * .label2                                 
+	 *     const %6 = 1                       
+	 *     sub %7 = %0, %6                    
+	 *     assign %0 = %7                     
+	 *     goto label3                             
+	 * .label0                                 
+	 *     const %8 = 0                       
+	 *     assign %0 = %8                     
+	 *     goto label3                             
+	 * .label3
+	 *
+ * + * Here, we see that switch expression is first stored into the temporary + * register 3. Then, each of the values 0 -- 2 is routed to the start of its + * block, with * representing the default case. + * + * @param stmt + * --- Statement to be translated. + * @param environment + * --- Mapping from variable names to block registers. + * @param codes + * --- Code block into which this statement is to be translated. + * @param context + * --- Enclosing context of this statement (i.e. type, constant, + * function or method declaration). The context is used to aid + * with error reporting as it determines the enclosing file. + * @return + */ private void generate(Switch s, Environment environment, Code.Block codes, Context context) throws Exception { String exitLab = CodeUtils.freshLabel(); @@ -900,6 +1302,50 @@ private void generate(Switch s, Environment environment, codes.add(Codes.Label(exitLab), attributes(s)); } + /** + * Translate a try-catch statement into WyIL bytecodes. Consider the + * following try-catch block: + * + * 
+	 * try:
+	 *     x = f(x+1)
+	 * catch(string err):
+	 *     return err
+	 * ...
+	 *
+ * + * This might be translated into the following WyIL bytecodes: + * + * 
+	 *     trycatch string->label4                 
+	 *         const %4 = 1                      
+	 *         add %5 = %0, %4                   
+	 *         invoke %2 = (%5) test:f : function(int) => int throws string
+	 *         goto label5                             
+	 * .label4                                 
+	 *     const %6 = 0                      
+	 *     return %6                         
+	 * .label5                                 
+	 *     ...
+	 *
+ * + * Here, we see the trycatch bytecode routes exceptions to the start of + * their catch handlers. Likewise, at the end of the try block control + * branches over the catch handlers to continue on with the remainder of the + * function. + * + * @param stmt + * --- Statement to be translated. + * @param environment + * --- Mapping from variable names to block registers. + * @param codes + * --- Code block into which this statement is to be translated. + * @param context + * --- Enclosing context of this statement (i.e. type, constant, + * function or method declaration). The context is used to aid + * with error reporting as it determines the enclosing file. + * @return + */ private void generate(TryCatch s, Environment environment, Code.Block codes, Context context) throws Exception { int start = codes.size(); int exceptionRegister = environment.allocate(Type.T_ANY); @@ -935,6 +1381,47 @@ private void generate(TryCatch s, Environment environment, Code.Block codes, Con codes.add(Codes.Label(exitLab), attributes(s)); } + /** + * Translate a while loop into WyIL bytecodes. Consider the following use of + * a while statement: + * + * 
+	 * while x < 10:
+	 *    x = x + 1     
+	 * ...
+	 *
+ * + * This might be translated into the following WyIL bytecodes: + * + * 
+	 * loop (%0)                               
+	 *     const %3 = 10                     
+	 *     ifge %0, %3 goto label0           
+	 *     const %7 = 1                      
+	 *     add %8 = %0, %7                   
+	 *     assign %0 = %8
+	 * .label0                                                        
+	 * ...
+	 *
+ * + * Here, we see that the evaluated loop condition is stored into temporary + * register 3 and that the condition is implemented using a conditional + * branch. Note that there is no explicit goto statement at the end of the + * loop body which loops back to the head (this is implicit in the loop + * bytecode). + * + * @param stmt + * --- Statement to be translated. + * @param environment + * --- Mapping from variable names to block registers. + * @param codes + * --- Code block into which this statement is to be translated. + * @param context + * --- Enclosing context of this statement (i.e. type, constant, + * function or method declaration). The context is used to aid + * with error reporting as it determines the enclosing file. + * @return + */ private void generate(While s, Environment environment, Code.Block codes, Context context) { String label = CodeUtils.freshLabel(); @@ -985,6 +1472,48 @@ private void generate(While s, Environment environment, Code.Block codes, codes.add(Codes.Label(exit), attributes(s)); } + /** + * Translate a do-while loop into WyIL bytecodes. Consider the following use + * of a do-while statement: + * + * 
+	 * do:
+	 *    x = x + 1
+	 * while x < 10     
+	 * ...
+	 *
+ * + * This might be translated into the following WyIL bytecodes: + * + * 
+	 * loop (%0)                               
+	 *     const %2 = 1                      
+	 *     add %3 = %0, %2                   
+	 *     assign %0 = %3                   
+	 *     const %5 = 10                     
+	 *     ifge %3, %5 goto label0
+	 * .label0                                                        
+	 * ...
+	 *
+ * + * Here, we see that the evaluated loop condition is stored into temporary + * register 3 and that the condition is implemented using a conditional + * branch. Note that there is no explicit goto statement at the end of the + * loop body which loops back to the head (this is implicit in the loop + * bytecode). + * + * @param stmt + * --- Statement to be translated. + * @param environment + * --- Mapping from variable names to block registers. + * @param codes + * --- Code block into which this statement is to be translated. + * @param context + * --- Enclosing context of this statement (i.e. type, constant, + * function or method declaration). The context is used to aid + * with error reporting as it determines the enclosing file. + * @return + */ private void generate(DoWhile s, Environment environment, Code.Block codes, Context context) { String label = CodeUtils.freshLabel(); @@ -1036,6 +1565,21 @@ private void generate(DoWhile s, Environment environment, Code.Block codes, codes.add(Codes.Label(exit), attributes(s)); } + /** + * Translate a forall loop into WyIL bytecodes. + * + * @param stmt + * --- Statement to be translated. + * @param environment + * --- Mapping from variable names to block registers. + * @param codes + * --- Code block into which this statement is to be translated. + * @param context + * --- Enclosing context of this statement (i.e. type, constant, + * function or method declaration). The context is used to aid + * with error reporting as it determines the enclosing file. + * @return + */ private void generate(ForAll s, Environment environment, Code.Block codes, Context context) { String label = CodeUtils.freshLabel(); @@ -1127,12 +1671,46 @@ private void generate(ForAll s, Environment environment, * Translate a source-level condition into a WyIL block, using a given * environment mapping named variables to slots. If the condition evaluates * to true, then control is transferred to the given target. Otherwise, - * control will fall through to the following bytecode. + * control will fall through to the following bytecode. This method is + * necessary because the WyIL bytecode implementing comparisons are only + * available as conditional branches. For example, consider this if + * statement: + * + * 
+	 * if x < y || x == y:
+	 *     x = y
+	 * else:
+	 *     x = -y
+	 *
+ * + * This might be translated into the following WyIL bytecodes: + * + * 
+	 *     iflt %0, %1 goto label0 : int           
+	 *     ifne %0, %1 goto label1 : int           
+	 * .label0                                                    
+	 *     assign %0 = %1  : int                   
+	 *     goto label2                             
+	 * .label1                                 
+	 *     neg %8 = %1 : int                       
+	 *     assign %0 = %8  : int                   
+	 * .label2
+	 *
+ * + * Here, we see that the condition "x < y || x == y" is broken down into two + * conditional branches (which additionally implement short-circuiting). The + * branches are carefully selected implement the semantics of the logical OR + * operator '||'. This function is responsible for translating conditional + * expressions like this into sequences of conditional branches using + * short-circuiting. * * @param target - * --- Target label to goto if condition is true. + * --- Target label to goto if condition is true. When the + * condition is false, control falls simply through to the next + * bytecode in sqeuence. * @param condition - * --- Source-level condition to be translated + * --- Source-level condition to be translated into a sequence of + * one or more conditional branches. * @param environment * --- Mapping from variable names to to slot numbers. * @param codes @@ -1143,6 +1721,10 @@ private void generate(ForAll s, Environment environment, public void generateCondition(String target, Expr condition, Environment environment, Code.Block codes, Context context) { try { + + // First, we see whether or not we can employ a special handler for + // translating this condition. + if (condition instanceof Expr.Constant) { generateCondition(target, (Expr.Constant) condition, environment, codes, context); @@ -1162,10 +1744,10 @@ public void generateCondition(String target, Expr condition, || condition instanceof Expr.FieldAccess || condition instanceof Expr.IndexOf) { - // The default case simply compares the computed value against - // true. In some cases, we could do better. For example, !(x < - // 5) - // could be rewritten into x>=5. + // This is the default case where no special handler applies. In + // this case, we simply compares the computed value against + // true. In some cases, we could actually do better. For + // example, !(x < 5) could be rewritten into x >= 5. int r1 = generate(condition, environment, codes, context); int r2 = environment.allocate(Type.T_BOOL); @@ -1187,6 +1769,34 @@ public void generateCondition(String target, Expr condition, } + /** + *

+ * Translate a source-level condition which is a constant (i.e. + * true or false) into a WyIL block, using a given + * environment mapping named variables to slots. This may seem like a + * perverse case, but it is permitted to allow selective commenting of code. + *

+ * + *

+ * When the constant is true, an unconditional branch to the target is + * generated. Otherwise, nothing is generated and control falls through to + * the next bytecode in sequence. + *

+ * + * @param target + * --- Target label to goto if condition is true. When the + * condition is false, control falls simply through to the next + * bytecode in sqeuence. + * @param condition + * --- Source-level condition to be translated into a sequence of + * one or more conditional branches. + * @param environment + * --- Mapping from variable names to to slot numbers. + * @param codes + * --- List of bytecodes onto which translation should be + * appended. + * @return + */ private void generateCondition(String target, Expr.Constant c, Environment environment, Code.Block codes, Context context) { Constant.Bool b = (Constant.Bool) c.value; @@ -1197,6 +1807,26 @@ private void generateCondition(String target, Expr.Constant c, } } + /** + *

+ * Translate a source-level condition which is a binary expression into WyIL + * bytecodes, using a given environment mapping named variables to slots. + *

+ * + * @param target + * --- Target label to goto if condition is true. When the + * condition is false, control falls simply through to the next + * bytecode in sqeuence. + * @param condition + * --- Source-level condition to be translated into a sequence of + * one or more conditional branches. + * @param environment + * --- Mapping from variable names to to slot numbers. + * @param codes + * --- List of bytecodes onto which translation should be + * appended. + * @return + */ private void generateCondition(String target, Expr.BinOp v, Environment environment, Code.Block codes, Context context) throws Exception { @@ -1256,21 +1886,57 @@ private void generateCondition(String target, Expr.BinOp v, } } + /** + *

+ * Translate a source-level condition which represents a runtime type test + * (e.g. x is int) into WyIL bytecodes, using a given + * environment mapping named variables to slots. One subtlety of this arises + * when the lhs is a single variable. In this case, the variable will be + * retyped and, in order for this to work, we *must* perform the type test + * on the actual varaible, rather than a temporary. + *

+ * + * @param target + * --- Target label to goto if condition is true. When the + * condition is false, control falls simply through to the next + * bytecode in sqeuence. + * @param condition + * --- Source-level condition to be translated into a sequence of + * one or more conditional branches. + * @param environment + * --- Mapping from variable names to to slot numbers. + * @param codes + * --- List of bytecodes onto which translation should be + * appended. + * @return + */ private void generateTypeCondition(String target, Expr.BinOp v, Environment environment, Code.Block codes, Context context) throws Exception { int leftOperand; if (v.lhs instanceof Expr.LocalVariable) { + + // This is the case where the lhs is a single variable and, hence, + // will be retyped by this operation. In this case, we must operate + // on the original variable directly, rather than a temporary + // variable (since, otherwise, we'll retype the temporary but not + // the intended variable). Expr.LocalVariable lhs = (Expr.LocalVariable) v.lhs; if (environment.get(lhs.var) == null) { syntaxError(errorMessage(UNKNOWN_VARIABLE), context, v.lhs); } leftOperand = environment.get(lhs.var); } else { + // This is the general case whether the lhs is an arbitrary variable + // and, hence, retyping does not apply. Therefore, we can simply + // evaluate the lhs into a temporary register as per usual. leftOperand = generate(v.lhs, environment, codes, context); } + // Note, the type checker guarantees that the rhs is a type val, so the + // following cast is always safe. Expr.TypeVal rhs = (Expr.TypeVal) v.rhs; + Code.Block constraint = generate(rhs.unresolvedType, context); if (constraint != null) { String exitLabel = CodeUtils.freshLabel(); @@ -1301,11 +1967,39 @@ private void generateTypeCondition(String target, Expr.BinOp v, } } + /** + *

+ * Translate a source-level condition which represents a unary condition + * into WyIL bytecodes, using a given environment mapping named variables to + * slots. Note, the only valid unary condition is logical not. To implement + * this, we simply generate the underlying condition and reroute its + * branch targets. + *

+ * + * @param target + * --- Target label to goto if condition is true. When the + * condition is false, control falls simply through to the next + * bytecode in sqeuence. + * @param condition + * --- Source-level condition to be translated into a sequence of + * one or more conditional branches. + * @param environment + * --- Mapping from variable names to to slot numbers. + * @param codes + * --- List of bytecodes onto which translation should be + * appended. + * @return + */ private void generateCondition(String target, Expr.UnOp v, Environment environment, Code.Block codes, Context context) { Expr.UOp uop = v.op; switch (uop) { case NOT: + + // What we do is generate the underlying expression whilst setting + // its true destination to a temporary label. Then, for the fall + // through case we branch to our true destination. + String label = CodeUtils.freshLabel(); generateCondition(label, v.mhs, environment, codes, context); codes.add(Codes.Goto(target)); @@ -1315,6 +2009,27 @@ private void generateCondition(String target, Expr.UnOp v, syntaxError(errorMessage(INVALID_BOOLEAN_EXPRESSION), context, v); } + /** + *

+ * Translate a source-level condition which represents a quantifier + * expression into WyIL bytecodes, using a given environment mapping named + * variables to slots. + *

+ * + * @param target + * --- Target label to goto if condition is true. When the + * condition is false, control falls simply through to the next + * bytecode in sqeuence. + * @param condition + * --- Source-level condition to be translated into a sequence of + * one or more conditional branches. + * @param environment + * --- Mapping from variable names to to slot numbers. + * @param codes + * --- List of bytecodes onto which translation should be + * appended. + * @return + */ private void generateCondition(String target, Expr.Comprehension e, Environment environment, Code.Block codes, Context context) { if (e.cop != Expr.COp.NONE && e.cop != Expr.COp.SOME && e.cop != Expr.COp.ALL) { @@ -2193,7 +2908,7 @@ public static void addDeclaredVariables(int root, TypePattern pattern, Type type private static final Code.Block EMPTY_BLOCK = new Code.Block(1); - + @SuppressWarnings("incomplete-switch") private static Expr invert(Expr e) { if (e instanceof Expr.BinOp) { Expr.BinOp bop = (Expr.BinOp) e; From 0c26aea96d1206e02242902a5792db44e41f4c85 Mon Sep 17 00:00:00 2001 From: DavePearce Date: Wed, 8 Oct 2014 18:18:14 +1300 Subject: [PATCH 11/11] Feature Complete for #435. This feels a bit like a hack really, though it is providing some useful additional error reporting. The basic problem is that the system is not well designed to support error messages with context. --- modules/wybs/src/wycc/lang/Attribute.java | 25 +++ modules/wybs/src/wycc/lang/SyntaxError.java | 144 ++++++++++-------- .../wyc/src/wyc/testing/AllInvalidTests.java | 4 +- modules/wycc/src/wycc/lang/Wyil2CBuilder.java | 8 +- .../src/wycs/builders/CodeGeneration.java | 60 +++++--- .../wyil/transforms/RuntimeAssertions.java | 28 ++-- tests/invalid/ConstrainedInt_Invalid_4.sysout | 4 + .../invalid/ConstrainedList_Invalid_2.sysout | 4 + tests/invalid/ConstrainedSet_Invalid_2.sysout | 4 + tests/invalid/Ensures_Invalid_1.sysout | 4 + tests/invalid/Ensures_Invalid_2.sysout | 4 + tests/invalid/Ensures_Invalid_3.sysout | 4 + tests/invalid/For_Invalid_7.sysout | 4 + tests/invalid/ListEmpty_Invalid_2.sysout | 4 + tests/invalid/ListEquals_Invalid_1.sysout | 4 + tests/invalid/ListLength_Invalid_3.sysout | 4 + tests/invalid/Quantifiers_Invalid_1.sysout | 4 + tests/invalid/Quantifiers_Invalid_2.sysout | 4 + tests/invalid/Quantifiers_Invalid_3.sysout | 4 + tests/invalid/Quantifiers_Invalid_4.sysout | 4 + tests/invalid/Quantifiers_Invalid_5.sysout | 4 + tests/invalid/Quantifiers_Invalid_6.sysout | 4 + tests/invalid/Quantifiers_Invalid_7.sysout | 4 + tests/invalid/Quantifiers_Invalid_8.sysout | 4 + tests/invalid/RealConvert_Invalid_1.sysout | 4 + tests/invalid/RealConvert_Invalid_2.sysout | 4 + tests/invalid/RealDiv_Invalid_2.sysout | 4 + tests/invalid/Requires_Invalid_1.sysout | 4 + tests/invalid/SetAssign_Invalid_1.sysout | 4 + .../invalid/SetComprehension_Invalid_6.sysout | 4 + tests/invalid/SetEmpty_Invalid_2.sysout | 4 + .../invalid/SetIntersection_Invalid_2.sysout | 4 + tests/invalid/SetSubset_Invalid_1.sysout | 4 + tests/invalid/SetSubset_Invalid_10.sysout | 4 + tests/invalid/SetSubset_Invalid_3.sysout | 4 + tests/invalid/SetSubset_Invalid_5.sysout | 4 + tests/invalid/SetSubset_Invalid_6.sysout | 4 + tests/invalid/SetSubset_Invalid_7.sysout | 4 + tests/invalid/SetSubset_Invalid_8.sysout | 4 + tests/invalid/SetSubset_Invalid_9.sysout | 4 + tests/invalid/SetUnion_Invalid_3.sysout | 4 + tests/invalid/SetUnion_Invalid_4.sysout | 4 + tests/invalid/While_Invalid_12.sysout | 4 + 43 files changed, 316 insertions(+), 101 deletions(-) diff --git a/modules/wybs/src/wycc/lang/Attribute.java b/modules/wybs/src/wycc/lang/Attribute.java index b96666bcd7..c5c2aca387 100755 --- a/modules/wybs/src/wycc/lang/Attribute.java +++ b/modules/wybs/src/wycc/lang/Attribute.java @@ -58,5 +58,30 @@ public String toString() { return "@" + start + ":" + end; } } + + /** + * Represents an originating source location for a given syntactic element. + * This typically occurs if some element from one file is included in + * another element from another file. + * + * @author David J. Pearce + * + */ + public final static class Origin implements Attribute { + public final String filename; + public final int start; // starting character index + public final int end; // end character index + public final int line; // line number + + public Origin(String filename, int start, int end, int line) { + this.filename = filename; + this.start = start; + this.end = end; + this.line = line; + } + public String toString() { + return filename + "@" + start + ":" + end; + } + } } diff --git a/modules/wybs/src/wycc/lang/SyntaxError.java b/modules/wybs/src/wycc/lang/SyntaxError.java index 9b46f2d25b..9783116c96 100755 --- a/modules/wybs/src/wycc/lang/SyntaxError.java +++ b/modules/wybs/src/wycc/lang/SyntaxError.java @@ -45,6 +45,7 @@ public class SyntaxError extends RuntimeException { private String filename; private int start; private int end; + private Attribute.Origin[] context; /** * Identify a syntax error at a particular point in a file. @@ -58,11 +59,12 @@ public class SyntaxError extends RuntimeException { * @param column * Column within line of file containing problem. */ - public SyntaxError(String msg, String filename, int start, int end) { + public SyntaxError(String msg, String filename, int start, int end, Attribute.Origin... context) { this.msg = msg; this.filename = filename; this.start = start; this.end = end; + this.context = context; } /** @@ -78,12 +80,13 @@ public SyntaxError(String msg, String filename, int start, int end) { * Column within line of file containing problem. */ public SyntaxError(String msg, String filename, int start, int end, - Throwable ex) { + Throwable ex, Attribute.Origin... context) { super(ex); this.msg = msg; this.filename = filename; this.start = start; this.end = end; + this.context = context; } public String getMessage() { @@ -149,71 +152,81 @@ public void outputSourceError(PrintStream output, boolean brief) { if (filename == null) { output.println("syntax error: " + getMessage()); } else { - int line = 0; - int lineStart = 0; - int lineEnd = 0; - StringBuilder text = new StringBuilder(); - try { - BufferedReader in = new BufferedReader(new InputStreamReader( - new FileInputStream(filename), "UTF-8")); + printError(output,brief,getMessage(),filename,start,end); + } + if(context != null && context.length > 0) { + if(!brief) { output.println(); } + for(Attribute.Origin o : context) { + printError(output,brief,"",o.filename,o.start,o.end); + } + } + } - // first, read whole file - int len = 0; - char[] buf = new char[1024]; - while ((len = in.read(buf)) != -1) { - text.append(buf, 0, len); - } + private static void printError(PrintStream output, boolean brief, + String message, String filename, int start, int end) { + int line = 0; + int lineStart = 0; + int lineEnd = 0; + StringBuilder text = new StringBuilder(); + try { + BufferedReader in = new BufferedReader(new InputStreamReader( + new FileInputStream(filename), "UTF-8")); - while (lineEnd < text.length() && lineEnd <= start) { - lineStart = lineEnd; - lineEnd = parseLine(text, lineEnd); - line = line + 1; - } - } catch (IOException e) { - output.println("syntax error: " + getMessage()); - return; + // first, read whole file + int len = 0; + char[] buf = new char[1024]; + while ((len = in.read(buf)) != -1) { + text.append(buf, 0, len); } - lineEnd = Math.min(lineEnd, text.length()); - if (brief) { - // brief form - output.println(filename + ":" + line + ":" - + (start - lineStart) + ":" + (end - lineStart) + ":\"" - + getMessage().replace("\n","\\n") + "\""); + while (lineEnd < text.length() && lineEnd <= start) { + lineStart = lineEnd; + lineEnd = parseLine(text, lineEnd); + line = line + 1; + } + } catch (IOException e) { + return; + } + lineEnd = Math.min(lineEnd, text.length()); + + if (brief) { + // brief form + output.println(filename + ":" + line + ":" + + (start - lineStart) + ":" + (end - lineStart) + ":\"" + + message.replace("\n","\\n") + "\""); + } else { + // Full form + output.println(filename + ":" + line + ": " + message); + // NOTE: in the following lines I don't print characters + // individually. The reason for this is that it messes up the + // ANT task output. + String str = ""; + for (int i = lineStart; i < lineEnd; ++i) { + str = str + text.charAt(i); + } + if (str.length() > 0 && str.charAt(str.length() - 1) == '\n') { + output.print(str); } else { - // Full form - output.println(filename + ":" + line + ": " + getMessage()); - // NOTE: in the following lines I don't print characters - // individually. The reason for this is that it messes up the - // ANT task output. - String str = ""; - for (int i = lineStart; i < lineEnd; ++i) { - str = str + text.charAt(i); - } - if (str.length() > 0 && str.charAt(str.length() - 1) == '\n') { - output.print(str); + // this must be the very last line of output and, in this + // particular case, there is no new-line character provided. + // Therefore, we need to provide one ourselves! + output.println(str); + } + str = ""; + for (int i = lineStart; i < start; ++i) { + if (text.charAt(i) == '\t') { + str += "\t"; } else { - // this must be the very last line of output and, in this - // particular case, there is no new-line character provided. - // Therefore, we need to provide one ourselves! - output.println(str); - } - str = ""; - for (int i = lineStart; i < start; ++i) { - if (text.charAt(i) == '\t') { - str += "\t"; - } else { - str += " "; - } - } - for (int i = start; i <= Math.min(end,lineEnd); ++i) { - str += "^"; + str += " "; } - output.println(str); } + for (int i = start; i <= Math.min(end,lineEnd); ++i) { + str += "^"; + } + output.println(str); } } - + private static int parseLine(StringBuilder buf, int index) { while (index < buf.length() && buf.charAt(index) != '\n') { index++; @@ -235,7 +248,13 @@ public static void syntaxError(String msg, String filename, end = attr.end; } - throw new SyntaxError(msg, filename, start, end); + Attribute.Origin context = (Attribute.Origin) elem + .attribute(Attribute.Origin.class); + if(context != null) { + throw new SyntaxError(msg, filename, start, end, context); + } else { + throw new SyntaxError(msg, filename, start, end); + } } public static void syntaxError(String msg, String filename, @@ -249,8 +268,13 @@ public static void syntaxError(String msg, String filename, start = attr.start; end = attr.end; } - - throw new SyntaxError(msg, filename, start, end, ex); + Attribute.Origin context = (Attribute.Origin) elem + .attribute(Attribute.Origin.class); + if(context != null) { + throw new SyntaxError(msg, filename, start, end, ex, context); + } else { + throw new SyntaxError(msg, filename, start, end, ex); + } } /** diff --git a/modules/wyc/src/wyc/testing/AllInvalidTests.java b/modules/wyc/src/wyc/testing/AllInvalidTests.java index 6d1850efd9..300a0c34aa 100755 --- a/modules/wyc/src/wyc/testing/AllInvalidTests.java +++ b/modules/wyc/src/wyc/testing/AllInvalidTests.java @@ -117,9 +117,9 @@ protected void runTest(String name) { // contains the sample output for this test String sampleOutputFile = WHILEY_SRC_DIR + File.separatorChar + name + ".sysout"; - + // Third, compare the output! - TestUtils.compare(output,sampleOutputFile); + TestUtils.compare(output,sampleOutputFile); } } diff --git a/modules/wycc/src/wycc/lang/Wyil2CBuilder.java b/modules/wycc/src/wycc/lang/Wyil2CBuilder.java index 3ee2c10343..d66ea947a9 100644 --- a/modules/wycc/src/wycc/lang/Wyil2CBuilder.java +++ b/modules/wycc/src/wycc/lang/Wyil2CBuilder.java @@ -943,8 +943,8 @@ public void checkCase(Case casIn, int idx) { int cnt = -1; List attCol = casIn.attributes(); //Block bod = casIn.body(); - Code.Block prec = casIn.precondition(); - Code.Block posc = casIn.postcondition(); + List prec = casIn.precondition(); + List posc = casIn.postcondition(); if (attCol == null) { ans += "// " + " no attributes\n"; @@ -952,13 +952,13 @@ public void checkCase(Case casIn, int idx) { cnt = attCol.size(); ans += "// " + " with " + cnt + " attributes\n"; } - if (prec == null) { + if (prec.isEmpty()) { ans += "// " + " no precondition\n"; } else { cnt = prec.size(); ans += "// " + " precondition of size " + cnt + "\n"; } - if (posc == null) { + if (posc.isEmpty()) { ans += "// " + " no postcondition\n"; } else { cnt = posc.size(); diff --git a/modules/wycs/src/wycs/builders/CodeGeneration.java b/modules/wycs/src/wycs/builders/CodeGeneration.java index 30a2179f11..07681435cf 100644 --- a/modules/wycs/src/wycs/builders/CodeGeneration.java +++ b/modules/wycs/src/wycs/builders/CodeGeneration.java @@ -75,12 +75,12 @@ protected WycsFile.Declaration generate(WyalFile.Macro d) { // Second, generate macro body HashMap environment = new HashMap(); Code parameter = Code.Variable(from, new Code[0], 0, - d.from.attribute(Attribute.Source.class)); + attributes(d.from)); addDeclaredVariables(parameter,d.from,environment); Code condition = generate(d.body, environment, d); // Third, create declaration return new WycsFile.Macro(d.name, type, condition, - d.attribute(Attribute.Source.class)); + attributes(d)); } protected WycsFile.Declaration generate(WyalFile.Function d) { @@ -97,16 +97,16 @@ protected WycsFile.Declaration generate(WyalFile.Function d) { if (d.constraint != null) { HashMap environment = new HashMap(); Code ret = Code.Variable(to, new Code[0], 0, - d.to.attribute(Attribute.Source.class)); + attributes(d.to)); Code parameter = Code.Variable(from, new Code[0], 1, - d.from.attribute(Attribute.Source.class)); + attributes(d.from)); addDeclaredVariables(parameter,d.from,environment); addDeclaredVariables(ret,d.to,environment); condition = generate(d.constraint, environment, d); } // Third, create declaration return new WycsFile.Function(d.name, type, condition, - d.attribute(Attribute.Source.class)); + attributes(d)); } protected void addDeclaredVariables(Code root, TypePattern t, @@ -125,7 +125,7 @@ protected void addDeclaredVariables(Code root, TypePattern t, TypePattern p = tt.elements.get(i); addDeclaredVariables( Code.Load((SemanticType.Tuple) root.type, root, i, - t.attribute(Attribute.Source.class)), p, + attributes(t)), p, environment); } } else if(t instanceof TypePattern.Record) { @@ -139,7 +139,7 @@ protected void addDeclaredVariables(Code root, TypePattern t, protected WycsFile.Declaration generate(WyalFile.Assert d) { Code condition = generate(d.expr, new HashMap(),d); - return new WycsFile.Assert(d.message, condition, d.attribute(Attribute.Source.class)); + return new WycsFile.Assert(d.message, condition, attributes(d)); } protected Code generate(Expr e, HashMap environment, WyalFile.Context context) { @@ -175,7 +175,7 @@ protected Code generate(Expr.Variable e, HashMap environment, WyalF protected Code generate(Expr.Constant v, HashMap environment, WyalFile.Context context) { return Code.Constant(v.value, - v.attribute(Attribute.Source.class)); + attributes(v)); } protected Code generate(Expr.Unary e, HashMap environment, WyalFile.Context context) { @@ -198,7 +198,7 @@ protected Code generate(Expr.Unary e, HashMap environment, WyalFile return null; } return Code.Unary(type, opcode, operand, - e.attribute(Attribute.Source.class)); + attributes(e)); } protected Code generate(Expr.Binary e, HashMap environment, WyalFile.Context context) { @@ -209,10 +209,10 @@ protected Code generate(Expr.Binary e, HashMap environment, WyalFil switch(e.op) { case AND: return Code.Nary(type, Code.Op.AND, new Code[] { lhs, rhs }, - e.attribute(Attribute.Source.class)); + attributes(e)); case OR: return Code.Nary(type, Code.Op.OR, new Code[] { lhs, rhs }, - e.attribute(Attribute.Source.class)); + attributes(e)); case ADD: opcode = Code.Op.ADD; break; @@ -237,14 +237,14 @@ protected Code generate(Expr.Binary e, HashMap environment, WyalFil case IMPLIES: lhs = Code.Unary(type, Code.Unary.Op.NOT, lhs); return Code.Nary(type, Code.Op.OR, new Code[] { lhs, rhs }, - e.attribute(Attribute.Source.class)); + attributes(e)); case IFF: Code nLhs = Code.Unary(type, Code.Unary.Op.NOT,lhs); Code nRhs = Code.Unary(type, Code.Unary.Op.NOT,rhs); lhs = Code.Nary(type, Code.Op.AND, new Code[]{lhs,rhs}); rhs = Code.Nary(type, Code.Op.AND, new Code[]{nLhs,nRhs}); return Code.Nary(type, Code.Op.OR, new Code[]{lhs,rhs}, - e.attribute(Attribute.Source.class)); + attributes(e)); case LT: opcode = Code.Op.LT; break; @@ -312,7 +312,7 @@ protected Code generate(Expr.Binary e, HashMap environment, WyalFil Code argument = Code.Nary(argType, Code.Op.TUPLE, new Code[] { lhs,rhs }); return Code.FunCall(funType, argument, nid, - e.attribute(Attribute.Source.class)); + attributes(e)); } case LISTAPPEND: { NameID nid = new NameID(WYCS_CORE_LIST,"Append"); @@ -323,7 +323,7 @@ protected Code generate(Expr.Binary e, HashMap environment, WyalFil Code argument = Code.Nary(argType, Code.Op.TUPLE, new Code[] { lhs,rhs }); return Code.FunCall(funType, argument, nid, - e.attribute(Attribute.Source.class)); + attributes(e)); } case RANGE: { NameID nid = new NameID(WYCS_CORE_LIST,"Range"); @@ -333,7 +333,7 @@ protected Code generate(Expr.Binary e, HashMap environment, WyalFil Code argument = Code.Nary(argType, Code.Op.TUPLE, new Code[] { lhs,rhs }); return Code.FunCall(funType, argument, nid, - e.attribute(Attribute.Source.class)); + attributes(e)); } default: internalFailure("unknown binary opcode encountered (" + e + ")", @@ -342,7 +342,7 @@ protected Code generate(Expr.Binary e, HashMap environment, WyalFil } return Code.Binary(type, opcode, lhs, rhs, - e.attribute(Attribute.Source.class)); + attributes(e)); } @@ -375,7 +375,7 @@ protected Code generate(Expr.Ternary e, HashMap environment, SemanticType.Function funType = SemanticType.Function(argType, type, generics); return Code.FunCall(funType, argument, nid, - e.attribute(Attribute.Source.class)); + attributes(e)); } protected Code generate(Expr.Nary e, HashMap environment, WyalFile.Context context) { @@ -417,7 +417,7 @@ protected Code generate(Expr.Nary e, HashMap environment, WyalFile. return null; } return Code.Nary(type, opcode, operands, - e.attribute(Attribute.Source.class)); + attributes(e)); } protected Code generate(Expr.Quantifier e, @@ -435,10 +435,10 @@ protected Code generate(Expr.Quantifier e, if(e instanceof Expr.ForAll) { return Code.Quantifier(type, Code.Op.FORALL, operand, types, - e.attribute(Attribute.Source.class)); + attributes(e)); } else { return Code.Quantifier(type, Code.Op.EXISTS, operand, types, - e.attribute(Attribute.Source.class)); + attributes(e)); } } @@ -469,7 +469,7 @@ protected void addQuantifiedVariables(TypePattern t, environment.put( tl.var.name, Code.Variable(type, index, - tl.attribute(Attribute.Source.class))); + attributes(tl))); } } else if(t instanceof TypePattern.Tuple) { TypePattern.Tuple tt = (TypePattern.Tuple) t; @@ -490,7 +490,7 @@ protected Code generate(Expr.Invoke e, HashMap environment, Pair p = builder .resolveAsFunctionType(e.name, context); return Code.FunCall(type, operand, p.first(), - e.attribute(Attribute.Source.class)); + attributes(e)); } catch (ResolveError re) { // should be unreachable if type propagation is already succeeded. syntaxError("cannot resolve as function or definition call", @@ -507,7 +507,7 @@ protected Code generate(Expr.IndexOf e, HashMap environment, WyalFi SemanticType.EffectiveTuple tt = (SemanticType.EffectiveTuple) operand_type; Value.Integer idx = (Value.Integer) ((Expr.Constant) e.index).value; return Code.Load(tt.tupleType(), source, idx.value.intValue(), - e.attribute(Attribute.Source.class)); + attributes(e)); } else { // FIXME: handle effective set here SemanticType.Set type = (SemanticType.Set) operand_type; @@ -521,7 +521,7 @@ protected Code generate(Expr.IndexOf e, HashMap environment, WyalFi Code argument = Code.Nary(argType, Code.Op.TUPLE, new Code[] { source, index }); return Code.FunCall(funType, argument, nid, - e.attribute(Attribute.Source.class)); + attributes(e)); } } @@ -581,6 +581,16 @@ protected SemanticType[] bindGenerics(NameID nid, SemanticType argumentType, } } + protected static Attribute[] attributes(SyntacticElement d) { + ArrayList attrs = new ArrayList(); + for(Attribute a : d.attributes()) { + if(a instanceof Attribute.Source || a instanceof Attribute.Origin) { + attrs.add(a); + } + } + return attrs.toArray(new Attribute[attrs.size()]); + } + protected static Code implies(Code lhs, Code rhs) { lhs = Code.Unary(SemanticType.Bool, Code.Op.NOT, lhs); return Code diff --git a/modules/wyil/src/wyil/transforms/RuntimeAssertions.java b/modules/wyil/src/wyil/transforms/RuntimeAssertions.java index 62c963e712..07c74b30e2 100644 --- a/modules/wyil/src/wyil/transforms/RuntimeAssertions.java +++ b/modules/wyil/src/wyil/transforms/RuntimeAssertions.java @@ -35,6 +35,7 @@ import wycc.lang.SyntacticElement; import wycc.lang.SyntaxError; import wycc.lang.Transform; +import wycc.util.Pair; import wycc.util.ResolveError; import wyfs.lang.Path; import wyil.*; @@ -236,9 +237,10 @@ public Code.Block transform(Code.Block.Entry entry, int freeSlot, public Code.Block transform(Codes.Invoke code, int freeSlot, SyntacticElement elem) throws Exception { - List precondition = findPrecondition(code.name, code.type(), elem); + Pair> p = findPrecondition(code.name, code.type(), elem); + List precondition = p.second(); - if (precondition.size() > 0) { + if (precondition != null && precondition.size() > 0) { Code.Block blk = new Code.Block(0); List paramTypes = code.type().params(); @@ -251,7 +253,7 @@ public Code.Block transform(Codes.Invoke code, int freeSlot, } for(Code.Block requires : precondition) { - requires = resource(requires, + requires = resource(requires, p.first(), elem.attribute(Attribute.Source.class)); importExternalAssert(blk, requires, binding); @@ -287,7 +289,7 @@ public Code.Block transform(Codes.Return code, int freeSlot, } for (Code.Block postcondition : methodCase.postcondition()) { - Code.Block block = resource(postcondition, + Code.Block block = resource(postcondition,filename, elem.attribute(Attribute.Source.class)); importExternalAssert(nBlock, block, binding); } @@ -429,7 +431,7 @@ public Code.Block transform(Codes.BinaryOperator code, int freeSlot, SyntacticEl return null; } - protected List findPrecondition(NameID name, Type.FunctionOrMethod fun, + protected Pair> findPrecondition(NameID name, Type.FunctionOrMethod fun, SyntacticElement elem) throws Exception { Path.Entry e = builder.project().get(name.module(),WyilFile.ContentType); if(e == null) { @@ -439,15 +441,15 @@ protected List findPrecondition(NameID name, Type.FunctionOrMethod f } WyilFile m = e.read(); WyilFile.FunctionOrMethodDeclaration method = m.functionOrMethod(name.name(),fun); - + for(WyilFile.Case c : method.cases()) { // FIXME: this is a hack for now, since method cases don't do // anything. if(c.precondition() != null) { - return c.precondition(); + return new Pair>(m.filename(),c.precondition()); } } - return Collections.EMPTY_LIST; + return null; } private java.util.List attributes(SyntacticElement elem) { @@ -546,13 +548,19 @@ public void importExternalAssert(Code.Block block, Code.Block external, * @param nsrc * @return */ - public static Code.Block resource(Code.Block block, Attribute.Source nsrc) { + public static Code.Block resource(Code.Block block, String filename, Attribute.Source nsrc) { if (block == null) { return null; } Code.Block nblock = new Code.Block(block.numInputs()); for (Entry e : block) { - nblock.add(e.code, nsrc); + Attribute.Origin context = null; + Attribute.Source src = e.attribute(Attribute.Source.class); + if (src != null) { + context = new Attribute.Origin(filename, src.start, src.end, + src.line); + } + nblock.add(e.code, nsrc, context); } return nblock; } diff --git a/tests/invalid/ConstrainedInt_Invalid_4.sysout b/tests/invalid/ConstrainedInt_Invalid_4.sysout index 4d056d6b99..67846dbe67 100644 --- a/tests/invalid/ConstrainedInt_Invalid_4.sysout +++ b/tests/invalid/ConstrainedInt_Invalid_4.sysout @@ -1,3 +1,7 @@ ../../tests/invalid/ConstrainedInt_Invalid_4.whiley:7: postcondition not satisfied return x ^^^^^^^^ + +../../tests/invalid/ConstrainedInt_Invalid_4.whiley:5: +ensures y != 1: + ^^^^^^ diff --git a/tests/invalid/ConstrainedList_Invalid_2.sysout b/tests/invalid/ConstrainedList_Invalid_2.sysout index cf7d63a3a9..064d3b6d98 100644 --- a/tests/invalid/ConstrainedList_Invalid_2.sysout +++ b/tests/invalid/ConstrainedList_Invalid_2.sysout @@ -1,3 +1,7 @@ ../../tests/invalid/ConstrainedList_Invalid_2.whiley:10: postcondition not satisfied return x ^^^^^^^^ + +../../tests/invalid/ConstrainedList_Invalid_2.whiley:5: +ensures (r > 0) && (r <= 256): + ^^^^^^^^^^^^^^^^^^^^^ diff --git a/tests/invalid/ConstrainedSet_Invalid_2.sysout b/tests/invalid/ConstrainedSet_Invalid_2.sysout index 1734d224fa..452f7a4215 100644 --- a/tests/invalid/ConstrainedSet_Invalid_2.sysout +++ b/tests/invalid/ConstrainedSet_Invalid_2.sysout @@ -1,3 +1,7 @@ ../../tests/invalid/ConstrainedSet_Invalid_2.whiley:10: postcondition not satisfied return x ^^^^^^^^ + +../../tests/invalid/ConstrainedSet_Invalid_2.whiley:5: +ensures (r > 0) && (r <= 256): + ^^^^^^^^^^^^^^^^^^^^^ diff --git a/tests/invalid/Ensures_Invalid_1.sysout b/tests/invalid/Ensures_Invalid_1.sysout index 7f3d353113..b257a8ba80 100644 --- a/tests/invalid/Ensures_Invalid_1.sysout +++ b/tests/invalid/Ensures_Invalid_1.sysout @@ -1,3 +1,7 @@ ../../tests/invalid/Ensures_Invalid_1.whiley:5: postcondition not satisfied return 1 ^^^^^^^^ + +../../tests/invalid/Ensures_Invalid_1.whiley:3: +ensures (2 * r) == 1: + ^^^^^^^^^^^^ diff --git a/tests/invalid/Ensures_Invalid_2.sysout b/tests/invalid/Ensures_Invalid_2.sysout index 585055f98e..da430618e2 100644 --- a/tests/invalid/Ensures_Invalid_2.sysout +++ b/tests/invalid/Ensures_Invalid_2.sysout @@ -1,3 +1,7 @@ ../../tests/invalid/Ensures_Invalid_2.whiley:10: precondition not satisfied f(1) ^^^^ + +../../tests/invalid/Ensures_Invalid_2.whiley:6: +requires x > g(x): + ^^^^^^^^ diff --git a/tests/invalid/Ensures_Invalid_3.sysout b/tests/invalid/Ensures_Invalid_3.sysout index 19f9ef7af6..2b69033620 100644 --- a/tests/invalid/Ensures_Invalid_3.sysout +++ b/tests/invalid/Ensures_Invalid_3.sysout @@ -1,3 +1,7 @@ ../../tests/invalid/Ensures_Invalid_3.whiley:6: postcondition not satisfied return y ^^^^^^^^ + +../../tests/invalid/Ensures_Invalid_3.whiley:4: +ensures x > 0: + ^^^^^ diff --git a/tests/invalid/For_Invalid_7.sysout b/tests/invalid/For_Invalid_7.sysout index bc490d916f..e8e7ac6451 100644 --- a/tests/invalid/For_Invalid_7.sysout +++ b/tests/invalid/For_Invalid_7.sysout @@ -1,3 +1,7 @@ ../../tests/invalid/For_Invalid_7.whiley:10: postcondition not satisfied return r ^^^^^^^^ + +../../tests/invalid/For_Invalid_7.whiley:5: +ensures x > 1: + ^^^^^ diff --git a/tests/invalid/ListEmpty_Invalid_2.sysout b/tests/invalid/ListEmpty_Invalid_2.sysout index b772d13681..80b006a447 100644 --- a/tests/invalid/ListEmpty_Invalid_2.sysout +++ b/tests/invalid/ListEmpty_Invalid_2.sysout @@ -1,3 +1,7 @@ ../../tests/invalid/ListEmpty_Invalid_2.whiley:8: precondition not satisfied f([]) ^^^^^ + +../../tests/invalid/ListEmpty_Invalid_2.whiley:3: +requires xs != []: + ^^^^^^^^ diff --git a/tests/invalid/ListEquals_Invalid_1.sysout b/tests/invalid/ListEquals_Invalid_1.sysout index 00ade7419f..85f2fff168 100644 --- a/tests/invalid/ListEquals_Invalid_1.sysout +++ b/tests/invalid/ListEquals_Invalid_1.sysout @@ -1,3 +1,7 @@ ../../tests/invalid/ListEquals_Invalid_1.whiley:8: precondition not satisfied f([]) ^^^^^ + +../../tests/invalid/ListEquals_Invalid_1.whiley:3: +requires xs != []: + ^^^^^^^^ diff --git a/tests/invalid/ListLength_Invalid_3.sysout b/tests/invalid/ListLength_Invalid_3.sysout index 5073733f13..f4f2ce771c 100644 --- a/tests/invalid/ListLength_Invalid_3.sysout +++ b/tests/invalid/ListLength_Invalid_3.sysout @@ -1,3 +1,7 @@ ../../tests/invalid/ListLength_Invalid_3.whiley:10: precondition not satisfied f(|sys.args| - 1) ^^^^^^^^^^^^^^^^^ + +../../tests/invalid/ListLength_Invalid_3.whiley:3: +requires (x + 1) > 0 + ^^^^^^^^^^^ diff --git a/tests/invalid/Quantifiers_Invalid_1.sysout b/tests/invalid/Quantifiers_Invalid_1.sysout index 4edc8709c1..938ef68237 100644 --- a/tests/invalid/Quantifiers_Invalid_1.sysout +++ b/tests/invalid/Quantifiers_Invalid_1.sysout @@ -1,3 +1,7 @@ ../../tests/invalid/Quantifiers_Invalid_1.whiley:7: precondition not satisfied f({1, 2, 3}) ^^^^^^^^^^^^ + +../../tests/invalid/Quantifiers_Invalid_1.whiley:3: +requires some { i in ls | i < 0 }: + ^^^^^^^^^^^^^^^^^^^^^^^^ diff --git a/tests/invalid/Quantifiers_Invalid_2.sysout b/tests/invalid/Quantifiers_Invalid_2.sysout index 1847f93c9e..18b308d49b 100644 --- a/tests/invalid/Quantifiers_Invalid_2.sysout +++ b/tests/invalid/Quantifiers_Invalid_2.sysout @@ -1,3 +1,7 @@ ../../tests/invalid/Quantifiers_Invalid_2.whiley:7: precondition not satisfied f({0, 1, 2, 3}) ^^^^^^^^^^^^^^^ + +../../tests/invalid/Quantifiers_Invalid_2.whiley:3: +requires no { i in ls | i <= 0 }: + ^^^^^^^^^^^^^^^^^^^^^^^ diff --git a/tests/invalid/Quantifiers_Invalid_3.sysout b/tests/invalid/Quantifiers_Invalid_3.sysout index 4ae9cd933d..dcf8c000d2 100644 --- a/tests/invalid/Quantifiers_Invalid_3.sysout +++ b/tests/invalid/Quantifiers_Invalid_3.sysout @@ -1,3 +1,7 @@ ../../tests/invalid/Quantifiers_Invalid_3.whiley:7: precondition not satisfied f([-1, 0, 1, 2, 3]) ^^^^^^^^^^^^^^^^^^^ + +../../tests/invalid/Quantifiers_Invalid_3.whiley:3: +requires no { i in {0, 1, 2, 3, 4} | (i >= 0) && ((i < |ls|) && (ls[i] < 0)) }: + ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^ diff --git a/tests/invalid/Quantifiers_Invalid_4.sysout b/tests/invalid/Quantifiers_Invalid_4.sysout index bd58925c0c..28c3e21292 100644 --- a/tests/invalid/Quantifiers_Invalid_4.sysout +++ b/tests/invalid/Quantifiers_Invalid_4.sysout @@ -1,3 +1,7 @@ ../../tests/invalid/Quantifiers_Invalid_4.whiley:7: precondition not satisfied f([1, 2, 3]) ^^^^^^^^^^^^ + +../../tests/invalid/Quantifiers_Invalid_4.whiley:3: +requires some { i in {0, 1, 2, 3, 4} | (i >= 0) && ((i < |ls|) && (ls[i] < 0)) }: + ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^ diff --git a/tests/invalid/Quantifiers_Invalid_5.sysout b/tests/invalid/Quantifiers_Invalid_5.sysout index c66c7f1f50..9ff34a95d5 100644 --- a/tests/invalid/Quantifiers_Invalid_5.sysout +++ b/tests/invalid/Quantifiers_Invalid_5.sysout @@ -1,3 +1,7 @@ ../../tests/invalid/Quantifiers_Invalid_5.whiley:7: precondition not satisfied f(ls) ^^^^^ + +../../tests/invalid/Quantifiers_Invalid_5.whiley:3: +requires some { i in ls | i < 0 }: + ^^^^^^^^^^^^^^^^^^^^^^^^ diff --git a/tests/invalid/Quantifiers_Invalid_6.sysout b/tests/invalid/Quantifiers_Invalid_6.sysout index c501667a41..67da530441 100644 --- a/tests/invalid/Quantifiers_Invalid_6.sysout +++ b/tests/invalid/Quantifiers_Invalid_6.sysout @@ -1,3 +1,7 @@ ../../tests/invalid/Quantifiers_Invalid_6.whiley:7: precondition not satisfied f(ls) ^^^^^ + +../../tests/invalid/Quantifiers_Invalid_6.whiley:3: +requires no { i in ls | i <= 0 }: + ^^^^^^^^^^^^^^^^^^^^^^^ diff --git a/tests/invalid/Quantifiers_Invalid_7.sysout b/tests/invalid/Quantifiers_Invalid_7.sysout index 0b1da81fd4..c9dcbbc0c1 100644 --- a/tests/invalid/Quantifiers_Invalid_7.sysout +++ b/tests/invalid/Quantifiers_Invalid_7.sysout @@ -1,3 +1,7 @@ ../../tests/invalid/Quantifiers_Invalid_7.whiley:8: precondition not satisfied f(ls) ^^^^^ + +../../tests/invalid/Quantifiers_Invalid_7.whiley:3: +requires some { i in {0, 1, 2, 3} | (i >= 0) && ((i < |ls|) && (ls[i] < 0)) }: + ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^ diff --git a/tests/invalid/Quantifiers_Invalid_8.sysout b/tests/invalid/Quantifiers_Invalid_8.sysout index dd5a7540a3..edb86f0cb0 100644 --- a/tests/invalid/Quantifiers_Invalid_8.sysout +++ b/tests/invalid/Quantifiers_Invalid_8.sysout @@ -1,3 +1,7 @@ ../../tests/invalid/Quantifiers_Invalid_8.whiley:8: precondition not satisfied f(ls) ^^^^^ + +../../tests/invalid/Quantifiers_Invalid_8.whiley:3: +requires no { i in {-1, 0, 1, 2, 3} | (i >= 0) && ((i < |ls|) && (ls[i] < 0)) }: + ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^ diff --git a/tests/invalid/RealConvert_Invalid_1.sysout b/tests/invalid/RealConvert_Invalid_1.sysout index c0e9b82e9f..62ec6b5357 100644 --- a/tests/invalid/RealConvert_Invalid_1.sysout +++ b/tests/invalid/RealConvert_Invalid_1.sysout @@ -1,3 +1,7 @@ ../../tests/invalid/RealConvert_Invalid_1.whiley:8: precondition not satisfied f(x) ^^^^ + +../../tests/invalid/RealConvert_Invalid_1.whiley:3: +requires x > 0.0: + ^^^^^^^ diff --git a/tests/invalid/RealConvert_Invalid_2.sysout b/tests/invalid/RealConvert_Invalid_2.sysout index 03e606c756..3eed1a31ea 100644 --- a/tests/invalid/RealConvert_Invalid_2.sysout +++ b/tests/invalid/RealConvert_Invalid_2.sysout @@ -1,3 +1,7 @@ ../../tests/invalid/RealConvert_Invalid_2.whiley:7: operand types are not compatible (real vs int) real x = f(1.0, 1) ^^^^^^^^^ + +../../tests/invalid/RealConvert_Invalid_2.whiley:3: +requires x >= (real) y: + ^^^^^^^^^^^^^ diff --git a/tests/invalid/RealDiv_Invalid_2.sysout b/tests/invalid/RealDiv_Invalid_2.sysout index fc71f80b88..6db572bc6b 100644 --- a/tests/invalid/RealDiv_Invalid_2.sysout +++ b/tests/invalid/RealDiv_Invalid_2.sysout @@ -1,3 +1,7 @@ ../../tests/invalid/RealDiv_Invalid_2.whiley:6: postcondition not satisfied return x / 3.0 ^^^^^^^^^^^^^^ + +../../tests/invalid/RealDiv_Invalid_2.whiley:4: +ensures y < 0.16: + ^^^^^^^^ diff --git a/tests/invalid/Requires_Invalid_1.sysout b/tests/invalid/Requires_Invalid_1.sysout index 7798cf72b3..9311ecca44 100644 --- a/tests/invalid/Requires_Invalid_1.sysout +++ b/tests/invalid/Requires_Invalid_1.sysout @@ -1,3 +1,7 @@ ../../tests/invalid/Requires_Invalid_1.whiley:8: precondition not satisfied g(y) ^^^^ + +../../tests/invalid/Requires_Invalid_1.whiley:3: +requires y > 0: + ^^^^^ diff --git a/tests/invalid/SetAssign_Invalid_1.sysout b/tests/invalid/SetAssign_Invalid_1.sysout index 3b82034fed..292616c29b 100644 --- a/tests/invalid/SetAssign_Invalid_1.sysout +++ b/tests/invalid/SetAssign_Invalid_1.sysout @@ -1,3 +1,7 @@ ../../tests/invalid/SetAssign_Invalid_1.whiley:15: precondition not satisfied f(zs) ^^^^^ + +../../tests/invalid/SetAssign_Invalid_1.whiley:3: +requires |xs| > 4: + ^^^^^^^^ diff --git a/tests/invalid/SetComprehension_Invalid_6.sysout b/tests/invalid/SetComprehension_Invalid_6.sysout index 3cbd7ce22e..ffe3341cb7 100644 --- a/tests/invalid/SetComprehension_Invalid_6.sysout +++ b/tests/invalid/SetComprehension_Invalid_6.sysout @@ -1,3 +1,7 @@ ../../tests/invalid/SetComprehension_Invalid_6.whiley:6: postcondition not satisfied return zs ^^^^^^^^^ + +../../tests/invalid/SetComprehension_Invalid_6.whiley:3: +ensures no { z in ys | z < 0 }: + ^^^^^^^^^^^^^^^^^^^^^^ diff --git a/tests/invalid/SetEmpty_Invalid_2.sysout b/tests/invalid/SetEmpty_Invalid_2.sysout index 30cede97d6..5e624b2e33 100644 --- a/tests/invalid/SetEmpty_Invalid_2.sysout +++ b/tests/invalid/SetEmpty_Invalid_2.sysout @@ -1,3 +1,7 @@ ../../tests/invalid/SetEmpty_Invalid_2.whiley:8: precondition not satisfied f({}) ^^^^^ + +../../tests/invalid/SetEmpty_Invalid_2.whiley:3: +requires xs != {}: + ^^^^^^^^ diff --git a/tests/invalid/SetIntersection_Invalid_2.sysout b/tests/invalid/SetIntersection_Invalid_2.sysout index 83b8c5920e..025670cf86 100644 --- a/tests/invalid/SetIntersection_Invalid_2.sysout +++ b/tests/invalid/SetIntersection_Invalid_2.sysout @@ -1,3 +1,7 @@ ../../tests/invalid/SetIntersection_Invalid_2.whiley:7: precondition not satisfied f(ys, zs, ys & zs) ^^^^^^^^^^^^^^^^^^ + +../../tests/invalid/SetIntersection_Invalid_2.whiley:3: +requires zs == (xs & {1, 2, 3}): + ^^^^^^^^^^^^^^^^^^^^^^ diff --git a/tests/invalid/SetSubset_Invalid_1.sysout b/tests/invalid/SetSubset_Invalid_1.sysout index 4cec898242..6d0abd7b67 100644 --- a/tests/invalid/SetSubset_Invalid_1.sysout +++ b/tests/invalid/SetSubset_Invalid_1.sysout @@ -1,3 +1,7 @@ ../../tests/invalid/SetSubset_Invalid_1.whiley:8: precondition not satisfied f({1, 4}, {1, 2, 3}) ^^^^^^^^^^^^^^^^^^^^ + +../../tests/invalid/SetSubset_Invalid_1.whiley:3: +requires xs ⊆ ys: + ^^^^^^^ diff --git a/tests/invalid/SetSubset_Invalid_10.sysout b/tests/invalid/SetSubset_Invalid_10.sysout index 8de6721377..e466aca264 100644 --- a/tests/invalid/SetSubset_Invalid_10.sysout +++ b/tests/invalid/SetSubset_Invalid_10.sysout @@ -1,3 +1,7 @@ ../../tests/invalid/SetSubset_Invalid_10.whiley:7: precondition not satisfied f(xs, ys) ^^^^^^^^^ + +../../tests/invalid/SetSubset_Invalid_10.whiley:3: +requires xs ⊂ ys: + ^^^^^^^ diff --git a/tests/invalid/SetSubset_Invalid_3.sysout b/tests/invalid/SetSubset_Invalid_3.sysout index 7fab10d999..21ab45255c 100644 --- a/tests/invalid/SetSubset_Invalid_3.sysout +++ b/tests/invalid/SetSubset_Invalid_3.sysout @@ -1,3 +1,7 @@ ../../tests/invalid/SetSubset_Invalid_3.whiley:8: precondition not satisfied f({1, 4}, {1, 2, 3}) ^^^^^^^^^^^^^^^^^^^^ + +../../tests/invalid/SetSubset_Invalid_3.whiley:3: +requires xs ⊂ ys: + ^^^^^^^ diff --git a/tests/invalid/SetSubset_Invalid_5.sysout b/tests/invalid/SetSubset_Invalid_5.sysout index 1be13e2357..fbfa0e7f61 100644 --- a/tests/invalid/SetSubset_Invalid_5.sysout +++ b/tests/invalid/SetSubset_Invalid_5.sysout @@ -1,3 +1,7 @@ ../../tests/invalid/SetSubset_Invalid_5.whiley:8: precondition not satisfied f(ys, xs) ^^^^^^^^^ + +../../tests/invalid/SetSubset_Invalid_5.whiley:3: +requires xs ⊆ ys: + ^^^^^^^ diff --git a/tests/invalid/SetSubset_Invalid_6.sysout b/tests/invalid/SetSubset_Invalid_6.sysout index f8d8b24a4d..48e6050df3 100644 --- a/tests/invalid/SetSubset_Invalid_6.sysout +++ b/tests/invalid/SetSubset_Invalid_6.sysout @@ -1,3 +1,7 @@ ../../tests/invalid/SetSubset_Invalid_6.whiley:8: precondition not satisfied f(xs, ys) ^^^^^^^^^ + +../../tests/invalid/SetSubset_Invalid_6.whiley:3: +requires xs ⊂ ys: + ^^^^^^^ diff --git a/tests/invalid/SetSubset_Invalid_7.sysout b/tests/invalid/SetSubset_Invalid_7.sysout index 61d69c8aa8..bf5a5299ee 100644 --- a/tests/invalid/SetSubset_Invalid_7.sysout +++ b/tests/invalid/SetSubset_Invalid_7.sysout @@ -1,3 +1,7 @@ ../../tests/invalid/SetSubset_Invalid_7.whiley:8: precondition not satisfied f(ys, xs) ^^^^^^^^^ + +../../tests/invalid/SetSubset_Invalid_7.whiley:3: +requires xs ⊂ ys: + ^^^^^^^ diff --git a/tests/invalid/SetSubset_Invalid_8.sysout b/tests/invalid/SetSubset_Invalid_8.sysout index 598411d76e..b455adb8ee 100644 --- a/tests/invalid/SetSubset_Invalid_8.sysout +++ b/tests/invalid/SetSubset_Invalid_8.sysout @@ -1,3 +1,7 @@ ../../tests/invalid/SetSubset_Invalid_8.whiley:8: precondition not satisfied f(xs, ys) ^^^^^^^^^ + +../../tests/invalid/SetSubset_Invalid_8.whiley:3: +requires xs ⊂ ys: + ^^^^^^^ diff --git a/tests/invalid/SetSubset_Invalid_9.sysout b/tests/invalid/SetSubset_Invalid_9.sysout index c4124e9536..3d274b739a 100644 --- a/tests/invalid/SetSubset_Invalid_9.sysout +++ b/tests/invalid/SetSubset_Invalid_9.sysout @@ -1,3 +1,7 @@ ../../tests/invalid/SetSubset_Invalid_9.whiley:7: precondition not satisfied f(xs, ys) ^^^^^^^^^ + +../../tests/invalid/SetSubset_Invalid_9.whiley:3: +requires xs ⊂ ys: + ^^^^^^^ diff --git a/tests/invalid/SetUnion_Invalid_3.sysout b/tests/invalid/SetUnion_Invalid_3.sysout index a1b99affe8..3c8b9ebbd6 100644 --- a/tests/invalid/SetUnion_Invalid_3.sysout +++ b/tests/invalid/SetUnion_Invalid_3.sysout @@ -1,3 +1,7 @@ ../../tests/invalid/SetUnion_Invalid_3.whiley:7: precondition not satisfied f(ys + zs) ^^^^^^^^^^ + +../../tests/invalid/SetUnion_Invalid_3.whiley:3: +requires |xs| > 0: + ^^^^^^^^ diff --git a/tests/invalid/SetUnion_Invalid_4.sysout b/tests/invalid/SetUnion_Invalid_4.sysout index 8d7ced22dd..41d72b8985 100644 --- a/tests/invalid/SetUnion_Invalid_4.sysout +++ b/tests/invalid/SetUnion_Invalid_4.sysout @@ -1,3 +1,7 @@ ../../tests/invalid/SetUnion_Invalid_4.whiley:7: precondition not satisfied f(ys, ys, ys + {6}) ^^^^^^^^^^^^^^^^^^^ + +../../tests/invalid/SetUnion_Invalid_4.whiley:3: +requires zs == (xs + ys): + ^^^^^^^^^^^^^^^ diff --git a/tests/invalid/While_Invalid_12.sysout b/tests/invalid/While_Invalid_12.sysout index 264493e59f..648485fe1e 100644 --- a/tests/invalid/While_Invalid_12.sysout +++ b/tests/invalid/While_Invalid_12.sysout @@ -1,3 +1,7 @@ ../../tests/invalid/While_Invalid_12.whiley:14: postcondition not satisfied return i ^^^^^^^^ + +../../tests/invalid/While_Invalid_12.whiley:5: +ensures r >= 0: + ^^^^^^