aboutsummaryrefslogtreecommitdiffstats
path: root/scheduling/RTLpathWFcheck.v
diff options
context:
space:
mode:
Diffstat (limited to 'scheduling/RTLpathWFcheck.v')
-rw-r--r--scheduling/RTLpathWFcheck.v187
1 files changed, 0 insertions, 187 deletions
diff --git a/scheduling/RTLpathWFcheck.v b/scheduling/RTLpathWFcheck.v
deleted file mode 100644
index 63b914ec..00000000
--- a/scheduling/RTLpathWFcheck.v
+++ /dev/null
@@ -1,187 +0,0 @@
-Require Import Coqlib.
-Require Import Maps.
-Require Import Lattice.
-Require Import AST.
-Require Import Op.
-Require Import Registers.
-Require Import Globalenvs Smallstep RTL RTLpath.
-Require Import Bool Errors.
-Require Import Program.
-Require RTLpathLivegen.
-
-Local Open Scope lazy_bool_scope.
-
-Local Open Scope option_monad_scope.
-
-Definition exit_checker {A} (pm: path_map) (pc: node) (v:A): option A :=
- SOME path <- pm!pc IN
- Some v.
-
-Lemma exit_checker_path_entry A (pm: path_map) (pc: node) (v:A) res:
- exit_checker pm pc v = Some res -> path_entry pm pc.
-Proof.
- unfold exit_checker, path_entry.
- inversion_SOME path; simpl; congruence.
-Qed.
-
-Lemma exit_checker_res A (pm: path_map) (pc: node) (v:A) res:
- exit_checker pm pc v = Some res -> v=res.
-Proof.
- unfold exit_checker, path_entry.
- inversion_SOME path; try_simplify_someHyps.
-Qed.
-
-Definition iinst_checker (pm: path_map) (i: instruction): option (node) :=
- match i with
- | Inop pc' | Iop _ _ _ pc' | Iload _ _ _ _ _ pc'
- | Istore _ _ _ _ pc' => Some (pc')
- | Icond cond args ifso ifnot _ =>
- exit_checker pm ifso ifnot
- | _ => None
- end.
-
-Local Hint Resolve exit_checker_path_entry: core.
-
-Lemma iinst_checker_path_entry (pm: path_map) (i: instruction) res pc:
- iinst_checker pm i = Some res ->
- early_exit i = Some pc -> path_entry pm pc.
-Proof.
- destruct i; simpl; try_simplify_someHyps; subst.
-Qed.
-
-Lemma iinst_checker_default_succ (pm: path_map) (i: instruction) res pc:
- iinst_checker pm i = Some res ->
- pc = res ->
- default_succ i = Some pc.
-Proof.
- destruct i; simpl; try_simplify_someHyps; subst;
- repeat (inversion_ASSERT); try_simplify_someHyps.
- intros; exploit exit_checker_res; eauto.
- intros; subst. simpl; auto.
-Qed.
-
-Fixpoint ipath_checker (ps:nat) (f: RTL.function) (pm: path_map) (pc:node): option (node) :=
- match ps with
- | O => Some (pc)
- | S p =>
- SOME i <- f.(fn_code)!pc IN
- SOME res <- iinst_checker pm i IN
- ipath_checker p f pm res
- end.
-
-Lemma ipath_checker_wellformed f pm ps: forall pc res,
- ipath_checker ps f pm pc = Some res ->
- wellformed_path f.(fn_code) pm 0 res ->
- wellformed_path f.(fn_code) pm ps pc.
-Proof.
- induction ps; simpl; try_simplify_someHyps.
- inversion_SOME i; inversion_SOME res'.
- intros. eapply wf_internal_node; eauto.
- * eapply iinst_checker_default_succ; eauto.
- * intros; eapply iinst_checker_path_entry; eauto.
-Qed.
-
-Fixpoint exit_list_checker (pm: path_map) (l: list node): bool :=
- match l with
- | nil => true
- | pc::l' => exit_checker pm pc tt &&& exit_list_checker pm l'
- end.
-
-Lemma exit_list_checker_correct pm l pc:
- exit_list_checker pm l = true -> List.In pc l -> exit_checker pm pc tt = Some tt.
-Proof.
- intros EXIT PC; induction l; intuition.
- simpl in * |-. rewrite RTLpathLivegen.lazy_and_Some_tt_true in EXIT.
- firstorder (subst; eauto).
-Qed.
-
-Local Hint Resolve exit_list_checker_correct: core.
-
-Definition inst_checker (pm: path_map) (i: instruction): option unit :=
- match i with
- | Icall sig ros args res pc' =>
- exit_checker pm pc' tt
- | Itailcall sig ros args =>
- Some tt
- | Ibuiltin ef args res pc' =>
- exit_checker pm pc' tt
- | Ijumptable arg tbl =>
- ASSERT exit_list_checker pm tbl IN
- Some tt
- | Ireturn optarg =>
- Some tt
- | _ =>
- SOME res <- iinst_checker pm i IN
- exit_checker pm res tt
- end.
-
-Lemma inst_checker_wellformed (c:code) pc (pm: path_map) (i: instruction):
- inst_checker pm i = Some tt ->
- c!pc = Some i -> wellformed_path c pm 0 pc.
-Proof.
- intros CHECK PC. eapply wf_last_node; eauto.
- clear c pc PC. intros pc PC.
- destruct i; simpl in * |- *; intuition (subst; eauto);
- try (generalize CHECK; clear CHECK; try (inversion_SOME path); repeat inversion_ASSERT; try_simplify_someHyps).
- intros X; exploit exit_checker_res; eauto.
- clear X. intros; subst; eauto.
-Qed.
-
-Definition path_checker (f: RTL.function) pm (pc: node) (path:path_info): option unit :=
- SOME res <- ipath_checker (path.(psize)) f pm pc IN
- SOME i <- f.(fn_code)!res IN
- inst_checker pm i.
-
-Lemma path_checker_wellformed f pm pc path:
- path_checker f pm pc path = Some tt -> wellformed_path (f.(fn_code)) pm (path.(psize)) pc.
-Proof.
- unfold path_checker.
- inversion_SOME res.
- inversion_SOME i.
- intros; eapply ipath_checker_wellformed; eauto.
- eapply inst_checker_wellformed; eauto.
-Qed.
-
-Fixpoint list_path_checker f pm (l:list (node*path_info)): bool :=
- match l with
- | nil => true
- | (pc, path)::l' =>
- path_checker f pm pc path &&& list_path_checker f pm l'
- end.
-
-Lemma list_path_checker_correct f pm l:
- list_path_checker f pm l = true -> forall e, List.In e l -> path_checker f pm (fst e) (snd e) = Some tt.
-Proof.
- intros CHECKER e H; induction l as [|(pc & path) l]; intuition.
- simpl in * |- *. rewrite RTLpathLivegen.lazy_and_Some_tt_true in CHECKER. intuition (subst; auto).
-Qed.
-
-Definition function_checker (f: RTL.function) (pm: path_map): bool :=
- pm!(f.(fn_entrypoint)) &&& list_path_checker f pm (PTree.elements pm).
-
-Lemma function_checker_correct f pm pc path:
- function_checker f pm = true ->
- pm!pc = Some path ->
- path_checker f pm pc path = Some tt.
-Proof.
- unfold function_checker; rewrite RTLpathLivegen.lazy_and_Some_true.
- intros (ENTRY & PATH) PC.
- exploit list_path_checker_correct; eauto.
- - eapply PTree.elements_correct; eauto.
- - simpl; auto.
-Qed.
-
-Lemma function_checker_wellformed_path_map f pm:
- function_checker f pm = true -> wellformed_path_map f.(fn_code) pm.
-Proof.
- unfold wellformed_path_map.
- intros; eapply path_checker_wellformed; eauto.
- intros; eapply function_checker_correct; eauto.
-Qed.
-
-Lemma function_checker_path_entry f pm:
- function_checker f pm = true -> path_entry pm (f.(fn_entrypoint)).
-Proof.
- unfold function_checker; rewrite RTLpathLivegen.lazy_and_Some_true;
- unfold path_entry. firstorder congruence.
-Qed.
generated by cgit (git 2.34.1) at 2024-05-20 02:30:03 +0000