Add symtab2gb to enable linking of .json_symtab files #4645

hannes-steffenhagen-diffblue · 2019-05-10T11:26:30Z

Right now we have the goto-cc tool to create goto binaries from C
files and link goto binaries together. This adds a similar type of
"linker" tool for the symtab language.

I had considered extending 'goto-cc' to handle symtab files as well,
however goto-cc (quite reasonably) makes some C-specific assumptions
about its input files, and I'd figured rather than working around that
it'd be easier to just have a simple command line tool to invoke
goto_convert and link_goto_model (which, in the end, is all we want
to do for json_symtabs).

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.

src/Makefile

hannes-steffenhagen-diffblue · 2019-05-10T11:40:22Z

There's no real need to look at the .json_symtab files in the tests, they're just big generated files containing symbol tables.

xbauch

Looks good.

martin-cs · 2019-05-10T13:41:01Z

@hannes-steffenhagen-diffblue : can you elaborate a bit on why this can't be part of goto-cc? It seems that a general for / against is something like:

Where possible we want to stop the proliferation of different tools and we already have a tool which is front-end producing goto-binaries.

We may want to be able to do Ada specific linking things, particularly around the questions of elaboration order and set-up.
Other languages that use .json_symtab may also need to do custom linking things.

I would particularly like to hear from @tautschnig as the author / warden of the linker.

hannes-steffenhagen-diffblue · 2019-05-10T17:13:34Z

@martin-cs regarding Ada, I think we can get away without any special elaboration support during linking, but that's not what I mean; The problem with goto-cc is that it assumes main is the entry point to the program (which isn't true in Ada, main is just a normal identifier there), and it also replaces any __CPROVER_start which is already present with the one from ansi_c_entry_point.

I thought it'd be useful to have something that just does a straight forward combining of symbol tables, and I'm not sure if that's really compatible with goto-cc which is supposed to act like a C compiler.

martin-cs · 2019-05-11T14:45:11Z

@hannes-steffenhagen-diffblue I am not sure if it is compatible either but I think it is a discussion worth having. If I understand the points you raise correctly there are:

A. where should we do language-specific linking things?
A.1. how and by whom is the entry point specified?
A.2. what do we do about set-up code and how does that get through linking?

B. where should linking be a stand-alone tool? In goto-cc? In goto-instrument?

I think in the next few weeks and months there are likely to be Ada-specific linking things to be done (we may need to support control over elaboration orders for example), so I am not exactly clear on what the best route forward is.

I would very much appreciate thoughts from others (including, ofcourse, @hannes-steffenhagen-diffblue )

tautschnig

I'd lean towards keeping such a simple linking tool as a separate binary, because goto-cc primarily deals with the various command-line options of existing compilers, none of which is of interest here. But then I'm wondering whether the binary could just go in the existing json-symtab-language folder?

tautschnig · 2019-05-11T17:40:30Z

regression/symtab2gb/multiple_symtabs/test.desc

@@ -0,0 +1,10 @@
+CORE
+entry_point.json_symtab
+user.json_symtab library.json_symtab


Could you please add a readme file or some other explanation describing how the symtab files were generated?

tautschnig · 2019-05-11T17:40:48Z

src/CMakeLists.txt

@@ -104,3 +104,5 @@ add_subdirectory(goto-instrument)
 add_subdirectory(goto-analyzer)
 add_subdirectory(goto-diff)
 add_subdirectory(goto-harness)
+


Unnecessary blank line?

tautschnig · 2019-05-11T17:41:14Z

src/Makefile

@@ -21,6 +21,7 @@ DIRS = analyses \
       solvers \
       util \
       xmllang \
+       symtab2gb \


Sort lexicographically.

tautschnig · 2019-05-11T17:42:01Z

src/symtab2gb/symtab2gb_main.cpp

@@ -0,0 +1,113 @@
+#include <fstream>


Missing copyright header

tautschnig · 2019-05-11T17:45:02Z

src/symtab2gb/symtab2gb_main.cpp

+      throw invalid_source_file_exceptiont{
+        "failed to typecheck symbol table from file `" + symtab_filename + "'"};
+    }
+    auto goto_model = goto_modelt{};


I'd prefer goto_modelt goto_model;

I prefer the auto form because with that I can make all declarations look the same, but I don't mind changing it if it bothers you.

It does bother me, but I'm just one voice here. If others like this better then there's no need to fight about it. (I actually don't think that all declarations looking the same is desirable - quite often I don't even care much about the name, just about the type.)

tautschnig · 2019-05-11T17:45:18Z

src/symtab2gb/symtab2gb_main.cpp

+      throw invalid_source_file_exceptiont{
+        "failed to parse symbol table from file `" + symtab_filename + "'"};
+    }
+    auto symtab = symbol_tablet{};


symbol_tablet symtab;

tautschnig · 2019-05-11T17:49:34Z

src/symtab2gb/symtab2gb_main.cpp

+        if(i + 1 >= argc)
+        {
+          throw invalid_command_line_argument_exceptiont{
+            "expected output file name", "--out"};


To be honest, this is a bit too simplistic to my taste: I think this should have support for --help and --version at bare minimum. Therefore I'd recommend inheriting from parse_options_baset.

hannes-steffenhagen-diffblue · 2019-05-13T17:42:58Z

@tautschnig I believe I've addressed your review comments

martin-cs

After a discussion with @chrisr-diffblue I think this is probably the best architecture for now.

martin-cs · 2019-05-13T17:55:26Z

src/symtab2gb/symtab2gb_main.cpp

+
+int main(int argc, const char *argv[])
+{
+  symtab2gb_parse_optionst parse_options{argc, argv};


Is there a reason for { } rather than ( ) ?

Brace initialisation avoids parsing ambiguities and prevents implicit conversions, and is recommended "by default" by the CPP Core Guidelines. Unless we have a good reason my preference would be to stick to those as the 'default'.

@martin-cs Preferred since #3546

martin-cs · 2019-05-13T17:55:50Z

src/symtab2gb/symtab2gb_parse_options.cpp

+  std::ofstream out_file{gb_filename};
+  if(!out_file.is_open())
+  {
+    throw system_exceptiont{"couldn't open output file `" + gb_filename + "'"};


martin-cs · 2019-05-13T17:55:59Z

src/symtab2gb/symtab2gb_parse_options.cpp

+    std::ifstream symtab_file{symtab_filename};
+    if(!symtab_file.is_open())
+    {
+      throw system_exceptiont{"couldn't open input file `" + symtab_filename +


allredj

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

hannes-steffenhagen-diffblue · 2019-05-13T21:38:37Z

Windows tests seem to fail the goto binaries that were written aren't readable? Honestly no idea what's going on there

tautschnig · 2019-05-13T22:02:59Z

Windows tests seem to fail the goto binaries that were written aren't readable? Honestly no idea what's going on there

I looked at the code again and nothing obvious springs to my mind. I can try to play with this in a Windows environment later this week.

chrisr-diffblue · 2019-05-14T09:01:46Z

regression/symtab2gb/Makefile

+show:
+	@for dir in *; do \
+		if [ -d "$$dir" ]; then \
+			vim -o "$$dir/*.c" "$$dir/*.out"; \


$VISUAL or $EDITOR, rather than "vim" ?

The -o option is specific to vim, and it's the same bit of code we have everywhere else. But I don't know whether anyone ever users this target?!

Ah, this was the first time I've actually noticed this target - never used it myself!

Ditto on never using it. It's honestly a bit of cargo culting, I was kind of assuming someone around here liked to work that way. But I certainly don't mind removing it, I have no attachment to it.

I'd vote for having a separate PR that removes all of those. If someone is still using them, we can then have that discussion on the PR.

chrisr-diffblue · 2019-05-14T09:11:07Z

src/symtab2gb/symtab2gb_parse_options.cpp

+{
+  // try opening all the files first to make sure we can
+  // even read/write what we want
+  std::ofstream out_file{gb_filename};


Regarding your windows CI issue, does windows still care about the difference between binary and ascii file modes, and if so, what does std::ofstream do by default? I'm wondering if you need to put the stream into a binary mode?

src/goto-cc/compiler.cpp does this: std::ofstream outfile(file_name, std::ios::binary); so I suspect you might need the binary mode.

Also, do you need to explicitly close() the output file as well?

binary yes, I had not considered that at all but now that you mention it that does seem to be the kind of thing that'd cause this problem.

close I don't think so, the std streams are all RAII controlled, so they should close even on exception.

I can put the input files in a smaller scope so they get closed before the actual writing starts, although I'm not sure how much of a benefit that's going to be (I'm opening all files at the start to be as-sure-as-reasonably-possible-in-advance that our IO operations are going to succeed, so we don't go half way through the linking bit only to find one of the files is misspelled or we don't have r/w access or something like that).

Could you actually add a precondition to write_goto_binary that tests that the stream is open in binary mode?

@tautschnig AFAIK iostreams don't expose a way to query or change the openmode

allredj

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

Right now we have the `goto-cc` tool to create goto binaries from C files and link goto binaries together. This adds a similar type of "linker" tool for the symtab language. I had considered extending 'goto-cc' to handle symtab files as well, however goto-cc (quite reasonably) makes some C-specific assumptions about its input files, and I'd figured rather than working around that it'd be easier to just have a simple command line tool to invoke `goto_convert` and `link_goto_model` (which, in the end, is all we want to do for json_symtabs).

allredj

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

hannes-steffenhagen-diffblue requested review from chrisr-diffblue, kroening, peterschrammel, smowton and tautschnig as code owners May 10, 2019 11:26

hannes-steffenhagen-diffblue added the do not review label May 10, 2019

xbauch reviewed May 10, 2019

View reviewed changes

src/Makefile Outdated Show resolved Hide resolved

hannes-steffenhagen-diffblue force-pushed the feature-symtab_linking branch from 0957ef5 to 28db2e6 Compare May 10, 2019 11:35

hannes-steffenhagen-diffblue removed the do not review label May 10, 2019

xbauch approved these changes May 10, 2019

View reviewed changes

tautschnig reviewed May 11, 2019

View reviewed changes

hannes-steffenhagen-diffblue force-pushed the feature-symtab_linking branch from 11c4c40 to 5d95d11 Compare May 13, 2019 17:41

martin-cs approved these changes May 13, 2019

View reviewed changes

hannes-steffenhagen-diffblue force-pushed the feature-symtab_linking branch from 9d634c8 to 1190bcc Compare May 13, 2019 18:56

allredj reviewed May 13, 2019

View reviewed changes

chrisr-diffblue reviewed May 14, 2019

View reviewed changes

allredj reviewed May 14, 2019

View reviewed changes

chrisr-diffblue approved these changes May 14, 2019

View reviewed changes

hannes-steffenhagen-diffblue force-pushed the feature-symtab_linking branch from 10d7a51 to da5fd45 Compare May 14, 2019 14:30

allredj reviewed May 14, 2019

View reviewed changes

tautschnig merged commit 81c3e02 into diffblue:develop May 15, 2019

Add symtab2gb to enable linking of .json_symtab files #4645

Add symtab2gb to enable linking of .json_symtab files #4645

Conversation

hannes-steffenhagen-diffblue commented May 10, 2019

hannes-steffenhagen-diffblue commented May 10, 2019

xbauch left a comment

Choose a reason for hiding this comment

martin-cs commented May 10, 2019

hannes-steffenhagen-diffblue commented May 10, 2019

martin-cs commented May 11, 2019

tautschnig 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

hannes-steffenhagen-diffblue commented May 13, 2019

martin-cs left a comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

hannes-steffenhagen-diffblue May 13, 2019 • edited Loading

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

allredj left a comment

Choose a reason for hiding this comment

hannes-steffenhagen-diffblue commented May 13, 2019

tautschnig commented May 13, 2019

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

hannes-steffenhagen-diffblue May 14, 2019 • edited Loading

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

allredj left a comment

Choose a reason for hiding this comment

allredj left a comment

Choose a reason for hiding this comment

hannes-steffenhagen-diffblue May 13, 2019 •

edited

Loading

hannes-steffenhagen-diffblue May 14, 2019 •

edited

Loading