Show abstract states in program source code #3215

kroening · 2018-10-21T11:37:22Z

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).
n/a 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.

allredj

Passed Diffblue compatibility checks (cbmc commit: 7258f15).
Build URL: https://travis-ci.com/diffblue/test-gen/builds/88660117

src/goto-analyzer/show_on_source.cpp

allredj

This PR failed Diffblue compatibility checks (cbmc commit: 77e7459).
Build URL: https://travis-ci.com/diffblue/test-gen/builds/88822020
Status will be re-evaluated on next push.
Please contact @peterschrammel, @thk123, or @allredj for support.

Common spurious failures:

the cbmc commit has disappeared in the mean time (e.g. in a force-push)
the author is not in the list of contributors (e.g. first-time contributors).

The incompatibility may have been introduced by an earlier PR. In that case merging this
PR should be avoided unless it fixes the current incompatibility.

allredj

Passed Diffblue compatibility checks (cbmc commit: 70269f5).
Build URL: https://travis-ci.com/diffblue/test-gen/builds/88836441

src/util/source_location.h

src/util/source_location.cpp

src/goto-analyzer/show_on_source.cpp

kroening · 2018-10-29T15:26:25Z

Both done!

martin-cs · 2018-10-29T19:57:44Z

src/goto-analyzer/goto_analyzer_parse_options.cpp

@@ -626,7 +627,18 @@ int goto_analyzer_parse_optionst::perform_analysis(const optionst &options)

    if(options.get_bool_option("show"))
    {
-      static_show_domain(goto_model, *analyzer, options, out);
+      if(


I think I would prefer a new option for output "text-on-source" or something like that and have show_on_source just called for that. That way we maintain backwards compatibility.

Ok, it's now --show-on-source.

allredj

🚫
This PR failed Diffblue compatibility checks (cbmc commit: cf04144).
Build URL: https://travis-ci.com/diffblue/test-gen/builds/89636240
Status will be re-evaluated on next push.
Please contact @peterschrammel, @thk123, or @allredj for support.

Common spurious failures:

the cbmc commit has disappeared in the mean time (e.g. in a force-push)
the author is not in the list of contributors (e.g. first-time contributors).

The incompatibility may have been introduced by an earlier PR. In that case merging this
PR should be avoided unless it fixes the current incompatibility.

src/goto-analyzer/goto_analyzer_parse_options.cpp

allredj

⚠️
Diffblue compatibility check is currently unavailable.
Please create manual bump.
(cbmc commit: d5d204e).
Build URL: https://travis-ci.com/diffblue/test-gen/builds/90749109

src/goto-analyzer/goto_analyzer_parse_options.h

tautschnig · 2018-11-08T19:09:25Z

src/goto-analyzer/goto_analyzer_parse_options.cpp

@@ -800,7 +811,8 @@ void goto_analyzer_parse_optionst::help()
    " goto-analyzer file.c ...     source file names\n"
    "\n"
    "Task options:\n"
-    " --show                       display the abstract domains\n"
+    " --show                       display the abstract states on the goto program\n"


Suggested change

" --show display the abstract states on the goto program\n"

// NOLINTNEXTLINE(whitespace/line_length)

" --show display the abstract states on the goto program\n"

The abstract states are shown in a different color on the source code text of the program, as opposed to the goto-program dump. Indentation of the output of the abstract is made to match the indentation of the source code.

allredj

⚠️
Diffblue compatibility check is currently unavailable.
Please create manual bump.
(cbmc commit: 5dd3760).
Build URL: https://travis-ci.com/diffblue/test-gen/builds/90819223

Co-Authored-By: kroening <[email protected]>

allredj

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

chrisr-diffblue

Looks good, and a nice feature.

martin-cs · 2018-11-16T11:38:01Z

src/goto-analyzer/show_on_source.cpp

+{
+  const auto abstract_state = ai.abstract_state_before(loc);
+  if(abstract_state->is_top())
+    return {};


This doesn't match the name of the function or the documentation; why should the file name depend on the domain?

martin-cs

I'm happy with the way this is implemented. I'm ... undecided on the change in the usage model. My understanding is that the usage model of CPROVER has been very much pipeline : you need the source to create the goto-program but after that you don't need it any more. This then loops back around and changes the relationship between analysis results and code. This is not a bad thing but it is a change of abstraction / architecture. If we are going to go this way (and I am not for or against doing so at this stage) then we should probably think about the consequences / necessary architectural changes. For example, do we need to store / be able to do byte-exact reconstruction of source from goto-programs?

So, I think the answer is merge this and if we find that we're adding lots more features, think about changing the architecture.

kroening · 2018-11-18T09:50:11Z

Yes, we do want pipeline! However, note that "view abstract fixedpoint on source code" is still very much a feature aimed at developers of analysis tools, as opposed to users, so if this gets broken by some transformation it's not a big deal. You'll then have to view using the goto-program, which is what we currently do.

kroening added enhancement Static Analyses labels Oct 21, 2018

kroening requested review from smowton and martin-cs October 21, 2018 11:37

kroening requested review from chrisr-diffblue and peterschrammel as code owners October 21, 2018 11:37

kroening force-pushed the show-ai-on-source branch from 38b0695 to 3004c58 Compare October 21, 2018 11:40

kroening requested review from cesaro, cristina-david and pkesseli as code owners October 21, 2018 11:40

kroening force-pushed the show-ai-on-source branch 2 times, most recently from c63de97 to 7258f15 Compare October 21, 2018 15:04

allredj reviewed Oct 21, 2018

View reviewed changes

tautschnig reviewed Oct 22, 2018

View reviewed changes

tautschnig assigned kroening Oct 22, 2018

tautschnig added the Needs rebase label Oct 22, 2018

kroening force-pushed the show-ai-on-source branch 2 times, most recently from d8faf32 to 77e7459 Compare October 23, 2018 09:04

kroening removed the Needs rebase label Oct 23, 2018

kroening force-pushed the show-ai-on-source branch from 77e7459 to fb8bffa Compare October 23, 2018 09:16

kroening assigned tautschnig and unassigned kroening Oct 23, 2018

allredj reviewed Oct 23, 2018

View reviewed changes

kroening force-pushed the show-ai-on-source branch from fb8bffa to 70269f5 Compare October 23, 2018 11:13

allredj reviewed Oct 23, 2018

View reviewed changes

tautschnig reviewed Oct 24, 2018

View reviewed changes

src/util/source_location.h Outdated Show resolved Hide resolved

src/util/source_location.cpp Outdated Show resolved Hide resolved

src/goto-analyzer/show_on_source.cpp Outdated Show resolved Hide resolved

tautschnig assigned kroening and unassigned tautschnig Oct 24, 2018

kroening force-pushed the show-ai-on-source branch from 70269f5 to ed7da5b Compare October 24, 2018 16:34

kroening removed their assignment Oct 24, 2018

tautschnig assigned chrisr-diffblue Oct 29, 2018

kroening force-pushed the show-ai-on-source branch from b8f7688 to 4598b6b Compare October 29, 2018 15:26

martin-cs requested changes Oct 29, 2018

View reviewed changes

kroening force-pushed the show-ai-on-source branch from 4598b6b to cf04144 Compare October 30, 2018 09:02

allredj reviewed Oct 30, 2018

View reviewed changes

tautschnig unassigned peterschrammel, chrisr-diffblue and martin-cs Oct 30, 2018

kroening force-pushed the show-ai-on-source branch 3 times, most recently from 05a5c0c to d5d204e Compare November 8, 2018 15:14

tautschnig reviewed Nov 8, 2018

View reviewed changes

src/goto-analyzer/goto_analyzer_parse_options.cpp Show resolved Hide resolved

allredj reviewed Nov 8, 2018

View reviewed changes

kroening force-pushed the show-ai-on-source branch from d5d204e to 38d0fa0 Compare November 8, 2018 18:41

kroening assigned martin-cs and unassigned kroening Nov 8, 2018

tautschnig reviewed Nov 8, 2018

View reviewed changes

added show_on_source for abstract domains

5dd3760

The abstract states are shown in a different color on the source code text of the program, as opposed to the goto-program dump. Indentation of the output of the abstract is made to match the indentation of the source code.

kroening force-pushed the show-ai-on-source branch from 38d0fa0 to 5dd3760 Compare November 9, 2018 07:12

allredj reviewed Nov 9, 2018

View reviewed changes

Update src/goto-analyzer/goto_analyzer_parse_options.h

3658167

Co-Authored-By: kroening <[email protected]>

allredj reviewed Nov 10, 2018

View reviewed changes

chrisr-diffblue approved these changes Nov 14, 2018

View reviewed changes

peterschrammel approved these changes Nov 14, 2018

View reviewed changes

martin-cs reviewed Nov 16, 2018

View reviewed changes

martin-cs approved these changes Nov 16, 2018

View reviewed changes

kroening merged commit 6747d24 into develop Nov 18, 2018

kroening deleted the show-ai-on-source branch November 18, 2018 09:50

	" --show display the abstract states on the goto program\n"
	// NOLINTNEXTLINE(whitespace/line_length)
	" --show display the abstract states on the goto program\n"

Show abstract states in program source code #3215

Show abstract states in program source code #3215

Uh oh!

Conversation

kroening commented Oct 21, 2018 • edited Loading Uh oh! There was an error while loading. Please reload this page.

Uh oh!

Uh oh!

allredj left a comment

Choose a reason for hiding this comment

Uh oh!

Uh oh!

Uh oh!

Uh oh!

Uh oh!

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!

Uh oh!

Uh oh!

kroening commented Oct 29, 2018

Uh oh!

martin-cs Oct 29, 2018

Choose a reason for hiding this comment

Uh oh!

kroening Nov 8, 2018

Choose a reason for hiding this comment

Uh oh!

allredj left a comment

Choose a reason for hiding this comment

Uh oh!

Uh oh!

allredj left a comment

Choose a reason for hiding this comment

Uh oh!

Uh oh!

tautschnig Nov 8, 2018

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!

chrisr-diffblue left a comment

Choose a reason for hiding this comment

Uh oh!

martin-cs Nov 16, 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!

martin-cs left a comment

Choose a reason for hiding this comment

Uh oh!

kroening commented Nov 18, 2018

Uh oh!

Uh oh!

kroening commented Oct 21, 2018 •

edited

Loading

martin-cs Nov 16, 2018 •

edited

Loading