diff options
author | David Monniaux <david.monniaux@univ-grenoble-alpes.fr> | 2019-04-27 19:51:59 +0200 |
---|---|---|
committer | David Monniaux <david.monniaux@univ-grenoble-alpes.fr> | 2019-04-27 19:51:59 +0200 |
commit | 6fed24f41ddc252ec1dc4d8a9a5595028bda1936 (patch) | |
tree | 3b04ada713b5f22a293ebee13bf1c6b6b94b41ef | |
parent | 146bf43966f0d0c7a1587fc4d8dab58958d621fa (diff) | |
download | compcert-kvx-6fed24f41ddc252ec1dc4d8a9a5595028bda1936.tar.gz compcert-kvx-6fed24f41ddc252ec1dc4d8a9a5595028bda1936.zip |
more base operators on bitfield
-rw-r--r-- | mppa_k1c/ExtValues.v | 19 |
1 files changed, 19 insertions, 0 deletions
diff --git a/mppa_k1c/ExtValues.v b/mppa_k1c/ExtValues.v index 97e48eb7..1348c0e8 100644 --- a/mppa_k1c/ExtValues.v +++ b/mppa_k1c/ExtValues.v @@ -30,6 +30,20 @@ Definition extfs stop start v := end else Vundef. +Definition zbitfield_mask stop start := + (Z.shiftl 1 (Z.succ stop)) - (Z.shiftl 1 start). + +Definition bitfield_mask stop start := + Vint(Int.repr (zbitfield_mask stop start)). + +Definition bitfield_maskl stop start := + Vlong(Int64.repr (zbitfield_mask stop start)). + +Definition insf stop start prev fld := + let mask := bitfield_mask stop start in + Val.or (Val.and prev (Val.notint mask)) + (Val.and (Val.shl fld (Vint (Int.repr start))) mask). + Definition is_bitfieldl stop start := (Z.leb start stop) && (Z.geb start Z.zero) @@ -57,3 +71,8 @@ Definition extfsl stop start v := | _ => Vundef end else Vundef. + +Definition insfl stop start prev fld := + let mask := bitfield_maskl stop start in + Val.orl (Val.andl prev (Val.notl mask)) + (Val.andl (Val.shll fld (Vint (Int.repr start))) mask). |