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 symbol_table_baset &symbol_table,
102{
103 // we search for "space" "identifier" "("
104 const std::string pattern=' '+id2string(identifier)+'(';
105
106 std::ostringstream s;
107
108 std::string code;
110 s << code;
111
112 // our own extensions
114 return convert(identifier, s, symbol_table, mh);
115
116 // this is Visual C/C++ only
118 {
120 return convert(identifier, s, symbol_table, mh);
121 }
122
123 // ARM stuff
125 {
127 return convert(identifier, s, symbol_table, mh);
128 }
129
130 // CW stuff
132 {
134 return convert(identifier, s, symbol_table, mh);
135 }
136
137 // GCC junk stuff, also for CLANG and ARM
138 if(
142 {
144 return convert(identifier, s, symbol_table, mh);
145
147 return convert(identifier, s, symbol_table, mh);
148
150 return convert(identifier, s, symbol_table, mh);
151
153 return convert(identifier, s, symbol_table, mh);
154
156 return convert(identifier, s, symbol_table, mh);
157
159 return convert(identifier, s, symbol_table, mh);
160
162 return convert(identifier, s, symbol_table, mh);
163
164 if(config.ansi_c.arch=="i386" ||
165 config.ansi_c.arch=="x86_64" ||
166 config.ansi_c.arch=="x32")
167 {
169 return convert(identifier, s, symbol_table, mh);
170
172 return convert(identifier, s, symbol_table, mh);
173
175 return convert(identifier, s, symbol_table, mh);
176
178 return convert(identifier, s, symbol_table, mh);
179
181 return convert(identifier, s, symbol_table, mh);
182
184 return convert(identifier, s, symbol_table, mh);
185 }
186 else if(config.ansi_c.arch=="arm64" ||
187 config.ansi_c.arch=="armel" ||
188 config.ansi_c.arch=="armhf" ||
189 config.ansi_c.arch=="arm")
190 {
192 return convert(identifier, s, symbol_table, mh);
193 }
194 else if(config.ansi_c.arch=="mips64el" ||
195 config.ansi_c.arch=="mipsn32el" ||
196 config.ansi_c.arch=="mipsel" ||
197 config.ansi_c.arch=="mips64" ||
198 config.ansi_c.arch=="mipsn32" ||
199 config.ansi_c.arch=="mips")
200 {
202 return convert(identifier, s, symbol_table, mh);
203 }
204 else if(config.ansi_c.arch=="powerpc" ||
205 config.ansi_c.arch=="ppc64" ||
206 config.ansi_c.arch=="ppc64le")
207 {
209 return convert(identifier, s, symbol_table, mh);
210 }
211 }
212
213 return true;
214}
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_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
bool builtin_factory(const irep_idt &identifier, symbol_table_baset &symbol_table, message_handlert &mh)
Check whether given identifier is a compiler built-in.
static bool convert(const irep_idt &identifier, const std::ostringstream &s, symbol_table_baset &symbol_table, message_handlert &message_handler)
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.