From 50fd8fe358b0eacb92d4cc28b6ada062e38023f5 Mon Sep 17 00:00:00 2001 From: Xavier Leroy Date: Mon, 3 Dec 2018 15:08:53 +0100 Subject: x86: wrong modeling of ZF flag for FP comparisons As written in the comment, ZF should be set if the two floats are equal or unordered. The "or unordered" case was missing in the original modeling of FP comparisons. - Set ZF flag correctly in the Asm.compare_floats and Asm.compare_floats32 functions. - Update the proofs in Asmgenproof1 accordingly. No change required to the code generated for FP comparisons: this code already anticipated the "or unordered" case. Problem reported by Alix Trieu. --- x86/Asm.v | 12 ++++++------ 1 file changed, 6 insertions(+), 6 deletions(-) (limited to 'x86/Asm.v') diff --git a/x86/Asm.v b/x86/Asm.v index dfa2a88a..32235c2d 100644 --- a/x86/Asm.v +++ b/x86/Asm.v @@ -442,8 +442,8 @@ Definition compare_longs (x y: val) (rs: regset) (m: mem): regset := #PF <- Vundef. (** Floating-point comparison between x and y: -- ZF = 1 if x=y or unordered, 0 if x<>y -- CF = 1 if x=y +- ZF = 1 if x=y or unordered, 0 if x<>y and ordered +- CF = 1 if x=y. - PF = 1 if unordered, 0 if ordered. - SF and 0F are undefined *) @@ -451,9 +451,9 @@ Definition compare_longs (x y: val) (rs: regset) (m: mem): regset := Definition compare_floats (vx vy: val) (rs: regset) : regset := match vx, vy with | Vfloat x, Vfloat y => - rs #ZF <- (Val.of_bool (negb (Float.cmp Cne x y))) + rs #ZF <- (Val.of_bool (Float.cmp Ceq x y || negb (Float.ordered x y))) #CF <- (Val.of_bool (negb (Float.cmp Cge x y))) - #PF <- (Val.of_bool (negb (Float.cmp Ceq x y || Float.cmp Clt x y || Float.cmp Cgt x y))) + #PF <- (Val.of_bool (negb (Float.ordered x y))) #SF <- Vundef #OF <- Vundef | _, _ => @@ -463,9 +463,9 @@ Definition compare_floats (vx vy: val) (rs: regset) : regset := Definition compare_floats32 (vx vy: val) (rs: regset) : regset := match vx, vy with | Vsingle x, Vsingle y => - rs #ZF <- (Val.of_bool (negb (Float32.cmp Cne x y))) + rs #ZF <- (Val.of_bool (Float32.cmp Ceq x y || negb (Float32.ordered x y))) #CF <- (Val.of_bool (negb (Float32.cmp Cge x y))) - #PF <- (Val.of_bool (negb (Float32.cmp Ceq x y || Float32.cmp Clt x y || Float32.cmp Cgt x y))) + #PF <- (Val.of_bool (negb (Float32.ordered x y))) #SF <- Vundef #OF <- Vundef | _, _ => -- cgit