diff options
author | Xavier Leroy <xavier.leroy@inria.fr> | 2016-10-01 17:25:18 +0200 |
---|---|---|
committer | Xavier Leroy <xavier.leroy@inria.fr> | 2016-10-01 17:25:18 +0200 |
commit | e637d041c5c2ee3a3ed395a7dab6c9101e8eb16c (patch) | |
tree | 518d558674d3e1c6ff41c46d84c784e727ed5d04 /cfrontend/Cop.v | |
parent | ad2a2c862abef3aee701d1bca0524fcbf2d07b30 (diff) | |
download | compcert-e637d041c5c2ee3a3ed395a7dab6c9101e8eb16c.tar.gz compcert-e637d041c5c2ee3a3ed395a7dab6c9101e8eb16c.zip |
Support for 64-bit architectures: generic support
- Introduce Archi.ptr64 parameter.
- Define module Ptrofs of integers as wide as a pointer (64 if Archi.ptr64, 32 otherwise).
- Use Ptrofs.int as the offset type for Vptr values and anywhere pointer offsets are manipulated.
- Modify Val operations that handle pointers (e.g. Val.add, Val.sub, Val.cmpu) so that in 64-bit pointer mode it is the "long" operation (e.g. Val.addl, Val.subl, Val.cmplu) that handles pointers.
- Update the memory model accordingly.
- Modify C operations that handle pointers (e.g. addition, subtraction, comparisons) accordingly.
- Make it possible to turn off the splitting of 64-bit integers into pairs of 32-bit integers.
- Update the compiler front-end and back-end accordingly.
Diffstat (limited to 'cfrontend/Cop.v')
-rw-r--r-- | cfrontend/Cop.v | 605 |
1 files changed, 327 insertions, 278 deletions
diff --git a/cfrontend/Cop.v b/cfrontend/Cop.v index 4ac56b04..8defd9d9 100644 --- a/cfrontend/Cop.v +++ b/cfrontend/Cop.v @@ -22,6 +22,7 @@ Require Import Floats. Require Import Values. Require Import Memory. Require Import Ctypes. +Require Archi. (** * Syntax of operators. *) @@ -72,7 +73,7 @@ Inductive incr_or_decr : Type := Incr | Decr. (** ** Casts and truth values *) Inductive classify_cast_cases : Type := - | cast_case_neutral (**r int|pointer -> int32|pointer *) + | cast_case_pointer (**r between pointer types or intptr_t types *) | cast_case_i2i (sz2:intsize) (si2:signedness) (**r int -> int *) | cast_case_f2f (**r double -> double *) | cast_case_s2s (**r single -> single *) @@ -89,10 +90,10 @@ Inductive classify_cast_cases : Type := | cast_case_l2s (si1: signedness) (**r long -> single *) | cast_case_f2l (si2:signedness) (**r double -> long *) | cast_case_s2l (si2:signedness) (**r single -> long *) + | cast_case_i2bool (**r int -> bool *) + | cast_case_l2bool (**r long -> bool *) | cast_case_f2bool (**r double -> bool *) | cast_case_s2bool (**r single -> bool *) - | cast_case_l2bool (**r long -> bool *) - | cast_case_p2bool (**r pointer -> bool *) | cast_case_struct (id1 id2: ident) (**r struct -> struct *) | cast_case_union (id1 id2: ident) (**r union -> union *) | cast_case_void (**r any -> void *) @@ -100,33 +101,54 @@ Inductive classify_cast_cases : Type := Definition classify_cast (tfrom tto: type) : classify_cast_cases := match tto, tfrom with - | Tint I32 si2 _, (Tint _ _ _ | Tpointer _ _ | Tarray _ _ _ | Tfunction _ _ _) => cast_case_neutral + (* To [void] *) + | Tvoid, _ => cast_case_void + (* To [_Bool] *) + | Tint IBool _ _, Tint _ _ _ => cast_case_i2bool + | Tint IBool _ _, Tlong _ _ => cast_case_l2bool | Tint IBool _ _, Tfloat F64 _ => cast_case_f2bool | Tint IBool _ _, Tfloat F32 _ => cast_case_s2bool - | Tint IBool _ _, (Tpointer _ _ | Tarray _ _ _ | Tfunction _ _ _) => cast_case_p2bool - | Tint sz2 si2 _, Tint sz1 si1 _ => cast_case_i2i sz2 si2 + | Tint IBool _ _, (Tpointer _ _ | Tarray _ _ _ | Tfunction _ _ _) => + if Archi.ptr64 then cast_case_l2bool else cast_case_i2bool + (* To [int] other than [_Bool] *) + | Tint sz2 si2 _, Tint _ _ _ => + if Archi.ptr64 then cast_case_i2i sz2 si2 + else if intsize_eq sz2 I32 then cast_case_pointer + else cast_case_i2i sz2 si2 + | Tint sz2 si2 _, Tlong _ _ => cast_case_l2i sz2 si2 | Tint sz2 si2 _, Tfloat F64 _ => cast_case_f2i sz2 si2 | Tint sz2 si2 _, Tfloat F32 _ => cast_case_s2i sz2 si2 - | Tfloat F64 _, Tfloat F64 _ => cast_case_f2f - | Tfloat F32 _, Tfloat F32 _ => cast_case_s2s - | Tfloat F64 _, Tfloat F32 _ => cast_case_s2f - | Tfloat F32 _, Tfloat F64 _ => cast_case_f2s - | Tfloat F64 _, Tint sz1 si1 _ => cast_case_i2f si1 - | Tfloat F32 _, Tint sz1 si1 _ => cast_case_i2s si1 - | Tpointer _ _, (Tint _ _ _ | Tpointer _ _ | Tarray _ _ _ | Tfunction _ _ _) => cast_case_neutral - | Tlong _ _, Tlong _ _ => cast_case_l2l + | Tint sz2 si2 _, (Tpointer _ _ | Tarray _ _ _ | Tfunction _ _ _) => + if Archi.ptr64 then cast_case_l2i sz2 si2 + else if intsize_eq sz2 I32 then cast_case_pointer + else cast_case_i2i sz2 si2 + (* To [long] *) + | Tlong _ _, Tlong _ _ => + if Archi.ptr64 then cast_case_pointer else cast_case_l2l | Tlong _ _, Tint sz1 si1 _ => cast_case_i2l si1 - | Tint IBool _ _, Tlong _ _ => cast_case_l2bool - | Tint sz2 si2 _, Tlong _ _ => cast_case_l2i sz2 si2 | Tlong si2 _, Tfloat F64 _ => cast_case_f2l si2 | Tlong si2 _, Tfloat F32 _ => cast_case_s2l si2 + | Tlong si2 _, (Tpointer _ _ | Tarray _ _ _ | Tfunction _ _ _) => + if Archi.ptr64 then cast_case_pointer else cast_case_i2l si2 + (* To [float] *) + | Tfloat F64 _, Tint sz1 si1 _ => cast_case_i2f si1 + | Tfloat F32 _, Tint sz1 si1 _ => cast_case_i2s si1 | Tfloat F64 _, Tlong si1 _ => cast_case_l2f si1 | Tfloat F32 _, Tlong si1 _ => cast_case_l2s si1 - | Tpointer _ _, Tlong _ _ => cast_case_l2i I32 Unsigned - | Tlong si2 _, (Tpointer _ _ | Tarray _ _ _ | Tfunction _ _ _) => cast_case_i2l si2 + | Tfloat F64 _, Tfloat F64 _ => cast_case_f2f + | Tfloat F32 _, Tfloat F32 _ => cast_case_s2s + | Tfloat F64 _, Tfloat F32 _ => cast_case_s2f + | Tfloat F32 _, Tfloat F64 _ => cast_case_f2s + (* To pointer types *) + | Tpointer _ _, Tint _ _ _ => + if Archi.ptr64 then cast_case_i2l Unsigned else cast_case_pointer + | Tpointer _ _, Tlong _ _ => + if Archi.ptr64 then cast_case_pointer else cast_case_l2i I32 Unsigned + | Tpointer _ _, (Tpointer _ _ | Tarray _ _ _ | Tfunction _ _ _) => cast_case_pointer + (* To struct or union types *) | Tstruct id2 _, Tstruct id1 _ => cast_case_struct id1 id2 | Tunion id2 _, Tunion id1 _ => cast_case_union id1 id2 - | Tvoid, _ => cast_case_void + (* Catch-all *) | _, _ => cast_case_default end. @@ -200,9 +222,11 @@ Definition cast_single_long (si : signedness) (f: float32) : option int64 := Definition sem_cast (v: val) (t1 t2: type) (m: mem): option val := match classify_cast t1 t2 with - | cast_case_neutral => + | cast_case_pointer => match v with - | Vint _ | Vptr _ _ => Some v + | Vptr _ _ => Some v + | Vint _ => if Archi.ptr64 then None else Some v + | Vlong _ => if Archi.ptr64 then Some v else None | _ => None end | cast_case_i2i sz2 si2 => @@ -258,6 +282,25 @@ Definition sem_cast (v: val) (t1 t2: type) (m: mem): option val := end | _ => None end + | cast_case_i2bool => + match v with + | Vint n => + Some(Vint(if Int.eq n Int.zero then Int.zero else Int.one)) + | Vptr b ofs => + if Archi.ptr64 then None else + if Mem.weak_valid_pointer m b (Ptrofs.unsigned ofs) then Some Vone else None + | _ => None + end + | cast_case_l2bool => + match v with + | Vlong n => + Some(Vint(if Int64.eq n Int64.zero then Int.zero else Int.one)) + | Vptr b ofs => + if negb Archi.ptr64 then None else + if Mem.weak_valid_pointer m b (Ptrofs.unsigned ofs) then Some Vone else None + + | _ => None + end | cast_case_f2bool => match v with | Vfloat f => @@ -270,12 +313,6 @@ Definition sem_cast (v: val) (t1 t2: type) (m: mem): option val := Some(Vint(if Float32.cmp Ceq f Float32.zero then Int.zero else Int.one)) | _ => None end - | cast_case_p2bool => - match v with - | Vint i => Some (Vint (cast_int_int IBool Signed i)) - | Vptr b ofs => if Mem.weak_valid_pointer m b (Int.unsigned ofs) then Some Vone else None - | _ => None - end | cast_case_l2l => match v with | Vlong n => Some (Vlong n) @@ -291,12 +328,6 @@ Definition sem_cast (v: val) (t1 t2: type) (m: mem): option val := | Vlong n => Some(Vint (cast_int_int sz si (Int.repr (Int64.unsigned n)))) | _ => None end - | cast_case_l2bool => - match v with - | Vlong n => - Some(Vint(if Int64.eq n Int64.zero then Int.zero else Int.one)) - | _ => None - end | cast_case_l2f si1 => match v with | Vlong i => Some (Vfloat (cast_long_float si1 i)) @@ -350,16 +381,15 @@ Definition sem_cast (v: val) (t1 t2: type) (m: mem): option val := Inductive classify_bool_cases : Type := | bool_case_i (**r integer *) + | bool_case_l (**r long *) | bool_case_f (**r double float *) | bool_case_s (**r single float *) - | bool_case_p (**r pointer *) - | bool_case_l (**r long *) | bool_default. Definition classify_bool (ty: type) : classify_bool_cases := match typeconv ty with | Tint _ _ _ => bool_case_i - | Tpointer _ _ => bool_case_p + | Tpointer _ _ => if Archi.ptr64 then bool_case_l else bool_case_i | Tfloat F64 _ => bool_case_f | Tfloat F32 _ => bool_case_s | Tlong _ _ => bool_case_l @@ -376,6 +406,17 @@ Definition bool_val (v: val) (t: type) (m: mem) : option bool := | bool_case_i => match v with | Vint n => Some (negb (Int.eq n Int.zero)) + | Vptr b ofs => + if Archi.ptr64 then None else + if Mem.weak_valid_pointer m b (Ptrofs.unsigned ofs) then Some true else None + | _ => None + end + | bool_case_l => + match v with + | Vlong n => Some (negb (Int64.eq n Int64.zero)) + | Vptr b ofs => + if negb Archi.ptr64 then None else + if Mem.weak_valid_pointer m b (Ptrofs.unsigned ofs) then Some true else None | _ => None end | bool_case_f => @@ -388,17 +429,6 @@ Definition bool_val (v: val) (t: type) (m: mem) : option bool := | Vsingle f => Some (negb (Float32.cmp Ceq f Float32.zero)) | _ => None end - | bool_case_p => - match v with - | Vint n => Some (negb (Int.eq n Int.zero)) - | Vptr b ofs => if Mem.weak_valid_pointer m b (Int.unsigned ofs) then Some true else None - | _ => None - end - | bool_case_l => - match v with - | Vlong n => Some (negb (Int64.eq n Int64.zero)) - | _ => None - end | bool_default => None end. @@ -407,35 +437,7 @@ Definition bool_val (v: val) (t: type) (m: mem) : option bool := (** *** Boolean negation *) Definition sem_notbool (v: val) (ty: type) (m: mem): option val := - match classify_bool ty with - | bool_case_i => - match v with - | Vint n => Some (Val.of_bool (Int.eq n Int.zero)) - | _ => None - end - | bool_case_f => - match v with - | Vfloat f => Some (Val.of_bool (Float.cmp Ceq f Float.zero)) - | _ => None - end - | bool_case_s => - match v with - | Vsingle f => Some (Val.of_bool (Float32.cmp Ceq f Float32.zero)) - | _ => None - end - | bool_case_p => - match v with - | Vint n => Some (Val.of_bool (Int.eq n Int.zero)) - | Vptr b ofs => if Mem.weak_valid_pointer m b (Int.unsigned ofs) then Some Vfalse else None - | _ => None - end - | bool_case_l => - match v with - | Vlong n => Some (Val.of_bool (Int64.eq n Int64.zero)) - | _ => None - end - | bool_default => None - end. + option_map (fun b => Val.of_bool (negb b)) (bool_val v ty m). (** *** Opposite and absolute value *) @@ -623,57 +625,55 @@ Definition sem_binarith (** *** Addition *) Inductive classify_add_cases : Type := - | add_case_pi(ty: type) (**r pointer, int *) - | add_case_ip(ty: type) (**r int, pointer *) - | add_case_pl(ty: type) (**r pointer, long *) - | add_case_lp(ty: type) (**r long, pointer *) - | add_default. (**r numerical type, numerical type *) + | add_case_pi (ty: type) (si: signedness) (**r pointer, int *) + | add_case_pl (ty: type) (**r pointer, long *) +(* + | add_case_ip (si: signedness) (ty: type) (**r int, pointer *) + | add_case_lp (ty: type) (**r long, pointer *) +*) + | add_default. (**r numerical type, numerical type *) Definition classify_add (ty1: type) (ty2: type) := match typeconv ty1, typeconv ty2 with - | Tpointer ty _, Tint _ _ _ => add_case_pi ty - | Tint _ _ _, Tpointer ty _ => add_case_ip ty + | Tpointer ty _, Tint _ si _ => add_case_pi ty si | Tpointer ty _, Tlong _ _ => add_case_pl ty +(* + | Tint _ si _, Tpointer ty _ => add_case_ip si ty | Tlong _ _, Tpointer ty _ => add_case_lp ty +*) | _, _ => add_default end. +Definition ptrofs_of_int (si: signedness) (n: int) : ptrofs := + match si with + | Signed => Ptrofs.of_ints n + | Unsigned => Ptrofs.of_intu n + end. + Definition sem_add (cenv: composite_env) (v1:val) (t1:type) (v2: val) (t2:type) (m: mem): option val := match classify_add t1 t2 with - | add_case_pi ty => (**r pointer plus integer *) - match v1,v2 with + | add_case_pi ty si => (**r pointer plus integer *) + match v1, v2 with | Vptr b1 ofs1, Vint n2 => - Some (Vptr b1 (Int.add ofs1 (Int.mul (Int.repr (sizeof cenv ty)) n2))) - | Vint n1, Vint n2 => - Some (Vint (Int.add n1 (Int.mul (Int.repr (sizeof cenv ty)) n2))) - | _, _ => None - end - | add_case_ip ty => (**r integer plus pointer *) - match v1,v2 with - | Vint n1, Vptr b2 ofs2 => - Some (Vptr b2 (Int.add ofs2 (Int.mul (Int.repr (sizeof cenv ty)) n1))) + let n2 := ptrofs_of_int si n2 in + Some (Vptr b1 (Ptrofs.add ofs1 (Ptrofs.mul (Ptrofs.repr (sizeof cenv ty)) n2))) | Vint n1, Vint n2 => - Some (Vint (Int.add n2 (Int.mul (Int.repr (sizeof cenv ty)) n1))) + if Archi.ptr64 then None else Some (Vint (Int.add n1 (Int.mul (Int.repr (sizeof cenv ty)) n2))) + | Vlong n1, Vint n2 => + let n2 := cast_int_long si n2 in + if Archi.ptr64 then Some (Vlong (Int64.add n1 (Int64.mul (Int64.repr (sizeof cenv ty)) n2))) else None | _, _ => None end | add_case_pl ty => (**r pointer plus long *) - match v1,v2 with + match v1, v2 with | Vptr b1 ofs1, Vlong n2 => - let n2 := Int.repr (Int64.unsigned n2) in - Some (Vptr b1 (Int.add ofs1 (Int.mul (Int.repr (sizeof cenv ty)) n2))) + let n2 := Ptrofs.of_int64 n2 in + Some (Vptr b1 (Ptrofs.add ofs1 (Ptrofs.mul (Ptrofs.repr (sizeof cenv ty)) n2))) | Vint n1, Vlong n2 => let n2 := Int.repr (Int64.unsigned n2) in - Some (Vint (Int.add n1 (Int.mul (Int.repr (sizeof cenv ty)) n2))) - | _, _ => None - end - | add_case_lp ty => (**r long plus pointer *) - match v1,v2 with - | Vlong n1, Vptr b2 ofs2 => - let n1 := Int.repr (Int64.unsigned n1) in - Some (Vptr b2 (Int.add ofs2 (Int.mul (Int.repr (sizeof cenv ty)) n1))) - | Vlong n1, Vint n2 => - let n1 := Int.repr (Int64.unsigned n1) in - Some (Vint (Int.add n2 (Int.mul (Int.repr (sizeof cenv ty)) n1))) + if Archi.ptr64 then None else Some (Vint (Int.add n1 (Int.mul (Int.repr (sizeof cenv ty)) n2))) + | Vlong n1, Vlong n2 => + if Archi.ptr64 then Some (Vlong (Int64.add n1 (Int64.mul (Int64.repr (sizeof cenv ty)) n2))) else None | _, _ => None end | add_default => @@ -688,14 +688,14 @@ Definition sem_add (cenv: composite_env) (v1:val) (t1:type) (v2: val) (t2:type) (** *** Subtraction *) Inductive classify_sub_cases : Type := - | sub_case_pi(ty: type) (**r pointer, int *) - | sub_case_pp(ty: type) (**r pointer, pointer *) - | sub_case_pl(ty: type) (**r pointer, long *) - | sub_default. (**r numerical type, numerical type *) + | sub_case_pi (ty: type) (si: signedness) (**r pointer, int *) + | sub_case_pp (ty: type) (**r pointer, pointer *) + | sub_case_pl (ty: type) (**r pointer, long *) + | sub_default. (**r numerical type, numerical type *) Definition classify_sub (ty1: type) (ty2: type) := match typeconv ty1, typeconv ty2 with - | Tpointer ty _, Tint _ _ _ => sub_case_pi ty + | Tpointer ty _, Tint _ si _ => sub_case_pi ty si | Tpointer ty _ , Tpointer _ _ => sub_case_pp ty | Tpointer ty _, Tlong _ _ => sub_case_pl ty | _, _ => sub_default @@ -703,22 +703,28 @@ Definition classify_sub (ty1: type) (ty2: type) := Definition sem_sub (cenv: composite_env) (v1:val) (t1:type) (v2: val) (t2:type) (m:mem): option val := match classify_sub t1 t2 with - | sub_case_pi ty => (**r pointer minus integer *) - match v1,v2 with + | sub_case_pi ty si => (**r pointer minus integer *) + match v1, v2 with | Vptr b1 ofs1, Vint n2 => - Some (Vptr b1 (Int.sub ofs1 (Int.mul (Int.repr (sizeof cenv ty)) n2))) + let n2 := ptrofs_of_int si n2 in + Some (Vptr b1 (Ptrofs.sub ofs1 (Ptrofs.mul (Ptrofs.repr (sizeof cenv ty)) n2))) | Vint n1, Vint n2 => - Some (Vint (Int.sub n1 (Int.mul (Int.repr (sizeof cenv ty)) n2))) + if Archi.ptr64 then None else Some (Vint (Int.sub n1 (Int.mul (Int.repr (sizeof cenv ty)) n2))) + | Vlong n1, Vint n2 => + let n2 := cast_int_long si n2 in + if Archi.ptr64 then Some (Vlong (Int64.sub n1 (Int64.mul (Int64.repr (sizeof cenv ty)) n2))) else None | _, _ => None end | sub_case_pl ty => (**r pointer minus long *) - match v1,v2 with + match v1, v2 with | Vptr b1 ofs1, Vlong n2 => - let n2 := Int.repr (Int64.unsigned n2) in - Some (Vptr b1 (Int.sub ofs1 (Int.mul (Int.repr (sizeof cenv ty)) n2))) + let n2 := Ptrofs.of_int64 n2 in + Some (Vptr b1 (Ptrofs.sub ofs1 (Ptrofs.mul (Ptrofs.repr (sizeof cenv ty)) n2))) | Vint n1, Vlong n2 => let n2 := Int.repr (Int64.unsigned n2) in - Some (Vint (Int.sub n1 (Int.mul (Int.repr (sizeof cenv ty)) n2))) + if Archi.ptr64 then None else Some (Vint (Int.sub n1 (Int.mul (Int.repr (sizeof cenv ty)) n2))) + | Vlong n1, Vlong n2 => + if Archi.ptr64 then Some (Vlong (Int64.sub n1 (Int64.mul (Int64.repr (sizeof cenv ty)) n2))) else None | _, _ => None end | sub_case_pp ty => (**r pointer minus pointer *) @@ -726,8 +732,8 @@ Definition sem_sub (cenv: composite_env) (v1:val) (t1:type) (v2: val) (t2:type) | Vptr b1 ofs1, Vptr b2 ofs2 => if eq_block b1 b2 then let sz := sizeof cenv ty in - if zlt 0 sz && zle sz Int.max_signed - then Some (Vint (Int.divs (Int.sub ofs1 ofs2) (Int.repr sz))) + if zlt 0 sz && zle sz Ptrofs.max_signed + then Some (Vptrofs (Ptrofs.divs (Ptrofs.sub ofs1 ofs2) (Ptrofs.repr sz))) else None else None | _, _ => None @@ -903,6 +909,8 @@ Definition sem_shr (v1:val) (t1:type) (v2: val) (t2:type) : option val := Inductive classify_cmp_cases : Type := | cmp_case_pp (**r pointer, pointer *) + | cmp_case_pi (si: signedness) (**r pointer, int *) + | cmp_case_ip (si: signedness) (**r int, pointer *) | cmp_case_pl (**r pointer, long *) | cmp_case_lp (**r long, pointer *) | cmp_default. (**r numerical, numerical *) @@ -910,32 +918,64 @@ Inductive classify_cmp_cases : Type := Definition classify_cmp (ty1: type) (ty2: type) := match typeconv ty1, typeconv ty2 with | Tpointer _ _ , Tpointer _ _ => cmp_case_pp - | Tpointer _ _ , Tint _ _ _ => cmp_case_pp - | Tint _ _ _, Tpointer _ _ => cmp_case_pp + | Tpointer _ _ , Tint _ si _ => cmp_case_pi si + | Tint _ si _, Tpointer _ _ => cmp_case_ip si | Tpointer _ _ , Tlong _ _ => cmp_case_pl | Tlong _ _ , Tpointer _ _ => cmp_case_lp | _, _ => cmp_default end. +Definition cmp_ptr (m: mem) (c: comparison) (v1 v2: val): option val := + option_map Val.of_bool + (if Archi.ptr64 + then Val.cmplu_bool (Mem.valid_pointer m) c v1 v2 + else Val.cmpu_bool (Mem.valid_pointer m) c v1 v2). + Definition sem_cmp (c:comparison) (v1: val) (t1: type) (v2: val) (t2: type) (m: mem): option val := match classify_cmp t1 t2 with | cmp_case_pp => - option_map Val.of_bool (Val.cmpu_bool (Mem.valid_pointer m) c v1 v2) + cmp_ptr m c v1 v2 + | cmp_case_pi si => + match v2 with + | Vint n2 => + let v2' := Vptrofs (ptrofs_of_int si n2) in + cmp_ptr m c v1 v2' + | Vptr b ofs => + if Archi.ptr64 then None else cmp_ptr m c v1 v2 + | _ => + None + end + | cmp_case_ip si => + match v1 with + | Vint n1 => + let v1' := Vptrofs (ptrofs_of_int si n1) in + cmp_ptr m c v1' v2 + | Vptr b ofs => + if Archi.ptr64 then None else cmp_ptr m c v1 v2 + | _ => + None + end | cmp_case_pl => match v2 with | Vlong n2 => - let n2 := Int.repr (Int64.unsigned n2) in - option_map Val.of_bool (Val.cmpu_bool (Mem.valid_pointer m) c v1 (Vint n2)) - | _ => None + let v2' := Vptrofs (Ptrofs.of_int64 n2) in + cmp_ptr m c v1 v2' + | Vptr b ofs => + if Archi.ptr64 then cmp_ptr m c v1 v2 else None + | _ => + None end | cmp_case_lp => match v1 with | Vlong n1 => - let n1 := Int.repr (Int64.unsigned n1) in - option_map Val.of_bool (Val.cmpu_bool (Mem.valid_pointer m) c (Vint n1) v2) - | _ => None + let v1' := Vptrofs (Ptrofs.of_int64 n1) in + cmp_ptr m c v1' v2 + | Vptr b ofs => + if Archi.ptr64 then cmp_ptr m c v1 v2 else None + | _ => + None end | cmp_default => sem_binarith @@ -1047,30 +1087,30 @@ Variables m m': mem. Hypothesis valid_pointer_inj: forall b1 ofs b2 delta, f b1 = Some(b2, delta) -> - Mem.valid_pointer m b1 (Int.unsigned ofs) = true -> - Mem.valid_pointer m' b2 (Int.unsigned (Int.add ofs (Int.repr delta))) = true. + Mem.valid_pointer m b1 (Ptrofs.unsigned ofs) = true -> + Mem.valid_pointer m' 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 m b1 (Int.unsigned ofs) = true -> - Mem.weak_valid_pointer m' b2 (Int.unsigned (Int.add ofs (Int.repr delta))) = true. + Mem.weak_valid_pointer m b1 (Ptrofs.unsigned ofs) = true -> + Mem.weak_valid_pointer m' 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 m b1 (Int.unsigned ofs) = true -> - 0 <= Int.unsigned ofs + Int.unsigned (Int.repr delta) <= Int.max_unsigned. + Mem.weak_valid_pointer m 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 m b1 (Int.unsigned ofs1) = true -> - Mem.valid_pointer m b2 (Int.unsigned ofs2) = true -> + Mem.valid_pointer m b1 (Ptrofs.unsigned ofs1) = true -> + Mem.valid_pointer m 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)). Remark val_inject_vtrue: forall f, Val.inject f Vtrue Vtrue. Proof. unfold Vtrue; auto. Qed. @@ -1082,11 +1122,18 @@ Remark val_inject_of_bool: forall f b, Val.inject f (Val.of_bool b) (Val.of_bool Proof. intros. unfold Val.of_bool. destruct b; [apply val_inject_vtrue|apply val_inject_vfalse]. Qed. -Hint Resolve val_inject_vtrue val_inject_vfalse val_inject_of_bool. +Remark val_inject_vptrofs: forall n, Val.inject f (Vptrofs n) (Vptrofs n). +Proof. intros. unfold Vptrofs. destruct Archi.ptr64; auto. Qed. + +Hint Resolve val_inject_vtrue val_inject_vfalse val_inject_of_bool val_inject_vptrofs. Ltac TrivialInject := match goal with - | |- exists v', Some ?v = Some v' /\ _ => exists v; split; auto + | [ H: None = Some _ |- _ ] => discriminate + | [ H: Some _ = Some _ |- _ ] => inv H; TrivialInject + | [ H: match ?x with Some _ => _ | None => _ end = Some _ |- _ ] => destruct x; TrivialInject + | [ H: match ?x with true => _ | false => _ end = Some _ |- _ ] => destruct x eqn:?; TrivialInject + | [ |- exists v', Some ?v = Some v' /\ _ ] => exists v; split; auto | _ => idtac end. @@ -1096,20 +1143,31 @@ Lemma sem_cast_inj: Val.inject f v1 tv1 -> exists tv, sem_cast tv1 ty1 ty m'= Some tv /\ Val.inject f v tv. Proof. - unfold sem_cast; intros; destruct (classify_cast ty1 ty); - inv H0; inv H; TrivialInject. + unfold sem_cast; intros; destruct (classify_cast ty1 ty); inv H0; TrivialInject. - econstructor; eauto. -- destruct (cast_float_int si2 f0); inv H1; TrivialInject. -- destruct (cast_single_int si2 f0); inv H1; TrivialInject. -- destruct (cast_float_long si2 f0); inv H1; TrivialInject. -- destruct (cast_single_long si2 f0); inv H1; TrivialInject. -- destruct (Mem.weak_valid_pointer m b1 (Int.unsigned ofs1)) eqn:VALID; inv H2. - erewrite weak_valid_pointer_inj by eauto. TrivialInject. -- destruct (ident_eq id1 id2); inv H2; TrivialInject. econstructor; eauto. -- destruct (ident_eq id1 id2); inv H2; TrivialInject. econstructor; eauto. +- erewrite weak_valid_pointer_inj by eauto. TrivialInject. +- erewrite weak_valid_pointer_inj by eauto. TrivialInject. +- destruct (ident_eq id1 id2); TrivialInject. econstructor; eauto. +- destruct (ident_eq id1 id2); TrivialInject. econstructor; eauto. - econstructor; eauto. Qed. +Lemma bool_val_inj: + forall v ty b tv, + bool_val v ty m = Some b -> + Val.inject f v tv -> + bool_val tv ty m' = Some b. +Proof. + unfold bool_val; intros. + destruct (classify_bool ty); inv H0; try congruence. + destruct Archi.ptr64; try discriminate. + destruct (Mem.weak_valid_pointer m b1 (Ptrofs.unsigned ofs1)) eqn:VP; inv H. + erewrite weak_valid_pointer_inj by eauto. auto. + destruct Archi.ptr64; try discriminate. + destruct (Mem.weak_valid_pointer m b1 (Ptrofs.unsigned ofs1)) eqn:VP; inv H. + erewrite weak_valid_pointer_inj by eauto. auto. +Qed. + Lemma sem_unary_operation_inj: forall op v1 ty v tv1, sem_unary_operation op v1 ty m = Some v -> @@ -1117,15 +1175,14 @@ Lemma sem_unary_operation_inj: exists tv, sem_unary_operation op tv1 ty m' = Some tv /\ Val.inject f v tv. Proof. unfold sem_unary_operation; intros. destruct op. - (* notbool *) - unfold sem_notbool in *; destruct (classify_bool ty); inv H0; inv H; TrivialInject. - destruct (Mem.weak_valid_pointer m b1 (Int.unsigned ofs1)) eqn:VP; inv H2. - erewrite weak_valid_pointer_inj by eauto. TrivialInject. - (* notint *) +- (* notbool *) + unfold sem_notbool in *. destruct (bool_val v1 ty m) as [b|] eqn:BV; simpl in H; inv H. + erewrite bool_val_inj by eauto. simpl. TrivialInject. +- (* notint *) unfold sem_notint in *; destruct (classify_notint ty); inv H0; inv H; TrivialInject. - (* neg *) +- (* neg *) unfold sem_neg in *; destruct (classify_neg ty); inv H0; inv H; TrivialInject. - (* absfloat *) +- (* absfloat *) unfold sem_absfloat in *; destruct (classify_neg ty); inv H0; inv H; TrivialInject. Qed. @@ -1175,6 +1232,24 @@ Proof. destruct (Int.ltu i0 Int64.iwordsize'); inv H; auto. Qed. +Remark sem_cmp_ptr_inj: + forall c v1 v2 v tv1 tv2, + cmp_ptr m c v1 v2 = Some v -> + Val.inject f v1 tv1 -> + Val.inject f v2 tv2 -> + exists tv, cmp_ptr m' c tv1 tv2 = Some tv /\ Val.inject f v tv. +Proof. + unfold cmp_ptr; intros. + remember (if Archi.ptr64 + then Val.cmplu_bool (Mem.valid_pointer m) c v1 v2 + else Val.cmpu_bool (Mem.valid_pointer m) c v1 v2) as ob. + destruct ob as [b|]; simpl in H; inv H. + exists (Val.of_bool b); split; auto. + destruct Archi.ptr64. + erewrite Val.cmplu_bool_inject by eauto. auto. + erewrite Val.cmpu_bool_inject by eauto. auto. +Qed. + Remark sem_cmp_inj: forall cmp v1 tv1 ty1 v2 tv2 ty2 v, sem_cmp cmp v1 ty1 v2 ty2 m = Some v -> @@ -1185,24 +1260,15 @@ Proof. intros. unfold sem_cmp in *; destruct (classify_cmp ty1 ty2). - (* pointer - pointer *) - destruct (Val.cmpu_bool (Mem.valid_pointer m) cmp v1 v2) as [b|] eqn:E; simpl in H; inv H. - replace (Val.cmpu_bool (Mem.valid_pointer m') cmp tv1 tv2) with (Some b). - simpl. TrivialInject. - symmetry. eapply Val.cmpu_bool_inject; eauto. + eapply sem_cmp_ptr_inj; eauto. +- (* pointer - int *) + inversion H1; subst; TrivialInject; eapply sem_cmp_ptr_inj; eauto. +- (* int - pointer *) + inversion H0; subst; TrivialInject; eapply sem_cmp_ptr_inj; eauto. - (* pointer - long *) - destruct v2; try discriminate. inv H1. - set (v2 := Vint (Int.repr (Int64.unsigned i))) in *. - destruct (Val.cmpu_bool (Mem.valid_pointer m) cmp v1 v2) as [b|] eqn:E; simpl in H; inv H. - replace (Val.cmpu_bool (Mem.valid_pointer m') cmp tv1 v2) with (Some b). - simpl. TrivialInject. - symmetry. eapply Val.cmpu_bool_inject with (v2 := v2); eauto. constructor. + inversion H1; subst; TrivialInject; eapply sem_cmp_ptr_inj; eauto. - (* long - pointer *) - destruct v1; try discriminate. inv H0. - set (v1 := Vint (Int.repr (Int64.unsigned i))) in *. - destruct (Val.cmpu_bool (Mem.valid_pointer m) cmp v1 v2) as [b|] eqn:E; simpl in H; inv H. - replace (Val.cmpu_bool (Mem.valid_pointer m') cmp v1 tv2) with (Some b). - simpl. TrivialInject. - symmetry. eapply Val.cmpu_bool_inject with (v1 := v1); eauto. constructor. + inversion H0; subst; TrivialInject; eapply sem_cmp_ptr_inj; eauto. - (* numerical - numerical *) assert (SELF: forall b, optval_self_injects (Some (Val.of_bool b))). { @@ -1220,26 +1286,22 @@ Proof. unfold sem_binary_operation; intros; destruct op. - (* add *) unfold sem_add in *; destruct (classify_add ty1 ty2). - + inv H0; inv H1; inv H. TrivialInject. TrivialInject. - econstructor. eauto. repeat rewrite Int.add_assoc. decEq. apply Int.add_commut. - + inv H0; inv H1; inv H. TrivialInject. TrivialInject. - econstructor. eauto. repeat rewrite Int.add_assoc. decEq. apply Int.add_commut. - + inv H0; inv H1; inv H. TrivialInject. TrivialInject. - econstructor. eauto. repeat rewrite Int.add_assoc. decEq. apply Int.add_commut. - + inv H0; inv H1; inv H. TrivialInject. TrivialInject. - econstructor. eauto. repeat rewrite Int.add_assoc. decEq. apply Int.add_commut. + + inv H0; inv H1; TrivialInject. + econstructor. eauto. repeat rewrite Ptrofs.add_assoc. decEq. apply Ptrofs.add_commut. + + inv H0; inv H1; TrivialInject. + econstructor. eauto. repeat rewrite Ptrofs.add_assoc. decEq. apply Ptrofs.add_commut. + eapply sem_binarith_inject; eauto; intros; exact I. - (* sub *) unfold sem_sub in *; destruct (classify_sub ty1 ty2). - + inv H0; inv H1; inv H. TrivialInject. TrivialInject. - econstructor. eauto. rewrite Int.sub_add_l. auto. - + inv H0; inv H1; inv H. TrivialInject. + + inv H0; inv H1; TrivialInject. + econstructor. eauto. rewrite Ptrofs.sub_add_l. auto. + + inv H0; inv H1; TrivialInject. destruct (eq_block b1 b0); try discriminate. subst b1. rewrite H0 in H2; inv H2. rewrite dec_eq_true. - destruct (zlt 0 (sizeof cenv ty) && zle (sizeof cenv ty) Int.max_signed); inv H3. - rewrite Int.sub_shifted. TrivialInject. - + inv H0; inv H1; inv H. TrivialInject. TrivialInject. - econstructor. eauto. rewrite Int.sub_add_l. auto. + destruct (zlt 0 (sizeof cenv ty) && zle (sizeof cenv ty) Ptrofs.max_signed); inv H. + rewrite Ptrofs.sub_shifted. TrivialInject. + + inv H0; inv H1; TrivialInject. + econstructor. eauto. rewrite Ptrofs.sub_add_l. auto. + eapply sem_binarith_inject; eauto; intros; exact I. - (* mul *) eapply sem_binarith_inject; eauto; intros; exact I. @@ -1286,18 +1348,6 @@ Proof. - eapply sem_cmp_inj; eauto. Qed. -Lemma bool_val_inj: - forall v ty b tv, - bool_val v ty m = Some b -> - Val.inject f v tv -> - bool_val tv ty m' = Some b. -Proof. - unfold bool_val; intros. - destruct (classify_bool ty); inv H0; try congruence. - destruct (Mem.weak_valid_pointer m b1 (Int.unsigned ofs1)) eqn:VP; inv H. - erewrite weak_valid_pointer_inj by eauto. auto. -Qed. - End GENERIC_INJECTION. Lemma sem_cast_inject: @@ -1364,7 +1414,7 @@ Lemma cast_bool_bool_val: assert (A: classify_bool t = match t with | Tint _ _ _ => bool_case_i - | Tpointer _ _ | Tarray _ _ _ | Tfunction _ _ _ => bool_case_p + | Tpointer _ _ | Tarray _ _ _ | Tfunction _ _ _ => if Archi.ptr64 then bool_case_l else bool_case_i | Tfloat F64 _ => bool_case_f | Tfloat F32 _ => bool_case_s | Tlong _ _ => bool_case_l @@ -1373,9 +1423,12 @@ Lemma cast_bool_bool_val: { unfold classify_bool; destruct t; simpl; auto. destruct i; auto. } - unfold bool_val. rewrite A. unfold sem_cast. destruct t; simpl; auto; destruct v; auto. + unfold bool_val. rewrite A. + unfold sem_cast, classify_cast; remember Archi.ptr64 as ptr64; destruct t; simpl; auto; destruct v; auto. destruct (Int.eq i0 Int.zero); auto. + destruct ptr64; auto. destruct (Mem.weak_valid_pointer m b (Ptrofs.unsigned i0)); auto. destruct (Int64.eq i Int64.zero); auto. + destruct (negb ptr64); auto. destruct (Mem.weak_valid_pointer m b (Ptrofs.unsigned i)); auto. destruct f; auto. destruct f; auto. destruct f; auto. @@ -1383,13 +1436,30 @@ Lemma cast_bool_bool_val: destruct (Float.cmp Ceq f0 Float.zero); auto. destruct f; auto. destruct (Float32.cmp Ceq f0 Float32.zero); auto. - destruct f; auto. + destruct f; auto. + destruct ptr64; auto. destruct (Int.eq i Int.zero); auto. - destruct (Mem.weak_valid_pointer m b (Int.unsigned i)); auto. - destruct (Int.eq i Int.zero); auto. - destruct (Mem.weak_valid_pointer m b (Int.unsigned i)); auto. - destruct (Int.eq i Int.zero); auto. - destruct (Mem.weak_valid_pointer m b (Int.unsigned i)); auto. + destruct ptr64; auto. + destruct ptr64; auto. + destruct ptr64; auto. destruct (Int64.eq i Int64.zero); auto. + destruct ptr64; auto. + destruct ptr64; auto. + destruct ptr64; auto. destruct (Mem.weak_valid_pointer m b (Ptrofs.unsigned i)); auto. + destruct (Mem.weak_valid_pointer m b (Ptrofs.unsigned i)); auto. + destruct ptr64; auto. + destruct ptr64; auto. destruct (Int.eq i Int.zero); auto. + destruct ptr64; auto. destruct (Int64.eq i Int64.zero); auto. + destruct ptr64; auto. + destruct ptr64; auto. + destruct ptr64; auto. destruct (Mem.weak_valid_pointer m b (Ptrofs.unsigned i)); auto. + destruct (Mem.weak_valid_pointer m b (Ptrofs.unsigned i)); auto. + destruct ptr64; auto. + destruct ptr64; auto. destruct (Int.eq i Int.zero); auto. + destruct ptr64; auto. destruct (Int64.eq i Int64.zero); auto. + destruct ptr64; auto. + destruct ptr64; auto. + destruct ptr64; auto. destruct (Mem.weak_valid_pointer m b (Ptrofs.unsigned i)); auto. + destruct (Mem.weak_valid_pointer m b (Ptrofs.unsigned i)); auto. Qed. (** Relation between Boolean value and Boolean negation. *) @@ -1399,13 +1469,13 @@ Lemma notbool_bool_val: sem_notbool v t m = match bool_val v t m with None => None | Some b => Some(Val.of_bool (negb b)) end. Proof. - intros. unfold sem_notbool, bool_val. - destruct (classify_bool t); auto; destruct v; auto; rewrite ? negb_involutive; auto. - destruct (Mem.weak_valid_pointer m b (Int.unsigned i)); auto. + intros. unfold sem_notbool. destruct (bool_val v t m) as [[] | ]; reflexivity. Qed. (** Properties of values obtained by casting to a given type. *) +Section VAL_CASTED. + Inductive val_casted: val -> type -> Prop := | val_casted_int: forall sz si attr n, cast_int_int sz si n = n -> @@ -1419,9 +1489,13 @@ Inductive val_casted: val -> type -> Prop := | val_casted_ptr_ptr: forall b ofs ty attr, val_casted (Vptr b ofs) (Tpointer ty attr) | val_casted_int_ptr: forall n ty attr, - val_casted (Vint n) (Tpointer ty attr) + Archi.ptr64 = false -> val_casted (Vint n) (Tpointer ty attr) | val_casted_ptr_int: forall b ofs si attr, - val_casted (Vptr b ofs) (Tint I32 si attr) + Archi.ptr64 = false -> val_casted (Vptr b ofs) (Tint I32 si attr) + | val_casted_long_ptr: forall n ty attr, + Archi.ptr64 = true -> val_casted (Vlong n) (Tpointer ty attr) + | val_casted_ptr_long: forall b ofs si attr, + Archi.ptr64 = true -> val_casted (Vptr b ofs) (Tlong si attr) | val_casted_struct: forall id attr b ofs, val_casted (Vptr b ofs) (Tstruct id attr) | val_casted_union: forall id attr b ofs, @@ -1429,6 +1503,8 @@ Inductive val_casted: val -> type -> Prop := | val_casted_void: forall v, val_casted v Tvoid. +Hint Constructors val_casted. + Remark cast_int_int_idem: forall sz sg i, cast_int_int sz sg (cast_int_int sz sg i) = cast_int_int sz sg i. Proof. @@ -1438,77 +1514,50 @@ Proof. destruct (Int.eq i Int.zero); auto. Qed. +Ltac DestructCases := + match goal with + | [H: match match ?x with _ => _ end with _ => _ end = Some _ |- _ ] => destruct x eqn:?; DestructCases + | [H: match ?x with _ => _ end = Some _ |- _ ] => destruct x eqn:?; DestructCases + | [H: Some _ = Some _ |- _ ] => inv H; DestructCases + | [H: None = Some _ |- _ ] => discriminate H + | [H: @eq intsize _ _ |- _ ] => discriminate H || (clear H; DestructCases) + | [ |- val_casted (Vint (if ?x then Int.zero else Int.one)) _ ] => + try (constructor; destruct x; reflexivity) + | [ |- val_casted (Vint _) (Tint ?sz ?sg _) ] => + try (constructor; apply (cast_int_int_idem sz sg)) + | _ => idtac + end. + Lemma cast_val_is_casted: forall v ty ty' v' m, sem_cast v ty ty' m = Some v' -> val_casted v' ty'. Proof. - unfold sem_cast; intros. destruct ty'; simpl in *. -- (* void *) - constructor. -- (* int *) - destruct i; destruct ty; simpl in H; try (destruct f); try discriminate; destruct v; inv H. - constructor. apply (cast_int_int_idem I8 s). - constructor. apply (cast_int_int_idem I8 s). - destruct (cast_single_int s f); inv H1. constructor. apply (cast_int_int_idem I8 s). - destruct (cast_float_int s f); inv H1. constructor. apply (cast_int_int_idem I8 s). - constructor. apply (cast_int_int_idem I16 s). - constructor. apply (cast_int_int_idem I16 s). - destruct (cast_single_int s f); inv H1. constructor. apply (cast_int_int_idem I16 s). - destruct (cast_float_int s f); inv H1. constructor. apply (cast_int_int_idem I16 s). - constructor. auto. - constructor. - constructor. auto. - destruct (cast_single_int s f); inv H1. constructor. auto. - destruct (cast_float_int s f); inv H1. constructor; auto. - constructor; auto. - constructor. - constructor; auto. - constructor. - constructor; auto. - constructor. - constructor. simpl. destruct (Int.eq i0 Int.zero); auto. - constructor. simpl. destruct (Int64.eq i Int64.zero); auto. - constructor. simpl. destruct (Float32.cmp Ceq f Float32.zero); auto. - constructor. simpl. destruct (Float.cmp Ceq f Float.zero); auto. - constructor. simpl. destruct (Int.eq i Int.zero); auto. - destruct (Mem.weak_valid_pointer m b (Int.unsigned i)); inv H1. constructor; auto. - constructor. simpl. destruct (Int.eq i Int.zero); auto. - destruct (Mem.weak_valid_pointer m b (Int.unsigned i)); inv H1. constructor; auto. - constructor. simpl. destruct (Int.eq i Int.zero); auto. - destruct (Mem.weak_valid_pointer m b (Int.unsigned i)); inv H1. constructor; auto. -- (* long *) - destruct ty; try (destruct f); try discriminate. - destruct v; inv H. constructor. - destruct v; inv H. constructor. - destruct v; try discriminate. destruct (cast_single_long s f); inv H. constructor. - destruct v; try discriminate. destruct (cast_float_long s f); inv H. constructor. - destruct v; inv H. constructor. - destruct v; inv H. constructor. - destruct v; inv H. constructor. -- (* float *) - destruct f; destruct ty; simpl in H; try (destruct f); try discriminate; destruct v; inv H; constructor. -- (* pointer *) - destruct ty; simpl in H; try discriminate; destruct v; inv H; try constructor. -- (* array (impossible case) *) - discriminate. -- (* function (impossible case) *) - discriminate. -- (* structs *) - destruct ty; try discriminate; destruct v; try discriminate. - destruct (ident_eq i0 i); inv H; constructor. -- (* unions *) - destruct ty; try discriminate; destruct v; try discriminate. - destruct (ident_eq i0 i); inv H; constructor. + unfold sem_cast; intros. + destruct ty, ty'; simpl in H; DestructCases; constructor; auto. Qed. +End VAL_CASTED. + (** As a consequence, casting twice is equivalent to casting once. *) Lemma cast_val_casted: forall v ty m, val_casted v ty -> sem_cast v ty ty m = Some v. Proof. - intros. inversion H; clear H; subst v ty; unfold sem_cast; simpl; auto. - destruct sz; congruence. - unfold proj_sumbool; repeat rewrite dec_eq_true; auto. - unfold proj_sumbool; repeat rewrite dec_eq_true; auto. + intros. unfold sem_cast; inversion H; clear H; subst v ty; simpl. +- destruct Archi.ptr64; [ | destruct (intsize_eq sz I32)]. ++ destruct sz; f_equal; f_equal; assumption. ++ subst sz; auto. ++ destruct sz; f_equal; f_equal; assumption. +- auto. +- auto. +- destruct Archi.ptr64; auto. +- auto. +- rewrite H0; auto. +- rewrite H0; auto. +- rewrite H0; auto. +- rewrite H0; auto. +- rewrite dec_eq_true; auto. +- rewrite dec_eq_true; auto. +- auto. Qed. Lemma cast_idempotent: |