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

Show file tree
Hide file tree
Changes from all 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
24 changes: 22 additions & 2 deletions pyk/src/pyk/ktool/krun.py
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -74,6 +74,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 +98,7 @@ def run_process(
check=False,
pipe_stderr=pipe_stderr,
debugger=debugger,
proof_hint=proof_hint,
)

def run(
Expand All @@ -115,6 +117,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,9 +132,10 @@ def run(
pipe_stderr=pipe_stderr,
bug_report=bug_report,
debugger=debugger,
proof_hint=proof_hint,
)

if output != KRunOutput.NONE:
if not proof_hint and output != KRunOutput.NONE:
output_kore = KoreParser(result.stdout).pattern()
match output:
case KRunOutput.JSON:
Expand Down Expand Up @@ -205,9 +209,11 @@ def _krun(
# ---
check: bool = True,
pipe_stderr: bool = True,
pipe_stdout: bool = True,
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 +242,7 @@ def _krun(
search_final=search_final,
no_pattern=no_pattern,
debugger=debugger,
proof_hint=proof_hint,
)

if bug_report is not None:
Expand All @@ -246,7 +253,17 @@ def _krun(
else:
bug_report.add_command(args)

return run_process(args, check=check, pipe_stderr=pipe_stderr, logger=logger or _LOGGER, exec_process=debugger)
if proof_hint and pipe_stdout:
raise ValueError('Cannot pipe stdout when using proof hints')

return run_process(
args,
check=check,
pipe_stderr=pipe_stderr,
pipe_stdout=not proof_hint and pipe_stdout,
logger=logger or _LOGGER,
exec_process=debugger,
)


def _build_arg_list(
Expand All @@ -265,6 +282,7 @@ def _build_arg_list(
search_final: bool,
no_pattern: bool,
debugger: bool,
proof_hint: bool,
) -> list[str]:
args = [command]
if input_file:
Expand Down Expand Up @@ -293,6 +311,8 @@ def _build_arg_list(
args += ['--no-pattern']
if debugger:
args += ['--debugger']
if proof_hint:
args += ['--proof-hint']
return args


Expand Down
2 changes: 2 additions & 0 deletions pyk/src/tests/unit/ktool/test_krun.py
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -23,6 +23,7 @@
('search_final', False),
('no_pattern', False),
('debugger', False),
('proof_hint', False),
Copy link
Contributor

Choose a reason for hiding this comment

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

Please add an integration test for checking the proof hints output for some execution.

]
)

Expand All @@ -40,6 +41,7 @@
'search_final': (True, ['--search-final']),
'no_pattern': (True, ['--no-pattern']),
'debugger': (True, ['--debugger']),
'proof_hint': (True, ['--proof-hint']),
}


Expand Down
Loading