cprover
Loading...
Searching...
No Matches
ansi_c_language.cpp
Go to the documentation of this file.
1/*******************************************************************\
2
3Module:
4
5Author: Daniel Kroening, kroening@kroening.com
6
7\*******************************************************************/
8
9#include "ansi_c_language.h"
10
11#include <util/config.h>
12#include <util/get_base_name.h>
13#include <util/symbol_table.h>
14
15#include <linking/linking.h>
17
18#include "ansi_c_entry_point.h"
20#include "ansi_c_parser.h"
21#include "ansi_c_typecheck.h"
22#include "c_preprocess.h"
23#include "expr2c.h"
24#include "type2name.h"
25
26#include <fstream>
27
28std::set<std::string> ansi_c_languaget::extensions() const
29{
30 return { "c", "i" };
31}
32
33void ansi_c_languaget::modules_provided(std::set<std::string> &modules)
34{
35 modules.insert(get_base_name(parse_path, true));
36}
37
40 std::istream &instream,
41 const std::string &path,
42 std::ostream &outstream,
43 message_handlert &message_handler)
44{
45 // stdin?
46 if(path.empty())
47 return c_preprocess(instream, outstream, message_handler);
48
49 return c_preprocess(path, outstream, message_handler);
50}
51
53 std::istream &instream,
54 const std::string &path,
55 message_handlert &message_handler)
56{
57 // store the path
58 parse_path=path;
59
60 // preprocessing
61 std::ostringstream o_preprocessed;
62
63 if(preprocess(instream, path, o_preprocessed, message_handler))
64 return true;
65
66 std::istringstream i_preprocessed(o_preprocessed.str());
67
68 // parsing
69
70 std::string code;
71 ansi_c_internal_additions(code, config.ansi_c.float16_type);
72 std::istringstream codestr(code);
73
74 ansi_c_parsert ansi_c_parser{message_handler};
75 ansi_c_parser.set_file(ID_built_in);
76 ansi_c_parser.in=&codestr;
77 ansi_c_parser.for_has_scope=config.ansi_c.for_has_scope;
78 ansi_c_parser.ts_18661_3_Floatn_types=config.ansi_c.ts_18661_3_Floatn_types;
79 ansi_c_parser.__float128_is_keyword = config.ansi_c.__float128_is_keyword;
80 ansi_c_parser.float16_type = config.ansi_c.float16_type;
81 ansi_c_parser.bf16_type = config.ansi_c.bf16_type;
82 ansi_c_parser.fp16_type = config.ansi_c.fp16_type;
83 ansi_c_parser.cpp98=false; // it's not C++
84 ansi_c_parser.cpp11=false; // it's not C++
85 ansi_c_parser.c17 =
86 config.ansi_c.c_standard == configt::ansi_ct::c_standardt::C17 ||
87 config.ansi_c.c_standard == configt::ansi_ct::c_standardt::C23;
88 ansi_c_parser.c23 =
89 config.ansi_c.c_standard == configt::ansi_ct::c_standardt::C23;
90 ansi_c_parser.mode=config.ansi_c.mode;
91
92 ansi_c_scanner_init(ansi_c_parser);
93
94 bool result=ansi_c_parser.parse();
95
96 if(!result)
97 {
98 ansi_c_parser.set_line_no(0);
99 ansi_c_parser.set_file(path);
100 ansi_c_parser.in=&i_preprocessed;
101 ansi_c_scanner_init(ansi_c_parser);
102 result=ansi_c_parser.parse();
103 }
104
105 // save result
106 parse_tree.swap(ansi_c_parser.parse_tree);
107
108 return result;
109}
110
112 symbol_table_baset &symbol_table,
113 const std::string &module,
114 message_handlert &message_handler,
115 const bool keep_file_local)
116{
117 return typecheck(symbol_table, module, message_handler, keep_file_local, {});
118}
119
121 symbol_table_baset &symbol_table,
122 const std::string &module,
123 message_handlert &message_handler,
124 const bool keep_file_local,
125 const std::set<irep_idt> &keep)
126{
127 symbol_tablet new_symbol_table;
128
129 if(ansi_c_typecheck(parse_tree, new_symbol_table, module, message_handler))
130 {
131 return true;
132 }
133
135 new_symbol_table, message_handler, keep_file_local, keep);
136
137 if(linking(symbol_table, new_symbol_table, message_handler))
138 return true;
139
140 return false;
141}
142
144 symbol_table_baset &symbol_table,
145 message_handlert &message_handler)
146{
147 // This creates __CPROVER_start and __CPROVER_initialize:
148 return ansi_c_entry_point(
149 symbol_table, message_handler, object_factory_params);
150}
151
153{
154 parse_tree.output(out);
155}
156
157std::unique_ptr<languaget> new_ansi_c_language()
158{
159 return std::make_unique<ansi_c_languaget>();
160}
161
163 const exprt &expr,
164 std::string &code,
165 const namespacet &ns)
166{
167 code=expr2c(expr, ns);
168 return false;
169}
170
172 const typet &type,
173 std::string &code,
174 const namespacet &ns)
175{
176 code=type2c(type, ns);
177 return false;
178}
179
181 const typet &type,
182 std::string &name,
183 const namespacet &ns)
184{
185 name=type2name(type, ns);
186 return false;
187}
188
190 const std::string &code,
191 const std::string &,
192 exprt &expr,
193 const namespacet &ns,
194 message_handlert &message_handler)
195{
196 expr.make_nil();
197
198 // no preprocessing yet...
199
200 std::istringstream i_preprocessed(
201 "void __my_expression = (void) (\n"+code+"\n);");
202
203 // parsing
204
205 ansi_c_parsert ansi_c_parser{message_handler};
206 ansi_c_parser.set_file(irep_idt());
207 ansi_c_parser.in=&i_preprocessed;
208 ansi_c_parser.for_has_scope = config.ansi_c.for_has_scope;
209 ansi_c_parser.ts_18661_3_Floatn_types=config.ansi_c.ts_18661_3_Floatn_types;
210 ansi_c_parser.__float128_is_keyword = config.ansi_c.__float128_is_keyword;
211 ansi_c_parser.float16_type = config.ansi_c.float16_type;
212 ansi_c_parser.bf16_type = config.ansi_c.bf16_type;
213 ansi_c_parser.fp16_type = config.ansi_c.fp16_type;
214 ansi_c_parser.cpp98 = false; // it's not C++
215 ansi_c_parser.cpp11 = false; // it's not C++
216 ansi_c_parser.mode = config.ansi_c.mode;
217 ansi_c_scanner_init(ansi_c_parser);
218
219 bool result=ansi_c_parser.parse();
220
221 if(ansi_c_parser.parse_tree.items.empty())
222 result=true;
223 else
224 {
225 expr=ansi_c_parser.parse_tree.items.front().declarator().value();
226
227 // typecheck it
228 result = ansi_c_typecheck(expr, message_handler, ns);
229 }
230
231 // now remove that (void) cast
232 if(expr.id()==ID_typecast &&
233 expr.type().id()==ID_empty &&
234 expr.operands().size()==1)
235 {
236 expr = to_typecast_expr(expr).op();
237 }
238
239 return result;
240}
241
bool ansi_c_entry_point(symbol_table_baset &symbol_table, message_handlert &message_handler, const c_object_factory_parameterst &object_factory_parameters)
void ansi_c_internal_additions(std::string &code, bool support_float16_type)
std::unique_ptr< languaget > new_ansi_c_language()
void ansi_c_scanner_init(ansi_c_parsert &)
bool ansi_c_typecheck(ansi_c_parse_treet &ansi_c_parse_tree, symbol_table_baset &symbol_table, const std::string &module, message_handlert &message_handler)
ANSI-C Language Type Checking.
configt config
Definition config.cpp:25
bool c_preprocess(std::istream &instream, std::ostream &outstream, message_handlert &message_handler)
ANSI-C preprocessing.
~ansi_c_languaget() override
std::set< std::string > extensions() const override
void show_parse(std::ostream &out, message_handlert &) override
bool from_type(const typet &type, std::string &code, const namespacet &ns) override
Formats the given type in a language-specific way.
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.
bool to_expr(const std::string &code, const std::string &module, exprt &expr, const namespacet &ns, message_handlert &message_handler) override
Parses the given string into an expression.
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.
bool typecheck(symbol_table_baset &symbol_table, const std::string &module, message_handlert &message_handler, const bool keep_file_local) override
typecheck without removing specified entries from the symbol table
bool preprocess(std::istream &instream, const std::string &path, std::ostream &outstream, message_handlert &message_handler) override
ANSI-C preprocessing.
bool generate_support_functions(symbol_table_baset &symbol_table, message_handlert &message_handler) override
Create language-specific support functions, such as __CPROVER_start, __CPROVER_initialize and languag...
ansi_c_parse_treet parse_tree
c_object_factory_parameterst object_factory_params
bool parse(std::istream &instream, const std::string &path, message_handlert &message_handler) override
Base class for all expressions.
Definition expr.h:56
typet & type()
Return the type of the expression.
Definition expr.h:84
operandst & operands()
Definition expr.h:94
void make_nil()
Definition irep.h:446
const irep_idt & id() const
Definition irep.h:388
A namespacet is essentially one or two symbol tables bound together, to allow for symbol lookups in t...
Definition namespace.h:91
void set_file(const irep_idt &file)
Definition parser.h:84
The symbol table base class interface.
The symbol table.
The type of an expression, extends irept.
Definition type.h:29
const exprt & op() const
Definition std_expr.h:391
std::string expr2c(const exprt &expr, const namespacet &ns, const expr2c_configurationt &configuration)
Definition expr2c.cpp:4184
std::string type2c(const typet &type, const namespacet &ns, const expr2c_configurationt &configuration)
Definition expr2c.cpp:4200
std::string get_base_name(const std::string &in, bool strip_suffix)
cleans a filename from path and extension
bool linking(symbol_table_baset &dest_symbol_table, const symbol_table_baset &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:1130
ANSI-C Linking.
void remove_internal_symbols(symbol_table_baset &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:2107
Author: Diffblue Ltd.
static std::string type2name(const typet &type, const namespacet &ns, symbol_numbert &symbol_number)
Definition type2name.cpp:82
Type Naming for C.
dstringt irep_idt