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 <sstream>
18 
19 #include <util/c_types.h>
20 #include <util/std_expr.h>
21 
22 #include <ansi-c/string_constant.h>
24 
26 {
27 public:
28  inline remove_asmt(
29  symbol_tablet &_symbol_table,
30  goto_functionst &_goto_functions):
31  symbol_table(_symbol_table),
32  goto_functions(_goto_functions)
33  {
34  }
35 
36  void operator()();
37 
38 protected:
41 
43  goto_programt::instructiont &instruction,
44  goto_programt &dest);
45 
46  void process_function(
48 
50  const irep_idt &function_base_name,
51  const codet &code,
52  goto_programt &dest);
53 };
54 
56  const irep_idt &function_base_name,
57  const codet &code,
58  goto_programt &dest)
59 {
60  irep_idt function_identifier=function_base_name;
61 
62  code_function_callt function_call;
63  function_call.lhs().make_nil();
64 
65  const typet void_pointer=
67 
68  // outputs
69  forall_operands(it, code.op1())
70  {
71  if(it->operands().size()==2)
72  {
73  function_call.arguments().push_back(
74  typecast_exprt(address_of_exprt(it->op1()), void_pointer));
75  }
76  }
77 
78  // inputs
79  forall_operands(it, code.op2())
80  {
81  if(it->operands().size()==2)
82  {
83  function_call.arguments().push_back(
84  typecast_exprt(address_of_exprt(it->op1()), void_pointer));
85  }
86  }
87 
88  code_typet fkt_type;
89  fkt_type.return_type()=void_typet();
90  fkt_type.make_ellipsis();
91 
92  symbol_exprt fkt(function_identifier, fkt_type);
93 
94  function_call.function()=fkt;
95 
97  call->code=function_call;
98  call->source_location=code.source_location();
99 
100  // do we have it?
101  if(!symbol_table.has_symbol(function_identifier))
102  {
103  symbolt symbol;
104 
105  symbol.name=function_identifier;
106  symbol.type=fkt_type;
107  symbol.base_name=function_base_name;
108  symbol.value=nil_exprt();
109 
110  symbol_table.add(symbol);
111  }
112 }
113 
116  goto_programt::instructiont &instruction,
117  goto_programt &dest)
118 {
119  const code_asmt &code=to_code_asm(instruction.code);
120 
121  const irep_idt &flavor=code.get_flavor();
122 
123  if(flavor==ID_gcc)
124  {
125  const irep_idt &i_str=
126  to_string_constant(code.op0()).get_value();
127 
128  // std::cout << "DOING " << i_str << '\n';
129 
130  std::istringstream str(id2string(i_str));
132  assembler_parser.in=&str;
134 
135  goto_programt tmp_dest;
136  bool unknown=false;
137  bool x86_32_locked_atomic=false;
138 
139  for(const auto &instruction : assembler_parser.instructions)
140  {
141  if(instruction.empty())
142  continue;
143 
144  #if 0
145  std::cout << "A ********************\n";
146  for(const auto &ins : instruction)
147  {
148  std::cout << "XX: " << ins.pretty() << '\n';
149  }
150 
151  std::cout << "B ********************\n";
152  #endif
153 
154  // deal with prefixes
155  irep_idt command;
156  unsigned pos=0;
157 
158  if(instruction.front().id()==ID_symbol &&
159  instruction.front().get(ID_identifier)=="lock")
160  {
161  x86_32_locked_atomic=true;
162  pos++;
163  }
164 
165  // done?
166  if(pos==instruction.size())
167  continue;
168 
169  if(instruction[pos].id()==ID_symbol)
170  {
171  command=instruction[pos].get(ID_identifier);
172  pos++;
173  }
174 
175  if(command=="xchg" || command=="xchgl")
176  x86_32_locked_atomic=true;
177 
178  if(x86_32_locked_atomic)
179  {
181  ab->source_location=code.source_location();
182 
184  t->source_location=code.source_location();
185  t->code=codet(ID_fence);
186  t->code.add_source_location()=code.source_location();
187  t->code.set(ID_WWfence, true);
188  t->code.set(ID_RRfence, true);
189  t->code.set(ID_RWfence, true);
190  t->code.set(ID_WRfence, true);
191  }
192 
193  if(command=="fstcw" ||
194  command=="fnstcw" ||
195  command=="fldcw") // x86
196  {
197  gcc_asm_function_call("__asm_"+id2string(command), code, tmp_dest);
198  }
199  else if(command=="mfence" ||
200  command=="lfence" ||
201  command=="sfence") // x86
202  {
203  gcc_asm_function_call("__asm_"+id2string(command), code, tmp_dest);
204  }
205  else if(command=="sync") // Power
206  {
208  t->source_location=code.source_location();
209  t->code=codet(ID_fence);
210  t->code.add_source_location()=code.source_location();
211  t->code.set(ID_WWfence, true);
212  t->code.set(ID_RRfence, true);
213  t->code.set(ID_RWfence, true);
214  t->code.set(ID_WRfence, true);
215  t->code.set(ID_WWcumul, true);
216  t->code.set(ID_RWcumul, true);
217  t->code.set(ID_RRcumul, true);
218  t->code.set(ID_WRcumul, true);
219  }
220  else if(command=="lwsync") // Power
221  {
223  t->source_location=code.source_location();
224  t->code=codet(ID_fence);
225  t->code.add_source_location()=code.source_location();
226  t->code.set(ID_WWfence, true);
227  t->code.set(ID_RRfence, true);
228  t->code.set(ID_RWfence, true);
229  t->code.set(ID_WWcumul, true);
230  t->code.set(ID_RWcumul, true);
231  t->code.set(ID_RRcumul, true);
232  }
233  else if(command=="isync") // Power
234  {
236  t->source_location=code.source_location();
237  t->code=codet(ID_fence);
238  t->code.add_source_location()=code.source_location();
239  // doesn't do anything by itself,
240  // needs to be combined with branch
241  }
242  else if(command=="dmb" || command=="dsb") // ARM
243  {
245  t->source_location=code.source_location();
246  t->code=codet(ID_fence);
247  t->code.add_source_location()=code.source_location();
248  t->code.set(ID_WWfence, true);
249  t->code.set(ID_RRfence, true);
250  t->code.set(ID_RWfence, true);
251  t->code.set(ID_WRfence, true);
252  t->code.set(ID_WWcumul, true);
253  t->code.set(ID_RWcumul, true);
254  t->code.set(ID_RRcumul, true);
255  t->code.set(ID_WRcumul, true);
256  }
257  else if(command=="isb") // ARM
258  {
260  t->source_location=code.source_location();
261  t->code=codet(ID_fence);
262  t->code.add_source_location()=code.source_location();
263  // doesn't do anything by itself,
264  // needs to be combined with branch
265  }
266  else
267  unknown=true; // give up
268 
269  if(x86_32_locked_atomic)
270  {
272  ae->source_location=code.source_location();
273 
274  x86_32_locked_atomic=false;
275  }
276  }
277 
278  if(unknown)
279  {
280  // we give up; we should perhaps print a warning
281  }
282  else
283  dest.destructive_append(tmp_dest);
284  }
285 }
286 
289  goto_functionst::goto_functiont &goto_function)
290 {
291  Forall_goto_program_instructions(it, goto_function.body)
292  {
293  if(it->is_other() && it->code.get_statement()==ID_asm)
294  {
295  goto_programt tmp_dest;
296  process_instruction(*it, tmp_dest);
297  it->make_skip();
298 
299  goto_programt::targett next=it;
300  next++;
301 
302  goto_function.body.destructive_insert(next, tmp_dest);
303  }
304  }
305 }
306 
309 {
311  {
312  process_function(it->second);
313  }
314 }
315 
318  symbol_tablet &symbol_table,
319  goto_functionst &goto_functions)
320 {
321  remove_asmt(symbol_table, goto_functions)();
322 }
323 
325 void remove_asm(goto_modelt &goto_model)
326 {
327  remove_asmt(goto_model.symbol_table, goto_model.goto_functions)();
328 }
The void type.
Definition: std_types.h:63
The type of an expression.
Definition: type.h:20
irep_idt name
The unique identifier.
Definition: symbol.h:46
semantic type conversion
Definition: std_expr.h:1725
assembler_parsert assembler_parser
targett add_instruction()
Adds an instruction at the end.
Base type of functions.
Definition: std_types.h:734
const std::string & id2string(const irep_idt &d)
Definition: irep.h:44
pointer_typet pointer_type(const typet &subtype)
Definition: c_types.cpp:296
void remove_asm(symbol_tablet &symbol_table, goto_functionst &goto_functions)
removes assembler
Definition: remove_asm.cpp:317
exprt & op0()
Definition: expr.h:84
std::istream * in
Definition: parser.h:26
literalt pos(literalt a)
Definition: literal.h:193
exprt value
Initial value of symbol.
Definition: symbol.h:40
const irep_idt & get_flavor() const
Definition: std_code.h:932
symbol_tablet symbol_table
Definition: goto_model.h:25
Symbol table entry.This is a symbol in the symbol table, stored in an object of type symbol_tablet...
Definition: symbol.h:33
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.
virtual void clear()
void gcc_asm_function_call(const irep_idt &function_base_name, const codet &code, goto_programt &dest)
Definition: remove_asm.cpp:55
argumentst & arguments()
Definition: std_code.h:689
symbol_tablet & symbol_table
Definition: remove_asm.cpp:39
The NIL expression.
Definition: std_expr.h:3764
void process_function(goto_functionst::goto_functiont &)
removes assembler
Definition: remove_asm.cpp:288
API to expression classes.
exprt & op1()
Definition: expr.h:87
The symbol table.
Definition: symbol_table.h:52
void process_instruction(goto_programt::instructiont &instruction, goto_programt &dest)
removes assembler
Definition: remove_asm.cpp:115
A function call.
Definition: std_code.h:657
#define forall_operands(it, expr)
Definition: expr.h:17
goto_functionst & goto_functions
Definition: remove_asm.cpp:40
bool add(const symbolt &symbol)
Add a new symbol to the symbol table.
goto_function_templatet< goto_programt > goto_functiont
Operator to return the address of an object.
Definition: std_expr.h:2593
void make_ellipsis()
Definition: std_types.h:819
A specialization of goto_program_templatet over goto programs in which instructions have codet type...
Definition: goto_program.h:24
typet type
Type of symbol.
Definition: symbol.h:37
virtual bool parse()
const string_constantt & to_string_constant(const exprt &expr)
exprt & function()
Definition: std_code.h:677
irep_idt base_name
Base (non-scoped) name.
Definition: symbol.h:52
std::list< instructiont > instructions
#define Forall_goto_functions(it, functions)
const source_locationt & source_location() const
Definition: expr.h:142
An inline assembler statement.
Definition: std_code.h:920
void operator()()
removes assembler
Definition: remove_asm.cpp:308
void make_nil()
Definition: irep.h:243
bool has_symbol(const irep_idt &name) const
Definition: symbol_table.h:87
#define Forall_goto_program_instructions(it, program)
Definition: goto_program.h:73
Expression to hold a symbol (variable)
Definition: std_expr.h:82
exprt & op2()
Definition: expr.h:90
void destructive_append(goto_program_templatet< codeT, guardT > &p)
Appends the given program, which is destroyed.
A statement in a programming language.
Definition: std_code.h:19
code_asmt & to_code_asm(codet &code)
Definition: std_code.h:943
goto_functionst goto_functions
Definition: goto_model.h:26
const typet & return_type() const
Definition: std_types.h:831
void set(const irep_namet &name, const irep_idt &value)
Definition: irep.h:214