Linux ci - Compile KVM with goto-cc #5916

nmanthey · 2021-03-12T08:46:10Z

This change adds a github workflow that compiles parts of the Linux kernel with goto-cc, and fails in case compilation fails. Furthermore, the input fails that lead to the failure are archived, to allow easy consumption and investigation.

Note: This is currently failing, and should help to improve goto-cc to be able to compile Linux

An example failed run with the broken input as artifact has been created as part of my testing: https://github.com/nmanthey/cbmc/pull/5/checks?check_run_id=2093209018

Each commit message has a non-empty body, explaining why the change was made.
[N/A] Methods or procedures I have added are documented, following the guidelines provided in CODING_STANDARD.md.
[N/A] The feature or user visible behaviour I have added or modified has been documented in the User Guide in doc/cprover-manual/
[N/A] 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.
White-space or formatting changes outside the feature-related changed lines are in commits of their own.

codecov · 2021-03-12T10:10:31Z

Codecov Report

Merging #5916 (1fbfd5e) into develop (7663a57) will decrease coverage by 0.02%.
The diff coverage is 58.18%.

@@             Coverage Diff             @@
##           develop    #5916      +/-   ##
===========================================
- Coverage    74.30%   74.27%   -0.03%     
===========================================
  Files         1444     1444              
  Lines       157453   157460       +7     
===========================================
- Hits        116995   116953      -42     
- Misses       40458    40507      +49

Impacted Files	Coverage Δ
src/solvers/smt2/smt2_conv.h	`100.00% <ø> (ø)`
src/ansi-c/c_typecheck_initializer.cpp	`61.61% <44.44%> (-12.97%)`	⬇️
src/solvers/smt2/smt2_conv.cpp	`60.38% <52.94%> (ø)`
src/solvers/smt2/smt2_solver.cpp	`83.11% <65.51%> (ø)`
src/util/config.cpp	`55.42% <0.00%> (+3.03%)`	⬆️
src/util/config.h	`62.50% <0.00%> (+12.50%)`	⬆️

Continue to review full report at Codecov.

Legend - Click here to learn more
Δ = absolute <relative> (impact), ø = not affected, ? = missing data
Powered by Codecov. Last update 2fdf995...1fbfd5e. Read the comment docs.

tautschnig · 2021-03-14T23:21:30Z

.github/workflows/build-and-test-Linux.yaml

+      - uses: actions/upload-artifact@v2
+        with:
+          name: CPROVER-faultyInput
+          path: CPROVER/faultyInput/*


How does one actually download these? GitHub keeps telling me that I need to have the "actions" scope, perhaps the repository permissions are set up in a way that doesn't permit non-members to do this?

How about doing tail -n +1 CPROVER/faultyInput/* instead? Really simple and avoids any permissions problems.

On the checks page (here, e.g.: https://github.com/diffblue/cbmc/pull/5916/checks there is an "artifacts" button on the top left, which allows (me) to download, I did not see any permission restrictions in the description of the action). Yes, I could also dump the content of the files, but that likely floods the output, as those are preprocessed already.

Err, thank you, that was too easy. A first fix is in #5928.

tautschnig · 2021-03-14T23:22:43Z

.github/workflows/build-and-test-Linux.yaml

+          sudo apt-get install --no-install-recommends -y coreutils  build-essential gcc git make flex bison software-properties-common curl python
+          sudo apt-get install --no-install-recommends -y bin86 gdb bcc liblzma-dev python-dev gettext iasl uuid-dev libncurses5-dev libncursesw5-dev pkg-config
+          sudo apt-get install --no-install-recommends -y libgtk2.0-dev libyajl-dev sudo time ccache
+          sudo apt-get install --no-install-recommends -y automake bc libssl-dev dkms libelf-dev libudev-dev libpci-dev libiberty-dev autoconf gawk jq


As far as I recall, we just need build-essential libssl-dev for the Linux kernel.

IIRC, that depends on the configuration. I can minimize this set.

tautschnig · 2021-03-14T23:23:41Z

.github/workflows/build-and-test-Linux.yaml

+      - name: Get Linux v5.10
+        run: git clone -b v5.10 --depth=1 https://git.kernel.org/pub/scm/linux/kernel/git/stable/linux-stable.git linux_5_10


I'd suggest to always use the latest release (at the risk of builds surprisingly breaking) and perhaps also using tar/zip instead of cloning?

If people are willing to take the risk, and address the issue (or roll this action back to the last known working release) I can build logic to always access the latest release.

On the other hand, I would like to be able to ensure that a specific version is always working.

This is the risk I see when always using the latest release: Once the latest release fails, people might ignore the failure or disable this action to unblock themselves. Afterwards, even compiling older relases might start to break again. Hence, I decided to pick a specific release for now.

Maybe we should have two such actions? One with a fixed, longterm-maintenance release (5.10 seems like a reasonable candidate) and one using the "master" branch?

Let's do the stable one for now, and iterate once that one is in.

tautschnig · 2021-03-15T13:40:02Z

We will next need #5730 to be merged.

tautschnig · 2021-03-15T13:51:30Z

We will next need #5730 to be merged.

And then #5723, at which point the job should actually succeed.

tautschnig · 2021-03-15T20:31:37Z

We will next need #5730 to be merged.

And then #5723, at which point the job should actually succeed.

Both of which are now merged, I believe this test should now succeed.

tautschnig · 2021-03-16T22:48:02Z

.github/workflows/build-and-test-Linux.yaml

+          make -C linux_5_10 allnoconfig
+          make -C linux_5_10 kvm_guest.config
+          make -C linux_5_10 bzImage -j $(nproc)


May I suggest the following variation of this:

cat > kvm-config <<EOF CONFIG_64BIT=y CONFIG_X86_64=y CONFIG_HIGH_RES_TIMERS=y CONFIG_MULTIUSER=y CONFIG_NET=y CONFIG_VIRTUALIZATION=y CONFIG_HYPERVISOR_GUEST=y CONFIG_PARAVIRT=y CONFIG_KVM_GUEST=y CONFIG_KVM=y CONFIG_KVM_INTEL=y CONFIG_KVM_AMD=y EOF KCONFIG_ALLCONFIG=kvm-config make allnoconfig make bzImage -j $(nproc)

Sure, I can re-iterate

tautschnig · 2021-03-16T22:48:35Z

.github/workflows/build-and-test-Linux.yaml

+          make -C linux_5_10 kvm_guest.config
+          make -C linux_5_10 bzImage -j $(nproc)
+          du -h . --max-depth=1
+          rm "linux_5_10/arch/x86/kernel/kvm.o"


With the above, perhaps instead do:

rm arch/x86/kernel/kvm.o find arch/x86/kvm/ -name "*.o" -delete

Will iterate

tautschnig · 2021-03-16T22:50:09Z

.github/workflows/build-and-test-Linux.yaml

+          make -C linux_5_10 bzImage -j $(nproc)
+          du -h . --max-depth=1
+          rm "linux_5_10/arch/x86/kernel/kvm.o"
+          one-line-scan/one-line-scan --add-to-path $(pwd)/src/cbmc --add-to-path $(pwd)/src/goto-diff  --add-to-path $(pwd)/src/goto-cc --no-analysis --trunc-existing --extra-cflags -Wno-error -o CPROVER -j 3 -- make -C linux_5_10 bzImage -j $(nproc) -k || true


I don't think we we should be ignoring failures here, thus drop -k || true. Also, shouldn't one-line-scan use (at least) the same -j as the command being run?

Yes, that should work.

The '-j' for one-line-scan is limited to not consume too much memory. For github, that should be good enough. For other use cases, that might be higher.

nmanthey · 2021-03-22T14:50:17Z

I addressed the comments, and factored out the actual compilation into a separate script, so that these steps can be executed in other environments more easily.

tautschnig · 2021-03-22T17:12:03Z

I addressed the comments, and factored out the actual compilation into a separate script, so that these steps can be executed in other environments more easily.

Thanks a lot, I'll review whether I already have a patch for the invariant failure.

tautschnig · 2021-03-22T22:46:25Z

I addressed the comments, and factored out the actual compilation into a separate script, so that these steps can be executed in other environments more easily.

Thanks a lot, I'll review whether I already have a patch for the invariant failure.

A proposal for the patch is in #5967, but I need to reconsider whether that's the correct approach (it is borrowed from #5738, which also made a number of other changes).

NlightNFotis

This looks good to me (modulo the CI failure).

I will wait for this to be fixed then I will approve this to get in.

tautschnig · 2021-04-21T15:34:10Z

@nmanthey #5967 is now merged, I believe this should pass once rebased.

Script the steps required to build linux, so that they can also be executed locally. Signed-off-by: Norbert Manthey <nmanthey@amazon.de> Signed-off-by: Norbert Manthey <nmanthey@amazon.de>

Similarly to Xen, CBMC should be able to compile the linux kernel. As compiling the full kernel is very time consuming, and with CBMC also space consuming, only compile a core part all its dependencies, with the smalles configuration possible. For this core part, we select the KVM hypervisor. Once this is working, the configuration, as well as targets to be compiled can be increased. When the linuxci fails, we want to be able to easily understand the failure. The used one-line-scan tool already captures input files that cannot be handled by goto-cc. Hence, also archives these files for easy access in the web UI. Signed-off-by: Norbert Manthey <nmanthey@amazon.de>

TGWDB · 2021-04-22T16:02:36Z

.github/workflows/build-and-test-Linux.yaml

+on:
+  pull_request:
+    branches:
+      - '**'


I'm a little hesitant about (another) CI job that runs on all PRs, specially one that we expect to report failures.

Feel free to suggest another branch pattern. I can also target the develop and production branch only. That might result in late surprises.

@TGWDB Why would you expect failures here?

@nmanthey I'm no git expert and don't have a better suggestion. I agree that late failures are not a good idea.

@tautschnig Based on the original PR text:

"This change adds a github workflow that compiles parts of the Linux kernel with goto-cc, and fails in case compilation fails. Furthermore, the input fails that lead to the failure are archived, to allow easy consumption and investigation."

I'm happy if this works without failures, but was (mis?)reading that we expect this to fail more often due to the target and perhaps related aspects of cbmc.

If we expect goto-cc to never fail this except for when we break something then I have no objection.

nmanthey requested a review from a team as a code owner March 12, 2021 08:46

tautschnig reviewed Mar 14, 2021

View reviewed changes

nmanthey force-pushed the linux-ci branch 2 times, most recently from 95c617f to e5d5a1e Compare March 15, 2021 13:29

tautschnig assigned nmanthey Mar 16, 2021

tautschnig reviewed Mar 16, 2021

View reviewed changes

nmanthey force-pushed the linux-ci branch from e5d5a1e to 121a6f1 Compare March 22, 2021 14:48

nmanthey requested review from chrisr-diffblue, hannes-steffenhagen-diffblue, kroening, peterschrammel and smowton as code owners March 22, 2021 14:48

nmanthey force-pushed the linux-ci branch from 121a6f1 to 24cd170 Compare March 22, 2021 14:49

nmanthey removed their assignment Mar 22, 2021

tautschnig self-assigned this Mar 22, 2021

NlightNFotis reviewed Mar 23, 2021

View reviewed changes

tautschnig changed the title ~~Linux ci - Compile KVM with goto-cc~~ Linux ci - Compile KVM with goto-cc [depends-on: #5967] Mar 31, 2021

tautschnig added the dependent - do not merge label Apr 3, 2021

nmanthey force-pushed the linux-ci branch from 24cd170 to 51aaca3 Compare April 6, 2021 11:29

nmanthey force-pushed the linux-ci branch 2 times, most recently from 7931bda to 21abee1 Compare April 19, 2021 08:22

tautschnig changed the title ~~Linux ci - Compile KVM with goto-cc [depends-on: #5967]~~ Linux ci - Compile KVM with goto-cc Apr 21, 2021

tautschnig removed the dependent - do not merge label Apr 21, 2021

tautschnig added the Needs rebase label Apr 21, 2021

tautschnig assigned nmanthey and unassigned tautschnig Apr 21, 2021

nmanthey added 2 commits April 22, 2021 09:17

linux: add compilation script

4b46a0a

Script the steps required to build linux, so that they can also be executed locally. Signed-off-by: Norbert Manthey <nmanthey@amazon.de> Signed-off-by: Norbert Manthey <nmanthey@amazon.de>

nmanthey force-pushed the linux-ci branch from 21abee1 to 1fbfd5e Compare April 22, 2021 07:17

tautschnig approved these changes Apr 22, 2021

View reviewed changes

tautschnig removed the Needs rebase label Apr 22, 2021

tautschnig assigned NlightNFotis and TGWDB and unassigned nmanthey Apr 22, 2021

TGWDB reviewed Apr 22, 2021

View reviewed changes

TGWDB approved these changes Apr 26, 2021

View reviewed changes

tautschnig merged commit dc30727 into diffblue:develop Apr 26, 2021

TGWDB mentioned this pull request May 20, 2021

Idea: Linux Kernel tests on RCU #903

Closed

Provide feedback

Saved searches

Use saved searches to filter your results more quickly

Linux ci - Compile KVM with goto-cc #5916

Linux ci - Compile KVM with goto-cc #5916

nmanthey commented Mar 12, 2021

codecov bot commented Mar 12, 2021 •

edited

Loading

tautschnig Mar 14, 2021

tautschnig Mar 14, 2021

nmanthey Mar 15, 2021

tautschnig Mar 15, 2021

tautschnig Mar 14, 2021

nmanthey Mar 15, 2021

tautschnig Mar 14, 2021

nmanthey Mar 15, 2021

tautschnig Mar 15, 2021

nmanthey Mar 22, 2021

tautschnig commented Mar 15, 2021

tautschnig commented Mar 15, 2021

tautschnig commented Mar 15, 2021

tautschnig Mar 16, 2021

nmanthey Mar 18, 2021

tautschnig Mar 16, 2021

nmanthey Mar 18, 2021

tautschnig Mar 16, 2021

nmanthey Mar 18, 2021

nmanthey commented Mar 22, 2021

tautschnig commented Mar 22, 2021

tautschnig commented Mar 22, 2021

NlightNFotis left a comment

tautschnig commented Apr 21, 2021

TGWDB Apr 22, 2021

nmanthey Apr 22, 2021

tautschnig Apr 22, 2021

TGWDB Apr 26, 2021

		- name: Get Linux v5.10
		run: git clone -b v5.10 --depth=1 https://git.kernel.org/pub/scm/linux/kernel/git/stable/linux-stable.git linux_5_10

Linux ci - Compile KVM with goto-cc #5916

Linux ci - Compile KVM with goto-cc #5916

Conversation

nmanthey commented Mar 12, 2021

Note: This is currently failing, and should help to improve goto-cc to be able to compile Linux

codecov bot commented Mar 12, 2021 • edited Loading

Codecov Report

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

tautschnig commented Mar 15, 2021

tautschnig commented Mar 15, 2021

tautschnig commented Mar 15, 2021

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

nmanthey commented Mar 22, 2021

tautschnig commented Mar 22, 2021

tautschnig commented Mar 22, 2021

NlightNFotis left a comment

Choose a reason for hiding this comment

tautschnig commented Apr 21, 2021

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

codecov bot commented Mar 12, 2021 •

edited

Loading