search

resource-reasoning / jscert_dev

This repository is now abandoned in favour of using
https://github.com/jscert/jscert
Other
0 stars 0 forks source link

SameValue Algorithm for [[DefineOwnProperty]] is wrong #18

Closed IgnoredAmbience closed 9 years ago

IgnoredAmbience commented 9 years ago

Transferred from Gforge:

new one: problem with negative infinity: tests/test262/ch11/11.4/11.4.7/S11.4.7_A4.2.js The problem doesn't appear to be with negation itself, but with assigning -0 to an already declared variable with a value of 0: x = 0; x = -0; 1/x; //inf Similarly: x = -0; x = 0; 1/x; //-inf Sounds like an overly lax equality check going on somewhere...?
IgnoredAmbience commented 9 years ago

This is still failing on all branches.

(Original bug: https://gforge.inria.fr/tracker/index.php?func=detail&aid=16194&group_id=4179&atid=13867)

IgnoredAmbience commented 9 years ago

Confirmed that:

var x = 0;
x = -0;
x    // returns: 0
var y = -0;
y = 0;
y    // returns: -0
IgnoredAmbience commented 9 years ago

8.12.9.6: Return true, if every field in Desc also occurs in current and the value of every field in Desc is the same value as the corresponding field in current when compared using the SameValue algorithm (9.12).

9.12.4.b/c: If x is +0 and y is -0, return false. If x is -0 and y is +0, return false.

Ah. Here's the bug: https://github.com/resource-reasoning/jscert_dev/blob/master/coq/JsCommon.v#L136 same_value is not the same as logical equality for zero.

IgnoredAmbience commented 9 years ago

Aaah. Just realised my problem is with prop_decidable. The documentation clearly states that it isn't extractable.