Merge pull request #7404 from esteffin/esteffin/fix-trace-invariant-violation

Fix trace invariant violation on smt2 incremental backend

Author: Enrico Steffinlongo

regression/cbmc-incr-smt2/pointers-conversions/byte_extract_issue.c renamed to regression/cbmc-incr-smt2/pointers-conversions/byte_extract.c

@@ -6,7 +6,7 @@ int main()
   uint32_t input;
   uint32_t original = input;
   uint8_t *ptr = (uint8_t *)(&input);
-  assert(*ptr == 0); // falsifiable
+  assert(*ptr != 42); // falsifiable
   *ptr = ~(*ptr);
   assert(input != original); // valid
 }

regression/cbmc-incr-smt2/pointers-conversions/byte_extract.desc

@@ -0,0 +1,19 @@
+CORE
+byte_extract.c
+--trace
+Running incremental SMT2 solving via
+Building error trace
+\[main\.assertion\.\d+\] line \d+ assertion \*ptr != 42: FAILURE
+\[main\.assertion\.\d+\] line \d+ assertion input != original: SUCCESS
+  input=42ul? \(00000000 00000000 00000000 00101010\)
+  original=42ul? \(00000000 00000000 00000000 00101010\)
+Violated property:
+  file byte_extract.c function main line \d+ thread \d+
+  assertion \*ptr != 42
+^EXIT=10$
+^SIGNAL=0$
+--
+Reached unimplemented Generation of SMT formula for byte extract expression: byte_extract_little_endian
+--
+This test is here to document our lack of support for byte_extract_little_endian
+in the pointers support for the new SMT backend.

regression/cbmc-incr-smt2/pointers-conversions/byte_extract_issue.desc

@@ -0,0 +1,12 @@
+#include <assert.h>
+#include <stdint.h>
+
+int main()
+{
+  uint32_t x = 0u;
+  uint8_t *ptr = (uint8_t *)(&x);
+  uint32_t offset;
+  __CPROVER_assume(offset >= 0u && offset < 4u);
+  *(ptr + offset) = 1u;
+  assert(x != 256u);
+}

regression/cbmc-incr-smt2/pointers-conversions/byte_update.c

@@ -0,0 +1,23 @@
+CORE
+byte_update.c
+--trace
+Running incremental SMT2 solving via
+Building error trace
+\[main\.assertion\.\d+\] line \d+ assertion x != 256u: FAILURE
+State \d+ file byte_update\.c function main line \d+ thread \d
+  offset=1ul? \(00000000 00000000 00000000 00000001\)
+Assumption:
+  file byte_update\.c line \d+ function main
+  offset >= 0u && offset < 4u
+State \d+ file byte_update\.c function main line \d+ thread \d+
+  byte_extract_little_endian\(x, \(signed long( long)? int\)offset, uint8_t\)=1 \(00000001\)
+Violated property:
+  file byte_update.c function main line \d+ thread \d+
+  assertion x != 256u
+^EXIT=10$
+^SIGNAL=0$
+--
+Reached unimplemented Generation of SMT formula for byte extract expression: byte_update_little_endian
+--
+This test is here to document our lack of support for byte_update_little_endian
+in the pointers support for the new SMT backend.

regression/cbmc-incr-smt2/pointers-conversions/byte_update.desc

@@ -164,6 +164,8 @@ extension_for_type(const typet &type)
     return smt_bit_vector_theoryt::sign_extend;
   if(can_cast_type<unsignedbv_typet>(type))
     return smt_bit_vector_theoryt::zero_extend;
+  if(can_cast_type<bv_typet>(type))
+    return smt_bit_vector_theoryt::zero_extend;
   UNREACHABLE;
 }
 
@@ -947,6 +949,9 @@ static smt_termt convert_to_smt_shift(
   INVARIANT(
     first_bit_vector_sort && second_bit_vector_sort,
     "Shift expressions are expected to have bit vector operands.");
+  INVARIANT(
+    shift.type() == shift.op0().type(),
+    "Shift expression type must be equals to first operand type.");
   const std::size_t first_width = first_bit_vector_sort->bit_width();
   const std::size_t second_width = second_bit_vector_sort->bit_width();
   if(first_width > second_width)
@@ -958,10 +963,11 @@ static smt_termt convert_to_smt_shift(
   }
   else if(first_width < second_width)
   {
-    return factory(
+    const auto result = factory(
       extension_for_type(shift.op0().type())(second_width - first_width)(
         first_operand),
       second_operand);
+    return smt_bit_vector_theoryt::extract(first_width - 1, 0)(result);
   }
   else
   {

regression/cbmc-incr-smt2/pointers-conversions/byte_update_issue.c

@@ -411,6 +411,29 @@ exprt smt2_incremental_decision_proceduret::get_expr(
     get_value_response->pairs()[0].get().value(), type);
 }
 
+// This is a fall back which builds resulting expression based on getting the
+// values of its operands. It is used during trace building in the case where
+// certain kinds of expression appear on the left hand side of an
+// assignment. For example in the following trace assignment -
+//   `byte_extract_little_endian(x, offset) = 1`
+// `::get` will be called on `byte_extract_little_endian(x, offset)` and
+// we build a resulting expression where `x` and `offset` are substituted
+// with their values.
+static exprt build_expr_based_on_getting_operands(
+  const exprt &expr,
+  const stack_decision_proceduret &decision_procedure)
+{
+  exprt copy = expr;
+  for(auto &op : copy.operands())
+  {
+    exprt eval_op = decision_procedure.get(op);
+    if(eval_op.is_nil())
+      return nil_exprt{};
+    op = std::move(eval_op);
+  }
+  return copy;
+}
+
 exprt smt2_incremental_decision_proceduret::get(const exprt &expr) const
 {
   log.conditional_output(log.debug(), [&](messaget::mstreamt &debug) {
@@ -431,29 +454,31 @@ exprt smt2_incremental_decision_proceduret::get(const exprt &expr) const
         return {};
       return smt_array_theoryt::select(*array, *index);
     }
-    return get_identifier(
-      expr, expression_handle_identifiers, expression_identifiers);
-  }();
-  if(!descriptor)
-  {
+    if(
+      auto identifier_descriptor = get_identifier(
+        expr, expression_handle_identifiers, expression_identifiers))
+    {
+      return identifier_descriptor;
+    }
     if(gather_dependent_expressions(expr).empty())
     {
       INVARIANT(
         objects_are_already_tracked(expr, object_map),
         "Objects in expressions being read should already be tracked from "
         "point of being set/handled.");
-      descriptor = ::convert_expr_to_smt(
+      return ::convert_expr_to_smt(
         expr,
         object_map,
         pointer_sizes_map,
         object_size_function.make_application,
         is_dynamic_object_function.make_application);
     }
-    else
+    return {};
+  }();
+  if(!descriptor)
+  {
+    if(const auto symbol_expr = expr_try_dynamic_cast<symbol_exprt>(expr))
     {
-      const auto symbol_expr = expr_try_dynamic_cast<symbol_exprt>(expr);
-      INVARIANT(
-        symbol_expr, "Unhandled expressions are expected to be symbols");
       // Note this case is currently expected to be encountered during trace
       // generation for -
       //  * Steps which were removed via --slice-formula.
@@ -466,6 +491,7 @@ exprt smt2_incremental_decision_proceduret::get(const exprt &expr) const
         << symbol_expr->get_identifier() << messaget::eom;
       return expr;
     }
+    return build_expr_based_on_getting_operands(expr, *this);
   }
   if(const auto array_type = type_try_dynamic_cast<array_typet>(expr.type()))
   {

regression/cbmc-incr-smt2/pointers-conversions/byte_update_issue.desc

@@ -1209,10 +1209,11 @@ TEST_CASE(
           symbol_exprt{"foo", make_type(8)},
           symbol_exprt{"bar", make_type(32)});
         INFO("Input expr: " + input.pretty(2, 0));
-        const smt_termt expected_result = make_shift_term(
-          make_extension(24)(
-            smt_identifier_termt{"foo", smt_bit_vector_sortt{8}}),
-          smt_identifier_termt{"bar", smt_bit_vector_sortt{32}});
+        const smt_termt expected_result =
+          smt_bit_vector_theoryt::extract(7, 0)(make_shift_term(
+            make_extension(24)(
+              smt_identifier_termt{"foo", smt_bit_vector_sortt{8}}),
+            smt_identifier_termt{"bar", smt_bit_vector_sortt{32}}));
         CHECK(test.convert(input) == expected_result);
       }
     }

src/solvers/smt2_incremental/convert_expr_to_smt.cpp

@@ -539,13 +539,26 @@ TEST_CASE(
     }
     SECTION("Invariant violated due to expression in unexpected form.")
     {
-      const mult_exprt unexpected{foo.symbol_expr(), from_integer(2, foo.type)};
-      const cbmc_invariants_should_throwt invariants_throw;
-      REQUIRE_THROWS_MATCHES(
-        test.procedure.get(unexpected),
-        invariant_failedt,
-        invariant_failure_containing(
-          "Unhandled expressions are expected to be symbols"));
+      const auto offset = from_integer(2, signedbv_typet{64});
+      const byte_extract_exprt byte_extract_expr{
+        ID_byte_extract_little_endian,
+        foo.symbol_expr(),
+        offset,
+        8,
+        unsignedbv_typet{8}};
+      test.mock_responses.push_back(
+        smt_get_value_responset{{{foo_term, term_42}}});
+      test.mock_responses.push_back(smt_get_value_responset{
+        {{smt_bit_vector_constant_termt{2, 64},
+          smt_bit_vector_constant_termt{2, 64}}}});
+      REQUIRE(
+        test.procedure.get(byte_extract_expr) ==
+        byte_extract_exprt{
+          ID_byte_extract_little_endian,
+          expr_42,
+          offset,
+          8,
+          unsignedbv_typet{8}});
     }
     SECTION("Error handling of mismatched response.")
     {