From bf9230427e62dc64a74226159bac868a59c1c769 Mon Sep 17 00:00:00 2001 From: Michael Tautschnig Date: Fri, 17 Jul 2026 13:35:51 +0000 Subject: [PATCH] Emit SMT object properties in deterministic order The incremental SMT2 decision procedure emitted size_of_object and is_dynamic_object definitions by directly iterating the object map, which is an unordered map keyed by the objects' base expressions. The emission order therefore depended on expression hash values, which vary across platforms and configurations. For example, whether plain char is signed or unsigned changes the hashes of char-typed base expressions, reordering the emitted assertions and thereby producing textually different SMT problems for semantically identical inputs. Such differences needlessly perturb solver heuristics and defeat byte-for-byte comparison of generated formulas across platforms (a milder relative of the cross-platform instability discussed in https://github.com/diffblue/cbmc/issues/8991). Sort the objects by their unique identifier before emitting their property definitions, so that the solver receives them in a stable order independent of hash values. The unit test that previously had to compare the sent commands as an unordered collection now requires the exact deterministic sequence. Co-authored-by: Kiro --- .../smt2_incremental_decision_procedure.cpp | 30 +++++++++++++++---- .../smt2_incremental_decision_procedure.cpp | 14 ++------- 2 files changed, 26 insertions(+), 18 deletions(-) diff --git a/src/solvers/smt2_incremental/smt2_incremental_decision_procedure.cpp b/src/solvers/smt2_incremental/smt2_incremental_decision_procedure.cpp index 2817ba012fe..968d9a7265f 100644 --- a/src/solvers/smt2_incremental/smt2_incremental_decision_procedure.cpp +++ b/src/solvers/smt2_incremental/smt2_incremental_decision_procedure.cpp @@ -24,8 +24,10 @@ #include #include +#include #include #include +#include /// Issues a command to the solving process which is expected to optionally /// return a success status followed by the actual response of interest. @@ -706,18 +708,34 @@ lookup_decision_procedure_result( void smt2_incremental_decision_proceduret::define_object_properties() { object_properties_defined.resize(object_map.size()); + // The object map is an unordered map, whose iteration order depends on the + // hash values of the object base expressions. These hashes may differ + // across platforms and toolchains, for example when the signedness of + // `char` differs. Establish a deterministic ordering based on the objects' + // unique identifiers before emitting the definitions, so that the solver + // receives them in a stable order. + std::vector objects; + objects.reserve(object_map.size()); for(const auto &key_value : object_map) + objects.push_back(&key_value.second); + std::sort( + objects.begin(), + objects.end(), + []( + const decision_procedure_objectt *left, + const decision_procedure_objectt *right) + { return left->unique_id < right->unique_id; }); + for(const decision_procedure_objectt *object : objects) { - const decision_procedure_objectt &object = key_value.second; - if(object_properties_defined[object.unique_id]) + if(object_properties_defined[object->unique_id]) continue; else - object_properties_defined[object.unique_id] = true; - define_dependent_functions(object.size); + object_properties_defined[object->unique_id] = true; + define_dependent_functions(object->size); solver_process->send(object_size_function.make_definition( - object.unique_id, convert_expr_to_smt(object.size))); + object->unique_id, convert_expr_to_smt(object->size))); solver_process->send(is_dynamic_object_function.make_definition( - object.unique_id, object.is_dynamic)); + object->unique_id, object->is_dynamic)); } } diff --git a/unit/solvers/smt2_incremental/smt2_incremental_decision_procedure.cpp b/unit/solvers/smt2_incremental/smt2_incremental_decision_procedure.cpp index 5fd0a855875..6462f1bb43c 100644 --- a/unit/solvers/smt2_incremental/smt2_incremental_decision_procedure.cpp +++ b/unit/solvers/smt2_incremental/smt2_incremental_decision_procedure.cpp @@ -480,22 +480,12 @@ TEST_CASE( std::vector expected_commands{ smt_declare_function_commandt{foo_term, {}}, smt_assert_commandt{smt_core_theoryt::equal(foo_term, term_42)}, - invalid_pointer_object_size_definition, null_object_size_definition, null_object_dynamic_definition, + invalid_pointer_object_size_definition, invalid_pointer_object_dynamic_definition, smt_check_sat_commandt{}}; - REQUIRE( - (test.sent_commands.size() == expected_commands.size() && - std::all_of( - expected_commands.begin(), - expected_commands.end(), - [&](const smt_commandt &command) -> bool { - return std::find( - test.sent_commands.begin(), - test.sent_commands.end(), - command) != test.sent_commands.end(); - }))); + REQUIRE(test.sent_commands == expected_commands); SECTION("Get \"foo\" value back") { test.sent_commands.clear();