Merge remote-tracking branch 'origin/master' into lsp

viperproject · Feb 11, 2025 · 5f19c3e · 5f19c3e
2 parents a033f91 + 858cdde
commit 5f19c3e
Show file tree

Hide file tree

Showing 10 changed files with 49 additions and 28 deletions.
diff --git a/.github/dependabot.yml b/.github/dependabot.yml
@@ -0,0 +1,12 @@
+version: 2
+
+updates:
+  - package-ecosystem: github-actions
+    directory: "/"
+    schedule:
+      interval: monthly
+      day: monday
+    groups:
+      all:
+        patterns:
+          - "*"
diff --git a/.github/workflows/license-check.yml b/.github/workflows/license-check.yml
@@ -17,7 +17,7 @@ jobs:
     runs-on: ubuntu-latest
     steps:
       - name: Checkout ViperServer repo
-        uses: actions/checkout@v3
+        uses: actions/checkout@v4
       - name: Check license headers
         uses: viperproject/check-license-header@v2
         with:

diff --git a/.github/workflows/scala.yml b/.github/workflows/scala.yml
@@ -55,7 +55,7 @@ jobs:
     container: viperproject/viperserver:v4_z3_4.8.7
     steps:
       - name: Checkout ViperServer
-        uses: actions/checkout@v3
+        uses: actions/checkout@v4
         with:
           path: viperserver
           submodules: recursive
@@ -87,7 +87,7 @@ jobs:
           echo "Silver: commit ${{ env.SILICON_SILVER_REF }}" >> versions.txt
         # first line overwrites versions.txt in case it already exists, all other append to the file
       - name: Upload version file
-        uses: actions/upload-artifact@v3
+        uses: actions/upload-artifact@v4
         with:
           name: versions.txt
           path: versions.txt
@@ -97,7 +97,7 @@ jobs:
         # note that the cache path is relative to the directory in which sbt is invoked.
 
       - name: Cache SBT
-        uses: actions/cache@v3
+        uses: actions/cache@v4
         with:
           path: |
             viperserver/sbt-cache/.sbtboot
@@ -115,7 +115,7 @@ jobs:
 
       - name: Upload log files
         if: ${{ failure() }}
-        uses: actions/upload-artifact@v3
+        uses: actions/upload-artifact@v4
         with:
           name: TestLogs
           path: viperserver/logs
@@ -129,7 +129,7 @@ jobs:
         working-directory: viperserver/target/universal/stage/lib
 
       - name: Upload ViperServer skinny JARs
-        uses: actions/upload-artifact@v3
+        uses: actions/upload-artifact@v4
         with:
           name: viperserver-skinny-jars
           path: viperserver/viperserver-skinny-jars.zip
@@ -139,7 +139,7 @@ jobs:
         working-directory: viperserver
 
       - name: Upload ViperServer fat JAR
-        uses: actions/upload-artifact@v3
+        uses: actions/upload-artifact@v4
         with:
           name: viperserver-fat-jar
           path: viperserver/target/scala-2.13/viperserver.jar
@@ -149,7 +149,7 @@ jobs:
         working-directory: viperserver
 
       - name: Upload ViperServer test fat JAR
-        uses: actions/upload-artifact@v3
+        uses: actions/upload-artifact@v4
         with:
           name: viperserver-test-fat-jar
           path: viperserver/target/scala-2.13/viperserver-test.jar
@@ -171,20 +171,20 @@ jobs:
     steps:
       # we need to checkout the repo to have access to the test files
       - name: Checkout ViperServer
-        uses: actions/checkout@v3
+        uses: actions/checkout@v4
         with:
           path: viperserver
 
       # we need to checkout the silicon repo to have access to the logback configuration file
       # as we do not use anything else except the logback config, we simply take the latest master branch (in all configurations)
       - name: Checkout Silicon
-        uses: actions/checkout@v3
+        uses: actions/checkout@v4
         with:
           repository: viperproject/silicon
           path: silicon
 
       - name: Download ViperServer test fat JAR
-        uses: actions/download-artifact@v3
+        uses: actions/download-artifact@v4
         with:
           name: viperserver-test-fat-jar
           path: viperserver
@@ -244,7 +244,7 @@ jobs:
         shell: bash
 
       - name: Setup Java JDK
-        uses: actions/setup-java@v3
+        uses: actions/setup-java@v4
         with:
           java-version: '11'
           distribution: 'temurin'
@@ -265,7 +265,7 @@ jobs:
 
       - name: Upload log files
         if: ${{ failure() }}
-        uses: actions/upload-artifact@v3
+        uses: actions/upload-artifact@v4
         with:
           name: TestLogs-${{ runner.os }}
           path: viperserver/logs
@@ -281,19 +281,19 @@ jobs:
         run: sudo apt-get install curl
 
       - name: Download ViperServer skinny JARs
-        uses: actions/download-artifact@v3
+        uses: actions/download-artifact@v4
         with:
           name: viperserver-skinny-jars
           path: deploy
 
       - name: Download ViperServer fat JAR
-        uses: actions/download-artifact@v3
+        uses: actions/download-artifact@v4
         with:
           name: viperserver-fat-jar
           path: deploy
 
       - name: Download version file
-        uses: actions/download-artifact@v3
+        uses: actions/download-artifact@v4
         with:
           name: versions.txt
 
@@ -365,19 +365,19 @@ jobs:
     runs-on: ubuntu-latest
     steps:
       - name: Download ViperServer skinny JARs
-        uses: actions/download-artifact@v3
+        uses: actions/download-artifact@v4
         with:
           name: viperserver-skinny-jars
           path: deploy
 
       - name: Download ViperServer fat JAR
-        uses: actions/download-artifact@v3
+        uses: actions/download-artifact@v4
         with:
           name: viperserver-fat-jar
           path: deploy
 
       - name: Download version file
-        uses: actions/download-artifact@v3
+        uses: actions/download-artifact@v4
         with:
           name: versions.txt
 

diff --git a/.github/workflows/update-submodules.yml b/.github/workflows/update-submodules.yml
@@ -17,7 +17,7 @@ jobs:
     runs-on: ubuntu-latest
     steps:
       - name: Check out the repo
-        uses: actions/checkout@v3
+        uses: actions/checkout@v4
         with:
           submodules: true
 
@@ -54,7 +54,7 @@ jobs:
 
       - name: Open a pull request
         id: pr
-        uses: peter-evans/create-pull-request@v4
+        uses: peter-evans/create-pull-request@v7
         if: (env.PREV_SILICON_REF != env.CUR_SILICON_REF) || (env.PREV_CARBON_REF != env.CUR_CARBON_REF)
         with:
           # Use viper-admin's token to workaround a restriction of GitHub.

diff --git a/carbon b/carbon
diff --git a/silicon b/silicon
diff --git a/src/main/scala/viper/server/vsi/HTTP.scala b/src/main/scala/viper/server/vsi/HTTP.scala
@@ -78,7 +78,7 @@ trait VerificationServerHttp extends VerificationServer with CustomizableHttp {
     ast_jobs = new JobPool("AST-pool", active_jobs)
     ver_jobs = new JobPool("Verification-pool", active_jobs)
     bindingFuture = Http().newServerAt("localhost", port).bindFlow(setRoutes())
-    _termActor = system.actorOf(Terminator.props(ast_jobs, ver_jobs, Some(bindingFuture)), "terminator")
+    _termActor = system.actorOf(Terminator.props(ast_jobs, ver_jobs, Some(bindingFuture)), Terminator.GetNextTerminatorName)
     bindingFuture.map { serverBinding =>
       val newPort = serverBinding.localAddress.getPort
       if (port == 0) {

diff --git a/src/main/scala/viper/server/vsi/JobPool.scala b/src/main/scala/viper/server/vsi/JobPool.scala
@@ -10,6 +10,7 @@ import akka.actor.ActorRef
 import akka.stream.scaladsl.SourceQueueWithComplete
 import org.reactivestreams.Publisher
 
+import java.util.concurrent.atomic.AtomicInteger
 import scala.collection.mutable
 import scala.concurrent.{Future, Promise}
 
@@ -56,14 +57,14 @@ class JobPool[S <: JobId, T <: JobHandle](val tag: String, val MAX_ACTIVE_JOBS:
   private val _jobCache: mutable.Map[S, Future[T]] = mutable.Map()
   def jobHandles: Map[S, Future[T]] = _jobHandles.map{ case (id, hand) => (id, hand.future) }.toMap
 
-  private var _nextJobId: Int = 0
+  private val _nextJobId: AtomicInteger = new AtomicInteger(0)
 
   def newJobsAllowed: Boolean = jobHandles.size < MAX_ACTIVE_JOBS
 
   def bookNewJob(job_executor: S => Future[T]): S = {
     require(newJobsAllowed)
 
-    val new_jid: S = jid_fact(_nextJobId)
+    val new_jid: S = jid_fact(_nextJobId.getAndIncrement())
 
     _jobHandles(new_jid) = Promise()
     _jobExecutors(new_jid) = () => {
@@ -79,7 +80,6 @@ class JobPool[S <: JobId, T <: JobHandle](val tag: String, val MAX_ACTIVE_JOBS:
         t_fut
       }
     }
-    _nextJobId = _nextJobId + 1
     new_jid
   }
 

diff --git a/src/main/scala/viper/server/vsi/Terminator.scala b/src/main/scala/viper/server/vsi/Terminator.scala
@@ -10,6 +10,7 @@ import akka.actor.{Actor, Props}
 import akka.http.scaladsl.Http
 import viper.server.core.VerificationExecutionContext
 
+import java.util.concurrent.atomic.AtomicInteger
 import scala.concurrent.Future
 
 // --- Actor: Terminator ---
@@ -19,6 +20,14 @@ object Terminator {
   case object Exit
   case class WatchJobQueue(jid: JobId, handle: JobHandle)
 
+  // Each server start creates a new Terminator actor. Akka does not like non-unique actor names.
+  // Thus, we increment a counter to ensure unique names for our Terminator actors even though at no point
+  // two of them should be active.
+  // Without this counter, the issue of non-unique actor names occurs in testing contexts as, e.g. in Gobra's tests,
+  // we start a new ViperServer instance for each testcase that needs it.
+  private val terminatorCounter = new AtomicInteger(0)
+  def GetNextTerminatorName: String = s"terminator${terminatorCounter.getAndIncrement()}"
+
   def props[R](ast_jobs: JobPool[AstJobId, AstHandle[R]],
                ver_jobs: JobPool[VerJobId, VerHandle],
                bindingFuture: Option[Future[Http.ServerBinding]] = None)

diff --git a/src/main/scala/viper/server/vsi/VerificationServer.scala b/src/main/scala/viper/server/vsi/VerificationServer.scala
@@ -319,7 +319,7 @@ trait DefaultVerificationServerStart extends VerificationServer {
   override def start(active_jobs: Int): Future[Done] = {
     ast_jobs = new JobPool("VSI-AST-pool", active_jobs)
     ver_jobs = new JobPool("VSI-Verification-pool", active_jobs)
-    _termActor = system.actorOf(Terminator.props(ast_jobs, ver_jobs), "terminator")
+    _termActor = system.actorOf(Terminator.props(ast_jobs, ver_jobs), Terminator.GetNextTerminatorName)
     isRunning = true
     Future.successful(Done)
   }
+2 −2		.github/workflows/ci.yml
+1 −1		project/plugins.sbt
+1 −1		silver
+6 −0		src/main/scala/viper/carbon/CarbonVerifier.scala
+4 −1		src/main/scala/viper/carbon/modules/PermModule.scala
+8 −0		src/main/scala/viper/carbon/modules/impls/DefaultExpModule.scala
+52 −15		src/main/scala/viper/carbon/modules/impls/DefaultFuncPredModule.scala
+4 −3		src/main/scala/viper/carbon/modules/impls/DefaultMainModule.scala
+3 −3		src/main/scala/viper/carbon/modules/impls/DefaultWandModule.scala
+99 −54		src/main/scala/viper/carbon/modules/impls/QuantifiedPermModule.scala
+3 −1		src/main/scala/viper/carbon/modules/impls/sequence_axioms/SequenceAxiomatization.scala
+2 −0		src/main/scala/viper/carbon/verifier/Verifier.scala
+10 −1		src/test/scala/viper/carbon/AllTests.scala
+27 −0		src/test/scala/viper/carbon/CarbonTestsOldPermissionSemantics.scala
+2 −2		.github/workflows/ci.yml
+1 −44		annotation/Terms.example.scala
+2 −2		project/plugins.sbt
+1 −1		silver
+1 −1		src/main/resources/dafny_axioms/sequences.vpr
+6 −0		src/main/scala/Config.scala
+65 −9		src/main/scala/Utils.scala
+288 −0		src/main/scala/debugger/DebugExp.scala
+52 −0		src/main/scala/debugger/DebugParser.scala
+32 −0		src/main/scala/debugger/DebugTypechecker.scala
+570 −0		src/main/scala/debugger/SiliconDebugger.scala
+153 −90		src/main/scala/decider/Decider.scala
+225 −13		src/main/scala/decider/PathConditions.scala
+22 −5		src/main/scala/decider/ProverStdIO.scala
+1 −1		src/main/scala/decider/TermToSMTLib2Converter.scala
+3 −3		src/main/scala/decider/TermToZ3APIConverter.scala
+28 −4		src/main/scala/decider/Z3ProverAPI.scala
+1 −2		src/main/scala/decider/Z3ProverStdIO.scala
+16 −11		src/main/scala/extensions/ConditionalPermissionRewriter.scala
+25 −5		src/main/scala/interfaces/Verification.scala
+15 −0		src/main/scala/interfaces/decider/Prover.scala
+17 −4		src/main/scala/interfaces/state/Chunks.scala
+3 −3		src/main/scala/logger/SymbExLogger.scala
+1 −1		src/main/scala/logger/records/data/DeciderAssumeRecord.scala
+3 −3		src/main/scala/logger/records/data/SingleMergeRecord.scala
+11 −12		src/main/scala/logger/writer/SymbExLogReportWriter.scala
+8 −5		src/main/scala/reporting/Converter.scala
+2 −2		src/main/scala/reporting/Formatters.scala
+53 −30		src/main/scala/resources/NonQuantifiedPropertyInterpreter.scala
+112 −77		src/main/scala/resources/PropertyInterpreter.scala
+19 −8		src/main/scala/resources/QuantifiedPropertyInterpreter.scala
+22 −8		src/main/scala/resources/ResourceDescriptions.scala
+28 −20		src/main/scala/rules/Brancher.scala
+66 −42		src/main/scala/rules/ChunkSupporter.scala
+144 −79		src/main/scala/rules/Consumer.scala
+4 −3		src/main/scala/rules/ConsumptionResult.scala
+557 −341		src/main/scala/rules/Evaluator.scala
+134 −74		src/main/scala/rules/Executor.scala
+35 −23		src/main/scala/rules/HavocSupporter.scala
+18 −6		src/main/scala/rules/Joiner.scala
+4 −4		src/main/scala/rules/LetSupporter.scala
+77 −44		src/main/scala/rules/MagicWandSupporter.scala
+182 −68		src/main/scala/rules/MoreCompleteExhaleSupporter.scala
+5 −3		src/main/scala/rules/PermissionSupporter.scala
+57 −26		src/main/scala/rules/PredicateSupporter.scala
+91 −48		src/main/scala/rules/Producer.scala
+523 −153		src/main/scala/rules/QuantifiedChunkSupport.scala
+98 −44		src/main/scala/rules/StateConsolidator.scala
+42 −4		src/main/scala/rules/SymbolicExecutionRules.scala
+90 −23		src/main/scala/state/Chunks.scala
+69 −43		src/main/scala/state/State.scala
+22 −12		src/main/scala/state/Store.scala
+17 −50		src/main/scala/state/Terms.scala
+43 −3		src/main/scala/state/Utils.scala
+1 −1		src/main/scala/state/package.scala
+2 −2		src/main/scala/supporters/BuiltinDomainsContributor.scala
+2 −2		src/main/scala/supporters/Domains.scala
+1 −1		src/main/scala/supporters/MethodSupporter.scala
+5 −3		src/main/scala/supporters/QuantifierSupporter.scala
+7 −6		src/main/scala/supporters/SnapshotSupporter.scala
+13 −2		src/main/scala/supporters/functions/FunctionData.scala
+1 −1		src/main/scala/supporters/functions/FunctionRecorder.scala
+30 −14		src/main/scala/supporters/functions/FunctionVerificationUnit.scala
+9 −5		src/main/scala/supporters/functions/HeapAccessReplacingExpressionTranslator.scala
+16 −5		src/main/scala/verifier/DefaultMainVerifier.scala
+4 −2		src/main/scala/verifier/VerificationPoolManager.scala
+29 −1		src/main/scala/verifier/Verifier.scala
+2 −1		src/main/scala/verifier/WorkerVerifier.scala
+3 −4		src/test/resources/moreCompleteExhale/0523.vpr
+25 −0		src/test/resources/moreCompleteExhale/0896.vpr
+2 −2		src/test/scala/CounterexampleTests.scala
+15 −0		src/test/scala/SiliconTestsOldPermSemantics.scala