Validation of smt response parse trees to produce either a strongly typed smt_responset representation, or a set of error messages. More...

#include "smt_response_validation.h"
#include <util/arith_tools.h>
#include <util/mp_arith.h>
#include <util/range.h>
#include <solvers/smt2_incremental/theories/smt_array_theory.h>
#include "smt_to_smt2_string.h"
#include <regex>

Include dependency graph for smt_response_validation.cpp:

Go to the source code of this file.

Functions
static response_or_errort< smt_termt >	validate_term (const irept &parse_tree, const std::unordered_map< irep_idt, smt_identifier_termt > &identifier_table)

template<typename argumentt , typename... argumentst>
void	collect_error_messages_impl (std::vector< std::string > &collected_error_messages, argumentt &&argument)

template<typename argumentt , typename... argumentst>
void	collect_error_messages_impl (std::vector< std::string > &collected_error_messages, argumentt &&argument, argumentst &&... arguments)

template<typename... argumentst>
std::vector< std::string >	collect_error_messages (argumentst &&... arguments)
	Builds a collection of error messages composed all error messages in the `response_or_errort` typed arguments in `arguments`. More...

template<typename smt_to_constructt , typename smt_baset = smt_to_constructt, typename... argumentst>
response_or_errort< smt_baset >	validation_propagating (argumentst &&... arguments)
	Given a class to construct and a set of arguments to its constructor which may include errors, either return the collected errors if there are any or construct the class otherwise. More...

static std::string	print_parse_tree (const irept &parse_tree)
	Produces a human-readable representation of the given `parse_tree`, for use in error messaging. More...

static response_or_errort< irep_idt >	validate_string_literal (const irept &parse_tree)

static std::optional< response_or_errort< smt_responset > >	valid_smt_error_response (const irept &parse_tree)

static bool	all_subs_are_pairs (const irept &parse_tree)

static std::optional< smt_termt >	valid_smt_indexed_bit_vector (const irept &parse_tree)
	Checks for valid bit vector constants of the form `(_ bv(value) (width))` for example - `(_ bv4 64)`. More...

static std::optional< smt_termt >	valid_smt_bool (const irept &parse_tree)

static std::optional< smt_termt >	valid_smt_binary (const std::string &text)

static std::optional< smt_termt >	valid_smt_hex (const std::string &text)

static std::optional< smt_termt >	valid_smt_bit_vector_constant (const irept &parse_tree)

static std::optional< response_or_errort< smt_termt > >	try_select_validation (const irept &parse_tree, const std::unordered_map< irep_idt, smt_identifier_termt > &identifier_table)

static response_or_errort< smt_get_value_responset::valuation_pairt >	validate_valuation_pair (const irept &pair_parse_tree, const std::unordered_map< irep_idt, smt_identifier_termt > &identifier_table)

static std::optional< response_or_errort< smt_responset > >	valid_smt_get_value_response (const irept &parse_tree, const std::unordered_map< irep_idt, smt_identifier_termt > &identifier_table)

response_or_errort< smt_responset >	validate_smt_response (const irept &parse_tree, const std::unordered_map< irep_idt, smt_identifier_termt > &identifier_table)

Detailed Description

Validation of smt response parse trees to produce either a strongly typed smt_responset representation, or a set of error messages.

Note

Functions named with the prefix validate_ require the given parse tree to be a particular kind of sub tree. Functions named with the prefix valid_ are called in places where the exact kind of sub-tree expected is unknown and so the function must determine if the sub-tree is of that type at all, before performing validation of it. These functions will return a response_or_errort in the case where the parse tree is of that type or an empty optional otherwise.

Definition in file smt_response_validation.cpp.

Function Documentation

◆ all_subs_are_pairs()

static bool all_subs_are_pairs ( const irept & parse_tree )

static

Definition at line 155 of file smt_response_validation.cpp.

◆ collect_error_messages()

template<typename... argumentst>

std::vector<std::string> collect_error_messages ( argumentst &&... arguments )

Builds a collection of error messages composed all error messages in the response_or_errort typed arguments in arguments.

This is a templated function in order to handle response_or_errort instances which are specialised differently.

Definition at line 63 of file smt_response_validation.cpp.

◆ collect_error_messages_impl() [1/2]

template<typename argumentt , typename... argumentst>

void collect_error_messages_impl	(	std::vector< std::string > &	collected_error_messages,
		argumentt &&	argument
	)

Definition at line 36 of file smt_response_validation.cpp.

◆ collect_error_messages_impl() [2/2]

template<typename argumentt , typename... argumentst>

void collect_error_messages_impl	(	std::vector< std::string > &	collected_error_messages,
		argumentt &&	argument,
		argumentst &&...	arguments
	)

Definition at line 49 of file smt_response_validation.cpp.

◆ print_parse_tree()

static std::string print_parse_tree ( const irept & parse_tree )

static

Produces a human-readable representation of the given parse_tree, for use in error messaging.

Note: This is currently implemented using pretty, but this function is used instead of calling pretty directly so that will be more straight forward to replace with an implementation specific to our use case which is more easily readable by users of CBMC.

Definition at line 106 of file smt_response_validation.cpp.

◆ try_select_validation()

static std::optional<response_or_errort<smt_termt> > try_select_validation	(	const irept &	parse_tree,
		const std::unordered_map< irep_idt, smt_identifier_termt > &	identifier_table
	)

static

Definition at line 243 of file smt_response_validation.cpp.

◆ valid_smt_binary()

static std::optional<smt_termt> valid_smt_binary ( const std::string & text )

static

Definition at line 203 of file smt_response_validation.cpp.

◆ valid_smt_bit_vector_constant()

static std::optional<smt_termt> valid_smt_bit_vector_constant ( const irept & parse_tree )

static

Definition at line 229 of file smt_response_validation.cpp.

◆ valid_smt_bool()

static std::optional<smt_termt> valid_smt_bool ( const irept & parse_tree )

static

Definition at line 192 of file smt_response_validation.cpp.

◆ valid_smt_error_response()

static std::optional<response_or_errort<smt_responset> > valid_smt_error_response ( const irept & parse_tree )

static

Returns: : A response or error in the case where the parse tree appears to be a get-value command. Returns empty otherwise.

Note: : Because this kind of response does not start with an identifying keyword, it will be considered that the response is intended to be a get-value response if it is composed of a collection of one or more pairs.

Definition at line 129 of file smt_response_validation.cpp.

◆ valid_smt_get_value_response()

static std::optional<response_or_errort<smt_responset> > valid_smt_get_value_response	(	const irept &	parse_tree,
		const std::unordered_map< irep_idt, smt_identifier_termt > &	identifier_table
	)

static

Returns: : A response or error in the case where the parse tree appears to be a get-value command. Returns empty otherwise.

Note: : Because this kind of response does not start with an identifying keyword, it will be considered that the response is intended to be a get-value response if it is composed of a collection of one or more pairs.

Definition at line 325 of file smt_response_validation.cpp.

◆ valid_smt_hex()

static std::optional<smt_termt> valid_smt_hex ( const std::string & text )

static

Definition at line 214 of file smt_response_validation.cpp.

◆ valid_smt_indexed_bit_vector()

static std::optional<smt_termt> valid_smt_indexed_bit_vector ( const irept & parse_tree )

static

Checks for valid bit vector constants of the form (_ bv(value) (width)) for example - (_ bv4 64).

Definition at line 166 of file smt_response_validation.cpp.

◆ validate_smt_response()

response_or_errort<smt_responset> validate_smt_response	(	const irept &	parse_tree,
		const std::unordered_map< irep_idt, smt_identifier_termt > &	identifier_table
	)

Definition at line 356 of file smt_response_validation.cpp.

◆ validate_string_literal()

static response_or_errort<irep_idt> validate_string_literal ( const irept & parse_tree )

static

Definition at line 112 of file smt_response_validation.cpp.

◆ validate_term()

static response_or_errort< smt_termt > validate_term	(	const irept &	parse_tree,
		const std::unordered_map< irep_idt, smt_identifier_termt > &	identifier_table
	)

static

Definition at line 267 of file smt_response_validation.cpp.

◆ validate_valuation_pair()

static response_or_errort<smt_get_value_responset::valuation_pairt> validate_valuation_pair	(	const irept &	pair_parse_tree,
		const std::unordered_map< irep_idt, smt_identifier_termt > &	identifier_table
	)

static

Definition at line 289 of file smt_response_validation.cpp.

◆ validation_propagating()

template<typename smt_to_constructt , typename smt_baset = smt_to_constructt, typename... argumentst>

response_or_errort<smt_baset> validation_propagating ( argumentst &&... arguments )

Given a class to construct and a set of arguments to its constructor which may include errors, either return the collected errors if there are any or construct the class otherwise.

Template Parameters

smt_to_constructt	The class to construct.
smt_baset	If the class to construct should be upcast to a base class before being stored in the `response_or_errort`, then the base class should be supplied in this parameter. If no upcast is required, then this should be left empty.
argumentst	The pack of argument types matching the constructor of `smt_to_constructt`. These must each be packed into an instance of `response_or_errort`.

Definition at line 88 of file smt_response_validation.cpp.