diff options
Diffstat (limited to 'cfrontend/Cop.v')
-rw-r--r-- | cfrontend/Cop.v | 52 |
1 files changed, 26 insertions, 26 deletions
diff --git a/cfrontend/Cop.v b/cfrontend/Cop.v index 2a5d17bc..6284660c 100644 --- a/cfrontend/Cop.v +++ b/cfrontend/Cop.v @@ -1054,13 +1054,13 @@ Hypothesis valid_different_pointers_inj: b1' <> b2' \/ Int.unsigned (Int.add ofs1 (Int.repr delta1)) <> Int.unsigned (Int.add ofs2 (Int.repr delta2)). -Remark val_inject_vtrue: forall f, val_inject f Vtrue Vtrue. +Remark val_inject_vtrue: forall f, Val.inject f Vtrue Vtrue. Proof. unfold Vtrue; auto. Qed. -Remark val_inject_vfalse: forall f, val_inject f Vfalse Vfalse. +Remark val_inject_vfalse: forall f, Val.inject f Vfalse Vfalse. Proof. unfold Vfalse; auto. Qed. -Remark val_inject_of_bool: forall f b, val_inject f (Val.of_bool b) (Val.of_bool b). +Remark val_inject_of_bool: forall f b, Val.inject f (Val.of_bool b) (Val.of_bool b). Proof. intros. unfold Val.of_bool. destruct b; [apply val_inject_vtrue|apply val_inject_vfalse]. Qed. @@ -1075,8 +1075,8 @@ Ltac TrivialInject := Lemma sem_cast_inject: forall v1 ty1 ty v tv1, sem_cast v1 ty1 ty = Some v -> - val_inject f v1 tv1 -> - exists tv, sem_cast tv1 ty1 ty = Some tv /\ val_inject f v tv. + Val.inject f v1 tv1 -> + exists tv, sem_cast tv1 ty1 ty = Some tv /\ Val.inject f v tv. Proof. unfold sem_cast; intros; destruct (classify_cast ty1 ty); inv H0; inv H; TrivialInject. @@ -1093,8 +1093,8 @@ Qed. Lemma sem_unary_operation_inj: forall op v1 ty v tv1, sem_unary_operation op v1 ty m = Some v -> - val_inject f v1 tv1 -> - exists tv, sem_unary_operation op tv1 ty m' = Some tv /\ val_inject f v tv. + Val.inject f v1 tv1 -> + exists tv, sem_unary_operation op tv1 ty m' = Some tv /\ Val.inject f v tv. Proof. unfold sem_unary_operation; intros. destruct op. (* notbool *) @@ -1118,15 +1118,15 @@ Definition optval_self_injects (ov: option val) : Prop := Remark sem_binarith_inject: forall sem_int sem_long sem_float sem_single v1 t1 v2 t2 v v1' v2', sem_binarith sem_int sem_long sem_float sem_single v1 t1 v2 t2 = Some v -> - val_inject f v1 v1' -> val_inject f v2 v2' -> + Val.inject f v1 v1' -> Val.inject f v2 v2' -> (forall sg n1 n2, optval_self_injects (sem_int sg n1 n2)) -> (forall sg n1 n2, optval_self_injects (sem_long sg n1 n2)) -> (forall n1 n2, optval_self_injects (sem_float n1 n2)) -> (forall n1 n2, optval_self_injects (sem_single n1 n2)) -> - exists v', sem_binarith sem_int sem_long sem_float sem_single v1' t1 v2' t2 = Some v' /\ val_inject f v v'. + exists v', sem_binarith sem_int sem_long sem_float sem_single v1' t1 v2' t2 = Some v' /\ Val.inject f v v'. Proof. intros. - assert (SELF: forall ov v, ov = Some v -> optval_self_injects ov -> val_inject f v v). + assert (SELF: forall ov v, ov = Some v -> optval_self_injects ov -> Val.inject f v v). { intros. subst ov; simpl in H7. destruct v0; contradiction || constructor. } @@ -1144,8 +1144,8 @@ Qed. Remark sem_shift_inject: forall sem_int sem_long v1 t1 v2 t2 v v1' v2', sem_shift sem_int sem_long v1 t1 v2 t2 = Some v -> - val_inject f v1 v1' -> val_inject f v2 v2' -> - exists v', sem_shift sem_int sem_long v1' t1 v2' t2 = Some v' /\ val_inject f v v'. + Val.inject f v1 v1' -> Val.inject f v2 v2' -> + exists v', sem_shift sem_int sem_long v1' t1 v2' t2 = Some v' /\ Val.inject f v v'. Proof. intros. exists v. unfold sem_shift in *; destruct (classify_shift t1 t2); inv H0; inv H1; try discriminate. @@ -1158,9 +1158,9 @@ Qed. Remark sem_cmp_inj: forall cmp v1 tv1 ty1 v2 tv2 ty2 v, sem_cmp cmp v1 ty1 v2 ty2 m = Some v -> - val_inject f v1 tv1 -> - val_inject f v2 tv2 -> - exists tv, sem_cmp cmp tv1 ty1 tv2 ty2 m' = Some tv /\ val_inject f v tv. + Val.inject f v1 tv1 -> + Val.inject f v2 tv2 -> + exists tv, sem_cmp cmp tv1 ty1 tv2 ty2 m' = Some tv /\ Val.inject f v tv. Proof. intros. unfold sem_cmp in *; destruct (classify_cmp ty1 ty2). @@ -1168,21 +1168,21 @@ Proof. destruct (Val.cmpu_bool (Mem.valid_pointer m) cmp v1 v2) as [b|] eqn:E; simpl in H; inv H. replace (Val.cmpu_bool (Mem.valid_pointer m') cmp tv1 tv2) with (Some b). simpl. TrivialInject. - symmetry. eapply val_cmpu_bool_inject; eauto. + symmetry. eapply Val.cmpu_bool_inject; eauto. - (* pointer - long *) destruct v2; try discriminate. inv H1. set (v2 := Vint (Int.repr (Int64.unsigned i))) in *. destruct (Val.cmpu_bool (Mem.valid_pointer m) cmp v1 v2) as [b|] eqn:E; simpl in H; inv H. replace (Val.cmpu_bool (Mem.valid_pointer m') cmp tv1 v2) with (Some b). simpl. TrivialInject. - symmetry. eapply val_cmpu_bool_inject with (v2 := v2); eauto. constructor. + symmetry. eapply Val.cmpu_bool_inject with (v2 := v2); eauto. constructor. - (* long - pointer *) destruct v1; try discriminate. inv H0. set (v1 := Vint (Int.repr (Int64.unsigned i))) in *. destruct (Val.cmpu_bool (Mem.valid_pointer m) cmp v1 v2) as [b|] eqn:E; simpl in H; inv H. replace (Val.cmpu_bool (Mem.valid_pointer m') cmp v1 tv2) with (Some b). simpl. TrivialInject. - symmetry. eapply val_cmpu_bool_inject with (v1 := v1); eauto. constructor. + symmetry. eapply Val.cmpu_bool_inject with (v1 := v1); eauto. constructor. - (* numerical - numerical *) assert (SELF: forall b, optval_self_injects (Some (Val.of_bool b))). { @@ -1194,8 +1194,8 @@ Qed. Lemma sem_binary_operation_inj: forall cenv op v1 ty1 v2 ty2 v tv1 tv2, sem_binary_operation cenv op v1 ty1 v2 ty2 m = Some v -> - val_inject f v1 tv1 -> val_inject f v2 tv2 -> - exists tv, sem_binary_operation cenv op tv1 ty1 tv2 ty2 m' = Some tv /\ val_inject f v tv. + Val.inject f v1 tv1 -> Val.inject f v2 tv2 -> + exists tv, sem_binary_operation cenv op tv1 ty1 tv2 ty2 m' = Some tv /\ Val.inject f v tv. Proof. unfold sem_binary_operation; intros; destruct op. - (* add *) @@ -1269,7 +1269,7 @@ Qed. Lemma bool_val_inj: forall v ty b tv, bool_val v ty m = Some b -> - val_inject f v tv -> + Val.inject f v tv -> bool_val tv ty m' = Some b. Proof. unfold bool_val; intros. @@ -1283,9 +1283,9 @@ End GENERIC_INJECTION. Lemma sem_unary_operation_inject: forall f m m' op v1 ty1 v tv1, sem_unary_operation op v1 ty1 m = Some v -> - val_inject f v1 tv1 -> + Val.inject f v1 tv1 -> Mem.inject f m m' -> - exists tv, sem_unary_operation op tv1 ty1 m' = Some tv /\ val_inject f v tv. + exists tv, sem_unary_operation op tv1 ty1 m' = Some tv /\ Val.inject f v tv. Proof. intros. eapply sem_unary_operation_inj; eauto. intros; eapply Mem.weak_valid_pointer_inject_val; eauto. @@ -1294,9 +1294,9 @@ Qed. Lemma sem_binary_operation_inject: forall f m m' cenv op v1 ty1 v2 ty2 v tv1 tv2, sem_binary_operation cenv op v1 ty1 v2 ty2 m = Some v -> - val_inject f v1 tv1 -> val_inject f v2 tv2 -> + Val.inject f v1 tv1 -> Val.inject f v2 tv2 -> Mem.inject f m m' -> - exists tv, sem_binary_operation cenv op tv1 ty1 tv2 ty2 m' = Some tv /\ val_inject f v tv. + exists tv, sem_binary_operation cenv op tv1 ty1 tv2 ty2 m' = Some tv /\ Val.inject f v tv. Proof. intros. eapply sem_binary_operation_inj; eauto. intros; eapply Mem.valid_pointer_inject_val; eauto. @@ -1308,7 +1308,7 @@ Qed. Lemma bool_val_inject: forall f m m' v ty b tv, bool_val v ty m = Some b -> - val_inject f v tv -> + Val.inject f v tv -> Mem.inject f m m' -> bool_val tv ty m' = Some b. Proof. |