Add codecov #4448

yumibagge · 2019-03-28T09:38:37Z

The purpose of this PR is to understand current CBMC coverage.

Below are justification of why I created buildspec-linux-make-gcc-cov.yml and modified config.inc

travis vs. CodeBuild
😢 travis has timeout = 50min and maximum log length 10k

😢 codecov does not support CodeBuild
🔨 Therefore CODECOV_TOKEN needs to be set as a environment variable in Build detail (not in buildspec.xml)
🔨 In order to coverage reporting available, needed to install lcov, curl, python-pip, then pip install codecov (This is to hope codecov.sh find all gcda files)

cmake vs. make

😞 make with CXXFLAGS in the same line causes compile error
🔨 to mitigate this, in config.inc, a new environment variable CPROVER_WITH_PROFILING with CXXFLAGS and LINKFLAGS are added
🔨 append CPROVER_WITH_PROFILING=1 is added for each make and also make -C regression test as it's calling driver which also require coverage instrumentation
❔ cmake and make shows different statistics
❔ it is unclear why it's reported failure when build is complete for cmake

codecov script
😞 bash does not work on CodeBuild
🔨 use the 4 line shell scripts

lcov
😞 codecov.sh does not find gcda files for some reasons, so had to generate coverage info file using lcov

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.

tautschnig · 2019-03-28T10:25:12Z

Would it be possible to add a few comments to clarify, including a full commit message? This looks like a piece of black magic right now. Useful documentation would include links to documentation that explain that this is the way to interact with codecov.io. Thanks!

chrisr-diffblue

This is a work-in-progress experiment by Yumi, which is not intended to be merged just yet. I'm putting a blocking comment here for now, until such times as the experiments are over and we can then decided whether to merge or close.

tautschnig · 2019-03-28T10:36:47Z

If we're talking code coverage, here's what I'm dreaming of:

Just overall coverage reports to see how we are doing.
A CI task that compares the coverage report to the changes proposed in a PR, much like we are doing this with clang-format, cpplint, doxygen. The task should fail if modified code is not covered, unless some break-glass option is used (such as special commands in the commit message to openly admit that the changes aren't covered by tests).

martin-cs · 2019-03-28T11:45:37Z

A long standing problem with the CPROVER code base is functionality bit-rotting because everyone assumed someone else was using / testing it. If this could help us identify or even avoid this, it would be great.

allredj

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

allredj

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

allredj

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

allredj

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

peterschrammel · 2019-05-23T14:07:20Z

.travis.yml

@@ -4,7 +4,7 @@ jobs:
  include:

    - &formatting-stage
-      stage: Linter + Doxygen + non-debug Ubuntu/gcc-5 test
+      stage: Linter + Doxygen + non-debug Ubuntu/gcc-5 test 


spurious change

The commit was removed

peterschrammel · 2019-05-29T10:14:10Z

buildspec-linux-make-gcc-cov.yml

+    - '/var/lib/apt/lists/**/*'
+    - '/root/.ccache/**/*'
+    - '/root/.cache/codecov.sh'
+


Remove the spaces in this line

allredj

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

chrisr-diffblue

I'm reasonably happy for this to go in as it is, but I've left a couple of queries as comments that would be good to check.

chrisr-diffblue · 2019-05-30T11:35:24Z

buildspec-linux-make-gcc-cov.yml

+      - make -C jbmc/unit test
+      - make -C jbmc/regression test
+      - lcov --capture --directory . --output-file ./lcov.info
+      - VCS_PULL_REQUEST=$(echo $CODEBUILD_SOURCE_VERSION | sed 's/pr\///g')


Is VCS_PULL_REQUEST actually used anywhere?

I am not too sure. As I referred in another your question. I took this 4 lines of scripts from codecov/codecov-python#140.

chrisr-diffblue · 2019-05-30T11:41:16Z

buildspec-linux-make-gcc-cov.yml

+      - VCS_PULL_REQUEST=$(echo $CODEBUILD_SOURCE_VERSION | sed 's/pr\///g')
+      - COV_SCRIPT=/root/.cache/codecov.sh
+      - if [ ! -f "$COV_SCRIPT" ]; then curl -s https://codecov.io/bash > "$COV_SCRIPT"; fi
+      - echo "$CODEBUILD_INITIATOR" | grep GitHub && bash "$COV_SCRIPT" -t "$CODECOV_TOKEN" || true      


I don't fully understand what this line is doing (I'm afraid I don't know what the contents of $CODEBUILD_INITIATOR is off the top of my head) - but I'm slightly worried by the || true - which will basically mask any errors that occur here?

Well, essentially I blindly used script example here
codecov/codecov-python#140
According to https://docs.aws.amazon.com/codebuild/latest/userguide/build-env-ref-env-vars.html, $CODEBUILD_INITIATOR is "the entity that started the build". In our case, (also from log), I believe this is webhook?
[Container] 2019/05/30 09:35:34 Running command echo "$CODEBUILD_INITIATOR" | grep GitHub && bash "$COV_SCRIPT" -t "$CODECOV_TOKEN" || true
GitHub-Hookshot/0a2cefb

Do you want me to try removing the || true?

I'm honestly not sure on the || true - I guess lets run it as is and see how reliable it is.

chrisr-diffblue · 2019-05-30T11:44:46Z

src/config.inc

@@ -8,6 +8,11 @@ else
  CXXFLAGS += -Wall -pedantic -Werror -Wno-deprecated-declarations -Wswitch-enum
 endif

+ifeq ($(CPROVER_WITH_PROFILING),1)


I know you mentioned that somehow CMake unit tests fail if coverage is enabled, but I think it would still be preferable if we kept Make and CMake builds in sync, and at least adding these options to CMake would be good - even if you raise an issue in the GitHub issue tracker to cover whatever failures you see in CMake unit tests rather than also fixing them in this PR.

True. The thing is this invariant violation happens only codebuild, and I've tried to reproduce it on local codebuild docker, it did not reproduce. I have a gut feeling though initially, cbmc-codecov environment was openjdk-8, not standard-2.0. Let me give me another go with cmake-coverage and if it's reproducible, I will raise an issue in the GitHub.

@chrisr-diffblue , OK, so perhaps the invariant violation I observed was because of AWS image. I no longer observe it. I still have a problem codecov does not find existing coverage files from the VM. I will push just one more time with extra LCOV command it should be able to report. In that case, do you want another buildspec file buildspec-linux-cmake-gcc-cov.yml and CMakeLists.txt to be part of this PR?

allredj

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

allredj

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

allredj

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

to be enabled for coverage measurement

This is not a part of CI.

yumibagge · 2019-05-30T21:08:38Z

@peterschrammel and @chrisr-diffblue, I am requesting re-review as the current state is

buildspec-linux-make-gcc-cov.xml, config.inc and README.md with codecov badge for CI (both of you approved in this state)
buildspec-linux-cmake-gcc-cov.xml and CMakeLists.txt for cmake build but not for CI.

As per request from @chrisr-diffblue, I checked cmake behaviour and a good news is cmake with coverage build does not cause the invariant violation I've initially observed.
Hence, the plan is to add buildspec for cmake-gcc-cov and CMakeLists for the future but not as a part of CI. (I have confirmed buildspec-linux-cmale-gcc-cov.xml succeeded to complete - but for some reasons the PR page said build failed)

However, I also realised that there is a quite a bit of difference in analysed lines between make and cmake (Above is make and below is cmake)

This trend is reproducible locally
make

cmake

make
https://codecov.io/gh/diffblue/cbmc/tree/2d7a508576462ca9fae683b642949b736a736997/

cmake
https://codecov.io/gh/diffblue/cbmc/tree/6feed18c171ea61a1a3e08dfe19345242c1d5bc4/

make reports higher coverage, but cmake analyses more lines (the difference in line is 27k?).

Do you want me to investigate this on any further before merged?

allredj

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

chrisr-diffblue · 2019-05-31T08:55:14Z

@yumibagge @peterschrammel - Thanks Yumi for the extra clarification. I'm happy for this to go in as it is - but it would be nice to understand why cmake and make give different coverage results. It doesn't entirely surprise me, and I can think of a number of reasons why coverage might be different, but it would be good to be sure :-) However, I'm happy for that work to be done separately to this PR.

peterschrammel · 2019-05-31T10:56:56Z

Do you want me to investigate this on any further before merged?

I think this definitely needs to be investigated, but it can be done as a follow-up action.

yumibagge marked this pull request as ready for review March 28, 2019 10:20

yumibagge requested review from chrisr-diffblue, forejtv, peterschrammel and thk123 as code owners March 28, 2019 10:20

chrisr-diffblue added do not merge do not review labels Mar 28, 2019

chrisr-diffblue changed the title ~~Add codecov~~ [WIP] Add codecov Mar 28, 2019

tautschnig assigned yumibagge Mar 28, 2019

chrisr-diffblue suggested changes Mar 28, 2019

View reviewed changes

allredj reviewed Mar 28, 2019

View reviewed changes

peterschrammel added the work in progress label Mar 28, 2019

yumibagge force-pushed the yb/codecov branch from 3ccfd64 to 09266be Compare March 29, 2019 08:51

yumibagge requested review from kroening, smowton and tautschnig as code owners March 29, 2019 08:51

yumibagge force-pushed the yb/codecov branch from 09266be to a62bf2d Compare March 30, 2019 15:10

allredj reviewed Mar 30, 2019

View reviewed changes

allredj reviewed Mar 31, 2019

View reviewed changes

yumibagge force-pushed the yb/codecov branch from 23c389f to 8cbcbce Compare March 31, 2019 10:00

allredj reviewed Mar 31, 2019

View reviewed changes

yumibagge force-pushed the yb/codecov branch 6 times, most recently from 09dbbc0 to 8863565 Compare March 31, 2019 15:17

peterschrammel changed the title ~~[WIP] Add codecov~~ Add codecov May 29, 2019

peterschrammel removed do not merge do not review work in progress labels May 29, 2019

peterschrammel approved these changes May 29, 2019

View reviewed changes

yumibagge force-pushed the yb/codecov branch 2 times, most recently from 5c0316d to 2d7a508 Compare May 30, 2019 08:45

allredj reviewed May 30, 2019

View reviewed changes

chrisr-diffblue approved these changes May 30, 2019

View reviewed changes

yumibagge force-pushed the yb/codecov branch 4 times, most recently from af5c1c2 to 5db16f5 Compare May 30, 2019 13:07

allredj reviewed May 30, 2019

View reviewed changes

yumibagge force-pushed the yb/codecov branch from 5db16f5 to 6feed18 Compare May 30, 2019 17:23

allredj reviewed May 30, 2019

View reviewed changes

yumibagge force-pushed the yb/codecov branch from 6feed18 to 41365e2 Compare May 30, 2019 19:23

allredj reviewed May 30, 2019

View reviewed changes

yumibagge added 5 commits May 30, 2019 22:06

Add AWS CodeBuild spec to run codecov

c1b1d07

Add CPROVER_WITH_PROFILING to make build

0ef5e78

to be enabled for coverage measurement

Add codecov badge

69dbdef

Add AWS CodeBuild spec to run codecov w cmake

0ea62e3

This is not a part of CI.

Add goto-harness dependency and unify format

a780511

yumibagge force-pushed the yb/codecov branch from 41365e2 to a780511 Compare May 30, 2019 21:06

allredj reviewed May 30, 2019

View reviewed changes

peterschrammel merged commit 24212bf into diffblue:develop May 31, 2019

yumibagge deleted the yb/codecov branch July 20, 2019 12:16

Add codecov #4448

Add codecov #4448

Uh oh!

Conversation

yumibagge commented Mar 28, 2019 • edited Loading Uh oh! There was an error while loading. Please reload this page.

Uh oh!

Uh oh!

tautschnig commented Mar 28, 2019

Uh oh!

chrisr-diffblue left a comment

Choose a reason for hiding this comment

Uh oh!

tautschnig commented Mar 28, 2019

Uh oh!

martin-cs commented Mar 28, 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!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

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!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

yumibagge May 30, 2019 • 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!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

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!

yumibagge commented May 30, 2019 • 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!

chrisr-diffblue commented May 31, 2019

Uh oh!

peterschrammel commented May 31, 2019

Uh oh!

Uh oh!

yumibagge commented Mar 28, 2019 •

edited

Loading

yumibagge May 30, 2019 •

edited

Loading

yumibagge commented May 30, 2019 •

edited

Loading