add_race_assertions.cpp File Reference

#include <goto-programs/add_race_assertions.h>
#include <functional>
#include <goto-programs/exception_globals.h>
#include <goto-programs/remove_no_op.h>
#include <goto-programs/rw_set.h>
#include <pointer-analysis/value_sets.h>
#include <util/expr/expr_util.h>
#include <util/irep/migrate.h>
#include <irep2/irep2_guard.h>
#include <util/base/prefix.h>
#include <util/irep/std_expr.h>
#include <util/symtab/symbol_generator.h>
#include <algorithm>
#include <map>
#include <set>

Include dependency graph for add_race_assertions.cpp:

Classes
class	w_guardst

Typedefs
using	escaping_paramst = std::map<irep_idt, std::set<unsigned>>

Functions
static void	collect_address_taken (const expr2tc &expr, rw_sett::shared_localst &out)
static expr2tc	lvalue_root (const expr2tc &e)
static void	collect_thread_escaped_locals (const goto_programt &goto_program, const namespacet &ns, rw_sett::shared_localst &out)
static bool	mentions_symbol (const expr2tc &e, const irep_idt &name)
static escaping_paramst	compute_escaping_params (const goto_functionst &goto_functions, const namespacet &ns)
static void	collect_escapes_through_calls (const goto_functionst &goto_functions, const escaping_paramst &esc, rw_sett::shared_localst &out)
static void	collect_address_taken_functions (const expr2tc &e, const goto_functionst &goto_functions, std::set< irep_idt > &escaped)
static void	collect_callees (const goto_programt &body, std::set< irep_idt > &out)
	Direct callees of body, plus every function whose address it takes (a function pointer may be called from anywhere, so counting it as a callee only ever over-approximates reachability).
static std::set< irep_idt >	closure (const goto_functionst &goto_functions, const std::set< irep_idt > &seeds)
static std::set< irep_idt >	compute_pre_thread_functions (const goto_functionst &goto_functions)
	Functions that provably run before any thread exists.
static std::set< irep_idt >	compute_always_atomic_functions (const goto_functionst &goto_functions)
static bool	call_runs_body (const expr2tc &code, const namespacet &ns)
static bool	has_write (const rw_sett &rw_set)
static bool	stores_call_result_in_shared (const goto_programt::instructiont &instruction, const rw_sett &rw_set, const namespacet &ns)
static bool	emitted_after_atomic_block (const goto_programt::instructiont &instruction, const namespacet &ns)
static bool	is_exception_dispatch (const goto_programt::instructiont &instruction)
static void	store_call_result_via_local (contextt &context, goto_programt &goto_program, goto_programt::targett call_it, symbol_generator &tmp_sym)
static goto_programt::instructiont	yield_instruction (contextt &context, const locationt &location)
void	add_race_assertions (contextt &context, goto_programt &goto_program, w_guardst &w_guards, const rw_sett::shared_localst &shared_locals, bool body_is_atomic, symbol_generator &tmp_sym)
void	add_race_assertions (contextt &context, goto_programt &goto_program)
static void	yield_after_lock_releases (contextt &context, goto_functionst &goto_functions)
	A release lets another thread acquire before the releasing one runs on.
void	add_race_assertions (contextt &context, goto_functionst &goto_functions)

Typedef Documentation

escaping_paramst

using escaping_paramst = std::map<irep_idt, std::set<unsigned>>

Function Documentation

add_race_assertions() [1/3]

void add_race_assertions	(	contextt &	context,
		goto_functionst &	goto_functions )

add_race_assertions() [2/3]

void add_race_assertions	(	contextt &	context,
		goto_programt &	goto_program )

add_race_assertions() [3/3]

void add_race_assertions	(	contextt &	context,
		goto_programt &	goto_program,
		w_guardst &	w_guards,
		const rw_sett::shared_localst &	shared_locals,
		bool	body_is_atomic,
		symbol_generator &	tmp_sym )

call_runs_body()

bool call_runs_body ( const expr2tc & code, const namespacet & ns )

static

closure()

std::set< irep_idt > closure ( const goto_functionst & goto_functions, const std::set< irep_idt > & seeds )

static

collect_address_taken()

void collect_address_taken ( const expr2tc & expr, rw_sett::shared_localst & out )

static

collect_address_taken_functions()

void collect_address_taken_functions ( const expr2tc & e, const goto_functionst & goto_functions, std::set< irep_idt > & escaped )

static

collect_callees()

void collect_callees ( const goto_programt & body, std::set< irep_idt > & out )

static

Direct callees of body, plus every function whose address it takes (a function pointer may be called from anywhere, so counting it as a callee only ever over-approximates reachability).

collect_escapes_through_calls()

void collect_escapes_through_calls ( const goto_functionst & goto_functions, const escaping_paramst & esc, rw_sett::shared_localst & out )

static

collect_thread_escaped_locals()

void collect_thread_escaped_locals ( const goto_programt & goto_program, const namespacet & ns, rw_sett::shared_localst & out )

static

compute_always_atomic_functions()

std::set< irep_idt > compute_always_atomic_functions ( const goto_functionst & goto_functions )

static

compute_escaping_params()

escaping_paramst compute_escaping_params ( const goto_functionst & goto_functions, const namespacet & ns )

static

compute_pre_thread_functions()

std::set< irep_idt > compute_pre_thread_functions ( const goto_functionst & goto_functions )

static

Functions that provably run before any thread exists.

__ESBMC_main performs the program's initialisation and then calls the entry point; only code reachable from the entry point ever creates a thread. So everything __ESBMC_main calls before its first spawn-reaching callee runs single-threaded, and those accesses cannot race with anything.

Worth suppressing rather than merely correct to suppress: each instrumented access costs a yield and two updates of the (infinite) race-flag array, and the Python frontend's generated python_init alone carries ~78 of them (github #6610). A function that also runs after the entry point is excluded, so this never hides an access that could race.

emitted_after_atomic_block()

bool emitted_after_atomic_block ( const goto_programt::instructiont & instruction, const namespacet & ns )

static

has_write()

bool has_write ( const rw_sett & rw_set )

static

is_exception_dispatch()

bool is_exception_dispatch ( const goto_programt::instructiont & instruction )

static

lvalue_root()

expr2tc lvalue_root ( const expr2tc & e )

static

mentions_symbol()

bool mentions_symbol ( const expr2tc & e, const irep_idt & name )

static

store_call_result_via_local()

void store_call_result_via_local ( contextt & context, goto_programt & goto_program, goto_programt::targett call_it, symbol_generator & tmp_sym )

static

stores_call_result_in_shared()

bool stores_call_result_in_shared ( const goto_programt::instructiont & instruction, const rw_sett & rw_set, const namespacet & ns )

static

yield_after_lock_releases()

void yield_after_lock_releases ( contextt & context, goto_functionst & goto_functions )

static

A release lets another thread acquire before the releasing one runs on.

The switch point at the end of each release exists only under race checking, where a race may need exactly that order and no shared access follows to provide one (#8189). Placing it in the callee covers calls through a pointer.

yield_instruction()

goto_programt::instructiont yield_instruction ( contextt & context, const locationt & location )

static