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/string_constant.h>
20 
23 
24 #include "assembler_parser.h"
25 
27 {
28 public:
29  remove_asmt(symbol_tablet &_symbol_table, goto_functionst &_goto_functions)
30  : symbol_table(_symbol_table), goto_functions(_goto_functions)
31  {
32  }
33 
34  void operator()()
35  {
36  for(auto &f : goto_functions.function_map)
37  process_function(f.second);
38  }
39 
40 protected:
43 
45 
47  goto_programt::instructiont &instruction,
48  goto_programt &dest);
49 
51 
52  void process_instruction_msc(const code_asmt &, goto_programt &dest);
53 
55  const irep_idt &function_base_name,
56  const code_asm_gcct &code,
57  goto_programt &dest);
58 
60  const irep_idt &function_base_name,
61  const code_asmt &code,
62  goto_programt &dest);
63 };
64 
73  const irep_idt &function_base_name,
74  const code_asm_gcct &code,
75  goto_programt &dest)
76 {
77  irep_idt function_identifier = function_base_name;
78 
80 
81  const typet void_pointer = pointer_type(empty_typet());
82 
83  // outputs
84  forall_operands(it, code.outputs())
85  {
86  if(it->operands().size() == 2)
87  {
88  arguments.push_back(typecast_exprt(
89  address_of_exprt(to_binary_expr(*it).op1()), void_pointer));
90  }
91  }
92 
93  // inputs
94  forall_operands(it, code.inputs())
95  {
96  if(it->operands().size() == 2)
97  {
98  arguments.push_back(typecast_exprt(
99  address_of_exprt(to_binary_expr(*it).op1()), void_pointer));
100  }
101  }
102 
103  code_typet fkt_type({}, empty_typet());
104  fkt_type.make_ellipsis();
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 
127  if(
128  goto_functions.function_map.find(function_identifier) ==
130  {
131  auto &f = goto_functions.function_map[function_identifier];
132  f.type = fkt_type;
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  fkt_type.make_ellipsis();
154 
155  symbol_exprt fkt(function_identifier, fkt_type);
156 
157  code_function_callt function_call(fkt);
158 
159  dest.add(
160  goto_programt::make_function_call(function_call, code.source_location()));
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;
169  symbol.base_name = function_base_name;
170  symbol.value = nil_exprt();
171  symbol.mode = ID_C;
172 
173  symbol_table.add(symbol);
174  }
175 
176  if(
177  goto_functions.function_map.find(function_identifier) ==
179  {
180  auto &f = goto_functions.function_map[function_identifier];
181  f.type = fkt_type;
182  }
183 }
184 
192  goto_programt::instructiont &instruction,
193  goto_programt &dest)
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)
202  process_instruction_msc(code, dest);
203  else
204  DATA_INVARIANT(false, "unexpected assembler flavor");
205 }
206 
213  const code_asm_gcct &code,
214  goto_programt &dest)
215 {
216  const irep_idt &i_str = to_string_constant(code.asm_text()).get_value();
217 
218  std::istringstream str(id2string(i_str));
220  assembler_parser.in = &str;
222 
223  goto_programt tmp_dest;
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  {
250  x86_32_locked_atomic = true;
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")
265  x86_32_locked_atomic = true;
266 
267  if(x86_32_locked_atomic)
268  {
270 
271  codet code_fence(ID_fence);
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(
279  goto_programt::make_other(code_fence, code.source_location()));
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  {
293  codet code_fence(ID_fence);
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(
305  goto_programt::make_other(code_fence, code.source_location()));
306  }
307  else if(command == ID_lwsync) // Power
308  {
309  codet code_fence(ID_fence);
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(
319  goto_programt::make_other(code_fence, code.source_location()));
320  }
321  else if(command == ID_isync) // Power
322  {
323  codet code_fence(ID_fence);
324  code_fence.add_source_location() = code.source_location();
325 
326  tmp_dest.add(
327  goto_programt::make_other(code_fence, code.source_location()));
328  // doesn't do anything by itself,
329  // needs to be combined with branch
330  }
331  else if(command == "dmb" || command == "dsb") // ARM
332  {
333  codet code_fence(ID_fence);
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(
345  goto_programt::make_other(code_fence, code.source_location()));
346  }
347  else if(command == "isb") // ARM
348  {
349  codet code_fence(ID_fence);
350  code_fence.add_source_location() = code.source_location();
351 
352  tmp_dest.add(
353  goto_programt::make_other(code_fence, code.source_location()));
354  // doesn't do anything by itself,
355  // needs to be combined with branch
356  }
357  else
358  unknown = true; // give up
359 
360  if(x86_32_locked_atomic)
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,
383  goto_programt &dest)
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 
392  goto_programt tmp_dest;
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  {
419  x86_32_locked_atomic = true;
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")
434  x86_32_locked_atomic = true;
435 
436  if(x86_32_locked_atomic)
437  {
439 
440  codet code_fence(ID_fence);
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(
448  goto_programt::make_other(code_fence, code.source_location()));
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 
463  if(x86_32_locked_atomic)
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  {
492  goto_programt tmp_dest;
493  process_instruction(*it, tmp_dest);
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 
512 void remove_asm(goto_functionst &goto_functions, symbol_tablet &symbol_table)
513 {
514  remove_asmt rem(symbol_table, goto_functions);
515  rem();
516 }
517 
525 void remove_asm(goto_modelt &goto_model)
526 {
527  remove_asm(goto_model.goto_functions, goto_model.symbol_table);
528 }
Forall_goto_program_instructions
#define Forall_goto_program_instructions(it, program)
Definition: goto_program.h:1201
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:1713
codet::op0
exprt & op0()
Definition: expr.h:102
code_asm_gcct::outputs
exprt & outputs()
Definition: std_code.h:1731
code_asmt
codet representation of an inline assembler statement.
Definition: std_code.h:1669
pos
literalt pos(literalt a)
Definition: literal.h:194
remove_asmt
Definition: remove_asm.cpp:27
typet
The type of an expression, extends irept.
Definition: type.h:29
remove_asmt::goto_functions
goto_functionst & goto_functions
Definition: remove_asm.cpp:42
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:85
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:686
goto_model.h
Symbol Table + CFG.
string_constant.h
code_asm_gcct::inputs
exprt & inputs()
Definition: std_code.h:1741
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:381
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:82
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:255
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:483
to_binary_expr
const binary_exprt & to_binary_expr(const exprt &expr)
Cast an exprt to a binary_exprt.
Definition: std_expr.h:678
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:1049
code_function_callt
codet representation of a function call statement.
Definition: std_code.h:1183
symbolt::mode
irep_idt mode
Language mode.
Definition: symbol.h:49
empty_typet
The empty type.
Definition: std_types.h:46
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:44
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:3973
remove_asmt::remove_asmt
remove_asmt(symbol_tablet &_symbol_table, goto_functionst &_goto_functions)
Definition: remove_asm.cpp:29
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:72
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:935
code_typet
Base type of functions.
Definition: std_types.h:736
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:212
code_function_callt::argumentst
exprt::operandst argumentst
Definition: std_code.h:1192
to_code_asm_gcc
code_asm_gcct & to_code_asm_gcc(codet &code)
Definition: std_code.h:1789
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:669
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:1698
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
code_typet::make_ellipsis
void make_ellipsis()
Definition: std_types.h:837
symbolt
Symbol table entry.
Definition: symbol.h:28
irept::set
void set(const irep_namet &name, const irep_idt &value)
Definition: irep.h:442
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:913
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:512
code_asm_gcct::asm_text
exprt & asm_text()
Definition: std_code.h:1721
goto_programt
A generic container class for the GOTO intermediate representation of one function.
Definition: goto_program.h:73
remove_asmt::operator()
void operator()()
Definition: remove_asm.cpp:34
address_of_exprt
Operator to return the address of an object.
Definition: std_expr.h:2786
exprt::add_source_location
source_locationt & add_source_location()
Definition: expr.h:259
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:1679
typecast_exprt
Semantic type conversion.
Definition: std_expr.h:2013
remove_asmt::symbol_table
symbol_tablet & symbol_table
Definition: remove_asm.cpp:41
remove_skip.h
Program Transformation.
binary_exprt::op1
exprt & op1()
Definition: expr.h:105
goto_programt::instructiont
This class represents an instruction in the GOTO intermediate representation.
Definition: goto_program.h:179
exprt::source_location
const source_locationt & source_location() const
Definition: expr.h:254
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:579
goto_programt::make_atomic_end
static instructiont make_atomic_end(const source_locationt &l=source_locationt::nil())
Definition: goto_program.h:946
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:191
codet
Data structure for representing an arbitrary statement in a program.
Definition: std_code.h:35