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/std_code.h>
22
25
26#include "assembler_parser.h"
27
66
76 const code_asm_gcct &code,
78{
79 irep_idt function_identifier = function_base_name;
80
82
84
85 // outputs
86 forall_operands(it, code.outputs())
87 {
88 if(it->operands().size() == 2)
89 {
90 arguments.push_back(typecast_exprt(
92 }
93 }
94
95 // inputs
96 forall_operands(it, code.inputs())
97 {
98 if(it->operands().size() == 2)
99 {
100 arguments.push_back(typecast_exprt(
102 }
103 }
104
106
107 symbol_exprt fkt(function_identifier, fkt_type);
108
109 code_function_callt function_call(std::move(fkt), std::move(arguments));
110
111 dest.add(
113
114 // do we have it?
115 if(!symbol_table.has_symbol(function_identifier))
116 {
117 symbolt symbol;
118
119 symbol.name = function_identifier;
120 symbol.type = fkt_type;
122 symbol.value = nil_exprt();
123 symbol.mode = ID_C;
124
125 symbol_table.add(symbol);
126
127 goto_functions.function_map.emplace(function_identifier, goto_functiont());
128 }
129 else
130 {
132 symbol_table.lookup_ref(function_identifier).type == fkt_type,
133 "function types should match");
134 }
135}
136
146 const code_asmt &code,
148{
149 irep_idt function_identifier = function_base_name;
150
152
154
155 symbol_exprt fkt(function_identifier, fkt_type);
156
157 code_function_callt function_call(fkt);
158
159 dest.add(
161
162 // do we have it?
163 if(!symbol_table.has_symbol(function_identifier))
164 {
165 symbolt symbol;
166
167 symbol.name = function_identifier;
168 symbol.type = fkt_type;
170 symbol.value = nil_exprt();
171 symbol.mode = ID_C;
172
173 symbol_table.add(symbol);
174
175 goto_functions.function_map.emplace(function_identifier, goto_functiont());
176 }
177 else
178 {
180 symbol_table.lookup_ref(function_identifier).type == fkt_type,
181 "function types should match");
182 }
183}
184
192 goto_programt::instructiont &instruction,
194{
195 const code_asmt &code = to_code_asm(instruction.get_other());
196
197 const irep_idt &flavor = code.get_flavor();
198
199 if(flavor == ID_gcc)
201 else if(flavor == ID_msc)
203 else
204 DATA_INVARIANT(false, "unexpected assembler flavor");
205}
206
213 const code_asm_gcct &code,
215{
217
218 std::istringstream str(id2string(i_str));
220 assembler_parser.in = &str;
222
224 bool unknown = false;
225 bool x86_32_locked_atomic = false;
226
227 for(const auto &instruction : assembler_parser.instructions)
228 {
229 if(instruction.empty())
230 continue;
231
232#if 0
233 std::cout << "A ********************\n";
234 for(const auto &ins : instruction)
235 {
236 std::cout << "XX: " << ins.pretty() << '\n';
237 }
238
239 std::cout << "B ********************\n";
240#endif
241
242 // deal with prefixes
243 irep_idt command;
244 unsigned pos = 0;
245
246 if(
247 instruction.front().id() == ID_symbol &&
248 instruction.front().get(ID_identifier) == "lock")
249 {
251 pos++;
252 }
253
254 // done?
255 if(pos == instruction.size())
256 continue;
257
258 if(instruction[pos].id() == ID_symbol)
259 {
260 command = instruction[pos].get(ID_identifier);
261 pos++;
262 }
263
264 if(command == "xchg" || command == "xchgl")
266
268 {
270
272 code_fence.add_source_location() = code.source_location();
273 code_fence.set(ID_WWfence, true);
274 code_fence.set(ID_RRfence, true);
275 code_fence.set(ID_RWfence, true);
276 code_fence.set(ID_WRfence, true);
277
278 tmp_dest.add(
280 }
281
282 if(command == "fstcw" || command == "fnstcw" || command == "fldcw") // x86
283 {
284 gcc_asm_function_call("__asm_" + id2string(command), code, tmp_dest);
285 }
286 else if(
287 command == "mfence" || command == "lfence" || command == "sfence") // x86
288 {
289 gcc_asm_function_call("__asm_" + id2string(command), code, tmp_dest);
290 }
291 else if(command == ID_sync) // Power
292 {
294 code_fence.add_source_location() = code.source_location();
295 code_fence.set(ID_WWfence, true);
296 code_fence.set(ID_RRfence, true);
297 code_fence.set(ID_RWfence, true);
298 code_fence.set(ID_WRfence, true);
299 code_fence.set(ID_WWcumul, true);
300 code_fence.set(ID_RWcumul, true);
301 code_fence.set(ID_RRcumul, true);
302 code_fence.set(ID_WRcumul, true);
303
304 tmp_dest.add(
306 }
307 else if(command == ID_lwsync) // Power
308 {
310 code_fence.add_source_location() = code.source_location();
311 code_fence.set(ID_WWfence, true);
312 code_fence.set(ID_RRfence, true);
313 code_fence.set(ID_RWfence, true);
314 code_fence.set(ID_WWcumul, true);
315 code_fence.set(ID_RWcumul, true);
316 code_fence.set(ID_RRcumul, true);
317
318 tmp_dest.add(
320 }
321 else if(command == ID_isync) // Power
322 {
324 code_fence.add_source_location() = code.source_location();
325
326 tmp_dest.add(
328 // doesn't do anything by itself,
329 // needs to be combined with branch
330 }
331 else if(command == "dmb" || command == "dsb") // ARM
332 {
334 code_fence.add_source_location() = code.source_location();
335 code_fence.set(ID_WWfence, true);
336 code_fence.set(ID_RRfence, true);
337 code_fence.set(ID_RWfence, true);
338 code_fence.set(ID_WRfence, true);
339 code_fence.set(ID_WWcumul, true);
340 code_fence.set(ID_RWcumul, true);
341 code_fence.set(ID_RRcumul, true);
342 code_fence.set(ID_WRcumul, true);
343
344 tmp_dest.add(
346 }
347 else if(command == "isb") // ARM
348 {
350 code_fence.add_source_location() = code.source_location();
351
352 tmp_dest.add(
354 // doesn't do anything by itself,
355 // needs to be combined with branch
356 }
357 else
358 unknown = true; // give up
359
361 {
363
364 x86_32_locked_atomic = false;
365 }
366 }
367
368 if(unknown)
369 {
370 // we give up; we should perhaps print a warning
371 }
372 else
373 dest.destructive_append(tmp_dest);
374}
375
382 const code_asmt &code,
384{
385 const irep_idt &i_str = to_string_constant(code.op0()).get_value();
386
387 std::istringstream str(id2string(i_str));
389 assembler_parser.in = &str;
391
393 bool unknown = false;
394 bool x86_32_locked_atomic = false;
395
396 for(const auto &instruction : assembler_parser.instructions)
397 {
398 if(instruction.empty())
399 continue;
400
401#if 0
402 std::cout << "A ********************\n";
403 for(const auto &ins : instruction)
404 {
405 std::cout << "XX: " << ins.pretty() << '\n';
406 }
407
408 std::cout << "B ********************\n";
409#endif
410
411 // deal with prefixes
412 irep_idt command;
413 unsigned pos = 0;
414
415 if(
416 instruction.front().id() == ID_symbol &&
417 instruction.front().get(ID_identifier) == "lock")
418 {
420 pos++;
421 }
422
423 // done?
424 if(pos == instruction.size())
425 continue;
426
427 if(instruction[pos].id() == ID_symbol)
428 {
429 command = instruction[pos].get(ID_identifier);
430 pos++;
431 }
432
433 if(command == "xchg" || command == "xchgl")
435
437 {
439
441 code_fence.add_source_location() = code.source_location();
442 code_fence.set(ID_WWfence, true);
443 code_fence.set(ID_RRfence, true);
444 code_fence.set(ID_RWfence, true);
445 code_fence.set(ID_WRfence, true);
446
447 tmp_dest.add(
449 }
450
451 if(command == "fstcw" || command == "fnstcw" || command == "fldcw") // x86
452 {
453 msc_asm_function_call("__asm_" + id2string(command), code, tmp_dest);
454 }
455 else if(
456 command == "mfence" || command == "lfence" || command == "sfence") // x86
457 {
458 msc_asm_function_call("__asm_" + id2string(command), code, tmp_dest);
459 }
460 else
461 unknown = true; // give up
462
464 {
466
467 x86_32_locked_atomic = false;
468 }
469 }
470
471 if(unknown)
472 {
473 // we give up; we should perhaps print a warning
474 }
475 else
476 dest.destructive_append(tmp_dest);
477}
478
484 goto_functionst::goto_functiont &goto_function)
485{
486 bool did_something = false;
487
488 Forall_goto_program_instructions(it, goto_function.body)
489 {
490 if(it->is_other() && it->get_other().get_statement() == ID_asm)
491 {
494 it->turn_into_skip();
495 did_something = true;
496
497 goto_programt::targett next = it;
498 next++;
499
500 goto_function.body.destructive_insert(next, tmp_dest);
501 }
502 }
503
504 if(did_something)
505 remove_skip(goto_function.body);
506}
507
512void remove_asm(goto_functionst &goto_functions, symbol_tablet &symbol_table)
513{
514 remove_asmt rem(symbol_table, goto_functions);
515 rem();
516}
517
525void remove_asm(goto_modelt &goto_model)
526{
527 remove_asm(goto_model.goto_functions, goto_model.symbol_table);
528}
assembler_parsert assembler_parser
pointer_typet pointer_type(const typet &subtype)
Definition c_types.cpp:253
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:564
virtual bool parse()
std::list< instructiont > instructions
virtual void clear()
exprt & op1()
Definition expr.h:102
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
codet representation of a function call statement.
Base type of functions.
Definition std_types.h:539
Data structure for representing an arbitrary statement in a program.
exprt & op0()
Definition expr.h:99
dstringt has one field, an unsigned integer no which is an index into a static table of strings.
Definition dstring.h:37
The empty type.
Definition std_types.h:51
const source_locationt & source_location() const
Definition expr.h:230
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:30
goto_functionst goto_functions
GOTO functions.
Definition goto_model.h:33
This class represents an instruction in the GOTO intermediate representation.
const codet & get_other() const
Get the statement for OTHER.
A generic container class for the GOTO intermediate representation of one function.
instructionst::iterator targett
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_atomic_begin(const source_locationt &l=source_locationt::nil())
static instructiont make_other(const codet &_code, const source_locationt &l=source_locationt::nil())
The NIL expression.
Definition std_expr.h:2874
std::istream * in
Definition parser.h:26
goto_functionst & goto_functions
symbol_tablet & symbol_table
void operator()()
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 msc_asm_function_call(const irep_idt &function_base_name, const code_asmt &code, goto_programt &dest)
Adds a call to a library function that implements the given msc-style inline assembly statement.
void process_instruction_msc(const code_asmt &, goto_programt &dest)
Translates the given inline assembly code (in msc style) to non-assembly goto program instructions.
void process_instruction(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 ...
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_function(goto_functionst::goto_functiont &)
Replaces inline assembly instructions in the goto function by non-assembly goto program instructions.
const irep_idt & get_value() const
Expression to hold a symbol (variable)
Definition std_expr.h:80
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
typet type
Type of symbol.
Definition symbol.h:31
irep_idt name
The unique identifier.
Definition symbol.h:40
irep_idt irep_idt base_name
Name of module the symbol belongs to.
Definition symbol.h:46
exprt value
Initial value of symbol.
Definition symbol.h:34
irep_idt mode
Language mode.
Definition symbol.h:49
Semantic type conversion.
Definition std_expr.h:1920
The type of an expression, extends irept.
Definition type.h:29
#define forall_operands(it, expr)
Definition expr.h:18
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.
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:510
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:627
const string_constantt & to_string_constant(const exprt &expr)