added global variable support

utwente-fmt · Jun 30, 2023 · 897b039 · 897b039
1 parent cfead68
commit 897b039
Show file tree

Hide file tree

Showing 3 changed files with 17 additions and 28 deletions.
diff --git a/src/col/vct/col/resolve/Resolve.scala b/src/col/vct/col/resolve/Resolve.scala
@@ -323,10 +323,15 @@ case object ResolveReferences extends LazyLogging {
       if (func.decl.contract.nonEmpty && func.decl.inits.size > 1) {
         throw MultipleForwardDeclarationContractError(func)
       }
-      ctx
-        .declare(CPP.paramsFromDeclarator(func.decl.inits.head.decl) ++ func.decl.contract.givenArgs ++ func.decl.contract.yieldsArgs)
-        .copy(currentResult = CPP.getDeclaratorInfo(func.decl.inits.head.decl)
-          .params.map(_ => RefCPPGlobalDeclaration(func, initIdx = 0)))
+      func.decl.inits.zipWithIndex.foldLeft(
+        ctx.declare(func.decl.contract.givenArgs ++ func.decl.contract.yieldsArgs)
+      ) {
+        case (ctx, (init, idx)) =>
+          val info = CPP.getDeclaratorInfo(init.decl)
+          ctx
+            .declare(info.params.getOrElse(Nil))
+            .copy(currentResult = info.params.map(_ => RefCPPGlobalDeclaration(func, idx)))
+      }
     case func: LlvmFunctionDefinition[G] => ctx
       .copy(currentResult = Some(RefLlvmFunctionDefinition(func)))
     case par: ParStatement[G] => ctx

diff --git a/src/main/vct/main/stages/Resolution.scala b/src/main/vct/main/stages/Resolution.scala
@@ -6,13 +6,11 @@ import org.antlr.v4.runtime.CharStreams
 import vct.col.ast._
 import vct.col.check.CheckError
 import vct.col.origin.{FileSpanningOrigin, LLVMOrigin, Origin}
-import vct.col.resolve.lang.{C, CPP}
 import vct.col.resolve.{Resolve, ResolveReferences, ResolveTypes}
 import vct.col.rewrite.Generation
 import vct.col.rewrite.bip.IsolateBipGlue
 import vct.col.rewrite.lang.{LangSpecificToCol, LangTypesToCol}
 import vct.importer.JavaLibraryLoader
-import vct.main.Main.TemporarilyUnsupported
 import vct.main.stages.Resolution.InputResolutionError
 import vct.options.Options
 import vct.options.types.ClassPathEntry
@@ -96,20 +94,6 @@ case class Resolution[G <: Generation]
   override def progressWeight: Int = 1
 
   override def run(in: ParseResult[G]): Verification[_ <: Generation] = {
-    in.decls.foreach(_.transSubnodes.foreach {
-      case decl: CGlobalDeclaration[_] => decl.decl.inits.foreach(init => {
-        if(C.getDeclaratorInfo(init.decl).params.isEmpty) {
-          throw TemporarilyUnsupported("GlobalCVariable", Seq(decl))
-        }
-      })
-      case decl: CPPGlobalDeclaration[_] => decl.decl.inits.foreach(init => {
-        if (CPP.getDeclaratorInfo(init.decl).params.isEmpty) {
-          throw TemporarilyUnsupported("GlobalCPPVariable", Seq(decl))
-        }
-      })
-      case _ =>
-    })
-
     implicit val o: Origin = FileSpanningOrigin
 
     val parsedProgram = Program(in.decls)(blameProvider())

diff --git a/src/rewrite/vct/rewrite/lang/LangCPPToCol.scala b/src/rewrite/vct/rewrite/lang/LangCPPToCol.scala
@@ -14,12 +14,6 @@ import vct.col.util.SuccessionMap
 import vct.result.VerificationError.UserError
 
 case object LangCPPToCol {
-  case class CPPGlobalStateNotSupported(example: CPPInit[_]) extends UserError {
-    override def code: String = "notSupported"
-
-    override def text: String =
-      example.o.messageInContext("Global variables in C++ are not supported.")
-  }
 
   case class WrongCPPType(decl: CPPLocalDeclaration[_]) extends UserError {
     override def code: String = "wrongCPPType"
@@ -47,6 +41,7 @@ case class LangCPPToCol[Pre <: Generation](rw: LangSpecificToCol[Pre]) extends L
   val cppFunctionSuccessor: SuccessionMap[CPPFunctionDefinition[Pre], Procedure[Post]] = SuccessionMap()
   val cppFunctionDeclSuccessor: SuccessionMap[(CPPGlobalDeclaration[Pre], Int), Procedure[Post]] = SuccessionMap()
   val cppNameSuccessor: SuccessionMap[CPPNameTarget[Pre], Variable[Post]] = SuccessionMap()
+  val cppGlobalNameSuccessor: SuccessionMap[CPPNameTarget[Pre], HeapVariable[Post]] = SuccessionMap()
   val cppCurrentDefinitionParamSubstitutions: ScopedStack[Map[CPPParam[Pre], CPPParam[Pre]]] = ScopedStack()
 
   def rewriteUnit(cppUnit: CPPTranslationUnit[Pre]): Unit = {
@@ -131,7 +126,8 @@ case class LangCPPToCol[Pre <: Generation](rw: LangSpecificToCol[Pre]) extends L
             )(AbstractApplicable)(init.o)
           )
         case None =>
-          throw CPPGlobalStateNotSupported(init)
+          cppGlobalNameSuccessor(RefCPPGlobalDeclaration(decl, idx)) =
+            rw.globalDeclarations.declare(new HeapVariable(t)(init.o))
       }
     }
   }
@@ -190,7 +186,11 @@ case class LangCPPToCol[Pre <: Generation](rw: LangSpecificToCol[Pre]) extends L
         else
           Local(cppNameSuccessor.ref(ref))
       case RefCPPFunctionDefinition(_) => throw NotAValue(local)
-      case RefCPPGlobalDeclaration(_, _) => throw NotAValue(local)
+      case ref @ RefCPPGlobalDeclaration(decl, initIdx) =>
+        CPP.getDeclaratorInfo(decl.decl.inits(initIdx).decl).params match {
+          case None => DerefHeapVariable[Post](cppGlobalNameSuccessor.ref(ref))(local.blame)
+          case Some(_) => throw NotAValue(local)
+        }
       case ref: RefCPPLocalDeclaration[Pre] => Local(cppNameSuccessor.ref(ref))
     }
   }