Smoke Testing

builduclid.sh

@@ -0,0 +1,9 @@
+#! /bin/bash
+
+sbt universal:packageBin
+cd target/universal
+rm -r uclid-0.9.5
+unzip uclid-0.9.5.zip
+cd uclid-0.9.5
+export PATH=$PATH:$PWD/bin
+cd ../../..

get-prerequisites-linux.sh

@@ -0,0 +1,5 @@
+#! /bin/bash
+
+source get-z3-linux.sh
+source get-cvc5-linux.sh
+source get-delphi-linux.sh

get-prerequisites-macos.sh

@@ -0,0 +1,5 @@
+#! /bin/bash
+
+source get-z3-macos.sh
+source get-cvc5-macos.sh
+source get-delphi-macos.sh

src/main/scala/uclid/SymbolicSimulator.scala

@@ -361,9 +361,11 @@ class SymbolicSimulator (module : Module) {
             printResults(proofResults, cmd.argObj, config)
             needToPrintResults=false
           case "print_cex" =>
-            printCEX(proofResults, cmd.args, cmd.argObj)
+            if (!config.smoke) {
+              printCEX(proofResults, cmd.args, cmd.argObj)
+            }
           case "print_cex_json" =>
-            if (!config.smtSolver.isEmpty)
+            if (!config.smtSolver.isEmpty && !config.smoke)
               printCEXJSON(proofResults, cmd.args, cmd.argObj, config, solver)
             else
               UclidMain.printError("print_cex_json works only with SMTLIB2Interface, skipping this command.")
@@ -1200,18 +1202,29 @@ class SymbolicSimulator (module : Module) {
       return
 
     Utils.assert(passCount + failCount + undetCount == assertionResults.size, "Unexpected assertion count.")
-    UclidMain.printResult("%d assertions passed.".format(passCount))
-    UclidMain.printResult("%d assertions failed.".format(failCount))
-    UclidMain.printResult("%d assertions indeterminate.".format(undetCount))
+
+    if (config.smoke) {
+      UclidMain.printResult("%d smoke tests run.".format(assertionResults.size))
+      UclidMain.printResult("%d warnings.".format(passCount))
+      UclidMain.printResult("%d tests indeterminate.".format(undetCount))
+    } else {
+      UclidMain.printResult("%d assertions passed.".format(passCount))
+      UclidMain.printResult("%d assertions failed.".format(failCount))
+      UclidMain.printResult("%d assertions indeterminate.".format(undetCount))
+    }
 
     if (config.verbose > 0) {
       assertionResults.foreach{ (p) =>
         if (p.result.isTrue) {
-          UclidMain.printStatus("  PASSED -> " + p.assert.toString)
+          if (config.smoke) {
+            UclidMain.printStatus("  WARNING -> " + p.assert.toString)
+          } else {
+            UclidMain.printStatus("  PASSED -> " + p.assert.toString)
+          }
         }
       }
     }
-    if (failCount > 0) {
+    if (failCount > 0 && !config.smoke) {
       assertionResults.foreach{ (p) =>
         if (p.result.isFalse) {
           UclidMain.printStatus("  FAILED -> " + p.assert.toString)

src/main/scala/uclid/UclidMain.scala

@@ -47,6 +47,8 @@ import scala.collection.immutable._
 import lang.{Identifier, Module,  _}
 import uclid.Utils.ParserErrorList
 import com.typesafe.scalalogging.Logger
+import java.io.{File, FileWriter}
+import uclid.lang.SmokeInserter
 
 /** This is the main class for Uclid.
  *
@@ -83,6 +85,8 @@ object UclidMain {
       ufToArray         : Boolean = false,
       printStackTrace   : Boolean = false,
       noLetify          : Boolean = false, // prevents SMTlib interface from letifying
+      smoke             : Boolean = false, 
+
       /* 
         verbosities:
         0: essential: print nothing but results and error messages
@@ -151,12 +155,16 @@ object UclidMain {
         ( x, c) => {c.copy(verbose = x)}
       }.text("verbosity level (0-4)")
 
+      opt[Unit]("smoke").action{
+        (_, c) => c.copy(smoke = true)
+      }.text("Smoke test for unreachable code.")
+
       help("help").text("prints this usage text")
 
       arg[java.io.File]("<file> ...").unbounded().required().action {
         (x, c) => c.copy(files = c.files :+ x)
       }.text("List of files to analyze.")
-      
+
       // override def renderingMode = scopt.RenderingMode.OneColumn
     }
     val config = parser.parse(args, Config())
@@ -224,6 +232,7 @@ object UclidMain {
 
   def createCompilePassManager(config: Config, test: Boolean, mainModuleName: lang.Identifier, recompile : Boolean = false) = {
     val passManager = new PassManager("compile")
+
     // adds init and next to every module
     passManager.addPass(new ModuleCanonicalizer())
     // introduces LTL operators (which were parsed as function applications)
@@ -308,6 +317,7 @@ object UclidMain {
     // checks module instancs are instantiated correctly
     passManager.addPass(new ModuleInstanceChecker())
     passManager.addPass(new CaseEliminator())
+
     passManager.addPass(new ForLoopUnroller())
     // hyperproperties for procedures
     passManager.addPass(new ModularProductProgram())
@@ -329,25 +339,29 @@ object UclidMain {
     passManager.addPass(new ModuleCleaner())
     passManager.addPass(new BlockVariableRenamer())
     passManager
-  }  
+  }
   /** Parse modules, typecheck them, inline procedures, create LTL monitors, etc. */
   def compile(config: Config, mainModuleName : Identifier, test : Boolean = false): List[Module] = {
     UclidMain.printVerbose("Compiling modules")
     type NameCountMap = Map[Identifier, Int]
     val srcFiles : Seq[java.io.File] = config.files
     var nameCnt : NameCountMap = Map().withDefaultValue(0)
-    val passManager = createCompilePassManager(config, test, mainModuleName)
+    val passManager = createCompilePassManager(config, test, mainModuleName, false)
 
     val filenameAdderPass = new AddFilenameRewriter(None)
+
     // Helper function to parse a single file.
     def parseFile(srcFile : String) : List[Module] = {
+
+
       val file = scala.io.Source.fromFile(srcFile)
-      // TODO: parse line by line instead of loading the complete file into a string
+
       val modules = UclidParser.parseModel(srcFile, file.mkString)
       file.close()
       filenameAdderPass.setFilename(srcFile)
       modules.map(m => filenameAdderPass.visit(m, Scope.empty)).flatten
     }
+
     val parsedModules = srcFiles.foldLeft(List.empty[Module]) {
       (acc, srcFile) => acc ++ parseFile(srcFile.getPath())
     }
@@ -432,6 +446,12 @@ object UclidMain {
     passManager.addPass(new ModuleEliminator(mainModuleName))
     // Expands (grounds) finite_forall and finite_exists quantifiers
     passManager.addPass(new FiniteQuantsExpander())
+    // test unreachable code
+    if (config.smoke) {
+      passManager.addPass(new SmokeAnalyzer())
+      passManager.addPass(new SmokeRemover())
+      passManager.addPass(new SmokeInserter())
+    }
     passManager.addPass(new LTLOperatorRewriter())
     passManager.addPass(new LTLPropertyRewriter())
     passManager.addPass(new Optimizer())

src/main/scala/uclid/lang/SmokeAnalyzer.scala

@@ -0,0 +1,62 @@
+/*
+ * 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 : Alejandro Sanchez Ocegueda
+ * 
+ * Smoke testing in conjunction with LTL is not supported.
+ * The analyzer throws an error if this is attempted.
+ * 
+ */
+
+package uclid
+package lang
+
+class SmokeAnalyzePass extends RewritePass {
+
+  // Check for LTL properties and throw an error if there are any.
+  override def rewriteModule(module: Module, ctx: Scope): Option[Module] = {
+    val moduleSpecs = module.decls.collect{ case spec : SpecDecl => spec }
+    val ltlSpecs = moduleSpecs.filter(s => s.params.exists(d => d == LTLExprDecorator))
+    if (ltlSpecs.size == 0) {
+      Some(module)
+    } else {
+      throw new Utils.RuntimeError(s"Smoke testing in the presence of LTL specifications is currently not supported. This support will be added in the next UCLID release.")
+    }
+  }
+
+}
+
+
+class SmokeAnalyzer() extends ASTRewriter(
+  "SmokeAnalyzer", new SmokeAnalyzePass()
+)

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

@@ -0,0 +1,67 @@
+/*
+ * 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 : Alejandro Sanchez Ocegueda
+ * 
+ * Inserts an 'assert false' statement at the end of each (nonempty) basic block.
+ * This is a sanity check for unreachable code.
+ * Note: Smoke testing should not be used with LTL properties yet.
+ * 
+ */
+
+package uclid
+package lang
+
+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}")))
+      assertFalse.setPos(st.stmts(st.stmts.length-1).pos)
+      val newstmts = st.stmts :+ assertFalse 
+      smokeCount += 1
+      Some(BlockStmt(st.vars, newstmts))
+    } else {
+      Some(st)
+    }
+
+  } 
+
+}
+
+
+class SmokeInserter() extends ASTRewriter(
+  "SmokerInserter", new SmokeInsertPass()
+)

src/main/scala/uclid/lang/SmokeRemover.scala

@@ -0,0 +1,61 @@
+/*
+ * 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 : Alejandro Sanchez Ocegueda
+ * 
+ * Removes all assertions and specifications (invariants, properties, etc.) in preparation for smoke testing.
+ * This is done to make the smoke tests more efficient, as they need only test reachability of code.
+ * 
+ */
+
+package uclid
+package lang
+
+class SmokeRemovePass extends RewritePass {
+
+  // Removes properties and invariants.
+  override def rewriteSpec(spec : SpecDecl, ctx : Scope) : Option[SpecDecl] = {
+    None
+  }
+
+  // Removes assert statements.
+  override def rewriteAssert(st : AssertStmt, ctx : Scope) : Option[Statement] = {
+    None
+  }
+
+}
+
+
+class SmokeRemover() extends ASTRewriter(
+  "SmokerRemover", new SmokeRemovePass()
+)