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 
22 
23 #include "goto_model.h"
24 #include "remove_skip.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 
50  void process_instruction_gcc(const code_asmt &, goto_programt &dest);
51 
52  void process_instruction_msc(const code_asmt &, goto_programt &dest);
53 
55  const irep_idt &function_base_name,
56  const code_asmt &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_asmt &code,
75  goto_programt &dest)
76 {
77  irep_idt function_identifier=function_base_name;
78 
79  code_function_callt function_call;
80  function_call.lhs().make_nil();
81 
82  const typet void_pointer=
84 
85  // outputs
86  forall_operands(it, code.op1())
87  {
88  if(it->operands().size()==2)
89  {
90  function_call.arguments().push_back(
91  typecast_exprt(address_of_exprt(it->op1()), void_pointer));
92  }
93  }
94 
95  // inputs
96  forall_operands(it, code.op2())
97  {
98  if(it->operands().size()==2)
99  {
100  function_call.arguments().push_back(
101  typecast_exprt(address_of_exprt(it->op1()), void_pointer));
102  }
103  }
104 
105  code_typet fkt_type({}, void_typet());
106  fkt_type.make_ellipsis();
107 
108  symbol_exprt fkt(function_identifier, fkt_type);
109 
110  function_call.function()=fkt;
111 
113  call->code=function_call;
114  call->source_location=code.source_location();
115 
116  // do we have it?
117  if(!symbol_table.has_symbol(function_identifier))
118  {
119  symbolt symbol;
120 
121  symbol.name=function_identifier;
122  symbol.type=fkt_type;
123  symbol.base_name=function_base_name;
124  symbol.value=nil_exprt();
125  symbol.mode = ID_C;
126 
127  symbol_table.add(symbol);
128  }
129 
130  if(
131  goto_functions.function_map.find(function_identifier) ==
133  {
134  auto &f = goto_functions.function_map[function_identifier];
135  f.type = fkt_type;
136  }
137 }
138 
147  const irep_idt &function_base_name,
148  const code_asmt &code,
149  goto_programt &dest)
150 {
151  irep_idt function_identifier = function_base_name;
152 
153  const typet void_pointer = pointer_type(void_typet());
154 
155  code_typet fkt_type({}, void_typet());
156  fkt_type.make_ellipsis();
157 
158  symbol_exprt fkt(function_identifier, fkt_type);
159 
160  code_function_callt function_call(fkt);
161 
163  call->code = function_call;
164  call->source_location = code.source_location();
165 
166  // do we have it?
167  if(!symbol_table.has_symbol(function_identifier))
168  {
169  symbolt symbol;
170 
171  symbol.name = function_identifier;
172  symbol.type = fkt_type;
173  symbol.base_name = function_base_name;
174  symbol.value = nil_exprt();
175  symbol.mode = ID_C;
176 
177  symbol_table.add(symbol);
178  }
179 
180  if(
181  goto_functions.function_map.find(function_identifier) ==
183  {
184  auto &f = goto_functions.function_map[function_identifier];
185  f.type = fkt_type;
186  }
187 }
188 
196  goto_programt::instructiont &instruction,
197  goto_programt &dest)
198 {
199  const code_asmt &code=to_code_asm(instruction.code);
200 
201  const irep_idt &flavor=code.get_flavor();
202 
203  if(flavor==ID_gcc)
204  process_instruction_gcc(code, dest);
205  else if(flavor == ID_msc)
206  process_instruction_msc(code, dest);
207  else
208  DATA_INVARIANT(false, "unexpected assembler flavor");
209 }
210 
217  const code_asmt &code,
218  goto_programt &dest)
219 {
220  const irep_idt &i_str = to_string_constant(code.op0()).get_value();
221 
222  std::istringstream str(id2string(i_str));
224  assembler_parser.in = &str;
226 
227  goto_programt tmp_dest;
228  bool unknown = false;
229  bool x86_32_locked_atomic = false;
230 
231  for(const auto &instruction : assembler_parser.instructions)
232  {
233  if(instruction.empty())
234  continue;
235 
236 #if 0
237  std::cout << "A ********************\n";
238  for(const auto &ins : instruction)
239  {
240  std::cout << "XX: " << ins.pretty() << '\n';
241  }
242 
243  std::cout << "B ********************\n";
244 #endif
245 
246  // deal with prefixes
247  irep_idt command;
248  unsigned pos = 0;
249 
250  if(
251  instruction.front().id() == ID_symbol &&
252  instruction.front().get(ID_identifier) == "lock")
253  {
254  x86_32_locked_atomic = true;
255  pos++;
256  }
257 
258  // done?
259  if(pos == instruction.size())
260  continue;
261 
262  if(instruction[pos].id() == ID_symbol)
263  {
264  command = instruction[pos].get(ID_identifier);
265  pos++;
266  }
267 
268  if(command == "xchg" || command == "xchgl")
269  x86_32_locked_atomic = true;
270 
271  if(x86_32_locked_atomic)
272  {
274  ab->source_location = code.source_location();
275 
277  t->source_location = code.source_location();
278  t->code = codet(ID_fence);
279  t->code.add_source_location() = code.source_location();
280  t->code.set(ID_WWfence, true);
281  t->code.set(ID_RRfence, true);
282  t->code.set(ID_RWfence, true);
283  t->code.set(ID_WRfence, true);
284  }
285 
286  if(command == "fstcw" || command == "fnstcw" || command == "fldcw") // x86
287  {
288  gcc_asm_function_call("__asm_" + id2string(command), code, tmp_dest);
289  }
290  else if(
291  command == "mfence" || command == "lfence" || command == "sfence") // x86
292  {
293  gcc_asm_function_call("__asm_" + id2string(command), code, tmp_dest);
294  }
295  else if(command == ID_sync) // Power
296  {
298  t->source_location = code.source_location();
299  t->code = codet(ID_fence);
300  t->code.add_source_location() = code.source_location();
301  t->code.set(ID_WWfence, true);
302  t->code.set(ID_RRfence, true);
303  t->code.set(ID_RWfence, true);
304  t->code.set(ID_WRfence, true);
305  t->code.set(ID_WWcumul, true);
306  t->code.set(ID_RWcumul, true);
307  t->code.set(ID_RRcumul, true);
308  t->code.set(ID_WRcumul, true);
309  }
310  else if(command == ID_lwsync) // Power
311  {
313  t->source_location = code.source_location();
314  t->code = codet(ID_fence);
315  t->code.add_source_location() = code.source_location();
316  t->code.set(ID_WWfence, true);
317  t->code.set(ID_RRfence, true);
318  t->code.set(ID_RWfence, true);
319  t->code.set(ID_WWcumul, true);
320  t->code.set(ID_RWcumul, true);
321  t->code.set(ID_RRcumul, true);
322  }
323  else if(command == ID_isync) // Power
324  {
326  t->source_location = code.source_location();
327  t->code = codet(ID_fence);
328  t->code.add_source_location() = code.source_location();
329  // doesn't do anything by itself,
330  // needs to be combined with branch
331  }
332  else if(command == "dmb" || command == "dsb") // ARM
333  {
335  t->source_location = code.source_location();
336  t->code = codet(ID_fence);
337  t->code.add_source_location() = code.source_location();
338  t->code.set(ID_WWfence, true);
339  t->code.set(ID_RRfence, true);
340  t->code.set(ID_RWfence, true);
341  t->code.set(ID_WRfence, true);
342  t->code.set(ID_WWcumul, true);
343  t->code.set(ID_RWcumul, true);
344  t->code.set(ID_RRcumul, true);
345  t->code.set(ID_WRcumul, true);
346  }
347  else if(command == "isb") // ARM
348  {
350  t->source_location = code.source_location();
351  t->code = codet(ID_fence);
352  t->code.add_source_location() = 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  ae->source_location = code.source_location();
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  ab->source_location = code.source_location();
440 
442  t->source_location = code.source_location();
443  t->code = codet(ID_fence);
444  t->code.add_source_location() = code.source_location();
445  t->code.set(ID_WWfence, true);
446  t->code.set(ID_RRfence, true);
447  t->code.set(ID_RWfence, true);
448  t->code.set(ID_WRfence, true);
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  ae->source_location = code.source_location();
467 
468  x86_32_locked_atomic = false;
469  }
470  }
471 
472  if(unknown)
473  {
474  // we give up; we should perhaps print a warning
475  }
476  else
477  dest.destructive_append(tmp_dest);
478 }
479 
485  goto_functionst::goto_functiont &goto_function)
486 {
487  bool did_something = false;
488 
489  Forall_goto_program_instructions(it, goto_function.body)
490  {
491  if(it->is_other() && it->code.get_statement()==ID_asm)
492  {
493  goto_programt tmp_dest;
494  process_instruction(*it, tmp_dest);
495  it->make_skip();
496  did_something = true;
497 
498  for(auto &instruction : tmp_dest.instructions)
499  instruction.function = it->function;
500 
501  goto_programt::targett next=it;
502  next++;
503 
504  goto_function.body.destructive_insert(next, tmp_dest);
505  }
506  }
507 
508  if(did_something)
509  remove_skip(goto_function.body);
510 }
511 
516 void remove_asm(goto_functionst &goto_functions, symbol_tablet &symbol_table)
517 {
518  remove_asmt rem(symbol_table, goto_functions);
519  rem();
520 }
521 
529 void remove_asm(goto_modelt &goto_model)
530 {
531  remove_asm(goto_model.goto_functions, goto_model.symbol_table);
532 }
Forall_goto_program_instructions
#define Forall_goto_program_instructions(it, program)
Definition: goto_program.h:809
exprt::op2
exprt & op2()
Definition: expr.h:90
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:78
dstringt
dstringt has one field, an unsigned integer no which is an index into a static table of strings.
Definition: dstring.h:35
symbol_tablet
The symbol table.
Definition: symbol_table.h:19
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:485
code_asmt
codet representation of an inline assembler statement.
Definition: std_code.h:1459
pos
literalt pos(literalt a)
Definition: literal.h:193
remove_asmt
Definition: remove_asm.cpp:26
irept::make_nil
void make_nil()
Definition: irep.h:315
typet
The type of an expression, extends irept.
Definition: type.h:27
remove_asmt::goto_functions
goto_functionst & goto_functions
Definition: remove_asm.cpp:42
assembler_parsert::parse
virtual bool parse()
Definition: assembler_parser.h:43
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
to_string_constant
const string_constantt & to_string_constant(const exprt &expr)
Definition: string_constant.h:34
goto_model.h
string_constant.h
goto_modelt
Definition: goto_model.h:24
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
exprt::op0
exprt & op0()
Definition: expr.h:84
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:143
assembler_parser
assembler_parsert assembler_parser
Definition: assembler_parser.cpp:13
code_function_callt::lhs
exprt & lhs()
Definition: std_code.h:1089
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:484
goto_programt::add_instruction
targett add_instruction()
Adds an instruction at the end.
Definition: goto_program.h:541
code_function_callt
codet representation of a function call statement.
Definition: std_code.h:1036
symbolt::mode
irep_idt mode
Language mode.
Definition: symbol.h:49
void_typet
The void type, the same as empty_typet.
Definition: std_types.h:57
parsert::in
std::istream * in
Definition: parser.h:26
id2string
const std::string & id2string(const irep_idt &d)
Definition: irep.h:44
goto_programt::instructiont::code
codet code
Definition: goto_program.h:181
forall_operands
#define forall_operands(it, expr)
Definition: expr.h:20
assembler_parsert::clear
virtual void clear()
Definition: assembler_parser.h:49
nil_exprt
The NIL expression.
Definition: std_expr.h:4461
exprt::op1
exprt & op1()
Definition: expr.h:87
remove_asmt::remove_asmt
remove_asmt(symbol_tablet &_symbol_table, goto_functionst &_goto_functions)
Definition: remove_asm.cpp:29
pointer_type
pointer_typet pointer_type(const typet &subtype)
Definition: c_types.cpp:243
code_typet
Base type of functions.
Definition: std_types.h:751
OTHER
Definition: goto_program.h:37
assembler_parsert::instructions
std::list< instructiont > instructions
Definition: assembler_parser.h:24
code_function_callt::arguments
argumentst & arguments()
Definition: std_code.h:1109
goto_programt::destructive_append
void destructive_append(goto_programt &p)
Appends the given program p to *this. p is destroyed.
Definition: goto_program.h:524
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:1490
symbol_table_baset::add
bool add(const symbolt &symbol)
Add a new symbol to the symbol table.
Definition: symbol_table_base.cpp:18
goto_programt::instructions
instructionst instructions
The list of instructions in the goto program.
Definition: goto_program.h:420
goto_functionst
A collection of goto functions.
Definition: goto_functions.h:22
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:32
code_typet::make_ellipsis
void make_ellipsis()
Definition: std_types.h:873
symbolt
Symbol table entry.
Definition: symbol.h:27
irept::set
void set(const irep_namet &name, const irep_idt &value)
Definition: irep.h:286
assembler_parser.h
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:516
FUNCTION_CALL
Definition: goto_program.h:49
goto_programt
A generic container class for the GOTO intermediate representation of one function.
Definition: goto_program.h:72
ATOMIC_END
Definition: goto_program.h:44
remove_asmt::operator()
void operator()()
Definition: remove_asm.cpp:34
ATOMIC_BEGIN
Definition: goto_program.h:43
address_of_exprt
Operator to return the address of an object.
Definition: std_expr.h:3255
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:146
code_asmt::get_flavor
const irep_idt & get_flavor() const
Definition: std_code.h:1471
typecast_exprt
Semantic type conversion.
Definition: std_expr.h:2277
remove_asmt::symbol_table
symbol_tablet & symbol_table
Definition: remove_asm.cpp:41
remove_skip.h
goto_programt::instructiont
This class represents an instruction in the GOTO intermediate representation.
Definition: goto_program.h:178
exprt::source_location
const source_locationt & source_location() const
Definition: expr.h:228
goto_modelt::symbol_table
symbol_tablet symbol_table
Symbol table.
Definition: goto_model.h:29
c_types.h
symbolt::name
irep_idt name
The unique identifier.
Definition: symbol.h:40
goto_programt::targett
instructionst::iterator targett
Definition: goto_program.h:414
code_function_callt::function
exprt & function()
Definition: std_code.h:1099
remove_asmt::gcc_asm_function_call
void gcc_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 gcc-style inline assembly statement.
Definition: remove_asm.cpp:72
remove_asmt::process_instruction_gcc
void process_instruction_gcc(const code_asmt &, goto_programt &dest)
Translates the given inline assembly code (in gcc style) to non-assembly goto program instructions.
Definition: remove_asm.cpp:216
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:195
codet
Data structure for representing an arbitrary statement in a program.
Definition: std_code.h:34