From 13bfea23b0729614cfd7616b5c7c819b442bc1b0 Mon Sep 17 00:00:00 2001 From: FedericoAureliano Date: Fri, 12 Jan 2024 22:32:44 +0000 Subject: [PATCH] Add CI for smoke testing. Make helper function for smoke testing so that CI uses same code as main source. --- builduclid.sh | 9 --- get-prerequisites-linux.sh | 5 -- get-prerequisites-macos.sh | 5 -- src/main/scala/uclid/SymbolicSimulator.scala | 34 ++------- src/main/scala/uclid/Utils.scala | 34 +++++++++ src/test/scala/SmokeSpec.scala | 76 ++++++++++++++++++++ 6 files changed, 114 insertions(+), 49 deletions(-) delete mode 100644 builduclid.sh delete mode 100644 get-prerequisites-linux.sh delete mode 100644 get-prerequisites-macos.sh create mode 100644 src/test/scala/SmokeSpec.scala diff --git a/builduclid.sh b/builduclid.sh deleted file mode 100644 index 55e641399..000000000 --- a/builduclid.sh +++ /dev/null @@ -1,9 +0,0 @@ -#! /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 ../../.. diff --git a/get-prerequisites-linux.sh b/get-prerequisites-linux.sh deleted file mode 100644 index 1c225b478..000000000 --- a/get-prerequisites-linux.sh +++ /dev/null @@ -1,5 +0,0 @@ -#! /bin/bash - -source get-z3-linux.sh -source get-cvc5-linux.sh -source get-delphi-linux.sh diff --git a/get-prerequisites-macos.sh b/get-prerequisites-macos.sh deleted file mode 100644 index 102732f13..000000000 --- a/get-prerequisites-macos.sh +++ /dev/null @@ -1,5 +0,0 @@ -#! /bin/bash - -source get-z3-macos.sh -source get-cvc5-macos.sh -source get-delphi-macos.sh diff --git a/src/main/scala/uclid/SymbolicSimulator.scala b/src/main/scala/uclid/SymbolicSimulator.scala index 1c0801c77..f39615074 100644 --- a/src/main/scala/uclid/SymbolicSimulator.scala +++ b/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("-")) { diff --git a/src/main/scala/uclid/Utils.scala b/src/main/scala/uclid/Utils.scala index 6e8761c59..9145f0bfd 100644 --- a/src/main/scala/uclid/Utils.scala +++ b/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) { diff --git a/src/test/scala/SmokeSpec.scala b/src/test/scala/SmokeSpec.scala new file mode 100644 index 000000000..e5d2dbb32 --- /dev/null +++ b/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} + } +}