From 6a74d2e648903e54300f276a024e396978629b30 Mon Sep 17 00:00:00 2001 From: Yann Herklotz Date: Sun, 17 Sep 2023 12:09:25 +0100 Subject: Add unhashed functions for comparisons --- debug/vericertTest.ml | 48 ++++++++++++++++++++--------------------- src/Compiler.v | 2 +- src/hls/GiblePargen.v | 44 +++++++++++++++++++++++++++++++++++++ src/hls/GiblePargenproofEquiv.v | 47 ++++++++++++++++++++++++++++++++++++++++ 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, -- cgit