From 57925286e8ba6055534cd0acbcf2b411366d3e0b Mon Sep 17 00:00:00 2001 From: David Monniaux Date: Fri, 5 Apr 2019 09:40:45 +0200 Subject: selectl with condition --- mppa_k1c/SelectOp.vp | 16 +++++++++++++--- 1 file changed, 13 insertions(+), 3 deletions(-) (limited to 'mppa_k1c/SelectOp.vp') 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. -- cgit