hide internal symbols in the goto trace #1272

tautschnig · 2017-08-22T15:03:32Z

None of this is my work - these are commits already merged into develop (test-gen-support).

…est-gen-support set internal for variable assignments related to dynamic_object[0-9], dynamic_[0-9]_array, _start function-return step, and CPROVER internal functions (e.g., __CPROVER_initialize). This PR fixes diffblue/test-gen#20.

Added internal field to json output so that we set it to tru as we find some specific variable that is not supposed to be shown in the counterexample trace.

Fixes issue https://github.com/diffblue/test-gen/issues/334. The patch avoids marking any steps in _start whose source is a code_function_callt, which includes the main function call and its argument assignments. Internal function calls in _start (e.g. __CPROVER_initialize) are marked by previous checks. Includes a minimal test case from https://github.com/DiffBlue-benchmarks/java-test which sparked the issue.

pkesseli

I added the function call check on 163 to 170 and the regression test. Both look good.

pkesseli · 2017-08-24T14:00:15Z

src/goto-symex/build_goto_trace.cpp

+  if(SSA_step.is_function_call())
+  {
+    if(SSA_step.source.pc->source_location.as_string().empty())
+      goto_trace_step.internal=true;


Perhaps return after setting internal to true?

pkesseli · 2017-08-24T14:00:22Z

src/goto-symex/build_goto_trace.cpp

+  if(goto_trace_step.type==goto_trace_stept::typet::OUTPUT ||
+      goto_trace_step.type==goto_trace_stept::typet::INPUT)
+  {
+    goto_trace_step.internal=true;


Perhaps return after setting internal to true?

pkesseli

I added the function call check on 163 to 170 and the regression test. Both look good.

lucasccordeiro

LGTM

tautschnig · 2017-09-02T10:30:56Z

To be honest, I'm failing to understand what these commits are trying to achieve. There may be a clue in https://github.com/diffblue/test-gen/issues/20, but it's not public so I can't tell.

If it helps, #709 is the main original PR, but it doesn't have much of a discussion. My main question is: how is "internal" different from "hidden"? @lucasccordeiro @peterschrammel @pkesseli any insights? Thanks!

As a side note: I would have additional cleanup ready to go, following @pkesseli's suggestions. But doing this work made me wonder what's actually going on here.

Another note: this is blocking a series of further PRs to go into master.

kroening · 2017-09-03T07:52:49Z

The management of 'hiding steps' on the trace appears to be way to late to me. This PR seems to be a hack to me.

lucasccordeiro · 2017-09-04T07:44:42Z

The UI team requested us to hide the dynamic_object and CPROVER internal functions (e.g., __CPROVER_initialize) from the CBMC counterexample. In order to keep compatibility, we decided to add the internal field to the JSON output so that the dynamic_object and CPROVER internal functions could be easily hidden in the UI application.

tautschnig · 2017-09-04T09:01:22Z

Thanks a lot for the input. I do not have sufficient state on customers to tell whether anyone does depend on those bits not being hidden and thus call out to @kroening for clarification. One of two things need to happen: either this feature needs to be documented properly to make clear what is "hidden" vs what is "internal", or "internal" should be removed and those bits simply be "hidden." Assigning to @kroening to request guidance.

peterschrammel · 2017-09-04T09:52:21Z

See also #1311

peterschrammel · 2017-09-04T09:52:25Z

I investigated this further:

Current sources of hidden:

goto_functionst::type has a hidden attribute that is set if the function contains a __CPROVER_hide label
symbols with #return_value! (sic) suffixes are hidden in symex_assign
assignment steps with source locations with hide attribute set are hidden in symex_assign (but this seems to be used only in goto_inline where the code setting it is deactivated)
declaration steps are set hidden if the identifier symbol is_auxiliary

Current uses of hidden:

hidden steps are hidden in show_goto_trace in the plain text output
hidden steps are hidden in graphml output.
hidden are not instrumented in cover

The purpose of hidden is to hide steps in the trace,
whereas the purpose of internalis to label all lhs symbols that are not known to occur in the user's program. The two notions do not coincide for dynamic objects, for example.

kroening · 2017-09-04T17:15:56Z

Ok, so "internal" is a property of a variable symbol, and not a property of a program step.

Would it not be better to have a namespace for the internal symbols?

Or we may wish to output a symbol table with the trace?

tautschnig · 2017-10-23T08:08:47Z

@peterschrammel Would you be able to take a lead on this issue? This seems to be one that needs careful consideration within Diffblue. (And it is one of the blockers for progress on the develop->master transition.)

peterschrammel · 2017-10-23T08:26:59Z

@tautschnig, yes.

peterschrammel · 2017-10-23T08:30:07Z

@kroening, yes, it's true that internal is a property of a symbol rather than a step.
Yet, the symbols we have to know about are exactly those occurring in lhs of assignments in the trace (not everything in the symbol table). Therefore it seemed more appropriate to attach the information to the trace steps.

We could output a list of non-internal symbols if this is less contentious.

tautschnig · 2017-11-09T14:53:58Z

Had some further out-of-band discussion with @peterschrammel on this. Taking this onto my stack of tasks in order to clean it up/take it further.

tautschnig · 2018-02-23T07:26:33Z

While the develop->master transition might not happen as originally planned, this PR still includes a significant discussion about "internal" symbols. To be resolved by @peterschrammel and myself.

NlightNFotis · 2021-02-24T10:28:40Z

Hi @tautschnig, is that still something we want to push through?

This looks in a relatively good state (no merge conflicts and approved by other contributors) but it will need some work still (it adds a file to regression/cbmc-java that no longer appears to be there (I'm assuming it's under jbmc/ somewhere).

NlightNFotis · 2021-02-24T14:29:10Z

Also, I just noticed - this is merging to master, not develop.

Is that still something we want?

martin-cs · 2021-02-24T14:55:18Z

@NlightNFotis the PR or the master branch in general. I think both are valid questions but I think the later one probably needs an issue of it's own.

NlightNFotis · 2021-02-25T10:31:12Z

@martin-cs I'm talking about both.

Do we want to go through with the PR in general? Is this adding value? It looks in a better state than most other old PRs, but I realised that's probably because it's targeting master which hasn't seen action in months (probably years) so that's why there's probably no conflicts.
Should we even be targeting master with PRs? My understanding is that we are using develop as our master (sort of) and any merge to master should be using develop as the source. Is that a fair statement?

By the way I looked into the code changes a bit, and they appear to be replicated in develop in any case, so maybe this PR is wholly obsolete?

martin-cs · 2021-02-25T22:07:29Z

I think having some way to hide purely internal things in the traces is useful, esp. as they are getting larger. As the discussion says, it would be best to have 1 way of doing this, not lots.
I wasn't at the meeting where the master / develop split was proposed but my understanding is that the original idea was that develop would move faster and things would be cherry-picked across to master when they were of sufficient quality. Releases would then be from master. I think. master has stagnated so much and releases are now from develop so ... I don't really see there being much point in having the master branch at all.

The comment at the top does suggest it is already in develop. I guess this might have been part of the "feeding changes back from develop to master" process. Maybe @tautschnig knows?

peterschrammel · 2021-02-25T22:39:53Z

There was once a plan to merge releases from develop into master so that the head of master is always the last (stable) release version, but we never really started doing that and created releases from develop instead. Atm the master branch is completely stale, so merging PRs into it is pointless.

peterschrammel · 2021-02-25T22:42:24Z

Based on #1272 (comment), #1272 (comment) and #1272 (comment) the management of hiding steps needs a complete overhaul.

TGWDB · 2021-08-05T10:39:58Z

Based on #1272 (comment), #1272 (comment) and #1272 (comment) the management of hiding steps needs a complete overhaul.

Based on this and the general concerns with this PR I'm closing it. While this does not resolve the question of hiding some internal symbols in the trace, since this PR is out of date, badly targeted, and not doing the hiding right anyway, it seems pointless to keep it open. Please create a new PR with a better approach (or create an RFC if you wish to discuss) for addressing the underlying problem in future. (Note that this PR can still be observed/referenced, closing only since it is not going to be merged/continued in it's current state.)

lucasccordeiro and others added 3 commits August 22, 2017 16:01

added internal field to json output

335d815

Added internal field to json output so that we set it to tru as we find some specific variable that is not supposed to be shown in the counterexample trace.

tautschnig requested review from lucasccordeiro and pkesseli August 22, 2017 15:03

peterschrammel approved these changes Aug 22, 2017

View reviewed changes

tautschnig assigned kroening Aug 23, 2017

pkesseli reviewed Aug 24, 2017

View reviewed changes

pkesseli approved these changes Aug 24, 2017

View reviewed changes

lucasccordeiro approved these changes Aug 30, 2017

View reviewed changes

tautschnig added the develop->master label Sep 2, 2017

tautschnig changed the title ~~[develop->master] hide internal symbols in the goto trace~~ hide internal symbols in the goto trace Sep 2, 2017

tautschnig assigned lucasccordeiro, peterschrammel and pkesseli Sep 2, 2017

tautschnig unassigned kroening Sep 3, 2017

peterschrammel mentioned this pull request Sep 3, 2017

Refactor system_library_symbolst to support languages beyond C #1311

Closed

tautschnig assigned kroening and unassigned lucasccordeiro, peterschrammel and pkesseli Sep 4, 2017

kroening added the do not merge label Sep 6, 2017

kroening removed their assignment Sep 7, 2017

kroening assigned peterschrammel Sep 7, 2017

tautschnig assigned tautschnig and unassigned peterschrammel Nov 9, 2017

tautschnig assigned peterschrammel Feb 23, 2018

tautschnig mentioned this pull request Apr 26, 2018

Lazy methods: allow driver program to provide stubs #2124

Merged

martin-cs mentioned this pull request Jul 13, 2020

Hidden attribute for malloc is inconsistent in traces #5413

Closed

TGWDB closed this Aug 5, 2021

Provide feedback

Saved searches

Use saved searches to filter your results more quickly

hide internal symbols in the goto trace #1272

hide internal symbols in the goto trace #1272

tautschnig commented Aug 22, 2017

pkesseli left a comment

pkesseli Aug 24, 2017

pkesseli Aug 24, 2017

pkesseli left a comment

lucasccordeiro left a comment

tautschnig commented Sep 2, 2017 •

edited

Loading

kroening commented Sep 3, 2017

lucasccordeiro commented Sep 4, 2017

tautschnig commented Sep 4, 2017

peterschrammel commented Sep 4, 2017

peterschrammel commented Sep 4, 2017 •

edited

Loading

kroening commented Sep 4, 2017

tautschnig commented Oct 23, 2017

peterschrammel commented Oct 23, 2017

peterschrammel commented Oct 23, 2017 •

edited

Loading

tautschnig commented Nov 9, 2017

tautschnig commented Feb 23, 2018

NlightNFotis commented Feb 24, 2021

NlightNFotis commented Feb 24, 2021

martin-cs commented Feb 24, 2021

NlightNFotis commented Feb 25, 2021

martin-cs commented Feb 25, 2021

peterschrammel commented Feb 25, 2021

peterschrammel commented Feb 25, 2021

TGWDB commented Aug 5, 2021

hide internal symbols in the goto trace #1272

hide internal symbols in the goto trace #1272

Conversation

tautschnig commented Aug 22, 2017

pkesseli left a comment

Choose a reason for hiding this comment

pkesseli Aug 24, 2017

Choose a reason for hiding this comment

pkesseli Aug 24, 2017

Choose a reason for hiding this comment

pkesseli left a comment

Choose a reason for hiding this comment

lucasccordeiro left a comment

Choose a reason for hiding this comment

tautschnig commented Sep 2, 2017 • edited Loading

kroening commented Sep 3, 2017

lucasccordeiro commented Sep 4, 2017

tautschnig commented Sep 4, 2017

peterschrammel commented Sep 4, 2017

peterschrammel commented Sep 4, 2017 • edited Loading

kroening commented Sep 4, 2017

tautschnig commented Oct 23, 2017

peterschrammel commented Oct 23, 2017

peterschrammel commented Oct 23, 2017 • edited Loading

tautschnig commented Nov 9, 2017

tautschnig commented Feb 23, 2018

NlightNFotis commented Feb 24, 2021

NlightNFotis commented Feb 24, 2021

martin-cs commented Feb 24, 2021

NlightNFotis commented Feb 25, 2021

martin-cs commented Feb 25, 2021

peterschrammel commented Feb 25, 2021

peterschrammel commented Feb 25, 2021

TGWDB commented Aug 5, 2021

tautschnig commented Sep 2, 2017 •

edited

Loading

peterschrammel commented Sep 4, 2017 •

edited

Loading

peterschrammel commented Oct 23, 2017 •

edited

Loading