Add benchmarking of unhashed commandsdebug/unhashed

3 files changed, 235 insertions, 38 deletions

diff --git a/debug/vericertTest.ml b/debug/vericertTest.ml
index a67d30d..4733c2c 100644
--- a/debug/vericertTest.ml
+++ b/debug/vericertTest.ml
@@ -16,6 +16,8 @@ open Integers
 open Op
 open Printf
 
+let _ = Clflags.option_timings := true
+
 let schedule_oracle l bb bbt =
   match abstract_sequence_top bb with
   | Some p ->
@@ -34,6 +36,24 @@ let schedule_oracle l bb bbt =
      | None -> (printf "FAILED1\n"; false))
   | None -> (printf "FAILED2\n"; false)
 
+let schedule_oracle' l bb bbt =
+  match abstract_sequence_top bb with
+  | Some p ->
+    let (p0, m_expr) = p in
+    let (bb', reg_expr) = p0 in
+    (match abstract_sequence_top (concat (concat bbt)) with
+     | Some p1 ->
+       let (p2, m_expr_t) = p1 in
+       let (bbt', reg_expr_t) = p2 in
+       printf "F1:\n%a\n" PrintAbstr.print_forest bb';
+       printf "F2:\n%a\n" PrintAbstr.print_forest bbt'; flush stdout;
+       (&&)
+         ((&&) ((&&) (if check [] bb' bbt' then true else (Printf.printf "Failed 1\n"; false)) (empty_trees bb bbt))
+           (if (check_evaluability1 reg_expr reg_expr_t) then true else (Printf.printf "Failed 12\n"; false)))
+         (if check_evaluability2 m_expr m_expr_t then true else (Printf.printf "Failed 13\n"; false))
+     | None -> (printf "FAILED1\n"; false))
+  | None -> (printf "FAILED2\n"; false)
+
 (** val check_scheduled_trees :
     GibleSeq.SeqBB.t PTree.t -> GiblePar.ParBB.t PTree.t -> bool **)
 
@@ -52,28 +72,32 @@ let seteq p d1 r1 r2: Gible.instr = RBsetpred (p, Ccomp Ceq, [reg r1; reg r2], p
 let sett p d1 r1: Gible.instr = RBsetpred (p, Ccompimm (Ceq, int 0), [reg r1], pred d1)
 let goto p n: Gible.instr = RBexit (p, (RBgoto (node n)))
 
+let time_schedules name arg1 arg2 = 
+  let _ = Timing.time (name ^ "_unhashed") (schedule_oracle [] arg1) arg2 in
+  Timing.time name (schedule_oracle' [] arg1) arg2
+
 let () =
-  (if schedule_oracle []
-       [ add None 2 1 4;
-         seteq (Some (plit true 1)) 3 4 2;
-         add (Some (plit true 1)) 1 2 4;
-         mul (Some (Pand (plit false 1, plit false 2))) 3 1 1;
-         mul (Some (plit true 2)) 3 1 4;
-         goto (Some (plit true 2)) 10;
-         mul (Some (plit false 2)) 3 3 3;
-         goto None 10;
-       ]
-       [ [ [ mul (Some (Pand (plit false 1, plit false 2))) 3 1 1; ];
-           [ add None 2 1 4;
-             add (Some (plit true 1)) 1 2 4;
-             seteq (Some (plit true 1)) 3 4 2; ] ];
-         [ [ mul (Some (plit true 2)) 3 1 4; ];
-           [ mul (Some (plit false 2)) 3 3 3; ];
-           [ goto None 10; ]
-         ]
-       ]
-  then Printf.printf "Passed 1\n"
-   else Printf.printf "Failed 1\n");
+  (* (if schedule_oracle [] *)
+  (*      [ add None 2 1 4; *)
+  (*        seteq (Some (plit true 1)) 3 4 2; *)
+  (*        add (Some (plit true 1)) 1 2 4; *)
+  (*        mul (Some (Pand (plit false 1, plit false 2))) 3 1 1; *)
+  (*        mul (Some (plit true 2)) 3 1 4; *)
+  (*        goto (Some (plit true 2)) 10; *)
+  (*        mul (Some (plit false 2)) 3 3 3; *)
+  (*        goto None 10; *)
+  (*      ] *)
+  (*      [ [ [ mul (Some (Pand (plit false 1, plit false 2))) 3 1 1; ]; *)
+  (*          [ add None 2 1 4; *)
+  (*            add (Some (plit true 1)) 1 2 4; *)
+  (*            seteq (Some (plit true 1)) 3 4 2; ] ]; *)
+  (*        [ [ mul (Some (plit true 2)) 3 1 4; ]; *)
+  (*          [ mul (Some (plit false 2)) 3 3 3; ]; *)
+  (*          [ goto None 10; ] *)
+  (*        ] *)
+  (*      ] *)
+  (* then Printf.printf "Passed 1\n" *)
+  (*  else Printf.printf "Failed 1\n"); *)
   (* (if schedule_oracle [] *)
   (*       [ seteq (Some (plit true 1)) 2 1 2; *)
   (*         goto None 10; *)
@@ -104,14 +128,14 @@ let () =
   (*       ] ] ] *)
   (* then Printf.printf "Passed 1\n" *)
   (*  else Printf.printf "Failed 1\n"); *)
-  (if schedule_oracle []
-        [ const (Some (plit true 1)) 1 0;
-          const (Some (Por (plit true 1, plit false 1))) 1 1;
-        ]
-        [ [ [ const None 1 1;
-        ] ] ]
-   then Printf.printf "Passed 1\n"
-   else Printf.printf "Failed 1\n");
+  (* (if schedule_oracle [] *)
+  (*       [ const (Some (plit true 1)) 1 0; *)
+  (*         const (Some (Por (plit true 1, plit false 1))) 1 1; *)
+  (*       ] *)
+  (*       [ [ [ const None 1 1; *)
+  (*       ] ] ] *)
+  (*  then Printf.printf "Passed 1\n" *)
+  (*  else Printf.printf "Failed 1\n"); *)
   (* (if schedule_oracle [(pred 3, pred 2)] *)
   (*      [ add None 2 1 4; *)
   (*        seteq None 1 10 11; *)
@@ -173,7 +197,7 @@ let () =
   (* then Printf.printf "Passed 110\n" *)
   (*    else Printf.printf "Failed 102\n"); *)
   (*   (if schedule_oracle [(pred 3, pred 2)] *)
-  (*      [  *)
+  (*      [ *)
   (*        seteq None 1 10 11; *)
   (*        seteq None 3 12 13; *)
   (*        seteq None 2 12 13; *)
@@ -203,4 +227,173 @@ let () =
   (*      ] ] ] *)
   (* then Printf.printf "Passed 110\n" *)
   (*    else Printf.printf "Failed 102\n") *)
-
+    (if time_schedules "1"
+       [ add (Some (Pand (plit false 1, plit false 2))) 2 2 1;
+         goto (Some (Pand (plit true 1, plit true 1))) 10
+       ]
+       [[[ 
+           goto (Some (Pand (plit true 1, plit true 1))) 10;
+           add (Some (Pand (plit false 1, plit false 2))) 2 2 1
+       ]]]
+  then Printf.printf "Passed 110\n"
+     else Printf.printf "Failed 102\n");
+    (if time_schedules "2"
+       [ 
+         add (Some (Pand (Pand (Pand (plit false 1, plit false 2), plit false 3), plit false 4))) 2 2 1;
+         goto (Some (Pand (plit true 1, plit true 1))) 10;
+         goto (Some (Pand (plit true 2, plit true 2))) 10;
+         goto (Some (Pand (plit true 3, plit true 3))) 10;
+         goto (Some (Pand (plit true 4, plit true 4))) 10;
+       ]
+       [[[ 
+            goto (Some (Pand (plit true 1, plit true 1))) 10;
+            goto (Some (Pand (plit true 2, plit true 2))) 10;
+            goto (Some (Pand (plit true 3, plit true 3))) 10;
+            goto (Some (Pand (plit true 4, plit true 4))) 10;
+            add (Some (Pand (Pand (Pand (plit false 1, plit false 2), plit false 3), plit false 4))) 2 2 1;
+       ]]]
+  then Printf.printf "Passed 110\n"
+     else Printf.printf "Failed 102\n");
+    (if time_schedules "3"
+       [ 
+         add (Some (Pand (Pand (Pand (plit false 1, plit false 2), plit false 3), plit false 4))) 2 2 1;
+         add (Some (Pand (Pand (Pand (plit false 1, plit false 2), plit false 3), plit true 4))) 10 2 3;
+         (* add (Some (Pand (Pand (Pand (plit false 1, plit false 2), plit true 3), plit false 4))) 2 2 4; *)
+         (* add (Some (Pand (Pand (Pand (plit false 1, plit true 2), plit false 3), plit false 4))) 2 2 5; *)
+         goto (Some (Pand (plit true 1, plit true 1))) 10;
+         goto (Some (Pand (plit true 2, plit true 2))) 10;
+         goto (Some (Pand (plit true 3, plit true 3))) 10;
+         goto (Some (Pand (plit true 4, plit true 4))) 10;
+       ]
+       [[[ 
+            goto (Some (Pand (plit true 1, plit true 1))) 10;
+            (* add (Some (Pand (Pand (Pand (plit false 1, plit true 2), plit false 3), plit false 4))) 2 2 5; *)
+            goto (Some (Pand (plit true 2, plit true 2))) 10;
+            (* add (Some (Pand (Pand (Pand (plit false 1, plit false 2), plit true 3), plit false 4))) 2 2 4; *)
+            goto (Some (Pand (plit true 3, plit true 3))) 10;
+            add (Some (Pand (Pand (Pand (plit false 1, plit false 2), plit false 3), plit true 4))) 10 2 3;
+            goto (Some (Pand (plit true 4, plit true 4))) 10;
+            add (Some (Pand (Pand (Pand (plit false 1, plit false 2), plit false 3), plit false 4))) 2 2 1;
+       ]]]
+  then Printf.printf "Passed 110\n"
+     else Printf.printf "Failed 102\n");
+    (if time_schedules "4"
+       [ 
+         add (Some (Pand (Pand (Pand (plit false 1, plit false 2), plit false 3), plit false 4))) 2 2 1;
+         add (Some (Pand (Pand (Pand (plit false 1, plit false 2), plit false 3), plit true 4))) 10 2 3;
+         add (Some (Pand (Pand (Pand (plit false 1, plit false 2), plit true 3), plit false 4))) 11 2 4;
+         (* add (Some (Pand (Pand (Pand (plit false 1, plit true 2), plit false 3), plit false 4))) 2 2 5; *)
+         goto (Some (Pand (plit true 1, plit true 1))) 10;
+         goto (Some (Pand (plit true 2, plit true 2))) 10;
+         goto (Some (Pand (plit true 3, plit true 3))) 10;
+         goto (Some (Pand (plit true 4, plit true 4))) 10;
+       ]
+       [[[ 
+            goto (Some (Pand (plit true 1, plit true 1))) 10;
+            (* add (Some (Pand (Pand (Pand (plit false 1, plit true 2), plit false 3), plit false 4))) 2 2 5; *)
+            goto (Some (Pand (plit true 2, plit true 2))) 10;
+            add (Some (Pand (Pand (Pand (plit false 1, plit false 2), plit true 3), plit false 4))) 11 2 4;
+            goto (Some (Pand (plit true 3, plit true 3))) 10;
+            add (Some (Pand (Pand (Pand (plit false 1, plit false 2), plit false 3), plit true 4))) 10 2 3;
+            goto (Some (Pand (plit true 4, plit true 4))) 10;
+            add (Some (Pand (Pand (Pand (plit false 1, plit false 2), plit false 3), plit false 4))) 2 2 1;
+       ]]]
+  then Printf.printf "Passed 110\n"
+     else Printf.printf "Failed 102\n");
+    (if time_schedules "5"
+       [            
+         add (Some (Pand (plit false 1, plit false 10))) 40 50 51;
+         seteq (Some (plit false 1)) 2 40 41;
+         (* add (Some (Pand (plit true 10, plit true 4))) 40 52 53; *)
+         (* seteq (Some (plit false 5)) 3 40 42; *)
+         goto (Some (Pand (plit true 1, plit true 1))) 10;
+         add (Some (Pand (Pand (Pand (plit false 1, plit false 2), plit false 3), plit false 4))) 2 2 1;
+         add (Some (Pand (Pand (Pand (plit false 1, plit false 2), plit false 3), plit true 4))) 10 2 3;
+         add (Some (Pand (Pand (Pand (plit false 1, plit false 2), plit true 3), plit false 4))) 11 2 4;
+         (* add (Some (Pand (Pand (Pand (plit false 1, plit true 2), plit false 3), plit false 4))) 2 2 5; *)
+         goto (Some (Pand (plit true 1, plit true 1))) 10;
+         goto (Some (Pand (plit true 2, plit true 2))) 10;
+         goto (Some (Pand (plit true 3, plit true 3))) 10;
+         goto (Some (Pand (plit true 4, plit true 4))) 10;
+       ]
+       [[[ 
+            add (Some (Pand (plit false 1, plit false 10))) 40 50 51;
+            seteq (Some (plit false 1)) 2 40 41;
+            (* add (Some (Pand (plit true 10, plit true 4))) 40 52 53; *)
+            (* seteq (Some (plit false 5)) 3 40 42; *)
+            goto (Some (Pand (plit true 1, plit true 1))) 10;
+            (* add (Some (Pand (Pand (Pand (plit false 1, plit true 2), plit false 3), plit false 4))) 2 2 5; *)
+            goto (Some (Pand (plit true 2, plit true 2))) 10;
+            add (Some (Pand (Pand (Pand (plit false 1, plit false 2), plit true 3), plit false 4))) 11 2 4;
+            goto (Some (Pand (plit true 3, plit true 3))) 10;
+            add (Some (Pand (Pand (Pand (plit false 1, plit false 2), plit false 3), plit true 4))) 10 2 3;
+            goto (Some (Pand (plit true 4, plit true 4))) 10;
+            add (Some (Pand (Pand (Pand (plit false 1, plit false 2), plit false 3), plit false 4))) 2 2 1;
+       ]]]
+  then Printf.printf "Passed 110\n"
+     else Printf.printf "Failed 104\n");
+(if time_schedules "6"
+       [            
+         add (Some (Pand (plit false 1, plit false 10))) 40 50 51;
+         seteq (Some (plit false 1)) 2 40 41;
+         (* add (Some (Pand (plit true 10, plit true 4))) 40 52 53; *)
+         (* seteq (Some (plit false 5)) 3 40 42; *)
+            seteq (Some (plit false 5)) 3 41 40;
+         goto (Some (Pand (plit true 1, plit true 1))) 10;
+         add (Some (Pand (Pand (Pand (plit false 1, plit false 2), plit false 3), plit false 4))) 2 2 1;
+         add (Some (Pand (Pand (Pand (plit false 1, plit false 2), plit false 3), plit true 4))) 10 2 3;
+         add (Some (Pand (Pand (Pand (plit false 1, plit false 2), plit true 3), plit false 4))) 11 2 4;
+         (* add (Some (Pand (Pand (Pand (plit false 1, plit true 2), plit false 3), plit false 4))) 2 2 5; *)
+         goto (Some (Pand (plit true 1, plit true 1))) 10;
+         goto (Some (Pand (plit true 2, plit true 2))) 10;
+         goto (Some (Pand (plit true 3, plit true 3))) 10;
+         goto (Some (Pand (plit true 4, plit true 4))) 10;
+       ]
+       [[[ 
+            add (Some (Pand (plit false 1, plit false 10))) 40 50 51;
+            seteq (Some (plit false 1)) 2 40 41;
+            (* add (Some (Pand (plit true 10, plit true 4))) 40 52 53; *)
+            seteq (Some (plit false 5)) 3 41 40;
+            goto (Some (Pand (plit true 1, plit true 1))) 10;
+            (* add (Some (Pand (Pand (Pand (plit false 1, plit true 2), plit false 3), plit false 4))) 2 2 5; *)
+            goto (Some (Pand (plit true 2, plit true 2))) 10;
+            add (Some (Pand (Pand (Pand (plit false 1, plit false 2), plit true 3), plit false 4))) 11 2 4;
+            goto (Some (Pand (plit true 3, plit true 3))) 10;
+            add (Some (Pand (Pand (Pand (plit false 1, plit false 2), plit false 3), plit true 4))) 10 2 3;
+            goto (Some (Pand (plit true 4, plit true 4))) 10;
+            add (Some (Pand (Pand (Pand (plit false 1, plit false 2), plit false 3), plit false 4))) 2 2 1;
+       ]]]
+  then Printf.printf "Passed 110\n"
+     else Printf.printf "Failed 104\n");
+    (if time_schedules "7"
+       [            
+         add (Some (Pand (plit false 1, plit false 10))) 40 50 51;
+         seteq (Some (plit false 1)) 2 40 41;
+         add (Some (Pand (plit true 10, plit true 4))) 40 52 53;
+         seteq (Some (plit false 5)) 3 40 42;
+         goto (Some (Pand (plit true 1, plit true 1))) 10;
+         add (Some (Pand (Pand (Pand (plit false 1, plit false 2), plit false 3), plit false 4))) 2 2 1;
+         add (Some (Pand (Pand (Pand (plit false 1, plit false 2), plit false 3), plit true 4))) 10 2 3;
+         add (Some (Pand (Pand (Pand (plit false 1, plit false 2), plit true 3), plit false 4))) 11 2 4;
+         (* add (Some (Pand (Pand (Pand (plit false 1, plit true 2), plit false 3), plit false 4))) 2 2 5; *)
+         goto (Some (Pand (plit true 1, plit true 1))) 10;
+         goto (Some (Pand (plit true 2, plit true 2))) 10;
+         goto (Some (Pand (plit true 3, plit true 3))) 10;
+         goto (Some (Pand (plit true 4, plit true 4))) 10;
+       ]
+       [[[ 
+            add (Some (Pand (plit false 1, plit false 10))) 40 50 51;
+            seteq (Some (plit false 1)) 2 40 41;
+            add (Some (Pand (plit true 10, plit true 4))) 40 52 53;
+            seteq (Some (plit false 5)) 3 40 42;
+            goto (Some (Pand (plit true 1, plit true 1))) 10;
+            (* add (Some (Pand (Pand (Pand (plit false 1, plit true 2), plit false 3), plit false 4))) 2 2 5; *)
+            goto (Some (Pand (plit true 2, plit true 2))) 10;
+            add (Some (Pand (Pand (Pand (plit false 1, plit false 2), plit true 3), plit false 4))) 11 2 4;
+            goto (Some (Pand (plit true 3, plit true 3))) 10;
+            add (Some (Pand (Pand (Pand (plit false 1, plit false 2), plit false 3), plit true 4))) 10 2 3;
+            goto (Some (Pand (plit true 4, plit true 4))) 10;
+            add (Some (Pand (Pand (Pand (plit false 1, plit false 2), plit false 3), plit false 4))) 2 2 1;
+       ]]]
+  then Printf.printf "Passed 110\n"
+     else Printf.printf "Failed 104\n")
diff --git a/src/extraction/Extraction.v b/src/extraction/Extraction.v
index 0a83f02..cd8b037 100644
--- a/src/extraction/Extraction.v
+++ b/src/extraction/Extraction.v
@@ -28,6 +28,8 @@ From vericert Require
      HLSOpts
      Predicate
      Bourdoncle
+     GiblePargenproofEquiv
+     GiblePargen
 .
 
 From Coq Require DecidableClass.
@@ -209,7 +211,8 @@ Separate Extraction
          Verilog.stmnt_to_list
          Bourdoncle.bourdoncle
 
-   Smtpredicate.check_smt_total
+   Smtpredicate.check_smt_total GiblePargenproofEquiv.check GiblePargen.check_evaluability1
+   GiblePargen.check_evaluability2
 
    Compiler.transf_c_program Compiler.transf_cminor_program
    Cexec.do_initial_state Cexec.do_step Cexec.at_final_state
diff --git a/src/hls/GiblePargenproofEquiv.v b/src/hls/GiblePargenproofEquiv.v
index 262e9d5..702da5b 100644
--- a/src/hls/GiblePargenproofEquiv.v
+++ b/src/hls/GiblePargenproofEquiv.v
@@ -1547,12 +1547,13 @@ Definition check_mutexcl {A} eq_dec (pe: predicated A) :=
   else false.
 
 Definition check_mutexcl_unhashed {A} eq_dec (preds: PTree.t pred_pexpr) (pe: predicated A) :=
-  if NE.norepet_check eq_dec pe then
-    let lpe := NE.to_list pe in
-    let pairs := map (fun x => fst x → negate (or_list (map fst (remove eq_dec x lpe)))) lpe in
-    let (np1, h) := TVL.hash_predicate (transf_pred_op (from_pred_op preds (simplify (and_list pairs)))) (Maps.PTree.empty _) in
-    STV.check_smt_total np1
-  else false.
+  (* if NE.norepet_check eq_dec pe then *)
+  (*   let lpe := NE.to_list pe in *)
+  (*   let pairs := map (fun x => fst x → negate (or_list (map fst (remove eq_dec x lpe)))) lpe in *)
+  (*   let (np1, h) := TVL.hash_predicate (transf_pred_op (from_pred_op preds (simplify (and_list pairs)))) (Maps.PTree.empty _) in *)
+  (*   STV.check_smt_total np1 *)
+  (* else false. *)
+  check_mutexcl eq_dec pe.
 
 (* Import ListNotations. *)
 (* Compute deep_simplify peq (and_list (map (fun x => x → negate (or_list (remove (Predicate.eq_dec peq) x [Plit (true, 2)]))) [Plit (true, 2)])). *)