diff options
Diffstat (limited to 'scheduling/RTLpathLivegen.v')
| -rw-r--r-- | scheduling/RTLpathLivegen.v | 17 |
1 files changed, 15 insertions, 2 deletions
diff --git a/scheduling/RTLpathLivegen.v b/scheduling/RTLpathLivegen.v index 7855d375..9f646ad0 100644 --- a/scheduling/RTLpathLivegen.v +++ b/scheduling/RTLpathLivegen.v @@ -46,7 +46,6 @@ Proof. inversion_ASSERT; try_simplify_someHyps. Qed. -(* FIXME - what about trap? *) Definition iinst_checker (pm: path_map) (alive: Regset.t) (i: instruction): option (Regset.t * node) := match i with | Inop pc' => Some (alive, pc') @@ -63,7 +62,7 @@ Definition iinst_checker (pm: path_map) (alive: Regset.t) (i: instruction): opti | Icond cond args ifso ifnot _ => ASSERT list_mem args alive IN exit_checker pm alive ifso (alive, ifnot) - | _ => None (* TODO jumptable ? *) + | _ => None end. @@ -109,6 +108,20 @@ Proof. * intros; eapply iinst_checker_path_entry; eauto. Qed. + +Lemma ipath_checker_default_succ (f: RTLpath.function) path: forall alive pc res, + ipath_checker path f (fn_path f) alive pc = Some res + -> nth_default_succ (fn_code f) path pc = Some (snd res). +Proof. + induction path; simpl. + + try_simplify_someHyps. + + intros alive pc res. + inversion_SOME i; intros INST. + inversion_SOME res0; intros ICHK IPCHK. + rewrite INST. + erewrite iinst_checker_default_succ; eauto. +Qed. + Definition reg_option_mem (or: option reg) (alive: Regset.t) := match or with None => true | Some r => Regset.mem r alive end. |