Basic placeholder information about cprover printing. #3392

sonodtt · 2018-11-13T15:09:44Z

Each commit message has a non-empty body, explaining why the change was made.
Methods or procedures I have added are documented, following the guidelines provided in CODING_STANDARD.md.
Regression or unit tests are included, or existing tests cover the modified code (in this case I have detailed which ones those are in the commit message).
My commit message includes data points confirming performance improvements (if claimed).
My PR is restricted to a single feature or bugfix.
White-space or formatting changes outside the feature-related changed lines are in commits of their own.

Basic information about Cprover printing.
Placeholder in util folder readme for some generic information about the types of classes / locations where Cprover can provide output.

chrisr-diffblue · 2018-11-13T15:25:47Z

src/util/README.md

+Exceptions also print to std::cerr - and have a standard 'what()' interface. More information on exceptions can be found in `exception_utils.h`.
+
+* messages - filtered by a 'verbosity' level.
+\ref messaget provides messages with a built-in verbosity 'level'.


Maybe provide a link to the appropriate header file as well, and not just to the type?

peterschrammel · 2018-11-13T21:26:01Z

src/util/README.md

+* output from invariants / exceptions
+Invariants output to std::cerr - and provide a backtrace and optionally some diagnostic information.
+For more information on invariants, see `invariant.h`
+Exceptions also print to std::cerr - and have a standard 'what()' interface. More information on exceptions can be found in `exception_utils.h`.


Is this the same of json_ui and xml_ui?

Also, I don't think exceptions print directly? If we ever (it would be a bug) let them propagate all the way to the entry point then the OS will do whatever it thinks is right. We actually ought to catch them and put the information (from what()) into a message handler.

@peterschrammel
I'll add a few notes about the json and xml output.

To answer the specifics:
In the case of cbmc_parse_optionst (I haven't looked at all the other drivers, I'd hope they all behave in similar fashion - because... well, why wouldn't they)

• uit::PLAIN
then ui_message_handlert::message_handler
is not left as nullptr but is initialised to
message_handler = &*console_message_handler; (with relevant 'flush' type)

void console_message_handlert::print(
...
if(level>=4)
{
std::cout << message << '\n';
}
else
std::cerr << message << '\n';

• for uit:: XML_UI

void ui_message_handlert::xml_ui_msg(
...
xmlt result;
...
out << result;
(where out has been initialised to std::cout)

• for uit:: JSON_UI
json_stream =
std::unique_ptr<json_stream_arrayt>(new json_stream_arrayt(out));
where out has been initialised to std::cout

So I left that part vague...

@ Tautschnig

"Hmm, are we trying to document

the interface that the developer should use (don't use cout/cerr),

the implementation behind any of those interfaces (uses cout/cerr), or

the effect (prints something on cout/cerr)?"

I thought that this was a little too essential (and complex) to have no documentation/information of current state - so I wrote a little, not least to get this kind of debate going.
My intention was to overview briefly 'what's there'.
As an aside - I feel the same about the invariant header file - if these macros are to be used often, then surely a few usage examples and better overview of edge cases would be useful. It's quite a hefty file for a new developer - to add a few invariants, they'll have to read it thoroughly. Hmmm, come to think of it - perhaps that's a feature... (?)
But I tend to think of that as a risky assumption.

@tautschnig w.r. to exception printing
This is how I unwrap what's happening. Clarified here, because I genuinely would like to be pointed in the right direction if I got it wrong.
There's a fair bit of unravelling before you actually get to the bottom of it.
provisos as above - cbmc_parse_options only considered.

A)
parse_options.cpp

int parse_options_baset::main()

catch(const invalid_command_line_argument_exceptiont &e)
{
std::cerr << e.what() << "\n";
return CPROVER_EXIT_USAGE_ERROR;
}
catch(const cprover_exception_baset &e)
{
std::cerr << e.what() << '\n';
return CPROVER_EXIT_EXCEPTION;
}

B)
cbmc_parse_optionst

int cbmc_parse_optionst::get_goto_program(

catch(incorrect_goto_program_exceptiont &e)
{
log.error() << e.what() << log.eom;
return CPROVER_EXIT_EXCEPTION;
}
catch(const char *e)
{
log.error() << e << log.eom;
return CPROVER_EXIT_EXCEPTION;
}

cbmc_parse_optionst::cbmc_parse_optionst(int argc, const char **argv)
: parse_options_baset(CBMC_OPTIONS, argc, argv),
xml_interfacet(cmdline),
messaget(ui_message_handler),
ui_message_handler(cmdline, std::string("CBMC ") + CBMC_VERSION),
path_strategy_chooser()
{
}

int get_goto_program_ret =
get_goto_program(goto_model, options, cmdline, *this, ui_message_handler);

*this initialises log with cbmc_parse_optionst, which is subclassed from messaget

• The exceptions print to log.error() , i.e. are given a level 1
then if the output is plain ->

void console_message_handlert::print(
...
if(level>=4)
{
std::cout << message << '\n';
}
else
std::cerr << message << '\n';

So in the case of JSON and XML output - the output will be to std::cout, but otherwise, its out to std::cerr

Apologies that I'll keep belabouring the same point: please decide on the target audience first. I believe we've even got open issues about the mess that output is at the moment. Front-ends (aka driver programs), such as "cbmc", should provide documentation on what the user can expect (i.e., exceptions and errors will be shown on stderr, etc.). Documentation aimed at developers should provide guidance on how to do it right. To them, it shouldn't really matter where or how it ends up printed, because they should reasonably be able to assume that the right thing will happen if they follow the guidelines spelled out in here.

@tautschnig
Belabour away if you think it'll improve things. We have a common objective :)
I pulled Chris over for a quick review - and that clarified things a little.

I've rewritten the section to put forward 'what people really should be doing', i.e. using the messaging interface - with a little bit of an introduction to its objectives.

I've kept a subsection for 'how some things are at the moment, but this is not how we should do them going forward'.

tautschnig · 2018-11-14T12:16:42Z

src/util/README.md

@@ -329,3 +329,18 @@ serialisation queries save only that integer hash code of the string.

 \subsubsection irep-serialization-ireps Serialization of `irept` Instances

+
+\subsection CProver-output CProver output - printing
+Cprover has 3 principal types of output:


Is there consistency in how "cprover"/"Cprover"/"CProver"/"CPROVER" is being written across the docs?

Ah.... excellent point. I've now posted on internal slack to raise that issue.

I'd go with CProver. That's most readable IMO.

tautschnig · 2018-11-14T12:17:06Z

src/util/README.md

+\subsection CProver-output CProver output - printing
+Cprover has 3 principal types of output:
+
+* direct output via std::cout & std::cerr (these are in the process of being removed).


Let's put this last, it's how it should not be done.

tautschnig · 2018-11-14T12:20:09Z

src/util/README.md

+* output from invariants / exceptions
+Invariants output to std::cerr - and provide a backtrace and optionally some diagnostic information.
+For more information on invariants, see `invariant.h`
+Exceptions also print to std::cerr - and have a standard 'what()' interface. More information on exceptions can be found in `exception_utils.h`.


Also, I don't think exceptions print directly? If we ever (it would be a bug) let them propagate all the way to the entry point then the OS will do whatever it thinks is right. We actually ought to catch them and put the information (from what()) into a message handler.

tautschnig · 2018-11-14T12:21:00Z

src/util/README.md

+For more information on invariants, see `invariant.h`
+Exceptions also print to std::cerr - and have a standard 'what()' interface. More information on exceptions can be found in `exception_utils.h`.
+
+* messages - filtered by a 'verbosity' level.


Really, this is the only acceptable form of generating output (other than writing information to a file).

@tautschnig

int parse_options_baset::main()
catch(const invalid_command_line_argument_exceptiont &e)
{
std::cerr << e.what() << "\n";
return CPROVER_EXIT_USAGE_ERROR;
}
catch(const cprover_exception_baset &e)
{
std::cerr << e.what() << '\n';
return CPROVER_EXIT_EXCEPTION;
}

Otherwise it seems that we are going through a message handler (verified via a quick search - not foolproof 'std::cerr ?<<.+what' ).

tautschnig · 2018-11-14T12:22:02Z

src/util/README.md

+
+* messages - filtered by a 'verbosity' level.
+\ref messaget provides messages with a built-in verbosity 'level'.
+These are then processed by a subclass of \ref message_handlert - which filters out all messages above a set verbosity level.  An example of this is \ref stream_message_handlert and its subtypes, which directs messages to an output stream (std::cout & std::cerr - std::log is not used).


What is std::log?

The natural (base e) logarithm. But that doesn't help us a great deal here.
std::clog.

allredj

✔️
Passed Diffblue compatibility checks (cbmc commit: 270222b).
Build URL: https://travis-ci.com/diffblue/test-gen/builds/91529880

allredj

✔️
Passed Diffblue compatibility checks (cbmc commit: f5bd587).
Build URL: https://travis-ci.com/diffblue/test-gen/builds/91548851

sonodtt requested review from kroening, peterschrammel, pkesseli, smowton and tautschnig as code owners November 13, 2018 15:09

chrisr-diffblue reviewed Nov 13, 2018

View reviewed changes

peterschrammel added the documentation label Nov 13, 2018

peterschrammel reviewed Nov 13, 2018

View reviewed changes

peterschrammel assigned sonodtt Nov 13, 2018

tautschnig reviewed Nov 14, 2018

View reviewed changes

allredj reviewed Nov 15, 2018

View reviewed changes

Basic information about cprover output

f5bd587

sonodtt force-pushed the doc-day-cprover-printing-overview branch from 270222b to f5bd587 Compare November 15, 2018 16:03

allredj reviewed Nov 15, 2018

View reviewed changes

sonodtt assigned tautschnig Nov 19, 2018

tautschnig approved these changes Nov 24, 2018

View reviewed changes

tautschnig merged commit 23932b8 into diffblue:develop Nov 24, 2018

Basic placeholder information about cprover printing. #3392

Basic placeholder information about cprover printing. #3392

Uh oh!

Conversation

sonodtt commented Nov 13, 2018

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

sonodtt Nov 14, 2018 • edited Loading Uh oh! There was an error while loading. Please reload this page.

Uh oh!

Choose a reason for hiding this comment

Uh oh!

tautschnig Nov 14, 2018 • edited by sonodtt Loading Uh oh! There was an error while loading. Please reload this page.

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

allredj left a comment

Choose a reason for hiding this comment

Uh oh!

allredj left a comment

Choose a reason for hiding this comment

Uh oh!

Uh oh!

sonodtt Nov 14, 2018 •

edited

Loading

tautschnig Nov 14, 2018 •

edited by sonodtt

Loading