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 
277  for(const auto &gf_entry : goto_functions.function_map)
278  {
279  const goto_programt &goto_program = gf_entry.second.body;
280 
281  for(const auto &instruction : goto_program.instructions)
282  {
283  if(instruction.is_assert())
284  {
285  const auto &source_location = instruction.source_location;
286  source_locationt new_source_location;
287 
288  new_source_location.set_file(source_location.get_file());
289  new_source_location.set_line(source_location.get_line());
290  new_source_location.set_function(source_location.get_function());
291 
292  claim_set[new_source_location].comment_set.insert(
293  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  const source_locationt &source_location=it->first;
302 
303  std::string code = get_code(source_location);
304 
305  switch(format)
306  {
307  case LATEX:
308  out << "\\claimlocation{File "
309  << escape_latex(source_location.get_string("file"), false)
310  << " function "
311  << escape_latex(source_location.get_string("function"), false)
312  << "}\n";
313 
314  out << '\n';
315 
316  for(std::set<irep_idt>::const_iterator
317  s_it=it->second.comment_set.begin();
318  s_it!=it->second.comment_set.end();
319  s_it++)
320  out << "\\claim{" << escape_latex(id2string(*s_it), false)
321  << "}\n";
322 
323  out << '\n';
324 
325  out << "\\begin{alltt}\\claimcode\n"
326  << code
327  << "\\end{alltt}\n";
328 
329  out << '\n';
330  out << '\n';
331  break;
332 
333  case HTML:
334  out << "<div class=\"claim\">\n"
335  << "<div class=\"location\">File "
336  << escape_html(source_location.get_string("file"))
337  << " function "
338  << escape_html(source_location.get_string("function"))
339  << "</div>\n";
340 
341  out << '\n';
342 
343  for(std::set<irep_idt>::const_iterator
344  s_it=it->second.comment_set.begin();
345  s_it!=it->second.comment_set.end();
346  s_it++)
347  out << "<div class=\"description\">\n"
348  << escape_html(id2string(*s_it)) << '\n'
349  << "</div>\n";
350 
351  out << '\n';
352 
353  out << "<div class=\"code\">\n"
354  << code
355  << "</div> <!-- code -->\n";
356 
357  out << "</div> <!-- claim -->\n";
358  out << '\n';
359  break;
360  }
361  }
362 }
363 
365  const goto_modelt &goto_model,
366  std::ostream &out)
367 {
368  document_propertiest(goto_model.goto_functions, out).html();
369 }
370 
372  const goto_modelt &goto_model,
373  std::ostream &out)
374 {
375  document_propertiest(goto_model.goto_functions, out).latex();
376 }
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::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
goto_functionst::function_map
function_mapt function_map
Definition: goto_functions.h:27
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
document_propertiest::LATEX
@ LATEX
Definition: document_properties.cpp:67
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:49
expr2c.h
document_properties_latex
void document_properties_latex(const goto_modelt &goto_model, std::ostream &out)
Definition: document_properties.cpp:371
source_locationt::set_file
void set_file(const irep_idt &file)
Definition: source_location.h:96
document_propertiest::format
enum document_propertiest::@5 format
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
goto_programt::instructions
instructionst instructions
The list of instructions in the goto program.
Definition: goto_program.h:569
irept::get_string
const std::string & get_string(const irep_namet &name) const
Definition: irep.h:420
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
goto_programt
A generic container class for the GOTO intermediate representation of one function.
Definition: goto_program.h:74
source_locationt::get_file
const irep_idt & get_file() const
Definition: source_location.h:36
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:364
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