cprover
gcc_mode.cpp
Go to the documentation of this file.
1 /*******************************************************************\
2 
3 Module: GCC Mode
4 
5 Author: CM Wintersteiger, 2006
6 
7 \*******************************************************************/
8 
11 
12 #include "gcc_mode.h"
13 
14 #ifdef _WIN32
15 #define EX_OK 0
16 #define EX_USAGE 64
17 #define EX_SOFTWARE 70
18 #else
19 #include <sysexits.h>
20 #endif
21 
22 #include <algorithm>
23 #include <cstddef>
24 #include <cstdio>
25 #include <iostream>
26 #include <iterator>
27 #include <fstream>
28 #include <cstring>
29 #include <numeric>
30 #include <sstream>
31 
32 #include <json/json_parser.h>
33 
34 #include <util/expr.h>
35 #include <util/c_types.h>
36 #include <util/arith_tools.h>
37 #include <util/invariant.h>
38 #include <util/tempdir.h>
39 #include <util/tempfile.h>
40 #include <util/config.h>
41 #include <util/prefix.h>
42 #include <util/suffix.h>
43 #include <util/get_base_name.h>
44 #include <util/run.h>
45 #include <util/replace_symbol.h>
46 
48 
49 #include "hybrid_binary.h"
50 #include "linker_script_merge.h"
51 
52 static std::string compiler_name(
53  const cmdlinet &cmdline,
54  const std::string &base_name)
55 {
56  if(cmdline.isset("native-compiler"))
57  return cmdline.get_value("native-compiler");
58 
59  if(base_name=="bcc" ||
60  base_name.find("goto-bcc")!=std::string::npos)
61  return "bcc";
62 
63  std::string::size_type pos=base_name.find("goto-gcc");
64 
65  if(pos==std::string::npos ||
66  base_name=="goto-gcc" ||
67  base_name=="goto-ld")
68  {
69  #ifdef __FreeBSD__
70  return "clang";
71  #else
72  return "gcc";
73  #endif
74  }
75 
76  std::string result=base_name;
77  result.replace(pos, 8, "gcc");
78 
79  return result;
80 }
81 
82 static std::string linker_name(
83  const cmdlinet &cmdline,
84  const std::string &base_name)
85 {
86  if(cmdline.isset("native-linker"))
87  return cmdline.get_value("native-linker");
88 
89  std::string::size_type pos=base_name.find("goto-ld");
90 
91  if(pos==std::string::npos ||
92  base_name=="goto-gcc" ||
93  base_name=="goto-ld")
94  return "ld";
95 
96  std::string result=base_name;
97  result.replace(pos, 7, "ld");
98 
99  return result;
100 }
101 
103  goto_cc_cmdlinet &_cmdline,
104  const std::string &_base_name,
105  bool _produce_hybrid_binary):
106  goto_cc_modet(_cmdline, _base_name, gcc_message_handler),
107  produce_hybrid_binary(_produce_hybrid_binary),
108  goto_binary_tmp_suffix(".goto-cc-saved"),
109 
110  // Keys are architectures specified in configt::set_arch().
111  // Values are lists of GCC architectures that can be supplied as
112  // arguments to the -march, -mcpu, and -mtune flags (see the GCC
113  // manual https://gcc.gnu.org/onlinedocs/).
114  arch_map(
115  {
116  // ARM information taken from the following:
117  //
118  // the "ARM core timeline" table on this page:
119  // https://en.wikipedia.org/wiki/List_of_ARM_microarchitectures
120  //
121  // articles on particular core groups, e.g.
122  // https://en.wikipedia.org/wiki/ARM9
123  //
124  // The "Cores" table on this page:
125  // https://en.wikipedia.org/wiki/ARM_architecture
126  // NOLINTNEXTLINE(whitespace/braces)
127  {"arm", {
128  "strongarm", "strongarm110", "strongarm1100", "strongarm1110",
129  "arm2", "arm250", "arm3", "arm6", "arm60", "arm600", "arm610",
130  "arm620", "fa526", "fa626", "fa606te", "fa626te", "fmp626",
131  "xscale", "iwmmxt", "iwmmxt2", "xgene1"
132  }}, // NOLINTNEXTLINE(whitespace/braces)
133  {"armhf", {
134  "armv7", "arm7m", "arm7d", "arm7dm", "arm7di", "arm7dmi",
135  "arm70", "arm700", "arm700i", "arm710", "arm710c", "arm7100",
136  "arm720", "arm7500", "arm7500fe", "arm7tdmi", "arm7tdmi-s",
137  "arm710t", "arm720t", "arm740t", "mpcore", "mpcorenovfp",
138  "arm8", "arm810", "arm9", "arm9e", "arm920", "arm920t",
139  "arm922t", "arm946e-s", "arm966e-s", "arm968e-s", "arm926ej-s",
140  "arm940t", "arm9tdmi", "arm10tdmi", "arm1020t", "arm1026ej-s",
141  "arm10e", "arm1020e", "arm1022e", "arm1136j-s", "arm1136jf-s",
142  "arm1156t2-s", "arm1156t2f-s", "arm1176jz-s", "arm1176jzf-s",
143  "cortex-a5", "cortex-a7", "cortex-a8", "cortex-a9",
144  "cortex-a12", "cortex-a15", "cortex-a53", "cortex-r4",
145  "cortex-r4f", "cortex-r5", "cortex-r7", "cortex-m7",
146  "cortex-m4", "cortex-m3", "cortex-m1", "cortex-m0",
147  "cortex-m0plus", "cortex-m1.small-multiply",
148  "cortex-m0.small-multiply", "cortex-m0plus.small-multiply",
149  "marvell-pj4", "ep9312", "fa726te",
150  }}, // NOLINTNEXTLINE(whitespace/braces)
151  {"arm64", {
152  "cortex-a57", "cortex-a72", "exynos-m1"
153  }}, // NOLINTNEXTLINE(whitespace/braces)
154  {"hppa", {"1.0", "1.1", "2.0"}}, // NOLINTNEXTLINE(whitespace/braces)
155  // PowerPC
156  // https://en.wikipedia.org/wiki/List_of_PowerPC_processors
157  // NOLINTNEXTLINE(whitespace/braces)
158  {"powerpc", {
159  "powerpc", "601", "602", "603", "603e", "604", "604e", "630",
160  // PowerPC G3 == 7xx series
161  "G3", "740", "750",
162  // PowerPC G4 == 74xx series
163  "G4", "7400", "7450",
164  // SoC and low power: https://en.wikipedia.org/wiki/PowerPC_400
165  "401", "403", "405", "405fp", "440", "440fp", "464", "464fp",
166  "476", "476fp",
167  // e series. x00 are 32-bit, x50 are 64-bit. See e.g.
168  // https://en.wikipedia.org/wiki/PowerPC_e6500
169  "e300c2", "e300c3", "e500mc", "ec603e",
170  // https://en.wikipedia.org/wiki/Titan_(microprocessor)
171  "titan",
172  }},
173  // NOLINTNEXTLINE(whitespace/braces)
174  {"powerpc64", {
175  "powerpc64",
176  // First IBM 64-bit processor
177  "620",
178  "970", "G5"
179  // All IBM POWER processors are 64 bit, but POWER 8 is
180  // little-endian so not in this list.
181  // https://en.wikipedia.org/wiki/Ppc64
182  "power3", "power4", "power5", "power5+", "power6", "power6x",
183  "power7", "rs64",
184  // e series SoC chips. x00 are 32-bit, x50 are 64-bit. See e.g.
185  // https://en.wikipedia.org/wiki/PowerPC_e6500
186  "e500mc64", "e5500", "e6500",
187  // https://en.wikipedia.org/wiki/IBM_A2
188  "a2",
189  }},
190  // The latest Power processors are little endian.
191  {"powerpc64le", {"powerpc64le", "power8"}},
192  // There are two MIPS architecture series. The 'old' one comprises
193  // MIPS I - MIPS V (where MIPS I and MIPS II are 32-bit
194  // architectures, and the III, IV and V are 64-bit). The 'new'
195  // architecture series comprises MIPS32 and MIPS64. Source: [0].
196  //
197  // CPROVER's names for these are in configt::this_architecture(),
198  // in particular note the preprocessor variable names. MIPS
199  // processors can run in little-endian or big-endian mode; [1]
200  // gives more information on particular processors. Particular
201  // processors and their architectures are at [2]. This means that
202  // we cannot use the processor flags alone to decide which CPROVER
203  // name to use; we also need to check for the -EB or -EL flags to
204  // decide whether little- or big-endian code should be generated.
205  // Therefore, the keys in this part of the map don't directly map
206  // to CPROVER architectures.
207  //
208  // [0] https://en.wikipedia.org/wiki/MIPS_architecture
209  // [1] https://www.debian.org/ports/mips/
210  // [2] https://en.wikipedia.org/wiki/List_of_MIPS_architecture_processors
211  // NOLINTNEXTLINE(whitespace/braces)
212  {"mips64n", {
213  "loongson2e", "loongson2f", "loongson3a", "mips64", "mips64r2",
214  "mips64r3", "mips64r5", "mips64r6 4kc", "5kc", "5kf", "20kc",
215  "octeon", "octeon+", "octeon2", "octeon3", "sb1", "vr4100",
216  "vr4111", "vr4120", "vr4130", "vr4300", "vr5000", "vr5400",
217  "vr5500", "sr71000", "xlp",
218  }}, // NOLINTNEXTLINE(whitespace/braces)
219  {"mips32n", {
220  "mips32", "mips32r2", "mips32r3", "mips32r5", "mips32r6",
221  // https://www.imgtec.com/mips/classic/
222  "4km", "4kp", "4ksc", "4kec", "4kem", "4kep", "4ksd", "24kc",
223  "24kf2_1", "24kf1_1", "24kec", "24kef2_1", "24kef1_1", "34kc",
224  "34kf2_1", "34kf1_1", "34kn", "74kc", "74kf2_1", "74kf1_1",
225  "74kf3_2", "1004kc", "1004kf2_1", "1004kf1_1", "m4k", "m14k",
226  "m14kc", "m14ke", "m14kec",
227  // https://en.wikipedia.org/wiki/List_of_MIPS_architecture_processors
228  "p5600", "xlr",
229  }}, // NOLINTNEXTLINE(whitespace/braces)
230  {"mips32o", {
231  "mips1", "mips2", "r2000", "r3000",
232  "r6000", // Not a mistake, r4000 came out _after_ this
233  }}, // NOLINTNEXTLINE(whitespace/braces)
234  {"mips64o", {
235  "mips3", "mips4", "r4000", "r4400", "r4600", "r4650", "r4700",
236  "r8000", "rm7000", "rm9000", "r10000", "r12000", "r14000",
237  "r16000",
238  }},
239  // These are IBM mainframes. s390 is 32-bit; s390x is 64-bit [0].
240  // Search that page for s390x and note that 32-bit refers to
241  // everything "prior to 2000's z900 model". The list of model
242  // numbers is at [1].
243  // [0] https://en.wikipedia.org/wiki/Linux_on_z_Systems
244  // [1] https://en.wikipedia.org/wiki/IBM_System_z
245  // NOLINTNEXTLINE(whitespace/braces)
246  {"s390", {
247  "z900", "z990", "g5", "g6",
248  }}, // NOLINTNEXTLINE(whitespace/braces)
249  {"s390x", {
250  "z9-109", "z9-ec", "z10", "z196", "zEC12", "z13"
251  }},
252  // SPARC
253  // In the "Implementations" table of [0], everything with an arch
254  // version up to V8 is 32-bit. V9 and onward are 64-bit.
255  // [0] https://en.wikipedia.org/wiki/SPARC
256  // NOLINTNEXTLINE(whitespace/braces)
257  {"sparc", {
258  "v7", "v8", "leon", "leon3", "leon3v7", "cypress", "supersparc",
259  "hypersparc", "sparclite", "f930", "f934", "sparclite86x",
260  "tsc701",
261  }}, // NOLINTNEXTLINE(whitespace/braces)
262  {"sparc64", {
263  "v9", "ultrasparc", "ultrasparc3", "niagara", "niagara2",
264  "niagara3", "niagara4",
265  }}, // NOLINTNEXTLINE(whitespace/braces)
266  {"ia64", {
267  "itanium", "itanium1", "merced", "itanium2", "mckinley"
268  }}, // NOLINTNEXTLINE(whitespace/braces)
269  // x86 and x86_64. See
270  // https://en.wikipedia.org/wiki/List_of_AMD_microprocessors
271  // https://en.wikipedia.org/wiki/List_of_Intel_microprocessors
272  {"i386", {
273  // Intel generic
274  "i386", "i486", "i586", "i686",
275  // AMD
276  "k6", "k6-2", "k6-3", "athlon" "athlon-tbird", "athlon-4",
277  "athlon-xp", "athlon-mp",
278  // Everything called "pentium" by GCC is 32 bits; the only 64-bit
279  // Pentium flag recognized by GCC is "nocona".
280  "pentium", "pentium-mmx", "pentiumpro" "pentium2", "pentium3",
281  "pentium3m", "pentium-m" "pentium4", "pentium4m", "prescott",
282  // Misc
283  "winchip-c6", "winchip2", "c3", "c3-2", "geode",
284  }}, // NOLINTNEXTLINE(whitespace/braces)
285  {"x86_64", {
286  // Intel
287  "nocona", "core2", "nehalem" "westmere", "sandybridge", "knl",
288  "ivybridge", "haswell", "broadwell" "bonnell", "silvermont",
289  // AMD generic
290  "k8", "k8-sse3", "opteron", "athlon64", "athlon-fx",
291  "opteron-sse3" "athlon64-sse3", "amdfam10", "barcelona",
292  // AMD "bulldozer" (high power, family 15h)
293  "bdver1", "bdver2" "bdver3", "bdver4",
294  // AMD "bobcat" (low power, family 14h)
295  "btver1", "btver2",
296  }},
297  })
298 {
299 }
300 
301 bool gcc_modet::needs_preprocessing(const std::string &file)
302 {
303  if(has_suffix(file, ".c") ||
304  has_suffix(file, ".cc") ||
305  has_suffix(file, ".cp") ||
306  has_suffix(file, ".cpp") ||
307  has_suffix(file, ".CPP") ||
308  has_suffix(file, ".c++") ||
309  has_suffix(file, ".C"))
310  return true;
311  else
312  return false;
313 }
314 
317 {
318  if(cmdline.isset('?') ||
319  cmdline.isset("help"))
320  {
321  help();
322  return EX_OK;
323  }
324 
327 
328  auto default_verbosity = (cmdline.isset("Wall") || cmdline.isset("Wextra")) ?
331  cmdline.get_value("verbosity"), default_verbosity, gcc_message_handler);
332 
333  bool act_as_bcc=
334  base_name=="bcc" ||
335  base_name.find("goto-bcc")!=std::string::npos;
336 
337  // if we are gcc or bcc, then get the version number
339 
340  if((cmdline.isset('v') && cmdline.have_infile_arg()) ||
341  (cmdline.isset("version") && !produce_hybrid_binary))
342  {
343  // "-v" a) prints the version and b) increases verbosity.
344  // Compilation continues, don't exit!
345 
346  if(act_as_bcc)
347  std::cout << "bcc: version " << gcc_version
348  << " (goto-cc " CBMC_VERSION ")\n";
349  else
350  {
352  std::cout << "clang version " << gcc_version
353  << " (goto-cc " CBMC_VERSION ")\n";
354  else
355  std::cout << "gcc (goto-cc " CBMC_VERSION ") " << gcc_version << '\n';
356  }
357  }
358 
359  compilet compiler(cmdline,
361  cmdline.isset("Werror") &&
362  cmdline.isset("Wextra") &&
363  !cmdline.isset("Wno-error"));
364 
365  if(cmdline.isset("version"))
366  {
368  return run_gcc(compiler);
369 
370  std::cout
371  << '\n'
372  << "Copyright (C) 2006-2018 Daniel Kroening, Christoph Wintersteiger\n"
373  << "CBMC version: " CBMC_VERSION << '\n'
374  << "Architecture: " << config.this_architecture() << '\n'
375  << "OS: " << config.this_operating_system() << '\n';
376 
378  std::cout << "clang: " << gcc_version << '\n';
379  else
380  std::cout << "gcc: " << gcc_version << '\n';
381 
382  return EX_OK; // Exit!
383  }
384 
385  if(
386  cmdline.isset("dumpmachine") || cmdline.isset("dumpspecs") ||
387  cmdline.isset("dumpversion") || cmdline.isset("print-sysroot") ||
388  cmdline.isset("print-sysroot-headers-suffix"))
389  {
391  return run_gcc(compiler);
392 
393  // GCC will only print one of these, even when multiple arguments are
394  // passed, so we do the same
395  if(cmdline.isset("dumpmachine"))
396  std::cout << config.this_architecture() << '\n';
397  else if(cmdline.isset("dumpversion"))
398  std::cout << gcc_version << '\n';
399 
400  // we don't have any meaningful output for the other options, and GCC
401  // doesn't necessarily produce non-empty output either
402 
403  return EX_OK;
404  }
405 
406  if(act_as_bcc)
407  {
409  debug() << "BCC mode (hybrid)" << eom;
410  else
411  debug() << "BCC mode" << eom;
412  }
413  else
414  {
416  debug() << "GCC mode (hybrid)" << eom;
417  else
418  debug() << "GCC mode" << eom;
419  }
420 
421  // determine actions to be undertaken
422  if(cmdline.isset('S'))
423  compiler.mode=compilet::ASSEMBLE_ONLY;
424  else if(cmdline.isset('c'))
425  compiler.mode=compilet::COMPILE_ONLY;
426  else if(cmdline.isset('E'))
427  compiler.mode=compilet::PREPROCESS_ONLY;
428  else if(cmdline.isset("shared") ||
429  cmdline.isset('r')) // really not well documented
430  compiler.mode=compilet::COMPILE_LINK;
431  else
432  compiler.mode=compilet::COMPILE_LINK_EXECUTABLE;
433 
434  // In gcc mode, we have just pass on to gcc to handle the following:
435  // * if -M or -MM is given, we do dependencies only
436  // * preprocessing (-E)
437  // * no input files given
438 
439  if(cmdline.isset('M') ||
440  cmdline.isset("MM") ||
441  cmdline.isset('E') ||
443  return run_gcc(compiler); // exit!
444 
445  // get configuration
446  config.set(cmdline);
447 
448  // Intel-specific
449  // in GCC, m16 is 32-bit (!), as documented here:
450  // https://gcc.gnu.org/bugzilla/show_bug.cgi?id=59672
451  if(cmdline.isset("m16") ||
452  cmdline.isset("m32") || cmdline.isset("mx32"))
453  {
454  config.ansi_c.arch="i386";
456  }
457  else if(cmdline.isset("m64"))
458  {
459  config.ansi_c.arch="x86_64";
461  }
462 
463  // ARM-specific
464  if(cmdline.isset("mbig-endian") || cmdline.isset("mbig"))
466  else if(cmdline.isset("little-endian") || cmdline.isset("mlittle"))
468 
469  if(cmdline.isset("mthumb") || cmdline.isset("mthumb-interwork"))
471 
472  // -mcpu sets both the arch and tune, but should only be used if
473  // neither -march nor -mtune are passed on the command line.
474  std::string target_cpu=
475  cmdline.isset("march") ? cmdline.get_value("march") :
476  cmdline.isset("mtune") ? cmdline.get_value("mtune") :
477  cmdline.isset("mcpu") ? cmdline.get_value("mcpu") : "";
478 
479  if(target_cpu!="")
480  {
481  // Work out what CPROVER architecture we should target.
482  for(auto &pair : arch_map)
483  for(auto &processor : pair.second)
484  if(processor==target_cpu)
485  {
486  if(pair.first.find("mips")==std::string::npos)
487  config.set_arch(pair.first);
488  else
489  {
490  // Targeting a MIPS processor. MIPS is special; we also need
491  // to know the endianness. -EB (big-endian) is the default.
492  if(cmdline.isset("EL"))
493  {
494  if(pair.first=="mips32o")
495  config.set_arch("mipsel");
496  else if(pair.first=="mips32n")
497  config.set_arch("mipsn32el");
498  else
499  config.set_arch("mips64el");
500  }
501  else
502  {
503  if(pair.first=="mips32o")
504  config.set_arch("mips");
505  else if(pair.first=="mips32n")
506  config.set_arch("mipsn32");
507  else
508  config.set_arch("mips64");
509  }
510  }
511  }
512  }
513 
514  // -fshort-wchar makes wchar_t "short unsigned int"
515  if(cmdline.isset("fshort-wchar"))
516  {
519  }
520 
521  // -fsingle-precision-constant makes floating-point constants "float"
522  // instead of double
523  if(cmdline.isset("-fsingle-precision-constant"))
525 
526  // ISO/IEC TS 18661-3:2015 support was introduced with gcc 7.0
530 
531  int gcc_float128_minor_version = config.ansi_c.arch == "x86_64" ? 3 : 5;
532 
535  gcc_version.is_at_least(4, gcc_float128_minor_version);
536 
537  // -fshort-double makes double the same as float
538  if(cmdline.isset("fshort-double"))
540 
541  switch(compiler.mode)
542  {
544  debug() << "Linking a library only" << eom; break;
546  debug() << "Compiling only" << eom; break;
548  debug() << "Assembling only" << eom; break;
550  debug() << "Preprocessing only" << eom; break;
552  debug() << "Compiling and linking a library" << eom; break;
554  debug() << "Compiling and linking an executable" << eom; break;
555  }
556 
557  if(cmdline.isset("i386-win32") ||
558  cmdline.isset("winx64"))
559  {
560  // We may wish to reconsider the below.
562  debug() << "Enabling Visual Studio syntax" << eom;
563  }
564  else if(config.this_operating_system()=="macos")
566  else
568 
569  if(compiler.mode==compilet::ASSEMBLE_ONLY)
570  compiler.object_file_extension="s";
571  else
572  compiler.object_file_extension="o";
573 
574  if(cmdline.isset("std"))
575  {
576  std::string std_string=cmdline.get_value("std");
577 
578  if(std_string=="gnu89" || std_string=="c89")
580 
581  if(std_string=="gnu99" || std_string=="c99" || std_string=="iso9899:1999" ||
582  std_string=="gnu9x" || std_string=="c9x" || std_string=="iso9899:199x")
584 
585  if(std_string=="gnu11" || std_string=="c11" ||
586  std_string=="gnu1x" || std_string=="c1x")
588 
589  if(std_string=="c++11" || std_string=="c++1x" ||
590  std_string=="gnu++11" || std_string=="gnu++1x" ||
591  std_string=="c++1y" ||
592  std_string=="gnu++1y")
593  config.cpp.set_cpp11();
594 
595  if(std_string=="gnu++14" || std_string=="c++14")
596  config.cpp.set_cpp14();
597  }
598  else
599  {
602  }
603 
604  // gcc's default is 32 bits for wchar_t
605  if(cmdline.isset("short-wchar"))
607 
608  // gcc's default is 64 bits for double
609  if(cmdline.isset("short-double"))
611 
612  // gcc's default is signed chars on most architectures
613  if(cmdline.isset("funsigned-char"))
615 
616  if(cmdline.isset("fsigned-char"))
618 
619  if(cmdline.isset('U'))
621 
622  if(cmdline.isset("undef"))
623  config.ansi_c.preprocessor_options.push_back("-undef");
624 
625  if(cmdline.isset("nostdinc"))
626  config.ansi_c.preprocessor_options.push_back("-nostdinc");
627 
628  if(cmdline.isset('L'))
629  compiler.library_paths=cmdline.get_values('L');
630  // Don't add the system paths!
631 
632  if(cmdline.isset('l'))
633  compiler.libraries=cmdline.get_values('l');
634 
635  if(cmdline.isset("static"))
636  compiler.libraries.push_back("c");
637 
638  if(cmdline.isset("pthread"))
639  compiler.libraries.push_back("pthread");
640 
641  if(cmdline.isset('o'))
642  {
643  // given gcc -o file1 -o file2,
644  // gcc will output to file2, not file1
645  compiler.output_file_object=cmdline.get_values('o').back();
646  compiler.output_file_executable=cmdline.get_values('o').back();
647  }
648  else
649  {
650  compiler.output_file_object="";
651  compiler.output_file_executable="a.out";
652  }
653 
654  // We now iterate over any input files
655 
656  temp_dirt temp_dir("goto-cc-XXXXXX");
657 
658  {
659  std::string language;
660 
661  for(goto_cc_cmdlinet::parsed_argvt::iterator
662  arg_it=cmdline.parsed_argv.begin();
663  arg_it!=cmdline.parsed_argv.end();
664  arg_it++)
665  {
666  if(arg_it->is_infile_name)
667  {
668  // do any preprocessing needed
669 
670  if(language=="cpp-output" || language=="c++-cpp-output")
671  {
672  compiler.add_input_file(arg_it->arg);
673  }
674  else if(language=="c" || language=="c++" ||
675  (language=="" && needs_preprocessing(arg_it->arg)))
676  {
677  std::string new_suffix;
678 
679  if(language=="c")
680  new_suffix=".i";
681  else if(language=="c++")
682  new_suffix=".ii";
683  else
684  new_suffix=has_suffix(arg_it->arg, ".c")?".i":".ii";
685 
686  std::string new_name=
687  get_base_name(arg_it->arg, true)+new_suffix;
688  std::string dest=temp_dir(new_name);
689 
690  int exit_code=
691  preprocess(language, arg_it->arg, dest, act_as_bcc);
692 
693  if(exit_code!=0)
694  {
695  error() << "preprocessing has failed" << eom;
696  return exit_code;
697  }
698 
699  compiler.add_input_file(dest);
700  }
701  else
702  compiler.add_input_file(arg_it->arg);
703  }
704  else if(arg_it->arg=="-x")
705  {
706  arg_it++;
707  if(arg_it!=cmdline.parsed_argv.end())
708  {
709  language=arg_it->arg;
710  if(language=="none")
711  language="";
712  }
713  }
714  else if(has_prefix(arg_it->arg, "-x"))
715  {
716  language=std::string(arg_it->arg, 2, std::string::npos);
717  if(language=="none")
718  language="";
719  }
720  }
721  }
722 
723  // Revert to gcc in case there is no source to compile
724  // and no binary to link.
725 
726  if(compiler.source_files.empty() &&
727  compiler.object_files.empty())
728  return run_gcc(compiler); // exit!
729 
730  if(compiler.mode==compilet::ASSEMBLE_ONLY)
731  return asm_output(act_as_bcc, compiler.source_files, compiler);
732 
733  // do all the rest
734  if(compiler.doit())
735  return 1; // GCC exit code for all kinds of errors
736 
737  // We can generate hybrid ELF and Mach-O binaries
738  // containing both executable machine code and the goto-binary.
739  if(produce_hybrid_binary && !act_as_bcc)
740  return gcc_hybrid_binary(compiler);
741 
742  return EX_OK;
743 }
744 
747  const std::string &language,
748  const std::string &src,
749  const std::string &dest,
750  bool act_as_bcc)
751 {
752  // build new argv
753  std::vector<std::string> new_argv;
754 
755  new_argv.reserve(cmdline.parsed_argv.size());
756 
757  bool skip_next=false;
758 
759  for(goto_cc_cmdlinet::parsed_argvt::const_iterator
760  it=cmdline.parsed_argv.begin();
761  it!=cmdline.parsed_argv.end();
762  it++)
763  {
764  if(skip_next)
765  {
766  // skip
767  skip_next=false;
768  }
769  else if(it->is_infile_name)
770  {
771  // skip
772  }
773  else if(it->arg=="-c" || it->arg=="-E" || it->arg=="-S")
774  {
775  // skip
776  }
777  else if(it->arg=="-o")
778  {
779  skip_next=true;
780  }
781  else if(has_prefix(it->arg, "-o"))
782  {
783  // ignore
784  }
785  else
786  new_argv.push_back(it->arg);
787  }
788 
789  // We just want to preprocess.
790  new_argv.push_back("-E");
791 
792  // destination file
793  std::string stdout_file;
794  if(act_as_bcc)
795  stdout_file=dest;
796  else
797  {
798  new_argv.push_back("-o");
799  new_argv.push_back(dest);
800  }
801 
802  // language, if given
803  if(language!="")
804  {
805  new_argv.push_back("-x");
806  new_argv.push_back(language);
807  }
808 
809  // source file
810  new_argv.push_back(src);
811 
812  // overwrite argv[0]
813  INVARIANT(new_argv.size()>=1, "No program name in argv");
814  new_argv[0]=native_tool_name.c_str();
815 
816  debug() << "RUN:";
817  for(std::size_t i=0; i<new_argv.size(); i++)
818  debug() << " " << new_argv[i];
819  debug() << eom;
820 
821  return run(new_argv[0], new_argv, cmdline.stdin_file, stdout_file);
822 }
823 
824 int gcc_modet::run_gcc(const compilet &compiler)
825 {
826  PRECONDITION(!cmdline.parsed_argv.empty());
827 
828  // build new argv
829  std::vector<std::string> new_argv;
830  new_argv.reserve(cmdline.parsed_argv.size());
831  for(const auto &a : cmdline.parsed_argv)
832  new_argv.push_back(a.arg);
833 
834  if(compiler.wrote_object_files())
835  {
836  // Undefine all __CPROVER macros for the system compiler
837  std::map<irep_idt, std::size_t> arities;
838  compiler.cprover_macro_arities(arities);
839  for(const auto &pair : arities)
840  {
841  std::ostringstream addition;
842  addition << "-D" << id2string(pair.first) << "(";
843  std::vector<char> params(pair.second);
844  std::iota(params.begin(), params.end(), 'a');
845  for(std::vector<char>::iterator it=params.begin(); it!=params.end(); ++it)
846  {
847  addition << *it;
848  if(it+1!=params.end())
849  addition << ",";
850  }
851  addition << ")= ";
852  new_argv.push_back(addition.str());
853  }
854  }
855 
856  // overwrite argv[0]
857  new_argv[0]=native_tool_name;
858 
859  debug() << "RUN:";
860  for(std::size_t i=0; i<new_argv.size(); i++)
861  debug() << " " << new_argv[i];
862  debug() << eom;
863 
864  return run(new_argv[0], new_argv, cmdline.stdin_file);
865 }
866 
868 {
869  {
870  bool have_files=false;
871 
872  for(goto_cc_cmdlinet::parsed_argvt::const_iterator
873  it=cmdline.parsed_argv.begin();
874  it!=cmdline.parsed_argv.end();
875  it++)
876  if(it->is_infile_name)
877  have_files=true;
878 
879  if(!have_files)
880  return EX_OK;
881  }
882 
883  std::list<std::string> output_files;
884 
885  if(cmdline.isset('c'))
886  {
887  if(cmdline.isset('o'))
888  {
889  // there should be only one input file
890  output_files.push_back(cmdline.get_value('o'));
891  }
892  else
893  {
894  for(goto_cc_cmdlinet::parsed_argvt::const_iterator
895  i_it=cmdline.parsed_argv.begin();
896  i_it!=cmdline.parsed_argv.end();
897  i_it++)
898  if(i_it->is_infile_name &&
899  needs_preprocessing(i_it->arg))
900  output_files.push_back(get_base_name(i_it->arg, true)+".o");
901  }
902  }
903  else
904  {
905  // -c is not given
906  if(cmdline.isset('o'))
907  output_files.push_back(cmdline.get_value('o'));
908  else
909  output_files.push_back("a.out");
910  }
911 
912  if(output_files.empty() ||
913  (output_files.size()==1 &&
914  output_files.front()=="/dev/null"))
915  return EX_OK;
916 
917  debug() << "Running " << native_tool_name
918  << " to generate hybrid binary" << eom;
919 
920  // save the goto-cc output files
921  std::list<std::string> goto_binaries;
922  for(std::list<std::string>::const_iterator
923  it=output_files.begin();
924  it!=output_files.end();
925  it++)
926  {
927  std::string bin_name=*it+goto_binary_tmp_suffix;
928  int result=rename(it->c_str(), bin_name.c_str());
929  if(result!=0)
930  {
931  error() << "Rename failed: " << std::strerror(errno) << eom;
932  return result;
933  }
934  goto_binaries.push_back(bin_name);
935  }
936 
937  int result=run_gcc(compiler);
938 
939  if(result==0 &&
940  cmdline.isset('T') &&
941  goto_binaries.size()==1 &&
942  output_files.size()==1)
943  {
944  linker_script_merget ls_merge(
945  compiler, output_files.front(), goto_binaries.front(),
947  result=ls_merge.add_linker_script_definitions();
948  }
949 
950  std::string native_tool;
951 
953  native_tool=linker_name(cmdline, base_name);
954  else if(has_suffix(compiler_name(cmdline, base_name), "-gcc"))
955  native_tool=compiler_name(cmdline, base_name);
956 
957  // merge output from gcc with goto-binaries
958  // using objcopy, or do cleanup if an earlier call failed
959  for(std::list<std::string>::const_iterator
960  it=output_files.begin();
961  it!=output_files.end();
962  it++)
963  {
964  std::string goto_binary=*it+goto_binary_tmp_suffix;
965 
966  if(result==0)
968  native_tool, goto_binary, *it, get_message_handler());
969  }
970 
971  return result;
972 }
973 
975  bool act_as_bcc,
976  const std::list<std::string> &preprocessed_source_files,
977  const compilet &compiler)
978 {
979  {
980  bool have_files=false;
981 
982  for(goto_cc_cmdlinet::parsed_argvt::const_iterator
983  it=cmdline.parsed_argv.begin();
984  it!=cmdline.parsed_argv.end();
985  it++)
986  if(it->is_infile_name)
987  have_files=true;
988 
989  if(!have_files)
990  return EX_OK;
991  }
992 
994  {
995  debug() << "Running " << native_tool_name
996  << " to generate native asm output" << eom;
997 
998  int result=run_gcc(compiler);
999  if(result!=0)
1000  // native tool failed
1001  return result;
1002  }
1003 
1004  std::map<std::string, std::string> output_files;
1005 
1006  if(cmdline.isset('o'))
1007  {
1008  // GCC --combine supports more than one source file
1009  for(const auto &s : preprocessed_source_files)
1010  output_files.insert(std::make_pair(s, cmdline.get_value('o')));
1011  }
1012  else
1013  {
1014  for(const std::string &s : preprocessed_source_files)
1015  output_files.insert(
1016  std::make_pair(s, get_base_name(s, true)+".s"));
1017  }
1018 
1019  if(output_files.empty() ||
1020  (output_files.size()==1 &&
1021  output_files.begin()->second=="/dev/null"))
1022  return EX_OK;
1023 
1024  debug()
1025  << "Appending preprocessed sources to generate hybrid asm output"
1026  << eom;
1027 
1028  for(const auto &so : output_files)
1029  {
1030  std::ifstream is(so.first);
1031  if(!is.is_open())
1032  {
1033  error() << "Failed to open input source " << so.first << eom;
1034  return 1;
1035  }
1036 
1037  std::ofstream os(so.second, std::ios::app);
1038  if(!os.is_open())
1039  {
1040  error() << "Failed to open output file " << so.second << eom;
1041  return 1;
1042  }
1043 
1044  const char comment=act_as_bcc ? ':' : '#';
1045 
1046  os << comment << comment << " GOTO-CC" << '\n';
1047 
1048  std::string line;
1049 
1050  while(std::getline(is, line))
1051  {
1052  os << comment << comment << line << '\n';
1053  }
1054  }
1055 
1056  return EX_OK;
1057 }
1058 
1061 {
1062  std::cout << "goto-cc understands the options of "
1063  << "gcc plus the following.\n\n";
1064 }
void set_arch_spec_arm(const irep_idt &subarch)
Definition: config.cpp:278
const bool produce_hybrid_binary
Definition: gcc_mode.h:39
const std::list< std::string > & get_values(const std::string &option) const
Definition: cmdline.cpp:110
struct configt::ansi_ct ansi_c
const std::string & id2string(const irep_idt &d)
Definition: irep.h:43
enum gcc_versiont::flavort flavor
const std::string goto_binary_tmp_suffix
Definition: gcc_mode.h:43
std::string stdin_file
int run_gcc(const compilet &compiler)
call gcc with original command line
Definition: gcc_mode.cpp:824
std::string comment(const rw_set_baset::entryt &entry, bool write)
Definition: race_check.cpp:107
int asm_output(bool act_as_bcc, const std::list< std::string > &preprocessed_source_files, const compilet &compiler)
Definition: gcc_mode.cpp:974
std::size_t single_width
Definition: config.h:37
bool single_precision_constant
Definition: config.h:47
int run(const std::string &what, const std::vector< std::string > &argv, const std::string &std_input, const std::string &std_output, const std::string &std_error)
Definition: run.cpp:82
static unsigned eval_verbosity(const std::string &user_input, const message_levelt default_verbosity, message_handlert &dest)
Parse a (user-)provided string as a verbosity level and set it as the verbosity of dest...
Definition: message.cpp:78
endiannesst endianness
Definition: config.h:76
Read Goto Programs.
literalt pos(literalt a)
Definition: literal.h:193
std::string get_value(char option) const
Definition: cmdline.cpp:45
Base class for command line interpretation.
unsignedbv_typet size_type()
Definition: c_types.cpp:58
std::size_t double_width
Definition: config.h:38
std::list< std::string > undefines
Definition: config.h:113
bool wrote_object_files() const
Has this compiler written any object files?
Definition: compile.h:77
static mstreamt & eom(mstreamt &m)
Definition: message.h:272
configt config
Definition: config.cpp:23
std::string get_base_name(const std::string &in, bool strip_suffix)
cleans a filename from path and extension
gcc_message_handlert gcc_message_handler
Definition: gcc_mode.h:37
void get(const std::string &executable)
Definition: gcc_version.cpp:19
#define INVARIANT(CONDITION, REASON)
Definition: invariant.h:205
void cprover_macro_arities(std::map< irep_idt, std::size_t > &cprover_macros) const
__CPROVER_... macros written to object files and their arities
Definition: compile.h:84
static std::string linker_name(const cmdlinet &cmdline, const std::string &base_name)
Definition: gcc_mode.cpp:82
int preprocess(const std::string &language, const std::string &src, const std::string &dest, bool act_as_bcc)
call gcc for preprocessing
Definition: gcc_mode.cpp:746
void set_cpp14()
Definition: config.h:134
bool set(const cmdlinet &cmdline)
Definition: config.cpp:737
void set_c89()
Definition: config.h:51
virtual bool isset(char option) const
Definition: cmdline.cpp:27
flavourt mode
Definition: config.h:106
Create hybrid binary with goto-binary section.
void set_arch_spec_x86_64()
Definition: config.cpp:180
gcc_modet(goto_cc_cmdlinet &_cmdline, const std::string &_base_name, bool _produce_hybrid_binary)
Definition: gcc_mode.cpp:102
void set_arch(const irep_idt &)
Definition: config.cpp:673
goto_cc_cmdlinet & cmdline
Definition: goto_cc_mode.h:37
bool is_at_least(unsigned v_major, unsigned v_minor=0, unsigned v_patchlevel=0) const
mstreamt & error() const
Definition: message.h:302
irep_idt arch
Definition: config.h:84
enum configt::cppt::cpp_standardt cpp_standard
#define PRECONDITION(CONDITION)
Definition: invariant.h:230
bool has_prefix(const std::string &s, const std::string &prefix)
Definition: converter.cpp:13
configt::ansi_ct::c_standardt default_c_standard
Definition: gcc_version.h:39
bool char_is_unsigned
Definition: config.h:43
gcc_versiont gcc_version
Definition: gcc_mode.h:66
void set_c11()
Definition: config.h:53
void help_mode() final
display command line help
Definition: gcc_mode.cpp:1060
enum configt::ansi_ct::c_standardt c_standard
std::size_t wchar_t_width
Definition: config.h:40
int gcc_hybrid_binary(compilet &compiler)
Definition: gcc_mode.cpp:867
bool Float128_type
Definition: config.h:46
int doit() final
does it.
Definition: gcc_mode.cpp:316
static bool needs_preprocessing(const std::string &)
Definition: gcc_mode.cpp:301
static irep_idt this_operating_system()
Definition: config.cpp:1309
struct configt::cppt cpp
void set_c99()
Definition: config.h:52
message_handlert & get_message_handler()
Definition: message.h:153
void set_cpp11()
Definition: config.h:133
mstreamt & result() const
Definition: message.h:312
std::string native_tool_name
Definition: gcc_mode.h:41
int hybrid_binary(const std::string &compiler_or_linker, const std::string &goto_binary_file, const std::string &output_file, message_handlert &message_handler)
Merges a goto binary into an object file (e.g.
virtual void help()
display command line help
void set_arch_spec_i386()
Definition: config.cpp:148
bool have_infile_arg() const
const std::map< std::string, std::set< std::string > > arch_map
Associate CBMC architectures with processor names.
Definition: gcc_mode.h:46
static std::string compiler_name(const cmdlinet &cmdline, const std::string &base_name)
Definition: gcc_mode.cpp:52
bool has_suffix(const std::string &s, const std::string &suffix)
Definition: suffix.h:15
parsed_argvt parsed_argv
mstreamt & debug() const
Definition: message.h:332
Merge linker script-defined symbols into a goto-program.
bool wchar_t_is_unsigned
Definition: config.h:43
std::list< std::string > preprocessor_options
Definition: config.h:114
configt::cppt::cpp_standardt default_cxx_standard
Definition: gcc_version.h:40
bool ts_18661_3_Floatn_types
Definition: config.h:45
const std::string base_name
Definition: goto_cc_mode.h:38
static irep_idt this_architecture()
Definition: config.cpp:1212
std::size_t short_int_width
Definition: config.h:34
Definition: kdev_t.h:19
Synthesise definitions of symbols that are defined in linker scripts.