From f6fbefa927c4429247b8876fe245a480ea4593c1 Mon Sep 17 00:00:00 2001
From: Pointerbender <pointerbender@gmail.com>
Date: Fri, 27 May 2022 18:03:58 +0200
Subject: [PATCH] fixed another corner case with regression test #581

---
 .../standard/adt/AdtPASTExtension.scala       | 24 ++++++++++++++++++-
 .../plugin/standard/adt/AdtPlugin.scala       | 11 +++++++++
 src/test/resources/adt/issue-581.vpr          | 14 +++++++++++
 3 files changed, 48 insertions(+), 1 deletion(-)

diff --git a/src/main/scala/viper/silver/plugin/standard/adt/AdtPASTExtension.scala b/src/main/scala/viper/silver/plugin/standard/adt/AdtPASTExtension.scala
index 6ab0a3a86..831057ebf 100644
--- a/src/main/scala/viper/silver/plugin/standard/adt/AdtPASTExtension.scala
+++ b/src/main/scala/viper/silver/plugin/standard/adt/AdtPASTExtension.scala
@@ -515,4 +515,26 @@ case class PDiscriminatorCall(name: PIdnUse, rcv: PExp)
       case _ => sys.error("type unification error - should report and not crash")
     }
   }
-}
\ No newline at end of file
+}
+
+case class PAdtResultLit(adt: PIdnUse, args: Seq[PType])(val pos: (Position, Position)) extends PExtender with PExp {
+  // These two function must be mandatorily extended due to semantic analysis rules
+  override final val typeSubstitutions = Seq(PTypeSubstitution.id)
+  override def forceSubstitution(ts: PTypeSubstitution) = {}
+
+  override def getSubnodes(): Seq[PNode] = Seq(adt) ++ args
+
+  // The typecheck funtion for PAst node corresponding to the expression
+  override def typecheck(t: TypeChecker, n: NameAnalyser): Option[Seq[String]] = None
+
+  // The translator function to translate the PAst node corresponding to the Ast node
+  override def translateExp(t: Translator): Exp = {
+    t.getMembers().get(adt.name) match {
+      case Some(d) =>
+        val adt = d.asInstanceOf[Adt]
+        val typVarMapping = adt.typVars zip (args map t.ttyp)
+        Result(AdtType(adt, typVarMapping.toMap))(t.liftPos(this))
+      case None => sys.error("undeclared adt type")
+    }
+  }
+}
diff --git a/src/main/scala/viper/silver/plugin/standard/adt/AdtPlugin.scala b/src/main/scala/viper/silver/plugin/standard/adt/AdtPlugin.scala
index 19091f525..066b8eb0a 100644
--- a/src/main/scala/viper/silver/plugin/standard/adt/AdtPlugin.scala
+++ b/src/main/scala/viper/silver/plugin/standard/adt/AdtPlugin.scala
@@ -119,6 +119,17 @@ class AdtPlugin(reporter: viper.silver.reporter.Reporter,
         PFieldAssign(PFieldAccess(transformStrategy(fieldAcc.rcv), fieldAcc.idnuse)(fieldAcc.pos), transformStrategy(rhs))(pfa.pos)
       case pfa@PFieldAccess(rcv, idnuse) if declaredConstructorArgsNames.exists(_.name == idnuse.name) => PDestructorCall(idnuse.name, rcv)(pfa.pos)
       case pfa@PFieldAccess(rcv, idnuse) if declaredConstructorNames.exists("is" + _.name == idnuse.name) => PDiscriminatorCall(PIdnUse(idnuse.name.substring(2))(idnuse.pos), rcv)(pfa.pos)
+      case pr@PResultLit() => {
+        var parent = pr.parent.get
+        while (!parent.isInstanceOf[PFunction] && !parent.isInstanceOf[PFieldAccess] && !parent.isInstanceOf[PDestructorCall] && !parent.isInstanceOf[PDiscriminatorCall]) {
+          if (parent == null) sys.error("cannot use 'result' outside of function")
+          parent = parent.parent.get
+        }
+        parent match {
+          case pf@PFunction(_, _, typ@PDomainType(idnuse, args), _, _, _) if declaredAdtNames.exists(_.name == idnuse.name) => PAdtResultLit(idnuse, args)(pr.pos)
+          case _ => pr
+        }
+      }
     }).recurseFunc({
       // Stop the recursion if a destructor call or discriminator call is parsed as left-hand side of a field assignment
       case PFieldAssign(fieldAcc, _) if declaredConstructorArgsNames.exists(_.name == fieldAcc.idnuse.name) ||
diff --git a/src/test/resources/adt/issue-581.vpr b/src/test/resources/adt/issue-581.vpr
index 73beb244b..4a5c7e4ca 100644
--- a/src/test/resources/adt/issue-581.vpr
+++ b/src/test/resources/adt/issue-581.vpr
@@ -12,6 +12,20 @@ function foo(): Test
 function bar(): Test
     ensures result.isB
     ensures result.b == 42
+    ensures inv(result)
 {
     B(42)
 }
+
+function inv(t: Test): Bool {
+    t.isB && t.b > 10
+}
+
+// FIXME: this triggers an error: [typechecker.error] expected identifier, but got PAdtConstructor(PIdnDef(A),List())
+// FIXME: see https://github.com/viperproject/silver/issues/581
+// function baz(): Test
+//     ensures A() == result
+//     // ensures result == A()
+// {
+//     A
+// }