cprover
xml_goto_program_hashing.cpp
Go to the documentation of this file.
1 /*******************************************************************\
2 
3 Module: Convert goto programs to xml structures and back (with irep
4  hashing)
5 
6 Author: CM Wintersteiger
7 
8 Date: July 2006
9 
10 \*******************************************************************/
11 
14 
16 
17 #include <sstream>
18 #include <iostream>
19 
20 #include "xml_irep_hashing.h"
21 
27  const goto_programt &goto_program,
28  xmlt &xml)
29 {
30  std::stringstream tmp;
31  // std::cout << "TNO: " << goto_program.target_numbers.size() << '\n';
32 
33  for(const auto &inst : goto_program.instructions)
34  {
35  xmlt &ins=xml.new_element("instruction");
36  if(!inst.location.is_nil())
37  {
39  inst.location, ins.new_element("location"));
40  }
41 
42  if(!inst.labels.empty())
43  {
44  xmlt &lbl=ins.new_element("labels");
45  for(goto_programt::instructiont::labelst::const_iterator
46  l_it=inst.labels.begin();
47  l_it!=inst.labels.end();
48  l_it++)
49  {
50  lbl.new_element("label").set_attribute("name", id2string(*l_it));
51  }
52  }
53 
54 
55  if(inst.target_number!=0)
56  {
57  // std::cout << "Targetlabel found!\n";
58  tmp.str("");
59  tmp << inst.target_number;
60  ins.set_attribute("targetlabel", tmp.str());
61  }
62 
63  switch(inst.type)
64  {
65  case GOTO:
66  {
67  ins.name="goto";
68  if(!inst.guard.is_true())
69  {
70  xmlt &g=ins.new_element("guard");
71  irepconverter.reference_convert(inst.guard, g);
72  }
73  xmlt &tgt=ins.new_element("targets");
74  for(goto_programt::instructiont::targetst::const_iterator
75  gt_it=inst.targets.begin();
76  gt_it!=inst.targets.end();
77  gt_it++)
78  {
79  tmp.str("");
80  tmp << (*gt_it)->target_number;
81  tgt.new_element("target").data=tmp.str();
82  }
83  break;
84  }
85 
86  case ASSUME:
87  {
88  ins.name="assume";
89  xmlt &g=ins.new_element("guard");
90  irepconverter.reference_convert(inst.guard, g);
91  const irep_idt &comment=inst.location.get("comment");
92  if(comment!="")
93  ins.new_element("comment").data=id2string(comment);
94  break;
95  }
96 
97  case ASSERT:
98  {
99  ins.name="assert";
100  xmlt &g=ins.new_element("guard");
101  irepconverter.reference_convert(inst.guard, g);
102  const irep_idt &comment=inst.location.get("comment");
103  if(comment!="")
104  ins.new_element("comment").data=id2string(comment);
105  break;
106  }
107 
108  case SKIP:
109  ins.name="skip";
110  break;
111 
112  case END_FUNCTION:
113  ins.name="end_function";
114  break;
115 
116  case LOCATION:
117  ins.name="location";
118  break;
119 
120  case DEAD:
121  ins.name="dead";
122  break;
123 
124  case ATOMIC_BEGIN:
125  ins.name="atomic_begin";
126  break;
127 
128  case ATOMIC_END:
129  ins.name="atomic_end";
130  break;
131 
132  case RETURN:
133  {
134  ins.name="return";
135  xmlt &c=ins.new_element("code");
136  irepconverter.reference_convert(inst.code, c);
137  break;
138  }
139 
140  case OTHER:
141  {
142  ins.name="instruction";
143  xmlt &c=ins.new_element("code");
144  irepconverter.reference_convert(inst.code, c);
145  break;
146  }
147 
148  case ASSIGN:
149  {
150  ins.name="assign";
151  xmlt &c=ins.new_element("code");
152  irepconverter.reference_convert(inst.code, c);
153  break;
154  }
155 
156  case FUNCTION_CALL:
157  {
158  ins.name="functioncall";
159  xmlt &c=ins.new_element("code");
160  irepconverter.reference_convert(inst.code, c);
161  break;
162  }
163 
164  case START_THREAD:
165  {
166  ins.name="thread_start";
167  xmlt &tgt=ins.new_element("targets");
168  if(inst.targets.size()==1)
169  {
170  tmp.str("");
171  tmp << inst.targets.front()->target_number;
172  tgt.new_element("target").data=tmp.str();
173  }
174  break;
175  }
176 
177  case END_THREAD:
178  ins.name="thread_end";
179  break;
180 
181  default:
182  ins.name="unknown";
183  break;
184  }
185 
186  if(inst.function!="")
187  {
188  xmlt &fnc=ins.new_element("function");
189  fnc.data=id2string(inst.function);
190  }
191  }
192 }
193 
199  const xmlt &xml,
200  goto_programt &goto_program)
201 {
202  goto_program.clear();
203  goto_programt::instructionst &instructions=goto_program.instructions;
204 
205  for(const auto &element : xml.elements)
206  {
207  goto_programt::targett inst=goto_program.add_instruction();
208  inst->targets.clear();
209 
210  if(element.name=="goto")
211  {
212  inst->type=GOTO;
213  }
214  else if(element.name=="assume")
215  {
216  inst->type=ASSUME;
217  }
218  else if(element.name=="assert")
219  {
220  inst->type=ASSERT;
221  }
222  else if(element.name=="skip")
223  {
224  inst->type=SKIP;
225  }
226  else if(element.name=="end_function")
227  {
228  inst->type=END_FUNCTION;
229  }
230  else if(element.name=="location")
231  {
232  inst->type=LOCATION;
233  }
234  else if(element.name=="dead")
235  {
236  inst->type=DEAD;
237  }
238  else if(element.name=="atomic_begin")
239  {
240  inst->type=ATOMIC_BEGIN;
241  }
242  else if(element.name=="atomic_end")
243  {
244  inst->type=ATOMIC_END;
245  }
246  else if(element.name=="return")
247  {
248  inst->make_return();
249  }
250  else if(element.name=="instruction") // OTHER
251  {
252  inst->make_other();
253  }
254  else if(element.name=="assign") // OTHER
255  {
256  inst->make_other();
257  inst->type=ASSIGN;
258  }
259  else if(element.name=="functioncall") // OTHER
260  {
261  inst->make_other();
262  inst->type=FUNCTION_CALL;
263  }
264  else if(element.name=="thread_start")
265  {
266  inst->type=START_THREAD;
267  }
268  else if(element.name=="thread_end")
269  {
270  inst->type=END_THREAD;
271  }
272  else
273  {
274  std::cout << "Unknown instruction type encountered ("
275  << element.name << ")\n";
276  return;
277  }
278 
279  xmlt::elementst::const_iterator eit=element.elements.begin();
280  for(const auto &sub : element.elements)
281  {
282  if(sub.name=="location")
283  {
284  irepconverter.convert(*eit, inst->location);
285  irepconverter.resolve_references(inst->location);
286  }
287  else if(sub.name=="variables")
288  {
289  }
290  else if(sub.name=="labels")
291  {
292  xmlt::elementst::const_iterator lit=sub.elements.begin();
293  for(; lit != sub.elements.end(); lit++)
294  {
295  if(lit->name=="label")
296  {
297  std::string ls=lit->get_attribute("name");
298  inst->labels.push_back(ls);
299  }
300  else
301  {
302  std::cout << "Unknown node in labels section.\n";
303  return;
304  }
305  }
306  }
307  else if(sub.name=="guard")
308  {
309  inst->guard.remove("value");
310  irepconverter.convert(*eit, inst->guard);
311  irepconverter.resolve_references(inst->guard);
312  }
313  else if(sub.name=="code")
314  {
315  irepconverter.convert(*eit, inst->code);
316  irepconverter.resolve_references(inst->code);
317  }
318  else if(sub.name=="targets")
319  {
320  // Don't do anything here, we'll need a second run for that
321  }
322  else if(sub.name=="comment")
323  {
324  inst->location.set("comment", sub.data);
325  }
326  else if(sub.name=="function")
327  {
328  inst->function=sub.data;
329  }
330  }
331  }
332 
333  // assign line numbers
334  goto_program.compute_location_numbers();
335 
336  // second run, for targets
337  goto_programt::targett ins_it=instructions.begin();
338  for(const auto &element : xml.elements)
339  {
340  if(ins_it==instructions.end())
341  break;
342 
343  for(const auto &sub : element.elements)
344  {
345  if(sub.name=="targets")
346  {
347  for(const auto &t : sub.elements)
348  {
349  if(t.name=="target")
350  {
352  find_instruction(xml, instructions, t.data);
353  if(tins!=instructions.end())
354  {
355  // Here we insert the iterators that somehow seem
356  // to be strange afterwards (see line 87)
357  ins_it->targets.push_back(tins);
358  }
359  else
360  {
361  std::cout << "Warning: instruction not found when "
362  "resolving target links.\n";
363  }
364  }
365  else
366  {
367  std::cout << "Unknown node in targets section.\n";
368  return;
369  }
370  }
371  }
372  }
373  ins_it++;
374  }
375 
376  // resolve links
377  goto_program.update();
378 
379  // std::cout << "TNI: " << goto_program.target_numbers.size() << '\n';
380 }
381 
388  const xmlt &xml,
389  goto_programt::instructionst &instructions,
390  const std::string &label)
391 {
392  goto_programt::targett ins_it=instructions.begin();
393  for(const auto &element : xml.elements)
394  {
395  if(ins_it==instructions.end())
396  break;
397 
398  if(label==element.get_attribute("targetlabel"))
399  return ins_it;
400  ins_it++;
401  }
402  return instructions.end();
403 }
void update()
Update all indices.
targett add_instruction()
Adds an instruction at the end.
const std::string & id2string(const irep_idt &d)
Definition: irep.h:44
void clear()
Clear the goto program.
std::string comment(const rw_set_baset::entryt &entry, bool write)
Definition: race_check.cpp:115
instructionst instructions
The list of instructions in the goto program.
void compute_location_numbers(unsigned &nr)
Compute location numbers.
std::string name
Definition: xml.h:30
void reference_convert(const irept &irep, xmlt &xml)
xmlt xml(const source_locationt &location)
Definition: xml_expr.cpp:25
void convert(const goto_programt &, xmlt &)
constructs the xml structure according to the goto program and the namespace into the given xml objec...
XML-irep conversions with hashing.
goto_programt::targett find_instruction(const xmlt &, goto_programt::instructionst &, const std::string &)
finds the index of the instruction labelled with the given target label in the given xml-program ...
void resolve_references(const irept &cur)
resolves references to ireps from an irep after reading an irep hash map into memory.
void convert(const irept &irep, xmlt &xml)
elementst elements
Definition: xml.h:33
void set_attribute(const std::string &attribute, unsigned value)
Definition: xml.cpp:174
Definition: xml.h:18
std::string data
Definition: xml.h:30
xmlt & new_element(const std::string &name)
Definition: xml.h:86
A specialization of goto_program_templatet over goto programs in which instructions have codet type...
Definition: goto_program.h:24
Convert goto programs into xml structures and back (with irep hashing)