Fix for issue #32.

uclid-org · Jun 29, 2020 · 8bb6492 · 8bb6492
1 parent 2b1e8a8
commit 8bb6492
Show file tree

Hide file tree

Showing 3 changed files with 27 additions and 14 deletions.
diff --git a/src/main/scala/uclid/AssertionTree.scala b/src/main/scala/uclid/AssertionTree.scala
@@ -101,14 +101,27 @@ class AssertionTree {
   val initialRoot : TreeNode = root
   var currentNode : TreeNode = root
 
+  /** Helper function to create a new child node. */
+  def newChildNode() {
+    val childNode = new TreeNode(Some(currentNode), List.empty)
+    currentNode.children += childNode
+    currentNode = childNode
+  }
+
+  /** This function should be called for each separate verificaiton task.
+   *
+   *  It ensures that assumptions are not reused across procedures or
+   *  other verification tasks.
+   */
+  def startVerificationScope() {
+    newChildNode()
+  }
+
   def addAssumption(assump: smt.Expr) {
     if (currentNode.assertions.size > 0) {
-      val childNode = new TreeNode(Some(currentNode), List(assump))
-      currentNode.children += childNode
-      currentNode = childNode
-    } else {
-      currentNode += assump
+      newChildNode()
     }
+    currentNode += assump
   }
 
   def addAssert(assert: AssertInfo) {

diff --git a/src/main/scala/uclid/SymbolicSimulator.scala b/src/main/scala/uclid/SymbolicSimulator.scala
@@ -188,6 +188,7 @@ class SymbolicSimulator (module : Module) {
             proofResults = List.empty
             dumpResults("clear_context", defaultLog)
           case "unroll" =>
+            assertionTree.startVerificationScope()
             val label : String = cmd.resultVar match {
               case Some(l) => l.toString
               case None    => "unroll"
@@ -196,12 +197,6 @@ class SymbolicSimulator (module : Module) {
             val properties : List[Identifier] = extractProperties(Identifier("properties"), cmd.params)
             symbolicSimulateLambdas(0, cmd.args(0)._1.asInstanceOf[IntLit].value.toInt, true, false, 
                                     context, label, createNoLTLFilter(properties), createNoLTLFilter(properties), solver)
-            //initialize(false, true, false, context, label, noLTLFilter)
-            //symbolicSimulate(0, cmd.args(0)._1.asInstanceOf[IntLit].value.toInt, true, false, context, label, noLTLFilter)
-            // initialize(false, true, false, context, label, noLTLFilter)
-            // symbolicSimulate(0, cmd.args(0)._1.asInstanceOf[IntLit].value.toInt, true, false, context, label, noLTLFilter)
-            //runLazySC(cmd.args(0)._1.asInstanceOf[IntLit].value.toInt, context, label, noLTLFilter, solver)
-
           case "horn" =>
             val label : String = cmd.resultVar match {
               case Some(l) => l.toString
@@ -220,6 +215,7 @@ class SymbolicSimulator (module : Module) {
             val propertyFilter = createNoLTLFilter(properties)
             runLazySC(lz, cmd.args(0)._1.asInstanceOf[IntLit].value.toInt, context, label, propertyFilter, propertyFilter, solver)
           case "bmc" =>
+            assertionTree.startVerificationScope()
             val label : String = cmd.resultVar match {
               case Some(l) => l.toString()
               case None => "bmc"
@@ -229,6 +225,7 @@ class SymbolicSimulator (module : Module) {
             initialize(false, true, false, context, label, propertyFilter, propertyFilter)
             symbolicSimulate(0, cmd.args(0)._1.asInstanceOf[IntLit].value.toInt, true, false, context, label, propertyFilter, propertyFilter)
           case "induction" =>
+            assertionTree.startVerificationScope()
             val labelBase : String = cmd.resultVar match {
               case Some(l) => l.toString + ": induction_base"
               case None    => "induction_base"
@@ -1414,6 +1411,7 @@ class SymbolicSimulator (module : Module) {
   }
   /** Add assumption. */
   def addAssumptionToTree(e : smt.Expr, params : List[ExprDecorator]) {
+    assertLog.debug("Assumption: {}", e.toString())
     assertionTree.addAssumption(e)
   }
 
@@ -1486,6 +1484,8 @@ class SymbolicSimulator (module : Module) {
   }
 
   def verifyProcedure(proc : ProcedureDecl, label : String) = {
+    assertionTree.startVerificationScope()
+
     val procScope = context + proc
     val initSymbolTable = getInitSymbolTable(context)
     val initProcState0 = newInputSymbols(initSymbolTable, 1, context)

diff --git a/src/test/scala/VerifierSpec.scala b/src/test/scala/VerifierSpec.scala
@@ -160,9 +160,9 @@ class BasicVerifierSpec extends FlatSpec {
   "test-functions-1.ucl" should "verify successfully." in {
     VerifierSpec.expectedFails("./test/test-functions-1.ucl", 0)
   }
-  // "test-conflicting-assumptions.ucl" should "verify all but 1 assertion" in {
-  //   VerifierSpec.expectedFails("./test/test-conflicting-assumptions.ucl", 1)
-  // }
+  "test-conflicting-assumptions.ucl" should "verify all but 1 assertion" in {
+    VerifierSpec.expectedFails("./test/test-conflicting-assumptions.ucl", 1)
+  }
   "test-exprs-1.ucl" should "verify four assertions and fail to verify two assertions." in {
     VerifierSpec.expectedFails("./test/test-exprs-1.ucl", 2)
   }