diff options
Diffstat (limited to 'riscV/Op.v')
| -rw-r--r-- | riscV/Op.v | 537 |
1 files changed, 319 insertions, 218 deletions
@@ -38,6 +38,12 @@ Set Implicit Arguments. (** Conditions (boolean-valued operators). *) +(** Type to modelize the use of a special register in arith operations *) + +Inductive oreg: Type := + | X0_L: oreg + | X0_R: oreg. + Inductive condition : Type := | Ccomp (c: comparison) (**r signed integer comparison *) | Ccompu (c: comparison) (**r unsigned integer comparison *) @@ -52,22 +58,30 @@ Inductive condition : Type := | Ccompfs (c: comparison) (**r 32-bit floating-point comparison *) | Cnotcompfs (c: comparison) (**r negation of a floating-point comparison *) (* Expansed branches *) - | CEbeqw (optR0: option bool) (**r branch-if-equal signed *) - | CEbnew (optR0: option bool) (**r branch-if-not-equal signed *) - | CEbequw (optR0: option bool) (**r branch-if-equal unsigned *) - | CEbneuw (optR0: option bool) (**r branch-if-not-equal unsigned *) - | CEbltw (optR0: option bool) (**r branch-if-less signed *) - | CEbltuw (optR0: option bool) (**r branch-if-less unsigned *) - | CEbgew (optR0: option bool) (**r branch-if-greater-or-equal signed *) - | CEbgeuw (optR0: option bool) (**r branch-if-greater-or-equal unsigned *) - | CEbeql (optR0: option bool) (**r branch-if-equal signed *) - | CEbnel (optR0: option bool) (**r branch-if-not-equal signed *) - | CEbequl (optR0: option bool) (**r branch-if-equal unsigned *) - | CEbneul (optR0: option bool) (**r branch-if-not-equal unsigned *) - | CEbltl (optR0: option bool) (**r branch-if-less signed *) - | CEbltul (optR0: option bool) (**r branch-if-less unsigned *) - | CEbgel (optR0: option bool) (**r branch-if-greater-or-equal signed *) - | CEbgeul (optR0: option bool). (**r branch-if-greater-or-equal unsigned *) + | CEbeqw (optR: option oreg) (**r branch-if-equal signed *) + | CEbnew (optR: option oreg) (**r branch-if-not-equal signed *) + | CEbequw (optR: option oreg) (**r branch-if-equal unsigned *) + | CEbneuw (optR: option oreg) (**r branch-if-not-equal unsigned *) + | CEbltw (optR: option oreg) (**r branch-if-less signed *) + | CEbltuw (optR: option oreg) (**r branch-if-less unsigned *) + | CEbgew (optR: option oreg) (**r branch-if-greater-or-equal signed *) + | CEbgeuw (optR: option oreg) (**r branch-if-greater-or-equal unsigned *) + | CEbeql (optR: option oreg) (**r branch-if-equal signed *) + | CEbnel (optR: option oreg) (**r branch-if-not-equal signed *) + | CEbequl (optR: option oreg) (**r branch-if-equal unsigned *) + | CEbneul (optR: option oreg) (**r branch-if-not-equal unsigned *) + | CEbltl (optR: option oreg) (**r branch-if-less signed *) + | CEbltul (optR: option oreg) (**r branch-if-less unsigned *) + | CEbgel (optR: option oreg) (**r branch-if-greater-or-equal signed *) + | CEbgeul (optR: option oreg). (**r branch-if-greater-or-equal unsigned *) + +(* This type will define the eval function of a OEmayundef operation. *) + +Inductive mayundef: Type := + | MUint: mayundef + | MUlong: mayundef + | MUshrx: int -> mayundef + | MUshrxl: int -> mayundef. (** Arithmetic and logical operations. In the descriptions, [rd] is the result of the operation and [r1], [r2], etc, are the arguments. *) @@ -172,35 +186,40 @@ Inductive operation : Type := (*c Boolean tests: *) | Ocmp (cond: condition) (**r [rd = 1] if condition holds, [rd = 0] otherwise. *) (* Expansed conditions *) - | OEseqw (optR0: option bool) (**r [rd <- rs1 == rs2] signed *) - | OEsnew (optR0: option bool) (**r [rd <- rs1 != rs2] signed *) - | OEsequw (optR0: option bool) (**r [rd <- rs1 == rs2] unsigned *) - | OEsneuw (optR0: option bool) (**r [rd <- rs1 != rs2] unsigned *) - | OEsltw (optR0: option bool) (**r set-less-than *) - | OEsltuw (optR0: option bool) (**r set-less-than unsigned *) - | OEsltiw (n: int) (**r set-less-than immediate *) - | OEsltiuw (n: int) (**r set-less-than unsigned immediate *) - | OExoriw (n: int) (**r xor immediate *) - | OEluiw (n: int) (is_long: bool) (**r load upper-immediate *) - | OEaddiwr0 (n: int) (is_long: bool) (**r add immediate *) - | OEseql (optR0: option bool) (**r [rd <- rs1 == rs2] signed *) - | OEsnel (optR0: option bool) (**r [rd <- rs1 != rs2] signed *) - | OEsequl (optR0: option bool) (**r [rd <- rs1 == rs2] unsigned *) - | OEsneul (optR0: option bool) (**r [rd <- rs1 != rs2] unsigned *) - | OEsltl (optR0: option bool) (**r set-less-than *) - | OEsltul (optR0: option bool) (**r set-less-than unsigned *) - | OEsltil (n: int64) (**r set-less-than immediate *) - | OEsltiul (n: int64) (**r set-less-than unsigned immediate *) - | OExoril (n: int64) (**r xor immediate *) - | OEluil (n: int64) (**r load upper-immediate *) - | OEaddilr0 (n: int64) (**r add immediate *) - | OEloadli (n: int64) (**r load an immediate int64 *) - | OEfeqd (**r compare equal *) - | OEfltd (**r compare less-than *) - | OEfled (**r compare less-than/equal *) - | OEfeqs (**r compare equal *) - | OEflts (**r compare less-than *) - | OEfles (**r compare less-than/equal *) + | OEseqw (optR: option oreg) (**r [rd <- rs1 == rs2] signed *) + | OEsnew (optR: option oreg) (**r [rd <- rs1 != rs2] signed *) + | OEsequw (optR: option oreg) (**r [rd <- rs1 == rs2] unsigned *) + | OEsneuw (optR: option oreg) (**r [rd <- rs1 != rs2] unsigned *) + | OEsltw (optR: option oreg) (**r set-less-than *) + | OEsltuw (optR: option oreg) (**r set-less-than unsigned *) + | OEsltiw (n: int) (**r set-less-than immediate *) + | OEsltiuw (n: int) (**r set-less-than unsigned immediate *) + | OEaddiw (optR: option oreg) (n: int) (**r add immediate *) + | OEandiw (n: int) (**r and immediate *) + | OEoriw (n: int) (**r or immediate *) + | OExoriw (n: int) (**r xor immediate *) + | OEluiw (n: int) (**r load upper-immediate *) + | OEseql (optR: option oreg) (**r [rd <- rs1 == rs2] signed *) + | OEsnel (optR: option oreg) (**r [rd <- rs1 != rs2] signed *) + | OEsequl (optR: option oreg) (**r [rd <- rs1 == rs2] unsigned *) + | OEsneul (optR: option oreg) (**r [rd <- rs1 != rs2] unsigned *) + | OEsltl (optR: option oreg) (**r set-less-than *) + | OEsltul (optR: option oreg) (**r set-less-than unsigned *) + | OEsltil (n: int64) (**r set-less-than immediate *) + | OEsltiul (n: int64) (**r set-less-than unsigned immediate *) + | OEaddil (optR: option oreg) (n: int64) (**r add immediate *) + | OEandil (n: int64) (**r and immediate *) + | OEoril (n: int64) (**r or immediate *) + | OExoril (n: int64) (**r xor immediate *) + | OEluil (n: int64) (**r load upper-immediate *) + | OEloadli (n: int64) (**r load an immediate int64 *) + | OEmayundef (mu: mayundef) + | OEfeqd (**r compare equal *) + | OEfltd (**r compare less-than *) + | OEfled (**r compare less-than/equal *) + | OEfeqs (**r compare equal *) + | OEflts (**r compare less-than *) + | OEfles (**r compare less-than/equal *) | Obits_of_single | Obits_of_float | Osingle_of_bits @@ -217,12 +236,15 @@ Inductive addressing: Type := (** Comparison functions (used in modules [CSE] and [Allocation]). *) +Definition oreg_eq: forall (x y: oreg), {x=y} + {x<>y}. +Proof. decide equality. Defined. + Definition eq_condition (x y: condition) : {x=y} + {x<>y}. Proof. - generalize Int.eq_dec Int64.eq_dec bool_dec; intros. + generalize Int.eq_dec Int64.eq_dec bool_dec oreg_eq; intros. assert (forall (x y: comparison), {x=y}+{x<>y}). decide equality. decide equality. - all: destruct optR0, optR1; decide equality. + all: destruct optR, optR0; decide equality. Defined. Definition eq_addressing (x y: addressing) : {x=y} + {x<>y}. @@ -233,9 +255,9 @@ Defined. Definition eq_operation: forall (x y: operation), {x=y} + {x<>y}. Proof. - generalize Int.eq_dec Int64.eq_dec Ptrofs.eq_dec Float.eq_dec Float32.eq_dec ident_eq eq_condition bool_dec; intros. + generalize Int.eq_dec Int64.eq_dec Ptrofs.eq_dec Float.eq_dec Float32.eq_dec ident_eq eq_condition bool_dec Val.eq oreg_eq; intros. decide equality. - all: destruct optR0, optR1; decide equality. + all: try destruct optR, optR0; try decide equality. Defined. (* Alternate definition: @@ -252,41 +274,51 @@ Defined. Global Opaque eq_condition eq_addressing eq_operation. -(** * Evaluation functions *) - -(** Evaluation of conditions, operators and addressing modes applied - to lists of values. Return [None] when the computation can trigger an - error, e.g. integer division by zero. [eval_condition] returns a boolean, - [eval_operation] and [eval_addressing] return a value. *) +(** Generic function to evaluate an instruction according to the given specific register *) Definition zero32 := (Vint Int.zero). Definition zero64 := (Vlong Int64.zero). -Definition apply_bin_r0 {B} (optR0: option bool) (sem: val -> val -> B) (v1 v2 vz: val): B := - match optR0 with +Definition apply_bin_oreg {B} (optR: option oreg) (sem: val -> val -> B) (v1 v2 vz: val): B := + match optR with | None => sem v1 v2 - | Some true => sem vz v1 - | Some false => sem v1 vz + | Some X0_L => sem vz v1 + | Some X0_R => sem v1 vz end. -Definition may_undef_int (is_long: bool) (sem: val -> val -> val) (v1 vimm vz: val): val := - if negb is_long then - match v1 with - | Vint _ => sem vimm vz - | _ => Vundef - end - else - match v1 with - | Vlong _ => sem vimm vz - | _ => Vundef - end. - -Definition may_undef_luil (v1: val) (n: int64): val := - match v1 with - | Vlong _ => Vlong (Int64.sign_ext 32 (Int64.shl n (Int64.repr 12))) - | _ => Vundef +(** Mayundef evaluation according to the above defined type *) + +Definition eval_may_undef (mu: mayundef) (v1 v2: val): val := + match mu with + | MUint => match v1, v2 with + | Vint _, Vint _ => v2 + | _, _ => Vundef + end + | MUlong => match v1, v2 with + | Vlong _, Vint _ => v2 + | _, _ => Vundef + end + | MUshrx i => + match v1, v2 with + | Vint _, Vint _ => + if Int.ltu i (Int.repr 31) then v2 else Vundef + | _, _ => Vundef + end + | MUshrxl i => + match v1, v2 with + | Vlong _, Vlong _ => + if Int.ltu i (Int.repr 63) then v2 else Vundef + | _, _ => Vundef + end end. +(** * Evaluation functions *) + +(** Evaluation of conditions, operators and addressing modes applied + to lists of values. Return [None] when the computation can trigger an + error, e.g. integer division by zero. [eval_condition] returns a boolean, + [eval_operation] and [eval_addressing] return a value. *) + Definition eval_condition (cond: condition) (vl: list val) (m: mem): option bool := match cond, vl with | Ccomp c, v1 :: v2 :: nil => Val.cmp_bool c v1 v2 @@ -302,25 +334,33 @@ Definition eval_condition (cond: condition) (vl: list val) (m: mem): option bool | Ccompfs c, v1 :: v2 :: nil => Val.cmpfs_bool c v1 v2 | Cnotcompfs c, v1 :: v2 :: nil => option_map negb (Val.cmpfs_bool c v1 v2) (* Expansed branches *) - | CEbeqw optR0, v1 :: v2 :: nil => apply_bin_r0 optR0 (Val.cmp_bool Ceq) v1 v2 zero32 - | CEbnew optR0, v1 :: v2 :: nil => apply_bin_r0 optR0 (Val.cmp_bool Cne) v1 v2 zero32 - | CEbequw optR0, v1 :: v2 :: nil => apply_bin_r0 optR0 (Val.cmpu_bool (Mem.valid_pointer m) Ceq) v1 v2 zero32 - | CEbneuw optR0, v1 :: v2 :: nil => apply_bin_r0 optR0 (Val.cmpu_bool (Mem.valid_pointer m) Cne) v1 v2 zero32 - | CEbltw optR0, v1 :: v2 :: nil => apply_bin_r0 optR0 (Val.cmp_bool Clt) v1 v2 zero32 - | CEbltuw optR0, v1 :: v2 :: nil => apply_bin_r0 optR0 (Val.cmpu_bool (Mem.valid_pointer m) Clt) v1 v2 zero32 - | CEbgew optR0, v1 :: v2 :: nil => apply_bin_r0 optR0 (Val.cmp_bool Cge) v1 v2 zero32 - | CEbgeuw optR0, v1 :: v2 :: nil => apply_bin_r0 optR0 (Val.cmpu_bool (Mem.valid_pointer m) Cge) v1 v2 zero32 - | CEbeql optR0, v1 :: v2 :: nil => apply_bin_r0 optR0 (Val.cmpl_bool Ceq) v1 v2 zero64 - | CEbnel optR0, v1 :: v2 :: nil => apply_bin_r0 optR0 (Val.cmpl_bool Cne) v1 v2 zero64 - | CEbequl optR0, v1 :: v2 :: nil => apply_bin_r0 optR0 (Val.cmplu_bool (Mem.valid_pointer m) Ceq) v1 v2 zero64 - | CEbneul optR0, v1 :: v2 :: nil => apply_bin_r0 optR0 (Val.cmplu_bool (Mem.valid_pointer m) Cne) v1 v2 zero64 - | CEbltl optR0, v1 :: v2 :: nil => apply_bin_r0 optR0 (Val.cmpl_bool Clt) v1 v2 zero64 - | CEbltul optR0, v1 :: v2 :: nil => apply_bin_r0 optR0 (Val.cmplu_bool (Mem.valid_pointer m) Clt) v1 v2 zero64 - | CEbgel optR0, v1 :: v2 :: nil => apply_bin_r0 optR0 (Val.cmpl_bool Cge) v1 v2 zero64 - | CEbgeul optR0, v1 :: v2 :: nil => apply_bin_r0 optR0 (Val.cmplu_bool (Mem.valid_pointer m) Cge) v1 v2 zero64 + | CEbeqw optR, v1 :: v2 :: nil => apply_bin_oreg optR (Val.cmp_bool Ceq) v1 v2 zero32 + | CEbnew optR, v1 :: v2 :: nil => apply_bin_oreg optR (Val.cmp_bool Cne) v1 v2 zero32 + | CEbequw optR, v1 :: v2 :: nil => apply_bin_oreg optR (Val.cmpu_bool (Mem.valid_pointer m) Ceq) v1 v2 zero32 + | CEbneuw optR, v1 :: v2 :: nil => apply_bin_oreg optR (Val.cmpu_bool (Mem.valid_pointer m) Cne) v1 v2 zero32 + | CEbltw optR, v1 :: v2 :: nil => apply_bin_oreg optR (Val.cmp_bool Clt) v1 v2 zero32 + | CEbltuw optR, v1 :: v2 :: nil => apply_bin_oreg optR (Val.cmpu_bool (Mem.valid_pointer m) Clt) v1 v2 zero32 + | CEbgew optR, v1 :: v2 :: nil => apply_bin_oreg optR (Val.cmp_bool Cge) v1 v2 zero32 + | CEbgeuw optR, v1 :: v2 :: nil => apply_bin_oreg optR (Val.cmpu_bool (Mem.valid_pointer m) Cge) v1 v2 zero32 + | CEbeql optR, v1 :: v2 :: nil => apply_bin_oreg optR (Val.cmpl_bool Ceq) v1 v2 zero64 + | CEbnel optR, v1 :: v2 :: nil => apply_bin_oreg optR (Val.cmpl_bool Cne) v1 v2 zero64 + | CEbequl optR, v1 :: v2 :: nil => apply_bin_oreg optR (Val.cmplu_bool (Mem.valid_pointer m) Ceq) v1 v2 zero64 + | CEbneul optR, v1 :: v2 :: nil => apply_bin_oreg optR (Val.cmplu_bool (Mem.valid_pointer m) Cne) v1 v2 zero64 + | CEbltl optR, v1 :: v2 :: nil => apply_bin_oreg optR (Val.cmpl_bool Clt) v1 v2 zero64 + | CEbltul optR, v1 :: v2 :: nil => apply_bin_oreg optR (Val.cmplu_bool (Mem.valid_pointer m) Clt) v1 v2 zero64 + | CEbgel optR, v1 :: v2 :: nil => apply_bin_oreg optR (Val.cmpl_bool Cge) v1 v2 zero64 + | CEbgeul optR, v1 :: v2 :: nil => apply_bin_oreg optR (Val.cmplu_bool (Mem.valid_pointer m) Cge) v1 v2 zero64 | _, _ => None end. +(** Assert sp is a pointer *) + +Definition get_sp sp := + match sp with + | Vptr _ _ => sp + | _ => Vundef + end. + Definition eval_operation (F V: Type) (genv: Genv.t F V) (sp: val) (op: operation) (vl: list val) (m: mem): option val := @@ -423,29 +463,36 @@ Definition eval_operation | Ofloat_of_bits, v1::nil => Some (ExtValues.float_of_bits v1) | Ocmp c, _ => Some (Val.of_optbool (eval_condition c vl m)) (* Expansed conditions *) - | OEseqw optR0, v1::v2::nil => Some (apply_bin_r0 optR0 (Val.cmp Ceq) v1 v2 zero32) - | OEsnew optR0, v1::v2::nil => Some (apply_bin_r0 optR0 (Val.cmp Cne) v1 v2 zero32) - | OEsequw optR0, v1::v2::nil => Some (apply_bin_r0 optR0 (Val.cmpu (Mem.valid_pointer m) Ceq) v1 v2 zero32) - | OEsneuw optR0, v1::v2::nil => Some (apply_bin_r0 optR0 (Val.cmpu (Mem.valid_pointer m) Cne) v1 v2 zero32) - | OEsltw optR0, v1::v2::nil => Some (apply_bin_r0 optR0 (Val.cmp Clt) v1 v2 zero32) - | OEsltuw optR0, v1::v2::nil => Some (apply_bin_r0 optR0 (Val.cmpu (Mem.valid_pointer m) Clt) v1 v2 zero32) + | OEseqw optR, v1::v2::nil => Some (apply_bin_oreg optR (Val.cmp Ceq) v1 v2 zero32) + | OEsnew optR, v1::v2::nil => Some (apply_bin_oreg optR (Val.cmp Cne) v1 v2 zero32) + | OEsequw optR, v1::v2::nil => Some (apply_bin_oreg optR (Val.cmpu (Mem.valid_pointer m) Ceq) v1 v2 zero32) + | OEsneuw optR, v1::v2::nil => Some (apply_bin_oreg optR (Val.cmpu (Mem.valid_pointer m) Cne) v1 v2 zero32) + | OEsltw optR, v1::v2::nil => Some (apply_bin_oreg optR (Val.cmp Clt) v1 v2 zero32) + | OEsltuw optR, v1::v2::nil => Some (apply_bin_oreg optR (Val.cmpu (Mem.valid_pointer m) Clt) v1 v2 zero32) | OEsltiw n, v1::nil => Some (Val.cmp Clt v1 (Vint n)) | OEsltiuw n, v1::nil => Some (Val.cmpu (Mem.valid_pointer m) Clt v1 (Vint n)) | OExoriw n, v1::nil => Some (Val.xor v1 (Vint n)) - | OEluiw n is_long, v1::nil => Some (may_undef_int is_long Val.shl v1 (Vint n) (Vint (Int.repr 12))) - | OEaddiwr0 n is_long, v1::nil => Some (may_undef_int is_long Val.add v1 (Vint n) zero32) - | OEseql optR0, v1::v2::nil => Some (Val.maketotal (apply_bin_r0 optR0 (Val.cmpl Ceq) v1 v2 zero64)) - | OEsnel optR0, v1::v2::nil => Some (Val.maketotal (apply_bin_r0 optR0 (Val.cmpl Cne) v1 v2 zero64)) - | OEsequl optR0, v1::v2::nil => Some (Val.maketotal (apply_bin_r0 optR0 (Val.cmplu (Mem.valid_pointer m) Ceq) v1 v2 zero64)) - | OEsneul optR0, v1::v2::nil => Some (Val.maketotal (apply_bin_r0 optR0 (Val.cmplu (Mem.valid_pointer m) Cne) v1 v2 zero64)) - | OEsltl optR0, v1::v2::nil => Some (Val.maketotal (apply_bin_r0 optR0 (Val.cmpl Clt) v1 v2 zero64)) - | OEsltul optR0, v1::v2::nil => Some (Val.maketotal (apply_bin_r0 optR0 (Val.cmplu (Mem.valid_pointer m) Clt) v1 v2 zero64)) + | OEluiw n, nil => Some (Val.shl (Vint n) (Vint (Int.repr 12))) + | OEaddiw optR n, nil => Some (apply_bin_oreg optR Val.add (Vint n) Vundef zero32) + | OEaddiw optR n, v1::nil => Some (apply_bin_oreg optR Val.add v1 (Vint n) Vundef) + | OEandiw n, v1::nil => Some (Val.and (Vint n) v1) + | OEoriw n, v1::nil => Some (Val.or (Vint n) v1) + | OEseql optR, v1::v2::nil => Some (Val.maketotal (apply_bin_oreg optR (Val.cmpl Ceq) v1 v2 zero64)) + | OEsnel optR, v1::v2::nil => Some (Val.maketotal (apply_bin_oreg optR (Val.cmpl Cne) v1 v2 zero64)) + | OEsequl optR, v1::v2::nil => Some (Val.maketotal (apply_bin_oreg optR (Val.cmplu (Mem.valid_pointer m) Ceq) v1 v2 zero64)) + | OEsneul optR, v1::v2::nil => Some (Val.maketotal (apply_bin_oreg optR (Val.cmplu (Mem.valid_pointer m) Cne) v1 v2 zero64)) + | OEsltl optR, v1::v2::nil => Some (Val.maketotal (apply_bin_oreg optR (Val.cmpl Clt) v1 v2 zero64)) + | OEsltul optR, v1::v2::nil => Some (Val.maketotal (apply_bin_oreg optR (Val.cmplu (Mem.valid_pointer m) Clt) v1 v2 zero64)) | OEsltil n, v1::nil => Some (Val.maketotal (Val.cmpl Clt v1 (Vlong n))) | OEsltiul n, v1::nil => Some (Val.maketotal (Val.cmplu (Mem.valid_pointer m) Clt v1 (Vlong n))) | OExoril n, v1::nil => Some (Val.xorl v1 (Vlong n)) - | OEluil n, v1::nil => Some (may_undef_luil v1 n) - | OEaddilr0 n, v1::nil => Some (may_undef_int true Val.addl v1 (Vlong n) zero64) + | OEluil n, nil => Some (Vlong (Int64.sign_ext 32 (Int64.shl n (Int64.repr 12)))) + | OEaddil optR n, nil => Some (apply_bin_oreg optR Val.addl (Vlong n) Vundef zero64) + | OEaddil optR n, v1::nil => Some (apply_bin_oreg optR Val.addl v1 (Vlong n) Vundef) + | OEandil n, v1::nil => Some (Val.andl (Vlong n) v1) + | OEoril n, v1::nil => Some (Val.orl (Vlong n) v1) | OEloadli n, nil => Some (Vlong n) + | OEmayundef mu, v1 :: v2 :: nil => Some (eval_may_undef mu v1 v2) | OEfeqd, v1::v2::nil => Some (Val.cmpf Ceq v1 v2) | OEfltd, v1::v2::nil => Some (Val.cmpf Clt v1 v2) | OEfled, v1::v2::nil => Some (Val.cmpf Cle v1 v2) @@ -530,6 +577,15 @@ Definition type_of_condition (c: condition) : list typ := | CEbgeul _ => Tlong :: Tlong :: nil end. +(** The type of mayundef and addsp is dynamic *) + +Definition type_of_mayundef mu := + match mu with + | MUint | MUshrx _ => (Tint :: Tint :: nil, Tint) + | MUlong => (Tlong :: Tint :: nil, Tint) + | MUshrxl _ => (Tlong :: Tlong :: nil, Tlong) + end. + Definition type_of_operation (op: operation) : list typ * typ := match op with | Omove => (nil, Tint) (* treated specially *) @@ -634,8 +690,11 @@ Definition type_of_operation (op: operation) : list typ * typ := | OEsltiw _ => (Tint :: nil, Tint) | OEsltiuw _ => (Tint :: nil, Tint) | OExoriw _ => (Tint :: nil, Tint) - | OEluiw _ _ => (Tint :: nil, Tint) - | OEaddiwr0 _ _ => (Tint :: nil, Tint) + | OEluiw _ => (nil, Tint) + | OEaddiw None _ => (Tint :: nil, Tint) + | OEaddiw (Some _) _ => (nil, Tint) + | OEandiw _ => (Tint :: nil, Tint) + | OEoriw _ => (Tint :: nil, Tint) | OEseql _ => (Tlong :: Tlong :: nil, Tint) | OEsnel _ => (Tlong :: Tlong :: nil, Tint) | OEsequl _ => (Tlong :: Tlong :: nil, Tint) @@ -644,10 +703,14 @@ Definition type_of_operation (op: operation) : list typ * typ := | OEsltul _ => (Tlong :: Tlong :: nil, Tint) | OEsltil _ => (Tlong :: nil, Tint) | OEsltiul _ => (Tlong :: nil, Tint) + | OEandil _ => (Tlong :: nil, Tlong) + | OEoril _ => (Tlong :: nil, Tlong) | OExoril _ => (Tlong :: nil, Tlong) - | OEluil _ => (Tlong :: nil, Tlong) - | OEaddilr0 _ => (Tlong :: nil, Tlong) + | OEluil _ => (nil, Tlong) + | OEaddil None _ => (Tlong :: nil, Tlong) + | OEaddil (Some _) _ => (nil, Tlong) | OEloadli _ => (nil, Tlong) + | OEmayundef mu => type_of_mayundef mu | OEfeqd => (Tfloat :: Tfloat :: nil, Tint) | OEfltd => (Tfloat :: Tfloat :: nil, Tint) | OEfled => (Tfloat :: Tfloat :: nil, Tint) @@ -689,6 +752,14 @@ Proof. intros. unfold Val.has_type, Val.addl. destruct Archi.ptr64, v1, v2; auto. Qed. +Remark type_mayundef: + forall mu v1 v2, Val.has_type (eval_may_undef mu v1 v2) (snd (type_of_mayundef mu)). +Proof. + intros. unfold eval_may_undef. + destruct mu eqn:EQMU, v1, v2; simpl; auto. + all: destruct Int.ltu; simpl; auto. +Qed. + Lemma type_of_operation_sound: forall op vl sp v m, op <> Omove -> @@ -698,7 +769,7 @@ Proof with (try exact I; try reflexivity; auto using Val.Vptr_has_type). intros. destruct op; simpl; simpl in H0; FuncInv; subst; simpl. (* move *) - - congruence. + - simpl in H; congruence. (* intconst, longconst, floatconst, singleconst *) - exact I. - exact I. @@ -866,67 +937,79 @@ Proof with (try exact I; try reflexivity; auto using Val.Vptr_has_type). (* cmp *) - destruct (eval_condition cond vl m)... destruct b... (* OEseqw *) - - destruct optR0 as [[]|]; simpl; unfold Val.cmp; + - destruct optR as [[]|]; simpl; unfold Val.cmp; destruct Val.cmp_bool... all: destruct b... (* OEsnew *) - - destruct optR0 as [[]|]; simpl; unfold Val.cmp; + - destruct optR as [[]|]; simpl; unfold Val.cmp; destruct Val.cmp_bool... all: destruct b... (* OEsequw *) - - destruct optR0 as [[]|]; simpl; unfold Val.cmpu; + - destruct optR as [[]|]; simpl; unfold Val.cmpu; destruct Val.cmpu_bool... all: destruct b... (* OEsneuw *) - - destruct optR0 as [[]|]; simpl; unfold Val.cmpu; + - destruct optR as [[]|]; simpl; unfold Val.cmpu; destruct Val.cmpu_bool... all: destruct b... (* OEsltw *) - - destruct optR0 as [[]|]; simpl; unfold Val.cmp; + - destruct optR as [[]|]; simpl; unfold Val.cmp; destruct Val.cmp_bool... all: destruct b... (* OEsltuw *) - - destruct optR0 as [[]|]; simpl; unfold Val.cmpu; + - destruct optR as [[]|]; simpl; unfold Val.cmpu; destruct Val.cmpu_bool... all: destruct b... (* OEsltiw *) - unfold Val.cmp; destruct Val.cmp_bool... all: destruct b... (* OEsltiuw *) - unfold Val.cmpu; destruct Val.cmpu_bool... destruct b... + (* OEaddiw *) + - destruct optR as [[]|]; simpl in *; trivial. + - destruct optR as [[]|]; simpl in *; trivial; + apply type_add. + (* OEandiw *) + - destruct v0... + (* OEoriw *) + - destruct v0... (* OExoriw *) - destruct v0... (* OEluiw *) - - unfold may_undef_int; - destruct v0, is_long; simpl; trivial; - destruct (Int.ltu _ _); cbn; trivial. - (* OEaddiwr0 *) - - destruct v0, is_long; simpl; trivial. + - destruct (Int.ltu _ _); cbn; trivial. (* OEseql *) - - destruct optR0 as [[]|]; simpl; unfold Val.cmpl; + - destruct optR as [[]|]; simpl; unfold Val.cmpl; destruct Val.cmpl_bool... all: destruct b... (* OEsnel *) - - destruct optR0 as [[]|]; simpl; unfold Val.cmpl; + - destruct optR as [[]|]; simpl; unfold Val.cmpl; destruct Val.cmpl_bool... all: destruct b... (* OEsequl *) - - destruct optR0 as [[]|]; simpl; unfold Val.cmplu; + - destruct optR as [[]|]; simpl; unfold Val.cmplu; destruct Val.cmplu_bool... all: destruct b... (* OEsneul *) - - destruct optR0 as [[]|]; simpl; unfold Val.cmplu; + - destruct optR as [[]|]; simpl; unfold Val.cmplu; destruct Val.cmplu_bool... all: destruct b... (* OEsltl *) - - destruct optR0 as [[]|]; simpl; unfold Val.cmpl; + - destruct optR as [[]|]; simpl; unfold Val.cmpl; destruct Val.cmpl_bool... all: destruct b... (* OEsltul *) - - destruct optR0 as [[]|]; simpl; unfold Val.cmplu; + - destruct optR as [[]|]; simpl; unfold Val.cmplu; destruct Val.cmplu_bool... all: destruct b... (* OEsltil *) - unfold Val.cmpl; destruct Val.cmpl_bool... all: destruct b... (* OEsltiul *) - unfold Val.cmplu; destruct Val.cmplu_bool... destruct b... + (* OEaddil *) + - destruct optR as [[]|]; simpl in *; trivial. + - destruct optR as [[]|]; simpl in *; trivial; + apply type_addl. + (* OEandil *) + - destruct v0... + (* OEoril *) + - destruct v0... (* OExoril *) - destruct v0... (* OEluil *) - - destruct v0; simpl; trivial. - (* OEaddilr0 *) - - destruct v0; simpl; trivial. + - simpl; trivial. (* OEloadli *) - trivial. + (* OEmayundef *) + - apply type_mayundef. (* OEfeqd *) - destruct v0; destruct v1; cbn; auto. destruct Float.cmp; cbn; auto. @@ -978,11 +1061,14 @@ Lemma is_trapping_op_sound: eval_operation genv sp op vl m <> None. Proof. unfold args_of_operation. - destruct op; destruct eq_operation; intros; simpl in *; try congruence. + destruct op eqn:E; destruct eq_operation; intros; simpl in *; try congruence. all: try (destruct vl as [ | vh1 vl1]; try discriminate). all: try (destruct vl1 as [ | vh2 vl2]; try discriminate). all: try (destruct vl2 as [ | vh3 vl3]; try discriminate). all: try (destruct vl3 as [ | vh4 vl4]; try discriminate). + all: try destruct optR as [[]|]; simpl in H0; try discriminate. + all: try destruct Archi.ptr64; simpl in *; try discriminate. + all: try destruct mu; simpl in *; try discriminate. Qed. End SOUNDNESS. @@ -1026,22 +1112,22 @@ Definition negate_condition (cond: condition): condition := | Cnotcompf c => Ccompf c | Ccompfs c => Cnotcompfs c | Cnotcompfs c => Ccompfs c - | CEbeqw optR0 => CEbnew optR0 - | CEbnew optR0 => CEbeqw optR0 - | CEbequw optR0 => CEbneuw optR0 - | CEbneuw optR0 => CEbequw optR0 - | CEbltw optR0 => CEbgew optR0 - | CEbltuw optR0 => CEbgeuw optR0 - | CEbgew optR0 => CEbltw optR0 - | CEbgeuw optR0 => CEbltuw optR0 - | CEbeql optR0 => CEbnel optR0 - | CEbnel optR0 => CEbeql optR0 - | CEbequl optR0 => CEbneul optR0 - | CEbneul optR0 => CEbequl optR0 - | CEbltl optR0 => CEbgel optR0 - | CEbltul optR0 => CEbgeul optR0 - | CEbgel optR0 => CEbltl optR0 - | CEbgeul optR0 => CEbltul optR0 + | CEbeqw optR => CEbnew optR + | CEbnew optR => CEbeqw optR + | CEbequw optR => CEbneuw optR + | CEbneuw optR => CEbequw optR + | CEbltw optR => CEbgew optR + | CEbltuw optR => CEbgeuw optR + | CEbgew optR => CEbltw optR + | CEbgeuw optR => CEbltuw optR + | CEbeql optR => CEbnel optR + | CEbnel optR => CEbeql optR + | CEbequl optR => CEbneul optR + | CEbneul optR => CEbequl optR + | CEbltl optR => CEbgel optR + | CEbltul optR => CEbgeul optR + | CEbgel optR => CEbltl optR + | CEbgeul optR => CEbltul optR end. Lemma eval_negate_condition: @@ -1062,37 +1148,37 @@ Proof. repeat (destruct vl; auto). repeat (destruct vl; auto). destruct (Val.cmpfs_bool c v v0) as [[]|]; auto. - repeat (destruct vl; auto); replace (Cne) with (negate_comparison Ceq) by auto; destruct optR0 as [[]|]; + repeat (destruct vl; auto); replace (Cne) with (negate_comparison Ceq) by auto; destruct optR as [[]|]; apply Val.negate_cmp_bool. - repeat (destruct vl; auto); replace (Ceq) with (negate_comparison Cne) by auto; destruct optR0 as [[]|]; + repeat (destruct vl; auto); replace (Ceq) with (negate_comparison Cne) by auto; destruct optR as [[]|]; apply Val.negate_cmp_bool. - repeat (destruct vl; auto); replace (Cne) with (negate_comparison Ceq) by auto; destruct optR0 as [[]|]; + repeat (destruct vl; auto); replace (Cne) with (negate_comparison Ceq) by auto; destruct optR as [[]|]; apply Val.negate_cmpu_bool. - repeat (destruct vl; auto); replace (Ceq) with (negate_comparison Cne) by auto; destruct optR0 as [[]|]; + repeat (destruct vl; auto); replace (Ceq) with (negate_comparison Cne) by auto; destruct optR as [[]|]; apply Val.negate_cmpu_bool. - repeat (destruct vl; auto); replace (Cge) with (negate_comparison Clt) by auto; destruct optR0 as [[]|]; + repeat (destruct vl; auto); replace (Cge) with (negate_comparison Clt) by auto; destruct optR as [[]|]; apply Val.negate_cmp_bool. - repeat (destruct vl; auto); replace (Cge) with (negate_comparison Clt) by auto; destruct optR0 as [[]|]; + repeat (destruct vl; auto); replace (Cge) with (negate_comparison Clt) by auto; destruct optR as [[]|]; apply Val.negate_cmpu_bool. - repeat (destruct vl; auto); replace (Clt) with (negate_comparison Cge) by auto; destruct optR0 as [[]|]; + repeat (destruct vl; auto); replace (Clt) with (negate_comparison Cge) by auto; destruct optR as [[]|]; apply Val.negate_cmp_bool. - repeat (destruct vl; auto); replace (Clt) with (negate_comparison Cge) by auto; destruct optR0 as [[]|]; + repeat (destruct vl; auto); replace (Clt) with (negate_comparison Cge) by auto; destruct optR as [[]|]; apply Val.negate_cmpu_bool. - repeat (destruct vl; auto); replace (Cne) with (negate_comparison Ceq) by auto; destruct optR0 as [[]|]; + repeat (destruct vl; auto); replace (Cne) with (negate_comparison Ceq) by auto; destruct optR as [[]|]; apply Val.negate_cmpl_bool. - repeat (destruct vl; auto); replace (Ceq) with (negate_comparison Cne) by auto; destruct optR0 as [[]|]; + repeat (destruct vl; auto); replace (Ceq) with (negate_comparison Cne) by auto; destruct optR as [[]|]; apply Val.negate_cmpl_bool. - repeat (destruct vl; auto); replace (Cne) with (negate_comparison Ceq) by auto; destruct optR0 as [[]|]; + repeat (destruct vl; auto); replace (Cne) with (negate_comparison Ceq) by auto; destruct optR as [[]|]; apply Val.negate_cmplu_bool. - repeat (destruct vl; auto); replace (Ceq) with (negate_comparison Cne) by auto; destruct optR0 as [[]|]; + repeat (destruct vl; auto); replace (Ceq) with (negate_comparison Cne) by auto; destruct optR as [[]|]; apply Val.negate_cmplu_bool. - repeat (destruct vl; auto); replace (Cge) with (negate_comparison Clt) by auto; destruct optR0 as [[]|]; + repeat (destruct vl; auto); replace (Cge) with (negate_comparison Clt) by auto; destruct optR as [[]|]; apply Val.negate_cmpl_bool. - repeat (destruct vl; auto); replace (Cge) with (negate_comparison Clt) by auto; destruct optR0 as [[]|]; + repeat (destruct vl; auto); replace (Cge) with (negate_comparison Clt) by auto; destruct optR as [[]|]; apply Val.negate_cmplu_bool. - repeat (destruct vl; auto); replace (Clt) with (negate_comparison Cge) by auto; destruct optR0 as [[]|]; + repeat (destruct vl; auto); replace (Clt) with (negate_comparison Cge) by auto; destruct optR as [[]|]; apply Val.negate_cmpl_bool. - repeat (destruct vl; auto); replace (Clt) with (negate_comparison Cge) by auto; destruct optR0 as [[]|]; + repeat (destruct vl; auto); replace (Clt) with (negate_comparison Cge) by auto; destruct optR as [[]|]; apply Val.negate_cmplu_bool. Qed. @@ -1119,7 +1205,8 @@ 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. + intros. destruct op; auto; + try destruct optR as [[]|]; simpl; auto. Qed. Lemma eval_shift_stack_addressing: @@ -1136,7 +1223,7 @@ Lemma eval_shift_stack_operation: 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. destruct vl; auto. + intros. destruct op eqn:E; simpl; auto; destruct vl; auto. rewrite Ptrofs.add_zero_l, Ptrofs.add_commut; auto. Qed. @@ -1237,7 +1324,7 @@ Proof. f_equal. f_equal. apply cond_depends_on_memory_correct; trivial. all: intros; repeat (destruct args; auto); unfold Val.cmpu, Val.cmpu_bool, Val.cmplu, Val.cmplu_bool; - try destruct optR0 as [[]|]; simpl; + try destruct optR as [[]|]; simpl; destruct v; try destruct v0; simpl; auto; try apply negb_false_iff in H; try rewrite H; auto. Qed. @@ -1249,7 +1336,7 @@ Lemma cond_valid_pointer_eq: Proof. intros until m2. intro MEM. destruct cond eqn:COND; simpl; try congruence. all: repeat (destruct args; simpl; try congruence); - try destruct optR0 as [[]|]; simpl; + try destruct optR as [[]|]; simpl; try destruct v, v0; try rewrite !MEM; auto; try erewrite cmpu_bool_valid_pointer_eq || erewrite cmplu_bool_valid_pointer_eq; eauto. Qed. @@ -1262,7 +1349,7 @@ Proof. intros until m2. destruct op; simpl; try congruence. intro MEM; erewrite cond_valid_pointer_eq; eauto. all: intros MEM; repeat (destruct args; simpl; try congruence); - try destruct optR0 as [[]|]; simpl; try destruct v, v0; try rewrite !MEM; auto; + try destruct optR as [[]|]; simpl; try destruct v, v0; try rewrite !MEM; auto; unfold Val.cmpu, Val.cmplu; erewrite cmpu_bool_valid_pointer_eq || erewrite cmplu_bool_valid_pointer_eq; eauto. Qed. @@ -1394,21 +1481,22 @@ Proof. intros EQ; rewrite EQ; destruct b; simpl; constructor; eauto. Qed. -Lemma eval_cmpu_bool_inj_opt: forall c v v' v0 v'0 optR0, +Lemma eval_cmpu_bool_inj_opt: forall c v v' v0 v'0 optR, Val.inject f v v' -> Val.inject f v0 v'0 -> - Val.inject f (apply_bin_r0 optR0 (Val.cmpu (Mem.valid_pointer m1) c) v v0 zero32) - (apply_bin_r0 optR0 (Val.cmpu (Mem.valid_pointer m2) c) v' v'0 zero32). + Val.inject f (apply_bin_oreg optR (Val.cmpu (Mem.valid_pointer m1) c) v v0 zero32) + (apply_bin_oreg optR (Val.cmpu (Mem.valid_pointer m2) c) v' v'0 zero32). Proof. - intros until optR0. intros HV1 HV2. - destruct optR0 as [[]|]; simpl; unfold zero32, Val.cmpu; + intros until optR. intros HV1 HV2. + destruct optR as [[]|]; simpl; unfold zero32, Val.cmpu; destruct (Val.cmpu_bool (Mem.valid_pointer m1) c _ _) eqn:?; eauto; assert (HVI: Val.inject f (Vint Int.zero) (Vint Int.zero)) by apply Val.inject_int. + exploit eval_cmpu_bool_inj'. eapply HVI. eapply HV1. eapply Heqo. intros EQ; rewrite EQ; destruct b; simpl; constructor; eauto. + exploit eval_cmpu_bool_inj'. eapply HV1. eapply HVI. eapply Heqo. intros EQ; rewrite EQ; destruct b; simpl; constructor; eauto. - + exploit eval_cmpu_bool_inj'. eapply HV1. eapply HV2. eapply Heqo. + + exploit eval_cmpu_bool_inj'. eapply HV1. instantiate (1:=v'0). + eauto. eapply Heqo. intros EQ; rewrite EQ; destruct b; simpl; constructor; eauto. Qed. @@ -1435,21 +1523,22 @@ Proof. intros EQ; rewrite EQ; destruct b; simpl; constructor; eauto. Qed. -Lemma eval_cmplu_bool_inj_opt: forall c v v' v0 v'0 optR0, +Lemma eval_cmplu_bool_inj_opt: forall c v v' v0 v'0 optR, Val.inject f v v' -> Val.inject f v0 v'0 -> - Val.inject f (Val.maketotal (apply_bin_r0 optR0 (Val.cmplu (Mem.valid_pointer m1) c) v v0 zero64)) - (Val.maketotal (apply_bin_r0 optR0 (Val.cmplu (Mem.valid_pointer m2) c) v' v'0 zero64)). + Val.inject f (Val.maketotal (apply_bin_oreg optR (Val.cmplu (Mem.valid_pointer m1) c) v v0 zero64)) + (Val.maketotal (apply_bin_oreg optR (Val.cmplu (Mem.valid_pointer m2) c) v' v'0 zero64)). Proof. - intros until optR0. intros HV1 HV2. - destruct optR0 as [[]|]; simpl; unfold zero64, Val.cmplu; + intros until optR. intros HV1 HV2. + destruct optR as [[]|]; simpl; unfold zero64, Val.cmplu; destruct (Val.cmplu_bool (Mem.valid_pointer m1) c _ _) eqn:?; eauto; assert (HVI: Val.inject f (Vlong Int64.zero) (Vlong Int64.zero)) by apply Val.inject_long. + exploit eval_cmplu_bool_inj'. eapply HVI. eapply HV1. eapply Heqo. intros EQ; rewrite EQ; destruct b; simpl; constructor; eauto. + exploit eval_cmplu_bool_inj'. eapply HV1. eapply HVI. eapply Heqo. intros EQ; rewrite EQ; destruct b; simpl; constructor; eauto. - + exploit eval_cmplu_bool_inj'. eapply HV1. eapply HV2. eapply Heqo. + + exploit eval_cmplu_bool_inj'. eapply HV1. instantiate (1:=v'0). + eauto. eapply Heqo. intros EQ; rewrite EQ; destruct b; simpl; constructor; eauto. Qed. @@ -1475,37 +1564,37 @@ Proof. - 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. -- destruct optR0 as [[]|]; unfold apply_bin_r0 in *; +- destruct optR as [[]|]; unfold apply_bin_oreg in *; inv H3; inv H2; simpl in H0; inv H0; auto. -- destruct optR0 as [[]|]; unfold apply_bin_r0 in *; +- destruct optR as [[]|]; unfold apply_bin_oreg in *; inv H3; inv H2; simpl in H0; inv H0; auto. -- destruct optR0 as [[]|]; unfold apply_bin_r0 in *; +- destruct optR as [[]|]; unfold apply_bin_oreg in *; eapply eval_cmpu_bool_inj'; eauto. -- destruct optR0 as [[]|]; unfold apply_bin_r0 in *; +- destruct optR as [[]|]; unfold apply_bin_oreg in *; eapply eval_cmpu_bool_inj'; eauto. -- destruct optR0 as [[]|]; simpl; +- destruct optR as [[]|]; simpl; inv H3; inv H2; simpl in H0; inv H0; auto. -- destruct optR0 as [[]|]; unfold apply_bin_r0 in *; +- destruct optR as [[]|]; unfold apply_bin_oreg in *; eapply eval_cmpu_bool_inj'; eauto. -- destruct optR0 as [[]|]; simpl; +- destruct optR as [[]|]; simpl; inv H3; inv H2; simpl in H0; inv H0; auto. -- destruct optR0 as [[]|]; unfold apply_bin_r0 in *; +- destruct optR as [[]|]; unfold apply_bin_oreg in *; eapply eval_cmpu_bool_inj'; eauto. -- destruct optR0 as [[]|]; unfold apply_bin_r0 in *; +- destruct optR as [[]|]; unfold apply_bin_oreg in *; inv H3; inv H2; simpl in H0; inv H0; auto. -- destruct optR0 as [[]|]; unfold apply_bin_r0 in *; +- destruct optR as [[]|]; unfold apply_bin_oreg in *; inv H3; inv H2; simpl in H0; inv H0; auto. -- destruct optR0 as [[]|]; unfold apply_bin_r0 in *; +- destruct optR as [[]|]; unfold apply_bin_oreg in *; eapply eval_cmplu_bool_inj'; eauto. -- destruct optR0 as [[]|]; unfold apply_bin_r0 in *; +- destruct optR as [[]|]; unfold apply_bin_oreg in *; eapply eval_cmplu_bool_inj'; eauto. -- destruct optR0 as [[]|]; simpl; +- destruct optR as [[]|]; simpl; inv H3; inv H2; simpl in H0; inv H0; auto. -- destruct optR0 as [[]|]; unfold apply_bin_r0 in *; +- destruct optR as [[]|]; unfold apply_bin_oreg in *; eapply eval_cmplu_bool_inj'; eauto. -- destruct optR0 as [[]|]; simpl; +- destruct optR as [[]|]; simpl; inv H3; inv H2; simpl in H0; inv H0; auto. -- destruct optR0 as [[]|]; unfold apply_bin_r0 in *; +- destruct optR as [[]|]; unfold apply_bin_oreg in *; eapply eval_cmplu_bool_inj'; eauto. Qed. @@ -1652,7 +1741,7 @@ Proof. (* shru, shruimm *) - inv H4; inv H2; simpl; auto. destruct (Int.ltu i0 Int64.iwordsize'); auto. - inv H4; simpl; auto. destruct (Int.ltu n Int64.iwordsize'); auto. - (* shrx *) + (* shrx *) - inv H4; cbn; try apply Val.val_inject_undef. destruct (Int.ltu n (Int.repr 63)); cbn. apply Val.inject_long. @@ -1716,11 +1805,11 @@ Proof. destruct b; simpl; constructor. simpl; constructor. (* OEseqw *) - - destruct optR0 as [[]|]; simpl; unfold zero32, Val.cmp; + - destruct optR as [[]|]; simpl; unfold zero32, Val.cmp; inv H4; inv H2; simpl; try destruct (Int.eq _ _); simpl; cbn; auto; try apply Val.inject_int. (* OEsnew *) - - destruct optR0 as [[]|]; simpl; unfold zero32, Val.cmp; + - destruct optR as [[]|]; simpl; unfold zero32, Val.cmp; inv H4; inv H2; simpl; try destruct (Int.eq _ _); simpl; cbn; auto; try apply Val.inject_int. (* OEsequw *) @@ -1728,7 +1817,7 @@ Proof. (* OEsneuw *) - apply eval_cmpu_bool_inj_opt; auto. (* OEsltw *) - - destruct optR0 as [[]|]; simpl; unfold zero32, Val.cmp; + - destruct optR as [[]|]; simpl; unfold zero32, Val.cmp; inv H4; inv H2; simpl; try destruct (Int.lt _ _); simpl; cbn; auto; try apply Val.inject_int. (* OEsltuw *) @@ -1737,23 +1826,26 @@ Proof. - inv H4; simpl; cbn; auto; try destruct (Int.lt _ _); apply Val.inject_int. (* OEsltiuw *) - apply eval_cmpu_bool_inj; auto. + (* OEaddiw *) + - destruct optR as [[]|]; auto; simpl. + rewrite Int.add_zero_l; auto. + rewrite Int.add_commut, Int.add_zero_l; auto. + - destruct optR as [[]|]; auto; simpl; + eapply Val.add_inject; auto. + (* OEandiw *) + - inv H4; cbn; auto. + (* OEoriw *) + - inv H4; cbn; auto. (* OExoriw *) - inv H4; simpl; auto. (* OEluiw *) - - unfold may_undef_int; - destruct is_long; - inv H4; simpl; auto; - destruct (Int.ltu _ _); auto. - (* OEaddiwr0 *) - - unfold may_undef_int; - destruct is_long; - inv H4; simpl; auto. + - destruct (Int.ltu _ _); auto. (* OEseql *) - - destruct optR0 as [[]|]; simpl; unfold zero64, Val.cmpl; + - destruct optR as [[]|]; simpl; unfold zero64, Val.cmpl; inv H4; inv H2; simpl; try destruct (Int64.eq _ _); simpl; cbn; auto; try apply Val.inject_int. (* OEsnel *) - - destruct optR0 as [[]|]; simpl; unfold zero64, Val.cmpl; + - destruct optR as [[]|]; simpl; unfold zero64, Val.cmpl; inv H4; inv H2; simpl; try destruct (Int64.eq _ _); simpl; cbn; auto; try apply Val.inject_int. (* OEsequl *) @@ -1761,7 +1853,7 @@ Proof. (* OEsneul *) - apply eval_cmplu_bool_inj_opt; auto. (* OEsltl *) - - destruct optR0 as [[]|]; simpl; unfold zero64, Val.cmpl; + - destruct optR as [[]|]; simpl; unfold zero64, Val.cmpl; inv H4; inv H2; simpl; try destruct (Int64.lt _ _); simpl; cbn; auto; try apply Val.inject_int. (* OEsltul *) @@ -1770,13 +1862,22 @@ Proof. - inv H4; simpl; cbn; auto; try destruct (Int64.lt _ _); apply Val.inject_int. (* OEsltiul *) - apply eval_cmplu_bool_inj; auto. + (* OEaddil *) + - destruct optR as [[]|]; auto; simpl. + rewrite Int64.add_zero_l; auto. + rewrite Int64.add_commut, Int64.add_zero_l; auto. + - destruct optR as [[]|]; auto; simpl; + eapply Val.addl_inject; auto. + (* OEandil *) + - inv H4; cbn; auto. + (* OEoril *) + - inv H4; cbn; auto. (* OExoril *) - inv H4; simpl; auto. - (* OEluil *) - - inv H4; simpl; auto. - (* OEaddilr0 *) - - unfold may_undef_int; - inv H4; simpl; auto. + (* OEmayundef *) + - destruct mu; inv H4; inv H2; simpl; auto; + try destruct (Int.ltu _ _); simpl; auto. + all: eapply Val.inject_ptr; eauto. (* OEfeqd *) - inv H4; inv H2; cbn; simpl; auto. destruct Float.cmp; unfold Vtrue, Vfalse; cbn; auto. |