Test gen support string additional options#695
Test gen support string additional options#695romainbrenguier wants to merge 17 commits intodiffblue:test-gen-supportfrom
Conversation
There was a problem hiding this comment.
It seems that making substitute_* do an in-place substitution could simplify the code.
for(auto &op : expr.operands())
substitute_array_access(op);
There was a problem hiding this comment.
I've made substitute_array_access in-place 14a1138
But I've let substitute_array_with_expr as it is because I think it is simpler in the current state.
There was a problem hiding this comment.
This loop would be simpler if you considered the first element as default case of the ite chain. Is there a formula readability argument against this?
There was a problem hiding this comment.
The readability would be fine with first element as default, but I don't see why it would make the loop simpler. It would just shift the bounds by 1?
There was a problem hiding this comment.
What is the meaning of -1 ?
There was a problem hiding this comment.
I'd prefer using an unsigned integer and std::numeric_limits::max() as default upper limit. What is "no limit" supposed to mean in your case? What is the relation to MAX_CONCRETE_STRING_SIZE?
There was a problem hiding this comment.
auto &it (several instances)
src/cbmc/cbmc_parse_options.h
Outdated
There was a problem hiding this comment.
I suggest to put each option on a separate line to facilitate merging.
There was a problem hiding this comment.
Is ulong needed here? It's initialised from uint.
|
Please remove the [string-refine] prefix from commit messages. |
There was a problem hiding this comment.
Why do we need a long here?
There was a problem hiding this comment.
This is because length of string in java are 32 bits integer, while int in c++ on some systems could be 16 bits if I'm not mistaken
There was a problem hiding this comment.
Yes, minimum size of int is 16 bits. For Java, int32_t would make it independent of the system. For other languages, this might be different. Eg c++ string::max_size() tells me something close to 2^64 on my machine.
There was a problem hiding this comment.
As pointed out earlier, this loop is not nice. The mixture of long, unsigned, size_t etc is likely to cause trouble. I dig up my earlier proposal that does without indexing.
Added field in string_refinement and string_constraint_generator to bound size of strings in the program and enforce a range on the characters.
We add the options string-max-length, string-non-empty, and string-printable
This option is no longer requiered because the implementation is now language independent.
Unknown values could cause type problems if we do not force the type for them.
romainbrenguier
force-pushed
the
test-gen-support-string-additional-options
branch
from
5066dab to
6898cca
Compare
|
Superseded by #738 |
3 participants
This adds the option --string-max-length to the string solver, this constrains all the strings to be smaller than the maximal length. This shouldn't affect much the performance of the decision procedure but may be necessary for obtaining concrete traces (when the --trace option is activated).
I also added the options --string-non-empty to constrain the nondet strings to have length at least 1 (to avoid obtaining counter-example that concatenates the empty string two times, which is not very interesting), and --string-printable to constrain strings to contain only characters in the range between (space, U+0020) and ~ (tilde, U+007E). making the example nicer than a sequence of null characters.
This also fixes a couple of bugs in the solver.
This corresponds to PR #652 on master