| Commit message (Collapse) | Author | Age | Files | Lines |
|---|
| |
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
| |
Fixes non-determinism within the DPLL algorithm and disallows
infeasible counter examples directly in the formula.
The function to compute all solutions was flawed and thus only
returned a subset of the solutions. The algorithm would stop too soon
and thus depending on the ordering of the symbols return more or less
solutions. I also added printing a warning when the search was stopped
because the max recursion depth was reached. This is very useful as an
explanation of spuriously failing regression tests, since less counter
examples might be reported. In such a case the recursion depth should
be set to infinite by adding `-Ypatmat-exhaust-depth off`.
The mapping of the solutions of the DPLL algorithm to counter examples
has been adapted to take the additional solutions from the
solver into account:
Consider for example `t8430.scala`:
```Scala
sealed trait CL3Literal
case object IntLit extends CL3Literal
case object CharLit extends CL3Literal
case object BooleanLit extends CL3Literal
case object UnitLit extends CL3Literal
sealed trait Tree
case class LetL(value: CL3Literal) extends Tree
case object LetP extends Tree
case object LetC extends Tree
case object LetF extends Tree
object Test {
(tree: Tree) => tree match {case LetL(CharLit) => ??? }
}
```
This test contains 2 domains, `IntLit, CharLit, ...` and `LetL, LetP, ...`,
the corresponding formula to check exhaustivity looks like:
```
V1=LetC.type#13 \/ V1=LetF.type#14 \/ V1=LetL#11 \/ V1=LetP.type#15 /\
V2=BooleanLit.type#16 \/ V2=CharLit#12 \/ V2=IntLit.type#17 \/ V2=UnitLit.type#18 /\
-V1=LetL#11 \/ -V2=CharLit#12 \/ \/
```
The first two lines assign a value of the domain to the scrutinee (and
the correponding member in case of `LetL`) and prohibit the counter
example `LetL(CharLit)` since it's covered by the pattern match. The
used Boolean encoding allows that scrutinee `V1` can be equal to
`LetC` and `LetF` at the same time and thus, during enumeration of all
possible solutions of the formula, such a solution will be found,
since only one literal needs to be set to true, to satisfy that
clause. That means, if at least one of the literals of such a clause
was in the `unassigned` list of the DPLL procedure, we will get
solutions where the scrutinee is equal to more than one element of the
domain.
A remedy would be to add constraints that forbid both literals
to be true at the same time. His is infeasible for big domains (see
`pos/t8531.scala`), since we would have to add a quadratic number of
clauses (one clause for each pair in the domain). A much simpler
solution is to just filter the invalid results. Since both values for
`unassigned` literals are explored, we will eventually find a valid
counter example.
|
| |
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
| |
Some scalac output is on stderr, and it's useful to see that
in the log file, especially for debugging.
Adds a line filter for logs, specified as "filter: pattern"
in the test source.
Backslashes are made forward only when detected as paths.
Test alignments:
Deprecations which do not pertain to the system under test
are corrected in the obvious way.
When testing deprecated API, suppress warnings by deprecating
the Test object.
Check files are updated with useful true warnings, instead of
running under -nowarn.
Language feature imports as required, instead of running under -language.
Language feature not required, such as casual use of postfix.
Heed useful warning.
Ignore broken warnings. (Rarely, -nowarn.)
Inliner warnings pop up under -optimise only, so for now, just
filter them out where they occur.
Debug output from the test required an update.
|
| |
|
|
|
|
|
| |
some tests (unreachability, exhaustivity, @switch annotation checking) are still run under -Xoldpatmat,
but that will change before we go into RC mode (then the test/ partest of this commit will be reverted)
removed irrelevant dependency on patmat
|
|
|
TreeMakers (esp. CondTreeMakers) are approximated by hash-cons'ed Conds
sharing is detected for prefixes of Conds, and shared conditions are only tested once
their results are stored, and repeated tests branch on the last shared condition,
reusing the results from the first time they were checked
a Test is 1-to-1 with a TreeMaker, but may share its Cond
TODO: clean separation of the two translation strategies:
- naive flatMap/orElse (for virtualization)
- less-naive if-then-else (with CSE etc coming)
sharing trees caused wrong bytecode to be emitted (verifyerror)
tentative explanation:
"because lambdalift uses mutable state to track which variables have been captured
if you refer to the same variable with the same tree twice
it'll get confused"
Sent at 8:27 PM on Thursday
>> grzegorz.kossakowski: so we found a bug in jvm
according to http://java.sun.com/docs/books/jvms/second_edition/html/Instructions2.doc2.html
checkcast should throw a classcastexception
becuase it's a shorthand for if !(x instanceof T) throw ClassCastExcpt
but jvm decided to throw verifyerror
and yeah, the check is wrong
if jvm was not throwing verifyerror it would throw classcast exception
saying that ObjectRef cannot be casted to $colon$colon
...
>> me:
so now where does it come from?
since a ref is involved, i thought LambdaLift
>> grzegorz.kossakowski: yup
or now
I don't think lambalift introduces that kind of low-level casts
but I might be wrong
btw. it's interesting that it unpacks stuff from objectref twice
in your code
and in one place checkcast is correct
and in another is wrong
Sent at 9:33 PM on Thursday
>> grzegorz.kossakowski: also, since it's a verifyerror
I think genjvm should have an assertion
>> grzegorz.kossakowski:
193: getfield #54; //Field scala/runtime/ObjectRef.elem:Ljava/lang/Object;
196: checkcast #8; //class scala/runtime/ObjectRef
199: invokevirtual #95; //Method scala/collection/immutable/$colon$colon.tl$1:()Lscala/collection/immutable/List;
it's this
see
you have checkcast for ObjectRef
and then on that value, you try to call tl() method from List
Sent at 9:56 PM on Thursday
>> me: fixed
sharing trees is bad
very bad
because lambdalift uses mutable state to track which variables have been captured
if you refer to the same variable with the same tree twice
it'll get confused
|
