Make convert_java_nondet more general #2505

owen-mc-diffblue · 2018-07-02T15:48:51Z

Currently, convert_nondet only converts nondets that are on the
right hand side of assignments. This is fine if the remove_returns
pass has been run. However, if the remove_returns pass has not
been run then there are also nondets in return statements.

This PR makes convert_nondet consider all operands of all
statements. It has unit tests.

thk123 · 2018-07-02T16:31:58Z

Not reviewed or anything, but a cursory glance suggests this needs a pointer bump before merging, but you probably knew that already :)

owen-mc-diffblue · 2018-07-03T06:20:23Z

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

smowton · 2018-07-03T08:59:17Z

jbmc/src/java_bytecode/convert_java_nondet.cpp

+    const typet &type = side_effect.type();
+    // If the lhs type doesn't have a subtype then I guess it's primitive and
+    // we want to bail out now
+    if(!(type.id() == ID_pointer && type.has_subtype()))


This check is redundant: a pointer_typet is a type_with_subtypet

smowton · 2018-07-03T08:59:49Z

jbmc/src/java_bytecode/convert_java_nondet.cpp

-  {
-    return next_instr;
-  }
+    // Although, if the type is a ptr-to-void then we also want to bail


Might as well update this comment to note that function pointers are also left alone

smowton · 2018-07-03T09:01:12Z

jbmc/src/java_bytecode/convert_java_nondet.cpp

+
+    // Insert the new instructions into the instruction list before target
+    goto_program.destructive_insert(target, new_instructions);
+    goto_program.update();


The update() procedure is quite expensive, so best done en masse after all replacements. The one caveat: instructions won't necessarily have a reasonable location_number before update() is run, but this pass does not appear to use location_number.

smowton · 2018-07-03T09:01:25Z

jbmc/unit/java_bytecode/java_replace_nondet/replace_nondet.cpp

+void validate_nondets_converted(
+  std::list<goto_programt::instructiont> instructions)
+{
+  bool nondetExists = false, allocateExists = false;


smowton · 2018-07-03T09:03:20Z

jbmc/unit/java_bytecode/java_replace_nondet/replace_nondet.cpp

+
+    std::stringstream out;
+    goto_function.body.output(namespacet(symbol_table), "", out);
+    std::string res = out.str();


Is this debugging code accidentally left in?

smowton · 2018-07-03T09:04:06Z

jbmc/unit/java_bytecode/java_replace_nondet/replace_nondet.cpp

+    std::string output = "";
+    for(auto instruction : model_function.get_goto_function().body.instructions)
+    {
+      output += instruction.code.pretty(0, 0) + "\n\n\n";


Similarly debug code here

allredj

Passed Diffblue compatibility checks (cbmc commit: 283c4f8).
Build URL: https://travis-ci.com/diffblue/test-gen/builds/78082033

owen-mc-diffblue · 2018-07-04T15:48:59Z

CI is now passing, and the TG bump is passing too.

@smowton I've addressed your review comments.

smowton

Looks good, one recommended further optimisation

smowton · 2018-07-04T20:47:24Z

jbmc/src/java_bytecode/convert_java_nondet.cpp

@@ -134,6 +163,8 @@ void convert_nondet(
      object_factory_parameters,
      mode);
  }
+
+  goto_program.update();


Only do this if any change was made

allredj

Passed Diffblue compatibility checks (cbmc commit: d05d8f9).
Build URL: https://travis-ci.com/diffblue/test-gen/builds/78159655

thk123

Think the body of the main loop is a bit complex TBH. I'm also a little confused about the unit tests

thk123 · 2018-07-05T10:36:20Z

jbmc/src/java_bytecode/convert_java_nondet.cpp

  {
-    return next_instr;
-  }
+    if(op.id() != ID_side_effect)


You might consider first std::copy_if and then looping over the remainder to split out the statements you don't care about from what you are doing with them.

thk123 · 2018-07-05T10:37:50Z

jbmc/src/java_bytecode/convert_java_nondet.cpp

+      continue;
+    }
+
+    // Check whether the nondet object may be null


This comment doesn't really add anything, might be more useful to say why you set max_nonnull_tree_depth to 1 if it is nullable (the question I really have is, are we setting it to 1 when previously zero, or 1 when previously >1? And if the later, why not leave it as greater than 1?

I don't know why - I'm just copying code that was there before. I guess this is now the expected behaviour.

thk123 · 2018-07-05T10:38:24Z

jbmc/src/java_bytecode/convert_java_nondet.cpp

+    // Get the symbol to nondet-init
+    const auto source_loc = target->source_location;
+
+    // Create aux symbol for nondet object


Don't think this comment really adds anything - perhaps "for storing the nondet object" might be useful?

thk123 · 2018-07-05T10:39:52Z

jbmc/src/java_bytecode/convert_java_nondet.cpp

+      aux_block, symbol_table, aux_instructions, message_handler, mode);
+    CHECK_RETURN(aux_instructions.instructions.size() == 2);
+
+    // Generate nondet init code


Again - don't think this adds anything on top of the call to gen_nondet_init

thk123 · 2018-07-05T10:41:27Z

jbmc/src/java_bytecode/convert_java_nondet.cpp

+      init_code,
+      symbol_table,
+      source_loc,
+      true,


A nice way of simulating named parameters here would be to assign this variable to a value immediately before the call:

const bool skip_classid = true

which of course begs the question, why is this true?

I'm not sure - I'm copying code that was here already.

thk123 · 2018-07-05T10:57:34Z

jbmc/unit/java_bytecode/java_replace_nondet/replace_nondet.cpp

+  {
+    replace_java_nondet(model_function);
+
+    remove_returns(model_function, [](const irep_idt &) { return false; });


The THEN says when remove_returns hasn't been called, but you're calling it?

I have changed the text to make it clear it's about "before" or "after" remove_returns is run.

thk123 · 2018-07-05T11:01:05Z

jbmc/unit/java_bytecode/java_replace_nondet/replace_nondet.cpp

+
+    convert_nondet(model_function, null_message_handler, params, ID_java);
+
+    remove_returns(model_function, [](const irep_idt &) { return false; });


Shouldn't this happen first? (before replace and convert)

You're right - this seems to be a copy-paste error :(

thk123 · 2018-07-05T11:01:23Z

jbmc/unit/java_bytecode/java_replace_nondet/replace_nondet.cpp

+
+    remove_returns(model_function, [](const irep_idt &) { return false; });
+
+    std::stringstream out;


Left over debug code?

thk123 · 2018-07-05T11:01:42Z

jbmc/unit/java_bytecode/java_replace_nondet/replace_nondet.cpp

  {
    replace_java_nondet(model_function);

+    convert_nondet(model_function, null_message_handler, params, ID_java);
+
    remove_returns(model_function, [](const irep_idt &) { return false; });


Still called despite text in THEN

I have changed the text to make it clear it's about "before" or "after" remove_returns is run.

thk123 · 2018-07-05T11:02:21Z

jbmc/unit/java_bytecode/java_replace_nondet/replace_nondet.cpp

+  }
+
+  REQUIRE(!nondet_exists);
+  REQUIRE(allocate_exists);


Might be good to validate the type of the allocation as well

Good suggestion - I will consider it in future, but I'd rather it didn't hold up this PR

allredj

Passed Diffblue compatibility checks (cbmc commit: ad06cf5).
Build URL: https://travis-ci.com/diffblue/test-gen/builds/78202562

allredj

Passed Diffblue compatibility checks (cbmc commit: ad06cf5).
Build URL: https://travis-ci.com/diffblue/test-gen/builds/78204235

owen-mc-diffblue · 2018-07-06T13:58:31Z

@thk123 Please re-review

allredj

Passed Diffblue compatibility checks (cbmc commit: bda76be).
Build URL: https://travis-ci.com/diffblue/test-gen/builds/78306527

owen-mc-diffblue · 2018-07-06T16:14:48Z

The TG bump is failing

allredj

This PR failed Diffblue compatibility checks (cbmc commit: 8522f9a).
Build URL: https://travis-ci.com/diffblue/test-gen/builds/78357054
Status will be re-evaluated on next push.
Please contact @peterschrammel, @thk123, or @allredj for support.

Common spurious failures:

the cbmc commit has disappeared in the mean time (e.g. in a force-push)
the author is not in the list of contributors (e.g. first-time contributors).

allredj

Passed Diffblue compatibility checks (cbmc commit: 1b7cfe9).
Build URL: https://travis-ci.com/diffblue/test-gen/builds/78357206

owen-mc-diffblue · 2018-07-08T06:39:33Z

I've rebased and the TG bump is passing.

NathanJPhillips · 2018-07-10T15:59:02Z

jbmc/src/java_bytecode/convert_java_nondet.cpp

-  // Return if the rhs of the assignment isn't a side effect expression
-  const auto &assign=to_code_assign(target->code);
-  if(assign.rhs().id()!=ID_side_effect)
+  // We only expect to find nondets in the rhs of an assignments or in return


This comment misleads me into believing you're doing something specific to these instructions types.

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

jbmc/src/java_bytecode/convert_java_nondet.cpp

-  {
-    return next_instr;
-  }
+    const auto &nondet_expr = to_side_effect_expr_nondet(op);


Use the generic try_cast thing above instead of can_cast/to_expr?

It's a little more complicated because side_effect_expr_nondet is distinguished by its id and its tag. At the least I'd have to create a new specialisation.

NathanJPhillips · 2018-07-10T16:01:58Z

jbmc/src/java_bytecode/convert_java_nondet.cpp

-  {
-    return next_instr;
-  }
+    // If the lhs type doesn't have a subtype then I guess it's primitive and


lhs -> expression

NathanJPhillips · 2018-07-10T16:09:36Z

jbmc/src/java_bytecode/convert_java_nondet.cpp

-      instruction_iterator!=end;)
+  bool changed = false;
+  auto instruction_iterator = goto_program.instructions.begin();
+  auto end = goto_program.instructions.end();


These hand-optimisations can actually make things worse. Leave end in the comparison below. There are Stack Overflow articles about this.

NathanJPhillips · 2018-07-10T16:11:18Z

jbmc/src/java_bytecode/convert_java_nondet.cpp

+      source_loc,
+      ID_java,
+      symbol_table);
+    aux_symbol.is_static_lifetime = false;


Is this not the default? (just asking the question - I don't know)

NathanJPhillips · 2018-07-10T16:15:41Z

jbmc/src/java_bytecode/convert_java_nondet.cpp

+    const goto_programt::targett target2 = std::next(target);
+
+    code_blockt gen_nondet_init_code;
+    const bool skip_classid = true;


Why this change?

Previously we were just passing true as an argument. I made the change to make it clearer what the argument represents.

Yuk! I'd strongly advise against adopting this style unless your caller needs a reference (which is what I assumed at first). Use a comment after the argument instead.

NathanJPhillips · 2018-07-10T16:16:57Z

jbmc/unit/java_bytecode/java_replace_nondet/replace_nondet.cpp

+         : inst.is_return() ? to_code_return(inst.code).return_value()
+                            : inst.code);
+
+    if(target_expression.id() == ID_side_effect)


Candidate for try_cast thing again?

NathanJPhillips · 2018-07-10T16:19:48Z

jbmc/unit/java_bytecode/java_replace_nondet/replace_nondet.cpp

  THEN(
-    "Code should work when remove returns is called before "
-    "replace_java_nondet.")
+    "Replace and convert nondet should work after remove returns has been "


Bit concerned that we never test that validate_nondets_converted fails if we don't call convert_nondet at all. That would require restructuring it to return nondet_exists though.

thk123

Yup looks much better - would still prefer the "filter" part of the loop to be pulled out. I also think breaking up the code gen and splicing (which though 1000x simpler is still a little fiddly). By which I mean bundle up the gen_nondet_init and goto_convert calls to return a goto_programt so that all you do in your loop body looks like:

if(!is_nondet_pointer)
  continue;

goto_programt replacement_code = gen_replacement...?
goto_program.insert_before_swap(target, declaration)
goto_program.destructive_insert(target, replacement_code);
goto_program.insert_after(target, dead)

I don't think I've got that quite right but that's the structure I'd like. Not really blocking at this stage, but still personally find the code a little fiddly to wrap my head round.

thk123 · 2018-07-11T09:28:16Z

jbmc/src/java_bytecode/convert_java_nondet.cpp

  {
-    return next_instr;
-  }
+    if(!can_cast_expr<side_effect_expr_nondett>(op))


Thought we'd agreed to try to reduce length of loop by pulling out a simple function is_nondet_pointer?

thk123 · 2018-07-11T12:48:46Z

jbmc/src/java_bytecode/convert_java_nondet.cpp

+    dead_aux_symbol->code = code_deadt(aux_symbol_expr);
+    dead_aux_symbol->source_location = source_loc;
+
+    // Insert an instruction declaring `aux_symbol` before `target`, being


Nit: add the decl before adding the dead, (don't think it makes any different since target remains unmoved after each op?)

Nope. After goto_program.insert_before_swap(target, decl_aux_symbol);, target points to the decl_aux_symbol and std::next(target) points to what target used to point to. This is because what we actually do is put decl_aux_symbol in a new instruction after target and then swap the contents of target and std::next(target).

However, I think I can make it a bit simpler.

thk123 · 2018-07-11T12:49:12Z

jbmc/src/java_bytecode/convert_java_nondet.cpp

+    goto_program.insert_before_swap(target, decl_aux_symbol);
+
+    // Keep track of the new location of the original instruction.
+    const goto_programt::targett target2 = std::next(target);


Can we come up with a better name original_instruction?

instruction containing op?

thk123 · 2018-07-11T12:50:23Z

jbmc/unit/java_bytecode/java_replace_nondet/replace_nondet.cpp

+  REQUIRE_FALSE(nondet_exists);
+  REQUIRE(allocate_exists);
+}
+#include<iostream>


Debug includes? In any case should be at the top of the file (but probably deleted)

thk123 · 2018-07-11T12:54:13Z

jbmc/src/java_bytecode/convert_java_nondet.cpp

+    goto_programt::instructiont decl_aux_symbol(DECL);
+    decl_aux_symbol.code = code_declt(aux_symbol_expr);
+    decl_aux_symbol.source_location = source_loc;
+    goto_program.insert_before_swap(target, decl_aux_symbol);


My reading of the docs for this method is it destroys the original instruction, which I think is what you want, but on the next line you say std::next(target) is the location of the original instruction, but I think this is not right?

The docs aren't very clear - they mean that it destroys the second argument passed to it, which is fine as we never use decl_aux_symbol again.

thk123 · 2018-07-11T13:00:33Z

jbmc/src/java_bytecode/convert_java_nondet.cpp

+
+    // Insert an instruction declaring `aux_symbol` before `target`, being
+    // careful to preserve jumps to `target`
+    goto_programt::instructiont decl_aux_symbol(DECL);


Use make_decl(code_declt{aux_symbol_expr}) - not idea as you still need to set the source location manually, but I really dislike the pattern of create then mutate

thk123 · 2018-07-11T13:02:45Z

jbmc/src/java_bytecode/convert_java_nondet.cpp

+
+    // It is simplest to insert the final instruction first, before everything
+    // gets moved around
+    goto_programt::targett dead_aux_symbol = goto_program.insert_after(target);


Not really an improvement in this case, but might make it easier to improve in future, if you first build the instructiont (using make_dead followed by a bunch of mutating statements. and then use goto_program.insert_after urgh you can't construct the instruction then insert_after feel free to ignore as out of scope, but the ability to insert_after(target, instruction) might be a nice way to reduce the size of this

Well, you could create make_dead and call insert_after(target).swap(make_dead). However, the way I've done it seems to be consistent with the way it's done everywhere else insert_after is used.

allredj

This PR failed Diffblue compatibility checks (cbmc commit: cc46781).
Build URL: https://travis-ci.com/diffblue/test-gen/builds/78809166
Status will be re-evaluated on next push.
Please contact @peterschrammel, @thk123, or @allredj for support.

Common spurious failures:

the cbmc commit has disappeared in the mean time (e.g. in a force-push)
the author is not in the list of contributors (e.g. first-time contributors).

allredj

This PR failed Diffblue compatibility checks (cbmc commit: 623410e).
Build URL: https://travis-ci.com/diffblue/test-gen/builds/78815298
Status will be re-evaluated on next push.
Please contact @peterschrammel, @thk123, or @allredj for support.

Common spurious failures:

the cbmc commit has disappeared in the mean time (e.g. in a force-push)
the author is not in the list of contributors (e.g. first-time contributors).

allredj

This PR failed Diffblue compatibility checks (cbmc commit: 3d39655).
Build URL: https://travis-ci.com/diffblue/test-gen/builds/78815148
Status will be re-evaluated on next push.
Please contact @peterschrammel, @thk123, or @allredj for support.

Common spurious failures:

the cbmc commit has disappeared in the mean time (e.g. in a force-push)
the author is not in the list of contributors (e.g. first-time contributors).

thk123

Thanks for all your improvements on this 💯

thk123 · 2018-07-12T14:51:06Z

jbmc/src/java_bytecode/convert_java_nondet.cpp

@@ -22,90 +22,140 @@ Author: Reuben Thomas, [email protected]

 #include "java_object_factory.h" // gen_nondet_init

+/// Return whether `expr` is a nondet pointer that we should convert


Define here what nondet pointers should be converted (and why?).

/// Returns true if `expr` is a nondet pointer that isn't a function pointer or a void* pointer /// as these can be meaningfully non-det initalized.

thk123 · 2018-07-12T14:51:44Z

jbmc/src/java_bytecode/convert_java_nondet.cpp

+
+/// Populate `instructions` with goto instructions to nondet init
+/// `aux_symbol_expr`
+static void get_gen_nondet_init_instructions(


Nit: Prefer returning the instructions rather than passing in by reference

owen-mc-diffblue · 2018-07-13T08:41:25Z

@thk123 I've updated those things, squashed all my commits and rebased to the current location of the cbmc pointer in TG. I've updated the TG bump.

allredj

This PR failed Diffblue compatibility checks (cbmc commit: 6d9e805).
Build URL: https://travis-ci.com/diffblue/test-gen/builds/78911263
Status will be re-evaluated on next push.
Please contact @peterschrammel, @thk123, or @allredj for support.

Common spurious failures:

the cbmc commit has disappeared in the mean time (e.g. in a force-push)
the author is not in the list of contributors (e.g. first-time contributors).

NathanJPhillips · 2018-07-13T10:25:59Z

jbmc/src/java_bytecode/convert_java_nondet.cpp

-      instruction_iterator!=end;)
+  bool changed = false;
+  auto instruction_iterator = goto_program.instructions.begin();
+


Random blank line!

NathanJPhillips · 2018-07-13T10:27:34Z

jbmc/src/java_bytecode/convert_java_nondet.cpp

+    const goto_programt::targett target2 = std::next(target);
+
+    code_blockt gen_nondet_init_code;
+    const bool skip_classid = true;


Yuk! I'd strongly advise against adopting this style unless your caller needs a reference (which is what I assumed at first). Use a comment after the argument instead.

NathanJPhillips · 2018-07-13T10:33:00Z

jbmc/src/java_bytecode/convert_java_nondet.cpp

+  // and we do not want to convert it. If the type is a ptr-to-void or a
+  // function pointer then we also do not want to convert it.
+  const typet &type = expr.type();
+  const bool non_void_non_function_pointer = type.id() == ID_pointer &&


If you want to break this into a separate test then it would be more conventional to do an if(!cond1) return false; return cond2;

NathanJPhillips · 2018-07-13T10:33:57Z

jbmc/src/java_bytecode/convert_java_nondet.cpp

+  const bool non_void_non_function_pointer = type.id() == ID_pointer &&
+                                             type.subtype().id() != ID_empty &&
+                                             type.subtype().id() != ID_code;
+  return can_cast_expr<side_effect_expr_nondett>(expr) &&


Unless you take the advice above then reversing the order of these would be more efficient as && short-circuits.

NathanJPhillips · 2018-07-13T10:35:10Z

jbmc/src/java_bytecode/convert_java_nondet.cpp

+    gen_nondet_init_code,
+    symbol_table,
+    source_loc,
+    skip_classid,


As suggested in comment above true, // Skip class ID

NathanJPhillips · 2018-07-13T10:42:13Z

jbmc/unit/java_bytecode/java_replace_nondet/replace_nondet.cpp

+    exprt target_expression =
+      (inst.is_assign()
+         ? to_code_assign(inst.code).rhs()
+         : inst.is_return() ? to_code_return(inst.code).return_value()


Sometimes I hate clang format. But well done using it.

…/make-linter-happier Fix whitespace errors and a typo from #2505

54f3731 Merge pull request diffblue#2610 from smowton/smowton/fix/ssa-trace-unreachable-values 6397f62 Merge pull request diffblue#2626 from qaphla/local_bitvector_analysis_fix 0c0e288 Merge pull request diffblue#2423 from tautschnig/vs-negation e90b61b Transform float_utils unit test to use CATCH and enable it 8b2bd7b Convert to signed type to make negation meaningful 7823d9c Merge pull request diffblue#2606 from diffblue/ms_cl_options 0f60b26 Merge pull request diffblue#2627 from diffblue/cleanup-ansi-c-scanner f33459f Merge pull request diffblue#2529 from tautschnig/debian1 1927fb2 remove bitvector and bitvector_u rules 1e07546 Fixed secondary issues arising from local_bitvector_analysis fix. 131e525 Fixed a bug in local_bitvector_analysis wherein an expression's ID was used in place of the expression's type's ID. 501546a SSA trace: don't concretise steps that will subsequently be dropped 709b45f Merge pull request diffblue#2591 from allredj/log-suffix-in-testpl f3630f0 Merge pull request diffblue#2612 from svorenova/multidim_arrays_tg3821_util c010edb Merge pull request diffblue#2623 from diffblue/cbmc-empty-message d5adef5 Merge pull request diffblue#2624 from diffblue/va_arg_mode 3e3303d symbols for va_args need a mode 398dd39 cbmc: avoid an empty message during result reporting 8bca5cd Merge pull request diffblue#2585 from smowton/smowton/admin/java-clean-deref-tests a0e339d Disable broken string test d0cf433 Strengthen local_safe_pointers to handle common Java operations e7b1a8a Merge pull request diffblue#2616 from smowton/smowton/admin/ai-unit-test 738ecad Merge pull request diffblue#2621 from diffblue/amazon-linux-instructions 4156283 Add test for ait framework 08bd1a8 Merge pull request diffblue#2596 from martin-cs/feature/context-sensitive-ait-merge-1 c572866 Use can_cast_type instead of raw type id check a1ab7a6 Improve documentation for java array types 745670b instructions for Amazon Linux 299417b Merge pull request diffblue#2614 from chrisr-diffblue/is_zero_bitfield_support 0c8eff6 Merge pull request diffblue#2598 from mmuesly/feature_posix_memalign fad7735 Merge pull request diffblue#2613 from NathanJPhillips/cleanup/irep_ids-def-not-h e34fc57 Merge pull request diffblue#2600 from peterschrammel/doxygen-graphviz 54cc818 clang-format fixups 9986ea1 Make exprt::is_zero() support bitfields dbf4384 Merge pull request diffblue#2605 from NathanJPhillips/feature/cast-for-code_typet 7798aaa Updated comment for the fact that IDs are defined in def files now b72b968 Remove unused function e66f76f Add a check functions for (multi-dimensional) array types f4f4190 Added can_cast_type implementation for code_typet f6c34f2 Merge pull request diffblue#2603 from smowton/smowton/fix/stub-string-lengths 9c9c375 two further Visual Studio CL options 05bebb7 Merge pull request diffblue#2595 from thk123/doc/use-can-cast 9a75c65 Merge pull request diffblue#2597 from allredj/update-jbmc-gitignore c98688b Fix stub string lengths 819560f Merge pull request diffblue#2601 from owen-jones-diffblue/owen-jones-diffblue/update-codeowners-3 39323e0 Remove code owners from low-risk files 8f8052a Make directories match from root 1a36a21 Install graphviz for doxygen job on travis 3e0b2a5 Doxygen the comments describing the abstract domain interface. 4f8d445 Upgrade from a warning in the comments to a protected constructor. 2b9c880 Clang format the domain files. 028d8b6 Add a method to convert the domain to a predicate to the basic domain API. 918e947 Expand the comments describing the base domain interface. f60027b Move the interface of domains to it's own header file. 15aa61f Adding support for posix_memalign from the stdlib in c. ba01589 Add guidelines for using irepts in the code base 37fc4e6 Update jbmc gitignore ec79bdd Merge pull request diffblue#2385 from polgreen/aggressive_slicer_v2 78b7119 Merge pull request diffblue#2491 from diffblue/std_code_constructors a99c4ff Merge pull request diffblue#2497 from diffblue/simplify_byte_extract_fix 8c7dc17 make comment // not /* ea085d3 move aggressive slicer options into macro aa4848d Apply clang format to includes in goto_instrument_parse_options 4ac9199 Aggressive slicer 2954205 aggressive slicer regression tests de7e1af call graph helper functions 357358d remove mistake in grapht c7457fb Merge pull request diffblue#2543 from tautschnig/vs-unsigned-byte-swap 0e72433 Merge pull request diffblue#2516 from polgreen/cbmc_trace_options 2e90035 Merge pull request diffblue#2590 from peterschrammel/use-proper-irep-ids a354235 Merge pull request diffblue#2592 from NathanJPhillips/cleanup/fix-typo-in-comment 59b1a9e Fix a small typo in a comment that I happened to come across 282468c Print log suffix when running tests c98c9df Merge branch 'develop' into cbmc_trace_options 12e970b Use irep ids for #comments 569c854 Merge pull request diffblue#2489 from diffblue/fix-empty-indexset 993735b Merge pull request diffblue#2507 from mgudemann/bugfix/java/keep-typecasts-on-stack a63212e Add regression test for stack variables with typecasts 6f63050 Simplify stack element replacement loop 731c69e Keep expressions unchanged when adding temporary variables d10e44d Merge pull request diffblue#2586 from hannes-steffenhagen-diffblue/fix-json_unit_test 8d6bfdd Merge pull request diffblue#2575 from nmanthey/upstream-ls_parse 2d14b22 Merge pull request diffblue#2545 from tautschnig/vs-unnecessary ff0414e Merge pull request diffblue#2546 from tautschnig/vs-wmm-int ed48122 Make json parser unit tests independent of working directory 14dc11e Merge pull request diffblue#2495 from diffblue/aws-codebuild-windows-jbmc-tests cefdc21 Merge pull request diffblue#2579 from peterschrammel/clean-up-java-options 64a63a0 Merge pull request diffblue#2584 from diffblue/fp-constant-folding 44cfeb9 Clean up redundant specification of CBMC option 38fe61e Trim JBMC help text width to 80 chars 080fc91 Break overlong lines in help text ebae090 Deactivate smt1 option in JBMC 04fcc5b Check that string options are used with strings turned on 0520732 Use default options in JBMC e4cfb04 Remove built-in-assertions option from JBMC 0d924ce Remove error-label option from JBMC 35f69f0 Remove GOTO_CHECK options from JBMC 86d4fec Remove --refine-strings from tests 7ef8a0e Remove obsolete string-max-length option e5e5e9e remove unneeded NOLINT 9449ac7 Encapsulate constraints for equals d74672b Use const references in string_constraintt fdf14f5 Add invariants on the sign of string_constraintt bounds 16052f8 Move string_constraintt constructor to cpp f01c03c Fix string_constraintt bound values 8edc5ee C front-end: constant folding for floating-point f795ef9 Remove trailing newlines that trip up regex on Windows 53d24e5 the jbmc tests now work on Windows f9c5faf adjust_float_expressions can now take a rounding mode argument 6ccce5b Merge pull request diffblue#2521 from svorenova/array_element_type_util 201ba8c Merge pull request diffblue#2581 from romainbrenguier/refactor/to_code e4b8c44 Clean-up in gen_nondet_instruction_info bb7ea78 Merge pull request diffblue#2528 from tautschnig/dev-null f10badb Add functions to retrieve a reference to the java array element type 7f8b2be Merge pull request diffblue#2582 from jeannielynnmoulton/jeannie/parse-bridge-flag-for-thk123 1f62596 Clean-up get_return_lhs 8966f09 Merge pull request diffblue#2560 from tautschnig/force-inline cb587a9 Adding unit test for checking bridge methods attribute is parsed correctly efadba2 Read the bride flag for methods 26781a6 Remove unnecessary cast to_code a18b32d Merge pull request diffblue#2571 from jeannielynnmoulton/jeannie/InnerClassAccessibility c959c3f Tests get_outer_class with deeply nested classes. 8201c19 Parse and capture outer class for inner classes. 87c2a68 Merge pull request diffblue#2577 from owen-jones-diffblue/owen-jones-diffblue/make-linter-happier a1b9e07 Fix whitespace errors and a typo from diffblue#2505 45eae64 Merge pull request diffblue#2505 from owen-jones-diffblue/owen-jones-diffblue/fix/convert-nondet 6d9e805 Make convert_java_nondet more general 70887e2 Merge pull request diffblue#2564 from tautschnig/vs-java-parse-tree 6c5ecec Merge pull request diffblue#2570 from johnnonweiler/doc-git-submodule-update d5ea306 ls_parse: improve debugging by printing a trace 17bc726 ls_parse: Allow handling unknown blocks aad1692 Add minisat download to jbmc/README.md f7ddb02 Remove --recursive from git submodule update 206f7fb Include submodule update in jbmc/README.md d5f3c32 Fix a typo JMBC->JBMC b5075d7 Document git submodule update in COMPILING.md 9b9aecf Remove unused macro BUFSIZE 0146874 Make all unicode operations use native endianness 8d93087 Move unicode unit test to CATCH and enable it 680227e Explicit unsigned -> uint16_t casts to avoid conversion warnings ea9dc15 goto-gcc: run original compiler even when output is /dev/null 0a990ef Do not (unnecessarily) require preprocessing for fixed 32/64 bit regression tests 0c15fed Cleanup java_bytecode_parse_treet: all members are public, no virtual tables required 36d13f7 Support Visual Studio's __forceinline 5953f6a goto-instrument/wmm: explicit conversion of bool to 0/1 6dc6ea9 Avoid unncessary signed/unsigned conversion 081f743 use proper constructor for code_assertt 8e44191 use proper constructor for code_expressiont 47f5405 use proper constructor for side_effect_expr_function_callt bf02ec7 use proper constructor for code_declt 9fa0733 use proper constructor for codet dbbd568 mark various 'partial constructors' as deprecated, and introduce complete ones 180e066 add option to show code in CBMC trace 4fbc10d Add option to show function calls and returns in CBMC trace f532b4b allow unsigned long instead of unsigned in regression test for hex_trace 94cacc6 represent numerical values in CBMC trace in hex fc4aab3 avoid non-termination of simplify_exprt::simplify_byte_extract when given array_of git-subtree-dir: cbmc git-subtree-split: 54f3731

owen-mc-diffblue requested review from cesaro, mgudemann, peterschrammel, smowton and thk123 as code owners July 2, 2018 15:48

thk123 added the do not merge label Jul 2, 2018

smowton reviewed Jul 3, 2018

View reviewed changes

owen-mc-diffblue force-pushed the owen-jones-diffblue/fix/convert-nondet branch 2 times, most recently from f567784 to 283c4f8 Compare July 4, 2018 10:33

allredj reviewed Jul 4, 2018

View reviewed changes

smowton approved these changes Jul 4, 2018

View reviewed changes

owen-mc-diffblue force-pushed the owen-jones-diffblue/fix/convert-nondet branch 2 times, most recently from 94e15b6 to d05d8f9 Compare July 5, 2018 09:13

allredj reviewed Jul 5, 2018

View reviewed changes

thk123 reviewed Jul 5, 2018

View reviewed changes

allredj reviewed Jul 5, 2018

View reviewed changes

owen-mc-diffblue requested review from cristina-david, NathanJPhillips, pkesseli and a team as code owners July 6, 2018 13:54

owen-mc-diffblue requested a review from thk123 July 6, 2018 13:58

allredj reviewed Jul 6, 2018

View reviewed changes

owen-mc-diffblue force-pushed the owen-jones-diffblue/fix/convert-nondet branch 2 times, most recently from 8522f9a to 1b7cfe9 Compare July 7, 2018 07:43

allredj reviewed Jul 7, 2018

View reviewed changes

NathanJPhillips suggested changes Jul 10, 2018

View reviewed changes

thk123 approved these changes Jul 11, 2018

View reviewed changes

thk123 removed the do not merge label Jul 11, 2018

allredj reviewed Jul 12, 2018

View reviewed changes

owen-mc-diffblue force-pushed the owen-jones-diffblue/fix/convert-nondet branch 2 times, most recently from 623410e to 3d39655 Compare July 12, 2018 12:28

allredj reviewed Jul 12, 2018

View reviewed changes

thk123 approved these changes Jul 12, 2018

View reviewed changes

Make convert_java_nondet more general

6d9e805

owen-mc-diffblue force-pushed the owen-jones-diffblue/fix/convert-nondet branch from 3d39655 to 6d9e805 Compare July 13, 2018 08:38

allredj reviewed Jul 13, 2018

View reviewed changes

NathanJPhillips reviewed Jul 13, 2018

View reviewed changes

NathanJPhillips approved these changes Jul 13, 2018

View reviewed changes

owen-mc-diffblue merged commit 45eae64 into diffblue:develop Jul 13, 2018

owen-mc-diffblue deleted the owen-jones-diffblue/fix/convert-nondet branch July 13, 2018 10:55

owen-mc-diffblue pushed a commit to owen-mc-diffblue/cbmc that referenced this pull request Jul 13, 2018

Fix whitespace errors and a typo from diffblue#2505

a1b9e07

smowton added a commit that referenced this pull request Jul 13, 2018

Merge pull request #2577 from owen-jones-diffblue/owen-jones-diffblue…

87c2a68

…/make-linter-happier Fix whitespace errors and a typo from #2505


		convert_nondet(model_function, null_message_handler, params, ID_java);

		remove_returns(model_function, [](const irep_idt &) { return false; });


		remove_returns(model_function, [](const irep_idt &) { return false; });

		std::stringstream out;

		@@ -22,90 +22,140 @@ Author: Reuben Thomas, [email protected]

		#include "java_object_factory.h" // gen_nondet_init

		/// Return whether `expr` is a nondet pointer that we should convert

Make convert_java_nondet more general #2505

Make convert_java_nondet more general #2505

Conversation

owen-mc-diffblue commented Jul 2, 2018

thk123 commented Jul 2, 2018

owen-mc-diffblue commented Jul 3, 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

allredj left a comment

Choose a reason for hiding this comment

owen-mc-diffblue commented Jul 4, 2018

smowton left a comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

allredj left a comment

Choose a reason for hiding this comment

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

owen-mc-diffblue Jul 5, 2018 • edited Loading

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

allredj left a comment

Choose a reason for hiding this comment

allredj left a comment

Choose a reason for hiding this comment

owen-mc-diffblue commented Jul 6, 2018

allredj left a comment

Choose a reason for hiding this comment

owen-mc-diffblue commented Jul 6, 2018

allredj left a comment

Choose a reason for hiding this comment

allredj left a comment

Choose a reason for hiding this comment

owen-mc-diffblue commented Jul 8, 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

NathanJPhillips Jul 13, 2018 • edited Loading

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

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

owen-mc-diffblue Jul 12, 2018 • edited Loading

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

allredj left a comment

Choose a reason for hiding this comment

owen-mc-diffblue Jul 5, 2018 •

edited

Loading

NathanJPhillips Jul 13, 2018 •

edited

Loading

owen-mc-diffblue Jul 12, 2018 •

edited

Loading

NathanJPhillips Jul 13, 2018 •

edited

Loading