From e1bcd218ad071da752fd74da9172776f16adbe67 Mon Sep 17 00:00:00 2001
From: Remy Willems <rwillems@amazon.com>
Date: Tue, 8 Oct 2024 14:19:34 +0200
Subject: [PATCH] Fix concurrency issue

---
 Source/Core/BasicTypeVisitor.cs                    | 14 ++++++++++++--
 Source/VCGeneration/Checker.cs                     |  6 +++++-
 Source/VCGeneration/ConditionGeneration.cs         |  2 +-
 Source/VCGeneration/Splits/Split.cs                |  3 +--
 .../VCGeneration/VerificationConditionGenerator.cs |  2 +-
 5 files changed, 20 insertions(+), 7 deletions(-)

diff --git a/Source/Core/BasicTypeVisitor.cs b/Source/Core/BasicTypeVisitor.cs
index 3fd2ad5ad..a9aaeecf8 100644
--- a/Source/Core/BasicTypeVisitor.cs
+++ b/Source/Core/BasicTypeVisitor.cs
@@ -1,15 +1,25 @@
+using System;
 using System.Collections.Generic;
 
 namespace Microsoft.Boogie;
 
 public class BasicTypeVisitor : ReadOnlyVisitor
 {
+  private readonly Func<Absy, bool> enterNode;
   private HashSet<Type> basicTypes = new();
-  public BasicTypeVisitor(Absy absy)
-  {
+  public BasicTypeVisitor(Absy absy, Func<Absy, bool> enterNode) {
+    this.enterNode = enterNode;
     Visit(absy);
   }
 
+  public override Absy Visit(Absy node) {
+    if (enterNode(node)) {
+      return base.Visit(node);
+    }
+
+    return node;
+  }
+
   public override Type VisitBasicType(BasicType node)
   {
     basicTypes.Add(node);
diff --git a/Source/VCGeneration/Checker.cs b/Source/VCGeneration/Checker.cs
index 49f23b1df..e4ff0b351 100644
--- a/Source/VCGeneration/Checker.cs
+++ b/Source/VCGeneration/Checker.cs
@@ -128,7 +128,11 @@ public Checker(CheckerPool pool, string /*?*/ logFilePath, bool appendLogFile)
 
     public void Target(Program prog, ProverContext ctx, Split split)
     {
-      var usedTypes = new BasicTypeVisitor(prog).GetBasicTypes().ToList();
+      /* We should not traverse implementations other than the current one, because they might be in the process of being modified.
+       */
+      bool EnterNode(Absy node) => node is not Implementation implementation || implementation == split.Implementation;
+
+      var usedTypes = new BasicTypeVisitor(prog, EnterNode).GetBasicTypes().ToList();
       lock (this)
       {
         hasOutput = default;
diff --git a/Source/VCGeneration/ConditionGeneration.cs b/Source/VCGeneration/ConditionGeneration.cs
index 425959f0a..cd720b8cb 100644
--- a/Source/VCGeneration/ConditionGeneration.cs
+++ b/Source/VCGeneration/ConditionGeneration.cs
@@ -85,7 +85,7 @@ void ObjectInvariant()
 
     public Dictionary<Incarnation, Absy> IncarnationOriginMap = new();
 
-    public Program program;
+    public readonly Program program;
     public CheckerPool CheckerPool { get; }
 
     public ConditionGeneration(Program program, CheckerPool checkerPool)
diff --git a/Source/VCGeneration/Splits/Split.cs b/Source/VCGeneration/Splits/Split.cs
index ef80d61fe..3b8b1c6e4 100644
--- a/Source/VCGeneration/Splits/Split.cs
+++ b/Source/VCGeneration/Splits/Split.cs
@@ -56,8 +56,7 @@ public IReadOnlyList<Declaration> PrunedDeclarations {
       int assertionCount;
       double assertionCost; // without multiplication by paths
 
-      public readonly VerificationConditionGenerator /*!*/
-        parent;
+      public readonly VerificationConditionGenerator /*!*/ parent;
 
       public Implementation /*!*/ Implementation => Run.Implementation;
 
diff --git a/Source/VCGeneration/VerificationConditionGenerator.cs b/Source/VCGeneration/VerificationConditionGenerator.cs
index db6af4f90..9ce5d739e 100644
--- a/Source/VCGeneration/VerificationConditionGenerator.cs
+++ b/Source/VCGeneration/VerificationConditionGenerator.cs
@@ -32,7 +32,7 @@ record ImplementationTransformationData
 
   public class VerificationConditionGenerator : ConditionGeneration
   {
-    private static ConditionalWeakTable<Implementation, ImplementationTransformationData> implementationData = new();
+    private static readonly ConditionalWeakTable<Implementation, ImplementationTransformationData> implementationData = new();
 
 
     /// <summary>