#include <optional>
#include <limits>
#include <type_traits>
#include <vector>
#include <util/arith/arith_tools.h>
#include <util/expr/base_type.h>
#include <util/lang/c_types.h>
#include <util/expr/expr_reassociate.h>
#include <util/expr/expr_util.h>
#include <irep2/irep2.h>
#include <irep2/irep2_utils.h>
#include <irep2/simplification_check.h>
#include <util/expr/type_byte_size.h>

Include dependency graph for expr_simplifier.cpp:

Classes
struct	Addtor< constant_type >
struct	Subtor< constant_type >
struct	Multor< constant_type >
struct	Negator< constant_type >
struct	abstor< constant_type >
struct	Andtor< constant_type >
struct	Ortor< constant_type >
struct	Xortor< constant_type >
struct	Impliestor< constant_type >
struct	IEEE_equalitytor< constant_type >
struct	Equalitytor< constant_type >
struct	IEEE_notequalitytor< constant_type >
struct	Notequaltor< constant_type >
struct	Lessthantor< constant_type >
struct	Greaterthantor< constant_type >
struct	Lessthanequaltor< constant_type >
struct	Greaterthanequaltor< constant_type >
struct	Isnantor< constant_type >
struct	Isinftor< constant_type >
struct	Isnormaltor< constant_type >
struct	Isfinitetor< constant_type >
struct	Signbittor< constant_type >
struct	IEEE_addtor< constant_type >
struct	IEEE_subtor< constant_type >
struct	IEEE_multor< constant_type >
struct	IEEE_divtor< constant_type >

Macros
#define	ESBMC_NIL_SIMPLIFY(name)

Functions
static expr2tc	try_simplification (const expr2tc &expr)
static expr2tc	typecast_check_return (const type2tc &type, const expr2tc &expr)
template<template< typename > class TFunctor, typename constructor>
static expr2tc	simplify_arith_2ops (const type2tc &type, const expr2tc &side_1, const expr2tc &side_2)
static bool	fits_in_width (const BigInt &value, unsigned width, bool is_signed)
	Check if value fits in given bit width without overflow.
static bool	is_all_ones_constant (const expr2tc &e)
	True if `e` is a constant_int that holds the all-ones bit pattern for its type.
static bool	coerce_to_common_type (expr2tc &a, expr2tc &b)
	Coerce two operands of a binary fold to a common type so a freshly rebuilt node is well-formed even when `a` and `b` carry different concrete bv widths.
static expr2tc	simplify_pointer_add_const (const type2tc &type, const expr2tc &side_1, const expr2tc &side_2)
	(p + C1) + C2 -> p + (C1 + C2), for a pointer-typed add.
static expr2tc	fold_bitnot_plus_const (const type2tc &type, const expr2tc &first, const expr2tc &second)
	~B + C -> (C - 1) - B for one ordering of the operands, since ~B == -B - 1.
static expr2tc	simplify_add_bv_identities (const type2tc &type, const expr2tc &side_1, const expr2tc &side_2)
	Bitvector-only add identities that reassociation leaves behind (#626).
static bool	address_root_and_offset (const expr2tc &e, expr2tc &root, BigInt &offset)
	Decompose an address into the object it is rooted at and its constant byte offset within it, walking constant subscripts and members and looking through the pointer casts a byte-distance idiom spells.
static expr2tc	fold_address_difference (const expr2tc &a, const expr2tc &b, const type2tc &type)
	&base.x - &base.y and &base[i] - &base[j] fold to the distance between the two sub-objects, in units of the operands' own pointee type.
static expr2tc	fold_common_addend (const expr2tc &a, const expr2tc &b, const type2tc &type)
	(w + x) - (y + z) with one shared addend cancels the common term; nil when no addend is shared or the surviving pair cannot be rebuilt.
static expr2tc	fold_pointer_minus_const (const type2tc &type, const expr2tc &side_1, const expr2tc &side_2)
	p - c -> p + (-c) for a signed constant c.
static expr2tc	fold_pointer_sub (const type2tc &type, const expr2tc &side_1, const expr2tc &side_2)
	The two folds a subtraction over addresses has: the distance between two of them, and a decrement re-spelled as an increment.
template<template< typename > class TFunctor, typename constructor>
static expr2tc	simplify_arith_1op (const type2tc &type, const expr2tc &value)
static bool	float_signs_agree (const expr2tc &a, const expr2tc &b)
	Do the float constants in two expressions that already compare equal agree on their signs?
static bool	same_value_and_sign (const expr2tc &a, const expr2tc &b)
	Whether two expressions denote the same value, sign included.
static bool	is_plus_zero (const expr2tc &e)
	Whether a constant is zero, and +0.0 if it is a float.
static bool	index_outside (const constant_int2t &index, size_t size)
static expr2tc	fold_union_member_read (const constant_union2t &uni, const irep_idt &member, const type2tc &type)
	Project a member read out of a constant union literal, or return nothing.
static expr2tc	fold_struct_member_read (const constant_struct2t &lit, const irep_idt &member, const type2tc &type)
	The selected member of a struct literal, or nil when the fold does not apply.
static expr2tc	simplify_object (const expr2tc &expr)
static bool	is_null_pointer_constant (const expr2tc &expr)
static bool	ptr_subtype_resolvable (const expr2tc &ptr_op)
	Whether a symbol-typed (named struct/union) subtype of `ptr_op` can be resolved here: type_byte_size_expr follows it through the installed namespace.
static bool	index_values_equal (const expr2tc &idx1, const expr2tc &idx2)
static expr2tc	resolve_with_chain_lookup (const type2tc &elem_type, const expr2tc &source, const expr2tc &lookup_index)
template<template< typename > class TFunctor, typename constructor>
static expr2tc	simplify_logic_2ops (const type2tc &type, const expr2tc &side_1, const expr2tc &side_2)
template<typename OpType, typename OpConstructor>
expr2tc	simplify_associative_binary_op (const type2tc &result_type, const expr2tc &side_1, const expr2tc &side_2, bool(is_op_type)(const expr2tc &), const OpType &(to_op_type)(const expr2tc &), OpConstructor op_constructor)
template<typename constructor, typename U64Op>
static expr2tc	do_bit_munge_operation (U64Op opfunc, const type2tc &type, const expr2tc &side_1, const expr2tc &side_2)
template<class ShiftT>
static expr2tc	combine_constant_shifts (const type2tc &type, const expr2tc &outer_lhs, const expr2tc &outer_amt, bool(is_inner)(const expr2tc &), const ShiftT &(to_inner)(const expr2tc &))
	Try to combine outer(inner(x, c1), c2) where both c1 and c2 are constant ints into outer(x, c1 + c2).
static bool	is_null_pointer (const expr2tc &expr)
static bool	address_of_is_provably_non_null (const expr2tc &e)
static bool	is_null_pointer_value (const expr2tc &expr)
static std::optional< expr2tc >	fold_constant_bool_source (const type2tc &type, const expr2tc &simp, const expr2tc &rounding_mode)
	Typecast of a constant bool to a number type; nullopt when no arm matches.
static std::optional< expr2tc >	fold_constant_bv_source (const type2tc &type, const expr2tc &simp, const expr2tc &rounding_mode)
	Typecast of a constant integer to a number type; nullopt when no arm matches.
static std::optional< expr2tc >	fold_constant_fixedbv_source (const type2tc &type, const expr2tc &simp, const expr2tc &rounding_mode)
	Typecast of a constant fixed-point value to a number type; nullopt when no arm matches.
static std::optional< expr2tc >	fold_constant_floatbv_source (const type2tc &type, const expr2tc &simp, const expr2tc &rounding_mode)
	Typecast of a constant float to a number type; nullopt when no arm matches.
static std::optional< expr2tc >	fold_constant_typecast (const type2tc &type, const expr2tc &simp, const expr2tc &rounding_mode)
	Constant-operand typecasts, dispatched on the source type.
static expr2tc	linearise_enclosing_indices (const index2t &idx, BigInt &offset)
	Linearise the constant-indexed rows enclosing `idx:` for &a[c1]..[cn][e] return the same chain with every enclosing index zeroed, and set `offset` to c1*s1 + .
template<template< typename > class TFunctor>
static expr2tc	simplify_constant_relation (const type2tc &type, const expr2tc &side_1, const expr2tc &side_2)
	Fold a relation between two constants.
static expr2tc	subscript_offset_in_units (const std::vector< const expr2tc * > &chain, const type2tc &pointee, const type2tc &offset_t)
	Sum a chain's subscripts, each scaled into `pointee-sized` units; nil when a step is not a whole number of them or cannot be measured at all.
static expr2tc	flatten_nested_index_address (const address_of2t &ao)
	Flatten &a[i][j] to &a[0][0] + (i * N + j), and &s[i].v[j] likewise, with the offset counted in the pointer's own pointee type.
static const expr2tc *	byte_view_root (const expr2tc &obj)
	(char )&root.m[i], or a byte member's own &root.c, as (char )&root + byte offset: a byte-wise walk and its bound then share one base whichever member or element each end names, as the relation folds below need.
static expr2tc	byte_view_anchor (const expr2tc &root, const type2tc &to)
	One anchor for every byte view of `root`, so both ends compare equal: a cast the frontend wrote and one built here need not.
static expr2tc	byte_address_on_root (const expr2tc &e)
static expr2tc	flatten_addressof_under_add (const expr2tc &e)
	Reach the address_of under pointer arithmetic: an induction variable started at &a[1][0] arrives here as &a[1][0] + k and has to be put on the same base as the bound it is compared against.
static expr2tc	normalize_addressof_index (const expr2tc &e)
template<typename Rebuild>
static expr2tc	normalize_addressof_operands (const expr2tc &a, const expr2tc &b, Rebuild rebuild)
	Put both operands of a pointer comparison into &base[0] + c form, and return the rebuilt comparison when either changed.
template<typename constructor>
static expr2tc	compare_with_bare_base (const type2tc &type, const expr2tc &base, const expr2tc &sum, bool base_first)
	A bare byte base is base + 0: (char )&o < (char )&o + 12 is 0 < 12.
template<typename constructor>
static expr2tc	cancel_shared_pointer_base (const type2tc &type, const expr2tc &side_1, const expr2tc &side_2)
	(&x + c1) ~ (&x + c2) reduces to c1 ~ c2: when the bases match, comparing addresses is comparing offsets.
template<template< typename > class TFunctor, typename constructor>
static expr2tc	simplify_relations (const type2tc &type, const expr2tc &side_1, const expr2tc &side_2)
template<template< typename > class TFunctor, typename constructor>
static expr2tc	simplify_floatbv_relations (const type2tc &type, const expr2tc &side_1, const expr2tc &side_2)
static expr2tc	widened_bool_compared_to_zero (const expr2tc &side_1, const expr2tc &side_2)
	Recognise (T)b compared against zero, for b already boolean.
template<class Rel2t>
static expr2tc	fold_const_across_addsub (const expr2tc &side_1, const expr2tc &side_2)
	(x + c1) REL c2 -> x REL (c2 - c1), and (x - c1) REL c2 -> x REL (c2 + c1), for REL in {==, !=}: the two hold together, since != x y is exactly the negation of == x y.
template<typename Rebuild>
static expr2tc	coerce_and_rebuild (const expr2tc &a_in, const expr2tc &b_in, Rebuild rebuild)
	Rewrite &base[c] to &base[0] + c for one comparison operand.
template<typename Rebuild>
static expr2tc	cancel_common_addend_operand (const expr2tc &side_1, const expr2tc &side_2, Rebuild rebuild)
	d + c ~ d + e -> c ~ e and (d - c) ~ (d - e) -> c ~ e: cancel the addend or minuend the two sides share.
template<typename Rebuild>
static expr2tc	cancel_common_unary_operand (const expr2tc &side_1, const expr2tc &side_2, Rebuild rebuild)
	(-x) ~ (-y) and (~x) ~ (~y): cancel the wrapper both sides share.
static const expr2tc &	peel_pointer_offsets (const expr2tc &e)
static expr2tc	obj_equals_addr_of (const expr2tc &a, const expr2tc &b)
static expr2tc	fold_distinct_objects_cmp (const expr2tc &s1, const expr2tc &s2, bool eq)
static expr2tc	simplify_pointer_cmp (const expr2tc &s1, const expr2tc &s2, bool eq)
static expr2tc	fold_odd_multiple_of_zero (const expr2tc &side_1, const expr2tc &side_2)
	(x * c) == 0 -> x == 0 when c is odd, or nothing.
template<class T>
static bool	is_negative_constant (const T &v)
	A bool constant is never negative, and GCC rejects bool < 0 outright (-Wbool-compare), so the sign shortcut below has to be skipped for the bool instantiation rather than merely evaluate to false.
static bool	is_type_max (const BigInt &c, const type2tc &t)
	Type-extreme detector.
static bool	is_type_min (const BigInt &c, const type2tc &t)
static bool	is_provably_nonneg (const expr2tc &e)
static bool	conditions_equivalent (const expr2tc &a, const expr2tc &b)
static expr2tc	handle_symmetric_cases (const expr2tc &a, const expr2tc &b)
static bool	symbol_is_own_object (const symbol2t &s)
static bool	distinct_named_objects (const symbol2t &a, const symbol2t &b)
template<template< typename > class TFunctor, typename constructor>
static expr2tc	simplify_floatbv_1op (const type2tc &type, const expr2tc &value)
template<template< typename > class TFunctor, typename constructor>
static expr2tc	simplify_floatbv_2ops (const type2tc &type, const expr2tc &side_1, const expr2tc &side_2, const expr2tc &rounding_mode)

Macro Definition Documentation

◆ ESBMC_NIL_SIMPLIFY

#define ESBMC_NIL_SIMPLIFY ( name )

Value:

  expr2tc name##2t ::do_simplify() const                                       \
  {                                                                            \
    return expr2tc();                                                          \
  }

Function Documentation

◆ address_of_is_provably_non_null()

bool address_of_is_provably_non_null ( const expr2tc & e )

static

◆ address_root_and_offset()

bool address_root_and_offset	(	const expr2tc &	e,
		expr2tc &	root,
		BigInt &	offset )

static

Decompose an address into the object it is rooted at and its constant byte offset within it, walking constant subscripts and members and looking through the pointer casts a byte-distance idiom spells.

False when any step is not a compile-time constant, which leaves the difference unfolded.

◆ byte_address_on_root()

expr2tc byte_address_on_root ( const expr2tc & e )

static

◆ byte_view_anchor()

expr2tc byte_view_anchor	(	const expr2tc &	root,
		const type2tc &	to )

static

One anchor for every byte view of root, so both ends compare equal: a cast the frontend wrote and one built here need not.

An array is anchored at its first element, since a pointer to the whole array can have a width get_width() rejects (alloca_ptrdiff_max); a byte array is left to the index path, where the cast would be a no-op. Nil for any other root.

◆ byte_view_root()

const expr2tc * byte_view_root ( const expr2tc & obj )

static

(char *)&root.m[i], or a byte member's own &root.c, as (char *)&root + byte offset: a byte-wise walk and its bound then share one base whichever member or element each end names, as the relation folds below need.

Nil unless the pointee is a byte, the chain is rooted at a symbol, and its offset is constant. The named object a member/index chain obj lives in, or nil when the chain passes anything else: a dereference would root it at the pointer variable instead of the pointee.

◆ cancel_common_addend_operand()

template<typename Rebuild>

expr2tc cancel_common_addend_operand	(	const expr2tc &	side_1,
		const expr2tc &	side_2,
		Rebuild	rebuild )

static

d + c ~ d + e -> c ~ e and (d - c) ~ (d - e) -> c ~ e: cancel the addend or minuend the two sides share.

Shared by equality2t and notequal2t: != x y holds iff == x y doesn't, so a rewrite that preserves equality preserves inequality too.

◆ cancel_common_unary_operand()

template<typename Rebuild>

expr2tc cancel_common_unary_operand	(	const expr2tc &	side_1,
		const expr2tc &	side_2,
		Rebuild	rebuild )

static

(-x) ~ (-y) and (~x) ~ (~y): cancel the wrapper both sides share.

◆ cancel_shared_pointer_base()

template<typename constructor>

expr2tc cancel_shared_pointer_base	(	const type2tc &	type,
		const expr2tc &	side_1,
		const expr2tc &	side_2 )

static

(&x + c1) ~ (&x + c2) reduces to c1 ~ c2: when the bases match, comparing addresses is comparing offsets.

Split out of simplify_relations to keep its decision count off the complexity gate.

◆ coerce_and_rebuild()

template<typename Rebuild>

expr2tc coerce_and_rebuild	(	const expr2tc &	a_in,
		const expr2tc &	b_in,
		Rebuild	rebuild )

static

Rewrite &base[c] to &base[0] + c for one comparison operand.

A loop exit spelled &a[4] must meet an induction variable built from increments off a, which carries the &a[0] + k shape; without a common form the guard stays a comparison symex cannot decide and the loop never exits (#6778). The rewrite is applied here rather than in expr2t::simplify because folding every address_of loses the concrete offset the value-set analysis needs (regression/incremental-smt/incremental-24). Re-emit a comparison over a_in and b_in after coercing them to a common type; nil when they have none. Pointer-arith chains reach the cancellations below with mixed-width integer offsets ((int)c against (long)e), so the coercion is not optional.

◆ coerce_to_common_type()

bool coerce_to_common_type	(	expr2tc &	a,
		expr2tc &	b )

static

Coerce two operands of a binary fold to a common type so a freshly rebuilt node is well-formed even when a and b carry different concrete bv widths.

Picks the wider of the two operand types; for non-constant operands a type mismatch is unsoundable, so returns false. Constants are reinterpreted at the common type via integer2binary round-trip so the bit pattern under sign-extension matches what the SMT layer would see.

Use whenever a peephole cancellation produces a fresh node from two surviving operands whose types may diverge — pointer-arith chains commonly mix (int)1 with (long)2 after C-frontend promotion, so a strict type-match guard would refuse the fold.

◆ combine_constant_shifts()

template<class ShiftT>

expr2tc combine_constant_shifts	(	const type2tc &	type,
		const expr2tc &	outer_lhs,
		const expr2tc &	outer_amt,
		bool(*	is_inner )(const expr2tc &),
		const ShiftT &(*	to_inner )(const expr2tc &) )

static

Try to combine outer(inner(x, c1), c2) where both c1 and c2 are constant ints into outer(x, c1 + c2).

Returns nil unless every operand is well-shaped and the combined amount is strictly less than the result width — beyond that, C semantics make the original UB and we must not mask the runtime overflow check.

◆ compare_with_bare_base()

template<typename constructor>

expr2tc compare_with_bare_base	(	const type2tc &	type,
		const expr2tc &	base,
		const expr2tc &	sum,
		bool	base_first )

static

A bare byte base is base + 0: (char *)&o < (char *)&o + 12 is 0 < 12.

Bytes only, since with a zero-sized pointee p and p + 1 are one address. base_first says which side of the relation base was.

◆ conditions_equivalent()

bool conditions_equivalent	(	const expr2tc &	a,
		const expr2tc &	b )

static

◆ distinct_named_objects()

bool distinct_named_objects	(	const symbol2t &	a,
		const symbol2t &	b )

static

◆ do_bit_munge_operation()

template<typename constructor, typename U64Op>

expr2tc do_bit_munge_operation	(	U64Op	opfunc,
		const type2tc &	type,
		const expr2tc &	side_1,
		const expr2tc &	side_2 )

static

◆ fits_in_width()

bool fits_in_width	(	const BigInt &	value,
		unsigned	width,
		bool	is_signed )

static

Check if value fits in given bit width without overflow.

◆ flatten_addressof_under_add()

expr2tc flatten_addressof_under_add ( const expr2tc & e )

static

Reach the address_of under pointer arithmetic: an induction variable started at &a[1][0] arrives here as &a[1][0] + k and has to be put on the same base as the bound it is compared against.

Nil when nothing nested was found, so the single-subscript path below stays as it was.

◆ flatten_nested_index_address()

expr2tc flatten_nested_index_address ( const address_of2t & ao )

static

Flatten &a[i][j] to &a[0][0] + (i * N + j), and &s[i].v[j] likewise, with the offset counted in the pointer's own pointee type.

address_of2t::do_simplify rewrites only the innermost subscript, so two addresses that differ in an outer one keep different bases and the cancellation below cannot reach them: a flat walk from &a[0][0] to &a[1][2] never exits. Zeroing every subscript gives them a base to share; members are kept as they are and contribute their own constant offset, so an array of structs walked as flat memory is the same rewrite rather than a second one. Only the comparison's operands are rewritten, so no dereference is built from the flattened form (#6778).

A subscript contributes subscript * (sizeof(element) / unit), which keeps a symbolic subscript symbolic.

◆ float_signs_agree()

bool float_signs_agree	(	const expr2tc &	a,
		const expr2tc &	b )

static

Do the float constants in two expressions that already compare equal agree on their signs?

Callers rely on a and b having the same shape.

◆ fold_address_difference()

expr2tc fold_address_difference	(	const expr2tc &	a,
		const expr2tc &	b,
		const type2tc &	type )

static

&base.x - &base.y and &base[i] - &base[j] fold to the distance between the two sub-objects, in units of the operands' own pointee type.

C23 6.5.6p9 defines pointer subtraction as that difference, so this is the standard's own answer rather than an optimisation; a differing root is undefined there and is left unfolded (#6779). Without it the difference stays a comparison operand symex cannot decide, and a loop bounded by it never exits.

◆ fold_bitnot_plus_const()

expr2tc fold_bitnot_plus_const	(	const type2tc &	type,
		const expr2tc &	first,
		const expr2tc &	second )

static

~B + C -> (C - 1) - B for one ordering of the operands, since ~B == -B - 1.

The bitnot folds into the constant beside it, and vanishes outright at C == 1. Applied across one level of an add chain too, this is the (A + 1) + ~B -> A - B family in whichever permutation reassociation leaves behind. A constant is required, so the rewrite never trades a bitnot for a longer expression.

◆ fold_common_addend()

expr2tc fold_common_addend	(	const expr2tc &	a,
		const expr2tc &	b,
		const type2tc &	type )

static

(w + x) - (y + z) with one shared addend cancels the common term; nil when no addend is shared or the surviving pair cannot be rebuilt.

Pointer-arith chains can have a common pointer base with mixed-width integer offsets, and the surviving sub's result type is the parent sub's type (ptrdiff for pointer-pointer subtraction, otherwise the arith type) — so the operands are coerced before the rebuilt sub2tc is handed back.

◆ fold_const_across_addsub()

template<class Rel2t>

expr2tc fold_const_across_addsub	(	const expr2tc &	side_1,
		const expr2tc &	side_2 )

static

(x + c1) REL c2 -> x REL (c2 - c1), and (x - c1) REL c2 -> x REL (c2 + c1), for REL in {==, !=}: the two hold together, since != x y is exactly the negation of == x y.

Requires homogeneous types across the entire shape: the add or sub, BOTH its operands, and c2 must share a single arithmetic domain. Mixed widths (e.g. (x_u8 + c_u16) == c2_u16) would silently rewrite into something that confuses modular semantics. The folded constant must also fit the compared type, or the rewrite would wrap where the original did not.

◆ fold_constant_bool_source()

std::optional< expr2tc > fold_constant_bool_source	(	const type2tc &	type,
		const expr2tc &	simp,
		const expr2tc &	rounding_mode )

static

Typecast of a constant bool to a number type; nullopt when no arm matches.

◆ fold_constant_bv_source()

std::optional< expr2tc > fold_constant_bv_source	(	const type2tc &	type,
		const expr2tc &	simp,
		const expr2tc &	rounding_mode )

static

Typecast of a constant integer to a number type; nullopt when no arm matches.

◆ fold_constant_fixedbv_source()

std::optional< expr2tc > fold_constant_fixedbv_source	(	const type2tc &	type,
		const expr2tc &	simp,
		const expr2tc &	rounding_mode )

static

Typecast of a constant fixed-point value to a number type; nullopt when no arm matches.

◆ fold_constant_floatbv_source()

std::optional< expr2tc > fold_constant_floatbv_source	(	const type2tc &	type,
		const expr2tc &	simp,
		const expr2tc &	rounding_mode )

static

Typecast of a constant float to a number type; nullopt when no arm matches.

◆ fold_constant_typecast()

std::optional< expr2tc > fold_constant_typecast	(	const type2tc &	type,
		const expr2tc &	simp,
		const expr2tc &	rounding_mode )

static

Constant-operand typecasts, dispatched on the source type.

nullopt when no arm matches, so the caller falls through to the non-constant cases exactly as the inline chain did; a nil expr2tc means an arm matched and declined (a non-constant rounding mode), which is do_simplify's own "no simplification" answer.

◆ fold_distinct_objects_cmp()

expr2tc fold_distinct_objects_cmp	(	const expr2tc &	s1,
		const expr2tc &	s2,
		bool	eq )

static

◆ fold_odd_multiple_of_zero()

expr2tc fold_odd_multiple_of_zero	(	const expr2tc &	side_1,
		const expr2tc &	side_2 )

static

(x * c) == 0 -> x == 0 when c is odd, or nothing.

Restricted to odd constants because modular bv multiplication is injective only for invertibles mod 2^width — i.e. constants coprime to 2^width, which for power-of-two moduli is exactly the odd constants. With c=2 in 8-bit unsigned, for example, x=128 also satisfies x*2 == 0 (mod 256), so dropping the multiplication would silently strengthen the predicate. The type guards keep the rewritten equality homogeneous.

◆ fold_pointer_minus_const()

expr2tc fold_pointer_minus_const	(	const type2tc &	type,
		const expr2tc &	side_1,
		const expr2tc &	side_2 )

static

p - c -> p + (-c) for a signed constant c.

A decrementing walk otherwise never reaches the base + offset form an incrementing one has, and every shared-base cancellation that decides a pointer comparison matches add2t, so the guard of a p-- loop stays undecidable and the loop never exits (#6779). An unsigned c is left alone: negating it is a wrap this rewrite has no reason to commit to.

◆ fold_pointer_sub()

expr2tc fold_pointer_sub	(	const type2tc &	type,
		const expr2tc &	side_1,
		const expr2tc &	side_2 )

static

The two folds a subtraction over addresses has: the distance between two of them, and a decrement re-spelled as an increment.

◆ fold_struct_member_read()

expr2tc fold_struct_member_read	(	const constant_struct2t &	lit,
		const irep_idt &	member,
		const type2tc &	type )

static

The selected member of a struct literal, or nil when the fold does not apply.

member2t's constructor asserts that the member resolves exactly once in the source's type, but only in debug builds; a release build reached the .value() this replaces and threw bad_optional_access, and an operand count short of the type's components read past the end of the vector. Both are the shape of the tuple-projection bound (#7758): decline, which is always sound, rather than trust the invariant (docs/roadmap/scope-clang-cpp-irep2.md §7.4).

◆ fold_union_member_read()

expr2tc fold_union_member_read	(	const constant_union2t &	uni,
		const irep_idt &	member,
		const type2tc &	type )

static

Project a member read out of a constant union literal, or return nothing.

A cross-member read between integer members of one width is an exact bit reinterpretation: { .r=v }.s is (s-type)v. Wider or non-integer members stay unfolded.

◆ handle_symmetric_cases()

expr2tc handle_symmetric_cases	(	const expr2tc &	a,
		const expr2tc &	b )

static

◆ index_outside()

bool index_outside	(	const constant_int2t &	index,
		size_t	size )

static

◆ index_values_equal()

bool index_values_equal	(	const expr2tc &	idx1,
		const expr2tc &	idx2 )

static

◆ is_all_ones_constant()

bool is_all_ones_constant ( const expr2tc & e )

static

True if e is a constant_int that holds the all-ones bit pattern for its type.

For signed bv that's -1 (BigInt(-1)); for unsigned bv that's 2^width - 1 (UINT_MAX). Useful for bitwise identities like x & all1 = x.

◆ is_negative_constant()

template<class T>

bool is_negative_constant ( const T & v )

static

A bool constant is never negative, and GCC rejects bool < 0 outright (-Wbool-compare), so the sign shortcut below has to be skipped for the bool instantiation rather than merely evaluate to false.

◆ is_null_pointer()

bool is_null_pointer ( const expr2tc & expr )

static

◆ is_null_pointer_constant()

bool is_null_pointer_constant ( const expr2tc & expr )

static

◆ is_null_pointer_value()

bool is_null_pointer_value ( const expr2tc & expr )

static

◆ is_plus_zero()

bool is_plus_zero ( const expr2tc & e )

static

Whether a constant is zero, and +0.0 if it is a float.

◆ is_provably_nonneg()

bool is_provably_nonneg ( const expr2tc & e )

static

◆ is_type_max()

bool is_type_max	(	const BigInt &	c,
		const type2tc &	t )

static

Type-extreme detector.

For an integer constant c against bv type t, reports whether the constant equals the type's representable max or min. Used to short-circuit ordered comparisons against the bounds of the type.

◆ is_type_min()

bool is_type_min	(	const BigInt &	c,
		const type2tc &	t )

static

◆ linearise_enclosing_indices()

expr2tc linearise_enclosing_indices	(	const index2t &	idx,
		BigInt &	offset )

static

Linearise the constant-indexed rows enclosing idx: for &a[c1]..[cn][e] return the same chain with every enclosing index zeroed, and set offset to c1*s1 + .

. + cn*sn counted in elements of the innermost type. Nil when there is no enclosing index, when one is not constant, or when a dimension has no constant size — the caller then keeps the single-level form.

This is what lets a pointer walking a as flat memory meet a bound spelled &a[1][2]: both sides reduce to an offset off &a[0][0] (#6778).

◆ normalize_addressof_index()

expr2tc normalize_addressof_index ( const expr2tc & e )

static

◆ normalize_addressof_operands()

template<typename Rebuild>

expr2tc normalize_addressof_operands	(	const expr2tc &	a,
		const expr2tc &	b,
		Rebuild	rebuild )

static

Put both operands of a pointer comparison into &base[0] + c form, and return the rebuilt comparison when either changed.

rebuild re-emits the node so the common-addend cancellation in the caller can decide it.

◆ obj_equals_addr_of()

expr2tc obj_equals_addr_of	(	const expr2tc &	a,
		const expr2tc &	b )

static

◆ peel_pointer_offsets()

const expr2tc & peel_pointer_offsets ( const expr2tc & e )

static

◆ ptr_subtype_resolvable()

bool ptr_subtype_resolvable ( const expr2tc & ptr_op )

static

Whether a symbol-typed (named struct/union) subtype of ptr_op can be resolved here: type_byte_size_expr follows it through the installed namespace.

Without one the offset is left to the SMT layer. Resolution can still find an incomplete or dynamically sized type; type_byte_size_expr owns that outcome.

◆ resolve_with_chain_lookup()

expr2tc resolve_with_chain_lookup	(	const type2tc &	elem_type,
		const expr2tc &	source,
		const expr2tc &	lookup_index )

static

◆ same_value_and_sign()

bool same_value_and_sign	(	const expr2tc &	a,
		const expr2tc &	b )

static

Whether two expressions denote the same value, sign included.

expr2tc equality on constant floats is IEEE equality (ieee_float.cpp), and under it -0.0 == +0.0. A rewrite that drops one of two "equal" operands – if(c, x, y) -> x, or with(s, f, v) -> s – therefore returns the wrong sign whenever they disagree on it, at any depth inside an aggregate constant (esbmc/esbmc#7321). NaN needs no guard here: IEEE equality already reports two NaNs as unequal, so those rewrites never fire on them.

◆ simplify_add_bv_identities()

expr2tc simplify_add_bv_identities	(	const type2tc &	type,
		const expr2tc &	side_1,
		const expr2tc &	side_2 )

static

Bitvector-only add identities that reassociation leaves behind (#626).

◆ simplify_arith_1op()

template<template< typename > class TFunctor, typename constructor>

expr2tc simplify_arith_1op	(	const type2tc &	type,
		const expr2tc &	value )

static

◆ simplify_arith_2ops()

template<template< typename > class TFunctor, typename constructor>

expr2tc simplify_arith_2ops	(	const type2tc &	type,
		const expr2tc &	side_1,
		const expr2tc &	side_2 )

static

◆ simplify_associative_binary_op()

template<typename OpType, typename OpConstructor>

expr2tc simplify_associative_binary_op	(	const type2tc &	result_type,
		const expr2tc &	side_1,
		const expr2tc &	side_2,
		bool(*	is_op_type )(const expr2tc &),
		const OpType &(*	to_op_type )(const expr2tc &),
		OpConstructor	op_constructor )

◆ simplify_constant_relation()

template<template< typename > class TFunctor>

expr2tc simplify_constant_relation	(	const type2tc &	type,
		const expr2tc &	side_1,
		const expr2tc &	side_2 )

static

Fold a relation between two constants.

The constant kind and the comparison itself are per-domain, so this dispatches on the operand type; C compares two booleans only after widening them to int, but a Java goto binary compares them directly. Split out of simplify_relations, whose own decision count is already over the complexity gate's threshold.

◆ simplify_floatbv_1op()

template<template< typename > class TFunctor, typename constructor>

expr2tc simplify_floatbv_1op	(	const type2tc &	type,
		const expr2tc &	value )

static

◆ simplify_floatbv_2ops()

template<template< typename > class TFunctor, typename constructor>

expr2tc simplify_floatbv_2ops	(	const type2tc &	type,
		const expr2tc &	side_1,
		const expr2tc &	side_2,
		const expr2tc &	rounding_mode )

static

◆ simplify_floatbv_relations()

template<template< typename > class TFunctor, typename constructor>

expr2tc simplify_floatbv_relations	(	const type2tc &	type,
		const expr2tc &	side_1,
		const expr2tc &	side_2 )

static

◆ simplify_logic_2ops()

template<template< typename > class TFunctor, typename constructor>

expr2tc simplify_logic_2ops	(	const type2tc &	type,
		const expr2tc &	side_1,
		const expr2tc &	side_2 )

static

◆ simplify_object()

expr2tc simplify_object ( const expr2tc & expr )

static

◆ simplify_pointer_add_const()

expr2tc simplify_pointer_add_const	(	const type2tc &	type,
		const expr2tc &	side_1,
		const expr2tc &	side_2 )

static

(p + C1) + C2 -> p + (C1 + C2), for a pointer-typed add.

Symex sometimes calls do_simplify() directly after renaming a pointer increment, bypassing the full expr2t::simplify() reassociation pass. Keep this pointer-only fold local so repeated increments still canonicalize.

◆ simplify_pointer_cmp()

expr2tc simplify_pointer_cmp	(	const expr2tc &	s1,
		const expr2tc &	s2,
		bool	eq )

static

◆ simplify_relations()

template<template< typename > class TFunctor, typename constructor>

expr2tc simplify_relations	(	const type2tc &	type,
		const expr2tc &	side_1,
		const expr2tc &	side_2 )

static

◆ subscript_offset_in_units()

expr2tc subscript_offset_in_units	(	const std::vector< const expr2tc * > &	chain,
		const type2tc &	pointee,
		const type2tc &	offset_t )

static

Sum a chain's subscripts, each scaled into pointee-sized units; nil when a step is not a whole number of them or cannot be measured at all.

Members contribute nothing: the rebuilt base keeps the member path as it is, so their offset is already in there. Counting it here too only shows up once the struct has padding before the member (struct { char c; int v[3]; } s[2]).

◆ symbol_is_own_object()

bool symbol_is_own_object ( const symbol2t & s )

static

◆ try_simplification()

expr2tc try_simplification ( const expr2tc & expr )

static

◆ typecast_check_return()

expr2tc typecast_check_return	(	const type2tc &	type,
		const expr2tc &	expr )

static

◆ widened_bool_compared_to_zero()

expr2tc widened_bool_compared_to_zero	(	const expr2tc &	side_1,
		const expr2tc &	side_2 )

static

Recognise (T)b compared against zero, for b already boolean.

Widening a bool to an integer yields exactly 0 or 1, so comparing it with zero recovers b itself – the bool->int->bool round trip every condition over a stored _Bool produces. Returns b, or nil when the operands are not that shape (#4626). The reverse trip does not fold: (int)(_Bool)i keeps only whether i was non-zero, so it is not the identity on i.

Classes

Macros

Functions

Macro Definition Documentation

◆ ESBMC_NIL_SIMPLIFY

Function Documentation

◆ address_of_is_provably_non_null()

◆ address_root_and_offset()

◆ byte_address_on_root()

◆ byte_view_anchor()

◆ byte_view_root()

◆ cancel_common_addend_operand()

◆ cancel_common_unary_operand()

◆ cancel_shared_pointer_base()

◆ coerce_and_rebuild()

◆ coerce_to_common_type()

◆ combine_constant_shifts()

◆ compare_with_bare_base()

◆ conditions_equivalent()

◆ distinct_named_objects()

◆ do_bit_munge_operation()

◆ fits_in_width()

◆ flatten_addressof_under_add()

◆ flatten_nested_index_address()

◆ float_signs_agree()

◆ fold_address_difference()

◆ fold_bitnot_plus_const()

◆ fold_common_addend()

◆ fold_const_across_addsub()

◆ fold_constant_bool_source()

◆ fold_constant_bv_source()

◆ fold_constant_fixedbv_source()

◆ fold_constant_floatbv_source()

◆ fold_constant_typecast()

◆ fold_distinct_objects_cmp()

◆ fold_odd_multiple_of_zero()

◆ fold_pointer_minus_const()

◆ fold_pointer_sub()

◆ fold_struct_member_read()

◆ fold_union_member_read()

◆ handle_symmetric_cases()

◆ index_outside()

◆ index_values_equal()

◆ is_all_ones_constant()

◆ is_negative_constant()

◆ is_null_pointer()

◆ is_null_pointer_constant()

◆ is_null_pointer_value()

◆ is_plus_zero()

◆ is_provably_nonneg()

◆ is_type_max()

◆ is_type_min()

◆ linearise_enclosing_indices()

◆ normalize_addressof_index()

◆ normalize_addressof_operands()

◆ obj_equals_addr_of()

◆ peel_pointer_offsets()

◆ ptr_subtype_resolvable()

◆ resolve_with_chain_lookup()

◆ same_value_and_sign()

◆ simplify_add_bv_identities()

◆ simplify_arith_1op()

◆ simplify_arith_2ops()

◆ simplify_associative_binary_op()

◆ simplify_constant_relation()

◆ simplify_floatbv_1op()

◆ simplify_floatbv_2ops()

◆ simplify_floatbv_relations()

◆ simplify_logic_2ops()

◆ simplify_object()

◆ simplify_pointer_add_const()

◆ simplify_pointer_cmp()

◆ simplify_relations()

◆ subscript_offset_in_units()

◆ symbol_is_own_object()

◆ try_simplification()

◆ typecast_check_return()

◆ widened_bool_compared_to_zero()