Getting blames right for free func

src/col/vct/col/ast/Node.scala

@@ -620,7 +620,7 @@ final case class Select[G](condition: Expr[G], whenTrue: Expr[G], whenFalse: Exp
 final case class NewObject[G](cls: Ref[G, Class[G]])(implicit val o: Origin) extends Expr[G] with NewObjectImpl[G]
 final case class NewArray[G](element: Type[G], dims: Seq[Expr[G]], moreDims: Int, initialize: Boolean)(val blame: Blame[ArraySizeError])(implicit val o: Origin) extends Expr[G] with NewArrayImpl[G]
 final case class NewPointerArray[G](element: Type[G], size: Expr[G])(val blame: Blame[ArraySizeError])(implicit val o: Origin) extends Expr[G] with NewPointerArrayImpl[G]
-final case class FreePointer[G](pointer: Expr[G])(val blame: Blame[InvocationFailure])(implicit val o: Origin) extends Expr[G] with FreePointerImpl[G]
+final case class FreePointer[G](pointer: Expr[G])(val blame: Blame[PointerFreeError])(implicit val o: Origin) extends Expr[G] with FreePointerImpl[G]
 final case class Old[G](expr: Expr[G], at: Option[Ref[G, LabelDecl[G]]])(val blame: Blame[LabelNotReached])(implicit val o: Origin) extends Expr[G] with OldImpl[G]
 final case class AmbiguousSubscript[G](collection: Expr[G], index: Expr[G])(val blame: Blame[FrontendSubscriptError])(implicit val o: Origin) extends Expr[G] with AmbiguousSubscriptImpl[G]
 final case class SeqSubscript[G](seq: Expr[G], index: Expr[G])(val blame: Blame[SeqBoundFailure])(implicit val o: Origin) extends Expr[G] with SeqSubscriptImpl[G]

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

@@ -548,7 +548,33 @@ sealed trait PointerSubscriptError extends FrontendSubscriptError
 sealed trait PointerDerefError extends PointerSubscriptError
 sealed trait PointerLocationError extends PointerDerefError
 sealed trait PointerAddError extends FrontendAdditiveError
-case class PointerNull(node: Expr[_]) extends PointerLocationError with PointerAddError with NodeVerificationFailure {
+sealed trait PointerFreeError extends FrontendInvocationError
+
+case class PointerOffsetNonZero(node: Expr[_]) extends PointerFreeError with NodeVerificationFailure {
+  override def code: String = "ptrOffsetNonZero"
+  override def descInContext: String = "Free can only be called on pointers which are allocated and are at the start of the pointer block."
+  override def inlineDescWithSource(source: String): String = s"Pointer in `$source` cannot be freed due to invalid pointer block."
+}
+
+case class PointerInsufficientFreePermission(node: Expr[_]) extends PointerFreeError with NodeVerificationFailure {
+  override def code: String = "ptrFreePerm"
+  override def descInContext: String = "Not enough permission to free the whole pointer block."
+  override def inlineDescWithSource(source: String): String = s"Pointer in `$source` cannot be freed due to insufficient permission."
+}
+
+case class GenericPointerFreeError(node: Expr[_]) extends PointerFreeError with NodeVerificationFailure {
+  override def code: String = "ptrFreeError"
+  override def descInContext: String = "Pointer block cannot be freed."
+  override def inlineDescWithSource(source: String): String = s"Pointer in `$source` cannot be freed."
+}
+
+case class PointerInsufficientFreeFieldPermission(node: Expr[_], field: String) extends PointerFreeError with NodeVerificationFailure {
+  override def code: String = "ptrFreeFieldError"
+  override def descInContext: String = s"Not enough permission to free the whole pointer block, since we miss permission for field `$field`"
+  override def inlineDescWithSource(source: String): String = s"Pointer in `$source` cannot be freed."
+}
+
+case class PointerNull(node: Expr[_]) extends PointerLocationError with PointerAddError with PointerFreeError with NodeVerificationFailure {
   override def code: String = "ptrNull"
   override def descInContext: String = "Pointer may be null."
   override def inlineDescWithSource(source: String): String = s"Pointer in `$source` may be null."

src/col/vct/col/typerules/CoercingRewriter.scala

@@ -231,7 +231,6 @@ abstract class CoercingRewriter[Pre <: Generation]() extends AbstractRewriter[Pr
     case node: IterVariable[Pre] => node
     case node: CDeclaration[Pre] => node
     case node: CDeclarator[Pre] => node
-    case node: CDeclaration[Pre] => node
     case node: CDeclarationSpecifier[Pre] => node
     case node: CTypeQualifier[Pre] => node
     case node: CPointer[Pre] => node

src/col/vct/col/util/AstBuildHelpers.scala

@@ -472,6 +472,11 @@ object AstBuildHelpers {
     case SplitAccountedPredicate(left, right) => Star(foldStar(left), foldStar(right))
   }
 
+  def foldPredicate[G](exprs: Seq[Expr[G]])(implicit o: Origin): AccountedPredicate[G] = exprs match {
+    case x :: Seq() => UnitAccountedPredicate(x)
+    case x :: xs => SplitAccountedPredicate(UnitAccountedPredicate(x), foldPredicate(xs))
+  }
+
   def foldOr[G](exprs: Seq[Expr[G]])(implicit o: Origin): Expr[G] =
     exprs.reduceOption(Or(_, _)).getOrElse(ff)
 }

src/rewrite/vct/rewrite/EncodeArrayValues.scala

@@ -2,7 +2,6 @@ package vct.col.rewrite
 
 import hre.util.FuncTools
 import vct.col.ast.{Expr, _}
-import vct.col.rewrite.error.ExtraNode
 import vct.col.origin._
 import vct.col.resolve.lang.Java
 import vct.rewrite.lang.LangCToCol.UnsupportedStructPerm
@@ -56,6 +55,20 @@ case object EncodeArrayValues extends RewriterBuilder {
       case other => throw Unreachable(s"Invalid invocation failure: $other")
     }
   }
+
+  case class PointerFreeFailed[G](free: FreePointer[G], errors: Seq[Expr[G] =>  PointerFreeError]) extends Blame[InvocationFailure] {
+    override def blame(error: InvocationFailure): Unit = error match {
+      case PreconditionFailed(path, _, _) => blame_searcher(path, errors)
+      case other => throw Unreachable(s"Invalid invocation failure: $other")
+    }
+
+    def blame_searcher(path: Seq[AccountedDirection], errors: Seq[Expr[G] =>  PointerFreeError]): Unit = (path, errors) match {
+      case (Seq(FailLeft), e :: _) => free.blame.blame(e(free.pointer))
+      case (Seq(FailRight), _ :: e :: _) => free.blame.blame(e(free.pointer))
+      case (FailRight :: pathTail, _ :: errorsTail) => blame_searcher(pathTail, errorsTail)
+      case _ => throw Unreachable(s"Invalid invocation failure for free")
+    }
+  }
 }
 
 case class EncodeArrayValues[Pre <: Generation]() extends Rewriter[Pre] {
@@ -67,12 +80,13 @@ case class EncodeArrayValues[Pre <: Generation]() extends Rewriter[Pre] {
 
   val pointerArrayCreationMethods: mutable.Map[Type[Pre], Procedure[Post]] = mutable.Map()
 
-  val freeMethods: mutable.Map[Type[Post], Procedure[Post]] = mutable.Map()
+  val freeMethods: mutable.Map[Type[Post], (Procedure[Post], FreePointer[Pre] => PointerFreeFailed[Pre])] = mutable.Map()
 
-  def makeFree(t: Type[Post]): Procedure[Post] = {
+  def makeFree(t: Type[Post]): (Procedure[Post], FreePointer[Pre] => PointerFreeFailed[Pre])  = {
     implicit val o: Origin = freeFuncOrigin
+    var errors: Seq[Expr[Pre] => PointerFreeError] = Seq()
 
-    globalDeclarations.declare({
+    val proc = globalDeclarations.declare({
       val (vars, ptr) = variables.collect {
         val a_var = new Variable[Post](TPointer(t))(o.where(name= "p"))
         variables.declare(a_var)
@@ -96,18 +110,29 @@ case class EncodeArrayValues[Pre <: Generation]() extends Rewriter[Pre] {
         requires (\forall* int i; 0 <= i && i < \pointer_block_length(ptr); Perm(ptr[i], write));
         (and recurse for struct fields)
        */
+      var requiresT: Seq[(Expr[Post], Expr[Pre] => PointerFreeError)] =
+        Seq(
+          (ptr !== Null(), (p: Expr[Pre]) => PointerNull(p)),
+          (PointerBlockOffset(ptr)(FramedPtrBlockOffset) === zero, (p: Expr[Pre]) => PointerOffsetNonZero(p)),
+          (makeStruct.makePerm(i => PointerLocation(PointerAdd(ptr, i.get)(FramedPtrOffset))(FramedPtrOffset),
+              IteratedPtrInjective), (p: Expr[Pre]) => PointerInsufficientFreePermission(p))
+        )
       var requires = (ptr !== Null()) &*
         (PointerBlockOffset(ptr)(FramedPtrBlockOffset) === zero) &*
-        makeStruct.makePerm(i => PointerLocation(PointerAdd(ptr, i.get)(FramedPtrOffset))(FramedPtrOffset))
-      requires = if (!typeIsRef(t)) requires else {
-        requires &* makeStruct.makeUnique(access)
+        makeStruct.makePerm(i => PointerLocation(PointerAdd(ptr, i.get)(FramedPtrOffset))(FramedPtrOffset),
+          IteratedPtrInjective)
+      requiresT = if (!typeIsRef(t)) requiresT else {
+        // I think this error actually can never happen, since we require full write permission already
+        requiresT :+ (makeStruct.makeUnique(access), (p: Expr[Pre]) => GenericPointerFreeError(p))
       }
       // If structure contains structs, the permission for those fields need to be released as well
       val permFields = t match {
         case t: TClass[Post] => unwrapStructPerm(access, t, o, makeStruct)
         case _ => Seq()
       }
-      requires = if (permFields.isEmpty) requires else requires &* foldStar(permFields)
+      requiresT = if (permFields.isEmpty) requiresT else requiresT ++ permFields
+      val requiresPred = foldPredicate(requiresT.map(_._1))
+      errors = requiresT.map(_._2)
 
       procedure(
         blame = AbstractApplicable,
@@ -117,12 +142,11 @@ case class EncodeArrayValues[Pre <: Generation]() extends Rewriter[Pre] {
         outArgs = Nil,
         typeArgs = Nil,
         body = None,
-        requires = UnitAccountedPredicate(
-          requires
-        ),
+        requires = requiresPred,
         decreases = Some(DecreasesClauseNoRecursion[Post]())
       )(o.where("free_" + t.toString))
     })
+    (proc, (node: FreePointer[Pre]) => PointerFreeFailed(node, errors))
   }
 
   def makeFunctionFor(arrayType: TArray[Pre]): Function[Post] = {
@@ -235,19 +259,23 @@ case class EncodeArrayValues[Pre <: Generation]() extends Rewriter[Pre] {
     }))
   }
 
-  def unwrapStructPerm(struct: Variable[Post] => Expr[Post], structType: TClass[Post], origin: Origin, makeStruct: MakeAnns, visited: Seq[TClass[Post]] = Seq()): Seq[Expr[Post]] = {
+  def unwrapStructPerm(struct: Variable[Post] => Expr[Post], structType: TClass[Post], origin: Origin,
+                       makeStruct: MakeAnns, visited: Seq[TClass[Post]] = Seq()): Seq[(Expr[Post], Expr[Pre] => PointerFreeError)] = {
     if (visited.contains(structType)) throw UnsupportedStructPerm(origin) // We do not allow this notation for recursive structs
     implicit val o: Origin = origin
-    val blame = PanicBlame("Cannot Fail")
 
     val fields = structType match {
       case TClass(ref) => ref.decl.declarations.collect { case field: InstanceField[Post] => field }
       case _ => Seq()
     }
     val newFieldPerms = fields.map(member => {
-      val loc = (i: Variable[Post]) => Deref[Post](struct(i), member.ref)(blame)
-      var anns = Seq(makeStruct.makePerm(i => FieldLocation[Post](struct(i), member.ref)))
-      anns = if(typeIsRef(member.t)) anns ++ Seq(makeStruct.makeUnique(loc)) else anns
+      val loc = (i: Variable[Post]) => Deref[Post](struct(i), member.ref)(DerefPerm)
+      var anns : Seq[(Expr[Post], Expr[Pre] => PointerFreeError)] =
+        Seq((makeStruct.makePerm(i => FieldLocation[Post](struct(i), member.ref), IteratedPtrInjective),
+          (p: Expr[Pre]) => PointerInsufficientFreeFieldPermission(p, member.toInlineString)))
+      anns = if(typeIsRef(member.t))
+          anns :+ (makeStruct.makeUnique(loc), (p: Expr[Pre]) => GenericPointerFreeError(p))
+        else anns
       member.t match {
         case newStruct: TClass[Post] =>
           // We recurse, since a field is another struct
@@ -260,9 +288,8 @@ case class EncodeArrayValues[Pre <: Generation]() extends Rewriter[Pre] {
   }
 
   case class MakeAnns(i: Variable[Post], j: Variable[Post], size: Expr[Post], trigger: Expr[Post], triggerUnique: Seq[Expr[Post]]){
-    def makePerm(location: Variable[Post] => Location[Post]): Expr[Post] = {
+    def makePerm(location: Variable[Post] => Location[Post], blame: Blame[ReceiverNotInjective]): Expr[Post] = {
       implicit val o: Origin = arrayCreationOrigin
-      val blame = PanicBlame("Already checked")
       val zero =  const[Post](0)
       val body = (zero <= i.get && i.get < size) ==> Perm(location(i), WritePerm[Post]())
       Starall(Seq(i), Seq(Seq(trigger)), body)(blame)
@@ -306,7 +333,7 @@ case class EncodeArrayValues[Pre <: Generation]() extends Rewriter[Pre] {
         (PointerBlockLength(result)(FramedPtrBlockLength) === sizeArg.get) &*
         (PointerBlockOffset(result)(FramedPtrBlockOffset) === zero)
       // Pointer location needs pointer add, not pointer subscript
-      ensures = ensures &* makeStruct.makePerm(i => PointerLocation(PointerAdd(result, i.get)(FramedPtrOffset))(FramedPtrOffset))
+      ensures = ensures &* makeStruct.makePerm(i => PointerLocation(PointerAdd(result, i.get)(FramedPtrOffset))(FramedPtrOffset), IteratedPtrInjective)
       ensures = if (!typeIsRef(elementType)) ensures else {
         ensures &* makeStruct.makeUnique(access)
       }
@@ -316,7 +343,7 @@ case class EncodeArrayValues[Pre <: Generation]() extends Rewriter[Pre] {
         case _ => Seq()
       }
 
-      ensures = if (permFields.isEmpty) ensures else ensures &* foldStar(permFields)
+      ensures = if (permFields.isEmpty) ensures else ensures &* foldStar(permFields.map(_._1))
 
       procedure(
         blame = AbstractApplicable,
@@ -345,8 +372,8 @@ case class EncodeArrayValues[Pre <: Generation]() extends Rewriter[Pre] {
       case free @ FreePointer(xs) =>
         val newXs = dispatch (xs)
         val TPointer(t) = newXs.t
-        val freeFunc = freeMethods.getOrElseUpdate (t, makeFree(t))
-        ProcedureInvocation[Post](freeFunc.ref, Seq (newXs), Nil, Nil, Nil, Nil) (free.blame)(free.o)
+        val (freeFunc, freeBlame) = freeMethods.getOrElseUpdate (t, makeFree(t))
+        ProcedureInvocation[Post](freeFunc.ref, Seq (newXs), Nil, Nil, Nil, Nil) (freeBlame(free))(free.o)
       case other => rewriteDefault(other)
     }
   }

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

@@ -16,24 +16,65 @@ class CSpec extends VercorsSpec {
   }
   """
   vercors should fail withCode "assignFieldFailed" using silicon in "cannot access field of struct after freeing" c
-  """
-  #include <stdlib.h>
+    """
+    #include <stdlib.h>
 
-  struct d{
-    int x;
-  };
+    struct d{
+      int x;
+    };
 
-  struct e{
-    struct d s;
-    int x;
-  };
+    struct e{
+      struct d s;
+      int x;
+    };
 
-  int main(){
-    struct e* a = (struct e*) malloc(1*sizeof(struct e));
-    a->s.x = 1;
-    struct d* b = &(a->s);
-    free(a);
-    b->x = 2;
-  }
-  """
+    int main(){
+      struct e* a = (struct e*) malloc(1*sizeof(struct e));
+      a->s.x = 1;
+      struct d* b = &(a->s);
+      free(a);
+      b->x = 2;
+    }
+    """
+
+  vercors should fail withCode "ptrNull" using silicon in "free null pointer" c
+    """
+      #include <stdlib.h>
+      int main(){
+          int* xs;
+          free(xs);
+      }
+    """
+
+  vercors should fail withCode "ptrOffsetNonZero" using silicon in "free null pointer" c
+    """
+      #include <stdlib.h>
+      int main(){
+          int* xs = (int*) malloc(sizeof(int)*3);
+          free(xs+1);
+      }
+    """
+
+  vercors should fail withCode "ptrFreePerm" using silicon in "free pointer with insufficient permission" c
+    """
+      #include <stdlib.h>
+      int main(){
+          int* xs = (int*) malloc(sizeof(int)*3);
+          //@ exhale Perm(&xs[0], 1\2);
+          free(xs);
+      }
+    """
+  vercors should fail withCode "ptrFreeFieldError" using silicon in "free pointer with insufficient permission for field" c
+    """
+    #include <stdlib.h>
+    struct d{
+     int x;
+    };
+    int main(){
+        struct d* xs = (struct d*) malloc(sizeof(struct d)*3);
+        struct d* ys = (struct d*) malloc(sizeof(struct d)*3);
+        //@ exhale Perm(xs[0].x, 1\2);
+        free(xs);
+    }
+    """
 }