Limited x86 verification from SAWScript #630
Merged
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
Now works on a function from SIKE p434
andreistefanescu
approved these changes
Feb 4, 2020
There was a problem hiding this comment.
@chameco nice job! Mostly nits, let's try to track alignment as much as possible
|
@chameco thank you for addressing all comments. Please go ahead and merge this. |
RyanGlScott
added
the
subsystem: x86
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.
This PR adds a new toplevel command,
crucible_llvm_verify_x86 : LLVMModule -> String -> String -> [(String, Int)] -> CrucibleSetup () -> TopLevel CrucibleMethodSpec. This command takes the path to an ELF file, the name of a symbol in that ELF file, and a specification of the same type that would be passed tocrucible_llvm_verify. The x86_64 function corresponding to the given symbol is simulated usingmacaw-symbolicandcrucible, and a method spec corresponding to the external declaration of that symbol in the given LLVM module is returned. The initial state of memory and any postconditions to check are derived from the given specification.(The unmentioned
[(String, Int)]argument is a list associating symbol names of global variables with sizes.)Notable limitations / eventual to-do list:
At present, this feature is therefore only really usable for verifying memory safety of x86_64 functions (ideally call graph leaves) called from LLVM, and then using those functions as overrides without having to write two specifications. (Fortunately, that's also exactly my use case 🙂 )