goto-gcc hybrid binaries on OS X #3867

tautschnig · 2019-01-21T11:38:34Z

Depends on #3702, #3866, only the last three commits are specifically for this feature. They finally provide a test for the code touched in #3702.

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).
n/a My commit message includes data points confirming performance improvements (if claimed).
My PR is restricted to a single feature or bugfix.
n/a White-space or formatting changes outside the feature-related changed lines are in commits of their own.

allredj

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

chrisr-diffblue

I'm not an expert on Mach-O (only read the lowlevelbits.org summary, plus some background knowledge of other object formats, such as ELF, COFF, etc). Mach-O parsing functionality looks OK to me. I might question the user experience a bit though. For instance, what happens if a user on, say, a linux host attempts to analyse Mach-O object files? As far as I can tell they'll get told that the files are not goto-programs - where in reality the situation is that reading Mach-O object files is only supported on APPLE platforms. It would be a nicer if there was an explicit message to that affect.

smowton

On grounds the @chrisr-diffblue knows his onions, happy to proxy approve :)

tautschnig · 2019-01-22T08:49:34Z

Rebase done, I'll try to implement @chrisr-diffblue's suggestion as soon as possible.

allredj

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

tautschnig · 2019-01-22T13:32:45Z

@chrisr-diffblue @smowton @kroening I have added a commit that should enable detection, and yield a warning if we are on a platform where we cannot fully parse the file. Should be ready for (re-)review.

chrisr-diffblue · 2019-01-22T14:16:48Z

LGTM - thanks for the improved user experience.

allredj

🚫
This PR failed Diffblue compatibility checks (cbmc commit: adc6af1).
Build URL: https://travis-ci.com/diffblue/test-gen/builds/100295745
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

⚠️
This PR failed Diffblue compatibility checks (cbmc commit: 7893de0).
Build URL: https://travis-ci.com/diffblue/test-gen/builds/102433712
Status will be re-evaluated on next push.
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 compatibility was already broken by an earlier merge.

Pass a message handler to is_goto_binary [blocks: #3867]

allredj

⚠️
This PR failed Diffblue compatibility checks (cbmc commit: d16fdcb).
Build URL: https://travis-ci.com/diffblue/test-gen/builds/103556283
Status will be re-evaluated on next push.
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 compatibility was already broken by an earlier merge.

allredj

⚠️
This PR failed Diffblue compatibility checks (cbmc commit: 76600d0).
Build URL: https://travis-ci.com/diffblue/test-gen/builds/104510954
Status will be re-evaluated on next push.
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 compatibility was already broken by an earlier merge.

lipo/fat binaries only work properly for executables as it isn't possible to build archives of fat binaries containing goto-cc sections (ranlib complains about invalid object files); conversely, adding additional sections isn't possible with executables, but fat binaries work fine.

A basic Mach-O header parser, only functional on OS X.

The test requires building platform-specific code, and thus additional rules were added to the Makefile.

Hard-code the magic values as extracted from OS X header files, but check them when actually building on OS X.

tautschnig added enhancement dependent - do not merge labels Jan 21, 2019

tautschnig requested review from kroening, peterschrammel, pkesseli and smowton as code owners January 21, 2019 11:38

allredj reviewed Jan 21, 2019

View reviewed changes

chrisr-diffblue approved these changes Jan 21, 2019

View reviewed changes

smowton approved these changes Jan 21, 2019

View reviewed changes

tautschnig changed the title ~~goto-gcc hybrid binaries on OS X [depends-on: #3702, #3866]~~ goto-gcc hybrid binaries on OS X [depends-on: #3702] Jan 21, 2019

kroening added the Needs rebase label Jan 22, 2019

tautschnig changed the title ~~goto-gcc hybrid binaries on OS X [depends-on: #3702]~~ goto-gcc hybrid binaries on OS X Jan 22, 2019

tautschnig force-pushed the osx-hybrid-binaries branch from 48629e2 to aeeccd1 Compare January 22, 2019 08:48

tautschnig removed Needs rebase dependent - do not merge labels Jan 22, 2019

tautschnig assigned kroening and tautschnig Jan 22, 2019

tautschnig added the work in progress label Jan 22, 2019

allredj reviewed Jan 22, 2019

View reviewed changes

tautschnig force-pushed the osx-hybrid-binaries branch from aeeccd1 to cced593 Compare January 22, 2019 13:30

tautschnig requested review from cesaro and cristina-david as code owners January 22, 2019 13:30

tautschnig force-pushed the osx-hybrid-binaries branch from cced593 to f26a30a Compare January 22, 2019 13:32

tautschnig removed their assignment Jan 22, 2019

tautschnig removed the work in progress label Jan 22, 2019

tautschnig force-pushed the osx-hybrid-binaries branch from f26a30a to cdb3726 Compare January 23, 2019 13:44

tautschnig assigned peterschrammel Jan 23, 2019

allredj reviewed Feb 8, 2019

View reviewed changes

tautschnig added the Needs TG approval 🦉 Only merge with explicit approval from test-gen maintainers label Feb 21, 2019

tautschnig force-pushed the osx-hybrid-binaries branch from adc6af1 to 7893de0 Compare February 27, 2019 01:26

allredj reviewed Feb 27, 2019

View reviewed changes

tautschnig mentioned this pull request Mar 7, 2019

Pass a message handler to is_goto_binary [blocks: #3867] #4341

Merged

3 tasks

tautschnig changed the title ~~goto-gcc hybrid binaries on OS X~~ goto-gcc hybrid binaries on OS X [depends-on: #4341] Mar 7, 2019

tautschnig added dependent - do not merge and removed Needs TG approval 🦉 Only merge with explicit approval from test-gen maintainers labels Mar 7, 2019

tautschnig assigned tautschnig and unassigned kroening Mar 7, 2019

tautschnig added a commit that referenced this pull request Mar 7, 2019

Merge pull request #4341 from tautschnig/is_goto_binary

35a0ac3

Pass a message handler to is_goto_binary [blocks: #3867]

tautschnig force-pushed the osx-hybrid-binaries branch from 7893de0 to d16fdcb Compare March 7, 2019 14:13

tautschnig removed the dependent - do not merge label Mar 7, 2019

tautschnig assigned kroening and unassigned tautschnig Mar 7, 2019

allredj reviewed Mar 7, 2019

View reviewed changes

tautschnig changed the title ~~goto-gcc hybrid binaries on OS X [depends-on: #4341]~~ goto-gcc hybrid binaries on OS X Mar 14, 2019

tautschnig force-pushed the osx-hybrid-binaries branch from d16fdcb to 76600d0 Compare March 14, 2019 22:02

allredj reviewed Mar 15, 2019

View reviewed changes

kroening approved these changes Apr 30, 2019

View reviewed changes

tautschnig force-pushed the osx-hybrid-binaries branch from 76600d0 to e615d37 Compare April 30, 2019 13:56

tautschnig assigned tautschnig and unassigned kroening Apr 30, 2019

tautschnig added 4 commits April 30, 2019 22:26

Read goto-cc section from Mach-O object files

c1108c9

A basic Mach-O header parser, only functional on OS X.

Test loading files from an archive

d155d87

The test requires building platform-specific code, and thus additional rules were added to the Makefile.

Detect OSX fat archives or Mach-O objects on all architectures

c7e8bcc

Hard-code the magic values as extracted from OS X header files, but check them when actually building on OS X.

tautschnig force-pushed the osx-hybrid-binaries branch from e615d37 to c7e8bcc Compare April 30, 2019 22:27

tautschnig merged commit 104a704 into diffblue:develop Apr 30, 2019

tautschnig deleted the osx-hybrid-binaries branch April 30, 2019 23:26

Provide feedback

Saved searches

Use saved searches to filter your results more quickly

Uh oh!

goto-gcc hybrid binaries on OS X #3867

goto-gcc hybrid binaries on OS X #3867

Uh oh!

tautschnig commented Jan 21, 2019

Uh oh!

allredj left a comment

Uh oh!

chrisr-diffblue left a comment

Uh oh!

smowton left a comment

Uh oh!

tautschnig commented Jan 22, 2019

Uh oh!

allredj left a comment

Uh oh!

tautschnig commented Jan 22, 2019

Uh oh!

chrisr-diffblue commented Jan 22, 2019

Uh oh!

allredj left a comment

Uh oh!

allredj left a comment

Uh oh!

allredj left a comment

Uh oh!

allredj left a comment

Uh oh!

Uh oh!

goto-gcc hybrid binaries on OS X #3867

goto-gcc hybrid binaries on OS X #3867

Uh oh!

Conversation

tautschnig commented Jan 21, 2019

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!

smowton left a comment

Choose a reason for hiding this comment

Uh oh!

tautschnig commented Jan 22, 2019

Uh oh!

allredj left a comment

Choose a reason for hiding this comment

Uh oh!

tautschnig commented Jan 22, 2019

Uh oh!

chrisr-diffblue commented Jan 22, 2019

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!

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!