diff options
| author | Xavier Leroy <xavier.leroy@college-de-france.fr> | 2019-04-14 10:45:58 +0200 |
|---|---|---|
| committer | Xavier Leroy <xavierleroy@users.noreply.github.com> | 2019-05-20 18:00:46 +0200 |
| commit | 72ab6ad1dcf13dd61d3bdb896660b0f399e9f8a5 (patch) | |
| tree | e6747bed65fb8927fa5a840e31a7bdaa2bfc67af | |
| parent | 3830a91a4711c4570394e02e93e4e08db88eac6f (diff) | |
| download | compcert-72ab6ad1dcf13dd61d3bdb896660b0f399e9f8a5.tar.gz compcert-72ab6ad1dcf13dd61d3bdb896660b0f399e9f8a5.zip | |
Give a semantics to the Pisel instruction
| -rw-r--r-- | powerpc/Asm.v | 8 |
1 files changed, 7 insertions, 1 deletions
diff --git a/powerpc/Asm.v b/powerpc/Asm.v index ad24f563..748058c4 100644 --- a/powerpc/Asm.v +++ b/powerpc/Asm.v @@ -860,6 +860,13 @@ Definition exec_instr (f: function) (i: instruction) (rs: regset) (m: mem) : out Next (nextinstr (rs#rd <- (Val.subf rs#r1 rs#r2))) m | Pfsubs rd r1 r2 => Next (nextinstr (rs#rd <- (Val.subfs rs#r1 rs#r2))) m + | Pisel rd r1 r2 bit => + let v := + match rs#(reg_of_crbit bit) with + | Vint n => if Int.eq n Int.zero then rs#r2 else rs#r1 + | _ => Vundef + end in + Next (nextinstr (rs#rd <- v)) m | Plbz rd cst r1 => load1 Mint8unsigned rd cst r1 rs m | Plbzx rd r1 r2 => @@ -1073,7 +1080,6 @@ Definition exec_instr (f: function) (i: instruction) (rs: regset) (m: mem) : out | Pfrsqrte _ _ | Pfres _ _ | Pfsel _ _ _ _ - | Pisel _ _ _ _ | Plwarx _ _ _ | Plwbrx _ _ _ | Picbi _ _ |