JBMC: Add symex-based program loading #1759

smowton · 2018-01-19T17:08:19Z

This adds the final few pieces required and enables symex-driven program loading in JBMC, controlled by the --symex-driven-lazy-loading command-line option. In this mode, functions are effectively finalised one-by-one, including committing to final location numbers, loop numbers and so on, so that references to instructions taken by symex remain valid in the eyes of subsequent passes.

Some JBMC options are currently incompatible: some for fundamental reasons (--lazy-loading specifies an alternate, incompatible loading scheme; --all-properties requests a list of assertions with no particular entry-point in mind and therefore nowhere to symex from; --full-slice fundamentally requires a whole program available), and one that will require a little extra work (java-unwind-static-init is currently implemented in a way that clashes with symex-driven loading, but can be reworked in a subsequent PR).

The whole JBMC test corpus is used to test symex-driven loading, with a small number of tests tagged to indicate incompatibility.

smowton · 2018-01-19T17:08:55Z

@NathanJPhillips please review

tautschnig · 2018-01-19T17:21:54Z

Is it show-properties rather than all-properties that’s in conflict?

NathanJPhillips

Most significant request is not to std::move something passed into a function by l-value.

NathanJPhillips · 2018-01-30T16:00:10Z

src/goto-programs/remove_exceptions.cpp

  goto_functionst &goto_functions,
  remove_exceptions_typest type)
 {
  const namespacet ns(symbol_table);
  std::map<irep_idt, std::set<irep_idt>> exceptions_map;
  uncaught_exceptions(goto_functions, ns, exceptions_map);
+  // NOLINTNEXTLINE


Can the linter be fixed or this lint error ignored in review?

Couple of other instances of this too.

Long-standing problem; haven't the time or inclination to dig into the linter just now...

NathanJPhillips · 2018-01-30T18:15:26Z

src/cbmc/bmc.cpp

@@ -448,6 +388,107 @@ safety_checkert::resultt bmct::execute(const goto_functionst &goto_functions)
  }
 }

+safety_checkert::resultt bmct::execute(lazy_goto_modelt &lazy_model)


This parameter needs to be passed by r-value if you're going to std::move it below. i.e. the model needs to be moved into this function, indicating to the caller that it is no longer valid after this function has been called.

NathanJPhillips · 2018-01-30T18:21:20Z

src/jbmc/jbmc_parse_options.h

+  // `const goto_functionst` (ahead-of-time function loading) or
+  // `lazy_goto_modelt` (symex-driven function loading).
+  template<class ModelorfunctionsT>
+    int run_bmc(


Is this normally indented?

tautschnig · 2018-02-02T15:01:22Z

regression/test.pl

@@ -244,6 +266,8 @@ ($$$$)
  -K         known: run tests associated with known bugs
  -D <key=value> Define - replace \$key string with "value" string in
                 test descriptors
+  -I <tag>   run only tests that have the given secondary tag. Can be repeated.
+  -X <tag>   exclude tests that have the given secondary tag. Can be repeated.


I think this commit (extending test.pl) could be moved to a separate PR

Actual change request: please extend the documentation that describes the syntax of test.desc files to cover the new tagging mechansim.

Ignore the first one, but the second item still stands.

Done in the other PR; will drop this commit here.

tautschnig

"Symex: handle java-new side-effect" seems to be a wrong fix for whatever-the-symptom as ID_java_new ought not to exist at this point. Also, the tests need to be debugged fully. Otherwise a few comments.

tautschnig · 2018-02-02T15:05:30Z

src/goto-symex/goto_symex_state.h

  void switch_to_thread(unsigned t);
  bool record_events;
-  std::unique_ptr<const dirtyt> dirty;
+  std::unordered_set<irep_idt, irep_id_hash> dirty_processed_functions;


To me, this is the wrong place: this belong's to the state of the symbolic executor (goto_symext) and is not part of the symbolic program state.

tautschnig · 2018-02-02T15:14:17Z

src/cbmc/bmc.cpp

-    }
-
-    return decide(goto_functions, prop_conv);
+    return torun();


Why did you need to rewrite the entire function when seemingly just the type of the parameter should change?

I needed to provide two alternate versions of execute (see below this function), which have different prefixes depending on whether they're using a lazy or an eager goto model, but then converge after symex. This particular factoring was to avoid duplicating the error-handling code between the two cases.

tautschnig · 2018-02-02T15:17:06Z

src/goto-symex/symex_assign.cpp

@@ -63,7 +63,7 @@ void goto_symext::symex_assign(
      statement == ID_cpp_new || statement == ID_cpp_new_array ||
      statement == ID_java_new_array_data)
      symex_cpp_new(state, lhs, side_effect_expr);
-    else if(statement==ID_allocate)
+    else if(statement==ID_allocate || statement==ID_java_new)


How come? This should have been removed by remove_java_new!

Previously remove_java_new could not be run per-function, because it lowered into a sized malloc, and types could later gain fields when method conversion encountered a field access against a stubbed type. However this is no longer true, so the whole remove_java_new malarkey can now go away again. I'll submit a PR to that effect on Monday.

tautschnig · 2018-02-02T15:21:15Z

regression/jbmc-strings/java_char_array_init/test.desc

+Runs indefinitely under symex-driven lazy loading. Unsure why yet; this could
+be a bug, or could simply be variations in order of VCCs / functions perturbing
+the string solver and leading to a long unfruitful search that would actually
+terminate eventually.


Please debug properly, for example by comparing the results of --program-only.

These two have now been solved and therefore this change dropped.

tautschnig · 2018-02-02T15:21:39Z

regression/strings-smoke-tests/java_append_char/test.desc

+Runs indefinitely under symex-driven lazy loading. Unsure why yet; this could
+be a bug, or could simply be variations in order of VCCs / functions perturbing
+the string solver and leading to a long unfruitful search that would actually
+terminate eventually.


As above: please debug. No throwing-over-the-fence, please.

Change also dropped.

martin-cs

Looks fine from the point of view of the bits of code I look after, hence approve. BUT there are some pretty wide API-breaking changes here so I'm hoping that someone with a wider view of that part of the code can comment.

martin-cs · 2018-02-08T15:00:53Z

src/analyses/goto_check.h

@@ -26,6 +26,7 @@ void goto_check(
 void goto_check(
  const namespacet &ns,
  const optionst &options,
+  const irep_idt &mode,


A string called "mode" is a bit leading ... no chance of a doxygen comment on what the inputs are is there?

martin-cs · 2018-02-08T15:03:15Z

src/goto-instrument/cover.h

+  const cover_configt &,
+  goto_model_functiont &,
+  message_handlert &message_handler);
+


I guess this fits with @peterschrammel 's changes to coverage...

smowton · 2018-02-09T16:41:43Z

@tautschnig @NathanJPhillips changes applied, except as specifically noted. @tautschnig the dirty analysis check-if-function-already-analysed code has gone into incremental_dirtyt, defined alongside dirtyt.

@peterschrammel @thk123 @chrisr-diffblue this is now rebased and ready for review.

smowton · 2018-02-09T17:04:28Z

test.pl improvement moved to #1821 (but also still in this PR until that one lands).

tautschnig · 2018-02-09T17:03:58Z

src/goto-symex/symex_main.cpp

-  state.dirty=util_make_unique<dirtyt>(goto_functions);
-
+  state.dirty=util_make_unique<incremental_dirtyt>();
+  if(!pc->function.empty())


This ought to be an invariant. See #1799 for a discussion.

Suggesting merging #1843 then it will be

tautschnig · 2018-02-09T17:09:40Z

src/goto-symex/symex_main.cpp

+static goto_symext::get_goto_functiont get_function_from_goto_functions(
+  const goto_functionst &goto_functions)
+{
+  /// NOLINTNEXTLINE


I don't think that's needed here, let alone as a doxygen comment

tautschnig · 2018-02-09T17:13:39Z

src/goto-symex/symex_main.cpp

    throw "the program has no entry point";
+  }


I'd suggest to turn this into a PRECONDITION - the problem can be detected much earlier and should detected by the caller. (I know this isn't really your bug, but since lots of this code is being touched here ... if you don't mind?)

tautschnig · 2018-02-09T17:16:05Z

regression/test.pl

@@ -244,6 +266,8 @@ ($$$$)
  -K         known: run tests associated with known bugs
  -D <key=value> Define - replace \$key string with "value" string in
                 test descriptors
+  -I <tag>   run only tests that have the given secondary tag. Can be repeated.
+  -X <tag>   exclude tests that have the given secondary tag. Can be repeated.


Ignore the first one, but the second item still stands.

smowton · 2018-02-14T18:35:46Z

@tautschnig @karkhaz rebased this on top of the recent symex changes. Will peel off the first couple of commits as a separate PR later tonight.

smowton · 2018-02-16T14:24:20Z

This has been rebased to exclude the commits that landed in #1844. I'm now expecting @karkhaz to rebase #1641, then this PR will be next in line after some rewriting of its changes to the BMC driver (cbmc/bmc.cpp).

NathanJPhillips · 2018-02-16T17:42:16Z

src/jbmc/jbmc_parse_options.cpp

+    if(using_symex_driven_loading)
+    {
+      if(show_loaded_functions(goto_model))
+        exit(0);


This may abort without flushing JSON output.

NathanJPhillips · 2018-02-16T17:42:48Z

src/jbmc/jbmc_parse_options.cpp

+    // unwinds <clinit> loops to number of enum elements
+    // side effect: add this as explicit unwind to unwind set
+    if(options.get_bool_option("java-unwind-enum-static"))
+      remove_static_init_loops(goto_model, options, get_message_handler());


Where has this code come from?

tautschnig · 2018-03-21T10:09:50Z

src/java_bytecode/java_bytecode_language.cpp

@@ -814,6 +814,9 @@ void java_bytecode_languaget::methods_provided(id_sett &methods) const
  // Add all concrete methods to map
  for(const auto &kv : method_bytecode)
    methods.insert(kv.first);
+  // Add all synthetic methods to map


What is a "synthetic method"? Does this in any way relate to stubbing? If so, could we please use a consistent terminology across the code base?

I think synthetic methods are things like clinit_wrapper that we introduce to handle some JVM mechanisms, I could be wrong though? Perhaps could be defined in, e.g., synthetic_methods_map.h?

Sort of. The synthetic methods are either clinit methods, generated for stub types, or static initializer method wrappers, generated for all static initializers to ensure they only run once, generated whether a stub type or not. In future the methods defined for array types (e.g. .clone()) will probably go in this map too. Stub bodies are currently provided with a different mechanism but could use this too.

In general a synthetic method is one generated internally by the language frontend without corresponding user bytecode. Stubs are thus synthetic, but not all synthetics are stubs.

I suggest this definition goes somewhere find able in the codebase.

This isn't really related to this PR, so I've made #1953

tautschnig · 2018-03-21T10:11:37Z

src/java_bytecode/java_bytecode_language.cpp

@@ -58,8 +58,8 @@ void java_bytecode_languaget::get_language_options(const cmdlinet &cmd)
  object_factory_parameters.string_printable = cmd.isset("string-printable");
  if(cmd.isset("java-max-vla-length"))
    max_user_array_length=std::stoi(cmd.get_value("java-max-vla-length"));
-  if(cmd.isset("lazy-methods-context-sensitive"))
-    lazy_methods_mode=LAZY_METHODS_MODE_CONTEXT_SENSITIVE;
+  if(cmd.isset("symex-driven-lazy-loading"))


Somewhere there must be --help output describing this, which also needs to be fixed. And so does the parse-options header file.

Actually no, the option was added ages ago in anticipation of a driver program using it. That is now happening, but the anticipated name isn't the best.

So you're removing an option? Different kind of update, but still one expected?!

Nobody (except this file) ever accepted it until now. JBMC now accepts "symex-driven-lazy-loading".

tautschnig · 2018-03-21T10:14:32Z

src/cbmc/bmc.cpp

+    // This provides the frontend the opportunity to do things like a
+    // symbol-table or goto-functions dump instead of actually running the
+    // checker, like show-vcc except frontend specific.
+    if(frontend_callback_after_symex && frontend_callback_after_symex())


The examples seem strange: why should dumping a symbol table or goto functions require running symex? show-vcc of course does.

Because we use symex to load the functions, running show-goto-functions before symex would result in just __CPROVER_Start. The comment should probably make it explicit that this is used when looking at the "symbol-table... in conjunction with symex driven loading"

Because with symex-driven lazy loading in play, symex is the only way functions get loaded. Thus show-goto-functions has to come after symex in that case.

@thk123 added comment.

Sorry, but having to do symbolic execution in order to obtain syntactic information makes no sense. It's ok to forbid lazy loading together with show-goto-functions, but please don't produce a tool that requires a semantic analysis to produce syntactic information.

This is a reasonable thing to want for debug purposes: if I want to know what got loaded by symex-driven loading, I would pass --symex-driven-lazy-loading --list-goto-functions for example. If I want the whole class file I just don't use symex-driven-lazy-loading, which processes show/list-goto-functions the old fashioned way.

This implies that the behaviour of show-goto-functions is context-dependent. My take on this is: if you want a way to show the subset of functions that have been loaded during symbolic execution, add a new command-line option. Don't overload an existing one.

We already have --lazy-methods, under which --show-goto-functions will again show whatever was loaded, not all the functions in a particular class file.

It didn't claim that was good either ;-)

What I would suggest is additional text to the help output that explains the interaction of the command-line options.

tautschnig · 2018-03-21T10:20:51Z

regression/jbmc-strings/StringIndexOf/test.desc

+see any reason why this is the case except Minisat happening to get down a rabbit hole when
+there are other choices that lead to a quick solution. Disabling the test under symex-driven
+loading for now; most likely it will start working again in the near future for equally
+spurious reasons.


Doesn't @romainbrenguier have some fix for indexOf? Is this maybe no longer relevant?

Re-tested and this indeed appears to have cleared in the meantime. Removed the tag.

smowton · 2018-03-21T10:34:57Z

TG bump: https://github.com/diffblue/test-gen/pull/1609

thk123

Nothing blocking - some places where I think a few things could be clearer.

thk123 · 2018-03-21T10:26:26Z

src/java_bytecode/java_bytecode_language.cpp

@@ -814,6 +814,9 @@ void java_bytecode_languaget::methods_provided(id_sett &methods) const
  // Add all concrete methods to map
  for(const auto &kv : method_bytecode)
    methods.insert(kv.first);
+  // Add all synthetic methods to map


I think synthetic methods are things like clinit_wrapper that we introduce to handle some JVM mechanisms, I could be wrong though? Perhaps could be defined in, e.g., synthetic_methods_map.h?

thk123 · 2018-03-21T10:30:44Z

src/cbmc/bmc.cpp

+    // This provides the frontend the opportunity to do things like a
+    // symbol-table or goto-functions dump instead of actually running the
+    // checker, like show-vcc except frontend specific.
+    if(frontend_callback_after_symex && frontend_callback_after_symex())


Because we use symex to load the functions, running show-goto-functions before symex would result in just __CPROVER_Start. The comment should probably make it explicit that this is used when looking at the "symbol-table... in conjunction with symex driven loading"

thk123 · 2018-03-21T10:32:57Z

src/cbmc/bmc.h

@@ -147,7 +148,8 @@ class bmct:public safety_checkert
    message_handlert &_message_handler,


Add doc for the callback_after_symex specifically what the return value of the callback should indicate

thk123 · 2018-03-21T10:35:27Z

src/jbmc/jbmc_parse_options.cpp

+  if(cmdline.isset("symex-driven-lazy-loading"))
+  {
+    options.set_option("symex-driven-lazy-loading", true);
+    for(const char *opt :


for(const std::string &opt :)?

They look like const char *'s to me ;-)
If you want to do the construction of a std::string for some reason and you want to push it into the for loop then at least use const std::string instead of relying on lifetime-extension using const std::string & as this will indicate that this is newly created in this scope, not a reference to something created elsewhere.

thk123 · 2018-03-21T10:39:38Z

src/jbmc/jbmc_parse_options.cpp

+        lazy_goto_model,
+        ui_message_handler.get_ui(),
+        *this,
+        configure_bmc,


Is this always null here? No - when java-unwind-enum-static is set? Perhaps a comment (though I'm wary it risks going out of date).

Comment added

thk123 · 2018-03-21T10:40:53Z

src/jbmc/jbmc_parse_options.cpp

@@ -865,6 +1003,8 @@ void jbmc_parse_optionst::help()
    // This one is handled by jbmc_parse_options not by the Java frontend,
    // hence its presence here:
    " --java-unwind-enum-static    try to unwind loops in static initialization of enums\n" // NOLINT(*)
+    // Currently only supported in the JBMC frontend:
+    " --symex-driven-lazy-loading  only load functions when first entered by symbolic execution\n" // NOLINT(*)


This should be defined in a header file to allow re-use across different driver programs

Hmmm, it is pretty jbmc-specific at the moment though. I can't see anything except the option name being shareable with test-gen at the moment -- and it surely doesn't belong to bmct or goto_symext, both of which don't care exactly how their get_goto_program function works.

In short I agree some sort of factoring is in order at some point, but I can't see how to do it just now.

But maybe in future CBMC will care?

This is possible. For now CBMC uses none of the lazy loading infrastructure at all, and I believe @kroening's plan is for it to stay that way for a while. If and when it does, some factoring will be in order.

thk123 · 2018-03-21T10:41:49Z

regression/cbmc-java/NondetInit/test_lazy.desc

@@ -1,4 +1,4 @@
-CORE
+CORE symex-driven-lazy-loading-expected-failure


Probably good to add a comment to this test.desc explaining why this is an expected failure

I see it is because of the lazy-methods flag. I still think they'd benefit from a uniform comment, but you may disagree.

+1 for having a comment on each of the skipped desc to mention the reason they are skipped.

thk123 · 2018-03-21T10:43:59Z

regression/cbmc-java/lvt-groovy/test.desc

 DetectSplitPackagesTask.class
 --show-symbol-table
 ^EXIT=0$
 ^SIGNAL=0$
 --
 --
+This doesn't work under lazy loading because no entry-point function is given.


Probably should call it "symex driven lazy loading" since otherwise will get confusing.

thk123 · 2018-03-21T10:44:18Z

regression/cbmc-java/lvt-unexpected/test.desc

@@ -10,3 +10,5 @@ expected by the bytecode to goto conversion algorithms. Namely, the live range
 of parameter x in that method is not preceeded by a store_i instruction, which
 is perfectly possibly as per the JVM specs but currently additionally required
 in CBMC.
+
+This doesn't work under lazy loading because no entry-point function is given.


Probably should call it "symex driven lazy loading" since otherwise will get confusing. et a.

thk123 · 2018-03-21T10:45:17Z

regression/strings-smoke-tests/CMakeLists.txt

@@ -1,3 +1,10 @@
 add_test_pl_tests(
    "$<TARGET_FILE:jbmc>"
 )
+
+add_test_pl_profile(


Should these profiles be somehow added to Makefiles as well? Is that even feasible?

smowton · 2018-03-21T10:57:31Z

@tautschnig comments addressed

peterschrammel

Re --show-properties: there is a --drop-unused-functions option that also works in combination with --show-properties. Maybe you can achieve a similar behaviour for --show-properties when used together with your option.

smowton · 2018-03-21T16:52:51Z

@thk123 @tautschnig all comments addressed, please re-review

thk123

LGTM (TG bump passes as well).

FWIW my two cents re: --show-goto-functions is that the interaction is expected and useful when combined with --symex-driven-lazy-loading, it has certainly never surprised me that that is how it behaves for --lazy-methods.

I would be disappointed if we lost the ability to show loaded GOTO functions and it seems unnecessarily confusing to have a --show-loaded-goto-functions that is only useful when you've got a lazy loading on, and --show-goto-functions that's only useful when you've got it off.

smowton · 2018-03-22T11:04:44Z

@peterschrammel after a little more thought I realised show-properties could be accommodated similarly to --show-symbol-table et al. I've added a commit switching it back on, along with its test.

NathanJPhillips

Might want to squash a couple of the later test commits.

NathanJPhillips · 2018-03-22T11:46:29Z

src/cbmc/bmc.cpp

@@ -377,6 +377,15 @@ safety_checkert::resultt bmct::execute(
    const goto_functionst &goto_functions =
      goto_model.get_goto_functions();

+    // This provides the frontend the opportunity to do things like a


Is this done by a front-end or a driver? If the former then hyphenate, if the latter then reword here and rename the variable.

Good point, done

NathanJPhillips · 2018-03-22T11:57:06Z

src/jbmc/jbmc_parse_options.cpp

+  if(cmdline.isset("symex-driven-lazy-loading"))
+  {
+    options.set_option("symex-driven-lazy-loading", true);
+    for(const char *opt :


They look like const char *'s to me ;-)
If you want to do the construction of a std::string for some reason and you want to push it into the for loop then at least use const std::string instead of relying on lifetime-extension using const std::string & as this will indicate that this is newly created in this scope, not a reference to something created elsewhere.

smowton · 2018-03-22T12:57:15Z

@tautschnig are you satisfied, can we go ahead?

This removes high-level exception-related instructions from a single function, at the cost of some accuracy as we can no longer analyse other functions to determine whether or not they may throw, and therefore always assume they will.

This informs symex-driven lazy loading that certain synthetic methods can be given bodies on demand by the Java frontend, similar to how normal methods we have bytecode for are treated.

This name is more accurate, as the frontend is no longer in charge of choosing what gets loaded and why -- it just obeys convert_lazy_method requests given by the driver program.

This permits frontend programs to intervene after symex executes, either in addition to or instead of running bmc. Its current use case is to implement show-goto-functions and similar debug output options when symex-driven lazy loading means that function bodies are not populated until symex has run. When --paths is in use, the callback will be made every time symex finishes a path.

This adds the symex-driven-lazy-loading option, which causes functions to be loaded only when symex first requests their body. This means that all frontend effort can be saved relating to functions that symex reveals to be inaccessible, such as virtual function calls whose full array of possible targets are known to be unreachable as a result of value-set analysis on the type of the callee instance.

This adds variants of the three test directories that use JBMC (cbmc-java, jbmc-strings and strings-smoke-tests) to run with --symex-driven-lazy-loading, except for the small number of tests that are expected to fail for harmless reasons, and one that is expected to fail and which may be a bug (strings-smoke-tests/java_append_char).

These were trying to match for a blank line, which doesn't occur in the output any more, and was surely not intentionally searched for in the first place. This only causes a problem under Windows (or more likely, under certain versions of Perl), probably due to a change in empty line stripping.

This can be accommodated using the same post-symex reporting phase as show-goto-functions et al. The one cbmc-java test that uses --show-properties is consequently re-enabled.

chrisr-diffblue

Reviewing the parts I'm code owner for looks fine by me.

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

smowton requested review from cesaro, chrisr-diffblue, kroening, martin-cs, mgudemann, peterschrammel, tautschnig and thk123 as code owners January 19, 2018 17:08

smowton force-pushed the smowton/feature/symex-driven-program-loading branch from c263c1a to 0d54e64 Compare January 22, 2018 15:00

NathanJPhillips suggested changes Jan 30, 2018

View reviewed changes

tautschnig reviewed Feb 2, 2018

View reviewed changes

tautschnig requested changes Feb 2, 2018

View reviewed changes

martin-cs approved these changes Feb 8, 2018

View reviewed changes

smowton force-pushed the smowton/feature/symex-driven-program-loading branch from 0d54e64 to f27905a Compare February 9, 2018 16:39

tautschnig reviewed Feb 9, 2018

View reviewed changes

karkhaz mentioned this pull request Feb 13, 2018

[path explore 1/8] Tidy up symext top-level funs #1827

Merged

tautschnig mentioned this pull request Feb 13, 2018

Symex class cleanup #1833

Merged

smowton force-pushed the smowton/feature/symex-driven-program-loading branch from f27905a to 32a929a Compare February 14, 2018 18:35

This was referenced Feb 15, 2018

Prepare symex for lazy loading #1844

Merged

Add support for path exploration to CBMC/JBMC, in addition to full bounded model checking #1641

Merged

smowton force-pushed the smowton/feature/symex-driven-program-loading branch from 32a929a to 79ff2b0 Compare February 16, 2018 14:20

smowton force-pushed the smowton/feature/symex-driven-program-loading branch from 79ff2b0 to c81ac56 Compare February 16, 2018 14:29

NathanJPhillips reviewed Feb 16, 2018

View reviewed changes

tautschnig assigned smowton Feb 21, 2018

tautschnig reviewed Mar 21, 2018

View reviewed changes

thk123 reviewed Mar 21, 2018

View reviewed changes

smowton force-pushed the smowton/feature/symex-driven-program-loading branch from f8b0e9d to b6c01f7 Compare March 21, 2018 10:55

peterschrammel reviewed Mar 21, 2018

View reviewed changes

smowton force-pushed the smowton/feature/symex-driven-program-loading branch from b6c01f7 to d3f5d44 Compare March 21, 2018 16:34

smowton force-pushed the smowton/feature/symex-driven-program-loading branch from d3f5d44 to 42e8e3d Compare March 21, 2018 17:26

thk123 approved these changes Mar 21, 2018

View reviewed changes

smowton mentioned this pull request Mar 22, 2018

Clarify slightly that show-symbol-table et al are restricted to loaded symbols #1957

Merged

NathanJPhillips approved these changes Mar 22, 2018

View reviewed changes

tautschnig approved these changes Mar 22, 2018

View reviewed changes

smowton added 9 commits March 22, 2018 14:36

Remove exceptions: add per-function entry point

890b8b1

This removes high-level exception-related instructions from a single function, at the cost of some accuracy as we can no longer analyse other functions to determine whether or not they may throw, and therefore always assume they will.

Java frontend: note availability of synthetic methods

98741f9

This informs symex-driven lazy loading that certain synthetic methods can be given bodies on demand by the Java frontend, similar to how normal methods we have bytecode for are treated.

Java frontend: rename externally driven loading

8df9350

This name is more accurate, as the frontend is no longer in charge of choosing what gets loaded and why -- it just obeys convert_lazy_method requests given by the driver program.

Fix broken test descriptions

ccb2cf3

Enable show-properties with symex-driven lazy loading

953e2df

This can be accommodated using the same post-symex reporting phase as show-goto-functions et al. The one cbmc-java test that uses --show-properties is consequently re-enabled.

smowton force-pushed the smowton/feature/symex-driven-program-loading branch from 0468b0c to 953e2df Compare March 22, 2018 14:37

peterschrammel approved these changes Mar 22, 2018

View reviewed changes

chrisr-diffblue approved these changes Mar 22, 2018

View reviewed changes

smowton merged commit 7e00a30 into diffblue:develop Mar 22, 2018

smowton mentioned this pull request Mar 23, 2018

Remove exceptions pass: introduce per-function operation #1721

Closed

		@@ -147,7 +148,8 @@ class bmct:public safety_checkert
		message_handlert &_message_handler,

		@@ -1,4 +1,4 @@
		CORE
		CORE symex-driven-lazy-loading-expected-failure

JBMC: Add symex-based program loading #1759

JBMC: Add symex-based program loading #1759

Conversation

smowton commented Jan 19, 2018 • edited Loading

smowton commented Jan 19, 2018

tautschnig commented Jan 19, 2018

NathanJPhillips 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

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

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

martin-cs left a comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

smowton commented Feb 9, 2018

smowton commented Feb 9, 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

smowton commented Feb 14, 2018

smowton commented Feb 16, 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

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

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

smowton commented Mar 21, 2018

thk123 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

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

smowton commented Jan 19, 2018 •

edited

Loading