TG-58 New PR for Complete rework of string solver to avoid using infinite arrays #1539
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
Using model of char array functions in tests. Also correct java_if test description file. Remove java_object_allocation test, this should be replaced by unit tests. Removing java_append_char test duplicate of the one in string-smoke-test. Including models of char array functions for some string regression tests.
Rebase corrections in string_refinement (cast moved to another file)
initialization This will be used to let the string solver now about any correspondance between pointers and arrays.
This add a new function for initialization of nondeterministic strings. Refactor max_value to use (un)signedbv_typet largest. max_value was assuming 32 bits which may not always be the case.
This has a similar interface to union_find but also allows to replace expressions. It will be used in the string solver instead of a simple replace_mapt.
This devides string_exprt into two types:
* refined_string_exprt which is used in the preprocessing to pass
arguments to string primitives
* array_string_exprt which is used by the string solver
The solver therefore now works with arrays in the back end.
This commit contains a lot of renaming from string_exprt to one of the
two new expression type, and the solver procedure is adapted for
working on finite arrays.
Also remove useless include and debug output.
This could potentially be used to signal exceptions. For primitives whose result is a string given as first parameter, the returned value should have an integer type has given by get_return_code_type().
Remove declaration of unimplemented function. Correcting typo. Update documentation of convert_exprt_to_string_exprt.
Structure using GIVEN WHEN THEN
Style: correct indentation in string preprocess Documentation: decl_string_expr, make_nondet_infinite_char_array, pointer to array association, array to length association, string expr of function, string_expr_of_function, code_assign_java_string_to_string_expr
Constant arrays index set are initialized with the full list of indexes so there is no need to add things to it.
not_contains_constraints are present In the case of not_contains_constraints, the fixpoint of the index set may not be enough to ensure the model is correct. Therefore we allow continuing even if the index set does not grow, progress is ensured in that case by the addition of counter-examples.
Now returns optional with no value if the model of the array is incomplete instead of an empty string. This way the result of get is more coherent: we return the same expression as the input if the model cannot be found, instead of an empty string.
not_contains_constraints more uniform
This is in the case where super_get does not anything about the array we give it. This is necessary so that the string solver returns an array of the correct size, if the size is the only thing we know about the string. Add warning message in the case where the symbol is unknown to super_get
This is done by looking at which arrays were associted to pointers in the generator.
We use this in get to distinguish between strings and arrays of characters
This removes unused functions, declaration of unimplemented function, unused constants and unused fields.
In initialisation of string objects, this prevents the created objects from getting out of scope.
The function what was there before was not correct. It was calling cprover_string_copy which is deprecated.
The check for a specific object number was removed so this does not check what we want anyway. It is difficult to make it check the original intended behaviour using only regular expressions.
This more accurately describe what this object is.
Add nolint marker on line with lambdas, which are formatted by clang in a way that is not compatible with cpp-lint.
romainbrenguier
requested review from
kroening,
martin-cs,
mgudemann,
peterschrammel,
smowton and
tautschnig
as code owners
romainbrenguier
changed the title
smowton
approved these changes
Oct 31, 2017
peterschrammel
approved these changes
Oct 31, 2017
smowton
pushed a commit
to smowton/cbmc
that referenced
this pull request
May 9, 2018
4820601 Merge remote-tracking branch 'diffblue/develop' into merge-dev-to-ss 278f309 Merge pull request diffblue#1526 from reuk/reuk/fixup-unified-diff 69ba9e7 Merge pull request diffblue#1546 from smowton/smowton/feature/expose_tarjan 05dc65c Use lower-case characters to start error messages 8d0b23b Change asserts to invariants a7afc6c Return from get_diff by value 6833af6 Fix formatting 4555d9f Remove unused parameter e32c6c5 Make instructions_equal static f815cc0 Move instructions_equal definition 11c9acc Add getter for data member 8c35211 Make data member private f54db47 Rename differences map data member b67d6e8 Merge pull request diffblue#1543 from chrisr-diffblue/cleanup/add-java-array-element-type-helper c9241cd Make generic Tarjan's algorithm publically available ebabdb9 Merge pull request diffblue#1542 from smowton/smowton/cleanup/sharing-node-assertion a523d6f Add a helper function for accessing the element type of a Java array type d8e8a68 Use INVARIANT rather than assert for sharing-node assertions 64d5dd2 Merge pull request diffblue#1538 from smowton/smowton/cleanup/remove-returns-asserts-to-invariants fca7c04 Merge pull request diffblue#1537 from smowton/smowton/cleanup/sharing-node-test-to-catch e35372a Merge pull request diffblue#1539 from romainbrenguier/bugfix/char-array-in-java-strings#TG-58#newpr 4d011b5 Merge pull request diffblue#1541 from owen-jones-diffblue/replace-unsigned-with-number-type b2a4e39 Merge pull request diffblue#1540 from owen-jones-diffblue/rename-detach 2f6ceed Replace unsigned with appropriate type 938ab2b Replace 'detatch' with 'detach' c219663 Convert sharing-node test to run under Catch dec5ddf Remove-returns: asserts -> invariants 3b1f485 Merge pull request diffblue#1535 from andreast271/ignore-eclipse-vs-dirs 6cea5aa Ignore files and directories created by Eclipse and Visual Studio aa94fe8 Style: add nolint marker on lines formated by clang ee4a887 Merge pull request diffblue#1458 from LAJW/perl-platform 4da5a94 Add templating functionality to the perl script 21b2641 Move make_function_application to java_utils 5196e40 Merge pull request diffblue#884 from nmanthey/ipasir-no-ci 3ee3b25 Refactor: remove m_ prefix from member fields 539ff9f Refactoring: simplify and remove unused expression 5a0d6b4 Rename first_index in array_expr d03b8cc Remove regression test that is not checking anything 90c8495 Improve tests for StringBuilder.append([C) 232617c Add code for String constructor from array a2d7811 Use dynamic object instead of tmp_object in init daef30f Splitting is_string and init_string parts of init ad65847 Style: rename i in chr_int to avoid clash e59349f Remove redundant check in from_int_with_radix 038b476 Allow index for argument of associate array to pointer 73d51fc Remove insert_long which duplicates insert_int bb22700 Cleanup unused fields of constraint generator 2355e8e Fix set of created strings in generator and use it 26e895d Distinguish strings and char arrays in get 4b8a421 Make get_array return array of unknown expr ca8213f Simplify not_contains constraints before negation 92897f7 Style fixes in string_constraint_generator.h 145364c String refinement: Improve debug information 3e5b3f1 Minor code improvements in string refinement 3d5465e Minor code improvements in generator_insert 86e1444 Refactoring: use begin()+3 instead of 3 times next fef1c5f Correction in debug model 28590fe Correction in constraints for concat 6861b9d Documentation fixes in stirng constraint generator c410159 Regression: StringBuilder append with int argument e6700ff Minor improvements in bytecode typecheck 61f0e1b Making check_axioms for string_constraints and not_contains_constraints more uniform f2122c6 Correct signature of convert_exprt_to_string_exprt_unit_test 9edbb90 [string-refinement] Change get_array to return optional 86e4782 [string-refinement] Allow index set saturation if not_contains_constraints are present c9c612d [string-refinement] Do not update index set of constant arrays b88fe35 [string-refinement] Check for char type 1a22916 [string-refinement] Display debug info for index-set 982a5fc Style and documentation fixes in preprocessing a83daa7 Minor indentation, naming and const-fixes 15fd1b4 Fix typos in strings and comments of string solver 26ae9a9 Unit test improve convert exprt to string exprt b76b116 Minor improvements in string preprocessing 05a6b09 [constraint-generator] Removing declarations of unimplemented functions 302f92e Make string primitives return return_code_type b80d063 Doxygen corrections 369dd62 Unit test: adapte instantiate_nc for new signature dcae158 [string-refinement] Removing unused functions b6b2669 Style changes in string_constraint_generator_testing edf7057 Complete string solver rework 9ea2eda Unit tests for union_find_replacet 4adf5d0 New class for union find replace 1d112d5 Java object factory for nondet strings 0ae71b0 [string-preprocessing] New functions for calling string primitives in initialization e89f5e4 [string-preprocess] Refactor java_types_matches_tag 2505982 Extra preconditions in string solver 6378400 Style improvements in the string solver 36d6e6d [util/irep_ids] Additional identifiers fa45b34 Regression test mprovement for if expressions 76cd14d Unit test for gen_nondet_string_init c71c64b Regression: include model for string to char array c3d527c compiling: add IPASIR notes for Linux 900a0fc tests: do not match iterations line 751208d tests: drop number of iterations 12a6917 build: add ipasir solver support 14419d2 solvers: add ipasir driver 8aa89be build: introduce LIBSOLVER environment variable df45bdb Merge pull request diffblue#1524 from reuk/reuk/fix-linter 4b39446 Merge pull request diffblue#1518 from diffblue/taint-for-C 25e18c0 Merge pull request diffblue#1529 from smowton/smowton/fix/float128 3cf67f7 Merge pull request diffblue#1531 from reuk/reuk/expr-cast-fixup 2169a39 Add _Float128 spelling for 128-bit float type a3cf849 Merge pull request diffblue#1530 from martin-cs/feature/document-return-codes 188f263 Enable casting from derived types to other derived types 3dd7f6c first regression tests 29bc3b8 custom_bitvector_domain: allow objects that are members ab7270e check taint on sinks _before_ the call 6daa8bd Merge pull request diffblue#1528 from tautschnig/shl-overflow 2df2abb Change a few erronious return codes so that they are more internally consistent. cf96cef Minor changes to erronious exit behaviour. c8dfd48 Replace constants exit codes with meaningfully named macros. 961d33a Replace literal constants in returns / exits with their symbolic names. e74b442 Named, possibly even descriptive macros for the exit codes that are used. 1e3712c Shifts of non-integers and left shifts of negative integers are undefined 6bb3872 Check for overflow on left shift of signed ints f9af374 Merge pull request diffblue#1512 from thk123/bugfix/TG-1058/crash-inner-class-generic-class bd2e9c2 Merge pull request diffblue#1522 from reuk/reuk/clang-format-plain-diff f892f4a Added tests for bracket matcher to include different types of brackets 3beab8b Fixed error in find_closing_delimiter 0b3058f Tightened up exception for unknown handling 9f87a80 Assertion on unmatched ; for parsing reference types 5922826 Adding doubly nested generic tests 4a62b07 Simplifying method names for unit test ee39620 Extended tests to verify the generic information is being parsed correctly. 465a473 Parse multiple nested generic type informations b8d43ab Pulled out method for parsing a list of multiple types 2a5c280 Correctly parse multiple input parameters for functions 35d974f Add method for finding the matching ; corresponding to a reference L e1621a3 Hide methods relating to getting multiple type variables for specific param e952708 Adding tests for parsing methods of generic classes with inner classes 958c006 Adding utilities for code_type structures 72a041b Don't crash when found an invalid reference type ed545cb Refactored out the code for erasing generic types effc1b2 Parse the whole class when generics are present d23a0cc Added function for getting the full class name of a type 34c185e Unit test reproducing the bug described in TG-1058 5b92002 Adding utilities for checking types in unit tests a00edd3 Disable dowhile brace check by default d38b5d8 Disable colour in travis diff display git-subtree-dir: cbmc git-subtree-split: 4820601
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 is a replacement for #1420 which takes too long to load because of the 300+ conversations.