CBMC
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
26std::set<std::string> ansi_c_languaget::extensions() const
27{
28 return { "c", "i" };
29}
30
31void ansi_c_languaget::modules_provided(std::set<std::string> &modules)
32{
33 modules.insert(get_base_name(parse_path, true));
34}
35
38 std::istream &instream,
39 const std::string &path,
40 std::ostream &outstream,
41 message_handlert &message_handler)
42{
43 // stdin?
44 if(path.empty())
45 return c_preprocess(instream, outstream, message_handler);
46
47 return c_preprocess(path, outstream, message_handler);
48}
49
51 std::istream &instream,
52 const std::string &path,
53 message_handlert &message_handler)
54{
55 // store the path
56 parse_path=path;
57
58 // preprocessing
59 std::ostringstream o_preprocessed;
60
61 if(preprocess(instream, path, o_preprocessed, message_handler))
62 return true;
63
64 std::istringstream i_preprocessed(o_preprocessed.str());
65
66 // parsing
67
68 std::string code;
69 ansi_c_internal_additions(code, config.ansi_c.float16_type);
70 std::istringstream codestr(code);
71
72 ansi_c_parsert ansi_c_parser{message_handler};
73 ansi_c_parser.set_file(ID_built_in);
74 ansi_c_parser.in=&codestr;
75 ansi_c_parser.for_has_scope=config.ansi_c.for_has_scope;
76 ansi_c_parser.ts_18661_3_Floatn_types=config.ansi_c.ts_18661_3_Floatn_types;
77 ansi_c_parser.__float128_is_keyword = config.ansi_c.__float128_is_keyword;
78 ansi_c_parser.float16_type = config.ansi_c.float16_type;
79 ansi_c_parser.bf16_type = config.ansi_c.bf16_type;
80 ansi_c_parser.fp16_type = config.ansi_c.fp16_type;
81 ansi_c_parser.cpp98=false; // it's not C++
82 ansi_c_parser.cpp11=false; // it's not C++
83 ansi_c_parser.c17 =
86 ansi_c_parser.c23 =
88 ansi_c_parser.mode=config.ansi_c.mode;
89
90 ansi_c_scanner_init(ansi_c_parser);
91
92 bool result=ansi_c_parser.parse();
93
94 if(!result)
95 {
96 ansi_c_parser.set_line_no(0);
97 ansi_c_parser.set_file(path);
98 ansi_c_parser.in=&i_preprocessed;
99 ansi_c_scanner_init(ansi_c_parser);
100 result=ansi_c_parser.parse();
101 }
102
103 // save result
104 parse_tree.swap(ansi_c_parser.parse_tree);
105
106 return result;
107}
108
110 symbol_table_baset &symbol_table,
111 const std::string &module,
112 message_handlert &message_handler,
113 const bool keep_file_local)
114{
115 return typecheck(symbol_table, module, message_handler, keep_file_local, {});
116}
117
119 symbol_table_baset &symbol_table,
120 const std::string &module,
121 message_handlert &message_handler,
122 const bool keep_file_local,
123 const std::set<irep_idt> &keep)
124{
125 symbol_tablet new_symbol_table;
126
127 if(ansi_c_typecheck(parse_tree, new_symbol_table, module, message_handler))
128 {
129 return true;
130 }
131
133 new_symbol_table, message_handler, keep_file_local, keep);
134
135 if(linking(symbol_table, new_symbol_table, message_handler))
136 return true;
137
138 return false;
139}
140
142 symbol_table_baset &symbol_table,
143 message_handlert &message_handler)
144{
145 // This creates __CPROVER_start and __CPROVER_initialize:
146 return ansi_c_entry_point(
147 symbol_table, message_handler, object_factory_params);
148}
149
151{
152 parse_tree.output(out);
153}
154
155std::unique_ptr<languaget> new_ansi_c_language()
156{
157 return std::make_unique<ansi_c_languaget>();
158}
159
161 const exprt &expr,
162 std::string &code,
163 const namespacet &ns)
164{
165 code=expr2c(expr, ns);
166 return false;
167}
168
170 const typet &type,
171 std::string &code,
172 const namespacet &ns)
173{
174 code=type2c(type, ns);
175 return false;
176}
177
179 const typet &type,
180 std::string &name,
181 const namespacet &ns)
182{
183 name=type2name(type, ns);
184 return false;
185}
186
188 const std::string &code,
189 const std::string &,
190 exprt &expr,
191 const namespacet &ns,
192 message_handlert &message_handler)
193{
194 expr.make_nil();
195
196 // no preprocessing yet...
197
198 std::istringstream i_preprocessed(
199 "void __my_expression = (void) (\n"+code+"\n);");
200
201 // parsing
202
203 ansi_c_parsert ansi_c_parser{message_handler};
204 ansi_c_parser.set_file(irep_idt());
205 ansi_c_parser.in=&i_preprocessed;
206 ansi_c_parser.for_has_scope = config.ansi_c.for_has_scope;
207 ansi_c_parser.ts_18661_3_Floatn_types=config.ansi_c.ts_18661_3_Floatn_types;
208 ansi_c_parser.__float128_is_keyword = config.ansi_c.__float128_is_keyword;
209 ansi_c_parser.float16_type = config.ansi_c.float16_type;
210 ansi_c_parser.bf16_type = config.ansi_c.bf16_type;
211 ansi_c_parser.fp16_type = config.ansi_c.fp16_type;
212 ansi_c_parser.cpp98 = false; // it's not C++
213 ansi_c_parser.cpp11 = false; // it's not C++
214 ansi_c_parser.mode = config.ansi_c.mode;
215 ansi_c_scanner_init(ansi_c_parser);
216
217 bool result=ansi_c_parser.parse();
218
219 if(ansi_c_parser.parse_tree.items.empty())
220 result=true;
221 else
222 {
223 expr=ansi_c_parser.parse_tree.items.front().declarator().value();
224
225 // typecheck it
226 result = ansi_c_typecheck(expr, message_handler, ns);
227 }
228
229 // now remove that (void) cast
230 if(expr.id()==ID_typecast &&
231 expr.type().id()==ID_empty &&
232 expr.operands().size()==1)
233 {
234 expr = to_typecast_expr(expr).op();
235 }
236
237 return result;
238}
239
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.
ait supplies three of the four components needed: an abstract interpreter (in this case handling func...
Definition ai.h:562
~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
void swap(ansi_c_parse_treet &other)
void output(std::ostream &out) const
struct configt::ansi_ct ansi_c
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
The symbol table base class interface.
The symbol table.
The type of an expression, extends irept.
Definition type.h:29
std::string expr2c(const exprt &expr, const namespacet &ns, const expr2c_configurationt &configuration)
Definition expr2c.cpp:4190
std::string type2c(const typet &type, const namespacet &ns, const expr2c_configurationt &configuration)
Definition expr2c.cpp:4206
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