From 93117b6e766c25c5aeecdc20a963d5114fb91e59 Mon Sep 17 00:00:00 2001 From: Yann Herklotz Date: Tue, 11 Jul 2023 15:45:59 +0100 Subject: Add equivalence classes --- debug/vericertTest.ml | 206 ++++++++++++++++++++++++++++++++++++++++++++++++++ 1 file changed, 206 insertions(+) create mode 100644 debug/vericertTest.ml (limited to 'debug/vericertTest.ml') diff --git a/debug/vericertTest.ml b/debug/vericertTest.ml new file mode 100644 index 0000000..4d4e55f --- /dev/null +++ b/debug/vericertTest.ml @@ -0,0 +1,206 @@ +open Vericert + +open AST +open Abstr +open BinNums +open Coqlib +open Datatypes +open Errors +open GiblePargenproofEquiv +open List0 +open Maps +open Optionmonad +open Predicate +open GiblePargen +open Integers +open Op +open Printf + +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 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)) + | 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 **) + +let z = Camlcoq.Z.of_sint +let int n = Int.repr (z n) +let reg = Camlcoq.P.of_int +let pred = Camlcoq.P.of_int +let node = Camlcoq.P.of_int +let plit b p = Plit (b, pred p) + +let const p d c: Gible.instr = RBop (p, Ointconst (z c), [], reg d) +let add p d1 r1 r2: Gible.instr = RBop (p, Olea (Aindexed2 (z 0)), [reg r1; reg r2], reg d1) +let mul p d1 r1 r2: Gible.instr = RBop (p, Omul, [reg r1; reg r2], reg d1) +let div p d1 r1 r2: Gible.instr = RBop (p, Odiv, [reg r1; reg r2], reg d1) +let seteq p d1 r1 r2: Gible.instr = RBsetpred (p, Ccomp Ceq, [reg r1; reg r2], pred d1) +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 () = + (* (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; *) + (* ] *) + (* [ [ [ goto (Some (plit false 1)) 10; *) + (* seteq None 2 1 2; *) + (* goto None 10; *) + (* ] ] ] *) + (* then Printf.printf "Passed 1\n" *) + (* else Printf.printf "Failed 1\n"); *) + (* (if schedule_oracle [] *) + (* [ seteq None 2 1 2; *) + (* seteq None 3 1 2; *) + (* seteq (Some (Por (plit true 2, plit false 3))) 4 1 3; *) + (* ] *) + (* [ [ [ seteq None 2 1 2; *) + (* seteq None 3 1 2; *) + (* seteq None 4 1 3; *) + (* ] ] ] *) + (* then Printf.printf "Passed 1\n" *) + (* else Printf.printf "Failed 1\n"); *) + (* (if schedule_oracle [] *) + (* [ sett (Some (plit false 1)) 2 1; *) + (* div (Some (plit true 1)) 1 2 3; *) + (* ] *) + (* [ [ [ div (Some (plit true 1)) 1 2 3; *) + (* sett (Some (plit false 1)) 2 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; *) + (* add (Some (plit true 1)) 1 2 4; *) + (* seteq (Some (plit true 1)) 2 12 13; *) + (* mul (Some (Pand (plit true 1, plit true 2))) 3 1 4; *) + (* goto (Some (Pand (plit true 1, plit true 2))) 10; *) + (* mul (Some (Pand (plit true 1, plit false 2))) 3 3 3; *) + (* goto (Some (Pand (plit true 1, plit false 2))) 10; *) + (* seteq (Some (plit false 1)) 3 12 13; *) + (* mul (Some (Pand (plit false 1, plit true 3))) 3 1 4; *) + (* goto (Some (Pand (plit false 1, plit true 3))) 10; *) + (* mul (Some (Pand (plit false 1, plit false 3))) 3 1 1; *) + (* mul (Some (Pand (plit false 1, plit false 3))) 3 3 3; *) + (* goto (Some (Pand (plit false 1, plit false 3))) 10; *) + (* ] *) + (* [ [ [ seteq None 1 10 11; *) + (* add None 2 1 4; *) + (* seteq (Some (plit false 1)) 3 12 13; *) + (* seteq (Some (plit true 1)) 2 12 13; *) + (* add (Some (plit true 1)) 1 2 4; *) + (* mul (Some (Pand (plit true 1, plit true 2))) 3 1 4; *) + (* mul (Some (Pand (plit true 1, plit false 2))) 3 3 3; *) + (* mul (Some (Pand (plit false 1, plit true 2))) 3 1 4; *) + (* mul (Some (Pand (plit false 1, plit false 2))) 3 1 1; *) + (* mul (Some (Pand (plit false 1, plit false 2))) 3 3 3; *) + (* goto None 10; *) + (* ] ] ] *) + (* then Printf.printf "Passed 110\n" *) + (* else Printf.printf "Failed 102\n"); *) + (* (if schedule_oracle [(pred 3, pred 2)] *) + (* [ add None 2 1 4; *) + (* seteq None 1 10 11; *) + (* add (Some (plit true 1)) 1 2 4; *) + (* seteq (Some (plit true 1)) 2 12 13; *) + (* mul (Some (Pand (plit true 1, plit true 2))) 3 1 4; *) + (* goto (Some (Pand (plit true 1, plit true 2))) 10; *) + (* mul (Some (Pand (plit true 1, plit false 2))) 5 3 3; *) + (* goto (Some (Pand (plit true 1, plit false 2))) 10; *) + (* seteq (Some (plit false 1)) 3 12 13; *) + (* mul (Some (Pand (plit false 1, plit true 3))) 3 1 4; *) + (* goto (Some (Pand (plit false 1, plit true 3))) 10; *) + (* mul (Some (Pand (plit false 1, plit false 3))) 3 1 1; *) + (* mul (Some (Pand (plit false 1, plit false 3))) 5 3 3; *) + (* goto (Some (Pand (plit false 1, plit false 3))) 10; *) + (* ] *) + (* [ [ [ seteq None 1 10 11; *) + (* add None 2 1 4; *) + (* seteq (Some (plit false 1)) 3 12 13; *) + (* seteq (Some (plit true 1)) 2 12 13; *) + (* add (Some (plit true 1)) 1 2 4; *) + (* mul (Some (Pand (plit true 1, plit true 2))) 3 1 4; *) + (* mul (Some (Pand (plit false 1, plit true 2))) 3 1 4; *) + (* mul (Some (Pand (plit false 1, plit false 2))) 3 1 1; *) + (* mul (Some (Pand (plit true 1, plit false 2))) 5 3 3; *) + (* mul (Some (Pand (plit false 1, plit false 2))) 5 3 3; *) + (* goto None 10; *) + (* ] ] ] *) + (* 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; *) + (* add None 2 1 4; *) + (* mul (Some (Pand (plit false 1, plit false 3))) 3 1 1; *) + (* mul (Some (Pand (plit false 1, plit false 3))) 5 3 3; *) + (* goto (Some (Pand (plit false 1, plit false 3))) 10; *) + (* mul (Some (Pand (plit false 1, plit true 3))) 3 1 4; *) + (* goto (Some (Pand (plit false 1, plit true 3))) 10; *) + (* add (Some (plit true 1)) 1 2 4; *) + (* mul (Some (Pand (plit true 1, plit false 2))) 5 3 3; *) + (* goto (Some (Pand (plit true 1, plit false 2))) 10; *) + (* mul (Some (Pand (plit true 1, plit true 2))) 3 1 4; *) + (* goto (Some (Pand (plit true 1, plit true 2))) 10; *) + (* ] *) + (* [ [ [ seteq None 1 10 11; *) + (* seteq None 3 12 13; *) + (* seteq None 2 12 13; *) + (* 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; *) + (* mul (Some (Pand (plit false 1, plit true 2))) 3 1 4; *) + (* mul (Some (Pand (plit true 1, plit true 2))) 3 1 4; *) + (* mul (Some (Pand (plit false 1, plit false 2))) 5 3 3; *) + (* mul (Some (Pand (plit true 1, plit false 2))) 5 3 3; *) + (* goto None 10; *) + (* ] ] ] *) + (* then Printf.printf "Passed 110\n" *) + (* else Printf.printf "Failed 102\n") *) + -- cgit