diff options
Diffstat (limited to 'riscV/ExtValues.v')
-rw-r--r-- | riscV/ExtValues.v | 29 |
1 files changed, 15 insertions, 14 deletions
diff --git a/riscV/ExtValues.v b/riscV/ExtValues.v index d79604f7..f9996a97 100644 --- a/riscV/ExtValues.v +++ b/riscV/ExtValues.v @@ -104,6 +104,7 @@ Definition single_of_bits x := | _ => Vundef end. +(* Definition bitwise_select_int b vtrue vfalse := Val.or (Val.and (Val.neg b) vtrue) (Val.and (Val.sub b Vone) vfalse). @@ -139,18 +140,18 @@ Proof. rewrite Int.or_commut. apply Int.or_zero. Qed. + *) Definition bitwise_select_long b vtrue vfalse := - let b' := Val.longofint b in - Val.orl (Val.andl (Val.negl b') vtrue) - (Val.andl (Val.subl b' (Vlong Int64.one)) vfalse). + let b' := Int64.repr (Int64.unsigned b) in + Int64.or (Int64.and (Int64.neg b') vtrue) + (Int64.and (Int64.sub b' Int64.one) vfalse). Lemma bitwise_select_long_true : forall vtrue vfalse, - bitwise_select_long (Val.of_optbool (Some true)) (Vlong vtrue) (Vlong vfalse) - = Vlong vtrue. + bitwise_select_long Int64.one vtrue vfalse = vtrue. Proof. - intros. cbn. f_equal. + intros. unfold bitwise_select_long. cbn. change (Int64.neg Int64.one) with Int64.mone. rewrite Int64.and_commut. rewrite Int64.and_mone. @@ -162,11 +163,10 @@ Qed. Lemma bitwise_select_long_false : forall vtrue vfalse, - bitwise_select_long (Val.of_optbool (Some false)) (Vlong vtrue) (Vlong vfalse) - = Vlong vfalse. + bitwise_select_long Int64.zero vtrue vfalse = vfalse. Proof. - intros. cbn. f_equal. - change (Int64.repr (Int.signed Int.zero)) with Int64.zero. + intros. unfold bitwise_select_long. cbn. + change (Int64.repr (Int64.unsigned Int64.zero)) with Int64.zero. rewrite Int64.neg_zero. rewrite Int64.and_commut. rewrite Int64.and_zero. @@ -178,7 +178,8 @@ Proof. apply Int64.or_zero. Qed. -(* -Compute (Int.unsigned (Float32.to_bits (Float32.of_int (Int.repr 4200)))). -Compute (Int64.unsigned (Float.to_bits (Float.of_int (Int.repr 4233)))). -*) +Definition bitwise_select_value vt m b vtrue vfalse := + value_of_int64 vt m (bitwise_select_long b + (int64_of_value m vtrue) + (int64_of_value m vfalse)). + |