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/prefix.h>
17 #include <util/string_utils.h>
18 
19 #include <ostream>
20 #include <sstream>
21 
22 static 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 
42 static bool convert(
43  const irep_idt &identifier,
44  const std::ostringstream &s,
45  symbol_tablet &symbol_table,
46  message_handlert &message_handler)
47 {
48  std::istringstream in(s.str());
49 
51  ansi_c_parser.set_file(ID_built_in);
52  ansi_c_parser.in=&in;
53  ansi_c_parser.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 
61  if(ansi_c_parser.parse())
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_tablet &symbol_table,
101  message_handlert &mh)
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
113  if(find_pattern(pattern, cprover_builtin_headers, s))
114  return convert(identifier, s, symbol_table, mh);
115 
116  // this is Visual C/C++ only
118  {
119  if(find_pattern(pattern, windows_builtin_headers, s))
120  return convert(identifier, s, symbol_table, mh);
121  }
122 
123  // ARM stuff
125  {
126  if(find_pattern(pattern, arm_builtin_headers, s))
127  return convert(identifier, s, symbol_table, mh);
128  }
129 
130  // CW stuff
132  {
133  if(find_pattern(pattern, cw_builtin_headers, s))
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 
146  if(find_pattern(pattern, gcc_builtin_headers_math, s))
147  return convert(identifier, s, symbol_table, mh);
148 
150  return convert(identifier, s, symbol_table, mh);
151 
152  if(find_pattern(pattern, gcc_builtin_headers_omp, s))
153  return convert(identifier, s, symbol_table, mh);
154 
155  if(find_pattern(pattern, gcc_builtin_headers_tm, s))
156  return convert(identifier, s, symbol_table, mh);
157 
158  if(find_pattern(pattern, gcc_builtin_headers_ubsan, s))
159  return convert(identifier, s, symbol_table, mh);
160 
161  if(find_pattern(pattern, clang_builtin_headers, s))
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  {
168  if(find_pattern(pattern, gcc_builtin_headers_ia32, s))
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  }
180  else if(config.ansi_c.arch=="arm64" ||
181  config.ansi_c.arch=="armel" ||
182  config.ansi_c.arch=="armhf" ||
183  config.ansi_c.arch=="arm")
184  {
185  if(find_pattern(pattern, gcc_builtin_headers_arm, s))
186  return convert(identifier, s, symbol_table, mh);
187  }
188  else if(config.ansi_c.arch=="mips64el" ||
189  config.ansi_c.arch=="mipsn32el" ||
190  config.ansi_c.arch=="mipsel" ||
191  config.ansi_c.arch=="mips64" ||
192  config.ansi_c.arch=="mipsn32" ||
193  config.ansi_c.arch=="mips")
194  {
195  if(find_pattern(pattern, gcc_builtin_headers_mips, s))
196  return convert(identifier, s, symbol_table, mh);
197  }
198  else if(config.ansi_c.arch=="powerpc" ||
199  config.ansi_c.arch=="ppc64" ||
200  config.ansi_c.arch=="ppc64le")
201  {
202  if(find_pattern(pattern, gcc_builtin_headers_power, s))
203  return convert(identifier, s, symbol_table, mh);
204  }
205  }
206 
207  return true;
208 }
messaget
Class that provides messages with a built-in verbosity 'level'.
Definition: message.h:155
ansi_c_parser
ansi_c_parsert ansi_c_parser
Definition: ansi_c_parser.cpp:13
dstringt
dstringt has one field, an unsigned integer no which is an index into a static table of strings.
Definition: dstring.h:37
symbol_tablet
The symbol table.
Definition: symbol_table.h:20
ansi_c_typecheck.h
ANSI-C Language Type Checking.
gcc_builtin_headers_omp
const char gcc_builtin_headers_omp[]
Definition: ansi_c_internal_additions.cpp:38
configt::ansi_ct::for_has_scope
bool for_has_scope
Definition: config.h:45
gcc_builtin_headers_arm
const char gcc_builtin_headers_arm[]
Definition: ansi_c_internal_additions.cpp:72
string_utils.h
configt::ansi_ct::flavourt::CODEWARRIOR
@ CODEWARRIOR
ansi_c_parsert::cpp98
bool cpp98
Definition: ansi_c_parser.h:79
windows_builtin_headers
const char windows_builtin_headers[]
Definition: ansi_c_internal_additions.cpp:107
configt::ansi_ct::os
ost os
Definition: config.h:80
prefix.h
builtin_factory
bool builtin_factory(const irep_idt &identifier, symbol_tablet &symbol_table, message_handlert &mh)
Check whether given identifier is a compiler built-in.
Definition: builtin_factory.cpp:98
gcc_builtin_headers_mem_string
const char gcc_builtin_headers_mem_string[]
Definition: ansi_c_internal_additions.cpp:33
messaget::eom
static eomt eom
Definition: message.h:297
configt::ansi_c
struct configt::ansi_ct ansi_c
configt::ansi_ct::flavourt::ARM
@ ARM
configt::ansi_ct::flavourt::CLANG
@ CLANG
gcc_builtin_headers_ubsan
const char gcc_builtin_headers_ubsan[]
Definition: ansi_c_internal_additions.cpp:48
message
static const char * message(const static_verifier_resultt::statust &status)
Makes a status message string from a status.
Definition: static_verifier.cpp:74
clang_builtin_headers
const char clang_builtin_headers[]
Definition: ansi_c_internal_additions.cpp:97
strip_string
std::string strip_string(const std::string &s)
Remove all whitespace characters from either end of a string.
Definition: string_utils.cpp:22
convert
static bool convert(const irep_idt &identifier, const std::ostringstream &s, symbol_tablet &symbol_table, message_handlert &message_handler)
Definition: builtin_factory.cpp:42
parsert::in
std::istream * in
Definition: parser.h:26
id2string
const std::string & id2string(const irep_idt &d)
Definition: irep.h:44
find_pattern
static bool find_pattern(const std::string &pattern, const char *header_file, std::ostream &out)
Definition: builtin_factory.cpp:22
ansi_c_parsert::clear
virtual void clear() override
Definition: ansi_c_parser.h:49
ansi_c_internal_additions.h
ansi_c_scanner_init
void ansi_c_scanner_init()
gcc_builtin_headers_ia32
const char gcc_builtin_headers_ia32[]
Definition: ansi_c_internal_additions.cpp:53
messaget::set_message_handler
virtual void set_message_handler(message_handlert &_message_handler)
Definition: message.h:179
ansi_c_internal_additions
void ansi_c_internal_additions(std::string &code)
Definition: ansi_c_internal_additions.cpp:153
gcc_builtin_headers_ia32_2
const char gcc_builtin_headers_ia32_2[]
Definition: ansi_c_internal_additions.cpp:57
cw_builtin_headers
const char cw_builtin_headers[]
Definition: ansi_c_internal_additions.cpp:92
configt::ansi_ct::arch
irep_idt arch
Definition: config.h:85
configt::ansi_ct::ost::OS_WIN
@ OS_WIN
message_handlert
Definition: message.h:28
arm_builtin_headers
const char arm_builtin_headers[]
Definition: ansi_c_internal_additions.cpp:87
builtin_factory.h
config
configt config
Definition: config.cpp:24
ansi_c_parsert::cpp11
bool cpp11
Definition: ansi_c_parser.h:79
ansi_c_parsert::mode
modet mode
Definition: ansi_c_parser.h:76
gcc_builtin_headers_mips
const char gcc_builtin_headers_mips[]
Definition: ansi_c_internal_additions.cpp:77
symbol_table_baset::add
bool add(const symbolt &symbol)
Add a new symbol to the symbol table.
Definition: symbol_table_base.cpp:18
configt::ansi_ct::mode
flavourt mode
Definition: config.h:116
cprover_builtin_headers
const char cprover_builtin_headers[]
Definition: ansi_c_internal_additions.cpp:102
ansi_c_parsert::parse_tree
ansi_c_parse_treet parse_tree
Definition: ansi_c_parser.h:30
gcc_builtin_headers_power
const char gcc_builtin_headers_power[]
Definition: ansi_c_internal_additions.cpp:82
symbol_table_baset::symbols
const symbolst & symbols
Read-only field, used to look up symbols given their names.
Definition: symbol_table_base.h:30
gcc_builtin_headers_ia32_3
const char gcc_builtin_headers_ia32_3[]
Definition: ansi_c_internal_additions.cpp:60
ansi_c_parsert::parse
virtual bool parse() override
Definition: ansi_c_parser.h:44
gcc_builtin_headers_tm
const char gcc_builtin_headers_tm[]
Definition: ansi_c_internal_additions.cpp:43
ansi_c_typecheck
bool ansi_c_typecheck(ansi_c_parse_treet &ansi_c_parse_tree, symbol_tablet &symbol_table, const std::string &module, message_handlert &message_handler)
Definition: ansi_c_typecheck.cpp:22
config.h
configt::ansi_ct::flavourt::GCC
@ GCC
gcc_builtin_headers_ia32_4
const char gcc_builtin_headers_ia32_4[]
Definition: ansi_c_internal_additions.cpp:63
has_prefix
bool has_prefix(const std::string &s, const std::string &prefix)
Definition: converter.cpp:13
gcc_builtin_headers_generic
const char gcc_builtin_headers_generic[]
Definition: ansi_c_internal_additions.cpp:23
ansi_c_parser.h
ansi_c_parsert::for_has_scope
bool for_has_scope
Definition: ansi_c_parser.h:82
parsert::set_file
void set_file(const irep_idt &file)
Definition: parser.h:85
gcc_builtin_headers_math
const char gcc_builtin_headers_math[]
Definition: ansi_c_internal_additions.cpp:28