summaryrefslogtreecommitdiff
diff options
context:
space:
mode:
-rw-r--r--cfrontend/Cexec.v14
-rw-r--r--cfrontend/Cminorgenproof.v99
-rw-r--r--cfrontend/Csem.v34
-rw-r--r--cfrontend/Csharpminor.v9
-rw-r--r--cfrontend/Cshmgen.v27
-rw-r--r--cfrontend/Cshmgenproof.v12
-rw-r--r--common/Determinism.v19
-rw-r--r--common/Events.v21
-rw-r--r--common/Memdata.v8
-rw-r--r--common/Memory.v10
-rw-r--r--ia32/Asmgenproof1.v24
-rw-r--r--ia32/Asmgenretaddr.v17
-rw-r--r--ia32/standard/Stacklayout.v10
-rw-r--r--lib/Maps.v5
-rw-r--r--powerpc/Asmgenproof.v8
-rw-r--r--powerpc/Asmgenproof1.v10
16 files changed, 1 insertions, 326 deletions
diff --git a/cfrontend/Cexec.v b/cfrontend/Cexec.v
index 383eeb8..e3b57c5 100644
--- a/cfrontend/Cexec.v
+++ b/cfrontend/Cexec.v
@@ -1653,20 +1653,6 @@ Definition do_step (w: world) (s: state) : list (trace * state) :=
| _ => nil
end.
-(*
-Definition at_external (S: state): option (external_function * list val * mem) :=
- match S with
- | Callstate (External ef _ _) vargs k m => Some (ef, vargs, m)
- | _ => None
- end.
-
-Definition after_external (S: state) (v: val) (m: mem): option state :=
- match S with
- | Callstate _ _ k _ => Some (Returnstate v k m)
- | _ => None
- end.
-*)
-
Ltac myinv :=
match goal with
| [ |- In _ nil -> _ ] => intro X; elim X
diff --git a/cfrontend/Cminorgenproof.v b/cfrontend/Cminorgenproof.v
index 0590a60..10ffbe4 100644
--- a/cfrontend/Cminorgenproof.v
+++ b/cfrontend/Cminorgenproof.v
@@ -479,10 +479,6 @@ Lemma match_env_alloc_same:
Proof.
intros until tv.
intros ME ALLOC INCR ACOND OTHER TE E.
-(*
- assert (ALLOC_RES: b = Mem.nextblock m1) by eauto with mem.
- assert (ALLOC_NEXT: Mem.nextblock m2 = Zsucc(Mem.nextblock m1)) by eauto with mem.
-*)
inv ME; constructor.
(* vars *)
intros. rewrite PMap.gsspec. destruct (peq id0 id). subst id0.
@@ -901,22 +897,6 @@ Proof.
exists id; exists lv; intuition. apply PTree.elements_complete. auto.
Qed.
-(*
-Lemma free_list_perm:
- forall l m m',
- Mem.free_list m l = Some m' ->
- forall b ofs p,
- Mem.perm m' b ofs p -> Mem.perm m b ofs p.
-Proof.
- induction l; simpl; intros.
- inv H; auto.
- revert H. destruct a as [[b' lo'] hi'].
- caseEq (Mem.free m b' lo' hi'); try congruence.
- intros m1 FREE1 FREE2.
- eauto with mem.
-Qed.
-*)
-
Lemma match_callstack_freelist:
forall f cenv tf e le te sp lo hi cs m m' tm,
Mem.inject f m tm ->
@@ -1662,85 +1642,6 @@ Proof.
eapply match_callstack_store_mapped; eauto.
Qed.
-(*
-Lemma var_set_self_correct:
- forall cenv id ty s a f tf e le te sp lo hi m cs tm tv te' v m' fn k,
- var_set_self cenv id ty s = OK a ->
- match_callstack f m tm (Frame cenv tf e le te sp lo hi :: cs) (Mem.nextblock m) (Mem.nextblock tm) ->
- val_inject f v tv ->
- Mem.inject f m tm ->
- exec_assign ge e m id v m' ->
- te'!(for_var id) = Some tv ->
- (forall i, i <> for_var id -> te'!i = te!i) ->
- exists te'', exists tm',
- star step tge (State fn a k (Vptr sp Int.zero) te' tm)
- E0 (State fn s k (Vptr sp Int.zero) te'' tm') /\
- Mem.inject f m' tm' /\
- match_callstack f m' tm' (Frame cenv tf e le te'' sp lo hi :: cs) (Mem.nextblock m') (Mem.nextblock tm') /\
- (forall id', id' <> for_var id -> te''!id' = te'!id').
-Proof.
- intros until k.
- intros VS MCS VINJ MINJ ASG VAL OTHERS.
- unfold var_set_self in VS. inv ASG.
- assert (NEXTBLOCK: Mem.nextblock m' = Mem.nextblock m).
- eapply Mem.nextblock_store; eauto.
- assert (MV: match_var f id e m te sp cenv!!id).
- inv MCS. inv MENV. auto.
- assert (EVAR: eval_expr tge (Vptr sp Int.zero) te' tm (Evar (for_var id)) tv).
- constructor. auto.
- revert VS; inv MV; intro VS; inv VS; inv H; try congruence.
- (* var_local *)
- assert (b0 = b) by congruence. subst b0.
- assert (chunk0 = chunk) by congruence. subst chunk0.
- exists te'; exists tm.
- split. apply star_refl.
- split. eapply Mem.store_unmapped_inject; eauto.
- split. rewrite NEXTBLOCK.
- apply match_callstack_extensional with (PTree.set (for_var id) tv te).
- intros. repeat rewrite PTree.gsspec.
- destruct (peq (for_var id0) (for_var id)). congruence. auto.
- intros. assert (for_temp id0 <> for_var id). unfold for_temp, for_var; congruence.
- rewrite PTree.gso; auto.
- eapply match_callstack_store_local; eauto.
- intros. auto.
- (* var_stack_scalar *)
- assert (b0 = b) by congruence. subst b0.
- assert (chunk0 = chunk) by congruence. subst chunk0.
- assert (Mem.storev chunk m (Vptr b Int.zero) v = Some m'). assumption.
- exploit make_store_correct.
- eapply make_stackaddr_correct.
- eauto. eauto. eauto. eauto. eauto.
- intros [tm' [tvrhs' [EVAL' [STORE' MEMINJ]]]].
- exists te'; exists tm'.
- split. eapply star_three. constructor. eauto. constructor. traceEq.
- split. auto.
- split. rewrite NEXTBLOCK. rewrite (nextblock_storev _ _ _ _ _ STORE').
- apply match_callstack_extensional with te.
- intros. apply OTHERS. unfold for_var; congruence.
- intros. apply OTHERS. unfold for_var, for_temp; congruence.
- eapply match_callstack_storev_mapped; eauto.
- auto.
- (* var_global_scalar *)
- simpl in *.
- assert (chunk0 = chunk). exploit H4; eauto. congruence. subst chunk0.
- assert (Mem.storev chunk m (Vptr b Int.zero) v = Some m'). assumption.
- exploit match_callstack_match_globalenvs; eauto. intros [bnd MG]. inv MG.
- exploit make_store_correct.
- eapply make_globaladdr_correct; eauto.
- rewrite symbols_preserved; eauto. eauto. eauto. eauto. eauto. eauto.
- intros [tm' [tvrhs' [EVAL' [STORE' MEMINJ]]]].
- exists te'; exists tm'.
- split. eapply star_three. constructor. eauto. constructor. traceEq.
- split. auto.
- split. rewrite NEXTBLOCK. rewrite (nextblock_storev _ _ _ _ _ STORE').
- apply match_callstack_extensional with te.
- intros. apply OTHERS. unfold for_var; congruence.
- intros. apply OTHERS. unfold for_var, for_temp; congruence.
- eapply match_callstack_store_mapped; eauto.
- auto.
-Qed.
-*)
-
(** * Correctness of stack allocation of local variables *)
(** This section shows the correctness of the translation of Csharpminor
diff --git a/cfrontend/Csem.v b/cfrontend/Csem.v
index 90bb2e3..426a753 100644
--- a/cfrontend/Csem.v
+++ b/cfrontend/Csem.v
@@ -61,40 +61,6 @@ Definition cast_float_float (sz: floatsize) (f: float) : float :=
| F64 => f
end.
-(*
-Definition neutral_for_cast (t: type) : bool :=
- match t with
- | Tint I32 sg => true
- | Tpointer ty => true
- | Tarray ty sz => true
- | Tfunction targs tres => true
- | _ => false
- end.
-
-Function sem_cast (v: val) (t1 t2: type) : option val :=
- match v, t1, t2 with
- | Vint i, Tint sz1 si1, Tint sz2 si2 => (**r int to int *)
- Some (Vint (cast_int_int sz2 si2 i))
- | Vfloat f, Tfloat sz1, Tint sz2 si2 => (**r float to int *)
- match cast_float_int si2 f with
- | Some i => Some (Vint (cast_int_int sz2 si2 i))
- | None => None
- end
- | Vint i, Tint sz1 si1, Tfloat sz2 => (**r int to float *)
- Some (Vfloat (cast_float_float sz2 (cast_int_float si1 i)))
- | Vfloat f, Tfloat sz1, Tfloat sz2 => (**r float to float *)
- Some (Vfloat (cast_float_float sz2 f))
- | Vptr b ofs, _, _ => (**r int32|pointer to int32|pointer *)
- if neutral_for_cast t1 && neutral_for_cast t2
- then Some(Vptr b ofs) else None
- | Vint n, _, _ => (**r int32|pointer to int32|pointer *)
- if neutral_for_cast t1 && neutral_for_cast t2
- then Some(Vint n) else None
- | _, _, _ =>
- None
- end.
-*)
-
Function sem_cast (v: val) (t1 t2: type) : option val :=
match classify_cast t1 t2 with
| cast_case_neutral =>
diff --git a/cfrontend/Csharpminor.v b/cfrontend/Csharpminor.v
index c192e46..a1ed8b3 100644
--- a/cfrontend/Csharpminor.v
+++ b/cfrontend/Csharpminor.v
@@ -416,15 +416,6 @@ Inductive exec_assign: env -> mem -> ident -> val -> mem -> Prop :=
Mem.store chunk m b 0 v = Some m' ->
exec_assign e m id v m'.
-(*
-Inductive exec_opt_assign: env -> mem -> option ident -> val -> mem -> Prop :=
- | exec_assign_none: forall e m v,
- exec_opt_assign e m None v m
- | exec_assign_some: forall e m id v m',
- exec_assign e m id v m' ->
- exec_opt_assign e m (Some id) v m'.
-*)
-
(** One step of execution *)
Inductive step: state -> trace -> state -> Prop :=
diff --git a/cfrontend/Cshmgen.v b/cfrontend/Cshmgen.v
index 9856b9e..bbd4cfe 100644
--- a/cfrontend/Cshmgen.v
+++ b/cfrontend/Cshmgen.v
@@ -209,32 +209,7 @@ Definition make_cmp (c: comparison) (e1: expr) (ty1: type) (e2: expr) (ty2: type
end.
(** [make_cast from to e] applies to [e] the numeric conversions needed
- to transform a result of type [from] to a result of type [to].
- It is decomposed in two functions:
-- [make_cast1] converts from integers to floats or from floats to integers;
-- [make_cast2] converts to a "small" int or float type if necessary.
-*)
-(*
-Definition make_cast1 (from to: type) (e: expr) :=
- match from, to with
- | Tint _ uns, Tfloat _ => make_floatofint e uns
- | Tfloat _, Tint _ uns => make_intoffloat e uns
- | _, _ => e
- end.
-
-Definition make_cast2 (from to: type) (e: expr) :=
- match to with
- | Tint I8 Signed => Eunop Ocast8signed e
- | Tint I8 Unsigned => Eunop Ocast8unsigned e
- | Tint I16 Signed => Eunop Ocast16signed e
- | Tint I16 Unsigned => Eunop Ocast16unsigned e
- | Tfloat F32 => Eunop Osingleoffloat e
- | _ => e
- end.
-
-Definition make_cast (from to: type) (e: expr) :=
- make_cast2 from to (make_cast1 from to e).
-*)
+ to transform a result of type [from] to a result of type [to]. *)
Definition make_cast_int (e: expr) (sz: intsize) (si: signedness) :=
match sz, si with
diff --git a/cfrontend/Cshmgenproof.v b/cfrontend/Cshmgenproof.v
index fa9ba1d..db5b7bc 100644
--- a/cfrontend/Cshmgenproof.v
+++ b/cfrontend/Cshmgenproof.v
@@ -494,18 +494,6 @@ Definition binary_constructor_correct
eval_expr ge e le m b vb ->
eval_expr ge e le m c v.
-(*
-Definition binary_constructor_correct'
- (make: expr -> type -> expr -> type -> res expr)
- (sem: val -> val -> option val): Prop :=
- forall a tya b tyb c va vb v e le m,
- sem va vb = Some v ->
- make a tya b tyb = OK c ->
- eval_expr ge e le m a va ->
- eval_expr ge e le m b vb ->
- eval_expr ge e le m c v.
-*)
-
Lemma make_add_correct: binary_constructor_correct make_add sem_add.
Proof.
red; intros until m. intro SEM. unfold make_add.
diff --git a/common/Determinism.v b/common/Determinism.v
index 29cc695..778ba22 100644
--- a/common/Determinism.v
+++ b/common/Determinism.v
@@ -126,25 +126,6 @@ Proof.
inv H4; inv H3. inv H7; inv H6. auto.
Qed.
-(*
-Lemma possible_event_final_world:
- forall w ev w1 w2,
- possible_event w ev w1 -> possible_event w ev w2 -> w1 = w2.
-Proof.
- intros. inv H; inv H0; congruence.
-Qed.
-
-Lemma possible_trace_final_world:
- forall w0 t w1, possible_trace w0 t w1 ->
- forall w2, possible_trace w0 t w2 -> w1 = w2.
-Proof.
- induction 1; intros.
- inv H. auto.
- inv H1. assert (w2 = w5) by (eapply possible_event_final_world; eauto).
- subst; eauto.
-Qed.
-*)
-
CoInductive possible_traceinf: world -> traceinf -> Prop :=
| possible_traceinf_cons: forall w1 ev w2 T,
possible_event w1 ev w2 ->
diff --git a/common/Events.v b/common/Events.v
index 3948640..f18c091 100644
--- a/common/Events.v
+++ b/common/Events.v
@@ -1044,18 +1044,6 @@ Proof.
intros. inv H.
inv H1. inv H13. inv H14. inv H10. inv H11.
exploit Mem.loadbytes_length; eauto. intros LEN.
-(*
- destruct (zle sz 0).
- (* empty copy *)
- rewrite nat_of_Z_neg in LEN; auto.
- assert (bytes = nil). destruct bytes; simpl in LEN; congruence.
- subst. rewrite Mem.storebytes_empty in H8. inv H8.
- exists Vundef; exists m1'.
- split. econstructor; eauto. rewrite Mem.loadbytes_empty; eauto.
- apply Mem.storebytes_empty.
- split. constructor. split. auto. red; auto.
- (* nonempty copy *)
-*)
exploit Mem.loadbytes_extends; eauto. intros [bytes2 [A B]].
exploit Mem.storebytes_within_extends; eauto. intros [m2' [C D]].
exists Vundef; exists m2'.
@@ -1079,15 +1067,6 @@ Proof.
(* injections *)
intros. inv H0. inv H2. inv H14. inv H15. inv H11. inv H12.
exploit Mem.loadbytes_length; eauto. intros LEN.
-(*
- destruct (zle sz 0).
- (* empty copy *)
- rewrite nat_of_Z_neg in LEN; auto.
- assert (bytes = nil). destruct bytes; simpl in LEN; congruence.
- subst. rewrite Mem.storebytes_empty in H9. inv H9.
- exists f; exists Vundef; exists m1'.
- split. econstructor; eauto.
-*)
assert (RPSRC: Mem.range_perm m1 bsrc (Int.unsigned osrc) (Int.unsigned osrc + sz) Nonempty).
eapply Mem.range_perm_implies. eapply Mem.loadbytes_range_perm; eauto. auto with mem.
assert (RPDST: Mem.range_perm m1 bdst (Int.unsigned odst) (Int.unsigned odst + sz) Nonempty).
diff --git a/common/Memdata.v b/common/Memdata.v
index 16adb23..fde8b47 100644
--- a/common/Memdata.v
+++ b/common/Memdata.v
@@ -534,14 +534,6 @@ Definition decode_val (chunk: memory_chunk) (vl: list memval) : val :=
end
end.
-(*
-Lemma inj_pointer_length:
- forall b ofs n, List.length(inj_pointer n b ofs) = n.
-Proof.
- induction n; simpl; congruence.
-Qed.
-*)
-
Lemma encode_val_length:
forall chunk v, length(encode_val chunk v) = size_chunk_nat chunk.
Proof.
diff --git a/common/Memory.v b/common/Memory.v
index b456191..157867e 100644
--- a/common/Memory.v
+++ b/common/Memory.v
@@ -947,16 +947,6 @@ Variable ofs: Z.
Variable v: val.
Variable m2: mem.
Hypothesis STORE: store chunk m1 b ofs v = Some m2.
-(*
-Lemma store_result:
- m2 = unchecked_store chunk m1 b ofs v.
-Proof.
- unfold store in STORE.
- destruct (valid_access_dec m1 chunk b ofs Writable).
- congruence.
- congruence.
-Qed.
-*)
Lemma store_access: mem_access m2 = mem_access m1.
Proof.
diff --git a/ia32/Asmgenproof1.v b/ia32/Asmgenproof1.v
index c00332e..be40f3d 100644
--- a/ia32/Asmgenproof1.v
+++ b/ia32/Asmgenproof1.v
@@ -232,30 +232,6 @@ Qed.
Hint Resolve nontemp_diff: ppcgen.
-(*
-Remark undef_regs_1:
- forall l ms r, ms r = Vundef -> Mach.undef_regs l ms r = Vundef.
-Proof.
- induction l; simpl; intros. auto. apply IHl. unfold Regmap.set.
- destruct (RegEq.eq r a); congruence.
-Qed.
-
-Remark undef_regs_2:
- forall l ms r, In r l -> Mach.undef_regs l ms r = Vundef.
-Proof.
- induction l; simpl; intros. contradiction.
- destruct H. subst. apply undef_regs_1. apply Regmap.gss.
- auto.
-Qed.
-
-Remark undef_regs_3:
- forall l ms r, ~In r l -> Mach.undef_regs l ms r = ms r.
-Proof.
- induction l; simpl; intros. auto.
- rewrite IHl. apply Regmap.gso. intuition. intuition.
-Qed.
-*)
-
Lemma agree_exten_temps:
forall ms sp rs rs',
agree ms sp rs ->
diff --git a/ia32/Asmgenretaddr.v b/ia32/Asmgenretaddr.v
index e963c2e..1a1ea20 100644
--- a/ia32/Asmgenretaddr.v
+++ b/ia32/Asmgenretaddr.v
@@ -90,23 +90,6 @@ Qed.
Hint Resolve is_tail_refl: ppcretaddr.
-(*
-Ltac IsTail :=
- auto with ppcretaddr;
- match goal with
- | [ |- is_tail _ (_ :: _) ] => constructor; IsTail
- | [ |- is_tail _ (match ?x with true => _ | false => _ end) ] => destruct x; IsTail
- | [ |- is_tail _ (match ?x with left _ => _ | right _ => _ end) ] => destruct x; IsTail
- | [ |- is_tail _ (match ?x with nil => _ | _ :: _ => _ end) ] => destruct x; IsTail
- | [ |- is_tail _ (match ?x with Tint => _ | Tfloat => _ end) ] => destruct x; IsTail
- | [ |- is_tail _ (?f _ _ _ _ _ _ ?k) ] => apply is_tail_trans with k; IsTail
- | [ |- is_tail _ (?f _ _ _ _ _ ?k) ] => apply is_tail_trans with k; IsTail
- | [ |- is_tail _ (?f _ _ _ _ ?k) ] => apply is_tail_trans with k; IsTail
- | [ |- is_tail _ (?f _ _ _ ?k) ] => apply is_tail_trans with k; IsTail
- | [ |- is_tail _ (?f _ _ ?k) ] => apply is_tail_trans with k; IsTail
- | _ => idtac
- end.
-*)
Ltac IsTail :=
eauto with ppcretaddr;
match goal with
diff --git a/ia32/standard/Stacklayout.v b/ia32/standard/Stacklayout.v
index 1fa3fb3..063fb4f 100644
--- a/ia32/standard/Stacklayout.v
+++ b/ia32/standard/Stacklayout.v
@@ -138,13 +138,3 @@ Proof.
tauto.
Qed.
-(*
-Remark align_float_part:
- forall b,
- 4 * bound_outgoing b + 4 + 4 + 4 * bound_int_local b + 4 * bound_int_callee_save b <=
- align (4 * bound_outgoing b + 4 + 4 + 4 * bound_int_local b + 4 * bound_int_callee_save b) 8.
-
-Proof.
- intros. apply align_le. omega.
-Qed.
-*) \ No newline at end of file
diff --git a/lib/Maps.v b/lib/Maps.v
index 793c223..f8d1bd5 100644
--- a/lib/Maps.v
+++ b/lib/Maps.v
@@ -998,11 +998,6 @@ Module PTree <: TREE.
destruct H0. congruence.
Qed.
-(*
- Definition fold (A B : Type) (f: B -> positive -> A -> B) (tr: t A) (v: B) :=
- List.fold_left (fun a p => f a (fst p) (snd p)) (elements tr) v.
-*)
-
Fixpoint xfold (A B: Type) (f: B -> positive -> A -> B)
(i: positive) (m: t A) (v: B) {struct m} : B :=
match m with
diff --git a/powerpc/Asmgenproof.v b/powerpc/Asmgenproof.v
index d22bc3d..27b2108 100644
--- a/powerpc/Asmgenproof.v
+++ b/powerpc/Asmgenproof.v
@@ -114,14 +114,6 @@ Proof.
eauto.
Qed.
-(*
-Remark code_size_pos:
- forall fn, code_size fn >= 0.
-Proof.
- induction fn; simpl; omega.
-Qed.
-*)
-
Remark code_tail_bounds:
forall fn ofs i c,
code_tail ofs fn (i :: c) -> 0 <= ofs < list_length_z fn.
diff --git a/powerpc/Asmgenproof1.v b/powerpc/Asmgenproof1.v
index 42355ad..0b7f4d0 100644
--- a/powerpc/Asmgenproof1.v
+++ b/powerpc/Asmgenproof1.v
@@ -559,16 +559,6 @@ Qed.
(** * Correctness of PowerPC constructor functions *)
-(*
-Ltac SIMP :=
- match goal with
- | [ |- nextinstr _ _ = _ ] => rewrite nextinstr_inv; [auto | auto with ppcgen]
- | [ |- Pregmap.get ?x (Pregmap.set ?x _ _) = _ ] => rewrite Pregmap.gss; auto
- | [ |- Pregmap.set ?x _ _ ?x = _ ] => rewrite Pregmap.gss; auto
- | [ |- Pregmap.get _ (Pregmap.set _ _ _) = _ ] => rewrite Pregmap.gso; [auto | auto with ppcgen]
- | [ |- Pregmap.set _ _ _ _ = _ ] => rewrite Pregmap.gso; [auto | auto with ppcgen]
- end.
-*)
Ltac SIMP :=
(rewrite nextinstr_inv || rewrite Pregmap.gss || rewrite Pregmap.gso); auto with ppcgen.