String max input length option #1235

romainbrenguier · 2017-08-12T17:46:54Z

This adds a string-max-input-length option that limits the size of input strings (the ones non-deterministically created by CPROVER_start).

cesaro · 2017-08-12T20:01:31Z

Is this ready for review or you want to have general comments on it?

romainbrenguier · 2017-08-14T08:13:24Z

@cesaro

Is this ready for review or you want to have general comments on it?

What's the difference? I guess both.

cesaro · 2017-08-14T17:21:29Z

@romainbrenguier I discussed with @peterschrammel about my proposed changes, let's discuss tomorrow.

romainbrenguier · 2017-08-18T08:10:18Z

@cesaro @peterschrammel this is based on #1241 which is why there are lots of commits, only the 3 last ones are relevant.

allredj · 2017-08-22T12:31:09Z

This needs to be rebased once #1241 is merged.

LAJW · 2017-08-22T13:06:45Z

Squashing would be useful.

LAJW · 2017-09-01T12:41:49Z

src/java_bytecode/java_object_factory.cpp

+           class_identifier=="java.lang.StringBuffer" ||
+           class_identifier=="java.lang.StringBuilder"))
+      {
+        exprt max_length=from_integer(


Add assumption where string max length cannot be greater than max value of me.type().

LAJW · 2017-09-04T12:27:29Z

Fixup, tidy and clean up completed. Re-requesting review.

allredj · 2017-09-04T13:55:16Z

regression/strings-smoke-tests/max_input_length/Test.java

+	// This prevent anything from happening if string-max-length is smaller
+	// than 40
+	String t = new String("0123456789012345678901234567890123456789");
+	if(s.length() >= 30)


Bad indent on these lines

allredj · 2017-09-04T13:56:49Z

regression/strings-smoke-tests/max_input_length/test1.desc

@@ -0,0 +1,7 @@
+CORE
+Test.class
+--refine-strings --string-max-length 45  --string-max-input-length 35


How about 31 instead of 35?

allredj · 2017-09-04T14:09:25Z

regression/strings-smoke-tests/max_input_length/Test.java

+public class Test {
+
+    public static void main(String s) {
+	// This prevent anything from happening if string-max-length is smaller


That comment is not clear about what should happen when --string-max-length is below 40. From a CBMC point of view I guess it's equivalent to unreachability. From a test-gen point of vue, it means no test will be generated for that block of code.
To check that the limit only affects a certain block, could we modify the test so that it looks like this:

public class Test { public static void main(String s, int i) { if (i==1) { String t = new String("0123456789012345678901234567890123456789"); if(s.length() >= 30) { assert false; } } else { assert false; } } }

and check that the first assertion is valid and the other one is failed?

Also prevent -> prevents.

We should also have tests for input strings that are not function parameters.

It appears that this new String(...) disables entire function, not only the block in which it is defined.

OK, then we can just clarify the comment.

allredj · 2017-09-04T14:14:59Z

src/cbmc/cbmc_parse_options.cpp

@@ -1107,10 +1111,11 @@ void cbmc_parse_optionst::help()
    " --yices                      use Yices\n"
    " --z3                         use Z3\n"
    " --refine                     use refinement procedure (experimental)\n"
-    " --refine-strings             use string refinement (experimental)\n"
+    " --refine-strings             use string refinement\n"


I would not remove the (experimental) mention, as string support is not fit for bmc verification. We've been developing it in the prospect of test generation, which is very different. What do you think?

allredj · 2017-09-04T14:25:51Z

src/java_bytecode/java_bytecode_language.h

@@ -48,6 +48,7 @@ Author: Daniel Kroening, [email protected]
  "                                  A '.*' wildcard is allowed to specify all class members\n"

 #define MAX_NONDET_ARRAY_LENGTH_DEFAULT 5
+#define MAX_NONDET_STRING_LENGTH 20


Is that the value by default when no --string-max-input-length is given?

Yes, it is. Previously it was maximum value of size_t but that exceeded maximum java static string array limit (which is around 16k characters).

It's not usual to have a limit by default in the cbmc options. This kind of option is generally meant to restrict the search space, not to extend it. For instance, if we run a bmc that never ends, then we retry with -unwind 100, knowing that we are restricting the model, and thus eliminating possible assertion failures. If omitting the --unwind option cbmc would fall back to a default unwinding value, it would be very confusing and the user might think that his program is valid although some assertion violations are accessible at higher unwindings.

I believe it should be the same reasoning in that case. What do you think?

allredj · 2017-09-04T14:28:30Z

src/java_bytecode/java_object_factory.cpp

+      if(name=="length" &&
+          (class_identifier=="java.lang.String" ||
+           class_identifier=="java.lang.StringBuffer" ||
+           class_identifier=="java.lang.StringBuilder"))


Do we also need to care about character arrays and CharSequence here?

I believe these are the only types that we are supporting at the moment, but @romainbrenguier might answer that question more thoroughly.

CharSequence is also supported but since it is abstract I didn't know if it made sense to initialize an object of that class in java_object_factory, it probably does so we could add it here.

If we're not sure whether we can have CharSequence here, we should probably add an assertion. If we do, we might also want to check that we don't have AbstractStringBuilder either.

Added invariant after those ifs preventing instantiation of said abstract types.

Can you check that this will not be violated with a Java program where a function takes a CharSequence as argument?

allredj · 2017-09-06T08:49:58Z

@romainbrenguier Could you please rebase? I would like to test something on that PR.

allredj · 2017-09-11T11:04:04Z

I can't build the HEAD of test-gen/master with that PR. I think it needs a rebase.

allredj

Looks fine aside from some formatting issues. But I'd like to test something once that PR is rebased.

allredj · 2017-09-11T11:04:27Z

src/cbmc/cbmc_parse_options.cpp

      cmdline.isset("java-max-input-array-length")
        ? std::stoul(cmdline.get_value("java-max-input-array-length"))
        : MAX_NONDET_ARRAY_LENGTH_DEFAULT;
-    const size_t max_nondet_tree_depth=
+    factory_params.max_nondet_string_length=
+        cmdline.isset("string-max-input-length")


allredj · 2017-09-11T11:06:42Z

src/java_bytecode/java_object_factory.cpp

+           class_identifier=="java.lang.StringBuilder")
+        {
+          PRECONDITION(object_factory_parameters.max_nondet_string_length <=
+                       max_value(me.type()));


Usually, we break after the first (.

allredj · 2017-09-11T11:06:56Z

src/java_bytecode/java_object_factory.cpp

+        }
+        else
+        {
+          INVARIANT(class_identifier!="java.lang.CharSequence" &&


Here too. Break after the first (.

allredj

LGTM

romainbrenguier

This looks good. The commits can be squashed.

romainbrenguier · 2017-09-18T07:45:53Z

src/java_bytecode/java_bytecode_language.h

+  size_t max_nondet_string_length=MAX_NONDET_STRING_LENGTH;
+
+  /// Maximum depth for object hierarchy on input.
+  /// Used to prevent object factoryto loop infinitely during the


romainbrenguier · 2017-09-18T07:47:14Z

src/java_bytecode/java_object_factory.cpp

@@ -760,6 +750,15 @@ symbol_exprt java_object_factoryt::gen_nondet_subtype_pointer_init(
  return new_symbol.symbol_expr();
 }

+static size_t max_value(const typet& type)


Document this function

romainbrenguier · 2017-09-18T07:51:18Z

src/java_bytecode/java_object_factory.cpp

+        {
+          PRECONDITION(
+            object_factory_parameters.max_nondet_string_length <=
+              max_value(me.type()));


Instead of a precondition here, we could just not add the assumption when this is not satisfied, as the constraint on the size will be enforced by the type anyway.
So we can replace this PRECONDITION by an if.

allredj · 2017-09-18T13:30:49Z

Could you please add a link to the test-gen PR for this?

d0d3620 Merge remote-tracking branch 'upstream/develop' into security-scanner-support 875d554 Merge branch 'develop' of github.com:diffblue/cbmc into develop 3a06eda don't rely on index expressions to be vector or arrays 6d6e1df Merge pull request diffblue#1407 from jasigal/fix/instantiate-not-contains#TG-592 8da3eef Merge pull request diffblue#1414 from antlechner/antonia/Character 0b56d97 Fix signatures for methods in java.lang.Character e4e2b10 TG-592 Implemented the correct instantiation procedure for not contains constraints ae83e4e Added install command for required projects. 0e70863 Merge pull request diffblue#1279 from NathanJPhillips/feature/expr_dynamic_cast 1e9837e Merge pull request diffblue#1405 from smowton/cleanup/remove_instanceof 7eb3c76 Merge pull request diffblue#1411 from diffblue/revert-1322-feature/java_support_generics 3b3fee3 Revert "TG-374 Feature/java support generics" 0e14431 Merge pull request diffblue#1408 from reuk/reuk/regression-filenames 2ddb0bc Simplify remove_instanceof logic b4f57ee Merge pull request diffblue#1410 from LAJW/fix-test-gen bcfb914 Remove invariant causing failure in unit test generation involving CharSequences 93149be Merge pull request diffblue#1322 from mgudemann/feature/java_support_generics c731b98 Merge pull request diffblue#1404 from LAJW/string-refinement-functional e5f5e8b Use `optionalt` for signature f68e817 Parse LocalVariabletypetable / Signature attributes use in types 585fb66 Merge pull request diffblue#1400 from reuk/reuk/enable-compile-commands da4df03 Switch from pointers to optionalt 413fc1b Automatically deduce test names from dir names 05d5a9b Address commenters' suggestions c48170e Merge pull request diffblue#192 from diffblue/smowton/feature/split_frontend_final_stage 0823f05 allow goto-cc -E 00cbad7 test for va_args 96f2d9e Added a PRECONDITION assert/invariant b8ab624 Code review fixup 775d9dd Renamed can_cast_expr c372eb3 Used typeinfo functions instead of rolling own 95f6505 Comment on types for which expr_dynamic_cast is not implemented d35710f Made validate_expr non-template de8a8d0 Implementation of expr_dynamic_cast f763691 Tidy up remove_instanceof f4df5c6 Add tests for mixed GOTO and C input 215d5bf Split the entry-point-generation phase into two parts ab347d5 Merge pull request diffblue#195 from diffblue/bugfix/missing-const_cast 73fba6e Fixed missing const_cast 751e8f5 Adhere to lintage b544a4b Fix unit test build 9b8a025 Fix get lambdas bee20f1 Remove unused add_lemma parameter d03866d static add axioms for string assings 1531f0e static debug_model f5c1b29 static get_array 7f11ccf static set_char_array_equality 229568a static Instantiate not contains 78303df Static concretize strings, lengths and results 918297c static concretize length a4c8cf5 Static index set functions e5e1ff4 static index_set functions 65ad3db Public methods made public 2eed573 Static add_axioms for strings 666c146 make static check_axioms bcd6111 Static is_axiom_sat 01b8301 static is_valid_string_constraint cfb47db Remove unused functions from string_refinement header 8e69d6d Make functions static 0cec13d Merge pull request diffblue#1360 from KPouliasis/konst_splice_call 9f9f30d fixup return value eaf97f6 Simplify remove_instanceof logic bc30987 Merge pull request diffblue#1235 from romainbrenguier/feature/string-max-input-length#948 0323ed0 Merge pull request diffblue#1349 from peterschrammel/cleanup/use-preformatted-output 621da87 Tests for new option string-max-input-length 440d19f Adding string max input length option e957025 Print results to result stream instead of status ad6484e Print XML and JSON objects on message stream 4969295 Tidy up remove_instanceof 6cb2f90 Merge pull request diffblue#1398 from diffblue/json_direct_return f365afe Merge pull request diffblue#1392 from reuk/reuk/fixup-appveyor-regressions 4a1565b Enable compile command output 523f028 Merge pull request diffblue#1368 from diffblue/use_size_t 358b435 prefer a ranged for over indexed iteration 69a8eaf use std::size_t for container indices cef7659 counters need to be size_t 2a7a0e8 the step number needs to be a size_t 9d48225 json_irept now returns ireps and jsont directly f22a864 Merge pull request diffblue#1386 from diffblue/return_directly 2b050a0 Merge pull request diffblue#1372 from diffblue/preconditions 6a509a8 goto-instrument no longer needs partial inlining by default e3f75d3 fixup coverage tests 1ff6bf2 missing include ac022e2 inlined functions are no longer ignored when doing coverage 4cb72b3 check error message in test 3a4ebeb use preconditions in the library f443b18 partial inlining is no longer needed 5624b15 instrumentation for preconditions 54e80da added __CPROVER_precondtion(c, d) 1d81035 Merge pull request diffblue#1393 from diffblue/byte_extract_is_binary 4e1fe93 Merge pull request diffblue#1396 from diffblue/String6-fixup 9497b02 Merge pull request diffblue#1395 from diffblue/msvc_unistd 17c6ca0 MSVC doesn't have strcasecmp and strncasecmp; use header for free() 237b31a Visual Studio doesn't have unistd.h; signal.h isn't needed for the MSVC build 5ef9c17 Revert 20e4def (preformatted_output flag) 3d4c794 Pass ostream instead of using cout in natural_loops 2716410 Update linter to cope with CBMC subtree 63fc53b Stop using sed to modify scripts! 58b75cf Merge pull request diffblue#1307 from zemanlx/coverity da91319 Adapt to upstream change in write_goto_binary interface and languaget 177a13d Add Coverity scan 22fb7c1 added splice-call feature in goto instrument It prepends a nullary function call say foo in the body of another call say moo when called as --splice-call moo,foo added tests a400c23 Merge pull request diffblue#1387 from thk123/feature/disable-mac-builds 68f2862 byte_extract expressions are binary expressions ec6ad09 Merge pull request diffblue#1379 from diffblue/remove-symex 1c1d3c2 remove path-symex and the symex tool f96ff48 Merge pull request diffblue#1384 from thk123/bugfix/regresssion-makefile 785bf43 Disable OSX builds 428b985 return STL containers directly for some variants of compute_called_functions 4bdd9c4 Corrected regression makefile 2b2a841 Convert display_index_set to a free function 9fff116 Remove constructor boilerplate 150bab1 Group string_refinement arguments 317c1c6 Group bv_refinement config variables bf47f81 Use expr_cast in string_exprt casts c5fa708 Refactor integer conversions f99c8ff Replace exceptions with optional git-subtree-dir: cbmc git-subtree-split: d0d3620

romainbrenguier requested review from cesaro, peterschrammel and LAJW August 12, 2017 17:46

romainbrenguier force-pushed the feature/string-max-input-length#948 branch from 52276aa to 15dd83f Compare August 12, 2017 17:51

romainbrenguier force-pushed the feature/string-max-input-length#948 branch 2 times, most recently from 4e267e6 to 313448d Compare August 14, 2017 09:48

romainbrenguier force-pushed the feature/string-max-input-length#948 branch from 313448d to b160adc Compare August 18, 2017 08:08

tautschnig changed the base branch from test-gen-support to develop August 22, 2017 12:15

tautschnig changed the title ~~String max input length option~~ [depends: #1241] String max input length option Aug 22, 2017

LAJW approved these changes Aug 22, 2017

View reviewed changes

tautschnig assigned romainbrenguier Aug 23, 2017

romainbrenguier assigned LAJW and unassigned romainbrenguier Aug 30, 2017

romainbrenguier force-pushed the feature/string-max-input-length#948 branch from b160adc to da04046 Compare August 31, 2017 08:23

LAJW reviewed Sep 1, 2017

View reviewed changes

LAJW force-pushed the feature/string-max-input-length#948 branch from ac31e98 to 37f12ec Compare September 4, 2017 11:36

tautschnig changed the title ~~[depends: #1241] String max input length option~~ String max input length option Sep 4, 2017

romainbrenguier requested review from cesaro and peterschrammel and removed request for cesaro and peterschrammel September 4, 2017 13:43

allredj reviewed Sep 4, 2017

View reviewed changes

LAJW force-pushed the feature/string-max-input-length#948 branch 2 times, most recently from 113681c to 9ea8cdc Compare September 6, 2017 11:29

allredj reviewed Sep 11, 2017

View reviewed changes

LAJW force-pushed the feature/string-max-input-length#948 branch from 47fba28 to 899592f Compare September 14, 2017 08:49

allredj approved these changes Sep 14, 2017

View reviewed changes

LAJW force-pushed the feature/string-max-input-length#948 branch from 899592f to 2563123 Compare September 14, 2017 11:56

romainbrenguier commented Sep 18, 2017

View reviewed changes

LAJW force-pushed the feature/string-max-input-length#948 branch 3 times, most recently from 1f6e6b4 to 6fe89b4 Compare September 18, 2017 09:09

romainbrenguier added 2 commits September 18, 2017 11:24

Adding string max input length option

440d19f

Tests for new option string-max-input-length

621da87

LAJW force-pushed the feature/string-max-input-length#948 branch from 6fe89b4 to 621da87 Compare September 18, 2017 10:40

allredj merged commit bc30987 into diffblue:develop Sep 18, 2017

String max input length option #1235

String max input length option #1235

Conversation

romainbrenguier commented Aug 12, 2017

cesaro commented Aug 12, 2017 • edited Loading

romainbrenguier commented Aug 14, 2017

cesaro commented Aug 14, 2017

romainbrenguier commented Aug 18, 2017

allredj commented Aug 22, 2017

LAJW commented Aug 22, 2017

Choose a reason for hiding this comment

LAJW commented Sep 4, 2017

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

LAJW Sep 6, 2017 • edited Loading

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

LAJW Sep 6, 2017 • edited Loading

Choose a reason for hiding this comment

Choose a reason for hiding this comment

allredj commented Sep 6, 2017

allredj commented Sep 11, 2017

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

allredj left a comment

Choose a reason for hiding this comment

romainbrenguier 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

allredj commented Sep 18, 2017

cesaro commented Aug 12, 2017 •

edited

Loading

LAJW Sep 6, 2017 •

edited

Loading

LAJW Sep 6, 2017 •

edited

Loading