- Generated by
1.15.0
|
ESBMC
Efficient SMT-based Context-Bounded Model Checker
|
Encapsulates the integer-encoding IEEE 754 path (–int-encoding –ir-ieee). More...
#include <ir_ieee_conv.h>
Classes | |
| struct | ra_interval_t |
| Interval [lo, hi] in the real-arithmetic SMT encoding. More... | |
Public Member Functions | |
| ir_ieee_convt (smt_solver_baset *ctx) | |
| void | propagate_interval (smt_astt lhs, smt_astt rhs) |
| Propagate interval metadata from rhs to lhs after an SSA assignment. | |
| void | assert_symbol_range (const std::string &name, smt_astt sym_ast, const symbol2t &sym) |
| Assert C integer type range for narrow symbols (width < 32 bits). | |
| void | assert_representable_magnitude (smt_astt sym_ast, const floatbv_type2t &fbv_type) |
| Assert that a float symbol's real value is representable: every finite value has magnitude at most max_normal, and the only magnitude above it is the infinity sentinel that arithmetic saturates to on overflow. | |
| ra_interval_t | get_interval (smt_astt t) const |
| Look up the tracked interval for t; fall back to the point interval {t, t}. | |
| void | store_interval (smt_astt t, smt_astt lo, smt_astt hi) |
| Store an interval for t in the map. | |
| smt_astt | encode_ieee_add (const expr2tc &expr) |
| Integer-encoding path for ieee_add. | |
| smt_astt | encode_ieee_sub (const expr2tc &expr) |
| Integer-encoding path for ieee_sub. | |
| smt_astt | encode_ieee_mul (const expr2tc &expr) |
| Integer-encoding path for ieee_mul. | |
| smt_astt | encode_ieee_div (const expr2tc &expr) |
| Integer-encoding path for ieee_div. | |
| smt_astt | encode_ieee_fma (const expr2tc &expr) |
| Integer-encoding path for ieee_fma (fused multiply-add). | |
| smt_astt | encode_ieee_rem (const expr2tc &expr) |
| Encode ieee_rem2t (IEEE 754 remainder, C's remainder()). | |
| void | store_nan_pred (smt_astt t, smt_astt nan_pred) |
| Record that the SMT AST t may be NaN; nan_pred is a boolean SMT term that is true iff t holds a NaN value (e.g. | |
| smt_astt | get_nan_pred (smt_astt t) const |
| Return the stored NaN predicate for t, or nullptr if none is known. | |
| void | propagate_nan_pred (smt_astt lhs, smt_astt rhs) |
| Propagate a NaN predicate from rhs to lhs after an SSA assignment. | |
| smt_astt | apply_nan_cmp (smt_astt cmp, smt_astt a, smt_astt b, bool is_neq) |
| Wrap a comparison result with IEEE NaN semantics. | |
| smt_astt | combine_nan_preds (smt_astt a, smt_astt b) const |
| Combine two NaN predicates with OR. | |
| void | store_neg_zero_pred (smt_astt t, smt_astt neg_zero_pred) |
| Record a predicate that is true iff the SMT AST t represents IEEE 754 -0.0. | |
| smt_astt | get_neg_zero_pred (smt_astt t) const |
| Return the stored negative-zero predicate for t, or nullptr if no negative-zero metadata is recorded for t. | |
| void | propagate_neg_zero_pred (smt_astt lhs, smt_astt rhs) |
| Propagate a negative-zero predicate from rhs to lhs after an SSA assignment. | |
| void | propagate_neg_zero_through_ite (smt_astt outer, smt_astt inner, smt_astt guard) |
| Re-attach inner's negative-zero predicate (if any) to outer, guarded by guard (the condition under which outer actually evaluates to inner). | |
| std::pair< smt_astt, smt_astt > | apply_ieee754_rne_enclosure (smt_astt real_result, smt_astt lo_r, smt_astt hi_r, const floatbv_type2t &fbv_type) |
| Interval-lifted RNE enclosure helper. | |
| std::pair< smt_astt, smt_astt > | apply_ieee754_rna_enclosure (smt_astt real_result, smt_astt lo_r, smt_astt hi_r, const floatbv_type2t &fbv_type) |
| Interval-lifted RNA enclosure helper (round-to-nearest-away). | |
| std::pair< smt_astt, smt_astt > | apply_ieee754_rup_enclosure (smt_astt real_result, smt_astt lo_r, smt_astt hi_r, const floatbv_type2t &fbv_type) |
| Interval-lifted RUP enclosure helper (round-to-plus-infinity). | |
| std::pair< smt_astt, smt_astt > | apply_ieee754_rdn_enclosure (smt_astt real_result, smt_astt lo_r, smt_astt hi_r, const floatbv_type2t &fbv_type) |
| Interval-lifted RDN enclosure helper (round-to-minus-infinity). | |
| std::pair< smt_astt, smt_astt > | apply_ieee754_rtz_enclosure (smt_astt real_result, smt_astt lo_r, smt_astt hi_r, const floatbv_type2t &fbv_type) |
| Interval-lifted RTZ enclosure helper (round-to-zero / truncation). | |
Encapsulates the integer-encoding IEEE 754 path (–int-encoding –ir-ieee).
All state that belongs solely to this encoding is kept here, away from the main smt_solver_baset class:
smt_solver_baset holds a pointer to this class (ir_ieee_api) and delegates the int_encoding branch of each ieee_*_id switch case to the corresponding encode_ieee_* method. The sqrt case and apply_ieee754_semantics remain in smt_solver_baset and call back into this class via ir_ieee_api.
|
explicit |
| std::pair< smt_astt, smt_astt > ir_ieee_convt::apply_ieee754_rdn_enclosure | ( | smt_astt | real_result, |
| smt_astt | lo_r, | ||
| smt_astt | hi_r, | ||
| const floatbv_type2t & | fbv_type ) |
Interval-lifted RDN enclosure helper (round-to-minus-infinity).
| std::pair< smt_astt, smt_astt > ir_ieee_convt::apply_ieee754_rna_enclosure | ( | smt_astt | real_result, |
| smt_astt | lo_r, | ||
| smt_astt | hi_r, | ||
| const floatbv_type2t & | fbv_type ) |
Interval-lifted RNA enclosure helper (round-to-nearest-away).
| std::pair< smt_astt, smt_astt > ir_ieee_convt::apply_ieee754_rne_enclosure | ( | smt_astt | real_result, |
| smt_astt | lo_r, | ||
| smt_astt | hi_r, | ||
| const floatbv_type2t & | fbv_type ) |
Interval-lifted RNE enclosure helper.
Input: exact real result and pre-computed interval endpoints [lo_r, hi_r]. Returns {ra_lo, ra_hi} for storage in the interval map.
| std::pair< smt_astt, smt_astt > ir_ieee_convt::apply_ieee754_rtz_enclosure | ( | smt_astt | real_result, |
| smt_astt | lo_r, | ||
| smt_astt | hi_r, | ||
| const floatbv_type2t & | fbv_type ) |
Interval-lifted RTZ enclosure helper (round-to-zero / truncation).
| std::pair< smt_astt, smt_astt > ir_ieee_convt::apply_ieee754_rup_enclosure | ( | smt_astt | real_result, |
| smt_astt | lo_r, | ||
| smt_astt | hi_r, | ||
| const floatbv_type2t & | fbv_type ) |
Interval-lifted RUP enclosure helper (round-to-plus-infinity).
Wrap a comparison result with IEEE NaN semantics.
If either operand has a known NaN predicate, returns ite(nan_pred, is_neq, cmp) so that ordered comparisons (is_neq=false) evaluate to false when either operand is NaN, and != (is_neq=true) evaluates to true. Returns cmp unchanged when no NaN predicate is known.
| void ir_ieee_convt::assert_representable_magnitude | ( | smt_astt | sym_ast, |
| const floatbv_type2t & | fbv_type ) |
Assert that a float symbol's real value is representable: every finite value has magnitude at most max_normal, and the only magnitude above it is the infinity sentinel that arithmetic saturates to on overflow.
Called from smt_solver_baset::convert_terminal for symbol_id.
| void ir_ieee_convt::assert_symbol_range | ( | const std::string & | name, |
| smt_astt | sym_ast, | ||
| const symbol2t & | sym ) |
Assert C integer type range for narrow symbols (width < 32 bits).
Called from smt_solver_baset::convert_terminal for symbol_id.
Combine two NaN predicates with OR.
Returns nullptr if neither is set; the non-null one if only one is set; mk_or(a, b) if both are set.
Integer-encoding path for ieee_fma (fused multiply-add).
Encode ieee_rem2t (IEEE 754 remainder, C's remainder()).
Exact, so no rounding, enclosure or flush; r is pinned as x - n*y through a fresh integer n nearest x/y, even on ties.
| ir_ieee_convt::ra_interval_t ir_ieee_convt::get_interval | ( | smt_astt | t | ) | const |
Look up the tracked interval for t; fall back to the point interval {t, t}.
Used by both encode_ieee_* methods and the sqrt case in smt_solver.cpp.
Return the stored NaN predicate for t, or nullptr if none is known.
Return the stored negative-zero predicate for t, or nullptr if no negative-zero metadata is recorded for t.
Propagate interval metadata from rhs to lhs after an SSA assignment.
Called from smt_solver_baset::convert_assign.
Propagate a NaN predicate from rhs to lhs after an SSA assignment.
Called from smt_solver_baset::convert_assign alongside propagate_interval.
Propagate a negative-zero predicate from rhs to lhs after an SSA assignment.
Called from smt_solver_baset::convert_assign alongside propagate_interval and propagate_nan_pred.
One-way: if rhs carries no predicate, any existing entry already recorded for lhs is left in place rather than cleared. This is harmless under SSA, where each assignment gives lhs a fresh AST with no prior entry of its own, but callers reusing an AST across more than one assignment should not assume this clears stale metadata.
| void ir_ieee_convt::propagate_neg_zero_through_ite | ( | smt_astt | outer, |
| smt_astt | inner, | ||
| smt_astt | guard ) |
Re-attach inner's negative-zero predicate (if any) to outer, guarded by guard (the condition under which outer actually evaluates to inner).
Must be used whenever a term that may carry negative-zero metadata is wrapped in a further SMT term such as an ite – e.g. encode_ieee_div's div-by-zero selection – since the metadata map is keyed by AST pointer and the wrapper is a different pointer from inner, so a lookup on the wrapper alone would silently miss it.
Store an interval for t in the map.
Used by both encode_ieee_* methods and the sqrt case in smt_solver.cpp.
Record that the SMT AST t may be NaN; nan_pred is a boolean SMT term that is true iff t holds a NaN value (e.g.
not(operand >= 0) for sqrt with a negative operand).
Record a predicate that is true iff the SMT AST t represents IEEE 754 -0.0.
Such predicates originate when a negative subnormal-range result is flushed to zero and when a literal negative-zero float constant is converted, and may subsequently be propagated through assignments or wrapper terms. This does not implement general signed-zero semantics.
1.15.0