[TG-2608] Use string dependencies to reduce the number of constraints #1947

romainbrenguier · 2018-03-19T17:00:12Z

Instead of adding all constraints corresponding to a string function
call, we look at which strings may be used in a testing function (such
as endsWith, equals, compare, etc...).
We only add constraints for these function calls, since the other operations can not matter for the
satisfiability problem.

tautschnig

I have only reviewed the changes to graph.h.

tautschnig · 2018-03-19T17:30:45Z

src/util/graph.h

+/// \param set: set of source nodes, must be a container with an
+///   `insert(const value_type&)` method.
+/// \param for_each_successor: function which given a node `n` and a function
+///   `f`, applies `f` on all successors of `n`.


Could this comment please be a bit more technical and actually say which graph traversal algorithm is used (I think it's depth-first search), and explain what the idea behind this function is?

I updated the comment

tautschnig · 2018-03-19T17:33:14Z

src/util/graph.h

+    const std::function<void(const typename Container::value_type &)> &)>
+    &for_each_successor)
+{
+  std::vector<nodet> stack;


Don't store nodet, use node_indext. Going from a node_indext to a nodet is constant time, but a node_indext will typically consume a lot less memory.

Since this function is generic you can use it different ways, in particular if you give a set of node_indext then the algorithm will only manipulate node_indext. nodet here does not have to correspond to graph::node_t.

tautschnig · 2018-03-19T17:36:31Z

src/util/graph.h

+/// \param for_each_successor: function which given a node `n` and a function
+///   `f`, applies `f` on all successors of `n`.
+template <class Container, typename nodet = typename Container::value_type>
+void get_reachable(


~~This function is introduced, but never used in this PR?~~

It used in b2ca937

romainbrenguier · 2018-03-22T12:04:50Z

I extracted a few commits which correct existing bugs in #1958 which should be merged before this PR.

LAJW · 2018-03-23T10:58:29Z

src/solvers/refinement/string_refinement_util.cpp

+  std::for_each(
+    node.dependencies.begin(),
+    node.dependencies.end(),
+    [&](const std::size_t &index) { f(builtin_function_nodes[index]); });


It looks like you could just use a ranged for-loop.

LAJW · 2018-03-23T10:59:30Z

src/solvers/refinement/string_refinement_util.cpp

  }
  else
-    UNREACHABLE;
+  {
+    INVARIANT(node.kind == nodet::STRING, "nodes are either BUILTIN or STRING");


I think UNREACHABLE at the end would be better.

peterschrammel · 2018-03-23T14:07:16Z

src/solvers/refinement/string_builtin_function.h

+  /// Tells whether the builtin function can be a testing function, that is a
+  /// function that does not return a string, for instance like `equals`,
+  /// `indexOf` or `compare`.
+  virtual bool maybe_testing_function() const


Why maybe and not is?

For the functions that don't have yet a dedicated builtin_function class we consider that could be testing function although we don't actually know. Ultimately this can be replaced by a is

peterschrammel · 2018-03-23T14:08:46Z

src/solvers/refinement/string_refinement_util.cpp

+        f(*string_node);
+      else
+      {
+        std::cout << "Warning no node for " << format(current) << std::endl;


cout is forbidden outside #ifdef DEBUG

peterschrammel · 2018-03-23T14:09:02Z

src/solvers/refinement/string_refinement_util.cpp

+      else
+      {
+        std::cout << "Warning no node for " << format(current) << std::endl;
+        //UNREACHABLE;


Why is this commented out?

I reestablish it in a later commit that could be squashed with this one.
ec6321f

peterschrammel

There's a failing test: https://ci.appveyor.com/project/diffblue/cbmc/build/1.0.8107#L5008

This is for builtin functions supported by string_constraint_generatort but not string_builtin_functiont.

We add constraints directly from the constructed graph instead of going through all the equations.

This is more natural than always having to refer to the builtin_function_nodes array.

This is to know whether the result of a function can be used outside of string operations.

Because of some issues with Visual Studio these need to be defined.

This takes as argument a set and a for_each_successor function. This can be used even by classes that do not inherit from grapht.

This is to be able to use containers such as unordered_set/unordered_map

Instead of adding all constraints corresponding to a string function call, we look at which strings may be used in a testing function (such as endsWith, equals, compare, etc...). We only add constraints for these function calls, since the other operations cannot matter for the satisfiability problem.

This reduces the number of universal formulas added (from 6 to 3), and avoid introducing new strings. Ideally the add_axioms_-function should not introduce new strings, that would make it easier to refactor and add new functionalities.

This tests, check that only constraints for the string operation that matters are added to the list of axioms of the string solver. In the example added here, the solver would previously consider 11 constraints, but now only 3, and still finds the correct result.

These two functions deal with one type of node. Type safety ensures we don't mix the two kinds of node, so these two functions can be made public.

The interface for string dependencies has changed so these need to be adapted.

This defines functions adding constraints on length of strings. This constraints are used in the add_axioms_* functions and the goal is to reuse them in string dependencies, to add axioms only about the length and not the content of the strings.

This give the constraints that ensure the length of the result of a buitin function is correct. Will be used when we don't need the constraints about the actual content of the strings.

When the result of a function is not tested we don't need to add full constraints, but constraints about the length may still be necessary as the length field of the string can be accessed directly.

This could be used in several places in this file.

We make sure a node is created for each atomic string in arguments of builtin functions. This allows us to restablish the check that a node exists for each dependency of a builtin function.

constraint_generator is kept as a class member because it is used by get, but we need to make sure it is cleared at each dec_solve call so that we don't keep unecessary or redundant constraints.

Execution time can vary depending on what the sat solver find as a model at the refinement steps. Observed execution time go from 0.2s to 7s. Setting the limit to 100 limit these variations (maximum observed is 0.3s).

207b801 Merge branch 'develop' into merge_2018-03-26 301cd46 Merge pull request diffblue#1969 from smowton/smowton/cleanup/document_sccs_guarantee 9c04abd Document grapht::SCCs 18478e9 Merge pull request diffblue#1947 from romainbrenguier/dependency-graph/stop-adding-unecessary-constraints#TG-2608 be66b35 Merge pull request diffblue#1961 from danpoe/slice-global-inits-fix 60bfbd0 Reduce string-max-length on String.equals test 50cfe34 Clear constraints at each call to dec_solve 367ca13 Ensure all atomic strings in arguments have node 0bb2fad Define a for_each_atomic_string helper function 805f45f Correct add_constraints in string_dependencies 61b3910 Add length_constraint method to builtin functions 8684e6d Helper functions for length constraints on strings 8a98246 Adapt unit tests for the new interface c3aed85 Define two helper functions for for_each_successor a45c64f Add tests for the use of string dependencies e3da98c Deactivating invariant 2655a9b Rewrite axioms for insert be5f194 Add double quotes to output_dot 4b342f7 Only add constraints on test function dependencies 3c61cf2 Add a hash function for nodes 23f8cd4 Correct name of builtin function with no eval c487c4b Generic get_reachable function 46d2507 Add move constructors to builtin_function_nodet 6609247 Add a maybe_testing_function to builtin functions 97ee2d6 Store builtin function pointer inside builtin node 41c0294 Add constraints from the string dependencies 8a7d194 add_constraints method in string_dependencies b8df2b3 Initialize return_code for all builtin_functions 82f552c Add and add_constraint method to builtin functions 2e7057a Remove use of unknown_dependency 408adbe never return nullptr in to_string_builtin_function c26b83d Constructor for builtin function with no eval 54a4d7d Add class for builtin function with no eval 8e0f974 Merge pull request diffblue#1970 from tautschnig/java-bytecode-fixes edb8eeb Merge pull request diffblue#1905 from smowton/smowton/cleanup/broken-regression-tests c188986 Merge pull request diffblue#1957 from smowton/smowton/cleanup/show-goto-functions-documentation df1c7e3 Builds require javac as of f66288b 1782e8f Include missing map header 55656ff Include missing invariant header 0b17511 Merge pull request diffblue#1955 from svorenova/bugfix_tg2842 eb1ac7b Merge pull request diffblue#1964 from peterschrammel/documentation/online-docs-link 356a96c Merge pull request diffblue#1953 from smowton/smowton/cleanup/document-java-synthetic-methods 19e5bba Document synthetic methods generated by the Java frontend 706ffa7 Make test lambda1 compatible with symex-driven loading 0759129 Clarify slightly that show-symbol-table et al are restricted to loaded symbols d7efdd1 Improve docs TOC structure 4043681 Add online documentation to README 076aa5a Improving warnings for unsupported signatures for generics cont. c63c05b Add unit tests for mocked/unsupported generics cont. 067eeff Refactoring and adding utility functions in require_type 11e9a77 Ignore generic arguments for mocked and unsupported generic classes cont. 3a45ee9 Improving warnings for unsupported signatures for generics f3cdd97 Add unit tests for mocked/unsupported generics 51a5845 Pull out common generic classes/interfaces for unit tests fc83526 Ignore generic arguments for mocked and unsupported generic classes 3b00bdc Fix tests with missing EXIT or SIGNAL tests 7b56203 Merge pull request diffblue#1965 from smowton/smowton/fix/reachability-slicer-incompatible-with-symex-driven-loading 5903b62 Merge pull request diffblue#1952 from diffblue/more-builtins e25a7ac Mark the new reachability-slicer incompatible with symex-driven loading c5b4e19 Merge pull request diffblue#1963 from tautschnig/dimacs-output 4f3fb8b Merge pull request diffblue#1958 from romainbrenguier/bugfix/insert-offset cd184f1 Merge pull request diffblue#1780 from Charliemowood/documentation/review-cbmc-docs 1ee0dd9 Merge pull request diffblue#1943 from forejtv/forejtv/reachability-slicer 9aa70a7 Add doc README.md files to each directory 1b7f57d Use doxygen layout file c22e2e9 Add make doc to Makefile c50f40d Remove old doxygen module directives from header files c1f9e34 Move SATABS references to separate from user manual 42f9f36 Improve docs content layout and front page 0afcf90 dimacs: make sure printing a dimacs is fast a403fdd Fix a bug in slice global inits where guard expressions were disregarded 7e00a30 Merge pull request diffblue#1759 from smowton/smowton/feature/symex-driven-program-loading 22e9b32 Merge pull request diffblue#1960 from smowton/smowton/admin/remove-reuk f10c697 Remove reuk as a code-owner c5aa507 Document builtin function constructors 953e2df Enable show-properties with symex-driven lazy loading 6c79494 Fix broken static_init_order test descriptions ccb2cf3 Fix broken test descriptions 8aa38e7 Add tests for symex-driven lazy loading 7b5d73b JBMC: use symex-driven lazy loading 978ca5b Add callback after symex to bmct 8df9350 Java frontend: rename externally driven loading 98741f9 Java frontend: note availability of synthetic methods 890b8b1 Remove exceptions: add per-function entry point 3ef9ec8 Correct for_each_successor method aebadee Correct offset in eval for insert 71983b3 Remove mention of size in eval_string 4cca831 Move string_builtin_function class to a new file 6120c17 Changes to the reachability slicer f6219d4 Merge pull request diffblue#1940 from smowton/smowton/cleanup/remove-virtual-functions 34b2b02 Merge pull request diffblue#1939 from romainbrenguier/bugfix/builtin-string-insert-eval 9d9fafa Merge pull request diffblue#1941 from diffblue/rotate 84186ff Tests for CProverString.append with start/end args 882bbb1 Fix eval of concatenation builtin functions ad9b86c Fix add_axioms_for_concat_substr b43bbff Tests for CProverString.substring 4be7532 Test for CProverString.insert 5f96226 Fix string constraints for substring 9ff1e82 Fix eval of insert to match string constraints f3694af added support for rotation operators 126e90a Remove virtual functions: fix no-fallback-function mode 442f315 Merge pull request diffblue#1951 from zemanlx/support/public-cprover-documentation 8c501cc Use abstract_goto_modelt instead of goto_functionst in bmc reporting phase 760d1ca Lazy goto model: implement abstract_goto_modelt a4f5d77 goto_modelt: implement abstract_goto_modelt 311ca9c Add abstract_goto_modelt 2fe999c Add gcloud integration to Travis a5c26a8 Add script for uploading documentation 566539e Add encrypted GCloud key for Travis 07bafd2 move CPROVER built-in functions into the factory 7f3ba30 Merge pull request diffblue#1814 from NlightNFotis/flush-json-stream 7161f17 Merge pull request diffblue#1879 from diffblue/smt2-frontend ab68848 tests for smt2_solver 246472f an SMT2 solver using boolbv and satcheckt a75ee3f Add missing langapi dependency to util d83fa17 Merge pull request diffblue#1932 from romainbrenguier/stop-adding-counter-examples b5f12ff Correct initial index set computation c905c2c Remove "Adding counter-examples" message 7085f9c Correct find_index function for `if`-expressions 123be20 Fix goto-diff tests that got broken by streaming json 2ab3b9c Activate JSON streaming when printing goto-traces 54bae24 Refactor huge convert function into multiple ones a68125c Base JSON UI message handler upon json_streamt 35ac459 Introduce class for streaming JSON to the output a2a3140 Correct bounds in instantiate method 0910010 Fix string constraints 7586f76 Only add counter examples when index set exhausted 5268c44 a translator from SMT2 into expressions 6dde6b1 add support for let_exprt 37f69b2 added to_mathematical_function_type 7b670cd fix line number counting in SMT2 tokenizer f3cb5bb Merge pull request diffblue#1938 from romainbrenguier/fix-cmake 213cb57 Fix cmake build 9e11b41 Replace java_int_type by tyep deduced from array fc67510 Get rid of java_bytecode includes in string solver 461b3a5 Merge pull request diffblue#1922 from romainbrenguier/dependency-graph/get-model#TG-2607 1a874b3 Add name method to builtin functions 8d4a057 Decompose if_expr when adding dependencies cb72bb7 Correct insert builtin function construction d0a8868 Constructor and destructor of builtin functions 7bb5aff Make node point to builtin func they result from a89ceb0 Tests for string solver get with new dependencies 0b3796e Declare a nodet class in string_dependencies fb676d5 Add a cache for eval in string dependences 095d57b Add concat_char builtin function for strings 44693e8 Use eval of builtin function in get when available 56cb571 Activate dependency computation in string solver 69f31c1 Add eval function to string_dependenciest 357cb44 Add const node_at function in string dependencies e308bad Rename class to string_dependenciest 06dc6b2 Add an evaluation method to builtin functions f6a153e Check type before adding dependencies 0139424 Fix linting problem in string_constraint 5108a72 Fix string constraints printing a2fab10 Linting corrections in string_refinement 05a3426 Merge pull request diffblue#1925 from hannes-steffenhagen-diffblue/testpl_use_env_testpl 8869dd8 Merge pull request diffblue#1920 from diffblue/bugfix/continue_bootstrapmethods_parsing_after_unsupported_entry d404a55 Merge pull request diffblue#1931 from owen-jones-diffblue/owen-jones-diffblue/fix-release-build-compilation c6102f7 Merge pull request diffblue#1918 from thk123/tests/tg-2485/lambda-lazy-loading 008de5d Use environment variable for jobs in test.pl ea6f00f Fixing linter error 0b20a81 Added explanation to the test 1974010 Adjusted the if check to aid readability 42065ec Adjust the interface of the bootstrap methods map dcd680f Correcting formating on java file d8edf4f Adjusted test to pass c0f054a Removing redundant method from test f494674 Use function that actually contains the lambdas 8615500 Added to readme that the file is compiled using the eclipse compiler a604b26 !fixup Removed impossible condition (9fc5bfd) 12f049e Added extra information to the warnings to differentaite the different cases 1db68a5 Moved the first condition to after the explanation of our assumptions c1aa16c Renamed parameter variables 4bb98f0 Removed impossible condition 9749d5a Refactored error reporting method into a seperate function 6400294 Replace nested else ifs with a continue on error conditions 067ccbf Rename j to boostrap_method_index d7a4e50 Add regression test compiled with ecj e11163c Continue parsing after unsupported BootstrapMethods entry e1961d8 Adding unit tests for verifying the behaviour of lazy methods on lambdas 28c6477 Adding utility for getting symbols out of the symbol table 06ab440 Merge pull request diffblue#1930 from owen-jones-diffblue/owen-jones-diffblue/skip-duplicate-callsites-in-lazy-methods-v1 6eab160 Speed up resolution of virtual callsites in lazy loading v1 c470bdf Replace assert(false) by UNREACHABLE 3af5509 Merge pull request diffblue#1923 from romainbrenguier/author-refinement-util 802b819 Merge pull request diffblue#1926 from tautschnig/fix-json 08ad919 Merge pull request diffblue#1913 from thk123/refactor/lazy-load-java-class-unit-tests 1abbaff Merge pull request diffblue#1927 from peterschrammel/json-xml-timestamps 3864e6c Updating comment with relevant JIRA ticket 72fc31e Add lazy version of load_java_class 5912a04 Refactored java_load_class to allow specifying different cmd line args 9374a1f Remove trailing whitespace from timestamp string 2ae5310 Add timestamp to JSON and XML messages 22b1628 goto-analyzer (un)reachable-functions: build valid json output 1e7f2bc Merge pull request diffblue#1907 from chrisr-diffblue/travis-test-speedups ee2cf14 Correct author entry 2e7f785 Merge pull request diffblue#1895 from romainbrenguier/dependency-graph#TG-2582 86b3e87 Merge pull request diffblue#1919 from mgudemann/enhancement/fix_diffblue_author 123541f Correct string-max-input-length tests 411e654 Unit tests for dependency graph c4ba7b4 Separate pointer/function substitutions in solver a599003 Define function for array_pointer_association a556d3d Pull out a get_function_name function 859d74c Class for string builtin functions and dependences bd8ee51 Define function template for output_dot 0b58e31 Move utility functions to string_refinement_util 68ecd9e Make interface of equation_symbol_mappingt clearer 3e688e0 Create string_refinement_util for utility function e72eacf Pull array_pool class out of constraint generator 42971da Remove default axiom in associate array to pointer f5adb47 Pull symbol generation out of constraint generator e2ca928 DiffBlue -> Diffblue d430ddc Replace copyright notice with author entry 631acab Fix Diffblue author entries e6e5134 Merge pull request diffblue#1911 from thk123/bugfix/TG-2434/static-constructor-calling-opaque-constructor 1a89e97 Remove lambda in favour of direct construction bf86af4 Correcting review comments 44153b7 Adding unit tests verifying initalizsers are correctly labelled 80a439d Apply clang-format 6edaaa0 Remove the uncasted member_type so all references use the correct version e8cbf90 Adding wrappers around whether a code_type is a constructor e5ff31f Replace checks for <init> with a call to is_constructor b25301e Remove redundant method and constructor setter c84cf21 Made member_type_lazy return type match what the method returns 6505e8c Merge pull request diffblue#1875 from peterschrammel/remove-cout-solvers 26ef31c Use invariant instead of abort() fe40b19 Use invariant instead of printing error message to cerr 066ba51 Merge pull request diffblue#1778 from peterschrammel/java-array-is-object 3548d99 Merge pull request diffblue#1917 from owen-jones-diffblue/owen-jones-diffblue/lazy-methods-do-not-create-stubs-when-resolving-virtual-calls e7a6769 Merge pull request diffblue#1877 from svorenova/specialized_generics_tg1419 b87661e Do not create stubs when resolving virtual methods 0ac57ba Rename `needed_methods` to `callable_methods` 9fef129 Rename `needed_classes` to `instantiated_classes` 0d524ee Merge pull request diffblue#1893 from diffblue/expression-printer 48024c7 Replace function applications: don't break irep sharing 86bf547 replace_expr: avoid breaking irep sharing 69bef76 Typo in function header c53cb29 Adding and updating unit tests a1e9d00 Updating and extending utility functions 2964910 Fix a bug in function for extracting generic interface reference 5c00440 Remove the old way of specializing generics 624cc91 Use the map of parameter-type pairs to specialize generics 3111255 Introduce a map of parameter-type pairs aaf9477 Use ranged for and const 7018ab4 Clean up commented out code 2529211 Clang-format f7afe1f Replace assert by invariant fc44d99 Use invariant instead if printing error message to cout a15b75f Merge pull request diffblue#1910 from diffblue/builtin-factory 5de436b usage of format() instead of from_expr for debugging b38ecc3 added format() for exprt and typet 2c8ae92 Makefile: use a variable for all those generated .inc files 17d9897 switch to C++ version of find_pattern 80ee0b1 pass type definitions to the C++ front-end 15ec42f use the builtins factory in the C frontend 1711345 added a factory for builtin function declarations 4a5b952 export all gcc bultin headers 691816b Improve job scheduling when running regression tests with -jN 87526e0 Enable a coarse-grained prallelism when running regression test jobs via Makefiles 76b93e8 Factoring out a private code from module 'remove_virtual_functions.cpp'. 15d7b71 Merge pull request diffblue#1908 from mgudemann/bugfix/fix_bootstrapmethods_empty_optional 0fd6482 Add regression test 5fa3a1a Refactor: improve variable naming ae276ef Activate two instanceof regression tests 8995fce Java arrays are instanceof Object 881b127 Refactor: use class_typet instead of struct_typet for java class fdba57c Merge pull request diffblue#1901 from romainbrenguier/fix/quantifier_exprt 782df52 Merge pull request diffblue#1909 from chrisr-diffblue/travis-make-options-cleanup 1edf0e8 Cleanup Travis Makefile build commands 1457849 Merge pull request diffblue#1894 from thomasspriggs/lambdas_compiliers_test 0ed21ca Treat empty optional case separately 3e298ef Formmatting fixes/updates for `java_bytecode_parse_lambda_method_handle` test update. f1ee826 Update `java_bytecode_parse_lambda_method_handle` tests to run for each java compiler. fe34bf6 AWS Codebuild: 4th attempt to speed up install 58b4196 AWS Codebuild: 3nd attempt to speed up install 71ab5cd AWS Codebuild: 2nd attempt to speed up install b95383a Merge branch 'develop' of github.com:diffblue/cbmc into develop e7bb127 AWS Codebuild: avoid one round of apt-get update f20e8d7 Merge pull request diffblue#1891 from diffblue/deprecated-exprt-methods 20fc8d1 Merge pull request diffblue#1363 from diffblue/undeclared-return-conflict 92b4873 Merge pull request diffblue#1791 from thk123/feature/make-irep-ids-modifiable-by-all 2fef8fd Merge pull request diffblue#1772 from tautschnig/fix-1771 f6890b3 modernisation of sum_expr and mul_expr 4d87ba1 remove exprt::negate, sum, mul, subtract (deprecated since 2011) 0d0dca4 Merge pull request diffblue#1839 from thomasspriggs/tidy_up1 1b24851 Merge pull request diffblue#1903 from chrisr-diffblue/travis-speedups b19b4a2 codebuild: enable the tests 44aa443 AWS codebuild: enable ccache 8549ecb AWS codebuild: enable cache a7cc2a0 Merge pull request diffblue#1885 from tautschnig/use-std-expr 6ef804c Merge pull request diffblue#1888 from tautschnig/linker-script-fixes d04312f Use std_{code,expr,type} constructors 00ec070 Slightly increase the number of parallel build jobs f0fc345 Increase ccache size for debug builds 423cd49 Ensure all compile jobs declare their compiler type 7b6f849 Avoid double invoking ccache a75c4f0 attempt 6 to use AWS Codebuild d3ebda0 attempt 5 to use AWS Codebuild a185ae0 fourth attempt to use AWS Codebuild 2948a43 third attempt to use AWS Codebuild 097de57 second attempt to use AWS Codebuild 4331120 first attempt to use AWS Codebuild 5c18ccc Type conflicts on the return value of implicitly declared functions are errors d074537 test for signature conflict with undeclared function 37a11f9 Merge pull request diffblue#1808 from LAJW/lajw/floating-point-to-java-string b3f2320 Add unit test for floating_point_to_java_string 7ac4fda Refactor and expose floating point to java conversion in expr2java.h 1a88479 Merge pull request diffblue#1896 from NathanJPhillips/bugfix/erroneous-reference f5330c9 Correct can_cast_expr for quantifier_exprt 00cc4b1 Merge pull request diffblue#1897 from diffblue/quantifier_exprt 8897709 Merge pull request diffblue#1800 from tautschnig/fix-process_array_expr fd513a6 added a base class for forall_exprt and exists_exprt c3ee2a1 Merge pull request diffblue#1010 from danpoe/no-body-inlining 8d8c2e0 Fix bug causing crash on Windows 4dd0f29 Merge pull request diffblue#1892 from diffblue/remove-OPERANDS_IN_GETSUB b519b41 remove OPERANDS_IN_GETSUB define, which is now simply the only option 80060ea goto-diff is missing dependencies on goto-instrument and goto-symex 7a71c80 Merge pull request diffblue#1884 from mgudemann/enhancement/update_copyright_2018 bb47a84 Merge pull request diffblue#1883 from tautschnig/implement-popcount 90beed4 Merge pull request diffblue#1845 from tautschnig/fix-1837 5cdfa94 Merge pull request diffblue#1804 from mgudemann/feature/parse_bootstrapmethods_attribute ea7975f Remove unused goto_functions parameters 76d4014 Adding tests for inner classes that capture outer class variables 9b8a73e Adding tests for lambdas as member variables db1f3b5 Adding tests for local lambdas ba8b958 Adding tests for static lambdas ebdcfb1 Adding utiltiy functions required for unit tests f79e895 Fix format and account for reviewer's comments 51bb367 Merge pull request diffblue#1886 from smowton/smowton/fix/static-inititialisers-doxygen e0ccb12 Refactor BootstrapMethods attribute reading into function 463ffe1 Refactor parse_method_handle to just deal with the lambda special case ca5dae4 Fixup Use the strcutured classes to simplify and make more explict the code b56e42e Fix missing swap for classt e3ff312 Use the strcutured classes to simplify and make more explict the code 3ac7d09 Introduce classes representing relevant constant pool entries 0e40081 Adding validation on the type of descriptor found 6d44836 Use optionalt<lambda_method_handlet> as return value f765a0d Rename, some more comments 01dcda5 status()->debug() 603aced Add regression test for lambda functions e79a655 Initial support for reading BootstrapMethods attribute b371e28 Linker-scripts: support linker symbols with struct type e999552 Linker-script processing: mind temporaries 1612f74 Do not modify object_files list while processing it 60487f7 Distribute ls_parse.py with goto-cc 631ea60 Make linker-script processing failures non-fatal 1f753d8 fixup! goto-gcc removes CPROVER macros for native gcc 716103e Implement popcount in SAT back-end ddde9dc Introduce popcount_exprt 3e793f5 Merge pull request diffblue#1887 from diffblue/string-constant-to-util 683d821 move ansi-c/string_constant.h to util/ 3188f10 Merge pull request diffblue#1795 from thk123/bugfix/TG-1358/local-variables 0cfd14b Add missing Doxygen parameter 81d2ea4 Update copyright in help output for {CJ}BM and goto-analyzer 06483f3 Merge pull request diffblue#1881 from tautschnig/fix-runtime-report 3c17453 Merge pull request diffblue#1882 from tautschnig/address_bits ce600d9 Update copyright in .cpp/.h files 004626c Adding invariant to check instruction is normal wide 60af165 Adding handmade class file exhibiting the same problem 5bdaa64 Adding test demonstrating the too many variables problem e976d6f Correctly handle wide iload commands f59092c address_bits need not return an arbitrary-sized integer 3bcb3a5 Fix decision procedure runtime computation 4d33a91 Add missing brackets to multiline if statements. 357bbe4 Fix formatting in assert replacements. f8c2b09 Replace asserts with new equivalents. ecbbc73 Remove unused `forall_symbols` macro. f1670b2 Refactor `forall_symbols` usage into c++11 loop. a8319a3 Remove unused macro `forall_symbol_module_map` 96bf623 Merge pull request diffblue#1856 from thk123/refactor/fieldref_expr 3819295 Merge pull request diffblue#1797 from thk123/bugfix/TG-1358/long-jumps 7e5922a remove functions without a body bc2c0cd Inliner fixes 0003d8a Merge pull request diffblue#1864 from owen-jones-diffblue/owen-jones-diffblue/consistent-casts-in-remove-virtual-function d2e10af Remove the "fieldref" id 2ba794d Introduce fieldref_exprt to represent a field reference c9f3ea4 Test casts in remove_virtual_function() 9df769a Byte offset to array index translation must use array type f4fb099 Fix process_array_expr to take into account pointer offset 379705f Process array_equal the same way as array_{replace,copy} c62b957 Merge pull request diffblue#1551 from tautschnig/perf-test-improvements 1dfb5cd Merge pull request diffblue#1871 from mgudemann/bugfix/superclass_references_for_implicit_generic 71b32f4 Merge pull request diffblue#1777 from romainbrenguier/refactor/java-bytecode-instrument-TG-2331 25eb1a3 Add unit test for implicitly generic super class 590fc2d Make USE_DSTRING conditional and disable it in Ubuntu/Clang/DEBUG Travis job 52290b0 Include string when not using dstringt as irep_idt representation 25ffad4 Do not use dstringt-specific APIs with irep_idt 534f4d2 Include list in expr.h d87d6e4 Include unordered_map where using a std::unordered_map a72f52a [TG-2585] Support implicitly generic superclasses 83d9272 Merge pull request diffblue#1870 from diffblue/chrono-precision 2dc9fcd do not round reported durations to seconds 28c3c9f Merge pull request diffblue#853 from owen-jones-diffblue/feature/pointer-function-parameters ab1b267 Merge pull request diffblue#1832 from diffblue/smt2-backend 11f3699 Merge pull request diffblue#1853 from danpoe/is-threaded-fixes 3e7e840 Merge pull request diffblue#1829 from romainbrenguier/refactor/substitute_array_access#TG-2138 830d519 Merge pull request diffblue#1830 from romainbrenguier/feature/cover-basic-block-java#TG-1404 3a112af Merge pull request diffblue#1846 from hannes-steffenhagen-diffblue/develop-fix_appveyor 9d1e625 Merge pull request diffblue#1641 from karkhaz/kk-big-6-6 7e176f7 Make argument of instrument_code be of type codet b0df38d Make return type of expr_instrumentation an optional 9c838a1 Documentation improvements in bytecode instrument ea3ba42 Remove unused includes f6488d7 Using constant string vector instead of irep_idt d67fa60 [path explore 7/7] Path exploration documentation 53df567 [path explore 6/7] cpplint & clang-fmt agree on : e8eec2c [path explore 5/7] Support path-based exploratio2 c88a3ab [path explore 4/7] Factor out common BMC code d7a70e1 [path explore 3/7] Logical ops for resultt c53d630 [path explore 2/7] Ignore jbmc binary 6d657a0 Merge pull request diffblue#1779 from diffblue/smt2-integers 63beb71 Update coverage goals in goto-diff test 654418a Unit tests for sparse_arrayt d65bf9f Class for sparse arrays representations 773721b Refactoring of substitute array access dc5ffc9 Documentation improvements in string solver 5f54049 Add unit tests for java block instrumentation 105c7e3 Adapt coverage test for new instrumentation c1045aa Use [] instead of `at` on vector 6811238 cover_block implementation using bytecode location acf9fe4 Refer to interface rather than cover_basic_blockst 3cd2f0b Put interface to cover_blocks in virtual class 8e7f129 Correct types from unsigned to std::size_t 0fc9c5e Merge pull request diffblue#1866 from romainbrenguier/feature/code-location-in-preprocessing f270e92 Merge pull request diffblue#1835 from diffblue/remove-goto-templates d82c586 missing header for std::time_t fdc5b1e Add source location to code added by preprocessing 0208218 Merge pull request diffblue#1861 from peterschrammel/goto-diff-properties 8192246 Make remove_virtual_function() consistent 9c12abb make linter happy ba8bbe2 expand goto_programt and goto_functionst templates b36a90a Merge pull request diffblue#1851 from tautschnig/remove-expr-listt 897e29e Fix CMakeLists to correctly pass test exclusion flags 07e0d58 Merge pull request diffblue#1841 from NathanJPhillips/cleanup/remove-unused-params 4d3ab7a Merge pull request diffblue#1838 from mgudemann/bugfix/catch_unsupported_generics_exception a8bdb09 Merge pull request diffblue#1817 from allredj/string-primitives-for-exceptions 1ebec11 get values for nondet symbols a827c77 fix: add missing integer casts and operations bf9b2c1 Merge pull request diffblue#1862 from diffblue/cbmc-test-results-quantifiers 2b92cd3 Update regression tests to use string primitives dd5a674 Add jbmc string primitives to CProverString 8f6431c Introduce more string primitives in JBMC a39fff8 remove iteration count from test result daab304 remove spurious spaces 482ec4a edit a space df9aab5 Test for goto-diff show properties a4d3dc3 Show properties in goto-diff d3eb1f3 Use CPROVER exit codes a0e5063 Enable goto check and cover options in goto-diff a0c45f4 Factor out show properties command line def and docs 937b5f9 Expose conversion of properties of a goto-program into a JSON array f4a8b0c Replace cout in show_properties c480d28 Merge pull request diffblue#1842 from NathanJPhillips/feature/depth_iterator_get_mutable 416bbe0 Allow non-const depth_iteratort to be created from a const root ac37f0b Removed unused parameter/private field 7070296 Add unit test to Makefile f42eeb2 Add unit test for generic superclass with unsupported signature e760d6b Catch unsupported generics exception in superclass ref extraction b0eb45e Merge pull request diffblue#1840 from NathanJPhillips/bugfix/test-name 6f622d1 Fixes for is_threadedt, --is-threaded 13b77d8 Include list where using a std::list and drop forall_expr_list macro 2ccc41b Remove destination directory before trying to move to it in AppVeyor a094990 Fixed test name a0bfd42 smt2irep now uses smt2_tokenizert 3587184 added an SMT-LIB2 tokenizer dea2592 treat real and integer as 'numeric' in C front-end 57ecf15 + is multi-ary in SMT-LIB2 12ae728 fixes for integers in SMT2 698ccdd use a ranged for bc0ebd3 Bounds checks in fgets, read dda54c7 Adding test includes a jump to address 2^16 3f202fa Add support for reading nop operations 7a205f0 Correct handling of two byte offsets cb2c7a8 Adding the irep_ids file to frequently modified low risk files 03095d4 Use svcomp18 as base f659577 perf-test: build configuration using glucose 98b9ae6 SV-COMP now requires zip files 1c0cf32 Support custom CodeBuild templates 6eeb672 Permit selecting a regular-expression-defined set of tasks d3b29d2 Update cprover-sv-comp, benchexec to latest version 3269da7 Utility to generate HTML reports from perf-test experiments cf4eeb2 Move code into code block instead of copying it 7f4a79e Tidy up C symbol factory code REVERT: f7602af Merge commit 'bb88574aaa4043f0ebf0ad6881ccaaeb1f0413ff' into merge-develop-20180327 git-subtree-dir: cbmc git-subtree-split: 207b801

romainbrenguier requested review from kroening, martin-cs, peterschrammel, smowton and tautschnig as code owners March 19, 2018 17:00

romainbrenguier force-pushed the dependency-graph/stop-adding-unecessary-constraints#TG-2608 branch from 0f45aaf to fb5aae6 Compare March 19, 2018 17:01

romainbrenguier requested a review from LAJW March 19, 2018 17:01

tautschnig reviewed Mar 19, 2018

View reviewed changes

romainbrenguier force-pushed the dependency-graph/stop-adding-unecessary-constraints#TG-2608 branch from fb5aae6 to fe41aa9 Compare March 20, 2018 07:14

romainbrenguier requested a review from chrisr-diffblue as a code owner March 20, 2018 07:14

romainbrenguier mentioned this pull request Mar 21, 2018

Make get_reachable a function rather than a method romainbrenguier/cbmc#5

Closed

romainbrenguier force-pushed the dependency-graph/stop-adding-unecessary-constraints#TG-2608 branch 2 times, most recently from 85a293a to d9ab3fc Compare March 22, 2018 11:23

romainbrenguier mentioned this pull request Mar 22, 2018

Bug fixes in String builtin functions [TG-2459] #1958

Merged

romainbrenguier added the In progress label Mar 22, 2018

romainbrenguier force-pushed the dependency-graph/stop-adding-unecessary-constraints#TG-2608 branch from d9ab3fc to 7d1a807 Compare March 23, 2018 09:40

LAJW approved these changes Mar 23, 2018

View reviewed changes

romainbrenguier force-pushed the dependency-graph/stop-adding-unecessary-constraints#TG-2608 branch 2 times, most recently from 6950a1d to 3687790 Compare March 23, 2018 11:32

romainbrenguier requested review from cesaro, mgudemann and thk123 as code owners March 23, 2018 12:19

peterschrammel requested changes Mar 23, 2018

View reviewed changes

romainbrenguier force-pushed the dependency-graph/stop-adding-unecessary-constraints#TG-2608 branch 2 times, most recently from d959354 to 2900b71 Compare March 23, 2018 16:04

romainbrenguier removed the In progress label Mar 23, 2018

peterschrammel reviewed Mar 23, 2018

View reviewed changes

romainbrenguier added 2 commits March 24, 2018 19:24

Add class for builtin function with no eval

54a4d7d

This is for builtin functions supported by string_constraint_generatort but not string_builtin_functiont.

Constructor for builtin function with no eval

c26b83d

romainbrenguier added 9 commits March 24, 2018 19:24

add_constraints method in string_dependencies

8a7d194

Add constraints from the string dependencies

41c0294

We add constraints directly from the constructed graph instead of going through all the equations.

Store builtin function pointer inside builtin node

97ee2d6

This is more natural than always having to refer to the builtin_function_nodes array.

Add a maybe_testing_function to builtin functions

6609247

This is to know whether the result of a function can be used outside of string operations.

Add move constructors to builtin_function_nodet

46d2507

Because of some issues with Visual Studio these need to be defined.

Generic get_reachable function

c487c4b

This takes as argument a set and a for_each_successor function. This can be used even by classes that do not inherit from grapht.

Correct name of builtin function with no eval

23f8cd4

Add a hash function for nodes

3c61cf2

This is to be able to use containers such as unordered_set/unordered_map

romainbrenguier force-pushed the dependency-graph/stop-adding-unecessary-constraints#TG-2608 branch 3 times, most recently from a57554a to 1238d63 Compare March 24, 2018 22:02

romainbrenguier added 13 commits March 25, 2018 11:15

Add double quotes to output_dot

be5f194

Rewrite axioms for insert

2655a9b

This reduces the number of universal formulas added (from 6 to 3), and avoid introducing new strings. Ideally the add_axioms_-function should not introduce new strings, that would make it easier to refactor and add new functionalities.

Deactivating invariant

e3da98c

Define two helper functions for for_each_successor

c3aed85

These two functions deal with one type of node. Type safety ensures we don't mix the two kinds of node, so these two functions can be made public.

Adapt unit tests for the new interface

8a98246

The interface for string dependencies has changed so these need to be adapted.

Add length_constraint method to builtin functions

61b3910

This give the constraints that ensure the length of the result of a buitin function is correct. Will be used when we don't need the constraints about the actual content of the strings.

Correct add_constraints in string_dependencies

805f45f

When the result of a function is not tested we don't need to add full constraints, but constraints about the length may still be necessary as the length field of the string can be accessed directly.

Define a for_each_atomic_string helper function

0bb2fad

This could be used in several places in this file.

Ensure all atomic strings in arguments have node

367ca13

We make sure a node is created for each atomic string in arguments of builtin functions. This allows us to restablish the check that a node exists for each dependency of a builtin function.

Clear constraints at each call to dec_solve

50cfe34

constraint_generator is kept as a class member because it is used by get, but we need to make sure it is cleared at each dec_solve call so that we don't keep unecessary or redundant constraints.

Reduce string-max-length on String.equals test

60bfbd0

Execution time can vary depending on what the sat solver find as a model at the refinement steps. Observed execution time go from 0.2s to 7s. Setting the limit to 100 limit these variations (maximum observed is 0.3s).

romainbrenguier force-pushed the dependency-graph/stop-adding-unecessary-constraints#TG-2608 branch from 1238d63 to 60bfbd0 Compare March 25, 2018 10:15

peterschrammel approved these changes Mar 26, 2018

View reviewed changes

romainbrenguier merged commit 18478e9 into diffblue:develop Mar 26, 2018

romainbrenguier deleted the dependency-graph/stop-adding-unecessary-constraints#TG-2608 branch March 26, 2018 08:35

Provide feedback

Saved searches

Use saved searches to filter your results more quickly

[TG-2608] Use string dependencies to reduce the number of constraints #1947

[TG-2608] Use string dependencies to reduce the number of constraints #1947

romainbrenguier commented Mar 19, 2018

tautschnig left a comment

tautschnig Mar 19, 2018

romainbrenguier Mar 20, 2018

tautschnig Mar 19, 2018

romainbrenguier Mar 20, 2018

tautschnig Mar 20, 2018

tautschnig Mar 19, 2018 •

edited

romainbrenguier Mar 20, 2018

romainbrenguier commented Mar 22, 2018

LAJW Mar 23, 2018

LAJW Mar 23, 2018

peterschrammel Mar 23, 2018

romainbrenguier Mar 23, 2018

peterschrammel Mar 23, 2018

peterschrammel Mar 23, 2018

romainbrenguier Mar 23, 2018

peterschrammel left a comment

[TG-2608] Use string dependencies to reduce the number of constraints #1947

[TG-2608] Use string dependencies to reduce the number of constraints #1947

Conversation

romainbrenguier commented Mar 19, 2018

tautschnig 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

tautschnig Mar 19, 2018 • edited

Choose a reason for hiding this comment

Choose a reason for hiding this comment

romainbrenguier commented Mar 22, 2018

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

peterschrammel left a comment

Choose a reason for hiding this comment

tautschnig Mar 19, 2018 •

edited