Handles all string-related operations for Python-to-C conversion. More...

#include <string_handler.h>

Public Member Functions
	string_handler (python_converter &converter, contextt &symbol_table, type_handler &type_handler, string_builder *str_builder)
	Constructs a string_handler.
void	set_string_builder (string_builder *sb)
BigInt	get_string_size (const exprt &expr)
	Calculate the size of a string expression.
exprt	convert_to_string (const exprt &expr)
	Convert an expression to a string representation.
exprt	build_fstring_conversion (const nlohmann::json &value, int conversion, const exprt &operand, const locationt &location)
	The rendered part for an f-string replacement field carrying a !r / !a conversion: the folded repr where possible, else a sound nondet string.
exprt	build_repr (const exprt &value, const locationt &location)
	repr() of a runtime value, or nil when its type has no model: a number or bool renders as str() does, a str through __python_str_repr.
exprt	format_fstring_part (const nlohmann::json &value)
	The rendered text of one f-string replacement field.
exprt	build_nondet_string_fallback (const locationt &location)
exprt	build_nondet_string (const locationt &location)
	A bounded, NUL-terminated str of nondet content, as nondet_str() gives.
std::string	extract_string_from_array_operands (const exprt &array_expr) const
	Extract string content from array operands.
void	ensure_string_array (exprt &expr)
	Ensure an expression is a null-terminated string array.
exprt	ensure_null_terminated_string (exprt &e)
	Ensure string is null-terminated.
std::string	process_format_spec (const nlohmann::json &format_spec)
	Process format specification for f-strings.
exprt	apply_format_specification (const exprt &expr, const std::string &format)
	Apply format specification to an expression.
exprt	format_runtime_value (const exprt &expr, const std::string &format)
	A spec on a value not folded at conversion time: a fixed-point float through its model, anything else as a nondet string.
exprt	get_fstring_expr (const nlohmann::json &element)
	Convert f-string JSON to expression.
exprt	handle_string_concatenation (const exprt &lhs, const exprt &rhs, const nlohmann::json &left, const nlohmann::json &right)
	Handle string concatenation.
exprt	handle_string_concatenation_with_promotion (exprt &lhs, exprt &rhs, const nlohmann::json &left, const nlohmann::json &right)
	Handle string concatenation with type promotion.
exprt	handle_string_comparison (const std::string &op, exprt &lhs, exprt &rhs, const nlohmann::json &element)
	Handle string comparison operations.
exprt	handle_single_char_comparison (const std::string &op, exprt &lhs, exprt &rhs)
	Handle single character comparisons.
exprt	create_char_comparison_expr (const std::string &op, const exprt &lhs_char_value, const exprt &rhs_char_value, const exprt &lhs_source, const exprt &rhs_source) const
	Create a character comparison expression.
exprt	handle_string_repetition (exprt &lhs, exprt &rhs)
	Handle string repetition.
exprt	handle_string_operations (const std::string &op, exprt &lhs, exprt &rhs, const nlohmann::json &left, const nlohmann::json &right, const nlohmann::json &element)
	Handle general string operations.
exprt	handle_str_join (const nlohmann::json &call_json)
	Handle str.join() method.
exprt	join_unfoldable_iterable (const exprt &separator, const nlohmann::json &call_json)
exprt	convert_join_items (const nlohmann::json &elements, std::vector< exprt > &elem_exprs)
	Convert a join() literal's elements into elem_exprs.
exprt	handle_string_attribute_call (const nlohmann::json &call_json)
	Dispatch and handle string attribute method calls.
exprt	read_tagged_str_receiver (const exprt &receiver, const std::string &method, const nlohmann::json &call_json)
	The str a tagged receiver of str-only method method holds, after raising AttributeError on the paths where it holds another type.
exprt	try_handle_len_string_fast_path (const nlohmann::json &call_json, const exprt &arg_expr)
	Try fast-path folding for len() when argument is string-like.
exprt	char_array_type_length (const exprt &arg_expr) const
exprt	handle_string_startswith (const exprt &string_obj, const exprt &prefix_arg, const locationt &location)
	Handle str.startswith() method.
exprt	handle_string_endswith (const exprt &string_obj, const exprt &suffix_arg, const locationt &location)
	Handle str.endswith() method.
exprt	handle_startswith_endswith_with_pos (const exprt &string_obj, const nlohmann::json &args, python_converter &converter, const locationt &location, bool is_suffix)
	Handle str.startswith/endswith with optional start/end position arguments: s.startswith(prefix, start[, end]) is evaluated as s[start:end].startswith(prefix).
exprt	build_affix_tuple_match (const exprt &string_obj, const exprt &affix_tuple, const locationt &location, bool is_suffix)
	Shared implementation for startswith()/endswith() with a tuple of affixes: True iff the string matches any element.
exprt	handle_string_isdigit (const exprt &string_obj, const locationt &location)
	Handle str.isdigit() method.
exprt	handle_string_isalpha (const exprt &string_obj, const locationt &location)
	Handle str.isalpha() method.
exprt	handle_string_isspace (const exprt &str_expr, const locationt &location)
	Handle str.isspace() method for strings.
exprt	handle_char_isspace (const exprt &char_expr, const locationt &location)
	Handle char.isspace() method for single characters.
exprt	handle_string_lstrip (const exprt &str_expr, const exprt &chars_arg, const locationt &location)
	Handle str.lstrip() method.
exprt	handle_string_strip (const exprt &str_expr, const exprt &chars_arg, const locationt &location)
	Handle str.strip() method.
exprt	handle_string_rstrip (const exprt &str_expr, const exprt &chars_arg, const locationt &location)
	Handle str.rstrip() method.
exprt	handle_string_membership (exprt &lhs, exprt &rhs, const nlohmann::json &element)
	Handle 'in' operator for strings.
exprt	handle_string_islower (const exprt &string_obj, const locationt &location)
	Handle Python's str.islower() method.
exprt	handle_string_lower (const exprt &string_obj, const locationt &location)
	Handle str.lower() method.
exprt	handle_string_upper (const exprt &string_obj, const locationt &location)
	Handle str.upper() method.
exprt	handle_string_find (const exprt &string_obj, const exprt &find_arg, const locationt &location)
	Handle str.find() method.
exprt	handle_string_find_range (const exprt &string_obj, const exprt &find_arg, const exprt &start_arg, const exprt &end_arg, const locationt &location)
	Handle str.find() with start/end.
exprt	handle_string_index (const nlohmann::json &call, const exprt &string_obj, const exprt &find_arg, const locationt &location)
	Handle str.index() method.
exprt	handle_string_index_range (const nlohmann::json &call, const exprt &string_obj, const exprt &find_arg, const exprt &start_arg, const exprt &end_arg, const locationt &location)
	Handle str.index() with start/end.
exprt	handle_string_rfind (const exprt &string_obj, const exprt &find_arg, const locationt &location)
	Handle str.rfind() method.
exprt	handle_string_rfind_range (const exprt &string_obj, const exprt &find_arg, const exprt &start_arg, const exprt &end_arg, const locationt &location)
	Handle str.rfind() with start/end.
exprt	handle_string_rindex (const nlohmann::json &call, const exprt &string_obj, const exprt &find_arg, const locationt &location)
	Handle str.rindex() method (rfind that raises on not-found).
exprt	handle_string_rindex_range (const nlohmann::json &call, const exprt &string_obj, const exprt &find_arg, const exprt &start_arg, const exprt &end_arg, const locationt &location)
	Handle str.rindex() with start/end.
exprt	handle_string_replace (const exprt &string_obj, const exprt &old_arg, const exprt &new_arg, const exprt &count_arg, const locationt &location)
	Handle str.replace() method.
exprt	handle_string_capitalize (const exprt &string_obj, const locationt &location)
	Handle str.capitalize() method.
exprt	handle_string_title (const exprt &string_obj, const locationt &location)
	Handle str.title() method.
exprt	handle_string_swapcase (const exprt &string_obj, const locationt &location)
	Handle str.swapcase() method.
exprt	handle_string_casefold (const exprt &string_obj, const locationt &location)
	Handle str.casefold() method.
exprt	handle_string_count (const exprt &string_obj, const exprt &sub_arg, const exprt &start_arg, const exprt &end_arg, const locationt &location)
	Handle str.count() method (constant fold, else runtime model).
exprt	handle_string_removeprefix (const exprt &string_obj, const exprt &prefix_arg, const locationt &location)
	Handle str.removeprefix() method.
exprt	handle_string_removesuffix (const exprt &string_obj, const exprt &suffix_arg, const locationt &location)
	Handle str.removesuffix() method.
exprt	handle_string_splitlines (const nlohmann::json &call, const exprt &string_obj, const locationt &location, bool keepends=false)
	Handle str.splitlines() method (constant-only support).
exprt	handle_string_format (const nlohmann::json &call, const exprt &string_obj, const locationt &location)
	Handle str.format() method (minimal support, constant-only).
exprt	handle_string_partition (const exprt &string_obj, const exprt &sep_arg, const locationt &location)
	Handle str.partition() method (constant-only support).
exprt	handle_string_rpartition (const exprt &string_obj, const exprt &sep_arg, const locationt &location)
	Handle str.rpartition() method (constant-only support).
exprt	build_partition_tuple (const exprt &string_obj, const exprt &sep_arg, const locationt &location, bool from_right)
	Shared implementation of partition()/rpartition(): builds the 3-tuple (before, sep, after), searching from the left when `from_right` is false and from the right when true.
exprt	handle_string_isalnum (const exprt &string_obj, const locationt &location)
	Handle str.isalnum() method.
exprt	handle_string_isupper (const exprt &string_obj, const locationt &location)
	Handle str.isupper() method.
exprt	handle_string_isnumeric (const exprt &string_obj, const locationt &location)
	Handle str.isnumeric() method.
exprt	handle_string_isidentifier (const exprt &string_obj, const locationt &location)
	Handle str.isidentifier() method.
exprt	handle_string_center (const exprt &string_obj, const exprt &width_arg, const exprt &fill_arg, const locationt &location)
	Handle str.center() method (constant-only support).
exprt	handle_string_ljust (const exprt &string_obj, const exprt &width_arg, const exprt &fill_arg, const locationt &location)
	Handle str.ljust() method (constant-only support).
exprt	handle_string_rjust (const exprt &string_obj, const exprt &width_arg, const exprt &fill_arg, const locationt &location)
	Handle str.rjust() method (constant-only support).
exprt	handle_string_zfill (const exprt &string_obj, const exprt &width_arg, const locationt &location)
	Handle str.zfill() method (constant-only support).
exprt	handle_string_expandtabs (const exprt &string_obj, const exprt &tabsize_arg, const locationt &location)
	Handle str.expandtabs() method (constant-only support).
exprt	handle_string_format_map (const nlohmann::json &call, const exprt &string_obj, const locationt &location)
	Handle str.format_map() method (minimal support, constant-only).
bool	is_zero_length_array (const exprt &expr)
	Check if an expression is a zero-length array.
exprt	get_array_base_address (const exprt &arr)
	Get base address of array (first element).
exprt	handle_string_to_int (const exprt &string_obj, const exprt &base_arg, const locationt &location)
	Convert a string to an integer using Python's int() function.
exprt	handle_string_to_int_base10 (const exprt &string_obj, const locationt &location)
	Convert a string to an integer using base 10 (convenience method).
exprt	handle_int_conversion (const exprt &arg, const locationt &location)
	Handle int() builtin with automatic type detection Supports int(x) where x can be: int, float, bool, or string.
exprt	handle_int_conversion_with_base (const exprt &arg, const exprt &base, const locationt &location)
	Handle int() builtin with explicit base Supports int(x, base) where x is a string.
exprt	handle_string_to_float (const exprt &string_obj, const locationt &location)
	Convert a runtime string expression to a double via the __python_str_to_float operational model.
exprt	handle_string_is_float (const exprt &string_obj, const locationt &location)
	Build a call to the __python_str_is_float operational model, returning a bool that is true iff the runtime string is a valid Python float literal.
exprt	handle_chr_conversion (const exprt &codepoint_arg, const locationt &location)
	Handle chr() builtin function Converts a Unicode code point to its string representation Supports chr(i) where i is an integer in range [0, 0x10FFFF].
exprt	handle_ord_conversion (const exprt &string_obj, const locationt &location)
	Handle ord() of a runtime string whose value is not known at compile time.

Static Public Member Functions
static std::string	fstring_repr_of_constant (const nlohmann::json &operand)
	Build a sound symbolic fallback for a char * string value when a string handler cannot compile-time-fold its argument.
static int	nondet_str_buffer_size ()
	The nondet str buffer size: –nondet-str-length plus the NUL.
static bool	extract_constant_string (const nlohmann::json &node, python_converter &converter, std::string &out)
	Extract a constant string from the AST node (literal or const var).
static std::string	cpython_float_str (double d)
	Render a constant double as CPython's str()/repr() would: the shortest decimal string that reads back as the same double.

Detailed Description

Handles all string-related operations for Python-to-C conversion.

This class extracts string manipulation functionality from python_converter to improve modularity and maintainability. It handles:

String size calculations
String-to-expression conversions
String formatting and f-string processing
String comparison operations
String method operations (startswith, endswith, isdigit, isalpha, etc.)
String concatenation and membership testing
String joining operations (str.join)
Character-level comparisons

Constructor & Destructor Documentation

◆ string_handler()

string_handler::string_handler	(	python_converter &	converter,
		contextt &	symbol_table,
		type_handler &	type_handler,
		string_builder *	str_builder )

Constructs a string_handler.

Parameters

converter	Reference to the parent python_converter
symbol_table	Reference to the symbol table (contextt)
type_handler	Reference to the type handler
str_builder	Pointer to the string builder

Member Function Documentation

◆ apply_format_specification()

exprt string_handler::apply_format_specification	(	const exprt &	expr,
		const std::string &	format )

Apply format specification to an expression.

Parameters

expr	Expression to format
format	Format string

Returns: Formatted expression

◆ build_affix_tuple_match()

exprt string_handler::build_affix_tuple_match	(	const exprt &	string_obj,
		const exprt &	affix_tuple,
		const locationt &	location,
		bool	is_suffix )

Shared implementation for startswith()/endswith() with a tuple of affixes: True iff the string matches any element.

is_suffix selects endswith (true) vs startswith (false).

◆ build_fstring_conversion()

exprt string_handler::build_fstring_conversion	(	const nlohmann::json &	value,
		int	conversion,
		const exprt &	operand,
		const locationt &	location )

The rendered part for an f-string replacement field carrying a !r / !a conversion: the folded repr where possible, else a sound nondet string.

◆ build_nondet_string()

exprt string_handler::build_nondet_string ( const locationt & location )

A bounded, NUL-terminated str of nondet content, as nondet_str() gives.

◆ build_nondet_string_fallback()

exprt string_handler::build_nondet_string_fallback ( const locationt & location )

◆ build_partition_tuple()

exprt string_handler::build_partition_tuple	(	const exprt &	string_obj,
		const exprt &	sep_arg,
		const locationt &	location,
		bool	from_right )

Shared implementation of partition()/rpartition(): builds the 3-tuple (before, sep, after), searching from the left when from_right is false and from the right when true.

◆ build_repr()

exprt string_handler::build_repr	(	const exprt &	value,
		const locationt &	location )

repr() of a runtime value, or nil when its type has no model: a number or bool renders as str() does, a str through __python_str_repr.

For an ASCII value this is also ascii().

◆ char_array_type_length()

exprt string_handler::char_array_type_length ( const exprt & arg_expr ) const

◆ convert_join_items()

exprt string_handler::convert_join_items	(	const nlohmann::json &	elements,
		std::vector< exprt > &	elem_exprs )

Convert a join() literal's elements into elem_exprs.

Returns a TypeError raise for an element that is known not to be a str, nil otherwise.

◆ convert_to_string()

exprt string_handler::convert_to_string ( const exprt & expr )

Convert an expression to a string representation.

Parameters

expr	Expression to convert

Returns: String array expression

◆ cpython_float_str()

std::string string_handler::cpython_float_str ( double d )

static

Render a constant double as CPython's str()/repr() would: the shortest decimal string that reads back as the same double.

A whole value below 1e16 gets the "N.0" spelling; every other finite value (and nan/inf) uses the fewest g significant digits that round-trip, which reproduces CPython's shortest repr and its fixed/exponential cut-over. This is total: it renders every double, so str()/repr() and f-string interpolation fold to the exact CPython string for inexact values too (str(0.1 + 0.2) == "0.30000000000000004", str(1e-5) == "1e-05"). The caller still emits a nondet string for a 32-bit float or a nondet value.

◆ create_char_comparison_expr()

exprt string_handler::create_char_comparison_expr	(	const std::string &	op,
		const exprt &	lhs_char_value,
		const exprt &	rhs_char_value,
		const exprt &	lhs_source,
		const exprt &	rhs_source ) const

Create a character comparison expression.

Parameters

op	Comparison operator
lhs_char_value	Left character value (as integer)
rhs_char_value	Right character value (as integer)
lhs_source	Original left source expression
rhs_source	Original right source expression

Returns: Comparison expression with proper location info

◆ ensure_null_terminated_string()

exprt string_handler::ensure_null_terminated_string ( exprt & e )

Ensure string is null-terminated.

Parameters

e	String expression

Returns: Null-terminated string expression

◆ ensure_string_array()

void string_handler::ensure_string_array ( exprt & expr )

Ensure an expression is a null-terminated string array.

Parameters

expr	Expression to convert

◆ extract_constant_string()

bool string_handler::extract_constant_string	(	const nlohmann::json &	node,
		python_converter &	converter,
		std::string &	out )

static

Extract a constant string from the AST node (literal or const var).

Parameters

node	JSON node to inspect
converter	Converter used to resolve Name references
out	Output string

Returns: True if a constant string was resolved

◆ extract_string_from_array_operands()

std::string string_handler::extract_string_from_array_operands ( const exprt & array_expr ) const

Extract string content from array operands.

Parameters

array_expr Array expression containing characters

Returns: Extracted string

◆ format_fstring_part()

exprt string_handler::format_fstring_part ( const nlohmann::json & value )

The rendered text of one f-string replacement field.

◆ format_runtime_value()

exprt string_handler::format_runtime_value	(	const exprt &	expr,
		const std::string &	format )

A spec on a value not folded at conversion time: a fixed-point float through its model, anything else as a nondet string.

◆ fstring_repr_of_constant()

std::string string_handler::fstring_repr_of_constant ( const nlohmann::json & operand )

static

Build a sound symbolic fallback for a char * string value when a string handler cannot compile-time-fold its argument.

Replaces the historical throw "X() requires constant string" aborts so that GOTO conversion can proceed. Returns a side_effect_expr_nondett of pointer-to-char type; subsequent string ops see arbitrary content, which is sound over-approximation for safety properties (we cannot conclude a specific functional result, but we cannot wrongly conclude SAFE either). repr() of a constant f-string operand under !r / !a, or empty when the spelling is one this does not fold. Only an int's digits and a string needing no escape are folded: reproducing CPython's quote choice and escaping here would be easy to get subtly wrong (#7559).

◆ get_array_base_address()

exprt string_handler::get_array_base_address ( const exprt & arr )

Get base address of array (first element).

Parameters

arr	Array expression

Returns: Address expression

◆ get_fstring_expr()

exprt string_handler::get_fstring_expr ( const nlohmann::json & element )

Convert f-string JSON to expression.

Parameters

element JSON element representing f-string

Returns: Concatenated f-string expression

◆ get_string_size()

BigInt string_handler::get_string_size ( const exprt & expr )

Calculate the size of a string expression.

Parameters

expr	Expression to measure

Returns: Size of string including null terminator

◆ handle_char_isspace()

exprt string_handler::handle_char_isspace	(	const exprt &	char_expr,
		const locationt &	location )

Handle char.isspace() method for single characters.

Parameters

char_expr	Character expression
location	Source location

Returns: Boolean expression result

◆ handle_chr_conversion()

exprt string_handler::handle_chr_conversion	(	const exprt &	codepoint_arg,
		const locationt &	location )

Handle chr() builtin function Converts a Unicode code point to its string representation Supports chr(i) where i is an integer in range [0, 0x10FFFF].

Parameters

codepoint_arg	The integer code point to convert
location	Source location for error reporting

Returns: Expression representing the resulting string (char array pointer)

◆ handle_int_conversion()

exprt string_handler::handle_int_conversion	(	const exprt &	arg,
		const locationt &	location )

Handle int() builtin with automatic type detection Supports int(x) where x can be: int, float, bool, or string.

Parameters

arg	The argument to convert
location	Source location for error reporting

Returns: Expression representing the integer result

◆ handle_int_conversion_with_base()

exprt string_handler::handle_int_conversion_with_base	(	const exprt &	arg,
		const exprt &	base,
		const locationt &	location )

Handle int() builtin with explicit base Supports int(x, base) where x is a string.

Parameters

arg	The string argument to convert
base	The base for conversion
location	Source location for error reporting

Returns: Expression representing the integer result

◆ handle_ord_conversion()

exprt string_handler::handle_ord_conversion	(	const exprt &	string_obj,
		const locationt &	location )

Handle ord() of a runtime string whose value is not known at compile time.

Returns the integer code point of the string's first character, (int) *base. A length-1 precondition is not enforced because a runtime guard cannot be short-circuited inside an and/or operand; constant strings (including multi-byte) are folded by the caller instead.

Parameters

string_obj	The runtime string argument
location	Source location for error reporting

Returns: Expression representing the integer code point

◆ handle_single_char_comparison()

exprt string_handler::handle_single_char_comparison	(	const std::string &	op,
		exprt &	lhs,
		exprt &	rhs )

Handle single character comparisons.

Parameters

op	Comparison operator
lhs	Left operand
rhs	Right operand

Returns: Comparison expression or nil_exprt if not a char comparison

◆ handle_startswith_endswith_with_pos()

exprt string_handler::handle_startswith_endswith_with_pos	(	const exprt &	string_obj,
		const nlohmann::json &	args,
		python_converter &	converter,
		const locationt &	location,
		bool	is_suffix )

Handle str.startswith/endswith with optional start/end position arguments: s.startswith(prefix, start[, end]) is evaluated as s[start:end].startswith(prefix).

is_suffix selects endswith. Constant receiver and constant start/end only.

◆ handle_str_join()

exprt string_handler::handle_str_join ( const nlohmann::json & call_json )

Handle str.join() method.

Parameters

call_json JSON node representing the join call

Returns: Expression representing the joined string

Handles Python's str.join(iterable) method, e.g.:

" ".join(["a", "b", "c"]) -> "a b c"
"-".join(list_var) -> joined string

◆ handle_string_attribute_call()

exprt string_handler::handle_string_attribute_call ( const nlohmann::json & call_json )

Dispatch and handle string attribute method calls.

Returns a non-nil expression when the attribute method is recognized as a supported string operation. Returns nil_exprt for non-string methods so callers can continue normal dispatch.

◆ handle_string_capitalize()

exprt string_handler::handle_string_capitalize	(	const exprt &	string_obj,
		const locationt &	location )

Handle str.capitalize() method.

◆ handle_string_casefold()

exprt string_handler::handle_string_casefold	(	const exprt &	string_obj,
		const locationt &	location )

Handle str.casefold() method.

◆ handle_string_center()

exprt string_handler::handle_string_center	(	const exprt &	string_obj,
		const exprt &	width_arg,
		const exprt &	fill_arg,
		const locationt &	location )

Handle str.center() method (constant-only support).

◆ handle_string_comparison()

exprt string_handler::handle_string_comparison	(	const std::string &	op,
		exprt &	lhs,
		exprt &	rhs,
		const nlohmann::json &	element )

Handle string comparison operations.

Parameters

op	Comparison operator (Eq, NotEq, etc.)
lhs	Left operand
rhs	Right operand
element	JSON element with location info

Returns: Comparison expression or nil_exprt to continue with standard comparison

◆ handle_string_concatenation()

exprt string_handler::handle_string_concatenation	(	const exprt &	lhs,
		const exprt &	rhs,
		const nlohmann::json &	left,
		const nlohmann::json &	right )

Handle string concatenation.

Parameters

lhs	Left operand
rhs	Right operand
left	JSON node for left operand
right	JSON node for right operand

Returns: Concatenated string expression

◆ handle_string_concatenation_with_promotion()

exprt string_handler::handle_string_concatenation_with_promotion	(	exprt &	lhs,
		exprt &	rhs,
		const nlohmann::json &	left,
		const nlohmann::json &	right )

Handle string concatenation with type promotion.

Parameters

lhs	Left operand
rhs	Right operand
left	JSON node for left operand
right	JSON node for right operand

Returns: Concatenated string expression

◆ handle_string_count()

exprt string_handler::handle_string_count	(	const exprt &	string_obj,
		const exprt &	sub_arg,
		const exprt &	start_arg,
		const exprt &	end_arg,
		const locationt &	location )

Handle str.count() method (constant fold, else runtime model).

◆ handle_string_endswith()

exprt string_handler::handle_string_endswith	(	const exprt &	string_obj,
		const exprt &	suffix_arg,
		const locationt &	location )

Handle str.endswith() method.

Parameters

string_obj	String object
suffix_arg	Suffix to check
location	Source location

Returns: Boolean expression result

◆ handle_string_expandtabs()

exprt string_handler::handle_string_expandtabs	(	const exprt &	string_obj,
		const exprt &	tabsize_arg,
		const locationt &	location )

Handle str.expandtabs() method (constant-only support).

◆ handle_string_find()

exprt string_handler::handle_string_find	(	const exprt &	string_obj,
		const exprt &	find_arg,
		const locationt &	location )

Handle str.find() method.

Parameters

string_obj	String object
find_arg	String to check
location	Source location

Returns: returns the index of the first occurrence of the substring. If not found, it returns -1.

◆ handle_string_find_range()

exprt string_handler::handle_string_find_range	(	const exprt &	string_obj,
		const exprt &	find_arg,
		const exprt &	start_arg,
		const exprt &	end_arg,
		const locationt &	location )

Handle str.find() with start/end.

Parameters

string_obj	String object
find_arg	String to check
start_arg	Start index
end_arg	End index (INT_MIN means default)
location	Source location

Returns: index of the first occurrence within range, or -1 if not found

◆ handle_string_format()

exprt string_handler::handle_string_format	(	const nlohmann::json &	call,
		const exprt &	string_obj,
		const locationt &	location )

Handle str.format() method (minimal support, constant-only).

◆ handle_string_format_map()

exprt string_handler::handle_string_format_map	(	const nlohmann::json &	call,
		const exprt &	string_obj,
		const locationt &	location )

Handle str.format_map() method (minimal support, constant-only).

◆ handle_string_index()

exprt string_handler::handle_string_index	(	const nlohmann::json &	call,
		const exprt &	string_obj,
		const exprt &	find_arg,
		const locationt &	location )

Handle str.index() method.

Parameters

string_obj	String object
find_arg	String to check
location	Source location

Returns: returns the index of the first occurrence of the substring.

Exceptions

ValueError if substring is not found.

◆ handle_string_index_range()

exprt string_handler::handle_string_index_range	(	const nlohmann::json &	call,
		const exprt &	string_obj,
		const exprt &	find_arg,
		const exprt &	start_arg,
		const exprt &	end_arg,
		const locationt &	location )

Handle str.index() with start/end.

Parameters

string_obj	String object
find_arg	String to check
start_arg	Start index
end_arg	End index (INT_MIN means default)
location	Source location

Returns: index of the first occurrence within range.

Exceptions

ValueError if substring is not found.

◆ handle_string_is_float()

exprt string_handler::handle_string_is_float	(	const exprt &	string_obj,
		const locationt &	location )

Build a call to the __python_str_is_float operational model, returning a bool that is true iff the runtime string is a valid Python float literal.

Parameters

string_obj	The string argument to validate
location	Source location for error reporting

Returns: Boolean expression (the validity predicate)

◆ handle_string_isalnum()

exprt string_handler::handle_string_isalnum	(	const exprt &	string_obj,
		const locationt &	location )

Handle str.isalnum() method.

◆ handle_string_isalpha()

exprt string_handler::handle_string_isalpha	(	const exprt &	string_obj,
		const locationt &	location )

Handle str.isalpha() method.

Parameters

string_obj	String object (can be string or single char)
location	Source location

Returns: Boolean expression result

◆ handle_string_isdigit()

exprt string_handler::handle_string_isdigit	(	const exprt &	string_obj,
		const locationt &	location )

Handle str.isdigit() method.

Parameters

string_obj	String object
location	Source location

Returns: Boolean expression result

◆ handle_string_isidentifier()

exprt string_handler::handle_string_isidentifier	(	const exprt &	string_obj,
		const locationt &	location )

Handle str.isidentifier() method.

◆ handle_string_islower()

exprt string_handler::handle_string_islower	(	const exprt &	string_obj,
		const locationt &	location )

Handle Python's str.islower() method.

Parameters

string_obj	Expression representing the string or character to check
location	Source location for error reporting

Returns: Boolean expression: true if all cased chars are lowercase, false otherwise

◆ handle_string_isnumeric()

exprt string_handler::handle_string_isnumeric	(	const exprt &	string_obj,
		const locationt &	location )

Handle str.isnumeric() method.

◆ handle_string_isspace()

exprt string_handler::handle_string_isspace	(	const exprt &	str_expr,
		const locationt &	location )

Handle str.isspace() method for strings.

Parameters

str_expr	String expression
location	Source location

Returns: Boolean expression result

◆ handle_string_isupper()

exprt string_handler::handle_string_isupper	(	const exprt &	string_obj,
		const locationt &	location )

Handle str.isupper() method.

◆ handle_string_ljust()

exprt string_handler::handle_string_ljust	(	const exprt &	string_obj,
		const exprt &	width_arg,
		const exprt &	fill_arg,
		const locationt &	location )

Handle str.ljust() method (constant-only support).

◆ handle_string_lower()

exprt string_handler::handle_string_lower	(	const exprt &	string_obj,
		const locationt &	location )

Handle str.lower() method.

Parameters

string_obj	String object
location	Source location

Returns: Pointer to lowercase string

◆ handle_string_lstrip()

exprt string_handler::handle_string_lstrip	(	const exprt &	str_expr,
		const exprt &	chars_arg,
		const locationt &	location )

Handle str.lstrip() method.

Parameters

str_expr	String expression
chars_arg	Optional characters to strip (empty for whitespace)
location	Source location

Returns: Pointer to stripped string

◆ handle_string_membership()

exprt string_handler::handle_string_membership	(	exprt &	lhs,
		exprt &	rhs,
		const nlohmann::json &	element )

Handle 'in' operator for strings.

Parameters

lhs	Substring to find
rhs	String to search in
element	JSON element with location info

Returns: Boolean expression result

◆ handle_string_operations()

exprt string_handler::handle_string_operations	(	const std::string &	op,
		exprt &	lhs,
		exprt &	rhs,
		const nlohmann::json &	left,
		const nlohmann::json &	right,
		const nlohmann::json &	element )

Handle general string operations.

Parameters

op	Operation type
lhs	Left operand
rhs	Right operand
left	JSON node for left operand
right	JSON node for right operand
element	JSON element with location info

Returns: Operation result expression

◆ handle_string_partition()

exprt string_handler::handle_string_partition	(	const exprt &	string_obj,
		const exprt &	sep_arg,
		const locationt &	location )

Handle str.partition() method (constant-only support).

◆ handle_string_removeprefix()

exprt string_handler::handle_string_removeprefix	(	const exprt &	string_obj,
		const exprt &	prefix_arg,
		const locationt &	location )

Handle str.removeprefix() method.

◆ handle_string_removesuffix()

exprt string_handler::handle_string_removesuffix	(	const exprt &	string_obj,
		const exprt &	suffix_arg,
		const locationt &	location )

Handle str.removesuffix() method.

◆ handle_string_repetition()

exprt string_handler::handle_string_repetition	(	exprt &	lhs,
		exprt &	rhs )

Handle string repetition.

Parameters

lhs	Left operand
rhs	Right operand

Returns: Repetition expression

◆ handle_string_replace()

exprt string_handler::handle_string_replace	(	const exprt &	string_obj,
		const exprt &	old_arg,
		const exprt &	new_arg,
		const exprt &	count_arg,
		const locationt &	location )

Handle str.replace() method.

Parameters

string_obj	String object
old_arg	Substring to replace
new_arg	Replacement substring
count_arg	Maximum replacements (-1 for all)
location	Source location

Returns: Pointer to replaced string

◆ handle_string_rfind()

exprt string_handler::handle_string_rfind	(	const exprt &	string_obj,
		const exprt &	find_arg,
		const locationt &	location )

Handle str.rfind() method.

Parameters

string_obj	String object
find_arg	String to check
location	Source location

Returns: returns the index of the last occurrence of the substring. If not found, it returns -1.

◆ handle_string_rfind_range()

exprt string_handler::handle_string_rfind_range	(	const exprt &	string_obj,
		const exprt &	find_arg,
		const exprt &	start_arg,
		const exprt &	end_arg,
		const locationt &	location )

Handle str.rfind() with start/end.

Parameters

string_obj	String object
find_arg	String to check
start_arg	Start index
end_arg	End index (INT_MIN means default)
location	Source location

Returns: index of the last occurrence within range, or -1 if not found

◆ handle_string_rindex()

exprt string_handler::handle_string_rindex	(	const nlohmann::json &	call,
		const exprt &	string_obj,
		const exprt &	find_arg,
		const locationt &	location )

Handle str.rindex() method (rfind that raises on not-found).

Parameters

call	Call AST node (for the temp/exception location)
string_obj	String object
find_arg	Substring to locate
location	Source location

Returns: index of the last occurrence of the substring.

Exceptions

ValueError if substring is not found.

◆ handle_string_rindex_range()

exprt string_handler::handle_string_rindex_range	(	const nlohmann::json &	call,
		const exprt &	string_obj,
		const exprt &	find_arg,
		const exprt &	start_arg,
		const exprt &	end_arg,
		const locationt &	location )

Handle str.rindex() with start/end.

Parameters

call	Call AST node (for the temp/exception location)
string_obj	String object
find_arg	Substring to locate
start_arg	Start index
end_arg	End index (INT_MIN means default)
location	Source location

Returns: index of the last occurrence within range.

Exceptions

ValueError if substring is not found.

◆ handle_string_rjust()

exprt string_handler::handle_string_rjust	(	const exprt &	string_obj,
		const exprt &	width_arg,
		const exprt &	fill_arg,
		const locationt &	location )

Handle str.rjust() method (constant-only support).

◆ handle_string_rpartition()

exprt string_handler::handle_string_rpartition	(	const exprt &	string_obj,
		const exprt &	sep_arg,
		const locationt &	location )

Handle str.rpartition() method (constant-only support).

Like partition() but splits at the last occurrence of the separator.

◆ handle_string_rstrip()

exprt string_handler::handle_string_rstrip	(	const exprt &	str_expr,
		const exprt &	chars_arg,
		const locationt &	location )

Handle str.rstrip() method.

Parameters

str_expr	String expression
chars_arg	Optional characters to strip (empty for whitespace)
location	Source location

Returns: Pointer to stripped string

◆ handle_string_splitlines()

exprt string_handler::handle_string_splitlines	(	const nlohmann::json &	call,
		const exprt &	string_obj,
		const locationt &	location,
		bool	keepends = false )

Handle str.splitlines() method (constant-only support).

◆ handle_string_startswith()

exprt string_handler::handle_string_startswith	(	const exprt &	string_obj,
		const exprt &	prefix_arg,
		const locationt &	location )

Handle str.startswith() method.

Parameters

string_obj	String object
prefix_arg	Prefix to check
location	Source location

Returns: Boolean expression result

◆ handle_string_strip()

exprt string_handler::handle_string_strip	(	const exprt &	str_expr,
		const exprt &	chars_arg,
		const locationt &	location )

Handle str.strip() method.

Parameters

str_expr	String expression
chars_arg	Optional characters to strip (empty for whitespace)
location	Source location

Returns: Pointer to stripped string

◆ handle_string_swapcase()

exprt string_handler::handle_string_swapcase	(	const exprt &	string_obj,
		const locationt &	location )

Handle str.swapcase() method.

◆ handle_string_title()

exprt string_handler::handle_string_title	(	const exprt &	string_obj,
		const locationt &	location )

Handle str.title() method.

◆ handle_string_to_float()

exprt string_handler::handle_string_to_float	(	const exprt &	string_obj,
		const locationt &	location )

Convert a runtime string expression to a double via the __python_str_to_float operational model.

Handles both char arrays and char pointers (function parameters). The caller is responsible for gating the conversion on handle_string_is_float() and raising ValueError on the invalid path.

Parameters

string_obj	The string argument to convert
location	Source location for error reporting

Returns: Expression representing the float (double) result

◆ handle_string_to_int()

exprt string_handler::handle_string_to_int	(	const exprt &	string_obj,
		const exprt &	base_arg,
		const locationt &	location )

Convert a string to an integer using Python's int() function.

Parameters

string_obj	The string expression to convert
base_arg	The base for conversion (2-36, or 0 for auto-detect)
location	Source location for error reporting

Returns: Expression representing the integer result

◆ handle_string_to_int_base10()

exprt string_handler::handle_string_to_int_base10	(	const exprt &	string_obj,
		const locationt &	location )

Convert a string to an integer using base 10 (convenience method).

Parameters

string_obj	The string expression to convert
location	Source location for error reporting

Returns: Expression representing the integer result

◆ handle_string_upper()

exprt string_handler::handle_string_upper	(	const exprt &	string_obj,
		const locationt &	location )

Handle str.upper() method.

Parameters

string_obj	String object
location	Source location

Returns: Pointer to uppercase string

◆ handle_string_zfill()

exprt string_handler::handle_string_zfill	(	const exprt &	string_obj,
		const exprt &	width_arg,
		const locationt &	location )

Handle str.zfill() method (constant-only support).

◆ is_zero_length_array()

bool string_handler::is_zero_length_array ( const exprt & expr )

Check if an expression is a zero-length array.

Parameters

expr	Expression to check

Returns: True if zero-length array

◆ join_unfoldable_iterable()

exprt string_handler::join_unfoldable_iterable	(	const exprt &	separator,
		const nlohmann::json &	call_json )

◆ nondet_str_buffer_size()

int string_handler::nondet_str_buffer_size ( )

static

The nondet str buffer size: –nondet-str-length plus the NUL.

◆ process_format_spec()

std::string string_handler::process_format_spec ( const nlohmann::json & format_spec )

Process format specification for f-strings.

Parameters

format_spec JSON format specification

Returns: Format string

◆ read_tagged_str_receiver()

exprt string_handler::read_tagged_str_receiver	(	const exprt &	receiver,
		const std::string &	method,
		const nlohmann::json &	call_json )

The str a tagged receiver of str-only method method holds, after raising AttributeError on the paths where it holds another type.

Any other receiver is returned unchanged.

◆ set_string_builder()

void string_handler::set_string_builder ( string_builder * sb )

inline

◆ try_handle_len_string_fast_path()

exprt string_handler::try_handle_len_string_fast_path	(	const nlohmann::json &	call_json,
		const exprt &	arg_expr )

Try fast-path folding for len() when argument is string-like.

Returns non-nil when a compile-time or cheap symbolic shortcut is available. Returns nil_exprt when caller should fall back to the generic len() handling path.

The documentation for this class was generated from the following files:

src/python-frontend/string/string_handler.h
src/python-frontend/string/string_handler.cpp
src/python-frontend/string/string_method_handler.cpp

Public Member Functions

Static Public Member Functions

Detailed Description

Constructor & Destructor Documentation

◆ string_handler()

Member Function Documentation

◆ apply_format_specification()

◆ build_affix_tuple_match()

◆ build_fstring_conversion()

◆ build_nondet_string()

◆ build_nondet_string_fallback()

◆ build_partition_tuple()

◆ build_repr()

◆ char_array_type_length()

◆ convert_join_items()

◆ convert_to_string()

◆ cpython_float_str()

◆ create_char_comparison_expr()

◆ ensure_null_terminated_string()

◆ ensure_string_array()

◆ extract_constant_string()

◆ extract_string_from_array_operands()

◆ format_fstring_part()

◆ format_runtime_value()

◆ fstring_repr_of_constant()

◆ get_array_base_address()

◆ get_fstring_expr()

◆ get_string_size()

◆ handle_char_isspace()

◆ handle_chr_conversion()

◆ handle_int_conversion()

◆ handle_int_conversion_with_base()

◆ handle_ord_conversion()

◆ handle_single_char_comparison()

◆ handle_startswith_endswith_with_pos()

◆ handle_str_join()

◆ handle_string_attribute_call()

◆ handle_string_capitalize()

◆ handle_string_casefold()

◆ handle_string_center()

◆ handle_string_comparison()

◆ handle_string_concatenation()

◆ handle_string_concatenation_with_promotion()

◆ handle_string_count()

◆ handle_string_endswith()

◆ handle_string_expandtabs()

◆ handle_string_find()

◆ handle_string_find_range()

◆ handle_string_format()

◆ handle_string_format_map()

◆ handle_string_index()

◆ handle_string_index_range()

◆ handle_string_is_float()

◆ handle_string_isalnum()

◆ handle_string_isalpha()

◆ handle_string_isdigit()

◆ handle_string_isidentifier()

◆ handle_string_islower()

◆ handle_string_isnumeric()

◆ handle_string_isspace()

◆ handle_string_isupper()

◆ handle_string_ljust()

◆ handle_string_lower()

◆ handle_string_lstrip()

◆ handle_string_membership()

◆ handle_string_operations()

◆ handle_string_partition()

◆ handle_string_removeprefix()

◆ handle_string_removesuffix()

◆ handle_string_repetition()

◆ handle_string_replace()

◆ handle_string_rfind()

◆ handle_string_rfind_range()

◆ handle_string_rindex()

◆ handle_string_rindex_range()

◆ handle_string_rjust()

◆ handle_string_rpartition()

◆ handle_string_rstrip()

◆ handle_string_splitlines()

◆ handle_string_startswith()