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