From 3b4ce043817f75cc85a8e6b2414cc637a9269a40 Mon Sep 17 00:00:00 2001
From: adwait <godbole15@gmail.com>
Date: Fri, 10 May 2024 18:21:21 -0700
Subject: [PATCH] Fix minor bug in ADT datatype declaration field ordering

- added tests to catch such bugs in the future
- also added a test for ADT field reuse
---
 .../scala/uclid/smt/SMTLIB2Interface.scala    |  2 +-
 src/test/scala/ParserSpec.scala               | 22 ++++++++++++++
 src/test/scala/VerifierSpec.scala             |  3 ++
 test/test-adt-26-goodconstructionordering.ucl | 29 +++++++++++++++++++
 test/test-adt-27-badconstructionordering.ucl  | 29 +++++++++++++++++++
 test/test-adt-28-fieldreuse.ucl               | 29 +++++++++++++++++++
 6 files changed, 113 insertions(+), 1 deletion(-)
 create mode 100644 test/test-adt-26-goodconstructionordering.ucl
 create mode 100644 test/test-adt-27-badconstructionordering.ucl
 create mode 100644 test/test-adt-28-fieldreuse.ucl

diff --git a/src/main/scala/uclid/smt/SMTLIB2Interface.scala b/src/main/scala/uclid/smt/SMTLIB2Interface.scala
index baa9c83b..2d592d3f 100644
--- 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
index 81dde746..d958967f 100644
--- 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
index 1a20f12c..7f694c72 100644
--- 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
new file mode 100644
index 00000000..65c2855b
--- /dev/null
+++ 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();
+    }
+
+}
\ No newline at end of file
diff --git a/test/test-adt-27-badconstructionordering.ucl b/test/test-adt-27-badconstructionordering.ucl
new file mode 100644
index 00000000..4007e244
--- /dev/null
+++ 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();
+    }
+
+}
\ No newline at end of file
diff --git a/test/test-adt-28-fieldreuse.ucl b/test/test-adt-28-fieldreuse.ucl
new file mode 100644
index 00000000..95d61625
--- /dev/null
+++ 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();
+    }
+
+}
\ No newline at end of file