From 30d81d3cb933fb3730e4c0713a09bc126bc1cfd1 Mon Sep 17 00:00:00 2001 From: tryh4rd-26 Date: Mon, 11 May 2026 20:56:44 +0530 Subject: [PATCH] Fix FPA/BV model-validation soundness bug for Array + Datatype theories --- src/smt/smt_model_generator.cpp | 38 ++++++++----- src/smt/theory_fpa.cpp | 95 +++++++++++++++++++++++++++++++++ src/smt/theory_fpa.h | 18 ++++++- 3 files changed, 137 insertions(+), 14 deletions(-) diff --git a/src/smt/smt_model_generator.cpp b/src/smt/smt_model_generator.cpp index e49701a33..6df96b700 100644 --- a/src/smt/smt_model_generator.cpp +++ b/src/smt/smt_model_generator.cpp @@ -26,6 +26,7 @@ Revision History: #include "smt/smt_model_generator.h" #include "smt/proto_model/proto_model.h" #include "model/model_v2_pp.h" +#include "smt/theory_fpa.h" namespace smt { @@ -132,6 +133,11 @@ namespace smt { root2proc.insert(r, proc); } } + + theory * fpa_th = m_context->get_theory(m.mk_family_id("fpa")); + if (fpa_th) { + static_cast(fpa_th)->register_fpa2bv_processors(*this, root2proc, roots, procs); + } } model_value_proc* model_generator::mk_model_value(enode* r) { @@ -370,18 +376,22 @@ namespace smt { enode * child = d.get_enode(); TRACE(mg_top_sort, tout << "#" << n->get_owner_id() << " (" << mk_pp(n->get_expr(), m) << "): " << mk_pp(child->get_expr(), m) << " " << mk_pp(child->get_root()->get_expr(), m) << "\n";); - child = child->get_root(); - dependency_values.push_back(m_root2value[child]); - } - } - val = proc->mk_value(*this, dependency_values); - } - register_value(val); - m_asts.push_back(val); - m_root2value.insert(n, val); - } - } - // send model + child = child->get_root(); + app * child_val = nullptr; + m_root2value.find(child, child_val); + CTRACE("mg", !child_val, + tout << "null dependency value for: " << mk_pp(child->get_expr(), m) << "\n";); + dependency_values.push_back(child_val); + } + } + val = proc->mk_value(*this, dependency_values); + } + register_value(val); + m_asts.push_back(val); + m_root2value.insert(n, val); + } + } + // send model for (enode * n : m_context->enodes()) { if (is_uninterp_const(n->get_expr()) && m_context->is_relevant(n)) { func_decl * d = n->get_expr()->get_decl(); @@ -403,7 +413,9 @@ namespace smt { } app * model_generator::get_value(enode * n) const { - return m_root2value[n->get_root()]; + app * val = nullptr; + m_root2value.find(n->get_root(), val); + return val; } /** diff --git a/src/smt/theory_fpa.cpp b/src/smt/theory_fpa.cpp index ec64bfd61..3e5c7d2d7 100644 --- a/src/smt/theory_fpa.cpp +++ b/src/smt/theory_fpa.cpp @@ -647,6 +647,101 @@ namespace smt { } } + app * theory_fpa::fpa2bv_value_proc::mk_value(model_generator & mg, expr_ref_vector const & values) { + ast_manager & m = m_th.get_manager(); + fpa_util & fu = m_th.m_fpa_util; + bv_util & bu = m_th.m_bv_util; + context & ctx = m_th.get_context(); + + app * fpa_val = (values.empty() || !values[0]) ? nullptr : to_app(values[0]); + if (!fpa_val) { + if (!mg.get_root2value().find(m_fpa_n, fpa_val)) { + datatype_util dt(m); + expr * expr_n = m_fpa_n->get_expr(); + if (is_app(expr_n) && to_app(expr_n)->get_num_args() == 1) { + func_decl * f = to_app(expr_n)->get_decl(); + if (dt.is_accessor(f)) { + enode * arg_n = m_fpa_n->get_arg(0)->get_root(); + app * arg_val = nullptr; + if (mg.get_root2value().find(arg_n, arg_val)) { + if (dt.is_constructor(arg_val)) { + ptr_vector const * accessors = dt.get_constructor_accessors(arg_val->get_decl()); + if (accessors) { + for (unsigned i = 0; i < accessors->size(); ++i) { + if ((*accessors)[i] == f) { + expr * acc_val = arg_val->get_arg(i); + if (m.is_value(acc_val)) { + fpa_val = to_app(acc_val); + } + else if (is_app(acc_val) && ctx.e_internalized(acc_val)) { + enode * acc_n = ctx.get_enode(acc_val)->get_root(); + mg.get_root2value().find(acc_n, fpa_val); + } + break; + } + } + } + } + } + } + } + } + } + + if (!fpa_val) { + TRACE("fpa", tout << "fpa2bv_value_proc: defaulting to +0.0 for " << mk_pp(m_fpa_n->get_expr(), m) << "\n";); + fpa_val = fu.mk_pzero(m_ebits, m_sbits); + } + + scoped_mpf v(fu.fm()); + if (fu.is_numeral(fpa_val, v)) { + expr_ref result_fp(m); + m_th.m_converter.mk_numeral(fpa_val->get_sort(), v, result_fp); + if (fu.is_fp(result_fp)) { + expr * sgn = to_app(result_fp)->get_arg(0); + expr * exp = to_app(result_fp)->get_arg(1); + expr * sig = to_app(result_fp)->get_arg(2); + return bu.mk_concat(bu.mk_concat(sgn, exp), sig); + } + } + return bu.mk_numeral(0, m_ebits + m_sbits); + } + + void theory_fpa::register_fpa2bv_processors(model_generator & mg, obj_map & root2proc, ptr_vector & roots, ptr_vector & procs) { + for (auto const& kv : m_conversions) { + expr * fpa_expr = kv.m_key; + expr * bv_expr = kv.m_value; + if (ctx.e_internalized(fpa_expr) && ctx.e_internalized(bv_expr) && m_fpa_util.is_float(fpa_expr)) { + app_ref owner(m); + owner = get_ite_value(fpa_expr); + if (!owner || owner->get_family_id() == get_family_id()) + continue; + + enode * fpa_n = ctx.get_enode(fpa_expr)->get_root(); + enode * bv_n = ctx.get_enode(bv_expr)->get_root(); + + // if (!root2proc.contains(fpa_n)) + // continue; + + if (root2proc.contains(bv_n)) { + if (dynamic_cast(root2proc[bv_n])) + continue; + } + + unsigned ebits = m_fpa_util.get_ebits(fpa_expr->get_sort()); + unsigned sbits = m_fpa_util.get_sbits(fpa_expr->get_sort()); + model_value_proc * proc = alloc(fpa2bv_value_proc, this, ebits, sbits, fpa_n); + procs.push_back(proc); + + bool is_new = !root2proc.contains(bv_n); + root2proc.insert(bv_n, proc); + if (is_new) { + roots.push_back(bv_n); + } + } + } + } + void theory_fpa::display(std::ostream & out) const { diff --git a/src/smt/theory_fpa.h b/src/smt/theory_fpa.h index badce4e2a..a142c56bf 100644 --- a/src/smt/theory_fpa.h +++ b/src/smt/theory_fpa.h @@ -56,6 +56,22 @@ namespace smt { app * mk_value(model_generator & mg, expr_ref_vector const & values) override; }; + class fpa2bv_value_proc : public model_value_proc { + theory_fpa & m_th; + unsigned m_ebits; + unsigned m_sbits; + enode * m_fpa_n; + public: + fpa2bv_value_proc(theory_fpa * th, unsigned ebits, unsigned sbits, enode * fpa_n) : + m_th(*th), m_ebits(ebits), m_sbits(sbits), m_fpa_n(fpa_n) {} + + void get_dependencies(buffer & result) override { + result.push_back(model_value_dependency(m_fpa_n)); + } + + app * mk_value(model_generator & mg, expr_ref_vector const & values) override; + }; + class fpa_rm_value_proc : public model_value_proc { theory_fpa & m_th; ast_manager & m; @@ -110,6 +126,7 @@ namespace smt { public: theory_fpa(context& ctx); + void register_fpa2bv_processors(model_generator & mg, obj_map & root2proc, ptr_vector & roots, ptr_vector & procs); ~theory_fpa() override; void display(std::ostream & out) const override; @@ -127,4 +144,3 @@ namespace smt { }; }; -