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/cmdline.h>
17 #include <util/config.h>
18 #include <util/unicode.h>
19 
20 #include "language.h"
21 #include "mode.h"
22 
25  const cmdlinet &cmdline,
26  ui_message_handlert &_ui_message_handler):
27  _cmdline(cmdline),
28  ui_message_handler(_ui_message_handler)
29 {
31 }
32 
35 {
36 }
37 
39 {
40  for(const auto &filename : _cmdline.args)
41  if(parse(filename))
42  return true;
43 
44  return false;
45 }
46 
47 bool language_uit::parse(const std::string &filename)
48 {
49  #ifdef _MSC_VER
50  std::ifstream infile(widen(filename));
51  #else
52  std::ifstream infile(filename);
53  #endif
54 
55  if(!infile)
56  {
57  error() << "failed to open input file `" << filename << "'" << eom;
58  return true;
59  }
60 
63 
64  if(lf.language==nullptr)
65  {
66  source_locationt location;
67  location.set_file(filename);
68  error().source_location=location;
69  error() << "failed to figure out type of file" << eom;
70  return true;
71  }
72 
73  languaget &language=*lf.language;
76 
77  status() << "Parsing " << filename << eom;
78 
79  if(language.parse(infile, filename))
80  {
82  std::cerr << "PARSING ERROR\n";
83 
84  return true;
85  }
86 
87  lf.get_modules();
88 
89  return false;
90 }
91 
93 {
94  status() << "Converting" << eom;
95 
97 
99  {
100  error() << "CONVERSION ERROR" << eom;
101  return true;
102  }
103 
104  return false;
105 }
106 
108 {
110 
111  // Enable/disable stub generation for opaque methods
112  bool stubs_enabled=_cmdline.isset("generate-opaque-stubs");
114 
116  {
117  error() << "CONVERSION ERROR" << eom;
118  return true;
119  }
120 
122 
123  return false;
124 }
125 
127 {
128  switch(get_ui())
129  {
131  show_symbol_table_plain(std::cout, brief);
132  break;
133 
136  break;
137 
138  default:
139  error() << "cannot show symbol table in this format" << eom;
140  }
141 }
142 
144 {
145  error() << "cannot show symbol table in this format" << eom;
146 }
147 
149  std::ostream &out,
150  bool brief)
151 {
152  if(!brief)
153  out << "\nSymbols:\n\n";
154 
155  // we want to sort alphabetically
156  std::set<std::string> symbols;
157 
158  for(const auto &symbol_pair : symbol_table.symbols)
159  {
160  symbols.insert(id2string(symbol_pair.first));
161  }
162 
163  const namespacet ns(symbol_table);
164 
165  for(const std::string &id : symbols)
166  {
167  const symbolt &symbol=ns.lookup(id);
168 
169  std::unique_ptr<languaget> ptr;
170 
171  if(symbol.mode=="")
172  {
173  ptr=get_default_language();
174  }
175  else
176  {
177  ptr=get_language_from_mode(symbol.mode);
178  }
179 
180  if(!ptr)
181  throw "symbol "+id2string(symbol.name)+" has unknown mode";
182 
183  std::string type_str, value_str;
184 
185  if(symbol.type.is_not_nil())
186  ptr->from_type(symbol.type, type_str, ns);
187 
188  if(symbol.value.is_not_nil())
189  ptr->from_expr(symbol.value, value_str, ns);
190 
191  if(brief)
192  {
193  out << symbol.name << " " << type_str << '\n';
194  continue;
195  }
196 
197  out << "Symbol......: " << symbol.name << '\n' << std::flush;
198  out << "Pretty name.: " << symbol.pretty_name << '\n';
199  out << "Module......: " << symbol.module << '\n';
200  out << "Base name...: " << symbol.base_name << '\n';
201  out << "Mode........: " << symbol.mode << '\n';
202  out << "Type........: " << type_str << '\n';
203  out << "Value.......: " << value_str << '\n';
204  out << "Flags.......:";
205 
206  if(symbol.is_lvalue)
207  out << " lvalue";
208  if(symbol.is_static_lifetime)
209  out << " static_lifetime";
210  if(symbol.is_thread_local)
211  out << " thread_local";
212  if(symbol.is_file_local)
213  out << " file_local";
214  if(symbol.is_type)
215  out << " type";
216  if(symbol.is_extern)
217  out << " extern";
218  if(symbol.is_input)
219  out << " input";
220  if(symbol.is_output)
221  out << " output";
222  if(symbol.is_macro)
223  out << " macro";
224  if(symbol.is_parameter)
225  out << " parameter";
226  if(symbol.is_auxiliary)
227  out << " auxiliary";
228  if(symbol.is_weak)
229  out << " weak";
230  if(symbol.is_property)
231  out << " property";
232  if(symbol.is_state_var)
233  out << " state_var";
234  if(symbol.is_exported)
235  out << " exported";
236  if(symbol.is_volatile)
237  out << " volatile";
238 
239  out << '\n';
240  out << "Location....: " << symbol.location << '\n';
241 
242  out << '\n' << std::flush;
243  }
244 }
symbol_tablet symbol_table
Definition: language_ui.h:25
irep_idt name
The unique identifier.
Definition: symbol.h:43
bool is_output
Definition: symbol.h:63
virtual ~language_uit()
Destructor.
Definition: language_ui.cpp:34
const std::string & id2string(const irep_idt &d)
Definition: irep.h:43
bool is_not_nil() const
Definition: irep.h:103
bool is_thread_local
Definition: symbol.h:67
bool final(symbol_table_baset &symbol_table)
virtual bool parse()
Definition: language_ui.cpp:38
std::wstring widen(const char *s)
Definition: unicode.cpp:56
irep_idt mode
Language mode.
Definition: symbol.h:52
std::unique_ptr< languaget > get_default_language()
Returns the default language.
Definition: mode.cpp:138
virtual void get_language_options(const cmdlinet &)
Definition: language.h:43
std::unique_ptr< languaget > get_language_from_mode(const irep_idt &mode)
Get the language corresponding to the given mode.
Definition: mode.cpp:50
uit get_ui()
Definition: language_ui.h:48
language_filest language_files
Definition: language_ui.h:24
language_filet & add_file(const std::string &filename)
Definition: language_file.h:76
exprt value
Initial value of symbol.
Definition: symbol.h:37
irep_idt module
Name of module the symbol belongs to.
Definition: symbol.h:46
virtual bool typecheck()
Definition: language_ui.cpp:92
irep_idt pretty_name
Language-specific display name.
Definition: symbol.h:55
const cmdlinet & _cmdline
Definition: language_ui.h:54
virtual void show_symbol_table(bool brief=false)
std::unique_ptr< languaget > get_language_from_filename(const std::string &filename)
Get the language corresponding to the registered file name extensions.
Definition: mode.cpp:101
Symbol table entry.This is a symbol in the symbol table, stored in an object of type symbol_tablet...
Definition: symbol.h:30
static mstreamt & eom(mstreamt &m)
Definition: message.h:272
configt config
Definition: config.cpp:23
bool is_static_lifetime
Definition: symbol.h:67
bool is_input
Definition: symbol.h:63
virtual void show_symbol_table_xml_ui(bool brief)
std::unique_ptr< languaget > language
Definition: language_file.h:46
argst args
Definition: cmdline.h:37
virtual bool isset(char option) const
Definition: cmdline.cpp:27
bool is_exported
Definition: symbol.h:63
language_uit(const cmdlinet &cmdline, ui_message_handlert &ui_message_handler)
Constructor.
Definition: language_ui.cpp:24
bool is_parameter
Definition: symbol.h:68
source_locationt source_location
Definition: message.h:214
void set_file(const irep_idt &file)
ui_message_handlert & ui_message_handler
Definition: language_ui.h:55
mstreamt & error() const
Definition: message.h:302
TO_BE_DOCUMENTED.
Definition: namespace.h:74
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:148
void set_should_generate_opaque_method_stubs(bool stubs_enabled)
Turn on or off stub generation for all the languages.
const symbolst & symbols
bool is_volatile
Definition: symbol.h:68
bool is_extern
Definition: symbol.h:68
virtual bool from_type(const typet &type, std::string &code, const namespacet &ns)
Formats the given type in a language-specific way.
Definition: language.cpp:46
virtual void show_symbol_table_plain(std::ostream &out, bool brief)
typet type
Type of symbol.
Definition: symbol.h:34
source_locationt location
Source code location of definition of symbol.
Definition: symbol.h:40
virtual bool final()
message_handlert & get_message_handler()
Definition: message.h:153
mstreamt & status() const
Definition: message.h:317
bool is_state_var
Definition: symbol.h:63
irep_idt base_name
Base (non-scoped) name.
Definition: symbol.h:49
bool is_file_local
Definition: symbol.h:68
bool is_weak
Definition: symbol.h:68
bool is_auxiliary
Definition: symbol.h:68
virtual bool from_expr(const exprt &expr, std::string &code, const namespacet &ns)
Formats the given expression in a language-specific way.
Definition: language.cpp:37
bool is_type
Definition: symbol.h:63
virtual bool parse(std::istream &instream, const std::string &path)=0
bool is_property
Definition: symbol.h:63
message_handlert * message_handler
Definition: message.h:342
bool is_macro
Definition: symbol.h:63
bool lookup(const irep_idt &name, const symbolt *&symbol) const override
See namespace_baset::lookup().
Definition: namespace.cpp:130
void set_object_bits_from_symbol_table(const symbol_tablet &)
Sets the number of bits used for object addresses.
Definition: config.cpp:1177
bool is_lvalue
Definition: symbol.h:68