Skip to content

Minimize JSON output by dropping unused attributes#3568

Merged
rv-jenkins merged 7 commits intodevelopfrom
minimize-json
Aug 10, 2023
Merged

Minimize JSON output by dropping unused attributes#3568
rv-jenkins merged 7 commits intodevelopfrom
minimize-json

Conversation

@ehildenb
Copy link
Copy Markdown
Member

@ehildenb ehildenb commented Aug 10, 2023 •
edited
Loading

Part of: #3540

This PR minimizes the JSON output of definitions dramatically by doing three things:

  • Encoding KVariable sort directly instead of as an attribute (breaking change, version bump induced).
  • Dropping attributes on KTokens, KApply, and InjectedKLabel (the parser was not reading these back in, and pyk is not reading these).
  • Dropping attributes on KRewrite and KAs, as well as dropping reading these in the parser (pyk is not reading these).

This should speed up definition loading time for KEVM a bit, it dropped the overall definition size in compiled.json from 22MB => 9MB.

@ehildenb ehildenb self-assigned this Aug 10, 2023
@rv-jenkins rv-jenkins merged commit 2767970 into develop Aug 10, 2023
@rv-jenkins rv-jenkins deleted the minimize-json branch August 10, 2023 22:24
@tothtamas28 tothtamas28 mentioned this pull request Aug 11, 2023
Merged
@ehildenb ehildenb mentioned this pull request Aug 14, 2023
Merged
@radumereuta radumereuta mentioned this pull request Oct 23, 2023
Closed
5 tasks
@Baltoli Baltoli mentioned this pull request Dec 12, 2023
Closed
@ehildenb ehildenb mentioned this pull request Feb 27, 2024
Merged
rv-jenkins pushed a commit to runtimeverification/pyk that referenced this pull request Feb 28, 2024
@ehildenb @rv-auditor
Several small KCFG and CTermSymbolic class refactors/cleanups (#926)
21af7b6 
While working on some larger KCFG/CTermSymbolic refactors/cleanups
(https://github.com/runtimeverification/pyk/issues/918 and
https://github.com/runtimeverification/pyk/issues/919), several smaller
changes came up, which are in this PR.

- When inserting `CTerm` into the KCFG, we used to process it to remove
source locations from the term. But since
runtimeverification/k#3568, we no longer have
attributes on `KInner`. So that processing routine is removed from
`Node` insertion, and the routine `remove_source_attributes` is removed
from `kast/manip.py` as well as it's not used.
- A feature of `KCFG.successors`, `KCFG.predecessors`, and
`KCFG.reachable_nodes`, where the user could select which types of edges
to traverse, is removed. This feature is not used anywhere, and only had
a single test (which is now removed).
- It's enforced that subclasses of `KCFG.Successor` must implement the
`to_dict` method.
- All methods of `CTermSymbolic` have the `module_name: str | None`
parameter added to them, and passed through to the RPC server.
- Methods `CTermSymbolic.{simplify,assume_defined}` are refactored to
amke use of existing `CTermSymbolic.kast_simplify` method.
- Several unused methods in `kast/manip.py` are removed,
`omit_large_tokens`, `remove_constraint_clauses_for`, and
`remove_constraints_for`.

---------

Co-authored-by: devops <devops@runtimeverification.com>
Baltoli pushed a commit that referenced this pull request Apr 9, 2024
@ehildenb @rv-auditor
Several small KCFG and CTermSymbolic class refactors/cleanups (#926)
904619f 
While working on some larger KCFG/CTermSymbolic refactors/cleanups
(https://github.com/runtimeverification/pyk/issues/918 and
https://github.com/runtimeverification/pyk/issues/919), several smaller
changes came up, which are in this PR.

- When inserting `CTerm` into the KCFG, we used to process it to remove
source locations from the term. But since
#3568, we no longer have
attributes on `KInner`. So that processing routine is removed from
`Node` insertion, and the routine `remove_source_attributes` is removed
from `kast/manip.py` as well as it's not used.
- A feature of `KCFG.successors`, `KCFG.predecessors`, and
`KCFG.reachable_nodes`, where the user could select which types of edges
to traverse, is removed. This feature is not used anywhere, and only had
a single test (which is now removed).
- It's enforced that subclasses of `KCFG.Successor` must implement the
`to_dict` method.
- All methods of `CTermSymbolic` have the `module_name: str | None`
parameter added to them, and passed through to the RPC server.
- Methods `CTermSymbolic.{simplify,assume_defined}` are refactored to
amke use of existing `CTermSymbolic.kast_simplify` method.
- Several unused methods in `kast/manip.py` are removed,
`omit_large_tokens`, `remove_constraint_clauses_for`, and
`remove_constraints_for`.

---------

Co-authored-by: devops <devops@runtimeverification.com>
Baltoli pushed a commit that referenced this pull request Apr 9, 2024
@ehildenb @rv-auditor
Several small KCFG and CTermSymbolic class refactors/cleanups (runtim…
a6fc3a2 
…everification/pyk#926)

While working on some larger KCFG/CTermSymbolic refactors/cleanups
(https://github.com/runtimeverification/pyk/issues/918 and
https://github.com/runtimeverification/pyk/issues/919), several smaller
changes came up, which are in this PR.

- When inserting `CTerm` into the KCFG, we used to process it to remove
source locations from the term. But since
#3568, we no longer have
attributes on `KInner`. So that processing routine is removed from
`Node` insertion, and the routine `remove_source_attributes` is removed
from `kast/manip.py` as well as it's not used.
- A feature of `KCFG.successors`, `KCFG.predecessors`, and
`KCFG.reachable_nodes`, where the user could select which types of edges
to traverse, is removed. This feature is not used anywhere, and only had
a single test (which is now removed).
- It's enforced that subclasses of `KCFG.Successor` must implement the
`to_dict` method.
- All methods of `CTermSymbolic` have the `module_name: str | None`
parameter added to them, and passed through to the RPC server.
- Methods `CTermSymbolic.{simplify,assume_defined}` are refactored to
amke use of existing `CTermSymbolic.kast_simplify` method.
- Several unused methods in `kast/manip.py` are removed,
`omit_large_tokens`, `remove_constraint_clauses_for`, and
`remove_constraints_for`.

---------

Co-authored-by: devops <devops@runtimeverification.com>
Baltoli pushed a commit that referenced this pull request Apr 9, 2024
@ehildenb @rv-auditor @Baltoli
Several small KCFG and CTermSymbolic class refactors/cleanups (runtim…
33077f8 
…everification/pyk#926)

While working on some larger KCFG/CTermSymbolic refactors/cleanups
(https://github.com/runtimeverification/pyk/issues/918 and
https://github.com/runtimeverification/pyk/issues/919), several smaller
changes came up, which are in this PR.

- When inserting `CTerm` into the KCFG, we used to process it to remove
source locations from the term. But since
#3568, we no longer have
attributes on `KInner`. So that processing routine is removed from
`Node` insertion, and the routine `remove_source_attributes` is removed
from `kast/manip.py` as well as it's not used.
- A feature of `KCFG.successors`, `KCFG.predecessors`, and
`KCFG.reachable_nodes`, where the user could select which types of edges
to traverse, is removed. This feature is not used anywhere, and only had
a single test (which is now removed).
- It's enforced that subclasses of `KCFG.Successor` must implement the
`to_dict` method.
- All methods of `CTermSymbolic` have the `module_name: str | None`
parameter added to them, and passed through to the RPC server.
- Methods `CTermSymbolic.{simplify,assume_defined}` are refactored to
amke use of existing `CTermSymbolic.kast_simplify` method.
- Several unused methods in `kast/manip.py` are removed,
`omit_large_tokens`, `remove_constraint_clauses_for`, and
`remove_constraints_for`.

---------

Co-authored-by: devops <devops@runtimeverification.com>
Baltoli pushed a commit that referenced this pull request Apr 10, 2024
@ehildenb @rv-auditor @Baltoli
Several small KCFG and CTermSymbolic class refactors/cleanups (runtim…
37ef23c 
…everification/pyk#926)

While working on some larger KCFG/CTermSymbolic refactors/cleanups
(https://github.com/runtimeverification/pyk/issues/918 and
https://github.com/runtimeverification/pyk/issues/919), several smaller
changes came up, which are in this PR.

- When inserting `CTerm` into the KCFG, we used to process it to remove
source locations from the term. But since
#3568, we no longer have
attributes on `KInner`. So that processing routine is removed from
`Node` insertion, and the routine `remove_source_attributes` is removed
from `kast/manip.py` as well as it's not used.
- A feature of `KCFG.successors`, `KCFG.predecessors`, and
`KCFG.reachable_nodes`, where the user could select which types of edges
to traverse, is removed. This feature is not used anywhere, and only had
a single test (which is now removed).
- It's enforced that subclasses of `KCFG.Successor` must implement the
`to_dict` method.
- All methods of `CTermSymbolic` have the `module_name: str | None`
parameter added to them, and passed through to the RPC server.
- Methods `CTermSymbolic.{simplify,assume_defined}` are refactored to
amke use of existing `CTermSymbolic.kast_simplify` method.
- Several unused methods in `kast/manip.py` are removed,
`omit_large_tokens`, `remove_constraint_clauses_for`, and
`remove_constraints_for`.

---------

Co-authored-by: devops <devops@runtimeverification.com>
Baltoli pushed a commit that referenced this pull request Apr 10, 2024
@ehildenb @rv-auditor @Baltoli
Several small KCFG and CTermSymbolic class refactors/cleanups (runtim…
c64fb1d 
…everification/pyk#926)

While working on some larger KCFG/CTermSymbolic refactors/cleanups
(https://github.com/runtimeverification/pyk/issues/918 and
https://github.com/runtimeverification/pyk/issues/919), several smaller
changes came up, which are in this PR.

- When inserting `CTerm` into the KCFG, we used to process it to remove
source locations from the term. But since
#3568, we no longer have
attributes on `KInner`. So that processing routine is removed from
`Node` insertion, and the routine `remove_source_attributes` is removed
from `kast/manip.py` as well as it's not used.
- A feature of `KCFG.successors`, `KCFG.predecessors`, and
`KCFG.reachable_nodes`, where the user could select which types of edges
to traverse, is removed. This feature is not used anywhere, and only had
a single test (which is now removed).
- It's enforced that subclasses of `KCFG.Successor` must implement the
`to_dict` method.
- All methods of `CTermSymbolic` have the `module_name: str | None`
parameter added to them, and passed through to the RPC server.
- Methods `CTermSymbolic.{simplify,assume_defined}` are refactored to
amke use of existing `CTermSymbolic.kast_simplify` method.
- Several unused methods in `kast/manip.py` are removed,
`omit_large_tokens`, `remove_constraint_clauses_for`, and
`remove_constraints_for`.

---------

Co-authored-by: devops <devops@runtimeverification.com>
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment

Reviewers

@tothtamas28 tothtamas28 Awaiting requested review from tothtamas28

@gtrepta gtrepta Awaiting requested review from gtrepta

1 more reviewer

@radumereuta radumereuta radumereuta approved these changes

Reviewers whose approvals may not affect merge requirements

Assignees

@ehildenb ehildenb

Labels

automerge

Projects

None yet

Milestone

No milestone

Development

Successfully merging this pull request may close these issues.

3 participants

@ehildenb @radumereuta @rv-jenkins