From 81bd688f0418204376bbaa65370e9eb28c649c53 Mon Sep 17 00:00:00 2001 From: thk123 Date: Fri, 7 Feb 2020 14:34:06 +0000 Subject: [PATCH 1/2] Add test cases for simplifying boolean formula --- unit/util/simplify_expr.cpp | 122 ++++++++++++++++++++++++++++++++++++ 1 file changed, 122 insertions(+) diff --git a/unit/util/simplify_expr.cpp b/unit/util/simplify_expr.cpp index cf837a62109..1fe546b8c44 100644 --- a/unit/util/simplify_expr.cpp +++ b/unit/util/simplify_expr.cpp @@ -298,3 +298,125 @@ TEST_CASE("Simplify cast from bool", "[core][util]") REQUIRE(simp == B); } } + +TEST_CASE("simplify_expr boolean expressions", "[core][util]") +{ + symbol_tablet symbol_table; + namespacet ns{symbol_table}; + + SECTION("Binary boolean operations") + { + struct test_entryt + { + exprt lhs; + exprt rhs; + exprt expected_value; + }; + + SECTION("AND") + { + std::vector test_values = { + {true_exprt(), true_exprt(), true_exprt()}, + {true_exprt(), false_exprt(), false_exprt()}, + {false_exprt(), true_exprt(), false_exprt()}, + {false_exprt(), false_exprt(), false_exprt()}, + }; + + for(const auto &entry : test_values) + { + const exprt result = simplify_expr(and_exprt{entry.lhs, entry.rhs}, ns); + REQUIRE(result == entry.expected_value); + } + } + + SECTION("OR") + { + std::vector test_values = { + {true_exprt(), true_exprt(), true_exprt()}, + {true_exprt(), false_exprt(), true_exprt()}, + {false_exprt(), true_exprt(), true_exprt()}, + {false_exprt(), false_exprt(), false_exprt()}, + }; + + for(const auto &entry : test_values) + { + const exprt result = simplify_expr(or_exprt{entry.lhs, entry.rhs}, ns); + REQUIRE(result == entry.expected_value); + } + } + + SECTION("Implies") + { + std::vector test_values = { + {true_exprt(), true_exprt(), true_exprt()}, + {true_exprt(), false_exprt(), false_exprt()}, + {false_exprt(), true_exprt(), true_exprt()}, + {false_exprt(), false_exprt(), true_exprt()}, + }; + + for(const auto &entry : test_values) + { + const exprt result = + simplify_expr(implies_exprt{entry.lhs, entry.rhs}, ns); + REQUIRE(result == entry.expected_value); + } + } + } + SECTION("Not") + { + REQUIRE(simplify_expr(not_exprt{true_exprt()}, ns) == false_exprt()); + REQUIRE(simplify_expr(not_exprt{false_exprt()}, ns) == true_exprt()); + } + SECTION("Nested boolean expressions") + { + INFO("((!true) || (false => false)) && true)") + REQUIRE( + simplify_expr( + and_exprt{or_exprt{not_exprt{true_exprt{}}, + implies_exprt{false_exprt{}, false_exprt{}}}, + true_exprt{}}, + ns) == true_exprt{}); + } + SECTION("Numeric comparisons") + { + struct test_entryt + { + irep_idt comparison; + int lhs; + int rhs; + exprt expected; + }; + + std::vector comparisons = { + {ID_lt, -1, 1, true_exprt()}, + {ID_lt, 1, 1, false_exprt()}, + {ID_lt, 1, -1, false_exprt()}, + + {ID_le, -1, 1, true_exprt()}, + {ID_le, 1, 1, true_exprt()}, + {ID_le, 1, -1, false_exprt()}, + + {ID_ge, -1, 1, false_exprt()}, + {ID_ge, 1, 1, true_exprt()}, + {ID_ge, 1, -1, true_exprt()}, + + {ID_gt, -1, 1, false_exprt()}, + {ID_gt, 1, 1, false_exprt()}, + {ID_gt, 1, -1, true_exprt()}, + }; + + const auto binary_relation_from = [](const test_entryt &entry) { + const signedbv_typet int_type(32); + return binary_relation_exprt{from_integer(entry.lhs, int_type), + entry.comparison, + from_integer(entry.rhs, int_type)}; + }; + + for(const test_entryt &test_entry : comparisons) + { + REQUIRE( + simplify_expr(binary_relation_from(test_entry), ns) == + test_entry.expected); + } + } +} From a8c1571b9c1ca6d6e51a78551c8d1744008e5afa Mon Sep 17 00:00:00 2001 From: thk123 Date: Fri, 7 Feb 2020 15:22:26 +0000 Subject: [PATCH 2/2] Import tests for checking type cast removal --- unit/util/simplify_expr.cpp | 80 +++++++++++++++++++++++++++++++++++++ 1 file changed, 80 insertions(+) diff --git a/unit/util/simplify_expr.cpp b/unit/util/simplify_expr.cpp index 1fe546b8c44..15ba59a65ab 100644 --- a/unit/util/simplify_expr.cpp +++ b/unit/util/simplify_expr.cpp @@ -420,3 +420,83 @@ TEST_CASE("simplify_expr boolean expressions", "[core][util]") } } } + +TEST_CASE("Simplifying cast expressions", "[core][util]") +{ + symbol_tablet symbol_table; + namespacet ns(symbol_table); + const auto short_type = signedbv_typet(16); + const auto int_type = signedbv_typet(32); + const auto long_type = signedbv_typet(64); + array_typet array_type(int_type, from_integer(5, int_type)); + + symbolt a_symbol; + a_symbol.base_name = "a"; + a_symbol.name = "a"; + a_symbol.type = array_type; + a_symbol.is_lvalue = true; + symbol_table.add(a_symbol); + + symbolt i_symbol; + i_symbol.base_name = "i"; + i_symbol.name = "i"; + i_symbol.type = int_type; + i_symbol.is_lvalue = true; + symbol_table.add(i_symbol); + + config.set_arch("none"); + + SECTION("Simplifying a[(signed long int)0]") + { + // a[(signed long int)0] + index_exprt expr{symbol_exprt{"a", array_type}, + typecast_exprt{from_integer(0, int_type), long_type}}; + // cast is applied on the constant + const auto simplified_expr = simplify_expr(expr, ns); + REQUIRE( + simplified_expr == + index_exprt{symbol_exprt{"a", array_type}, from_integer(0, long_type)}); + } + SECTION("Simplifying a[(signed long int)i]") + { + // a[(signed long int)0] + index_exprt expr{symbol_exprt{"a", array_type}, + typecast_exprt{i_symbol.symbol_expr(), long_type}}; + // Cast is not removed as up casting a symbol + const auto simplified_expr = simplify_expr(expr, ns); + REQUIRE(simplified_expr == expr); + } + SECTION("Simplifying a[(signed int)i]") + { + // a[(signed int)i] + index_exprt expr{symbol_exprt{"a", array_type}, + typecast_exprt{i_symbol.symbol_expr(), int_type}}; + + const auto simplified_expr = simplify_expr(expr, ns); + REQUIRE( + simplified_expr == + index_exprt{symbol_exprt{"a", array_type}, i_symbol.symbol_expr()}); + } + SECTION("Simplifying a[(signed short)0]") + { + // a[(signed short)0] + index_exprt expr{symbol_exprt{"a", array_type}, + typecast_exprt{from_integer(0, int_type), short_type}}; + + // Can be simplified as the number is a constant + const auto simplified_expr = simplify_expr(expr, ns); + REQUIRE( + simplified_expr == + index_exprt{symbol_exprt{"a", array_type}, from_integer(0, short_type)}); + } + SECTION("Simplifying a[(signed short)i]") + { + // a[(signed short)i] + index_exprt expr{symbol_exprt{"a", array_type}, + typecast_exprt{i_symbol.symbol_expr(), short_type}}; + + // No simplification as the cast may have an effect + const auto simplified_expr = simplify_expr(expr, ns); + REQUIRE(simplified_expr == expr); + } +}