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