7 files changed, 678 insertions, 0 deletions
diff --git a/benchmarks/polybench-syn-div/stencils/Makefile b/benchmarks/polybench-syn-div/stencils/Makefile
new file mode 100644
index 0000000..d2e1c9b
--- /dev/null
+++ b/benchmarks/polybench-syn-div/stencils/Makefile
@@ -0,0 +1,6 @@
+TARGETS := adi fdtd-2d heat-3d jacobi-1d jacobi-2d seidel-2d
+
+include ../common.mk
+
+adi.v: adi.c
+	$(VERICERT) $(VERICERT_OPTS) -O0 -finline $< -o $@
diff --git a/benchmarks/polybench-syn-div/stencils/adi.c b/benchmarks/polybench-syn-div/stencils/adi.c
new file mode 100644
index 0000000..be2b766
--- /dev/null
+++ b/benchmarks/polybench-syn-div/stencils/adi.c
@@ -0,0 +1,125 @@
+/**
+ * This version is stamped on May 10, 2016
+ *
+ * Contact:
+ *   Louis-Noel Pouchet <pouchet.ohio-state.edu>
+ *   Tomofumi Yuki <tomofumi.yuki.fr>
+ *
+ * Web address: http://polybench.sourceforge.net
+ */
+/* adi.c: this file is part of PolyBench/C */
+
+#ifndef SYNTHESIS
+#include <stdio.h>
+#endif 
+
+static
+void init_array (int n, int u[ 20 + 0][20 + 0])
+{
+  int i, j;
+
+  for (i = 0; i < n; i++)
+    for (j = 0; j < n; j++)
+    {
+      u[i][j] = (((int)(i + n-j)) / n);
+    }
+}
+
+
+
+
+static
+int print_array(int n, int u[ 20 + 0][20 + 0])
+{
+  int i, j;
+  int res = 0;
+
+  for (i = 0; i < n; i++)
+    for (j = 0; j < n; j++) {
+      res ^= u[i][j];
+    }
+#ifndef SYNTHESIS
+  printf("finished: %u\n", res);
+#endif
+
+  return res;
+}
+static
+void kernel_adi(int tsteps, int n,
+                int u[ 20 + 0][20 + 0],
+                int v[ 20 + 0][20 + 0],
+                int p[ 20 + 0][20 + 0],
+                int q[ 20 + 0][20 + 0])
+{
+  int t, i, j;
+  int B1, B2;
+  int mul1, mul2;
+  int a, b, c, d, e, f;
+
+  B1 = 2;
+  B2 = 1;
+  mul1 = ((B1 * n * n) / tsteps);
+  mul2 = ((B2 * n * n) /tsteps);
+
+  a = -((mul1 / 2));
+  b = 1+mul1;
+  c = a;
+  d = -((mul2 / 2));
+  e = 1+mul2;
+  f = d;
+  int ZERO = 0;
+
+  for (t=1; t<=tsteps; t++) {
+
+    for (i=1; i<n-1; i++) {
+      v[ZERO][i] = 1;
+      p[i][ZERO] = 0;
+      q[i][ZERO] = v[ZERO][i];
+      for (j=1; j<n-1; j++) {
+        p[i][j] = -(c / (a*p[i][j-1]+b));
+        q[i][j] = -((-d*u[j][i-1]+(1+2*d)*u[j][i] - f*u[j][i+1]-a*q[i][j-1]) / (a*p[i][j-1]+b));
+      }
+
+      v[n-1][i] = 1;
+      for (j=n-2; j>=1; j--) {
+        v[j][i] = p[i][j] * v[j+1][i] + q[i][j];
+      }
+    }
+
+    for (i=1; i<n-1; i++) {
+      u[i][ZERO] = 1;
+      p[i][ZERO] = 0;
+      q[i][ZERO] = u[i][ZERO];
+      for (j=1; j<n-1; j++) {
+        p[i][j] = -(f / (d*p[i][j-1]+e));
+        q[i][j] = ((-a*v[i-1][j]+(1+2*a)*v[i][j] - c*v[i+1][j]-d*q[i][j-1]) / (d*p[i][j-1]+e));
+      }
+      u[i][n-1] = 1;
+      for (j=n-2; j>=1; j--) {
+        u[i][j] = p[i][j] * u[i][j+1] + q[i][j];
+      }
+    }
+  }
+}
+
+int main()
+{
+
+  int n = 20;
+  int tsteps = 20;
+
+
+  int u[20 + 0][20 + 0]; 
+  int v[20 + 0][20 + 0]; 
+  int p[20 + 0][20 + 0]; 
+  int q[20 + 0][20 + 0]; 
+
+
+
+  init_array (n, u);
+
+  kernel_adi (tsteps, n, u, v, p, q);
+
+  return print_array(n, u);
+
+}
diff --git a/benchmarks/polybench-syn-div/stencils/fdtd-2d.c b/benchmarks/polybench-syn-div/stencils/fdtd-2d.c
new file mode 100644
index 0000000..2c5cdb2
--- /dev/null
+++ b/benchmarks/polybench-syn-div/stencils/fdtd-2d.c
@@ -0,0 +1,134 @@
+/**
+ * This version is stamped on May 10, 2016
+ *
+ * Contact:
+ *   Louis-Noel Pouchet <pouchet.ohio-state.edu>
+ *   Tomofumi Yuki <tomofumi.yuki.fr>
+ *
+ * Web address: http://polybench.sourceforge.net
+ */
+/* fdtd-2d.c: this file is part of PolyBench/C */
+
+#ifndef SYNTHESIS
+#include <stdio.h>
+#endif
+
+#define plus(i) i = i + ONE
+static
+void init_array (int tmax,
+   int nx,
+   int ny,
+   int ex[ 20 + 0][30 + 0],
+   int ey[ 20 + 0][30 + 0],
+   int hz[ 20 + 0][30 + 0],
+   int _fict_[ 20 + 0])
+{
+  int i, j;
+  int ONE = 1;
+
+  for (i = 0; i < tmax; plus(i))
+    _fict_[i] = (int) i;
+  for (i = 0; i < nx; plus(i))
+    for (j = 0; j < ny; plus(j))
+    {
+      ex[i][j] = ((i*(j+1)) / nx);
+      ey[i][j] = ((i*(j+2)) / ny);
+      hz[i][j] = ((i*(j+3)) / nx);
+    }
+      
+}
+
+
+
+
+static
+int print_array(int nx,
+   int ny,
+   int ex[ 20 + 0][30 + 0],
+   int ey[ 20 + 0][30 + 0],
+   int hz[ 20 + 0][30 + 0])
+{
+  int i, j;
+  int res = 0;
+  int ONE = 1;
+
+  for (i = 0; i < nx; plus(i))
+    for (j = 0; j < ny; plus(j)) {
+      res ^= ex[i][j];
+    }
+  for (i = 0; i < nx; plus(i))
+    for (j = 0; j < ny; plus(j)) {
+      res ^= ey[i][j];
+    }
+  for (i = 0; i < nx; plus(i))
+    for (j = 0; j < ny; plus(j)) {
+      res ^= hz[i][j];
+    }
+
+#ifndef SYNTHESIS
+  printf("finished: %u\n", res);
+#endif
+
+  return res;
+}
+
+
+static
+void kernel_fdtd_2d(int tmax,
+      int nx,
+      int ny,
+      int ex[ 20 + 0][30 + 0],
+      int ey[ 20 + 0][30 + 0],
+      int hz[ 20 + 0][30 + 0],
+      int _fict_[ 20 + 0])
+{
+  int t, i, j;
+  int ONE = 1;
+
+ for(t = 0; t < tmax; t=t+ONE)
+    {
+      for (j = 0; j < ny; plus(j))
+ ey[0][j] = _fict_[t];
+      for (i = 1; i < nx; plus(i))
+ for (j = 0; j < ny; plus(j))
+   ey[i][j] = ey[i][j] - ((hz[i][j]-((hz[i-ONE][j])>>1)));
+      for (i = 0; i < nx; plus(i))
+ for (j = 1; j < ny; plus(j))
+   ex[i][j] = ex[i][j] - ((hz[i][j]-((hz[i][j-ONE])>>1)));
+      for (i = 0; i < nx - ONE; plus(i))
+ for (j = 0; j < ny - ONE; plus(j)){
+   int tmp = (ex[i][j+ONE] - ex[i][j] +
+           ey[i+ONE][j] - ey[i][j]);
+   hz[i][j] = hz[i][j] - (tmp >> 1) - (tmp >> 2);
+           }
+    }
+
+}
+
+
+int main()
+{
+
+  int tmax = 20;
+  int nx = 20;
+  int ny = 30;
+
+
+  int ex[20 + 0][30 + 0]; 
+  int ey[20 + 0][30 + 0]; 
+  int hz[20 + 0][30 + 0]; 
+  int _fict_[20 + 0];     
+
+  init_array (tmax, nx, ny,
+       ex,
+       ey,
+       hz,
+       _fict_);
+  kernel_fdtd_2d (tmax, nx, ny,
+    ex,
+    ey,
+    hz,
+    _fict_);
+
+  return print_array(nx, ny, ex, ey, hz);
+}
diff --git a/benchmarks/polybench-syn-div/stencils/heat-3d.c b/benchmarks/polybench-syn-div/stencils/heat-3d.c
new file mode 100644
index 0000000..f93082e
--- /dev/null
+++ b/benchmarks/polybench-syn-div/stencils/heat-3d.c
@@ -0,0 +1,112 @@
+/**
+ * This version is stamped on May 10, 2016
+ *
+ * Contact:
+ *   Louis-Noel Pouchet <pouchet.ohio-state.edu>
+ *   Tomofumi Yuki <tomofumi.yuki.fr>
+ *
+ * Web address: http://polybench.sourceforge.net
+ */
+/* heat-3d.c: this file is part of PolyBench/C */
+
+#include "../include/misc.h"
+
+#ifndef SYNTHESIS
+#include <stdio.h>
+#endif
+
+#define plus(i) i = i + ONE
+static
+void init_array (int n,
+   int A[ 10 + 0][10 + 0][10 + 0],
+   int B[ 10 + 0][10 + 0][10 + 0])
+{
+  int i, j, k;
+  int ONE = 1;
+
+  for (i = 0; i < n; plus(i))
+    for (j = 0; j < n; plus(j))
+      for (k = 0; k < n; plus(k))
+        A[i][j][k] = B[i][j][k] = (int) (i + j + (n-k))* (10 / n);
+}
+
+
+
+
+static
+int print_array(int n,
+   int A[ 10 + 0][10 + 0][10 + 0])
+
+{
+  int i, j, k;
+  int ONE = 1;
+  int res = 0;
+
+  for (i = 0; i < n; plus(i))
+    for (j = 0; j < n; plus(j))
+      for (k = 0; k < n; plus(k)) {
+         res ^= A[i][j][k];
+      }
+#ifndef SYNTHESIS
+  printf("finished %u\n", res);
+#endif
+    return res;
+}
+
+
+
+
+static
+void kernel_heat_3d(int tsteps,
+        int n,
+        int A[ 10 + 0][10 + 0][10 + 0],
+        int B[ 10 + 0][10 + 0][10 + 0])
+{
+  int t, i, j, k;
+  int ONE = 1;
+  int TWO = 2;
+
+ for (t = 1; t <= 5; plus(t)) {
+        for (i = 1; i < n-ONE; plus(i)) {
+            for (j = 1; j < n-ONE; plus(j)) {
+                for (k = 1; k < n-ONE; plus(k)) {
+                    B[i][j][k] = ((A[i+ONE][j][k] - TWO * A[i][j][k] + A[i-ONE][j][k]) >> 4) 
+                                 + ((A[i][j+ONE][k] - TWO * A[i][j][k] + A[i][j-ONE][k]) >> 4)
+                                 + ((A[i][j][k+ONE] - TWO * A[i][j][k] + A[i][j][k-ONE]) >> 4)
+                                 + A[i][j][k]
+                                    ;
+                }
+            }
+        }
+        for (i = 1; i < n-ONE; plus(i)) {
+           for (j = 1; j < n-ONE; plus(j)) {
+               for (k = 1; k < n-ONE; plus(k)) {
+                   A[i][j][k] = ((B[i+ONE][j][k] - TWO * B[i][j][k] + B[i-ONE][j][k]) >> 4 )
+                                + ((B[i][j+ONE][k] - TWO * B[i][j][k] + B[i][j-ONE][k]) >> 4 )
+                                + ((B[i][j][k+ONE] - TWO * B[i][j][k] + B[i][j][k-ONE]) >> 4 )
+                                + B[i][j][k];
+                                    //;
+               }
+           }
+       }
+    }
+}
+
+
+int main()
+{
+
+  int n = 10;
+  int tsteps = 20;
+
+
+  int A[10 + 0][10 + 0][10 + 0];
+  int B[10 + 0][10 + 0][10 + 0];
+
+  init_array (n, A, B);
+
+  kernel_heat_3d (tsteps, n, A, B);
+
+  return print_array(n, A);
+
+}
diff --git a/benchmarks/polybench-syn-div/stencils/jacobi-1d.c b/benchmarks/polybench-syn-div/stencils/jacobi-1d.c
new file mode 100644
index 0000000..993773e
--- /dev/null
+++ b/benchmarks/polybench-syn-div/stencils/jacobi-1d.c
@@ -0,0 +1,101 @@
+/**
+ * This version is stamped on May 10, 2016
+ *
+ * Contact:
+ *   Louis-Noel Pouchet <pouchet.ohio-state.edu>
+ *   Tomofumi Yuki <tomofumi.yuki.fr>
+ *
+ * Web address: http://polybench.sourceforge.net
+ */
+/* jacobi-1d.c: this file is part of PolyBench/C */
+
+#ifndef SYNTHESIS
+#include <stdio.h>
+#endif
+
+#define plus(i) i = i + ONE
+static
+void init_array (int n,
+   int A[ 30 + 0],
+   int B[ 30 + 0])
+{
+  int i;
+  int ONE = 1;
+  int TWO = 2;
+  int THREE = 3;
+
+  for (i = 0; i < n; plus(i))
+      {
+        A[i] = (((int) i+TWO) / n);
+        B[i] = (((int) i+THREE) / n);
+      }
+}
+
+
+
+
+static
+int print_array(int n,
+   int A[ 30 + 0])
+
+{
+  int i;
+  int ONE = 1;
+  int res = 0;
+
+  for (i = 0; i < n; plus(i))
+    {
+      res ^= A[i];
+    }
+#ifndef SYNTHESIS
+  printf("finished %u\n", res);
+#endif
+    return res;
+}
+
+
+
+
+static
+void kernel_jacobi_1d(int tsteps,
+       int n,
+       int A[ 30 + 0],
+       int B[ 30 + 0])
+{
+  int t, i;
+  int ONE = 1;
+
+  for (t = 0; t < tsteps; plus(t))
+  {
+    for (i = 1; i < n - ONE; plus(i)){
+      B[i] = (A[i-ONE] + A[i] + A[i + ONE]);
+      B[i] = B[i] >> 2;
+    }
+    for (i = 1; i < n - ONE; plus(i)){
+      A[i] = (B[i-ONE] + B[i] + B[i + ONE]);
+      A[i] = A[i] >> 2;
+    }
+  }
+
+}
+
+
+int main()
+{
+
+  int n = 30;
+  int tsteps = 20;
+
+
+  int A[30 + 0]; 
+  int B[30 + 0]; 
+
+
+
+  init_array (n, A, B);
+
+  kernel_jacobi_1d(tsteps, n, A, B);
+
+  return print_array(n, A);
+
+}
diff --git a/benchmarks/polybench-syn-div/stencils/jacobi-2d.c b/benchmarks/polybench-syn-div/stencils/jacobi-2d.c
new file mode 100644
index 0000000..bb6afec
--- /dev/null
+++ b/benchmarks/polybench-syn-div/stencils/jacobi-2d.c
@@ -0,0 +1,108 @@
+/**
+ * This version is stamped on May 10, 2016
+ *
+ * Contact:
+ *   Louis-Noel Pouchet <pouchet.ohio-state.edu>
+ *   Tomofumi Yuki <tomofumi.yuki.fr>
+ *
+ * Web address: http://polybench.sourceforge.net
+ */
+/* jacobi-2d.c: this file is part of PolyBench/C */
+
+#include "../include/misc.h"
+
+#ifndef SYNTHESIS
+#include <stdio.h>
+#endif
+
+
+#define plus(i) i = i + ONE
+static
+void init_array (int n,
+   int A[ 30 + 0][30 + 0],
+   int B[ 30 + 0][30 + 0])
+{
+  int i, j;
+  int ONE = 1;
+  int TWO = 2;
+  int THREE = 3;
+
+  for (i = 0; i < n; plus(i))
+    for (j = 0; j < n; plus(j))
+      {
+        A[i][j] = (((int) i*(j+TWO) + TWO) / n);
+        B[i][j] = (((int) i*(j+THREE) + THREE) / n);
+      }
+}
+
+
+
+
+static
+int print_array(int n,
+   int A[ 30 + 0][30 + 0])
+
+{
+  int i, j;
+  int ONE = 1;
+  int res = 0;
+
+  for (i = 0; i < n; plus(i))
+    for (j = 0; j < n; plus(j)) {
+      res ^= A[i][j];
+    }
+#ifndef SYNTHESIS
+  printf("finished %u\n", res);
+#endif
+    return res;
+}
+
+
+
+
+static
+void kernel_jacobi_2d(int tsteps,
+       int n,
+       int A[ 30 + 0][30 + 0],
+       int B[ 30 + 0][30 + 0])
+{
+  int t, i, j;
+  int ONE = 1;
+  int TWO = 2;
+
+  for (t = 0; t < tsteps; plus(t))
+  {
+    for (i = 1; i < n - ONE; plus(i))
+      for (j = 1; j < n - ONE; plus(j)){
+        B[i][j] = (A[i][j] + A[i][j-ONE] + A[i][ONE+j] + A[ONE+i][j] + A[i-ONE][j]);
+        B[i][j] = B[i][j] >> TWO;
+      }
+    for (i = 1; i < n - ONE; plus(i))
+      for (j = 1; j < n - ONE; plus(j)){
+        A[i][j] = (B[i][j] + B[i][j-ONE] + B[i][ONE+j] + B[ONE+i][j] + B[i-ONE][j]);
+        A[i][j] = A[i][j] >> TWO; 
+      }
+  }
+
+}
+
+
+int main()
+{
+
+  int n = 30;
+  int tsteps = 5;
+
+
+  int A[30 + 0][30 + 0];
+  int B[30 + 0][30 + 0];
+
+
+
+  init_array (n, A, B);
+
+  kernel_jacobi_2d(tsteps, n, A, B);
+
+  return print_array(n, A);
+
+}
diff --git a/benchmarks/polybench-syn-div/stencils/seidel-2d.c b/benchmarks/polybench-syn-div/stencils/seidel-2d.c
new file mode 100644
index 0000000..4a3b1ac
--- /dev/null
+++ b/benchmarks/polybench-syn-div/stencils/seidel-2d.c
@@ -0,0 +1,92 @@
+/**
+ * This version is stamped on May 10, 2016
+ *
+ * Contact:
+ *   Louis-Noel Pouchet <pouchet.ohio-state.edu>
+ *   Tomofumi Yuki <tomofumi.yuki.fr>
+ *
+ * Web address: http://polybench.sourceforge.net
+ */
+/* seidel-2d.c: this file is part of PolyBench/C */
+
+#include "../include/misc.h"
+
+#ifndef SYNTHESIS
+#include <stdio.h>
+#endif
+
+#define plus(i) i = i + ONE
+static
+void init_array (int n,
+   int A[ 40 + 0][40 + 0])
+{
+  int i, j;
+  int ONE = 1;
+  int TWO = 2;
+
+  for (i = 0; i < n; plus(i))
+    for (j = 0; j < n; plus(j))
+      A[i][j] = (((int) i*(j+TWO) + TWO) / n);
+}
+
+
+
+
+static
+int print_array(int n,
+   int A[ 40 + 0][40 + 0])
+
+{
+  int i, j;
+  int ONE = 1;
+  int res = 0;
+
+  for (i = 0; i < n; plus(i))
+    for (j = 0; j < n; plus(j)) {
+      res ^= A[i][j];
+    }
+#ifndef SYNTHESIS
+  printf("finished %u\n", res);
+#endif
+  return res;
+}
+
+
+
+
+static
+void kernel_seidel_2d(int tsteps,
+        int n,
+        int A[ 40 + 0][40 + 0])
+{
+  int t, i, j;
+  int ONE = 1;
+  int TWO = 2;
+  int NINE = 9;
+
+ for (t = 0; t <= tsteps - ONE; plus(t))
+    for (i = ONE; i<= n - TWO; plus(i))
+      for (j = ONE; j <= n - TWO; plus(j))
+ A[i][j] = ((A[i-ONE][j-ONE] + A[i-ONE][j] + A[i-ONE][j+ONE]
+     + A[i][j-ONE] + A[i][j] + A[i][j+ONE]
+     + A[i+ONE][j-ONE] + A[i+ONE][j] + A[i+ONE][j+ONE]) / NINE);
+
+}
+
+
+int main()
+{
+
+  int n = 40;
+  int tsteps = 5;
+
+
+  int A[40 + 0][40 + 0]; 
+
+  init_array (n, A);
+
+  kernel_seidel_2d (tsteps, n, A);
+
+  return print_array(n, A);
+
+}