Unit tests for simplifying boolean and cast expressions

unit/util/simplify_expr.cpp

@@ -298,3 +298,205 @@ 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_entryt> 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_entryt> 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_entryt> 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<test_entryt> 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);
+    }
+  }
+}
+
+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);
+  }
+}