Trace output configuration options #1565

polgreen · 2017-11-07T11:24:21Z

This pull request adds the following configuration options for the trace output:

--trace-show-function-calls show functions calls and returns in trace (default is to hide)
--trace-hide-assignments hide all assignments in trace (default is to show)
--trace-hide-inputs hide all inputs in trace (default is to show)
--trace-hide-outputs hide all outputs in trace (default is to show)
--trace-show-source-code show lines of source code (default is to hide)
--trace-hex outputs assignments to variables in hex (default is binary)
--trace-html outputs trace in html format

The default, if no command line options are used, maintains the same output as before. The xml and json outputs are unaffected.

Introduces cmd line options --hex and --trace-verbosity --hex outputs all trace values in hex instead of binary setting --trace-verbosity >1 will output the corresponding line of source code with each state If numbers stop being stored as binary, this implementation will need to change, but this also applies to the binary output. NOTE: The command line interfaces for this are tidied up in a future commit that introduces trace_configurationt: 235bb01

This outputs HTML to the command line. The trace is represented in a javascript accordion, with collapsible functions. NOTE: the command line interface is cleaned up in this future commit, to use the global trace_configurationt: 6b6098c

if trace-verbosity is set to 3 or higher, output the function calls and function returns NOTE: this command line interface is cleaned up in the future commit that introduces global trace_configurationt: 235bb01

CBMC doesn't violate assumptions, it violates assertions

Introduces trace_configurationt, which tidies up the multiple command line options introduced for configuring the trace output Adds cmd line options to help file and to cbmc_parse_optionst Note that this is only implemented for CBMC, I am working in a repository that doesn't contain symex.

In this commit: - switches goto_trace to use trace_configurationt - rewrites trace_value to avoid passing 4 different members of the same struct goto_trace_stept by reference - moves the code that displays source code into show_state_header - modernises the for loops used in case INPUT and case OUTPUT - replaces "\n" with '\n'

The HTML trace now has the same configuration options as the standard trace, and uses the global trace_config variable. This commit also modernises some for loops used in case INPUT and case OUTPUT

tautschnig · 2017-11-07T11:27:48Z

@polgreen Please adjust the assert to fix the linter faillure.
Others: I had reviewed those changes internally at Amazon and would appreciate input from others before placing any approval of mine.

smowton

Style nitpicks, plus two substantiative changes I'd recommend:

Deeptest has some fork of this file; I know they'd appreciate it if the changes to the plaintext goto-trace were restructured to minimise the diff size -- for example, omitting changing "\n" to '\n' everywhere, and avoiding code structure that requires re-indenting every line
At least JBMC should surely also support this feature, so I suggest moving the command-line options and help text into the feature header and including it in the same way as we already do for GOTO_CHECK_OPT and the similar argument spec for the Java frontend.

smowton · 2017-11-07T12:02:35Z

src/goto-programs/goto_trace.cpp

 }

+static std::string expr_to_hex(const exprt & expr)


Style: exprt &expr

smowton · 2017-11-07T12:03:19Z

src/goto-programs/goto_trace.cpp

 }

+static std::string expr_to_hex(const exprt & expr)
+{
+  mp_integer value_int=binary2integer


Style:

binary2integer( id2string(to_constant_expr(expr).get_value()), false);

smowton · 2017-11-07T12:06:53Z

src/goto-programs/goto_trace.cpp


  std::string value_string;

+


Remove extra line?

smowton · 2017-11-07T12:08:20Z

src/goto-programs/goto_trace.cpp

-      << from_expr(ns, identifier, full_lhs)
-      << "=" << value_string
-      << "\n";
+      << from_expr(ns, identifier,


Style: either

from_expr( ns, identifier, (member_symbol ? step.full_lhs : step.lhs_object))

or

from_expr( ns, identifier, (member_symbol ? step.full_lhs : step.lhs_object))

smowton · 2017-11-07T12:08:44Z

src/goto-programs/goto_trace.cpp

 }

-void show_state_header(
+


Remove extra line

smowton · 2017-11-07T12:22:16Z

src/goto-programs/goto_trace.h

 void show_goto_trace(
  std::ostream &out,
  const namespacet &,
  const goto_tracet &);

 void trace_value(
-  std::ostream &out,
+  std::ostream &,


Keep the param name, it's (marginally) informative?

smowton · 2017-11-07T12:23:42Z

src/goto-programs/html_goto_trace.cpp

+void output_html_header(std::ostream &out)
+{
+  out << "<!DOCTYPE html> \n" << "<html> \n" << "<head> \n" << "<style> \n"
+      << "button.function_call{ background-color: #eee; color: Black; cursor: pointer; \n"  // NOLINT(*)


Suggest a break after each property to make this easier on people hand-editing the HTML or editing this code

smowton · 2017-11-07T12:25:10Z

src/goto-programs/html_goto_trace.cpp

+      << "div.panel1 { padding: 0 18px; display: none; background-color: AliceBlue; border: 1px solid gray } \n"  // NOLINT(*)
+      << "div.panel2 { padding: 0 18px; display: none; background-color: CornSilk; border: 1px solid gray} \n"  // NOLINT(*)
+      << "div.property_panel { padding: 0 18px; display: block; background-color: LightGray; border: 1px red} \n"  // NOLINT(*)
+


If we're doing style we should probably do so everywhere, and turn e.g. <strong><span style=\"color: Red;\"> below into <span class=\"violated_property\">, rather than intermixing out-of-line and inline style.

smowton · 2017-11-07T12:25:40Z

src/goto-programs/html_goto_trace.cpp

+
+  out << " " << state.pc->source_location
+      << " thread " << state.thread_nr
+      << "</strong>></p>\n";


smowton · 2017-11-07T12:28:34Z

src/goto-programs/html_goto_trace.cpp

+    case goto_trace_stept::typet::ASSIGNMENT:
+      if(config.trace_config.show_value_assignments)
+      {
+        if(step.pc->is_assign() || step.pc->is_return()


One disjunct per line?

polgreen · 2017-11-07T12:47:38Z

Ok,

1a) I added all the changes from "\n" to '\n' at Michael's request. I can revert them, but could you and Michael reach a consensus about that before I spend the time doing it?
1b) ok, will change the if statements to if() break;

Can you point me to where GOTO_CHECK_OPT is included? I can't find it with git grep.

I've currently got one failing java regression test, which I can fix if I give the trace_configurationt default values. Is using default values here acceptable?

smowton · 2017-11-07T13:03:20Z

Inclusion of OPT_GOTO_CHECK (oops, got the name the wrong way around): https://github.com/diffblue/cbmc/blob/develop/src/cbmc/cbmc_parse_options.h#L36

Similarly its help text is factored so it doesn't have to be duplicated across different driver programs: https://github.com/diffblue/cbmc/blob/develop/src/cbmc/cbmc_parse_options.cpp#L974

Basically I'd move the help text, the options and the parser function (https://github.com/diffblue/cbmc/pull/1565/files#diff-41db988013f70caad45ce489749c7df6R105) alongside the feature, then you can trivially include it in both cbmc and jbmc

smowton · 2017-11-07T13:03:40Z

@tautschnig willing to keep "\n"?

smowton · 2017-11-07T13:05:43Z

One more thing, there should be a couple of regression and/or unit tests for this, otherwise it's likely to moulder

tautschnig · 2017-11-07T13:48:32Z

@tautschnig willing to keep "\n"?

@polgreen @smowton As much as I think using '\n' is better when writing fresh code, we should not cause extra work for people who already have patches on top of the existing code base. Hence, Elizabeth if reasonably possible, could you please revert those changes?

peterschrammel · 2017-11-07T21:53:50Z

regression/Makefile

-       strings-smoke-tests \
-       test-script \
+DIRS =  cbmc-java \
+       #cbmc-java-inheritance \


Please undo this spurious change

peterschrammel · 2017-11-07T21:55:23Z

src/cbmc/cbmc_parse_options.cpp

+    config.trace_config.numeric_representation =
+        configt::numeric_representationt::BINARY;
+
+  config.trace_config.show_source_code =


Using config for this kind of settings is uncommon. Use options.

peterschrammel · 2017-11-07T21:56:50Z

src/cbmc/cbmc_parse_options.cpp

+    "--trace-hide-outputs         hide all outputs in trace (default is to show)\n" // NOLINT(*)
+    "--trace-show-source-code     show lines of source code (default is to hide)\n" // NOLINT(*)
+    "--trace-hex                  outputs assignments to variables in hex (default is binary)\n" // NOLINT(*)
+    "--trace-html                 outputs trace in html format\n"


What is the result of using --trace-htmltogether with --json-ui?

json overrides. I don't know what the expected result should be, but the json trace doesn't use any of my new configuration options

peterschrammel · 2017-11-07T21:58:27Z

src/goto-programs/goto_trace.cpp

@@ -17,10 +17,12 @@ Author: Daniel Kroening
 #include <ostream>

 #include <util/arith_tools.h>
+#include <util/config.h>


Following our efforts to get rid of the global config eventually, this dependency should be avoided.

peterschrammel · 2017-11-07T22:08:06Z

Further suggestions: use clang-format and add doxygen comments to newly introduced functions.

peterschrammel · 2017-11-07T22:11:25Z

The failing of some unit tests (which looks somehow unrelated) is concerning: https://travis-ci.org/diffblue/cbmc/jobs/298527593#L2227

polgreen · 2017-11-08T09:11:11Z

The failing regression tests are java tests and it's because I haven't integrated this into the jbmc front end properly yet, will fix

polgreen · 2018-01-05T09:10:58Z

resurrecting this PR.

@peterschrammel, you requested that I don't use config, and use options instead. That means I will have to change the function signature for several intermediate functions that options will need to be passed to. Is that ok? @tautschnig, I think we talked about this when i was originally implementing this and you suggested using config instead of options, I think for that reason?

peterschrammel · 2018-01-05T09:37:09Z

I suggest to turn html_goto_trace into a proper class show_html_goto_tracet with options as a member so that you don't have to pass them around into utility functions. As far as I see, only show_goto_trace() will require an options parameter. In the places where show_goto_trace is called an options object is already available.

tautschnig · 2018-01-05T09:38:58Z

Yes, using configt seemed to be the quicker route, resulting in a smaller patch. Using optionst is the cleaner approach, and should likely be the way to go once all other concerns are out of the way. (And while typing this @peterschrammel has already provided guidance on how to make this work.)

polgreen · 2018-07-02T13:24:41Z

I'm redoing this PR.
@peterschrammel, there now appears to be a global trace_optionst; this seems slightly at odds with the aim of removing global config, but does that change your view on how to implement this? I assume that since there has already been a global introduced, it would make sense for me to use that global

TGWDB · 2021-06-09T13:11:57Z

Closing as this appears to have been long abandoned. Please reopen and update if this closure is erroneous.

polgreen added 10 commits November 7, 2017 10:53

Start of HTML goto trace output

686fedd

This outputs HTML to the command line. The trace is represented in a javascript accordion, with collapsible functions. NOTE: the command line interface is cleaned up in this future commit, to use the global trace_configurationt: 6b6098c

Output function calls in trace

6725c8c

if trace-verbosity is set to 3 or higher, output the function calls and function returns NOTE: this command line interface is cleaned up in the future commit that introduces global trace_configurationt: 235bb01

Change "violated assumption" to "assumption" in trace

24a4875

CBMC doesn't violate assumptions, it violates assertions

Tidy up CBMC parse_options trace configuration

cb560d3

Update html_goto_trace to use trace_configurationt

c05ab18

The HTML trace now has the same configuration options as the standard trace, and uses the global trace_config variable. This commit also modernises some for loops used in case INPUT and case OUTPUT

rename "html-trace" to "trace-html"

671db6b

Fix html trace colour alternation for function calls

51bfbd7

polgreen requested review from kroening, peterschrammel, smowton and tautschnig as code owners November 7, 2017 11:24

polgreen added 2 commits November 7, 2017 11:28

replace assert with invariant

5129907

doxygen changes

94391c1

smowton reviewed Nov 7, 2017

View reviewed changes

configure trace otuput for graphml witness

9b8cbfb

peterschrammel reviewed Nov 7, 2017

View reviewed changes

peterschrammel added the do not merge label Nov 10, 2017

tautschnig assigned polgreen Nov 30, 2017

tautschnig mentioned this pull request Jan 3, 2018

Add raw irept dump of lhs to trace #1694

Merged

TGWDB closed this Jun 9, 2021

Provide feedback

Saved searches

Use saved searches to filter your results more quickly

Trace output configuration options #1565

Trace output configuration options #1565

polgreen commented Nov 7, 2017

tautschnig commented Nov 7, 2017

smowton left a comment

smowton Nov 7, 2017

smowton Nov 7, 2017

smowton Nov 7, 2017

smowton Nov 7, 2017

smowton Nov 7, 2017

smowton Nov 7, 2017

smowton Nov 7, 2017

smowton Nov 7, 2017

smowton Nov 7, 2017

smowton Nov 7, 2017

polgreen commented Nov 7, 2017

smowton commented Nov 7, 2017

smowton commented Nov 7, 2017

smowton commented Nov 7, 2017

tautschnig commented Nov 7, 2017

peterschrammel Nov 7, 2017

peterschrammel Nov 7, 2017

peterschrammel Nov 7, 2017

polgreen Nov 8, 2017

peterschrammel Nov 7, 2017

peterschrammel commented Nov 7, 2017

peterschrammel commented Nov 7, 2017 •

edited

Loading

polgreen commented Nov 8, 2017

polgreen commented Jan 5, 2018

peterschrammel commented Jan 5, 2018

tautschnig commented Jan 5, 2018

polgreen commented Jul 2, 2018

TGWDB commented Jun 9, 2021

Trace output configuration options #1565

Trace output configuration options #1565

Conversation

polgreen commented Nov 7, 2017

tautschnig commented Nov 7, 2017

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

polgreen commented Nov 7, 2017

smowton commented Nov 7, 2017

smowton commented Nov 7, 2017

smowton commented Nov 7, 2017

tautschnig commented Nov 7, 2017

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

peterschrammel commented Nov 7, 2017

peterschrammel commented Nov 7, 2017 • edited Loading

polgreen commented Nov 8, 2017

polgreen commented Jan 5, 2018

peterschrammel commented Jan 5, 2018

tautschnig commented Jan 5, 2018

polgreen commented Jul 2, 2018

TGWDB commented Jun 9, 2021

peterschrammel commented Nov 7, 2017 •

edited

Loading