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"
11
12#include "ansi_c_parser.h"
13#include "ansi_c_typecheck.h"
14
15#include <util/config.h>
16#include <util/prefix.h>
17#include <util/string_utils.h>
18
19#include <sstream>
20
21static bool find_pattern(
22 const std::string &pattern,
23 const char *header_file,
24 std::ostream &out)
25{
26 std::istringstream hdr(header_file);
27 std::string line;
28 while(std::getline(hdr, line))
29 {
30 line = strip_string(line);
31 if(has_prefix(line, "//") || line.find(pattern) == std::string::npos)
32 continue;
33
34 out << line;
35 return true;
36 }
37
38 return false;
39}
40
41static bool convert(
42 const irep_idt &identifier,
43 const std::ostringstream &s,
44 symbol_tablet &symbol_table,
45 message_handlert &message_handler)
46{
47 std::istringstream in(s.str());
48
51 ansi_c_parser.in=&in;
52 ansi_c_parser.set_message_handler(message_handler);
54 ansi_c_parser.cpp98=false; // it's not C++
55 ansi_c_parser.cpp11=false; // it's not C++
57
59
61 return true;
62
63 symbol_tablet new_symbol_table;
64
65 // this is recursive -- builtin_factory is called
66 // from the typechecker
69 new_symbol_table,
70 "", // module
71 message_handler))
72 {
73 return true;
74 }
75
76 // we should now have a new symbol
77 symbol_tablet::symbolst::const_iterator s_it=
78 new_symbol_table.symbols.find(identifier);
79
80 if(s_it==new_symbol_table.symbols.end())
81 {
82 messaget message(message_handler);
83 message.error() << "failed to produce built-in symbol '" << identifier
84 << '\'' << messaget::eom;
85 return true;
86 }
87
88 // copy the new symbol
89 symbol_table.add(s_it->second);
90
91 return false;
92}
93
98 const irep_idt &identifier,
99 symbol_tablet &symbol_table,
101{
102 // we search for "space" "identifier" "("
103 const std::string pattern=' '+id2string(identifier)+'(';
104
105 std::ostringstream s;
106
107 std::string code;
109 s << code;
110
111 // our own extensions
113 return convert(identifier, s, symbol_table, mh);
114
115 // this is Visual C/C++ only
117 {
119 return convert(identifier, s, symbol_table, mh);
120 }
121
122 // ARM stuff
124 {
126 return convert(identifier, s, symbol_table, mh);
127 }
128
129 // CW stuff
131 {
133 return convert(identifier, s, symbol_table, mh);
134 }
135
136 // GCC junk stuff, also for CLANG and ARM
137 if(
141 {
143 return convert(identifier, s, symbol_table, mh);
144
146 return convert(identifier, s, symbol_table, mh);
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
161 return convert(identifier, s, symbol_table, mh);
162
163 if(config.ansi_c.arch=="i386" ||
164 config.ansi_c.arch=="x86_64" ||
165 config.ansi_c.arch=="x32")
166 {
168 return convert(identifier, s, symbol_table, mh);
169
171 return convert(identifier, s, symbol_table, mh);
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 }
182 else if(config.ansi_c.arch=="arm64" ||
183 config.ansi_c.arch=="armel" ||
184 config.ansi_c.arch=="armhf" ||
185 config.ansi_c.arch=="arm")
186 {
188 return convert(identifier, s, symbol_table, mh);
189 }
190 else if(config.ansi_c.arch=="mips64el" ||
191 config.ansi_c.arch=="mipsn32el" ||
192 config.ansi_c.arch=="mipsel" ||
193 config.ansi_c.arch=="mips64" ||
194 config.ansi_c.arch=="mipsn32" ||
195 config.ansi_c.arch=="mips")
196 {
198 return convert(identifier, s, symbol_table, mh);
199 }
200 else if(config.ansi_c.arch=="powerpc" ||
201 config.ansi_c.arch=="ppc64" ||
202 config.ansi_c.arch=="ppc64le")
203 {
205 return convert(identifier, s, symbol_table, mh);
206 }
207 }
208
209 return true;
210}
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[]
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[]
void ansi_c_internal_additions(std::string &code)
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_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_tablet &symbol_table, const std::string &module, message_handlert &message_handler)
ANSI-C Language Type Checking.
static bool convert(const irep_idt &identifier, const std::ostringstream &s, symbol_tablet &symbol_table, message_handlert &message_handler)
bool builtin_factory(const irep_idt &identifier, symbol_tablet &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:564
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:37
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
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.
configt config
Definition config.cpp:25
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.