This PR is for making it easier to work on proofs with default pyk prove ... functionalities.
Factor out and reuse SpecOptions in ProveOptions class.
Add options to pyk prove:
--max-iterations: control how many iterations of proof extension to do.
--max-depth: control the maximum number of steps to take in an execute request.
--save-directory: allow saving off the proof state after executing it.
--temp-directory: allow setting the temporary directory to use for intermediate artifacts.
--show-kcfg: display the resulting proof KCFG after executing the proof.
Handle the RuntimeError thrown by crashes of the call to kprove --dry-run ... directly and more gracefully, instead of printing a stack trace.
Add command pyk show which reuses a lot of the same options as pyk prove, and calls pyk prove in a way that it just loads the proof from disk and displays the KCFG.
Changes to the KProve.prove_rpc functionality:
Source many of the options from the ProveOptions class, which contains the above options and more.
Only initialize a CTermSymbolic (and thus an RPC server) if it's needed (will take more than 0 proof steps, and the proof isn't already passed).
Allow setting the prefix of the temporary file parsed to for get_claims_modules.
Modify a test in regression-new to exercise the new pyk prove --show-kcfg ... option.
Baltoli
commented
6 months ago
This PR is for making it easier to work on proofs with default
pyk prove ...functionalities.SpecOptionsinProveOptionsclass.pyk prove:--max-iterations: control how many iterations of proof extension to do.--max-depth: control the maximum number of steps to take in anexecuterequest.--save-directory: allow saving off the proof state after executing it.--temp-directory: allow setting the temporary directory to use for intermediate artifacts.--show-kcfg: display the resulting proof KCFG after executing the proof.RuntimeErrorthrown by crashes of the call tokprove --dry-run ...directly and more gracefully, instead of printing a stack trace.pyk showwhich reuses a lot of the same options aspyk prove, and callspyk provein a way that it just loads the proof from disk and displays the KCFG.KProve.prove_rpcfunctionality:ProveOptionsclass, which contains the above options and more.CTermSymbolic(and thus an RPC server) if it's needed (will take more than 0 proof steps, and the proof isn't already passed).get_claims_modules.regression-newto exercise the newpyk prove --show-kcfg ...option.