diff options
Diffstat (limited to 'common/Values.v')
| -rw-r--r-- | common/Values.v | 298 |
1 files changed, 290 insertions, 8 deletions
diff --git a/common/Values.v b/common/Values.v index 127d1085..6401ba52 100644 --- a/common/Values.v +++ b/common/Values.v @@ -132,6 +132,40 @@ Proof. simpl in *. InvBooleans. destruct H0. split; auto. eapply has_subtype; eauto. Qed. +Definition has_type_dec (v: val) (t: typ) : { has_type v t } + { ~ has_type v t }. +Proof. + unfold has_type; destruct v. +- auto. +- destruct t; auto. +- destruct t; auto. +- destruct t; auto. +- destruct t; auto. +- destruct t. + apply bool_dec. + auto. + apply bool_dec. + auto. + apply bool_dec. + auto. +Defined. + +Definition has_rettype (v: val) (r: rettype) : Prop := + match r, v with + | Tret t, _ => has_type v t + | Tint8signed, Vint n => n = Int.sign_ext 8 n + | Tint8unsigned, Vint n => n = Int.zero_ext 8 n + | Tint16signed, Vint n => n = Int.sign_ext 16 n + | Tint16unsigned, Vint n => n = Int.zero_ext 16 n + | _, Vundef => True + | _, _ => False + end. + +Lemma has_proj_rettype: forall v r, + has_rettype v r -> has_type v (proj_rettype r). +Proof. + destruct r; simpl; intros; auto; destruct v; try contradiction; exact I. +Qed. + (** Truth values. Non-zero integers are treated as [True]. The integer 0 (also used to represent the null pointer) is [False]. Other values are neither true nor false. *) @@ -766,6 +800,17 @@ Definition rolml (v: val) (amount: int) (mask: int64): val := | _ => Vundef end. +Definition zero_ext_l (nbits: Z) (v: val) : val := + match v with + | Vlong n => Vlong(Int64.zero_ext nbits n) + | _ => Vundef + end. + +Definition sign_ext_l (nbits: Z) (v: val) : val := + match v with + | Vlong n => Vlong(Int64.sign_ext nbits n) + | _ => Vundef + end. (** Comparisons *) @@ -899,6 +944,55 @@ Definition offset_ptr (v: val) (delta: ptrofs) : val := | _ => Vundef end. +(** Normalize a value to the given type, turning it into Vundef if it does not + match the type. *) + +Definition normalize (v: val) (ty: typ) : val := + match v, ty with + | Vundef, _ => Vundef + | Vint _, Tint => v + | Vlong _, Tlong => v + | Vfloat _, Tfloat => v + | Vsingle _, Tsingle => v + | Vptr _ _, (Tint | Tany32) => if Archi.ptr64 then Vundef else v + | Vptr _ _, Tlong => if Archi.ptr64 then v else Vundef + | (Vint _ | Vsingle _), Tany32 => v + | _, Tany64 => v + | _, _ => Vundef + end. + +Lemma normalize_type: + forall v ty, has_type (normalize v ty) ty. +Proof. + intros; destruct v; simpl. +- auto. +- destruct ty; exact I. +- destruct ty; exact I. +- destruct ty; exact I. +- destruct ty; exact I. +- unfold has_type; destruct ty, Archi.ptr64; auto. +Qed. + +Lemma normalize_idem: + forall v ty, has_type v ty -> normalize v ty = v. +Proof. + unfold has_type, normalize; intros. destruct v. +- auto. +- destruct ty; intuition auto. +- destruct ty; intuition auto. +- destruct ty; intuition auto. +- destruct ty; intuition auto. +- destruct ty, Archi.ptr64; intuition congruence. +Qed. + +(** Select between two values based on the result of a comparison. *) + +Definition select (cmp: option bool) (v1 v2: val) (ty: typ) := + match cmp with + | Some b => normalize (if b then v1 else v2) ty + | None => Vundef + end. + (** [load_result] reflects the effect of storing a value with a given memory chunk, then reading it back with the same chunk. Depending on the chunk and the type of the value, some normalization occurs. @@ -926,10 +1020,24 @@ Definition load_result (chunk: memory_chunk) (v: val) := | _, _ => Vundef end. +Lemma load_result_rettype: + forall chunk v, has_rettype (load_result chunk v) (rettype_of_chunk chunk). +Proof. + intros. unfold has_rettype; destruct chunk; destruct v; simpl; auto. +- rewrite Int.sign_ext_idem by omega; auto. +- rewrite Int.zero_ext_idem by omega; auto. +- rewrite Int.sign_ext_idem by omega; auto. +- rewrite Int.zero_ext_idem by omega; auto. +- destruct Archi.ptr64 eqn:SF; simpl; auto. +- destruct Archi.ptr64 eqn:SF; simpl; auto. +- destruct Archi.ptr64 eqn:SF; simpl; auto. +Qed. + Lemma load_result_type: forall chunk v, has_type (load_result chunk v) (type_of_chunk chunk). Proof. - intros. unfold has_type; destruct chunk; destruct v; simpl; auto; destruct Archi.ptr64 eqn:SF; simpl; auto. + intros. rewrite <- proj_rettype_of_chunk. apply has_proj_rettype. + apply load_result_rettype. Qed. Lemma load_result_same: @@ -1362,6 +1470,60 @@ Proof. assert (32 < Int.max_unsigned) by reflexivity. omega. Qed. +Theorem shrx1_shr: + forall x z, + shrx x (Vint (Int.repr 1)) = Some z -> + z = shr (add x (shru x (Vint (Int.repr 31)))) (Vint (Int.repr 1)). +Proof. + intros. destruct x; simpl in H; try discriminate. + change (Int.ltu (Int.repr 1) (Int.repr 31)) with true in H; simpl in H. + inversion_clear H. + simpl. + change (Int.ltu (Int.repr 31) Int.iwordsize) with true; simpl. + change (Int.ltu (Int.repr 1) Int.iwordsize) with true; simpl. + f_equal. + rewrite Int.shrx1_shr by reflexivity. + reflexivity. +Qed. + +Theorem shrx_shr_3: + forall n x z, + shrx x (Vint n) = Some z -> + z = (if Int.eq n Int.zero then x else + if Int.eq n Int.one + then shr (add x (shru x (Vint (Int.repr 31)))) (Vint Int.one) + else shr (add x (shru (shr x (Vint (Int.repr 31))) + (Vint (Int.sub (Int.repr 32) n)))) + (Vint n)). +Proof. + intros. destruct x; simpl in H; try discriminate. + destruct (Int.ltu n (Int.repr 31)) eqn:LT; inv H. + exploit Int.ltu_inv; eauto. change (Int.unsigned (Int.repr 31)) with 31; intros LT'. + predSpec Int.eq Int.eq_spec n Int.zero. +- subst n. unfold Int.shrx. rewrite Int.shl_zero. unfold Int.divs. change (Int.signed Int.one) with 1. + rewrite Z.quot_1_r. rewrite Int.repr_signed; auto. +- predSpec Int.eq Int.eq_spec n Int.one. + * subst n. simpl. + change (Int.ltu (Int.repr 31) Int.iwordsize) with true. simpl. + change (Int.ltu Int.one Int.iwordsize) with true. simpl. + f_equal. + apply Int.shrx1_shr. + reflexivity. + * clear H0. + simpl. change (Int.ltu (Int.repr 31) Int.iwordsize) with true. simpl. + replace (Int.ltu (Int.sub (Int.repr 32) n) Int.iwordsize) with true. simpl. + replace (Int.ltu n Int.iwordsize) with true. + f_equal; apply Int.shrx_shr_2; assumption. + symmetry; apply zlt_true. change (Int.unsigned n < 32); omega. + symmetry; apply zlt_true. unfold Int.sub. change (Int.unsigned (Int.repr 32)) with 32. + assert (Int.unsigned n <> 0). + { red; intros; elim H. + rewrite <- (Int.repr_unsigned n), H0. auto. } + rewrite Int.unsigned_repr. + change (Int.unsigned Int.iwordsize) with 32; omega. + assert (32 < Int.max_unsigned) by reflexivity. omega. +Qed. + Theorem or_rolm: forall x n m1 m2, or (rolm x n m1) (rolm x n m2) = rolm x n (Int.or m1 m2). @@ -1621,6 +1783,58 @@ Proof. assert (64 < Int.max_unsigned) by reflexivity. omega. Qed. +Theorem shrxl1_shrl: + forall x z, + shrxl x (Vint (Int.repr 1)) = Some z -> + z = shrl (addl x (shrlu x (Vint (Int.repr 63)))) (Vint (Int.repr 1)). +Proof. + intros. destruct x; simpl in H; try discriminate. + change (Int.ltu (Int.repr 1) (Int.repr 63)) with true in H; simpl in H. + inversion_clear H. + simpl. + change (Int.ltu (Int.repr 63) Int64.iwordsize') with true; simpl. + change (Int.ltu (Int.repr 1) Int64.iwordsize') with true; simpl. + f_equal. + rewrite Int64.shrx'1_shr' by reflexivity. + reflexivity. +Qed. + +Theorem shrxl_shrl_3: + forall n x z, + shrxl x (Vint n) = Some z -> + z = (if Int.eq n Int.zero then x else + if Int.eq n Int.one + then shrl (addl x (shrlu x (Vint (Int.repr 63)))) (Vint Int.one) + else shrl (addl x (shrlu (shrl x (Vint (Int.repr 63))) + (Vint (Int.sub (Int.repr 64) n)))) + (Vint n)). +Proof. + intros. destruct x; simpl in H; try discriminate. + destruct (Int.ltu n (Int.repr 63)) eqn:LT; inv H. + exploit Int.ltu_inv; eauto. change (Int.unsigned (Int.repr 63)) with 63; intros LT'. + predSpec Int.eq Int.eq_spec n Int.zero. +- subst n. unfold Int64.shrx'. rewrite Int64.shl'_zero. unfold Int64.divs. change (Int64.signed Int64.one) with 1. + rewrite Z.quot_1_r. rewrite Int64.repr_signed; auto. +- predSpec Int.eq Int.eq_spec n Int.one. + * subst n. simpl. + change (Int.ltu (Int.repr 63) Int64.iwordsize') with true. simpl. + change (Int.ltu Int.one Int64.iwordsize') with true. simpl. + f_equal. + apply Int64.shrx'1_shr'. + reflexivity. + * clear H0. +simpl. change (Int.ltu (Int.repr 63) Int64.iwordsize') with true. simpl. + replace (Int.ltu (Int.sub (Int.repr 64) n) Int64.iwordsize') with true. simpl. + replace (Int.ltu n Int64.iwordsize') with true. + f_equal; apply Int64.shrx'_shr_2; assumption. + symmetry; apply zlt_true. change (Int.unsigned n < 64); omega. + symmetry; apply zlt_true. unfold Int.sub. change (Int.unsigned (Int.repr 64)) with 64. + assert (Int.unsigned n <> 0). { red; intros; elim H. rewrite <- (Int.repr_unsigned n), H0. auto. } + rewrite Int.unsigned_repr. + change (Int.unsigned Int64.iwordsize') with 64; omega. + assert (64 < Int.max_unsigned) by reflexivity. omega. +Qed. + Theorem negate_cmp_bool: forall c x y, cmp_bool (negate_comparison c) x y = option_map negb (cmp_bool c x y). Proof. @@ -1833,10 +2047,18 @@ Qed. Lemma zero_ext_and: forall n v, - 0 < n < Int.zwordsize -> + 0 <= n -> Val.zero_ext n v = Val.and v (Vint (Int.repr (two_p n - 1))). Proof. - intros. destruct v; simpl; auto. decEq. apply Int.zero_ext_and; auto. omega. + intros. destruct v; simpl; auto. decEq. apply Int.zero_ext_and; auto. +Qed. + +Lemma zero_ext_andl: + forall n v, + 0 <= n -> + Val.zero_ext_l n v = Val.andl v (Vlong (Int64.repr (two_p n - 1))). +Proof. + intros. destruct v; simpl; auto. decEq. apply Int64.zero_ext_and; auto. Qed. Lemma rolm_lt_zero: @@ -1884,7 +2106,7 @@ Inductive lessdef_list: list val -> list val -> Prop := lessdef v1 v2 -> lessdef_list vl1 vl2 -> lessdef_list (v1 :: vl1) (v2 :: vl2). -Hint Resolve lessdef_refl lessdef_undef lessdef_list_nil lessdef_list_cons. +Hint Resolve lessdef_refl lessdef_undef lessdef_list_nil lessdef_list_cons : core. Lemma lessdef_list_inv: forall vl1 vl2, lessdef_list vl1 vl2 -> vl1 = vl2 \/ In Vundef vl1. @@ -2045,6 +2267,36 @@ Proof. intros. destruct v; simpl; auto. f_equal. apply Ptrofs.add_assoc. Qed. +Lemma lessdef_normalize: + forall v ty, lessdef (normalize v ty) v. +Proof. + intros. destruct v; simpl. + - auto. + - destruct ty; auto. + - destruct ty; auto. + - destruct ty; auto. + - destruct ty; auto. + - destruct ty, Archi.ptr64; auto. +Qed. + +Lemma normalize_lessdef: + forall v v' ty, lessdef v v' -> lessdef (normalize v ty) (normalize v' ty). +Proof. + intros. inv H; auto. +Qed. + +Lemma select_lessdef: + forall ob ob' v1 v1' v2 v2' ty, + ob = None \/ ob = ob' -> + lessdef v1 v1' -> lessdef v2 v2' -> + lessdef (select ob v1 v2 ty) (select ob' v1' v2' ty). +Proof. + intros; unfold select. destruct H. +- subst ob; auto. +- subst ob'; destruct ob as [b|]; auto. + apply normalize_lessdef. destruct b; auto. +Qed. + (** * Values and memory injections *) (** A memory injection [f] is a function from addresses to either [None] @@ -2079,7 +2331,7 @@ Inductive inject (mi: meminj): val -> val -> Prop := | val_inject_undef: forall v, inject mi Vundef v. -Hint Constructors inject. +Hint Constructors inject : core. Inductive inject_list (mi: meminj): list val -> list val-> Prop:= | inject_list_nil : @@ -2088,7 +2340,7 @@ Inductive inject_list (mi: meminj): list val -> list val-> Prop:= inject mi v v' -> inject_list mi vl vl'-> inject_list mi (v :: vl) (v' :: vl'). -Hint Resolve inject_list_nil inject_list_cons. +Hint Resolve inject_list_nil inject_list_cons : core. Lemma inject_ptrofs: forall mi i, inject mi (Vptrofs i) (Vptrofs i). @@ -2096,7 +2348,7 @@ Proof. unfold Vptrofs; intros. destruct Archi.ptr64; auto. Qed. -Hint Resolve inject_ptrofs. +Hint Resolve inject_ptrofs : core. Section VAL_INJ_OPS. @@ -2329,6 +2581,36 @@ Proof. intros. unfold Val.hiword; inv H; auto. Qed. +Lemma normalize_inject: + forall v v' ty, inject f v v' -> inject f (normalize v ty) (normalize v' ty). +Proof. + intros. inv H. +- destruct ty; constructor. +- destruct ty; constructor. +- destruct ty; constructor. +- destruct ty; constructor. +- simpl. destruct ty. ++ destruct Archi.ptr64; econstructor; eauto. ++ auto. ++ destruct Archi.ptr64; econstructor; eauto. ++ auto. ++ destruct Archi.ptr64; econstructor; eauto. ++ econstructor; eauto. +- constructor. +Qed. + +Lemma select_inject: + forall ob ob' v1 v1' v2 v2' ty, + ob = None \/ ob = ob' -> + inject f v1 v1' -> inject f v2 v2' -> + inject f (select ob v1 v2 ty) (select ob' v1' v2' ty). +Proof. + intros; unfold select. destruct H. +- subst ob; auto. +- subst ob'; destruct ob as [b|]; auto. + apply normalize_inject. destruct b; auto. +Qed. + End VAL_INJ_OPS. End Val. @@ -2369,7 +2651,7 @@ Proof. constructor. eapply val_inject_incr; eauto. auto. Qed. -Hint Resolve inject_incr_refl val_inject_incr val_inject_list_incr. +Hint Resolve inject_incr_refl val_inject_incr val_inject_list_incr : core. Lemma val_inject_lessdef: forall v1 v2, Val.lessdef v1 v2 <-> Val.inject (fun b => Some(b, 0)) v1 v2. |