resolve last warnings

build.sc

@@ -112,6 +112,7 @@ object util {
     override def scalacOptions = T {
       val shared = Seq(
         "-deprecation",
+        "-feature",
       )
 
       if (strictOptions()) {

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

@@ -16,7 +16,6 @@ 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

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

@@ -16,7 +16,6 @@ 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

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

@@ -21,7 +21,6 @@ trait CStructAccessImpl[G] { this: CStructAccess[G] =>
     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
   }
 

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

@@ -19,7 +19,6 @@ 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
   }
 

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

@@ -18,7 +18,6 @@ trait JavaDerefImpl[G] { this: JavaDeref[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)
   }
 

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

@@ -20,7 +20,6 @@ trait JavaInvocationImpl[G] { this: JavaInvocation[G] =>
     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/PVLInvocationImpl.scala

@@ -18,7 +18,6 @@ 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/resolve/ctx/Referrable.scala

@@ -81,6 +81,7 @@ sealed trait Referrable[G] {
     case RefBipTransition(decl) => Referrable.originName(decl)
     case RefBipTransitionSynchronization(decl) => ""
     case RefBipConstructor(decl) => Referrable.originName(decl)
+    case RefHeapVariable(decl) => Referrable.originName(decl)
 
     case RefJavaBipGlueContainer() => ""
     case PVLBuiltinInstanceMethod(_) => ""
@@ -172,6 +173,7 @@ case object Referrable {
     case decl: BipTransition[G] => RefBipTransition(decl)
     case decl: BipTransitionSynchronization[G] => RefBipTransitionSynchronization(decl)
     case decl: BipConstructor[G] => RefBipConstructor(decl)
+    case decl: HeapVariable[G] => RefHeapVariable(decl)
   })
 
   def originName(decl: Declaration[_]): String = decl.o match {
@@ -258,7 +260,7 @@ case class RefJavaField[G](decls: JavaFields[G], idx: Int) extends Referrable[G]
 case class RefJavaLocalDeclaration[G](decls: JavaLocalDeclaration[G], idx: Int) extends Referrable[G] with JavaNameTarget[G]
 case class RefJavaConstructor[G](decl: JavaConstructor[G]) extends Referrable[G] with JavaConstructorTarget[G]
 case class RefJavaMethod[G](decl: JavaMethod[G]) extends Referrable[G] with JavaInvocationTarget[G] with ResultTarget[G]
-case class RefJavaParam[G](decl: JavaParam[G]) extends Referrable[G] with JavaNameTarget[G] with JavaDerefTarget[G]
+case class RefJavaParam[G](decl: JavaParam[G]) extends Referrable[G] with JavaNameTarget[G]
 case class RefJavaAnnotationMethod[G](decl: JavaAnnotationMethod[G]) extends Referrable[G] with JavaInvocationTarget[G] with ResultTarget[G]
 case class RefInstanceFunction[G](decl: InstanceFunction[G]) extends Referrable[G] with SpecInvocationTarget[G] with ResultTarget[G]
 case class RefInstanceMethod[G](decl: InstanceMethod[G]) extends Referrable[G] with SpecInvocationTarget[G] with ResultTarget[G]
@@ -294,8 +296,9 @@ case class RefBipStatePredicate[G](decl: BipStatePredicate[G]) extends Referrabl
 case class RefBipTransition[G](decl: BipTransition[G]) extends Referrable[G]
 case class RefBipTransitionSynchronization[G](decl: BipTransitionSynchronization[G]) extends Referrable[G]
 case class RefBipConstructor[G](decl: BipConstructor[G]) extends Referrable[G]
+case class RefHeapVariable[G](decl: HeapVariable[G]) extends Referrable[G]
 
-case class RefLlvmSpecFunction[G](decl: LlvmSpecFunction[G]) extends Referrable[G] with SpecInvocationTarget[G] with ResultTarget[G]
+case class RefLlvmSpecFunction[G](decl: LlvmSpecFunction[G]) extends Referrable[G] with LlvmInvocationTarget[G] with ResultTarget[G]
 case class RefSeqProg[G](decl: VeyMontSeqProg[G]) extends Referrable[G]
 case class RefVeyMontThread[G](decl: VeyMontThread[G]) extends Referrable[G] with PVLNameTarget[G]
 case class RefProverType[G](decl: ProverType[G]) extends Referrable[G] with SpecTypeNameTarget[G]

src/rewrite/vct/rewrite/CheckProcessAlgebra.scala

@@ -25,6 +25,8 @@ case class CheckProcessAlgebra[Pre <: Generation]() extends Rewriter[Pre] with L
         PanicBlame("Generated methods for models do not have context_everywhere clauses.").blame(ctx)
       case _: SignalsFailed | _: ExceptionNotInSignals =>
         PanicBlame("Generated methods for models do not throw exceptions.").blame(error)
+      case _: TerminationMeasureFailed =>
+        PanicBlame("Generated methods for models do not have termination measures (yet).").blame(error)
     }
   }
 

src/rewrite/vct/rewrite/FloatToRat.scala

@@ -26,13 +26,13 @@ case object FloatToRat extends RewriterBuilder {
 }
 
 case class FloatToRat[Pre <: Generation]() extends Rewriter[Pre] {
-  def name(t: Type[_]) = t match {
+  def name(t: TFloat[_]) = t match {
     case t if t == PVL.float64 => "f64"
     case t if t == PVL.float32 => "f32"
     case TFloat(e, m) => s"f${e}_$m"
   }
 
-  def makeCast(from: Type[Pre], to: Type[Pre]): Function[Post] = {
+  def makeCast(from: TFloat[Pre], to: TFloat[Pre]): Function[Post] = {
     globalDeclarations.declare(function[Post](
       args = Seq(new Variable(dispatch(from))(DiagnosticOrigin)),
       returnType = dispatch(to),
@@ -47,7 +47,10 @@ case class FloatToRat[Pre <: Generation]() extends Rewriter[Pre] {
       if (e.t == t) {
         dispatch(e)
       } else {
-        val f: Function[Post] = casts.getOrElseUpdate((e.t, t), makeCast(e.t, t))
+        // PB: just casting to float is a bit dubious here, but at least:
+        // - e is type-checked to be coercible to TFloats.max
+        // - t is "supposed" to be a floaty type I guess
+        val f: Function[Post] = casts.getOrElseUpdate((e.t, t), makeCast(e.t.asInstanceOf[TFloat[Pre]], t.asInstanceOf[TFloat[Pre]]))
         implicit val o: Origin = expr.o
         FunctionInvocation(f.ref[Function[Post]], Seq(dispatch(e)), Nil, Nil, Nil)(PanicBlame("Can always call cast on float"))
       }

src/rewrite/vct/rewrite/InlineApplicables.scala

@@ -241,6 +241,14 @@ case class InlineApplicables[Pre <: Generation]() extends Rewriter[Pre] with Laz
           case InstancePredicateApply(_, Ref(pred), _, WritePerm()) =>
             dispatch((obj + args).expr(pred.body.getOrElse(throw AbstractInlineable(apply, pred))))
           case InstancePredicateApply(_, Ref(pred), _, _) => ???
+          case CoalesceInstancePredicateApply(_, Ref(pred), _, WritePerm()) =>
+            dispatch((obj + args).expr(
+              Implies(
+                Neq(obj.replacing, Null()),
+                pred.body.getOrElse(throw AbstractInlineable(apply, pred)),
+              )
+            ))
+          case CoalesceInstancePredicateApply(_, Ref(pred), _, _) => ???
         }
       }
 

src/rewrite/vct/rewrite/ResolveExpressionSideEffects.scala

@@ -319,6 +319,27 @@ case class ResolveExpressionSideEffects[Pre <: Generation]() extends Rewriter[Pr
       case assn: SilverFieldAssign[Pre] => rewriteDefault(assn)
       case assn: SilverLocalAssign[Pre] => rewriteDefault(assn)
       case proof: FramedProof[Pre] => rewriteDefault(proof)
+      case extract: Extract[Pre] => rewriteDefault(extract)
+      case branch: IndetBranch[Pre] => rewriteDefault(branch)
+      case LlvmLoop(cond, contract, body) =>
+        evaluateOne(cond) match {
+          case (Nil, Nil, cond) =>
+            LlvmLoop(cond, dispatch(contract), dispatch(body))
+          case (variables, sideEffects, cond) =>
+            val break = new LabelDecl[Post]()(BreakOrigin)
+
+            Block(Seq(
+              LlvmLoop(tt, dispatch(contract), Block(Seq(
+                Scope(variables,
+                  Block(sideEffects :+ Branch(Seq(Not(cond) -> Goto(break.ref))))),
+                dispatch(body),
+              ))),
+              Label(break, Block(Nil)),
+            ))
+        }
+      case rangedFor: RangedFor[Pre] => rewriteDefault(rangedFor)
+      case assign: VeyMontAssignExpression[Pre] => rewriteDefault(assign)
+      case expr: VeyMontCommExpression[Pre] => rewriteDefault(expr)
       case _: CStatement[Pre] => throw ExtraNode
       case _: CPPStatement[Pre] => throw ExtraNode
       case _: JavaStatement[Pre] => throw ExtraNode

src/rewrite/vct/rewrite/SmtlibToProverTypes.scala

@@ -3,13 +3,20 @@ package vct.rewrite
 import vct.col.ast._
 import vct.col.origin.Origin
 import vct.col.rewrite.{Generation, Rewriter, RewriterBuilder, Rewritten}
+import vct.result.VerificationError.UserError
+import vct.rewrite.SmtlibToProverTypes.NotRepresentable
 
 import scala.collection.mutable
 import scala.jdk.StreamConverters.IntStreamHasToScala
 
 case object SmtlibToProverTypes extends RewriterBuilder {
   override def key: String = "smtlib"
   override def desc: String = "Encode smtlib types and functions into their stringified counterpart"
+
+  case class NotRepresentable(t: Type[_]) extends UserError {
+    override def code: String = "notSmtRepresentable"
+    override def text: String = t.o.messageInContext("This type does not have a stable representation on the smt level yet.")
+  }
 }
 
 case class SmtlibToProverTypes[Pre <: Generation]() extends Rewriter[Pre] {
@@ -31,6 +38,7 @@ case class SmtlibToProverTypes[Pre <: Generation]() extends Rewriter[Pre] {
     case TSmtlibString() => "String"
     case TSmtlibRegLan() => "RegLan"
     case TSmtlibSeq(element) => s"(Seq ${smtTypeString(element)})"
+    case other => throw NotRepresentable(other)
   }
 
   val declaredType: mutable.Map[String, ProverType[Post]] = mutable.Map()

src/rewrite/vct/rewrite/adt/ImportADT.scala

@@ -4,7 +4,7 @@ import hre.util.ScopedStack
 import vct.col.ast.RewriteHelpers.RewriteProgram
 import vct.col.ast.`type`.TFloats
 import vct.col.ast.util.Declarator
-import vct.col.ast.{CPPType, CType, Declaration, GlobalDeclaration, JavaType, PVLType, Program, TAny, TArray, TAxiomatic, TBag, TBool, TBoundedInt, TChar, TClass, TEither, TFloat, TFraction, TInt, TMap, TMatrix, TModel, TNotAValue, TNothing, TNull, TOption, TPointer, TProcess, TRational, TRef, TResource, TSeq, TSet, TString, TTuple, TType, TUnion, TVar, TVoid, TZFraction, Type}
+import vct.col.ast._
 import vct.col.typerules.CoercingRewriter
 import vct.col.rewrite.error.ExtraNode
 import vct.col.origin.{Blame, SourceNameOrigin, UnsafeCoercion}
@@ -61,7 +61,22 @@ case object ImportADT {
     case TMap(key, value) => "map$" + typeText(key) + "__" + typeText(value) + "$"
     case TClass(Ref(cls)) => cls.o.preferredName
     case TVar(Ref(v)) => v.o.preferredName
-    case TUnion(ts) => "union$" + ts.map(typeText).mkString("__") + "$"
+    case TUnion(ts) => "union" + ts.map(typeText).mkString("$", "__", "$")
+    case SilverPartialTAxiomatic(Ref(adt), _) => adt.o.preferredName
+    case TAnyClass() => "cls"
+    case TEnum(Ref(enum)) => enum.o.preferredName
+    case TProverType(Ref(t)) => t.o.preferredName
+    case TSYCLQueue() => "syclqueue"
+    case TSeqProg(Ref(prog)) => prog.o.preferredName
+    case TSmtlibArray(index, value) => "smtarr" + (index :+ value).map(typeText).mkString("$" , "__", "$")
+    case TSmtlibBitVector(size) => s"bitvec$size"
+    case TSmtlibFloatingPoint(e, m) => s"fp_${e}_$m"
+    case TSmtlibRegLan() => "reglan"
+    case TSmtlibRoundingMode() => "roundingmode"
+    case TSmtlibSeq(t) => "smtseq$" + typeText(t) + "$"
+    case TSmtlibString() => "smtstr"
+    case TVeyMontChannel(t) => "veymontchan$" + t + "$"
+    case TVeyMontThread(Ref(thread)) => thread.o.preferredName
     case _: JavaType[_] => throw ExtraNode
     case _: CType[_] => throw ExtraNode
     case _: CPPType[_] => throw ExtraNode

src/rewrite/vct/rewrite/bip/BipVerificationResults.scala

@@ -5,6 +5,7 @@ import vct.col.ast.{BipComponent, BipTransition}
 import vct.result.VerificationError
 import vct.result.VerificationError.SystemError
 
+import scala.language.implicitConversions
 import scala.collection.{mutable => mut}
 
 case object BIP {

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

@@ -186,9 +186,8 @@ case class LangCPPToCol[Pre <: Generation](rw: LangSpecificToCol[Pre]) extends L
   def local(local: CPPLocal[Pre]): Expr[Post] = {
     implicit val o: Origin = local.o
     local.ref.get match {
-      case RefAxiomaticDataType(_) => throw NotAValue(local)
-      case RefVariable(decl) => Local(rw.succ(decl))
-      case RefModelField(decl) => ModelDeref[Post](rw.currentThis.top, rw.succ(decl))(local.blame)
+      case spec: SpecNameTarget[Pre] => rw.specLocal(spec, local, local.blame)
+      case _: SpecInvocationTarget[Pre] => throw NotAValue(local)
       case ref: RefCPPParam[Pre] =>
         if (cppCurrentDefinitionParamSubstitutions.nonEmpty)
           Local(cppNameSuccessor.ref(RefCPPParam(cppCurrentDefinitionParamSubstitutions.top.getOrElse(ref.decl, ref.decl))))
@@ -208,32 +207,13 @@ case class LangCPPToCol[Pre <: Generation](rw: LangSpecificToCol[Pre]) extends L
     val CPPInvocation(applicable, args, givenMap, yields) = inv
     implicit val o: Origin = inv.o
     inv.ref.get match {
-      case RefFunction(decl) =>
-        FunctionInvocation[Post](rw.succ(decl), args.map(rw.dispatch), Nil,
-          givenMap.map { case (Ref(v), e) => (rw.succ(v), rw.dispatch(e)) },
-          yields.map { case (e, Ref(v)) => (rw.dispatch(e), rw.succ(v)) })(inv.blame)
-      case RefProcedure(decl) =>
-        ProcedureInvocation[Post](rw.succ(decl), args.map(rw.dispatch), Nil, Nil,
-          givenMap.map { case (Ref(v), e) => (rw.succ(v), rw.dispatch(e)) },
-          yields.map { case (e, Ref(v)) => (rw.dispatch(e), rw.succ(v)) })(inv.blame)
-      case RefPredicate(decl) =>
-        PredicateApply[Post](rw.succ(decl), args.map(rw.dispatch), WritePerm())
-      case RefInstanceFunction(decl) => ???
-      case RefInstanceMethod(decl) => ???
-      case RefInstancePredicate(decl) => ???
-      case RefADTFunction(decl) =>
-        ADTFunctionInvocation[Post](None, rw.succ(decl), args.map(rw.dispatch))
-      case RefModelProcess(decl) =>
-        ProcessApply[Post](rw.succ(decl), args.map(rw.dispatch))
-      case RefModelAction(decl) =>
-        ActionApply[Post](rw.succ(decl), args.map(rw.dispatch))
-      case BuiltinInstanceMethod(f) => ???
+      case spec: SpecInvocationTarget[Pre] =>
+        rw.specInvocation(None, spec, Nil, args, givenMap, yields, inv, inv.blame)
       case ref: RefCPPFunctionDefinition[Pre] =>
         ProcedureInvocation[Post](cppFunctionSuccessor.ref(ref.decl), args.map(rw.dispatch), Nil, Nil,
           givenMap.map { case (Ref(v), e) => (rw.succ(v), rw.dispatch(e)) },
           yields.map { case (e, Ref(v)) => (rw.dispatch(e), rw.succ(v)) })(inv.blame)
       case e: RefCPPGlobalDeclaration[Pre] => globalInvocation(e, inv)
-      case RefProverFunction(decl) => ProverFunctionInvocation(rw.succ(decl), args.map(rw.dispatch))
     }
   }