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" ||
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):
100 produce_hybrid_binary(_produce_hybrid_binary),
101 goto_binary_tmp_suffix(
".goto-cc-saved"),
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",
321 base_name.find(
"goto-bcc")!=std::string::npos;
333 std::cout <<
"bcc: version " <<
gcc_version <<
" (goto-cc "
338 std::cout <<
"clang version " <<
gcc_version <<
" (goto-cc "
358 <<
"Copyright (C) 2006-2018 Daniel Kroening, Christoph Wintersteiger\n"
479 std::string target_cpu=
484 if(!target_cpu.empty())
488 for(
auto &processor : pair.second)
489 if(processor==target_cpu)
491 if(pair.first.find(
"mips")==std::string::npos)
499 if(pair.first==
"mips32o")
501 else if(pair.first==
"mips32n")
508 if(pair.first==
"mips32o")
510 else if(pair.first==
"mips32n")
523 static const std::map<std::string, std::string> target_map = {
524 {
"aarch64",
"arm64" },
525 {
"aarch64_32",
"arm" },
526 {
"aarch64_be",
"none" },
530 {
"arm64_32",
"arm" },
536 {
"hexagon",
"none" },
540 {
"mips64",
"mips64" },
541 {
"mips64el",
"mips64el" },
542 {
"mipsel",
"mipsel" },
545 {
"nvptx64",
"none" },
546 {
"ppc32",
"powerpc" },
548 {
"ppc64le",
"ppc64le" },
550 {
"riscv32",
"none" },
551 {
"riscv64",
"riscv64" },
553 {
"sparcel",
"none" },
554 {
"sparcv9",
"sparc64" },
555 {
"systemz",
"none" },
557 {
"thumbeb",
"none" },
561 {
"x86_64",
"x86_64" },
566 target_map.find(arch_quadruple.substr(0, arch_quadruple.find(
'-')));
567 if(it == target_map.end())
592 switch(compiler.
mode)
607 log.debug() <<
"Compiling and linking a library" <<
messaget::eom;
610 log.debug() <<
"Compiling and linking an executable" <<
messaget::eom;
619 log.debug() <<
"Enabling Visual Studio syntax" <<
messaget::eom;
638 if(std_string==
"gnu89" || std_string==
"c89")
641 if(std_string==
"gnu99" || std_string==
"c99" || std_string==
"iso9899:1999" ||
642 std_string==
"gnu9x" || std_string==
"c9x" || std_string==
"iso9899:199x")
645 if(std_string==
"gnu11" || std_string==
"c11" ||
646 std_string==
"gnu1x" || std_string==
"c1x")
649 if(std_string==
"c++11" || std_string==
"c++1x" ||
650 std_string==
"gnu++11" || std_string==
"gnu++1x" ||
651 std_string==
"c++1y" ||
652 std_string==
"gnu++1y")
655 if(std_string==
"gnu++14" || std_string==
"c++14")
658 if(std_string ==
"gnu++17" || std_string ==
"c++17")
719 std::vector<temp_dirt> temp_dirs;
722 std::string language;
724 for(goto_cc_cmdlinet::parsed_argvt::iterator
729 if(arg_it->is_infile_name)
733 if(language==
"cpp-output" || language==
"c++-cpp-output")
738 language ==
"c" || language ==
"c++" ||
741 std::string new_suffix;
745 else if(language==
"c++")
748 new_suffix=
has_suffix(arg_it->arg,
".c")?
".i":
".ii";
750 std::string new_name=
753 temp_dirs.emplace_back(
"goto-cc-XXXXXX");
754 std::string dest = temp_dirs.back()(new_name);
757 preprocess(language, arg_it->arg, dest, act_as_bcc);
770 else if(arg_it->arg==
"-x")
775 language=arg_it->arg;
782 language=std::string(arg_it->arg, 2, std::string::npos);
793 log.error() <<
"cannot specify -o with -c with multiple files"
822 const std::string &language,
823 const std::string &src,
824 const std::string &dest,
828 std::vector<std::string> new_argv;
832 bool skip_next=
false;
834 for(goto_cc_cmdlinet::parsed_argvt::const_iterator
844 else if(it->is_infile_name)
848 else if(it->arg==
"-c" || it->arg==
"-E" || it->arg==
"-S")
852 else if(it->arg==
"-o")
861 new_argv.push_back(it->arg);
865 new_argv.push_back(
"-E");
868 std::string stdout_file;
873 new_argv.push_back(
"-o");
874 new_argv.push_back(dest);
878 if(!language.empty())
880 new_argv.push_back(
"-x");
881 new_argv.push_back(language);
885 new_argv.push_back(src);
888 INVARIANT(new_argv.size()>=1,
"No program name in argv");
892 log.debug() <<
"RUN:";
893 for(std::size_t i=0; i<new_argv.size(); i++)
894 log.debug() <<
" " << new_argv[i];
905 std::vector<std::string> new_argv;
908 new_argv.push_back(a.arg);
913 std::map<irep_idt, std::size_t> arities;
915 for(
const auto &pair : arities)
917 std::ostringstream addition;
918 addition <<
"-D" <<
id2string(pair.first) <<
"(";
919 std::vector<char> params(pair.second);
920 std::iota(params.begin(), params.end(),
'a');
921 for(std::vector<char>::iterator it=params.begin(); it!=params.end(); ++it)
924 if(it+1!=params.end())
928 new_argv.push_back(addition.str());
936 log.debug() <<
"RUN:";
937 for(std::size_t i=0; i<new_argv.size(); i++)
938 log.debug() <<
" " << new_argv[i];
947 bool have_files=
false;
949 for(goto_cc_cmdlinet::parsed_argvt::const_iterator
953 if(it->is_infile_name)
960 std::list<std::string> output_files;
971 for(goto_cc_cmdlinet::parsed_argvt::const_iterator
975 if(i_it->is_infile_name &&
986 output_files.push_back(
"a.out");
989 if(output_files.empty() ||
990 (output_files.size()==1 &&
991 output_files.front()==
"/dev/null"))
995 log.debug() <<
"Running " <<
native_tool_name <<
" to generate hybrid binary"
999 std::list<std::string> goto_binaries;
1000 for(std::list<std::string>::const_iterator
1001 it=output_files.begin();
1002 it!=output_files.end();
1017 goto_binaries.push_back(bin_name);
1024 goto_binaries.size()==1 &&
1025 output_files.size()==1)
1028 output_files.front(),
1029 goto_binaries.front(),
1035 std::string native_tool;
1044 for(std::list<std::string>::const_iterator
1045 it=output_files.begin();
1046 it!=output_files.end();
1065 const std::list<std::string> &preprocessed_source_files,
1069 bool have_files=
false;
1071 for(goto_cc_cmdlinet::parsed_argvt::const_iterator
1075 if(it->is_infile_name)
1095 std::map<std::string, std::string> output_files;
1100 for(
const auto &s : preprocessed_source_files)
1105 for(
const std::string &s : preprocessed_source_files)
1106 output_files.insert(
1110 if(output_files.empty() ||
1111 (output_files.size()==1 &&
1112 output_files.begin()->second==
"/dev/null"))
1115 log.debug() <<
"Appending preprocessed sources to generate hybrid asm output"
1118 for(
const auto &so : output_files)
1120 std::ifstream is(so.first);
1123 log.error() <<
"Failed to open input source " << so.first
1128 std::ofstream os(so.second, std::ios::app);
1131 log.error() <<
"Failed to open output file " << so.second
1136 const char comment=act_as_bcc ?
':' :
'#';
1142 while(std::getline(is, line))
1154 std::cout <<
"goto-cc understands the options of "
1155 <<
"gcc plus the following.\n\n";
std::string get_value(char option) const
virtual bool isset(char option) const
const std::list< std::string > & get_values(const std::string &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
std::list< std::string > library_paths
std::string output_file_executable
void set_arch(const irep_idt &)
bool set(const cmdlinet &cmdline)
static irep_idt this_architecture()
static irep_idt this_operating_system()
struct configt::ansi_ct ansi_c
Base class for exceptions thrown in the cprover project.
virtual std::string what() const
A human readable description of what went wrong.
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)
void get(const std::string &executable)
configt::cppt::cpp_standardt default_cxx_standard
configt::ansi_ct::c_standardt default_c_standard
enum gcc_versiont::flavort flavor
bool have_infile_arg() const
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)
void file_rename(const std::string &old_path, const std::string &new_path)
Rename a file.
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'.
enum configt::ansi_ct::c_standardt c_standard
std::list< std::string > undefines
std::list< std::string > preprocessor_options
bool single_precision_constant
void set_arch_spec_arm(const irep_idt &subarch)
std::size_t wchar_t_width
void set_arch_spec_x86_64()
void set_arch_spec_i386()
std::size_t short_int_width
enum configt::cppt::cpp_standardt cpp_standard
bool has_suffix(const std::string &s, const std::string &suffix)
const char * CBMC_VERSION