Merge pull request #243 from uclid-org/fix-242

Fix Type Checking + Type Declaration Bugs with ADTs
uclid-org · May 11, 2024 · a4c5f77 · a4c5f77
2 parents d0f0c10 + 97e94b0
commit a4c5f77
Show file tree

Hide file tree

Showing 6 changed files with 82 additions and 11 deletions.
diff --git a/src/main/scala/uclid/lang/TypeChecker.scala b/src/main/scala/uclid/lang/TypeChecker.scala
@@ -98,7 +98,13 @@ class TypeSynonymFinderPass extends ReadOnlyPass[Unit]
         TupleType(fieldTypes.map(simplifyType(_, visited, m)))
       case RecordType(fields) =>
         RecordType(fields.map((f) => (f._1, simplifyType(f._2, visited, m))))
-      case dt: DataType => dt
+      case dt: DataType => 
+        DataType(dt.id, dt.constructors.map(c => (c._1, c._2.map(s => (s._1, {
+          s._2 match {
+            case SynonymType(id) if id == dt.id => s._2
+            case _ => simplifyType(s._2, visited, m)
+          }
+        })))))
       case MapType(inTypes, outType) =>
         MapType(inTypes.map(simplifyType(_, visited, m)), simplifyType(outType, visited, m))
       case ArrayType(inTypes, outType) =>

diff --git a/src/main/scala/uclid/smt/SMTLIB2Interface.scala b/src/main/scala/uclid/smt/SMTLIB2Interface.scala
@@ -131,18 +131,25 @@ trait SMTLIB2Base {
           case dt : DataType =>
             val typeName = dt.id
             val nameString = "((%s 0))".format(typeName)
-            val constructorsString = Utils.join(dt.cstors.map(c => {
-              val sels = Utils.join(c.inTypes.map(s => {
-                val inner = generateDatatype(s._2) 
-                val sel = "(%s %s)".format(Context.getFieldName(s._1), inner._1)
-                sel
-              }), " ")
-              val constru = "(%s %s)".format(c.id, sels)
-              constru
-            }), " ")
+            val (consNames : String, newTypesNames1 : List[String], newTypes1 : List[String]) = dt.cstors
+              .foldRight("", List.empty[String], List.empty[String]) {
+                (c, acc) => {
+                  val (_consNames : String, _newTypesNames1 : List[String], _newTypes1: List[String]) = c.inTypes
+                    .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),
+                        _acc._2 ++ newTypeNames, _acc._3 ++ newTypes)
+                    }
+                  }
+                  (acc._1 + " " + s"(${c.id} ${_consNames})",  
+                    acc._2 ++ _newTypesNames1, acc._3 ++ _newTypes1)
+                }
+            }
+            val constructorsString = consNames
             val newType = "(declare-datatypes %s ((%s)))".format(nameString, constructorsString)
             typeMap = typeMap.addSynonym(typeName, t)
-            (typeName, typeName :: Nil, newType :: List.empty)
+            (typeName, typeName :: newTypesNames1, newType :: newTypes1)
           case BoolType => 
             typeMap = typeMap.addSynonym("Bool", t)
             ("Bool", List.empty, List.empty)

diff --git a/src/test/scala/ParserSpec.scala b/src/test/scala/ParserSpec.scala
@@ -168,6 +168,11 @@ class ParserSpec extends AnyFlatSpec {
         assert (p.errors.size > 0)
     }
   }
+  "test-adt-24.ucl" should "parse successfully" in {
+    val fileModules = UclidMain.compile(ConfigCons.createConfig("test/test-adt-24.ucl"), lang.Identifier("main"))
+    val instantiatedModules = UclidMain.instantiateModules(UclidMain.Config(), fileModules, lang.Identifier("main"))
+    assert (instantiatedModules.size == 1)
+  }
   "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
@@ -128,6 +128,9 @@ class VerifierSanitySpec extends AnyFlatSpec {
   "test-adt-23-datatypegeneration.ucl" should "verify successfully." in {
     VerifierSpec.expectedFails("./test/test-adt-23-datatypegeneration.ucl", 0)
   }
+  "test-adt-25.ucl" should "verify successfully." in {
+    VerifierSpec.expectedFails("./test/test-adt-25.ucl", 0)
+  }
   "test-array-0.ucl" should "verify successfully." in {
     VerifierSpec.expectedFails("./test/test-array-0.ucl", 0)
   }

diff --git a/test/test-adt-24.ucl b/test/test-adt-24.ucl
@@ -0,0 +1,17 @@
+module main {
+    type t = record {a: integer, b: integer};
+    datatype option_t = Some(value: t) | None();
+
+    var x: option_t;
+    var y: t;
+
+    init {
+        assert x.value == y;
+    }
+
+    control {
+        bmc(0);
+        check;
+        print_results;
+    }
+}
diff --git a/test/test-adt-25.ucl b/test/test-adt-25.ucl
@@ -0,0 +1,33 @@
+
+
+module main {
+
+    type e_t = enum {X, Y, Z};
+
+    datatype adt_t = 
+        A (a: e_t) | B (b : e_t, c: e_t);
+
+
+    var adt1 : adt_t;
+    var adt2 : adt_t;
+
+    init {
+        adt1 = A(Y);
+        adt2 = B(Y, Y);
+    }
+
+    next {
+        adt1' = A(adt2.b);
+        adt2' = B(adt1.a, adt2.c);
+    }
+
+    property match: adt1.a == adt2.b;
+
+    control {
+        v = bmc(2);
+        check;
+        print_results;
+        v.print_cex_json();
+    }
+
+}