Add llvm-16 build to CI, switch from --cppstd to --std + remove default -std=c++03 #1817

fbrausse · 2024-05-07T14:36:11Z

This PR:

Switches from --cppstd N to --std c++N or --std gnu++N in accordance with earlier discussion; closes [option] language standard #1050. Also, there is no default C++ standard selected anymore (closes [C++ verification] Shall we consider C++11 as the default standard in ESBMC? #1740 as per @mikhailramalho's comment there): If --std is not given, Clang's default is used: gnu++14 up until Clang-15, gnu++17 since v16. This could be a breaking change for users, so it must be mentioned in the Release Notes.
- This caused some existing C++ tests to fail which didn't specify --std. I've duplicated those tests to be KNOWNBUG without the option and CORE with the correct --std.
- The config.language field becomes a struct containing language_id and the string from the --std option.
Adds a Clang-16 based build to the CI and adds support for clang::UsingType (exists since Clang-14, but seems to be generated only by Clang-16+).
Fixes Clang-16 compatibility #862 by adding the corresponding -Wno-error= flags to the failing C test cases. The reason for choosing this solution over others mentioned in a comment below is that "regression tests are not wrong, only their status is", but keeping unmodifed "parsing error" ones doesn't test anything besides Clang's defaults. So only the command line is changed.

Fixes 3 knownbug and adds duplicated tests for 36 new knownbug tests. These bugs are actually not known, but most of them seem to have to do with std::sort and potentially std::move, so they are related to the first item above. This is the list of all new knownbug:

regression/esbmc-cpp/algorithm/algorithm108
regression/esbmc-cpp/algorithm/algorithm109
regression/esbmc-cpp/algorithm/algorithm110
regression/esbmc-cpp/algorithm/algorithm111
regression/esbmc-cpp/algorithm/algorithm112
regression/esbmc-cpp/algorithm/algorithm113
regression/esbmc-cpp/algorithm/algorithm122
regression/esbmc-cpp/algorithm/algorithm123
regression/esbmc-cpp/algorithm/algorithm15
regression/esbmc-cpp/algorithm/algorithm16
regression/esbmc-cpp/algorithm/algorithm17
regression/esbmc-cpp/algorithm/algorithm33
regression/esbmc-cpp/algorithm/algorithm40
regression/esbmc-cpp/algorithm/algorithm40_sort1
regression/esbmc-cpp/algorithm/algorithm40_sort2
regression/esbmc-cpp/algorithm/algorithm42
regression/esbmc-cpp/algorithm/algorithm42_partial_sort1
regression/esbmc-cpp/algorithm/algorithm79
regression/esbmc-cpp/algorithm/algorithm80
regression/esbmc-cpp/algorithm/algorithm92
regression/esbmc-cpp/algorithm/algorithm94
regression/esbmc-cpp/algorithm/algorithm99
regression/esbmc-cpp/algorithm/algorithm_swap
regression/esbmc-cpp/cpp/llbmc_sort-test02
regression/esbmc-cpp/multiset/multiset-begin
regression/esbmc-cpp/multiset/multiset-end-bug
regression/esbmc-cpp/multiset/multiset-end
regression/esbmc-cpp/set/set-begin
regression/esbmc-cpp/set/set-end-bug
regression/esbmc-cpp/set/set-end
regression/esbmc-cpp/set/set-swap
regression/esbmc-cpp/set/set-value_comp-c++03
regression/esbmc-cpp/template/algorithm32
regression/esbmc-cpp/vector/ch11_25
regression/esbmc-cpp/vector/vector22
regression/esbmc-cpp/vector/vector35

…ersions

…re we?

lucasccordeiro · 2024-05-09T07:40:03Z

Hi @fbrausse,

I'm fine with your proposed solution (disable -Werror for the tests affected).

fbrausse · 2024-05-09T08:13:18Z

Hi @fbrausse,

I'm fine with your proposed solution (disable -Werror for the tests affected).

OK, great!

The 3 tests failing on the clang-16 CI actually already fail with clang-15 in local tests (edit: they work with clang-14):

	2217 - regression/esbmc-cpp11/constructors/MoveAssignOperator (Failed)
	2219 - regression/esbmc-cpp11/constructors/MoveConstructor (Failed)
	2232 - regression/esbmc-cpp11/reference/Reference4 (Failed)

…t --std

fbrausse · 2024-05-09T10:51:38Z

These tests failing on clang-11 and clang-13 (and clang-14, locally) work on clang-15 and beyond:

	3757 - regression/esbmc-cpp/vector/ch11_25 (Failed)
	3797 - regression/esbmc-cpp/vector/vector22 (Failed)
	3812 - regression/esbmc-cpp/vector/vector35 (Failed)

…rk for clang < 15)

mikhailramalho

LGTM, although I'm still annoyed that we use --std= instead of -std= like the clang cmdline

fbrausse · 2024-05-09T15:09:44Z

LGTM, although I'm still annoyed that we use --std= instead of -std= like the clang cmdline

Me too. It's due to boost, though. @kunjsong01 has looked into it before and found -option not to be supported. :(

mikhailramalho · 2024-05-09T15:13:28Z

It looks there is a way: https://stackoverflow.com/questions/7233325/boost-program-options-syntax Em qui., 9 de mai. de 2024 às 12:10, Franz Brauße ***@***.***> escreveu:

…

LGTM, although I'm still annoyed that we use --std= instead of -std= like the clang cmdline Me too. It's due to boost, though. @kunjsong01 <https://github.com/kunjsong01> has looked into it before and found -option not to be supported. :( — Reply to this email directly, view it on GitHub <#1817 (comment)>, or unsubscribe <https://github.com/notifications/unsubscribe-auth/AAKEJH4YSSNMRFP4LHXCJFDZBOGU5AVCNFSM6AAAAABHLES6NSVHI2DSMVQWIX3LMV43OSLTON2WKQ3PNVWWK3TUHMZDCMBSHA2TCOJSGI> . You are receiving this because you were mentioned.Message ID: ***@***.***>

-- Mikhail R. Gadelha, Ph.D.

fbrausse · 2024-05-09T20:12:16Z

Master:

Statistics:          23805 Files
  correct:           14204
    correct true:     7814
    correct false:    6390
  incorrect:            42
    incorrect true:     13
    incorrect false:    29
  unknown:            9559
  Score:             21138 (max: 38482)

https://github.com/esbmc/esbmc/actions/runs/9018938790

This PR:

Statistics:          23805 Files
  correct:           14182
    correct true:     7795
    correct false:    6387
  incorrect:            42
    incorrect true:     13
    incorrect false:    29
  unknown:            9581
  Score:             21097 (max: 38482)

https://github.com/esbmc/esbmc/actions/runs/9018942491

lucasccordeiro · 2024-05-09T20:52:03Z

Thanks for submitting this PR, @fbrausse.

@XLiZHI: can I ask you to check the failed test case and submit another PR to fix them?

fbrausse force-pushed the fb/llvm-16+ branch 5 times, most recently from fe57871 to d75db5c Compare May 7, 2024 15:13

fbrausse added 2 commits May 7, 2024 17:15

[github] build against llvm-16, see #862

78a28b4

[github] use parts of llvm.sh script to enable repos for newer llvm v…

453080c

…ersions

fbrausse force-pushed the fb/llvm-16+ branch from d75db5c to 453080c Compare May 7, 2024 15:16

[github] fix?

06d9914

fbrausse force-pushed the fb/llvm-16+ branch from ee9ed16 to 06d9914 Compare May 7, 2024 15:24

fbrausse mentioned this pull request May 7, 2024

Support compilation against LLVM-17 and -18 #1816

Merged

fbrausse changed the title ~~Support building against llvm-16, see #862~~ Add llvm-16 build to CI, see #862 May 7, 2024

fbrausse added 2 commits May 7, 2024 19:06

[clang-c] avoid deprecated Clang API

1ca7a2b

[options] move --cppstd to --std and support it for C as well

1279bbe

fbrausse force-pushed the fb/llvm-16+ branch from bb9bcea to 1279bbe Compare May 7, 2024 19:45

fbrausse added the needs-svcomp-run label May 7, 2024

fbrausse force-pushed the fb/llvm-16+ branch 5 times, most recently from 7a6cb8c to 6c6eedb Compare May 8, 2024 06:21

fbrausse added 4 commits May 8, 2024 08:41

[clang-cpp] fix --std parsing

1e4322b

[clang-cpp] what the hell? we are not the language standard police, a…

18888dd

…re we?

[clang-cpp] only force -std= param if --std was given

397b4e8

[solidity] parse dummy C file with correct language setting

535a958

fbrausse force-pushed the fb/llvm-16+ branch from c25f194 to bf1a7a2 Compare May 8, 2024 06:45

fbrausse added 4 commits May 8, 2024 12:31

[clang-cpp] support UsingType for clang >= 14

880a56b

[cpp] <string> constructor from const-qualified char *

04e6562

[regression] linux/ is mostly gnu89, except for spinlock test

80e510d

[regression] fixed 1 knownbug

f06e844

fbrausse added 2 commits May 9, 2024 08:47

[regression] dup test, success with --std c++03, knownbug without

badc9a9

Merge remote-tracking branch 'upstream/master' into fb/llvm-16+

ab8cab0

fbrausse changed the title ~~Add llvm-16 build to CI, see #862~~ Add llvm-16 build to CI, switch from --cppstd to --std + remove default -std=c++03 May 9, 2024

[regression] add -Wno-error=int-conversion to test

e788a83

[regression] fails for < c++17, succeeds after; remove version withou…

15ae4fa

…t --std

fbrausse force-pushed the fb/llvm-16+ branch from 0c3df73 to 15ae4fa Compare May 9, 2024 08:38

fbrausse added 2 commits May 9, 2024 12:47

[regression] unfix knownbug

2ac09db

[regression] move --cppstd to --std c++

1a114be

[regression] unfix knownbug (they are knowbug for clang >= 15, but wo…

d0b5b5b

…rk for clang < 15)

fbrausse mentioned this pull request May 9, 2024

Clang-15+ based frontends cause regressions #1822

Closed

fbrausse marked this pull request as ready for review May 9, 2024 14:33

fbrausse requested review from mikhailramalho, lucasccordeiro, rafaelsamenezes and XLiZHI May 9, 2024 14:54

Merge branch 'master' into fb/llvm-16+

1c15a6e

mikhailramalho approved these changes May 9, 2024

View reviewed changes

lucasccordeiro approved these changes May 9, 2024

View reviewed changes

fbrausse removed the needs-svcomp-run label May 9, 2024

rafaelsamenezes approved these changes May 9, 2024

View reviewed changes

XLiZHI approved these changes May 9, 2024

View reviewed changes

lucasccordeiro merged commit ae774f7 into master May 9, 2024
12 of 13 checks passed

lucasccordeiro deleted the fb/llvm-16+ branch May 9, 2024 20:51

Provide feedback

Saved searches

Use saved searches to filter your results more quickly

Add llvm-16 build to CI, switch from --cppstd to --std + remove default -std=c++03 #1817

Add llvm-16 build to CI, switch from --cppstd to --std + remove default -std=c++03 #1817

fbrausse commented May 7, 2024 •

edited

Loading

lucasccordeiro commented May 9, 2024

fbrausse commented May 9, 2024 •

edited

Loading

fbrausse commented May 9, 2024

mikhailramalho left a comment

fbrausse commented May 9, 2024

mikhailramalho commented May 9, 2024 via email

fbrausse commented May 9, 2024

lucasccordeiro commented May 9, 2024

Add llvm-16 build to CI, switch from --cppstd to --std + remove default -std=c++03 #1817

Add llvm-16 build to CI, switch from --cppstd to --std + remove default -std=c++03 #1817

Conversation

fbrausse commented May 7, 2024 • edited Loading

lucasccordeiro commented May 9, 2024

fbrausse commented May 9, 2024 • edited Loading

fbrausse commented May 9, 2024

mikhailramalho left a comment

Choose a reason for hiding this comment

fbrausse commented May 9, 2024

mikhailramalho commented May 9, 2024 via email

fbrausse commented May 9, 2024

lucasccordeiro commented May 9, 2024

fbrausse commented May 7, 2024 •

edited

Loading

fbrausse commented May 9, 2024 •

edited

Loading