Merge branch 'develop'

config.xml

@@ -1,4 +1,4 @@
 <project name="BuildConfig">
-  <property name="version" value="0.3.32"/>
+  <property name="version" value="0.3.33"/>
   <property name="JASM_JAR" value="lib/jasm-v0.1.7.jar"/>
 </project>

misc/emacs/whiley.el

@@ -38,7 +38,7 @@ For detail, see `comment-dwim'."
     "Whiley keywords.")
 
 (defvar whiley-types
-  '("real" "int" "bool" "void" "string" "char" "void" "ref")
+  '("real" "int" "bool" "void" "void" "ref")
   "Whiley types.")
 
 (defvar whiley-keywords-regexp (regexp-opt whiley-keywords 'words))

modules/wybs/build.xml

@@ -2,7 +2,7 @@
   <import file="../../config.xml"/>
 
   <target name="compile-wybs">
-    <javac memoryMaximumSize="2048m" fork="true" debug="true" debuglevel="vars,lines,source" source="1.6" includeantruntime="true">
+    <javac memoryMaximumSize="2048m" fork="true" debug="true" debuglevel="vars,lines,source" source="1.7" target="1.7" includeantruntime="true">
       <src path="src"/>
       <include name="*/**"/>
       <exclude name="*/**/package-info.java"/>

modules/wyc/build.xml

@@ -2,7 +2,7 @@
   <import file="../../config.xml"/>
 
   <target name="compile-wyc">
-    <javac debug="true" debuglevel="vars,lines,source" source="1.7" includeantruntime="true" classpath="../wyil/src:../wybs/src/:../wycs/src:../wyrl/src/">
+    <javac debug="true" debuglevel="vars,lines,source" source="1.7" target="1.7" includeantruntime="true" classpath="../wyil/src:../wybs/src/:../wycs/src:../wyrl/src/">
       <src path="src"/>
       <include name="*/**"/>
       <exclude name="*/**/package-info.java"/>

modules/wyc/src/wyc/builder/CodeGenerator.java

@@ -1108,21 +1108,18 @@ private void generate(Stmt.While s, Environment environment,
 		if(s.invariants.size() > 0) {
 			// Ok, there is at least one invariant expression. Therefore, create
 			// an invariant bytecode.
-			AttributedCodeBlock invariant = body.createSubBlock();
-
+
 			for (Expr e : s.invariants) {
 				String nextLab = CodeUtils.freshLabel();
+				AttributedCodeBlock invariant = body.createSubBlock();
 				generateCondition(nextLab, e, environment, invariant, context);
 				invariant.add(Codes.Fail(), attributes(e));
 				invariant.add(Codes.Label(nextLab));
-			}
-			// Terminate invariant block
-			invariant.add(Codes.Return());
-
-			// FIXME: should we be creating multiple invariant bytecodes,
-			// instead of one monolithic one? Yes, as this will give much better
-			// error reporting as well!
-			body.add(Codes.Invariant(invariant.bytecodes()), attributes(s));
+				// Terminate invariant block --- see #480
+				invariant.add(Codes.Return());
+				// Create the invariant block
+				body.add(Codes.Invariant(invariant.bytecodes()), attributes(e));
+			}			
 		}
 
 		generateCondition(exit, invert(s.condition), environment, body, context);
@@ -1197,21 +1194,16 @@ private void generate(Stmt.DoWhile s, Environment environment,
 		if (s.invariants.size() > 0) {
 			// Ok, there is at least one invariant expression. Therefore, create
 			// an invariant bytecode.
-			AttributedCodeBlock invariant = body.createSubBlock();
-
 			for (Expr e : s.invariants) {
 				String nextLab = CodeUtils.freshLabel();
+				AttributedCodeBlock invariant = body.createSubBlock();				
 				generateCondition(nextLab, e, environment, invariant, context);
 				invariant.add(Codes.Fail(), attributes(e));
 				invariant.add(Codes.Label(nextLab));
+				// Terminate invariant block
+				invariant.add(Codes.Return());
+				body.add(Codes.Invariant(invariant.bytecodes()), attributes(e));				
 			}
-			// Terminate invariant block
-			invariant.add(Codes.Return());
-
-			// FIXME: should we be creating multiple invariant bytecodes,
-			// instead of one monolithic one?
-
-			body.add(Codes.Invariant(invariant.bytecodes()), attributes(s));
 		}
 
 		generateCondition(exit, invert(s.condition), environment, body, context);
@@ -1258,11 +1250,8 @@ private void generate(Stmt.ForAll s, Environment environment,
 			invariant.add(Codes.Label(nextLab));
 			// Terminate invariant block
 			invariant.add(Codes.Return());
-
-			// FIXME: should we be creating multiple invariant bytecodes,
-			// instead of one monolithic one?
-
-			body.add(Codes.Invariant(invariant.bytecodes()), attributes(s));
+			body.add(Codes.Invariant(invariant.bytecodes()),
+					attributes(s.invariant));
 		}
 
 		// FIXME: add a continue scope
@@ -1736,9 +1725,6 @@ public int generate(Expr expression, Environment environment,
 			} else if (expression instanceof Expr.SubList) {
 				return generate((Expr.SubList) expression, environment, codes,
 						context);
-			} else if (expression instanceof Expr.SubString) {
-				return generate((Expr.SubString) expression, environment,
-						codes, context);
 			} else if (expression instanceof Expr.BinOp) {
 				return generate((Expr.BinOp) expression, environment, codes,
 						context);
@@ -1977,8 +1963,9 @@ private int generate(Expr.LocalVariable expr, Environment environment,
 			AttributedCodeBlock codes, Context context) throws ResolveError {
 
 		if (environment.get(expr.var) != null) {
+			int target = environment.get(expr.var); 
 			Type type = expr.result().raw();
-			return environment.get(expr.var);
+			return target;
 		} else {
 			syntaxError(errorMessage(VARIABLE_POSSIBLY_UNITIALISED), context,
 					expr);
@@ -2111,30 +2098,7 @@ private int generate(Expr.BinOp v, Environment environment,
 				codes.add(Codes.ListOperator((Type.EffectiveList) result,
 						target, leftOperand, rightOperand,
 						Codes.ListOperatorKind.APPEND), attributes(v));
-				break;
-
-			case STRINGAPPEND:
-				Type lhs = v.lhs.result().raw();
-				Type rhs = v.rhs.result().raw();
-				Codes.StringOperatorKind op;
-				if (lhs == Type.T_STRING && rhs == Type.T_STRING) {
-					op = Codes.StringOperatorKind.APPEND;
-				} else if (lhs == Type.T_STRING
-						&& Type.isSubtype(Type.T_CHAR, rhs)) {
-					op = Codes.StringOperatorKind.LEFT_APPEND;
-				} else if (rhs == Type.T_STRING
-						&& Type.isSubtype(Type.T_CHAR, lhs)) {
-					op = Codes.StringOperatorKind.RIGHT_APPEND;
-				} else {
-					// this indicates that one operand must be explicitly
-					// converted
-					// into a string.
-					op = Codes.StringOperatorKind.APPEND;
-				}
-				codes.add(Codes.StringOperator(target, leftOperand,
-						rightOperand, op), attributes(v));
-				break;
-
+				break;			
 			default:
 				codes.add(Codes.BinaryOperator(result, target, leftOperand,
 						rightOperand, OP2BOP(bop, v, context)), attributes(v));
@@ -2173,18 +2137,6 @@ private int generate(Expr.SubList expr, Environment environment,
 		return target;
 	}
 
-	private int generate(Expr.SubString v, Environment environment,
-			AttributedCodeBlock codes, Context context) {
-		int srcOperand = generate(v.src, environment, codes, context);
-		int startOperand = generate(v.start, environment, codes, context);
-		int endOperand = generate(v.end, environment, codes, context);
-		int target = environment.allocate(v.result().raw());
-		codes.add(
-				Codes.SubString(target, srcOperand, startOperand, endOperand),
-				attributes(v));
-		return target;
-	}
-
 	private int generate(Expr.Quantifier e, Environment environment,
 			AttributedCodeBlock codes, Context context) {
 		String trueLabel = CodeUtils.freshLabel();

modules/wyc/src/wyc/builder/FlowTypeChecker.java

@@ -628,7 +628,7 @@ private Environment propagate(Stmt.Break stmt, Environment environment) {
 	 */
 	private Environment propagate(Stmt.Debug stmt, Environment environment) {
 		stmt.expr = propagate(stmt.expr, environment, current);
-		checkIsSubtype(Type.T_STRING, stmt.expr);
+		checkIsSubtype(Type.List(Type.T_INT,false), stmt.expr);
 		return environment;
 	}
 
@@ -1557,10 +1557,8 @@ private Pair<Expr, Environment> resolveLeafCondition(Expr.BinOp bop,
 		case LTEQ:
 		case GTEQ:
 		case GT:
-			checkSuptypes(lhs, context, Nominal.T_INT, Nominal.T_REAL,
-					Nominal.T_CHAR);
-			checkSuptypes(rhs, context, Nominal.T_INT, Nominal.T_REAL,
-					Nominal.T_CHAR);
+			checkSuptypes(lhs, context, Nominal.T_INT, Nominal.T_REAL);
+			checkSuptypes(rhs, context, Nominal.T_INT, Nominal.T_REAL);
 			//
 			if (!lhsRawType.equals(rhsRawType)) {
 				syntaxError(
@@ -1680,8 +1678,6 @@ public Expr propagate(Expr expr, Environment environment, Context context) {
 				return propagate((Expr.Set) expr, environment, context);
 			} else if (expr instanceof Expr.SubList) {
 				return propagate((Expr.SubList) expr, environment, context);
-			} else if (expr instanceof Expr.SubString) {
-				return propagate((Expr.SubString) expr, environment, context);
 			} else if (expr instanceof Expr.Dereference) {
 				return propagate((Expr.Dereference) expr, environment, context);
 			} else if (expr instanceof Expr.Record) {
@@ -1743,29 +1739,10 @@ private Expr propagate(Expr.BinOp expr, Environment environment,
 		boolean rhs_set = Type.isSubtype(Type.T_SET_ANY, rhsRawType);
 		boolean lhs_list = Type.isSubtype(Type.T_LIST_ANY, lhsRawType);
 		boolean rhs_list = Type.isSubtype(Type.T_LIST_ANY, rhsRawType);
-		boolean lhs_str = Type.isSubtype(Type.T_STRING, lhsRawType);
-		boolean rhs_str = Type.isSubtype(Type.T_STRING, rhsRawType);
 
 		Type srcType;
 
-		if (lhs_str || rhs_str) {
-			if (!lhs_str) {
-				checkIsSubtype(Type.T_CHAR, lhs, context);
-			} else if (!rhs_str) {
-				checkIsSubtype(Type.T_CHAR, rhs, context);
-			}
-			switch (expr.op) {
-			case LISTAPPEND:
-				expr.op = Expr.BOp.STRINGAPPEND;
-			case STRINGAPPEND:
-				break;
-			default:
-				syntaxError("Invalid string operation: " + expr.op, context,
-						expr);
-			}
-
-			srcType = Type.T_STRING;
-		} else if (lhs_list || rhs_list) {
+		if (lhs_list || rhs_list) {
 			checkIsSubtype(Type.T_LIST_ANY, lhs, context);
 			checkIsSubtype(Type.T_LIST_ANY, rhs, context);
 			Type.EffectiveList lel = (Type.EffectiveList) lhsRawType;
@@ -1862,10 +1839,8 @@ private Expr propagate(Expr.BinOp expr, Environment environment,
 				break;
 			default:
 				// all other operations go through here
-				checkSuptypes(lhs, context, Nominal.T_INT, Nominal.T_REAL,
-						Nominal.T_CHAR);
-				checkSuptypes(rhs, context, Nominal.T_INT, Nominal.T_REAL,
-						Nominal.T_CHAR);
+				checkSuptypes(lhs, context, Nominal.T_INT, Nominal.T_REAL);
+				checkSuptypes(rhs, context, Nominal.T_INT, Nominal.T_REAL);
 				//
 				if (!lhsRawType.equals(rhsRawType)) {
 					syntaxError(
@@ -2139,26 +2114,18 @@ private Expr propagate(Expr.IndexOf expr, Environment environment,
 	private Expr propagate(Expr.LengthOf expr, Environment environment,
 			Context context) throws IOException, ResolveError {
 		expr.src = propagate(expr.src, environment, context);
-		Nominal srcType = expr.src.result();
-		Type rawSrcType = srcType.raw();
 
-		// First, check whether this is still only an abstract access and, in
-		// such case, upgrade it to the appropriate access expression.
+		Nominal.EffectiveCollection srcType = expandAsEffectiveCollection(expr.src
+				.result());
 
-		if (rawSrcType instanceof Type.EffectiveCollection) {
-			expr.srcType = expandAsEffectiveCollection(srcType);
-			return expr;
-		} else {
+		if (srcType == null) {
 			syntaxError("found " + expr.src.result().nominal()
 					+ ", expected string, set, list or dictionary.", context,
 					expr.src);
+		} else {
+			expr.srcType = srcType;
 		}
 
-		// Second, determine the expanded src type for this access expression
-		// and check the key value.
-
-		checkIsSubtype(Type.T_STRING, expr.src, context);
-
 		return expr;
 	}
 
@@ -2269,31 +2236,12 @@ private Expr propagate(Expr.SubList expr, Environment environment,
 		expr.start = propagate(expr.start, environment, context);
 		expr.end = propagate(expr.end, environment, context);
 
-		checkSuptypes(expr.src, context, Nominal.T_LIST_ANY, Nominal.T_STRING);
+		checkSuptypes(expr.src, context, Nominal.T_LIST_ANY);
 		checkIsSubtype(Type.T_INT, expr.start, context);
 		checkIsSubtype(Type.T_INT, expr.end, context);
 
 		expr.type = expandAsEffectiveList(expr.src.result());
-		if (expr.type == null) {
-			// must be a substring
-			return new Expr.SubString(expr.src, expr.start, expr.end,
-					expr.attributes());
-		}
-
-		return expr;
-	}
-
-	private Expr propagate(Expr.SubString expr, Environment environment,
-			Context context) throws IOException {
-
-		expr.src = propagate(expr.src, environment, context);
-		expr.start = propagate(expr.start, environment, context);
-		expr.end = propagate(expr.end, environment, context);
-
-		checkIsSubtype(Type.T_STRING, expr.src, context);
-		checkIsSubtype(Type.T_INT, expr.start, context);
-		checkIsSubtype(Type.T_INT, expr.end, context);
-
+
 		return expr;
 	}
 
@@ -2668,8 +2616,7 @@ private Pair<NameID, Nominal.FunctionOrMethod> selectCandidateFunctionOrMethod(
 							WhileyFile.FunctionOrMethod.class,
 							candidateID.name())) {
 						if (d.parameters.equals(candidateType.params())) {
-							if (!d.hasModifier(Modifier.PUBLIC)
-									&& !d.hasModifier(Modifier.PROTECTED)) {
+							if (!d.hasModifier(Modifier.PUBLIC)) {
 								String msg = candidateID.module() + "." + name
 										+ parameterString(parameters)
 										+ " is not visible";
@@ -2682,8 +2629,7 @@ private Pair<NameID, Nominal.FunctionOrMethod> selectCandidateFunctionOrMethod(
 				WyilFile m = builder.getModule(candidateID.module());
 				WyilFile.FunctionOrMethod d = m.functionOrMethod(
 						candidateID.name(), candidateType.nominal());
-				if (!d.hasModifier(Modifier.PUBLIC)
-						&& !d.hasModifier(Modifier.PROTECTED)) {
+				if (!d.hasModifier(Modifier.PUBLIC)) {
 					String msg = candidateID.module() + "." + name
 							+ parameterString(parameters) + " is not visible";
 					throw new ResolveError(msg);
@@ -3040,14 +2986,10 @@ private Type resolveAsType(SyntacticType t, Context context,
 				return Type.T_BOOL;
 			} else if (t instanceof SyntacticType.Byte) {
 				return Type.T_BYTE;
-			} else if (t instanceof SyntacticType.Char) {
-				return Type.T_CHAR;
 			} else if (t instanceof SyntacticType.Int) {
 				return Type.T_INT;
 			} else if (t instanceof SyntacticType.Real) {
 				return Type.T_REAL;
-			} else if (t instanceof SyntacticType.Strung) {
-				return Type.T_STRING;
 			} else {
 				internalFailure("unrecognised type encountered ("
 						+ t.getClass().getName() + ")", context, t);
@@ -3308,14 +3250,10 @@ private int resolveAsType(SyntacticType.Primitive t, Context context,
 			kind = Type.K_BOOL;
 		} else if (t instanceof SyntacticType.Byte) {
 			kind = Type.K_BYTE;
-		} else if (t instanceof SyntacticType.Char) {
-			kind = Type.K_CHAR;
 		} else if (t instanceof SyntacticType.Int) {
 			kind = Type.K_INT;
 		} else if (t instanceof SyntacticType.Real) {
 			kind = Type.K_RATIONAL;
-		} else if (t instanceof SyntacticType.Strung) {
-			kind = Type.K_STRING;
 		} else {
 			internalFailure("unrecognised type encountered ("
 					+ t.getClass().getName() + ")", context, t);
@@ -3585,8 +3523,7 @@ public boolean isNameVisible(NameID nid, Context context)
 		if (nid.module().equals(context.file().module)) {
 			return true;
 		} else {
-			return hasModifier(nid, context, Modifier.PUBLIC)
-					|| hasModifier(nid, context, Modifier.PROTECTED);
+			return hasModifier(nid, context, Modifier.PUBLIC);
 		}
 	}