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