Skip to content

Fixup e59511c9168f04cb21e85642aa8875c1cb4b4 #2964

New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Jump to bottom
Merged
merged 2 commits into from
Sep 22, 2018
Merged

Fixup e59511c9168f04cb21e85642aa8875c1cb4b4 #2964

merged 2 commits into from
Sep 22, 2018

Conversation

kroening
Copy link
Member

read_goto_binary does not set the config; only read_object_and_link does that.

Fixes issue #2949

peterschrammel
peterschrammel approved these changes Sep 15, 2018
View reviewed changes
Copy link
Member

@peterschrammel peterschrammel left a comment

Choose a reason for hiding this comment

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

If possible, add the test that exposed the issue.

allredj
allredj reviewed Sep 15, 2018
View reviewed changes
Copy link
Contributor

@allredj allredj left a comment

Choose a reason for hiding this comment

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

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

@kroening
Copy link
Member Author

The test is not trivial with our current scripts; in particular, it would fail on anything other than x86/i386.

@peterschrammel
Copy link
Member

Ok, needs a rebase.

tautschnig
tautschnig requested changes Sep 18, 2018
View reviewed changes
src/goto-programs/read_goto_binary.h Outdated
@@ -19,25 +19,33 @@ class goto_modelt;
class message_handlert;
class symbol_tablet;

// Read given goto binary
// Does not update config
Copy link
Collaborator

Choose a reason for hiding this comment

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

Could the documentation please be placed with the definition and use Doxygen style?

src/goto-instrument/goto_instrument_parse_options.cpp
@@ -898,11 +898,13 @@ void goto_instrument_parse_optionst::get_goto_program()
{
status() << "Reading GOTO program from `" << cmdline.args[0] << "'" << eom;

config.set(cmdline);

Copy link
Collaborator

Choose a reason for hiding this comment

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

Is this actually necessary/useful at all? AFAIK the config will be overwritten below?

Copy link
Member Author

Choose a reason for hiding this comment

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

Yes, but not all of it -- only what is called 'architectural configuration'. Say include paths aren't.

src/goto-instrument/goto_instrument_parse_options.cpp Outdated
if(read_goto_binary(cmdline.args[0],
goto_model, get_message_handler()))
throw 0;

config.set(cmdline);
config.set_from_symbol_table(goto_model.symbol_table);
Copy link
Collaborator

Choose a reason for hiding this comment

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

We might need a custom wrapper script to test this, but some tests certainly seem necessary. In particular, the command-line should actually be ignored.

@kroening kroening force-pushed the fixup-e59511c9168f04cb21e85642aa8875c1cb4b4 branch from e7cc22e to a816370 Compare September 18, 2018 17:07
allredj
allredj reviewed Sep 18, 2018
View reviewed changes
Copy link
Contributor

@allredj allredj left a comment

Choose a reason for hiding this comment

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

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

@tautschnig
Copy link
Collaborator

May I suggest that, in place of a proper CI-ed test, the commit message of the second commit describe in detail a workflow that failed before and works now?

@kroening kroening force-pushed the fixup-e59511c9168f04cb21e85642aa8875c1cb4b4 branch from a816370 to 6aa7d25 Compare September 20, 2018 07:17
@kroening
Copy link
Member Author

ok, done

@kroening
Copy link
Member Author

There is temptation to allow regression tests that are arbitrary shell scripts; my main fear is that we'll have tests that nobody can debug anymore.

tautschnig
tautschnig reviewed Sep 20, 2018
View reviewed changes
Copy link
Collaborator

@tautschnig tautschnig left a comment

Choose a reason for hiding this comment

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

Both ends of the spectrum:

  1. I really like how the commit message has been extended (with the minor note that mentioning 32 vs. 64 bit architecture seems necessary). I think this is a better route than coming up with arbitrary test scripts, even though it would mean we don't catch such problems in CI for now.
  2. The comments added need a big overhaul.

src/goto-programs/read_goto_binary.cpp Outdated
@@ -27,6 +27,8 @@ Module: Read Goto Programs
#include "elf_reader.h"
#include "osx_fat_reader.h"

/// Read given goto binary
/// Does not update config
Copy link
Collaborator

Choose a reason for hiding this comment

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

Would it be possible to be a bit more explicit? To be frank: this is a commit that has one job, and it doesn't actually do that job. The parameters are not documented, the return value is not explained, failure modes are not covered.

allredj
allredj reviewed Sep 20, 2018
View reviewed changes
Copy link
Contributor

@allredj allredj left a comment

Choose a reason for hiding this comment

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

Passed Diffblue compatibility checks (cbmc commit: 6aa7d25).
Build URL: https://travis-ci.com/diffblue/test-gen/builds/85395135

Daniel Kroening added 2 commits September 21, 2018 10:19
add documentation to read_goto_binary and read_object_and_link
b7cf102
read_goto_binary does not set the config
637afdc 
Fixes #2949

This enables auto-detecting the architecture of a goto-binary when
performing transformations on it, e.g., with main.c:

int main(){
  char buffer[] = "a";
  int x = strlen(buffer);
  return x;
}

the commands

  goto-cc -m32 -o main.gb main.c
  goto-instrument --add-library main.gb main2.gb

now pass.
@kroening kroening force-pushed the fixup-e59511c9168f04cb21e85642aa8875c1cb4b4 branch from 6aa7d25 to 637afdc Compare September 21, 2018 09:20
allredj
allredj reviewed Sep 21, 2018
View reviewed changes
Copy link
Contributor

@allredj allredj left a comment

Choose a reason for hiding this comment

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

Passed Diffblue compatibility checks (cbmc commit: 637afdc).
Build URL: https://travis-ci.com/diffblue/test-gen/builds/85544888

@kroening kroening assigned tautschnig and unassigned kroening Sep 21, 2018
@tautschnig tautschnig merged commit e1f5644 into develop Sep 22, 2018
@tautschnig tautschnig deleted the fixup-e59511c9168f04cb21e85642aa8875c1cb4b4 branch September 22, 2018 12:18
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Reviewers

@allredj allredj allredj left review comments

@tautschnig tautschnig tautschnig approved these changes

@peterschrammel peterschrammel peterschrammel approved these changes

@chrisr-diffblue chrisr-diffblue Awaiting requested review from chrisr-diffblue

@martin-cs martin-cs Awaiting requested review from martin-cs martin-cs is a code owner

@pkesseli pkesseli Awaiting requested review from pkesseli

@smowton smowton Awaiting requested review from smowton

Assignees

@tautschnig tautschnig

Labels
None yet
Projects
None yet
Milestone
No milestone
Development

Successfully merging this pull request may close these issues.
4 participants
@kroening @peterschrammel @tautschnig @allredj