From 581d576e96463da6be672db1a85678a2a15f93a6 Mon Sep 17 00:00:00 2001 From: David Monniaux Date: Thu, 25 Apr 2019 07:17:06 +0200 Subject: some progress on bitfields --- mppa_k1c/SelectOp.vp | 8 ++++++++ 1 file changed, 8 insertions(+) (limited to 'mppa_k1c/SelectOp.vp') diff --git a/mppa_k1c/SelectOp.vp b/mppa_k1c/SelectOp.vp index d5e3ee4a..8f953425 100644 --- a/mppa_k1c/SelectOp.vp +++ b/mppa_k1c/SelectOp.vp @@ -202,6 +202,14 @@ Nondetfunction shrimm (e1: expr) (n: int) := if Int.ltu (Int.add n n1) Int.iwordsize then Eop (Oshrimm (Int.add n n1)) (t1:::Enil) else Eop (Oshrimm n) (e1:::Enil) + | Eop (Oshlimm n1) (t1:::Enil) => + let stop := Int.sub Int.iwordsize (Int.add n1 Int.one) in + let start := Int.sub (Int.add (Int.add n stop) Int.one) Int.iwordsize in + if (Int.cmp Cle start stop) + && (Int.cmp Cge start Int.zero) + && (Int.cmp Clt stop Int.iwordsize) + then Eop (Oextfz stop start) (t1:::Enil) + else Eop (Oshrimm n) (e1:::Enil) | _ => Eop (Oshrimm n) (e1:::Enil) end. -- cgit