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 
39  goto_program.insert_before_swap(end);
40 
41  const string_constantt mutex_locked_string("mutex-locked");
42 
43  // NULL is any
44  binary_predicate_exprt get_may{
46  ID_get_may,
47  address_of_exprt(mutex_locked_string)};
48 
49  *end = goto_programt::make_assertion(not_exprt(get_may), source_location);
50 
51  end->source_location.set_comment("mutexes must not be locked on thread exit");
52 }
53 
55 {
56  // we'll look for START THREAD
57  std::set<irep_idt> thread_fkts;
58 
59  forall_goto_functions(f_it, goto_model.goto_functions)
60  {
61  if(has_start_thread(f_it->second.body))
62  {
63  // now look for functions called
64 
65  for(const auto &instruction : f_it->second.body.instructions)
66  if(instruction.is_function_call())
67  {
68  const exprt &function=
69  to_code_function_call(instruction.code).function();
70  if(function.id()==ID_symbol)
71  thread_fkts.insert(to_symbol_expr(function).get_identifier());
72  }
73  }
74  }
75 
76  // now instrument
77  for(const auto &fkt : thread_fkts)
79  goto_model.goto_functions.function_map[fkt].body);
80 }
81 
84  goto_programt &goto_program,
85  typet lock_type)
86 {
87  symbol_tablet::symbolst::const_iterator f_it =
88  symbol_table.symbols.find(CPROVER_PREFIX "set_must");
89 
90  if(f_it==symbol_table.symbols.end())
91  return;
92 
93  Forall_goto_program_instructions(it, goto_program)
94  {
95  if(it->is_assign())
96  {
97  const code_assignt &code_assign=
98  to_code_assign(it->code);
99 
100  if(code_assign.lhs().type()==lock_type)
101  {
102  const code_function_callt call(
103  f_it->second.symbol_expr(),
104  {address_of_exprt(code_assign.lhs()),
105  address_of_exprt(string_constantt("mutex-init"))});
106 
107  goto_program.insert_after(
109  }
110  }
111  }
112 }
113 
115 {
116  // get pthread_mutex_lock
117 
118  symbol_tablet::symbolst::const_iterator lock_entry =
119  goto_model.symbol_table.symbols.find("pthread_mutex_lock");
120 
121  if(lock_entry == goto_model.symbol_table.symbols.end())
122  return;
123 
124  // get type of lock argument
125  code_typet code_type = to_code_type(to_code_type(lock_entry->second.type));
126  if(code_type.parameters().size()!=1)
127  return;
128 
129  typet lock_type=code_type.parameters()[0].type();
130 
131  if(lock_type.id()!=ID_pointer)
132  return;
133 
134  Forall_goto_functions(f_it, goto_model.goto_functions)
136  goto_model.symbol_table,
137  f_it->second.body,
138  to_pointer_type(lock_type).subtype());
139 }
Forall_goto_program_instructions
#define Forall_goto_program_instructions(it, program)
Definition: goto_program.h:1201
symbol_tablet
The symbol table.
Definition: symbol_table.h:20
mutex_init_instrumentation
void mutex_init_instrumentation(const symbol_tablet &symbol_table, goto_programt &goto_program, typet lock_type)
Definition: thread_instrumentation.cpp:82
typet
The type of an expression, extends irept.
Definition: type.h:29
goto_model.h
Symbol Table + CFG.
string_constant.h
exprt
Base class for all expressions.
Definition: expr.h:53
goto_modelt
Definition: goto_model.h:26
goto_functionst::function_map
function_mapt function_map
Definition: goto_functions.h:27
string_constantt
Definition: string_constant.h:16
has_start_thread
static bool has_start_thread(const goto_programt &goto_program)
Definition: thread_instrumentation.cpp:16
thread_instrumentation.h
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
goto_programt::make_assertion
static instructiont make_assertion(const exprt &g, const source_locationt &l=source_locationt::nil())
Definition: goto_program.h:893
empty_typet
The empty type.
Definition: std_types.h:46
null_pointer_exprt
The null pointer constant.
Definition: std_expr.h:3989
binary_predicate_exprt
A base class for expressions that are predicates, i.e., Boolean-typed, and that take exactly two argu...
Definition: std_expr.h:694
code_assignt::lhs
exprt & lhs()
Definition: std_code.h:312
pointer_type
pointer_typet pointer_type(const typet &subtype)
Definition: c_types.cpp:243
to_symbol_expr
const symbol_exprt & to_symbol_expr(const exprt &expr)
Cast an exprt to a symbol_exprt.
Definition: std_expr.h:177
code_typet
Base type of functions.
Definition: std_types.h:736
irept::id
const irep_idt & id() const
Definition: irep.h:418
to_code_function_call
const code_function_callt & to_code_function_call(const codet &code)
Definition: std_code.h:1294
code_typet::parameters
const parameterst & parameters() const
Definition: std_types.h:857
to_pointer_type
const pointer_typet & to_pointer_type(const typet &type)
Cast a typet to a pointer_typet.
Definition: std_types.h:1526
Forall_goto_functions
#define Forall_goto_functions(it, functions)
Definition: goto_functions.h:117
source_locationt
Definition: source_location.h:20
goto_programt::instructions
instructionst instructions
The list of instructions in the goto program.
Definition: goto_program.h:585
goto_modelt::goto_functions
goto_functionst goto_functions
GOTO functions.
Definition: goto_model.h:33
to_code_assign
const code_assignt & to_code_assign(const codet &code)
Definition: std_code.h:383
symbol_table_baset::symbols
const symbolst & symbols
Read-only field, used to look up symbols given their names.
Definition: symbol_table_base.h:30
CPROVER_PREFIX
#define CPROVER_PREFIX
Definition: cprover_prefix.h:14
goto_programt
A generic container class for the GOTO intermediate representation of one function.
Definition: goto_program.h:73
goto_programt::insert_after
targett insert_after(const_targett target)
Insertion after the instruction pointed-to by the given instruction iterator target.
Definition: goto_program.h:655
forall_goto_functions
#define forall_goto_functions(it, functions)
Definition: goto_functions.h:122
address_of_exprt
Operator to return the address of an object.
Definition: std_expr.h:2786
goto_programt::insert_before_swap
void insert_before_swap(targett target)
Insertion that preserves jumps to "target".
Definition: goto_program.h:606
code_assignt
A codet representing an assignment in the program.
Definition: std_code.h:295
thread_exit_instrumentation
void thread_exit_instrumentation(goto_programt &goto_program)
Definition: thread_instrumentation.cpp:25
exprt::source_location
const source_locationt & source_location() const
Definition: expr.h:254
goto_modelt::symbol_table
symbol_tablet symbol_table
Symbol table.
Definition: goto_model.h:30
c_types.h
goto_programt::targett
instructionst::iterator targett
Definition: goto_program.h:579
code_function_callt::function
exprt & function()
Definition: std_code.h:1218
not_exprt
Boolean negation.
Definition: std_expr.h:2843