Add pointers

README.md

@@ -100,6 +100,16 @@ _invariant: TRUE
 } while ((r1 % 2) != 0)
 ```
 
+### Declassificaton
+
+To specify the declassification of a predicate it is necessary to specify both the expression being declassified and under what conditions this can happen. For example,
+
+```
+out = d(sum/cnt, cnt > min)
+```
+
+specifies that at this particular line the expression `sum/cnt` can be declassified if `cnt > min`.
+
 ### Supported operations
 * `=` assignment
 * `==` equal to
@@ -124,8 +134,22 @@ _invariant: TRUE
 ## TODOs
 ### Unsupported language features
 Below is an inconclusive list of unsupported language features.
- * Pointers
+ * Dynamic thread creation
+ * Objects
+
+### Improve Type System
+ * Nested arrays
+ * Arrays/Pointers to Bools
+ * Arrays of pointers
 
 ### Weak memory model
 The logic for the weak memory model is currently not implemented
 
+## Optimisations
+### Passification
+
+### General Improvemens
+ * Implement a standard interface for identifiers and remove specific logic where possible
+ * Objects are implemented, but implementation appears to be incorrect. Treiber stack put does not pass
+
+

tests/declassify/avg

@@ -0,0 +1,16 @@
+global var sum:
+_L: FALSE
+
+global var cnt:
+_L: TRUE
+
+global var out:
+_L: TRUE
+
+_Gamma_0: sum -> HIGH
+_Rely: TRUE
+_Guar: TRUE
+
+if (cnt > 5) {
+	out = d(sum/cnt, cnt > 5);
+}

tests/declassify/if1

@@ -0,0 +1,16 @@
+local var pass:
+
+local var ans:
+
+global var out:
+_L: TRUE
+
+_Gamma_0: pass -> HIGH
+_Rely: TRUE
+_Guar: TRUE
+
+if (d(pass == ans, TRUE)) {
+  out = 1;
+} else {
+  out = 0;
+}

tests/declassify/neg/avg1

@@ -0,0 +1,16 @@
+global var sum:
+_L: FALSE
+
+global var cnt:
+_L: TRUE
+
+global var out:
+_L: TRUE
+
+_Gamma_0: sum -> HIGH
+_Rely: TRUE
+_Guar: TRUE
+
+if (cnt > 5) {
+	out = sum/cnt;
+}

tests/declassify/neg/avg2

@@ -0,0 +1,16 @@
+global var sum:
+_L: FALSE
+
+global var cnt:
+_L: TRUE
+
+global var out:
+_L: TRUE
+
+_Gamma_0: sum -> HIGH
+_Rely: TRUE
+_Guar: TRUE
+
+if (cnt >= 5) {
+	out = d(sum/cnt, cnt > 5);
+}

tests/declassify/neg/if1

@@ -0,0 +1,16 @@
+local var pass:
+
+local var ans:
+
+global var out:
+_L: TRUE
+
+_Gamma_0: pass -> HIGH
+_Rely: TRUE
+_Guar: TRUE
+
+if (pass == ans) {
+  out = 1;
+} else {
+  out = 0;
+}

tests/declassify/put

@@ -0,0 +1,51 @@
+global var z:
+_L: TRUE
+
+global var tail:
+_L: TRUE
+
+global var head:
+_L: TRUE
+
+global var L:
+_L: TRUE
+
+global array tasks[1]:
+_L: levels[_i] == 1
+_Rely: tasks[_i] == tasks'[_i]
+_Guar: TRUE
+
+global array levels[1]:
+_L: TRUE
+_Rely: levels[_i] == levels'[_i]
+_Guar: (z % 2 == 0 && z' == z) => (levels[_i] == levels'[_i])
+
+local var t:
+
+global var task:
+_L: level == 1
+
+global var level:
+_L: TRUE
+
+local var dec:
+
+_Gamma_0: z -> LOW, dec -> LOW
+_Rely: z == z' && task == task' && level == level' && L == L'
+_Guar: z' >= z
+
+if (z % 2 == 1) {
+	z = z + 1;
+}
+
+t = tail;
+z = z + 1;
+if (dec == 1) {
+	levels[t % L] = 1;
+	tasks[t % L] = d(task, dec == 1);
+} else {
+	levels[t % L] = level;
+	tasks[t % L] = task;
+}
+z = z + 1;
+tail = t + 1;

tests/rg/caslev/steal_0 → tests/rg/caslev/steal_

@@ -23,7 +23,6 @@ _Guar: levels[_i] == levels'[_i]
 local var t:
 local var h:
 local var r:
-local var index:
 local var level:
 local var task:
 
@@ -47,10 +46,9 @@ if (h < t) {
 			r = z;
 		} while (r % 2 == 1)
 
-		index = h % L;
-		level = levels[index];
+		level = levels[h % L];
 		if (level == 1) {
-			task = tasks[index];
+			task = tasks[h % L];
 		} else {
 			task = -1; // fail
 		}

tests/rg/neg/pointers1

@@ -0,0 +1,13 @@
+global var a:
+_L: FALSE
+
+global var b:
+_L: FALSE
+
+_Rely: a == a' && b == b'
+_Guar: TRUE
+
+a = 2;
+b = &a;
+*b = 1;
+assert a == 2;

tests/rg/neg/pointers2

@@ -0,0 +1,19 @@
+global var a:
+_L: FALSE
+
+global var b:
+_L: FALSE
+
+global var out:
+_L: a % 2 == 0
+
+global var secret:
+_L: FALSE
+
+_Rely: a == a' && b == b'
+_Guar: TRUE
+
+a = 1;
+b = &a;
+*b = 2;
+out = secret;

tests/rg/neg/pointers3

@@ -0,0 +1,22 @@
+global var a:
+_L: FALSE
+
+global var *b:
+_L: FALSE
+_PT: a
+
+global var out:
+_L: a == 2
+
+global var secret:
+_L: FALSE
+
+_Gamma_0: out -> LOW
+_Rely: a == a' && b == b'
+_Guar: TRUE
+
+a = 2;
+b = &a;
+*b = 1;
+out = secret; // SAFE: a = 1
+*b = 2; // UNSAFE: invalid control

tests/rg/neg/pointers4

@@ -0,0 +1,21 @@
+global var a:
+_L: FALSE
+_PT: b
+
+global var b:
+_L: FALSE
+
+global var c:
+_L: *b == 1
+
+global var secret:
+_L: FALSE
+
+_Rely: a == a' && b == b' && c == c'
+_Guar: TRUE
+
+a = 1;
+b = &a;
+a = 1;
+c = secret;
+

tests/rg/neg/pointers5

@@ -0,0 +1,21 @@
+global var a:
+_L: FALSE
+_PT: b
+
+global var b:
+_L: FALSE
+
+global var c:
+_L: *b == 1
+
+global var secret:
+_L: FALSE
+
+_Rely: a == a' && b == b' && c == c'
+_Guar: TRUE
+
+b = &a;
+a = 0; // SAFE
+c = secret;
+a = 1; // UNSAFE
+

tests/rg/neg/pointers6

@@ -0,0 +1,15 @@
+global var a:
+_L: FALSE
+_PT: b
+
+global var b:
+_L: FALSE
+
+global var c:
+_L: *b == 1
+
+_Rely: a == a' && b == b' && c == c'
+_Guar: TRUE
+
+b = &a;
+