CBMC
parser.h
Go to the documentation of this file.
1 /*******************************************************************\
2 
3 Module: Parser utilities
4 
5 Author: Daniel Kroening, kroening@kroening.com
6 
7 \*******************************************************************/
8 
11 
12 #ifndef CPROVER_UTIL_PARSER_H
13 #define CPROVER_UTIL_PARSER_H
14 
15 #include "expr.h"
16 #include "message.h"
17 
18 #include <filesystem>
19 #include <iosfwd>
20 #include <string>
21 #include <vector>
22 
23 class parsert
24 {
25 public:
26  std::istream *in;
27 
28  std::string this_line, last_line;
29 
30  std::vector<exprt> stack;
31 
32  explicit parsert(message_handlert &message_handler)
33  : in(nullptr),
34  log(message_handler),
35  line_no(0),
37  column(1)
38  {
39  }
40 
41  virtual ~parsert() { }
42 
43  // The following are for the benefit of the scanner
44 
45  bool read(char &ch)
46  {
47  if(!in->read(&ch, 1))
48  return false;
49 
50  if(ch=='\n')
51  {
52  last_line.swap(this_line);
53  this_line.clear();
54  }
55  else
56  this_line+=ch;
57 
58  return true;
59  }
60 
61  virtual bool parse()=0;
62 
63  bool eof()
64  {
65  return in->eof();
66  }
67 
68  void parse_error(
69  const std::string &message,
70  const std::string &before);
71 
72  void inc_line_no()
73  {
74  ++line_no;
75  column=1;
76  }
77 
78  void set_line_no(unsigned _line_no)
79  {
80  line_no=_line_no;
81  }
82 
83  void set_file(const irep_idt &file)
84  {
87  std::filesystem::current_path().string());
88  }
89 
91  {
92  return source_location.get_file();
93  }
94 
95  unsigned get_line_no() const
96  {
97  return line_no;
98  }
99 
100  unsigned get_column() const
101  {
102  return column;
103  }
104 
105  void set_column(unsigned _column)
106  {
107  column=_column;
108  }
109 
111  {
112  // Only set line number when needed, as this destroys sharing.
114  {
117  }
118 
120  }
121 
122  void set_function(const irep_idt &function)
123  {
124  source_location.set_function(function);
125  }
126 
127  void advance_column(unsigned token_width)
128  {
129  column+=token_width;
130  }
131 
132 protected:
136  unsigned column;
137 };
138 
139 exprt &_newstack(parsert &parser, unsigned &x);
140 
141 #define newstack(x) _newstack(PARSER, (x))
142 
143 #define parser_stack(x) (PARSER.stack[x])
144 #define stack_expr(x) (PARSER.stack[x])
145 #define stack_type(x) \
146  (static_cast<typet &>(static_cast<irept &>(PARSER.stack[x])))
147 
148 #define YY_INPUT(buf, result, max_size) \
149  do { \
150  for(result=0; result<max_size;) \
151  { \
152  char ch; \
153  if(!PARSER.read(ch)) /* NOLINT(readability/braces) */ \
154  { \
155  if(result==0) \
156  result=YY_NULL; \
157  break; \
158  } \
159  \
160  if(ch!='\r') /* NOLINT(readability/braces) */ \
161  { \
162  buf[result++]=ch; \
163  if(ch=='\n') /* NOLINT(readability/braces) */ \
164  { \
165  PARSER.inc_line_no(); \
166  break; \
167  } \
168  } \
169  } \
170  } while(0)
171 
172 // The following tracks the column of the token, and is nicely explained here:
173 // http://oreilly.com/linux/excerpts/9780596155971/error-reporting-recovery.html
174 
175 #define YY_USER_ACTION PARSER.advance_column(yyleng);
176 
177 #endif // CPROVER_UTIL_PARSER_H
dstringt has one field, an unsigned integer no which is an index into a static table of strings.
Definition: dstring.h:38
Base class for all expressions.
Definition: expr.h:56
source_locationt & add_source_location()
Definition: expr.h:236
Class that provides messages with a built-in verbosity 'level'.
Definition: message.h:154
Definition: parser.h:24
void advance_column(unsigned token_width)
Definition: parser.h:127
source_locationt source_location
Definition: parser.h:134
parsert(message_handlert &message_handler)
Definition: parser.h:32
std::istream * in
Definition: parser.h:26
void inc_line_no()
Definition: parser.h:72
void set_column(unsigned _column)
Definition: parser.h:105
bool eof()
Definition: parser.h:63
void set_file(const irep_idt &file)
Definition: parser.h:83
unsigned get_line_no() const
Definition: parser.h:95
std::string last_line
Definition: parser.h:28
virtual ~parsert()
Definition: parser.h:41
virtual bool parse()=0
unsigned column
Definition: parser.h:136
void set_source_location(exprt &e)
Definition: parser.h:110
messaget log
Definition: parser.h:133
std::string this_line
Definition: parser.h:28
bool read(char &ch)
Definition: parser.h:45
unsigned previous_line_no
Definition: parser.h:135
void parse_error(const std::string &message, const std::string &before)
Definition: parser.cpp:30
irep_idt get_file() const
Definition: parser.h:90
std::vector< exprt > stack
Definition: parser.h:30
unsigned line_no
Definition: parser.h:135
void set_line_no(unsigned _line_no)
Definition: parser.h:78
unsigned get_column() const
Definition: parser.h:100
void set_function(const irep_idt &function)
Definition: parser.h:122
void set_working_directory(const irep_idt &cwd)
const irep_idt & get_file() const
void set_file(const irep_idt &file)
void set_line(const irep_idt &line)
void set_function(const irep_idt &function)
exprt & _newstack(parsert &parser, unsigned &x)
Definition: parser.cpp:19