CBMC
Loading...
Searching...
No Matches
c_preprocess.cpp
Go to the documentation of this file.
1/*******************************************************************\
2
3Module:
4
5Author: Daniel Kroening, kroening@kroening.com
6
7\*******************************************************************/
8
9#include "c_preprocess.h"
10
11#include <util/c_types.h>
12#include <util/config.h>
13#include <util/message.h>
14#include <util/prefix.h>
15#include <util/run.h>
16#include <util/suffix.h>
17#include <util/tempfile.h>
18#include <util/unicode.h>
19
20#include <fstream>
21
22static void error_parse_line(
23 const std::string &line,
24 bool warning_only,
25 messaget &message)
26{
27 std::string error_msg=line;
29
30 if(has_prefix(line, "file "))
31 {
32 const char *tptr=line.c_str();
33 int state=0;
34 std::string file, line_no, column, _error_msg, function;
35
36 tptr+=5;
37
38 char previous=0;
39
40 while(*tptr!=0)
41 {
42 if(has_prefix(tptr, " line ") && state != 4)
43 {
44 state=1;
45 tptr+=6;
46 continue;
47 }
48 else if(has_prefix(tptr, " column ") && state != 4)
49 {
50 state=2;
51 tptr+=8;
52 continue;
53 }
54 else if(has_prefix(tptr, " function ") && state != 4)
55 {
56 state=3;
57 tptr+=10;
58 continue;
59 }
60 else if(*tptr==':' && state!=4)
61 {
62 if(tptr[1]==' ' && previous!=':')
63 {
64 state=4;
65 tptr++;
66 while(*tptr==' ') tptr++;
67 continue;
68 }
69 }
70
71 if(state==0) // file
72 file+=*tptr;
73 else if(state==1) // line number
74 line_no+=*tptr;
75 else if(state==2) // column
76 column+=*tptr;
77 else if(state==3) // function
78 function+=*tptr;
79 else if(state==4) // error message
81
82 previous=*tptr;
83
84 tptr++;
85 }
86
87 if(state==4)
88 {
89 saved_error_location.set_file(file);
90 saved_error_location.set_function(function);
91 saved_error_location.set_line(line_no);
92 saved_error_location.set_column(column);
94 }
95 }
96 else if(has_prefix(line, "In file included from "))
97 {
98 }
99 else
100 {
101 const char *tptr=line.c_str();
102 int state=0;
103 std::string file, line_no;
104
105 while(*tptr!=0)
106 {
107 if(state==0)
108 {
109 if(*tptr==':')
110 state++;
111 else
112 file+=*tptr;
113 }
114 else if(state==1)
115 {
116 if(*tptr==':')
117 state++;
118 else if(isdigit(*tptr))
119 line_no+=*tptr;
120 else
121 state=3;
122 }
123
124 tptr++;
125 }
126
127 if(state==2)
128 {
129 saved_error_location.set_file(file);
130 saved_error_location.set_function(irep_idt());
131 saved_error_location.set_line(line_no);
132 saved_error_location.set_column(irep_idt());
133 }
134 }
135
137 warning_only ? message.warning() : message.error();
139 m << error_msg << messaget::eom;
140}
141
142static void error_parse(
143 std::istream &errors,
144 bool warning_only,
145 messaget &message)
146{
147 std::string line;
148
149 while(std::getline(errors, line))
150 error_parse_line(line, warning_only, message);
151}
152
155 std::istream &instream,
156 std::ostream &outstream,
157 message_handlert &message_handler)
158{
159 temporary_filet tmp_file("tmp.stdin", ".c");
160
161 std::ofstream tmp(tmp_file());
162
163 if(!tmp)
164 {
165 messaget message(message_handler);
166 message.error() << "failed to open temporary file" << messaget::eom;
167 return true; // error
168 }
169
170 tmp << instream.rdbuf(); // copy
171
172 tmp.close(); // flush
173
174 bool result=c_preprocess(tmp_file(), outstream, message_handler);
175
176 return result;
177}
178
180static bool is_dot_i_file(const std::string &path)
181{
182 return has_suffix(path, ".i") || has_suffix(path, ".ii");
183}
184
187 const std::string &, std::ostream &, message_handlert &);
189 const std::string &, std::ostream &, message_handlert &);
191 const std::string &,
192 std::ostream &,
196 const std::string &, std::ostream &, message_handlert &);
198 const std::string &, std::ostream &, message_handlert &);
199
201 const std::string &path,
202 std::ostream &outstream,
203 message_handlert &message_handler)
204{
205 switch(config.ansi_c.preprocessor)
206 {
208 return c_preprocess_codewarrior(path, outstream, message_handler);
209
211 return
213 path, outstream, message_handler, config.ansi_c.preprocessor);
214
216 return
218 path, outstream, message_handler, config.ansi_c.preprocessor);
219
221 return c_preprocess_visual_studio(path, outstream, message_handler);
222
224 return c_preprocess_arm(path, outstream, message_handler);
225
227 return c_preprocess_none(path, outstream, message_handler);
228 }
229
230 // not reached
231 return true;
232}
233
236 const std::string &file,
237 std::ostream &outstream,
238 message_handlert &message_handler)
239{
240 // check extension
241 if(is_dot_i_file(file))
242 return c_preprocess_none(file, outstream, message_handler);
243
244 messaget message(message_handler);
245
246 // use Visual Studio's CL
247
248 temporary_filet stderr_file("tmp.stderr", "");
249 temporary_filet command_file_name("tmp.cl-cmd", "");
250
251 {
252 std::ofstream command_file(command_file_name());
253
254 // This marks the command file as UTF-8, which Visual Studio
255 // understands.
256 command_file << char(0xef) << char(0xbb) << char(0xbf);
257
258 command_file << "/nologo" << '\n';
259 command_file << "/E" << '\n';
260
261 // This option will make CL produce utf-8 output, as
262 // opposed to 8-bit with some code page.
263 // It only works on Visual Studio 2015 or newer.
264 command_file << "/source-charset:utf-8" << '\n';
265
266 command_file << "/D__CPROVER__" << "\n";
267 command_file << "/D__WORDSIZE=" << config.ansi_c.pointer_width << "\n";
268
270 {
271 command_file << "\"/D__PTRDIFF_TYPE__=long long int\"" << "\n";
272 // yes, both _WIN32 and _WIN64 get defined
273 command_file << "/D_WIN64" << "\n";
274 }
275 else if(config.ansi_c.int_width == 16 && config.ansi_c.pointer_width == 32)
276 {
277 // 16-bit LP32 is an artificial architecture we simulate when using --16
280 "Pointer difference expected to be long int typed");
281 command_file << "/D__PTRDIFF_TYPE__=long" << '\n';
282 }
283 else
284 {
287 "Pointer difference expected to be int typed");
288 command_file << "/D__PTRDIFF_TYPE__=int" << "\n";
289 }
290
291 if(config.ansi_c.char_is_unsigned)
292 command_file << "/J" << "\n"; // This causes _CHAR_UNSIGNED to be defined
293
294 for(const auto &define : config.ansi_c.defines)
295 command_file << "/D" << shell_quote(define) << "\n";
296
297 for(const auto &include_path : config.ansi_c.include_paths)
298 command_file << "/I" << shell_quote(include_path) << "\n";
299
300 for(const auto &include_file : config.ansi_c.include_files)
301 command_file << "/FI" << shell_quote(include_file) << "\n";
302
303 // Finally, the file to be preprocessed
304 // (this is already in UTF-8).
305 command_file << shell_quote(file) << "\n";
306 }
307
308 int result =
309 run("cl", {"cl", "@" + command_file_name()}, "", outstream, stderr_file());
310
311 // errors/warnings
312 std::ifstream stderr_stream(stderr_file());
313 error_parse(stderr_stream, result==0, message);
314
315 if(result!=0)
316 {
317 message.error() << "CL Preprocessing failed" << messaget::eom;
318 return true;
319 }
320
321 return false;
322}
323
326 std::istream &instream,
327 std::ostream &outstream)
328{
329 // CodeWarrior prepends some header to the file,
330 // marked with '#' signs.
331 // We skip over it.
332 //
333 // CodeWarrior has an ugly way of marking lines, e.g.:
334 //
335 // /* #line 1 "__ppc_eabi_init.cpp" /* stack depth 0 */
336 //
337 // We remove the initial '/* ' prefix
338
339 std::string line;
340
341 while(instream)
342 {
343 std::getline(instream, line);
344
345 if(line.size()>=2 &&
346 line[0]=='#' && (line[1]=='#' || line[1]==' ' || line[1]=='\t'))
347 {
348 // skip the line!
349 }
350 else if(line.size()>=3 &&
351 line[0]=='/' && line[1]=='*' && line[2]==' ')
352 {
353 outstream << line.c_str()+3 << "\n"; // strip the '/* '
354 }
355 else
356 outstream << line << "\n";
357 }
358}
359
362 const std::string &file,
363 std::ostream &outstream,
364 message_handlert &message_handler)
365{
366 // check extension
367 if(is_dot_i_file(file))
368 return c_preprocess_none(file, outstream, message_handler);
369
370 // preprocessing
371 messaget message(message_handler);
372
373 temporary_filet stderr_file("tmp.stderr", "");
374
375 std::vector<std::string> command = {
376 "mwcceppc", "-E", "-P", "-D__CPROVER__", "-ppopt", "line", "-ppopt full"};
377
378 for(const auto &define : config.ansi_c.defines)
379 command.push_back(" -D" + define);
380
381 for(const auto &include_path : config.ansi_c.include_paths)
382 command.push_back(" -I" + include_path);
383
384 for(const auto &include_file : config.ansi_c.include_files)
385 {
386 command.push_back(" -include");
387 command.push_back(include_file);
388 }
389
390 for(const auto &opt : config.ansi_c.preprocessor_options)
391 command.push_back(opt);
392
393 temporary_filet tmpi("tmp.cl", "");
394 command.push_back(file);
395 command.push_back("-o");
396 command.push_back(tmpi());
397
398 int result = run(command[0], command, "", "", stderr_file());
399
400 std::ifstream stream_i(tmpi());
401
402 if(stream_i)
403 {
405
406 stream_i.close();
407 }
408 else
409 {
410 message.error() << "Preprocessing failed (fopen failed)"
411 << messaget::eom;
412 return true;
413 }
414
415 // errors/warnings
416 std::ifstream stderr_stream(stderr_file());
417 error_parse(stderr_stream, result==0, message);
418
419 if(result!=0)
420 {
421 message.error() << "Preprocessing failed" << messaget::eom;
422 return true;
423 }
424
425 return false;
426}
427
430 const std::string &file,
431 std::ostream &outstream,
432 message_handlert &message_handler,
434{
435 // check extension
436 if(is_dot_i_file(file))
437 return c_preprocess_none(file, outstream, message_handler);
438
439 // preprocessing
440 messaget message(message_handler);
441
442 temporary_filet stderr_file("tmp.stderr", "");
443
444 std::vector<std::string> argv;
445
447 argv.push_back("clang");
448 else
449 argv.push_back("gcc");
450
451 argv.push_back("-E");
452 argv.push_back("-D__CPROVER__");
453
454 const irep_idt &arch = config.ansi_c.arch;
455
456 if(config.ansi_c.pointer_width == 16)
457 {
458 if(arch == "i386" || arch == "x86_64" || arch == "x32")
459 argv.push_back("-m16");
460 else if(arch.starts_with("mips"))
461 argv.push_back("-mips16");
462 }
463 else if(config.ansi_c.pointer_width == 32)
464 {
465 if(arch == "i386" || arch == "x86_64")
466 argv.push_back("-m32");
467 else if(arch == "x32")
468 argv.push_back("-mx32");
469 else if(arch.starts_with("mips"))
470 argv.push_back("-mabi=32");
471 else if(arch == "powerpc" || arch == "ppc64" || arch == "ppc64le")
472 argv.push_back("-m32");
473 else if(arch == "s390" || arch == "s390x")
474 argv.push_back("-m31"); // yes, 31, not 32!
475 else if(arch == "sparc" || arch == "sparc64")
476 argv.push_back("-m32");
477 }
478 else if(config.ansi_c.pointer_width == 64)
479 {
480 if(arch == "i386" || arch == "x86_64" || arch == "x32")
481 argv.push_back("-m64");
482 else if(arch.starts_with("mips"))
483 argv.push_back("-mabi=64");
484 else if(arch == "powerpc" || arch == "ppc64" || arch == "ppc64le")
485 argv.push_back("-m64");
486 else if(arch == "s390" || arch == "s390x")
487 argv.push_back("-m64");
488 else if(arch == "sparc" || arch == "sparc64")
489 argv.push_back("-m64");
490 }
491
492 // The width of wchar_t depends on the OS!
493 if(config.ansi_c.wchar_t_width == config.ansi_c.short_int_width)
494 argv.push_back("-fshort-wchar");
495
496 if(config.ansi_c.char_is_unsigned)
497 argv.push_back("-funsigned-char");
498
500 argv.push_back("-nostdinc");
501
502 // Set the standard
503 if(
504 has_suffix(file, ".cpp") || has_suffix(file, ".CPP") ||
506 has_suffix(file, ".C") ||
507#endif
508 has_suffix(file, ".c++") || has_suffix(file, ".C++") ||
509 has_suffix(file, ".cp") || has_suffix(file, ".CP") ||
510 has_suffix(file, ".cc") || has_suffix(file, ".cxx"))
511 {
512 switch(config.cpp.cpp_standard)
513 {
515#if defined(__OpenBSD__)
517 argv.push_back("-std=c++98");
518 else
519#endif
520 argv.push_back("-std=gnu++98");
521 break;
522
524#if defined(__OpenBSD__)
526 argv.push_back("-std=c++03");
527 else
528#endif
529 argv.push_back("-std=gnu++03");
530 break;
531
533#if defined(__OpenBSD__)
535 argv.push_back("-std=c++11");
536 else
537#endif
538 argv.push_back("-std=gnu++11");
539 break;
540
542#if defined(__OpenBSD__)
544 argv.push_back("-std=c++14");
545 else
546#endif
547 argv.push_back("-std=gnu++14");
548 break;
549
551#if defined(__OpenBSD__)
553 argv.push_back("-std=c++17");
554 else
555#endif
556 argv.push_back("-std=gnu++17");
557 break;
558 }
559 }
560 else
561 {
562 switch(config.ansi_c.c_standard)
563 {
565#if defined(__OpenBSD__)
567 argv.push_back("-std=c89");
568 else
569#endif
570 argv.push_back("-std=gnu89");
571 break;
572
574#if defined(__OpenBSD__)
576 argv.push_back("-std=c99");
577 else
578#endif
579 argv.push_back("-std=gnu99");
580 break;
581
583#if defined(__OpenBSD__)
585 argv.push_back("-std=c11");
586 else
587#endif
588 argv.push_back("-std=gnu11");
589 break;
590
592#if defined(__OpenBSD__)
594 argv.push_back("-std=c17");
595 else
596#endif
597 argv.push_back("-std=gnu17");
598 break;
599
601#if defined(__OpenBSD__)
603 argv.push_back("-std=c2x");
604 else
605#endif
606 argv.push_back("-std=gnu2x");
607 break;
608 }
609 }
610
611 for(const auto &define : config.ansi_c.defines)
612 argv.push_back("-D" + define);
613
614 for(const auto &include_path : config.ansi_c.include_paths)
615 argv.push_back("-I" + include_path);
616
617 for(const auto &include_file : config.ansi_c.include_files)
618 {
619 argv.push_back("-include");
620 argv.push_back(include_file);
621 }
622
623 for(const auto &opt : config.ansi_c.preprocessor_options)
624 argv.push_back(opt);
625
626 int result;
627
628 #if 0
629 // the following forces the mode
630 switch(config.ansi_c.mode)
631 {
632 case configt::ansi_ct::flavourt::GCC_C: command+=" -x c"; break;
633 case configt::ansi_ct::flavourt::GCC_CPP: command+=" -x c++"; break;
634 default:
635 {
636 }
637 }
638 #endif
639
640 // the file that is to be preprocessed
641 argv.push_back(file);
642
643 // execute clang or gcc
644 result = run(argv[0], argv, "", outstream, stderr_file());
645
646 // errors/warnings
647 std::ifstream stderr_stream(stderr_file());
648 error_parse(stderr_stream, result==0, message);
649
650 if(result!=0)
651 {
652 message.error() << "GCC preprocessing failed" << messaget::eom;
653 return true;
654 }
655
656 return false;
657}
658
661 const std::string &file,
662 std::ostream &outstream,
663 message_handlert &message_handler)
664{
665 // check extension
666 if(is_dot_i_file(file))
667 return c_preprocess_none(file, outstream, message_handler);
668
669 // preprocessing using armcc
670 messaget message(message_handler);
671
672 temporary_filet stderr_file("tmp.stderr", "");
673
674 std::vector<std::string> argv;
675
676 argv.push_back("armcc");
677 argv.push_back("-E");
678 argv.push_back("-D__CPROVER__");
679
681 argv.push_back("--bigend");
682 else
683 argv.push_back("--littleend");
684
685 if(config.ansi_c.char_is_unsigned)
686 argv.push_back("--unsigned_chars");
687 else
688 argv.push_back("--signed_chars");
689
690 // Set the standard
691 // https://developer.arm.com/documentation/101458/2404/Standards-support/Supported-C-C---standards-in-Arm-C-C---Compiler
692 switch(config.ansi_c.c_standard)
693 {
695 argv.push_back("--c90");
696 break;
697
699 argv.push_back("--c99");
700 break;
701
703 argv.push_back("--c11");
704 break;
705
707 argv.push_back("--c17");
708 break;
709
711 // C23 is not yet supported by armcc
712 argv.push_back("--c17");
713 break;
714 }
715
716 for(const auto &define : config.ansi_c.defines)
717 argv.push_back("-D" + define);
718
719 for(const auto &include_path : config.ansi_c.include_paths)
720 argv.push_back("-I" + include_path);
721
722 // the file that is to be preprocessed
723 argv.push_back(file);
724
725 int result;
726
727 // execute armcc
728 result = run(argv[0], argv, "", outstream, stderr_file());
729
730 // errors/warnings
731 std::ifstream stderr_stream(stderr_file());
732 error_parse(stderr_stream, result==0, message);
733
734 if(result!=0)
735 {
736 message.error() << "ARMCC preprocessing failed" << messaget::eom;
737 return true;
738 }
739
740 return false;
741}
742
745 const std::string &file,
746 std::ostream &outstream,
747 message_handlert &message_handler)
748{
749 std::ifstream infile(widen_if_needed(file));
750
751 if(!infile)
752 {
753 messaget message(message_handler);
754 message.error() << "failed to open '" << file << "'" << messaget::eom;
755 return true;
756 }
757
759 {
760 // special treatment for "/* #line"
762 }
763 else
764 {
765 char ch;
766
767 while(infile.read(&ch, 1))
768 outstream << ch;
769 }
770
771 return false;
772}
773
775const char c_test_program[]=
776 "#include <stdlib.h>\n"
777 "\n"
778 "int main() { }\n";
779
781{
782 std::ostringstream out;
783 std::istringstream in(c_test_program);
784
785 return c_preprocess(in, out, message_handler);
786}
configt config
Definition config.cpp:25
bool c_preprocess_visual_studio(const std::string &, std::ostream &, message_handlert &)
ANSI-C preprocessing.
bool c_preprocess_arm(const std::string &, std::ostream &, message_handlert &)
ANSI-C preprocessing.
bool c_preprocess_none(const std::string &, std::ostream &, message_handlert &)
ANSI-C preprocessing.
static void error_parse(std::istream &errors, bool warning_only, messaget &message)
const char c_test_program[]
tests ANSI-C preprocessing
bool c_preprocess_codewarrior(const std::string &, std::ostream &, message_handlert &)
ANSI-C preprocessing.
static void error_parse_line(const std::string &line, bool warning_only, messaget &message)
void postprocess_codewarrior(std::istream &instream, std::ostream &outstream)
post-processing specifically for CodeWarrior
bool c_preprocess(std::istream &instream, std::ostream &outstream, message_handlert &message_handler)
ANSI-C preprocessing.
bool test_c_preprocessor(message_handlert &message_handler)
bool c_preprocess_gcc_clang(const std::string &, std::ostream &, message_handlert &, configt::ansi_ct::preprocessort)
ANSI-C preprocessing.
static bool is_dot_i_file(const std::string &path)
ANSI-C preprocessing.
signedbv_typet signed_long_int_type()
Definition c_types.cpp:72
signedbv_typet signed_int_type()
Definition c_types.cpp:22
signedbv_typet pointer_diff_type()
Definition c_types.cpp:220
signedbv_typet signed_long_long_int_type()
Definition c_types.cpp:79
ait supplies three of the four components needed: an abstract interpreter (in this case handling func...
Definition ai.h:562
struct configt::cppt cpp
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:38
bool starts_with(const char *s) const
equivalent of as_string().starts_with(s)
Definition dstring.h:95
source_locationt source_location
Definition message.h:239
Class that provides messages with a built-in verbosity 'level'.
Definition message.h:154
mstreamt & error() const
Definition message.h:391
mstreamt & warning() const
Definition message.h:396
static eomt eom
Definition message.h:289
bool has_prefix(const std::string &s, const std::string &prefix)
Definition converter.cpp:13
int isdigit(int c)
Definition ctype.c:24
int run(const std::string &what, const std::vector< std::string > &argv)
Definition run.cpp:49
std::string shell_quote(const std::string &src)
quote a string for bash and CMD
Definition run.cpp:452
#define DATA_INVARIANT(CONDITION, REASON)
This condition should be used to document that assumptions that are made on goto_functions,...
Definition invariant.h:534
bool has_suffix(const std::string &s, const std::string &suffix)
Definition suffix.h:17
#define widen_if_needed(s)
Definition unicode.h:28
dstringt irep_idt