From 10f3467291b5a1e7ed195906eb23ef1ac57a0bd7 Mon Sep 17 00:00:00 2001 From: David Monniaux Date: Fri, 16 Jul 2021 21:19:32 +0200 Subject: rename parameterized versions --- backend/CSE3.v | 14 ++++++------ backend/CSE3proof.v | 62 ++++++++++++++++++++++++++--------------------------- 2 files changed, 38 insertions(+), 38 deletions(-) (limited to 'backend') diff --git a/backend/CSE3.v b/backend/CSE3.v index 5d05821a..f3a0af24 100644 --- a/backend/CSE3.v +++ b/backend/CSE3.v @@ -82,7 +82,7 @@ Definition find_cond_in_fmap fmap pc cond args := end else None. -Definition transf_instr (fmap : PMap.t RB.t) +Definition param_transf_instr (fmap : PMap.t RB.t) (pc: node) (instr: instruction) := match instr with | Iop op args dst s => @@ -118,7 +118,7 @@ Definition transf_instr (fmap : PMap.t RB.t) end. End REWRITE. -Definition transf_function (f: function) : res function := +Definition param_transf_function (f: function) : res function := do tenv <- type_function f; let (invariants, hints) := preanalysis tenv f in let ctx := context_from_hints hints in @@ -127,15 +127,15 @@ Definition transf_function (f: function) : res function := OK {| fn_sig := f.(fn_sig); fn_params := f.(fn_params); fn_stacksize := f.(fn_stacksize); - fn_code := PTree.map (transf_instr (ctx := ctx) invariants) + fn_code := PTree.map (param_transf_instr (ctx := ctx) invariants) f.(fn_code); fn_entrypoint := f.(fn_entrypoint) |} else Error (msg "cse3: not inductive"). -Definition transf_fundef (fd: fundef) : res fundef := - AST.transf_partial_fundef transf_function fd. +Definition param_transf_fundef (fd: fundef) : res fundef := + AST.transf_partial_fundef param_transf_function fd. -Definition transf_program (p: program) : res program := - transform_partial_program transf_fundef p. +Definition param_transf_program (p: program) : res program := + transform_partial_program param_transf_fundef p. End PARAMS. diff --git a/backend/CSE3proof.v b/backend/CSE3proof.v index 2d9992c6..2e9f99c5 100644 --- a/backend/CSE3proof.v +++ b/backend/CSE3proof.v @@ -32,10 +32,10 @@ Section PARAMS. Variable params : cse3params. Definition match_prog (p tp: RTL.program) := - match_program (fun ctx f tf => transf_fundef params f = OK tf) eq p tp. + match_program (fun ctx f tf => param_transf_fundef params f = OK tf) eq p tp. Lemma transf_program_match: - forall p tp, transf_program params p = OK tp -> match_prog p tp. + forall p tp, param_transf_program params p = OK tp -> match_prog p tp. Proof. intros. eapply match_transform_partial_program; eauto. Qed. @@ -113,7 +113,7 @@ Lemma functions_translated: forall (v: val) (f: RTL.fundef), Genv.find_funct ge v = Some f -> exists tf, - Genv.find_funct tge v = Some tf /\ transf_fundef params f = OK tf. + Genv.find_funct tge v = Some tf /\ param_transf_fundef params f = OK tf. Proof. apply (Genv.find_funct_transf_partial TRANSF). Qed. @@ -122,7 +122,7 @@ Lemma function_ptr_translated: forall (b: block) (f: RTL.fundef), Genv.find_funct_ptr ge b = Some f -> exists tf, - Genv.find_funct_ptr tge b = Some tf /\ transf_fundef params f = OK tf. + Genv.find_funct_ptr tge b = Some tf /\ param_transf_fundef params f = OK tf. Proof. apply (Genv.find_funct_ptr_transf_partial TRANSF). Qed. @@ -141,7 +141,7 @@ Proof. Qed. Lemma sig_preserved: - forall f tf, transf_fundef params f = OK tf -> funsig tf = funsig f. + forall f tf, param_transf_fundef params f = OK tf -> funsig tf = funsig f. Proof. destruct f; simpl; intros. - monadInv H. @@ -156,7 +156,7 @@ Proof. Qed. Lemma stacksize_preserved: - forall f tf, transf_function params f = OK tf -> fn_stacksize tf = fn_stacksize f. + forall f tf, param_transf_function params f = OK tf -> fn_stacksize tf = fn_stacksize f. Proof. unfold transf_function; destruct f; simpl; intros. monadInv H. @@ -168,7 +168,7 @@ Proof. Qed. Lemma params_preserved: - forall f tf, transf_function params f = OK tf -> fn_params tf = fn_params f. + forall f tf, param_transf_function params f = OK tf -> fn_params tf = fn_params f. Proof. unfold transf_function; destruct f; simpl; intros. monadInv H. @@ -180,7 +180,7 @@ Proof. Qed. Lemma entrypoint_preserved: - forall f tf, transf_function params f = OK tf -> fn_entrypoint tf = fn_entrypoint f. + forall f tf, param_transf_function params f = OK tf -> fn_entrypoint tf = fn_entrypoint f. Proof. unfold transf_function; destruct f; simpl; intros. monadInv H. @@ -192,7 +192,7 @@ Proof. Qed. Lemma sig_preserved2: - forall f tf, transf_function params f = OK tf -> fn_sig tf = fn_sig f. + forall f tf, param_transf_function params f = OK tf -> fn_sig tf = fn_sig f. Proof. unfold transf_function; destruct f; simpl; intros. monadInv H. @@ -204,7 +204,7 @@ Proof. Qed. Lemma transf_function_is_typable: - forall f tf, transf_function params f = OK tf -> + forall f tf, param_transf_function params f = OK tf -> exists tenv, type_function f = OK tenv. Proof. unfold transf_function; destruct f; simpl; intros. @@ -213,7 +213,7 @@ Proof. assumption. Qed. Lemma transf_function_invariants_inductive: - forall f tf tenv, transf_function params f = OK tf -> + forall f tf tenv, param_transf_function params f = OK tf -> type_function f = OK tenv -> check_inductiveness (ctx:=(context_from_hints (snd (preanalysis tenv f)))) f tenv (fst (preanalysis tenv f)) = true. @@ -230,7 +230,7 @@ Lemma find_function_translated: forall ros rs fd, find_function ge ros rs = Some fd -> exists tfd, - find_function tge ros rs = Some tfd /\ transf_fundef params fd = OK tfd. + find_function tge ros rs = Some tfd /\ param_transf_fundef params fd = OK tfd. Proof. unfold find_function; intros. destruct ros as [r|id]. eapply functions_translated; eauto. @@ -245,7 +245,7 @@ Inductive match_stackframes: list stackframe -> list stackframe -> signature -> | match_stackframes_cons: forall res f sp pc rs s tf ts sg tenv (STACKS: match_stackframes s ts (fn_sig tf)) - (FUN: transf_function params f = OK tf) + (FUN: param_transf_function params f = OK tf) (WTF: type_function f = OK tenv) (WTRS: wt_regset tenv rs) (WTRES: tenv res = proj_sig_res sg) @@ -262,7 +262,7 @@ Inductive match_states: state -> state -> Prop := | match_states_intro: forall s f sp pc rs m ts tf tenv (STACKS: match_stackframes s ts (fn_sig tf)) - (FUN: transf_function params f = OK tf) + (FUN: param_transf_function params f = OK tf) (WTF: type_function f = OK tenv) (WTRS: wt_regset tenv rs) (REL: sem_rel_b sp (context_from_hints (snd (preanalysis tenv f))) ((fst (preanalysis tenv f))#pc) rs m), @@ -271,7 +271,7 @@ Inductive match_states: state -> state -> Prop := | match_states_call: forall s f args m ts tf (STACKS: match_stackframes s ts (funsig tf)) - (FUN: transf_fundef params f = OK tf) + (FUN: param_transf_fundef params f = OK tf) (WTARGS: Val.has_type_list args (sig_args (funsig tf))), match_states (Callstate s f args m) (Callstate ts tf args m) @@ -296,10 +296,10 @@ Qed. Lemma transf_function_at: forall f tf pc tenv instr - (TF : transf_function params f = OK tf) + (TF : param_transf_function params f = OK tf) (TYPE : type_function f = OK tenv) (PC : (fn_code f) ! pc = Some instr), - (fn_code tf) ! pc = Some (transf_instr + (fn_code tf) ! pc = Some (param_transf_instr (ctx := (context_from_hints (snd (preanalysis tenv f)))) params (fst (preanalysis tenv f)) pc instr). @@ -500,9 +500,9 @@ Proof. - (* Iop *) exists (State ts tf sp pc' (rs # res <- v) m). split. - + pose (transf_instr (ctx:=(context_from_hints (snd (preanalysis tenv f)))) params (fst (preanalysis tenv f)) pc (Iop op args res pc')) as instr'. - assert (instr' = (transf_instr (ctx:=(context_from_hints (snd (preanalysis tenv f)))) params (fst (preanalysis tenv f)) pc (Iop op args res pc'))) by reflexivity. - unfold transf_instr, find_op_in_fmap in instr'. + + pose (param_transf_instr (ctx:=(context_from_hints (snd (preanalysis tenv f)))) params (fst (preanalysis tenv f)) pc (Iop op args res pc')) as instr'. + assert (instr' = (param_transf_instr (ctx:=(context_from_hints (snd (preanalysis tenv f)))) params (fst (preanalysis tenv f)) pc (Iop op args res pc'))) by reflexivity. + unfold param_transf_instr, find_op_in_fmap in instr'. destruct (@PMap.get (option RELATION.t) pc) eqn:INV_PC. pose proof (rhs_find_sound (sp:=sp) (genv:=ge) (ctx:=(context_from_hints (snd (preanalysis tenv f)))) pc (SOp op) (subst_args (ctx:=(context_from_hints (snd (preanalysis tenv f)))) (fst (preanalysis tenv f)) pc args) t) as FIND_SOUND. @@ -583,9 +583,9 @@ Proof. (* END INVARIANT *) - (* Iload *) exists (State ts tf sp pc' (rs # dst <- v) m). split. - + pose (transf_instr (ctx:=(context_from_hints (snd (preanalysis tenv f)))) params (fst (preanalysis tenv f)) pc (Iload trap chunk addr args dst pc')) as instr'. - assert (instr' = (transf_instr (ctx:=(context_from_hints (snd (preanalysis tenv f)))) params (fst (preanalysis tenv f)) pc (Iload trap chunk addr args dst pc'))) by reflexivity. - unfold transf_instr, find_load_in_fmap in instr'. + + pose (param_transf_instr (ctx:=(context_from_hints (snd (preanalysis tenv f)))) params (fst (preanalysis tenv f)) pc (Iload trap chunk addr args dst pc')) as instr'. + assert (instr' = (param_transf_instr (ctx:=(context_from_hints (snd (preanalysis tenv f)))) params (fst (preanalysis tenv f)) pc (Iload trap chunk addr args dst pc'))) by reflexivity. + unfold param_transf_instr, find_load_in_fmap in instr'. destruct (@PMap.get (option RELATION.t) pc) eqn:INV_PC. pose proof (rhs_find_sound (sp:=sp) (genv:=ge) (ctx:=(context_from_hints (snd (preanalysis tenv f)))) pc (SLoad chunk addr) (subst_args (ctx:=(context_from_hints (snd (preanalysis tenv f)))) (fst (preanalysis tenv f)) pc args) t) as FIND_SOUND. @@ -661,9 +661,9 @@ Proof. - (* Iload notrap1 *) exists (State ts tf sp pc' (rs # dst <- Vundef) m). split. - + pose (transf_instr (ctx:=(context_from_hints (snd (preanalysis tenv f)))) params (fst (preanalysis tenv f)) pc (Iload NOTRAP chunk addr args dst pc')) as instr'. - assert (instr' = (transf_instr (ctx:=(context_from_hints (snd (preanalysis tenv f)))) params (fst (preanalysis tenv f)) pc (Iload NOTRAP chunk addr args dst pc'))) by reflexivity. - unfold transf_instr, find_load_in_fmap in instr'. + + pose (param_transf_instr (ctx:=(context_from_hints (snd (preanalysis tenv f)))) params (fst (preanalysis tenv f)) pc (Iload NOTRAP chunk addr args dst pc')) as instr'. + assert (instr' = (param_transf_instr (ctx:=(context_from_hints (snd (preanalysis tenv f)))) params (fst (preanalysis tenv f)) pc (Iload NOTRAP chunk addr args dst pc'))) by reflexivity. + unfold param_transf_instr, find_load_in_fmap in instr'. destruct (@PMap.get (option RELATION.t) pc) eqn:INV_PC. pose proof (rhs_find_sound (sp:=sp) (genv:=ge) (ctx:=(context_from_hints (snd (preanalysis tenv f)))) pc (SLoad chunk addr) (subst_args (ctx:=(context_from_hints (snd (preanalysis tenv f)))) (fst (preanalysis tenv f)) pc args) t) as FIND_SOUND. @@ -737,9 +737,9 @@ Proof. - (* Iload notrap2 *) exists (State ts tf sp pc' (rs # dst <- Vundef) m). split. - + pose (transf_instr (ctx:=(context_from_hints (snd (preanalysis tenv f)))) params (fst (preanalysis tenv f)) pc (Iload NOTRAP chunk addr args dst pc')) as instr'. - assert (instr' = (transf_instr (ctx:=(context_from_hints (snd (preanalysis tenv f)))) params (fst (preanalysis tenv f)) pc (Iload NOTRAP chunk addr args dst pc'))) by reflexivity. - unfold transf_instr, find_load_in_fmap in instr'. + + pose (param_transf_instr (ctx:=(context_from_hints (snd (preanalysis tenv f)))) params (fst (preanalysis tenv f)) pc (Iload NOTRAP chunk addr args dst pc')) as instr'. + assert (instr' = (param_transf_instr (ctx:=(context_from_hints (snd (preanalysis tenv f)))) params (fst (preanalysis tenv f)) pc (Iload NOTRAP chunk addr args dst pc'))) by reflexivity. + unfold param_transf_instr, find_load_in_fmap in instr'. destruct (@PMap.get (option RELATION.t) pc) eqn:INV_PC. pose proof (rhs_find_sound (sp:=sp) (genv:=ge) (ctx:=(context_from_hints (snd (preanalysis tenv f)))) pc (SLoad chunk addr) (subst_args (ctx:=(context_from_hints (snd (preanalysis tenv f)))) (fst (preanalysis tenv f)) pc args) t) as FIND_SOUND. @@ -946,7 +946,7 @@ Proof. destruct (find_cond_in_fmap (ctx := ctx) params invs pc cond args) as [bfound | ] eqn:FIND_COND. + econstructor; split. * eapply exec_Inop; try eassumption. - TR_AT. unfold transf_instr. fold invs. fold ctx. rewrite FIND_COND. reflexivity. + TR_AT. unfold param_transf_instr. fold invs. fold ctx. rewrite FIND_COND. reflexivity. * replace bfound with b. { econstructor; eauto. (* BEGIN INVARIANT *) @@ -1037,7 +1037,7 @@ Proof. discriminate. + econstructor; split. * eapply exec_Icond with (args := (subst_args (ctx:=(context_from_hints (snd (preanalysis tenv f)))) (fst (preanalysis tenv f)) pc args)); try eassumption. - ** TR_AT. unfold transf_instr. fold invs. fold ctx. + ** TR_AT. unfold param_transf_instr. fold invs. fold ctx. rewrite FIND_COND. reflexivity. ** rewrite subst_args_ok with (sp:=sp) (m:=m) by trivial. -- cgit