cprover
Loading...
Searching...
No Matches
as_mode.cpp
Go to the documentation of this file.
1/*******************************************************************\
2
3Module: Assembler Mode
4
5Author: Michael Tautschnig
6
7\*******************************************************************/
8
11
12#include "as_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 <fstream>
23#include <iostream>
24
25#include <util/cmdline.h>
26#include <util/config.h>
27#include <util/file_util.h>
28#include <util/get_base_name.h>
29#include <util/run.h>
30#include <util/tempdir.h>
31#include <util/version.h>
32
33#include "compile.h"
34#include "goto_cc_cmdline.h"
35#include "hybrid_binary.h"
36
37static std::string assembler_name(
38 const cmdlinet &cmdline,
39 const std::string &base_name)
40{
41 if(cmdline.isset("native-assembler"))
42 return cmdline.get_value("native-assembler");
43
44 if(base_name=="as86" ||
45 base_name.find("goto-as86")!=std::string::npos)
46 return "as86";
47
48 std::string::size_type pos=base_name.find("goto-as");
49
50 if(pos==std::string::npos)
51 return "as";
52
53 std::string result=base_name;
54 result.replace(pos, 7, "as");
55
56 return result;
57}
58
60 goto_cc_cmdlinet &_cmdline,
61 const std::string &_base_name,
62 bool _produce_hybrid_binary):
63 goto_cc_modet(_cmdline, _base_name, message_handler),
64 produce_hybrid_binary(_produce_hybrid_binary),
65 native_tool_name(assembler_name(cmdline, base_name))
66{
67}
68
71{
72 if(cmdline.isset('?') ||
73 cmdline.isset("help"))
74 {
75 help();
76 return EX_OK;
77 }
78
80
81 bool act_as_as86=
82 base_name=="as86" ||
83 base_name.find("goto-as86")!=std::string::npos;
84
85 if((cmdline.isset('v') && act_as_as86) ||
86 cmdline.isset("version"))
87 {
88 if(act_as_as86)
89 {
90 log.status() << "as86 version: 0.16.17 (goto-cc " << CBMC_VERSION << ")"
92 }
93 else
94 {
95 log.status() << "GNU assembler version 2.20.51.0.7 20100318"
96 << " (goto-cc " << CBMC_VERSION << ")" << messaget::eom;
97 }
98
99 log.status()
100 << '\n'
101 << "Copyright (C) 2006-2014 Daniel Kroening, Christoph Wintersteiger\n"
102 << "CBMC version: " << CBMC_VERSION << '\n'
103 << "Architecture: " << config.this_architecture() << '\n'
105
106 return EX_OK; // Exit!
107 }
108
109 auto default_verbosity = (cmdline.isset("w-") || cmdline.isset("warn")) ?
112 cmdline.get_value("verbosity"), default_verbosity, message_handler);
113
114 if(act_as_as86)
115 {
117 log.debug() << "AS86 mode (hybrid)" << messaget::eom;
118 else
119 log.debug() << "AS86 mode" << messaget::eom;
120 }
121 else
122 {
124 log.debug() << "AS mode (hybrid)" << messaget::eom;
125 else
126 log.debug() << "AS mode" << messaget::eom;
127 }
128
129 // get configuration
131
132 // determine actions to be undertaken
133 compilet compiler(cmdline, message_handler, cmdline.isset("fatal-warnings"));
134
135 if(cmdline.isset('b')) // as86 only
136 {
138 log.debug() << "Compiling and linking an executable" << messaget::eom;
139 }
140 else
141 {
143 log.debug() << "Compiling and linking a library" << messaget::eom;
144 }
145
147
148 compiler.object_file_extension="o";
149
150 if(cmdline.isset('o'))
151 {
154 }
155 else if(cmdline.isset('b')) // as86 only
156 {
159 }
160 else
161 {
162 compiler.output_file_object="a.out";
163 compiler.output_file_executable="a.out";
164 }
165
166 // We now iterate over any input files
167
168 temp_dirt temp_dir("goto-cc-XXXXXX");
169
170 for(goto_cc_cmdlinet::parsed_argvt::iterator
171 arg_it=cmdline.parsed_argv.begin();
172 arg_it!=cmdline.parsed_argv.end();
173 arg_it++)
174 {
175 if(!arg_it->is_infile_name)
176 continue;
177
178 // extract the preprocessed source from the file
179 std::string infile=arg_it->arg=="-"?cmdline.stdin_file:arg_it->arg;
180 std::ifstream is(infile);
181 if(!is.is_open())
182 {
183 log.error() << "Failed to open input source " << infile << messaget::eom;
184 return 1;
185 }
186
187 // there could be multiple source files in case GCC's --combine
188 // was used
189 unsigned outputs=0;
190 std::string line;
191 std::ofstream os;
192 std::string dest;
193
194 const std::string comment2=act_as_as86 ? "::" : "##";
195
196 // search for comment2 GOTO-CC
197 // strip comment2 from all subsequent lines
198 while(std::getline(is, line))
199 {
200 if(line==comment2+" GOTO-CC")
201 {
202 if(outputs>0)
203 {
204 assert(!dest.empty());
205 compiler.add_input_file(dest);
206 os.close();
207 }
208
209 ++outputs;
210 std::string new_name=
211 get_base_name(infile, true)+"_"+
212 std::to_string(outputs)+".i";
213 dest=temp_dir(new_name);
214
215 os.open(dest);
216 if(!os.is_open())
217 {
218 log.error() << "Failed to tmp output file " << dest << messaget::eom;
219 return 1;
220 }
221
222 continue;
223 }
224 else if(outputs==0)
225 continue;
226
227 if(line.size()>2)
228 os << line.substr(2) << '\n';
229 }
230
231 if(outputs>0)
232 {
233 assert(!dest.empty());
234 compiler.add_input_file(dest);
235 }
236 else
237 {
238 log.warning() << "No GOTO-CC section found in " << arg_it->arg
239 << messaget::eom;
240 }
241 }
242
243 // Revert to as in case there is no source to compile
244
245 if(compiler.source_files.empty())
246 return run_as(); // exit!
247
248 // do all the rest
249 if(compiler.doit())
250 return 1; // GCC exit code for all kinds of errors
251
252 // We can generate hybrid ELF and Mach-O binaries
253 // containing both executable machine code and the goto-binary.
255 return as_hybrid_binary(compiler);
256
257 return EX_OK;
258}
259
262{
263 assert(!cmdline.parsed_argv.empty());
264
265 // build new argv
266 std::vector<std::string> new_argv;
267 new_argv.reserve(cmdline.parsed_argv.size());
268 for(const auto &a : cmdline.parsed_argv)
269 new_argv.push_back(a.arg);
270
271 // overwrite argv[0]
272 new_argv[0]=native_tool_name;
273
274 #if 0
275 std::cout << "RUN:";
276 for(std::size_t i=0; i<new_argv.size(); i++)
277 std::cout << " " << new_argv[i];
278 std::cout << '\n';
279 #endif
280
281 return run(new_argv[0], new_argv, cmdline.stdin_file, "", "");
282}
283
285{
286 std::string output_file="a.out";
287
288 if(cmdline.isset('o'))
289 {
290 output_file=cmdline.get_value('o');
291 }
292 else if(cmdline.isset('b')) // as86 only
293 output_file=cmdline.get_value('b');
294
295 if(output_file=="/dev/null")
296 return EX_OK;
297
299 log.debug() << "Running " << native_tool_name << " to generate hybrid binary"
300 << messaget::eom;
301
302 // save the goto-cc output file
303 std::string saved = output_file + ".goto-cc-saved";
304 try
305 {
306 file_rename(output_file, saved);
307 }
308 catch(const cprover_exception_baset &e)
309 {
310 log.error() << "Rename failed: " << e.what() << messaget::eom;
311 return 1;
312 }
313
314 int result = run_as();
315
316 if(result == 0)
317 {
318 result = hybrid_binary(
320 saved,
321 output_file,
324 }
325
326 return result;
327}
328
331{
332 std::cout << "goto-as understands the options of as plus the following.\n\n";
333}
static std::string assembler_name(const cmdlinet &cmdline, const std::string &base_name)
Definition as_mode.cpp:37
Assembler Mode.
int run_as()
run as or as86 with original command line
Definition as_mode.cpp:261
virtual void help_mode()
display command line help
Definition as_mode.cpp:330
virtual int doit()
does it.
Definition as_mode.cpp:70
as_modet(goto_cc_cmdlinet &_cmdline, const std::string &_base_name, bool _produce_hybrid_binary)
Definition as_mode.cpp:59
const bool produce_hybrid_binary
Definition as_mode.h:35
const std::string native_tool_name
Definition as_mode.h:36
int as_hybrid_binary(const compilet &compiler)
Definition as_mode.cpp:284
gcc_message_handlert message_handler
Definition as_mode.h:34
std::string get_value(char option) const
Definition cmdline.cpp:48
virtual bool isset(char option) const
Definition cmdline.cpp:30
@ COMPILE_LINK_EXECUTABLE
Definition compile.h:42
@ COMPILE_LINK
Definition compile.h:41
std::string output_file_object
Definition compile.h:54
bool add_input_file(const std::string &)
puts input file names into a list and does preprocessing for libraries.
Definition compile.cpp:173
bool doit()
reads and source and object files, compiles and links them into goto program objects.
Definition compile.cpp:60
std::list< std::string > source_files
Definition compile.h:46
std::string object_file_extension
Definition compile.h:50
enum compilet::@3 mode
std::string output_file_executable
Definition compile.h:51
bool set(const cmdlinet &cmdline)
Definition config.cpp:798
static irep_idt this_architecture()
Definition config.cpp:1350
static irep_idt this_operating_system()
Definition config.cpp:1450
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.
parsed_argvt parsed_argv
std::string stdin_file
goto_cc_cmdlinet & cmdline
const std::string base_name
void help()
display command line help
Class that provides messages with a built-in verbosity 'level'.
Definition message.h:155
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
@ M_ERROR
Definition message.h:170
@ M_WARNING
Definition message.h:170
static eomt eom
Definition message.h:297
Compile and link source and object files.
configt config
Definition config.cpp:25
void file_rename(const std::string &old_path, const std::string &new_path)
Rename a file.
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.
literalt pos(literalt a)
Definition literal.h:194
int run(const std::string &what, const std::vector< std::string > &argv)
Definition run.cpp:48
flavourt mode
Definition config.h:222
const char * CBMC_VERSION