Merge pull request #7285 from esteffin/esteffin/byte-extraction-update-2

Support byte extract and update for new SMT backend

Author: thomasspriggs

regression/cbmc-incr-smt2/bitvector-bitwise-operators/array-misalign-between.c

@@ -0,0 +1,18 @@
+#include <assert.h>
+#include <stdint.h>
+
+int main()
+{
+  uint16_t x[3];
+  x[0] = 0;
+  x[1] = 0;
+  x[2] = 0;
+  uint8_t *c = x;
+  c[1] = 1;
+  assert(x[0] == 256);
+  assert(x[0] == 0);
+  assert(x[1] == 0);
+  assert(x[2] == 0);
+  uint16_t between = c[1];
+  assert(between == 1);
+}

regression/cbmc-incr-smt2/bitvector-bitwise-operators/array-misalign-between.desc

@@ -0,0 +1,12 @@
+CORE
+array-misalign-between.c
+--slice-formula
+\[main\.assertion\.1\] line \d+ assertion x\[0\] == 256: SUCCESS
+\[main\.assertion\.2\] line \d+ assertion x\[0\] == 0: FAILURE
+\[main\.assertion\.3\] line \d+ assertion x\[1\] == 0: SUCCESS
+\[main\.assertion\.4\] line \d+ assertion x\[2\] == 0: SUCCESS
+\[main\.assertion\.5\] line \d+ assertion between == 1: SUCCESS
+^EXIT=10$
+^SIGNAL=0$
+--
+--

regression/cbmc-incr-smt2/bitvector-bitwise-operators/array-misalign.c

@@ -0,0 +1,16 @@
+#include <assert.h>
+#include <stdint.h>
+
+int main()
+{
+  uint16_t x[3];
+  x[0] = 0;
+  x[1] = 0;
+  x[2] = 0;
+  uint8_t *c = x;
+  c[1] = 1;
+  assert(x[0] == 256ul);
+  assert(x[0] == 0ul);
+  assert(x[1] == 0ul);
+  assert(x[2] == 0ul);
+}

regression/cbmc-incr-smt2/bitvector-bitwise-operators/array-misalign.desc

@@ -0,0 +1,11 @@
+CORE
+array-misalign.c
+--slice-formula
+\[main.assertion\.1\] line \d+ assertion x\[0\] == 256ul: SUCCESS
+\[main.assertion\.2\] line \d+ assertion x\[0\] == 0ul: FAILURE
+\[main.assertion\.3\] line \d+ assertion x\[1\] == 0ul: SUCCESS
+\[main.assertion\.4\] line \d+ assertion x\[2\] == 0ul: SUCCESS
+^EXIT=10$
+^SIGNAL=0$
+--
+--

regression/cbmc-incr-smt2/bitvector-bitwise-operators/byte-extract-small.c

@@ -0,0 +1,12 @@
+#include <assert.h>
+#include <stdint.h>
+
+int main()
+{
+  uint8_t x[2];
+  x[0] = 1u;
+  x[1] = 1u;
+  uint16_t *y = x;
+  uint16_t z = *y;
+  assert(z == 257);
+}

regression/cbmc-incr-smt2/bitvector-bitwise-operators/byte-extract-small.desc

@@ -0,0 +1,8 @@
+CORE
+byte-extract-small.c
+--slice-formula
+\[main.assertion\.1\] line \d+ assertion z == 257: SUCCESS
+^EXIT=0$
+^SIGNAL=0$
+--
+--

regression/cbmc-incr-smt2/bitvector-bitwise-operators/byte-extract.c

@@ -0,0 +1,9 @@
+#include <assert.h>
+#include <stdint.h>
+
+int main()
+{
+  uint16_t x;
+  uint8_t *y = &x;
+  assert(y[0] == 0);
+}

regression/cbmc-incr-smt2/bitvector-bitwise-operators/byte-extract.desc

@@ -0,0 +1,8 @@
+CORE
+byte-extract.c
+--slice-formula
+\[main.assertion\.1\] line \d+ assertion y\[0\] == 0: FAILURE
+^EXIT=10$
+^SIGNAL=0$
+--
+--

regression/cbmc-incr-smt2/bitvector-bitwise-operators/byte-update-small.c

@@ -0,0 +1,13 @@
+#include <assert.h>
+#include <stdint.h>
+
+int main()
+{
+  uint8_t x[2];
+  x[0] = 0;
+  x[1] = 0;
+  uint16_t *y = x;
+  *y = 258;
+  assert(x[0] == 2);
+  assert(x[1] == 1);
+}

regression/cbmc-incr-smt2/bitvector-bitwise-operators/byte-update-small.desc

@@ -0,0 +1,9 @@
+CORE
+byte-update-small.c
+--slice-formula
+\[main\.assertion\.1\] line \d+ assertion x\[0\] == 2: SUCCESS
+\[main\.assertion\.2\] line \d+ assertion x\[1\] == 1: SUCCESS
+^EXIT=0$
+^SIGNAL=0$
+--
+--

regression/cbmc-incr-smt2/bitvector-bitwise-operators/byte-update.c

@@ -0,0 +1,10 @@
+#include <assert.h>
+#include <stdint.h>
+
+int main()
+{
+  uint16_t x = 0;
+  uint8_t *y = &x;
+  y[1] = 1;
+  assert(x == 256);
+}

regression/cbmc-incr-smt2/bitvector-bitwise-operators/byte-update.desc

@@ -0,0 +1,8 @@
+CORE
+byte-update.c
+--slice-formula
+\[main\.assertion\.1\] line \d+ assertion x == 256: SUCCESS
+^EXIT=0$
+^SIGNAL=0$
+--
+--

src/solvers/smt2_incremental/convert_expr_to_smt.cpp

@@ -367,7 +367,7 @@ static smt_termt convert_expr_to_smt(
   const bitand_exprt &bitwise_and_expr,
   const sub_expression_mapt &converted)
 {
-  if(operands_are_of_type<integer_bitvector_typet>(bitwise_and_expr))
+  if(operands_are_of_type<bitvector_typet>(bitwise_and_expr))
   {
     return convert_multiary_operator_to_terms(
       bitwise_and_expr, converted, smt_bit_vector_theoryt::make_and);
@@ -384,7 +384,7 @@ static smt_termt convert_expr_to_smt(
   const bitor_exprt &bitwise_or_expr,
   const sub_expression_mapt &converted)
 {
-  if(operands_are_of_type<integer_bitvector_typet>(bitwise_or_expr))
+  if(operands_are_of_type<bitvector_typet>(bitwise_or_expr))
   {
     return convert_multiary_operator_to_terms(
       bitwise_or_expr, converted, smt_bit_vector_theoryt::make_or);
@@ -401,7 +401,7 @@ static smt_termt convert_expr_to_smt(
   const bitxor_exprt &bitwise_xor,
   const sub_expression_mapt &converted)
 {
-  if(operands_are_of_type<integer_bitvector_typet>(bitwise_xor))
+  if(operands_are_of_type<bitvector_typet>(bitwise_xor))
   {
     return convert_multiary_operator_to_terms(
       bitwise_xor, converted, smt_bit_vector_theoryt::make_xor);
@@ -418,10 +418,7 @@ static smt_termt convert_expr_to_smt(
   const bitnot_exprt &bitwise_not,
   const sub_expression_mapt &converted)
 {
-  const bool operand_is_bitvector =
-    can_cast_type<integer_bitvector_typet>(bitwise_not.op().type());
-
-  if(operand_is_bitvector)
+  if(can_cast_type<bitvector_typet>(bitwise_not.op().type()))
   {
     return smt_bit_vector_theoryt::make_not(converted.at(bitwise_not.op()));
   }
@@ -436,9 +433,7 @@ static smt_termt convert_expr_to_smt(
   const unary_minus_exprt &unary_minus,
   const sub_expression_mapt &converted)
 {
-  const bool operand_is_bitvector =
-    can_cast_type<integer_bitvector_typet>(unary_minus.op().type());
-  if(operand_is_bitvector)
+  if(can_cast_type<integer_bitvector_typet>(unary_minus.op().type()))
   {
     return smt_bit_vector_theoryt::negate(converted.at(unary_minus.op()));
   }

src/solvers/smt2_incremental/smt2_incremental_decision_procedure.cpp

@@ -11,6 +11,7 @@
 #include <util/string_utils.h>
 #include <util/symbol.h>
 
+#include <solvers/lowering/expr_lowering.h>
 #include <solvers/smt2_incremental/ast/smt_commands.h>
 #include <solvers/smt2_incremental/ast/smt_responses.h>
 #include <solvers/smt2_incremental/ast/smt_terms.h>
@@ -257,19 +258,23 @@ smt2_incremental_decision_proceduret::smt2_incremental_decision_proceduret(
 }
 
 void smt2_incremental_decision_proceduret::ensure_handle_for_expr_defined(
-  const exprt &expr)
+  const exprt &in_expr)
 {
   if(
-    expression_handle_identifiers.find(expr) !=
+    expression_handle_identifiers.find(in_expr) !=
     expression_handle_identifiers.cend())
   {
     return;
   }
 
-  define_dependent_functions(expr);
+  const exprt lowered_expr = lower_byte_operators(in_expr, ns);
+
+  define_dependent_functions(lowered_expr);
   smt_define_function_commandt function{
-    "B" + std::to_string(handle_sequence()), {}, convert_expr_to_smt(expr)};
-  expression_handle_identifiers.emplace(expr, function.identifier());
+    "B" + std::to_string(handle_sequence()),
+    {},
+    convert_expr_to_smt(lowered_expr)};
+  expression_handle_identifiers.emplace(in_expr, function.identifier());
   identifier_table.emplace(
     function.identifier().identifier(), function.identifier());
   solver_process->send(function);
@@ -283,15 +288,23 @@ void smt2_incremental_decision_proceduret::define_index_identifiers(
       return;
     if(const auto with_expr = expr_try_dynamic_cast<with_exprt>(expr_node))
     {
-      const auto index_expr = with_expr->where();
-      const auto index_term = convert_expr_to_smt(index_expr);
-      const auto index_identifier = "index_" + std::to_string(index_sequence());
-      const auto index_definition =
-        smt_define_function_commandt{index_identifier, {}, index_term};
-      expression_identifiers.emplace(index_expr, index_definition.identifier());
-      identifier_table.emplace(index_identifier, index_definition.identifier());
-      solver_process->send(
-        smt_define_function_commandt{index_identifier, {}, index_term});
+      for(auto operand_ite = ++with_expr->operands().begin();
+          operand_ite != with_expr->operands().end();
+          operand_ite += 2)
+      {
+        const auto index_expr = *operand_ite;
+        const auto index_term = convert_expr_to_smt(index_expr);
+        const auto index_identifier =
+          "index_" + std::to_string(index_sequence());
+        const auto index_definition =
+          smt_define_function_commandt{index_identifier, {}, index_term};
+        expression_identifiers.emplace(
+          index_expr, index_definition.identifier());
+        identifier_table.emplace(
+          index_identifier, index_definition.identifier());
+        solver_process->send(
+          smt_define_function_commandt{index_identifier, {}, index_term});
+      }
     }
   });
 }
@@ -476,22 +489,25 @@ smt2_incremental_decision_proceduret::get_number_of_solver_calls() const
   return number_of_solver_calls;
 }
 
-void smt2_incremental_decision_proceduret::set_to(const exprt &expr, bool value)
+void smt2_incremental_decision_proceduret::set_to(
+  const exprt &in_expr,
+  bool value)
 {
-  PRECONDITION(can_cast_type<bool_typet>(expr.type()));
+  const exprt lowered_expr = lower_byte_operators(in_expr, ns);
+  PRECONDITION(can_cast_type<bool_typet>(lowered_expr.type()));
   log.conditional_output(log.debug(), [&](messaget::mstreamt &debug) {
     debug << "`set_to` (" << std::string{value ? "true" : "false"} << ") -\n  "
-          << expr.pretty(2, 0) << messaget::eom;
+          << lowered_expr.pretty(2, 0) << messaget::eom;
   });
 
-  define_dependent_functions(expr);
+  define_dependent_functions(lowered_expr);
   auto converted_term = [&]() -> smt_termt {
     const auto expression_handle_identifier =
-      expression_handle_identifiers.find(expr);
+      expression_handle_identifiers.find(lowered_expr);
     if(expression_handle_identifier != expression_handle_identifiers.cend())
       return expression_handle_identifier->second;
     else
-      return convert_expr_to_smt(expr);
+      return convert_expr_to_smt(lowered_expr);
   }();
   if(!value)
     converted_term = smt_core_theoryt::make_not(converted_term);