cprover
ansi_c_language.cpp
Go to the documentation of this file.
1 /*******************************************************************\
2 
3 Module:
4 
5 Author: Daniel Kroening, kroening@kroening.com
6 
7 \*******************************************************************/
8 
9 #include "ansi_c_language.h"
10 
11 #include <cstring>
12 #include <sstream>
13 #include <fstream>
14 
15 #include <util/config.h>
16 #include <util/get_base_name.h>
17 
18 #include <linking/linking.h>
20 
21 #include "ansi_c_entry_point.h"
22 #include "ansi_c_typecheck.h"
23 #include "ansi_c_parser.h"
24 #include "expr2c.h"
25 #include "c_preprocess.h"
27 #include "type2name.h"
28 
29 std::set<std::string> ansi_c_languaget::extensions() const
30 {
31  return { "c", "i" };
32 }
33 
34 void ansi_c_languaget::modules_provided(std::set<std::string> &modules)
35 {
36  modules.insert(get_base_name(parse_path, true));
37 }
38 
41  std::istream &instream,
42  const std::string &path,
43  std::ostream &outstream)
44 {
45  // stdin?
46  if(path.empty())
47  return c_preprocess(instream, outstream, get_message_handler());
48 
49  return c_preprocess(path, outstream, get_message_handler());
50 }
51 
53  std::istream &instream,
54  const std::string &path)
55 {
56  // store the path
57  parse_path=path;
58 
59  // preprocessing
60  std::ostringstream o_preprocessed;
61 
62  if(preprocess(instream, path, o_preprocessed))
63  return true;
64 
65  std::istringstream i_preprocessed(o_preprocessed.str());
66 
67  // parsing
68 
69  std::string code;
71  std::istringstream codestr(code);
72 
74  ansi_c_parser.set_file(ID_built_in);
75  ansi_c_parser.in=&codestr;
79  ansi_c_parser.cpp98=false; // it's not C++
80  ansi_c_parser.cpp11=false; // it's not C++
82 
84 
85  bool result=ansi_c_parser.parse();
86 
87  if(!result)
88  {
90  ansi_c_parser.set_file(path);
91  ansi_c_parser.in=&i_preprocessed;
94  }
95 
96  // save result
98 
99  // save some memory
101 
102  return result;
103 }
104 
106  symbol_tablet &symbol_table,
107  const std::string &module,
108  const bool keep_file_local)
109 {
110  symbol_tablet new_symbol_table;
111 
112  if(ansi_c_typecheck(
113  parse_tree,
114  new_symbol_table,
115  module,
117  {
118  return true;
119  }
120 
122  new_symbol_table, this->get_message_handler(), keep_file_local);
123 
124  if(linking(symbol_table, new_symbol_table, get_message_handler()))
125  return true;
126 
127  return false;
128 }
129 
131  symbol_tablet &symbol_table)
132 {
133  // This creates __CPROVER_start and __CPROVER_initialize:
134  return ansi_c_entry_point(
135  symbol_table, get_message_handler(), object_factory_params);
136 }
137 
138 void ansi_c_languaget::show_parse(std::ostream &out)
139 {
140  parse_tree.output(out);
141 }
142 
143 std::unique_ptr<languaget> new_ansi_c_language()
144 {
145  return util_make_unique<ansi_c_languaget>();
146 }
147 
149  const exprt &expr,
150  std::string &code,
151  const namespacet &ns)
152 {
153  code=expr2c(expr, ns);
154  return false;
155 }
156 
158  const typet &type,
159  std::string &code,
160  const namespacet &ns)
161 {
162  code=type2c(type, ns);
163  return false;
164 }
165 
167  const typet &type,
168  std::string &name,
169  const namespacet &ns)
170 {
171  name=type2name(type, ns);
172  return false;
173 }
174 
176  const std::string &code,
177  const std::string &,
178  exprt &expr,
179  const namespacet &ns)
180 {
181  expr.make_nil();
182 
183  // no preprocessing yet...
184 
185  std::istringstream i_preprocessed(
186  "void __my_expression = (void) (\n"+code+"\n);");
187 
188  // parsing
189 
192  ansi_c_parser.in=&i_preprocessed;
197 
198  bool result=ansi_c_parser.parse();
199 
200  if(ansi_c_parser.parse_tree.items.empty())
201  result=true;
202  else
203  {
204  expr=ansi_c_parser.parse_tree.items.front().declarator().value();
205 
206  // typecheck it
208  }
209 
210  // save some memory
212 
213  // now remove that (void) cast
214  if(expr.id()==ID_typecast &&
215  expr.type().id()==ID_empty &&
216  expr.operands().size()==1)
217  {
218  expr = to_typecast_expr(expr).op();
219  }
220 
221  return result;
222 }
223 
225 {
226 }
bool ansi_c_entry_point(symbol_tablet &symbol_table, message_handlert &message_handler, const c_object_factory_parameterst &object_factory_parameters)
void ansi_c_internal_additions(std::string &code)
std::unique_ptr< languaget > new_ansi_c_language()
ansi_c_parsert ansi_c_parser
void ansi_c_scanner_init()
bool ansi_c_typecheck(ansi_c_parse_treet &ansi_c_parse_tree, symbol_tablet &symbol_table, const std::string &module, message_handlert &message_handler)
ANSI-C Language Type Checking.
bool c_preprocess(std::istream &instream, std::ostream &outstream, message_handlert &message_handler)
ANSI-C preprocessing.
bool preprocess(std::istream &instream, const std::string &path, std::ostream &outstream) override
ANSI-C preprocessing.
~ansi_c_languaget() override
std::set< std::string > extensions() const override
bool typecheck(symbol_tablet &symbol_table, const std::string &module, const bool keep_file_local) override
typecheck without removing specified entries from the symbol table
void show_parse(std::ostream &out) override
bool parse(std::istream &instream, const std::string &path) override
bool from_type(const typet &type, std::string &code, const namespacet &ns) override
Formats the given type in a language-specific way.
bool to_expr(const std::string &code, const std::string &module, exprt &expr, const namespacet &ns) override
Parses the given string into an expression.
bool generate_support_functions(symbol_tablet &symbol_table) override
Create language-specific support functions, such as __CPROVER_start, __CPROVER_initialize and languag...
std::string parse_path
bool from_expr(const exprt &expr, std::string &code, const namespacet &ns) override
Formats the given expression in a language-specific way.
void modules_provided(std::set< std::string > &modules) override
bool type_to_name(const typet &type, std::string &name, const namespacet &ns) override
Encodes the given type in a language-specific way.
ansi_c_parse_treet parse_tree
c_object_factory_parameterst object_factory_params
void swap(ansi_c_parse_treet &other)
void output(std::ostream &out) const
bool ts_18661_3_Floatn_types
Definition: ansi_c_parser.h:84
ansi_c_parse_treet parse_tree
Definition: ansi_c_parser.h:29
virtual void clear() override
Definition: ansi_c_parser.h:48
virtual bool parse() override
Definition: ansi_c_parser.h:43
struct configt::ansi_ct ansi_c
Base class for all expressions.
Definition: expr.h:54
typet & type()
Return the type of the expression.
Definition: expr.h:82
operandst & operands()
Definition: expr.h:96
const irep_idt & id() const
Definition: irep.h:407
void make_nil()
Definition: irep.h:464
mstreamt & result() const
Definition: message.h:409
message_handlert & get_message_handler()
Definition: message.h:184
virtual void set_message_handler(message_handlert &_message_handler)
Definition: message.h:179
A namespacet is essentially one or two symbol tables bound together, to allow for symbol lookups in t...
Definition: namespace.h:92
std::istream * in
Definition: parser.h:26
void set_file(const irep_idt &file)
Definition: parser.h:85
void set_line_no(unsigned _line_no)
Definition: parser.h:80
The symbol table.
Definition: symbol_table.h:20
The type of an expression, extends irept.
Definition: type.h:28
const exprt & op() const
Definition: std_expr.h:294
configt config
Definition: config.cpp:24
std::string expr2c(const exprt &expr, const namespacet &ns, const expr2c_configurationt &configuration)
Definition: expr2c.cpp:3921
std::string type2c(const typet &type, const namespacet &ns, const expr2c_configurationt &configuration)
Definition: expr2c.cpp:3937
std::string get_base_name(const std::string &in, bool strip_suffix)
cleans a filename from path and extension
dstringt irep_idt
Definition: irep.h:37
bool linking(symbol_tablet &dest_symbol_table, symbol_tablet &new_symbol_table, message_handlert &message_handler)
Definition: linking.cpp:1437
ANSI-C Linking.
void remove_internal_symbols(symbol_tablet &symbol_table, message_handlert &mh, const bool keep_file_local)
Removes internal symbols from a symbol table A symbol is EXPORTED if it is a.
Remove symbols that are internal only.
const typecast_exprt & to_typecast_expr(const exprt &expr)
Cast an exprt to a typecast_exprt.
Definition: std_expr.h:1815
bool for_has_scope
Definition: config.h:125
bool ts_18661_3_Floatn_types
Definition: config.h:126
flavourt mode
Definition: config.h:196
static std::string type2name(const typet &type, const namespacet &ns, symbol_numbert &symbol_number)
Definition: type2name.cpp:81
Type Naming for C.