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 }
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:46
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:20
ansi_c_typecheck.h
ANSI-C Language Type Checking.
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:166
configt::ansi_ct::for_has_scope
bool for_has_scope
Definition: config.h:45
ansi_c_entry_point.h
irept::make_nil
void make_nil()
Definition: irep.h:475
typet
The type of an expression, extends irept.
Definition: type.h:29
ansi_c_parsert::cpp98
bool cpp98
Definition: ansi_c_parser.h:79
ansi_c_languaget::~ansi_c_languaget
~ansi_c_languaget() override
Definition: ansi_c_language.cpp:224
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:175
ansi_c_parse_treet::items
itemst items
Definition: ansi_c_parse_tree.h:22
type2name.h
Type Naming for C.
c_preprocess.h
exprt
Base class for all expressions.
Definition: expr.h:53
irep_idt
dstringt irep_idt
Definition: irep.h:32
configt::ansi_c
struct configt::ansi_ct ansi_c
remove_internal_symbols
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.
Definition: remove_internal_symbols.cpp:77
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:157
namespacet
A namespacet is essentially one or two symbol tables bound together, to allow for symbol lookups in t...
Definition: namespace.h:92
exprt::type
typet & type()
Return the type of the expression.
Definition: expr.h:81
ansi_c_parsert::ts_18661_3_Floatn_types
bool ts_18661_3_Floatn_types
Definition: ansi_c_parser.h:85
messaget::result
mstreamt & result() const
Definition: message.h:409
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:81
expr2c.h
expr2c
std::string expr2c(const exprt &expr, const namespacet &ns, const expr2c_configurationt &configuration)
Definition: expr2c.cpp:3878
linking
bool linking(symbol_tablet &dest_symbol_table, symbol_tablet &new_symbol_table, message_handlert &message_handler)
Definition: linking.cpp:1441
ansi_c_parsert::clear
virtual void clear() override
Definition: ansi_c_parser.h:49
ansi_c_internal_additions.h
ansi_c_scanner_init
void ansi_c_scanner_init()
messaget::set_message_handler
virtual void set_message_handler(message_handlert &_message_handler)
Definition: message.h:179
ansi_c_internal_additions
void ansi_c_internal_additions(std::string &code)
Definition: ansi_c_internal_additions.cpp:153
linking.h
ANSI-C Linking.
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:418
get_base_name.h
unary_exprt::op
const exprt & op() const
Definition: std_expr.h:281
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:103
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:109
ansi_c_parsert::cpp11
bool cpp11
Definition: ansi_c_parser.h:79
ansi_c_parsert::mode
modet mode
Definition: ansi_c_parser.h:76
configt::ansi_ct::mode
flavourt mode
Definition: config.h:116
messaget::get_message_handler
message_handlert & get_message_handler()
Definition: message.h:184
ansi_c_parsert::parse_tree
ansi_c_parse_treet parse_tree
Definition: ansi_c_parser.h:30
ansi_c_languaget::parse_tree
ansi_c_parse_treet parse_tree
Definition: ansi_c_language.h:106
ansi_c_language.h
ansi_c_languaget::show_parse
void show_parse(std::ostream &out) override
Definition: ansi_c_language.cpp:138
ansi_c_languaget::parse
bool parse(std::istream &instream, const std::string &path) override
Definition: ansi_c_language.cpp:52
to_typecast_expr
const typecast_exprt & to_typecast_expr(const exprt &expr)
Cast an exprt to a typecast_exprt.
Definition: std_expr.h:2047
ansi_c_languaget::extensions
std::set< std::string > extensions() const override
Definition: ansi_c_language.cpp:29
remove_internal_symbols.h
Remove symbols that are internal only.
new_ansi_c_language
std::unique_ptr< languaget > new_ansi_c_language()
Definition: ansi_c_language.cpp:143
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:22
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:130
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:148
config.h
exprt::operands
operandst & operands()
Definition: expr.h:95
type2c
std::string type2c(const typet &type, const namespacet &ns, const expr2c_configurationt &configuration)
Definition: expr2c.cpp:3894
ansi_c_languaget::typecheck
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
Definition: ansi_c_language.cpp:105
ansi_c_parser.h
ansi_c_parsert::for_has_scope
bool for_has_scope
Definition: ansi_c_parser.h:82
c_preprocess
bool c_preprocess(std::istream &instream, std::ostream &outstream, message_handlert &message_handler)
ANSI-C preprocessing.
Definition: c_preprocess.cpp:227
ansi_c_languaget::parse_path
std::string parse_path
Definition: ansi_c_language.h:107
parsert::set_file
void set_file(const irep_idt &file)
Definition: parser.h:85
parsert::set_line_no
void set_line_no(unsigned _line_no)
Definition: parser.h:80