Public globals

.depend

@@ -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

Makefile

@@ -91,6 +91,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 \

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.

arm/Op.v

@@ -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.

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. 

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" } }
 ;
 

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.