Merge pull request #1314 from utwente-fmt/small-fixes

Small fixes
utwente-fmt · Feb 14, 2025 · 4bd0a11 · 4bd0a11
2 parents 0700d5a + 6fb0555
commit 4bd0a11
Show file tree

Hide file tree

Showing 11 changed files with 80 additions and 34 deletions.
diff --git a/examples/publications/2023/FASE2023JavaBIP/casinoAdjusted/Casino.java b/examples/publications/2023/FASE2023JavaBIP/casinoAdjusted/Casino.java
@@ -127,13 +127,15 @@ public boolean isGuessed() {
     @Pure
     @Guard(name = IS_OPERATOR)
     public boolean isOperator(@Data(name = OPERATOR) Integer sender) {
-        return sender == operator;
+        //@ ghost int x = (\assuming sender != null; sender.intValue());
+        return sender.intValue() == operator;
     }
 
     @Pure
     @Guard(name = IS_NOT_OPERATOR)
     public boolean isNotOperator(@Data(name = PLAYER) Integer sender) {
-        return sender != operator;
+        //@ ghost int x = (\assuming sender != null; sender.intValue());
+        return sender.intValue() != operator;
     }
 
     @Pure
@@ -153,11 +155,11 @@ public int getWin() {
     public int getPot() {
         return pot;
     }
-    
+
     @Pure
     @Guard(name = ENOUGH_FUNDS)
     public boolean enoughFunds(@Data(name = INCOMING_FUNDS) int funds) {
-        return funds <= pot; 
+        return funds <= pot;
     }
 
     @Pure

diff --git a/examples/publications/2023/FASE2023JavaBIP/casinoBroken/Casino.java b/examples/publications/2023/FASE2023JavaBIP/casinoBroken/Casino.java
@@ -129,13 +129,15 @@ public boolean isGuessed() {
     @Pure
     @Guard(name = IS_OPERATOR)
     public boolean isOperator(@Data(name = OPERATOR) Integer sender) {
-        return sender == operator;
+        //@ ghost int x = (\assuming sender != null; sender.intValue());
+        return sender.intValue() == operator;
     }
 
     @Pure
     @Guard(name = IS_NOT_OPERATOR)
     public boolean isNotOperator(@Data(name = PLAYER) Integer sender) {
-        return sender != operator;
+        //@ ghost int x = (\assuming sender != null; sender.intValue());
+        return sender.intValue() != operator;
     }
 
     @Pure
@@ -155,11 +157,11 @@ public int getWin() {
     public int getPot() {
         return pot;
     }
-    
+
     @Pure
     @Guard(name = ENOUGH_FUNDS)
     public boolean enoughFunds(@Data(name = INCOMING_FUNDS) int funds) {
-        return funds <= pot; 
+        return funds <= pot;
     }
 
     @Pure

diff --git a/src/col/vct/col/ast/Node.scala b/src/col/vct/col/ast/Node.scala
@@ -1036,6 +1036,9 @@ final case class CoerceCPPArrayPointer[G](elementType: Type[G])(
 final case class CoerceCVectorVector[G](size: BigInt, elementType: Type[G])(
     implicit val o: Origin
 ) extends Coercion[G] with CoerceCVectorVectorImpl[G]
+final case class CoerceNullLLVMPointer[G](elementType: Option[Type[G]])(
+    implicit val o: Origin
+) extends Coercion[G] with CoerceNullLLVMPointerImpl[G]
 
 final case class CoerceFracZFrac[G]()(implicit val o: Origin)
     extends Coercion[G] with CoerceFracZFracImpl[G]

diff --git a/src/col/vct/col/ast/family/coercion/CoerceNullLLVMPointerImpl.scala b/src/col/vct/col/ast/family/coercion/CoerceNullLLVMPointerImpl.scala
@@ -0,0 +1,9 @@
+package vct.col.ast.family.coercion
+
+import vct.col.ast.ops.CoerceNullLLVMPointerOps
+import vct.col.ast.{CoerceNullLLVMPointer, LLVMTPointer}
+
+trait CoerceNullLLVMPointerImpl[G] extends CoerceNullLLVMPointerOps[G] {
+  this: CoerceNullLLVMPointer[G] =>
+  override def target: LLVMTPointer[G] = LLVMTPointer(elementType)
+}
diff --git a/src/col/vct/col/typerules/CoercingRewriter.scala b/src/col/vct/col/typerules/CoercingRewriter.scala
@@ -725,6 +725,25 @@ abstract class CoercingRewriter[Pre <: Generation]()
     }
   }
 
+  def nonAny(
+      e: Expr[Pre],
+      left: Expr[Pre],
+      right: Expr[Pre],
+      cons: (Expr[Pre], Expr[Pre]) => Expr[Pre],
+  ): Expr[Pre] =
+    (left.t, right.t) match {
+      case (TAnyValue(), _) | (_, TAnyValue()) =>
+        cons(coerce(left, TAnyValue()), coerce(right, TAnyValue()))
+      case (lt, rt) =>
+        val sharedType = Types.leastCommonSuperType(lt, rt)
+        if (sharedType == TAnyValue[Pre]()) {
+          throw IncoercibleExplanation(
+            e,
+            "Coercion of the two operands of this operator yielded the `any` type, this is likely unintended and therefore disallowed. To use this operator with two differently-typed operands make sure one of the operands is already of the `any` type.",
+          )
+        } else { cons(coerce(left, sharedType), coerce(right, sharedType)) }
+    }
+
   override def postCoerce(e: Expr[Pre]): Expr[Post] =
     e match {
       case ApplyCoercion(e, coercion) =>
@@ -799,13 +818,7 @@ abstract class CoercingRewriter[Pre <: Generation]()
           vectorFloatOp2(div, (l, r) => AmbiguousDiv(l, r)(div.blame)),
         )
       case AmbiguousEq(left, right, vectorInnerType, elementSize) =>
-        val sharedType = Types.leastCommonSuperType(left.t, right.t)
-        AmbiguousEq(
-          coerce(left, sharedType),
-          coerce(right, sharedType),
-          vectorInnerType,
-          elementSize,
-        )
+        nonAny(e, left, right, AmbiguousEq(_, _, vectorInnerType, elementSize))
       case g @ AmbiguousGreater(left, right, elementSize) =>
         firstOk(
           e,
@@ -1022,13 +1035,7 @@ abstract class CoercingRewriter[Pre <: Generation]()
           },
         )
       case AmbiguousNeq(left, right, vectorInnerType, elementSize) =>
-        val sharedType = Types.leastCommonSuperType(left.t, right.t)
-        AmbiguousNeq(
-          coerce(left, sharedType),
-          coerce(right, sharedType),
-          vectorInnerType,
-          elementSize,
-        )
+        nonAny(e, left, right, AmbiguousNeq(_, _, vectorInnerType, elementSize))
       case AmbiguousOr(left, right) =>
         firstOk(
           e,
@@ -1278,9 +1285,7 @@ abstract class CoercingRewriter[Pre <: Generation]()
       case Empty(obj) => Empty(sized(obj)._1)
       case EmptyProcess() => EmptyProcess()
       case use @ EnumUse(enum, const) => use
-      case Eq(left, right) =>
-        val sharedType = Types.leastCommonSuperType(left.t, right.t)
-        Eq(coerce(left, sharedType), coerce(right, sharedType))
+      case Eq(left, right) => nonAny(e, left, right, Eq(_, _))
       case EitherLeft(e) => EitherLeft(e)
       case EitherRight(e) => EitherRight(e)
       case EndpointName(ref) => EndpointName(ref)
@@ -1575,9 +1580,7 @@ abstract class CoercingRewriter[Pre <: Generation]()
       case NdLength(dimensions) => NdLength(dimensions.map(int))
       case NdPartialIndex(indices, linearIndex, dimensions) =>
         NdPartialIndex(indices.map(int), int(linearIndex), dimensions.map(int))
-      case Neq(left, right) =>
-        val sharedType = Types.leastCommonSuperType(left.t, right.t)
-        Neq(coerce(left, sharedType), coerce(right, sharedType))
+      case Neq(left, right) => nonAny(e, left, right, Neq(_, _))
       case na @ NewArray(element, dims, moreDims, initialize) =>
         NewArray(element, dims.map(int), moreDims, initialize)(na.blame)
       case na @ NewPointerArray(element, size) =>

diff --git a/src/col/vct/col/typerules/CoercionUtils.scala b/src/col/vct/col/typerules/CoercionUtils.scala
@@ -123,7 +123,9 @@ case object CoercionUtils {
       case (TNull(), TAnyClass()) => CoerceNullAnyClass()
       case (TNull(), TPointer(target)) => CoerceNullPointer(target)
       case (TNull(), CTPointer(target)) => CoerceNullPointer(target)
+      case (TNull(), CTArray(_, target)) => CoerceNullPointer(target)
       case (TNull(), TEnum(target)) => CoerceNullEnum(target)
+      case (TNull(), LLVMTPointer(target)) => CoerceNullLLVMPointer(target)
 
       case (CTArray(_, innerType), TArray(element)) if element == innerType =>
         CoerceCArrayPointer(element)
@@ -159,6 +161,14 @@ case object CoercionUtils {
             getAnyCoercion(element, innerType).getOrElse(return None),
           ))
         }
+      case (CPPTArray(_, innerType), TPointer(element)) =>
+        if (element == innerType) { CoerceCPPArrayPointer(innerType) }
+        else {
+          CoercionSequence(Seq(
+            CoerceCPPArrayPointer(element),
+            getAnyCoercion(element, innerType).getOrElse(return None),
+          ))
+        }
       case (TFraction(), TZFraction()) => CoerceFracZFrac()
       case (TFraction(), TRational()) =>
         CoercionSequence(Seq(CoerceFracZFrac(), CoerceZFracRat()))

diff --git a/src/main/vct/main/stages/Parsing.scala b/src/main/vct/main/stages/Parsing.scala
@@ -122,7 +122,7 @@ case class Parsing[G <: Generation](
                 blameProvider,
                 ccpp,
                 cppSystemInclude,
-                readable.underlyingPath.map(_.getParent).toSeq ++
+                readable.underlyingPath.map(_.toAbsolutePath.getParent).toSeq ++
                   cppOtherIncludes,
                 cppDefines,
               )

diff --git a/src/rewrite/vct/rewrite/ClassToRef.scala b/src/rewrite/vct/rewrite/ClassToRef.scala
@@ -860,6 +860,8 @@ case class ClassToRef[Pre <: Generation]() extends Rewriter[Pre] {
           case _: TPointer[Pre] | _: TNonNullPointer[Pre] => e.rewriteDefault()
           // Keep integer casts intact for casting between integers and pointers
           case _: TInt[Pre] => e.rewriteDefault()
+          // Keep any casts intact for the adtAny stage
+          case _: TAnyValue[Pre] => e.rewriteDefault()
           case other => ???
         }
       case TypeOf(value) =>

diff --git a/src/rewrite/vct/rewrite/adt/ImportAny.scala b/src/rewrite/vct/rewrite/adt/ImportAny.scala
@@ -3,6 +3,7 @@ package vct.col.rewrite.adt
 import hre.util.ScopedStack
 import vct.col.ast.{
   AxiomaticDataType,
+  Cast,
   CoerceSomethingAnyValue,
   Coercion,
   Expr,
@@ -12,6 +13,7 @@ import vct.col.ast.{
   TAxiomatic,
   TType,
   Type,
+  TypeValue,
 }
 import vct.col.origin.{Origin, PanicBlame}
 import vct.col.ref.LazyRef
@@ -48,10 +50,23 @@ case class ImportAny[Pre <: Generation](importer: ImportADTImporter)
       case TType(TAnyValue()) =>
         // Only the any adt definition refers to itself, so this is the only place this trick is necessary.
         if (inAnyLoad.isEmpty)
-          rewriteDefault(t)
+          super.postCoerce(t)
         else
           TType(TAxiomatic(new LazyRef(anyAdt), Nil))
       case TAnyValue() => TAxiomatic(anyAdt.ref, Nil)
-      case other => rewriteDefault(other)
+      case other => super.postCoerce(other)
+    }
+
+  override def postCoerce(e: Expr[Pre]): Expr[Post] =
+    e match {
+      case Cast(value, TypeValue(TAnyValue())) =>
+        FunctionInvocation[Post](
+          anyFrom.ref,
+          Seq(dispatch(value)),
+          Seq(dispatch(value.t)),
+          Nil,
+          Nil,
+        )(PanicBlame("coercing to any requires nothing."))(e.o)
+      case other => super.postCoerce(other)
     }
 }
diff --git a/src/rewrite/vct/rewrite/adt/ImportPointer.scala b/src/rewrite/vct/rewrite/adt/ImportPointer.scala
@@ -556,6 +556,8 @@ case class ImportPointer[Pre <: Generation](importer: ImportADTImporter)
             OptSome(applyAsTypeFunction(innerType, value, newValue))
           case (TNonNullPointer(innerType), TNonNullPointer(_)) =>
             applyAsTypeFunction(innerType, value, newValue)
+          // Other type of cast probably a cast to any
+          case (_, _) => super.postCoerce(e)
         }
       case IntegerPointerCast(value, typeValue, typeSize) =>
         val targetType = typeValue.t.asInstanceOf[TType[Pre]].t

diff --git a/test/main/vct/test/integration/examples/TechnicalSpec.scala b/test/main/vct/test/integration/examples/TechnicalSpec.scala
@@ -52,12 +52,10 @@ class TechnicalSpec extends VercorsSpec {
     void main(C arg);
   """
 
-  vercors should verify using anyBackend in
+  vercors should error withCode "resolutionError:type" in
     "example showing comparison of unrelated types" pvl """
     void test() {
-      /*[/expect assertFailed:false]*/
       assert 1 == false;
-      /*[/end]*/
     }
   """