Compiling SMIR JSON to kore to avoid static data in config #745
Conversation
…d program will define them)
…ables kompile to do the job)
…g-to-K * removed ADT Map * followed decoding.md and kmir.py changes
…g-to-K-generating-kore
…g-to-K-generating-kore
…c` and `prove-raw`
jberthold
force-pushed
the
EXPERIMENT-compiling-to-K-generating-kore
branch
from
9ca31ce to
56ddf51
Compare
| spec_file = tmp_path / f'{testname}.k' | ||
| gen_opts = GenSpecOpts(smir_json, spec_file, 'main') | ||
|
|
||
| proof_dir = tmp_path / 'proof' | ||
| prove_opts = ProveRawOpts(spec_file, proof_dir=proof_dir) | ||
|
|
||
| _kmir_gen_spec(gen_opts) | ||
| _kmir_prove_raw(prove_opts) | ||
|
|
||
| claim_labels = kmir.get_claim_index(spec_file).labels() | ||
| for label in claim_labels: | ||
| proof = Proof.read_proof_data(proof_dir, label) | ||
| assert proof.passed | ||
|
|
||
| prove_rs_opts = ProveRSOpts(rs_file=smir_json, smir=True) | ||
|
|
||
| PROVING_DIR = (Path(__file__).parent / 'data' / 'proving').resolve(strict=True) | ||
| PROVING_FILES = list(PROVING_DIR.glob('*-spec.k')) | ||
|
|
||
|
|
||
| @pytest.mark.parametrize( | ||
| 'spec', | ||
| PROVING_FILES, | ||
| ids=[spec.stem for spec in PROVING_FILES], | ||
| ) | ||
| def test_prove(spec: Path, tmp_path: Path, kmir: KMIR) -> None: | ||
| proof_dir = tmp_path / (spec.stem + 'proofs') | ||
| prove_opts = ProveRawOpts(spec, proof_dir=proof_dir) | ||
| _kmir_prove_raw(prove_opts) | ||
|
|
||
| claim_labels = kmir.get_claim_index(spec).labels() | ||
| for label in claim_labels: | ||
| proof = Proof.read_proof_data(proof_dir, label) | ||
| assert proof.passed | ||
| proof = KMIR.prove_rs(prove_rs_opts) | ||
| assert proof.passed |
There was a problem hiding this comment.
I have removed the single test that we had which was based on gen-spec and prove-raw, as well as switching the test_prove_termination suite to using prove_rs. This means the gen-spec and prove-raw commands are now untested. I would suggest removing them because they don't fit well with the changed execution in this PR.
There was a problem hiding this comment.
I agree, we should focus on features that are necessary to complete the proofs. Legacy and untested code should be removed.
Can you open an issue for tracking features that we should remove?
jberthold
changed the title
…before creating refs)
| <memory> ALLOCMAP </memory> | ||
| requires ALLOC_ID in_keys(ALLOCMAP) | ||
| andBool lengthBytes(BYTES) ==Int 16 // fat pointer (assumes usize == u64) | ||
| requires isValue(lookupAlloc(ALLOC_ID)) | ||
| andBool lengthBytes(BYTES) ==Int 16 // fat pointer (assumes usize == u64) |
There was a problem hiding this comment.
This is now thunking instead of creating an AllocRef to data that could not be decoded.
Expected output for enum-two-refs-fail changes because of this.
I removed the notes file that had some explanations, but yes, that's exactly it. |
3 participants
Pervasive changes to the semantics and python client code to replace the lookup tables in the config (
memory,functions,types) by lookup functions whose equations are generated from theSMIRInfoi.e., from the SMIR JSON , for each program.Previously we had
Map-sorted config cellsfunctions,typesandmemory, which are now functions instead. The function equations have to be added and then compiled with the LLVM backend for it to work, but the configuration is much smaller and does not have any static data any more.