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 
17 
18 #ifdef LOCAL_MAY
20 #endif
21 
23  const rw_set_baset &code_rw_set,
24  const rw_set_baset &isr_rw_set)
25 {
26  // R/W race?
27  forall_rw_set_r_entries(e_it, code_rw_set)
28  {
29  if(isr_rw_set.has_w_entry(e_it->first))
30  return true;
31  }
32 
33  return false;
34 }
35 
37  const rw_set_baset &code_rw_set,
38  const rw_set_baset &isr_rw_set)
39 {
40  // W/R or W/W?
41  forall_rw_set_w_entries(e_it, code_rw_set)
42  {
43  if(isr_rw_set.has_r_entry(e_it->first))
44  return true;
45 
46  if(isr_rw_set.has_w_entry(e_it->first))
47  return true;
48  }
49 
50  return false;
51 }
52 
53 void interrupt(
54  value_setst &value_sets,
56 #ifdef LOCAL_MAY
57  const goto_functionst::goto_functiont &goto_function,
58 #endif
59  goto_programt &goto_program,
60  const symbol_exprt &interrupt_handler,
61  const rw_set_baset &isr_rw_set)
62 {
64 
65  Forall_goto_program_instructions(i_it, goto_program)
66  {
67  goto_programt::instructiont &instruction=*i_it;
68 
69 #ifdef LOCAL_MAY
70  local_may_aliast local_may(goto_function);
71 #endif
72  rw_set_loct rw_set(ns, value_sets, i_it
73 #ifdef LOCAL_MAY
74  , local_may
75 #endif
76  ); // NOLINT(whitespace/parens)
77 
78  // potential race?
79  bool race_on_read=potential_race_on_read(rw_set, isr_rw_set);
80  bool race_on_write=potential_race_on_write(rw_set, isr_rw_set);
81 
82  if(!race_on_read && !race_on_write)
83  continue;
84 
85  // Insert the call to the ISR.
86  // We do before for races on Read, and before and after
87  // for races on Write.
88 
89  if(race_on_read || race_on_write)
90  {
91  goto_programt::instructiont original_instruction;
92  original_instruction.swap(instruction);
93 
94  const source_locationt &source_location=
95  original_instruction.source_location;
96 
97  code_function_callt isr_call(interrupt_handler);
98  isr_call.add_source_location()=source_location;
99 
100  goto_programt::targett t_goto=i_it;
101  goto_programt::targett t_call=goto_program.insert_after(t_goto);
102  goto_programt::targett t_orig=goto_program.insert_after(t_call);
103 
104  t_goto->make_goto(t_orig);
105  t_goto->source_location=source_location;
106  t_goto->guard = side_effect_expr_nondett(bool_typet(), source_location);
107  t_goto->function=original_instruction.function;
108 
109  t_call->make_function_call(isr_call);
110  t_call->source_location=source_location;
111  t_call->function=original_instruction.function;
112 
113  t_orig->swap(original_instruction);
114 
115  i_it=t_orig; // the for loop already counts us up
116  }
117 
118  if(race_on_write)
119  {
120  // insert _after_ the instruction with race
121  goto_programt::targett t_orig=i_it;
122  t_orig++;
123 
124  goto_programt::targett t_goto=goto_program.insert_after(i_it);
125  goto_programt::targett t_call=goto_program.insert_after(t_goto);
126 
127  const source_locationt &source_location=i_it->source_location;
128 
129  code_function_callt isr_call(interrupt_handler);
130  isr_call.add_source_location()=source_location;
131 
132  t_goto->make_goto(t_orig);
133  t_goto->source_location=source_location;
134  t_goto->guard = side_effect_expr_nondett(bool_typet(), source_location);
135  t_goto->function=i_it->function;
136 
137  t_call->make_function_call(isr_call);
138  t_call->source_location=source_location;
139  t_call->function=i_it->function;
140 
141  i_it=t_call; // the for loop already counts us up
142  }
143  }
144 }
145 
148  const irep_idt &interrupt_handler)
149 {
150  std::list<symbol_exprt> matches;
151 
152  forall_symbol_base_map(m_it, symbol_table.symbol_base_map, interrupt_handler)
153  {
154  // look it up
155  symbol_tablet::symbolst::const_iterator s_it=
156  symbol_table.symbols.find(m_it->second);
157 
158  if(s_it==symbol_table.symbols.end())
159  continue;
160 
161  if(s_it->second.type.id()==ID_code)
162  matches.push_back(s_it->second.symbol_expr());
163  }
164 
165  if(matches.empty())
166  throw "interrupt handler `"+id2string(interrupt_handler)+"' not found";
167 
168  if(matches.size()>=2)
169  throw "interrupt handler `"+id2string(interrupt_handler)+"' is ambiguous";
170 
171  symbol_exprt isr=matches.front();
172 
173  if(!to_code_type(isr.type()).parameters().empty())
174  throw "interrupt handler `"+id2string(interrupt_handler)+
175  "' must not have parameters";
176 
177  return isr;
178 }
179 
181  value_setst &value_sets,
182  goto_modelt &goto_model,
183  const irep_idt &interrupt_handler)
184 {
185  // look up the ISR
186  symbol_exprt isr=
187  get_isr(goto_model.symbol_table, interrupt_handler);
188 
189  // we first figure out which objects are read/written by the ISR
190  rw_set_functiont isr_rw_set(
191  value_sets, goto_model, isr);
192 
193  // now instrument
194 
195  Forall_goto_functions(f_it, goto_model.goto_functions)
196  if(f_it->first != INITIALIZE_FUNCTION &&
197  f_it->first!=goto_functionst::entry_point() &&
198  f_it->first!=isr.get_identifier())
199  interrupt(
200  value_sets, goto_model.symbol_table,
201 #ifdef LOCAL_MAY
202  f_it->second,
203 #endif
204  f_it->second.body, isr, isr_rw_set);
205 
206  goto_model.goto_functions.update();
207 }
irep_idt function
The function this instruction belongs to.
Definition: goto_program.h:184
const std::string & id2string(const irep_idt &d)
Definition: irep.h:44
const code_typet & to_code_type(const typet &type)
Cast a typet to a code_typet.
Definition: std_types.h:982
const symbol_base_mapt & symbol_base_map
const irep_idt & get_identifier() const
Definition: std_expr.h:176
#define forall_rw_set_w_entries(it, rw_set)
Definition: rw_set.h:111
symbol_exprt get_isr(const symbol_tablet &symbol_table, const irep_idt &interrupt_handler)
Definition: interrupt.cpp:146
typet & type()
Return the type of the expression.
Definition: expr.h:68
The Boolean type.
Definition: std_types.h:28
symbol_tablet symbol_table
Symbol table.
Definition: goto_model.h:29
This class represents an instruction in the GOTO intermediate representation.
Definition: goto_program.h:178
#define forall_rw_set_r_entries(it, rw_set)
Definition: rw_set.h:107
instructionst::iterator targett
Definition: goto_program.h:414
bool has_r_entry(irep_idt object) const
Definition: rw_set.h:82
bool has_w_entry(irep_idt object) const
Definition: rw_set.h:77
#define INITIALIZE_FUNCTION
The symbol table.
Definition: symbol_table.h:19
A namespacet is essentially one or two symbol tables bound together, to allow for symbol lookups in t...
Definition: namespace.h:93
::goto_functiont goto_functiont
A side_effect_exprt that returns a non-deterministically chosen value.
Definition: std_code.h:1633
codet representation of a function call statement.
Definition: std_code.h:1036
dstringt has one field, an unsigned integer no which is an index into a static table of strings.
Definition: dstring.h:35
const symbolst & symbols
bool potential_race_on_write(const rw_set_baset &code_rw_set, const rw_set_baset &isr_rw_set)
Definition: interrupt.cpp:36
Interrupt Instrumentation for Goto Programs.
A generic container class for the GOTO intermediate representation of one function.
Definition: goto_program.h:72
bool potential_race_on_read(const rw_set_baset &code_rw_set, const rw_set_baset &isr_rw_set)
Definition: interrupt.cpp:22
void swap(dstringt &b)
Definition: dstring.h:132
static irep_idt entry_point()
Get the identifier of the entry point to a goto model.
#define forall_symbol_base_map(it, expr, base_name)
Definition: symbol_table.h:11
source_locationt source_location
The location of the instruction in the source file.
Definition: goto_program.h:187
#define Forall_goto_functions(it, functions)
void swap(instructiont &instruction)
Swap two instructions.
Definition: goto_program.h:344
source_locationt & add_source_location()
Definition: expr.h:233
void interrupt(value_setst &value_sets, const symbol_tablet &symbol_table, goto_programt &goto_program, const symbol_exprt &interrupt_handler, const rw_set_baset &isr_rw_set)
Definition: interrupt.cpp:53
#define Forall_goto_program_instructions(it, program)
Definition: goto_program.h:809
Expression to hold a symbol (variable)
Definition: std_expr.h:143
goto_functionst goto_functions
GOTO functions.
Definition: goto_model.h:32
Field-insensitive, location-sensitive may-alias analysis.