witnesses.cpp File Reference

#include "irep2/irep2_expr.h"
#include <goto-symex/witness/witnesses.h>
#include <ac_config.h>
#include <boost/property_tree/ptree.hpp>
#include <fstream>
#include <langapi/languages.h>
#include <irep2/irep2.h>
#include <solvers/smt/smt_conv.h>
#include <util/base/picosha2.h>
#include <boost/date_time/posix_time/posix_time.hpp>
#include <boost/version.hpp>
#include <boost/uuid/uuid.hpp>
#include <boost/uuid/uuid_generators.hpp>
#include <boost/uuid/uuid_io.hpp>
#include <util/base/prefix.h>
#include <util/lang/c_types.h>
#include <boost/property_tree/detail/xml_parser_writer_settings.hpp>
#include <cassert>
#include <goto-symex/equation/slice.h>
#include <irep2/irep2_utils.h>

Include dependency graph for witnesses.cpp:

Typedefs
typedef boost::property_tree::ptree	xmlnodet

Functions
int	generate_sha256_hash_for_file (const char *path, std::string &output)
std::string	read_file (const std::string &path)
std::string	trim (const std::string &str)
void	create_waypoint (const waypoint &wp, YAML::Emitter &waypoint)
void	create_node_node (nodet &node, xmlnodet &nodenode)
	Create a node node.
void	create_edge_node (edget &edge, xmlnodet &edgenode)
	Create a edge node.
void	create_graphml (xmlnodet &graphml)
	Create a GraphML node, which is the most external one and includes graph, edges, and nodes.
void	_create_graph_node (std::string &verifiedfile, optionst &options, xmlnodet &graphnode)
void	_create_yaml_metadata_emitter (const std::string &verifiedfile, const optionst &options, YAML::Emitter &metadata)
void	create_violation_graph_node (std::string &verifiedfile, optionst &options, xmlnodet &graphnode)
	Create a violation graph node.
void	create_correctness_graph_node (std::string &verifiedfile, optionst &options, xmlnodet &graphnode)
	Create a correctness graph node.
void	create_correctness_yaml_emitter (std::string &verifiedfile, optionst &options, YAML::Emitter &root)
void	create_violation_yaml_emitter (std::string &verifiedfile, optionst &options, YAML::Emitter &root)
void	check_replace_invalid_assignment (std::string &assignment)
	Clear an assumption a witness validator would reject: one naming an ESBMC-internal object, or spelling anything but a C scalar expression.
std::string	get_formated_assignment (const namespacet &ns, const goto_trace_stept &step, bool yaml)
	If the current step is an assignment, this function will return the lhs and rhs formated in a way expected by the assumption field.
bool	is_valid_witness_step (const namespacet &ns, const goto_trace_stept &step)
	This function checks if the current counterexample step is valid for the GraphML.
bool	is_valid_witness_expr (const namespacet &ns, const irep_container< expr2t > &exp)
BigInt	get_line_number (const std::string &verified_file, BigInt relative_line_number, optionst &options)
std::string	read_line (std::string file, BigInt line_number)
static const std::regex	regex_invariants ("( " "+)?(__((VERIFIER|ESBMC))_)?(assume|assert)\\‍([a-zA-Z(-?(0-9))\\‍[\\‍]_>=+/" "*<~.&! \\‍(\\‍)]+\\‍);( +)?")
std::string	get_invariant (std::string verified_file, BigInt line_number, optionst &options)
void	generate_testcase_metadata ()
	This generates test-cases as described in: https://gitlab.com/sosy-lab/test-comp/test-format/-/tree/main/.
static bool	is_nondet_symbol_name (const std::string &name)
bool	find_nondet_in_expr (const expr2tc &expr)
	Returns true if any sub-expression of expr is a nondet symbol.
static expr2tc	zero_fill_aggregate (const type2tc &expected_type, const expr2tc &value, const expr2tc &root_expr, smt_convt &smt_conv)
std::vector< collected_nondet_value >	collect_nondet_values (const symex_target_equationt &target, smt_convt &smt_conv)
	Collect all nondet values from SSA.
expr2tc	make_blocking_expr (const std::vector< collected_nondet_value > &nondets)
	Build a blocking clause that excludes the given input tuple from future solver queries: NOT (sym_1 == val_1 AND sym_2 == val_2 AND ...).
void	generate_testcase (const std::string &file_name, const symex_target_equationt &target, smt_convt &smt_conv)

Typedef Documentation

xmlnodet

typedef boost::property_tree::ptree xmlnodet

Function Documentation

_create_graph_node()

void _create_graph_node	(	std::string &	verifiedfile,
		optionst &	options,
		xmlnodet &	graphnode )

_create_yaml_metadata_emitter()

void _create_yaml_metadata_emitter	(	const std::string &	verifiedfile,
		const optionst &	options,
		YAML::Emitter &	metadata )

check_replace_invalid_assignment()

void check_replace_invalid_assignment

(

std::string &

assignment

)

Clear an assumption a witness validator would reject: one naming an ESBMC-internal object, or spelling anything but a C scalar expression.

collect_nondet_values()

std::vector< collected_nondet_value > collect_nondet_values	(	const symex_target_equationt &	target,
		smt_convt &	smt_conv )

Collect all nondet values from SSA.

create_correctness_graph_node()

void create_correctness_graph_node	(	std::string &	verifiedfile,
		optionst &	options,
		xmlnodet &	graphnode )

Create a correctness graph node.

See create_violation_graph_node().

create_correctness_yaml_emitter()

void create_correctness_yaml_emitter	(	std::string &	verifiedfile,
		optionst &	options,
		YAML::Emitter &	root )

create_edge_node()

void create_edge_node	(	edget &	edge,
		xmlnodet &	edgenode )

Create a edge node.

This node contains information about lines, offsets, assumptions, invariants, and etc.

create_graphml()

void create_graphml

(

xmlnodet &

graphml

)

Create a GraphML node, which is the most external one and includes graph, edges, and nodes.

create_node_node()

void create_node_node	(	nodet &	node,
		xmlnodet &	nodenode )

Create a node node.

create_violation_graph_node()

void create_violation_graph_node	(	std::string &	verifiedfile,
		optionst &	options,
		xmlnodet &	graphnode )

Create a violation graph node.

This node contains all edges and vertexes of the GraphML requested by SVCOMP.

create_violation_yaml_emitter()

void create_violation_yaml_emitter	(	std::string &	verifiedfile,
		optionst &	options,
		YAML::Emitter &	root )

create_waypoint()

void create_waypoint	(	const waypoint &	wp,
		YAML::Emitter &	waypoint )

find_nondet_in_expr()

bool find_nondet_in_expr

(

const expr2tc &

expr

)

Returns true if any sub-expression of expr is a nondet symbol.

Handles compound expressions (arithmetic, bitwise, casts, etc.) by walking every operand via the generic get_sub_expr interface.

generate_sha256_hash_for_file()

int generate_sha256_hash_for_file	(	const char *	path,
		std::string &	output )

generate_testcase()

void generate_testcase	(	const std::string &	file_name,
		const symex_target_equationt &	target,
		smt_convt &	smt_conv )

generate_testcase_metadata()

void generate_testcase_metadata

(

)

This generates test-cases as described in: https://gitlab.com/sosy-lab/test-comp/test-format/-/tree/main/.

get_formated_assignment()

std::string get_formated_assignment	(	const namespacet &	ns,
		const goto_trace_stept &	step,
		bool	yaml )

If the current step is an assignment, this function will return the lhs and rhs formated in a way expected by the assumption field.

get_invariant()

std::string get_invariant	(	std::string	verified_file,
		BigInt	line_number,
		optionst &	options )

get_line_number()

BigInt get_line_number	(	const std::string &	verified_file,
		BigInt	relative_line_number,
		optionst &	options )

is_nondet_symbol_name()

bool is_nondet_symbol_name ( const std::string & name )

static

is_valid_witness_expr()

bool is_valid_witness_expr	(	const namespacet &	ns,
		const irep_container< expr2t > &	exp )

is_valid_witness_step()

bool is_valid_witness_step	(	const namespacet &	ns,
		const goto_trace_stept &	step )

This function checks if the current counterexample step is valid for the GraphML.

A priori, ESBMC only prints steps from the original program (i.e., internals and built-in are excluded).

make_blocking_expr()

expr2tc make_blocking_expr

(

const std::vector< collected_nondet_value > &

nondets

)

Build a blocking clause that excludes the given input tuple from future solver queries: NOT (sym_1 == val_1 AND sym_2 == val_2 AND ...).

Used by –all-witnesses to enumerate distinct input vectors that violate the same property without re-encoding the SMT instance: assert the returned expression on the active solver, then re-call dec_solve().

Returns a literal false expression when nondets is empty (forces UNSAT on re-solve so the caller's enumeration loop terminates cleanly).

read_file()

std::string read_file

(

const std::string &

path

)

read_line()

std::string read_line	(	std::string	file,
		BigInt	line_number )

regex_invariants()

const std::regex regex_invariants ( "( " "+)?(__((VERIFIER|ESBMC))_)?(assume|assert)\\‍([a-zA-Z(-?(0-9))\\‍[\\‍]_>=+/" "*<~.&! \\‍(\\‍)]+\\‍);( +)?" )

static

trim()

std::string trim

(

const std::string &

str

)

zero_fill_aggregate()

expr2tc zero_fill_aggregate ( const type2tc & expected_type, const expr2tc & value, const expr2tc & root_expr, smt_convt & smt_conv )

static