cprover
xml_irep_hashing.cpp
Go to the documentation of this file.
1 /*******************************************************************\
2 
3 Module: XML-irep conversions with hashing
4 
5 Author: CM Wintersteiger
6 
7 Date: July 2006
8 
9 \*******************************************************************/
10 
13 
14 #include "xml_irep_hashing.h"
15 
16 #include <sstream>
17 #include <iostream>
18 
19 #include "string_hash.h"
20 
22  const irept &irep,
23  xmlt &xml)
24 {
25  if(irep.id()!="nil")
26  xml.new_element("id").data=irep.id_string();
27 
28  forall_irep(it, irep.get_sub())
29  {
30  xmlt &x_sub=xml.new_element("s");
31  reference_convert(*it, x_sub);
32  }
33 
35  {
36  xmlt &x_nsub=xml.new_element("ns");
37  x_nsub.set_attribute("n", name2string(it->first));
38  reference_convert(it->second, x_nsub);
39  }
40 
42  {
43  xmlt &x_com=xml.new_element("c");
44  x_com.set_attribute("n", name2string(it->first));
45  reference_convert(it->second, x_com);
46  }
47 }
48 
50  const xmlt &xml,
51  irept &irep)
52 {
53  irep.id("nil");
54  xmlt::elementst::const_iterator it=xml.elements.begin();
55  for(; it != xml.elements.end(); it++)
56  {
57  if(it->name=="R")
58  {
59  irep.id("__REFERENCE__");
60  irep.set("REF", it->data);
61  }
62  else if(it->name=="id")
63  {
64  irep.id(it->data);
65  }
66  else if(it->name=="ns")
67  {
68  irept r;
69  convert(*it, r);
70  std::string named_name=it->get_attribute("n");
71  irep.move_to_named_sub(named_name, r);
72  }
73  else if(it->name=="s")
74  {
75  irept r;
76  convert(*it, r);
77  irep.move_to_sub(r);
78  }
79  else if(it->name=="c")
80  {
81  irept r;
82  convert(*it, r);
83  std::string named_name=it->get_attribute("n");
84  irep.move_to_named_sub(named_name, r);
85  }
86  else
87  {
88  // Should not happen
89  std::cout << "Unknown sub found (" << it->name << "); malformed xml?\n";
90  }
91  }
92 }
93 
95  const irept &irep,
96  xmlt &xml)
97 {
98  xmlt &ir=xml.new_element("R");
99 
100  ireps_containert::content_containert::const_iterator fi=
101  find_irep_by_content(irep);
102  if(fi==ireps_container.content_container.end())
103  {
105  ir.data=long_to_string(id);
106  }
107  else
108  {
109  ir.data=
111  }
112 }
113 
114 unsigned long xml_irep_convertt::add_with_childs(const irept &iwi)
115 {
116  unsigned long id=insert((unsigned long)&iwi, iwi);
117  if(id!=(unsigned long)&iwi)
118  return id;
119 
120  forall_irep(it, iwi.get_sub())
121  {
122  ireps_containert::content_containert::const_iterator fi=
124  if(fi==ireps_container.content_container.end())
125  {
126  add_with_childs(*it);
127  }
128  }
129  forall_named_irep(it, iwi.get_named_sub())
130  {
131  ireps_containert::content_containert::const_iterator fi=
132  find_irep_by_content(it->second);
133  if(fi==ireps_container.content_container.end())
134  {
135  add_with_childs(it->second);
136  }
137  }
138  forall_named_irep(it, iwi.get_comments())
139  {
140  ireps_containert::content_containert::const_iterator fi=
141  find_irep_by_content(it->second);
142  if(fi==ireps_container.content_container.end())
143  {
144  add_with_childs(it->second);
145  }
146  }
147  return id;
148 }
149 
154 {
155  if(cur.id() == "__REFERENCE__")
156  {
157  unsigned long id=string_to_long(cur.get_string("REF"));
158  ireps_containert::id_containert::const_iterator itr=find_irep_by_id(id);
159  if(itr==ireps_container.id_container.end())
160  {
161  std::cout << "Warning: can't resolve irep reference (sub "
162  << cur.get("REF") << ")\n";
163  }
164  else
165  {
166  irept &curX=const_cast<irept&>(cur);
167  curX=itr->second;
168  }
169  }
170 
171  forall_irep(iti, cur.get_sub())
172  resolve_references(*iti);
173 
174  forall_named_irep(iti, cur.get_named_sub())
175  resolve_references(iti->second);
176 
177  forall_named_irep(iti, cur.get_comments())
178  resolve_references(iti->second);
179 }
180 
184 std::string xml_irep_convertt::long_to_string(const unsigned long l)
185 {
186  std::stringstream s;
187  s << std::hex << l;
188  return s.str();
189 }
190 
195 unsigned long xml_irep_convertt::string_to_long(const std::string &s)
196 {
197  std::stringstream ss(s);
198  unsigned long res=0;
199  ss >> std::hex >> res;
200  return res;
201 }
202 
206 xml_irep_convertt::ireps_containert::id_containert::const_iterator
207  xml_irep_convertt::find_irep_by_id(const unsigned int id)
208 {
209  return ireps_container.id_container.find(id);
210 }
211 
215 xml_irep_convertt::ireps_containert::content_containert::const_iterator
217 {
218  return ireps_container.content_container.find(irep);
219 }
220 
225  unsigned long id,
226  const irept &i)
227 {
228  ireps_containert::content_containert::const_iterator sit;
229  sit=find_irep_by_content(i);
230  if(sit==ireps_container.content_container.end())
231  {
233  std::pair<irept, unsigned long>(i, id));
234 
235  if(ireps_container.id_container.insert(
236  std::pair<unsigned long, irept>(id, i)).second)
237  {
240  }
241 
242  return id;
243  }
244  else
245  {
246  return sit->second;
247  }
248 }
249 
254  const std::string &id,
255  const irept &i)
256 {
257  return insert(string_to_long(id), i);
258 }
259 
264 {
265  ireps_containert::id_containert::iterator hit=
267  for(; hit!=ireps_container.id_container.end(); hit++)
268  {
269  xmlt &xmlhe=xml.new_element("irep");
270  xmlhe.set_attribute(
271  "id",
273  convert(hit->second, xmlhe);
274  }
275 }
276 
281 void xml_irep_convertt::output_map(std::ostream &out, unsigned indent)
282 {
283  ireps_containert::id_containert::iterator hit=
285  for(; hit!=ireps_container.id_container.end(); hit++)
286  {
287  xmlt xmlhe("irep");
288  xmlhe.set_attribute(
289  "id",
291  convert(hit->second, xmlhe);
292  xmlhe.output(out, indent);
293  }
294 }
static int8_t r
Definition: irep_hash.h:59
unsigned long string_to_long(const std::string &)
converts the string to an unsigned long that used to give a pointer to an irep in an old compilation ...
ireps_containert::content_containert::const_iterator find_irep_by_content(const irept &irep)
finds an irep in the ireps hash set by checking contents
void move_to_sub(irept &irep)
Definition: irep.cpp:204
void convert_map(xmlt &xml)
converts the current hash map of ireps into the given xml structure
ireps_containert::id_containert::const_iterator find_irep_by_id(const unsigned int)
finds an irep in the ireps hash set by its id
void reference_convert(const irept &irep, xmlt &xml)
#define forall_named_irep(it, irep)
Definition: irep.h:70
xmlt xml(const source_locationt &location)
Definition: xml_expr.cpp:25
XML-irep conversions with hashing.
subt & get_sub()
Definition: irep.h:245
ireps_containert & ireps_container
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)
const irep_idt & id() const
Definition: irep.h:189
elementst elements
Definition: xml.h:33
const std::string & name2string(const irep_namet &n)
Definition: irep.h:53
void set_attribute(const std::string &attribute, unsigned value)
Definition: xml.cpp:174
const irep_idt & get(const irep_namet &name) const
Definition: irep.cpp:213
Definition: xml.h:18
named_subt & get_comments()
Definition: irep.h:249
Base class for tree-like data structures with sharing.
Definition: irep.h:87
std::string data
Definition: xml.h:30
xmlt & new_element(const std::string &name)
Definition: xml.h:86
unsigned long insert(unsigned long, const irept &)
inserts an irep into the hashtable
named_subt & get_named_sub()
Definition: irep.h:247
const std::string & get_string(const irep_namet &name) const
Definition: irep.h:202
const std::string & id_string() const
Definition: irep.h:192
string hashing
unsigned long add_with_childs(const irept &)
std::string long_to_string(const unsigned long)
converts the hash value to a readable string
void set(const irep_namet &name, const irep_idt &value)
Definition: irep.h:214
void move_to_named_sub(const irep_namet &name, irept &irep)
Definition: irep.cpp:195
void output_map(std::ostream &out, unsigned indent)
converts the current hash map of ireps into xml nodes and outputs them to the stream ...
#define forall_irep(it, irep)
Definition: irep.h:62
void output(std::ostream &out, unsigned indent=0) const
Definition: xml.cpp:31