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
60  const symbol_exprt &interrupt_handler,
61  const rw_set_baset &isr_rw_set)
62 {
64 
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;
98  isr_call.add_source_location()=source_location;
99  isr_call.function()=interrupt_handler;
100 
101  goto_programt::targett t_goto=i_it;
104 
105  t_goto->make_goto(t_orig);
106  t_goto->source_location=source_location;
107  t_goto->guard = side_effect_expr_nondett(bool_typet(), source_location);
108  t_goto->function=original_instruction.function;
109 
110  t_call->make_function_call(isr_call);
111  t_call->source_location=source_location;
112  t_call->function=original_instruction.function;
113 
114  t_orig->swap(original_instruction);
115 
116  i_it=t_orig; // the for loop already counts us up
117  }
118 
119  if(race_on_write)
120  {
121  // insert _after_ the instruction with race
122  goto_programt::targett t_orig=i_it;
123  t_orig++;
124 
127 
128  const source_locationt &source_location=i_it->source_location;
129 
130  code_function_callt isr_call;
131  isr_call.add_source_location()=source_location;
132  isr_call.function()=interrupt_handler;
133 
134  t_goto->make_goto(t_orig);
135  t_goto->source_location=source_location;
136  t_goto->guard = side_effect_expr_nondett(bool_typet(), source_location);
137  t_goto->function=i_it->function;
138 
139  t_call->make_function_call(isr_call);
140  t_call->source_location=source_location;
141  t_call->function=i_it->function;
142 
143  i_it=t_call; // the for loop already counts us up
144  }
145  }
146 }
147 
150  const irep_idt &interrupt_handler)
151 {
152  std::list<symbol_exprt> matches;
153 
154  forall_symbol_base_map(m_it, symbol_table.symbol_base_map, interrupt_handler)
155  {
156  // look it up
157  symbol_tablet::symbolst::const_iterator s_it=
158  symbol_table.symbols.find(m_it->second);
159 
160  if(s_it==symbol_table.symbols.end())
161  continue;
162 
163  if(s_it->second.type.id()==ID_code)
164  matches.push_back(s_it->second.symbol_expr());
165  }
166 
167  if(matches.empty())
168  throw "interrupt handler `"+id2string(interrupt_handler)+"' not found";
169 
170  if(matches.size()>=2)
171  throw "interrupt handler `"+id2string(interrupt_handler)+"' is ambiguous";
172 
173  symbol_exprt isr=matches.front();
174 
175  if(!to_code_type(isr.type()).parameters().empty())
176  throw "interrupt handler `"+id2string(interrupt_handler)+
177  "' must not have parameters";
178 
179  return isr;
180 }
181 
183  value_setst &value_sets,
184  goto_modelt &goto_model,
185  const irep_idt &interrupt_handler)
186 {
187  // look up the ISR
188  symbol_exprt isr=
189  get_isr(goto_model.symbol_table, interrupt_handler);
190 
191  // we first figure out which objects are read/written by the ISR
192  rw_set_functiont isr_rw_set(
193  value_sets, goto_model, isr);
194 
195  // now instrument
196 
197  Forall_goto_functions(f_it, goto_model.goto_functions)
198  if(f_it->first != INITIALIZE_FUNCTION &&
199  f_it->first!=goto_functionst::entry_point() &&
200  f_it->first!=isr.get_identifier())
201  interrupt(
202  value_sets, goto_model.symbol_table,
203 #ifdef LOCAL_MAY
204  f_it->second,
205 #endif
206  f_it->second.body, isr, isr_rw_set);
207 
208  goto_model.goto_functions.update();
209 }
irep_idt function
The function this instruction belongs to.
Definition: goto_program.h:179
const std::string & id2string(const irep_idt &d)
Definition: irep.h:44
const code_typet & to_code_type(const typet &type)
Cast a generic typet to a code_typet.
Definition: std_types.h:993
const symbol_base_mapt & symbol_base_map
const irep_idt & get_identifier() const
Definition: std_expr.h:128
#define forall_rw_set_w_entries(it, rw_set)
Definition: rw_set.h:108
symbol_exprt get_isr(const symbol_tablet &symbol_table, const irep_idt &interrupt_handler)
Definition: interrupt.cpp:148
typet & type()
Definition: expr.h:56
The proper Booleans.
Definition: std_types.h:34
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:173
#define forall_rw_set_r_entries(it, rw_set)
Definition: rw_set.h:104
instructionst::iterator targett
Definition: goto_program.h:397
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
TO_BE_DOCUMENTED.
Definition: namespace.h:74
::goto_functiont goto_functiont
targett insert_after(const_targett target)
Insertion after the given target.
Definition: goto_program.h:480
A side effect that returns a non-deterministically chosen value.
Definition: std_code.h:1340
A function call.
Definition: std_code.h:858
dstringt has one field, an unsigned integer no which is an index into a static table of strings...
Definition: dstring.h:33
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:70
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:130
static irep_idt entry_point()
#define forall_symbol_base_map(it, expr, base_name)
Definition: symbol_table.h:11
exprt & function()
Definition: std_code.h:878
source_locationt source_location
The location of the instruction in the source file.
Definition: goto_program.h:182
#define Forall_goto_functions(it, functions)
const source_locationt & source_location() const
Definition: expr.h:125
void swap(instructiont &instruction)
Swap two instructions.
Definition: goto_program.h:339
goto_programt & goto_program
Definition: cover.cpp:63
source_locationt & add_source_location()
Definition: expr.h:130
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:740
Expression to hold a symbol (variable)
Definition: std_expr.h:90
goto_functionst goto_functions
GOTO functions.
Definition: goto_model.h:32
Field-insensitive, location-sensitive may-alias analysis.