Merge pull request #247 from uclid-org/adt.constructionordering

Fix minor bug in ADT datatype declaration field ordering
uclid-org · May 11, 2024 · 6f3f8da · 6f3f8da
2 parents a4c5f77 + 3b4ce04
commit 6f3f8da
Show file tree

Hide file tree

Showing 6 changed files with 113 additions and 1 deletion.
diff --git a/src/main/scala/uclid/smt/SMTLIB2Interface.scala b/src/main/scala/uclid/smt/SMTLIB2Interface.scala
@@ -138,7 +138,7 @@ trait SMTLIB2Base {
                     .foldRight("", List.empty[String], List.empty[String]){
                       (s, _acc) => {
                       val (fldName, newTypeNames, newTypes) = generateDatatype(s._2)
-                      (_acc._1 + " " + "(%s %s)".format(Context.getFieldName(s._1), fldName),
+                      ("(%s %s)".format(Context.getFieldName(s._1), fldName)  + " " + _acc._1,
                         _acc._2 ++ newTypeNames, _acc._3 ++ newTypes)
                     }
                   }

diff --git a/src/test/scala/ParserSpec.scala b/src/test/scala/ParserSpec.scala
@@ -173,6 +173,28 @@ class ParserSpec extends AnyFlatSpec {
     val instantiatedModules = UclidMain.instantiateModules(UclidMain.Config(), fileModules, lang.Identifier("main"))
     assert (instantiatedModules.size == 1)
   }
+  "test-adt-27-badconstructionordering.ucl" should "not parse successfully." in {
+    try {
+      val filename = "test/test-adt-27-badconstructionordering.ucl"
+      val fileModules = UclidMain.compile(ConfigCons.createConfig(filename), lang.Identifier("main"))
+      assert (fileModules.size == 1)
+    }
+    catch {
+      case p : Utils.TypeErrorList =>
+        assert (p.errors.size > 0)
+    }
+  }
+  "test-adt-28-fieldreuse.ucl" should "not parse successfully." in {
+    try {
+      val filename = "test/test-adt-28-fieldreuse.ucl"
+      val fileModules = UclidMain.compile(ConfigCons.createConfig(filename), lang.Identifier("main"))
+      assert (fileModules.size == 1)
+    }
+    catch {
+      case p : Utils.TypeErrorList =>
+        assert (p.errors.size > 0)
+    }
+  }
   "test-type1.ucl" should "not parse successfully." in {
     try {
       val filename = "test/test-type1.ucl"

diff --git a/src/test/scala/VerifierSpec.scala b/src/test/scala/VerifierSpec.scala
@@ -131,6 +131,9 @@ class VerifierSanitySpec extends AnyFlatSpec {
   "test-adt-25.ucl" should "verify successfully." in {
     VerifierSpec.expectedFails("./test/test-adt-25.ucl", 0)
   }
+  "test-adt-26-goodconstructionordering.ucl" should "verify successfully." in {
+    VerifierSpec.expectedFails("./test/test-adt-26-goodconstructionordering.ucl", 0)
+  }
   "test-array-0.ucl" should "verify successfully." in {
     VerifierSpec.expectedFails("./test/test-array-0.ucl", 0)
   }

diff --git a/test/test-adt-26-goodconstructionordering.ucl b/test/test-adt-26-goodconstructionordering.ucl
@@ -0,0 +1,29 @@
+
+
+module main {
+
+    datatype adt_t = A (ia : integer, ba : bv4) | B (ib : integer, bb : boolean);
+
+    var adt1 : adt_t;
+    var adt2 : adt_t;
+
+    init {
+        adt1 = B(10, true);
+        adt2 = A(10, 4bv4);
+    }
+
+    next {
+        adt1' = B(adt1.ib+1, adt1.bb);
+        adt2' = A(adt2.ia+1, adt2.ba);
+    }
+
+    property match: adt1.ib == adt2.ia;
+
+    control {
+        v = bmc(2);
+        check;
+        print_results;
+        v.print_cex_json();
+    }
+
+}
diff --git a/test/test-adt-27-badconstructionordering.ucl b/test/test-adt-27-badconstructionordering.ucl
@@ -0,0 +1,29 @@
+
+
+module main {
+
+    datatype adt_t = A (ia : integer, ba : bv4) | B (ib : integer, bb : boolean);
+
+    var adt1 : adt_t;
+    var adt2 : adt_t;
+
+    init {
+        adt1 = B(true, 10);
+        adt2 = A(10, 4bv4);
+    }
+
+    next {
+        adt1' = B(adt1.ib+1, adt1.bb);
+        adt2' = A(adt2.ia+1, adt2.ba);
+    }
+
+    property match: adt1.ib == adt2.ia;
+
+    control {
+        v = bmc(2);
+        check;
+        print_results;
+        v.print_cex_json();
+    }
+
+}
diff --git a/test/test-adt-28-fieldreuse.ucl b/test/test-adt-28-fieldreuse.ucl
@@ -0,0 +1,29 @@
+
+
+module main {
+
+    datatype adt_t = A (i : integer, b : bv4) | B (i : integer, b : boolean);
+
+    var adt1 : adt_t;
+    var adt2 : adt_t;
+
+    init {
+        adt1 = B(10, true);
+        adt2 = A(10, 4bv4);
+    }
+
+    next {
+        adt1' = B(adt1.i+1, adt1.b);
+        adt2' = A(adt2.i+1, adt2.b);
+    }
+
+    property match: adt1.i == adt2.i;
+
+    control {
+        v = bmc(2);
+        check;
+        print_results;
+        v.print_cex_json();
+    }
+
+}