Adding initial version of `goto-inspect`. #7673

NlightNFotis · 2023-04-19T08:58:01Z

This allows to inspect a goto-binary (this means showing the goto-functions, for now at least).

The reason this binary is helpful is that different tools (CBMC, goto-instrument, etc) perform instrumentation before showing the goto-functions, and there's a need to be able to inspect certain properties of a goto-binary without doing instrumentation.

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.
The feature or user visible behaviour I have added or modified has been documented in the User Guide in doc/cprover-manual/
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.

martin-cs · 2023-04-19T09:17:58Z

How different is this to just using goto-instrument --show-goto-programs ?

martin-cs · 2023-04-19T09:20:43Z

Apologies, I hadn't seen #7674, will discuss there.

codecov · 2023-04-19T09:54:12Z

Codecov Report

Patch coverage: 59.45% and project coverage change: +0.13 🎉

Comparison is base (68af7a4) 78.42% compared to head (13997e0) 78.55%.

❗ Current head 13997e0 differs from pull request most recent head 7724092. Consider uploading reports for the commit 7724092 to get more accurate results

Additional details and impacted files

@@             Coverage Diff             @@
##           develop    #7673      +/-   ##
===========================================
+ Coverage    78.42%   78.55%   +0.13%     
===========================================
  Files         1674     1689      +15     
  Lines       191935   192964    +1029     
===========================================
+ Hits        150521   151582    +1061     
+ Misses       41414    41382      -32

Impacted Files	Coverage Δ
src/goto-inspect/goto_inspect_parse_options.cpp	`55.88% <55.88%> (ø)`
src/goto-inspect/goto_inspect_main.cpp	`100.00% <100.00%> (ø)`
src/goto-inspect/goto_inspect_parse_options.h	`100.00% <100.00%> (ø)`

... and 94 files with indirect coverage changes

☔ View full report in Codecov by Sentry.
📢 Do you have feedback about the report comment? Let us know in this issue.

tautschnig · 2023-04-20T12:21:19Z

Please take a look at #7415, which is the most recent new tool that was added and is much more complete in what it takes to add a new tool.

NlightNFotis · 2023-05-02T09:25:52Z

Hi Michael (@tautschnig), latest commit should have everything that has been asked.

Let me know if this is closer to what you envisioned.

thomasspriggs

Looks reasonable to me, aside from a few minor issues.

thomasspriggs · 2023-05-02T11:24:15Z

src/goto-inspect/CMakeLists.txt

+install(TARGETS goto-inspect DESTINATION ${CMAKE_INSTALL_BINDIR})
+
+# # Man page
+# if(NOT WIN32)


Why is this commented out?

Good catch - it shouldn't be commented out.

It was in the first commit, when we didn't have a man page at first, but now we do.

thomasspriggs · 2023-05-02T11:25:48Z

CMakeLists.txt

    goto-harness
+    goto-inspect


Nitpick: duplication

Good catch.

thomasspriggs · 2023-05-02T11:34:37Z

src/goto-inspect/goto_inspect_parse_options.cpp

+  // This just sets up the defaults (and would interpret options such as --32).
+  config.set(cmdline);
+
+  // Normally we would register language front-ends here but as goto-harness


Should "goto-harness" here be "goto-inspect"?

Yes, this was a copy-paste fail.

I used the code under src/goto-harness as the base for a lot of what you're seeing here, but it seems like I forgot to update some of the references.

Will have another look myself, just to make sure.

TGWDB · 2023-05-10T10:21:45Z

doc/man/goto-inspect.1

@@ -0,0 +1,33 @@
+.TH GOTO-INSPECT "2" "May 2023" "goto-inspect-5.81.0" "User Commands"


Probably not worth pinning a date/version here.

This reference leads me to believe that the date is necessary in the title line.

It does look like the date we have though doesn't align with the proposed format in the reference I linked. I'm not sure how the tools behave if I leave it with an empty date, but it seems to be diverging from the expected format too much IMO.

TGWDB · 2023-05-10T10:22:00Z

doc/man/goto-inspect.1

+.BR goto-cc (1)
+.BR goto-instrument (1)
+.SH COPYRIGHT
+2023, Fotis Koutoulakis


Copyright is Diffblue I believe.

You are right - I copied and hastily changed this from a previous one, so I've made a number of mistakes.

I'm fixing now.

TGWDB · 2023-05-10T10:25:49Z

src/goto-inspect/goto_inspect_parse_options.cpp

+  // Before we do anything else, positional arguments needs to be > 1.
+  // (i.e. a filename has been given).
+  if(cmdline.args.size() < 1)
+  {
+    help();
+    throw invalid_command_line_argument_exceptiont{
+      "failed to supply a goto-binary name",
+      "<input goto-binary> <inspection-option>"};
+  }


This looks like it should be > 2 and < 2 since we require a binary name and another option?

Maybe we also need a code path before this to response to the --help option.

This looks like it should be > 2 and < 2 since we require a binary name and another option?

Yes, changed to > 2. With the current implementation, if just a binary is given, the behaviour is that the tool doesn't appear to do anything. It's reasonable in my opinion, but not very helpful, as it doesn't indicate to the user whether it succeeded or failed, or what.

Maybe we also need a code path before this to response to the --help option.

We don't need to do that, as it's handled already by the base class parse_options_baset::main(), where it's checking for h or help before calling doit().

TGWDB · 2023-05-10T10:27:34Z

src/goto-inspect/goto_inspect_parse_options.cpp

+  // No options was passed in - erroneously?
+  return CPROVER_EXIT_INCORRECT_TASK;


The failure for lack of an option should be caught/reported earlier as in comment above, so this code path should perhaps be unreachable?

It should be unreachable - I have added a lengthier comment addressing why the value is there, in order not to confuse people. Let me know if it now makes more sense.

TGWDB · 2023-05-18T09:58:16Z

src/goto-inspect/goto_inspect_parse_options.cpp

@@ -63,7 +63,14 @@ int goto_inspect_parse_optionst::doit()
    return CPROVER_EXIT_SUCCESS;
  }

-  // No options was passed in - erroneously?
+  // If an option + binary was provided, the program will have exited gracefully
+  // through different a different branch. If we hit the code below, it means


"different a different" -> "a different"

kroening · 2023-05-18T14:22:30Z

May I suggest that you consider the user interface. In particular, consider swapping the order of the command line arguments.

All command line tools that I can think of have the order "action" and then "file name". E.g., think git add some_file.cpp, or maybe tar tfz tarball.tgz.

NlightNFotis · 2023-05-18T14:35:58Z

Hi @kroening, I'm working on adding tests (didn't want to commit to writing tests before there's conclusion that the approach is not objectionable to people) and during the authoring of tests I have discovered some issues with the interface that led me to rethink the approach.

Will update the PR as soon as my current change is stable and the interface is smoother.

NlightNFotis · 2023-05-19T15:02:19Z

Hi @kroening, I've had some more time to play around with this, and it doesn't have any particular dependency on the order of arguments, i.e. both: goto-inspect --show-goto-functions example.goto and goto-inspect example.goto --show-goto-functions will work.

peterschrammel

The individual commits are not very clean. I suggest to squash them as they all fix up earlier commits of the same PR.

peterschrammel · 2023-05-19T15:12:37Z

src/goto-inspect/goto_inspect_parse_options.cpp

+
+  if(
+    cmdline.isset("show-goto-functions") ||
+    cmdline.isset("list-goto-functions"))


This alias is not configured in GOTO_INSPECT_OPTIONS.

NlightNFotis · 2023-05-19T15:30:58Z

Squashed the commits down to one.

kroening · 2023-05-19T16:05:01Z

Hi @kroening, I've had some more time to play around with this, and it doesn't have any particular dependency on the order of arguments, i.e. both: goto-inspect --show-goto-functions example.goto and goto-inspect example.goto --show-goto-functions will work.

I got thrown off by your comment "Yes, changed to > 2" -- this is outdated?

NlightNFotis · 2023-05-22T17:06:37Z

Hi @kroening,

I got thrown off by your comment "Yes, changed to > 2" -- this is outdated?

Yes. Thomas had asked if I can tighten the error checking there, which I initially did by checking that the cmdline.args > 2 (1 for the filename and 1 for the option). After some experimenting during the addition of tests, I found out that the initial approach was (more) correct because cmdline.args contains the positional arguments of the program, with the optional ones being added to the cmdline.options vector (so if you issue, for example, $ goto-inspect --show-goto-functions example.gb, the option --show-goto-functions won't be present in the cmdline.args, and cmdline.args == 1 holds)

At that point, I changed it to check that we always get one positional argument (based on the fact that the tool, for now, operates on one goto-binary at a time) before we do anything, and dispatches to various inspection options based on them being set and the above precondition (at least 1 positional argument, i.e. 1 goto-binary filename) holds.

If the positional argument doesn't correspond to a goto-binary, we get an error that the program failed to read a goto-binary.

This allows to inspect a goto-binary (this means showing the goto-functions, for now at least). The reason this binary is helpful is that different tools (CBMC, goto-instrument, etc) perform instrumentation before showing the goto-functions, and there's a need to be able to inspect certain properties of a goto-binary without doing instrumentation.

NlightNFotis self-assigned this Apr 19, 2023

NlightNFotis mentioned this pull request Apr 19, 2023

New binary for inspection of properties of goto-programs: goto-inspect #7674

Open

NlightNFotis force-pushed the goto-inspect branch from 4901439 to d7dc025 Compare May 2, 2023 09:47

NlightNFotis marked this pull request as ready for review May 2, 2023 09:47

NlightNFotis requested review from a team, jimgrundy, TGWDB, kroening, tautschnig, peterschrammel and chris-ryder as code owners May 2, 2023 09:47

NlightNFotis force-pushed the goto-inspect branch from d7dc025 to 7c90a0e Compare May 2, 2023 09:58

thomasspriggs reviewed May 2, 2023

View reviewed changes

NlightNFotis force-pushed the goto-inspect branch 2 times, most recently from 306ea84 to 075630b Compare May 3, 2023 09:51

thomasspriggs approved these changes May 9, 2023

View reviewed changes

TGWDB reviewed May 10, 2023

View reviewed changes

TGWDB approved these changes May 18, 2023

View reviewed changes

NlightNFotis force-pushed the goto-inspect branch 2 times, most recently from 2aaaac2 to b79bfaa Compare May 18, 2023 10:02

NlightNFotis force-pushed the goto-inspect branch 2 times, most recently from ac8c34a to 13997e0 Compare May 19, 2023 14:59

peterschrammel approved these changes May 19, 2023

View reviewed changes

NlightNFotis force-pushed the goto-inspect branch 3 times, most recently from c7e67aa to 5cffca7 Compare May 19, 2023 15:30

NlightNFotis enabled auto-merge May 19, 2023 15:31

NlightNFotis force-pushed the goto-inspect branch from 5cffca7 to ac30b42 Compare May 22, 2023 16:57

NlightNFotis force-pushed the goto-inspect branch from ac30b42 to 52b31f5 Compare May 22, 2023 17:27

NlightNFotis force-pushed the goto-inspect branch from 52b31f5 to 7724092 Compare May 23, 2023 14:54

NlightNFotis merged commit 1ad9a76 into diffblue:develop May 23, 2023

NlightNFotis deleted the goto-inspect branch May 23, 2023 17:01

Provide feedback

Saved searches

Use saved searches to filter your results more quickly

Adding initial version of `goto-inspect`. #7673

Adding initial version of `goto-inspect`. #7673

NlightNFotis commented Apr 19, 2023

martin-cs commented Apr 19, 2023

martin-cs commented Apr 19, 2023

codecov bot commented Apr 19, 2023 •

edited

Loading

tautschnig commented Apr 20, 2023

NlightNFotis commented May 2, 2023

thomasspriggs left a comment

thomasspriggs May 2, 2023

NlightNFotis May 2, 2023

thomasspriggs May 2, 2023

NlightNFotis May 2, 2023

thomasspriggs May 2, 2023

NlightNFotis May 2, 2023

TGWDB May 10, 2023

NlightNFotis May 18, 2023

TGWDB May 10, 2023

NlightNFotis May 18, 2023

TGWDB May 10, 2023

NlightNFotis May 18, 2023

TGWDB May 10, 2023

NlightNFotis May 18, 2023

TGWDB May 18, 2023

NlightNFotis May 18, 2023

kroening commented May 18, 2023

NlightNFotis commented May 18, 2023

NlightNFotis commented May 19, 2023

peterschrammel left a comment

peterschrammel May 19, 2023

NlightNFotis May 19, 2023

NlightNFotis commented May 19, 2023

kroening commented May 19, 2023

NlightNFotis commented May 22, 2023

		@@ -0,0 +1,33 @@
		.TH GOTO-INSPECT "2" "May 2023" "goto-inspect-5.81.0" "User Commands"

		// No options was passed in - erroneously?
		return CPROVER_EXIT_INCORRECT_TASK;

Adding initial version of goto-inspect. #7673

Adding initial version of goto-inspect. #7673

Conversation

NlightNFotis commented Apr 19, 2023

martin-cs commented Apr 19, 2023

martin-cs commented Apr 19, 2023

codecov bot commented Apr 19, 2023 • edited Loading

Codecov Report

tautschnig commented Apr 20, 2023

NlightNFotis commented May 2, 2023

thomasspriggs 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

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

kroening commented May 18, 2023

NlightNFotis commented May 18, 2023

NlightNFotis commented May 19, 2023

peterschrammel left a comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

NlightNFotis commented May 19, 2023

kroening commented May 19, 2023

NlightNFotis commented May 22, 2023

Adding initial version of `goto-inspect`. #7673

Adding initial version of `goto-inspect`. #7673

codecov bot commented Apr 19, 2023 •

edited

Loading