cprover
document_properties.cpp
Go to the documentation of this file.
1 /*******************************************************************\
2 
3 Module: Subgoal Documentation
4 
5 Author: Daniel Kroening, kroening@kroening.com
6 
7 \*******************************************************************/
8 
11 
12 #include "document_properties.h"
13 
14 #include <fstream>
15 
16 #include <util/string2int.h>
17 
18 #include <ansi-c/expr2c.h>
19 
21 
22 #define MAXWIDTH 62
23 
25 {
26 public:
28  const goto_functionst &_goto_functions,
29  std::ostream &_out):
30  goto_functions(_goto_functions),
31  out(_out),
32  format(HTML)
33  {
34  }
35 
36  void html()
37  {
38  format=HTML;
39  doit();
40  }
41 
42  void latex()
43  {
44  format=LATEX;
45  doit();
46  }
47 
48 private:
50  std::ostream &out;
51 
52  struct linet
53  {
54  std::string text;
56  };
57 
58  static void strip_space(std::list<linet> &lines);
59 
60  void get_code(
61  const source_locationt &source_location,
62  std::string &dest);
63 
64  struct doc_claimt
65  {
66  std::set<irep_idt> comment_set;
67  };
68 
69  enum { HTML, LATEX } format;
70 
71  void doit();
72 };
73 
74 void document_propertiest::strip_space(std::list<linet> &lines)
75 {
76  unsigned strip=50;
77 
78  for(std::list<linet>::const_iterator it=lines.begin();
79  it!=lines.end(); it++)
80  {
81  for(std::size_t j=0; j<strip && j<it->text.size(); j++)
82  if(it->text[j]!=' ')
83  {
84  strip=j;
85  break;
86  }
87  }
88 
89  if(strip!=0)
90  {
91  for(std::list<linet>::iterator it=lines.begin();
92  it!=lines.end(); it++)
93  {
94  if(it->text.size()>=strip)
95  it->text=std::string(it->text, strip, std::string::npos);
96 
97  if(it->text.size()>=MAXWIDTH)
98  it->text=std::string(it->text, 0, MAXWIDTH);
99  }
100  }
101 }
102 
103 std::string escape_latex(const std::string &s, bool alltt)
104 {
105  std::string dest;
106 
107  for(std::size_t i=0; i<s.size(); i++)
108  {
109  if(s[i]=='\\' || s[i]=='{' || s[i]=='}')
110  dest+="\\";
111 
112  if(!alltt &&
113  (s[i]=='_' || s[i]=='$' || s[i]=='~' ||
114  s[i]=='^' || s[i]=='%' || s[i]=='#' ||
115  s[i]=='&'))
116  dest+="\\";
117 
118  dest+=s[i];
119  }
120 
121  return dest;
122 }
123 
124 std::string escape_html(const std::string &s)
125 {
126  std::string dest;
127 
128  for(std::size_t i=0; i<s.size(); i++)
129  {
130  switch(s[i])
131  {
132  case '&': dest+="&amp;"; break;
133  case '<': dest+="&lt;"; break;
134  case '>': dest+="&gt;"; break;
135  default: dest+=s[i];
136  }
137  }
138 
139  return dest;
140 }
141 
142 bool is_empty(const std::string &s)
143 {
144  for(std::size_t i=0; i<s.size(); i++)
145  if(isgraph(s[i]))
146  return false;
147 
148  return true;
149 }
150 
152  const source_locationt &source_location,
153  std::string &dest)
154 {
155  dest="";
156 
157  const irep_idt &file=source_location.get_file();
158  const irep_idt &line=source_location.get_line();
159 
160  if(file=="" || line=="")
161  return;
162 
163  std::ifstream in(id2string(file));
164 
165  if(!in)
166  {
167  dest+="ERROR: unable to open ";
168  dest+=id2string(file);
169  dest+="\n";
170  return;
171  }
172 
173  int line_int=unsafe_string2int(id2string(line));
174 
175  int line_start=line_int-3,
176  line_end=line_int+3;
177 
178  if(line_start<=1)
179  line_start=1;
180 
181  // skip line_start-1 lines
182 
183  for(int l=0; l<line_start-1; l++)
184  {
185  std::string tmp;
186  std::getline(in, tmp);
187  }
188 
189  // read till line_end
190 
191  std::list<linet> lines;
192 
193  for(int l=line_start; l<=line_end && in; l++)
194  {
195  lines.push_back(linet());
196 
197  std::string &line=lines.back().text;
198  std::getline(in, line);
199 
200  if(!line.empty() && line[line.size()-1]=='\r')
201  line.resize(line.size()-1);
202 
203  lines.back().line_number=l;
204  }
205 
206  // remove empty lines at the end and at the beginning
207 
208  for(std::list<linet>::iterator it=lines.begin();
209  it!=lines.end();)
210  {
211  if(is_empty(it->text))
212  it=lines.erase(it);
213  else
214  break;
215  }
216 
217  for(std::list<linet>::iterator it=lines.end();
218  it!=lines.begin();)
219  {
220  it--;
221 
222  if(is_empty(it->text))
223  it=lines.erase(it);
224  else
225  break;
226  }
227 
228  // strip space
229  strip_space(lines);
230 
231  // build dest
232 
233  for(std::list<linet>::iterator it=lines.begin();
234  it!=lines.end(); it++)
235  {
236  std::string line_no=std::to_string(it->line_number);
237 
238  std::string tmp;
239 
240  switch(format)
241  {
242  case LATEX:
243  while(line_no.size()<4)
244  line_no=" "+line_no;
245 
246  line_no+" ";
247 
248  tmp+=escape_latex(it->text, true);
249 
250  if(it->line_number==line_int)
251  tmp="{\\ttb{}"+tmp+"}";
252 
253  break;
254 
255  case HTML:
256  while(line_no.size()<4)
257  line_no="&nbsp;"+line_no;
258 
259  line_no+"&nbsp;&nbsp;";
260 
261  tmp+=escape_html(it->text);
262 
263  if(it->line_number==line_int)
264  tmp="<em>"+tmp+"</em>";
265 
266  break;
267  }
268 
269  dest+=tmp+"\n";
270  }
271 }
272 
274 {
275  typedef std::map<source_locationt, doc_claimt> claim_sett;
276  claim_sett claim_set;
277 
279  {
280  const goto_programt &goto_program=f_it->second.body;
281 
283  {
284  if(i_it->is_assert())
285  {
286  source_locationt new_source_location;
287 
288  new_source_location.set_file(i_it->source_location.get_file());
289  new_source_location.set_line(i_it->source_location.get_line());
290  new_source_location.set_function(i_it->source_location.get_function());
291 
292  claim_set[new_source_location].comment_set.
293  insert(i_it->source_location.get_comment());
294  }
295  }
296  }
297 
298  for(claim_sett::const_iterator it=claim_set.begin();
299  it!=claim_set.end(); it++)
300  {
301  std::string code;
302  const source_locationt &source_location=it->first;
303 
304  get_code(source_location, code);
305 
306  switch(format)
307  {
308  case LATEX:
309  out << "\\claimlocation{File "
310  << escape_latex(source_location.get_string("file"), false)
311  << " function "
312  << escape_latex(source_location.get_string("function"), false)
313  << "}\n";
314 
315  out << '\n';
316 
317  for(std::set<irep_idt>::const_iterator
318  s_it=it->second.comment_set.begin();
319  s_it!=it->second.comment_set.end();
320  s_it++)
321  out << "\\claim{" << escape_latex(id2string(*s_it), false)
322  << "}\n";
323 
324  out << '\n';
325 
326  out << "\\begin{alltt}\\claimcode\n"
327  << code
328  << "\\end{alltt}\n";
329 
330  out << '\n';
331  out << '\n';
332  break;
333 
334  case HTML:
335  out << "<div class=\"claim\">\n"
336  << "<div class=\"location\">File "
337  << escape_html(source_location.get_string("file"))
338  << " function "
339  << escape_html(source_location.get_string("function"))
340  << "</div>\n";
341 
342  out << '\n';
343 
344  for(std::set<irep_idt>::const_iterator
345  s_it=it->second.comment_set.begin();
346  s_it!=it->second.comment_set.end();
347  s_it++)
348  out << "<div class=\"description\">\n"
349  << escape_html(id2string(*s_it)) << '\n'
350  << "</div>\n";
351 
352  out << '\n';
353 
354  out << "<div class=\"code\">\n"
355  << code
356  << "</div> <!-- code -->\n";
357 
358  out << "</div> <!-- claim -->\n";
359  out << '\n';
360  break;
361  }
362  }
363 }
364 
366  const goto_modelt &goto_model,
367  std::ostream &out)
368 {
369  document_propertiest(goto_model.goto_functions, out).html();
370 }
371 
373  const goto_modelt &goto_model,
374  std::ostream &out)
375 {
376  document_propertiest(goto_model.goto_functions, out).latex();
377 }
std::string escape_latex(const std::string &s, bool alltt)
void set_function(const irep_idt &function)
const std::string & id2string(const irep_idt &d)
Definition: irep.h:44
enum document_propertiest::@3 format
document_propertiest(const goto_functionst &_goto_functions, std::ostream &_out)
Documentation of Properties.
Symbol Table + CFG.
const irep_idt & get_line() const
void set_file(const irep_idt &file)
#define MAXWIDTH
void set_line(const irep_idt &line)
void get_code(const source_locationt &source_location, std::string &dest)
dstringt has one field, an unsigned integer no which is an index into a static table of strings...
Definition: dstring.h:33
const goto_functionst & goto_functions
void document_properties_latex(const goto_modelt &goto_model, std::ostream &out)
void document_properties_html(const goto_modelt &goto_model, std::ostream &out)
A generic container class for the GOTO intermediate representation of one function.
Definition: goto_program.h:70
std::string escape_html(const std::string &s)
const irep_idt & get_file() const
static void strip_space(std::list< linet > &lines)
std::string to_string(const string_constraintt &expr)
Used for debug printing.
bool is_empty(const std::string &s)
const std::string & get_string(const irep_namet &name) const
Definition: irep.h:272
goto_programt & goto_program
Definition: cover.cpp:63
#define forall_goto_functions(it, functions)
#define forall_goto_program_instructions(it, program)
Definition: goto_program.h:735
int unsafe_string2int(const std::string &str, int base)
Definition: string2int.cpp:64
goto_functionst goto_functions
GOTO functions.
Definition: goto_model.h:32
Definition: kdev_t.h:19