17 #define EX_SOFTWARE 70
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")
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");
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",
328 base_name.find(
"goto-bcc")!=std::string::npos;
340 std::cout <<
"bcc: version " <<
gcc_version <<
" (goto-cc "
345 std::cout <<
"clang version " <<
gcc_version <<
" (goto-cc "
365 <<
"Copyright (C) 2006-2018 Daniel Kroening, Christoph Wintersteiger\n"
472 std::string target_cpu=
477 if(!target_cpu.empty())
481 for(
auto &processor : pair.second)
482 if(processor==target_cpu)
484 if(pair.first.find(
"mips")==std::string::npos)
492 if(pair.first==
"mips32o")
494 else if(pair.first==
"mips32n")
501 if(pair.first==
"mips32o")
503 else if(pair.first==
"mips32n")
531 switch(compiler.
mode)
546 log.debug() <<
"Compiling and linking a library" <<
messaget::eom;
549 log.debug() <<
"Compiling and linking an executable" <<
messaget::eom;
558 log.debug() <<
"Enabling Visual Studio syntax" <<
messaget::eom;
577 if(std_string==
"gnu89" || std_string==
"c89")
580 if(std_string==
"gnu99" || std_string==
"c99" || std_string==
"iso9899:1999" ||
581 std_string==
"gnu9x" || std_string==
"c9x" || std_string==
"iso9899:199x")
584 if(std_string==
"gnu11" || std_string==
"c11" ||
585 std_string==
"gnu1x" || std_string==
"c1x")
588 if(std_string==
"c++11" || std_string==
"c++1x" ||
589 std_string==
"gnu++11" || std_string==
"gnu++1x" ||
590 std_string==
"c++1y" ||
591 std_string==
"gnu++1y")
594 if(std_string==
"gnu++14" || std_string==
"c++14")
655 std::vector<temp_dirt> temp_dirs;
658 std::string language;
660 for(goto_cc_cmdlinet::parsed_argvt::iterator
665 if(arg_it->is_infile_name)
669 if(language==
"cpp-output" || language==
"c++-cpp-output")
674 language ==
"c" || language ==
"c++" ||
677 std::string new_suffix;
681 else if(language==
"c++")
684 new_suffix=
has_suffix(arg_it->arg,
".c")?
".i":
".ii";
686 std::string new_name=
689 temp_dirs.emplace_back(
"goto-cc-XXXXXX");
690 std::string dest = temp_dirs.back()(new_name);
693 preprocess(language, arg_it->arg, dest, act_as_bcc);
706 else if(arg_it->arg==
"-x")
711 language=arg_it->arg;
718 language=std::string(arg_it->arg, 2, std::string::npos);
729 log.error() <<
"cannot specify -o with -c with multiple files"
758 const std::string &language,
759 const std::string &src,
760 const std::string &dest,
764 std::vector<std::string> new_argv;
768 bool skip_next=
false;
770 for(goto_cc_cmdlinet::parsed_argvt::const_iterator
780 else if(it->is_infile_name)
784 else if(it->arg==
"-c" || it->arg==
"-E" || it->arg==
"-S")
788 else if(it->arg==
"-o")
797 new_argv.push_back(it->arg);
801 new_argv.push_back(
"-E");
804 std::string stdout_file;
809 new_argv.push_back(
"-o");
810 new_argv.push_back(dest);
814 if(!language.empty())
816 new_argv.push_back(
"-x");
817 new_argv.push_back(language);
821 new_argv.push_back(src);
824 INVARIANT(new_argv.size()>=1,
"No program name in argv");
828 log.debug() <<
"RUN:";
829 for(std::size_t i=0; i<new_argv.size(); i++)
830 log.debug() <<
" " << new_argv[i];
841 std::vector<std::string> new_argv;
844 new_argv.push_back(a.arg);
849 std::map<irep_idt, std::size_t> arities;
851 for(
const auto &pair : arities)
853 std::ostringstream addition;
854 addition <<
"-D" <<
id2string(pair.first) <<
"(";
855 std::vector<char> params(pair.second);
856 std::iota(params.begin(), params.end(),
'a');
857 for(std::vector<char>::iterator it=params.begin(); it!=params.end(); ++it)
860 if(it+1!=params.end())
864 new_argv.push_back(addition.str());
872 log.debug() <<
"RUN:";
873 for(std::size_t i=0; i<new_argv.size(); i++)
874 log.debug() <<
" " << new_argv[i];
883 bool have_files=
false;
885 for(goto_cc_cmdlinet::parsed_argvt::const_iterator
889 if(it->is_infile_name)
896 std::list<std::string> output_files;
907 for(goto_cc_cmdlinet::parsed_argvt::const_iterator
911 if(i_it->is_infile_name &&
922 output_files.push_back(
"a.out");
925 if(output_files.empty() ||
926 (output_files.size()==1 &&
927 output_files.front()==
"/dev/null"))
931 log.debug() <<
"Running " <<
native_tool_name <<
" to generate hybrid binary"
935 std::list<std::string> goto_binaries;
936 for(std::list<std::string>::const_iterator
937 it=output_files.begin();
938 it!=output_files.end();
953 goto_binaries.push_back(bin_name);
960 goto_binaries.size()==1 &&
961 output_files.size()==1)
964 output_files.front(),
965 goto_binaries.front(),
971 std::string native_tool;
980 for(std::list<std::string>::const_iterator
981 it=output_files.begin();
982 it!=output_files.end();
1001 const std::list<std::string> &preprocessed_source_files,
1005 bool have_files=
false;
1007 for(goto_cc_cmdlinet::parsed_argvt::const_iterator
1011 if(it->is_infile_name)
1031 std::map<std::string, std::string> output_files;
1036 for(
const auto &s : preprocessed_source_files)
1041 for(
const std::string &s : preprocessed_source_files)
1042 output_files.insert(
1046 if(output_files.empty() ||
1047 (output_files.size()==1 &&
1048 output_files.begin()->second==
"/dev/null"))
1051 log.debug() <<
"Appending preprocessed sources to generate hybrid asm output"
1054 for(
const auto &so : output_files)
1056 std::ifstream is(so.first);
1059 log.error() <<
"Failed to open input source " << so.first
1064 std::ofstream os(so.second, std::ios::app);
1067 log.error() <<
"Failed to open output file " << so.second
1072 const char comment=act_as_bcc ?
':' :
'#';
1078 while(std::getline(is, line))
1090 std::cout <<
"goto-cc understands the options of "
1091 <<
"gcc plus the following.\n\n";
unsignedbv_typet size_type()
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 =0
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)
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