From d2159e300b2d5e017a3144c747d34949b2ff2769 Mon Sep 17 00:00:00 2001 From: David Monniaux Date: Tue, 2 Feb 2021 10:21:17 +0100 Subject: begin implementing select --- riscV/Asm.v | 8 +++++-- riscV/Asmexpand.ml | 15 ++++++++++++- riscV/ExtValues.v | 10 +++++++++ riscV/NeedOp.v | 11 ++++++++++ riscV/Op.v | 16 +++++++++++++- riscV/TargetPrinter.ml | 2 ++ riscV/ValueAOp.v | 57 ++++++++++++++++++++++++++++++++++++++++++++++++-- 7 files changed, 113 insertions(+), 6 deletions(-) (limited to 'riscV') diff --git a/riscV/Asm.v b/riscV/Asm.v index d1946a06..9a4b2a57 100644 --- a/riscV/Asm.v +++ b/riscV/Asm.v @@ -63,10 +63,10 @@ Inductive freg: Type := | F24: freg | F25: freg | F26: freg | F27: freg | F28: freg | F29: freg | F30: freg | F31: freg. -Lemma ireg_eq: forall (x y: ireg), {x=y} + {x<>y}. +Definition ireg_eq: forall (x y: ireg), {x=y} + {x<>y}. Proof. decide equality. Defined. -Lemma ireg0_eq: forall (x y: ireg0), {x=y} + {x<>y}. +Definition ireg0_eq: forall (x y: ireg0), {x=y} + {x<>y}. Proof. decide equality. apply ireg_eq. Defined. Lemma freg_eq: forall (x y: freg), {x=y} + {x<>y}. @@ -348,6 +348,7 @@ Inductive instruction : Type := | Pbtbl (r: ireg) (tbl: list label) (**r N-way branch through a jump table *) | Pbuiltin: external_function -> list (builtin_arg preg) -> builtin_res preg -> instruction (**r built-in function (pseudo) *) + | Pselectl (rd: ireg) (rb: ireg0) (rt: ireg0) (rf: ireg0) | Pnop : instruction. (**r nop instruction *) @@ -954,6 +955,9 @@ Definition exec_instr (f: function) (i: instruction) (rs: regset) (m: mem) : out | _ => Stuck end end + | Pselectl rd rb rt rf => + Next (nextinstr (rs#rd <- (ExtValues.select01_long + (rs###rb) (rs###rt) (rs###rf)))) m | Plabel lbl => Next (nextinstr rs) m | Ploadsymbol rd s ofs => diff --git a/riscV/Asmexpand.ml b/riscV/Asmexpand.ml index 810514a3..9dd8cac9 100644 --- a/riscV/Asmexpand.ml +++ b/riscV/Asmexpand.ml @@ -582,9 +582,22 @@ let expand_builtin_inline name args res = raise (Error ("unrecognized builtin " ^ name)) (* Expansion of instructions *) - + let expand_instruction instr = match instr with + | Pselectl(rd, rb, rt, rf) -> + if not (ireg0_eq rt rf) + then + if (ireg0_eq (X rd) rt) || (ireg0_eq (X rd) rf) + then failwith "Pselectl" + else + begin + emit (Psubl(X31, X0, rb)); + emit (Paddil(rd, rb, Int64.mone)); + emit (Pandl(X31, X X31, rt)); + emit (Pandl(rd, X rd, rf)); + emit (Porl(rd, X rd, X X31)) + end | Pallocframe (sz, ofs) -> let sg = get_current_function_sig() in emit (Pmv (X30, X2)); diff --git a/riscV/ExtValues.v b/riscV/ExtValues.v index e0557de4..81688ca6 100644 --- a/riscV/ExtValues.v +++ b/riscV/ExtValues.v @@ -73,3 +73,13 @@ Definition select01_long (vb : val) (vtrue : val) (vfalse : val) : val := else Vundef | _ => Vundef end. + +Lemma normalize_select01: + forall x y z, Val.normalize (select01_long x y z) AST.Tlong = select01_long x (Val.normalize y AST.Tlong) (Val.normalize z AST.Tlong). +Proof. + unfold select01_long. + intros. + destruct x; cbn; trivial. + destruct (Int.eq i Int.one); trivial. + destruct (Int.eq i Int.zero); trivial. +Qed. diff --git a/riscV/NeedOp.v b/riscV/NeedOp.v index 136c157f..9e1ad004 100644 --- a/riscV/NeedOp.v +++ b/riscV/NeedOp.v @@ -91,6 +91,7 @@ Definition needs_of_operation (op: operation) (nv: nval): list nval := | Obits_of_float => op1 (default nv) | Osingle_of_bits => op1 (default nv) | Ofloat_of_bits => op1 (default nv) + | Oselectl => All :: nv :: nv :: nil end. Definition operation_is_redundant (op: operation) (nv: nval): bool := @@ -158,6 +159,16 @@ Proof. - apply shlimm_sound; auto. - apply shrimm_sound; auto. - apply shruimm_sound; auto. +- (* selectl *) + unfold ExtValues.select01_long. + destruct v0; auto with na. + assert (Val.lessdef (Vint i) v4) as LESSDEF by auto with na. + inv LESSDEF. + destruct (Int.eq i Int.one). + { apply normalize_sound; auto. } + destruct (Int.eq i Int.zero). + { apply normalize_sound; auto. } + cbn. auto with na. Qed. Lemma operation_is_redundant_sound: diff --git a/riscV/Op.v b/riscV/Op.v index 21de7787..64d5e4c9 100644 --- a/riscV/Op.v +++ b/riscV/Op.v @@ -157,7 +157,8 @@ Inductive operation : Type := | Obits_of_single | Obits_of_float | Osingle_of_bits - | Ofloat_of_bits. + | Ofloat_of_bits + | Oselectl. (** Addressing modes. [r1], [r2], etc, are the arguments to the addressing. *) @@ -327,6 +328,7 @@ Definition eval_operation | Osingle_of_bits, v1::nil => Some (ExtValues.single_of_bits v1) | Ofloat_of_bits, v1::nil => Some (ExtValues.float_of_bits v1) | Ocmp c, _ => Some (Val.of_optbool (eval_condition c vl m)) + | Oselectl, vb::vt::vf::nil => Some (Val.normalize (ExtValues.select01_long vb vt vf) Tlong) | _, _ => None end. @@ -487,6 +489,7 @@ Definition type_of_operation (op: operation) : list typ * typ := | Obits_of_float => (Tfloat :: nil, Tlong) | Osingle_of_bits => (Tint :: nil, Tsingle) | Ofloat_of_bits => (Tlong :: nil, Tfloat) + | Oselectl => (Tint :: Tlong :: Tlong :: nil, Tlong) end. Definition type_of_addressing (addr: addressing) : list typ := @@ -699,6 +702,12 @@ Proof with (try exact I; try reflexivity; auto using Val.Vptr_has_type). (* single, float of bits *) - destruct v0; cbn; trivial. - destruct v0; cbn; trivial. + (* selectl *) + - destruct v0; cbn; trivial. + destruct Int.eq; cbn. + apply Val.normalize_type. + destruct Int.eq; cbn; trivial. + apply Val.normalize_type. Qed. (* This should not be simplified to "false" because it breaks proofs elsewhere. *) @@ -1271,6 +1280,11 @@ Proof. (* single, double of bits *) - inv H4; simpl; auto. - inv H4; simpl; auto. + (* selectl *) + - inv H4; trivial. cbn. + destruct (Int.eq i Int.one). + + auto using Val.normalize_inject. + + destruct (Int.eq i Int.zero); cbn; auto using Val.normalize_inject. Qed. Lemma eval_addressing_inj: diff --git a/riscV/TargetPrinter.ml b/riscV/TargetPrinter.ml index 4bcfa6af..1f00c440 100644 --- a/riscV/TargetPrinter.ml +++ b/riscV/TargetPrinter.ml @@ -529,6 +529,8 @@ module Target : TARGET = fprintf oc " fcvt.s.d %a, %a\n" freg fd freg fs (* Pseudo-instructions expanded in Asmexpand *) + | Pselectl(_, _, _, _) -> + assert false | Pallocframe(sz, ofs) -> assert false | Pfreeframe(sz, ofs) -> diff --git a/riscV/ValueAOp.v b/riscV/ValueAOp.v index f94669a2..e779b114 100644 --- a/riscV/ValueAOp.v +++ b/riscV/ValueAOp.v @@ -66,6 +66,15 @@ Definition float_of_bits (v : aval) : aval := | _ => ntop1 v end. +Definition select01_long (vb : aval) (vt : aval) (vf : aval) := + match vb with + | I b => + if Int.eq b Int.one then add_undef vt + else if Int.eq b Int.zero then add_undef vf + else add_undef (vlub vt vf) + | _ => add_undef (vlub vt vf) + end. + Definition eval_static_operation (op: operation) (vl: list aval): aval := match op, vl with | Omove, v1::nil => v1 @@ -165,6 +174,7 @@ Definition eval_static_operation (op: operation) (vl: list aval): aval := | Obits_of_float, v1::nil => bits_of_float v1 | Osingle_of_bits, v1::nil => single_of_bits v1 | Ofloat_of_bits, v1::nil => float_of_bits v1 + | Oselectl, vb::vt::vf::nil => select01_long vb vt vf | _, _ => Vbot end. @@ -200,7 +210,50 @@ Proof. unfold ExtValues.bits_of_float; intros. inv H; cbn; constructor. Qed. -Hint Resolve bits_of_single_sound bits_of_float_sound single_of_bits_sound float_of_bits_sound : va. + +Lemma select01_long_sound: + forall vb xb vt xt vf xf + (MATCH_b : vmatch bc vb xb) + (MATCH_t : vmatch bc vt xt) + (MATCH_f : vmatch bc vf xf), + vmatch bc (Val.normalize (ExtValues.select01_long vb vt vf) Tlong) + (select01_long xb xt xf). +Proof. + intros. + inv MATCH_b; cbn; try apply add_undef_undef. + - destruct (Int.eq i Int.one). { apply add_undef_normalize; trivial. } + destruct (Int.eq i Int.zero). { apply add_undef_normalize; trivial. } + cbn. apply add_undef_undef. + - destruct (Int.eq i Int.one). + { apply add_undef_normalize. + apply vmatch_lub_l. + trivial. } + destruct (Int.eq i Int.zero). + { apply add_undef_normalize. + apply vmatch_lub_r. + trivial. } + cbn. apply add_undef_undef. + - destruct (Int.eq i Int.one). + { apply add_undef_normalize. + apply vmatch_lub_l. + trivial. } + destruct (Int.eq i Int.zero). + { apply add_undef_normalize. + apply vmatch_lub_r. + trivial. } + cbn. apply add_undef_undef. + - destruct (Int.eq i Int.one). + { apply add_undef_normalize. + apply vmatch_lub_l. + trivial. } + destruct (Int.eq i Int.zero). + { apply add_undef_normalize. + apply vmatch_lub_r. + trivial. } + cbn. apply add_undef_undef. +Qed. + +Hint Resolve bits_of_single_sound bits_of_float_sound single_of_bits_sound float_of_bits_sound select01_long_sound : va. Theorem eval_static_condition_sound: forall cond vargs m aargs, @@ -254,7 +307,7 @@ Proof. destruct addr; InvHyps; eauto with va. rewrite Ptrofs.add_zero_l; eauto with va. Qed. - + Theorem eval_static_operation_sound: forall op vargs m vres aargs, eval_operation ge (Vptr sp Ptrofs.zero) op vargs m = Some vres -> -- cgit