Clean up the PR

build.sc

@@ -68,7 +68,7 @@ object external extends Module {
 object viper extends ScalaModule {
   object silverGit extends GitModule {
     def url = T { "https://github.com/viperproject/silver.git" }
-    def commitish = T { "93bc9b7516a710c8f01438e430058c4a54e20512" }
+    def commitish = T { "10b1b26a20957e5f000bf1bbcd4017145148afd7" }
     def filteredRepo = T {
       val workspace = repo()
       os.remove.all(workspace / "src" / "test")
@@ -78,7 +78,7 @@ object viper extends ScalaModule {
 
   object siliconGit extends GitModule {
     def url = T { "https://github.com/superaxander/silicon.git" }
-    def commitish = T { "c63989f64eb759f33bde68c330ce07d6e34134fa" }
+    def commitish = T { "2030e3eb63f4b1c92ddc8885f7c937673effc9bd" }
     def filteredRepo = T {
       val workspace = repo()
       os.remove.all(workspace / "src" / "test")
@@ -89,7 +89,7 @@ object viper extends ScalaModule {
 
   object carbonGit extends GitModule {
     def url = T { "https://github.com/viperproject/carbon.git" }
-    def commitish = T { "758481ef42f42720c36406bb278820ba802c7e68" }
+    def commitish = T { "d14a703fc6428fbae54e7333d8ede7efbbf850f0" }
     def filteredRepo = T {
       val workspace = repo()
       os.remove.all(workspace / "src" / "test")

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

@@ -1409,10 +1409,6 @@ final case class DerefPointer[G](pointer: Expr[G])(
     val blame: Blame[PointerDerefError]
 )(implicit val o: Origin)
     extends Expr[G] with DerefPointerImpl[G]
-final case class RawDerefPointer[G](pointer: Expr[G])(
-    val blame: Blame[PointerDerefError]
-)(implicit val o: Origin)
-    extends Expr[G] with RawDerefPointerImpl[G]
 final case class PointerAdd[G](pointer: Expr[G], offset: Expr[G])(
     val blame: Blame[PointerAddError]
 )(implicit val o: Origin)

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

@@ -1261,8 +1261,6 @@ abstract class CoercingRewriter[Pre <: Generation]()
       case deref @ Deref(obj, ref) => Deref(cls(obj), ref)(deref.blame)
       case deref @ DerefHeapVariable(ref) => DerefHeapVariable(ref)(deref.blame)
       case deref @ DerefPointer(p) => DerefPointer(pointer(p)._1)(deref.blame)
-      case deref @ RawDerefPointer(p) =>
-        RawDerefPointer(pointer(p)._1)(deref.blame)
       case Drop(xs, count) => Drop(seq(xs)._1, int(count))
       case Empty(obj) => Empty(sized(obj)._1)
       case EmptyProcess() => EmptyProcess()

src/main/vct/main/stages/Transformation.scala

@@ -341,7 +341,6 @@ case class SilverTransformation(
         EncodeString, // Encode spec string as seq<int>
         EncodeChar,
         CollectLocalDeclarations, // all decls in Scope
-//        EncodeByValueClass,
         VariableToPointer, // should happen before ParBlockEncoder so it can distinguish between variables which can and can't altered in a parallel block
         DesugarPermissionOperators, // no PointsTo, \pointer, etc.
         ReadToValue, // resolve wildcard into fractional permission

src/rewrite/vct/rewrite/LowerLocalHeapVariables.scala

@@ -13,28 +13,13 @@ case object LowerLocalHeapVariables extends RewriterBuilder {
 
   override def desc: String =
     "Lower LocalHeapVariables to Variables if their address is never taken"
-
-  private val pointerCreationOrigin: Origin = Origin(
-    Seq(LabelContext("pointer creation method"))
-  )
 }
 
 case class LowerLocalHeapVariables[Pre <: Generation]() extends Rewriter[Pre] {
-  import LowerLocalHeapVariables._
-
   private val stripped: SuccessionMap[LocalHeapVariable[Pre], Variable[Post]] =
     SuccessionMap()
   private val lowered: SuccessionMap[LocalHeapVariable[Pre], Variable[Post]] =
     SuccessionMap()
-//  private val pointerCreationMethods: SuccessionMap[Type[Pre], Procedure[Post]] = SuccessionMap()
-//
-//  def makePointerCreationMethod(t: Type[Pre]): Procedure[Post] = {
-//    implicit val o: Origin = pointerCreationOrigin
-//
-//    val proc = globalDeclarations.declare(withResult((result: Result[Post]) => {
-//
-//    }))
-//  }
 
   override def dispatch(program: Program[Pre]): Program[Post] = {
     val dereferencedHeapLocals = program.collect {

src/rewrite/vct/rewrite/PrepareByValueClass.scala

@@ -271,7 +271,6 @@ case class PrepareByValueClass[Pre <: Generation]() extends Rewriter[Pre] {
             dp,
             v.t.asPointer.get.element.asInstanceOf[TByValueClass[Pre]],
           )
-        // TODO: Check for copy semantics in inappropriate places (i.e. when the user has made this a pointer)
         case dp @ DerefPointer(DerefHeapVariable(Ref(v)))
             if v.t.asPointer.get.element.isInstanceOf[TByValueClass[Pre]] =>
           rewriteInCopyContext(

src/rewrite/vct/rewrite/VariableToPointer.scala

@@ -56,7 +56,6 @@ case class VariableToPointer[Pre <: Generation]() extends Rewriter[Pre] {
 
   override def dispatch(decl: Declaration[Pre]): Unit =
     decl match {
-      // TODO: Use some sort of NonNull pointer type instead
       case v: HeapVariable[Pre] if addressedSet.contains(v) =>
         heapVariableMap(v) = globalDeclarations
           .succeed(v, new HeapVariable(TNonNullPointer(dispatch(v.t)))(v.o))
@@ -94,8 +93,6 @@ case class VariableToPointer[Pre <: Generation]() extends Rewriter[Pre] {
         )
       case i @ Instantiate(cls, out)
           if cls.decl.isInstanceOf[ByValueClass[Pre]] =>
-        // TODO: Make sure that we recursively build newobject for byvalueclasses
-        //       maybe get rid this entirely and only have it in encode by value class
         Block(Seq(i.rewriteDefault()) ++ cls.decl.declarations.flatMap {
           case f: InstanceField[Pre] =>
             if (f.t.asClass.isDefined) {

src/rewrite/vct/rewrite/adt/ImportPointer.scala

@@ -407,31 +407,6 @@ case class ImportPointer[Pre <: Generation](importer: ImportADTImporter)
             )(PanicBlame("ptr_deref requires nothing.")),
           field = getPointerField(pointer),
         )(PointerFieldInsufficientPermission(deref.blame, deref))
-      case deref @ RawDerefPointer(pointer) =>
-        FunctionInvocation[Post](
-          ref = pointerDeref.ref,
-          args = Seq(
-            if (
-              inAxiom.isEmpty &&
-              !deref.o.find[LabelContext]
-                .exists(_.label == "classToRef cast helpers")
-            ) {
-              FunctionInvocation[Post](
-                ref = pointerAdd.ref,
-                // Always index with zero, otherwise quantifiers with pointers do not get triggered
-                args = Seq(unwrapOption(pointer, deref.blame), const(0)),
-                typeArgs = Nil,
-                Nil,
-                Nil,
-              )(NoContext(
-                DerefPointerBoundsPreconditionFailed(deref.blame, pointer)
-              ))
-            } else { unwrapOption(pointer, deref.blame) }
-          ),
-          typeArgs = Nil,
-          Nil,
-          Nil,
-        )(PanicBlame("ptr_deref requires nothing."))
       case len @ PointerBlockLength(pointer) =>
         ADTFunctionInvocation[Post](
           typeArgs = Some((blockAdt.ref, Nil)),

src/rewrite/vct/rewrite/lang/LangLLVMToCol.scala

@@ -596,7 +596,6 @@ case class LangLLVMToCol[Pre <: Generation](rw: LangSpecificToCol[Pre])
         // TODO: Use an actual Blame
 
         // Acquire the actual struct through a PointerAdd
-        // TODO: Can we somehow wrap the rw.dispatch(gep.pointer) to add the known type structureType?
         gep.pointer.t match {
           case LLVMTPointer(None) =>
             val structPointer =
@@ -798,7 +797,7 @@ case class LangLLVMToCol[Pre <: Generation](rw: LangSpecificToCol[Pre])
   effectively transforming the CFG into a tree. More efficient restructuring algorithms but this works for now.
 
   This of course only works for acyclic CFGs as otherwise replacement would be infinitely recursive.
-  Loop restructuring should be handled by pallas as it has much more analytical and contextual information about
+  Loop restructuring should be handled by Pallas as it has much more analytical and contextual information about
   the program.
    */
   case class GotoEliminator(bodyScope: Scope[Pre]) extends LazyLogging {

src/rewrite/vct/rewrite/veymont/generation/SpecializeEndpointClasses.scala

@@ -1,4 +1,4 @@
-package vct.rewrite.veymont
+package vct.rewrite.veymont.generation
 
 import com.typesafe.scalalogging.LazyLogging
 import vct.col.ast.{

src/viper/viper/api/backend/silicon/SiliconLogListener.scala

@@ -281,7 +281,7 @@ class SiliconMemberLogListener(
     if (log.traceBranchConditions) {
       val textCond =
         branchConditions.head match {
-          case BranchConditionExp(e) => e.toString()
+          case BranchConditionExp(e) => e.toString
           case BranchConditionTerm(e) => e.toString
           case BranchConditionNone(at, count) => s"alternative $at/$count"
         }

src/viper/viper/api/transform/ColToSilver.scala

@@ -6,7 +6,7 @@ import vct.col.ref.Ref
 import vct.col.util.AstBuildHelpers.unfoldStar
 import vct.col.{ast => col}
 import vct.result.VerificationError.{SystemError, Unreachable}
-import viper.silver.ast.{AnnotationInfo, ConsInfo, TypeVar, WildcardPerm}
+import viper.silver.ast.{TypeVar, WildcardPerm}
 import viper.silver.plugin.standard.termination.{
   DecreasesClause,
   DecreasesTuple,