Trace for box_filter_rowsum✔
  1. Preprocessing loop contracts✔
  2. Reduce.intro [cVarDef "s"];✔
  3. Specialize.variable_multi ~mark_then:fst ~mark_else:"nokn" ["kn", int 3; "kn", int 5] [cFunBody "rowSum"; cFor "i"];✔
  4. Reduce.elim ~inline:true [nbMulti; cMark "kn"; cFun "reduce_spe1"];✔
  5. Loop.collapse [nbMulti; cMark "kn"; cFor "i"];✔
  6. Loop.swap [nbMulti; cMark "nokn"; cFor "i"];✔
  7. Reduce.slide ~mark_alloc:"acc" [nbMulti; cMark "nokn"; cArrayWrite "D"];✔
  8. Reduce.elim [nbMulti; cMark "acc"; cFun "reduce_spe1"];✔
  9. Variable.elim_reuse [nbMulti; cMark "acc"];✔
  10. Reduce.elim ~inline:true [nbMulti; cMark "nokn"; cFor "i"; cFun "reduce_spe1"];✔
  11. Specialize.variable_multi ~mark_then:fst ["cn", int 1; "cn", int 3; "cn", int 4] [cMark "nokn"; cFor "c"];✔
  12. Loop.unroll [nbMulti; cMark "cn"; cFor "c"];✔
  13. Target.foreach [nbMulti; cMark "cn"] (fun c -> Loop.fusion_targets ~into:FuseIntoLast [nbMulti; c; cFor "i" ~body:[cArrayWrite "D"]]; Instr.gather_targets [c; cStrict; cArrayWrite "D"]; Loop.fusion_targets ~into:FuseIntoLast [nbMulti; c; cFor ~stop:[cVar "kn"] "i"]; Instr.gather_targets [c; cFor "i"; cArrayWrite "D"]; );✔
  14. Cleanup.std ~arith_simpl:Arith.([expand; euclidian; gather_rec]) (); )✔
tmp/{before9c7231.cpp → after3f8776.cpp} RENAMED
@@ -1,33 +1,110 @@
1
  #include <optitrust.h>
2
 
3
  typedef uint8_t T;
4
 
5
  typedef uint16_t ST;
6
 
7
  void rowSum(const int kn, const uint8_t* S, uint16_t* D, const int n,
8
  const int cn) {
 
9
- __requires("__is_geq(kn, 0)");
10
- __requires("__is_geq(n, 1)");
11
- __requires("__is_geq(cn, 0)");
12
- __modifies("D ~> Matrix2(n, cn)");
13
- __reads("S ~> Matrix2(n + kn - 1, cn)");
 
 
 
 
 
 
 
 
 
 
 
 
 
 
14
- for (int i = 0; i < n; i++) {
 
 
 
 
15
- __sreads("S ~> Matrix2(n + kn - 1, cn)");
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
16
- __xmodifies("for c in 0..cn -> &D[MINDEX2(n, cn, i, c)] ~> Cell");
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
17
  for (int c = 0; c < cn; c++) {
18
- __sreads("S ~> Matrix2(n + kn - 1, cn)");
19
- __xmodifies("&D[MINDEX2(n, cn, i, c)] ~> Cell");
20
- __ghost(assume, "F := is_subrange(i..i + kn, 0..n + kn - 1)");
21
- uint16_t s = 0;
22
- for (int k = i; k < i + kn; k++) {
23
- __ghost(in_range_extend,
24
- "x := k, r1 := i..i + kn, r2 := 0..n + kn - 1");
25
- const __ghost_fn focus =
26
- __ghost_begin(matrix2_ro_focus, "M := S, i := k, j := c");
27
- s += S[MINDEX2(n + kn - 1, cn, k, c)];
28
- __ghost_end(focus);
29
- }
 
 
 
 
30
- D[MINDEX2(n, cn, i, c)] = s;
 
 
 
 
31
  }
 
32
  }
33
  }
1
  #include <optitrust.h>
2
 
3
  typedef uint8_t T;
4
 
5
  typedef uint16_t ST;
6
 
7
  void rowSum(const int kn, const uint8_t* S, uint16_t* D, const int n,
8
  const int cn) {
9
+ if (kn == 3) /*@kn*/ {
10
+ for (int ic = 0; ic < n * cn; ic++) {
 
 
11
+ D[ic] = (uint16_t)S[ic] + (uint16_t)S[ic % cn + (1 + ic / cn) * cn] +
12
+ (uint16_t)S[ic % cn + (2 + ic / cn) * cn];
13
+ }
14
+ } /*kn@*/
15
+ else {
16
+ if (kn == 5) /*@kn*/ {
17
+ for (int ic = 0; ic < n * cn; ic++) {
18
+ D[ic] = (uint16_t)S[ic] + (uint16_t)S[ic % cn + (1 + ic / cn) * cn] +
19
+ (uint16_t)S[ic % cn + (2 + ic / cn) * cn] +
20
+ (uint16_t)S[ic % cn + (3 + ic / cn) * cn] +
21
+ (uint16_t)S[ic % cn + (4 + ic / cn) * cn];
22
+ }
23
+ } /*kn@*/
24
+ else /*@nokn*/ {
25
+ if (cn == 1) /*@cn*/ {
26
+ uint16_t s = (uint16_t)0;
27
+ for (int i = 0; i < kn; i++) {
28
+ s += (uint16_t)S[i];
29
+ }
30
+ D[0] = s;
31
+ for (int i = 1; i < n; i++) {
32
+ s = s + (uint16_t)S[-1 + i + kn] - (uint16_t)S[-1 + i];
33
+ D[i] = s;
34
+ }
35
+ } /*cn@*/
36
+ else {
37
+ if (cn == 3) /*@cn*/ {
38
+ uint16_t s = (uint16_t)0;
39
+ uint16_t s2 = (uint16_t)0;
40
+ uint16_t s3 = (uint16_t)0;
41
+ for (int i = 0; i < kn; i++) {
42
+ s += (uint16_t)S[3 * i];
43
+ s2 += (uint16_t)S[1 + 3 * i];
44
+ s3 += (uint16_t)S[2 + 3 * i];
45
+ }
46
+ D[0] = s;
47
+ D[1] = s2;
48
+ D[2] = s3;
49
+ for (int i = 1; i < n; i++) {
50
+ s = s + (uint16_t)S[3 * -1 + 3 * i + 3 * kn] -
51
+ (uint16_t)S[3 * -1 + 3 * i];
52
+ s2 = s2 + (uint16_t)S[1 + 3 * (-1 + i + kn)] -
53
+ (uint16_t)S[1 + 3 * (-1 + i)];
54
+ s3 = s3 + (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] = s2;
58
+ D[2 + 3 * i] = s3;
59
+ }
60
+ } /*cn@*/
61
+ else {
62
+ if (cn == 4) /*@cn*/ {
63
+ uint16_t s = (uint16_t)0;
64
+ uint16_t s4 = (uint16_t)0;
65
+ uint16_t s5 = (uint16_t)0;
66
+ uint16_t s6 = (uint16_t)0;
67
+ for (int i = 0; i < kn; i++) {
68
+ s += (uint16_t)S[4 * i];
69
+ s4 += (uint16_t)S[1 + 4 * i];
70
+ s5 += (uint16_t)S[2 + 4 * i];
71
+ s6 += (uint16_t)S[3 + 4 * i];
72
+ }
73
+ D[0] = s;
74
+ D[1] = s4;
75
+ D[2] = s5;
76
+ D[3] = s6;
77
+ for (int i = 1; i < n; i++) {
78
+ s = s + (uint16_t)S[4 * -1 + 4 * i + 4 * kn] -
79
+ (uint16_t)S[4 * -1 + 4 * i];
80
+ s4 = s4 + (uint16_t)S[1 + 4 * (-1 + i + kn)] -
81
+ (uint16_t)S[1 + 4 * (-1 + i)];
82
+ s5 = s5 + (uint16_t)S[2 + 4 * (-1 + i + kn)] -
83
+ (uint16_t)S[2 + 4 * (-1 + i)];
84
+ s6 = s6 + (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] = s4;
88
+ D[2 + 4 * i] = s5;
89
+ D[3 + 4 * i] = s6;
90
+ }
91
+ } /*cn@*/
92
+ else {
93
  for (int c = 0; c < cn; c++) {
 
 
 
94
+ uint16_t s = (uint16_t)0;
95
+ for (int i = 0; i < kn; i++) {
 
 
 
 
96
+ 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
+ }
105
+ }
106
+ }
107
  }
108
+ } /*nokn@*/
109
  }
110
  }
 Show: