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  explicit remove_asmt(symbol_tablet &_symbol_table)
29  : symbol_table(_symbol_table)
30  {
31  }
32 
34 
35 protected:
37 
39  goto_programt::instructiont &instruction,
40  goto_programt &dest);
41 
43  const irep_idt &function_base_name,
44  const codet &code,
45  goto_programt &dest);
46 };
47 
49  const irep_idt &function_base_name,
50  const codet &code,
51  goto_programt &dest)
52 {
53  irep_idt function_identifier=function_base_name;
54 
55  code_function_callt function_call;
56  function_call.lhs().make_nil();
57 
58  const typet void_pointer=
60 
61  // outputs
62  forall_operands(it, code.op1())
63  {
64  if(it->operands().size()==2)
65  {
66  function_call.arguments().push_back(
67  typecast_exprt(address_of_exprt(it->op1()), void_pointer));
68  }
69  }
70 
71  // inputs
72  forall_operands(it, code.op2())
73  {
74  if(it->operands().size()==2)
75  {
76  function_call.arguments().push_back(
77  typecast_exprt(address_of_exprt(it->op1()), void_pointer));
78  }
79  }
80 
81  code_typet fkt_type({}, void_typet());
82  fkt_type.make_ellipsis();
83 
84  symbol_exprt fkt(function_identifier, fkt_type);
85 
86  function_call.function()=fkt;
87 
89  call->code=function_call;
90  call->source_location=code.source_location();
91 
92  // do we have it?
93  if(!symbol_table.has_symbol(function_identifier))
94  {
95  symbolt symbol;
96 
97  symbol.name=function_identifier;
98  symbol.type=fkt_type;
99  symbol.base_name=function_base_name;
100  symbol.value=nil_exprt();
101 
102  symbol_table.add(symbol);
103  }
104 }
105 
108  goto_programt::instructiont &instruction,
109  goto_programt &dest)
110 {
111  const code_asmt &code=to_code_asm(instruction.code);
112 
113  const irep_idt &flavor=code.get_flavor();
114 
115  if(flavor==ID_gcc)
116  {
117  const irep_idt &i_str=
118  to_string_constant(code.op0()).get_value();
119 
120  // std::cout << "DOING " << i_str << '\n';
121 
122  std::istringstream str(id2string(i_str));
124  assembler_parser.in=&str;
126 
127  goto_programt tmp_dest;
128  bool unknown=false;
129  bool x86_32_locked_atomic=false;
130 
131  for(const auto &instruction : assembler_parser.instructions)
132  {
133  if(instruction.empty())
134  continue;
135 
136  #if 0
137  std::cout << "A ********************\n";
138  for(const auto &ins : instruction)
139  {
140  std::cout << "XX: " << ins.pretty() << '\n';
141  }
142 
143  std::cout << "B ********************\n";
144  #endif
145 
146  // deal with prefixes
147  irep_idt command;
148  unsigned pos=0;
149 
150  if(instruction.front().id()==ID_symbol &&
151  instruction.front().get(ID_identifier)=="lock")
152  {
153  x86_32_locked_atomic=true;
154  pos++;
155  }
156 
157  // done?
158  if(pos==instruction.size())
159  continue;
160 
161  if(instruction[pos].id()==ID_symbol)
162  {
163  command=instruction[pos].get(ID_identifier);
164  pos++;
165  }
166 
167  if(command=="xchg" || command=="xchgl")
168  x86_32_locked_atomic=true;
169 
170  if(x86_32_locked_atomic)
171  {
173  ab->source_location=code.source_location();
174 
176  t->source_location=code.source_location();
177  t->code=codet(ID_fence);
178  t->code.add_source_location()=code.source_location();
179  t->code.set(ID_WWfence, true);
180  t->code.set(ID_RRfence, true);
181  t->code.set(ID_RWfence, true);
182  t->code.set(ID_WRfence, true);
183  }
184 
185  if(command=="fstcw" ||
186  command=="fnstcw" ||
187  command=="fldcw") // x86
188  {
189  gcc_asm_function_call("__asm_"+id2string(command), code, tmp_dest);
190  }
191  else if(command=="mfence" ||
192  command=="lfence" ||
193  command=="sfence") // x86
194  {
195  gcc_asm_function_call("__asm_"+id2string(command), code, tmp_dest);
196  }
197  else if(command == ID_sync) // Power
198  {
200  t->source_location=code.source_location();
201  t->code=codet(ID_fence);
202  t->code.add_source_location()=code.source_location();
203  t->code.set(ID_WWfence, true);
204  t->code.set(ID_RRfence, true);
205  t->code.set(ID_RWfence, true);
206  t->code.set(ID_WRfence, true);
207  t->code.set(ID_WWcumul, true);
208  t->code.set(ID_RWcumul, true);
209  t->code.set(ID_RRcumul, true);
210  t->code.set(ID_WRcumul, true);
211  }
212  else if(command == ID_lwsync) // Power
213  {
215  t->source_location=code.source_location();
216  t->code=codet(ID_fence);
217  t->code.add_source_location()=code.source_location();
218  t->code.set(ID_WWfence, true);
219  t->code.set(ID_RRfence, true);
220  t->code.set(ID_RWfence, true);
221  t->code.set(ID_WWcumul, true);
222  t->code.set(ID_RWcumul, true);
223  t->code.set(ID_RRcumul, true);
224  }
225  else if(command == ID_isync) // Power
226  {
228  t->source_location=code.source_location();
229  t->code=codet(ID_fence);
230  t->code.add_source_location()=code.source_location();
231  // doesn't do anything by itself,
232  // needs to be combined with branch
233  }
234  else if(command=="dmb" || command=="dsb") // ARM
235  {
237  t->source_location=code.source_location();
238  t->code=codet(ID_fence);
239  t->code.add_source_location()=code.source_location();
240  t->code.set(ID_WWfence, true);
241  t->code.set(ID_RRfence, true);
242  t->code.set(ID_RWfence, true);
243  t->code.set(ID_WRfence, true);
244  t->code.set(ID_WWcumul, true);
245  t->code.set(ID_RWcumul, true);
246  t->code.set(ID_RRcumul, true);
247  t->code.set(ID_WRcumul, true);
248  }
249  else if(command=="isb") // ARM
250  {
252  t->source_location=code.source_location();
253  t->code=codet(ID_fence);
254  t->code.add_source_location()=code.source_location();
255  // doesn't do anything by itself,
256  // needs to be combined with branch
257  }
258  else
259  unknown=true; // give up
260 
261  if(x86_32_locked_atomic)
262  {
264  ae->source_location=code.source_location();
265 
266  x86_32_locked_atomic=false;
267  }
268  }
269 
270  if(unknown)
271  {
272  // we give up; we should perhaps print a warning
273  }
274  else
275  dest.destructive_append(tmp_dest);
276  }
277 }
278 
281  goto_functionst::goto_functiont &goto_function)
282 {
283  bool did_something = false;
284 
285  Forall_goto_program_instructions(it, goto_function.body)
286  {
287  if(it->is_other() && it->code.get_statement()==ID_asm)
288  {
289  goto_programt tmp_dest;
290  process_instruction(*it, tmp_dest);
291  it->make_skip();
292  did_something = true;
293 
294  goto_programt::targett next=it;
295  next++;
296 
297  goto_function.body.destructive_insert(next, tmp_dest);
298  }
299  }
300 
301  if(did_something)
302  remove_skip(goto_function.body);
303 }
304 
307  goto_functionst::goto_functiont &goto_function,
308  symbol_tablet &symbol_table)
309 {
310  remove_asmt rem(symbol_table);
311  rem.process_function(goto_function);
312 }
313 
315 void remove_asm(goto_functionst &goto_functions, symbol_tablet &symbol_table)
316 {
317  remove_asmt rem(symbol_table);
318  for(auto &f : goto_functions.function_map)
319  rem.process_function(f.second);
320 }
321 
323 void remove_asm(goto_modelt &goto_model)
324 {
325  remove_asm(goto_model.goto_functions, goto_model.symbol_table);
326 }
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:43
pointer_typet pointer_type(const typet &subtype)
Definition: c_types.cpp:243
exprt & op0()
Definition: expr.h:72
std::istream * in
Definition: parser.h:26
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:1155
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
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()
void gcc_asm_function_call(const irep_idt &function_base_name, const codet &code, goto_programt &dest)
Definition: remove_asm.cpp:48
Symbol Table + CFG.
argumentst & arguments()
Definition: std_code.h:860
symbol_tablet & symbol_table
Definition: remove_asm.cpp:36
instructionst::iterator targett
Definition: goto_program.h:397
The NIL expression.
Definition: std_expr.h:4510
void process_function(goto_functionst::goto_functiont &)
removes assembler
Definition: remove_asm.cpp:280
exprt & op1()
Definition: expr.h:75
The symbol table.
Definition: symbol_table.h:19
::goto_functiont goto_functiont
void process_instruction(goto_programt::instructiont &instruction, goto_programt &dest)
removes assembler
Definition: remove_asm.cpp:107
A function call.
Definition: std_code.h:828
#define forall_operands(it, expr)
Definition: expr.h:17
Operator to return the address of an object.
Definition: std_expr.h:3170
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
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:848
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:1143
void make_nil()
Definition: irep.h:243
#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.
code_asmt & to_code_asm(codet &code)
Definition: std_code.h:1174
goto_functionst goto_functions
GOTO functions.
Definition: goto_model.h:32
void set(const irep_namet &name, const irep_idt &value)
Definition: irep.h:214
remove_asmt(symbol_tablet &_symbol_table)
Definition: remove_asm.cpp:28
void remove_asm(goto_functionst::goto_functiont &goto_function, symbol_tablet &symbol_table)
removes assembler
Definition: remove_asm.cpp:306