Add more proofs for RTLPargen correctness

3 files changed, 97 insertions, 26 deletions

diff --git a/src/hls/RTLPar.v b/src/hls/RTLPar.v
index 3707b42..1e5dd43 100644
--- a/src/hls/RTLPar.v
+++ b/src/hls/RTLPar.v
@@ -28,11 +28,15 @@ Require Import compcert.lib.Integers.
 Require Import compcert.lib.Maps.
 Require Import compcert.verilog.Op.
 
+Require Import vericert.common.Vericertlib.
 Require Import vericert.hls.RTLBlockInstr.
 
 Definition bblock_body := list (list instr).
 Definition bblock := RTLBlockInstr.bblock bblock_body.
 
+Definition is_empty (b: bblock_body) : Prop :=
+  Forall (fun n => Forall (fun m => m = RBnop) n) b.
+
 Definition code : Type := PTree.t bblock.
 
 Record function: Type := mkfunction {
@@ -140,40 +144,46 @@ Section RELSEM.
       step (Block stack f sp (mk_bblock (bb :: bbs) cfi) rs m) E0
            (Block stack f sp (mk_bblock bbs cfi) rs' m')
   | exec_RBcall:
-      forall s f sp rs m res fd ros sig args pc',
+      forall s f sp rs m res fd ros sig args pc' el,
       find_function ros rs = Some fd ->
       funsig fd = sig ->
-      step (Block s f sp (mk_bblock nil (RBcall sig ros args res pc')) rs m)
+      is_empty el ->
+      step (Block s f sp (mk_bblock el (RBcall sig ros args res pc')) rs m)
            E0 (Callstate (Stackframe res f sp pc' rs :: s) fd rs##args m)
   | exec_RBtailcall:
-      forall s f stk rs m sig ros args fd m',
+      forall s f stk rs m sig ros args fd m' el,
       find_function ros rs = Some fd ->
       funsig fd = sig ->
       Mem.free m stk 0 f.(fn_stacksize) = Some m' ->
-      step (Block s f (Vptr stk Ptrofs.zero) (mk_bblock nil (RBtailcall sig ros args)) rs m)
+      is_empty el ->
+      step (Block s f (Vptr stk Ptrofs.zero) (mk_bblock el (RBtailcall sig ros args)) rs m)
         E0 (Callstate s fd rs##args m')
   | exec_RBbuiltin:
-      forall s f sp rs m ef args res pc' vargs t vres m',
+      forall s f sp rs m ef args res pc' vargs t vres m' el,
       eval_builtin_args ge (fun r => rs#r) sp m args vargs ->
       external_call ef ge vargs m t vres m' ->
-      step (Block s f sp (mk_bblock nil (RBbuiltin ef args res pc')) rs m)
+      is_empty el ->
+      step (Block s f sp (mk_bblock el (RBbuiltin ef args res pc')) rs m)
          t (State s f sp pc' (regmap_setres res vres rs) m')
   | exec_RBcond:
-      forall s f sp rs m cond args ifso ifnot b pc',
+      forall s f sp rs m cond args ifso ifnot b pc' el,
       eval_condition cond rs##args m = Some b ->
       pc' = (if b then ifso else ifnot) ->
-      step (Block s f sp (mk_bblock nil (RBcond cond args ifso ifnot)) rs m)
+      is_empty el ->
+      step (Block s f sp (mk_bblock el (RBcond cond args ifso ifnot)) rs m)
         E0 (State s f sp pc' rs m)
   | exec_RBjumptable:
-      forall s f sp rs m arg tbl n pc',
+      forall s f sp rs m arg tbl n pc' el,
       rs#arg = Vint n ->
       list_nth_z tbl (Int.unsigned n) = Some pc' ->
-      step (Block s f sp (mk_bblock nil (RBjumptable arg tbl)) rs m)
+      is_empty el ->
+      step (Block s f sp (mk_bblock el (RBjumptable arg tbl)) rs m)
         E0 (State s f sp pc' rs m)
   | exec_Ireturn:
-      forall s f stk rs m or m',
+      forall s f stk rs m or m' el,
       Mem.free m stk 0 f.(fn_stacksize) = Some m' ->
-      step (Block s f (Vptr stk Ptrofs.zero) (mk_bblock nil (RBreturn or)) rs m)
+      is_empty el ->
+      step (Block s f (Vptr stk Ptrofs.zero) (mk_bblock el (RBreturn or)) rs m)
         E0 (Returnstate s (regmap_optget or Vundef rs) m')
   | exec_function_internal:
       forall s f args m m' stk,
diff --git a/src/hls/RTLPargen.v b/src/hls/RTLPargen.v
index f745466..d592206 100644
--- a/src/hls/RTLPargen.v
+++ b/src/hls/RTLPargen.v
@@ -485,13 +485,13 @@ Get a sequence from the basic block.
 Fixpoint abstract_sequence (f : forest) (b : list instr) : forest :=
   match b with
   | nil => f
-  | i :: l => abstract_sequence (update f i) l
+  | i :: l => update (abstract_sequence f l) i
   end.
 
 Fixpoint abstract_sequence_par (f : forest) (b : list (list instr)) : forest :=
   match b with
   | nil => f
-  | i :: l => abstract_sequence_par (abstract_sequence f i) l
+  | i :: l => abstract_sequence (abstract_sequence_par f l) i
   end.
 
 (*|
@@ -507,9 +507,21 @@ We define the top-level oracle that will check if two basic blocks are equivalen
 transformation.
 |*)
 
+Definition empty_trees (bb: RTLBlock.bblock_body) (bbt: RTLPar.bblock_body) : bool :=
+  match bb with
+  | nil =>
+    match bbt with
+    | nil => true
+    | _ => false
+    end
+  | _ => true
+  end.
+
 Definition schedule_oracle (bb: RTLBlock.bblock) (bbt: RTLPar.bblock) : bool :=
   check (abstract_sequence empty (bb_body bb))
-        (abstract_sequence_par empty (bb_body bbt)).
+        (abstract_sequence_par empty (bb_body bbt)) &&
+  check_control_flow_instr (bb_exit bb) (bb_exit bbt) &&
+  empty_trees (bb_body bb) (bb_body bbt).
 
 Definition check_scheduled_trees := beq2 schedule_oracle.
 
@@ -539,9 +551,13 @@ Proof. solve_scheduled_trees_correct. Qed.
 Parameter schedule : RTLBlock.function -> RTLPar.function.
 
 Definition transl_function (f: RTLBlock.function) : Errors.res RTLPar.function :=
-  let tf := schedule f in
-  if check_scheduled_trees f.(RTLBlock.fn_code) tf.(fn_code) then
-    Errors.OK tf
+  let tfcode := fn_code (schedule f) in
+  if check_scheduled_trees f.(RTLBlock.fn_code) tfcode then
+    Errors.OK (mkfunction f.(RTLBlock.fn_sig)
+                          f.(RTLBlock.fn_params)
+                          f.(RTLBlock.fn_stacksize)
+                          tfcode
+                          f.(RTLBlock.fn_entrypoint))
   else
     Errors.Error (Errors.msg "RTLPargen: Could not prove the blocks equivalent.").
 
diff --git a/src/hls/RTLPargenproof.v b/src/hls/RTLPargenproof.v
index 21caf7f..730ac98 100644
--- a/src/hls/RTLPargenproof.v
+++ b/src/hls/RTLPargenproof.v
@@ -18,8 +18,8 @@
 
 Require Import compcert.common.AST.
 Require Import compcert.common.Errors.
-Require Import compcert.common.Globalenvs.
 Require Import compcert.common.Linking.
+Require Import compcert.common.Globalenvs.
 Require Import compcert.lib.Maps.
 
 Require Import vericert.common.Vericertlib.
@@ -98,8 +98,38 @@ Section CORRECTNESS.
 
   Lemma senv_preserved:
     Senv.equiv (Genv.to_senv ge) (Genv.to_senv tge).
-  Proof
-    (Genv.senv_transf_partial TRANSL).
+  Proof (Genv.senv_transf_partial TRANSL).
+
+  Lemma sig_transl_function:
+    forall (f: RTLBlock.fundef) (tf: RTLPar.fundef),
+      transl_fundef f = OK tf ->
+      RTLPar.funsig tf = RTLBlock.funsig f.
+  Proof.
+    unfold transl_fundef, transf_partial_fundef, transl_function; intros;
+    repeat destruct_match; crush;
+    match goal with H: OK _ = OK _ |- _ => inv H end; auto.
+  Qed.
+
+  Lemma find_function_translated:
+    forall ros rs f,
+      RTLBlock.find_function ge ros rs = Some f ->
+      exists tf, RTLPar.find_function tge ros rs = Some tf
+                 /\ transl_fundef f = OK tf.
+  Proof.
+    destruct ros; simplify;
+    [ exploit functions_translated; eauto
+    | rewrite symbols_preserved; destruct_match;
+      try (apply function_ptr_translated); crush ].
+  Qed.
+
+  Lemma schedule_oracle_nil:
+    forall bb cfi,
+      schedule_oracle {| bb_body := nil; bb_exit := cfi |} bb = true ->
+      is_empty (bb_body bb) /\ bb_exit bb = cfi.
+  Proof.
+    unfold schedule_oracle, check_control_flow_instr, is_empty.
+    simplify; repeat destruct_match; crush.
+  Qed.
 
   Theorem transl_step_correct :
     forall (S1 : RTLBlock.state) t S2,
@@ -118,12 +148,27 @@ Section CORRECTNESS.
         destruct (check_scheduled_trees (RTLBlock.fn_code f) (fn_code (schedule f))) eqn:?;
                  [| discriminate ]; inv H2
       | [ H: context[check_scheduled_trees] |- _ ] =>
-        eapply check_scheduled_trees_correct in H; [| solve [ eauto ] ]
+        let H2 := fresh "CHECK" in
+        learn H as H2;
+        eapply check_scheduled_trees_correct in H2; [| solve [eauto] ]
+      | [ H: schedule_oracle {| bb_body := nil; bb_exit := _ |} ?bb = true |- _ ] =>
+        let H2 := fresh "SCHED" in
+        learn H as H2;
+        apply schedule_oracle_nil in H2
       | [ H: exists _, _ |- _ ] => inv H
+      | _ => progress simplify
       end.
 
-    induction 1; simplify; repeat t; simplify.
+    induction 1; repeat t.
 
-    - repeat econstructor; eauto.
-    - admit.
-    - repeat econstructor; eauto.
+    { repeat econstructor; eauto. }
+    { admit. }
+    { destruct bb'; exploit find_function_translated; simplify;
+        repeat econstructor; eauto using sig_transl_function. }
+    { destruct bb'; exploit find_function_translated; simplify;
+        repeat econstructor; eauto using sig_transl_function. }
+    { destruct bb'; simplify; subst; repeat econstructor; eauto using Events.eval_builtin_args_preserved, Events.external_call_symbols_preserved, symbols_preserved, senv_preserved, Events.E0_right. }
+    { destruct bb'; simplify; subst; repeat econstructor; eauto. }
+    { destruct bb'; simplify; subst; repeat econstructor; eauto. }
+    { destruct bb'; simplify; subst; repeat econstructor; eauto. }
+    { repeat econstructor; eauto. }