LTL support and more descriptive test results.

src/main/scala/uclid/SymbolicSimulator.scala

@@ -1205,23 +1205,23 @@ class SymbolicSimulator (module : Module) {
 
     if (config.smoke) {
 
-      var reachableLines : List[Int] = Nil
-      var unreachableLines : List[Int] = Nil
-      var undeterminedLines : List[Int] = Nil
+      var reachableLines : List[String] = Nil
+      var unreachableLines : List[String] = Nil
+      var undeterminedLines : List[String] = Nil
 
       assertionResults.foreach { (p) =>
         if (p.result.isTrue) {
-          unreachableLines = p.assert.pos.pos.line +: unreachableLines
+          unreachableLines = p.assert.name +: unreachableLines
         } else if (p.result.isFalse) {
-          reachableLines = p.assert.pos.pos.line +: reachableLines
+          reachableLines = p.assert.name +: reachableLines
         } else {
-          undeterminedLines = p.assert.pos.pos.line +: undeterminedLines
+          undeterminedLines = p.assert.name +: undeterminedLines
         }
       }
 
-      var reachableSet : Set[Int] = reachableLines.toSet
-      var unreachableSet : Set[Int] = unreachableLines.toSet
-      var undeterminedSet : Set[Int] = undeterminedLines.toSet
+      var reachableSet : Set[String] = reachableLines.toSet
+      var unreachableSet : Set[String] = unreachableLines.toSet
+      var undeterminedSet : Set[String] = undeterminedLines.toSet
 
       unreachableSet = unreachableSet.diff(reachableSet)
       undeterminedSet = undeterminedSet.diff(reachableSet)
@@ -1239,10 +1239,14 @@ class SymbolicSimulator (module : Module) {
       UclidMain.printResult("%d tests inconclusive.".format(undeterminedSet.size))
 
       unreachableLines.foreach { (l) =>
-        UclidMain.printStatus(" WARNING -> code block ending at line %d is never run.".format(l))
+        if (l.contains("-")) {
+          UclidMain.printStatus(" WARNING -> %s are never run.".format(l))
+        } else {
+          UclidMain.printStatus(" WARNING -> %s is never run.".format(l))
+        }
       }
       undeterminedLines.foreach { (l) =>
-        UclidMain.printStatus(" WARNING -> line %d's reachability is inconclusive.".format(l))
+        UclidMain.printStatus(" WARNING -> %s's reachability is inconclusive.".format(l))
       }
 
     } else {
@@ -1269,7 +1273,7 @@ class SymbolicSimulator (module : Module) {
         }
       }
     }
-    if (undetCount > 0) {
+    if (undetCount > 0 && !config.smoke) {
       assertionResults.foreach{ (p) =>
         if (p.result.isUndefined) {
           UclidMain.printStatus("  UNDEF -> " + p.assert.toString)

src/main/scala/uclid/UclidMain.scala

@@ -233,14 +233,15 @@ object UclidMain {
 
     // test unreachable code
     if (config.smoke) {
-      passManager.addPass(new SmokeAnalyzer())
       passManager.addPass(new SmokeRemover())
       passManager.addPass(new SmokeInserter())
     }
     // adds init and next to every module
     passManager.addPass(new ModuleCanonicalizer())
     // introduces LTL operators (which were parsed as function applications)
-    passManager.addPass(new LTLOperatorIntroducer())
+    if (!config.smoke) {
+      passManager.addPass(new LTLOperatorIntroducer())
+    }
     // imports all declarations except init and next declarations into module
     passManager.addPass(new ModuleImportRewriter())
     // imports types into module
@@ -450,8 +451,10 @@ object UclidMain {
     passManager.addPass(new ModuleEliminator(mainModuleName))
     // Expands (grounds) finite_forall and finite_exists quantifiers
     passManager.addPass(new FiniteQuantsExpander())
-    passManager.addPass(new LTLOperatorRewriter())
-    passManager.addPass(new LTLPropertyRewriter())
+    if (!config.smoke) {
+      passManager.addPass(new LTLOperatorRewriter())
+      passManager.addPass(new LTLPropertyRewriter())
+    }
     passManager.addPass(new Optimizer())
     // optimisation, has previously been called
     passManager.addPass(new ModuleCleaner())

src/main/scala/uclid/lang/SmokeInserter.scala

@@ -47,8 +47,17 @@ class SmokeInsertPass() extends RewritePass {
   var smokeCount = 1
   override def rewriteBlock(st : BlockStmt, ctx : Scope) : Option[Statement] = {
 
-    if (st.stmts.length > 0) {
-      var assertFalse = AssertStmt(BoolLit(false), Some(Identifier(s"Smoke signal ${smokeCount}")))
+    if (st.stmts.length == 1) {
+      val line = st.stmts(0).pos.line
+      var assertFalse = AssertStmt(BoolLit(false), Some(Identifier(s"line %d".format(line))))
+      assertFalse.setPos(st.stmts(0).pos)
+      val newstmts = st.stmts :+ assertFalse 
+      smokeCount += 1
+      Some(BlockStmt(st.vars, newstmts))
+    } else if (st.stmts.length > 1) {
+      val topLine = st.stmts(0).pos.line
+      val bottomLine = st.stmts(st.stmts.length-1).pos.line
+      var assertFalse = AssertStmt(BoolLit(false), Some(Identifier(s"lines %d-%d".format(topLine, bottomLine))))
       assertFalse.setPos(st.stmts(st.stmts.length-1).pos)
       val newstmts = st.stmts :+ assertFalse 
       smokeCount += 1

test/test-smoke-bmc-fixed.ucl

@@ -0,0 +1,34 @@
+/* This program shows the correct implementation of the buggy program in test-smoke-bmc.ucl */
+
+module main {
+  var a : integer;
+  var safe_var : boolean;
+
+  init {
+    a = 0;
+    safe_var = true;
+  }
+
+  next {
+    case  
+    (a >= 0) : {
+      a' = a - 1;
+      safe_var' = true;
+    }
+
+    (a < 0) : {
+      a' = a + 1;
+      safe_var' = false;
+    }
+    esac
+  }
+
+  invariant safety_inv: safe_var == true;
+
+  control {
+    bmc(3);
+    check;
+    print_results;
+  }
+
+}

test/test-smoke-bmc.ucl

@@ -14,7 +14,7 @@ module main {
   next {
     case  
     (a > 0) : {
-      a' = a + 1;
+      a' = a - 1;
       safe_var' = true;
     }
 

test/test-smoke-ltl-error.ucl → test/test-smoke-ltl.ucl

@@ -1,17 +1,20 @@
-// TODO
-/* Check that the error message for LTL is correctly thrown */
+/* Check that smoke testing works properly in the presence of LTL. */
 
 module main {
 
   var prop : boolean;
-
   init {
     prop = true;
   }
 
 
   next {
-    prop' = true;
+    if (prop == false) {
+      prop' = false;
+    }
+    else {
+      prop' = true;
+    }
   }
 
   property[LTL] always_true : G(prop == true);
@@ -22,7 +25,6 @@ module main {
     print_results;
   }
 
-
 }