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 <fstream>
12 
13 #include <util/config.h>
14 #include <util/get_base_name.h>
15 
16 #include <linking/linking.h>
18 
19 #include "ansi_c_entry_point.h"
20 #include "ansi_c_typecheck.h"
21 #include "ansi_c_parser.h"
22 #include "expr2c.h"
23 #include "c_preprocess.h"
25 #include "type2name.h"
26 
27 std::set<std::string> ansi_c_languaget::extensions() const
28 {
29  return { "c", "i" };
30 }
31 
32 void ansi_c_languaget::modules_provided(std::set<std::string> &modules)
33 {
34  modules.insert(get_base_name(parse_path, true));
35 }
36 
39  std::istream &instream,
40  const std::string &path,
41  std::ostream &outstream)
42 {
43  // stdin?
44  if(path.empty())
45  return c_preprocess(instream, outstream, get_message_handler());
46 
47  return c_preprocess(path, outstream, get_message_handler());
48 }
49 
51  std::istream &instream,
52  const std::string &path)
53 {
54  // store the path
55  parse_path=path;
56 
57  // preprocessing
58  std::ostringstream o_preprocessed;
59 
60  if(preprocess(instream, path, o_preprocessed))
61  return true;
62 
63  std::istringstream i_preprocessed(o_preprocessed.str());
64 
65  // parsing
66 
67  std::string code;
69  std::istringstream codestr(code);
70 
72  ansi_c_parser.set_file(ID_built_in);
73  ansi_c_parser.in=&codestr;
77  ansi_c_parser.cpp98=false; // it's not C++
78  ansi_c_parser.cpp11=false; // it's not C++
80 
82 
83  bool result=ansi_c_parser.parse();
84 
85  if(!result)
86  {
88  ansi_c_parser.set_file(path);
89  ansi_c_parser.in=&i_preprocessed;
92  }
93 
94  // save result
96 
97  // save some memory
99 
100  return result;
101 }
102 
104  symbol_tablet &symbol_table,
105  const std::string &module,
106  const bool keep_file_local)
107 {
108  symbol_tablet new_symbol_table;
109 
110  if(ansi_c_typecheck(
111  parse_tree,
112  new_symbol_table,
113  module,
115  {
116  return true;
117  }
118 
120  new_symbol_table, this->get_message_handler(), keep_file_local);
121 
122  if(linking(symbol_table, new_symbol_table, get_message_handler()))
123  return true;
124 
125  return false;
126 }
127 
129  symbol_tablet &symbol_table)
130 {
131  // This creates __CPROVER_start and __CPROVER_initialize:
132  return ansi_c_entry_point(
133  symbol_table, get_message_handler(), object_factory_params);
134 }
135 
136 void ansi_c_languaget::show_parse(std::ostream &out)
137 {
138  parse_tree.output(out);
139 }
140 
141 std::unique_ptr<languaget> new_ansi_c_language()
142 {
143  return util_make_unique<ansi_c_languaget>();
144 }
145 
147  const exprt &expr,
148  std::string &code,
149  const namespacet &ns)
150 {
151  code=expr2c(expr, ns);
152  return false;
153 }
154 
156  const typet &type,
157  std::string &code,
158  const namespacet &ns)
159 {
160  code=type2c(type, ns);
161  return false;
162 }
163 
165  const typet &type,
166  std::string &name,
167  const namespacet &ns)
168 {
169  name=type2name(type, ns);
170  return false;
171 }
172 
174  const std::string &code,
175  const std::string &,
176  exprt &expr,
177  const namespacet &ns)
178 {
179  expr.make_nil();
180 
181  // no preprocessing yet...
182 
183  std::istringstream i_preprocessed(
184  "void __my_expression = (void) (\n"+code+"\n);");
185 
186  // parsing
187 
190  ansi_c_parser.in=&i_preprocessed;
195 
196  bool result=ansi_c_parser.parse();
197 
198  if(ansi_c_parser.parse_tree.items.empty())
199  result=true;
200  else
201  {
202  expr=ansi_c_parser.parse_tree.items.front().declarator().value();
203 
204  // typecheck it
206  }
207 
208  // save some memory
210 
211  // now remove that (void) cast
212  if(expr.id()==ID_typecast &&
213  expr.type().id()==ID_empty &&
214  expr.operands().size()==1)
215  {
216  expr = to_typecast_expr(expr).op();
217  }
218 
219  return result;
220 }
221 
223 {
224 }
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:80
ansi_c_parse_treet parse_tree
Definition: ansi_c_parser.h:26
virtual void clear() override
Definition: ansi_c_parser.h:45
virtual bool parse() override
Definition: ansi_c_parser.h:40
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:92
const irep_idt & id() const
Definition: irep.h:396
void make_nil()
Definition: irep.h:454
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:91
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:14
The type of an expression, extends irept.
Definition: type.h:29
const exprt & op() const
Definition: std_expr.h:293
configt config
Definition: config.cpp:25
std::string expr2c(const exprt &expr, const namespacet &ns, const expr2c_configurationt &configuration)
Definition: expr2c.cpp:4011
std::string type2c(const typet &type, const namespacet &ns, const expr2c_configurationt &configuration)
Definition: expr2c.cpp:4027
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, const symbol_tablet &new_symbol_table, message_handlert &message_handler)
Merges the symbol table new_symbol_table into dest_symbol_table, renaming symbols from new_symbol_tab...
Definition: linking.cpp:1470
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:1954
bool for_has_scope
Definition: config.h:123
bool ts_18661_3_Floatn_types
Definition: config.h:124
flavourt mode
Definition: config.h:222
static std::string type2name(const typet &type, const namespacet &ns, symbol_numbert &symbol_number)
Definition: type2name.cpp:81
Type Naming for C.