Allow casting back up to "greater" type

utwente-fmt · Sep 17, 2024 · bede2fc · bede2fc
1 parent 72cb421
commit bede2fc
Show file tree

Hide file tree

Showing 4 changed files with 81 additions and 27 deletions.
diff --git a/src/rewrite/vct/rewrite/ClassToRef.scala b/src/rewrite/vct/rewrite/ClassToRef.scala
@@ -712,30 +712,48 @@ case class ClassToRef[Pre <: Generation]() extends Rewriter[Pre] {
       implicit o: Origin
   ): Expr[Post] = {
     val newT = dispatch(t)
-    val constraint = forall[Post](
-      TNonNullPointer(outerType),
-      body = { p =>
-        PolarityDependent(
-          Greater(
-            CurPerm(PointerLocation(p)(PanicBlame(
-              "Referring to a non-null pointer should not cause any verification failures"
-            ))),
-            NoPerm(),
-          ) ==>
-            (InlinePattern(Cast(p, TypeValue(TNonNullPointer(newT)))) ===
-              adtFunctionInvocation(
-                valueAsFunctions
-                  .getOrElseUpdate(t, makeValueAsFunction(t.toString, newT))
-                  .ref,
-                typeArgs = Some((valueAdt.ref(()), Seq(outerType))),
-                args = Seq(DerefPointer(p)(PanicBlame(
-                  "Pointer deref is safe since the permission is framed"
-                ))),
-              )),
-          tt,
-        )
-      },
-    )
+    val constraint =
+      forall[Post](
+        TNonNullPointer(outerType),
+        body = { p =>
+          PolarityDependent(
+            Greater(
+              CurPerm(PointerLocation(p)(PanicBlame(
+                "Referring to a non-null pointer should not cause any verification failures"
+              ))),
+              NoPerm(),
+            ) ==>
+              (InlinePattern(Cast(p, TypeValue(TNonNullPointer(newT)))) ===
+                adtFunctionInvocation(
+                  valueAsFunctions
+                    .getOrElseUpdate(t, makeValueAsFunction(t.toString, newT))
+                    .ref,
+                  typeArgs = Some((valueAdt.ref(()), Seq(outerType))),
+                  args = Seq(DerefPointer(p)(PanicBlame(
+                    "Pointer deref is safe since the permission is framed"
+                  ))),
+                )),
+            tt,
+          )
+        },
+      ) &* forall[Post](
+        TNonNullPointer(outerType),
+        body = { p =>
+          PolarityDependent(
+            Greater(
+              CurPerm(PointerLocation(p)(PanicBlame(
+                "Referring to a non-null pointer should not cause any verification failures"
+              ))),
+              NoPerm(),
+            ) ==>
+              (InlinePattern(Cast(
+                Cast(p, TypeValue(TNonNullPointer(newT))),
+                TypeValue(TNonNullPointer(outerType)),
+              )) === p),
+            tt,
+          )
+        },
+      )
 
     if (t.isInstanceOf[TByValueClass[Pre]]) {
       constraint &*

diff --git a/src/rewrite/vct/rewrite/DisambiguateLocation.scala b/src/rewrite/vct/rewrite/DisambiguateLocation.scala
@@ -2,8 +2,17 @@ package vct.col.rewrite
 
 import vct.col.ast._
 import vct.col.rewrite.DisambiguateLocation.NotALocation
-import vct.col.origin.{Blame, Origin, PointerLocationError}
+import vct.col.origin.{
+  Blame,
+  Origin,
+  PanicBlame,
+  PointerAddError,
+  PointerBounds,
+  PointerLocationError,
+  PointerNull,
+}
 import vct.col.rewrite.{Generation, Rewriter, RewriterBuilder}
+import vct.col.util.AstBuildHelpers.const
 import vct.result.VerificationError.UserError
 
 case object DisambiguateLocation extends RewriterBuilder {
@@ -25,19 +34,43 @@ case object DisambiguateLocation extends RewriterBuilder {
         "This expression is not a heap location." + hint.getOrElse("")
       )
   }
+
+  case class PointerAddRedirect(blame: Blame[PointerLocationError])
+      extends Blame[PointerAddError] {
+    override def blame(error: PointerAddError): Unit =
+      error match {
+        case nil: PointerNull => blame.blame(nil)
+        // It should not be possible to acquire an out-of-bounds pointer and pass it around
+        case bounds: PointerBounds =>
+          PanicBlame("Got location of pointer that was out of bounds")
+      }
+  }
+
   override def key: String = "disambiguateLocation"
 
   override def desc: String =
     "Translate ambiguous location type into concrete location type."
 }
 
 case class DisambiguateLocation[Pre <: Generation]() extends Rewriter[Pre] {
+  import DisambiguateLocation._
+
   def exprToLoc(expr: Expr[Pre], blame: Blame[PointerLocationError])(
       implicit o: Origin
   ): Location[Post] =
     expr match {
       case expr if expr.t.asPointer.isDefined =>
-        PointerLocation(dispatch(expr))(blame)
+        expr match {
+          case e: PointerAdd[Pre] => PointerLocation(dispatch(e))(blame)
+          // Adding ptr + 0 for triggering purposes (is there a better place to do this transformation?)
+          case e =>
+            PointerLocation(
+              PointerAdd[Post](dispatch(e), const[Post](0))(PointerAddRedirect(
+                blame
+              ))
+            )(blame)
+        }
+
       case expr if expr.t.isInstanceOf[TByValueClass[Pre]] =>
         ByValueClassLocation(dispatch(expr))(blame)
       case DerefHeapVariable(ref) => HeapVariableLocation(succ(ref.decl))

diff --git a/src/rewrite/vct/rewrite/lang/LangCToCol.scala b/src/rewrite/vct/rewrite/lang/LangCToCol.scala
@@ -420,6 +420,9 @@ case class LangCToCol[Pre <: Generation](rw: LangSpecificToCol[Pre])
           CoercionUtils.firstElementIsType(
             newE.t.asPointer.get.element,
             newT.asPointer.get.element,
+          ) || CoercionUtils.firstElementIsType(
+            newT.asPointer.get.element,
+            newE.t.asPointer.get.element,
           )
         ) { Cast(newE, TypeValue(newT)(t.o))(c.o) }
         else { throw UnsupportedCast(c) }

diff --git a/src/viper/viper/api/transform/SilverToCol.scala b/src/viper/viper/api/transform/SilverToCol.scala
@@ -559,7 +559,7 @@ case class SilverToCol[G](
 
       case silver.ForPerm(variables, resource, body) => ??(e)
       case silver.EpsilonPerm() => ??(e)
-      case silver.InhaleExhaleExp(in, ex) => ??(e)
+      case silver.InhaleExhaleExp(in, ex) => col.PolarityDependent(f(in), f(ex))
       case silver.MagicWand(left, right) => ??(e)
       case silver.Applying(wand, body) => ??(e)
       case silver.BackendFuncApp(backendFunc, args) => ??(e)