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