From a14b9578ee5297d954103e05d7b2d322816ddd8f Mon Sep 17 00:00:00 2001 From: Xavier Leroy Date: Sat, 1 Oct 2016 17:38:24 +0200 Subject: Support for 64-bit architectures: x86 in 64-bit mode This commit enriches the IA32 port so that it supports x86 processors in 64-bit mode as well as in 32-bit mode, depending on the value of Archi.ptr64, which itself is set from the configuration model. To activate x86-64 bit support, configure with "x86_64-linux". Main steps: - Enrich Op.v and Asm.v with 64-bit operations - SelectLong: in 64-bit mode, use 64-bit operations directly; in 32-bit mode, fall back on the old implementation based on pairs of 32-bit integers - Conventions1: support x86-64 ABI in addition to the 32-bit ABI. - Add support for the new 64-bit operations everywhere. - runtime/x86_64: implementation of the supporting library appropriate for x86 in 64-bit mode To do: - More optimizations are possible on 64-bit integer arithmetic operations. - Could add new chunks to load, say, an unsigned byte into a 64-bit long (currently we load as a 32-bit int then zero-extend). - Implements the wrong ABI for struct passing. --- ia32/Op.v | 895 ++++++++++++++++++++++++++++++++++++++++++++------------------ 1 file changed, 631 insertions(+), 264 deletions(-) (limited to 'ia32/Op.v') diff --git a/ia32/Op.v b/ia32/Op.v index f21d7c6a..ed96c132 100644 --- a/ia32/Op.v +++ b/ia32/Op.v @@ -17,7 +17,7 @@ - [operation]: arithmetic and logical operations; - [addressing]: addressing modes for load and store operations. - These types are IA32-specific and correspond roughly to what the + These types are X86-64-specific and correspond roughly to what the processor can compute in one instruction. In other terms, these types reflect the state of the program after instruction selection. For a processor-independent set of operations, see the abstract @@ -38,135 +38,179 @@ Set Implicit Arguments. (** Conditions (boolean-valued operators). *) Inductive condition : Type := - | Ccomp: comparison -> condition (**r signed integer comparison *) - | Ccompu: comparison -> condition (**r unsigned integer comparison *) - | Ccompimm: comparison -> int -> condition (**r signed integer comparison with a constant *) - | Ccompuimm: comparison -> int -> condition (**r unsigned integer comparison with a constant *) - | Ccompf: comparison -> condition (**r 64-bit floating-point comparison *) - | Cnotcompf: comparison -> condition (**r negation of a floating-point comparison *) - | Ccompfs: comparison -> condition (**r 32-bit floating-point comparison *) - | Cnotcompfs: comparison -> condition (**r negation of a floating-point comparison *) - | Cmaskzero: int -> condition (**r test [(arg & constant) == 0] *) - | Cmasknotzero: int -> condition. (**r test [(arg & constant) != 0] *) + | Ccomp (c: comparison) (**r signed integer comparison *) + | Ccompu (c: comparison) (**r unsigned integer comparison *) + | Ccompimm (c: comparison) (n: int) (**r signed integer comparison with a constant *) + | Ccompuimm (c: comparison) (n: int) (**r unsigned integer comparison with a constant *) + | Ccompl (c: comparison) (**r signed 64-bit integer comparison *) + | Ccomplu (c: comparison) (**r unsigned 64-bit integer comparison *) + | Ccomplimm (c: comparison) (n: int64) (**r signed 64-bit integer comparison with a constant *) + | Ccompluimm (c: comparison) (n: int64) (**r unsigned 64-bit integer comparison with a constant *) + | Ccompf (c: comparison) (**r 64-bit floating-point comparison *) + | Cnotcompf (c: comparison) (**r negation of a floating-point comparison *) + | Ccompfs (c: comparison) (**r 32-bit floating-point comparison *) + | Cnotcompfs (c: comparison) (**r negation of a floating-point comparison *) + | Cmaskzero (n: int) (**r test [(arg & constant) == 0] *) + | Cmasknotzero (n: int). (**r test [(arg & constant) != 0] *) (** Addressing modes. [r1], [r2], etc, are the arguments to the addressing. *) Inductive addressing: Type := - | Aindexed: int -> addressing (**r Address is [r1 + offset] *) - | Aindexed2: int -> addressing (**r Address is [r1 + r2 + offset] *) - | Ascaled: int -> int -> addressing (**r Address is [r1 * scale + offset] *) - | Aindexed2scaled: int -> int -> addressing - (**r Address is [r1 + r2 * scale + offset] *) - | Aglobal: ident -> int -> addressing (**r Address is [symbol + offset] *) - | Abased: ident -> int -> addressing (**r Address is [symbol + offset + r1] *) - | Abasedscaled: int -> ident -> int -> addressing (**r Address is [symbol + offset + r1 * scale] *) - | Ainstack: int -> addressing. (**r Address is [stack_pointer + offset] *) + | Aindexed: Z -> addressing (**r Address is [r1 + offset] *) + | Aindexed2: Z -> addressing (**r Address is [r1 + r2 + offset] *) + | Ascaled: Z -> Z -> addressing (**r Address is [r1 * scale + offset] *) + | Aindexed2scaled: Z -> Z -> addressing + (**r Address is [r1 + r2 * scale + offset] *) + | Aglobal: ident -> ptrofs -> addressing (**r Address is [symbol + offset] *) + | Abased: ident -> ptrofs -> addressing (**r Address is [symbol + offset + r1] *) + | Abasedscaled: Z -> ident -> ptrofs -> addressing (**r Address is [symbol + offset + r1 * scale] *) + | Ainstack: ptrofs -> addressing. (**r Address is [stack_pointer + offset] *) (** Arithmetic and logical operations. In the descriptions, [rd] is the result of the operation and [r1], [r2], etc, are the arguments. *) Inductive operation : Type := - | Omove: operation (**r [rd = r1] *) - | Ointconst: int -> operation (**r [rd] is set to the given integer constant *) - | Ofloatconst: float -> operation (**r [rd] is set to the given float constant *) - | Osingleconst: float32 -> operation (**r [rd] is set to the given float constant *) - | Oindirectsymbol: ident -> operation (**r [rd] is set to the address of the symbol *) -(*c Integer arithmetic: *) - | Ocast8signed: operation (**r [rd] is 8-bit sign extension of [r1] *) - | Ocast8unsigned: operation (**r [rd] is 8-bit zero extension of [r1] *) - | Ocast16signed: operation (**r [rd] is 16-bit sign extension of [r1] *) - | Ocast16unsigned: operation (**r [rd] is 16-bit zero extension of [r1] *) - | Oneg: operation (**r [rd = - r1] *) - | Osub: operation (**r [rd = r1 - r2] *) - | Omul: operation (**r [rd = r1 * r2] *) - | Omulimm: int -> operation (**r [rd = r1 * n] *) - | Omulhs: operation (**r [rd = high part of r1 * r2, signed] *) - | Omulhu: operation (**r [rd = high part of r1 * r2, unsigned] *) - | Odiv: operation (**r [rd = r1 / r2] (signed) *) - | Odivu: operation (**r [rd = r1 / r2] (unsigned) *) - | Omod: operation (**r [rd = r1 % r2] (signed) *) - | Omodu: operation (**r [rd = r1 % r2] (unsigned) *) - | Oand: operation (**r [rd = r1 & r2] *) - | Oandimm: int -> operation (**r [rd = r1 & n] *) - | Oor: operation (**r [rd = r1 | r2] *) - | Oorimm: int -> operation (**r [rd = r1 | n] *) - | Oxor: operation (**r [rd = r1 ^ r2] *) - | Oxorimm: int -> operation (**r [rd = r1 ^ n] *) - | Onot: operation (**r [rd = ~r1] *) - | Oshl: operation (**r [rd = r1 << r2] *) - | Oshlimm: int -> operation (**r [rd = r1 << n] *) - | Oshr: operation (**r [rd = r1 >> r2] (signed) *) - | Oshrimm: int -> operation (**r [rd = r1 >> n] (signed) *) - | Oshrximm: int -> operation (**r [rd = r1 / 2^n] (signed) *) - | Oshru: operation (**r [rd = r1 >> r2] (unsigned) *) - | Oshruimm: int -> operation (**r [rd = r1 >> n] (unsigned) *) - | Ororimm: int -> operation (**r rotate right immediate *) - | Oshldimm: int -> operation (**r [rd = r1 << n | r2 >> (32-n)] *) - | Olea: addressing -> operation (**r effective address *) + | Omove (**r [rd = r1] *) + | Ointconst (n: int) (**r [rd] is set to the given integer constant *) + | Olongconst (n: int64) (**r [rd] is set to the given integer constant *) + | Ofloatconst (n: float) (**r [rd] is set to the given float constant *) + | Osingleconst (n: float32)(**r [rd] is set to the given float constant *) + | Oindirectsymbol (id: ident) (**r [rd] is set to the address of the symbol *) +(*c 32-bit integer arithmetic: *) + | Ocast8signed (**r [rd] is 8-bit sign extension of [r1] *) + | Ocast8unsigned (**r [rd] is 8-bit zero extension of [r1] *) + | Ocast16signed (**r [rd] is 16-bit sign extension of [r1] *) + | Ocast16unsigned (**r [rd] is 16-bit zero extension of [r1] *) + | Oneg (**r [rd = - r1] *) + | Osub (**r [rd = r1 - r2] *) + | Omul (**r [rd = r1 * r2] *) + | Omulimm (n: int) (**r [rd = r1 * n] *) + | Omulhs (**r [rd = high part of r1 * r2, signed] *) + | Omulhu (**r [rd = high part of r1 * r2, unsigned] *) + | Odiv (**r [rd = r1 / r2] (signed) *) + | Odivu (**r [rd = r1 / r2] (unsigned) *) + | Omod (**r [rd = r1 % r2] (signed) *) + | Omodu (**r [rd = r1 % r2] (unsigned) *) + | Oand (**r [rd = r1 & r2] *) + | Oandimm (n: int) (**r [rd = r1 & n] *) + | Oor (**r [rd = r1 | r2] *) + | Oorimm (n: int) (**r [rd = r1 | n] *) + | Oxor (**r [rd = r1 ^ r2] *) + | Oxorimm (n: int) (**r [rd = r1 ^ n] *) + | Onot (**r [rd = ~r1] *) + | Oshl (**r [rd = r1 << r2] *) + | Oshlimm (n: int) (**r [rd = r1 << n] *) + | Oshr (**r [rd = r1 >> r2] (signed) *) + | Oshrimm (n: int) (**r [rd = r1 >> n] (signed) *) + | Oshrximm (n: int) (**r [rd = r1 / 2^n] (signed) *) + | Oshru (**r [rd = r1 >> r2] (unsigned) *) + | Oshruimm (n: int) (**r [rd = r1 >> n] (unsigned) *) + | Ororimm (n: int) (**r rotate right immediate *) + | Oshldimm (n: int) (**r [rd = r1 << n | r2 >> (32-n)] *) + | Olea (a: addressing) (**r effective address *) +(*c 64-bit integer arithmetic: *) + | Omakelong (**r [rd = r1 << 32 | r2] *) + | Olowlong (**r [rd = low-word(r1)] *) + | Ohighlong (**r [rd = high-word(r1)] *) + | Ocast32signed (**r [rd] is 32-bit sign extension of [r1] *) + | Ocast32unsigned (**r [rd] is 32-bit zero extension of [r1] *) + | Onegl (**r [rd = - r1] *) + | Oaddlimm (n: int64) (**r [rd = r1 + n] *) + | Osubl (**r [rd = r1 - r2] *) + | Omull (**r [rd = r1 * r2] *) + | Omullimm (n: int64) (**r [rd = r1 * n] *) + | Odivl (**r [rd = r1 / r2] (signed) *) + | Odivlu (**r [rd = r1 / r2] (unsigned) *) + | Omodl (**r [rd = r1 % r2] (signed) *) + | Omodlu (**r [rd = r1 % r2] (unsigned) *) + | Oandl (**r [rd = r1 & r2] *) + | Oandlimm (n: int64) (**r [rd = r1 & n] *) + | Oorl (**r [rd = r1 | r2] *) + | Oorlimm (n: int64) (**r [rd = r1 | n] *) + | Oxorl (**r [rd = r1 ^ r2] *) + | Oxorlimm (n: int64) (**r [rd = r1 ^ n] *) + | Onotl (**r [rd = ~r1] *) + | Oshll (**r [rd = r1 << r2] *) + | Oshllimm (n: int) (**r [rd = r1 << n] *) + | Oshrl (**r [rd = r1 >> r2] (signed) *) + | Oshrlimm (n: int) (**r [rd = r1 >> n] (signed) *) + | Oshrlu (**r [rd = r1 >> r2] (unsigned) *) + | Oshrluimm (n: int) (**r [rd = r1 >> n] (unsigned) *) + | Ororlimm (n: int) (**r rotate right immediate *) + | Oleal (a: addressing) (**r effective address *) (*c Floating-point arithmetic: *) - | Onegf: operation (**r [rd = - r1] *) - | Oabsf: operation (**r [rd = abs(r1)] *) - | Oaddf: operation (**r [rd = r1 + r2] *) - | Osubf: operation (**r [rd = r1 - r2] *) - | Omulf: operation (**r [rd = r1 * r2] *) - | Odivf: operation (**r [rd = r1 / r2] *) - | Onegfs: operation (**r [rd = - r1] *) - | Oabsfs: operation (**r [rd = abs(r1)] *) - | Oaddfs: operation (**r [rd = r1 + r2] *) - | Osubfs: operation (**r [rd = r1 - r2] *) - | Omulfs: operation (**r [rd = r1 * r2] *) - | Odivfs: operation (**r [rd = r1 / r2] *) - | Osingleoffloat: operation (**r [rd] is [r1] truncated to single-precision float *) - | Ofloatofsingle: operation (**r [rd] is [r1] extended to double-precision float *) + | Onegf (**r [rd = - r1] *) + | Oabsf (**r [rd = abs(r1)] *) + | Oaddf (**r [rd = r1 + r2] *) + | Osubf (**r [rd = r1 - r2] *) + | Omulf (**r [rd = r1 * r2] *) + | Odivf (**r [rd = r1 / r2] *) + | Onegfs (**r [rd = - r1] *) + | Oabsfs (**r [rd = abs(r1)] *) + | Oaddfs (**r [rd = r1 + r2] *) + | Osubfs (**r [rd = r1 - r2] *) + | Omulfs (**r [rd = r1 * r2] *) + | Odivfs (**r [rd = r1 / r2] *) + | Osingleoffloat (**r [rd] is [r1] truncated to single-precision float *) + | Ofloatofsingle (**r [rd] is [r1] extended to double-precision float *) (*c Conversions between int and float: *) - | Ointoffloat: operation (**r [rd = signed_int_of_float64(r1)] *) - | Ofloatofint: operation (**r [rd = float64_of_signed_int(r1)] *) - | Ointofsingle: operation (**r [rd = signed_int_of_float32(r1)] *) - | Osingleofint: operation (**r [rd = float32_of_signed_int(r1)] *) -(*c Manipulating 64-bit integers: *) - | Omakelong: operation (**r [rd = r1 << 32 | r2] *) - | Olowlong: operation (**r [rd = low-word(r1)] *) - | Ohighlong: operation (**r [rd = high-word(r1)] *) + | Ointoffloat (**r [rd = signed_int_of_float64(r1)] *) + | Ofloatofint (**r [rd = float64_of_signed_int(r1)] *) + | Ointofsingle (**r [rd = signed_int_of_float32(r1)] *) + | Osingleofint (**r [rd = float32_of_signed_int(r1)] *) + | Olongoffloat (**r [rd = signed_long_of_float64(r1)] *) + | Ofloatoflong (**r [rd = float64_of_signed_long(r1)] *) + | Olongofsingle (**r [rd = signed_long_of_float32(r1)] *) + | Osingleoflong (**r [rd = float32_of_signed_long(r1)] *) (*c Boolean tests: *) - | Ocmp: condition -> operation. (**r [rd = 1] if condition holds, [rd = 0] otherwise. *) - -(** Derived operators. *) - -Definition Oaddrsymbol (id: ident) (ofs: int) : operation := Olea (Aglobal id ofs). -Definition Oaddrstack (ofs: int) : operation := Olea (Ainstack ofs). -Definition Oaddimm (n: int) : operation := Olea (Aindexed n). + | Ocmp (cond: condition). (**r [rd = 1] if condition holds, [rd = 0] otherwise. *) (** Comparison functions (used in modules [CSE] and [Allocation]). *) Definition eq_condition (x y: condition) : {x=y} + {x<>y}. Proof. - generalize Int.eq_dec; intro. + generalize Int.eq_dec Int64.eq_dec; intro. assert (forall (x y: comparison), {x=y}+{x<>y}). decide equality. decide equality. Defined. Definition eq_addressing (x y: addressing) : {x=y} + {x<>y}. Proof. - generalize Int.eq_dec; intro. - assert (forall (x y: ident), {x=y}+{x<>y}). exact peq. + generalize ident_eq Ptrofs.eq_dec zeq; intros. decide equality. Defined. Definition eq_operation (x y: operation): {x=y} + {x<>y}. Proof. - generalize Int.eq_dec; intro. - generalize Float.eq_dec; intro. - generalize Float32.eq_dec; intro. - generalize Int64.eq_dec; intro. + generalize Int.eq_dec Int64.eq_dec Float.eq_dec Float32.eq_dec; intros. decide equality. - apply peq. + apply ident_eq. + apply eq_addressing. apply eq_addressing. apply eq_condition. Defined. Global Opaque eq_condition eq_addressing eq_operation. +(** In addressing modes, offsets are 32-bit signed integers, even in 64-bit mode. + The following function checks that an addressing mode is valid, i.e. that + the offsets are in range. *) + +Definition offset_in_range (n: Z) : bool := zle Int.min_signed n && zle n Int.max_signed. + +Definition addressing_valid (a: addressing) : bool := + match a with + | Aindexed n => offset_in_range n + | Aindexed2 n => offset_in_range n + | Ascaled sc ofs => offset_in_range ofs + | Aindexed2scaled sc ofs => offset_in_range ofs + | Aglobal s ofs => true + | Abased s ofs => true + | Abasedscaled sc s ofs => true + | Ainstack ofs => offset_in_range (Ptrofs.signed ofs) + end. + (** * Evaluation functions *) (** Evaluation of conditions, operators and addressing modes applied @@ -180,6 +224,10 @@ Definition eval_condition (cond: condition) (vl: list val) (m: mem): option bool | Ccompu c, v1 :: v2 :: nil => Val.cmpu_bool (Mem.valid_pointer m) c v1 v2 | Ccompimm c n, v1 :: nil => Val.cmp_bool c v1 (Vint n) | Ccompuimm c n, v1 :: nil => Val.cmpu_bool (Mem.valid_pointer m) c v1 (Vint n) + | Ccompl c, v1 :: v2 :: nil => Val.cmpl_bool c v1 v2 + | Ccomplu c, v1 :: v2 :: nil => Val.cmplu_bool (Mem.valid_pointer m) c v1 v2 + | Ccomplimm c n, v1 :: nil => Val.cmpl_bool c v1 (Vlong n) + | Ccompluimm c n, v1 :: nil => Val.cmplu_bool (Mem.valid_pointer m) c v1 (Vlong n) | Ccompf c, v1 :: v2 :: nil => Val.cmpf_bool c v1 v2 | Cnotcompf c, v1 :: v2 :: nil => option_map negb (Val.cmpf_bool c v1 v2) | Ccompfs c, v1 :: v2 :: nil => Val.cmpfs_bool c v1 v2 @@ -189,38 +237,65 @@ Definition eval_condition (cond: condition) (vl: list val) (m: mem): option bool | _, _ => None end. -Definition eval_addressing +Definition eval_addressing32 (F V: Type) (genv: Genv.t F V) (sp: val) (addr: addressing) (vl: list val) : option val := match addr, vl with | Aindexed n, v1::nil => - Some (Val.add v1 (Vint n)) + Some (Val.add v1 (Vint (Int.repr n))) | Aindexed2 n, v1::v2::nil => - Some (Val.add (Val.add v1 v2) (Vint n)) + Some (Val.add (Val.add v1 v2) (Vint (Int.repr n))) | Ascaled sc ofs, v1::nil => - Some (Val.add (Val.mul v1 (Vint sc)) (Vint ofs)) + Some (Val.add (Val.mul v1 (Vint (Int.repr sc))) (Vint (Int.repr ofs))) | Aindexed2scaled sc ofs, v1::v2::nil => - Some(Val.add v1 (Val.add (Val.mul v2 (Vint sc)) (Vint ofs))) + Some(Val.add v1 (Val.add (Val.mul v2 (Vint (Int.repr sc))) (Vint (Int.repr ofs)))) | Aglobal s ofs, nil => - Some (Genv.symbol_address genv s ofs) + if Archi.ptr64 then None else Some (Genv.symbol_address genv s ofs) | Abased s ofs, v1::nil => - Some (Val.add (Genv.symbol_address genv s ofs) v1) + if Archi.ptr64 then None else Some (Val.add (Genv.symbol_address genv s ofs) v1) | Abasedscaled sc s ofs, v1::nil => - Some (Val.add (Genv.symbol_address genv s ofs) (Val.mul v1 (Vint sc))) + if Archi.ptr64 then None else Some (Val.add (Genv.symbol_address genv s ofs) (Val.mul v1 (Vint (Int.repr sc)))) | Ainstack ofs, nil => - Some(Val.add sp (Vint ofs)) + if Archi.ptr64 then None else Some(Val.offset_ptr sp ofs) | _, _ => None end. +Definition eval_addressing64 + (F V: Type) (genv: Genv.t F V) (sp: val) + (addr: addressing) (vl: list val) : option val := + match addr, vl with + | Aindexed n, v1::nil => + Some (Val.addl v1 (Vlong (Int64.repr n))) + | Aindexed2 n, v1::v2::nil => + Some (Val.addl (Val.addl v1 v2) (Vlong (Int64.repr n))) + | Ascaled sc ofs, v1::nil => + Some (Val.addl (Val.mull v1 (Vlong (Int64.repr sc))) (Vlong (Int64.repr ofs))) + | Aindexed2scaled sc ofs, v1::v2::nil => + Some(Val.addl v1 (Val.addl (Val.mull v2 (Vlong (Int64.repr sc))) (Vlong (Int64.repr ofs)))) + | Aglobal s ofs, nil => + if Archi.ptr64 then Some (Genv.symbol_address genv s ofs) else None + | Ainstack ofs, nil => + if Archi.ptr64 then Some(Val.offset_ptr sp ofs) else None + | _, _ => None + end. + +Definition eval_addressing + (F V: Type) (genv: Genv.t F V) (sp: val) + (addr: addressing) (vl: list val) : option val := + if Archi.ptr64 + then eval_addressing64 genv sp addr vl + else eval_addressing32 genv sp addr vl. + Definition eval_operation (F V: Type) (genv: Genv.t F V) (sp: val) (op: operation) (vl: list val) (m: mem): option val := match op, vl with | Omove, v1::nil => Some v1 | Ointconst n, nil => Some (Vint n) + | Olongconst n, nil => Some (Vlong n) | Ofloatconst n, nil => Some (Vfloat n) | Osingleconst n, nil => Some (Vsingle n) - | Oindirectsymbol id, nil => Some (Genv.symbol_address genv id Int.zero) + | Oindirectsymbol id, nil => Some (Genv.symbol_address genv id Ptrofs.zero) | Ocast8signed, v1 :: nil => Some (Val.sign_ext 8 v1) | Ocast8unsigned, v1 :: nil => Some (Val.zero_ext 8 v1) | Ocast16signed, v1 :: nil => Some (Val.sign_ext 16 v1) @@ -252,7 +327,36 @@ Definition eval_operation | Ororimm n, v1::nil => Some (Val.ror v1 (Vint n)) | Oshldimm n, v1::v2::nil => Some (Val.or (Val.shl v1 (Vint n)) (Val.shru v2 (Vint (Int.sub Int.iwordsize n)))) - | Olea addr, _ => eval_addressing genv sp addr vl + | Olea addr, _ => eval_addressing32 genv sp addr vl + | Omakelong, v1::v2::nil => Some(Val.longofwords v1 v2) + | Olowlong, v1::nil => Some(Val.loword v1) + | Ohighlong, v1::nil => Some(Val.hiword v1) + | Ocast32signed, v1 :: nil => Some (Val.longofint v1) + | Ocast32unsigned, v1 :: nil => Some (Val.longofintu v1) + | Onegl, v1::nil => Some (Val.negl v1) + | Oaddlimm n, v1::nil => Some (Val.addl v1 (Vlong n)) + | Osubl, v1::v2::nil => Some (Val.subl v1 v2) + | Omull, v1::v2::nil => Some (Val.mull v1 v2) + | Omullimm n, v1::nil => Some (Val.mull v1 (Vlong n)) + | Odivl, v1::v2::nil => Val.divls v1 v2 + | Odivlu, v1::v2::nil => Val.divlu v1 v2 + | Omodl, v1::v2::nil => Val.modls v1 v2 + | Omodlu, v1::v2::nil => Val.modlu v1 v2 + | Oandl, v1::v2::nil => Some(Val.andl v1 v2) + | Oandlimm n, v1::nil => Some (Val.andl v1 (Vlong n)) + | Oorl, v1::v2::nil => Some(Val.orl v1 v2) + | Oorlimm n, v1::nil => Some (Val.orl v1 (Vlong n)) + | Oxorl, v1::v2::nil => Some(Val.xorl v1 v2) + | Oxorlimm n, v1::nil => Some (Val.xorl v1 (Vlong n)) + | Onotl, v1::nil => Some(Val.notl v1) + | Oshll, v1::v2::nil => Some (Val.shll v1 v2) + | Oshllimm n, v1::nil => Some (Val.shll v1 (Vint n)) + | Oshrl, v1::v2::nil => Some (Val.shrl v1 v2) + | Oshrlimm n, v1::nil => Some (Val.shrl v1 (Vint n)) + | Oshrlu, v1::v2::nil => Some (Val.shrlu v1 v2) + | Oshrluimm n, v1::nil => Some (Val.shrlu v1 (Vint n)) + | Ororlimm n, v1::nil => Some (Val.rorl v1 (Vint n)) + | Oleal addr, _ => eval_addressing64 genv sp addr vl | Onegf, v1::nil => Some(Val.negf v1) | Oabsf, v1::nil => Some(Val.absf v1) | Oaddf, v1::v2::nil => Some(Val.addf v1 v2) @@ -271,21 +375,48 @@ Definition eval_operation | Ofloatofint, v1::nil => Val.floatofint v1 | Ointofsingle, v1::nil => Val.intofsingle v1 | Osingleofint, v1::nil => Val.singleofint v1 - | Omakelong, v1::v2::nil => Some(Val.longofwords v1 v2) - | Olowlong, v1::nil => Some(Val.loword v1) - | Ohighlong, v1::nil => Some(Val.hiword v1) + | Olongoffloat, v1::nil => Val.longoffloat v1 + | Ofloatoflong, v1::nil => Val.floatoflong v1 + | Olongofsingle, v1::nil => Val.longofsingle v1 + | Osingleoflong, v1::nil => Val.singleoflong v1 | Ocmp c, _ => Some(Val.of_optbool (eval_condition c vl m)) | _, _ => None end. +Remark eval_addressing_Aglobal: + forall (F V: Type) (genv: Genv.t F V) sp id ofs, + eval_addressing genv sp (Aglobal id ofs) nil = Some (Genv.symbol_address genv id ofs). +Proof. + intros. unfold eval_addressing, eval_addressing32, eval_addressing64; destruct Archi.ptr64; auto. +Qed. + +Remark eval_addressing_Ainstack: + forall (F V: Type) (genv: Genv.t F V) sp ofs, + eval_addressing genv sp (Ainstack ofs) nil = Some (Val.offset_ptr sp ofs). +Proof. + intros. unfold eval_addressing, eval_addressing32, eval_addressing64; destruct Archi.ptr64; auto. +Qed. + +Remark eval_addressing_Ainstack_inv: + forall (F V: Type) (genv: Genv.t F V) sp ofs vl v, + eval_addressing genv sp (Ainstack ofs) vl = Some v -> vl = nil /\ v = Val.offset_ptr sp ofs. +Proof. + unfold eval_addressing, eval_addressing32, eval_addressing64; + intros; destruct Archi.ptr64; destruct vl; inv H; auto. +Qed. + Ltac FuncInv := match goal with | H: (match ?x with nil => _ | _ :: _ => _ end = Some _) |- _ => - destruct x; simpl in H; try discriminate; FuncInv + destruct x; simpl in H; try discriminate H; FuncInv | H: (match ?v with Vundef => _ | Vint _ => _ | Vfloat _ => _ | Vptr _ _ => _ end = Some _) |- _ => - destruct v; simpl in H; try discriminate; FuncInv + destruct v; simpl in H; try discriminate H; FuncInv + | H: (if Archi.ptr64 then _ else _) = Some _ |- _ => + destruct Archi.ptr64 eqn:?; try discriminate H; FuncInv | H: (Some _ = Some _) |- _ => injection H; intros; clear H; FuncInv + | H: (None = Some _) |- _ => + discriminate H | _ => idtac end. @@ -298,6 +429,10 @@ Definition type_of_condition (c: condition) : list typ := | Ccompu _ => Tint :: Tint :: nil | Ccompimm _ _ => Tint :: nil | Ccompuimm _ _ => Tint :: nil + | Ccompl _ => Tlong :: Tlong :: nil + | Ccomplu _ => Tlong :: Tlong :: nil + | Ccomplimm _ _ => Tlong :: nil + | Ccompluimm _ _ => Tlong :: nil | Ccompf _ => Tfloat :: Tfloat :: nil | Cnotcompf _ => Tfloat :: Tfloat :: nil | Ccompfs _ => Tsingle :: Tsingle :: nil @@ -306,25 +441,30 @@ Definition type_of_condition (c: condition) : list typ := | Cmasknotzero _ => Tint :: nil end. -Definition type_of_addressing (addr: addressing) : list typ := +Definition type_of_addressing_gen (tyA: typ) (addr: addressing): list typ := match addr with - | Aindexed _ => Tint :: nil - | Aindexed2 _ => Tint :: Tint :: nil - | Ascaled _ _ => Tint :: nil - | Aindexed2scaled _ _ => Tint :: Tint :: nil + | Aindexed _ => tyA :: nil + | Aindexed2 _ => tyA :: tyA :: nil + | Ascaled _ _ => tyA :: nil + | Aindexed2scaled _ _ => tyA :: tyA :: nil | Aglobal _ _ => nil - | Abased _ _ => Tint :: nil - | Abasedscaled _ _ _ => Tint :: nil + | Abased _ _ => tyA :: nil + | Abasedscaled _ _ _ => tyA :: nil | Ainstack _ => nil end. +Definition type_of_addressing := type_of_addressing_gen Tptr. +Definition type_of_addressing32 := type_of_addressing_gen Tint. +Definition type_of_addressing64 := type_of_addressing_gen Tlong. + Definition type_of_operation (op: operation) : list typ * typ := match op with | Omove => (nil, Tint) (* treated specially *) | Ointconst _ => (nil, Tint) + | Olongconst _ => (nil, Tlong) | Ofloatconst f => (nil, Tfloat) | Osingleconst f => (nil, Tsingle) - | Oindirectsymbol _ => (nil, Tint) + | Oindirectsymbol _ => (nil, Tptr) | Ocast8signed => (Tint :: nil, Tint) | Ocast8unsigned => (Tint :: nil, Tint) | Ocast16signed => (Tint :: nil, Tint) @@ -355,7 +495,36 @@ Definition type_of_operation (op: operation) : list typ * typ := | Oshruimm _ => (Tint :: nil, Tint) | Ororimm _ => (Tint :: nil, Tint) | Oshldimm _ => (Tint :: Tint :: nil, Tint) - | Olea addr => (type_of_addressing addr, Tint) + | Olea addr => (type_of_addressing32 addr, Tint) + | Omakelong => (Tint :: Tint :: nil, Tlong) + | Olowlong => (Tlong :: nil, Tint) + | Ohighlong => (Tlong :: nil, Tint) + | Ocast32signed => (Tint :: nil, Tlong) + | Ocast32unsigned => (Tint :: nil, Tlong) + | Onegl => (Tlong :: nil, Tlong) + | Oaddlimm _ => (Tlong :: nil, Tlong) + | Osubl => (Tlong :: Tlong :: nil, Tlong) + | Omull => (Tlong :: Tlong :: nil, Tlong) + | Omullimm _ => (Tlong :: nil, Tlong) + | Odivl => (Tlong :: Tlong :: nil, Tlong) + | Odivlu => (Tlong :: Tlong :: nil, Tlong) + | Omodl => (Tlong :: Tlong :: nil, Tlong) + | Omodlu => (Tlong :: Tlong :: nil, Tlong) + | Oandl => (Tlong :: Tlong :: nil, Tlong) + | Oandlimm _ => (Tlong :: nil, Tlong) + | Oorl => (Tlong :: Tlong :: nil, Tlong) + | Oorlimm _ => (Tlong :: nil, Tlong) + | Oxorl => (Tlong :: Tlong :: nil, Tlong) + | Oxorlimm _ => (Tlong :: nil, Tlong) + | Onotl => (Tlong :: nil, Tlong) + | Oshll => (Tlong :: Tint :: nil, Tlong) + | Oshllimm _ => (Tlong :: nil, Tlong) + | Oshrl => (Tlong :: Tint :: nil, Tlong) + | Oshrlimm _ => (Tlong :: nil, Tlong) + | Oshrlu => (Tlong :: Tint :: nil, Tlong) + | Oshrluimm _ => (Tlong :: nil, Tlong) + | Ororlimm _ => (Tlong :: nil, Tlong) + | Oleal addr => (type_of_addressing64 addr, Tlong) | Onegf => (Tfloat :: nil, Tfloat) | Oabsf => (Tfloat :: nil, Tfloat) | Oaddf => (Tfloat :: Tfloat :: nil, Tfloat) @@ -374,9 +543,10 @@ Definition type_of_operation (op: operation) : list typ * typ := | Ofloatofint => (Tint :: nil, Tfloat) | Ointofsingle => (Tsingle :: nil, Tint) | Osingleofint => (Tint :: nil, Tsingle) - | Omakelong => (Tint :: Tint :: nil, Tlong) - | Olowlong => (Tlong :: nil, Tint) - | Ohighlong => (Tlong :: nil, Tint) + | Olongoffloat => (Tfloat :: nil, Tlong) + | Ofloatoflong => (Tlong :: nil, Tfloat) + | Olongofsingle => (Tsingle :: nil, Tlong) + | Osingleoflong => (Tlong :: nil, Tsingle) | Ocmp c => (type_of_condition c, Tint) end. @@ -389,22 +559,45 @@ Section SOUNDNESS. Variable A V: Type. Variable genv: Genv.t A V. -Lemma type_of_addressing_sound: +Remark type_add: + forall v1 v2, Val.has_type (Val.add v1 v2) Tint. +Proof. + intros. unfold Val.has_type, Val.add. destruct Archi.ptr64, v1, v2; auto. +Qed. + +Remark type_addl: + forall v1 v2, Val.has_type (Val.addl v1 v2) Tlong. +Proof. + intros. unfold Val.has_type, Val.addl. destruct Archi.ptr64, v1, v2; auto. +Qed. + +Lemma type_of_addressing64_sound: forall addr vl sp v, - eval_addressing genv sp addr vl = Some v -> + eval_addressing64 genv sp addr vl = Some v -> + Val.has_type v Tlong. +Proof. + intros. destruct addr; simpl in H; FuncInv; subst; simpl; auto using type_addl. +- unfold Genv.symbol_address; destruct (Genv.find_symbol genv i); simpl; auto. +- destruct sp; simpl; auto. +Qed. + +Lemma type_of_addressing32_sound: + forall addr vl sp v, + eval_addressing32 genv sp addr vl = Some v -> Val.has_type v Tint. -Proof with (try exact I). - intros. destruct addr; simpl in H; FuncInv; subst; simpl. - destruct v0... - destruct v0... destruct v1... destruct v1... - destruct v0... - destruct v0... destruct v1... destruct v1... - unfold Genv.symbol_address; destruct (Genv.find_symbol genv i)... - unfold Genv.symbol_address; destruct (Genv.find_symbol genv i)... - unfold Genv.symbol_address; destruct (Genv.find_symbol genv i)... destruct v0... - destruct v0... - unfold Genv.symbol_address; destruct (Genv.find_symbol genv i0)... destruct v0... - destruct sp... +Proof. + intros. destruct addr; simpl in H; FuncInv; subst; simpl; auto using type_add. +- unfold Genv.symbol_address; destruct (Genv.find_symbol genv i); simpl; auto. +- destruct sp; simpl; auto. +Qed. + +Corollary type_of_addressing_sound: + forall addr vl sp v, + eval_addressing genv sp addr vl = Some v -> + Val.has_type v Tptr. +Proof. + unfold eval_addressing, Tptr; intros. + destruct Archi.ptr64; eauto using type_of_addressing64_sound, type_of_addressing32_sound. Qed. Lemma type_of_operation_sound: @@ -419,13 +612,17 @@ Proof with (try exact I). exact I. exact I. exact I. - unfold Genv.symbol_address; destruct (Genv.find_symbol genv i)... + exact I. + unfold Genv.symbol_address; destruct (Genv.find_symbol genv id)... + unfold Val.has_type, Tptr; destruct Archi.ptr64; auto. destruct v0... destruct v0... destruct v0... destruct v0... destruct v0... - destruct v0; destruct v1... simpl. destruct (eq_block b b0)... + destruct v0; destruct v1; simpl... + unfold Val.has_type; destruct Archi.ptr64; auto. + unfold Val.has_type; destruct Archi.ptr64; auto. destruct (eq_block b b0); auto. destruct v0; destruct v1... destruct v0... destruct v0; destruct v1... @@ -444,16 +641,49 @@ Proof with (try exact I). destruct v0... destruct v0... destruct v0; destruct v1; simpl... destruct (Int.ltu i0 Int.iwordsize)... - destruct v0; simpl... destruct (Int.ltu i Int.iwordsize)... + destruct v0; simpl... destruct (Int.ltu n Int.iwordsize)... destruct v0; destruct v1; simpl... destruct (Int.ltu i0 Int.iwordsize)... - destruct v0; simpl... destruct (Int.ltu i Int.iwordsize)... - destruct v0; simpl in H0; try discriminate. destruct (Int.ltu i (Int.repr 31)); inv H0... + destruct v0; simpl... destruct (Int.ltu n Int.iwordsize)... + destruct v0; simpl in H0; try discriminate. destruct (Int.ltu n (Int.repr 31)); inv H0... destruct v0; destruct v1; simpl... destruct (Int.ltu i0 Int.iwordsize)... - destruct v0; simpl... destruct (Int.ltu i Int.iwordsize)... + destruct v0; simpl... destruct (Int.ltu n Int.iwordsize)... + destruct v0... + destruct v0; simpl... destruct (Int.ltu n Int.iwordsize)... + destruct v1; simpl... destruct (Int.ltu (Int.sub Int.iwordsize n) Int.iwordsize)... + eapply type_of_addressing32_sound; eauto. + destruct v0; destruct v1... + destruct v0... + destruct v0... + destruct v0... + destruct v0... + destruct v0... + destruct v0; simpl... unfold Val.has_type; destruct Archi.ptr64; auto. + destruct v0; destruct v1; simpl... + unfold Val.has_type; destruct Archi.ptr64; auto. + unfold Val.has_type; destruct Archi.ptr64; simpl; auto. destruct (eq_block b b0); auto. + destruct v0; destruct v1... + destruct v0... + destruct v0; destruct v1; simpl in *; inv H0. + destruct (Int64.eq i0 Int64.zero || Int64.eq i (Int64.repr Int64.min_signed) && Int64.eq i0 Int64.mone); inv H2... + destruct v0; destruct v1; simpl in *; inv H0. destruct (Int64.eq i0 Int64.zero); inv H2... + destruct v0; destruct v1; simpl in *; inv H0. + destruct (Int64.eq i0 Int64.zero || Int64.eq i (Int64.repr Int64.min_signed) && Int64.eq i0 Int64.mone); inv H2... + destruct v0; destruct v1; simpl in *; inv H0. destruct (Int64.eq i0 Int64.zero); inv H2... + destruct v0; destruct v1... + destruct v0... + destruct v0; destruct v1... + destruct v0... + destruct v0; destruct v1... + destruct v0... + destruct v0... + destruct v0; destruct v1; simpl... destruct (Int.ltu i0 Int64.iwordsize')... + destruct v0; simpl... destruct (Int.ltu n Int64.iwordsize')... + destruct v0; destruct v1; simpl... destruct (Int.ltu i0 Int64.iwordsize')... + destruct v0; simpl... destruct (Int.ltu n Int64.iwordsize')... + destruct v0; destruct v1; simpl... destruct (Int.ltu i0 Int64.iwordsize')... + destruct v0; simpl... destruct (Int.ltu n Int64.iwordsize')... destruct v0... - destruct v0; simpl... destruct (Int.ltu i Int.iwordsize)... - destruct v1; simpl... destruct (Int.ltu (Int.sub Int.iwordsize i) Int.iwordsize)... - eapply type_of_addressing_sound; eauto. + eapply type_of_addressing64_sound; eauto. destruct v0... destruct v0... destruct v0; destruct v1... @@ -472,10 +702,11 @@ Proof with (try exact I). destruct v0; simpl in H0; inv H0... destruct v0; simpl in H0; inv H0. destruct (Float32.to_int f); inv H2... destruct v0; simpl in H0; inv H0... - destruct v0; destruct v1... - destruct v0... - destruct v0... - destruct (eval_condition c vl m); simpl... destruct b... + destruct v0; simpl in H0; inv H0. destruct (Float.to_long f); inv H2... + destruct v0; simpl in H0; inv H0... + destruct v0; simpl in H0; inv H0. destruct (Float32.to_long f); inv H2... + destruct v0; simpl in H0; inv H0... + destruct (eval_condition cond vl m); simpl... destruct b... Qed. End SOUNDNESS. @@ -512,6 +743,10 @@ Definition negate_condition (cond: condition): condition := | Ccompu c => Ccompu(negate_comparison c) | Ccompimm c n => Ccompimm (negate_comparison c) n | Ccompuimm c n => Ccompuimm (negate_comparison c) n + | Ccompl c => Ccompl(negate_comparison c) + | Ccomplu c => Ccomplu(negate_comparison c) + | Ccomplimm c n => Ccomplimm (negate_comparison c) n + | Ccompluimm c n => Ccompluimm (negate_comparison c) n | Ccompf c => Cnotcompf c | Cnotcompf c => Ccompf c | Ccompfs c => Cnotcompfs c @@ -529,25 +764,30 @@ Proof. repeat (destruct vl; auto). apply Val.negate_cmpu_bool. repeat (destruct vl; auto). apply Val.negate_cmp_bool. repeat (destruct vl; auto). apply Val.negate_cmpu_bool. + repeat (destruct vl; auto). apply Val.negate_cmpl_bool. + repeat (destruct vl; auto). apply Val.negate_cmplu_bool. + repeat (destruct vl; auto). apply Val.negate_cmpl_bool. + repeat (destruct vl; auto). apply Val.negate_cmplu_bool. repeat (destruct vl; auto). repeat (destruct vl; auto). destruct (Val.cmpf_bool c v v0) as [[]|]; auto. repeat (destruct vl; auto). repeat (destruct vl; auto). destruct (Val.cmpfs_bool c v v0) as [[]|]; auto. destruct vl; auto. destruct vl; auto. - destruct vl; auto. destruct vl; auto. destruct (Val.maskzero_bool v i) as [[]|]; auto. + destruct vl; auto. destruct vl; auto. destruct (Val.maskzero_bool v n) as [[]|]; auto. Qed. (** Shifting stack-relative references. This is used in [Stacking]. *) -Definition shift_stack_addressing (delta: int) (addr: addressing) := +Definition shift_stack_addressing (delta: Z) (addr: addressing) := match addr with - | Ainstack ofs => Ainstack (Int.add delta ofs) + | Ainstack ofs => Ainstack (Ptrofs.add ofs (Ptrofs.repr delta)) | _ => addr end. -Definition shift_stack_operation (delta: int) (op: operation) := +Definition shift_stack_operation (delta: Z) (op: operation) := match op with - | Olea addr => Olea (shift_stack_addressing delta addr) + | Olea addr => Olea (shift_stack_addressing delta addr) + | Oleal addr => Oleal (shift_stack_addressing delta addr) | _ => op end. @@ -560,75 +800,116 @@ Qed. Lemma type_shift_stack_operation: forall delta op, type_of_operation (shift_stack_operation delta op) = type_of_operation op. Proof. - intros. destruct op; auto. simpl. decEq. apply type_shift_stack_addressing. + intros. destruct op; auto; simpl; decEq; destruct a; auto. Qed. -Lemma eval_shift_stack_addressing: +Lemma eval_shift_stack_addressing32: forall F V (ge: Genv.t F V) sp addr vl delta, - eval_addressing ge sp (shift_stack_addressing delta addr) vl = - eval_addressing ge (Val.add sp (Vint delta)) addr vl. + eval_addressing32 ge (Vptr sp Ptrofs.zero) (shift_stack_addressing delta addr) vl = + eval_addressing32 ge (Vptr sp (Ptrofs.repr delta)) addr vl. Proof. intros. destruct addr; simpl; auto. - rewrite Val.add_assoc. simpl. auto. + destruct vl; auto. destruct Archi.ptr64 eqn:SF; auto. + do 2 f_equal. rewrite Ptrofs.add_zero_l. apply Ptrofs.add_commut. +Qed. + +Lemma eval_shift_stack_addressing64: + forall F V (ge: Genv.t F V) sp addr vl delta, + eval_addressing64 ge (Vptr sp Ptrofs.zero) (shift_stack_addressing delta addr) vl = + eval_addressing64 ge (Vptr sp (Ptrofs.repr delta)) addr vl. +Proof. + intros. destruct addr; simpl; auto. + destruct vl; auto. destruct Archi.ptr64 eqn:SF; auto. + do 2 f_equal. rewrite Ptrofs.add_zero_l. apply Ptrofs.add_commut. +Qed. + +Lemma eval_shift_stack_addressing: + forall F V (ge: Genv.t F V) sp addr vl delta, + eval_addressing ge (Vptr sp Ptrofs.zero) (shift_stack_addressing delta addr) vl = + eval_addressing ge (Vptr sp (Ptrofs.repr delta)) addr vl. +Proof. + intros. unfold eval_addressing. + destruct Archi.ptr64; auto using eval_shift_stack_addressing32, eval_shift_stack_addressing64. Qed. Lemma eval_shift_stack_operation: forall F V (ge: Genv.t F V) sp op vl m delta, - eval_operation ge sp (shift_stack_operation delta op) vl m = - eval_operation ge (Val.add sp (Vint delta)) op vl m. + eval_operation ge (Vptr sp Ptrofs.zero) (shift_stack_operation delta op) vl m = + eval_operation ge (Vptr sp (Ptrofs.repr delta)) op vl m. Proof. - intros. destruct op; simpl; auto. - apply eval_shift_stack_addressing. + intros. destruct op; simpl; auto using eval_shift_stack_addressing32, eval_shift_stack_addressing64. Qed. (** Offset an addressing mode [addr] by a quantity [delta], so that it designates the pointer [delta] bytes past the pointer designated - by [addr]. On PowerPC and ARM, this may be undefined, in which case - [None] is returned. On IA32, it is always defined, but we keep the - same interface. *) + by [addr]. This may be undefined if an offset overflows, in which case + [None] is returned. *) -Definition offset_addressing_total (addr: addressing) (delta: int) : addressing := +Definition offset_addressing_total (addr: addressing) (delta: Z) : addressing := match addr with - | Aindexed n => Aindexed (Int.add n delta) - | Aindexed2 n => Aindexed2 (Int.add n delta) - | Ascaled sc n => Ascaled sc (Int.add n delta) - | Aindexed2scaled sc n => Aindexed2scaled sc (Int.add n delta) - | Aglobal s n => Aglobal s (Int.add n delta) - | Abased s n => Abased s (Int.add n delta) - | Abasedscaled sc s n => Abasedscaled sc s (Int.add n delta) - | Ainstack n => Ainstack (Int.add n delta) + | Aindexed n => Aindexed (n + delta) + | Aindexed2 n => Aindexed2 (n + delta) + | Ascaled sc n => Ascaled sc (n + delta) + | Aindexed2scaled sc n => Aindexed2scaled sc (n + delta) + | Aglobal s n => Aglobal s (Ptrofs.add n (Ptrofs.repr delta)) + | Abased s n => Abased s (Ptrofs.add n (Ptrofs.repr delta)) + | Abasedscaled sc s n => Abasedscaled sc s (Ptrofs.add n (Ptrofs.repr delta)) + | Ainstack n => Ainstack (Ptrofs.add n (Ptrofs.repr delta)) end. -Definition offset_addressing (addr: addressing) (delta: int) : option addressing := - Some(offset_addressing_total addr delta). +Definition offset_addressing (addr: addressing) (delta: Z) : option addressing := + let addr' := offset_addressing_total addr delta in + if addressing_valid addr' then Some addr' else None. -Lemma eval_offset_addressing_total: +Lemma eval_offset_addressing_total_32: forall (F V: Type) (ge: Genv.t F V) sp addr args delta v, - eval_addressing ge sp addr args = Some v -> - eval_addressing ge sp (offset_addressing_total addr delta) args = - Some(Val.add v (Vint delta)). + eval_addressing32 ge sp addr args = Some v -> + eval_addressing32 ge sp (offset_addressing_total addr delta) args = Some(Val.add v (Vint (Int.repr delta))). Proof. - intros. destruct addr; simpl in *; FuncInv; subst. - rewrite Val.add_assoc; auto. - rewrite !Val.add_assoc; auto. - rewrite !Val.add_assoc; auto. - rewrite !Val.add_assoc; auto. - unfold Genv.symbol_address. destruct (Genv.find_symbol ge i); auto. - unfold Genv.symbol_address. destruct (Genv.find_symbol ge i); auto. - rewrite Val.add_assoc. rewrite Val.add_permut. rewrite Val.add_commut. auto. - unfold Genv.symbol_address. destruct (Genv.find_symbol ge i0); auto. - rewrite Val.add_assoc. rewrite Val.add_permut. rewrite Val.add_commut. auto. - rewrite Val.add_assoc. auto. + assert (A: forall x y, Int.add (Int.repr x) (Int.repr y) = Int.repr (x + y)). + { intros. apply Int.eqm_samerepr; auto with ints. } + assert (B: forall delta, Archi.ptr64 = false -> Ptrofs.repr delta = Ptrofs.of_int (Int.repr delta)). + { intros; symmetry; auto with ptrofs. } + intros. destruct addr; simpl in *; FuncInv; subst; simpl. +- rewrite <- A, ! Val.add_assoc; auto. +- rewrite <- A, ! Val.add_assoc; auto. +- rewrite <- A, ! Val.add_assoc; auto. +- rewrite <- A, ! Val.add_assoc; auto. +- rewrite B, Genv.shift_symbol_address_32 by auto. auto. +- rewrite B, Genv.shift_symbol_address_32 by auto. rewrite ! Val.add_assoc. do 2 f_equal. apply Val.add_commut. +- rewrite B, Genv.shift_symbol_address_32 by auto. rewrite ! Val.add_assoc. do 2 f_equal. apply Val.add_commut. +- destruct sp; simpl; auto. rewrite Heqb. rewrite Ptrofs.add_assoc. do 4 f_equal. symmetry; auto with ptrofs. Qed. +Lemma eval_offset_addressing_total_64: + forall (F V: Type) (ge: Genv.t F V) sp addr args delta v, + eval_addressing64 ge sp addr args = Some v -> + eval_addressing64 ge sp (offset_addressing_total addr delta) args = Some(Val.addl v (Vlong (Int64.repr delta))). +Proof. + assert (A: forall x y, Int64.add (Int64.repr x) (Int64.repr y) = Int64.repr (x + y)). + { intros. apply Int64.eqm_samerepr; auto with ints. } + assert (B: forall delta, Archi.ptr64 = true -> Ptrofs.repr delta = Ptrofs.of_int64 (Int64.repr delta)). + { intros; symmetry; auto with ptrofs. } + intros. destruct addr; simpl in *; FuncInv; subst; simpl. +- rewrite <- A, ! Val.addl_assoc; auto. +- rewrite <- A, ! Val.addl_assoc; auto. +- rewrite <- A, ! Val.addl_assoc; auto. +- rewrite <- A, ! Val.addl_assoc; auto. +- rewrite B, Genv.shift_symbol_address_64 by auto. auto. +- destruct sp; simpl; auto. rewrite Heqb. rewrite Ptrofs.add_assoc. do 4 f_equal. symmetry; auto with ptrofs. +Qed. + +(** The following lemma is used only in [Allocproof] in cases where [Archi.ptr64 = false]. *) + Lemma eval_offset_addressing: forall (F V: Type) (ge: Genv.t F V) sp addr args delta addr' v, offset_addressing addr delta = Some addr' -> eval_addressing ge sp addr args = Some v -> - eval_addressing ge sp addr' args = Some(Val.add v (Vint delta)). + Archi.ptr64 = false -> + eval_addressing ge sp addr' args = Some(Val.add v (Vint (Int.repr delta))). Proof. - intros. unfold offset_addressing in H; inv H. - eapply eval_offset_addressing_total; eauto. + intros. unfold offset_addressing in H. destruct (addressing_valid (offset_addressing_total addr delta)); inv H. + unfold eval_addressing in *; rewrite H1 in *. apply eval_offset_addressing_total_32; auto. Qed. (** Operations that are so cheap to recompute that CSE should not factor them out. *) @@ -637,8 +918,11 @@ Definition is_trivial_op (op: operation) : bool := match op with | Omove => true | Ointconst _ => true + | Olongconst _ => true | Olea (Aglobal _ _) => true | Olea (Ainstack _) => true + | Oleal (Aglobal _ _) => true + | Oleal (Ainstack _) => true | _ => false end. @@ -646,8 +930,10 @@ Definition is_trivial_op (op: operation) : bool := Definition op_depends_on_memory (op: operation) : bool := match op with - | Ocmp (Ccompu _) => true - | Ocmp (Ccompuimm _ _) => true + | Ocmp (Ccompu _) => negb Archi.ptr64 + | Ocmp (Ccompuimm _ _) => negb Archi.ptr64 + | Ocmp (Ccomplu _) => Archi.ptr64 + | Ocmp (Ccompluimm _ _) => Archi.ptr64 | _ => false end. @@ -657,7 +943,8 @@ Lemma op_depends_on_memory_correct: eval_operation ge sp op args m1 = eval_operation ge sp op args m2. Proof. intros until m2. destruct op; simpl; try congruence. - destruct c; simpl; auto; congruence. + destruct cond; simpl; intros SF; auto; rewrite ? negb_false_iff in SF; + unfold Val.cmpu_bool, Val.cmplu_bool; rewrite SF; reflexivity. Qed. (** Global variables mentioned in an operation or addressing mode *) @@ -674,6 +961,7 @@ Definition globals_operation (op: operation) : list ident := match op with | Oindirectsymbol s => s :: nil | Olea addr => globals_addressing addr + | Oleal addr => globals_addressing addr | _ => nil end. @@ -692,13 +980,30 @@ Variable ge2: Genv.t F2 V2. Hypothesis agree_on_symbols: forall (s: ident), Genv.find_symbol ge2 s = Genv.find_symbol ge1 s. +Lemma eval_addressing32_preserved: + forall sp addr vl, + eval_addressing32 ge2 sp addr vl = eval_addressing32 ge1 sp addr vl. +Proof. + intros. + unfold eval_addressing32, Genv.symbol_address; destruct addr; try rewrite agree_on_symbols; + reflexivity. +Qed. + +Lemma eval_addressing64_preserved: + forall sp addr vl, + eval_addressing64 ge2 sp addr vl = eval_addressing64 ge1 sp addr vl. +Proof. + intros. + unfold eval_addressing64, Genv.symbol_address; destruct addr; try rewrite agree_on_symbols; + reflexivity. +Qed. + Lemma eval_addressing_preserved: forall sp addr vl, eval_addressing ge2 sp addr vl = eval_addressing ge1 sp addr vl. Proof. intros. - unfold eval_addressing, Genv.symbol_address; destruct addr; try rewrite agree_on_symbols; - reflexivity. + unfold eval_addressing; destruct Archi.ptr64; auto using eval_addressing32_preserved, eval_addressing64_preserved. Qed. Lemma eval_operation_preserved: @@ -708,7 +1013,8 @@ Proof. intros. unfold eval_operation; destruct op; auto. unfold Genv.symbol_address. rewrite agree_on_symbols. auto. - apply eval_addressing_preserved. + apply eval_addressing32_preserved. + apply eval_addressing64_preserved. Qed. End GENV_TRANSF. @@ -728,30 +1034,30 @@ Variable m2: mem. Hypothesis valid_pointer_inj: forall b1 ofs b2 delta, f b1 = Some(b2, delta) -> - Mem.valid_pointer m1 b1 (Int.unsigned ofs) = true -> - Mem.valid_pointer m2 b2 (Int.unsigned (Int.add ofs (Int.repr delta))) = true. + Mem.valid_pointer m1 b1 (Ptrofs.unsigned ofs) = true -> + Mem.valid_pointer m2 b2 (Ptrofs.unsigned (Ptrofs.add ofs (Ptrofs.repr delta))) = true. Hypothesis weak_valid_pointer_inj: forall b1 ofs b2 delta, f b1 = Some(b2, delta) -> - Mem.weak_valid_pointer m1 b1 (Int.unsigned ofs) = true -> - Mem.weak_valid_pointer m2 b2 (Int.unsigned (Int.add ofs (Int.repr delta))) = true. + Mem.weak_valid_pointer m1 b1 (Ptrofs.unsigned ofs) = true -> + Mem.weak_valid_pointer m2 b2 (Ptrofs.unsigned (Ptrofs.add ofs (Ptrofs.repr delta))) = true. Hypothesis weak_valid_pointer_no_overflow: forall b1 ofs b2 delta, f b1 = Some(b2, delta) -> - Mem.weak_valid_pointer m1 b1 (Int.unsigned ofs) = true -> - 0 <= Int.unsigned ofs + Int.unsigned (Int.repr delta) <= Int.max_unsigned. + Mem.weak_valid_pointer m1 b1 (Ptrofs.unsigned ofs) = true -> + 0 <= Ptrofs.unsigned ofs + Ptrofs.unsigned (Ptrofs.repr delta) <= Ptrofs.max_unsigned. Hypothesis valid_different_pointers_inj: forall b1 ofs1 b2 ofs2 b1' delta1 b2' delta2, b1 <> b2 -> - Mem.valid_pointer m1 b1 (Int.unsigned ofs1) = true -> - Mem.valid_pointer m1 b2 (Int.unsigned ofs2) = true -> + Mem.valid_pointer m1 b1 (Ptrofs.unsigned ofs1) = true -> + Mem.valid_pointer m1 b2 (Ptrofs.unsigned ofs2) = true -> f b1 = Some (b1', delta1) -> f b2 = Some (b2', delta2) -> b1' <> b2' \/ - Int.unsigned (Int.add ofs1 (Int.repr delta1)) <> Int.unsigned (Int.add ofs2 (Int.repr delta2)). + Ptrofs.unsigned (Ptrofs.add ofs1 (Ptrofs.repr delta1)) <> Ptrofs.unsigned (Ptrofs.add ofs2 (Ptrofs.repr delta2)). Ltac InvInject := match goal with @@ -775,16 +1081,20 @@ Lemma eval_condition_inj: eval_condition cond vl2 m2 = Some b. Proof. intros. destruct cond; simpl in H0; FuncInv; InvInject; simpl; auto. - inv H3; inv H2; simpl in H0; inv H0; auto. - eauto 3 using Val.cmpu_bool_inject, Mem.valid_pointer_implies. - inv H3; simpl in H0; inv H0; auto. - eauto 3 using Val.cmpu_bool_inject, Mem.valid_pointer_implies. - inv H3; inv H2; simpl in H0; inv H0; auto. - inv H3; inv H2; simpl in H0; inv H0; auto. - inv H3; inv H2; simpl in H0; inv H0; auto. - inv H3; inv H2; simpl in H0; inv H0; auto. - inv H3; try discriminate; auto. - inv H3; try discriminate; auto. +- inv H3; inv H2; simpl in H0; inv H0; auto. +- eauto 3 using Val.cmpu_bool_inject, Mem.valid_pointer_implies. +- inv H3; simpl in H0; inv H0; auto. +- eauto 3 using Val.cmpu_bool_inject, Mem.valid_pointer_implies. +- inv H3; inv H2; simpl in H0; inv H0; auto. +- eauto 3 using Val.cmplu_bool_inject, Mem.valid_pointer_implies. +- inv H3; simpl in H0; inv H0; auto. +- eauto 3 using Val.cmplu_bool_inject, Mem.valid_pointer_implies. +- inv H3; inv H2; simpl in H0; inv H0; auto. +- inv H3; inv H2; simpl in H0; inv H0; auto. +- inv H3; inv H2; simpl in H0; inv H0; auto. +- inv H3; inv H2; simpl in H0; inv H0; auto. +- inv H3; try discriminate; auto. +- inv H3; try discriminate; auto. Qed. Ltac TrivialExists := @@ -794,6 +1104,36 @@ Ltac TrivialExists := | _ => idtac end. +Lemma eval_addressing32_inj: + forall addr sp1 vl1 sp2 vl2 v1, + (forall id ofs, + In id (globals_addressing addr) -> + Val.inject f (Genv.symbol_address ge1 id ofs) (Genv.symbol_address ge2 id ofs)) -> + Val.inject f sp1 sp2 -> + Val.inject_list f vl1 vl2 -> + eval_addressing32 ge1 sp1 addr vl1 = Some v1 -> + exists v2, eval_addressing32 ge2 sp2 addr vl2 = Some v2 /\ Val.inject f v1 v2. +Proof. + assert (A: forall v1 v2 v1' v2', Val.inject f v1 v1' -> Val.inject f v2 v2' -> Val.inject f (Val.mul v1 v2) (Val.mul v1' v2')). + { intros. inv H; simpl; auto. inv H0; auto. } + intros. destruct addr; simpl in *; FuncInv; InvInject; TrivialExists; eauto using Val.add_inject, Val.offset_ptr_inject with coqlib. +Qed. + +Lemma eval_addressing64_inj: + forall addr sp1 vl1 sp2 vl2 v1, + (forall id ofs, + In id (globals_addressing addr) -> + Val.inject f (Genv.symbol_address ge1 id ofs) (Genv.symbol_address ge2 id ofs)) -> + Val.inject f sp1 sp2 -> + Val.inject_list f vl1 vl2 -> + eval_addressing64 ge1 sp1 addr vl1 = Some v1 -> + exists v2, eval_addressing64 ge2 sp2 addr vl2 = Some v2 /\ Val.inject f v1 v2. +Proof. + assert (A: forall v1 v2 v1' v2', Val.inject f v1 v1' -> Val.inject f v2 v2' -> Val.inject f (Val.mull v1 v2) (Val.mull v1' v2')). + { intros. inv H; simpl; auto. inv H0; auto. } + intros. destruct addr; simpl in *; FuncInv; InvInject; TrivialExists; eauto using Val.addl_inject, Val.offset_ptr_inject with coqlib. +Qed. + Lemma eval_addressing_inj: forall addr sp1 vl1 sp2 vl2 v1, (forall id ofs, @@ -804,15 +1144,7 @@ Lemma eval_addressing_inj: eval_addressing ge1 sp1 addr vl1 = Some v1 -> exists v2, eval_addressing ge2 sp2 addr vl2 = Some v2 /\ Val.inject f v1 v2. Proof. - intros. destruct addr; simpl in H2; simpl; FuncInv; InvInject; TrivialExists. - apply Values.Val.add_inject; auto. - apply Values.Val.add_inject; auto. apply Values.Val.add_inject; auto. - apply Values.Val.add_inject; auto. inv H5; simpl; auto. - apply Values.Val.add_inject; auto. apply Values.Val.add_inject; auto. inv H3; simpl; auto. - apply H; simpl; auto. - apply Values.Val.add_inject; auto. apply H; simpl; auto. - apply Values.Val.add_inject; auto. apply H; simpl; auto. inv H5; simpl; auto. - apply Values.Val.add_inject; auto. + unfold eval_addressing; intros. destruct Archi.ptr64; eauto using eval_addressing32_inj, eval_addressing64_inj. Qed. Lemma eval_operation_inj: @@ -832,10 +1164,7 @@ Proof. inv H4; simpl; auto. inv H4; simpl; auto. inv H4; simpl; auto. - inv H4; inv H2; simpl; auto. econstructor; eauto. - rewrite Int.sub_add_l. auto. - destruct (eq_block b1 b0); auto. subst. rewrite H1 in H0. inv H0. rewrite dec_eq_true. - rewrite Int.sub_shifted. auto. + apply Val.sub_inject; auto. inv H4; inv H2; simpl; auto. inv H4; simpl; auto. inv H4; inv H2; simpl; auto. @@ -856,17 +1185,50 @@ Proof. inv H4; simpl; auto. inv H4; simpl; auto. inv H4; inv H2; simpl; auto. destruct (Int.ltu i0 Int.iwordsize); auto. - inv H4; simpl; auto. destruct (Int.ltu i Int.iwordsize); auto. + inv H4; simpl; auto. destruct (Int.ltu n Int.iwordsize); auto. inv H4; inv H2; simpl; auto. destruct (Int.ltu i0 Int.iwordsize); auto. - inv H4; simpl; auto. destruct (Int.ltu i Int.iwordsize); auto. + inv H4; simpl; auto. destruct (Int.ltu n Int.iwordsize); auto. inv H4; simpl in H1; try discriminate. simpl. - destruct (Int.ltu i (Int.repr 31)); inv H1. TrivialExists. + destruct (Int.ltu n (Int.repr 31)); inv H1. TrivialExists. inv H4; inv H2; simpl; auto. destruct (Int.ltu i0 Int.iwordsize); auto. - inv H4; simpl; auto. destruct (Int.ltu i Int.iwordsize); auto. + inv H4; simpl; auto. destruct (Int.ltu n Int.iwordsize); auto. + inv H4; simpl; auto. + inv H4; simpl; auto. destruct (Int.ltu n Int.iwordsize); auto. + inv H2; simpl; auto. destruct (Int.ltu (Int.sub Int.iwordsize n) Int.iwordsize); auto. + eapply eval_addressing32_inj; eauto. + inv H4; inv H2; simpl; auto. + inv H4; simpl; auto. + inv H4; simpl; auto. + inv H4; simpl; auto. inv H4; simpl; auto. - inv H4; simpl; auto. destruct (Int.ltu i Int.iwordsize); auto. - inv H2; simpl; auto. destruct (Int.ltu (Int.sub Int.iwordsize i) Int.iwordsize); auto. - eapply eval_addressing_inj; eauto. + inv H4; simpl; auto. + apply Val.addl_inject; auto. + apply Val.subl_inject; auto. + inv H4; inv H2; simpl; auto. + inv H4; simpl; auto. + inv H4; inv H3; simpl in H1; inv H1. simpl. + destruct (Int64.eq i0 Int64.zero || Int64.eq i (Int64.repr Int64.min_signed) && Int64.eq i0 Int64.mone); inv H2. TrivialExists. + inv H4; inv H3; simpl in H1; inv H1. simpl. + destruct (Int64.eq i0 Int64.zero); inv H2. TrivialExists. + inv H4; inv H3; simpl in H1; inv H1. simpl. + destruct (Int64.eq i0 Int64.zero || Int64.eq i (Int64.repr Int64.min_signed) && Int64.eq i0 Int64.mone); inv H2. TrivialExists. + inv H4; inv H3; simpl in H1; inv H1. simpl. + destruct (Int64.eq i0 Int64.zero); inv H2. TrivialExists. + inv H4; inv H2; simpl; auto. + inv H4; simpl; auto. + inv H4; inv H2; simpl; auto. + inv H4; simpl; auto. + inv H4; inv H2; simpl; auto. + inv H4; simpl; auto. + inv H4; simpl; auto. + inv H4; inv H2; simpl; auto. destruct (Int.ltu i0 Int64.iwordsize'); auto. + inv H4; simpl; auto. destruct (Int.ltu n Int64.iwordsize'); auto. + inv H4; inv H2; simpl; auto. destruct (Int.ltu i0 Int64.iwordsize'); auto. + inv H4; simpl; auto. destruct (Int.ltu n Int64.iwordsize'); auto. + inv H4; inv H2; simpl; auto. destruct (Int.ltu i0 Int64.iwordsize'); auto. + inv H4; simpl; auto. destruct (Int.ltu n Int64.iwordsize'); auto. + inv H4; simpl; auto. + eapply eval_addressing64_inj; eauto. inv H4; simpl; auto. inv H4; simpl; auto. inv H4; inv H2; simpl; auto. @@ -887,10 +1249,13 @@ Proof. inv H4; simpl in H1; inv H1. simpl. destruct (Float32.to_int f0); simpl in H2; inv H2. exists (Vint i); auto. inv H4; simpl in H1; inv H1. simpl. TrivialExists. - inv H4; inv H2; simpl; auto. - inv H4; simpl; auto. - inv H4; simpl; auto. - subst v1. destruct (eval_condition c vl1 m1) eqn:?. + inv H4; simpl in H1; inv H1. simpl. destruct (Float.to_long f0); simpl in H2; inv H2. + exists (Vlong i); auto. + inv H4; simpl in H1; inv H1. simpl. TrivialExists. + inv H4; simpl in H1; inv H1. simpl. destruct (Float32.to_long f0); simpl in H2; inv H2. + exists (Vlong i); auto. + inv H4; simpl in H1; inv H1. simpl. TrivialExists. + subst v1. destruct (eval_condition cond vl1 m1) eqn:?. exploit eval_condition_inj; eauto. intros EQ; rewrite EQ. destruct b; simpl; constructor. simpl; constructor. @@ -909,40 +1274,40 @@ Remark valid_pointer_extends: forall m1 m2, Mem.extends m1 m2 -> forall b1 ofs b2 delta, Some(b1, 0) = Some(b2, delta) -> - Mem.valid_pointer m1 b1 (Int.unsigned ofs) = true -> - Mem.valid_pointer m2 b2 (Int.unsigned (Int.add ofs (Int.repr delta))) = true. + Mem.valid_pointer m1 b1 (Ptrofs.unsigned ofs) = true -> + Mem.valid_pointer m2 b2 (Ptrofs.unsigned (Ptrofs.add ofs (Ptrofs.repr delta))) = true. Proof. - intros. inv H0. rewrite Int.add_zero. eapply Mem.valid_pointer_extends; eauto. + intros. inv H0. rewrite Ptrofs.add_zero. eapply Mem.valid_pointer_extends; eauto. Qed. Remark weak_valid_pointer_extends: forall m1 m2, Mem.extends m1 m2 -> forall b1 ofs b2 delta, Some(b1, 0) = Some(b2, delta) -> - Mem.weak_valid_pointer m1 b1 (Int.unsigned ofs) = true -> - Mem.weak_valid_pointer m2 b2 (Int.unsigned (Int.add ofs (Int.repr delta))) = true. + Mem.weak_valid_pointer m1 b1 (Ptrofs.unsigned ofs) = true -> + Mem.weak_valid_pointer m2 b2 (Ptrofs.unsigned (Ptrofs.add ofs (Ptrofs.repr delta))) = true. Proof. - intros. inv H0. rewrite Int.add_zero. eapply Mem.weak_valid_pointer_extends; eauto. + intros. inv H0. rewrite Ptrofs.add_zero. eapply Mem.weak_valid_pointer_extends; eauto. Qed. Remark weak_valid_pointer_no_overflow_extends: forall m1 b1 ofs b2 delta, Some(b1, 0) = Some(b2, delta) -> - Mem.weak_valid_pointer m1 b1 (Int.unsigned ofs) = true -> - 0 <= Int.unsigned ofs + Int.unsigned (Int.repr delta) <= Int.max_unsigned. + Mem.weak_valid_pointer m1 b1 (Ptrofs.unsigned ofs) = true -> + 0 <= Ptrofs.unsigned ofs + Ptrofs.unsigned (Ptrofs.repr delta) <= Ptrofs.max_unsigned. Proof. - intros. inv H. rewrite Zplus_0_r. apply Int.unsigned_range_2. + intros. inv H. rewrite Zplus_0_r. apply Ptrofs.unsigned_range_2. Qed. Remark valid_different_pointers_extends: forall m1 b1 ofs1 b2 ofs2 b1' delta1 b2' delta2, b1 <> b2 -> - Mem.valid_pointer m1 b1 (Int.unsigned ofs1) = true -> - Mem.valid_pointer m1 b2 (Int.unsigned ofs2) = true -> + Mem.valid_pointer m1 b1 (Ptrofs.unsigned ofs1) = true -> + Mem.valid_pointer m1 b2 (Ptrofs.unsigned ofs2) = true -> Some(b1, 0) = Some (b1', delta1) -> Some(b2, 0) = Some (b2', delta2) -> b1' <> b2' \/ - Int.unsigned(Int.add ofs1 (Int.repr delta1)) <> Int.unsigned(Int.add ofs2 (Int.repr delta2)). + Ptrofs.unsigned(Ptrofs.add ofs1 (Ptrofs.repr delta1)) <> Ptrofs.unsigned(Ptrofs.add ofs2 (Ptrofs.repr delta2)). Proof. intros. inv H2; inv H3. auto. Qed. @@ -1022,7 +1387,7 @@ Remark symbol_address_inject: Proof. intros. unfold Genv.symbol_address. destruct (Genv.find_symbol genv id) eqn:?; auto. exploit (proj1 globals); eauto. intros. - econstructor; eauto. rewrite Int.add_zero; auto. + econstructor; eauto. rewrite Ptrofs.add_zero; auto. Qed. Lemma eval_condition_inject: @@ -1042,34 +1407,36 @@ Qed. Lemma eval_addressing_inject: forall addr vl1 vl2 v1, Val.inject_list f vl1 vl2 -> - eval_addressing genv (Vptr sp1 Int.zero) addr vl1 = Some v1 -> + eval_addressing genv (Vptr sp1 Ptrofs.zero) addr vl1 = Some v1 -> exists v2, - eval_addressing genv (Vptr sp2 Int.zero) (shift_stack_addressing (Int.repr delta) addr) vl2 = Some v2 + eval_addressing genv (Vptr sp2 Ptrofs.zero) (shift_stack_addressing delta addr) vl2 = Some v2 /\ Val.inject f v1 v2. Proof. intros. - rewrite eval_shift_stack_addressing. simpl. - eapply eval_addressing_inj with (sp1 := Vptr sp1 Int.zero); eauto. + rewrite eval_shift_stack_addressing. + eapply eval_addressing_inj with (sp1 := Vptr sp1 Ptrofs.zero); eauto. intros. apply symbol_address_inject. + econstructor; eauto. rewrite Ptrofs.add_zero_l; auto. Qed. Lemma eval_operation_inject: forall op vl1 vl2 v1 m1 m2, Val.inject_list f vl1 vl2 -> Mem.inject f m1 m2 -> - eval_operation genv (Vptr sp1 Int.zero) op vl1 m1 = Some v1 -> + eval_operation genv (Vptr sp1 Ptrofs.zero) op vl1 m1 = Some v1 -> exists v2, - eval_operation genv (Vptr sp2 Int.zero) (shift_stack_operation (Int.repr delta) op) vl2 m2 = Some v2 + eval_operation genv (Vptr sp2 Ptrofs.zero) (shift_stack_operation delta op) vl2 m2 = Some v2 /\ Val.inject f v1 v2. Proof. intros. rewrite eval_shift_stack_operation. simpl. - eapply eval_operation_inj with (sp1 := Vptr sp1 Int.zero) (m1 := m1); eauto. + eapply eval_operation_inj with (sp1 := Vptr sp1 Ptrofs.zero) (m1 := m1); eauto. intros; eapply Mem.valid_pointer_inject_val; eauto. intros; eapply Mem.weak_valid_pointer_inject_val; eauto. intros; eapply Mem.weak_valid_pointer_inject_no_overflow; eauto. intros; eapply Mem.different_pointers_inject; eauto. intros. apply symbol_address_inject. + econstructor; eauto. rewrite Ptrofs.add_zero_l; auto. Qed. End EVAL_INJECT. -- cgit