BTL Scheduler oracle and some drafts

9 files changed, 136 insertions, 13 deletions

diff --git a/driver/Compiler.vexpand b/driver/Compiler.vexpand
index 85f265db..40ea0d68 100644
--- a/driver/Compiler.vexpand
+++ b/driver/Compiler.vexpand
@@ -300,7 +300,7 @@ EXPAND_RTL_FORWARD_SIMULATIONS
   eapply compose_forward_simulations.
     eapply RTLtoBTLproof.transf_program_correct; eassumption.
   eapply compose_forward_simulations.
-    eapply BTLtoRTLproof.transf_program_correct_cfg; eassumption.
+    eapply BTLtoRTLproof.transf_program_correct; eassumption.
   eapply compose_forward_simulations.
     eapply Allocationproof.transf_program_correct; eassumption.
   eapply compose_forward_simulations.
diff --git a/scheduling/BTLScheduleraux.ml b/scheduling/BTLScheduleraux.ml
index ad0c307d..b87636e1 100644
--- a/scheduling/BTLScheduleraux.ml
+++ b/scheduling/BTLScheduleraux.ml
@@ -4,6 +4,7 @@ open Registers
 open BTL
 open BTLtypes
 open DebugPrint
+open PrintBTL
 open RTLcommonaux
 open InstructionScheduler
 open PrepassSchedulingOracleDeps
@@ -243,8 +244,11 @@ let rec do_schedule btl = function
       let btl' = schedule_blk n ibf btl in
       do_schedule btl' blks
 
-let btl_scheduler btl =
+let btl_scheduler f =
+  let btl = f.fn_code in
   (*debug_flag := true;*)
   let btl' = do_schedule btl (PTree.elements btl) in
+  debug "Scheduled BTL Code:\n";
+  print_btl_code stderr btl';
   (*debug_flag := false;*)
   btl'
diff --git a/scheduling/BTL_Livecheck.v b/scheduling/BTL_Livecheck.v
index 2baba025..6064e4cd 100644
--- a/scheduling/BTL_Livecheck.v
+++ b/scheduling/BTL_Livecheck.v
@@ -4,8 +4,51 @@ Require Import Errors RTL BTL BTLmatchRTL.
 
 (** TODO: adapt stuff RTLpathLivegen *)
 
-Definition liveness_checker (f: BTL.function): res unit := OK tt. (* TODO: implement this ! *)
-
+Local Open Scope lazy_bool_scope.
+
+Local Open Scope option_monad_scope.
+
+Fixpoint list_mem (rl: list reg) (alive: Regset.t) {struct rl}: bool :=
+  match rl with
+  | nil => true
+  | r1 :: rs => Regset.mem r1 alive &&& list_mem rs alive
+  end.
+
+(*
+Fixpoint iblock_checker (btl: code) (ib: iblock) (alive: Regset.t) : option Regset.t :=
+  match ib with
+  | Bseq ib1 ib2 =>
+      SOME alive' <- iblock_checker btl ib1 alive IN
+      iblock_checker btl ib1 alive' (Some ib2)
+  | Bnop _ =>
+      iblock_checker btl alive
+  | Bop _ args dest _ =>
+      ASSERT list_mem args alive IN
+      iblock_checker btl (Regset.add dest alive)
+  | Bload _ _ _ args dest _ =>
+      ASSERT list_mem args alive IN
+      iblock_checker btl (Regset.add dest alive)
+  | Bstore _ _ args src _ =>
+      ASSERT Regset.mem src alive IN
+      ASSERT list_mem args alive IN
+      iblock_checker btl alive
+  | Bcond _ args (BF (Bgoto s) _) ib2 _ =>
+      ASSERT list_mem args alive IN
+      SOME _ <- iblock_checker btl ib2 alive None IN
+      SOME next <- btl!s IN
+      ASSERT Regset.subset next.(input_regs) alive IN
+      iblock_checker btl next.(entry) next.(input_regs) None
+  | Bcond _ _ _ _ _ => None
+  | BF _ _ => Some tt
+  end.
+
+Definition liveness_checker (f: BTL.function): res unit :=
+  match f.(fn_code)!(f.(fn_entrypoint)) with
+  | Some ibf => iblock_checker f.(fn_code) ibf.(entry) ibf.(input_regs)
+  | None => Error (msg "liveness_checker: empty function")
+  end.
+ *)
+Definition liveness_checker (f: BTL.function): res unit := OK tt.
 Definition liveness_ok_function (f: BTL.function): Prop := liveness_checker f = OK tt.
 
 (** TODO: adapt stuff RTLpathLivegenproof *)
diff --git a/scheduling/BTL_Scheduler.v b/scheduling/BTL_Scheduler.v
index 43d6dd5e..b479204c 100644
--- a/scheduling/BTL_Scheduler.v
+++ b/scheduling/BTL_Scheduler.v
@@ -7,6 +7,8 @@ Require Import Errors Linking BTL_SEtheory.
 (** External oracle *)
 Axiom scheduler: BTL.function -> BTL.code.
 
+Extract Constant scheduler => "BTLScheduleraux.btl_scheduler".
+
 (* a specification of the verification to do on each function *)
 Record match_function (f1 f2: BTL.function): Prop := {
   preserv_fnsig: fn_sig f1 = fn_sig f2;
diff --git a/scheduling/BTLmatchRTL.v b/scheduling/BTLmatchRTL.v
index 8994579d..8081b3a6 100644
--- a/scheduling/BTLmatchRTL.v
+++ b/scheduling/BTLmatchRTL.v
@@ -30,21 +30,55 @@ Qed.
 
 Local Hint Resolve tr_inputs_lessdef init_regs_lessdef_preserv find_function_lessdef regs_lessdef_regs
   lessdef_state_refl: core.
+Local Hint Unfold regs_lessdef: core.
 
-Lemma fsem2cfgsem_ibistep_simu ge sp rs1 m1 ib rs1' m1' of
+Lemma fsem2cfgsem_ibistep_simu ge sp rs1 m1 rs1' m1' of
+  rs2 m2 ib
   (ISTEP: iblock_istep ge sp rs1 m1 ib rs1' m1' of)
-  rs2 m2
   (REGS: forall r, Val.lessdef rs1#r rs2#r)
   (MEMS: Mem.extends m1 m2)
   : exists rs2' m2', iblock_istep_run ge sp ib rs2 m2 = Some (out rs2' m2' of) 
      /\ (forall r, Val.lessdef rs1'#r rs2'#r)
      /\ (Mem.extends m1' m2').
 Proof.
-  induction ISTEP; simpl; try_simplify_someHyps.
+  induction ISTEP; simpl; try_simplify_someHyps; intros.
+  - (* Bop *)
+    exploit (@eval_operation_lessdef _ _ ge sp op (rs ## args)); eauto.
+    intros (v1 & EVAL' & LESSDEF).
+    do 2 eexists; rewrite EVAL'. repeat (split; eauto).
+    eapply set_reg_lessdef; eauto.
+  - (* Bload *)
+    exploit (@eval_addressing_lessdef _ _ ge sp addr (rs ## args)); eauto.
+    intros (v2 & EVAL' & LESSDEF). exploit Mem.loadv_extends; eauto.
+    intros (v3 & LOAD' & LESSDEF').
+    do 2 eexists; rewrite EVAL', LOAD'. repeat (split; eauto).
+    eapply set_reg_lessdef; eauto.
+  - (* Bstore *)
+    exploit (@eval_addressing_lessdef _ _ ge sp addr (rs ## args)); eauto.
+    intros (v2 & EVAL' & LESSDEF). exploit Mem.storev_extends; eauto.
+    intros (v3 & STORE' & LESSDEF').
+    do 2 eexists; rewrite EVAL', STORE'. repeat (split; eauto).
+  - (* Bseq stop *)
+    exploit IHISTEP; eauto. intros (rs2' & m2' & IBIS & REGS' & MEMS').
+    destruct (iblock_istep_run _ _ _ _ _); try congruence.
+    destruct o, _fin; simpl in *; try congruence. eauto.
+  - (* Bseq continue *)
+    
+    (* TODO gourdinl induction pb?
+    exploit IHISTEP1; eauto. intros (rs3 & m3 & IBIS1 & REGS1 & MEMS1).
+    rewrite IBIS1; simpl. rewrite iblock_istep_run_equiv in ISTEP2.
+    exploit IHISTEP2; eauto. intros (rs4 & m4 & IBIS2 & REGS2 & MEMS2).
+    destruct o, _fin; simpl in *; try congruence; try_simplify_someHyps.
+    intros; apply IHISTEP1 in MEMS; auto.
+    exploit IHISTEP2; eauto. intros (rs3 & m3 & IBIS1 & REGS1 & MEMS1).
+    
+
+    destruct (iblock_istep_run _ _ _ _ _) eqn:EQb1.
+    2: { rewrite iblock_istep_run_equiv in ISTEP1. destruct b1; simpl in *; try congruence.
+       destruct o, _fin; simpl in *; try congruence; try_simplify_someHyps.*)
 Admitted.
 
 Local Hint Constructors lessdef_stackframe lessdef_state final_step list_forall2 step: core.
-Local Hint Unfold regs_lessdef: core.
 
 Lemma fsem2cfgsem_finalstep_simu ge stk1 f sp rs1 m1 fin t s1 stk2 rs2 m2
   (FSTEP: final_step tr_inputs ge stk1 f sp rs1 m1 fin t s1)
diff --git a/scheduling/RTLtoBTLaux.ml b/scheduling/RTLtoBTLaux.ml
index d04326ea..e709d846 100644
--- a/scheduling/RTLtoBTLaux.ml
+++ b/scheduling/RTLtoBTLaux.ml
@@ -6,7 +6,6 @@ open RTLcommonaux
 open DebugPrint
 open BTLtypes
 open BTLcommonaux
-open BTLScheduleraux
 
 let encaps_final inst osucc =
   match inst with
@@ -102,19 +101,16 @@ let rtl2btl (f : RTL.coq_function) =
   let btl = translate_function code entry join_points liveness in
   let dm = PTree.map (fun n i -> n) btl in
   (* TODO gourdinl move elsewhere *)
-  let btl' = btl_scheduler btl in
   debug "Entry %d\n" (p2i entry);
   (*debug_flag := true;*)
   debug "RTL Code: ";
   print_code code;
   debug "BTL Code:\n";
   print_btl_code stderr btl;
-  debug "Scheduled BTL Code:\n";
-  print_btl_code stderr btl';
   (*debug_flag := false;*)
   debug "Dupmap:\n";
   print_ptree print_pint dm;
   debug "Join points: ";
   print_true_nodes join_points;
   debug "\n";
-  ((btl', entry), dm)
+  ((btl, entry), dm)
diff --git a/test/c/cscript.sh b/test/c/cscript.sh
new file mode 100755
index 00000000..f797df7b
--- /dev/null
+++ b/test/c/cscript.sh
@@ -0,0 +1,21 @@
+#!/bin/bash
+
+CCREF="/home/yuki/Work/VERIMAG/Compcert_riscv_bis/ccomp -static -stdlib /home/yuki/Work/VERIMAG/Compcert_riscv_bis/runtime -fno-expanse-rtlcond -fno-expanse-others"
+CCTEST="/home/yuki/Work/VERIMAG/Compcert_riscv_third/ccomp -static -stdlib /home/yuki/Work/VERIMAG/Compcert_riscv_third/runtime -fno-expanse-rtlcond -fno-expanse-others"
+
+$CCREF nsieve.c > refout 2>&1
+mv a.out ref.out
+$CCTEST nsieve.c > testout 2>&1
+#sort -k1 -n -t, refout -o refout
+#sort -k1 -n -t, testout -o testout
+qemu-riscv64 ref.out > logref 2>&1
+{ qemu-riscv64 a.out > logtest 2>&1; } 2> logtest
+if cat logref | ack "Primes"; then
+  if cmp -s logref logtest; then
+    exit 1
+  else
+    exit 0
+  fi
+else
+  exit 1
+fi
diff --git a/test/c/cscript2.sh b/test/c/cscript2.sh
new file mode 100755
index 00000000..350c392d
--- /dev/null
+++ b/test/c/cscript2.sh
@@ -0,0 +1,5 @@
+#/bin/bash
+
+/home/gourdinl/Work/VERIMAG/Compcert_riscv_third/ccomp -static -fprepass= revlist -U__GNUC__ -stdlib ../../runtime -dclight -dasm   -c qsort.c > log 2>&1
+
+cat log | ack "instead of Some"
diff --git a/test/c/pbcompare.sh b/test/c/pbcompare.sh
new file mode 100755
index 00000000..b47c83c4
--- /dev/null
+++ b/test/c/pbcompare.sh
@@ -0,0 +1,18 @@
+#!/bin/bash
+
+CCREF="/home/yuki/Work/VERIMAG/Compcert_riscv_bis/ccomp -static -S -stdlib /home/yuki/Work/VERIMAG/Compcert_riscv_bis/runtime -fno-expanse-rtlcond -fno-expanse-others"
+CCTEST="/home/yuki/Work/VERIMAG/Compcert_riscv_third/ccomp -static -S -stdlib /home/yuki/Work/VERIMAG/Compcert_riscv_third/runtime -fno-expanse-rtlcond -fno-expanse-others"
+
+for prog in *.c; do
+  $CCREF $prog > refout 2>&1
+  $CCTEST $prog > testout 2>&1
+  sort -k1 -n -t, refout -o refout
+  sort -k1 -n -t, testout -o testout
+  if cmp -s refout testout; then
+    echo "$prog passed"
+  else
+    echo "$prog failed"
+    diff -y refout testout
+    exit 1
+  fi
+done