cprover
language_ui.cpp
Go to the documentation of this file.
1 /*******************************************************************\
2 
3 Module:
4 
5 Author: Daniel Kroening, kroening@cs.cmu.edu
6 
7 \*******************************************************************/
8 
9 #include "language_ui.h"
10 
11 #include <fstream>
12 #include <memory>
13 #include <iostream>
14 
15 #include <util/namespace.h>
16 #include <util/language.h>
17 #include <util/cmdline.h>
18 #include <util/unicode.h>
19 
20 #include "mode.h"
21 
24  const cmdlinet &cmdline,
25  ui_message_handlert &_ui_message_handler):
26  _cmdline(cmdline),
27  ui_message_handler(_ui_message_handler)
28 {
30 }
31 
34 {
35 }
36 
38 {
39  for(unsigned i=0; i<_cmdline.args.size(); i++)
40  {
41  if(parse(_cmdline.args[i]))
42  return true;
43  }
44 
45  return false;
46 }
47 
48 bool language_uit::parse(const std::string &filename)
49 {
50  #ifdef _MSC_VER
51  std::ifstream infile(widen(filename));
52  #else
53  std::ifstream infile(filename);
54  #endif
55 
56  if(!infile)
57  {
58  error() << "failed to open input file `" << filename << "'" << eom;
59  return true;
60  }
61 
62  std::pair<language_filest::file_mapt::iterator, bool>
64  std::pair<std::string, language_filet>(filename, language_filet()));
65 
66  language_filet &lf=result.first->second;
67 
68  lf.filename=filename;
70 
71  if(lf.language==nullptr)
72  {
73  source_locationt location;
74  location.set_file(filename);
75  error().source_location=location;
76  error() << "failed to figure out type of file" << eom;
77  return true;
78  }
79 
80  languaget &language=*lf.language;
83 
84  status() << "Parsing " << filename << eom;
85 
86  if(language.parse(infile, filename))
87  {
89  std::cerr << "PARSING ERROR\n";
90 
91  return true;
92  }
93 
94  lf.get_modules();
95 
96  return false;
97 }
98 
100 {
101  status() << "Converting" << eom;
102 
104 
106  {
107  error() << "CONVERSION ERROR" << eom;
108  return true;
109  }
110 
111  return false;
112 }
113 
115 {
117 
119  {
120  error() << "CONVERSION ERROR" << eom;
121  return true;
122  }
123 
124  return false;
125 }
126 
128 {
129  switch(get_ui())
130  {
132  show_symbol_table_plain(std::cout, brief);
133  break;
134 
137  break;
138 
139  default:
140  error() << "cannot show symbol table in this format" << eom;
141  }
142 }
143 
145 {
146  error() << "cannot show symbol table in this format" << eom;
147 }
148 
150  std::ostream &out,
151  bool brief)
152 {
153  if(!brief)
154  out << "\nSymbols:\n\n";
155 
156  // we want to sort alphabetically
157  std::set<std::string> symbols;
158 
160  symbols.insert(id2string(it->first));
161 
162  const namespacet ns(symbol_table);
163 
164  for(const std::string &id : symbols)
165  {
166  const symbolt &symbol=ns.lookup(id);
167 
168  languaget *ptr;
169 
170  if(symbol.mode=="")
171  ptr=get_default_language();
172  else
173  {
174  ptr=get_language_from_mode(symbol.mode);
175  if(ptr==nullptr)
176  throw "symbol "+id2string(symbol.name)+" has unknown mode";
177  }
178 
179  std::unique_ptr<languaget> p(ptr);
180  std::string type_str, value_str;
181 
182  if(symbol.type.is_not_nil())
183  p->from_type(symbol.type, type_str, ns);
184 
185  if(symbol.value.is_not_nil())
186  p->from_expr(symbol.value, value_str, ns);
187 
188  if(brief)
189  {
190  out << symbol.name << " " << type_str << '\n';
191  continue;
192  }
193 
194  out << "Symbol......: " << symbol.name << '\n' << std::flush;
195  out << "Pretty name.: " << symbol.pretty_name << '\n';
196  out << "Module......: " << symbol.module << '\n';
197  out << "Base name...: " << symbol.base_name << '\n';
198  out << "Mode........: " << symbol.mode << '\n';
199  out << "Type........: " << type_str << '\n';
200  out << "Value.......: " << value_str << '\n';
201  out << "Flags.......:";
202 
203  if(symbol.is_lvalue)
204  out << " lvalue";
205  if(symbol.is_static_lifetime)
206  out << " static_lifetime";
207  if(symbol.is_thread_local)
208  out << " thread_local";
209  if(symbol.is_file_local)
210  out << " file_local";
211  if(symbol.is_type)
212  out << " type";
213  if(symbol.is_extern)
214  out << " extern";
215  if(symbol.is_input)
216  out << " input";
217  if(symbol.is_output)
218  out << " output";
219  if(symbol.is_macro)
220  out << " macro";
221  if(symbol.is_parameter)
222  out << " parameter";
223  if(symbol.is_auxiliary)
224  out << " auxiliary";
225  if(symbol.is_weak)
226  out << " weak";
227  if(symbol.is_property)
228  out << " property";
229  if(symbol.is_state_var)
230  out << " state_var";
231  if(symbol.is_exported)
232  out << " exported";
233  if(symbol.is_volatile)
234  out << " volatile";
235 
236  out << '\n';
237  out << "Location....: " << symbol.location << '\n';
238 
239  out << '\n' << std::flush;
240  }
241 }
symbol_tablet symbol_table
Definition: language_ui.h:24
irep_idt name
The unique identifier.
Definition: symbol.h:46
mstreamt & result()
Definition: message.h:233
virtual bool lookup(const irep_idt &name, const symbolt *&symbol) const
Definition: namespace.cpp:139
bool is_output
Definition: symbol.h:66
virtual ~language_uit()
Destructor.
Definition: language_ui.cpp:33
const std::string & id2string(const irep_idt &d)
Definition: irep.h:44
bool is_not_nil() const
Definition: irep.h:104
bool is_thread_local
Definition: symbol.h:70
virtual bool parse()
Definition: language_ui.cpp:37
#define forall_symbols(it, expr)
Definition: symbol_table.h:28
std::wstring widen(const char *s)
Definition: unicode.cpp:56
irep_idt mode
Language mode.
Definition: symbol.h:55
languaget * language
Definition: language_file.h:41
mstreamt & status()
Definition: message.h:238
virtual void get_language_options(const cmdlinet &)
Definition: language.h:31
uit get_ui()
Definition: language_ui.h:47
language_filest language_files
Definition: language_ui.h:23
exprt value
Initial value of symbol.
Definition: symbol.h:40
irep_idt module
Name of module the symbol belongs to.
Definition: symbol.h:49
virtual bool typecheck()
Definition: language_ui.cpp:99
irep_idt pretty_name
Language-specific display name.
Definition: symbol.h:58
const cmdlinet & _cmdline
Definition: language_ui.h:53
virtual void show_symbol_table(bool brief=false)
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
bool is_static_lifetime
Definition: symbol.h:70
bool is_input
Definition: symbol.h:66
virtual void show_symbol_table_xml_ui(bool brief)
argst args
Definition: cmdline.h:35
symbolst symbols
Definition: symbol_table.h:57
bool is_exported
Definition: symbol.h:66
language_uit(const cmdlinet &cmdline, ui_message_handlert &ui_message_handler)
Constructor.
Definition: language_ui.cpp:23
bool is_parameter
Definition: symbol.h:71
source_locationt source_location
Definition: message.h:175
void set_file(const irep_idt &file)
ui_message_handlert & ui_message_handler
Definition: language_ui.h:54
TO_BE_DOCUMENTED.
Definition: namespace.h:62
Abstract interface to support a programming language.
bool typecheck(symbol_tablet &symbol_table)
virtual void set_message_handler(message_handlert &_message_handler)
Definition: message.h:122
languaget * get_default_language()
Definition: mode.cpp:85
bool is_volatile
Definition: symbol.h:71
bool final(symbol_tablet &symbol_table)
bool is_extern
Definition: symbol.h:71
virtual bool from_type(const typet &type, std::string &code, const namespacet &ns)
Definition: language.cpp:41
virtual void show_symbol_table_plain(std::ostream &out, bool brief)
typet type
Type of symbol.
Definition: symbol.h:37
source_locationt location
Source code location of definition of symbol.
Definition: symbol.h:43
virtual bool final()
message_handlert & get_message_handler()
Definition: message.h:127
languaget * get_language_from_mode(const irep_idt &mode)
Definition: mode.cpp:40
bool is_state_var
Definition: symbol.h:66
languaget * get_language_from_filename(const std::string &filename)
Definition: mode.cpp:51
irep_idt base_name
Base (non-scoped) name.
Definition: symbol.h:52
file_mapt file_map
Definition: language_file.h:63
bool is_file_local
Definition: symbol.h:71
std::string filename
Definition: language_file.h:42
mstreamt & error()
Definition: message.h:223
bool is_weak
Definition: symbol.h:71
bool is_auxiliary
Definition: symbol.h:71
virtual bool from_expr(const exprt &expr, std::string &code, const namespacet &ns)
Definition: language.cpp:32
bool is_type
Definition: symbol.h:66
virtual bool parse(std::istream &instream, const std::string &path)=0
bool is_property
Definition: symbol.h:66
message_handlert * message_handler
Definition: message.h:259
bool is_macro
Definition: symbol.h:66
bool is_lvalue
Definition: symbol.h:71