Skip to content

[DO NOT MERGE] v3.11 #25

New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Open
kim-yoonseung wants to merge 2 commits into
base: v3.9
Choose a base branch
from
Open

[DO NOT MERGE] v3.11 #25

Show file tree
Hide file tree
Changes from all commits
Commits
Show all changes
2 commits
Select commit Hold shift + click to select a range
ef05597
Bump CompCert version to 3.11
kim-yoonseung Feb 19, 2023
3a3d98a
Minor fix
kim-yoonseung Feb 25, 2023
File filter

Filter by extension

Filter by extension
Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
17 changes: 15 additions & 2 deletions Makefile
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -34,6 +34,19 @@ Makefile.coq: Makefile $(COQTHEORIES)
echo "-R proof $(COQMODULE)"; \
echo "-R demo $(COQMODULE)"; \
echo "-R selfsim $(COQMODULE)"; \
\
echo "-R ../lib compcertr.lib"; \
echo "-R ../common compcertr.common"; \
echo "-R ../x86 compcertr.x86"; \
echo "-R ../x86_64 compcertr.x86_64"; \
echo "-R ../backend compcertr.backend"; \
echo "-R ../cfrontend compcertr.cfrontend"; \
echo "-R ../driver compcertr.driver"; \
echo "-R ../export compcertr.export"; \
echo "-R ../cparser compcertr.cparser"; \
echo "-R ../demo compcertr.demo"; \
echo "-R ../flocq Flocq"; \
\
echo $(COQTHEORIES)) > _CoqProject
coq_makefile -f _CoqProject -o Makefile.coq

Expand Down Expand Up @@ -63,8 +76,8 @@ Makefile.coq: Makefile $(COQTHEORIES)
# echo "-R ../../backend compcert.backend"; \
# echo "-R ../../cfrontend compcert.cfrontend"; \
# echo "-R ../../driver compcert.driver"; \
# echo "-R ../../flocq compcert.flocq"; \
# echo "-R ../../exportclight compcert.exportclight"; \
# echo "-R ../../flocq Flocq"; \
# echo "-R ../../export compcert.export"; \
# echo "-R ../../cparser compcert.cparser"; \
# echo $(COQTHEORIES)) > _CoqProject
# coq_makefile -f _CoqProject -o Makefile.coq-rsync
Expand Down
4 changes: 2 additions & 2 deletions backend/AllocproofC.v
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -86,8 +86,8 @@ 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: (RTL.get_mem st_src0) = sm0.(SimMem.src))
(MCOMPATTGT: (LTLC.get_mem st_tgt0) = sm0.(SimMem.tgt))
(MCOMPATSRC: (RTL.get_mem st_src0) = (SimMem.src sm0))
(MCOMPATTGT: (LTLC.get_mem st_tgt0) = (SimMem.tgt sm0))
(DUMMYTGT: strong_wf_tgt st_tgt0).

Theorem make_match_genvs :
Expand Down
4 changes: 2 additions & 2 deletions backend/CSEproofC.v
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -40,8 +40,8 @@ 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: (get_mem st_src0) = sm0.(SimMem.src))
(MCOMPATTGT: (get_mem st_tgt0) = sm0.(SimMem.tgt)).
(MCOMPATSRC: (get_mem st_src0) = (SimMem.src sm0))
(MCOMPATTGT: (get_mem st_tgt0) = (SimMem.tgt sm0)).

Theorem make_match_genvs :
SimSymbId.sim_skenv (SkEnv.project skenv_link (Mod.sk md_src))
Expand Down
4 changes: 2 additions & 2 deletions backend/CleanupLabelsproofC.v
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -42,8 +42,8 @@ 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: (LinearC.get_mem st_src0) = sm0.(SimMem.src))
(MCOMPATTGT: (LinearC.get_mem st_tgt0) = sm0.(SimMem.tgt))
(MCOMPATSRC: (LinearC.get_mem st_src0) = (SimMem.src sm0))
(MCOMPATTGT: (LinearC.get_mem st_tgt0) = (SimMem.tgt sm0))
(DUMMYTGT: strong_wf_tgt st_tgt0)
(MEASURE: measure st_src0 = idx).

Expand Down
2 changes: 1 addition & 1 deletion backend/CminorC.v
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -48,7 +48,7 @@ Section MODSEM.
(CSTYLE: Args.is_cstyle args /\ fd.(fn_sig).(sig_cstyle) = true)
(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)):
(LEN: (length (Args.vs args)) = (length fd.(fn_sig).(sig_args))):
initial_frame args (Callstate (Args.fptr args) fd.(fn_sig) tvs Kstop (Args.m args)).

Inductive final_frame: state -> Retv.t -> Prop :=
Expand Down
2 changes: 1 addition & 1 deletion backend/CminorSelC.v
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -48,7 +48,7 @@ Section MODSEM.
(CSTYLE: Args.is_cstyle args /\ fd.(fn_sig).(sig_cstyle) = true)
(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)):
(LEN: (length (Args.vs args)) = (length fd.(fn_sig).(sig_args))):
initial_frame args (Callstate (Args.fptr args) fd.(fn_sig) tvs Kstop (Args.m args)).

Inductive final_frame: state -> Retv.t -> Prop :=
Expand Down
4 changes: 2 additions & 2 deletions backend/ConstpropproofC.v
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -38,8 +38,8 @@ 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: (get_mem st_src0) = sm0.(SimMem.src))
(MCOMPATTGT: (get_mem st_tgt0) = sm0.(SimMem.tgt)).
(MCOMPATSRC: (get_mem st_src0) = (SimMem.src sm0))
(MCOMPATTGT: (get_mem st_tgt0) = (SimMem.tgt sm0)).

Theorem make_match_genvs :
SimSymbId.sim_skenv (SkEnv.project skenv_link (Mod.sk md_src))
Expand Down
4 changes: 2 additions & 2 deletions backend/DeadcodeproofC.v
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -40,8 +40,8 @@ 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: (get_mem st_src0) = sm0.(SimMem.src))
(MCOMPATTGT: (get_mem st_tgt0) = sm0.(SimMem.tgt)).
(MCOMPATSRC: (get_mem st_src0) = (SimMem.src sm0))
(MCOMPATTGT: (get_mem st_tgt0) = (SimMem.tgt sm0)).

Theorem make_match_genvs :
SimSymbId.sim_skenv (SkEnv.project skenv_link (Mod.sk md_src))
Expand Down
4 changes: 2 additions & 2 deletions backend/DebugvarproofC.v
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -41,8 +41,8 @@ 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: (get_mem st_src0) = sm0.(SimMem.src))
(MCOMPATTGT: (get_mem st_tgt0) = sm0.(SimMem.tgt))
(MCOMPATSRC: (get_mem st_src0) = (SimMem.src sm0))
(MCOMPATTGT: (get_mem st_tgt0) = (SimMem.tgt sm0))
(DUMMYTGT: strong_wf_tgt st_tgt0).

Theorem make_match_genvs :
Expand Down
4 changes: 2 additions & 2 deletions backend/LinearizeproofC.v
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -44,8 +44,8 @@ Inductive match_states
(idx: nat) (st_src0: LTL.state) (st_tgt0: Linear.state) (sm0: SimMem.t): Prop :=
| match_states_intro
(MATCHST: Linearizeproof.match_states st_src0 st_tgt0)
(MCOMPATSRC: (LTLC.get_mem st_src0) = sm0.(SimMem.src))
(MCOMPATTGT: (LinearC.get_mem st_tgt0) = sm0.(SimMem.tgt))
(MCOMPATSRC: (LTLC.get_mem st_src0) = (SimMem.src sm0))
(MCOMPATTGT: (LinearC.get_mem st_tgt0) = (SimMem.tgt sm0))
(DUMMYTGT: strong_wf_tgt st_tgt0)
(MEASURE: measure st_src0 = idx).

Expand Down
2 changes: 1 addition & 1 deletion backend/LocationsC.v
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -347,7 +347,7 @@ Lemma arguments_loc sg sl delta ty
Proof.
generalize (loc_arguments_acceptable_2 _ _ IN). i. ss. des_ifs.
set (loc_arguments_bounded _ _ _ IN).
splits; eauto; [omega|]. unfold typesize in *. des_ifs; ss; lia.
splits; eauto; [lia|]. unfold typesize in *. des_ifs; ss; lia.
Qed.

Lemma regs_of_rpair_In A (l: list (rpair A)):
Expand Down
24 changes: 12 additions & 12 deletions backend/MachExtra.v
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -21,17 +21,17 @@ Hint Unfold valid_blocks src_private tgt_private range.
Lemma mach_store_arguments_simmem
sm0 rs vs sg m_tgt0
(MWF: SimMem.wf sm0)
(STORE: StoreArguments.store_arguments sm0.(SimMem.tgt) rs vs sg m_tgt0):
(STORE: StoreArguments.store_arguments (SimMem.tgt sm0) rs vs sg m_tgt0):
(*** TODO: don't use unchanged_on, it is needlessly complex for our use. just define my own. *)
exists sm1,
<<SM: sm1 = (mk sm0.(src) m_tgt0 sm0.(inj)
sm0.(src_external) sm0.(tgt_external)
sm0.(src_parent_nb) sm0.(tgt_parent_nb)
sm0.(src_ge_nb) sm0.(tgt_ge_nb))>> /\
<<SM: sm1 = (mk (src sm0) m_tgt0 (inj sm0)
(src_external sm0) (tgt_external sm0)
(src_parent_nb sm0) (tgt_parent_nb sm0)
(src_ge_nb sm0) (tgt_ge_nb sm0))>> /\
<<MWF: SimMem.wf sm1>> /\
<<MLE: SimMem.le sm0 sm1>> /\
<<PRIV: forall ofs (IN: 0 <= ofs < 4 * size_arguments sg),
(tgt_private sm1) sm0.(SimMem.tgt).(Mem.nextblock) ofs>>.
(tgt_private sm1) (SimMem.tgt sm0).(Mem.nextblock) ofs>>.
Proof.
i. subst_locals. inv STORE.
exploit Mem.alloc_right_inject; try apply MWF; eauto. i; des.
Expand All @@ -41,21 +41,21 @@ Proof.
- econs; ss; try apply MWF; eauto.
+ eapply Mem.inject_extends_compose; eauto. econs; eauto.
{ econs.
- ii. inv H0. replace (ofs + 0) with ofs by omega.
- ii. inv H0. replace (ofs + 0) with ofs by lia.
destruct (eq_block b2 (Mem.nextblock (tgt sm0))); destruct (zle 0 ofs); destruct (zlt ofs (4 * size_arguments sg));
try (eapply Mem.perm_unchanged_on; eauto; ss; des_ifs; omega).
subst b2. exploit (PERM ofs). omega. i. eapply Mem.perm_cur. eapply Mem.perm_implies; eauto. econs.
try (eapply Mem.perm_unchanged_on; eauto; ss; des_ifs; lia).
subst b2. exploit (PERM ofs). lia. i. eapply Mem.perm_cur. eapply Mem.perm_implies; eauto. econs.
- ii. inv H0. eapply Z.divide_0_r.
- ii. inv H0. replace (ofs + 0) with ofs by omega.
- ii. inv H0. replace (ofs + 0) with ofs by lia.
destruct (eq_block b2 (Mem.nextblock (tgt sm0))); destruct (zle 0 ofs); destruct (zlt ofs (4 * size_arguments sg));
try (exploit Mem.unchanged_on_contents; eauto; ss; des_ifs; try omega; i; rewrite H0; eapply memval_inject_Reflexive).
try (exploit Mem.unchanged_on_contents; eauto; ss; des_ifs; try lia; i; rewrite H0; eapply memval_inject_Reflexive).
Transparent Mem.alloc. unfold Mem.alloc in ALC. inv ALC. ss.
rewrite PMap.gss. rewrite ZMap.gi. eapply memval_inject_undef.
}
{ i. left. assert(Mem.valid_block m1 b).
{ r. rewrite NB. eapply Mem.perm_valid_block; eauto. }
destruct (eq_block b (Mem.nextblock (tgt sm0))) eqn:BEQ; destruct (zle 0 ofs); destruct (zlt ofs (4 * size_arguments sg));
try by (eapply Mem.perm_unchanged_on_2; eauto; ss; rewrite BEQ; eauto; try omega).
try by (eapply Mem.perm_unchanged_on_2; eauto; ss; rewrite BEQ; eauto; try lia).
subst b. eapply Mem.perm_cur. eapply Mem.perm_implies. eapply Mem.perm_alloc_2; eauto. econs.
}
+ etransitivity; try apply MWF; eauto. unfold tgt_private. ss. u. ii; des. esplits; eauto with congruence.
Expand Down
4 changes: 2 additions & 2 deletions backend/RTLC.v
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -39,7 +39,7 @@ Section MODSEM.
(CSTYLE: Args.is_cstyle args /\ fd.(fn_sig).(sig_cstyle) = true)
(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)):
(LEN: (length (Args.vs args)) = (length fd.(fn_sig).(sig_args))):
initial_frame args (Callstate [] (Args.fptr args) fd.(fn_sig) tvs (Args.m args)).

Inductive initial_frame2 (args: Args.t): state -> Prop :=
Expand All @@ -48,7 +48,7 @@ Section MODSEM.
(CSTYLE: Args.is_cstyle args /\ fd.(fn_sig).(sig_cstyle) = true)
(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))
(LEN: length (Args.vs args) = length fd.(fn_sig).(sig_args))
(JUNK: assign_junk_blocks (Args.m args) n = m0):
initial_frame2 args (Callstate [] (Args.fptr args) fd.(fn_sig) tvs m0).

Expand Down
4 changes: 2 additions & 2 deletions backend/RTLgenproofC.v
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -38,8 +38,8 @@ Inductive match_states
(idx: nat * nat) (st_src0: CminorSel.state) (st_tgt0: RTL.state) (sm0: SimMem.t): Prop :=
| match_states_intro
(MATCHST: RTLgenproof.match_states st_src0 st_tgt0)
(MCOMPATSRC: (CminorSelC.get_mem st_src0) = sm0.(SimMem.src))
(MCOMPATTGT: (get_mem st_tgt0) = sm0.(SimMem.tgt))
(MCOMPATSRC: (CminorSelC.get_mem st_src0) = (SimMem.src sm0))
(MCOMPATTGT: (get_mem st_tgt0) = (SimMem.tgt sm0))
(MEASRUE: idx = measure_state st_src0).

Theorem make_match_genvs :
Expand Down
4 changes: 2 additions & 2 deletions backend/RenumberproofC.v
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -35,8 +35,8 @@ Inductive match_states
(idx: nat) (st_src0: RTL.state) (st_tgt0: RTL.state) (sm0: SimMem.t): Prop :=
| match_states_intro
(MATCHST: Renumberproof.match_states st_src0 st_tgt0)
(MCOMPATSRC: (get_mem st_src0) = sm0.(SimMem.src))
(MCOMPATTGT: (get_mem st_tgt0) = sm0.(SimMem.tgt)).
(MCOMPATSRC: (get_mem st_src0) = (SimMem.src sm0))
(MCOMPATTGT: (get_mem st_tgt0) = (SimMem.tgt sm0)).

Theorem make_match_genvs :
SimSymbId.sim_skenv (SkEnv.project skenv_link (Mod.sk md_src))
Expand Down
4 changes: 2 additions & 2 deletions backend/SelectionproofC.v
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -39,8 +39,8 @@ Inductive match_states
(idx: nat) (st_src0: Cminor.state) (st_tgt0: CminorSel.state) (sm0: SimMem.t): Prop :=
| match_states_intro
(MATCHST: Selectionproof.match_states prog ge st_src0 st_tgt0)
(MCOMPATSRC: (CminorC.get_mem st_src0) = sm0.(SimMem.src))
(MCOMPATTGT: (CminorSelC.get_mem st_tgt0) = sm0.(SimMem.tgt))
(MCOMPATSRC: (CminorC.get_mem st_src0) = (SimMem.src sm0))
(MCOMPATTGT: (CminorSelC.get_mem st_tgt0) = (SimMem.tgt sm0))
(MEASURE: idx = measure st_src0).

Theorem make_match_genvs :
Expand Down
Loading