Skip to content

GitLab

Commit b7720bc5 authored by Léo Gourdin's avatar Léo Gourdin
Browse files

Removing addptrofs draft, next will be merging

parent 2f2e7b1d
Hide whitespace changes
Inline Side-by-side
riscV/Asmgen.v
View file @ b7720bc5
......@@ -212,12 +212,10 @@ Definition apply_bin_oreg_ireg0 (optR: option oreg) (r1 r2: ireg0): (ireg0 * ire
| None => (r1, r2)
| Some X0_L => (X0, r1)
| Some X0_R => (r1, X0)
| Some SP_S => (X SP, r1)
end.
Definition get_oreg (optR: option oreg) (r: ireg0) :=
match optR with
| Some SP_S => X SP
| Some X0_L | Some X0_R => X0
| _ => r
end.
......@@ -846,12 +844,6 @@ Definition transl_op
do rd <- ireg_of res;
let rs := get_oreg optR X0 in
OK (Paddiw rd rs n :: k)
| OEaddiw (Some SP_S) n, a1 :: nil =>
do rd <- ireg_of res;
do rs <- ireg_of a1;
if Int.eq n Int.zero then
OK (Paddw rd SP rs :: k)
else Error (msg "Asmgen.transl_op")
| OEaddiw optR n, a1 :: nil =>
do rd <- ireg_of res;
do rs <- ireg_of a1;
......@@ -920,12 +912,6 @@ Definition transl_op
do rd <- ireg_of res;
let rs := get_oreg optR X0 in
OK (Paddil rd rs n :: k)
| OEaddil (Some SP_S) n, a1 :: nil =>
do rd <- ireg_of res;
do rs <- ireg_of a1;
if Int64.eq n Int64.zero then
OK (Paddl rd SP rs :: k)
else Error (msg "Asmgen.transl_op")
| OEaddil optR n, a1 :: nil =>
do rd <- ireg_of res;
do rs <- ireg_of a1;
......
riscV/Asmgenproof.v
View file @ b7720bc5
......@@ -320,8 +320,6 @@ Opaque Int.eq.
- destruct optR as [[]|]; simpl in *; TailNoLabel.
- destruct optR as [[]|]; simpl in *; TailNoLabel.
- destruct optR as [[]|]; simpl in *; TailNoLabel.
- destruct optR as [[]|]; simpl in *; TailNoLabel.
- destruct optR as [[]|]; simpl in *; TailNoLabel.
Qed.
Remark indexed_memory_access_label:
......
riscV/Asmgenproof1.v
View file @ b7720bc5
......@@ -1274,7 +1274,7 @@ Opaque Int.eq.
{ exploit transl_cond_op_correct; eauto. intros (rs' & A & B & C).
exists rs'; split. eexact A. eauto with asmgen. }
(* Expanded instructions from RTL *)
8,9,17,18:
9,10,19,20:
econstructor; split; try apply exec_straight_one; simpl; eauto;
split; intros; Simpl; try destruct (rs x0);
try rewrite Int64.add_commut;
......@@ -1283,9 +1283,8 @@ Opaque Int.eq.
try rewrite Int.and_commut; auto;
try rewrite Int64.or_commut;
try rewrite Int.or_commut; auto.
1-14:
1-16:
destruct optR as [[]|]; try discriminate;
try (ArgsInv; simpl in EV; SimplEval EV; try TranslOpSimpl);
unfold apply_bin_oreg_ireg0, apply_bin_oreg in *; try inv EQ3; try inv EQ2;
try destruct (Int.eq _ _) eqn:A; try inv H0;
try destruct (Int64.eq _ _) eqn:A; try inv H1;
......
riscV/ExpansionOracle.ml
View file @ b7720bc5
......@@ -606,31 +606,6 @@ let expanse_cbranch_fp vn cnot fn_cond cmp f1 f2 info succ1 succ2 =
Sfinalcond (CEbnew (Some X0_R), [ r'; r' ], succ1, succ2, info) :: l
else Sfinalcond (CEbeqw (Some X0_R), [ r'; r' ], succ1, succ2, info) :: l
let addptrofs vn n dest =
if Ptrofs.eq_dec n Ptrofs.zero then [ addinst vn OEmoveSP [] dest ]
else if Archi.ptr64 then
match make_immed64 (Ptrofs.to_int64 n) with
| Imm64_single imm -> [ addinst vn (OEaddil (Some SP_S, imm)) [] dest ]
| Imm64_pair (hi, lo) ->
let r = r2pi () in
let l = load_hilo64 vn r hi lo in
let r', l' = extract_arg l in
addinst vn (OEaddil (Some SP_S, Int64.zero)) [ r' ] dest :: l'
| Imm64_large imm ->
let r = r2pi () in
let op1 = OEloadli imm in
let i1 = addinst vn op1 [] r in
let r', l = extract_arg [ i1 ] in
addinst vn (OEaddil (Some SP_S, Int64.zero)) [ r' ] dest :: l
else
match make_immed32 (Ptrofs.to_int n) with
| Imm32_single imm -> [ addinst vn (OEaddiw (Some SP_S, imm)) [] dest ]
| Imm32_pair (hi, lo) ->
let r = r2pi () in
let l = load_hilo32 vn r hi lo in
let r', l' = extract_arg l in
addinst vn (OEaddiw (Some SP_S, Int.zero)) [ r' ] dest :: l'
(** Form a list containing both sources and destination regs of an instruction *)
let get_regindent = function Coq_inr _ -> [] | Coq_inl r -> [ r ]
......@@ -1033,11 +1008,6 @@ let expanse (sb : superblock) code pm =
exp := addinst vn (OEmayundef (MUshrxl n)) [ r4; r4 ] dest :: l4);
exp := extract_final vn !exp dest succ;
was_exp := true
(*| Iop (Oaddrstack n, nil, dest, succ) ->*)
(*if exp_debug then eprintf "Iop/Oaddrstack\n";*)
(*exp := addptrofs vn n dest;*)
(*exp := extract_final vn !exp dest succ;*)
(*was_exp := true*)
| _ -> ());
(* Update the CSE numbering *)
(if not !was_exp then
......
riscV/NeedOp.v
View file @ b7720bc5
......@@ -87,7 +87,6 @@ Definition needs_of_operation (op: operation) (nv: nval): list nval :=
| Ointofsingle | Ointuofsingle | Osingleofint | Osingleofintu => op1 (default nv)
| Olongofsingle | Olonguofsingle | Osingleoflong | Osingleoflongu => op1 (default nv)
| Ocmp c => needs_of_condition c
| OEmoveSP => nil
| OEseqw _ => op2 (default nv)
| OEsnew _ => op2 (default nv)
| OEsequw _ => op2 (default nv)
......
riscV/Op.v
View file @ b7720bc5
......@@ -42,8 +42,7 @@ Set Implicit Arguments.
Inductive oreg: Type :=
| X0_L: oreg
| X0_R: oreg
| SP_S: oreg.
| X0_R: oreg.
Inductive condition : Type :=
| Ccomp (c: comparison) (**r signed integer comparison *)
......@@ -187,7 +186,6 @@ Inductive operation : Type :=
(*c Boolean tests: *)
| Ocmp (cond: condition) (**r [rd = 1] if condition holds, [rd = 0] otherwise. *)
(* Expansed conditions *)
| 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 *)
......@@ -281,12 +279,11 @@ Global Opaque eq_condition eq_addressing eq_operation.
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 sp: val): B :=
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 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 *)
......@@ -337,22 +334,22 @@ 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 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
| 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.
......@@ -466,41 +463,32 @@ 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 *)
| 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)
| 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, 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 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))
| 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 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))
| 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, 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 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))
| 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)
......@@ -598,14 +586,6 @@ Definition type_of_mayundef mu :=
| 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 *)
......@@ -701,7 +681,6 @@ Definition type_of_operation (op: operation) : list typ * typ :=
| Osingleoflong => (Tlong :: nil, Tsingle)
| Osingleoflongu => (Tlong :: nil, Tsingle)
| Ocmp c => (type_of_condition c, Tint)
| OEmoveSP => (nil, Tptr)
| OEseqw _ => (Tint :: Tint :: nil, Tint)
| OEsnew _ => (Tint :: Tint :: nil, Tint)
| OEsequw _ => (Tint :: Tint :: nil, Tint)
......@@ -713,7 +692,6 @@ Definition type_of_operation (op: operation) : list typ * typ :=
| OExoriw _ => (Tint :: nil, Tint)
| OEluiw _ => (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)
......@@ -730,7 +708,6 @@ Definition type_of_operation (op: operation) : list typ * typ :=
| OExoril _ => (Tlong :: nil, Tlong)
| OEluil _ => (nil, Tlong)
| OEaddil None _ => (Tlong :: nil, Tlong)
| OEaddil (Some SP_S) _ => type_addsp true
| OEaddil (Some _) _ => (nil, Tlong)
| OEloadli _ => (nil, Tlong)
| OEmayundef mu => type_of_mayundef mu
......@@ -959,9 +936,6 @@ 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...
(* 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...
......@@ -986,12 +960,9 @@ Proof with (try exact I; try reflexivity; auto using Val.Vptr_has_type).
(* OEsltiuw *)
- unfold Val.cmpu; destruct Val.cmpu_bool... destruct b...
(* OEaddiw *)
- destruct optR as [[]|]; simpl in *; trivial.
- 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.
apply type_add.
(* OEandiw *)
- destruct v0...
(* OEoriw *)
......@@ -1024,12 +995,9 @@ Proof with (try exact I; try reflexivity; auto using Val.Vptr_has_type).
(* OEsltiul *)
- unfold Val.cmplu; destruct Val.cmplu_bool... destruct b...
(* OEaddil *)
- destruct optR as [[]|]; simpl in *; trivial.
- 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.
apply type_addl.
(* OEandil *)
- destruct v0...
(* OEoril *)
......@@ -1099,7 +1067,6 @@ Proof.
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.
......@@ -1226,9 +1193,6 @@ 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.
......@@ -1260,20 +1224,7 @@ Lemma eval_shift_stack_operation:
eval_operation ge (Vptr sp (Ptrofs.repr delta)) op vl m.
Proof.
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.
rewrite Ptrofs.add_zero_l, Ptrofs.add_commut; auto.
Qed.
(** Offset an addressing mode [addr] by a quantity [delta], so that
......@@ -1533,8 +1484,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 Vundef)
(apply_bin_oreg optR (Val.cmpu (Mem.valid_pointer m2) c) v' v'0 zero32 Vundef).
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 optR. intros HV1 HV2.
destruct optR as [[]|]; simpl; unfold zero32, Val.cmpu;
......@@ -1544,11 +1495,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).
+ exploit eval_cmpu_bool_inj'. eapply HV1. instantiate (1:=v'0).
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.
Lemma eval_cmplu_bool_inj': forall b c v v' v0 v0',
......@@ -1577,8 +1526,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 Vundef))
(Val.maketotal (apply_bin_oreg optR (Val.cmplu (Mem.valid_pointer m2) c) v' v'0 zero64 Vundef)).
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 optR. intros HV1 HV2.
destruct optR as [[]|]; simpl; unfold zero64, Val.cmplu;
......@@ -1588,11 +1537,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).
+ exploit eval_cmplu_bool_inj'. eapply HV1. instantiate (1:=v'0).
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.
Lemma eval_condition_inj:
......@@ -1857,9 +1804,6 @@ Proof.
exploit eval_condition_inj; eauto. intros EQ; rewrite EQ.
destruct b; simpl; constructor.
simpl; constructor.
(* 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;
......@@ -1883,14 +1827,11 @@ Proof.
(* OEsltiuw *)
- apply eval_cmpu_bool_inj; auto.
(* OEaddiw *)
- 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.
- 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 *)
......@@ -1922,13 +1863,11 @@ Proof.
(* OEsltiul *)
- apply eval_cmplu_bool_inj; auto.
(* OEaddil *)
- 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.
- 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 *)
......
riscV/PrintOp.ml
View file @ b7720bc5
......@@ -40,12 +40,10 @@ let get_optR_s c reg pp r1 r2 = function
| None -> fprintf pp "(%a %s %a)" reg r1 (comparison_name c) reg r2
| Some X0_L -> fprintf pp "(X0 %s %a)" (comparison_name c) reg r1
| Some X0_R -> fprintf pp "(%a %s X0)" reg r1 (comparison_name c)
| Some SP_S -> failwith "PrintOp: SP_S in get_optR_s instruction (problem with RTL expansions?)"
let get_optR_a pp = function
| None -> failwith "PrintOp: None in get_optR_a instruction (problem with RTL expansions?)"
| Some X0_L | Some X0_R -> fprintf pp "X0"
| Some SP_S -> fprintf pp "SP"
let print_condition reg pp = function
| (Ccomp c, [r1;r2]) ->
......
riscV/RTLpathSE_simplify.v
View file @ b7720bc5
......@@ -309,36 +309,6 @@ Definition expanse_cbranch_fp (cnot: bool) fn_cond cmp (lhsv: list_hsval) : (con
let hl := make_lhsv_cmp false hvs hvs in
if normal' then ((CEbnew (Some X0_R)), hl) else ((CEbeqw (Some X0_R)), hl).
(** ** Add pointer expansion *)
Definition addptrofs (n: ptrofs) :=
if Ptrofs.eq_dec n Ptrofs.zero then
fSop OEmoveSP fSnil
else
if Archi.ptr64
then (
match make_immed64 (Ptrofs.to_int64 n) with
| Imm64_single imm =>
fSop (OEaddil (Some SP_S) imm) fSnil
| Imm64_pair hi lo =>
let hvs := load_hilo64 hi lo in
let hl := make_lhsv_single hvs in
fSop (OEaddil (Some SP_S) Int64.zero) hl
| Imm64_large imm =>
let hvs := fSop (OEloadli imm) fSnil in
let hl := make_lhsv_single hvs in
fSop (OEaddil (Some SP_S) Int64.zero) hl
end)
else (
match make_immed32 (Ptrofs.to_int n) with
| Imm32_single imm =>
fSop (OEaddiw (Some SP_S) imm) fSnil
| Imm32_pair hi lo =>
let hvs := load_hilo32 hi lo in
let hl := make_lhsv_single hvs in
fSop (OEaddiw (Some SP_S) Int.zero) hl
end).
(** * Target simplifications using "fake" values *)
Definition target_op_simplify (op: operation) (lr: list reg) (hst: hsistate_local): option hsval :=
......@@ -507,8 +477,6 @@ Definition target_op_simplify (op: operation) (lr: list reg) (hst: hsistate_loca
let srail_s' := fSop (Oshrlimm n) addl_l in
let srail_l' := make_lhsv_cmp false srail_s' srail_s' in
Some (fSop (OEmayundef (MUshrxl n)) srail_l')
(* TODO gourdinl | Oaddrstack n, nil =>*)
(*Some (addptrofs n)*)
| _, _ => None
end.
......@@ -1943,8 +1911,6 @@ Proof.
eapply simplify_longconst_correct; eauto.
eapply simplify_floatconst_correct; eauto.
eapply simplify_singleconst_correct; eauto.
(* TODO gourdinl*)
(*admit.*)
eapply simplify_cast8signed_correct; eauto.
eapply simplify_cast16signed_correct; eauto.
eapply simplify_addimm_correct; eauto.
......@@ -1975,7 +1941,6 @@ Proof.
- eapply simplify_ccompfs_correct; eauto.
- eapply simplify_cnotcompfs_correct; eauto.
Qed.
(*Admitted.*)
Lemma target_cbranch_expanse_correct hst c l ge sp rs0 m0 st c' l': forall
(TARGET: target_cbranch_expanse hst c l = Some (c', l'))
......
riscV/ValueAOp.v
View file @ b7720bc5
......@@ -22,12 +22,11 @@ Definition zero64 := (L Int64.zero).
(** Functions to select a special register (see Op.v) *)
Definition apply_bin_oreg {B} (optR: option oreg) (sem: aval -> aval -> B) (v1 v2 vz sp: aval): B :=
Definition apply_bin_oreg {B} (optR: option oreg) (sem: aval -> aval -> B) (v1 v2 vz: aval): 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.
Definition eval_may_undef (mu: mayundef) (v1 v2: aval): aval :=
......@@ -68,22 +67,22 @@ Definition eval_static_condition (cond: condition) (vl: list aval): abool :=
| Cnotcompf c, v1 :: v2 :: nil => cnot (cmpf_bool c v1 v2)
| Ccompfs c, v1 :: v2 :: nil => cmpfs_bool c v1 v2
| Cnotcompfs c, v1 :: v2 :: nil => cnot (cmpfs_bool c v1 v2)
| CEbeqw optR, v1 :: v2 :: nil => apply_bin_oreg optR (cmp_bool Ceq) v1 v2 zero32 (Ifptr Ptop)
| CEbnew optR, v1 :: v2 :: nil => apply_bin_oreg optR (cmp_bool Cne) v1 v2 zero32 (Ifptr Ptop)
| CEbequw optR, v1 :: v2 :: nil => apply_bin_oreg optR (cmpu_bool Ceq) v1 v2 zero32 (Ifptr Ptop)
| CEbneuw optR, v1 :: v2 :: nil => apply_bin_oreg optR (cmpu_bool Cne) v1 v2 zero32 (Ifptr Ptop)
| CEbltw optR, v1 :: v2 :: nil => apply_bin_oreg optR (cmp_bool Clt) v1 v2 zero32 (Ifptr Ptop)
| CEbltuw optR, v1 :: v2 :: nil => apply_bin_oreg optR (cmpu_bool Clt) v1 v2 zero32 (Ifptr Ptop)
| CEbgew optR, v1 :: v2 :: nil => apply_bin_oreg optR (cmp_bool Cge) v1 v2 zero32 (Ifptr Ptop)
| CEbgeuw optR, v1 :: v2 :: nil => apply_bin_oreg optR (cmpu_bool Cge) v1 v2 zero32 (Ifptr Ptop)
| CEbeql optR, v1 :: v2 :: nil => apply_bin_oreg optR (cmpl_bool Ceq) v1 v2 zero64 (Ifptr Ptop)
| CEbnel optR, v1 :: v2 :: nil => apply_bin_oreg optR (cmpl_bool Cne) v1 v2 zero64 (Ifptr Ptop)
| CEbequl optR, v1 :: v2 :: nil => apply_bin_oreg optR (cmplu_bool Ceq) v1 v2 zero64 (Ifptr Ptop)