Add unhashed functions for comparisons

4 files changed, 116 insertions, 25 deletions

diff --git a/debug/vericertTest.ml b/debug/vericertTest.ml
index 4d4e55f..a67d30d 100644
--- a/debug/vericertTest.ml
+++ b/debug/vericertTest.ml
@@ -28,9 +28,9 @@ let schedule_oracle l bb bbt =
        printf "F1:\n%a\n" PrintAbstr.print_forest bb';
        printf "F2:\n%a\n" PrintAbstr.print_forest bbt'; flush stdout;
        (&&)
-         ((&&) ((&&) (if check l 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))
+         ((&&) ((&&) (if check_unhashed [] bb' bbt' then true else (Printf.printf "Failed 1\n"; false)) (empty_trees bb bbt))
+           (if (check_evaluability1_unhashed bb'.forest_preds bbt'.forest_preds reg_expr reg_expr_t) then true else (Printf.printf "Failed 12\n"; false)))
+         (if check_evaluability2_unhashed bb'.forest_preds bbt'.forest_preds m_expr m_expr_t then true else (Printf.printf "Failed 13\n"; false))
      | None -> (printf "FAILED1\n"; false))
   | None -> (printf "FAILED2\n"; false)
 
@@ -53,27 +53,27 @@ let sett p d1 r1: Gible.instr = RBsetpred (p, Ccompimm (Ceq, int 0), [reg r1], p
 let goto p n: Gible.instr = RBexit (p, (RBgoto (node n)))
 
 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; *)
diff --git a/src/Compiler.v b/src/Compiler.v
index d76db43..8e28792 100644
--- a/src/Compiler.v
+++ b/src/Compiler.v
@@ -293,7 +293,7 @@ Definition transf_hls_temp (p : Csyntax.program) : res Verilog.program :=
    @@ print (print_GibleSeq 4)
   @@@ DeadBlocks.transf_program
    @@ print (print_GibleSeq 5)
-  @@@ GiblePargen.transl_program
+  @@@ time "Scheduling" GiblePargen.transl_program_unhashed
    @@ print (print_GiblePar 0)
   @@@ HTLPargen.transl_program
    @@ print (print_DHTL 0)
diff --git a/src/hls/GiblePargen.v b/src/hls/GiblePargen.v
index e3cfcda..61b9819 100644
--- a/src/hls/GiblePargen.v
+++ b/src/hls/GiblePargen.v
@@ -411,11 +411,26 @@ Definition check_evaluability1 a b :=
     ) a
   ) b.
 
+Definition check_evaluability1_unhashed p p' a b :=
+  forallb (fun be =>
+    existsb (fun ae =>
+      resource_eq (fst ae) (fst be) 
+      && HN.beq_pred_expr_unhashed p p' (snd ae) (snd be)
+      && check_mutexcl HN.pred_Ht_dec (snd ae)
+      && check_mutexcl HN.pred_Ht_dec (snd be)
+    ) a
+  ) b.
+
 Definition check_evaluability2 a b :=
   forallb (fun be => existsb (fun ae => HN.beq_pred_expr nil ae be
                                      && check_mutexcl HN.pred_Ht_dec ae
                                      && check_mutexcl HN.pred_Ht_dec be) a) b.
 
+Definition check_evaluability2_unhashed p p' a b :=
+  forallb (fun be => existsb (fun ae => HN.beq_pred_expr_unhashed p p' ae be
+                                     && check_mutexcl HN.pred_Ht_dec ae
+                                     && check_mutexcl HN.pred_Ht_dec be) a) b.
+
 Definition schedule_oracle (bb: SeqBB.t) (bbt: ParBB.t) : bool :=
   match abstract_sequence_top bb, abstract_sequence_top (concat (concat bbt)) with
   | Some (bb', reg_expr, m_expr), Some (bbt', reg_expr_t, m_expr_t) =>
@@ -425,8 +440,19 @@ Definition schedule_oracle (bb: SeqBB.t) (bbt: ParBB.t) : bool :=
   | _, _ => false
   end.
 
+Definition schedule_oracle_unhashed (bb: SeqBB.t) (bbt: ParBB.t) : bool :=
+  match abstract_sequence_top bb, abstract_sequence_top (concat (concat bbt)) with
+  | Some (bb', reg_expr, m_expr), Some (bbt', reg_expr_t, m_expr_t) =>
+      check_unhashed nil bb' bbt' && empty_trees bb bbt
+      && check_evaluability1_unhashed bb'.(forest_preds) bbt'.(forest_preds) reg_expr reg_expr_t
+      && check_evaluability2_unhashed bb'.(forest_preds) bbt'.(forest_preds) m_expr m_expr_t
+  | _, _ => false
+  end.
+
 Definition check_scheduled_trees := beq2 schedule_oracle.
 
+Definition check_scheduled_trees_unhashed := beq2 schedule_oracle_unhashed.
+
 Ltac solve_scheduled_trees_correct :=
   intros; unfold check_scheduled_trees in *;
   match goal with
@@ -468,7 +494,25 @@ Definition transl_function (f: GibleSeq.function)
     Err.Error
       (Err.msg "GiblePargen: Could not prove the blocks equivalent.").
 
+Definition transl_function_unhashed (f: GibleSeq.function)
+  : Err.res GiblePar.function :=
+  let tfcode := fn_code (schedule f) in
+  if check_scheduled_trees_unhashed f.(GibleSeq.fn_code) tfcode then
+    Err.OK (mkfunction f.(GibleSeq.fn_sig)
+                          f.(GibleSeq.fn_params)
+                          f.(GibleSeq.fn_stacksize)
+                          tfcode
+                          f.(GibleSeq.fn_entrypoint))
+  else
+    Err.Error
+      (Err.msg "GiblePargen: Could not prove the blocks equivalent.").
+
 Definition transl_fundef := transf_partial_fundef transl_function.
 
 Definition transl_program (p : GibleSeq.program) : Err.res GiblePar.program :=
   transform_partial_program transl_fundef p.
+
+Definition transl_fundef_unhashed := transf_partial_fundef transl_function_unhashed.
+
+Definition transl_program_unhashed (p : GibleSeq.program) : Err.res GiblePar.program :=
+  transform_partial_program transl_fundef_unhashed p.
diff --git a/src/hls/GiblePargenproofEquiv.v b/src/hls/GiblePargenproofEquiv.v
index df14e31..262e9d5 100644
--- a/src/hls/GiblePargenproofEquiv.v
+++ b/src/hls/GiblePargenproofEquiv.v
@@ -1177,18 +1177,37 @@ Module HashExprNorm(HS: Hashable).
       mk_pred_stmnt tree == mk_pred_stmnt tree'.
   Proof. Abort.
 
+  Definition equiv_check_unhashed (pe1 pe2: pred_pexpr) :=
+    if pred_pexpr_eqb pe1 pe2 then true else
+    let (np1, h) := TVL.hash_predicate (transf_pred_op (simplify pe1)) (Maps.PTree.empty _) in
+    let (np2, h') := TVL.hash_predicate (transf_pred_op (simplify pe2)) h in
+    STV.check_smt_total (TV.equiv np1 np2).
+
   Definition tree_equiv_check_el eq_list (np2: PTree.t pred_op) (n: positive) (p: pred_op): bool :=
     match np2 ! n with
     | Some p' => equiv_check_eq_list eq_list p p'
     | None => equiv_check_eq_list eq_list p ⟂
     end.
 
+  Definition tree_equiv_check_el_unhashed (pexpr pexpr': PTree.t pred_pexpr) 
+      (np2: PTree.t pred_op) (n: positive) (p: pred_op): bool :=
+    match np2 ! n with
+    | Some p' => equiv_check_unhashed (from_pred_op pexpr p) (from_pred_op pexpr' p')
+    | None => equiv_check_unhashed (from_pred_op pexpr p) ⟂
+    end.
+
   Definition tree_equiv_check_None_el eq_list (np2: PTree.t pred_op) (n: positive) (p: pred_op): bool :=
     match np2 ! n with
     | Some p' => true
     | None => equiv_check_eq_list eq_list p ⟂
     end.
 
+  Definition tree_equiv_check_None_el_unhashed (pexpr pexpr': PTree.t pred_pexpr) (np2: PTree.t pred_op) (n: positive) (p: pred_op): bool :=
+    match np2 ! n with
+    | Some p' => true
+    | None => equiv_check_unhashed (from_pred_op pexpr p) ⟂
+    end.
+
   Definition beq_pred_expr eq_list (pe1 pe2: predicated HS.t) : bool :=
     if pred_expr_dec pe1 pe2 then true else
     let (np1, h) := norm_expression 1 pe1 (PTree.empty _) in
@@ -1196,6 +1215,13 @@ Module HashExprNorm(HS: Hashable).
     forall_ptree (tree_equiv_check_el eq_list np2) np1
     && forall_ptree (tree_equiv_check_None_el eq_list np1) np2.
 
+  Definition beq_pred_expr_unhashed (preds preds': PTree.t pred_pexpr) (pe1 pe2: predicated HS.t) : bool :=
+    if pred_expr_dec pe1 pe2 then true else
+    let (np1, h) := norm_expression 1 pe1 (PTree.empty _) in
+    let (np2, h') := norm_expression 1 pe2 h in
+    forall_ptree (tree_equiv_check_el_unhashed preds preds' np2) np1
+    && forall_ptree (tree_equiv_check_None_el_unhashed preds preds' np1) np2.
+
   Lemma beq_pred_expr_correct:
     forall eq_list np1 np2 e p p' c,
       sat_predicate (eq_list_to_pred_op eq_list) c = true ->
@@ -1520,6 +1546,14 @@ Definition check_mutexcl {A} eq_dec (pe: predicated A) :=
     end
   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.
+
 (* 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)])). *)
 
@@ -1610,6 +1644,9 @@ Qed.
 Definition check_mutexcl_tree {A} eq_dec (f: PTree.t (predicated A)) :=
   forall_ptree (fun _ => check_mutexcl eq_dec) f.
 
+Definition check_mutexcl_tree_unhashed {A} eq_dec preds (f: PTree.t (predicated A)) :=
+  forall_ptree (fun _ => check_mutexcl_unhashed preds eq_dec) f.
+
 Lemma check_mutexcl_tree_correct:
   forall A eq_dec (f: PTree.t (predicated A)) i pe,
     check_mutexcl_tree eq_dec f = true ->
@@ -1649,6 +1686,16 @@ Definition check (eq_list: list (positive * positive)) f1 f2 :=
   && check_mutexcl EHN.pred_Ht_dec f1.(forest_exit)
   && check_mutexcl EHN.pred_Ht_dec f2.(forest_exit)
   && (forallb (fun x => beq_pred_pexpr (f1 #p (fst x)) (f1 #p (snd x))) eq_list).
+  
+Definition check_unhashed (eq_list: list (positive * positive)) f1 f2 :=
+  RTree.beq (HN.beq_pred_expr_unhashed f1.(forest_preds) f2.(forest_preds)) f1.(forest_regs) f2.(forest_regs)
+  && PTree.beq beq_pred_pexpr f1.(forest_preds) f2.(forest_preds)
+  && EHN.beq_pred_expr_unhashed f1.(forest_preds) f2.(forest_preds) f1.(forest_exit) f2.(forest_exit)
+  && check_mutexcl_tree_unhashed f1.(forest_preds) HN.pred_Ht_dec f1.(forest_regs)
+  && check_mutexcl_tree_unhashed f2.(forest_preds) HN.pred_Ht_dec f2.(forest_regs)
+  && check_mutexcl_unhashed EHN.pred_Ht_dec f1.(forest_preds) f1.(forest_exit)
+  && check_mutexcl_unhashed EHN.pred_Ht_dec f2.(forest_preds) f2.(forest_exit)
+  && (forallb (fun x => beq_pred_pexpr (f1 #p (fst x)) (f1 #p (snd x))) eq_list).
 
 Lemma sem_pexpr_forward_eval1 :
   forall A ctx f_p ps,