Merge remote-tracking branch 'origin/develop'

runtimeverification · Sep 19, 2024 · 444e9ee · 444e9ee
2 parents 8b860f9 + 4c858f4
commit 444e9ee
Show file tree

Hide file tree

Showing 4 changed files with 10 additions and 1 deletion.
diff --git 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
@@ -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
@@ -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
@@ -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")))