cprover
skip_loops.cpp
Go to the documentation of this file.
1 /*******************************************************************\
2 
3 Module: Skip over selected loops by adding gotos
4 
5 Author: Michael Tautschnig
6 
7 Date: January 2016
8 
9 \*******************************************************************/
10 
13 
14 #include "skip_loops.h"
15 
16 #include <util/message.h>
17 #include <util/string2int.h>
18 
20 
21 typedef std::set<unsigned> loop_idst;
22 typedef std::map<irep_idt, loop_idst> loop_mapt;
23 
24 static bool skip_loops(
25  goto_programt &goto_program,
26  const loop_idst &loop_ids,
28 {
29  loop_idst::const_iterator l_it=loop_ids.begin();
30  Forall_goto_program_instructions(it, goto_program)
31  {
32  if(l_it==loop_ids.end())
33  break;
34  if(!it->is_backwards_goto())
35  continue;
36 
37  const unsigned loop_id=it->loop_number;
38  if(*l_it<loop_id)
39  break; // error handled below
40  if(*l_it>loop_id)
41  continue;
42 
43  goto_programt::targett loop_head=it->get_target();
44  goto_programt::targett next=it;
45  ++next;
46  assert(next!=goto_program.instructions.end());
47 
48  goto_program.insert_before(
49  loop_head,
51 
52  ++l_it;
53  }
54  if(l_it!=loop_ids.end())
55  {
56  message.error() << "Loop " << *l_it << " not found"
57  << messaget::eom;
58  return true;
59  }
60 
61  return false;
62 }
63 
64 static bool parse_loop_ids(
65  const std::string &loop_ids,
66  loop_mapt &loop_map)
67 {
68  std::string::size_type length=loop_ids.length();
69 
70  for(std::string::size_type idx=0; idx<length; idx++)
71  {
72  std::string::size_type next=loop_ids.find(",", idx);
73  std::string val=loop_ids.substr(idx, next-idx);
74  std::string::size_type delim=val.rfind(".");
75 
76  if(delim==std::string::npos)
77  return true;
78 
79  std::string fn=val.substr(0, delim);
80  unsigned nr=safe_string2unsigned(val.substr(delim+1));
81 
82  loop_map[fn].insert(nr);
83 
84  if(next==std::string::npos)
85  break;
86  idx=next;
87  }
88 
89  return false;
90 }
91 
93  goto_modelt &goto_model,
94  const std::string &loop_ids,
95  message_handlert &message_handler)
96 {
97  messaget message(message_handler);
98 
99  loop_mapt loop_map;
100  if(parse_loop_ids(loop_ids, loop_map))
101  {
102  message.error() << "Failed to parse loop ids" << messaget::eom;
103  return true;
104  }
105 
106  loop_mapt::const_iterator it=loop_map.begin();
107  Forall_goto_functions(f_it, goto_model.goto_functions)
108  {
109  if(it==loop_map.end() || it->first<f_it->first)
110  break; // possible error handled below
111  else if(it->first==f_it->first)
112  {
113  if(skip_loops(f_it->second.body, it->second, message))
114  return true;
115  ++it;
116  }
117  }
118  if(it!=loop_map.end())
119  {
120  message.error() << "No function " << it->first << " in goto program"
121  << messaget::eom;
122  return true;
123  }
124 
125  // update counters etc.
126  goto_model.goto_functions.update();
127 
128  return false;
129 }
messaget
Class that provides messages with a built-in verbosity 'level'.
Definition: message.h:155
Forall_goto_program_instructions
#define Forall_goto_program_instructions(it, program)
Definition: goto_program.h:1201
parse_loop_ids
static bool parse_loop_ids(const std::string &loop_ids, loop_mapt &loop_map)
Definition: skip_loops.cpp:64
loop_mapt
std::map< irep_idt, loop_idst > loop_mapt
Definition: skip_loops.cpp:22
skip_loops.h
Skip over selected loops by adding gotos.
irept::find
const irept & find(const irep_namet &name) const
Definition: irep.cpp:103
skip_loops
static bool skip_loops(goto_programt &goto_program, const loop_idst &loop_ids, messaget &message)
Definition: skip_loops.cpp:24
goto_model.h
Symbol Table + CFG.
loop_idst
std::set< unsigned > loop_idst
Definition: skip_loops.cpp:21
goto_modelt
Definition: goto_model.h:26
messaget::eom
static eomt eom
Definition: message.h:297
goto_programt::make_goto
static instructiont make_goto(targett _target, const source_locationt &l=source_locationt::nil())
Definition: goto_program.h:998
message
static const char * message(const static_verifier_resultt::statust &status)
Makes a status message string from a status.
Definition: static_verifier.cpp:74
string2int.h
goto_programt::insert_before
targett insert_before(const_targett target)
Insertion before the instruction pointed-to by the given instruction iterator target.
Definition: goto_program.h:639
message_handlert
Definition: message.h:28
safe_string2unsigned
unsigned safe_string2unsigned(const std::string &str, int base)
Definition: string2int.cpp:19
Forall_goto_functions
#define Forall_goto_functions(it, functions)
Definition: goto_functions.h:117
goto_programt::instructions
instructionst instructions
The list of instructions in the goto program.
Definition: goto_program.h:585
goto_modelt::goto_functions
goto_functionst goto_functions
GOTO functions.
Definition: goto_model.h:33
goto_functionst::update
void update()
Definition: goto_functions.h:81
goto_programt
A generic container class for the GOTO intermediate representation of one function.
Definition: goto_program.h:73
size_type
unsignedbv_typet size_type()
Definition: c_types.cpp:58
message.h
true_exprt
The Boolean constant true.
Definition: std_expr.h:3955
exprt::source_location
const source_locationt & source_location() const
Definition: expr.h:254
goto_programt::targett
instructionst::iterator targett
Definition: goto_program.h:579