From 4c858f4bc6142bfd3f8e6b28f2cfc5926d1efa0b Mon Sep 17 00:00:00 2001
From: Roberto Rosmaninho <roberto.rosmaninho@pi2.network>
Date: Thu, 19 Sep 2024 17:02:10 -0300
Subject: [PATCH] Fix `--statistics` flag by calling `get_steps()` instead of
 trying to access the `steps` global variable (#1149)

The previous way of accessing the `steps` global variable was broken,
generating a segmentation fault. By making this simple modification, the
correct number of steps taken by the program execution can be returned
as expected. A regression test to check the correct behavior of this
feature was also added.
---
 runtime/util/finish_rewriting.cpp   | 3 ++-
 test/defn/imp.kore                  | 1 +
 test/lit.cfg.py                     | 5 +++++
 test/output/imp.statistics.out.diff | 2 ++
 4 files changed, 10 insertions(+), 1 deletion(-)
 create mode 100644 test/output/imp.statistics.out.diff

diff --git a/runtime/util/finish_rewriting.cpp b/runtime/util/finish_rewriting.cpp
index fd587d855..98c72900c 100644
--- a/runtime/util/finish_rewriting.cpp
+++ b/runtime/util/finish_rewriting.cpp
@@ -16,7 +16,7 @@ bool binary_output = false;
 bool proof_output = false;
 size_t proof_chunk_size = 0;
 
-extern int64_t steps;
+uint64_t get_steps();
 extern bool safe_partial;
 extern bool proof_hint_instrumentation_slow;
 
@@ -54,6 +54,7 @@ void init_outputs(char const *output_filename) {
   }
 
   if (statistics) {
+    uint64_t steps = get_steps();
     print_statistics(output_file, steps);
   }
 
diff --git a/test/defn/imp.kore b/test/defn/imp.kore
index 6d3528e56..4ac67067f 100644
--- a/test/defn/imp.kore
+++ b/test/defn/imp.kore
@@ -1,5 +1,6 @@
 // RUN: %interpreter
 // RUN: %check-grep
+// RUN: %check-statistics
 // RUN: %proof-interpreter
 // RUN: %check-proof-out
 [topCellInitializer{}(LblinitGeneratedTopCell{}()), org'Stop'kframework'Stop'attributes'Stop'Source{}("Source(/home/robertorosmaninho/rv/k/llvm-backend/src/main/native/llvm-backend/test/defn/k-files/imp.md)")]
diff --git a/test/lit.cfg.py b/test/lit.cfg.py
index 6093c5e6b..1cc74d211 100644
--- a/test/lit.cfg.py
+++ b/test/lit.cfg.py
@@ -134,6 +134,9 @@ def exclude_macos(s):
         %kore-convert %t.out.bin -o %t.out.kore
         %kore-convert %test-diff-out --to=text | diff - %t.out.kore
     ''')),
+    ('%check-statistics', one_line('''
+        %run-statistics | diff - %test-diff-statistics-out
+    ''')),
 
     ('%check-dir-grep', one_line('''
         for out in %test-dir-out/*.out.grep; do
@@ -266,6 +269,7 @@ def exclude_macos(s):
     ('%run-binary-out', 'rm -f %t.out.bin && %t.interpreter %test-input -1 %t.out.bin --binary-output'),
     ('%run-binary', 'rm -f %t.bin && %convert-input && %t.interpreter %t.bin -1 /dev/stdout'),
     ('%run-proof-out', 'rm -f %t.out.bin && %t.interpreter %test-input -1 %t.out.bin --proof-output'),
+    ('%run-statistics', '%t.interpreter %test-input -1 /dev/stdout --statistics'),
     ('%run-proof-chunks-out', 'rm -f %t.out.bin.* && %t.interpreter %test-input -1 %t.out.bin --proof-output --proof-chunk-size 100'),
     ('%run', '%t.interpreter %test-input -1 /dev/stdout'),
 
@@ -278,6 +282,7 @@ def exclude_macos(s):
     ('%test-input', os.path.join('%input-dir', '%test-basename.in')),
     ('%test-grep-out', os.path.join('%output-dir', '%test-basename.out.grep')),
     ('%test-diff-out', os.path.join('%output-dir', '%test-basename.out.diff')),
+    ('%test-diff-statistics-out', os.path.join('%output-dir', '%test-basename.statistics.out.diff')),
     ('%test-dir-out', os.path.join('%output-dir', '%test-basename')),
     ('%test-dir-in', os.path.join('%input-dir', '%test-basename')),
     ('%test-proof-diff-out', os.path.join('%output-dir', '%test-basename.proof.out.diff')),
diff --git a/test/output/imp.statistics.out.diff b/test/output/imp.statistics.out.diff
new file mode 100644
index 000000000..1bbbf3fe3
--- /dev/null
+++ b/test/output/imp.statistics.out.diff
@@ -0,0 +1,2 @@
+4505
+Lbl'-LT-'generatedTop'-GT-'{}(Lbl'-LT-'T'-GT-'{}(Lbl'-LT-'k'-GT-'{}(dotk{}()),Lbl'-LT-'state'-GT-'{}(\left-assoc{}(Lbl'Unds'Map'Unds'{}(Lbl'UndsPipe'-'-GT-Unds'{}(inj{SortId{}, SortKItem{}}(\dv{SortId{}}("s")),inj{SortInt{}, SortKItem{}}(\dv{SortInt{}}("66"))),Lbl'UndsPipe'-'-GT-Unds'{}(inj{SortId{}, SortKItem{}}(\dv{SortId{}}("q")),inj{SortInt{}, SortKItem{}}(\dv{SortInt{}}("1"))),Lbl'UndsPipe'-'-GT-Unds'{}(inj{SortId{}, SortKItem{}}(\dv{SortId{}}("m")),inj{SortInt{}, SortKItem{}}(\dv{SortInt{}}("2"))),Lbl'UndsPipe'-'-GT-Unds'{}(inj{SortId{}, SortKItem{}}(\dv{SortId{}}("r")),inj{SortInt{}, SortKItem{}}(\dv{SortInt{}}("3"))),Lbl'UndsPipe'-'-GT-Unds'{}(inj{SortId{}, SortKItem{}}(\dv{SortId{}}("n")),inj{SortInt{}, SortKItem{}}(\dv{SortInt{}}("1"))))))),Lbl'-LT-'generatedCounter'-GT-'{}(\dv{SortInt{}}("0")))
\ No newline at end of file