From 8a57683e35e761389e0ca976d79f2a5a4c387733 Mon Sep 17 00:00:00 2001 From: Sylvain Boulmé Date: Mon, 8 Feb 2021 14:01:06 +0100 Subject: intro RTLpathWFcheck --- Makefile | 2 +- scheduling/RTLpathScheduler.v | 8 ++++---- scheduling/RTLpathWFcheck.v | 28 ++++++++++++++++++++++++++++ 3 files changed, 33 insertions(+), 5 deletions(-) create mode 100644 scheduling/RTLpathWFcheck.v diff --git a/Makefile b/Makefile index aabd01a4..9adeb6db 100644 --- a/Makefile +++ b/Makefile @@ -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..eca5b24e --- /dev/null +++ b/scheduling/RTLpathWFcheck.v @@ -0,0 +1,28 @@ +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 function_checker (f: RTL.function) (pm: path_map): bool := + pm!(f.(fn_entrypoint)) &&& true. (* TODO: &&& list_path_checker f pm (PTree.elements pm) *) + +Lemma function_checker_wellformed_path_map f pm: + function_checker f pm = true -> wellformed_path_map f.(fn_code) pm. +Admitted. + +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. -- cgit From 0d41f5a2c9b7f1f01e142211edcc498b40c7506f Mon Sep 17 00:00:00 2001 From: Léo Gourdin Date: Mon, 8 Feb 2021 15:25:13 +0100 Subject: Checker for wellformed path --- scheduling/RTLpathWFcheck.v | 177 +++++++++++++++++++++++++++++++++++++++++++- 1 file changed, 175 insertions(+), 2 deletions(-) diff --git a/scheduling/RTLpathWFcheck.v b/scheduling/RTLpathWFcheck.v index eca5b24e..f5198e68 100644 --- a/scheduling/RTLpathWFcheck.v +++ b/scheduling/RTLpathWFcheck.v @@ -13,12 +13,185 @@ 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)) &&& true. (* TODO: &&& list_path_checker f pm (PTree.elements pm) *) + 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. -Admitted. +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)). -- cgit From 7d41f98bf46cb5ab9b286903859ba6bcf375bba8 Mon Sep 17 00:00:00 2001 From: Léo Gourdin Date: Mon, 8 Feb 2021 15:29:51 +0100 Subject: Checker for wellformed path --- scheduling/RTLpathWFcheck.v | 177 +++++++++++++++++++++++++++++++++++++++++++- 1 file changed, 175 insertions(+), 2 deletions(-) diff --git a/scheduling/RTLpathWFcheck.v b/scheduling/RTLpathWFcheck.v index eca5b24e..f5198e68 100644 --- a/scheduling/RTLpathWFcheck.v +++ b/scheduling/RTLpathWFcheck.v @@ -13,12 +13,185 @@ 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)) &&& true. (* TODO: &&& list_path_checker f pm (PTree.elements pm) *) + 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. -Admitted. +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)). -- cgit From 52faac3240cf454d68ed95fdd3985df88f9e6c80 Mon Sep 17 00:00:00 2001 From: Sylvain Boulmé Date: Wed, 10 Feb 2021 10:18:46 +0100 Subject: factorize lazy_and_Some_* lemmas --- scheduling/RTLpathWFcheck.v | 19 +++---------------- 1 file changed, 3 insertions(+), 16 deletions(-) diff --git a/scheduling/RTLpathWFcheck.v b/scheduling/RTLpathWFcheck.v index f5198e68..0ddc3142 100644 --- a/scheduling/RTLpathWFcheck.v +++ b/scheduling/RTLpathWFcheck.v @@ -88,24 +88,11 @@ Fixpoint exit_list_checker (pm: path_map) (l: list node): bool := | 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. + simpl in * |-. rewrite RTLpathLivegen.lazy_and_Some_tt_true in EXIT. firstorder (subst; eauto). Qed. @@ -167,7 +154,7 @@ 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). + 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 := @@ -178,7 +165,7 @@ Lemma function_checker_correct f pm pc path: pm!pc = Some path -> path_checker f pm pc path = Some tt. Proof. - unfold function_checker; rewrite lazy_and_Some_true. + unfold function_checker; rewrite RTLpathLivegen.lazy_and_Some_true. intros (ENTRY & PATH) PC. exploit list_path_checker_correct; eauto. - eapply PTree.elements_correct; eauto. -- cgit