Skip to content

Commit

Permalink
Adding --proof-hint flag to PyK KRun (#4532)
Browse files Browse the repository at this point in the history 
This PR aims to add the `--proof-hint` krun's flag to PyK infrastructure
so we can use it in semantics that currently relies on PyK for building
itself and execute programs.

Fixes: Pi-Squared-Inc/pi2#1725

---------

Co-authored-by: Tamás Tóth <[email protected]>
  • Loading branch information
@Robertorosmaninho @tothtamas28
Robertorosmaninho and tothtamas28 authored Aug 12, 2024
1 parent 015327f commit 4ebb140
Show file tree
Hide file tree
Showing 3 changed files with 196 additions and 1 deletion.
108 changes: 107 additions & 1 deletion pyk/src/pyk/ktool/krun.py
View file
Original file line number Diff line number Diff line change
Expand Up @@ -2,8 +2,12 @@

import logging
from enum import Enum
from os import execvp
from pathlib import Path
from subprocess import CalledProcessError
from shlex import join, split
from subprocess import PIPE, CalledProcessError, run
from sys import stderr, stdout
from time import time
from typing import TYPE_CHECKING

from ..cli.utils import check_dir_path, check_file_path
Expand Down Expand Up @@ -99,6 +103,104 @@ def run_process(
debugger=debugger,
)

def run_proof_hint(
self,
pgm: Pattern,
*,
cmap: Mapping[str, str] | None = None,
pmap: Mapping[str, str] | None = None,
output: KRunOutput | None = None,
parser: str | None = None,
term: bool = False,
temp_dir: Path | None = None,
depth: int | None = None,
expand_macros: bool = True,
search_final: bool = False,
no_pattern: bool = False,
check: bool = False,
pipe_stderr: bool = True,
debugger: bool = False,
proof_hint: bool = False,
) -> bytes:
with self._temp_file() as ntf:
pgm.write(ntf)
ntf.flush()

args = _build_arg_list(
command='krun',
input_file=Path(ntf.name),
definition_dir=self.definition_dir,
output=output,
parser=parser,
depth=depth,
pmap=pmap,
cmap=cmap,
term=term,
temp_dir=temp_dir,
no_expand_macros=not expand_macros,
search_final=search_final,
no_pattern=no_pattern,
debugger=debugger,
proof_hint=proof_hint,
)

hints_bytes = self.__run_proof_hint_process(
args=args, check=check, pipe_stderr=pipe_stderr, logger=_LOGGER, exec_process=debugger
)

return hints_bytes.stdout

def __run_proof_hint_process(
self,
args: str | Iterable[str],
*,
check: bool = True,
input: str | None = None,
pipe_stdout: bool = True,
pipe_stderr: bool = False,
cwd: str | Path | None = None,
logger: Logger | None = None,
exec_process: bool = False,
) -> CompletedProcess:

if cwd is not None:
cwd = Path(cwd)
check_dir_path(cwd)

if type(args) is str:
command = args
else:
args = tuple(args)
command = join(args)

if not logger:
logger = _LOGGER

proc_stdout = PIPE if pipe_stdout else None
proc_stderr = PIPE if pipe_stderr else None

logger.info(f'Running: {command}')

if exec_process:
stdout.flush()
stderr.flush()
if type(args) is str:
args = split(args)
argslist = list(args)
execvp(argslist[0], argslist)

start_time = time()

res = run(args, input=input, cwd=cwd, stdout=proc_stdout, stderr=proc_stderr, text=False)

delta_time = time() - start_time
logger.info(f'Completed in {delta_time:.3f}s with status {res.returncode}: {command}')

if check:
res.check_returncode()

return res

def run(
self,
pgm: Pattern,
Expand Down Expand Up @@ -236,6 +338,7 @@ def _krun(
search_final=search_final,
no_pattern=no_pattern,
debugger=debugger,
proof_hint=False,
)

if bug_report is not None:
Expand Down Expand Up @@ -265,6 +368,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 +397,8 @@ def _build_arg_list(
args += ['--no-pattern']
if debugger:
args += ['--debugger']
if proof_hint:
args += ['--proof-hint']
return args


Expand Down
87 changes: 87 additions & 0 deletions pyk/src/tests/integration/test_krun_proof_hints.py
View file
Original file line number Diff line number Diff line change
@@ -0,0 +1,87 @@
from __future__ import annotations

from typing import TYPE_CHECKING

import pyk.kllvm.hints.prooftrace as prooftrace
from pyk.kore.parser import KoreParser
from pyk.testing import KRunTest, ProofTraceTest

if TYPE_CHECKING:
from pyk.ktool.krun import KRun


class Test0Decrement(KRunTest, ProofTraceTest):
KOMPILE_DEFINITION = """
module DECREMENT-SYNTAX
syntax Nat ::= "0" | s(Nat)
endmodule
module DECREMENT
imports DECREMENT-SYNTAX
rule [decrement] : s(N:Nat) => N
endmodule
"""

KOMPILE_MAIN_MODULE = 'DECREMENT'
KOMPILE_BACKEND = 'llvm'
KOMPILE_ARGS = {'llvm_proof_hint_instrumentation': True}

HINTS_INPUT_KORE = """
LblinitGeneratedTopCell{}(Lbl'Unds'Map'Unds'{}(Lbl'Stop'Map{}(),Lbl'UndsPipe'-'-GT-Unds'{}(inj{SortKConfigVar{}, SortKItem{}}(\\dv{SortKConfigVar{}}("$PGM")),inj{SortNat{}, SortKItem{}}(Lbl0'Unds'DECREMENT-SYNTAX'Unds'Nat{}()))))
"""

HINTS_OUTPUT = """version: 11
hook: MAP.element Lbl'UndsPipe'-'-GT-Unds'{} ()
function: Lbl'UndsPipe'-'-GT-Unds'{} ()
arg: kore[\\dv{SortKConfigVar{}}("$PGM")]
arg: kore[Lbl0'Unds'DECREMENT-SYNTAX'Unds'Nat{}()]
hook result: kore[Lbl'UndsPipe'-'-GT-Unds'{}(\\dv{SortKConfigVar{}}("$PGM"),Lbl0'Unds'DECREMENT-SYNTAX'Unds'Nat{}())]
hook: MAP.unit Lbl'Stop'Map{} ()
function: Lbl'Stop'Map{} ()
hook result: kore[Lbl'Stop'Map{}()]
hook: MAP.concat Lbl'Unds'Map'Unds'{} ()
function: Lbl'Unds'Map'Unds'{} ()
arg: kore[Lbl'Stop'Map{}()]
arg: kore[Lbl'UndsPipe'-'-GT-Unds'{}(\\dv{SortKConfigVar{}}("$PGM"),Lbl0'Unds'DECREMENT-SYNTAX'Unds'Nat{}())]
hook result: kore[Lbl'UndsPipe'-'-GT-Unds'{}(\\dv{SortKConfigVar{}}("$PGM"),Lbl0'Unds'DECREMENT-SYNTAX'Unds'Nat{}())]
function: LblinitGeneratedTopCell{} ()
rule: 99 1
VarInit = kore[Lbl'UndsPipe'-'-GT-Unds'{}(\\dv{SortKConfigVar{}}("$PGM"),Lbl0'Unds'DECREMENT-SYNTAX'Unds'Nat{}())]
function: LblinitKCell{} (0)
rule: 100 1
VarInit = kore[Lbl'UndsPipe'-'-GT-Unds'{}(\\dv{SortKConfigVar{}}("$PGM"),Lbl0'Unds'DECREMENT-SYNTAX'Unds'Nat{}())]
function: Lblproject'Coln'KItem{} (0:0)
hook: MAP.lookup LblMap'Coln'lookup{} (0:0:0:0)
function: LblMap'Coln'lookup{} (0:0:0:0)
arg: kore[Lbl'UndsPipe'-'-GT-Unds'{}(\\dv{SortKConfigVar{}}("$PGM"),Lbl0'Unds'DECREMENT-SYNTAX'Unds'Nat{}())]
arg: kore[\\dv{SortKConfigVar{}}("$PGM")]
hook result: kore[Lbl0'Unds'DECREMENT-SYNTAX'Unds'Nat{}()]
rule: 139 1
VarK = kore[Lbl0'Unds'DECREMENT-SYNTAX'Unds'Nat{}()]
function: LblinitGeneratedCounterCell{} (1)
rule: 98 0
config: kore[Lbl'-LT-'generatedTop'-GT-'{}(Lbl'-LT-'k'-GT-'{}(kseq{}(Lbl0'Unds'DECREMENT-SYNTAX'Unds'Nat{}(),dotk{}())),Lbl'-LT-'generatedCounter'-GT-'{}(\\dv{SortInt{}}("0")))]
config: kore[Lbl'-LT-'generatedTop'-GT-'{}(Lbl'-LT-'k'-GT-'{}(kseq{}(Lbl0'Unds'DECREMENT-SYNTAX'Unds'Nat{}(),dotk{}())),Lbl'-LT-'generatedCounter'-GT-'{}(\\dv{SortInt{}}("0")))]
"""

def test_parse_proof_hint_0_decrement(self, krun: KRun, header: prooftrace.KoreHeader) -> None:
pgm = KoreParser(self.HINTS_INPUT_KORE).pattern()

hints = krun.run_proof_hint(
pgm,
parser='cat',
term=True,
proof_hint=True,
)

pt = prooftrace.LLVMRewriteTrace.parse(hints, header)
assert pt is not None

# 11 initialization events
assert len(pt.pre_trace) == 11

# 1 post-initial-configuration event
assert len(pt.trace) == 1

# Check if the proof trace is correct
assert str(pt) == self.HINTS_OUTPUT
2 changes: 2 additions & 0 deletions pyk/src/tests/unit/ktool/test_krun.py
View file
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),
]
)

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

0 comments on commit 4ebb140

Please sign in to comment.