diff options
author | David Monniaux <david.monniaux@univ-grenoble-alpes.fr> | 2019-06-03 20:09:19 +0200 |
---|---|---|
committer | David Monniaux <david.monniaux@univ-grenoble-alpes.fr> | 2019-06-03 20:11:48 +0200 |
commit | 677771949bd62f7f5bbcf99bba6b6f816f07a6c2 (patch) | |
tree | 597b2ccc5867bc2bbb083c4e13f792671b2042c1 /x86/SelectOp.vp | |
parent | 36e64ee96ded0c94c83da6fb12202c276e66ba45 (diff) | |
parent | b7e0d70de2ace6f0a22f9f65cc244d875ee48496 (diff) | |
download | compcert-kvx-677771949bd62f7f5bbcf99bba6b6f816f07a6c2.tar.gz compcert-kvx-677771949bd62f7f5bbcf99bba6b6f816f07a6c2.zip |
Merge branch 'if-conversion' of https://github.com/AbsInt/CompCert into mppa-if-conversion
Diffstat (limited to 'x86/SelectOp.vp')
-rw-r--r-- | x86/SelectOp.vp | 30 |
1 files changed, 29 insertions, 1 deletions
diff --git a/x86/SelectOp.vp b/x86/SelectOp.vp index eadda093..c0434a67 100644 --- a/x86/SelectOp.vp +++ b/x86/SelectOp.vp @@ -457,7 +457,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). |