Fix for cbmc running out of memory while printing traces using json_ui / target: develop #1814

NlightNFotis · 2018-02-08T14:58:59Z

This is a port of #1767 to develop (instead of goto-analyzer-develop as requested by @peterschrammel and @martin-cs . Below is the message of the original PR:

There has been a bug reported to us where cbmc would run out of memory while creating a huge json object in memory to report the traces with. This is changing the tracing report facility to use a new json class that streams the objects immediately as created, and therefore fixes the issue.

peterschrammel · 2018-02-08T15:03:58Z

src/goto-programs/json_goto_trace.cpp

This can be removed now.

The commit message isn't very useful.

peterschrammel · 2018-02-08T15:04:24Z

src/util/ui_message.h

This change is in the wrong commit.

peterschrammel · 2018-02-08T15:05:43Z

src/cbmc/all_properties.cpp

        {
-          jsont &json_trace=result["trace"];
-          convert(bmc.ns, g.second.goto_trace, json_trace, bmc.trace_options());
+          json_stream_arrayt &json_trace=result.push_back_stream_array("trace");


(commit for entire commit) This commit should come after the json_goto_trace refactoring.

peterschrammel · 2018-02-08T15:07:30Z

src/util/json.cpp

  }
 }

+void jsont::output_object(std::ostream &out, const objectt &object, unsigned indent)


Some doxygen would be good (sorry that I threw that over to you without docs).

peterschrammel · 2018-02-08T15:10:43Z

src/util/json_stream.h

this should go into the commit where this file was introduced

these changes should go into the first commit

peterschrammel · 2018-02-08T15:12:06Z

src/util/ui_message.cpp

This seems still necessary as XML output hasn't been moved an xml_stream yet.

peterschrammel · 2018-02-08T15:12:49Z

src/util/ui_message.cpp

This include should come first.

peterschrammel · 2018-02-08T15:13:08Z

src/util/ui_message.cpp

Unclear why this file is modified in this commit.

peterschrammel · 2018-02-08T15:13:48Z

src/goto-programs/json_goto_trace.cpp

(comment for entire commit) These changes should be squashed with the previous commit.

I suggest to improve the commit message.

peterschrammel · 2018-02-08T19:51:30Z

src/util/json.h

unclear why this line is removed

peterschrammel · 2018-02-08T19:52:40Z

src/util/json_stream.cpp

there should be some doxygen for all this

peterschrammel · 2018-02-08T19:52:55Z

src/util/json_stream.h

peterschrammel · 2018-02-08T19:58:14Z

src/util/json_stream.cpp

The changes to this file should be in the previous commit.

peterschrammel · 2018-02-08T19:58:48Z

src/util/message.h

Why is there a json_stream_arrayt variant, but no json_stream_objectt one?

peterschrammel · 2018-02-08T19:59:25Z

src/goto-programs/json_goto_trace.cpp

this include should be the first

peterschrammel · 2018-02-08T20:00:06Z

src/util/json_stream.h

these changes should go into the first commit

peterschrammel · 2018-02-08T20:00:48Z

src/goto-programs/json_goto_trace.h

why is this non-const?

peterschrammel · 2018-02-08T20:01:25Z

src/goto-programs/json_goto_trace.cpp

doxygen missing throughout these files

peterschrammel · 2018-02-08T20:01:48Z

src/goto-programs/json_goto_trace.cpp

why is this non-const?

peterschrammel · 2018-02-08T20:04:11Z

@NlightNFotis, there's a compiliation error: https://travis-ci.org/diffblue/cbmc/jobs/339128397#L1550

peterschrammel · 2018-02-08T20:04:47Z

Also, cpplint and clang-format are complaining. Be careful to reformat the changes in each commit separately.

peterschrammel · 2018-02-09T12:12:03Z

src/goto-programs/json_goto_trace.h

There are a couple of header files that can be put into the cpp file.

NlightNFotis · 2018-02-09T17:47:43Z

This should be ready to review, this only needs the clang format changes to be squashed to their appropriate commits.

tautschnig

The PR talks about fixing an out-of-memory problem, but then in the middle of the PR suddenly there is a refactoring commit as well. Lots of seemingly unnecessary whitespace changes. All of that makes reviewing extremely hard.

My main concern, however, is the core API that is not at all self-documenting. I get the problem that it is trying to solve, but it's very hard to tell whether that solution is actually fit for purpose. See details in my comments.

tautschnig · 2018-02-10T16:33:55Z

src/util/json.cpp

Shouldn't the newline also be conditional on o_it!=object.beginn()?

No, because an object always starts with an opening brace, after which we put a newline (code snippet factored out from lines 69-85 above).

tautschnig · 2018-02-10T16:36:16Z

src/util/json.cpp

Not a big deal, but out << "\": "; would also do the trick, wouldn't it?

tautschnig · 2018-02-10T16:37:39Z

src/util/json.h

Remote friends are bad.

Seems unnecessary to have them.

tautschnig · 2018-02-10T16:40:08Z

src/util/json_stream.cpp

To be honest, that's a very strange piece of code. It seems to be extremely context-dependent and far from side-effect free.

tautschnig · 2018-02-10T16:40:56Z

src/util/json_stream.cpp

The constructor does out << '[' so I'd expect this to be done in a destructor (otherwise the constructor shouldn't be doing the opening bracket).

This is exactly what it is doing (by calling close() which, in turn, calls output_finalizer).

tautschnig · 2018-02-10T16:45:28Z

src/util/json_stream.cpp

Nit pick: no comma before "that"

tautschnig · 2018-02-10T16:47:29Z

src/util/json_stream.h

The only public operation is close - that's truly weird. Please create a meaningful API, which might have virtual ...(...) = 0; members - but at least it would explain how to use this thingy.

The only public facility that this base class provides is close().
output_current and output_finalizer should be made abstract.

I don't think this has happened? Maybe it has, but they are all protected so I have no idea what is the public interface of (children of) json_streamt.

tautschnig · 2018-02-10T16:50:13Z

src/util/json_stream.h

How does this fit in a "stream" class?!

It allows mixing streamed and non-streamed json elements. The API enforces that the parent of a streamed element must always be a streamed element.

Why does it even make sense to mix them? Or is my above thought that a json_streamt is actually also some form of jsont that actually holds data?!

tautschnig · 2018-02-10T16:51:10Z

src/cbmc/all_properties.cpp

Whitespace changes?

These whitespace changes are unnecessary.

tautschnig · 2018-02-10T16:56:01Z

src/goto-programs/json_goto_trace.h

Why does this need to be a template argument?

To be able to use both the streaming and the object version.

peterschrammel · 2018-02-13T13:23:52Z

src/goto-programs/json_goto_trace.h

To be able to use both the streaming and the object version.

peterschrammel · 2018-02-13T13:29:29Z

src/cbmc/all_properties.cpp

These whitespace changes are unnecessary.

peterschrammel · 2018-02-13T13:29:41Z

src/cbmc/bmc_cover.cpp

unnecessary.

peterschrammel · 2018-02-13T13:30:47Z

src/goto-programs/json_goto_trace.cpp

The changes in this file are unnecessary.

peterschrammel · 2018-02-13T13:34:01Z

src/util/json.cpp

No, because an object always starts with an opening brace, after which we put a newline (code snippet factored out from lines 69-85 above).

peterschrammel · 2018-02-13T13:40:09Z

src/util/json_stream.cpp

I agree. There is some doxygen work to be done to explain how things fit together.

peterschrammel · 2018-02-13T13:41:38Z

src/util/json_stream.h

This "new class" will soon be an "old class" ;)

peterschrammel · 2018-02-13T13:43:17Z

src/util/json_stream.h

The only public facility that this base class provides is close().
output_current and output_finalizer should be made abstract.

peterschrammel · 2018-02-13T13:50:29Z

src/util/json_stream.h

It allows mixing streamed and non-streamed json elements. The API enforces that the parent of a streamed element must always be a streamed element.

peterschrammel · 2018-02-13T13:51:13Z

src/util/message.h

This change seems unnecessary.

NlightNFotis · 2018-02-21T17:16:48Z

I have added one last commit that attempts to fix the goto-diff broken tests, due to the way they interact with the new class.

I will write a lengthier report about what was happening and why this is necessary later.

peterschrammel

Thanks, @NlightNFotis, this looks good now. Please update the TG bump.

tautschnig

Various comments below, with the definitive blocker of using std::cout (and thus iostream) in a header file.

I'm still not sure I'm on the right track: do we now have multiple classes that serve one and the same purpose, but differ in how output is implemented? Does this mix data representation and behaviour? Are you solving an original design deficiency in that a jsont took care of its own output by adding a variant that takes care of its own output in a different way? Shouldn't output just never have been a member function of jsont? Isn't this one of the prototypical situations to use the visitor pattern? Even more so as jsont is the root of a nice family of classes, and also a very much bounded one so that it wouldn't be necessary to add more members to a visitor (as is sort of the case for anything based on irept)?

tautschnig · 2018-02-23T08:55:39Z

src/util/message.h

Please explain why this isn't get_json_stream() = 0; or marked protected?

If I change it to get_json_stream() = 0; then I get compilation errors that some variables, such as message_handler in line 189 of graphml.cpp can not be initialised to an abstract type. I understand that this happens because other members of the hierarchy, like null_message_handlert are not redefining get_json_stream(), a now pure virtual function.

If it's marked protected, that creates problems with the interaction with the class mstreamt in the same file (message.h, line 184), particularly with the method json_stream() in line 244, which contains the statement return message.message_handler->get_json_stream();, which can not work with get_json_stream() being protected.

If I change it to get_json_stream() = 0; then I get compilation errors that some variables, such as message_handler in line 189 of graphml.cpp can not be initialised to an abstract type. I understand that this happens because other members of the hierarchy, like null_message_handlert are not redefining get_json_stream(), a now pure virtual function.

To me, this looks like a prime example of why compile-time errors are preferable over runtime errors: in my opinion, that just means that null_message_handlert needs to be fixed.

tautschnig · 2018-02-23T08:57:21Z

src/util/message.h

I believe a forward declaration class json_stream_arrayt; would suffice.

tautschnig · 2018-02-23T08:59:07Z

src/util/json.h

If you remove this, then also the public in line 123 is redundant.

@NlightNFotis, this shouldn't be removed. Only move the function that is required to the public section.

tautschnig · 2018-02-23T09:00:27Z

src/util/json_stream.cpp

Isn't this prone to attempts of closing a closed file? child_stream is not reset.

Closing closed files is not a practical issue here because json_streamt only wraps the actual stream (that could be a file). json_streamt never closes that stream - that's in the realm of the user of json_streamt. However, to avoid confusion, I would assign child_stream = nullptr here and put appropriate PRECONDITIONS to make sure that there is no double-close (which is indeed a sign of a programming error).

tautschnig · 2018-02-23T09:08:30Z

src/util/json_stream.cpp

What is the purpose of all these push_back_stream* functions ("Add a JSON ..." -- to what?) as none of them are invoked anywhere in this commit, and why aren't they just a single one in the parent class? I understand that they have different return types, but is that actually necessary (as anything done to those return values can be resolved to the right child class via virtual tables)?

It would be very inconvenient to let the user cast to json_stream_arrayt and json_stream_objectt in order to use their respective interfaces (objects and arrays are quite different things).

I think this fits with my overall comment: there seems to be a strong case for re-architecting here to use a visitor rather than this proposed design of inheritance.

@tautschnig, could you please explain how 'use a visitor' would contribute to a solution in this context?
Inheritance is used here because json_stream_arrayt and json_stream_objectt are both json streams, which share common functionality, namely flushing the data. If this is considered too little to justify a base class the common code can be duplicated in the respective derived classes at the cost of complicating the logic to flush the stream and to enforce the single-stream-at-a-time invariant.

In my opinion, there should be one class that knows how to stream jsont. That class would be the visitor. It has methods that know how to stream a json_arrayt or json_objectt (and json_numbert, json_stringt, etc.).

tautschnig · 2018-02-23T09:23:33Z

src/util/json_stream.h

Why do you need compatibility with jsont? Are you saying that this some sort of replacement for jsont? Please tell me that I'm wrong.

tautschnig · 2018-02-23T09:25:08Z

src/util/json_stream.h

Why does it even make sense to mix them? Or is my above thought that a json_streamt is actually also some form of jsont that actually holds data?!

tautschnig · 2018-02-23T09:26:28Z

src/util/message.h

Why is there a json_stream_arrayt variant, but no json_stream_objectt one?

tautschnig · 2018-02-23T09:29:20Z

src/util/ui_message.h

Nope. Not in a header file.

@NlightNFotis, the implementation of the constructor must go into the .cpp file.

tautschnig · 2018-02-23T09:32:09Z

src/util/ui_message.h

First, there seems to be no point of even having a std::ostream member as there is a single function that relies on it, and no way to setting it to any other value. Second, this has no place in a header file.

No, out is used many, many times in the .cpp file. Eventually, assigning out should be the only use of std::cout in the codebase.
The implementation of the constructor must be moved back into the cpp file.

peterschrammel · 2018-02-24T11:34:29Z

src/util/json.h

@NlightNFotis, this shouldn't be removed. Only move the function that is required to the public section.

peterschrammel · 2018-02-24T11:38:08Z

src/util/json_stream.cpp

They are actually quite similar. The only difference is that array elements don't have keys.

peterschrammel · 2018-02-24T11:40:58Z

src/util/json_stream.cpp

Closing closed files is not a practical issue here because json_streamt only wraps the actual stream (that could be a file). json_streamt never closes that stream - that's in the realm of the user of json_streamt. However, to avoid confusion, I would assign child_stream = nullptr here and put appropriate PRECONDITIONS to make sure that there is no double-close (which is indeed a sign of a programming error).

peterschrammel · 2018-02-24T11:48:17Z

src/util/json_stream.cpp

It would be very inconvenient to let the user cast to json_stream_arrayt and json_stream_objectt in order to use their respective interfaces (objects and arrays are quite different things).

peterschrammel · 2018-02-24T11:53:10Z

src/util/json_stream.h

No. open is the state of this not child_stream. You can create and close many child streams sequentially (timewise), e.g. for each element in an array or each property in an object). The invariant is that there can only be at most child stream at a time.

peterschrammel · 2018-02-24T11:53:39Z

src/util/json_stream.h

@NlightNFotis, it seems that open requires explanation.

peterschrammel · 2018-02-24T11:59:21Z

src/util/ui_message.h

@NlightNFotis, the implementation of the constructor must go into the .cpp file.

peterschrammel · 2018-02-24T12:04:45Z

src/util/ui_message.h

No, out is used many, many times in the .cpp file. Eventually, assigning out should be the only use of std::cout in the codebase.
The implementation of the constructor must be moved back into the cpp file.

NlightNFotis · 2018-03-06T13:40:29Z

Hi @tautschnig. I think your concerns have been addressed. Is it possible that you take another look and let me know if there's anything more you want to be done, else give it the green light?

Thanks for your time,

tautschnig · 2018-03-06T15:37:08Z

To what extent has #1814 (comment):

think this fits with my overall comment: there seems to be a strong case for re-architecting here to use a visitor rather than this proposed design of inheritance.

been addressed? Anyone is free to override my non-approval, but I do maintain that the architecture here is flawed and that implementing a different form of output by inheriting and overriding the data representation is wrong.

martin-cs · 2018-03-06T15:43:53Z

@tautschnig As the person who had the initial problem -- would it help if I had a review?

tautschnig · 2018-03-06T15:48:01Z

@martin-cs Your reviews are always welcome! It may very well be the case that an urgent solution is required and I thus invite overrides to my non-approval. Any maybe my suggested architecture is also flawed. I'm always open to input.

Introduce a new json object class that streams the object immediately to an output instead of building the object in memory and then output it to the stream.

Refactor the templated convert function with switch statements that handle different instructions to dispatch to functions that are specialised per instruction.

NlightNFotis · 2018-03-16T10:04:46Z

@tautschnig @peterschrammel I have been made aware that there have been offline discussions regarding the architectural changes in this PR, and the disagreements have been resolved. Can you both take a look to let me know if everything is alright, and if yes, possibly merge it as well?

@peterschrammel The associated testgen PR is also passing with no problems

tautschnig · 2018-03-19T13:11:59Z

My apologies for having been dense and not fully understanding the problem this was trying to solve. It took an out-of-band chat with @peterschrammel to get me on track: it was not clear to me that constructing the jsont (and keeping it in memory) was the problem, not just constructing a very long std::string of output. With that insight I was able to make sense of all the bits that make up the proposed API. It's not the way I would have solved the problem (see below), but it's an existing solution so I'm not going to stand in the way any further.

Here is what I would have done: make json_streamt a factory (of sorts) that owns all jsont objects and can memory-manage them. Rather than changing jsont (or its children) I'd keep a stack of "open" objects in json_streamt, with any push_back or operator[] access going through the factory. The desired advantage is that the data representation would remain with jsont, and it would seem closer to an established design pattern. But it might have disadvantages that one would only get to see when really implementing it in full.

NlightNFotis requested review from kroening, peterschrammel, smowton and tautschnig as code owners February 8, 2018 14:58

peterschrammel requested changes Feb 8, 2018

View reviewed changes

NlightNFotis force-pushed the flush-json-stream branch from 4dc26ce to c3790b8 Compare February 8, 2018 18:05

NlightNFotis requested review from cesaro, chrisr-diffblue, martin-cs and mgudemann as code owners February 8, 2018 18:05

NlightNFotis force-pushed the flush-json-stream branch 4 times, most recently from 0086ac0 to 0a83f06 Compare February 8, 2018 19:04

peterschrammel requested changes Feb 8, 2018

View reviewed changes

peterschrammel reviewed Feb 9, 2018

View reviewed changes

src/goto-programs/json_goto_trace.h Outdated

Copy link

Member

peterschrammel Feb 9, 2018

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

There are a couple of header files that can be put into the cpp file.

NlightNFotis force-pushed the flush-json-stream branch 3 times, most recently from 268a8f5 to 7c8ea18 Compare February 9, 2018 17:41

tautschnig reviewed Feb 10, 2018

View reviewed changes

NlightNFotis force-pushed the flush-json-stream branch 4 times, most recently from 8bb7f83 to 6544980 Compare February 12, 2018 17:09

peterschrammel requested changes Feb 13, 2018

View reviewed changes

NlightNFotis force-pushed the flush-json-stream branch 2 times, most recently from 3e9a845 to fdb4576 Compare February 15, 2018 11:42

NlightNFotis force-pushed the flush-json-stream branch 2 times, most recently from 4e39f6d to e74cdf6 Compare February 21, 2018 10:04

tautschnig assigned NlightNFotis and peterschrammel Feb 21, 2018

NlightNFotis force-pushed the flush-json-stream branch from 3cedf1d to 8049ef1 Compare February 21, 2018 17:15

NlightNFotis force-pushed the flush-json-stream branch from 8049ef1 to 63140dd Compare February 22, 2018 17:01

peterschrammel approved these changes Feb 23, 2018

View reviewed changes

tautschnig requested changes Feb 23, 2018

View reviewed changes

peterschrammel reviewed Feb 24, 2018

View reviewed changes

NlightNFotis force-pushed the flush-json-stream branch from 63140dd to 4cf7dfc Compare February 27, 2018 10:25

NlightNFotis force-pushed the flush-json-stream branch from 4cf7dfc to 496476a Compare March 15, 2018 10:17

NlightNFotis added 5 commits March 15, 2018 13:41

Introduce class for streaming JSON to the output

35ac459

Introduce a new json object class that streams the object immediately to an output instead of building the object in memory and then output it to the stream.

Base JSON UI message handler upon json_streamt

a68125c

Refactor huge convert function into multiple ones

54bae24

Refactor the templated convert function with switch statements that handle different instructions to dispatch to functions that are specialised per instruction.

Activate JSON streaming when printing goto-traces

2ab3b9c

Fix goto-diff tests that got broken by streaming json

123be20

NlightNFotis force-pushed the flush-json-stream branch from 496476a to 123be20 Compare March 15, 2018 13:48

tautschnig approved these changes Mar 19, 2018

View reviewed changes

chrisr-diffblue merged commit 7f3ba30 into diffblue:develop Mar 19, 2018

NlightNFotis mentioned this pull request Mar 19, 2018

Fix for cbmc running out of memory while printing traces using json_ui #1767

Closed

tautschnig mentioned this pull request Sep 5, 2018

Do not artificially separate message handler and uit #2434

Merged

NlightNFotis deleted the flush-json-stream branch February 19, 2021 11:22

Fix for cbmc running out of memory while printing traces using json_ui / target: develop #1814

Fix for cbmc running out of memory while printing traces using json_ui / target: develop #1814

Uh oh!

Conversation

NlightNFotis commented Feb 8, 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!

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!

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!

peterschrammel commented Feb 8, 2018

Uh oh!

peterschrammel commented Feb 8, 2018

Uh oh!

Choose a reason for hiding this comment

Uh oh!

NlightNFotis commented Feb 9, 2018

Uh oh!

tautschnig left a comment

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