From 7033967feddb92e080fbceb6804f99c62dbda2b4 Mon Sep 17 00:00:00 2001 From: FedericoAureliano Date: Wed, 3 Jul 2024 22:13:08 -0700 Subject: [PATCH 1/3] add failing test --- src/test/scala/SMTLIB2Spec.scala | 3 +++ test/issue-255.ucl | 17 +++++++++++++++++ 2 files changed, 20 insertions(+) create mode 100644 test/issue-255.ucl diff --git a/src/test/scala/SMTLIB2Spec.scala b/src/test/scala/SMTLIB2Spec.scala index 502fba632..5f30817a8 100644 --- a/src/test/scala/SMTLIB2Spec.scala +++ b/src/test/scala/SMTLIB2Spec.scala @@ -445,6 +445,9 @@ class SMTLIB2Spec extends AnyFlatSpec { "issue-187b.ucl" should "verify all assertions." in { SMTLIB2Spec.expectedFails("./test/issue-187b.ucl", 0) } + "issue-255.ucl" should "faill single assertion." in { + SMTLIB2Spec.expectedFails("./test/issue-255.ucl", 1) + } "test-redundant-assign.ucl" should "verify all assertions." in { SMTLIB2Spec.expectedFails("./test/test-redundant-assign.ucl", 0) } diff --git a/test/issue-255.ucl b/test/issue-255.ucl new file mode 100644 index 000000000..3df523383 --- /dev/null +++ b/test/issue-255.ucl @@ -0,0 +1,17 @@ +module main { + type t; + datatype a = A(x: t); + + var y: a; + var z: t; + + init { + assert y.x == z; + } + + control { + bmc(0); + check; + print_results; + } +} \ No newline at end of file From 0cad47670f49dfbdc92c7119681099d59b423a18 Mon Sep 17 00:00:00 2001 From: FedericoAureliano Date: Wed, 3 Jul 2024 22:17:18 -0700 Subject: [PATCH 2/3] preassert should only declare types with no dependencies --- .../scala/uclid/smt/SMTLIB2Interface.scala | 46 ++++++++++++++----- 1 file changed, 35 insertions(+), 11 deletions(-) diff --git a/src/main/scala/uclid/smt/SMTLIB2Interface.scala b/src/main/scala/uclid/smt/SMTLIB2Interface.scala index 2d592d3fe..67b9a02d1 100644 --- a/src/main/scala/uclid/smt/SMTLIB2Interface.scala +++ b/src/main/scala/uclid/smt/SMTLIB2Interface.scala @@ -45,11 +45,13 @@ import scala.collection.mutable.{Set => MutableSet} import scala.collection.mutable.ListBuffer import com.typesafe.scalalogging.Logger import lang.Identifier - import org.json4s._ import lang.Scope import lang.ExpressionEnvironment +import scala.annotation.tailrec +import scala.collection.mutable + trait SMTLIB2Base { val smtlib2BaseLogger = Logger(classOf[SMTLIB2Base]) @@ -539,24 +541,46 @@ class SMTLIB2Interface(args: List[String], var disableLetify: Boolean=false) ext } override def preassert(e: Expr) { - val declCommands = new ListBuffer[(String, String)]() + val declCommands = new mutable.HashMap[String, String]() Context.findTypes(e).filter(typ => !typeMap.contains(typ)).foreach { newType => { val (name, newTypeNames, newTypes) = generateDatatype(newType) - (newTypeNames zip newTypes).foreach({case (n, typ) => declCommands.append((n, typ))}) + (newTypeNames zip newTypes).foreach({case (n, typ) => declCommands += (n -> typ)}) } } - // Figure out which type depends on which other type and then declare them in the right order. - def dependsOn(d1: (String, String), d2: (String, String)) : Boolean = { - return d2._2.contains(d1._1) - } - val declCommandsSorted = declCommands.toList.sortWith(dependsOn) - declCommandsSorted.foreach{ - decl => { - writeCommand(decl._2) + val dependsGraph = new mutable.HashMap[String, List[String]]() + declCommands.foreach(d1 => declCommands.foreach(d2 => { + if (d1._1 != d2._1 && d1._2.contains(d2._1)) { + // d1 depends on d2 + val d1deps = dependsGraph.getOrElse(d1._1, List()) + dependsGraph.update(d1._1, d2._1 :: d1deps) + } + })) + + @tailrec + def reduce(toWrite: Map[String, String], written: Set[String]): Unit = { + if (toWrite.isEmpty) { + return } + val change = new ListBuffer[String]() + toWrite.foreach(d => { + val depends = dependsGraph.getOrElse(d._1, List()) + val dependsFiltered = depends.filter(d => !written.contains(d)) + if (dependsFiltered == List()) { + writeCommand(d._2) + change.append(d._1) + } + }) + if (change.isEmpty) { + throw new Utils.AssertionError(s"Didn't make progress writing declarations. The following are not declared: ${toWrite.keys}") + } + val newToWrite = toWrite.filter(d => !change.contains(d._1)); + val newWritten = written ++ change + reduce(newToWrite, newWritten) } + + reduce(declCommands.toMap, Set.empty) } override def check(produceModel: Boolean = true) : SolverResult = { From 7b5a91eda054959eb5248c72712518d559ca866e Mon Sep 17 00:00:00 2001 From: FedericoAureliano Date: Wed, 3 Jul 2024 22:36:22 -0700 Subject: [PATCH 3/3] must be an exact word match to determine type dependency --- src/main/scala/uclid/smt/SMTLIB2Interface.scala | 11 +++++++++-- 1 file changed, 9 insertions(+), 2 deletions(-) diff --git a/src/main/scala/uclid/smt/SMTLIB2Interface.scala b/src/main/scala/uclid/smt/SMTLIB2Interface.scala index 67b9a02d1..b05201c20 100644 --- a/src/main/scala/uclid/smt/SMTLIB2Interface.scala +++ b/src/main/scala/uclid/smt/SMTLIB2Interface.scala @@ -45,6 +45,7 @@ import scala.collection.mutable.{Set => MutableSet} import scala.collection.mutable.ListBuffer import com.typesafe.scalalogging.Logger import lang.Identifier + import org.json4s._ import lang.Scope import lang.ExpressionEnvironment @@ -549,10 +550,16 @@ class SMTLIB2Interface(args: List[String], var disableLetify: Boolean=false) ext } } + def dependsOn(d1: (String, String), d2: (String, String)) : Boolean = { + // if the exact name is found in the body of the declaration, then it depends on it. + val body1 = d1._2.replaceAll("[()]", " ") + val name2 = s" ${d2._1} " + d1 != d2 && body1.contains(name2) + } + val dependsGraph = new mutable.HashMap[String, List[String]]() declCommands.foreach(d1 => declCommands.foreach(d2 => { - if (d1._1 != d2._1 && d1._2.contains(d2._1)) { - // d1 depends on d2 + if (dependsOn(d1, d2)) { val d1deps = dependsGraph.getOrElse(d1._1, List()) dependsGraph.update(d1._1, d2._1 :: d1deps) }