Formal Verification

Using stainless for Full Coverage Unit Test Generation

Thibaud Banderet, Liam Wachter, Shubhojyoti Nath

Goal


def isPrime(n:Int): Boolean = {
  require(n > 0)
  var r = true
  if (n <= 1) r = false
  else {
    var i:Int = 2
    (while (i < (n / 2)) {
      decreases(n-i)
      if (n % i == 0) r = false
      i += 1
    }).invariant(2 <= i && i <= n)
  }
  r
}.ensuring((res: Boolean) => res == (n > 1 && (2 until n).forall(i => n % i != 0)))


class IsPrimeTest extends FlatSpec with Matchers {
  "isPrime" should "fulfill the postcond" in {
    assert(!isPrime(1))
    assert(isPrime(5))
  }
}

Basic Block Coverage


assert(!isPrime(1))

Basic Block Coverage


assert(!isPrime(1))
assert(!isPrime(5))

Why

Unit tests for complex functions are hard to write
Execution environment can differ [EH07]
Unit tests are required for some certifications (DO-178C)
Unit test can be reused for other implementations
Can work with partial verification

How: Reaching Basic Blocks

How: Inputs

Counter example generation


[Warning ]  - Result for 'body assertion' VC for isPrime @25:12:
[Warning ] n <= 0
[Warning ] SubList.scala:25:12:  => INVALID
               assert(n != n, "BB_1")
                      ^^^^^^
[Warning ] Found counter-example:
[Warning ]   n: Int -> 1


isPrime(1)

How: Test Oracle

Ensuring Clause


def isPrime(n:Int): Boolean = {
  require(n > 0)
  var r = true
  if (n <= 1) r = false
  else {
    var i:Int = 2
    (while (i < (n / 2)) {
      decreases(n-i)
      if (n % i == 0) r = false
      i += 1
    }).invariant(2 <= i && i <= n)
  }
  r
}.ensuring((res: Boolean) => res == (n > 1 && (2 until n).forall(i => n % i != 0)))


val n = 2
assert(((res: Boolean) =>
res == (n > 1 && (2 until n).forall(i => n % i != 0)))
(isPrime(n)))

Background

assert(false)
Verification Condition (VC)
Counterexample ⇒ Witness for Reachability

Finding Counterexamples [Voi2019]

Now the question is: How do we find counterexamples for a verification condition? We find counterexamples using an SMT solver. SMT refers to satisfiability modulo theories. These are solvers for First Order Logic. We provide these solvers with formulas which are a bunch of conjuncts, so basically, like a bunch of equalities with function symbols, arithmetic, etc. They kind of look like a program, except for the fact that they have a logical semantics, and not program semantics. The difference between logical and program semantics is that functions in logic don't have a specific definition, they are arbitrarily interpreted, on the other hand, functions in program are defined by the function body. To ensure that the encoding given to the SMT solver and the program have the same semantics, we have to augument this encoding, and for this, we use blocking and unfolding techniqes.

SMT (Satisfiability Modulo Theories) solver
Automated solver for first order logic formulas
Blocking and unfolding

Blocking and Unfolding

Program


def size(list: List): BigInt = list match{
	case Cons(_,xs) => 1+size(xs)
	case Nil() => 0
}

size(list) <= 0

Blocking and Unfolding

Program


def size(list: List): BigInt = list match{
	case Cons(_,xs) => 1+size(xs)
	case Nil() => 0
}

size(list) <= 0

Counterexample: list = Cons(_,Nil())

Implementation

Stainless does tree transformations
We develop our own transformation
And place it in the pipeline

Implementation


def isPrime(n: Int): Boolean = {
  require(n > 0)
  val r: Boolean = true
  val t: (Unit, Boolean) = if (n <= 1) {
    val r: Boolean = false
    ((), r)
  } else {
    val i: Int = 2
    val t: (Unit, Int, Boolean) = if (i < n / 2) {
      isPrimeWhile(n, i, r)
    } else {
      ((), i, r)
    }
    val res: Unit = t._1
    val r: Boolean = t._3
    val i: Int = t._2
    (res, r)
  }
  val res: Unit = t._1
  val r: Boolean = t._2
  val tmp: Unit = res
  r
}


@derived(isPrime)
def isPrimeWhile(n: Int, i: Int, r: Boolean):
(Unit, Int, Boolean) = {
  require(((n > 0)): @dropConjunct )
  val r: Boolean = true
  require((!(n <= 1)): @dropConjunct )
  val i: Int = 2
  {
    require({
      val t: Boolean = if (2 <= i) {
        val t: Boolean = if (i <= n) {
          i < n / 2
        } else {
          false
        }
        val res: Boolean = t
        res
      } else {
        false
      }
      val res: Boolean = t
      res
    })
    decreases(n - i)
    val r: Boolean = r
    val i: Int = i
    val t: (Unit, Boolean) = if (n % i == 0) {
      val r: Boolean = false
      ((), r)
    } else {
      ((), r)
    }
    val res: Unit = t._1
    val r: Boolean = t._2
    val tmp: Unit = res
    val i: Int = i + 1
    val tmp: Unit = ()
    val tmp: Unit = ()
    if (i < n / 2) {
      isPrimeWhile(n, i, r)
    } else {
      ((), i, r)
    }
  } ensuring {
    (_res: (Unit, Int, Boolean)) => {
      val t: Boolean = if (2 <= _res._2) {
        val t: Boolean = if (_res._2 <= n) {
          !(_res._2 < n / 2)
        } else {
          false
        }
        val res: Boolean = t
        res
      } else {
        false
      }
      val res: Boolean = t
      res
    }
  }
}

Implementation


/**
 * Transform trees by inserting Reachability probes. s is the input tree, t is the transformed tree
 */
class ReachabilityProbeInjector(override val s: ast.Trees, override val t: ast.Trees)
                       (using val symbols: s.Symbols)
  extends transformers.ConcreteTreeTransformer(s, t) {
    override def transform(e: s.Expr): t.Expr = e match {
        // TODO add at beginning of method
        case s.MatchExpr(scrutine, cases) => t.MatchExpr(transform(scrutine), cases.map(casee => casee match {
            case s.MatchCase(pattern, optGuard, rhs) => t.MatchCase(pattern, transform(optGuard), t.ReachabilityProbe(transform(rhs)))
        }))
        case s.IfExpr(cond, _then, _else) => t.IfExpr(transform(cond), t.ReachabilityProbe(transform(_then)), t.ReachabilityProbe(transform(_else)))
        case _ => super.transform(e) // go through the other expressions and transform recursively
    }
}

Implementation


def isPrime(n: Int): Boolean = {
  require(n > 0)
  reachabilityProbe(n)
  val r: Boolean = true
  val targetBound: Boolean = n <= 1
  val t: (Unit, Boolean) = if (targetBound) {
    reachabilityProbe(n)
    val r: Boolean = false
    ((), r)
  } else {
    val i: Int = 2
    val t: (Unit, Int, Boolean) = if (i < n / 2) {
      isPrimeWhile(n, i, r)
    } else {
      ((), i, r)
    }
    val res: Unit = t._1
    val r: Boolean = t._3
    val i: Int = t._2
    (res, r)
  }
  val res: Unit = t._1
  val r: Boolean = t._2
  val tmp: Unit = res
  reachabilityProbe(n)
  r
}


@derived(isPrime)
def isPrimeWhile(n: Int, i: Int, r: Boolean):
(Unit, Int, Boolean) = {
  require(@dropConjunct @DropVCs (n > 0) &&&
  @dropConjunct @DropVCs (n ≠ n))
  val targetBound: Boolean = @DropVCs (n <= 1)
  require(@dropConjunct @DropVCs ¬targetBound)
  {
    require((2 <= i && i <= n) &&& (i < n / 2))
    decreases(n - i)
    val r: Boolean = r
    val i: Int = i
    reachabilityProbe(n)
    val targetBound: Boolean = n % i == 0
    val t: (Unit, Boolean) = if (targetBound) {
      reachabilityProbe(n)
      val r: Boolean = false
      ((), r)
    } else {
      ((), r)
    }
    val res: Unit = t._1
    val r: Boolean = t._2
    val tmp: Unit = res
    reachabilityProbe(n)
    val i: Int = i + 1
    val tmp: Unit = ()
    if (i < n / 2) {
      isPrimeWhile(n, i, r)
    } else {
      ((), i, r)
    }
  } ensuring {
    (_res: (Unit, Int, Boolean)) => {
      val r: Boolean = _res._3
      val i: Int = _res._2
      (2 <= i && i <= n) &&& ¬(i < n / 2)
    }
  }
}

Current progress

Added ReachabilityProbe expression in stainless
Added phase to insert probes in each code block
Registered phase in stainless pipeline

TODO's

Modify stainless to handle probes:

New case to handle probes
Check if that probe is reachable or not
If reachable show the input

Conclusion

Testing reachability
Automating (part of) unit testing
Plenty more progress to be done

Future scope

Testing inputs against post conditions on the fly
Actual generation of the unit tests code

Questions ?

Thanks for listening !

Bibliography

[EH2007] C. Engel and R. Hähnle, “Generating Unit Tests from Formal Proofs,” in Tests and Proofs,
Berlin, Heidelberg, 2007, pp. 169–188. doi: 10.1007/978-3-540-73770-4_10.
[Voi2019] Voirol, Nicolas Charles Yves. Verified functional programming. THESIS. EPFL, 2019.