advance in cfg checker

1 files changed, 138 insertions, 1 deletions

diff --git a/scheduling/BTL.v b/scheduling/BTL.v
index 28941e01..82a54061 100644
--- a/scheduling/BTL.v
+++ b/scheduling/BTL.v
@@ -513,11 +513,148 @@ Proof.
 Qed.
 
 (* TODO: deuxième étape (après BTLtoRTLproof.plus_simulation) *)
-Parameter verify_block: PTree.t node -> RTL.code -> bool -> node -> iblock -> res (option node).
+Fixpoint verify_block (dupmap: PTree.t node) cfg isfst pc ib : res (option node) :=
+  match ib with
+  | BF fi =>
+      match fi with
+      | Bgoto pc =>
+          match dupmap!pc with
+          | Some _ => OK None
+          | None => Error (msg "verify_block: incorrect dupmap Bgoto")
+          end
+      | _ =>
+          match cfg!pc with
+          | Some i => Error (msg "TODO") (* TODO *)
+          | None => Error (msg "verify_block: incorrect cfg BF")
+          end
+      end
+  | Bnop =>
+      match cfg!pc with
+      | Some (Inop pc') => OK (Some pc')
+      | _ => Error (msg "verify_block: incorrect cfg Bnop")
+      end
+  | Bop op lr r =>
+      match cfg!pc with
+      | Some (Iop op' lr' r' pc') =>
+          if (eq_operation op op') then
+            if (list_eq_dec Pos.eq_dec lr lr') then
+              if (Pos.eq_dec r r') then
+                OK (Some pc')
+              else Error (msg "verify_block: different r in Bop")
+            else Error (msg "verify_block: different lr in Bop")
+          else Error (msg "verify_block: different operations in Bop")
+      | _ => Error (msg "verify_block: incorrect cfg Bop")
+      end
+  | Bload tm m a lr r =>
+      match cfg!pc with
+      | Some (Iload tm' m' a' lr' r' pc') =>
+          if (trapping_mode_eq tm tm') then
+            if (chunk_eq m m') then
+              if (eq_addressing a a') then
+                if (list_eq_dec Pos.eq_dec lr lr') then
+                  if (Pos.eq_dec r r') then
+                    OK (Some pc')
+                  else Error (msg "verify_block: different r in Bload")
+                else Error (msg "verify_block: different lr in Bload")
+              else Error (msg "verify_block: different addressing in Bload")
+            else Error (msg "verify_block: different mchunk in Bload")
+          else Error (msg "verify_block: different trapping_mode in Bload")
+      | _ => Error (msg "verify_block: incorrect cfg Bload")
+      end
+  | Bstore m a lr r =>
+      match cfg!pc with
+      | Some (Istore m' a' lr' r' pc') =>
+          if (chunk_eq m m') then
+            if (eq_addressing a a') then
+              if (list_eq_dec Pos.eq_dec lr lr') then
+                if (Pos.eq_dec r r') then OK (Some pc')
+                else Error (msg "verify_block: different r in Bstore")
+              else Error (msg "verify_block: different lr in Bstore")
+            else Error (msg "verify_block: different addressing in Bstore")
+          else Error (msg "verify_block: different mchunk in Bstore")
+      | _ => Error (msg "verify_block: incorrect cfg Bstore")
+      end
+  | Bseq b1 b2 =>
+      do opc <- verify_block dupmap cfg isfst pc b1;
+      match opc with
+      | Some pc' =>
+          verify_block dupmap cfg false pc' b2
+      | None => Error (msg "verify_block: None next pc in Bseq (deadcode)")
+      end
+  | Bcond c lr bso bnot i =>
+      match cfg!pc with
+      | Some (Icond c' lr' pcso pcnot i') =>
+          if (list_eq_dec Pos.eq_dec lr lr') then
+            if (eq_condition c c') then
+              do opc1 <- verify_block dupmap cfg false pcso bso;
+              do opc2 <- verify_block dupmap cfg false pcnot bnot;
+              match opc1, opc2 with
+              | None, o => OK o
+              | o, None => OK o
+              | Some x, Some x' =>
+                  if Pos.eq_dec x x' then OK (Some x)
+                  else Error (msg "verify_block: is_join_opt incorrect for Bcond")
+              end
+            else Error (msg "verify_block: incompatible conditions in Bcond")
+          else Error (msg "verify_block: different lr in Bcond")
+      | _ => Error (msg "verify_block: incorrect cfg Bcond")
+      end
+  end.
 
 (* This property expresses that "relation" [match_iblock] is a partial function (see also [iblock_istep_run_equiv] above) *)
 Lemma verify_block_correct: forall dupmap cfg isfst pc ib fin,
    verify_block dupmap cfg isfst pc ib = (OK fin) -> match_iblock dupmap cfg isfst pc ib fin.
+Proof.
+  induction ib; intros;
+  try (unfold verify_block in H; destruct (cfg!pc) eqn:EQCFG; [ idtac | discriminate; fail ]).
+  - admit.
+  - (* Bnop *)
+    destruct i; inv H.
+    constructor; assumption.
+  - (* Bop *)
+    destruct i; try discriminate.
+    destruct (eq_operation _ _); try discriminate.
+    destruct (list_eq_dec _ _ _); try discriminate.
+    destruct (Pos.eq_dec _ _); try discriminate. inv H.
+    constructor; assumption.
+  - (* Bload *)
+    destruct i; try discriminate.
+    destruct (trapping_mode_eq _ _); try discriminate.
+    destruct (chunk_eq _ _); try discriminate.
+    destruct (eq_addressing _ _); try discriminate.
+    destruct (list_eq_dec _ _ _); try discriminate.
+    destruct (Pos.eq_dec _ _); try discriminate. inv H.
+    constructor; assumption.
+  - (* Bstore *)
+    destruct i; try discriminate.
+    destruct (chunk_eq _ _); try discriminate.
+    destruct (eq_addressing _ _); try discriminate.
+    destruct (list_eq_dec _ _ _); try discriminate.
+    destruct (Pos.eq_dec _ _); try discriminate. inv H.
+    constructor; assumption.
+  - (* Bseq *)
+    monadInv H.
+    destruct x; try discriminate.
+    eapply mib_seq_Some.
+    eapply IHib1; eauto. admit.
+    (*eapply IHib2; eauto.*)
+    (*destruct (cfg!pc) eqn:ECFG; try discriminate.*)
+    (*destruct i; try discriminate.*)
+  - (* Bcond *)
+    destruct i; try discriminate.
+    destruct (list_eq_dec _ _ _); try discriminate.
+    destruct (eq_condition _ _); try discriminate.
+    fold (verify_block dupmap cfg false n ib1) in H.
+    fold (verify_block dupmap cfg false n0 ib2) in H.
+    monadInv H.
+    destruct x, x0; try destruct (Pos.eq_dec _ _); try discriminate.
+    + inv EQ2. eapply mib_cond; eauto.
+      admit.
+      admit.
+      admit.
+    + admit.
+    + admit.
+    + admit.
 Admitted.
 Local Hint Resolve verify_block_correct: core.