Rename record fields when parsing

This fixes an issue highlighted in test/test-record-3.ucl, where record fields with names that clash with other variables fail the type checker
uclid-org · May 28, 2021 · f97a54c · f97a54c
1 parent fdd7ad6
commit f97a54c
Show file tree

Hide file tree

Showing 3 changed files with 12 additions and 2 deletions.
diff --git a/src/main/scala/uclid/lang/UclidParser.scala b/src/main/scala/uclid/lang/UclidParser.scala
@@ -237,7 +237,7 @@ object UclidParser extends UclidTokenParsers with PackratParsers {
     lazy val RelOp: Parser[String] = OpGT | OpUGT | OpLT | OpULT | OpEQ | OpNE | OpGE | OpUGE | OpLE | OpULE
     lazy val UnOp: Parser[String] = OpNot | OpMinus
     lazy val RecordSelectOp: Parser[PolymorphicSelect] = positioned {
-      ("." ~> Id) ^^ { case id => PolymorphicSelect(id) }
+      ("." ~> RecordElementId) ^^ { case id => PolymorphicSelect(id) }
     }
     lazy val HyperSelectOp: Parser[lang.HyperSelect] = positioned {
       "." ~> Integer ^^ { case i => lang.HyperSelect(i.value.toInt) }
@@ -257,6 +257,7 @@ object UclidParser extends UclidTokenParsers with PackratParsers {
       positioned { ("[" ~> Expr ~ ":" ~ Expr <~ "]") ^^ { case x ~ ":" ~ y => lang.VarExtractOp(lang.VarBitVectorSlice(x, y)) } }
     lazy val ExtractOp : Parser[lang.ExtractOp] = positioned { ConstExtractOp | VarExtractOp }
     lazy val Id: PackratParser[Identifier] = positioned { ident ^^ {case i => Identifier(i)} }
+    lazy val RecordElementId: PackratParser[Identifier] = positioned { ident ^^ {case i => Identifier("rec_"+i)} }
     /* BEGIN Literals. */
     lazy val Bool: PackratParser[BoolLit] =
       positioned { "false" ^^ { _ => BoolLit(false) } | "true" ^^ { _ => BoolLit(true) } }
@@ -402,7 +403,7 @@ object UclidParser extends UclidTokenParsers with PackratParsers {
       ("{" ~> Type ~ rep("," ~> Type) <~ "}") ^^ { case t ~ ts => lang.TupleType(t :: ts) }
     }
     lazy val RecordType : PackratParser[lang.RecordType] = positioned {
-      KwRecord ~> ("{" ~> IdType) ~ rep("," ~> IdType) <~ "}" ^^ { case id ~ ids => lang.RecordType(id::ids) }
+      KwRecord ~> ("{" ~> RecordIdType) ~ rep("," ~> RecordIdType) <~ "}" ^^ { case id ~ ids => lang.RecordType(id::ids) }
     }
     lazy val MapType : PackratParser[lang.MapType] = positioned {
       PrimitiveType ~ rep ("*" ~> PrimitiveType) ~ ("->" ~> Type) ^^ { case t ~ ts ~ rt => lang.MapType(t :: ts, rt)}
@@ -417,6 +418,9 @@ object UclidParser extends UclidTokenParsers with PackratParsers {
     lazy val Type : PackratParser[Type] = positioned {
       MapType | ArrayType | EnumType | TupleType | RecordType | ExternalType | SynonymType | PrimitiveType
     }
+
+    lazy val RecordIdType : PackratParser[(Identifier,Type)] =
+      RecordElementId ~ (":" ~> Type) ^^ { case id ~ typ => (id,typ)}
 
     lazy val IdType : PackratParser[(Identifier,Type)] =
       Id ~ (":" ~> Type) ^^ { case id ~ typ => (id,typ)}

diff --git a/src/test/scala/SMTLIB2Spec.scala b/src/test/scala/SMTLIB2Spec.scala
@@ -155,6 +155,9 @@ class SMTLIB2Spec extends AnyFlatSpec {
   "test-record-1.ucl" should "verify successfully." in {
     SMTLIB2Spec.expectedFails("./test/test-record-1.ucl", 0)
   }
+  "test-record-3.ucl" should "verify successfully." in {
+    SMTLIB2Spec.expectedFails("./test/test-record-1.ucl", 0)
+  }
   "test-tuple-record-1.ucl" should "verify successfully." in {
     SMTLIB2Spec.expectedFails("./test/test-tuple-record-1.ucl", 0)
   }

diff --git a/src/test/scala/VerifierSpec.scala b/src/test/scala/VerifierSpec.scala
@@ -158,6 +158,9 @@ class BasicVerifierSpec extends AnyFlatSpec {
   "test-record-1.ucl" should "verify successfully." in {
     VerifierSpec.expectedFails("./test/test-record-1.ucl", 0)
   }
+  "test-record-3.ucl" should "verify successfully." in {
+    VerifierSpec.expectedFails("./test/test-record-1.ucl", 0)
+  }
   "test-tuple-record-1.ucl" should "verify successfully." in {
     VerifierSpec.expectedFails("./test/test-tuple-record-1.ucl", 0)
   }