Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Jump to bottom

Fix --statistics flag by calling get_steps() instead of trying to access the steps global variable #1149

Merged
merged 5 commits into from
Sep 19, 2024
Merged

Fix --statistics flag by calling get_steps() instead of trying to access the steps global variable #1149

Show file tree
Hide file tree
Changes from 2 commits
Commits
Show all changes
5 commits
Select commit Hold shift + click to select a range
ea3cf9a
Fix `--statistics` flag by calling `get_steps()` instead of trying to…
Robertorosmaninho Sep 18, 2024
f72ddf0
Adding test to `statistics` feature
Robertorosmaninho Sep 18, 2024
971cc44
Using `uint64_t` instead of `int` and `int64_t` to avoid overflow
Robertorosmaninho Sep 18, 2024
a061d54
Deleting unused diff output file
Robertorosmaninho Sep 18, 2024
1439c9f
Merge branch 'develop' into fix-statistics
Robertorosmaninho Sep 19, 2024
File filter

Filter by extension

Filter by extension
Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
3 changes: 2 additions & 1 deletion runtime/util/finish_rewriting.cpp
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -15,7 +15,7 @@ bool statistics = false;
bool binary_output = false;
bool proof_output = false;

extern int64_t steps;
int64_t get_steps();
theo25 marked this conversation as resolved.
Show resolved Hide resolved
extern bool safe_partial;
extern bool proof_hint_instrumentation_slow;

Expand Down Expand Up @@ -51,6 +51,7 @@ void init_outputs(char const *output_filename) {
}

if (statistics) {
int steps = get_steps();
theo25 marked this conversation as resolved.
Show resolved Hide resolved
print_statistics(output_file, steps);
}

Expand Down
1 change: 1 addition & 0 deletions test/defn/imp.kore
View file
Open in desktop
Original file line number Diff line number Diff line change
@@ -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)")]
Expand Down
5 changes: 5 additions & 0 deletions test/lit.cfg.py
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -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
Expand Down Expand Up @@ -238,6 +241,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', '%t.interpreter %test-input -1 /dev/stdout'),

('%kprint-check', 'kprint %S %s true | diff - %s.out'),
Expand All @@ -249,6 +253,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')),
Expand Down
1 change: 1 addition & 0 deletions test/output/imp.out.diff
View file
Open in desktop
Original file line number Diff line number Diff line change
@@ -0,0 +1 @@
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")))
Robertorosmaninho marked this conversation as resolved.
Show resolved Hide resolved
2 changes: 2 additions & 0 deletions test/output/imp.statistics.out.diff
View file
Open in desktop
Original file line number Diff line number Diff line change
@@ -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")))
Loading