Out of resources error reporting

[keyboardDrummer]

Description

• When reporting a verification issue other than an assertion failure, such as running out of resources, use the token of the assertion batch, not of the entire verifiable symbol. This allows the user to figure out where the bad assertion is, and prevents duplicate error messages.
• Report the result of verification when using the --progress option
• Tweak the formatting of --progress

Examples

lemma{:resource_limit 10000000} L()
{
  assert true;
  assert f(10, 5) == 0; // runs out of resources
  assert true;
  assert f(10, 6) == 0; // runs out of resources
}

Results in

outOfResourceAndIsolateAssertions.dfy(4,18): Error: Verification out of resource (L)
outOfResourceAndIsolateAssertions.dfy(6,18): Error: Verification out of resource (L)

New look of --progress:

Verification part 7/9 of L, on line 6, verified successfully, taking 32ms and consuming 6.8E+003 resources
Verification part 8/9 of L, on line 4, ran out of resources, taking 23ms and consuming 1.0E+007 resources
Verification part 9/9 of L, on line 6, ran out of resources, taking 48ms and consuming 1.0E+007 resources

How has this been tested?

• Add a CLI test outOfResourceAndIsolateAssertions.dfy
• Update existing tests using --progress

By submitting this pull request, I confirm that my contribution is made under the terms of the MIT license.

[MikaelMayer]

Knowing which single assertion times out will be very useful for verification debugging.

[MikaelMayer]

What does "redacted" mean?

[keyboardDrummer]

Because the time taken is not consistent over runs, I replace it with "redacted" in tests using sed.

[MikaelMayer]

I know you replace it with "redacted", my question was really about the meaning of "redacted".
I don't know the rationale behind choosing "redacted" for that replacement. For me, "redacted" means "edit (text) for publication.".
If it was me, I would have just removed the variable part, so that the error would look like "verified successfully and consuming ...."
So my question is, why was the word "redacted" chosen here?

[keyboardDrummer]

I'm using it as a means to say "there was something else here, but it has been removed"