From bdc7b815d033f84e5538a1c8db87d3c061b1ca4c Mon Sep 17 00:00:00 2001
From: xleroy <xleroy@fca1b0fc-160b-0410-b1d3-a4f43f01ea2e>
Date: Wed, 5 Aug 2009 14:40:34 +0000
Subject: [PATCH] Added 'going wrong' behaviors
git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@1120 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
---
.depend | 5 +-
Makefile | 2 +-
arm/Asmgenproof.v | 2 +-
arm/Constpropproof.v | 2 +-
arm/Selectionproof.v | 2 +-
backend/Allocproof.v | 2 +-
backend/CSEproof.v | 2 +-
backend/Linearizeproof.v | 2 +-
backend/Machabstr2concr.v | 6 +-
backend/RTLgenproof.v | 2 +-
backend/Reloadproof.v | 2 +-
backend/Stackingproof.v | 2 +-
backend/Tailcallproof.v | 2 +-
backend/Tunneling.v | 51 ++++-----
backend/Tunnelingproof.v | 221 +++++++++++++++++++------------------
backend/Tunnelingtyping.v | 40 ++++---
cfrontend/Cminorgenproof.v | 2 +-
cfrontend/Cshmgenproof3.v | 13 ++-
common/Smallstep.v | 45 ++++++--
driver/Compiler.v | 62 ++++++-----
driver/Complements.v | 129 +++++++++++++---------
lib/Coqlib.v | 5 +
lib/Maps.v | 115 +++++++++++++++++++
powerpc/Asmgenproof.v | 2 +-
powerpc/Constpropproof.v | 2 +-
powerpc/Selectionproof.v | 2 +-
26 files changed, 449 insertions(+), 273 deletions(-)
diff --git a/.depend b/.depend
index d1b9ef8fe..c6df7798f 100644
--- a/.depend
+++ b/.depend
@@ -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
diff --git a/Makefile b/Makefile
index 14b8c29be..8bae5a05a 100644
--- a/Makefile
+++ b/Makefile
@@ -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 f9f4cd0f8..7b1fd62c8 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 7c7b87884..08c5baf34 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 967e2292c..cf7613b61 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 e2387b5d0..7e9334a87 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 265bb20ab..3751cec74 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 c24d37042..1fb068d8b 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 6e331f30b..139eac75c 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 1dd2294c0..df1ade9dd 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 ea7c5d194..a7becc36c 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 d5819f7ef..5b6f2dc7b 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 791db3742..1423e1e01 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 32d1b5955..4b1417fc5 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 08f5f6ccb..eccb62dd4 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 57e1271d1..91745dfbe 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 1a68c1030..984381a33 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 92a095627..6a8b676f8 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 f41fe4ed1..9e9063b08 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 97bc19b1e..cbf7df870 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 8ee70bdde..dfd3c4547 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 9e2199c12..416afa9cb 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. *)
diff --git a/lib/Maps.v b/lib/Maps.v
index a277e6772..766168ac4 100644
--- a/lib/Maps.v
+++ b/lib/Maps.v
@@ -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 40c593a34..0c1edec2f 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 dbd498f93..fb01f75bf 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 8a02c9975..27e9ee472 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.
--
GitLab