resolve some warnings

build.sc

@@ -356,6 +356,7 @@ object viper extends ScalaModule {
 
   object silver extends ScalaModule {
     override def scalaVersion = "2.13.10"
+    override def scalacOptions = T { Seq("-Xno-patmat-analysis") }
     def repo = silverGit
     override def sources = T.sources { repo.repo() / "src" / "main" / "scala" }
     override def ivyDeps = settings.deps.log ++ Agg(
@@ -387,11 +388,13 @@ object viper extends ScalaModule {
 
     object common extends ScalaModule {
       override def scalaVersion = "2.13.10"
+      override def scalacOptions = T { Seq("-Xno-patmat-analysis") }
       override def sources = T.sources { silicon.repo.repo() / "common" / "src" / "main" / "scala" }
       override def moduleDeps = Seq(silver)
     }
 
     override def scalaVersion = "2.13.10"
+    override def scalacOptions = T { Seq("-Xno-patmat-analysis") }
     def repo = siliconGit
     override def sources = T.sources { repo.repo() / "src" / "main" / "scala" }
     override def ivyDeps = settings.deps.log ++ Agg(
@@ -407,6 +410,7 @@ object viper extends ScalaModule {
 
   object carbon extends ScalaModule {
     override def scalaVersion = "2.13.10"
+    override def scalacOptions = T { Seq("-Xno-patmat-analysis") }
     def repo = carbonGit
     override def sources = T.sources { repo.repo() / "src" / "main" / "scala" }
     override def ivyDeps = settings.deps.log

src/col/vct/col/ast/expr/context/AmbiguousResultImpl.scala

@@ -22,7 +22,9 @@ trait AmbiguousResultImpl[G] extends NodeFamilyImpl[G] { this: AmbiguousResult[G
     case RefFunction(decl) => decl.returnType
     case RefProcedure(decl) => decl.returnType
     case RefJavaMethod(decl) => decl.returnType
+    case RefJavaAnnotationMethod(decl) => decl.returnType
     case RefLlvmFunctionDefinition(decl) => decl.returnType
+    case RefLlvmSpecFunction(decl) => decl.returnType
     case RefInstanceFunction(decl) => decl.returnType
     case RefInstanceMethod(decl) => decl.returnType
     case RefInstanceOperatorMethod(decl) => decl.returnType

src/col/vct/col/ast/family/coercion/CoercionImpl.scala

@@ -1,6 +1,6 @@
 package vct.col.ast.family.coercion
 
-import vct.col.ast.{CoerceBoolResource, CoerceBoundIntFrac, CoerceBoundIntZFrac, CoerceCPrimitiveToCol, CoerceCPPPrimitiveToCol, CoerceClassAnyClass, CoerceColToCPrimitive, CoerceColToCPPPrimitive, CoerceFloatRat, CoerceFracZFrac, CoerceIdentity, CoerceIncreasePrecision, CoerceIntRat, CoerceJavaClassAnyClass, CoerceJavaSupports, CoerceJoinUnion, CoerceMapBag, CoerceMapEither, CoerceMapMap, CoerceMapMatrix, CoerceMapOption, CoerceMapSeq, CoerceMapSet, CoerceMapTuple, CoerceMapType, CoerceNothingSomething, CoerceNullAnyClass, CoerceNullArray, CoerceNullClass, CoerceNullJavaClass, CoerceNullPointer, CoerceNullRef, CoerceRatZFrac, CoerceSelectUnion, CoerceSomethingAny, CoerceSupports, CoerceUnboundInt, CoerceWidenBound, CoerceZFracFrac, CoerceZFracRat, Coercion, CoercionSequence, Type}
+import vct.col.ast._
 
 trait CoercionImpl[G] { this: Coercion[G] =>
   def target: Type[G]
@@ -19,6 +19,7 @@ trait CoercionImpl[G] { this: Coercion[G] =>
     case CoerceNullJavaClass(_) => true
     case CoerceNullAnyClass() => true
     case CoerceNullPointer(_) => true
+    case CoerceNullEnum(_) => true
     case CoerceFracZFrac() => true
     case CoerceZFracRat() => true
     case CoerceFloatRat(_) => true
@@ -36,6 +37,8 @@ trait CoercionImpl[G] { this: Coercion[G] =>
     case CoerceColToCPrimitive(_, _) => true
     case CoerceCPPPrimitiveToCol(_, _) => true
     case CoerceColToCPPPrimitive(_, _) => true
+    case CoerceCPPArrayPointer(_) => true
+    case CoerceCArrayPointer(_) => true
     case CoerceMapOption(inner, _, _) => inner.isPromoting
     case CoerceMapTuple(inner, _, _) => inner.forall(_.isPromoting)
     case CoerceMapEither(inner, _, _) => inner._1.isPromoting && inner._2.isPromoting
@@ -47,5 +50,6 @@ trait CoercionImpl[G] { this: Coercion[G] =>
     case CoerceMapType(inner, _, _) => inner.isPromoting
     case CoerceRatZFrac() => false
     case CoerceZFracFrac() => false
+    case CoerceBoundIntFloat(_, _) => false
   }
 }

src/col/vct/col/ast/family/location/LocationImpl.scala

@@ -1,6 +1,6 @@
 package vct.col.ast.family.location
 
-import vct.col.ast.{AmbiguousLocation, ArrayLocation, FieldLocation, InstancePredicateLocation, Location, ModelLocation, PointerLocation, PredicateLocation, SilverFieldLocation, Type}
+import vct.col.ast.{AmbiguousLocation, ArrayLocation, FieldLocation, HeapVariableLocation, InstancePredicateLocation, Location, ModelLocation, PointerLocation, PredicateLocation, SilverFieldLocation, Type}
 
 trait LocationImpl[G] { this: Location[G] =>
   def t: Type[G] = {
@@ -13,5 +13,7 @@ trait LocationImpl[G] { this: Location[G] =>
       case PredicateLocation(predicate, args) => ???
       case InstancePredicateLocation(predicate, obj, args) => ???
       case AmbiguousLocation(expr) => expr.t
-    } }
+      case HeapVariableLocation(ref) => ref.decl.t
+    }
+  }
 }

src/col/vct/col/ast/lang/CInvocationImpl.scala

@@ -16,6 +16,8 @@ trait CInvocationImpl[G] { this: CInvocation[G] =>
     case RefModelAction(decl) => decl.returnType
     case RefCFunctionDefinition(decl) => C.typeOrReturnTypeFromDeclaration(decl.specs, decl.declarator)
     case RefCGlobalDeclaration(decls, initIdx) => C.typeOrReturnTypeFromDeclaration(decls.decl.specs, decls.decl.inits(initIdx).decl)
+    case RefLlvmSpecFunction(decl) => decl.returnType
+    case RefProverFunction(decl) => decl.returnType
     case RefInstanceMethod(decl) => decl.returnType
     case RefInstanceFunction(decl) => decl.returnType
     case RefInstancePredicate(decl) => decl.returnType

src/col/vct/col/ast/lang/CLocalImpl.scala

@@ -1,6 +1,6 @@
 package vct.col.ast.lang
 
-import vct.col.ast.{CLocal, CPrimitiveType, CTCudaVec, Type}
+import vct.col.ast.{CLocal, CPrimitiveType, CTCudaVec, TEnum, Type}
 import vct.col.print.{Ctx, Doc, Text}
 import vct.col.resolve.ctx._
 import vct.col.resolve.lang.C
@@ -27,6 +27,9 @@ trait CLocalImpl[G] { this: CLocal[G] =>
     case RefModelField(field) => field.t
     case target: SpecInvocationTarget[G] => Types.notAValue(target)
     case _: RefCudaVec[G] => CTCudaVec()
+    case cls: RefClass[G] => Types.notAValue(cls)
+    case enum: RefEnum[G] => Types.notAValue(enum)
+    case RefEnumConstant(enum, _) => TEnum(enum.get.ref)
   }
 
   override def layout(implicit ctx: Ctx): Doc = Text(name)

src/col/vct/col/ast/lang/CPPInvocationImpl.scala

@@ -16,6 +16,8 @@ trait CPPInvocationImpl[G] { this: CPPInvocation[G] =>
     case RefModelAction(decl) => decl.returnType
     case RefCPPFunctionDefinition(decl) => CPP.typeOrReturnTypeFromDeclaration(decl.specs, decl.declarator)
     case RefCPPGlobalDeclaration(decls, initIdx) => CPP.typeOrReturnTypeFromDeclaration(decls.decl.specs, decls.decl.inits(initIdx).decl)
+    case RefLlvmSpecFunction(decl) => decl.returnType
+    case RefProverFunction(decl) => decl.returnType
     case RefInstanceMethod(decl) => decl.returnType
     case RefInstanceFunction(decl) => decl.returnType
     case RefInstancePredicate(decl) => decl.returnType

src/col/vct/col/ast/lang/CPPLocalImpl.scala

@@ -1,6 +1,6 @@
 package vct.col.ast.lang
 
-import vct.col.ast.{CPPLocal, CPPPrimitiveType, Type}
+import vct.col.ast.{CPPLocal, CPPPrimitiveType, TEnum, Type}
 import vct.col.print.{Ctx, Doc, Text}
 import vct.col.resolve.ctx._
 import vct.col.resolve.lang.CPP
@@ -26,6 +26,9 @@ trait CPPLocalImpl[G] { this: CPPLocal[G] =>
       }
     case RefModelField(field) => field.t
     case target: SpecInvocationTarget[G] => Types.notAValue(target)
+    case cls: RefClass[G] => Types.notAValue(cls)
+    case enum: RefEnum[G] => Types.notAValue(enum)
+    case RefEnumConstant(enum, _) => TEnum(enum.get.ref)
   }
 
   override def layout(implicit ctx: Ctx): Doc = Text(name)

src/col/vct/col/ast/lang/CStructAccessImpl.scala

@@ -1,6 +1,6 @@
 package vct.col.ast.lang
 
-import vct.col.ast.{CStructAccess, TInt, TNotAValue, Type}
+import vct.col.ast.{CStructAccess, TEnum, TInt, TNotAValue, Type}
 import vct.col.print.{Ctx, Doc, Precedence, Text}
 import vct.col.resolve.ctx._
 import vct.col.typerules.Types
@@ -20,6 +20,9 @@ trait CStructAccessImpl[G] { this: CStructAccess[G] =>
     case ref: BuiltinField[G] => ref.f(struct).t
     case ref: BuiltinInstanceMethod[G] => Types.notAValue(ref)
     case ref: RefCudaVecDim[G] => TInt()
+    case RefEnumConstant(enum, _) => TEnum(enum.get.ref)
+    case RefLlvmSpecFunction(decl) => decl.returnType
+    case RefProverFunction(decl) => decl.returnType
   }
 
   override def precedence: Int = Precedence.POSTFIX

src/col/vct/col/ast/lang/GpgpuCudaKernelInvocationImpl.scala

@@ -19,6 +19,8 @@ trait GpgpuCudaKernelInvocationImpl[G] { this: GpgpuCudaKernelInvocation[G] =>
     case RefCFunctionDefinition(decl) => C.typeOrReturnTypeFromDeclaration(decl.specs, decl.declarator)
     case RefCGlobalDeclaration(decls, initIdx) => C.typeOrReturnTypeFromDeclaration(decls.decl.specs, decls.decl.inits(initIdx).decl)
     case BuiltinInstanceMethod(f) => ???
+    case RefLlvmSpecFunction(decl) => decl.returnType
+    case RefProverFunction(decl) => decl.returnType
   }
 
   override def layout(implicit ctx: Ctx): Doc =

src/col/vct/col/ast/lang/JavaDerefImpl.scala

@@ -15,10 +15,11 @@ trait JavaDerefImpl[G] { this: JavaDeref[G] =>
     case ref: RefModel[G] => Types.notAValue(ref)
     case RefVariable(v) => v.t
     case RefJavaField(decls, idx) => FuncTools.repeat[Type[G]](TArray(_), decls.decls(idx).moreDims, decls.t)
-    case RefEnumConstant(_, decl) => obj.t match {
-      case TNotAValue(RefEnum(enum: Enum[G])) => TEnum(enum.ref[Enum[G]])
-    }
+    case RefEnumConstant(enum, _) => TEnum(enum.get.ref)
     case BuiltinField(f) => f(obj).t
+    case ref: RefEnum[G] => Types.notAValue(ref)
+    case RefJavaParam(decl) => decl.t
+    case ref: RefProverType[G] => Types.notAValue(ref)
   }
 
   override def precedence: Int = Precedence.POSTFIX

src/col/vct/col/ast/lang/JavaInvocationImpl.scala

@@ -19,6 +19,8 @@ trait JavaInvocationImpl[G] { this: JavaInvocation[G] =>
     case RefJavaMethod(decl) => decl.returnType
     case RefProverFunction(decl) => decl.returnType
     case BuiltinInstanceMethod(f) => f(obj.get)(arguments).t
+    case RefJavaAnnotationMethod(decl) => decl.returnType
+    case RefLlvmSpecFunction(decl) => decl.returnType
   }
 
   override def precedence: Int = Precedence.POSTFIX

src/col/vct/col/ast/lang/JavaLocalImpl.scala

@@ -10,7 +10,7 @@ trait JavaLocalImpl[G] { this: JavaLocal[G] =>
   override lazy val t: Type[G] = ref.get match {
     case ref: RefAxiomaticDataType[G] => Types.notAValue(ref)
     case ref: RefEnum[G] => Types.notAValue(ref)
-    case RefEnumConstant(Some(enum), _) => TEnum(enum.ref[Enum[G]])
+    case RefEnumConstant(enum, _) => TEnum(enum.get.ref)
     case RefVariable(decl) => decl.t
     case ref: RefUnloadedJavaNamespace[G] => Types.notAValue(ref)
     case ref: RefJavaClass[G] => Types.notAValue(ref)
@@ -19,6 +19,7 @@ trait JavaLocalImpl[G] { this: JavaLocal[G] =>
     case RefJavaParam(decl) => decl.t
     case RefJavaBipGuard(_) => TBool()
     case RefModelField(field) => field.t
+    case ref: RefClass[G] => Types.notAValue(ref)
   }
 
   override def layout(implicit ctx: Ctx): Doc = Text(name)

src/col/vct/col/ast/lang/LLVMLocalImpl.scala

@@ -4,9 +4,7 @@ import vct.col.ast.{LlvmLocal, Type}
 import vct.col.print.{Ctx, Doc, Text}
 
 trait LLVMLocalImpl[G] { this: LlvmLocal[G] =>
-  override lazy val t: Type[G] = ref match {
-    case Some(ref) => ref.decl.t
-  }
+  override lazy val t: Type[G] = ref.get.decl.t
 
   override def layout(implicit ctx: Ctx): Doc = Text(name)
 }

src/col/vct/col/ast/lang/PVLDerefImpl.scala

@@ -8,9 +8,7 @@ trait PVLDerefImpl[G] { this: PVLDeref[G] =>
   override lazy val t: Type[G] = ref.get match {
     case ref: RefModelField[G] => ref.decl.t
     case ref: RefField[G] => ref.decl.t
-    case ref: RefEnumConstant[G] => obj.t match {
-      case TNotAValue(RefEnum(enum)) => TEnum(enum.ref[Enum[G]])
-    }
+    case RefEnumConstant(enum, _) => TEnum(enum.get.ref)
     case ref: BuiltinField[G] => ref.f(obj).t
   }
 

src/col/vct/col/ast/lang/PVLInvocationImpl.scala

@@ -18,6 +18,7 @@ trait PVLInvocationImpl[G] { this: PVLInvocation[G] =>
     case RefProverFunction(decl) => decl.returnType
     case PVLBuiltinInstanceMethod(f) => f(obj.get)(args).t
     case BuiltinInstanceMethod(f) => f(obj.get)(args).t
+    case RefLlvmSpecFunction(decl) => decl.returnType
   }
 
   override def layout(implicit ctx: Ctx): Doc =

src/col/vct/col/ast/lang/PVLLocalImpl.scala

@@ -1,6 +1,6 @@
 package vct.col.ast.lang
 
-import vct.col.ast.{PVLLocal, TNotAValue, Type}
+import vct.col.ast.{PVLLocal, TEnum, TNotAValue, Type}
 import vct.col.print.{Ctx, Doc, Text}
 import vct.col.resolve.ctx._
 import vct.col.typerules.Types
@@ -14,6 +14,7 @@ trait PVLLocalImpl[G] { this: PVLLocal[G] =>
     case ref: RefField[G] => ref.decl.t
     case ref: RefModelField[G] => ref.decl.t
     case ref: RefVeyMontThread[G] => ref.decl.threadType
+    case RefEnumConstant(enum, _) => TEnum(enum.get.ref)
   }
 
   override def layout(implicit ctx: Ctx): Doc = Text(name)

src/col/vct/col/ast/node/NodeImpl.scala

@@ -105,9 +105,9 @@ trait NodeImpl[G] extends Show { this: Node[G] =>
   private def debugLayout(x: scala.Any)(implicit ctx: Ctx): Doc = x match {
     case n: Node[_] => n.show
     case r: Ref[_, _] => Text("Ref(") <> ctx.name(r) <> ")"
-    case p: scala.Product => Group(Text(p.getClass.getSimpleName) <> "(" <> Doc.args(p.productIterator.map(debugLayout).toSeq) <> ")")
     case o: scala.Option[scala.Any] if o.isEmpty => Text("None")
     case o: scala.Option[scala.Any] => Text("Some(") <> debugLayout(o.get) <> ")"
+    case p: scala.Product => Group(Text(p.getClass.getSimpleName) <> "(" <> Doc.args(p.productIterator.map(debugLayout).toSeq) <> ")")
     case i: scala.Iterable[scala.Any] => Group(Text(i.getClass.getSimpleName) <> "(" <> Doc.args(i.map(debugLayout).toSeq) <> ")")
     case other => Text(other.toString)
   }

src/col/vct/col/ast/util/ExpressionEqualityCheck.scala

@@ -5,6 +5,7 @@ import vct.col.ast.{And, BinExpr, BitAnd, BitNot, BitOr, BitShl, BitShr, BitUShr
 import vct.result.VerificationError.UserError
 
 import scala.collection.mutable
+import scala.reflect.ClassTag
 
 object ExpressionEqualityCheck {
   def apply[G](info: Option[AnnotationVariableInfo[G]] = None): ExpressionEqualityCheck[G] = new ExpressionEqualityCheck[G](info)
@@ -147,9 +148,9 @@ class ExpressionEqualityCheck[G](info: Option[AnnotationVariableInfo[G]]) {
     case _ => isConstantInt(e).getOrElse(0) != 0
   }
 
-  def unfoldComm[B <: BinExpr[G]](e: Expr[G], base: B): Seq[Expr[G]] = {
+  def unfoldComm[B <: BinExpr[G]](e: Expr[G])(implicit tag: ClassTag[B]): Seq[Expr[G]] = {
     e match {
-      case e: B if e.getClass == base.getClass => unfoldComm[B](e.left, base) ++ unfoldComm[B](e.right, base)
+      case e: B /* checked */ => unfoldComm[B](e.left) ++ unfoldComm[B](e.right)
       case _ => Seq(e)
     }
   }
@@ -175,9 +176,9 @@ class ExpressionEqualityCheck[G](info: Option[AnnotationVariableInfo[G]]) {
       (resLeft, resRight)
     }
 
-    def commAssoc[B <: BinExpr[G]](e1: B, e2: B): Boolean = {
-      val e1s = unfoldComm[B](e1, e1)
-      val e2s = unfoldComm[B](e2, e2)
+    def commAssoc[B <: BinExpr[G]](e1: B, e2: B)(implicit tag: ClassTag[B]): Boolean = {
+      val e1s = unfoldComm[B](e1)
+      val e2s = unfoldComm[B](e2)
 
       val (e1rest, e1Ints) = partitionOptionList(e1s, isConstantInt)
       val (e2rest, e2Ints) = partitionOptionList(e2s, isConstantInt)
@@ -219,8 +220,8 @@ class ExpressionEqualityCheck[G](info: Option[AnnotationVariableInfo[G]]) {
     (lhs, rhs) match {
       // Unsure if we could check/pattern match on this easier
       // Commutative operators
-      case (lhs@Plus(_, _), rhs@Plus(_, _)) => commAssoc(lhs, rhs)
-      case (lhs@Mult(_, _), rhs@Mult(_, _)) => commAssoc(lhs, rhs)
+      case (lhs@Plus(_, _), rhs@Plus(_, _)) => commAssoc[Plus[G]](lhs, rhs)
+      case (lhs@Mult(_, _), rhs@Mult(_, _)) => commAssoc[Mult[G]](lhs, rhs)
       case (BitAnd(lhs1, lhs2), BitAnd(rhs1, rhs2)) => comm(lhs1, lhs2, rhs1, rhs2)
       case (BitOr(lhs1, lhs2), BitOr(rhs1, rhs2)) => comm(lhs1, lhs2, rhs1, rhs2)
       case (BitXor(lhs1, lhs2), BitXor(rhs1, rhs2)) => comm(lhs1, lhs2, rhs1, rhs2)

src/col/vct/col/feature/FeatureRainbow.scala

@@ -389,7 +389,6 @@ class FeatureRainbow[G] {
     case node: ParBlockDecl[G] => ParallelRegion
     case node: ParInvariantDecl[G] => ParallelRegion
     case node: IterVariable[G] => ParallelRegion
-    case node: ParSequential[G] => ParallelRegion
 
     case node: Permutation[G] => PermutationOperator
 

src/col/vct/col/resolve/Resolve.scala

@@ -278,9 +278,6 @@ case object ResolveReferences extends LazyLogging {
     case cls: Class[G] => ctx
       .copy(currentThis=Some(RefClass(cls)))
       .declare(cls.declarations)
-    case app: ContractApplicable[G] => ctx
-      .copy(currentResult=Some(Referrable.from(app).head.asInstanceOf[ResultTarget[G]] /* PB TODO: ew */))
-      .declare(app.declarations ++ app.body.map(scanLabels).getOrElse(Nil))
     case method: JavaMethod[G] => ctx
       .copy(currentResult=Some(RefJavaMethod(method)))
       .declare(method.declarations ++ method.body.map(scanLabels).getOrElse(Nil))
@@ -344,6 +341,9 @@ case object ResolveReferences extends LazyLogging {
       .declare(scanBlocks(par.impl).map(_.decl))
     case Scope(locals, body) => ctx
       .declare(locals ++ scanScope(body, inGPUKernel))
+    case app: ContractApplicable[G] => ctx
+      .copy(currentResult = Some(Referrable.from(app).head.asInstanceOf[ResultTarget[G]] /* PB TODO: ew */))
+      .declare(app.declarations ++ app.body.map(scanLabels).getOrElse(Nil))
     case app: Applicable[G] => ctx
       .declare(app.declarations ++ app.body.map(scanLabels).getOrElse(Nil))
     case declarator: Declarator[G] => ctx
@@ -364,7 +364,7 @@ case object ResolveReferences extends LazyLogging {
         Java.findJavaName(name, ctx.asTypeResolutionContext)
           .orElse(Java.findJavaTypeName(Seq(name), ctx.asTypeResolutionContext) match {
             case Some(target: JavaNameTarget[G]) => Some(target)
-            case None => None
+            case Some(_) | None => None
           }))
           .getOrElse(
             if (ctx.topLevelJavaDeref.isEmpty) throw NoSuchNameError("local", name, local)
@@ -632,6 +632,7 @@ case object ResolveReferences extends LazyLogging {
           }
         case RefLlvmSpecFunction(_) =>
           Some(Spec.findLocal(local.name, ctx).getOrElse(throw NoSuchNameError("local", local.name, local)).ref)
+        case _ => None
       }
     case inv: LlvmAmbiguousFunctionInvocation[G] =>
       inv.ref = LLVM.findCallable(inv.name, ctx) match {

src/col/vct/col/resolve/ctx/Referrable.scala

@@ -66,7 +66,13 @@ sealed trait Referrable[G] {
     case RefVeyMontThread(decl) => Referrable.originName(decl)
     case RefProverType(decl) => Referrable.originName(decl)
     case RefProverFunction(decl) => Referrable.originName(decl)
+    case RefJavaBipGuard(decl) => Referrable.originName(decl)
+    case RefLlvmFunctionDefinition(decl) => Referrable.originName(decl)
+    case RefLlvmGlobal(decl) => Referrable.originName(decl)
+    case RefLlvmSpecFunction(decl) => Referrable.originName(decl)
 
+    case RefJavaBipGlueContainer() => ""
+    case PVLBuiltinInstanceMethod(_) => ""
     case BuiltinField(_) => ""
     case BuiltinInstanceMethod(_) => ""
     case RefPVLConstructor(decl) => ""