Aggressive slicer v2 #2385

polgreen · 2018-06-21T12:14:07Z

This is a new version of #1587

It is dependent on:
#2381
#2369

The aggressive slicer by default removes function bodies of any functions not on the shortest path on the call graph between the start function and the property. If no property is specified, it will preseve the shortest path for each property. It is parameterisable:

--call-depth " preserves all functions within function calls of the shorets path " --preserve-function forces the aggressive slicer to preserve function
--preserve-function containing force the aggressive slicer to preserve all functions with names containing
--preserve-all-direct-paths force the aggressive slicer to preserve all functions on direct paths to the property. This option must be used with a specified property.

The aggressive slicer is designed to be used in conjunction with CBMC inbuilt features to block functions and to replace function bodies with approximations.

The results are not sound, it may produce spurious traces, due to over-approximating the removed function bodies, and it may miss traces due to the removed function bodies writing to global variables, or if "preserve-all-direct-paths" is not used. However, it is designed for use with code bases that are far too big to otherwise use cbmc on.

The parameterisation is intended to be used as a means of providing engineer feedback.

allredj

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

smowton

Just realised I've also commented on the dependent PRs here. Hopefully this is useful anyhow.

Major things:

Comments on tests indicating their intent
depth_limited_search could be much simpler

Otherwise minor comments

smowton · 2018-06-23T12:44:55Z

regression/goto-instrument/aggressive_slicer1/main.c

+  	D();
+}
+
+void B() 


So my guess is we'll fail to reach D because only the B -> C -> D path is actually feasible, but it isn't the shortest path to D? If so note that as a comment in either the test or the .desc file

I can't find any other regression tests with documentation; can you point me to an example?

regression/contracts/function_apply_01/ or indeed all of them in regression/contracts/ have info, in those cases both in the C source and the test.desc file.

Example syntax:

CORE PrimaryArg otherarg1 otherarg2 regex that must match another that must match -- regex that must not match another that must not match -- comments go here, below the second -- delimiter comments continue on subsequent lines.

Alternatively comment in the .c file for the regression test

smowton · 2018-06-23T12:47:17Z

regression/goto-instrument/aggressive_slicer5/main.c

+  __CPROVER_assert(0,"");
+}
+
+void C()


I think aggressive_slicer5 is missing a .desc file

smowton · 2018-06-23T12:47:44Z

regression/goto-instrument/aggressive_slicer5/main.c

@@ -0,0 +1,29 @@
+void D()


Similarly for the rest of these tests -- briefly comment stating the intent of the test, either in the source or the desc file

smowton · 2018-06-23T12:48:42Z

regression/goto-instrument/aggressive_slicer6/main.c

@@ -0,0 +1,29 @@
+void D()


Consider adding a test case with more than one property, so specifying a property makes a difference?

smowton · 2018-06-23T12:49:44Z

src/goto-instrument/aggressive_slicer.cpp

+ * aggressive_slicer.cpp
+ *
+ *  Created on: 18 Jun 2018
+ *      Author: polgreen


Author lines should give an email

smowton · 2018-06-23T13:21:45Z

src/util/graph.h

+{
+  PRECONDITION(nodes.size() < std::numeric_limits<std::size_t>::max());
+
+  if(limit <= 0)


std::size_t is unsigned, so == 0

smowton · 2018-06-23T13:29:42Z

src/util/graph.h

+std::vector<typename N::node_indext> grapht<N>::depth_limited_search(
+  const std::vector<node_indext> &src,
+  std::size_t &limit,
+  std::vector<bool> &visited,


How about making this a std::set<node_indext> &, then while the membership test would be a little more expensive than a vector<bool> you could use it as the result, rather than copying the result after each recursive call. The function would look something like

depth_limited_search(node_indext from, std::size_t steps, std::set<node_indext> &result) { for(const auto o : nodes[from].out) if(result.insert(o.first).second) depth_limited_search(o.first, steps - 1, result); }

smowton · 2018-06-23T13:30:23Z

src/util/graph.h

+/// should be performed.
+template <class N>
+std::vector<typename N::node_indext> grapht<N>::depth_limited_search(
+  const std::vector<node_indext> &src,


This would be much simpler if it worked over single sources rather lists-of-sources

Yes it would. I wrote the function to work with a vector of sources to be consistent with grapht::get_reachable, which has a function for a vector of sources and one for a single source. I don't know when you would want to do reachability from multiple sources, but given that is an option, it seems nicely symmetric to also have an option to do depth-limited reachability from multiple sources.

Sure, but the multi-source one can just be a wrapper, like

std::set<irep_idt> depth_limited_search( const std::vector<node_indext> &srcs, size_t depth) { std::set<irep_idt> result; for(const node_indext src : srcs) depth_limited_search(src, result, depth); return result; }

As discussed with @polgreen out-of-band: This doesn't quite work, you need to maintain a collection of nodes visited along some path, or else capture in some other way what your exploration frontier is. For example, a graph with nodes {a,b,c,d} and edges a->b->c, a->c->d must yield "d" for depth 2 even though "c" is already seen on one path.

Argh, true, sorry. Would breadth-first search do the trick?

Re BFS: I think you get in trouble whenever you use an implementation that uses recursion, because you need to communicate the depth of when you have seen a node across invocations.

I used BFS last time I implemented this, and, if I recall correctly, @smowton reviewed it and said that I should switch it to DFS in order to use more efficient containers.

(The way to do it with BFS is to mark the end of each frontier with some specific node index, I think I used numeric_limits::max)

I wasn't gunning for DFS in particular, I was trying to eliminate the copying of the results or frontier vector at each recursive call. However I've clearly made far more mess than is justified here, so I'll butt out.

The BFS implementation didn't involve recursion and copying, just a for loop. But it didn't use vectors, it used a stack.

Either way, I'd prefer it if we just stuck with one version now so that I can redo all my changes on top of that. it's easier for me to revert to the DFS version, since the BFS version was based on the old call graph class so I would pretty much have to rewrite it.

Oh I see, I thought you were referring to the review a few days ago, not a really old one

smowton · 2018-06-23T13:33:58Z

unit/analyses/disconnect_unreachable_nodes_in_graph.cpp

+#include <goto-programs/goto_convert_functions.h>
+
+static symbolt
+create_void_function_symbol(const irep_idt &name, const codet &code)


If these are being duplicated, suggest putting them in unit/call_graph_test_utils.h or something like that

smowton · 2018-06-23T13:41:31Z

src/util/graph.h

+    else if(i == reachable[reachable_idx])
+      reachable_idx++;
+    else if(i > reachable[reachable_idx])
+      throw "error disconnecting unreachable nodes";


This is an invariant rather than a throw, as it's a programming mistake rather than a user error / bad input

polgreen · 2018-06-25T13:04:43Z

changes done

tautschnig · 2018-06-25T13:19:02Z

I'll merge #2381 once CI passes so that this PR is reduced to a unique set of commits once rebased.

allredj

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

polgreen · 2018-06-28T08:12:53Z

this is now rebased

polgreen · 2018-06-29T09:43:30Z

Are there any further changes needed on this? I've incorporated all the changes requested above

polgreen · 2018-07-02T06:49:46Z

I've made all the changes requested on this and rebased it; are there any further changes required?

tautschnig

I seems I never found the time to complete this review: some nitpicks below.

tautschnig · 2018-06-28T09:13:45Z

regression/goto-instrument/aggressive_slicer1/test.desc

+^SIGNAL=0$
+^VERIFICATION SUCCESSFUL$
+--
+^warning: ignoring


Nit pick: github reminds us that there is no newline at the end of the file.

tautschnig · 2018-06-28T09:13:59Z

regression/goto-instrument/aggressive_slicer2/test.desc

+^SIGNAL=0$
+^VERIFICATION SUCCESSFUL$
+--
+^warning: ignoring


Missing newline

tautschnig · 2018-06-28T09:14:09Z

regression/goto-instrument/aggressive_slicer3/test.desc

+^SIGNAL=0$
+^VERIFICATION FAILED$
+--
+^warning: ignoring


Missing newline

tautschnig · 2018-06-28T09:14:18Z

regression/goto-instrument/aggressive_slicer4/test.desc

+^SIGNAL=0$
+^VERIFICATION FAILED$
+--
+^warning: ignoring


Missing newline

tautschnig · 2018-06-28T09:14:30Z

regression/goto-instrument/aggressive_slicer5/test.desc

+^SIGNAL=0$
+^VERIFICATION FAILED$
+--
+^warning: ignoring


Missing newline

tautschnig · 2018-06-28T09:14:39Z

regression/goto-instrument/aggressive_slicer6/test.desc

+^SIGNAL=0$
+^VERIFICATION FAILED$
+--
+^warning: ignoring


Missing newline

tautschnig · 2018-06-28T09:14:47Z

regression/goto-instrument/aggressive_slicer7/test.desc

+^SIGNAL=0$
+^VERIFICATION FAILED$
+--
+^warning: ignoring


Missing newline

tautschnig · 2018-07-02T17:17:48Z

src/goto-instrument/aggressive_slicer.cpp

+#include <goto-programs/show_properties.h>
+#include <util/message.h>
+
+void aggressive_slicert::note_functions_to_keep(irep_idt destination_function)


Pass by (const) reference.

polgreen · 2018-07-03T08:33:12Z

Changes made

allredj

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

allredj

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

polgreen · 2018-07-06T05:39:48Z

The tests pass on this, and the changes requested have all been made, is there anything else that needs doing?

It appears to have requested additional reviewers because I applied clang-format to goto_instrument_parse_options.cpp. I only applied the clang-format patch that was provided by the CI. I've left it in a separate commit because it is pretty unrelated to anything in this PR, but it is also necessary to get this PR to pass all the CI.

polgreen · 2018-07-23T08:31:45Z

Are there any additional changes required to this PR? If not, is there a reason it hasn't been merged?

martin-cs

A few things it would be good for you to look at but I'm not going to request this be held / re-reviewed once you've had a look at them.

martin-cs · 2018-07-23T13:39:34Z

src/analyses/call_graph_helpers.cpp

  std::set<irep_idt> result;
+  std::vector<std::size_t> start_indices;


This looks a little like an inconsistency when updating. Where the two PRs that this depended on changed and this undoes some of the changes?

One of the PRs that this depends on ended up in a mess, because I did a major requested change, then did some minor changes on top of that, and then had to reverse the major change. And so there are some bits and pieces that have ended up in this PR that shouldn't be, like passing std::size_t by reference. Those changes are deliberate.

Switching the order of start_indices and result is unintentional though, I've reversed that now

Thanks. I appreciate that some of this is a bit pedantic and my thanks for your patience. I just want to avoid getting into a fix / undo because PR raced with fix / fix loop.

I think @martin-cs' comment should be addressed.

martin-cs · 2018-07-23T13:41:04Z

src/util/graph.h

-    const node_indext &src,
-    std::size_t &limit,
-    bool forwards) const;
-


Why is this a mistake? Is there a body that needs removal as well?

No, the mistake is that the body was already removed

OK. In future it would be nice to have that in a commit message.

It would be good to amend the commit message according to @martin-cs' comment.

martin-cs · 2018-07-23T13:42:04Z

src/goto-instrument/aggressive_slicer.h

+  /// slicer, i.e., shortest path between two functions, or all direct paths.
+  /// Inserts functions to preserve into the functions_to_keep set
+  /// \param destination_function name of destination function for slice
+  void note_functions_to_keep(const irep_idt &destination_function);


Wow! Actual useful documentation!

martin-cs · 2018-07-23T13:43:25Z

src/goto-instrument/goto_instrument_parse_options.h

+  "(aggressive-slice-call-depth):" \
+  "(aggressive-slice-preserve-function):" \
+  "(aggressive-slice-preserve-functions-containing):" \
+  "(aggressive-slice-preserve-all-direct-paths)" \


The prevalent trend for these seems to be as an OPT_ macro, along with the coresponding help macro.

I think this comment should be addressed.

peterschrammel · 2018-07-23T21:31:23Z

src/util/graph.h

-    const node_indext &src,
-    std::size_t &limit,
-    bool forwards) const;
-


It would be good to amend the commit message according to @martin-cs' comment.

peterschrammel · 2018-07-23T21:34:08Z

regression/goto-instrument/aggressive_slicer5/test.desc

@@ -0,0 +1,8 @@
+CORE
+main.c


The file aggressive_slicer5/test.binary must not be committed.

peterschrammel · 2018-07-23T21:37:51Z

src/goto-instrument/goto_instrument_parse_options.cpp

+      aggressive_slicer.call_depth =
+        safe_string2unsigned(cmdline.get_value("aggressive-slice-call-depth"));
+
+    if(cmdline.isset("aggressive-slice-preserve-function"))


I don't quite understand the use of having this option plus aggressive-slice-preserve-functions-containing. Why not allow a regex to specify what should be preserved?

It could be done with a regex, I didn't need the full capabilities of regex though and found this easier to work with.

I'm saying that there are standard ways of specifying name filtering (wild cards, Regex). 'contains name snippet' is not among these and may confuse users. Using regexes would even save you a couple of lines in the implementation.

peterschrammel · 2018-07-23T21:38:38Z

src/goto-instrument/aggressive_slicer.h

+      goto_model(_goto_model),
+      message_handler(_msg)
+  {
+    start_function = goto_model.goto_functions.entry_point();


Not sure why this needs to be stored, and if necessary, make it const.

it's being used multiple times, so seemed better to store it than to call goto_model.goto_functions.entry_point() multiple times

peterschrammel · 2018-07-23T21:39:23Z

src/goto-instrument/aggressive_slicer.h

+      functions_to_keep.insert(f);
+  };
+
+  std::list<std::string> user_specified_properties;


Why are these public?

these are written to in goto_instrument_parse_options.cpp

peterschrammel · 2018-07-23T21:39:54Z

src/goto-instrument/aggressive_slicer.h

+      message_handler(_msg)
+  {
+    start_function = goto_model.goto_functions.entry_point();
+    call_depth = 0;


prefer assignment at declaration or in initializer

peterschrammel · 2018-07-23T21:40:20Z

src/goto-instrument/aggressive_slicer.h

+  bool preserve_all_direct_paths;
+
+private:
+  irep_idt start_function;


remove or make const

peterschrammel · 2018-07-23T21:40:31Z

src/goto-instrument/aggressive_slicer.h

+  void get_all_functions_containing_properties();
+};
+
+#endif /* CPROVER_GOTO_INSTRUMENT_AGGRESSIVE_SLICER_H  */


Use // comments

peterschrammel · 2018-07-23T21:41:21Z

src/goto-instrument/goto_instrument_parse_options.h

+  "(aggressive-slice-call-depth):" \
+  "(aggressive-slice-preserve-function):" \
+  "(aggressive-slice-preserve-functions-containing):" \
+  "(aggressive-slice-preserve-all-direct-paths)" \


I think this comment should be addressed.

peterschrammel · 2018-07-23T21:42:03Z

src/analyses/call_graph_helpers.cpp

  std::set<irep_idt> result;
+  std::vector<std::size_t> start_indices;


I think @martin-cs' comment should be addressed.

allredj

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

Function declaration exists but there is no body. Removing function declaration

polgreen · 2018-07-24T08:49:17Z

I've made the changes except the regex, which would be an extension of the functionality of this PR. Pending the CI, please could this be merged?

allredj

This PR failed Diffblue compatibility checks (cbmc commit: 8c7dc17).
Build URL: https://travis-ci.com/diffblue/test-gen/builds/79824378
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).

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

polgreen requested review from chrisr-diffblue, kroening, martin-cs, peterschrammel, smowton, tautschnig and thk123 as code owners June 21, 2018 12:14

polgreen force-pushed the aggressive_slicer_v2 branch from 59c3680 to 5dcb64a Compare June 21, 2018 12:21

allredj reviewed Jun 21, 2018

View reviewed changes

smowton reviewed Jun 23, 2018

View reviewed changes

smowton mentioned this pull request Jun 23, 2018

Depth limited search #2381

Merged

polgreen force-pushed the aggressive_slicer_v2 branch from 5dcb64a to 199caf6 Compare June 25, 2018 13:04

polgreen force-pushed the aggressive_slicer_v2 branch 5 times, most recently from 7df8d4e to f35cc0c Compare June 27, 2018 08:10

allredj reviewed Jun 27, 2018

View reviewed changes

tautschnig reviewed Jul 2, 2018

View reviewed changes

polgreen force-pushed the aggressive_slicer_v2 branch from f35cc0c to 23b005c Compare July 3, 2018 07:08

allredj reviewed Jul 3, 2018

View reviewed changes

polgreen force-pushed the aggressive_slicer_v2 branch 2 times, most recently from 9498579 to 2ac2a74 Compare July 5, 2018 10:04

polgreen requested review from cesaro and mgudemann as code owners July 5, 2018 10:04

polgreen force-pushed the aggressive_slicer_v2 branch from 2ac2a74 to c456098 Compare July 5, 2018 10:11

allredj reviewed Jul 5, 2018

View reviewed changes

kroening approved these changes Jul 23, 2018

View reviewed changes

martin-cs approved these changes Jul 23, 2018

View reviewed changes

polgreen force-pushed the aggressive_slicer_v2 branch from c456098 to 7be6f99 Compare July 23, 2018 13:58

peterschrammel reviewed Jul 23, 2018

View reviewed changes

peterschrammel assigned polgreen Jul 23, 2018

allredj reviewed Jul 23, 2018

View reviewed changes

polgreen force-pushed the aggressive_slicer_v2 branch from 7be6f99 to 5109c48 Compare July 24, 2018 08:47

polgreen added 7 commits July 24, 2018 10:48

remove mistake in grapht

357358d

Function declaration exists but there is no body. Removing function declaration

call graph helper functions

de7e1af

aggressive slicer regression tests

2954205

Aggressive slicer

4ac9199

Apply clang format to includes in goto_instrument_parse_options

aa4848d

move aggressive slicer options into macro

ea085d3

make comment // not /*

8c7dc17

polgreen force-pushed the aggressive_slicer_v2 branch from 5109c48 to 8c7dc17 Compare July 24, 2018 08:48

allredj reviewed Jul 24, 2018

View reviewed changes

kroening merged commit ec79bdd into diffblue:develop Jul 24, 2018

		std::set<irep_idt> result;
		std::vector<std::size_t> start_indices;

		@@ -0,0 +1,8 @@
		CORE
		main.c

Aggressive slicer v2 #2385

Aggressive slicer v2 #2385

Conversation

polgreen commented Jun 21, 2018

allredj left a comment

Choose a reason for hiding this comment

smowton 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

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

polgreen commented Jun 25, 2018

tautschnig commented Jun 25, 2018

allredj left a comment

Choose a reason for hiding this comment

polgreen commented Jun 28, 2018

polgreen commented Jun 29, 2018

polgreen commented Jul 2, 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

polgreen commented Jul 3, 2018

allredj left a comment

Choose a reason for hiding this comment

allredj left a comment

Choose a reason for hiding this comment

polgreen commented Jul 6, 2018

polgreen commented Jul 23, 2018

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

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