Add equivalence classes

2 files changed, 212 insertions, 0 deletions

diff --git a/debug/dune b/debug/dune
new file mode 100644
index 0000000..e47c832
--- /dev/null
+++ b/debug/dune
@@ -0,0 +1,6 @@
+(include_subdirs no)
+
+(executable
+ (name VericertTest)
+ (libraries vericert)
+ (flags (:standard -warn-error -A -w -8-9-16-20-26-27-32..36-39-41-44..45-50-60-67)))
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") *)
+