cprover
Loading...
Searching...
No Matches
thread_instrumentation.cpp
Go to the documentation of this file.
1/*******************************************************************\
2
3Module:
4
5Author: Daniel Kroening, kroening@kroening.com
6
7\*******************************************************************/
8
10
11#include <util/c_types.h>
12#include <util/pointer_expr.h>
14
16
17static 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 assert(end->is_end_function());
37
38 source_locationt source_location = end->source_location();
39
40 goto_program.insert_before_swap(end);
41
42 const string_constantt mutex_locked_string("mutex-locked");
43
44 // NULL is any
47 ID_get_may,
48 address_of_exprt(mutex_locked_string)};
49
50 *end = goto_programt::make_assertion(not_exprt(get_may), source_location);
51
52 end->source_location_nonconst().set_comment(
53 "mutexes must not be locked on thread exit");
54}
55
57{
58 // we'll look for START THREAD
59 std::set<irep_idt> thread_fkts;
60
61 for(const auto &gf_entry : goto_model.goto_functions.function_map)
62 {
63 if(has_start_thread(gf_entry.second.body))
64 {
65 // now look for functions called
66
67 for(const auto &instruction : gf_entry.second.body.instructions)
68 if(instruction.is_function_call())
69 {
70 const exprt &function = instruction.call_function();
71 if(function.id()==ID_symbol)
72 thread_fkts.insert(to_symbol_expr(function).get_identifier());
73 }
74 }
75 }
76
77 // now instrument
78 for(const auto &fkt : thread_fkts)
80 goto_model.goto_functions.function_map[fkt].body);
81}
82
84 const symbol_tablet &symbol_table,
85 goto_programt &goto_program,
86 typet lock_type)
87{
88 symbol_tablet::symbolst::const_iterator f_it =
89 symbol_table.symbols.find(CPROVER_PREFIX "set_must");
90
91 if(f_it==symbol_table.symbols.end())
92 return;
93
94 Forall_goto_program_instructions(it, goto_program)
95 {
96 if(it->is_assign())
97 {
98 if(it->assign_lhs().type() == lock_type)
99 {
100 const code_function_callt call(
101 f_it->second.symbol_expr(),
102 {address_of_exprt(it->assign_lhs()),
103 address_of_exprt(string_constantt("mutex-init"))});
104
105 goto_program.insert_after(
107 }
108 }
109 }
110}
111
113{
114 // get pthread_mutex_lock
115
116 symbol_tablet::symbolst::const_iterator lock_entry =
117 goto_model.symbol_table.symbols.find("pthread_mutex_lock");
118
119 if(lock_entry == goto_model.symbol_table.symbols.end())
120 return;
121
122 // get type of lock argument
123 code_typet code_type = to_code_type(to_code_type(lock_entry->second.type));
124 if(code_type.parameters().size()!=1)
125 return;
126
127 typet lock_type=code_type.parameters()[0].type();
128
129 if(lock_type.id()!=ID_pointer)
130 return;
131
132 for(auto &gf_entry : goto_model.goto_functions.function_map)
133 {
135 goto_model.symbol_table,
136 gf_entry.second.body,
137 to_pointer_type(lock_type).base_type());
138 }
139}
void base_type(typet &type, const namespacet &ns)
Definition: base_type.cpp:109
pointer_typet pointer_type(const typet &subtype)
Definition: c_types.cpp:253
Operator to return the address of an object.
Definition: pointer_expr.h:361
A base class for expressions that are predicates, i.e., Boolean-typed, and that take exactly two argu...
Definition: std_expr.h:643
codet representation of a function call statement.
Base type of functions.
Definition: std_types.h:539
const parameterst & parameters() const
Definition: std_types.h:655
The empty type.
Definition: std_types.h:51
Base class for all expressions.
Definition: expr.h:54
const source_locationt & source_location() const
Definition: expr.h:230
function_mapt function_map
symbol_tablet symbol_table
Symbol table.
Definition: goto_model.h:30
goto_functionst goto_functions
GOTO functions.
Definition: goto_model.h:33
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:598
void insert_before_swap(targett target)
Insertion that preserves jumps to "target".
Definition: goto_program.h:619
instructionst::iterator targett
Definition: goto_program.h:592
targett insert_after(const_targett target)
Insertion after the instruction pointed-to by the given instruction iterator target.
Definition: goto_program.h:684
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:922
const irep_idt & id() const
Definition: irep.h:396
Boolean negation.
Definition: std_expr.h:2181
The null pointer constant.
Definition: pointer_expr.h:723
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:79
static optionalt< smt_termt > get_identifier(const exprt &expr, const std::unordered_map< exprt, smt_identifier_termt, irep_hash > &expression_handle_identifiers, const std::unordered_map< exprt, smt_identifier_termt, irep_hash > &expression_identifiers)
const symbol_exprt & to_symbol_expr(const exprt &expr)
Cast an exprt to a symbol_exprt.
Definition: std_expr.h:189
const code_typet & to_code_type(const typet &type)
Cast a typet to a code_typet.
Definition: std_types.h:744
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)