Merge pull request #7772 from NlightNFotis/enum_in_range

Add lookup for unlowered form in `get_identifier`.

Author: Enrico Steffinlongo

regression/cbmc/enum_is_in_range/enum_test5.desc

@@ -1,4 +1,4 @@
-CORE
+CORE new-smt-backend
 enum_test5.c
 --enum-range-check
 ^EXIT=10$

src/solvers/smt2_incremental/smt2_incremental_decision_procedure.cpp

@@ -351,14 +351,24 @@ static optionalt<smt_termt> get_identifier(
     &expression_identifiers,
   const namespacet &ns)
 {
-  const exprt lowered_expr = lower_enum(expr, ns);
-  const auto handle_find_result =
-    expression_handle_identifiers.find(lowered_expr);
+  // Lookup the non-lowered form first.
+  const auto handle_find_result = expression_handle_identifiers.find(expr);
   if(handle_find_result != expression_handle_identifiers.cend())
     return handle_find_result->second;
-  const auto expr_find_result = expression_identifiers.find(lowered_expr);
+  const auto expr_find_result = expression_identifiers.find(expr);
   if(expr_find_result != expression_identifiers.cend())
     return expr_find_result->second;
+
+  // If that didn't yield any results, then try the lowered form.
+  const exprt lowered_expr = lower_enum(expr, ns);
+  const auto lowered_handle_find_result =
+    expression_handle_identifiers.find(lowered_expr);
+  if(lowered_handle_find_result != expression_handle_identifiers.cend())
+    return lowered_handle_find_result->second;
+  const auto lowered_expr_find_result =
+    expression_identifiers.find(lowered_expr);
+  if(lowered_expr_find_result != expression_identifiers.cend())
+    return lowered_expr_find_result->second;
   return {};
 }
 

unit/solvers/smt2_incremental/encoding/enum_encoding.cpp

@@ -29,7 +29,7 @@ static c_enum_typet make_c_enum_type(
   return enum_type;
 }
 
-constant_exprt create_enum_tag_typed_constant(
+static constant_exprt create_enum_tag_typed_constant(
   const mp_integer &value,
   const c_enum_typet &enum_type,
   const c_enum_tag_typet &enum_tag_type)

unit/solvers/smt2_incremental/smt2_incremental_decision_procedure.cpp

@@ -25,6 +25,7 @@
 // strings instead of `{?}` being printed. It works because catch uses the
 // appropriate overload of `operator<<` where it exists.
 #include <util/byte_operators.h>
+#include <util/c_types.h>
 
 #include <goto-symex/path_storage.h>
 #include <solvers/smt2_incremental/smt_to_smt2_string.h>
@@ -908,3 +909,46 @@ TEST_CASE(
     REQUIRE(test.sent_commands == expected_commands);
   }
 }
+
+static c_enum_typet make_c_enum_type(
+  const unsignedbv_typet &underlying_type,
+  unsigned int value_count)
+{
+  c_enum_typet enum_type{underlying_type};
+
+  auto &members = enum_type.members();
+  members.reserve(value_count);
+
+  for(unsigned int i = 0; i < value_count; ++i)
+  {
+    c_enum_typet::c_enum_membert member;
+    member.set_identifier("V" + std::to_string(i));
+    member.set_base_name("V" + std::to_string(i));
+    member.set_value(integer2bvrep(i, underlying_type.get_width()));
+    members.push_back(member);
+  }
+  return enum_type;
+}
+
+TEST_CASE(
+  "smt2_incremental_decision_proceduret getting enum values back from solver.",
+  "[core][smt2_incremental]")
+{
+  auto test = decision_procedure_test_environmentt::make();
+  const unsignedbv_typet enum_underlying_type{32};
+  const c_enum_typet enum_type = make_c_enum_type(enum_underlying_type, 5);
+  const type_symbolt enum_symbol{"my_enum", enum_type, ID_C};
+  test.symbol_table.insert(enum_symbol);
+  const c_enum_tag_typet enum_tag{enum_symbol.name};
+  const symbolt enum_value_symbol{"my_enum_value", enum_tag, ID_C};
+  test.symbol_table.insert(enum_value_symbol);
+  const auto symbol_expr = enum_value_symbol.symbol_expr();
+  const auto eq_expr = equal_exprt{symbol_expr, symbol_expr};
+
+  test.procedure.handle(eq_expr);
+  test.mock_responses.push_back(
+    smt_get_value_responset{{{"B0", smt_bool_literal_termt{true}}}});
+  auto returned = test.procedure.get(eq_expr);
+
+  REQUIRE(returned == constant_exprt{"true", bool_typet{}});
+}