summaryrefslogtreecommitdiff
path: root/test/files/run
Commit message (Collapse)AuthorAgeFilesLines
* Merge pull request #3963 from erikerlandson/si-8835-prLukas Rytz2014-11-112-6/+39
|\ | | | | SI-8835 Fix implementation of Iterator drop to remove quadratic behavior
| * SI-8835 Fix implementation of Iterator drop to remove quadratic behaviorErik Erlandson2014-10-212-6/+39
| |
* | Merge pull request #4120 from retronym/ticket/5665Lukas Rytz2014-11-101-0/+13
|\ \ | | | | | | SI-5665 Test case for fixed private[this], trait crasher
| * | SI-5665 Test case for fixed private[this], trait crasherJason Zaugg2014-11-091-0/+13
| | | | | | | | | | | | Fixed in SI-5508 / cca4d51db.
* | | Merge pull request #4110 from lrytz/t8960-delambdafyJason Zaugg2014-11-101-1/+7
|\ \ \ | | | | | | | | Make t8960 pass under delambdafy:method
| * | | Make t8960 pass under delambdafy:methodLukas Rytz2014-11-071-1/+7
| |/ / | | | | | | | | | | | | | | | | | | When using delambdafy:method, anonymous function classes are not currently specialized, as noted here: https://github.com/scala/scala/blob/f08e96571479552b103b15cc2d40ea5454999546/src/compiler/scala/tools/nsc/transform/Delambdafy.scala#L26
* | | Merge pull request #4109 from retronym/ticket/1994Lukas Rytz2014-11-101-0/+20
|\ \ \ | | | | | | | | SI-1994 Test case for fixed overriding problem
| * | | SI-1994 Test case for fixed overriding problemJason Zaugg2014-11-071-0/+20
| | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | The test case passes since Scala 2.9.2. Prior, it failed with: ~/scala/2.9.1/bin/scalac sandbox/t1994.scala sandbox/t1994.scala:9: error: method y overrides nothing override def y = 1 ^ one error found
* | | | Merge pull request #4101 from adriaanm/sam-exLukas Rytz2014-11-103-0/+10
|\ \ \ \ | | | | | | | | | | [sammy] eta-expansion, overloading, existentials
| * | | | [sammy] support repeated paramsAdriaan Moors2014-11-073-0/+10
| | | | | | | | | | | | | | | | | | | | | | | | | Generate correct trees to refer to repeated params using `gen.paramToArg`. Based on retronym's review feedback.
* | | | | Merge pull request #4095 from retronym/ticket/8933Lukas Rytz2014-11-106-0/+44
|\ \ \ \ \ | |_|_|/ / |/| | | | Fix problems in Symbol Literal static caching
| * | | | SI-7974 Fix over-eager optimization of Symbol literalsJason Zaugg2014-11-071-0/+14
| | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | A classic mistake of discarding a non-trivial qualifier. We actually should have fixed this before merging #3149, as it was raised in review, but I suppose we got too caught up in the difficulty of resolving the right overload of `Symbol_apply` that we forgot.
| * | | | SI-8933 Disable static Symbol literal cache in traitsJason Zaugg2014-11-075-0/+30
| | |/ / | |/| | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | In Scala 2.8.2, an optimization was added to create a static cache for Symbol literals (ie, the results of `Symbol.apply("foo"))`. This saves the map lookup on the second pass through code. This actually was broken somewhere during the Scala 2.10 series, after the addition of an overloaded `apply` method to `Symbol`. The cache synthesis code was made aware of the overload and brought back to working condition recently, in #3149. However, this has uncovered a latent bug when the Symbol literals are defined with traits. One of the enclosed tests failed with: jvm > t8933b-run.log java.lang.IllegalAccessError: tried to access field MotherClass.symbol$1 from class MixinWithSymbol$class at MixinWithSymbol$class.symbolFromTrait(A.scala:3) at MotherClass.symbolFromTrait(Test.scala:1) This commit simply disables the optimization if we are in a trait. Alternative fixes might be: a) make the static Symbol cache field public / b) "mixin" the static symbol cache. Neither of these seem worth the effort and risk for an already fairly situational optimization. Here's how the optimization looks in a class: % cat sandbox/test.scala; qscalac sandbox/test.scala && echo ":javap C" | qscala; class C { 'a; 'b } Welcome to Scala version 2.11.5-20141106-145558-aa558dce6d (Java HotSpot(TM) 64-Bit Server VM, Java 1.8.0_20). Type in expressions to have them evaluated. Type :help for more information. scala> :javap C Size 722 bytes MD5 checksum 6bb00189166917254e8d40499ee7c887 Compiled from "test.scala" public class C { public static {}; descriptor: ()V flags: ACC_PUBLIC, ACC_STATIC Code: stack=2, locals=0, args_size=0 0: getstatic #16 // Field scala/Symbol$.MODULE$:Lscala/Symbol$; 3: ldc #18 // String a 5: invokevirtual #22 // Method scala/Symbol$.apply:(Ljava/lang/String;)Lscala/Symbol; 8: putstatic #26 // Field symbol$1:Lscala/Symbol; 11: getstatic #16 // Field scala/Symbol$.MODULE$:Lscala/Symbol$; 14: ldc #28 // String b 16: invokevirtual #22 // Method scala/Symbol$.apply:(Ljava/lang/String;)Lscala/Symbol; 19: putstatic #31 // Field symbol$2:Lscala/Symbol; 22: return public C(); descriptor: ()V flags: ACC_PUBLIC Code: stack=1, locals=1, args_size=1 0: aload_0 1: invokespecial #34 // Method java/lang/Object."<init>":()V 4: getstatic #26 // Field symbol$1:Lscala/Symbol; 7: pop 8: getstatic #31 // Field symbol$2:Lscala/Symbol; 11: pop 12: return } fixup
* | | | Merge pull request #4047 from lrytz/delambda-method-testsLukas Rytz2014-11-075-3/+14
|\ \ \ \ | | | | | | | | | | Fix tests under -Ydelambdafy:method
| * | | | Ensure delambafy:inline for anonymous function class javap testLukas Rytz2014-10-102-1/+5
| | | | | | | | | | | | | | | | | | | | https://issues.scala-lang.org/browse/SI-8898
| * | | | Ensure closure elimination test runs under -Ydelambdafy:inlineLukas Rytz2014-10-101-1/+1
| | | | |
| * | | | Fix t8549 under -Ydelambdafy:methodLukas Rytz2014-10-101-1/+4
| | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | the structure of Option.class generated by delambdafy:method is slightly different. For example, lambdas declared within Option are not emitted as nested classes, so under delambdafy:method there's no inner class entry for anonfun classes. The test failed because serializing a ClassTag involves serializing an Option. Option did not have a `@SerialVersionUID`, and the classfile generated by delambdafy:method has a different value. The annotation is required on the parent class (Option) as well as the subclasses (Some / None). De-serializing a Some will fail if Option has a different SerialVersionUID. Relates to SI-8576. We should probably have more SVUID annotations in the library.
| * | | | Update check files for -Ydelambdafy:methodLukas Rytz2014-10-101-0/+4
| | | | | | | | | | | | | | | | | | | | Should have been done in 63207e1.
* | | | | Merge pull request #4080 from gourlaysama/wip/t8931-redundant-interfaces-2Jason Zaugg2014-11-072-0/+16
|\ \ \ \ \ | | | | | | | | | | | | SI-8931 make generic signature consistent with interface list in classfiles
| * | | | | SI-8931 make generic signature consistent with interface list in classfilesAntoine Gourlay2014-11-052-0/+16
| | |_|_|/ | |/| | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | An optimization was introduced in 7a99c03 (SI-5278) to remove redundant interfaces from the list of implemented interfaces in the bytecode. However the same change was not propagated to the generic signature of a class, which also contains a list of direct parent classes and interfaces. The JVM does not check the well-formedness of signatures at class loading or linking (see ยง4.3.4 of jdk7 jvms), but other tools might assume the number of implemented interfaces is the same whether one asked for generic or erased interfaces. It doesn't break reflection so nobody complained, but it does show: scala> val c = classOf[Tuple1[String]] c: Class[(String,)] = class scala.Tuple1 scala> c.getInterfaces // Product is gone res0: Array[Class[_]] = Array(interface scala.Product1, interface scala.Serializable) scala> c.getGenericInterfaces // Product is back! res1: Array[java.lang.reflect.Type] = Array(scala.Product1<T1>, interface scala.Product, interface scala.Serializable) This moves the optimization to erasure, for use in emitting the generic signature, and the backend calls into it later for the list of interfaces.
* | | | | Merge pull request #4096 from retronym/ticket/7019Jason Zaugg2014-11-071-0/+10
|\ \ \ \ \ | |_|_|/ / |/| | | | SI-7019 Fix crasher with private[this] extension methods
| * | | | SI-7019 Fix crasher with private[this] extension methodsJason Zaugg2014-11-061-0/+10
| | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | When we move the body of value class methods to the corresponding extension method, we typecheck a forward method that remains in the class. In order to allow access, this commit weakens the access of `private[local]` extension methods to `private`.
* | | | | Merge pull request #4093 from lrytz/t8960Lukas Rytz2014-11-065-5/+71
|\ \ \ \ \ | |/ / / / |/| | | | SI-8960 Bring back the SerialVersionUID to anonymous function classes
| * | | | SI-8960 Bring back the SerialVersionUID to anonymous function classesLukas Rytz2014-11-055-5/+71
| | |_|/ | |/| | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | In PR #1673 / 4267444, the annotation `SerialVersionId` was changed from a `StaticAnnotation` to `ClassFileAnnotation` in order to enforce annotation arguments to be constants. That was 2.11.0. The ID value in the AnnotationInfo moved from `args` to `assocs`, but the backend was not adjusted. This was fixed in PR #3711 / ecbc9d0 for 2.11.1. Unfortunately, the synthetic AnnotationInfo that is added to anonymous function classes still used the old constructor (`args` instead of `assocs`), so extracting the value failed, and no field was added to the classfile.
* | | | Merge pull request #4069 from som-snytt/issue/8898Lukas Rytz2014-11-052-0/+27
|\ \ \ \ | | | | | | | | | | SI-8898 javap -fun under new style lambdas
| * | | | SI-8898 javap -fun under new style lambdasSom Snytt2014-11-042-0/+27
| | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | To support both -Ydelambdafy strategies, look for both inline (anonfun) and method (lambda) closure classes. For method (lambda) style, use the anonfun method that is invoked by the accessor. Also, the output of javap must be captured eagerly for filtering for the current target method. If the user asks for a module, e.g., `Foo$`, don't yield results for companion class, but for `Foo`, do yield companion module results. Just because.
* | | | | Merge pull request #4017 from lrytz/t6541Lukas Rytz2014-11-055-0/+113
|\ \ \ \ \ | |_|/ / / |/| | | | SI-6541 valid wildcard existentials for case-module-unapply
| * | | | SI-6541 valid wildcard existentials for case-module-unapplyLukas Rytz2014-11-053-0/+45
| | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | Instead of letting the compiler infer the return type of case module unapply methods, provide them explicitly. This is enabled only under -Xsource:2.12, because the change is not source compatible.
| * | | | Fix default value for ScalaVersionSettingLukas Rytz2014-11-042-0/+68
| | |/ / | |/| | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | The default value was NoScalaVersion before, because tryToSet (where the default was supposed to be set) is not called at all if the option is not specified. The initial value of Xmigration is set to NoScalaVersion (which it was before, the AnyScalaVersion argument was ignored). AnyScalaVersion would be wrong, it would give a warning in `Map(1 -> "eis").values` if the option was not specified. See tests.
* | | | Merge pull request #4036 from retronym/topic/opt-tail-callsJason Zaugg2014-11-042-0/+55
|\ \ \ \ | | | | | | | | | | SI-8893 Restore linear perf in TailCalls with nested matches
| * | | | SI-8893 Test tailcall transform for mix of tail/non-tail recursionJason Zaugg2014-11-031-0/+15
| | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | Another excellent test suggestion by Dear Reviewer. After tail calls, the transform results in: ``` def tick(i: Int): Unit = { <synthetic> val _$this: Test.type = Test.this; _tick(_$this: Test.type, i: Int){ if (i.==(0)) () else if (i.==(42)) { Test.this.tick(0); _tick(Test.this, i.-(1).asInstanceOf[Int]()) } else _tick(Test.this, i.-(1).asInstanceOf[Int]()).asInstanceOf[Unit]() } }; ``` We test this by mostly exercising the tail-recursive code path with a level of recursion that would overflow the stack if we weren't using jumps.
| * | | | SI-8893 Test case to show that tailrec continues to workJason Zaugg2014-11-021-0/+40
| | |/ / | |/| | | | | | | | | | | | | | | | | | | | | | | | | | As suggested during code review, this test checks that the tailcalls phase recurses appropriately below a method that doesn and does not itself tail call. The test case is based on the pattern of code that to trigger super-linear performance in this transform.
* | | | Merge pull request #4063 from som-snytt/issue/direct-showdef-testJason Zaugg2014-11-042-36/+24
|\ \ \ \ | | | | | | | | | | Make global-showdef a DirectTest
| * | | | Reduce compiles for global-showdef testSom Snytt2014-10-282-7/+9
| | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | You can only show one class or object at a time, but we can show one of each to reduce the compilations for this test. It seems the original issue happened because the test started to create class files after SI-8217. So, also stop compile after typer, because why stress the kitteh.
| * | | | Make global-showdef a DirectTestSom Snytt2014-10-281-32/+18
| | |/ / | |/| | | | | | | | | | | | | | | | | | | | | | | | | | | | | | The test test/files/run/global-showdef.scala was outputting to the cwd instead of the test output dir. Good behavior is now inherited from DirectTest. Test frameworks, of any ilk or capability, rock.
* / | | SI-4950 Add tests, looks like it has been fixed earlierSimon Ochsenreither2014-10-232-0/+21
|/ / /
* | | Merge pull request #4048 from lrytz/t8899Grzegorz Kossakowski2014-10-201-1/+1
|\ \ \ | | | | | | | | [nomerge] SI-8899 Revert "SI-8627 make Stream.filterNot non-eager"
| * | | [nomerge] SI-8899 Revert "SI-8627 make Stream.filterNot non-eager"Lukas Rytz2014-10-121-1/+1
| |/ / | | | | | | | | | | | | | | | | | | | | | | | | This reverts commit 9276a1205f74fdec74206209712831913e93f359. The change is not binary compatible, See discussion on SI-8899. Making filterImpl non-private changes its call-sites (within TraversableLike) from INVOKESTATIC to INVOKEINTERFACE. Subclasses of TraversableLike compiled before this change don't have a mixin for filterImpl.
* / / SI-8907 Don't force symbol info in isModuleNotMethodLukas Rytz2014-10-151-0/+39
|/ / | | | | | | | | | | | | | | | | | | | | | | | | | | Test case by Jason. RefChecks adds the lateMETHOD flag lazily in its info transformer. This means that forcing the `sym.info` may change the value of `sym.isMethod`. 0ccdb151f introduced a check to force the info in isModuleNotMethod, but it turns out this leads to errors on stub symbols (SI-8907). The responsibility to force info is transferred to callers, which is the case for other operations on symbols, too.
* | SI-4788/SI-5948 Respect RetentionPolicy of Java annotationsSimon Ochsenreither2014-10-0718-0/+132
| | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | Note that I removed the check to ignore @deprecated: - @deprecated extends StaticAnnotation, so they aren't supposed to show up in the RuntimeInvisibleAnnotation attribute anyway, and the earlier check for "extends ClassfileAnnotationClass" makes this check superflous anyway. - Otherwise, if @deprecated was extending ClassfileAnnotationClass it would seem inconsistent that we don't emit @deprecated, but would do so for @deprecatedOverriding, @deprecatedInheritance, etc. Anyway, due to ClassfileAnnotation not working in Scala, and the additional check which only allows Java-defined annotations, this is pretty pointless from every perspective.
* | Merge pull request #4030 from som-snytt/issue/8843Grzegorz Kossakowski2014-10-071-0/+33
|\ \ | | | | | | SI-8843 AbsFileCL acts like a CL
| * | SI-8843 AbsFileCL acts like a CLSom Snytt2014-10-061-0/+33
| | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | Let the AbstractFileClassLoader override just the usual suspects. Normal delegation behavior should ensue. That's instead of overriding `getResourceAsStream`, which was intended that "The repl classloader now works more like you'd expect a classloader to." (Workaround for "Don't know how to construct an URL for something which exists only in memory.") Also override `findResources` so that `getResources` does the obvious thing, namely, return one iff `getResource` does. The translating class loader for REPL only special-cases `foo.class`: as a fallback, take `foo` as `$line42.$read$something$foo` and try that class file. That's the use case for "works like you'd expect it to." There was a previous fix to ensure `getResource` doesn't take a class name. The convenience behavior, that `classBytes` takes either a class name or a resource path ending in ".class", has been promoted to `ScalaClassLoader`.
* | | Merge pull request #3986 from som-snytt/issue/6502-no-cpGrzegorz Kossakowski2014-10-071-1/+1
|\ \ \ | | | | | | | | SI-6502 Repl reset/replay take settings args
| * | | SI-6502 Repl reset/replay take settings argsSom Snytt2014-09-221-1/+1
| | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | The reset and replay commands take arbitrary command line args. When settings args are supplied, the compiler is recreated. For uniformity, the settings command performs only the usual arg parsing: use -flag:true instead of +flag, and clearing a setting is promoted to the command line, so that -Xlint: is not an error but clears the flags. ``` scala> maqicode.Test main null <console>:8: error: not found: value maqicode maqicode.Test main null ^ scala> :reset -classpath/a target/scala-2.11/sample_2.11-1.0.jar Resetting interpreter state. Forgetting all expression results and named terms: $intp scala> maqicode.Test main null Hello, world. scala> val i = 42 i: Int = 42 scala> s"$i is the loneliest numbah." res1: String = 42 is the loneliest numbah. scala> :replay -classpath "" Replaying: maqicode.Test main null Hello, world. Replaying: val i = 42 i: Int = 42 Replaying: s"$i is the loneliest numbah." res1: String = 42 is the loneliest numbah. scala> :replay -classpath/a "" Replaying: maqicode.Test main null <console>:8: error: not found: value maqicode maqicode.Test main null ^ Replaying: val i = 42 i: Int = 42 Replaying: s"$i is the loneliest numbah." res1: String = 42 is the loneliest numbah. ``` Clearing a clearable setting: ``` scala> :reset -Xlint:missing-interpolator Resetting interpreter state. scala> { val i = 42 ; "$i is the loneliest numbah." } <console>:8: warning: possible missing interpolator: detected interpolated identifier `$i` { val i = 42 ; "$i is the loneliest numbah." } ^ res0: String = $i is the loneliest numbah. scala> :reset -Xlint: Resetting interpreter state. Forgetting this session history: { val i = 42 ; "$i is the loneliest numbah." } scala> { val i = 42 ; "$i is the loneliest numbah." } res0: String = $i is the loneliest numbah. ```
* | | | Merge pull request #4016 from lrytz/t8731Grzegorz Kossakowski2014-10-073-8/+8
|\ \ \ \ | | | | | | | | | | SI-8731 warning if @switch is ignored
| * | | | SI-8731 warning if @switch is ignoredLukas Rytz2014-10-063-8/+8
| | |_|/ | |/| | | | | | | | | | | | | | For matches with two or fewer cases, @switch is ignored. This should not happen silently.
* | | | Merge pull request #4033 from retronym/ticket/8888Lukas Rytz2014-10-072-0/+13
|\ \ \ \ | | | | | | | | | | SI-8888 Avoid ClassFormatError under -Ydelambdafy:method
| * | | | SI-8888 Avoid ClassFormatError under -Ydelambdafy:methodJason Zaugg2014-10-072-0/+13
| | |_|/ | |/| | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | The pattern matcher phase (conceivably, among others) can generate code that binds local `Ident`s symbolically, rather than according to the lexical scope. This means that a lambda can capture more than one local of the same name. In the enclosed test case, this ends up creating the following tree after delambdafy [[syntax trees at end of delambdafy]] // delambday-patmat-path-dep.scala matchEnd4({ case <synthetic> val x1: Object = (x2: Object); case5(){ if (x1.$isInstanceOf[C]()) { <synthetic> val x2#19598: C = (x1.$asInstanceOf[C](): C); matchEnd4({ { (new resume$1(x2#19598, x2#19639): runtime.AbstractFunction0) }; scala.runtime.BoxedUnit.UNIT }) } else case6() }; ... }) ... <synthetic> class resume$1 extends AbstractFunction0 { <synthetic> var x2: C = null; <synthetic> var x2: C = null; ... } After this commit, the var members of `resume$1` are given fresh names, rather than directly using the name of the captured var: <synthetic> var x2$3: C = null; <synthetic> var x2$4: C = null;
* | | | Merge pull request #3954 from gbasler/ticket/7746-2.11Grzegorz Kossakowski2014-10-062-0/+2
|\ \ \ \ | | | | | | | | | | SI-7746 fix unspecifc non-exhaustiveness warnings and non-determinism in pattern matcher (2.11)
| * | | | SI-7746 patmat: fix non-determinism, infeasible counter examplesGerard Basler2014-10-052-0/+2
| | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | 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.
generated by cgit v1.2.3 (git 2.39.1) at 2024-07-13 18:29:48 +0000