Repair¶
Leon can repair buggy Pure Scala programs. Given a specification and an erroneous implementation for a function, Leon will localize the cause of the bug and provide an alternative solution. In the following we will give some insight into how repair works through a simple example.
An example¶
In the following code, a user has tried to implement a function that performs natural number division using only addition and subtraction. However, this snippet contains a bug:
def moddiv(a: Int, b: Int): (Int, Int) = {
require(a >= 0 && b > 0);
if (b > a) {
(1, 0) // fixme: should be (a, 0)
} else {
val (r1, r2) = moddiv(a-b, b)
(r1, r2+1)
}
} ensuring {
res => b*res._2 + res._1 == a
}
Leon can discover and repair this error. Invoking leon --repair --functions=moddiv will yield:
[ Info ] ======================= 1. Discovering tests for moddiv =======================
[ Info ] - Passing: 1
[ Info ] - Failing: 5
[ Info ] - Minimal Failing Set Size: 2
[ Info ] Finished in 836ms
[ Info ] ==================== 2. Locating/Focusing synthesis problem ====================
[ Info ] Program size : 152
[ Info ] Original body size: 30
[ Info ] Focused expr size : 3
[ Info ] Finished in 78ms
[ Info ] =============================== 3. Synthesizing ===============================
[ Info ] ⟦ a;b, ↓ moddiv(a, b) && ⊙ {(1, 0)} && a >= 0 && b > 0 && b > a ≺ ⟨ val res = x27;
[ Info ] b * res._2 + res._1 == a ⟩ x27 ⟧
[ Info ] [CEGLESS ] ⟦ a;b, ↓ moddiv(a, b) && ⊙ {(1, 0)} && a >= 0 && b > 0 && b > a ≺
[ Info ] ⟨ val res = x27; b * res._2 + res._1 == a ⟩ x27 ⟧
[ Info ] [CEGLESS ] Solved with: ⟨ true | (a, 0) ⟩...
[ Info ] Finished in 1995ms
[ Info ] Found trusted solution!
[ Info ] ============================== Repair successful: ==============================
[ Info ] --------------------------------- Solution 1: ---------------------------------
[ Info ] (a, 0)
[ Info ] ================================= In context: =================================
[ Info ] --------------------------------- Solution 1: ---------------------------------
[ Info ] def moddiv(a : Int, b : Int): (Int, Int) = {
require(a >= 0 && b > 0)
if (b > a) {
(a, 0)
} else {
val (r1, r2) = moddiv(a - b, b)
(r1, (r2 + 1))
}
} ensuring {
(res : (Int, Int)) => (b * res._2 + res._1 == a)
}
Leon has localized the error on the expression (1, 0) and provided the correct alternative (a, 0), as well as the entire repaired function (due to some implementation restrictions, the function body which Leon outputs is a little more complex than the one given above, but equivalent to it).
Repair Mechanism¶
We can break down the repair mechanism of Leon in three phases:
Test Case Generation¶
In the beginning, Leon will try to generate test cases which will help localize the error. Sample inputs are generated by an enumeration technique, and then the function under repair is executed on them. The test cases are divided in passing (those that satisfy the function specification) and failing. What we are actually interested in are the failing test cases; if none are generated, we resort to an SMT solver to discover a counterexample for the function (or possibly prove it correct).
Next, a dependency analysis is run on the discovered failing tests, and those that recursively invoke the function with another failing input are rejected.
Fault Localization¶
In the next step, Leon will try to localize the problem to the smallest possible subexpression of the function body. The idea is to run the failing test cases through the function and isolate the paths followed by some erroneous executions. In moddiv, Leon will successfully identify the expression (1, 0) as the source of the error. Repair will work even in the presence of more than one errors; however, the discovered subexpression may be larger. This is compensated for in a later stage.
Because of this approach, repair works better for programs that contain a small number of localized errors. Errors that wrap the whole body of the function will fail to be localized, and repair will fall back to generic synthesis.
Synthesis of the Repaired Expression¶
Leon then tries to synthesize an alternative expression in place of the erroneous one which satisfies the function specification. To this, it uses generic Synthesis, enhanced with a rule for similar term exploration, due to our hypothesis of small localized errors.
Verification of the synthesized solution¶
Finally, Leon will try to verify the synthesized solution. In case of failure to prove it correct (but also to disprove it), Leon will still present it as an untrusted solution.
Repairing with IO-examples¶
In the Pure Scala section, we have presented the passes construct. This construct is especially useful when it comes to repair. Look at the following example:
sealed abstract class List {
def drop(i: Int): List[T] = { (this, i) match {
case (Nil(), _) => Nil()
case (Cons(h, t), ) =>
t // FIXME should be this
case (Cons(_, t), i) =>
t.drop(i) //FIXME should be i-1
}} ensuring { res => ((this, i), res) passes {
case (Cons(_, Nil()), 42) => Nil()
case (l@Cons(_, _), 0) => l
case (Cons(a, Cons(b, Nil())), 1) => Cons(b, Nil())
case (Cons(a, Cons(b, Cons(c, Nil()))), 2) => Cons(c, Nil())
}}
}
case class Cons[T](h: T, t: List[T]) extends List[T]
case class Nil[T]() extends List[T]
In the above example, the programmer has chosen to specify drop through a list of IO-examples, describing what the function should do in the cases where the elements to drop are more than the size of the list, or 0, 1 or 2 elements are to be dropped by a list with enough elements.
Leon manages to repair this program:
...
[ Info ] Found trusted solution!
[ Info ] ============================== Repair successful: ==============================
[ Info ] --------------------------------- Solution 1: ---------------------------------
[ Info ] val scrut = ($this, i);
[ Info ] scrut match {
[ Info ] case (Nil(), _) =>
[ Info ] Nil[T]()
[ Info ] case (Cons(h, t), 0) =>
[ Info ] scrut._1
[ Info ] case (Cons(_, t), i) =>
[ Info ] t.drop(i - 1)
[ Info ] }
...