diff options
| -rw-r--r-- | cfrontend/Cexec.v | 14 | ||||
| -rw-r--r-- | cfrontend/Cminorgenproof.v | 99 | ||||
| -rw-r--r-- | cfrontend/Csem.v | 34 | ||||
| -rw-r--r-- | cfrontend/Csharpminor.v | 9 | ||||
| -rw-r--r-- | cfrontend/Cshmgen.v | 27 | ||||
| -rw-r--r-- | cfrontend/Cshmgenproof.v | 12 | ||||
| -rw-r--r-- | common/Determinism.v | 19 | ||||
| -rw-r--r-- | common/Events.v | 21 | ||||
| -rw-r--r-- | common/Memdata.v | 8 | ||||
| -rw-r--r-- | common/Memory.v | 10 | ||||
| -rw-r--r-- | ia32/Asmgenproof1.v | 24 | ||||
| -rw-r--r-- | ia32/Asmgenretaddr.v | 17 | ||||
| -rw-r--r-- | ia32/standard/Stacklayout.v | 10 | ||||
| -rw-r--r-- | lib/Maps.v | 5 | ||||
| -rw-r--r-- | powerpc/Asmgenproof.v | 8 | ||||
| -rw-r--r-- | powerpc/Asmgenproof1.v | 10 |
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 @@ -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. |