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
52 ansi_c_parser.in=&in;
53 ansi_c_parser.log.set_message_handler(message_handler);
55 ansi_c_parser.cpp98=false; // it's not C++
56 ansi_c_parser.cpp11=false; // it's not C++
58
60
62 return true;
63
64 symbol_tablet new_symbol_table;
65
66 // this is recursive -- builtin_factory is called
67 // from the typechecker
70 new_symbol_table,
71 "", // module
72 message_handler))
73 {
74 return true;
75 }
76
77 // we should now have a new symbol
78 symbol_tablet::symbolst::const_iterator s_it=
79 new_symbol_table.symbols.find(identifier);
80
81 if(s_it==new_symbol_table.symbols.end())
82 {
83 messaget message(message_handler);
84 message.error() << "failed to produce built-in symbol '" << identifier
85 << '\'' << messaget::eom;
86 return true;
87 }
88
89 // copy the new symbol
90 symbol_table.add(s_it->second);
91
92 return false;
93}
94
99 const irep_idt &identifier,
100 bool support_float16_type,
101 symbol_table_baset &symbol_table,
103{
104 // we search for "space" "identifier" "("
105 const std::string pattern=' '+id2string(identifier)+'(';
106
107 std::ostringstream s;
108
109 std::string code;
110 ansi_c_internal_additions(code, support_float16_type);
111 s << code;
112
113 // our own extensions
115 return convert(identifier, s, symbol_table, mh);
116
117 // this is Visual C/C++ only
119 {
121 return convert(identifier, s, symbol_table, mh);
122 }
123
124 // ARM stuff
126 {
128 return convert(identifier, s, symbol_table, mh);
129 }
130
131 // CW stuff
133 {
135 return convert(identifier, s, symbol_table, mh);
136 }
137
138 // GCC junk stuff, also for CLANG and ARM
139 if(
143 {
145 return convert(identifier, s, symbol_table, mh);
146
148 return convert(identifier, s, symbol_table, mh);
149
151 return convert(identifier, s, symbol_table, mh);
152
154 return convert(identifier, s, symbol_table, mh);
155
157 return convert(identifier, s, symbol_table, mh);
158
160 return convert(identifier, s, symbol_table, mh);
161
163 return convert(identifier, s, symbol_table, mh);
164
165 if(config.ansi_c.arch=="i386" ||
166 config.ansi_c.arch=="x86_64" ||
167 config.ansi_c.arch=="x32")
168 {
170 return convert(identifier, s, symbol_table, mh);
171
173 return convert(identifier, s, symbol_table, mh);
174
176 return convert(identifier, s, symbol_table, mh);
177
179 return convert(identifier, s, symbol_table, mh);
180
182 return convert(identifier, s, symbol_table, mh);
183
185 return convert(identifier, s, symbol_table, mh);
186 }
187 else if(config.ansi_c.arch=="arm64" ||
188 config.ansi_c.arch=="armel" ||
189 config.ansi_c.arch=="armhf" ||
190 config.ansi_c.arch=="arm")
191 {
193 return convert(identifier, s, symbol_table, mh);
194 }
195 else if(config.ansi_c.arch=="mips64el" ||
196 config.ansi_c.arch=="mipsn32el" ||
197 config.ansi_c.arch=="mipsel" ||
198 config.ansi_c.arch=="mips64" ||
199 config.ansi_c.arch=="mipsn32" ||
200 config.ansi_c.arch=="mips")
201 {
203 return convert(identifier, s, symbol_table, mh);
204 }
205 else if(config.ansi_c.arch=="powerpc" ||
206 config.ansi_c.arch=="ppc64" ||
207 config.ansi_c.arch=="ppc64le")
208 {
210 return convert(identifier, s, symbol_table, mh);
211 }
212 }
213
214 return true;
215}
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_mem_string[]
const char gcc_builtin_headers_ia32_4[]
const char gcc_builtin_headers_generic[]
const char gcc_builtin_headers_tm[]
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[]
ansi_c_parsert ansi_c_parser
void ansi_c_scanner_init()
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)
ait supplies three of the four components needed: an abstract interpreter (in this case handling func...
Definition ai.h:563
ansi_c_parse_treet parse_tree
virtual void clear() override
virtual bool parse() override
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:39
Class that provides messages with a built-in verbosity 'level'.
Definition message.h:155
mstreamt & error() const
Definition message.h:399
virtual void set_message_handler(message_handlert &_message_handler)
Definition message.h:179
static eomt eom
Definition message.h:297
std::istream * in
Definition parser.h:26
void set_file(const irep_idt &file)
Definition parser.h:85
messaget log
Definition parser.h:136
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:47
std::string strip_string(const std::string &s)
Remove all whitespace characters from either end of a string.
Author: Diffblue Ltd.