diff options
author | Sylvain Boulmé <sylvain.boulme@univ-grenoble-alpes.fr> | 2020-07-06 19:12:36 +0200 |
---|---|---|
committer | Sylvain Boulmé <sylvain.boulme@univ-grenoble-alpes.fr> | 2020-07-06 19:13:54 +0200 |
commit | b411a789feb2c600b0c978b7a6314d6f17959dff (patch) | |
tree | 90dbfa641d1d28615a7c1d315c74dfbe79e7c905 | |
parent | 3234aa0bad93a2ec12f30142e271452cf4ebc402 (diff) | |
download | compcert-kvx-b411a789feb2c600b0c978b7a6314d6f17959dff.tar.gz compcert-kvx-b411a789feb2c600b0c978b7a6314d6f17959dff.zip |
introduce if_opt_bool_val.
-rw-r--r-- | aarch64/Asmblock.v | 19 |
1 files changed, 12 insertions, 7 deletions
diff --git a/aarch64/Asmblock.v b/aarch64/Asmblock.v index 193941aa..2d0eeb11 100644 --- a/aarch64/Asmblock.v +++ b/aarch64/Asmblock.v @@ -1229,14 +1229,16 @@ Definition arith_eval_p (i : arith_p) : val := | Pfmovimmd f => Vfloat f end. +Definition if_opt_bool_val (c: option bool) v1 v2: val := + match c with + | Some true => v1 + | Some false => v2 + | None => Vundef + end. + Definition arith_eval_c_p (i : arith_c_p) (c : option bool) : val := match i with - | Pcset => - (match c with - | Some true => Vint Int.one - | Some false => Vint Int.zero - | None => Vundef - end) + | Pcset => if_opt_bool_val c (Vint Int.one) (Vint Int.zero) end. Definition arith_eval_pp i v := @@ -1311,8 +1313,10 @@ Definition arith_eval_ppp i v1 v2 := end. Definition arith_eval_c_ppp (i : arith_c_ppp) (v1 v2 : val) (c : option bool) := + if_opt_bool_val c v1 v2. + (* match i with - | Pcsel => + | Pcsel => (match c with | Some true => v1 | Some false => v2 @@ -1325,6 +1329,7 @@ Definition arith_eval_c_ppp (i : arith_c_ppp) (v1 v2 : val) (c : option bool) := | None => Vundef end) end. + *) Definition arith_rr0r_isize (i: arith_rr0r) := match i with |