From f041ceab2eefafdfa2dba28afa475c1bb155958a Mon Sep 17 00:00:00 2001 From: bors Date: Tue, 3 Sep 2024 06:00:23 +0000 Subject: [PATCH 01/33] Updates submodules --- carbon | 2 +- silicon | 2 +- 2 files changed, 2 insertions(+), 2 deletions(-) diff --git a/carbon b/carbon index 759f3c1e..73bfc173 160000 --- a/carbon +++ b/carbon @@ -1 +1 @@ -Subproject commit 759f3c1e80724d5ab6c53fc9cfb989ccc4be1fc6 +Subproject commit 73bfc173104ae9fc5a199c77ef5ac6d44a39853e diff --git a/silicon b/silicon index 46a35ffb..e3a690b4 160000 --- a/silicon +++ b/silicon @@ -1 +1 @@ -Subproject commit 46a35ffb154afc8962a9e3646673bd62ccff33c4 +Subproject commit e3a690b4279bc88541ad2c424deffac6b7e24d5c From 99bfbf09d506a3216313039dacd5b122f1f5b225 Mon Sep 17 00:00:00 2001 From: marcoeilers Date: Wed, 4 Sep 2024 09:26:17 +0000 Subject: [PATCH 02/33] Updates submodules --- silicon | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/silicon b/silicon index e3a690b4..96892edd 160000 --- a/silicon +++ b/silicon @@ -1 +1 @@ -Subproject commit e3a690b4279bc88541ad2c424deffac6b7e24d5c +Subproject commit 96892edd6829c9da5eb96d5540b545fc8f7390d9 From 5e23335eb0f3bc1ebdcee5148a12c0d9f44ac317 Mon Sep 17 00:00:00 2001 From: Marco Eilers Date: Wed, 4 Sep 2024 11:32:02 +0200 Subject: [PATCH 03/33] Update silicon reference --- silicon | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/silicon b/silicon index e3a690b4..96892edd 160000 --- a/silicon +++ b/silicon @@ -1 +1 @@ -Subproject commit e3a690b4279bc88541ad2c424deffac6b7e24d5c +Subproject commit 96892edd6829c9da5eb96d5540b545fc8f7390d9 From dca6718df5edad5fbbe13c9937c79b3714244d35 Mon Sep 17 00:00:00 2001 From: bors Date: Sun, 8 Sep 2024 06:00:21 +0000 Subject: [PATCH 04/33] Updates submodules --- carbon | 2 +- silicon | 2 +- 2 files changed, 2 insertions(+), 2 deletions(-) diff --git a/carbon b/carbon index 73bfc173..0adb3dcc 160000 --- a/carbon +++ b/carbon @@ -1 +1 @@ -Subproject commit 73bfc173104ae9fc5a199c77ef5ac6d44a39853e +Subproject commit 0adb3dcc1b31a93fc24e40ab0311af886d7eca1e diff --git a/silicon b/silicon index 96892edd..58ba972f 160000 --- a/silicon +++ b/silicon @@ -1 +1 @@ -Subproject commit 96892edd6829c9da5eb96d5540b545fc8f7390d9 +Subproject commit 58ba972fc66e4b7617622878ea6adec7da88bfdc From b3559b04fbd9909fcf192d1c8173f5da847ae8c6 Mon Sep 17 00:00:00 2001 From: bors Date: Fri, 13 Sep 2024 06:00:33 +0000 Subject: [PATCH 05/33] Updates submodules --- carbon | 2 +- silicon | 2 +- 2 files changed, 2 insertions(+), 2 deletions(-) diff --git a/carbon b/carbon index 0adb3dcc..098c7066 160000 --- a/carbon +++ b/carbon @@ -1 +1 @@ -Subproject commit 0adb3dcc1b31a93fc24e40ab0311af886d7eca1e +Subproject commit 098c70669b72cce234ae16963d205322463f1f22 diff --git a/silicon b/silicon index 58ba972f..768a8b60 160000 --- a/silicon +++ b/silicon @@ -1 +1 @@ -Subproject commit 58ba972fc66e4b7617622878ea6adec7da88bfdc +Subproject commit 768a8b600fd69da7166e1888f8f2738c27539e95 From bf2def80e7cdd1fa223c96780e9b1f2113daf1a6 Mon Sep 17 00:00:00 2001 From: bors Date: Mon, 16 Sep 2024 06:00:27 +0000 Subject: [PATCH 06/33] Updates submodules --- carbon | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/carbon b/carbon index 098c7066..d14a703f 160000 --- a/carbon +++ b/carbon @@ -1 +1 @@ -Subproject commit 098c70669b72cce234ae16963d205322463f1f22 +Subproject commit d14a703fc6428fbae54e7333d8ede7efbbf850f0 From 7535a1e3adfdc8a664ebc7820e99372131229655 Mon Sep 17 00:00:00 2001 From: bors Date: Wed, 18 Sep 2024 06:00:39 +0000 Subject: [PATCH 07/33] Updates submodules --- silicon | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/silicon b/silicon index 768a8b60..b737e366 160000 --- a/silicon +++ b/silicon @@ -1 +1 @@ -Subproject commit 768a8b600fd69da7166e1888f8f2738c27539e95 +Subproject commit b737e3663677d77729c9a2eb8de975493bc17c3f From d5057a6d6f021d38a642f11faf92ddf626e8050d Mon Sep 17 00:00:00 2001 From: bors Date: Fri, 27 Sep 2024 06:00:35 +0000 Subject: [PATCH 08/33] Updates submodules --- silicon | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/silicon b/silicon index b737e366..2030e3eb 160000 --- a/silicon +++ b/silicon @@ -1 +1 @@ -Subproject commit b737e3663677d77729c9a2eb8de975493bc17c3f +Subproject commit 2030e3eb63f4b1c92ddc8885f7c937673effc9bd From 8798dd9704a3fa4c14e192837918360ee3d69652 Mon Sep 17 00:00:00 2001 From: bors Date: Thu, 17 Oct 2024 06:00:26 +0000 Subject: [PATCH 09/33] Updates submodules --- silicon | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/silicon b/silicon index 2030e3eb..4d756c79 160000 --- a/silicon +++ b/silicon @@ -1 +1 @@ -Subproject commit 2030e3eb63f4b1c92ddc8885f7c937673effc9bd +Subproject commit 4d756c797d31cb37f03a6e759c7b128bd0e306b5 From 7b04d3a04038f75caf6adff20703fc59993f197d Mon Sep 17 00:00:00 2001 From: bors Date: Fri, 15 Nov 2024 06:00:23 +0000 Subject: [PATCH 10/33] Updates submodules --- carbon | 2 +- silicon | 2 +- 2 files changed, 2 insertions(+), 2 deletions(-) diff --git a/carbon b/carbon index d14a703f..2da52018 160000 --- a/carbon +++ b/carbon @@ -1 +1 @@ -Subproject commit d14a703fc6428fbae54e7333d8ede7efbbf850f0 +Subproject commit 2da52018ead6e1f17fb1c67adc65ecdd4ff6c155 diff --git a/silicon b/silicon index 4d756c79..2257d9c0 160000 --- a/silicon +++ b/silicon @@ -1 +1 @@ -Subproject commit 4d756c797d31cb37f03a6e759c7b128bd0e306b5 +Subproject commit 2257d9c029d368629ed1f831c3c959713b1d1d10 From 2c1362c9c43cc97ed56ec22defae35671e94c04b Mon Sep 17 00:00:00 2001 From: jcp19 Date: Wed, 4 Dec 2024 20:16:14 +0000 Subject: [PATCH 11/33] Updates submodules --- carbon | 2 +- silicon | 2 +- 2 files changed, 2 insertions(+), 2 deletions(-) diff --git a/carbon b/carbon index 2da52018..481ee3fa 160000 --- a/carbon +++ b/carbon @@ -1 +1 @@ -Subproject commit 2da52018ead6e1f17fb1c67adc65ecdd4ff6c155 +Subproject commit 481ee3fab739df243175374e6f22a0268f07d5fc diff --git a/silicon b/silicon index 2257d9c0..61eeb81e 160000 --- a/silicon +++ b/silicon @@ -1 +1 @@ -Subproject commit 2257d9c029d368629ed1f831c3c959713b1d1d10 +Subproject commit 61eeb81ee06f6332477e967aa7ec82011b93287f From 0959fff634b3fe2297c84c5f0f21280c40e788b3 Mon Sep 17 00:00:00 2001 From: bors Date: Fri, 6 Dec 2024 06:00:28 +0000 Subject: [PATCH 12/33] Updates submodules --- silicon | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/silicon b/silicon index 61eeb81e..07bb7d3b 160000 --- a/silicon +++ b/silicon @@ -1 +1 @@ -Subproject commit 61eeb81ee06f6332477e967aa7ec82011b93287f +Subproject commit 07bb7d3bfc2554cbc2aa2168b3bcffe71f5132a7 From 69c059c42520c575469202dadb823afaa8d97dc6 Mon Sep 17 00:00:00 2001 From: bors Date: Sun, 8 Dec 2024 06:00:21 +0000 Subject: [PATCH 13/33] Updates submodules --- carbon | 2 +- silicon | 2 +- 2 files changed, 2 insertions(+), 2 deletions(-) diff --git a/carbon b/carbon index 481ee3fa..1f06ed80 160000 --- a/carbon +++ b/carbon @@ -1 +1 @@ -Subproject commit 481ee3fab739df243175374e6f22a0268f07d5fc +Subproject commit 1f06ed80fa755daac5d5c17a36b38edbbe6c949e diff --git a/silicon b/silicon index 07bb7d3b..f68c1805 160000 --- a/silicon +++ b/silicon @@ -1 +1 @@ -Subproject commit 07bb7d3bfc2554cbc2aa2168b3bcffe71f5132a7 +Subproject commit f68c1805c7774e441d70006d06a2cff7607aa22f From f87df2888529f80201a7519f7cdf496f49a0c9e9 Mon Sep 17 00:00:00 2001 From: bors Date: Tue, 10 Dec 2024 06:00:24 +0000 Subject: [PATCH 14/33] Updates submodules --- silicon | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/silicon b/silicon index f68c1805..efaf7697 160000 --- a/silicon +++ b/silicon @@ -1 +1 @@ -Subproject commit f68c1805c7774e441d70006d06a2cff7607aa22f +Subproject commit efaf7697ce81ebe37ed1408da03e9362c7302abe From 4504fc4d63cefc162c4aac4ee4efd985d0ceb8c8 Mon Sep 17 00:00:00 2001 From: viper-admin <59963956+viper-admin@users.noreply.github.com> Date: Thu, 19 Dec 2024 17:21:37 +0100 Subject: [PATCH 15/33] Updates submodules (#253) Co-authored-by: jcp19 --- carbon | 2 +- silicon | 2 +- 2 files changed, 2 insertions(+), 2 deletions(-) diff --git a/carbon b/carbon index 1f06ed80..61417700 160000 --- a/carbon +++ b/carbon @@ -1 +1 @@ -Subproject commit 1f06ed80fa755daac5d5c17a36b38edbbe6c949e +Subproject commit 6141770038c41f9efd74be7ffee5d6dd6d059f85 diff --git a/silicon b/silicon index efaf7697..88604a20 160000 --- a/silicon +++ b/silicon @@ -1 +1 @@ -Subproject commit efaf7697ce81ebe37ed1408da03e9362c7302abe +Subproject commit 88604a20d877712808ac288df7a89e827b8bd952 From c63c402989c63a79fb6d4d0a3c17f3681120fca3 Mon Sep 17 00:00:00 2001 From: jcp19 Date: Fri, 20 Dec 2024 08:04:41 +0000 Subject: [PATCH 16/33] Updates submodules --- carbon | 2 +- silicon | 2 +- 2 files changed, 2 insertions(+), 2 deletions(-) diff --git a/carbon b/carbon index 61417700..0508e8ff 160000 --- a/carbon +++ b/carbon @@ -1 +1 @@ -Subproject commit 6141770038c41f9efd74be7ffee5d6dd6d059f85 +Subproject commit 0508e8ff6eb460df8b1e3ed970b20f62dd214da5 diff --git a/silicon b/silicon index 88604a20..03e7dab5 160000 --- a/silicon +++ b/silicon @@ -1 +1 @@ -Subproject commit 88604a20d877712808ac288df7a89e827b8bd952 +Subproject commit 03e7dab5bd140f6927e3869bf915a16eec6ddcf5 From aeafb33d80f686dd3874a409f97daefb6ce258a1 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Jo=C3=A3o=20Pereira?= Date: Fri, 20 Dec 2024 16:22:20 +0100 Subject: [PATCH 17/33] Update version of the action create-pull-request to avoid deprecation notice (#255) --- .github/workflows/update-submodules.yml | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/.github/workflows/update-submodules.yml b/.github/workflows/update-submodules.yml index 1b56357b..6f1ebc2c 100644 --- a/.github/workflows/update-submodules.yml +++ b/.github/workflows/update-submodules.yml @@ -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. From 6fb54ca33ddce884cb860b971189607932b9aa8d Mon Sep 17 00:00:00 2001 From: bors <26634292+bors@users.noreply.github.com> Date: Tue, 24 Dec 2024 06:00:26 +0000 Subject: [PATCH 18/33] Updates submodules --- carbon | 2 +- silicon | 2 +- 2 files changed, 2 insertions(+), 2 deletions(-) diff --git a/carbon b/carbon index 0508e8ff..5b32f7fe 160000 --- a/carbon +++ b/carbon @@ -1 +1 @@ -Subproject commit 0508e8ff6eb460df8b1e3ed970b20f62dd214da5 +Subproject commit 5b32f7fe22489d044ff552d158a19bc98479d4cd diff --git a/silicon b/silicon index 03e7dab5..457c6eca 160000 --- a/silicon +++ b/silicon @@ -1 +1 @@ -Subproject commit 03e7dab5bd140f6927e3869bf915a16eec6ddcf5 +Subproject commit 457c6eca2e985bbfd8e32e8389cada402c10463b From 98f31acdf773a1238225f3e61a9f58dd4bf49789 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Jon=C3=A1=C5=A1=20Fiala?= Date: Thu, 26 Dec 2024 12:29:56 +0100 Subject: [PATCH 19/33] Handle `WarningsDuringVerification` in http server --- .../server/frontends/http/jsonWriters/ViperIDEProtocol.scala | 1 + 1 file changed, 1 insertion(+) diff --git a/src/main/scala/viper/server/frontends/http/jsonWriters/ViperIDEProtocol.scala b/src/main/scala/viper/server/frontends/http/jsonWriters/ViperIDEProtocol.scala index fe150218..f89da795 100644 --- a/src/main/scala/viper/server/frontends/http/jsonWriters/ViperIDEProtocol.scala +++ b/src/main/scala/viper/server/frontends/http/jsonWriters/ViperIDEProtocol.scala @@ -493,6 +493,7 @@ object ViperIDEProtocol extends akka.http.scaladsl.marshallers.sprayjson.SprayJs case q: QuantifierInstantiationsMessage => q.toJson case q: QuantifierChosenTriggersMessage => q.toJson case v: VerificationTerminationMessage => v.toJson + case w: WarningsDuringVerification => w.toJson })) }) From b110c74eaa38b306ad5d2d74f393e73389ebd7c4 Mon Sep 17 00:00:00 2001 From: bors <26634292+bors@users.noreply.github.com> Date: Mon, 30 Dec 2024 06:00:26 +0000 Subject: [PATCH 20/33] Updates submodules --- carbon | 2 +- silicon | 2 +- 2 files changed, 2 insertions(+), 2 deletions(-) diff --git a/carbon b/carbon index 5b32f7fe..f7e0a9a7 160000 --- a/carbon +++ b/carbon @@ -1 +1 @@ -Subproject commit 5b32f7fe22489d044ff552d158a19bc98479d4cd +Subproject commit f7e0a9a79a879aee9461d1a328a1c989ec3b1045 diff --git a/silicon b/silicon index 457c6eca..9b1e2cb9 160000 --- a/silicon +++ b/silicon @@ -1 +1 @@ -Subproject commit 457c6eca2e985bbfd8e32e8389cada402c10463b +Subproject commit 9b1e2cb9095419fa96c80877b478f2cb98fbf28a From 374270a14a3f92f8fcda96dfcfdfa8f2d2bc11c1 Mon Sep 17 00:00:00 2001 From: viper-admin <59963956+viper-admin@users.noreply.github.com> Date: Tue, 31 Dec 2024 10:23:54 +0100 Subject: [PATCH 21/33] Updates submodules (#259) Co-authored-by: jcp19 <6281876+jcp19@users.noreply.github.com> --- carbon | 2 +- silicon | 2 +- 2 files changed, 2 insertions(+), 2 deletions(-) diff --git a/carbon b/carbon index f7e0a9a7..645f6bb4 160000 --- a/carbon +++ b/carbon @@ -1 +1 @@ -Subproject commit f7e0a9a79a879aee9461d1a328a1c989ec3b1045 +Subproject commit 645f6bb447cfbd5c303976fbbf61b78abcf154b3 diff --git a/silicon b/silicon index 9b1e2cb9..438bb975 160000 --- a/silicon +++ b/silicon @@ -1 +1 @@ -Subproject commit 9b1e2cb9095419fa96c80877b478f2cb98fbf28a +Subproject commit 438bb975cd4007262681c8e6c815a284763058d9 From 24f3d9ddfde760bc5dab7cdaa0d35fc4c8b0b246 Mon Sep 17 00:00:00 2001 From: jcp19 <6281876+jcp19@users.noreply.github.com> Date: Wed, 8 Jan 2025 15:45:37 +0000 Subject: [PATCH 22/33] Updates submodules --- silicon | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/silicon b/silicon index 438bb975..616f93a0 160000 --- a/silicon +++ b/silicon @@ -1 +1 @@ -Subproject commit 438bb975cd4007262681c8e6c815a284763058d9 +Subproject commit 616f93a0427a4528da85e50702205d8a5e3bb8e1 From e64cc3b127421f2a8301a6cb3a4f2de4580a59bf Mon Sep 17 00:00:00 2001 From: jcp19 <6281876+jcp19@users.noreply.github.com> Date: Fri, 10 Jan 2025 17:31:13 +0000 Subject: [PATCH 23/33] Updates submodules --- carbon | 2 +- silicon | 2 +- 2 files changed, 2 insertions(+), 2 deletions(-) diff --git a/carbon b/carbon index 645f6bb4..9def42ca 160000 --- a/carbon +++ b/carbon @@ -1 +1 @@ -Subproject commit 645f6bb447cfbd5c303976fbbf61b78abcf154b3 +Subproject commit 9def42cad0f44c3bbcdaac9cc3991cf4a1adafa8 diff --git a/silicon b/silicon index 616f93a0..e4141e33 160000 --- a/silicon +++ b/silicon @@ -1 +1 @@ -Subproject commit 616f93a0427a4528da85e50702205d8a5e3bb8e1 +Subproject commit e4141e33db1bde58628aa69e6c7b273159d91236 From d3949f954bb1feb995abe55958f37da6d177cdda Mon Sep 17 00:00:00 2001 From: jcp19 <6281876+jcp19@users.noreply.github.com> Date: Tue, 14 Jan 2025 16:00:50 +0000 Subject: [PATCH 24/33] Updates submodules --- silicon | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/silicon b/silicon index e4141e33..2e6cff1a 160000 --- a/silicon +++ b/silicon @@ -1 +1 @@ -Subproject commit e4141e33db1bde58628aa69e6c7b273159d91236 +Subproject commit 2e6cff1a945ac0a3a6838463880d057eafe54aae From 2bba7574d2c4df37c7809c514b130842da762176 Mon Sep 17 00:00:00 2001 From: Linard Arquint Date: Sat, 18 Jan 2025 23:07:32 +0100 Subject: [PATCH 25/33] resolves a data race resulting in two jobs getting the same jid, which has been observed in a unit test --- src/main/scala/viper/server/vsi/JobPool.scala | 6 +++--- 1 file changed, 3 insertions(+), 3 deletions(-) diff --git a/src/main/scala/viper/server/vsi/JobPool.scala b/src/main/scala/viper/server/vsi/JobPool.scala index e0b12ad5..fc8ab945 100644 --- 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 } From 4d2bedae00f2511c7f257e5ada8ca0405829fb37 Mon Sep 17 00:00:00 2001 From: Linard Arquint Date: Tue, 21 Jan 2025 11:55:53 +0100 Subject: [PATCH 26/33] ensures uniqueness of Terminator actors --- src/main/scala/viper/server/vsi/HTTP.scala | 2 +- src/main/scala/viper/server/vsi/Terminator.scala | 9 +++++++++ src/main/scala/viper/server/vsi/VerificationServer.scala | 2 +- 3 files changed, 11 insertions(+), 2 deletions(-) diff --git a/src/main/scala/viper/server/vsi/HTTP.scala b/src/main/scala/viper/server/vsi/HTTP.scala index 0d54abd0..02755567 100644 --- 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/Terminator.scala b/src/main/scala/viper/server/vsi/Terminator.scala index c4dd85b0..d335424f 100644 --- 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) + val 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 index 5912af1a..ba29596a 100644 --- a/src/main/scala/viper/server/vsi/VerificationServer.scala +++ b/src/main/scala/viper/server/vsi/VerificationServer.scala @@ -280,7 +280,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) } From d6243bd7078484cc74152081baa0f2534407c989 Mon Sep 17 00:00:00 2001 From: Linard Arquint Date: Tue, 21 Jan 2025 12:29:40 +0100 Subject: [PATCH 27/33] val was obviously the wrong keyword --- src/main/scala/viper/server/vsi/Terminator.scala | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/src/main/scala/viper/server/vsi/Terminator.scala b/src/main/scala/viper/server/vsi/Terminator.scala index d335424f..271296e0 100644 --- a/src/main/scala/viper/server/vsi/Terminator.scala +++ b/src/main/scala/viper/server/vsi/Terminator.scala @@ -26,7 +26,7 @@ object Terminator { // 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) - val GetNextTerminatorName: String = s"terminator${terminatorCounter.getAndIncrement()}" + def GetNextTerminatorName: String = s"terminator${terminatorCounter.getAndIncrement()}" def props[R](ast_jobs: JobPool[AstJobId, AstHandle[R]], ver_jobs: JobPool[VerJobId, VerHandle], From 1dbce0be602ab26e7c7343a0ef49d414e9dc3fc6 Mon Sep 17 00:00:00 2001 From: Linard Arquint Date: Fri, 31 Jan 2025 10:06:24 +0100 Subject: [PATCH 28/33] adds Dependabot --- .github/dependabot.yml | 12 ++++++++++++ 1 file changed, 12 insertions(+) create mode 100644 .github/dependabot.yml diff --git a/.github/dependabot.yml b/.github/dependabot.yml new file mode 100644 index 00000000..13109b4a --- /dev/null +++ b/.github/dependabot.yml @@ -0,0 +1,12 @@ +version: 2 + +updates: + - package-ecosystem: github-actions + directory: "/" + schedule: + interval: monthly + day: monday + groups: + all: + patterns: + - "*" From b1cd81f6840aa7cff9c24cfdae92602e1f1d8b4b Mon Sep 17 00:00:00 2001 From: "dependabot[bot]" <49699333+dependabot[bot]@users.noreply.github.com> Date: Fri, 31 Jan 2025 09:07:20 +0000 Subject: [PATCH 29/33] Bump the all group with 5 updates Bumps the all group with 5 updates: | Package | From | To | | --- | --- | --- | | [actions/checkout](https://github.com/actions/checkout) | `3` | `4` | | [actions/upload-artifact](https://github.com/actions/upload-artifact) | `3` | `4` | | [actions/cache](https://github.com/actions/cache) | `3` | `4` | | [actions/download-artifact](https://github.com/actions/download-artifact) | `3` | `4` | | [actions/setup-java](https://github.com/actions/setup-java) | `3` | `4` | Updates `actions/checkout` from 3 to 4 - [Release notes](https://github.com/actions/checkout/releases) - [Changelog](https://github.com/actions/checkout/blob/main/CHANGELOG.md) - [Commits](https://github.com/actions/checkout/compare/v3...v4) Updates `actions/upload-artifact` from 3 to 4 - [Release notes](https://github.com/actions/upload-artifact/releases) - [Commits](https://github.com/actions/upload-artifact/compare/v3...v4) Updates `actions/cache` from 3 to 4 - [Release notes](https://github.com/actions/cache/releases) - [Changelog](https://github.com/actions/cache/blob/main/RELEASES.md) - [Commits](https://github.com/actions/cache/compare/v3...v4) Updates `actions/download-artifact` from 3 to 4 - [Release notes](https://github.com/actions/download-artifact/releases) - [Commits](https://github.com/actions/download-artifact/compare/v3...v4) Updates `actions/setup-java` from 3 to 4 - [Release notes](https://github.com/actions/setup-java/releases) - [Commits](https://github.com/actions/setup-java/compare/v3...v4) --- updated-dependencies: - dependency-name: actions/checkout dependency-type: direct:production update-type: version-update:semver-major dependency-group: all - dependency-name: actions/upload-artifact dependency-type: direct:production update-type: version-update:semver-major dependency-group: all - dependency-name: actions/cache dependency-type: direct:production update-type: version-update:semver-major dependency-group: all - dependency-name: actions/download-artifact dependency-type: direct:production update-type: version-update:semver-major dependency-group: all - dependency-name: actions/setup-java dependency-type: direct:production update-type: version-update:semver-major dependency-group: all ... Signed-off-by: dependabot[bot] --- .github/workflows/license-check.yml | 2 +- .github/workflows/scala.yml | 36 ++++++++++++------------- .github/workflows/update-submodules.yml | 2 +- 3 files changed, 20 insertions(+), 20 deletions(-) diff --git a/.github/workflows/license-check.yml b/.github/workflows/license-check.yml index c286d011..09a74de3 100644 --- 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 index 2f6ba787..290b1a65 100644 --- 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 index 6f1ebc2c..fe2886eb 100644 --- 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 From 77918764d108011283a5f2fc7a705f3944667b8f Mon Sep 17 00:00:00 2001 From: bors <26634292+bors@users.noreply.github.com> Date: Sun, 2 Feb 2025 06:00:29 +0000 Subject: [PATCH 30/33] Updates submodules --- carbon | 2 +- silicon | 2 +- 2 files changed, 2 insertions(+), 2 deletions(-) diff --git a/carbon b/carbon index 9def42ca..3b5cc0f5 160000 --- a/carbon +++ b/carbon @@ -1 +1 @@ -Subproject commit 9def42cad0f44c3bbcdaac9cc3991cf4a1adafa8 +Subproject commit 3b5cc0f53f53054deb28b8fe3bb7518e0dad29b9 diff --git a/silicon b/silicon index 2e6cff1a..eb09327d 160000 --- a/silicon +++ b/silicon @@ -1 +1 @@ -Subproject commit 2e6cff1a945ac0a3a6838463880d057eafe54aae +Subproject commit eb09327dd0498e666ce584a2428735d09faa9158 From ed5a72654e1f59dcad58483021bda1c3cac90d27 Mon Sep 17 00:00:00 2001 From: jcp19 <6281876+jcp19@users.noreply.github.com> Date: Sun, 2 Feb 2025 13:19:05 +0000 Subject: [PATCH 31/33] Updates submodules --- carbon | 2 +- silicon | 2 +- 2 files changed, 2 insertions(+), 2 deletions(-) diff --git a/carbon b/carbon index 3b5cc0f5..23e87086 160000 --- a/carbon +++ b/carbon @@ -1 +1 @@ -Subproject commit 3b5cc0f53f53054deb28b8fe3bb7518e0dad29b9 +Subproject commit 23e87086bd78d78d7c7f7c300300f1abac395693 diff --git a/silicon b/silicon index eb09327d..d573c86f 160000 --- a/silicon +++ b/silicon @@ -1 +1 @@ -Subproject commit eb09327dd0498e666ce584a2428735d09faa9158 +Subproject commit d573c86fd91be0ca03434e02e3624e8ce717ef1f From 646ca10b6a155993e3619a4bb0c30316190a601a Mon Sep 17 00:00:00 2001 From: jcp19 <6281876+jcp19@users.noreply.github.com> Date: Tue, 4 Feb 2025 11:04:20 +0000 Subject: [PATCH 32/33] Updates submodules --- carbon | 2 +- silicon | 2 +- 2 files changed, 2 insertions(+), 2 deletions(-) diff --git a/carbon b/carbon index 23e87086..4508758d 160000 --- a/carbon +++ b/carbon @@ -1 +1 @@ -Subproject commit 23e87086bd78d78d7c7f7c300300f1abac395693 +Subproject commit 4508758d513fd1b97c7ac548ccc40350f2c19530 diff --git a/silicon b/silicon index d573c86f..ccab28cc 160000 --- a/silicon +++ b/silicon @@ -1 +1 @@ -Subproject commit d573c86fd91be0ca03434e02e3624e8ce717ef1f +Subproject commit ccab28cc44cfa57f027780bb29160f7f1195d3ee From 8b69c09ae087870a8f15ca686c99e95a86bd2afa Mon Sep 17 00:00:00 2001 From: jcp19 <6281876+jcp19@users.noreply.github.com> Date: Thu, 6 Feb 2025 09:59:09 +0000 Subject: [PATCH 33/33] Updates submodules --- carbon | 2 +- silicon | 2 +- 2 files changed, 2 insertions(+), 2 deletions(-) diff --git a/carbon b/carbon index 4508758d..c6807b8f 160000 --- a/carbon +++ b/carbon @@ -1 +1 @@ -Subproject commit 4508758d513fd1b97c7ac548ccc40350f2c19530 +Subproject commit c6807b8f0e8b8c16684b91a1d3b9337be559c3ce diff --git a/silicon b/silicon index ccab28cc..16030e9a 160000 --- a/silicon +++ b/silicon @@ -1 +1 @@ -Subproject commit ccab28cc44cfa57f027780bb29160f7f1195d3ee +Subproject commit 16030e9adfbdbad875c68db4c5e4b0c381891f31