From 0d8f4f46407b1634fba4f6cd46ba4955a7859863 Mon Sep 17 00:00:00 2001 From: David Monniaux Date: Wed, 27 Mar 2019 07:53:34 +0100 Subject: match some 'and' --- mppa_k1c/SelectLong.vp | 8 +++++++- 1 file changed, 7 insertions(+), 1 deletion(-) (limited to 'mppa_k1c/SelectLong.vp') diff --git a/mppa_k1c/SelectLong.vp b/mppa_k1c/SelectLong.vp index 26ae55f6..9bf35581 100644 --- a/mppa_k1c/SelectLong.vp +++ b/mppa_k1c/SelectLong.vp @@ -258,7 +258,13 @@ Nondetfunction andl (e1: expr) (e2: expr) := | Eop (Olongconst n1) Enil, t2 => andlimm n1 t2 | t1, Eop (Olongconst n2) Enil => andlimm n2 t1 | (Eop Onotl (t1:::Enil)), t2 => Eop Oandnl (t1:::t2:::Enil) - | t1, (Eop Onotl (t2:::Enil)) => Eop Oandnl (t2:::t1:::Enil) + | t1, (Eop Onotl (t2:::Enil)) => Eop Oandnl (t2:::t1:::Enil) + | (Eop Ocast32signed + ((Eop Oneg ((Eop (Ocmp (Ccomplimm Cne zero1)) + (y1:::Enil)):::Enil)):::Enil)), v1 => + if Int64.eq zero1 Int64.zero + then Eop Oselectl ((Eop (Olongconst Int64.zero) Enil):::v1:::y1:::Enil) + else Eop Oandl (e1:::e2:::Enil) | _, _ => Eop Oandl (e1:::e2:::Enil) end. -- cgit