44 const std::string &base_name)
46 if(cmdline.
isset(
"native-compiler"))
47 return cmdline.
get_value(
"native-compiler");
49 if(base_name==
"bcc" ||
50 base_name.find(
"goto-bcc")!=std::string::npos)
53 if(base_name==
"goto-clang")
56 std::string::size_type
pos=base_name.find(
"goto-gcc");
58 if(
pos==std::string::npos ||
59 base_name==
"goto-gcc" ||
62#if defined(__FreeBSD__) || defined(__OpenBSD__)
69 std::string result=base_name;
70 result.replace(
pos, 8,
"gcc");
77 const std::string &base_name)
79 if(cmdline.
isset(
"native-linker"))
80 return cmdline.
get_value(
"native-linker");
82 std::string::size_type
pos=base_name.find(
"goto-ld");
84 if(
pos==std::string::npos ||
85 base_name==
"goto-gcc" ||
89 std::string result=base_name;
90 result.replace(
pos, 7,
"ld");
97 const std::string &_base_name,
98 bool _produce_hybrid_binary):
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"
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",
145 "cortex-a57",
"cortex-a72",
"exynos-m1"
147 {
"hppa", {
"1.0",
"1.1",
"2.0"}},
152 "powerpc",
"601",
"602",
"603",
"603e",
"604",
"604e",
"630",
156 "G4",
"7400",
"7450",
158 "401",
"403",
"405",
"405fp",
"440",
"440fp",
"464",
"464fp",
162 "e300c2",
"e300c3",
"e500mc",
"ec603e",
175 "power3",
"power4",
"power5",
"power5+",
"power6",
"power6x",
179 "e500mc64",
"e5500",
"e6500",
184 {
"powerpc64le", {
"powerpc64le",
"power8"}},
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",
213 "mips32",
"mips32r2",
"mips32r3",
"mips32r5",
"mips32r6",
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",
224 "mips1",
"mips2",
"r2000",
"r3000",
228 "mips3",
"mips4",
"r4000",
"r4400",
"r4600",
"r4650",
"r4700",
229 "r8000",
"rm7000",
"rm9000",
"r10000",
"r12000",
"r14000",
240 "z900",
"z990",
"g5",
"g6",
243 "z9-109",
"z9-ec",
"z10",
"z196",
"zEC12",
"z13"
251 "v7",
"v8",
"leon",
"leon3",
"leon3v7",
"cypress",
"supersparc",
252 "hypersparc",
"sparclite",
"f930",
"f934",
"sparclite86x",
256 "v9",
"ultrasparc",
"ultrasparc3",
"niagara",
"niagara2",
257 "niagara3",
"niagara4",
260 "itanium",
"itanium1",
"merced",
"itanium2",
"mckinley"
267 "i386",
"i486",
"i586",
"i686",
269 "k6",
"k6-2",
"k6-3",
"athlon" "athlon-tbird",
"athlon-4",
270 "athlon-xp",
"athlon-mp",
273 "pentium",
"pentium-mmx",
"pentiumpro" "pentium2",
"pentium3",
274 "pentium3m",
"pentium-m" "pentium4",
"pentium4m",
"prescott",
276 "winchip-c6",
"winchip2",
"c3",
"c3-2",
"geode",
280 "nocona",
"core2",
"nehalem" "westmere",
"sandybridge",
"knl",
281 "ivybridge",
"haswell",
"broadwell" "bonnell",
"silvermont",
283 "k8",
"k8-sse3",
"opteron",
"athlon64",
"athlon-fx",
284 "opteron-sse3" "athlon64-sse3",
"amdfam10",
"barcelona",
286 "bdver1",
"bdver2" "bdver3",
"bdver4",
314 auto default_verbosity = (
cmdline.isset(
"Wall") ||
cmdline.isset(
"Wextra")) ?
323 base_name.find(
"goto-bcc")!=std::string::npos;
335 std::cout <<
"bcc: version " <<
gcc_version <<
" (goto-cc "
340 std::cout <<
"clang version " <<
gcc_version <<
" (goto-cc "
360 <<
"Copyright (C) 2006-2018 Daniel Kroening, Christoph Wintersteiger\n"
362 <<
"Architecture: " <<
config.this_architecture() <<
'\n'
363 <<
"OS: " <<
config.this_operating_system() <<
'\n';
390 cmdline.isset(
"print-sysroot-headers-suffix"))
397 if(
cmdline.isset(
"dumpmachine"))
398 std::cout <<
config.this_architecture() <<
'\n';
399 else if(
cmdline.isset(
"dumpversion"))
435 else if(
cmdline.isset(
"shared") ||
461 config.ansi_c.arch=
"i386";
462 config.ansi_c.set_arch_spec_i386();
466 config.ansi_c.arch=
"x86_64";
467 config.ansi_c.set_arch_spec_x86_64();
473 else if(
cmdline.isset(
"little-endian") ||
cmdline.isset(
"mlittle"))
477 config.ansi_c.set_arch_spec_arm(
"armhf");
481 std::string target_cpu=
486 if(!target_cpu.empty())
490 for(
auto &processor : pair.second)
491 if(processor==target_cpu)
493 if(pair.first.find(
"mips")==std::string::npos)
494 config.set_arch(pair.first);
501 if(pair.first==
"mips32o")
502 config.set_arch(
"mipsel");
503 else if(pair.first==
"mips32n")
504 config.set_arch(
"mipsn32el");
506 config.set_arch(
"mips64el");
510 if(pair.first==
"mips32o")
512 else if(pair.first==
"mips32n")
513 config.set_arch(
"mipsn32");
515 config.set_arch(
"mips64");
525 static const std::map<std::string, std::string> target_map = {
526 {
"aarch64",
"arm64" },
527 {
"aarch64_32",
"arm" },
528 {
"aarch64_be",
"none" },
532 {
"arm64_32",
"arm" },
538 {
"hexagon",
"none" },
542 {
"mips64",
"mips64" },
543 {
"mips64el",
"mips64el" },
544 {
"mipsel",
"mipsel" },
547 {
"nvptx64",
"none" },
548 {
"ppc32",
"powerpc" },
550 {
"ppc64le",
"ppc64le" },
552 {
"riscv32",
"none" },
553 {
"riscv64",
"riscv64" },
555 {
"sparcel",
"none" },
556 {
"sparcv9",
"sparc64" },
557 {
"systemz",
"none" },
559 {
"thumbeb",
"none" },
563 {
"x86_64",
"x86_64" },
566 std::string arch_quadruple =
cmdline.get_value(
"target");
568 target_map.find(arch_quadruple.substr(0, arch_quadruple.find(
'-')));
569 if(it == target_map.end())
572 config.set_arch(it->second);
576 if(
cmdline.isset(
"fshort-wchar"))
578 config.ansi_c.wchar_t_width=
config.ansi_c.short_int_width;
579 config.ansi_c.wchar_t_is_unsigned=
true;
584 if(
cmdline.isset(
"-fsingle-precision-constant"))
585 config.ansi_c.single_precision_constant=
true;
588 if(
cmdline.isset(
"fshort-double"))
594 switch(compiler.
mode)
616 if(
cmdline.isset(
"i386-win32") ||
638 std::string std_string=
cmdline.get_value(
"std");
640 if(std_string==
"gnu89" || std_string==
"c89")
643 if(std_string==
"gnu99" || std_string==
"c99" || std_string==
"iso9899:1999" ||
644 std_string==
"gnu9x" || std_string==
"c9x" || std_string==
"iso9899:199x")
647 if(std_string==
"gnu11" || std_string==
"c11" ||
648 std_string==
"gnu1x" || std_string==
"c1x")
652 std_string ==
"gnu17" || std_string ==
"c17" || std_string ==
"gnu18" ||
659 std_string ==
"gnu2x" || std_string ==
"c2x" || std_string ==
"gnu23" ||
665 if(std_string==
"c++11" || std_string==
"c++1x" ||
666 std_string==
"gnu++11" || std_string==
"gnu++1x" ||
667 std_string==
"c++1y" ||
668 std_string==
"gnu++1y")
671 if(std_string==
"gnu++14" || std_string==
"c++14")
674 if(std_string ==
"gnu++17" || std_string ==
"c++17")
684 if(
cmdline.isset(
"short-wchar"))
685 config.ansi_c.wchar_t_width=16;
688 if(
cmdline.isset(
"short-double"))
689 config.ansi_c.double_width=32;
692 if(
cmdline.isset(
"funsigned-char"))
693 config.ansi_c.char_is_unsigned=
true;
695 if(
cmdline.isset(
"fsigned-char"))
696 config.ansi_c.char_is_unsigned=
false;
702 config.ansi_c.preprocessor_options.push_back(
"-undef");
705 config.ansi_c.preprocessor_options.push_back(
"-nostdinc");
735 std::vector<temp_dirt> temp_dirs;
738 std::string language;
740 for(goto_cc_cmdlinet::parsed_argvt::iterator
741 arg_it=
cmdline.parsed_argv.begin();
742 arg_it!=
cmdline.parsed_argv.end();
745 if(arg_it->is_infile_name)
749 if(language==
"cpp-output" || language==
"c++-cpp-output")
754 language ==
"c" || language ==
"c++" ||
757 std::string new_suffix;
761 else if(language==
"c++")
764 new_suffix=
has_suffix(arg_it->arg,
".c")?
".i":
".ii";
766 std::string new_name=
769 temp_dirs.emplace_back(
"goto-cc-XXXXXX");
770 std::string dest = temp_dirs.back()(new_name);
773 preprocess(language, arg_it->arg, dest, act_as_bcc);
786 else if(arg_it->arg==
"-x")
789 if(arg_it!=
cmdline.parsed_argv.end())
791 language=arg_it->arg;
798 language=std::string(arg_it->arg, 2, std::string::npos);
809 log.
error() <<
"cannot specify -o with -c with multiple files"
838 const std::string &language,
839 const std::string &src,
840 const std::string &dest,
844 std::vector<std::string> new_argv;
846 new_argv.reserve(
cmdline.parsed_argv.size());
848 bool skip_next=
false;
850 for(goto_cc_cmdlinet::parsed_argvt::const_iterator
851 it=
cmdline.parsed_argv.begin();
860 else if(it->is_infile_name)
864 else if(it->arg==
"-c" || it->arg==
"-E" || it->arg==
"-S")
868 else if(it->arg==
"-o")
877 new_argv.push_back(it->arg);
881 new_argv.push_back(
"-E");
884 std::string stdout_file;
889 new_argv.push_back(
"-o");
890 new_argv.push_back(dest);
894 if(!language.empty())
896 new_argv.push_back(
"-x");
897 new_argv.push_back(language);
901 new_argv.push_back(src);
904 INVARIANT(new_argv.size()>=1,
"No program name in argv");
908 log.
debug() <<
"RUN:";
909 for(std::size_t i=0; i<new_argv.size(); i++)
910 log.
debug() <<
" " << new_argv[i];
913 return run(new_argv[0], new_argv,
cmdline.stdin_file, stdout_file,
"");
921 std::vector<std::string> new_argv;
922 new_argv.reserve(
cmdline.parsed_argv.size());
923 for(
const auto &a :
cmdline.parsed_argv)
924 new_argv.push_back(a.arg);
929 std::map<irep_idt, std::size_t> arities;
931 for(
const auto &pair : arities)
933 std::ostringstream addition;
934 addition <<
"-D" <<
id2string(pair.first) <<
"(";
935 std::vector<char> params(pair.second);
936 std::iota(params.begin(), params.end(),
'a');
937 for(std::vector<char>::iterator it=params.begin(); it!=params.end(); ++it)
940 if(it+1!=params.end())
944 new_argv.push_back(addition.str());
952 log.
debug() <<
"RUN:";
953 for(std::size_t i=0; i<new_argv.size(); i++)
954 log.
debug() <<
" " << new_argv[i];
957 return run(new_argv[0], new_argv,
cmdline.stdin_file,
"",
"");
963 bool have_files=
false;
965 for(goto_cc_cmdlinet::parsed_argvt::const_iterator
966 it=
cmdline.parsed_argv.begin();
969 if(it->is_infile_name)
976 std::list<std::string> output_files;
983 output_files.push_back(
cmdline.get_value(
'o'));
987 for(goto_cc_cmdlinet::parsed_argvt::const_iterator
988 i_it=
cmdline.parsed_argv.begin();
989 i_it!=
cmdline.parsed_argv.end();
991 if(i_it->is_infile_name &&
999 output_files.push_back(
cmdline.value_opt(
'o').value_or(
"a.out"));
1002 if(output_files.empty() ||
1003 (output_files.size()==1 &&
1004 output_files.front()==
"/dev/null"))
1012 std::list<std::string> goto_binaries;
1013 for(std::list<std::string>::const_iterator
1014 it=output_files.begin();
1015 it!=output_files.end();
1022 std::filesystem::rename(*it, bin_name);
1024 catch(
const std::filesystem::filesystem_error &e)
1030 goto_binaries.push_back(bin_name);
1037 goto_binaries.size()==1 &&
1038 output_files.size()==1)
1041 output_files.front(),
1042 goto_binaries.front(),
1048 std::string native_tool;
1057 for(std::list<std::string>::const_iterator
1058 it=output_files.begin();
1059 it!=output_files.end();
1078 const std::list<std::string> &preprocessed_source_files,
1082 bool have_files=
false;
1084 for(goto_cc_cmdlinet::parsed_argvt::const_iterator
1085 it=
cmdline.parsed_argv.begin();
1086 it!=
cmdline.parsed_argv.end();
1088 if(it->is_infile_name)
1108 std::map<std::string, std::string> output_files;
1113 for(
const auto &s : preprocessed_source_files)
1114 output_files.insert(std::make_pair(s,
cmdline.get_value(
'o')));
1118 for(
const std::string &s : preprocessed_source_files)
1119 output_files.insert(
1123 if(output_files.empty() ||
1124 (output_files.size()==1 &&
1125 output_files.begin()->second==
"/dev/null"))
1128 log.
debug() <<
"Appending preprocessed sources to generate hybrid asm output"
1131 for(
const auto &so : output_files)
1133 std::ifstream is(so.first);
1136 log.
error() <<
"Failed to open input source " << so.first
1141 std::ofstream os(so.second, std::ios::app);
1144 log.
error() <<
"Failed to open output file " << so.second
1149 const char comment=act_as_bcc ?
':' :
'#';
1155 while(std::getline(is, line))
1167 std::cout <<
"goto-cc understands the options of "
1168 <<
"gcc plus the following.\n\n";
std::string get_value(char option) const
virtual bool isset(char option) const
@ COMPILE_LINK_EXECUTABLE
std::string output_file_object
bool add_input_file(const std::string &)
puts input file names into a list and does preprocessing for libraries.
std::list< std::string > libraries
void cprover_macro_arities(std::map< irep_idt, std::size_t > &cprover_macros) const
__CPROVER_... macros written to object files and their arities
std::list< std::string > object_files
bool doit()
reads and source and object files, compiles and links them into goto program objects.
std::list< std::string > source_files
bool wrote_object_files() const
Has this compiler written any object files?
std::string object_file_extension
enum compilet::@010007010156070135133373264143331307343141370152 mode
std::list< std::string > library_paths
std::string output_file_executable
std::string native_tool_name
int preprocess(const std::string &language, const std::string &src, const std::string &dest, bool act_as_bcc)
call gcc for preprocessing
gcc_modet(goto_cc_cmdlinet &_cmdline, const std::string &_base_name, bool _produce_hybrid_binary)
static bool needs_preprocessing(const std::string &)
const std::string goto_binary_tmp_suffix
int run_gcc(const compilet &compiler)
call gcc with original command line
gcc_message_handlert gcc_message_handler
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.
const bool produce_hybrid_binary
int asm_output(bool act_as_bcc, const std::list< std::string > &preprocessed_source_files, const compilet &compiler)
int gcc_hybrid_binary(compilet &compiler)
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'.
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.
Compile and link source and object files.
bool has_prefix(const std::string &s, const std::string &prefix)
static std::string linker_name(const cmdlinet &cmdline, const std::string &base_name)
static std::string compiler_name(const cmdlinet &cmdline, const std::string &base_name)
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)
Merge linker script-defined symbols into a goto-program.
static std::string comment(const rw_set_baset::entryt &entry, bool write)
int run(const std::string &what, const std::vector< std::string > &argv)
#define PRECONDITION(CONDITION)
#define INVARIANT(CONDITION, REASON)
This macro uses the wrapper function 'invariant_violated_string'.
bool has_suffix(const std::string &s, const std::string &suffix)
const char * CBMC_VERSION