8000 SI-6942 more efficient unreachability analysis · scala/scala@f539781 · GitHub
[go: up one dir, main page]
Skip to content

Commit f539781

Browse files
adriaanmadriaanm
committed
SI-6942 more efficient unreachability analysis
Avoid blowing the stack/the analysis budget by more eagerly translating the propositions that model matches to CNF. First building a large proposition that represents the match, and then converting to CNF tends to blow the stack. Luckily, it's easy to convert to CNF as we go. The optimization relies on `CNF(P1 /\ ... /\ PN) == CNF(P1) ++ CNF(...) ++ CNF(PN)`: Normalizing a conjunction of propositions yields the same formula as concatenating the normalized conjuncts. CNF conversion is expensive for large propositions, so we push it down into the conjunction and then concatenate the resulting arrays of clauses (which is cheap). (CNF converts a free-form proposition into an `Array[Set[Lit]]`, where: - the Array's elements are /\'ed together; - and the Set's elements are \/'ed; - a Lit is a possibly negated variable.) NOTE: - removeVarEq may throw an AnalysisBudget.Exception - also reworked the interface used to build formula, so that we can more easily plug in SAT4J when the time comes
1 parent 1a63cf8 commit f539781

File tree

4 files changed

+348
-24
lines changed

4 files changed

+348
-24
lines changed

‎src/compiler/scala/tools/nsc/typechecker/PatternMatching.scala

Lines changed: 48 additions & 24 deletions
Original file line numberDiff line numberDiff line change
@@ -1954,7 +1954,8 @@ trait PatternMatching extends Transform with TypingTransformers with ast.TreeDSL
19541954
//
19551955
// TODO: for V1 representing x1 and V2 standing for x1.head, encode that
19561956
// V1 = Nil implies -(V2 = Ci) for all Ci in V2's domain (i.e., it is unassignable)
1957-
def removeVarEq(props: List[Prop], modelNull: Boolean = false): (Prop, List[Prop]) = {
1957+
// may throw an AnalysisBudget.Exception
1958+
def removeVarEq(props: List[Prop], modelNull: Boolean = false): (Formula, List[Formula]) = {
19581959
val start = if (Statistics.canEnable) Statistics.startTimer(patmatAnaVarEq) else null
19591960

19601961
val vars = new scala.collection.mutable.HashSet[Var]
@@ -1978,10 +1979,10 @@ trait PatternMatching extends Transform with TypingTransformers with ast.TreeDSL
19781979
props foreach gatherEqualities.apply
19791980
if (modelNull) vars foreach (_.registerNull)
19801981

1981-
val pure = props map rewriteEqualsToProp.apply
1982+
val pure = props map (p => eqFreePropToSolvable(rewriteEqualsToProp(p)))
19821983

1983-
var eqAxioms: Prop = True
1984-
def addAxiom(p: Prop) = eqAxioms = And(eqAxioms, p)
1984+
val eqAxioms = formulaBuilder
1985+
@inline def addAxiom(p: Prop) = addFormula(eqAxioms, eqFreePropToSolvable(p))
19851986

19861987
patmatDebug("removeVarEq vars: "+ vars)
19871988
vars.foreach { v =>
@@ -2007,23 +2008,37 @@ trait PatternMatching extends Transform with TypingTransformers with ast.TreeDSL
20072008
}
20082009
}
20092010

2010-
patmatDebug("eqAxioms:\n"+ cnfString(eqFreePropToSolvable(eqAxioms)))
2011-
patmatDebug("pure:"+ pure.map(p => cnfString(eqFreePropToSolvable(p))).mkString("\n"))
2011+
patmatDebug("eqAxioms:\n"+ cnfString(toFormula(eqAxioms)))
2012+
patmatDebug("pure:"+ pure.map(p => cnfString(p)).mkString("\n"))
20122013

20132014
if (Statistics.canEnable) Statistics.stopTimer(patmatAnaVarEq, start)
20142015

2015-
(eqAxioms, pure)
2016+
(toFormula(eqAxioms), pure)
20162017
}
20172018

20182019

2020+
// an interface that should be suitable for feeding a SAT solver when the time comes
20192021
type Formula
2022+
type FormulaBuilder
2023+
2024+
// creates an empty formula builder to which more formulae can be added
2025+
def formulaBuilder: FormulaBuilder
2026+
2027+
// val f = formulaBuilder; addFormula(f, f1); ... addFormula(f, fN)
2028+
// toFormula(f) == andFormula(f1, andFormula(..., fN))
2029+
def addFormula(buff: FormulaBuilder, f: Formula): Unit
2030+
def toFormula(buff: FormulaBuilder): Formula
2031+
2032+
// the conjunction of formulae `a` and `b`
20202033
def andFormula(a: Formula, b: Formula): Formula
20212034

2035+
// equivalent formula to `a`, but simplified in a lightweight way (drop duplicate clauses)
2036+
def simplifyFormula(a: Formula): Formula
20222037

20232038
// may throw an AnalysisBudget.Exception
20242039
def propToSolvable(p: Prop): Formula = {
20252040
val (eqAxioms, pure :: Nil) = removeVarEq(List(p), modelNull = false)
2026-
eqFreePropToSolvable(And(eqAxioms, pure))
2041+
andFormula(eqAxioms, pure)
20272042
}
20282043

20292044
// may throw an AnalysisBudget.Exception
@@ -2039,24 +2054,34 @@ trait PatternMatching extends Transform with TypingTransformers with ast.TreeDSL
20392054
}
20402055

20412056
trait CNF extends Logic {
2042-
// CNF: a formula is a conjunction of clauses
2043-
type Formula = Array[Clause]
20442057
/** Override Array creation for efficiency (to not go through reflection). */
20452058
private implicit val clauseTag: scala.reflect.ClassTag[Clause] = new scala.reflect.ClassTag[Clause] {
20462059
def runtimeClass: java.lang.Class[Clause] = classOf[Clause]
20472060
final override def newArray(len: Int): Array[Clause] = new Array[Clause](len)
20482061
}
2062+
2063+
import scala.collection.mutable.ArrayBuffer
2064+
type FormulaBuilder = ArrayBuffer[Clause]
2065+
def formulaBuilder = ArrayBuffer[Clause]()
2066+
def addFormula(buff: FormulaBuilder, f: Formula): Unit = buff ++= f
2067+
def toFormula(buff: FormulaBuilder): Formula = buff.toArray
2068+
2069+
// CNF: a formula is a conjunction of clauses
2070+
type Formula = Array[Clause]
20492071
def formula(c: Clause*): Formula = c.toArray
2050-
def andFormula(a: Formula, b: Formula): Formula = a ++ b
20512072

2073+
type Clause = Set[Lit]
20522074
// a clause is a disjunction of distinct literals
2053-
type Clause = Set[Lit]
20542075
def clause(l: Lit*): Clause = l.toSet
2055-
private def merge(a: Clause, b: Clause) = a ++ b
20562076

20572077
type Lit
20582078
def Lit(sym: Sym, pos: Boolean = true): Lit
20592079

2080+
def andFormula(a: Formula, b: Formula): Formula = a ++ b
2081+
def simplifyFormula(a: Formula): Formula = a.distinct
2082+
2083+
private def merge(a: Clause, b: Clause) = a ++ b
2084+
20602085
// throws an AnalysisBudget.Exception when the prop results in a CNF that's too big
20612086
// TODO: be smarter/more efficient about this (http://lara.epfl.ch/w/sav09:tseitin_s_encoding)
20622087
def eqFreePropToSolvable(p: Prop): Formula = {
@@ -2621,23 +2646,22 @@ trait PatternMatching extends Transform with TypingTransformers with ast.TreeDSL
26212646

26222647
val propsCasesOk = testCasesOk map (t => symbolicCase(t, modelNull = true))
26232648
val propsCasesFail = testCasesFail map (t => Not(symbolicCase(t, modelNull = true)))
2624-
val (eqAxiomsFail, symbolicCasesFail) = removeVarEq(propsCasesFail, modelNull = true)
2625-
val (eqAxiomsOk, symbolicCasesOk) = removeVarEq(propsCasesOk, modelNull = true)
26262649

26272650
try {
2628-
// most of the time eqAxiomsFail == eqAxiomsOk, but the different approximations might cause different variables to disapper in general
2629-
val eqAxiomsCNF =
2630-
if (eqAxiomsFail == eqAxiomsOk) eqFreePropToSolvable(eqAxiomsFail)
2631-
else eqFreePropToSolvable(And(eqAxiomsFail, eqAxiomsOk))
2651+
val (eqAxiomsFail, symbolicCasesFail) = removeVarEq(propsCasesFail, modelNull = true)
2652+
val (eqAxiomsOk, symbolicCasesOk) = removeVarEq(propsCasesOk, modelNull = true)
2653+
val eqAxioms = simplifyFormula(andFormula(eqAxiomsOk, eqAxiomsFail)) // I'm pretty sure eqAxiomsOk == eqAxiomsFail, but not 100% sure.
2654+
2655+
val prefix = formulaBuilder
2656+
addFormula(prefix, eqAxioms)
26322657

2633-
var prefix = eqAxiomsCNF
26342658
var prefixRest = symbolicCasesFail
26352659
var current = symbolicCasesOk
26362660
var reachable = true
26372661
var caseIndex = 0
26382662

26392663
patmatDebug("reachability, vars:\n"+ ((propsCasesFail flatMap gatherVariables).distinct map (_.describe) mkString ("\n")))
2640-
patmatDebug("equality axioms:\n"+ cnfString(eqAxiomsCNF))
2664+
patmatDebug("equality axioms:\n"+ cnfString(eqAxiomsOk))
26412665

26422666
// invariant (prefixRest.length == current.length) && (prefix.reverse ++ prefixRest == symbolicCasesFail)
26432667
// termination: prefixRest.length decreases by 1
@@ -2647,11 +2671,11 @@ trait PatternMatching extends Transform with TypingTransformers with ast.TreeDSL
26472671
prefixRest = prefixRest.tail
26482672
if (prefixRest.isEmpty) reachable = true
26492673
else {
2650-
prefix = andFormula(eqFreePropToSolvable(prefHead), prefix)
2674+
addFormula(prefix, prefHead)
26512675
current = current.tail
2652-
val model = findModelFor(andFormula(eqFreePropToSolvable(current.head), prefix))
2676+
val model = findModelFor(andFormula(current.head, toFormula(prefix)))
26532677

2654-
// patmatDebug("trying to reach:\n"+ cnfString(eqFreePropToSolvable(current.head)) +"\nunder prefix:\n"+ cnfString(prefix))
2678+
// patmatDebug("trying to reach:\n"+ cnfString(current.head) +"\nunder prefix:\n"+ cnfString(prefix))
26552679
// if (NoModel ne model) patmatDebug("reached: "+ modelString(model))
26562680

26572681
reachable = NoModel ne model

‎test/files/pos/t6942.flags

Lines changed: 1 addition & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1 @@
1+
-Xfatal-warnings

‎test/files/pos/t6942/Bar.java

Lines changed: 235 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,235 @@
1+
package foo;
2+
3+
public enum Bar {
4+
ANGUILLA /*("US")*/,
5+
ANTIGUA_AND_BARBUDA /*("US")*/,
6+
ARGENTINA /*("US")*/,
7+
ARUBA /*("US")*/,
8+
BAHAMAS /*("US")*/,
9+
BARBADOS /*("US")*/,
10+
BELIZE /*("US")*/,
11+
BERMUDA /*("US")*/,
12+
BOLIVIA /*("US")*/,
13+
BRAZIL /*("US")*/,
14+
BRITISH_VIRGIN_ISLANDS /*("US")*/,
15+
CANADA /*("US")*/,
16+
CAYMAN_ISLANDS /*("US")*/,
17+
CHILE /*("US")*/,
18+
CHRISTMAS_ISLANDS /*("US")*/,
19+
COCOS /*("US")*/,
20+
COLOMBIA /*("US")*/,
21+
COSTA_RICA /*("US")*/,
22+
CUBA /*("US")*/,
23+
DOMINICA /*("US")*/,
24+
DOMINICAN_REPUBLIC /*("US")*/,
25+
ECUADOR /*("US")*/,
26+
EL_SALVADOR /*("US")*/,
27+
FALKLAND_ISLANDS /*("US")*/,
28+
GRENADA /*("US")*/,
29+
GUADALOUPE /*("US")*/,
30+
GUATEMALA /*("US")*/,
31+
HAITI /*("US")*/,
32+
HONDURAS /*("US")*/,
33+
NETHERLANDS_ANTILLES /*("US")*/,
34+
NICARAGUA /*("US")*/,
35+
PANAMA /*("US")*/,
36+
PARAGUAY /*("US")*/,
37+
PERU /*("US")*/,
38+
PUERTO_RICO /*("US")*/,
39+
JAMAICA /*("US")*/,
40+
MARTINIQUE /*("US")*/,
41+
MEXICO /*("US")*/,
42+
MONTSERRAT /*("US")*/,
43+
ST_KITTS /*("US")*/,
44+
ST_LUCIA /*("US")*/,
45+
ST_VINCENT /*("US")*/,
46+
SUPRA_NATIONAL /*("US")*/,
47+
TRINIDAD /*("US")*/,
48+
TURKS_AND_CAICOS /*("US")*/,
49+
UNITED_STATES /*("US")*/,
50+
URUGUAY /*("US")*/,
51+
VENEZUELA /*("US")*/,
52+
VIRGIN_ISLANDS /*("US")*/,
53+
54+
AUSTRALIA /*("AP")*/,
55+
BANGLADESH /*("AP")*/,
56+
BHUTAN /*("AP")*/,
57+
CAMBODIA /*("AP")*/,
58+
CHINA /*("AP")*/,
59+
COOK_ISLANDS /*("AP")*/,
60+
EAST_TIMOR /*("AP")*/,
61+
FIJI /*("AP")*/,
62+
GUAM /*("AP")*/,
63+
HONG_KONG /*("AP")*/,
64+
INDIA /*("AP")*/,
65+
INDONESIA /*("AP")*/,
66+
JAPAN /*("AP")*/,
67+
KIRIBATI /*("AP")*/,
68+
LAOS /*("AP")*/,
69+
MACAU /*("AP")*/,
70+
MALAYSIA /*("AP")*/,
71+
MICRONESIA /*("AP")*/,
72+
MONGOLIA /*("AP")*/,
73+
MYANMAR /*("AP")*/,
74+
NEPAL /*("AP")*/,
75+
NEW_CALEDONIA /*("AP")*/,
76+
NEW_ZEALAND /*("AP")*/,
77+
NORFOLK_ISLAND /*("AP")*/,
78+
NORTH_KOREA /*("AP")*/,
79+
PAKISTAN /*("AP")*/,
80+
PALAU /*("AP")*/,
81+
PAPUA_NEW_GUINEA /*("AP")*/,
82+
PHILIPPINES /*("AP")*/,
83+
PITCAIRN_ISLANDS /*("AP")*/,
84+
SAMOA /*("AP")*/,
85+
WEST_SAMOA /*("AP")*/,
86+
SINGAPORE /*("AP")*/,
87+
SOUTH_KOREA /*("AP")*/,
88+
SRI_LANKA /*("AP")*/,
89+
TAIWAN /*("AP")*/,
90+
THAILAND /*("AP")*/,
91+
TOKELAU /*("AP")*/,
92+
TONGA /*("AP")*/,
93+
TUVALU /*("AP")*/,
94+
VANUATU /*("AP")*/,
95+
VIETNAM /*("AP")*/,
96+
97+
AFGHANISTAN /*("EU")*/,
98+
ALBANIA /*("EU")*/,
99+
ALGERIA /*("EU")*/,
100+
ANDORRA /*("EU")*/,
101+
ANGOLA /*("EU")*/,
102+
ARMENIA /*("EU")*/,
103+
AUSTRIA /*("EU")*/,
104+
AZERBAIJAN /*("EU")*/,
105+
BAHRAIN /*("EU")*/,
106+
BELARUS /*("EU")*/,
107+
BELGIUM /*("EU")*/,
108+
BENIN /*("EU")*/,
109+
BOSNIA_AND_HERZEGOVINA /*("EU")*/,
110+
BOTSWANA /*("EU")*/,
111+
BOUVET_ISLAND /*("EU")*/,
112+
BRUNEI /*("EU")*/,
113+
BULGARIA /*("EU")*/,
114+
BURKINA_FASO /*("EU")*/,
115+
BURUNDI /*("EU")*/,
116+
CAMEROON /*("EU")*/,
117+
CAPE_VERDE /*("EU")*/,
118+
CHAD /*("EU")*/,
119+
COMOROS /*("EU")*/,
120+
CONGO /*("EU")*/,
121+
CROATIA /*("EU")*/,
122+
CYPRUS /*("EU")*/,
123+
CZECH_REPUBLIC /*("EU")*/,
124+
DR_CONGO /*("EU")*/,
125+
DENMARK /*("EU")*/,
126+
DJIBOUTI /*("EU")*/,
127+
EGYPT /*("EU")*/,
128+
EQUATORIAL_GUINEA /*("EU")*/,
129+
ERITREA /*("EU")*/,
130+
ESTONIA /*("EU")*/,
131+
ETHIOPIA /*("EU")*/,
132+
FAEROE_ISLANDS /*("EU")*/,
133+
FINLAND /*("EU")*/,
134+
FRANCE /*("EU")*/,
135+
FRENCH_GUIANA /*("EU")*/,
136+
GABON /*("EU")*/,
137+
GAMBIA /*("EU")*/,
138+
GEORGIA /*("EU")*/,
139+
GERMANY /*("EU")*/,
140+
GHANA /*("EU")*/,
141+
GIBRALTAR /*("EU")*/,
142+
GREAT_BRITAIN /*("EU")*/,
143+
GREECE /*("EU")*/,
144+
GREENLAND /*("EU")*/,
145+
GUINEA /*("EU")*/,
146+
GUINEA_BISSAU /*("EU")*/,
147+
GUYANA /*("EU")*/,
148+
HUNGARY /*("EU")*/,
149+
ICELAND /*("EU")*/,
150+
IRAN /*("EU")*/,
151+
IRAQ /*("EU")*/,
152+
IRELAND /*("EU")*/,
153+
ISLE_OF_MAN /*("EU")*/,
154+
ISRAEL /*("EU")*/,
155+
ITALY /*("EU")*/,
156+
IVORY_COAST /*("EU")*/,
157+
JERSEY /*("EU")*/,
158+
JORDAN /*("EU")*/,
159+
KAZAKHSTAN /*("EU")*/,
160+
KENYA /*("EU")*/,
161+
KUWAIT /*("EU")*/,
162+
KYRGYZSTAN /*("EU")*/,
163+
LATVIA /*("EU")*/,
164+
LEBANON /*("EU")*/,
165+
LESOTHO /*("EU")*/,
166+
LIBERIA /*("EU")*/,
167+
LIBYA /*("EU")*/,
168+
LIECHTENSTEIN /*("EU")*/,
169+
LITHUANIA /*("EU")*/,
170+
LUXEMBOURG /*("EU")*/,
171+
MACEDONIA /*("EU")*/,
172+
MADAGASCAR /*("EU")*/,
173+
MALAWI /*("EU")*/,
174+
MALDIVES /*("EU")*/,
175+
MALI /*("EU")*/,
176+
MALTA /*("EU")*/,
177+
MARSHALL_ISLAND /*("EU")*/,
178+
MAURITANIA /*("EU")*/,
179+
MAURITIUS /*("EU")*/,
180+
MAYOTTE /*("EU")*/,
181+
MOLDOVA /*("EU")*/,
182+
MONACO /*("EU")*/,
183+
MOROCCO /*("EU")*/,
184+
MOZAMBIQUE /*("EU")*/,
185+
NAMIBIA /*("EU")*/,
186+
NETHERLANDS /*("EU")*/,
187+
NIGER_REPUBLIC /*("EU")*/,
188+
NIGERIA /*("EU")*/,
189+
NORWAY /*("EU")*/,
190+
OMAN /*("EU")*/,
191+
PALESTINE /*("EU")*/,
192+
POLAND /*("EU")*/,
193+
PORTUGAL /*("EU")*/,
194+
QATAR /*("EU")*/,
195+
REUNION /*("EU")*/,
196+
ROMANIA /*("EU")*/,
197+
RUSSIA /*("EU")*/,
198+
RWANDA /*("EU")*/,
199+
SAN_MARINO /*("EU")*/,
200+
SAO_TOME /*("EU")*/,
201+
SAUDI_ARABIA /*("EU")*/,
202+
SENEGAL /*("EU")*/,
203+
SERBIA /*("EU")*/,
204+
SEYCHELLES /*("EU")*/,
205+
SEIRRA_LEONE /*("EU")*/,
206+
SLOVAKIA /*("EU")*/,
207+
SLOVENIA /*("EU")*/,
208+
SOMALIA /*("EU")*/,
209+
SOUTH_AFRICA /*("EU")*/,
210+
SPAIN /*("EU")*/,
211+
ST_HELENA /*("EU")*/,
212+
SUDAN /*("EU")*/,
213+
SURINAME /*("EU")*/,
214+
SVALBARD /*("EU")*/,
215+
SWAZILAND /*("EU")*/,
216+
SWEDEN /*("EU")*/,
217+
SWITZERLAND /*("EU")*/,
218+
SYRIA /*("EU")*/,
219+
TAJIKSTAN /*("EU")*/,
220+
TANZANIA /*("EU")*/,
221+
TOGO /*("EU")*/,
222+
TUNISIA /*("EU")*/,
223+
TURKEY /*("EU")*/,
224+
TURKMENISTAN /*("EU")*/,
225+
UAE /*("EU")*/,
226+
UGANDA /*("EU")*/,
227+
UKRAINE /*("EU")*/,
228+
UZBEKISTAN /*("EU")*/,
229+
VATICAN_CITY /*("EU")*/,
230+
WESTERN_SAHARA /*("EU")*/,
231+
YEMEN /*("EU")*/,
232+
ZAMBIA /*("EU")*/,
233+
ZIMBABWE /*("EU")*/;
234+
235+
}

0 commit comments

Comments
 (0)
0