Skip to content

Commit

Permalink
Compiles with 2 admits in SelectionproofC
Browse files Browse the repository at this point in the history
  • Loading branch information
@alxest
alxest committed Dec 23, 2019
1 parent c34dc79 commit 1f9cc54
Show file tree
Hide file tree
Showing 101 changed files with 953 additions and 952 deletions.
20 changes: 10 additions & 10 deletions backend/AllocproofC.v
View file
Original file line number Diff line number Diff line change
Expand Up @@ -22,7 +22,7 @@ Set Implicit Arguments.


Definition strong_wf_tgt (st_tgt0: LTL.state): Prop :=
exists sg_init ls_init, last_option st_tgt0.(LTLC.get_stack) = Some (LTL.dummy_stack sg_init ls_init).
exists sg_init ls_init, last_option (LTLC.get_stack st_tgt0) = Some (LTL.dummy_stack sg_init ls_init).

Lemma agree_callee_save_after
tstks ls sg tv
Expand All @@ -42,7 +42,7 @@ Qed.
Lemma match_stackframes_after
tse tge stks tstks sg
(STACKS: match_stackframes tse tge stks tstks sg):
<<STACKS: match_stackframes tse tge stks tstks.(stackframes_after_external) sg>>.
<<STACKS: match_stackframes tse tge stks (stackframes_after_external tstks) sg>>.
Proof.
inv STACKS; econs; et.
i. exploit STEPS; et. clear - H1.
Expand Down Expand Up @@ -70,25 +70,25 @@ Variable prog: RTL.program.
Variable tprog: LTL.program.
Let md_src: Mod.t := (RTLC.module2 prog).
Let md_tgt: Mod.t := (LTLC.module tprog).
Hypothesis (INCLSRC: SkEnv.includes skenv_link md_src.(Mod.sk)).
Hypothesis (INCLTGT: SkEnv.includes skenv_link md_tgt.(Mod.sk)).
Hypothesis (INCLSRC: SkEnv.includes skenv_link (Mod.sk md_src)).
Hypothesis (INCLTGT: SkEnv.includes skenv_link (Mod.sk md_tgt)).
Hypothesis (WF: SkEnv.wf skenv_link).
Hypothesis TRANSL: match_prog prog tprog.
Let ge := (SkEnv.revive (SkEnv.project skenv_link md_src.(Mod.sk)) prog).
Let tge := (SkEnv.revive (SkEnv.project skenv_link md_tgt.(Mod.sk)) tprog).
Let ge := (SkEnv.revive (SkEnv.project skenv_link (Mod.sk md_src)) prog).
Let tge := (SkEnv.revive (SkEnv.project skenv_link (Mod.sk md_tgt)) tprog).
Definition msp: ModSemPair.t := ModSemPair.mk (md_src skenv_link) (md_tgt skenv_link) (SimSymbId.mk md_src md_tgt) sm_link.

Inductive match_states
(idx: nat) (st_src0: RTL.state) (st_tgt0: LTL.state) (sm0: SimMem.t): Prop :=
| match_states_intro
(MATCHST: Allocproof.match_states skenv_link tge st_src0 st_tgt0)
(MCOMPATSRC: st_src0.(RTL.get_mem) = sm0.(SimMem.src))
(MCOMPATTGT: st_tgt0.(LTLC.get_mem) = sm0.(SimMem.tgt))
(MCOMPATSRC: (RTL.get_mem st_src0) = sm0.(SimMem.src))
(MCOMPATTGT: (LTLC.get_mem st_tgt0) = sm0.(SimMem.tgt))
(DUMMYTGT: strong_wf_tgt st_tgt0).

Theorem make_match_genvs :
SimSymbId.sim_skenv (SkEnv.project skenv_link md_src.(Mod.sk))
(SkEnv.project skenv_link md_tgt.(Mod.sk)) ->
SimSymbId.sim_skenv (SkEnv.project skenv_link (Mod.sk md_src))
(SkEnv.project skenv_link (Mod.sk md_tgt)) ->
Genv.match_genvs (match_globdef (fun _ f tf => transf_fundef f = OK tf) eq prog) ge tge.
Proof. subst_locals. eapply SimSymbId.sim_skenv_revive; eauto. Qed.

Expand Down
16 changes: 8 additions & 8 deletions backend/CSEproofC.v
View file
Original file line number Diff line number Diff line change
Expand Up @@ -22,25 +22,25 @@ Variable sm_link: SimMem.t.
Variables prog tprog: program.
Let md_src: Mod.t := (RTLC.module prog).
Let md_tgt: Mod.t := (RTLC.module tprog).
Hypothesis (INCLSRC: SkEnv.includes skenv_link md_src.(Mod.sk)).
Hypothesis (INCLTGT: SkEnv.includes skenv_link md_tgt.(Mod.sk)).
Hypothesis (INCLSRC: SkEnv.includes skenv_link (Mod.sk md_src)).
Hypothesis (INCLTGT: SkEnv.includes skenv_link (Mod.sk md_tgt)).
Hypothesis (WF: SkEnv.wf skenv_link).

Hypothesis TRANSL: match_prog prog tprog.
Let ge := (SkEnv.revive (SkEnv.project skenv_link md_src.(Mod.sk)) prog).
Let tge := (SkEnv.revive (SkEnv.project skenv_link md_tgt.(Mod.sk)) tprog).
Let ge := (SkEnv.revive (SkEnv.project skenv_link (Mod.sk md_src)) prog).
Let tge := (SkEnv.revive (SkEnv.project skenv_link (Mod.sk md_tgt)) tprog).
Definition msp: ModSemPair.t := ModSemPair.mk (md_src skenv_link) (md_tgt skenv_link) (SimSymbId.mk md_src md_tgt) sm_link.

Inductive match_states
(idx: unit) (st_src0: RTL.state) (st_tgt0: RTL.state) (sm0: SimMem.t): Prop :=
| match_states_intro
(MATCHST: CSEproof.match_states prog ge st_src0 st_tgt0)
(MCOMPATSRC: st_src0.(get_mem) = sm0.(SimMem.src))
(MCOMPATTGT: st_tgt0.(get_mem) = sm0.(SimMem.tgt)).
(MCOMPATSRC: (get_mem st_src0) = sm0.(SimMem.src))
(MCOMPATTGT: (get_mem st_tgt0) = sm0.(SimMem.tgt)).

Theorem make_match_genvs :
SimSymbId.sim_skenv (SkEnv.project skenv_link md_src.(Mod.sk))
(SkEnv.project skenv_link md_tgt.(Mod.sk)) ->
SimSymbId.sim_skenv (SkEnv.project skenv_link (Mod.sk md_src))
(SkEnv.project skenv_link (Mod.sk md_tgt)) ->
Genv.match_genvs (match_globdef (fun cu f tf => transf_fundef (romem_for cu) f = OK tf) eq prog) ge tge.
Proof. subst_locals. eapply SimSymbId.sim_skenv_revive; eauto. Qed.

Expand Down
18 changes: 9 additions & 9 deletions backend/CleanupLabelsproofC.v
View file
Original file line number Diff line number Diff line change
Expand Up @@ -19,7 +19,7 @@ Set Implicit Arguments.


Definition strong_wf_tgt (st_tgt0: Linear.state): Prop :=
exists sg_init ls_init, last_option st_tgt0.(LinearC.get_stack) = Some (Linear.dummy_stack sg_init ls_init).
exists sg_init ls_init, last_option (LinearC.get_stack st_tgt0) = Some (Linear.dummy_stack sg_init ls_init).

Section SIMMODSEM.

Expand All @@ -28,26 +28,26 @@ Variable sm_link: SimMem.t.
Variable prog tprog: Linear.program.
Let md_src: Mod.t := (LinearC.module prog).
Let md_tgt: Mod.t := (LinearC.module tprog).
Hypothesis (INCLSRC: SkEnv.includes skenv_link md_src.(Mod.sk)).
Hypothesis (INCLTGT: SkEnv.includes skenv_link md_tgt.(Mod.sk)).
Hypothesis (INCLSRC: SkEnv.includes skenv_link (Mod.sk md_src)).
Hypothesis (INCLTGT: SkEnv.includes skenv_link (Mod.sk md_tgt)).
Hypothesis (WF: SkEnv.wf skenv_link).
Hypothesis TRANSL: match_prog prog tprog.
Let ge := (SkEnv.revive (SkEnv.project skenv_link md_src.(Mod.sk)) prog).
Let tge := (SkEnv.revive (SkEnv.project skenv_link md_tgt.(Mod.sk)) tprog).
Let ge := (SkEnv.revive (SkEnv.project skenv_link (Mod.sk md_src)) prog).
Let tge := (SkEnv.revive (SkEnv.project skenv_link (Mod.sk md_tgt)) tprog).
Definition msp: ModSemPair.t := ModSemPair.mk (md_src skenv_link) (md_tgt skenv_link) (SimSymbId.mk md_src md_tgt) sm_link.

Inductive match_states
(idx: nat) (st_src0 st_tgt0: Linear.state) (sm0: SimMem.t): Prop :=
| match_states_intro
(MATCHST: CleanupLabelsproof.match_states st_src0 st_tgt0)
(MCOMPATSRC: st_src0.(LinearC.get_mem) = sm0.(SimMem.src))
(MCOMPATTGT: st_tgt0.(LinearC.get_mem) = sm0.(SimMem.tgt))
(MCOMPATSRC: (LinearC.get_mem st_src0) = sm0.(SimMem.src))
(MCOMPATTGT: (LinearC.get_mem st_tgt0) = sm0.(SimMem.tgt))
(DUMMYTGT: strong_wf_tgt st_tgt0)
(MEASURE: measure st_src0 = idx).

Theorem make_match_genvs :
SimSymbId.sim_skenv (SkEnv.project skenv_link md_src.(Mod.sk))
(SkEnv.project skenv_link md_tgt.(Mod.sk)) ->
SimSymbId.sim_skenv (SkEnv.project skenv_link (Mod.sk md_src))
(SkEnv.project skenv_link (Mod.sk md_tgt)) ->
Genv.match_genvs (match_globdef (fun ctx f tf => tf = transf_fundef f) eq prog) ge tge.
Proof. subst_locals. eapply SimSymbId.sim_skenv_revive; eauto. Qed.

Expand Down
22 changes: 11 additions & 11 deletions backend/CminorC.v
View file
Original file line number Diff line number Diff line change
Expand Up @@ -31,24 +31,24 @@ Section MODSEM.

Variable skenv_link: SkEnv.t.
Variable p: program.
Let skenv: SkEnv.t := skenv_link.(SkEnv.project) p.(Sk.of_program fn_sig).
Let ge: genv := skenv.(SkEnv.revive) p.
Let skenv: SkEnv.t := (SkEnv.project skenv_link) (Sk.of_program fn_sig p).
Let ge: genv := (SkEnv.revive skenv) p.

Inductive at_external: state -> Args.t -> Prop :=
| at_external_intro
fptr_arg sg_arg vs_arg k0 m0
(EXTERNAL: ge.(Genv.find_funct) fptr_arg = None)
(SIG: exists skd, skenv_link.(Genv.find_funct) fptr_arg = Some skd /\ Sk.get_csig skd = Some sg_arg):
(EXTERNAL: (Genv.find_funct ge) fptr_arg = None)
(SIG: exists skd, (Genv.find_funct skenv_link) fptr_arg = Some skd /\ Sk.get_csig skd = Some sg_arg):
at_external (Callstate fptr_arg sg_arg vs_arg k0 m0) (Args.mk fptr_arg vs_arg m0).

Inductive initial_frame (args: Args.t): state -> Prop :=
| initial_frame_intro
fd tvs
(CSTYLE: Args.is_cstyle args /\ fd.(fn_sig).(sig_cstyle) = true)
(FINDF: Genv.find_funct ge args.(Args.fptr) = Some (Internal fd))
(TYP: typecheck args.(Args.vs) fd.(fn_sig) tvs)
(LEN: args.(Args.vs).(length) = fd.(fn_sig).(sig_args).(length)):
initial_frame args (Callstate args.(Args.fptr) fd.(fn_sig) tvs Kstop args.(Args.m)).
(FINDF: Genv.find_funct ge (Args.fptr args) = Some (Internal fd))
(TYP: typecheck (Args.vs args) fd.(fn_sig) tvs)
(LEN: (Args.vs args).(length) = fd.(fn_sig).(sig_args).(length)):
initial_frame args (Callstate (Args.fptr args) fd.(fn_sig) tvs Kstop (Args.m args)).

Inductive final_frame: state -> Retv.t -> Prop :=
| final_frame_intro
Expand All @@ -60,10 +60,10 @@ Section MODSEM.
fptr_arg sg_arg vs_arg k m_arg
retv tv
(CSTYLE: Retv.is_cstyle retv)
(TYP: typify retv.(Retv.v) sg_arg.(proj_sig_res) = tv):
(TYP: typify (Retv.v retv) (proj_sig_res sg_arg) = tv):
after_external (Callstate fptr_arg sg_arg vs_arg k m_arg)
retv
(Returnstate tv k retv.(Retv.m)).
(Returnstate tv k (Retv.m retv)).

Program Definition modsem: ModSem.t :=
{| ModSem.step := step;
Expand Down Expand Up @@ -114,4 +114,4 @@ Section MODSEM.
End MODSEM.

Program Definition module (p: program): Mod.t :=
{| Mod.data := p; Mod.get_sk := Sk.of_program fn_sig; Mod.get_modsem := modsem; |}.
{| Mod.data := p; Mod.get_sk := Sk.of_program fn_sig; Mod.get_modsem := modsem; |}.
22 changes: 11 additions & 11 deletions backend/CminorSelC.v
View file
Original file line number Diff line number Diff line change
Expand Up @@ -31,24 +31,24 @@ Section MODSEM.

Variable skenv_link: SkEnv.t.
Variable p: program.
Let skenv: SkEnv.t := skenv_link.(SkEnv.project) p.(Sk.of_program fn_sig).
Let ge: genv := skenv.(SkEnv.revive) p.
Let skenv: SkEnv.t := (SkEnv.project skenv_link) (Sk.of_program fn_sig p).
Let ge: genv := (SkEnv.revive skenv) p.

Inductive at_external: state -> Args.t -> Prop :=
| at_external_intro
fptr_arg sg_arg vs_arg k0 m0
(EXTERNAL: ge.(Genv.find_funct) fptr_arg = None)
(SIG: exists skd, skenv_link.(Genv.find_funct) fptr_arg = Some skd /\ Sk.get_csig skd = Some sg_arg):
(EXTERNAL: (Genv.find_funct ge) fptr_arg = None)
(SIG: exists skd, (Genv.find_funct skenv_link) fptr_arg = Some skd /\ Sk.get_csig skd = Some sg_arg):
at_external (Callstate fptr_arg sg_arg vs_arg k0 m0) (Args.mk fptr_arg vs_arg m0).

Inductive initial_frame (args: Args.t): state -> Prop :=
| initial_frame_intro
fd tvs
(CSTYLE: Args.is_cstyle args /\ fd.(fn_sig).(sig_cstyle) = true)
(FINDF: Genv.find_funct ge args.(Args.fptr) = Some (Internal fd))
(TYP: typecheck args.(Args.vs) fd.(fn_sig) tvs)
(LEN: args.(Args.vs).(length) = fd.(fn_sig).(sig_args).(length)):
initial_frame args (Callstate args.(Args.fptr) fd.(fn_sig) tvs Kstop args.(Args.m)).
(FINDF: Genv.find_funct ge (Args.fptr args) = Some (Internal fd))
(TYP: typecheck (Args.vs args) fd.(fn_sig) tvs)
(LEN: (Args.vs args).(length) = fd.(fn_sig).(sig_args).(length)):
initial_frame args (Callstate (Args.fptr args) fd.(fn_sig) tvs Kstop (Args.m args)).

Inductive final_frame: state -> Retv.t -> Prop :=
| final_frame_intro
Expand All @@ -59,10 +59,10 @@ Section MODSEM.
| after_external_intro
fptr_arg sg_arg vs_arg k m_arg retv tv
(CSTYLE: Retv.is_cstyle retv)
(TYP: typify retv.(Retv.v) sg_arg.(proj_sig_res) = tv):
(TYP: typify (Retv.v retv) (proj_sig_res sg_arg) = tv):
after_external (Callstate fptr_arg sg_arg vs_arg k m_arg)
retv
(Returnstate tv k retv.(Retv.m)).
(Returnstate tv k (Retv.m retv)).

Program Definition modsem: ModSem.t :=
{| ModSem.step := step;
Expand Down Expand Up @@ -146,4 +146,4 @@ Section MODSEM.
End MODSEM.

Program Definition module (p: program): Mod.t :=
{| Mod.data := p; Mod.get_sk := Sk.of_program fn_sig; Mod.get_modsem := modsem; |}.
{| Mod.data := p; Mod.get_sk := Sk.of_program fn_sig; Mod.get_modsem := modsem; |}.
16 changes: 8 additions & 8 deletions backend/ConstpropproofC.v
View file
Original file line number Diff line number Diff line change
Expand Up @@ -21,24 +21,24 @@ Variable sm_link: SimMem.t.
Variables prog tprog: program.
Let md_src: Mod.t := (RTLC.module prog).
Let md_tgt: Mod.t := (RTLC.module tprog).
Hypothesis (INCLSRC: SkEnv.includes skenv_link md_src.(Mod.sk)).
Hypothesis (INCLTGT: SkEnv.includes skenv_link md_tgt.(Mod.sk)).
Hypothesis (INCLSRC: SkEnv.includes skenv_link (Mod.sk md_src)).
Hypothesis (INCLTGT: SkEnv.includes skenv_link (Mod.sk md_tgt)).
Hypothesis (WF: SkEnv.wf skenv_link).
Hypothesis TRANSL: match_prog prog tprog.
Let ge := (SkEnv.revive (SkEnv.project skenv_link md_src.(Mod.sk)) prog).
Let tge := (SkEnv.revive (SkEnv.project skenv_link md_tgt.(Mod.sk)) tprog).
Let ge := (SkEnv.revive (SkEnv.project skenv_link (Mod.sk md_src)) prog).
Let tge := (SkEnv.revive (SkEnv.project skenv_link (Mod.sk md_tgt)) tprog).
Definition msp: ModSemPair.t := ModSemPair.mk (md_src skenv_link) (md_tgt skenv_link) (SimSymbId.mk md_src md_tgt) sm_link.

Inductive match_states
(idx: nat) (st_src0: RTL.state) (st_tgt0: RTL.state) (sm0: SimMem.t): Prop :=
| match_states_intro
(MATCHST: Constpropproof.match_states prog idx st_src0 st_tgt0)
(MCOMPATSRC: st_src0.(get_mem) = sm0.(SimMem.src))
(MCOMPATTGT: st_tgt0.(get_mem) = sm0.(SimMem.tgt)).
(MCOMPATSRC: (get_mem st_src0) = sm0.(SimMem.src))
(MCOMPATTGT: (get_mem st_tgt0) = sm0.(SimMem.tgt)).

Theorem make_match_genvs :
SimSymbId.sim_skenv (SkEnv.project skenv_link md_src.(Mod.sk))
(SkEnv.project skenv_link md_tgt.(Mod.sk)) ->
SimSymbId.sim_skenv (SkEnv.project skenv_link (Mod.sk md_src))
(SkEnv.project skenv_link (Mod.sk md_tgt)) ->
Genv.match_genvs (match_globdef (fun cu f tf => tf = transf_fundef (romem_for cu) f) eq prog) ge tge.
Proof. subst_locals. eapply SimSymbId.sim_skenv_revive; eauto. Qed.

Expand Down
16 changes: 8 additions & 8 deletions backend/DeadcodeproofC.v
View file
Original file line number Diff line number Diff line change
Expand Up @@ -22,25 +22,25 @@ Variable sm_link: SimMem.t.
Variables prog tprog: program.
Let md_src: Mod.t := (RTLC.module prog).
Let md_tgt: Mod.t := (RTLC.module tprog).
Hypothesis (INCLSRC: SkEnv.includes skenv_link md_src.(Mod.sk)).
Hypothesis (INCLTGT: SkEnv.includes skenv_link md_tgt.(Mod.sk)).
Hypothesis (INCLSRC: SkEnv.includes skenv_link (Mod.sk md_src)).
Hypothesis (INCLTGT: SkEnv.includes skenv_link (Mod.sk md_tgt)).
Hypothesis (WF: SkEnv.wf skenv_link).

Hypothesis TRANSL: match_prog prog tprog.
Let ge := (SkEnv.revive (SkEnv.project skenv_link md_src.(Mod.sk)) prog).
Let tge := (SkEnv.revive (SkEnv.project skenv_link md_tgt.(Mod.sk)) tprog).
Let ge := (SkEnv.revive (SkEnv.project skenv_link (Mod.sk md_src)) prog).
Let tge := (SkEnv.revive (SkEnv.project skenv_link (Mod.sk md_tgt)) tprog).
Definition msp: ModSemPair.t := ModSemPair.mk (md_src skenv_link) (md_tgt skenv_link) (SimSymbId.mk md_src md_tgt) sm_link.

Inductive match_states
(idx: unit) (st_src0: RTL.state) (st_tgt0: RTL.state) (sm0: SimMem.t): Prop :=
| match_states_intro
(MATCHST: Deadcodeproof.match_states prog ge st_src0 st_tgt0)
(MCOMPATSRC: st_src0.(get_mem) = sm0.(SimMem.src))
(MCOMPATTGT: st_tgt0.(get_mem) = sm0.(SimMem.tgt)).
(MCOMPATSRC: (get_mem st_src0) = sm0.(SimMem.src))
(MCOMPATTGT: (get_mem st_tgt0) = sm0.(SimMem.tgt)).

Theorem make_match_genvs :
SimSymbId.sim_skenv (SkEnv.project skenv_link md_src.(Mod.sk))
(SkEnv.project skenv_link md_tgt.(Mod.sk)) ->
SimSymbId.sim_skenv (SkEnv.project skenv_link (Mod.sk md_src))
(SkEnv.project skenv_link (Mod.sk md_tgt)) ->
Genv.match_genvs (match_globdef (fun cu f tf => transf_fundef (romem_for cu) f = OK tf) eq prog) ge tge.
Proof. subst_locals. eapply SimSymbId.sim_skenv_revive; eauto. Qed.

Expand Down
18 changes: 9 additions & 9 deletions backend/DebugvarproofC.v
View file
Original file line number Diff line number Diff line change
Expand Up @@ -16,7 +16,7 @@ Set Implicit Arguments.


Definition strong_wf_tgt (st_tgt0: Linear.state): Prop :=
exists sg_init ls_init, last_option st_tgt0.(LinearC.get_stack) = Some (Linear.dummy_stack sg_init ls_init).
exists sg_init ls_init, last_option (LinearC.get_stack st_tgt0) = Some (Linear.dummy_stack sg_init ls_init).

Section SIMMODSEM.

Expand All @@ -25,25 +25,25 @@ Variable sm_link: SimMem.t.
Variables prog tprog: program.
Let md_src: Mod.t := (LinearC.module prog).
Let md_tgt: Mod.t := (LinearC.module tprog).
Hypothesis (INCLSRC: SkEnv.includes skenv_link md_src.(Mod.sk)).
Hypothesis (INCLTGT: SkEnv.includes skenv_link md_tgt.(Mod.sk)).
Hypothesis (INCLSRC: SkEnv.includes skenv_link (Mod.sk md_src)).
Hypothesis (INCLTGT: SkEnv.includes skenv_link (Mod.sk md_tgt)).
Hypothesis (WF: SkEnv.wf skenv_link).
Hypothesis TRANSL: match_prog prog tprog.
Let ge := (SkEnv.revive (SkEnv.project skenv_link md_src.(Mod.sk)) prog).
Let tge := (SkEnv.revive (SkEnv.project skenv_link md_tgt.(Mod.sk)) tprog).
Let ge := (SkEnv.revive (SkEnv.project skenv_link (Mod.sk md_src)) prog).
Let tge := (SkEnv.revive (SkEnv.project skenv_link (Mod.sk md_tgt)) tprog).
Definition msp: ModSemPair.t := ModSemPair.mk (md_src skenv_link) (md_tgt skenv_link) (SimSymbId.mk md_src md_tgt) sm_link.

Inductive match_states
(idx: nat) (st_src0: Linear.state) (st_tgt0: Linear.state) (sm0: SimMem.t): Prop :=
| match_states_intro
(MATCHST: Debugvarproof.match_states st_src0 st_tgt0)
(MCOMPATSRC: st_src0.(get_mem) = sm0.(SimMem.src))
(MCOMPATTGT: st_tgt0.(get_mem) = sm0.(SimMem.tgt))
(MCOMPATSRC: (get_mem st_src0) = sm0.(SimMem.src))
(MCOMPATTGT: (get_mem st_tgt0) = sm0.(SimMem.tgt))
(DUMMYTGT: strong_wf_tgt st_tgt0).

Theorem make_match_genvs :
SimSymbId.sim_skenv (SkEnv.project skenv_link md_src.(Mod.sk))
(SkEnv.project skenv_link md_tgt.(Mod.sk)) ->
SimSymbId.sim_skenv (SkEnv.project skenv_link (Mod.sk md_src))
(SkEnv.project skenv_link (Mod.sk md_tgt)) ->
Genv.match_genvs (match_globdef (fun _ f tf => transf_fundef f = Errors.OK tf) eq prog) ge tge.
Proof. subst_locals. eapply SimSymbId.sim_skenv_revive; eauto. Qed.

Expand Down
10 changes: 5 additions & 5 deletions backend/InliningproofC.v
View file
Original file line number Diff line number Diff line change
Expand Up @@ -25,12 +25,12 @@ Variable sm_link: SimMem.t.
Variables prog tprog: program.
Let md_src: Mod.t := (RTLC.module prog).
Let md_tgt: Mod.t := (RTLC.module tprog).
Hypothesis (INCLSRC: SkEnv.includes skenv_link md_src.(Mod.sk)).
Hypothesis (INCLTGT: SkEnv.includes skenv_link md_tgt.(Mod.sk)).
Hypothesis (INCLSRC: SkEnv.includes skenv_link (Mod.sk md_src)).
Hypothesis (INCLTGT: SkEnv.includes skenv_link (Mod.sk md_tgt)).
Hypothesis (WF: SkEnv.wf skenv_link).
Hypothesis TRANSL: match_prog prog tprog.
Let ge := (SkEnv.revive (SkEnv.project skenv_link md_src.(Mod.sk)) prog).
Let tge := (SkEnv.revive (SkEnv.project skenv_link md_tgt.(Mod.sk)) tprog).
Let ge := (SkEnv.revive (SkEnv.project skenv_link (Mod.sk md_src)) prog).
Let tge := (SkEnv.revive (SkEnv.project skenv_link (Mod.sk md_tgt)) tprog).
Definition msp: ModSemPair.t := ModSemPair.mk (md_src skenv_link) (md_tgt skenv_link) (SimSymbId.mk md_src md_tgt) sm_link.

Inductive match_states
Expand All @@ -40,7 +40,7 @@ Inductive match_states
(MCOMPATIDX: idx = Inliningproof.measure st_src0).

Theorem make_match_genvs :
SimSymbId.sim_skenv (SkEnv.project skenv_link md_src.(Mod.sk)) (SkEnv.project skenv_link md_tgt.(Mod.sk)) ->
SimSymbId.sim_skenv (SkEnv.project skenv_link (Mod.sk md_src)) (SkEnv.project skenv_link (Mod.sk md_tgt)) ->
Genv.match_genvs (match_globdef (fun cunit f tf => transf_fundef (funenv_program cunit) f = OK tf) eq prog) ge tge.
Proof. subst_locals. eapply SimSymbId.sim_skenv_revive; eauto. Qed.

Expand Down
Loading

0 comments on commit 1f9cc54

Please sign in to comment.