cprover_library.cpp File Reference

#include <c2goto/cprover_library.h>
#include "util/expr/symbolic_types.h"
#include <ac_config.h>
#include <boost/filesystem.hpp>
#include <cstdlib>
#include <fstream>
#include <goto-programs/goto_binary_reader.h>
#include <util/symtab/context.h>
#include <util/message/message.h>
#include <util/base/time_stopping.h>
#include <util/lang/c_link.h>
#include <util/config/config.h>
#include <util/lang/language.h>
#include <goto-programs/goto_functions.h>
#include <list>
#include <unordered_set>

Include dependency graph for cprover_library.cpp:

Classes
struct	library_load_report

Functions
static void	generate_symbol_deps (irep_idt name, irept irep, std::multimap< irep_idt, irep_idt > &deps)
static bool	is_cbmc_memory_primitive (const symbolt &s)
static std::unordered_set< std::string >	program_references (const contextt &ctx)
	Names the program's own symbols refer to, including through their types.
static bool	store_library_symbol (const contextt &context, const symbolt &s, bool bundled_wholesale, const std::unordered_set< std::string > &referenced)
	Whether a library symbol belongs in the context handed to the rest of the run.
static void	ingest_symbol (irep_idt name, std::multimap< irep_idt, irep_idt > &deps, std::list< irep_idt > &to_include)
static void	read_python_blob (bool is_python, contextt &new_ctx, contextt &ignored_ctx)
	Merge the Python operational models into what was already read from clib.
static void	report_library_load (const library_load_report &r)
void	record_library_symbol (const irep_idt &id)
	Record that id came from a bundled operational-model library rather than from the program.
static void	collect_expr_deps (const irep_idt &from, const expr2tc &e, std::multimap< irep_idt, irep_idt > &deps)
	Record every symbol e names, however deeply, as a dependency of from.
void	prune_unreferenced_library_functions (contextt &context, const goto_functionst *prelowered)
	Erase every library FUNCTION symbol not reachable from the program's own symbols, so goto_convert never lowers it.
void	assert_no_pruned_calls (const goto_functionst &functions)
	Abort if any call in functions targets a symbol the prune erased.
void	add_cprover_library (contextt &context, const languaget *language)

Variables
const uint8_t	clib32_buf []
const uint8_t	clib64_buf []
const unsigned int	clib32_buf_size
const unsigned int	clib64_buf_size
const uint8_t	clib32_fp_buf []
const uint8_t	clib64_fp_buf []
const unsigned int	clib32_fp_buf_size
const unsigned int	clib64_fp_buf_size
const uint8_t	clib32_cherih_buf []
const uint8_t	clib64_cherih_buf []
const unsigned int	clib32_cherih_buf_size
const unsigned int	clib64_cherih_buf_size
const uint8_t	clib32_fp_cherih_buf []
const uint8_t	clib64_fp_cherih_buf []
const unsigned int	clib32_fp_cherih_buf_size
const unsigned int	clib64_fp_cherih_buf_size
const uint8_t	clib32_cherip_buf []
const uint8_t	clib64_cherip_buf []
const unsigned int	clib32_cherip_buf_size
const unsigned int	clib64_cherip_buf_size
const uint8_t	clib32_fp_cherip_buf []
const uint8_t	clib64_fp_cherip_buf []
const unsigned int	clib32_fp_cherip_buf_size
const unsigned int	clib64_fp_cherip_buf_size

Function Documentation

add_cprover_library()

void add_cprover_library	(	contextt &	context,
		const languaget *	language )

assert_no_pruned_calls()

void assert_no_pruned_calls

(

const goto_functionst &

functions

)

Abort if any call in functions targets a symbol the prune erased.

collect_expr_deps()

void collect_expr_deps ( const irep_idt & from, const expr2tc & e, std::multimap< irep_idt, irep_idt > & deps )

static

Record every symbol e names, however deeply, as a dependency of from.

generate_symbol_deps()

void generate_symbol_deps ( irep_idt name, irept irep, std::multimap< irep_idt, irep_idt > & deps )

static

ingest_symbol()

void ingest_symbol ( irep_idt name, std::multimap< irep_idt, irep_idt > & deps, std::list< irep_idt > & to_include )

static

is_cbmc_memory_primitive()

bool is_cbmc_memory_primitive ( const symbolt & s )

static

program_references()

std::unordered_set< std::string > program_references ( const contextt & ctx )

static

Names the program's own symbols refer to, including through their types.

A function whose address is taken counts as referenced, since the reference appears in the value that takes it.

prune_unreferenced_library_functions()

void prune_unreferenced_library_functions	(	contextt &	context,
		const goto_functionst *	prelowered = nullptr )

Erase every library FUNCTION symbol not reachable from the program's own symbols, so goto_convert never lowers it.

Frontends whose converter resolves model calls by name (Python) cannot use the declaration-driven filter in add_cprover_library, because at load time the context holds no program yet: they link the models wholesale and call this once the converter has run. Only code symbols are erased – types stay, so the closed-world exception registry (exception_typeidt) is unchanged.

Pair it with assert_no_pruned_calls after goto_convert: a pass that runs between the two can introduce a reference this closure could not see, and that must fail loudly rather than leave a bodyless function returning nondet.

prelowered carries the bodies of a library shipped as GOTO (the Python model blob), whose symbols reach the context with nil values: without it the walk sees no edge out of a model function and erases everything it calls.

read_python_blob()

void read_python_blob ( bool is_python, contextt & new_ctx, contextt & ignored_ctx )

static

Merge the Python operational models into what was already read from clib.

py64 holds only the models, so it is read whole; the libc, libm and pthread symbols they call stay in clib and are reached through the dependency closure below. Hence the skip: a declaration the models' headers carry must not displace the clib definition of that name, which the closure has no way to add once the id is taken. No-op for every other language, as select_solidity_blob is.

record_library_symbol()

void record_library_symbol

(

const irep_idt &

id

)

Record that id came from a bundled operational-model library rather than from the program.

Loaders outside this file (the Python model blob) call it so prune_unreferenced_library_functions can tell the two apart by provenance instead of by guessing from the symbol name.

report_library_load()

void report_library_load ( const library_load_report & r )

static

store_library_symbol()

bool store_library_symbol ( const contextt & context, const symbolt & s, bool bundled_wholesale, const std::unordered_set< std::string > & referenced )

static

Whether a library symbol belongs in the context handed to the rest of the run.

bundled_wholesale frontends (Python, Solidity) filter upstream, so everything their blob carries is kept; for the rest a symbol is a library body the program declared and left empty, minus the memory primitives it never mentions.

Variable Documentation

clib32_buf

const uint8_t clib32_buf[]

extern

clib32_buf_size

const unsigned int clib32_buf_size

extern

clib32_cherih_buf

const uint8_t clib32_cherih_buf[]

extern

clib32_cherih_buf_size

const unsigned int clib32_cherih_buf_size

extern

clib32_cherip_buf

const uint8_t clib32_cherip_buf[]

extern

clib32_cherip_buf_size

const unsigned int clib32_cherip_buf_size

extern

clib32_fp_buf

const uint8_t clib32_fp_buf[]

extern

clib32_fp_buf_size

const unsigned int clib32_fp_buf_size

extern

clib32_fp_cherih_buf

const uint8_t clib32_fp_cherih_buf[]

extern

clib32_fp_cherih_buf_size

const unsigned int clib32_fp_cherih_buf_size

extern

clib32_fp_cherip_buf

const uint8_t clib32_fp_cherip_buf[]

extern

clib32_fp_cherip_buf_size

const unsigned int clib32_fp_cherip_buf_size

extern

clib64_buf

const uint8_t clib64_buf[]

extern

clib64_buf_size

const unsigned int clib64_buf_size

extern

clib64_cherih_buf

const uint8_t clib64_cherih_buf[]

extern

clib64_cherih_buf_size

const unsigned int clib64_cherih_buf_size

extern

clib64_cherip_buf

const uint8_t clib64_cherip_buf[]

extern

clib64_cherip_buf_size

const unsigned int clib64_cherip_buf_size

extern

clib64_fp_buf

const uint8_t clib64_fp_buf[]

extern

clib64_fp_buf_size

const unsigned int clib64_fp_buf_size

extern

clib64_fp_cherih_buf

const uint8_t clib64_fp_cherih_buf[]

extern

clib64_fp_cherih_buf_size

const unsigned int clib64_fp_cherih_buf_size

extern

clib64_fp_cherip_buf

const uint8_t clib64_fp_cherip_buf[]

extern

clib64_fp_cherip_buf_size

const unsigned int clib64_fp_cherip_buf_size

extern