witnesses.h File Reference

#include <boost/property_tree/xml_parser.hpp>
#include <util/symtab/namespace.h>
#include <irep2/irep2.h>
#include <langapi/language_util.h>
#include <goto-symex/trace/goto_trace.h>
#include <goto-symex/equation/symex_target_equation.h>
#include <goto-symex/waypoint.h>
#include <string>
#include <regex>
#include <vector>
#include <big-int/bigint.hh>
#include <yaml-cpp/yaml.h>

Include dependency graph for witnesses.h:

This graph shows which files directly or indirectly include this file:

Go to the source code of this file.

Classes
class	nodet
class	edget
class	invariant
class	grapht
class	yamlt
struct	collected_nondet_value
	Helper structure for collected nondet values. More...

Functions
void	create_graphml (xmlnodet &graphml)
	Create a GraphML node, which is the most external one and includes graph, edges, and nodes.
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	create_waypoint (const waypoint &wp, YAML::Emitter &waypoint)
void	create_edge_node (edget &edge, xmlnodet &edgenode)
	Create a edge node.
void	create_node_node (nodet &node, xmlnodet &nodenode)
	Create a node node.
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.
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.
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.
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)
int	generate_sha256_hash_for_file (const char *path, std::string &output)
std::string	get_invariant (std::string verified_file, BigInt line_number, optionst &options)
bool	find_nondet_in_expr (const expr2tc &expr)
	Returns true if any sub-expression of expr is a nondet symbol.
void	generate_testcase_metadata ()
	This generates test-cases as described in: https://gitlab.com/sosy-lab/test-comp/test-format/-/tree/main/.
void	generate_testcase (const std::string &file_name, const symex_target_equationt &target, 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 ...).

Function Documentation

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_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).