Read-only memory sections maintained throughout program #92
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
added 4 commits
October 9, 2023 09:55
…es, add useArrayAxioms flag to test suite, update readme with information about that
…amma_mem[i] == old(Gamma_mem[i]))))) to empty relies
This was referenced Oct 9, 2023
Merged
|
Can we add a doc comment to explain specifically which elf section is included and why, i.e. the outcome of the email discussion about which sections are modifiable. Correct me if I'm wrong but might we want to do future work to map in more memory from the elf header to include the statically initialized but mutable values? |
|
We do already have some of the statically initialised but mutable sections, but I'll add comments to document it. |
added 3 commits
October 17, 2023 11:27
# Conflicts: # src/main/scala/ir/Program.scala # src/main/scala/translating/IRToBoogie.scala # src/main/scala/util/RunUtils.scala # src/test/correct/basicfree/clang/basicfree.expected # src/test/correct/basicfree/clang_no_plt_no_pic/basicfree.expected # src/test/correct/basicfree/clang_pic/basicfree.expected # src/test/correct/basicfree/gcc/basicfree.expected # src/test/correct/basicfree/gcc_no_plt_no_pic/basicfree.expected # src/test/correct/basicfree/gcc_pic/basicfree.expected # src/test/correct/function1/clang/function1.expected # src/test/correct/function1/clang_O2/function1.expected # src/test/correct/function1/clang_no_plt_no_pic/function1.expected # src/test/correct/function1/clang_pic/function1.expected # src/test/correct/function1/gcc/function1.expected # src/test/correct/function1/gcc_O2/function1.expected # src/test/correct/function1/gcc_no_plt_no_pic/function1.expected # src/test/correct/function1/gcc_pic/function1.expected # src/test/correct/functions_with_params/clang/functions_with_params.expected # src/test/correct/functions_with_params/clang_no_plt_no_pic/functions_with_params.expected # src/test/correct/functions_with_params/clang_pic/functions_with_params.expected # src/test/correct/functions_with_params/gcc/functions_with_params.expected # src/test/correct/functions_with_params/gcc_no_plt_no_pic/functions_with_params.expected # src/test/correct/functions_with_params/gcc_pic/functions_with_params.expected # src/test/correct/indirect_call/clang/indirect_call.expected # src/test/correct/indirect_call/clang_O2/indirect_call.expected # src/test/correct/indirect_call/clang_no_plt_no_pic/indirect_call.expected # src/test/correct/indirect_call/clang_pic/indirect_call.expected # src/test/correct/indirect_call/gcc/indirect_call.expected # src/test/correct/indirect_call/gcc_O2/indirect_call.expected # src/test/correct/indirect_call/gcc_no_plt_no_pic/indirect_call.expected # src/test/correct/indirect_call/gcc_pic/indirect_call.expected # src/test/correct/jumptable/gcc/jumptable.expected # src/test/correct/jumptable/gcc_pic/jumptable.expected # src/test/correct/malloc_with_local/clang/malloc_with_local.expected # src/test/correct/malloc_with_local/clang_O2/malloc_with_local.expected # src/test/correct/malloc_with_local/clang_no_plt_no_pic/malloc_with_local.expected # src/test/correct/malloc_with_local/clang_pic/malloc_with_local.expected # src/test/correct/malloc_with_local/gcc/malloc_with_local.expected # src/test/correct/malloc_with_local/gcc_O2/malloc_with_local.expected # src/test/correct/malloc_with_local/gcc_no_plt_no_pic/malloc_with_local.expected # src/test/correct/malloc_with_local/gcc_pic/malloc_with_local.expected # src/test/correct/malloc_with_local2/clang/malloc_with_local2.expected # src/test/correct/malloc_with_local2/clang_O2/malloc_with_local2.expected # src/test/correct/malloc_with_local2/clang_no_plt_no_pic/malloc_with_local2.expected # src/test/correct/malloc_with_local2/clang_pic/malloc_with_local2.expected # src/test/correct/malloc_with_local2/gcc/malloc_with_local2.expected # src/test/correct/malloc_with_local2/gcc_O2/malloc_with_local2.expected # src/test/correct/malloc_with_local2/gcc_no_plt_no_pic/malloc_with_local2.expected # src/test/correct/malloc_with_local2/gcc_pic/malloc_with_local2.expected # src/test/correct/malloc_with_local3/clang/malloc_with_local3.expected # src/test/correct/malloc_with_local3/clang_O2/malloc_with_local3.expected # src/test/correct/malloc_with_local3/clang_no_plt_no_pic/malloc_with_local3.expected # src/test/correct/malloc_with_local3/clang_pic/malloc_with_local3.expected # src/test/correct/malloc_with_local3/gcc/malloc_with_local3.expected # src/test/correct/malloc_with_local3/gcc_O2/malloc_with_local3.expected # src/test/correct/malloc_with_local3/gcc_no_plt_no_pic/malloc_with_local3.expected # src/test/correct/malloc_with_local3/gcc_pic/malloc_with_local3.expected # src/test/correct/multi_malloc/clang/multi_malloc.expected # src/test/correct/multi_malloc/clang_O2/multi_malloc.expected # src/test/correct/multi_malloc/clang_no_plt_no_pic/multi_malloc.expected # src/test/correct/multi_malloc/clang_pic/multi_malloc.expected # src/test/correct/multi_malloc/gcc/multi_malloc.expected # src/test/correct/multi_malloc/gcc_O2/multi_malloc.expected # src/test/correct/multi_malloc/gcc_no_plt_no_pic/multi_malloc.expected # src/test/correct/multi_malloc/gcc_pic/multi_malloc.expected # src/test/correct/switch2/clang_O2/switch2.expected # src/test/correct/switch2/gcc_O2/switch2.expected # src/test/correct/syscall/clang/syscall.expected # src/test/correct/syscall/clang_no_plt_no_pic/syscall.expected # src/test/correct/syscall/clang_pic/syscall.expected # src/test/correct/syscall/gcc/syscall.expected # src/test/correct/syscall/gcc_O2/syscall.expected # src/test/correct/syscall/gcc_no_plt_no_pic/syscall.expected # src/test/correct/syscall/gcc_pic/syscall.expected # src/test/scala/SystemTests.scala
…t went missing in a merge
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.
Addresses #81. Since Boogie does not support mutable global variable references in axioms, the solution was to place the relevant predicates in the pre- & post-conditions of every procedure, since we are safely assuming they will be maintained by the program. This allows more tests to pass than before, mostly
/gcc_pictests.The global offset table was handled by just adding in the relevant offset/address pairs listed in the
.rela.dyntable, which is sufficient for our current purposes.The following postcondition for the rely procedure in Boogie was removed if the rely is empty, as it is redundant and affects both performance and verification success:
ensures (forall i: bv64 :: (((mem[i] == old(mem[i])) ==> (Gamma_mem[i] == old(Gamma_mem[i])))))#77 was also addressed by making the tests use the
/useArrayAxiomsflag which significantly improves performance.