Use byte_update lowering in SMT2 conversion

tautschnig · tautschnig · commit 8209c9a5d08a · 2019-02-21T17:21:12.000Z
The locally implemented lowering was very incomplete.
diff --git a/regression/cbmc/Endianness4/test.desc b/regression/cbmc/Endianness4/test.desc
@@ -1,4 +1,4 @@
-CORE broken-smt-backend
+CORE
 main.c
 
 ^EXIT=0$
diff --git a/regression/cbmc/Endianness6/test.desc b/regression/cbmc/Endianness6/test.desc
@@ -1,4 +1,4 @@
-CORE broken-smt-backend
+CORE
 main.c
 --big-endian
 ^EXIT=0$
diff --git a/regression/cbmc/Pointer_byte_extract5/no-simplify.desc b/regression/cbmc/Pointer_byte_extract5/no-simplify.desc
@@ -1,4 +1,4 @@
-CORE broken-smt-backend
+CORE
 main.i
 --bounds-check --32 --no-simplify
 ^EXIT=10$
diff --git a/regression/cbmc/Pointer_byte_extract5/test.desc b/regression/cbmc/Pointer_byte_extract5/test.desc
@@ -1,4 +1,4 @@
-CORE broken-smt-backend
+CORE
 main.i
 --bounds-check --32
 ^EXIT=10$
diff --git a/regression/cbmc/Pointer_byte_extract9/test.desc b/regression/cbmc/Pointer_byte_extract9/test.desc
@@ -1,4 +1,4 @@
-CORE broken-smt-backend
+CORE
 main.c
 
 ^EXIT=10$
diff --git a/regression/cbmc/Promotion3/test.desc b/regression/cbmc/Promotion3/test.desc
@@ -1,4 +1,4 @@
-CORE
+CORE broken-smt-backend
 main.c
 
 ^EXIT=0$
diff --git a/regression/cbmc/array_constraints1/test.desc b/regression/cbmc/array_constraints1/test.desc
@@ -1,4 +1,4 @@
-CORE broken-smt-backend
+CORE
 main.c
 --unwind 2 --pointer-check
 ^EXIT=10$
diff --git a/regression/cbmc/byte_update2/test.desc b/regression/cbmc/byte_update2/test.desc
@@ -1,4 +1,4 @@
-CORE broken-smt-backend
+CORE
 main.c
 --little-endian
 ^EXIT=0$
diff --git a/regression/cbmc/byte_update3/test.desc b/regression/cbmc/byte_update3/test.desc
@@ -1,4 +1,4 @@
-CORE broken-smt-backend
+CORE
 main.c
 --little-endian
 ^EXIT=0$
diff --git a/regression/cbmc/byte_update4/test.desc b/regression/cbmc/byte_update4/test.desc
@@ -1,4 +1,4 @@
-CORE broken-smt-backend
+CORE
 main.c
 --little-endian
 ^EXIT=0$
diff --git a/regression/cbmc/byte_update5/test.desc b/regression/cbmc/byte_update5/test.desc
@@ -1,4 +1,4 @@
-CORE broken-smt-backend
+CORE
 main.c
 --little-endian
 ^EXIT=0$
diff --git a/regression/cbmc/byte_update6/test.desc b/regression/cbmc/byte_update6/test.desc
@@ -1,4 +1,4 @@
-CORE broken-smt-backend
+CORE
 main.c
 --little-endian
 ^EXIT=0$
diff --git a/regression/cbmc/byte_update7/test.desc b/regression/cbmc/byte_update7/test.desc
@@ -1,4 +1,4 @@
-CORE broken-smt-backend
+CORE
 main.c
 --little-endian
 ^EXIT=0$
diff --git a/regression/cbmc/byte_update8/test.desc b/regression/cbmc/byte_update8/test.desc
@@ -1,4 +1,4 @@
-CORE broken-smt-backend
+CORE
 main.c
 --little-endian
 ^EXIT=0$
diff --git a/regression/cbmc/byte_update9/test.desc b/regression/cbmc/byte_update9/test.desc
@@ -1,4 +1,4 @@
-CORE broken-smt-backend
+CORE
 main.c
 --big-endian
 ^EXIT=0$
diff --git a/regression/cbmc/gcc_c99-bool-1/test.desc b/regression/cbmc/gcc_c99-bool-1/test.desc
@@ -1,4 +1,4 @@
-CORE
+CORE broken-smt-backend
 c99-bool-1.c
 
 ^EXIT=0$
diff --git a/regression/cbmc/memory_allocation1/test.desc b/regression/cbmc/memory_allocation1/test.desc
@@ -1,4 +1,4 @@
-CORE broken-smt-backend
+CORE
 main.c
 --pointer-check
 ^EXIT=10$
diff --git a/regression/cbmc/scanf1/test.desc b/regression/cbmc/scanf1/test.desc
@@ -1,4 +1,4 @@
-CORE broken-smt-backend
+CORE
 main.i
 --little-endian
 ^EXIT=10$
diff --git a/regression/cbmc/struct6/test.desc b/regression/cbmc/struct6/test.desc
@@ -1,4 +1,4 @@
-CORE broken-smt-backend
+CORE
 main.c
 --bounds-check --pointer-check
 ^EXIT=0$
diff --git a/regression/cbmc/union12/test.desc b/regression/cbmc/union12/test.desc
@@ -1,4 +1,4 @@
-CORE broken-smt-backend
+CORE
 main.c
 --pointer-check
 ^EXIT=10$
diff --git a/regression/cbmc/union6/test.desc b/regression/cbmc/union6/test.desc
@@ -1,8 +1,11 @@
-CORE
+CORE broken-smt-backend
 main.c
 --little-endian
 ^EXIT=0$
 ^SIGNAL=0$
 ^VERIFICATION SUCCESSFUL$
 --
 ^warning: ignoring
+--
+This test reports a VERIFICATION ERROR when running with the SMT2 solver on
+Windows only.
diff --git a/regression/cbmc/union7/test.desc b/regression/cbmc/union7/test.desc
@@ -6,3 +6,6 @@ main.c
 ^VERIFICATION SUCCESSFUL$
 --
 ^warning: ignoring
+--
+This test reports a VERIFICATION ERROR when running with the SMT2 solver on
+Windows only.
diff --git a/regression/cbmc/union9/test.desc b/regression/cbmc/union9/test.desc
@@ -1,4 +1,4 @@
-CORE broken-smt-backend
+CORE
 main.c
 
 ^EXIT=0$
diff --git a/src/solvers/smt2/smt2_conv.cpp b/src/solvers/smt2/smt2_conv.cpp
@@ -622,102 +622,11 @@ void smt2_convt::convert_byte_extract(const byte_extract_exprt &expr)
 
 void smt2_convt::convert_byte_update(const byte_update_exprt &expr)
 {
-  #if 0
-  // The situation: expr.op0 needs to be split in 3 parts
-  // |<--- L --->|<--- M --->|<--- R --->|
-  // where M is the expr.op1'th byte
-  // We need to output L expr.op2 R
-
-  mp_integer i = numeric_cast_v<mp_integer>(expr.op());
-
-  std::size_t total_width=boolbv_width(expr.op().type());
-  CHECK_RETURN_WITH_DIAGNOSTICS(
-    total_width != 0,
-    "failed to get width of byte_update");
-
-  std::size_t value_width=boolbv_width(expr.value().type());
-
-  mp_integer upper, lower; // of the byte
-  mp_integer max=total_width-1;
-
-  if(expr.id()==ID_byte_update_little_endian)
-  {
-    lower = i*8;
-    upper = lower+value_width-1;
-  }
-  else if(expr.id()==ID_byte_update_big_endian)
-  {
-    upper = max-(i*8);
-    lower = max-((i+1)*8-1);
-  }
-  else
-    UNEXPECTEDCASE("byte update neither big nor little endian");
-
-  unflatten(BEGIN, expr.type());
-
-  if(upper==max)
-  {
-    if(lower==0) // the update expression is expr.value()
-    {
-      flatten2bv(expr.value());
-    }
-    else // uppermost byte selected, only R needed
-    {
-      out << "(concat ";
-      flatten2bv(expr.value());
-      out << " ((_ extract " << lower-1 << " 0) ";
-      flatten2bv(expr.op());
-      out << "))";
-    }
-  }
-  else
-  {
-    if(lower==0) // lowermost byte selected, only L needed
-    {
-      out << "(concat ";
-      out << "((_ extract " << max << " " << (upper+1) << ") ";
-      flatten2bv(expr.op());
-      out << ") ";
-      flatten2bv(expr.value());
-      out << ")";
-    }
-    else // byte in the middle selected, L & R needed
-    {
-      out << "(concat (concat ";
-      out << "((_ extract " << max << " " << (upper+1) << ") ";
-      flatten2bv(expr.op());
-      out << ") ";
-      flatten2bv(expr.value());
-      out << ") ((_ extract " << (lower-1) << " 0) ";
-      flatten2bv(expr.op());
-      out << "))";
-    }
-  }
-
-  unflatten(END, expr.type());
-
-  #else
-
-  // We'll do an AND-mask for op(), and then OR-in
-  // the value() shifted by the offset * 8.
-
-  std::size_t total_width=boolbv_width(expr.op().type());
-  std::size_t value_width=boolbv_width(expr.value().type());
-
-  mp_integer mask=power(2, value_width)-1;
-  exprt one_mask=from_integer(mask, unsignedbv_typet(total_width));
-
-  const mult_exprt distance(
-    expr.offset(), from_integer(8, expr.offset().type()));
-
-  const bitand_exprt and_expr(expr.op(), bitnot_exprt(one_mask));
-  const typecast_exprt ext_value(expr.value(), one_mask.type());
-  const bitor_exprt or_expr(and_expr, shl_exprt(ext_value, distance));
-
+  // we just run the flattener
+  exprt flattened_expr = lower_byte_update(expr, ns);
   unflatten(wheret::BEGIN, expr.type());
-  flatten2bv(or_expr);
+  convert_expr(flattened_expr);
   unflatten(wheret::END, expr.type());
-  #endif
 }
 
 literalt smt2_convt::convert(const exprt &expr)

Original file line number	Diff line number	Diff line change
`@@ -1,4 +1,4 @@`
`1`		`-CORE broken-smt-backend`
	`1`	`+CORE`
`2`	`2`	`main.c`
`3`	`3`
`4`	`4`	`^EXIT=0$`
Original file line number	Diff line number	Diff line change
`@@ -1,4 +1,4 @@`
`1`		`-CORE`
	`1`	`+CORE broken-smt-backend`
`2`	`2`	`main.c`
`3`	`3`
`4`	`4`	`^EXIT=0$`