Module normalize 

Structs

ConstraintContext 🔒

Simple facts learned from the normalized conjunction currently being queried.

Functions

add_cannot_overflow_256 🔒

Returns whether unsigned addition of two expressions cannot overflow 256 bits.

add_overflow_check 🔒

Returns whether left > left + increment is an impossible overflow check.

add_with_operand 🔒

Returns the operands if expr is an addition involving operand.

bool_contains_udiv 🔒

Returns whether a boolean expression syntactically contains unsigned division.

bool_from_word_expr 🔒

Extracts the boolean condition represented by a word-valued 0/1 expression.

collect_normalized_conjunct 🔒

collect_or_terms 🔒

Flattens nested bitwise-OR expressions into their leaf terms.

expr_contains_udiv 🔒

Returns whether a word expression syntactically contains unsigned division.

expr_unsigned_bits 🔒

Returns a conservative unsigned bit-width upper bound for an expression.

extracted_shifted_byte_term 🔒

Returns the source word and byte index for one shifted extracted-byte term.

extracted_unshifted_byte_source 🔒

Returns the source word for an unshifted byte extraction at index.

guarded_self_div_word_condition 🔒

Returns the boolean represented by a == 0 ? 0 : a / a.

mul_cannot_overflow_256 🔒

Returns whether unsigned multiplication of two expressions cannot overflow 256 bits.

normalize_add_overflow_cmp_for_solver 🔒

Rewrites exact unsigned-addition overflow checks when operand bounds preclude overflow.

normalize_bool_for_solver 🔒

Normalizes one boolean expression into an equivalent, solver-friendlier form.

normalize_constraint_batch 🔒

normalize_constraints_for_solver 🔒

Normalizes path constraints into an equivalent, solver-friendlier form.

normalize_expr_eq_zero_for_solver 🔒

Rewrites expr == 0 when expr contains exactly-normalizable unsigned division.

normalize_expr_for_solver 🔒

Normalizes one word expression into an equivalent, solver-friendlier form.

normalize_expr_ne_zero_for_solver 🔒

Rewrites expr != 0 when expr contains exactly-normalizable unsigned division.

normalize_ite_expr_for_solver 🔒

Normalizes a word-valued conditional expression.

normalize_udiv_bool_for_solver 🔒

Rewrites exact EVM unsigned-division zero/nonzero predicates without bvudiv.

normalize_udiv_cmp_for_solver 🔒

Rewrites udiv(a, b) zero/nonzero comparisons using EVM division-by-zero semantics.

normalize_udiv_eq_zero 🔒

Rewrites udiv(a, b) == 0 predicates using EVM division-by-zero semantics.

rebuild_word_from_extracted_byte_terms 🔒

Rebuilds a word from OR-ed byte-extraction terms when the source is recoverable.

self_div_expr_matches_zero_check 🔒

Returns whether expr is a / a for the operand guarded by cond.

udiv_nonzero_condition 🔒

Builds the exact condition for EVM udiv(numerator, denominator) != 0.

udiv_operands 🔒

Returns the operands for an unsigned division expression.

udiv_zero_condition 🔒

Builds the exact condition for EVM udiv(numerator, denominator) == 0.

word_bool_always_true 🔒

Returns whether a word-valued boolean expression is an exact tautology.

word_bool_term 🔒

Converts one 0/1 word boolean term into its boolean condition.

word_from_bool_expr 🔒

Converts a boolean condition into its 0/1 word representation.

zero_check_operand 🔒

Returns the operand tested by operand == 0.