Chalice: Improve smoke testing: look for preconditions of functions, predicates and monitor invariants that are equivalent to false, and add a command line option "/smokeAll" to insert 'assert false' after *every* Chalice statement.

6 files changed, 91 insertions, 46 deletions

diff --git a/Chalice/src/Chalice.scala b/Chalice/src/Chalice.scala
index 524ab5f6..3b0bd70d 100644
--- a/Chalice/src/Chalice.scala
+++ b/Chalice/src/Chalice.scala
@@ -38,6 +38,7 @@ object Chalice {
   // percentageSupport 3: use an uninterpreted function and axiomatize the properties of multiplication

   private[chalice] var percentageSupport = 2;

   private[chalice] var smoke = false;

+  private[chalice] var smokeAll = false;

 

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

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

@@ -97,7 +98,10 @@ object Chalice {
        "show the full stack trace if an exception is encountered"),

      "smoke" -> (

        {() => smoke = true},

-       "smoke testing; try to find unreachable code, preconditions/invariants/predicates that are equivalent to false and assumptions that introduce contradictions, by trying to prove 'false' at various positions.")

+       "smoke testing; try to find unreachable code, preconditions/invariants/predicates that are equivalent to false and assumptions that introduce contradictions, by trying to prove 'false' at various positions."),

+     "smokeAll" -> (

+       {() => smokeAll = true; smoke = true},

+       "aggressive smoke testing; try to prove false after every statement.")

     )

     // help text for options with arguments

     val nonBooleanOptions = ListMap(

diff --git a/Chalice/src/PrettyPrinter.scala b/Chalice/src/PrettyPrinter.scala
index bc7f2811..718c0413 100644
--- a/Chalice/src/PrettyPrinter.scala
+++ b/Chalice/src/PrettyPrinter.scala
@@ -80,8 +80,12 @@ object PrintProgram {
     }

   }

   def Stmt(s: Statement, indent: Int): Unit = s match {

-    case Assert(e) =>

-      print("assert "); Expr(e); println(Semi)

+    case a@Assert(e) =>

+      print("assert "); Expr(e);

+      if (!a.smokeErrorNr.isEmpty)

+        println(Semi + " // smoke assertion: " + SmokeTest.smokeWarningMessage(a.smokeErrorNr.get))

+      else

+        println(Semi)

     case Assume(e) =>

       print("assume "); Expr(e); println(Semi)

     case BlockStmt(ss) =>

diff --git a/Chalice/src/SmokeTest.scala b/Chalice/src/SmokeTest.scala
index bf2622ce..8a8f46eb 100644
--- a/Chalice/src/SmokeTest.scala
+++ b/Chalice/src/SmokeTest.scala
@@ -33,10 +33,15 @@ object SmokeTest {
   private var smokeAssertions: Map[Int,SmokeAssert] = Map()

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

   

+  /** Get the warning message from an ID */

+  def smokeWarningMessage(id: Int) = {

+    smokeAssertions(id).msg

+  }

+  

   /** 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 SmokePattern = ".*: SMOKE-TEST-([0-9]+).*".r

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

     var verificationResult = "";

     var smokeErrors: Set[Int] = Set()

@@ -123,6 +128,11 @@ object SmokeTest {
   /** Add smoke assertions for a statement (if necessary). */

   private def smokeStmt(stmt: Statement, in: Set[SmokeAssert]): (List[Statement], Set[SmokeAssert]) = {

     var out = in

+    

+    def helper(name: String): List[Statement] = {

+      val (stmts, sout) = smokeSimpleStmt(stmt, in, name); out = sout; stmts

+    }

+    

     val result = stmt match {

       // composite statements

       case BlockStmt(ss) =>

@@ -169,31 +179,31 @@ object SmokeTest {
         stmt :: assumeSmoke.chaliceAssert :: Nil

       

       // simple statements that inhale something

-      case Unfold(_) => val (stmts, sout) = smokeSimpleStmt(stmt, in, "unfold"); out = sout; stmts

-      case JoinAsync(_, _) => val (stmts, sout) = smokeSimpleStmt(stmt, in, "join"); out = sout; stmts

-      case _: Call => val (stmts, sout) = smokeSimpleStmt(stmt, in, "method call"); out = sout; stmts

-      case _: SpecStmt => val (stmts, sout) = smokeSimpleStmt(stmt, in, "specification"); out = sout; stmts

-      case Receive(_, _, _) => val (stmts, sout) = smokeSimpleStmt(stmt, in, "receive"); out = sout; stmts

-      case Acquire(_) => val (stmts, sout) = smokeSimpleStmt(stmt, in, "acquire"); out = sout; stmts

-      case RdAcquire(_) => val (stmts, sout) = smokeSimpleStmt(stmt, in, "rd acquire"); out = sout; stmts

+      case Unfold(_) => helper("unfold")

+      case JoinAsync(_, _) => helper("join")

+      case _: Call => helper("method call")

+      case _: SpecStmt => helper("specification")

+      case Receive(_, _, _) => helper("receive")

+      case Acquire(_) => helper("acquire")

+      case RdAcquire(_) => helper("rd acquire")

       

       // any other simple statements

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

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

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

-      case _: LocalVar => stmt :: Nil

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

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

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

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

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

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

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

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

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

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

-      case _: Signal => stmt :: Nil

-      case _: Wait => stmt :: Nil

+      case Assert(_) => if (Chalice.smokeAll) helper("assert") else stmt :: Nil

+      case Assign(_, _) => if (Chalice.smokeAll) helper("assign") else stmt :: Nil

+      case FieldUpdate(_, _) => if (Chalice.smokeAll) helper("field update") else stmt :: Nil

+      case _: LocalVar => if (Chalice.smokeAll) helper("local variable") else stmt :: Nil

+      case Install(_, _, _) => if (Chalice.smokeAll) helper("reorder") else stmt :: Nil

+      case Share(_, _, _) => if (Chalice.smokeAll) helper("share") else stmt :: Nil

+      case Unshare(_) => if (Chalice.smokeAll) helper("unshare") else stmt :: Nil

+      case Release(_) => if (Chalice.smokeAll) helper("release") else stmt :: Nil

+      case RdRelease(_) => if (Chalice.smokeAll) helper("rd release") else stmt :: Nil

+      case Downgrade(_) => if (Chalice.smokeAll) helper("downgrade") else stmt :: Nil

+      case Free(_) => if (Chalice.smokeAll) helper("free") else stmt :: Nil

+      case Fold(_) => if (Chalice.smokeAll) helper("fold") else stmt :: Nil

+      case CallAsync(_, _, _, _, _) => if (Chalice.smokeAll) helper("fork") else stmt :: Nil

+      case Send(_, _) => if (Chalice.smokeAll) helper("send") else stmt :: Nil

+      case _: Signal => if (Chalice.smokeAll) helper("signal") else stmt :: Nil

+      case _: Wait => if (Chalice.smokeAll) helper("wait") else stmt :: Nil

     }

     (result, out)

   }

diff --git a/Chalice/src/Translator.scala b/Chalice/src/Translator.scala
index 99fb6fb4..ccfdefe6 100644
--- a/Chalice/src/Translator.scala
+++ b/Chalice/src/Translator.scala
@@ -100,6 +100,11 @@ class Translator {
         Havoc(etran.Heap) ::

         // check that invariant is well-defined

         etran.WhereOldIs(h1, m1, c1).Inhale(invs map { mi => mi.e}, "monitor invariant", true, methodK) :::

+        // smoke test: is the monitor invariant equivalent to false?

+        (if (Chalice.smoke) {

+          val a = SmokeTest.initSmokeAssert(pos, "Monitor invariant is equivalent to false.")

+          translateStatement(a.chaliceAssert, methodK)

+        } else Nil) :::

         (if (! Chalice.checkLeaks || invs.length == 0) Nil else

           // check that there are no loops among .mu permissions in monitors

           // !CanWrite[this,mu]

@@ -147,6 +152,11 @@ class Translator {
       // check definedness of the precondition

       InhaleWithChecking(Preconditions(f.spec) map { p => (if(0 < Chalice.defaults) UnfoldPredicatesWithReceiverThis(p) else p)}, "precondition", functionK) :::

       bassume(CurrentModule ==@ VarExpr(ModuleName(currentClass))) :: // verify the body assuming that you are in the module

+      // smoke test: is precondition equivalent to false?

+      (if (Chalice.smoke) {

+        val a = SmokeTest.initSmokeAssert(f.pos, "Precondition of function " + f.Id + " is equivalent to false.")

+        translateStatement(a.chaliceAssert, functionK)

+      } else Nil) :::

       // check definedness of function body

       checkBody :::

       (f.definition match {case Some(e) => BLocal(myresult) :: (Boogie.VarExpr("result") := etran.Tr(e)); case None => Nil}) :::

@@ -301,7 +311,13 @@ class Translator {
       DefaultPrecondition(),

       predicateKStmts :::

       DefinePreInitialState :::

-      InhaleWithChecking(List(DefinitionOf(pred)), "predicate definition", predicateK))

+      InhaleWithChecking(List(DefinitionOf(pred)), "predicate definition", predicateK) :::

+      // smoke test: is the predicate equivalent to false?

+      (if (Chalice.smoke) {

+        val a = SmokeTest.initSmokeAssert(pred.pos, "Predicate " + pred.FullName + " is equivalent to false.")

+        translateStatement(a.chaliceAssert, predicateK)

+      } else Nil)

+    )

   }

 

   def translateMethod(method: Method): List[Decl] = {

@@ -446,7 +462,7 @@ class Translator {
             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 + ".", 0) :: Nil

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

         }

       case Assume(e) =>

         Comment("assume") ::

@@ -1934,17 +1950,17 @@ class ExpressionTranslator(globals: List[Boogie.Expr], preGlobals: List[Boogie.E
       case PermTimes(lhs, rhs) => {

         val l = needExactChecking(lhs, default);

         val r = needExactChecking(rhs, default);

-        if (l == false || r == false) false else true // if one side doesn't need exact checking, the whole multiplication doesn't

+        (if (l == false || r == false) false else true) // if one side doesn't need exact checking, the whole multiplication doesn't

       }

       case PermPlus(lhs, rhs) => {

         val l = needExactChecking(lhs, default);

         val r = needExactChecking(rhs, default);

-        if (l == true || r == true) true else false // if one side needs exact checking, use exact

+        (if (l == true || r == true) true else false) // if one side needs exact checking, use exact

       }

       case PermMinus(lhs, rhs) => {

         val l = needExactChecking(lhs, default);

         val r = needExactChecking(rhs, default);

-        if (l == true || r == true) true else false // if one side needs exact checking, use exact

+        (if (l == true || r == true) true else false) // if one side needs exact checking, use exact

       }

     }

   }

diff --git a/Chalice/tests/examples/SmokeTestTest.chalice b/Chalice/tests/examples/SmokeTestTest.chalice
index 2f32625e..44bba5da 100644
--- a/Chalice/tests/examples/SmokeTestTest.chalice
+++ b/Chalice/tests/examples/SmokeTestTest.chalice
@@ -2,6 +2,9 @@
 class Cell {

   var f: int;

   

+  invariant acc(this.f) && f == 1

+  invariant f == 2 // SMOKE: contradiction

+  

   method a1()

     requires false // SMOKE: precondition is false

   {}

@@ -109,4 +112,9 @@ class Cell {
   {

     call a13(); // SMOKE: statements afterwards not reachable anymore

   }

+  

+  predicate valid {

+    1 == 2 // SMOKE: contradiction

+  }

 }

+

diff --git a/Chalice/tests/examples/SmokeTestTest.output.txt b/Chalice/tests/examples/SmokeTestTest.output.txt
index 0d7985d6..697119cb 100644
--- a/Chalice/tests/examples/SmokeTestTest.output.txt
+++ b/Chalice/tests/examples/SmokeTestTest.output.txt
@@ -1,19 +1,22 @@
 Verification of SmokeTestTest.chalice using parameters="" 

 

-  103.3: The postcondition at 104.13 might not hold. The expression at 104.13 might not evaluate to true.
+  106.3: The postcondition at 107.13 might not hold. The expression at 107.13 might not evaluate to true.
 
 The program did not fully verify; the smoke warnings might be misleading if contradictions are introduced by failing proof attempts of the verification.
-  5.3: Precondition of method a1 is equivalent to false.
-  9.3: Precondition of method a2 is equivalent to false.
-  24.5: The begging of the if-branch is unreachable.
-  40.5: The begging of the if-branch is unreachable.
-  50.5: Assumption introduces a contradiction.
-  56.5: The statements after the while-loop are unreachable.
-  73.5: The begging of the else-branch is unreachable.
-  87.5: The begging of the if-branch is unreachable.
-  90.7: The begging of the else-branch is unreachable.
-  90.19: Assumption introduces a contradiction.
-  97.5: Assumption introduces a contradiction.
-  110.5: The statements after the method call statement are unreachable.
+  2.1: Monitor invariant is equivalent to false.
+  8.3: Precondition of method a1 is equivalent to false.
+  12.3: Precondition of method a2 is equivalent to false.
+  27.5: The begging of the if-branch is unreachable.
+  43.5: The begging of the if-branch is unreachable.
+  53.5: Assumption introduces a contradiction.
+  59.5: The statements after the while-loop are unreachable.
+  76.5: The begging of the else-branch is unreachable.
+  83.3: Precondition of function f1 is equivalent to false.
+  90.5: The begging of the if-branch is unreachable.
+  93.7: The begging of the else-branch is unreachable.
+  93.19: Assumption introduces a contradiction.
+  100.5: Assumption introduces a contradiction.
+  113.5: The statements after the method call statement are unreachable.
+  116.3: Predicate Cell.valid is equivalent to false.
 
-Boogie program verifier finished with 1 errors and 12 smoke test warnings.

+Boogie program verifier finished with 1 errors and 15 smoke test warnings.