Merge remote-tracking branch 'origin/dev' into pallas

examples/concepts/c/malloc_free.c

@@ -13,31 +13,39 @@ struct e{
 
 int main(){
     int* xs = (int*) malloc(sizeof(int)*3);
+    if (xs == NULL) return 1;
 
     xs[0] = 3;
     xs[1] = 2;
     xs[2] = 1;
     free(xs);
 
     int** xxs = (int * *) malloc(sizeof(int *)*3);
+    if (xxs == NULL) return 1;
 
     int temp[3] = {1,2,3};
     xxs[0] = temp;
     assert(xxs[0][0] == 1);
     free(xxs);
 
     struct d* ys = (struct d*) malloc(3*sizeof(struct d));
+    if (ys == NULL) return 1;
+
     ys[0].x = 3;
     ys[1].x = 2;
     ys[2].x = 1;
     free(ys);
 
     struct e* a = (struct e*) malloc(1*sizeof(struct e));
+    if (a == NULL) return 1;
+
     a->s.x = 1;
     struct d* b = &(a->s);
     free(a);
 
     float * z = (float *) malloc(sizeof(float));
+    if (z == NULL) return 1;
+
     z[0] = 3.0;
     *z = 2.0;
     free(z);

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

@@ -1892,9 +1892,11 @@ final case class NewArray[G](
     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)
+final case class NewPointerArray[G](
+    element: Type[G],
+    size: Expr[G],
+    fallible: Boolean,
+)(val blame: Blame[ArraySizeError])(implicit val o: Origin)
     extends Expr[G] with NewPointerArrayImpl[G]
 final case class NewNonNullPointerArray[G](element: Type[G], size: Expr[G])(
     val blame: Blame[ArraySizeError]

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

@@ -1569,8 +1569,8 @@ abstract class CoercingRewriter[Pre <: Generation]()
         Neq(coerce(left, sharedType), coerce(right, sharedType))
       case na @ NewArray(element, dims, moreDims, initialize) =>
         NewArray(element, dims.map(int), moreDims, initialize)(na.blame)
-      case na @ NewPointerArray(element, size) =>
-        NewPointerArray(element, size)(na.blame)
+      case na @ NewPointerArray(element, size, fallible) =>
+        NewPointerArray(element, size, fallible)(na.blame)
       case na @ NewNonNullPointerArray(element, size) =>
         NewNonNullPointerArray(element, size)(na.blame)
       case NewObject(cls) => NewObject(cls)

src/rewrite/vct/rewrite/EncodeArrayValues.scala

@@ -106,7 +106,7 @@ case class EncodeArrayValues[Pre <: Generation]() extends Rewriter[Pre] {
       : mutable.Map[(Type[Pre], Int, Int, Boolean), Procedure[Post]] = mutable
     .Map()
 
-  val pointerArrayCreationMethods: mutable.Map[Type[Pre], Procedure[Post]] =
+  val pointerArrayCreationMethods: mutable.Map[(Type[Pre], Boolean), Procedure[Post]] =
     mutable.Map()
   val nonNullPointerArrayCreationMethods
       : mutable.Map[Type[Pre], Procedure[Post]] = mutable.Map()
@@ -496,10 +496,11 @@ case class EncodeArrayValues[Pre <: Generation]() extends Rewriter[Pre] {
   def makePointerCreationMethodFor(
       elementType: Type[Pre],
       nullable: Boolean,
+      fallible: Boolean,
   ) = {
     implicit val o: Origin = arrayCreationOrigin
-    // ar != null
-    // ar.length == dim0
+    // fallible? then 'ar != null ==> ...'; otherwise 'ar != null ** ...'
+    // ar.length == size
     // forall ar[i] :: Perm(ar[i], write)
     // (if type ar[i] is pointer or struct):
     // forall i,j :: i!=j ==> ar[i] != ar[j]
@@ -554,6 +555,12 @@ case class EncodeArrayValues[Pre <: Generation]() extends Rewriter[Pre] {
         else
           ensures &* foldStar(permFields.map(_._1))
 
+      ensures =
+        if (!fallible)
+          (result !== Null()) &* ensures
+        else
+          Star(Implies(result !== Null(), ensures), tt)
+
       procedure(
         blame = AbstractApplicable,
         contractBlame = TrueSatisfiable,
@@ -563,7 +570,7 @@ case class EncodeArrayValues[Pre <: Generation]() extends Rewriter[Pre] {
         args = Seq(sizeArg),
         requires = UnitAccountedPredicate(requires),
         ensures = UnitAccountedPredicate(ensures),
-      )(o.where(name = "make_pointer_array_" + elementType.toString))
+      )(o.where(name = "make_pointer_array_" + elementType.toString + (if (fallible) "_fallible" else "")))
     }))
   }
 
@@ -594,10 +601,10 @@ case class EncodeArrayValues[Pre <: Generation]() extends Rewriter[Pre] {
           Nil,
           Nil,
         )(ArrayCreationFailed(newArr))
-      case newPointerArr @ NewPointerArray(element, size) =>
+      case newPointerArr @ NewPointerArray(element, size, fallible) =>
         val method = pointerArrayCreationMethods.getOrElseUpdate(
-          element,
-          makePointerCreationMethodFor(element, nullable = true),
+          (element, fallible),
+          makePointerCreationMethodFor(element, nullable = true, fallible=fallible),
         )
         ProcedureInvocation[Post](
           method.ref,
@@ -610,7 +617,7 @@ case class EncodeArrayValues[Pre <: Generation]() extends Rewriter[Pre] {
       case newPointerArr @ NewNonNullPointerArray(element, size) =>
         val method = nonNullPointerArrayCreationMethods.getOrElseUpdate(
           element,
-          makePointerCreationMethodFor(element, nullable = false),
+          makePointerCreationMethodFor(element, nullable = false, fallible=false),
         )
         ProcedureInvocation[Post](
           method.ref,

src/rewrite/vct/rewrite/TrivialAddrOf.scala

@@ -103,7 +103,7 @@ case class TrivialAddrOf[Pre <: Generation]() extends Rewriter[Pre] {
     val newPointer = Eval(
       PreAssignExpression(
         newTarget,
-        NewPointerArray(newValue.t, const[Post](1))(PanicBlame("Size is > 0")),
+        NewPointerArray(newValue.t, const[Post](1), fallible=false)(PanicBlame("Size is > 0")),
       )(blame)
     )
     (newPointer, newTarget, newValue)

src/rewrite/vct/rewrite/lang/LangCPPToCol.scala

@@ -2740,11 +2740,11 @@ case class LangCPPToCol[Pre <: Generation](rw: LangSpecificToCol[Pre])
         (sizeOption, init.init) match {
           case (None, None) => throw WrongCPPType(decl)
           case (Some(size), None) =>
-            val newArr = NewPointerArray[Post](t, rw.dispatch(size))(cta.blame)
+            val newArr = NewPointerArray[Post](t, rw.dispatch(size), fallible=false)(cta.blame)
             Block(Seq(LocalDecl(v), assignLocal(v.get, newArr)))
           case (None, Some(CPPLiteralArray(exprs))) =>
             val newArr =
-              NewPointerArray[Post](t, c_const[Post](exprs.size))(cta.blame)
+              NewPointerArray[Post](t, c_const[Post](exprs.size), fallible=false)(cta.blame)
             Block(
               Seq(LocalDecl(v), assignLocal(v.get, newArr)) ++
                 assignliteralArray(v, exprs, o)
@@ -2755,7 +2755,7 @@ case class LangCPPToCol[Pre <: Generation](rw: LangSpecificToCol[Pre])
             if (realSize < exprs.size)
               logger.warn(s"Excess elements in array initializer: '${decl}'")
             val newArr =
-              NewPointerArray[Post](t, c_const[Post](realSize))(cta.blame)
+              NewPointerArray[Post](t, c_const[Post](realSize), fallible=false)(cta.blame)
             Block(
               Seq(LocalDecl(v), assignLocal(v.get, newArr)) ++
                 assignliteralArray(v, exprs.take(realSize.intValue), o)

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

@@ -409,7 +409,7 @@ case class LangCToCol[Pre <: Generation](rw: LangSpecificToCol[Pre])
               (t1, rw.dispatch(r))
             case _ => throw UnsupportedMalloc(c)
           }
-        NewPointerArray(rw.dispatch(t1), size)(ArrayMallocFailed(inv))(c.o)
+        NewPointerArray(rw.dispatch(t1), size, fallible=true)(ArrayMallocFailed(inv))(c.o)
       case CCast(CInvocation(CLocal("__vercors_malloc"), _, _, _), _) =>
         throw UnsupportedMalloc(c)
       case CCast(n @ Null(), t) if t.asPointer.isDefined => rw.dispatch(n)
@@ -648,6 +648,7 @@ case class LangCToCol[Pre <: Generation](rw: LangSpecificToCol[Pre])
           NewPointerArray[Post](
             getInnerType(cNameSuccessor(d).t),
             Local(v.ref),
+            fallible=false,
           )(PanicBlame("Shared memory sizes cannot be negative.")),
         )
         declarations ++= Seq(cNameSuccessor(d))
@@ -662,6 +663,7 @@ case class LangCToCol[Pre <: Generation](rw: LangSpecificToCol[Pre])
           NewPointerArray[Post](
             getInnerType(cNameSuccessor(d).t),
             CIntegerValue(size),
+            fallible=false
           )(blame.get),
         )
         declarations ++= Seq(cNameSuccessor(d))
@@ -1129,11 +1131,11 @@ case class LangCToCol[Pre <: Generation](rw: LangSpecificToCol[Pre])
         (sizeOption, init.init) match {
           case (None, None) => throw WrongCType(decl)
           case (Some(size), None) =>
-            val newArr = NewPointerArray[Post](t, rw.dispatch(size))(cta.blame)
+            val newArr = NewPointerArray[Post](t, rw.dispatch(size), fallible=false)(cta.blame)
             Block(Seq(LocalDecl(v), assignLocal(v.get, newArr)))
           case (None, Some(CLiteralArray(exprs))) =>
             val newArr =
-              NewPointerArray[Post](t, c_const[Post](exprs.size))(cta.blame)
+              NewPointerArray[Post](t, c_const[Post](exprs.size), fallible=false)(cta.blame)
             Block(
               Seq(LocalDecl(v), assignLocal(v.get, newArr)) ++
                 assignliteralArray(v, exprs, o)
@@ -1144,7 +1146,7 @@ case class LangCToCol[Pre <: Generation](rw: LangSpecificToCol[Pre])
             if (realSize < exprs.size)
               logger.warn(s"Excess elements in array initializer: '${decl}'")
             val newArr =
-              NewPointerArray[Post](t, c_const[Post](realSize))(cta.blame)
+              NewPointerArray[Post](t, c_const[Post](realSize), fallible=false)(cta.blame)
             Block(
               Seq(LocalDecl(v), assignLocal(v.get, newArr)) ++
                 assignliteralArray(v, exprs.take(realSize.intValue), o)

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

@@ -34,13 +34,25 @@ class CSpec extends VercorsSpec {
 
     int main(){
       struct e* a = (struct e*) malloc(1*sizeof(struct e));
+      if (a == NULL) return 1;
+
       a->s.x = 1;
       struct d* b = &(a->s);
       free(a);
       b->x = 2;
     }
     """
 
+  vercors should fail withCode "ptrNull" using silicon in "use malloc result without null check" c
+    """
+      #include <stdlib.h>
+      int main(){
+          int* xs = (int*) malloc(1*sizeof(int));
+          *xs = 12;
+          free(xs);
+      }
+    """
+
   vercors should verify using silicon in "free null pointer" c
     """
       #include <stdlib.h>
@@ -403,6 +415,7 @@ class CSpec extends VercorsSpec {
       struct nested *np = NULL;
       np = (struct nested*) NULL;
       np = (struct nested*) malloc(sizeof(struct nested));
+      if (np == NULL) return;
       np->inner = NULL;
       np->inner = (struct nested*) NULL;
     }