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 <ansi-c/string_constant.h>
13 
14 static bool has_start_thread(const goto_programt &goto_program)
15 {
16  for(const auto &instruction : goto_program.instructions)
17  if(instruction.is_start_thread())
18  return true;
19 
20  return false;
21 }
22 
24 {
25  if(goto_program.instructions.empty())
26  return;
27 
28  // add assertion that all may flags for mutex-locked are gone
29  // at the end
30  goto_programt::targett end=goto_program.instructions.end();
31  end--;
32 
33  assert(end->is_end_function());
34 
35  source_locationt source_location=end->source_location;
36  irep_idt function=end->function;
37 
38  goto_program.insert_before_swap(end);
39 
40  exprt mutex_locked_string=
41  string_constantt("mutex-locked");
42 
43  binary_exprt get_may("get_may");
44 
45  // NULL is any
47  get_may.op1()=address_of_exprt(mutex_locked_string);
48 
49  end->make_assertion(not_exprt(get_may));
50 
51  end->source_location=source_location;
52  end->source_location.set_comment("mutexes must not be locked on thread exit");
53  end->function=function;
54 }
55 
57 {
58  // we'll look for START THREAD
59  std::set<irep_idt> thread_fkts;
60 
61  forall_goto_functions(f_it, goto_functions)
62  {
63  if(has_start_thread(f_it->second.body))
64  {
65  // now look for functions called
66 
67  for(const auto &instruction : f_it->second.body.instructions)
68  if(instruction.is_function_call())
69  {
70  const exprt &function=
71  to_code_function_call(instruction.code).function();
72  if(function.id()==ID_symbol)
73  thread_fkts.insert(to_symbol_expr(function).get_identifier());
74  }
75  }
76  }
77 
78  // now instrument
79  for(const auto &fkt : thread_fkts)
80  {
81  thread_exit_instrumentation(goto_functions.function_map[fkt].body);
82  }
83 }
84 
86  const symbol_tablet &symbol_table,
87  goto_programt &goto_program,
88  typet lock_type)
89 {
90  symbol_tablet::symbolst::const_iterator f_it=
91  symbol_table.symbols.find("__CPROVER_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  code_function_callt call;
108 
109  call.function()=f_it->second.symbol_expr();
110  call.arguments().resize(2);
111  call.arguments()[0]=address_of_exprt(code_assign.lhs());
112  call.arguments()[1]=address_of_exprt(string_constantt("mutex-init"));
113 
114  t->make_function_call(call);
115  t->source_location=it->source_location;
116  }
117  }
118  }
119 }
120 
122  const symbol_tablet &symbol_table,
123  goto_functionst &goto_functions)
124 {
125  // get pthread_mutex_lock
126 
127  symbol_tablet::symbolst::const_iterator f_it=
128  symbol_table.symbols.find("pthread_mutex_lock");
129 
130  if(f_it==symbol_table.symbols.end())
131  return;
132 
133  // get type of lock argument
134  code_typet code_type=to_code_type(to_code_type(f_it->second.type));
135  if(code_type.parameters().size()!=1)
136  return;
137 
138  typet lock_type=code_type.parameters()[0].type();
139 
140  if(lock_type.id()!=ID_pointer)
141  return;
142 
143  Forall_goto_functions(f_it, goto_functions)
145  symbol_table, f_it->second.body, lock_type.subtype());
146 }
The type of an expression.
Definition: type.h:20
Boolean negation.
Definition: std_expr.h:2648
Base type of functions.
Definition: std_types.h:734
pointer_typet pointer_type(const typet &subtype)
Definition: c_types.cpp:296
void mutex_init_instrumentation(const symbol_tablet &symbol_table, goto_programt &goto_program, typet lock_type)
exprt & op0()
Definition: expr.h:84
instructionst instructions
The list of instructions in the goto program.
The null pointer constant.
Definition: std_expr.h:3774
typet & type()
Definition: expr.h:60
static bool has_start_thread(const goto_programt &goto_program)
const code_assignt & to_code_assign(const codet &code)
Definition: std_code.h:178
const irep_idt & id() const
Definition: irep.h:189
exprt & lhs()
Definition: std_code.h:157
argumentst & arguments()
Definition: std_code.h:689
symbolst symbols
Definition: symbol_table.h:57
A generic base class for binary expressions.
Definition: std_expr.h:471
The empty type.
Definition: std_types.h:53
exprt & op1()
Definition: expr.h:87
The symbol table.
Definition: symbol_table.h:52
A function call.
Definition: std_code.h:657
targett insert_after(const_targett target)
Insertion after the given target.
Operator to return the address of an object.
Definition: std_expr.h:2593
A specialization of goto_program_templatet over goto programs in which instructions have codet type...
Definition: goto_program.h:24
exprt & function()
Definition: std_code.h:677
Base class for all expressions.
Definition: expr.h:46
const parameterst & parameters() const
Definition: std_types.h:841
const symbol_exprt & to_symbol_expr(const exprt &expr)
Cast a generic exprt to a symbol_exprt.
Definition: std_expr.h:202
#define Forall_goto_functions(it, functions)
void insert_before_swap(targett target)
Insertion that preserves jumps to "target".
const code_typet & to_code_type(const typet &type)
Cast a generic typet to a code_typet.
Definition: std_types.h:884
#define Forall_goto_program_instructions(it, program)
Definition: goto_program.h:73
const typet & subtype() const
Definition: type.h:31
#define forall_goto_functions(it, functions)
Assignment.
Definition: std_code.h:144
const code_function_callt & to_code_function_call(const codet &code)
Definition: std_code.h:700
void thread_exit_instrumentation(goto_programt &goto_program)