diff options
| author | David Monniaux <david.monniaux@univ-grenoble-alpes.fr> | 2019-04-25 07:17:06 +0200 |
|---|---|---|
| committer | David Monniaux <david.monniaux@univ-grenoble-alpes.fr> | 2019-04-25 07:17:06 +0200 |
| commit | 581d576e96463da6be672db1a85678a2a15f93a6 (patch) | |
| tree | 2e838040bab6f88cb26349aeb561b40e072ff6df /mppa_k1c/SelectOp.vp | |
| parent | 59089e5d11428dd224b3239bc7f5db602df9b177 (diff) | |
| download | compcert-kvx-581d576e96463da6be672db1a85678a2a15f93a6.tar.gz compcert-kvx-581d576e96463da6be672db1a85678a2a15f93a6.zip | |
some progress on bitfields
Diffstat (limited to 'mppa_k1c/SelectOp.vp')
| -rw-r--r-- | mppa_k1c/SelectOp.vp | 8 |
1 files changed, 8 insertions, 0 deletions
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. |