Turn string constraints into struct #2
Closed
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
ID_bswap was previously used without a dedicated class.
Previously only constants were supported via expression simplification.
On some systems htonl etc. are just macros (always true for big-endian systems, where they are null macros; and also true on Mac OS). For others we to provide the implementation. In all cases the full support for bswap* is necessary, and that is now available as of the preceding commit. Also fixes arpa/inet.h being unavailable on Windows/Visual Studio.
romainbrenguier
force-pushed
the
refactor/split-axiom-vectors
branch
4 times, most recently
from
c60968a to
ff28aed
Compare
romainbrenguier
force-pushed
the
refactor/split-axiom-vectors
branch
4 times, most recently
from
002bb33 to
f3088ed
Compare
This is necessary because not all functions work with goto_programt::get_function_id, e.g. those with empty bodies.
Validate referred to the old name for cproverNondetInitialize, cproverNondetValidate.
Previously this method was run after each supertype of a relevant type was initialised, e.g. if MyClass <: MySupertype <: Object, then MyClass.cproverNondetInitialize would get run after my inner Object was set up, then again after MySupertype was set up, then one more time after the whole class was set up. Now it will only run after the whole initialisation is complete. This fixes a bug where array members could have inconsistent length and data field values because they had not been initialised yet, leading to an assertion failure during nondetInitialize, and also has the desirable side-effect that an initialiser will still be run when creating a subtype.
romainbrenguier
force-pushed
the
refactor/split-axiom-vectors
branch
from
f3088ed to
857fcf9
Compare
Previously upon encountering a second array this would truncate the search for available types, but since they may have different element types this could lead to missing the availability of one or more of the element classes. Now we search array::reference every time we encounter it.
…hods-array-element-types CI lazy methods: re-explore array types with different element types
This allows the jar_file class to load from a buffer (c array) as opposed to a file
The 'core models' is a set of .class files that model core classes from the Java Class Library, such as java.lang.Object or java.lang.Thread. A minimum is necessary for CBMC to understand, e.g., when a new thread is created. These core classes live in `src/java_bytecode/library`. This commit adds support to compile and pack the core classes into a single jar file, core-models.jar, and a converter program that transforms that .jar file into a C-language array of data that can then be linked into CBMC, thus making the .jar file be present in the data segment of the CBMC ELF. Other modifications: - New option --no-core-models, allowing to disable the loading of the internal core models - make and cmake now compile the core models into a single core-models.jar - Add regression one regression tests ensuring the the core-models.jar is loaded by default
Including .Cpp file in a regression-test was causing linker issues with CMake, specifically ODR (One Definition Rule) violations. Commit addresses this by modifying the test to include the header file instead.
…ialize-after-initialize Java frontend: only run cproverNondetInitialize after all fields are initialized
JBMC Java Core models library
This adds a mechanism to the Java frontend class loader for its caller to advise it of extra class dependencies to load, and uses it from the String preprocessor to indicate that since it will add base classes to String, StringBuilder etc, then the class loader should create symbols for those bases. This restores the invariant that holds when --string-refine is not passed, that if a class references another as a base, then that other class has an entry in the symbol table (although that entry may be incomplete).
This was partially supported already, but didn't apply exactly the same rules as the whole-program instrument_cover_goals function. This factors the whole-program version to use the per-function version, and allows the configuration to be parsed up-front and passed into the per-function version.
This mirrors the existing class_hierarchyt, except that it inherits from grapht and so is suitable for use with generic graph algorithms.
…solver-ensure-class-graph-consistency Java string solver: ensure base types are loaded
Makes code of this function clearer.
CI lazy methods now notices cases like global g1 having initialiser &g2, in which case having a reference to global g1 implies a reference to global g2. Currently this only happens in the string solver in Java, where a literal's initialiser references a constant array global.
This creates String and Class literals ahead of running java_bytecode_convert_method instead of creating them in an after-the-fact fixup in typecheck_expr as previously. These now exist before method conversion begins and __CPROVER_initialize is created, which means the String literals are correctly initialised even when using incremental method conversion. This can be a little wasteful if they are only referred to from methods that would never truly be invoked, but preliminary experiments suggest that creating ~10000 Strings takes under a second, and that Java lazy loading can quickly delete ones that are not in fact used. Java CI lazy methods is augmented a little to notice that if we need global A, and global A is initialised with a reference to global B, then we need global B as well. We appear to have got away wtih this before because the inter-global references were introduced after CI lazy methods finished loading methods.
…axiom-vectors Split string generator axioms into separate vectors
Use string_split in set_classpath
…ierarchy-grapht Add class-hierarchy variant based on grapht
Implement bswap in SAT back-end
…ent_cover_per_function Coverage: support instrumenting one function at a time
…ontend-create-literal-globals-early Java frontend: create String and Class literals earlier
romainbrenguier
force-pushed
the
refactor/turn-constraint-into-struct
branch
from
69f5880 to
8300efe
Compare
romainbrenguier
pushed a commit
that referenced
this pull request
Aug 2, 2018
romainbrenguier
pushed a commit
that referenced
this pull request
Mar 22, 2019
We should keep the struct tag type, not follow it and get the struct type
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.
No description provided.