cprover
read_goto_object.cpp
Go to the documentation of this file.
1 /*******************************************************************\
2 
3 Module: Read goto object files.
4 
5 Author: CM Wintersteiger
6 
7 Date: June 2006
8 
9 \*******************************************************************/
10 
13 
14 #include "read_goto_object.h"
15 
16 #include <xmllang/xml_parser.h>
17 #include <util/namespace.h>
18 #include <util/base_type.h>
19 #include <util/message.h>
20 
21 #define XML_VERSION "1.4"
22 
23 #include <langapi/mode.h>
24 
26 #include "xml_irep_hashing.h"
27 #include "xml_symbol_hashing.h"
28 
33  std::istream &in,
34  const std::string &filename,
35  symbol_tablet &symbol_table,
36  goto_functionst &functions,
37  message_handlert &message_handler)
38 {
39  messaget message(message_handler);
40 
41  xml_parser.clear();
42  xml_parser.filename = filename;
43  xml_parser.in = &in;
44  xml_parser.set_message_handler(message_handler);
45 
46  if(xml_parser.parse())
47  return true;
48 
50 
51  if(top.get_attribute("version")!=XML_VERSION)
52  {
53  message.error() <<
54  "The input was compiled with a different version of "
55  "goto-cc, please recompile." << messaget::eom;
56  return true;
57  }
58 
60  xml_irep_convertt irepconverter(ic);
61  xml_symbol_convertt symbolconverter(ic);
62  xml_goto_function_convertt gfconverter(ic);
63 
64  if(top.name.substr(0, 11)=="goto-object")
65  {
66  for(xmlt::elementst::const_iterator
67  sec_it=top.elements.begin();
68  sec_it != top.elements.end();
69  sec_it++)
70  {
71  xmlt sec = *sec_it;
72  if(sec.name=="irep_hash_map")
73  {
74  for(xmlt::elementst::const_iterator
75  irep_it = sec.elements.begin();
76  irep_it != sec.elements.end();
77  irep_it++)
78  {
79  irept i;
80  irepconverter.convert(*irep_it, i);
81  irepconverter.insert(irep_it->get_attribute("id"), i);
82  }
83  }
84  else if(sec.name=="symbols")
85  {
86  for(xmlt::elementst::const_iterator
87  sym_it = sec.elements.begin();
88  sym_it != sec.elements.end();
89  sym_it++)
90  {
91  symbolt symbol;
92  symbolconverter.convert(*sym_it, symbol);
93  // std::cout << "Adding Symbol: " << symbol.name << '\n';
94  if(!symbol.is_type &&
95  symbol.type.id()=="code")
96  {
97  // makes sure there is an empty function
98  // for this symbol. if we got code for it,
99  // it will be added later on.
100  functions.function_map[symbol.name].type=
101  to_code_type(symbol.type);
102  }
103  symbol_table.add(symbol);
104  }
105  }
106  else if(sec.name=="functions")
107  {
108  for(xmlt::elementst::const_iterator
109  fun_it = sec.elements.begin();
110  fun_it != sec.elements.end();
111  fun_it++)
112  {
113  std::string fname = fun_it->get_attribute("name");
114  // std::cout << "Adding function body: " << fname << '\n';
115  goto_functionst::goto_functiont &f = functions.function_map[fname];
116  gfconverter.convert(*fun_it, f);
117  }
118  }
119  else
120  {
121  message.error() << "Unknown Section '" << sec.name
122  << "' in object file." << messaget::eom;
123  return true;
124  }
125  }
126  }
127  else
128  {
129  message.error() << "no goto-object" << messaget::eom;
130  return true;
131  }
132 
133  xml_parser.clear();
134  return false;
135 }
irep_idt name
The unique identifier.
Definition: symbol.h:46
std::istream * in
Definition: parser.h:26
Read goto object files.
virtual void clear()
Definition: xml_parser.h:42
std::string name
Definition: xml.h:30
Symbol table entry.This is a symbol in the symbol table, stored in an object of type symbol_tablet...
Definition: symbol.h:33
static mstreamt & eom(mstreamt &m)
Definition: message.h:193
XML-irep conversions with hashing.
#define XML_VERSION
std::string get_attribute(const std::string &attribute) const
Definition: xml.h:54
void convert(const xmlt &, goto_functionst::goto_functiont &)
constructs the goto_function according to the information in the xml structure.
void convert(const irept &irep, xmlt &xml)
const irep_idt & id() const
Definition: irep.h:189
elementst elements
Definition: xml.h:33
The symbol table.
Definition: symbol_table.h:52
Definition: xml.h:18
Base class for tree-like data structures with sharing.
Definition: irep.h:87
virtual void set_message_handler(message_handlert &_message_handler)
Definition: message.h:122
bool add(const symbolt &symbol)
Add a new symbol to the symbol table.
goto_function_templatet< goto_programt > goto_functiont
xml_parsert xml_parser
Definition: xml_parser.cpp:15
Convert goto functions into xml structures and back (with irep hashing).
unsigned long insert(unsigned long, const irept &)
inserts an irep into the hashtable
typet type
Type of symbol.
Definition: symbol.h:37
virtual bool parse()
Definition: xml_parser.h:31
const code_typet & to_code_type(const typet &type)
Cast a generic typet to a code_typet.
Definition: std_types.h:884
XML-symbol conversions with irep hashing.
mstreamt & error()
Definition: message.h:223
bool read_goto_object(std::istream &in, const std::string &filename, symbol_tablet &symbol_table, goto_functionst &functions, message_handlert &message_handler)
reads a goto object xml file back into a symbol and a function table
bool is_type
Definition: symbol.h:66
Base Type Computation.
void convert(const symbolt &, xmlt &)
converts a symbol to an xml symbol node
xml_parse_treet parse_tree
Definition: xml_parser.h:22