From 996f2e071baaf52105714283d141af2eac8ffbfb Mon Sep 17 00:00:00 2001 From: Xavier Leroy Date: Mon, 15 Apr 2019 15:21:49 +0200 Subject: Implement a `Osel` operation for x86 The operation compiles down to conditional moves. --- x86/SelectOp.vp | 30 +++++++++++++++++++++++++++++- 1 file changed, 29 insertions(+), 1 deletion(-) (limited to 'x86/SelectOp.vp') diff --git a/x86/SelectOp.vp b/x86/SelectOp.vp index a1583600..cf0f37ec 100644 --- a/x86/SelectOp.vp +++ b/x86/SelectOp.vp @@ -456,7 +456,35 @@ Nondetfunction cast16signed (e: expr) := Eop Ocast16signed (e ::: Enil) end. -(** Floating-point conversions *) +(** ** Selection *) + +Definition select_supported (ty: typ) : bool := + match ty with + | Tint => true + | Tlong => Archi.ptr64 + | _ => false + end. + +(** [Asmgen.mk_sel] cannot always handle the conditions that are + implemented as a "and" of two processor flags. However it can + handle the negation of those conditions, which are implemented + as an "or". So, for the risky conditions we just take their + negation and swap the two arguments of the [select]. *) + +Definition select_swap (cond: condition) := + match cond with + | Ccompf Cne | Ccompfs Cne | Cnotcompf Ceq | Cnotcompfs Ceq => true + | _ => false + end. + +Definition select (ty: typ) (cond: condition) (args: exprlist) (e1 e2: expr) := + if select_supported ty then + if select_swap cond + then Some (Eop (Osel (negate_condition cond) ty) (e2 ::: e1 ::: args)) + else Some (Eop (Osel cond ty) (e1 ::: e2 ::: args)) + else None. + +(** ** Floating-point conversions *) Definition singleoffloat (e: expr) := Eop Osingleoffloat (e ::: Enil). Definition floatofsingle (e: expr) := Eop Ofloatofsingle (e ::: Enil). -- cgit