cprover
Loading...
Searching...
No Matches
remove_asm.cpp
Go to the documentation of this file.
1/*******************************************************************\
2
3Module: Remove 'asm' statements by compiling them into suitable
4 standard goto program instructions
5
6Author: Daniel Kroening
7
8Date: December 2014
9
10\*******************************************************************/
11
15
16#include "remove_asm.h"
17
18#include <util/c_types.h>
19#include <util/pointer_expr.h>
20#include <util/prefix.h>
21#include <util/range.h>
22#include <util/std_code.h>
24
27
28#include "assembler_parser.h"
29
31{
32public:
37
39 {
40 for(auto &f : goto_functions.function_map)
41 process_function(f.first, f.second);
42 }
43
44protected:
47
49
51 const irep_idt &function_id,
52 goto_programt::instructiont &instruction,
53 goto_programt &dest);
54
56
58 const irep_idt &,
59 const code_asmt &,
60 goto_programt &dest);
61
64 const code_asm_gcct &code,
65 goto_programt &dest);
66
69 const exprt::operandst &operands,
70 const code_asmt &code,
71 goto_programt &dest);
72};
73
83 const code_asm_gcct &code,
84 goto_programt &dest)
85{
86 irep_idt function_identifier = function_base_name;
87
89
91
92 // outputs
93 forall_operands(it, code.outputs())
94 {
95 if(it->operands().size() == 2)
96 {
97 arguments.push_back(typecast_exprt(
99 }
100 }
101
102 // inputs
103 forall_operands(it, code.inputs())
104 {
105 if(it->operands().size() == 2)
106 {
107 arguments.push_back(typecast_exprt(
109 }
110 }
111
114 arguments.size(), code_typet::parametert{void_pointer}},
115 empty_typet()};
116
117 symbol_exprt fkt(function_identifier, fkt_type);
118
119 code_function_callt function_call(std::move(fkt), std::move(arguments));
120
121 dest.add(
123
124 // do we have it?
125 if(!symbol_table.has_symbol(function_identifier))
126 {
127 symbolt symbol{function_identifier, fkt_type, ID_C};
128 symbol.base_name = function_base_name;
129
130 symbol_table.add(symbol);
131
132 goto_functions.function_map.emplace(function_identifier, goto_functiont());
133 }
134 else
135 {
137 symbol_table.lookup_ref(function_identifier).type == fkt_type,
138 "function types should match");
139 }
140}
141
152 const exprt::operandst &operands,
153 const code_asmt &code,
154 goto_programt &dest)
155{
156 irep_idt function_identifier = function_base_name;
157
159
161
162 for(const auto &op : operands)
163 arguments.push_back(typecast_exprt::conditional_cast(op, void_pointer));
164
167 arguments.size(), code_typet::parametert{void_pointer}},
168 empty_typet()};
169
170 symbol_exprt fkt(function_identifier, fkt_type);
171
172 code_function_callt function_call(std::move(fkt), std::move(arguments));
173
174 dest.add(
176
177 // do we have it?
178 if(!symbol_table.has_symbol(function_identifier))
179 {
180 symbolt symbol{function_identifier, fkt_type, ID_C};
181 symbol.base_name = function_base_name;
182
183 symbol_table.add(symbol);
184
185 goto_functions.function_map.emplace(function_identifier, goto_functiont());
186 }
187 else
188 {
190 symbol_table.lookup_ref(function_identifier).type == fkt_type,
191 "function types should match");
192 }
193}
194
203 const irep_idt &function_id,
204 goto_programt::instructiont &instruction,
205 goto_programt &dest)
206{
207 const code_asmt &code = to_code_asm(instruction.get_other());
208
209 const irep_idt &flavor = code.get_flavor();
210
211 if(flavor == ID_gcc)
213 else if(flavor == ID_msc)
214 process_instruction_msc(function_id, code, dest);
215 else
216 DATA_INVARIANT(false, "unexpected assembler flavor");
217}
218
225 const code_asm_gcct &code,
226 goto_programt &dest)
227{
228 const irep_idt &i_str = to_string_constant(code.asm_text()).get_value();
229
230 std::istringstream str(id2string(i_str));
232 assembler_parser.in = &str;
234
236 bool unknown = false;
237 bool x86_32_locked_atomic = false;
238
239 for(const auto &instruction : assembler_parser.instructions)
240 {
241 if(instruction.empty())
242 continue;
243
244#if 0
245 std::cout << "A ********************\n";
246 for(const auto &ins : instruction)
247 {
248 std::cout << "XX: " << ins.pretty() << '\n';
249 }
250
251 std::cout << "B ********************\n";
252#endif
253
254 // deal with prefixes
255 irep_idt command;
256 unsigned pos = 0;
257
258 if(
259 instruction.front().id() == ID_symbol &&
260 instruction.front().get(ID_identifier) == "lock")
261 {
263 pos++;
264 }
265
266 // done?
267 if(pos == instruction.size())
268 continue;
269
270 if(instruction[pos].id() == ID_symbol)
271 {
272 command = instruction[pos].get(ID_identifier);
273 pos++;
274 }
275
276 if(command == "xchg" || command == "xchgl")
278
280 {
282
284 code_fence.add_source_location() = code.source_location();
285 code_fence.set(ID_WWfence, true);
286 code_fence.set(ID_RRfence, true);
287 code_fence.set(ID_RWfence, true);
288 code_fence.set(ID_WRfence, true);
289
290 tmp_dest.add(
292 }
293
294 if(command == "fstcw" || command == "fnstcw" || command == "fldcw") // x86
295 {
296 gcc_asm_function_call("__asm_" + id2string(command), code, tmp_dest);
297 }
298 else if(
299 command == "mfence" || command == "lfence" || command == "sfence") // x86
300 {
301 gcc_asm_function_call("__asm_" + id2string(command), code, tmp_dest);
302 }
303 else if(command == ID_sync) // Power
304 {
306 code_fence.add_source_location() = code.source_location();
307 code_fence.set(ID_WWfence, true);
308 code_fence.set(ID_RRfence, true);
309 code_fence.set(ID_RWfence, true);
310 code_fence.set(ID_WRfence, true);
311 code_fence.set(ID_WWcumul, true);
312 code_fence.set(ID_RWcumul, true);
313 code_fence.set(ID_RRcumul, true);
314 code_fence.set(ID_WRcumul, true);
315
316 tmp_dest.add(
318 }
319 else if(command == ID_lwsync) // Power
320 {
322 code_fence.add_source_location() = code.source_location();
323 code_fence.set(ID_WWfence, true);
324 code_fence.set(ID_RRfence, true);
325 code_fence.set(ID_RWfence, true);
326 code_fence.set(ID_WWcumul, true);
327 code_fence.set(ID_RWcumul, true);
328 code_fence.set(ID_RRcumul, true);
329
330 tmp_dest.add(
332 }
333 else if(command == ID_isync) // Power
334 {
336 code_fence.add_source_location() = code.source_location();
337
338 tmp_dest.add(
340 // doesn't do anything by itself,
341 // needs to be combined with branch
342 }
343 else if(command == "dmb" || command == "dsb") // ARM
344 {
346 code_fence.add_source_location() = code.source_location();
347 code_fence.set(ID_WWfence, true);
348 code_fence.set(ID_RRfence, true);
349 code_fence.set(ID_RWfence, true);
350 code_fence.set(ID_WRfence, true);
351 code_fence.set(ID_WWcumul, true);
352 code_fence.set(ID_RWcumul, true);
353 code_fence.set(ID_RRcumul, true);
354 code_fence.set(ID_WRcumul, true);
355
356 tmp_dest.add(
358 }
359 else if(command == "isb") // ARM
360 {
362 code_fence.add_source_location() = code.source_location();
363
364 tmp_dest.add(
366 // doesn't do anything by itself,
367 // needs to be combined with branch
368 }
369 else
370 unknown = true; // give up
371
373 {
375
376 x86_32_locked_atomic = false;
377 }
378 }
379
380 if(unknown)
381 {
382 // we give up; we should perhaps print a warning
383 }
384 else
386}
387
395 const irep_idt &function_id,
396 const code_asmt &code,
397 goto_programt &dest)
398{
399 const irep_idt &i_str = to_string_constant(code.op0()).get_value();
400
401 std::istringstream str(id2string(i_str));
403 assembler_parser.in = &str;
405
407 bool unknown = false;
408 bool x86_32_locked_atomic = false;
409
410 for(const auto &instruction : assembler_parser.instructions)
411 {
412 if(instruction.empty())
413 continue;
414
415#if 0
416 std::cout << "A ********************\n";
417 for(const auto &ins : instruction)
418 {
419 std::cout << "XX: " << ins.pretty() << '\n';
420 }
421
422 std::cout << "B ********************\n";
423#endif
424
425 // deal with prefixes
426 irep_idt command;
427 unsigned pos = 0;
428
429 if(
430 instruction.front().id() == ID_symbol &&
431 instruction.front().get(ID_identifier) == "lock")
432 {
434 pos++;
435 }
436
437 // done?
438 if(pos == instruction.size())
439 continue;
440
441 if(instruction[pos].id() == ID_symbol)
442 {
443 command = instruction[pos].get(ID_identifier);
444 pos++;
445 }
446
447 if(command == "xchg" || command == "xchgl")
449
451 {
453
455 code_fence.add_source_location() = code.source_location();
456 code_fence.set(ID_WWfence, true);
457 code_fence.set(ID_RRfence, true);
458 code_fence.set(ID_RWfence, true);
459 code_fence.set(ID_WRfence, true);
460
461 tmp_dest.add(
463 }
464
465 if(command == "fstcw" || command == "fnstcw" || command == "fldcw") // x86
466 {
468 // try to typecheck the argument
469 if(pos != instruction.size() && instruction[pos].id() == ID_symbol)
470 {
471 const irep_idt &name = instruction[pos].get(ID_identifier);
472 for(const auto &entry : equal_range(symbol_table.symbol_base_map, name))
473 {
474 // global scope symbol, don't replace a local one
475 if(entry.second == name && args[0].id() != ID_address_of)
476 {
477 args[0] =
478 address_of_exprt{symbol_table.lookup_ref(name).symbol_expr()};
479 }
480 // parameter or symbol in local scope
481 else if(has_prefix(
482 id2string(entry.second), id2string(function_id) + "::"))
483 {
484 args[0] = address_of_exprt{
485 symbol_table.lookup_ref(entry.second).symbol_expr()};
486 }
487 }
488 }
490 "__asm_" + id2string(command), args, code, tmp_dest);
491 }
492 else if(
493 command == "mfence" || command == "lfence" || command == "sfence") // x86
494 {
495 msc_asm_function_call("__asm_" + id2string(command), {}, code, tmp_dest);
496 }
497 else
498 unknown = true; // give up
499
501 {
503
504 x86_32_locked_atomic = false;
505 }
506 }
507
508 if(unknown)
509 {
510 // we give up; we should perhaps print a warning
511 }
512 else
514}
515
522 const irep_idt &function_id,
523 goto_functionst::goto_functiont &goto_function)
524{
525 bool did_something = false;
526
527 Forall_goto_program_instructions(it, goto_function.body)
528 {
529 if(it->is_other() && it->get_other().get_statement() == ID_asm)
530 {
532 process_instruction(function_id, *it, tmp_dest);
533 it->turn_into_skip();
534 did_something = true;
535
536 goto_programt::targett next = it;
537 next++;
538
539 goto_function.body.destructive_insert(next, tmp_dest);
540 }
541 }
542
543 if(did_something)
544 remove_skip(goto_function.body);
545}
546
551void remove_asm(goto_functionst &goto_functions, symbol_tablet &symbol_table)
552{
553 remove_asmt rem(symbol_table, goto_functions);
554 rem();
555}
556
564void remove_asm(goto_modelt &goto_model)
565{
566 remove_asm(goto_model.goto_functions, goto_model.symbol_table);
567}
assembler_parsert assembler_parser
pointer_typet pointer_type(const typet &subtype)
Definition c_types.cpp:240
Operator to return the address of an object.
ait supplies three of the four components needed: an abstract interpreter (in this case handling func...
Definition ai.h:563
virtual bool parse()
std::list< instructiont > instructions
virtual void clear()
codet representation of an inline assembler statement, for the gcc flavor.
Definition std_code.h:1297
exprt & asm_text()
Definition std_code.h:1305
exprt & outputs()
Definition std_code.h:1315
exprt & inputs()
Definition std_code.h:1325
codet representation of an inline assembler statement.
Definition std_code.h:1253
const irep_idt & get_flavor() const
Definition std_code.h:1263
goto_instruction_codet representation of a function call statement.
Base type of functions.
Definition std_types.h:539
std::vector< parametert > parameterst
Definition std_types.h:542
Data structure for representing an arbitrary statement in a program.
exprt & op0()
Definition expr.h:125
dstringt has one field, an unsigned integer no which is an index into a static table of strings.
Definition dstring.h:39
The empty type.
Definition std_types.h:51
std::vector< exprt > operandst
Definition expr.h:58
const source_locationt & source_location() const
Definition expr.h:223
A collection of goto functions.
function_mapt function_map
::goto_functiont goto_functiont
A goto function, consisting of function body (see body) and parameter identifiers (see parameter_iden...
symbol_tablet symbol_table
Symbol table.
Definition goto_model.h:31
goto_functionst goto_functions
GOTO functions.
Definition goto_model.h:34
This class represents an instruction in the GOTO intermediate representation.
const goto_instruction_codet & get_other() const
Get the statement for OTHER.
A generic container class for the GOTO intermediate representation of one function.
instructionst::iterator targett
void destructive_append(goto_programt &p)
Appends the given program p to *this. p is destroyed.
static instructiont make_atomic_end(const source_locationt &l=source_locationt::nil())
static instructiont make_function_call(const code_function_callt &_code, const source_locationt &l=source_locationt::nil())
Create a function call instruction.
static instructiont make_other(const goto_instruction_codet &_code, const source_locationt &l=source_locationt::nil())
static instructiont make_atomic_begin(const source_locationt &l=source_locationt::nil())
targett add(instructiont &&instruction)
Adds a given instruction at the end.
The null pointer constant.
std::istream * in
Definition parser.h:26
goto_functionst & goto_functions
symbol_tablet & symbol_table
void process_function(const irep_idt &, goto_functionst::goto_functiont &)
Replaces inline assembly instructions in the goto function by non-assembly goto program instructions.
void operator()()
void process_instruction_msc(const irep_idt &, const code_asmt &, goto_programt &dest)
Translates the given inline assembly code (in msc style) to non-assembly goto program instructions.
void msc_asm_function_call(const irep_idt &function_base_name, const exprt::operandst &operands, const code_asmt &code, goto_programt &dest)
Adds a call to a library function that implements the given msc-style inline assembly statement.
remove_asmt(symbol_tablet &_symbol_table, goto_functionst &_goto_functions)
void process_instruction_gcc(const code_asm_gcct &, goto_programt &dest)
Translates the given inline assembly code (in gcc style) to non-assembly goto program instructions.
void gcc_asm_function_call(const irep_idt &function_base_name, const code_asm_gcct &code, goto_programt &dest)
Adds a call to a library function that implements the given gcc-style inline assembly statement.
void process_instruction(const irep_idt &function_id, goto_programt::instructiont &instruction, goto_programt &dest)
Translates the given inline assembly code (which must be in either gcc or msc style) to non-assembly ...
Expression to hold a symbol (variable)
Definition std_expr.h:113
const symbol_base_mapt & symbol_base_map
Read-only field, used to look up symbol names given their base names.
bool has_symbol(const irep_idt &name) const
Check whether a symbol exists in the symbol table.
bool add(const symbolt &symbol)
Add a new symbol to the symbol table.
const symbolt & lookup_ref(const irep_idt &name) const
Find a symbol in the symbol table for read-only access.
The symbol table.
Symbol table entry.
Definition symbol.h:28
Semantic type conversion.
Definition std_expr.h:2017
static exprt conditional_cast(const exprt &expr, const typet &type)
Definition std_expr.h:2025
The type of an expression, extends irept.
Definition type.h:29
bool has_prefix(const std::string &s, const std::string &prefix)
Definition converter.cpp:13
#define forall_operands(it, expr)
Definition expr.h:20
Symbol Table + CFG.
#define Forall_goto_program_instructions(it, program)
const std::string & id2string(const irep_idt &d)
Definition irep.h:47
literalt pos(literalt a)
Definition literal.h:194
API to expression classes for Pointers.
Ranges: pair of begin and end iterators, which can be initialized from containers,...
ranget< typename multimapt::const_iterator > equal_range(const multimapt &multimap, const typename multimapt::key_type &key)
Utility function to make equal_range method of multimap easier to use by returning a ranget object.
Definition range.h:541
void remove_asm(goto_functionst &goto_functions, symbol_tablet &symbol_table)
Replaces inline assembly instructions in the goto program (i.e., instructions of kind OTHER with a co...
Remove 'asm' statements by compiling them into suitable standard goto program instructions.
void remove_skip(goto_programt &goto_program, goto_programt::targett begin, goto_programt::targett end)
remove unnecessary skip statements
Program Transformation.
#define DATA_INVARIANT(CONDITION, REASON)
This condition should be used to document that assumptions that are made on goto_functions,...
Definition invariant.h:534
code_asm_gcct & to_code_asm_gcc(codet &code)
Definition std_code.h:1373
code_asmt & to_code_asm(codet &code)
Definition std_code.h:1282
const binary_exprt & to_binary_expr(const exprt &expr)
Cast an exprt to a binary_exprt.
Definition std_expr.h:660
const string_constantt & to_string_constant(const exprt &expr)