Merge pull request #1052 from utwente-fmt/sycl-rq1

Implemented basic C++ support

build.sc

@@ -41,19 +41,20 @@ object col extends VercorsModule {
 
 
 object parsers extends VercorsModule {
-  def key = "parsers"
-  def generatedSources = T.sources {
-    Seq(
-      antlr.c.generate(),
-      antlr.java.generate(),
-      antlr.pvl.generate(),
-			antlr.llvm.generate(),
-    )
-  }
-  def deps = Agg(
-    ivy"org.antlr:antlr4-runtime:4.8"
-  )
-  def moduleDeps = Seq(hre, col)
+	def key = "parsers"
+	def generatedSources = T.sources {
+		Seq(
+			antlr.c.generate(),
+			antlr.cpp.generate(),
+			antlr.java.generate(),
+			antlr.pvl.generate(),
+      antlr.llvm.generate(),
+		)
+	}
+	def deps = Agg(
+		ivy"org.antlr:antlr4-runtime:4.8"
+	)
+	def moduleDeps = Seq(hre, col)
 }
 
 object rewrite extends VercorsModule {

examples/concepts/cpp/Arrays.cpp

@@ -0,0 +1,21 @@
+// -*- tab-width:2 ; indent-tabs-mode:nil -*-
+//:: cases Loops
+//:: tools silicon
+//:: verdict Pass
+
+//@ requires size > 0;
+//@ context \pointer(a, size, read);
+//@ requires (\forall int i = 0 .. size; {: a[i] :} == 0);
+//@ ensures \result == b;
+int sumWithLast(int a[], int size, int b) {
+	int sum = a[size-1] + b;
+	//@ assert a[size-1] == 0;
+	return sum;
+}
+
+//@ requires size > 2;
+//@ context \pointer(a, size, write);
+//@ ensures a[2] == 5;
+void writeToArray(int a[], int size) {
+	a[2] = 5;
+}

examples/concepts/cpp/Conditionals.cpp

@@ -0,0 +1,33 @@
+// -*- tab-width:2 ; indent-tabs-mode:nil -*-
+//:: cases Conditionals
+//:: tools silicon
+//:: verdict Pass
+
+void onlyAssignInIf() {
+	int num = 5;
+	int result;
+	if (num < 10) {
+		result = 10;
+	}
+	//@ assert result == 10;
+}
+
+void matchIf() {
+	int num = 5;
+	int result = 0;
+	if (num < 10) {
+		result = 10;
+	}
+	//@ assert result == 10;
+}
+
+void matchElse() {
+	int num = 5;
+	int result = 0;
+	if (num < 5) {
+		result = 10;
+	} else {
+		result = 20;
+	}
+	//@ assert result == 20;
+}

examples/concepts/cpp/Loops.cpp

@@ -0,0 +1,26 @@
+// -*- tab-width:2 ; indent-tabs-mode:nil -*-
+//:: cases Loops
+//:: tools silicon
+//:: verdict Pass
+
+
+void whileLoop() {
+	int numLoops = 10;
+	//@ decreases numLoops;
+	//@ loop_invariant numLoops >= 0;
+	while(numLoops > 0) {
+		numLoops--;
+	}
+}
+
+//@ context_everywhere size >= 0;
+//@ context_everywhere \pointer(arr, size, read);
+void forArrayLoop(bool arr[], int size) {
+	bool sum = true;
+
+	//@ loop_invariant i >= 0 && i <= size;
+	//@ loop_invariant sum == (\forall int j; j >= 0 && j < i; arr[j]);
+	for(int i = 0; i < size; i++) {
+		sum = sum && arr[i];
+	}
+}

examples/concepts/cpp/Namespaces.cpp

@@ -0,0 +1,48 @@
+// -*- tab-width:2 ; indent-tabs-mode:nil -*-
+//:: cases Namespaces
+//:: tools silicon
+//:: verdict Pass
+
+int x;
+
+namespace spaceA {
+	int x;
+
+	//@ context Perm(x, write);
+	//@ ensures x == 90;
+	//@ ensures \result == \old(x) + 1;
+	int incr() {
+		int newX = x + 1;
+		x = 90;
+		return newX;
+	}
+
+	namespace spaceB {
+		//@ context Perm(x, 0.5);
+		//@ ensures \result == x + 2;
+		int incr() {
+  		return x + 2;
+  	}
+
+  	void doNothing() {};
+	}
+}
+
+//@ context Perm(spaceA::x, write);
+//@ context Perm(x, write);
+int main() {
+	x = 99;
+	spaceA::x = 5;
+	//@ assert spaceA::x == 5;
+  int varA = spaceA::incr();
+  //@ assert varA == 6;
+  //@ assert spaceA::x == 90;
+  int varB = spaceA::spaceB::incr();
+  //@ assert varB == 92;
+  spaceA::spaceB::doNothing();
+  int varX = spaceA::x;
+  //@ assert varX == 90;
+
+  //@ assert x == 99;
+  return 0;
+}

examples/concepts/cpp/NamespacesDoNotFindWithoutNamespacePrefix.cpp

@@ -0,0 +1,15 @@
+// -*- tab-width:2 ; indent-tabs-mode:nil -*-
+//:: cases NamespacesDoNotFindWithoutNamespacePrefix
+//:: tools silicon
+//:: verdict Fail
+
+namespace spaceA {
+
+	namespace spaceB {
+	  int b = 10;
+	}
+
+	int getB() {
+	   return b;
+	}
+}

examples/concepts/cpp/Operators.cpp

@@ -0,0 +1,88 @@
+// -*- tab-width:2 ; indent-tabs-mode:nil -*-
+//:: cases Operators
+//:: tools silicon
+//:: verdict Pass
+
+void test() {
+
+    int num = 5;
+
+    int numPlus = num + 5;
+    //@ assert numPlus == 10;
+
+    int numMinus = num - 5;
+    //@ assert numMinus == 0;
+
+    int numMult = num * 5;
+    //@ assert numMult == 25;
+
+    int numDiv = num / 5;
+    //@ assert numDiv == 1;
+
+    int numMod = num % 5;
+    //@ assert numMod == 0;
+
+    num++;
+    //@ assert num == 6;
+
+    num--;
+    //@ assert num == 5;
+
+    num += 5;
+    //@ assert num == 10;
+
+    num -= 5;
+    //@ assert num == 5;
+
+    num *= 5;
+    //@ assert num == 25;
+
+    num /= 5;
+    //@ assert num == 5;
+
+    num %= 5;
+    //@ assert num == 0;
+
+    int numMinus2 = -5;
+    //@ assert numMinus2 == -5;
+
+    int numPlus2 = +5;
+    //@ assert numPlus2 == 5;
+
+    bool boolean = true;
+
+    bool booleanNot = !boolean;
+    //@ assert booleanNot == false;
+
+    bool booleanNot2 = not boolean;
+    //@ assert booleanNot2 == false;
+
+    bool booleanAnd = boolean && false;
+    //@ assert booleanAnd == false;
+
+    bool booleanOr = boolean || false;
+    //@ assert booleanOr == true;
+
+    bool booleanEquals = boolean == true;
+    //@ assert booleanEquals == true;
+
+    bool booleanNotEquals = boolean != true;
+    //@ assert booleanNotEquals == false;
+
+    num = 5;
+
+    bool booleanLess = num < 6;
+    //@ assert booleanLess == true;
+
+    bool booleanLessEq = num <= 5;
+    //@ assert booleanLessEq == true;
+
+    bool booleanGreater = num > 4;
+    //@ assert booleanGreater == true;
+
+    bool booleanGreaterEq = num >= 5;
+    //@ assert booleanGreaterEq == true;
+
+    //@ assert 4 - 3 - 2 - 1 == (((4 - 3) - 2) - 1);
+
+}

examples/concepts/cpp/Pointers.cpp

@@ -0,0 +1,12 @@
+// -*- tab-width:2 ; indent-tabs-mode:nil -*-
+//:: cases Pointers
+//:: tools silicon
+//:: verdict Pass
+
+//@ context \pointer(ints, size, write);
+void test(int ints[], int size, int* p) {
+	int* intsPtr = ints;
+	//@ assert intsPtr == ints;
+
+	void* voidPtr = nullptr;
+}

examples/concepts/cpp/Scoping.cpp

@@ -0,0 +1,17 @@
+// -*- tab-width:2 ; indent-tabs-mode:nil -*-
+//:: cases Scoping
+//:: tools silicon
+//:: verdict Pass
+void test() {
+	int a = 10;
+	int b = 10;
+
+	{
+		a = 20;
+		int b = 20;
+		//@ assert a == 20;
+		//@ assert b == 20;
+	}
+	//@ assert a == 20;
+	//@ assert b == 10;
+}

examples/concepts/cpp/Types.cpp

@@ -0,0 +1,17 @@
+// -*- tab-width:2 ; indent-tabs-mode:nil -*-
+//:: cases Types
+//:: tools silicon
+//:: verdict Pass
+
+void test() {
+	bool aBool = true;
+
+	int anInt = 5;
+	long aLong = 5;
+	double aDouble = 5.1;
+	float aFloat = 5.1;
+
+	char aChar = 'a';
+
+	void* voidPtr = nullptr;
+}

examples/concepts/cpp/methods/AbstractMethod.cpp

@@ -0,0 +1,13 @@
+// -*- tab-width:2 ; indent-tabs-mode:nil -*-
+//:: cases AbstractMethod
+//:: tools silicon
+//:: verdict Pass
+
+/*@ ghost
+	ensures \result == a >= 0;
+	bool isPositive(int a);
+*/
+
+//@ requires b != 0;
+//@ ensures \result == a / b;
+int div(int a, int b);

examples/concepts/cpp/methods/ContextAndContextEverywhere.cpp

@@ -0,0 +1,23 @@
+// -*- tab-width:2 ; indent-tabs-mode:nil -*-
+//:: cases ContextAndContextEverywhere
+//:: tools silicon
+//:: verdict Pass
+
+//@ context b != 0;
+// requires b != 0;
+// ensures b != 0;
+int div(int a, int b) {
+	return a / b;
+}
+
+//@ context_everywhere number > 0;
+// requires number > 0;
+// ensures number > 0;
+int factorial(int number) {
+	int result = 1;
+	// loop_invariant number > 0;
+	for(int i = 2; i <= number; i++) {
+		result *= i;
+	}
+	return result;
+}

examples/concepts/cpp/methods/Decreases.cpp

@@ -0,0 +1,12 @@
+// -*- tab-width:2 ; indent-tabs-mode:nil -*-
+//:: cases Decreases
+//:: tools silicon
+//:: verdict Pass
+
+//@ decreases number;
+int factorial(int number) {
+	if (number <= 1) {
+		return 1;
+	}
+	return number * factorial(number - 1);
+}