From 4d542bc7eafadb16b845cf05d1eb4988eb55ed0f Mon Sep 17 00:00:00 2001 From: Bernhard Schommer Date: Tue, 20 Oct 2015 13:32:18 +0200 Subject: Updated PR by removing whitespaces. Bug 17450. --- cfrontend/Cop.v | 108 ++++++++++++++++++++++++++++---------------------------- 1 file changed, 54 insertions(+), 54 deletions(-) (limited to 'cfrontend/Cop.v') diff --git a/cfrontend/Cop.v b/cfrontend/Cop.v index 948ccaca..b4784028 100644 --- a/cfrontend/Cop.v +++ b/cfrontend/Cop.v @@ -65,7 +65,7 @@ Inductive incr_or_decr : Type := Incr | Decr. The [sem_*] functions below compute the result of an operator application. Since operators are overloaded, the result depends both on the static types of the arguments and on their run-time values. - The corresponding [classify_*] function is first called on the + The corresponding [classify_*] function is first called on the types of the arguments to resolve static overloading. It is then followed by a case analysis on the values of the arguments. *) @@ -139,7 +139,7 @@ Definition cast_int_int (sz: intsize) (sg: signedness) (i: int) : int := | I8, Signed => Int.sign_ext 8 i | I8, Unsigned => Int.zero_ext 8 i | I16, Signed => Int.sign_ext 16 i - | I16, Unsigned => Int.zero_ext 16 i + | I16, Unsigned => Int.zero_ext 16 i | I32, _ => i | IBool, _ => if Int.eq i Int.zero then Int.zero else Int.one end. @@ -343,8 +343,8 @@ Definition sem_cast (v: val) (t1 t2: type) : option val := end. (** The following describes types that can be interpreted as a boolean: - integers, floats, pointers. It is used for the semantics of - the [!] and [?] operators, as well as the [if], [while], + integers, floats, pointers. It is used for the semantics of + the [!] and [?] operators, as well as the [if], [while], and [for] statements. *) Inductive classify_bool_cases : Type := @@ -638,33 +638,33 @@ Definition classify_add (ty1: type) (ty2: type) := end. Definition sem_add (cenv: composite_env) (v1:val) (t1:type) (v2: val) (t2:type) : option val := - match classify_add t1 t2 with + match classify_add t1 t2 with | add_case_pi ty => (**r pointer plus integer *) match v1,v2 with - | Vptr b1 ofs1, Vint n2 => + | Vptr b1 ofs1, Vint n2 => Some (Vptr b1 (Int.add ofs1 (Int.mul (Int.repr (sizeof cenv ty)) n2))) | _, _ => None - end + end | add_case_ip ty => (**r integer plus pointer *) match v1,v2 with - | Vint n1, Vptr b2 ofs2 => + | Vint n1, Vptr b2 ofs2 => Some (Vptr b2 (Int.add ofs2 (Int.mul (Int.repr (sizeof cenv ty)) n1))) | _, _ => None - end + end | add_case_pl ty => (**r pointer plus long *) match v1,v2 with - | Vptr b1 ofs1, Vlong n2 => + | Vptr b1 ofs1, Vlong n2 => let n2 := Int.repr (Int64.unsigned n2) in Some (Vptr b1 (Int.add ofs1 (Int.mul (Int.repr (sizeof cenv ty)) n2))) | _, _ => None - end + end | add_case_lp ty => (**r long plus pointer *) match v1,v2 with - | Vlong n1, Vptr b2 ofs2 => + | Vlong n1, Vptr b2 ofs2 => let n1 := Int.repr (Int64.unsigned n1) in Some (Vptr b2 (Int.add ofs2 (Int.mul (Int.repr (sizeof cenv ty)) n1))) | _, _ => None - end + end | add_default => sem_binarith (fun sg n1 n2 => Some(Vint(Int.add n1 n2))) @@ -694,13 +694,13 @@ Definition sem_sub (cenv: composite_env) (v1:val) (t1:type) (v2: val) (t2:type) match classify_sub t1 t2 with | sub_case_pi ty => (**r pointer minus integer *) match v1,v2 with - | Vptr b1 ofs1, Vint n2 => + | Vptr b1 ofs1, Vint n2 => Some (Vptr b1 (Int.sub ofs1 (Int.mul (Int.repr (sizeof cenv ty)) n2))) | _, _ => None end | sub_case_pl ty => (**r pointer minus long *) match v1,v2 with - | Vptr b1 ofs1, Vlong n2 => + | Vptr b1 ofs1, Vlong n2 => let n2 := Int.repr (Int64.unsigned n2) in Some (Vptr b1 (Int.sub ofs1 (Int.mul (Int.repr (sizeof cenv ty)) n2))) | _, _ => None @@ -724,7 +724,7 @@ Definition sem_sub (cenv: composite_env) (v1:val) (t1:type) (v2: val) (t2:type) (fun n1 n2 => Some(Vsingle(Float32.sub n1 n2))) v1 t1 v2 t2 end. - + (** *** Multiplication, division, modulus *) Definition sem_mul (v1:val) (t1:type) (v2: val) (t2:type) : option val := @@ -842,28 +842,28 @@ Definition sem_shift match classify_shift t1 t2 with | shift_case_ii sg => match v1, v2 with - | Vint n1, Vint n2 => + | Vint n1, Vint n2 => if Int.ltu n2 Int.iwordsize then Some(Vint(sem_int sg n1 n2)) else None | _, _ => None end | shift_case_il sg => match v1, v2 with - | Vint n1, Vlong n2 => + | Vint n1, Vlong n2 => if Int64.ltu n2 (Int64.repr 32) then Some(Vint(sem_int sg n1 (Int64.loword n2))) else None | _, _ => None end | shift_case_li sg => match v1, v2 with - | Vlong n1, Vint n2 => + | Vlong n1, Vint n2 => if Int.ltu n2 Int64.iwordsize' then Some(Vlong(sem_long sg n1 (Int64.repr (Int.unsigned n2)))) else None | _, _ => None end | shift_case_ll sg => match v1, v2 with - | Vlong n1, Vlong n2 => + | Vlong n1, Vlong n2 => if Int64.ltu n2 Int64.iwordsize then Some(Vlong(sem_long sg n1 n2)) else None | _, _ => None @@ -892,7 +892,7 @@ Inductive classify_cmp_cases : Type := | cmp_default. (**r numerical, numerical *) Definition classify_cmp (ty1: type) (ty2: type) := - match typeconv ty1, typeconv ty2 with + match typeconv ty1, typeconv ty2 with | Tpointer _ _ , Tpointer _ _ => cmp_case_pp | Tpointer _ _ , Tint _ _ _ => cmp_case_pp | Tint _ _ _, Tpointer _ _ => cmp_case_pp @@ -909,14 +909,14 @@ Definition sem_cmp (c:comparison) option_map Val.of_bool (Val.cmpu_bool (Mem.valid_pointer m) c v1 v2) | cmp_case_pl => match v2 with - | Vlong n2 => + | Vlong n2 => let n2 := Int.repr (Int64.unsigned n2) in option_map Val.of_bool (Val.cmpu_bool (Mem.valid_pointer m) c v1 (Vint n2)) | _ => None end | cmp_case_lp => match v1 with - | Vlong n1 => + | Vlong n1 => let n1 := Int.repr (Int64.unsigned n1) in option_map Val.of_bool (Val.cmpu_bool (Mem.valid_pointer m) c (Vint n1) v2) | _ => None @@ -941,7 +941,7 @@ Inductive classify_fun_cases : Type := | fun_default. Definition classify_fun (ty: type) := - match ty with + match ty with | Tfunction args res cc => fun_case_f args res cc | Tpointer (Tfunction args res cc) _ => fun_case_f args res cc | _ => fun_default @@ -989,15 +989,15 @@ Definition sem_binary_operation (m: mem): option val := match op with | Oadd => sem_add cenv v1 t1 v2 t2 - | Osub => sem_sub cenv v1 t1 v2 t2 + | Osub => sem_sub cenv v1 t1 v2 t2 | Omul => sem_mul v1 t1 v2 t2 | Omod => sem_mod v1 t1 v2 t2 - | Odiv => sem_div v1 t1 v2 t2 + | Odiv => sem_div v1 t1 v2 t2 | Oand => sem_and v1 t1 v2 t2 | Oor => sem_or v1 t1 v2 t2 | Oxor => sem_xor v1 t1 v2 t2 | Oshl => sem_shl v1 t1 v2 t2 - | Oshr => sem_shr v1 t1 v2 t2 + | Oshr => sem_shr v1 t1 v2 t2 | Oeq => sem_cmp Ceq v1 t1 v2 t2 m | One => sem_cmp Cne v1 t1 v2 t2 m | Olt => sem_cmp Clt v1 t1 v2 t2 m @@ -1063,7 +1063,7 @@ 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). -Proof. intros. unfold Val.of_bool. destruct b; [apply val_inject_vtrue|apply val_inject_vfalse]. +Proof. intros. unfold Val.of_bool. destruct b; [apply val_inject_vtrue|apply val_inject_vfalse]. Qed. Hint Resolve val_inject_vtrue val_inject_vfalse val_inject_of_bool. @@ -1082,7 +1082,7 @@ Lemma sem_cast_inject: Proof. unfold sem_cast; intros; destruct (classify_cast ty1 ty); inv H0; inv H; TrivialInject. -- econstructor; eauto. +- econstructor; eauto. - destruct (cast_float_int si2 f0); inv H1; TrivialInject. - destruct (cast_single_int si2 f0); inv H1; TrivialInject. - destruct (cast_float_long si2 f0); inv H1; TrivialInject. @@ -1102,7 +1102,7 @@ Proof. (* notbool *) unfold sem_notbool in *; destruct (classify_bool ty); inv H0; inv H; TrivialInject. destruct (Mem.weak_valid_pointer m b1 (Int.unsigned ofs1)) eqn:VP; inv H2. - erewrite weak_valid_pointer_inj by eauto. TrivialInject. + erewrite weak_valid_pointer_inj by eauto. TrivialInject. (* notint *) unfold sem_notint in *; destruct (classify_notint ty); inv H0; inv H; TrivialInject. (* neg *) @@ -1127,7 +1127,7 @@ Remark sem_binarith_inject: (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'. Proof. - intros. + intros. 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. @@ -1169,22 +1169,22 @@ Proof. - (* pointer - pointer *) 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. + simpl. TrivialInject. + symmetry. eapply Val.cmpu_bool_inject; eauto. - (* pointer - long *) - destruct v2; try discriminate. inv H1. + 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. + simpl. TrivialInject. + symmetry. eapply Val.cmpu_bool_inject with (v2 := v2); eauto. constructor. - (* long - pointer *) - destruct v1; try discriminate. inv H0. + 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. + simpl. TrivialInject. + 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))). { @@ -1202,13 +1202,13 @@ Proof. unfold sem_binary_operation; intros; destruct op. - (* add *) unfold sem_add in *; destruct (classify_add ty1 ty2). - + inv H0; inv H1; inv H. TrivialInject. + + inv H0; inv H1; inv H. TrivialInject. econstructor. eauto. repeat rewrite Int.add_assoc. decEq. apply Int.add_commut. - + inv H0; inv H1; inv H. TrivialInject. + + inv H0; inv H1; inv H. TrivialInject. econstructor. eauto. repeat rewrite Int.add_assoc. decEq. apply Int.add_commut. - + inv H0; inv H1; inv H. TrivialInject. + + inv H0; inv H1; inv H. TrivialInject. econstructor. eauto. repeat rewrite Int.add_assoc. decEq. apply Int.add_commut. - + inv H0; inv H1; inv H. TrivialInject. + + inv H0; inv H1; inv H. TrivialInject. econstructor. eauto. repeat rewrite Int.add_assoc. decEq. apply Int.add_commut. + eapply sem_binarith_inject; eauto; intros; exact I. - (* sub *) @@ -1216,8 +1216,8 @@ Proof. + inv H0; inv H1; inv H. TrivialInject. econstructor. eauto. rewrite Int.sub_add_l. auto. + inv H0; inv H1; inv H. TrivialInject. - destruct (eq_block b1 b0); try discriminate. subst b1. - rewrite H0 in H2; inv H2. rewrite dec_eq_true. + destruct (eq_block b1 b0); try discriminate. subst b1. + rewrite H0 in H2; inv H2. rewrite dec_eq_true. destruct (zlt 0 (sizeof cenv ty) && zle (sizeof cenv ty) Int.max_signed); inv H3. rewrite Int.sub_shifted. TrivialInject. + inv H0; inv H1; inv H. TrivialInject. @@ -1274,7 +1274,7 @@ Lemma bool_val_inj: Val.inject f v tv -> bool_val tv ty m' = Some b. Proof. - unfold bool_val; intros. + unfold bool_val; intros. destruct (classify_bool ty); inv H0; try congruence. destruct (Mem.weak_valid_pointer m b1 (Int.unsigned ofs1)) eqn:VP; inv H. erewrite weak_valid_pointer_inj by eauto. auto. @@ -1289,7 +1289,7 @@ Lemma sem_unary_operation_inject: Mem.inject f m m' -> 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 sem_unary_operation_inj; eauto. intros; eapply Mem.weak_valid_pointer_inject_val; eauto. Qed. @@ -1300,7 +1300,7 @@ Lemma sem_binary_operation_inject: Mem.inject f m m' -> 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 sem_binary_operation_inj; eauto. intros; eapply Mem.valid_pointer_inject_val; eauto. intros; eapply Mem.weak_valid_pointer_inject_val; eauto. intros; eapply Mem.weak_valid_pointer_inject_no_overflow; eauto. @@ -1359,9 +1359,9 @@ Proof. destruct f; auto. destruct (Float32.cmp Ceq f0 Float32.zero); auto. destruct f; auto. - destruct (Int.eq i Int.zero); auto. - destruct (Int.eq i Int.zero); auto. - destruct (Int.eq i Int.zero); auto. + destruct (Int.eq i Int.zero); auto. + destruct (Int.eq i Int.zero); auto. + destruct (Int.eq i Int.zero); auto. Qed. (** Relation between Boolean value and Boolean negation. *) @@ -1371,9 +1371,9 @@ Lemma notbool_bool_val: sem_notbool v t m = match bool_val v t m with None => None | Some b => Some(Val.of_bool (negb b)) end. Proof. - intros. unfold sem_notbool, bool_val. + intros. unfold sem_notbool, bool_val. destruct (classify_bool t); auto; destruct v; auto; rewrite ? negb_involutive; auto. - destruct (Mem.weak_valid_pointer m b (Int.unsigned i)); auto. + destruct (Mem.weak_valid_pointer m b (Int.unsigned i)); auto. Qed. (** Relation with the arithmetic conversions of ISO C99, section 6.3.1 *) @@ -1558,4 +1558,4 @@ End ArithConv. - + -- cgit