diff options
59 files changed, 2379 insertions, 763 deletions
@@ -71,6 +71,8 @@ backend/NeedDomain.vo backend/NeedDomain.glob backend/NeedDomain.v.beautified: b $(ARCH)/NeedOp.vo $(ARCH)/NeedOp.glob $(ARCH)/NeedOp.v.beautified: $(ARCH)/NeedOp.v lib/Coqlib.vo common/AST.vo lib/Integers.vo lib/Floats.vo common/Values.vo common/Memory.vo common/Globalenvs.vo $(ARCH)/Op.vo backend/NeedDomain.vo backend/RTL.vo backend/Deadcode.vo backend/Deadcode.glob backend/Deadcode.v.beautified: backend/Deadcode.v lib/Coqlib.vo common/Errors.vo lib/Maps.vo common/AST.vo lib/Integers.vo lib/Floats.vo common/Memory.vo backend/Registers.vo $(ARCH)/Op.vo backend/RTL.vo lib/Lattice.vo backend/Kildall.vo backend/ValueDomain.vo backend/ValueAnalysis.vo backend/NeedDomain.vo $(ARCH)/NeedOp.vo backend/Deadcodeproof.vo backend/Deadcodeproof.glob backend/Deadcodeproof.v.beautified: backend/Deadcodeproof.v lib/Coqlib.vo common/Errors.vo lib/Maps.vo lib/IntvSets.vo common/AST.vo lib/Integers.vo lib/Floats.vo common/Values.vo common/Memory.vo common/Globalenvs.vo common/Events.vo common/Smallstep.vo $(ARCH)/Op.vo backend/Registers.vo backend/RTL.vo lib/Lattice.vo backend/Kildall.vo backend/ValueDomain.vo backend/ValueAnalysis.vo backend/NeedDomain.vo $(ARCH)/NeedOp.vo backend/Deadcode.vo +backend/Unusedglob.vo backend/Unusedglob.glob backend/Unusedglob.v.beautified: backend/Unusedglob.v lib/Coqlib.vo lib/Ordered.vo lib/Maps.vo lib/Iteration.vo common/AST.vo common/Errors.vo $(ARCH)/Op.vo backend/Registers.vo backend/RTL.vo +backend/Unusedglobproof.vo backend/Unusedglobproof.glob backend/Unusedglobproof.v.beautified: backend/Unusedglobproof.v lib/Coqlib.vo lib/Ordered.vo lib/Maps.vo lib/Iteration.vo common/AST.vo common/Errors.vo lib/Integers.vo common/Values.vo common/Memory.vo common/Globalenvs.vo common/Events.vo common/Smallstep.vo $(ARCH)/Op.vo backend/Registers.vo backend/RTL.vo backend/Unusedglob.vo $(ARCH)/Machregs.vo $(ARCH)/Machregs.glob $(ARCH)/Machregs.v.beautified: $(ARCH)/Machregs.v lib/Coqlib.vo lib/Maps.vo common/AST.vo lib/Integers.vo $(ARCH)/Op.vo backend/Locations.vo backend/Locations.glob backend/Locations.v.beautified: backend/Locations.v lib/Coqlib.vo lib/Maps.vo lib/Ordered.vo common/AST.vo common/Values.vo $(ARCH)/Machregs.vo $(ARCH)/Conventions1.vo $(ARCH)/Conventions1.glob $(ARCH)/Conventions1.v.beautified: $(ARCH)/Conventions1.v lib/Coqlib.vo common/AST.vo common/Events.vo backend/Locations.vo @@ -117,7 +119,7 @@ cfrontend/Csharpminor.vo cfrontend/Csharpminor.glob cfrontend/Csharpminor.v.beau cfrontend/Cminorgen.vo cfrontend/Cminorgen.glob cfrontend/Cminorgen.v.beautified: cfrontend/Cminorgen.v lib/Coqlib.vo common/Errors.vo lib/Maps.vo lib/Ordered.vo common/AST.vo lib/Integers.vo lib/Floats.vo cfrontend/Csharpminor.vo backend/Cminor.vo cfrontend/Cminorgenproof.vo cfrontend/Cminorgenproof.glob cfrontend/Cminorgenproof.v.beautified: cfrontend/Cminorgenproof.v lib/Coqlib.vo lib/Intv.vo common/Errors.vo lib/Maps.vo common/AST.vo lib/Integers.vo lib/Floats.vo common/Values.vo common/Memory.vo common/Events.vo common/Globalenvs.vo common/Smallstep.vo common/Switch.vo cfrontend/Csharpminor.vo backend/Cminor.vo cfrontend/Cminorgen.vo driver/Compopts.vo driver/Compopts.glob driver/Compopts.v.beautified: driver/Compopts.v -driver/Compiler.vo driver/Compiler.glob driver/Compiler.v.beautified: driver/Compiler.v lib/Coqlib.vo common/Errors.vo common/AST.vo common/Smallstep.vo cfrontend/Csyntax.vo cfrontend/Csem.vo cfrontend/Cstrategy.vo cfrontend/Cexec.vo cfrontend/Clight.vo cfrontend/Csharpminor.vo backend/Cminor.vo backend/CminorSel.vo backend/RTL.vo backend/LTL.vo backend/Linear.vo backend/Mach.vo $(ARCH)/Asm.vo cfrontend/Initializers.vo cfrontend/SimplExpr.vo cfrontend/SimplLocals.vo cfrontend/Cshmgen.vo cfrontend/Cminorgen.vo backend/Selection.vo backend/RTLgen.vo backend/Tailcall.vo backend/Inlining.vo backend/Renumber.vo backend/Constprop.vo backend/CSE.vo backend/Deadcode.vo backend/Allocation.vo backend/Tunneling.vo backend/Linearize.vo backend/CleanupLabels.vo backend/Stacking.vo $(ARCH)/Asmgen.vo cfrontend/SimplExprproof.vo cfrontend/SimplLocalsproof.vo cfrontend/Cshmgenproof.vo cfrontend/Cminorgenproof.vo backend/Selectionproof.vo backend/RTLgenproof.vo backend/Tailcallproof.vo backend/Inliningproof.vo backend/Renumberproof.vo backend/Constpropproof.vo backend/CSEproof.vo backend/Deadcodeproof.vo backend/Allocproof.vo backend/Tunnelingproof.vo backend/Linearizeproof.vo backend/CleanupLabelsproof.vo backend/Stackingproof.vo $(ARCH)/Asmgenproof.vo +driver/Compiler.vo driver/Compiler.glob driver/Compiler.v.beautified: driver/Compiler.v lib/Coqlib.vo common/Errors.vo common/AST.vo common/Smallstep.vo cfrontend/Csyntax.vo cfrontend/Csem.vo cfrontend/Cstrategy.vo cfrontend/Cexec.vo cfrontend/Clight.vo cfrontend/Csharpminor.vo backend/Cminor.vo backend/CminorSel.vo backend/RTL.vo backend/LTL.vo backend/Linear.vo backend/Mach.vo $(ARCH)/Asm.vo cfrontend/Initializers.vo cfrontend/SimplExpr.vo cfrontend/SimplLocals.vo cfrontend/Cshmgen.vo cfrontend/Cminorgen.vo backend/Selection.vo backend/RTLgen.vo backend/Tailcall.vo backend/Inlining.vo backend/Renumber.vo backend/Constprop.vo backend/CSE.vo backend/Deadcode.vo backend/Unusedglob.vo backend/Allocation.vo backend/Tunneling.vo backend/Linearize.vo backend/CleanupLabels.vo backend/Stacking.vo $(ARCH)/Asmgen.vo cfrontend/SimplExprproof.vo cfrontend/SimplLocalsproof.vo cfrontend/Cshmgenproof.vo cfrontend/Cminorgenproof.vo backend/Selectionproof.vo backend/RTLgenproof.vo backend/Tailcallproof.vo backend/Inliningproof.vo backend/Renumberproof.vo backend/Constpropproof.vo backend/CSEproof.vo backend/Deadcodeproof.vo backend/Allocproof.vo backend/Tunnelingproof.vo backend/Linearizeproof.vo backend/CleanupLabelsproof.vo backend/Stackingproof.vo $(ARCH)/Asmgenproof.vo driver/Complements.vo driver/Complements.glob driver/Complements.v.beautified: driver/Complements.v lib/Coqlib.vo common/AST.vo lib/Integers.vo common/Values.vo common/Events.vo common/Globalenvs.vo common/Smallstep.vo common/Behaviors.vo cfrontend/Csyntax.vo cfrontend/Csem.vo cfrontend/Cstrategy.vo cfrontend/Clight.vo backend/Cminor.vo backend/RTL.vo $(ARCH)/Asm.vo driver/Compiler.vo common/Errors.vo flocq/Core/Fcore_Raux.vo flocq/Core/Fcore_Raux.glob flocq/Core/Fcore_Raux.v.beautified: flocq/Core/Fcore_Raux.v flocq/Core/Fcore_Zaux.vo flocq/Core/Fcore_Zaux.vo flocq/Core/Fcore_Zaux.glob flocq/Core/Fcore_Zaux.v.beautified: flocq/Core/Fcore_Zaux.v @@ -28,6 +28,7 @@ COQDEP="$(COQBIN)coqdep" $(COQINCLUDES) COQDOC="$(COQBIN)coqdoc" COQEXEC="$(COQBIN)coqtop" $(COQINCLUDES) -batch -load-vernac-source COQCHK="$(COQBIN)coqchk" $(COQINCLUDES) +CP=cp VPATH=$(DIRS) GPATH=$(DIRS) @@ -74,6 +75,7 @@ BACKEND=\ ConstpropOp.v Constprop.v ConstpropOpproof.v Constpropproof.v \ CSEdomain.v CombineOp.v CSE.v CombineOpproof.v CSEproof.v \ NeedDomain.v NeedOp.v Deadcode.v Deadcodeproof.v \ + Unusedglob.v Unusedglobproof.v \ Machregs.v Locations.v Conventions1.v Conventions.v LTL.v \ Allocation.v Allocproof.v \ Tunneling.v Tunnelingproof.v \ @@ -190,16 +192,16 @@ latexdoc: @chmod -w $*.v compcert.ini: Makefile.config VERSION - (echo stdlib_path=$(LIBDIR); \ - echo prepro=$(CPREPRO); \ - echo asm=$(CASM); \ - echo linker=$(CLINKER); \ - echo arch=$(ARCH); \ - echo model=$(MODEL); \ - echo abi=$(ABI); \ - echo system=$(SYSTEM); \ - echo has_runtime_lib=$(HAS_RUNTIME_LIB); \ - echo asm_supports_cfi=$(ASM_SUPPORTS_CFI); \ + (echo "stdlib_path=$(LIBDIR)"; \ + echo "prepro=$(CPREPRO)"; \ + echo "asm=$(CASM)"; \ + echo "linker=$(CLINKER)"; \ + echo "arch=$(ARCH)"; \ + echo "model=$(MODEL)"; \ + echo "abi=$(ABI)"; \ + echo "system=$(SYSTEM)"; \ + echo "has_runtime_lib=$(HAS_RUNTIME_LIB)"; \ + echo "asm_supports_cfi=$(ASM_SUPPORTS_CFI)"; \ version=`cat VERSION`; \ echo version=$$version) \ > compcert.ini diff --git a/arm/Asmgenproof.v b/arm/Asmgenproof.v index 713e012c..c687722c 100644 --- a/arm/Asmgenproof.v +++ b/arm/Asmgenproof.v @@ -50,6 +50,14 @@ Proof. exact TRANSF. Qed. +Lemma public_preserved: + forall id, Genv.public_symbol tge id = Genv.public_symbol ge id. +Proof. + intros. unfold ge, tge. + apply Genv.public_symbol_transf_partial with transf_fundef. + exact TRANSF. +Qed. + Lemma functions_translated: forall b f, Genv.find_funct_ptr ge b = Some f -> @@ -748,7 +756,7 @@ Opaque loadind. eapply exec_step_builtin. eauto. eauto. eapply find_instr_tail; eauto. eapply external_call_symbols_preserved'; eauto. - exact symbols_preserved. exact varinfo_preserved. + exact symbols_preserved. exact public_preserved. exact varinfo_preserved. eauto. econstructor; eauto. Simpl. rewrite set_pregs_other_2. rewrite undef_regs_other_2. rewrite <- H0. simpl. econstructor; eauto. @@ -770,7 +778,7 @@ Opaque loadind. eapply exec_step_annot. eauto. eauto. eapply find_instr_tail; eauto. eauto. eapply external_call_symbols_preserved'; eauto. - exact symbols_preserved. exact varinfo_preserved. + exact symbols_preserved. exact public_preserved. exact varinfo_preserved. eapply match_states_intro with (ep := false); eauto with coqlib. unfold nextinstr. rewrite Pregmap.gss. rewrite <- H1; simpl. econstructor; eauto. @@ -927,7 +935,7 @@ Opaque loadind. left; econstructor; split. apply plus_one. eapply exec_step_external; eauto. eapply external_call_symbols_preserved'; eauto. - exact symbols_preserved. exact varinfo_preserved. + exact symbols_preserved. exact public_preserved. exact varinfo_preserved. econstructor; eauto. apply agree_set_other; auto with asmgen. eapply agree_set_mregs; eauto. @@ -972,7 +980,7 @@ Theorem transf_program_correct: forward_simulation (Mach.semantics return_address_offset prog) (Asm.semantics tprog). Proof. eapply forward_simulation_star with (measure := measure). - eexact symbols_preserved. + eexact public_preserved. eexact transf_initial_states. eexact transf_final_states. exact step_simulation. @@ -720,36 +720,15 @@ Proof. intros. destruct c; simpl; auto; congruence. Qed. -(** Checking whether two addressings, applied to the same arguments, produce - separated memory addresses. Used in [CSE]. *) - -Definition addressing_separated (chunk1: memory_chunk) (addr1: addressing) - (chunk2: memory_chunk) (addr2: addressing) : bool := - match addr1, addr2 with - | Aindexed ofs1, Aindexed ofs2 => - Int.no_overlap ofs1 (size_chunk chunk1) ofs2 (size_chunk chunk2) - | Ainstack ofs1, Ainstack ofs2 => - Int.no_overlap ofs1 (size_chunk chunk1) ofs2 (size_chunk chunk2) - | _, _ => false +(** Global variables mentioned in an operation or addressing mode *) + +Definition globals_operation (op: operation) : list ident := + match op with + | Oaddrsymbol s ofs => s :: nil + | _ => nil end. -Lemma addressing_separated_sound: - forall (F V: Type) (ge: Genv.t F V) sp chunk1 addr1 chunk2 addr2 vl b1 n1 b2 n2, - addressing_separated chunk1 addr1 chunk2 addr2 = true -> - eval_addressing ge sp addr1 vl = Some(Vptr b1 n1) -> - eval_addressing ge sp addr2 vl = Some(Vptr b2 n2) -> - b1 <> b2 \/ Int.unsigned n1 + size_chunk chunk1 <= Int.unsigned n2 \/ Int.unsigned n2 + size_chunk chunk2 <= Int.unsigned n1. -Proof. - unfold addressing_separated; intros. - generalize (size_chunk_pos chunk1) (size_chunk_pos chunk2); intros SZ1 SZ2. - destruct addr1; destruct addr2; try discriminate; simpl in *; FuncInv. -(* Aindexed *) - destruct v; simpl in *; inv H1; inv H2. - right. apply Int.no_overlap_sound; auto. -(* Ainstack *) - destruct sp; simpl in *; inv H1; inv H2. - right. apply Int.no_overlap_sound; auto. -Qed. +Definition globals_addressing (addr: addressing) : list ident := nil. (** * Invariance and compatibility properties. *) @@ -791,14 +770,11 @@ End GENV_TRANSF. Section EVAL_COMPAT. -Variable F V: Type. -Variable genv: Genv.t F V. +Variable F1 F2 V1 V2: Type. +Variable ge1: Genv.t F1 V1. +Variable ge2: Genv.t F2 V2. Variable f: meminj. -Hypothesis symbol_address_inj: - forall id ofs, - val_inject f (Genv.symbol_address genv id ofs) (Genv.symbol_address genv id ofs). - Variable m1: mem. Variable m2: mem. @@ -885,12 +861,16 @@ Ltac TrivialExists := Lemma eval_operation_inj: forall op sp1 vl1 sp2 vl2 v1, + (forall id ofs, + In id (globals_operation op) -> + val_inject f (Genv.symbol_address ge1 id ofs) (Genv.symbol_address ge2 id ofs)) -> val_inject f sp1 sp2 -> val_list_inject f vl1 vl2 -> - eval_operation genv sp1 op vl1 m1 = Some v1 -> - exists v2, eval_operation genv sp2 op vl2 m2 = Some v2 /\ val_inject f v1 v2. + eval_operation ge1 sp1 op vl1 m1 = Some v1 -> + exists v2, eval_operation ge2 sp2 op vl2 m2 = Some v2 /\ val_inject f v1 v2. Proof. - intros. destruct op; simpl in H1; simpl; FuncInv; InvInject; TrivialExists. + intros until v1; intros GL; intros. destruct op; simpl in H1; simpl; FuncInv; InvInject; TrivialExists. + apply GL; simpl; auto. apply Values.val_add_inject; auto. inv H4; simpl; auto. inv H4; simpl; auto. @@ -976,15 +956,15 @@ Qed. Lemma eval_addressing_inj: forall addr sp1 vl1 sp2 vl2 v1, + (forall id ofs, + In id (globals_addressing addr) -> + val_inject f (Genv.symbol_address ge1 id ofs) (Genv.symbol_address ge2 id ofs)) -> val_inject f sp1 sp2 -> val_list_inject f vl1 vl2 -> - eval_addressing genv sp1 addr vl1 = Some v1 -> - exists v2, eval_addressing genv sp2 addr vl2 = Some v2 /\ val_inject f v1 v2. + eval_addressing ge1 sp1 addr vl1 = Some v1 -> + exists v2, eval_addressing ge2 sp2 addr vl2 = Some v2 /\ val_inject f v1 v2. Proof. - assert (UNUSED: forall id ofs, - val_inject f (Genv.symbol_address genv id ofs) (Genv.symbol_address genv id ofs)). - exact symbol_address_inj. - intros. destruct addr; simpl in H1; simpl; FuncInv; InvInject; TrivialExists. + intros. destruct addr; simpl in H2; simpl; FuncInv; InvInject; TrivialExists. apply Values.val_add_inject; auto. apply Values.val_add_inject; auto. apply Values.val_add_inject; auto. apply eval_shift_inj; auto. @@ -1069,11 +1049,11 @@ Proof. eval_operation genv sp op vl2 m2 = Some v2 /\ val_inject (fun b => Some(b, 0)) v1 v2). eapply eval_operation_inj with (m1 := m1) (sp1 := sp). - intros. rewrite <- val_inject_lessdef; auto. apply valid_pointer_extends; auto. apply weak_valid_pointer_extends; auto. apply weak_valid_pointer_no_overflow_extends. apply valid_different_pointers_extends; auto. + intros. rewrite <- val_inject_lessdef; auto. rewrite <- val_inject_lessdef; auto. eauto. auto. destruct H2 as [v2 [A B]]. exists v2; split; auto. rewrite val_inject_lessdef; auto. @@ -1144,7 +1124,7 @@ Proof. intros. rewrite eval_shift_stack_addressing. simpl. eapply eval_addressing_inj with (sp1 := Vptr sp1 Int.zero); eauto. - exact symbol_address_inject. + intros; apply symbol_address_inject. Qed. Lemma eval_operation_inject: @@ -1159,11 +1139,11 @@ Proof. intros. rewrite eval_shift_stack_operation. simpl. eapply eval_operation_inj with (sp1 := Vptr sp1 Int.zero) (m1 := m1); eauto. - exact symbol_address_inject. intros; eapply Mem.valid_pointer_inject_val; eauto. intros; eapply Mem.weak_valid_pointer_inject_val; eauto. intros; eapply Mem.weak_valid_pointer_inject_no_overflow; eauto. intros; eapply Mem.different_pointers_inject; eauto. + intros; apply symbol_address_inject. Qed. End EVAL_INJECT. diff --git a/arm/PrintAsm.ml b/arm/PrintAsm.ml index 7b9e2cc8..c7157aac 100644 --- a/arm/PrintAsm.ml +++ b/arm/PrintAsm.ml @@ -168,8 +168,10 @@ let thumbS oc = let name_of_section = function | Section_text -> ".text" - | Section_data i | Section_small_data i -> if i then ".data" else "COMM" - | Section_const | Section_small_const -> ".section .rodata" + | Section_data i | Section_small_data i -> + if i then ".data" else "COMM" + | Section_const i | Section_small_const i -> + if i then ".section .rodata" else "COMM" | Section_string -> ".section .rodata" | Section_literal -> ".text" | Section_jumptable -> ".text" diff --git a/arm/Unusedglob1.ml b/arm/Unusedglob1.ml deleted file mode 100644 index 33a9bf8d..00000000 --- a/arm/Unusedglob1.ml +++ /dev/null @@ -1,32 +0,0 @@ -(* *********************************************************************) -(* *) -(* The Compcert verified compiler *) -(* *) -(* Xavier Leroy, INRIA Paris-Rocquencourt *) -(* *) -(* Copyright Institut National de Recherche en Informatique et en *) -(* Automatique. All rights reserved. This file is distributed *) -(* under the terms of the INRIA Non-Commercial License Agreement. *) -(* *) -(* *********************************************************************) - -(* Identifiers referenced from an ARM Asm instruction *) - -open Datatypes -open AST -open Asm - -let referenced_builtin ef = - match ef with - | EF_vload_global(chunk, id, ofs) -> [id] - | EF_vstore_global(chunk, id, ofs) -> [id] - | _ -> [] - -let referenced_instr = function - | Pbsymb(s, _) -> [s] - | Pblsymb(s, _) -> [s] - | Ploadsymbol(_, s, _) -> [s] - | Pbuiltin(ef, _, _) -> referenced_builtin ef - | _ -> [] - -let code_of_function f = f.fn_code diff --git a/backend/Allocproof.v b/backend/Allocproof.v index 588a674e..2612ebf2 100644 --- a/backend/Allocproof.v +++ b/backend/Allocproof.v @@ -1453,6 +1453,14 @@ Proof. exact TRANSF. Qed. +Lemma public_preserved: + forall (s: ident), Genv.public_symbol tge s = Genv.public_symbol ge s. +Proof. + intro. unfold ge, tge. + apply Genv.public_symbol_transf_partial with transf_fundef. + exact TRANSF. +Qed. + Lemma varinfo_preserved: forall b, Genv.find_var_info tge b = Genv.find_var_info ge b. Proof. @@ -2016,7 +2024,7 @@ Proof. eapply star_trans. eexact A1. eapply star_left. econstructor. econstructor. unfold reglist. eapply external_call_symbols_preserved; eauto. - exact symbols_preserved. exact varinfo_preserved. + exact symbols_preserved. exact public_preserved. exact varinfo_preserved. instantiate (1 := vl'); auto. instantiate (1 := ls2); auto. eapply star_right. eexact A3. @@ -2038,7 +2046,7 @@ Proof. eapply star_two. econstructor. eapply external_call_symbols_preserved' with (ge1 := ge). econstructor; eauto. - exact symbols_preserved. exact varinfo_preserved. + exact symbols_preserved. exact public_preserved. exact varinfo_preserved. eauto. constructor. eauto. eauto. traceEq. exploit satisf_successors. eauto. eauto. simpl; eauto. eauto. eapply satisf_undef_reg with (r := res). @@ -2133,7 +2141,7 @@ Proof. apply plus_one. econstructor; eauto. eapply external_call_symbols_preserved' with (ge1 := ge). econstructor; eauto. - exact symbols_preserved. exact varinfo_preserved. + exact symbols_preserved. exact public_preserved. exact varinfo_preserved. econstructor; eauto. simpl. replace (map (Locmap.setlist (map R (loc_result (ef_sig ef))) @@ -2204,7 +2212,7 @@ Theorem transf_program_correct: Proof. set (ms := fun s s' => wt_state s /\ match_states s s'). eapply forward_simulation_plus with (match_states := ms). -- exact symbols_preserved. +- exact public_preserved. - intros. exploit initial_states_simulation; eauto. intros [st2 [A B]]. exists st2; split; auto. split; auto. apply wt_initial_state with (p := prog); auto. exact wt_prog. diff --git a/backend/CMparser.mly b/backend/CMparser.mly index ad92a12e..10cf8bf4 100644 --- a/backend/CMparser.mly +++ b/backend/CMparser.mly @@ -400,10 +400,12 @@ let mkmatch expr cases = prog: EQUAL STRINGLIT global_declarations EOF { { prog_defs = List.rev $3; + prog_public = List.map fst $3; (* FIXME *) prog_main = intern_string $2; } } | global_declarations EOF { { prog_defs = List.rev $1; + prog_public = List.map fst $1; (* FIXME *) prog_main = intern_string "main" } } ; diff --git a/backend/CSEproof.v b/backend/CSEproof.v index af138f83..ae8052be 100644 --- a/backend/CSEproof.v +++ b/backend/CSEproof.v @@ -818,6 +818,10 @@ Lemma symbols_preserved: forall (s: ident), Genv.find_symbol tge s = Genv.find_symbol ge s. Proof (Genv.find_symbol_transf_partial (transf_fundef rm) prog TRANSF). +Lemma public_preserved: + forall (s: ident), Genv.public_symbol tge s = Genv.public_symbol ge s. +Proof (Genv.public_symbol_transf_partial (transf_fundef rm) prog TRANSF). + Lemma varinfo_preserved: forall b, Genv.find_var_info tge b = Genv.find_var_info ge b. Proof (Genv.find_var_info_transf_partial (transf_fundef rm) prog TRANSF). @@ -1104,7 +1108,7 @@ Proof. econstructor; split. eapply exec_Ibuiltin; eauto. eapply external_call_symbols_preserved; eauto. - exact symbols_preserved. exact varinfo_preserved. + exact symbols_preserved. exact public_preserved. exact varinfo_preserved. econstructor; eauto. eapply analysis_correct_1; eauto. simpl; auto. * unfold transfer; rewrite H. @@ -1188,7 +1192,7 @@ Proof. econstructor; split. eapply exec_function_external; eauto. eapply external_call_symbols_preserved; eauto. - exact symbols_preserved. exact varinfo_preserved. + exact symbols_preserved. exact public_preserved. exact varinfo_preserved. econstructor; eauto. - (* return *) @@ -1227,7 +1231,7 @@ Theorem transf_program_correct: Proof. eapply forward_simulation_step with (match_states := fun s1 s2 => sound_state prog s1 /\ match_states s1 s2). -- eexact symbols_preserved. +- eexact public_preserved. - intros. exploit transf_initial_states; eauto. intros [s2 [A B]]. exists s2. split. auto. split. apply sound_initial; auto. auto. - intros. destruct H. eapply transf_final_states; eauto. diff --git a/backend/CleanupLabelsproof.v b/backend/CleanupLabelsproof.v index 65ba61c9..f952f1ea 100644 --- a/backend/CleanupLabelsproof.v +++ b/backend/CleanupLabelsproof.v @@ -43,6 +43,13 @@ Proof. apply Genv.find_symbol_transf. Qed. +Lemma public_preserved: + forall (s: ident), Genv.public_symbol tge s = Genv.public_symbol ge s. +Proof. + intros; unfold ge, tge, tprog, transf_program. + apply Genv.public_symbol_transf. +Qed. + Lemma varinfo_preserved: forall b, Genv.find_var_info tge b = Genv.find_var_info ge b. Proof. @@ -285,12 +292,12 @@ Proof. (* Lbuiltin *) left; econstructor; split. econstructor; eauto. eapply external_call_symbols_preserved'; eauto. - exact symbols_preserved. exact varinfo_preserved. + exact symbols_preserved. exact public_preserved. exact varinfo_preserved. econstructor; eauto with coqlib. (* Lannot *) left; econstructor; split. econstructor; eauto. eapply external_call_symbols_preserved'; eauto. - exact symbols_preserved. exact varinfo_preserved. + exact symbols_preserved. exact public_preserved. exact varinfo_preserved. econstructor; eauto with coqlib. (* Llabel *) case_eq (Labelset.mem lbl (labels_branched_to (fn_code f))); intros. @@ -329,7 +336,7 @@ Proof. (* external function *) left; econstructor; split. econstructor; eauto. eapply external_call_symbols_preserved'; eauto. - exact symbols_preserved. exact varinfo_preserved. + exact symbols_preserved. exact public_preserved. exact varinfo_preserved. econstructor; eauto with coqlib. (* return *) inv H3. inv H1. left; econstructor; split. @@ -362,7 +369,7 @@ Theorem transf_program_correct: forward_simulation (Linear.semantics prog) (Linear.semantics tprog). Proof. eapply forward_simulation_opt. - eexact symbols_preserved. + eexact public_preserved. eexact transf_initial_states. eexact transf_final_states. eexact transf_step_correct. diff --git a/backend/Constpropproof.v b/backend/Constpropproof.v index b79c721e..98e6e577 100644 --- a/backend/Constpropproof.v +++ b/backend/Constpropproof.v @@ -54,6 +54,13 @@ Proof. apply Genv.find_symbol_transf. Qed. +Lemma public_preserved: + forall (s: ident), Genv.public_symbol tge s = Genv.public_symbol ge s. +Proof. + intros; unfold ge, tge, tprog, transf_program. + apply Genv.public_symbol_transf. +Qed. + Lemma varinfo_preserved: forall b, Genv.find_var_info tge b = Genv.find_var_info ge b. Proof. @@ -510,7 +517,7 @@ Opaque builtin_strength_reduction. left; econstructor; econstructor; split. eapply exec_Ibuiltin. eauto. eapply external_call_symbols_preserved; eauto. - exact symbols_preserved. exact varinfo_preserved. + exact symbols_preserved. exact public_preserved. exact varinfo_preserved. eapply match_states_succ; eauto. simpl; auto. apply set_reg_lessdef; auto. @@ -582,7 +589,7 @@ Opaque builtin_strength_reduction. simpl. left; econstructor; econstructor; split. eapply exec_function_external; eauto. eapply external_call_symbols_preserved; eauto. - exact symbols_preserved. exact varinfo_preserved. + exact symbols_preserved. exact public_preserved. exact varinfo_preserved. constructor; auto. (* return *) @@ -638,7 +645,7 @@ Proof. intros [ [n2 [s2' [A B]]] | [n2 [A [B C]]]]. exists n2; exists s2'; split; auto. left; apply plus_one; auto. exists n2; exists s2; split; auto. right; split; auto. subst t; apply star_refl. -- eexact symbols_preserved. +- eexact public_preserved. Qed. End PRESERVATION. diff --git a/backend/Deadcodeproof.v b/backend/Deadcodeproof.v index 2fdedc63..4d09c5ba 100644 --- a/backend/Deadcodeproof.v +++ b/backend/Deadcodeproof.v @@ -381,6 +381,14 @@ Proof. exact TRANSF. Qed. +Lemma public_preserved: + forall (s: ident), Genv.public_symbol tge s = Genv.public_symbol ge s. +Proof. + intro. unfold ge, tge. + apply Genv.public_symbol_transf_partial with (transf_fundef rm). + exact TRANSF. +Qed. + Lemma varinfo_preserved: forall b, Genv.find_var_info tge b = Genv.find_var_info ge b. Proof. @@ -792,7 +800,7 @@ Ltac UseTransfer := eapply exec_Ibuiltin; eauto. eapply external_call_symbols_preserved. simpl. rewrite <- H4. constructor. eauto. - exact symbols_preserved. exact varinfo_preserved. + exact symbols_preserved. exact public_preserved. exact varinfo_preserved. eapply match_succ_states; eauto. simpl; auto. apply eagree_update; eauto 2 with na. eapply magree_monotone; eauto. intros. apply incl_nmem_add; auto. @@ -812,7 +820,7 @@ Ltac UseTransfer := eapply exec_Ibuiltin; eauto. eapply external_call_symbols_preserved. simpl. econstructor; eauto. - exact symbols_preserved. exact varinfo_preserved. + exact symbols_preserved. exact public_preserved. exact varinfo_preserved. eapply match_succ_states; eauto. simpl; auto. apply eagree_update; eauto 2 with na. eapply magree_monotone; eauto. intros. apply incl_nmem_add; auto. @@ -825,7 +833,7 @@ Ltac UseTransfer := econstructor; split. eapply exec_Ibuiltin; eauto. eapply external_call_symbols_preserved. simpl; eauto. - exact symbols_preserved. exact varinfo_preserved. + exact symbols_preserved. exact public_preserved. exact varinfo_preserved. eapply match_succ_states; eauto. simpl; auto. apply eagree_update; eauto 3 with na. + (* volatile global store *) @@ -838,7 +846,7 @@ Ltac UseTransfer := eapply exec_Ibuiltin; eauto. eapply external_call_symbols_preserved. simpl. rewrite volatile_store_global_charact. exists b; split; eauto. - exact symbols_preserved. exact varinfo_preserved. + exact symbols_preserved. exact public_preserved. exact varinfo_preserved. eapply match_succ_states; eauto. simpl; auto. apply eagree_update; eauto 2 with na. + (* memcpy *) @@ -870,7 +878,7 @@ Ltac UseTransfer := eapply exec_Ibuiltin; eauto. eapply external_call_symbols_preserved. simpl. inv LD1. inv LD2. econstructor; eauto. - exact symbols_preserved. exact varinfo_preserved. + exact symbols_preserved. exact public_preserved. exact varinfo_preserved. eapply match_succ_states; eauto. simpl; auto. apply eagree_update; eauto 3 with na. + (* memcpy eliminated *) @@ -893,7 +901,7 @@ Ltac UseTransfer := eapply exec_Ibuiltin; eauto. eapply external_call_symbols_preserved. simpl; constructor. eapply eventval_list_match_lessdef; eauto 2 with na. - exact symbols_preserved. exact varinfo_preserved. + exact symbols_preserved. exact public_preserved. exact varinfo_preserved. eapply match_succ_states; eauto. simpl; auto. apply eagree_update; eauto 2 with na. + (* annot val *) @@ -902,7 +910,7 @@ Ltac UseTransfer := eapply exec_Ibuiltin; eauto. eapply external_call_symbols_preserved. simpl; constructor. eapply eventval_match_lessdef; eauto 2 with na. - exact symbols_preserved. exact varinfo_preserved. + exact symbols_preserved. exact public_preserved. exact varinfo_preserved. eapply match_succ_states; eauto. simpl; auto. apply eagree_update; eauto 3 with na. + (* all other builtins *) @@ -917,7 +925,7 @@ Ltac UseTransfer := econstructor; split. eapply exec_Ibuiltin; eauto. eapply external_call_symbols_preserved. eauto. - exact symbols_preserved. exact varinfo_preserved. + exact symbols_preserved. exact public_preserved. exact varinfo_preserved. eapply match_succ_states; eauto. simpl; auto. apply eagree_update; eauto 3 with na. eapply mextends_agree; eauto. @@ -969,7 +977,7 @@ Ltac UseTransfer := econstructor; split. econstructor; eauto. eapply external_call_symbols_preserved; eauto. - exact symbols_preserved. exact varinfo_preserved. + exact symbols_preserved. exact public_preserved. exact varinfo_preserved. econstructor; eauto. - (* return *) @@ -1009,7 +1017,7 @@ Proof. intros. apply forward_simulation_step with (match_states := fun s1 s2 => sound_state prog s1 /\ match_states s1 s2). -- exact symbols_preserved. +- exact public_preserved. - simpl; intros. exploit transf_initial_states; eauto. intros [st2 [A B]]. exists st2; intuition. eapply sound_initial; eauto. - simpl; intros. destruct H. eapply transf_final_states; eauto. diff --git a/backend/Inliningproof.v b/backend/Inliningproof.v index 2564a736..9b1aec4c 100644 --- a/backend/Inliningproof.v +++ b/backend/Inliningproof.v @@ -43,6 +43,12 @@ Proof. intros. apply Genv.find_symbol_transf_partial with (transf_fundef fenv); auto. Qed. +Lemma public_preserved: + forall (s: ident), Genv.public_symbol tge s = Genv.public_symbol ge s. +Proof. + intros. apply Genv.public_symbol_transf_partial with (transf_fundef fenv); auto. +Qed. + Lemma varinfo_preserved: forall b, Genv.find_var_info tge b = Genv.find_var_info ge b. Proof. @@ -1008,7 +1014,7 @@ Proof. left; econstructor; split. eapply plus_one. eapply exec_Ibuiltin; eauto. eapply external_call_symbols_preserved; eauto. - exact symbols_preserved. exact varinfo_preserved. + exact symbols_preserved. exact public_preserved. exact varinfo_preserved. econstructor. eapply match_stacks_inside_set_reg. eapply match_stacks_inside_extcall with (F1 := F) (F2 := F1) (m1 := m) (m1' := m'0); eauto. @@ -1161,7 +1167,7 @@ Proof. left; econstructor; split. eapply plus_one. eapply exec_function_external; eauto. eapply external_call_symbols_preserved; eauto. - exact symbols_preserved. exact varinfo_preserved. + exact symbols_preserved. exact public_preserved. exact varinfo_preserved. econstructor. eapply match_stacks_bound with (Mem.nextblock m'0). eapply match_stacks_extcall with (F1 := F) (F2 := F1) (m1 := m) (m1' := m'0); eauto. @@ -1250,7 +1256,7 @@ Theorem transf_program_correct: forward_simulation (semantics prog) (semantics tprog). Proof. eapply forward_simulation_star. - eexact symbols_preserved. + eexact public_preserved. eexact transf_initial_states. eexact transf_final_states. eexact step_simulation. diff --git a/backend/Linearizeproof.v b/backend/Linearizeproof.v index 3b22fc68..63fa6565 100644 --- a/backend/Linearizeproof.v +++ b/backend/Linearizeproof.v @@ -62,6 +62,11 @@ Lemma symbols_preserved: Genv.find_symbol tge id = Genv.find_symbol ge id. Proof (Genv.find_symbol_transf_partial transf_fundef _ TRANSF). +Lemma public_preserved: + forall id, + Genv.public_symbol tge id = Genv.public_symbol ge id. +Proof (Genv.public_symbol_transf_partial transf_fundef _ TRANSF). + Lemma varinfo_preserved: forall b, Genv.find_var_info tge b = Genv.find_var_info ge b. Proof (Genv.find_var_info_transf_partial transf_fundef _ TRANSF). @@ -640,14 +645,14 @@ Proof. left; econstructor; split. simpl. apply plus_one. eapply exec_Lbuiltin; eauto. eapply external_call_symbols_preserved'; eauto. - exact symbols_preserved. exact varinfo_preserved. + exact symbols_preserved. exact public_preserved. exact varinfo_preserved. econstructor; eauto. (* Lannot *) left; econstructor; split. simpl. apply plus_one. eapply exec_Lannot; eauto. eapply external_call_symbols_preserved'; eauto. - exact symbols_preserved. exact varinfo_preserved. + exact symbols_preserved. exact public_preserved. exact varinfo_preserved. econstructor; eauto. (* Lbranch *) @@ -705,7 +710,7 @@ Proof. monadInv H8. left; econstructor; split. apply plus_one. eapply exec_function_external; eauto. eapply external_call_symbols_preserved'; eauto. - exact symbols_preserved. exact varinfo_preserved. + exact symbols_preserved. exact public_preserved. exact varinfo_preserved. econstructor; eauto. (* return *) @@ -741,7 +746,7 @@ Theorem transf_program_correct: forward_simulation (LTL.semantics prog) (Linear.semantics tprog). Proof. eapply forward_simulation_star. - eexact symbols_preserved. + eexact public_preserved. eexact transf_initial_states. eexact transf_final_states. eexact transf_step_correct. diff --git a/backend/NeedDomain.v b/backend/NeedDomain.v index 73b6831a..8beff265 100644 --- a/backend/NeedDomain.v +++ b/backend/NeedDomain.v @@ -862,12 +862,12 @@ Proof. destruct H0. inv H0; constructor; auto with na. inv H0; constructor; auto with na. inv H8; constructor; auto with na. } - exploit (@eval_operation_inj _ _ ge inject_id). - intros. apply val_inject_lessdef. auto. + exploit (@eval_operation_inj _ _ _ _ ge ge inject_id). eassumption. auto. auto. auto. + instantiate (1 := op). intros. apply val_inject_lessdef; auto. apply val_inject_lessdef. instantiate (1 := Vptr sp Int.zero). instantiate (1 := Vptr sp Int.zero). auto. - apply val_list_inject_lessdef. eauto. - eauto. + apply val_list_inject_lessdef; eauto. + eauto. intros (v2 & A & B). exists v2; split; auto. apply vagree_lessdef. apply val_inject_lessdef. auto. Qed. diff --git a/backend/RTLgenproof.v b/backend/RTLgenproof.v index 2aa5ab92..8acce510 100644 --- a/backend/RTLgenproof.v +++ b/backend/RTLgenproof.v @@ -361,6 +361,11 @@ Lemma symbols_preserved: Proof (Genv.find_symbol_transf_partial transl_fundef _ TRANSL). +Lemma public_preserved: + forall (s: ident), Genv.public_symbol tge s = Genv.public_symbol ge s. +Proof + (Genv.public_symbol_transf_partial transl_fundef _ TRANSL). + Lemma function_ptr_translated: forall (b: block) (f: CminorSel.fundef), Genv.find_funct_ptr ge b = Some f -> @@ -687,7 +692,8 @@ Proof. (* Exec *) split. eapply star_right. eexact EX1. eapply exec_Ibuiltin; eauto. - eapply external_call_symbols_preserved; eauto. exact symbols_preserved. exact varinfo_preserved. + eapply external_call_symbols_preserved; eauto. + exact symbols_preserved. exact public_preserved. exact varinfo_preserved. reflexivity. (* Match-env *) split. eauto with rtlg. @@ -720,7 +726,8 @@ Proof. eapply star_left. eapply exec_Icall; eauto. simpl. rewrite symbols_preserved. rewrite H. eauto. auto. eapply star_left. eapply exec_function_external. - eapply external_call_symbols_preserved; eauto. exact symbols_preserved. exact varinfo_preserved. + eapply external_call_symbols_preserved; eauto. + exact symbols_preserved. exact public_preserved. exact varinfo_preserved. apply star_one. apply exec_return. reflexivity. reflexivity. reflexivity. (* Match-env *) @@ -1292,7 +1299,7 @@ Proof. left. eapply plus_right. eexact E. eapply exec_Ibuiltin. eauto. eapply external_call_symbols_preserved. eauto. - exact symbols_preserved. exact varinfo_preserved. + exact symbols_preserved. exact public_preserved. exact varinfo_preserved. traceEq. econstructor; eauto. constructor. eapply match_env_update_dest; eauto. @@ -1410,7 +1417,7 @@ Proof. econstructor; split. left; apply plus_one. eapply exec_function_external; eauto. eapply external_call_symbols_preserved. eauto. - exact symbols_preserved. exact varinfo_preserved. + exact symbols_preserved. exact public_preserved. exact varinfo_preserved. constructor; auto. (* return *) @@ -1448,7 +1455,7 @@ Theorem transf_program_correct: forward_simulation (CminorSel.semantics prog) (RTL.semantics tprog). Proof. eapply forward_simulation_star_wf with (order := lt_state). - eexact symbols_preserved. + eexact public_preserved. eexact transl_initial_states. eexact transl_final_states. apply lt_state_wf. diff --git a/backend/Renumberproof.v b/backend/Renumberproof.v index f18d3c2e..19c3b680 100644 --- a/backend/Renumberproof.v +++ b/backend/Renumberproof.v @@ -47,6 +47,11 @@ Lemma symbols_preserved: Genv.find_symbol tge id = Genv.find_symbol ge id. Proof (@Genv.find_symbol_transf _ _ _ transf_fundef prog). +Lemma public_preserved: + forall id, + Genv.public_symbol tge id = Genv.public_symbol ge id. +Proof (@Genv.public_symbol_transf _ _ _ transf_fundef prog). + Lemma varinfo_preserved: forall b, Genv.find_var_info tge b = Genv.find_var_info ge b. Proof (@Genv.find_var_info_transf _ _ _ transf_fundef prog). @@ -194,7 +199,7 @@ Proof. econstructor; split. eapply exec_Ibuiltin; eauto. eapply external_call_symbols_preserved; eauto. - exact symbols_preserved. exact varinfo_preserved. + exact symbols_preserved. exact public_preserved. exact varinfo_preserved. constructor; auto. eapply reach_succ; eauto. simpl; auto. (* cond *) econstructor; split. @@ -219,7 +224,7 @@ Proof. econstructor; split. eapply exec_function_external; eauto. eapply external_call_symbols_preserved; eauto. - exact symbols_preserved. exact varinfo_preserved. + exact symbols_preserved. exact public_preserved. exact varinfo_preserved. constructor; auto. (* return *) inv STACKS. inv H1. @@ -251,7 +256,7 @@ Theorem transf_program_correct: forward_simulation (RTL.semantics prog) (RTL.semantics tprog). Proof. eapply forward_simulation_step. - eexact symbols_preserved. + eexact public_preserved. eexact transf_initial_states. eexact transf_final_states. exact step_simulation. diff --git a/backend/Selectionproof.v b/backend/Selectionproof.v index 658e6603..672853e3 100644 --- a/backend/Selectionproof.v +++ b/backend/Selectionproof.v @@ -56,6 +56,12 @@ Proof. intros. eapply Genv.find_symbol_transf_partial; eauto. Qed. +Lemma public_preserved: + forall (s: ident), Genv.public_symbol tge s = Genv.public_symbol ge s. +Proof. + intros. eapply Genv.public_symbol_transf_partial; eauto. +Qed. + Lemma function_ptr_translated: forall (b: block) (f: Cminor.fundef), Genv.find_funct_ptr ge b = Some f -> @@ -105,7 +111,7 @@ Proof. split. auto. split. auto. intros. eapply external_call_symbols_preserved; eauto. - exact symbols_preserved. exact varinfo_preserved. + exact symbols_preserved. exact public_preserved. exact varinfo_preserved. Qed. Lemma builtin_implements_preserved: @@ -115,7 +121,7 @@ Lemma builtin_implements_preserved: Proof. unfold builtin_implements; intros. eapply external_call_symbols_preserved; eauto. - exact symbols_preserved. exact varinfo_preserved. + exact symbols_preserved. exact public_preserved. exact varinfo_preserved. Qed. Lemma helpers_correct_preserved: @@ -795,7 +801,7 @@ Proof. intros [vres' [m2 [A [B [C D]]]]]. left; econstructor; split. econstructor. eauto. eapply external_call_symbols_preserved; eauto. - exact symbols_preserved. exact varinfo_preserved. + exact symbols_preserved. exact public_preserved. exact varinfo_preserved. constructor; auto. destruct optid; simpl; auto. apply set_var_lessdef; auto. - (* Seq *) @@ -872,14 +878,14 @@ Proof. intros [vres' [m2 [A [B [C D]]]]]. left; econstructor; split. econstructor. eapply external_call_symbols_preserved; eauto. - exact symbols_preserved. exact varinfo_preserved. + exact symbols_preserved. exact public_preserved. exact varinfo_preserved. constructor; auto. - (* external call turned into a Sbuiltin *) exploit external_call_mem_extends; eauto. intros [vres' [m2 [A [B [C D]]]]]. left; econstructor; split. econstructor. eauto. eapply external_call_symbols_preserved; eauto. - exact symbols_preserved. exact varinfo_preserved. + exact symbols_preserved. exact public_preserved. exact varinfo_preserved. constructor; auto. - (* return *) inv MC. @@ -927,7 +933,7 @@ Proof. intros. unfold sel_program in H. destruct (get_helpers (Genv.globalenv prog)) as [hf|] eqn:E; simpl in H; try discriminate. apply forward_simulation_opt with (match_states := match_states prog tprog hf) (measure := measure). - eapply symbols_preserved; eauto. + eapply public_preserved; eauto. apply sel_initial_states; auto. apply sel_final_states; auto. apply sel_step_correct; auto. eapply helpers_correct_preserved; eauto. apply get_helpers_correct. auto. diff --git a/backend/Stackingproof.v b/backend/Stackingproof.v index c25721bc..e3e3a0d0 100644 --- a/backend/Stackingproof.v +++ b/backend/Stackingproof.v @@ -2242,6 +2242,14 @@ Proof. exact TRANSF. Qed. +Lemma public_preserved: + forall id, Genv.public_symbol tge id = Genv.public_symbol ge id. +Proof. + intros. unfold ge, tge. + apply Genv.public_symbol_transf_partial with transf_fundef. + exact TRANSF. +Qed. + Lemma varinfo_preserved: forall b, Genv.find_var_info tge b = Genv.find_var_info ge b. Proof. @@ -2681,7 +2689,7 @@ Proof. econstructor; split. apply plus_one. econstructor; eauto. eapply external_call_symbols_preserved'; eauto. - exact symbols_preserved. exact varinfo_preserved. + exact symbols_preserved. exact public_preserved. exact varinfo_preserved. econstructor; eauto with coqlib. inversion H; inversion A; subst. eapply match_stack_change_extcall; eauto. @@ -2705,7 +2713,7 @@ Proof. econstructor; split. apply plus_one. econstructor; eauto. eapply external_call_symbols_preserved'; eauto. - exact symbols_preserved. exact varinfo_preserved. + exact symbols_preserved. exact public_preserved. exact varinfo_preserved. econstructor; eauto with coqlib. inv H; inv A. eapply match_stack_change_extcall; eauto. apply Plt_Ple. change (Mem.valid_block m sp0). eapply agree_valid_linear; eauto. @@ -2813,7 +2821,7 @@ Proof. econstructor; split. apply plus_one. eapply exec_function_external; eauto. eapply external_call_symbols_preserved'; eauto. - exact symbols_preserved. exact varinfo_preserved. + exact symbols_preserved. exact public_preserved. exact varinfo_preserved. econstructor; eauto. apply match_stacks_change_bounds with (Mem.nextblock m) (Mem.nextblock m'0). inv H0; inv A. eapply match_stack_change_extcall; eauto. apply Ple_refl. apply Ple_refl. @@ -2879,7 +2887,7 @@ Theorem transf_program_correct: Proof. set (ms := fun s s' => wt_state s /\ match_states s s'). eapply forward_simulation_plus with (match_states := ms). -- exact symbols_preserved. +- exact public_preserved. - intros. exploit transf_initial_states; eauto. intros [st2 [A B]]. exists st2; split; auto. split; auto. apply wt_initial_state with (prog := prog); auto. exact wt_prog. diff --git a/backend/Tailcallproof.v b/backend/Tailcallproof.v index cc4ff55e..5ee7ccc1 100644 --- a/backend/Tailcallproof.v +++ b/backend/Tailcallproof.v @@ -241,6 +241,10 @@ Lemma symbols_preserved: forall (s: ident), Genv.find_symbol tge s = Genv.find_symbol ge s. Proof (Genv.find_symbol_transf transf_fundef prog). +Lemma public_preserved: + forall (s: ident), Genv.public_symbol tge s = Genv.public_symbol ge s. +Proof (Genv.public_symbol_transf transf_fundef prog). + Lemma varinfo_preserved: forall b, Genv.find_var_info tge b = Genv.find_var_info ge b. Proof (Genv.find_var_info_transf transf_fundef prog). @@ -506,7 +510,7 @@ Proof. left. exists (State s' (transf_function f) (Vptr sp0 Int.zero) pc' (rs'#res <- v') m'1); split. eapply exec_Ibuiltin; eauto. eapply external_call_symbols_preserved; eauto. - exact symbols_preserved. exact varinfo_preserved. + exact symbols_preserved. exact public_preserved. exact varinfo_preserved. econstructor; eauto. apply regset_set; auto. (* cond *) @@ -567,7 +571,7 @@ Proof. left. exists (Returnstate s' res' m2'); split. simpl. econstructor; eauto. eapply external_call_symbols_preserved; eauto. - exact symbols_preserved. exact varinfo_preserved. + exact symbols_preserved. exact public_preserved. exact varinfo_preserved. constructor; auto. (* returnstate *) @@ -616,7 +620,7 @@ Theorem transf_program_correct: forward_simulation (RTL.semantics prog) (RTL.semantics tprog). Proof. eapply forward_simulation_opt with (measure := measure); eauto. - eexact symbols_preserved. + eexact public_preserved. eexact transf_initial_states. eexact transf_final_states. exact transf_step_correct. diff --git a/backend/Tunnelingproof.v b/backend/Tunnelingproof.v index d02cb2e1..e6588938 100644 --- a/backend/Tunnelingproof.v +++ b/backend/Tunnelingproof.v @@ -160,6 +160,11 @@ Lemma symbols_preserved: Genv.find_symbol tge id = Genv.find_symbol ge id. Proof (@Genv.find_symbol_transf _ _ _ tunnel_fundef prog). +Lemma public_preserved: + forall id, + Genv.public_symbol tge id = Genv.public_symbol ge id. +Proof (@Genv.public_symbol_transf _ _ _ tunnel_fundef prog). + Lemma varinfo_preserved: forall b, Genv.find_var_info tge b = Genv.find_var_info ge b. Proof (@Genv.find_var_info_transf _ _ _ tunnel_fundef prog). @@ -335,13 +340,13 @@ Proof. left; simpl; econstructor; split. eapply exec_Lbuiltin; eauto. eapply external_call_symbols_preserved'; eauto. - exact symbols_preserved. exact varinfo_preserved. + exact symbols_preserved. exact public_preserved. exact varinfo_preserved. econstructor; eauto. (* Lannot *) left; simpl; econstructor; split. eapply exec_Lannot; eauto. eapply external_call_symbols_preserved'; eauto. - exact symbols_preserved. exact varinfo_preserved. + exact symbols_preserved. exact public_preserved. exact varinfo_preserved. econstructor; eauto. (* Lbranch (preserved) *) @@ -373,7 +378,7 @@ Proof. left; simpl; econstructor; split. eapply exec_function_external; eauto. eapply external_call_symbols_preserved'; eauto. - exact symbols_preserved. exact varinfo_preserved. + exact symbols_preserved. exact public_preserved. exact varinfo_preserved. simpl. econstructor; eauto. (* return *) inv H3. inv H1. @@ -408,7 +413,7 @@ Theorem transf_program_correct: forward_simulation (LTL.semantics prog) (LTL.semantics tprog). Proof. eapply forward_simulation_opt. - eexact symbols_preserved. + eexact public_preserved. eexact transf_initial_states. eexact transf_final_states. eexact tunnel_step_correct. diff --git a/backend/Unusedglob.ml b/backend/Unusedglob.ml deleted file mode 100644 index 1a88ee96..00000000 --- a/backend/Unusedglob.ml +++ /dev/null @@ -1,90 +0,0 @@ -(* *********************************************************************) -(* *) -(* The Compcert verified compiler *) -(* *) -(* Xavier Leroy, INRIA Paris-Rocquencourt *) -(* *) -(* Copyright Institut National de Recherche en Informatique et en *) -(* Automatique. All rights reserved. This file is distributed *) -(* under the terms of the INRIA Non-Commercial License Agreement. *) -(* *) -(* *********************************************************************) - -(* Removing unused definitions of static functions and global variables *) - -open Camlcoq -open Maps -open AST -open Asm -open Unusedglob1 - -module IdentSet = Set.Make(struct type t = ident let compare = compare end) - -(* The set of globals referenced from a function definition *) - -let add_referenced_instr rf i = - List.fold_right IdentSet.add (referenced_instr i) rf - -let referenced_function f = - List.fold_left add_referenced_instr IdentSet.empty (code_of_function f) - -(* The set of globals referenced from a variable definition (initialization) *) - -let add_referenced_init_data rf = function - | Init_addrof(id, ofs) -> IdentSet.add id rf - | _ -> rf - -let referenced_globvar gv = - List.fold_left add_referenced_init_data IdentSet.empty gv.gvar_init - -(* The map global |-> set of globals it references *) - -let referenced_globdef gd = - match gd with - | Gfun(Internal f) -> referenced_function f - | Gfun(External ef) -> IdentSet.empty - | Gvar gv -> referenced_globvar gv - -let use_map p = - List.fold_left (fun m (id, gd) -> PTree.set id (referenced_globdef gd) m) - PTree.empty p.prog_defs - -(* Worklist algorithm computing the set of used globals *) - -let rec used_idents usemap used wrk = - match wrk with - | [] -> used - | id :: wrk -> - if IdentSet.mem id used then used_idents usemap used wrk else - match PTree.get id usemap with - | None -> used_idents usemap used wrk - | Some s -> used_idents usemap (IdentSet.add id used) - (IdentSet.fold (fun id l -> id::l) s wrk) - -(* The worklist is initially populated with all nonstatic globals *) - -let add_nonstatic wrk id = - if C2C.atom_is_static id then wrk else id :: wrk - -let initial_worklist p = - List.fold_left (fun wrk (id, gd) -> add_nonstatic wrk id) - [] p.prog_defs - -(* Eliminate unused definitions *) - -let rec filter used = function - | [] -> [] - | (id, def) :: rem -> - if IdentSet.mem id used - then (id, def) :: filter used rem - else filter used rem - -let filter_prog used p = - { prog_defs = filter used p.prog_defs; - prog_main = p.prog_main } - -(* Entry point *) - -let transf_program p = - filter_prog (used_idents (use_map p) IdentSet.empty (initial_worklist p)) p - diff --git a/backend/Unusedglob.v b/backend/Unusedglob.v new file mode 100644 index 00000000..55a093a4 --- /dev/null +++ b/backend/Unusedglob.v @@ -0,0 +1,141 @@ +(* *********************************************************************) +(* *) +(* The Compcert verified compiler *) +(* *) +(* Xavier Leroy, INRIA Paris-Rocquencourt *) +(* *) +(* Copyright Institut National de Recherche en Informatique et en *) +(* Automatique. All rights reserved. This file is distributed *) +(* under the terms of the INRIA Non-Commercial License Agreement. *) +(* *) +(* *********************************************************************) + +(** Elimination of unreferenced static definitions *) + +Require Import FSets. +Require Import Coqlib. +Require Import Ordered. +Require Import Maps. +Require Import Iteration. +Require Import AST. +Require Import Errors. +Require Import Op. +Require Import Registers. +Require Import RTL. + +Local Open Scope string_scope. + +(** * Determination of global identifiers that are referenced *) + +(** The working set *) + +Module IS := FSetAVL.Make(OrderedPositive). + +Record workset := mk_workset { + w_seen :> IS.t; + w_todo: list ident +}. + +Definition add_workset (id: ident) (w: workset) : workset := + if IS.mem id w.(w_seen) + then w + else {| w_seen := IS.add id w.(w_seen); w_todo := id :: w.(w_todo) |}. + +Fixpoint addlist_workset (l: list ident) (w: workset) : workset := + match l with + | nil => w + | id :: l' => addlist_workset l' (add_workset id w) + end. + +(** Global symbols referenced in a function or variable definition *) + +Definition ref_instruction (i: instruction) : list ident := + match i with + | Inop _ => nil + | Iop op _ _ _ => globals_operation op + | Iload _ addr _ _ _ => globals_addressing addr + | Istore _ addr _ _ _ => globals_addressing addr + | Icall _ (inl r) _ _ _ => nil + | Icall _ (inr id) _ _ _ => id :: nil + | Itailcall _ (inl r) _ => nil + | Itailcall _ (inr id) _ => id :: nil + | Ibuiltin ef _ _ _ => globals_external ef + | Icond cond _ _ _ => nil + | Ijumptable _ _ => nil + | Ireturn _ => nil + end. + +Definition add_ref_instruction (w: workset) (pc: node) (i: instruction) : workset := + addlist_workset (ref_instruction i) w. + +Definition add_ref_function (f: function) (w: workset): workset := + PTree.fold add_ref_instruction f.(fn_code) w. + +Definition add_ref_init_data (w: workset) (i: init_data) : workset := + match i with + | Init_addrof id _ => add_workset id w + | _ => w + end. + +Definition add_ref_globvar (gv: globvar unit) (w: workset): workset := + List.fold_left add_ref_init_data gv.(gvar_init) w. + +Definition prog_map : Type := PTree.t (globdef fundef unit). + +Definition add_ref_definition (pm: prog_map) (id: ident) (w: workset): workset := + match pm!id with + | None => w + | Some (Gfun (Internal f)) => add_ref_function f w + | Some (Gfun (External ef)) => addlist_workset (globals_external ef) w + | Some (Gvar gv) => add_ref_globvar gv w + end. + +(** Traversal of the dependency graph. *) + +Definition iter_step (pm: prog_map) (w: workset) : IS.t + workset := + match w.(w_todo) with + | nil => + inl _ w.(w_seen) + | id :: rem => + inr _ (add_ref_definition pm id {| w_seen := w.(w_seen); w_todo := rem |}) + end. + +Definition initial_workset (p: program): workset := + add_workset p.(prog_main) + (List.fold_left (fun w id => add_workset id w) + p.(prog_public) + {| w_seen := IS.empty; w_todo := nil |}). + +Definition add_def_prog_map (pm: prog_map) (id_df: ident * globdef fundef unit) : prog_map := + PTree.set (fst id_df) (snd id_df) pm. + +Definition program_map (p: program) : prog_map := + List.fold_left add_def_prog_map p.(prog_defs) (PTree.empty _). + +Definition used_globals (p: program) : option IS.t := + let pm := program_map p in + PrimIter.iterate _ _ (iter_step pm) (initial_workset p). + +(** * Elimination of unreferenced global definitions *) + +(** We also eliminate multiple definitions of the same global name, keeping ony + the last definition (in program definition order). *) + +Fixpoint filter_globdefs (used: IS.t) (accu defs: list (ident * globdef fundef unit)) := + match defs with + | nil => accu + | (id, gd) :: defs' => + if IS.mem id used + then filter_globdefs (IS.remove id used) ((id, gd) :: accu) defs' + else filter_globdefs used accu defs' + end. + +Definition transform_program (p: program) : res program := + match used_globals p with + | None => Error (msg "Unusedglob: analysis failed") + | Some used => + OK {| prog_defs := filter_globdefs used nil (List.rev p.(prog_defs)); + prog_public := p.(prog_public); + prog_main := p.(prog_main) |} + end. + diff --git a/backend/Unusedglobproof.v b/backend/Unusedglobproof.v new file mode 100644 index 00000000..5be9344f --- /dev/null +++ b/backend/Unusedglobproof.v @@ -0,0 +1,1256 @@ +(* *********************************************************************) +(* *) +(* The Compcert verified compiler *) +(* *) +(* Xavier Leroy, INRIA Paris-Rocquencourt *) +(* *) +(* Copyright Institut National de Recherche en Informatique et en *) +(* Automatique. All rights reserved. This file is distributed *) +(* under the terms of the INRIA Non-Commercial License Agreement. *) +(* *) +(* *********************************************************************) + +(** Elimination of unreferenced static definitions *) + +Require Import FSets. +Require Import Coqlib. +Require Import Ordered. +Require Import Maps. +Require Import Iteration. +Require Import AST. +Require Import Errors. +Require Import Integers. +Require Import Values. +Require Import Memory. +Require Import Globalenvs. +Require Import Events. +Require Import Smallstep. +Require Import Op. +Require Import Registers. +Require Import RTL. +Require Import Unusedglob. + +Module ISF := FSetFacts.Facts(IS). +Module ISP := FSetProperties.Properties(IS). + +(** * Properties of the analysis *) + +(** Monotonic evolution of the workset. *) + +Inductive workset_incl (w1 w2: workset) : Prop := + workset_incl_intro: + forall (SEEN: IS.Subset w1.(w_seen) w2.(w_seen)) + (TODO: List.incl w1.(w_todo) w2.(w_todo)) + (TRACK: forall id, IS.In id w2.(w_seen) -> + IS.In id w1.(w_seen) \/ List.In id w2.(w_todo)), + workset_incl w1 w2. + +Lemma seen_workset_incl: + forall w1 w2 id, workset_incl w1 w2 -> IS.In id w1 -> IS.In id w2. +Proof. + intros. destruct H. auto. +Qed. + +Lemma workset_incl_refl: forall w, workset_incl w w. +Proof. + intros; split. red; auto. red; auto. auto. +Qed. + +Lemma workset_incl_trans: + forall w1 w2 w3, workset_incl w1 w2 -> workset_incl w2 w3 -> workset_incl w1 w3. +Proof. + intros. destruct H, H0; split. + red; eauto. + red; eauto. + intros. edestruct TRACK0; eauto. edestruct TRACK; eauto. +Qed. + +Lemma add_workset_incl: + forall id w, workset_incl w (add_workset id w). +Proof. + unfold add_workset; intros. destruct (IS.mem id w) eqn:MEM. +- apply workset_incl_refl. +- split; simpl. + + red; intros. apply IS.add_2; auto. + + red; simpl; auto. + + intros. destruct (ident_eq id id0); auto. apply IS.add_3 in H; auto. +Qed. + +Lemma addlist_workset_incl: + forall l w, workset_incl w (addlist_workset l w). +Proof. + induction l; simpl; intros. + apply workset_incl_refl. + eapply workset_incl_trans. apply add_workset_incl. eauto. +Qed. + +Lemma add_ref_function_incl: + forall f w, workset_incl w (add_ref_function f w). +Proof. + unfold add_ref_function; intros. apply PTree_Properties.fold_rec. +- auto. +- apply workset_incl_refl. +- intros. apply workset_incl_trans with a; auto. + unfold add_ref_instruction. apply addlist_workset_incl. +Qed. + +Lemma add_ref_globvar_incl: + forall gv w, workset_incl w (add_ref_globvar gv w). +Proof. + unfold add_ref_globvar; intros. + revert w. induction (gvar_init gv); simpl; intros. + apply workset_incl_refl. + eapply workset_incl_trans; [ | eauto ]. + unfold add_ref_init_data. + destruct a; (apply workset_incl_refl || apply add_workset_incl). +Qed. + +Lemma add_ref_definition_incl: + forall pm id w, workset_incl w (add_ref_definition pm id w). +Proof. + unfold add_ref_definition; intros. + destruct (pm!id) as [[[] | ? ] | ]. + apply add_ref_function_incl. + apply addlist_workset_incl. + apply add_ref_globvar_incl. + apply workset_incl_refl. +Qed. + +Lemma initial_workset_incl: + forall p, workset_incl {| w_seen := IS.empty; w_todo := nil |} (initial_workset p). +Proof. + unfold initial_workset; intros. + eapply workset_incl_trans. 2: apply add_workset_incl. + generalize {| w_seen := IS.empty; w_todo := nil |}. induction (prog_public p); simpl; intros. + apply workset_incl_refl. + eapply workset_incl_trans. eapply add_workset_incl. eapply IHl. +Qed. + +(** Soundness properties for functions that add identifiers to the workset *) + +Lemma seen_add_workset: + forall id (w: workset), IS.In id (add_workset id w). +Proof. + unfold add_workset; intros. + destruct (IS.mem id w) eqn:MEM. + apply IS.mem_2; auto. + simpl. apply IS.add_1; auto. +Qed. + +Lemma seen_addlist_workset: + forall id l (w: workset), + In id l -> IS.In id (addlist_workset l w). +Proof. + induction l; simpl; intros. + tauto. + destruct H. subst a. + eapply seen_workset_incl. apply addlist_workset_incl. apply seen_add_workset. + apply IHl; auto. +Qed. + +Definition ref_function (f: function) (id: ident) : Prop := + exists pc i, f.(fn_code)!pc = Some i /\ In id (ref_instruction i). + +Lemma seen_add_ref_function: + forall id f w, + ref_function f id -> IS.In id (add_ref_function f w). +Proof. + intros until w. unfold ref_function, add_ref_function. apply PTree_Properties.fold_rec; intros. +- destruct H1 as (pc & i & A & B). apply H0; auto. exists pc, i; split; auto. rewrite H; auto. +- destruct H as (pc & i & A & B). rewrite PTree.gempty in A; discriminate. +- destruct H2 as (pc & i & A & B). rewrite PTree.gsspec in A. destruct (peq pc k). + + inv A. unfold add_ref_instruction. apply seen_addlist_workset; auto. + + unfold add_ref_instruction. eapply seen_workset_incl. apply addlist_workset_incl. + apply H1. exists pc, i; auto. +Qed. + +Definition ref_fundef (fd: fundef) (id: ident) : Prop := + match fd with Internal f => ref_function f id | External ef => In id (globals_external ef) end. + +Definition ref_def (gd: globdef fundef unit) (id: ident) : Prop := + match gd with + | Gfun fd => ref_fundef fd id + | Gvar gv => exists ofs, List.In (Init_addrof id ofs) gv.(gvar_init) + end. + +Lemma seen_add_ref_definition: + forall pm id gd id' w, + pm!id = Some gd -> ref_def gd id' -> IS.In id' (add_ref_definition pm id w). +Proof. + unfold add_ref_definition; intros. rewrite H. red in H0; destruct gd as [[f|ef]|gv]. + apply seen_add_ref_function; auto. + apply seen_addlist_workset; auto. + destruct H0 as (ofs & IN). + unfold add_ref_globvar. + assert (forall l (w: workset), + IS.In id' w \/ In (Init_addrof id' ofs) l -> + IS.In id' (fold_left add_ref_init_data l w)). + { + induction l; simpl; intros. + tauto. + apply IHl. intuition auto. + left. destruct a; simpl; auto. eapply seen_workset_incl. apply add_workset_incl. auto. + subst; left; simpl. apply seen_add_workset. + } + apply H0; auto. +Qed. + +Lemma seen_main_initial_workset: + forall p, IS.In p.(prog_main) (initial_workset p). +Proof. + unfold initial_workset; intros. apply seen_add_workset. +Qed. + +Lemma seen_public_initial_workset: + forall p id, In id p.(prog_public) -> IS.In id (initial_workset p). +Proof. + intros. unfold initial_workset. eapply seen_workset_incl. apply add_workset_incl. + assert (forall l (w: workset), + IS.In id w \/ In id l -> IS.In id (fold_left (fun w id => add_workset id w) l w)). + { + induction l; simpl; intros. + tauto. + apply IHl. intuition auto; left. + eapply seen_workset_incl. apply add_workset_incl. auto. + subst a. apply seen_add_workset. + } + apply H0. auto. +Qed. + +(** * Semantic preservation *) + +Section SOUNDNESS. +Variable p: program. +Variable tp: program. +Hypothesis TRANSF: transform_program p = OK tp. +Let ge := Genv.globalenv p. +Let tge := Genv.globalenv tp. + +Let pm := program_map p. + + +(** Correctness of the dependency graph traversal. *) + +Definition workset_invariant (w: workset) : Prop := + forall id gd id', + IS.In id w -> ~List.In id (w_todo w) -> pm!id = Some gd -> ref_def gd id' -> + IS.In id' w. + +Definition used_set_closed (u: IS.t) : Prop := + forall id gd id', + IS.In id u -> pm!id = Some gd -> ref_def gd id' -> IS.In id' u. + +Lemma iter_step_invariant: + forall w, + workset_invariant w -> + match iter_step pm w with + | inl u => used_set_closed u + | inr w' => workset_invariant w' + end. +Proof. + unfold iter_step, workset_invariant, used_set_closed; intros. + destruct (w_todo w) as [ | id rem ]; intros. +- eapply H; eauto. +- set (w' := {| w_seen := w.(w_seen); w_todo := rem |}) in *. + destruct (add_ref_definition_incl pm id w'). + destruct (ident_eq id id0). + + subst id0. eapply seen_add_ref_definition; eauto. + + exploit TRACK; eauto. intros [A|A]. + * apply SEEN. eapply H; eauto. simpl. + assert (~ In id0 rem). + { change rem with (w_todo w'). red; intros. elim H1; auto. } + tauto. + * contradiction. +Qed. + +Theorem used_globals_sound: + forall u, used_globals p = Some u -> used_set_closed u. +Proof. + unfold used_globals; intros. eapply PrimIter.iterate_prop with (P := workset_invariant); eauto. +- intros. apply iter_step_invariant; auto. +- destruct (initial_workset_incl p). + red; intros. edestruct TRACK; eauto. + simpl in H4. eelim IS.empty_1; eauto. + contradiction. +Qed. + +Theorem used_globals_incl: + forall u, used_globals p = Some u -> IS.Subset (initial_workset p) u. +Proof. + unfold used_globals; intros. + eapply PrimIter.iterate_prop with (P := fun (w: workset) => IS.Subset (initial_workset p) w); eauto. +- fold pm; unfold iter_step; intros. destruct (w_todo a) as [ | id rem ]. + auto. + destruct (add_ref_definition_incl pm id {| w_seen := a; w_todo := rem |}). + red; auto. +- red; auto. +Qed. + +Definition used: IS.t := + match used_globals p with Some u => u | None => IS.empty end. + +Remark USED_GLOBALS: used_globals p = Some used. +Proof. + unfold used. unfold transform_program in TRANSF. destruct (used_globals p). auto. discriminate. +Qed. + +Definition kept (id: ident) : Prop := IS.In id used. + +Theorem kept_closed: + forall id gd id', + kept id -> pm!id = Some gd -> ref_def gd id' -> kept id'. +Proof. + intros. assert (UC: used_set_closed used) by (apply used_globals_sound; apply USED_GLOBALS). + eapply UC; eauto. +Qed. + +Theorem kept_main: + kept p.(prog_main). +Proof. + unfold kept. eapply used_globals_incl; eauto. apply USED_GLOBALS. apply seen_main_initial_workset. +Qed. + +Theorem kept_public: + forall id, In id p.(prog_public) -> kept id. +Proof. + intros. unfold kept. eapply used_globals_incl; eauto. apply USED_GLOBALS. apply seen_public_initial_workset; auto. +Qed. + +Remark filter_globdefs_accu: + forall defs accu1 accu2 u, + filter_globdefs u (accu1 ++ accu2) defs = filter_globdefs u accu1 defs ++ accu2. +Proof. + induction defs; simpl; intros. + auto. + destruct a as [id gd]. destruct (IS.mem id u); auto. + rewrite <- IHdefs. auto. +Qed. + +Remark filter_globdefs_nil: + forall u accu defs, + filter_globdefs u accu defs = filter_globdefs u nil defs ++ accu. +Proof. + intros. rewrite <- filter_globdefs_accu. auto. +Qed. + +Theorem transform_program_charact: + forall id, (program_map tp)!id = if IS.mem id used then pm!id else None. +Proof. + intros. + assert (X: forall l u m1 m2, + IS.In id u -> + m1!id = m2!id -> + (fold_left add_def_prog_map (filter_globdefs u nil l) m1)!id = + (fold_left add_def_prog_map (List.rev l) m2)!id). + { + induction l; simpl; intros. + auto. + destruct a as [id1 gd1]. rewrite fold_left_app. simpl. + destruct (IS.mem id1 u) eqn:MEM. + rewrite filter_globdefs_nil. rewrite fold_left_app. simpl. + unfold add_def_prog_map at 1 3. simpl. + rewrite ! PTree.gsspec. destruct (peq id id1). auto. + apply IHl; auto. apply IS.remove_2; auto. + unfold add_def_prog_map at 2. simpl. rewrite PTree.gso. apply IHl; auto. + red; intros; subst id1. + assert (IS.mem id u = true) by (apply IS.mem_1; auto). congruence. + } + assert (Y: forall l u m1, + IS.mem id u = false -> + m1!id = None -> + (fold_left add_def_prog_map (filter_globdefs u nil l) m1)!id = None). + { + induction l; simpl; intros. + auto. + destruct a as [id1 gd1]. + destruct (IS.mem id1 u) eqn:MEM. + rewrite filter_globdefs_nil. rewrite fold_left_app. simpl. + unfold add_def_prog_map at 1. simpl. rewrite PTree.gso by congruence. eapply IHl; eauto. + rewrite ISF.remove_b. rewrite H; auto. + eapply IHl; eauto. + } + unfold pm, program_map. + unfold transform_program in TRANSF; rewrite USED_GLOBALS in TRANSF. inversion TRANSF. + simpl. destruct (IS.mem id used) eqn: MEM. + erewrite X. rewrite List.rev_involutive. eauto. apply IS.mem_2; auto. auto. + apply Y. auto. apply PTree.gempty. +Qed. + +(** Program map and Genv operations *) + +Definition genv_progmap_match (ge: genv) (pm: prog_map) : Prop := + forall id, + match Genv.find_symbol ge id with + | None => pm!id = None + | Some b => + match pm!id with + | None => False + | Some (Gfun fd) => Genv.find_funct_ptr ge b = Some fd + | Some (Gvar gv) => Genv.find_var_info ge b = Some gv + end + end. + +Lemma genv_program_map: + forall p, genv_progmap_match (Genv.globalenv p) (program_map p). +Proof. + intros. unfold Genv.globalenv, program_map. + assert (REC: forall defs g m, + genv_progmap_match g m -> + genv_progmap_match (Genv.add_globals g defs) (fold_left add_def_prog_map defs m)). + { + induction defs; simpl; intros. + auto. + apply IHdefs. red; intros. specialize (H id). + destruct a as [id1 [fd|gv]]; + unfold Genv.add_global, Genv.find_symbol, Genv.find_funct_ptr, Genv.find_var_info, add_def_prog_map in *; + simpl. + - rewrite PTree.gsspec. destruct (peq id id1); subst. + + rewrite ! PTree.gss. auto. + + destruct (Genv.genv_symb g)!id as [b|] eqn:S; rewrite PTree.gso by auto. + * rewrite PTree.gso. auto. apply Plt_ne. eapply Genv.genv_symb_range; eauto. + * auto. + - rewrite PTree.gsspec. destruct (peq id id1); subst. + + rewrite ! PTree.gss. auto. + + destruct (Genv.genv_symb g)!id as [b|] eqn:S; rewrite PTree.gso by auto. + * rewrite PTree.gso. auto. apply Plt_ne. eapply Genv.genv_symb_range; eauto. + * auto. + } + apply REC. red; intros. unfold Genv.find_symbol, Genv.empty_genv; simpl. rewrite ! PTree.gempty; auto. +Qed. + +Lemma transform_program_kept: + forall id b, Genv.find_symbol tge id = Some b -> kept id. +Proof. + intros. generalize (genv_program_map tp id). fold tge; rewrite H. + rewrite transform_program_charact. intros. destruct (IS.mem id used) eqn:U. + unfold kept; apply IS.mem_2; auto. + contradiction. +Qed. + +(** Injections that preserve used globals. *) + +Record meminj_preserves_globals (f: meminj) : Prop := { + symbols_inject_1: forall id b b' delta, + f b = Some(b', delta) -> Genv.find_symbol ge id = Some b -> + delta = 0 /\ Genv.find_symbol tge id = Some b'; + symbols_inject_2: forall id b, + kept id -> Genv.find_symbol ge id = Some b -> + exists b', Genv.find_symbol tge id = Some b' /\ f b = Some(b', 0); + symbols_inject_3: forall id b', + Genv.find_symbol tge id = Some b' -> + exists b, Genv.find_symbol ge id = Some b /\ f b = Some(b', 0); + funct_ptr_inject: forall b b' delta fd, + f b = Some(b', delta) -> Genv.find_funct_ptr ge b = Some fd -> + Genv.find_funct_ptr tge b' = Some fd /\ delta = 0 /\ + (forall id, ref_fundef fd id -> kept id); + var_info_inject: forall b b' delta gv, + f b = Some(b', delta) -> Genv.find_var_info ge b = Some gv -> + Genv.find_var_info tge b' = Some gv /\ delta = 0; + var_info_rev_inject: forall b b' delta gv, + f b = Some(b', delta) -> Genv.find_var_info tge b' = Some gv -> + Genv.find_var_info ge b = Some gv /\ delta = 0 +}. + +Definition init_meminj : meminj := + fun b => + match Genv.invert_symbol ge b with + | Some id => + match Genv.find_symbol tge id with + | Some b' => Some (b', 0) + | None => None + end + | None => None + end. + +Remark init_meminj_invert: + forall b b' delta, + init_meminj b = Some(b', delta) -> + delta = 0 /\ exists id, Genv.find_symbol ge id = Some b /\ Genv.find_symbol tge id = Some b'. +Proof. + unfold init_meminj; intros. + destruct (Genv.invert_symbol ge b) as [id|] eqn:S; try discriminate. + destruct (Genv.find_symbol tge id) as [b''|] eqn:F; inv H. + split. auto. exists id. split. apply Genv.invert_find_symbol; auto. auto. +Qed. + +Lemma init_meminj_preserves_globals: + meminj_preserves_globals init_meminj. +Proof. + constructor; intros. +- exploit init_meminj_invert; eauto. intros (A & id1 & B & C). + assert (id1 = id) by (eapply (Genv.genv_vars_inj ge); eauto). subst id1. + auto. +- unfold init_meminj. erewrite Genv.find_invert_symbol by eauto. apply IS.mem_1 in H. + generalize (genv_program_map p id) (genv_program_map tp id). fold ge; fold tge; fold pm. + rewrite transform_program_charact. rewrite H, H0. + destruct (Genv.find_symbol tge id) as [b'|]; intros. + exists b'; auto. rewrite H2 in H1; contradiction. +- generalize (genv_program_map tp id). fold tge. rewrite H. intros. + destruct (program_map tp)!id as [gd|] eqn:PM; try contradiction. + generalize (transform_program_charact id). rewrite PM. + destruct (IS.mem id used) eqn:USED; intros; try discriminate. + generalize (genv_program_map p id). fold ge; fold pm. + destruct (Genv.find_symbol ge id) as [b|] eqn:FS; intros; try congruence. + exists b; split; auto. unfold init_meminj. + erewrite Genv.find_invert_symbol by eauto. rewrite H. auto. +- exploit init_meminj_invert; eauto. intros (A & id & B & C). + generalize (genv_program_map p id) (genv_program_map tp id). fold ge; fold tge; fold pm. + rewrite transform_program_charact. rewrite B, C. intros. + destruct (IS.mem id used) eqn:KEPT; try contradiction. + destruct (pm!id) as [gd|] eqn:PM; try contradiction. + destruct gd as [fd'|gv']. + + assert (fd' = fd) by congruence. subst fd'. split. auto. split. auto. + intros. eapply kept_closed; eauto. red; apply IS.mem_2; auto. + + assert (b <> b) by (eapply Genv.genv_funs_vars; eassumption). congruence. +- exploit init_meminj_invert; eauto. intros (A & id & B & C). split; auto. + generalize (genv_program_map p id) (genv_program_map tp id). fold ge; fold tge; fold pm. + rewrite transform_program_charact. rewrite B, C. intros. + destruct (IS.mem id used); try contradiction. + destruct (pm!id) as [gd|]; try contradiction. + destruct gd as [fd'|gv']. + + assert (b <> b) by (eapply Genv.genv_funs_vars; eassumption). congruence. + + congruence. +- exploit init_meminj_invert; eauto. intros (A & id & B & C). split; auto. + generalize (genv_program_map p id) (genv_program_map tp id). fold ge; fold tge; fold pm. + rewrite transform_program_charact. rewrite B, C. intros. + destruct (IS.mem id used); try contradiction. + destruct (pm!id) as [gd|]; try contradiction. + destruct gd as [fd'|gv']. + + assert (b' <> b') by (eapply Genv.genv_funs_vars; eassumption). congruence. + + congruence. +Qed. + +Lemma globals_symbols_inject: + forall j, meminj_preserves_globals j -> symbols_inject j ge tge. +Proof. + intros. + assert (E1: Genv.genv_public ge = p.(prog_public)). + { apply Genv.globalenv_public. } + assert (E2: Genv.genv_public tge = p.(prog_public)). + { unfold tge; rewrite Genv.globalenv_public. + unfold transform_program in TRANSF. rewrite USED_GLOBALS in TRANSF. inversion TRANSF. auto. } + split; [|split;[|split]]; intros. + + unfold Genv.public_symbol; rewrite E1, E2. + destruct (Genv.find_symbol tge id) as [b'|] eqn:TFS. + exploit symbols_inject_3; eauto. intros (b & FS & INJ). rewrite FS. auto. + destruct (Genv.find_symbol ge id) as [b|] eqn:FS; auto. + destruct (in_dec ident_eq id (prog_public p)); simpl; auto. + exploit symbols_inject_2; eauto. apply kept_public; auto. + intros (b' & TFS' & INJ). congruence. + + eapply symbols_inject_1; eauto. + + unfold Genv.public_symbol in H0. + destruct (Genv.find_symbol ge id) as [b|] eqn:FS; try discriminate. + rewrite E1 in H0. + destruct (in_dec ident_eq id (prog_public p)); try discriminate. inv H1. + exploit symbols_inject_2; eauto. apply kept_public; auto. + intros (b' & A & B); exists b'; auto. + + unfold block_is_volatile. + destruct (Genv.find_var_info ge b1) as [gv|] eqn:V1. + exploit var_info_inject; eauto. intros [A B]. rewrite A. auto. + destruct (Genv.find_var_info tge b2) as [gv|] eqn:V2; auto. + exploit var_info_rev_inject; eauto. intros [A B]. congruence. +Qed. + +Lemma symbol_address_inject: + forall j id ofs, + meminj_preserves_globals j -> kept id -> + val_inject j (Genv.symbol_address ge id ofs) (Genv.symbol_address tge id ofs). +Proof. + intros. unfold Genv.symbol_address. destruct (Genv.find_symbol ge id) as [b|] eqn:FS; auto. + exploit symbols_inject_2; eauto. intros (b' & TFS & INJ). rewrite TFS. + econstructor; eauto. rewrite Int.add_zero; auto. +Qed. + +(** Semantic preservation *) + +Definition regset_inject (f: meminj) (rs rs': regset): Prop := + forall r, val_inject f rs#r rs'#r. + +Lemma regs_inject: + forall f rs rs', regset_inject f rs rs' -> forall l, val_list_inject f rs##l rs'##l. +Proof. + induction l; simpl. constructor. constructor; auto. +Qed. + +Lemma set_reg_inject: + forall f rs rs' r v v', + regset_inject f rs rs' -> val_inject f v v' -> + regset_inject f (rs#r <- v) (rs'#r <- v'). +Proof. + intros; red; intros. rewrite ! Regmap.gsspec. destruct (peq r0 r); auto. +Qed. + +Lemma regset_inject_incr: + forall f f' rs rs', regset_inject f rs rs' -> inject_incr f f' -> regset_inject f' rs rs'. +Proof. + intros; red; intros. apply val_inject_incr with f; auto. +Qed. + +Lemma regset_undef_inject: + forall f, regset_inject f (Regmap.init Vundef) (Regmap.init Vundef). +Proof. + intros; red; intros. rewrite Regmap.gi. auto. +Qed. + +Lemma init_regs_inject: + forall f args args', val_list_inject f args args' -> + forall params, + regset_inject f (init_regs args params) (init_regs args' params). +Proof. + induction 1; intros; destruct params; simpl; try (apply regset_undef_inject). + apply set_reg_inject; auto. +Qed. + +Inductive match_stacks (j: meminj): + list stackframe -> list stackframe -> block -> block -> Prop := + | match_stacks_nil: forall bound tbound, + meminj_preserves_globals j -> + Ple (Genv.genv_next ge) bound -> Ple (Genv.genv_next tge) tbound -> + match_stacks j nil nil bound tbound + | match_stacks_cons: forall res f sp pc rs s tsp trs ts bound tbound + (STACKS: match_stacks j s ts sp tsp) + (KEPT: forall id, ref_function f id -> kept id) + (SPINJ: j sp = Some(tsp, 0)) + (REGINJ: regset_inject j rs trs) + (BELOW: Plt sp bound) + (TBELOW: Plt tsp tbound), + match_stacks j (Stackframe res f (Vptr sp Int.zero) pc rs :: s) + (Stackframe res f (Vptr tsp Int.zero) pc trs :: ts) + bound tbound. + +Lemma match_stacks_preserves_globals: + forall j s ts bound tbound, + match_stacks j s ts bound tbound -> + meminj_preserves_globals j. +Proof. + induction 1; auto. +Qed. + +Lemma match_stacks_incr: + forall j j', inject_incr j j' -> + forall s ts bound tbound, match_stacks j s ts bound tbound -> + (forall b1 b2 delta, + j b1 = None -> j' b1 = Some(b2, delta) -> Ple bound b1 /\ Ple tbound b2) -> + match_stacks j' s ts bound tbound. +Proof. + induction 2; intros. +- assert (SAME: forall b b' delta, Plt b (Genv.genv_next ge) -> + j' b = Some(b', delta) -> j b = Some(b', delta)). + { intros. destruct (j b) as [[b1 delta1] | ] eqn: J. + exploit H; eauto. congruence. + exploit H3; eauto. intros [A B]. elim (Plt_strict b). + eapply Plt_Ple_trans. eauto. eapply Ple_trans; eauto. } + assert (SAME': forall b b' delta, Plt b' (Genv.genv_next tge) -> + j' b = Some(b', delta) -> j b = Some (b', delta)). + { intros. destruct (j b) as [[b1 delta1] | ] eqn: J. + exploit H; eauto. congruence. + exploit H3; eauto. intros [A B]. elim (Plt_strict b'). + eapply Plt_Ple_trans. eauto. eapply Ple_trans; eauto. } + constructor; auto. constructor; intros. + + exploit symbols_inject_1; eauto. apply SAME; auto. + eapply Genv.genv_symb_range; eauto. + + exploit symbols_inject_2; eauto. intros (b' & A & B). + exists b'; auto. + + exploit symbols_inject_3; eauto. intros (b & A & B). + exists b; auto. + + eapply funct_ptr_inject; eauto. apply SAME; auto. + eapply Genv.genv_funs_range; eauto. + + eapply var_info_inject; eauto. apply SAME; auto. + eapply Genv.genv_vars_range; eauto. + + eapply var_info_rev_inject; eauto. apply SAME'; auto. + eapply Genv.genv_vars_range; eauto. +- econstructor; eauto. + apply IHmatch_stacks. + intros. exploit H1; eauto. intros [A B]. split; eapply Ple_trans; eauto. + apply Plt_Ple; auto. apply Plt_Ple; auto. + apply regset_inject_incr with j; auto. +Qed. + +Lemma match_stacks_bound: + forall j s ts bound tbound bound' tbound', + match_stacks j s ts bound tbound -> + Ple bound bound' -> Ple tbound tbound' -> + match_stacks j s ts bound' tbound'. +Proof. + induction 1; intros. +- constructor; auto. eapply Ple_trans; eauto. eapply Ple_trans; eauto. +- econstructor; eauto. eapply Plt_Ple_trans; eauto. eapply Plt_Ple_trans; eauto. +Qed. + +Inductive match_states: state -> state -> Prop := + | match_states_regular: forall s f sp pc rs m ts tsp trs tm j + (STACKS: match_stacks j s ts sp tsp) + (KEPT: forall id, ref_function f id -> kept id) + (SPINJ: j sp = Some(tsp, 0)) + (REGINJ: regset_inject j rs trs) + (MEMINJ: Mem.inject j m tm), + match_states (State s f (Vptr sp Int.zero) pc rs m) + (State ts f (Vptr tsp Int.zero) pc trs tm) + | match_states_call: forall s fd args m ts targs tm j + (STACKS: match_stacks j s ts (Mem.nextblock m) (Mem.nextblock tm)) + (KEPT: forall id, ref_fundef fd id -> kept id) + (ARGINJ: val_list_inject j args targs) + (MEMINJ: Mem.inject j m tm), + match_states (Callstate s fd args m) + (Callstate ts fd targs tm) + | match_states_return: forall s res m ts tres tm j + (STACKS: match_stacks j s ts (Mem.nextblock m) (Mem.nextblock tm)) + (RESINJ: val_inject j res tres) + (MEMINJ: Mem.inject j m tm), + match_states (Returnstate s res m) + (Returnstate ts tres tm). + +Lemma external_call_inject: + forall ef vargs m1 t vres m2 f m1' vargs', + meminj_preserves_globals f -> + external_call ef ge vargs m1 t vres m2 -> + (forall id, In id (globals_external ef) -> kept id) -> + Mem.inject f m1 m1' -> + val_list_inject f vargs vargs' -> + exists f', exists vres', exists m2', + external_call ef tge vargs' m1' t vres' m2' + /\ val_inject f' vres vres' + /\ Mem.inject f' m2 m2' + /\ Mem.unchanged_on (loc_unmapped f) m1 m2 + /\ Mem.unchanged_on (loc_out_of_reach f m1) m1' m2' + /\ inject_incr f f' + /\ inject_separated f f' m1 m1'. +Proof. + intros. eapply external_call_mem_inject_gen; eauto. +- apply globals_symbols_inject; auto. +- intros. exploit symbols_inject_2; eauto. + intros (b' & A & B); exists b'; auto. +Qed. + +Lemma find_function_inject: + forall j ros rs fd trs, + meminj_preserves_globals j -> + find_function ge ros rs = Some fd -> + match ros with inl r => regset_inject j rs trs | inr id => kept id end -> + find_function tge ros trs = Some fd /\ (forall id, ref_fundef fd id -> kept id). +Proof. + intros. destruct ros as [r|id]; simpl in *. +- exploit Genv.find_funct_inv; eauto. intros (b & R). rewrite R in H0. + rewrite Genv.find_funct_find_funct_ptr in H0. + specialize (H1 r). rewrite R in H1. inv H1. + exploit funct_ptr_inject; eauto. intros (A & B & C). + rewrite B; auto. +- destruct (Genv.find_symbol ge id) as [b|] eqn:FS; try discriminate. + exploit symbols_inject_2; eauto. intros (tb & P & Q). rewrite P. + exploit funct_ptr_inject; eauto. intros (A & B & C). + auto. +Qed. + +Theorem step_simulation: + forall S1 t S2, step ge S1 t S2 -> + forall S1' (MS: match_states S1 S1'), + exists S2', step tge S1' t S2' /\ match_states S2 S2'. +Proof. + induction 1; intros; inv MS. + +- (* nop *) + econstructor; split. + eapply exec_Inop; eauto. + econstructor; eauto. + +- (* op *) + assert (A: exists tv, + eval_operation tge (Vptr tsp Int.zero) op trs##args tm = Some tv + /\ val_inject j v tv). + { apply eval_operation_inj with (ge1 := ge) (m1 := m) (sp1 := Vptr sp0 Int.zero) (vl1 := rs##args). + intros; eapply Mem.valid_pointer_inject_val; eauto. + intros; eapply Mem.weak_valid_pointer_inject_val; eauto. + intros; eapply Mem.weak_valid_pointer_inject_no_overflow; eauto. + intros; eapply Mem.different_pointers_inject; eauto. + intros. apply symbol_address_inject. eapply match_stacks_preserves_globals; eauto. + apply KEPT. red. exists pc, (Iop op args res pc'); auto. + econstructor; eauto. + apply regs_inject; auto. + assumption. } + destruct A as (tv & B & C). + econstructor; split. eapply exec_Iop; eauto. + econstructor; eauto. apply set_reg_inject; auto. + +- (* load *) + assert (A: exists ta, + eval_addressing tge (Vptr tsp Int.zero) addr trs##args = Some ta + /\ val_inject j a ta). + { apply eval_addressing_inj with (ge1 := ge) (sp1 := Vptr sp0 Int.zero) (vl1 := rs##args). + intros. apply symbol_address_inject. eapply match_stacks_preserves_globals; eauto. + apply KEPT. red. exists pc, (Iload chunk addr args dst pc'); auto. + econstructor; eauto. + apply regs_inject; auto. + assumption. } + destruct A as (ta & B & C). + exploit Mem.loadv_inject; eauto. intros (tv & D & E). + econstructor; split. eapply exec_Iload; eauto. + econstructor; eauto. apply set_reg_inject; auto. + +- (* store *) + assert (A: exists ta, + eval_addressing tge (Vptr tsp Int.zero) addr trs##args = Some ta + /\ val_inject j a ta). + { apply eval_addressing_inj with (ge1 := ge) (sp1 := Vptr sp0 Int.zero) (vl1 := rs##args). + intros. apply symbol_address_inject. eapply match_stacks_preserves_globals; eauto. + apply KEPT. red. exists pc, (Istore chunk addr args src pc'); auto. + econstructor; eauto. + apply regs_inject; auto. + assumption. } + destruct A as (ta & B & C). + exploit Mem.storev_mapped_inject; eauto. intros (tm' & D & E). + econstructor; split. eapply exec_Istore; eauto. + econstructor; eauto. + +- (* call *) + exploit find_function_inject. + eapply match_stacks_preserves_globals; eauto. eauto. + destruct ros as [r|id]. eauto. apply KEPT. red. econstructor; econstructor; split; eauto. simpl; auto. + intros (A & B). + econstructor; split. eapply exec_Icall; eauto. + econstructor; eauto. + econstructor; eauto. + change (Mem.valid_block m sp0). eapply Mem.valid_block_inject_1; eauto. + change (Mem.valid_block tm tsp). eapply Mem.valid_block_inject_2; eauto. + apply regs_inject; auto. + +- (* tailcall *) + exploit find_function_inject. + eapply match_stacks_preserves_globals; eauto. eauto. + destruct ros as [r|id]. eauto. apply KEPT. red. econstructor; econstructor; split; eauto. simpl; auto. + intros (A & B). + exploit Mem.free_parallel_inject; eauto. rewrite ! Zplus_0_r. intros (tm' & C & D). + econstructor; split. + eapply exec_Itailcall; eauto. + econstructor; eauto. + apply match_stacks_bound with stk tsp; auto. + apply Plt_Ple. + change (Mem.valid_block m' stk). eapply Mem.valid_block_inject_1; eauto. + apply Plt_Ple. + change (Mem.valid_block tm' tsp). eapply Mem.valid_block_inject_2; eauto. + apply regs_inject; auto. + +- (* builtin *) + exploit external_call_inject; eauto. + eapply match_stacks_preserves_globals; eauto. + intros. apply KEPT. red. econstructor; econstructor; eauto. + apply regs_inject; eauto. + intros (j' & tv & tm' & A & B & C & D & E & F & G). + econstructor; split. + eapply exec_Ibuiltin; eauto. + eapply match_states_regular with (j := j'); eauto. + apply match_stacks_incr with j; auto. + intros. exploit G; eauto. intros [P Q]. + assert (Mem.valid_block m sp0) by (eapply Mem.valid_block_inject_1; eauto). + assert (Mem.valid_block tm tsp) by (eapply Mem.valid_block_inject_2; eauto). + unfold Mem.valid_block in *; xomega. + apply set_reg_inject; auto. apply regset_inject_incr with j; auto. + +- (* cond *) + assert (C: eval_condition cond trs##args tm = Some b). + { eapply eval_condition_inject; eauto. apply regs_inject; auto. } + econstructor; split. + eapply exec_Icond with (pc' := if b then ifso else ifnot); eauto. + econstructor; eauto. + +- (* jumptbl *) + generalize (REGINJ arg); rewrite H0; intros INJ; inv INJ. + econstructor; split. + eapply exec_Ijumptable; eauto. + econstructor; eauto. + +- (* return *) + exploit Mem.free_parallel_inject; eauto. rewrite ! Zplus_0_r. intros (tm' & C & D). + econstructor; split. + eapply exec_Ireturn; eauto. + econstructor; eauto. + apply match_stacks_bound with stk tsp; auto. + apply Plt_Ple. + change (Mem.valid_block m' stk). eapply Mem.valid_block_inject_1; eauto. + apply Plt_Ple. + change (Mem.valid_block tm' tsp). eapply Mem.valid_block_inject_2; eauto. + destruct or; simpl; auto. + +- (* internal function *) + exploit Mem.alloc_parallel_inject. eauto. eauto. apply Zle_refl. apply Zle_refl. + intros (j' & tm' & tstk & C & D & E & F & G). + assert (STK: stk = Mem.nextblock m) by (eapply Mem.alloc_result; eauto). + assert (TSTK: tstk = Mem.nextblock tm) by (eapply Mem.alloc_result; eauto). + assert (STACKS': match_stacks j' s ts stk tstk). + { rewrite STK, TSTK. + apply match_stacks_incr with j; auto. + intros. destruct (eq_block b1 stk). + subst b1. rewrite F in H1; inv H1. subst b2. split; apply Ple_refl. + rewrite G in H1 by auto. congruence. } + econstructor; split. + eapply exec_function_internal; eauto. + eapply match_states_regular with (j := j'); eauto. + apply init_regs_inject; auto. apply val_list_inject_incr with j; auto. + +- (* external function *) + exploit external_call_inject; eauto. + eapply match_stacks_preserves_globals; eauto. + intros (j' & tres & tm' & A & B & C & D & E & F & G). + econstructor; split. + eapply exec_function_external; eauto. + eapply match_states_return with (j := j'); eauto. + apply match_stacks_bound with (Mem.nextblock m) (Mem.nextblock tm). + apply match_stacks_incr with j; auto. + intros. exploit G; eauto. intros [P Q]. + unfold Mem.valid_block in *; xomega. + eapply external_call_nextblock; eauto. + eapply external_call_nextblock; eauto. + +- (* return *) + inv STACKS. econstructor; split. + eapply exec_return. + econstructor; eauto. apply set_reg_inject; auto. +Qed. + +(** Relating initial memory states *) + +Remark init_meminj_no_overlap: + forall m, Mem.meminj_no_overlap init_meminj m. +Proof. + intros; red; intros. + exploit init_meminj_invert. eexact H0. intros (A1 & id1 & B1 & C1). + exploit init_meminj_invert. eexact H1. intros (A2 & id2 & B2 & C2). + left; red; intros; subst b2'. + assert (id1 = id2) by (eapply Genv.genv_vars_inj; eauto). + congruence. +Qed. + +Lemma store_zeros_unmapped_inj: + forall m1 b1 i n m1', + store_zeros m1 b1 i n = Some m1' -> + forall m2, + Mem.mem_inj init_meminj m1 m2 -> + init_meminj b1 = None -> + Mem.mem_inj init_meminj m1' m2. +Proof. + intros until m1'. functional induction (store_zeros m1 b1 i n); intros. + inv H. auto. + eapply IHo; eauto. eapply Mem.store_unmapped_inj; eauto. + discriminate. +Qed. + +Lemma store_zeros_mapped_inj: + forall m1 b1 i n m1', + store_zeros m1 b1 i n = Some m1' -> + forall m2 b2, + Mem.mem_inj init_meminj m1 m2 -> + init_meminj b1 = Some(b2, 0) -> + exists m2', store_zeros m2 b2 i n = Some m2' /\ Mem.mem_inj init_meminj m1' m2'. +Proof. + intros until m1'. functional induction (store_zeros m1 b1 i n); intros. + inv H. exists m2; split; auto. rewrite store_zeros_equation, e; auto. + exploit Mem.store_mapped_inj; eauto. apply init_meminj_no_overlap. instantiate (1 := Vzero); constructor. + intros (m2' & A & B). rewrite Zplus_0_r in A. + exploit IHo; eauto. intros (m3' & C & D). + exists m3'; split; auto. rewrite store_zeros_equation, e, A, C; auto. + discriminate. +Qed. + +Lemma store_init_data_unmapped_inj: + forall m1 b1 i id m1' m2, + Genv.store_init_data ge m1 b1 i id = Some m1' -> + Mem.mem_inj init_meminj m1 m2 -> + init_meminj b1 = None -> + Mem.mem_inj init_meminj m1' m2. +Proof. + intros. destruct id; simpl in H; try (eapply Mem.store_unmapped_inj; now eauto). + inv H; auto. + destruct (Genv.find_symbol ge i0); try discriminate. eapply Mem.store_unmapped_inj; now eauto. +Qed. + +Lemma store_init_data_mapped_inj: + forall m1 b1 i init m1' b2 m2, + Genv.store_init_data ge m1 b1 i init = Some m1' -> + Mem.mem_inj init_meminj m1 m2 -> + init_meminj b1 = Some(b2, 0) -> + (forall id ofs, init = Init_addrof id ofs -> kept id) -> + exists m2', Genv.store_init_data tge m2 b2 i init = Some m2' /\ Mem.mem_inj init_meminj m1' m2'. +Proof. + intros. replace i with (i + 0) by omega. pose proof (init_meminj_no_overlap m1). + destruct init; simpl in *; try (eapply Mem.store_mapped_inj; now eauto). + inv H. exists m2; auto. + destruct (Genv.find_symbol ge i0) as [bi|] eqn:FS1; try discriminate. + exploit symbols_inject_2. eapply init_meminj_preserves_globals. eapply H2; eauto. eauto. + intros (bi' & A & B). rewrite A. eapply Mem.store_mapped_inj; eauto. + econstructor; eauto. rewrite Int.add_zero; auto. +Qed. + + Lemma store_init_data_list_unmapped_inj: + forall initlist m1 b1 i m1' m2, + Genv.store_init_data_list ge m1 b1 i initlist = Some m1' -> + Mem.mem_inj init_meminj m1 m2 -> + init_meminj b1 = None -> + Mem.mem_inj init_meminj m1' m2. +Proof. + induction initlist; simpl; intros. +- inv H; auto. +- destruct (Genv.store_init_data ge m1 b1 i a) as [m1''|] eqn:ST; try discriminate. + eapply IHinitlist; eauto. eapply store_init_data_unmapped_inj; eauto. +Qed. + +Lemma store_init_data_list_mapped_inj: + forall initlist m1 b1 i m1' b2 m2, + Genv.store_init_data_list ge m1 b1 i initlist = Some m1' -> + Mem.mem_inj init_meminj m1 m2 -> + init_meminj b1 = Some(b2, 0) -> + (forall id ofs, In (Init_addrof id ofs) initlist -> kept id) -> + exists m2', Genv.store_init_data_list tge m2 b2 i initlist = Some m2' /\ Mem.mem_inj init_meminj m1' m2'. +Proof. + induction initlist; simpl; intros. +- inv H. exists m2; auto. +- destruct (Genv.store_init_data ge m1 b1 i a) as [m1''|] eqn:ST; try discriminate. + exploit store_init_data_mapped_inj; eauto. intros (m2'' & A & B). + exploit IHinitlist; eauto. intros (m2' & C & D). + exists m2'; split; auto. rewrite A; auto. +Qed. + +Lemma alloc_global_unmapped_inj: + forall m1 id g m1' m2, + Genv.alloc_global ge m1 (id, g) = Some m1' -> + Mem.mem_inj init_meminj m1 m2 -> + init_meminj (Mem.nextblock m1) = None -> + Mem.mem_inj init_meminj m1' m2. +Proof. + unfold Genv.alloc_global; intros. destruct g as [fd|gv]. +- destruct (Mem.alloc m1 0 1) as (m1a, b) eqn:ALLOC. + exploit Mem.alloc_result; eauto. intros EQ. rewrite <- EQ in H1. + eapply Mem.drop_unmapped_inj with (m1 := m1a); eauto. + eapply Mem.alloc_left_unmapped_inj; eauto. +- set (sz := Genv.init_data_list_size (gvar_init gv)) in *. + destruct (Mem.alloc m1 0 sz) as (m1a, b) eqn:ALLOC. + destruct (store_zeros m1a b 0 sz) as [m1b|] eqn: STZ; try discriminate. + destruct (Genv.store_init_data_list ge m1b b 0 (gvar_init gv)) as [m1c|] eqn:ST; try discriminate. + exploit Mem.alloc_result; eauto. intros EQ. rewrite <- EQ in H1. + eapply Mem.drop_unmapped_inj with (m1 := m1c); eauto. + eapply store_init_data_list_unmapped_inj with (m1 := m1b); eauto. + eapply store_zeros_unmapped_inj with (m1 := m1a); eauto. + eapply Mem.alloc_left_unmapped_inj; eauto. +Qed. + +Lemma alloc_global_mapped_inj: + forall m1 id g m1' m2, + Genv.alloc_global ge m1 (id, g) = Some m1' -> + Mem.mem_inj init_meminj m1 m2 -> + init_meminj (Mem.nextblock m1) = Some(Mem.nextblock m2, 0) -> + (forall id, ref_def g id -> kept id) -> + exists m2', + Genv.alloc_global tge m2 (id, g) = Some m2' /\ Mem.mem_inj init_meminj m1' m2'. +Proof. + unfold Genv.alloc_global; intros. destruct g as [fd|gv]. +- destruct (Mem.alloc m1 0 1) as (m1a, b1) eqn:ALLOC. + exploit Mem.alloc_result; eauto. intros EQ. rewrite <- EQ in H1. + destruct (Mem.alloc m2 0 1) as (m2a, b2) eqn:ALLOC2. + exploit Mem.alloc_result; eauto. intros EQ2. rewrite <- EQ2 in H1. + assert (Mem.mem_inj init_meminj m1a m2a). + { eapply Mem.alloc_left_mapped_inj with (b1 := b1) (b2 := b2) (delta := 0). + eapply Mem.alloc_right_inj; eauto. + eauto. + eauto with mem. + red; intros; apply Z.divide_0_r. + intros. apply Mem.perm_implies with Freeable; auto with mem. + eapply Mem.perm_alloc_2; eauto. omega. + auto. + } + exploit Mem.drop_mapped_inj; eauto. apply init_meminj_no_overlap. +- set (sz := Genv.init_data_list_size (gvar_init gv)) in *. + destruct (Mem.alloc m1 0 sz) as (m1a, b1) eqn:ALLOC. + destruct (store_zeros m1a b1 0 sz) as [m1b|] eqn: STZ; try discriminate. + destruct (Genv.store_init_data_list ge m1b b1 0 (gvar_init gv)) as [m1c|] eqn:ST; try discriminate. + exploit Mem.alloc_result; eauto. intros EQ. rewrite <- EQ in H1. + destruct (Mem.alloc m2 0 sz) as (m2a, b2) eqn:ALLOC2. + exploit Mem.alloc_result; eauto. intros EQ2. rewrite <- EQ2 in H1. + assert (Mem.mem_inj init_meminj m1a m2a). + { eapply Mem.alloc_left_mapped_inj with (b1 := b1) (b2 := b2) (delta := 0). + eapply Mem.alloc_right_inj; eauto. + eauto. + eauto with mem. + red; intros; apply Z.divide_0_r. + intros. apply Mem.perm_implies with Freeable; auto with mem. + eapply Mem.perm_alloc_2; eauto. omega. + auto. + } + exploit store_zeros_mapped_inj; eauto. intros (m2b & A & B). + exploit store_init_data_list_mapped_inj; eauto. + intros. apply H2. red. exists ofs; auto. intros (m2c & C & D). + exploit Mem.drop_mapped_inj; eauto. apply init_meminj_no_overlap. intros (m2' & E & F). + exists m2'; split; auto. rewrite ! Zplus_0_r in E. rewrite A, C, E. auto. +Qed. + +Lemma alloc_globals_app: + forall F V (g: Genv.t F V) defs1 m defs2, + Genv.alloc_globals g m (defs1 ++ defs2) = + match Genv.alloc_globals g m defs1 with + | None => None + | Some m1 => Genv.alloc_globals g m1 defs2 + end. +Proof. + induction defs1; simpl; intros. auto. + destruct (Genv.alloc_global g m a); auto. +Qed. + +Lemma alloc_globals_snoc: + forall F V (g: Genv.t F V) m defs1 id_def, + Genv.alloc_globals g m (defs1 ++ id_def :: nil) = + match Genv.alloc_globals g m defs1 with + | None => None + | Some m1 => Genv.alloc_global g m1 id_def + end. +Proof. + intros. rewrite alloc_globals_app. + destruct (Genv.alloc_globals g m defs1); auto. unfold Genv.alloc_globals. + destruct (Genv.alloc_global g m0 id_def); auto. +Qed. + +Lemma alloc_globals_inj: + forall pubs defs m1 u g1 g2, + Genv.alloc_globals ge Mem.empty (List.rev defs) = Some m1 -> + g1 = Genv.add_globals (Genv.empty_genv _ _ pubs) (List.rev defs) -> + g2 = Genv.add_globals (Genv.empty_genv _ _ pubs) (filter_globdefs u nil defs) -> + Mem.nextblock m1 = Genv.genv_next g1 -> + (forall id, IS.In id u -> Genv.find_symbol g1 id = Genv.find_symbol ge id) -> + (forall id, IS.In id u -> Genv.find_symbol g2 id = Genv.find_symbol tge id) -> + (forall b id, Genv.find_symbol ge id = Some b -> Plt b (Mem.nextblock m1) -> kept id -> IS.In id u) -> + (forall id, IS.In id u -> (fold_left add_def_prog_map (List.rev defs) (PTree.empty _))!id = pm!id) -> + exists m2, + Genv.alloc_globals tge Mem.empty (filter_globdefs u nil defs) = Some m2 + /\ Mem.nextblock m2 = Genv.genv_next g2 + /\ Mem.mem_inj init_meminj m1 m2. +Proof. + induction defs; simpl; intros until g2; intros ALLOC GE1 GE2 NEXT1 SYMB1 SYMB2 SYMB3 PROGMAP. +- inv ALLOC. exists Mem.empty. intuition auto. constructor; intros. + eelim Mem.perm_empty; eauto. + exploit init_meminj_invert; eauto. intros [A B]. subst delta. apply Z.divide_0_r. + eelim Mem.perm_empty; eauto. +- rewrite Genv.add_globals_app in GE1. simpl in GE1. + set (g1' := Genv.add_globals (Genv.empty_genv fundef unit pubs) (rev defs)) in *. + rewrite alloc_globals_snoc in ALLOC. + destruct (Genv.alloc_globals ge Mem.empty (rev defs)) as [m1'|] eqn:ALLOC1'; try discriminate. + exploit Genv.alloc_global_nextblock; eauto. intros NEXTBLOCK1. + assert (NEXTGE1: Genv.genv_next g1 = Pos.succ (Genv.genv_next g1')) by (rewrite GE1; reflexivity). + assert (NEXT1': Mem.nextblock m1' = Genv.genv_next g1') by (unfold block in *; xomega). + rewrite fold_left_app in PROGMAP. simpl in PROGMAP. + destruct a as [id gd]. unfold add_def_prog_map at 1 in PROGMAP. simpl in PROGMAP. + destruct (IS.mem id u) eqn:MEM. + + rewrite filter_globdefs_nil in *. rewrite alloc_globals_snoc. + rewrite Genv.add_globals_app in GE2. simpl in GE2. + set (g2' := Genv.add_globals (Genv.empty_genv fundef unit pubs) (filter_globdefs (IS.remove id u) nil defs)) in *. + assert (NEXTGE2: Genv.genv_next g2 = Pos.succ (Genv.genv_next g2')) by (rewrite GE2; reflexivity). + assert (FS1: Genv.find_symbol ge id = Some (Mem.nextblock m1')). + { rewrite <- SYMB1 by (apply IS.mem_2; auto). + rewrite GE1. unfold Genv.find_symbol; simpl. rewrite PTree.gss. congruence. } + exploit (IHdefs m1' (IS.remove id u) g1' g2'); eauto. + intros. rewrite ISF.remove_iff in H; destruct H. + rewrite <- SYMB1 by auto. rewrite GE1. unfold Genv.find_symbol; simpl. + rewrite PTree.gso; auto. + intros. rewrite ISF.remove_iff in H; destruct H. + rewrite <- SYMB2 by auto. rewrite GE2. unfold Genv.find_symbol; simpl. + rewrite PTree.gso; auto. + intros. rewrite ISF.remove_iff. destruct (ident_eq id id0). + subst id0. rewrite FS1 in H. inv H. eelim Plt_strict; eauto. + exploit SYMB3. eexact H. unfold block in *; xomega. auto. tauto. + intros. rewrite ISF.remove_iff in H; destruct H. + rewrite <- PROGMAP by auto. rewrite PTree.gso by auto. auto. + intros (m2' & A & B & C). fold g2' in B. + assert (FS2: Genv.find_symbol tge id = Some (Mem.nextblock m2')). + { rewrite <- SYMB2 by (apply IS.mem_2; auto). + rewrite GE2. unfold Genv.find_symbol; simpl. rewrite PTree.gss. congruence. } + assert (INJ: init_meminj (Mem.nextblock m1') = Some (Mem.nextblock m2', 0)). + { apply Genv.find_invert_symbol in FS1. unfold init_meminj. rewrite FS1, FS2. auto. } + exploit alloc_global_mapped_inj. eexact ALLOC. eexact C. exact INJ. + intros. apply kept_closed with id gd. eapply transform_program_kept; eauto. + rewrite <- PROGMAP by (apply IS.mem_2; auto). apply PTree.gss. auto. + intros (m2 & D & E). + exploit Genv.alloc_global_nextblock; eauto. intros NEXTBLOCK2. + exists m2; split. rewrite A, D. auto. + split. unfold block in *; xomega. + auto. + + exploit (IHdefs m1' u g1' g2); auto. + intros. rewrite <- SYMB1 by auto. rewrite GE1. + unfold Genv.find_symbol; simpl. rewrite PTree.gso; auto. + red; intros; subst id0. apply IS.mem_1 in H. congruence. + intros. eapply SYMB3; eauto. unfold block in *; xomega. + intros. rewrite <- PROGMAP by auto. rewrite PTree.gso; auto. + apply IS.mem_1 in H. congruence. + intros (m2 & A & B & C). + assert (NOTINJ: init_meminj (Mem.nextblock m1') = None). + { destruct (init_meminj (Mem.nextblock m1')) as [[b' delta]|] eqn:J; auto. + exploit init_meminj_invert; eauto. intros (U & id1 & V & W). + exploit SYMB3; eauto. unfold block in *; xomega. + eapply transform_program_kept; eauto. + intros P. + revert V. rewrite <- SYMB1, GE1 by auto. unfold Genv.find_symbol; simpl. + rewrite PTree.gsspec. rewrite NEXT1'. destruct (peq id1 id); intros Q. + subst id1. apply IS.mem_1 in P. congruence. + eelim Plt_strict. eapply Genv.genv_symb_range; eauto. } + exists m2; intuition auto. eapply alloc_global_unmapped_inj; eauto. +Qed. + +Theorem init_mem_inject: + forall m, + Genv.init_mem p = Some m -> + exists f tm, Genv.init_mem tp = Some tm /\ Mem.inject f m tm /\ meminj_preserves_globals f. +Proof. + intros. + unfold transform_program in TRANSF; rewrite USED_GLOBALS in TRANSF; injection TRANSF. intros EQ. + destruct (alloc_globals_inj (prog_public p) (List.rev (prog_defs p)) m used ge tge) as (tm & A & B & C). + rewrite rev_involutive; auto. + rewrite rev_involutive; auto. + unfold tge; rewrite <- EQ; auto. + symmetry. apply Genv.init_mem_genv_next; auto. + auto. auto. auto. + intros. rewrite rev_involutive. auto. + assert (D: Genv.init_mem tp = Some tm). + { unfold Genv.init_mem. fold tge. rewrite <- EQ. exact A. } + pose proof (init_meminj_preserves_globals). + exists init_meminj, tm; intuition auto. + constructor; intros. + + auto. + + destruct (init_meminj b) as [[b1 delta1]|] eqn:INJ; auto. + exploit init_meminj_invert; eauto. intros (P & id & Q & R). + elim H1. eapply Genv.find_symbol_not_fresh; eauto. + + exploit init_meminj_invert; eauto. intros (P & id & Q & R). + eapply Genv.find_symbol_not_fresh; eauto. + + apply init_meminj_no_overlap. + + exploit init_meminj_invert; eauto. intros (P & id & Q & R). + split. omega. generalize (Int.unsigned_range_2 ofs). omega. +Qed. + +Lemma transf_initial_states: + forall S1, initial_state p S1 -> exists S2, initial_state tp S2 /\ match_states S1 S2. +Proof. + intros. inv H. exploit init_mem_inject; eauto. intros (j & tm & A & B & C). + exploit symbols_inject_2. eauto. apply kept_main. eexact H1. intros (tb & P & Q). + exploit funct_ptr_inject. eauto. eexact Q. exact H2. + intros (R & S & T). + exists (Callstate nil f nil tm); split. + econstructor; eauto. + fold tge. unfold transform_program in TRANSF; rewrite USED_GLOBALS in TRANSF; inversion TRANSF; auto. + econstructor; eauto. + constructor. auto. + erewrite <- Genv.init_mem_genv_next by eauto. apply Ple_refl. + erewrite <- Genv.init_mem_genv_next by eauto. apply Ple_refl. +Qed. + +Lemma transf_final_states: + forall S1 S2 r, + match_states S1 S2 -> final_state S1 r -> final_state S2 r. +Proof. + intros. inv H0. inv H. inv STACKS. inv RESINJ. constructor. +Qed. + +Theorem transf_program_correct: + forward_simulation (semantics p) (semantics tp). +Proof. + intros. + eapply forward_simulation_step. + exploit globals_symbols_inject. apply init_meminj_preserves_globals. intros [A B]. exact A. + eexact transf_initial_states. + eexact transf_final_states. + eexact step_simulation. +Qed. + +End SOUNDNESS. diff --git a/cfrontend/C2C.ml b/cfrontend/C2C.ml index 73d9edbd..4d5d6c07 100644 --- a/cfrontend/C2C.ml +++ b/cfrontend/C2C.ml @@ -28,6 +28,8 @@ open Csyntax open Initializers open Floats +(** ** Extracting information about global variables from their atom *) + (** Record useful information about global variables and functions, and associate it with the corresponding atoms. *) @@ -43,6 +45,61 @@ type atom_info = let decl_atom : (AST.ident, atom_info) Hashtbl.t = Hashtbl.create 103 +let atom_is_static a = + try + let i = Hashtbl.find decl_atom a in + (* inline functions can remain in generated code, but should not + be global, unless explicitly marked "extern" *) + match i.a_storage with + | C.Storage_default -> i.a_inline + | C.Storage_extern -> false + | C.Storage_static -> true + | C.Storage_register -> false (* should not happen *) + with Not_found -> + false + +let atom_is_extern a = + try + (Hashtbl.find decl_atom a).a_storage = C.Storage_extern + with Not_found -> + false + +let atom_alignof a = + try + (Hashtbl.find decl_atom a).a_alignment + with Not_found -> + None + +let atom_sections a = + try + (Hashtbl.find decl_atom a).a_sections + with Not_found -> + [] + +let atom_is_small_data a ofs = + try + (Hashtbl.find decl_atom a).a_access = Sections.Access_near + with Not_found -> + false + +let atom_is_rel_data a ofs = + try + (Hashtbl.find decl_atom a).a_access = Sections.Access_far + with Not_found -> + false + +let atom_is_inline a = + try + (Hashtbl.find decl_atom a).a_inline + with Not_found -> + false + +let atom_location a = + try + (Hashtbl.find decl_atom a).a_loc + with Not_found -> + Cutil.no_loc + (** Hooks -- overriden in machine-dependent CPragmas module *) let process_pragma_hook = ref (fun (s: string) -> false) @@ -1059,6 +1116,13 @@ let cleanupGlobals p = clean defs (g :: accu) gl in clean IdentSet.empty [] (List.rev p) +(** Extract the list of public (non-static) names *) + +let public_globals gl = + List.fold_left + (fun accu (id, g) -> if atom_is_static id then accu else id :: accu) + [] gl + (** Convert a [C.program] into a [Csyntax.program] *) let convertProgram p = @@ -1072,66 +1136,11 @@ let convertProgram p = let gl1 = convertGlobdecls (translEnv Env.empty p) [] (cleanupGlobals p) in let gl2 = globals_for_strings gl1 in let p' = { AST.prog_defs = gl2; - AST.prog_main = intern_string "main" } in + AST.prog_public = public_globals gl2; + AST.prog_main = intern_string "main" } in if !numErrors > 0 then None else Some p' with Env.Error msg -> error (Env.error_message msg); None -(** ** Extracting information about global variables from their atom *) - -let atom_is_static a = - try - let i = Hashtbl.find decl_atom a in - (* inline functions can remain in generated code, but should not - be global, unless explicitly marked "extern" *) - match i.a_storage with - | C.Storage_default -> i.a_inline - | C.Storage_extern -> false - | C.Storage_static -> true - | C.Storage_register -> false (* should not happen *) - with Not_found -> - false - -let atom_is_extern a = - try - (Hashtbl.find decl_atom a).a_storage = C.Storage_extern - with Not_found -> - false - -let atom_alignof a = - try - (Hashtbl.find decl_atom a).a_alignment - with Not_found -> - None - -let atom_sections a = - try - (Hashtbl.find decl_atom a).a_sections - with Not_found -> - [] - -let atom_is_small_data a ofs = - try - (Hashtbl.find decl_atom a).a_access = Sections.Access_near - with Not_found -> - false - -let atom_is_rel_data a ofs = - try - (Hashtbl.find decl_atom a).a_access = Sections.Access_far - with Not_found -> - false - -let atom_is_inline a = - try - (Hashtbl.find decl_atom a).a_inline - with Not_found -> - false - -let atom_location a = - try - (Hashtbl.find decl_atom a).a_loc - with Not_found -> - Cutil.no_loc diff --git a/cfrontend/Cexec.v b/cfrontend/Cexec.v index c33068d9..80748df1 100644 --- a/cfrontend/Cexec.v +++ b/cfrontend/Cexec.v @@ -106,7 +106,10 @@ Definition eventval_of_val (v: val) (t: typ) : option eventval := | Vfloat f, AST.Tfloat => Some (EVfloat f) | Vsingle f, AST.Tsingle => Some (EVsingle f) | Vlong n, AST.Tlong => Some (EVlong n) - | Vptr b ofs, AST.Tint => do id <- Genv.invert_symbol ge b; Some (EVptr_global id ofs) + | Vptr b ofs, AST.Tint => + do id <- Genv.invert_symbol ge b; + check (Genv.public_symbol ge id); + Some (EVptr_global id ofs) | _, _ => None end. @@ -126,7 +129,10 @@ Definition val_of_eventval (ev: eventval) (t: typ) : option val := | EVfloat f, AST.Tfloat => Some (Vfloat f) | EVsingle f, AST.Tsingle => Some (Vsingle f) | EVlong n, AST.Tlong => Some (Vlong n) - | EVptr_global id ofs, AST.Tint => do b <- Genv.find_symbol ge id; Some (Vptr b ofs) + | EVptr_global id ofs, AST.Tint => + check (Genv.public_symbol ge id); + do b <- Genv.find_symbol ge id; + Some (Vptr b ofs) | _, _ => None end. @@ -134,15 +140,16 @@ Lemma eventval_of_val_sound: forall v t ev, eventval_of_val v t = Some ev -> eventval_match ge ev t v. Proof. intros. destruct v; destruct t; simpl in H; inv H; try constructor. - destruct (Genv.invert_symbol ge b) as [id|] eqn:?; inv H1. - constructor. apply Genv.invert_find_symbol; auto. + destruct (Genv.invert_symbol ge b) as [id|] eqn:?; try discriminate. + destruct (Genv.public_symbol ge id) eqn:?; inv H1. + constructor. auto. apply Genv.invert_find_symbol; auto. Qed. Lemma eventval_of_val_complete: forall ev t v, eventval_match ge ev t v -> eventval_of_val v t = Some ev. Proof. induction 1; simpl; auto. - rewrite (Genv.find_invert_symbol _ _ H). auto. + rewrite (Genv.find_invert_symbol _ _ H0). rewrite H. auto. Qed. Lemma list_eventval_of_val_sound: @@ -166,14 +173,15 @@ Lemma val_of_eventval_sound: forall ev t v, val_of_eventval ev t = Some v -> eventval_match ge ev t v. Proof. intros. destruct ev; destruct t; simpl in H; inv H; try constructor. + destruct (Genv.public_symbol ge i) eqn:?; try discriminate. destruct (Genv.find_symbol ge i) as [b|] eqn:?; inv H1. - constructor. auto. + constructor; auto. Qed. Lemma val_of_eventval_complete: forall ev t v, eventval_match ge ev t v -> val_of_eventval ev t = Some v. Proof. - induction 1; simpl; auto. rewrite H; auto. + induction 1; simpl; auto. rewrite H, H0; auto. Qed. (** Volatile memory accesses. *) diff --git a/cfrontend/Cminorgenproof.v b/cfrontend/Cminorgenproof.v index 7cb604ec..17c59b97 100644 --- a/cfrontend/Cminorgenproof.v +++ b/cfrontend/Cminorgenproof.v @@ -46,6 +46,10 @@ Lemma symbols_preserved: forall (s: ident), Genv.find_symbol tge s = Genv.find_symbol ge s. Proof (Genv.find_symbol_transf_partial transl_fundef _ TRANSL). +Lemma public_preserved: + forall (s: ident), Genv.public_symbol tge s = Genv.public_symbol ge s. +Proof (Genv.public_symbol_transf_partial transl_fundef _ TRANSL). + Lemma function_ptr_translated: forall (b: block) (f: Csharpminor.fundef), Genv.find_funct_ptr ge b = Some f -> @@ -2026,7 +2030,7 @@ Proof. left; econstructor; split. apply plus_one. econstructor. eauto. eapply external_call_symbols_preserved; eauto. - exact symbols_preserved. eexact varinfo_preserved. + exact symbols_preserved. exact public_preserved. eexact varinfo_preserved. assert (MCS': match_callstack f' m' tm' (Frame cenv tfn e le te sp lo hi :: cs) (Mem.nextblock m') (Mem.nextblock tm')). @@ -2181,7 +2185,7 @@ Opaque PTree.set. left; econstructor; split. apply plus_one. econstructor. eapply external_call_symbols_preserved; eauto. - exact symbols_preserved. eexact varinfo_preserved. + exact symbols_preserved. exact public_preserved. eexact varinfo_preserved. econstructor; eauto. apply match_callstack_incr_bound with (Mem.nextblock m) (Mem.nextblock tm). eapply match_callstack_external_call; eauto. @@ -2246,7 +2250,7 @@ Theorem transl_program_correct: forward_simulation (Csharpminor.semantics prog) (Cminor.semantics tprog). Proof. eapply forward_simulation_star; eauto. - eexact symbols_preserved. + eexact public_preserved. eexact transl_initial_states. eexact transl_final_states. eexact transl_step_correct. diff --git a/cfrontend/Cshmgenproof.v b/cfrontend/Cshmgenproof.v index fdf5b06d..9cb112b0 100644 --- a/cfrontend/Cshmgenproof.v +++ b/cfrontend/Cshmgenproof.v @@ -743,6 +743,10 @@ Lemma symbols_preserved: forall s, Genv.find_symbol tge s = Genv.find_symbol ge s. Proof (Genv.find_symbol_transf_partial2 transl_fundef transl_globvar _ TRANSL). +Lemma public_preserved: + forall s, Genv.public_symbol tge s = Genv.public_symbol ge s. +Proof (Genv.public_symbol_transf_partial2 transl_fundef transl_globvar _ TRANSL). + Lemma functions_translated: forall v f, Genv.find_funct ge v = Some f -> @@ -1285,7 +1289,7 @@ Proof. apply plus_one. econstructor. eapply transl_arglist_correct; eauto. eapply external_call_symbols_preserved_2; eauto. - exact symbols_preserved. + exact symbols_preserved. exact public_preserved. eexact (Genv.find_var_info_transf_partial2 transl_fundef transl_globvar _ TRANSL). eexact (Genv.find_var_info_rev_transf_partial2 transl_fundef transl_globvar _ TRANSL). eapply match_states_skip; eauto. @@ -1466,7 +1470,7 @@ Proof. econstructor; split. apply plus_one. constructor. eauto. eapply external_call_symbols_preserved_2; eauto. - exact symbols_preserved. + exact symbols_preserved. exact public_preserved. eexact (Genv.find_var_info_transf_partial2 transl_fundef transl_globvar _ TRANSL). eexact (Genv.find_var_info_rev_transf_partial2 transl_fundef transl_globvar _ TRANSL). econstructor; eauto. @@ -1506,7 +1510,7 @@ Theorem transl_program_correct: forward_simulation (Clight.semantics2 prog) (Csharpminor.semantics tprog). Proof. eapply forward_simulation_plus. - eexact symbols_preserved. + eexact public_preserved. eexact transl_initial_states. eexact transl_final_states. eexact transl_step. diff --git a/cfrontend/SimplExpr.v b/cfrontend/SimplExpr.v index df33d727..089797f2 100644 --- a/cfrontend/SimplExpr.v +++ b/cfrontend/SimplExpr.v @@ -541,4 +541,4 @@ Fixpoint transl_globdefs Definition transl_program (p: Csyntax.program) : res program := do gl' <- transl_globdefs p.(prog_defs) (initial_generator tt); - OK (mkprogram gl' p.(prog_main)). + OK (mkprogram gl' p.(prog_public) p.(prog_main)). diff --git a/cfrontend/SimplExprproof.v b/cfrontend/SimplExprproof.v index 3802b957..250f2b26 100644 --- a/cfrontend/SimplExprproof.v +++ b/cfrontend/SimplExprproof.v @@ -49,6 +49,13 @@ Proof. simpl. tauto. Qed. +Lemma public_preserved: + forall (s: ident), Genv.public_symbol tge s = Genv.public_symbol ge s. +Proof. + intros. eapply Genv.public_symbol_match. eapply transl_program_spec; eauto. + simpl. tauto. +Qed. + Lemma function_ptr_translated: forall b f, Genv.find_funct_ptr ge b = Some f -> @@ -155,7 +162,7 @@ Proof. rewrite H1. split; auto. eapply deref_loc_value; eauto. (* By_value, volatile *) rewrite H0; rewrite H1. eapply volatile_load_preserved with (ge1 := ge); auto. - exact symbols_preserved. exact block_is_volatile_preserved. + exact symbols_preserved. exact public_preserved. exact block_is_volatile_preserved. (* By reference *) rewrite H0. destruct (type_is_volatile ty); split; auto; eapply deref_loc_reference; eauto. (* By copy *) @@ -175,7 +182,7 @@ Proof. rewrite H1. split; auto. eapply assign_loc_value; eauto. (* By_value, volatile *) rewrite H0; rewrite H1. eapply volatile_store_preserved with (ge1 := ge); auto. - exact symbols_preserved. exact block_is_volatile_preserved. + exact symbols_preserved. exact public_preserved. exact block_is_volatile_preserved. (* By copy *) rewrite H0. destruct (type_is_volatile ty); split; auto; eapply assign_loc_copy; eauto. Qed. @@ -1861,7 +1868,7 @@ Proof. left. eapply plus_left. constructor. apply star_one. econstructor; eauto. eapply external_call_symbols_preserved; eauto. - exact symbols_preserved. exact varinfo_preserved. + exact symbols_preserved. exact public_preserved. exact varinfo_preserved. traceEq. econstructor; eauto. change sl2 with (nil ++ sl2). apply S. constructor. simpl; auto. auto. @@ -1872,7 +1879,7 @@ Proof. left. eapply plus_left. constructor. apply star_one. econstructor; eauto. eapply external_call_symbols_preserved; eauto. - exact symbols_preserved. exact varinfo_preserved. + exact symbols_preserved. exact public_preserved. exact varinfo_preserved. traceEq. econstructor; eauto. change sl2 with (nil ++ sl2). apply S. @@ -2161,7 +2168,7 @@ Proof. econstructor; split. left; apply plus_one. econstructor; eauto. eapply external_call_symbols_preserved; eauto. - exact symbols_preserved. exact varinfo_preserved. + exact symbols_preserved. exact public_preserved. exact varinfo_preserved. constructor; auto. (* return *) @@ -2198,7 +2205,7 @@ Proof. econstructor. exploit Genv.init_mem_match; eauto. simpl. fold tge. rewrite symbols_preserved. - destruct MP as [A B]. rewrite B; eexact H1. + destruct MP as (A & B & C). rewrite B; eexact H1. eexact FIND. rewrite <- H3. apply type_of_fundef_preserved. auto. constructor. auto. constructor. @@ -2215,7 +2222,7 @@ Theorem transl_program_correct: forward_simulation (Cstrategy.semantics prog) (Clight.semantics1 tprog). Proof. eapply forward_simulation_star_wf with (order := ltof _ measure). - eexact symbols_preserved. + eexact public_preserved. eexact transl_initial_states. eexact transl_final_states. apply well_founded_ltof. diff --git a/cfrontend/SimplLocalsproof.v b/cfrontend/SimplLocalsproof.v index 67a7e626..15d0af06 100644 --- a/cfrontend/SimplLocalsproof.v +++ b/cfrontend/SimplLocalsproof.v @@ -48,6 +48,12 @@ Proof. exact (Genv.find_symbol_transf_partial _ _ TRANSF). Qed. +Lemma public_preserved: + forall (s: ident), Genv.public_symbol tge s = Genv.public_symbol ge s. +Proof. + exact (Genv.public_symbol_transf_partial _ _ TRANSF). +Qed. + Lemma varinfo_preserved: forall b, Genv.find_var_info tge b = Genv.find_var_info ge b. Proof. @@ -2031,7 +2037,7 @@ Proof. intros [j' [tvres [tm' [P [Q [R [S [T [U V]]]]]]]]]. econstructor; split. apply plus_one. econstructor; eauto. eapply external_call_symbols_preserved; eauto. - exact symbols_preserved. exact varinfo_preserved. + exact symbols_preserved. exact public_preserved. exact varinfo_preserved. econstructor; eauto with compat. eapply match_envs_set_opttemp; eauto. eapply match_envs_extcall; eauto. @@ -2187,7 +2193,7 @@ Proof. intros [j' [tvres [tm' [P [Q [R [S [T [U V]]]]]]]]]. econstructor; split. apply plus_one. econstructor; eauto. eapply external_call_symbols_preserved; eauto. - exact symbols_preserved. exact varinfo_preserved. + exact symbols_preserved. exact public_preserved. exact varinfo_preserved. econstructor; eauto. intros. apply match_cont_incr_bounds with (Mem.nextblock m) (Mem.nextblock tm). eapply match_cont_extcall; eauto. xomega. xomega. @@ -2242,7 +2248,7 @@ Theorem transf_program_correct: forward_simulation (semantics1 prog) (semantics2 tprog). Proof. eapply forward_simulation_plus. - eexact symbols_preserved. + eexact public_preserved. eexact initial_states_simulation. eexact final_states_simulation. eexact step_simulation. diff --git a/checklink/Bitstring_utils.ml b/checklink/Bitstring_utils.ml index 2253b63f..3218f898 100644 --- a/checklink/Bitstring_utils.ml +++ b/checklink/Bitstring_utils.ml @@ -9,6 +9,13 @@ type bitstring = Bitstring.bitstring bitstring may be longer. @param size number of bits to check *) + +let is_zeros (bs: bitstring) (size: int): bool = + Bitstring.bitstring_length bs >= size + && Bitstring.is_zeroes_bitstring (Bitstring.subbitstring bs 0 size) + +(* + let rec is_zeros (bs: bitstring) (size: int): bool = size = 0 || if size >= 64 @@ -23,3 +30,4 @@ let rec is_zeros (bs: bitstring) (size: int): bool = | { 0L : size : int } -> true | { _ } -> false ) +*) diff --git a/checklink/Check.ml b/checklink/Check.ml index 5213b266..db0159c4 100644 --- a/checklink/Check.ml +++ b/checklink/Check.ml @@ -69,8 +69,8 @@ let name_of_section_Linux: section_name -> string = function | Section_text -> ".text" | Section_data i -> if i then ".data" else "COMM" | Section_small_data i -> if i then ".sdata" else ".sbss" -| Section_const -> ".rodata" -| Section_small_const -> ".sdata2" +| Section_const i -> if i then ".rodata" else "COMM" +| Section_small_const i -> if i then ".sdata2" else "COMM" | Section_string -> ".rodata" | Section_literal -> ".rodata.cst8" | Section_jumptable -> ".text" @@ -79,10 +79,10 @@ let name_of_section_Linux: section_name -> string = function (** Adapted from CompCert *) let name_of_section_Diab: section_name -> string = function | Section_text -> ".text" -| Section_data i -> if i then ".data" else ".bss" +| Section_data i -> if i then ".data" else "COMM" | Section_small_data i -> if i then ".sdata" else ".sbss" -| Section_const -> ".text" -| Section_small_const -> ".sdata2" +| Section_const _ -> ".text" +| Section_small_const _ -> ".sdata2" | Section_string -> ".text" | Section_literal -> ".text" | Section_jumptable -> ".text" @@ -91,7 +91,6 @@ let name_of_section_Diab: section_name -> string = function (** Taken from CompCert *) let name_of_section: section_name -> string = begin match Configuration.system with - | "macosx" -> fatal "Unsupported CompCert configuration: macosx" | "linux" -> name_of_section_Linux | "diab" -> name_of_section_Diab | _ -> fatal "Unsupported CompCert configuration" @@ -535,12 +534,6 @@ let check_label_existence ffw = had the expected [size]. *) let rec match_jmptbl lbllist vaddr size ffw = - let atom = Hashtbl.find ffw.sf.atoms ffw.this_ident in - let jmptbl_section = - match atom.a_sections with - | [_; _; j] -> j - | _ -> Section_jumptable - in let rec match_jmptbl_aux lbllist bs ffw = match lbllist with | [] -> OK ffw @@ -556,21 +549,14 @@ let rec match_jmptbl lbllist vaddr size ffw = ) in let elf = ffw.sf.ef.elf in - begin match section_at_vaddr elf vaddr with + begin match bitstring_at_vaddr elf vaddr size with | None -> ERR("No section for the jumptable") - | Some(sndx) -> - begin match bitstring_at_vaddr elf vaddr size with - | None -> ERR("") - | Some(bs, pofs, psize) -> - ffw - >>> (ff_sf ^%= - match_sections_name jmptbl_section elf.e_shdra.(sndx).sh_name - ) - >>> match_jmptbl_aux lbllist bs - >>^ (ff_ef ^%= - add_range pofs psize 0 Jumptable - ) - end + | Some(bs, pofs, psize) -> + ffw + >>> match_jmptbl_aux lbllist bs + >>^ (ff_ef ^%= + add_range pofs psize 0 Jumptable + ) end let match_bo_bt_bool bo = diff --git a/common/AST.v b/common/AST.v index 1c46389e..9c29a374 100644 --- a/common/AST.v +++ b/common/AST.v @@ -201,6 +201,8 @@ Record globvar (V: Type) : Type := mkglobvar { (** Whole programs consist of: - a collection of global definitions (name and description); +- a set of public names (the names that are visible outside + this compilation unit); - the name of the ``main'' function that serves as entry point in the program. A global definition is either a global function or a global variable. @@ -218,6 +220,7 @@ Implicit Arguments Gvar [F V]. Record program (F V: Type) : Type := mkprogram { prog_defs: list (ident * globdef F V); + prog_public: list ident; prog_main: ident }. @@ -244,6 +247,7 @@ Definition transform_program_globdef (idg: ident * globdef A V) : ident * globde Definition transform_program (p: program A V) : program B V := mkprogram (List.map transform_program_globdef p.(prog_defs)) + p.(prog_public) p.(prog_main). Lemma transform_program_function: @@ -295,7 +299,8 @@ Fixpoint transf_globdefs (l: list (ident * globdef A V)) : res (list (ident * gl end. Definition transform_partial_program2 (p: program A V) : res (program B W) := - do gl' <- transf_globdefs p.(prog_defs); OK(mkprogram gl' p.(prog_main)). + do gl' <- transf_globdefs p.(prog_defs); + OK (mkprogram gl' p.(prog_public) p.(prog_main)). Lemma transform_partial_program2_function: forall p tp i tf, @@ -363,6 +368,14 @@ Proof. intros. monadInv H. reflexivity. Qed. +Lemma transform_partial_program2_public: + forall p tp, + transform_partial_program2 p = OK tp -> + tp.(prog_public) = p.(prog_public). +Proof. + intros. monadInv H. reflexivity. +Qed. + (** Additionally, we can also "augment" the program with new global definitions and a different "main" function. *) @@ -373,7 +386,7 @@ Variable new_main: ident. Definition transform_partial_augment_program (p: program A V) : res (program B W) := do gl' <- transf_globdefs p.(prog_defs); - OK(mkprogram (gl' ++ new_globs) new_main). + OK(mkprogram (gl' ++ new_globs) p.(prog_public) new_main). Lemma transform_partial_augment_program_main: forall p tp, @@ -416,6 +429,14 @@ Proof. apply transform_partial_program2_main. Qed. +Lemma transform_partial_program_public: + forall p tp, + transform_partial_program p = OK tp -> + tp.(prog_public) = p.(prog_public). +Proof. + apply transform_partial_program2_public. +Qed. + Lemma transform_partial_program_function: forall p tp i tf, transform_partial_program p = OK tp -> @@ -480,7 +501,8 @@ Definition match_program (new_globs : list (ident * globdef B W)) (p1: program A V) (p2: program B W) : Prop := (exists tglob, list_forall2 match_globdef p1.(prog_defs) tglob /\ p2.(prog_defs) = tglob ++ new_globs) /\ - p2.(prog_main) = new_main. + p2.(prog_main) = new_main /\ + p2.(prog_public) = p1.(prog_public). End MATCH_PROGRAM. @@ -635,6 +657,15 @@ Proof. Defined. Global Opaque external_function_eq. +(** Global variables referenced by an external function *) + +Definition globals_external (ef: external_function) : list ident := + match ef with + | EF_vload_global _ id _ => id :: nil + | EF_vstore_global _ id _ => id :: nil + | _ => nil + end. + (** Function definitions are the union of internal and external functions. *) Inductive fundef (F: Type): Type := diff --git a/common/Events.v b/common/Events.v index 8787a14b..175655be 100644 --- a/common/Events.v +++ b/common/Events.v @@ -276,6 +276,7 @@ Inductive eventval_match: eventval -> typ -> val -> Prop := | ev_match_single: forall f, eventval_match (EVsingle f) Tsingle (Vsingle f) | ev_match_ptr: forall id b ofs, + Genv.public_symbol ge id = true -> Genv.find_symbol ge id = Some b -> eventval_match (EVptr_global id ofs) Tint (Vptr b ofs). @@ -318,45 +319,6 @@ Proof. inv H1. constructor. eapply eventval_match_lessdef; eauto. eauto. Qed. -(** Compatibility with memory injections *) - -Variable f: block -> option (block * Z). - -Definition meminj_preserves_globals : Prop := - (forall id b, Genv.find_symbol ge id = Some b -> f b = Some(b, 0)) - /\ (forall b gv, Genv.find_var_info ge b = Some gv -> f b = Some(b, 0)) - /\ (forall b1 b2 delta gv, Genv.find_var_info ge b2 = Some gv -> f b1 = Some(b2, delta) -> b2 = b1). - -Hypothesis glob_pres: meminj_preserves_globals. - -Lemma eventval_match_inject: - forall ev ty v1 v2, - eventval_match ev ty v1 -> val_inject f v1 v2 -> eventval_match ev ty v2. -Proof. - intros. inv H; inv H0; try constructor; auto. - destruct glob_pres as [A [B C]]. - exploit A; eauto. intro EQ; rewrite H3 in EQ; inv EQ. - rewrite Int.add_zero. econstructor; eauto. -Qed. - -Lemma eventval_match_inject_2: - forall ev ty v, - eventval_match ev ty v -> val_inject f v v. -Proof. - induction 1; auto. - destruct glob_pres as [A [B C]]. - exploit A; eauto. intro EQ. - econstructor; eauto. rewrite Int.add_zero; auto. -Qed. - -Lemma eventval_list_match_inject: - forall evl tyl vl1, eventval_list_match evl tyl vl1 -> - forall vl2, val_list_inject f vl1 vl2 -> eventval_list_match evl tyl vl2. -Proof. - induction 1; intros. inv H; constructor. - inv H1. constructor. eapply eventval_match_inject; eauto. eauto. -Qed. - (** Determinism *) Lemma eventval_match_determ_1: @@ -388,7 +350,7 @@ Definition eventval_valid (ev: eventval) : Prop := | EVlong _ => True | EVfloat _ => True | EVsingle _ => True - | EVptr_global id ofs => exists b, Genv.find_symbol ge id = Some b + | EVptr_global id ofs => Genv.public_symbol ge id = true end. Definition eventval_type (ev: eventval) : typ := @@ -407,19 +369,21 @@ Lemma eventval_match_receptive: exists v2, eventval_match ev2 ty v2. Proof. intros. inv H; destruct ev2; simpl in H2; try discriminate. - exists (Vint i0); constructor. - destruct H1 as [b EQ]. exists (Vptr b i1); constructor; auto. - exists (Vlong i0); constructor. - exists (Vfloat f1); constructor. - exists (Vsingle f1); constructor; auto. - exists (Vint i); constructor. - destruct H1 as [b' EQ]. exists (Vptr b' i0); constructor; auto. +- exists (Vint i0); constructor. +- simpl in H1; exploit Genv.public_symbol_exists; eauto. intros [b FS]. + exists (Vptr b i1); constructor; auto. +- exists (Vlong i0); constructor. +- exists (Vfloat f0); constructor. +- exists (Vsingle f0); constructor; auto. +- exists (Vint i); constructor. +- simpl in H1. exploit Genv.public_symbol_exists. eexact H1. intros [b' FS]. + exists (Vptr b' i0); constructor; auto. Qed. Lemma eventval_match_valid: forall ev ty v, eventval_match ev ty v -> eventval_valid ev. Proof. - destruct 1; simpl; auto. exists b; auto. + destruct 1; simpl; auto. Qed. Lemma eventval_match_same_type: @@ -439,6 +403,15 @@ Variables F1 V1 F2 V2: Type. Variable ge1: Genv.t F1 V1. Variable ge2: Genv.t F2 V2. +Hypothesis public_preserved: + forall id, Genv.public_symbol ge2 id = Genv.public_symbol ge1 id. + +Lemma eventval_valid_preserved: + forall ev, eventval_valid ge1 ev -> eventval_valid ge2 ev. +Proof. + intros. destruct ev; simpl in *; auto. rewrite <- H; auto. +Qed. + Hypothesis symbols_preserved: forall id, Genv.find_symbol ge2 id = Genv.find_symbol ge1 id. @@ -446,7 +419,9 @@ Lemma eventval_match_preserved: forall ev ty v, eventval_match ge1 ev ty v -> eventval_match ge2 ev ty v. Proof. - induction 1; constructor; auto. rewrite symbols_preserved; auto. + induction 1; constructor; auto. + rewrite public_preserved; auto. + rewrite symbols_preserved; auto. Qed. Lemma eventval_list_match_preserved: @@ -456,14 +431,68 @@ Proof. induction 1; constructor; auto. eapply eventval_match_preserved; eauto. Qed. -Lemma eventval_valid_preserved: - forall ev, eventval_valid ge1 ev -> eventval_valid ge2 ev. +End EVENTVAL_INV. + +(** Used for the semantics of volatile memory accesses. Move to [Globalenv] ? *) + +Definition block_is_volatile (F V: Type) (ge: Genv.t F V) (b: block) : bool := + match Genv.find_var_info ge b with + | None => false + | Some gv => gv.(gvar_volatile) + end. + +(** Compatibility with memory injections *) + +Section EVENTVAL_INJECT. + +Variables F1 V1 F2 V2: Type. +Variable f: block -> option (block * Z). +Variable ge1: Genv.t F1 V1. +Variable ge2: Genv.t F2 V2. + +Definition symbols_inject : Prop := + (forall id, Genv.public_symbol ge2 id = Genv.public_symbol ge1 id) +/\ (forall id b1 b2 delta, + f b1 = Some(b2, delta) -> Genv.find_symbol ge1 id = Some b1 -> + delta = 0 /\ Genv.find_symbol ge2 id = Some b2) +/\ (forall id b1, + Genv.public_symbol ge1 id = true -> Genv.find_symbol ge1 id = Some b1 -> + exists b2, f b1 = Some(b2, 0) /\ Genv.find_symbol ge2 id = Some b2) +/\ (forall b1 b2 delta, + f b1 = Some(b2, delta) -> + block_is_volatile ge2 b2 = block_is_volatile ge1 b1). + +Hypothesis symb_inj: symbols_inject. + +Lemma eventval_match_inject: + forall ev ty v1 v2, + eventval_match ge1 ev ty v1 -> val_inject f v1 v2 -> eventval_match ge2 ev ty v2. Proof. - unfold eventval_valid; destruct ev; auto. - intros [b A]. exists b; rewrite symbols_preserved; auto. + intros. inv H; inv H0; try constructor; auto. + destruct symb_inj as (A & B & C & D). exploit C; eauto. intros [b3 [EQ FS]]. rewrite H4 in EQ; inv EQ. + rewrite Int.add_zero. constructor; auto. rewrite A; auto. Qed. -End EVENTVAL_INV. +Lemma eventval_match_inject_2: + forall ev ty v1, + eventval_match ge1 ev ty v1 -> + exists v2, eventval_match ge2 ev ty v2 /\ val_inject f v1 v2. +Proof. + intros. inv H; try (econstructor; split; eauto; constructor; fail). + destruct symb_inj as (A & B & C & D). exploit C; eauto. intros [b2 [EQ FS]]. + exists (Vptr b2 ofs); split. econstructor; eauto. + econstructor; eauto. rewrite Int.add_zero; auto. +Qed. + +Lemma eventval_list_match_inject: + forall evl tyl vl1, eventval_list_match ge1 evl tyl vl1 -> + forall vl2, val_list_inject f vl1 vl2 -> eventval_list_match ge2 evl tyl vl2. +Proof. + induction 1; intros. inv H; constructor. + inv H1. constructor. eapply eventval_match_inject; eauto. eauto. +Qed. + +End EVENTVAL_INJECT. (** * Matching traces. *) @@ -501,8 +530,8 @@ Variables F1 V1 F2 V2: Type. Variable ge1: Genv.t F1 V1. Variable ge2: Genv.t F2 V2. -Hypothesis symbols_preserved: - forall id, Genv.find_symbol ge2 id = Genv.find_symbol ge1 id. +Hypothesis public_preserved: + forall id, Genv.public_symbol ge2 id = Genv.public_symbol ge1 id. Lemma match_traces_preserved: forall t1 t2, match_traces ge1 t1 t2 -> match_traces ge2 t1 t2. @@ -531,12 +560,6 @@ Fixpoint output_trace (t: trace) : Prop := (** * Semantics of volatile memory accesses *) -Definition block_is_volatile (F V: Type) (ge: Genv.t F V) (b: block) : bool := - match Genv.find_var_info ge b with - | None => false - | Some gv => gv.(gvar_volatile) - end. - Inductive volatile_load (F V: Type) (ge: Genv.t F V): memory_chunk -> mem -> block -> int -> trace -> val -> Prop := | volatile_load_vol: forall chunk m b ofs id ev v, @@ -600,7 +623,8 @@ Definition inject_separated (f f': meminj) (m1 m2: mem): Prop := ~Mem.valid_block m1 b1 /\ ~Mem.valid_block m2 b2. Record extcall_properties (sem: extcall_sem) - (sg: signature) : Prop := mk_extcall_properties { + (sg: signature) (free_globals: list ident) : Prop := + mk_extcall_properties { (** The return value of an external call must agree with its signature. *) ec_well_typed: @@ -612,6 +636,7 @@ Record extcall_properties (sem: extcall_sem) ec_symbols_preserved: forall F1 V1 (ge1: Genv.t F1 V1) F2 V2 (ge2: Genv.t F2 V2) vargs m1 t vres m2, (forall id, Genv.find_symbol ge2 id = Genv.find_symbol ge1 id) -> + (forall id, Genv.public_symbol ge2 id = Genv.public_symbol ge1 id) -> (forall b, block_is_volatile ge2 b = block_is_volatile ge1 b) -> sem F1 V1 ge1 vargs m1 t vres m2 -> sem F2 V2 ge2 vargs m1 t vres m2; @@ -653,13 +678,16 @@ Record extcall_properties (sem: extcall_sem) (** External calls must commute with memory injections, in the following sense. *) ec_mem_inject: - forall F V (ge: Genv.t F V) vargs m1 t vres m2 f m1' vargs', - meminj_preserves_globals ge f -> - sem F V ge vargs m1 t vres m2 -> + forall F1 V1 F2 V2 (ge1: Genv.t F1 V1) (ge2: Genv.t F2 V2) vargs m1 t vres m2 f m1' vargs', + symbols_inject f ge1 ge2 -> + (forall id b1, + In id free_globals -> Genv.find_symbol ge1 id = Some b1 -> + exists b2, f b1 = Some(b2, 0) /\ Genv.find_symbol ge2 id = Some b2) -> + sem F1 V1 ge1 vargs m1 t vres m2 -> Mem.inject f m1 m1' -> val_list_inject f vargs vargs' -> exists f', exists vres', exists m2', - sem F V ge vargs' m1' t vres' m2' + sem F2 V2 ge2 vargs' m1' t vres' m2' /\ val_inject f' vres vres' /\ Mem.inject f' m2 m2' /\ Mem.unchanged_on (loc_unmapped f) m1 m2 @@ -696,15 +724,16 @@ Inductive volatile_load_sem (chunk: memory_chunk) (F V: Type) (ge: Genv.t F V): Lemma volatile_load_preserved: forall F1 V1 (ge1: Genv.t F1 V1) F2 V2 (ge2: Genv.t F2 V2) chunk m b ofs t v, (forall id, Genv.find_symbol ge2 id = Genv.find_symbol ge1 id) -> + (forall id, Genv.public_symbol ge2 id = Genv.public_symbol ge1 id) -> (forall b, block_is_volatile ge2 b = block_is_volatile ge1 b) -> volatile_load ge1 chunk m b ofs t v -> volatile_load ge2 chunk m b ofs t v. Proof. - intros. inv H1; constructor; auto. - rewrite H0; auto. + intros. inv H2; constructor; auto. + rewrite H1; auto. rewrite H; auto. eapply eventval_match_preserved; eauto. - rewrite H0; auto. + rewrite H1; auto. Qed. Lemma volatile_load_extends: @@ -718,35 +747,28 @@ Proof. exploit Mem.load_extends; eauto. intros [v' [A B]]. exists v'; split; auto. constructor; auto. Qed. -Remark meminj_preserves_block_is_volatile: - forall F V (ge: Genv.t F V) f b1 b2 delta, - meminj_preserves_globals ge f -> - f b1 = Some (b2, delta) -> - block_is_volatile ge b2 = block_is_volatile ge b1. -Proof. - intros. destruct H as [A [B C]]. unfold block_is_volatile. - case_eq (Genv.find_var_info ge b1); intros. - exploit B; eauto. intro EQ; rewrite H0 in EQ; inv EQ. rewrite H; auto. - case_eq (Genv.find_var_info ge b2); intros. - exploit C; eauto. intro EQ. congruence. - auto. -Qed. - Lemma volatile_load_inject: - forall F V (ge: Genv.t F V) f chunk m b ofs t v b' ofs' m', - meminj_preserves_globals ge f -> - volatile_load ge chunk m b ofs t v -> + forall F1 V1 F2 V2 (ge1: Genv.t F1 V1) (ge2: Genv.t F2 V2) f chunk m b ofs t v b' ofs' m', + symbols_inject f ge1 ge2 -> + volatile_load ge1 chunk m b ofs t v -> val_inject f (Vptr b ofs) (Vptr b' ofs') -> Mem.inject f m m' -> - exists v', volatile_load ge chunk m' b' ofs' t v' /\ val_inject f v v'. -Proof. - intros. inv H0. - inv H1. exploit (proj1 H); eauto. intros EQ; rewrite H8 in EQ; inv EQ. - rewrite Int.add_zero. exists (Val.load_result chunk v0); split. - constructor; auto. - apply val_load_result_inject. eapply eventval_match_inject_2; eauto. - exploit Mem.loadv_inject; eauto. simpl; eauto. simpl; intros [v' [A B]]. exists v'; split; auto. - constructor; auto. rewrite <- H3. inv H1. eapply meminj_preserves_block_is_volatile; eauto. + exists v', volatile_load ge2 chunk m' b' ofs' t v' /\ val_inject f v v'. +Proof. + intros until m'; intros SI VL VI MI. generalize SI; intros (A & B & C & D). + inv VL. +- (* volatile load *) + inv VI. exploit B; eauto. intros [U V]. subst delta. + exploit eventval_match_inject_2; eauto. intros (v2 & X & Y). + rewrite Int.add_zero. exists (Val.load_result chunk v2); split. + constructor; auto. + erewrite D; eauto. + apply val_load_result_inject. auto. +- (* normal load *) + exploit Mem.loadv_inject; eauto. simpl; eauto. simpl; intros (v2 & X & Y). + exists v2; split; auto. + constructor; auto. + inv VI. erewrite D; eauto. Qed. Lemma volatile_load_receptive: @@ -763,14 +785,15 @@ Qed. Lemma volatile_load_ok: forall chunk, extcall_properties (volatile_load_sem chunk) - (mksignature (Tint :: nil) (Some (type_of_chunk chunk)) cc_default). + (mksignature (Tint :: nil) (Some (type_of_chunk chunk)) cc_default) + nil. Proof. intros; constructor; intros. (* well typed *) unfold proj_sig_res; simpl. inv H. inv H0. apply Val.load_result_type. eapply Mem.load_type; eauto. (* symbols *) - inv H1. constructor. eapply volatile_load_preserved; eauto. + inv H2. constructor. eapply volatile_load_preserved; eauto. (* valid blocks *) inv H; auto. (* max perms *) @@ -782,7 +805,7 @@ Proof. exploit volatile_load_extends; eauto. intros [v' [A B]]. exists v'; exists m1'; intuition. constructor; auto. (* mem injects *) - inv H0. inv H2. inv H7. inversion H5; subst. + inv H1. inv H3. inv H8. inversion H6; subst. exploit volatile_load_inject; eauto. intros [v' [A B]]. exists f; exists v'; exists m1'; intuition. constructor; auto. red; intros. congruence. @@ -825,14 +848,15 @@ Qed. Lemma volatile_load_global_ok: forall chunk id ofs, extcall_properties (volatile_load_global_sem chunk id ofs) - (mksignature nil (Some (type_of_chunk chunk)) cc_default). + (mksignature nil (Some (type_of_chunk chunk)) cc_default) + (id :: nil). Proof. intros; constructor; intros. (* well typed *) unfold proj_sig_res; simpl. inv H. inv H1. apply Val.load_result_type. eapply Mem.load_type; eauto. (* symbols *) - inv H1. econstructor. rewrite H; eauto. eapply volatile_load_preserved; eauto. + inv H2. econstructor. rewrite H; eauto. eapply volatile_load_preserved; eauto. (* valid blocks *) inv H; auto. (* max perm *) @@ -843,9 +867,10 @@ Proof. inv H. inv H1. exploit volatile_load_extends; eauto. intros [v' [A B]]. exists v'; exists m1'; intuition. econstructor; eauto. (* inject *) - inv H0. inv H2. - assert (val_inject f (Vptr b ofs) (Vptr b ofs)). - exploit (proj1 H); eauto. intros EQ. econstructor. eauto. rewrite Int.add_zero; auto. + inv H1. inv H3. + exploit H0; eauto with coqlib. intros (b2 & INJ & FS2). + assert (val_inject f (Vptr b ofs) (Vptr b2 ofs)). + econstructor; eauto. rewrite Int.add_zero; auto. exploit volatile_load_inject; eauto. intros [v' [A B]]. exists f; exists v'; exists m1'; intuition. econstructor; eauto. red; intros; congruence. @@ -872,15 +897,16 @@ Inductive volatile_store_sem (chunk: memory_chunk) (F V: Type) (ge: Genv.t F V): Lemma volatile_store_preserved: forall F1 V1 (ge1: Genv.t F1 V1) F2 V2 (ge2: Genv.t F2 V2) chunk m1 b ofs v t m2, (forall id, Genv.find_symbol ge2 id = Genv.find_symbol ge1 id) -> + (forall id, Genv.public_symbol ge2 id = Genv.public_symbol ge1 id) -> (forall b, block_is_volatile ge2 b = block_is_volatile ge1 b) -> volatile_store ge1 chunk m1 b ofs v t m2 -> volatile_store ge2 chunk m1 b ofs v t m2. Proof. - intros. inv H1; constructor; auto. - rewrite H0; auto. + intros. inv H2; constructor; auto. + rewrite H1; auto. rewrite H; auto. eapply eventval_match_preserved; eauto. - rewrite H0; auto. + rewrite H1; auto. Qed. Lemma volatile_store_readonly: @@ -922,38 +948,44 @@ Proof. Qed. Lemma volatile_store_inject: - forall F V (ge: Genv.t F V) f chunk m1 b ofs v t m2 m1' b' ofs' v', - meminj_preserves_globals ge f -> - volatile_store ge chunk m1 b ofs v t m2 -> + forall F1 V1 F2 V2 (ge1: Genv.t F1 V1) (ge2: Genv.t F2 V2) f chunk m1 b ofs v t m2 m1' b' ofs' v', + symbols_inject f ge1 ge2 -> + volatile_store ge1 chunk m1 b ofs v t m2 -> val_inject f (Vptr b ofs) (Vptr b' ofs') -> val_inject f v v' -> Mem.inject f m1 m1' -> exists m2', - volatile_store ge chunk m1' b' ofs' v' t m2' + volatile_store ge2 chunk m1' b' ofs' v' t m2' /\ Mem.inject f m2 m2' /\ Mem.unchanged_on (loc_unmapped f) m1 m2 /\ Mem.unchanged_on (loc_out_of_reach f m1) m1' m2'. Proof. - intros. inv H0. -- inv H1. exploit (proj1 H); eauto. intros EQ; rewrite H9 in EQ; inv EQ. - rewrite Int.add_zero. exists m1'. intuition. - constructor; auto. - eapply eventval_match_inject; eauto. apply val_load_result_inject; auto. -- assert (Mem.storev chunk m1 (Vptr b ofs) v = Some m2). simpl; auto. + intros until v'; intros SI VS AI VI MI. + generalize SI; intros (P & Q & R & S). + inv VS. +- (* volatile store *) + inv AI. exploit Q; eauto. intros [A B]. subst delta. + rewrite Int.add_zero. exists m1'; split. + constructor; auto. erewrite S; eauto. + eapply eventval_match_inject; eauto. apply val_load_result_inject. auto. + intuition auto with mem. +- (* normal store *) + inversion AI; subst. + assert (Mem.storev chunk m1 (Vptr b ofs) v = Some m2). simpl; auto. exploit Mem.storev_mapped_inject; eauto. intros [m2' [A B]]. - inv H1. exists m2'; intuition. -+ constructor; auto. rewrite <- H4. eapply meminj_preserves_block_is_volatile; eauto. + exists m2'; intuition auto. ++ constructor; auto. erewrite S; eauto. + eapply Mem.store_unchanged_on; eauto. - unfold loc_unmapped; intros. congruence. + unfold loc_unmapped; intros. inv AI; congruence. + eapply Mem.store_unchanged_on; eauto. unfold loc_out_of_reach; intros. red; intros. simpl in A. assert (EQ: Int.unsigned (Int.add ofs (Int.repr delta)) = Int.unsigned ofs + delta) by (eapply Mem.address_inject; eauto with mem). rewrite EQ in *. - eelim H6; eauto. - exploit Mem.store_valid_access_3. eexact H5. intros [P Q]. + eelim H3; eauto. + exploit Mem.store_valid_access_3. eexact H0. intros [X Y]. apply Mem.perm_cur_max. apply Mem.perm_implies with Writable; auto with mem. - apply P. omega. + apply X. omega. Qed. Lemma volatile_store_receptive: @@ -966,13 +998,14 @@ Qed. Lemma volatile_store_ok: forall chunk, extcall_properties (volatile_store_sem chunk) - (mksignature (Tint :: type_of_chunk chunk :: nil) None cc_default). + (mksignature (Tint :: type_of_chunk chunk :: nil) None cc_default) + nil. Proof. intros; constructor; intros. (* well typed *) unfold proj_sig_res; simpl. inv H; constructor. (* symbols preserved *) - inv H1. constructor. eapply volatile_store_preserved; eauto. + inv H2. constructor. eapply volatile_store_preserved; eauto. (* valid block *) inv H. inv H1. auto. eauto with mem. (* perms *) @@ -984,7 +1017,7 @@ Proof. exploit volatile_store_extends; eauto. intros [m2' [A [B C]]]. exists Vundef; exists m2'; intuition. constructor; auto. (* mem inject *) - inv H0. inv H2. inv H7. inv H8. inversion H5; subst. + inv H1. inv H3. inv H8. inv H9. inversion H6; subst. exploit volatile_store_inject; eauto. intros [m2' [A [B [C D]]]]. exists f; exists Vundef; exists m2'; intuition. constructor; auto. red; intros; congruence. (* trace length *) @@ -1021,13 +1054,14 @@ Qed. Lemma volatile_store_global_ok: forall chunk id ofs, extcall_properties (volatile_store_global_sem chunk id ofs) - (mksignature (type_of_chunk chunk :: nil) None cc_default). + (mksignature (type_of_chunk chunk :: nil) None cc_default) + (id :: nil). Proof. intros; constructor; intros. (* well typed *) unfold proj_sig_res; simpl. inv H; constructor. (* symbols preserved *) - inv H1. econstructor. rewrite H; eauto. eapply volatile_store_preserved; eauto. + inv H2. econstructor. rewrite H; eauto. eapply volatile_store_preserved; eauto. (* valid block *) inv H. inv H2. auto. eauto with mem. (* perms *) @@ -1040,13 +1074,13 @@ Proof. intros [vres' [m2' [A [B [C D]]]]]. exists vres'; exists m2'; intuition. rewrite volatile_store_global_charact. exists b; auto. (* mem inject *) - rewrite volatile_store_global_charact in H0. destruct H0 as [b [P Q]]. - exploit (proj1 H). eauto. intros EQ. - assert (val_inject f (Vptr b ofs) (Vptr b ofs)). econstructor; eauto. rewrite Int.add_zero; auto. - exploit ec_mem_inject. eapply volatile_store_ok. eauto. eexact Q. eauto. eauto. + rewrite volatile_store_global_charact in H1. destruct H1 as [b [P Q]]. + exploit H0; eauto with coqlib. intros (b2 & INJ & FS2). + assert (val_inject f (Vptr b ofs) (Vptr b2 ofs)). econstructor; eauto. rewrite Int.add_zero; auto. + exploit ec_mem_inject. eapply volatile_store_ok. eauto. intuition. eexact Q. eauto. constructor. eauto. eauto. intros [f' [vres' [m2' [A [B [C [D [E G]]]]]]]]. exists f'; exists vres'; exists m2'; intuition. - rewrite volatile_store_global_charact. exists b; auto. + rewrite volatile_store_global_charact. exists b2; auto. (* trace length *) inv H. inv H1; simpl; omega. (* receptive *) @@ -1069,7 +1103,8 @@ Inductive extcall_malloc_sem (F V: Type) (ge: Genv.t F V): Lemma extcall_malloc_ok: extcall_properties extcall_malloc_sem - (mksignature (Tint :: nil) (Some Tint) cc_default). + (mksignature (Tint :: nil) (Some Tint) cc_default) + nil. Proof. assert (UNCHANGED: forall (P: block -> Z -> Prop) m n m' b m'', @@ -1089,7 +1124,7 @@ Proof. (* well typed *) inv H. unfold proj_sig_res; simpl. auto. (* symbols preserved *) - inv H1; econstructor; eauto. + inv H2; econstructor; eauto. (* valid block *) inv H. eauto with mem. (* perms *) @@ -1109,7 +1144,7 @@ Proof. econstructor; eauto. eapply UNCHANGED; eauto. (* mem injects *) - inv H0. inv H2. inv H6. inv H8. + inv H1. inv H3. inv H7. inv H9. exploit Mem.alloc_parallel_inject; eauto. apply Zle_refl. apply Zle_refl. intros [f' [m3' [b' [ALLOC [A [B [C D]]]]]]]. exploit Mem.store_mapped_inject. eexact A. eauto. eauto. @@ -1121,8 +1156,8 @@ Proof. eapply UNCHANGED; eauto. eapply UNCHANGED; eauto. red; intros. destruct (eq_block b1 b). - subst b1. rewrite C in H2. inv H2. eauto with mem. - rewrite D in H2. congruence. auto. + subst b1. rewrite C in H3. inv H3. eauto with mem. + rewrite D in H3 by auto. congruence. (* trace length *) inv H; simpl; omega. (* receptive *) @@ -1144,13 +1179,14 @@ Inductive extcall_free_sem (F V: Type) (ge: Genv.t F V): Lemma extcall_free_ok: extcall_properties extcall_free_sem - (mksignature (Tint :: nil) None cc_default). + (mksignature (Tint :: nil) None cc_default) + nil. Proof. constructor; intros. (* well typed *) inv H. unfold proj_sig_res. simpl. auto. (* symbols preserved *) - inv H1; econstructor; eauto. + inv H2; econstructor; eauto. (* valid block *) inv H. eauto with mem. (* perms *) @@ -1173,13 +1209,13 @@ Proof. eapply Mem.free_range_perm. eexact H4. eauto. } tauto. (* mem inject *) - inv H0. inv H2. inv H7. inv H9. + inv H1. inv H3. inv H8. inv H10. exploit Mem.load_inject; eauto. intros [vsz [A B]]. inv B. assert (Mem.range_perm m1 b (Int.unsigned lo - 4) (Int.unsigned lo + Int.unsigned sz) Cur Freeable). eapply Mem.free_range_perm; eauto. exploit Mem.address_inject; eauto. apply Mem.perm_implies with Freeable; auto with mem. - apply H0. instantiate (1 := lo). omega. + apply H1. instantiate (1 := lo). omega. intro EQ. exploit Mem.free_parallel_inject; eauto. intros (m2' & C & D). exists f, Vundef, m2'; split. @@ -1191,9 +1227,9 @@ Proof. split. auto. split. eapply Mem.free_unchanged_on; eauto. unfold loc_unmapped. intros; congruence. split. eapply Mem.free_unchanged_on; eauto. unfold loc_out_of_reach. - intros. red; intros. eelim H7; eauto. + intros. red; intros. eelim H8; eauto. apply Mem.perm_cur_max. apply Mem.perm_implies with Freeable; auto with mem. - apply H0. omega. + apply H1. omega. split. auto. red; intros. congruence. (* trace length *) @@ -1221,13 +1257,15 @@ Inductive extcall_memcpy_sem (sz al: Z) (F V: Type) (ge: Genv.t F V): list val - Lemma extcall_memcpy_ok: forall sz al, - extcall_properties (extcall_memcpy_sem sz al) (mksignature (Tint :: Tint :: nil) None cc_default). + extcall_properties (extcall_memcpy_sem sz al) + (mksignature (Tint :: Tint :: nil) None cc_default) + nil. Proof. intros. constructor. - (* return type *) intros. inv H. constructor. - (* change of globalenv *) - intros. inv H1. econstructor; eauto. + intros. inv H2. econstructor; eauto. - (* valid blocks *) intros. inv H. eauto with mem. - (* perms *) @@ -1253,7 +1291,7 @@ Proof. erewrite list_forall2_length; eauto. tauto. - (* injections *) - intros. inv H0. inv H2. inv H14. inv H15. inv H11. inv H12. + intros. inv H1. inv H3. inv H15. inv H16. inv H12. inv H13. destruct (zeq sz 0). + (* special case sz = 0 *) assert (bytes = nil). @@ -1304,7 +1342,7 @@ Proof. split. eapply Mem.storebytes_unchanged_on; eauto. unfold loc_unmapped; intros. congruence. split. eapply Mem.storebytes_unchanged_on; eauto. unfold loc_out_of_reach; intros. red; intros. - eelim H2; eauto. + eelim H3; eauto. apply Mem.perm_cur_max. apply Mem.perm_implies with Writable; auto with mem. eapply Mem.storebytes_range_perm; eauto. erewrite list_forall2_length; eauto. @@ -1340,13 +1378,15 @@ Inductive extcall_annot_sem (text: ident) (targs: list annot_arg) (F V: Type) (g Lemma extcall_annot_ok: forall text targs, - extcall_properties (extcall_annot_sem text targs) (mksignature (annot_args_typ targs) None cc_default). + extcall_properties (extcall_annot_sem text targs) + (mksignature (annot_args_typ targs) None cc_default) + nil. Proof. intros; constructor; intros. (* well typed *) inv H. simpl. auto. (* symbols *) - inv H1. econstructor; eauto. + inv H2. econstructor; eauto. eapply eventval_list_match_preserved; eauto. (* valid blocks *) inv H; auto. @@ -1360,7 +1400,7 @@ Proof. econstructor; eauto. eapply eventval_list_match_lessdef; eauto. (* mem injects *) - inv H0. + inv H1. exists f; exists Vundef; exists m1'; intuition. econstructor; eauto. eapply eventval_list_match_inject; eauto. @@ -1384,13 +1424,15 @@ Inductive extcall_annot_val_sem (text: ident) (targ: typ) (F V: Type) (ge: Genv. Lemma extcall_annot_val_ok: forall text targ, - extcall_properties (extcall_annot_val_sem text targ) (mksignature (targ :: nil) (Some targ) cc_default). + extcall_properties (extcall_annot_val_sem text targ) + (mksignature (targ :: nil) (Some targ) cc_default) + nil. Proof. intros; constructor; intros. (* well typed *) inv H. unfold proj_sig_res; simpl. eapply eventval_match_type; eauto. (* symbols *) - inv H1. econstructor; eauto. + inv H2. econstructor; eauto. eapply eventval_match_preserved; eauto. (* valid blocks *) inv H; auto. @@ -1404,7 +1446,7 @@ Proof. econstructor; eauto. eapply eventval_match_lessdef; eauto. (* mem inject *) - inv H0. inv H2. inv H7. + inv H1. inv H3. inv H8. exists f; exists v'; exists m1'; intuition. econstructor; eauto. eapply eventval_match_inject; eauto. @@ -1429,14 +1471,14 @@ Qed. Parameter external_functions_sem: ident -> signature -> extcall_sem. Axiom external_functions_properties: - forall id sg, extcall_properties (external_functions_sem id sg) sg. + forall id sg, extcall_properties (external_functions_sem id sg) sg nil. (** We treat inline assembly similarly. *) Parameter inline_assembly_sem: ident -> extcall_sem. Axiom inline_assembly_properties: - forall id, extcall_properties (inline_assembly_sem id) (mksignature nil None cc_default). + forall id, extcall_properties (inline_assembly_sem id) (mksignature nil None cc_default) nil. (** ** Combined semantics of external calls *) @@ -1469,9 +1511,9 @@ Definition external_call (ef: external_function): extcall_sem := Theorem external_call_spec: forall ef, - extcall_properties (external_call ef) (ef_sig ef). + extcall_properties (external_call ef) (ef_sig ef) (globals_external ef). Proof. - intros. unfold external_call, ef_sig. destruct ef. + intros. unfold external_call, ef_sig, globals_external; destruct ef. apply external_functions_properties. apply external_functions_properties. apply volatile_load_ok. @@ -1492,7 +1534,7 @@ Definition external_call_valid_block ef := ec_valid_block (external_call_spec ef Definition external_call_max_perm ef := ec_max_perm (external_call_spec ef). Definition external_call_readonly ef := ec_readonly (external_call_spec ef). Definition external_call_mem_extends ef := ec_mem_extends (external_call_spec ef). -Definition external_call_mem_inject ef := ec_mem_inject (external_call_spec ef). +Definition external_call_mem_inject_gen ef := ec_mem_inject (external_call_spec ef). Definition external_call_trace_length ef := ec_trace_length (external_call_spec ef). Definition external_call_receptive ef := ec_receptive (external_call_spec ef). Definition external_call_determ ef := ec_determ (external_call_spec ef). @@ -1503,11 +1545,12 @@ Lemma external_call_symbols_preserved: forall ef F1 F2 V (ge1: Genv.t F1 V) (ge2: Genv.t F2 V) vargs m1 t vres m2, external_call ef ge1 vargs m1 t vres m2 -> (forall id, Genv.find_symbol ge2 id = Genv.find_symbol ge1 id) -> + (forall id, Genv.public_symbol ge2 id = Genv.public_symbol ge1 id) -> (forall b, Genv.find_var_info ge2 b = Genv.find_var_info ge1 b) -> external_call ef ge2 vargs m1 t vres m2. Proof. intros. eapply external_call_symbols_preserved_gen; eauto. - intros. unfold block_is_volatile. rewrite H1. auto. + intros. unfold block_is_volatile. rewrite H2. auto. Qed. Require Import Errors. @@ -1517,6 +1560,7 @@ Lemma external_call_symbols_preserved_2: (ge1: Genv.t F1 V1) (ge2: Genv.t F2 V2) vargs m1 t vres m2, external_call ef ge1 vargs m1 t vres m2 -> (forall id, Genv.find_symbol ge2 id = Genv.find_symbol ge1 id) -> + (forall id, Genv.public_symbol ge2 id = Genv.public_symbol ge1 id) -> (forall b gv1, Genv.find_var_info ge1 b = Some gv1 -> exists gv2, Genv.find_var_info ge2 b = Some gv2 /\ transf_globvar tvar gv1 = OK gv2) -> (forall b gv2, Genv.find_var_info ge2 b = Some gv2 -> @@ -1526,9 +1570,9 @@ Proof. intros. eapply external_call_symbols_preserved_gen; eauto. intros. unfold block_is_volatile. case_eq (Genv.find_var_info ge1 b); intros. - exploit H1; eauto. intros [g2 [A B]]. rewrite A. monadInv B. destruct g; auto. + exploit H2; eauto. intros [g2 [A B]]. rewrite A. monadInv B. destruct g; auto. case_eq (Genv.find_var_info ge2 b); intros. - exploit H2; eauto. intros [g1 [A B]]. congruence. + exploit H3; eauto. intros [g1 [A B]]. congruence. auto. Qed. @@ -1545,6 +1589,40 @@ Proof. unfold Plt, Ple in *; zify; omega. Qed. +(** Special case of [external_call_mem_inject_gen] (for backward compatibility) *) + +Definition meminj_preserves_globals (F V: Type) (ge: Genv.t F V) (f: block -> option (block * Z)) : Prop := + (forall id b, Genv.find_symbol ge id = Some b -> f b = Some(b, 0)) + /\ (forall b gv, Genv.find_var_info ge b = Some gv -> f b = Some(b, 0)) + /\ (forall b1 b2 delta gv, Genv.find_var_info ge b2 = Some gv -> f b1 = Some(b2, delta) -> b2 = b1). + +Lemma external_call_mem_inject: + forall ef F V (ge: Genv.t F V) vargs m1 t vres m2 f m1' vargs', + meminj_preserves_globals ge f -> + external_call ef ge vargs m1 t vres m2 -> + Mem.inject f m1 m1' -> + val_list_inject f vargs vargs' -> + exists f', exists vres', exists m2', + external_call ef ge vargs' m1' t vres' m2' + /\ val_inject f' vres vres' + /\ Mem.inject f' m2 m2' + /\ Mem.unchanged_on (loc_unmapped f) m1 m2 + /\ Mem.unchanged_on (loc_out_of_reach f m1) m1' m2' + /\ inject_incr f f' + /\ inject_separated f f' m1 m1'. +Proof. + intros. destruct H as (A & B & C). eapply external_call_mem_inject_gen; eauto. + repeat split; intros. + + simpl in H3. exploit A; eauto. intros EQ; rewrite EQ in H; inv H. auto. + + simpl in H3. exploit A; eauto. intros EQ; rewrite EQ in H; inv H. auto. + + simpl in H3. exists b1; split; eauto. + + unfold block_is_volatile; simpl. + destruct (Genv.find_var_info ge b1) as [gv1|] eqn:V1. + * exploit B; eauto. intros EQ; rewrite EQ in H; inv H. rewrite V1; auto. + * destruct (Genv.find_var_info ge b2) as [gv2|] eqn:V2; auto. + exploit C; eauto. intros EQ; subst b2. congruence. +Qed. + (** Corollaries of [external_call_determ]. *) Lemma external_call_match_traces: @@ -1658,6 +1736,7 @@ Lemma external_call_symbols_preserved': forall ef F1 F2 V (ge1: Genv.t F1 V) (ge2: Genv.t F2 V) vargs m1 t vres m2, external_call' ef ge1 vargs m1 t vres m2 -> (forall id, Genv.find_symbol ge2 id = Genv.find_symbol ge1 id) -> + (forall id, Genv.public_symbol ge2 id = Genv.public_symbol ge1 id) -> (forall b, Genv.find_var_info ge2 b = Genv.find_var_info ge1 b) -> external_call' ef ge2 vargs m1 t vres m2. Proof. diff --git a/common/Globalenvs.v b/common/Globalenvs.v index e4772e25..eb98e876 100644 --- a/common/Globalenvs.v +++ b/common/Globalenvs.v @@ -82,6 +82,7 @@ Variable V: Type. (**r The type of information attached to variables *) (** The type of global environments. *) Record t: Type := mkgenv { + genv_public: list ident; (**r which symbol names are public *) genv_symb: PTree.t block; (**r mapping symbol -> block *) genv_funs: PTree.t F; (**r mapping function pointer -> definition *) genv_vars: PTree.t (globvar V); (**r mapping variable pointer -> info *) @@ -112,6 +113,14 @@ Definition symbol_address (ge: t) (id: ident) (ofs: int) : val := | None => Vundef end. +(** [public_symbol ge id] says whether the name [id] is public and defined. *) + +Definition public_symbol (ge: t) (id: ident) : bool := + match find_symbol ge id with + | None => false + | Some _ => In_dec ident_eq id ge.(genv_public) + end. + (** [find_funct_ptr ge b] returns the function description associated with the given address. *) @@ -144,6 +153,7 @@ Definition find_var_info (ge: t) (b: block) : option (globvar V) := Program Definition add_global (ge: t) (idg: ident * globdef F V) : t := @mkgenv + ge.(genv_public) (PTree.set idg#1 ge.(genv_next) ge.(genv_symb)) (match idg#2 with | Gfun f => PTree.set ge.(genv_next) f ge.(genv_funs) @@ -208,8 +218,8 @@ Proof. induction gl1; simpl; intros. auto. rewrite IHgl1; auto. Qed. -Program Definition empty_genv : t := - @mkgenv (PTree.empty _) (PTree.empty _) (PTree.empty _) 1%positive _ _ _ _ _. +Program Definition empty_genv (pub: list ident): t := + @mkgenv pub (PTree.empty _) (PTree.empty _) (PTree.empty _) 1%positive _ _ _ _ _. Next Obligation. rewrite PTree.gempty in H. discriminate. Qed. @@ -227,7 +237,7 @@ Next Obligation. Qed. Definition globalenv (p: program F V) := - add_globals empty_genv p.(prog_defs). + add_globals (empty_genv p.(prog_public)) p.(prog_defs). (** Proof principles *) @@ -277,6 +287,14 @@ End GLOBALENV_PRINCIPLES. (** ** Properties of the operations over global environments *) +Theorem public_symbol_exists: + forall ge id, public_symbol ge id = true -> exists b, find_symbol ge id = Some b. +Proof. + unfold public_symbol; intros. destruct (find_symbol ge id) as [b|]. + exists b; auto. + discriminate. +Qed. + Theorem shift_symbol_address: forall ge id ofs n, symbol_address ge id (Int.add ofs n) = Val.add (symbol_address ge id ofs) (Vint n). @@ -486,6 +504,21 @@ Proof. rewrite IHgl. auto. Qed. +Remark genv_public_add_globals: + forall gl ge, + genv_public (add_globals ge gl) = genv_public ge. +Proof. + induction gl; simpl; intros. + auto. + rewrite IHgl; auto. +Qed. + +Theorem globalenv_public: + forall p, genv_public (globalenv p) = prog_public p. +Proof. + unfold globalenv; intros. rewrite genv_public_add_globals. auto. +Qed. + (** * Construction of the initial memory state *) Section INITMEM. @@ -1092,7 +1125,7 @@ Lemma init_mem_genv_next: forall p m, Proof. unfold init_mem; intros. exploit alloc_globals_nextblock; eauto. rewrite Mem.nextblock_empty. intro. - generalize (genv_next_add_globals (prog_defs p) empty_genv). + generalize (genv_next_add_globals (prog_defs p) (empty_genv (prog_public p))). fold (globalenv p). simpl genv_next. intros. congruence. Qed. @@ -1606,6 +1639,17 @@ Proof. intros. destruct globalenvs_match. unfold find_symbol. auto. Qed. +Theorem public_symbol_match: + forall (s : ident), + ~In s (map fst new_globs) -> + public_symbol (globalenv p') s = public_symbol (globalenv p) s. +Proof. + intros. unfold public_symbol. rewrite find_symbol_match by auto. + destruct (find_symbol (globalenv p) s); auto. + rewrite ! globalenv_public. + destruct progmatch as (P & Q & R). rewrite R. auto. +Qed. + Hypothesis new_ids_fresh : forall s', find_symbol (globalenv p) s' <> None -> ~In s' (map fst new_globs). @@ -1804,6 +1848,14 @@ Proof. intros. eapply find_symbol_match. eexact prog_match. auto. Qed. +Theorem public_symbol_transf_augment: + forall (s: ident), + ~ In s (map fst new_globs) -> + public_symbol (globalenv p') s = public_symbol (globalenv p) s. +Proof. + intros. eapply public_symbol_match. eexact prog_match. auto. +Qed. + Theorem init_mem_transf_augment: (forall s', find_symbol (globalenv p) s' <> None -> ~ In s' (map fst new_globs)) -> @@ -1910,6 +1962,14 @@ Proof. auto. Qed. +Theorem public_symbol_transf_partial2: + forall (s: ident), + public_symbol (globalenv p') s = public_symbol (globalenv p) s. +Proof. + pose proof (@public_symbol_transf_augment _ _ _ _ _ _ _ _ _ _ transf_augment_OK). + auto. +Qed. + Theorem init_mem_transf_partial2: forall m, init_mem p = Some m -> init_mem p' = Some m. Proof. @@ -1968,6 +2028,13 @@ Proof. exact (@find_symbol_transf_partial2 _ _ _ _ _ _ _ _ transf_OK). Qed. +Theorem public_symbol_transf_partial: + forall (s: ident), + public_symbol (globalenv p') s = public_symbol (globalenv p) s. +Proof. + exact (@public_symbol_transf_partial2 _ _ _ _ _ _ _ _ transf_OK). +Qed. + Theorem find_var_info_transf_partial: forall (b: block), find_var_info (globalenv p') b = find_var_info (globalenv p) b. @@ -2047,6 +2114,13 @@ Proof. exact (@find_symbol_transf_partial _ _ _ _ _ _ transf_OK). Qed. +Theorem public_symbol_transf: + forall (s: ident), + public_symbol (globalenv tp) s = public_symbol (globalenv p) s. +Proof. + exact (@public_symbol_transf_partial _ _ _ _ _ _ transf_OK). +Qed. + Theorem find_var_info_transf: forall (b: block), find_var_info (globalenv tp) b = find_var_info (globalenv p) b. diff --git a/common/Sections.ml b/common/Sections.ml index d7ae8195..c6d4c4c2 100644 --- a/common/Sections.ml +++ b/common/Sections.ml @@ -21,8 +21,8 @@ type section_name = | Section_text | Section_data of bool (* true = init data, false = uninit data *) | Section_small_data of bool - | Section_const - | Section_small_const + | Section_const of bool + | Section_small_const of bool | Section_string | Section_literal | Section_jumptable @@ -68,13 +68,13 @@ let builtin_sections = [ sec_writable = true; sec_executable = false; sec_access = Access_near}; "CONST", - {sec_name_init = Section_const; - sec_name_uninit = Section_const; + {sec_name_init = Section_const true; + sec_name_uninit = Section_const false; sec_writable = false; sec_executable = false; sec_access = Access_default}; "SCONST", - {sec_name_init = Section_small_const; - sec_name_uninit = Section_small_const; + {sec_name_init = Section_small_const true; + sec_name_uninit = Section_small_const false; sec_writable = false; sec_executable = false; sec_access = Access_near}; "STRING", diff --git a/common/Sections.mli b/common/Sections.mli index ff6c8c95..38b99db0 100644 --- a/common/Sections.mli +++ b/common/Sections.mli @@ -20,8 +20,8 @@ type section_name = | Section_text | Section_data of bool (* true = init data, false = uninit data *) | Section_small_data of bool - | Section_const - | Section_small_const + | Section_const of bool + | Section_small_const of bool | Section_string | Section_literal | Section_jumptable diff --git a/common/Smallstep.v b/common/Smallstep.v index 02b18fc8..e74101b5 100644 --- a/common/Smallstep.v +++ b/common/Smallstep.v @@ -516,8 +516,8 @@ Record forward_simulation (L1 L2: semantics) : Type := exists i', exists s2', (Plus L2 s2 t s2' \/ (Star L2 s2 t s2' /\ fsim_order i' i)) /\ fsim_match_states i' s1' s2'; - fsim_symbols_preserved: - forall id, Genv.find_symbol (globalenv L2) id = Genv.find_symbol (globalenv L1) id + fsim_public_preserved: + forall id, Genv.public_symbol (globalenv L2) id = Genv.public_symbol (globalenv L1) id }. Implicit Arguments forward_simulation []. @@ -548,8 +548,8 @@ Section FORWARD_SIMU_DIAGRAMS. Variable L1: semantics. Variable L2: semantics. -Hypothesis symbols_preserved: - forall id, Genv.find_symbol (globalenv L2) id = Genv.find_symbol (globalenv L1) id. +Hypothesis public_preserved: + forall id, Genv.public_symbol (globalenv L2) id = Genv.public_symbol (globalenv L1) id. Variable match_states: state L1 -> state L2 -> Prop. @@ -809,7 +809,7 @@ Proof. right; split. subst t; apply star_refl. red. right. auto. exists s3; auto. (* symbols *) - intros. transitivity (Genv.find_symbol (globalenv L2) id); apply fsim_symbols_preserved; auto. + intros. transitivity (Genv.public_symbol (globalenv L2) id); apply fsim_public_preserved; auto. Qed. End COMPOSE_SIMULATIONS. @@ -927,8 +927,8 @@ Record backward_simulation (L1 L2: semantics) : Type := exists i', exists s1', (Plus L1 s1 t s1' \/ (Star L1 s1 t s1' /\ bsim_order i' i)) /\ bsim_match_states i' s1' s2'; - bsim_symbols_preserved: - forall id, Genv.find_symbol (globalenv L2) id = Genv.find_symbol (globalenv L1) id + bsim_public_preserved: + forall id, Genv.public_symbol (globalenv L2) id = Genv.public_symbol (globalenv L1) id }. (** An alternate form of the simulation diagram *) @@ -957,8 +957,8 @@ Section BACKWARD_SIMU_DIAGRAMS. Variable L1: semantics. Variable L2: semantics. -Hypothesis symbols_preserved: - forall id, Genv.find_symbol (globalenv L2) id = Genv.find_symbol (globalenv L1) id. +Hypothesis public_preserved: + forall id, Genv.public_symbol (globalenv L2) id = Genv.public_symbol (globalenv L1) id. Variable match_states: state L1 -> state L2 -> Prop. @@ -1201,7 +1201,7 @@ Proof. (* simulation *) exact bb_simulation. (* symbols *) - intros. transitivity (Genv.find_symbol (globalenv L2) id); apply bsim_symbols_preserved; auto. + intros. transitivity (Genv.public_symbol (globalenv L2) id); apply bsim_public_preserved; auto. Qed. End COMPOSE_BACKWARD_SIMULATIONS. @@ -1298,7 +1298,7 @@ Proof. subst. inv H1. elim H2; auto. right; intuition. eapply match_traces_preserved with (ge1 := (globalenv L2)); auto. - intros; symmetry; apply (fsim_symbols_preserved FS). + intros; symmetry; apply (fsim_public_preserved FS). Qed. Lemma f2b_determinacy_star: @@ -1492,7 +1492,7 @@ Proof. (* simulation *) exact f2b_simulation_step. (* symbols preserved *) - exact (fsim_symbols_preserved FS). + exact (fsim_public_preserved FS). Qed. End FORWARD_TO_BACKWARD. @@ -1614,7 +1614,7 @@ Proof. (* simulation *) exact ffs_simulation. (* symbols preserved *) - simpl. exact (fsim_symbols_preserved sim). + simpl. exact (fsim_public_preserved sim). Qed. End FACTOR_FORWARD_SIMULATION. @@ -1711,7 +1711,7 @@ Proof. (* simulation *) exact fbs_simulation. (* symbols *) - simpl. exact (bsim_symbols_preserved sim). + simpl. exact (bsim_public_preserved sim). Qed. End FACTOR_BACKWARD_SIMULATION. @@ -154,7 +154,7 @@ case "$target" in abi="standard" system="macosx" cc="${toolprefix}gcc -arch i386" - cprepro="${toolprefix}gcc -arch i386 -U__GNUC__ -U__clang__ -U__BLOCKS__ '-D__attribute__(x)=' -E" + cprepro="${toolprefix}gcc -arch i386 -U__GNUC__ -U__clang__ -U__BLOCKS__ '-D__attribute__(x)=' '-D__asm(x)=' -E" casm="${toolprefix}gcc -arch i386 -c" case `uname -r` in [1-9].*|10.*|11.*) # up to MacOS 10.7 included diff --git a/cparser/Elab.ml b/cparser/Elab.ml index c4057e63..43a72a0e 100644 --- a/cparser/Elab.ml +++ b/cparser/Elab.ml @@ -1770,18 +1770,13 @@ let enter_decdefs local loc env sto dl = if sto <> Storage_default && dl = [] then warning loc "Storage class specifier on empty declaration"; let rec enter_decdef (decls, env) (s, ty, init) = + let isfun = is_function_type env ty in if sto = Storage_extern && init <> NO_INIT then error loc "'extern' declaration cannot have an initializer"; - (* Adjust storage for function declarations *) - let sto1 = - match unroll env ty, sto with - | TFun _, Storage_default -> - Storage_extern - | TFun _, (Storage_static | Storage_register) -> - if local then error loc "invalid storage class for '%s'" s; - sto - | _, _ -> - sto in + if local && isfun && (sto = Storage_static || sto = Storage_register) then + error loc "invalid storage class for '%s'" s; + (* Local function declarations are always treated as extern *) + let sto1 = if local && isfun then Storage_extern else sto in (* enter ident in environment with declared type, because initializer can refer to the ident *) let (id, sto', env1) = enter_or_refine_ident local loc env s sto1 ty in @@ -1791,10 +1786,10 @@ let enter_decdefs local loc env sto dl = let env2 = Env.add_ident env1 id sto' ty' in (* check for incomplete type *) if local && sto' <> Storage_extern - && not (is_function_type env ty') + && not isfun && wrap incomplete_type loc env ty' then error loc "'%s' has incomplete type" s; - if local && sto' <> Storage_extern && sto' <> Storage_static then + if local && not isfun && sto' <> Storage_extern && sto' <> Storage_static then (* Local definition *) ((sto', id, ty', init') :: decls, env2) else begin diff --git a/driver/Compiler.v b/driver/Compiler.v index fb813c7c..0afa7bfb 100644 --- a/driver/Compiler.v +++ b/driver/Compiler.v @@ -46,6 +46,7 @@ Require Renumber. Require Constprop. Require CSE. Require Deadcode. +Require Unusedglob. Require Allocation. Require Tunneling. Require Linearize. @@ -65,6 +66,7 @@ Require Renumberproof. Require Constpropproof. Require CSEproof. Require Deadcodeproof. +Require Unusedglobproof. Require Allocproof. Require Tunnelingproof. Require Linearizeproof. @@ -135,6 +137,8 @@ Definition transf_rtl_program (f: RTL.program) : res Asm.program := @@ print (print_RTL 6) @@@ partial_if Compopts.optim_redundancy (time "Redundancy elimination" Deadcode.transf_program) @@ print (print_RTL 7) + @@@ time "Unused globals" Unusedglob.transform_program + @@ print (print_RTL 8) @@@ time "Register allocation" Allocation.transf_program @@ print print_LTL @@ time "Branch tunneling" Tunneling.tunnel_program @@ -244,7 +248,8 @@ Proof. set (p21 := total_if optim_constprop Renumber.transf_program p2) in *. destruct (partial_if optim_CSE CSE.transf_program p21) as [p3|] eqn:?; simpl in H; try discriminate. destruct (partial_if optim_redundancy Deadcode.transf_program p3) as [p31|] eqn:?; simpl in H; try discriminate. - destruct (Allocation.transf_program p31) as [p4|] eqn:?; simpl in H; try discriminate. + destruct (Unusedglob.transform_program p31) as [p32|] eqn:?; simpl in H; try discriminate. + destruct (Allocation.transf_program p32) as [p4|] eqn:?; simpl in H; try discriminate. set (p5 := Tunneling.tunnel_program p4) in *. destruct (Linearize.transf_program p5) as [p6|] eqn:?; simpl in H; try discriminate. set (p7 := CleanupLabels.transf_program p6) in *. @@ -263,6 +268,8 @@ Proof. eapply partial_if_simulation; eauto. apply CSEproof.transf_program_correct. apply compose_forward_simulation with (RTL.semantics p31). eapply partial_if_simulation; eauto. apply Deadcodeproof.transf_program_correct. + apply compose_forward_simulation with (RTL.semantics p32). + apply Unusedglobproof.transf_program_correct; auto. apply compose_forward_simulation with (LTL.semantics p4). apply Allocproof.transf_program_correct; auto. apply compose_forward_simulation with (LTL.semantics p5). diff --git a/driver/Configuration.ml b/driver/Configuration.ml index 1956b151..e73125f7 100644 --- a/driver/Configuration.ml +++ b/driver/Configuration.ml @@ -23,7 +23,7 @@ let _ = open_in env_file with Not_found -> let dir = Sys.getcwd () - and name = Sys.argv.(0) in + and name = Sys.executable_name in let dirname = if Filename.is_relative name then Filename.dirname (Filename.concat dir name) else @@ -58,8 +58,6 @@ let get_config key = let bad_config key v = Printf.eprintf "Invalid value `%s' for configuation option `%s'\n" v key; exit 2 -let stdlib_path = get_config "stdlib_path" - let prepro = get_config "prepro" let asm = get_config "asm" let linker = get_config "linker" @@ -81,6 +79,13 @@ let has_runtime_lib = | "false" -> false | v -> bad_config "has_runtime_lib" v + +let stdlib_path = + if has_runtime_lib then + get_config "stdlib_path" + else + "" + let asm_supports_cfi = match get_config "asm_supports_cfi" with | "true" -> true diff --git a/driver/Driver.ml b/driver/Driver.ml index 76509f41..fec87420 100644 --- a/driver/Driver.ml +++ b/driver/Driver.ml @@ -150,7 +150,7 @@ let compile_c_ast sourcename csyntax ofile = let asm = match Compiler.transf_c_program csyntax with | Errors.OK asm -> - Asmexpand.expand_program (Unusedglob.transf_program asm) + Asmexpand.expand_program asm | Errors.Error msg -> print_error stderr msg; exit 2 in diff --git a/driver/Interp.ml b/driver/Interp.ml index e277ebe0..9bb9d237 100644 --- a/driver/Interp.ml +++ b/driver/Interp.ml @@ -380,13 +380,33 @@ let do_printf m fmt args = let (>>=) opt f = match opt with None -> None | Some arg -> f arg +(* Like eventval_of_val, but accepts static globals as well *) + +let convert_external_arg ge v t = + match v, t with + | Vint i, AST.Tint -> Some (EVint i) + | Vfloat f, AST.Tfloat -> Some (EVfloat f) + | Vsingle f, AST.Tsingle -> Some (EVsingle f) + | Vlong n, AST.Tlong -> Some (EVlong n) + | Vptr(b, ofs), AST.Tint -> + Genv.invert_symbol ge b >>= fun id -> Some (EVptr_global(id, ofs)) + | _, _ -> None + +let rec convert_external_args ge vl tl = + match vl, tl with + | [], [] -> Some [] + | v1::vl, t1::tl -> + convert_external_arg ge v1 t1 >>= fun e1 -> + convert_external_args ge vl tl >>= fun el -> Some (e1 :: el) + | _, _ -> None + let do_external_function id sg ge w args m = match extern_atom id, args with | "printf", Vptr(b, ofs) :: args' -> extract_string m b ofs >>= fun fmt -> print_string (do_printf m fmt args'); flush stdout; - Cexec.list_eventval_of_val ge args sg.sig_args >>= fun eargs -> + convert_external_args ge args sg.sig_args >>= fun eargs -> Some(((w, [Event_syscall(id, eargs, EVint Int.zero)]), Vint Int.zero), m) | _ -> None @@ -612,7 +632,8 @@ let change_main_function p old_main old_main_ty = fn_params = []; fn_vars = []; fn_body = body } in let new_main_id = intern_string "___main" in { prog_main = new_main_id; - prog_defs = (new_main_id, Gfun(Internal new_main_fn)) :: p.prog_defs } + prog_defs = (new_main_id, Gfun(Internal new_main_fn)) :: p.prog_defs; + prog_public = p.prog_public } let rec find_main_function name = function | [] -> None diff --git a/ia32/Asmgenproof.v b/ia32/Asmgenproof.v index eba710a1..57d7de4a 100644 --- a/ia32/Asmgenproof.v +++ b/ia32/Asmgenproof.v @@ -48,6 +48,14 @@ Proof. exact TRANSF. Qed. +Lemma public_preserved: + forall id, Genv.public_symbol tge id = Genv.public_symbol ge id. +Proof. + intros. unfold ge, tge. + apply Genv.public_symbol_transf_partial with transf_fundef. + exact TRANSF. +Qed. + Lemma functions_translated: forall b f, Genv.find_funct_ptr ge b = Some f -> @@ -672,7 +680,7 @@ Opaque loadind. eapply exec_step_builtin. eauto. eauto. eapply find_instr_tail; eauto. eapply external_call_symbols_preserved'; eauto. - exact symbols_preserved. exact varinfo_preserved. + exact symbols_preserved. exact public_preserved. exact varinfo_preserved. eauto. econstructor; eauto. instantiate (2 := tf); instantiate (1 := x). @@ -699,7 +707,7 @@ Opaque loadind. eapply exec_step_annot. eauto. eauto. eapply find_instr_tail; eauto. eauto. eapply external_call_symbols_preserved'; eauto. - exact symbols_preserved. exact varinfo_preserved. + exact symbols_preserved. exact public_preserved. exact varinfo_preserved. eapply match_states_intro with (ep := false); eauto with coqlib. unfold nextinstr. rewrite Pregmap.gss. rewrite <- H1; simpl. econstructor; eauto. @@ -876,7 +884,7 @@ Transparent destroyed_at_function_entry. left; econstructor; split. apply plus_one. eapply exec_step_external; eauto. eapply external_call_symbols_preserved'; eauto. - exact symbols_preserved. exact varinfo_preserved. + exact symbols_preserved. exact public_preserved. exact varinfo_preserved. econstructor; eauto. unfold loc_external_result. apply agree_set_other; auto. apply agree_set_mregs; auto. @@ -920,7 +928,7 @@ Theorem transf_program_correct: forward_simulation (Mach.semantics return_address_offset prog) (Asm.semantics tprog). Proof. eapply forward_simulation_star with (measure := measure). - eexact symbols_preserved. + eexact public_preserved. eexact transf_initial_states. eexact transf_final_states. exact step_simulation. @@ -659,6 +659,23 @@ Proof. destruct c; simpl; try congruence. reflexivity. Qed. +(** Global variables mentioned in an operation or addressing mode *) + +Definition globals_addressing (addr: addressing) : list ident := + match addr with + | Aglobal s n => s :: nil + | Abased s n => s :: nil + | Abasedscaled sc s n => s :: nil + | _ => nil + end. + +Definition globals_operation (op: operation) : list ident := + match op with + | Oindirectsymbol s => s :: nil + | Olea addr => globals_addressing addr + | _ => nil + end. + (** * Invariance and compatibility properties. *) (** [eval_operation] and [eval_addressing] depend on a global environment @@ -699,14 +716,11 @@ End GENV_TRANSF. Section EVAL_COMPAT. -Variable F V: Type. -Variable genv: Genv.t F V. +Variable F1 F2 V1 V2: Type. +Variable ge1: Genv.t F1 V1. +Variable ge2: Genv.t F2 V2. Variable f: meminj. -Hypothesis symbol_address_inj: - forall id ofs, - val_inject f (Genv.symbol_address genv id ofs) (Genv.symbol_address genv id ofs). - Variable m1: mem. Variable m2: mem. @@ -781,29 +795,37 @@ Ltac TrivialExists := Lemma eval_addressing_inj: forall addr sp1 vl1 sp2 vl2 v1, + (forall id ofs, + In id (globals_addressing addr) -> + val_inject f (Genv.symbol_address ge1 id ofs) (Genv.symbol_address ge2 id ofs)) -> val_inject f sp1 sp2 -> val_list_inject f vl1 vl2 -> - eval_addressing genv sp1 addr vl1 = Some v1 -> - exists v2, eval_addressing genv sp2 addr vl2 = Some v2 /\ val_inject f v1 v2. + eval_addressing ge1 sp1 addr vl1 = Some v1 -> + exists v2, eval_addressing ge2 sp2 addr vl2 = Some v2 /\ val_inject f v1 v2. Proof. - intros. destruct addr; simpl in H1; simpl; FuncInv; InvInject; TrivialExists. + intros. destruct addr; simpl in H2; simpl; FuncInv; InvInject; TrivialExists. apply Values.val_add_inject; auto. apply Values.val_add_inject; auto. apply Values.val_add_inject; auto. - apply Values.val_add_inject; auto. inv H4; simpl; auto. - apply Values.val_add_inject; auto. apply Values.val_add_inject; auto. inv H2; simpl; auto. - apply Values.val_add_inject; auto. - apply Values.val_add_inject; auto. inv H4; simpl; auto. + apply Values.val_add_inject; auto. inv H5; simpl; auto. + apply Values.val_add_inject; auto. apply Values.val_add_inject; auto. inv H3; simpl; auto. + apply H; simpl; auto. + apply Values.val_add_inject; auto. apply H; simpl; auto. + apply Values.val_add_inject; auto. apply H; simpl; auto. inv H5; simpl; auto. apply Values.val_add_inject; auto. Qed. Lemma eval_operation_inj: forall op sp1 vl1 sp2 vl2 v1, + (forall id ofs, + In id (globals_operation op) -> + val_inject f (Genv.symbol_address ge1 id ofs) (Genv.symbol_address ge2 id ofs)) -> val_inject f sp1 sp2 -> val_list_inject f vl1 vl2 -> - eval_operation genv sp1 op vl1 m1 = Some v1 -> - exists v2, eval_operation genv sp2 op vl2 m2 = Some v2 /\ val_inject f v1 v2. + eval_operation ge1 sp1 op vl1 m1 = Some v1 -> + exists v2, eval_operation ge2 sp2 op vl2 m2 = Some v2 /\ val_inject f v1 v2. Proof. - intros. destruct op; simpl in H1; simpl; FuncInv; InvInject; TrivialExists. + intros until v1; intros GL; intros. destruct op; simpl in H1; simpl; FuncInv; InvInject; TrivialExists. + apply GL; simpl; auto. inv H4; simpl; auto. inv H4; simpl; auto. inv H4; simpl; auto. @@ -951,13 +973,14 @@ Proof. eval_operation genv sp op vl2 m2 = Some v2 /\ val_inject (fun b => Some(b, 0)) v1 v2). eapply eval_operation_inj with (m1 := m1) (sp1 := sp). - intros. rewrite <- val_inject_lessdef; auto. apply valid_pointer_extends; auto. apply weak_valid_pointer_extends; auto. apply weak_valid_pointer_no_overflow_extends. apply valid_different_pointers_extends; auto. - rewrite <- val_inject_lessdef; auto. - eauto. auto. + intros. apply val_inject_lessdef. auto. + apply val_inject_lessdef; auto. + eauto. + auto. destruct H2 as [v2 [A B]]. exists v2; split; auto. rewrite val_inject_lessdef; auto. Qed. @@ -1026,7 +1049,7 @@ Proof. intros. rewrite eval_shift_stack_addressing. simpl. eapply eval_addressing_inj with (sp1 := Vptr sp1 Int.zero); eauto. - exact symbol_address_inject. + intros. apply symbol_address_inject. Qed. Lemma eval_operation_inject: @@ -1041,11 +1064,11 @@ Proof. intros. rewrite eval_shift_stack_operation. simpl. eapply eval_operation_inj with (sp1 := Vptr sp1 Int.zero) (m1 := m1); eauto. - exact symbol_address_inject. intros; eapply Mem.valid_pointer_inject_val; eauto. intros; eapply Mem.weak_valid_pointer_inject_val; eauto. intros; eapply Mem.weak_valid_pointer_inject_no_overflow; eauto. intros; eapply Mem.different_pointers_inject; eauto. + intros. apply symbol_address_inject. Qed. End EVAL_INJECT. diff --git a/ia32/PrintAsm.ml b/ia32/PrintAsm.ml index 5c84af6b..649fd292 100644 --- a/ia32/PrintAsm.ml +++ b/ia32/PrintAsm.ml @@ -57,7 +57,7 @@ let preg oc = function (* System dependend printer functions *) -module type SYSTEM= +module type SYSTEM = sig val raw_symbol: out_channel -> string -> unit val symbol: out_channel -> P.t -> unit @@ -69,6 +69,8 @@ module type SYSTEM= val print_fun_info: out_channel -> P.t -> unit val print_var_info: out_channel -> P.t -> unit val print_epilogue: out_channel -> unit + val print_comm_decl: out_channel -> P.t -> Z.t -> int -> unit + val print_lcomm_decl: out_channel -> P.t -> Z.t -> int -> unit end (* Printer functions for cygwin *) @@ -86,8 +88,10 @@ module Cygwin_System = let name_of_section = function | Section_text -> ".text" - | Section_data _ | Section_small_data _ -> ".data" - | Section_const | Section_small_const -> ".section .rdata,\"dr\"" + | Section_data i | Section_small_data i -> + if i then ".data" else "COMM" + | Section_const i | Section_small_const i -> + if i then ".section .rdata,\"dr\"" else "COMM" | Section_string -> ".section .rdata,\"dr\"" | Section_literal -> ".section .rdata,\"dr\"" | Section_jumptable -> ".text" @@ -108,6 +112,14 @@ module Cygwin_System = let print_var_info _ _ = () let print_epilogue _ = () + + let print_comm_decl oc name sz al = + fprintf oc " .comm %a, %s, %d\n" symbol name (Z.to_string sz) al + + let print_lcomm_decl oc name sz al = + fprintf oc " .local %a\n" symbol name; + print_comm_decl oc name sz al + end:SYSTEM) (* Printer functions for ELF *) @@ -125,8 +137,10 @@ module ELF_System = let name_of_section = function | Section_text -> ".text" - | Section_data i | Section_small_data i -> if i then ".data" else "COMM" - | Section_const | Section_small_const -> ".section .rodata" + | Section_data i | Section_small_data i -> + if i then ".data" else "COMM" + | Section_const i | Section_small_const i -> + if i then ".section .rodata" else "COMM" | Section_string -> ".section .rodata" | Section_literal -> ".section .rodata.cst8,\"aM\",@progbits,8" | Section_jumptable -> ".text" @@ -151,6 +165,14 @@ module ELF_System = fprintf oc " .size %a, . - %a\n" symbol name symbol name let print_epilogue _ = () + + let print_comm_decl oc name sz al = + fprintf oc " .comm %a, %s, %d\n" symbol name (Z.to_string sz) al + + let print_lcomm_decl oc name sz al = + fprintf oc " .local %a\n" symbol name; + print_comm_decl oc name sz al + end:SYSTEM) (* Printer functions for MacOS *) @@ -161,15 +183,17 @@ module MacOS_System = fprintf oc "_%s" s let symbol oc symb = - fprintf oc "%s" (extern_atom symb) + fprintf oc "_%s" (extern_atom symb) let label oc lbl = fprintf oc "L%d" lbl let name_of_section = function | Section_text -> ".text" - | Section_data _ | Section_small_data _ -> ".data" - | Section_const | Section_small_const -> ".const" + | Section_data i | Section_small_data i -> + if i then ".data" else "COMM" + | Section_const i | Section_small_const i -> + if i then ".const" else "COMM" | Section_string -> ".const" | Section_literal -> ".literal8" | Section_jumptable -> ".const" @@ -206,7 +230,16 @@ module MacOS_System = fprintf oc "L%a$non_lazy_ptr:\n" raw_symbol s; fprintf oc " .indirect_symbol %a\n" raw_symbol s; fprintf oc " .long 0\n") - !indirect_symbols + !indirect_symbols; + indirect_symbols := StringSet.empty + + let print_comm_decl oc name sz al = + fprintf oc " .comm %a, %s, %d\n" + symbol name (Z.to_string sz) (log2 al) + + let print_lcomm_decl oc name sz al = + fprintf oc " .lcomm %a, %s, %d\n" + symbol name (Z.to_string sz) (log2 al) end:SYSTEM) @@ -638,7 +671,6 @@ let print_builtin_inline oc name args res = let float64_literals : (int * int64) list ref = ref [] let float32_literals : (int * int32) list ref = ref [] let jumptables : (int * label list) list ref = ref [] -let indirect_symbols : StringSet.t ref = ref StringSet.empty (* Reminder on AT&T syntax: op source, dest *) @@ -996,12 +1028,9 @@ let print_var oc name v = end else begin let sz = match v.gvar_init with [Init_space sz] -> sz | _ -> assert false in - if C2C.atom_is_static name then - fprintf oc " .local %a\n" symbol name; - fprintf oc " .comm %a, %s, %d\n" - symbol name - (Z.to_string sz) - align + if C2C.atom_is_static name + then Target.print_lcomm_decl oc name sz align + else Target.print_comm_decl oc name sz align end let print_globdef oc (name, gdef) = @@ -1032,7 +1061,8 @@ let print_program oc p = Hashtbl.clear Printer.filename_num; List.iter (Printer.print_globdef oc) p.prog_defs; if !Printer.need_masks then begin - Printer.section oc Section_const; (* not Section_literal because not 8-bytes *) + Printer.section oc (Section_const true); + (* not Section_literal because not 8-bytes *) Target.print_align oc 16; fprintf oc "%a: .quad 0x8000000000000000, 0\n" Target.raw_symbol "__negd_mask"; @@ -1042,4 +1072,6 @@ let print_program oc p = Target.raw_symbol "__negs_mask"; fprintf oc "%a: .long 0x7FFFFFFF, 0xFFFFFFFF, 0xFFFFFFFF, 0xFFFFFFFF\n" Target.raw_symbol "__abss_mask" - end + end; + Target.print_epilogue oc + diff --git a/ia32/Unusedglob1.ml b/ia32/Unusedglob1.ml deleted file mode 100644 index eb0298bb..00000000 --- a/ia32/Unusedglob1.ml +++ /dev/null @@ -1,46 +0,0 @@ -(* *********************************************************************) -(* *) -(* The Compcert verified compiler *) -(* *) -(* Xavier Leroy, INRIA Paris-Rocquencourt *) -(* *) -(* Copyright Institut National de Recherche en Informatique et en *) -(* Automatique. All rights reserved. This file is distributed *) -(* under the terms of the INRIA Non-Commercial License Agreement. *) -(* *) -(* *********************************************************************) - -(* Identifiers referenced from an IA32 Asm instruction *) - -open Datatypes -open AST -open Asm - -let referenced_addr (Addrmode(base, ofs, const)) = - match const with - | Coq_inl n -> [] - | Coq_inr(s, ofs) -> [s] - -let referenced_builtin ef = - match ef with - | EF_vload_global(chunk, id, ofs) -> [id] - | EF_vstore_global(chunk, id, ofs) -> [id] - | _ -> [] - -let referenced_instr = function - | Pmov_rm (_, a) | Pmov_mr (a, _) - | Pmov_rm_a (_, a) | Pmov_mr_a (a, _) - | Pmovsd_fm (_, a) | Pmovsd_mf(a, _) - | Pmovss_fm (_, a) | Pmovss_mf(a, _) - | Pfldl_m a | Pflds_m a | Pfstpl_m a | Pfstps_m a - | Pmovb_mr (a, _) | Pmovw_mr (a, _) - | Pmovzb_rm (_, a) | Pmovsb_rm (_, a) - | Pmovzw_rm (_, a) | Pmovsw_rm (_, a) - | Plea (_, a) -> referenced_addr a - | Pjmp_s(s, _) -> [s] - | Pcall_s(s, _) -> [s] - | Pbuiltin(ef, args, res) -> referenced_builtin ef - | _ -> [] - -let code_of_function f = f.fn_code - diff --git a/ia32/ValueAOp.v b/ia32/ValueAOp.v index 874c2be3..53013337 100644 --- a/ia32/ValueAOp.v +++ b/ia32/ValueAOp.v @@ -58,7 +58,7 @@ Definition eval_static_operation (op: operation) (vl: list aval): aval := | Ointconst n, nil => I n | Ofloatconst n, nil => if propagate_float_constants tt then F n else ftop | Osingleconst n, nil => if propagate_float_constants tt then FS n else ftop - | Oindirectsymbol id, nil => Ptr (Gl id Int.zero) + | Oindirectsymbol id, nil => Ifptr (Gl id Int.zero) | Ocast8signed, v1 :: nil => sign_ext 8 v1 | Ocast8unsigned, v1 :: nil => zero_ext 8 v1 | Ocast16signed, v1 :: nil => sign_ext 16 v1 @@ -145,7 +145,16 @@ Proof. intros; apply symbol_address_sound; apply GENV. Qed. -Hint Resolve symbol_address_sound: va. +Lemma symbol_address_sound_2: + forall id ofs, + vmatch bc (Genv.symbol_address ge id ofs) (Ifptr (Gl id ofs)). +Proof. + intros. unfold Genv.symbol_address. destruct (Genv.find_symbol ge id) as [b|] eqn:F. + constructor. constructor. apply GENV; auto. + constructor. +Qed. + +Hint Resolve symbol_address_sound symbol_address_sound_2: va. Ltac InvHyps := match goal with diff --git a/powerpc/Asmgenproof.v b/powerpc/Asmgenproof.v index 9adf44dc..c7439c3d 100644 --- a/powerpc/Asmgenproof.v +++ b/powerpc/Asmgenproof.v @@ -49,6 +49,14 @@ Proof. exact TRANSF. Qed. +Lemma public_preserved: + forall id, Genv.public_symbol tge id = Genv.public_symbol ge id. +Proof. + intros. unfold ge, tge. + apply Genv.public_symbol_transf_partial with transf_fundef. + exact TRANSF. +Qed. + Lemma varinfo_preserved: forall b, Genv.find_var_info tge b = Genv.find_var_info ge b. Proof. @@ -755,7 +763,7 @@ Hint Resolve agree_nextinstr agree_set_other: asmgen. eapply exec_step_builtin. eauto. eauto. eapply find_instr_tail; eauto. eapply external_call_symbols_preserved'; eauto. - exact symbols_preserved. exact varinfo_preserved. + exact symbols_preserved. exact public_preserved. exact varinfo_preserved. eauto. econstructor; eauto. Simpl. rewrite set_pregs_other_2. rewrite undef_regs_other_2. rewrite <- H0. simpl. econstructor; eauto. @@ -777,7 +785,7 @@ Hint Resolve agree_nextinstr agree_set_other: asmgen. eapply exec_step_annot. eauto. eauto. eapply find_instr_tail; eauto. eauto. eapply external_call_symbols_preserved'; eauto. - exact symbols_preserved. exact varinfo_preserved. + exact symbols_preserved. exact public_preserved. exact varinfo_preserved. eapply match_states_intro with (ep := false); eauto with coqlib. unfold nextinstr. rewrite Pregmap.gss. rewrite <- H1; simpl. econstructor; eauto. @@ -960,7 +968,7 @@ Local Transparent destroyed_by_jumptable. left; econstructor; split. apply plus_one. eapply exec_step_external; eauto. eapply external_call_symbols_preserved'; eauto. - exact symbols_preserved. exact varinfo_preserved. + exact symbols_preserved. exact public_preserved. exact varinfo_preserved. econstructor; eauto. unfold loc_external_result. apply agree_set_other; auto. apply agree_set_mregs; auto. @@ -1005,7 +1013,7 @@ Theorem transf_program_correct: forward_simulation (Mach.semantics return_address_offset prog) (Asm.semantics tprog). Proof. eapply forward_simulation_star with (measure := measure). - eexact symbols_preserved. + eexact public_preserved. eexact transf_initial_states. eexact transf_final_states. exact step_simulation. diff --git a/powerpc/Op.v b/powerpc/Op.v index dbec2755..3d5b1fc5 100644 --- a/powerpc/Op.v +++ b/powerpc/Op.v @@ -581,6 +581,22 @@ Proof. destruct c; simpl; auto; discriminate. Qed. +(** Global variables mentioned in an operation or addressing mode *) + +Definition globals_operation (op: operation) : list ident := + match op with + | Oaddrsymbol s ofs => s :: nil + | Oaddsymbol s ofs => s :: nil + | _ => nil + end. + +Definition globals_addressing (addr: addressing) : list ident := + match addr with + | Aglobal s n => s :: nil + | Abased s n => s :: nil + | _ => nil + end. + (** * Invariance and compatibility properties. *) (** [eval_operation] and [eval_addressing] depend on a global environment @@ -622,14 +638,11 @@ End GENV_TRANSF. Section EVAL_COMPAT. -Variable F V: Type. -Variable genv: Genv.t F V. +Variable F1 F2 V1 V2: Type. +Variable ge1: Genv.t F1 V1. +Variable ge2: Genv.t F2 V2. Variable f: meminj. -Hypothesis symbol_address_inj: - forall id ofs, - val_inject f (Genv.symbol_address genv id ofs) (Genv.symbol_address genv id ofs). - Variable m1: mem. Variable m2: mem. @@ -704,18 +717,22 @@ Ltac TrivialExists := Lemma eval_operation_inj: forall op sp1 vl1 sp2 vl2 v1, + (forall id ofs, + In id (globals_operation op) -> + val_inject f (Genv.symbol_address ge1 id ofs) (Genv.symbol_address ge2 id ofs)) -> val_inject f sp1 sp2 -> val_list_inject f vl1 vl2 -> - eval_operation genv sp1 op vl1 m1 = Some v1 -> - exists v2, eval_operation genv sp2 op vl2 m2 = Some v2 /\ val_inject f v1 v2. + eval_operation ge1 sp1 op vl1 m1 = Some v1 -> + exists v2, eval_operation ge2 sp2 op vl2 m2 = Some v2 /\ val_inject f v1 v2. Proof. - intros. destruct op; simpl in H1; simpl; FuncInv; InvInject; TrivialExists. - inv H; simpl; econstructor; eauto. repeat rewrite Int.add_assoc. decEq. apply Int.add_commut. + intros until v1; intros GL; intros. destruct op; simpl in H1; simpl; FuncInv; InvInject; TrivialExists. + apply GL; simpl; auto. + apply Values.val_add_inject; auto. inv H4; simpl; auto. inv H4; simpl; auto. apply Values.val_add_inject; auto. apply Values.val_add_inject; auto. - apply Values.val_add_inject; auto. + apply Values.val_add_inject; auto. apply GL; simpl; auto. inv H4; inv H2; simpl; auto. econstructor; eauto. rewrite Int.sub_add_l. auto. destruct (eq_block b1 b0); auto. subst. rewrite H1 in H0. inv H0. rewrite dec_eq_true. @@ -777,13 +794,18 @@ Qed. Lemma eval_addressing_inj: forall addr sp1 vl1 sp2 vl2 v1, + (forall id ofs, + In id (globals_addressing addr) -> + val_inject f (Genv.symbol_address ge1 id ofs) (Genv.symbol_address ge2 id ofs)) -> val_inject f sp1 sp2 -> val_list_inject f vl1 vl2 -> - eval_addressing genv sp1 addr vl1 = Some v1 -> - exists v2, eval_addressing genv sp2 addr vl2 = Some v2 /\ val_inject f v1 v2. + eval_addressing ge1 sp1 addr vl1 = Some v1 -> + exists v2, eval_addressing ge2 sp2 addr vl2 = Some v2 /\ val_inject f v1 v2. Proof. - intros. destruct addr; simpl in H1; simpl; FuncInv; InvInject; TrivialExists; + intros. destruct addr; simpl in H2; simpl; FuncInv; InvInject; TrivialExists; auto using Values.val_add_inject. + apply H; simpl; auto. + apply Values.val_add_inject; auto. apply H; simpl; auto. Qed. End EVAL_COMPAT. @@ -864,11 +886,11 @@ Proof. eval_operation genv sp op vl2 m2 = Some v2 /\ val_inject (fun b => Some(b, 0)) v1 v2). eapply eval_operation_inj with (m1 := m1) (sp1 := sp). - intros. rewrite <- val_inject_lessdef; auto. apply valid_pointer_extends; auto. apply weak_valid_pointer_extends; auto. apply weak_valid_pointer_no_overflow_extends; auto. apply valid_different_pointers_extends; auto. + intros. rewrite <- val_inject_lessdef; auto. rewrite <- val_inject_lessdef; auto. eauto. auto. destruct H2 as [v2 [A B]]. exists v2; split; auto. rewrite val_inject_lessdef; auto. @@ -939,7 +961,7 @@ Proof. intros. rewrite eval_shift_stack_addressing. simpl. eapply eval_addressing_inj with (sp1 := Vptr sp1 Int.zero); eauto. - exact symbol_address_inject. + intros. apply symbol_address_inject. Qed. Lemma eval_operation_inject: @@ -954,11 +976,11 @@ Proof. intros. rewrite eval_shift_stack_operation. simpl. eapply eval_operation_inj with (sp1 := Vptr sp1 Int.zero) (m1 := m1); eauto. - exact symbol_address_inject. intros; eapply Mem.valid_pointer_inject_val; eauto. intros; eapply Mem.weak_valid_pointer_inject_val; eauto. intros; eapply Mem.weak_valid_pointer_inject_no_overflow; eauto. intros; eapply Mem.different_pointers_inject; eauto. + intros. apply symbol_address_inject. Qed. End EVAL_INJECT. diff --git a/powerpc/PrintAsm.ml b/powerpc/PrintAsm.ml index 587dfccf..760ed275 100644 --- a/powerpc/PrintAsm.ml +++ b/powerpc/PrintAsm.ml @@ -105,13 +105,14 @@ module Linux_System = let name_of_section = function | Section_text -> ".text" - | Section_data i -> if i then ".data" else "COMM" + | Section_data i -> + if i then ".data" else "COMM" | Section_small_data i -> - if i - then ".section .sdata,\"aw\",@progbits" - else ".section .sbss,\"aw\",@progbits" - | Section_const -> ".rodata" - | Section_small_const -> ".section .sdata2,\"a\",@progbits" + if i then ".section .sdata,\"aw\",@progbits" else "COMM" + | Section_const i -> + if i then ".rodata" else "COMM" + | Section_small_const i -> + if i then ".section .sdata2,\"a\",@progbits" else "COMM" | Section_string -> ".rodata" | Section_literal -> ".section .rodata.cst8,\"aM\",@progbits,8" | Section_jumptable -> ".text" @@ -197,10 +198,10 @@ module Diab_System = let name_of_section = function | Section_text -> ".text" - | Section_data i -> if i then ".data" else ".bss" + | Section_data i -> if i then ".data" else "COMM" | Section_small_data i -> if i then ".sdata" else ".sbss" - | Section_const -> ".text" - | Section_small_const -> ".sdata2" + | Section_const _ -> ".text" + | Section_small_const _ -> ".sdata2" | Section_string -> ".text" | Section_literal -> ".text" | Section_jumptable -> ".text" diff --git a/powerpc/Unusedglob1.ml b/powerpc/Unusedglob1.ml deleted file mode 100644 index 2d3efe39..00000000 --- a/powerpc/Unusedglob1.ml +++ /dev/null @@ -1,67 +0,0 @@ -(* *********************************************************************) -(* *) -(* The Compcert verified compiler *) -(* *) -(* Xavier Leroy, INRIA Paris-Rocquencourt *) -(* *) -(* Copyright Institut National de Recherche en Informatique et en *) -(* Automatique. All rights reserved. This file is distributed *) -(* under the terms of the INRIA Non-Commercial License Agreement. *) -(* *) -(* *********************************************************************) - -(* Identifiers referenced from a PowerPC Asm instruction *) - -open Datatypes -open AST -open Asm - -let referenced_constant = function - | Cint n -> [] - | Csymbol_low(s, ofs) -> [s] - | Csymbol_high(s, ofs) -> [s] - | Csymbol_sda(s, ofs) -> [s] - | Csymbol_rel_low(s, ofs) -> [s] - | Csymbol_rel_high(s, ofs) -> [s] - -let referenced_builtin ef = - match ef with - | EF_vload_global(chunk, id, ofs) -> [id] - | EF_vstore_global(chunk, id, ofs) -> [id] - | _ -> [] - -let referenced_instr = function - | Pbl(s, _) -> [s] - | Pbs(s, _) -> [s] - | Paddi(_, _, c) - | Paddic(_, _, c) - | Paddis(_, _, c) - | Pandi_(_, _, c) - | Pandis_(_, _, c) - | Pcmplwi(_, c) - | Pcmpwi(_, c) - | Plbz(_, c, _) - | Plfd(_, c, _) - | Plfd_a(_, c, _) - | Plfs(_, c, _) - | Plha(_, c, _) - | Plhz(_, c, _) - | Plwz(_, c, _) - | Plwz_a(_, c, _) - | Pmulli(_, _, c) - | Pori(_, _, c) - | Poris(_, _, c) - | Pstb(_, c, _) - | Pstfd(_, c, _) - | Pstfd_a(_, c, _) - | Pstfs(_, c, _) - | Psth(_, c, _) - | Pstw(_, c, _) - | Pstw_a(_, c, _) - | Psubfic(_, _, c) - | Pxori(_, _, c) - | Pxoris(_, _, c) -> referenced_constant c - | Pbuiltin(ef, _, _) -> referenced_builtin ef - | _ -> [] - -let code_of_function f = f.fn_code diff --git a/test/regression/Makefile b/test/regression/Makefile index f4f96233..5c601211 100644 --- a/test/regression/Makefile +++ b/test/regression/Makefile @@ -16,7 +16,8 @@ TESTS=int32 int64 floats floats-basics \ expr1 expr6 funptr2 initializers initializers2 initializers3 \ volatile1 volatile2 volatile3 \ funct3 expr5 struct7 struct8 struct11 casts1 casts2 char1 \ - sizeof1 sizeof2 binops bool for1 switch switch2 compound + sizeof1 sizeof2 binops bool for1 switch switch2 compound \ + decl1 # Can run, but only in compiled mode, and have reference output in Results diff --git a/test/regression/Results/decl1 b/test/regression/Results/decl1 new file mode 100644 index 00000000..fa8248b0 --- /dev/null +++ b/test/regression/Results/decl1 @@ -0,0 +1 @@ +Result is 2 diff --git a/test/regression/decl1.c b/test/regression/decl1.c new file mode 100644 index 00000000..6049b4af --- /dev/null +++ b/test/regression/decl1.c @@ -0,0 +1,21 @@ +#include <stdio.h> + +/* Local function declarations */ + +int f (int p) +{ + p = p + 1; + return p; +} + +int main (int argc, char **argv) +{ + int (*p)(int); + int f(); + int i; + + p = f; + i = (*p)(1); + printf("Result is %d\n", i); + return 0; +} diff --git a/test/spass/clock.c b/test/spass/clock.c index 7106669a..d9472338 100644 --- a/test/spass/clock.c +++ b/test/spass/clock.c @@ -104,7 +104,7 @@ void clock_StartCounter(CLOCK_CLOCKS ClockCounter) **********************************************************/ { #ifndef CLOCK_NO_TIMING - ftime(&(clock_Counters[ClockCounter])); + gettimeofday(&(clock_Counters[ClockCounter]), NULL); #endif } @@ -121,7 +121,7 @@ void clock_StopPassedTime(CLOCK_CLOCKS ClockCounter) { #ifndef CLOCK_NO_TIMING CLOCK_TMS newtime; - ftime(&newtime); + gettimeofday(&newtime, NULL); clock_Akku[ClockCounter] = clock_GetSeconds(ClockCounter); #endif } @@ -139,7 +139,7 @@ void clock_StopAddPassedTime(CLOCK_CLOCKS ClockCounter) { #ifndef CLOCK_NO_TIMING CLOCK_TMS newtime; - ftime(&newtime); + gettimeofday(&newtime, NULL); clock_Akku[ClockCounter] += clock_GetSeconds(ClockCounter); #endif } @@ -157,13 +157,21 @@ float clock_GetSeconds(CLOCK_CLOCKS ClockCounter) { #ifndef CLOCK_NO_TIMING CLOCK_TMS newtime; - ftime(&newtime); - return ((float) (newtime.time - clock_Counters[ClockCounter].time) - + (((newtime.millitm - clock_Counters[ClockCounter].millitm)) - /(float)1000)); -#else + time_t seconds_passed; + long microseconds_passed; + + gettimeofday(&newtime, NULL); + + seconds_passed = newtime.tv_sec - clock_Counters[ClockCounter].tv_sec; + microseconds_passed = newtime.tv_usec - clock_Counters[ClockCounter].tv_usec; + + return ((float) seconds_passed + + (microseconds_passed /(float)1000000)); + +#else /* CLOCK_NO_TIMING */ return 0; -#endif +#endif /* ! CLOCK_NO_TIMING */ + } #ifdef WIN diff --git a/test/spass/clock.h b/test/spass/clock.h index 6e675742..80f6c003 100644 --- a/test/spass/clock.h +++ b/test/spass/clock.h @@ -49,7 +49,7 @@ #include "misc.h" #include <sys/types.h> -#include <sys/timeb.h> +#include <sys/time.h> typedef enum { clock_BACKTRACK, @@ -61,7 +61,7 @@ typedef enum { clock_TYPESIZE } CLOCK_CLOCKS; -typedef struct timeb CLOCK_TMS; +typedef struct timeval CLOCK_TMS; void clock_Init(void); void clock_InitCounter(CLOCK_CLOCKS); |