From 4700fa7764f7eacc794115683e91903942ef84f8 Mon Sep 17 00:00:00 2001 From: Daniel Kroening Date: Thu, 16 Jan 2025 13:29:36 -0800 Subject: [PATCH] BMC: return property handles/literals The property handles/literals for the BMC time frames are now returned as return values, as opposed to being returned via a reference. This removes the ambiguity about what should happen when there are values in those vectors prior to the call. --- src/ebmc/bdd_engine.cpp | 4 ++-- src/ebmc/bmc.cpp | 9 ++------- src/ebmc/cegar/bmc_cegar.cpp | 2 +- src/ebmc/property_checker.cpp | 4 ++-- src/trans-netlist/unwind_netlist.cpp | 9 +++++---- src/trans-netlist/unwind_netlist.h | 5 +---- src/trans-word-level/property.cpp | 9 +++++---- src/trans-word-level/property.h | 3 +-- 8 files changed, 19 insertions(+), 26 deletions(-) diff --git a/src/ebmc/bdd_engine.cpp b/src/ebmc/bdd_engine.cpp index bb51b4788..c98d26c4a 100644 --- a/src/ebmc/bdd_engine.cpp +++ b/src/ebmc/bdd_engine.cpp @@ -409,8 +409,8 @@ void bdd_enginet::compute_counterexample( auto netlist_property = netlist.properties.find(property.identifier); CHECK_RETURN(netlist_property != netlist.properties.end()); - ::unwind_property( - netlist_property->second, bmc_map, property.timeframe_literals); + property.timeframe_literals = + ::unwind_property(netlist_property->second, bmc_map); // we need the propertyt to fail in one of the timeframes bvt clause=property.timeframe_literals; diff --git a/src/ebmc/bmc.cpp b/src/ebmc/bmc.cpp index ac60a9816..6b39e0fe4 100644 --- a/src/ebmc/bmc.cpp +++ b/src/ebmc/bmc.cpp @@ -230,13 +230,8 @@ property_checker_resultt bmc( continue; } - ::property( - property.normalized_expr, - property.timeframe_handles, - message_handler, - solver, - bound + 1, - ns); + property.timeframe_handles = ::property( + property.normalized_expr, message_handler, solver, bound + 1, ns); // If it's an assumption, then add it as constraint. if(property.is_assumed()) diff --git a/src/ebmc/cegar/bmc_cegar.cpp b/src/ebmc/cegar/bmc_cegar.cpp index dfd8db4e1..5ef020bd9 100644 --- a/src/ebmc/cegar/bmc_cegar.cpp +++ b/src/ebmc/cegar/bmc_cegar.cpp @@ -78,7 +78,7 @@ void bmc_cegart::unwind( for(auto &property_it : netlist.properties) { auto &prop_bv = prop_bv_map[property_it.first]; - unwind_property(property_it.second, bmc_map, prop_bv); + prop_bv = unwind_property(property_it.second, bmc_map); disjuncts.push_back(!solver.land(prop_bv)); } diff --git a/src/ebmc/property_checker.cpp b/src/ebmc/property_checker.cpp index 8b6bddae1..c748f81ba 100644 --- a/src/ebmc/property_checker.cpp +++ b/src/ebmc/property_checker.cpp @@ -257,8 +257,8 @@ property_checker_resultt bit_level_bmc( auto netlist_property = netlist.properties.find(property.identifier); CHECK_RETURN(netlist_property != netlist.properties.end()); - ::unwind_property( - netlist_property->second, bmc_map, property.timeframe_literals); + property.timeframe_literals = + ::unwind_property(netlist_property->second, bmc_map); if(property.is_assumed()) { diff --git a/src/trans-netlist/unwind_netlist.cpp b/src/trans-netlist/unwind_netlist.cpp index d52c067c8..490f03680 100644 --- a/src/trans-netlist/unwind_netlist.cpp +++ b/src/trans-netlist/unwind_netlist.cpp @@ -141,21 +141,22 @@ Function: unwind_property \*******************************************************************/ -void unwind_property( +bvt unwind_property( const netlistt::propertyt &property, - const bmc_mapt &bmc_map, - bvt &prop_bv) + const bmc_mapt &bmc_map) { PRECONDITION(std::holds_alternative(property)); auto property_node = std::get(property).p; - prop_bv.resize(bmc_map.timeframe_map.size()); + bvt prop_bv{bmc_map.timeframe_map.size()}; for(std::size_t t = 0; t < bmc_map.timeframe_map.size(); t++) { literalt l=bmc_map.translate(t, property_node); prop_bv[t]=l; } + + return prop_bv; } /*******************************************************************\ diff --git a/src/trans-netlist/unwind_netlist.h b/src/trans-netlist/unwind_netlist.h index 5d01b081a..b3fb46028 100644 --- a/src/trans-netlist/unwind_netlist.h +++ b/src/trans-netlist/unwind_netlist.h @@ -36,9 +36,6 @@ void unwind( bool netlist_bmc_supports_property(const class exprt &); // unwind a netlist property -void unwind_property( - const netlistt::propertyt &, - const bmc_mapt &, - bvt &prop_bv); +bvt unwind_property(const netlistt::propertyt &, const bmc_mapt &); #endif diff --git a/src/trans-word-level/property.cpp b/src/trans-word-level/property.cpp index 70acd2fb2..8889a8765 100644 --- a/src/trans-word-level/property.cpp +++ b/src/trans-word-level/property.cpp @@ -682,9 +682,8 @@ Function: property \*******************************************************************/ -void property( +exprt::operandst property( const exprt &property_expr, - exprt::operandst &prop_handles, message_handlert &message_handler, decision_proceduret &solver, std::size_t no_timeframes, @@ -696,8 +695,8 @@ void property( auto obligations = property_obligations(property_expr, no_timeframes); // Map obligations onto timeframes. - prop_handles.clear(); - prop_handles.resize(no_timeframes, true_exprt()); + exprt::operandst prop_handles{no_timeframes, true_exprt()}; + for(auto &obligation_it : obligations.map) { auto t = obligation_it.first; @@ -706,4 +705,6 @@ void property( auto t_int = numeric_cast_v(t); prop_handles[t_int] = solver.handle(conjunction(obligation_it.second)); } + + return prop_handles; } diff --git a/src/trans-word-level/property.h b/src/trans-word-level/property.h index 1bff3522b..64d6feaef 100644 --- a/src/trans-word-level/property.h +++ b/src/trans-word-level/property.h @@ -16,9 +16,8 @@ Author: Daniel Kroening, kroening@kroening.com #include -void property( +exprt::operandst property( const exprt &property_expr, - exprt::operandst &prop_handles, message_handlert &, decision_proceduret &solver, std::size_t no_timeframes,