cprover
interrupt.cpp
Go to the documentation of this file.
1 /*******************************************************************\
2 
3 Module: Interrupt Instrumentation
4 
5 Author: Daniel Kroening
6 
7 Date: September 2011
8 
9 \*******************************************************************/
10 
13 
14 #include "interrupt.h"
15 
16 #include <util/range.h>
17 
19 
20 #ifdef LOCAL_MAY
22 #endif
23 
24 #include "rw_set.h"
25 
27  const rw_set_baset &code_rw_set,
28  const rw_set_baset &isr_rw_set)
29 {
30  // R/W race?
31  for(const auto &r_entry : code_rw_set.r_entries)
32  {
33  if(isr_rw_set.has_w_entry(r_entry.first))
34  return true;
35  }
36 
37  return false;
38 }
39 
41  const rw_set_baset &code_rw_set,
42  const rw_set_baset &isr_rw_set)
43 {
44  // W/R or W/W?
45  for(const auto &w_entry : code_rw_set.w_entries)
46  {
47  if(isr_rw_set.has_r_entry(w_entry.first))
48  return true;
49 
50  if(isr_rw_set.has_w_entry(w_entry.first))
51  return true;
52  }
53 
54  return false;
55 }
56 
57 static void interrupt(
58  value_setst &value_sets,
59  const symbol_tablet &symbol_table,
60  const irep_idt &function_id,
61 #ifdef LOCAL_MAY
62  const goto_functionst::goto_functiont &goto_function,
63 #endif
64  goto_programt &goto_program,
65  const symbol_exprt &interrupt_handler,
66  const rw_set_baset &isr_rw_set)
67 {
68  namespacet ns(symbol_table);
69 
70  Forall_goto_program_instructions(i_it, goto_program)
71  {
72  goto_programt::instructiont &instruction=*i_it;
73 
74 #ifdef LOCAL_MAY
75  local_may_aliast local_may(goto_function);
76 #endif
77  rw_set_loct rw_set(
78  ns,
79  value_sets,
80  function_id,
81  i_it
82 #ifdef LOCAL_MAY
83  ,
84  local_may
85 #endif
86  ); // NOLINT(whitespace/parens)
87 
88  // potential race?
89  bool race_on_read=potential_race_on_read(rw_set, isr_rw_set);
90  bool race_on_write=potential_race_on_write(rw_set, isr_rw_set);
91 
92  if(!race_on_read && !race_on_write)
93  continue;
94 
95  // Insert the call to the ISR.
96  // We do before for races on Read, and before and after
97  // for races on Write.
98 
99  if(race_on_read || race_on_write)
100  {
101  goto_programt::instructiont original_instruction;
102  original_instruction.swap(instruction);
103 
104  const source_locationt &source_location=
105  original_instruction.source_location;
106 
107  code_function_callt isr_call(interrupt_handler);
108  isr_call.add_source_location()=source_location;
109 
110  goto_programt::targett t_goto=i_it;
111  goto_programt::targett t_call=goto_program.insert_after(t_goto);
112  goto_programt::targett t_orig=goto_program.insert_after(t_call);
113 
114  *t_goto = goto_programt::make_goto(
115  t_orig,
116  side_effect_expr_nondett(bool_typet(), source_location),
117  source_location);
118 
119  *t_call = goto_programt::make_function_call(isr_call, source_location);
120 
121  t_orig->swap(original_instruction);
122 
123  i_it=t_orig; // the for loop already counts us up
124  }
125 
126  if(race_on_write)
127  {
128  // insert _after_ the instruction with race
129  goto_programt::targett t_orig=i_it;
130  t_orig++;
131 
132  const source_locationt &source_location=i_it->source_location;
133 
134  code_function_callt isr_call(interrupt_handler);
135  isr_call.add_source_location()=source_location;
136 
137  goto_programt::targett t_goto = goto_program.insert_after(
138  i_it,
140  t_orig,
141  side_effect_expr_nondett(bool_typet(), source_location),
142  source_location));
143 
144  goto_programt::targett t_call = goto_program.insert_after(
145  t_goto, goto_programt::make_function_call(isr_call, source_location));
146 
147  i_it=t_call; // the for loop already counts us up
148  }
149  }
150 }
151 
152 static symbol_exprt
153 get_isr(const symbol_tablet &symbol_table, const irep_idt &interrupt_handler)
154 {
155  std::list<symbol_exprt> matches;
156 
157  for(const auto &symbol_name_entry :
158  equal_range(symbol_table.symbol_base_map, interrupt_handler))
159  {
160  // look it up
161  symbol_tablet::symbolst::const_iterator s_it =
162  symbol_table.symbols.find(symbol_name_entry.second);
163 
164  if(s_it==symbol_table.symbols.end())
165  continue;
166 
167  if(s_it->second.type.id()==ID_code)
168  matches.push_back(s_it->second.symbol_expr());
169  }
170 
171  if(matches.empty())
172  throw "interrupt handler '" + id2string(interrupt_handler) + "' not found";
173 
174  if(matches.size()>=2)
175  throw "interrupt handler '" + id2string(interrupt_handler) +
176  "' is ambiguous";
177 
178  symbol_exprt isr=matches.front();
179 
180  if(!to_code_type(isr.type()).parameters().empty())
181  throw "interrupt handler '" + id2string(interrupt_handler) +
182  "' must not have parameters";
183 
184  return isr;
185 }
186 
188  value_setst &value_sets,
189  goto_modelt &goto_model,
190  const irep_idt &interrupt_handler)
191 {
192  // look up the ISR
193  symbol_exprt isr=
194  get_isr(goto_model.symbol_table, interrupt_handler);
195 
196  // we first figure out which objects are read/written by the ISR
197  rw_set_functiont isr_rw_set(
198  value_sets, goto_model, isr);
199 
200  // now instrument
201 
202  for(auto &gf_entry : goto_model.goto_functions.function_map)
203  {
204  if(
205  gf_entry.first != INITIALIZE_FUNCTION &&
206  gf_entry.first != goto_functionst::entry_point() &&
207  gf_entry.first != isr.get_identifier())
208  {
209  interrupt(
210  value_sets,
211  goto_model.symbol_table,
212  gf_entry.first,
213 #ifdef LOCAL_MAY
214  gf_entry.second,
215 #endif
216  gf_entry.second.body,
217  isr,
218  isr_rw_set);
219  }
220  }
221 
222  goto_model.goto_functions.update();
223 }
The Boolean type.
Definition: std_types.h:36
codet representation of a function call statement.
Definition: std_code.h:1213
const parameterst & parameters() const
Definition: std_types.h:655
dstringt has one field, an unsigned integer no which is an index into a static table of strings.
Definition: dstring.h:37
source_locationt & add_source_location()
Definition: expr.h:235
typet & type()
Return the type of the expression.
Definition: expr.h:82
function_mapt function_map
::goto_functiont goto_functiont
static irep_idt entry_point()
Get the identifier of the entry point to a goto model.
symbol_tablet symbol_table
Symbol table.
Definition: goto_model.h:30
goto_functionst goto_functions
GOTO functions.
Definition: goto_model.h:33
This class represents an instruction in the GOTO intermediate representation.
Definition: goto_program.h:178
source_locationt source_location
The location of the instruction in the source file.
Definition: goto_program.h:431
void swap(instructiont &instruction)
Swap two instructions.
Definition: goto_program.h:577
A generic container class for the GOTO intermediate representation of one function.
Definition: goto_program.h:71
instructionst::iterator targett
Definition: goto_program.h:646
static instructiont make_function_call(const code_function_callt &_code, const source_locationt &l=source_locationt::nil())
Create a function call instruction.
static instructiont make_goto(targett _target, const source_locationt &l=source_locationt::nil())
A namespacet is essentially one or two symbol tables bound together, to allow for symbol lookups in t...
Definition: namespace.h:91
entriest r_entries
Definition: rw_set.h:59
bool has_w_entry(irep_idt object) const
Definition: rw_set.h:79
bool has_r_entry(irep_idt object) const
Definition: rw_set.h:84
entriest w_entries
Definition: rw_set.h:59
A side_effect_exprt that returns a non-deterministically chosen value.
Definition: std_code.h:1966
Expression to hold a symbol (variable)
Definition: std_expr.h:80
const irep_idt & get_identifier() const
Definition: std_expr.h:109
const symbol_base_mapt & symbol_base_map
Read-only field, used to look up symbol names given their base names.
const symbolst & symbols
Read-only field, used to look up symbols given their names.
The symbol table.
Definition: symbol_table.h:14
#define Forall_goto_program_instructions(it, program)
static bool potential_race_on_read(const rw_set_baset &code_rw_set, const rw_set_baset &isr_rw_set)
Definition: interrupt.cpp:26
static bool potential_race_on_write(const rw_set_baset &code_rw_set, const rw_set_baset &isr_rw_set)
Definition: interrupt.cpp:40
static void interrupt(value_setst &value_sets, const symbol_tablet &symbol_table, const irep_idt &function_id, goto_programt &goto_program, const symbol_exprt &interrupt_handler, const rw_set_baset &isr_rw_set)
Definition: interrupt.cpp:57
static symbol_exprt get_isr(const symbol_tablet &symbol_table, const irep_idt &interrupt_handler)
Definition: interrupt.cpp:153
Interrupt Instrumentation for Goto Programs.
const std::string & id2string(const irep_idt &d)
Definition: irep.h:49
Field-insensitive, location-sensitive may-alias analysis.
Ranges: pair of begin and end iterators, which can be initialized from containers,...
ranget< typename multimapt::const_iterator > equal_range(const multimapt &multimap, const typename multimapt::key_type &key)
Utility function to make equal_range method of multimap easier to use by returning a ranget object.
Definition: range.h:541
Race Detection for Threaded Goto Programs.
#define INITIALIZE_FUNCTION
const code_typet & to_code_type(const typet &type)
Cast a typet to a code_typet.
Definition: std_types.h:744