diff options
author | Sylvain Boulmé <sylvain.boulme@univ-grenoble-alpes.fr> | 2021-02-10 16:41:06 +0100 |
---|---|---|
committer | Sylvain Boulmé <sylvain.boulme@univ-grenoble-alpes.fr> | 2021-02-10 16:41:06 +0100 |
commit | aaaa8f529716876a61f9405f4f696fc09505370a (patch) | |
tree | 6064d6be6cb4cc2d1478737a63c46817c6f9a277 | |
parent | df1038971b3124ae8c5d1b48409d4df3ac906961 (diff) | |
parent | 52faac3240cf454d68ed95fdd3985df88f9e6c80 (diff) | |
download | compcert-kvx-aaaa8f529716876a61f9405f4f696fc09505370a.tar.gz compcert-kvx-aaaa8f529716876a61f9405f4f696fc09505370a.zip |
Merge branch 'CompCert_RTLpath_simuX' into kvx-work
-rw-r--r-- | Makefile | 2 | ||||
-rw-r--r-- | scheduling/RTLpathScheduler.v | 8 | ||||
-rw-r--r-- | scheduling/RTLpathWFcheck.v | 188 |
3 files changed, 193 insertions, 5 deletions
@@ -140,7 +140,7 @@ SCHEDULING= \ RTLpathLivegen.v RTLpathSE_impl.v \ RTLpathproof.v RTLpathSE_theory.v \ RTLpathSchedulerproof.v RTLpath.v \ - RTLpathScheduler.v + RTLpathScheduler.v RTLpathWFcheck.v # C front-end modules (in cfrontend/) diff --git a/scheduling/RTLpathScheduler.v b/scheduling/RTLpathScheduler.v index beab405f..6f90b455 100644 --- a/scheduling/RTLpathScheduler.v +++ b/scheduling/RTLpathScheduler.v @@ -7,7 +7,7 @@ This module is inspired from [Duplicate] and [Duplicateproof] Require Import AST Linking Values Maps Globalenvs Smallstep Registers. Require Import Coqlib Maps Events Errors Op. Require Import RTL RTLpath RTLpathLivegen RTLpathLivegenproof RTLpathSE_theory RTLpathSE_impl. - +Require RTLpathWFcheck. Notation "'ASSERT' A 'WITH' MSG 'IN' B" := (if A then B else Error (msg MSG)) (at level 200, A at level 100, B at level 200) @@ -32,14 +32,14 @@ Extract Constant untrusted_scheduler => "RTLpathScheduleraux.scheduler". Program Definition function_builder (tfr: RTL.function) (tpm: path_map) : { r : res RTLpath.function | forall f', r = OK f' -> fn_RTL f' = tfr} := - match RTLpathLivegen.function_checker tfr tpm with + match RTLpathWFcheck.function_checker tfr tpm with | false => Error (msg "In function_builder: (tfr, tpm) is not wellformed") | true => OK {| fn_RTL := tfr; fn_path := tpm |} end. Next Obligation. - apply function_checker_path_entry. auto. + apply RTLpathWFcheck.function_checker_path_entry. auto. Defined. Next Obligation. - apply function_checker_wellformed_path_map. auto. + apply RTLpathWFcheck.function_checker_wellformed_path_map. auto. Defined. Definition entrypoint_check (dm: PTree.t node) (fr tfr: RTL.function) : res unit := diff --git a/scheduling/RTLpathWFcheck.v b/scheduling/RTLpathWFcheck.v new file mode 100644 index 00000000..0ddc3142 --- /dev/null +++ b/scheduling/RTLpathWFcheck.v @@ -0,0 +1,188 @@ +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. + +(* FIXME - what about trap? *) +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 (* TODO jumptable ? *) + 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. |