diff options
| -rw-r--r-- | .depend | 5 | ||||
| -rw-r--r-- | Makefile | 2 | ||||
| -rw-r--r-- | arm/Asmgenproof.v | 2 | ||||
| -rw-r--r-- | arm/Constpropproof.v | 2 | ||||
| -rw-r--r-- | arm/Selectionproof.v | 2 | ||||
| -rw-r--r-- | backend/Allocproof.v | 2 | ||||
| -rw-r--r-- | backend/CSEproof.v | 2 | ||||
| -rw-r--r-- | backend/Linearizeproof.v | 2 | ||||
| -rw-r--r-- | backend/Machabstr2concr.v | 6 | ||||
| -rw-r--r-- | backend/RTLgenproof.v | 2 | ||||
| -rw-r--r-- | backend/Reloadproof.v | 2 | ||||
| -rw-r--r-- | backend/Stackingproof.v | 2 | ||||
| -rw-r--r-- | backend/Tailcallproof.v | 2 | ||||
| -rw-r--r-- | backend/Tunneling.v | 51 | ||||
| -rw-r--r-- | backend/Tunnelingproof.v | 221 | ||||
| -rw-r--r-- | backend/Tunnelingtyping.v | 40 | ||||
| -rw-r--r-- | cfrontend/Cminorgenproof.v | 2 | ||||
| -rw-r--r-- | cfrontend/Cshmgenproof3.v | 13 | ||||
| -rw-r--r-- | common/Smallstep.v | 45 | ||||
| -rw-r--r-- | driver/Compiler.v | 62 | ||||
| -rw-r--r-- | driver/Complements.v | 129 | ||||
| -rw-r--r-- | lib/Coqlib.v | 5 | ||||
| -rw-r--r-- | lib/Maps.v | 115 | ||||
| -rw-r--r-- | powerpc/Asmgenproof.v | 2 | ||||
| -rw-r--r-- | powerpc/Constpropproof.v | 2 | ||||
| -rw-r--r-- | powerpc/Selectionproof.v | 2 |
26 files changed, 449 insertions, 273 deletions
@@ -7,6 +7,7 @@ lib/Lattice.vo: lib/Lattice.v lib/Coqlib.vo lib/Maps.vo lib/Maps.vo: lib/Maps.v lib/Coqlib.vo lib/Ordered.vo: lib/Ordered.v lib/Coqlib.vo lib/Maps.vo lib/Parmov.vo: lib/Parmov.v lib/Coqlib.vo +lib/UnionFind.vo: lib/UnionFind.v lib/Coqlib.vo common/AST.vo: common/AST.v lib/Coqlib.vo common/Errors.vo lib/Integers.vo lib/Floats.vo common/Errors.vo: common/Errors.v lib/Coqlib.vo common/Events.vo: common/Events.v lib/Coqlib.vo common/AST.vo lib/Integers.vo lib/Floats.vo common/Values.vo common/Mem.vo @@ -70,9 +71,9 @@ backend/Stackingtyping.vo: backend/Stackingtyping.v lib/Coqlib.vo lib/Maps.vo co backend/Stacking.vo: backend/Stacking.v lib/Coqlib.vo lib/Maps.vo common/Errors.vo common/AST.vo lib/Integers.vo $(ARCH)/Op.vo backend/RTL.vo backend/Locations.vo backend/Linear.vo backend/Bounds.vo backend/Mach.vo $(ARCH)/$(VARIANT)/Conventions.vo $(ARCH)/$(VARIANT)/Stacklayout.vo backend/Tailcallproof.vo: backend/Tailcallproof.v lib/Coqlib.vo lib/Maps.vo common/AST.vo lib/Integers.vo common/Values.vo common/Mem.vo $(ARCH)/Op.vo common/Events.vo common/Globalenvs.vo common/Smallstep.vo backend/Registers.vo backend/RTL.vo $(ARCH)/$(VARIANT)/Conventions.vo backend/Tailcall.vo backend/Tailcall.vo: backend/Tailcall.v lib/Coqlib.vo lib/Maps.vo common/AST.vo common/Globalenvs.vo backend/Registers.vo $(ARCH)/Op.vo backend/RTL.vo $(ARCH)/$(VARIANT)/Conventions.vo -backend/Tunnelingproof.vo: backend/Tunnelingproof.v lib/Coqlib.vo lib/Maps.vo common/AST.vo common/Values.vo common/Mem.vo common/Events.vo common/Globalenvs.vo common/Smallstep.vo $(ARCH)/Op.vo backend/Locations.vo backend/LTL.vo backend/Tunneling.vo +backend/Tunnelingproof.vo: backend/Tunnelingproof.v lib/Coqlib.vo lib/Maps.vo lib/UnionFind.vo common/AST.vo common/Values.vo common/Mem.vo common/Events.vo common/Globalenvs.vo common/Smallstep.vo $(ARCH)/Op.vo backend/Locations.vo backend/LTL.vo backend/Tunneling.vo backend/Tunnelingtyping.vo: backend/Tunnelingtyping.v lib/Coqlib.vo lib/Maps.vo common/AST.vo common/Values.vo common/Mem.vo common/Globalenvs.vo $(ARCH)/Op.vo backend/Locations.vo backend/LTL.vo backend/LTLtyping.vo backend/Tunneling.vo backend/Tunnelingproof.vo -backend/Tunneling.vo: backend/Tunneling.v lib/Coqlib.vo lib/Maps.vo common/AST.vo common/Values.vo common/Globalenvs.vo $(ARCH)/Op.vo backend/Locations.vo backend/LTL.vo +backend/Tunneling.vo: backend/Tunneling.v lib/Coqlib.vo lib/Maps.vo lib/UnionFind.vo common/AST.vo common/Values.vo common/Globalenvs.vo $(ARCH)/Op.vo backend/Locations.vo backend/LTL.vo cfrontend/Cminorgenproof.vo: cfrontend/Cminorgenproof.v lib/Coqlib.vo common/Errors.vo lib/Maps.vo common/AST.vo lib/Integers.vo lib/Floats.vo common/Values.vo common/Mem.vo common/Events.vo common/Globalenvs.vo cfrontend/Csharpminor.vo $(ARCH)/Op.vo backend/Cminor.vo cfrontend/Cminorgen.vo cfrontend/Cminorgen.vo: cfrontend/Cminorgen.v lib/Coqlib.vo common/Errors.vo lib/Maps.vo lib/Ordered.vo common/AST.vo lib/Integers.vo common/Mem.vo cfrontend/Csharpminor.vo $(ARCH)/Op.vo backend/Cminor.vo cfrontend/Csem.vo: cfrontend/Csem.v lib/Coqlib.vo common/Errors.vo lib/Maps.vo lib/Integers.vo lib/Floats.vo common/Values.vo common/AST.vo common/Mem.vo common/Events.vo common/Globalenvs.vo cfrontend/Csyntax.vo common/Smallstep.vo @@ -36,7 +36,7 @@ GPATH=$(DIRS) # General-purpose libraries (in lib/) LIB=Coqlib.v Maps.v Lattice.v Ordered.v \ - Iteration.v Integers.v Floats.v Parmov.v + Iteration.v Integers.v Floats.v Parmov.v UnionFind.v # Parts common to the front-ends and the back-end (in common/) diff --git a/arm/Asmgenproof.v b/arm/Asmgenproof.v index f9f4cd0..7b1fd62 100644 --- a/arm/Asmgenproof.v +++ b/arm/Asmgenproof.v @@ -1173,7 +1173,7 @@ Proof. Qed. Theorem transf_program_correct: - forall (beh: program_behavior), + forall (beh: program_behavior), not_wrong beh -> Machconcr.exec_program prog beh -> Asm.exec_program tprog beh. Proof. unfold Machconcr.exec_program, Asm.exec_program; intros. diff --git a/arm/Constpropproof.v b/arm/Constpropproof.v index 7c7b878..08c5baf 100644 --- a/arm/Constpropproof.v +++ b/arm/Constpropproof.v @@ -947,7 +947,7 @@ Qed. [Smallstep.simulation_step_preservation]. *) Theorem transf_program_correct: - forall (beh: program_behavior), + forall (beh: program_behavior), not_wrong beh -> exec_program prog beh -> exec_program tprog beh. Proof. unfold exec_program; intros. diff --git a/arm/Selectionproof.v b/arm/Selectionproof.v index 967e229..cf7613b 100644 --- a/arm/Selectionproof.v +++ b/arm/Selectionproof.v @@ -1446,7 +1446,7 @@ Proof. Qed. Theorem transf_program_correct: - forall (beh: program_behavior), + forall (beh: program_behavior), not_wrong beh -> Cminor.exec_program prog beh -> CminorSel.exec_program tprog beh. Proof. unfold CminorSel.exec_program, Cminor.exec_program; intros. diff --git a/backend/Allocproof.v b/backend/Allocproof.v index e2387b5..7e9334a 100644 --- a/backend/Allocproof.v +++ b/backend/Allocproof.v @@ -750,7 +750,7 @@ Proof. Qed. Theorem transf_program_correct: - forall (beh: program_behavior), + forall (beh: program_behavior), not_wrong beh -> RTL.exec_program prog beh -> LTL.exec_program tprog beh. Proof. unfold RTL.exec_program, LTL.exec_program; intros. diff --git a/backend/CSEproof.v b/backend/CSEproof.v index 265bb20..3751cec 100644 --- a/backend/CSEproof.v +++ b/backend/CSEproof.v @@ -973,7 +973,7 @@ Proof. Qed. Theorem transf_program_correct: - forall (beh: program_behavior), + forall (beh: program_behavior), not_wrong beh -> exec_program prog beh -> exec_program tprog beh. Proof. unfold exec_program; intros. diff --git a/backend/Linearizeproof.v b/backend/Linearizeproof.v index c24d370..1fb068d 100644 --- a/backend/Linearizeproof.v +++ b/backend/Linearizeproof.v @@ -707,7 +707,7 @@ Proof. Qed. Theorem transf_program_correct: - forall (beh: program_behavior), + forall (beh: program_behavior), not_wrong beh -> LTL.exec_program prog beh -> LTLin.exec_program tprog beh. Proof. unfold LTL.exec_program, exec_program; intros. diff --git a/backend/Machabstr2concr.v b/backend/Machabstr2concr.v index 6e331f3..139eac7 100644 --- a/backend/Machabstr2concr.v +++ b/backend/Machabstr2concr.v @@ -905,7 +905,7 @@ Proof. Qed. Theorem exec_program_equiv: - forall (beh: program_behavior), + forall (beh: program_behavior), not_wrong beh -> Machabstr.exec_program p beh -> Machconcr.exec_program p beh. Proof. unfold Machconcr.exec_program, Machabstr.exec_program; intros. @@ -915,10 +915,10 @@ Proof. (match_states := fun st1 st2 => match_states st1 st2 /\ wt_state st1). eexact equiv_initial_states. eexact equiv_final_states. - intros. destruct H1. exploit step_equiv; eauto. + intros. destruct H2. exploit step_equiv; eauto. intros [st2' [A B]]. exists st2'; split. auto. split. auto. eapply Machtyping.subject_reduction; eauto. - auto. + auto. auto. Qed. End SIMULATION. diff --git a/backend/RTLgenproof.v b/backend/RTLgenproof.v index 1dd2294..df1ade9 100644 --- a/backend/RTLgenproof.v +++ b/backend/RTLgenproof.v @@ -1289,7 +1289,7 @@ Proof. Qed. Theorem transf_program_correct: - forall (beh: program_behavior), + forall (beh: program_behavior), not_wrong beh -> CminorSel.exec_program prog beh -> RTL.exec_program tprog beh. Proof. unfold CminorSel.exec_program, RTL.exec_program; intros. diff --git a/backend/Reloadproof.v b/backend/Reloadproof.v index ea7c5d1..a7becc3 100644 --- a/backend/Reloadproof.v +++ b/backend/Reloadproof.v @@ -1345,7 +1345,7 @@ Proof. Qed. Theorem transf_program_correct: - forall (beh: program_behavior), + forall (beh: program_behavior), not_wrong beh -> LTLin.exec_program prog beh -> Linear.exec_program tprog beh. Proof. unfold LTLin.exec_program, Linear.exec_program; intros. diff --git a/backend/Stackingproof.v b/backend/Stackingproof.v index d5819f7..5b6f2dc 100644 --- a/backend/Stackingproof.v +++ b/backend/Stackingproof.v @@ -1592,7 +1592,7 @@ Proof. Qed. Theorem transf_program_correct: - forall (beh: program_behavior), + forall (beh: program_behavior), not_wrong beh -> Linear.exec_program prog beh -> Machabstr.exec_program tprog beh. Proof. unfold Linear.exec_program, Machabstr.exec_program; intros. diff --git a/backend/Tailcallproof.v b/backend/Tailcallproof.v index 791db37..1423e1e 100644 --- a/backend/Tailcallproof.v +++ b/backend/Tailcallproof.v @@ -722,7 +722,7 @@ Qed. [Smallstep.simulation_opt_preservation]. *) Theorem transf_program_correct: - forall (beh: program_behavior), + forall (beh: program_behavior), not_wrong beh -> exec_program prog beh -> exec_program tprog beh. Proof. unfold exec_program; intros. diff --git a/backend/Tunneling.v b/backend/Tunneling.v index 32d1b59..4b1417f 100644 --- a/backend/Tunneling.v +++ b/backend/Tunneling.v @@ -14,6 +14,7 @@ Require Import Coqlib. Require Import Maps. +Require Import UnionFind. Require Import AST. Require Import Values. Require Import Globalenvs. @@ -42,9 +43,6 @@ Require Import LTL. dead code (as the "goto L3" in the example above). *) -Definition is_goto_instr (b: option instruction) : option node := - match b with Some (Lnop s) => Some s | _ => None end. - (** [branch_target f pc] returns the node of the CFG that is at the end of the branch sequence starting at [pc]. If the instruction at [pc] is not a [goto], [pc] itself is returned. @@ -77,50 +75,44 @@ Definition is_goto_instr (b: option instruction) : option node := is simpler if we return the label of the first [goto] in the sequence. *) -Fixpoint branch_target_rec (f: LTL.function) (pc: node) (count: nat) - {struct count} : option node := - match count with - | Datatypes.O => None - | Datatypes.S count' => - match is_goto_instr f.(fn_code)!pc with - | Some s => branch_target_rec f s count' - | None => Some pc - end - end. +Module U := UnionFind.UF(PTree). -Definition branch_target (f: LTL.function) (pc: node) := - match branch_target_rec f pc 10%nat with - | Some pc' => pc' - | None => pc +Definition record_goto (uf: U.t) (pc: node) (i: instruction) : U.t := + match i with + | Lnop s => U.union uf pc s + | _ => uf end. +Definition record_gotos (f: LTL.function) : U.t := + PTree.fold record_goto f.(fn_code) U.empty. + (** The tunneling optimization simply rewrites all LTL basic blocks, replacing the destinations of the [Bgoto] and [Bcond] instructions with their final target, as computed by [branch_target]. *) -Definition tunnel_instr (f: LTL.function) (b: instruction) : instruction := +Definition tunnel_instr (uf: U.t) (b: instruction) : instruction := match b with | Lnop s => - Lnop (branch_target f s) + Lnop (U.repr uf s) | Lop op args res s => - Lop op args res (branch_target f s) + Lop op args res (U.repr uf s) | Lload chunk addr args dst s => - Lload chunk addr args dst (branch_target f s) + Lload chunk addr args dst (U.repr uf s) | Lstore chunk addr args src s => - Lstore chunk addr args src (branch_target f s) + Lstore chunk addr args src (U.repr uf s) | Lcall sig ros args res s => - Lcall sig ros args res (branch_target f s) + Lcall sig ros args res (U.repr uf s) | Ltailcall sig ros args => Ltailcall sig ros args | Lcond cond args s1 s2 => - Lcond cond args (branch_target f s1) (branch_target f s2) + Lcond cond args (U.repr uf s1) (U.repr uf s2) | Lreturn or => Lreturn or end. Lemma wf_tunneled_code: - forall (f: LTL.function), - let tc := PTree.map (fun pc b => tunnel_instr f b) (fn_code f) in + forall (f: LTL.function) (uf: U.t), + let tc := PTree.map (fun pc b => tunnel_instr uf b) (fn_code f) in forall (pc: node), Plt pc (fn_nextpc f) \/ tc!pc = None. Proof. intros. elim (fn_code_wf f pc); intro. @@ -129,14 +121,15 @@ Proof. Qed. Definition tunnel_function (f: LTL.function) : LTL.function := + let uf := record_gotos f in mkfunction (fn_sig f) (fn_params f) (fn_stacksize f) - (PTree.map (fun pc b => tunnel_instr f b) (fn_code f)) - (branch_target f (fn_entrypoint f)) + (PTree.map (fun pc b => tunnel_instr uf b) (fn_code f)) + (U.repr uf (fn_entrypoint f)) (fn_nextpc f) - (wf_tunneled_code f). + (wf_tunneled_code f uf). Definition tunnel_fundef (f: LTL.fundef) : LTL.fundef := transf_fundef tunnel_function f. diff --git a/backend/Tunnelingproof.v b/backend/Tunnelingproof.v index 08f5f6c..eccb62d 100644 --- a/backend/Tunnelingproof.v +++ b/backend/Tunnelingproof.v @@ -14,6 +14,7 @@ Require Import Coqlib. Require Import Maps. +Require Import UnionFind. Require Import AST. Require Import Values. Require Import Mem. @@ -25,98 +26,112 @@ Require Import Locations. Require Import LTL. Require Import Tunneling. -(** * Properties of branch target computation *) +(** * Properties of the branch map computed using union-find. *) -Lemma is_goto_instr_correct: - forall b s, - is_goto_instr b = Some s -> b = Some (Lnop s). -Proof. - unfold is_goto_instr; intros. - destruct b; try discriminate. - destruct i; discriminate || congruence. -Qed. - -Lemma branch_target_rec_1: - forall f pc n, - branch_target_rec f pc n = Some pc - \/ branch_target_rec f pc n = None - \/ exists pc', f.(fn_code)!pc = Some(Lnop pc'). -Proof. - intros. destruct n; simpl. - right; left; auto. - caseEq (is_goto_instr f.(fn_code)!pc); intros. - right; right. exists n0. apply is_goto_instr_correct; auto. - left; auto. -Qed. +(** A variant of [record_goto] that also incrementally computes a measure [f: node -> nat] + counting the number of [Lnop] instructions starting at a given [pc] that were eliminated. *) -Lemma branch_target_rec_2: - forall f n pc1 pc2 pc3, - f.(fn_code)!pc1 = Some (Lnop pc2) -> - branch_target_rec f pc1 n = Some pc3 -> - branch_target_rec f pc2 n = Some pc3. +Definition measure_edge (u: U.t) (pc s: node) (f: node -> nat) : node -> nat := + fun x => if peq (U.repr u s) pc then f x + else if peq (U.repr u x) pc then (f x + f s + 1)%nat + else f x. + +Definition record_goto' (uf: U.t * (node -> nat)) (pc: node) (i: instruction) : U.t * (node -> nat) := + match i with + | Lnop s => let (u, f) := uf in (U.union u pc s, measure_edge u pc s f) + | _ => uf + end. + +Definition branch_map_correct (c: code) (uf: U.t * (node -> nat)): Prop := + forall pc, + match c!pc with + | Some(Lnop s) => + U.repr (fst uf) pc = pc \/ (U.repr (fst uf) pc = U.repr (fst uf) s /\ snd uf s < snd uf pc)%nat + | _ => + U.repr (fst uf) pc = pc + end. + +Lemma record_gotos'_correct: + forall c, + branch_map_correct c (PTree.fold record_goto' c (U.empty, fun (x: node) => O)). Proof. - induction n. - simpl. intros; discriminate. - intros pc1 pc2 pc3 ATpc1 H. simpl in H. - unfold is_goto_instr in H; rewrite ATpc1 in H. - simpl. caseEq (is_goto_instr f.(fn_code)!pc2); intros. - apply IHn with pc2. apply is_goto_instr_correct; auto. auto. - destruct n; simpl in H. discriminate. rewrite H0 in H. auto. + intros. + apply PTree_Properties.fold_rec with (P := fun c uf => branch_map_correct c uf). + +(* extensionality *) + intros. red; intros. rewrite <- H. apply H0. + +(* base case *) + red; intros; simpl. rewrite PTree.gempty. apply U.repr_empty. + +(* inductive case *) + intros m uf pc i; intros. destruct uf as [u f]. + assert (PC: U.repr u pc = pc). + generalize (H1 pc). rewrite H. auto. + assert (record_goto' (u, f) pc i = (u, f) + \/ exists s, i = Lnop s /\ record_goto' (u, f) pc i = (U.union u pc s, measure_edge u pc s f)). + unfold record_goto'; simpl. destruct i; auto. right. exists n; auto. + destruct H2 as [B | [s [EQ B]]]. + +(* u and f are unchanged *) + rewrite B. + red. intro pc'. simpl. rewrite PTree.gsspec. destruct (peq pc' pc). subst pc'. + destruct i; auto. + apply H1. + +(* i is Lnop s, u becomes union u pc s, f becomes measure_edge u pc s f *) + rewrite B. + red. intro pc'. simpl. rewrite PTree.gsspec. destruct (peq pc' pc). subst pc'. rewrite EQ. + +(* The new instruction *) + rewrite (U.repr_union_2 u pc s); auto. rewrite U.repr_union_3. + unfold measure_edge. destruct (peq (U.repr u s) pc). auto. right. split. auto. + rewrite PC. rewrite peq_true. omega. + +(* An old instruction *) + assert (U.repr u pc' = pc' -> U.repr (U.union u pc s) pc' = pc'). + intro. rewrite <- H2 at 2. apply U.repr_union_1. congruence. + generalize (H1 pc'). simpl. destruct (m!pc'); auto. destruct i0; auto. + intros [P | [P Q]]. left; auto. right. + split. apply U.sameclass_union_2. auto. + unfold measure_edge. destruct (peq (U.repr u s) pc). auto. + rewrite P. destruct (peq (U.repr u n0) pc). omega. auto. Qed. -(** Counting the number of consecutive gotos. *) - -Fixpoint count_goto_rec (f: LTL.function) (pc: node) (count: nat) - {struct count} : nat := - match count with - | Datatypes.O => Datatypes.O - | Datatypes.S count' => - match is_goto_instr f.(fn_code)!pc with - | Some s => Datatypes.S (count_goto_rec f s count') - | None => Datatypes.O - end - end. - -Definition count_goto (f: LTL.function) (pc: node) : nat := - count_goto_rec f pc 10%nat. - -Lemma count_goto_rec_prop: - forall f n pc1 pc2 pc3, - f.(fn_code)!pc1 = Some (Lnop pc2) -> - branch_target_rec f pc1 n = Some pc3 -> - (count_goto_rec f pc2 n < count_goto_rec f pc1 n)%nat. +Definition record_gotos' (f: function) := + PTree.fold record_goto' f.(fn_code) (U.empty, fun (x: node) => O). + +Lemma record_gotos_gotos': + forall f, fst (record_gotos' f) = record_gotos f. Proof. - induction n. - simpl; intros. discriminate. - intros pc1 pc2 pc3 ATpc1 H. simpl in H. - unfold is_goto_instr in H; rewrite ATpc1 in H. - simpl. unfold is_goto_instr at 2. rewrite ATpc1. - caseEq (is_goto_instr f.(fn_code)!pc2); intros. - exploit (IHn pc2); eauto. apply is_goto_instr_correct; eauto. - omega. - omega. + intros. unfold record_gotos', record_gotos. + repeat rewrite PTree.fold_spec. + generalize (PTree.elements (fn_code f)) (U.empty) (fun _ : node => O). + induction l; intros; simpl. + auto. + unfold record_goto' at 2. unfold record_goto at 2. + destruct (snd a); apply IHl. Qed. -(** The following lemma captures the property of [branch_target] - on which the proof of semantic preservation relies. *) +Definition branch_target (f: function) (pc: node) : node := + U.repr (record_gotos f) pc. -Lemma branch_target_characterization: +Definition count_gotos (f: function) (pc: node) : nat := + snd (record_gotos' f) pc. + +Theorem record_gotos_correct: forall f pc, - branch_target f pc = pc \/ - (exists pc', f.(fn_code)!pc = Some(Lnop pc') - /\ branch_target f pc' = branch_target f pc - /\ count_goto f pc' < count_goto f pc)%nat. + match f.(fn_code)!pc with + | Some(Lnop s) => + branch_target f pc = pc \/ + (branch_target f pc = branch_target f s /\ count_gotos f s < count_gotos f pc)%nat + | _ => branch_target f pc = pc + end. Proof. - intros. unfold branch_target. - generalize (branch_target_rec_1 f pc 10%nat). - intros [A|[A|[pc' AT]]]. - rewrite A. left; auto. - rewrite A. left; auto. - caseEq (branch_target_rec f pc 10%nat). intros pcx BT. - right. exists pc'. split. auto. - split. rewrite (branch_target_rec_2 _ _ _ _ _ AT BT). auto. - unfold count_goto. eapply count_goto_rec_prop; eauto. - intro. left; auto. + intros. + generalize (record_gotos'_correct f.(fn_code) pc). simpl. + fold (record_gotos' f). unfold branch_map_correct, branch_target, count_gotos. + rewrite record_gotos_gotos'. auto. Qed. (** * Preservation of semantics *) @@ -186,7 +201,7 @@ Qed. original and transformed codes. *) Definition tunneled_code (f: function) := - PTree.map (fun pc b => tunnel_instr f b) (fn_code f). + PTree.map (fun pc b => tunnel_instr (record_gotos f) b) (fn_code f). Inductive match_stackframes: stackframe -> stackframe -> Prop := | match_stackframes_intro: @@ -219,25 +234,15 @@ Inductive match_states: state -> state -> Prop := Definition measure (st: state) : nat := match st with - | State s f sp pc ls m => count_goto f pc + | State s f sp pc ls m => count_gotos f pc | Callstate s f ls m => 0%nat | Returnstate s ls m => 0%nat end. -Lemma branch_target_identity: - forall f pc, - match f.(fn_code)!pc with Some(Lnop _) => False | _ => True end -> - branch_target f pc = pc. -Proof. - intros. - destruct (branch_target_characterization f pc) as [A | [pc' [B C]]]. - auto. rewrite B in H. contradiction. -Qed. - Lemma tunnel_function_lookup: forall f pc i, f.(fn_code)!pc = Some i -> - (tunnel_function f).(fn_code)!pc = Some (tunnel_instr f i). + (tunnel_function f).(fn_code)!pc = Some (tunnel_instr (record_gotos f) i). Proof. intros. simpl. rewrite PTree.gmap. rewrite H. auto. Qed. @@ -250,23 +255,23 @@ Lemma tunnel_step_correct: Proof. induction 1; intros; try inv MS. (* Lnop *) - destruct (branch_target_characterization f pc) as [A | [pc1 [B [C D]]]]. + generalize (record_gotos_correct f pc); rewrite H. + intros [A | [B C]]. left; econstructor; split. eapply exec_Lnop. rewrite A. rewrite (tunnel_function_lookup _ _ _ H); simpl; auto. econstructor; eauto. - assert (pc1 = pc') by congruence. subst pc1. right. split. simpl. auto. split. auto. - rewrite <- C. econstructor; eauto. + rewrite B. econstructor; eauto. (* Lop *) - rewrite (branch_target_identity f pc); [idtac | rewrite H; auto]. + generalize (record_gotos_correct f pc); rewrite H; intro A; rewrite A. left; econstructor; split. eapply exec_Lop with (v := v); eauto. rewrite (tunnel_function_lookup _ _ _ H); simpl; auto. rewrite <- H0. apply eval_operation_preserved. exact symbols_preserved. econstructor; eauto. (* Lload *) - rewrite (branch_target_identity f pc); [idtac | rewrite H; auto]. + generalize (record_gotos_correct f pc); rewrite H; intro A; rewrite A. left; econstructor; split. eapply exec_Lload with (a := a). rewrite (tunnel_function_lookup _ _ _ H); simpl; auto. @@ -274,7 +279,7 @@ Proof. eauto. econstructor; eauto. (* Lstore *) - rewrite (branch_target_identity f pc); [idtac | rewrite H; auto]. + generalize (record_gotos_correct f pc); rewrite H; intro A; rewrite A. left; econstructor; split. eapply exec_Lstore with (a := a). rewrite (tunnel_function_lookup _ _ _ H); simpl; auto. @@ -282,36 +287,36 @@ Proof. eauto. econstructor; eauto. (* Lcall *) + generalize (record_gotos_correct f pc); rewrite H; intro A. left; econstructor; split. eapply exec_Lcall with (f' := tunnel_fundef f'); eauto. - rewrite (branch_target_identity f pc); [idtac | rewrite H; auto]. - rewrite (tunnel_function_lookup _ _ _ H); simpl. + rewrite A. rewrite (tunnel_function_lookup _ _ _ H); simpl. rewrite sig_preserved. auto. apply find_function_translated; auto. econstructor; eauto. constructor; auto. constructor; auto. (* Ltailcall *) + generalize (record_gotos_correct f pc); rewrite H; intro A. left; econstructor; split. eapply exec_Ltailcall with (f' := tunnel_fundef f'); eauto. - rewrite (branch_target_identity f pc); [idtac | rewrite H; auto]. - rewrite (tunnel_function_lookup _ _ _ H); simpl. + rewrite A. rewrite (tunnel_function_lookup _ _ _ H); simpl. rewrite sig_preserved. auto. apply find_function_translated; auto. econstructor; eauto. (* cond *) - rewrite (branch_target_identity f pc); [idtac | rewrite H; auto]. + generalize (record_gotos_correct f pc); rewrite H; intro A; rewrite A. left; econstructor; split. eapply exec_Lcond_true; eauto. rewrite (tunnel_function_lookup _ _ _ H); simpl; eauto. econstructor; eauto. - rewrite (branch_target_identity f pc); [idtac | rewrite H; auto]. + generalize (record_gotos_correct f pc); rewrite H; intro A; rewrite A. left; econstructor; split. eapply exec_Lcond_false; eauto. rewrite (tunnel_function_lookup _ _ _ H); simpl; eauto. econstructor; eauto. (* return *) - rewrite (branch_target_identity f pc); [idtac | rewrite H; auto]. + generalize (record_gotos_correct f pc); rewrite H; intro A; rewrite A. left; econstructor; split. eapply exec_Lreturn; eauto. rewrite (tunnel_function_lookup _ _ _ H); simpl; eauto. @@ -355,7 +360,7 @@ Proof. Qed. Theorem transf_program_correct: - forall (beh: program_behavior), + forall (beh: program_behavior), not_wrong beh -> exec_program p beh -> exec_program tp beh. Proof. unfold exec_program; intros. diff --git a/backend/Tunnelingtyping.v b/backend/Tunnelingtyping.v index 57e1271..91745df 100644 --- a/backend/Tunnelingtyping.v +++ b/backend/Tunnelingtyping.v @@ -14,6 +14,7 @@ Require Import Coqlib. Require Import Maps. +Require Import UnionFind. Require Import AST. Require Import Values. Require Import Mem. @@ -27,20 +28,26 @@ Require Import Tunnelingproof. (** Tunneling preserves typing. *) -Lemma branch_target_rec_valid: - forall f, wt_function f -> - forall count pc pc', - branch_target_rec f pc count = Some pc' -> +Lemma branch_target_valid_1: + forall f pc, wt_function f -> valid_successor f pc -> - valid_successor f pc'. + valid_successor f (branch_target f pc). Proof. - induction count; simpl. - intros; discriminate. - intros until pc'. caseEq (is_goto_instr (fn_code f)!pc); intros. - generalize (is_goto_instr_correct _ _ H0). intro. - eapply IHcount; eauto. - generalize (wt_instrs _ H _ _ H3); intro WTI; inv WTI. auto. - inv H1; auto. + intros. + assert (forall n p, + (count_gotos f p < n)%nat -> + valid_successor f p -> + valid_successor f (branch_target f p)). + induction n; intros. + omegaContradiction. + elim H2; intros i EQ. + generalize (record_gotos_correct f p). rewrite EQ. + destruct i; try congruence. + intros [A | [B C]]. congruence. + generalize (wt_instrs _ H _ _ EQ); intro WTI; inv WTI. + rewrite B. apply IHn. omega. auto. + + apply H1 with (Datatypes.S (count_gotos f pc)); auto. Qed. Lemma tunnel_valid_successor: @@ -49,7 +56,7 @@ Lemma tunnel_valid_successor: Proof. intros. destruct H as [i AT]. unfold valid_successor; simpl. rewrite PTree.gmap. rewrite AT. - simpl. exists (tunnel_instr f i); auto. + simpl. exists (tunnel_instr (record_gotos f) i); auto. Qed. Lemma branch_target_valid: @@ -58,16 +65,13 @@ Lemma branch_target_valid: valid_successor f pc -> valid_successor (tunnel_function f) (branch_target f pc). Proof. - intros. apply tunnel_valid_successor. - unfold branch_target. caseEq (branch_target_rec f pc 10); intros. - eapply branch_target_rec_valid; eauto. - auto. + intros. apply tunnel_valid_successor. apply branch_target_valid_1; auto. Qed. Lemma wt_tunnel_instr: forall f i, wt_function f -> - wt_instr f i -> wt_instr (tunnel_function f) (tunnel_instr f i). + wt_instr f i -> wt_instr (tunnel_function f) (tunnel_instr (record_gotos f) i). Proof. intros; inv H0; simpl; econstructor; eauto; eapply branch_target_valid; eauto. diff --git a/cfrontend/Cminorgenproof.v b/cfrontend/Cminorgenproof.v index 1a68c10..984381a 100644 --- a/cfrontend/Cminorgenproof.v +++ b/cfrontend/Cminorgenproof.v @@ -2610,7 +2610,7 @@ Qed. Theorem transl_program_correct: forall (beh: program_behavior), - Csharpminor.exec_program prog beh -> + not_wrong beh -> Csharpminor.exec_program prog beh -> Cminor.exec_program tprog beh. Proof. unfold Csharpminor.exec_program, Cminor.exec_program; intros. diff --git a/cfrontend/Cshmgenproof3.v b/cfrontend/Cshmgenproof3.v index 92a0956..6a8b676 100644 --- a/cfrontend/Cshmgenproof3.v +++ b/cfrontend/Cshmgenproof3.v @@ -1657,7 +1657,7 @@ Qed. Theorem transl_program_correct: forall (beh: program_behavior), - Csem.exec_program prog beh -> + not_wrong beh -> Csem.exec_program prog beh -> Csharpminor.exec_program tprog beh. Proof. set (order := fun (S1 S2: Csem.state) => False). @@ -1669,21 +1669,22 @@ Proof. /\ match_states S2 T2). intros. exploit transl_step; eauto. intros [T2 [A B]]. exists T2; split. auto. auto. - intros. inv H. + intros. inv H0. assert (exists t1, exists s1, Csem.step (Genv.globalenv prog) s t1 s1). - inv H1. inv H0; inv H2. exists t1; exists s2; auto. - destruct H as [t1 [s1 ST]]. + inv H3. inv H2. inv H1. exists t1; exists s2; auto. + destruct H0 as [t1 [s1 ST]]. exploit transl_initial_states; eauto. intros [R [A B]]. exploit simulation_star_star; eauto. intros [R' [C D]]. econstructor; eauto. eapply transl_final_states; eauto. assert (exists t1, exists s1, Csem.step (Genv.globalenv prog) s t1 s1). - inv H1. exists t; exists s2; auto. - destruct H as [t1 [s1 ST]]. + inv H2. exists t; exists s2; auto. + destruct H0 as [t1 [s1 ST]]. exploit transl_initial_states; eauto. intros [R [A B]]. exploit simulation_star_forever; eauto. unfold order; red. intros. constructor; intros. contradiction. intro C. econstructor; eauto. + contradiction. Qed. End CORRECTNESS. diff --git a/common/Smallstep.v b/common/Smallstep.v index f41fe4e..9e9063b 100644 --- a/common/Smallstep.v +++ b/common/Smallstep.v @@ -21,6 +21,7 @@ Require Import Wf. Require Import Wf_nat. +Require Import Classical. Require Import Coqlib. Require Import AST. Require Import Events. @@ -281,18 +282,28 @@ Qed. (** * Outcomes for program executions *) -(** The two valid outcomes for the execution of a program: +(** The three possible outcomes for the execution of a program: - Termination, with a finite trace of observable events and an integer value that stands for the process exit code (the return value of the main function). - Divergence with an infinite trace of observable events. (The actual events generated by the execution can be a finite prefix of this trace, or the whole trace.) +- Going wrong, with a finite trace of observable events + performed before the program gets stuck. *) Inductive program_behavior: Type := | Terminates: trace -> int -> program_behavior - | Diverges: traceinf -> program_behavior. + | Diverges: traceinf -> program_behavior + | Goes_wrong: trace -> program_behavior. + +Definition not_wrong (beh: program_behavior) : Prop := + match beh with + | Terminates _ _ => True + | Diverges _ => True + | Goes_wrong _ => False + end. (** Given a characterization of initial states and final states, [program_behaves] relates a program behaviour with the @@ -311,7 +322,13 @@ Inductive program_behaves (ge: genv): program_behavior -> Prop := | program_diverges: forall s T, initial_state s -> forever ge s T -> - program_behaves ge (Diverges T). + program_behaves ge (Diverges T) + | program_goes_wrong: forall s t s', + initial_state s -> + star ge s t s' -> + (forall t1 s1, ~step ge s' t1 s1) -> + (forall r, ~final_state s' r) -> + program_behaves ge (Goes_wrong t). End CLOSURES. @@ -418,16 +435,18 @@ Qed. Lemma simulation_star_wf_preservation: forall beh, + not_wrong beh -> program_behaves step1 initial_state1 final_state1 ge1 beh -> program_behaves step2 initial_state2 final_state2 ge2 beh. Proof. - intros. inversion H; subst. - destruct (match_initial_states H0) as [s2 [A B]]. - destruct (simulation_star_star H1 B) as [s2' [C D]]. + intros. inv H0; simpl in H. + destruct (match_initial_states H1) as [s2 [A B]]. + destruct (simulation_star_star H2 B) as [s2' [C D]]. econstructor; eauto. - destruct (match_initial_states H0) as [s2 [A B]]. + destruct (match_initial_states H1) as [s2 [A B]]. econstructor; eauto. eapply simulation_star_forever; eauto. + contradiction. Qed. End SIMULATION_STAR_WF. @@ -448,16 +467,17 @@ Hypothesis simulation: Lemma simulation_star_preservation: forall beh, + not_wrong beh -> program_behaves step1 initial_state1 final_state1 ge1 beh -> program_behaves step2 initial_state2 final_state2 ge2 beh. Proof. intros. apply simulation_star_wf_preservation with (ltof _ measure). apply well_founded_ltof. intros. - destruct (simulation H0 H1) as [[st2' [A B]] | [A [B C]]]. + destruct (simulation H1 H2) as [[st2' [A B]] | [A [B C]]]. exists st2'; auto. exists st2; split. right; split. rewrite B. apply star_refl. auto. auto. - auto. + auto. auto. Qed. End SIMULATION_STAR. @@ -474,6 +494,7 @@ Hypothesis simulation: Lemma simulation_step_preservation: forall beh, + not_wrong beh -> program_behaves step1 initial_state1 final_state1 ge1 beh -> program_behaves step2 initial_state2 final_state2 ge2 beh. Proof. @@ -484,7 +505,7 @@ Proof. forall st2, match_states st1 st2 -> (exists st2', plus step2 ge2 st2 t st2' /\ match_states st1' st2') \/ (measure st1' < measure st1 /\ t = E0 /\ match_states st1' st2)%nat). - intros. destruct (simulation H0 H1) as [st2' [A B]]. + intros. destruct (simulation H1 H2) as [st2' [A B]]. left; exists st2'; split. apply plus_one; auto. auto. eapply simulation_star_preservation; eauto. Qed. @@ -503,6 +524,7 @@ Hypothesis simulation: Lemma simulation_plus_preservation: forall beh, + not_wrong beh -> program_behaves step1 initial_state1 final_state1 ge1 beh -> program_behaves step2 initial_state2 final_state2 ge2 beh. Proof. @@ -513,7 +535,7 @@ Proof. forall st2, match_states st1 st2 -> (exists st2', plus step2 ge2 st2 t st2' /\ match_states st1' st2') \/ (measure st1' < measure st1 /\ t = E0 /\ match_states st1' st2)%nat). - intros. destruct (simulation H0 H1) as [st2' [A B]]. + intros. destruct (simulation H1 H2) as [st2' [A B]]. left; exists st2'; auto. eapply simulation_star_preservation; eauto. Qed. @@ -538,6 +560,7 @@ Hypothesis simulation: Lemma simulation_opt_preservation: forall beh, + not_wrong beh -> program_behaves step1 initial_state1 final_state1 ge1 beh -> program_behaves step2 initial_state2 final_state2 ge2 beh. Proof. diff --git a/driver/Compiler.v b/driver/Compiler.v index 97bc19b..cbf7df8 100644 --- a/driver/Compiler.v +++ b/driver/Compiler.v @@ -228,29 +228,30 @@ Qed. Theorem transf_rtl_program_correct: forall p tp beh, transf_rtl_program p = OK tp -> + not_wrong beh -> RTL.exec_program p beh -> Asm.exec_program tp beh. Proof. intros. unfold transf_rtl_program, transf_rtl_fundef in H. - destruct (transform_partial_program_compose _ _ _ _ _ _ _ _ H) as [p7 [H7 P7]]. + destruct (transform_partial_program_compose _ _ _ _ _ _ _ _ H) as [p7 [X7 P7]]. clear H. - destruct (transform_partial_program_compose _ _ _ _ _ _ _ _ H7) as [p6 [H6 P6]]. - clear H7. - destruct (transform_partial_program_compose _ _ _ _ _ _ _ _ H6) as [p5 [H5 P5]]. - clear H6. generalize (transform_program_partial_program _ _ _ _ _ _ P5). clear P5. intro P5. - destruct (transform_partial_program_compose _ _ _ _ _ _ _ _ H5) as [p4 [H4 P4]]. - clear H5. - destruct (transform_partial_program_compose _ _ _ _ _ _ _ _ H4) as [p3 [H3 P3]]. - clear H4. generalize (transform_program_partial_program _ _ _ _ _ _ P3). clear P3. intro P3. - destruct (transform_partial_program_compose _ _ _ _ _ _ _ _ H3) as [p2 [H2 P2]]. - clear H3. - destruct (transform_program_compose _ _ _ _ _ _ _ _ H2) as [p1 [H1 P1]]. - clear H2. - destruct (transform_program_compose _ _ _ _ _ _ _ _ H1) as [p0 [H00 P0]]. - clear H1. - destruct (transform_program_compose _ _ _ _ _ _ _ _ H00) as [p00 [H000 P00]]. - clear H00. - generalize (transform_partial_program_identity _ _ _ _ H000). clear H000. intro. subst p00. + destruct (transform_partial_program_compose _ _ _ _ _ _ _ _ X7) as [p6 [X6 P6]]. + clear X7. + destruct (transform_partial_program_compose _ _ _ _ _ _ _ _ X6) as [p5 [X5 P5]]. + clear X6. generalize (transform_program_partial_program _ _ _ _ _ _ P5). clear P5. intro P5. + destruct (transform_partial_program_compose _ _ _ _ _ _ _ _ X5) as [p4 [X4 P4]]. + clear X5. + destruct (transform_partial_program_compose _ _ _ _ _ _ _ _ X4) as [p3 [X3 P3]]. + clear X4. generalize (transform_program_partial_program _ _ _ _ _ _ P3). clear P3. intro P3. + destruct (transform_partial_program_compose _ _ _ _ _ _ _ _ X3) as [p2 [X2 P2]]. + clear X3. + destruct (transform_program_compose _ _ _ _ _ _ _ _ X2) as [p1 [X1 P1]]. + clear X2. + destruct (transform_program_compose _ _ _ _ _ _ _ _ X1) as [p0 [X0 P0]]. + clear X1. + destruct (transform_program_compose _ _ _ _ _ _ _ _ X0) as [p00 [X00 P00]]. + clear X0. + generalize (transform_partial_program_identity _ _ _ _ X00). clear X00. intro. subst p00. assert (WT3 : LTLtyping.wt_program p3). apply Alloctyping.program_typing_preserved with p2. auto. @@ -268,28 +269,28 @@ Proof. apply Stackingproof.transf_program_correct with p6; auto. subst p6; apply Reloadproof.transf_program_correct; auto. apply Linearizeproof.transf_program_correct with p4; auto. - subst p4; apply Tunnelingproof.transf_program_correct. + subst p4; apply Tunnelingproof.transf_program_correct; auto. apply Allocproof.transf_program_correct with p2; auto. - subst p2; apply CSEproof.transf_program_correct. - subst p1; apply Constpropproof.transf_program_correct. - subst p0; apply Tailcallproof.transf_program_correct. - auto. + subst p2; apply CSEproof.transf_program_correct; auto. + subst p1; apply Constpropproof.transf_program_correct; auto. + subst p0; apply Tailcallproof.transf_program_correct; auto. Qed. Theorem transf_cminor_program_correct: forall p tp beh, transf_cminor_program p = OK tp -> + not_wrong beh -> Cminor.exec_program p beh -> Asm.exec_program tp beh. Proof. intros. unfold transf_cminor_program, transf_cminor_fundef in H. - destruct (transform_partial_program_compose _ _ _ _ _ _ _ _ H) as [p3 [H3 P3]]. + destruct (transform_partial_program_compose _ _ _ _ _ _ _ _ H) as [p3 [X3 P3]]. clear H. - destruct (transform_partial_program_compose _ _ _ _ _ _ _ _ H3) as [p2 [H2 P2]]. - clear H3. - destruct (transform_program_compose _ _ _ _ _ _ _ _ H2) as [p1 [H1 P1]]. - generalize (transform_partial_program_identity _ _ _ _ H1). clear H1. intro. subst p1. - apply transf_rtl_program_correct with p3. auto. + destruct (transform_partial_program_compose _ _ _ _ _ _ _ _ X3) as [p2 [X2 P2]]. + clear X3. + destruct (transform_program_compose _ _ _ _ _ _ _ _ X2) as [p1 [X1 P1]]. + generalize (transform_partial_program_identity _ _ _ _ X1). clear X1. intro. subst p1. + apply transf_rtl_program_correct with p3; auto. apply RTLgenproof.transf_program_correct with p2; auto. rewrite <- P1. apply Selectionproof.transf_program_correct; auto. Qed. @@ -297,6 +298,7 @@ Qed. Theorem transf_c_program_correct: forall p tp beh, transf_c_program p = OK tp -> + not_wrong beh -> Csem.exec_program p beh -> Asm.exec_program tp beh. Proof. @@ -304,7 +306,7 @@ Proof. caseEq (Ctyping.typecheck_program p); try congruence; intro. caseEq (Cshmgen.transl_program p); simpl; try congruence; intros p1 EQ1. caseEq (Cminorgen.transl_program p1); simpl; try congruence; intros p2 EQ2. - intros EQ3 SEM. + intros EQ3 NOTW SEM. eapply transf_cminor_program_correct; eauto. eapply Cminorgenproof.transl_program_correct; eauto. eapply Cshmgenproof3.transl_program_correct; eauto. diff --git a/driver/Complements.v b/driver/Complements.v index 8ee70bd..dfd3c45 100644 --- a/driver/Complements.v +++ b/driver/Complements.v @@ -224,10 +224,12 @@ Proof. intros. inv H; inv H0. reflexivity. Qed. +Definition nostep (ge: genv) (st: state) : Prop := forall t st', ~step ge st t st'. + Lemma final_state_not_step: - forall ge st r t st', final_state st r -> step ge st t st' -> False. + forall ge st r, final_state st r -> nostep ge st. Proof. - intros. inv H. inv H0. + unfold nostep. intros. red; intros. inv H. inv H0. unfold Vzero in H1. congruence. unfold Vzero in H1. congruence. Qed. @@ -242,21 +244,19 @@ Qed. Lemma steps_deterministic: forall ge s0 t1 s1, star step ge s0 t1 s1 -> - forall r1 r2 t2 s2 w0 w1 w2, star step ge s0 t2 s2 -> - final_state s1 r1 -> final_state s2 r2 -> + forall t2 s2 w0 w1 w2, star step ge s0 t2 s2 -> + nostep ge s1 -> nostep ge s2 -> possible_trace w0 t1 w1 -> possible_trace w0 t2 w2 -> - t1 = t2 /\ r1 = r2. + t1 = t2 /\ s1 = s2. Proof. induction 1; intros. - inv H. split. auto. eapply final_state_deterministic; eauto. - byContradiction. eapply final_state_not_step with (st := s); eauto. - inv H2. byContradiction. eapply final_state_not_step with (st := s0); eauto. + inv H. auto. + elim (H0 _ _ H4). + inv H2. elim (H4 _ _ H). possibleTraceInv. exploit step_deterministic. eexact H. eexact H7. eauto. eauto. intros [A [B C]]. subst s5 t3 w3. - exploit IHstar. eexact H8. eauto. eauto. eauto. eauto. - intros [A B]. subst t4 r2. - auto. + exploit IHstar; eauto. intros [A B]. split; congruence. Qed. (** ** Determinism for infinite transition sequences. *) @@ -281,14 +281,14 @@ Proof. Qed. Lemma star_final_not_forever: - forall ge s1 t s2 r T w1 w2, + forall ge s1 t s2 T w1 w2, star step ge s1 t s2 -> - final_state s2 r -> forever step ge s1 T -> + nostep ge s2 -> forever step ge s1 T -> possible_trace w1 t w2 -> possible_traceinf w1 T -> False. Proof. intros. exploit forever_star_inv; eauto. intros [T' [A [B C]]]. - inv A. eapply final_state_not_step; eauto. + inv A. elim (H0 _ _ H4). Qed. (** ** Minimal traces for divergence. *) @@ -472,7 +472,14 @@ Inductive exec_program' (p: program) (w: world): program_behavior -> Prop := forever step (Genv.globalenv p) s T -> possible_traceinf w T -> minimal_trace (Genv.globalenv p) s w T -> - exec_program' p w (Diverges T). + exec_program' p w (Diverges T) + | program_goes_wrong': forall s t s' w', + initial_state p s -> + star step (Genv.globalenv p) s t s' -> + possible_trace w t w' -> + nostep (Genv.globalenv p) s' -> + (forall r, ~final_state s' r) -> + exec_program' p w (Goes_wrong t). (** We show that any [exec_program] execution corresponds to an [exec_program'] execution. *) @@ -481,6 +488,7 @@ Definition possible_behavior (w: world) (b: program_behavior) : Prop := match b with | Terminates t r => exists w', possible_trace w t w' | Diverges T => possible_traceinf w T + | Goes_wrong t => exists w', possible_trace w t w' end. Inductive matching_behaviors: program_behavior -> program_behavior -> Prop := @@ -488,7 +496,9 @@ Inductive matching_behaviors: program_behavior -> program_behavior -> Prop := matching_behaviors (Terminates t r) (Terminates t r) | matching_behaviors_diverges: forall T1 T2, traceinf_prefix T2 T1 -> - matching_behaviors (Diverges T1) (Diverges T2). + matching_behaviors (Diverges T1) (Diverges T2) + | matching_behaviors_goeswrong: forall t , + matching_behaviors (Goes_wrong t) (Goes_wrong t). Theorem exec_program_program': forall p b w, @@ -505,6 +515,10 @@ Proof. exists (Diverges T0); split. econstructor; eauto. constructor. apply C; auto. + (* going wrong *) + destruct H0 as [w' A]. + exists (Goes_wrong t). + split. econstructor; eauto. constructor. Qed. (** Moreover, [exec_program'] is deterministic, in that the behavior @@ -516,7 +530,9 @@ Inductive same_behaviors: program_behavior -> program_behavior -> Prop := same_behaviors (Terminates t r) (Terminates t r) | same_behaviors_diverges: forall T1 T2, traceinf_sim T2 T1 -> - same_behaviors (Diverges T1) (Diverges T2). + same_behaviors (Diverges T1) (Diverges T2) + | same_behaviors_goes_wrong: forall t, + same_behaviors (Goes_wrong t) (Goes_wrong t). Theorem exec_program'_deterministic: forall p b1 b2 w, @@ -524,16 +540,35 @@ Theorem exec_program'_deterministic: same_behaviors b1 b2. Proof. intros. inv H; inv H0; - assert (s0 = s) by (eapply initial_state_deterministic; eauto); subst s0. + try (assert (s0 = s) by (eapply initial_state_deterministic; eauto); subst s0). (* terminates, terminates *) - exploit steps_deterministic. eexact H2. eexact H5. eauto. eauto. eauto. eauto. - intros [A B]. subst. constructor. + exploit steps_deterministic. eexact H2. eexact H5. + eapply final_state_not_step; eauto. eapply final_state_not_step; eauto. eauto. eauto. + intros [A B]. subst. + exploit final_state_deterministic. eexact H4. eexact H7. + intro. subst. constructor. (* terminates, diverges *) - byContradiction. eapply star_final_not_forever; eauto. + byContradiction. eapply star_final_not_forever; eauto. eapply final_state_not_step; eauto. + (* terminates, goes wrong *) + exploit steps_deterministic. eexact H2. eexact H5. + eapply final_state_not_step; eauto. auto. eauto. eauto. + intros [A B]. subst. elim (H8 _ H4). (* diverges, terminates *) - byContradiction. eapply star_final_not_forever; eauto. + byContradiction. eapply star_final_not_forever; eauto. eapply final_state_not_step; eauto. (* diverges, diverges *) constructor. apply traceinf_prefix_2_sim; auto. + (* diverges, goes wrong *) + byContradiction. eapply star_final_not_forever; eauto. + (* goes wrong, terminates *) + exploit steps_deterministic. eexact H2. eexact H6. eauto. + eapply final_state_not_step; eauto. eauto. eauto. + intros [A B]. subst. elim (H5 _ H8). + (* goes wrong, diverges *) + byContradiction. eapply star_final_not_forever; eauto. + (* goes wrong, goes wrong *) + exploit steps_deterministic. eexact H2. eexact H6. + eauto. eauto. eauto. eauto. + intros [A B]. subst. constructor. Qed. Lemma matching_behaviors_same: @@ -545,6 +580,7 @@ Proof. constructor. constructor. apply traceinf_prefix_compat with T2 T1. auto. apply traceinf_sim_sym; auto. apply traceinf_sim_refl. + constructor. Qed. (** * Additional semantic preservation property *) @@ -559,23 +595,18 @@ Qed. predicate. *) Theorem transf_c_program_correct_strong: - forall p tp b w, + forall p tp w, transf_c_program p = OK tp -> - Csem.exec_program p b -> - possible_behavior w b -> - (exists b', exec_program' tp w b') -/\(forall b', exec_program' tp w b' -> - exists b0, Csem.exec_program p b0 /\ matching_behaviors b0 b'). + (exists b, Csem.exec_program p b /\ possible_behavior w b /\ not_wrong b) -> + (forall b, exec_program' tp w b -> exists b0, Csem.exec_program p b0 /\ matching_behaviors b0 b). Proof. - intros. - assert (Asm.exec_program tp b). + intros. destruct H0 as [b0 [A [B C]]]. + assert (Asm.exec_program tp b0). eapply transf_c_program_correct; eauto. exploit exec_program_program'; eauto. - intros [b' [A B]]. - split. exists b'; auto. - intros. exists b. split. auto. - apply matching_behaviors_same with b'. auto. - eapply exec_program'_deterministic; eauto. + intros [b1 [D E]]. + assert (same_behaviors b1 b). eapply exec_program'_deterministic; eauto. + exists b0. split. auto. eapply matching_behaviors_same; eauto. Qed. Section SPECS_PRESERVED. @@ -601,28 +632,24 @@ Hypothesis spec_safety: forall T T', traceinf_prefix T T' -> spec (Diverges T') -> spec (Diverges T). Theorem transf_c_program_preserves_spec: - forall p tp b w, + forall p tp w, transf_c_program p = OK tp -> - Csem.exec_program p b -> - possible_behavior w b -> - spec b -> - (exists b', exec_program' tp w b') -/\(forall b', exec_program' tp w b' -> spec b'). + (exists b, Csem.exec_program p b /\ possible_behavior w b /\ not_wrong b) -> + (forall b, Csem.exec_program p b -> possible_behavior w b -> spec b) -> + (forall b, exec_program' tp w b -> not_wrong b /\ spec b). Proof. - intros. - assert (Asm.exec_program tp b). + intros. destruct H0 as [b1 [A [B C]]]. + assert (Asm.exec_program tp b1). eapply transf_c_program_correct; eauto. exploit exec_program_program'; eauto. - intros [b' [A B]]. - split. exists b'; auto. - intros b'' EX. - assert (same_behaviors b' b''). eapply exec_program'_deterministic; eauto. - inv B; inv H4. + intros [b' [D E]]. + assert (same_behaviors b b'). eapply exec_program'_deterministic; eauto. + inv E; inv H3. auto. - apply spec_safety with T1. - eapply traceinf_prefix_compat with T2 T1. - auto. apply traceinf_sim_sym; auto. apply traceinf_sim_refl. + split. simpl. auto. apply spec_safety with T1. + eapply traceinf_prefix_compat. eauto. auto. apply traceinf_sim_refl. auto. + simpl in C. contradiction. Qed. End SPECS_PRESERVED. diff --git a/lib/Coqlib.v b/lib/Coqlib.v index 9e2199c..416afa9 100644 --- a/lib/Coqlib.v +++ b/lib/Coqlib.v @@ -781,6 +781,11 @@ Proof. right; red; intros. elim n0. eapply list_disjoint_cons_left; eauto. Defined. +(** [list_equiv l1 l2] holds iff the lists [l1] and [l2] contain the same elements. *) + +Definition list_equiv (A : Type) (l1 l2: list A) : Prop := + forall x, In x l1 <-> In x l2. + (** [list_norepet l] holds iff the list [l] contains no repetitions, i.e. no element occurs twice. *) @@ -74,6 +74,9 @@ Module Type TREE. Hypothesis gro: forall (A: Type) (i j: elt) (m: t A), i <> j -> get i (remove j m) = get i m. + Hypothesis grspec: + forall (A: Type) (i j: elt) (m: t A), + get i (remove j m) = if elt_eq i j then None else get i m. (** Extensional equality between trees. *) Variable beq: forall (A: Type), (A -> A -> bool) -> t A -> t A -> bool. @@ -333,6 +336,13 @@ Module PTree <: TREE. auto. Qed. + Theorem grspec: + forall (A: Type) (i j: elt) (m: t A), + get i (remove j m) = if elt_eq i j then None else get i m. + Proof. + intros. destruct (elt_eq i j). subst j. apply grs. apply gro; auto. + Qed. + Section EXTENSIONAL_EQUALITY. Variable A: Type. @@ -1127,6 +1137,111 @@ Module EMap(X: EQUALITY_TYPE) <: MAP. Qed. End EMap. +(** * Additional properties over trees *) + +Module Tree_Properties(T: TREE). + +(** An induction principle over [fold]. *) + +Section TREE_FOLD_IND. + +Variables V A: Type. +Variable f: A -> T.elt -> V -> A. +Variable P: T.t V -> A -> Prop. +Variable init: A. +Variable m_final: T.t V. + +Hypothesis P_compat: + forall m m' a, + (forall x, T.get x m = T.get x m') -> + P m a -> P m' a. + +Hypothesis H_base: + P (T.empty _) init. + +Hypothesis H_rec: + forall m a k v, + T.get k m = None -> T.get k m_final = Some v -> P m a -> P (T.set k v m) (f a k v). + +Definition f' (a: A) (p : T.elt * V) := f a (fst p) (snd p). + +Definition P' (l: list (T.elt * V)) (a: A) : Prop := + forall m, list_equiv l (T.elements m) -> P m a. + +Remark H_base': + P' nil init. +Proof. + red; intros. apply P_compat with (T.empty _); auto. + intros. rewrite T.gempty. symmetry. case_eq (T.get x m); intros; auto. + assert (In (x, v) nil). rewrite (H (x, v)). apply T.elements_correct. auto. + contradiction. +Qed. + +Remark H_rec': + forall k v l a, + ~In k (List.map (@fst T.elt V) l) -> + In (k, v) (T.elements m_final) -> + P' l a -> + P' (l ++ (k, v) :: nil) (f a k v). +Proof. + unfold P'; intros. + set (m0 := T.remove k m). + apply P_compat with (T.set k v m0). + intros. unfold m0. rewrite T.gsspec. destruct (T.elt_eq x k). + symmetry. apply T.elements_complete. rewrite <- (H2 (x, v)). + apply in_or_app. simpl. intuition congruence. + apply T.gro. auto. + apply H_rec. unfold m0. apply T.grs. apply T.elements_complete. auto. + apply H1. red. intros [k' v']. + split; intros. + apply T.elements_correct. unfold m0. rewrite T.gro. apply T.elements_complete. + rewrite <- (H2 (k', v')). apply in_or_app. auto. + red; intro; subst k'. elim H. change k with (fst (k, v')). apply in_map. auto. + assert (T.get k' m0 = Some v'). apply T.elements_complete. auto. + unfold m0 in H4. rewrite T.grspec in H4. destruct (T.elt_eq k' k). congruence. + assert (In (k', v') (T.elements m)). apply T.elements_correct; auto. + rewrite <- (H2 (k', v')) in H5. destruct (in_app_or _ _ _ H5). auto. + simpl in H6. intuition congruence. +Qed. + +Lemma fold_rec_aux: + forall l1 l2 a, + list_equiv (l2 ++ l1) (T.elements m_final) -> + list_disjoint (List.map (@fst T.elt V) l1) (List.map (@fst T.elt V) l2) -> + list_norepet (List.map (@fst T.elt V) l1) -> + P' l2 a -> P' (l2 ++ l1) (List.fold_left f' l1 a). +Proof. + induction l1; intros; simpl. + rewrite <- List.app_nil_end. auto. + destruct a as [k v]; simpl in *. inv H1. + change ((k, v) :: l1) with (((k, v) :: nil) ++ l1). rewrite <- List.app_ass. apply IHl1. + rewrite app_ass. auto. + red; intros. rewrite map_app in H3. destruct (in_app_or _ _ _ H3). apply H0; auto with coqlib. + simpl in H4. intuition congruence. + auto. + unfold f'. simpl. apply H_rec'; auto. eapply list_disjoint_notin; eauto with coqlib. + rewrite <- (H (k, v)). apply in_or_app. simpl. auto. +Qed. + +Theorem fold_rec: + P m_final (T.fold f m_final init). +Proof. + intros. rewrite T.fold_spec. fold f'. + assert (P' (nil ++ T.elements m_final) (List.fold_left f' (T.elements m_final) init)). + apply fold_rec_aux. + simpl. red; intros; tauto. + simpl. red; intros. elim H0. + apply T.elements_keys_norepet. + apply H_base'. + simpl in H. red in H. apply H. red; intros. tauto. +Qed. + +End TREE_FOLD_IND. + +End Tree_Properties. + +Module PTree_Properties := Tree_Properties(PTree). + (** * Useful notations *) Notation "a ! b" := (PTree.get b a) (at level 1). diff --git a/powerpc/Asmgenproof.v b/powerpc/Asmgenproof.v index 40c593a..0c1edec 100644 --- a/powerpc/Asmgenproof.v +++ b/powerpc/Asmgenproof.v @@ -1322,7 +1322,7 @@ Proof. Qed. Theorem transf_program_correct: - forall (beh: program_behavior), + forall (beh: program_behavior), not_wrong beh -> Machconcr.exec_program prog beh -> Asm.exec_program tprog beh. Proof. unfold Machconcr.exec_program, Asm.exec_program; intros. diff --git a/powerpc/Constpropproof.v b/powerpc/Constpropproof.v index dbd498f..fb01f75 100644 --- a/powerpc/Constpropproof.v +++ b/powerpc/Constpropproof.v @@ -931,7 +931,7 @@ Qed. [Smallstep.simulation_step_preservation]. *) Theorem transf_program_correct: - forall (beh: program_behavior), + forall (beh: program_behavior), not_wrong beh -> exec_program prog beh -> exec_program tprog beh. Proof. unfold exec_program; intros. diff --git a/powerpc/Selectionproof.v b/powerpc/Selectionproof.v index 8a02c99..27e9ee4 100644 --- a/powerpc/Selectionproof.v +++ b/powerpc/Selectionproof.v @@ -1420,7 +1420,7 @@ Proof. Qed. Theorem transf_program_correct: - forall (beh: program_behavior), + forall (beh: program_behavior), not_wrong beh -> Cminor.exec_program prog beh -> CminorSel.exec_program tprog beh. Proof. unfold CminorSel.exec_program, Cminor.exec_program; intros. |