Completely finish RTLBlockgenproof

2 files changed, 171 insertions, 24 deletions

diff --git a/src/hls/RTLBlockgen.v b/src/hls/RTLBlockgen.v
index 8b0ea65..cb18147 100644
--- a/src/hls/RTLBlockgen.v
+++ b/src/hls/RTLBlockgen.v
@@ -179,17 +179,117 @@ Definition check_present_blocks (c: code) (n: list positive) (max: positive) (i:
   | None => false
   end.
 
+Definition check_valid_node (tc: code) (e: node) :=
+  match tc ! e with
+  | Some _ => true
+  | _ => false
+  end.
+
+Fixpoint check_code' (c: RTL.code) (tc: code) (pc: node) (b: bb) (i: cf_instr) :=
+  match b, i, c ! pc with
+  | RBnop :: (_ :: _) as b', _, Some (RTL.Inop pc') =>
+      check_code' c tc pc' b' i
+  | RBop None op args dst :: (_ :: _) as b', _, Some (RTL.Iop op' args' dst' pc') =>
+      ceq operation_eq op op'
+      && ceq list_pos_eq args args'
+      && ceq peq dst dst'
+      && check_code' c tc pc' b' i
+  | RBload None chunk addr args dst :: (_ :: _) as b', _,
+    Some (RTL.Iload chunk' addr' args' dst' pc') =>
+      ceq memory_chunk_eq chunk chunk'
+      && ceq addressing_eq addr addr'
+      && ceq list_pos_eq args args'
+      && ceq peq dst dst'
+      && check_code' c tc pc' b' i
+  | RBstore None chunk addr args src :: (_ :: _) as b', _,
+    Some (RTL.Istore chunk' addr' args' src' pc') =>
+      ceq memory_chunk_eq chunk chunk'
+      && ceq addressing_eq addr addr'
+      && ceq list_pos_eq args args'
+      && ceq peq src src'
+      && check_code' c tc pc' b' i
+  | RBnop :: nil, RBgoto pc', Some (RTL.Inop pc'') =>
+      check_valid_node tc pc'
+      && ceq peq pc' pc''
+  | RBop None op args dst :: nil, RBgoto pc', Some (RTL.Iop op' args' dst' pc'') =>
+      check_valid_node tc pc'
+      && ceq peq pc' pc''
+      && ceq operation_eq op op'
+      && ceq list_pos_eq args args'
+      && ceq peq dst dst'
+  | RBload None chunk addr args dst :: nil, RBgoto pc',
+    Some (RTL.Iload chunk' addr' args' dst' pc'') =>
+      check_valid_node tc pc'
+      && ceq peq pc' pc''
+      && ceq memory_chunk_eq chunk chunk'
+      && ceq addressing_eq addr addr'
+      && ceq list_pos_eq args args'
+      && ceq peq dst dst'
+  | RBstore None chunk addr args src :: nil, RBgoto pc',
+    Some (RTL.Istore chunk' addr' args' src' pc'') =>
+      check_valid_node tc pc'
+      && ceq peq pc' pc''
+      && ceq memory_chunk_eq chunk chunk'
+      && ceq addressing_eq addr addr'
+      && ceq list_pos_eq args args'
+      && ceq peq src src'
+  | RBnop :: nil, RBcall sig (inl r) args dst pc',
+    Some (RTL.Icall sig' (inl r') args' dst' pc'') =>
+      check_valid_node tc pc'
+      && ceq peq pc' pc''
+      && ceq signature_eq sig sig'
+      && ceq peq r r'
+      && ceq list_pos_eq args args'
+      && ceq peq dst dst'
+  | RBnop :: nil, RBcall sig (inr i) args dst pc',
+    Some (RTL.Icall sig' (inr i') args' dst' pc'') =>
+      check_valid_node tc pc'
+      && ceq peq pc' pc''
+      && ceq signature_eq sig sig'
+      && ceq peq i i'
+      && ceq list_pos_eq args args'
+      && ceq peq dst dst'
+  | RBnop :: nil, RBtailcall sig' (inl r') args',
+    Some (RTL.Itailcall sig (inl r) args) =>
+      ceq signature_eq sig sig'
+      && ceq peq r r'
+      && ceq list_pos_eq args args'
+  | RBnop :: nil, RBtailcall sig' (inr r') args',
+    Some (RTL.Itailcall sig (inr r) args) =>
+      ceq signature_eq sig sig'
+      && ceq peq r r'
+      && ceq list_pos_eq args args'
+  | RBnop :: nil, RBcond cond' args' n1' n2', Some (RTL.Icond cond args n1 n2) =>
+      check_valid_node tc n1
+      && check_valid_node tc n2
+      && ceq condition_eq cond cond'
+      && ceq list_pos_eq args args'
+      && ceq peq n1 n1'
+      && ceq peq n2 n2'
+  | RBnop :: nil, RBjumptable r' ns', Some (RTL.Ijumptable r ns) =>
+      ceq peq r r'
+      && ceq list_pos_eq ns ns'
+      && forallb (check_valid_node tc) ns
+  | RBnop :: nil, RBreturn (Some r'), Some (RTL.Ireturn (Some r)) =>
+      ceq peq r r'
+  | RBnop :: nil, RBreturn None, Some (RTL.Ireturn None) => true
+  | _, _, _ => false
+  end.
+
+Definition check_code c tc pc b :=
+  check_code' c tc pc b.(bb_body) b.(bb_exit).
+
 Parameter partition : RTL.function -> Errors.res function.
 
 Definition transl_function (f: RTL.function) :=
   match partition f with
   | Errors.OK f' =>
-      let blockids := map fst (PTree.elements f'.(fn_code)) in
-      if forall_ptree (check_present_blocks f'.(fn_code) blockids (fold_right Pos.max 1 blockids))
-                      f.(RTL.fn_code) then
-        Errors.OK
-          (mkfunction f.(RTL.fn_sig) f.(RTL.fn_params) f.(RTL.fn_stacksize) f'.(fn_code) f.(RTL.fn_entrypoint))
-      else Errors.Error (Errors.msg "check_present_blocks failed")
+      if check_valid_node f'.(fn_code) f.(RTL.fn_entrypoint) then
+        if forall_ptree (check_code f.(RTL.fn_code) f'.(fn_code)) f'.(fn_code) then
+          Errors.OK
+            (mkfunction f.(RTL.fn_sig) f.(RTL.fn_params) f.(RTL.fn_stacksize) f'.(fn_code) f.(RTL.fn_entrypoint))
+        else Errors.Error (Errors.msg "check_present_blocks failed")
+      else Errors.Error (Errors.msg "entrypoint does not exists")
   | Errors.Error msg => Errors.Error msg
   end.
 
diff --git a/src/hls/RTLBlockgenproof.v b/src/hls/RTLBlockgenproof.v
index 875c582..642264f 100644
--- a/src/hls/RTLBlockgenproof.v
+++ b/src/hls/RTLBlockgenproof.v
@@ -35,6 +35,7 @@ Require Import compcert.common.Memory.
 Require Import compcert.common.Values.
 
 Require Import vericert.common.Vericertlib.
+Require Import vericert.common.DecEq.
 Require Import vericert.hls.RTLBlockInstr.
 Require Import vericert.hls.RTLBlock.
 Require Import vericert.hls.RTLBlockgen.
@@ -325,6 +326,65 @@ whole execution (in one big step) of the basic block.
     | Some b' => 1 + length b'
     end.
 
+  Lemma check_valid_node_correct :
+    forall a b, check_valid_node a b = true -> valid_succ a b.
+  Proof.
+    intros. unfold valid_succ, check_valid_node in *.
+    destruct_match; try discriminate; eauto.
+  Qed.
+
+  Lemma transl_entrypoint_exists :
+    forall f tf,
+      transl_function f = OK tf ->
+      valid_succ (fn_code tf) (fn_entrypoint tf).
+  Proof.
+    unfold transl_function; intros.
+    repeat (destruct_match; try discriminate; []). inv H. simplify.
+    eauto using check_valid_node_correct.
+  Qed.
+
+  Lemma ceq_eq :
+    forall A a (b: A) c,
+      ceq a b c = true ->
+      b = c.
+  Proof.
+    intros. unfold ceq in H. destruct_match; try discriminate. auto.
+  Qed.
+
+  Ltac unfold_ands :=
+    repeat match goal with
+           | H: _ && _ = true |- _ => apply andb_prop in H
+           | H: _ /\ _ |- _ => inv H
+           | H: ceq _ _ _ = true |- _ => apply ceq_eq in H; subst
+           end.
+
+  Lemma transl_match_code' :
+    forall c tc b pc i,
+      check_code' c tc pc b i = true ->
+      match_block c tc pc b i.
+  Proof.
+    induction b; [crush|].
+    intros. unfold check_code' in H.
+    do 4 (destruct_match; try discriminate);
+    try (repeat (destruct_match; try discriminate; []); unfold_ands; constructor; auto using check_valid_node_correct);
+    fold check_code' in *;
+    try (destruct_match; try discriminate; unfold_ands; econstructor; eauto);
+    apply Forall_forall; intros. eapply forallb_forall in H1; eauto using check_valid_node_correct.
+  Qed.
+
+  Lemma transl_match_code :
+    forall f tf,
+      transl_function f = OK tf ->
+      match_code f.(RTL.fn_code) tf.(fn_code).
+  Proof.
+    unfold transl_function; intros.
+    repeat (destruct_match; try discriminate; []). inv H. simplify.
+    unfold match_code; intros.
+    eapply forall_ptree_true in Heqb0; eauto.
+    unfold check_code in *.
+    eauto using transl_match_code'.
+  Qed.
+
   Lemma transl_initial_states :
     forall s1, RTL.initial_state prog s1 ->
       exists s2, RTLBlock.initial_state tprog s2 /\ match_states None s1 s2.
@@ -751,18 +811,6 @@ whole execution (in one big step) of the basic block.
     unfold sem_extrap. intros. setoid_rewrite H5 in H8. crush.
   Qed.
 
-  Lemma transl_entrypoint_exists :
-    forall f tf,
-      transl_function f = OK tf ->
-      exists b, (fn_code tf) ! (fn_entrypoint tf) = Some b.
-  Proof. Admitted.
-
-  Lemma transl_match_code :
-    forall f tf,
-      transl_function f = OK tf ->
-      match_code f.(RTL.fn_code) tf.(fn_code).
-  Proof. Admitted.
-
   Lemma init_regs_equiv :
     forall b a, init_regs a b = RTL.init_regs a b.
   Proof. induction b; crush. Qed.
@@ -781,9 +829,8 @@ whole execution (in one big step) of the basic block.
     inversion 1; subst; simplify.
     monadInv TF. inv H0.
     pose proof (transl_match_code _ _ EQ).
-    pose proof (transl_entrypoint_exists _ _ EQ).
+    pose proof (transl_entrypoint_exists _ _ EQ). unfold valid_succ in H1.
     simplify.
-    exploit transl_entrypoint_exists; eauto; simplify.
     destruct x0.
     apply sim_plus. do 3 econstructor.
     assert (fn_stacksize x = RTL.fn_stacksize f).
@@ -802,14 +849,14 @@ whole execution (in one big step) of the basic block.
       repeat (destruct_match; try discriminate; []).
       inv EQ; auto. }
     unfold match_code in H0.
-    pose proof (H0 _ _ H3).
+    pose proof (H0 _ _ H2).
     econstructor; eauto.
     rewrite <- H1. eauto.
     rewrite H1.
-    rewrite init_regs_equiv. rewrite H4. eapply star_refl.
+    rewrite init_regs_equiv. rewrite H3. eapply star_refl.
     unfold sem_extrap; intros.
-    setoid_rewrite H2 in H7; simplify.
-    rewrite H4. eauto.
+    setoid_rewrite H2 in H6; simplify.
+    rewrite H3. eauto.
   Qed.
 
   Lemma transl_externalcall_correct: