CBMC: /home/runner/work/cbmc/cbmc/src/ansi-c/ansi_c_language.cpp Source File

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/arith_tools.h>
12#include <util/c_types.h>
13#include <util/config.h>
14#include <util/get_base_name.h>
15#include <util/replace_symbol.h>
16#include <util/symbol_table.h>
17
18#include <linking/linking.h>
19#include <linking/remove_internal_symbols.h>
20
21#include "ansi_c_entry_point.h"
22#include "ansi_c_internal_additions.h"
23#include "ansi_c_parser.h"
24#include "ansi_c_typecheck.h"
25#include "c_preprocess.h"
26#include "expr2c.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 message_handlert &message_handler)
45{
46 // stdin?
47 if(path.empty())
48 return c_preprocess(instream, outstream, message_handler);
49
50 return c_preprocess(path, outstream, message_handler);
51}
52
54 std::istream &instream,
55 const std::string &path,
56 message_handlert &message_handler)
57{
58 // store the path
59 parse_path=path;
60
61 // preprocessing
62 std::ostringstream o_preprocessed;
63
64 if(preprocess(instream, path, o_preprocessed, message_handler))
65 return true;
66
67 std::istringstream i_preprocessed(o_preprocessed.str());
68
69 // parsing
70
71 std::string code;
72 ansi_c_internal_additions(code, config.ansi_c.float16_type);
73 std::istringstream codestr(code);
74
75 ansi_c_parsert ansi_c_parser{message_handler};
76 ansi_c_parser.set_file(ID_built_in);
77 ansi_c_parser.in=&codestr;
78 ansi_c_parser.for_has_scope=config.ansi_c.for_has_scope;
79 ansi_c_parser.ts_18661_3_Floatn_types=config.ansi_c.ts_18661_3_Floatn_types;
80 ansi_c_parser.__float128_is_keyword = config.ansi_c.__float128_is_keyword;
81 ansi_c_parser.float16_type = config.ansi_c.float16_type;
82 ansi_c_parser.bf16_type = config.ansi_c.bf16_type;
83 ansi_c_parser.fp16_type = config.ansi_c.fp16_type;
84 ansi_c_parser.cpp98=false; // it's not C++
85 ansi_c_parser.cpp11=false; // it's not C++
86 ansi_c_parser.c17 =
89 ansi_c_parser.c23 =
91 ansi_c_parser.mode=config.ansi_c.mode;
92
93 ansi_c_scanner_init(ansi_c_parser);
94
95 bool result=ansi_c_parser.parse();
96
97 if(!result)
98 {
99 ansi_c_parser.set_line_no(0);
100 ansi_c_parser.set_file(path);
101 ansi_c_parser.in=&i_preprocessed;
102 ansi_c_scanner_init(ansi_c_parser);
103 result=ansi_c_parser.parse();
104 }
105
106 // save result
107 parse_tree.swap(ansi_c_parser.parse_tree);
108
109 return result;
110}
111
117{
119 for(auto it = symbol_table.begin(); it != symbol_table.end(); ++it)
120 {
121 const symbolt &symbol = it->second;
122 if(
123 symbol.is_static_lifetime && !symbol.is_extern && !symbol.is_type &&
124 !symbol.is_macro && symbol.type.id() == ID_array &&
125 to_array_type(symbol.type).size().is_nil())
126 {
127 symbolt &writeable_symbol = it.get_writeable_symbol();
129 to_array_type(writeable_symbol.type).size() =
132 }
133 }
134
135 if(array_type_updates.empty())
136 return;
137
138 // Apply the type updates to the values (initializers) of all symbols.
139 for(auto it = symbol_table.begin(); it != symbol_table.end(); ++it)
140 {
141 if(
142 !it->second.is_type && !it->second.is_macro &&
143 it->second.value.is_not_nil())
144 {
145 array_type_updates(it.get_writeable_symbol().value);
146 }
147 }
148}
149
151 symbol_table_baset &symbol_table,
152 const std::string &module,
153 message_handlert &message_handler,
154 const bool keep_file_local)
155{
156 return typecheck(symbol_table, module, message_handler, keep_file_local, {});
157}
158
160 symbol_table_baset &symbol_table,
161 const std::string &module,
162 message_handlert &message_handler,
163 const bool keep_file_local,
164 const std::set<irep_idt> &keep)
165{
166 symbol_tablet new_symbol_table;
167
168 if(ansi_c_typecheck(parse_tree, new_symbol_table, module, message_handler))
169 {
170 return true;
171 }
172
173 // C standard 6.9.2(5): non-extern file-scope incomplete array definitions
174 // are adjusted to an array of size 1. Done here (in the front end, before
175 // linking) so the symbol's type and the types carried on symbol expressions
176 // in code stay consistent.
177 adjust_tentative_array_definitions(new_symbol_table);
178
180 new_symbol_table, message_handler, keep_file_local, keep);
181
182 if(linking(symbol_table, new_symbol_table, message_handler))
183 return true;
184
185 return false;
186}
187
189 symbol_table_baset &symbol_table,
190 message_handlert &message_handler)
191{
192 // This creates __CPROVER_start and __CPROVER_initialize:
193 return ansi_c_entry_point(
194 symbol_table, message_handler, object_factory_params);
195}
196
198{
199 parse_tree.output(out);
200}
201
202 std::unique_ptr<languaget> new_ansi_c_language()
203{
204 return std::make_unique<ansi_c_languaget>();
205}
206
208 const exprt &expr,
209 std::string &code,
210 const namespacet &ns)
211{
212 code=expr2c(expr, ns);
213 return false;
214}
215
217 const typet &type,
218 std::string &code,
219 const namespacet &ns)
220{
221 code=type2c(type, ns);
222 return false;
223}
224
226 const typet &type,
227 std::string &name,
228 const namespacet &ns)
229{
230 name=type2name(type, ns);
231 return false;
232}
233
235 const std::string &code,
236 const std::string &,
237 exprt &expr,
238 const namespacet &ns,
239 message_handlert &message_handler)
240{
241 expr.make_nil();
242
243 // no preprocessing yet...
244
245 std::istringstream i_preprocessed(
246 "void __my_expression = (void) (\n"+code+"\n);");
247
248 // parsing
249
250 ansi_c_parsert ansi_c_parser{message_handler};
251 ansi_c_parser.set_file(irep_idt());
252 ansi_c_parser.in=&i_preprocessed;
253 ansi_c_parser.for_has_scope = config.ansi_c.for_has_scope;
254 ansi_c_parser.ts_18661_3_Floatn_types=config.ansi_c.ts_18661_3_Floatn_types;
255 ansi_c_parser.__float128_is_keyword = config.ansi_c.__float128_is_keyword;
256 ansi_c_parser.float16_type = config.ansi_c.float16_type;
257 ansi_c_parser.bf16_type = config.ansi_c.bf16_type;
258 ansi_c_parser.fp16_type = config.ansi_c.fp16_type;
259 ansi_c_parser.cpp98 = false; // it's not C++
260 ansi_c_parser.cpp11 = false; // it's not C++
261 ansi_c_parser.mode = config.ansi_c.mode;
262 ansi_c_scanner_init(ansi_c_parser);
263
264 bool result=ansi_c_parser.parse();
265
266 if(ansi_c_parser.parse_tree.items.empty())
267 result=true;
268 else
269 {
270 expr=ansi_c_parser.parse_tree.items.front().declarator().value();
271
272 // typecheck it
273 result = ansi_c_typecheck(expr, message_handler, ns);
274 }
275
276 // now remove that (void) cast
277 if(expr.id()==ID_typecast &&
278 expr.type().id()==ID_empty &&
279 expr.operands().size()==1)
280 {
281 expr = to_typecast_expr(expr).op();
282 }
283
284 return result;
285}
286
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)
static void adjust_tentative_array_definitions(symbol_table_baset &symbol_table)
Adjust non-extern file-scope incomplete array definitions (tentative definitions without a size) to a...
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
constant_exprt from_integer(const mp_integer &int_value, const typet &type)
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:566
~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
Definition ansi_c_parser.h:25
struct configt::ansi_ct ansi_c
Base class for all expressions.
Definition expr.h:57
typet & type()
Return the type of the expression.
Definition expr.h:85
operandst & operands()
Definition expr.h:95
void make_nil()
Definition irep.h:446
const irep_idt & id() const
Definition irep.h:388
Definition message.h:27
A namespacet is essentially one or two symbol tables bound together, to allow for symbol lookups in t...
Definition namespace.h:91
Expression to hold a symbol (variable)
Definition std_expr.h:132
The symbol table base class interface.
virtual iteratort begin()=0
virtual iteratort end()=0
The symbol table.
Definition symbol_table.h:14
Symbol table entry.
Definition symbol.h:28
bool is_extern
Definition symbol.h:74
bool is_macro
Definition symbol.h:62
bool is_static_lifetime
Definition symbol.h:70
bool is_type
Definition symbol.h:61
typet type
Type of symbol.
Definition symbol.h:31
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:4198
std::string type2c(const typet &type, const namespacet &ns, const expr2c_configurationt &configuration)
Definition expr2c.cpp:4214
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:1132
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:2024
const array_typet & to_array_type(const typet &type)
Cast a typet to an array_typet.
Definition std_types.h:887
@ C17
@ C23
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.
#define size_type
Definition unistd.c:186
dstringt irep_idt

AltStyle によって変換されたページ (->オリジナル) /