diff options
| author | David Monniaux <david.monniaux@univ-grenoble-alpes.fr> | 2019-04-05 15:04:46 +0200 |
|---|---|---|
| committer | David Monniaux <david.monniaux@univ-grenoble-alpes.fr> | 2019-04-05 15:04:46 +0200 |
| commit | 27d1525b819cf4f82e4a2f2943596001b50c44b7 (patch) | |
| tree | c9341fdeeab54a1ead28604e51c9918e2e26b815 /mppa_k1c/SelectLong.vp | |
| parent | 5ff1a009561973e65437edadd752f627c12c1a29 (diff) | |
| download | compcert-kvx-27d1525b819cf4f82e4a2f2943596001b50c44b7.tar.gz compcert-kvx-27d1525b819cf4f82e4a2f2943596001b50c44b7.zip | |
reinstated the orl selectl construct
Diffstat (limited to 'mppa_k1c/SelectLong.vp')
| -rw-r--r-- | mppa_k1c/SelectLong.vp | 9 |
1 files changed, 3 insertions, 6 deletions
diff --git a/mppa_k1c/SelectLong.vp b/mppa_k1c/SelectLong.vp index f8f5bf3b..f7cb3c82 100644 --- a/mppa_k1c/SelectLong.vp +++ b/mppa_k1c/SelectLong.vp @@ -286,10 +286,6 @@ Nondetfunction orl (e1: expr) (e2: expr) := | t1, Eop (Olongconst n2) Enil => orlimm n2 t1 | (Eop Onotl (t1:::Enil)), t2 => Eop Oornl (t1:::t2:::Enil) | t1, (Eop Onotl (t2:::Enil)) => Eop Oornl (t2:::t1:::Enil) - | _, _ => Eop Oorl (e1:::e2:::Enil) - end. - - (* | (Eop Oandl ((Eop Ocast32signed ((Eop Oneg ((Eop (Ocmp (Ccomplimm Ceq zero0)) (y0:::Enil)):::Enil)):::Enil)):::v0:::Enil)), @@ -299,9 +295,10 @@ Nondetfunction orl (e1: expr) (e2: expr) := if same_expr_pure y0 y1 && Int64.eq zero0 Int64.zero && Int64.eq zero1 Int64.zero - then Eop Oselectl (v0:::v1:::y0:::Enil) + then Eop (Oselectl (Ccompl0 Cne)) (v0:::v1:::y0:::Enil) else Eop Oorl (e1:::e2:::Enil) - *) + | _, _ => Eop Oorl (e1:::e2:::Enil) + end. Nondetfunction xorlimm (n1: int64) (e2: expr) := if Int64.eq n1 Int64.zero then e2 else |