cprover
remove_asm.cpp
Go to the documentation of this file.
1 /*******************************************************************\
2 
3 Module: Remove 'asm' statements by compiling into suitable standard
4  code
5 
6 Author: Daniel Kroening
7 
8 Date: December 2014
9 
10 \*******************************************************************/
11 
14 
15 #include "remove_asm.h"
16 
17 #include <util/c_types.h>
18 #include <util/string_constant.h>
19 
21 
22 #include "goto_model.h"
23 #include "remove_skip.h"
24 
26 {
27 public:
28  remove_asmt(symbol_tablet &_symbol_table, goto_functionst &_goto_functions)
29  : symbol_table(_symbol_table), goto_functions(_goto_functions)
30  {
31  }
32 
33  void operator()()
34  {
35  for(auto &f : goto_functions.function_map)
36  process_function(f.second);
37  }
38 
39 protected:
42 
44 
46  goto_programt::instructiont &instruction,
47  goto_programt &dest);
48 
49  void process_instruction_gcc(const code_asmt &, goto_programt &dest);
50 
51  void process_instruction_msc(const code_asmt &, goto_programt &dest);
52 
54  const irep_idt &function_base_name,
55  const code_asmt &code,
56  goto_programt &dest);
57 
59  const irep_idt &function_base_name,
60  const code_asmt &code,
61  goto_programt &dest);
62 };
63 
65  const irep_idt &function_base_name,
66  const code_asmt &code,
67  goto_programt &dest)
68 {
69  irep_idt function_identifier=function_base_name;
70 
71  code_function_callt function_call;
72  function_call.lhs().make_nil();
73 
74  const typet void_pointer=
76 
77  // outputs
78  forall_operands(it, code.op1())
79  {
80  if(it->operands().size()==2)
81  {
82  function_call.arguments().push_back(
83  typecast_exprt(address_of_exprt(it->op1()), void_pointer));
84  }
85  }
86 
87  // inputs
88  forall_operands(it, code.op2())
89  {
90  if(it->operands().size()==2)
91  {
92  function_call.arguments().push_back(
93  typecast_exprt(address_of_exprt(it->op1()), void_pointer));
94  }
95  }
96 
97  code_typet fkt_type({}, void_typet());
98  fkt_type.make_ellipsis();
99 
100  symbol_exprt fkt(function_identifier, fkt_type);
101 
102  function_call.function()=fkt;
103 
105  call->code=function_call;
106  call->source_location=code.source_location();
107 
108  // do we have it?
109  if(!symbol_table.has_symbol(function_identifier))
110  {
111  symbolt symbol;
112 
113  symbol.name=function_identifier;
114  symbol.type=fkt_type;
115  symbol.base_name=function_base_name;
116  symbol.value=nil_exprt();
117  symbol.mode = ID_C;
118 
119  symbol_table.add(symbol);
120  }
121 
122  if(
123  goto_functions.function_map.find(function_identifier) ==
125  {
126  auto &f = goto_functions.function_map[function_identifier];
127  f.type = fkt_type;
128  }
129 }
130 
132  const irep_idt &function_base_name,
133  const code_asmt &code,
134  goto_programt &dest)
135 {
136  irep_idt function_identifier = function_base_name;
137 
138  code_function_callt function_call;
139  function_call.lhs().make_nil();
140 
141  const typet void_pointer = pointer_type(void_typet());
142 
143  code_typet fkt_type({}, void_typet());
144  fkt_type.make_ellipsis();
145 
146  symbol_exprt fkt(function_identifier, fkt_type);
147 
148  function_call.function() = fkt;
149 
151  call->code = function_call;
152  call->source_location = code.source_location();
153 
154  // do we have it?
155  if(!symbol_table.has_symbol(function_identifier))
156  {
157  symbolt symbol;
158 
159  symbol.name = function_identifier;
160  symbol.type = fkt_type;
161  symbol.base_name = function_base_name;
162  symbol.value = nil_exprt();
163  symbol.mode = ID_C;
164 
165  symbol_table.add(symbol);
166  }
167 
168  if(
169  goto_functions.function_map.find(function_identifier) ==
171  {
172  auto &f = goto_functions.function_map[function_identifier];
173  f.type = fkt_type;
174  }
175 }
176 
179  goto_programt::instructiont &instruction,
180  goto_programt &dest)
181 {
182  const code_asmt &code=to_code_asm(instruction.code);
183 
184  const irep_idt &flavor=code.get_flavor();
185 
186  if(flavor==ID_gcc)
187  process_instruction_gcc(code, dest);
188  else if(flavor == ID_msc)
189  process_instruction_msc(code, dest);
190  else
191  DATA_INVARIANT(false, "unexpected assembler flavor");
192 }
193 
196  const code_asmt &code,
197  goto_programt &dest)
198 {
199  const irep_idt &i_str = to_string_constant(code.op0()).get_value();
200 
201  std::istringstream str(id2string(i_str));
203  assembler_parser.in = &str;
205 
206  goto_programt tmp_dest;
207  bool unknown = false;
208  bool x86_32_locked_atomic = false;
209 
210  for(const auto &instruction : assembler_parser.instructions)
211  {
212  if(instruction.empty())
213  continue;
214 
215 #if 0
216  std::cout << "A ********************\n";
217  for(const auto &ins : instruction)
218  {
219  std::cout << "XX: " << ins.pretty() << '\n';
220  }
221 
222  std::cout << "B ********************\n";
223 #endif
224 
225  // deal with prefixes
226  irep_idt command;
227  unsigned pos = 0;
228 
229  if(
230  instruction.front().id() == ID_symbol &&
231  instruction.front().get(ID_identifier) == "lock")
232  {
233  x86_32_locked_atomic = true;
234  pos++;
235  }
236 
237  // done?
238  if(pos == instruction.size())
239  continue;
240 
241  if(instruction[pos].id() == ID_symbol)
242  {
243  command = instruction[pos].get(ID_identifier);
244  pos++;
245  }
246 
247  if(command == "xchg" || command == "xchgl")
248  x86_32_locked_atomic = true;
249 
250  if(x86_32_locked_atomic)
251  {
253  ab->source_location = code.source_location();
254 
256  t->source_location = code.source_location();
257  t->code = codet(ID_fence);
258  t->code.add_source_location() = code.source_location();
259  t->code.set(ID_WWfence, true);
260  t->code.set(ID_RRfence, true);
261  t->code.set(ID_RWfence, true);
262  t->code.set(ID_WRfence, true);
263  }
264 
265  if(command == "fstcw" || command == "fnstcw" || command == "fldcw") // x86
266  {
267  gcc_asm_function_call("__asm_" + id2string(command), code, tmp_dest);
268  }
269  else if(
270  command == "mfence" || command == "lfence" || command == "sfence") // x86
271  {
272  gcc_asm_function_call("__asm_" + id2string(command), code, tmp_dest);
273  }
274  else if(command == ID_sync) // Power
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  t->code.set(ID_WWcumul, true);
285  t->code.set(ID_RWcumul, true);
286  t->code.set(ID_RRcumul, true);
287  t->code.set(ID_WRcumul, true);
288  }
289  else if(command == ID_lwsync) // Power
290  {
292  t->source_location = code.source_location();
293  t->code = codet(ID_fence);
294  t->code.add_source_location() = code.source_location();
295  t->code.set(ID_WWfence, true);
296  t->code.set(ID_RRfence, true);
297  t->code.set(ID_RWfence, true);
298  t->code.set(ID_WWcumul, true);
299  t->code.set(ID_RWcumul, true);
300  t->code.set(ID_RRcumul, true);
301  }
302  else if(command == ID_isync) // Power
303  {
305  t->source_location = code.source_location();
306  t->code = codet(ID_fence);
307  t->code.add_source_location() = code.source_location();
308  // doesn't do anything by itself,
309  // needs to be combined with branch
310  }
311  else if(command == "dmb" || command == "dsb") // ARM
312  {
314  t->source_location = code.source_location();
315  t->code = codet(ID_fence);
316  t->code.add_source_location() = code.source_location();
317  t->code.set(ID_WWfence, true);
318  t->code.set(ID_RRfence, true);
319  t->code.set(ID_RWfence, true);
320  t->code.set(ID_WRfence, true);
321  t->code.set(ID_WWcumul, true);
322  t->code.set(ID_RWcumul, true);
323  t->code.set(ID_RRcumul, true);
324  t->code.set(ID_WRcumul, true);
325  }
326  else if(command == "isb") // ARM
327  {
329  t->source_location = code.source_location();
330  t->code = codet(ID_fence);
331  t->code.add_source_location() = code.source_location();
332  // doesn't do anything by itself,
333  // needs to be combined with branch
334  }
335  else
336  unknown = true; // give up
337 
338  if(x86_32_locked_atomic)
339  {
341  ae->source_location = code.source_location();
342 
343  x86_32_locked_atomic = false;
344  }
345  }
346 
347  if(unknown)
348  {
349  // we give up; we should perhaps print a warning
350  }
351  else
352  dest.destructive_append(tmp_dest);
353 }
354 
357  const code_asmt &code,
358  goto_programt &dest)
359 {
360  const irep_idt &i_str = to_string_constant(code.op0()).get_value();
361 
362  std::istringstream str(id2string(i_str));
364  assembler_parser.in = &str;
366 
367  goto_programt tmp_dest;
368  bool unknown = false;
369  bool x86_32_locked_atomic = false;
370 
371  for(const auto &instruction : assembler_parser.instructions)
372  {
373  if(instruction.empty())
374  continue;
375 
376 #if 0
377  std::cout << "A ********************\n";
378  for(const auto &ins : instruction)
379  {
380  std::cout << "XX: " << ins.pretty() << '\n';
381  }
382 
383  std::cout << "B ********************\n";
384 #endif
385 
386  // deal with prefixes
387  irep_idt command;
388  unsigned pos = 0;
389 
390  if(
391  instruction.front().id() == ID_symbol &&
392  instruction.front().get(ID_identifier) == "lock")
393  {
394  x86_32_locked_atomic = true;
395  pos++;
396  }
397 
398  // done?
399  if(pos == instruction.size())
400  continue;
401 
402  if(instruction[pos].id() == ID_symbol)
403  {
404  command = instruction[pos].get(ID_identifier);
405  pos++;
406  }
407 
408  if(command == "xchg" || command == "xchgl")
409  x86_32_locked_atomic = true;
410 
411  if(x86_32_locked_atomic)
412  {
414  ab->source_location = code.source_location();
415 
417  t->source_location = code.source_location();
418  t->code = codet(ID_fence);
419  t->code.add_source_location() = code.source_location();
420  t->code.set(ID_WWfence, true);
421  t->code.set(ID_RRfence, true);
422  t->code.set(ID_RWfence, true);
423  t->code.set(ID_WRfence, true);
424  }
425 
426  if(command == "fstcw" || command == "fnstcw" || command == "fldcw") // x86
427  {
428  msc_asm_function_call("__asm_" + id2string(command), code, tmp_dest);
429  }
430  else if(
431  command == "mfence" || command == "lfence" || command == "sfence") // x86
432  {
433  msc_asm_function_call("__asm_" + id2string(command), code, tmp_dest);
434  }
435  else
436  unknown = true; // give up
437 
438  if(x86_32_locked_atomic)
439  {
441  ae->source_location = code.source_location();
442 
443  x86_32_locked_atomic = false;
444  }
445  }
446 
447  if(unknown)
448  {
449  // we give up; we should perhaps print a warning
450  }
451  else
452  dest.destructive_append(tmp_dest);
453 }
454 
457  goto_functionst::goto_functiont &goto_function)
458 {
459  bool did_something = false;
460 
461  Forall_goto_program_instructions(it, goto_function.body)
462  {
463  if(it->is_other() && it->code.get_statement()==ID_asm)
464  {
465  goto_programt tmp_dest;
466  process_instruction(*it, tmp_dest);
467  it->make_skip();
468  did_something = true;
469 
470  goto_programt::targett next=it;
471  next++;
472 
473  goto_function.body.destructive_insert(next, tmp_dest);
474  }
475  }
476 
477  if(did_something)
478  remove_skip(goto_function.body);
479 }
480 
482 void remove_asm(goto_functionst &goto_functions, symbol_tablet &symbol_table)
483 {
484  remove_asmt rem(symbol_table, goto_functions);
485  rem();
486 }
487 
489 void remove_asm(goto_modelt &goto_model)
490 {
491  remove_asm(goto_model.goto_functions, goto_model.symbol_table);
492 }
The void type.
Definition: std_types.h:64
The type of an expression.
Definition: type.h:22
irep_idt name
The unique identifier.
Definition: symbol.h:43
semantic type conversion
Definition: std_expr.h:2111
assembler_parsert assembler_parser
Base type of functions.
Definition: std_types.h:764
const std::string & id2string(const irep_idt &d)
Definition: irep.h:44
pointer_typet pointer_type(const typet &subtype)
Definition: c_types.cpp:243
exprt & op0()
Definition: expr.h:72
irep_idt mode
Language mode.
Definition: symbol.h:52
std::istream * in
Definition: parser.h:26
void process_instruction_gcc(const code_asmt &, goto_programt &dest)
removes gcc assembler
Definition: remove_asm.cpp:195
literalt pos(literalt a)
Definition: literal.h:193
void destructive_append(goto_programt &p)
Appends the given program, which is destroyed.
Definition: goto_program.h:486
exprt value
Initial value of symbol.
Definition: symbol.h:37
function_mapt function_map
const irep_idt & get_flavor() const
Definition: std_code.h:1187
symbol_tablet symbol_table
Symbol table.
Definition: goto_model.h:29
Symbol table entry.This is a symbol in the symbol table, stored in an object of type symbol_tablet...
Definition: symbol.h:30
void gcc_asm_function_call(const irep_idt &function_base_name, const code_asmt &code, goto_programt &dest)
Definition: remove_asm.cpp:64
remove_asmt(symbol_tablet &_symbol_table, goto_functionst &_goto_functions)
Definition: remove_asm.cpp:28
Remove &#39;asm&#39; statements by compiling into suitable standard code.
This class represents an instruction in the GOTO intermediate representation.
Definition: goto_program.h:173
virtual void clear()
Symbol Table + CFG.
argumentst & arguments()
Definition: std_code.h:890
symbol_tablet & symbol_table
Definition: remove_asm.cpp:40
instructionst::iterator targett
Definition: goto_program.h:397
The NIL expression.
Definition: std_expr.h:4508
void process_function(goto_functionst::goto_functiont &)
removes assembler
Definition: remove_asm.cpp:456
exprt & op1()
Definition: expr.h:75
The symbol table.
Definition: symbol_table.h:19
::goto_functiont goto_functiont
void msc_asm_function_call(const irep_idt &function_base_name, const code_asmt &code, goto_programt &dest)
Definition: remove_asm.cpp:131
void process_instruction(goto_programt::instructiont &instruction, goto_programt &dest)
removes assembler
Definition: remove_asm.cpp:178
A function call.
Definition: std_code.h:858
#define forall_operands(it, expr)
Definition: expr.h:17
goto_functionst & goto_functions
Definition: remove_asm.cpp:41
dstringt has one field, an unsigned integer no which is an index into a static table of strings...
Definition: dstring.h:33
Operator to return the address of an object.
Definition: std_expr.h:3168
bool has_symbol(const irep_idt &name) const
Check whether a symbol exists in the symbol table.
void make_ellipsis()
Definition: std_types.h:885
A generic container class for the GOTO intermediate representation of one function.
Definition: goto_program.h:70
void remove_asm(goto_functionst &goto_functions, symbol_tablet &symbol_table)
removes assembler
Definition: remove_asm.cpp:482
typet type
Type of symbol.
Definition: symbol.h:34
virtual bool parse()
const string_constantt & to_string_constant(const exprt &expr)
exprt & function()
Definition: std_code.h:878
targett add_instruction()
Adds an instruction at the end.
Definition: goto_program.h:505
irep_idt base_name
Base (non-scoped) name.
Definition: symbol.h:49
void remove_skip(goto_programt &goto_program, goto_programt::targett begin, goto_programt::targett end)
remove unnecessary skip statements
Definition: remove_skip.cpp:86
std::list< instructiont > instructions
const source_locationt & source_location() const
Definition: expr.h:125
An inline assembler statement.
Definition: std_code.h:1175
void operator()()
Definition: remove_asm.cpp:33
void make_nil()
Definition: irep.h:315
#define Forall_goto_program_instructions(it, program)
Definition: goto_program.h:740
Expression to hold a symbol (variable)
Definition: std_expr.h:90
exprt & op2()
Definition: expr.h:78
bool add(const symbolt &symbol)
Add a new symbol to the symbol table.
A statement in a programming language.
Definition: std_code.h:21
Program Transformation.
#define DATA_INVARIANT(CONDITION, REASON)
Definition: invariant.h:278
void process_instruction_msc(const code_asmt &, goto_programt &dest)
removes msc assembler
Definition: remove_asm.cpp:356
code_asmt & to_code_asm(codet &code)
Definition: std_code.h:1206
goto_functionst goto_functions
GOTO functions.
Definition: goto_model.h:32
void set(const irep_namet &name, const irep_idt &value)
Definition: irep.h:286