From d2dc422b91ed628f0f8d6286a23f6f4fb9869248 Mon Sep 17 00:00:00 2001 From: David Monniaux Date: Mon, 1 Feb 2021 15:07:46 +0100 Subject: Obits_of_single etc --- riscV/ValueAOp.v | 28 ++++++++++++++++++++++++++++ 1 file changed, 28 insertions(+) (limited to 'riscV/ValueAOp.v') diff --git a/riscV/ValueAOp.v b/riscV/ValueAOp.v index f4b7b4d6..e1ba878e 100644 --- a/riscV/ValueAOp.v +++ b/riscV/ValueAOp.v @@ -42,6 +42,18 @@ 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 eval_static_operation (op: operation) (vl: list aval): aval := match op, vl with | Omove, v1::nil => v1 @@ -137,6 +149,8 @@ Definition eval_static_operation (op: operation) (vl: list aval): aval := | Osingleoflong, v1::nil => singleoflong v1 | Osingleoflongu, v1::nil => singleoflongu v1 | 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 | _, _ => Vbot end. @@ -148,6 +162,20 @@ 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. + +Hint Resolve bits_of_single_sound bits_of_float_sound : va. + Theorem eval_static_condition_sound: forall cond vargs m aargs, list_forall2 (vmatch bc) vargs aargs -> -- cgit 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 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/ValueAOp.v | 57 ++++++++++++++++++++++++++++++++++++++++++++++++++++++-- 1 file changed, 55 insertions(+), 2 deletions(-) (limited to 'riscV/ValueAOp.v') 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