Skip to content
This repository has been archived by the owner on Apr 25, 2024. It is now read-only.

Add proof exploration and display options to CLI #1043

Closed
wants to merge 17 commits into from
Closed
Changes from 13 commits
Commits
Show all changes
17 commits
Select commit Hold shift + click to select a range
fa62121
ktool/kprove, cli/pyk, __main__: add --max-depth option for controlli…
ehildenb Mar 27, 2024
9444941
cli/{args,pyk}, ktool/kprove: factor out and reuse SpecOptions from P…
ehildenb Apr 2, 2024
0d18b7c
ktool/kprove, cli/pyk, __main__: add option --save-directory for savi…
ehildenb Apr 2, 2024
b76936c
ktool/{kprint,kprove}, cli/args, __main__: wire up --temp-dir options…
ehildenb Apr 2, 2024
d62abc3
ktool/kprove, __main__: print out structured error for failed call to…
ehildenb Apr 2, 2024
2ccf94f
ktool/kprove, cli/pyk, __main__: dont load CTermSymbolic if no progre…
ehildenb Apr 2, 2024
89a57da
cli/pyk, __main__: add option for showing proof KCFG after execution
ehildenb Apr 3, 2024
94b8eb2
ktool/kprove: if proof exists on disk already, reload it from saved s…
ehildenb Apr 3, 2024
438e71d
cli/pyk, __main__: implement rudimentary proof showing option
ehildenb Apr 3, 2024
31df1ec
Merge remote-tracking branch 'upstream/master' into proof-functionali…
ehildenb Apr 3, 2024
5e75e1e
regression-new/kprove-haskell: add test of pyk prove --show-kcfg
ehildenb Apr 3, 2024
17e88ae
Merge remote-tracking branch 'upstream/master' into proof-functionali…
ehildenb Apr 3, 2024
9e9a063
Merge 17e88ae402b3064be56caac9f6fd9f467d97c3c2 into d7219ab4897536fd0…
ehildenb Apr 3, 2024
67aada7
Set Version: 0.1.769
Apr 3, 2024
ab2e9ee
ktool/kprove: source max_depth from ProveOptions class
ehildenb Apr 3, 2024
1a59e8b
cli/args: pyupgrade
ehildenb Apr 3, 2024
ea29f4e
cli/args, __main__: factor out KCLIArgs.spec_args for pyk [prove|show]
ehildenb Apr 3, 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
1 change: 1 addition & 0 deletions regression-new/kprove-haskell/Makefile
Original file line number Diff line number Diff line change
@@ -2,6 +2,7 @@ DEF=verif
EXT=verif
TESTDIR=.
KOMPILE_BACKEND=haskell
KPROVE_FLAGS=--show-kcfg
export KORE_EXEC_OPTS=--log-level error

include ../include/ktest.mak
123 changes: 123 additions & 0 deletions regression-new/kprove-haskell/sum-spec.k.out
Original file line number Diff line number Diff line change
@@ -11,3 +11,126 @@ APRProof: 3b7070ca4603e18d26d032c0fe64dd71ffadc2c63dae9d57315e8e471a371bd3
bounded: 0
execution time: 0s
Subproofs: 0

┌─ 1 (root, init)
│ <generatedTop>
│ <k>
│ addCounter ( N:Int )
│ ~> K_CELL_fc656f08:K
│ </k>
│ <counter>
│ C:Int
│ </counter>
│ <sum>
│ S:Int
│ </sum>
│ <generatedCounter>
│ GENERATEDCOUNTER_CELL_949ec677:Int
│ </generatedCounter>
│ </generatedTop>
│ #And { true #Equals N:Int >=Int 0 }
┃ (1 step)
┣━━┓
┃ │
┃ ├─ 3
┃ │ <generatedTop>
┃ │ <k>
┃ │ addCounter ( N:Int +Int -1 )
┃ │ ~> K_CELL_fc656f08:K
┃ │ </k>
┃ │ <counter>
┃ │ C:Int +Int 1
┃ │ </counter>
┃ │ <sum>
┃ │ S:Int +Int C:Int
┃ │ </sum>
┃ │ <generatedCounter>
┃ │ GENERATEDCOUNTER_CELL_949ec677:Int
┃ │ </generatedCounter>
┃ │ </generatedTop>
┃ │ #And { true #Equals N:Int >Int 0 }
┃ │ #And { true #Equals N:Int >=Int 0 }
┃ │
┃ │ (1 step)
┃ ├─ 5
┃ │ <generatedTop>
┃ │ <k>
┃ │ K_CELL_fc656f08:K
┃ │ </k>
┃ │ <counter>
┃ │ ?_COUNTER_CELL_af8c44a5:Int
┃ │ </counter>
┃ │ <sum>
┃ │ S:Int +Int C:Int +Int N:Int +Int -1 *Int C:Int +Int 1 +Int N:Int +Int -2 *Int N:Int +Int -1 /Int 2
┃ │ </sum>
┃ │ <generatedCounter>
┃ │ ?_GENERATEDCOUNTER_CELL_5e3e01ba:Int
┃ │ </generatedCounter>
┃ │ </generatedTop>
┃ │ #And { true #Equals N:Int >Int 0 }
┃ │ #And { true #Equals N:Int >=Int 0 }
┃ │ #And { true #Equals N:Int +Int -1 >=Int 0 }
┃ │
┃ ┊ constraint: OMITTED CONSTRAINT
┃ ┊ subst: OMITTED SUBST
┃ └─ 2 (leaf, target)
┃ <generatedTop>
┃ <k>
┃ K_CELL_fc656f08:K ~> .K
┃ </k>
┃ <counter>
┃ COUNTER_CELL_af8c44a5:Int
┃ </counter>
┃ <sum>
┃ ?S:Int
┃ </sum>
┃ <generatedCounter>
┃ GENERATEDCOUNTER_CELL_5e3e01ba:Int
┃ </generatedCounter>
┃ </generatedTop>
┃ #And { true #Equals N:Int >=Int 0 }
┃ #And { true #Equals ?S:Int ==Int S:Int +Int N:Int *Int C:Int +Int N:Int -Int 1 *Int N:Int /Int 2 }
┗━━┓
├─ 4
│ <generatedTop>
│ <k>
│ K_CELL_fc656f08:K
│ </k>
│ <counter>
│ C:Int
│ </counter>
│ <sum>
│ S:Int
│ </sum>
│ <generatedCounter>
│ GENERATEDCOUNTER_CELL_949ec677:Int
│ </generatedCounter>
│ </generatedTop>
│ #And { N:Int #Equals 0 }
┊ constraint: OMITTED CONSTRAINT
┊ subst: OMITTED SUBST
└─ 2 (leaf, target)
<generatedTop>
<k>
K_CELL_fc656f08:K ~> .K
</k>
<counter>
COUNTER_CELL_af8c44a5:Int
</counter>
<sum>
?S:Int
</sum>
<generatedCounter>
GENERATEDCOUNTER_CELL_5e3e01ba:Int
</generatedCounter>
</generatedTop>
#And { true #Equals N:Int >=Int 0 }
#And { true #Equals ?S:Int ==Int S:Int +Int N:Int *Int C:Int +Int N:Int -Int 1 *Int N:Int /Int 2 }




37 changes: 37 additions & 0 deletions regression-new/kprove-haskell/test-fail-spec.k.out
Original file line number Diff line number Diff line change
@@ -26,3 +26,40 @@ Failing nodes:
Failed to generate a model.

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

┌─ 1 (root, stuck, leaf, init)
│ <generatedTop>
│ <k>
│ doIt ( -3 )
│ ~> K_CELL_fc656f08:K
│ </k>
│ <counter>
│ COUNTER_CELL
│ </counter>
│ <sum>
│ SUM_CELL
│ </sum>
│ <generatedCounter>
│ GENERATEDCOUNTER_CELL_c84b0b5f:Int
│ </generatedCounter>
│ </generatedTop>

┌─ 2 (root, leaf, target)
│ <generatedTop>
│ <k>
│ doIt ( 0 )
│ ~> K_CELL_fc656f08:K
│ </k>
│ <counter>
│ COUNTER_CELL
│ </counter>
│ <sum>
│ SUM_CELL
│ </sum>
│ <generatedCounter>
│ GENERATEDCOUNTER_CELL_6de8d71b:Int
│ </generatedCounter>
│ </generatedTop>



58 changes: 58 additions & 0 deletions regression-new/kprove-haskell/test-spec.k.out
Original file line number Diff line number Diff line change
@@ -11,3 +11,61 @@ APRProof: 8b72c409e7e4e821e957233b93c93d850e4c2f79fa4be4a12f32ab064030dce7
bounded: 0
execution time: 0s
Subproofs: 0

┌─ 1 (root, init)
│ <generatedTop>
│ <k>
│ doIt ( 3 )
│ ~> K_CELL_fc656f08:K
│ </k>
│ <counter>
│ COUNTER_CELL
│ </counter>
│ <sum>
│ SUM_CELL
│ </sum>
│ <generatedCounter>
│ GENERATEDCOUNTER_CELL_c84b0b5f:Int
│ </generatedCounter>
│ </generatedTop>
│ (3 steps)
├─ 3
│ <generatedTop>
│ <k>
│ doIt ( 0 )
│ ~> K_CELL_fc656f08:K
│ </k>
│ <counter>
│ COUNTER_CELL:Int
│ </counter>
│ <sum>
│ SUM_CELL:Int
│ </sum>
│ <generatedCounter>
│ GENERATEDCOUNTER_CELL_c84b0b5f:Int
│ </generatedCounter>
│ </generatedTop>
┊ constraint: true
┊ subst: GENERATEDCOUNTER_CELL_6de8d71b <- GENERATEDCOUNTER_CELL_c84b0b5f:Int
└─ 2 (leaf, target)
<generatedTop>
<k>
doIt ( 0 )
~> K_CELL_fc656f08:K
</k>
<counter>
COUNTER_CELL
</counter>
<sum>
SUM_CELL
</sum>
<generatedCounter>
GENERATEDCOUNTER_CELL_6de8d71b:Int
</generatedCounter>
</generatedTop>




90 changes: 87 additions & 3 deletions src/pyk/__main__.py
Original file line number Diff line number Diff line change
@@ -37,7 +37,8 @@
from .ktool.krun import KRun
from .prelude.k import GENERATED_TOP_CELL
from .prelude.ml import is_top, mlAnd, mlOr
from .proof.reachability import APRFailureInfo
from .proof.reachability import APRFailureInfo, APRProof
from .proof.show import APRProofNodePrinter, APRProofShow
from .utils import check_file_path, ensure_dir_path, exit_with_process_error

if TYPE_CHECKING:
@@ -248,17 +249,32 @@ def exec_prove(options: ProveOptions) -> None:
_LOGGER.info(f'Using kompiled directory: {kompiled_directory}.')
else:
kompiled_directory = options.definition_dir
kprove = KProve(kompiled_directory)
proofs = kprove.prove_rpc(options=options)
kprove = KProve(kompiled_directory, use_directory=options.temp_directory)
try:
proofs = kprove.prove_rpc(options=options)
except RuntimeError as err:
_, _, _, cpe = err.args
exit_with_process_error(cpe)
for proof in sorted(proofs, key=lambda p: p.id):
print('\n'.join(proof.summary.lines))
if proof.failed and options.failure_info:
failure_info = proof.failure_info
if type(failure_info) is APRFailureInfo:
print('\n'.join(failure_info.print()))
if options.show_kcfg and type(proof) is APRProof:
node_printer = APRProofNodePrinter(proof, kprove, full_printer=True, minimize=False)
show = APRProofShow(kprove, node_printer=node_printer)
print('\n'.join(show.show(proof)))
sys.exit(len([p.id for p in proofs if not p.passed]))


def exec_show(options: ProveOptions) -> None:
options.max_iterations = 0
options.show_kcfg = True
options.failure_info = True
exec_prove(options)


def exec_kompile(options: KompileCommandOptions) -> None:
main_file = Path(options.main_file)
check_file_path(main_file)
@@ -467,6 +483,74 @@ def create_argument_parser() -> ArgumentParser:
action='store_true',
help='Print out more information about proof failures.',
)
prove_args.add_argument(
'--show-kcfg',
default=None,
action='store_true',
help='Display the resulting proof KCFG.',
)
prove_args.add_argument(
'--max-depth',
default=None,
type=int,
help='Maximum number of steps to take in symbolic execution per basic block.',
)
prove_args.add_argument(
'--max-iterations',
default=None,
type=int,
help='Maximum number of KCFG explorations to take in attempting to discharge proof.',
)
prove_args.add_argument(
'--save-directory',
dest='save_directory',
default=None,
type=ensure_dir_path,
help='Directory to save proof artifacts to for reuse.',
)
prove_args.add_argument(
'--temp-directory',
'--temp-dir',
'--tmp-dir',
dest='temp_directory',
default=None,
type=ensure_dir_path,
help='Directory to save intermediate temporaries to.',
)

show_args = pyk_args_command.add_parser(
'show',
help='Display the status of a given proof.',
parents=[k_cli_args.logging_args],
)
show_args.add_argument('spec_file', type=file_path, help='File with the specification module.')
show_args.add_argument('--definition', type=dir_path, dest='definition_dir', help='Path to definition to use.')
show_args.add_argument('--spec-module', dest='spec_module', type=str, help='Module with claims to be proven.')
show_args.add_argument(
'--type-inference-mode', type=TypeInferenceMode, help='Mode for doing K rule type inference in.'
)
show_args.add_argument(
'--failure-info',
default=None,
action='store_true',
help='Print out more information about proof failures.',
)
show_args.add_argument(
'--save-directory',
dest='save_directory',
default=None,
type=ensure_dir_path,
help='Directory to save proof artifacts to for reuse.',
)
show_args.add_argument(
'--temp-directory',
'--temp-dir',
'--tmp-dir',
dest='temp_directory',
default=None,
type=ensure_dir_path,
help='Directory to save intermediate temporaries to.',
)

graph_imports_args = pyk_args_command.add_parser(
'graph-imports',
12 changes: 9 additions & 3 deletions src/pyk/cli/args.py
Original file line number Diff line number Diff line change
@@ -11,6 +11,8 @@
from .utils import bug_report_arg, ensure_dir_path, file_path

if TYPE_CHECKING:
from typing import Iterable

from ..utils import BugReport


@@ -82,24 +84,28 @@ def default() -> dict[str, Any]:

class SaveDirOptions(Options):
save_directory: Path | None
temp_directory: Path | None

@staticmethod
def default() -> dict[str, Any]:
return {
'save_directory': None,
'temp_directory': None,
}


class SpecOptions(SaveDirOptions):
spec_file: Path
claim_labels: list[str] | None
exclude_claim_labels: list[str]
spec_module: str | None
claim_labels: Iterable[str] | None
exclude_claim_labels: Iterable[str] | None

@staticmethod
def default() -> dict[str, Any]:
return {
'spec_module': None,
'claim_labels': None,
'exclude_claim_labels': [],
'exclude_claim_labels': None,
}


15 changes: 11 additions & 4 deletions src/pyk/cli/pyk.py
Original file line number Diff line number Diff line change
@@ -11,6 +11,8 @@
KompileOptions,
LoggingOptions,
OutputFileOptions,
SaveDirOptions,
SpecOptions,
WarningOptions,
)

@@ -42,6 +44,8 @@ def generate_options(args: dict[str, Any]) -> LoggingOptions:
return ProveLegacyOptions(args)
case 'prove':
return ProveOptions(args)
case 'show':
return ProveOptions(args)
case 'kompile':
return KompileCommandOptions(args)
case 'run':
@@ -121,20 +125,23 @@ def default() -> dict[str, Any]:
}


class ProveOptions(LoggingOptions):
spec_file: Path
class ProveOptions(LoggingOptions, SpecOptions, SaveDirOptions):
definition_dir: Path | None
spec_module: str | None
type_inference_mode: TypeInferenceMode | None
failure_info: bool
max_depth: int | None
max_iterations: int | None
show_kcfg: bool

@staticmethod
def default() -> dict[str, Any]:
return {
'definition_dir': None,
'spec_module': None,
'type_inference_mode': None,
'failure_info': False,
'max_depth': None,
'max_iterations': None,
'show_kcfg': False,
}


3 changes: 2 additions & 1 deletion src/pyk/ktool/kprint.py
Original file line number Diff line number Diff line change
@@ -211,11 +211,12 @@ def __init__(
self._bug_report = bug_report

@contextmanager
def _temp_file(self, suffix: str | None = None) -> Iterator[_TemporaryFileWrapper]:
def _temp_file(self, prefix: str | None = None, suffix: str | None = None) -> Iterator[_TemporaryFileWrapper]:
with NamedTemporaryFile(
'w',
dir=self.use_directory,
delete=not self.use_directory,
prefix=prefix,
suffix=suffix,
) as ntf:
_LOGGER.info(f'Created temporary file: {ntf.name}')
115 changes: 69 additions & 46 deletions src/pyk/ktool/kprove.py
Original file line number Diff line number Diff line change
@@ -105,7 +105,7 @@ def _kprove(
return run_process(run_args, logger=_LOGGER, env=env, check=check)
except CalledProcessError as err:
raise RuntimeError(
f'Command kprove exited with code {err.returncode} for: {spec_file}', err.stdout, err.stderr
f'Command kprove exited with code {err.returncode} for: {spec_file}', err.stdout, err.stderr, err
) from err


@@ -285,53 +285,72 @@ def prove_claim_rpc(
fallback_on: Iterable[FallbackReason] | None = None,
interim_simplification: int | None = None,
no_post_exec_simplify: bool = False,
max_depth: int | None = None,
save_directory: Path | None = None,
max_iterations: int | None = None,
) -> Proof:
with cterm_symbolic(
self.definition,
self.kompiled_kore,
self.definition_dir,
id=id,
port=port,
kore_rpc_command=kore_rpc_command,
llvm_definition_dir=llvm_definition_dir,
smt_timeout=smt_timeout,
smt_retry_limit=smt_retry_limit,
smt_tactic=smt_tactic,
bug_report=bug_report,
haskell_log_format=haskell_log_format,
haskell_log_entries=haskell_log_entries,
log_axioms_file=log_axioms_file,
trace_rewrites=trace_rewrites,
start_server=start_server,
maude_port=maude_port,
fallback_on=fallback_on,
interim_simplification=interim_simplification,
no_post_exec_simplify=no_post_exec_simplify,
) as cts:
kcfg_explore = KCFGExplore(cts, kcfg_semantics=kcfg_semantics)
proof: Proof
prover: Prover
lhs_top = extract_lhs(claim.body)
if type(lhs_top) is KApply and self.definition.symbols[lhs_top.label.name] in self.definition.functions:
proof = EqualityProof.from_claim(claim, self.definition)
prover = ImpliesProver(proof, kcfg_explore)
else:
proof = APRProof.from_claim(self.definition, claim, {})
prover = APRProver(proof, kcfg_explore)
prover.advance_proof()
if proof.passed:
_LOGGER.info(f'Proof passed: {proof.id}')
elif proof.failed:
_LOGGER.info(f'Proof failed: {proof.id}')
else:
_LOGGER.info(f'Proof pending: {proof.id}')
return proof
proof: Proof
prover: Prover
lhs_top = extract_lhs(claim.body)
is_functional_claim = (
type(lhs_top) is KApply and self.definition.symbols[lhs_top.label.name] in self.definition.functions
)

if is_functional_claim:
proof = EqualityProof.from_claim(claim, self.definition, proof_dir=save_directory)
if save_directory is not None and EqualityProof.proof_data_exists(proof.id, save_directory):
_LOGGER.info(f'Reloading from disk {proof.id}: {save_directory}')
proof = EqualityProof.read_proof_data(save_directory, proof.id)

else:
proof = APRProof.from_claim(self.definition, claim, {}, proof_dir=save_directory)
if save_directory is not None and APRProof.proof_data_exists(proof.id, save_directory):
_LOGGER.info(f'Reloading from disk {proof.id}: {save_directory}')
proof = APRProof.read_proof_data(save_directory, proof.id)

if not proof.passed and (max_iterations is None or max_iterations > 0):
with cterm_symbolic(
self.definition,
self.kompiled_kore,
self.definition_dir,
id=id,
port=port,
kore_rpc_command=kore_rpc_command,
llvm_definition_dir=llvm_definition_dir,
smt_timeout=smt_timeout,
smt_retry_limit=smt_retry_limit,
smt_tactic=smt_tactic,
bug_report=bug_report,
haskell_log_format=haskell_log_format,
haskell_log_entries=haskell_log_entries,
log_axioms_file=log_axioms_file,
trace_rewrites=trace_rewrites,
start_server=start_server,
maude_port=maude_port,
fallback_on=fallback_on,
interim_simplification=interim_simplification,
no_post_exec_simplify=no_post_exec_simplify,
) as cts:
kcfg_explore = KCFGExplore(cts, kcfg_semantics=kcfg_semantics)
if is_functional_claim:
assert type(proof) is EqualityProof
prover = ImpliesProver(proof, kcfg_explore)
else:
assert type(proof) is APRProof
prover = APRProver(proof, kcfg_explore, execute_depth=max_depth)
prover.advance_proof(max_iterations=max_iterations)

if proof.passed:
_LOGGER.info(f'Proof passed: {proof.id}')
elif proof.failed:
_LOGGER.info(f'Proof failed: {proof.id}')
else:
_LOGGER.info(f'Proof pending: {proof.id}')
return proof

def prove_rpc(
self,
options: ProveOptions,
claim_labels: Iterable[str] | None = None,
exclude_claim_labels: Iterable[str] | None = None,
kcfg_semantics: KCFGSemantics | None = None,
id: str | None = None,
port: int | None = None,
@@ -350,6 +369,7 @@ def prove_rpc(
fallback_on: Iterable[FallbackReason] | None = None,
interim_simplification: int | None = None,
no_post_exec_simplify: bool = False,
max_depth: int | None = None,
) -> list[Proof]:
def _prove_claim_rpc(claim: KClaim) -> Proof:
return self.prove_claim_rpc(
@@ -372,13 +392,16 @@ def _prove_claim_rpc(claim: KClaim) -> Proof:
fallback_on=fallback_on,
interim_simplification=interim_simplification,
no_post_exec_simplify=no_post_exec_simplify,
max_depth=max_depth,
save_directory=options.save_directory,
max_iterations=options.max_iterations,
)

all_claims = self.get_claims(
options.spec_file,
spec_module_name=options.spec_module,
claim_labels=claim_labels,
exclude_claim_labels=exclude_claim_labels,
claim_labels=options.claim_labels,
exclude_claim_labels=options.exclude_claim_labels,
type_inference_mode=options.type_inference_mode,
)
if all_claims is None:
@@ -393,7 +416,7 @@ def get_claim_modules(
md_selector: str | None = None,
type_inference_mode: TypeInferenceMode | None = None,
) -> KFlatModuleList:
with self._temp_file() as ntf:
with self._temp_file(prefix=f'{spec_file.name}.parsed.json.') as ntf:
_kprove(
spec_file=spec_file,
kompiled_dir=self.definition_dir,
2 changes: 1 addition & 1 deletion src/tests/integration/ktool/test_imp.py
Original file line number Diff line number Diff line change
@@ -194,9 +194,9 @@ def test_prove_rpc(
{
'spec_file': Path(spec_file),
'spec_module': spec_module,
'claim_labels': [claim_id],
}
),
claim_labels=[claim_id],
kcfg_semantics=ImpSemantics(kprove.definition),
)
)