From 46a42487cb032637f2466d06c43767c316839083 Mon Sep 17 00:00:00 2001
From: Aaron Tomb <aarotomb@amazon.com>
Date: Fri, 19 Apr 2024 12:43:07 -0700
Subject: [PATCH] Log exit codes during verification

Temporary debugging code to help diagnose what seem like incorrect exit
codes.
---
 SmithyDafnyMakefile.mk | 14 ++++----------
 run-dafny.sh           | 11 +++++++++++
 2 files changed, 15 insertions(+), 10 deletions(-)
 create mode 100755 run-dafny.sh

diff --git a/SmithyDafnyMakefile.mk b/SmithyDafnyMakefile.mk
index 19e84a8e87..501714ede8 100644
--- a/SmithyDafnyMakefile.mk
+++ b/SmithyDafnyMakefile.mk
@@ -79,16 +79,10 @@ GRADLEW := $(SMITHY_DAFNY_ROOT)/codegen/gradlew
 verify:Z3_PROCESSES=$(shell echo $$(( $(CORES) >= 3 ? 2 : 1 )))
 verify:DAFNY_PROCESSES=$(shell echo $$(( ($(CORES) - 1 ) / ($(CORES) >= 3 ? 2 : 1))))
 verify:
-	find . -name '*.dfy' | xargs -n 1 -P $(DAFNY_PROCESSES) -I % dafny \
-		-vcsCores:$(Z3_PROCESSES) \
-		-compile:0 \
-		-definiteAssignment:3 \
-		-unicodeChar:0 \
-		-functionSyntax:3 \
-		-verificationLogger:csv \
-		-timeLimit:$(VERIFY_TIMEOUT) \
-		-trace \
-		%
+	@find . -name '*.dfy' | xargs -n 1 -P $(DAFNY_PROCESSES) -I % \
+		$(SMITHY_DAFNY_ROOT)/run-dafny.sh $(Z3_PROCESSES) $(VERIFY_TIMEOUT) % ;\
+	EXIT_CODE=$$?;\
+	echo "Overall verification has exit code $$EXIT_CODE"
 
 # Verify single file FILE with text logger.
 # This is useful for debugging resource count usage within a file.
diff --git a/run-dafny.sh b/run-dafny.sh
new file mode 100755
index 0000000000..b1f0cde4e7
--- /dev/null
+++ b/run-dafny.sh
@@ -0,0 +1,11 @@
+dafny \
+		-vcsCores:$1 \
+		-compile:0 \
+		-definiteAssignment:3 \
+		-unicodeChar:0 \
+		-functionSyntax:3 \
+		-verificationLogger:csv \
+		-timeLimit:$2 \
+		-trace \
+		$3
+echo "$3 has exit code $?"