diff options
| author | David Monniaux <david.monniaux@univ-grenoble-alpes.fr> | 2019-04-05 09:40:45 +0200 |
|---|---|---|
| committer | David Monniaux <david.monniaux@univ-grenoble-alpes.fr> | 2019-04-05 09:40:45 +0200 |
| commit | 57925286e8ba6055534cd0acbcf2b411366d3e0b (patch) | |
| tree | c8dfba8a2a178a829e7c4dacc1782380befdd790 /mppa_k1c/SelectOp.vp | |
| parent | 483d0e37880dbe44af3dafdcac9b1110a37139c4 (diff) | |
| download | compcert-kvx-57925286e8ba6055534cd0acbcf2b411366d3e0b.tar.gz compcert-kvx-57925286e8ba6055534cd0acbcf2b411366d3e0b.zip | |
selectl with condition
Diffstat (limited to 'mppa_k1c/SelectOp.vp')
| -rw-r--r-- | mppa_k1c/SelectOp.vp | 16 |
1 files changed, 13 insertions, 3 deletions
diff --git a/mppa_k1c/SelectOp.vp b/mppa_k1c/SelectOp.vp index 906d6791..eeb3ffae 100644 --- a/mppa_k1c/SelectOp.vp +++ b/mppa_k1c/SelectOp.vp @@ -62,10 +62,20 @@ Section SELECT. Context {hf: helper_functions}. (** Ternary operator *) -Definition select o0 o1 oselect := +Definition select_base o0 o1 oselect := Eop (Oselect (Ccomp0 Cne)) (o0:::o1:::oselect:::Enil). +Definition select o0 o1 oselect := + select_base o0 o1 oselect. + +Definition selectl_base o0 o1 oselect := + Eop (Oselectl (Ccomp0 Cne)) + (o0:::o1:::oselect:::Enil). + +Definition selectl o0 o1 oselect := + selectl_base o0 o1 oselect. + (** ** Constants **) Definition addrsymbol (id: ident) (ofs: ptrofs) := @@ -288,7 +298,7 @@ Nondetfunction or (e1: expr) (e2: expr) := if same_expr_pure y0 y1 && Int.eq zero0 Int.zero && Int.eq zero1 Int.zero - then select v0 v1 y0 + then select_base v0 v1 y0 else Eop Oor (e1:::e2:::Enil) | (Eop Oand ((Eop Oneg ((Eop (Ocmp (Ccompuimm Ceq zero0)) (y0:::Enil)):::Enil)):::v0:::Enil)), @@ -297,7 +307,7 @@ Nondetfunction or (e1: expr) (e2: expr) := if same_expr_pure y0 y1 && Int.eq zero0 Int.zero && Int.eq zero1 Int.zero - then select v0 v1 y0 + then select_base v0 v1 y0 else Eop Oor (e1:::e2:::Enil) | _, _ => Eop Oor (e1:::e2:::Enil) end. |