Repository navigation
Construct KCFGs for Foundry proof obligations - #1372
Conversation
tothtamas28
left a comment
tothtamas28
left a comment
There was a problem hiding this comment.
LGTM. Added some comments for potential follow-up tasks.
| kevm.prove( | ||
| foundry_main_file, | ||
| spec_module_name=spec_module, | ||
| dry_run=True, | ||
| args=(['--emit-json-spec', str(parsed_spec)] + prove_args), | ||
| ) |
There was a problem hiding this comment.
Ideally we should emit the JSON spec (or the CFGs) directly. Is that feasible?
There was a problem hiding this comment.
Yes, it's feasible. I thought of it after opening this PR, but figured it could wait.
There was a problem hiding this comment.
I can change it though.
| _LOGGER.info(f'Producting KCFG: {cfg_label}') | ||
| cfgs[cfg_label] = KCFG_from_claim(kevm.definition, claim).to_dict() | ||
| with open(kcfgs_file, 'w') as kf: | ||
| kf.write(json.dumps(cfgs)) |
There was a problem hiding this comment.
What is the advantage of having a single file for all the specs? (I guess we have a single main file because kompiling all modules at once is more efficient than kompiling them separately. But for the specs it shouldn't matter, right?)
There was a problem hiding this comment.
You mean a single file for all the KCFGs? I think that it's actually a disadvantage, but it matched more closely what the summarizer expects as input, so I figured I would stick to that. I can change it though.
| foundry_definition_dir = foundry_out / 'kompiled' | ||
| foundry_main_file = foundry_definition_dir / 'foundry.k' |
There was a problem hiding this comment.
Unrelated to this PR: I think we should have a separate folder for the K specs.
There was a problem hiding this comment.
Perhaps. I don't think ti matters to much where it goes. But I do want to put it in the Foundry output directory, to keep it in snyc with the other artifacts there.
| return _flat_module_list | ||
|
|
||
|
|
||
| def KCFG_from_claim(defn: KDefinition, claim: KClaim) -> KCFG: # noqa: N802 |
There was a problem hiding this comment.
Is this following section copy-pasted from ksummarize? We should probably upstream this to pyk (with unit tests).
There was a problem hiding this comment.
Yes, it's directly from KSummarize.
There was a problem hiding this comment.
Well, not quite actually. Directly from KSummarize, then minor refactor.
There was a problem hiding this comment.
It's recorded here: https://github.com/runtimeverification/ksummarize/issues/82
|
This is the first time I have seen this "KCFG"-mode. Is it documented somewhere? |
|
@RaoulSchaffranek no it's not documented anywhere, implementation here: https://github.com/runtimeverification/pyk/blob/master/src/pyk/kcfg.py |
Co-authored-by: Tamás Tóth <tothtamas28@users.noreply.github.com>
Fixes: #1358
Instead of storing K claims for each Foundry test, we store KCFGs with the proof obligations.
--reparseand--reinittofoundry-kompile, which enables re-parsingfoundry.ktospec.json, and regeneratingkcfgs.jsonfromspec.json, respectively. This requires pulling in several downstream functions from ksummarize:KCFG_from_claimandsanitize_config.read_kast_flatmodulelistfor reading the output ofkprove --emit-json-spec ....utils.py(which have been upstreamed/replaced):get_productions,get_production_for_klabel, andget_label_for_cell_sorts..AccountCellMapto be as.Baginstead of empty. When there are 1 or more accounts, it's ok to unparse.AccountCellMapas empty, but when there are no accounts, you get things like( => ?_ACCOUNTS_FINAL). In both cases (no accounts, some accounts), it's safe to use.Bag.