Merge pull request #30 from charguer/dot-rename

Rename vectvectmul to dot (product), improve a few things

Author: Bastacyclop

case_studies/vectvectmul/vectvectmul.cpp case_studies/dot_product/dot.cppcase_studies/vectvectmul/vectvectmul.cpp renamed to case_studies/dot_product/dot.cpp

@@ -8,7 +8,7 @@ __DEF(matmul, "fun (A B: int * int -> float) (p: int) -> fun (i j: int) -> reduc
 /* Multiplies the vect A (dim n) by the vector B (dim n),
  * and returns the result of the scalar product.
 */
-float vect_vect_mul(float* a, float* b, int n) { // todo: requires divides
+float dot(float* a, float* b, int n) { // todo: requires divides
   __requires("A: int -> float, B: int -> float");
   __reads("a ~> Matrix1(n, A), b ~> Matrix1(n, B)");
   __ensures("_Res =. reduce_sum(n, fun j -> A(j) *. B(j))");
@@ -21,8 +21,8 @@ float vect_vect_mul(float* a, float* b, int n) { // todo: requires divides
     s += a[MINDEX1(n,i)] * b[MINDEX1(n,i)];
     __GHOST_END(focusA);
     __GHOST_END(focusB);
-    __ghost(in_range_bounds, "i", "i_gt_0 <- lower_bound");
-    __ghost(rewrite_float_linear, "inside := fun v -> &s ~~> v, by := reduce_sum_add_right(i, fun j -> A(j) *. B(j), i_gt_0)");
+    __ghost(in_range_bounds, "i", "i_ge_0 <- lower_bound");
+    __ghost(rewrite_float_linear, "inside := fun v -> &s ~~> v, by := reduce_sum_add_right(i, fun j -> A(j) *. B(j), i_ge_0)");
   }
   __ghost(eq_refl_float, "reduce_sum(n, fun j -> A(j) *. B(j))");
   return s;

case_studies/vectvectmul/vectvectmul.ml case_studies/dot_product/dot.mlcase_studies/vectvectmul/vectvectmul.ml renamed to case_studies/dot_product/dot.ml

@@ -20,32 +20,36 @@ let _ = if part = 1 then Run.script_cpp (fun () ->
   !! Loop.tile (int 32) ~index:"bi" ~bound:TileDivides [cFor "i"];
 
   (* LATER: !! Variable.local_name ~var:"s" ~local_var:"t" [tSpanSeq [cForBody "bi"]]; *)
-  !! Sequence.intro ~mark:"t_scope" ~start:[tFirst; cForBody "bi"] ~stop:[tLast; cForBody "bi"] ();
-  !! Variable.local_name ~var:"s" ~local_var:"t" [cMark "t_scope"];
-  !! Sequence.elim [cMark "t_scope"];
+  !! (
+    Sequence.intro ~mark:"t_scope" ~start:[tFirst; cForBody "bi"] ~stop:[tLast; cForBody "bi"] ();
+    Variable.local_name ~var:"s" ~local_var:"t" [cMark "t_scope"];
+    Sequence.elim [cMark "t_scope"];
+  );
 
   (* DEPRECATED? !! Sequence_basic.insert (trm_let (new_var "d", typ_f32) (trm_get (trm_find_var "s" []))) [tFirst; cForBody "bi"]; *)
-  !! Variable.insert ~name:"d" ~typ:typ_f32 ~value:(trm_get (trm_find_var "s" [])) [cForBody "bi"; tFirst];
+  !! (
+    Variable.insert ~name:"d" ~typ:typ_f32 ~value:(trm_get (trm_find_var "s" [])) [cForBody "bi"; tFirst];
 
-  (* at this line, the output is the equivalent of vectvectmul0_gen.cpp,
+  (* at this line, the output is the equivalent of dot0_gen.cpp,
     beware that "==" needs to be replaced with "=." and all the "__is_true" must be removed;
     some +. and + need to be fixed
-    ----> LATER: tweak display so that the output of _after.cpp is exactly  vectvectmul0.cpp *)
+    ----> LATER: tweak display so that the output of _after.cpp is exactly  dot0.cpp *)
 (* )
 
 (* Part 2: *)
 let _ = if part = 2 then Run.script_cpp ~filename:"vv1.cpp" (fun () ->
 *)
   (* Why nbMulti? !! Accesses.shift_var ~inv:true ~factor:(trm_find_var "d" []) [nbMulti; cVarDef "t"]; *)
-  !! Accesses.shift_var ~inv:true ~factor:(trm_find_var "d" []) [cFor "bi"; cVarDef "t"];
-  !! Variable.inline [cVarDef "d"];
-  !! Arith.simpl_surrounding_expr Arith.gather_rec [nbMulti; cVar "s"];
+    Accesses.shift_var ~inv:true ~factor:(trm_find_var "d" []) [cFor "bi"; cVarDef "t"];
+    Variable.inline [cVarDef "d"];
+    Arith.simpl_surrounding_expr Arith.gather_rec [nbMulti; cVar "s"];
+  );
 (* )
 
 (* Part 3: *)
 let _ = if part = 3 then Run.script_cpp ~filename:"vv2.cpp" (fun () ->
 *)
-  !! Resources.loop_minimize [cFor "i"];
+  (* !! Resources.loop_minimize [cFor "i"]; *)
 
   !! Loop.hoist [cVarDef "t"];
   !! Loop.fission [tBefore; cFor "bi"; cWriteVar "s"];

case_studies/vectvectmul/vectvectmul0.cpp case_studies/dot_product/dot0.cppcase_studies/vectvectmul/vectvectmul0.cpp renamed to case_studies/dot_product/dot0.cpp

@@ -19,7 +19,7 @@ __ghost(define,
         "fun (i: int) (j: int) -> reduce_sum(p, fun k -> A(i, k) *. B(k, j))",
         "matmul <- x");
 
-float vect_vect_mul(float* a, float* b, int n) {
+float dot(float* a, float* b, int n) {
   __requires("A: int -> float");
   __requires("B: int -> float");
   __ensures("(_Res =. reduce_sum(n, fun j -> A(j) *. B(j)))");

case_studies/vectvectmul/vectvectmul1.cpp case_studies/dot_product/dot1.cppcase_studies/vectvectmul/vectvectmul1.cpp renamed to case_studies/dot_product/dot1.cpp

@@ -19,7 +19,7 @@ __ghost(define,
         "fun (i: int) (j: int) -> reduce_sum(p, fun k -> A(i, k) *. B(k, j))",
         "matmul <- x");
 
-float vect_vect_mul(float* a, float* b, int n) {
+float dot(float* a, float* b, int n) {
   __requires("A: int -> float");
   __requires("B: int -> float");
   __ensures("(_Res =. reduce_sum(n, fun j -> A(j) *. B(j)))");

case_studies/vectvectmul/vectvectmul2.cpp case_studies/dot_product/dot2.cppcase_studies/vectvectmul/vectvectmul2.cpp renamed to case_studies/dot_product/dot2.cpp

@@ -19,7 +19,7 @@ __ghost(define,
         "fun (i: int) (j: int) -> reduce_sum(p, fun k -> A(i, k) *. B(k, j))",
         "matmul <- x");
 
-float vect_vect_mul(float* a, float* b, int n) {
+float dot(float* a, float* b, int n) {
   __requires("A: int -> float");
   __requires("B: int -> float");
   __ensures("(_Res =. reduce_sum(n, fun j -> A(j) *. B(j)))");

case_studies/dot_product/dot_exp.cpp

@@ -0,0 +1,36 @@
+#include <optitrust_models.h>
+
+#include "omp.h"
+
+float dot(float* a, float* b, int n) {
+  float s = 0.f;
+  float* const t = (float*)malloc(exact_div(n, 32) * sizeof(float));
+#pragma omp parallel for
+  for (int bi = 0; bi < exact_div(n, 32); bi++) {
+    t[bi] = ({
+      float arith_res = 0;
+      const float arith_res1 = arith_res;
+      arith_res1;
+    });
+    for (int i = 0; i < 32; i++) {
+      t[bi] = ({
+        float arith_res = a[32 * bi + i] * b[32 * bi + i] + t[bi];
+        const float arith_res2 = arith_res;
+        arith_res2;
+      });
+    }
+  }
+  for (int bi = 0; bi < exact_div(n, 32); bi++) {
+    s = ({
+      float get = ({
+        float arith_res = t[bi] + s;
+        const float arith_res3 = arith_res;
+        arith_res3;
+      });
+      const float getc = get;
+      getc;
+    });
+  }
+  free(t);
+  return s;
+}

case_studies/vectvectmul/vv1.cpp case_studies/dot_product/vv1.cppcase_studies/vectvectmul/vv1.cpp renamed to case_studies/dot_product/vv1.cpp

@@ -18,7 +18,7 @@ __ghost(define,
         "fun (i: int) (j: int) -> reduce_sum(p, fun k -> A(i, k) *. B(k, j))",
         "matmul <- x");
 
-float vect_vect_mul(float* a, float* b, int n) {
+float dot(float* a, float* b, int n) {
   __requires("A: int -> float");
   __requires("B: int -> float");
   __ensures("_Res =. reduce_sum(n, fun j -> A(j) *. B(j))");

case_studies/vectvectmul/vv2.cpp case_studies/dot_product/vv2.cppcase_studies/vectvectmul/vv2.cpp renamed to case_studies/dot_product/vv2.cpp

@@ -18,7 +18,7 @@ __ghost(define,
         "fun (i: int) (j: int) -> reduce_sum(p, fun k -> A(i, k) *. B(k, j))",
         "matmul <- x");
 
-float vect_vect_mul(float* a, float* b, int n) {
+float dot(float* a, float* b, int n) {
   __requires("A: int -> float");
   __requires("B: int -> float");
   __ensures("_Res =. reduce_sum(n, fun j -> A(j) *. B(j))");

include/optitrust_common.h

@@ -307,7 +307,7 @@ __GHOST(in_range_shift_extend) {
 __GHOST(in_range_bounds) {
   __requires("x: int, a: int, b: int, s: int");
   __requires("in_range(x, range(a, b, s)), s >= 0");
-  __ensures("lower_bound: x >= a, upper_bound: x <= b");
+  __ensures("lower_bound: x >= a, upper_bound: x < b");
   __admitted();
 }