diff options
| -rw-r--r-- | arm/ConstpropOp.vp | 14 | ||||
| -rw-r--r-- | arm/ConstpropOpproof.v | 28 | ||||
| -rw-r--r-- | arm/ValueAOp.v | 4 | ||||
| -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 | ||||
| -rw-r--r-- | cparser/Rename.ml | 1 | ||||
| -rw-r--r-- | debug/DwarfPrinter.ml | 4 | ||||
| -rw-r--r-- | driver/Driver.ml | 4 | ||||
| -rw-r--r-- | exportclight/ExportClight.ml | 10 | ||||
| -rw-r--r-- | ia32/ConstpropOp.vp | 18 | ||||
| -rw-r--r-- | ia32/ConstpropOpproof.v | 40 | ||||
| -rw-r--r-- | ia32/ValueAOp.v | 6 | ||||
| -rw-r--r-- | powerpc/Asm.v | 12 | ||||
| -rw-r--r-- | powerpc/AsmToJSON.ml | 9 | ||||
| -rw-r--r-- | powerpc/Asmexpand.ml | 6 | ||||
| -rw-r--r-- | powerpc/CBuiltins.ml | 9 | ||||
| -rw-r--r-- | powerpc/ConstpropOp.vp | 14 | ||||
| -rw-r--r-- | powerpc/ConstpropOpproof.v | 28 | ||||
| -rw-r--r-- | powerpc/TargetPrinter.ml | 6 | ||||
| -rw-r--r-- | powerpc/ValueAOp.v | 4 | ||||
| -rw-r--r-- | test/regression/Makefile | 2 | ||||
| -rw-r--r-- | test/regression/Results/alias | 8 | ||||
| -rw-r--r-- | test/regression/alias.c | 168 |
25 files changed, 667 insertions, 394 deletions
diff --git a/arm/ConstpropOp.vp b/arm/ConstpropOp.vp index 4f4bf5aa..872493a6 100644 --- a/arm/ConstpropOp.vp +++ b/arm/ConstpropOp.vp @@ -96,12 +96,12 @@ Definition make_cmp_base (c: condition) (args: list reg) (vl: list aval) := Nondetfunction make_cmp (c: condition) (args: list reg) (vl: list aval) := match c, args, vl with | Ccompimm Ceq n, r1 :: nil, v1 :: nil => - if Int.eq_dec n Int.one && vincl v1 (Uns 1) then (Omove, r1 :: nil) - else if Int.eq_dec n Int.zero && vincl v1 (Uns 1) then (Oxorimm Int.one, r1 :: nil) + if Int.eq_dec n Int.one && vincl v1 (Uns Ptop 1) then (Omove, r1 :: nil) + else if Int.eq_dec n Int.zero && vincl v1 (Uns Ptop 1) then (Oxorimm Int.one, r1 :: nil) else make_cmp_base c args vl | Ccompimm Cne n, r1 :: nil, v1 :: nil => - if Int.eq_dec n Int.zero && vincl v1 (Uns 1) then (Omove, r1 :: nil) - else if Int.eq_dec n Int.one && vincl v1 (Uns 1) then (Oxorimm Int.one, r1 :: nil) + if Int.eq_dec n Int.zero && vincl v1 (Uns Ptop 1) then (Omove, r1 :: nil) + else if Int.eq_dec n Int.one && vincl v1 (Uns Ptop 1) then (Oxorimm Int.one, r1 :: nil) else make_cmp_base c args vl | _, _, _ => make_cmp_base c args vl @@ -164,7 +164,7 @@ Definition make_divuimm (n: int) (r1 r2: reg) := Definition make_andimm (n: int) (r: reg) (a: aval) := if Int.eq n Int.zero then (Ointconst Int.zero, nil) else if Int.eq n Int.mone then (Omove, r :: nil) - else if match a with Uns m => Int.eq (Int.zero_ext m (Int.not n)) Int.zero + else if match a with Uns _ m => Int.eq (Int.zero_ext m (Int.not n)) Int.zero | _ => false end then (Omove, r :: nil) else (Oandimm n, r :: nil). @@ -190,9 +190,9 @@ Definition make_mulfsimm (n: float32) (r r1 r2: reg) := else (Omulfs, r1 :: r2 :: nil). Definition make_cast8signed (r: reg) (a: aval) := - if vincl a (Sgn 8) then (Omove, r :: nil) else (Ocast8signed, r :: nil). + if vincl a (Sgn Ptop 8) then (Omove, r :: nil) else (Ocast8signed, r :: nil). Definition make_cast16signed (r: reg) (a: aval) := - if vincl a (Sgn 16) then (Omove, r :: nil) else (Ocast16signed, r :: nil). + if vincl a (Sgn Ptop 16) then (Omove, r :: nil) else (Ocast16signed, r :: nil). Nondetfunction op_strength_reduction (op: operation) (args: list reg) (vl: list aval) := diff --git a/arm/ConstpropOpproof.v b/arm/ConstpropOpproof.v index 597c9602..fa20d17e 100644 --- a/arm/ConstpropOpproof.v +++ b/arm/ConstpropOpproof.v @@ -163,24 +163,24 @@ Lemma make_cmp_correct: /\ Val.lessdef (Val.of_optbool (eval_condition c rs##args m)) v. Proof. intros c args vl. - assert (Y: forall r, vincl (AE.get r ae) (Uns 1) = true -> + assert (Y: forall r, vincl (AE.get r ae) (Uns Ptop 1) = true -> rs#r = Vundef \/ rs#r = Vint Int.zero \/ rs#r = Vint Int.one). - { intros. apply vmatch_Uns_1 with bc. eapply vmatch_ge. eapply vincl_ge; eauto. apply MATCH. } + { intros. apply vmatch_Uns_1 with bc Ptop. eapply vmatch_ge. eapply vincl_ge; eauto. apply MATCH. } unfold make_cmp. case (make_cmp_match c args vl); intros. -- destruct (Int.eq_dec n Int.one && vincl v1 (Uns 1)) eqn:E1. +- destruct (Int.eq_dec n Int.one && vincl v1 (Uns Ptop 1)) eqn:E1. simpl in H; inv H. InvBooleans. subst n. exists (rs#r1); split; auto. simpl. exploit Y; eauto. intros [A | [A | A]]; rewrite A; simpl; auto. - destruct (Int.eq_dec n Int.zero && vincl v1 (Uns 1)) eqn:E0. + destruct (Int.eq_dec n Int.zero && vincl v1 (Uns Ptop 1)) eqn:E0. simpl in H; inv H. InvBooleans. subst n. exists (Val.xor rs#r1 (Vint Int.one)); split; auto. simpl. exploit Y; eauto. intros [A | [A | A]]; rewrite A; simpl; auto. apply make_cmp_base_correct; auto. -- destruct (Int.eq_dec n Int.zero && vincl v1 (Uns 1)) eqn:E0. +- destruct (Int.eq_dec n Int.zero && vincl v1 (Uns Ptop 1)) eqn:E0. simpl in H; inv H. InvBooleans. subst n. exists (rs#r1); split; auto. simpl. exploit Y; eauto. intros [A | [A | A]]; rewrite A; simpl; auto. - destruct (Int.eq_dec n Int.one && vincl v1 (Uns 1)) eqn:E1. + destruct (Int.eq_dec n Int.one && vincl v1 (Uns Ptop 1)) eqn:E1. simpl in H; inv H. InvBooleans. subst n. exists (Val.xor rs#r1 (Vint Int.one)); split; auto. simpl. exploit Y; eauto. intros [A | [A | A]]; rewrite A; simpl; auto. @@ -302,7 +302,7 @@ Proof. subst n. exists (Vint Int.zero); split; auto. destruct (rs#r); simpl; auto. rewrite Int.and_zero; auto. predSpec Int.eq Int.eq_spec n Int.mone; intros. subst n. exists (rs#r); split; auto. destruct (rs#r); simpl; auto. rewrite Int.and_mone; auto. - destruct (match x with Uns k => Int.eq (Int.zero_ext k (Int.not n)) Int.zero + destruct (match x with Uns _ k => Int.eq (Int.zero_ext k (Int.not n)) Int.zero | _ => false end) eqn:UNS. destruct x; try congruence. exists (rs#r); split; auto. @@ -313,7 +313,7 @@ Proof. rewrite Int.bits_zero. simpl. rewrite andb_true_r. auto. rewrite <- EQ. rewrite Int.bits_zero_ext by omega. rewrite zlt_true by auto. rewrite Int.bits_not by auto. apply negb_involutive. - rewrite H5 by auto. auto. + rewrite H6 by auto. auto. econstructor; split; eauto. auto. Qed. @@ -404,11 +404,11 @@ Lemma make_cast8signed_correct: let (op, args) := make_cast8signed r x in exists v, eval_operation ge (Vptr sp Int.zero) op rs##args m = Some v /\ Val.lessdef (Val.sign_ext 8 rs#r) v. Proof. - intros; unfold make_cast8signed. destruct (vincl x (Sgn 8)) eqn:INCL. + intros; unfold make_cast8signed. destruct (vincl x (Sgn Ptop 8)) eqn:INCL. exists rs#r; split; auto. - assert (V: vmatch bc rs#r (Sgn 8)). + assert (V: vmatch bc rs#r (Sgn Ptop 8)). { eapply vmatch_ge; eauto. apply vincl_ge; auto. } - inv V; simpl; auto. rewrite is_sgn_sign_ext in H3 by auto. rewrite H3; auto. + inv V; simpl; auto. rewrite is_sgn_sign_ext in H4 by auto. rewrite H4; auto. econstructor; split; simpl; eauto. Qed. @@ -418,11 +418,11 @@ Lemma make_cast16signed_correct: let (op, args) := make_cast16signed r x in exists v, eval_operation ge (Vptr sp Int.zero) op rs##args m = Some v /\ Val.lessdef (Val.sign_ext 16 rs#r) v. Proof. - intros; unfold make_cast16signed. destruct (vincl x (Sgn 16)) eqn:INCL. + intros; unfold make_cast16signed. destruct (vincl x (Sgn Ptop 16)) eqn:INCL. exists rs#r; split; auto. - assert (V: vmatch bc rs#r (Sgn 16)). + assert (V: vmatch bc rs#r (Sgn Ptop 16)). { eapply vmatch_ge; eauto. apply vincl_ge; auto. } - inv V; simpl; auto. rewrite is_sgn_sign_ext in H3 by auto. rewrite H3; auto. + inv V; simpl; auto. rewrite is_sgn_sign_ext in H4 by auto. rewrite H4; auto. econstructor; split; simpl; eauto. Qed. diff --git a/arm/ValueAOp.v b/arm/ValueAOp.v index a14d6b98..b388bf12 100644 --- a/arm/ValueAOp.v +++ b/arm/ValueAOp.v @@ -64,8 +64,8 @@ Definition eval_static_operation (op: operation) (vl: list aval): aval := match op, vl with | Omove, v1::nil => v1 | Ointconst n, nil => I n - | Ofloatconst n, nil => if propagate_float_constants tt then F n else ftop - | Osingleconst n, nil => if propagate_float_constants tt then FS n else ftop + | Ofloatconst n, nil => if propagate_float_constants tt then F n else ntop + | Osingleconst n, nil => if propagate_float_constants tt then FS n else ntop | Oaddrsymbol id ofs, nil => Ptr (Gl id ofs) | Oaddrstack ofs, nil => Ptr (Stk ofs) | Ocast8signed, v1 :: nil => sign_ext 8 v1 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 diff --git a/cparser/Rename.ml b/cparser/Rename.ml index cf82bc9f..b0dc120f 100644 --- a/cparser/Rename.ml +++ b/cparser/Rename.ml @@ -48,6 +48,7 @@ let enter_static env id file = let id' = StringMap.find id.name env.re_public in { env with re_id = IdentMap.add id id' env.re_id } with Not_found -> + let file = String.map (fun a -> match a with 'a'..'z' | 'A'..'Z' | '0'..'9' -> a | _ -> '_') file in let id' = {id with name = Printf.sprintf "_%s_%s" file id.name} in { re_id = IdentMap.add id id' env.re_id; re_public = env.re_public; diff --git a/debug/DwarfPrinter.ml b/debug/DwarfPrinter.ml index 9e565ee4..67245ca8 100644 --- a/debug/DwarfPrinter.ml +++ b/debug/DwarfPrinter.ml @@ -393,8 +393,8 @@ module DwarfPrinter(Target: DWARF_TARGET)(DwarfAbbrevs:DWARF_ABBREVS): print_opt_value oc st.structure_name print_string let print_subprogram_addr oc (s,e) = - fprintf oc " .4byte %a\n" label s; - fprintf oc " .4byte %a\n" label e + fprintf oc " .4byte %a\n" label e; + fprintf oc " .4byte %a\n" label s let print_subprogram oc sp = let addr = get_fun_addr sp.subprogram_name in diff --git a/driver/Driver.ml b/driver/Driver.ml index 1dce08ac..2932e879 100644 --- a/driver/Driver.ml +++ b/driver/Driver.ml @@ -159,8 +159,8 @@ let jdump_magic_number = "CompCertJDUMP" ^ Version.version let dump_jasm asm destfile = let oc = open_out_bin destfile in - fprintf oc "{\n\"Version\":\"%s\",\n\"Asm Ast\":%a}" - jdump_magic_number AsmToJSON.p_program asm; + fprintf oc "{\n\"Version\":\"%s\",\n\"System\":\"%s\",\n\"Asm Ast\":%a}" + jdump_magic_number Configuration.system AsmToJSON.p_program asm; close_out oc diff --git a/exportclight/ExportClight.ml b/exportclight/ExportClight.ml index 397d04b1..9563d551 100644 --- a/exportclight/ExportClight.ml +++ b/exportclight/ExportClight.ml @@ -135,6 +135,11 @@ let coqsingle p n = let coqN p n = fprintf p "%ld%%N" (N.to_int32 n) +(* Coq strings *) + +let coqstring p s = + fprintf p "\"%s\"" (camlstring_of_coqstring s) + (* Raw attributes *) let attribute p a = @@ -201,7 +206,8 @@ and typlist p = function and callconv p cc = if cc = cc_default then fprintf p "cc_default" - else fprintf p "{|cc_vararg:=%b; cc_structret:=%b|}" cc.cc_vararg cc.cc_structret + else fprintf p "{|cc_vararg:=%b; cc_unproto:=%b; cc_structret:=%b|}" + cc.cc_vararg cc.cc_unproto cc.cc_structret (* External functions *) @@ -262,7 +268,7 @@ let external_function p = function fprintf p "@[<hov 2>(EF_inline_asm %ld%%positive@ %a@ %a)@]" (P.to_int32 text) signatur sg - (print_list ident) clob + (print_list coqstring) clob (* Expressions *) diff --git a/ia32/ConstpropOp.vp b/ia32/ConstpropOp.vp index 8c7f01fa..a3de748c 100644 --- a/ia32/ConstpropOp.vp +++ b/ia32/ConstpropOp.vp @@ -50,12 +50,12 @@ Definition make_cmp_base (c: condition) (args: list reg) (vl: list aval) := Nondetfunction make_cmp (c: condition) (args: list reg) (vl: list aval) := match c, args, vl with | Ccompimm Ceq n, r1 :: nil, v1 :: nil => - if Int.eq_dec n Int.one && vincl v1 (Uns 1) then (Omove, r1 :: nil) - else if Int.eq_dec n Int.zero && vincl v1 (Uns 1) then (Oxorimm Int.one, r1 :: nil) + if Int.eq_dec n Int.one && vincl v1 (Uns Ptop 1) then (Omove, r1 :: nil) + else if Int.eq_dec n Int.zero && vincl v1 (Uns Ptop 1) then (Oxorimm Int.one, r1 :: nil) else make_cmp_base c args vl | Ccompimm Cne n, r1 :: nil, v1 :: nil => - if Int.eq_dec n Int.zero && vincl v1 (Uns 1) then (Omove, r1 :: nil) - else if Int.eq_dec n Int.one && vincl v1 (Uns 1) then (Oxorimm Int.one, r1 :: nil) + if Int.eq_dec n Int.zero && vincl v1 (Uns Ptop 1) then (Omove, r1 :: nil) + else if Int.eq_dec n Int.one && vincl v1 (Uns Ptop 1) then (Oxorimm Int.one, r1 :: nil) else make_cmp_base c args vl | _, _, _ => make_cmp_base c args vl @@ -138,7 +138,7 @@ Definition make_mulimm (n: int) (r: reg) := Definition make_andimm (n: int) (r: reg) (a: aval) := if Int.eq n Int.zero then (Ointconst Int.zero, nil) else if Int.eq n Int.mone then (Omove, r :: nil) - else if match a with Uns m => Int.eq (Int.zero_ext m (Int.not n)) Int.zero + else if match a with Uns _ m => Int.eq (Int.zero_ext m (Int.not n)) Int.zero | _ => false end then (Omove, r :: nil) else (Oandimm n, r :: nil). @@ -184,13 +184,13 @@ Definition make_mulfsimm (n: float32) (r r1 r2: reg) := else (Omulfs, r1 :: r2 :: nil). Definition make_cast8signed (r: reg) (a: aval) := - if vincl a (Sgn 8) then (Omove, r :: nil) else (Ocast8signed, r :: nil). + if vincl a (Sgn Ptop 8) then (Omove, r :: nil) else (Ocast8signed, r :: nil). Definition make_cast8unsigned (r: reg) (a: aval) := - if vincl a (Uns 8) then (Omove, r :: nil) else (Ocast8unsigned, r :: nil). + if vincl a (Uns Ptop 8) then (Omove, r :: nil) else (Ocast8unsigned, r :: nil). Definition make_cast16signed (r: reg) (a: aval) := - if vincl a (Sgn 16) then (Omove, r :: nil) else (Ocast16signed, r :: nil). + if vincl a (Sgn Ptop 16) then (Omove, r :: nil) else (Ocast16signed, r :: nil). Definition make_cast16unsigned (r: reg) (a: aval) := - if vincl a (Uns 16) then (Omove, r :: nil) else (Ocast16unsigned, r :: nil). + if vincl a (Uns Ptop 16) then (Omove, r :: nil) else (Ocast16unsigned, r :: nil). Nondetfunction op_strength_reduction (op: operation) (args: list reg) (vl: list aval) := diff --git a/ia32/ConstpropOpproof.v b/ia32/ConstpropOpproof.v index 6adb26fe..47a6c536 100644 --- a/ia32/ConstpropOpproof.v +++ b/ia32/ConstpropOpproof.v @@ -178,24 +178,24 @@ Lemma make_cmp_correct: /\ Val.lessdef (Val.of_optbool (eval_condition c e##args m)) v. Proof. intros c args vl. - assert (Y: forall r, vincl (AE.get r ae) (Uns 1) = true -> + assert (Y: forall r, vincl (AE.get r ae) (Uns Ptop 1) = true -> e#r = Vundef \/ e#r = Vint Int.zero \/ e#r = Vint Int.one). - { intros. apply vmatch_Uns_1 with bc. eapply vmatch_ge. eapply vincl_ge; eauto. apply MATCH. } + { intros. apply vmatch_Uns_1 with bc Ptop. eapply vmatch_ge. eapply vincl_ge; eauto. apply MATCH. } unfold make_cmp. case (make_cmp_match c args vl); intros. -- destruct (Int.eq_dec n Int.one && vincl v1 (Uns 1)) eqn:E1. +- destruct (Int.eq_dec n Int.one && vincl v1 (Uns Ptop 1)) eqn:E1. simpl in H; inv H. InvBooleans. subst n. exists (e#r1); split; auto. simpl. exploit Y; eauto. intros [A | [A | A]]; rewrite A; simpl; auto. - destruct (Int.eq_dec n Int.zero && vincl v1 (Uns 1)) eqn:E0. + destruct (Int.eq_dec n Int.zero && vincl v1 (Uns Ptop 1)) eqn:E0. simpl in H; inv H. InvBooleans. subst n. exists (Val.xor e#r1 (Vint Int.one)); split; auto. simpl. exploit Y; eauto. intros [A | [A | A]]; rewrite A; simpl; auto. apply make_cmp_base_correct; auto. -- destruct (Int.eq_dec n Int.zero && vincl v1 (Uns 1)) eqn:E0. +- destruct (Int.eq_dec n Int.zero && vincl v1 (Uns Ptop 1)) eqn:E0. simpl in H; inv H. InvBooleans. subst n. exists (e#r1); split; auto. simpl. exploit Y; eauto. intros [A | [A | A]]; rewrite A; simpl; auto. - destruct (Int.eq_dec n Int.one && vincl v1 (Uns 1)) eqn:E1. + destruct (Int.eq_dec n Int.one && vincl v1 (Uns Ptop 1)) eqn:E1. simpl in H; inv H. InvBooleans. subst n. exists (Val.xor e#r1 (Vint Int.one)); split; auto. simpl. exploit Y; eauto. intros [A | [A | A]]; rewrite A; simpl; auto. @@ -324,7 +324,7 @@ Proof. subst n. exists (Vint Int.zero); split; auto. destruct (e#r); simpl; auto. rewrite Int.and_zero; auto. predSpec Int.eq Int.eq_spec n Int.mone; intros. subst n. exists (e#r); split; auto. destruct (e#r); simpl; auto. rewrite Int.and_mone; auto. - destruct (match x with Uns k => Int.eq (Int.zero_ext k (Int.not n)) Int.zero + destruct (match x with Uns _ k => Int.eq (Int.zero_ext k (Int.not n)) Int.zero | _ => false end) eqn:UNS. destruct x; try congruence. exists (e#r); split; auto. @@ -335,7 +335,7 @@ Proof. rewrite Int.bits_zero. simpl. rewrite andb_true_r. auto. rewrite <- EQ. rewrite Int.bits_zero_ext by omega. rewrite zlt_true by auto. rewrite Int.bits_not by auto. apply negb_involutive. - rewrite H5 by auto. auto. + rewrite H6 by auto. auto. econstructor; split; eauto. auto. Qed. @@ -425,11 +425,11 @@ Lemma make_cast8signed_correct: let (op, args) := make_cast8signed r x in exists v, eval_operation ge (Vptr sp Int.zero) op e##args m = Some v /\ Val.lessdef (Val.sign_ext 8 e#r) v. Proof. - intros; unfold make_cast8signed. destruct (vincl x (Sgn 8)) eqn:INCL. + intros; unfold make_cast8signed. destruct (vincl x (Sgn Ptop 8)) eqn:INCL. exists e#r; split; auto. - assert (V: vmatch bc e#r (Sgn 8)). + assert (V: vmatch bc e#r (Sgn Ptop 8)). { eapply vmatch_ge; eauto. apply vincl_ge; auto. } - inv V; simpl; auto. rewrite is_sgn_sign_ext in H3 by auto. rewrite H3; auto. + inv V; simpl; auto. rewrite is_sgn_sign_ext in H4 by auto. rewrite H4; auto. econstructor; split; simpl; eauto. Qed. @@ -439,11 +439,11 @@ Lemma make_cast8unsigned_correct: let (op, args) := make_cast8unsigned r x in exists v, eval_operation ge (Vptr sp Int.zero) op e##args m = Some v /\ Val.lessdef (Val.zero_ext 8 e#r) v. Proof. - intros; unfold make_cast8unsigned. destruct (vincl x (Uns 8)) eqn:INCL. + intros; unfold make_cast8unsigned. destruct (vincl x (Uns Ptop 8)) eqn:INCL. exists e#r; split; auto. - assert (V: vmatch bc e#r (Uns 8)). + assert (V: vmatch bc e#r (Uns Ptop 8)). { eapply vmatch_ge; eauto. apply vincl_ge; auto. } - inv V; simpl; auto. rewrite is_uns_zero_ext in H3 by auto. rewrite H3; auto. + inv V; simpl; auto. rewrite is_uns_zero_ext in H4 by auto. rewrite H4; auto. econstructor; split; simpl; eauto. Qed. @@ -453,11 +453,11 @@ Lemma make_cast16signed_correct: let (op, args) := make_cast16signed r x in exists v, eval_operation ge (Vptr sp Int.zero) op e##args m = Some v /\ Val.lessdef (Val.sign_ext 16 e#r) v. Proof. - intros; unfold make_cast16signed. destruct (vincl x (Sgn 16)) eqn:INCL. + intros; unfold make_cast16signed. destruct (vincl x (Sgn Ptop 16)) eqn:INCL. exists e#r; split; auto. - assert (V: vmatch bc e#r (Sgn 16)). + assert (V: vmatch bc e#r (Sgn Ptop 16)). { eapply vmatch_ge; eauto. apply vincl_ge; auto. } - inv V; simpl; auto. rewrite is_sgn_sign_ext in H3 by auto. rewrite H3; auto. + inv V; simpl; auto. rewrite is_sgn_sign_ext in H4 by auto. rewrite H4; auto. econstructor; split; simpl; eauto. Qed. @@ -467,11 +467,11 @@ Lemma make_cast16unsigned_correct: let (op, args) := make_cast16unsigned r x in exists v, eval_operation ge (Vptr sp Int.zero) op e##args m = Some v /\ Val.lessdef (Val.zero_ext 16 e#r) v. Proof. - intros; unfold make_cast16unsigned. destruct (vincl x (Uns 16)) eqn:INCL. + intros; unfold make_cast16unsigned. destruct (vincl x (Uns Ptop 16)) eqn:INCL. exists e#r; split; auto. - assert (V: vmatch bc e#r (Uns 16)). + assert (V: vmatch bc e#r (Uns Ptop 16)). { eapply vmatch_ge; eauto. apply vincl_ge; auto. } - inv V; simpl; auto. rewrite is_uns_zero_ext in H3 by auto. rewrite H3; auto. + inv V; simpl; auto. rewrite is_uns_zero_ext in H4 by auto. rewrite H4; auto. econstructor; split; simpl; eauto. Qed. diff --git a/ia32/ValueAOp.v b/ia32/ValueAOp.v index 53013337..93fd8954 100644 --- a/ia32/ValueAOp.v +++ b/ia32/ValueAOp.v @@ -56,8 +56,8 @@ Definition eval_static_operation (op: operation) (vl: list aval): aval := match op, vl with | Omove, v1::nil => v1 | Ointconst n, nil => I n - | Ofloatconst n, nil => if propagate_float_constants tt then F n else ftop - | Osingleconst n, nil => if propagate_float_constants tt then FS n else ftop + | Ofloatconst n, nil => if propagate_float_constants tt then F n else ntop + | Osingleconst n, nil => if propagate_float_constants tt then FS n else ntop | Oindirectsymbol id, nil => Ifptr (Gl id Int.zero) | Ocast8signed, v1 :: nil => sign_ext 8 v1 | Ocast8unsigned, v1 :: nil => zero_ext 8 v1 @@ -132,7 +132,7 @@ Proof. inv VM. destruct cond; auto with va. inv H0. - destruct cond; simpl; eauto with va. + destruct cond; simpl; eauto with va. inv H2. destruct cond; simpl; eauto with va. destruct cond; auto with va. diff --git a/powerpc/Asm.v b/powerpc/Asm.v index a1d8338a..f1e84146 100644 --- a/powerpc/Asm.v +++ b/powerpc/Asm.v @@ -161,10 +161,11 @@ Inductive instruction : Type := | Pcmplwi: ireg -> constant -> instruction (**r same, with immediate argument *) | Pcmpw: ireg -> ireg -> instruction (**r signed integer comparison *) | Pcmpwi: ireg -> constant -> instruction (**r same, with immediate argument *) - | Pcntlzw: ireg -> ireg -> instruction (**r count leading zeros *) + | Pcntlzw: ireg -> ireg -> instruction (**r count leading zeros *) | Pcreqv: crbit -> crbit -> crbit -> instruction (**r not-xor between condition bits *) | Pcror: crbit -> crbit -> crbit -> instruction (**r or between condition bits *) | Pcrxor: crbit -> crbit -> crbit -> instruction (**r xor between condition bits *) + | Pdcbi: ireg -> ireg -> instruction (**r data cache invalidate *) | Pdivw: ireg -> ireg -> ireg -> instruction (**r signed division *) | Pdivwu: ireg -> ireg -> ireg -> instruction (**r unsigned division *) | Peieio: instruction (**r EIEIO barrier *) @@ -201,6 +202,7 @@ Inductive instruction : Type := | Pfres: freg -> freg -> instruction (**r approximate inverse *) | Pfsel: freg -> freg -> freg -> freg -> instruction (**r FP conditional move *) | Pisync: instruction (**r ISYNC barrier *) + | Picbi: ireg -> ireg -> instruction (**r instruction cache invalidate *) | Plbz: ireg -> constant -> ireg -> instruction (**r load 8-bit unsigned int *) | Plbzx: ireg -> ireg -> ireg -> instruction (**r same, with 2 index regs *) | Plfd: freg -> constant -> ireg -> instruction (**r load 64-bit float *) @@ -270,6 +272,7 @@ Inductive instruction : Type := | Psubfze: ireg -> ireg -> instruction (**r integer opposite with carry *) | Psubfic: ireg -> ireg -> constant -> instruction (**r integer subtraction from immediate *) | Psync: instruction (**r SYNC barrier *) + | Plwsync: instruction (**r LWSYNC barrier *) | Ptrap: instruction (**r unconditional trap *) | Pxor: ireg -> ireg -> ireg -> instruction (**r bitwise xor *) | Pxori: ireg -> ireg -> constant -> instruction (**r bitwise xor with immediate *) @@ -856,6 +859,7 @@ Definition exec_instr (f: function) (i: instruction) (rs: regset) (m: mem) : out | Pcntlzw _ _ | Pcreqv _ _ _ | Pcrxor _ _ _ + | Pdcbi _ _ | Peieio | Pfctiw _ _ | Pfctiwz _ _ @@ -869,7 +873,9 @@ Definition exec_instr (f: function) (i: instruction) (rs: regset) (m: mem) : out | Pfsel _ _ _ _ | Plwarx _ _ _ | Plwbrx _ _ _ + | Picbi _ _ | Pisync + | Plwsync | Plhbrx _ _ _ | Plwzu _ _ _ | Pmfcr _ @@ -1060,6 +1066,4 @@ Definition data_preg (r: preg) : bool := | CR0_0 => false | CR0_1 => false | CR0_2 => false | CR0_3 => false | CARRY => false | _ => true - end. - - + end.
\ No newline at end of file diff --git a/powerpc/AsmToJSON.ml b/powerpc/AsmToJSON.ml index 520bc1ed..81ffd500 100644 --- a/powerpc/AsmToJSON.ml +++ b/powerpc/AsmToJSON.ml @@ -175,6 +175,7 @@ let p_instruction oc ic = | Pcreqv (cr1,cr2,cr3) -> fprintf oc "{\"Instruction Name\":\"Pcreqv\",\"Args\":[%a,%a,%a]}" p_crbit cr1 p_crbit cr2 p_crbit cr3 | Pcror (cr1,cr2,cr3) -> fprintf oc "{\"Instruction Name\":\"Pcror\",\"Args\":[%a,%a,%a]}" p_crbit cr1 p_crbit cr2 p_crbit cr3 | Pcrxor (cr1,cr2,cr3) -> fprintf oc "{\"Instruction Name\":\"Pcrxor\",\"Args\":[%a,%a,%a]}" p_crbit cr1 p_crbit cr2 p_crbit cr3 + | Pdcbi (ir1,ir2) -> fprintf oc "{\"Instruction Name\":\"Pdcbi\",\"Args\":[%a,%a]}" p_ireg ir1 p_ireg ir2 | Pdivw (ir1,ir2,ir3) -> fprintf oc "{\"Instruction Name\":\"Pdivw\",\"Args\":[%a,%a,%a]}" p_ireg ir1 p_ireg ir2 p_ireg ir3 | Pdivwu (ir1,ir2,ir3) -> fprintf oc "{\"Instruction Name\":\"Pdivwu\",\"Args\":[%a,%a,%a]}" p_ireg ir1 p_ireg ir2 p_ireg ir3 | Peieio -> fprintf oc "{\"Instruction Name\":\"Peieio,\"Args\":[]}" @@ -210,13 +211,15 @@ let p_instruction oc ic = | Pfrsqrte (fr1,fr2) -> fprintf oc "{\"Instruction Name\":\"Pfsqrte\",\"Args\":[%a,%a]}" p_freg fr1 p_freg fr2 | Pfres (fr1,fr2) -> fprintf oc "{\"Instruction Name\":\"Pfres\",\"Args\":[%a,%a]}" p_freg fr1 p_freg fr2 | Pfsel (fr1,fr2,fr3,fr4) -> fprintf oc "{\"Instruction Name\":\"Pfsel\",\"Args\":[%a,%a,%a,%a]}" p_freg fr1 p_freg fr2 p_freg fr3 p_freg fr4 + | Picbi (ir1,ir2) -> fprintf oc "{\"Instruction Name\":\"Picbi\",\"Args\":[%a,%a]}" p_ireg ir1 p_ireg ir2 | Pisync -> fprintf oc "{\"Instruction Name\":\"Pisync\",\"Args\":[]}" + | Plwsync -> fprintf oc "{\"Instruction Name\":\"Plwsync\",\"Args\":[]}" | Plbz (ir1,c,ir2) -> fprintf oc "{\"Instruction Name\":\"Plbz\",\"Args\":[%a,%a,%a]}" p_ireg ir1 p_constant c p_ireg ir2 | Plbzx (ir1,ir2,ir3) -> fprintf oc "{\"Instruction Name\":\"Pblzx\",\"Args\":[%a,%a,%a]}" p_ireg ir1 p_ireg ir2 p_ireg ir3 | Plfd (fr,c,ir) | Plfd_a (fr,c,ir) -> fprintf oc "{\"Instruction Name\":\"Plfd\",\"Args\":[%a,%a,%a]}" p_freg fr p_constant c p_ireg ir - | Plfdx (fr,ir1,ir2) - | Plfdx_a (fr,ir1,ir2) -> fprintf oc "{\"Instruction Name\":\"Plfdx\",\"Args\":[%a,%a,%a]}" p_freg fr p_ireg ir1 p_ireg ir2 + | Plfdx (fr,ir1,ir2) + | Plfdx_a (fr,ir1,ir2) -> fprintf oc "{\"Instruction Name\":\"Plfdx\",\"Args\":[%a,%a,%a]}" p_freg fr p_ireg ir1 p_ireg ir2 | Plfs (fr,c,ir) -> fprintf oc "{\"Instruction Name\":\"Plfs\",\"Args\":[%a,%a,%a]}" p_freg fr p_constant c p_ireg ir | Plfsx (fr,ir1,ir2) -> fprintf oc "{\"Instruction Name\":\"Plfsx\",\"Args\":[%a,%a,%a]}" p_freg fr p_ireg ir1 p_ireg ir2 | Plha (ir1,c,ir2) -> fprintf oc "{\"Instruction Name\":\"Plha\",\"Args\":[%a,%a,%a]}" p_ireg ir1 p_constant c p_ireg ir2 @@ -349,7 +352,7 @@ let p_vardef oc (name,v) = fprintf oc "{\"Var Name\":%a,\"Var Readonly\":%B,\"Var Volatile\":%B,\n\"Var Storage Class\":%a,\n\"Var Alignment\":%a,\n\"Var Section\":%a,\n\"Var Init\":%a}\n" p_atom name v.gvar_readonly v.gvar_volatile p_storage static p_int_opt alignment p_section section - (p_list p_init_data) v.gvar_init + (p_list p_init_data) v.gvar_init let p_program oc prog = let prog_vars,prog_funs = List.fold_left (fun (vars,funs) (ident,def) -> diff --git a/powerpc/Asmexpand.ml b/powerpc/Asmexpand.ml index b8d30ae3..976f4e77 100644 --- a/powerpc/Asmexpand.ml +++ b/powerpc/Asmexpand.ml @@ -386,12 +386,18 @@ let expand_builtin_inline name args res = emit (Psync) | "__builtin_isync", [], _ -> emit (Pisync) + | "__builtin_lwsync", [], _ -> + emit (Plwsync) | "__builtin_trap", [], _ -> emit (Ptrap) (* Vararg stuff *) | "__builtin_va_start", [IR a], _ -> expand_builtin_va_start a (* Catch-all *) + | "__builtin_dcbi", [IR a1],_ -> + emit (Pdcbi (GPR0,a1)) + | "__builtin_icbi", [IR a1],_ -> + emit (Picbi(GPR0,a1)) | _ -> invalid_arg ("unrecognized builtin " ^ name) diff --git a/powerpc/CBuiltins.ml b/powerpc/CBuiltins.ml index 222a4d94..e774614e 100644 --- a/powerpc/CBuiltins.ml +++ b/powerpc/CBuiltins.ml @@ -83,8 +83,15 @@ let builtins = { (TVoid [], [], false); "__builtin_isync", (TVoid [], [], false); + "__builtin_lwsync", + (TVoid [], [], false); "__builtin_trap", - (TVoid [], [], false) + (TVoid [], [], false); + (* Cache isntructions *) + "__builtin_dcbi", + (TVoid [],[TPtr(TVoid [], [])],false); + "__builtin_icbi", + (TVoid [],[TPtr(TVoid [], [])],false) ] } diff --git a/powerpc/ConstpropOp.vp b/powerpc/ConstpropOp.vp index bba0fad4..7265337d 100644 --- a/powerpc/ConstpropOp.vp +++ b/powerpc/ConstpropOp.vp @@ -52,12 +52,12 @@ Definition make_cmp_base (c: condition) (args: list reg) (vl: list aval) := Nondetfunction make_cmp (c: condition) (args: list reg) (vl: list aval) := match c, args, vl with | Ccompimm Ceq n, r1 :: nil, v1 :: nil => - if Int.eq_dec n Int.one && vincl v1 (Uns 1) then (Omove, r1 :: nil) - else if Int.eq_dec n Int.zero && vincl v1 (Uns 1) then (Oxorimm Int.one, r1 :: nil) + if Int.eq_dec n Int.one && vincl v1 (Uns Ptop 1) then (Omove, r1 :: nil) + else if Int.eq_dec n Int.zero && vincl v1 (Uns Ptop 1) then (Oxorimm Int.one, r1 :: nil) else make_cmp_base c args vl | Ccompimm Cne n, r1 :: nil, v1 :: nil => - if Int.eq_dec n Int.zero && vincl v1 (Uns 1) then (Omove, r1 :: nil) - else if Int.eq_dec n Int.one && vincl v1 (Uns 1) then (Oxorimm Int.one, r1 :: nil) + if Int.eq_dec n Int.zero && vincl v1 (Uns Ptop 1) then (Omove, r1 :: nil) + else if Int.eq_dec n Int.one && vincl v1 (Uns Ptop 1) then (Oxorimm Int.one, r1 :: nil) else make_cmp_base c args vl | _, _, _ => make_cmp_base c args vl @@ -120,7 +120,7 @@ Definition make_divuimm (n: int) (r1 r2: reg) := Definition make_andimm (n: int) (r: reg) (a: aval) := if Int.eq n Int.zero then (Ointconst Int.zero, nil) else if Int.eq n Int.mone then (Omove, r :: nil) - else if match a with Uns m => Int.eq (Int.zero_ext m (Int.not n)) Int.zero + else if match a with Uns _ m => Int.eq (Int.zero_ext m (Int.not n)) Int.zero | _ => false end then (Omove, r :: nil) else (Oandimm n, r :: nil). @@ -146,9 +146,9 @@ Definition make_mulfsimm (n: float32) (r r1 r2: reg) := else (Omulfs, r1 :: r2 :: nil). Definition make_cast8signed (r: reg) (a: aval) := - if vincl a (Sgn 8) then (Omove, r :: nil) else (Ocast8signed, r :: nil). + if vincl a (Sgn Ptop 8) then (Omove, r :: nil) else (Ocast8signed, r :: nil). Definition make_cast16signed (r: reg) (a: aval) := - if vincl a (Sgn 16) then (Omove, r :: nil) else (Ocast16signed, r :: nil). + if vincl a (Sgn Ptop 16) then (Omove, r :: nil) else (Ocast16signed, r :: nil). Nondetfunction op_strength_reduction (op: operation) (args: list reg) (vl: list aval) := diff --git a/powerpc/ConstpropOpproof.v b/powerpc/ConstpropOpproof.v index 8498868a..aac37dc6 100644 --- a/powerpc/ConstpropOpproof.v +++ b/powerpc/ConstpropOpproof.v @@ -131,24 +131,24 @@ Lemma make_cmp_correct: /\ Val.lessdef (Val.of_optbool (eval_condition c rs##args m)) v. Proof. intros c args vl. - assert (Y: forall r, vincl (AE.get r ae) (Uns 1) = true -> + assert (Y: forall r, vincl (AE.get r ae) (Uns Ptop 1) = true -> rs#r = Vundef \/ rs#r = Vint Int.zero \/ rs#r = Vint Int.one). - { intros. apply vmatch_Uns_1 with bc. eapply vmatch_ge. eapply vincl_ge; eauto. apply MATCH. } + { intros. apply vmatch_Uns_1 with bc Ptop. eapply vmatch_ge. eapply vincl_ge; eauto. apply MATCH. } unfold make_cmp. case (make_cmp_match c args vl); intros. -- destruct (Int.eq_dec n Int.one && vincl v1 (Uns 1)) eqn:E1. +- destruct (Int.eq_dec n Int.one && vincl v1 (Uns Ptop 1)) eqn:E1. simpl in H; inv H. InvBooleans. subst n. exists (rs#r1); split; auto. simpl. exploit Y; eauto. intros [A | [A | A]]; rewrite A; simpl; auto. - destruct (Int.eq_dec n Int.zero && vincl v1 (Uns 1)) eqn:E0. + destruct (Int.eq_dec n Int.zero && vincl v1 (Uns Ptop 1)) eqn:E0. simpl in H; inv H. InvBooleans. subst n. exists (Val.xor rs#r1 (Vint Int.one)); split; auto. simpl. exploit Y; eauto. intros [A | [A | A]]; rewrite A; simpl; auto. apply make_cmp_base_correct; auto. -- destruct (Int.eq_dec n Int.zero && vincl v1 (Uns 1)) eqn:E0. +- destruct (Int.eq_dec n Int.zero && vincl v1 (Uns Ptop 1)) eqn:E0. simpl in H; inv H. InvBooleans. subst n. exists (rs#r1); split; auto. simpl. exploit Y; eauto. intros [A | [A | A]]; rewrite A; simpl; auto. - destruct (Int.eq_dec n Int.one && vincl v1 (Uns 1)) eqn:E1. + destruct (Int.eq_dec n Int.one && vincl v1 (Uns Ptop 1)) eqn:E1. simpl in H; inv H. InvBooleans. subst n. exists (Val.xor rs#r1 (Vint Int.one)); split; auto. simpl. exploit Y; eauto. intros [A | [A | A]]; rewrite A; simpl; auto. @@ -271,7 +271,7 @@ Proof. subst n. exists (Vint Int.zero); split; auto. destruct (rs#r); simpl; auto. rewrite Int.and_zero; auto. predSpec Int.eq Int.eq_spec n Int.mone; intros. subst n. exists (rs#r); split; auto. destruct (rs#r); simpl; auto. rewrite Int.and_mone; auto. - destruct (match x with Uns k => Int.eq (Int.zero_ext k (Int.not n)) Int.zero + destruct (match x with Uns _ k => Int.eq (Int.zero_ext k (Int.not n)) Int.zero | _ => false end) eqn:UNS. destruct x; try congruence. exists (rs#r); split; auto. @@ -282,7 +282,7 @@ Proof. rewrite Int.bits_zero. simpl. rewrite andb_true_r. auto. rewrite <- EQ. rewrite Int.bits_zero_ext by omega. rewrite zlt_true by auto. rewrite Int.bits_not by auto. apply negb_involutive. - rewrite H5 by auto. auto. + rewrite H6 by auto. auto. econstructor; split; eauto. auto. Qed. @@ -372,11 +372,11 @@ Lemma make_cast8signed_correct: let (op, args) := make_cast8signed r x in exists v, eval_operation ge (Vptr sp Int.zero) op rs##args m = Some v /\ Val.lessdef (Val.sign_ext 8 rs#r) v. Proof. - intros; unfold make_cast8signed. destruct (vincl x (Sgn 8)) eqn:INCL. + intros; unfold make_cast8signed. destruct (vincl x (Sgn Ptop 8)) eqn:INCL. exists rs#r; split; auto. - assert (V: vmatch bc rs#r (Sgn 8)). + assert (V: vmatch bc rs#r (Sgn Ptop 8)). { eapply vmatch_ge; eauto. apply vincl_ge; auto. } - inv V; simpl; auto. rewrite is_sgn_sign_ext in H3 by auto. rewrite H3; auto. + inv V; simpl; auto. rewrite is_sgn_sign_ext in H4 by auto. rewrite H4; auto. econstructor; split; simpl; eauto. Qed. @@ -386,11 +386,11 @@ Lemma make_cast16signed_correct: let (op, args) := make_cast16signed r x in exists v, eval_operation ge (Vptr sp Int.zero) op rs##args m = Some v /\ Val.lessdef (Val.sign_ext 16 rs#r) v. Proof. - intros; unfold make_cast16signed. destruct (vincl x (Sgn 16)) eqn:INCL. + intros; unfold make_cast16signed. destruct (vincl x (Sgn Ptop 16)) eqn:INCL. exists rs#r; split; auto. - assert (V: vmatch bc rs#r (Sgn 16)). + assert (V: vmatch bc rs#r (Sgn Ptop 16)). { eapply vmatch_ge; eauto. apply vincl_ge; auto. } - inv V; simpl; auto. rewrite is_sgn_sign_ext in H3 by auto. rewrite H3; auto. + inv V; simpl; auto. rewrite is_sgn_sign_ext in H4 by auto. rewrite H4; auto. econstructor; split; simpl; eauto. Qed. diff --git a/powerpc/TargetPrinter.ml b/powerpc/TargetPrinter.ml index 1cd7fe37..cb3ce87a 100644 --- a/powerpc/TargetPrinter.ml +++ b/powerpc/TargetPrinter.ml @@ -469,6 +469,8 @@ module Target (System : SYSTEM):TARGET = fprintf oc " cror %a, %a, %a\n" crbit c1 crbit c2 crbit c3 | Pcrxor(c1, c2, c3) -> fprintf oc " crxor %a, %a, %a\n" crbit c1 crbit c2 crbit c3 + | Pdcbi (r1,r2) -> + fprintf oc " dcbi %a, %a\n" ireg r1 ireg r2 | Pdivw(r1, r2, r3) -> fprintf oc " divw %a, %a, %a\n" ireg r1 ireg r2 ireg r3 | Pdivwu(r1, r2, r3) -> @@ -535,8 +537,12 @@ module Target (System : SYSTEM):TARGET = fprintf oc " fres %a, %a\n" freg r1 freg r2 | Pfsel(r1, r2, r3, r4) -> fprintf oc " fsel %a, %a, %a, %a\n" freg r1 freg r2 freg r3 freg r4 + | Picbi (r1,r2) -> + fprintf oc " icbi %a,%a\n" ireg r1 ireg r2 | Pisync -> fprintf oc " isync\n" + | Plwsync -> + fprintf oc " lwsync\n" | Plbz(r1, c, r2) -> fprintf oc " lbz %a, %a(%a)\n" ireg r1 constant c ireg r2 | Plbzx(r1, r2, r3) -> diff --git a/powerpc/ValueAOp.v b/powerpc/ValueAOp.v index a5a1db80..8cb29145 100644 --- a/powerpc/ValueAOp.v +++ b/powerpc/ValueAOp.v @@ -51,8 +51,8 @@ Definition eval_static_operation (op: operation) (vl: list aval): aval := match op, vl with | Omove, v1::nil => v1 | Ointconst n, nil => I n - | Ofloatconst n, nil => if propagate_float_constants tt then F n else ftop - | Osingleconst n, nil => if propagate_float_constants tt then FS n else ftop + | Ofloatconst n, nil => if propagate_float_constants tt then F n else ntop + | Osingleconst n, nil => if propagate_float_constants tt then FS n else ntop | Oaddrsymbol id ofs, nil => Ptr (Gl id ofs) | Oaddrstack ofs, nil => Ptr (Stk ofs) | Ocast8signed, v1 :: nil => sign_ext 8 v1 diff --git a/test/regression/Makefile b/test/regression/Makefile index e2d94aa9..00c80047 100644 --- a/test/regression/Makefile +++ b/test/regression/Makefile @@ -24,7 +24,7 @@ TESTS=int32 int64 floats floats-basics \ TESTS_COMP=attribs1 bitfields1 bitfields2 bitfields3 bitfields4 \ bitfields5 bitfields6 bitfields7 bitfields8 \ builtins-$(ARCH) packedstruct1 packedstruct2 alignas \ - varargs1 varargs2 sections + varargs1 varargs2 sections alias # Can run, both in compiled mode and in interpreter mode, # but produce processor-dependent results, so no reference output in Results diff --git a/test/regression/Results/alias b/test/regression/Results/alias new file mode 100644 index 00000000..677bed3c --- /dev/null +++ b/test/regression/Results/alias @@ -0,0 +1,8 @@ +Test 1: 1 +Test 2: 1 +Test 3: 1 +Test 4: 1 +Test 5: 1 +Test 6: 1 +Test 7: 1 +Test 8: 0 diff --git a/test/regression/alias.c b/test/regression/alias.c new file mode 100644 index 00000000..a38e6dfd --- /dev/null +++ b/test/regression/alias.c @@ -0,0 +1,168 @@ +/* Testing the alias analysis on ill-defined codes + where it should remain conservative. */ + +typedef unsigned int uintptr_t; +typedef signed int ptrdiff_t; + +/* For testing with GCC */ +#define NOINLINE __attribute__((noinline)) + +/* Passing a pointer through a long long */ + +void NOINLINE set1(long long x) +{ + int * p = (int *) (uintptr_t) x; + *p = 1; +} + +int get1(void) +{ + int x = 0; + set1((uintptr_t) &x); + return x; +} + +/* Passing a pointer through a double */ + +void NOINLINE set2(double x) +{ + int * p = (int *) (uintptr_t) x; + *p = 1; +} + +int get2(void) +{ + int x = 0; + set2((uintptr_t) &x); + return x; +} + +/* Tagging a pointer */ + +void NOINLINE set3(uintptr_t x) +{ + int * p = (int *) (x & ~1); + *p = 1; +} + +int get3(void) +{ + int x = 0; + set3((uintptr_t) &x | 1); + return x; +} + +/* XOR-ing a pointer */ + +static uintptr_t key = 0xDEADBEEF; + +void NOINLINE set4(uintptr_t x) +{ + int * p = (int *) (x ^ key); + *p = 1; +} + +int get4(void) +{ + int x = 0; + set4((uintptr_t) &x ^ key); + return x; +} + +/* Byte-swapping a pointer */ + +inline uintptr_t bswap(uintptr_t x) +{ + return (x >> 24) + | (((x >> 16) & 0xFF) << 8) + | (((x >> 8) & 0xFF) << 16) + | ((x & 0xFF) << 24); +} + +void NOINLINE set5(uintptr_t x) +{ + int * p = (int *) bswap(x); + *p = 1; +} + +int get5(void) +{ + int x = 0; + set5(bswap((uintptr_t) &x)); + return x; +} + +/* Even more fun with xor. This one manufactures a pointer to one object + from a pointer to another, distinct object. Neither GCC nor CompCert + promise to implement the expected behavior, but both happen to do it. +*/ + +int g; + +void NOINLINE set6(int * p, uintptr_t z) +{ + int * q = (int *) ((uintptr_t) p ^ z); + *q = 1; +} + +int get6(void) +{ + int y = 0; + uintptr_t z = (uintptr_t) &g ^ (uintptr_t) &y; + set6(&g, z); + int res1 = y; + g = 0; + set6(&y, z); + int res2 = g; + return res1 & res2; +} + +/* Aligning pointers the hard way */ + +int offset = 3; /* but not const */ + +int get7(void) +{ + union { int i; char c[4]; } u; /* force alignment to 4 */ + u.c[0] = 0; + uintptr_t x = (uintptr_t) &(u.c[offset]); + x = x & ~3; + *((char *) x) = 1; + return u.c[0]; +} + +/* This is an example where wild pointer arithmetic is used to jump + from one object to another. Like GCC and Clang, we don't preserve the + expected behavior. */ + +ptrdiff_t NOINLINE delta8(int * p) +{ + return p - &g; +} + +int get8(void) +{ + int x; + ptrdiff_t d = delta8(&x); + x = 0; + *(&g + d) = 1; + return x; +} + +/* Test harness */ + +#include <stdio.h> + +int main() +{ + printf("Test 1: %d\n", get1()); + printf("Test 2: %d\n", get2()); + printf("Test 3: %d\n", get3()); + printf("Test 4: %d\n", get4()); + printf("Test 5: %d\n", get5()); + printf("Test 6: %d\n", get6()); + printf("Test 7: %d\n", get7()); + printf("Test 8: %d\n", get8()); + return 0; +} + |