Value-set of pointers #2
Draft
Conversation
This file contains hidden or 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
This is part of our streamlining and cleanup of our CI infrastructure.
This helps us validate that the new job is working as it should, by being the only one that should be submitting results under the currently active token.
There was a problem with symtab2gb and libour_archive.a not being added as a target during coverage builds, whic was causing some of the tests under cbmc/regression/symtab2gb and cbmc/regression/goto-gcc/archives to fail.
…_port [CI] Port CMake Codecov job from Codebuild to Github Actions.
jezhiggins
force-pushed
the
vsd-value-set-implementation
branch
from
724bb13 to
f363e38
Compare
jezhiggins
force-pushed
the
vsd-value-set-of-pointers
branch
3 times, most recently
from
8298fb8 to
a0479f9
Compare
…entation Vsd value set implementation
jezhiggins
force-pushed
the
vsd-value-set-of-pointers
branch
3 times, most recently
from
85160cc to
8342a92
Compare
Although our implementation does not care about the suffix, we should avoid surprises. We mostly already used .gb as a suffix in documentation, and consistently do so in regression tests. This commit fixes the remaining occurrences of .goto in documentation, replacing all of them by .gb.
This adds support for the distinct operator in SMTlib, by directly translating it into "not equal" Prior to this change, the distinct operator was ignored, giving incorrect results
fix distinct operator
Documentation: consistently use .gb suffix for goto binaries
The special-casing of the endianness encoding handled by bv_endianness_mapt is really specific to bv_pointerst, not boolbvt in general. Thus, move this data structure to bv_pointers.cpp and enable overriding the endianness map from boolbvt. This commit is refactoring only, no changes in behaviour intended.
With upcoming changes to pointer encoding it will be necessary to enable children of boolbvt to define their own bit encoding width of data types. This commit is refactoring only, no changes in behaviour intended.
In preparation of tweaking the propositional encoding, place all knowledge of the bit width of encoded pointers in bv_pointerst. Also, do not hard-code the width just once, but really look at each type.
We use __float128 to distinguish GCC versions, which is not a distinguishing factor for Clang. (It's supported on several Clang versions on x86, but not on Apple's M1/ARM.) This commit effectively disables the gcc_version1 test on macOS (where "gcc" really is Clang). Fixes: diffblue#5828
Store pointer encoding configuration in boolbv_widtht
The tests exercise the way the back-end encodes pointers. Upcoming encoding changes will ensure that these can soundly be handled.
Do not rely on Clang's results to verify our GCC version handling
Tests demonstrating pointer-encoding unsoundness
Instead of having in-out non-const bvt references, return bvt by value and rely on copy elision for performance. This simplifies the code in that it avoids creating (and sometimes unnecessarily resizing) objects that are then to be populated by a function. For convert_address_of_rec use optionalt<bvt> to remove the true/false error reporting.
bv_pointerst: make all members return (optional) bvt
This adds a new builtin function that allows user to explicitly check that an enum has a valid value (and also this function in an assert).
Adds regression tests for enum_is_in_range to test positive, negative and error outcomes on both named and typedef'd enumerations.
Adds documentation of how to use the CPROVER_enum_is_in_range function to explain to a user how to use this function.
This replaces a codebuild job that had not been ported yet, so that codebuild can be safely deactivated as a CI provider, having all the configurations ported so far.
Add goto-ld to .gitignore.
…_program Refactor process_goto_program so that all tools use common processing code
An assignment may invalidate pointers used in the left-hand side. In case the result of the assignment is used, we therefore cannot re-use the left-hand side to represent the result. Instead, introduce temporaries as needed to store the right-hand side value, and use the temporary to represent the result. Fixes: diffblue#5857
Add some information to the readme with regard to the main platforms we are building/testing CBMC on Github Actions.
[CI] Cleanup .github/ folder
Assignment side effects may require additional temporaries
The fixes in diffblue#5858 addressed the problem of assignments having side effects, but did not consider function calls or pre-increment/decrement, which eventually also yield assignments, and thus may have similar side effects.
fixup! Assignment side effects may require additional temporaries
This mirrors the change in diffblue#5861 by replacing the use of code_deadt by directly returning the symbol_exprt. The client code is simplified.
This addresses the issue of the ambiguous dual-use of code_declt in both the C front-end and the goto-program API by replacing the use of code_declt by directly returning the symbol_exprt. The client code is simplified.
This mirrors the change in diffblue#5861 by replacing the use of code_returnt by directly returning the return value expression. The client code is simplified considerably.
De-duplicate explicit-allocation check construction
introduce instructiont::return_value()
introduce instructiont::dead_symbol()
This replaces the use of code_assignt by an explicit lhs/rhs pair in goto symex. This avoids constructing the code_assignt in a number of places.
Before it was using the index operator. However, since there is no initialisation, this caused an error if there was unreachable code in the goto model. This can be fixed by simply using abstract_state_before which will always return a valid domain state (bottom for unreachable code) instead.
…x/constant-propagator-bug Fix bug in constant propagator
symex: use lhs/rhs instead of code_assignt
introduce instructiont::decl_symbol()
Loops with multiple entry points previously resulted in unlimited unwinding as loop counters were wrongly being reset via edges leaving one of the loops (and entering the other).
Fix formatting issues in the --help output text
Loop counter resetting must not result in unlimited unwinding
Introduce new base class, abstract_pointer_objectt. It should be, but is not yet, an abstract (in C++ terms) class as it's not intended to be directly instantiable. pointer_abstract_object now renamed two_value_pointer_abstract_objectt. constant_pointer_abstract_objectt and two_value_pointer_abstract_objectt are now peers. Deleted the unused value_set_pointer_abstract_objectt in anticipation of reintroducing a more functional value-set pointer representation shortly.
Stripped back value_set_abstract_object now it doesn't have to deal with pointers. Pulled out abstract_object_sett as a type not just an alias. Add behaviour with functions pulled across from value_set_abstract_objectt and value_set_pointer_abstract_objectt.
Remove expression_transform and write from value-set of pointers. Dereference value-set of pointers to a single value
Test uses intervals. Value-sets should also work but we can't write that test yet as we needs more work on asserting value-set equality.
Tests determinate and indeterminate write through a pointer
jezhiggins
force-pushed
the
vsd-value-set-of-pointers
branch
from
8342a92 to
df41607
Compare
…nters Vsd value set of pointers
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 leads on from diffblue#5793, separating out value-sets of constants from value-sets of pointers.
Prior to this work,
value_set_abstract_objecttdid double duty for constants and pointers, contained a certain amount of runtime type checking to do the right thing, did a decent job for values, but a poor job for pointers. Separating the two out isolates the constant and pointer specific behaviours, immediately increasing clarity and enabling some easy fixes for pointer dereferencing and writing through.I could have gone further, as there's the pointer behaviour, while improved, is not complete, and there's still a certain amount of duplication that could be eliminated. However, I believe much of this will be addressed, and actually more easily addressed, in the upcoming working on multiple-dispatch/cross-representation evaluation and merge.