diff options
| -rw-r--r-- | Makefile | 4 | ||||
| -rw-r--r-- | riscV/OpWeights.ml | 2 | ||||
| -rw-r--r-- | scheduling/RTLpath.v | 5 | ||||
| -rw-r--r-- | scheduling/RTLpathScheduler.v | 18 | ||||
| -rw-r--r-- | scheduling/RTLpathWFcheck.v | 201 |
5 files changed, 215 insertions, 15 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/) @@ -278,7 +278,7 @@ latexdoc: # (currently: export extra Coq-functions for OCaml code, depending on the target) extraction/extraction.v: Makefile extraction/extraction.vexpand (echo "(* WARNING: this file is generated from extraction.vexpand *)"; \ - echo "(* by the Makefile -- target \"extraction/extraction.v\" *)\n"; \ + echo "(* by the Makefile -- target \"extraction/extraction.v\" *)"; \ cat extraction/extraction.vexpand; \ echo "$(EXTRA_EXTRACTION)"; \ echo ".") > extraction/extraction.v diff --git a/riscV/OpWeights.ml b/riscV/OpWeights.ml index 09760db9..5ac318c8 100644 --- a/riscV/OpWeights.ml +++ b/riscV/OpWeights.ml @@ -116,7 +116,7 @@ module SweRV_EH1 = | Omul | Omulhs | Omulhu | Omull | Omullhs | Omullhu -> [| 1 ; 0 ; 1 |] | Odiv | Odivu | Odivl | Odivlu -> [| 0 ; 0; 0 |] - | _ -> [| 1; 0; 0; 0 |];; + | _ -> [| 1; 0; 0 |];; let non_pipelined_resources_of_op (op : operation) (nargs : int) = match op with diff --git a/scheduling/RTLpath.v b/scheduling/RTLpath.v index 35512652..cccc8147 100644 --- a/scheduling/RTLpath.v +++ b/scheduling/RTLpath.v @@ -91,8 +91,7 @@ Record path_info := { Definition path_map: Type := PTree.t path_info. -Definition path_entry (*c:code*) (pm: path_map) (n: node): Prop - := pm!n <> None (*/\ c!n <> None*). +Definition path_entry (pm: path_map) (n: node): Prop := pm!n <> None. Inductive wellformed_path (c:code) (pm: path_map): nat -> node -> Prop := | wf_last_node i pc: @@ -119,7 +118,7 @@ Record function : Type := { fn_RTL:> RTL.function; fn_path: path_map; (* condition 1 below: the entry-point of the code is an entry-point of a path *) - fn_entry_point_wf: path_entry (*fn_RTL.(fn_code)*) fn_path fn_RTL.(fn_entrypoint); + fn_entry_point_wf: path_entry fn_path fn_RTL.(fn_entrypoint); (* condition 2 below: the path_map is well-formed *) fn_path_wf: wellformed_path_map fn_RTL.(fn_code) fn_path }. diff --git a/scheduling/RTLpathScheduler.v b/scheduling/RTLpathScheduler.v index b98a01b9..01a11cb3 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,15 +32,15 @@ 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 -(* | false => Error (msg "In function_builder: (tfr, tpm) is not wellformed") *) - | _ => OK {| fn_RTL := tfr; fn_path := tpm |} + 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. Admitted. -(* apply function_checker_path_entry. auto. *) -(* Defined. *) Next Obligation. Admitted. -(* apply function_checker_wellformed_path_map. auto. -Defined. *) +Next Obligation. + apply RTLpathWFcheck.function_checker_path_entry. auto. +Defined. Next Obligation. + apply RTLpathWFcheck.function_checker_wellformed_path_map. auto. +Defined. Definition entrypoint_check (dm: PTree.t node) (fr tfr: RTL.function) : res unit := match dm ! (fn_entrypoint tfr) with diff --git a/scheduling/RTLpathWFcheck.v b/scheduling/RTLpathWFcheck.v new file mode 100644 index 00000000..f5198e68 --- /dev/null +++ b/scheduling/RTLpathWFcheck.v @@ -0,0 +1,201 @@ +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 lazy_and_Some_true A (o: option A) (b: bool): o &&& b = true <-> (exists v, o = Some v) /\ b = true. +Proof. + destruct o; simpl; intuition. + - eauto. + - firstorder. try_simplify_someHyps. +Qed. + +Lemma lazy_and_Some_tt_true (o: option unit) (b: bool): o &&& b = true <-> o = Some tt /\ b = true. +Proof. + intros; rewrite lazy_and_Some_true; firstorder. + destruct x; auto. +Qed. + +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 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 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 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. |