Merge pull request #7755 from esteffin/esteffin/incr-smt2-c-enum-tag

Incremental SMT2 support for enum values

Author: Enrico Steffinlongo

regression/cbmc-incr-smt2/enums/enum_in_array.c

@@ -0,0 +1,19 @@
+#include <assert.h>
+
+enum E
+{
+  V0 = 0,
+  V1 = 1,
+  V2 = 2
+};
+
+int main()
+{
+  unsigned i;
+  __CPROVER_assume(i < 3);
+  enum E e[3];
+  e[0] = V0;
+  e[1] = V1;
+  e[2] = V2;
+  __CPROVER_assert(e[i] > 0, "Array at index 0 is V0, so this should fail");
+}

regression/cbmc-incr-smt2/enums/enum_in_array.desc

@@ -0,0 +1,15 @@
+CORE
+enum_in_array.c
+--trace
+Passing problem to incremental SMT2 solving
+line 18 Array at index 0 is V0, so this should fail: FAILURE
+i=0u \(00000000 00000000 00000000 00000000\)
+e\[0l+\]=/\*enum\*/V0 \(00000000 00000000 00000000 00000000\)
+e\[1l+\]=/\*enum\*/V1 \(00000000 00000000 00000000 00000001\)
+e\[2l+\]=/\*enum\*/V2 \(00000000 00000000 00000000 00000010\)
+^EXIT=10$
+^SIGNAL=0$
+--
+--
+Test that we support enum values and traces for an array of enums. At the time of adding the
+regression test, this exercised the conversion code specific to c_enum_tag_typet.

regression/cbmc-incr-smt2/enums/enum_in_struct.c

@@ -0,0 +1,22 @@
+#include <assert.h>
+
+enum E
+{
+  V0 = 0,
+  V1 = 1,
+  V2 = 2
+};
+
+struct S
+{
+  enum E a;
+  int b;
+};
+
+int main()
+{
+  struct S s;
+  s.a = V1;
+  __CPROVER_assume(__CPROVER_enum_is_in_range(s.a));
+  __CPROVER_assert(s.a > 10, "Struct field s.a is V1, so this should fail");
+}

regression/cbmc-incr-smt2/enums/enum_in_struct.desc

@@ -0,0 +1,12 @@
+CORE
+enum_in_struct.c
+--trace
+Passing problem to incremental SMT2 solving
+line 21 Struct field s\.a is V1, so this should fail: FAILURE
+s\.a=/\*enum\*/V1 \(00000000 00000000 00000000 00000001\)
+^EXIT=10$
+^SIGNAL=0$
+--
+--
+Test that we support enum values and traces for an struct with enums fields. At the time of adding
+the regression test, this exercised the conversion code specific to c_enum_tag_typet.

regression/cbmc-incr-smt2/enums/simple.c

@@ -0,0 +1,16 @@
+#include <assert.h>
+
+enum E
+{
+  V0 = 0,
+  V1 = 1,
+  V2 = 2
+};
+
+int main()
+{
+  enum E e;
+  e = V1;
+  __CPROVER_assume(__CPROVER_enum_is_in_range(e));
+  __CPROVER_assert(e > 10, "Variable e is V1, so this should fail");
+}

regression/cbmc-incr-smt2/enums/simple.desc

@@ -0,0 +1,14 @@
+CORE
+simple.c
+--trace
+Passing problem to incremental SMT2 solving
+line 15 Variable e is V1, so this should fail: FAILURE
+e=/\*enum\*/V0 \(00000000 00000000 00000000 00000000\)
+e=/\*enum\*/V1 \(00000000 00000000 00000000 00000001\)
+^EXIT=10$
+^SIGNAL=0$
+--
+--
+Test that we support enum values and traces for a trivial example. At the
+time of adding the regression test, this exercised the conversion code specific
+to c_enum_tag_typet.

regression/cbmc/enum-trace1/test_json.desc

@@ -1,4 +1,4 @@
-CORE
+CORE new-smt-backend
 main.c
 --json-ui --function test --trace
 activate-multi-line-match

regression/cbmc/enum-trace1/test_xml.desc

@@ -1,4 +1,4 @@
-CORE
+CORE new-smt-backend
 main.c
 --xml-ui --function test --trace
 activate-multi-line-match

regression/cbmc/enum3/test.desc

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

regression/cbmc/enum_is_in_range/enum_test4.desc

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

regression/cbmc/enum_is_in_range/enum_test8.desc

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

src/solvers/Makefile

@@ -210,7 +210,8 @@ SRC = $(BOOLEFORCE_SRC) \
       smt2_incremental/smt_solver_process.cpp \
       smt2_incremental/smt_to_smt2_string.cpp \
       smt2_incremental/smt2_incremental_decision_procedure.cpp \
-      smt2_incremental/struct_encoding.cpp \
+      smt2_incremental/encoding/struct_encoding.cpp \
+      smt2_incremental/encoding/enum_encoding.cpp \
       smt2_incremental/theories/smt_array_theory.cpp \
       smt2_incremental/theories/smt_bit_vector_theory.cpp \
       smt2_incremental/theories/smt_core_theory.cpp \

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/encoding/enum_encoding.cpp

@@ -0,0 +1,53 @@
+// Author: Diffblue Ltd.
+
+#include "enum_encoding.h"
+
+#include <util/c_types.h>
+#include <util/expr_cast.h>
+#include <util/namespace.h>
+
+#include <queue>
+
+// Internal function to lower inner types of compound types (at the moment only
+// arrays)
+static typet encode(typet type, const namespacet &ns)
+{
+  std::queue<typet *> work_queue;
+  work_queue.push(&type);
+  while(!work_queue.empty())
+  {
+    typet &current = *work_queue.front();
+    work_queue.pop();
+    if(const auto c_enum_tag = type_try_dynamic_cast<c_enum_tag_typet>(current))
+    {
+      // Replace the type of the c_enum_tag with the underlying type of the enum
+      // it points to
+      current = ns.follow_tag(*c_enum_tag).underlying_type();
+    }
+    if(const auto array = type_try_dynamic_cast<array_typet>(current))
+    {
+      // Add the type of the array's elements to the queue to be explored
+      work_queue.push(&array->element_type());
+    }
+  }
+  return type;
+}
+
+// Worklist algorithm to lower enum types of expr and its sub-expressions.
+exprt lower_enum(exprt expr, const namespacet &ns)
+{
+  std::queue<exprt *> work_queue;
+  work_queue.push(&expr);
+  while(!work_queue.empty())
+  {
+    exprt &current = *work_queue.front();
+    work_queue.pop();
+
+    // Replace the type of the expression node with the encoded one
+    current.type() = encode(current.type(), ns);
+
+    for(auto &operand : current.operands())
+      work_queue.push(&operand);
+  }
+  return expr;
+}

src/solvers/smt2_incremental/encoding/enum_encoding.h

@@ -0,0 +1,16 @@
+// Author: Diffblue Ltd.
+
+#ifndef CPROVER_SOLVERS_SMT2_INCREMENTAL_ENCODING_ENUM_ENCODING_H
+#define CPROVER_SOLVERS_SMT2_INCREMENTAL_ENCODING_ENUM_ENCODING_H
+
+#include <util/expr.h>
+
+/// Function to lower `expr` and its sub-expressions containing enum types.
+/// Specifically it replaces the node `c_enum_tag_typet` type with the
+/// underlying type of the enum the tag points to.
+/// @param expr the expression to lower.
+/// @param ns the namespace where to lookup `c_enum_tag_type`s.
+/// @return the lowered expression.
+exprt lower_enum(exprt expr, const namespacet &ns);
+
+#endif // CPROVER_SOLVERS_SMT2_INCREMENTAL_ENCODING_ENUM_ENCODING_H

src/solvers/smt2_incremental/encoding/module_dependencies.txt

@@ -0,0 +1 @@
+util

src/solvers/smt2_incremental/struct_encoding.cpp renamed to src/solvers/smt2_incremental/encoding/struct_encoding.cpp

@@ -16,6 +16,7 @@
 #include <solvers/smt2_incremental/ast/smt_terms.h>
 #include <solvers/smt2_incremental/construct_value_expr_from_smt.h>
 #include <solvers/smt2_incremental/convert_expr_to_smt.h>
+#include <solvers/smt2_incremental/encoding/enum_encoding.h>
 #include <solvers/smt2_incremental/smt_solver_process.h>
 #include <solvers/smt2_incremental/theories/smt_array_theory.h>
 #include <solvers/smt2_incremental/theories/smt_core_theory.h>
@@ -347,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 {};
@@ -409,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
@@ -446,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;
     }
@@ -590,8 +596,8 @@ void smt2_incremental_decision_proceduret::define_object_properties()
 
 exprt smt2_incremental_decision_proceduret::lower(exprt expression)
 {
-  const exprt lowered =
-    struct_encoding.encode(lower_byte_operators(expression, ns));
+  const exprt lowered = struct_encoding.encode(
+    lower_enum(lower_byte_operators(expression, ns), ns));
   log.conditional_output(log.debug(), [&](messaget::mstreamt &debug) {
     if(lowered != expression)
       debug << "lowered to -\n  " << lowered.pretty(2, 0) << messaget::eom;

src/solvers/smt2_incremental/struct_encoding.h renamed to src/solvers/smt2_incremental/encoding/struct_encoding.h

@@ -10,10 +10,10 @@
 #include <util/std_expr.h>
 
 #include <solvers/smt2_incremental/ast/smt_terms.h>
+#include <solvers/smt2_incremental/encoding/struct_encoding.h>
 #include <solvers/smt2_incremental/object_tracking.h>
 #include <solvers/smt2_incremental/smt_is_dynamic_object.h>
 #include <solvers/smt2_incremental/smt_object_size.h>
-#include <solvers/smt2_incremental/struct_encoding.h>
 #include <solvers/smt2_incremental/type_size_mapping.h>
 #include <solvers/stack_decision_procedure.h>