diff options
Diffstat (limited to 'backend')
| -rw-r--r-- | backend/CSE.v | 8 | ||||
| -rw-r--r-- | backend/CSEproof.v | 10 | ||||
| -rw-r--r-- | backend/ValueAnalysis.v | 8 | ||||
| -rw-r--r-- | backend/ValueDomain.v | 640 |
4 files changed, 365 insertions, 301 deletions
diff --git a/backend/CSE.v b/backend/CSE.v index e9006d4f..c0efa941 100644 --- a/backend/CSE.v +++ b/backend/CSE.v @@ -289,10 +289,10 @@ Definition kill_loads_after_store Definition store_normalized_range (chunk: memory_chunk) : aval := match chunk with - | Mint8signed => Sgn 8 - | Mint8unsigned => Uns 8 - | Mint16signed => Sgn 16 - | Mint16unsigned => Uns 16 + | Mint8signed => Sgn Ptop 8 + | Mint8unsigned => Uns Ptop 8 + | Mint16signed => Sgn Ptop 16 + | Mint16unsigned => Uns Ptop 16 | _ => Vtop end. diff --git a/backend/CSEproof.v b/backend/CSEproof.v index 74e3ceca..c24fa69b 100644 --- a/backend/CSEproof.v +++ b/backend/CSEproof.v @@ -493,10 +493,10 @@ Lemma store_normalized_range_sound: Val.lessdef (Val.load_result chunk v) v. Proof. intros. destruct chunk; simpl in *; destruct v; auto. -- inv H. rewrite is_sgn_sign_ext in H3 by omega. rewrite H3; auto. -- inv H. rewrite is_uns_zero_ext in H3 by omega. rewrite H3; auto. -- inv H. rewrite is_sgn_sign_ext in H3 by omega. rewrite H3; auto. -- inv H. rewrite is_uns_zero_ext in H3 by omega. rewrite H3; auto. +- inv H. rewrite is_sgn_sign_ext in H4 by omega. rewrite H4; auto. +- inv H. rewrite is_uns_zero_ext in H4 by omega. rewrite H4; auto. +- inv H. rewrite is_sgn_sign_ext in H4 by omega. rewrite H4; auto. +- inv H. rewrite is_uns_zero_ext in H4 by omega. rewrite H4; auto. Qed. Lemma add_store_result_hold: @@ -696,7 +696,7 @@ Proof. rs#r = Vptr b o -> aaddr approx r = Stk i -> b = sp /\ i = o). { intros until i. unfold aaddr; subst approx. intros. - specialize (H5 r). rewrite H6 in H5. rewrite match_aptr_of_aval in H5. + specialize (H5 r). rewrite H6 in H5. apply match_aptr_of_aval in H5. rewrite H10 in H5. inv H5. split; auto. eapply bc_stack; eauto. } exploit (A rsrc); eauto. intros [P Q]. diff --git a/backend/ValueAnalysis.v b/backend/ValueAnalysis.v index 28934ce9..c559aa25 100644 --- a/backend/ValueAnalysis.v +++ b/backend/ValueAnalysis.v @@ -79,11 +79,11 @@ Definition transfer_builtin (ae: aenv) (am: amem) (rm: romem) (ef: external_func VA.State (AE.set res a ae) am | Builtin_vstore chunk aaddr av => let am' := storev chunk am aaddr av in - VA.State (AE.set res itop ae) (mlub am am') + VA.State (AE.set res ntop ae) (mlub am am') | Builtin_memcpy sz al adst asrc => let p := loadbytes am rm (aptr_of_aval asrc) in let am' := storebytes am (aptr_of_aval adst) sz p in - VA.State (AE.set res itop ae) am' + VA.State (AE.set res ntop ae) am' | Builtin_annot_val av => VA.State (AE.set res av ae) am | Builtin_default => @@ -164,9 +164,9 @@ Definition store_init_data (ab: ablock) (p: Z) (id: init_data) : ablock := | Init_int32 n => ablock_store Mint32 ab p (I n) | Init_int64 n => ablock_store Mint64 ab p (L n) | Init_float32 n => ablock_store Mfloat32 ab p - (if propagate_float_constants tt then FS n else ftop) + (if propagate_float_constants tt then FS n else ntop) | Init_float64 n => ablock_store Mfloat64 ab p - (if propagate_float_constants tt then F n else ftop) + (if propagate_float_constants tt then F n else ntop) | Init_addrof symb ofs => ablock_store Mint32 ab p (Ptr (Gl symb ofs)) | Init_space n => ab end. diff --git a/backend/ValueDomain.v b/backend/ValueDomain.v index b4c1df61..3d95bdd1 100644 --- a/backend/ValueDomain.v +++ b/backend/ValueDomain.v @@ -64,7 +64,11 @@ Variable bc: block_classification. (** * Abstracting the result of conditions (type [option bool]) *) -Inductive abool := Bnone | Just (b: bool) | Maybe (b: bool) | Btop. +Inductive abool := + | Bnone (**r always [None] (undefined) *) + | Just (b: bool) (**r always [Some b] (defined and known to be [b]) *) + | Maybe (b: bool) (**r either [None] or [Some b] (known to be [b] if defined) *) + | Btop. (**r unknown, all results are possible *) Inductive cmatch: option bool -> abool -> Prop := | cmatch_none: cmatch None Bnone @@ -121,14 +125,14 @@ Qed. (** * Abstracting pointers *) Inductive aptr : Type := - | Pbot - | Gl (id: ident) (ofs: int) - | Glo (id: ident) - | Glob - | Stk (ofs: int) - | Stack - | Nonstack - | Ptop. + | Pbot (**r bottom (empty set of pointers) *) + | Gl (id: ident) (ofs: int) (**r pointer into the block for global variable [id] at offset [ofs] *) + | Glo (id: ident) (**r pointer anywhere into the block for global [id] *) + | Glob (**r pointer into any global variable *) + | Stk (ofs: int) (**r pointer into the current stack frame at offset [ofs] *) + | Stack (**r pointer anywhere into the current stack frame *) + | Nonstack (**r pointer anywhere but into the current stack frame *) + | Ptop. (**r any valid pointer *) Definition eq_aptr: forall (p1 p2: aptr), {p1=p2} + {p1<>p2}. Proof. @@ -301,6 +305,7 @@ Definition pincl (p q: aptr) : bool := | (Gl _ _ | Glo _ | Glob | Nonstack), Nonstack => true | Stk ofs1, Stk ofs2 => Int.eq_dec ofs1 ofs2 | Stk ofs1, Stack => true + | Stack, Stack => true | _, Ptop => true | _, _ => false end. @@ -311,6 +316,14 @@ Proof. InvBooleans; subst; auto with va. Qed. +Lemma pincl_ge_2: forall p q, pge p q -> pincl q p = true. +Proof. + destruct 1; simpl; auto. +- destruct p; auto. +- destruct p; simpl; auto; rewrite ! proj_sumbool_is_true; auto. +- rewrite ! proj_sumbool_is_true; auto. +Qed. + Lemma pincl_sound: forall b ofs p q, pincl p q = true -> pmatch b ofs p -> pmatch b ofs q. @@ -503,15 +516,25 @@ Qed. (** * Abstracting values *) Inductive aval : Type := - | Vbot - | I (n: int) - | Uns (n: Z) - | Sgn (n: Z) - | L (n: int64) - | F (f: float) - | FS (f: float32) - | Ptr (p: aptr) - | Ifptr (p: aptr). + | Vbot (**r bottom (empty set of values) *) + | I (n: int) (**r exactly [Vint n] *) + | Uns (p: aptr) (n: Z) (**r a [n]-bit unsigned integer, or [Vundef] *) + | Sgn (p: aptr) (n: Z) (**r a [n]-bit signed integer, or [Vundef] *) + | L (n: int64) (**r exactly [Vlong n] *) + | F (f: float) (**r exactly [Vfloat f] *) + | FS (f: float32) (**r exactly [Vsingle f] *) + | Ptr (p: aptr) (**r a pointer from the set [p], or [Vundef] *) + | Ifptr (p: aptr). (**r a pointer from the set [p], or a number, or [Vundef] *) + +(** The "top" of the value domain is defined as any pointer, or any + number, or [Vundef]. *) + +Definition Vtop := Ifptr Ptop. + +(** The [p] parameter (an abstract pointer) to [Uns] and [Sgn] helps keeping + track of pointers that leak through arithmetic operations such as shifts. + See the section "Tracking leakage of pointers" below. + In strict analysis mode, [p] is always [Pbot]. *) Definition eq_aval: forall (v1 v2: aval), {v1=v2} + {v1<>v2}. Proof. @@ -519,11 +542,6 @@ Proof. decide equality. Defined. -Definition Vtop := Ifptr Ptop. -Definition itop := Ifptr Pbot. -Definition ftop := Ifptr Pbot. -Definition ltop := Ifptr Pbot. - Definition is_uns (n: Z) (i: int) : Prop := forall m, 0 <= m < Int.zwordsize -> m >= n -> Int.testbit i m = false. Definition is_sgn (n: Z) (i: int) : Prop := @@ -531,10 +549,10 @@ Definition is_sgn (n: Z) (i: int) : Prop := Inductive vmatch : val -> aval -> Prop := | vmatch_i: forall i, vmatch (Vint i) (I i) - | vmatch_Uns: forall i n, 0 <= n -> is_uns n i -> vmatch (Vint i) (Uns n) - | vmatch_Uns_undef: forall n, vmatch Vundef (Uns n) - | vmatch_Sgn: forall i n, 0 < n -> is_sgn n i -> vmatch (Vint i) (Sgn n) - | vmatch_Sgn_undef: forall n, vmatch Vundef (Sgn n) + | vmatch_Uns: forall p i n, 0 <= n -> is_uns n i -> vmatch (Vint i) (Uns p n) + | vmatch_Uns_undef: forall p n, vmatch Vundef (Uns p n) + | vmatch_Sgn: forall p i n, 0 < n -> is_sgn n i -> vmatch (Vint i) (Sgn p n) + | vmatch_Sgn_undef: forall p n, vmatch Vundef (Sgn p n) | vmatch_l: forall i, vmatch (Vlong i) (L i) | vmatch_f: forall f, vmatch (Vfloat f) (F f) | vmatch_s: forall f, vmatch (Vsingle f) (FS f) @@ -560,23 +578,7 @@ Proof. intros. apply vmatch_ifptr. intros. subst v. inv H; eapply pmatch_top'; eauto. Qed. -Lemma vmatch_itop: forall i, vmatch (Vint i) itop. -Proof. intros; constructor. Qed. - -Lemma vmatch_undef_itop: vmatch Vundef itop. -Proof. constructor. Qed. - -Lemma vmatch_ftop: forall f, vmatch (Vfloat f) ftop. -Proof. intros; constructor. Qed. - -Lemma vmatch_ftop_single: forall f, vmatch (Vsingle f) ftop. -Proof. intros; constructor. Qed. - -Lemma vmatch_undef_ftop: vmatch Vundef ftop. -Proof. constructor. Qed. - -Hint Constructors vmatch : va. -Hint Resolve vmatch_itop vmatch_undef_itop vmatch_ftop vmatch_ftop_single vmatch_undef_ftop : va. +Hint Extern 1 (vmatch _ _) => constructor : va. (* Some properties about [is_uns] and [is_sgn]. *) @@ -692,21 +694,53 @@ Proof. rewrite Int.bits_zero. destruct (zeq i 0). subst i; auto. apply H; omega. Qed. +(** Tracking leakage of pointers through arithmetic operations. + +In the CompCert semantics, arithmetic operations (e.g. "xor") applied +to pointer values are undefined or produce the [Vundef] result. +So, in strict mode, we can abstract the result values of such operations +as [Ifptr Pbot], namely: [Vundef], or any number, but not a pointer. + +In real code, such arithmetic over pointers occurs, so we need to be +more prudent. The policy we take, inspired by that of GCC, is that +"undefined" arithmetic operations involving pointer arguments can +produce a pointer, but not any pointer: rather, a pointer to the same +block, but possibly with a different offset. Hence, if the operation +has a pointer to abstract region [p] as argument, the result value +can be a pointer to abstract region [poffset p]. In other words, +the result value is abstracted as [Ifptr (poffset p)]. + +We encapsulate this reasoning in the following [ntop1] and [ntop2] functions +("numerical top"). *) + +Definition provenance (x: aval) : aptr := + if va_strict tt then Pbot else + match x with + | Ptr p | Ifptr p | Uns p _ | Sgn p _ => poffset p + | _ => Pbot + end. + +Definition ntop : aval := Ifptr Pbot. + +Definition ntop1 (x: aval) : aval := Ifptr (provenance x). + +Definition ntop2 (x y: aval) : aval := Ifptr (plub (provenance x) (provenance y)). + (** Smart constructors for [Uns] and [Sgn]. *) -Definition uns (n: Z) : aval := - if zle n 1 then Uns 1 - else if zle n 7 then Uns 7 - else if zle n 8 then Uns 8 - else if zle n 15 then Uns 15 - else if zle n 16 then Uns 16 - else itop. +Definition uns (p: aptr) (n: Z) : aval := + if zle n 1 then Uns p 1 + else if zle n 7 then Uns p 7 + else if zle n 8 then Uns p 8 + else if zle n 15 then Uns p 15 + else if zle n 16 then Uns p 16 + else Ifptr p. -Definition sgn (n: Z) : aval := - if zle n 8 then Sgn 8 else if zle n 16 then Sgn 16 else itop. +Definition sgn (p: aptr) (n: Z) : aval := + if zle n 8 then Sgn p 8 else if zle n 16 then Sgn p 16 else Ifptr p. Lemma vmatch_uns': - forall i n, is_uns (Zmax 0 n) i -> vmatch (Vint i) (uns n). + forall p i n, is_uns (Zmax 0 n) i -> vmatch (Vint i) (uns p n). Proof. intros. assert (A: forall n', n' >= 0 -> n' >= n -> is_uns n' i) by (eauto with va). @@ -720,12 +754,12 @@ Proof. Qed. Lemma vmatch_uns: - forall i n, is_uns n i -> vmatch (Vint i) (uns n). + forall p i n, is_uns n i -> vmatch (Vint i) (uns p n). Proof. intros. apply vmatch_uns'. eauto with va. Qed. -Lemma vmatch_uns_undef: forall n, vmatch Vundef (uns n). +Lemma vmatch_uns_undef: forall p n, vmatch Vundef (uns p n). Proof. intros. unfold uns. destruct (zle n 1). auto with va. @@ -736,7 +770,7 @@ Proof. Qed. Lemma vmatch_sgn': - forall i n, is_sgn (Zmax 1 n) i -> vmatch (Vint i) (sgn n). + forall p i n, is_sgn (Zmax 1 n) i -> vmatch (Vint i) (sgn p n). Proof. intros. assert (A: forall n', n' >= 1 -> n' >= n -> is_sgn n' i) by (eauto with va). @@ -746,12 +780,12 @@ Proof. Qed. Lemma vmatch_sgn: - forall i n, is_sgn n i -> vmatch (Vint i) (sgn n). + forall p i n, is_sgn n i -> vmatch (Vint i) (sgn p n). Proof. intros. apply vmatch_sgn'. eauto with va. Qed. -Lemma vmatch_sgn_undef: forall n, vmatch Vundef (sgn n). +Lemma vmatch_sgn_undef: forall p n, vmatch Vundef (sgn p n). Proof. intros. unfold sgn. destruct (zle n 8). auto with va. @@ -761,7 +795,7 @@ Qed. Hint Resolve vmatch_uns vmatch_uns_undef vmatch_sgn vmatch_sgn_undef : va. Lemma vmatch_Uns_1: - forall v, vmatch v (Uns 1) -> v = Vundef \/ v = Vint Int.zero \/ v = Vint Int.one. + forall p v, vmatch v (Uns p 1) -> v = Vundef \/ v = Vint Int.zero \/ v = Vint Int.one. Proof. intros. inv H; auto. right. exploit is_uns_1; eauto. intuition congruence. Qed. @@ -774,11 +808,11 @@ Inductive vge: aval -> aval -> Prop := | vge_l: forall i, vge (L i) (L i) | vge_f: forall f, vge (F f) (F f) | vge_s: forall f, vge (FS f) (FS f) - | vge_uns_i: forall n i, 0 <= n -> is_uns n i -> vge (Uns n) (I i) - | vge_uns_uns: forall n1 n2, n1 >= n2 -> vge (Uns n1) (Uns n2) - | vge_sgn_i: forall n i, 0 < n -> is_sgn n i -> vge (Sgn n) (I i) - | vge_sgn_sgn: forall n1 n2, n1 >= n2 -> vge (Sgn n1) (Sgn n2) - | vge_sgn_uns: forall n1 n2, n1 > n2 -> vge (Sgn n1) (Uns n2) + | vge_uns_i: forall p n i, 0 <= n -> is_uns n i -> vge (Uns p n) (I i) + | vge_uns_uns: forall p1 n1 p2 n2, n1 >= n2 -> pge p1 p2 -> vge (Uns p1 n1) (Uns p2 n2) + | vge_sgn_i: forall p n i, 0 < n -> is_sgn n i -> vge (Sgn p n) (I i) + | vge_sgn_sgn: forall p1 n1 p2 n2, n1 >= n2 -> pge p1 p2 -> vge (Sgn p1 n1) (Sgn p2 n2) + | vge_sgn_uns: forall p1 n1 p2 n2, n1 > n2 -> pge p1 p2 -> vge (Sgn p1 n1) (Uns p2 n2) | vge_p_p: forall p q, pge p q -> vge (Ptr p) (Ptr q) | vge_ip_p: forall p q, pge p q -> vge (Ifptr p) (Ptr q) | vge_ip_ip: forall p q, pge p q -> vge (Ifptr p) (Ifptr q) @@ -786,8 +820,8 @@ Inductive vge: aval -> aval -> Prop := | vge_ip_l: forall p i, vge (Ifptr p) (L i) | vge_ip_f: forall p f, vge (Ifptr p) (F f) | vge_ip_s: forall p f, vge (Ifptr p) (FS f) - | vge_ip_uns: forall p n, vge (Ifptr p) (Uns n) - | vge_ip_sgn: forall p n, vge (Ifptr p) (Sgn n). + | vge_ip_uns: forall p q n, pge p q -> vge (Ifptr p) (Uns q n) + | vge_ip_sgn: forall p q n, pge p q -> vge (Ifptr p) (Sgn q n). Hint Constructors vge : va. @@ -805,13 +839,13 @@ Qed. Lemma vge_trans: forall u v, vge u v -> forall w, vge v w -> vge u w. Proof. - induction 1; intros w V; inv V; eauto with va; constructor; eapply pge_trans; eauto. + induction 1; intros w V; inv V; eauto using pge_trans with va. Qed. Lemma vmatch_ge: forall v x y, vge x y -> vmatch v y -> vmatch v x. Proof. - induction 1; intros V; inv V; eauto with va; constructor; eapply pmatch_ge; eauto. + induction 1; intros V; inv V; eauto using pmatch_ge with va. Qed. (** Least upper bound *) @@ -823,30 +857,32 @@ Definition vlub (v w: aval) : aval := | I i1, I i2 => if Int.eq i1 i2 then v else if Int.lt i1 Int.zero || Int.lt i2 Int.zero - then sgn (Z.max (ssize i1) (ssize i2)) - else uns (Z.max (usize i1) (usize i2)) - | I i, Uns n | Uns n, I i => + then sgn Pbot (Z.max (ssize i1) (ssize i2)) + else uns Pbot (Z.max (usize i1) (usize i2)) + | I i, Uns p n | Uns p n, I i => if Int.lt i Int.zero - then sgn (Z.max (ssize i) (n + 1)) - else uns (Z.max (usize i) n) - | I i, Sgn n | Sgn n, I i => - sgn (Z.max (ssize i) n) + then sgn p (Z.max (ssize i) (n + 1)) + else uns p (Z.max (usize i) n) + | I i, Sgn p n | Sgn p n, I i => + sgn p (Z.max (ssize i) n) | I i, (Ptr p | Ifptr p) | (Ptr p | Ifptr p), I i => if va_strict tt || Int.eq i Int.zero then Ifptr p else Vtop - | Uns n1, Uns n2 => Uns (Z.max n1 n2) - | Uns n1, Sgn n2 => sgn (Z.max (n1 + 1) n2) - | Sgn n1, Uns n2 => sgn (Z.max n1 (n2 + 1)) - | Sgn n1, Sgn n2 => sgn (Z.max n1 n2) + | Uns p1 n1, Uns p2 n2 => Uns (plub p1 p2) (Z.max n1 n2) + | Uns p1 n1, Sgn p2 n2 => sgn (plub p1 p2) (Z.max (n1 + 1) n2) + | Sgn p1 n1, Uns p2 n2 => sgn (plub p1 p2) (Z.max n1 (n2 + 1)) + | Sgn p1 n1, Sgn p2 n2 => sgn (plub p1 p2) (Z.max n1 n2) | F f1, F f2 => - if Float.eq_dec f1 f2 then v else ftop + if Float.eq_dec f1 f2 then v else ntop | FS f1, FS f2 => - if Float32.eq_dec f1 f2 then v else ftop + if Float32.eq_dec f1 f2 then v else ntop | L i1, L i2 => - if Int64.eq i1 i2 then v else ltop + if Int64.eq i1 i2 then v else ntop | Ptr p1, Ptr p2 => Ptr(plub p1 p2) | Ptr p1, Ifptr p2 => Ifptr(plub p1 p2) | Ifptr p1, Ptr p2 => Ifptr(plub p1 p2) | Ifptr p1, Ifptr p2 => Ifptr(plub p1 p2) + | (Ptr p1 | Ifptr p1), (Uns p2 _ | Sgn p2 _) => Ifptr(plub p1 p2) + | (Uns p1 _ | Sgn p1 _), (Ptr p2 | Ifptr p2) => Ifptr(plub p1 p2) | _, (Ptr p | Ifptr p) | (Ptr p | Ifptr p), _ => if va_strict tt then Ifptr p else Vtop | _, _ => Vtop end. @@ -859,10 +895,14 @@ Proof. congruence. rewrite orb_comm. destruct (Int.lt n0 Int.zero || Int.lt n Int.zero); f_equal; apply Z.max_comm. -- f_equal; apply Z.max_comm. -- f_equal; apply Z.max_comm. -- f_equal; apply Z.max_comm. -- f_equal; apply Z.max_comm. +- f_equal. apply plub_comm. apply Z.max_comm. +- f_equal. apply plub_comm. apply Z.max_comm. +- f_equal; apply plub_comm. +- f_equal; apply plub_comm. +- f_equal. apply plub_comm. apply Z.max_comm. +- f_equal. apply plub_comm. apply Z.max_comm. +- f_equal; apply plub_comm. +- f_equal; apply plub_comm. - rewrite Int64.eq_sym. predSpec Int64.eq Int64.eq_spec n0 n; congruence. - rewrite dec_eq_sym. destruct (Float.eq_dec f0 f). congruence. auto. - rewrite dec_eq_sym. destruct (Float32.eq_dec f0 f). congruence. auto. @@ -870,11 +910,15 @@ Proof. - f_equal; apply plub_comm. - f_equal; apply plub_comm. - f_equal; apply plub_comm. +- f_equal; apply plub_comm. +- f_equal; apply plub_comm. +- f_equal; apply plub_comm. +- f_equal; apply plub_comm. Qed. -Lemma vge_uns_uns': forall n, vge (uns n) (Uns n). +Lemma vge_uns_uns': forall p n, vge (uns p n) (Uns p n). Proof. - unfold uns, itop; intros. + unfold uns; intros. destruct (zle n 1). auto with va. destruct (zle n 7). auto with va. destruct (zle n 8). auto with va. @@ -882,21 +926,21 @@ Proof. destruct (zle n 16); auto with va. Qed. -Lemma vge_uns_i': forall n i, 0 <= n -> is_uns n i -> vge (uns n) (I i). +Lemma vge_uns_i': forall p n i, 0 <= n -> is_uns n i -> vge (uns p n) (I i). Proof. - intros. apply vge_trans with (Uns n). apply vge_uns_uns'. auto with va. + intros. apply vge_trans with (Uns p n). apply vge_uns_uns'. auto with va. Qed. -Lemma vge_sgn_sgn': forall n, vge (sgn n) (Sgn n). +Lemma vge_sgn_sgn': forall p n, vge (sgn p n) (Sgn p n). Proof. - unfold sgn, itop; intros. + unfold sgn; intros. destruct (zle n 8). auto with va. destruct (zle n 16); auto with va. Qed. -Lemma vge_sgn_i': forall n i, 0 < n -> is_sgn n i -> vge (sgn n) (I i). +Lemma vge_sgn_i': forall p n i, 0 < n -> is_sgn n i -> vge (sgn p n) (I i). Proof. - intros. apply vge_trans with (Sgn n). apply vge_sgn_sgn'. auto with va. + intros. apply vge_trans with (Sgn p n). apply vge_sgn_sgn'. auto with va. Qed. Hint Resolve vge_uns_uns' vge_uns_i' vge_sgn_sgn' vge_sgn_i' : va. @@ -915,9 +959,9 @@ Qed. Lemma vge_lub_l: forall x y, vge (vlub x y) x. Proof. - assert (IFSTRICT: forall (cond: bool) x y, vge x y -> vge (if cond then x else Vtop ) y). + assert (IFSTRICT: forall (cond: bool) x1 x2 y, vge x1 y -> vge x2 y -> vge (if cond then x1 else x2) y). { destruct cond; auto with va. } - unfold vlub; destruct x, y; eauto with va. + unfold vlub; destruct x, y; eauto using pge_lub_l with va. - predSpec Int.eq Int.eq_spec n n0. auto with va. destruct (Int.lt n Int.zero || Int.lt n0 Int.zero). apply vge_sgn_i'. generalize (ssize_pos n); xomega. eauto with va. @@ -928,20 +972,16 @@ Proof. - apply vge_sgn_i'. generalize (ssize_pos n); xomega. eauto with va. - destruct (Int.lt n0 Int.zero). eapply vge_trans. apply vge_sgn_sgn'. - apply vge_trans with (Sgn (n + 1)); eauto with va. + apply vge_trans with (Sgn p (n + 1)); eauto with va. eapply vge_trans. apply vge_uns_uns'. eauto with va. - eapply vge_trans. apply vge_sgn_sgn'. - apply vge_trans with (Sgn (n + 1)); eauto with va. -- eapply vge_trans. apply vge_sgn_sgn'. eauto with va. -- eapply vge_trans. apply vge_sgn_sgn'. eauto with va. + apply vge_trans with (Sgn p (n + 1)); eauto using pge_lub_l with va. - eapply vge_trans. apply vge_sgn_sgn'. eauto with va. +- eapply vge_trans. apply vge_sgn_sgn'. eauto using pge_lub_l with va. +- eapply vge_trans. apply vge_sgn_sgn'. eauto using pge_lub_l with va. - destruct (Int64.eq n n0); constructor. - destruct (Float.eq_dec f f0); constructor. - destruct (Float32.eq_dec f f0); constructor. -- constructor; apply pge_lub_l; auto. -- constructor; apply pge_lub_l; auto. -- constructor; apply pge_lub_l; auto. -- constructor; apply pge_lub_l; auto. Qed. Lemma vge_lub_r: @@ -962,20 +1002,28 @@ Proof. intros. rewrite vlub_comm. apply vmatch_lub_l; auto. Qed. +(** In the CompCert semantics, a memory load or store succeeds only + if the address is a pointer value. Hence, in strict mode, + [aptr_of_aval x] returns [Pbot] (no pointer value) if [x] + denotes a number or [Vundef]. However, in real code, memory + addresses are sometimes synthesized from integers, e.g. an absolute + address for a hardware device. It is a reasonable assumption + that these absolute addresses do not point within the stack block, + however. Therefore, in relaxed mode, [aptr_of_aval x] returns + [Nonstack] (any pointer outside the stack) when [x] denotes a number. *) + Definition aptr_of_aval (v: aval) : aptr := match v with | Ptr p => p | Ifptr p => p - | _ => Pbot + | _ => if va_strict tt then Pbot else Nonstack end. Lemma match_aptr_of_aval: forall b ofs av, - vmatch (Vptr b ofs) av <-> pmatch b ofs (aptr_of_aval av). + vmatch (Vptr b ofs) av -> pmatch b ofs (aptr_of_aval av). Proof. - unfold aptr_of_aval; intros; split; intros. -- inv H; auto. -- destruct av; ((constructor; assumption) || inv H). + unfold aptr_of_aval; intros. inv H; auto. Qed. Definition vplub (v: aval) (p: aptr) : aptr := @@ -1010,8 +1058,7 @@ Qed. Definition vpincl (v: aval) (p: aptr) : bool := match v with - | Ptr q => pincl q p - | Ifptr q => pincl q p + | Ptr q | Ifptr q | Uns q _ | Sgn q _ => pincl q p | _ => true end. @@ -1031,36 +1078,26 @@ Definition vincl (v w: aval) : bool := match v, w with | Vbot, _ => true | I i, I j => Int.eq_dec i j - | I i, Uns n => Int.eq_dec (Int.zero_ext n i) i && zle 0 n - | I i, Sgn n => Int.eq_dec (Int.sign_ext n i) i && zlt 0 n - | Uns n, Uns m => zle n m - | Uns n, Sgn m => zlt n m - | Sgn n, Sgn m => zle n m + | I i, Uns p n => Int.eq_dec (Int.zero_ext n i) i && zle 0 n + | I i, Sgn p n => Int.eq_dec (Int.sign_ext n i) i && zlt 0 n + | Uns p n, Uns q m => zle n m && pincl p q + | Uns p n, Sgn q m => zlt n m && pincl p q + | Sgn p n, Sgn q m => zle n m && pincl p q | L i, L j => Int64.eq_dec i j | F i, F j => Float.eq_dec i j | FS i, FS j => Float32.eq_dec i j | Ptr p, Ptr q => pincl p q - | Ptr p, Ifptr q => pincl p q - | Ifptr p, Ifptr q => pincl p q + | (Ptr p | Ifptr p | Uns p _ | Sgn p _), Ifptr q => pincl p q | _, Ifptr _ => true | _, _ => false end. Lemma vincl_ge: forall v w, vincl v w = true -> vge w v. Proof. - unfold vincl; destruct v; destruct w; intros; try discriminate; auto with va. - InvBooleans. subst; auto with va. - InvBooleans. constructor; auto. rewrite is_uns_zero_ext; auto. - InvBooleans. constructor; auto. rewrite is_sgn_sign_ext; auto. - InvBooleans. constructor; auto with va. - InvBooleans. constructor; auto with va. - InvBooleans. constructor; auto with va. - InvBooleans. subst; auto with va. - InvBooleans. subst; auto with va. - InvBooleans. subst; auto with va. - constructor; apply pincl_ge; auto. - constructor; apply pincl_ge; auto. - constructor; apply pincl_ge; auto. + unfold vincl; destruct v; destruct w; + intros; try discriminate; try InvBooleans; try subst; auto using pincl_ge with va. +- constructor; auto. rewrite is_uns_zero_ext; auto. +- constructor; auto. rewrite is_sgn_sign_ext; auto. Qed. (** Loading constants *) @@ -1105,7 +1142,7 @@ Qed. (** Generic operations that just do constant propagation. *) Definition unop_int (sem: int -> int) (x: aval) := - match x with I n => I (sem n) | _ => itop end. + match x with I n => I (sem n) | _ => ntop1 x end. Lemma unop_int_sound: forall sem v x, @@ -1116,7 +1153,7 @@ Proof. Qed. Definition binop_int (sem: int -> int -> int) (x y: aval) := - match x, y with I n, I m => I (sem n m) | _, _ => itop end. + match x, y with I n, I m => I (sem n m) | _, _ => ntop2 x y end. Lemma binop_int_sound: forall sem v x w y, @@ -1127,7 +1164,7 @@ Proof. Qed. Definition unop_float (sem: float -> float) (x: aval) := - match x with F n => F (sem n) | _ => ftop end. + match x with F n => F (sem n) | _ => ntop1 x end. Lemma unop_float_sound: forall sem v x, @@ -1138,7 +1175,7 @@ Proof. Qed. Definition binop_float (sem: float -> float -> float) (x y: aval) := - match x, y with F n, F m => F (sem n m) | _, _ => ftop end. + match x, y with F n, F m => F (sem n m) | _, _ => ntop2 x y end. Lemma binop_float_sound: forall sem v x w y, @@ -1149,7 +1186,7 @@ Proof. Qed. Definition unop_single (sem: float32 -> float32) (x: aval) := - match x with FS n => FS (sem n) | _ => ftop end. + match x with FS n => FS (sem n) | _ => ntop1 x end. Lemma unop_single_sound: forall sem v x, @@ -1160,7 +1197,7 @@ Proof. Qed. Definition binop_single (sem: float32 -> float32 -> float32) (x y: aval) := - match x, y with FS n, FS m => FS (sem n m) | _, _ => ftop end. + match x, y with FS n, FS m => FS (sem n m) | _, _ => ntop2 x y end. Lemma binop_single_sound: forall sem v x w y, @@ -1178,19 +1215,19 @@ Definition shl (v w: aval) := if Int.ltu amount Int.iwordsize then match v with | I i => I (Int.shl i amount) - | Uns n => uns (n + Int.unsigned amount) - | Sgn n => sgn (n + Int.unsigned amount) - | _ => itop + | Uns p n => uns p (n + Int.unsigned amount) + | Sgn p n => sgn p (n + Int.unsigned amount) + | _ => ntop1 v end - else itop - | _ => itop + else ntop1 v + | _ => ntop1 v end. Lemma shl_sound: forall v w x y, vmatch v x -> vmatch w y -> vmatch (Val.shl v w) (shl x y). Proof. intros. - assert (DEFAULT: vmatch (Val.shl v w) itop). + assert (DEFAULT: vmatch (Val.shl v w) (ntop1 x)). { destruct v; destruct w; simpl; try constructor. destruct (Int.ltu i0 Int.iwordsize); constructor. @@ -1214,18 +1251,18 @@ Definition shru (v w: aval) := if Int.ltu amount Int.iwordsize then match v with | I i => I (Int.shru i amount) - | Uns n => uns (n - Int.unsigned amount) - | _ => uns (Int.zwordsize - Int.unsigned amount) + | Uns p n => uns p (n - Int.unsigned amount) + | _ => uns (provenance v) (Int.zwordsize - Int.unsigned amount) end - else itop - | _ => itop + else ntop1 v + | _ => ntop1 v end. Lemma shru_sound: forall v w x y, vmatch v x -> vmatch w y -> vmatch (Val.shru v w) (shru x y). Proof. intros. - assert (DEFAULT: vmatch (Val.shru v w) itop). + assert (DEFAULT: vmatch (Val.shru v w) (ntop1 x)). { destruct v; destruct w; simpl; try constructor. destruct (Int.ltu i0 Int.iwordsize); constructor. @@ -1233,7 +1270,7 @@ Proof. destruct y; auto. inv H0. unfold shru, Val.shru. destruct (Int.ltu n Int.iwordsize) eqn:LTU; auto. exploit Int.ltu_inv; eauto. intros RANGE. change (Int.unsigned Int.iwordsize) with Int.zwordsize in RANGE. - assert (DEFAULT2: forall i, vmatch (Vint (Int.shru i n)) (uns (Int.zwordsize - Int.unsigned n))). + assert (DEFAULT2: forall i, vmatch (Vint (Int.shru i n)) (uns (provenance x) (Int.zwordsize - Int.unsigned n))). { intros. apply vmatch_uns. red; intros. rewrite Int.bits_shru by omega. apply zlt_false. omega. @@ -1252,19 +1289,19 @@ Definition shr (v w: aval) := if Int.ltu amount Int.iwordsize then match v with | I i => I (Int.shr i amount) - | Uns n => sgn (n + 1 - Int.unsigned amount) - | Sgn n => sgn (n - Int.unsigned amount) - | _ => sgn (Int.zwordsize - Int.unsigned amount) + | Uns p n => sgn p (n + 1 - Int.unsigned amount) + | Sgn p n => sgn p (n - Int.unsigned amount) + | _ => sgn (provenance v) (Int.zwordsize - Int.unsigned amount) end - else itop - | _ => itop + else ntop1 v + | _ => ntop1 v end. Lemma shr_sound: forall v w x y, vmatch v x -> vmatch w y -> vmatch (Val.shr v w) (shr x y). Proof. intros. - assert (DEFAULT: vmatch (Val.shr v w) itop). + assert (DEFAULT: vmatch (Val.shr v w) (ntop1 x)). { destruct v; destruct w; simpl; try constructor. destruct (Int.ltu i0 Int.iwordsize); constructor. @@ -1272,7 +1309,7 @@ Proof. destruct y; auto. inv H0. unfold shr, Val.shr. destruct (Int.ltu n Int.iwordsize) eqn:LTU; auto. exploit Int.ltu_inv; eauto. intros RANGE. change (Int.unsigned Int.iwordsize) with Int.zwordsize in RANGE. - assert (DEFAULT2: forall i, vmatch (Vint (Int.shr i n)) (sgn (Int.zwordsize - Int.unsigned n))). + assert (DEFAULT2: forall i, vmatch (Vint (Int.shr i n)) (sgn (provenance x) (Int.zwordsize - Int.unsigned n))). { intros. apply vmatch_sgn. red; intros. rewrite ! Int.bits_shr by omega. f_equal. @@ -1280,7 +1317,7 @@ Proof. destruct (zlt (Int.zwordsize - 1 + Int.unsigned n) Int.zwordsize); omega. } - assert (SGN: forall i p, is_sgn p i -> 0 < p -> vmatch (Vint (Int.shr i n)) (sgn (p - Int.unsigned n))). + assert (SGN: forall q i p, is_sgn p i -> 0 < p -> vmatch (Vint (Int.shr i n)) (sgn q (p - Int.unsigned n))). { intros. apply vmatch_sgn'. red; intros. zify. rewrite ! Int.bits_shr by omega. @@ -1300,12 +1337,13 @@ Qed. Definition and (v w: aval) := match v, w with | I i1, I i2 => I (Int.and i1 i2) - | I i, Uns n | Uns n, I i => uns (Z.min n (usize i)) - | I i, _ | _, I i => uns (usize i) - | Uns n1, Uns n2 => uns (Z.min n1 n2) - | Uns n, _ | _, Uns n => uns n - | Sgn n1, Sgn n2 => sgn (Z.max n1 n2) - | _, _ => itop + | I i, Uns p n | Uns p n, I i => uns p (Z.min n (usize i)) + | I i, x | x, I i => uns (provenance x) (usize i) + | Uns p1 n1, Uns p2 n2 => uns (plub p1 p2) (Z.min n1 n2) + | Uns p n, _ => uns (plub p (provenance w)) n + | _, Uns p n => uns (plub (provenance v) p) n + | Sgn p1 n1, Sgn p2 n2 => sgn (plub p1 p2) (Z.max n1 n2) + | _, _ => ntop2 v w end. Lemma and_sound: @@ -1335,10 +1373,10 @@ Qed. Definition or (v w: aval) := match v, w with | I i1, I i2 => I (Int.or i1 i2) - | I i, Uns n | Uns n, I i => uns (Z.max n (usize i)) - | Uns n1, Uns n2 => uns (Z.max n1 n2) - | Sgn n1, Sgn n2 => sgn (Z.max n1 n2) - | _, _ => itop + | I i, Uns p n | Uns p n, I i => uns p (Z.max n (usize i)) + | Uns p1 n1, Uns p2 n2 => uns (plub p1 p2) (Z.max n1 n2) + | Sgn p1 n1, Sgn p2 n2 => sgn (plub p1 p2) (Z.max n1 n2) + | _, _ => ntop2 v w end. Lemma or_sound: @@ -1360,10 +1398,10 @@ Qed. Definition xor (v w: aval) := match v, w with | I i1, I i2 => I (Int.xor i1 i2) - | I i, Uns n | Uns n, I i => uns (Z.max n (usize i)) - | Uns n1, Uns n2 => uns (Z.max n1 n2) - | Sgn n1, Sgn n2 => sgn (Z.max n1 n2) - | _, _ => itop + | I i, Uns p n | Uns p n, I i => uns p (Z.max n (usize i)) + | Uns p1 n1, Uns p2 n2 => uns (plub p1 p2) (Z.max n1 n2) + | Sgn p1 n1, Sgn p2 n2 => sgn (plub p1 p2) (Z.max n1 n2) + | _, _ => ntop2 v w end. Lemma xor_sound: @@ -1385,9 +1423,9 @@ Qed. Definition notint (v: aval) := match v with | I i => I (Int.not i) - | Uns n => sgn (n + 1) - | Sgn n => Sgn n - | _ => itop + | Uns p n => sgn p (n + 1) + | Sgn p n => Sgn p n + | _ => ntop1 v end. Lemma notint_sound: @@ -1403,20 +1441,20 @@ Qed. Definition ror (x y: aval) := match y, x with - | I j, I i => if Int.ltu j Int.iwordsize then I(Int.ror i j) else itop - | _, _ => itop + | I j, I i => if Int.ltu j Int.iwordsize then I(Int.ror i j) else ntop + | _, _ => ntop1 x end. Lemma ror_sound: forall v w x y, vmatch v x -> vmatch w y -> vmatch (Val.ror v w) (ror x y). Proof. intros. - assert (DEFAULT: vmatch (Val.ror v w) itop). + assert (DEFAULT: forall p, vmatch (Val.ror v w) (Ifptr p)). { destruct v; destruct w; simpl; try constructor. destruct (Int.ltu i0 Int.iwordsize); constructor. } - unfold ror; destruct y; auto. inv H0. unfold Val.ror. + unfold ror; destruct y; try apply DEFAULT; auto. inv H0. unfold Val.ror. destruct (Int.ltu n Int.iwordsize) eqn:LTU. inv H; auto with va. inv H; auto with va. @@ -1425,7 +1463,7 @@ Qed. Definition rolm (x: aval) (amount mask: int) := match x with | I i => I (Int.rolm i amount mask) - | _ => uns (usize mask) + | _ => uns (provenance x) (usize mask) end. Lemma rolm_sound: @@ -1433,13 +1471,14 @@ Lemma rolm_sound: vmatch v x -> vmatch (Val.rolm v amount mask) (rolm x amount mask). Proof. intros. - assert (UNS: forall i, vmatch (Vint (Int.rolm i amount mask)) (uns (usize mask))). + assert (UNS_r: forall i j n, is_uns n j -> is_uns n (Int.and i j)). { - intros. - change (vmatch (Val.and (Vint (Int.rol i amount)) (Vint mask)) - (and itop (I mask))). - apply and_sound; auto with va. + intros; red; intros. rewrite Int.bits_and by auto. rewrite (H0 m) by auto. + apply andb_false_r. } + assert (UNS: forall i, vmatch (Vint (Int.rolm i amount mask)) + (uns (provenance x) (usize mask))). + { intros. unfold Int.rolm. apply vmatch_uns. apply UNS_r. auto with va. } unfold Val.rolm, rolm. inv H; auto with va. Qed. @@ -1459,7 +1498,7 @@ Definition add (x y: aval) := | Ifptr p, I i | I i, Ifptr p => Ifptr (padd p i) | Ifptr p, Ifptr q => Ifptr (plub (poffset p) (poffset q)) | Ifptr p, _ | _, Ifptr p => Ifptr (poffset p) - | _, _ => Vtop + | _, _ => ntop2 x y end. Lemma add_sound: @@ -1481,19 +1520,16 @@ Definition sub (v w: aval) := *) | Ptr p, _ => Ifptr (poffset p) | Ifptr p, I i => Ifptr (psub p i) - | Ifptr p, (Uns _ | Sgn _) => Ifptr (poffset p) - | Ifptr p1, Ptr p2 => itop - | _, _ => Vtop + | Ifptr p, _ => Ifptr (plub (poffset p) (provenance w)) + | _, _ => ntop2 v w end. Lemma sub_sound: forall v w x y, vmatch v x -> vmatch w y -> vmatch (Val.sub v w) (sub x y). Proof. - intros. inv H; inv H0; simpl; + intros. inv H; subst; inv H0; subst; simpl; try (destruct (eq_block b b0)); - try (constructor; (apply psub_sound || eapply poffset_sound); eauto). - change Vtop with (Ifptr (poffset Ptop)). - constructor; eapply poffset_sound. eapply pmatch_top'; eauto. + eauto using psub_sound, poffset_sound, pmatch_lub_l with va. Qed. Definition mul := binop_int Int.mul. @@ -1519,9 +1555,9 @@ Definition divs (v w: aval) := | I i2, I i1 => if Int.eq i2 Int.zero || Int.eq i1 (Int.repr Int.min_signed) && Int.eq i2 Int.mone - then if va_strict tt then Vbot else itop + then if va_strict tt then Vbot else ntop else I (Int.divs i1 i2) - | _, _ => itop + | _, _ => ntop2 v w end. Lemma divs_sound: @@ -1537,9 +1573,9 @@ Definition divu (v w: aval) := match w, v with | I i2, I i1 => if Int.eq i2 Int.zero - then if va_strict tt then Vbot else itop + then if va_strict tt then Vbot else ntop else I (Int.divu i1 i2) - | _, _ => itop + | _, _ => ntop2 v w end. Lemma divu_sound: @@ -1555,9 +1591,9 @@ Definition mods (v w: aval) := | I i2, I i1 => if Int.eq i2 Int.zero || Int.eq i1 (Int.repr Int.min_signed) && Int.eq i2 Int.mone - then if va_strict tt then Vbot else itop + then if va_strict tt then Vbot else ntop else I (Int.mods i1 i2) - | _, _ => itop + | _, _ => ntop2 v w end. Lemma mods_sound: @@ -1573,10 +1609,10 @@ Definition modu (v w: aval) := match w, v with | I i2, I i1 => if Int.eq i2 Int.zero - then if va_strict tt then Vbot else itop + then if va_strict tt then Vbot else ntop else I (Int.modu i1 i2) - | I i2, _ => uns (usize i2) - | _, _ => itop + | I i2, _ => uns (provenance v) (usize i2) + | _, _ => ntop2 v w end. Lemma modu_sound: @@ -1600,8 +1636,8 @@ Qed. Definition shrx (v w: aval) := match v, w with - | I i, I j => if Int.ltu j (Int.repr 31) then I(Int.shrx i j) else itop - | _, _ => itop + | I i, I j => if Int.ltu j (Int.repr 31) then I(Int.shrx i j) else ntop + | _, _ => ntop1 v end. Lemma shrx_sound: @@ -1693,8 +1729,8 @@ Proof (binop_single_sound Float32.div). Definition zero_ext (nbits: Z) (v: aval) := match v with | I i => I (Int.zero_ext nbits i) - | Uns n => uns (Z.min n nbits) - | _ => uns nbits + | Uns p n => uns p (Z.min n nbits) + | _ => uns (provenance v) nbits end. Lemma zero_ext_sound: @@ -1713,15 +1749,15 @@ Qed. Definition sign_ext (nbits: Z) (v: aval) := match v with | I i => I (Int.sign_ext nbits i) - | Uns n => if zlt n nbits then Uns n else sgn nbits - | Sgn n => sgn (Z.min n nbits) - | _ => sgn nbits + | Uns p n => if zlt n nbits then Uns p n else sgn p nbits + | Sgn p n => sgn p (Z.min n nbits) + | _ => sgn (provenance v) nbits end. Lemma sign_ext_sound: forall nbits v x, 0 < nbits -> vmatch v x -> vmatch (Val.sign_ext nbits v) (sign_ext nbits x). Proof. - assert (DFL: forall nbits i, 0 < nbits -> vmatch (Vint (Int.sign_ext nbits i)) (sgn nbits)). + assert (DFL: forall p nbits i, 0 < nbits -> vmatch (Vint (Int.sign_ext nbits i)) (sgn p nbits)). { intros. apply vmatch_sgn. apply is_sign_ext_sgn; auto with va. } @@ -1736,14 +1772,14 @@ Qed. Definition singleoffloat (v: aval) := match v with | F f => FS (Float.to_single f) - | _ => ftop + | _ => ntop1 v end. Lemma singleoffloat_sound: forall v x, vmatch v x -> vmatch (Val.singleoffloat v) (singleoffloat x). Proof. intros. - assert (DEFAULT: vmatch (Val.singleoffloat v) ftop). + assert (DEFAULT: vmatch (Val.singleoffloat v) (ntop1 x)). { destruct v; constructor. } destruct x; auto. inv H. constructor. Qed. @@ -1751,14 +1787,14 @@ Qed. Definition floatofsingle (v: aval) := match v with | FS f => F (Float.of_single f) - | _ => ftop + | _ => ntop1 v end. Lemma floatofsingle_sound: forall v x, vmatch v x -> vmatch (Val.floatofsingle v) (floatofsingle x). Proof. intros. - assert (DEFAULT: vmatch (Val.floatofsingle v) ftop). + assert (DEFAULT: vmatch (Val.floatofsingle v) (ntop1 x)). { destruct v; constructor. } destruct x; auto. inv H. constructor. Qed. @@ -1768,9 +1804,9 @@ Definition intoffloat (x: aval) := | F f => match Float.to_int f with | Some i => I i - | None => if va_strict tt then Vbot else itop + | None => if va_strict tt then Vbot else ntop end - | _ => itop + | _ => ntop1 x end. Lemma intoffloat_sound: @@ -1786,9 +1822,9 @@ Definition intuoffloat (x: aval) := | F f => match Float.to_intu f with | Some i => I i - | None => if va_strict tt then Vbot else itop + | None => if va_strict tt then Vbot else ntop end - | _ => itop + | _ => ntop1 x end. Lemma intuoffloat_sound: @@ -1802,7 +1838,7 @@ Qed. Definition floatofint (x: aval) := match x with | I i => F(Float.of_int i) - | _ => ftop + | _ => ntop1 x end. Lemma floatofint_sound: @@ -1815,7 +1851,7 @@ Qed. Definition floatofintu (x: aval) := match x with | I i => F(Float.of_intu i) - | _ => ftop + | _ => ntop1 x end. Lemma floatofintu_sound: @@ -1830,9 +1866,9 @@ Definition intofsingle (x: aval) := | FS f => match Float32.to_int f with | Some i => I i - | None => if va_strict tt then Vbot else itop + | None => if va_strict tt then Vbot else ntop end - | _ => itop + | _ => ntop1 x end. Lemma intofsingle_sound: @@ -1848,9 +1884,9 @@ Definition intuofsingle (x: aval) := | FS f => match Float32.to_intu f with | Some i => I i - | None => if va_strict tt then Vbot else itop + | None => if va_strict tt then Vbot else ntop end - | _ => itop + | _ => ntop1 x end. Lemma intuofsingle_sound: @@ -1864,7 +1900,7 @@ Qed. Definition singleofint (x: aval) := match x with | I i => FS(Float32.of_int i) - | _ => ftop + | _ => ntop1 x end. Lemma singleofint_sound: @@ -1877,7 +1913,7 @@ Qed. Definition singleofintu (x: aval) := match x with | I i => FS(Float32.of_intu i) - | _ => ftop + | _ => ntop1 x end. Lemma singleofintu_sound: @@ -1890,31 +1926,31 @@ Qed. Definition floatofwords (x y: aval) := match x, y with | I i, I j => F(Float.from_words i j) - | _, _ => ftop + | _, _ => ntop2 x y end. Lemma floatofwords_sound: forall v w x y, vmatch v x -> vmatch w y -> vmatch (Val.floatofwords v w) (floatofwords x y). Proof. - intros. unfold floatofwords, ftop; inv H; simpl; auto with va; inv H0; auto with va. + intros. unfold floatofwords; inv H; simpl; auto with va; inv H0; auto with va. Qed. Definition longofwords (x y: aval) := - match x, y with - | I i, I j => L(Int64.ofwords i j) - | _, _ => ltop + match y, x with + | I j, I i => L(Int64.ofwords i j) + | _, _ => ntop2 x y end. Lemma longofwords_sound: forall v w x y, vmatch v x -> vmatch w y -> vmatch (Val.longofwords v w) (longofwords x y). Proof. - intros. unfold longofwords, ltop; inv H; simpl; auto with va; inv H0; auto with va. + intros. unfold longofwords; inv H0; inv H; simpl; auto with va. Qed. Definition loword (x: aval) := match x with | L i => I(Int64.loword i) - | _ => itop + | _ => ntop1 x end. Lemma loword_sound: forall v x, vmatch v x -> vmatch (Val.loword v) (loword x). @@ -1925,7 +1961,7 @@ Qed. Definition hiword (x: aval) := match x with | L i => I(Int64.hiword i) - | _ => itop + | _ => ntop1 x end. Lemma hiword_sound: forall v x, vmatch v x -> vmatch (Val.hiword v) (hiword x). @@ -2009,7 +2045,7 @@ Qed. Definition uintv (v: aval) : Z * Z := match v with | I n => (Int.unsigned n, Int.unsigned n) - | Uns n => if zlt n Int.zwordsize then (0, two_p n - 1) else (0, Int.max_unsigned) + | Uns _ n => if zlt n Int.zwordsize then (0, two_p n - 1) else (0, Int.max_unsigned) | _ => (0, Int.max_unsigned) end. @@ -2047,9 +2083,9 @@ Qed. Definition sintv (v: aval) : Z * Z := match v with | I n => (Int.signed n, Int.signed n) - | Uns n => + | Uns _ n => if zlt n Int.zwordsize then (0, two_p n - 1) else (Int.min_signed, Int.max_signed) - | Sgn n => + | Sgn _ n => if zlt n Int.zwordsize then (let x := two_p (n-1) in (-x, x-1)) else (Int.min_signed, Int.max_signed) @@ -2104,11 +2140,11 @@ Qed. Definition cmpu_bool (c: comparison) (v w: aval) : abool := match v, w with | I i1, I i2 => Just (Int.cmpu c i1 i2) - | Ptr _, (I _ | Uns _ | Sgn _) => cmp_different_blocks c - | (I _ | Uns _ | Sgn _), Ptr _ => cmp_different_blocks c + | Ptr _, I _ => cmp_different_blocks c + | I _, Ptr _ => cmp_different_blocks c | Ptr p1, Ptr p2 => pcmp c p1 p2 - | Ptr p1, Ifptr p2 => club (pcmp c p1 p2) (cmp_different_blocks c) - | Ifptr p1, Ptr p2 => club (pcmp c p1 p2) (cmp_different_blocks c) + | Ptr p1, (Ifptr p2 | Uns p2 _ | Sgn p2 _) => club (pcmp c p1 p2) (cmp_different_blocks c) + | (Ifptr p1 | Uns p1 _ | Sgn p1 _), Ptr p2 => club (pcmp c p1 p2) (cmp_different_blocks c) | _, I i => club (cmp_intv c (uintv v) (Int.unsigned i)) (cmp_different_blocks c) | I i, _ => club (cmp_intv (swap_comparison c) (uintv w) (Int.unsigned i)) (cmp_different_blocks c) | _, _ => Btop @@ -2181,7 +2217,7 @@ Qed. Definition maskzero (x: aval) (mask: int) : abool := match x with | I i => Just (Int.eq (Int.and i mask) Int.zero) - | Uns n => if Int.eq (Int.zero_ext n mask) Int.zero then Maybe true else Btop + | Uns p n => if Int.eq (Int.zero_ext n mask) Int.zero then Maybe true else Btop | _ => Btop end. @@ -2203,14 +2239,14 @@ Qed. Definition of_optbool (ab: abool) : aval := match ab with | Just b => I (if b then Int.one else Int.zero) - | _ => Uns 1 + | _ => Uns Pbot 1 end. Lemma of_optbool_sound: forall ob ab, cmatch ob ab -> vmatch (Val.of_optbool ob) (of_optbool ab). Proof. intros. - assert (DEFAULT: vmatch (Val.of_optbool ob) (Uns 1)). + assert (DEFAULT: vmatch (Val.of_optbool ob) (Uns Pbot 1)). { destruct ob; simpl; auto with va. destruct b; constructor; try omega. @@ -2240,26 +2276,27 @@ Definition vnormalize (chunk: memory_chunk) (v: aval) := match chunk, v with | _, Vbot => Vbot | Mint8signed, I i => I (Int.sign_ext 8 i) - | Mint8signed, Uns n => if zlt n 8 then Uns n else Sgn 8 - | Mint8signed, Sgn n => Sgn (Z.min n 8) - | Mint8signed, _ => Sgn 8 + | Mint8signed, Uns p n => if zlt n 8 then Uns (provenance v) n else Sgn (provenance v) 8 + | Mint8signed, Sgn p n => Sgn (provenance v) (Z.min n 8) + | Mint8signed, _ => Sgn (provenance v) 8 | Mint8unsigned, I i => I (Int.zero_ext 8 i) - | Mint8unsigned, Uns n => Uns (Z.min n 8) - | Mint8unsigned, _ => Uns 8 + | Mint8unsigned, Uns p n => Uns (provenance v) (Z.min n 8) + | Mint8unsigned, _ => Uns (provenance v) 8 | Mint16signed, I i => I (Int.sign_ext 16 i) - | Mint16signed, Uns n => if zlt n 16 then Uns n else Sgn 16 - | Mint16signed, Sgn n => Sgn (Z.min n 16) - | Mint16signed, _ => Sgn 16 + | Mint16signed, Uns p n => if zlt n 16 then Uns (provenance v) n else Sgn (provenance v) 16 + | Mint16signed, Sgn p n => Sgn (provenance v) (Z.min n 16) + | Mint16signed, _ => Sgn (provenance v) 16 | Mint16unsigned, I i => I (Int.zero_ext 16 i) - | Mint16unsigned, Uns n => Uns (Z.min n 16) - | Mint16unsigned, _ => Uns 16 - | Mint32, (I _ | Ptr _ | Ifptr _) => v + | Mint16unsigned, Uns p n => Uns (provenance v) (Z.min n 16) + | Mint16unsigned, _ => Uns (provenance v) 16 + | Mint32, (I _ | Uns _ _ | Sgn _ _ | Ptr _ | Ifptr _) => v | Mint64, L _ => v + | Mint64, (Ptr p | Ifptr p | Uns p _ | Sgn p _) => Ifptr (if va_strict tt then Pbot else p) | Mfloat32, FS f => v | Mfloat64, F f => v - | Many32, (I _ | Ptr _ | Ifptr _ | FS _) => v + | Many32, (I _ | Uns _ _ | Sgn _ _ | Ptr _ | Ifptr _ | FS _) => v | Many64, _ => v - | _, _ => Ifptr Pbot + | _, _ => Ifptr (provenance v) end. Lemma vnormalize_sound: @@ -2316,39 +2353,66 @@ Proof. auto. Qed. +Remark poffset_monotone: + forall p q, pge p q -> pge (poffset p) (poffset q). +Proof. + destruct 1; simpl; auto with va. +Qed. + +Remark provenance_monotone: + forall x y, vge x y -> pge (provenance x) (provenance y). +Proof. + unfold provenance; intros. destruct (va_strict tt). constructor. + inv H; auto using poffset_monotone with va. +Qed. + Lemma vnormalize_monotone: forall chunk x y, vge x y -> vge (vnormalize chunk x) (vnormalize chunk y). -Proof. - induction 1; destruct chunk; simpl; auto with va. -- destruct (zlt n 8); constructor; auto with va. - apply is_sign_ext_uns; auto with va. - apply is_sign_ext_sgn; auto with va. -- constructor; auto with va. apply is_zero_ext_uns; auto with va. - apply Z.min_case; auto with va. -- destruct (zlt n 16); constructor; auto with va. - apply is_sign_ext_uns; auto with va. - apply is_sign_ext_sgn; auto with va. -- constructor; auto with va. apply is_zero_ext_uns; auto with va. - apply Z.min_case; auto with va. -- destruct (zlt n1 8). rewrite zlt_true by omega. auto with va. - destruct (zlt n2 8); auto with va. -- destruct (zlt n1 16). rewrite zlt_true by omega. auto with va. - destruct (zlt n2 16); auto with va. -- constructor; auto with va. apply is_sign_ext_sgn; auto with va. - apply Z.min_case; auto with va. -- constructor; auto with va. apply is_zero_ext_uns; auto with va. -- constructor; auto with va. apply is_sign_ext_sgn; auto with va. - apply Z.min_case; auto with va. -- constructor; auto with va. apply is_zero_ext_uns; auto with va. -- destruct (zlt n2 8); constructor; auto with va. -- destruct (zlt n2 16); constructor; auto with va. -- constructor; auto with va. apply is_sign_ext_sgn; auto with va. -- constructor; auto with va. apply is_zero_ext_uns; auto with va. -- constructor; auto with va. apply is_sign_ext_sgn; auto with va. -- constructor; auto with va. apply is_zero_ext_uns; auto with va. -- destruct (zlt n 8); constructor; auto with va. -- destruct (zlt n 16); constructor; auto with va. +Proof with (auto using provenance_monotone with va). + intros chunk x y V; inversion V; subst; destruct chunk; simpl... +- destruct (zlt n 8); constructor... + apply is_sign_ext_uns... + apply is_sign_ext_sgn... +- constructor... apply is_zero_ext_uns... apply Z.min_case... +- destruct (zlt n 16); constructor... + apply is_sign_ext_uns... + apply is_sign_ext_sgn... +- constructor... apply is_zero_ext_uns... apply Z.min_case... +- unfold provenance; destruct (va_strict tt)... +- destruct (zlt n1 8). rewrite zlt_true by omega... + destruct (zlt n2 8)... +- destruct (zlt n1 16). rewrite zlt_true by omega... + destruct (zlt n2 16)... +- destruct (va_strict tt)... +- constructor... apply is_sign_ext_sgn... apply Z.min_case... +- constructor... apply is_zero_ext_uns... +- constructor... apply is_sign_ext_sgn... apply Z.min_case... +- constructor... apply is_zero_ext_uns... +- unfold provenance; destruct (va_strict tt)... +- destruct (va_strict tt)... +- destruct (zlt n2 8); constructor... +- destruct (zlt n2 16); constructor... +- destruct (va_strict tt)... +- destruct (va_strict tt)... +- destruct (va_strict tt)... +- destruct (va_strict tt)... +- constructor... apply is_sign_ext_sgn... +- constructor... apply is_zero_ext_uns... +- constructor... apply is_sign_ext_sgn... +- constructor... apply is_zero_ext_uns... +- unfold provenance; destruct (va_strict tt)... +- unfold provenance; destruct (va_strict tt)... +- unfold provenance; destruct (va_strict tt)... +- unfold provenance; destruct (va_strict tt)... +- unfold provenance; destruct (va_strict tt)... +- unfold provenance; destruct (va_strict tt)... +- unfold provenance; destruct (va_strict tt)... +- unfold provenance; destruct (va_strict tt)... +- destruct (zlt n 8)... +- destruct (zlt n 16)... +- destruct (va_strict tt)... +- destruct (va_strict tt)... Qed. (** Abstracting memory blocks *) @@ -4011,7 +4075,7 @@ End VA. Hint Constructors cmatch : va. Hint Constructors pmatch: va. -Hint Constructors vmatch : va. +Hint Constructors vmatch: va. Hint Resolve cnot_sound symbol_address_sound shl_sound shru_sound shr_sound and_sound or_sound xor_sound notint_sound |