Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Jump to bottom

StackOverflowError in patmat analysis (regression from 2.11.x) #10387

Closed
larsrh opened this issue Jun 22, 2017 · 4 comments
Closed

StackOverflowError in patmat analysis (regression from 2.11.x) #10387

larsrh opened this issue Jun 22, 2017 · 4 comments
Assignees
@hrhino
Labels
compiler crash patmat
Milestone
2.12.5

Comments

@larsrh
Copy link

larsrh commented Jun 22, 2017

The attached file contains an excerpt from code generated by Isabelle. Admittedly, it is a very large pattern match.

test2.scala.txt

Here are the behaviours of various Scala versions:

$ time ./scalas/scala-2.11.8/bin/scalac -d bin test2.scala 
test2.scala:11: warning: match may not be exhaustive.
It would fail on the following input: Char(Bit0(_))
def integer_of_char(x0: char): BigInt = x0 match {
                                        ^
test2.scala:9: warning: Class foo$Char differs only in case from foo$char. Such classes will overwrite one another on case-insensitive filesystems.
final case class Char(a: num) extends char
                 ^
warning: there was one unchecked warning; re-run with -unchecked for details
three warnings found

real    0m55,346s
user    1m21,119s
sys     0m0,392s

$ time ./scalas/scala-2.11.10/bin/scalac -d bin test2.scala 
test2.scala:11: warning: match may not be exhaustive.
It would fail on the following input: Char(Bit0(Bit0(Bit1(Bit0(Bit1(Bit1(Bit0(Bit0(_)))))))))
def integer_of_char(x0: char): BigInt = x0 match {
                                        ^
test2.scala:9: warning: Class foo$Char differs only in case from foo$char. Such classes will overwrite one another on case-insensitive filesystems.
final case class Char(a: num) extends char
                 ^
warning: there was one unchecked warning; re-run with -unchecked for details
three warnings found

real    2m11,399s
user    2m46,762s
sys     0m0,457s

$ time ./scalas/scala-2.12.2/bin/scalac -d bin test2.scala
... snip ...
        at scala.tools.nsc.transform.patmat.Solving$Solver.findTseitinModelFor(Solving.scala:484)
        at scala.tools.nsc.transform.patmat.Solving$Solver.findTseitinModelFor$(Solving.scala:471)
        at scala.tools.nsc.transform.patmat.PatternMatching$OptimizingMatchTranslator.findTseitinModelFor(PatternMatching.scala:89)

real    0m31,439s
user    0m45,385s
sys     0m0,305s
@DarkDimius
Copy link
Member

ping @liufengyun, this might be a good test to add to Dotty.

@liufengyun
Copy link

Thanks @DarkDimius , just tried, it seems Dotty stackoverflow at Erasure.

@mcoblenz
Copy link

mcoblenz commented Dec 8, 2017 •
edited

I'm encountering this bug on my project, which is a language implementation. Stack overflow with a similar pattern of calls.

Specifically, one can reproduce with this repository: http://github.com/mcoblenz/Obsidian/

I've tried increasing the stack sizes but haven't solved the problem yet. Is there a way of telling which code is causing the problem so I can consider refactoring it?

hrhino added a commit to hrhino/scala that referenced this issue Dec 12, 2017
@hrhino
wip tailrecursive tseitin model solver (scala/bug#10387)
849edf1
@mcoblenz
Copy link

hrhino's patch above looks like it fixes this problem. I hope we can get the change merged in so everyone can benefit.

mcoblenz added a commit to mcoblenz/Obsidian that referenced this issue Dec 14, 2017
@mcoblenz
Adopt a custom version of Scalac to work around a scala compiler bug (s…
885dcca 
…cala/bug#10387).
@hrhino hrhino self-assigned this Dec 19, 2017
hrhino added a commit to hrhino/scala that referenced this issue Dec 20, 2017
@hrhino
Tail-recursive Tseitsin model solver.
480c2b7 
Large (hopefully computer-generated) matches can lead to a
search to become deep enough to send `findTseitinModelFor`
into a `StackOverflowError`. The change here is a faithful
reification of the call stack as a `List`.

This fixes scala/bug#10387.

Additionally, some `Set[Int]`s in which the elements won't
be negative are changed to use `BitSet`s instead, to maybe
help performance. My wholly unscientific benchmark against
the attached test case yields:

    ===== BEFORE =====

    time spent in patmat          : 11 spans, 145843ms
      of which DPLL               : 280 spans, 62026ms (42.5%)
      of which in CNF conversion  : 0 spans, 0ms (0.0%)
      of which variable equality  : 17 spans, 129ms (0.1%)
      of which in exhaustivity    : 1 spans, 26361ms (18.1%)
      of which in unreachability  : 8 spans, 101925ms (69.9%)

    time spent in patmat          : 11 spans, 161592ms
      of which DPLL               : 280 spans, 64320ms (39.8%)
      of which in CNF conversion  : 0 spans, 0ms (0.0%)
      of which variable equality  : 17 spans, 137ms (0.1%)
      of which in exhaustivity    : 1 spans, 29818ms (18.5%)
      of which in unreachability  : 8 spans, 110926ms (68.6%)

    time spent in patmat          : 11 spans, 161660ms
      of which DPLL               : 280 spans, 68797ms (42.6%)
      of which in CNF conversion  : 0 spans, 0ms (0.0%)
      of which variable equality  : 17 spans, 142ms (0.1%)
      of which in exhaustivity    : 1 spans, 27751ms (17.2%)
      of which in unreachability  : 8 spans, 114899ms (71.1%)

    time spent in patmat          : 11 spans, 151320ms
      of which DPLL               : 280 spans, 64325ms (42.5%)
      of which in CNF conversion  : 0 spans, 0ms (0.0%)
      of which variable equality  : 17 spans, 126ms (0.1%)
      of which in exhaustivity    : 1 spans, 26645ms (17.6%)
      of which in unreachability  : 8 spans, 106730ms (70.5%)

    time spent in patmat          : 11 spans, 143872ms
      of which DPLL               : 280 spans, 62331ms (43.3%)
      of which in CNF conversion  : 0 spans, 0ms (0.0%)
      of which variable equality  : 17 spans, 134ms (0.1%)
      of which in exhaustivity    : 1 spans, 24667ms (17.1%)
      of which in unreachability  : 8 spans, 102261ms (71.1%)

    ===== AFTER =====

    time spent in patmat          : 11 spans, 138693ms
      of which DPLL               : 280 spans, 42176ms (30.4%)
      of which in CNF conversion  : 0 spans, 0ms (0.0%)
      of which variable equality  : 17 spans, 195ms (0.1%)
      of which in exhaustivity    : 1 spans, 30043ms (21.7%)
      of which in unreachability  : 8 spans, 85335ms (61.5%)

    time spent in patmat          : 11 spans, 124888ms
      of which DPLL               : 280 spans, 40456ms (32.4%)
      of which in CNF conversion  : 0 spans, 0ms (0.0%)
      of which variable equality  : 17 spans, 134ms (0.1%)
      of which in exhaustivity    : 1 spans, 25034ms (20.0%)
      of which in unreachability  : 8 spans, 82255ms (65.9%)

    time spent in patmat          : 11 spans, 167081ms
      of which DPLL               : 280 spans, 40552ms (24.3%)
      of which in CNF conversion  : 0 spans, 0ms (0.0%)
      of which variable equality  : 17 spans, 223ms (0.1%)
      of which in exhaustivity    : 1 spans, 27742ms (16.6%)
      of which in unreachability  : 8 spans, 119810ms (71.7%)

    time spent in patmat          : 11 spans, 130727ms
      of which DPLL               : 280 spans, 40632ms (31.1%)
      of which in CNF conversion  : 0 spans, 0ms (0.0%)
      of which variable equality  : 17 spans, 158ms (0.1%)
      of which in exhaustivity    : 1 spans, 25878ms (19.8%)
      of which in unreachability  : 8 spans, 86081ms (65.8%)

    time spent in patmat          : 11 spans, 132853ms
      of which DPLL               : 280 spans, 41660ms (31.4%)
      of which in CNF conversion  : 0 spans, 0ms (0.0%)
      of which variable equality  : 17 spans, 142ms (0.1%)
      of which in exhaustivity    : 1 spans, 28138ms (21.2%)
      of which in unreachability  : 8 spans, 86297ms (65.0%)
hrhino added a commit to hrhino/scala that referenced this issue Dec 20, 2017
@hrhino
Tail-recursive Tseitsin model solver.
a2404b0 
Large (hopefully computer-generated) matches can lead to a
search to become deep enough to send `findTseitinModelFor`
into a `StackOverflowError`. The change here is a faithful
reification of the call stack as a `List`.

This fixes scala/bug#10387.

Additionally, some `Set[Int]`s in which the elements won't
be negative are changed to use `BitSet`s instead, to maybe
help performance. My wholly unscientific benchmark against
the attached test case yields:

    ===== BEFORE =====

    time spent in patmat          : 11 spans, 145843ms
      of which DPLL               : 280 spans, 62026ms (42.5%)
      of which in CNF conversion  : 0 spans, 0ms (0.0%)
      of which variable equality  : 17 spans, 129ms (0.1%)
      of which in exhaustivity    : 1 spans, 26361ms (18.1%)
      of which in unreachability  : 8 spans, 101925ms (69.9%)

    time spent in patmat          : 11 spans, 161592ms
      of which DPLL               : 280 spans, 64320ms (39.8%)
      of which in CNF conversion  : 0 spans, 0ms (0.0%)
      of which variable equality  : 17 spans, 137ms (0.1%)
      of which in exhaustivity    : 1 spans, 29818ms (18.5%)
      of which in unreachability  : 8 spans, 110926ms (68.6%)

    time spent in patmat          : 11 spans, 161660ms
      of which DPLL               : 280 spans, 68797ms (42.6%)
      of which in CNF conversion  : 0 spans, 0ms (0.0%)
      of which variable equality  : 17 spans, 142ms (0.1%)
      of which in exhaustivity    : 1 spans, 27751ms (17.2%)
      of which in unreachability  : 8 spans, 114899ms (71.1%)

    time spent in patmat          : 11 spans, 151320ms
      of which DPLL               : 280 spans, 64325ms (42.5%)
      of which in CNF conversion  : 0 spans, 0ms (0.0%)
      of which variable equality  : 17 spans, 126ms (0.1%)
      of which in exhaustivity    : 1 spans, 26645ms (17.6%)
      of which in unreachability  : 8 spans, 106730ms (70.5%)

    time spent in patmat          : 11 spans, 143872ms
      of which DPLL               : 280 spans, 62331ms (43.3%)
      of which in CNF conversion  : 0 spans, 0ms (0.0%)
      of which variable equality  : 17 spans, 134ms (0.1%)
      of which in exhaustivity    : 1 spans, 24667ms (17.1%)
      of which in unreachability  : 8 spans, 102261ms (71.1%)

    ===== AFTER =====

    time spent in patmat          : 11 spans, 138693ms
      of which DPLL               : 280 spans, 42176ms (30.4%)
      of which in CNF conversion  : 0 spans, 0ms (0.0%)
      of which variable equality  : 17 spans, 195ms (0.1%)
      of which in exhaustivity    : 1 spans, 30043ms (21.7%)
      of which in unreachability  : 8 spans, 85335ms (61.5%)

    time spent in patmat          : 11 spans, 124888ms
      of which DPLL               : 280 spans, 40456ms (32.4%)
      of which in CNF conversion  : 0 spans, 0ms (0.0%)
      of which variable equality  : 17 spans, 134ms (0.1%)
      of which in exhaustivity    : 1 spans, 25034ms (20.0%)
      of which in unreachability  : 8 spans, 82255ms (65.9%)

    time spent in patmat          : 11 spans, 167081ms
      of which DPLL               : 280 spans, 40552ms (24.3%)
      of which in CNF conversion  : 0 spans, 0ms (0.0%)
      of which variable equality  : 17 spans, 223ms (0.1%)
      of which in exhaustivity    : 1 spans, 27742ms (16.6%)
      of which in unreachability  : 8 spans, 119810ms (71.7%)

    time spent in patmat          : 11 spans, 130727ms
      of which DPLL               : 280 spans, 40632ms (31.1%)
      of which in CNF conversion  : 0 spans, 0ms (0.0%)
      of which variable equality  : 17 spans, 158ms (0.1%)
      of which in exhaustivity    : 1 spans, 25878ms (19.8%)
      of which in unreachability  : 8 spans, 86081ms (65.8%)

    time spent in patmat          : 11 spans, 132853ms
      of which DPLL               : 280 spans, 41660ms (31.4%)
      of which in CNF conversion  : 0 spans, 0ms (0.0%)
      of which variable equality  : 17 spans, 142ms (0.1%)
      of which in exhaustivity    : 1 spans, 28138ms (21.2%)
      of which in unreachability  : 8 spans, 86297ms (65.0%)
hrhino added a commit to hrhino/scala that referenced this issue Dec 20, 2017
@hrhino
Tail-recursive Tseitsin model solver.
3e437c1 
Large (hopefully computer-generated) matches can lead to a
search to become deep enough to send `findTseitinModelFor`
into a `StackOverflowError`. The change here is a faithful
reification of the call stack as a `List`.

This fixes scala/bug#10387.

Additionally, some `Set[Int]`s in which the elements won't
be negative are changed to use `BitSet`s instead, to maybe
help performance. My wholly unscientific benchmark against
the attached test case yields:

    ===== BEFORE =====

    time spent in patmat          : 11 spans, 145843ms
      of which DPLL               : 280 spans, 62026ms (42.5%)
      of which in CNF conversion  : 0 spans, 0ms (0.0%)
      of which variable equality  : 17 spans, 129ms (0.1%)
      of which in exhaustivity    : 1 spans, 26361ms (18.1%)
      of which in unreachability  : 8 spans, 101925ms (69.9%)

    time spent in patmat          : 11 spans, 161592ms
      of which DPLL               : 280 spans, 64320ms (39.8%)
      of which in CNF conversion  : 0 spans, 0ms (0.0%)
      of which variable equality  : 17 spans, 137ms (0.1%)
      of which in exhaustivity    : 1 spans, 29818ms (18.5%)
      of which in unreachability  : 8 spans, 110926ms (68.6%)

    time spent in patmat          : 11 spans, 161660ms
      of which DPLL               : 280 spans, 68797ms (42.6%)
      of which in CNF conversion  : 0 spans, 0ms (0.0%)
      of which variable equality  : 17 spans, 142ms (0.1%)
      of which in exhaustivity    : 1 spans, 27751ms (17.2%)
      of which in unreachability  : 8 spans, 114899ms (71.1%)

    time spent in patmat          : 11 spans, 151320ms
      of which DPLL               : 280 spans, 64325ms (42.5%)
      of which in CNF conversion  : 0 spans, 0ms (0.0%)
      of which variable equality  : 17 spans, 126ms (0.1%)
      of which in exhaustivity    : 1 spans, 26645ms (17.6%)
      of which in unreachability  : 8 spans, 106730ms (70.5%)

    time spent in patmat          : 11 spans, 143872ms
      of which DPLL               : 280 spans, 62331ms (43.3%)
      of which in CNF conversion  : 0 spans, 0ms (0.0%)
      of which variable equality  : 17 spans, 134ms (0.1%)
      of which in exhaustivity    : 1 spans, 24667ms (17.1%)
      of which in unreachability  : 8 spans, 102261ms (71.1%)

    ===== AFTER =====

    time spent in patmat          : 11 spans, 138693ms
      of which DPLL               : 280 spans, 42176ms (30.4%)
      of which in CNF conversion  : 0 spans, 0ms (0.0%)
      of which variable equality  : 17 spans, 195ms (0.1%)
      of which in exhaustivity    : 1 spans, 30043ms (21.7%)
      of which in unreachability  : 8 spans, 85335ms (61.5%)

    time spent in patmat          : 11 spans, 124888ms
      of which DPLL               : 280 spans, 40456ms (32.4%)
      of which in CNF conversion  : 0 spans, 0ms (0.0%)
      of which variable equality  : 17 spans, 134ms (0.1%)
      of which in exhaustivity    : 1 spans, 25034ms (20.0%)
      of which in unreachability  : 8 spans, 82255ms (65.9%)

    time spent in patmat          : 11 spans, 167081ms
      of which DPLL               : 280 spans, 40552ms (24.3%)
      of which in CNF conversion  : 0 spans, 0ms (0.0%)
      of which variable equality  : 17 spans, 223ms (0.1%)
      of which in exhaustivity    : 1 spans, 27742ms (16.6%)
      of which in unreachability  : 8 spans, 119810ms (71.7%)

    time spent in patmat          : 11 spans, 130727ms
      of which DPLL               : 280 spans, 40632ms (31.1%)
      of which in CNF conversion  : 0 spans, 0ms (0.0%)
      of which variable equality  : 17 spans, 158ms (0.1%)
      of which in exhaustivity    : 1 spans, 25878ms (19.8%)
      of which in unreachability  : 8 spans, 86081ms (65.8%)

    time spent in patmat          : 11 spans, 132853ms
      of which DPLL               : 280 spans, 41660ms (31.4%)
      of which in CNF conversion  : 0 spans, 0ms (0.0%)
      of which variable equality  : 17 spans, 142ms (0.1%)
      of which in exhaustivity    : 1 spans, 28138ms (21.2%)
      of which in unreachability  : 8 spans, 86297ms (65.0%)
hrhino added a commit to hrhino/scala that referenced this issue Dec 20, 2017
@hrhino
Tail-recursive Tseitsin model solver.
b9ec65f 
Large (hopefully computer-generated) matches can lead to a
search to become deep enough to send `findTseitinModelFor`
into a `StackOverflowError`. The change here is a faithful
reification of the call stack as a `List`.

This fixes scala/bug#10387.

Additionally, some `Set[Int]`s in which the elements won't
be negative are changed to use `BitSet`s instead, to maybe
help performance. My wholly unscientific benchmark against
the attached test case yields:

    ===== BEFORE =====

    time spent in patmat          : 11 spans, 145843ms
      of which DPLL               : 280 spans, 62026ms (42.5%)
      of which in CNF conversion  : 0 spans, 0ms (0.0%)
      of which variable equality  : 17 spans, 129ms (0.1%)
      of which in exhaustivity    : 1 spans, 26361ms (18.1%)
      of which in unreachability  : 8 spans, 101925ms (69.9%)

    time spent in patmat          : 11 spans, 161592ms
      of which DPLL               : 280 spans, 64320ms (39.8%)
      of which in CNF conversion  : 0 spans, 0ms (0.0%)
      of which variable equality  : 17 spans, 137ms (0.1%)
      of which in exhaustivity    : 1 spans, 29818ms (18.5%)
      of which in unreachability  : 8 spans, 110926ms (68.6%)

    time spent in patmat          : 11 spans, 161660ms
      of which DPLL               : 280 spans, 68797ms (42.6%)
      of which in CNF conversion  : 0 spans, 0ms (0.0%)
      of which variable equality  : 17 spans, 142ms (0.1%)
      of which in exhaustivity    : 1 spans, 27751ms (17.2%)
      of which in unreachability  : 8 spans, 114899ms (71.1%)

    time spent in patmat          : 11 spans, 151320ms
      of which DPLL               : 280 spans, 64325ms (42.5%)
      of which in CNF conversion  : 0 spans, 0ms (0.0%)
      of which variable equality  : 17 spans, 126ms (0.1%)
      of which in exhaustivity    : 1 spans, 26645ms (17.6%)
      of which in unreachability  : 8 spans, 106730ms (70.5%)

    time spent in patmat          : 11 spans, 143872ms
      of which DPLL               : 280 spans, 62331ms (43.3%)
      of which in CNF conversion  : 0 spans, 0ms (0.0%)
      of which variable equality  : 17 spans, 134ms (0.1%)
      of which in exhaustivity    : 1 spans, 24667ms (17.1%)
      of which in unreachability  : 8 spans, 102261ms (71.1%)

    ===== AFTER =====

    time spent in patmat          : 11 spans, 138693ms
      of which DPLL               : 280 spans, 42176ms (30.4%)
      of which in CNF conversion  : 0 spans, 0ms (0.0%)
      of which variable equality  : 17 spans, 195ms (0.1%)
      of which in exhaustivity    : 1 spans, 30043ms (21.7%)
      of which in unreachability  : 8 spans, 85335ms (61.5%)

    time spent in patmat          : 11 spans, 124888ms
      of which DPLL               : 280 spans, 40456ms (32.4%)
      of which in CNF conversion  : 0 spans, 0ms (0.0%)
      of which variable equality  : 17 spans, 134ms (0.1%)
      of which in exhaustivity    : 1 spans, 25034ms (20.0%)
      of which in unreachability  : 8 spans, 82255ms (65.9%)

    time spent in patmat          : 11 spans, 167081ms
      of which DPLL               : 280 spans, 40552ms (24.3%)
      of which in CNF conversion  : 0 spans, 0ms (0.0%)
      of which variable equality  : 17 spans, 223ms (0.1%)
      of which in exhaustivity    : 1 spans, 27742ms (16.6%)
      of which in unreachability  : 8 spans, 119810ms (71.7%)

    time spent in patmat          : 11 spans, 130727ms
      of which DPLL               : 280 spans, 40632ms (31.1%)
      of which in CNF conversion  : 0 spans, 0ms (0.0%)
      of which variable equality  : 17 spans, 158ms (0.1%)
      of which in exhaustivity    : 1 spans, 25878ms (19.8%)
      of which in unreachability  : 8 spans, 86081ms (65.8%)

    time spent in patmat          : 11 spans, 132853ms
      of which DPLL               : 280 spans, 41660ms (31.4%)
      of which in CNF conversion  : 0 spans, 0ms (0.0%)
      of which variable equality  : 17 spans, 142ms (0.1%)
      of which in exhaustivity    : 1 spans, 28138ms (21.2%)
      of which in unreachability  : 8 spans, 86297ms (65.0%)
hrhino added a commit to hrhino/scala that referenced this issue Dec 21, 2017
@hrhino
Tail-recursive Tseitin model solver.
51c5183 
Large (hopefully computer-generated) matches can lead to a
search to become deep enough to send `findTseitinModelFor`
into a `StackOverflowError`. The change here is a faithful
reification of the call stack as a `List`.

This fixes scala/bug#10387.

Additionally, some `Set[Int]`s in which the elements won't
be negative are changed to use `BitSet`s instead, to maybe
help performance. My wholly unscientific benchmark against
the attached test case yields:

    ===== BEFORE =====

    time spent in patmat          : 11 spans, 145843ms
      of which DPLL               : 280 spans, 62026ms (42.5%)
      of which in CNF conversion  : 0 spans, 0ms (0.0%)
      of which variable equality  : 17 spans, 129ms (0.1%)
      of which in exhaustivity    : 1 spans, 26361ms (18.1%)
      of which in unreachability  : 8 spans, 101925ms (69.9%)

    time spent in patmat          : 11 spans, 161592ms
      of which DPLL               : 280 spans, 64320ms (39.8%)
      of which in CNF conversion  : 0 spans, 0ms (0.0%)
      of which variable equality  : 17 spans, 137ms (0.1%)
      of which in exhaustivity    : 1 spans, 29818ms (18.5%)
      of which in unreachability  : 8 spans, 110926ms (68.6%)

    time spent in patmat          : 11 spans, 161660ms
      of which DPLL               : 280 spans, 68797ms (42.6%)
      of which in CNF conversion  : 0 spans, 0ms (0.0%)
      of which variable equality  : 17 spans, 142ms (0.1%)
      of which in exhaustivity    : 1 spans, 27751ms (17.2%)
      of which in unreachability  : 8 spans, 114899ms (71.1%)

    time spent in patmat          : 11 spans, 151320ms
      of which DPLL               : 280 spans, 64325ms (42.5%)
      of which in CNF conversion  : 0 spans, 0ms (0.0%)
      of which variable equality  : 17 spans, 126ms (0.1%)
      of which in exhaustivity    : 1 spans, 26645ms (17.6%)
      of which in unreachability  : 8 spans, 106730ms (70.5%)

    time spent in patmat          : 11 spans, 143872ms
      of which DPLL               : 280 spans, 62331ms (43.3%)
      of which in CNF conversion  : 0 spans, 0ms (0.0%)
      of which variable equality  : 17 spans, 134ms (0.1%)
      of which in exhaustivity    : 1 spans, 24667ms (17.1%)
      of which in unreachability  : 8 spans, 102261ms (71.1%)

    ===== AFTER =====

    time spent in patmat          : 11 spans, 138693ms
      of which DPLL               : 280 spans, 42176ms (30.4%)
      of which in CNF conversion  : 0 spans, 0ms (0.0%)
      of which variable equality  : 17 spans, 195ms (0.1%)
      of which in exhaustivity    : 1 spans, 30043ms (21.7%)
      of which in unreachability  : 8 spans, 85335ms (61.5%)

    time spent in patmat          : 11 spans, 124888ms
      of which DPLL               : 280 spans, 40456ms (32.4%)
      of which in CNF conversion  : 0 spans, 0ms (0.0%)
      of which variable equality  : 17 spans, 134ms (0.1%)
      of which in exhaustivity    : 1 spans, 25034ms (20.0%)
      of which in unreachability  : 8 spans, 82255ms (65.9%)

    time spent in patmat          : 11 spans, 167081ms
      of which DPLL               : 280 spans, 40552ms (24.3%)
      of which in CNF conversion  : 0 spans, 0ms (0.0%)
      of which variable equality  : 17 spans, 223ms (0.1%)
      of which in exhaustivity    : 1 spans, 27742ms (16.6%)
      of which in unreachability  : 8 spans, 119810ms (71.7%)

    time spent in patmat          : 11 spans, 130727ms
      of which DPLL               : 280 spans, 40632ms (31.1%)
      of which in CNF conversion  : 0 spans, 0ms (0.0%)
      of which variable equality  : 17 spans, 158ms (0.1%)
      of which in exhaustivity    : 1 spans, 25878ms (19.8%)
      of which in unreachability  : 8 spans, 86081ms (65.8%)

    time spent in patmat          : 11 spans, 132853ms
      of which DPLL               : 280 spans, 41660ms (31.4%)
      of which in CNF conversion  : 0 spans, 0ms (0.0%)
      of which variable equality  : 17 spans, 142ms (0.1%)
      of which in exhaustivity    : 1 spans, 28138ms (21.2%)
      of which in unreachability  : 8 spans, 86297ms (65.0%)
@hrhino hrhino mentioned this issue Dec 21, 2017
Merged
@hrhino hrhino added this to the 2.12.5 milestone Dec 21, 2017
hrhino added a commit to hrhino/scala that referenced this issue Dec 22, 2017
@hrhino
Tail-recursive Tseitin model solver.
627781b 
Large (hopefully computer-generated) matches can lead to a
search to become deep enough to send `findTseitinModelFor`
into a `StackOverflowError`. The change here is a faithful
reification of the call stack as a `List`.

This fixes scala/bug#10387.

Additionally, some `Set[Int]`s in which the elements won't
be negative are changed to use `BitSet`s instead, to maybe
help performance. My wholly unscientific benchmark against
the attached test case yields:

    ===== BEFORE =====

    time spent in patmat          : 11 spans, 145843ms
      of which DPLL               : 280 spans, 62026ms (42.5%)
      of which in CNF conversion  : 0 spans, 0ms (0.0%)
      of which variable equality  : 17 spans, 129ms (0.1%)
      of which in exhaustivity    : 1 spans, 26361ms (18.1%)
      of which in unreachability  : 8 spans, 101925ms (69.9%)

    time spent in patmat          : 11 spans, 161592ms
      of which DPLL               : 280 spans, 64320ms (39.8%)
      of which in CNF conversion  : 0 spans, 0ms (0.0%)
      of which variable equality  : 17 spans, 137ms (0.1%)
      of which in exhaustivity    : 1 spans, 29818ms (18.5%)
      of which in unreachability  : 8 spans, 110926ms (68.6%)

    time spent in patmat          : 11 spans, 161660ms
      of which DPLL               : 280 spans, 68797ms (42.6%)
      of which in CNF conversion  : 0 spans, 0ms (0.0%)
      of which variable equality  : 17 spans, 142ms (0.1%)
      of which in exhaustivity    : 1 spans, 27751ms (17.2%)
      of which in unreachability  : 8 spans, 114899ms (71.1%)

    time spent in patmat          : 11 spans, 151320ms
      of which DPLL               : 280 spans, 64325ms (42.5%)
      of which in CNF conversion  : 0 spans, 0ms (0.0%)
      of which variable equality  : 17 spans, 126ms (0.1%)
      of which in exhaustivity    : 1 spans, 26645ms (17.6%)
      of which in unreachability  : 8 spans, 106730ms (70.5%)

    time spent in patmat          : 11 spans, 143872ms
      of which DPLL               : 280 spans, 62331ms (43.3%)
      of which in CNF conversion  : 0 spans, 0ms (0.0%)
      of which variable equality  : 17 spans, 134ms (0.1%)
      of which in exhaustivity    : 1 spans, 24667ms (17.1%)
      of which in unreachability  : 8 spans, 102261ms (71.1%)

    ===== AFTER =====

    time spent in patmat          : 11 spans, 138693ms
      of which DPLL               : 280 spans, 42176ms (30.4%)
      of which in CNF conversion  : 0 spans, 0ms (0.0%)
      of which variable equality  : 17 spans, 195ms (0.1%)
      of which in exhaustivity    : 1 spans, 30043ms (21.7%)
      of which in unreachability  : 8 spans, 85335ms (61.5%)

    time spent in patmat          : 11 spans, 124888ms
      of which DPLL               : 280 spans, 40456ms (32.4%)
      of which in CNF conversion  : 0 spans, 0ms (0.0%)
      of which variable equality  : 17 spans, 134ms (0.1%)
      of which in exhaustivity    : 1 spans, 25034ms (20.0%)
      of which in unreachability  : 8 spans, 82255ms (65.9%)

    time spent in patmat          : 11 spans, 167081ms
      of which DPLL               : 280 spans, 40552ms (24.3%)
      of which in CNF conversion  : 0 spans, 0ms (0.0%)
      of which variable equality  : 17 spans, 223ms (0.1%)
      of which in exhaustivity    : 1 spans, 27742ms (16.6%)
      of which in unreachability  : 8 spans, 119810ms (71.7%)

    time spent in patmat          : 11 spans, 130727ms
      of which DPLL               : 280 spans, 40632ms (31.1%)
      of which in CNF conversion  : 0 spans, 0ms (0.0%)
      of which variable equality  : 17 spans, 158ms (0.1%)
      of which in exhaustivity    : 1 spans, 25878ms (19.8%)
      of which in unreachability  : 8 spans, 86081ms (65.8%)

    time spent in patmat          : 11 spans, 132853ms
      of which DPLL               : 280 spans, 41660ms (31.4%)
      of which in CNF conversion  : 0 spans, 0ms (0.0%)
      of which variable equality  : 17 spans, 142ms (0.1%)
      of which in exhaustivity    : 1 spans, 28138ms (21.2%)
      of which in unreachability  : 8 spans, 86297ms (65.0%)
@lrytz lrytz closed this as completed Jan 5, 2018
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Assignees

@hrhino hrhino

Labels
compiler crash patmat
Projects
None yet
Milestone
2.12.5
Development

No branches or pull requests
6 participants
@lrytz @liufengyun @larsrh @DarkDimius @mcoblenz @hrhino