cprover
unified_diff.cpp
Go to the documentation of this file.
1 /*******************************************************************\
2 
3 Module: Unified diff (using LCSS) of goto functions
4 
5 Author: Michael Tautschnig
6 
7 Date: April 2016
8 
9 \*******************************************************************/
10 
13 
14 #include "unified_diff.h"
15 
16 #include <algorithm>
17 
19 
21  const goto_modelt &model_new):
22  old_goto_functions(model_old.goto_functions),
23  ns_old(model_old.symbol_table),
24  new_goto_functions(model_new.goto_functions),
25  ns_new(model_new.symbol_table)
26 {
27 }
28 
30  const irep_idt &function,
31  goto_program_difft &dest) const
32 {
33  dest.clear();
34 
35  differences_mapt::const_iterator entry=
36  differences_map.find(function);
37  if(entry==differences_map.end())
38  return;
39 
40  goto_functionst::function_mapt::const_iterator old_fit=
41  old_goto_functions.function_map.find(function);
42  goto_functionst::function_mapt::const_iterator new_fit=
43  new_goto_functions.function_map.find(function);
44 
45  goto_programt empty;
46 
47  const goto_programt &old_goto_program=
48  old_fit==old_goto_functions.function_map.end() ?
49  empty :
50  old_fit->second.body;
51  const goto_programt &new_goto_program=
52  new_fit==new_goto_functions.function_map.end() ?
53  empty :
54  new_fit->second.body;
55 
56  get_diff(
57  function,
58  old_goto_program,
59  new_goto_program,
60  entry->second,
61  dest);
62 }
63 
65  const irep_idt &identifier,
66  const goto_programt &old_goto_program,
67  const goto_programt &new_goto_program,
68  const differencest &differences,
69  goto_program_difft &dest) const
70 {
71  goto_programt::instructionst::const_iterator old_it=
72  old_goto_program.instructions.begin();
73  goto_programt::instructionst::const_iterator new_it=
74  new_goto_program.instructions.begin();
75 
76  for(differencest::const_reverse_iterator rit=differences.rbegin();
77  rit!=differences.rend();
78  ++rit)
79  {
80  switch(*rit)
81  {
82  case differencet::SAME:
83  dest.push_back(std::make_pair(new_it, differencet::SAME));
84  assert(old_it!=old_goto_program.instructions.end());
85  ++old_it;
86  assert(new_it!=new_goto_program.instructions.end());
87  ++new_it;
88  break;
90  dest.push_back(std::make_pair(old_it, differencet::DELETED));
91  assert(old_it!=old_goto_program.instructions.end());
92  ++old_it;
93  break;
94  case differencet::NEW:
95  dest.push_back(std::make_pair(new_it, differencet::NEW));
96  assert(new_it!=new_goto_program.instructions.end());
97  ++new_it;
98  break;
99  }
100  }
101 }
102 
104  const irep_idt &identifier,
105  const goto_programt &old_goto_program,
106  const goto_programt &new_goto_program,
107  const differencest &differences,
108  std::ostream &os) const
109 {
110  goto_program_difft diff;
111  get_diff(
112  identifier,
113  old_goto_program,
114  new_goto_program,
115  differences,
116  diff);
117 
118  bool has_diff=false;
119  for(const auto &d : diff)
120  {
121  if(d.second!=differencet::SAME)
122  {
123  has_diff=true;
124  break;
125  }
126  }
127  if(!has_diff)
128  return;
129 
130  os << "/** " << identifier << " **/\n";
131 
132  for(const auto &d : diff)
133  {
134  switch(d.second)
135  {
136  case differencet::SAME:
137  os << ' ';
138  new_goto_program.output_instruction(
139  ns_new,
140  identifier,
141  os,
142  d.first);
143  break;
145  os << '-';
146  old_goto_program.output_instruction(
147  ns_old,
148  identifier,
149  os,
150  d.first);
151  break;
152  case differencet::NEW:
153  os << '+';
154  new_goto_program.output_instruction(
155  ns_new,
156  identifier,
157  os,
158  d.first);
159  break;
160  }
161  }
162 }
163 
165  const irep_idt &identifier,
166  const goto_programt &old_goto_program,
167  const goto_programt &new_goto_program,
168  differencest &differences) const
169 {
170  std::size_t old_count=old_goto_program.instructions.size();
171  std::size_t new_count=new_goto_program.instructions.size();
172 
173  differences.reserve(old_count+new_count);
174 
175  // skip common prefix
176  goto_programt::instructionst::const_iterator old_it=
177  old_goto_program.instructions.begin();
178  goto_programt::instructionst::const_iterator new_it=
179  new_goto_program.instructions.begin();
180 
181  for( ;
182  old_it!=old_goto_program.instructions.end() &&
183  new_it!=new_goto_program.instructions.end();
184  ++old_it, ++new_it)
185  {
186  if(!instructions_equal(*old_it, *new_it))
187  break;
188 
189  --old_count;
190  --new_count;
191  }
192  // old_it, new_it are now iterators to the first instructions that
193  // differ
194 
195  // skip common suffix
196  goto_programt::instructionst::const_iterator old_rit=
197  old_goto_program.instructions.end();
198  goto_programt::instructionst::const_iterator new_rit=
199  new_goto_program.instructions.end();
200 
201  while(old_rit!=old_it && new_rit!=new_it)
202  {
203  --old_rit;
204  --new_rit;
205 
206  if(!instructions_equal(*old_rit, *new_rit))
207  {
208  ++old_rit;
209  ++new_rit;
210  break;
211  }
212 
213  --old_count;
214  --new_count;
215  differences.push_back(differencet::SAME);
216  }
217  // old_rit, new_rit are now iterators to the first instructions of
218  // the common tail
219 
220  if(old_count==0 && new_count==0)
221  return;
222 
223  // apply longest common subsequence (LCSS)
224  typedef std::vector<std::vector<std::size_t> > lcss_matrixt;
225  lcss_matrixt lcss_matrix(
226  old_count+1,
227  std::vector<size_t>(new_count+1, 0));
228 
229  // fill the matrix
230  std::size_t i=1, j=1;
231  for(goto_programt::instructionst::const_iterator old_it2=old_it;
232  old_it2!=old_rit;
233  ++old_it2)
234  {
235  j=1;
236  for(goto_programt::instructionst::const_iterator new_it2=new_it;
237  new_it2!=new_rit;
238  ++new_it2)
239  {
240  if(instructions_equal(*old_it2, *new_it2))
241  lcss_matrix[i][j]+=lcss_matrix[i-1][j-1]+1;
242  else
243  lcss_matrix[i][j]=
244  std::max(lcss_matrix[i][j-1], lcss_matrix[i-1][j]);
245 
246  ++j;
247  }
248  ++i;
249  }
250 
251  #if 0
252  std::cerr << "old_count=" << old_count << '\n';
253  std::cerr << "new_count=" << new_count << '\n';
254  for(i=0; i<=old_count; ++i)
255  {
256  for(j=0; j<=new_count; ++j)
257  {
258  std::cerr << " ";
259  if(lcss_matrix[i][j]<10)
260  std::cerr << " ";
261  std::cerr << lcss_matrix[i][j];
262  }
263  std::cerr << '\n';
264  }
265  #endif
266 
267  // backtracking
268  // note that the order in case of multiple possible matches of
269  // the if-clauses is important to provide a convenient ordering
270  // of - and + lines (- goes before +)
271  i=old_count;
272  j=new_count;
273  --old_rit;
274  --new_rit;
275 
276  while(i>0 || j>0)
277  {
278  if(i==0)
279  {
280  differences.push_back(differencet::NEW);
281  --j;
282  --new_rit;
283  }
284  else if(j==0)
285  {
286  differences.push_back(differencet::DELETED);
287  --i;
288  --old_rit;
289  }
290  else if(instructions_equal(*old_rit, *new_rit))
291  {
292  differences.push_back(differencet::SAME);
293  --i;
294  --old_rit;
295  --j;
296  --new_rit;
297  }
298  else if(lcss_matrix[i][j-1]<lcss_matrix[i][j])
299  {
300  differences.push_back(differencet::DELETED);
301  --i;
302  --old_rit;
303  }
304  else
305  {
306  differences.push_back(differencet::NEW);
307  --j;
308  --new_rit;
309  }
310  }
311 
312  // add common prefix (if any)
313  for( ; old_it!=old_goto_program.instructions.begin(); --old_it)
314  differences.push_back(differencet::SAME);
315 }
316 
318  const irep_idt &identifier,
319  const goto_programt &old_goto_program,
320  const goto_programt &new_goto_program)
321 {
322  differencest &differences=differences_map[identifier];
323  differences.clear();
324 
325  if(old_goto_program.instructions.empty() ||
326  new_goto_program.instructions.empty())
327  {
328  if(new_goto_program.instructions.empty())
329  differences.resize(
330  old_goto_program.instructions.size(),
332  else
333  differences.resize(
334  new_goto_program.instructions.size(),
336  }
337  else
338  lcss(identifier, old_goto_program, new_goto_program, differences);
339 }
340 
342 {
343  typedef std::map<irep_idt,
344  goto_functionst::function_mapt::const_iterator>
345  function_mapt;
346 
347  function_mapt old_funcs, new_funcs;
348 
350  old_funcs.insert(std::make_pair(it->first, it));
352  new_funcs.insert(std::make_pair(it->first, it));
353 
354  goto_programt empty;
355 
356  function_mapt::const_iterator ito=old_funcs.begin();
357  for(function_mapt::const_iterator itn=new_funcs.begin();
358  itn!=new_funcs.end();
359  ++itn)
360  {
361  for( ;
362  ito!=old_funcs.end() && ito->first<itn->first;
363  ++ito)
364  unified_diff(ito->first, ito->second->second.body, empty);
365 
366  if(ito==old_funcs.end() || itn->first<ito->first)
367  unified_diff(itn->first, empty, itn->second->second.body);
368  else
369  {
370  assert(ito->first==itn->first);
371  unified_diff(
372  itn->first,
373  ito->second->second.body,
374  itn->second->second.body);
375  ++ito;
376  }
377  }
378  for( ; ito!=old_funcs.end(); ++ito)
379  unified_diff(ito->first, ito->second->second.body, empty);
380 
381  return !differences_map.empty();
382 }
383 
384 void unified_difft::output(std::ostream &os) const
385 {
386  goto_programt empty;
387 
388  for(const std::pair<irep_idt, differencest> &p : differences_map)
389  {
390  goto_functionst::function_mapt::const_iterator f1=
391  old_goto_functions.function_map.find(p.first);
392  goto_functionst::function_mapt::const_iterator f2=
393  new_goto_functions.function_map.find(p.first);
394 
395  output_diff(
396  p.first,
397  f1==old_goto_functions.function_map.end()?empty:f1->second.body,
398  f2==new_goto_functions.function_map.end()?empty:f2->second.body,
399  p.second,
400  os);
401  }
402 }
instructionst instructions
The list of instructions in the goto program.
const goto_functionst & old_goto_functions
Definition: unified_diff.h:57
void output_diff(const irep_idt &identifier, const goto_programt &old_goto_program, const goto_programt &new_goto_program, const differencest &differences, std::ostream &os) const
Symbol Table + CFG.
unified_difft(const goto_modelt &model_old, const goto_modelt &model_new)
std::vector< differencet > differencest
Definition: unified_diff.h:62
const namespacet ns_old
Definition: unified_diff.h:58
differences_mapt differences_map
Definition: unified_diff.h:65
Unified diff (using LCSS) of goto functions.
A specialization of goto_program_templatet over goto programs in which instructions have codet type...
Definition: goto_program.h:24
void output(std::ostream &os) const
void unified_diff(const irep_idt &identifier, const goto_programt &old_goto_program, const goto_programt &new_goto_program)
bool instructions_equal(const goto_programt::instructiont &ins1, const goto_programt::instructiont &ins2, bool recurse=true) const
Definition: unified_diff.h:92
dstringt irep_idt
Definition: irep.h:32
std::list< std::pair< goto_programt::const_targett, differencet > > goto_program_difft
Definition: unified_diff.h:50
void get_diff(const irep_idt &function, goto_program_difft &dest) const
#define forall_goto_functions(it, functions)
std::ostream & output_instruction(const class namespacet &ns, const irep_idt &identifier, std::ostream &out, instructionst::const_iterator it) const
See below.
const goto_functionst & new_goto_functions
Definition: unified_diff.h:59
void lcss(const irep_idt &identifier, const goto_programt &old_goto_program, const goto_programt &new_goto_program, differencest &differences) const
const namespacet ns_new
Definition: unified_diff.h:60