Do not convert code values in address_of expressions to SMT

Previous to this commit, C examples containing function pointers
would cause INVARIANT violations due to an attempt to convert code
values inside address_of expressions into SMT terms. This commit avoids
performing the conversion. This is a valid approach as the decision
procedure only needs to handle code addresses, not the actual code
itself.

Author: thomasspriggs

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
@@ -1845,6 +1846,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,
@@ -1864,18 +1905,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

@@ -69,10 +69,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) ||
@@ -82,7 +89,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;
 }