27 assert(unwind_set.empty());
29 std::vector<std::string> result;
31 assert(!result.empty());
33 if(result.front().empty())
36 for(std::vector<std::string>::const_iterator it=result.begin();
37 it!=result.end(); it++)
49 unsigned loop_id=std::stoi(
id);
50 int loop_bound=std::stoi(bound);
53 throw "given unwind bound < -1";
55 unwind_set[func][loop_id]=loop_bound;
64 assert(start->location_number<end->location_number);
65 assert(goto_program.
empty());
68 typedef std::map<goto_programt::const_targett, unsigned> target_mapt;
69 target_mapt target_map;
77 std::vector<goto_programt::targett> target_vector;
78 target_vector.reserve(target_map.size());
79 assert(target_vector.empty());
86 target_vector.push_back(t_new);
89 assert(goto_program.
instructions.size()==target_vector.size());
92 for(std::size_t i=0; i<target_vector.size(); i++)
101 target_mapt::const_iterator m_it=target_map.find(tgt);
103 if(m_it!=target_map.end())
105 unsigned j=m_it->second;
107 assert(j<target_vector.size());
108 t->set_target(target_vector[j]);
120 std::vector<goto_programt::targett> iteration_points;
121 unwind(goto_program, loop_head, loop_exit, k, unwind_strategy,
131 std::vector<goto_programt::targett> &iteration_points)
133 assert(iteration_points.empty());
134 assert(loop_head->location_number<loop_exit->location_number);
145 t->source_location=loop_head->source_location;
146 t->function=loop_head->function;
147 t->location_number=loop_head->location_number;
157 assert(t->is_backwards_goto());
162 if(!t->guard.is_true())
165 exit_cond.make_not();
167 else if(loop_head->is_goto())
169 if(loop_head->get_target()==loop_exit)
170 exit_cond=loop_head->guard;
176 new_t->make_assertion(exit_cond);
178 new_t->make_assumption(exit_cond);
182 new_t->source_location=loop_head->source_location;
183 new_t->function=loop_head->function;
184 new_t->location_number=loop_head->location_number;
188 assert(!rest_program.
empty());
195 iteration_points.resize(k);
202 if(!t_before->is_goto() || !t_before->guard.is_true())
208 t_goto->source_location=loop_exit->source_location;
209 t_goto->function=loop_exit->function;
211 t_goto->location_number=loop_exit->location_number;
220 t_skip->source_location=loop_head->source_location;
221 t_skip->function=loop_head->function;
222 t_skip->location_number=loop_head->location_number;
228 iteration_points[0]=loop_iter;
239 if(t->get_target()==loop_head)
240 t->set_target(loop_iter);
244 for(
unsigned i=1; i<k; i++)
252 copies.destructive_append(tmp_program);
263 t_skip->source_location=loop_head->source_location;
264 t_skip->function=loop_head->function;
265 t_skip->location_number=loop_head->location_number;
275 if(t->location_number>=loop_head->location_number &&
276 t->location_number<loop_exit->location_number)
278 i_it->set_target(t_skip);
287 copies.destructive_append(rest_program);
295 const unsigned loop_id,
299 assert(global_k>=-1);
301 unwind_sett::const_iterator f_it=unwind_set.find(func);
302 if(f_it==unwind_set.end())
305 const std::map<unsigned, int> &m=f_it->second;
306 std::map<unsigned, int>::const_iterator l_it=m.find(loop_id);
330 std::cout <<
"Instruction:\n";
334 if(!i_it->is_backwards_goto())
341 assert(!func.
empty());
343 unsigned loop_number=i_it->loop_number;
345 int final_k=
get_k(func, loop_number, k, unwind_set);
358 unwind(goto_program, loop_head, loop_exit, final_k, unwind_strategy);
381 std::cout <<
"Function: " << it->first <<
'\n';
386 unwind(goto_program, unwind_set, k, unwind_strategy);
396 for(location_mapt::const_iterator it=location_map.begin();
397 it!=location_map.end(); it++)
402 unsigned location_number=it->second;
404 object[
"originalLocationNumber"]=
json_numbert(std::to_string(
406 object[
"newLocationNumber"]=
json_numbert(std::to_string(
407 target->location_number));
bool body_available() const
targett add_instruction()
Adds an instruction at the end.
void insert(const goto_programt::const_targett target, const unsigned location_number)
instructionst instructions
The list of instructions in the goto program.
void parse_unwindset(const std::string &us, unwind_sett &unwind_set)
Goto Programs with Functions.
bool empty() const
Is the program empty?
void operator()(goto_functionst &goto_functions, const unsigned k, const unwind_strategyt unwind_strategy=unwind_strategyt::PARTIAL)
json_arrayt & make_array()
jsont & push_back(const jsont &json)
instructionst::const_iterator const_targett
The boolean constant true.
API to expression classes.
targett const_cast_target(const_targett t)
Convert a const_targett to a targett - use with care and avoid whenever possible. ...
void copy_segment(const goto_programt::const_targett start, const goto_programt::const_targett end, goto_programt &goto_program)
Helper functions for k-induction and loop invariants.
targett insert_before(const_targett target)
Insertion before the given target.
A specialization of goto_program_templatet over goto programs in which instructions have codet type...
int get_k(const irep_idt func, const unsigned loop_id, const int global_k, const unwind_sett &unwind_set) const
void split_string(const std::string &s, char delim, std::vector< std::string > &result, bool strip, bool remove_empty)
Base class for all expressions.
jsont output_log_json() const
#define Forall_goto_functions(it, functions)
#define Forall_goto_program_instructions(it, program)
void destructive_insert(const_targett target, goto_program_templatet< codeT, guardT > &p)
Inserts the given program at the given location.
std::map< irep_idt, std::map< unsigned, int > > unwind_sett
json_objectt & make_object()
void unwind(goto_programt &goto_program, const goto_programt::const_targett loop_head, const goto_programt::const_targett loop_exit, const unsigned k, const unwind_strategyt unwind_strategy)
std::ostream & output_instruction(const class namespacet &ns, const irep_idt &identifier, std::ostream &out, instructionst::const_iterator it) const
See below.
instructionst::iterator targett