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  // This creates __CPROVER_start and __CPROVER_initialize:
133  return ansi_c_entry_point(
134  symbol_table, get_message_handler(), object_factory_params);
135 }
136 
137 void ansi_c_languaget::show_parse(std::ostream &out)
138 {
139  parse_tree.output(out);
140 }
141 
142 std::unique_ptr<languaget> new_ansi_c_language()
143 {
144  return util_make_unique<ansi_c_languaget>();
145 }
146 
148  const exprt &expr,
149  std::string &code,
150  const namespacet &ns)
151 {
152  code=expr2c(expr, ns);
153  return false;
154 }
155 
157  const typet &type,
158  std::string &code,
159  const namespacet &ns)
160 {
161  code=type2c(type, ns);
162  return false;
163 }
164 
166  const typet &type,
167  std::string &name,
168  const namespacet &ns)
169 {
170  name=type2name(type, ns);
171  return false;
172 }
173 
175  const std::string &code,
176  const std::string &,
177  exprt &expr,
178  const namespacet &ns)
179 {
180  expr.make_nil();
181 
182  // no preprocessing yet...
183 
184  std::istringstream i_preprocessed(
185  "void __my_expression = (void) (\n"+code+"\n);");
186 
187  // parsing
188 
191  ansi_c_parser.in=&i_preprocessed;
196 
197  bool result=ansi_c_parser.parse();
198 
199  if(ansi_c_parser.parse_tree.items.empty())
200  result=true;
201  else
202  {
203  expr=ansi_c_parser.parse_tree.items.front().declarator().value();
204 
205  // typecheck it
207  }
208 
209  // save some memory
211 
212  // now remove that (void) cast
213  if(expr.id()==ID_typecast &&
214  expr.type().id()==ID_empty &&
215  expr.operands().size()==1)
216  expr=expr.op0();
217 
218  return result;
219 }
220 
222 {
223 }
ansi_c_parser
ansi_c_parsert ansi_c_parser
Definition: ansi_c_parser.cpp:13
configt::ansi_ct::ts_18661_3_Floatn_types
bool ts_18661_3_Floatn_types
Definition: config.h:45
get_base_name
std::string get_base_name(const std::string &in, bool strip_suffix)
cleans a filename from path and extension
Definition: get_base_name.cpp:16
symbol_tablet
The symbol table.
Definition: symbol_table.h:19
ansi_c_typecheck.h
ansi_c_languaget::type_to_name
bool type_to_name(const typet &type, std::string &name, const namespacet &ns) override
Encodes the given type in a language-specific way.
Definition: ansi_c_language.cpp:165
configt::ansi_ct::for_has_scope
bool for_has_scope
Definition: config.h:44
ansi_c_entry_point.h
irept::make_nil
void make_nil()
Definition: irep.h:315
typet
The type of an expression, extends irept.
Definition: type.h:27
ansi_c_parsert::cpp98
bool cpp98
Definition: ansi_c_parser.h:77
ansi_c_languaget::~ansi_c_languaget
~ansi_c_languaget() override
Definition: ansi_c_language.cpp:221
ansi_c_languaget::to_expr
bool to_expr(const std::string &code, const std::string &module, exprt &expr, const namespacet &ns) override
Parses the given string into an expression.
Definition: ansi_c_language.cpp:174
ansi_c_parse_treet::items
itemst items
Definition: ansi_c_parse_tree.h:22
type2name.h
remove_internal_symbols
void remove_internal_symbols(symbol_tablet &symbol_table)
Removes internal symbols from a symbol table A symbol is EXPORTED if it is a.
Definition: remove_internal_symbols.cpp:74
c_preprocess.h
exprt
Base class for all expressions.
Definition: expr.h:54
exprt::op0
exprt & op0()
Definition: expr.h:84
irep_idt
dstringt irep_idt
Definition: irep.h:32
configt::ansi_c
struct configt::ansi_ct ansi_c
ansi_c_languaget::from_type
bool from_type(const typet &type, std::string &code, const namespacet &ns) override
Formats the given type in a language-specific way.
Definition: ansi_c_language.cpp:156
namespacet
A namespacet is essentially one or two symbol tables bound together, to allow for symbol lookups in t...
Definition: namespace.h:93
exprt::type
typet & type()
Return the type of the expression.
Definition: expr.h:68
ansi_c_parsert::ts_18661_3_Floatn_types
bool ts_18661_3_Floatn_types
Definition: ansi_c_parser.h:83
messaget::result
mstreamt & result() const
Definition: message.h:396
parsert::in
std::istream * in
Definition: parser.h:26
type2name
static std::string type2name(const typet &type, const namespacet &ns, symbol_numbert &symbol_number)
Definition: type2name.cpp:95
expr2c.h
expr2c
std::string expr2c(const exprt &expr, const namespacet &ns, const expr2c_configurationt &configuration)
Definition: expr2c.cpp:3955
linking
bool linking(symbol_tablet &dest_symbol_table, symbol_tablet &new_symbol_table, message_handlert &message_handler)
Definition: linking.cpp:1391
ansi_c_parsert::clear
virtual void clear() override
Definition: ansi_c_parser.h:49
configt::ansi_ct::Float128_type
bool Float128_type
Definition: config.h:46
ansi_c_internal_additions.h
messaget::set_message_handler
virtual void set_message_handler(message_handlert &_message_handler)
Definition: message.h:169
ansi_c_internal_additions
void ansi_c_internal_additions(std::string &code)
Definition: ansi_c_internal_additions.cpp:123
linking.h
ansi_c_parse_treet::swap
void swap(ansi_c_parse_treet &other)
Definition: ansi_c_parse_tree.cpp:13
ansi_c_languaget::preprocess
bool preprocess(std::istream &instream, const std::string &path, std::ostream &outstream) override
ANSI-C preprocessing.
Definition: ansi_c_language.cpp:40
irept::id
const irep_idt & id() const
Definition: irep.h:259
get_base_name.h
ansi_c_entry_point
bool ansi_c_entry_point(symbol_tablet &symbol_table, message_handlert &message_handler, const c_object_factory_parameterst &object_factory_parameters)
Definition: ansi_c_entry_point.cpp:112
config
configt config
Definition: config.cpp:24
ansi_c_parse_treet::output
void output(std::ostream &out) const
Definition: ansi_c_parse_tree.cpp:23
ansi_c_languaget::object_factory_params
c_object_factory_parameterst object_factory_params
Definition: ansi_c_language.h:97
ansi_c_parsert::cpp11
bool cpp11
Definition: ansi_c_parser.h:77
ansi_c_parsert::mode
modet mode
Definition: ansi_c_parser.h:74
configt::ansi_ct::mode
flavourt mode
Definition: config.h:115
messaget::get_message_handler
message_handlert & get_message_handler()
Definition: message.h:174
ansi_c_parsert::parse_tree
ansi_c_parse_treet parse_tree
Definition: ansi_c_parser.h:29
ansi_c_languaget::parse_tree
ansi_c_parse_treet parse_tree
Definition: ansi_c_language.h:94
ansi_c_language.h
ansi_c_parsert::Float128_type
bool Float128_type
Definition: ansi_c_parser.h:86
ansi_c_languaget::show_parse
void show_parse(std::ostream &out) override
Definition: ansi_c_language.cpp:137
ansi_c_languaget::parse
bool parse(std::istream &instream, const std::string &path) override
Definition: ansi_c_language.cpp:52
ansi_c_languaget::extensions
std::set< std::string > extensions() const override
Definition: ansi_c_language.cpp:29
remove_internal_symbols.h
new_ansi_c_language
std::unique_ptr< languaget > new_ansi_c_language()
Definition: ansi_c_language.cpp:142
ansi_c_parsert::parse
virtual bool parse() override
Definition: ansi_c_parser.h:44
ansi_c_languaget::modules_provided
void modules_provided(std::set< std::string > &modules) override
Definition: ansi_c_language.cpp:34
ansi_c_typecheck
bool ansi_c_typecheck(ansi_c_parse_treet &ansi_c_parse_tree, symbol_tablet &symbol_table, const std::string &module, message_handlert &message_handler)
Definition: ansi_c_typecheck.cpp:26
ansi_c_languaget::generate_support_functions
bool generate_support_functions(symbol_tablet &symbol_table) override
Create language-specific support functions, such as __CPROVER_start, __CPROVER_initialize and languag...
Definition: ansi_c_language.cpp:129
ansi_c_languaget::from_expr
bool from_expr(const exprt &expr, std::string &code, const namespacet &ns) override
Formats the given expression in a language-specific way.
Definition: ansi_c_language.cpp:147
config.h
ansi_c_scanner_init
void ansi_c_scanner_init()
Definition: ansi_c_lex.yy.cpp:4391
exprt::operands
operandst & operands()
Definition: expr.h:78
type2c
std::string type2c(const typet &type, const namespacet &ns, const expr2c_configurationt &configuration)
Definition: expr2c.cpp:3971
ansi_c_parser.h
ansi_c_parsert::for_has_scope
bool for_has_scope
Definition: ansi_c_parser.h:80
c_preprocess
bool c_preprocess(std::istream &instream, std::ostream &outstream, message_handlert &message_handler)
ANSI-C preprocessing.
Definition: c_preprocess.cpp:226
ansi_c_languaget::parse_path
std::string parse_path
Definition: ansi_c_language.h:95
parsert::set_file
void set_file(const irep_idt &file)
Definition: parser.h:85
ansi_c_languaget::typecheck
bool typecheck(symbol_tablet &symbol_table, const std::string &module) override
Definition: ansi_c_language.cpp:106
parsert::set_line_no
void set_line_no(unsigned _line_no)
Definition: parser.h:80