Skip to content

Commit

Permalink
Merge branch 'dev' into vcllvm_globals
Browse files Browse the repository at this point in the history
  • Loading branch information
pieter-bos authored Jul 7, 2023
2 parents a736980 + 0cfbe99 commit 7011e7d
Show file tree
Hide file tree
Showing 120 changed files with 4,550 additions and 84 deletions.
2 changes: 1 addition & 1 deletion .github/workflows/scalatest.yml
Original file line number Diff line number Diff line change
Expand Up @@ -33,7 +33,7 @@ jobs:
!**/upstreamAssembly.json
key: vercors-ci-ubuntu
- name: Compile
run: ./mill --no-default-predef -j 0 allTests.assembly
run: ./mill -j 0 allTests.assembly
- name: Upload
uses: actions/upload-artifact@v3
with:
Expand Down
2 changes: 1 addition & 1 deletion .mill-version
Original file line number Diff line number Diff line change
@@ -1 +1 @@
0.11.0-M11
0.11.1
27 changes: 14 additions & 13 deletions build.sc
Original file line number Diff line number Diff line change
Expand Up @@ -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 {
Expand Down
21 changes: 21 additions & 0 deletions examples/concepts/cpp/Arrays.cpp
Original file line number Diff line number Diff line change
@@ -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;
}
33 changes: 33 additions & 0 deletions examples/concepts/cpp/Conditionals.cpp
Original file line number Diff line number Diff line change
@@ -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;
}
26 changes: 26 additions & 0 deletions examples/concepts/cpp/Loops.cpp
Original file line number Diff line number Diff line change
@@ -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];
}
}
48 changes: 48 additions & 0 deletions examples/concepts/cpp/Namespaces.cpp
Original file line number Diff line number Diff line change
@@ -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;
}
Original file line number Diff line number Diff line change
@@ -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;
}
}
88 changes: 88 additions & 0 deletions examples/concepts/cpp/Operators.cpp
Original file line number Diff line number Diff line change
@@ -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);

}
12 changes: 12 additions & 0 deletions examples/concepts/cpp/Pointers.cpp
Original file line number Diff line number Diff line change
@@ -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;
}
17 changes: 17 additions & 0 deletions examples/concepts/cpp/Scoping.cpp
Original file line number Diff line number Diff line change
@@ -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;
}
17 changes: 17 additions & 0 deletions examples/concepts/cpp/Types.cpp
Original file line number Diff line number Diff line change
@@ -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;
}
13 changes: 13 additions & 0 deletions examples/concepts/cpp/methods/AbstractMethod.cpp
Original file line number Diff line number Diff line change
@@ -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);
23 changes: 23 additions & 0 deletions examples/concepts/cpp/methods/ContextAndContextEverywhere.cpp
Original file line number Diff line number Diff line change
@@ -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;
}
12 changes: 12 additions & 0 deletions examples/concepts/cpp/methods/Decreases.cpp
Original file line number Diff line number Diff line change
@@ -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);
}
Loading

0 comments on commit 7011e7d

Please sign in to comment.