Support for enum in incremental SMT2 traces

This commit enables the generation of traces containing expression of
type `c_enum_tag_typet`.

Author: Enrico Steffinlongo

src/solvers/smt2_incremental/construct_value_expr_from_smt.cpp

@@ -1,6 +1,8 @@
 // Author: Diffblue Ltd.
 
 #include <util/arith_tools.h>
+#include <util/c_types.h>
+#include <util/namespace.h>
 #include <util/pointer_expr.h>
 #include <util/std_expr.h>
 #include <util/std_types.h>
@@ -13,10 +15,13 @@ class value_expr_from_smt_factoryt : public smt_term_const_downcast_visitort
 {
 private:
   const typet &type_to_construct;
+  const namespacet &ns;
   optionalt<exprt> result;
 
-  explicit value_expr_from_smt_factoryt(const typet &type_to_construct)
-    : type_to_construct{type_to_construct}, result{}
+  explicit value_expr_from_smt_factoryt(
+    const typet &type_to_construct,
+    const namespacet &ns)
+    : type_to_construct{type_to_construct}, ns{ns}, result{}
   {
   }
 
@@ -70,6 +75,20 @@ class value_expr_from_smt_factoryt : public smt_term_const_downcast_visitort
       result = from_integer(bit_vector_constant.value(), type_to_construct);
       return;
     }
+    if(
+      const auto c_enum_tag_type =
+        type_try_dynamic_cast<c_enum_tag_typet>(type_to_construct))
+    {
+      const c_enum_typet &real_type = ns.follow_tag(*c_enum_tag_type);
+      INVARIANT(
+        to_bitvector_type(real_type.underlying_type()).get_width() ==
+          sort_width,
+        "Width of smt bit vector term must match the width of bit vector "
+        "underlying type of the original c_enum type.");
+      result = from_integer(bit_vector_constant.value(), real_type);
+      result->type() = type_to_construct;
+      return;
+    }
 
     INVARIANT(
       false,
@@ -102,9 +121,12 @@ class value_expr_from_smt_factoryt : public smt_term_const_downcast_visitort
   /// \brief This function is complete the external interface to this class. All
   ///   construction of this class and construction of expressions should be
   ///   carried out via this function.
-  static exprt make(const smt_termt &value_term, const typet &type_to_construct)
+  static exprt make(
+    const smt_termt &value_term,
+    const typet &type_to_construct,
+    const namespacet &ns)
   {
-    value_expr_from_smt_factoryt factory{type_to_construct};
+    value_expr_from_smt_factoryt factory{type_to_construct, ns};
     value_term.accept(factory);
     INVARIANT(factory.result.has_value(), "Factory must result in expr value.");
     return *factory.result;
@@ -113,7 +135,8 @@ class value_expr_from_smt_factoryt : public smt_term_const_downcast_visitort
 
 exprt construct_value_expr_from_smt(
   const smt_termt &value_term,
-  const typet &type_to_construct)
+  const typet &type_to_construct,
+  const namespacet &ns)
 {
-  return value_expr_from_smt_factoryt::make(value_term, type_to_construct);
+  return value_expr_from_smt_factoryt::make(value_term, type_to_construct, ns);
 }

src/solvers/smt2_incremental/construct_value_expr_from_smt.h

@@ -18,6 +18,9 @@ class typet;
 /// \param type_to_construct
 ///   The type which the constructed expr returned is expected to have. This
 ///   type must be compatible with the sort of \p value_term.
+/// \param ns
+///   The namespace to resolve `c_enum_tag_type` to reconstruct the correct
+///   type of enum values in the trace.
 /// \note The type is required separately in order to carry out this conversion,
 /// because the smt value term does not contain all the required information.
 /// For example an 8 bit, bit vector with a value of 255 could be used to
@@ -26,6 +29,7 @@ class typet;
 /// using the type.
 exprt construct_value_expr_from_smt(
   const smt_termt &value_term,
-  const typet &type_to_construct);
+  const typet &type_to_construct,
+  const namespacet &ns);
 
 #endif // CPROVER_SOLVERS_SMT2_INCREMENTAL_CONSTRUCT_VALUE_EXPR_FROM_SMT_H

src/solvers/smt2_incremental/smt2_incremental_decision_procedure.cpp

@@ -348,12 +348,15 @@ static optionalt<smt_termt> get_identifier(
   const std::unordered_map<exprt, smt_identifier_termt, irep_hash>
     &expression_handle_identifiers,
   const std::unordered_map<exprt, smt_identifier_termt, irep_hash>
-    &expression_identifiers)
+    &expression_identifiers,
+  const namespacet &ns)
 {
-  const auto handle_find_result = expression_handle_identifiers.find(expr);
+  const exprt lowered_expr = lower_enum(expr, ns);
+  const auto handle_find_result =
+    expression_handle_identifiers.find(lowered_expr);
   if(handle_find_result != expression_handle_identifiers.cend())
     return handle_find_result->second;
-  const auto expr_find_result = expression_identifiers.find(expr);
+  const auto expr_find_result = expression_identifiers.find(lowered_expr);
   if(expr_find_result != expression_identifiers.cend())
     return expr_find_result->second;
   return {};
@@ -410,7 +413,7 @@ exprt smt2_incremental_decision_proceduret::get_expr(
       response.pretty()};
   }
   return construct_value_expr_from_smt(
-    get_value_response->pairs()[0].get().value(), type);
+    get_value_response->pairs()[0].get().value(), type, ns);
 }
 
 // This is a fall back which builds resulting expression based on getting the
@@ -447,18 +450,20 @@ exprt smt2_incremental_decision_proceduret::get(const exprt &expr) const
       const auto array = get_identifier(
         index_expr->array(),
         expression_handle_identifiers,
-        expression_identifiers);
+        expression_identifiers,
+        ns);
       const auto index = get_identifier(
         index_expr->index(),
         expression_handle_identifiers,
-        expression_identifiers);
+        expression_identifiers,
+        ns);
       if(!array || !index)
         return {};
       return smt_array_theoryt::select(*array, *index);
     }
     if(
       auto identifier_descriptor = get_identifier(
-        expr, expression_handle_identifiers, expression_identifiers))
+        expr, expression_handle_identifiers, expression_identifiers, ns))
     {
       return identifier_descriptor;
     }

unit/solvers/smt2_incremental/construct_value_expr_from_smt.cpp

@@ -3,8 +3,10 @@
 #include <util/arith_tools.h>
 #include <util/bitvector_types.h>
 #include <util/c_types.h>
+#include <util/namespace.h>
 #include <util/std_expr.h>
 #include <util/std_types.h>
+#include <util/symbol_table.h>
 
 #include <solvers/smt2_incremental/ast/smt_terms.h>
 #include <solvers/smt2_incremental/construct_value_expr_from_smt.h>
@@ -31,6 +33,8 @@ static mp_integer max_int(const std::size_t bits)
 
 TEST_CASE("Value expr construction from smt.", "[core][smt2_incremental]")
 {
+  const symbol_tablet symbol_table;
+  const namespacet ns{symbol_table};
   optionalt<smt_termt> input_term;
   optionalt<exprt> expected_result;
 
@@ -90,7 +94,7 @@ TEST_CASE("Value expr construction from smt.", "[core][smt2_incremental]")
     "\" from \"" + smt_to_smt2_string(*input_term) + "\"")
   {
     REQUIRE(
-      construct_value_expr_from_smt(*input_term, expected_result->type()) ==
+      construct_value_expr_from_smt(*input_term, expected_result->type(), ns) ==
       *expected_result);
   }
 }
@@ -99,6 +103,8 @@ TEST_CASE(
   "Invariant violations in value expr construction from smt.",
   "[core][smt2_incremental]")
 {
+  const symbol_tablet symbol_table;
+  const namespacet ns{symbol_table};
   optionalt<smt_termt> input_term;
   optionalt<typet> input_type;
   std::string invariant_reason;
@@ -145,8 +151,9 @@ TEST_CASE(
   SECTION(invariant_reason)
   {
     const cbmc_invariants_should_throwt invariants_throw;
+
     REQUIRE_THROWS_MATCHES(
-      construct_value_expr_from_smt(*input_term, *input_type),
+      construct_value_expr_from_smt(*input_term, *input_type, ns),
       invariant_failedt,
       invariant_failure_containing(invariant_reason));
   }