-
Notifications
You must be signed in to change notification settings - Fork 3
better KMIR show & new kmir info to get the de-refed type #648
New issue
Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.
By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.
Already on GitHub? Sign in to your account
better KMIR show & new kmir info to get the de-refed type #648
Conversation
- Create KMIRPrettyPrinter class inheriting from PrettyPrinter - Add custom ListItem formatting with proper indentation for multiline content - Implement symbol table customization for ListItem in __init__ - Use indent() function for consistent 2-space indentation - Make custom printer the default with --use-default-printer option to switch back - Add proper logging support for debugging ListItem formatting
- Add utility functions for common kmir operations - Improve code organization and reusability
- Add detailed usage examples for all new show command options - Document --nodes, --node-deltas, --omit-cells parameters - Add examples for --full-printer, --no-omit-static-info options - Include debugging workflow examples and performance analysis - Add advanced usage patterns and recommended workflows - Update command options section with all new parameters - Provide practical examples for different use cases
- Remove utils.py as it contains unused utility functions - Clean up codebase by removing dead code - No functionality is affected as the file was not imported anywhere
- Fix KeyError in unref_type when pointee_type doesn't exist in types - Add proper handling for RefType and PtrType that can be integers directly - Add new 'info' command to show type information from SMIR JSON files - Add InfoOpts class for command line options - Improve error handling and logging for missing types
1c1c178
to
0fb2cf8
Compare
- Add `kmir info` command to inspect SMIR JSON metadata, allowing users to query specific type IDs. - Update README with usage examples for the new `info` command, including details on the `--types` option. - Refactor imports in `__main__.py` and `kprint.py` for clarity and correctness. - Clean up whitespace in several files for improved code readability.
kmir/src/kmir/smir.py
Outdated
type_info = self.types[ty] | ||
while isinstance(type_info, RefT): | ||
if Ty(type_info.pointee_type) not in self.types: | ||
_LOGGER.warning(f'Pointee type {Ty(type_info.pointee_type)} not found in types for reference type {ty}') |
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
Maybe we should reduce the verbosity here? It is a kind of "warning" but we expect some of the pointees to be unavailable at this point.
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
I changed to use info
. What do you think?
# Show specific nodes only | ||
uv --project kmir run kmir show proof_id --proof-dir ./proof_dir --nodes "1,2,3" | ||
|
||
# Show node deltas (transitions between specific nodes) | ||
uv --project kmir run kmir show proof_id --proof-dir ./proof_dir --node-deltas "1:2,3:4" | ||
|
||
# Display full node information (default is compact) | ||
uv --project kmir run kmir show proof_id --proof-dir ./proof_dir --full-printer | ||
|
||
# Show static information cells (functions, types, etc.) | ||
uv --project kmir run kmir show proof_id --proof-dir ./proof_dir --no-omit-static-info | ||
|
||
# Show current body cell content | ||
uv --project kmir run kmir show proof_id --proof-dir ./proof_dir --no-omit-current-body | ||
|
||
# Omit specific cells from output | ||
uv --project kmir run kmir show proof_id --proof-dir ./proof_dir --omit-cells "cell1,cell2" | ||
|
||
# Combine multiple options for detailed analysis | ||
uv --project kmir run kmir show proof_id --proof-dir ./proof_dir --full-printer --no-omit-static-info --nodes "1,2" --verbose |
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
These options are not currently implemented (would be in options.py
) ...
Were you planning to extend the PR with them ?
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
They are not available? let me check. Because I use cherry-pick to get this branch, it may lost something.
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
Sorry, I missed this commit. These options should be able to use now.
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
These cells will be omitted by default:
omit_cells: ('<functions>', '<start-symbol>', '<types>', '<adt-to-ty>', '<currentBody>')
…g options - Add nodes, node_deltas, and omit_cells parameters to ShowOpts - Implement default static info cells omission (functions, start-symbol, types, adt-to-ty) - Add --no-omit-static-info option to display static information - Add --use-default-printer option to switch between custom and standard printers - Change default behavior: --full-printer now defaults to False - Consolidate omit_labels and omit_cells into unified omit_cells parameter - Update _kmir_show function to handle new parameters correctly
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
This will have some fall-out in the kompass
repo but is definitely very useful, the new show
options make a lot of sense!
- provide more options to `kmir show`; - add a new command `kmir info` to show the dereferenced types.
kmir show
;kmir info
to show the dereferenced types.