diff options
| author | David Monniaux <david.monniaux@univ-grenoble-alpes.fr> | 2019-05-11 10:21:59 +0200 |
|---|---|---|
| committer | David Monniaux <david.monniaux@univ-grenoble-alpes.fr> | 2019-05-11 10:21:59 +0200 |
| commit | 3ef3e6c78026cc1d5793ccb4e905a0232ec7bb4e (patch) | |
| tree | 2c4e87342b978883fb471559ca0c18e5f7a3cc00 /mppa_k1c/SelectLong.vp | |
| parent | ae22df3c5ef0a60527ea85b83bb71e8c95a6ab9c (diff) | |
| download | compcert-kvx-3ef3e6c78026cc1d5793ccb4e905a0232ec7bb4e.tar.gz compcert-kvx-3ef3e6c78026cc1d5793ccb4e905a0232ec7bb4e.zip | |
generate multiply-sub long
Diffstat (limited to 'mppa_k1c/SelectLong.vp')
| -rw-r--r-- | mppa_k1c/SelectLong.vp | 6 |
1 files changed, 5 insertions, 1 deletions
diff --git a/mppa_k1c/SelectLong.vp b/mppa_k1c/SelectLong.vp index 717b0120..b29b9712 100644 --- a/mppa_k1c/SelectLong.vp +++ b/mppa_k1c/SelectLong.vp @@ -118,6 +118,10 @@ Nondetfunction subl (e1: expr) (e2: expr) := addlimm n1 (Eop Osubl (t1:::t2:::Enil)) | t1, Eop (Oaddlimm n2) (t2:::Enil) => addlimm (Int64.neg n2) (Eop Osubl (t1:::t2:::Enil)) + | t1, (Eop Omull (t2:::t3:::Enil)) => + Eop Omsubl (t1:::t2:::t3:::Enil) + | t1, (Eop (Omullimm n) (t2:::Enil)) => + Eop (Omaddlimm (Int64.neg n)) (t1:::t2:::Enil) | _, _ => Eop Osubl (e1:::e2:::Enil) end. @@ -225,7 +229,7 @@ Definition mullimm_base (n1: int64) (e2: expr) := | i :: j :: nil => Elet e2 (addl (shllimm (Eletvar 0) i) (shllimm (Eletvar 0) j)) | _ => - Eop Omull (e2 ::: longconst n1 ::: Enil) + Eop (Omullimm n1) (e2 ::: Enil) end. Nondetfunction mullimm (n1: int64) (e2: expr) := |