Fixing type checking for predicate instance plugin (#835)

Author: marcoeilers

Diff for: src/main/scala/viper/silver/plugin/standard/predicateinstance/PredicateInstancePASTExtension.scala

@@ -22,10 +22,11 @@ case class PPredicateInstance(m: PReserved[PMarkerSymbol.type], idnuse: PIdnRef[
 
   typ = PPrimitiv(PReserved(PPredicateInstanceKeyword)(NoPosition, NoPosition))(NoPosition, NoPosition)
 
-  // TODO: Don't know if this is correct
-  private val _typeSubstitutions = new scala.collection.mutable.ArrayDeque[PTypeSubstitution]()
+  private var _typeSubstitutions = new scala.collection.mutable.ArrayDeque[PTypeSubstitution]()
   final override def typeSubstitutions: mutable.ArrayDeque[PTypeSubstitution] = _typeSubstitutions
-  override def forceSubstitution(ts: PTypeSubstitution): Unit = {}
+  override def forceSubstitution(ts: PTypeSubstitution): Unit = {
+    args.inner.toSeq.foreach(_.forceSubstitution(ts))
+  }
 
   override def typecheck(t: TypeChecker, n: NameAnalyser): Option[Seq[String]] = {
     if (idnuse.decls.isEmpty)
@@ -36,6 +37,7 @@ case class PPredicateInstance(m: PReserved[PMarkerSymbol.type], idnuse: PIdnRef[
       // type checking should be the same as for PPredicateAccess nodes
       val predicateAccess = PCall(idnuse.retype(), args, None)(pos)
       t.checkInternal(predicateAccess)
+      _typeSubstitutions = predicateAccess.typeSubstitutions
       None
     }
   }

Diff for: src/test/resources/all/issues/silver/0835.vpr

@@ -0,0 +1,50 @@
+// Any copyright is dedicated to the Public Domain.
+// http://creativecommons.org/publicdomain/zero/1.0/
+
+
+domain Tuple2[T0, T1]  {
+
+  function get0of2(p: Tuple2[T0, T1]): T0
+
+  function get1of2(p: Tuple2[T0, T1]): T1
+
+  function tuple2(t0: T0, t1: T1): Tuple2[T0, T1]
+
+  axiom getter_over_tuple2 {
+    (forall t0: T0, t1: T1 ::
+      { (tuple2(t0, t1): Tuple2[T0, T1]) }
+      (get0of2((tuple2(t0, t1): Tuple2[T0, T1])): T0) == t0 &&
+      (get1of2((tuple2(t0, t1): Tuple2[T0, T1])): T1) == t1)
+  }
+
+  axiom tuple2_over_getter {
+    (forall p: Tuple2[T0, T1] ::
+      { (get0of2(p): T0) }
+      { (get1of2(p): T1) }
+      (tuple2((get0of2(p): T0), (get1of2(p): T1)): Tuple2[T0, T1]) == p)
+  }
+}
+
+domain Poly[T]  {
+
+  function box_Poly(x: T): Ref
+
+  function unbox_Poly(y: Ref): T
+
+  axiom {
+    (forall x: T ::
+      { (box_Poly(x): Ref) }
+      (unbox_Poly((box_Poly(x): Ref)): T) == x)
+  }
+}
+
+domain Types {
+      function Errno_8b6e126d_T_Types(): Types
+}
+
+function DefinedErrno_8b6e126d_T$$$$_E_$$$_IsDuplicableMem_8b6e126d_MErrno_IsDuplicableMem_ad177c4e_SY$db8f20c_ad177c4e__proof(e_V0: Int): Bool
+  requires acc(dynamic_pred_0((tuple2((box_Poly(e_V0): Ref), Errno_8b6e126d_T_Types()): Tuple2[Ref, Types])), wildcard)
+  decreases dynamic_pred_0((tuple2((box_Poly(e_V0): Ref), Errno_8b6e126d_T_Types()): Tuple2[Ref, Types]))
+
+
+predicate dynamic_pred_0(i: Tuple2[Ref, Types])