Merge pull request #7894 from thomasspriggs/tas/smt_function_pointers2

Add function pointer support to incremental SMT decision procedure

Author: thomasspriggs

regression/cbmc/Function_Pointer8/test.desc

@@ -1,4 +1,4 @@
-CORE
+CORE new-smt-backend
 main.c
 
 ^EXIT=10$

src/solvers/smt2_incremental/convert_expr_to_smt.cpp

@@ -24,6 +24,7 @@
 #include <algorithm>
 #include <functional>
 #include <numeric>
+#include <stack>
 
 /// Post order visitation is used in order to construct the the smt terms bottom
 /// upwards without using recursion to traverse the input `exprt`. Therefore
@@ -1875,6 +1876,46 @@ exprt lower_address_of_array_index(exprt expr)
   return expr;
 }
 
+/// Post order traversal where the children of a node are only visited if
+/// applying the \p filter function to that node returns true. Note that this
+/// function is based on the `visit_post_template` function.
+void filtered_visit_post(
+  const exprt &_expr,
+  std::function<bool(const exprt &)> filter,
+  std::function<void(const exprt &)> visitor)
+{
+  struct stack_entryt
+  {
+    const exprt *e;
+    bool operands_pushed;
+    explicit stack_entryt(const exprt *_e) : e(_e), operands_pushed(false)
+    {
+    }
+  };
+
+  std::stack<stack_entryt> stack;
+
+  stack.emplace(&_expr);
+
+  while(!stack.empty())
+  {
+    auto &top = stack.top();
+    if(top.operands_pushed)
+    {
+      visitor(*top.e);
+      stack.pop();
+    }
+    else
+    {
+      // do modification of 'top' before pushing in case 'top' isn't stable
+      top.operands_pushed = true;
+      if(filter(*top.e))
+        for(auto &op : top.e->operands())
+          stack.emplace(&op);
+    }
+  }
+}
+
 smt_termt convert_expr_to_smt(
   const exprt &expr,
   const smt_object_mapt &object_map,
@@ -1894,18 +1935,30 @@ smt_termt convert_expr_to_smt(
 #endif
   sub_expression_mapt sub_expression_map;
   const auto lowered_expr = lower_address_of_array_index(expr);
-  lowered_expr.visit_post([&](const exprt &expr) {
-    const auto find_result = sub_expression_map.find(expr);
-    if(find_result != sub_expression_map.cend())
-      return;
-    smt_termt term = dispatch_expr_to_smt_conversion(
-      expr,
-      sub_expression_map,
-      object_map,
-      pointer_sizes,
-      object_size,
-      is_dynamic_object);
-    sub_expression_map.emplace_hint(find_result, expr, std::move(term));
-  });
+  filtered_visit_post(
+    lowered_expr,
+    [](const exprt &expr) {
+      // Code values inside "address of" expressions do not need to be converted
+      // as the "address of" conversion only depends on the object identifier.
+      // Avoiding the conversion side steps a need to convert arbitrary code to
+      // SMT terms.
+      const auto address_of = expr_try_dynamic_cast<address_of_exprt>(expr);
+      if(!address_of)
+        return true;
+      return !can_cast_type<code_typet>(address_of->object().type());
+    },
+    [&](const exprt &expr) {
+      const auto find_result = sub_expression_map.find(expr);
+      if(find_result != sub_expression_map.cend())
+        return;
+      smt_termt term = dispatch_expr_to_smt_conversion(
+        expr,
+        sub_expression_map,
+        object_map,
+        pointer_sizes,
+        object_size,
+        is_dynamic_object);
+      sub_expression_map.emplace_hint(find_result, expr, std::move(term));
+    });
   return std::move(sub_expression_map.at(lowered_expr));
 }

src/solvers/smt2_incremental/smt2_incremental_decision_procedure.cpp

@@ -70,10 +70,17 @@ get_problem_messages(const smt_responset &response)
 ///   returned by this`gather_dependent_expressions` function.
 /// \details `symbol_exprt`, `array_exprt` and `nondet_symbol_exprt` add
 ///   dependant expressions.
-static std::vector<exprt> gather_dependent_expressions(const exprt &expr)
+static std::vector<exprt> gather_dependent_expressions(const exprt &root_expr)
 {
   std::vector<exprt> dependent_expressions;
-  expr.visit_pre([&](const exprt &expr_node) {
+
+  std::stack<const exprt *> stack;
+  stack.push(&root_expr);
+
+  while(!stack.empty())
+  {
+    const exprt &expr_node = *stack.top();
+    stack.pop();
     if(
       can_cast_expr<symbol_exprt>(expr_node) ||
       can_cast_expr<array_exprt>(expr_node) ||
@@ -83,7 +90,17 @@ static std::vector<exprt> gather_dependent_expressions(const exprt &expr)
     {
       dependent_expressions.push_back(expr_node);
     }
-  });
+    // The decision procedure does not depend on the values inside address of
+    // code typed expressions. We can build the address without knowing the
+    // value at that memory location. In this case the hypothetical compiled
+    // machine instructions at the address are not relevant to solving, only
+    // representing *which* function a pointer points to is needed.
+    const auto address_of = expr_try_dynamic_cast<address_of_exprt>(expr_node);
+    if(address_of && can_cast_type<code_typet>(address_of->object().type()))
+      continue;
+    for(auto &operand : expr_node.operands())
+      stack.push(&operand);
+  }
   return dependent_expressions;
 }
 

unit/solvers/smt2_incremental/convert_expr_to_smt.cpp

@@ -1477,29 +1477,46 @@ TEST_CASE(
   const symbol_exprt bar{"bar", unsignedbv_typet{32}};
   SECTION("Address of symbol")
   {
-    const address_of_exprt address_of_foo{foo};
-    track_expression_objects(address_of_foo, ns, test.object_map);
-    INFO("Expression " + address_of_foo.pretty(1, 0));
-    SECTION("8 object bits")
+    SECTION("bit vector symbol")
+    {
+      const address_of_exprt address_of_foo{foo};
+      track_expression_objects(address_of_foo, ns, test.object_map);
+      INFO("Expression " + address_of_foo.pretty(1, 0));
+      SECTION("8 object bits")
+      {
+        config.bv_encoding.object_bits = 8;
+        const auto converted = test.convert(address_of_foo);
+        CHECK(test.object_map.at(foo).unique_id == 2);
+        CHECK(
+          converted == smt_bit_vector_theoryt::concat(
+                         smt_bit_vector_constant_termt{2, 8},
+                         smt_bit_vector_constant_termt{0, 56}));
+      }
+      SECTION("16 object bits")
+      {
+        config.bv_encoding.object_bits = 16;
+        const auto converted = test.convert(address_of_foo);
+        CHECK(test.object_map.at(foo).unique_id == 2);
+        CHECK(
+          converted == smt_bit_vector_theoryt::concat(
+                         smt_bit_vector_constant_termt{2, 16},
+                         smt_bit_vector_constant_termt{0, 48}));
+      }
+    }
+    SECTION("Code symbol")
     {
       config.bv_encoding.object_bits = 8;
-      const auto converted = test.convert(address_of_foo);
-      CHECK(test.object_map.at(foo).unique_id == 2);
+      const symbol_exprt function{"opaque", code_typet{{}, void_type()}};
+      const address_of_exprt function_pointer{function};
+      track_expression_objects(function_pointer, ns, test.object_map);
+      INFO("Expression " + function_pointer.pretty(1, 0));
+      const auto converted = test.convert(function_pointer);
+      CHECK(test.object_map.at(function).unique_id == 2);
       CHECK(
         converted == smt_bit_vector_theoryt::concat(
                        smt_bit_vector_constant_termt{2, 8},
                        smt_bit_vector_constant_termt{0, 56}));
     }
-    SECTION("16 object bits")
-    {
-      config.bv_encoding.object_bits = 16;
-      const auto converted = test.convert(address_of_foo);
-      CHECK(test.object_map.at(foo).unique_id == 2);
-      CHECK(
-        converted == smt_bit_vector_theoryt::concat(
-                       smt_bit_vector_constant_termt{2, 16},
-                       smt_bit_vector_constant_termt{0, 48}));
-    }
   }
   SECTION("Invariant checks")
   {

unit/solvers/smt2_incremental/smt2_incremental_decision_procedure.cpp

@@ -731,6 +731,30 @@ TEST_CASE(
   REQUIRE(test.sent_commands == expected_commands);
 }
 
+TEST_CASE(
+  "smt2_incremental_decision_proceduret function pointer support.",
+  "[core][smt2_incremental]")
+{
+  auto test = decision_procedure_test_environmentt::make();
+  const code_typet function_type{{}, void_type()};
+  const symbolt function{"opaque", function_type, ID_C};
+  test.symbol_table.insert(function);
+  const address_of_exprt function_pointer{function.symbol_expr()};
+  const equal_exprt equals_null{
+    function_pointer, null_pointer_exprt{pointer_typet{function_type, 32}}};
+
+  test.sent_commands.clear();
+  test.procedure.set_to(equals_null, false);
+
+  const std::vector<smt_commandt> expected_commands{
+    smt_assert_commandt{smt_core_theoryt::make_not(smt_core_theoryt::equal(
+      smt_bit_vector_theoryt::concat(
+        smt_bit_vector_constant_termt{2, 8},
+        smt_bit_vector_constant_termt{0, 24}),
+      smt_bit_vector_constant_termt{0, 32}))}};
+  REQUIRE(test.sent_commands == expected_commands);
+}
+
 TEST_CASE(
   "smt2_incremental_decision_proceduret multi-ary with_exprt introduces "
   "correct number of indexes.",