CBMC
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/pointer_expr.h>
13 #include <util/string_constant.h>
14 
16 
17 static bool has_start_thread(const goto_programt &goto_program)
18 {
19  for(const auto &instruction : goto_program.instructions)
20  if(instruction.is_start_thread())
21  return true;
22 
23  return false;
24 }
25 
27 {
28  if(goto_program.instructions.empty())
29  return;
30 
31  // add assertion that all may flags for mutex-locked are gone
32  // at the end
33  goto_programt::targett end=goto_program.instructions.end();
34  end--;
35 
36  DATA_INVARIANT(end->is_end_function(), "must be end of function");
37 
38  goto_program.insert_before_swap(end);
39 
40  const string_constantt mutex_locked_string("mutex-locked");
41 
42  // NULL is any
43  binary_predicate_exprt get_may{
45  ID_get_may,
46  address_of_exprt(mutex_locked_string)};
47 
48  source_locationt source_location = end->source_location();
49  source_location.set_comment("mutexes must not be locked on thread exit");
50  *end = goto_programt::make_assertion(not_exprt(get_may), source_location);
51 }
52 
54 {
55  // we'll look for START THREAD
56  std::set<irep_idt> thread_fkts;
57 
58  for(const auto &gf_entry : goto_model.goto_functions.function_map)
59  {
60  if(has_start_thread(gf_entry.second.body))
61  {
62  // now look for functions called
63 
64  for(const auto &instruction : gf_entry.second.body.instructions)
65  if(instruction.is_function_call())
66  {
67  const exprt &function = instruction.call_function();
68  if(function.id()==ID_symbol)
69  thread_fkts.insert(to_symbol_expr(function).get_identifier());
70  }
71  }
72  }
73 
74  // now instrument
75  for(const auto &fkt : thread_fkts)
77  goto_model.goto_functions.function_map[fkt].body);
78 }
79 
81  const symbol_tablet &symbol_table,
82  goto_programt &goto_program,
83  typet lock_type)
84 {
85  symbol_tablet::symbolst::const_iterator f_it =
86  symbol_table.symbols.find(CPROVER_PREFIX "set_must");
87 
88  if(f_it==symbol_table.symbols.end())
89  return;
90 
91  Forall_goto_program_instructions(it, goto_program)
92  {
93  if(it->is_assign())
94  {
95  if(it->assign_lhs().type() == lock_type)
96  {
97  const code_function_callt call(
98  f_it->second.symbol_expr(),
99  {address_of_exprt(it->assign_lhs()),
100  address_of_exprt(string_constantt("mutex-init"))});
101 
102  goto_program.insert_after(
104  }
105  }
106  }
107 }
108 
110 {
111  // get pthread_mutex_lock
112 
113  symbol_tablet::symbolst::const_iterator lock_entry =
114  goto_model.symbol_table.symbols.find("pthread_mutex_lock");
115 
116  if(lock_entry == goto_model.symbol_table.symbols.end())
117  return;
118 
119  // get type of lock argument
120  code_typet code_type = to_code_type(to_code_type(lock_entry->second.type));
121  if(code_type.parameters().size()!=1)
122  return;
123 
124  typet lock_type=code_type.parameters()[0].type();
125 
126  if(lock_type.id()!=ID_pointer)
127  return;
128 
129  for(auto &gf_entry : goto_model.goto_functions.function_map)
130  {
132  goto_model.symbol_table,
133  gf_entry.second.body,
134  to_pointer_type(lock_type).base_type());
135  }
136 }
pointer_typet pointer_type(const typet &subtype)
Definition: c_types.cpp:235
Operator to return the address of an object.
Definition: pointer_expr.h:540
A base class for expressions that are predicates, i.e., Boolean-typed, and that take exactly two argu...
Definition: std_expr.h:731
goto_instruction_codet representation of a function call statement.
Base type of functions.
Definition: std_types.h:583
const parameterst & parameters() const
Definition: std_types.h:699
The empty type.
Definition: std_types.h:51
Base class for all expressions.
Definition: expr.h:56
const source_locationt & source_location() const
Definition: expr.h:231
function_mapt function_map
symbol_tablet symbol_table
Symbol table.
Definition: goto_model.h:31
goto_functionst goto_functions
GOTO functions.
Definition: goto_model.h:34
A generic container class for the GOTO intermediate representation of one function.
Definition: goto_program.h:73
instructionst instructions
The list of instructions in the goto program.
Definition: goto_program.h:622
void insert_before_swap(targett target)
Insertion that preserves jumps to "target".
Definition: goto_program.h:643
instructionst::iterator targett
Definition: goto_program.h:614
targett insert_after(const_targett target)
Insertion after the instruction pointed-to by the given instruction iterator target.
Definition: goto_program.h:708
static instructiont make_function_call(const code_function_callt &_code, const source_locationt &l=source_locationt::nil())
Create a function call instruction.
static instructiont make_assertion(const exprt &g, const source_locationt &l=source_locationt::nil())
Definition: goto_program.h:933
const irep_idt & id() const
Definition: irep.h:388
Boolean negation.
Definition: std_expr.h:2327
The null pointer constant.
Definition: pointer_expr.h:909
void set_comment(const irep_idt &comment)
const symbolst & symbols
Read-only field, used to look up symbols given their names.
The symbol table.
Definition: symbol_table.h:14
The type of an expression, extends irept.
Definition: type.h:29
#define CPROVER_PREFIX
Symbol Table + CFG.
#define Forall_goto_program_instructions(it, program)
API to expression classes for Pointers.
const pointer_typet & to_pointer_type(const typet &type)
Cast a typet to a pointer_typet.
Definition: pointer_expr.h:93
#define DATA_INVARIANT(CONDITION, REASON)
This condition should be used to document that assumptions that are made on goto_functions,...
Definition: invariant.h:534
const symbol_exprt & to_symbol_expr(const exprt &expr)
Cast an exprt to a symbol_exprt.
Definition: std_expr.h:272
const code_typet & to_code_type(const typet &type)
Cast a typet to a code_typet.
Definition: std_types.h:788
void thread_exit_instrumentation(goto_programt &goto_program)
void mutex_init_instrumentation(const symbol_tablet &symbol_table, goto_programt &goto_program, typet lock_type)
static bool has_start_thread(const goto_programt &goto_program)