cprover
Loading...
Searching...
No Matches
builtin_factory.cpp
Go to the documentation of this file.
1/*******************************************************************\
2
3Module:
4
5Author: Daniel Kroening, kroening@kroening.com
6
7\*******************************************************************/
8
9#include "builtin_factory.h"
10
11#include <util/config.h>
12#include <util/prefix.h>
13#include <util/string_utils.h>
14#include <util/symbol_table.h>
15
17#include "ansi_c_parser.h"
18#include "ansi_c_typecheck.h"
19
20#include <sstream>
21
22static bool find_pattern(
23 const std::string &pattern,
24 const char *header_file,
25 std::ostream &out)
26{
27 std::istringstream hdr(header_file);
28 std::string line;
29 while(std::getline(hdr, line))
30 {
31 line = strip_string(line);
32 if(has_prefix(line, "//") || line.find(pattern) == std::string::npos)
33 continue;
34
35 out << line;
36 return true;
37 }
38
39 return false;
40}
41
42static bool convert(
43 const irep_idt &identifier,
44 const std::ostringstream &s,
45 symbol_table_baset &symbol_table,
46 message_handlert &message_handler)
47{
48 std::istringstream in(s.str());
49
50 ansi_c_parsert ansi_c_parser{message_handler};
51 ansi_c_parser.set_file(ID_built_in);
52 ansi_c_parser.in=&in;
53 ansi_c_parser.for_has_scope=config.ansi_c.for_has_scope;
54 ansi_c_parser.ts_18661_3_Floatn_types = config.ansi_c.ts_18661_3_Floatn_types;
55 ansi_c_parser.__float128_is_keyword = config.ansi_c.__float128_is_keyword;
56 ansi_c_parser.float16_type = config.ansi_c.float16_type;
57 ansi_c_parser.bf16_type = config.ansi_c.bf16_type;
58 ansi_c_parser.fp16_type = config.ansi_c.fp16_type;
59 ansi_c_parser.cpp98=false; // it's not C++
60 ansi_c_parser.cpp11=false; // it's not C++
61 ansi_c_parser.mode=config.ansi_c.mode;
62
63 ansi_c_scanner_init(ansi_c_parser);
64
65 if(ansi_c_parser.parse())
66 return true;
67
68 symbol_tablet new_symbol_table;
69
70 // this is recursive -- builtin_factory is called
71 // from the typechecker
73 ansi_c_parser.parse_tree,
74 new_symbol_table,
75 "", // module
76 message_handler))
77 {
78 return true;
79 }
80
81 // we should now have a new symbol
82 symbol_tablet::symbolst::const_iterator s_it=
83 new_symbol_table.symbols.find(identifier);
84
85 if(s_it==new_symbol_table.symbols.end())
86 {
87 messaget message(message_handler);
88 message.error() << "failed to produce built-in symbol '" << identifier
89 << '\'' << messaget::eom;
90 return true;
91 }
92
93 // copy the new symbol
94 symbol_table.add(s_it->second);
95
96 return false;
97}
98
103 const irep_idt &identifier,
104 bool support_float16_type,
105 symbol_table_baset &symbol_table,
107{
108 // we search for "space" "identifier" "("
109 const std::string pattern=' '+id2string(identifier)+'(';
110
111 std::ostringstream s;
112
113 std::string code;
114 ansi_c_internal_additions(code, support_float16_type);
115 s << code;
116
117 // our own extensions
119 return convert(identifier, s, symbol_table, mh);
120
121 // this is Visual C/C++ only
123 {
125 return convert(identifier, s, symbol_table, mh);
126 }
127
128 // ARM stuff
130 {
131 if(find_pattern(pattern, arm_builtin_headers, s))
132 return convert(identifier, s, symbol_table, mh);
133 }
134
135 // CW stuff
137 {
138 if(find_pattern(pattern, cw_builtin_headers, s))
139 return convert(identifier, s, symbol_table, mh);
140 }
141
142 // GCC junk stuff, also for CLANG and ARM
143 if(
147 {
149 return convert(identifier, s, symbol_table, mh);
150
152 return convert(identifier, s, symbol_table, mh);
153
155 return convert(identifier, s, symbol_table, mh);
156
158 return convert(identifier, s, symbol_table, mh);
159
160 if(find_pattern(pattern, gcc_builtin_headers_tm, s))
161 return convert(identifier, s, symbol_table, mh);
162
164 return convert(identifier, s, symbol_table, mh);
165
166 if(find_pattern(pattern, clang_builtin_headers, s))
167 return convert(identifier, s, symbol_table, mh);
168
169 if(config.ansi_c.arch=="i386" ||
170 config.ansi_c.arch=="x86_64" ||
171 config.ansi_c.arch=="x32")
172 {
174 return convert(identifier, s, symbol_table, mh);
175
177 return convert(identifier, s, symbol_table, mh);
178
180 return convert(identifier, s, symbol_table, mh);
181
183 return convert(identifier, s, symbol_table, mh);
184
186 return convert(identifier, s, symbol_table, mh);
187
189 return convert(identifier, s, symbol_table, mh);
190
192 return convert(identifier, s, symbol_table, mh);
193
195 return convert(identifier, s, symbol_table, mh);
196
198 return convert(identifier, s, symbol_table, mh);
199 }
200 else if(config.ansi_c.arch=="arm64" ||
201 config.ansi_c.arch=="armel" ||
202 config.ansi_c.arch=="armhf" ||
203 config.ansi_c.arch=="arm")
204 {
206 return convert(identifier, s, symbol_table, mh);
207 }
208 else if(config.ansi_c.arch=="mips64el" ||
209 config.ansi_c.arch=="mipsn32el" ||
210 config.ansi_c.arch=="mipsel" ||
211 config.ansi_c.arch=="mips64" ||
212 config.ansi_c.arch=="mipsn32" ||
213 config.ansi_c.arch=="mips")
214 {
216 return convert(identifier, s, symbol_table, mh);
217 }
218 else if(config.ansi_c.arch=="powerpc" ||
219 config.ansi_c.arch=="ppc64" ||
220 config.ansi_c.arch=="ppc64le")
221 {
223 return convert(identifier, s, symbol_table, mh);
224 }
225 }
226
227 return true;
228}
const char gcc_builtin_headers_ia32_7[]
const char cprover_builtin_headers[]
const char gcc_builtin_headers_ia32[]
const char gcc_builtin_headers_ia32_2[]
const char gcc_builtin_headers_ia32_5[]
const char gcc_builtin_headers_ubsan[]
void ansi_c_internal_additions(std::string &code, bool support_float16_type)
const char windows_builtin_headers[]
const char gcc_builtin_headers_ia32_8[]
const char gcc_builtin_headers_mem_string[]
const char gcc_builtin_headers_ia32_4[]
const char gcc_builtin_headers_generic[]
const char gcc_builtin_headers_tm[]
const char gcc_builtin_headers_ia32_9[]
const char cw_builtin_headers[]
const char gcc_builtin_headers_math[]
const char gcc_builtin_headers_arm[]
const char gcc_builtin_headers_ia32_6[]
const char gcc_builtin_headers_mips[]
const char clang_builtin_headers[]
const char arm_builtin_headers[]
const char gcc_builtin_headers_omp[]
const char gcc_builtin_headers_ia32_3[]
const char gcc_builtin_headers_power[]
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
static bool convert(const irep_idt &identifier, const std::ostringstream &s, symbol_table_baset &symbol_table, message_handlert &message_handler)
bool builtin_factory(const irep_idt &identifier, bool support_float16_type, symbol_table_baset &symbol_table, message_handlert &mh)
Check whether given identifier is a compiler built-in.
static bool find_pattern(const std::string &pattern, const char *header_file, std::ostream &out)
struct configt::ansi_ct ansi_c
dstringt has one field, an unsigned integer no which is an index into a static table of strings.
Definition dstring.h:38
Class that provides messages with a built-in verbosity 'level'.
Definition message.h:154
mstreamt & error() const
Definition message.h:391
static eomt eom
Definition message.h:289
void set_file(const irep_idt &file)
Definition parser.h:83
The symbol table base class interface.
const symbolst & symbols
Read-only field, used to look up symbols given their names.
bool add(const symbolt &symbol)
Add a new symbol to the symbol table.
The symbol table.
bool has_prefix(const std::string &s, const std::string &prefix)
Definition converter.cpp:13
const std::string & id2string(const irep_idt &d)
Definition irep.h:44
std::string strip_string(const std::string &s)
Remove all whitespace characters from either end of a string.
bool for_has_scope
Definition config.h:151
bool float16_type
Definition config.h:155
bool ts_18661_3_Floatn_types
Definition config.h:152
irep_idt arch
Definition config.h:223
bool __float128_is_keyword
Definition config.h:154
flavourt mode
Definition config.h:256
Author: Diffblue Ltd.