17 #define EX_SOFTWARE 70 41 const std::string &base_name)
43 if(cmdline.
isset(
"native-compiler"))
44 return cmdline.
get_value(
"native-compiler");
46 if(base_name==
"bcc" ||
47 base_name.find(
"goto-bcc")!=std::string::npos)
52 if(pos==std::string::npos ||
53 base_name==
"goto-gcc" ||
63 std::string result=base_name;
64 result.replace(pos, 8,
"gcc");
71 const std::string &base_name)
73 if(cmdline.
isset(
"native-linker"))
74 return cmdline.
get_value(
"native-linker");
78 if(pos==std::string::npos ||
79 base_name==
"goto-gcc" ||
83 std::string result=base_name;
84 result.replace(pos, 7,
"ld");
91 const std::string &_base_name,
92 bool _produce_hybrid_binary):
94 produce_hybrid_binary(_produce_hybrid_binary),
95 act_as_ld(base_name==
"ld" ||
96 base_name.find(
"goto-ld")!=
std::string::npos),
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" 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",
140 "cortex-a57",
"cortex-a72",
"exynos-m1" 142 {
"hppa", {
"1.0",
"1.1",
"2.0"}},
147 "powerpc",
"601",
"602",
"603",
"603e",
"604",
"604e",
"630",
151 "G4",
"7400",
"7450",
153 "401",
"403",
"405",
"405fp",
"440",
"440fp",
"464",
"464fp",
157 "e300c2",
"e300c3",
"e500mc",
"ec603e",
170 "power3",
"power4",
"power5",
"power5+",
"power6",
"power6x",
174 "e500mc64",
"e5500",
"e6500",
179 {
"powerpc64le", {
"powerpc64le",
"power8"}},
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",
208 "mips32",
"mips32r2",
"mips32r3",
"mips32r5",
"mips32r6",
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",
219 "mips1",
"mips2",
"r2000",
"r3000",
223 "mips3",
"mips4",
"r4000",
"r4400",
"r4600",
"r4650",
"r4700",
224 "r8000",
"rm7000",
"rm9000",
"r10000",
"r12000",
"r14000",
235 "z900",
"z990",
"g5",
"g6",
238 "z9-109",
"z9-ec",
"z10",
"z196",
"zEC12",
"z13" 246 "v7",
"v8",
"leon",
"leon3",
"leon3v7",
"cypress",
"supersparc",
247 "hypersparc",
"sparclite",
"f930",
"f934",
"sparclite86x",
251 "v9",
"ultrasparc",
"ultrasparc3",
"niagara",
"niagara2",
252 "niagara3",
"niagara4",
255 "itanium",
"itanium1",
"merced",
"itanium2",
"mckinley" 262 "i386",
"i486",
"i586",
"i686",
264 "k6",
"k6-2",
"k6-3",
"athlon" "athlon-tbird",
"athlon-4",
265 "athlon-xp",
"athlon-mp",
268 "pentium",
"pentium-mmx",
"pentiumpro" "pentium2",
"pentium3",
269 "pentium3m",
"pentium-m" "pentium4",
"pentium4m",
"prescott",
271 "winchip-c6",
"winchip2",
"c3",
"c3-2",
"geode",
275 "nocona",
"core2",
"nehalem" "westmere",
"sandybridge",
"knl",
276 "ivybridge",
"haswell",
"broadwell" "bonnell",
"silvermont",
278 "k8",
"k8-sse3",
"opteron",
"athlon64",
"athlon-fx",
279 "opteron-sse3" "athlon64-sse3",
"amdfam10",
"barcelona",
281 "bdver1",
"bdver2" "bdver3",
"bdver4",
318 unsigned int verbosity=1;
322 base_name.find(
"goto-bcc")!=std::string::npos;
331 std::cout <<
"GNU ld version 2.16.91 20050610 (goto-cc " CBMC_VERSION 334 std::cout <<
"bcc: version 0.16.17 (goto-cc " CBMC_VERSION
")\n";
336 std::cout <<
"gcc version 3.4.4 (goto-cc " CBMC_VERSION
")\n";
345 "Copyright (C) 2006-2014 Daniel Kroening, Christoph Wintersteiger\n" <<
358 std::cout <<
"3.4.4\n";
373 debug() <<
"LD mode (hybrid)" <<
eom;
380 debug() <<
"BCC mode (hybrid)" <<
eom;
387 debug() <<
"GCC mode (hybrid)" <<
eom;
435 std::string target_cpu=
444 for(
auto &processor : pair.second)
445 if(processor==target_cpu)
447 if(pair.first.find(
"mips")==std::string::npos)
455 if(pair.first==
"mips32o")
457 else if(pair.first==
"mips32n")
464 if(pair.first==
"mips32o")
466 else if(pair.first==
"mips32n")
515 switch(compiler.mode)
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;
536 debug() <<
"Enabling Visual Studio syntax" <<
eom;
544 compiler.object_file_extension=
"s";
546 compiler.object_file_extension=
"o";
552 if(std_string==
"gnu89" || std_string==
"c89")
555 if(std_string==
"gnu99" || std_string==
"c99" || std_string==
"iso9899:1999" ||
556 std_string==
"gnu9x" || std_string==
"c9x" || std_string==
"iso9899:199x")
559 if(std_string==
"gnu11" || std_string==
"c11" ||
560 std_string==
"gnu1x" || std_string==
"c1x")
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")
569 if(std_string==
"gnu++14" || std_string==
"c++14")
605 compiler.libraries.push_back(
"c");
608 compiler.libraries.push_back(
"pthread");
619 compiler.output_file_object=
"";
620 compiler.output_file_executable=
"a.out";
628 std::string language;
630 for(goto_cc_cmdlinet::parsed_argvt::iterator
635 if(arg_it->is_infile_name)
639 if(language==
"cpp-output" || language==
"c++-cpp-output")
641 compiler.add_input_file(arg_it->arg);
643 else if(language==
"c" || language==
"c++" ||
646 std::string new_suffix;
650 else if(language==
"c++")
653 new_suffix=
has_suffix(arg_it->arg,
".c")?
".i":
".ii";
655 std::string new_name=
657 std::string dest=temp_dir(new_name);
660 preprocess(language, arg_it->arg, dest, act_as_bcc);
664 error() <<
"preprocessing has failed" <<
eom;
668 compiler.add_input_file(dest);
671 compiler.add_input_file(arg_it->arg);
673 else if(arg_it->arg==
"-x")
678 language=arg_it->arg;
685 language=std::string(arg_it->arg, 2, std::string::npos);
695 if(compiler.source_files.empty() &&
696 compiler.object_files.empty())
700 return asm_output(act_as_bcc, compiler.source_files);
716 const std::string &language,
717 const std::string &src,
718 const std::string &dest,
722 std::vector<std::string> new_argv;
726 bool skip_next=
false;
728 for(goto_cc_cmdlinet::parsed_argvt::const_iterator
738 else if(it->is_infile_name)
742 else if(it->arg==
"-c" || it->arg==
"-E" || it->arg==
"-S")
746 else if(it->arg==
"-o")
755 new_argv.push_back(it->arg);
759 new_argv.push_back(
"-E");
762 std::string stdout_file;
767 new_argv.push_back(
"-o");
768 new_argv.push_back(dest);
774 new_argv.push_back(
"-x");
775 new_argv.push_back(language);
779 new_argv.push_back(src);
782 INVARIANT(new_argv.size()>=1,
"No program name in argv");
786 for(std::size_t i=0; i<new_argv.size(); i++)
787 debug() <<
" " << new_argv[i];
799 std::vector<std::string> new_argv;
802 new_argv.push_back(a.arg);
808 for(std::size_t i=0; i<new_argv.size(); i++)
809 debug() <<
" " << new_argv[i];
818 bool have_files=
false;
820 for(goto_cc_cmdlinet::parsed_argvt::const_iterator
824 if(it->is_infile_name)
831 std::list<std::string> output_files;
842 for(goto_cc_cmdlinet::parsed_argvt::const_iterator
846 if(i_it->is_infile_name &&
857 output_files.push_back(
"a.out");
860 if(output_files.empty() ||
861 (output_files.size()==1 &&
862 output_files.front()==
"/dev/null"))
866 <<
" to generate hybrid binary" <<
eom;
869 for(std::list<std::string>::const_iterator
870 it=output_files.begin();
871 it!=output_files.end();
874 rename(it->c_str(), (*it+
".goto-cc-saved").c_str());
877 std::string objcopy_cmd;
881 objcopy_cmd.erase(objcopy_cmd.size()-2);
886 objcopy_cmd.erase(objcopy_cmd.size()-3);
888 objcopy_cmd+=
"objcopy";
894 for(std::list<std::string>::const_iterator
895 it=output_files.begin();
896 it!=output_files.end();
899 debug() <<
"merging " << *it <<
eom;
900 std::string saved=*it+
".goto-cc-saved";
906 std::vector<std::string> objcopy_argv;
908 objcopy_argv.push_back(objcopy_cmd);
909 objcopy_argv.push_back(
"--remove-section=goto-cc");
910 objcopy_argv.push_back(*it);
912 result=
run(objcopy_argv[0], objcopy_argv,
"",
"");
918 std::vector<std::string> objcopy_argv;
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);
925 result=
run(objcopy_argv[0], objcopy_argv,
"",
"");
928 remove(saved.c_str());
929 #elif defined(__APPLE__) 933 std::vector<std::string> lipo_argv;
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);
945 result=
run(lipo_argv[0], lipo_argv,
"",
"");
948 remove(saved.c_str());
951 error() <<
"binary merging not implemented for this platform" <<
eom;
961 const std::list<std::string> &preprocessed_source_files)
964 bool have_files=
false;
966 for(goto_cc_cmdlinet::parsed_argvt::const_iterator
970 if(it->is_infile_name)
980 <<
" to generate native asm output" <<
eom;
988 std::map<std::string, std::string> output_files;
993 for(
const auto &s : preprocessed_source_files)
998 for(
const std::string &s : preprocessed_source_files)
1003 if(output_files.empty() ||
1004 (output_files.size()==1 &&
1005 output_files.begin()->second==
"/dev/null"))
1009 <<
"Appending preprocessed sources to generate hybrid asm output" 1012 for(
const auto &so : output_files)
1014 std::ifstream is(so.first);
1017 error() <<
"Failed to open input source " << so.first <<
eom;
1021 std::ofstream os(so.second, std::ios::app);
1024 error() <<
"Failed to open output file " << so.second <<
eom;
1028 const char comment=act_as_bcc ?
':' :
'#';
1030 os << comment << comment <<
" GOTO-CC" <<
'\n';
1034 while(std::getline(is, line))
1036 os << comment << comment << line <<
'\n';
1047 std::cout <<
"goto-ld understands the options of " 1048 <<
"ld plus the following.\n\n";
1050 std::cout <<
"goto-cc understands the options of " 1051 <<
"gcc plus the following.\n\n";
void set_arch_spec_arm(const irep_idt &subarch)
const bool produce_hybrid_binary
const std::list< std::string > & get_values(const std::string &option) const
struct configt::ansi_ct ansi_c
std::string comment(const rw_set_baset::entryt &entry, bool write)
unsigned unsafe_string2unsigned(const std::string &str, int base)
bool single_precision_constant
std::string get_value(char option) const
Base class for command line interpretation.
unsignedbv_typet size_type()
std::list< std::string > undefines
static mstreamt & eom(mstreamt &m)
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
#define INVARIANT(CONDITION, REASON)
static std::string linker_name(const cmdlinet &cmdline, const std::string &base_name)
int preprocess(const std::string &language, const std::string &src, const std::string &dest, bool act_as_bcc)
call gcc for preprocessing
bool set(const cmdlinet &cmdline)
bool rename(exprt &expr, const irep_idt &old_name, const irep_idt &new_name)
automated variable renaming
int run_gcc()
run gcc or clang with original command line
virtual bool isset(char option) const
void set_arch_spec_x86_64()
gcc_modet(goto_cc_cmdlinet &_cmdline, const std::string &_base_name, bool _produce_hybrid_binary)
void set_arch(const irep_idt &)
goto_cc_cmdlinet & cmdline
#define PRECONDITION(CONDITION)
bool has_prefix(const std::string &s, const std::string &prefix)
void help_mode() final
display command line help
static bool needs_preprocessing(const std::string &)
Compile and link source and object files.
static irep_idt this_operating_system()
std::string native_tool_name
virtual void help()
display command line help
void set_arch_spec_i386()
bool have_infile_arg() const
void set_verbosity(unsigned _verbosity)
const std::map< std::string, std::set< std::string > > arch_map
static std::string compiler_name(const cmdlinet &cmdline, const std::string &base_name)
bool has_suffix(const std::string &s, const std::string &suffix)
std::list< std::string > preprocessor_options
int asm_output(bool act_as_bcc, const std::list< std::string > &preprocessed_source_files)
const std::string base_name
static irep_idt this_architecture()
int run(const std::string &what, const std::vector< std::string > &argv, const std::string &std_input, const std::string &std_output)