CBMC
Loading...
Searching...
No Matches
accelerate.cpp
Go to the documentation of this file.
1/*******************************************************************\
2
3Module: Loop Acceleration
4
5Author: Matt Lewis
6
7\*******************************************************************/
8
11
12#include "accelerate.h"
13
15
17
18#include <util/arith_tools.h>
19#include <util/find_symbols.h>
20#include <util/std_code.h>
21#include <util/std_expr.h>
22
23#include <iostream>
24#include <list>
25
26#include "accelerator.h"
29#include "path.h"
30#include "scratch_program.h"
31#include "util.h"
32
33#ifdef DEBUG
34# include <util/format_expr.h>
35#endif
36
38 goto_programt::targett loop_header)
39{
41 natural_loops.loop_map.at(loop_header);
43
44 for(const auto &t : loop)
45 {
46 if(
47 t->is_goto() && t->condition().is_true() && t->targets.size() == 1 &&
48 t->targets.front() == loop_header &&
49 t->location_number > back_jump->location_number)
50 {
51 back_jump=t;
52 }
53 }
54
55 return back_jump;
56}
57
59{
61 natural_loops.loop_map.at(loop_header);
62
63 for(const auto &t : loop)
64 {
65 if(t->is_backwards_goto())
66 {
67 if(t->targets.size()!=1 ||
68 t->get_target()!=loop_header)
69 {
70 return true;
71 }
72 }
73
74 // Header of some other loop?
75 if(t != loop_header && natural_loops.is_loop_header(t))
76 {
77 return true;
78 }
79 }
80
81 return false;
82}
83
85{
88 int num_accelerated=0;
89 std::list<path_acceleratort> accelerators;
91 natural_loops.loop_map.at(loop_header);
92
93 if(contains_nested_loops(loop_header))
94 {
95 // For now, only accelerate innermost loops.
96#ifdef DEBUG
97 std::cout << "Not accelerating an outer loop\n";
98#endif
99 return 0;
100 }
101
104 program.update();
105
106#if 1
111 program,
112 loop,
113 loop_header,
116#else
118 acceleration(symbol_table, goto_functions, program, loop, loop_header);
119#endif
120
121 path_acceleratort accelerator;
122
123 while(acceleration.accelerate(accelerator) &&
124 (accelerate_limit < 0 ||
126 {
127 // set_dirty_vars(accelerator);
128
129 if(is_underapproximate(accelerator))
130 {
131 // We have some underapproximated variables -- just punt for now.
132#ifdef DEBUG
133 std::cout << "Not inserting accelerator because of underapproximation\n";
134#endif
135
136 continue;
137 }
138
139 accelerators.push_back(accelerator);
141
142#ifdef DEBUG
143 std::cout << "Accelerated path:\n";
144 output_path(accelerator.path, program, ns, std::cout);
145
146 std::cout << "Accelerator has "
147 << accelerator.pure_accelerator.instructions.size()
148 << " instructions\n";
149#endif
150 }
151
153 program.insert_before_swap(loop_header, skip);
154
156 ++new_inst;
157
158 loop.insert_instruction(new_inst);
159
160 std::cout << "Overflow loc is " << overflow_loc->location_number << '\n';
161 std::cout << "Back jump is " << back_jump->location_number << '\n';
162
163 for(std::list<path_acceleratort>::iterator it=accelerators.begin();
164 it!=accelerators.end();
165 ++it)
166 {
167 subsumed_patht inserted(it->path);
168
169 insert_accelerator(loop_header, back_jump, *it, inserted);
170 subsumed.push_back(inserted);
172 }
173
174 return num_accelerated;
175}
176
178 goto_programt::targett &loop_header,
180 path_acceleratort &accelerator,
182{
184 loop_header,
185 back_jump,
186 accelerator.pure_accelerator,
187 subsumed_path.accelerator);
188
189 if(!accelerator.overflow_path.instructions.empty())
190 {
192 loop_header, back_jump, accelerator.overflow_path, subsumed_path.residue);
193 }
194}
195
196/*
197 * Insert a looping path (usually an accelerator) into a goto-program,
198 * beginning at loop_header and jumping back to loop_header via back_jump.
199 * Stores the locations at which the looping path was added in inserted_path.
200 *
201 * THIS DESTROYS looping_path!!
202 */
233
235 goto_programt::targett loop_header,
238{
239 symbolt overflow_sym=utils.fresh_symbol("accelerate::overflow", bool_typet());
240 const exprt &overflow_var=overflow_sym.symbol_expr();
242 natural_loops.loop_map.at(loop_header);
243 overflow_instrumentert instrumenter(program, overflow_var, symbol_table);
244
245 for(const auto &loop_instruction : loop)
246 {
249
251 for(const auto &new_instruction : added)
252 loop.insert_instruction(new_instruction);
253 }
254
256 loop_header,
258 t->swap(*loop_header);
259 loop.insert_instruction(t);
260 overflow_locs[loop_header].push_back(t);
261
263 overflow_loc->swap(*loop_end);
264 loop.insert_instruction(overflow_loc);
265
268 t2->swap(*loop_end);
269 overflow_locs[overflow_loc].push_back(t2);
270 loop.insert_instruction(t2);
271
275}
276
278{
280
281 for(subsumed_pathst::iterator it=subsumed.begin();
282 it!=subsumed.end();
283 ++it)
284 {
285 if(!it->subsumed.empty())
286 {
287#ifdef DEBUG
289 std::cout << "Restricting path:\n";
290 output_path(it->subsumed, program, ns, std::cout);
291#endif
292
293 automaton.add_path(it->subsumed);
294 }
295
297 patht::iterator jt=double_accelerator.begin();
298 double_accelerator.insert(
299 jt, it->accelerator.begin(), it->accelerator.end());
300 double_accelerator.insert(
301 jt, it->accelerator.begin(), it->accelerator.end());
302
303#ifdef DEBUG
305 std::cout << "Restricting path:\n";
307#endif
309 }
310
311 std::cout << "Building trace automaton...\n";
312
313 automaton.build();
315}
316
318{
319 for(std::set<exprt>::iterator it=accelerator.dirty_vars.begin();
320 it!=accelerator.dirty_vars.end();
321 ++it)
322 {
323 expr_mapt::iterator jt=dirty_vars_map.find(*it);
325
326 if(jt==dirty_vars_map.end())
327 {
329 symbolt new_sym=utils.fresh_symbol("accelerate::dirty", bool_typet());
330 dirty_var=new_sym.symbol_expr();
332 }
333 else
334 {
335 dirty_var=jt->second;
336 }
337
338#ifdef DEBUG
339 std::cout << "Setting dirty flag " << format(dirty_var) << " for "
340 << format(*it) << '\n';
341#endif
342
343 accelerator.pure_accelerator.add(
345 }
346}
347
349{
350 for(expr_mapt::iterator it=dirty_vars_map.begin();
351 it!=dirty_vars_map.end();
352 ++it)
353 {
357 }
358
360
362 it!=program.instructions.end();
363 it=next)
364 {
365 next=it;
366 ++next;
367
368 // If this is an assign to a tracked variable, clear the dirty flag.
369 // Note: this order of insertions means that we assume each of the read
370 // variables is clean _before_ clearing any dirty flags.
371 if(it->is_assign())
372 {
373 const exprt &lhs = it->assign_lhs();
374 expr_mapt::iterator dirty_var=dirty_vars_map.find(lhs);
375
376 if(dirty_var!=dirty_vars_map.end())
377 {
381 }
382 }
383
384 // Find which symbols are read, i.e. those appearing in a guard or on
385 // the right hand side of an assignment. Assume each is not dirty.
386 std::set<symbol_exprt> read;
387
388 if(it->has_condition())
389 find_symbols(it->condition(), read);
390
391 if(it->is_assign())
392 find_symbols(it->assign_rhs(), read);
393
394 for(const auto &var : read)
395 {
396 expr_mapt::iterator dirty_var=dirty_vars_map.find(var);
397
398 if(dirty_var==dirty_vars_map.end())
399 {
400 continue;
401 }
402
406 }
407 }
408}
409
411{
412 for(std::set<exprt>::iterator it=accelerator.dirty_vars.begin();
413 it!=accelerator.dirty_vars.end();
414 ++it)
415 {
416 if(it->id()==ID_symbol && it->type() == bool_typet())
417 {
418 const irep_idt &id=to_symbol_expr(*it).get_identifier();
419 const symbolt &sym = symbol_table.lookup_ref(id);
420
421 if(sym.module=="scratch")
422 {
423 continue;
424 }
425 }
426
427#ifdef DEBUG
428 std::cout << "Underapproximate variable: " << format(*it) << '\n';
429#endif
430 return true;
431 }
432
433 return false;
434}
435
437{
438 symbolt ret{name, std::move(type), irep_idt{}};
439 ret.module="accelerate";
440 ret.base_name=name;
441 ret.pretty_name=name;
442
444
445 return ret;
446}
447
449{
450#if 0
452 code_declt code(sym);
453
454 decl->make_decl();
455 decl->code=code;
456#endif
457}
458
466
468{
469 symbolt state_sym=make_symbol("trace_automaton::state",
471 symbolt next_state_sym=make_symbol("trace_automaton::next_state",
473 symbol_exprt state=state_sym.symbol_expr();
474 symbol_exprt next_state=next_state_sym.symbol_expr();
475
476 trace_automatont::sym_mapt transitions;
477 state_sett accept_states;
478
479 automaton.get_transitions(transitions);
480 automaton.accept_states(accept_states);
481
482 std::cout
483 << "Inserting trace automaton with "
484 << automaton.num_states() << " states, "
485 << accept_states.size() << " accepting states and "
486 << transitions.size() << " transitions\n";
487
488 // Declare the variables we'll use to encode the state machine.
490 decl(state, t, from_integer(automaton.init_state(), state.type()));
491 decl(next_state, t);
492
493 // Now for each program location that appears as a symbol in the
494 // trace automaton, add the appropriate code to drive the state
495 // machine.
496 for(const auto &sym : automaton.alphabet)
497 {
500 trace_automatont::sym_range_pairt p=transitions.equal_range(sym);
501
502 build_state_machine(p.first, p.second, accept_states, state, next_state,
504
506 }
507}
508
510 trace_automatont::sym_mapt::iterator begin,
511 trace_automatont::sym_mapt::iterator end,
512 state_sett &accept_states,
513 symbol_exprt state,
514 symbol_exprt next_state,
516{
517 std::map<unsigned int, unsigned int> successor_counts;
518 unsigned int max_count=0;
519 unsigned int likely_next=0;
520
521 // Optimisation: find the most common successor state and initialise
522 // next_state to that value. This reduces the size of the state machine
523 // driver substantially.
524 for(trace_automatont::sym_mapt::iterator p=begin; p!=end; ++p)
525 {
527 unsigned int to=state_pair.second;
528 unsigned int count=0;
529
530 if(successor_counts.find(to)==successor_counts.end())
531 {
532 count=1;
533 }
534 else
535 {
536 count=successor_counts[to] + 1;
537 }
538
539 successor_counts[to]=count;
540
541 if(count > max_count)
542 {
543 max_count=count;
545 }
546 }
547
548 // Optimisation: if there is only one possible successor state, just
549 // jump straight to it instead of driving the whole machine.
550 if(successor_counts.size()==1)
551 {
552 if(accept_states.find(likely_next)!=accept_states.end())
553 {
554 // It's an accept state. Just assume(false).
555 state_machine.assume(false_exprt());
556 }
557 else
558 {
559 state_machine.assign(state,
560 from_integer(likely_next, next_state.type()));
561 }
562
563 return;
564 }
565
566 state_machine.assign(next_state,
567 from_integer(likely_next, next_state.type()));
568
569 for(trace_automatont::sym_mapt::iterator p=begin; p!=end; ++p)
570 {
572 unsigned int from=state_pair.first;
573 unsigned int to=state_pair.second;
574
575 if(to==likely_next)
576 {
577 continue;
578 }
579
580 // We're encoding the transition
581 //
582 // from -loc-> to
583 //
584 // which we encode by inserting:
585 //
586 // next_state=(state==from) ? to : next_state;
587 //
588 // just before loc.
589 equal_exprt guard(state, from_integer(from, state.type()));
590 if_exprt rhs(guard, from_integer(to, next_state.type()), next_state);
591 state_machine.assign(next_state, rhs);
592 }
593
594 // Update the state and assume(false) if we've hit an accept state.
595 state_machine.assign(state, next_state);
596
597 for(state_sett::iterator it=accept_states.begin();
598 it!=accept_states.end();
599 ++it)
600 {
601 state_machine.assume(
602 not_exprt(equal_exprt(state, from_integer(*it, state.type()))));
603 }
604}
605
607{
608 int num_accelerated=0;
609
610 for(natural_loops_mutablet::loop_mapt::iterator it =
611 natural_loops.loop_map.begin();
612 it!=natural_loops.loop_map.end();
613 ++it)
614 {
615 goto_programt::targett t=it->first;
617 }
618
619 program.update();
620
621 if(num_accelerated > 0)
622 {
623 std::cout << "Engaging crush mode...\n";
624
626 // add_dirty_checks();
627 program.update();
628
629 std::cout << "Crush mode engaged.\n";
630 }
631
632 return num_accelerated;
633}
634
636 goto_modelt &goto_model,
637 message_handlert &message_handler,
638 bool use_z3,
639 guard_managert &guard_manager)
640{
641 for(auto &gf_entry : goto_model.goto_functions.function_map)
642 {
643 std::cout << "Accelerating function " << gf_entry.first << '\n';
644 acceleratet accelerate(
645 gf_entry.second.body, goto_model, message_handler, use_z3, guard_manager);
646
647 int num_accelerated=accelerate.accelerate_loops();
648
649 if(num_accelerated > 0)
650 {
651 std::cout << "Added " << num_accelerated
652 << " accelerator(s)\n";
653 }
654 }
655}
void accelerate_functions(goto_modelt &goto_model, message_handlert &message_handler, bool use_z3, guard_managert &guard_manager)
Loop Acceleration.
Loop Acceleration.
constant_exprt from_integer(const mp_integer &int_value, const typet &type)
static exprt guard(const exprt::operandst &guards, exprt cond)
void add_dirty_checks()
void insert_accelerator(goto_programt::targett &loop_header, goto_programt::targett &back_jump, path_acceleratort &accelerator, subsumed_patht &subsumed_path)
void insert_automaton(trace_automatont &automaton)
acceleration_utilst utils
Definition accelerate.h:118
goto_programt & program
Definition accelerate.h:111
symbolt make_symbol(std::string name, typet type)
natural_loops_mutablet natural_loops
Definition accelerate.h:116
message_handlert & message_handler
Definition accelerate.h:57
void decl(symbol_exprt &sym, goto_programt::targett t)
symbol_tablet & symbol_table
Definition accelerate.h:113
expr_mapt dirty_vars_map
Definition accelerate.h:127
subsumed_pathst subsumed
Definition accelerate.h:117
int accelerate_loops()
bool contains_nested_loops(goto_programt::targett &loop_header)
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)
void make_overflow_loc(goto_programt::targett loop_header, goto_programt::targett &loop_end, goto_programt::targett &overflow_loc)
void restrict_traces()
overflow_mapt overflow_locs
Definition accelerate.h:125
namespacet ns
Definition accelerate.h:115
void set_dirty_vars(path_acceleratort &accelerator)
goto_functionst & goto_functions
Definition accelerate.h:112
bool is_underapproximate(path_acceleratort &accelerator)
static const int accelerate_limit
Definition accelerate.h:54
goto_programt::targett find_back_jump(goto_programt::targett loop_header)
guard_managert & guard_manager
Definition accelerate.h:114
void insert_looping_path(goto_programt::targett &loop_header, goto_programt::targett &back_jump, goto_programt &looping_path, patht &inserted_path)
int accelerate_loop(goto_programt::targett &loop_header)
symbolt fresh_symbol(std::string base, typet type)
ait supplies three of the four components needed: an abstract interpreter (in this case handling func...
Definition ai.h:562
The Boolean type.
Definition std_types.h:36
A goto_instruction_codet representing an assignment in the program.
A goto_instruction_codet representing the declaration of a local variable.
dstringt has one field, an unsigned integer no which is an index into a static table of strings.
Definition dstring.h:38
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
The Boolean constant false.
Definition std_expr.h:3199
function_mapt function_map
goto_functionst goto_functions
GOTO functions.
Definition goto_model.h:34
This class represents an instruction in the GOTO intermediate representation.
A generic container class for the GOTO intermediate representation of one function.
static instructiont make_assumption(const exprt &g, const source_locationt &l=source_locationt::nil())
instructionst instructions
The list of instructions in the goto program.
void update()
Update all indices.
void insert_before_swap(targett target)
Insertion that preserves jumps to "target".
void destructive_insert(const_targett target, goto_programt &p)
Inserts the given program p before target.
instructionst::iterator targett
static instructiont make_assignment(const code_assignt &_code, const source_locationt &l=source_locationt::nil())
Create an assignment instruction.
static instructiont make_skip(const source_locationt &l=source_locationt::nil())
targett insert_after(const_targett target)
Insertion after the instruction pointed-to by the given instruction iterator target.
targett add(instructiont &&instruction)
Adds a given instruction at the end.
static instructiont make_goto(targett _target, const source_locationt &l=source_locationt::nil())
targett insert_before(const_targett target)
Insertion before the instruction pointed-to by the given instruction iterator target.
std::list< targett > targetst
The trinary if-then-else operator.
Definition std_expr.h:2497
loop_mapt loop_map
bool is_loop_header(const T instruction) const
Returns true if instruction is the header of any loop.
A namespacet is essentially one or two symbol tables bound together, to allow for symbol lookups in t...
Definition namespace.h:91
Boolean negation.
Definition std_expr.h:2454
goto_programt overflow_path
Definition accelerator.h:64
std::set< exprt > dirty_vars
Definition accelerator.h:66
goto_programt pure_accelerator
Definition accelerator.h:63
A side_effect_exprt that returns a non-deterministically chosen value.
Definition std_code.h:1520
Expression to hold a symbol (variable)
Definition std_expr.h:131
bool add(const symbolt &symbol)
Add a new symbol to the symbol table.
const symbolt & lookup_ref(const irep_idt &name) const
Find a symbol in the symbol table for read-only access.
Symbol table entry.
Definition symbol.h:28
std::pair< sym_mapt::iterator, sym_mapt::iterator > sym_range_pairt
std::multimap< goto_programt::targett, state_pairt, goto_programt::target_less_than > sym_mapt
std::pair< statet, statet > state_pairt
The Boolean constant true.
Definition std_expr.h:3190
The type of an expression, extends irept.
Definition type.h:29
static bool find_symbols(symbol_kindt, const typet &, std::function< bool(const symbol_exprt &)>, std::unordered_set< irep_idt > &bindings, const std::vector< irep_idt > &subs_to_find)
Find identifiers with id ID_symbol of the sub expressions and the subs with ID in subs_to_find consid...
static format_containert< T > format(const T &o)
Definition format.h:37
Goto Programs with Functions.
@ SKIP
int __CPROVER_ID java::java io InputStream read
Definition java.io.c:5
Compute natural loops in a goto_function.
Loop Acceleration.
void output_path(const patht &path, std::ostream &str)
Definition path.cpp:16
Loop Acceleration.
std::list< patht > pathst
Definition path.h:45
std::list< path_nodet > patht
Definition path.h:44
Loop Acceleration.
API to expression classes.
const symbol_exprt & to_symbol_expr(const exprt &expr)
Cast an exprt to a symbol_exprt.
Definition std_expr.h:272
This is unused by this implementation of guards, but can be used by other implementations of the same...
Definition guard_expr.h:20
std::set< statet > state_sett
unsignedbv_typet unsigned_poly_type()
Definition util.cpp:25
Loop Acceleration.