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/Op.v | 14 +++++++++++++- 1 file changed, 13 insertions(+), 1 deletion(-) (limited to 'riscV/Op.v') 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: -- cgit