cprover
xml_goto_program.cpp
Go to the documentation of this file.
1 /*******************************************************************\
2 
3 Module: Convert goto programs to xml structures and back.
4 
5 Author: CM Wintersteiger
6 
7 Date: June 2006
8 
9 \*******************************************************************/
10 
13 
14 #include "xml_goto_program.h"
15 
16 #include <sstream>
17 #include <iostream>
18 
19 #include <util/xml_irep.h>
20 
25 void convert(const goto_programt &goto_program,
26  xmlt &xml)
27 {
28  std::stringstream tmp;
29  // std::cout << "TNO: " << goto_program.target_numbers.size() << '\n';
30 
31  for(const auto &inst : goto_program.instructions)
32  {
33  xmlt &ins=xml.new_element("instruction");
34 
35  if(!inst.location.is_nil())
36  {
37  convert(inst.location, ins.new_element("location"));
38  }
39 
40  if(!inst.labels.empty())
41  {
42  xmlt &lbl=ins.new_element("labels");
43  for(goto_programt::instructiont::labelst::const_iterator
44  l_it=inst.labels.begin();
45  l_it!=inst.labels.end();
46  l_it++)
47  {
48  lbl.new_element("label").set_attribute("name", id2string(*l_it));
49  }
50  }
51 
52 
53  if(inst.target_number!=0)
54  {
55  // std::cout << "Targetlabel found!\n";
56  tmp.str("");
57  tmp << inst.target_number;
58  ins.set_attribute("targetlabel", tmp.str());
59  }
60 
61  switch(inst.type)
62  {
63  case GOTO:
64  {
65  ins.name="goto";
66  if(!inst.guard.is_true())
67  {
68  xmlt &g=ins.new_element("guard");
69  convert(inst.guard, g);
70  }
71  xmlt &tgt=ins.new_element("targets");
72  for(goto_programt::instructiont::targetst::const_iterator
73  gt_it=inst.targets.begin();
74  gt_it!=inst.targets.end();
75  gt_it++)
76  {
77  tmp.str("");
78  tmp << (*gt_it)->target_number;
79  tgt.new_element("target").data=tmp.str();
80  }
81  break;
82  }
83 
84  case ASSUME:
85  {
86  ins.name="assume";
87  xmlt &g=ins.new_element("guard");
88  convert(inst.guard, g);
89 
90  const irep_idt &comment=inst.location.get("comment");
91 
92  if(comment!="")
93  ins.new_element("comment").data=id2string(comment);
94 
95  break;
96  }
97 
98  case ASSERT:
99  {
100  ins.name="assert";
101  xmlt &g=ins.new_element("guard");
102  convert(inst.guard, g);
103  const irep_idt &comment=inst.location.get("comment");
104 
105  if(comment!="")
106  ins.new_element("comment").data=id2string(comment);
107 
108  break;
109  }
110 
111  case SKIP:
112  ins.name="skip";
113  break;
114 
115  case END_FUNCTION:
116  ins.name="end_function";
117  break;
118 
119  case LOCATION:
120  ins.name="location";
121  break;
122 
123  case DEAD:
124  ins.name="dead";
125  break;
126 
127  case ATOMIC_BEGIN:
128  ins.name="atomic_begin";
129  break;
130 
131  case ATOMIC_END:
132  ins.name="atomic_end";
133  break;
134 
135  case RETURN:
136  {
137  ins.name="return";
138  xmlt &c=ins.new_element("code");
139  convert(inst.code, c);
140  break;
141  }
142 
143  case OTHER:
144  {
145  ins.name="instruction";
146  xmlt &c=ins.new_element("code");
147  convert(inst.code, c);
148  break;
149  }
150 
151  case ASSIGN:
152  {
153  ins.name="assign";
154  xmlt &c=ins.new_element("code");
155  convert(inst.code, c);
156  break;
157  }
158 
159  case FUNCTION_CALL:
160  {
161  ins.name="functioncall";
162  xmlt &c=ins.new_element("code");
163  convert(inst.code, c);
164  break;
165  }
166 
167  case START_THREAD:
168  {
169  ins.name="thread_start";
170  xmlt &tgt=ins.new_element("targets");
171  if(inst.targets.size()==1)
172  {
173  tmp.str("");
174  tmp << inst.targets.front()->target_number;
175  tgt.new_element("target").data=tmp.str();
176  }
177  break;
178  }
179 
180  case END_THREAD:
181  ins.name="thread_end";
182  break;
183 
184  default:
185  ins.name="unknown";
186  break;
187  }
188 
189  if(inst.function!="")
190  {
191  xmlt &fnc=ins.new_element("function");
192  fnc.data=id2string(inst.function);
193  }
194  }
195 }
196 
202 void convert(const xmlt &xml, goto_programt &goto_program)
203 {
204  goto_program.clear();
205  goto_programt::instructionst &instructions = goto_program.instructions;
206 
207  xmlt::elementst::const_iterator it = xml.elements.begin();
208  for(; it != xml.elements.end(); it++)
209  {
210  goto_programt::targett inst = goto_program.add_instruction();
211  inst->targets.clear();
212 
213  if(it->name=="goto")
214  {
215  inst->type = GOTO;
216  }
217  else if(it->name=="assume")
218  {
219  inst->type = ASSUME;
220  }
221  else if(it->name=="assert")
222  {
223  inst->type = ASSERT;
224  }
225  else if(it->name=="skip")
226  {
227  inst->type = SKIP;
228  }
229  else if(it->name=="end_function")
230  {
231  inst->type = END_FUNCTION;
232  }
233  else if(it->name=="location")
234  {
235  inst->type = LOCATION;
236  }
237  else if(it->name=="dead")
238  {
239  inst->type = DEAD;
240  }
241  else if(it->name=="atomic_begin")
242  {
243  inst->type = ATOMIC_BEGIN;
244  }
245  else if(it->name=="atomic_end")
246  {
247  inst->type = ATOMIC_END;
248  }
249  else if(it->name=="return")
250  {
251  inst->make_return();
252  }
253  else if(it->name=="instruction") // OTHER
254  {
255  inst->make_other();
256  }
257  else if(it->name=="assign")
258  {
259  inst->make_other();
260  inst->type=ASSIGN;
261  }
262  else if(it->name=="functioncall")
263  {
264  inst->make_other();
265  inst->type=FUNCTION_CALL;
266  }
267  else if(it->name=="thread_start")
268  {
269  inst->type = START_THREAD;
270  }
271  else if(it->name=="thread_end")
272  {
273  inst->type = END_THREAD;
274  }
275  else
276  {
277  std::cout << "Unknown instruction type encountered (" << it->name
278  << ")\n";
279  return;
280  }
281 
282  xmlt::elementst::const_iterator eit = it->elements.begin();
283  for(; eit != it->elements.end(); eit++)
284  {
285  if(eit->name=="location")
286  {
287  convert(*eit, inst->location);
288  }
289  else if(eit->name=="variables")
290  {
291  }
292  else if(eit->name=="labels")
293  {
294  xmlt::elementst::const_iterator lit = eit->elements.begin();
295  for(; lit != eit->elements.end(); lit++)
296  {
297  if(lit->name=="label")
298  {
299  std::string ls = lit->get_attribute("name");
300  inst->labels.push_back(ls);
301  }
302  else
303  {
304  std::cout << "Unknown node in labels section.\n";
305  return;
306  }
307  }
308  }
309  else if(eit->name=="guard")
310  {
311  inst->guard.remove("value");
312  convert(*eit, inst->guard);
313  }
314  else if(eit->name=="code")
315  {
316  convert(*eit, inst->code);
317  }
318  else if(eit->name=="targets")
319  {
320  // Don't do anything here, we'll need a second run for that
321  }
322  else if(eit->name=="comment")
323  {
324  inst->location.set("comment", eit->data);
325  }
326  else if(eit->name=="function")
327  {
328  inst->function = eit->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  it = xml.elements.begin();
339  for(; it != xml.elements.end() && ins_it!=instructions.end(); it++)
340  {
341  xmlt::elementst::const_iterator eit = it->elements.begin();
342  for(; eit != it->elements.end(); eit++)
343  {
344  if(eit->name=="targets")
345  {
346  xmlt::elementst::const_iterator tit = eit->elements.begin();
347  for(; tit != eit->elements.end(); tit++)
348  {
349  if(tit->name=="target")
350  {
352  find_instruction(xml, instructions, tit->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 
389  const xmlt &xml,
390  goto_programt::instructionst &instructions,
391  const irep_idt &label)
392 {
393  goto_programt::targett ins_it=instructions.begin();
394  xmlt::elementst::const_iterator it=xml.elements.begin();
395 
396  for(; it != xml.elements.end() && ins_it!=instructions.end(); it++)
397  {
398  if(label==it->get_attribute("targetlabel"))
399  return ins_it;
400 
401  ins_it++;
402  }
403 
404  return instructions.end();
405 }
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
xmlt xml(const source_locationt &location)
Definition: xml_expr.cpp:25
elementst elements
Definition: xml.h:33
void set_attribute(const std::string &attribute, unsigned value)
Definition: xml.cpp:174
Definition: xml.h:18
goto_programt::targett find_instruction(const xmlt &xml, goto_programt::instructionst &instructions, const irep_idt &label)
finds the index of the instruction labelled with the given target label in the given xml-program ...
std::string data
Definition: xml.h:30
Convert goto programs into xml structures and back.
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
void convert(const goto_programt &goto_program, xmlt &xml)
constructs the xml structure according to the goto program and the namespace into the given xml objec...