diff options
Diffstat (limited to 'riscV/Op.v')
| -rw-r--r-- | riscV/Op.v | 296 |
1 files changed, 187 insertions, 109 deletions
@@ -38,10 +38,12 @@ Set Implicit Arguments. (** Conditions (boolean-valued operators). *) -(* Type to modelize the use of a special register in arith operations *) +(** Type to modelize the use of a special register in arith operations *) + Inductive oreg: Type := | X0_L: oreg - | X0_R: oreg. + | X0_R: oreg + | SP_S: oreg. Inductive condition : Type := | Ccomp (c: comparison) (**r signed integer comparison *) @@ -75,17 +77,13 @@ Inductive condition : Type := | 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. -(* Type for allowing a single RTL constructor to perform an arith operation between an immediate and X0 *) -Inductive opimm: Type := - | OPimmADD: int -> opimm - | OPimmADDL: int64 -> opimm. - (** Arithmetic and logical operations. In the descriptions, [rd] is the result of the operation and [r1], [r2], etc, are the arguments. *) @@ -189,41 +187,41 @@ Inductive operation : Type := (*c Boolean tests: *) | Ocmp (cond: condition) (**r [rd = 1] if condition holds, [rd = 0] otherwise. *) (* Expansed conditions *) - | OEimmR0 (opi: opimm) + | OEmoveSP | 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 (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 *) + | 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 (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 *) + | 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 *) + | 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 @@ -277,47 +275,46 @@ Defined. *) Global Opaque eq_condition eq_addressing eq_operation. + +(** 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_oreg {B} (optR: option oreg) (sem: val -> val -> B) (v1 v2 vz: val): B := +Definition apply_bin_oreg {B} (optR: option oreg) (sem: val -> val -> B) (v1 v2 vz sp: val): B := match optR with | None => sem v1 v2 | Some X0_L => sem vz v1 | Some X0_R => sem v1 vz + | Some SP_S => sem v1 sp end. +(** Mayundef evaluation according to the above defined type *) + Definition eval_may_undef (mu: mayundef) (v1 v2: val): val := match mu with - | MUint => match v1 with - | Vint _ => v2 - | _ => Vundef + | MUint => match v1, v2 with + | Vint _, Vint _ => v2 + | _, _ => Vundef end - | MUlong => match v1 with - | Vlong _ => v2 - | _ => Vundef + | MUlong => match v1, v2 with + | Vlong _, Vint _ => v2 + | _, _ => Vundef end | MUshrx i => - match v1 with - | Vint _ => - if Int.ltu i (Int.repr 31) then v1 else Vundef - | _ => Vundef + match v1, v2 with + | Vint _, Vint _ => + if Int.ltu i (Int.repr 31) then v2 else Vundef + | _, _ => Vundef end | MUshrxl i => - match v1 with - | Vlong _ => - if Int.ltu i (Int.repr 63) then v1 else Vundef - | _ => Vundef + match v1, v2 with + | Vlong _, Vlong _ => + if Int.ltu i (Int.repr 63) then v2 else Vundef + | _, _ => Vundef end end. -Definition eval_opimmR0 (opi: opimm): val := - match opi with - | OPimmADD i => Val.add (Vint i) zero32 - | OPimmADDL i => Val.addl (Vlong i) zero64 - end. - (** * Evaluation functions *) (** Evaluation of conditions, operators and addressing modes applied @@ -340,25 +337,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 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 + | CEbeqw optR, v1 :: v2 :: nil => apply_bin_oreg optR (Val.cmp_bool Ceq) v1 v2 zero32 Vundef + | CEbnew optR, v1 :: v2 :: nil => apply_bin_oreg optR (Val.cmp_bool Cne) v1 v2 zero32 Vundef + | CEbequw optR, v1 :: v2 :: nil => apply_bin_oreg optR (Val.cmpu_bool (Mem.valid_pointer m) Ceq) v1 v2 zero32 Vundef + | CEbneuw optR, v1 :: v2 :: nil => apply_bin_oreg optR (Val.cmpu_bool (Mem.valid_pointer m) Cne) v1 v2 zero32 Vundef + | CEbltw optR, v1 :: v2 :: nil => apply_bin_oreg optR (Val.cmp_bool Clt) v1 v2 zero32 Vundef + | CEbltuw optR, v1 :: v2 :: nil => apply_bin_oreg optR (Val.cmpu_bool (Mem.valid_pointer m) Clt) v1 v2 zero32 Vundef + | CEbgew optR, v1 :: v2 :: nil => apply_bin_oreg optR (Val.cmp_bool Cge) v1 v2 zero32 Vundef + | CEbgeuw optR, v1 :: v2 :: nil => apply_bin_oreg optR (Val.cmpu_bool (Mem.valid_pointer m) Cge) v1 v2 zero32 Vundef + | CEbeql optR, v1 :: v2 :: nil => apply_bin_oreg optR (Val.cmpl_bool Ceq) v1 v2 zero64 Vundef + | CEbnel optR, v1 :: v2 :: nil => apply_bin_oreg optR (Val.cmpl_bool Cne) v1 v2 zero64 Vundef + | CEbequl optR, v1 :: v2 :: nil => apply_bin_oreg optR (Val.cmplu_bool (Mem.valid_pointer m) Ceq) v1 v2 zero64 Vundef + | CEbneul optR, v1 :: v2 :: nil => apply_bin_oreg optR (Val.cmplu_bool (Mem.valid_pointer m) Cne) v1 v2 zero64 Vundef + | CEbltl optR, v1 :: v2 :: nil => apply_bin_oreg optR (Val.cmpl_bool Clt) v1 v2 zero64 Vundef + | CEbltul optR, v1 :: v2 :: nil => apply_bin_oreg optR (Val.cmplu_bool (Mem.valid_pointer m) Clt) v1 v2 zero64 Vundef + | CEbgel optR, v1 :: v2 :: nil => apply_bin_oreg optR (Val.cmpl_bool Cge) v1 v2 zero64 Vundef + | CEbgeul optR, v1 :: v2 :: nil => apply_bin_oreg optR (Val.cmplu_bool (Mem.valid_pointer m) Cge) v1 v2 zero64 Vundef | _, _ => 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 := @@ -461,31 +466,41 @@ 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 *) - | OEimmR0 opi, nil => Some (eval_opimmR0 opi) - | 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) + | OEmoveSP, nil => Some (get_sp sp) + | OEseqw optR, v1::v2::nil => Some (apply_bin_oreg optR (Val.cmp Ceq) v1 v2 zero32 Vundef) + | OEsnew optR, v1::v2::nil => Some (apply_bin_oreg optR (Val.cmp Cne) v1 v2 zero32 Vundef) + | OEsequw optR, v1::v2::nil => Some (apply_bin_oreg optR (Val.cmpu (Mem.valid_pointer m) Ceq) v1 v2 zero32 Vundef) + | OEsneuw optR, v1::v2::nil => Some (apply_bin_oreg optR (Val.cmpu (Mem.valid_pointer m) Cne) v1 v2 zero32 Vundef) + | OEsltw optR, v1::v2::nil => Some (apply_bin_oreg optR (Val.cmp Clt) v1 v2 zero32 Vundef) + | OEsltuw optR, v1::v2::nil => Some (apply_bin_oreg optR (Val.cmpu (Mem.valid_pointer m) Clt) v1 v2 zero32 Vundef) | 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, nil => Some (Val.shl (Vint n) (Vint (Int.repr 12))) - | OEaddiw n, v1::nil => Some (Val.add (Vint n) v1) + | OEaddiw optR n, nil => Some (apply_bin_oreg optR Val.add (Vint n) Vundef zero32 Vundef) + | OEaddiw ((Some SP_S) as optR) n, v1::nil => + let sp' := Val.add (Vint n) (get_sp sp) in + Some (apply_bin_oreg optR Val.add v1 Vundef Vundef sp') + | OEaddiw optR n, v1::nil => + Some (apply_bin_oreg optR Val.add v1 (Vint n) Vundef (get_sp sp)) | 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)) + | OEseql optR, v1::v2::nil => Some (Val.maketotal (apply_bin_oreg optR (Val.cmpl Ceq) v1 v2 zero64 Vundef)) + | OEsnel optR, v1::v2::nil => Some (Val.maketotal (apply_bin_oreg optR (Val.cmpl Cne) v1 v2 zero64 Vundef)) + | OEsequl optR, v1::v2::nil => Some (Val.maketotal (apply_bin_oreg optR (Val.cmplu (Mem.valid_pointer m) Ceq) v1 v2 zero64 Vundef)) + | OEsneul optR, v1::v2::nil => Some (Val.maketotal (apply_bin_oreg optR (Val.cmplu (Mem.valid_pointer m) Cne) v1 v2 zero64 Vundef)) + | OEsltl optR, v1::v2::nil => Some (Val.maketotal (apply_bin_oreg optR (Val.cmpl Clt) v1 v2 zero64 Vundef)) + | OEsltul optR, v1::v2::nil => Some (Val.maketotal (apply_bin_oreg optR (Val.cmplu (Mem.valid_pointer m) Clt) v1 v2 zero64 Vundef)) | 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, nil => Some (Vlong (Int64.sign_ext 32 (Int64.shl n (Int64.repr 12)))) - | OEaddil n, v1::nil => Some (Val.addl (Vlong n) v1) + | OEaddil optR n, nil => Some (apply_bin_oreg optR Val.addl (Vlong n) Vundef zero64 Vundef) + | OEaddil ((Some SP_S) as optR) n, v1::nil => + let sp' := Val.addl (Vlong n) (get_sp sp) in + Some (apply_bin_oreg optR Val.addl v1 Vundef Vundef sp') + | OEaddil optR n, v1::nil => + Some (apply_bin_oreg optR Val.addl v1 (Vlong n) Vundef (get_sp sp)) | 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) @@ -574,12 +589,23 @@ Definition type_of_condition (c: condition) : list typ := | CEbgeul _ => Tlong :: Tlong :: nil end. -Definition type_of_opimmR0 (opi: opimm) : typ := - match opi with - | OPimmADD _ => Tint - | OPimmADDL _ => Tlong +(** 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_addsp (is_long: bool): list typ * typ := + if Archi.ptr64 then ( + if is_long then (Tlong :: nil, Tptr) + else (nil, Tint)) + else ( + if is_long then (nil, Tlong) + else (Tint :: nil, Tptr)). + Definition type_of_operation (op: operation) : list typ * typ := match op with | Omove => (nil, Tint) (* treated specially *) @@ -675,7 +701,7 @@ Definition type_of_operation (op: operation) : list typ * typ := | Osingleoflong => (Tlong :: nil, Tsingle) | Osingleoflongu => (Tlong :: nil, Tsingle) | Ocmp c => (type_of_condition c, Tint) - | OEimmR0 opi => (nil, type_of_opimmR0 opi) + | OEmoveSP => (nil, Tptr) | OEseqw _ => (Tint :: Tint :: nil, Tint) | OEsnew _ => (Tint :: Tint :: nil, Tint) | OEsequw _ => (Tint :: Tint :: nil, Tint) @@ -686,7 +712,9 @@ Definition type_of_operation (op: operation) : list typ * typ := | OEsltiuw _ => (Tint :: nil, Tint) | OExoriw _ => (Tint :: nil, Tint) | OEluiw _ => (nil, Tint) - | OEaddiw _ => (Tint :: nil, Tint) + | OEaddiw None _ => (Tint :: nil, Tint) + | OEaddiw (Some SP_S) _ => type_addsp false + | OEaddiw (Some _) _ => (nil, Tint) | OEandiw _ => (Tint :: nil, Tint) | OEoriw _ => (Tint :: nil, Tint) | OEseql _ => (Tlong :: Tlong :: nil, Tint) @@ -701,9 +729,11 @@ Definition type_of_operation (op: operation) : list typ * typ := | OEoril _ => (Tlong :: nil, Tlong) | OExoril _ => (Tlong :: nil, Tlong) | OEluil _ => (nil, Tlong) - | OEaddil _ => (Tlong :: nil, Tlong) + | OEaddil None _ => (Tlong :: nil, Tlong) + | OEaddil (Some SP_S) _ => type_addsp true + | OEaddil (Some _) _ => (nil, Tlong) | OEloadli _ => (nil, Tlong) - | OEmayundef _ => (Tany64 :: Tany64 :: nil, Tany64) + | OEmayundef mu => type_of_mayundef mu | OEfeqd => (Tfloat :: Tfloat :: nil, Tint) | OEfltd => (Tfloat :: Tfloat :: nil, Tint) | OEfled => (Tfloat :: Tfloat :: nil, Tint) @@ -746,7 +776,7 @@ Proof. Qed. Remark type_mayundef: - forall mu v1 v2, Val.has_type (eval_may_undef mu v1 v2) Tany64. + 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. @@ -762,7 +792,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. @@ -929,8 +959,9 @@ Proof with (try exact I; try reflexivity; auto using Val.Vptr_has_type). - destruct v0; cbn; trivial. (* cmp *) - destruct (eval_condition cond vl m)... destruct b... - (* OEimmR0 *) - - destruct opi; unfold eval_opimmR0; simpl; auto. + (* OEmoveSP *) + - destruct sp; unfold Tptr; destruct Archi.ptr64 eqn:?; + simpl; trivial. (* OEseqw *) - destruct optR as [[]|]; simpl; unfold Val.cmp; destruct Val.cmp_bool... all: destruct b... @@ -955,7 +986,12 @@ Proof with (try exact I; try reflexivity; auto using Val.Vptr_has_type). (* OEsltiuw *) - unfold Val.cmpu; destruct Val.cmpu_bool... destruct b... (* OEaddiw *) - - fold (Val.add (Vint n) v0); apply type_add. + - destruct optR as [[]|]; simpl in *; trivial; + destruct vl; inv H0; simpl; trivial; + destruct vl; inv H2; simpl; trivial; + destruct v0; simpl; trivial; + destruct (get_sp sp); destruct Archi.ptr64 eqn:HA; simpl; trivial; + unfold type_addsp, Tptr; try rewrite HA; simpl; trivial. (* OEandiw *) - destruct v0... (* OEoriw *) @@ -988,7 +1024,12 @@ Proof with (try exact I; try reflexivity; auto using Val.Vptr_has_type). (* OEsltiul *) - unfold Val.cmplu; destruct Val.cmplu_bool... destruct b... (* OEaddil *) - - fold (Val.addl (Vlong n) v0); apply type_addl. + - destruct optR as [[]|]; simpl in *; trivial; + destruct vl; inv H0; simpl; trivial; + destruct vl; inv H2; simpl; trivial; + destruct v0; simpl; trivial; + destruct (get_sp sp); destruct Archi.ptr64 eqn:HA; simpl; trivial; + unfold type_addsp, Tptr; try rewrite HA; simpl; trivial. (* OEandil *) - destruct v0... (* OEoril *) @@ -1052,11 +1093,15 @@ 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: unfold type_addsp in *; simpl in *. + all: try destruct Archi.ptr64; simpl in *; try discriminate. + all: try destruct mu; simpl in *; try discriminate. Qed. End SOUNDNESS. @@ -1181,6 +1226,9 @@ Definition shift_stack_addressing (delta: Z) (addr: addressing) := Definition shift_stack_operation (delta: Z) (op: operation) := match op with | Oaddrstack ofs => Oaddrstack (Ptrofs.add ofs (Ptrofs.repr delta)) + | OEmoveSP => Oaddrstack (Ptrofs.add Ptrofs.zero (Ptrofs.repr delta)) + | OEaddiw (Some SP_S) n => OEaddiw (Some SP_S) (Ptrofs.to_int (Ptrofs.add (Ptrofs.of_int n) (Ptrofs.repr delta))) + | OEaddil (Some SP_S) n => OEaddil (Some SP_S) (Ptrofs.to_int64 (Ptrofs.add (Ptrofs.of_int64 n) (Ptrofs.repr delta))) | _ => op end. @@ -1193,7 +1241,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: @@ -1210,8 +1259,21 @@ 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. - rewrite Ptrofs.add_zero_l, Ptrofs.add_commut; auto. + intros. destruct op eqn:E; simpl; auto; destruct vl; auto. + - rewrite Ptrofs.add_zero_l, Ptrofs.add_commut; auto. + - rewrite !Ptrofs.add_zero_l; auto. + - destruct optR as [[]|]; simpl; auto. + - destruct vl, optR as [[]|]; auto; unfold apply_bin_oreg; simpl; auto. + destruct v, Archi.ptr64 eqn:EA; simpl; try rewrite EA; simpl; auto. + rewrite Ptrofs.add_zero_l; auto. + rewrite Ptrofs.of_int_to_int; auto. + rewrite (Ptrofs.add_commut (Ptrofs.of_int n) (Ptrofs.repr delta)); reflexivity. + - destruct optR as [[]|]; simpl; auto. + - destruct vl, optR as [[]|]; auto; unfold apply_bin_oreg; simpl; auto. + destruct Archi.ptr64 eqn:EA; auto. + rewrite Ptrofs.add_zero_l; auto. + rewrite Ptrofs.of_int64_to_int64; auto. + rewrite (Ptrofs.add_commut (Ptrofs.of_int64 n) (Ptrofs.repr delta)); reflexivity. Qed. (** Offset an addressing mode [addr] by a quantity [delta], so that @@ -1471,8 +1533,8 @@ Qed. 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_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). + Val.inject f (apply_bin_oreg optR (Val.cmpu (Mem.valid_pointer m1) c) v v0 zero32 Vundef) + (apply_bin_oreg optR (Val.cmpu (Mem.valid_pointer m2) c) v' v'0 zero32 Vundef). Proof. intros until optR. intros HV1 HV2. destruct optR as [[]|]; simpl; unfold zero32, Val.cmpu; @@ -1482,6 +1544,9 @@ Proof. 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. do 2 instantiate (1:=Vundef). + eauto. eapply Heqo. + intros EQ; rewrite EQ; destruct b; simpl; constructor; eauto. + exploit eval_cmpu_bool_inj'. eapply HV1. eapply HV2. eapply Heqo. intros EQ; rewrite EQ; destruct b; simpl; constructor; eauto. Qed. @@ -1512,8 +1577,8 @@ Qed. 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_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)). + Val.inject f (Val.maketotal (apply_bin_oreg optR (Val.cmplu (Mem.valid_pointer m1) c) v v0 zero64 Vundef)) + (Val.maketotal (apply_bin_oreg optR (Val.cmplu (Mem.valid_pointer m2) c) v' v'0 zero64 Vundef)). Proof. intros until optR. intros HV1 HV2. destruct optR as [[]|]; simpl; unfold zero64, Val.cmplu; @@ -1523,6 +1588,9 @@ Proof. 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. do 2 instantiate (1:=Vundef). + eauto. eapply Heqo. + intros EQ; rewrite EQ; destruct b; simpl; constructor; eauto. + exploit eval_cmplu_bool_inj'. eapply HV1. eapply HV2. eapply Heqo. intros EQ; rewrite EQ; destruct b; simpl; constructor; eauto. Qed. @@ -1789,8 +1857,9 @@ Proof. exploit eval_condition_inj; eauto. intros EQ; rewrite EQ. destruct b; simpl; constructor. simpl; constructor. - (* OEimmR0 *) - - destruct opi; unfold eval_opimmR0; simpl; auto. + (* moveSP *) + - unfold get_sp; inv H; auto. + econstructor; eauto. (* OEseqw *) - destruct optR as [[]|]; simpl; unfold zero32, Val.cmp; inv H4; inv H2; simpl; try destruct (Int.eq _ _); simpl; cbn; auto; @@ -1814,9 +1883,14 @@ Proof. (* OEsltiuw *) - apply eval_cmpu_bool_inj; auto. (* OEaddiw *) - - fold (Val.add (Vint n) v); - fold (Val.add (Vint n) v'); + - destruct optR as [[]|]; auto; simpl; FuncInv; InvInject; TrivialExists; + try fold (Val.add (Vint n) (get_sp sp1)); + try fold (Val.add (Vint n) (get_sp sp2)); + (*try destruct (get_sp sp1), (get_sp sp2);*) apply Val.add_inject; auto. + apply Val.add_inject; auto. + destruct sp1, sp2; simpl; auto; + inv H. (* OEandiw *) - inv H4; cbn; auto. (* OEoriw *) @@ -1848,9 +1922,13 @@ Proof. (* OEsltiul *) - apply eval_cmplu_bool_inj; auto. (* OEaddil *) - - fold (Val.addl (Vlong n) v); - fold (Val.addl (Vlong n) v'); + - destruct optR as [[]|]; auto; simpl; FuncInv; InvInject; TrivialExists; + try fold (Val.addl (Vlong n) (get_sp sp1)); + try fold (Val.addl (Vlong n) (get_sp sp2)); + apply Val.addl_inject; auto. apply Val.addl_inject; auto. + destruct sp1, sp2; simpl; auto; + inv H. (* OEandil *) - inv H4; cbn; auto. (* OEoril *) |