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/cprover_prefix.h>
17 #include <util/std_expr.h>
18 #include <util/std_code.h>
19 #include <util/prefix.h>
20 #include <util/symbol_table.h>
21 
23 
24 #include "rw_set.h"
25 
26 #ifdef LOCAL_MAY
28 #endif
29 
31  const rw_set_baset &code_rw_set,
32  const rw_set_baset &isr_rw_set)
33 {
34  // R/W race?
35  forall_rw_set_r_entries(e_it, code_rw_set)
36  {
37  if(isr_rw_set.has_w_entry(e_it->first))
38  return true;
39  }
40 
41  return false;
42 }
43 
45  const rw_set_baset &code_rw_set,
46  const rw_set_baset &isr_rw_set)
47 {
48  // W/R or W/W?
49  forall_rw_set_w_entries(e_it, code_rw_set)
50  {
51  if(isr_rw_set.has_r_entry(e_it->first))
52  return true;
53 
54  if(isr_rw_set.has_w_entry(e_it->first))
55  return true;
56  }
57 
58  return false;
59 }
60 
61 void interrupt(
62  value_setst &value_sets,
63  const symbol_tablet &symbol_table,
64 #ifdef LOCAL_MAY
65  const goto_functionst::goto_functiont &goto_function,
66 #endif
67  goto_programt &goto_program,
68  const symbol_exprt &interrupt_handler,
69  const rw_set_baset &isr_rw_set)
70 {
71  namespacet ns(symbol_table);
72 
73  Forall_goto_program_instructions(i_it, goto_program)
74  {
75  goto_programt::instructiont &instruction=*i_it;
76 
77 #ifdef LOCAL_MAY
78  local_may_aliast local_may(goto_function);
79 #endif
80  rw_set_loct rw_set(ns, value_sets, i_it
81 #ifdef LOCAL_MAY
82  , local_may
83 #endif
84  ); // NOLINT(whitespace/parens)
85 
86  // potential race?
87  bool race_on_read=potential_race_on_read(rw_set, isr_rw_set);
88  bool race_on_write=potential_race_on_write(rw_set, isr_rw_set);
89 
90  if(!race_on_read && !race_on_write)
91  continue;
92 
93  // Insert the call to the ISR.
94  // We do before for races on Read, and before and after
95  // for races on Write.
96 
97  if(race_on_read || race_on_write)
98  {
99  goto_programt::instructiont original_instruction;
100  original_instruction.swap(instruction);
101 
102  const source_locationt &source_location=
103  original_instruction.source_location;
104 
105  code_function_callt isr_call;
106  isr_call.add_source_location()=source_location;
107  isr_call.function()=interrupt_handler;
108 
109  goto_programt::targett t_goto=i_it;
110  goto_programt::targett t_call=goto_program.insert_after(t_goto);
111  goto_programt::targett t_orig=goto_program.insert_after(t_call);
112 
113  t_goto->make_goto(t_orig);
114  t_goto->source_location=source_location;
115  t_goto->guard=side_effect_expr_nondett(bool_typet());
116  t_goto->function=original_instruction.function;
117 
118  t_call->make_function_call(isr_call);
119  t_call->source_location=source_location;
120  t_call->function=original_instruction.function;
121 
122  t_orig->swap(original_instruction);
123 
124  i_it=t_orig; // the for loop already counts us up
125  }
126 
127  if(race_on_write)
128  {
129  // insert _after_ the instruction with race
130  goto_programt::targett t_orig=i_it;
131  t_orig++;
132 
133  goto_programt::targett t_goto=goto_program.insert_after(i_it);
134  goto_programt::targett t_call=goto_program.insert_after(t_goto);
135 
136  const source_locationt &source_location=i_it->source_location;
137 
138  code_function_callt isr_call;
139  isr_call.add_source_location()=source_location;
140  isr_call.function()=interrupt_handler;
141 
142  t_goto->make_goto(t_orig);
143  t_goto->source_location=source_location;
144  t_goto->guard=side_effect_expr_nondett(bool_typet());
145  t_goto->function=i_it->function;
146 
147  t_call->make_function_call(isr_call);
148  t_call->source_location=source_location;
149  t_call->function=i_it->function;
150 
151  i_it=t_call; // the for loop already counts us up
152  }
153  }
154 }
155 
157  const symbol_tablet &symbol_table,
158  const irep_idt &interrupt_handler)
159 {
160  std::list<symbol_exprt> matches;
161 
162  forall_symbol_base_map(m_it, symbol_table.symbol_base_map, interrupt_handler)
163  {
164  // look it up
165  symbol_tablet::symbolst::const_iterator s_it=
166  symbol_table.symbols.find(m_it->second);
167 
168  if(s_it==symbol_table.symbols.end())
169  continue;
170 
171  if(s_it->second.type.id()==ID_code)
172  matches.push_back(s_it->second.symbol_expr());
173  }
174 
175  if(matches.empty())
176  throw "interrupt handler `"+id2string(interrupt_handler)+"' not found";
177 
178  if(matches.size()>=2)
179  throw "interrupt handler `"+id2string(interrupt_handler)+"' is ambiguous";
180 
181  symbol_exprt isr=matches.front();
182 
183  if(!to_code_type(isr.type()).parameters().empty())
184  throw "interrupt handler `"+id2string(interrupt_handler)+
185  "' must not have parameters";
186 
187  return isr;
188 }
189 
191  value_setst &value_sets,
192  const symbol_tablet &symbol_table,
193  goto_functionst &goto_functions,
194  const irep_idt &interrupt_handler)
195 {
196  // look up the ISR
197  symbol_exprt isr=get_isr(symbol_table, interrupt_handler);
198 
199  // we first figure out which objects are read/written by the ISR
200  const namespacet ns(symbol_table);
201  rw_set_functiont isr_rw_set(
202  value_sets, ns, goto_functions, isr);
203 
204  // now instrument
205 
206  Forall_goto_functions(f_it, goto_functions)
207  if(f_it->first!=CPROVER_PREFIX "initialize" &&
208  f_it->first!=goto_functionst::entry_point() &&
209  f_it->first!=isr.get_identifier())
210  interrupt(
211  value_sets, symbol_table,
212 #ifdef LOCAL_MAY
213  f_it->second,
214 #endif
215  f_it->second.body, isr, isr_rw_set);
216 
217  goto_functions.update();
218 }
const std::string & id2string(const irep_idt &d)
Definition: irep.h:44
#define CPROVER_PREFIX
const irep_idt & get_identifier() const
Definition: std_expr.h:120
Goto Programs with Functions.
#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:156
typet & type()
Definition: expr.h:60
The proper Booleans.
Definition: std_types.h:33
symbol_base_mapt symbol_base_map
Definition: symbol_table.h:58
#define forall_rw_set_r_entries(it, rw_set)
Definition: rw_set.h:104
symbolst symbols
Definition: symbol_table.h:57
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
API to expression classes.
The symbol table.
Definition: symbol_table.h:52
TO_BE_DOCUMENTED.
Definition: namespace.h:62
A side effect that returns a non-deterministically chosen value.
Definition: std_code.h:1037
A function call.
Definition: std_code.h:657
goto_function_templatet< goto_programt > goto_functiont
Symbol table.
bool potential_race_on_write(const rw_set_baset &code_rw_set, const rw_set_baset &isr_rw_set)
Definition: interrupt.cpp:44
Interrupt Instrumentation for Goto Programs.
A specialization of goto_program_templatet over goto programs in which instructions have codet type...
Definition: goto_program.h:24
bool potential_race_on_read(const rw_set_baset &code_rw_set, const rw_set_baset &isr_rw_set)
Definition: interrupt.cpp:30
#define forall_symbol_base_map(it, expr, base_name)
Definition: symbol_table.h:39
exprt & function()
Definition: std_code.h:677
#define Forall_goto_functions(it, functions)
const source_locationt & source_location() const
Definition: expr.h:142
const code_typet & to_code_type(const typet &type)
Cast a generic typet to a code_typet.
Definition: std_types.h:884
void swap(irept &irep)
Definition: irep.h:231
source_locationt & add_source_location()
Definition: expr.h:147
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:61
#define Forall_goto_program_instructions(it, program)
Definition: goto_program.h:73
Expression to hold a symbol (variable)
Definition: std_expr.h:82
Field-insensitive, location-sensitive may-alias analysis.
Race Detection for Threaded Goto Programs.