diff options
| author | David Monniaux <david.monniaux@univ-grenoble-alpes.fr> | 2021-02-01 20:53:06 +0100 |
|---|---|---|
| committer | David Monniaux <david.monniaux@univ-grenoble-alpes.fr> | 2021-02-01 20:53:06 +0100 |
| commit | 485952d5513a9de25f7e3ee3ca7a35442f154d04 (patch) | |
| tree | cbf3589aa9068d9c45c64ea7273d28ccfae3fd45 /riscV | |
| parent | 9c03320dd809295239a9cdf71cd8726f02df0d33 (diff) | |
| download | compcert-kvx-485952d5513a9de25f7e3ee3ca7a35442f154d04.tar.gz compcert-kvx-485952d5513a9de25f7e3ee3ca7a35442f154d04.zip | |
int64_of_value some more
Diffstat (limited to 'riscV')
| -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)). + |