Chalice: Smoke testing to find unreachable code, preconditions that are equivalent to false and assumptions that introduce contradictions. Can be used with the command line switch "-smoke".

6 files changed, 311 insertions, 26 deletions

diff --git a/Chalice/src/Ast.scala b/Chalice/src/Ast.scala
index 8c59882f..f6fea537 100644
--- a/Chalice/src/Ast.scala
+++ b/Chalice/src/Ast.scala
@@ -303,7 +303,9 @@ sealed abstract class Statement extends ASTNode {
   def Declares: List[Variable] = Nil // call after resolution

   def Targets: Set[Variable] = Set() // assigned local variables

 }

-case class Assert(e: Expression) extends Statement

+case class Assert(e: Expression) extends Statement {

+  var smokeErrorNr: Option[Int] = None

+}

 case class Assume(e: Expression) extends Statement

 case class BlockStmt(ss: List[Statement]) extends Statement {

   override def Targets = (ss :\ Set[Variable]()) { (s, vars) => vars ++ s.Targets}

diff --git a/Chalice/src/Chalice.scala b/Chalice/src/Chalice.scala
index 973d6b94..ed543df3 100644
--- a/Chalice/src/Chalice.scala
+++ b/Chalice/src/Chalice.scala
@@ -37,6 +37,7 @@ object Chalice {
   // percentageSupport 2: use function and provide some (redundant) axioms

   // percentageSupport 3: use an uninterpreted function and axiomatize the properties of multiplication

   private[chalice] var percentageSupport = 2;

+  private[chalice] var smoke = false;

 

   def main(args: Array[String]): Unit = {

     var boogiePath = "C:\\boogie\\Binaries\\Boogie.exe"

@@ -62,7 +63,8 @@ object Chalice {
      "-autoFold" -> {() => autoFold = true},

      "-autoMagic"-> {() => autoMagic = true},

      "-noFreeAssume" -> {() => noFreeAssume = true},

-     "-showFullStackTrace" -> {() => showFullStackTrace = true}

+     "-showFullStackTrace" -> {() => showFullStackTrace = true},

+     "-smoke" -> {() => smoke = true}

     )

     lazy val help = options.keys.foldLeft("syntax: chalice")((s, o) => s + " [" + o + "]") +

     " [-boogie:path]" +

@@ -88,7 +90,7 @@ object Chalice {
        } catch { case _ => CommandLineError("-percentageSupport takes integer argument", help); }

      }

      else if (a.startsWith("-") || a.startsWith("/"))

-			boogieArgs += ('"' + a + '"' + " ")

+			boogieArgs += ("\"" + a + "\"" + " ")

 				// other arguments starting with "-" or "/" are sent to Boogie.exe

 				/* [MHS] Quote whole argument to not confuse Boogie with arguments that

 				 * contain spaces, e.g. if Chalice is invoked as

@@ -97,6 +99,13 @@ object Chalice {
      else inputs += a

     }

     

+    // for smoke testing, we want to see all failing assertions, so we use no

+    // error limit (or a very high one), and turn the subsumption option off

+    if (smoke) {

+      boogieArgs += ("\"-subsumption:0\" ")

+      boogieArgs += ("\"-errorLimit:10000\" ")

+    }

+    

     percentageSupport match {

       case 0 => TranslatorPrelude.addComponent(PercentageStandardPL)

       case 1 => TranslatorPrelude.addComponent(PercentageStandardPL, PercentageFixedDenominatorPL)

@@ -134,8 +143,9 @@ object Chalice {
          Console.err.println("Error: " + e);

        Nil

      case parser.Success(prog, _) =>

-       if (printProgram) PrintProgram.P(prog)

-       prog

+       val pprog = if (smoke) SmokeTest.smokeProgram(prog) else prog

+       if (printProgram) PrintProgram.P(pprog)

+       pprog

     }).flatten;

     if (parseErrors) return;

 

@@ -209,14 +219,25 @@ object Chalice {
            val input = new BufferedReader(new InputStreamReader(boogie.getInputStream));

            var line = input.readLine();

            var previous_line = null: String;

-           while(line!=null){

-             Console.out.println(line);

-             Console.out.flush;

+           val boogieOutput: ListBuffer[String] = new ListBuffer()

+           while (line!=null){

+             if (!smoke) {

+               Console.out.println(line);

+               Console.out.flush;

+             }

+             boogieOutput += line

              previous_line = line;

              line = input.readLine();

            }

            boogie.waitFor;

            input.close;

+           

+           // smoke test output

+           if (smoke) {

+             val output = SmokeTest.processBoogieOutput(boogieOutput.toList)

+             Console.out.println(output);

+             Console.out.flush;

+           }

 

            // generate code

            if(gen && (previous_line != null) && previous_line.endsWith(" 0 errors")) { // hack

@@ -230,14 +251,14 @@ object Chalice {
   }

 

   def writeFile(filename: String, text: String) {

-   val writer = new FileWriter(new File(filename));

-   writer.write(text);

-   writer.flush();

-   writer.close();

+    val writer = new FileWriter(new File(filename));

+    writer.write(text);

+    writer.flush();

+    writer.close();

   }

 

   def CommandLineError(msg: String, help: String) = {

-   Console.err.println("Error: " + msg)

+    Console.err.println("Error: " + msg)

   }

 

   def ReportError(pos: Position, msg: String) = {

@@ -252,3 +273,4 @@ object Chalice {
 

 class InternalErrorException(val msg: String) extends Throwable

 class NotSupportedException(val msg: String) extends Throwable

+

diff --git a/Chalice/src/SmokeTest.scala b/Chalice/src/SmokeTest.scala
new file mode 100644
index 00000000..659de182
--- /dev/null
+++ b/Chalice/src/SmokeTest.scala
@@ -0,0 +1,163 @@
+

+package chalice;

+

+import scala.util.parsing.input.Position

+import scala.util.parsing.input.NoPosition

+

+/** SmokeTest allows to perform 'smoke testing' on any given Chalice program.

+ *  The prover is instructed to try proving 'false' at various places in the

+ *  program to find unreachable code, precondition that are equivalent to false

+ *  or assumptions that introduce a contradiction.

+ *

+ *  @author Stefan Heule

+ */

+object SmokeTest {

+

+  /** Map from error message ID's to their position, error message and location name (e.g. method+class name) */

+  private var errorMessages: scala.collection.SortedMap[Int, (Position, String, String)] = scala.collection.SortedMap()

+  private var count: Int = 0 // current error message id

+  

+  /** Process the output of Boogie and generate the correct warnings from smoke testing */

+  def processBoogieOutput(out: List[String]): String = {

+    var errorCount: Map[String, Int] = Map()

+    val SmokePattern = ".*: SMOKE-TEST-([0-9]+).".r

+    val SummaryPattern = "Boogie program verifier finished with ([0-9]+) verified, ([0-9]+) errors".r

+    var result = "";

+    var smokeErrors: Set[Int] = Set()

+    var outcome: Option[(Int,Int)] = None

+    for (s <- out) s match {

+      case SmokePattern(id) => smokeErrors += id.toInt

+      case SummaryPattern(verified, errors) => outcome = Some((verified.toInt,errors.toInt))

+      case _ => result += s + "\n"

+    }

+    val smokeTestAssertions = errorMessages.size

+    val smokeTestWarnings = smokeTestAssertions - smokeErrors.size

+    

+    {

+      var t = "";

+      for ((errNr, (pos, msg, location)) <- errorMessages) yield {

+        if (!errorCount.contains(location)) errorCount += location -> 0

+        if (!smokeErrors.contains(errNr)) {

+          errorCount += location -> (errorCount(location)+1)

+          t += "  " + pos + ": " + msg + "\n"

+        }

+      }

+      t

+    } + "\n" +

+    "Smoke testing finished with " + errorCount.values.filter(_ == 0).size + " verified, " + smokeTestWarnings + " warnings\n"

+    // for the moment do not show errors not related to smoke testing

+    /* "General Boogie program verifier errors" + "\n" +

+    result +

+    (outcome match {

+      case None => ""

+      case Some((verified,errors)) => "Boogie program verifier finished."

+    })*/

+  }

+  

+  /** Add smoke assertions for to a program. */

+  def smokeProgram(prog: List[TopLevelDecl]): List[TopLevelDecl] = {

+    for (decl <- prog) yield decl match {

+      case cl: Class =>

+        val newmembers = for (m <- cl.members) yield m match {

+          case MonitorInvariant(e) => m

+          case f@ Field(id, t, ghost) => m

+          case method: Method =>

+            copyPosition(method, smokeMethod(method, cl))

+          case Condition(id, optE) => m

+          case Predicate(id, definition) => m

+          case Function(id, ins, out, specs, e) => m

+          case m: MethodTransform => m

+          case CouplingInvariant(ids, e) => m

+        }

+        copyPosition(cl, Class(cl.classId, cl.parameters, cl.module, newmembers))

+      case ch: Channel => ch

+    }

+  }

+  

+  /** Add smoke assertions for a method (if necessary). */

+  private def smokeMethod(method: Method, cl: Class) = {

+    val location = "method " + cl.classId + "." + method.id

+    var newbody = smokeStmt(method.body, location)

+    val preassert = smokeAssert(method.pos, "Precondition of method " + method.Id + " is equivalent to false.", location)

+    val postassert = smokeAssert(method.pos, "The end of method " + method.Id + " is unreachable.", location)

+    newbody = preassert :: newbody ::: postassert :: Nil

+    Method(method.id, method.ins, method.outs, method.spec, newbody)

+  }

+  

+  /** Add smoke assertions for multiple statements (if necessary). */

+  private def smokeStmt(stmts: List[Statement], location: String): List[Statement] = {

+    (for (s <- stmts) yield copyPosition(s, smokeStmt(s, location))).flatten

+  }

+  

+  /** Add smoke assertions for a statement (if necessary). */

+  private def smokeStmt(stmt: Statement, location: String): List[Statement] = {

+    stmt match {

+      case Assume(_) => stmt :: smokeAssert(stmt.pos, "Assumption might introduce a contradiction.", location) :: Nil

+      case BlockStmt(ss) => smokeStmt(ss, location)

+      case ifs@IfStmt(guard, BlockStmt(then), els) =>

+        val newthen = smokeStmt(then, location) ::: smokeAssert(ifs.pos, "The end of the if-branch is unreachable.", location) :: Nil

+        val newelse = els match {

+          case None => None

+          case Some(s) => Some(BlockStmt(smokeStmt(s, location) ::: smokeAssert(ifs.pos, "The end of the else-branch is unreachable.", location) :: Nil))

+        }

+        IfStmt(guard, BlockStmt(newthen), newelse) :: Nil

+      case WhileStmt(guard, oldInvs, newInvs, lkch, BlockStmt(body)) =>

+        val newbody = smokeStmt(body, location) ::: smokeAssert(stmt.pos, "The end of the while-body is unreachable.", location) :: Nil

+        WhileStmt(guard, oldInvs, newInvs, lkch, BlockStmt(newbody)) :: Nil

+      case Lock(obj, BlockStmt(body), rdLock) =>

+        Lock(obj, BlockStmt(smokeStmt(body, location)), rdLock) :: Nil

+      case _: RefinementBlock => stmt :: Nil

+      

+      case Assert(_) => stmt :: Nil

+      case Assign(_, _) => stmt :: Nil

+      case FieldUpdate(_, _) => stmt :: Nil

+      case _: LocalVar => stmt :: Nil

+      case _: SpecStmt => stmt :: Nil

+      case _: Call => stmt :: Nil

+      case Install(_, _, _) => stmt :: Nil

+      case Share(_, _, _) => stmt :: Nil

+      case Unshare(_) => stmt :: Nil

+      case Acquire(_) => stmt :: Nil

+      case Release(_) => stmt :: Nil

+      case RdAcquire(_) => stmt :: Nil

+      case RdRelease(_) => stmt :: Nil

+      case Downgrade(_) => stmt :: Nil

+      case Free(_) => stmt :: Nil

+      case Fold(_) => stmt :: Nil

+      case Unfold(_) => stmt :: Nil

+      case CallAsync(_, _, _, _, _) => stmt :: Nil

+      case JoinAsync(_, _) => stmt :: Nil

+      case Send(_, _) => stmt :: Nil

+      case Receive(_, _, _) => stmt :: Nil

+      case _: Signal => stmt :: Nil

+      case _: Wait => stmt :: Nil

+    }

+  }

+  

+  /** Generate an "assert false" with a certain position and a certain error

+   *  message. Note: We generate "assert 1!=1" instead of "assert false", as

+   *  Boogie seems to perform some weird optimization for false, which does

+   *  not generate warnings for all failing assertions (even if the command

+   *  line switch /subsumption:0 is used).

+   */

+  private def smokeAssert(pos: Position, error: String, location: String) = {

+    count += 1

+    errorMessages += count -> (pos, error, location)

+    val assert = Assert(Neq(IntLiteral(1), IntLiteral(1)))

+    assert.smokeErrorNr = Some(count)

+    assert.pos = pos

+    assert

+  }

+  

+  /** Copy the position of an old AST node to a new node (if not already

+   *  present).

+   */

+  private def copyPosition[A <: ASTNode](oldNode: A, newNode: A): A = {

+    if (newNode.pos == NoPosition) newNode.pos = oldNode.pos

+    newNode

+  }

+  /** Copy the position from one old AST node to multiple new nodes. */

+  private def copyPosition[A <: ASTNode](oldNode: A, newNodes: List[A]): List[A] = {

+    for (newNode <- newNodes) yield copyPosition(oldNode, newNode)

+  }

+}
\ No newline at end of file
diff --git a/Chalice/src/Translator.scala b/Chalice/src/Translator.scala
index f8a196d0..28d74176 100644
--- a/Chalice/src/Translator.scala
+++ b/Chalice/src/Translator.scala
@@ -310,6 +310,7 @@ class Translator {
     val methodKStmts = BLocal(methodKV) :: bassume(0 < methodK && 1000*methodK < permissionOnePercent)

     

     // check definedness of the method contract

+    (if (!Chalice.smoke)

     Proc(method.FullName + "$checkDefinedness", 

       NewBVarWhere("this", new Type(currentClass)) :: (method.ins map {i => Variable2BVarWhere(i)}),

       method.outs map {i => Variable2BVarWhere(i)},

@@ -326,7 +327,8 @@ class Translator {
         // check postcondition

         InhaleWithChecking(Postconditions(method.spec), "postcondition", methodK) :::

         // check lockchange

-        (LockChanges(method.spec) flatMap { lc => isDefined(lc)})) ::

+        (LockChanges(method.spec) flatMap { lc => isDefined(lc)})) :: Nil

+    else Nil) :::

     // check that method body satisfies the method contract

     Proc(method.FullName,

       NewBVarWhere("this", new Type(currentClass)) :: (method.ins map {i => Variable2BVarWhere(i)}),

@@ -431,18 +433,23 @@ class Translator {
 

   def translateStatement(s: Statement, methodK: Expr): List[Stmt] = {

     s match {

-      case Assert(e) =>

-        val newGlobals = etran.FreshGlobals("assert");

-        val tmpHeap = Boogie.NewBVar(HeapName, theap, true);

-        val tmpMask = Boogie.NewBVar(MaskName, tmask, true); 

-        val tmpCredits = Boogie.NewBVar(CreditsName, tcredits, true); 

-        val tmpTranslator = new ExpressionTranslator(List(tmpHeap._1.id, tmpMask._1.id, tmpCredits._1.id), List(etran.ChooseEtran(true).Heap, etran.ChooseEtran(true).Mask, etran.ChooseEtran(true).Credits), currentClass);        

-        Comment("assert") ::

-        // exhale e in a copy of the heap/mask/credits

-        BLocal(tmpHeap._1) :: (tmpHeap._2 := etran.Heap) ::

-        BLocal(tmpMask._1) :: (tmpMask._2 := etran.Mask) ::

-        BLocal(tmpCredits._1) :: (tmpCredits._2 := etran.Credits) ::

-        tmpTranslator.Exhale(List((e, ErrorMessage(s.pos, "Assertion might not hold."))), "assert", true, methodK, true)

+      case a@Assert(e) =>

+        a.smokeErrorNr match {

+          case None =>

+            val newGlobals = etran.FreshGlobals("assert");

+            val tmpHeap = Boogie.NewBVar(HeapName, theap, true);

+            val tmpMask = Boogie.NewBVar(MaskName, tmask, true); 

+            val tmpCredits = Boogie.NewBVar(CreditsName, tcredits, true); 

+            val tmpTranslator = new ExpressionTranslator(List(tmpHeap._1.id, tmpMask._1.id, tmpCredits._1.id), List(etran.ChooseEtran(true).Heap, etran.ChooseEtran(true).Mask, etran.ChooseEtran(true).Credits), currentClass);        

+            Comment("assert") ::

+            // exhale e in a copy of the heap/mask/credits

+            BLocal(tmpHeap._1) :: (tmpHeap._2 := etran.Heap) ::

+            BLocal(tmpMask._1) :: (tmpMask._2 := etran.Mask) ::

+            BLocal(tmpCredits._1) :: (tmpCredits._2 := etran.Credits) ::

+            tmpTranslator.Exhale(List((e, ErrorMessage(s.pos, "Assertion might not hold."))), "assert", true, methodK, true)

+          case Some(err) =>

+            bassert(e, a.pos, "SMOKE-TEST-" + err + ".") :: Nil

+        }

       case Assume(e) =>

         Comment("assume") ::

         isDefined(e) :::

diff --git a/Chalice/tests/examples/SmokeTestTest.chalice b/Chalice/tests/examples/SmokeTestTest.chalice
new file mode 100644
index 00000000..a9bbf197
--- /dev/null
+++ b/Chalice/tests/examples/SmokeTestTest.chalice
@@ -0,0 +1,76 @@
+// chalice-parameter=-smoke

+// This file is meant as a test for Chalice's smoke testing feature (command line switch -smoke)

+class Cell {

+  var f: int;

+  

+  method a1()

+    requires false

+  {}

+  

+  method a2()

+    requires acc(this.f,-2)

+  {}

+  

+  method a3()

+    requires acc(this.f)

+  {

+    if (this.f > 0) {

+      this.f := 0;

+    }

+  }

+  

+  method a4()

+    requires acc(this.f)

+  {

+    if (false) {

+      this.f := 0;

+    }

+  }

+  

+  method a5()

+    requires acc(this.f)

+  {

+    if (true) {

+      this.f := 0;

+    }

+  }

+  

+  method a6()

+    requires acc(this.f)

+  {

+    if (false) {

+      this.f := 0;

+    } else {

+      this.f := 1;

+    }

+  }

+  

+  method a7(i: int, j: int)

+    requires i != j;

+  {

+    assume i == j;

+  }

+  

+  method a8()

+    requires acc(this.f)

+  {

+    while (true) {

+      this.f := this.f + 1

+    }

+  }

+  

+  method a9()

+  {

+    call a8()

+  }

+  

+  method a10()

+    requires acc(this.f)

+  {

+    if (true) {

+      this.f := 0;

+    } else {

+      this.f := 1;

+    }

+  }

+}

diff --git a/Chalice/tests/examples/SmokeTestTest.output.txt b/Chalice/tests/examples/SmokeTestTest.output.txt
new file mode 100644
index 00000000..1fe23f64
--- /dev/null
+++ b/Chalice/tests/examples/SmokeTestTest.output.txt
@@ -0,0 +1,15 @@
+Verification of SmokeTestTest.chalice using parameters="-smoke" 

+

+  6.3: Precondition of method a1 is equivalent to false.
+  6.3: The end of method a1 is unreachable.
+  10.3: Precondition of method a2 is equivalent to false.
+  10.3: The end of method a2 is unreachable.
+  25.5: The end of the if-branch is unreachable.
+  41.5: The end of the if-branch is unreachable.
+  51.5: Assumption might introduce a contradiction.
+  48.3: The end of method a7 is unreachable.
+  54.3: The end of method a8 is unreachable.
+  70.5: The end of the else-branch is unreachable.
+
+Smoke testing finished with 3 verified, 10 warnings
+