use compiler defaults for gcc defines #2217

kroening · 2018-05-22T07:56:47Z

This removes the attempt to undef all gcc/clang built-in compiler preprocessing defines and then recreate them.

The effect is that cbmc will appear to have the identity of the installed compiler. This, in effect, removes the "cross-architecture" feature; however, this requires installation of target-specific headers, and then installing the target preprocessor isn't a large additional step.

Finally, this brings the behaviour of cbmc closer to that of goto-cc. In the long term, one could see cbmc calling goto-gcc, goto-cl, etc.

tautschnig · 2018-05-22T09:58:19Z

Is there net benefit in taking this intermediate step instead of putting in effort to use goto-cc's code directly?

kroening · 2018-05-22T10:09:48Z

Yes; using goto-cc's code would require changing the front-end output to goto-functions first.

tautschnig · 2018-05-22T10:23:54Z

Yes; using goto-cc's code would require changing the front-end output to goto-functions first.

Agreed, but is there urgency that would justify this detour?

kroening · 2018-05-22T12:48:30Z

Yes; this PR changes the externally-visible behaviour, and I'd like to get it in before the release. We can do the front-end change for the next, and that will then be invisible.

tautschnig

Various smaller changes below, but a main step is adding libc6-dev-i386 to the Travis config so that regression tests that use -m32 pass. There is also a single regression test that uses --16 -- that one should be fixed by renaming the source file from main.c to main.i so that preprocessing is evaded.

tautschnig · 2018-05-22T13:05:22Z

src/ansi-c/c_preprocess.cpp


  if(preprocessor==configt::ansi_ct::preprocessort::CLANG)
  {
+    // not sure about the below
    command+=" -D_Noreturn=\"__attribute__((__noreturn__))\"";


This is from bbf7998 - I'd say this should be removed, the front-end does parse this properly.

tautschnig · 2018-05-22T13:06:41Z

src/ansi-c/c_preprocess.cpp

-    break;
-
-  case configt::ansi_ct::ost::NO_OS:
-    command+=" -nostdinc"; // make sure we don't mess with the system library


This should still be handled/used.

Not sure I want to retain like this, but ok for now.

tautschnig · 2018-05-22T13:07:39Z

src/ansi-c/c_preprocess.cpp

-//  command+=" -D__arm__";
-
-//  if(config.ansi_c.endianness==configt::ansi_ct::IS_BIG_ENDIAN)
-//    command+=" -D__BIG_ENDIAN";


If armcc has the same options as GCC, then this should translate to -mbig-endian

The manpage suggests it's -bigend

Yeah, armcc has --bigend (note the double -) (I used to develop armcc...)

tautschnig · 2018-05-22T13:08:03Z

src/ansi-c/c_preprocess.cpp

-//    command+=" -D__BIG_ENDIAN";
-
-//  if(config.ansi_c.char_is_unsigned)
-//    command+=" -D__CHAR_UNSIGNED__";


Should be handled like it is for GCC.

The manpage doesn't give an option.

Ah, found one

tautschnig · 2018-05-22T13:08:22Z

src/ansi-c/c_preprocess.cpp

-      command+=GCC_DEFINES_32;
-    else if(config.ansi_c.int_width==64)
-      command+=GCC_DEFINES_LP64;
-  }


To be handled as is done for GCC.

Off the top of my head, I don't think armcc has a direct equivalent to gcc's -m16/32/64 options.... Probably the closes is some combination of --thumb or --arm or maybe specifying a suitable --cpu= with a suitable ARM architecture target. Wide char width can be controlled by --wchar16/32. I don't believe any publicly available version of armcc ever supported AArch64 (public support for that went into armclang).

smowton · 2018-05-23T07:53:29Z

src/util/config.cpp

@@ -653,12 +653,16 @@ configt::ansi_ct::c_standardt configt::ansi_ct::default_c_standard()
  // By default, clang on FreeBSD builds C code in GNU C99
  return c_standardt::C99;
  #else
-  return c_standardt::C99;
+  // By default, gcc 5.4 or higher use gnu11; older versions use gnu89


I continue to think we should parse the version of the compiler we're using, and vary our behaviour for compatibility (previously suggested to avoid defining _Float32 et al except when we're pretending to be GCC 7+)

@smowton my experience with armcc (and that of EDG, the front-end it used) was that when we add GCC emulation it proved to be quite important for customers that we respected the GCC version we were pretending to be - a surprising amount of software broke if we didn't (and in some cases, this included needing to emulate certain GCC bugs).

Yes; I would say that needs to go into goto-gcc first, and then we switch the cbmc front-end to use the goto-gcc flow.

The version parsing is now in #2240.

kroening · 2018-05-23T10:23:59Z

Any idea whether clang on Linux/ubuntu can do -m32 at all?

tautschnig · 2018-05-23T10:33:56Z

Yes, clang happily does -m32:

$ clang -m32 ub14.c
$ uname -a
Linux udc4a3e98390d5836f203 4.4.0-124-generic #148~14.04.1-Ubuntu SMP Thu May 3 07:26:53 UTC 2018 x86_64 x86_64 x86_64 GNU/Linux

peterschrammel · 2018-05-25T13:36:25Z

Well-spotted, @chrisr-diffblue.

tautschnig · 2018-05-29T13:43:14Z

.travis.yml

      before_install:
-        - mkdir bin ; ln -s /usr/bin/clang-3.7 bin/gcc
+        - mkdir bin ; ln -s /usr/bin/gcc-5 bin/gcc


I don't understand this change? Is gcc-5 even installed in this configuration?

The problem is that clang on Travis won't allow the -m32.

That seems rather weird - what's the error message?

It can't find the 32-bit headers; clang has it's own headers, so there may well be a package that adds the 32-bit headers for clang.

Ok, it still seems a bit magical that gcc-5 is even present. But ok, it works... As this might break at some random future point (or, equally, clang packages be fixed), could the commit message please be made verbose to explain what is going on here? Moving to some other version of GCC will be painful if it cannot be found out what is going on in those lines.

it still seems a bit magical that gcc-5 is even present.

libstdc++-5-dev (https://github.com/diffblue/cbmc/pull/2217/files#diff-354f30a63fb0907d4ad57269548329e3R169) depends on package gcc-5

tautschnig · 2018-05-31T11:27:15Z

.travis.yml

      before_install:
-        - mkdir bin ; ln -s /usr/bin/clang-3.7 bin/gcc
+        - mkdir bin ; ln -s /usr/bin/gcc-5 bin/gcc


Ok, it still seems a bit magical that gcc-5 is even present. But ok, it works... As this might break at some random future point (or, equally, clang packages be fixed), could the commit message please be made verbose to explain what is going on here? Moving to some other version of GCC will be painful if it cannot be found out what is going on in those lines.

This requires changing the compiler that runs the tests from clang to gcc-5.

kroening · 2018-05-31T16:52:29Z

done

peterschrammel · 2018-06-03T14:14:49Z

.travis.yml

      before_install:
-        - mkdir bin ; ln -s /usr/bin/clang-3.7 bin/gcc
+        - mkdir bin ; ln -s /usr/bin/gcc-5 bin/gcc


it still seems a bit magical that gcc-5 is even present.

libstdc++-5-dev (https://github.com/diffblue/cbmc/pull/2217/files#diff-354f30a63fb0907d4ad57269548329e3R169) depends on package gcc-5

8de6a33 Merge pull request diffblue#2006 from tautschnig/opt-no-self-loops 6605699 Merge pull request diffblue#2217 from diffblue/c-preprocessing-cleanout f1d787b Merge pull request diffblue#2166 from tautschnig/out-of-bounds 25339d5 Add option not to transform self-loops into assumes 5e6a3af Merge pull request diffblue#2249 from tautschnig/attribute-used d3d888b Bounds check for flexible array members 41003e8 Handle negative byte_extract offsets efea5c4 Fix flattening of access beyond type-specified bounds 0ec87c8 Merge pull request diffblue#2271 from diffblue/letification 090790a Interpret GCC's attribute __used__ 7985716 Merge pull request diffblue#2252 from tautschnig/fresh-symbol-cleanup 022846a letify: use irep_hash_mapt when hashing is expensive 15dff7d Merge pull request diffblue#2260 from antlechner/antonia/annotation-class-value 9a0ffae added irep_hash_mapt da0adfe bugfix: irep_hash_containert now keeps a copy of the contained ireps 45436ce use std::size_t for container sizes 0c26a53 let_count_idt is now a struct e0a5142 Merge pull request diffblue#2206 from diffblue/use-get_identifier e0ad069 Add support for Java annotations with Class value 3817341 Merge pull request diffblue#2237 from smowton/smowton/feature/initialize-class-literals 25c097e use get_identifier() instead of get(ID_identifier) on symbols 4eda8ad Java class literals: init using a library hook when possible 70f13f3 Merge pull request diffblue#1906 from tautschnig/missing-return-semantics 57885a5 Merge pull request diffblue#1868 from tautschnig/fix-1867 b49822e Merge pull request diffblue#2028 from tautschnig/regression-fix 2815e84 Merge pull request diffblue#2259 from smowton/smowton/feature/note-abstract-methods 09b8cf7 Merge pull request diffblue#2014 from tautschnig/cadical-experiment f50237b Merge pull request diffblue#1967 from romainbrenguier/refactor/drop-constraint-inheritance2 3f951dd Merge pull request diffblue#2234 from nmanthey/upstream-fpr c6c2928 Drop inheritance from constraint on exprt 0ffd0ae Replace negation of constraint by a method f653dec use compiler defaults for gcc defines a31f530 remove need to do preprocessing on 16-bit test 24210e9 enable AWS Codebuild to do -m32 bfae4e3 enable Travis to do -m32 34a3d85 Merge pull request diffblue#2247 from antlechner/antonia/annotation-conversion 15ed961 Note when symbol-table entries are abstract methods 3a7135a Add module_dependencies.txt in test folder 1fa0b97 Generalize and rename does_annotation_exist 1db0af4 Define inverse function of convert_annotations ff25b2c get_max: do not parse every symbol name in the symbol table b603703 Add missing override 70da606 Merge pull request diffblue#2251 from tautschnig/rename-cleanup 49429cf Merge pull request diffblue#2257 from owen-jones-diffblue/owen-jones-diffblue/fix-cmake-macro 4b7a195 Improve naming of annotation variables 57d96e5 Fix CMake macro f9058e7 Merge pull request diffblue#2246 from diffblue/z3-fpa 6b0f265 Merge pull request diffblue#2248 from thk123/bugfix/doxygen-including-jbmc 72e99a0 Merge pull request diffblue#2201 from diffblue/remove-incomplete-type-constructors d4abbea smt2 implementation for popcount_exprt e8fa1c9 bswap_exprt now knows how many bits a byte has a6652d2 Merge pull request diffblue#2255 from tautschnig/speedup-no-pointer-check 4b0a2d6 goto_check: do not unnecessarily build size-of expressions 1fe7cd7 remove mathematical_typet() constructor, which produces an incomplete object 25d393b remove vector_typet() constructor, which produces an incomplete object e7c52e4 remove range_typet() constructor, which produces an incomplete object f92083d remove array_typet() constructor, which produces an incomplete object 72f63f3 remove tag_typet() constructor, which produces an incomplete object 516ed14 remove symbol_typet() constructor, which produces an incomplete object 4215f21 Consistently use get_fresh_aux_symbol instead of local implementations e6cd488 Remove unused goto_symext::new_name c24b820 Remove goto_convertt::lookup a816b26 Do not include rename.h when not using its functions 52ab088 called_functions: use unordered_set 157a12c Fix doxyfile to include JBMC documentation 026e93f function-pointer-removal: drop unused set b75fcbc smt2 implementation for bswap_exprt e276b27 Avoid extern/parameter name collisions in show-goto-functions/dump-c output 87c5948 C front-end: Record extern declarations in current scope a47941d perf-test: add -W/--witness-check to validate SV-COMP witness checking 5b0395f perf-test: Update Ubuntu AMI ids for latest version 1288ec7 perf-test: speed up builds just like e7bb127 did afccaec Provide goto-cc in performance tests f802d87 Support CaDiCaL in performance tests, remove redundant script 7872f7c Replace a missing return value by nondet 829068f Don't require the simplifier to solve this regression test git-subtree-dir: cbmc git-subtree-split: 8de6a33

kroening assigned tautschnig May 22, 2018

kroening requested review from tautschnig, peterschrammel and chrisr-diffblue May 22, 2018 07:56

kroening force-pushed the c-preprocessing-cleanout branch from a731181 to 16efc1d Compare May 22, 2018 07:59

kroening added C++ Front End C Front End labels May 22, 2018

kroening force-pushed the c-preprocessing-cleanout branch 2 times, most recently from 4b9de00 to ea19e1b Compare May 22, 2018 08:11

tautschnig requested changes May 22, 2018

View reviewed changes

tautschnig assigned kroening and unassigned tautschnig May 22, 2018

kroening force-pushed the c-preprocessing-cleanout branch from ea19e1b to da589ff Compare May 22, 2018 13:21

kroening requested a review from smowton as a code owner May 22, 2018 13:21

kroening force-pushed the c-preprocessing-cleanout branch 2 times, most recently from 39a82f6 to 271700a Compare May 22, 2018 15:43

kroening requested review from forejtv and thk123 as code owners May 22, 2018 15:43

kroening force-pushed the c-preprocessing-cleanout branch 6 times, most recently from 0d702d5 to bc7ebaa Compare May 22, 2018 21:03

smowton reviewed May 23, 2018

View reviewed changes

chrisr-diffblue force-pushed the c-preprocessing-cleanout branch from ec8436f to 909b3a7 Compare May 25, 2018 13:45

kroening assigned tautschnig and unassigned kroening May 26, 2018

tautschnig reviewed May 29, 2018

View reviewed changes

tautschnig assigned kroening and unassigned tautschnig May 29, 2018

tautschnig approved these changes May 31, 2018

View reviewed changes

Daniel Kroening added 4 commits May 31, 2018 17:51

enable Travis to do -m32

bfae4e3

This requires changing the compiler that runs the tests from clang to gcc-5.

enable AWS Codebuild to do -m32

24210e9

remove need to do preprocessing on 16-bit test

a31f530

use compiler defaults for gcc defines

f653dec

kroening force-pushed the c-preprocessing-cleanout branch from 909b3a7 to f653dec Compare May 31, 2018 16:52

kroening assigned peterschrammel and thk123 and unassigned kroening May 31, 2018

peterschrammel approved these changes Jun 3, 2018

View reviewed changes

kroening merged commit 6605699 into develop Jun 4, 2018

kroening deleted the c-preprocessing-cleanout branch June 4, 2018 12:26

Provide feedback

Saved searches

Use saved searches to filter your results more quickly

use compiler defaults for gcc defines #2217

use compiler defaults for gcc defines #2217

kroening commented May 22, 2018

tautschnig commented May 22, 2018

kroening commented May 22, 2018

tautschnig commented May 22, 2018

kroening commented May 22, 2018

tautschnig left a comment

tautschnig May 22, 2018

tautschnig May 22, 2018

kroening May 22, 2018

tautschnig May 22, 2018

kroening May 22, 2018

chrisr-diffblue May 22, 2018 •

edited

Loading

tautschnig May 22, 2018

kroening May 22, 2018

kroening May 22, 2018

tautschnig May 22, 2018

chrisr-diffblue May 22, 2018

smowton May 23, 2018

chrisr-diffblue May 23, 2018

kroening May 23, 2018

kroening May 30, 2018

kroening commented May 23, 2018

tautschnig commented May 23, 2018

peterschrammel commented May 25, 2018

tautschnig May 29, 2018

kroening May 30, 2018

tautschnig May 30, 2018

kroening May 30, 2018

tautschnig May 31, 2018

peterschrammel Jun 3, 2018

tautschnig May 31, 2018

kroening commented May 31, 2018

peterschrammel Jun 3, 2018

use compiler defaults for gcc defines #2217

use compiler defaults for gcc defines #2217

Conversation

kroening commented May 22, 2018

tautschnig commented May 22, 2018

kroening commented May 22, 2018

tautschnig commented May 22, 2018

kroening commented May 22, 2018

tautschnig left a 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

chrisr-diffblue May 22, 2018 • edited Loading

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

kroening commented May 23, 2018

tautschnig commented May 23, 2018

peterschrammel commented May 25, 2018

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

kroening commented May 31, 2018

Choose a reason for hiding this comment

chrisr-diffblue May 22, 2018 •

edited

Loading