cprover
trace_automaton.cpp
Go to the documentation of this file.
1 /*******************************************************************\
2 
3 Module: Loop Acceleration
4 
5 Author: Matt Lewis
6 
7 \*******************************************************************/
8 
11 
12 #include "trace_automaton.h"
13 
14 #include <utility>
15 #include <iostream>
16 
17 #include "path.h"
18 
20 {
21 #ifdef DEBUG
22  std::cout << "NTA:\n";
23  nta.output(std::cout);
24 #endif
25 
26  determinise();
27  // minimise();
28 
29 #ifdef DEBUG
30  std::cout << "DTA:\n";
31  dta.output(std::cout);
32 #endif
33 }
34 
35 /*
36  * Build the trace automaton alphabet.
37  *
38  * The alphabet is the set of distinguishing points, i.e. the
39  * successors of any location with multiple successors.
40  */
42 {
44  {
45  const auto succs=program.get_successors(it);
46  if(succs.size()>1)
47  {
48  alphabet.insert(succs.begin(), succs.end());
49  }
50  }
51 }
52 
54 {
56 
57  for(const auto &sym : alphabet)
59 }
60 
61 /*
62  * Add a path to the trace automaton.
63  */
65 {
66  statet state;
67 
68  state=nta.add_state();
70 
71 #ifdef DEBUG
72  std::cout << "Adding path: ";
73 #endif
74 
75  for(const auto &step : path)
76  {
77  goto_programt::targett l=step.loc;
78 
79 #ifdef DEBUG
80  std::cout << ", " << l->location_number << ':'
81  << l->source_location.as_string();
82 #endif
83 
84  if(in_alphabet(l))
85  {
86 #ifdef DEBUG
87  std::cout << "(*) ";
88 #endif
89 
90  statet new_state=nta.add_state();
91  nta.add_trans(state, l, new_state);
92  state=new_state;
93  }
94  }
95 
96 #ifdef DEBUG
97  std::cout << '\n';
98 
99  std::cout << "Final state: " << state << '\n';
100 #endif
101 
102  nta.set_accepting(state);
103 }
104 
105 /*
106  * Use the subset construction (cf. the Dragon book)
107  * to convert a nondeterministic trace automaton (NTA) to
108  * a deterministic one (DTA).
109  */
111 {
112 #ifdef DEBUG
113  std::cout << "Determinising automaton with " << nta.num_states
114  << " states and " << nta.accept_states.size()
115  << " accept states and " << nta.count_transitions()
116  << " transitions\n";
117 #endif
118 
119  dstates.clear();
120  unmarked_dstates.clear();
121  dta.clear();
122 
123  state_sett init_states;
124  init_states.insert(nta.init_state);
125  epsilon_closure(init_states);
126 
127 #ifdef DEBUG
128  std::cout << "There are " << init_states.size() << " init states\n";
129 #endif
130 
131  dta.init_state=add_dstate(init_states);
132 
133  while(!unmarked_dstates.empty())
134  {
135  state_sett t;
137  assert(find_dstate(t)!=no_state);
138 
139 
140  // For each symbol a such that there is a transition
141  //
142  // s -a-> s'
143  //
144  // for some s in t, find the states that are reachable
145  // using a-transitions and add them as a new state.
146  for(alphabett::iterator it=alphabet.begin();
147  it!=alphabet.end();
148  ++it)
149  {
150  if(*it==epsilon)
151  {
152  continue;
153  }
154 
155  state_sett u;
156 
157  nta.move(t, *it, u);
158  epsilon_closure(u);
159 
160  add_dstate(u);
161  add_dtrans(t, *it, u);
162  }
163  }
164 
165  dta.trim();
166 
167 #ifdef DEBUG
168  std::cout << "Produced DTA with " << dta.num_states << " states and "
169  << dta.accept_states.size() << " accept states and "
170  << dta.count_transitions() << " transitions\n";
171 #endif
172 }
173 
175 {
176  s=unmarked_dstates.back();
177  unmarked_dstates.pop_back();
178 }
179 
180 /*
181  * Calculate the epsilon closure of a set of states in a NTA.
182  */
184 {
185  std::vector<statet> queue(states.size());
186 
187  // Initialise -- fill queue with states.
188  for(state_sett::iterator it=states.begin();
189  it!=states.end();
190  ++it)
191  {
192  queue.push_back(*it);
193  }
194 
195  // Take epsilon transitions until we can take no more.
196  while(!queue.empty())
197  {
198  statet state=queue.back();
199  state_sett next_states;
200 
201  queue.pop_back();
202 
203  nta.move(state, epsilon, next_states);
204 
205  // Check if we've arrived at any fresh states. If so, recurse on them.
206  for(state_sett::iterator it=next_states.begin();
207  it!=next_states.end();
208  ++it)
209  {
210  if(states.find(*it)==states.end())
211  {
212  // This is a new state. Add it to the state set & enqueue it.
213  states.insert(*it);
214  queue.push_back(*it);
215  }
216  }
217  }
218 }
219 
220 /*
221  * Create a new (unmarked) state in the DTA if the state has not been added
222  * before.
223  */
225 {
226  statet state_num=find_dstate(s);
227 
228  if(state_num!=no_state)
229  {
230  // We've added this state before. Don't need to do it again.
231  return state_num;
232  }
233 
234  state_num=dta.add_state();
235  dstates[s]=state_num;
236  unmarked_dstates.push_back(s);
237 
238  assert(dstates.find(s)!=dstates.end());
239 
240  for(state_sett::iterator it=s.begin();
241  it!=s.end();
242  ++it)
243  {
244  if(nta.is_accepting(*it))
245  {
246 #ifdef DEBUG
247  std::cout << "NTA state " << *it
248  << " is accepting, so accepting DTA state "
249  << state_num << '\n';
250 #endif
251 
252  dta.set_accepting(state_num);
253  break;
254  }
255  }
256 
257  return state_num;
258 }
259 
261 {
262  state_mapt::iterator it=dstates.find(s);
263 
264  if(it==dstates.end())
265  {
266  return no_state;
267  }
268  else
269  {
270  return it->second;
271  }
272 }
273 
274 /*
275  * Add a new state.
276  */
278 {
279  transitionst trans;
280  transitions.push_back(trans);
281 
282  return num_states++;
283 }
284 
285 /*
286  * Add the transition s -a-> t.
287  */
289 {
290  assert(s < transitions.size());
291  transitionst &trans=transitions[s];
292 
293  trans.insert(std::make_pair(a, t));
294 }
295 
296 /*
297  * Add a transition to the DTA.
298  */
300  state_sett &s,
302  state_sett &t)
303 {
304  statet sidx=find_dstate(s);
305  statet tidx=find_dstate(t);
306 
307  assert(sidx!=no_state);
308  assert(tidx!=no_state);
309 
310  dta.add_trans(sidx, a, tidx);
311 }
312 
314 {
315  assert(s < transitions.size());
316 
317  transitionst &trans=transitions[s];
318 
319  transition_ranget range=trans.equal_range(a);
320 
321  for(transitionst::iterator it=range.first;
322  it!=range.second;
323  ++it)
324  {
325  t.insert(it->second);
326  }
327 }
328 
330  state_sett &s,
332  state_sett &t)
333 {
334  for(const auto &state : s)
335  move(state, a, t);
336 }
337 
339 {
341 
342  for(std::size_t i=0; i < dtrans.size(); ++i)
343  {
344  automatont::transitionst &dta_transitions=dtrans[i];
345 
346  for(const auto &trans : dta_transitions)
347  {
348  goto_programt::targett l=trans.first;
349  unsigned int j=trans.second;
350 
351  // We have a transition: i -l-> j.
352  state_pairt state_pair(i, j);
353  transitions.insert(std::make_pair(l, state_pair));
354  }
355  }
356 }
357 
359 {
360  transition_tablet old_table;
361  statet new_init;
362 
363  old_table.swap(transitions);
364 
365  for(std::size_t i=0; i < old_table.size(); i++)
366  {
367  transitions.push_back(transitionst());
368  }
369 
370  if(accept_states.empty())
371  {
372  num_states=0;
373  return;
374  }
375  else if(accept_states.size()==1)
376  {
377  new_init=*(accept_states.begin());
378  }
379  else
380  {
381  // More than one accept state. Introduce a new state with
382  // epsilon transitions to each accept state.
383  new_init=add_state();
384 
385  for(const auto &s : accept_states)
386  add_trans(new_init, epsilon, s);
387  }
388 
389  std::cout << "Reversing automaton, old init=" << init_state
390  << ", new init=" << new_init << ", old accept="
391  << *(accept_states.begin()) << '/' << accept_states.size()
392  << " new accept=" << init_state << '\n';
393 
394  accept_states.clear();
395  set_accepting(init_state);
396 
397  init_state=new_init;
398 
399  for(std::size_t i=0; i < old_table.size(); i++)
400  {
401  transitionst &trans=old_table[i];
402 
403  for(const auto &t : trans)
404  {
405  goto_programt::targett l=t.first;
406  unsigned int j=t.second;
407 
408  // There was a transition i -l-> j, so add a transition
409  // j -l-> i.
410  add_trans(j, l, i);
411  }
412  }
413 }
414 
416 {
417  state_sett reachable;
418  state_sett new_states;
419 
420  reachable.insert(init_state);
421  new_states.insert(init_state);
422 
423  do
424  {
425  state_sett tmp;
426 
427  for(const auto &s : new_states)
428  {
429  transitionst &trans=transitions[s];
430 
431  for(const auto &t : trans)
432  {
433  unsigned int j=t.second;
434 
435  if(reachable.find(j)==reachable.end())
436  {
437  reachable.insert(j);
438  tmp.insert(j);
439  }
440  }
441  }
442 
443  tmp.swap(new_states);
444  }
445  while(!new_states.empty());
446 
447  for(std::size_t i=0; i < num_states; i++)
448  {
449  if(reachable.find(i)==reachable.end())
450  {
451  transitions[i]=transitionst();
452  accept_states.erase(i);
453  }
454  }
455 }
456 
457 // Produce a minimal DTA using Brzozowski's algorithm.
459 {
461  determinise();
462 
463  nta.swap(dta);
465  determinise();
466 }
467 
468 void automatont::output(std::ostream &str)
469 {
470  str << "Init: " << init_state << '\n';
471 
472  str << "Accept states: ";
473 
474  for(const auto &state : accept_states)
475  str << state << ' ';
476 
477  str << '\n';
478 
479  for(unsigned int i=0; i < transitions.size(); ++i)
480  {
481  for(const auto &trans : transitions[i])
482  {
483  goto_programt::targett l=trans.first;
484  statet j=trans.second;
485 
486  str << i << " -- " << l->location_number << " --> " << j << '\n';
487  }
488  }
489 }
490 
492 {
493  std::size_t ret=0;
494 
495  for(const auto &trans : transitions)
496  ret+=trans.size();
497 
498  return ret;
499 }
void get_transitions(sym_mapt &transitions)
void epsilon_closure(state_sett &s)
std::pair< transitionst::iterator, transitionst::iterator > transition_ranget
std::multimap< goto_programt::targett, statet > transitionst
statet num_states
bool in_alphabet(goto_programt::targett t)
Loop Acceleration.
std::vector< transitionst > transition_tablet
statet find_dstate(state_sett &s)
void swap(automatont &that)
void accept_states(state_sett &states)
std::pair< statet, statet > state_pairt
static const statet no_state
void pop_unmarked_dstate(state_sett &s)
std::list< Target > get_successors(Target target) const
statet add_dstate(state_sett &s)
void add_trans(statet s, goto_programt::targett a, statet t)
void add_dtrans(state_sett &s, goto_programt::targett a, state_sett &t)
state_sett accept_states
bool is_accepting(statet s)
std::list< path_nodet > patht
Definition: path.h:45
std::size_t count_transitions()
void build_alphabet(goto_programt &program)
void add_path(patht &path)
std::set< statet > state_sett
statet add_state()
A specialization of goto_program_templatet over goto programs in which instructions have codet type...
Definition: goto_program.h:24
Loop Acceleration.
std::vector< state_sett > unmarked_dstates
std::multimap< goto_programt::targett, state_pairt > sym_mapt
void reverse(goto_programt::targett epsilon)
void move(statet s, goto_programt::targett a, state_sett &t)
transition_tablet transitions
#define Forall_goto_program_instructions(it, program)
Definition: goto_program.h:73
goto_programt::targett epsilon
statet init_state
unsigned int statet
void output(std::ostream &str)
void set_accepting(statet s)