cprover
builtin_factory.cpp
Go to the documentation of this file.
1 /*******************************************************************\
2 
3 Module:
4 
5 Author: 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/string_utils.h>
17 
18 #include <ostream>
19 #include <sstream>
20 
21 static 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 
41 static bool convert(
42  const irep_idt &identifier,
43  const std::ostringstream &s,
44  symbol_tablet &symbol_table,
46 {
47  std::istringstream in(s.str());
48 
50  ansi_c_parser.set_file(ID_built_in);
51  ansi_c_parser.in=&in;
54  ansi_c_parser.cpp98=false; // it's not C++
55  ansi_c_parser.cpp11=false; // it's not C++
57 
59 
60  if(ansi_c_parser.parse())
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
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 `"
84  << identifier << '\'' << 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,
100  message_handlert &mh)
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
112  if(find_pattern(pattern, cprover_builtin_headers, s))
113  return convert(identifier, s, symbol_table, mh);
114 
115  // this is Visual C/C++ only
117  {
118  if(find_pattern(pattern, windows_builtin_headers, s))
119  return convert(identifier, s, symbol_table, mh);
120  }
121 
122  // ARM stuff
124  {
125  if(find_pattern(pattern, arm_builtin_headers, s))
126  return convert(identifier, s, symbol_table, mh);
127  }
128 
129  // CW stuff
131  {
132  if(find_pattern(pattern, cw_builtin_headers, s))
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 
145  if(find_pattern(pattern, gcc_builtin_headers_math, s))
146  return convert(identifier, s, symbol_table, mh);
147 
149  return convert(identifier, s, symbol_table, mh);
150 
151  if(find_pattern(pattern, gcc_builtin_headers_omp, s))
152  return convert(identifier, s, symbol_table, mh);
153 
154  if(find_pattern(pattern, gcc_builtin_headers_tm, s))
155  return convert(identifier, s, symbol_table, mh);
156 
157  if(find_pattern(pattern, gcc_builtin_headers_ubsan, s))
158  return convert(identifier, s, symbol_table, mh);
159 
160  if(find_pattern(pattern, clang_builtin_headers, s))
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  {
167  if(find_pattern(pattern, gcc_builtin_headers_ia32, s))
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  }
179  else if(config.ansi_c.arch=="arm64" ||
180  config.ansi_c.arch=="armel" ||
181  config.ansi_c.arch=="armhf" ||
182  config.ansi_c.arch=="arm")
183  {
184  if(find_pattern(pattern, gcc_builtin_headers_arm, s))
185  return convert(identifier, s, symbol_table, mh);
186  }
187  else if(config.ansi_c.arch=="mips64el" ||
188  config.ansi_c.arch=="mipsn32el" ||
189  config.ansi_c.arch=="mipsel" ||
190  config.ansi_c.arch=="mips64" ||
191  config.ansi_c.arch=="mipsn32" ||
192  config.ansi_c.arch=="mips")
193  {
194  if(find_pattern(pattern, gcc_builtin_headers_mips, s))
195  return convert(identifier, s, symbol_table, mh);
196  }
197  else if(config.ansi_c.arch=="powerpc" ||
198  config.ansi_c.arch=="ppc64" ||
199  config.ansi_c.arch=="ppc64le")
200  {
201  if(find_pattern(pattern, gcc_builtin_headers_power, s))
202  return convert(identifier, s, symbol_table, mh);
203  }
204  }
205 
206  return true;
207 }
struct configt::ansi_ct ansi_c
const std::string & id2string(const irep_idt &d)
Definition: irep.h:44
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_parse_treet parse_tree
Definition: ansi_c_parser.h:29
const char gcc_builtin_headers_ia32_3[]
const char gcc_builtin_headers_ubsan[]
std::istream * in
Definition: parser.h:26
ANSI-C Language Type Checking.
std::string strip_string(const std::string &s)
Remove all whitespace characters from either end of a string.
static mstreamt & eom(mstreamt &m)
Definition: message.h:272
configt config
Definition: config.cpp:23
const char arm_builtin_headers[]
void ansi_c_internal_additions(std::string &code)
const char cw_builtin_headers[]
const char gcc_builtin_headers_omp[]
bool builtin_factory(const irep_idt &identifier, symbol_tablet &symbol_table, message_handlert &mh)
Check whether given identifier is a compiler built-in.
const char gcc_builtin_headers_mips[]
flavourt mode
Definition: config.h:114
virtual bool parse() override
Definition: ansi_c_parser.h:44
void set_file(const irep_idt &file)
Definition: parser.h:85
const char cprover_builtin_headers[]
The symbol table.
Definition: symbol_table.h:19
mstreamt & error() const
Definition: message.h:302
irep_idt arch
Definition: config.h:84
bool has_prefix(const std::string &s, const std::string &prefix)
Definition: converter.cpp:13
const char gcc_builtin_headers_generic[]
const char windows_builtin_headers[]
const char gcc_builtin_headers_tm[]
void ansi_c_scanner_init()
static bool convert(const irep_idt &identifier, const std::ostringstream &s, symbol_tablet &symbol_table, message_handlert &message_handler)
virtual void set_message_handler(message_handlert &_message_handler)
Definition: message.h:148
bool for_has_scope
Definition: config.h:44
const char gcc_builtin_headers_mem_string[]
dstringt has one field, an unsigned integer no which is an index into a static table of strings...
Definition: dstring.h:33
const symbolst & symbols
const char gcc_builtin_headers_ia32_4[]
const char clang_builtin_headers[]
const char gcc_builtin_headers_math[]
ansi_c_parsert ansi_c_parser
const char gcc_builtin_headers_ia32[]
static bool find_pattern(const std::string &pattern, const char *header_file, std::ostream &out)
bool add(const symbolt &symbol)
Add a new symbol to the symbol table.
const char gcc_builtin_headers_arm[]
goto_programt coverage_criteriont message_handlert & message_handler
Definition: cover.cpp:66
const char gcc_builtin_headers_ia32_2[]
virtual void clear() override
Definition: ansi_c_parser.h:49
const char gcc_builtin_headers_power[]