Merge branch '138-static'

src/main/java/wyboogie/tasks/BoogieBuildTask.java

@@ -177,6 +177,7 @@ public boolean verify(BoogieFile target) {
 					break;
 				}
 				default: {
+					System.out.println("GOT: " + err.toString());
 					// Fall back
 					throw new Syntactic.Exception(err.toString(), wyItem.getHeap(), wyItem);
 				}

src/main/java/wyboogie/tasks/BoogieCompiler.java

@@ -13,6 +13,7 @@
 // limitations under the License.
 package wyboogie.tasks;
 
+import java.lang.reflect.Modifier;
 import java.math.BigInteger;
 import java.util.*;
 import java.util.function.Function;
@@ -27,6 +28,7 @@
 import wyboogie.core.BoogieFile.Decl;
 import wyboogie.core.BoogieFile.Expr;
 import wyboogie.core.BoogieFile.Stmt;
+import wyboogie.core.BoogieFile.Decl.Variable;
 import wyboogie.core.BoogieFile.LVal;
 
 import wyboogie.util.*;
@@ -178,13 +180,19 @@ public Decl constructStaticVariable(WyilFile.Decl.StaticVariable d, Expr initial
         // Apply name mangling
         String name = toMangledName(d);
         // Final static variables declared as constants with corresponding axiom
-        decls.add(new Decl.Constant(name, type));
+        if(isFinal(d)) {
+        	decls.add(new Decl.Constant(name, type));
+        } else {
+        	decls.add(new Decl.Variable(name, type));
+        }
         if (initialiser != null) {
             Expr rhs = cast(d.getType(), d.getInitialiser().getType(), initialiser);
-            decls.add(new Decl.Axiom(EQ(VAR(name), rhs)));
-            // Add type invariant guarantee
-            decls.add(new Decl.Axiom(IMPLIES(GT(VAR("Context#Level"), CONST(1)), constructTypeTest(d.getType(), VAR(name), EMPTY_HEAPVAR, d))));
-            decls.addAll(constructStaticVariableCheck(d));
+            if(isFinal(d)) {
+                decls.add(new Decl.Axiom(EQ(VAR(name), rhs)));
+                // Add type invariant guarantee
+                decls.add(new Decl.Axiom(IMPLIES(GT(VAR("Context#Level"), CONST(1)), constructTypeTest(d.getType(), VAR(name), EMPTY_HEAPVAR, d))));
+            }
+            decls.addAll(constructStaticVariableCheck(d,initialiser));
             // Add any lambda's used within the function
             decls.addAll(constructLambdas(d));
         }
@@ -197,14 +205,16 @@ public Decl constructStaticVariable(WyilFile.Decl.StaticVariable d, Expr initial
      * @param d
      * @return
      */
-    private List<Decl> constructStaticVariableCheck(WyilFile.Decl.StaticVariable d) {
+    private List<Decl> constructStaticVariableCheck(WyilFile.Decl.StaticVariable d, Expr initialiser) {
         ArrayList<Decl> decls = new ArrayList<>();
         // Apply name mangling
         String name = toMangledName(d);
         // Construct precondition to prevents axiom firing trivially
         List<Expr.Logical> precondition = Arrays.asList(EQ(VAR("Context#Level"),CONST(1)));
         // Construct simple assertion for the body
-        Stmt body = SEQUENCE(ASSERT(constructTypeTest(d.getType(), VAR(name), EMPTY_HEAPVAR, d), ATTRIBUTE(d.getInitialiser()), ATTRIBUTE(WyilFile.STATIC_TYPEINVARIANT_FAILURE)));
+		Stmt body = SEQUENCE(
+				ASSERT(constructTypeTest(d.getType(), d.getInitialiser().getType(), initialiser, EMPTY_HEAPVAR, d),
+						ATTRIBUTE(d.getInitialiser()), ATTRIBUTE(WyilFile.STATIC_TYPEINVARIANT_FAILURE)));
         // Construct the checking method method
         decls.add(new Decl.Procedure(name + "#check", Collections.EMPTY_LIST, Collections.EMPTY_LIST, precondition, Collections.EMPTY_LIST, Collections.EMPTY_LIST, Collections.EMPTY_LIST, body));
         // Done
@@ -320,10 +330,17 @@ public List<Decl> constructProcedurePrototype(WyilFile.Decl.FunctionOrMethod d,
         requires.add(GT(VAR("Context#Level"), CONST(1)));
         // Apply method-specific stuff
         if(d instanceof WyilFile.Decl.Method) {
+        	WyilFile.Decl.Method md = (WyilFile.Decl.Method) d;
             // Add type invariant preservation guarantee
-            freeEnsures.addAll(constructMethodFrame((WyilFile.Decl.Method) d));
+            freeEnsures.addAll(constructMethodFrame(md));
             // Methods always modify the heap
-            modifies = Arrays.asList("HEAP");
+            modifies = new ArrayList<>();
+            modifies.add("HEAP");
+            for(WyilFile.Decl.StaticVariable v : extractModifiedVariables(md)) {
+            	String vName = toMangledName(v);
+            	modifies.add(vName);
+				freeRequires.add(constructTypeTest(v.getType(), VAR(vName), HEAP, d));
+            }
         } else {
             ArrayList<Decl.Parameter> f_params = new ArrayList<>(params);
             f_params.add(0,HEAP_PARAM);
@@ -425,6 +442,44 @@ private List<Decl> constructLambdaAxioms(String name, WyilFile.Type param, WyilF
         return decls;
     }
 
+	/**
+	 * Determine the approach list of modified variables for this method.
+	 *
+	 * @param md
+	 * @return
+	 */
+	public List<WyilFile.Decl.StaticVariable> extractModifiedVariables(WyilFile.Decl.Method md) {
+		// TODO: at this stage, Whiley doesn't have syntax for modified variabies.
+		// Therefore, assume all variables are modified.
+		ArrayList<WyilFile.Decl.StaticVariable> vars = new ArrayList<>();
+		// Search for all known global variables.
+		WyilFile wf = (WyilFile) md.getHeap();
+		WyilFile.Decl.Module mod = wf.getModule();
+		// Now, public external vars
+		for(WyilFile.Decl.Unit u : mod.getUnits()) {
+			for(WyilFile.Decl d : u.getDeclarations()) {
+				if(d instanceof WyilFile.Decl.StaticVariable) {
+					WyilFile.Decl.StaticVariable v = (WyilFile.Decl.StaticVariable) d;
+					if (!isFinal(v)) {
+						vars.add(v);
+					}
+				}
+			}
+		}
+		// Now, public external vars
+		for(WyilFile.Decl.Unit u : mod.getExterns()) {
+			for(WyilFile.Decl d : u.getDeclarations()) {
+				if(d instanceof WyilFile.Decl.StaticVariable) {
+					WyilFile.Decl.StaticVariable v = (WyilFile.Decl.StaticVariable) d;
+					if (!isFinal(v) && isPublic(v)) {
+						vars.add(v);
+					}
+				}
+			}
+		}
+		return vars;
+	}
+
     /**
      * Convert a sequence of Wyil parameter declarations into a sequence of Boogie parameter declarations. This requires
      * converting the Wyil type to its corresponding Boogie type.
@@ -855,7 +910,8 @@ public Stmt constructAssign(WyilFile.Stmt.Assign stmt, List _lhs, List _rhs) {
             // Extract the assigned variable
             WyilFile.Decl.Variable v = extractVariable(ith);
             // Apply type constraint (if applicable)
-            Expr.Logical c = constructTypeConstraint(v.getType(), VAR(toVariableName(v)), HEAP, ith);
+            String name = (v instanceof WyilFile.Decl.StaticVariable) ? toMangledName(v) : toVariableName(v);
+            Expr.Logical c = constructTypeConstraint(v.getType(), VAR(name), HEAP, ith);
             if (c != null) {
                 stmts.add(ASSERT(c, ATTRIBUTE(rvals.get(i)), ATTRIBUTE(WyilFile.STATIC_TYPEINVARIANT_FAILURE)));
             }
@@ -1021,10 +1077,17 @@ private Stmt constructAssign(WyilFile.LVal lval, Expr lhs, Expr rhs) {
                 return ASSIGN(HEAP, PUT(HEAP, src, rhs));
             }
             case WyilFile.EXPR_variablecopy:
-            case WyilFile.EXPR_variablemove: {
+            case WyilFile.EXPR_variablemove:{
                 WyilFile.Expr.VariableAccess expr = (WyilFile.Expr.VariableAccess) lval;
                 WyilFile.Decl.Variable decl = expr.getVariableDeclaration();
-                String name = toVariableName(expr.getVariableDeclaration());
+                String name = toVariableName(decl);
+                // NOTE: the manner in which the following cast is applied seems odd to me, and is an artifact of how WyC is currently typing assignments.
+                return ASSIGN(VAR(name), cast(decl.getType(), expr.getType(), rhs));
+            }
+            case WyilFile.EXPR_staticvariable: {
+                WyilFile.Expr.StaticVariableAccess expr = (WyilFile.Expr.StaticVariableAccess) lval;
+                WyilFile.Decl.StaticVariable decl = expr.getLink().getTarget();
+                String name = toMangledName(expr.getLink().getTarget());
                 // NOTE: the manner in which the following cast is applied seems odd to me, and is an artifact of how WyC is currently typing assignments.
                 return ASSIGN(VAR(name), cast(decl.getType(), expr.getType(), rhs));
             }
@@ -1505,7 +1568,10 @@ public Expr constructVariableAccessLVal(WyilFile.Expr.VariableAccess expr) {
 
 	@Override
 	public Expr constructStaticVariableAccessLVal(StaticVariableAccess expr) {
-		throw new Syntactic.Exception("implement me", expr.getHeap(), expr);
+		 // Determine mangled name of this variable
+		String name = toMangledName(expr.getLink().getTarget());
+        //
+        return VAR(name, ATTRIBUTE(expr));
 	}
 
     @Override
@@ -3263,7 +3329,7 @@ private Expr.Logical constructRecordTypeTest(WyilFile.Type.Record to, WyilFile.T
         // Combine indivudal cases
         Expr.Logical test = AND(inclauses, ATTRIBUTE(item));
         // Construct type test (when necessary)
-        Expr.Logical inbound = argument != nArgument ? AND(INVOKE("Record#is", argument), test, ATTRIBUTE(item)) : test;
+		Expr.Logical inbound = argument != nArgument ? AND(INVOKE("Record#is", argument), test, ATTRIBUTE(item)) : test;
         Expr.Logical outbound = FORALL(v.getVariable(), FIELD, IMPLIES(AND(outclauses), EQ(GET(nArgument, v), VOID)));
         // Finally, apply outbounds to closed records only since these are the ones whose fields we actually know about.
         return to.isOpen() ?  inbound : AND(inbound, outbound, ATTRIBUTE(item));
@@ -3870,7 +3936,7 @@ private String getMangle(WyilFile.Type type) {
     }
 
     private String toVariableName(WyilFile.Decl.Variable v) {
-        if (mangling) {
+    	if (mangling) {
             return v.getName().get() + "$" + v.getIndex();
         } else {
             return v.getName().get();
@@ -3975,6 +4041,16 @@ public static boolean isFinal(WyilFile.Decl.Variable var) {
         return var.getModifiers().match(WyilFile.Modifier.Final.class) != null;
     }
 
+    /**
+     * Check whether a given variable is marked as public or not.
+     *
+     * @param var
+     * @return
+     */
+    public static boolean isPublic(WyilFile.Decl.Variable var) {
+        return var.getModifiers().match(WyilFile.Modifier.Public.class) != null;
+    }
+
     /**
      * Check whether a given method declaration ends in a return statement or not. If it doesn't then we need to insert
      * a final assignment of the heap variable
@@ -4085,6 +4161,10 @@ private static WyilFile.Decl.Variable extractVariable(WyilFile.LVal lval) {
                 WyilFile.Expr.VariableAccess e = (WyilFile.Expr.VariableAccess) lval;
                 return e.getVariableDeclaration();
             }
+            case WyilFile.EXPR_staticvariable: {
+                WyilFile.Expr.StaticVariableAccess e = (WyilFile.Expr.StaticVariableAccess) lval;
+                return e.getLink().getTarget();
+            }
             default:
                 throw new IllegalArgumentException("invalid lval: " + lval);
         }

src/main/java/wyboogie/util/testing/BoogieVerifyTest.java

@@ -86,6 +86,7 @@ public Result apply(Trie path, Path dir, Map<Trie, TextFile> state, TestFile tf)
 			//
 			return new TestStage.Result(ignored, markers);
 		} catch (Syntactic.Exception e) {
+			e.printStackTrace();
 			if(e.getElement() != null) {
 				TestFile.Error err = WhileyCompileTest.toError(state,e);
 				return new TestStage.Result(ignored,new TestFile.Error[] {err});

src/test/java/wyboogie/WhileyCompilerTests.java

@@ -80,7 +80,7 @@ public enum Error {
 
 	@ParameterizedTest
 	@MethodSource("sourceFiles")
- 	public void test(Trie path) throws IOException {
+ 	public void mainTests(Trie path) throws IOException {
 		TestManager.Result r = manager.run(path);
 		//
 		if(r == Result.IGNORED) {
@@ -103,16 +103,17 @@ private static Stream<Trie> sourceFiles() throws IOException {
 
 	@ParameterizedTest
 	@MethodSource("debugFiles")
-	public void debugTest(Trie path) throws IOException {
+	public void debugTests(Trie path) throws IOException {
 		// Enable debugging
 		manager.setDebug(true);
 		// Run the test
-		test(path);
+		mainTests(path);
 	}
 
 	// Here we enumerate all available test cases.
 	private static Stream<Trie> debugFiles() throws IOException {
-		return readTestFiles(WHILEY_SRC_DIR, atleast(999999));
+		return readTestFiles(WHILEY_SRC_DIR, in(190,1163,1164,1418));
+//		return readTestFiles(WHILEY_SRC_DIR, atleast(99999));
 	}
 
 	// ======================================================================
@@ -134,6 +135,22 @@ public static Stream<Trie> readTestFiles(java.nio.file.Path dir, Predicate<Strin
 		return testcases.stream();
 	}
 
+	private static Predicate<String> in(int... tests) {
+		return n -> {
+			int t = Integer.parseInt(n.replace(".test", ""));
+			for(int i=0;i!=tests.length;++i) {
+				if(t == tests[i]) {
+					return true;
+				}
+			}
+			return false;
+		};
+	}
+
+	private static Predicate<String> equals(int testNumber) {
+		return n -> Integer.parseInt(n.replace(".test", "")) == testNumber;
+	}
+
 	private static Predicate<String> atleast(int testNumber) {
 		return n -> Integer.parseInt(n.replace(".test", "")) >= testNumber;
 	}

tests/000074.test

@@ -122,7 +122,7 @@ where |cards| == 52
 where all { i in 0..|cards|, j in 0..|cards| | (i != j) ==> (cards[i] != cards[j]) }
 
 // A real test of verifier performance!!
-Deck deck = [
+final Deck deck = [
         // Hearts
         TWO_HEARTS,
         THREE_HEARTS,

tests/000075.test

@@ -45,7 +45,7 @@ type Deck is (Card[] cards)
 where |cards| == 6
 
 // A real test of verifier performance!!
-Deck deck = [
+final Deck deck = [
         // Hearts
         TWO_HEARTS,
         THREE_HEARTS,

tests/000078.test

@@ -1,8 +1,7 @@
 original.name="Complex_Valid_4"
+boogie.timeout=120
 ======
 >>> main.whiley
-
-
 type BTree is null | {int item, BTree left, BTree right}
 
 function BTree() -> BTree:
@@ -50,5 +49,4 @@ public export method test() :
     assume contains(tree,8) == false
     assume contains(tree,1) == true
     assume contains(tree,9) == false
-
 ---

tests/000097.test

@@ -4,7 +4,7 @@ original.name="ConstrainedInt_Valid_22"
 type string is int[]
 type item is (int d) where (0 <= d) && (d < 7)
 
-string[] Days = ["Monday", "Tuesday", "Wednesday", "Thursday", "Friday", "Saturday", "Sunday"]
+final string[] Days = ["Monday", "Tuesday", "Wednesday", "Thursday", "Friday", "Saturday", "Sunday"]
 
 function inc(item i) -> item:
     return (i + 1) % 7

tests/000547.test

@@ -1,6 +1,4 @@
 original.name="StaticVar_Valid_11"
-boogie.ignore=true
-Whiley2Boogie.issue=138
 ======
 >>> main.whiley
 int var = 1

tests/000548.test

@@ -1,6 +1,4 @@
 original.name="StaticVar_Valid_12"
-boogie.ignore=true
-Whiley2Boogie.issue=138
 ======
 >>> main.whiley
 int var = 0

tests/000549.test

@@ -1,6 +1,4 @@
 original.name="StaticVar_Valid_13"
-boogie.ignore=true
-Whiley2Boogie.issue=138
 ======
 >>> main.whiley
 int var = 0

tests/000550.test

@@ -1,6 +1,4 @@
 original.name="StaticVar_Valid_14"
-boogie.ignore=true
-Whiley2Boogie.issue=138
 ======
 >>> main.whiley
 int var = 0

tests/000551.test

@@ -1,9 +1,5 @@
 original.name="StaticVar_Valid_15"
-whiley.execute.ignore=true
-WhileyCompiler.issue=1122
 js.compile.ignore=true
-boogie.ignore=true
-Whiley2Boogie.issue=138
 ======
 >>> main.whiley
 int var = 0

tests/000769.test

@@ -1,7 +1,7 @@
 original.name="While_Valid_19"
 ======
 >>> main.whiley
-int SIZE = 5
+final int SIZE = 5
 
 public export method test() :
     int[][] components = [[]; SIZE]

tests/000935.test

@@ -1,7 +1,5 @@
 original.name="DoWhile_Invalid_7"
 js.execute.ignore=true
-boogie.timeout=5
-boogie.ignore=true
 ======
 >>> main.whiley
 type nat is (int x) where x >= 0

tests/001163.test

@@ -1,6 +1,5 @@
 original.name="StaticVar_Invalid_13"
 js.compile.ignore=true
-boogie.ignore=true
 ======
 >>> main.whiley
 int var = -1
@@ -15,3 +14,8 @@ public export method test():
 ---
 E700 main.whiley 9,4:8
 E716 main.whiley 9,4:8
+=====
+>>> main.whiley 1:2
+type nat is (int x) where x >= 0
+nat var = 1
+---