From 378ac3925503e6efd24cc34796e85d95c031e72d Mon Sep 17 00:00:00 2001 From: Xavier Leroy Date: Sun, 13 Sep 2015 11:44:32 +0200 Subject: Use PowerPC 64 bits instructions (when available) for int<->FP conversions. Also: implement __builtin_isel on non-EREF platforms with a branch-free instruction sequence. Also: extend ./configure so that it recognizes "ppc64-" and "e5500-" platforms in addition to "ppc-". --- powerpc/Asmgenproof1.v | 12 ++++++++++++ 1 file changed, 12 insertions(+) (limited to 'powerpc/Asmgenproof1.v') diff --git a/powerpc/Asmgenproof1.v b/powerpc/Asmgenproof1.v index cb94c555..25e8bf07 100644 --- a/powerpc/Asmgenproof1.v +++ b/powerpc/Asmgenproof1.v @@ -941,6 +941,18 @@ Opaque Val.add. replace v with (Val.maketotal (Val.intoffloat (rs x))). TranslOpSimpl. rewrite H1; auto. + (* Ointuoffloat *) + replace v with (Val.maketotal (Val.intuoffloat (rs x))). + TranslOpSimpl. + rewrite H1; auto. + (* Ofloatofint *) + replace v with (Val.maketotal (Val.floatofint (rs x))). + TranslOpSimpl. + rewrite H1; auto. + (* Ofloatofintu *) + replace v with (Val.maketotal (Val.floatofintu (rs x))). + TranslOpSimpl. + rewrite H1; auto. (* Ocmp *) destruct (transl_cond_op_correct c0 args res k rs m c) as [rs' [A [B C]]]; auto. exists rs'; auto with asmgen. -- cgit