From 00fc8ea078e0cd2d250baf1a56dec8e301a83294 Mon Sep 17 00:00:00 2001 From: Michael Tautschnig Date: Tue, 22 Sep 2026 07:04:14 +0000 Subject: [PATCH] Fix semantics of onehot0: at most one bit set onehot0_exprt is meant to model SystemVerilog's $onehot0 (IEEE 1800-2017 20.9), which is true iff at most one bit of the operand is set, i.e., the operand is either one-hot or zero. The implementation (both the boolbv flattening and the lowering used by the SMT2 back-end) instead computed "exactly one bit is zero", i.e., onehot of the bitwise negation. Under an assumption $onehot0(x) this let a 4-bit x take the value 4'b1011. Fix the flattening, the lowering, and the class documentation, and correct the unit tests, which encoded the wrong semantics. onehot and onehot0 now differ exactly on the zero vector. Co-authored-by: Kiro --- src/solvers/flattening/boolbv_onehot.cpp | 15 ++++++++++----- src/util/bitvector_expr.cpp | 18 +++++++++++------- src/util/bitvector_expr.h | 4 +++- unit/solvers/flattening/boolbv_onehot.cpp | 22 ++++++++++++++++------ unit/util/bitvector_expr.cpp | 22 ++++++++++++++++------ 5 files changed, 56 insertions(+), 25 deletions(-) diff --git a/src/solvers/flattening/boolbv_onehot.cpp b/src/solvers/flattening/boolbv_onehot.cpp index 12679ed231c..7df8219892e 100644 --- a/src/solvers/flattening/boolbv_onehot.cpp +++ b/src/solvers/flattening/boolbv_onehot.cpp @@ -15,10 +15,6 @@ literalt boolbvt::convert_onehot(const unary_exprt &expr) bvt op=convert_bv(expr.op()); - // onehot0 is the same as onehot with the input bits flipped - if(expr.id() == ID_onehot0) - op = bv_utils.inverted(op); - literalt one_seen=const_literal(false); literalt more_than_one_seen=const_literal(false); @@ -29,5 +25,14 @@ literalt boolbvt::convert_onehot(const unary_exprt &expr) one_seen=prop.lor(*it, one_seen); } - return prop.land(one_seen, !more_than_one_seen); + if(expr.id() == ID_onehot) + { + // exactly one bit is set + return prop.land(one_seen, !more_than_one_seen); + } + else + { + // onehot0: at most one bit is set + return !more_than_one_seen; + } } diff --git a/src/util/bitvector_expr.cpp b/src/util/bitvector_expr.cpp index e578f52b6ea..c97adc2c433 100644 --- a/src/util/bitvector_expr.cpp +++ b/src/util/bitvector_expr.cpp @@ -307,7 +307,9 @@ exprt zero_extend_exprt::lower() const } } -static exprt onehot_lowering(const exprt &expr) +/// Returns a pair of expressions: the first is true iff at least one bit +/// of \p expr is set, the second is true iff more than one bit is set. +static std::pair onehot_lowering_helper(const exprt &expr) { exprt one_seen = false_exprt{}; const auto width = to_bitvector_type(expr.type()).get_width(); @@ -321,22 +323,24 @@ static exprt onehot_lowering(const exprt &expr) one_seen = or_exprt{one_seen, bit}; } - auto more_than_one_seen = disjunction(more_than_one_seen_disjuncts); - - return and_exprt{one_seen, not_exprt{more_than_one_seen}}; + return {one_seen, disjunction(more_than_one_seen_disjuncts)}; } exprt onehot_exprt::lower() const { auto symbol = symbol_exprt{"onehot-op", op().type()}; + auto [one_seen, more_than_one_seen] = onehot_lowering_helper(symbol); - return let_exprt{symbol, op(), onehot_lowering(symbol)}; + // exactly one bit is set + return let_exprt{ + symbol, op(), and_exprt{one_seen, not_exprt{more_than_one_seen}}}; } exprt onehot0_exprt::lower() const { auto symbol = symbol_exprt{"onehot-op", op().type()}; + auto [one_seen, more_than_one_seen] = onehot_lowering_helper(symbol); - // same as onehot, but on flipped operand bits - return let_exprt{symbol, bitnot_exprt{op()}, onehot_lowering(symbol)}; + // at most one bit is set + return let_exprt{symbol, op(), not_exprt{more_than_one_seen}}; } diff --git a/src/util/bitvector_expr.h b/src/util/bitvector_expr.h index b3dcb793602..d7502b307df 100644 --- a/src/util/bitvector_expr.h +++ b/src/util/bitvector_expr.h @@ -1936,7 +1936,9 @@ inline onehot_exprt &to_onehot_expr(exprt &expr) } /// \brief A Boolean expression returning true iff the given -/// operand consists of exactly one '0' and '1' otherwise. +/// operand contains at most one '1', i.e., the operand is either +/// one-hot or zero. This matches the semantics of SystemVerilog's +/// $onehot0. class onehot0_exprt : public unary_predicate_exprt { public: diff --git a/unit/solvers/flattening/boolbv_onehot.cpp b/unit/solvers/flattening/boolbv_onehot.cpp index 509652dfe39..ee37158cc1a 100644 --- a/unit/solvers/flattening/boolbv_onehot.cpp +++ b/unit/solvers/flattening/boolbv_onehot.cpp @@ -58,9 +58,9 @@ TEST_CASE("onehot flattening", "[core][solvers][flattening][boolbvt][onehot]") } } - GIVEN("A bit-vector that is one-hot 0") + GIVEN("A bit-vector that is one-hot") { - boolbv << onehot0_exprt{from_integer(0xfe, u8)}; + boolbv << onehot0_exprt{from_integer(64, u8)}; THEN("the lowering of onehot0 is true") { @@ -68,9 +68,19 @@ TEST_CASE("onehot flattening", "[core][solvers][flattening][boolbvt][onehot]") } } - GIVEN("A bit-vector that is not one-hot 0") + GIVEN("A bit-vector that is zero") { - boolbv << onehot0_exprt{from_integer(0x7e, u8)}; + boolbv << onehot0_exprt{from_integer(0, u8)}; + + THEN("the lowering of onehot0 is true") + { + REQUIRE(boolbv() == decision_proceduret::resultt::D_SATISFIABLE); + } + } + + GIVEN("A bit-vector with two bits set") + { + boolbv << onehot0_exprt{from_integer(5, u8)}; THEN("the lowering of onehot0 is false") { @@ -78,9 +88,9 @@ TEST_CASE("onehot flattening", "[core][solvers][flattening][boolbvt][onehot]") } } - GIVEN("A bit-vector that is not one-hot 0") + GIVEN("A bit-vector with all bits but one set") { - boolbv << onehot0_exprt{from_integer(0xff, u8)}; + boolbv << onehot0_exprt{from_integer(0xfe, u8)}; THEN("the lowering of onehot0 is false") { diff --git a/unit/util/bitvector_expr.cpp b/unit/util/bitvector_expr.cpp index 08555db0ad9..f0a53ea61d6 100644 --- a/unit/util/bitvector_expr.cpp +++ b/unit/util/bitvector_expr.cpp @@ -110,9 +110,9 @@ TEST_CASE("onehot expression lowering", "[core][util][expr]") } } - GIVEN("A bit-vector that is one-hot 0") + GIVEN("A bit-vector that is one-hot") { - boolbv << onehot0_exprt{from_integer(0xfe, u8)}.lower(); + boolbv << onehot0_exprt{from_integer(64, u8)}.lower(); THEN("the lowering of onehot0 is true") { @@ -120,9 +120,19 @@ TEST_CASE("onehot expression lowering", "[core][util][expr]") } } - GIVEN("A bit-vector that is not one-hot 0") + GIVEN("A bit-vector that is zero") { - boolbv << onehot0_exprt{from_integer(0x7e, u8)}.lower(); + boolbv << onehot0_exprt{from_integer(0, u8)}.lower(); + + THEN("the lowering of onehot0 is true") + { + REQUIRE(boolbv() == decision_proceduret::resultt::D_SATISFIABLE); + } + } + + GIVEN("A bit-vector with two bits set") + { + boolbv << onehot0_exprt{from_integer(5, u8)}.lower(); THEN("the lowering of onehot0 is false") { @@ -130,9 +140,9 @@ TEST_CASE("onehot expression lowering", "[core][util][expr]") } } - GIVEN("A bit-vector that is not one-hot 0") + GIVEN("A bit-vector with all bits but one set") { - boolbv << onehot0_exprt{from_integer(0xff, u8)}.lower(); + boolbv << onehot0_exprt{from_integer(0xfe, u8)}.lower(); THEN("the lowering of onehot0 is false") {