cprover
accelerate.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 "accelerate.h"
13 
14 #include <analyses/natural_loops.h>
15 
17 
18 #include <util/std_expr.h>
19 #include <util/arith_tools.h>
20 #include <util/find_symbols.h>
21 
22 #include <ansi-c/expr2c.h>
23 
24 #include <iostream>
25 #include <list>
26 
27 #include "path.h"
28 #include "polynomial_accelerator.h"
31 #include "overflow_instrumenter.h"
32 #include "util.h"
33 
35  goto_programt::targett loop_header)
36 {
38  natural_loops.loop_map[loop_header];
39  goto_programt::targett back_jump=loop_header;
40 
41  for(natural_loops_mutablet::natural_loopt::iterator it=loop.begin();
42  it!=loop.end();
43  ++it)
44  {
46  if(t->is_goto() &&
47  t->guard.is_true() &&
48  t->targets.size()==1 &&
49  t->targets.front()==loop_header &&
50  t->location_number > back_jump->location_number)
51  {
52  back_jump=t;
53  }
54  }
55 
56  return back_jump;
57 }
58 
60 {
62  natural_loops.loop_map[loop_header];
63 
64  for(natural_loops_mutablet::natural_loopt::iterator it=loop.begin();
65  it!=loop.end();
66  ++it)
67  {
68  const goto_programt::targett &t=*it;
69 
70  if(t->is_backwards_goto())
71  {
72  if(t->targets.size()!=1 ||
73  t->get_target()!=loop_header)
74  {
75  return true;
76  }
77  }
78 
79  if(t!=loop_header &&
81  {
82  return true;
83  }
84  }
85 
86  return false;
87 }
88 
90 {
91  pathst loop_paths, exit_paths;
92  goto_programt::targett back_jump=find_back_jump(loop_header);
93  int num_accelerated=0;
94  std::list<path_acceleratort> accelerators;
96  natural_loops.loop_map[loop_header];
97 
98  if(contains_nested_loops(loop_header))
99  {
100  // For now, only accelerate innermost loops.
101 #ifdef DEBUG
102  std::cout << "Not accelerating an outer loop\n";
103 #endif
104  return 0;
105  }
106 
107  goto_programt::targett overflow_loc;
108  make_overflow_loc(loop_header, back_jump, overflow_loc);
109  program.update();
110 
111 #if 1
112  enumerating_loop_accelerationt acceleration(
114  symbol_table,
116  program,
117  loop,
118  loop_header,
120 #else
122  acceleration(symbol_table, goto_functions, program, loop, loop_header);
123 #endif
124 
125  path_acceleratort accelerator;
126 
127  while(acceleration.accelerate(accelerator) &&
128  (accelerate_limit < 0 ||
129  num_accelerated < accelerate_limit))
130  {
131  // set_dirty_vars(accelerator);
132 
133  if(is_underapproximate(accelerator))
134  {
135  // We have some underapproximated variables -- just punt for now.
136 #ifdef DEBUG
137  std::cout << "Not inserting accelerator because of underapproximation\n";
138 #endif
139 
140  continue;
141  }
142 
143  accelerators.push_back(accelerator);
144  num_accelerated++;
145 
146 #ifdef DEBUG
147  std::cout << "Accelerated path:\n";
148  output_path(accelerator.path, program, ns, std::cout);
149 
150  std::cout << "Accelerator has "
151  << accelerator.pure_accelerator.instructions.size()
152  << " instructions\n";
153 #endif
154  }
155 
157  program.insert_before_swap(loop_header, skip);
158 
159  goto_programt::targett new_inst=loop_header;
160  ++new_inst;
161 
162  loop.insert(new_inst);
163 
164 
165  std::cout << "Overflow loc is " << overflow_loc->location_number << '\n';
166  std::cout << "Back jump is " << back_jump->location_number << '\n';
167 
168  for(std::list<path_acceleratort>::iterator it=accelerators.begin();
169  it!=accelerators.end();
170  ++it)
171  {
172  subsumed_patht inserted(it->path);
173 
174  insert_accelerator(loop_header, back_jump, *it, inserted);
175  subsumed.push_back(inserted);
176  num_accelerated++;
177  }
178 
179  return num_accelerated;
180 }
181 
183  goto_programt::targett &loop_header,
184  goto_programt::targett &back_jump,
185  path_acceleratort &accelerator,
186  subsumed_patht &subsumed_path)
187 {
189  loop_header,
190  back_jump,
191  accelerator.pure_accelerator,
192  subsumed_path.accelerator);
193 
194  if(!accelerator.overflow_path.instructions.empty())
195  {
197  loop_header, back_jump, accelerator.overflow_path, subsumed_path.residue);
198  }
199 }
200 
201 /*
202  * Insert a looping path (usually an accelerator) into a goto-program,
203  * beginning at loop_header and jumping back to loop_header via back_jump.
204  * Stores the locations at which the looping path was added in inserted_path.
205  *
206  * THIS DESTROYS looping_path!!
207  */
209  goto_programt::targett &loop_header,
210  goto_programt::targett &back_jump,
211  goto_programt &looping_path,
212  patht &inserted_path)
213 {
214  goto_programt::targett loop_body=loop_header;
215  ++loop_body;
216 
218  jump->make_goto(
219  loop_body,
221 
222  program.destructive_insert(loop_body, looping_path);
223 
224  jump=program.insert_before(loop_body);
225  jump->make_goto(back_jump, true_exprt());
226 
227  for(goto_programt::targett t=loop_header;
228  t!=loop_body;
229  ++t)
230  {
231  inserted_path.push_back(path_nodet(t));
232  }
233 
234  inserted_path.push_back(path_nodet(back_jump));
235 }
236 
238  goto_programt::targett loop_header,
239  goto_programt::targett &loop_end,
240  goto_programt::targett &overflow_loc)
241 {
242  symbolt overflow_sym=utils.fresh_symbol("accelerate::overflow", bool_typet());
243  const exprt &overflow_var=overflow_sym.symbol_expr();
245  natural_loops.loop_map[loop_header];
246  overflow_instrumentert instrumenter(program, overflow_var, symbol_table);
247 
248  for(natural_loops_mutablet::natural_loopt::iterator it=loop.begin();
249  it!=loop.end();
250  ++it)
251  {
254 
255  instrumenter.add_overflow_checks(*it, added);
256  loop.insert(added.begin(), added.end());
257  }
258 
260  t->make_assignment();
261  t->code=code_assignt(overflow_var, false_exprt());
262  t->swap(*loop_header);
263  loop.insert(t);
264  overflow_locs[loop_header].push_back(t);
265 
267  overflow_loc=program.insert_after(loop_end);
268  *overflow_loc=s;
269  overflow_loc->swap(*loop_end);
270  loop.insert(overflow_loc);
271 
273  g.guard=not_exprt(overflow_var);
274  g.targets.push_back(overflow_loc);
276  *t2=g;
277  t2->swap(*loop_end);
278  overflow_locs[overflow_loc].push_back(t2);
279  loop.insert(t2);
280 
281  goto_programt::targett tmp=overflow_loc;
282  overflow_loc=loop_end;
283  loop_end=tmp;
284 }
285 
287 {
288  trace_automatont automaton(program);
289 
290  for(subsumed_pathst::iterator it=subsumed.begin();
291  it!=subsumed.end();
292  ++it)
293  {
294  if(!it->subsumed.empty())
295  {
296 #ifdef DEBUG
298  std::cout << "Restricting path:\n";
299  output_path(it->subsumed, program, ns, std::cout);
300 #endif
301 
302  automaton.add_path(it->subsumed);
303  }
304 
305  patht double_accelerator;
306  patht::iterator jt=double_accelerator.begin();
307  double_accelerator.insert(
308  jt, it->accelerator.begin(), it->accelerator.end());
309  double_accelerator.insert(
310  jt, it->accelerator.begin(), it->accelerator.end());
311 
312 #ifdef DEBUG
314  std::cout << "Restricting path:\n";
315  output_path(double_accelerator, program, ns, std::cout);
316 #endif
317  automaton.add_path(double_accelerator);
318  }
319 
320  std::cout << "Building trace automaton...\n";
321 
322  automaton.build();
323  insert_automaton(automaton);
324 }
325 
327 {
328  for(std::set<exprt>::iterator it=accelerator.dirty_vars.begin();
329  it!=accelerator.dirty_vars.end();
330  ++it)
331  {
332  expr_mapt::iterator jt=dirty_vars_map.find(*it);
333  exprt dirty_var;
334 
335  if(jt==dirty_vars_map.end())
336  {
338  symbolt new_sym=utils.fresh_symbol("accelerate::dirty", bool_typet());
339  dirty_var=new_sym.symbol_expr();
340  dirty_vars_map[*it]=dirty_var;
341  }
342  else
343  {
344  dirty_var=jt->second;
345  }
346 
347 #ifdef DEBUG
348  std::cout << "Setting dirty flag " << expr2c(dirty_var, ns)
349  << " for " << expr2c(*it, ns) << '\n';
350 #endif
351 
352  accelerator.pure_accelerator.add_instruction(ASSIGN)->code =
353  code_assignt(dirty_var, true_exprt());
354  }
355 }
356 
358 {
359  for(expr_mapt::iterator it=dirty_vars_map.begin();
360  it!=dirty_vars_map.end();
361  ++it)
362  {
364  assign.code=code_assignt(it->second, false_exprt());
366  }
367 
369 
371  it!=program.instructions.end();
372  it=next)
373  {
374  next=it;
375  ++next;
376 
377  // If this is an assign to a tracked variable, clear the dirty flag.
378  // Note: this order of insertions means that we assume each of the read
379  // variables is clean _before_ clearing any dirty flags.
380  if(it->is_assign())
381  {
382  exprt &lhs=it->code.op0();
383  expr_mapt::iterator dirty_var=dirty_vars_map.find(lhs);
384 
385  if(dirty_var!=dirty_vars_map.end())
386  {
388  clear_flag.code=code_assignt(dirty_var->second, false_exprt());
389  program.insert_before_swap(it, clear_flag);
390  }
391  }
392 
393  // Find which symbols are read, i.e. those appearing in a guard or on
394  // the right hand side of an assignment. Assume each is not dirty.
395  find_symbols_sett read;
396 
397  find_symbols(it->guard, read);
398 
399  if(it->is_assign())
400  {
401  find_symbols(it->code.op1(), read);
402  }
403 
404  for(find_symbols_sett::iterator jt=read.begin();
405  jt!=read.end();
406  ++jt)
407  {
408  const exprt &var=ns.lookup(*jt).symbol_expr();
409  expr_mapt::iterator dirty_var=dirty_vars_map.find(var);
410 
411  if(dirty_var==dirty_vars_map.end())
412  {
413  continue;
414  }
415 
417  not_dirty.guard=not_exprt(dirty_var->second);
418  program.insert_before_swap(it, not_dirty);
419  }
420  }
421 }
422 
424 {
425  for(std::set<exprt>::iterator it=accelerator.dirty_vars.begin();
426  it!=accelerator.dirty_vars.end();
427  ++it)
428  {
429  if(it->id()==ID_symbol && it->type() == bool_typet())
430  {
431  const irep_idt &id=to_symbol_expr(*it).get_identifier();
432  const symbolt &sym=*symbol_table.lookup(id);
433 
434  if(sym.module=="scratch")
435  {
436  continue;
437  }
438  }
439 
440 #ifdef DEBUG
441  std::cout << "Underapproximate variable: " << expr2c(*it, ns) << '\n';
442 #endif
443  return true;
444  }
445 
446  return false;
447 }
448 
449 symbolt acceleratet::make_symbol(std::string name, typet type)
450 {
451  symbolt ret;
452  ret.module="accelerate";
453  ret.name=name;
454  ret.base_name=name;
455  ret.pretty_name=name;
456  ret.type=type;
457 
458  symbol_table.add(ret);
459 
460  return ret;
461 }
462 
464 {
465 #if 0
467  code_declt code(sym);
468 
469  decl->make_decl();
470  decl->code=code;
471 #endif
472 }
473 
475 {
476  decl(sym, t);
477 
479  code_assignt code(sym, init);
480 
481  assign->make_assignment();
482  assign->code=code;
483 }
484 
486 {
487  symbolt state_sym=make_symbol("trace_automaton::state",
489  symbolt next_state_sym=make_symbol("trace_automaton::next_state",
491  symbol_exprt state=state_sym.symbol_expr();
492  symbol_exprt next_state=next_state_sym.symbol_expr();
493 
494  trace_automatont::sym_mapt transitions;
495  state_sett accept_states;
496 
497  automaton.get_transitions(transitions);
498  automaton.accept_states(accept_states);
499 
500  std::cout
501  << "Inserting trace automaton with "
502  << automaton.num_states() << " states, "
503  << accept_states.size() << " accepting states and "
504  << transitions.size() << " transitions\n";
505 
506  // Declare the variables we'll use to encode the state machine.
508  decl(state, t, from_integer(automaton.init_state(), state.type()));
509  decl(next_state, t);
510 
511  // Now for each program location that appears as a symbol in the
512  // trace automaton, add the appropriate code to drive the state
513  // machine.
514  for(const auto &sym : automaton.alphabet)
515  {
517  trace_automatont::sym_range_pairt p=transitions.equal_range(sym);
518 
519  build_state_machine(p.first, p.second, accept_states, state, next_state,
520  state_machine);
521 
522  program.insert_before_swap(sym, state_machine);
523  }
524 }
525 
527  trace_automatont::sym_mapt::iterator begin,
528  trace_automatont::sym_mapt::iterator end,
529  state_sett &accept_states,
530  symbol_exprt state,
531  symbol_exprt next_state,
532  scratch_programt &state_machine)
533 {
534  std::map<unsigned int, unsigned int> successor_counts;
535  unsigned int max_count=0;
536  unsigned int likely_next=0;
537 
538  // Optimisation: find the most common successor state and initialise
539  // next_state to that value. This reduces the size of the state machine
540  // driver substantially.
541  for(trace_automatont::sym_mapt::iterator p=begin; p!=end; ++p)
542  {
543  trace_automatont::state_pairt state_pair=p->second;
544  unsigned int to=state_pair.second;
545  unsigned int count=0;
546 
547  if(successor_counts.find(to)==successor_counts.end())
548  {
549  count=1;
550  }
551  else
552  {
553  count=successor_counts[to] + 1;
554  }
555 
556  successor_counts[to]=count;
557 
558  if(count > max_count)
559  {
560  max_count=count;
561  likely_next=to;
562  }
563  }
564 
565  // Optimisation: if there is only one possible successor state, just
566  // jump straight to it instead of driving the whole machine.
567  if(successor_counts.size()==1)
568  {
569  if(accept_states.find(likely_next)!=accept_states.end())
570  {
571  // It's an accept state. Just assume(false).
572  state_machine.assume(false_exprt());
573  }
574  else
575  {
576  state_machine.assign(state,
577  from_integer(likely_next, next_state.type()));
578  }
579 
580  return;
581  }
582 
583  state_machine.assign(next_state,
584  from_integer(likely_next, next_state.type()));
585 
586  for(trace_automatont::sym_mapt::iterator p=begin; p!=end; ++p)
587  {
588  trace_automatont::state_pairt state_pair=p->second;
589  unsigned int from=state_pair.first;
590  unsigned int to=state_pair.second;
591 
592  if(to==likely_next)
593  {
594  continue;
595  }
596 
597  // We're encoding the transition
598  //
599  // from -loc-> to
600  //
601  // which we encode by inserting:
602  //
603  // next_state=(state==from) ? to : next_state;
604  //
605  // just before loc.
606  equal_exprt guard(state, from_integer(from, state.type()));
607  if_exprt rhs(guard, from_integer(to, next_state.type()), next_state);
608  state_machine.assign(next_state, rhs);
609  }
610 
611  // Update the state and assume(false) if we've hit an accept state.
612  state_machine.assign(state, next_state);
613 
614  for(state_sett::iterator it=accept_states.begin();
615  it!=accept_states.end();
616  ++it)
617  {
618  state_machine.assume(
619  not_exprt(equal_exprt(state, from_integer(*it, state.type()))));
620  }
621 }
622 
624 {
625  int num_accelerated=0;
626 
627  for(natural_loops_mutablet::loop_mapt::iterator it =
628  natural_loops.loop_map.begin();
629  it!=natural_loops.loop_map.end();
630  ++it)
631  {
632  goto_programt::targett t=it->first;
633  num_accelerated += accelerate_loop(t);
634  }
635 
636  program.update();
637 
638  if(num_accelerated > 0)
639  {
640  std::cout << "Engaging crush mode...\n";
641 
642  restrict_traces();
643  // add_dirty_checks();
644  program.update();
645 
646  std::cout << "Crush mode engaged.\n";
647  }
648 
649  return num_accelerated;
650 }
651 
653  goto_modelt &goto_model,
654  message_handlert &message_handler,
655  bool use_z3)
656 {
657  Forall_goto_functions(it, goto_model.goto_functions)
658  {
659  std::cout << "Accelerating function " << it->first << '\n';
660  acceleratet accelerate(
661  it->second.body, goto_model, message_handler, use_z3);
662 
663  int num_accelerated=accelerate.accelerate_loops();
664 
665  if(num_accelerated > 0)
666  {
667  std::cout << "Added " << num_accelerated
668  << " accelerator(s)\n";
669  }
670  }
671 }
exprt guard
Guard for gotos, assume, assert.
Definition: goto_program.h:193
void get_transitions(sym_mapt &transitions)
expr_mapt dirty_vars_map
Definition: accelerate.h:125
The type of an expression, extends irept.
Definition: type.h:27
irep_idt name
The unique identifier.
Definition: symbol.h:40
void insert_automaton(trace_automatont &automaton)
Definition: accelerate.cpp:485
Loop Acceleration.
void update()
Update all indices.
Boolean negation.
Definition: std_expr.h:3308
void make_overflow_loc(goto_programt::targett loop_header, goto_programt::targett &loop_end, goto_programt::targett &overflow_loc)
Definition: accelerate.cpp:237
void insert_before_swap(targett target)
Insertion that preserves jumps to "target".
Definition: goto_program.h:477
std::list< targett > targetst
Definition: goto_program.h:416
targett assign(const exprt &lhs, const exprt &rhs)
natural_loops_mutablet natural_loops
Definition: accelerate.h:117
static const int accelerate_limit
Definition: accelerate.h:56
unsigned num_states()
targett insert_before(const_targett target)
Insertion before the instruction pointed-to by the given instruction iterator target.
Definition: goto_program.h:510
exprt & op0()
Definition: expr.h:84
void insert_looping_path(goto_programt::targett &loop_header, goto_programt::targett &back_jump, goto_programt &looping_path, patht &inserted_path)
Definition: accelerate.cpp:208
goto_functionst & goto_functions
Definition: accelerate.h:114
patht residue
Definition: subsumed.h:30
bool contains_nested_loops(goto_programt::targett &loop_header)
Definition: accelerate.cpp:59
const irep_idt & get_identifier() const
Definition: std_expr.h:176
Goto Programs with Functions.
message_handlert & message_handler
Definition: accelerate.h:59
int accelerate_loop(goto_programt::targett &loop_header)
Definition: accelerate.cpp:89
The trinary if-then-else operator.
Definition: std_expr.h:3427
irep_idt module
Name of module the symbol belongs to.
Definition: symbol.h:43
irep_idt pretty_name
Language-specific display name.
Definition: symbol.h:52
typet & type()
Return the type of the expression.
Definition: expr.h:68
void accept_states(state_sett &states)
void set_dirty_vars(path_acceleratort &accelerator)
Definition: accelerate.cpp:326
The Boolean type.
Definition: std_types.h:28
Symbol table entry.
Definition: symbol.h:27
subsumed_pathst subsumed
Definition: accelerate.h:118
std::pair< statet, statet > state_pairt
symbol_tablet & symbol_table
Definition: accelerate.h:115
targetst targets
The list of successor instructions.
Definition: goto_program.h:203
goto_programt overflow_path
Definition: accelerator.h:64
Equality.
Definition: std_expr.h:1484
This class represents an instruction in the GOTO intermediate representation.
Definition: goto_program.h:178
void add_dirty_checks()
Definition: accelerate.cpp:357
void accelerate_functions(goto_modelt &goto_model, message_handlert &message_handler, bool use_z3)
Definition: accelerate.cpp:652
std::pair< sym_mapt::iterator, sym_mapt::iterator > sym_range_pairt
class symbol_exprt symbol_expr() const
Produces a symbol_exprt for a symbol.
Definition: symbol.cpp:121
The Boolean constant true.
Definition: std_expr.h:4443
unsignedbv_typet unsigned_poly_type()
Definition: util.cpp:25
patht accelerator
Definition: subsumed.h:29
instructionst::iterator targett
Definition: goto_program.h:414
A codet representing the declaration of a local variable.
Definition: std_code.h:352
targett assume(const exprt &guard)
symbolt fresh_symbol(std::string base, typet type)
goto_programt & program
Definition: accelerate.h:113
instructionst instructions
The list of instructions in the goto program.
Definition: goto_program.h:420
Loop Acceleration.
API to expression classes.
std::list< path_nodet > patht
Definition: path.h:45
A namespacet is essentially one or two symbol tables bound together, to allow for symbol lookups in t...
Definition: namespace.h:93
bool is_underapproximate(path_acceleratort &accelerator)
Definition: accelerate.cpp:423
targett insert_after(const_targett target)
Insertion after the instruction pointed-to by the given instruction iterator target.
Definition: goto_program.h:518
A side_effect_exprt that returns a non-deterministically chosen value.
Definition: std_code.h:1633
void destructive_insert(const_targett target, goto_programt &p)
Inserts the given program p before target.
Definition: goto_program.h:532
std::list< patht > pathst
Definition: path.h:46
const symbol_exprt & to_symbol_expr(const exprt &expr)
Cast an exprt to a symbol_exprt.
Definition: std_expr.h:251
void add_path(patht &path)
Loop Acceleration.
dstringt has one field, an unsigned integer no which is an index into a static table of strings...
Definition: dstring.h:35
std::set< statet > state_sett
The Boolean constant false.
Definition: std_expr.h:4452
symbolt make_symbol(std::string name, typet type)
Definition: accelerate.cpp:449
goto_programt::targett find_back_jump(goto_programt::targett loop_header)
Definition: accelerate.cpp:34
const source_locationt & source_location() const
Definition: type.h:62
A generic container class for the GOTO intermediate representation of one function.
Definition: goto_program.h:72
Loop Acceleration.
void decl(symbol_exprt &sym, goto_programt::targett t)
Definition: accelerate.cpp:463
void output_path(const patht &path, const goto_programt &program, const namespacet &ns, std::ostream &str)
Definition: path.cpp:18
typet type
Type of symbol.
Definition: symbol.h:31
std::multimap< goto_programt::targett, state_pairt > sym_mapt
std::set< exprt > dirty_vars
Definition: accelerator.h:66
targett add_instruction()
Adds an instruction at the end.
Definition: goto_program.h:541
Base class for all expressions.
Definition: expr.h:54
overflow_mapt overflow_locs
Definition: accelerate.h:123
irep_idt base_name
Base (non-scoped) name.
Definition: symbol.h:46
std::string expr2c(const exprt &expr, const namespacet &ns, const expr2c_configurationt &configuration)
Definition: expr2c.cpp:3955
#define Forall_goto_functions(it, functions)
goto_programt pure_accelerator
Definition: accelerator.h:63
void swap(instructiont &instruction)
Swap two instructions.
Definition: goto_program.h:344
void build_state_machine(trace_automatont::sym_mapt::iterator p, trace_automatont::sym_mapt::iterator end, state_sett &accept_states, symbol_exprt state, symbol_exprt next_state, scratch_programt &state_machine)
Definition: accelerate.cpp:526
Expression to hold a symbol (variable)
Definition: std_expr.h:143
bool add(const symbolt &symbol)
Add a new symbol to the symbol table.
void restrict_traces()
Definition: accelerate.cpp:286
Compute natural loops in a goto_function.
std::unordered_set< irep_idt > find_symbols_sett
Definition: find_symbols.h:20
int accelerate_loops()
Definition: accelerate.cpp:623
acceleration_utilst utils
Definition: accelerate.h:119
namespacet ns
Definition: accelerate.h:116
Loop Acceleration.
const symbolt * lookup(const irep_idt &name) const
Find a symbol in the symbol table for read-only access.
constant_exprt from_integer(const mp_integer &int_value, const typet &type)
void insert_accelerator(goto_programt::targett &loop_header, goto_programt::targett &back_jump, path_acceleratort &accelerator, subsumed_patht &subsumed_path)
Definition: accelerate.cpp:182
void find_symbols(const exprt &src, find_symbols_sett &dest)
goto_functionst goto_functions
GOTO functions.
Definition: goto_model.h:32
bool lookup(const irep_idt &name, const symbolt *&symbol) const override
See documentation for namespace_baset::lookup().
Definition: namespace.cpp:166
A codet representing an assignment in the program.
Definition: std_code.h:256