cprover
thread_instrumentation.cpp
Go to the documentation of this file.
1 /*******************************************************************\
2 
3 Module:
4 
5 Author: Daniel Kroening, kroening@kroening.com
6 
7 \*******************************************************************/
8 
10 
11 #include <util/c_types.h>
12 #include <util/string_constant.h>
13 
15 
16 static bool has_start_thread(const goto_programt &goto_program)
17 {
18  for(const auto &instruction : goto_program.instructions)
19  if(instruction.is_start_thread())
20  return true;
21 
22  return false;
23 }
24 
26 {
27  if(goto_program.instructions.empty())
28  return;
29 
30  // add assertion that all may flags for mutex-locked are gone
31  // at the end
32  goto_programt::targett end=goto_program.instructions.end();
33  end--;
34 
35  assert(end->is_end_function());
36 
37  source_locationt source_location=end->source_location;
38  irep_idt function=end->function;
39 
40  goto_program.insert_before_swap(end);
41 
42  const string_constantt mutex_locked_string("mutex-locked");
43 
44  binary_exprt get_may("get_may");
45 
46  // NULL is any
48  get_may.op1()=address_of_exprt(mutex_locked_string);
49 
50  end->make_assertion(not_exprt(get_may));
51 
52  end->source_location=source_location;
53  end->source_location.set_comment("mutexes must not be locked on thread exit");
54  end->function=function;
55 }
56 
58 {
59  // we'll look for START THREAD
60  std::set<irep_idt> thread_fkts;
61 
62  forall_goto_functions(f_it, goto_model.goto_functions)
63  {
64  if(has_start_thread(f_it->second.body))
65  {
66  // now look for functions called
67 
68  for(const auto &instruction : f_it->second.body.instructions)
69  if(instruction.is_function_call())
70  {
71  const exprt &function=
72  to_code_function_call(instruction.code).function();
73  if(function.id()==ID_symbol)
74  thread_fkts.insert(to_symbol_expr(function).get_identifier());
75  }
76  }
77  }
78 
79  // now instrument
80  for(const auto &fkt : thread_fkts)
82  goto_model.goto_functions.function_map[fkt].body);
83 }
84 
87  goto_programt &goto_program,
88  typet lock_type)
89 {
90  symbol_tablet::symbolst::const_iterator f_it =
91  symbol_table.symbols.find(CPROVER_PREFIX "set_must");
92 
93  if(f_it==symbol_table.symbols.end())
94  return;
95 
96  Forall_goto_program_instructions(it, goto_program)
97  {
98  if(it->is_assign())
99  {
100  const code_assignt &code_assign=
101  to_code_assign(it->code);
102 
103  if(code_assign.lhs().type()==lock_type)
104  {
105  goto_programt::targett t=goto_program.insert_after(it);
106 
107  const code_function_callt call(
108  f_it->second.symbol_expr(),
109  {address_of_exprt(code_assign.lhs()),
110  address_of_exprt(string_constantt("mutex-init"))});
111 
112  t->make_function_call(call);
113  t->source_location=it->source_location;
114  }
115  }
116  }
117 }
118 
120 {
121  // get pthread_mutex_lock
122 
123  symbol_tablet::symbolst::const_iterator lock_entry =
124  goto_model.symbol_table.symbols.find("pthread_mutex_lock");
125 
126  if(lock_entry == goto_model.symbol_table.symbols.end())
127  return;
128 
129  // get type of lock argument
130  code_typet code_type = to_code_type(to_code_type(lock_entry->second.type));
131  if(code_type.parameters().size()!=1)
132  return;
133 
134  typet lock_type=code_type.parameters()[0].type();
135 
136  if(lock_type.id()!=ID_pointer)
137  return;
138 
139  Forall_goto_functions(f_it, goto_model.goto_functions)
141  goto_model.symbol_table,
142  f_it->second.body,
143  to_pointer_type(lock_type).subtype());
144 }
The type of an expression, extends irept.
Definition: type.h:27
Boolean negation.
Definition: std_expr.h:3308
Base type of functions.
Definition: std_types.h:751
void insert_before_swap(targett target)
Insertion that preserves jumps to "target".
Definition: goto_program.h:477
pointer_typet pointer_type(const typet &subtype)
Definition: c_types.cpp:243
void mutex_init_instrumentation(const symbol_tablet &symbol_table, goto_programt &goto_program, typet lock_type)
exprt & op0()
Definition: expr.h:84
#define CPROVER_PREFIX
const code_typet & to_code_type(const typet &type)
Cast a typet to a code_typet.
Definition: std_types.h:982
The null pointer constant.
Definition: std_expr.h:4471
function_mapt function_map
typet & type()
Return the type of the expression.
Definition: expr.h:68
symbol_tablet symbol_table
Symbol table.
Definition: goto_model.h:29
static bool has_start_thread(const goto_programt &goto_program)
const code_assignt & to_code_assign(const codet &code)
Definition: std_code.h:334
const irep_idt & id() const
Definition: irep.h:259
exprt & lhs()
Definition: std_code.h:269
Symbol Table + CFG.
A base class for binary expressions.
Definition: std_expr.h:738
instructionst::iterator targett
Definition: goto_program.h:414
The empty type.
Definition: std_types.h:48
instructionst instructions
The list of instructions in the goto program.
Definition: goto_program.h:420
exprt & op1()
Definition: expr.h:87
The symbol table.
Definition: symbol_table.h:19
targett insert_after(const_targett target)
Insertion after the instruction pointed-to by the given instruction iterator target.
Definition: goto_program.h:518
codet representation of a function call statement.
Definition: std_code.h:1036
const symbol_exprt & to_symbol_expr(const exprt &expr)
Cast an exprt to a symbol_exprt.
Definition: std_expr.h:251
dstringt has one field, an unsigned integer no which is an index into a static table of strings...
Definition: dstring.h:35
Operator to return the address of an object.
Definition: std_expr.h:3255
const symbolst & symbols
A generic container class for the GOTO intermediate representation of one function.
Definition: goto_program.h:72
exprt & function()
Definition: std_code.h:1099
Base class for all expressions.
Definition: expr.h:54
const parameterst & parameters() const
Definition: std_types.h:893
#define Forall_goto_functions(it, functions)
const source_locationt & source_location() const
Definition: expr.h:228
#define Forall_goto_program_instructions(it, program)
Definition: goto_program.h:809
const pointer_typet & to_pointer_type(const typet &type)
Cast a typet to a pointer_typet.
Definition: std_types.h:1544
#define forall_goto_functions(it, functions)
goto_functionst goto_functions
GOTO functions.
Definition: goto_model.h:32
A codet representing an assignment in the program.
Definition: std_code.h:256
const code_function_callt & to_code_function_call(const codet &code)
Definition: std_code.h:1173
void thread_exit_instrumentation(goto_programt &goto_program)