CBMC
Loading...
Searching...
No Matches
polynomial_accelerator.cpp
Go to the documentation of this file.
1/*******************************************************************\
2
3Module: Loop Acceleration
4
5Author: Matt Lewis
6
7\*******************************************************************/
8
11
13
14#include <iostream>
15#include <map>
16#include <set>
17#include <string>
18
20
21#include <ansi-c/expr2c.h>
22
23#include <util/c_types.h>
24#include <util/std_code.h>
25#include <util/simplify_expr.h>
26#include <util/replace_expr.h>
27#include <util/arith_tools.h>
28
29#include "accelerator.h"
30#include "cone_of_influence.h"
32#include "scratch_program.h"
33#include "util.h"
34
36 patht &loop,
37 path_acceleratort &accelerator)
38{
40 accelerator.clear();
41
42 for(patht::iterator it=loop.begin();
43 it!=loop.end();
44 ++it)
45 {
46 body.push_back(*(it->loc));
47 }
48
49 expr_sett targets;
50 std::map<exprt, polynomialt> polynomials;
53
54 utils.find_modified(body, targets);
55
56#ifdef DEBUG
57 std::cout << "Polynomial accelerating program:\n";
58
59 for(goto_programt::instructionst::iterator it=body.begin();
60 it!=body.end();
61 ++it)
62 {
63 it->output(std::cout);
64 }
65
66 std::cout << "Modified:\n";
67
68 for(expr_sett::iterator it=targets.begin();
69 it!=targets.end();
70 ++it)
71 {
72 std::cout << expr2c(*it, ns) << '\n';
73 }
74#endif
75
76 for(goto_programt::instructionst::iterator it=body.begin();
77 it!=body.end();
78 ++it)
79 {
80 if(it->is_assign() || it->is_decl())
81 {
82 assigns.push_back(*it);
83 }
84 }
85
87 {
88 symbolt loop_sym=utils.fresh_symbol("polynomial::loop_counter",
90 loop_counter=loop_sym.symbol_expr();
91 }
92
93 for(expr_sett::iterator it=targets.begin();
94 it!=targets.end();
95 ++it)
96 {
98 exprt target=*it;
101
102 if(target.type()==bool_typet())
103 {
104 // Hack: don't accelerate booleans.
105 continue;
106 }
107
108 cone_of_influence(assigns, target, sliced_assigns, influence);
109
110 if(influence.find(target)==influence.end())
111 {
112#ifdef DEBUG
113 std::cout << "Found nonrecursive expression: "
114 << expr2c(target, ns) << '\n';
115#endif
116
117 nonrecursive.insert(target);
118 continue;
119 }
120
121 if(target.id()==ID_index ||
122 target.id()==ID_dereference)
123 {
124 // We can't accelerate a recursive indirect access...
125 accelerator.dirty_vars.insert(target);
126 continue;
127 }
128
130 {
131 std::map<exprt, polynomialt> this_poly;
132 this_poly[target]=poly;
133
134 if(check_inductive(this_poly, assigns))
135 {
136 polynomials.insert(std::make_pair(target, poly));
137 }
138 }
139 else
140 {
141#ifdef DEBUG
142 std::cout << "Failed to fit a polynomial for "
143 << expr2c(target, ns) << '\n';
144#endif
145 accelerator.dirty_vars.insert(*it);
146 }
147 }
148
149#if 0
150 if(polynomials.empty())
151 {
152 // return false;
153 }
154
155 if (!utils.check_inductive(polynomials, assigns)) {
156 // They're not inductive :-(
157 return false;
158 }
159#endif
160
162 stash_polynomials(program, polynomials, stashed, body);
163
164 exprt guard;
166
167 bool path_is_monotone;
168
169 try
170 {
173 }
174 catch(const std::string &s)
175 {
176 // Couldn't do WP.
177 std::cout << "Assumptions error: " << s << '\n';
178 return false;
179 }
180
182
183 for(std::map<exprt, polynomialt>::iterator it=polynomials.begin();
184 it!=polynomials.end();
185 ++it)
186 {
187 replace_expr(it->first, it->second.to_expr(), guard_last);
188 }
189
191 {
192 // OK cool -- the path is monotone, so we can just assume the condition for
193 // the first and last iterations.
197 guard_last);
198 // simplify(guard_last, ns);
199 }
200 else
201 {
202 // The path is not monotone, so we need to introduce a quantifier to ensure
203 // that the condition held for all 0 <= k < n.
205 const symbol_exprt k = k_sym.symbol_expr();
206
207 const and_exprt k_bound(
211
213 // simplify(implies, ns);
214
215 guard_last = forall_exprt(k, implies);
216 }
217
218 // All our conditions are met -- we can finally build the accelerator!
219 // It is of the form:
220 //
221 // assume(guard);
222 // loop_counter=*;
223 // target1=polynomial1;
224 // target2=polynomial2;
225 // ...
226 // assume(guard);
227 // assume(no overflows in previous code);
228
230
231 program.assign(
235
236 for(std::map<exprt, polynomialt>::iterator it=polynomials.begin();
237 it!=polynomials.end();
238 ++it)
239 {
240 program.assign(it->first, it->second.to_expr());
241 }
242
243 // Add in any array assignments we can do now.
245 assigns, polynomials, stashed, nonrecursive, program))
246 {
247 // We couldn't model some of the array assignments with polynomials...
248 // Unfortunately that means we just have to bail out.
249#ifdef DEBUG
250 std::cout << "Failed to accelerate a nonrecursive expression\n";
251#endif
252 return false;
253 }
254
256 program.fix_types();
257
259 {
260 utils.ensure_no_overflows(program);
261 }
262
263 accelerator.pure_accelerator.instructions.swap(program.instructions);
264
265 return true;
266}
267
270 exprt &var,
273{
274 // These are the variables that var depends on with respect to the body.
275 std::vector<expr_listt> parameters;
276 std::set<std::pair<expr_listt, exprt> > coefficients;
279 exprt overflow_var =
280 utils.fresh_symbol("polynomial::overflow", bool_typet()).symbol_expr();
281 overflow_instrumentert overflow(program, overflow_var, symbol_table);
282
283#ifdef DEBUG
284 std::cout << "Fitting a polynomial for " << expr2c(var, ns)
285 << ", which depends on:\n";
286
287 for(expr_sett::iterator it=influence.begin();
288 it!=influence.end();
289 ++it)
290 {
291 std::cout << expr2c(*it, ns) << '\n';
292 }
293#endif
294
295 for(expr_sett::iterator it=influence.begin();
296 it!=influence.end();
297 ++it)
298 {
299 if(it->id()==ID_index ||
300 it->id()==ID_dereference)
301 {
302 // Hack: don't accelerate variables that depend on arrays...
303 return false;
304 }
305
306 exprs.clear();
307
308 exprs.push_back(*it);
309 parameters.push_back(exprs);
310
311 exprs.push_back(loop_counter);
312 parameters.push_back(exprs);
313 }
314
315 // N
316 exprs.clear();
317 exprs.push_back(loop_counter);
318 parameters.push_back(exprs);
319
320 // N^2
321 exprs.push_back(loop_counter);
322 // parameters.push_back(exprs);
323
324 // Constant
325 exprs.clear();
326 parameters.push_back(exprs);
327
328 if(!is_bitvector(var.type()))
329 {
330 // We don't really know how to accelerate non-bitvectors anyway...
331 return false;
332 }
333
334 std::size_t width=to_bitvector_type(var.type()).get_width();
335 CHECK_RETURN(width > 0);
336
337 for(std::vector<expr_listt>::iterator it=parameters.begin();
338 it!=parameters.end();
339 ++it)
340 {
341 symbolt coeff=utils.fresh_symbol("polynomial::coeff",
342 signedbv_typet(width));
343 coefficients.insert(std::make_pair(*it, coeff.symbol_expr()));
344 }
345
346 // Build a set of values for all the parameters that allow us to fit a
347 // unique polynomial.
348
349 // XXX
350 // This isn't ok -- we're assuming 0, 1 and 2 are valid values for the
351 // variables involved, but this might make the path condition UNSAT. Should
352 // really be solving the path constraints a few times to get valid probe
353 // values...
354
355 std::map<exprt, int> values;
356
357 for(expr_sett::iterator it=influence.begin();
358 it!=influence.end();
359 ++it)
360 {
361 values[*it]=0;
362 }
363
364#ifdef DEBUG
365 std::cout << "Fitting polynomial over " << values.size()
366 << " variables\n";
367#endif
368
369 for(int n=0; n<=2; n++)
370 {
371 for(expr_sett::iterator it=influence.begin();
372 it!=influence.end();
373 ++it)
374 {
375 values[*it]=1;
376 assert_for_values(program, values, coefficients, n, body, var, overflow);
377 values[*it]=0;
378 }
379 }
380
381 // Now just need to assert the case where all values are 0 and all are 2.
382 assert_for_values(program, values, coefficients, 0, body, var, overflow);
383 assert_for_values(program, values, coefficients, 2, body, var, overflow);
384
385 for(expr_sett::iterator it=influence.begin();
386 it!=influence.end();
387 ++it)
388 {
389 values[*it]=2;
390 }
391
392 assert_for_values(program, values, coefficients, 2, body, var, overflow);
393
394#ifdef DEBUG
395 std::cout << "Fitting polynomial with program:\n";
396 program.output(ns, irep_idt(), std::cout);
397#endif
398
399 // Now do an ASSERT(false) to grab a counterexample
401
402 // If the path is satisfiable, we've fitted a polynomial. Extract the
403 // relevant coefficients and return the expression.
404 try
405 {
406 if(program.check_sat(guard_manager))
407 {
408 utils.extract_polynomial(program, coefficients, polynomial);
409 return true;
410 }
411 }
412 catch(const std::string &s)
413 {
414 std::cout << "Error in fitting polynomial SAT check: " << s << '\n';
415 }
416 catch(const char *s)
417 {
418 std::cout << "Error in fitting polynomial SAT check: " << s << '\n';
419 }
420
421 return false;
422}
423
436
439 exprt &target,
441{
442 // unused parameters
443 (void)body;
444 (void)target;
445 (void)poly;
446 return false;
447
448#if 0
450
451 program.append(body);
452 program.add_instruction(ASSERT)->guard=equal_exprt(target, not_exprt(target));
453
454 try
455 {
456 if(program.check_sat(false))
457 {
458#ifdef DEBUG
459 std::cout << "Fitting constant, eval'd to: "
460 << expr2c(program.eval(target), ns) << '\n';
461#endif
462 constant_exprt val=to_constant_expr(program.eval(target));
463 mp_integer mp=binary2integer(val.get_value().c_str(), true);
465 monomialt::termt term;
466
467 term.var=from_integer(1, target.type());
468 term.exp=1;
469 mon.terms.push_back(term);
470 mon.coeff=mp.to_long();
471
472 poly.monomials.push_back(mon);
473
474 return true;
475 }
476 }
477 catch(const std::string &s)
478 {
479 std::cout << "Error in fitting polynomial SAT check: " << s << '\n';
480 }
481 catch(const char *s)
482 {
483 std::cout << "Error in fitting polynomial SAT check: " << s << '\n';
484 }
485
486 return false;
487#endif
488}
489
491 scratch_programt &program,
492 std::map<exprt, int> &values,
493 std::set<std::pair<expr_listt, exprt> > &coefficients,
494 int num_unwindings,
496 exprt &target,
498{
499 // First figure out what the appropriate type for this expression is.
500 std::optional<typet> expr_type;
501
502 for(std::map<exprt, int>::iterator it=values.begin();
503 it!=values.end();
504 ++it)
505 {
506 typet this_type=it->first.type();
507 if(this_type.id()==ID_pointer)
508 {
509#ifdef DEBUG
510 std::cout << "Overriding pointer type\n";
511#endif
513 }
514
515 if(!expr_type.has_value())
516 {
518 }
519 else
520 {
522 }
523 }
524
525 INVARIANT(
526 to_bitvector_type(*expr_type).get_width() > 0,
527 "joined types must be non-empty bitvector types");
528
529 // Now set the initial values of the all the variables...
530 for(std::map<exprt, int>::iterator it=values.begin();
531 it!=values.end();
532 ++it)
533 {
534 program.assign(it->first, from_integer(it->second, *expr_type));
535 }
536
537 // Now unwind the loop as many times as we need to.
538 for(int i=0; i < num_unwindings; i++)
539 {
540 program.append(loop_body);
541 }
542
543 // Now build the polynomial for this point and assert it fits.
544 exprt rhs=nil_exprt();
545
546 for(std::set<std::pair<expr_listt, exprt> >::iterator it=coefficients.begin();
547 it!=coefficients.end();
548 ++it)
549 {
550 int concrete_value=1;
551
552 for(expr_listt::const_iterator e_it=it->first.begin();
553 e_it!=it->first.end();
554 ++e_it)
555 {
556 exprt e=*e_it;
557
558 if(e==loop_counter)
559 {
561 }
562 else
563 {
564 std::map<exprt, int>::iterator v_it=values.find(e);
565
566 if(v_it!=values.end())
567 {
568 concrete_value *= v_it->second;
569 }
570 }
571 }
572
573 // OK, concrete_value now contains the value of all the relevant variables
574 // multiplied together. Create the term concrete_value*coefficient and add
575 // it into the polynomial.
576 typecast_exprt cast(it->second, *expr_type);
577 const mult_exprt term(from_integer(concrete_value, *expr_type), cast);
578
579 if(rhs.is_nil())
580 {
581 rhs=term;
582 }
583 else
584 {
585 rhs=plus_exprt(rhs, term);
586 }
587 }
588
589 exprt overflow_expr;
590 overflow.overflow_expr(rhs, overflow_expr);
591
592 program.add(goto_programt::make_assumption(not_exprt(overflow_expr)));
593
594 rhs=typecast_exprt(rhs, target.type());
595
596 // We now have the RHS of the polynomial. Assert that this is equal to the
597 // actual value of the variable we're fitting.
598 const equal_exprt polynomial_holds(target, rhs);
599
600 // Finally, assert that the polynomial equals the variable we're fitting.
602}
603
606 exprt &target,
609{
610 utils.gather_rvalues(target, cone);
611
612 for(goto_programt::instructionst::reverse_iterator r_it=orig_body.rbegin();
613 r_it!=orig_body.rend();
614 ++r_it)
615 {
616 if(r_it->is_assign())
617 {
618 // XXX -- this doesn't work if the assignment is not to a symbol, e.g.
619 // A[i]=0;
620 // or
621 // *p=x;
622 exprt assignment_lhs = r_it->assign_lhs();
623 exprt assignment_rhs = r_it->assign_rhs();
625
627
628 for(expr_sett::iterator s_it=lhs_syms.begin();
629 s_it!=lhs_syms.end();
630 ++s_it)
631 {
632 if(cone.find(*s_it)!=cone.end())
633 {
634 // We're assigning to something in the cone of influence -- expand the
635 // cone.
636 body.push_front(*r_it);
637 cone.erase(assignment_lhs);
639 break;
640 }
641 }
642 }
643 }
644}
645
647 std::map<exprt, polynomialt> polynomials,
649{
650 // Checking that our polynomial is inductive with respect to the loop body is
651 // equivalent to checking safety of the following program:
652 //
653 // assume (target1==polynomial1);
654 // assume (target2==polynomial2)
655 // ...
656 // loop_body;
657 // loop_counter++;
658 // assert (target1==polynomial1);
659 // assert (target2==polynomial2);
660 // ...
662 std::vector<exprt> polynomials_hold;
664
666
667 for(std::map<exprt, polynomialt>::iterator it=polynomials.begin();
668 it!=polynomials.end();
669 ++it)
670 {
671 const equal_exprt holds(it->first, it->second.to_expr());
673
674 polynomials_hold.push_back(holds);
675 }
676
677 program.append(body);
678
683
684 for(std::vector<exprt>::iterator it=polynomials_hold.begin();
685 it!=polynomials_hold.end();
686 ++it)
687 {
688 program.add(goto_programt::make_assertion(*it));
689 }
690
691#ifdef DEBUG
692 std::cout << "Checking following program for inductiveness:\n";
693 program.output(ns, irep_idt(), std::cout);
694#endif
695
696 try
697 {
698 if(program.check_sat(guard_manager))
699 {
700 // We found a counterexample to inductiveness... :-(
701 #ifdef DEBUG
702 std::cout << "Not inductive!\n";
703 #endif
704 return false;
705 }
706 else
707 {
708 return true;
709 }
710 }
711 catch(const std::string &s)
712 {
713 std::cout << "Error in inductiveness SAT check: " << s << '\n';
714 return false;
715 }
716 catch(const char *s)
717 {
718 std::cout << "Error in inductiveness SAT check: " << s << '\n';
719 return false;
720 }
721}
722
724 scratch_programt &program,
725 std::map<exprt, polynomialt> &polynomials,
728{
729 expr_sett modified;
730 utils.find_modified(body, modified);
731 utils.stash_variables(program, modified, substitution);
732
733 for(std::map<exprt, polynomialt>::iterator it=polynomials.begin();
734 it!=polynomials.end();
735 ++it)
736 {
737 it->second.substitute(substitution);
738 }
739}
740
741/*
742 * Finds a precondition which guarantees that all the assumptions and assertions
743 * along this path hold.
744 *
745 * This is not the weakest precondition, since we make underapproximations due
746 * to aliasing.
747 */
748
750{
752
753 for(patht::reverse_iterator r_it=path.rbegin();
754 r_it!=path.rend();
755 ++r_it)
756 {
758
759 if(t->is_assign())
760 {
761 // XXX Need to check for aliasing...
762 const exprt &lhs = t->assign_lhs();
763 const exprt &rhs = t->assign_rhs();
764
765 if(lhs.id()==ID_symbol)
766 {
767 replace_expr(lhs, rhs, ret);
768 }
769 else if(lhs.id()==ID_index ||
770 lhs.id()==ID_dereference)
771 {
772 continue;
773 }
774 else
775 {
776 throw "couldn't take WP of " + expr2c(lhs, ns) + "=" + expr2c(rhs, ns);
777 }
778 }
779 else if(t->is_assume() || t->is_assert())
780 {
781 ret = implies_exprt(t->condition(), ret);
782 }
783 else
784 {
785 // Ignore.
786 }
787
788 if(!r_it->guard.is_true() && !r_it->guard.is_nil())
789 {
790 // The guard isn't constant true, so we need to accumulate that too.
791 ret=implies_exprt(r_it->guard, ret);
792 }
793 }
794
795 simplify(ret, ns);
796
797 return ret;
798}
std::list< exprt > expr_listt
Loop Acceleration.
constant_exprt from_integer(const mp_integer &int_value, const typet &type)
const bitvector_typet & to_bitvector_type(const typet &type)
Cast a typet to a bitvector_typet.
static exprt guard(const exprt::operandst &guards, exprt cond)
void find_modified(const patht &path, expr_sett &modified)
bool do_nonrecursive(goto_programt::instructionst &loop_body, std::map< exprt, polynomialt > &polynomials, substitutiont &substitution, expr_sett &nonrecursive, scratch_programt &program)
bool check_inductive(std::map< exprt, polynomialt > polynomials, patht &path, guard_managert &guard_manager)
void gather_rvalues(const exprt &expr, expr_sett &rvalues)
symbolt fresh_symbol(std::string base, typet type)
bool do_assumptions(std::map< exprt, polynomialt > polynomials, patht &body, exprt &guard, guard_managert &guard_manager)
void ensure_no_overflows(scratch_programt &program)
void extract_polynomial(scratch_programt &program, std::set< std::pair< expr_listt, exprt > > &coefficients, polynomialt &polynomial)
void stash_variables(scratch_programt &program, expr_sett modified, substitutiont &substitution)
virtual void output(const namespacet &ns, const irep_idt &function_id, const goto_programt &goto_program, std::ostream &out) const
Output the abstract states for a single function.
Definition ai.cpp:39
virtual void clear()
Reset the abstract state.
Definition ai.h:265
ait supplies three of the four components needed: an abstract interpreter (in this case handling func...
Definition ai.h:562
Boolean AND.
Definition std_expr.h:2125
A base class for relations, i.e., binary predicates whose two operands have the same type.
Definition std_expr.h:762
The Boolean type.
Definition std_types.h:36
A goto_instruction_codet representing an assignment in the program.
A constant literal expression.
Definition std_expr.h:3117
Equality.
Definition std_expr.h:1366
Base class for all expressions.
Definition expr.h:56
typet & type()
Return the type of the expression.
Definition expr.h:84
const source_locationt & source_location() const
Definition expr.h:231
The Boolean constant false.
Definition std_expr.h:3199
A forall expression.
static instructiont make_assumption(const exprt &g, const source_locationt &l=source_locationt::nil())
instructionst instructions
The list of instructions in the goto program.
instructionst::const_iterator const_targett
targett add_instruction()
Adds an instruction at the end.
static instructiont make_assignment(const code_assignt &_code, const source_locationt &l=source_locationt::nil())
Create an assignment instruction.
std::list< instructiont > instructionst
targett add(instructiont &&instruction)
Adds a given instruction at the end.
static instructiont make_assertion(const exprt &g, const source_locationt &l=source_locationt::nil())
Boolean implication.
Definition std_expr.h:2225
const irep_idt & id() const
Definition irep.h:388
bool is_nil() const
Definition irep.h:368
Binary minus.
Definition std_expr.h:1061
Binary multiplication Associativity is not specified.
Definition std_expr.h:1107
The NIL expression.
Definition std_expr.h:3208
Boolean negation.
Definition std_expr.h:2454
std::set< exprt > dirty_vars
Definition accelerator.h:66
goto_programt pure_accelerator
Definition accelerator.h:63
The plus expression Associativity is not specified.
Definition std_expr.h:1002
void assert_for_values(scratch_programt &program, std::map< exprt, int > &values, std::set< std::pair< expr_listt, exprt > > &coefficients, int num_unwindings, goto_programt::instructionst &loop_body, exprt &target, overflow_instrumentert &overflow)
symbol_table_baset & symbol_table
void stash_polynomials(scratch_programt &program, std::map< exprt, polynomialt > &polynomials, std::map< exprt, exprt > &stashed, goto_programt::instructionst &body)
bool fit_polynomial_sliced(goto_programt::instructionst &sliced_body, exprt &target, expr_sett &influence, polynomialt &polynomial)
bool accelerate(patht &loop, path_acceleratort &accelerator)
bool check_inductive(std::map< exprt, polynomialt > polynomials, goto_programt::instructionst &body)
bool fit_const(goto_programt::instructionst &loop_body, exprt &target, polynomialt &polynomial)
void cone_of_influence(goto_programt::instructionst &orig_body, exprt &target, goto_programt::instructionst &body, expr_sett &influence)
bool fit_polynomial(goto_programt::instructionst &loop_body, exprt &target, polynomialt &polynomial)
message_handlert & message_handler
bool check_sat(bool do_slice, guard_managert &guard_manager)
targett assign(const exprt &lhs, const exprt &rhs)
void append(goto_programt::instructionst &instructions)
exprt eval(const exprt &e)
A side_effect_exprt that returns a non-deterministically chosen value.
Definition std_code.h:1520
Fixed-width bit-vector with two's complement interpretation.
Expression to hold a symbol (variable)
Definition std_expr.h:131
Symbol table entry.
Definition symbol.h:28
class symbol_exprt symbol_expr() const
Produces a symbol_exprt for a symbol.
Definition symbol.cpp:121
Semantic type conversion.
Definition std_expr.h:2073
The type of an expression, extends irept.
Definition type.h:29
Loop Acceleration.
std::unordered_set< exprt, irep_hash > expr_sett
std::string expr2c(const exprt &expr, const namespacet &ns, const expr2c_configurationt &configuration)
Definition expr2c.cpp:4155
Concrete Goto Program.
@ ASSERT
const mp_integer binary2integer(const std::string &n, bool is_signed)
convert binary string representation to mp_integer
Definition mp_arith.cpp:117
Loop Acceleration.
std::list< path_nodet > patht
Definition path.h:44
std::map< exprt, exprt > substitutiont
Definition polynomial.h:39
Loop Acceleration.
bool replace_expr(const exprt &what, const exprt &by, exprt &dest)
Loop Acceleration.
bool simplify(exprt &expr, const namespacet &ns)
#define CHECK_RETURN(CONDITION)
Definition invariant.h:495
#define INVARIANT(CONDITION, REASON)
This macro uses the wrapper function 'invariant_violated_string'.
Definition invariant.h:423
const constant_exprt & to_constant_expr(const exprt &expr)
Cast an exprt to a constant_exprt.
Definition std_expr.h:3172
unsigned int exp
Definition polynomial.h:26
#define size_type
Definition unistd.c:186
typet join_types(const typet &t1, const typet &t2)
Return the smallest type that both t1 and t2 can be cast to without losing information.
Definition util.cpp:70
unsignedbv_typet unsigned_poly_type()
Definition util.cpp:25
bool is_bitvector(const typet &t)
Convenience function – is the type a bitvector of some kind?
Definition util.cpp:33
Loop Acceleration.
dstringt irep_idt