-
Notifications
You must be signed in to change notification settings - Fork 26
Commit
This commit does not belong to any branch on this repository, and may belong to a fork outside of the repository.
Merge branch 'dev' into rasi_generator
- Loading branch information
Showing
413 changed files
with
11,039 additions
and
6,453 deletions.
There are no files selected for viewing
Empty file.
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
| Original file line number | Diff line number | Diff line change |
|---|---|---|
| @@ -1,2 +1,2 @@ | ||
| -Xss32m | ||
| -Xss128m | ||
| -Xmx2G |
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
| Original file line number | Diff line number | Diff line change |
|---|---|---|
| @@ -1 +1 @@ | ||
| 0.11.6 | ||
| 0.11.7 |
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
| Original file line number | Diff line number | Diff line change |
|---|---|---|
| @@ -0,0 +1,30 @@ | ||
| version = 3.8.1 | ||
| runner.dialect = scala213 | ||
|
|
||
| maxColumn = 80 | ||
|
|
||
| # always add trailing commas in expressions with more than one argument | ||
| # do allow removing the trailing comma if the expression fits on one line | ||
| rewrite.trailingCommas.style = "multiple" | ||
| rewrite.trailingCommas.allowFolding = true | ||
|
|
||
| # regardless of the input, try to compact expressions into one line | ||
| # the readability of this option is guarded by the fact that maxColumn = 80 | ||
| newlines.source = fold | ||
| # never keep a part of the expression on the same line of a case/if/def/val if | ||
| # it is already multiple lines. | ||
| newlines.beforeMultiline = unfold | ||
| newlines.forceBeforeMultilineAssign = def | ||
| # try not to break strings by breaking them at interpolation points | ||
| # e.g. "longText ${x} moreLongText" | ||
| # should not be: | ||
| # "longText ${ | ||
| # x} moreLongText" | ||
| # and instead should just overflow the line. | ||
| newlines.inInterpolation = avoid | ||
| # prefer to place a newline *before* the "implicit" keyword; not after. | ||
| newlines.implicitParamListModifierPrefer = before | ||
|
|
||
| # default: align the => arrows in cases | ||
| # here: do not align them, typically doesn't help readability. | ||
| align.preset = none |
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
| Original file line number | Diff line number | Diff line change |
|---|---|---|
| @@ -0,0 +1,69 @@ | ||
| // Compile with | ||
| // gcc -mavx -o vector_add vector_add.c | ||
|
|
||
| #include <assert.h> | ||
| #include <immintrin.h> | ||
| #include <stdbool.h> | ||
|
|
||
| /*@ | ||
| context_everywhere n >= 0 && n % 4 == 0; | ||
| context_everywhere a != NULL && \pointer_length(a) >= n; | ||
| context_everywhere b != NULL && \pointer_length(b) >= n; | ||
| context_everywhere c != NULL && \pointer_length(c) >= n; | ||
| context_everywhere (\forall* int i; 0<=i && i<n; Perm(&a[i], 1\2)); | ||
| context_everywhere (\forall* int i; 0<=i && i<n; Perm(&b[i], 1\2)); | ||
| context_everywhere (\forall* int i; 0<=i && i<n; Perm(&c[i], write)); | ||
| ensures (\forall int j; 0 <= j && j<n; {:c[j]:} == a[j] + b[j]); | ||
| @*/ | ||
| void vector_add(int *a, int *b, int *c, int n){ | ||
| /*@ | ||
| loop_invariant 0<=i && i<=n && i%4 == 0; | ||
| loop_invariant (\forall int j; 0 <= j && j<i; {:c[j]:} == a[j] + b[j]); | ||
| @*/ | ||
| for(int i = 0; i < n; i+=4){ | ||
| // Normally this should be: | ||
| // a4 = _mm_load_si128((__m128i*)(a + i)); | ||
| // _mm_load_si128 | ||
| // But then we need good support for casting between pointers. | ||
| __v4si a4 = {a[i], a[i+1], a[i+2], a[i+3]}; | ||
| __v4si b4 = {b[i], b[i+1], b[i+2], b[i+3]}; | ||
| __v4si c4 = a4 + b4; | ||
| __v4si d4 = a4 == b4; | ||
| // _mm_store_si128(c+i, c4); | ||
| c[i] = c4[0]; | ||
| c[i+1] = c4[1]; | ||
| c[i+2] = c4[2]; | ||
| c[i+3] = c4[3]; | ||
| } | ||
| } | ||
|
|
||
|
|
||
| int main(){ | ||
|
|
||
| int a[4*100]; | ||
| int b[4*100]; | ||
| /*@ | ||
| loop_invariant 0<=i && i<=4*100; | ||
| loop_invariant (\forall* int j; 0 <= j && j<4*100; Perm(&a[j],write)); | ||
| loop_invariant (\forall* int j; 0 <= j && j<4*100; Perm(&b[j],write)); | ||
| loop_invariant (\forall int j; 0 <= j && j<i; a[j] == j); | ||
| loop_invariant (\forall int j; 0 <= j && j<i; b[j] == 400-j); | ||
| @*/ | ||
| for(int i = 0; i < 4*100; i++){ | ||
| a[i] = i; | ||
| b[i] = 400-i; | ||
| } | ||
| int c[4*100]; | ||
| vector_add(a, b, c, 4*100); | ||
| //@ assert((\forall int j; 0 <= j && j<4*100; c[j] == 400)); | ||
| /*@ | ||
| loop_invariant 0<=i && i<=4*100; | ||
| loop_invariant (\forall* int j; 0 <= j && j<4*100; Perm(&c[j],write)); | ||
| loop_invariant (\forall int j; 0 <= j && j<4*100; c[j] == 400); | ||
| @*/ | ||
| for(int i=0; i<4*100; i++){ | ||
| assert(c[i] == 400); | ||
| } | ||
|
|
||
| return 0; | ||
| } |
Oops, something went wrong.