-
Notifications
You must be signed in to change notification settings - Fork 261
Commit
This commit does not belong to any branch on this repository, and may belong to a fork outside of the repository.
Let
measure-complexity
output the worst performing verification tas…
…ks by resource count (#5631) ### Description - Let `measure-complexity` output the worst performing verification tasks by resource count - Add an option `--top-x` to `measure-complexity` to configure how many of the worst tasks are shown - Change the default of `--iterations` from 10 to 1 ### How has this been tested? - Add a CLI test <small>By submitting this pull request, I confirm that my contribution is made under the terms of the [MIT license](https://github.com/dafny-lang/dafny/blob/master/LICENSE.txt).</small>
- Loading branch information
1 parent
281922d
commit e397b4f
Showing
4 changed files
with
103 additions
and
4 deletions.
There are no files selected for viewing
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
20 changes: 20 additions & 0 deletions
20
Source/IntegrationTests/TestFiles/LitTests/LitTest/cli/measure-complexity.dfy
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Original file line number | Diff line number | Diff line change |
---|---|---|
@@ -0,0 +1,20 @@ | ||
// RUN: %exits-with 4 %baredafny measure-complexity --use-basename-for-filename --isolate-assertions --worst-amount 100 "%s" > %t.raw | ||
// RUN: %sed 's#\): \d+#): <redacted>#g' %t.raw > %t.raw2 | ||
// RUN: %sed 's#are \d+#are <redacted>#g' %t.raw2 > %t | ||
// RUN: %diff "%s.expect" "%t" | ||
method Foo() { | ||
assert Ack(0,0) == 10; | ||
assert Ack(1,3) == 10; | ||
assert Ack(3,3) == 10; | ||
assert Ack(3,4) == 10; | ||
} | ||
|
||
function Ack(m: nat, n: nat): nat | ||
{ | ||
if m == 0 then | ||
n + 1 | ||
else if n == 0 then | ||
Ack(m - 1, 1) | ||
else | ||
Ack(m - 1, Ack(m, n - 1)) | ||
} |
32 changes: 32 additions & 0 deletions
32
Source/IntegrationTests/TestFiles/LitTests/LitTest/cli/measure-complexity.dfy.expect
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Original file line number | Diff line number | Diff line change |
---|---|---|
@@ -0,0 +1,32 @@ | ||
Starting verification of iteration 1/1 with seed 0 | ||
measure-complexity.dfy(6,18): Error: assertion might not hold | ||
The total consumed resources are <redacted> | ||
The most demanding 100 verification tasks consumed these resources: | ||
measure-complexity.dfy(9,18): <redacted> | ||
measure-complexity.dfy(8,18): <redacted> | ||
measure-complexity.dfy(9,15): <redacted> | ||
measure-complexity.dfy(7,18): <redacted> | ||
measure-complexity.dfy(19,4): <redacted> | ||
measure-complexity.dfy(6,18): <redacted> | ||
measure-complexity.dfy(7,15): <redacted> | ||
measure-complexity.dfy(19,10): <redacted> | ||
measure-complexity.dfy(7,13): <redacted> | ||
measure-complexity.dfy(17,4): <redacted> | ||
measure-complexity.dfy(17,15): <redacted> | ||
measure-complexity.dfy(19,15): <redacted> | ||
measure-complexity.dfy(19,24): <redacted> | ||
measure-complexity.dfy(17,10): <redacted> | ||
measure-complexity.dfy(15,6): <redacted> | ||
measure-complexity.dfy(19,4): <redacted> | ||
measure-complexity.dfy(19,4): <redacted> | ||
measure-complexity.dfy(9,13): <redacted> | ||
measure-complexity.dfy(17,4): <redacted> | ||
measure-complexity.dfy(6,13): <redacted> | ||
measure-complexity.dfy(8,15): <redacted> | ||
measure-complexity.dfy(17,4): <redacted> | ||
measure-complexity.dfy(8,13): <redacted> | ||
measure-complexity.dfy(19,15): <redacted> | ||
measure-complexity.dfy(6,15): <redacted> | ||
measure-complexity.dfy(19,15): <redacted> | ||
measure-complexity.dfy(12,9): <redacted> | ||
measure-complexity.dfy(5,7): <redacted> |
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Original file line number | Diff line number | Diff line change |
---|---|---|
@@ -0,0 +1,5 @@ | ||
Let the command `measure-complexity` output which verification tasks performed the worst in terms of resource count. Output looks like: | ||
... | ||
Verification task on line 8 in file measure-complexity.dfy consumed 9984 resources | ||
Verification task on line 7 in file measure-complexity.dfy consumed 9065 resources | ||
... |