diff options
Diffstat (limited to 'common')
| -rw-r--r-- | common/Memdata.v | 16 | ||||
| -rw-r--r-- | common/Memory.v | 9 | ||||
| -rw-r--r-- | common/Memtype.v | 3 | ||||
| -rw-r--r-- | common/Values.v | 505 |
4 files changed, 296 insertions, 237 deletions
diff --git a/common/Memdata.v b/common/Memdata.v index fde8b47..47ed79e 100644 --- a/common/Memdata.v +++ b/common/Memdata.v @@ -1029,22 +1029,6 @@ Proof. apply repeat_Undef_inject_any. apply encode_val_length. Qed. -(** The identity injection has interesting properties. *) - -Definition inject_id : meminj := fun b => Some(b, 0). - -Lemma val_inject_id: - forall v1 v2, - val_inject inject_id v1 v2 <-> Val.lessdef v1 v2. -Proof. - intros; split; intros. - inv H. constructor. constructor. - unfold inject_id in H0. inv H0. rewrite Int.add_zero. constructor. - constructor. - inv H. destruct v2; econstructor. unfold inject_id; reflexivity. rewrite Int.add_zero; auto. - constructor. -Qed. - Definition memval_lessdef: memval -> memval -> Prop := memval_inject inject_id. Lemma memval_lessdef_refl: diff --git a/common/Memory.v b/common/Memory.v index 157867e..e1c68bd 100644 --- a/common/Memory.v +++ b/common/Memory.v @@ -3105,6 +3105,15 @@ Proof. eapply mi_access; eauto. auto. Qed. +Theorem valid_pointer_extends: + forall m1 m2 b ofs, + extends m1 m2 -> valid_pointer m1 b ofs = true -> valid_pointer m2 b ofs = true. +Proof. + intros. + rewrite valid_pointer_valid_access in *. + eapply valid_access_extends; eauto. +Qed. + (* Theorem bounds_extends: forall m1 m2 b, diff --git a/common/Memtype.v b/common/Memtype.v index 40e03a3..f763581 100644 --- a/common/Memtype.v +++ b/common/Memtype.v @@ -917,6 +917,9 @@ Axiom perm_extends: Axiom valid_access_extends: forall m1 m2 chunk b ofs p, extends m1 m2 -> valid_access m1 chunk b ofs p -> valid_access m2 chunk b ofs p. +Axiom valid_pointer_extends: + forall m1 m2 b ofs, + extends m1 m2 -> valid_pointer m1 b ofs = true -> valid_pointer m2 b ofs = true. (** * Memory injections *) diff --git a/common/Values.v b/common/Values.v index 4dc74b2..7fae3b7 100644 --- a/common/Values.v +++ b/common/Values.v @@ -54,8 +54,6 @@ Definition Vfalse: val := Vint Int.zero. Module Val. -Definition of_bool (b: bool): val := if b then Vtrue else Vfalse. - Definition has_type (v: val) (t: typ) : Prop := match v, t with | Vundef, _ => True @@ -115,28 +113,31 @@ Definition absf (v: val) : val := | _ => Vundef end. -Definition intoffloat (v: val) : val := +Definition maketotal (ov: option val) : val := + match ov with Some v => v | None => Vundef end. + +Definition intoffloat (v: val) : option val := match v with - | Vfloat f => match Float.intoffloat f with Some n => Vint n | None => Vundef end - | _ => Vundef + | Vfloat f => option_map Vint (Float.intoffloat f) + | _ => None end. -Definition intuoffloat (v: val) : val := +Definition intuoffloat (v: val) : option val := match v with - | Vfloat f => match Float.intuoffloat f with Some n => Vint n | None => Vundef end - | _ => Vundef + | Vfloat f => option_map Vint (Float.intuoffloat f) + | _ => None end. -Definition floatofint (v: val) : val := +Definition floatofint (v: val) : option val := match v with - | Vint n => Vfloat (Float.floatofint n) - | _ => Vundef + | Vint n => Some (Vfloat (Float.floatofint n)) + | _ => None end. -Definition floatofintu (v: val) : val := +Definition floatofintu (v: val) : option val := match v with - | Vint n => Vfloat (Float.floatofintu n) - | _ => Vundef + | Vint n => Some (Vfloat (Float.floatofintu n)) + | _ => None end. Definition floatofwords (v1 v2: val) : val := @@ -145,12 +146,20 @@ Definition floatofwords (v1 v2: val) : val := | _, _ => Vundef end. +Definition negint (v: val) : val := + match v with + | Vint n => Vint (Int.neg n) + | _ => Vundef + end. + Definition notint (v: val) : val := match v with - | Vint n => Vint (Int.xor n Int.mone) + | Vint n => Vint (Int.not n) | _ => Vundef end. +Definition of_bool (b: bool): val := if b then Vtrue else Vfalse. + Definition notbool (v: val) : val := match v with | Vint n => of_bool (Int.eq n Int.zero) @@ -199,32 +208,32 @@ Definition mul (v1 v2: val): val := | _, _ => Vundef end. -Definition divs (v1 v2: val): val := +Definition divs (v1 v2: val): option val := match v1, v2 with | Vint n1, Vint n2 => - if Int.eq n2 Int.zero then Vundef else Vint(Int.divs n1 n2) - | _, _ => Vundef + if Int.eq n2 Int.zero then None else Some(Vint(Int.divs n1 n2)) + | _, _ => None end. -Definition mods (v1 v2: val): val := +Definition mods (v1 v2: val): option val := match v1, v2 with | Vint n1, Vint n2 => - if Int.eq n2 Int.zero then Vundef else Vint(Int.mods n1 n2) - | _, _ => Vundef + if Int.eq n2 Int.zero then None else Some(Vint(Int.mods n1 n2)) + | _, _ => None end. -Definition divu (v1 v2: val): val := +Definition divu (v1 v2: val): option val := match v1, v2 with | Vint n1, Vint n2 => - if Int.eq n2 Int.zero then Vundef else Vint(Int.divu n1 n2) - | _, _ => Vundef + if Int.eq n2 Int.zero then None else Some(Vint(Int.divu n1 n2)) + | _, _ => None end. -Definition modu (v1 v2: val): val := +Definition modu (v1 v2: val): option val := match v1, v2 with | Vint n1, Vint n2 => - if Int.eq n2 Int.zero then Vundef else Vint(Int.modu n1 n2) - | _, _ => Vundef + if Int.eq n2 Int.zero then None else Some(Vint(Int.modu n1 n2)) + | _, _ => None end. Definition add_carry (v1 v2 cin: val): val := @@ -278,13 +287,13 @@ Definition shr_carry (v1 v2: val): val := | _, _ => Vundef end. -Definition shrx (v1 v2: val): val := +Definition shrx (v1 v2: val): option val := match v1, v2 with | Vint n1, Vint n2 => - if Int.ltu n2 Int.iwordsize - then Vint(Int.shrx n1 n2) - else Vundef - | _, _ => Vundef + if Int.ltu n2 (Int.repr 31) + then Some(Vint(Int.shrx n1 n2)) + else None + | _, _ => None end. Definition shru (v1 v2: val): val := @@ -335,48 +344,60 @@ Definition divf (v1 v2: val): val := | _, _ => Vundef end. -Definition cmp_mismatch (c: comparison): val := - match c with - | Ceq => Vfalse - | Cne => Vtrue - | _ => Vundef - end. +Section COMPARISONS. -Definition cmp (c: comparison) (v1 v2: val): val := +Variable valid_ptr: block -> Z -> bool. + +Definition cmp_bool (c: comparison) (v1 v2: val): option bool := match v1, v2 with - | Vint n1, Vint n2 => of_bool (Int.cmp c n1 n2) - | Vint n1, Vptr b2 ofs2 => - if Int.eq n1 Int.zero then cmp_mismatch c else Vundef - | Vptr b1 ofs1, Vptr b2 ofs2 => - if zeq b1 b2 - then of_bool (Int.cmp c ofs1 ofs2) - else cmp_mismatch c - | Vptr b1 ofs1, Vint n2 => - if Int.eq n2 Int.zero then cmp_mismatch c else Vundef - | _, _ => Vundef + | Vint n1, Vint n2 => Some (Int.cmp c n1 n2) + | _, _ => None end. -Definition cmpu (c: comparison) (v1 v2: val): val := +Definition cmp_different_blocks (c: comparison): option bool := + match c with + | Ceq => Some false + | Cne => Some true + | _ => None + end. + +Definition cmpu_bool (c: comparison) (v1 v2: val): option bool := match v1, v2 with | Vint n1, Vint n2 => - of_bool (Int.cmpu c n1 n2) + Some (Int.cmpu c n1 n2) | Vint n1, Vptr b2 ofs2 => - if Int.eq n1 Int.zero then cmp_mismatch c else Vundef + if Int.eq n1 Int.zero then cmp_different_blocks c else None | Vptr b1 ofs1, Vptr b2 ofs2 => - if zeq b1 b2 - then of_bool (Int.cmpu c ofs1 ofs2) - else cmp_mismatch c + if valid_ptr b1 (Int.unsigned ofs1) && valid_ptr b2 (Int.unsigned ofs2) then + if zeq b1 b2 + then Some (Int.cmpu c ofs1 ofs2) + else cmp_different_blocks c + else None | Vptr b1 ofs1, Vint n2 => - if Int.eq n2 Int.zero then cmp_mismatch c else Vundef - | _, _ => Vundef + if Int.eq n2 Int.zero then cmp_different_blocks c else None + | _, _ => None end. -Definition cmpf (c: comparison) (v1 v2: val): val := +Definition cmpf_bool (c: comparison) (v1 v2: val): option bool := match v1, v2 with - | Vfloat f1, Vfloat f2 => of_bool (Float.cmp c f1 f2) - | _, _ => Vundef + | Vfloat f1, Vfloat f2 => Some (Float.cmp c f1 f2) + | _, _ => None end. +Definition of_optbool (ob: option bool): val := + match ob with Some true => Vtrue | Some false => Vfalse | None => Vundef end. + +Definition cmp (c: comparison) (v1 v2: val): val := + of_optbool (cmp_bool c v1 v2). + +Definition cmpu (c: comparison) (v1 v2: val): val := + of_optbool (cmpu_bool c v1 v2). + +Definition cmpf (c: comparison) (v1 v2: val): val := + of_optbool (cmpf_bool c v1 v2). + +End COMPARISONS. + (** [load_result] is used in the memory model (library [Mem]) to post-process the results of a memory read. For instance, consider storing the integer value [0xFFF] on 1 byte at a @@ -483,6 +504,12 @@ Proof. destruct b; reflexivity. Qed. +Theorem notbool_negb_3: + forall ob, of_optbool (option_map negb ob) = notbool (of_optbool ob). +Proof. + destruct ob; auto. destruct b; auto. +Qed. + Theorem notbool_idem2: forall b, notbool(notbool(of_bool b)) = of_bool b. Proof. @@ -496,6 +523,12 @@ Proof. case (Int.eq i Int.zero); reflexivity. Qed. +Theorem notbool_idem4: + forall ob, notbool (notbool (of_optbool ob)) = of_optbool ob. +Proof. + destruct ob; auto. destruct b; auto. +Qed. + Theorem add_commut: forall x y, add x y = add y x. Proof. destruct x; destruct y; simpl; auto. @@ -612,59 +645,59 @@ Proof. Qed. Theorem mods_divs: - forall x y, mods x y = sub x (mul (divs x y) y). + forall x y z, + mods x y = Some z -> exists v, divs x y = Some v /\ z = sub x (mul v y). Proof. - destruct x; destruct y; simpl; auto. - case (Int.eq i0 Int.zero); simpl. auto. decEq. apply Int.mods_divs. + intros. destruct x; destruct y; simpl in *; try discriminate. + destruct (Int.eq i0 Int.zero); inv H. + exists (Vint (Int.divs i i0)); split; auto. + simpl. rewrite Int.mods_divs. auto. Qed. Theorem modu_divu: - forall x y, modu x y = sub x (mul (divu x y) y). + forall x y z, + modu x y = Some z -> exists v, divu x y = Some v /\ z = sub x (mul v y). Proof. - destruct x; destruct y; simpl; auto. - generalize (Int.eq_spec i0 Int.zero); - case (Int.eq i0 Int.zero); simpl. auto. - intro. decEq. apply Int.modu_divu. auto. + intros. destruct x; destruct y; simpl in *; try discriminate. + destruct (Int.eq i0 Int.zero) as []_eqn; inv H. + exists (Vint (Int.divu i i0)); split; auto. + simpl. rewrite Int.modu_divu. auto. + generalize (Int.eq_spec i0 Int.zero). rewrite Heqb; auto. Qed. Theorem divs_pow2: - forall x n logn, - Int.is_power2 n = Some logn -> - divs x (Vint n) = shrx x (Vint logn). + forall x n logn y, + Int.is_power2 n = Some logn -> Int.ltu logn (Int.repr 31) = true -> + divs x (Vint n) = Some y -> + shrx x (Vint logn) = Some y. Proof. - intros; destruct x; simpl; auto. - change 32 with (Z_of_nat Int.wordsize). - rewrite (Int.is_power2_range _ _ H). - generalize (Int.eq_spec n Int.zero); - case (Int.eq n Int.zero); intro. - subst n. compute in H. discriminate. - decEq. apply Int.divs_pow2. auto. + intros; destruct x; simpl in H1; inv H1. + destruct (Int.eq n Int.zero); inv H3. + simpl. rewrite H0. decEq. decEq. symmetry. apply Int.divs_pow2. auto. Qed. Theorem divu_pow2: - forall x n logn, + forall x n logn y, Int.is_power2 n = Some logn -> - divu x (Vint n) = shru x (Vint logn). + divu x (Vint n) = Some y -> + shru x (Vint logn) = y. Proof. - intros; destruct x; simpl; auto. - change 32 with (Z_of_nat Int.wordsize). - rewrite (Int.is_power2_range _ _ H). - generalize (Int.eq_spec n Int.zero); - case (Int.eq n Int.zero); intro. - subst n. compute in H. discriminate. - decEq. apply Int.divu_pow2. auto. + intros; destruct x; simpl in H0; inv H0. + destruct (Int.eq n Int.zero); inv H2. + simpl. + rewrite (Int.is_power2_range _ _ H). + decEq. symmetry. apply Int.divu_pow2. auto. Qed. Theorem modu_pow2: - forall x n logn, + forall x n logn y, Int.is_power2 n = Some logn -> - modu x (Vint n) = and x (Vint (Int.sub n Int.one)). + modu x (Vint n) = Some y -> + and x (Vint (Int.sub n Int.one)) = y. Proof. - intros; destruct x; simpl; auto. - generalize (Int.eq_spec n Int.zero); - case (Int.eq n Int.zero); intro. - subst n. compute in H. discriminate. - decEq. eapply Int.modu_and; eauto. + intros; destruct x; simpl in H0; inv H0. + destruct (Int.eq n Int.zero); inv H2. + simpl. decEq. symmetry. eapply Int.modu_and; eauto. Qed. Theorem and_commut: forall x y, and x y = and y x. @@ -700,7 +733,7 @@ Proof. decEq. apply Int.xor_assoc. Qed. -Theorem shl_mul: forall x y, Val.mul x (Val.shl Vone y) = Val.shl x y. +Theorem shl_mul: forall x y, mul x (shl Vone y) = shl x y. Proof. destruct x; destruct y; simpl; auto. case (Int.ltu i0 Int.iwordsize); auto. @@ -726,12 +759,32 @@ Proof. Qed. Theorem shrx_carry: - forall x y, - add (shr x y) (shr_carry x y) = shrx x y. -Proof. - destruct x; destruct y; simpl; auto. - case (Int.ltu i0 Int.iwordsize); auto. - simpl. decEq. apply Int.shrx_carry. + forall x y z, + shrx x y = Some z -> + add (shr x y) (shr_carry x y) = z. +Proof. + intros. destruct x; destruct y; simpl in H; inv H. + destruct (Int.ltu i0 (Int.repr 31)) as []_eqn; inv H1. + exploit Int.ltu_inv; eauto. change (Int.unsigned (Int.repr 31)) with 31. intros. + assert (Int.ltu i0 Int.iwordsize = true). + unfold Int.ltu. apply zlt_true. change (Int.unsigned Int.iwordsize) with 32. omega. + simpl. rewrite H0. simpl. decEq. rewrite Int.shrx_carry; auto. +Qed. + +Theorem shrx_shr: + forall x y z, + shrx x y = Some z -> + exists p, exists q, + x = Vint p /\ y = Vint q /\ + z = shr (if Int.lt p Int.zero then add x (Vint (Int.sub (Int.shl Int.one q) Int.one)) else x) (Vint q). +Proof. + intros. destruct x; destruct y; simpl in H; inv H. + destruct (Int.ltu i0 (Int.repr 31)) as []_eqn; inv H1. + exploit Int.ltu_inv; eauto. change (Int.unsigned (Int.repr 31)) with 31. intros. + assert (Int.ltu i0 Int.iwordsize = true). + unfold Int.ltu. apply zlt_true. change (Int.unsigned Int.iwordsize) with 32. omega. + exists i; exists i0; intuition. + rewrite Int.shrx_shr; auto. destruct (Int.lt i Int.zero); simpl; rewrite H0; auto. Qed. Theorem or_rolm: @@ -765,173 +818,112 @@ Proof. destruct x; destruct y; simpl; auto. decEq. apply Float.addf_commut. Qed. -Lemma negate_cmp_mismatch: - forall c, - cmp_mismatch (negate_comparison c) = notbool(cmp_mismatch c). +Theorem negate_cmp_bool: + forall c x y, cmp_bool (negate_comparison c) x y = option_map negb (cmp_bool c x y). Proof. - destruct c; reflexivity. + destruct x; destruct y; simpl; auto. rewrite Int.negate_cmp. auto. Qed. -Theorem negate_cmp: - forall c x y, - cmp (negate_comparison c) x y = notbool (cmp c x y). +Theorem negate_cmpu_bool: + forall valid_ptr c x y, + cmpu_bool valid_ptr (negate_comparison c) x y = option_map negb (cmpu_bool valid_ptr c x y). Proof. + assert (forall c, + cmp_different_blocks (negate_comparison c) = option_map negb (cmp_different_blocks c)). + destruct c; auto. destruct x; destruct y; simpl; auto. - rewrite Int.negate_cmp. apply notbool_negb_1. - case (Int.eq i Int.zero). apply negate_cmp_mismatch. reflexivity. - case (Int.eq i0 Int.zero). apply negate_cmp_mismatch. reflexivity. - case (zeq b b0); intro. - rewrite Int.negate_cmp. apply notbool_negb_1. - apply negate_cmp_mismatch. + rewrite Int.negate_cmpu. auto. + destruct (Int.eq i Int.zero); auto. + destruct (Int.eq i0 Int.zero); auto. + destruct (valid_ptr b (Int.unsigned i) && valid_ptr b0 (Int.unsigned i0)); auto. + destruct (zeq b b0); auto. rewrite Int.negate_cmpu. auto. Qed. -Theorem negate_cmpu: +Lemma not_of_optbool: + forall ob, of_optbool (option_map negb ob) = notbool (of_optbool ob). +Proof. + destruct ob; auto. destruct b; auto. +Qed. + +Theorem negate_cmp: forall c x y, - cmpu (negate_comparison c) x y = notbool (cmpu c x y). + cmp (negate_comparison c) x y = notbool (cmp c x y). Proof. - destruct x; destruct y; simpl; auto. - rewrite Int.negate_cmpu. apply notbool_negb_1. - case (Int.eq i Int.zero). apply negate_cmp_mismatch. reflexivity. - case (Int.eq i0 Int.zero). apply negate_cmp_mismatch. reflexivity. - case (zeq b b0); intro. - rewrite Int.negate_cmpu. apply notbool_negb_1. - apply negate_cmp_mismatch. + intros. unfold cmp. rewrite negate_cmp_bool. apply not_of_optbool. Qed. -Lemma swap_cmp_mismatch: - forall c, cmp_mismatch (swap_comparison c) = cmp_mismatch c. +Theorem negate_cmpu: + forall valid_ptr c x y, + cmpu valid_ptr (negate_comparison c) x y = notbool (cmpu valid_ptr c x y). Proof. - destruct c; reflexivity. + intros. unfold cmpu. rewrite negate_cmpu_bool. apply not_of_optbool. Qed. - -Theorem swap_cmp: + +Theorem swap_cmp_bool: forall c x y, - cmp (swap_comparison c) x y = cmp c y x. + cmp_bool (swap_comparison c) x y = cmp_bool c y x. Proof. - destruct x; destruct y; simpl; auto. - rewrite Int.swap_cmp. auto. - case (Int.eq i Int.zero). apply swap_cmp_mismatch. auto. - case (Int.eq i0 Int.zero). apply swap_cmp_mismatch. auto. - case (zeq b b0); intro. - subst b0. rewrite zeq_true. rewrite Int.swap_cmp. auto. - rewrite zeq_false. apply swap_cmp_mismatch. auto. + destruct x; destruct y; simpl; auto. rewrite Int.swap_cmp. auto. Qed. -Theorem swap_cmpu: - forall c x y, - cmpu (swap_comparison c) x y = cmpu c y x. +Theorem swap_cmpu_bool: + forall valid_ptr c x y, + cmpu_bool valid_ptr (swap_comparison c) x y = cmpu_bool valid_ptr c y x. Proof. + assert (forall c, cmp_different_blocks (swap_comparison c) = cmp_different_blocks c). + destruct c; auto. destruct x; destruct y; simpl; auto. rewrite Int.swap_cmpu. auto. - case (Int.eq i Int.zero). apply swap_cmp_mismatch. auto. - case (Int.eq i0 Int.zero). apply swap_cmp_mismatch. auto. - case (zeq b b0); intro. - subst b0. rewrite zeq_true. rewrite Int.swap_cmpu. auto. - rewrite zeq_false. apply swap_cmp_mismatch. auto. + case (Int.eq i Int.zero); auto. + case (Int.eq i0 Int.zero); auto. + destruct (valid_ptr b (Int.unsigned i)); destruct (valid_ptr b0 (Int.unsigned i0)); auto. + simpl. destruct (zeq b b0); subst. + rewrite zeq_true. rewrite Int.swap_cmpu. auto. + rewrite zeq_false; auto. Qed. Theorem negate_cmpf_eq: forall v1 v2, notbool (cmpf Cne v1 v2) = cmpf Ceq v1 v2. Proof. - destruct v1; destruct v2; simpl; auto. - rewrite Float.cmp_ne_eq. rewrite notbool_negb_1. - apply notbool_idem2. + destruct v1; destruct v2; auto. unfold cmpf, cmpf_bool. + rewrite Float.cmp_ne_eq. destruct (Float.cmp Ceq f f0); auto. Qed. Theorem negate_cmpf_ne: forall v1 v2, notbool (cmpf Ceq v1 v2) = cmpf Cne v1 v2. Proof. - destruct v1; destruct v2; simpl; auto. - rewrite Float.cmp_ne_eq. rewrite notbool_negb_1. auto. -Qed. - -Lemma or_of_bool: - forall b1 b2, or (of_bool b1) (of_bool b2) = of_bool (b1 || b2). -Proof. - destruct b1; destruct b2; reflexivity. + destruct v1; destruct v2; auto. unfold cmpf, cmpf_bool. + rewrite Float.cmp_ne_eq. destruct (Float.cmp Ceq f f0); auto. Qed. Theorem cmpf_le: forall v1 v2, cmpf Cle v1 v2 = or (cmpf Clt v1 v2) (cmpf Ceq v1 v2). Proof. - destruct v1; destruct v2; simpl; auto. - rewrite or_of_bool. decEq. apply Float.cmp_le_lt_eq. + destruct v1; destruct v2; auto. unfold cmpf, cmpf_bool. + rewrite Float.cmp_le_lt_eq. + destruct (Float.cmp Clt f f0); destruct (Float.cmp Ceq f f0); auto. Qed. Theorem cmpf_ge: forall v1 v2, cmpf Cge v1 v2 = or (cmpf Cgt v1 v2) (cmpf Ceq v1 v2). Proof. - destruct v1; destruct v2; simpl; auto. - rewrite or_of_bool. decEq. apply Float.cmp_ge_gt_eq. -Qed. - -Definition is_bool (v: val) := - v = Vundef \/ v = Vtrue \/ v = Vfalse. - -Lemma of_bool_is_bool: - forall b, is_bool (of_bool b). -Proof. - destruct b; unfold is_bool; simpl; tauto. -Qed. - -Lemma undef_is_bool: is_bool Vundef. -Proof. - unfold is_bool; tauto. + destruct v1; destruct v2; auto. unfold cmpf, cmpf_bool. + rewrite Float.cmp_ge_gt_eq. + destruct (Float.cmp Cgt f f0); destruct (Float.cmp Ceq f f0); auto. Qed. -Lemma cmp_mismatch_is_bool: - forall c, is_bool (cmp_mismatch c). +Lemma zero_ext_and: + forall n v, + 0 < n < Z_of_nat Int.wordsize -> + Val.zero_ext n v = Val.and v (Vint (Int.repr (two_p n - 1))). Proof. - destruct c; simpl; unfold is_bool; tauto. -Qed. - -Lemma cmp_is_bool: - forall c v1 v2, is_bool (cmp c v1 v2). -Proof. - destruct v1; destruct v2; simpl; try apply undef_is_bool. - apply of_bool_is_bool. - case (Int.eq i Int.zero). apply cmp_mismatch_is_bool. apply undef_is_bool. - case (Int.eq i0 Int.zero). apply cmp_mismatch_is_bool. apply undef_is_bool. - case (zeq b b0); intro. apply of_bool_is_bool. apply cmp_mismatch_is_bool. -Qed. - -Lemma cmpu_is_bool: - forall c v1 v2, is_bool (cmpu c v1 v2). -Proof. - destruct v1; destruct v2; simpl; try apply undef_is_bool. - apply of_bool_is_bool. - case (Int.eq i Int.zero). apply cmp_mismatch_is_bool. apply undef_is_bool. - case (Int.eq i0 Int.zero). apply cmp_mismatch_is_bool. apply undef_is_bool. - case (zeq b b0); intro. apply of_bool_is_bool. apply cmp_mismatch_is_bool. -Qed. - -Lemma cmpf_is_bool: - forall c v1 v2, is_bool (cmpf c v1 v2). -Proof. - destruct v1; destruct v2; simpl; - apply undef_is_bool || apply of_bool_is_bool. -Qed. - -Lemma notbool_is_bool: - forall v, is_bool (notbool v). -Proof. - destruct v; simpl. - apply undef_is_bool. apply of_bool_is_bool. - apply undef_is_bool. unfold is_bool; tauto. -Qed. - -Lemma notbool_xor: - forall v, is_bool v -> v = xor (notbool v) Vone. -Proof. - intros. elim H; intro. - subst v. reflexivity. - elim H0; intro; subst v; reflexivity. + intros. destruct v; simpl; auto. decEq. apply Int.zero_ext_and; auto. Qed. Lemma rolm_lt_zero: forall v, rolm v Int.one Int.one = cmp Clt v (Vint Int.zero). Proof. - intros. destruct v; simpl; auto. + intros. unfold cmp, cmp_bool; destruct v; simpl; auto. transitivity (Vint (Int.shru i (Int.repr (Z_of_nat Int.wordsize - 1)))). decEq. symmetry. rewrite Int.shru_rolm. auto. auto. rewrite Int.shru_lt_zero. destruct (Int.lt i Int.zero); auto. @@ -942,7 +934,7 @@ Lemma rolm_ge_zero: xor (rolm v Int.one Int.one) (Vint Int.one) = cmp Cge v (Vint Int.zero). Proof. intros. rewrite rolm_lt_zero. destruct v; simpl; auto. - destruct (Int.lt i Int.zero); auto. + unfold cmp; simpl. destruct (Int.lt i Int.zero); auto. Qed. (** The ``is less defined'' relation between values. @@ -953,6 +945,12 @@ Inductive lessdef: val -> val -> Prop := | lessdef_refl: forall v, lessdef v v | lessdef_undef: forall v, lessdef Vundef v. +Lemma lessdef_trans: + forall v1 v2 v3, lessdef v1 v2 -> lessdef v2 v3 -> lessdef v1 v3. +Proof. + intros. inv H. auto. constructor. +Qed. + Inductive lessdef_list: list val -> list val -> Prop := | lessdef_list_nil: lessdef_list nil nil @@ -972,6 +970,8 @@ Proof. left; congruence. tauto. tauto. Qed. +(** Compatibility of operations with the [lessdef] relation. *) + Lemma load_result_lessdef: forall chunk v1 v2, lessdef v1 v2 -> lessdef (load_result chunk v1) (load_result chunk v2). @@ -997,6 +997,37 @@ Proof. intros; inv H; simpl; auto. Qed. +Lemma add_lessdef: + forall v1 v1' v2 v2', + lessdef v1 v1' -> lessdef v2 v2' -> lessdef (add v1 v2) (add v1' v2'). +Proof. + intros. inv H. inv H0. auto. destruct v1'; simpl; auto. simpl; auto. +Qed. + +Lemma cmpu_bool_lessdef: + forall valid_ptr valid_ptr' c v1 v1' v2 v2' b, + (forall b ofs, valid_ptr b ofs = true -> valid_ptr' b ofs = true) -> + lessdef v1 v1' -> lessdef v2 v2' -> + cmpu_bool valid_ptr c v1 v2 = Some b -> + cmpu_bool valid_ptr' c v1' v2' = Some b. +Proof. + intros. + destruct v1; simpl in H2; try discriminate; + destruct v2; simpl in H2; try discriminate; + inv H0; inv H1; simpl; auto. + destruct (valid_ptr b0 (Int.unsigned i)) as []_eqn; try discriminate. + destruct (valid_ptr b1 (Int.unsigned i0)) as []_eqn; try discriminate. + rewrite (H _ _ Heqb2). rewrite (H _ _ Heqb0). auto. +Qed. + +Lemma of_optbool_lessdef: + forall ob ob', + (forall b, ob = Some b -> ob' = Some b) -> + lessdef (of_optbool ob) (of_optbool ob'). +Proof. + intros. destruct ob; simpl; auto. rewrite (H b); auto. +Qed. + End Val. (** * Values and memory injections *) @@ -1085,3 +1116,35 @@ Qed. Hint Resolve inject_incr_refl val_inject_incr val_list_inject_incr. +Lemma val_inject_lessdef: + forall v1 v2, Val.lessdef v1 v2 <-> val_inject (fun b => Some(b, 0)) v1 v2. +Proof. + intros; split; intros. + inv H; auto. destruct v2; econstructor; eauto. rewrite Int.add_zero; auto. + inv H; auto. inv H0. rewrite Int.add_zero; auto. +Qed. + +Lemma val_list_inject_lessdef: + forall vl1 vl2, Val.lessdef_list vl1 vl2 <-> val_list_inject (fun b => Some(b, 0)) vl1 vl2. +Proof. + intros; split. + induction 1; constructor; auto. apply val_inject_lessdef; auto. + induction 1; constructor; auto. apply val_inject_lessdef; auto. +Qed. + +(** The identity injection gives rise to the "less defined than" relation. *) + +Definition inject_id : meminj := fun b => Some(b, 0). + +Lemma val_inject_id: + forall v1 v2, + val_inject inject_id v1 v2 <-> Val.lessdef v1 v2. +Proof. + intros; split; intros. + inv H. constructor. constructor. + unfold inject_id in H0. inv H0. rewrite Int.add_zero. constructor. + constructor. + inv H. destruct v2; econstructor. unfold inject_id; reflexivity. rewrite Int.add_zero; auto. + constructor. +Qed. + |