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

Add :reproducible_resource_limit attribute #796

Merged
merged 5 commits into from
Oct 18, 2023
Merged

Add :reproducible_resource_limit attribute #796

Show file tree
Hide file tree
Changes from all commits
Commits
Show all changes
5 commits
Select commit Hold shift + click to select a range
d282653
Add :reproducible_resource_limit attribute
atomb Oct 13, 2023
05db7d3
Simplify to just removing rlimit multiplication
atomb Oct 17, 2023
446c942
Merge remote-tracking branch 'upstream/master' into reproducible-reso…
atomb Oct 17, 2023
68df232
Fix a test
atomb Oct 17, 2023
bd66afd
Fix one more test
atomb Oct 17, 2023
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
4 changes: 2 additions & 2 deletions Source/ExecutionEngine/CommandLineOptions.cs
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -1206,7 +1206,7 @@ protected override bool ParseOption(string name, CommandLineParseState ps)
return true;

case "rlimit":
ps.GetUnsignedNumericArgument(x => ResourceLimit = x, null);
ps.GetUnsignedNumericArgument(x => ResourceLimit = x);
return true;

case "timeLimitPerAssertionInPercent":
Expand Down Expand Up @@ -1978,7 +1978,7 @@ Set num to 0 to find as many assertion failures as possible.
Limit the number of seconds spent trying to verify
each procedure
/rlimit:<num>
Copy link
Collaborator

@keyboardDrummer keyboardDrummer Oct 16, 2023 •
edited
Loading

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Please update the documentation to say that this option is deprecated and will be removed. I would even prefer already removing it by returning an error when it is used.

Limit the Z3 resource spent trying to verify each procedure
Limit the Z3 resource spent trying to verify each procedure.
/errorTrace:<n>
0 - no Trace labels in the error output,
1 (default) - include useful Trace labels in error output,
Expand Down
2 changes: 1 addition & 1 deletion Source/VCGeneration/Checker.cs
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -150,7 +150,7 @@ private void SetTimeout(uint timeout)

private void SetRlimit(uint rlimit)
{
TheoremProver.SetRlimit(Util.BoundedMultiply(rlimit, 1000));
TheoremProver.SetRlimit(rlimit);
}

/// <summary>
Expand Down
4 changes: 2 additions & 2 deletions Test/test0/MaxKeepGoingSplits.bpl
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -16,7 +16,7 @@ function f(i:int, j:int) returns (int)
}

// Without the max keep going splits this runs out of resources.
procedure {:rlimit 150} test1(x:int)
procedure {:rlimit 150000} test1(x:int)
{
assert(f(8,3) == 0);
assert(f(8,4) == 0);
Expand All @@ -25,7 +25,7 @@ procedure {:rlimit 150} test1(x:int)
}

// Runs out of resources
procedure {:rlimit 150} test2(x:int)
procedure {:rlimit 150000} test2(x:int)
{
assert(f(8,3) == 0 && f(8,4) == 0 && f(8,5) == 0 && f(9,2) == 0);
}
6 changes: 3 additions & 3 deletions Test/test2/Rlimitouts0.bpl
View file
Open in desktop
Original file line number Diff line number Diff line change
@@ -1,5 +1,5 @@
// We use boogie here because parallel-boogie doesn't work well with -proverLog
// RUN: %boogie -rlimit:800 -proverLog:"%t.smt2" "%s"
// RUN: %boogie -rlimit:800000 -proverLog:"%t.smt2" "%s"
// RUN: %OutputCheck --file-to-check "%t.smt2" "%s"
// CHECK-L: (set-option :timeout 0)
// CHECK-L: (set-option :rlimit 800000)
Expand Down Expand Up @@ -43,7 +43,7 @@ procedure TestTimeouts1(in: [int]int, len: int) returns (out: [int]int);
requires 0 < len;
ensures (forall j: int :: 0 <= j && j < len ==> out[j] == j);

implementation {:rlimit 900} TestTimeouts1(in: [int]int, len: int) returns (out: [int]int)
implementation {:rlimit 900000} TestTimeouts1(in: [int]int, len: int) returns (out: [int]int)
{
var i : int;

Expand Down Expand Up @@ -72,7 +72,7 @@ procedure TestTimeouts2(in: [int]int, len: int) returns (out: [int]int);
requires 0 < len;
ensures (forall j: int :: 0 <= j && j < len ==> out[j] == j);

implementation {:rlimit 1000} TestTimeouts2(in: [int]int, len: int) returns (out: [int]int)
implementation {:rlimit 1000000} TestTimeouts2(in: [int]int, len: int) returns (out: [int]int)
{
var i : int;

Expand Down
2 changes: 1 addition & 1 deletion Test/test2/git-issue-366.bpl
View file
Open in desktop
Original file line number Diff line number Diff line change
@@ -1,4 +1,4 @@
// RUN: %parallel-boogie -rlimit:5 /proverOpt:O:smt.qi.eager_threshold=100 "%s" > "%t"
// RUN: %parallel-boogie -rlimit:5000 /proverOpt:O:smt.qi.eager_threshold=100 "%s" > "%t"
// RUN: %diff "%s.expect" "%t"

function f(i:int, j:int) returns (int)
Expand Down
Loading