Command tweaks #81
Merged
Command tweaks #81
Conversation
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Make continue/step/interrupt easier to access, leaving the other commands accessible via the minibuffer.
One of the helpers in Commands.hs took the quantified state while the other used the unquantified state. Make them both take the unquantified state (which makes more type variables visible).
This will ensure that exceptions are propagated
Audit some commands to better specify when they are valid (e.g., stepping execution is only possible when there is a current symbolic execution context). This commit also moves some command helpers (predicates as well as value extractors) to the core state module.
When resuming symbolic execution, send the symbolic execution session to "Executing" mode, which displays collected statistics. This affects both stepping and continuing. As part of that, add the profiling feature to the crux-dbg frontend (so metrics can be shown while execution proceeds). Also: - Removes some calls to error by adding an empty metrics value - Adds a more precise predicate to the "interrupt" command (only available during "execution" mode
This includes compiled bitcode (for now)
This also exports the overrides so that they could be reused elsewhere
This means that any failed assertion will trigger the debugger without the user having to change to crucible_debug_assert. This might be something that needs to change in practice (to be more configurable).
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment
Add this suggestion to a batch that can be applied as a single commit.
This suggestion is invalid because no changes were made to the code.
Suggestions cannot be applied while the pull request is closed.
Suggestions cannot be applied while viewing a subset of changes.
Only one suggestion per line can be applied in a batch.
Add this suggestion to a batch that can be applied as a single commit.
Applying suggestions on deleted lines is not supported.
You must change the existing code in this line in order to create a valid suggestion.
Outdated suggestions cannot be applied.
This suggestion has been applied or marked resolved.
Suggestions cannot be applied from pending reviews.
Suggestions cannot be applied on multi-line comments.
Suggestions cannot be applied while the pull request is queued to merge.
Suggestion cannot be applied right now. Please check back later.
Start cleaning up some commands and keymaps to improve the user experience