diff options
| author | David Monniaux <david.monniaux@univ-grenoble-alpes.fr> | 2019-03-26 20:51:34 +0100 |
|---|---|---|
| committer | David Monniaux <david.monniaux@univ-grenoble-alpes.fr> | 2019-03-26 20:51:34 +0100 |
| commit | d52a401b30a7618c1b36cc1e6bd514c843136690 (patch) | |
| tree | 590016047b6d287b32d8a7fe63144d90ee9c708b /mppa_k1c/SelectOp.vp | |
| parent | 45cab18f8f9fc1db4f9877333c09d5a5cb2dc64d (diff) | |
| download | compcert-kvx-d52a401b30a7618c1b36cc1e6bd514c843136690.tar.gz compcert-kvx-d52a401b30a7618c1b36cc1e6bd514c843136690.zip | |
ternary unsigned
Diffstat (limited to 'mppa_k1c/SelectOp.vp')
| -rw-r--r-- | mppa_k1c/SelectOp.vp | 9 |
1 files changed, 9 insertions, 0 deletions
diff --git a/mppa_k1c/SelectOp.vp b/mppa_k1c/SelectOp.vp index d01b7616..13650a2c 100644 --- a/mppa_k1c/SelectOp.vp +++ b/mppa_k1c/SelectOp.vp @@ -285,6 +285,15 @@ Nondetfunction or (e1: expr) (e2: expr) := && Int.eq zero1 Int.zero then Eop Oselect (v0:::v1:::y0:::Enil) else Eop Oor (e1:::e2:::Enil) + | (Eop Oand ((Eop Oneg ((Eop (Ocmp (Ccompuimm Ceq zero0)) + (y0:::Enil)):::Enil)):::v0:::Enil)), + (Eop Oand ((Eop Oneg ((Eop (Ocmp (Ccompuimm Cne zero1)) + (y1:::Enil)):::Enil)):::v1:::Enil)) => + if same_expr_pure y0 y1 + && Int.eq zero0 Int.zero + && Int.eq zero1 Int.zero + then Eop Oselect (v0:::v1:::y0:::Enil) + else Eop Oor (e1:::e2:::Enil) | _, _ => Eop Oor (e1:::e2:::Enil) end. |