Add raw irept dump of lhs to trace #1694

NathanJPhillips · 2018-01-03T14:04:21Z

Add a command-line switch to optionally add a raw irept dump of the lhs of assignments to the trace output.
This can be used for diagnostic purposes, for an intelligent UI to display a better interpretation of traces or for post-processing of traces.

smowton

Looks good, don't use camel-case in cbmc, and please add a basic regression test or two.

smowton · 2018-01-03T15:21:38Z

src/goto-programs/json_goto_trace.cpp

@@ -29,7 +30,8 @@ Author: Daniel Kroening
 void convert(
  const namespacet &ns,
  const goto_tracet &goto_trace,
-  jsont &dest)
+  jsont &dest,
+  bool useExtendedFormat)


Underscores not camel-case

smowton · 2018-01-03T15:23:04Z

src/goto-programs/json_goto_trace.h

@@ -21,6 +21,7 @@ Date: November 2005
 void convert(
  const namespacet &,
  const goto_tracet &,
-  jsont &);
+  jsont &,
+  bool useExtendedFormat = false);


allredj

I don't have much to say about the implementation, but I have two general remarks:

Could you please add a rationale for that change (at least in the commit or the PR description)? Is it for debug purposes or is this something that we want to use in the product?
Could we extend the "--trace" option instead of adding an entirely new option (there's already a lot of them)? I can't think of a case where we would use the --extended-trace option without the --trace option.

NathanJPhillips · 2018-01-03T16:45:10Z

@allredj - apparently we can't keep the current --trace and also support --trace=extended, which would be nice, I agree.
I've added some possible rationales in the description, though the use-cases this is being written for are actually company-specific so not relevant to the open-source product.

allredj · 2018-01-03T17:51:29Z

@NathanJPhillips Thanks for the rationale. Pity we can't improve the option. The code looks fine to me but I don't know this part well enough to judge of its sanity, so I'll leave that unapproved.

tautschnig · 2018-01-03T18:24:33Z

Please synchronise with #1565.

tautschnig · 2018-01-03T18:26:51Z

I've added some possible rationales in the description, though the use-cases this is being written for are actually company-specific so not relevant to the open-source product.

Could the information please be included in the commit messages? https://chris.beams.io/posts/git-commit/ - thanks.

NathanJPhillips · 2018-01-04T17:46:47Z

Please synchronise with #1565.

Does this mean this PR is effectively blocked for now?

tautschnig · 2018-01-04T17:54:38Z

Does this mean this PR is effectively blocked for now?

Why would that be the case? You're free to engage on #1565 in any way you feel is appropriate, and if @polgreen happens to be unavailable then you can just pick up her commits. (I think that sort of engagement should actually have happened well before posting this PR, TBH.)

polgreen · 2018-01-05T09:15:33Z

I can make some time to resurrect that PR. The thing i probably don't have time to do is integrating the trace output changes into jbmc (smowton has an outline of how to do it in the PR). I can address the other comments.

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

@tautschnig as far as I can tell there's no dependency between the two PRs, except to use a matching naming convention for the command-line options. @polgreen has e.g. --trace-hex, which seems reasonable -- @NathanJPhillips should perhaps therefore use --trace-json-extended for consistency. Otherwise I think they are independent functional additions and it should not matter which goes in first.

tautschnig · 2018-01-05T11:42:09Z

@tautschnig as far as I can tell there's no dependency between the two PRs, except to use a matching naming convention for the command-line options.

I had't claimed there was any dependency. But, as you say, matching naming conventions would be a good start. The second step would be synchronising those additional options across cbmc/jbmc front-ends (each of the two PRs does only one of them).

NathanJPhillips · 2018-01-05T14:18:44Z

This PR now covers CBMC and JBMC and has the facility to be extended with more options.

NathanJPhillips · 2018-01-05T15:05:32Z

Basic regression tests added as per request by @smowton

smowton · 2018-01-05T15:06:33Z

@tautschnig OK for this to go in?

tautschnig · 2018-01-05T14:41:40Z

src/cbmc/all_properties.cpp

+            bmc.ns,
+            g.second.goto_trace,
+            json_trace,
+            bmc.trace_options());


Why is that only enabled for --all-properties?

tautschnig · 2018-01-05T14:45:07Z

src/cbmc/bmc.h

+    return trace_optionst {
+      options.get_bool_option("extended-trace"),
+    };
+  }


Could options parsing please be moved to a single, common location? I'd just make this a member of trace_optionst.

tautschnig · 2018-01-05T14:48:22Z

src/goto-programs/json_goto_trace.h

@@ -21,6 +21,7 @@ Date: November 2005
 void convert(
  const namespacet &,
  const goto_tracet &,
-  jsont &);
+  jsont &,
+  trace_optionst trace_options = trace_optionst::default_options);


I'd suggest not to use default arguments here. That would make any call sites that haven't be adjusted fail compilation.

tautschnig · 2018-01-05T15:09:44Z

src/goto-programs/json_goto_trace.cpp

+              {
+                const symbolt &symbol = ns.lookup(expr.get(ID_identifier));
+                // Don't break sharing unless need to write to it
+                const irept::named_subt &comments = expr.get_comments();


Sharing will be broken in multiple ways: expr is non-const, thus a non-const member will be called; and sharing has been broken at the prior level already by invoking visit().

tautschnig · 2018-01-05T15:10:53Z

src/cbmc/bmc.h

+    return trace_optionst {
+      options.get_bool_option("trace-json-extended"),
+    };
+  }


Copying from a previous comment: Could options parsing please be moved to a single, common location? I'd just make this a member of trace_optionst.

tautschnig · 2018-01-08T13:30:59Z

src/cbmc/all_properties.cpp

@@ -219,7 +219,7 @@ void bmc_all_propertiest::report(const cover_goalst &cover_goals)
        if(g.second.status==goalt::statust::FAILURE)
        {
          jsont &json_trace=result["trace"];
-          convert(bmc.ns, g.second.goto_trace, json_trace);
+          convert(bmc.ns, g.second.goto_trace, json_trace, bmc.trace_options());


My question still stands: why is this only being done for that particular invocation of convert, and not for the one in bmc.cpp?

Add a raw irept dump of the lhs of assignments to the trace output. This can be used for diagnostic purposes, for an intelligent UI to display a better interpretation of traces or for post-processing of traces.

smowton · 2018-01-09T10:46:01Z

@tautschnig this is now done in bmc.cpp too for symmetry -- happy for this to go in?

tautschnig · 2018-01-09T10:58:32Z

@NathanJPhillips @smowton I'd prefer not to have default arguments here (i.e., in convert) to make sure people intentionally choose the default settings. If you strongly disagree then go ahead and merge as-is, else fix first and then merge.

smowton · 2018-01-09T11:04:04Z

I disagree on that one, I think unadjusted callsites will gain a sane default, and someone using it will additionally be given guidance about a sane default choice without having to search. Therefore I'll merge as-is.

d190fd8 Merge remote-tracking branch 'upstream/develop' into pull-support-20180112 5bd5962 Merge pull request diffblue#1667 from romainbrenguier/feature/type_cast 8ecb55a Merge pull request diffblue#1717 from smowton/smowton/feature/remove_virtual_functions_per_function 0d7310a Merge pull request diffblue#1691 from romainbrenguier/bugfix/getClass#TG-1245 2064849 Use type_checked_cast in boolbv_width c5fc351 Validate data in pointer_typet in to_pointer_typet 35905c6 Add can_cast_type, validate_type for pointer_typet b72bacf Define type_try_dynamic_cast and type_checked_cast 23c3561 Unit test for string symbol resolution c13e602 Adding only needed equations in symbol resolution ae4deff Debug information for string equations 912828d JBMC: Run remove-virtual-functions as each function is converted a711c64 Introduce mechanism for renumbering an individual GOTO program e308a32 Merge pull request diffblue#1679 from NlightNFotis/nondet_extra_test e6ceb91 Merge pull request diffblue#1724 from tautschnig/fix-visitor ea74bed Add extra test for nondet-static flag and arrays 4f74896 Use irept API, not implementation-level API c55b4a5 Merge pull request diffblue#1682 from martin-cs/fix/dependence-graph-namespace-lifespan 1a2c14b Merge pull request diffblue#1722 from diffblue/unsafe_type_constructors 957a568 Merge pull request diffblue#1677 from NlightNFotis/pb4_develop 9c5add4 remove deprecated constructors for three bitvector types c96e02a no longer use deprecated constructors for some bitvector types 954060e Add unit test for has_subtype 3dd3877 Refactor has_char_pointer_subtype with has_subtype 4699c13 Extend symbol resolution to string_typet 74144fc Handle if_exprt in add_axioms_for_string_literal c6c1b3f Add an optional guard to add_axioms_for_constant 933d635 Merge pull request diffblue#1716 from mgudemann/fix/null_check_for_java_instanceof 1659314 Merge pull request diffblue#1715 from smowton/smowton/cleanup/jbmc_unused_passes 9c457b7 Add regression test for null instanceof. 2080cd3 Complete instanceof for Java. d4300d0 Merge pull request diffblue#1697 from diffblue/nondet_symbol_exprt 1c68dd4 Merge pull request diffblue#1714 from tautschnig/c-library-strcat 44b5bae Merge pull request diffblue#1698 from thomasspriggs/tg1633 c4304ba JBMC: Remove C-only passes bb8cfaa C library: Check upper bounds in memset, memcpy, memmove 7d4984f C library: Implement strcat, strncat 2a5cea2 This introduces nondet_symbol_exprt, which is generated by symbolic execution in response to side_effect_expr_nondett 85193a0 Merge pull request diffblue#1694 from NathanJPhillips/feature/add-raw-lhs-to-trace d9122dc Merge pull request diffblue#1710 from NathanJPhillips/feature/remove_instanceof_per_function 092df69 Switch from custom file / path routines to Boost-filesystem c8821b2 Allow to remove instanceof when remove exceptions 94b7658 Don't pass iterators into function calls a9c4e4f Added regression tests 76318ce Protect extended trace behind a command line option 69b0ff1 Added base_name in comments for all symbols e86080a Add raw LHS irep field to trace output ddd1b7a Add remove_instanceof overload to remove from a particular instruction 1c227b7 Merge pull request diffblue#1660 from smowton/smowton/fix/lazy_methods_array_parameters ae89c94 Lazy loading: assume concrete generic parameter types are needed 80eb6a6 TG-1877: Include array pointer types in needed classes 1053e5f Fix for [TG-1633] Inner generic types have incorrect type identifier e2cda1a Merge pull request diffblue#1704 from tautschnig/fix-copy-paste ef4a65e Fix op1/op0 copy&paste typo 21ea31f Merge pull request diffblue#1702 from peterschrammel/goto-diff-java c4bc953 Merge pull request diffblue#1701 from peterschrammel/allow-instrument-jdk 2811363 Java regression test for goto-diff 43d2e09 Also reset fresh temporary symbol counter 9ef28f4 Compare relative goto target offsets eaf3a7d Get source location from symbol table ab59659 Allow instrumentation of java.* and org.cprover.* 6fbd59c Merge pull request diffblue#1631 from tautschnig/fix-pointer-minus 7c04b5c Merge pull request diffblue#1699 from NathanJPhillips/feature/reset-main-in-tests 5e0f186 Pointer difference over void* is difference over char* faf8f00 Merge commit 'a83b52cddbed22304372c276512c63701eb3aedb' into pull-support-20180104 8236db4 Merge pull request diffblue#1419 from peterschrammel/refactor/cover-instrument a580e27 Merge pull request diffblue#1689 from smowton/smowton/feature/get_this 591511a Allow callers of load_java_class to pass the name of the main function 1b86b27 Merge pull request diffblue#1687 from smowton/smowton/feature/class-hierarchy-dot fd2bf6a Merge pull request diffblue#1688 from smowton/smowton/feature/parameter_indices f570ce5 Merge pull request diffblue#1696 from smowton/smowton/fix/identical_struct_equality 61b0d6d Merge pull request diffblue#1666 from mgudemann/bugfix/removed_required_virtual_calls 3365054 Add regression test 2b6dc8b Resolve concrete function call if no implementation is found 3f1fd64 Add code_typet::get_parameter_indices 42cf61a Fix testing for empty line in test desc file 2090000 Fix missing newline at end of desc file e448d5f Fix unsatisfiable test line f7f033d String smoke tests: ensure no type mismatches are seen b627c3d Replace unsound struct-cast simplification 8fa42b3 Class hierarchy: add DOT output, unit tests 04f2faf Mark GOTO instructions with unresolved virtual calls aac181f Pass command line options via optionst b6fa3e8 Factorize source location initialization 8da5395 Document cover functions a7f0c3d Introduce cover instrumenter 873627a Split cover into several files 0fc08f3 Replace cover-function-only by cover-include-pattern 1f2102c Add code_typet::get_this 2801f0f Avoid crashing when --dependence-graph is used by correcting namespace scoping. acac776 Add a test for the same-named static functions crashing dependence graph in the goto-analyser 05f46a9 Fix the problem where two static functions with the same name would cause the dependency graph to fail. git-subtree-dir: cbmc git-subtree-split: d190fd8

NathanJPhillips requested review from cesaro, kroening, mgudemann, peterschrammel, smowton and tautschnig as code owners January 3, 2018 14:04

smowton reviewed Jan 3, 2018

View reviewed changes

smowton requested a review from allredj January 3, 2018 15:24

NathanJPhillips force-pushed the feature/add-raw-lhs-to-trace branch from fa82683 to 198dad4 Compare January 3, 2018 15:55

allredj reviewed Jan 3, 2018

View reviewed changes

NathanJPhillips force-pushed the feature/add-raw-lhs-to-trace branch from 198dad4 to ef03228 Compare January 5, 2018 14:17

NathanJPhillips force-pushed the feature/add-raw-lhs-to-trace branch from ef03228 to df0c923 Compare January 5, 2018 15:03

tautschnig reviewed Jan 5, 2018

View reviewed changes

NathanJPhillips force-pushed the feature/add-raw-lhs-to-trace branch 3 times, most recently from 258751a to f2d6a02 Compare January 5, 2018 16:49

smowton approved these changes Jan 8, 2018

View reviewed changes

tautschnig reviewed Jan 8, 2018

View reviewed changes

NathanJPhillips added 4 commits January 8, 2018 15:15

Add raw LHS irep field to trace output

e86080a

Add a raw irept dump of the lhs of assignments to the trace output. This can be used for diagnostic purposes, for an intelligent UI to display a better interpretation of traces or for post-processing of traces.

Added base_name in comments for all symbols

69b0ff1

Protect extended trace behind a command line option

76318ce

Added regression tests

a9c4e4f

NathanJPhillips force-pushed the feature/add-raw-lhs-to-trace branch from f2d6a02 to a9c4e4f Compare January 8, 2018 15:15

smowton requested a review from chrisr-diffblue January 9, 2018 10:46

smowton merged commit 85193a0 into diffblue:develop Jan 9, 2018

NathanJPhillips deleted the feature/add-raw-lhs-to-trace branch January 17, 2018 15:38

Provide feedback

Saved searches

Use saved searches to filter your results more quickly

Add raw irept dump of lhs to trace #1694

Add raw irept dump of lhs to trace #1694

NathanJPhillips commented Jan 3, 2018 •

edited

Loading

smowton left a comment

smowton Jan 3, 2018

smowton Jan 3, 2018

allredj left a comment

NathanJPhillips commented Jan 3, 2018

allredj commented Jan 3, 2018

tautschnig commented Jan 3, 2018

tautschnig commented Jan 3, 2018

NathanJPhillips commented Jan 4, 2018 •

edited

Loading

tautschnig commented Jan 4, 2018

polgreen commented Jan 5, 2018

smowton commented Jan 5, 2018

tautschnig commented Jan 5, 2018

NathanJPhillips commented Jan 5, 2018

NathanJPhillips commented Jan 5, 2018

smowton commented Jan 5, 2018

tautschnig Jan 5, 2018

tautschnig Jan 5, 2018

tautschnig Jan 5, 2018

tautschnig Jan 5, 2018

tautschnig Jan 5, 2018

tautschnig Jan 8, 2018

smowton commented Jan 9, 2018

tautschnig commented Jan 9, 2018

smowton commented Jan 9, 2018

Add raw irept dump of lhs to trace #1694

Add raw irept dump of lhs to trace #1694

Conversation

NathanJPhillips commented Jan 3, 2018 • edited Loading

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

allredj left a comment

Choose a reason for hiding this comment

NathanJPhillips commented Jan 3, 2018

allredj commented Jan 3, 2018

tautschnig commented Jan 3, 2018

tautschnig commented Jan 3, 2018

NathanJPhillips commented Jan 4, 2018 • edited Loading

tautschnig commented Jan 4, 2018

polgreen commented Jan 5, 2018

smowton commented Jan 5, 2018

tautschnig commented Jan 5, 2018

NathanJPhillips commented Jan 5, 2018

NathanJPhillips commented Jan 5, 2018

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

smowton commented Jan 9, 2018

tautschnig commented Jan 9, 2018

smowton commented Jan 9, 2018

NathanJPhillips commented Jan 3, 2018 •

edited

Loading

NathanJPhillips commented Jan 4, 2018 •

edited

Loading