Skip to content
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.

Sign up for GitHub

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

Jump to bottom

Heapster string literals #1456

Merged
merged 35 commits into from
Sep 15, 2021
Merged

Heapster string literals #1456

merged 35 commits into from
Sep 15, 2021

Conversation

eddywestbrook
Copy link
Contributor

Added support to Heapster for translating global constants in LLVM files, including string literals, into Heapster permissions and translations.

This also required the following changes:

  • Implemented support for Rust slice types (of a single field)
  • Added support for existential shapes in Rust function types
  • Added type-checking support for the Crucible BVZext and BVTrunc instructions
  • Added a number of useful combinators to OpenTerm
  • Added heapster_init_env_debug and heapster_init_env_from_file_debug commands, to turn on debugging as a Heapster environment is created

Eddy Westbrook added 30 commits August 31, 2021 12:27
fixed the IRT description generation to match the recent change that …
884b584 
…made the translation of bitvector permissions to just be bitvectors
Merge branch 'heapster-fix-memcpy-bug' into heapster-bugfix-bitvector…
e98bd33 
…-irts
Merge branch 'master' into heapster-bugfix-bitvector-irts
6387369
updated xor_swap_rust example to use the Rust type in the SAW script
5b5f422
added a case to the Rust to Heapster translator to handle function ty…
7b7709f 
…pes with no return value
whoops, forgot to update the bitcode file for xor_swap_rust
c18aec7
bugfix in the Rust to Heapster translator: empty return types need to…
5bc366a 
… be converted to unit, not to the empty struct
tweaked the error message for when Rust types do not translate correc…
068b735 
…tly to the expected LLVM type
started adding support for string literals by moving all creation of …
f63c326 
…a HeapsterEnv into a single function which iterates through the globals and adds those it can handle
added a formatting example in Rust, and started defining the necessar…
2720516 
…y types for it
started trying to figure out how Rust stores string literals in its g…
a6aee80 
…enerated LLVM files
Merge branch 'master' into heapster-string-literals
cd01dab
fixed the prtty-printing for constant values
024287e
changed TrueEnum::fmt to use the fmt method rather than the write! macro
917547e
whoops, changed the fmt method for TrueEnum back to using the write! …
389d0d2 
…macro, because that seems to be the proper way to do things
whoops, forgot to add the repr(u64) pragma to the TrueEnum type
f0ed90b
added a type-checking command for TrueEnum::fmt
1d6a5d7
moved some OpenTerm operators from SAWTranslation.hs to OpenTerm.hs
e987f42
added llvmReadBlockOfShape
2752723
more work trying to translate globals
92d04e1
got string literals translated, but now there is some translation bug...
4f911f7
whoops, translating a shape always yields exactly one term
64d3006
added helper function exprLLVMTypeBytes
01074a9
added support for Rust slice types
d2b4a22
whoops, combined the two cases for translating shared vs mutable refe…
3941cdb 
…rences into one
updated funPerm3FromArgLayout to handle layouts with existential perm…
2982d1f 
…issions
updated the rust_data example to use string literals
281d602
moved the LLVM globals code to a new file LLVMGlobalConst.hs
f0e36a1
fixed the translation of LLVM array constants to generate SAW core BV…
1eb2323 
…Vecs instead of SAW core Vecs
regenerated Coq files for saw-core-coq
9347756
ChrisEPhifer
ChrisEPhifer approved these changes Sep 15, 2021
View reviewed changes
Copy link
Member

@ChrisEPhifer ChrisEPhifer left a comment

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Everything here seems sensible to me; I'll admit I'm not the best person to check on things related to Crucible/SAWCore, but everything related to Rust translations seems good.

@eddywestbrook eddywestbrook added subsystem: heapster Issues specifically related to memory verification using Heapster PR: ready to merge Magic flag for pull requests to ask Mergify to merge given an approval and a successful CI run labels Sep 15, 2021
@eddywestbrook eddywestbrook merged commit 33fdd18 into master Sep 15, 2021
@mergify mergify bot deleted the heapster-string-literals branch September 15, 2021 18:00
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Reviewers

@ChrisEPhifer ChrisEPhifer ChrisEPhifer approved these changes

Assignees
No one assigned
Labels
PR: ready to merge Magic flag for pull requests to ask Mergify to merge given an approval and a successful CI run subsystem: heapster Issues specifically related to memory verification using Heapster
Projects
None yet
Milestone
No milestone
Development

Successfully merging this pull request may close these issues.
2 participants
@eddywestbrook @ChrisEPhifer