JBMC: Remove-returns per function #1730

smowton · 2018-01-12T11:05:30Z

Another day, another pass converted to per-function operation. This one is really quite awkward, though: remove-returns transforms x = f(); into f(); x = f#return_value;, and doing this function-by-function with other passes interleaved necessarily introduces some discord when a caller that hasn't been converted deals with a callee that has, or vice versa.

I've had a stab at a least-bad solution, and come up with:

When a given function is being remove-return'd, alter its own return statements and its callsites to expect remove-return style, creating #return_value variables on demand.
Do not alter the function's type, in the symbol table or the goto function map, so that other functions that must create callsites treat it as if it had its "real" return type. For example, the string solver will special-case functions that it expects to return String-related types, and become confused if they have been voided.
Any passes that run after remove-returns risk becoming confused as the function's type indicates it returns conventionally, but in fact it routes its return values via #return_value. However such a pass would normally assume all functions are void-typed in any case.

In summary, remove-returns is a really messy pass. The "proper" solution would be to separate the notions of return type and result type, and always use the latter plus a "get result" function that hides whether a function is in conventional or via-global style. However I suspect attempting to implement that now would be a fool's errand.

smowton · 2018-01-12T11:09:11Z

Test-gen bump: https://github.com/diffblue/test-gen/pull/1364

tautschnig · 2018-01-12T11:18:01Z

Could you please clarify what the first commit is supposed to achieve on its own? Only the second commit has a detailed commit message, yet is somewhat confusing as it heavily touches remove_returns once again.

tautschnig · 2018-01-12T11:33:30Z

Do not alter the function's type, in the symbol table or the goto function map, so that other functions that must create callsites treat it as if it had its "real" return type. For example, the string solver will special-case functions that it expects to return String-related types, and become confused if they have been voided.

I don't yet buy this one: my approach would have been to alter the type of a function f once done with all rewriting in f. There would of course be inconsistencies if not all available bodies in a goto_functionst had been converted, but that should be a transient state (and I don't think that's the one you are concerned about here).

If the string solver expects some functions to always have non-void return types, then the string solver needs to be fixed -- it should be able to handle the two cases (1) has a non-void return type and (2) has void type -> look at x#return_value.

Surely I'm missing something, so why is it that the string solver can't be fixed?

smowton · 2018-01-12T13:14:59Z

@tautschnig fixed the commits; the first one was supposed to do the real work, and the second one activate it in jbmc.

The string solver can be fixed, but my concern is any frontend pass that happens to examine the type of another function, e.g. to generate a call sequence, will need to be taught about remove_returns too. I think it will be better for the front-end to be able to ignore the existence of remove-returns (even though it would find out about it if it inspected the other function's body) and have to possibly teach passes that run after remove-returns to assume functions are void-typed, rather than the reverse.

I can also run a whole-program-level cleanup pass that makes the type void so everything is consistent then -- thus only passes that run during the loading process will need to care about the distinction.

tautschnig · 2018-01-12T13:31:48Z

[...] frontend pass that happens to examine the type of another function, e.g. to generate a call sequence, [...]

Would you have a concrete example of such a pass? The notion of "frontend" isn't perfectly clear to me here (I would not consider any analysis running on goto programs a "frontend" type pass anymore as, to me, the transition from codet to goto_programt is the step where we leave the front end).

smowton · 2018-01-12T13:35:38Z

The string solver is the only one I know about so far. The plan here is for symex to load functions on demand, so in practice, briefly defining "front-end" as anything that sees the code before loading is finished, the front-end will constitute everything from java-bytecode-convert-method through to the solver. Everything in java_bytecode_languaget and goto_convert is currently expecting conventional returns, and everything after process_goto_functions is currently expecting remove-returns style, or can tolerate both styles, so it's a question of which batch you'd rather fix. I favoured the later stages because things that expect remove-returns are very likely already ignoring the return type declared in the symbol table since it's meaningless, whereas earlier stages can reasonably expect the symbol table to truthfully reflect the return type.

tautschnig · 2018-01-12T13:52:44Z

Just had some out-of-band sync, @smowton will post updates.

smowton · 2018-01-12T13:54:12Z

Going to try the approach where we do alter the types in remove-returns just as in the whole-program case, but teach the Java frontend and related passes not to assume the symbol table is accurate, but rather to always use get_original_return_type or some close relative thereof that patches over the differences between conventional and removed-return style.

smowton · 2018-01-12T16:47:22Z

@tautschnig updated this to your design idea; in fact it turned out the string solver doesn't inspect other functions' types; rather it was failing because string-related functions can initially be created as stubs, and then later provided with a body. I worked around this by having java_bytecode_convert_method check whether that is the case before annotating a stub, also providing a hook for driver programs that supply their own stubs. If there's demand that can be generalised to allow the driver to supply a lambda, but I expect the manner in which stub bodies are supplied will be amended before then anyhow, as it would simplify lazy loading if they were "right first time", rather than being post-hoc fixed up.

Long story short, remove-returns now edits types just like the whole-program pass, and it appears that the frontend components are not perturbed, at least in the tests supplied with jbmc and deeptest. Please re-review.

tautschnig

I think this is ok, but it's too late to call this a serious review.

tautschnig · 2018-01-12T17:07:48Z

src/goto-programs/remove_returns.cpp

@@ -194,11 +219,45 @@ void remove_returnst::operator()(goto_functionst &goto_functions)
 {
  Forall_goto_functions(it, goto_functions)
  {
-    replace_returns(it);
-    do_function_calls(goto_functions, it->second.body);
+    auto function_is_stub = [&goto_functions](const irep_idt &function_id) {


NOLINT needed

tautschnig · 2018-01-12T17:07:56Z

src/goto-programs/remove_returns.cpp

+  if(goto_function.body.empty())
+    return;
+
+  auto function_is_stub = [&symbol_table](const irep_idt &function_id) {


NOLINT needed

tautschnig · 2018-01-12T21:20:02Z

src/java_bytecode/java_entry_point.cpp

+    // Consider some sort of annotation indicating a global variable that
+    // doesn't require initialisation?
+    return !has_suffix(id2string(sym.name), RETURN_VALUE_SUFFIX);
+  }


Is this necessary? The annotation you could use is marking it extern, which will avoid such initialisation in the C front-end. That might work for Java as well, because Java would not be using is_extern natively, I believe?

Disinclined to abuse the flag so, since I am providing a definition of the symbol, it just doesn't need start-of-day initialisation because we know it is always written before reading

It just strikes me as something very magical, and very much of unclear value. I accept that it may not be necessary to do the initialisation, but is it really that much harm?

At the moment at least with a largeish JAR available you'd get thousands of lines of __CPROVER_initialize that you didn't need, and therefore thousands of lines of state in goto-symex. Still, would it make you happier to invent a special value (no_initialisation_required_exprt?) that makes this clearer?

Ok, I get that this may yield many avoidable instructions. What makes me unhappy is this special casing and dependency of otherwise completely unrelated bits of code.

What about renaming the is_extern flag and making it no longer C-specific? It could be do_not_initialize?

Don't want to rename it, but I'll gladly add an extra flag.

That would impact (de)serialisation of goto binaries, so take extra care!

Argh, then I won't. A comment on the type seems like the least invasive solution in that case.

You might just want to tell me to shut up and go with your existing solution plus a TODO saying that a different approach would fall into the class of #1148 :-)

Nah that's okay, a type-comment (AKA an annotation, but that's an extra symbol field (which is a #1148 matter)) is strictly nicer than what I have now. I'll make a new version of this shortly, as the is-a-stub-callsite thing should be solved better anyhow.

tautschnig · 2018-01-12T21:23:13Z

src/java_bytecode/java_bytecode_convert_method.cpp

+        if((!driver_program_provides_stubs) &&
+           (!string_preprocess.implements_function(id)))
+        {
+          symbol.type.set(ID_C_incomplete, ID_1);


Use true instead of ID_1. The right thing will happen.

tautschnig · 2018-01-12T21:24:40Z

src/goto-programs/remove_returns.cpp

+/// the function being altered *and* any callees.
+///
+/// Unlike the whole-model version of remove-returns, this will *not* alter the
+/// function's return type, because other passes are likely to use that


Is this comment still accurate?

smowton · 2018-01-15T12:37:01Z

@tautschnig comments applied except for is_extern, which I am disinclined to use since it would misrepresent the linkage status of those variables.

smowton · 2018-01-15T17:21:41Z

@peterschrammel I suspect this is one you ought to review? Or possibly @cesaro?

peterschrammel · 2018-01-15T21:29:41Z

src/goto-programs/remove_returns.cpp

+  new_symbol.mode = function_symbol.mode;
+  // If we're creating this for the first time, the target function cannot have
+  // been remove_return'd yet, so this will still be the "true" return type:
+  new_symbol.type = return_type;


Ideally, we should have a consistency check function that could be used to add a debug-mode invariant whether a function has been remove_return'd or not. (Not TBD in this PR, but a note for future hardening of goto passes.)

peterschrammel · 2018-01-15T21:39:02Z

src/goto-programs/remove_returns.cpp

-        i_it->code=assignment;
-      }
+      // now turn the `return' into `assignment'
+      i_it->type=ASSIGN;


use i_it->make_assignment(assignment)

peterschrammel · 2018-01-15T21:54:38Z

src/java_bytecode/java_bytecode_convert_method_class.h

@@ -81,6 +83,10 @@ class java_bytecode_convert_methodt:public messaget
  /// Initialized in `convert`.
  unsigned slots_for_parameters;

+  /// True if the driver program will provide bodies for all stub functions;
+  /// will be used to annotate stubs created upon discovery of a callsite.
+  bool driver_program_provides_stubs;


Is there a use case for this?

Test-gen acts this way: stub functions are given a body shortly after creation.

Trying to understand how this will fit with the discussions around #1585 in the end...

At the moment if you (the driver program) have a non-default plan for stubs, you should set this parameter. For example, test-gen derives from java_bytecode_languaget in order to make similar customisations, and will set this once this change hits CBMC.

Later I would like for stubbing to take place via a standard callback provided by languaget, such that the driver program supplies an implementation there instead of customising the language frontend. There could be standard implementations (replace with assume-false, add a Java-style nondet-object-graph stub, ...), or the driver could do something cleverer.

I have no idea about urgencies, but really I'd want to see this addressed before merging this PR (knowing that this blocks a series of other PRs). My problem with the chosen approach is that function_is_stub is a piece of configuration information, yet is never documented as such in, e.g., the symbol table. That is, the semantics of the program depend on function_is_stub, but there is no way to recover from one choice or the other.

There is an ugly option of delaying things until symbolic execution, which would figure out that no function definition is present, and thus create an assignment to the return-value variable instead (where the communication that a return value is required is implicit via the existence of the return-value symbol). The advantage is that goto programs can be changed up to the very last moment.

The proposed "standard callback" solution seems preferable, but is possibly more work. Indeed the discussion in #1585 should be driven to a conclusion.

So this actually isn't quite the same as the please-provide-a-stub callback, rather the question is, of a function that has not yet been loaded, will a body ever be provided? Therefore I propose for this PR I'll implement function_will_have_body, a callback provided by the driver program (jbmc will check language_filest::lazy_method_map to determine this, test-gen will always answer yes). That will remove the need for annotation on stub creation as is happening in this PR.

The provide-stub-body callback is an entirely separate matter, and should be pursued independently.

smowton · 2018-01-16T10:52:57Z

@peterschrammel done one of your changes, replied to the other.

smowton · 2018-01-19T18:20:26Z

@tautschnig made both these updates:

Can-produce-function is now a property of lazy_goto_modelt that is routed through to remove_returns, so it can do the right thing without needing the frontend to correctly guess whether a stub will remain or be populated later on
#remove_return variables that don't need initialisation now communicate this fact with an annotation (comment tagged onto their type) rather than the frontends having to encode that knowledge.

smowton · 2018-01-23T11:17:33Z

@tautschnig @peterschrammel Travis failure is only on Mac builds cancelled due to problems at their end; this is ready for re-review.

peterschrammel

Looks good apart from some methods not having doxygen yet.

peterschrammel · 2018-01-23T12:02:21Z

src/goto-programs/remove_returns.cpp

-        i_it->code=assignment;
-      }
+      // now turn the `return' into `assignment'
+      i_it->make_assignment();


There's a make_assignment variant that takes a codet.

tautschnig · 2018-01-23T12:51:13Z

I have restarted the Mac builds: https://www.traviscistatus.com/ suggests that even the Mac side of the house should be back.

tautschnig · 2018-01-23T12:52:49Z

src/goto-programs/lazy_goto_functions_map.h

@@ -99,6 +99,11 @@ class lazy_goto_functions_mapt final
    return ensure_function_loaded_internal(name).second;
  }

+  bool can_produce_function(const key_type &name) const


Needs documentation.

tautschnig · 2018-01-23T12:53:58Z

src/goto-programs/lazy_goto_model.h

@@ -15,11 +15,18 @@
 class cmdlinet;
 class optionst;

+/// Interface
+struct can_produce_functiont


Interface to ... what?

tautschnig · 2018-01-23T12:54:41Z

src/goto-programs/lazy_goto_model.h

 /// Model that holds partially loaded map of functions
-class lazy_goto_modelt
+class lazy_goto_modelt : public can_produce_functiont


I don't know what a can_produce_functiont is supposed to be, hence I can't judge whether this is-a relation is justified.

See new docs on the interface

Thanks a lot for the clarification!

tautschnig · 2018-01-23T12:57:10Z

src/goto-programs/remove_returns.cpp

@@ -46,74 +51,91 @@ class remove_returnst
  void undo_function_calls(
    goto_functionst &goto_functions,
    goto_programt &goto_program);
+
+  symbol_exprt get_or_create_return_value_symbol(const irep_idt &function_id);


For future reference: it would have been nice to place the refactoring (which is where this function came about) in a separate commit. I believe this refactoring is a big improvement, but also it caused the biggest code churn here.

tautschnig · 2018-01-23T13:00:28Z

src/goto-programs/remove_returns.cpp

+  new_symbol.type = return_type;
+  // Return-value symbols will always be written before they are read, so there
+  // is no need for __CPROVER_initialize to do anything:
+  new_symbol.type.set(ID_C_no_initialization_required, true);


I know I should have commented on this days ago, but anyway: I like the idea, but would feel the .value field is a better place for that than the .type? It's not a property that is tied to the type, is it? I'm also saying this as the type continues to exist (that very same irept can be shared across all the instantiations), while the value will be overwritten anyway.

Neither is ideal -- really I want a map<irep_idt, irept> attributes defined for each symbol and GOTO function, but that's a breaking change. I chose the type because I thought it less likely to get copied into a place where the annotation no longer makes sense. I also wanted this to work with symbols with value nil, and nil-with-annotation-comment seemed dubious if anyone uses full_eq to compare them. However I can switch it if you prefer.

Yes, one of the variants that are a breaking change is the right way to go. With that agreed, I'd think that .value is a better place for it isn't getting duplicated during symbolic execution, but for sure it's not the perfect place either. I'll leave it to you to decide, certainly not a blocker in any way.

tautschnig · 2018-01-23T13:01:58Z

src/goto-programs/remove_returns.cpp

-  typet return_type=f_it->second.type.return_type();
-
-  const irep_idt function_id=f_it->first;
+  typet return_type=function.type.return_type();


I'd suggest following clang-format's suggestions throughout this patch as at least some of the changes do use the proposed formatting.

tautschnig · 2018-01-23T13:04:48Z

src/jbmc/jbmc_parse_options.cpp

+          !available_functions.can_produce_function(id);
+      };
+
+    // remove returns


Nit pick: I don't think this comment adds value.

smowton · 2018-01-23T13:35:41Z

@tautschnig @peterschrammel changes applied.

smowton · 2018-01-23T13:39:17Z

@tautschnig I also note that traviscistatus.com reports a 1800 job backlog for OSX nodes and 180 OSX nodes total, so I'm guessing it'll be at least half a day before anything runs.

tautschnig

I'm ok with this now, with one proposed change left at @smowton's discretion.

tautschnig · 2018-01-23T13:50:37Z

src/goto-programs/lazy_goto_model.h

 /// Model that holds partially loaded map of functions
-class lazy_goto_modelt
+class lazy_goto_modelt : public can_produce_functiont


Thanks a lot for the clarification!

This converts functions from conventional to via-global-variable return style on a function-by-function basis. It results in some complication, as the globals are now seen by the language's final pass, meaning it must ignore them for initialisation purposes, and we must cope with functions not having their "true" type while other functions are still being loaded. One test in cbmc-java failed because it was written in C, which we don't adapt to support incremental loading yet, so it is moved to the cbmc test directory, where it can still achieve its goal of checking whether uncaught_exceptions_analysist can tolerate CPROVER_assert and similar builtins, since cbmc also runs the remove_exceptions pass.

smowton · 2018-01-23T15:34:09Z

Confirmed with @peterschrammel in person that he is happy, so I'll merge this once Travis is done with this and the test-gen bump.

tautschnig · 2018-01-23T16:52:12Z

I'll start reviewing the PRs based off of that one once merged and rebased. I'd appreciate a ping once that's the case.

smowton · 2018-01-23T17:18:56Z

Only OSX pending. Merging rather than wait for more merge conflicts as the OSX builds take days at the moment.

f7602af Merge commit 'bb88574aaa4043f0ebf0ad6881ccaaeb1f0413ff' into merge-develop-20180327 906aeb3 Merge pull request diffblue#349 from diffblue/owen-jones-diffblue/fix-compilation-for-release 3d8423c Merge pull request diffblue#350 from diffblue/owen-jones-diffblue/skip-duplicate-callsites-in-lazy-methods 73fb488 bugfix from upstream repo for generic crash fd76555 Speed up resolution of virtual callsites in lazy loading 3fd28f3 Replace assert(X) by UNREACHABLE/INVARIANT(X) 557158e Merge pull request diffblue#334 from diffblue/pull-support-20180216 1e48132 Merge from master, 20180216 ad7b28e Updates requsted in the PR: mostly rename 'size -> length'. e3fcb9b Introducing MAX_FILE_NAME_SIZE constant. bb88574 Merge pull request diffblue#1806 from thk123/refactor/address-review-comments-from-1796 db9c214 Merge pull request diffblue#1850 from tautschnig/include-cleanup 78fbf08 Merge pull request diffblue#1844 from smowton/smowton/feature/prepare-symex-for-lazy-loading 4098ed5 Merge pull request diffblue#1849 from smowton/smowton/cleanup/java-main-function-types 06f3e83 Use C++ headers instead of their C variants e918a91 Goto-symex: add support for general function accessor 9e31303 Symex: switch to incrementally populating address-taken locals ac5af68 Address-taken locals analysis: support incremental analysis fe775f3 Merge pull request diffblue#1843 from peterschrammel/instructions-function a6fd729 Cleanup tests with anomalous main functions 5df3fca Clean up get_function_id hacks 552b100 Set function member of each goto instruction in goto program passes 38e6e4a Merge pull request diffblue#1813 from smowton/smowton/fix/cleanup-unused-clinits 278e4e6 Merge pull request diffblue#1826 from smowton/smowton/fix/java-inherited-static-fields a2ebb33 Merge pull request diffblue#1713 from karkhaz/kk-debug-timestamps 7b5dd17 Merge pull request diffblue#1834 from diffblue/library-preconditions 1da5be1 Add tests for inherited static fields 19d622b Add tests to verify that synthetic method removal is performed adc9fd4 Java frontend: clean up unused clinit symbols f15c312 Exclude j.l.O from possible static field hosts. afa443c US spelling of initialize d4d4a9a Tolerate stub static fields defined on non-stub types 873e1f6 Guess public access for stub globals d6783d8 Java method converter: look for inherited static fields 32cc538 Insert stub static globals onto any incomplete ancestor class b2d3d61 Search static fields inherited from interfaces 045ac05 Create stub globals on the first parent incomplete class 5b3cde5 Use a common instance of class_hierarchyt in get_inherited_component e73e756 Create stub globals: check for inherited globals bea6371 Annotate static fields with accessibility 168c2a8 Generalise get_inherited_method f3160e1 resolve_concrete_function_callt -> resolve_inherited_componentt 82549de Emit timestamps on each line of output 3f6965b Replace util/timer* with std::chrono ef08ae2 Merge pull request diffblue#1820 from smowton/smowton/fix/remove-string-solver-iteration-limit 0f20482 Merge pull request diffblue#1836 from karkhaz/kk-remove-unused-lambda-capture e8105bd Merge pull request diffblue#1833 from diffblue/symex_class_cleanup f6f45fc turn some assertions in the stdlib.h models into preconditions 9ea0cc6 pre-conditions for strings fbd54df Remove unused lambda capture 9620802 Merge pull request diffblue#1815 from smowton/smowton/feature/replace-clinit-unwinder 9b59631 Merge pull request diffblue#1828 from smowton/smowton/cleanup/remove-recreate-initialize 1ac9abe Remove string refinement iteration limit c94548c preconditions for delete and delete[] 9ba7fe2 cleanup of some noise (mostly obvious declarators) in the goto_symext class bb64ea6 clean up symex_assign vs. symex_assign_rec 932a38f Merge pull request diffblue#1827 from karkhaz/kk-symex-operator-tidy 968d97e Remove __CPROVER_initialize recreation 06a220a Reimplement remove-static-init-loops to avoid need to inspect GOTO program 2bb98d9 Merge pull request diffblue#1819 from romainbrenguier/refactor/coverage-instrumentation 6492b3a Rearrange cover_basic_blocks header a9549e7 Define constants as const fa35ccd Pull continuation_of_block function out 560d712 Declare constants as const 35422f3 Make update_covered_lines a static function b4cadf8 [path explore 1/8] Tidy up symext top-level funs 0f3ae1a Make representative_inst an optional dc696a4 Make format_number_range function instead of class 678218a Merge pull request diffblue#1825 from thk123/refactor/corrected-path-of-language-file ba76a8f Merge pull request diffblue#1751 from tautschnig/fix-1748 b665269 Correcting path to a file d0889a8 Merge pull request diffblue#1822 from diffblue/legacy-language 441f706 Merge pull request diffblue#1823 from diffblue/cleanup 11714b2 use constant_exprt version of to_integer 733f3b8 remove old-style constructor for member_exprt 63f09ac remove unused function make_next_state 77c8b9c remove translation for certain boolean program constructs 1bac484 cleanout decision_proceduret::in_core d8967f5 moving language.h and language_file.h to langapi folder f9b9599 Merge pull request diffblue#1761 from diffblue/function_typet dd040e5 Added function_typet. bcd88a0 Merge pull request diffblue#1821 from smowton/smowton/feature/test-pl-tags 45f0939 test.pl: add support for tagging test-cases 40b8c03 Updates requested in PR - mainly rename of functions. 7f868e2 Reused private code in 'remove_virtual_functions.cpp' by making it public. ae6775a Merge pull request diffblue#1790 from martin-cs/fix/correct-domain-interface d7bb937 Catch the case when a GOTO instruction is effectively a SKIP. b2fba97 Correct domain transformers so that they meet the preconditions. d447c26 Document the invariants on iterators arguments to transform and merge. e3db794 Whitespace changes to keep clang-format happy. 1990994 Revert "Add edge type parameter to ai transform method" 3ca91bc Revert "Fix iterator comparison bug in reaching_definitions.cpp" ac036fd Revert "Fix iterator equality check bug in dependence_graph.cpp" 86cadcd Revert "Fix iterator equality check bug in custom_bitvector_analysis.cpp" db925de Revert "Fix iterator equality check bug in constant_propagator.cpp" 2c69364 Merge pull request diffblue#1811 from cesaro/iterator-fix 807268e Fixes the symbol_base_tablet iterator 0df054c Merge pull request diffblue#1781 from smowton/smowton/feature/java-create-stub-globals-earlier e163ab6 Java frontend: create synthetic static initialisers for stub globals fbcb423 Merge pull request diffblue#1802 from NathanJPhillips/feature/symbol_iterator e106cf8 Merge pull request diffblue#1793 from smowton/smowton/cleanup/remove-java-new-lowering-pass 52dfc36 Merge pull request diffblue#1731 from diffblue/bugfix/all_resolved_calls f123ae9 Adding comment referencing where the invariant comes from f7c89e1 Add iterator for symbol_table_baset 150f826 Merge pull request diffblue#1801 from hannes-steffenhagen-diffblue/add-idea-gitignore 745afbc Merge pull request diffblue#1796 from thk123/refactor/bytecode-parsing-tidy 6362295 Add .idea (CLion) directory to .gitignore 31da890 Revert "Do lowering of java_new as a function-level pass" 6f6fda7 Merge pull request diffblue#1794 from smowton/smowton/fix/goto-diff-test-escapes 4a538d2 Adding comments on the non-standard patternt 9bfe177 Adding an early guard for correctly parsed exception table 6fe1808 Improved error reporting on invalid constant pool index 93dab4c Escape curly braces in regexes 814cfcc Adapt failing unit test for value set analysis 3ff90bc Add unit test e67a96e Add regression test 3df5348 Adapt regression tests for virtual functions. 09efc90 Re-Resolve function calls if only java.lang.Object was found. a619e48 Merge pull request diffblue#1763 from jeannielynnmoulton/base_class_info_tg1287 0b8dd57 Merge pull request diffblue#1785 from smowton/smowton/fix/core-models-cmake-script 50dcec8 Adding unit tests for extracting generic bases' info 54df3a1 Correcting generic parameters in bases for implicitly generic classes 6d691d7 Parsing generic bases' information into the class symbol 7d041f0 Defining a new type for generic bases f10eb71 Fix Java core-models build script 8d66028 Merge pull request diffblue#1774 from smowton/smowton/feature/java-create-clinit-state-earlier 679d9b8 Java frontend: create static initialiser globals ahead of time 4a93a29 Merge pull request diffblue#1788 from smowton/smowton/fix/java_tcmp_nan 6ad8ffd Fix Java ternary-compare against NaN 1e0ac30 Turn get_may, set_may, etc into irep_ids b0cb1ee Merge pull request diffblue#1766 from smowton/smowton/feature/java-frontend-create-literal-globals-early a2e3af5 Merge pull request diffblue#1744 from smowton/smowton/feature/instrument_cover_per_function 22ae7aa Merge pull request diffblue#1637 from tautschnig/bswap a1a972f Merge pull request diffblue#1776 from smowton/smowton/feature/class-hierarchy-grapht ef3c598 Merge pull request diffblue#1775 from diffblue/refactor/set_classpath 45dd840 Merge pull request diffblue#1728 from romainbrenguier/refactor/split-axiom-vectors 8a27950 Java frontend: create String an Class literals earlier d95cb12 Move string literal initialisation into separate file 515ebdd CI lazy methods: scan global initialisers for global references cab7b52 C front-end: fix promotion order for types ranking lower than int c450328 Support for --16 on Visual Studio, no _WIN64 in 32-bit mode b2c4188 Do not use non-trivial system headers with --32 80b972b Use split_string in set_classpath fdb2ebc Merge pull request diffblue#1773 from smowton/smowton/feature/string-solver-ensure-class-graph-consistency a6eed7c Add class-hierarchy variant based on grapht 311af6d Coverage: fully support instrumenting one function at a time ceafd85 Java string solver: ensure base types are loaded 1e17db6 Merge pull request diffblue#1735 from cesaro/core-models 6844760 Merge pull request diffblue#1769 from smowton/smowton/fix/nondet-initialize-after-initialize a8e659c Fixed CMake linker ODR violations caused by a regression-test f66288b Internalize core models of the Java Class Library 34216f5 Refactor jar loading ed008f9 Add constructors for having memory-loaded jar files This allows the jar_file class to load from a buffer (c array) as opposed to a file 86a34c9 Merge pull request diffblue#1765 from smowton/smowton/fix/ci-lazy-methods-array-element-types 1e11f6d Add test for multiple array types in single method 5009cbb CI lazy methods: re-explore array types with different element types 857fcf9 Cleanup unused fields in string refinement 51d86f5 Adapt unit tests for splitted axiom vectors 1843e44 Split string generator axioms into separate vectors 5669d9b Java: run nondet-initialize method *after* initialization 0b5a5c3 Rename test case 3440018 Provide function name in goto_model_functiont f17e2c8 Merge pull request diffblue#1741 from smowton/smowton/feature/add_failed_symbols_per_function f65f0fd Merge pull request diffblue#1764 from smowton/smowton/feature/java-infer-opaque-type-fields-earlier dbc00a7 Add doxygen to add-failed-symbols 3788467 JBMC: add failed symbols on a per-function basis e934867 Provide a journalling symbol table to process-goto-function e86e2a0 Java: infer opaque type fields before method conversion f0f50e3 Journalling symbol table: enable nesting 58d5980 Merge pull request diffblue#1740 from smowton/smowton/feature/adjust_float_expressions_per_function c91ff69 JBMC: adjust float expressions per function eed983a JBMC: add property checks on a per-function basis db3bc99 JBMC: run convert-nondet on a per-function basis 99ea8fe JBMC: run replace-Java-nondet on function-by-function basis bfd4f50 Merge pull request diffblue#1730 from smowton/smowton/feature/remove_returns_per_function 96569c3 JBMC: remove return values on a per-function basis a7595c1 Remove returns: support running per-function fd6e195 Merge pull request diffblue#1718 from cesaro/concurrency-team-small-fixes e6fe617 Merge pull request diffblue#1705 from jgwilson42/goto-diff-tests 22afc5c Fixes wrong invocation order for static initializers 5c3997d Refectors how CBMC interprets a codet thread-block 001c1a2 ireps of type "ID_atomic_begin" and "ID_atomic_end" will now be properly displayed when the "show-symbol-table" flag is specified. d978ef9 Folder build/ ignored. bc145fd Merge pull request diffblue#1756 from romainbrenguier/tests/index-of-corrections#TG-2246 47b4ee9 Merge pull request diffblue#1725 from cesaro/exception-handlig-fixes d397d6a Merge pull request diffblue#1726 from diffblue/multi_ary_expr2c bd95317 Merge pull request diffblue#1753 from diffblue/xor_exprt 1d4af6d Merge pull request diffblue#1747 from NathanJPhillips/feature/upstream-cleanup 9c7debb Merge pull request diffblue#1750 from pkesseli/feature/sat-interrupt f11c995 Merge pull request diffblue#1749 from pkesseli/ci/remove-unapproved 981c8e0 Merge pull request diffblue#1743 from tautschnig/dump-c-fix bcb076b Correct tests for String.indexOf ef5c6f0 Merge pull request diffblue#1742 from owen-jones-diffblue/owen-jones-diffblue/small-shared-ptr 6c9f05e Fixes to exception handling behaviour 80dd48a added multi-ary xor_exprt 703e4a3 Remove unapproved C++11 header warning. bf7ed1a Merge pull request diffblue#313 from diffblue/owen-jones-diffblue/add-structured-lhs-to-value-set cc9398d Expose MiniSAT's `interrupt()` 8360233 Merge pull request diffblue#1646 from peterschrammel/list-goto-functions e4a2763 Tests for scope changes for variables and functions 8ee1956 goto-diff tests for package name changes ce3a5e9 Basic tests for java goto-diff 3bf9987 Compare access qualifiers in goto-diff f71cc7f Attach class name to method symbol 1f06d35 Merge pull request diffblue#312 from diffblue/pull-support-20180112 fda9daa Cleanup of create-and-swap to emplace e42e97a Merge commit '23666e3af35673c734c9816ffc131b6b9a379e86' into pull-support-20180112 53f1a41 Populate structured_lhs in all `entryt`s d7121f2 dump-c: fix support of use-system-headers eb5ec24 Merge pull request diffblue#1736 from hannes-steffenhagen-diffblue/develop_fix-bitfield-pretty-printing 7a0de46 Add comment suggested by @owen-jones-diffblue b741d4b Use small intrusive pointer in irep 434cc99 Merge pull request diffblue#1732 from peterschrammel/catch-sat-memout 8ae53bb Merge pull request diffblue#1733 from peterschrammel/mem-limit 574101c Add `structured_lhs` field to entryt 4f1a67a Uses alternatives to get_string in type2name when possible b46149d Merge pull request diffblue#1719 from smowton/smowton/cleanup/remove_exceptions_single_global 82a7ec6 Adds regression test for bitfield naming bug 651d8d1 Fixes use of wrong identifier when pretty printing bitfield types 638937a Merge pull request diffblue#1709 from romainbrenguier/doc/string-solver-intro 1d1be4c Move non-string-specific part of doc to solvers 549eb57 Delete trailing whitespaces db3e044 Add introduction to string solver documentation 74be7fb Merge pull request diffblue#1729 from romainbrenguier/refactor/unused-nonempty-option d101b22 Set memory limit utility ef45a1d Replace assertions by invariants 84e04a7 Catch Glucose::OutOfMemoryException 89fc48d Replace assertions by invariants 5e85701 Catch Minisat::OutOfMemoryException b8cee29 Enable list-goto-functions in clobber d902ec8 Replace cout by message stream in show-goto-functions d970673 Move show-loops in the right place in goto-diff e1227ef Enable list-goto-functions in goto diff 7e1110c Enable list-goto-functions in goto-instrument 0fb4868 Enable list-goto-functions in goto-analyzer e67abfa Remove exceptions: switch to single inflight exception global 2fabbd4 Enable list-goto-functions in JBMC 9e1705f Enable list-goto-functions in CBMC ebd8248 Add list-goto-functions command line option 2fe43a9 Add parameter to list goto functions without printing bodies 3d492fe Add documentation of return values 5a8eea5 Remove the string-non-empty option 9810f92 Drop string_non_empty field for string refinement fec16d7 expr2c now distinguishes binary and multi-ary expressions d16a918 C library: network byteorder functions 05bc9ed Implement bswap in SAT back-end 4f37035 Introduce bswap_exprt git-subtree-dir: cbmc git-subtree-split: f7602af

smowton requested review from cesaro, kroening, mgudemann, peterschrammel, tautschnig and thk123 as code owners January 12, 2018 11:05

smowton force-pushed the smowton/feature/remove_returns_per_function branch 3 times, most recently from f59587e to fa04804 Compare January 12, 2018 16:37

tautschnig reviewed Jan 12, 2018

View reviewed changes

smowton force-pushed the smowton/feature/remove_returns_per_function branch 2 times, most recently from 478f92f to abcf36f Compare January 15, 2018 12:36

smowton force-pushed the smowton/feature/remove_returns_per_function branch 2 times, most recently from f6b2989 to 032b299 Compare January 15, 2018 14:08

smowton mentioned this pull request Jan 15, 2018

JBMC: run replace-Java-nondet on function-by-function basis #1737

Closed

peterschrammel reviewed Jan 15, 2018

View reviewed changes

smowton force-pushed the smowton/feature/remove_returns_per_function branch from 032b299 to b1e2eea Compare January 16, 2018 10:52

smowton force-pushed the smowton/feature/remove_returns_per_function branch from b1e2eea to 43b2d6d Compare January 19, 2018 18:18

smowton force-pushed the smowton/feature/remove_returns_per_function branch 4 times, most recently from ba655c4 to 6daa808 Compare January 22, 2018 12:39

peterschrammel reviewed Jan 23, 2018

View reviewed changes

tautschnig reviewed Jan 23, 2018

View reviewed changes

smowton force-pushed the smowton/feature/remove_returns_per_function branch from 6daa808 to ce3ea29 Compare January 23, 2018 13:35

tautschnig approved these changes Jan 23, 2018

View reviewed changes

smowton added 2 commits January 23, 2018 14:22

JBMC: remove return values on a per-function basis

96569c3

smowton force-pushed the smowton/feature/remove_returns_per_function branch from ce3ea29 to 96569c3 Compare January 23, 2018 14:22

peterschrammel approved these changes Jan 23, 2018

View reviewed changes

smowton merged commit bfd4f50 into diffblue:develop Jan 23, 2018

JBMC: Remove-returns per function #1730

JBMC: Remove-returns per function #1730

Conversation

smowton commented Jan 12, 2018 • edited Loading

smowton commented Jan 12, 2018

tautschnig commented Jan 12, 2018

tautschnig commented Jan 12, 2018

smowton commented Jan 12, 2018

tautschnig commented Jan 12, 2018

smowton commented Jan 12, 2018 • edited Loading

tautschnig commented Jan 12, 2018

smowton commented Jan 12, 2018

smowton commented Jan 12, 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

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 15, 2018

smowton commented Jan 15, 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

smowton commented Jan 16, 2018

smowton commented Jan 19, 2018

smowton commented Jan 23, 2018

peterschrammel left a comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

tautschnig commented Jan 23, 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

smowton commented Jan 23, 2018

smowton commented Jan 23, 2018

tautschnig left a comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

smowton commented Jan 23, 2018

tautschnig commented Jan 23, 2018

smowton commented Jan 23, 2018

smowton commented Jan 12, 2018 •

edited

Loading

smowton commented Jan 12, 2018 •

edited

Loading