Integrate opcode semantics summaries #2728
Conversation
Time cost with optimizations
|
|
@Stevengre Would it be possible to provide a |
Time cost with summaries
|
Stevengre
force-pushed
the
integrate-summaries
branch
from
81ee2cd to
cd037a8
Compare
|
@nishantjr Sure! The new commit provides these new targets! Hope this change is what you want! |
|
Thank you! It is! |
- Refactored the summarize function to print correct and compilable k definitions for summaries. - Added new summary targets for LLVM and Haskell backend in the KEVM plugin. - Updated the Makefile to include a new test target for `test-prove-summaries`. - Refactored the test suite to validate opcode summaries. - Adjusted imports in the driver and EDSL modules to incorporate the new summaries. - Cleaned up the `.gitignore` to ensure proper tracking of relevant files.
…and Haskell. This update expands the choices available for the `--target` argument to include `llvm-summary` and `haskell-summary`.
Stevengre
force-pushed
the
integrate-summaries
branch
from
cd037a8 to
0bfbf95
Compare
| test-prove-summaries: poetry | ||
| $(MAKE) -C kevm-pyk/ test-integration PYTEST_ARGS+="-k test_prove_summaries" |
There was a problem hiding this comment.
Should we enable these tests on CI?
There was a problem hiding this comment.
There are already summarization tests on CI? Should I delete the summarization process tests and use this one instead?
There was a problem hiding this comment.
Should I delete the summarization process tests and use this one instead?
Are these two targets interchangeable? What's the difference between test-summarize and test-prove-summaries?
There was a problem hiding this comment.
test-prove-summariesverifies the generated rules in the summaries folder.test-summarizeruns the summarization process and validate the generated kcfg using some assertions.
test-prove-summaries provides better assurance for the generated summaries, test-summarize ensures that the new introduced semantics doesn't harm the generation of the summaries.
I think the second target (target for test-summarize) is not quite useful as test-prove-summaries does. It more like update-expected.
So, we can use test-prove-summaries to replace test-summarize to verify the result of the summarization.
kevm-pyk/src/kevm_pyk/summarizer.py
Outdated
|
|
||
| ensure_dir_path(self.save_directory) | ||
| with open(self.save_directory / f'{proof.id.lower().replace("_", "-")}-summary.k', 'w') as f: | ||
| requires = [KRequire('../evm.md')] |
There was a problem hiding this comment.
Model instantiation can be moved out of the context manager's scope.
kevm-pyk/src/kevm_pyk/summarizer.py
Outdated
| kdef = KDefinition(module_name, [module], requires=requires) | ||
| f.write(self.kevm.pretty_print(kdef)) | ||
| with open(self.save_directory / 'summaries.k', 'w') as f: | ||
| k_files = sorted([f for f in self.save_directory.glob('*.k') if f.name != 'summaries.k']) |
- Changed the test suite for the 'Summarization' job from 'test-summarize' to 'test-prove-summaries'. - Adjusted timeout and parallel execution settings for the 'Summarization' job to improve performance. - Updated the build command for the distribution to include 'evm-semantics.haskell-summary' instead of 'evm-semantics.summary'.
…instantiation out of the context manager's scope.
kevm-pyk/src/kevm_pyk/summarizer.py
Outdated
| @@ -607,6 +607,110 @@ def create_kcfg_explore() -> KCFGExplore: | |||
| f.write('\n') | |||
| return passed | |||
|
|
|||
| def _transform_underscores(self, inner: KInner) -> KInner: | |||
There was a problem hiding this comment.
None of these methods refer to self, so they could be @staticmethod-s, or preferably, even module-level functions.
kevm-pyk/src/kevm_pyk/summarizer.py
Outdated
| body = self._transform_underscores(body) | ||
| requires, ensures = self._transform_underscores(requires), self._transform_underscores(ensures) | ||
| body, requires = self._transform_inf_gas(rule_id, body, requires) | ||
| body, requires = self._transform_dot_account_var(body, requires) | ||
| body, requires = self._transform_lhs_functions(rule_id, body, requires) |
kevm-pyk/src/kevm_pyk/summarizer.py
Outdated
| module_name = f'{proof.id.upper().replace("_", "-")}-SUMMARY' | ||
| requires = [KRequire('../evm.md')] | ||
| imports = [KImport('EVM')] | ||
| if proof.id == 'MSTORE8': | ||
| requires.append(KRequire('../buf.md')) | ||
| imports.append(KImport('BUF')) | ||
| sentences = self._to_rules(proof) | ||
| module = KFlatModule(module_name, sentences=sentences, imports=imports) | ||
| kdef = KDefinition(module_name, [module], requires=requires) |
There was a problem hiding this comment.
Consider extracting a helper.
kevm-pyk/src/kevm_pyk/summarizer.py
Outdated
| k_files = sorted([f for f in self.save_directory.glob('*.k') if f.name != 'summaries.k']) | ||
| module_names = [f.stem.upper() for f in k_files] | ||
| requires = [KRequire(k_file.name) for k_file in k_files] | ||
| imports = [KImport(module_name) for module_name in module_names] | ||
| module = KFlatModule('KEVM-SUMMARIES', imports=imports) | ||
| kdef = KDefinition('KEVM-SUMMARIES', [module], requires=requires) |
…functions to get the summary kdefinition for printing.
test-prove-summaries..gitignoreto ensure proper tracking of relevant files.