Output counterexamples for failed Foundry proofs #1946

palinatolmach · 2023-07-07T11:52:40Z

Closes #1927.

Using get-model request, adds concrete counterexamples (i.e., models) of failing and pending nodes to print_failure_info(proof, kcfg_explore).
UPDATE: after a discussion with @nwatson22, we decided that we should probably only show counterexamples for failing (not pending) nodes by default.
This information is shown in the output of foundry-prove if any of the proofs has failed, or foundry-show --failure-information. Also, prints the invitation to the Discord channel once in print_failure_info(print_failure_info(proof, kcfg_explore) (instead of printing it with every failing node info), and fixes the link to the channel.
UPDATE: the counterexample is generated if foundry-prove and foundry-show are called with the --counterexample-information option.
The output looks like this:

> `kevm foundry-prove --test ExampleTest.testBackdoor`

... 

PROOF FAILED: ExampleTest.testBackdoor
1 Failure nodes. (0 pending and 1 failing)

Failing nodes:

  Node id: 20
  Failure reason:
    Implication check failed, the following is the remaining implication:
    ( ( { true #Equals 0 <=Int CALLER_ID:Int }
    ...
  Path condition:
    { true #Equals chop ... ==Int 0 }
  Model:
    CALLER_ID = 0
    NUMBER_CELL = 0
    ORIGIN_ID = maxUInt160
    VV0_x_114b9705 = 6912213124124532

Join the Runtime Verification Discord server for support: https://discord.com/invite/CurfmXNtbN

Access documentation for KEVM foundry integration at https://docs.runtimeverification.com/kevm-integration-for-foundry/

Adds foundry-get-model command that shows models of nodes from a specific test. Can be called with --node NODE_ID, --failing, and --pending options. If none of these arguments are provided, the models of failing and pending nodes will be shown (i.e., missing --node, --failing and/or --pending is equivalent to --failing --pending), and a corresponding warning is shown to the user. The output looks like this:

> kevm foundry-get-model ExampleTest.testBackdoor --node 20

Node id: 20
  Model:
    CALLER_ID = 0
    NUMBER_CELL = 0
    ORIGIN_ID = maxUInt160
    VV0_x_114b9705 = 6912213124124532

nwatson22 · 2023-07-07T21:07:28Z

kevm-pyk/src/kevm_pyk/utils.py

+def print_model(node: KCFG.Node, kcfg_explore: KCFGExplore) -> list[str]:
+    res_lines: list[str] = []
+    result_subst = kcfg_explore.cterm_get_model(node.cterm)
+    if type(result_subst) is Subst:
+        res_lines.append('  Model:')
+        for var, term in result_subst.to_dict().items():
+            term_kast = KInner.from_dict(term)
+            res_lines.append(f'    {var} = {kcfg_explore.kprint.pretty_print(term_kast)}')
+    else:
+        res_lines.append('  Failed to generate a model.')
+
+    return res_lines


We rewrote the print_failure_info function in pyk to separate the printing from the RPC calls here: runtimeverification/pyk@6c28b66
Possibly we would want to do something similar here, since it makes testing cleaner. I realized we haven't updated kevm to use that function yet and we still just use the kevm version, so actually we can probably just refactor this when we make those changes later.

Thanks Noah! I can probably try integrating the new failure_info function into kevm to include it in this PR, if this works--will update you on that tomorrow.

Sorry, didn't have a chance to do this, and I'll unfortunately be travelling starting tomorrow. Could you please advise if we should merge it in as it is and refactor print_failure_info later? I'll create a separate issue for it, in this case.

nwatson22 · 2023-07-07T21:09:15Z

kevm-pyk/src/kevm_pyk/foundry.py

+            model_info = print_model(node, kcfg_explore)
+            res_lines.extend(model_info)


Suggested change

model_info = print_model(node, kcfg_explore)

res_lines.extend(model_info)

res_lines.extend(print_model(node, kcfg_explore))

I'm not sure which is better (same for other places this occurs).

Thanks! I agree, done in 13c0f97.

palinatolmach · 2023-07-11T15:00:47Z

Updates: (1) added the temporary --counterexample-information option to foundry-prove and foundry-show, which generates the counterexample for each failing node and adds it to the output. Since it's currently part of the print_failure_info() implementation, in foundry-show, it should be called with the --failure-information option (it's reflected in its description), i.e., foundry-show --failure-information --counterexample-information. The purpose of adding this option is to make sure this change (and the SMT solver requests it includes) doesn't cause major performance issues, while we test it a bit more.

(2) when foundry-prove --counterexample-information is called, the counterexamples are only generated for failing (and not pending) nodes.

tothtamas28 · 2023-07-12T08:14:39Z

kevm-pyk/src/kevm_pyk/foundry.py

@@ -795,6 +797,44 @@ def foundry_section_edge(
    apr_proof.write_proof()


+def foundry_get_model(


This function should produce a data structure (maybe FoundryModel | None). Function print_model can be a method on this class (without the "Failed to ..." branch). Function print_failure_info then can be redefined as

def print_failure_info(kprint: KPrint, proof: Proof, *, model: FoundryModel | None = None) -> list[str]: ...

Thanks, I agree! Will add the FoundryModel class and modify the printing functions accordingly (there's some more refactoring to be done, as suggested by @nwatson22), but I need a bit more time to work on it. Would you recommend to merge the current PR and refactor it later, or should I include this change in this PR? Thank you!

It's fine either way. If you decide to merge now, please open an issue to document the requested changes.

Issue created: #1955

* Showing counterexamples for failed Foundry tests * Add `smt-hook` to `chop` for SMT solving * Prettier counterexample printing * Revert `smtlib` -> `smt-hook` change to `chop` after fix * Fixed Discord link, counterexample error message * Refactor `print_failure_info`, add counterexamples * Add `foundry-get-model` command * Fix merge conflicts * Show Discord invite once in `print_failure_info` * Minor code quality fix * Set Version: 1.0.232 * Minor code refactor; update tests w/new output * Remove pending nodes model generation by default * Add `--counterexample-information` to prove, show * Use `counterexample_info=True` in Foundry tests --------- Co-authored-by: devops <[email protected]>

palinatolmach linked an issue Jul 7, 2023 that may be closed by this pull request

Output concrete counter-example for failed proofs #1927

Closed

palinatolmach force-pushed the foundry-counterexamples branch from 384dd6e to 62dfd40 Compare July 7, 2023 11:52

palinatolmach requested review from nwatson22 and tothtamas28 July 7, 2023 12:04

anvacaru assigned palinatolmach Jul 7, 2023

nwatson22 approved these changes Jul 7, 2023

View reviewed changes

tothtamas28 approved these changes Jul 10, 2023

View reviewed changes

palinatolmach added 10 commits July 10, 2023 18:49

Showing counterexamples for failed Foundry tests

c9e37f3

Add smt-hook to chop for SMT solving

b51288c

Prettier counterexample printing

89c0085

Revert smtlib -> smt-hook change to chop

28bedb6

Fixed Discord link, counterexample error message

f95834e

Refactor print_failure_info, add counterexamples

7bfa8df

Add foundry-get-model command

988e9e9

Fix merge conflicts

c7b11d8

Show Discord invite once in print_failure_info

cd569a7

Minor code quality fix

b9130b9

palinatolmach force-pushed the foundry-counterexamples branch from 656c91d to b9130b9 Compare July 10, 2023 10:50

devops and others added 2 commits July 10, 2023 10:50

Set Version: 1.0.232

c283305

Minor code refactor; update tests w/new output

c9d786f

palinatolmach force-pushed the foundry-counterexamples branch from 13c0f97 to c9d786f Compare July 11, 2023 09:24

palinatolmach requested a review from ehildenb July 11, 2023 09:39

palinatolmach added 2 commits July 11, 2023 21:47

Remove pending nodes model generation by default

6d0257a

Add --counterexample-information to prove, show

53142aa

Use counterexample_info=True in Foundry tests

dfb0c1b

palinatolmach requested review from nwatson22 and tothtamas28 July 11, 2023 18:32

palinatolmach marked this pull request as ready for review July 12, 2023 04:28

tothtamas28 reviewed Jul 12, 2023

View reviewed changes

palinatolmach mentioned this pull request Jul 12, 2023

Refactor foundry_get_model and print_failure_info #1955

Open

palinatolmach merged commit cf3b0f7 into master Jul 12, 2023

palinatolmach deleted the foundry-counterexamples branch July 12, 2023 12:59

palinatolmach mentioned this pull request Sep 26, 2023

Add counterexample to interactive KCFG viewer runtimeverification/kontrol#46

Closed

palinatolmach mentioned this pull request Jul 26, 2023

Better message than PROOF FAILED on some failing proofs #1764

Closed

Provide feedback

Saved searches

Use saved searches to filter your results more quickly

Output counterexamples for failed Foundry proofs #1946

Output counterexamples for failed Foundry proofs #1946

palinatolmach commented Jul 7, 2023 •

edited

Loading

nwatson22 Jul 7, 2023

palinatolmach Jul 10, 2023

palinatolmach Jul 11, 2023

nwatson22 Jul 7, 2023

palinatolmach Jul 10, 2023

palinatolmach commented Jul 11, 2023

tothtamas28 Jul 12, 2023

palinatolmach Jul 12, 2023

tothtamas28 Jul 12, 2023

palinatolmach Jul 12, 2023

		model_info = print_model(node, kcfg_explore)
		res_lines.extend(model_info)

	model_info = print_model(node, kcfg_explore)
	res_lines.extend(model_info)
	res_lines.extend(print_model(node, kcfg_explore))

		@@ -795,6 +797,44 @@ def foundry_section_edge(
		apr_proof.write_proof()


		def foundry_get_model(

Output counterexamples for failed Foundry proofs #1946

Output counterexamples for failed Foundry proofs #1946

Conversation

palinatolmach commented Jul 7, 2023 • edited Loading

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

palinatolmach commented Jul 11, 2023

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

palinatolmach commented Jul 7, 2023 •

edited

Loading