|
@@ -1,26 +1,110 @@
|
|
| 1 |
|
| 2 |
|
| 3 |
typedef uint8_t T;
|
| 4 |
|
| 5 |
typedef uint16_t ST;
|
| 6 |
|
| 7 |
void rowSum(const int kn, const T* S, ST* D, const int n, const int cn) {
|
| 8 |
-
__requires("__is_geq(kn, 0)");
|
| 9 |
-
__requires("__is_geq(n, 1)");
|
| 10 |
-
__requires("__is_geq(cn, 0)");
|
| 11 |
-
|
| 12 |
-
__reads("S ~> Matrix2(n + kn, cn)");
|
| 13 |
-
__ghost(swap_groups, "items := fun i, c -> &D[MINDEX2(n, cn, i, c)] ~> Cell");
|
| 14 |
-
|
| 15 |
-
__sreads("S ~> Matrix2(n + kn, cn)");
|
| 16 |
-
__xmodifies("for i in 0..n -> &D[MINDEX2(n, cn, i, c)] ~> Cell");
|
| 17 |
-
for (int i = 0; i < n; i++) {
|
| 18 |
-
__sreads("S ~> Matrix2(n + kn, cn)");
|
| 19 |
-
__xmodifies("&D[MINDEX2(n, cn, i, c)] ~> Cell");
|
| 20 |
-
__ghost(assume, "F := is_subrange(i..i + kn, 0..n + kn)");
|
| 21 |
-
D[
|
|
|
|
|
|
|
| 22 |
-
}
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
| 23 |
-
|
|
|
|
|
|
|
|
|
|
| 24 |
-
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
| 25 |
-
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
| 26 |
}
|
| 1 |
|
| 2 |
|
| 3 |
typedef uint8_t T;
|
| 4 |
|
| 5 |
typedef uint16_t ST;
|
| 6 |
|
| 7 |
void rowSum(const int kn, const T* S, ST* D, const int n, const int cn) {
|
|
|
|
|
|
|
|
|
|
| 8 |
+
if (kn == 3) /*@kn*/ {
|
|
|
|
|
|
|
| 9 |
+
for (int ic = 0; ic < n * cn; ic++) {
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
| 10 |
+
D[ic / cn * cn + ic % cn] = (uint16_t)S[ic / cn * cn + ic % cn] +
|
| 11 |
+
(uint16_t)S[(1 + ic / cn) * cn + ic % cn] +
|
| 12 |
+
(uint16_t)S[(2 + ic / cn) * cn + ic % cn];
|
| 13 |
+
}
|
| 14 |
+
} /*kn@*/
|
| 15 |
+
else {
|
| 16 |
+
if (kn == 5) /*@kn*/ {
|
| 17 |
+
for (int ic = 0; ic < n * cn; ic++) {
|
| 18 |
+
D[ic / cn * cn + ic % cn] = (uint16_t)S[ic / cn * cn + ic % cn] +
|
| 19 |
+
(uint16_t)S[(1 + ic / cn) * cn + ic % cn] +
|
| 20 |
+
(uint16_t)S[(2 + ic / cn) * cn + ic % cn] +
|
| 21 |
+
(uint16_t)S[(3 + ic / cn) * cn + ic % cn] +
|
| 22 |
+
(uint16_t)S[(4 + ic / cn) * cn + ic % cn];
|
| 23 |
+
}
|
| 24 |
+
} /*kn@*/
|
| 25 |
+
else {
|
| 26 |
+
if (cn == 1) /*@cn*/ {
|
| 27 |
+
uint16_t s = (uint16_t)0;
|
| 28 |
+
for (int i = 0; i < kn; i++) {
|
| 29 |
+
s = s + (uint16_t)S[i];
|
| 30 |
+
}
|
| 31 |
+
D[0] = s;
|
| 32 |
+
for (int i = 1; i < n; i++) {
|
| 33 |
+
s = s + (uint16_t)S[-1 + i + kn] - (uint16_t)S[-1 + i];
|
| 34 |
+
D[i] = s;
|
| 35 |
+
}
|
| 36 |
+
} /*cn@*/
|
| 37 |
+
else {
|
| 38 |
+
if (cn == 3) /*@cn*/ {
|
| 39 |
+
uint16_t s = (uint16_t)0;
|
| 40 |
+
uint16_t s5 = (uint16_t)0;
|
| 41 |
+
uint16_t s6 = (uint16_t)0;
|
| 42 |
+
for (int i = 0; i < kn; i++) {
|
| 43 |
+
s = s + (uint16_t)S[3 * i];
|
| 44 |
+
s5 = s5 + (uint16_t)S[1 + 3 * i];
|
| 45 |
+
s6 = s6 + (uint16_t)S[2 + 3 * i];
|
| 46 |
+
}
|
| 47 |
+
D[0] = s;
|
| 48 |
+
D[1] = s5;
|
| 49 |
+
D[2] = s6;
|
| 50 |
+
for (int i = 1; i < n; i++) {
|
| 51 |
+
s = s + (uint16_t)S[3 * (-1 + i + kn)] - (uint16_t)S[3 * (-1 + i)];
|
| 52 |
+
s5 = s5 + (uint16_t)S[1 + 3 * (-1 + i + kn)] -
|
| 53 |
+
(uint16_t)S[1 + 3 * (-1 + i)];
|
| 54 |
+
s6 = s6 + (uint16_t)S[2 + 3 * (-1 + i + kn)] -
|
| 55 |
+
(uint16_t)S[2 + 3 * (-1 + i)];
|
| 56 |
+
D[3 * i] = s;
|
| 57 |
+
D[1 + 3 * i] = s5;
|
| 58 |
+
D[2 + 3 * i] = s6;
|
| 59 |
+
}
|
| 60 |
+
} /*cn@*/
|
| 61 |
+
else {
|
| 62 |
+
if (cn == 4) /*@cn*/ {
|
| 63 |
+
uint16_t s = (uint16_t)0;
|
| 64 |
+
uint16_t s7 = (uint16_t)0;
|
| 65 |
+
uint16_t s8 = (uint16_t)0;
|
| 66 |
+
uint16_t s9 = (uint16_t)0;
|
| 67 |
+
for (int i = 0; i < kn; i++) {
|
| 68 |
+
s = s + (uint16_t)S[4 * i];
|
| 69 |
+
s7 = s7 + (uint16_t)S[1 + 4 * i];
|
| 70 |
+
s8 = s8 + (uint16_t)S[2 + 4 * i];
|
| 71 |
+
s9 = s9 + (uint16_t)S[3 + 4 * i];
|
| 72 |
+
}
|
| 73 |
+
D[0] = s;
|
| 74 |
+
D[1] = s7;
|
| 75 |
+
D[2] = s8;
|
| 76 |
+
D[3] = s9;
|
| 77 |
+
for (int i = 1; i < n; i++) {
|
| 78 |
+
s = s + (uint16_t)S[4 * (-1 + i + kn)] -
|
| 79 |
+
(uint16_t)S[4 * (-1 + i)];
|
| 80 |
+
s7 = s7 + (uint16_t)S[1 + 4 * (-1 + i + kn)] -
|
| 81 |
+
(uint16_t)S[1 + 4 * (-1 + i)];
|
| 82 |
+
s8 = s8 + (uint16_t)S[2 + 4 * (-1 + i + kn)] -
|
| 83 |
+
(uint16_t)S[2 + 4 * (-1 + i)];
|
| 84 |
+
s9 = s9 + (uint16_t)S[3 + 4 * (-1 + i + kn)] -
|
| 85 |
+
(uint16_t)S[3 + 4 * (-1 + i)];
|
| 86 |
+
D[4 * i] = s;
|
| 87 |
+
D[1 + 4 * i] = s7;
|
| 88 |
+
D[2 + 4 * i] = s8;
|
| 89 |
+
D[3 + 4 * i] = s9;
|
| 90 |
+
}
|
| 91 |
+
} /*cn@*/
|
| 92 |
+
else {
|
| 93 |
+
/*@generic*/ for (int c = 0; c < cn; c++) {
|
| 94 |
+
uint16_t s = (uint16_t)0;
|
| 95 |
+
for (int i = 0; i < kn; i++) {
|
| 96 |
+
s = s + (uint16_t)S[i * cn + c];
|
| 97 |
+
}
|
| 98 |
+
D[c] = s;
|
| 99 |
+
for (int i = 1; i < n; i++) {
|
| 100 |
+
s = s + (uint16_t)S[(-1 + i + kn) * cn + c] -
|
| 101 |
+
(uint16_t)S[(-1 + i) * cn + c];
|
| 102 |
+
D[i * cn + c] = s;
|
| 103 |
+
}
|
| 104 |
+
} /*generic@*/
|
| 105 |
+
}
|
| 106 |
+
}
|
| 107 |
+
}
|
| 108 |
+
}
|
| 109 |
+
}
|
| 110 |
}
|