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 static void interrupt(
54  value_setst &value_sets,
55  const symbol_tablet &symbol_table,
56  const irep_idt &function_id,
57 #ifdef LOCAL_MAY
58  const goto_functionst::goto_functiont &goto_function,
59 #endif
60  goto_programt &goto_program,
61  const symbol_exprt &interrupt_handler,
62  const rw_set_baset &isr_rw_set)
63 {
64  namespacet ns(symbol_table);
65 
66  Forall_goto_program_instructions(i_it, goto_program)
67  {
68  goto_programt::instructiont &instruction=*i_it;
69 
70 #ifdef LOCAL_MAY
71  local_may_aliast local_may(goto_function);
72 #endif
73  rw_set_loct rw_set(
74  ns,
75  value_sets,
76  function_id,
77  i_it
78 #ifdef LOCAL_MAY
79  ,
80  local_may
81 #endif
82  ); // NOLINT(whitespace/parens)
83 
84  // potential race?
85  bool race_on_read=potential_race_on_read(rw_set, isr_rw_set);
86  bool race_on_write=potential_race_on_write(rw_set, isr_rw_set);
87 
88  if(!race_on_read && !race_on_write)
89  continue;
90 
91  // Insert the call to the ISR.
92  // We do before for races on Read, and before and after
93  // for races on Write.
94 
95  if(race_on_read || race_on_write)
96  {
97  goto_programt::instructiont original_instruction;
98  original_instruction.swap(instruction);
99 
100  const source_locationt &source_location=
101  original_instruction.source_location;
102 
103  code_function_callt isr_call(interrupt_handler);
104  isr_call.add_source_location()=source_location;
105 
106  goto_programt::targett t_goto=i_it;
107  goto_programt::targett t_call=goto_program.insert_after(t_goto);
108  goto_programt::targett t_orig=goto_program.insert_after(t_call);
109 
110  *t_goto = goto_programt::make_goto(
111  t_orig,
112  side_effect_expr_nondett(bool_typet(), source_location),
113  source_location);
114 
115  *t_call = goto_programt::make_function_call(isr_call, source_location);
116 
117  t_orig->swap(original_instruction);
118 
119  i_it=t_orig; // the for loop already counts us up
120  }
121 
122  if(race_on_write)
123  {
124  // insert _after_ the instruction with race
125  goto_programt::targett t_orig=i_it;
126  t_orig++;
127 
128  const source_locationt &source_location=i_it->source_location;
129 
130  code_function_callt isr_call(interrupt_handler);
131  isr_call.add_source_location()=source_location;
132 
133  goto_programt::targett t_goto = goto_program.insert_after(
134  i_it,
136  t_orig,
137  side_effect_expr_nondett(bool_typet(), source_location),
138  source_location));
139 
140  goto_programt::targett t_call = goto_program.insert_after(
141  t_goto, goto_programt::make_function_call(isr_call, source_location));
142 
143  i_it=t_call; // the for loop already counts us up
144  }
145  }
146 }
147 
148 static symbol_exprt
149 get_isr(const symbol_tablet &symbol_table, const irep_idt &interrupt_handler)
150 {
151  std::list<symbol_exprt> matches;
152 
153  forall_symbol_base_map(m_it, symbol_table.symbol_base_map, interrupt_handler)
154  {
155  // look it up
156  symbol_tablet::symbolst::const_iterator s_it=
157  symbol_table.symbols.find(m_it->second);
158 
159  if(s_it==symbol_table.symbols.end())
160  continue;
161 
162  if(s_it->second.type.id()==ID_code)
163  matches.push_back(s_it->second.symbol_expr());
164  }
165 
166  if(matches.empty())
167  throw "interrupt handler '" + id2string(interrupt_handler) + "' not found";
168 
169  if(matches.size()>=2)
170  throw "interrupt handler '" + id2string(interrupt_handler) +
171  "' 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,
203  goto_model.symbol_table,
204  f_it->first,
205 #ifdef LOCAL_MAY
206  f_it->second,
207 #endif
208  f_it->second.body,
209  isr,
210  isr_rw_set);
211 
212  goto_model.goto_functions.update();
213 }
Forall_goto_program_instructions
#define Forall_goto_program_instructions(it, program)
Definition: goto_program.h:1201
dstringt
dstringt has one field, an unsigned integer no which is an index into a static table of strings.
Definition: dstring.h:37
symbol_tablet
The symbol table.
Definition: symbol_table.h:20
goto_programt::instructiont::source_location
source_locationt source_location
The location of the instruction in the source file.
Definition: goto_program.h:269
forall_rw_set_w_entries
#define forall_rw_set_w_entries(it, rw_set)
Definition: rw_set.h:114
get_isr
static symbol_exprt get_isr(const symbol_tablet &symbol_table, const irep_idt &interrupt_handler)
Definition: interrupt.cpp:149
symbol_table_baset::symbol_base_map
const symbol_base_mapt & symbol_base_map
Read-only field, used to look up symbol names given their base names.
Definition: symbol_table_base.h:33
goto_programt::instructiont::swap
void swap(instructiont &instruction)
Swap two instructions.
Definition: goto_program.h:510
goto_modelt
Definition: goto_model.h:26
bool_typet
The Boolean type.
Definition: std_types.h:37
symbol_exprt
Expression to hold a symbol (variable)
Definition: std_expr.h:82
local_may_aliast
Definition: local_may_alias.h:26
goto_programt::make_goto
static instructiont make_goto(targett _target, const source_locationt &l=source_locationt::nil())
Definition: goto_program.h:998
namespacet
A namespacet is essentially one or two symbol tables bound together, to allow for symbol lookups in t...
Definition: namespace.h:92
goto_programt::make_function_call
static instructiont make_function_call(const code_function_callt &_code, const source_locationt &l=source_locationt::nil())
Create a function call instruction.
Definition: goto_program.h:1049
exprt::type
typet & type()
Return the type of the expression.
Definition: expr.h:81
code_function_callt
codet representation of a function call statement.
Definition: std_code.h:1183
to_code_type
const code_typet & to_code_type(const typet &type)
Cast a typet to a code_typet.
Definition: std_types.h:946
interrupt.h
Interrupt Instrumentation for Goto Programs.
local_may_alias.h
Field-insensitive, location-sensitive may-alias analysis.
id2string
const std::string & id2string(const irep_idt &d)
Definition: irep.h:44
symbol_exprt::get_identifier
const irep_idt & get_identifier() const
Definition: std_expr.h:111
interrupt
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:53
forall_rw_set_r_entries
#define forall_rw_set_r_entries(it, rw_set)
Definition: rw_set.h:110
INITIALIZE_FUNCTION
#define INITIALIZE_FUNCTION
Definition: static_lifetime_init.h:23
code_typet::parameters
const parameterst & parameters() const
Definition: std_types.h:857
potential_race_on_read
static bool potential_race_on_read(const rw_set_baset &code_rw_set, const rw_set_baset &isr_rw_set)
Definition: interrupt.cpp:22
Forall_goto_functions
#define Forall_goto_functions(it, functions)
Definition: goto_functions.h:117
source_locationt
Definition: source_location.h:20
side_effect_expr_nondett
A side_effect_exprt that returns a non-deterministically chosen value.
Definition: std_code.h:1945
goto_functionst::goto_functiont
::goto_functiont goto_functiont
Definition: goto_functions.h:25
rw_set_baset::has_w_entry
bool has_w_entry(irep_idt object) const
Definition: rw_set.h:80
value_setst
Definition: value_sets.h:22
goto_modelt::goto_functions
goto_functionst goto_functions
GOTO functions.
Definition: goto_model.h:33
rw_set_loct
Definition: rw_set.h:186
rw_set_baset
Definition: rw_set.h:35
symbol_table_baset::symbols
const symbolst & symbols
Read-only field, used to look up symbols given their names.
Definition: symbol_table_base.h:30
forall_symbol_base_map
#define forall_symbol_base_map(it, expr, base_name)
Definition: symbol_table.h:11
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
rw_set_baset::has_r_entry
bool has_r_entry(irep_idt object) const
Definition: rw_set.h:85
goto_functionst::entry_point
static irep_idt entry_point()
Get the identifier of the entry point to a goto model.
Definition: goto_functions.h:90
static_lifetime_init.h
exprt::add_source_location
source_locationt & add_source_location()
Definition: expr.h:259
goto_programt::instructiont
This class represents an instruction in the GOTO intermediate representation.
Definition: goto_program.h:179
potential_race_on_write
static bool potential_race_on_write(const rw_set_baset &code_rw_set, const rw_set_baset &isr_rw_set)
Definition: interrupt.cpp:36
goto_modelt::symbol_table
symbol_tablet symbol_table
Symbol table.
Definition: goto_model.h:30
rw_set_functiont
Definition: rw_set.h:212
goto_programt::targett
instructionst::iterator targett
Definition: goto_program.h:579