Specific errors when struct copy does not work

src/col/vct/col/origin/Blame.scala

@@ -121,11 +121,26 @@ case class ExpectedErrorNotTripped(err: ExpectedError) extends ExpectedErrorFail
   override def inlineDesc: String = s"The expected error with code `${err.errorCode}` was not encountered."
 }
 
-case class AssignFailed(node: SilverFieldAssign[_]) extends NodeVerificationFailure {
+sealed trait AssignFailed extends NodeVerificationFailure
+
+case class AssignFieldFailed(node: SilverFieldAssign[_]) extends AssignFailed with NodeVerificationFailure {
   override def code: String = "assignFieldFailed"
   override def descInContext: String = "Insufficient permission to assign to field."
   override def inlineDescWithSource(source: String): String = s"Insufficient permission for assignment `$source`."
 }
+
+case class CopyStructFailed(node: Expr[_], field: String) extends AssignFailed with NodeVerificationFailure {
+  override def code: String = "copyStructFailed"
+  override def descInContext: String = s"Insufficient read permission for field '$field' to copy struct."
+  override def inlineDescWithSource(source: String): String = s"Insufficient permission for assignment `$source`."
+}
+
+case class CopyStructFailedBeforeCall(node: Expr[_], field: String) extends AssignFailed with FrontendInvocationError with NodeVerificationFailure {
+  override def code: String = "copyStructFailedBeforeCall"
+  override def descInContext: String = s"Insufficient read permission for field '$field' to copy struct before call."
+  override def inlineDescWithSource(source: String): String = s"Insufficient permission for call `$source`."
+}
+
 case class AssertFailed(failure: ContractFailure, node: Assert[_]) extends WithContractFailure {
   override def baseCode: String = "assertFailed"
   override def descInContext: String = "Assertion may not hold, since"

src/rewrite/vct/rewrite/lang/LangCToCol.scala

@@ -60,6 +60,13 @@ case object LangCToCol {
       decl.o.messageInContext(s"This has a struct type that is not supported.")
   }
 
+  case class TypeUsedAsValue(decl: Node[_]) extends UserError {
+    override def code: String = "typeUsedAsValue"
+
+    override def text: String =
+      decl.o.messageInContext(s"This type name is incorrectly used a value.")
+  }
+
   case class WrongGPULocalType(local: CLocalDeclaration[_]) extends UserError {
     override def code: String = "wrongGPULocalType"
     override def text: String =
@@ -139,6 +146,18 @@ case object LangCToCol {
     }
   }
 
+  case class StructCopyFailed(assign: PreAssignExpression[_], field: InstanceField[_]) extends Blame[InsufficientPermission] {
+    override def blame(error: InsufficientPermission): Unit = {
+      assign.blame.blame(CopyStructFailed(assign, Referrable.originName(field)))
+    }
+  }
+
+  case class StructCopyBeforeCallFailed(inv: CInvocation[_], field: InstanceField[_]) extends Blame[InsufficientPermission] {
+    override def blame(error: InsufficientPermission): Unit = {
+      inv.blame.blame(CopyStructFailedBeforeCall(inv, Referrable.originName(field)))
+    }
+  }
+
   case class UnsupportedCast(c: CCast[_]) extends UserError {
     override def code: String = "unsupportedCast"
     override def text: String = c.o.messageInContext("This cast is not supported")
@@ -946,7 +965,11 @@ case class LangCToCol[Pre <: Generation](rw: LangSpecificToCol[Pre]) extends Laz
       case dim: RefCudaVecDim[Pre] => getCuda(dim)
       case struct: RefCStruct[Pre] => ???
       case struct: RefCStructField[Pre] =>
-        val CTStruct(struct_ref) = getBaseType(deref.struct.t)
+        val struct_ref = getBaseType(deref.struct.t) match {
+          case CTStruct(struct_ref) => struct_ref
+          case _: TNotAValue[Pre] => throw TypeUsedAsValue(deref.struct)
+          case _ => ???
+        }
         Deref[Post](rw.dispatch(deref.struct), cStructFieldsSuccessor.ref((struct_ref.decl, struct.decls)))(deref.blame)
     }
   }
@@ -997,7 +1020,7 @@ case class LangCToCol[Pre <: Generation](rw: LangSpecificToCol[Pre]) extends Laz
   }
 
 
-  def createStructCopy(a: Expr[Post], target: CGlobalDeclaration[Pre]): Expr[Post] = {
+  def createStructCopy(a: Expr[Post], target: CGlobalDeclaration[Pre], blame: InstanceField[_] => Blame[InsufficientPermission]): Expr[Post] = {
     implicit val o: Origin = a.o
     val targetClass: Class[Post] = cStructSuccessor(target)
     val t = TClass[Post](targetClass.ref)
@@ -1007,7 +1030,7 @@ case class LangCToCol[Pre <: Generation](rw: LangSpecificToCol[Pre]) extends Laz
       case field: InstanceField[Post] =>
         val ref: Ref[Post, InstanceField[Post]] = field.ref
         // TODO: Pieter, what should I call the blames here? Could not work if did not have enough permission for a to start with.
-        assignField(v.get, ref, Deref[Post](a, field.ref)(PanicBlame("Should work")), PanicBlame("Should work"))
+        assignField(v.get, ref, Deref[Post](a, field.ref)(blame(field)), PanicBlame("Assignment should work"))
     }
 
     With(Block(Seq(LocalDecl(v), assignLocal(v.get, NewObject[Post](targetClass.ref))) ++ fieldAssigns), v.get)
@@ -1016,7 +1039,7 @@ case class LangCToCol[Pre <: Generation](rw: LangSpecificToCol[Pre]) extends Laz
   def assignStruct(assign: PreAssignExpression[Pre]): Expr[Post] = {
     assign.target.t match {
       case CPrimitiveType(Seq(CSpecificationType(CTStruct(ref)))) =>
-        val copy = createStructCopy(rw.dispatch(assign.value), ref.decl)
+        val copy = createStructCopy(rw.dispatch(assign.value), ref.decl, (f: InstanceField[_]) => StructCopyFailed(assign, f))
         PreAssignExpression(rw.dispatch(assign.target), copy)(AssignLocalOk)(assign.o)
       case _ => throw WrongStructType(assign.target)
     }
@@ -1045,7 +1068,7 @@ case class LangCToCol[Pre <: Generation](rw: LangSpecificToCol[Pre]) extends Laz
       a.t match {
         case CPrimitiveType(specs) if specs.collectFirst { case CSpecificationType(_: CTStruct[Pre]) => () }.isDefined =>
           specs match {
-            case Seq(CSpecificationType(CTStruct(ref))) => createStructCopy(rw.dispatch(a), ref.decl)
+            case Seq(CSpecificationType(CTStruct(ref))) => createStructCopy(rw.dispatch(a), ref.decl, (f: InstanceField[_]) => StructCopyBeforeCallFailed(inv, f))
             case _ => throw WrongStructType(a)
           }
         case _ => rw.dispatch(a)

src/viper/viper/api/backend/SilverBackend.scala

@@ -129,7 +129,7 @@ trait SilverBackend extends Backend with LazyLogging {
           case fieldAssign@col.SilverFieldAssign(_, _, _) =>
             reason match {
               case reasons.InsufficientPermission(access) if get[col.Node[_]](access) == fieldAssign =>
-                fieldAssign.blame.blame(blame.AssignFailed(fieldAssign))
+                fieldAssign.blame.blame(blame.AssignFieldFailed(fieldAssign))
               case otherReason =>
                 defer(otherReason)
             }

test/main/vct/test/integration/examples/CSpec.scala

@@ -284,7 +284,7 @@ class CSpec extends VercorsSpec {
     }
     """
 
-  vercors should error withCode "type" in "struct type is again no value" c
+  vercors should error withCode "resolutionError:type" in "struct type is again no value" c
     """
     struct d {
         int x;
@@ -295,4 +295,52 @@ class CSpec extends VercorsSpec {
         s = d;
     }
     """
+
+  vercors should error withCode "typeUsedAsValue" in "Struct deref type is used as value" c
+    """
+    struct d {
+        int x;
+    };
+
+    int main(){
+        struct d s;
+        //@ exhale Perm(d.x, 1\1);
+    }
+    """
+
+  vercors should fail withCode "copyStructFailedBeforeCall" using silicon in "Insufficient permission for field x to copy struct before call" c
+    """
+    struct d {
+        int x;
+    };
+
+
+    int test(struct d t){
+        return 1;
+    }
+
+    int main(){
+        struct d s;
+        //@ exhale Perm(s.x, 1\1);
+        test(s);
+    }
+    """
+
+  vercors should fail withCode "copyStructFailed" using silicon in "Insufficient permission for field x to copy struct before call" c
+    """
+    struct d {
+        int x;
+    };
+
+
+    int test(struct d t){
+        return 1;
+    }
+
+    int main(){
+        struct d s, t;
+        //@ exhale Perm(s.x, 1\1);
+        s = t;
+    }
+    """
 }