CBMC
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 <util/cmdline.h>
23#include <util/config.h>
24#include <util/get_base_name.h>
25#include <util/run.h>
26#include <util/tempdir.h>
27#include <util/version.h>
28
29#include "compile.h"
30#include "goto_cc_cmdline.h"
31#include "hybrid_binary.h"
32
33#include <filesystem>
34#include <fstream> // IWYU pragma: keep
35#include <iostream>
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
61 const std::string &_base_name,
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")) ?
114
115 if(act_as_as86)
116 {
118 log.debug() << "AS86 mode (hybrid)" << messaget::eom;
119 else
120 log.debug() << "AS86 mode" << messaget::eom;
121 }
122 else
123 {
125 log.debug() << "AS mode (hybrid)" << messaget::eom;
126 else
127 log.debug() << "AS mode" << messaget::eom;
128 }
129
130 // get configuration
132
133 // determine actions to be undertaken
135
136 if(cmdline.isset('b')) // as86 only
137 {
139 log.debug() << "Compiling and linking an executable" << messaget::eom;
140 }
141 else
142 {
144 log.debug() << "Compiling and linking a library" << messaget::eom;
145 }
146
148
149 compiler.object_file_extension="o";
150
151 if(cmdline.isset('o'))
152 {
153 compiler.output_file_object=cmdline.get_value('o');
154 compiler.output_file_executable=cmdline.get_value('o');
155 }
156 else if(cmdline.isset('b')) // as86 only
157 {
158 compiler.output_file_object=cmdline.get_value('b');
159 compiler.output_file_executable=cmdline.get_value('b');
160 }
161 else
162 {
163 compiler.output_file_object="a.out";
164 compiler.output_file_executable="a.out";
165 }
166
167 // We now iterate over any input files
168
169 temp_dirt temp_dir("goto-cc-XXXXXX");
170
171 for(goto_cc_cmdlinet::parsed_argvt::iterator
172 arg_it=cmdline.parsed_argv.begin();
174 arg_it++)
175 {
176 if(!arg_it->is_infile_name)
177 continue;
178
179 // extract the preprocessed source from the file
180 std::string infile=arg_it->arg=="-"?cmdline.stdin_file:arg_it->arg;
181 std::ifstream is(infile);
182 if(!is.is_open())
183 {
184 log.error() << "Failed to open input source " << infile << messaget::eom;
185 return 1;
186 }
187
188 // there could be multiple source files in case GCC's --combine
189 // was used
190 unsigned outputs=0;
191 std::string line;
192 std::ofstream os;
193 std::string dest;
194
195 const std::string comment2=act_as_as86 ? "::" : "##";
196
197 // search for comment2 GOTO-CC
198 // strip comment2 from all subsequent lines
199 while(std::getline(is, line))
200 {
201 if(line==comment2+" GOTO-CC")
202 {
203 if(outputs>0)
204 {
205 PRECONDITION(!dest.empty());
206 compiler.add_input_file(dest);
207 os.close();
208 }
209
210 ++outputs;
211 std::string new_name=
212 get_base_name(infile, true)+"_"+
213 std::to_string(outputs)+".i";
214 dest=temp_dir(new_name);
215
216 os.open(dest);
217 if(!os.is_open())
218 {
219 log.error() << "Failed to tmp output file " << dest << messaget::eom;
220 return 1;
221 }
222
223 continue;
224 }
225 else if(outputs==0)
226 continue;
227
228 if(line.size()>2)
229 os << line.substr(2) << '\n';
230 }
231
232 if(outputs>0)
233 {
234 PRECONDITION(!dest.empty());
235 compiler.add_input_file(dest);
236 }
237 else
238 {
239 log.warning() << "No GOTO-CC section found in " << arg_it->arg
240 << messaget::eom;
241 }
242 }
243
244 // Revert to as in case there is no source to compile
245
246 if(compiler.source_files.empty())
247 return run_as(); // exit!
248
249 // do all the rest
250 if(compiler.doit())
251 return 1; // GCC exit code for all kinds of errors
252
253 // We can generate hybrid ELF and Mach-O binaries
254 // containing both executable machine code and the goto-binary.
257
258 return EX_OK;
259}
260
263{
265
266 // build new argv
267 std::vector<std::string> new_argv;
268 new_argv.reserve(cmdline.parsed_argv.size());
269 for(const auto &a : cmdline.parsed_argv)
270 new_argv.push_back(a.arg);
271
272 // overwrite argv[0]
274
275 #if 0
276 std::cout << "RUN:";
277 for(std::size_t i=0; i<new_argv.size(); i++)
278 std::cout << " " << new_argv[i];
279 std::cout << '\n';
280 #endif
281
282 return run(new_argv[0], new_argv, cmdline.stdin_file, "", "");
283}
284
286{
287 std::string output_file="a.out";
288
289 if(cmdline.isset('o'))
290 {
292 }
293 else if(cmdline.isset('b')) // as86 only
295
296 if(output_file=="/dev/null")
297 return EX_OK;
298
300 log.debug() << "Running " << native_tool_name << " to generate hybrid binary"
301 << messaget::eom;
302
303 // save the goto-cc output file
304 std::string saved = output_file + ".goto-cc-saved";
305 try
306 {
307 std::filesystem::rename(output_file, saved);
308 }
309 catch(const std::filesystem::filesystem_error &e)
310 {
311 log.error() << "Rename failed: " << e.what() << messaget::eom;
312 return 1;
313 }
314
315 int result = run_as();
316
317 if(result == 0)
318 {
319 result = hybrid_binary(
321 saved,
325 }
326
327 return result;
328}
329
332{
333 std::cout << "goto-as understands the options of as plus the following.\n\n";
334}
configt config
Definition config.cpp:25
static std::string assembler_name(const cmdlinet &cmdline, const std::string &base_name)
Definition as_mode.cpp:37
Assembler Mode.
ait supplies three of the four components needed: an abstract interpreter (in this case handling func...
Definition ai.h:562
int run_as()
run as or as86 with original command line
Definition as_mode.cpp:262
virtual void help_mode()
display command line help
Definition as_mode.cpp:331
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:285
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:43
@ COMPILE_LINK
Definition compile.h:42
bool set(const cmdlinet &cmdline)
Definition config.cpp:863
static irep_idt this_architecture()
Definition config.cpp:1458
static irep_idt this_operating_system()
Definition config.cpp:1562
struct configt::ansi_ct ansi_c
void print_warnings_as_errors(bool yes)
With yes set to true, prefix warnings with "error:" instead of "warning:".
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:154
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:169
@ M_WARNING
Definition message.h:169
static eomt eom
Definition message.h:289
Compile and link source and object files.
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
double log(double x)
Definition math.c:2449
int run(const std::string &what, const std::vector< std::string > &argv)
Definition run.cpp:49
#define PRECONDITION(CONDITION)
Definition invariant.h:463
const char * CBMC_VERSION