Improve reviewability of extracted tests (for SMTChecker tests and source locations in general).

[ekpyron]

Especially for the SMTChecker tests reviews would be much simpler, if one could check out the branch locally, build isoltest and have it run all tests touched in the diff from develop. In this mode isoltest should single-step through the test expectations and highlight each one (even if succeesding) in the source with full error message (including secondary location - although we might add those to the expectations anyways).

If we'd want to be fancy, this mode in isoltest could even have the option to either agree with the test or open an editor, in which a message could be typed that would automatically be added as a comment to the PR (that should work using the github command line tools) - but even without that, it'd be a big help.

(ping @leonardoalt for comments)

[chriseth]

So the main issue here is that when looking at the test file itself, it is not easily visible what the error message refers to, right?
Or is it just about the secondary locations?

Is there a way to fix that in the test format itself?

Not specific to SMT checker, some ideas:

contract C {
  function f() {} //Error: No visibility specified. Did you intend to add "public"?
}

contract C {
  function f() {} //E[1]
}
// [1]: Error: No visibility specified. Did you intend to add "public"?

contract C {
  /*E[1]*/function f() {}/*[1]E*/
}
// [1]: Error: No visibility specified. Did you intend to add "public"?

[ekpyron]

It's a bit of both... With the SMT checker tests, especially after the counterexamples, I'm not sure they'd fit into an inline expectation all that well... and even if so, then having three of those might inflate the test case that much, s.t. it's hard to read it at once... (and SMTChecker tests often justifiably have several assertions in them...)

On the other hand, if isoltest highlighted the assertion for me and displayed me a full counterexample call chain or model for each assertion, one by one, then reviewing would be trivial...

But yeah, if we found a way to improve this without having to locally compile a PR branch and run something, it'd of course be better...

Your suggestion with the markers could work, would need to see it in action...

[leonardoalt]

But yeah, if we found a way to improve this without having to locally compile a PR branch and run something, it'd of course be better...

Also that, I think having to compile a branch locally in order to review a PR sounds like a lot of overhead

[ekpyron]

Maybe the two aren't mutually exclusive... I still think a review mode for isoltest on a PR diff with step-by-step highlighting would make reviewing of test-heavy and especially SMT PRs much easier, even if we had a nicer way to display things on github - depending on the size of the PR the overhead of building locally would be well worth it.
But even if I manage to convince you of that, we should still not take that as an excuse for not trying to improve the expectations in the test files and on github - in the end having both would be best.

[ekpyron]

We could actually even use the actual source locations as reported by the error reporter, i.e. for

contract C {
  function f() {}
}

The (relevant parts of the) output of solc is

Error: No visibility specified. Did you intend to add "public"?
 --> test.sol:2:3:
  |
2 |   function f() {}
  |   ^^^^^^^^^^^^^^^

So we could take the source location part and e.g. have

contract C {
  function f() {}
//^^^^^^^^^^^^^^^ [1] Error: No visibility specified. Did you intend to add "public"?
}

That way we could even hook into secondary locations as well... Multiple errors on the same line should also work like this (using multiple such comments below that line)...

[mijovic]

@ekpyron I like your idea.

Even starting with having line:column like in error reported in test expectations would make it better.

[ekpyron]

It doesn't really work well for multi-line source locations, though... the error reporter just says

Error: No visibility specified. Did you intend to add "public"?
 --> test.sol:2:3:
  |
2 |   function f()
  |   ^ (Relevant source part starts here and spans across multiple lines).

Not sure how best to deal with those... multi-line source locations could be treated differently, but at some point this will just be confusing, if we overdo it...

[leonardoalt]

Would this update the file or just be used for visualization?

[ekpyron]

I meant it as a new formatting in the file... Haha, imagine the size of the PR that would change this :-D...

For visualization the colored highlighting in isoltest is just fine I think (even though we could still have an option that makes it single-step).

[leonardoalt]

True, but then you have to checkout and compile the branch yourself just to review the PR, not ideal.

[ekpyron]

Maybe we should split the issue - both having better formatting in the actual file and having a review isoltest mode (in case one wants to bother compiling for the added convenience) would be good IMHO.

[leonardoalt]

One simple way, as a reviewer, is also to enforce the author to comment above the assert the reason why it fails. I wrote that in complex cases, but not all. Maybe I should stop being lazy and just enforce that.

[ekpyron]

We have been saying on several occasions that the expectations should also check secondary locations in general - since they'll tend to include counterexamples for the SMT tests, they should be as good as an author comment in most cases (unless it's a TODO case)... but that might be a path into another non-determinism-hell :-)...

[axic]

Two years before this issue was created, #4620 discusses the same topic with a different syntax suggestion. Which one are we closing as duplicate? 😬

[ekpyron]

It's not exactly duplicates - @chriseth just proposed to fix this by fixing #4620 instead - I still think it'd be nice to have both a solution to #4620 and a single-step mode in isoltest, which was the original intention of this issue - even though the discussion then in fact moved to actually discussing #4620 instead...