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.mode=config.ansi_c.mode;
86
87 ansi_c_scanner_init(ansi_c_parser);
88
89 bool result=ansi_c_parser.parse();
90
91 if(!result)
92 {
93 ansi_c_parser.set_line_no(0);
94 ansi_c_parser.set_file(path);
95 ansi_c_parser.in=&i_preprocessed;
96 ansi_c_scanner_init(ansi_c_parser);
97 result=ansi_c_parser.parse();
98 }
99
100 // save result
101 parse_tree.swap(ansi_c_parser.parse_tree);
102
103 return result;
104}
105
107 symbol_table_baset &symbol_table,
108 const std::string &module,
109 message_handlert &message_handler,
110 const bool keep_file_local)
111{
112 return typecheck(symbol_table, module, message_handler, keep_file_local, {});
113}
114
116 symbol_table_baset &symbol_table,
117 const std::string &module,
118 message_handlert &message_handler,
119 const bool keep_file_local,
120 const std::set<irep_idt> &keep)
121{
122 symbol_tablet new_symbol_table;
123
124 if(ansi_c_typecheck(parse_tree, new_symbol_table, module, message_handler))
125 {
126 return true;
127 }
128
130 new_symbol_table, message_handler, keep_file_local, keep);
131
132 if(linking(symbol_table, new_symbol_table, message_handler))
133 return true;
134
135 return false;
136}
137
139 symbol_table_baset &symbol_table,
140 message_handlert &message_handler)
141{
142 // This creates __CPROVER_start and __CPROVER_initialize:
143 return ansi_c_entry_point(
144 symbol_table, message_handler, object_factory_params);
145}
146
148{
149 parse_tree.output(out);
150}
151
152std::unique_ptr<languaget> new_ansi_c_language()
153{
154 return std::make_unique<ansi_c_languaget>();
155}
156
158 const exprt &expr,
159 std::string &code,
160 const namespacet &ns)
161{
162 code=expr2c(expr, ns);
163 return false;
164}
165
167 const typet &type,
168 std::string &code,
169 const namespacet &ns)
170{
171 code=type2c(type, ns);
172 return false;
173}
174
176 const typet &type,
177 std::string &name,
178 const namespacet &ns)
179{
180 name=type2name(type, ns);
181 return false;
182}
183
185 const std::string &code,
186 const std::string &,
187 exprt &expr,
188 const namespacet &ns,
189 message_handlert &message_handler)
190{
191 expr.make_nil();
192
193 // no preprocessing yet...
194
195 std::istringstream i_preprocessed(
196 "void __my_expression = (void) (\n"+code+"\n);");
197
198 // parsing
199
200 ansi_c_parsert ansi_c_parser{message_handler};
201 ansi_c_parser.set_file(irep_idt());
202 ansi_c_parser.in=&i_preprocessed;
203 ansi_c_parser.for_has_scope = config.ansi_c.for_has_scope;
204 ansi_c_parser.ts_18661_3_Floatn_types=config.ansi_c.ts_18661_3_Floatn_types;
205 ansi_c_parser.__float128_is_keyword = config.ansi_c.__float128_is_keyword;
206 ansi_c_parser.float16_type = config.ansi_c.float16_type;
207 ansi_c_parser.bf16_type = config.ansi_c.bf16_type;
208 ansi_c_parser.fp16_type = config.ansi_c.fp16_type;
209 ansi_c_parser.cpp98 = false; // it's not C++
210 ansi_c_parser.cpp11 = false; // it's not C++
211 ansi_c_parser.mode = config.ansi_c.mode;
212 ansi_c_scanner_init(ansi_c_parser);
213
214 bool result=ansi_c_parser.parse();
215
216 if(ansi_c_parser.parse_tree.items.empty())
217 result=true;
218 else
219 {
220 expr=ansi_c_parser.parse_tree.items.front().declarator().value();
221
222 // typecheck it
223 result = ansi_c_typecheck(expr, message_handler, ns);
224 }
225
226 // now remove that (void) cast
227 if(expr.id()==ID_typecast &&
228 expr.type().id()==ID_empty &&
229 expr.operands().size()==1)
230 {
231 expr = to_typecast_expr(expr).op();
232 }
233
234 return result;
235}
236
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:94
void set_file(const irep_idt &file)
Definition parser.h:83
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:4155
std::string type2c(const typet &type, const namespacet &ns, const expr2c_configurationt &configuration)
Definition expr2c.cpp:4171
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