#15569: Constant folding optimises 1 into 3 -------------------------------------+------------------------------------- Reporter: snowleopard | Owner: (none) Type: bug | Status: new Priority: normal | Milestone: 8.6.1 Component: Compiler | Version: 8.6.1-beta1 Resolution: | Keywords: Operating System: Unknown/Multiple | Architecture: | Unknown/Multiple Type of failure: None/Unknown | Test Case: Blocked By: | Blocking: Related Tickets: #9136 | Differential Rev(s): Wiki Page: | -------------------------------------+------------------------------------- Changes (by snowleopard): * related: => #9136 -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/15569#comment:1 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler

#15569: Constant folding optimises 1 into 3 -------------------------------------+------------------------------------- Reporter: snowleopard | Owner: (none) Type: bug | Status: new Priority: highest | Milestone: 8.6.1 Component: Compiler | Version: 8.6.1-beta1 Resolution: | Keywords: Operating System: Unknown/Multiple | Architecture: | Unknown/Multiple Type of failure: None/Unknown | Test Case: Blocked By: | Blocking: Related Tickets: #9136 | Differential Rev(s): Wiki Page: | -------------------------------------+------------------------------------- Changes (by mpickering): * priority: normal => highest -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/15569#comment:3 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler

#15569: Constant folding optimises 1 into 3 -------------------------------------+------------------------------------- Reporter: snowleopard | Owner: (none) Type: bug | Status: new Priority: highest | Milestone: 8.6.1 Component: Compiler | Version: 8.6.1-beta1 Resolution: | Keywords: Operating System: Unknown/Multiple | Architecture: | Unknown/Multiple Type of failure: None/Unknown | Test Case: Blocked By: | Blocking: Related Tickets: #9136 | Differential Rev(s): Wiki Page: | -------------------------------------+------------------------------------- Changes (by bgamari): * cc: hsyl20 (added) Comment: Yes, I think we are going to need to revert Phab:D2858 for now. The fact that this snuck through CI until now is deeply concerning and I'm also far from convinced that there aren't more bugs lurking. -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/15569#comment:5 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler

#15569: Constant folding optimises 1 into 3 -------------------------------------+------------------------------------- Reporter: snowleopard | Owner: (none) Type: bug | Status: new Priority: highest | Milestone: 8.6.1 Component: Compiler | Version: 8.6.1-beta1 Resolution: | Keywords: Operating System: Unknown/Multiple | Architecture: | Unknown/Multiple Type of failure: None/Unknown | Test Case: Blocked By: | Blocking: Related Tickets: #9136 | Differential Rev(s): Wiki Page: | -------------------------------------+------------------------------------- Changes (by alpmestan): * cc: alpmestan (added) -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/15569#comment:7 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler

#15569: Constant folding optimises 1 into 3 -------------------------------------+------------------------------------- Reporter: snowleopard | Owner: (none) Type: bug | Status: new Priority: highest | Milestone: 8.6.1 Component: Compiler | Version: 8.6.1-beta1 Resolution: | Keywords: Operating System: Unknown/Multiple | Architecture: | Unknown/Multiple Type of failure: None/Unknown | Test Case: Blocked By: | Blocking: Related Tickets: #9136 | Differential Rev(s): Wiki Page: | -------------------------------------+------------------------------------- Comment (by Krzysztof Gogolewski ): In [changeset:"65eec9cfd4410c0e30b0ed06116c15f8ce3de49d/ghc" 65eec9cf/ghc]: {{{ #!CommitTicketReference repository="ghc" revision="65eec9cfd4410c0e30b0ed06116c15f8ce3de49d" Fix a constant folding rule Summary: One of the constant folding rules introduced in D2858 is: ``` (L y :-: v) :-: (L x :-: w) -> return $ mkL (y-x) `add` (w `add` v) ``` Or, after removing syntactic noise: `(y - v) - (x - w) ==> (y - x) + (w + v)`. This is incorrect, since the sign of `v` is changed from negative to positive. As a consequence, the following program prints `3` when compiled with `-O`: ``` -- This is just subtraction in disguise minus :: Int -> Int -> Int minus x y = (8 - y) - (8 - x) {-# NOINLINE minus #-} main :: IO () main = print (2 `minus` 1) ``` The correct rule is: `(y - v) - (x - w) ==> (y - x) + (w - v)`. This commit does the fix. I haven't found any other issues with the constant folding code, but it's difficult to be certain without some automated checking. Reviewers: bgamari, tdammers Subscribers: hsyl20, tdammers, rwbarton, carter GHC Trac Issues: #15569 Differential Revision: https://phabricator.haskell.org/D5109 }}} -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/15569#comment:9 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler

#15569: Constant folding optimises 1 into 3 -------------------------------------+------------------------------------- Reporter: snowleopard | Owner: (none) Type: bug | Status: new Priority: highest | Milestone: 8.6.1 Component: Compiler | Version: 8.6.1-beta1 Resolution: | Keywords: Operating System: Unknown/Multiple | Architecture: | Unknown/Multiple Type of failure: None/Unknown | Test Case: Blocked By: | Blocking: Related Tickets: #9136 | Differential Rev(s): Phab:D5109 Wiki Page: | -------------------------------------+------------------------------------- Changes (by ChaiTRex): * Attachment "ConstantFolding.hs" added. Constant folding tester program -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/15569 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler

#15569: Constant folding optimises 1 into 3 -------------------------------------+------------------------------------- Reporter: snowleopard | Owner: (none) Type: bug | Status: new Priority: highest | Milestone: 8.6.1 Component: Compiler | Version: 8.6.1-beta1 Resolution: | Keywords: Operating System: Unknown/Multiple | Architecture: | Unknown/Multiple Type of failure: None/Unknown | Test Case: Blocked By: | Blocking: Related Tickets: #9136 | Differential Rev(s): Phab:D5109 Wiki Page: | -------------------------------------+------------------------------------- Comment (by ChaiTRex): = Semi-exhaustive testing is being performed using GHC before the fix = Using the attached program, I'm doing semi-exhaustive testing of constant folding up to an expression nesting depth of two (up to something like `(a + b)*(c + d)`) with literal and variable values in `[0, 1, 3, 7] :: [Int]`. Note that the attached program takes the better part of a day, so it might not be prudent to add it to the test suite unless that can be significantly reduced or a "very, very slow" testing option can be added. == Testing is being done before fix == To ensure the tester actually detects problems, the tester program was performed until it detected this bug report's bug with GHC before the fix (at GHC commit `ff29fc84c03c800cfa04c2a00eb8edf6fa5f4183`). The tester program is still running and full output will be attached when the program finishes. The first few lines of output are: {{{ ERROR! ((0 - x0) - (0 - x1)) is optimized incorrectly! ERROR! ((0 - x0) - (1 - x0)) is optimized incorrectly! ERROR! ((0 - x0) - (1 - x1)) is optimized incorrectly! ERROR! ((0 - x0) - (3 - x0)) is optimized incorrectly! ⋮ ⋮ ⋮ ⋮ ⋮ ⋮ ⋮ ⋮ ⋮ ⋮ ⋮ ⋮ ⋮ ⋮ ⋮ ⋮ }}} == Testing will be done after fix == Testing will next be performed using GHC at `HEAD` (after the above fix). Results will be posted in my next comment in about a day. == The program == There are two modules attached: * `ThisGHC.hs`: a Template Haskell helper module for running the specific GHC installation a program was compiled with. * `ConstantFolding.hs`: a program that repeatedly compiles a certain number of expressions at a time (to avoid heap overflows from compiling all expressions at once) with `-O2` and tests their output against those expressions compiled with `-O0`. -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/15569#comment:11 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler

#15569: Constant folding optimises 1 into 3 -------------------------------------+------------------------------------- Reporter: snowleopard | Owner: (none) Type: bug | Status: new Priority: highest | Milestone: 8.6.1 Component: Compiler | Version: 8.6.1-beta1 Resolution: | Keywords: Operating System: Unknown/Multiple | Architecture: | Unknown/Multiple Type of failure: None/Unknown | Test Case: Blocked By: | Blocking: Related Tickets: #9136 | Differential Rev(s): Phab:D5109 Wiki Page: | -------------------------------------+------------------------------------- Comment (by osa1): I think we'll be releasing 8.6.1 with the constant folding patch so we should run ChaiTRex's test program at least once before releasing. ChaiTRex, you said you'll be posting results, do you have the results yet? I'll also try to run it on my system. -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/15569#comment:13 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler

#15569: Constant folding optimises 1 into 3 -------------------------------------+------------------------------------- Reporter: snowleopard | Owner: (none) Type: bug | Status: new Priority: highest | Milestone: 8.6.1 Component: Compiler | Version: 8.6.1-beta1 Resolution: | Keywords: Operating System: Unknown/Multiple | Architecture: | Unknown/Multiple Type of failure: None/Unknown | Test Case: Blocked By: | Blocking: Related Tickets: #9136 | Differential Rev(s): Phab:D5109 Wiki Page: | -------------------------------------+------------------------------------- Comment (by ChaiTRex): Apologies for the delay: I had no power for a while and had to restart. The results before the patch are attached and point out only this bug. The results after the patch point out no bugs: {{{ }}} So, `Int`s look good on my end, at least up to an expression nesting depth of two (''i.e.'', up to something like `(a + b)*(c + d)`). For any future needs, I've put a newly-multithreaded version of the tester on GitHub at [https://github.com/ChaiTRex/ConstantFoldingTest ChaiTRex/ConstantFoldingTest]. -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/15569#comment:14 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler

#15569: Constant folding optimises 1 into 3 -------------------------------------+------------------------------------- Reporter: snowleopard | Owner: (none) Type: bug | Status: new Priority: highest | Milestone: 8.6.1 Component: Compiler | Version: 8.6.1-beta1 Resolution: | Keywords: Operating System: Unknown/Multiple | Architecture: | Unknown/Multiple Type of failure: None/Unknown | Test Case: Blocked By: | Blocking: Related Tickets: #9136 | Differential Rev(s): Phab:D5109 Wiki Page: | -------------------------------------+------------------------------------- Comment (by sgraf): For the record, here's ~~a paper~~ [https://arxiv.org/pdf/1809.02161.pdf a report] about how these kind of optimisations should be specified in a declarative language (like snowleopard's attempt above). Ultimately, these declarations could be synthesised by an SMT solver out of a language semantics (a.k.a. algebraic structure, in our case). -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/15569#comment:16 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler

#15569: Constant folding optimises 1 into 3 -------------------------------------+------------------------------------- Reporter: snowleopard | Owner: (none) Type: bug | Status: new Priority: highest | Milestone: 8.6.1 Component: Compiler | Version: 8.6.1-beta1 Resolution: | Keywords: Operating System: Unknown/Multiple | Architecture: | Unknown/Multiple Type of failure: None/Unknown | Test Case: Blocked By: | Blocking: Related Tickets: #9136 | Differential Rev(s): Phab:D5109 Wiki Page: | -------------------------------------+------------------------------------- Comment (by ChaiTRex): I've started reworking my code to generate a small subset of test cases that use one specific fixed constant (100^th^ prime, 200^th^ prime, ''etc''. to avoid coincidentally passing tests) for each spot where a literal or variable is expected, which should cut down significantly on the number of tests. I'd like to further cut down on the number of tests while still getting full coverage, but I've only skimmed some of the constant folding rules. Am I right in assuming that the following are true? * `Int`s are the only type we need to test (if this isn't true, my reworking will make the code take a type parameter, so generating tests for additional types will be simple). * The following expression shapes are the only ones required, where `∘` is multiplication, addition, or subtraction and where multiple occurrences in one expression can represent different operations. '''Note:''' negation stops after single-`∘` expressions: * `a` * `-a` * `a ∘ b` * `a ∘ -b` * `-a ∘ b` * `a ∘ (b ∘ c)` * `(a ∘ b) ∘ c` * `(a ∘ b) ∘ (c ∘ d)` -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/15569#comment:18 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler

#15569: Constant folding optimises 1 into 3 -------------------------------------+------------------------------------- Reporter: snowleopard | Owner: (none) Type: bug | Status: new Priority: highest | Milestone: 8.6.1 Component: Compiler | Version: 8.6.1-beta1 Resolution: | Keywords: Operating System: Unknown/Multiple | Architecture: | Unknown/Multiple Type of failure: None/Unknown | Test Case: Blocked By: | Blocking: Related Tickets: #9136 | Differential Rev(s): Phab:D5109 Wiki Page: | -------------------------------------+------------------------------------- Comment (by monoidal): I picked all rules from D2858, including the wrong and the correct version of `(L y :-: v) :-: (L x :-: w)` and used sympy to compute the difference between LHS and RHS symbolically. Result: all differences simplify to 0, except that one rule that was found to be wrong. Code: https://gist.github.com/monoidal/3d5565b986a013639389fc57081d2781 All of the rules use addition, subtraction and multiplication only (matters would be different if there was division). This makes me confident that the rules are algebraically correct. It doesn't mean the code is completely correct, but any remaining errors will be of different nature. If someone is willing to do further review, I would suggest things like: double-checking the code surrounding the rules, checking if integer overflow can occur, does this apply only to Int/Integer or other types etc. -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/15569#comment:20 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler

#15569: Constant folding optimises 1 into 3 -------------------------------------+------------------------------------- Reporter: snowleopard | Owner: (none) Type: bug | Status: new Priority: highest | Milestone: 8.6.1 Component: Compiler | Version: 8.6.1-beta1 Resolution: | Keywords: Operating System: Unknown/Multiple | Architecture: | Unknown/Multiple Type of failure: None/Unknown | Test Case: Blocked By: | Blocking: Related Tickets: #9136 | Differential Rev(s): Phab:D5109 Wiki Page: | -------------------------------------+------------------------------------- Comment (by sgraf): @jean, I'm not particularly invested in the field, but on page 6 in the report I linked there is a table of superoptimizers (I confused these with supercompilation in the past, which is totally different), the respective papers of which might be a good start. In particular, everything doing "synthesis" is probably fueled by an SMT solver. I think the essence boils down to formalising source and target language (which should be same algebraic structure in our example) and let the SMT solver synthesize a RHS to a given LHS expression which has minimal cost wrt. some metric. This seems like the most recent approach: https://arxiv.org/pdf/1711.04422.pdf -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/15569#comment:22 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler