Runtime Verification

examples/runtime/ledgerExample.java

@@ -0,0 +1,98 @@
+package test;
+
+import java.lang.reflect.Array;
+import java.util.concurrent.ConcurrentHashMap;
+
+
+class Ledger {
+
+    public static ConcurrentHashMap<Long, ConcurrentHashMap<Object, Double>> __runtime__ = new ConcurrentHashMap<Long, ConcurrentHashMap<Object, Double>>();
+    public static ConcurrentHashMap<Object, ConcurrentHashMap<Integer, Object>> __array_locations = new ConcurrentHashMap<Object, ConcurrentHashMap<Integer, Object>>();
+
+
+    public static void createHashMap() {
+        if (!__runtime__.containsKey(Thread.currentThread().getId())) {
+            __runtime__.put(Thread.currentThread().getId(), new ConcurrentHashMap<Object, Double>());
+        }
+    }
+
+    public static Double getPermission(Object input) {
+        createHashMap();
+        return __runtime__.get(Thread.currentThread().getId()).getOrDefault(input, 0.0);
+    }
+
+    public static Double getPermission(Object input, int location) {
+        createHashMap();
+        Object permLoc = __array_locations.get(input).get(location);
+        return getPermission(permLoc);
+    }
+
+    public static void setPermission(Object input, Double value) {
+        assert (value >= 0 && value <= 1) : "value is not between bounds 0 and 1: " + value;
+        createHashMap();
+        __runtime__.get(Thread.currentThread().getId()).put(input, value);
+    }
+
+    public static void setPermission(Object input, int location, Double value) {
+        createHashMap();
+        assert (input.getClass().isArray());
+        Object permLoc = __array_locations.get(input).get(location);
+        setPermission(permLoc, value);
+    }
+
+    public static void initiatePermission(Object input) {
+        createHashMap();
+        setPermission(input, 1.0);
+        if (input.getClass().isArray()) {
+            initiatePermission(input, Array.getLength(input));
+        }
+    }
+
+    public static void initiatePermission(Object input, int size) {
+        createHashMap();
+        setPermission(input, 1.0);
+        __array_locations.put(input, new ConcurrentHashMap<>());
+        for (int i = 0; i < size; i++) {
+            Object[] permLoc = {input, i};
+            __array_locations.get(input).put(i, permLoc);
+            setPermission(permLoc, 1.0);
+        }
+
+    }
+}
+
+
+class Test extends Thread{
+    int[] a;
+    int b;
+
+    public Test(int[] a) {
+        this.a = a;
+    }
+
+    /*@
+        requires Perm(this.a, write);
+     */
+    @Override
+    public void run() {
+        Ledger.setPermission(this.a, 1.0);
+        System.out.println("External thread: " + Ledger.getPermission(this.a));
+        super.run();
+    }
+}
+
+
+class Main {
+
+    public static void main(String[] args) {
+        int[] a = new int[]{1, 2, 3, 4};
+        Ledger.initiatePermission(a);
+        Test test = new Test(a);
+        Ledger.setPermission(test.a, Ledger.getPermission(test.a) - 1.0);
+        test.start();
+        Ledger.initiatePermission(test, 1);
+        System.out.println(Ledger.getPermission(test.a));
+        System.out.println(Ledger.getPermission(test, 0));
+    }
+}
+

examples/runtime/lockInvariant.java

@@ -0,0 +1,16 @@
+//@ lock_invariant Perm(this.i, write);
+class Source {
+    int i;
+
+    public void test(){
+        int x = this.i;
+        synchronized (this) {
+            this.i = 0;
+        }
+    }
+
+    public void main() {
+        Source source = new Source();
+        source.test();
+    }
+}

examples/runtime/loopInvariants.java

@@ -0,0 +1,29 @@
+class Program {
+    int[] a;
+
+    public void setA(int[] a) {
+        this.a = a;
+    }
+
+    public int indexOf(int b) {
+        //@ loop_invariant i <= a.length;
+        //@ loop_invariant (\forall* int j; 0 <= j && j < a.length; Perm(a[j], read));
+        //@ loop_invariant (\forall int j; 0 <= j && j < a.length; a[j] % 3 == 0);
+        for(int i = 0; i < a.length; i++) {
+            if(a[i] == b) {
+                return i;
+            }
+        }
+        return -1;
+    }
+
+    public void main() {
+        Program program = new Program();
+        int[] tmp = new int[3];
+        tmp[0] = 2;
+        tmp[1] = 4;
+        tmp[2] = 6;
+        program.setA(tmp);
+        program.indexOf(4);
+    }
+}

examples/runtime/predicates.java

@@ -0,0 +1,39 @@
+public class Main {
+
+    //@ requires c != null ** c.state(0);
+    //@ ensures c.state(2);
+    void foo(Counter c) {
+        c.increment(2);
+    }
+
+    public void execute() {
+        Counter c = new Counter();
+        //@ fold c.state(0);
+        Counter c2 = new Counter();
+        //@ fold c2.state(0);
+
+        foo(c);
+        foo(c2);
+    }
+
+    public void main() {
+        Main m = new Main();
+        m.execute();
+    }
+}
+
+
+class Counter {
+    int count;
+
+    //@ resource state(int val) = Perm(count, write) ** count == val;
+
+    //@ requires state(count);
+    //@ ensures state(count);
+    void increment(int n) {
+        int z = count;
+        //@ unfold state(count);
+        count += n;
+        //@ fold state(count);
+    };
+}

examples/runtime/quantifiers.java

@@ -0,0 +1,40 @@
+class Program {
+    int[] a;
+    int b;
+
+
+    /*@
+        requires (\forall* int i; 0 <= i && i < a.length; Perm(a[i], write));
+     */
+    public void setA(int[] a) {
+        this.a = a;
+    }
+
+    /*@
+        requires a.length > 0;
+        requires (\forall* int x; 0 <= x && x < a.length; Perm(a[x], write));
+        requires (\forall int x; 0 <= x && x < a.length; a[x] > 0);
+        requires (\forall int x; 0 <= x && x < a.length; (\forall int j; 0 <= j && j < x; a[j] >= a[x]));
+        ensures (\forall* int x; 0 <= x && x < a.length; Perm(a[x], write));
+        ensures (\exists int x; 0 <= x && x < a.length; a[x] > 0);
+     */
+    //ensures (\exists int x; 0 <= x && x < a.length; a[x] == b) ==> \result >= 0;
+    public int indexOf(int b) {
+        for (int i = 0; i < a.length; i++) {
+            if (a[i] == b) {
+                return i;
+            }
+        }
+        return -1;
+    }
+
+    public void main() {
+        Program program = new Program();
+        int[] tmp = new int[3];
+        tmp[0] = 2;
+        tmp[1] = 4;
+        tmp[2] = 6;
+        program.setA(tmp);
+        program.indexOf(4);
+    }
+}

examples/runtime/sinksource.java

@@ -0,0 +1,62 @@
+import java.util.*;
+
+
+class Source extends Thread {
+    int i;
+
+    /*@
+        requires Perm(this.i, 1);
+        ensures Perm(this.i, 1);
+     */
+    public void run() {
+        i = 42;
+    }
+
+    public void join(){}
+    public void start(){}
+}
+
+class Sink extends Thread {
+    Source source;
+
+    public void setSource(Source source) {
+        this.source = source;
+    }
+
+    /*@
+       requires Perm(source, 1);
+       ensures Perm(source, 1);
+       ensures Perm(source.i, 1/2);
+    */
+    public void run() {
+
+        //@ source.postJoin(1\2);
+        source.join();
+        source.i = 1;
+    }
+
+    public void join(){}
+    public void start(){}
+}
+
+class Main{
+
+    public void main() {
+        Source source = new Source();
+        Sink sink = new Sink();
+        sink.setSource(source);
+
+        sink.source.i = 1;
+        source.start();
+        sink.start();
+        //@ source.postJoin(1\2);
+        source.join();
+        //@ sink.postJoin(1);
+        sink.join();
+        source.i = 1988;
+    }
+}
+
+class Thread{
+
+}

examples/runtime/sinksourcearray.java

@@ -0,0 +1,67 @@
+class Source extends Thread {
+    int[] i;
+
+    public void createI() {
+        this.i = new int[2];
+    }
+
+    /*@
+        requires Perm(this.i, 1);
+        requires (\forall* int j; 0 <= j && j < i.length; Perm(i[j], write));
+        ensures Perm(this.i, 1);
+        ensures (\forall* int j; 0 <= j && j < i.length; Perm(i[j], write));
+     */
+    public void run() {
+        i[0] = 42;
+        i[1] = 43;
+    }
+
+
+    public void join(){}
+    public void start(){}
+}
+
+class Sink extends Thread {
+    Source source;
+
+    public void setSource(Source source) {
+        this.source = source;
+    }
+
+    /*@
+       requires Perm(source, 1);
+       ensures Perm(source, 1);
+       ensures Perm(source.i, 1/2);
+       ensures (\forall* int j; 0 <= j && j < source.i.length ==> Perm(source.i[j], 1/2));
+    */
+    public void run() {
+        //@ source.postJoin(1\2);
+        source.join();
+        source.i[0] = 1;
+    }
+
+    public void join(){}
+    public void start(){}
+}
+
+class Main{
+
+    public void main() {
+        Source source = new Source();
+        Sink sink = new Sink();
+        sink.setSource(source);
+        source.createI();
+
+        source.start();
+        sink.start();
+        //@ source.postJoin(1/2);
+        source.join();
+        //@ sink.postJoin(1);
+        sink.join();
+        source.i[0] = 1988;
+    }
+}
+
+class Thread{
+
+}

examples/runtime/sinksourcearrayobjects.java

@@ -0,0 +1,30 @@
+class DummyData {
+    int val;
+}
+
+class Source {
+    DummyData[] i;
+
+    public void createI() {
+        this.i = new DummyData[2];
+        DummyData o = new DummyData();
+        this.i[0] = o;
+        this.i[1] = o;
+    }
+
+    /*@
+        requires Perm(this.i, 1);
+        requires (\forall* int j; 0 <= j && j < i.length; Perm(i[j].val, write));
+        ensures Perm(this.i, 1);
+        ensures (\forall* int j; 0 <= j && j < i.length; Perm(i[j].val, write));
+     */
+    public void test() {
+
+    }
+
+    public void main(){
+        Source source = new Source();
+        source.createI();
+        source.test();
+    }
+}