Skip to content

Add a minimizing solver for smaller counter-examples

Viktor Kuncak requested to merge github/fork/SolalPirelli/sp/minimizer into scala-2.13

Created by: SolalPirelli

This is part of the Formal Verification course project from @mbovel and me, the idea is to add a "minimizing" solver that makes "smaller" counter-examples, such as ints/BVs closer to 0 and ADT constructors with fewer parameters.

Two examples from our project presentation:

def f(n: Int): Unit = {
  assert(n * n > 10)
}

With default Stainless this results in a counter-example of -1743011841, with our smt-z3-min solver it results in 0 instead (and the overflow counter-example is also far closer to 0).

sealed abstract class Thing {
  def size: Int = this match {
    case Big(a, b, c) => a + b + c
    case Small() => 0
    case Medium(a) => a
  }
}
case class Big(a: Int, b: Int, c: Int) extends Thing
case class Small() extends Thing
case class Medium(a: Int) extends Thing

def g(t: Thing): Unit = {
  assert(t.size > 10)
}

With default Stainless the output isn't stable, it will somewhat randomly be one of the three ADT constructors, with our smt-z3-min it's always Small() (and the overflow counter-examples are also minimized).

WDYT? In particular, should there be other kinds of minimization? What tests should there be, and is there an easier way to write such tests than the rather verbose one we added (the TIP format maybe)?

Merge request reports