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/ValueAOp.v | 28 +++++++++++++++++++++++++++- 1 file changed, 27 insertions(+), 1 deletion(-) (limited to 'riscV/ValueAOp.v') 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