Corrections to the string solver #574
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
This avoid dependencies between goto-programs and solver. We also removed function is_unrefined_string_type which should not be needed in the string solver. Removed also mention of java string types and unrefined types in the solver. These mentions should not be necessary, since we are not supposed to do anything java specific. The solver should only have to deal with refined string types and possibly char arrays.
This is a more appropriate location for this module since it's used both in the preprocessing of goto-programs and the string solver.
Refined string type should be used instead as we are trying to be language independent.
The class_name is now passed as argument so that we can reuse this function for StringBuilder and other "String-like" classes.
Better detection of string-like types and handling of char arrays Changing the way we deal with string initialisation from array Factorized part of type recognition and added StringBuilder and CharSequence to the list of java classes that should be considered as string. Changed the way we deal with StringBuilders: instead of having a map we add an assignment to the instructions. We also detect char arrays and handle them better. We now use substring and copy functions for initialisation from char array since the argument are always transformed into refined strings. For each string returned by a string function we also add into the java_string_to_cprover_string map a string_exprt. Corrected detection of typecast in make_cprover_string_assign Ensuring refined_string arguments of function applications are string_exprt Correct string_refine_preprocesst constructor. Order of initialisation is now the same as the order of declaration. This was picked up by g++ and clang. Added signatures for some StringBuilder functions. Removed map java_to_cprover_string and adapt signature for side effects. The usage of a map is not correct since strings can be modified by side effects. Signature is necessary for StringBuilders to be assigned in the right way with methods with side effects. Assign all string_exprt to refined string symbols in preprocessing. This makes it then easier to debug and to find witnesses for counter examples in the solver. Make signatures take priority over actual type and add signature for intern.
The code adding lemmas to the solver for each equality has been
completely remastered. It has been simplified and should
now cover all foreseable cases.
Add overflow constraints on sums for string solver
When creating sum expressions during string
refinement, e.g. when
adding string lengths, we shall add axioms to prevent the solver
from finding values that actually come from an integer
overflow.
Therefore, we introduce a new method plus_exprt_with_overflow_check()
that wraps around plus_exprt and generates the
relevant axioms.
Cache function applications
Cache converted function applications to avoid re-generating the axioms
if it has already been done for a given function application.
This seems to happen for function applications that are in an
assertion, and thus are treated separately by convert_bitvector.
Remove string_refinement::convert_symbol: the behaviour of
this function was to convert java strings to strings of
symbols. In hindsight, this was not a good idea, as we still refer
to the actual java string fields in some cases, e.g. to read its
length.
Replace add_axioms_for_string_expr
In all add_axioms_... methods, we replace all calls to
add_axioms_for_string_expr by the newly created function
get_string_expr, which simply returns a
string_exprt when we give it
an refined expr (such as a string_exprt or a symbol).
Update doc in add_axioms_for_index_string
Simplify constraint for is_prefix: apply distribution
law and update (and refactor) documentation.
Remove set_string_symbol_equal_to_expr()
Removed mentions of java string type in the string solver
Removing mentions of is_c_string_type
To use the string solver in C, we
should use a struct type with tag
__CPROVER_refined_string_type
Keep non-string axioms in a list
Instead of giving axioms to
super::boolbv_set_equality_to_true, which
may contain un-substituted symbols, we keep them in a list and
substitute them in dec_solve() before giving them to the
function.
Cleaning the add_axioms_for_string_expr method and renamed it
to add_axioms_for_refined_string to signify that it should
only be called on expression of type refined string.
An assertion was added at the beginning to ensure that.
Better get_array and string_of_array functions.
Cleaned the implementation of get_array and factorized
part of it.
Made string_of_array directly take a array_exprt, which can be
obtained from get_array.
Improved string_of_array for non printable characters
Resolve symbol to char arrays in non-string axioms.
We introduce a mapping that expresses the
maximal traversal of symbols
of char array type.
We use that map to, either obtain a char array from a symbol,
either get a unique symbol the aliases equivalence class.
This map is used to replace all symbols of char array type in
the axioms that are added using the parent method:
supert::boolbv_set_equality_to_true.
Defining several intermediary functions for
check_axioms and cleaning.
Check axioms is quite complicated so we splitted it in several
parts.
Avoid using same universal variable name in string comparison function.
Corrected test in index_of as characters could be signed
Corrected return type retrieval in
from_float functions.
The return type should be given as argument of the helper function
add_axioms_from_float.
Fixed type of contains in constraint generation
Introduce string_refinementt::set_to.
We now override the set_to() method
instead of set_equality_to_true().
This solves a problem where many lemmas were being dropped.
Handle array_of in set_char_array_equality.
Java assignments such as char[] str=new char[10]
involves assigning
the char array to 0, which is done using the array_of operator.
This operator is now handled when found on the rhs of a char
array assignment.
Optimized string hash code and intern functions to only
look at seen strings.
We only compare the argument to the strings on which hash_code
(resp. intern) was already called.
Add missing override keyword in declarations
Integrate strings into symbol resolution.
We now use for strings the mechanism that was
made for resolving symbols
to char arrays.
As a result, the symbol_to_string map has been removed.
We introduce an unresolved_symbol map to associate symbols
to string
expressions that were introduced during constraint generation.
Preventing return of nil exprt in sum_over_map
Enforce -1 for witnesses when strings are unequal.
This makes it easier to see when models for string
have different length.
Make more robust. Changes only applied to java tests.
In certain cases, omitting the argument of the main class makes cbmc crash. This test checks that this does not happen.
Was taken out of another test.
Correct a bad array access that caused a segmentation fault on the java_delete test.
romainbrenguier
force-pushed
the
string-refine-corrections
branch
2 times, most recently
from
1d50604 to
d987fd8
Compare
The option to concretize makes sure that the model that we get in the end is correct. Overiding the get method is necessary to get the actual valuation of string gotten by the solver. This two additions makes the trace generation for program with strings more likely to be actual traces of the program.
romainbrenguier
force-pushed
the
string-refine-corrections
branch
from
d987fd8 to
db85dc5
Compare
|
This PR is replaced by #646 which contains all these changes and some additional corrections. |
NathanJPhillips
pushed a commit
to NathanJPhillips/cbmc
that referenced
this pull request
Sep 6, 2018
…applied_rules SEC-658: Propagation of descriptions of rule applications to allow pretty error-traces browsing.
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.
The code adding lemmas to the solver for each equation has been
completely remastered. It has been simplified and should
now cover all foreseeable cases.
We add constraints on sums for avoiding overflows in the string solver.
This depends on #378 and #559.
This PR has been replaced by #646