Skip to content

Commit a3e1411

Browse files
thomasspriggsthomasspriggs
authored
Merge pull request #6669 from thomasspriggs/tas/smt_bv_functions_completion
Add remaining SMT bv functions to theory
2 parents c558465 + e59a77c commit a3e1411

File tree

3 files changed

+347
-0
lines changed

3 files changed

+347
-0
lines changed

‎src/solvers/smt2_incremental/smt_bit_vector_theory.cpp‎

Lines changed: 165 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -245,6 +245,28 @@ void smt_bit_vector_theoryt::xnort::validate(
245245
const smt_function_application_termt::factoryt<smt_bit_vector_theoryt::xnort>
246246
smt_bit_vector_theoryt::xnor{};
247247

248+
const char *smt_bit_vector_theoryt::comparet::identifier()
249+
{
250+
return "bvcomp";
251+
}
252+
253+
smt_sortt smt_bit_vector_theoryt::comparet::return_sort(
254+
const smt_termt &lhs,
255+
const smt_termt &rhs)
256+
{
257+
return smt_bit_vector_sortt{1};
258+
}
259+
260+
void smt_bit_vector_theoryt::comparet::validate(
261+
const smt_termt &lhs,
262+
const smt_termt &rhs)
263+
{
264+
validate_matched_bit_vector_sorts(lhs, rhs);
265+
}
266+
267+
const smt_function_application_termt::factoryt<smt_bit_vector_theoryt::comparet>
268+
smt_bit_vector_theoryt::compare{};
269+
248270
// Relational operator definitions
249271

250272
const char *smt_bit_vector_theoryt::unsigned_less_thant::identifier()
@@ -678,3 +700,146 @@ void smt_bit_vector_theoryt::arithmetic_shift_rightt::validate(
678700
const smt_function_application_termt::factoryt<
679701
smt_bit_vector_theoryt::arithmetic_shift_rightt>
680702
smt_bit_vector_theoryt::arithmetic_shift_right{};
703+
704+
const char *smt_bit_vector_theoryt::repeatt::identifier()
705+
{
706+
return "repeat";
707+
}
708+
709+
smt_sortt
710+
smt_bit_vector_theoryt::repeatt::return_sort(const smt_termt &operand) const
711+
{
712+
const std::size_t operand_width =
713+
operand.get_sort().cast<smt_bit_vector_sortt>()->bit_width();
714+
return smt_bit_vector_sortt{i * operand_width};
715+
}
716+
717+
std::vector<smt_indext> smt_bit_vector_theoryt::repeatt::indices() const
718+
{
719+
return {smt_numeral_indext{i}};
720+
}
721+
722+
void smt_bit_vector_theoryt::repeatt::validate(const smt_termt &operand) const
723+
{
724+
PRECONDITION(i >= 1);
725+
PRECONDITION(operand.get_sort().cast<smt_bit_vector_sortt>());
726+
}
727+
728+
smt_function_application_termt::factoryt<smt_bit_vector_theoryt::repeatt>
729+
smt_bit_vector_theoryt::repeat(std::size_t i)
730+
{
731+
PRECONDITION(i >= 1);
732+
return smt_function_application_termt::factoryt<repeatt>(i);
733+
}
734+
735+
const char *smt_bit_vector_theoryt::zero_extendt::identifier()
736+
{
737+
return "zero_extend";
738+
}
739+
740+
smt_sortt smt_bit_vector_theoryt::zero_extendt::return_sort(
741+
const smt_termt &operand) const
742+
{
743+
const std::size_t operand_width =
744+
operand.get_sort().cast<smt_bit_vector_sortt>()->bit_width();
745+
return smt_bit_vector_sortt{i + operand_width};
746+
}
747+
748+
std::vector<smt_indext> smt_bit_vector_theoryt::zero_extendt::indices() const
749+
{
750+
return {smt_numeral_indext{i}};
751+
}
752+
753+
void smt_bit_vector_theoryt::zero_extendt::validate(const smt_termt &operand)
754+
{
755+
PRECONDITION(operand.get_sort().cast<smt_bit_vector_sortt>());
756+
}
757+
758+
smt_function_application_termt::factoryt<smt_bit_vector_theoryt::zero_extendt>
759+
smt_bit_vector_theoryt::zero_extend(std::size_t i)
760+
{
761+
return smt_function_application_termt::factoryt<zero_extendt>(i);
762+
}
763+
764+
const char *smt_bit_vector_theoryt::sign_extendt::identifier()
765+
{
766+
return "sign_extend";
767+
}
768+
769+
smt_sortt smt_bit_vector_theoryt::sign_extendt::return_sort(
770+
const smt_termt &operand) const
771+
{
772+
const std::size_t operand_width =
773+
operand.get_sort().cast<smt_bit_vector_sortt>()->bit_width();
774+
return smt_bit_vector_sortt{i + operand_width};
775+
}
776+
777+
std::vector<smt_indext> smt_bit_vector_theoryt::sign_extendt::indices() const
778+
{
779+
return {smt_numeral_indext{i}};
780+
}
781+
782+
void smt_bit_vector_theoryt::sign_extendt::validate(const smt_termt &operand)
783+
{
784+
PRECONDITION(operand.get_sort().cast<smt_bit_vector_sortt>());
785+
}
786+
787+
smt_function_application_termt::factoryt<smt_bit_vector_theoryt::sign_extendt>
788+
smt_bit_vector_theoryt::sign_extend(std::size_t i)
789+
{
790+
return smt_function_application_termt::factoryt<sign_extendt>(i);
791+
}
792+
793+
const char *smt_bit_vector_theoryt::rotate_leftt::identifier()
794+
{
795+
return "rotate_left";
796+
}
797+
798+
smt_sortt
799+
smt_bit_vector_theoryt::rotate_leftt::return_sort(const smt_termt &operand)
800+
{
801+
return operand.get_sort();
802+
}
803+
804+
std::vector<smt_indext> smt_bit_vector_theoryt::rotate_leftt::indices() const
805+
{
806+
return {smt_numeral_indext{i}};
807+
}
808+
809+
void smt_bit_vector_theoryt::rotate_leftt::validate(const smt_termt &operand)
810+
{
811+
PRECONDITION(operand.get_sort().cast<smt_bit_vector_sortt>());
812+
}
813+
814+
smt_function_application_termt::factoryt<smt_bit_vector_theoryt::rotate_leftt>
815+
smt_bit_vector_theoryt::rotate_left(std::size_t i)
816+
{
817+
return smt_function_application_termt::factoryt<rotate_leftt>(i);
818+
}
819+
820+
const char *smt_bit_vector_theoryt::rotate_rightt::identifier()
821+
{
822+
return "rotate_right";
823+
}
824+
825+
smt_sortt
826+
smt_bit_vector_theoryt::rotate_rightt::return_sort(const smt_termt &operand)
827+
{
828+
return operand.get_sort();
829+
}
830+
831+
std::vector<smt_indext> smt_bit_vector_theoryt::rotate_rightt::indices() const
832+
{
833+
return {smt_numeral_indext{i}};
834+
}
835+
836+
void smt_bit_vector_theoryt::rotate_rightt::validate(const smt_termt &operand)
837+
{
838+
PRECONDITION(operand.get_sort().cast<smt_bit_vector_sortt>());
839+
}
840+
841+
smt_function_application_termt::factoryt<smt_bit_vector_theoryt::rotate_rightt>
842+
smt_bit_vector_theoryt::rotate_right(std::size_t i)
843+
{
844+
return smt_function_application_termt::factoryt<rotate_rightt>(i);
845+
}

‎src/solvers/smt2_incremental/smt_bit_vector_theory.h‎

Lines changed: 63 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -85,6 +85,14 @@ class smt_bit_vector_theoryt
8585
};
8686
static const smt_function_application_termt::factoryt<xnort> xnor;
8787

88+
struct comparet final
89+
{
90+
static const char *identifier();
91+
static smt_sortt return_sort(const smt_termt &lhs, const smt_termt &rhs);
92+
static void validate(const smt_termt &lhs, const smt_termt &rhs);
93+
};
94+
static const smt_function_application_termt::factoryt<comparet> compare;
95+
8896
// Relational operator class declarations
8997
struct unsigned_less_thant final
9098
{
@@ -256,6 +264,61 @@ class smt_bit_vector_theoryt
256264
};
257265
static const smt_function_application_termt::factoryt<arithmetic_shift_rightt>
258266
arithmetic_shift_right;
267+
268+
struct repeatt final
269+
{
270+
std::size_t i;
271+
static const char *identifier();
272+
smt_sortt return_sort(const smt_termt &operand) const;
273+
std::vector<smt_indext> indices() const;
274+
void validate(const smt_termt &operand) const;
275+
};
276+
static smt_function_application_termt::factoryt<repeatt>
277+
repeat(std::size_t i);
278+
279+
struct zero_extendt final
280+
{
281+
std::size_t i;
282+
static const char *identifier();
283+
smt_sortt return_sort(const smt_termt &operand) const;
284+
std::vector<smt_indext> indices() const;
285+
static void validate(const smt_termt &operand);
286+
};
287+
static smt_function_application_termt::factoryt<zero_extendt>
288+
zero_extend(std::size_t i);
289+
290+
struct sign_extendt final
291+
{
292+
std::size_t i;
293+
static const char *identifier();
294+
smt_sortt return_sort(const smt_termt &operand) const;
295+
std::vector<smt_indext> indices() const;
296+
static void validate(const smt_termt &operand);
297+
};
298+
static smt_function_application_termt::factoryt<sign_extendt>
299+
sign_extend(std::size_t i);
300+
301+
struct rotate_leftt final
302+
{
303+
std::size_t i;
304+
static const char *identifier();
305+
static smt_sortt return_sort(const smt_termt &operand);
306+
std::vector<smt_indext> indices() const;
307+
static void validate(const smt_termt &operand);
308+
};
309+
static smt_function_application_termt::factoryt<rotate_leftt>
310+
rotate_left(std::size_t i);
311+
312+
struct rotate_rightt final
313+
{
314+
std::size_t i;
315+
static const char *identifier();
316+
static smt_sortt return_sort(const smt_termt &operand);
317+
std::vector<smt_indext> indices() const;
318+
static void validate(const smt_termt &operand);
319+
};
320+
static smt_function_application_termt::factoryt<rotate_rightt>
321+
rotate_right(std::size_t i);
259322
};
260323

261324
#endif // CPROVER_SOLVERS_SMT2_INCREMENTAL_SMT_BIT_VECTOR_THEORY_H

‎unit/solvers/smt2_incremental/smt_bit_vector_theory.cpp‎

Lines changed: 119 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -174,6 +174,32 @@ TEST_CASE("SMT bit vector bitwise operators", "[core][smt2_incremental]")
174174
}
175175
}
176176

177+
TEST_CASE("SMT bit vector comparison", "[core][smt2_incremental]")
178+
{
179+
const smt_bit_vector_constant_termt a_valid{42, 16}, b_valid{8, 16};
180+
SECTION("Valid operands")
181+
{
182+
const auto compare = smt_bit_vector_theoryt::compare(a_valid, b_valid);
183+
const auto expected_return_sort = smt_bit_vector_sortt{1};
184+
REQUIRE(
185+
compare.function_identifier() ==
186+
smt_identifier_termt("bvcomp", expected_return_sort));
187+
REQUIRE(compare.get_sort() == expected_return_sort);
188+
REQUIRE(compare.arguments().size() == 2);
189+
REQUIRE(compare.arguments()[0].get() == a_valid);
190+
REQUIRE(compare.arguments()[1].get() == b_valid);
191+
}
192+
SECTION("Invalid operands")
193+
{
194+
const smt_bool_literal_termt false_term{false};
195+
const smt_bool_literal_termt true_term{true};
196+
cbmc_invariants_should_throwt invariants_throw;
197+
CHECK_THROWS(smt_bit_vector_theoryt::compare(a_valid, false_term));
198+
CHECK_THROWS(smt_bit_vector_theoryt::compare(false_term, a_valid));
199+
CHECK_THROWS(smt_bit_vector_theoryt::compare(false_term, true_term));
200+
}
201+
}
202+
177203
TEST_CASE("SMT bit vector predicates", "[core][smt2_incremental]")
178204
{
179205
const smt_bit_vector_constant_termt two{2, 8};
@@ -551,3 +577,96 @@ TEST_CASE("SMT bit vector shifts", "[core][smt2_incremental]")
551577
smt_bit_vector_theoryt::arithmetic_shift_right(true_val, three));
552578
}
553579
}
580+
581+
TEST_CASE("SMT bit vector repeat", "[core][smt2_incremental]")
582+
{
583+
const smt_bit_vector_constant_termt two{2, 8};
584+
const auto expected_return_sort = smt_bit_vector_sortt{32};
585+
const smt_bool_literal_termt true_val{true};
586+
const auto function_application = smt_bit_vector_theoryt::repeat(4)(two);
587+
REQUIRE(
588+
function_application.function_identifier() ==
589+
smt_identifier_termt(
590+
"repeat", expected_return_sort, {smt_numeral_indext{4}}));
591+
REQUIRE(function_application.get_sort() == expected_return_sort);
592+
REQUIRE(function_application.arguments().size() == 1);
593+
REQUIRE(function_application.arguments()[0].get() == two);
594+
cbmc_invariants_should_throwt invariants_throw;
595+
REQUIRE_THROWS(smt_bit_vector_theoryt::repeat(0));
596+
REQUIRE_THROWS(smt_bit_vector_theoryt::repeat(1)(true_val));
597+
}
598+
599+
TEST_CASE("SMT bit vector extend", "[core][smt2_incremental]")
600+
{
601+
const smt_bit_vector_constant_termt two{2, 8};
602+
const smt_bool_literal_termt true_val{true};
603+
SECTION("Zero extension")
604+
{
605+
const auto function_application =
606+
smt_bit_vector_theoryt::zero_extend(4)(two);
607+
const auto expected_return_sort = smt_bit_vector_sortt{12};
608+
REQUIRE(
609+
function_application.function_identifier() ==
610+
smt_identifier_termt(
611+
"zero_extend", expected_return_sort, {smt_numeral_indext{4}}));
612+
REQUIRE(function_application.get_sort() == expected_return_sort);
613+
REQUIRE(function_application.arguments().size() == 1);
614+
REQUIRE(function_application.arguments()[0].get() == two);
615+
cbmc_invariants_should_throwt invariants_throw;
616+
REQUIRE_NOTHROW(smt_bit_vector_theoryt::zero_extend(0));
617+
REQUIRE_THROWS(smt_bit_vector_theoryt::zero_extend(1)(true_val));
618+
}
619+
SECTION("Sign extension")
620+
{
621+
const auto function_application =
622+
smt_bit_vector_theoryt::sign_extend(4)(two);
623+
const auto expected_return_sort = smt_bit_vector_sortt{12};
624+
REQUIRE(
625+
function_application.function_identifier() ==
626+
smt_identifier_termt(
627+
"sign_extend", expected_return_sort, {smt_numeral_indext{4}}));
628+
REQUIRE(function_application.get_sort() == expected_return_sort);
629+
REQUIRE(function_application.arguments().size() == 1);
630+
REQUIRE(function_application.arguments()[0].get() == two);
631+
cbmc_invariants_should_throwt invariants_throw;
632+
REQUIRE_NOTHROW(smt_bit_vector_theoryt::sign_extend(0));
633+
REQUIRE_THROWS(smt_bit_vector_theoryt::sign_extend(1)(true_val));
634+
}
635+
}
636+
637+
TEST_CASE("SMT bit vector rotation", "[core][smt2_incremental]")
638+
{
639+
const smt_bit_vector_constant_termt two{2, 8};
640+
const smt_bool_literal_termt true_val{true};
641+
const auto expected_return_sort = smt_bit_vector_sortt{8};
642+
SECTION("Left rotation")
643+
{
644+
const auto function_application =
645+
smt_bit_vector_theoryt::rotate_left(4)(two);
646+
REQUIRE(
647+
function_application.function_identifier() ==
648+
smt_identifier_termt(
649+
"rotate_left", expected_return_sort, {smt_numeral_indext{4}}));
650+
REQUIRE(function_application.get_sort() == expected_return_sort);
651+
REQUIRE(function_application.arguments().size() == 1);
652+
REQUIRE(function_application.arguments()[0].get() == two);
653+
cbmc_invariants_should_throwt invariants_throw;
654+
REQUIRE_NOTHROW(smt_bit_vector_theoryt::rotate_left(0));
655+
REQUIRE_THROWS(smt_bit_vector_theoryt::rotate_left(1)(true_val));
656+
}
657+
SECTION("Right rotation")
658+
{
659+
const auto function_application =
660+
smt_bit_vector_theoryt::rotate_right(4)(two);
661+
REQUIRE(
662+
function_application.function_identifier() ==
663+
smt_identifier_termt(
664+
"rotate_right", expected_return_sort, {smt_numeral_indext{4}}));
665+
REQUIRE(function_application.get_sort() == expected_return_sort);
666+
REQUIRE(function_application.arguments().size() == 1);
667+
REQUIRE(function_application.arguments()[0].get() == two);
668+
cbmc_invariants_should_throwt invariants_throw;
669+
REQUIRE_NOTHROW(smt_bit_vector_theoryt::rotate_right(0));
670+
REQUIRE_THROWS(smt_bit_vector_theoryt::rotate_right(1)(true_val));
671+
}
672+
}

0 commit comments

Comments
 (0)