cprover
remove_asm.cpp
Go to the documentation of this file.
1 /*******************************************************************\
2 
3 Module: Remove 'asm' statements by compiling them into suitable
4  standard goto program instructions
5 
6 Author: Daniel Kroening
7 
8 Date: 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/string_constant.h>
21 
24 
25 #include "assembler_parser.h"
26 
28 {
29 public:
30  remove_asmt(symbol_tablet &_symbol_table, goto_functionst &_goto_functions)
31  : symbol_table(_symbol_table), goto_functions(_goto_functions)
32  {
33  }
34 
35  void operator()()
36  {
37  for(auto &f : goto_functions.function_map)
38  process_function(f.second);
39  }
40 
41 protected:
44 
46 
48  goto_programt::instructiont &instruction,
49  goto_programt &dest);
50 
52 
53  void process_instruction_msc(const code_asmt &, goto_programt &dest);
54 
56  const irep_idt &function_base_name,
57  const code_asm_gcct &code,
58  goto_programt &dest);
59 
61  const irep_idt &function_base_name,
62  const code_asmt &code,
63  goto_programt &dest);
64 };
65 
74  const irep_idt &function_base_name,
75  const code_asm_gcct &code,
76  goto_programt &dest)
77 {
78  irep_idt function_identifier = function_base_name;
79 
81 
82  const typet void_pointer = pointer_type(empty_typet());
83 
84  // outputs
85  forall_operands(it, code.outputs())
86  {
87  if(it->operands().size() == 2)
88  {
89  arguments.push_back(typecast_exprt(
90  address_of_exprt(to_binary_expr(*it).op1()), void_pointer));
91  }
92  }
93 
94  // inputs
95  forall_operands(it, code.inputs())
96  {
97  if(it->operands().size() == 2)
98  {
99  arguments.push_back(typecast_exprt(
100  address_of_exprt(to_binary_expr(*it).op1()), void_pointer));
101  }
102  }
103 
104  code_typet fkt_type({}, empty_typet());
105 
106  symbol_exprt fkt(function_identifier, fkt_type);
107 
108  code_function_callt function_call(std::move(fkt), std::move(arguments));
109 
110  dest.add(
111  goto_programt::make_function_call(function_call, code.source_location()));
112 
113  // do we have it?
114  if(!symbol_table.has_symbol(function_identifier))
115  {
116  symbolt symbol;
117 
118  symbol.name = function_identifier;
119  symbol.type = fkt_type;
120  symbol.base_name = function_base_name;
121  symbol.value = nil_exprt();
122  symbol.mode = ID_C;
123 
124  symbol_table.add(symbol);
125 
126  goto_functions.function_map.emplace(function_identifier, goto_functiont());
127  }
128  else
129  {
131  symbol_table.lookup_ref(function_identifier).type == fkt_type,
132  "function types should match");
133  }
134 }
135 
144  const irep_idt &function_base_name,
145  const code_asmt &code,
146  goto_programt &dest)
147 {
148  irep_idt function_identifier = function_base_name;
149 
150  const typet void_pointer = pointer_type(empty_typet());
151 
152  code_typet fkt_type({}, empty_typet());
153 
154  symbol_exprt fkt(function_identifier, fkt_type);
155 
156  code_function_callt function_call(fkt);
157 
158  dest.add(
159  goto_programt::make_function_call(function_call, code.source_location()));
160 
161  // do we have it?
162  if(!symbol_table.has_symbol(function_identifier))
163  {
164  symbolt symbol;
165 
166  symbol.name = function_identifier;
167  symbol.type = fkt_type;
168  symbol.base_name = function_base_name;
169  symbol.value = nil_exprt();
170  symbol.mode = ID_C;
171 
172  symbol_table.add(symbol);
173 
174  goto_functions.function_map.emplace(function_identifier, goto_functiont());
175  }
176  else
177  {
179  symbol_table.lookup_ref(function_identifier).type == fkt_type,
180  "function types should match");
181  }
182 }
183 
191  goto_programt::instructiont &instruction,
192  goto_programt &dest)
193 {
194  const code_asmt &code = to_code_asm(instruction.get_other());
195 
196  const irep_idt &flavor = code.get_flavor();
197 
198  if(flavor == ID_gcc)
200  else if(flavor == ID_msc)
201  process_instruction_msc(code, dest);
202  else
203  DATA_INVARIANT(false, "unexpected assembler flavor");
204 }
205 
212  const code_asm_gcct &code,
213  goto_programt &dest)
214 {
215  const irep_idt &i_str = to_string_constant(code.asm_text()).get_value();
216 
217  std::istringstream str(id2string(i_str));
219  assembler_parser.in = &str;
221 
222  goto_programt tmp_dest;
223  bool unknown = false;
224  bool x86_32_locked_atomic = false;
225 
226  for(const auto &instruction : assembler_parser.instructions)
227  {
228  if(instruction.empty())
229  continue;
230 
231 #if 0
232  std::cout << "A ********************\n";
233  for(const auto &ins : instruction)
234  {
235  std::cout << "XX: " << ins.pretty() << '\n';
236  }
237 
238  std::cout << "B ********************\n";
239 #endif
240 
241  // deal with prefixes
242  irep_idt command;
243  unsigned pos = 0;
244 
245  if(
246  instruction.front().id() == ID_symbol &&
247  instruction.front().get(ID_identifier) == "lock")
248  {
249  x86_32_locked_atomic = true;
250  pos++;
251  }
252 
253  // done?
254  if(pos == instruction.size())
255  continue;
256 
257  if(instruction[pos].id() == ID_symbol)
258  {
259  command = instruction[pos].get(ID_identifier);
260  pos++;
261  }
262 
263  if(command == "xchg" || command == "xchgl")
264  x86_32_locked_atomic = true;
265 
266  if(x86_32_locked_atomic)
267  {
269 
270  codet code_fence(ID_fence);
271  code_fence.add_source_location() = code.source_location();
272  code_fence.set(ID_WWfence, true);
273  code_fence.set(ID_RRfence, true);
274  code_fence.set(ID_RWfence, true);
275  code_fence.set(ID_WRfence, true);
276 
277  tmp_dest.add(
278  goto_programt::make_other(code_fence, code.source_location()));
279  }
280 
281  if(command == "fstcw" || command == "fnstcw" || command == "fldcw") // x86
282  {
283  gcc_asm_function_call("__asm_" + id2string(command), code, tmp_dest);
284  }
285  else if(
286  command == "mfence" || command == "lfence" || command == "sfence") // x86
287  {
288  gcc_asm_function_call("__asm_" + id2string(command), code, tmp_dest);
289  }
290  else if(command == ID_sync) // Power
291  {
292  codet code_fence(ID_fence);
293  code_fence.add_source_location() = code.source_location();
294  code_fence.set(ID_WWfence, true);
295  code_fence.set(ID_RRfence, true);
296  code_fence.set(ID_RWfence, true);
297  code_fence.set(ID_WRfence, true);
298  code_fence.set(ID_WWcumul, true);
299  code_fence.set(ID_RWcumul, true);
300  code_fence.set(ID_RRcumul, true);
301  code_fence.set(ID_WRcumul, true);
302 
303  tmp_dest.add(
304  goto_programt::make_other(code_fence, code.source_location()));
305  }
306  else if(command == ID_lwsync) // Power
307  {
308  codet code_fence(ID_fence);
309  code_fence.add_source_location() = code.source_location();
310  code_fence.set(ID_WWfence, true);
311  code_fence.set(ID_RRfence, true);
312  code_fence.set(ID_RWfence, true);
313  code_fence.set(ID_WWcumul, true);
314  code_fence.set(ID_RWcumul, true);
315  code_fence.set(ID_RRcumul, true);
316 
317  tmp_dest.add(
318  goto_programt::make_other(code_fence, code.source_location()));
319  }
320  else if(command == ID_isync) // Power
321  {
322  codet code_fence(ID_fence);
323  code_fence.add_source_location() = code.source_location();
324 
325  tmp_dest.add(
326  goto_programt::make_other(code_fence, code.source_location()));
327  // doesn't do anything by itself,
328  // needs to be combined with branch
329  }
330  else if(command == "dmb" || command == "dsb") // ARM
331  {
332  codet code_fence(ID_fence);
333  code_fence.add_source_location() = code.source_location();
334  code_fence.set(ID_WWfence, true);
335  code_fence.set(ID_RRfence, true);
336  code_fence.set(ID_RWfence, true);
337  code_fence.set(ID_WRfence, true);
338  code_fence.set(ID_WWcumul, true);
339  code_fence.set(ID_RWcumul, true);
340  code_fence.set(ID_RRcumul, true);
341  code_fence.set(ID_WRcumul, true);
342 
343  tmp_dest.add(
344  goto_programt::make_other(code_fence, code.source_location()));
345  }
346  else if(command == "isb") // ARM
347  {
348  codet code_fence(ID_fence);
349  code_fence.add_source_location() = code.source_location();
350 
351  tmp_dest.add(
352  goto_programt::make_other(code_fence, code.source_location()));
353  // doesn't do anything by itself,
354  // needs to be combined with branch
355  }
356  else
357  unknown = true; // give up
358 
359  if(x86_32_locked_atomic)
360  {
362 
363  x86_32_locked_atomic = false;
364  }
365  }
366 
367  if(unknown)
368  {
369  // we give up; we should perhaps print a warning
370  }
371  else
372  dest.destructive_append(tmp_dest);
373 }
374 
381  const code_asmt &code,
382  goto_programt &dest)
383 {
384  const irep_idt &i_str = to_string_constant(code.op0()).get_value();
385 
386  std::istringstream str(id2string(i_str));
388  assembler_parser.in = &str;
390 
391  goto_programt tmp_dest;
392  bool unknown = false;
393  bool x86_32_locked_atomic = false;
394 
395  for(const auto &instruction : assembler_parser.instructions)
396  {
397  if(instruction.empty())
398  continue;
399 
400 #if 0
401  std::cout << "A ********************\n";
402  for(const auto &ins : instruction)
403  {
404  std::cout << "XX: " << ins.pretty() << '\n';
405  }
406 
407  std::cout << "B ********************\n";
408 #endif
409 
410  // deal with prefixes
411  irep_idt command;
412  unsigned pos = 0;
413 
414  if(
415  instruction.front().id() == ID_symbol &&
416  instruction.front().get(ID_identifier) == "lock")
417  {
418  x86_32_locked_atomic = true;
419  pos++;
420  }
421 
422  // done?
423  if(pos == instruction.size())
424  continue;
425 
426  if(instruction[pos].id() == ID_symbol)
427  {
428  command = instruction[pos].get(ID_identifier);
429  pos++;
430  }
431 
432  if(command == "xchg" || command == "xchgl")
433  x86_32_locked_atomic = true;
434 
435  if(x86_32_locked_atomic)
436  {
438 
439  codet code_fence(ID_fence);
440  code_fence.add_source_location() = code.source_location();
441  code_fence.set(ID_WWfence, true);
442  code_fence.set(ID_RRfence, true);
443  code_fence.set(ID_RWfence, true);
444  code_fence.set(ID_WRfence, true);
445 
446  tmp_dest.add(
447  goto_programt::make_other(code_fence, code.source_location()));
448  }
449 
450  if(command == "fstcw" || command == "fnstcw" || command == "fldcw") // x86
451  {
452  msc_asm_function_call("__asm_" + id2string(command), code, tmp_dest);
453  }
454  else if(
455  command == "mfence" || command == "lfence" || command == "sfence") // x86
456  {
457  msc_asm_function_call("__asm_" + id2string(command), code, tmp_dest);
458  }
459  else
460  unknown = true; // give up
461 
462  if(x86_32_locked_atomic)
463  {
465 
466  x86_32_locked_atomic = false;
467  }
468  }
469 
470  if(unknown)
471  {
472  // we give up; we should perhaps print a warning
473  }
474  else
475  dest.destructive_append(tmp_dest);
476 }
477 
483  goto_functionst::goto_functiont &goto_function)
484 {
485  bool did_something = false;
486 
487  Forall_goto_program_instructions(it, goto_function.body)
488  {
489  if(it->is_other() && it->get_other().get_statement() == ID_asm)
490  {
491  goto_programt tmp_dest;
492  process_instruction(*it, tmp_dest);
493  it->turn_into_skip();
494  did_something = true;
495 
496  goto_programt::targett next = it;
497  next++;
498 
499  goto_function.body.destructive_insert(next, tmp_dest);
500  }
501  }
502 
503  if(did_something)
504  remove_skip(goto_function.body);
505 }
506 
511 void remove_asm(goto_functionst &goto_functions, symbol_tablet &symbol_table)
512 {
513  remove_asmt rem(symbol_table, goto_functions);
514  rem();
515 }
516 
524 void remove_asm(goto_modelt &goto_model)
525 {
526  remove_asm(goto_model.goto_functions, goto_model.symbol_table);
527 }
Forall_goto_program_instructions
#define Forall_goto_program_instructions(it, program)
Definition: goto_program.h:1185
symbol_table_baset::has_symbol
bool has_symbol(const irep_idt &name) const
Check whether a symbol exists in the symbol table.
Definition: symbol_table_base.h:87
dstringt
dstringt has one field, an unsigned integer no which is an index into a static table of strings.
Definition: dstring.h:37
symbol_tablet
The symbol table.
Definition: symbol_table.h:20
code_asm_gcct
codet representation of an inline assembler statement, for the gcc flavor.
Definition: std_code.h:1745
symbol_table_baset::lookup_ref
const symbolt & lookup_ref(const irep_idt &name) const
Find a symbol in the symbol table for read-only access.
Definition: symbol_table_base.h:104
codet::op0
exprt & op0()
Definition: expr.h:103
code_asm_gcct::outputs
exprt & outputs()
Definition: std_code.h:1763
code_asmt
codet representation of an inline assembler statement.
Definition: std_code.h:1701
pos
literalt pos(literalt a)
Definition: literal.h:194
remove_asmt
Definition: remove_asm.cpp:28
typet
The type of an expression, extends irept.
Definition: type.h:28
remove_asmt::goto_functions
goto_functionst & goto_functions
Definition: remove_asm.cpp:43
assembler_parsert::parse
virtual bool parse()
Definition: assembler_parser.h:44
symbolt::type
typet type
Type of symbol.
Definition: symbol.h:31
remove_skip
void remove_skip(goto_programt &goto_program, goto_programt::targett begin, goto_programt::targett end)
remove unnecessary skip statements
Definition: remove_skip.cpp:86
remove_asm.h
Remove 'asm' statements by compiling them into suitable standard goto program instructions.
to_string_constant
const string_constantt & to_string_constant(const exprt &expr)
Definition: string_constant.h:31
goto_programt::add
targett add(instructiont &&instruction)
Adds a given instruction at the end.
Definition: goto_program.h:670
goto_model.h
Symbol Table + CFG.
string_constant.h
code_asm_gcct::inputs
exprt & inputs()
Definition: std_code.h:1773
goto_modelt
Definition: goto_model.h:26
symbolt::base_name
irep_idt base_name
Base (non-scoped) name.
Definition: symbol.h:46
remove_asmt::process_instruction_msc
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.
Definition: remove_asm.cpp:380
goto_functionst::function_map
function_mapt function_map
Definition: goto_functions.h:27
symbol_exprt
Expression to hold a symbol (variable)
Definition: std_expr.h:80
assembler_parser
assembler_parsert assembler_parser
Definition: assembler_parser.cpp:11
goto_programt::instructiont::get_other
const codet & get_other() const
Get the statement for OTHER.
Definition: goto_program.h:333
remove_asmt::process_function
void process_function(goto_functionst::goto_functiont &)
Replaces inline assembly instructions in the goto function by non-assembly goto program instructions.
Definition: remove_asm.cpp:482
to_binary_expr
const binary_exprt & to_binary_expr(const exprt &expr)
Cast an exprt to a binary_exprt.
Definition: std_expr.h:627
goto_programt::make_function_call
static instructiont make_function_call(const code_function_callt &_code, const source_locationt &l=source_locationt::nil())
Create a function call instruction.
Definition: goto_program.h:1033
code_function_callt
codet representation of a function call statement.
Definition: std_code.h:1215
symbolt::mode
irep_idt mode
Language mode.
Definition: symbol.h:49
empty_typet
The empty type.
Definition: std_types.h:45
parsert::in
std::istream * in
Definition: parser.h:26
DATA_INVARIANT
#define DATA_INVARIANT(CONDITION, REASON)
This condition should be used to document that assumptions that are made on goto_functions,...
Definition: invariant.h:511
id2string
const std::string & id2string(const irep_idt &d)
Definition: irep.h:49
forall_operands
#define forall_operands(it, expr)
Definition: expr.h:18
assembler_parsert::clear
virtual void clear()
Definition: assembler_parser.h:50
nil_exprt
The NIL expression.
Definition: std_expr.h:2734
pointer_expr.h
API to expression classes for Pointers.
remove_asmt::remove_asmt
remove_asmt(symbol_tablet &_symbol_table, goto_functionst &_goto_functions)
Definition: remove_asm.cpp:30
remove_asmt::gcc_asm_function_call
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.
Definition: remove_asm.cpp:73
pointer_type
pointer_typet pointer_type(const typet &subtype)
Definition: c_types.cpp:243
goto_programt::make_atomic_begin
static instructiont make_atomic_begin(const source_locationt &l=source_locationt::nil())
Definition: goto_program.h:919
code_typet
Base type of functions.
Definition: std_types.h:533
remove_asmt::process_instruction_gcc
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.
Definition: remove_asm.cpp:211
goto_functiont
A goto function, consisting of function body (see body) and parameter identifiers (see parameter_iden...
Definition: goto_function.h:27
code_function_callt::argumentst
exprt::operandst argumentst
Definition: std_code.h:1224
to_code_asm_gcc
code_asm_gcct & to_code_asm_gcc(codet &code)
Definition: std_code.h:1821
assembler_parsert::instructions
std::list< instructiont > instructions
Definition: assembler_parser.h:25
goto_programt::destructive_append
void destructive_append(goto_programt &p)
Appends the given program p to *this. p is destroyed.
Definition: goto_program.h:653
goto_functionst::goto_functiont
::goto_functiont goto_functiont
Definition: goto_functions.h:25
to_code_asm
code_asmt & to_code_asm(codet &code)
Definition: std_code.h:1730
symbol_table_baset::add
bool add(const symbolt &symbol)
Add a new symbol to the symbol table.
Definition: symbol_table_base.cpp:18
goto_functionst
A collection of goto functions.
Definition: goto_functions.h:23
symbolt::value
exprt value
Initial value of symbol.
Definition: symbol.h:34
goto_modelt::goto_functions
goto_functionst goto_functions
GOTO functions.
Definition: goto_model.h:33
symbolt
Symbol table entry.
Definition: symbol.h:28
irept::set
void set(const irep_namet &name, const irep_idt &value)
Definition: irep.h:431
assembler_parser.h
goto_programt::make_other
static instructiont make_other(const codet &_code, const source_locationt &l=source_locationt::nil())
Definition: goto_program.h:897
remove_asm
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...
Definition: remove_asm.cpp:511
code_asm_gcct::asm_text
exprt & asm_text()
Definition: std_code.h:1753
goto_programt
A generic container class for the GOTO intermediate representation of one function.
Definition: goto_program.h:74
remove_asmt::operator()
void operator()()
Definition: remove_asm.cpp:35
address_of_exprt
Operator to return the address of an object.
Definition: pointer_expr.h:330
exprt::add_source_location
source_locationt & add_source_location()
Definition: expr.h:243
remove_asmt::msc_asm_function_call
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.
Definition: remove_asm.cpp:143
code_asmt::get_flavor
const irep_idt & get_flavor() const
Definition: std_code.h:1711
typecast_exprt
Semantic type conversion.
Definition: std_expr.h:1780
remove_asmt::symbol_table
symbol_tablet & symbol_table
Definition: remove_asm.cpp:42
remove_skip.h
Program Transformation.
binary_exprt::op1
exprt & op1()
Definition: expr.h:106
goto_programt::instructiont
This class represents an instruction in the GOTO intermediate representation.
Definition: goto_program.h:180
exprt::source_location
const source_locationt & source_location() const
Definition: expr.h:238
goto_modelt::symbol_table
symbol_tablet symbol_table
Symbol table.
Definition: goto_model.h:30
c_types.h
symbolt::name
irep_idt name
The unique identifier.
Definition: symbol.h:40
string_constantt::get_value
const irep_idt & get_value() const
Definition: string_constant.h:22
goto_programt::targett
instructionst::iterator targett
Definition: goto_program.h:563
goto_programt::make_atomic_end
static instructiont make_atomic_end(const source_locationt &l=source_locationt::nil())
Definition: goto_program.h:930
remove_asmt::process_instruction
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 ...
Definition: remove_asm.cpp:190
codet
Data structure for representing an arbitrary statement in a program.
Definition: std_code.h:35