[TG-2138] Stop adding default axioms in string solver #2052

romainbrenguier · 2018-04-13T06:43:08Z

This PR replaces #1873

The solver is currently adding default axioms on all the strings based on string-max-length.
This can be a problem if for instance an Object can be cast to String, because the axiom on the string also apply to the original object, independently of whether the branch on which it is cast is reached or not.
This PR removes these axioms.

LAJW

Looks good from the code quality standpoint. Logic-wise - someone should take a second look.

LAJW · 2018-04-13T10:05:33Z

src/solvers/refinement/string_constraint_generator_main.cpp

 array_string_exprt string_constraint_generatort::char_array_of_pointer(
  const exprt &pointer,
  const exprt &length)
 {
  const array_string_exprt array = array_pool.find(pointer, length);
-  add_default_axioms(array);
+  created_strings.insert(array);
  return array;


This could be written as:

return *created_strings.insert(array_pool.find(pointer, length)).first;

insert and emplace return a pair containing an iterator to the newly inserted element and a boolean, which is set to true if the element was newly inserted. That way you can avoid creating a temporary and return a reference to the newly created element.

(comment on commit message) creted -> created

LAJW · 2018-04-13T10:09:59Z

regression/jbmc-strings/max-length/test4.desc

+--
+The solver may give an ERROR because the value of string-max-length is too
+small to give an answer about the assertion.
+So we just check that the answer is not success.


Missing newline ;/

LAJW · 2018-04-13T10:12:48Z

regression/jbmc-strings/long_string/Test.java

-        if(u.length() < 67_108_864)
+        // 67_108_864 corresponds to the maximum length for which the solver
+        // will concretize the string.
+        if(u.length() <= 67_108_864)


Comment is helpful, but don't we have a file with constants?

This is a java file

allredj

That looks fine to me. As mentioned in the comments, please document the --string-max-length option as deprecated.

allredj · 2018-04-13T09:25:21Z

src/java_bytecode/java_bytecode_language.cpp

@@ -55,6 +55,10 @@ void java_bytecode_languaget::get_language_options(const cmdlinet &cmd)
  if(cmd.isset("string-max-input-length"))
    object_factory_parameters.max_nondet_string_length=
      std::stoi(cmd.get_value("string-max-input-length"));
+  else if(cmd.isset("string-max-length"))
+    object_factory_parameters.max_nondet_string_length =
+      std::stoi(cmd.get_value("string-max-length"));


That should be specified in the help string.

Also, as discussed, we should deprecate that option. We can then move to remove it from platform.

peterschrammel · 2018-04-23T08:19:16Z

src/solvers/refinement/string_constraint_generator_main.cpp

 array_string_exprt string_constraint_generatort::char_array_of_pointer(
  const exprt &pointer,
  const exprt &length)
 {
  const array_string_exprt array = array_pool.find(pointer, length);
-  add_default_axioms(array);
+  created_strings.insert(array);
  return array;


(comment on commit message) creted -> created

peterschrammel · 2018-04-23T08:22:52Z

src/solvers/refinement/string_refinement.cpp

-  for(exprt lemma : generator.get_lemmas())
-  {
-    symbol_resolve.replace_expr(lemma);
+  for(const exprt &lemma : generator.get_lemmas())


(comment on commit message) unecessary -> unnecessary

peterschrammel · 2018-04-23T08:23:31Z

src/java_bytecode/java_string_library_preprocess.cpp

@@ -877,7 +877,7 @@ codet java_string_library_preprocesst::code_assign_string_expr_to_java_string(
 /// \param symbol_table: symbol table
 /// \param [out] code: code block that gets appended the following code:
 /// ~~~~~~~~~~~~~~~~~~~~~~
-/// lhs.length=rhs->length
+/// lhs.length = rhs==null ? 0 : rhs->length


(comment on commit message) string_exrpt -> string_exprt

peterschrammel · 2018-04-23T08:26:52Z

src/solvers/refinement/string_refinement.cpp

+      std::string(
+        "apart from symbols, array valuations can be interpreted as "
+        "sparse arrays, id: ") +
+        array.id().c_str());


Use id2string(array.id())

peterschrammel · 2018-04-23T08:27:30Z

src/solvers/refinement/string_refinement.cpp

-  UNREACHABLE;
+  INVARIANT(
+    array.is_nil() || array.id() == ID_symbol,
+    "in case the array is unknown, it should be a symbol or nil");


Would be good to output the actual id here as well.

peterschrammel · 2018-04-23T08:28:47Z

regression/jbmc-strings/long_string/test_abort.desc

-This tests should abort, because concretizing a string of the required
-length may take to much memory.
+This tests that the object does not appear in the trace, because concretizing
+a string of the required length may take to much memory.


-> too much memory

To make the solver abort the length has to be strictly greater than 2^26.

This is already done in add_lemma.

We use this counter examples in the string solver but the formula given there don't use arrays so it is enough to use boolbvt.

Having input string longer than string-max-length does not make sense as the solver will not know how to analyse them. So when string-max-input-length is not specified we can use string-max-length instead.

Instead of aborting the program when the string is too long, we consider this happened because of some invalid object, and return nil as a model of the array. Access to this invalid object is prevented by other part of the code and should not occur in the trace.

nil_exprt happens when the underlying solver has no formula talking about the array

Although we should not reach this code if rhs is null, the association `pointer -> length` is added to the solver anyway, so we have to make sure the length of the string_exprt is set to something reasonable.

These default axioms where too strict and where applied even for strings that may never be created in the actual program. This could for instance lead to problematic contradiction for a Java object which could be casted either to a string or an int: the axiom added there would apply both on the string and on the integer.

In constraint generator, this was used for adding default axioms but is no longer used.

This adds an int greater than string-max-length in a generic array. This is to check that TG-2138 is fixed. Before the issue was solved setting the array to 101 was in contradiction with default axioms added by the string solver.

These tests show how the result of the solver can depend on the string-max-input-length and string-max-length parameters.

20e7bca Merge pull request diffblue#2179 from cesaro/java-concurrency-support3 25e5820 Java concurrency regression tests bc539b5 Adds support for concurrency in java programs 46849e9 Adding concurrency related methods to CProver.java c817486 Merge pull request diffblue#2171 from thomasspriggs/json_tweaks f3670e3 Expose `begin` and `end` methods of underlying `std::vector` in `json_arrayt`. 402bc56 Clang format updates. 2907ba9 Allow constructon of `json_stringt` from `irep_idt`. ce674b5 Update constructor of `jsont` based on the copy and move idiom. 28117d2 Expose `emplace_back` method of underlying `std::vector` in `json_arrayt`. a589a56 Supply `value_type` typedef in `json_arrayt` for STL algorithm usage. 1d0cd01 Merge pull request diffblue#2175 from diffblue/extract-goto-functiont 76d202a use goto_function.h when only goto_functiont is used b9cd297 split out goto_functiont from goto_functions.h into separate file 784b6dd Merge pull request diffblue#2119 from svorenova/gs_tg1121_regression 1b6a939 Merge pull request diffblue#2169 from sonodtt/patch-1 faaacec Add dashboard webhooks to travis 7b0673e Merge pull request diffblue#2154 from diffblue/jar-file-cleanup d069719 Merge pull request diffblue#1915 from karkhaz/kk-abstract-paths-worklist aac16d5 Merge pull request diffblue#2159 from peterschrammel/clean-up-specc d413dd8 Merge pull request diffblue#2123 from smowton/smowton/java-object-factory-zero-initializer 995a548 Merge pull request diffblue#2164 from tautschnig/cleanup-mp-arith a4d1891 Merge pull request diffblue#2160 from diffblue/fix-java-constructor-pretty-name b9db37d Merge pull request diffblue#2163 from tautschnig/fix-test 6b064b3 pretty name of constructors now uses empty declarator b008bf3 add signature to method pretty names a9bb35c strip package name from base_name of Java class symbols 7711933 Merge pull request diffblue#2162 from tautschnig/fix-format 7d91638 Merge pull request diffblue#2148 from diffblue/remove-fixedbv-option 7e09d5f Fix duplicate output of id in format() 033f4c5 Remove unnecessary (and inconsistent) return statement 90d59d8 Remove unused global constant 29763da Fix misleading comments: the required variant of numeric_cast does not exist a2260bd remove the --fixedbv command-line option 78901ef fix in rounder in fixed-point arithmetic class 8414886 Remove SpecC support 88bbe32 Clean up references to php frontend 3f52c59 Clean up commented include 01685b6 Clean up references to SpecC frontend 916eb1f Unit tests for path exploration strategies 88db26f Merge pull request diffblue#2155 from tautschnig/mode-fixes 2fb3d2f Add missing mode 85aba52 Make new LIFO path exploration the default feef069 Doxygen uses C++ parser for .h files 17951c8 Add path strategy chooser class 685937a Path exploration pushes both successors onto queue 2a86fb4 Bugfix: always print path exploration resume point e823538 Symex paths saved onto abstract data structure bbd4253 signal errors while getting file from JAR using optional 48f1af3 Merge pull request diffblue#2145 from cesaro/concurrency-support-for-clinit 8db6b22 Merge pull request diffblue#2139 from romainbrenguier/bugfix/annotations-as-comments 94bbbba Added new cmd option to jbmc, 'java-threading' 48914be Modifies the instrumented clinit_wrapper function ce9f046 Merge pull request diffblue#2146 from diffblue/extra-float-types 46267b5 Merge pull request diffblue#2153 from diffblue/elaborate-format_expr da940a9 Test for assignement of annotated field 9d94bf7 Make annotations comments in irep_idt 52e9737 new gcc floating-point type identifiers, Fixes: diffblue#2151 c6cbf7c Merge pull request diffblue#2147 from diffblue/fix-tempdir-buffer-overflow 957881c format now prints type expressions and the values of named sub-ireps 9609a52 simplify use of get_temporary_directory 5907f68 fix potential non-zero termination of a string buffer 41d7a45 Merge pull request diffblue#2129 from romainbrenguier/bugfix/generic_type_index 53bc892 Add invariant in java_generic_symbol_type e3f240a Use get_name in generic_type_index 4a6ae9b Add java_types unit tests to Makefile 4c5144d Unit test for generic_type_index 8f0f780 Unit test for java_generic_symbol_type 41b3a6a Move java_generic_symbol_typet definitions to cpp 0afbe0f Unit test java_type_from_string and fix doc b7c9ea1 Test for abstract class with two generic arguments c141611 Fix generic_type_index 8127d4d Merge pull request diffblue#2141 from romainbrenguier/bugfix/goto-convert-mode 4948b70 Merge pull request diffblue#1712 from karkhaz/kk-flush-all e0bc5fd Merge pull request diffblue#2143 from diffblue/missing-algorithm-include fbed57e Add precondition ensuring mode is not empty 2ef91e7 Make mode an argument of goto-convert functions 2b4cd76 missing #include <algorithm> for std::find_if_not 7d11e85 Zero-initialize object factory structs 392c765 cleanup the includes in src/java_bytecode 1050637 fix a comment c57439e missing const for parameter 227e83d Adding regression tests for multi-dimensional arrays b8ffa5e Merge pull request diffblue#2135 from diffblue/solver-cleanout 0dc35fd Merge pull request diffblue#2136 from diffblue/unwind_module_cleanout f6a92cc remove bmc_constraints a2d9822 remove OpenSMT 218dc31 remove support for SMT1 e8aaf09 remove unused includes b0f7476 remove do_unwind_module hook 4d75d3d Merge branch 'develop' of github.com:diffblue/cbmc into develop 60c03b3 whitespace fix 3ea32fe Merge pull request diffblue#2134 from peterschrammel/invalid-symbol-mode b2a58c8 Assign mode to invalid objects e4230c6 Merge pull request diffblue#2130 from romainbrenguier/bugfix/if-expr-mode c6beb68 Merge pull request diffblue#2128 from tautschnig/include-cleanup 973b309 Merge pull request diffblue#2073 from tautschnig/reset-namespace a6a825a Remove unused includes b04122e Move definition of base_type_eqt to .cpp 104bc56 Use pointer_offset_bits instead of locally hacking up what it does anyway 99755fe Move asserts to invariants (and provide suitable includes) 3af3d72 Do not unnecessarily use C string functions 3c697da Add test where tmp_if_expr is introduced 746e337 Set mode of if_exprt introduced in preprocessing 73e0c0f Use C++ streams instead of C-style snprintf d351a5d Use a single global INITIALIZE_FUNCTION macro instead of __CPROVER_initialize 9c03ca3 Use iosfwd instead of ostream where possible 6b8583d Merge pull request diffblue#2100 from tautschnig/string-table-cleanup 75caefa Merge pull request diffblue#2116 from peterschrammel/java-new-pass 6c90b35 Merge pull request diffblue#2052 from romainbrenguier/bugfix/default-axioms2#TG-2138 53dfa0a Merge pull request diffblue#2120 from diffblue/optional_optnr 8f7d9f0 use optional<size_t> instead of -1 in cmdlinet a61d03f Remove java_bytecode deps from Makefiles ce9f1fc Use remove_java_new 10d0042 more files to ignore 95ea29a Merge pull request diffblue#2115 from peterschrammel/language-mode-utils ce11613 Factor out java new removal into separate pass baa15f5 Add Makefile dependency for smt2_solver bacfa27 Merge pull request diffblue#2114 from tautschnig/type-renaming 2bdaafc Add more doxygen to language.h and mode.h 74c2c3d Utility functions to get mode and language b934aaf symex_dynamic::dynamic_object_size* are constants ef83f93 array_size symbols: set mode and avoid redundant settings 8b20ebb Merge pull request diffblue#2112 from diffblue/address_of_byte_extract 66aa851 Merge pull request diffblue#2109 from LAJW/lajw/free-lambda-from-cpplint-oppression 7339638 Merge pull request diffblue#2111 from peterschrammel/bugfix/missing-java-modes 18cab61 Rephrase and justify curly brace alignment exceptions 6670703 Added an extension point for irep ids 38782bd Move enum idt to the single translation unit that actually requires it e657da8 Fix Doxygen syntax f79b453 Check that the string table does not include unused entries 61ca5df Remove unused entries from the string table b2e4ca0 Use existing irep_idts instead of strings 2b819e6 Remove unused symbolt::{to,from}_irep 0b82ee2 allow address_of of byte_extract expressions 7747442 Associate dynamic objects with respective language mode 6438ee7 Bugfix: use proper language registration in unit tests c274c15 Set mode in goto_convert auxiliary symbols 9a896f9 Replace asserts by invariants 78191ee Remove NOLINTs for lambdas. 692c4f3 Remove brace checking from cpplint d344dd9 Update coding standard b59a453 Move MAX_CONCRETE_STRING_SIZE definition to magic 05b924c Deprecate string-max-length option 132a26b Add tests showing the effect on string-max-length 0e8a863 Add test for generics array and strings b83182f Get rid of string_max_length field d726577 Make char_array_of_pointer return a reference 2154047 Get rid of default axioms for strings 1d4f26c Assign 0 to string length for null Java String ff25fe2 Weaken invariant for nil exprt as model of array 56e7b37 Make get_array return nil for long strings 5fde05a Use string-max-length as default max input-length b0c6528 Use boolbvt for getting counter examples 5b3a1a4 Remove unnecessary replace_expr a630bb7 Correct bound in test with long string e4cf694 Bugfix: Java symbol types must have mode ID_java e158bb4 Bugfix: Java array symbols must have mode ID_java d475abc Reset namespace after symbolic execution 1ef0f41 Add --flush option to flush all output git-subtree-dir: cbmc git-subtree-split: 20e7bca

romainbrenguier requested review from cesaro, kroening, martin-cs, mgudemann, peterschrammel, smowton, tautschnig and thk123 as code owners April 13, 2018 06:43

romainbrenguier requested a review from LAJW April 13, 2018 06:43

romainbrenguier mentioned this pull request Apr 13, 2018

[TG-2138] Remove default axioms for strings in string solver #1873

Closed

romainbrenguier force-pushed the bugfix/default-axioms2#TG-2138 branch 2 times, most recently from 8be0b3d to ebd7f62 Compare April 13, 2018 09:02

LAJW approved these changes Apr 13, 2018

View reviewed changes

romainbrenguier force-pushed the bugfix/default-axioms2#TG-2138 branch from ebd7f62 to 3c9a81d Compare April 13, 2018 10:21

allredj approved these changes Apr 13, 2018

View reviewed changes

romainbrenguier force-pushed the bugfix/default-axioms2#TG-2138 branch 3 times, most recently from 10b0cb1 to ce43b3e Compare April 18, 2018 07:58

peterschrammel reviewed Apr 23, 2018

View reviewed changes

romainbrenguier added 11 commits April 23, 2018 10:27

Correct bound in test with long string

a630bb7

To make the solver abort the length has to be strictly greater than 2^26.

Remove unnecessary replace_expr

5b3a1a4

This is already done in add_lemma.

Use boolbvt for getting counter examples

b0c6528

We use this counter examples in the string solver but the formula given there don't use arrays so it is enough to use boolbvt.

Use string-max-length as default max input-length

5fde05a

Having input string longer than string-max-length does not make sense as the solver will not know how to analyse them. So when string-max-input-length is not specified we can use string-max-length instead.

Weaken invariant for nil exprt as model of array

ff25fe2

nil_exprt happens when the underlying solver has no formula talking about the array

Assign 0 to string length for null Java String

1d4f26c

Although we should not reach this code if rhs is null, the association `pointer -> length` is added to the solver anyway, so we have to make sure the length of the string_exprt is set to something reasonable.

Make char_array_of_pointer return a reference

d726577

Get rid of string_max_length field

b83182f

In constraint generator, this was used for adding default axioms but is no longer used.

Add test for generics array and strings

0e8a863

This adds an int greater than string-max-length in a generic array. This is to check that TG-2138 is fixed. Before the issue was solved setting the array to 101 was in contradiction with default axioms added by the string solver.

romainbrenguier added 3 commits April 23, 2018 10:53

Add tests showing the effect on string-max-length

132a26b

These tests show how the result of the solver can depend on the string-max-input-length and string-max-length parameters.

Deprecate string-max-length option

05b924c

Move MAX_CONCRETE_STRING_SIZE definition to magic

b59a453

romainbrenguier force-pushed the bugfix/default-axioms2#TG-2138 branch from ce43b3e to b59a453 Compare April 23, 2018 09:53

peterschrammel approved these changes Apr 26, 2018

View reviewed changes

kroening merged commit 6c90b35 into diffblue:develop Apr 26, 2018

peterschrammel mentioned this pull request Apr 27, 2018

Set mode of if_exprt introduced in preprocessing #2130

Merged

Provide feedback

Saved searches

Use saved searches to filter your results more quickly

[TG-2138] Stop adding default axioms in string solver #2052

[TG-2138] Stop adding default axioms in string solver #2052

romainbrenguier commented Apr 13, 2018

LAJW left a comment

LAJW Apr 13, 2018

peterschrammel Apr 23, 2018

LAJW Apr 13, 2018

LAJW Apr 13, 2018

romainbrenguier Apr 16, 2018

allredj left a comment

allredj Apr 13, 2018

allredj Apr 13, 2018

peterschrammel Apr 23, 2018

peterschrammel Apr 23, 2018

peterschrammel Apr 23, 2018

peterschrammel Apr 23, 2018

peterschrammel Apr 23, 2018

peterschrammel Apr 23, 2018

[TG-2138] Stop adding default axioms in string solver #2052

[TG-2138] Stop adding default axioms in string solver #2052

Conversation

romainbrenguier commented Apr 13, 2018

LAJW left a comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

allredj left a comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment