From d29d5f2c1fd94bf2336b3b450efb798cb9b4c9c3 Mon Sep 17 00:00:00 2001
From: Remy Willems <rwillems@amazon.com>
Date: Thu, 21 Mar 2024 13:27:47 +0100
Subject: [PATCH] Report resolution errors to downstream system

---
 Source/ExecutionEngine/ExecutionEngine.cs | 27 ++++++++++++++++++++---
 1 file changed, 24 insertions(+), 3 deletions(-)

diff --git a/Source/ExecutionEngine/ExecutionEngine.cs b/Source/ExecutionEngine/ExecutionEngine.cs
index 25553a0a0..42b13a615 100644
--- a/Source/ExecutionEngine/ExecutionEngine.cs
+++ b/Source/ExecutionEngine/ExecutionEngine.cs
@@ -702,9 +702,30 @@ private async Task<PipelineOutcome> VerifyEachImplementation(TextWriter outputWr
 
     }
 
-    public IReadOnlyList<IVerificationTask> GetVerificationTasks(Program program) {
-      program.Resolve(Options);
-      program.Typecheck(Options);
+    class CollectingErrorSink : IErrorSink
+    {
+      public readonly List<(IToken Token, string Message)> Errors = new();
+      
+      public void Error(IToken tok, string msg)
+      {
+        Errors.Add((tok, msg));
+      }
+    }
+    
+    public IReadOnlyList<IVerificationTask> GetVerificationTasks(Program program)
+    {
+      var sink = new CollectingErrorSink();
+      var resolutionErrors = program.Resolve(Options, sink);
+      var errors = string.Join("\n", sink.Errors.Select(t => $"{t.Token}: {t.Message}"));
+      if (resolutionErrors > 0)
+      {
+        throw new Exception($"Boogie program had {resolutionErrors} resolution errors:\n{errors}");
+      }
+      var typeErrors = program.Typecheck(Options, sink);
+      if (typeErrors > 0)
+      {
+        throw new Exception($"Boogie program had {typeErrors} type errors:\n{errors}");
+      }
 
       EliminateDeadVariables(program);
       CollectModSets(program);