Add CI for smoke testing. Make helper function for smoke testing so t…

…hat CI uses same code as main source.

src/main/scala/uclid/SymbolicSimulator.scala

@@ -1205,38 +1205,12 @@ class SymbolicSimulator (module : Module) {
 
     if (config.smoke) {
 
-      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.name +: unreachableLines
-        } else if (p.result.isFalse) {
-          reachableLines = p.assert.name +: reachableLines
-        } else {
-          undeterminedLines = p.assert.name +: undeterminedLines
-        }
-      }
-
-      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)
-      undeterminedSet = undeterminedSet.diff(unreachableSet)
-      reachableSet = reachableSet.diff(unreachableSet)
-      reachableSet = reachableSet.diff(undeterminedSet)
-
-      reachableLines = reachableSet.toList.sorted
-      unreachableLines = unreachableSet.toList.sorted
-      undeterminedLines = undeterminedSet.toList.sorted
+      val (reachableLines, unreachableLines, undeterminedLines) = Utils.smokeTestCounter(assertionResults)
 
       UclidMain.printResult("%d smoke tests run.".format(assertionResults.size))
-      UclidMain.printResult("%d code blocks tested.".format(reachableSet.size + unreachableSet.size + undeterminedSet.size))
-      UclidMain.printResult("%d warnings.".format(unreachableSet.size))
-      UclidMain.printResult("%d tests inconclusive.".format(undeterminedSet.size))
+      UclidMain.printResult("%d code blocks tested.".format(reachableLines.size + unreachableLines.size + undeterminedLines.size))
+      UclidMain.printResult("%d warnings.".format(unreachableLines.size))
+      UclidMain.printResult("%d inconclusives.".format(undeterminedLines.size))
 
       unreachableLines.foreach { (l) =>
         if (l.contains("-")) {

src/main/scala/uclid/Utils.scala

@@ -42,6 +42,7 @@ import scala.util.parsing.input.Position
 import com.typesafe.scalalogging.Logger
 import java.io.File
 import java.io.PrintWriter
+import _root_.scopt.Check
 
 object Utils {
   def writeToFile(p: String, s: String): Unit = {
@@ -182,6 +183,39 @@ object Utils {
     }
     roots.foldLeft(List.empty[V])((acc, r) => visit(r, List.empty[U], acc))
   }
+
+
+  def smokeTestCounter(assertionResults: List[CheckResult]) : (List[String], List[String], List[String]) = {
+    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.name +: unreachableLines
+      } else if (p.result.isFalse) {
+        reachableLines = p.assert.name +: reachableLines
+      } else {
+        undeterminedLines = p.assert.name +: undeterminedLines
+      }
+    }
+
+    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)
+    undeterminedSet = undeterminedSet.diff(unreachableSet)
+    reachableSet = reachableSet.diff(unreachableSet)
+    reachableSet = reachableSet.diff(undeterminedSet)
+
+    reachableLines = reachableSet.toList.sorted
+    unreachableLines = unreachableSet.toList.sorted
+    undeterminedLines = undeterminedSet.toList.sorted
+
+    return (reachableLines, unreachableLines, undeterminedLines)
+  }
 }
 
 class UniqueNamer(val prefix : String) {

src/test/scala/SmokeSpec.scala

@@ -0,0 +1,76 @@
+/*
+ * UCLID5 Verification and Synthesis Engine
+ *
+ * Copyright (c) 2017.
+ * Sanjit A. Seshia, Rohit Sinha and Pramod Subramanyan.
+ *
+ * All Rights Reserved.
+ * Redistribution and use in source and binary forms, with or without
+ * modification, are permitted provided that the following conditions are
+ * met:
+ * 1. Redistributions of source code must retain the above copyright notice,
+ *
+ * this list of conditions and the following disclaimer.
+ * 2. Redistributions in binary form must reproduce the above copyright
+ * notice, this list of conditions and the following disclaimer in the
+ *
+ * documentation and/or other materials provided with the distribution.
+ * 3. Neither the name of the copyright holder nor the names of its
+ * contributors may be used to endorse or promote products derived from this
+ * software without specific prior written permission.
+ *
+ * THIS SOFTWARE IS PROVIDED BY THE COPYRIGHT HOLDERS AND CONTRIBUTORS "AS
+ * IS" AND ANY EXPRESS OR IMPLIED WARRANTIES, INCLUDING, BUT NOT LIMITED TO,
+ * THE IMPLIED WARRANTIES OF MERCHANTABILITY AND FITNESS FOR A PARTICULAR
+ * PURPOSE ARE DISCLAIMED. IN NO EVENT SHALL THE COPYRIGHT HOLDER OR
+ * CONTRIBUTORS BE LIABLE FOR ANY DIRECT, INDIRECT, INCIDENTAL, SPECIAL,
+ * EXEMPLARY, OR CONSEQUENTIAL DAMAGES (INCLUDING, BUT NOT LIMITED TO,
+ * PROCUREMENT OF SUBSTITUTE GOODS OR SERVICES; LOSS OF USE, DATA, OR
+ * PROFITS; OR BUSINESS INTERRUPTION) HOWEVER CAUSED AND ON ANY THEORY OF
+ * LIABILITY, WHETHER IN CONTRACT, STRICT LIABILITY, OR TORT (INCLUDING
+ * NEGLIGENCE OR OTHERWISE) ARISING IN ANY WAY OUT OF THE USE OF THIS
+ * SOFTWARE, EVEN IF ADVISED OF THE POSSIBILITY OF SUCH DAMAGE.
+ *
+ * Author: Federico Mora (based on Elizabeth Polgreen's Oracle Spec)
+ *
+ * UCLID smoke testing tests
+ *
+ */
+
+package uclid
+package test
+
+import org.scalatest.flatspec.AnyFlatSpec
+import java.io.File
+import uclid.{lang => l}
+
+object SmokeSpec {
+  def runSmokeTesting(filename: String) : (List[String], List[String], List[String]) = {
+    UclidMain.enableStringOutput()
+    UclidMain.clearStringOutput()
+    val config = ConfigCons.createConfig(filename).copy(smoke=true)
+    val modules = UclidMain.compile(config, lang.Identifier("main"), true)
+    val mainModule = UclidMain.instantiate(config, modules, l.Identifier("main"))
+    assert (mainModule.isDefined)
+    val results = UclidMain.execute(mainModule.get, config)
+    return Utils.smokeTestCounter(results)
+  }
+}
+class SmokeSpec extends AnyFlatSpec {
+
+  "test-smoke-bmc.ucl" should "give two warnings." in {
+    val (reachableLines, unreachableLines, undeterminedLines) = SmokeSpec.runSmokeTesting("./test/test-smoke-bmc.ucl")
+    unreachableLines.foreach(l => info(l))
+    assertResult(2){unreachableLines.length}
+  }  
+  "test-smoke-induction.ucl" should "give no warnings." in {
+    val (reachableLines, unreachableLines, undeterminedLines) = SmokeSpec.runSmokeTesting("./test/test-smoke-induction.ucl")
+    unreachableLines.foreach(l => info(l))
+    assertResult(0){unreachableLines.length}
+  }  
+  "test-smoke-multiple-modules.ucl" should "give one warning." in {
+    val (reachableLines, unreachableLines, undeterminedLines) = SmokeSpec.runSmokeTesting("./test/test-smoke-multiple-modules.ucl")
+    unreachableLines.foreach(l => info(l))
+    assertResult(1){unreachableLines.length}
+  }
+}