From 21aaf9c53b2bb0c6d376c2ce436d6dd7f5442a47 Mon Sep 17 00:00:00 2001 From: David Monniaux Date: Mon, 1 Feb 2021 18:53:04 +0100 Subject: bits to float --- riscV/Asm.v | 11 +++++++++-- riscV/Builtins1.v | 10 +++++++++- riscV/CBuiltins.ml | 4 ++++ riscV/ExtValues.v | 12 ++++++++++++ riscV/NeedOp.v | 2 ++ riscV/Op.v | 14 +++++++++++++- riscV/SelectOp.vp | 2 ++ riscV/TargetPrinter.ml | 4 ++++ riscV/ValueAOp.v | 28 +++++++++++++++++++++++++++- 9 files changed, 82 insertions(+), 5 deletions(-) (limited to 'riscV') diff --git a/riscV/Asm.v b/riscV/Asm.v index 599002e7..d1946a06 100644 --- a/riscV/Asm.v +++ b/riscV/Asm.v @@ -256,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 *) @@ -924,6 +926,11 @@ Definition exec_instr (f: function) (i: instruction) (rs: regset) (m: mem) : out 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 *) diff --git a/riscV/Builtins1.v b/riscV/Builtins1.v index 86bcb2ac..47bacffa 100644 --- a/riscV/Builtins1.v +++ b/riscV/Builtins1.v @@ -22,23 +22,31 @@ Require ExtValues. Inductive platform_builtin : Type := | BI_bits_of_float -| BI_bits_of_double. +| 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) := ("__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 | 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 | 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 55b6bbd5..00b44fd5 100644 --- a/riscV/CBuiltins.ml +++ b/riscV/CBuiltins.ml @@ -50,6 +50,10 @@ let builtins = { (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 index 4edd2e3d..39070e7b 100644 --- a/riscV/ExtValues.v +++ b/riscV/ExtValues.v @@ -15,6 +15,18 @@ Definition bits_of_single x := | _ => 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_int b vtrue vfalse := Val.or (Val.and (Val.neg b) vtrue) (Val.and (Val.sub b Vone) vfalse). diff --git a/riscV/NeedOp.v b/riscV/NeedOp.v index 9a406b6f..136c157f 100644 --- a/riscV/NeedOp.v +++ b/riscV/NeedOp.v @@ -89,6 +89,8 @@ Definition needs_of_operation (op: operation) (nv: nval): list nval := | Ocmp c => needs_of_condition c | Obits_of_single => op1 (default nv) | Obits_of_float => op1 (default nv) + | Osingle_of_bits => op1 (default nv) + | Ofloat_of_bits => op1 (default nv) end. Definition operation_is_redundant (op: operation) (nv: nval): bool := diff --git a/riscV/Op.v b/riscV/Op.v index 160e4412..21de7787 100644 --- a/riscV/Op.v +++ b/riscV/Op.v @@ -155,7 +155,9 @@ Inductive operation : Type := (*c Boolean tests: *) | Ocmp (cond: condition) (**r [rd = 1] if condition holds, [rd = 0] otherwise. *) | Obits_of_single - | Obits_of_float. + | Obits_of_float + | Osingle_of_bits + | Ofloat_of_bits. (** Addressing modes. [r1], [r2], etc, are the arguments to the addressing. *) @@ -322,6 +324,8 @@ Definition eval_operation | 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)) | _, _ => None end. @@ -481,6 +485,8 @@ Definition type_of_operation (op: operation) : list typ * typ := | Ocmp c => (type_of_condition c, 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) end. Definition type_of_addressing (addr: addressing) : list typ := @@ -690,6 +696,9 @@ Proof with (try exact I; try reflexivity; auto using Val.Vptr_has_type). (* Bits_of_single, float *) - destruct v0; cbn; trivial. - destruct v0; cbn; trivial. + (* single, float of bits *) + - destruct v0; cbn; trivial. + - destruct v0; cbn; trivial. Qed. (* This should not be simplified to "false" because it breaks proofs elsewhere. *) @@ -1259,6 +1268,9 @@ Proof. (* Bits_of_single, double *) - inv H4; simpl; auto. - inv H4; simpl; auto. + (* single, double of bits *) + - inv H4; simpl; auto. + - inv H4; simpl; auto. Qed. Lemma eval_addressing_inj: diff --git a/riscV/SelectOp.vp b/riscV/SelectOp.vp index 87e3af05..7714f12d 100644 --- a/riscV/SelectOp.vp +++ b/riscV/SelectOp.vp @@ -465,4 +465,6 @@ Definition platform_builtin (b: platform_builtin) (args: exprlist) : option expr 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. \ No newline at end of file diff --git a/riscV/TargetPrinter.ml b/riscV/TargetPrinter.ml index 1f02ca71..4bcfa6af 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) -> diff --git a/riscV/ValueAOp.v b/riscV/ValueAOp.v index e1ba878e..f94669a2 100644 --- a/riscV/ValueAOp.v +++ b/riscV/ValueAOp.v @@ -54,6 +54,18 @@ Definition bits_of_float (v : aval) : aval := | _ => 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 eval_static_operation (op: operation) (vl: list aval): aval := match op, vl with | Omove, v1::nil => v1 @@ -151,6 +163,8 @@ Definition eval_static_operation (op: operation) (vl: list aval): aval := | Ocmp c, _ => of_optbool (eval_static_condition c vl) | 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 | _, _ => Vbot end. @@ -174,7 +188,19 @@ Proof. unfold ExtValues.bits_of_float; intros. inv H; cbn; constructor. Qed. -Hint Resolve bits_of_single_sound bits_of_float_sound : va. +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. + +Hint Resolve bits_of_single_sound bits_of_float_sound single_of_bits_sound float_of_bits_sound : va. Theorem eval_static_condition_sound: forall cond vargs m aargs, -- cgit