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