Fix unsoundness in pointer cast encoding

utwente-fmt · Sep 13, 2024 · 72cb421 · 72cb421
1 parent 55b69e3
commit 72cb421
Showing 1 changed file with 15 additions and 7 deletions.
diff --git a/src/rewrite/vct/rewrite/ClassToRef.scala b/src/rewrite/vct/rewrite/ClassToRef.scala
@@ -377,7 +377,6 @@ case class ClassToRef[Pre <: Generation]() extends Rewriter[Pre] {
           case cls: ByValueClass[Pre] =>
             implicit val o: Origin = cls.o
             val axiomType = TAxiomatic[Post](byValClassSucc.ref(cls), Nil)
-            val classType = cls.classType(Nil)
             var valueAsAxioms: Seq[ADTAxiom[Post]] = Seq()
             val (fieldFunctions, fieldInverses, fieldTypes) =
               cls.decls.collect { case field: Field[Pre] =>
@@ -409,12 +408,21 @@ case class ClassToRef[Pre <: Generation]() extends Rewriter[Pre] {
                     ))
 
                   valueAsAxioms =
-                    valueAsAxioms ++ unwrapValueAs(
-                      axiomType,
-                      field.t,
-                      newT,
-                      byValFieldSucc.ref(field),
-                    )
+                    valueAsAxioms ++
+                      (field.t match {
+                        case t: TByValueClass[Pre] =>
+                          // TODO: If there are no fields we should ignore the first field and add the axioms for the second field
+                          t.cls.decl.decls
+                            .collectFirst({ case innerF: InstanceField[Pre] =>
+                              unwrapValueAs(
+                                axiomType,
+                                innerF.t,
+                                dispatch(innerF.t),
+                                byValFieldSucc.ref(field),
+                              )
+                            }).getOrElse(Nil)
+                        case _ => Nil
+                      })
                 }
                 (
                   byValFieldSucc(field),