From 1850879e7e196c0e1c00900acf5facaaf5387beb Mon Sep 17 00:00:00 2001 From: Yann Herklotz Date: Mon, 18 Sep 2023 10:55:13 +0100 Subject: Add benchmarking of unhashed commands --- debug/vericertTest.ml | 255 +++++++++++++++++++++++++++++++++++----- src/extraction/Extraction.v | 5 +- src/hls/GiblePargenproofEquiv.v | 13 +- 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)])). *) -- cgit