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

Adding --proof-hint flag to PyK KRun #4532

Open
wants to merge 9 commits into
base: develop
Choose a base branch
from
Open

Adding --proof-hint flag to PyK KRun #4532

Changes from 2 commits
Commits
Show all changes
9 commits
Select commit Hold shift + click to select a range
55ee1b3
Adding `--proof-hint` flag to PyK KRun
Robertorosmaninho Jul 18, 2024
efcc3ed
Formatting code
Robertorosmaninho Jul 18, 2024
93ca0c0
Update pyk/src/pyk/ktool/krun.py
Robertorosmaninho Jul 19, 2024
ffb2d54
Adding `proof_hint` to krun unit-test
Robertorosmaninho Jul 19, 2024
86c8214
Adding `pipe_stdout` flag False when `proof_hint` is passed
Robertorosmaninho Jul 19, 2024
977bcb6
Formatting
Robertorosmaninho Jul 19, 2024
b5a445e
Deleting `write` call as the hints we're already printed by `subprocess`
Robertorosmaninho Jul 19, 2024
832c329
Merge branch 'develop' into pi2/proof-hint-flag-to-pyk-krun
Robertorosmaninho Jul 19, 2024
43d618d
Modfiying conditions with proof_hint
Robertorosmaninho Jul 19, 2024
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
15 changes: 15 additions & 0 deletions pyk/src/pyk/ktool/krun.py
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -2,6 +2,7 @@

import logging
from enum import Enum
from os import write
from pathlib import Path
from subprocess import CalledProcessError
from typing import TYPE_CHECKING
Expand Down Expand Up @@ -74,6 +75,7 @@ def run_process(
pipe_stderr: bool = True,
bug_report: BugReport | None = None,
debugger: bool = False,
proof_hint: bool = False,
) -> CompletedProcess:
with self._temp_file() as ntf:
pgm.write(ntf)
Expand All @@ -97,6 +99,7 @@ def run_process(
check=False,
pipe_stderr=pipe_stderr,
debugger=debugger,
proof_hint=proof_hint,
)

def run(
Expand All @@ -115,6 +118,7 @@ def run(
pipe_stderr: bool = True,
bug_report: BugReport | None = None,
debugger: bool = False,
proof_hint: bool = False,
Copy link
Contributor

@tothtamas28 tothtamas28 Jul 19, 2024 •
edited
Loading

Choose a reason for hiding this comment

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

Unfortunately, this approach won't work: under the hood it leads to a call like

subprocess.run(['krun', 'test.imp', '--proof-hint'], text=True, stdout=subprocess.PIPE)

which will raise an exception:

UnicodeDecodeError: 'utf-8' codec can't decode byte 0xff in position 8: invalid start byte

This is because

  • stdout=subprocess.PIPE, so CompletedProcess.stdout will be populated.
  • text=True, so the function will try to decode the bytes output to produce CompletedProcess.stdout.

You drop any of these arguments and it'll work.

Please add a test to reproduce this issue.

Workarounds:

  1. Reuse _build_arg_list and call subprocess.run directly.
  2. If we know how the bytes output is supposed to be decoded, we can thread argument encoding through to subprocess.run (standard encodings).
  3. You can pass pipe_stdout=False to run_process, so that you have stdout=None in subprocess.run.
  4. We can patch run_process (and it's newer version, run_process_2 ) to accept text=False, but that's not straightforward.

I'd prefer a solution that won't prevent us from dropping run_process in favor of run_process_2 in the future, i.e. (1) or (2).

Copy link
Contributor Author

Choose a reason for hiding this comment

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

You're right! I dropped text=True locally and forgot to commit this.

Copy link
Contributor Author

@Robertorosmaninho Robertorosmaninho Jul 19, 2024 •
edited
Loading

Choose a reason for hiding this comment

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

About your workarounds:

  1. Isn't that just a different way to create a third run_process?
  2. I don't think we can do this as the encoding was created by us on the llvm backend serializer; we really need to output the binary itself, not its text representation/deserialization.
  3. That's a good approach; we can have pipe_stdout = not prof_hint.
  4. Indeed, that's not trivial and isn't worth spending time on.

If you don't mind, I would prefer to stick to option 3 to unblock Pi2 folks, and when we need to drop run_process in favor of run_process_2, we can sit together again to brainstorm a way to make it compatible with proof hints.

) -> None:
result = self.run_process(
pgm,
Expand All @@ -129,8 +133,14 @@ def run(
pipe_stderr=pipe_stderr,
bug_report=bug_report,
debugger=debugger,
proof_hint=proof_hint,
)

if proof_hint:
# Print the binary proof hint to stdout regardless of the output option
write(1, result.stdout)
Copy link
Collaborator

Choose a reason for hiding this comment

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

I'm not sure what the intent of the code here is; it seems confusing that the proof hint mode will unconditionally escape the Python framework and dump directly to stdout.

Copy link
Contributor

Choose a reason for hiding this comment

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

I agree, it would be better to expose this operation mode as a separate function.

Copy link
Contributor Author

Choose a reason for hiding this comment

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

This is the actual behavior of the flag in the krun. kprint can't handle this kind of binary, so the idea is just to dump it in the console as krun does. The alternative, from my point of view, would be to Dump into a file but escape the Python framework anyway.

Copy link
Contributor Author

Choose a reason for hiding this comment

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

For instance, krun only cat .../result.kore when --prof-hint is passed as opposite to call kore-print ... result.kore when this flag isn't in use.

So I believe this mimics the same behavior we already have.

Copy link
Collaborator

Choose a reason for hiding this comment

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

The alternative, from my point of view, would be to Dump into a file but escape the Python framework anyway.

The point is that we manage stdout and stderr through the CompletedProcess object. If the hint has been captured by the subprocess library, then the way to get it to the calling app's stdout is not to bypass that management entirely; you should probably instead have the calling code write it out to a file yourself.

return

if output != KRunOutput.NONE:
output_kore = KoreParser(result.stdout).pattern()
match output:
Expand Down Expand Up @@ -208,6 +218,7 @@ def _krun(
logger: Logger | None = None,
bug_report: BugReport | None = None,
debugger: bool = False,
proof_hint: bool = False,
) -> CompletedProcess:
if input_file:
check_file_path(input_file)
Expand Down Expand Up @@ -236,6 +247,7 @@ def _krun(
search_final=search_final,
no_pattern=no_pattern,
debugger=debugger,
proof_hint=proof_hint,
)

if bug_report is not None:
Expand Down Expand Up @@ -265,6 +277,7 @@ def _build_arg_list(
search_final: bool,
no_pattern: bool,
debugger: bool,
proof_hint: bool = False,
Robertorosmaninho marked this conversation as resolved.
Show resolved Hide resolved
) -> list[str]:
args = [command]
if input_file:
Expand Down Expand Up @@ -293,6 +306,8 @@ def _build_arg_list(
args += ['--no-pattern']
if debugger:
args += ['--debugger']
if proof_hint:
args += ['--proof-hint']
return args


Expand Down
Loading