diff options
| author | Xavier Leroy <xavier.leroy@college-de-france.fr> | 2018-12-03 15:08:53 +0100 |
|---|---|---|
| committer | Xavier Leroy <xavierleroy@users.noreply.github.com> | 2018-12-20 15:19:42 +0100 |
| commit | 50fd8fe358b0eacb92d4cc28b6ada062e38023f5 (patch) | |
| tree | 80aca4c074539d5c773e8eab476af133c9edbedf /x86/Asm.v | |
| parent | 88e9a78529282605f097bff78c6604524d25b592 (diff) | |
| download | compcert-50fd8fe358b0eacb92d4cc28b6ada062e38023f5.tar.gz compcert-50fd8fe358b0eacb92d4cc28b6ada062e38023f5.zip | |
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.
Diffstat (limited to 'x86/Asm.v')
| -rw-r--r-- | x86/Asm.v | 12 |
1 files changed, 6 insertions, 6 deletions
@@ -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 or unordered, 0 if x>=y +- ZF = 1 if x=y or unordered, 0 if x<>y and ordered +- CF = 1 if x<y or unordered, 0 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 | _, _ => |