Skip to content

Commit

Permalink
Remove slow/fast discrimination for benchmarks
Browse files Browse the repository at this point in the history
  • Loading branch information
romac committed Jan 29, 2020
1 parent 37922a6 commit b287a92
Show file tree
Hide file tree
Showing 5 changed files with 4 additions and 147 deletions.
2 changes: 1 addition & 1 deletion .larabot.conf
Original file line number Diff line number Diff line change
Expand Up @@ -6,7 +6,7 @@ commands = [
nightly {
commands = [
"sbt -batch -Dparallel=5 test"
"bash bin/slow-tests.sh"
"sbt -batch -Dparallel=5 it:test"
"bash bin/external-tests.sh"
"sbt -batch scripted"
]
Expand Down
91 changes: 0 additions & 91 deletions bin/slow-tests.sh

This file was deleted.

18 changes: 0 additions & 18 deletions frontends/common/src/it/scala/stainless/SlowTests.scala

This file was deleted.

Original file line number Diff line number Diff line change
Expand Up @@ -27,33 +27,10 @@ trait ComponentTestSuite extends inox.TestSuite with inox.ResourceUtils with Inp
"solvr=" + options.findOptionOrDefault(inox.optSelectedSolvers).head + " " +
"lucky=" + options.findOptionOrDefault(inox.solvers.unrolling.optFeelingLucky) + " " +
"check=" + options.findOptionOrDefault(inox.solvers.optCheckModels) + " "
"type-checker=" + options.findOptionOrDefault(optTypeChecker)
"type-checker=" + options.findOptionOrDefault(verification.optTypeChecker)
}

protected val slowBenchmarks = Set(
"imperative/valid/NestedFunParamsMutation2",

"termination/valid/ConstantPropagation",
"termination/valid/NNFSimple",

"verification/invalid/BadConcRope",
"verification/invalid/Nested15",
"verification/invalid/PartialSplit",
"verification/valid/AmortizedQueue",
"verification/valid/BigIntRing",
"verification/valid/BitsTricksSlow",
"verification/valid/ConcRope",
"verification/valid/ConcTree",
"verification/valid/CovariantList",
"verification/valid/InnerClasses4",
"verification/valid/SuperCall4",
"verification/valid/TransitiveQuantification",
)

protected def filter(ctx: inox.Context, name: String): FilterStatus = name match {
case name if SlowTests.disabled && slowBenchmarks.contains(name) => Skip
case name => Test
}
protected def filter(ctx: inox.Context, name: String): FilterStatus = Test

def testAll(dir: String, recursive: Boolean = false)(block: (component.Analysis, inox.Reporter) => Unit): Unit = {
require(dir != null, "Function testAll must be called with a non-null directory string")
Expand Down
13 changes: 1 addition & 12 deletions frontends/scalac/src/it/scala/stainless/LibrarySuite.scala
Original file line number Diff line number Diff line change
Expand Up @@ -21,19 +21,8 @@ abstract class AbstractLibrarySuite(opts: Seq[inox.OptionValue[_]]) extends FunS
case id => id.name
}

protected def isSlow(id: Identifier): Boolean = {
symbolName(id).startsWith("stainless.collection.ConcRope")
}

protected def keepDerived(tr: ast.Trees)(flag: tr.Flag): Boolean = flag match {
case tr.Derived(id) => !isSlow(id)
case _ => true
}

protected def keep(tr: ast.Trees)(fd: tr.FunDef): Boolean = fd match {
case fd if fd.flags exists (_.name == "unchecked") => false
case fd if !SlowTests.enabled && isSlow(fd.id) => false
case fd if !fd.flags.forall(keepDerived(tr)) => false
case fd if fd.flags.exists(_.name == "unchecked") => false
case fd => true
}

Expand Down

0 comments on commit b287a92

Please sign in to comment.