Generates string constraints for the Java format function. More...

#include <iomanip>
#include <string>
#include <regex>
#include <vector>
#include <util/std_expr.h>
#include <util/unicode.h>
#include "string_builtin_function.h"
#include "string_constraint_generator.h"

Include dependency graph for string_constraint_generator_format.cpp:

Go to the source code of this file.

Classes
class	format_specifiert

class	format_textt

class	format_elementt

Functions
static format_specifiert	format_specifier_of_match (std::smatch &m)
	Helper function for parsing format strings. More...

static std::vector< format_elementt >	parse_format_string (std::string s)
	Parse the given string into format specifiers and text. More...

static exprt	get_component_in_struct (const struct_exprt &expr, irep_idt component_name)
	Helper for add_axioms_for_format_specifier. More...

static std::pair< array_string_exprt, string_constraintst >	add_axioms_for_format_specifier (symbol_generatort &fresh_symbol, const format_specifiert &fs, const struct_exprt &arg, const typet &index_type, const typet &char_type, array_poolt &array_pool, const messaget &message, const namespacet &ns)
	Parse `s` and add axioms ensuring the output corresponds to the output of String.format. More...

std::pair< exprt, string_constraintst >	add_axioms_for_format (symbol_generatort &fresh_symbol, const array_string_exprt &res, const std::string &s, const exprt::operandst &args, array_poolt &array_pool, const messaget &message, const namespacet &ns)
	Parse `s` and add axioms ensuring the output corresponds to the output of String.format. More...

std::string	utf16_constant_array_to_java (const array_exprt &arr, std::size_t length)
	Construct a string from a constant array. More...

std::pair< exprt, string_constraintst >	add_axioms_for_format (symbol_generatort &fresh_symbol, const function_application_exprt &f, array_poolt &array_pool, const messaget &message, const namespacet &ns)
	Formatted string using a format string and list of arguments. More...

Detailed Description

Generates string constraints for the Java format function.

Definition in file string_constraint_generator_format.cpp.

Function Documentation

◆ add_axioms_for_format() [1/2]

std::pair<exprt, string_constraintst> add_axioms_for_format	(	symbol_generatort &	fresh_symbol,
		const array_string_exprt &	res,
		const std::string &	s,
		const exprt::operandst &	args,
		array_poolt &	array_pool,
		const messaget &	message,
		const namespacet &	ns
	)

Parse s and add axioms ensuring the output corresponds to the output of String.format.

Parameters

fresh_symbol	generator of fresh symbols
res	string expression for the result of the format function
s	a format string
args	a vector of arguments
array_pool	pool of arrays representing strings
message	message handler for warnings
ns	namespace

Returns: code, 0 on success

Definition at line 381 of file string_constraint_generator_format.cpp.

◆ add_axioms_for_format() [2/2]

std::pair<exprt, string_constraintst> add_axioms_for_format	(	symbol_generatort &	fresh_symbol,
		const function_application_exprt &	f,
		array_poolt &	array_pool,
		const messaget &	message,
		const namespacet &	ns
	)

Formatted string using a format string and list of arguments.

Add axioms to specify the Java String.format function.

Parameters

fresh_symbol	generator of fresh symbols
f	a function application
array_pool	pool of arrays representing strings
message	message handler for warnings
ns	namespace

Returns: A string expression representing the return value of the String.format function on the given arguments, assuming the first argument in the function application is a constant. Otherwise the first argument is returned.

Definition at line 510 of file string_constraint_generator_format.cpp.

◆ add_axioms_for_format_specifier()

static std::pair<array_string_exprt, string_constraintst> add_axioms_for_format_specifier	(	symbol_generatort &	fresh_symbol,
		const format_specifiert &	fs,
		const struct_exprt &	arg,
		const typet &	index_type,
		const typet &	char_type,
		array_poolt &	array_pool,
		const messaget &	message,
		const namespacet &	ns
	)

static

Parse s and add axioms ensuring the output corresponds to the output of String.format.

Assumes the argument is a structured expression which contains the fields: string expr, int, float, char, boolean, hashcode, date_time. The correct component will be fetched depending on the format specifier.

Parameters

fresh_symbol	generator of fresh symbols
fs	a format specifier
arg	a struct containing the possible value of the argument to format
index_type	type for indexes in strings
char_type	type of characters
array_pool	pool of arrays representing strings
message	message handler for warnings
ns	namespace

Returns: String expression representing the output of String.format.

Definition at line 260 of file string_constraint_generator_format.cpp.

◆ format_specifier_of_match()

static format_specifiert format_specifier_of_match ( std::smatch & m )

static

Helper function for parsing format strings.

This follows the implementation in openJDK of the java.util.Formatter class: http://hg.openjdk.java.net/jdk7/jdk7/jdk/file/9b8c96f96a0f/src/share/classes/java/util/Formatter.java#l2660

Parameters

m	a match in a regular expression

Returns: Format specifier represented by the matched string. The groups in the match should represent: index, flag, width, precision, date and conversion type.

Definition at line 185 of file string_constraint_generator_format.cpp.

◆ get_component_in_struct()

static exprt get_component_in_struct	(	const struct_exprt &	expr,
		irep_idt	component_name
	)

static

Helper for add_axioms_for_format_specifier.

Parameters

expr	a structured expression
component_name	name of the desired component

Returns: Expression in the component of expr named component_name.

Definition at line 237 of file string_constraint_generator_format.cpp.

◆ parse_format_string()

static std::vector<format_elementt> parse_format_string ( std::string s )

static

Parse the given string into format specifiers and text.

This follows the implementation in openJDK of the java.util.Formatter class: http://hg.openjdk.java.net/jdk7/jdk7/jdk/file/9b8c96f96a0f/src/share/classes/java/util/Formatter.java#l2513

Parameters

s a string

Returns: A vector of format_elementt.

Definition at line 209 of file string_constraint_generator_format.cpp.

◆ utf16_constant_array_to_java()

std::string utf16_constant_array_to_java	(	const array_exprt &	arr,
		std::size_t	length
	)

Construct a string from a constant array.

Parameters

arr	an array expression containing only constants
length	an unsigned value representing the length of the array

Returns: String of length length represented by the array assuming each field in arr represents a character.

Definition at line 483 of file string_constraint_generator_format.cpp.

Classes

Functions

Detailed Description

Function Documentation

◆ add_axioms_for_format() [1/2]

◆ add_axioms_for_format() [2/2]

◆ add_axioms_for_format_specifier()

◆ format_specifier_of_match()

◆ get_component_in_struct()

◆ parse_format_string()

◆ utf16_constant_array_to_java()