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=="")
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;
80  ansi_c_parser.cpp98=false; // it's not C++
81  ansi_c_parser.cpp11=false; // it's not C++
83 
85 
86  bool result=ansi_c_parser.parse();
87 
88  if(!result)
89  {
91  ansi_c_parser.set_file(path);
92  ansi_c_parser.in=&i_preprocessed;
95  }
96 
97  // save result
99 
100  // save some memory
102 
103  return result;
104 }
105 
107  symbol_tablet &symbol_table,
108  const std::string &module)
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 
121  remove_internal_symbols(new_symbol_table);
122 
123  if(linking(symbol_table, new_symbol_table, get_message_handler()))
124  return true;
125 
126  return false;
127 }
128 
130  symbol_tablet &symbol_table)
131 {
132  // Note this can happen here because C doesn't currently
133  // support lazy loading at the symbol-table level, and therefore
134  // function bodies have already been populated and external stub
135  // symbols created during the typecheck() phase. If it gains lazy
136  // loading support then stubs will need to be created during
137  // function body parsing, or else generate-stubs moved to the
138  // final phase.
139  generate_opaque_method_stubs(symbol_table);
140  // This creates __CPROVER_start and __CPROVER_initialize:
141  return ansi_c_entry_point(symbol_table, get_message_handler());
142 }
143 
144 void ansi_c_languaget::show_parse(std::ostream &out)
145 {
146  parse_tree.output(out);
147 }
148 
149 std::unique_ptr<languaget> new_ansi_c_language()
150 {
151  return util_make_unique<ansi_c_languaget>();
152 }
153 
155  const exprt &expr,
156  std::string &code,
157  const namespacet &ns)
158 {
159  code=expr2c(expr, ns);
160  return false;
161 }
162 
164  const typet &type,
165  std::string &code,
166  const namespacet &ns)
167 {
168  code=type2c(type, ns);
169  return false;
170 }
171 
173  const typet &type,
174  std::string &name,
175  const namespacet &ns)
176 {
177  name=type2name(type, ns);
178  return false;
179 }
180 
182  const std::string &code,
183  const std::string &module,
184  exprt &expr,
185  const namespacet &ns)
186 {
187  expr.make_nil();
188 
189  // no preprocessing yet...
190 
191  std::istringstream i_preprocessed(
192  "void __my_expression = (void) (\n"+code+"\n);");
193 
194  // parsing
195 
198  ansi_c_parser.in=&i_preprocessed;
203 
204  bool result=ansi_c_parser.parse();
205 
206  if(ansi_c_parser.parse_tree.items.empty())
207  result=true;
208  else
209  {
210  expr=ansi_c_parser.parse_tree.items.front().declarator().value();
211 
212  // typecheck it
214  }
215 
216  // save some memory
218 
219  // now remove that (void) cast
220  if(expr.id()==ID_typecast &&
221  expr.type().id()==ID_empty &&
222  expr.operands().size()==1)
223  expr=expr.op0();
224 
225  return result;
226 }
227 
229 {
230 }
static std::string type2name(const typet &type, const namespacet &ns, symbol_numbert &symbol_number)
Definition: type2name.cpp:95
The type of an expression.
Definition: type.h:22
struct configt::ansi_ct ansi_c
~ansi_c_languaget() override
std::string parse_path
bool ansi_c_typecheck(ansi_c_parse_treet &ansi_c_parse_tree, symbol_tablet &symbol_table, const std::string &module, message_handlert &message_handler)
bool typecheck(symbol_tablet &symbol_table, const std::string &module) override
ansi_c_parse_treet parse_tree
Definition: ansi_c_parser.h:29
exprt & op0()
Definition: expr.h:72
ANSI-C Linking.
std::istream * in
Definition: parser.h:26
ANSI-C Language Type Checking.
ansi_c_parse_treet parse_tree
bool linking(symbol_tablet &dest_symbol_table, symbol_tablet &new_symbol_table, message_handlert &message_handler)
Definition: linking.cpp:1370
typet & type()
Definition: expr.h:56
bool c_preprocess(std::istream &instream, std::ostream &outstream, message_handlert &message_handler)
ANSI-C preprocessing.
bool parse(std::istream &instream, const std::string &path) override
configt config
Definition: config.cpp:23
std::string get_base_name(const std::string &in, bool strip_suffix)
cleans a filename from path and extension
bool to_expr(const std::string &code, const std::string &module, exprt &expr, const namespacet &ns) override
Parses the given string into an expression.
void ansi_c_internal_additions(std::string &code)
void output(std::ostream &out) const
const irep_idt & id() const
Definition: irep.h:189
bool generate_support_functions(symbol_tablet &symbol_table) override
Create language-specific support functions, such as __CPROVER_start, __CPROVER_initialize and languag...
flavourt mode
Definition: config.h:106
virtual bool parse() override
Definition: ansi_c_parser.h:44
void remove_internal_symbols(symbol_tablet &symbol_table)
Removes internal symbols from a symbol table A symbol is EXPORTED if it is a.
void set_file(const irep_idt &file)
Definition: parser.h:85
bool preprocess(std::istream &instream, const std::string &path, std::ostream &outstream) override
ANSI-C preprocessing.
The symbol table.
Definition: symbol_table.h:19
TO_BE_DOCUMENTED.
Definition: namespace.h:74
std::string type2c(const typet &type, const namespacet &ns)
Definition: expr2c.cpp:3975
void ansi_c_scanner_init()
virtual void set_message_handler(message_handlert &_message_handler)
Definition: message.h:148
bool for_has_scope
Definition: config.h:44
bool ansi_c_entry_point(symbol_tablet &symbol_table, message_handlert &message_handler)
bool type_to_name(const typet &type, std::string &name, const namespacet &ns) override
Encodes the given type in a language-specific way.
void show_parse(std::ostream &out) override
bool Float128_type
Definition: config.h:46
Type Naming for C.
message_handlert & get_message_handler()
Definition: message.h:153
mstreamt & result() const
Definition: message.h:312
Base class for all expressions.
Definition: expr.h:42
ansi_c_parsert ansi_c_parser
std::string expr2c(const exprt &expr, const namespacet &ns)
Definition: expr2c.cpp:3967
std::unique_ptr< languaget > new_ansi_c_language()
void make_nil()
Definition: irep.h:243
bool from_type(const typet &type, std::string &code, const namespacet &ns) override
Formats the given type in a language-specific way.
void set_line_no(unsigned _line_no)
Definition: parser.h:80
bool ts_18661_3_Floatn_types
Definition: ansi_c_parser.h:83
void swap(ansi_c_parse_treet &other)
dstringt irep_idt
Definition: irep.h:31
std::set< std::string > extensions() const override
bool from_expr(const exprt &expr, std::string &code, const namespacet &ns) override
Formats the given expression in a language-specific way.
Remove symbols that are internal only.
operandst & operands()
Definition: expr.h:66
void modules_provided(std::set< std::string > &modules) override
virtual void clear() override
Definition: ansi_c_parser.h:49
void generate_opaque_method_stubs(symbol_tablet &symbol_table)
When there are opaque methods (e.g.
Definition: language.cpp:79
bool ts_18661_3_Floatn_types
Definition: config.h:45