diff options
-rw-r--r-- | backend/Selectionproof.v | 4 | ||||
-rw-r--r-- | common/Values.v | 21 | ||||
-rwxr-xr-x | configure | 7 | ||||
-rw-r--r-- | riscV/Asm.v | 30 | ||||
-rw-r--r-- | riscV/Asmexpand.ml | 42 | ||||
-rw-r--r-- | riscV/Asmgen.v | 25 | ||||
-rw-r--r-- | riscV/Asmgenproof1.v | 48 | ||||
-rw-r--r-- | riscV/Builtins1.v | 27 | ||||
-rw-r--r-- | riscV/CBuiltins.ml | 8 | ||||
-rw-r--r-- | riscV/ExtValues.v | 123 | ||||
-rw-r--r-- | riscV/NeedOp.v | 15 | ||||
-rw-r--r-- | riscV/Op.v | 44 | ||||
-rw-r--r-- | riscV/PrintOp.ml | 5 | ||||
-rw-r--r-- | riscV/SelectOp.vp | 41 | ||||
-rw-r--r-- | riscV/SelectOpproof.v | 122 | ||||
-rw-r--r-- | riscV/TargetPrinter.ml | 6 | ||||
-rw-r--r-- | riscV/ValueAOp.v | 107 | ||||
-rw-r--r-- | test/monniaux/cmov/cmov.c | 22 | ||||
-rw-r--r-- | test/monniaux/cmov/cmov2.c | 28 |
19 files changed, 705 insertions, 20 deletions
diff --git a/backend/Selectionproof.v b/backend/Selectionproof.v index 4d075f4a..8f3f5f00 100644 --- a/backend/Selectionproof.v +++ b/backend/Selectionproof.v @@ -783,6 +783,8 @@ Lemma sel_select_opt_correct: Cminor.eval_expr ge sp e m cond vcond -> Cminor.eval_expr ge sp e m a1 v1 -> Cminor.eval_expr ge sp e m a2 v2 -> + Val.has_type v1 ty -> + Val.has_type v2 ty -> Val.bool_of_val vcond b -> env_lessdef e e' -> Mem.extends m m' -> exists v', eval_expr tge sp e' m' le a v' /\ Val.lessdef (Val.select (Some b) v1 v2 ty) v'. @@ -792,7 +794,7 @@ Proof. exploit sel_expr_correct. eexact H0. eauto. eauto. intros (vcond' & EVC & LDC). exploit sel_expr_correct. eexact H1. eauto. eauto. intros (v1' & EV1 & LD1). exploit sel_expr_correct. eexact H2. eauto. eauto. intros (v2' & EV2 & LD2). - assert (Val.bool_of_val vcond' b) by (inv H3; inv LDC; constructor). + assert (Val.bool_of_val vcond' b) by (inv H5; inv LDC; constructor). exploit eval_condition_of_expr. eexact EVC. eauto. rewrite C. intros (vargs' & EVARGS & EVCOND). exploit eval_select; eauto. intros (v' & X & Y). exists v'; split; eauto. diff --git a/common/Values.v b/common/Values.v index 4146dd59..5d32e54e 100644 --- a/common/Values.v +++ b/common/Values.v @@ -89,6 +89,27 @@ Definition has_type (v: val) (t: typ) : Prop := | _, _ => False end. +Definition has_type_b (v: val) (t: typ) := + match v, t with + | Vundef, _ => true + | Vint _, Tint => true + | Vlong _, Tlong => true + | Vfloat _, Tfloat => true + | Vsingle _, Tsingle => true + | Vptr _ _, Tint => negb Archi.ptr64 + | Vptr _ _, Tlong => Archi.ptr64 + | (Vint _ | Vsingle _), Tany32 => true + | Vptr _ _, Tany32 => negb Archi.ptr64 + | _, Tany64 => true + | _, _ => false + end. + +Lemma has_type_b_correct: forall v t, + has_type_b v t = true <-> has_type v t. +Proof. + destruct v; destruct t; cbn; destruct Archi.ptr64; cbn; split; intros; auto; discriminate. +Qed. + Fixpoint has_type_list (vl: list val) (tl: list typ) {struct vl} : Prop := match vl, tl with | nil, nil => True @@ -842,6 +842,13 @@ BACKENDLIB=Machblock.v Machblockgen.v Machblockgenproof.v\\ EOF fi +if [ "$arch" = "riscV" ] ; then +cat >> Makefile.config <<EOF +EXTRA_EXTRACTION=Asm.ireg_eq Asm.ireg0_eq +BACKENDLIB=Asmgenproof0.v Asmgenproof1.v ExtValues.v +EOF +fi + # # Generate Merlin and CoqProject files to simplify development # diff --git a/riscV/Asm.v b/riscV/Asm.v index dc410a3b..5d3518f2 100644 --- a/riscV/Asm.v +++ b/riscV/Asm.v @@ -30,6 +30,7 @@ Require Import Smallstep. Require Import Locations. Require Stacklayout. Require Import Conventions. +Require ExtValues. (** * Abstract syntax *) @@ -62,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}. @@ -255,8 +256,10 @@ Inductive instruction : Type := (* floating point register move *) | Pfmv (rd: freg) (rs: freg) (**r move *) - | Pfmvxs (rd: ireg) (rs: freg) (**r move FP single to integer register *) - | Pfmvxd (rd: ireg) (rs: freg) (**r move FP double to integer register *) + | Pfmvxs (rd: ireg) (rs: freg) (**r bitwise move FP single to integer register *) + | Pfmvxd (rd: ireg) (rs: freg) (**r bitwise move FP double to integer register *) + | Pfmvsx (rd: freg) (rs: ireg) (**r bitwise move integer register to FP single *) + | Pfmvdx (rd: freg) (rs: ireg) (**r bitwise move integer register to FP double*) (* 32-bit (single-precision) floating point *) | Pfls (rd: freg) (ra: ireg) (ofs: offset) (**r load float *) @@ -345,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 *) @@ -918,6 +922,17 @@ Definition exec_instr (f: function) (i: instruction) (rs: regset) (m: mem) : out Next (nextinstr (rs#d <- (Val.floatofsingle rs#s))) m | Pfcvtsd d s => Next (nextinstr (rs#d <- (Val.singleoffloat rs#s))) m + + | Pfmvxs d s => + Next (nextinstr (rs#d <- (ExtValues.bits_of_single rs#s))) m + | Pfmvxd d s => + Next (nextinstr (rs#d <- (ExtValues.bits_of_float rs#s))) m + + | Pfmvsx d s => + Next (nextinstr (rs#d <- (ExtValues.single_of_bits rs#s))) m + | Pfmvdx d s => + Next (nextinstr (rs#d <- (ExtValues.float_of_bits rs#s))) m + (** Pseudo-instructions *) | Pallocframe sz pos => @@ -940,6 +955,10 @@ 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))) + #X31 <- Vundef) m | Plabel lbl => Next (nextinstr rs) m | Ploadsymbol rd s ofs => @@ -968,9 +987,6 @@ Definition exec_instr (f: function) (i: instruction) (rs: regset) (m: mem) : out so we do not model them. *) | Pfence - | Pfmvxs _ _ - | Pfmvxd _ _ - | Pfmins _ _ _ | Pfmaxs _ _ _ | Pfsqrts _ _ diff --git a/riscV/Asmexpand.ml b/riscV/Asmexpand.ml index 810514a3..c5cd6817 100644 --- a/riscV/Asmexpand.ml +++ b/riscV/Asmexpand.ml @@ -582,9 +582,49 @@ 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 Archi.ptr64 + then failwith "Pselectl not available on RV32, only on RV64" + else + if ireg0_eq rt rf then + begin + if ireg0_eq (X rd) rt then + begin + end + else + begin + emit (Paddl(rd, X0, rt)) + end + end + else + if (ireg0_eq (X rd) rt) then + begin + emit (Psubl(X31, X0, rb)); + emit (Pandl(X31, X X31, rt)); + emit (Paddil(rd, rb, Int64.mone)); + emit (Pandl(rd, X rd, rf)); + emit (Porl(rd, X rd, X X31)) + end + else + if (ireg0_eq (X rd) rf) then + begin + emit (Paddil(X31, rb, Int64.mone)); + emit (Pandl(X31, X X31, rf)); + emit (Psubl(rd, X0, rb)); + emit (Pandl(rd, X rd, rt)); + emit (Porl(rd, X rd, X X31)) + end + 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/Asmgen.v b/riscV/Asmgen.v index 4876f7ec..252a9270 100644 --- a/riscV/Asmgen.v +++ b/riscV/Asmgen.v @@ -899,6 +899,31 @@ Definition transl_op do r1 <- freg_of f1; do r2 <- freg_of f2; OK (Pfles rd r1 r2 :: k) + + | Obits_of_single, a1 :: nil => + do rd <- ireg_of res; do rs <- freg_of a1; + OK (Pfmvxs rd rs :: k) + | Obits_of_float, a1 :: nil => + do rd <- ireg_of res; do rs <- freg_of a1; + OK (Pfmvxd rd rs :: k) + | Osingle_of_bits, a1 :: nil => + do rd <- freg_of res; do rs <- ireg_of a1; + OK (Pfmvsx rd rs :: k) + | Ofloat_of_bits, a1 :: nil => + do rd <- freg_of res; do rs <- ireg_of a1; + OK (Pfmvdx rd rs :: k) + + | Ocmp cmp, _ => + do rd <- ireg_of res; + transl_cond_op cmp rd args k + + | Oselectl, b::t::f::nil => + do rd <- ireg_of res; + do rb <- ireg_of b; + do rt <- ireg_of t; + do rf <- ireg_of f; + OK (Pselectl rd rb rt rf :: k) + | _, _ => Error(msg "Asmgen.transl_op") end. diff --git a/riscV/Asmgenproof1.v b/riscV/Asmgenproof1.v index a826455e..1b3a0dbf 100644 --- a/riscV/Asmgenproof1.v +++ b/riscV/Asmgenproof1.v @@ -1268,6 +1268,54 @@ Opaque Int.eq. split; intros; Simpl. all: destruct (rs x0); auto. all: destruct (rs x1); auto. + exists rs'; split; eauto. rewrite B; auto with asmgen. +- (* shrxlimm *) + destruct (Val.shrxl (rs x0) (Vint n)) eqn:TOTAL. + { + exploit Val.shrxl_shrl_3; eauto. intros E; subst v. + destruct (Int.eq n Int.zero). ++ econstructor; split. apply exec_straight_one. simpl; eauto. auto. + split; intros; Simpl. ++ destruct (Int.eq n Int.one). + * econstructor; split. + eapply exec_straight_step. simpl; reflexivity. auto. + eapply exec_straight_step. simpl; reflexivity. auto. + apply exec_straight_one. simpl; reflexivity. auto. + split; intros; Simpl. + + * change (Int.repr 64) with Int64.iwordsize'. set (n' := Int.sub Int64.iwordsize' n). + econstructor; split. + eapply exec_straight_step. simpl; reflexivity. auto. + eapply exec_straight_step. simpl; reflexivity. auto. + eapply exec_straight_step. simpl; reflexivity. auto. + apply exec_straight_one. simpl; reflexivity. auto. + split; intros; Simpl. + } + destruct (Int.eq n Int.zero). ++ econstructor; split. apply exec_straight_one. simpl; eauto. auto. + split; intros; Simpl. ++ destruct (Int.eq n Int.one). + * econstructor; split. + eapply exec_straight_step. simpl; reflexivity. auto. + eapply exec_straight_step. simpl; reflexivity. auto. + apply exec_straight_one. simpl; reflexivity. auto. + split; intros; Simpl. + + * change (Int.repr 64) with Int64.iwordsize'. set (n' := Int.sub Int64.iwordsize' n). + econstructor; split. + eapply exec_straight_step. simpl; reflexivity. auto. + eapply exec_straight_step. simpl; reflexivity. auto. + eapply exec_straight_step. simpl; reflexivity. auto. + apply exec_straight_one. simpl; reflexivity. auto. + split; intros; Simpl. + +- (* cond *) + exploit transl_cond_op_correct; eauto. intros (rs' & A & B & C). + exists rs'; split. eexact A. eauto with asmgen. +- (* select *) + econstructor; split. apply exec_straight_one. simpl; eauto. auto. + split; intros; Simpl. + apply Val.lessdef_normalize. Qed. (** Memory accesses *) diff --git a/riscV/Builtins1.v b/riscV/Builtins1.v index 53c83d7e..47bacffa 100644 --- a/riscV/Builtins1.v +++ b/riscV/Builtins1.v @@ -18,16 +18,35 @@ Require Import String Coqlib. Require Import AST Integers Floats Values. Require Import Builtins0. +Require ExtValues. -Inductive platform_builtin : Type := . +Inductive platform_builtin : Type := +| BI_bits_of_float +| BI_bits_of_double +| BI_float_of_bits +| BI_double_of_bits. Local Open Scope string_scope. Definition platform_builtin_table : list (string * platform_builtin) := - nil. + ("__builtin_bits_of_float", BI_bits_of_float) + :: ("__builtin_bits_of_double", BI_bits_of_double) + :: ("__builtin_float_of_bits", BI_float_of_bits) + :: ("__builtin_double_of_bits", BI_double_of_bits) + :: nil. Definition platform_builtin_sig (b: platform_builtin) : signature := - match b with end. + match b with + | BI_bits_of_float => mksignature (Tsingle :: nil) Tint cc_default + | BI_bits_of_double => mksignature (Tfloat :: nil) Tlong cc_default + | BI_float_of_bits => mksignature (Tint :: nil) Tsingle cc_default + | BI_double_of_bits => mksignature (Tlong :: nil) Tfloat cc_default + end. Definition platform_builtin_sem (b: platform_builtin) : builtin_sem (sig_res (platform_builtin_sig b)) := - match b with end. + match b with + | BI_bits_of_float => mkbuiltin_n1t Tsingle Tint Float32.to_bits + | BI_bits_of_double => mkbuiltin_n1t Tfloat Tlong Float.to_bits + | BI_float_of_bits => mkbuiltin_n1t Tint Tsingle Float32.of_bits + | BI_double_of_bits => mkbuiltin_n1t Tlong Tfloat Float.of_bits + end. diff --git a/riscV/CBuiltins.ml b/riscV/CBuiltins.ml index a2087cb7..00b44fd5 100644 --- a/riscV/CBuiltins.ml +++ b/riscV/CBuiltins.ml @@ -46,6 +46,14 @@ let builtins = { (TFloat(FDouble, []), [TFloat(FDouble, []); TFloat(FDouble, [])], false); "__builtin_fmin", (TFloat(FDouble, []), [TFloat(FDouble, []); TFloat(FDouble, [])], false); + "__builtin_bits_of_double", + (TInt(IULong, []), [TFloat(FDouble, [])], false); + "__builtin_bits_of_float", + (TInt(IUInt, []), [TFloat(FFloat, [])], false); + "__builtin_double_of_bits", + (TFloat(FDouble, []), [TInt(IULong, [])], false); + "__builtin_float_of_bits", + (TFloat(FFloat, []), [TInt(IUInt, [])], false); ] } diff --git a/riscV/ExtValues.v b/riscV/ExtValues.v new file mode 100644 index 00000000..edf359ef --- /dev/null +++ b/riscV/ExtValues.v @@ -0,0 +1,123 @@ +Require Import Coqlib. +Require Import Integers. +Require Import Values. +Require Import Floats. +Require Import Memory. +Require Import Lia. + +Definition bits_of_float x := + match x with + | Vfloat f => Vlong (Float.to_bits f) + | _ => Vundef + end. + +Definition bits_of_single x := + match x with + | Vsingle f => Vint (Float32.to_bits f) + | _ => Vundef + end. + +Definition float_of_bits x := + match x with + | Vlong f => Vfloat (Float.of_bits f) + | _ => Vundef + end. + +Definition single_of_bits x := + match x with + | Vint f => Vsingle (Float32.of_bits f) + | _ => Vundef + end. + +Definition bitwise_select_long b vtrue vfalse := + Int64.or (Int64.and (Int64.neg b) vtrue) + (Int64.and (Int64.sub b Int64.one) vfalse). + +Lemma bitwise_select_long_true : + forall vtrue vfalse, + bitwise_select_long Int64.one vtrue vfalse = vtrue. +Proof. + intros. unfold bitwise_select_long. cbn. + change (Int64.neg Int64.one) with Int64.mone. + rewrite Int64.and_commut. + rewrite Int64.and_mone. + rewrite Int64.sub_idem. + rewrite Int64.and_commut. + rewrite Int64.and_zero. + apply Int64.or_zero. +Qed. + +Lemma bitwise_select_long_false : + forall vtrue vfalse, + bitwise_select_long Int64.zero vtrue vfalse = vfalse. +Proof. + intros. unfold bitwise_select_long. cbn. + rewrite Int64.neg_zero. + rewrite Int64.and_commut. + rewrite Int64.and_zero. + rewrite Int64.sub_zero_r. + change (Int64.neg Int64.one) with Int64.mone. + rewrite Int64.and_commut. + rewrite Int64.and_mone. + rewrite Int64.or_commut. + apply Int64.or_zero. +Qed. + +Definition select01_long (vb : val) (vtrue : val) (vfalse : val) : val := + match vb with + | (Vint b) => + if Int.eq b Int.one + then vtrue + else if Int.eq b Int.zero + then vfalse + 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. + +Lemma select01_long_true: + forall vt vf, + select01_long Vtrue vt vf = vt. +Proof. + intros. unfold select01_long. cbn. + rewrite Int.eq_true. reflexivity. +Qed. + +Lemma select01_long_false: + forall vt vf, + select01_long Vfalse vt vf = vf. +Proof. + intros. unfold select01_long. cbn. + rewrite Int.eq_true. + rewrite Int.eq_false. reflexivity. + cbv. discriminate. +Qed. + +Lemma float_bits_normalize: + forall v1, + ExtValues.float_of_bits (Val.normalize (ExtValues.bits_of_float v1) AST.Tlong) = + Val.normalize v1 AST.Tfloat. +Proof. + destruct v1; cbn; trivial. + f_equal. + apply Float.of_to_bits. +Qed. + +Lemma single_bits_normalize: + forall v1, + ExtValues.single_of_bits (Val.normalize (ExtValues.bits_of_single v1) AST.Tint) = + Val.normalize v1 AST.Tsingle. +Proof. + destruct v1; cbn; trivial. + f_equal. + apply Float32.of_to_bits. +Qed. diff --git a/riscV/NeedOp.v b/riscV/NeedOp.v index d90c1b66..4b309f5b 100644 --- a/riscV/NeedOp.v +++ b/riscV/NeedOp.v @@ -116,6 +116,11 @@ Definition needs_of_operation (op: operation) (nv: nval): list nval := | OEfeqs => op2 (default nv) | OEflts => op2 (default nv) | OEfles => op2 (default nv) + | Obits_of_single => op1 (default nv) + | 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 := @@ -184,6 +189,16 @@ Proof. - apply shrimm_sound; auto. - apply shruimm_sound; auto. - apply xor_sound; auto with na. +- (* 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: @@ -32,6 +32,7 @@ Require Import BoolEqual Coqlib. Require Import AST Integers Floats. Require Import Values Memory Globalenvs Events. +Require ExtValues. Set Implicit Arguments. @@ -200,6 +201,12 @@ Inductive operation : Type := | OEfeqs (**r compare equal *) | OEflts (**r compare less-than *) | OEfles. (**r compare less-than/equal *) + | Ocmp (cond: condition) (**r [rd = 1] if condition holds, [rd = 0] otherwise. *) + | Obits_of_single + | Obits_of_float + | Osingle_of_bits + | Ofloat_of_bits + | Oselectl. (** Addressing modes. [r1], [r2], etc, are the arguments to the addressing. *) @@ -411,6 +418,10 @@ Definition eval_operation | Olonguofsingle, v1::nil => Some (Val.maketotal (Val.longuofsingle v1)) | Osingleoflong, v1::nil => Some (Val.maketotal (Val.singleoflong v1)) | Osingleoflongu, v1::nil => Some (Val.maketotal (Val.singleoflongu v1)) + | Obits_of_single, v1::nil => Some (ExtValues.bits_of_single v1) + | Obits_of_float, v1::nil => Some (ExtValues.bits_of_float v1) + | 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)) (* Expansed conditions *) | OEseqw optR0, v1::v2::nil => Some (apply_bin_r0 optR0 (Val.cmp Ceq) v1 v2 zero32) @@ -442,6 +453,7 @@ Definition eval_operation | OEfeqs, v1::v2::nil => Some (Val.cmpfs Ceq v1 v2) | OEflts, v1::v2::nil => Some (Val.cmpfs Clt v1 v2) | OEfles, v1::v2::nil => Some (Val.cmpfs Cle v1 v2) + | Oselectl, vb::vt::vf::nil => Some (Val.normalize (ExtValues.select01_long vb vt vf) Tlong) | _, _ => None end. @@ -472,9 +484,9 @@ Qed. Ltac FuncInv := match goal with | H: (match ?x with nil => _ | _ :: _ => _ end = Some _) |- _ => - destruct x; simpl in H; FuncInv + destruct x; cbn in H; FuncInv | H: (match ?v with Vundef => _ | Vint _ => _ | Vfloat _ => _ | Vptr _ _ => _ end = Some _) |- _ => - destruct v; simpl in H; FuncInv + destruct v; cbn in H; FuncInv | H: (if Archi.ptr64 then _ else _) = Some _ |- _ => destruct Archi.ptr64 eqn:?; FuncInv | H: (Some _ = Some _) |- _ => @@ -643,6 +655,11 @@ Definition type_of_operation (op: operation) : list typ * typ := | OEfeqs => (Tsingle :: Tsingle :: nil, Tint) | OEflts => (Tsingle :: Tsingle :: nil, Tint) | OEfles => (Tsingle :: Tsingle :: nil, Tint) + | Obits_of_single => (Tsingle :: nil, Tint) + | 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 := @@ -929,6 +946,18 @@ Proof with (try exact I; try reflexivity; auto using Val.Vptr_has_type). (* OEfles *) - destruct v0; destruct v1; cbn; auto. destruct Float32.cmp; cbn; auto. + (* Bits_of_single, float *) + - destruct v0; cbn; trivial. + - destruct v0; cbn; trivial. + (* 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. *) @@ -1767,6 +1796,17 @@ Proof. (* OEfles *) - inv H4; inv H2; cbn; simpl; auto. destruct Float32.cmp; unfold Vtrue, Vfalse; cbn; auto. + (* Bits_of_single, double *) + - inv H4; simpl; auto. + - inv H4; simpl; auto. + (* 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/PrintOp.ml b/riscV/PrintOp.ml index e11dd530..84380251 100644 --- a/riscV/PrintOp.ml +++ b/riscV/PrintOp.ml @@ -222,6 +222,11 @@ let print_operation reg pp = function | OEfeqs, [r1;r2] -> fprintf pp "OEfeqs(%a,%s,%a)" reg r1 (comparison_name Ceq) reg r2 | OEflts, [r1;r2] -> fprintf pp "OEflts(%a,%s,%a)" reg r1 (comparison_name Clt) reg r2 | OEfles, [r1;r2] -> fprintf pp "OEfles(%a,%s,%a)" reg r1 (comparison_name Cle) reg r2 + | Obits_of_single, [r1] -> fprintf pp "bits_of_single(%a)" reg r1 + | Obits_of_float, [r1] -> fprintf pp "bits_of_float(%a)" reg r1 + | Osingle_of_bits, [r1] -> fprintf pp "single_of_bits(%a)" reg r1 + | Ofloat_of_bits, [r1] -> fprintf pp "float_of_bits(%a)" reg r1 + | Oselectl, [rb;rt;rf] -> fprintf pp "selectl(b:%a, t:%a, f:%a)" reg rb reg rt reg rf | _ -> fprintf pp "<bad operator>" let print_addressing reg pp = function diff --git a/riscV/SelectOp.vp b/riscV/SelectOp.vp index e9920e46..9932aaf8 100644 --- a/riscV/SelectOp.vp +++ b/riscV/SelectOp.vp @@ -419,9 +419,39 @@ Definition floatofsingle (e: expr) := Eop Ofloatofsingle (e ::: Enil). (** ** Selection *) +Definition same_expr_pure (e1 e2: expr) := + match e1, e2 with + | Evar v1, Evar v2 => if ident_eq v1 v2 then true else false + | _, _ => false + end. + Definition select (ty: typ) (cond: condition) (args: exprlist) (e1 e2: expr) - : option expr - := None. + : option expr := + if same_expr_pure e1 e2 + then Some e1 + else + if Archi.ptr64 then + match ty with + | Tlong => Some (Eop Oselectl + ((Eop (Ocmp cond) args) ::: e1 ::: e2 ::: Enil)) + | Tint => Some (Eop Olowlong ((Eop Oselectl + ((Eop (Ocmp cond) args) ::: + (Eop Ocast32signed (e1 ::: Enil)) ::: + (Eop Ocast32signed (e2 ::: Enil)) ::: Enil)) ::: Enil)) + | Tfloat => Some (Eop Ofloat_of_bits ((Eop Oselectl + ((Eop (Ocmp cond) args) ::: + (Eop Obits_of_float (e1 ::: Enil)) ::: + (Eop Obits_of_float (e2 ::: Enil)) ::: Enil)) ::: Enil)) + | Tsingle => Some + (Eop Osingle_of_bits + ((Eop Olowlong ((Eop Oselectl + ((Eop (Ocmp cond) args) ::: + (Eop Ocast32signed ((Eop Obits_of_single (e1 ::: Enil)) ::: Enil)) ::: + (Eop Ocast32signed ((Eop Obits_of_single (e2 ::: Enil)) ::: Enil)) + ::: Enil)) ::: Enil)) ::: Enil)) + | _ => None + end + else None. (** ** Recognition of addressing modes for load and store operations *) @@ -462,4 +492,9 @@ Definition divfs_base (e1: expr) (e2: expr) := (** Platform-specific known builtins *) Definition platform_builtin (b: platform_builtin) (args: exprlist) : option expr := - None. + match b with + | BI_bits_of_float => Some (Eop Obits_of_single args) + | BI_bits_of_double => Some (Eop Obits_of_float args) + | BI_float_of_bits => Some (Eop Osingle_of_bits args) + | BI_double_of_bits => Some (Eop Ofloat_of_bits args) + end. diff --git a/riscV/SelectOpproof.v b/riscV/SelectOpproof.v index 1d13702a..ce80fc57 100644 --- a/riscV/SelectOpproof.v +++ b/riscV/SelectOpproof.v @@ -24,6 +24,7 @@ Require Import Cminor Op CminorSel. Require Import SelectOp. Require Import OpHelpers. Require Import OpHelpersproof. +Require Import Lia. Local Open Scope cminorsel_scope. @@ -875,6 +876,71 @@ Proof. red; intros. unfold floatofsingle. TrivialExists. Qed. +Lemma mod_small_negative: + forall a modulus, + modulus > 0 -> -modulus < a < 0 -> a mod modulus = a + modulus. +Proof. + intros. + replace (a mod modulus) with ((a + modulus) mod modulus). + apply Z.mod_small. + lia. + rewrite <- Zplus_mod_idemp_r. + rewrite Z.mod_same by lia. + rewrite Z.add_0_r. + reflexivity. +Qed. + +Remark normalize_low_long: forall + (PTR64 : Archi.ptr64 = true) v1, + Val.loword (Val.normalize (Val.longofint v1) Tlong) = Val.normalize v1 Tint. +Proof. + intros. + destruct v1; cbn; try rewrite PTR64; trivial. + f_equal. + unfold Int64.loword. + unfold Int.signed. + destruct zlt. + { rewrite Int64.int_unsigned_repr. + apply Int.repr_unsigned. + } + pose proof (Int.unsigned_range i). + rewrite Int64.unsigned_repr_eq. + replace ((Int.unsigned i - Int.modulus) mod Int64.modulus) + with (Int64.modulus + Int.unsigned i - Int.modulus). + { + rewrite <- (Int.repr_unsigned i) at 2. + apply Int.eqm_samerepr. + unfold Int.eqm, eqmod. + change Int.modulus with 4294967296 in *. + change Int64.modulus with 18446744073709551616 in *. + exists 4294967295. + lia. + } + { rewrite mod_small_negative. + lia. + constructor. + constructor. + change Int.modulus with 4294967296 in *. + change Int.half_modulus with 2147483648 in *. + change Int64.modulus with 18446744073709551616 in *. + lia. + lia. + } +Qed. + +Lemma same_expr_pure_correct: + forall le a1 a2 v1 v2 + (PURE : same_expr_pure a1 a2 = true) + (EVAL1 : eval_expr ge sp e m le a1 v1) + (EVAL2 : eval_expr ge sp e m le a2 v2), + v1 = v2. +Proof. + intros. + destruct a1; destruct a2; cbn in *; try discriminate. + inv EVAL1. inv EVAL2. + destruct (ident_eq i i0); congruence. +Qed. + Theorem eval_select: forall le ty cond al vl a1 v1 a2 v2 a b, select ty cond al a1 a2 = Some a -> @@ -886,7 +952,56 @@ Theorem eval_select: eval_expr ge sp e m le a v /\ Val.lessdef (Val.select (Some b) v1 v2 ty) v. Proof. - unfold select; intros; discriminate. + unfold select; intros. + pose proof (same_expr_pure_correct le a1 a2 v1 v2) as PURE. + destruct (same_expr_pure a1 a2). + { rewrite <- PURE by auto. + inv H. + exists v1. split. assumption. + unfold Val.select. + destruct b; apply Val.lessdef_normalize. + } + clear PURE. + destruct Archi.ptr64 eqn:PTR64. + 2: discriminate. + destruct ty; cbn in *; try discriminate. + - (* Tint *) + inv H. TrivialExists. + + cbn. repeat econstructor; eassumption. + + cbn. f_equal. rewrite ExtValues.normalize_select01. + rewrite H3. destruct b. + * rewrite ExtValues.select01_long_true. apply normalize_low_long; assumption. + * rewrite ExtValues.select01_long_false. apply normalize_low_long; assumption. + + - (* Tfloat *) + inv H. TrivialExists. + + cbn. repeat econstructor; eassumption. + + cbn. f_equal. rewrite ExtValues.normalize_select01. + rewrite H3. destruct b. + * rewrite ExtValues.select01_long_true. + apply ExtValues.float_bits_normalize. + * rewrite ExtValues.select01_long_false. + apply ExtValues.float_bits_normalize. + + - (* Tlong *) + inv H. TrivialExists. + + cbn. repeat econstructor; eassumption. + + cbn. f_equal. rewrite ExtValues.normalize_select01. + rewrite H3. destruct b. + * rewrite ExtValues.select01_long_true. reflexivity. + * rewrite ExtValues.select01_long_false. reflexivity. + + - (* Tsingle *) + inv H. TrivialExists. + + cbn. repeat econstructor; eassumption. + + cbn. f_equal. rewrite ExtValues.normalize_select01. + rewrite H3. destruct b. + * rewrite ExtValues.select01_long_true. + rewrite normalize_low_long by assumption. + apply ExtValues.single_bits_normalize. + * rewrite ExtValues.select01_long_false. + rewrite normalize_low_long by assumption. + apply ExtValues.single_bits_normalize. Qed. Theorem eval_addressing: @@ -969,7 +1084,10 @@ Theorem eval_platform_builtin: platform_builtin_sem bf vl = Some v -> exists v', eval_expr ge sp e m le a v' /\ Val.lessdef v v'. Proof. - intros. discriminate. + destruct bf; intros until le; intro Heval. + all: try (inversion Heval; subst a; clear Heval; + exists v; split; trivial; + repeat (try econstructor; try eassumption)). Qed. End CMCONSTR. diff --git a/riscV/TargetPrinter.ml b/riscV/TargetPrinter.ml index 1f02ca71..1f00c440 100644 --- a/riscV/TargetPrinter.ml +++ b/riscV/TargetPrinter.ml @@ -396,6 +396,10 @@ module Target : TARGET = fprintf oc " fmv.x.s %a, %a\n" ireg rd freg fs | Pfmvxd (rd,fs) -> fprintf oc " fmv.x.d %a, %a\n" ireg rd freg fs + | Pfmvsx (fd,rs) -> + fprintf oc " fmv.s.x %a, %a\n" freg fd ireg rs + | Pfmvdx (fd,rs) -> + fprintf oc " fmv.d.x %a, %a\n" freg fd ireg rs (* 32-bit (single-precision) floating point *) | Pfls (fd, ra, ofs) -> @@ -525,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 00b49bc1..97f3ff61 100644 --- a/riscV/ValueAOp.v +++ b/riscV/ValueAOp.v @@ -86,6 +86,39 @@ Definition eval_static_addressing (addr: addressing) (vl: list aval): aval := | _, _ => Vbot end. +Definition bits_of_single (v : aval) : aval := + match v with + | FS f => I (Float32.to_bits f) + | _ => ntop1 v + end. + +Definition bits_of_float (v : aval) : aval := + match v with + | F f => L (Float.to_bits f) + | _ => ntop1 v + end. + +Definition single_of_bits (v : aval) : aval := + match v with + | I f => FS (Float32.of_bits f) + | _ => ntop1 v + end. + +Definition float_of_bits (v : aval) : aval := + match v with + | L f => F (Float.of_bits f) + | _ => 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 @@ -210,6 +243,11 @@ Definition eval_static_operation (op: operation) (vl: list aval): aval := | OEfeqs, v1::v2::nil => of_optbool (cmpfs_bool Ceq v1 v2) | OEflts, v1::v2::nil => of_optbool (cmpfs_bool Clt v1 v2) | OEfles, v1::v2::nil => of_optbool (cmpfs_bool Cle v1 v2) + | Obits_of_single, v1::nil => bits_of_single v1 + | 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. @@ -221,6 +259,75 @@ Hypothesis GENV: genv_match bc ge. Variable sp: block. Hypothesis STACK: bc sp = BCstack. +Lemma bits_of_single_sound: + forall v x, vmatch bc v x -> vmatch bc (ExtValues.bits_of_single v) (bits_of_single x). +Proof. + unfold ExtValues.bits_of_single; intros. inv H; cbn; constructor. +Qed. + +Lemma bits_of_float_sound: + forall v x, vmatch bc v x -> vmatch bc (ExtValues.bits_of_float v) (bits_of_float x). +Proof. + unfold ExtValues.bits_of_float; intros. inv H; cbn; constructor. +Qed. + +Lemma single_of_bits_sound: + forall v x, vmatch bc v x -> vmatch bc (ExtValues.single_of_bits v) (single_of_bits x). +Proof. + unfold ExtValues.bits_of_single; intros. inv H; cbn; constructor. +Qed. + +Lemma float_of_bits_sound: + forall v x, vmatch bc v x -> vmatch bc (ExtValues.float_of_bits v) (float_of_bits x). +Proof. + unfold ExtValues.bits_of_float; intros. inv H; cbn; constructor. +Qed. + + +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, list_forall2 (vmatch bc) vargs aargs -> diff --git a/test/monniaux/cmov/cmov.c b/test/monniaux/cmov/cmov.c new file mode 100644 index 00000000..2e388834 --- /dev/null +++ b/test/monniaux/cmov/cmov.c @@ -0,0 +1,22 @@ +#include <stdio.h> + +long cmovl(int x, long y, long z) { + return __builtin_sel(x, y, z); +} + +int cmovi(int x, int y, int z) { + return __builtin_sel(x, y, z); +} + +double cmovd(int x, double y, double z) { + return __builtin_sel(x, y, z); +} + +int main() { + printf("%ld\n", cmovl(1, 42, 65)); + printf("%ld\n", cmovl(0, 42, 65)); + printf("%d\n", cmovi(1, 42, 65)); + printf("%d\n", cmovi(0, 42, 65)); + printf("%f\n", cmovd(1, 42., 65.)); + printf("%f\n", cmovd(0, 42., 65.)); +} diff --git a/test/monniaux/cmov/cmov2.c b/test/monniaux/cmov/cmov2.c new file mode 100644 index 00000000..6ecab61b --- /dev/null +++ b/test/monniaux/cmov/cmov2.c @@ -0,0 +1,28 @@ +#include <stdio.h> + +long cmovl(int x, long y, long z) { + return x ? y : z; +} + +int cmovi(int x, int y, int z) { + return x ? y : z; +} + +double cmovd(int x, double y, double z) { + return x ? y : z; +} + +float cmovf(int x, float y, float z) { + return x ? y : z; +} + +int main() { + printf("%ld\n", cmovl(1, 42, 65)); + printf("%ld\n", cmovl(0, 42, 65)); + printf("%d\n", cmovi(1, 42, 65)); + printf("%d\n", cmovi(0, 42, 65)); + printf("%f\n", cmovd(1, 42., 65.)); + printf("%f\n", cmovd(0, 42., 65.)); + printf("%f\n", cmovf(1, 42.f, 65.f)); + printf("%f\n", cmovf(0, 42.f, 65.f)); +} |