Repair

doc/repair.rst

@@ -2,3 +2,209 @@
 
 Repair
 ======
+
+Leon can repair buggy :ref:`Pure Scala <purescala>` 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:
+
+.. code-block:: scala
+
+   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 ≺  ⟨ val res = x27;
+  [  Info  ] 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 subexression 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 :ref:`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
+--------------------------
+
+Sometimes, a complete formal specification is hard to express,
+especially when it comes to simple, elementary functions. In such cases,
+it may be easier to provide a set of IO-examples. However, IO-examples can never
+cover all the possible executions of the function and are thus weaker than a formal
+specification. 
+
+Leon provides a powerful compromise between these two extremes.
+It introduces *symbolic IO-examples*, expressed through a specialized ``passes``
+construct, which resembles pattern-matching:
+
+.. code-block:: scala
+
+  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.
+Notice that the examples are symbolic, in that the elements of the lists are
+left as arbitrary values. 
+
+The semantics of ``passes: ( (A, B) => Boolean)`` are the following:
+
+.. code-block:: scala
+
+  (a, b) passes {
+    case p1 => e1
+    case p2 => e2
+    ...
+    case pN => eN
+  }
+
+where ``a: A`` is a tuple of method parameters and/or ``this``, ``b: B``,
+and for each i ``pi: A`` and ``ei: B``, is equivalent to
+
+.. code-block:: scala
+
+  a match {
+    case p1 => b == e1
+    case p2 => b == e2
+    ...
+    case pN => b == eN
+    case _  => true
+  }
+
+Leon will manage 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  ] }
+  ...
+
+

doc/synthesis.rst

+.. _synthesis:
+
 Synthesis
 =========