Add saturating addition/subtraction

Rust natively supports saturating arithmetic. For C code, it takes MMX
instructions to have access to this (which will be implemented in the next
commit), and even then it is limited to addition and subtraction. The
implementation now is equally restricted to these two arithmetic operations.

Fixes: #5841

Author: tautschnig

regression/cbmc/saturating_arithmetric/main.c

@@ -0,0 +1,17 @@
+#include <limits.h>
+
+int main()
+{
+  __CPROVER_assert(
+    __CPROVER_saturating_minus(INT_MIN, 1) == INT_MIN,
+    "subtracting from INT_MIN");
+  __CPROVER_assert(
+    __CPROVER_saturating_plus(LONG_MAX, 1l) == LONG_MAX, "adding to LONG_MAX");
+  __CPROVER_assert(
+    __CPROVER_saturating_minus(-1, INT_MIN) == INT_MAX, "no overflow");
+  __CPROVER_assert(
+    __CPROVER_saturating_plus(ULONG_MAX, 1ul) == ULONG_MAX,
+    "adding to ULONG_MAX");
+  __CPROVER_assert(
+    __CPROVER_saturating_minus(10ul, ULONG_MAX) == 0, "subtracting ULONG_MAX");
+}

regression/cbmc/saturating_arithmetric/output-formula.desc

@@ -0,0 +1,9 @@
+CORE
+main.c
+--program-only
+ASSERT\(__CPROVER_saturating_minus\(.*\)
+ASSERT\(__CPROVER_saturating_plus\(.*\)
+^EXIT=0$
+^SIGNAL=0$
+--
+^warning: ignoring

regression/cbmc/saturating_arithmetric/output-goto.desc

@@ -0,0 +1,9 @@
+CORE
+main.c
+--show-goto-functions
+ASSERT saturating-\(.*\)
+ASSERT saturating\+\(.*\)
+^EXIT=0$
+^SIGNAL=0$
+--
+^warning: ignoring

regression/cbmc/saturating_arithmetric/test.desc

@@ -0,0 +1,8 @@
+CORE broken-smt-backend
+main.c
+
+^EXIT=0$
+^SIGNAL=0$
+^VERIFICATION SUCCESSFUL$
+--
+^warning: ignoring

regression/validate-trace-xml-schema/check.py

@@ -29,13 +29,15 @@
     ['enum_is_in_range', 'format.desc'],
     ['r_w_ok9', 'simplify.desc'],
     ['reachability-slice-interproc2', 'test.desc'],
+    ['saturating_arithmetric', 'output-goto.desc'],
     # this one wants show-properties instead producing a trace
     ['show_properties1', 'test.desc'],
     # program-only instead of trace
     ['vla1', 'program-only.desc'],
     ['Pointer_Arithmetic19', 'test.desc'],
     ['Quantifiers-simplify', 'simplify_not_forall.desc'],
     ['array-cell-sensitivity15', 'test.desc'],
+    ['saturating_arithmetric', 'output-formula.desc'],
     # these test for invalid command line handling
     ['bad_option', 'test_multiple.desc'],
     ['bad_option', 'test.desc'],

src/ansi-c/c_typecheck_base.h

@@ -205,6 +205,8 @@ class c_typecheck_baset:
   exprt typecheck_builtin_overflow(
     side_effect_expr_function_callt &expr,
     const irep_idt &arith_op);
+  exprt
+  typecheck_saturating_arithmetic(const side_effect_expr_function_callt &expr);
   virtual optionalt<symbol_exprt> typecheck_gcc_polymorphic_builtin(
     const irep_idt &identifier,
     const exprt::operandst &arguments,

src/ansi-c/c_typecheck_expr.cpp

@@ -1967,6 +1967,15 @@ void c_typecheck_baset::typecheck_side_effect_function_call(
 
         return;
       }
+      else if(
+        identifier == CPROVER_PREFIX "saturating_minus" ||
+        identifier == CPROVER_PREFIX "saturating_plus")
+      {
+        exprt result = typecheck_saturating_arithmetic(expr);
+        expr.swap(result);
+
+        return;
+      }
       else if(
         auto gcc_polymorphic = typecheck_gcc_polymorphic_builtin(
           identifier, expr.arguments(), f_op.source_location()))
@@ -3298,6 +3307,35 @@ exprt c_typecheck_baset::typecheck_builtin_overflow(
                                     expr.source_location()};
 }
 
+exprt c_typecheck_baset::typecheck_saturating_arithmetic(
+  const side_effect_expr_function_callt &expr)
+{
+  const irep_idt &identifier = to_symbol_expr(expr.function()).get_identifier();
+
+  // check function signature
+  if(expr.arguments().size() != 2)
+  {
+    std::ostringstream error_message;
+    error_message << expr.source_location().as_string() << ": " << identifier
+                  << " takes exactly two arguments, but "
+                  << expr.arguments().size() << " were provided";
+    throw invalid_source_file_exceptiont{error_message.str()};
+  }
+
+  exprt result;
+  if(identifier == CPROVER_PREFIX "saturating_minus")
+    result = saturating_minus_exprt{expr.arguments()[0], expr.arguments()[1]};
+  else if(identifier == CPROVER_PREFIX "saturating_plus")
+    result = saturating_plus_exprt{expr.arguments()[0], expr.arguments()[1]};
+  else
+    UNREACHABLE;
+
+  typecheck_expr_binary_arithmetic(result);
+  result.add_source_location() = expr.source_location();
+
+  return result;
+}
+
 /// Typecheck the parameters in a function call expression, and where
 /// necessary, make implicit casts around parameters explicit.
 void c_typecheck_baset::typecheck_function_call_arguments(
@@ -3499,9 +3537,15 @@ void c_typecheck_baset::typecheck_expr_binary_arithmetic(exprt &expr)
     return;
   }
 
-  // promote!
-
-  implicit_typecast_arithmetic(op0, op1);
+  if(expr.id() == ID_saturating_minus || expr.id() == ID_saturating_plus)
+  {
+    implicit_typecast(op1, o_type0);
+  }
+  else
+  {
+    // promote!
+    implicit_typecast_arithmetic(op0, op1);
+  }
 
   const typet &type0 = op0.type();
   const typet &type1 = op1.type();
@@ -3562,6 +3606,16 @@ void c_typecheck_baset::typecheck_expr_binary_arithmetic(exprt &expr)
       }
     }
   }
+  else if(expr.id() == ID_saturating_minus || expr.id() == ID_saturating_plus)
+  {
+    if(
+      type0 == type1 &&
+      (type0.id() == ID_signedbv || type0.id() == ID_unsignedbv))
+    {
+      expr.type() = type0;
+      return;
+    }
+  }
 
   error().source_location = expr.source_location();
   error() << "operator '" << expr.id() << "' not defined for types '"

src/ansi-c/expr2c.cpp

@@ -3977,6 +3977,8 @@ optionalt<std::string> expr2ct::convert_function(const exprt &src)
     {ID_object_size, "OBJECT_SIZE"},
     {ID_pointer_object, "POINTER_OBJECT"},
     {ID_pointer_offset, "POINTER_OFFSET"},
+    {ID_saturating_minus, CPROVER_PREFIX "saturating_minus"},
+    {ID_saturating_plus, CPROVER_PREFIX "saturating_plus"},
     {ID_r_ok, "R_OK"},
     {ID_w_ok, "W_OK"},
     {ID_rw_ok, "RW_OK"},

src/solvers/flattening/boolbv.cpp

@@ -229,6 +229,8 @@ bvt boolbvt::convert_bitvector(const exprt &expr)
   }
   else if(expr.id() == ID_bitreverse)
     return convert_bitreverse(to_bitreverse_expr(expr));
+  else if(expr.id() == ID_saturating_minus || expr.id() == ID_saturating_plus)
+    return convert_saturating_add_sub(to_binary_expr(expr));
 
   return conversion_failed(expr);
 }

src/solvers/flattening/boolbv.h

@@ -194,6 +194,7 @@ class boolbvt:public arrayst
   virtual bvt convert_function_application(
     const function_application_exprt &expr);
   virtual bvt convert_bitreverse(const bitreverse_exprt &expr);
+  virtual bvt convert_saturating_add_sub(const binary_exprt &expr);
 
   virtual exprt make_bv_expr(const typet &type, const bvt &bv);
   virtual exprt make_free_bv_expr(const typet &type);

src/solvers/flattening/boolbv_add_sub.cpp

@@ -142,3 +142,92 @@ bvt boolbvt::convert_add_sub(const exprt &expr)
 
   return bv;
 }
+
+bvt boolbvt::convert_saturating_add_sub(const binary_exprt &expr)
+{
+  PRECONDITION(
+    expr.id() == ID_saturating_minus || expr.id() == ID_saturating_plus);
+
+  const typet &type = expr.type();
+
+  if(
+    type.id() != ID_unsignedbv && type.id() != ID_signedbv &&
+    type.id() != ID_fixedbv && type.id() != ID_complex &&
+    type.id() != ID_vector)
+  {
+    return conversion_failed(expr);
+  }
+
+  std::size_t width = boolbv_width(type);
+
+  if(width == 0)
+    return conversion_failed(expr);
+
+  DATA_INVARIANT(
+    expr.lhs().type() == type && expr.rhs().type() == type,
+    "saturating add/sub with mixed types:\n" + expr.pretty());
+
+  const bool subtract = expr.id() == ID_saturating_minus;
+
+  typet arithmetic_type = (type.id() == ID_vector || type.id() == ID_complex)
+                            ? to_type_with_subtype(type).subtype()
+                            : type;
+
+  bv_utilst::representationt rep =
+    (arithmetic_type.id() == ID_signedbv || arithmetic_type.id() == ID_fixedbv)
+      ? bv_utilst::representationt::SIGNED
+      : bv_utilst::representationt::UNSIGNED;
+
+  bvt bv = convert_bv(expr.lhs(), width);
+  const bvt &op = convert_bv(expr.rhs(), width);
+
+  if(type.id() != ID_vector && type.id() != ID_complex)
+    return bv_utils.saturating_add_sub(bv, op, subtract, rep);
+
+  std::size_t sub_width = boolbv_width(to_type_with_subtype(type).subtype());
+
+  INVARIANT(sub_width != 0, "vector elements shall have nonzero bit width");
+  INVARIANT(
+    width % sub_width == 0,
+    "total vector bit width shall be a multiple of the element bit width");
+
+  std::size_t size = width / sub_width;
+
+  for(std::size_t i = 0; i < size; i++)
+  {
+    bvt tmp_op;
+    tmp_op.resize(sub_width);
+
+    for(std::size_t j = 0; j < tmp_op.size(); j++)
+    {
+      const std::size_t index = i * sub_width + j;
+      INVARIANT(index < op.size(), "bit index shall be within bounds");
+      tmp_op[j] = op[index];
+    }
+
+    bvt tmp_result;
+    tmp_result.resize(sub_width);
+
+    for(std::size_t j = 0; j < tmp_result.size(); j++)
+    {
+      const std::size_t index = i * sub_width + j;
+      INVARIANT(index < bv.size(), "bit index shall be within bounds");
+      tmp_result[j] = bv[index];
+    }
+
+    tmp_result = bv_utils.saturating_add_sub(tmp_result, tmp_op, subtract, rep);
+
+    INVARIANT(
+      tmp_result.size() == sub_width,
+      "applying the add/sub operation shall not change the bitwidth");
+
+    for(std::size_t j = 0; j < tmp_result.size(); j++)
+    {
+      const std::size_t index = i * sub_width + j;
+      INVARIANT(index < bv.size(), "bit index shall be within bounds");
+      bv[index] = tmp_result[j];
+    }
+  }
+
+  return bv;
+}

src/solvers/flattening/bv_utils.cpp

@@ -360,6 +360,76 @@ bvt bv_utilst::add_sub(const bvt &op0, const bvt &op1, literalt subtract)
   return result;
 }
 
+bvt bv_utilst::saturating_add_sub(
+  const bvt &op0,
+  const bvt &op1,
+  bool subtract,
+  representationt rep)
+{
+  PRECONDITION(op0.size() == op1.size());
+  PRECONDITION(
+    rep == representationt::SIGNED || rep == representationt::UNSIGNED);
+
+  literalt carry_in = const_literal(subtract);
+  literalt carry_out;
+
+  bvt add_sub_result = op0;
+  bvt tmp_op1 = subtract ? inverted(op1) : op1;
+
+  adder(add_sub_result, tmp_op1, carry_in, carry_out);
+
+  bvt result;
+  result.reserve(add_sub_result.size());
+  if(rep == representationt::UNSIGNED)
+  {
+    // An unsigned overflow has occurred when carry_out is not equal to
+    // subtract: addition with a carry-out means an overflow beyond the maximum
+    // representable value, subtraction without a carry-out means an underflow
+    // below zero. For saturating arithmetic the former implies that all bits
+    // should be set to 1, in the latter case all bits should be set to zero.
+    for(const auto &literal : add_sub_result)
+    {
+      result.push_back(
+        subtract ? prop.land(literal, carry_out)
+                 : prop.lor(literal, carry_out));
+    }
+  }
+  else
+  {
+    // A signed overflow beyond the maximum representable value occurs when
+    // adding two positive numbers and the wrap-around result being negative, or
+    // when subtracting a negative from a positive number (and, again, the
+    // result being negative).
+    literalt overflow_to_max_int = prop.land(bvt{
+      !sign_bit(op0),
+      subtract ? sign_bit(op1) : !sign_bit(op1),
+      sign_bit(add_sub_result)});
+    // A signed underflow below the minimum representable value occurs when
+    // adding two negative numbers and arriving at a positive result, or
+    // subtracting a positive from a negative number (and, again, obtaining a
+    // positive wrap-around result).
+    literalt overflow_to_min_int = prop.land(bvt{
+      sign_bit(op0),
+      subtract ? !sign_bit(op1) : sign_bit(op1),
+      !sign_bit(add_sub_result)});
+
+    // set all bits except for the sign bit
+    PRECONDITION(!add_sub_result.empty());
+    for(std::size_t i = 0; i < add_sub_result.size() - 1; ++i)
+    {
+      const auto &literal = add_sub_result[i];
+      result.push_back(prop.land(
+        prop.lor(overflow_to_max_int, literal), !overflow_to_min_int));
+    }
+    // finally add the sign bit
+    result.push_back(prop.land(
+      prop.lor(overflow_to_min_int, add_sub_result.back()),
+      !overflow_to_max_int));
+  }
+
+  return result;
+}
+
 literalt bv_utilst::overflow_add(
   const bvt &op0, const bvt &op1, representationt rep)
 {

src/solvers/flattening/bv_utils.h

@@ -57,6 +57,11 @@ class bv_utilst
     const bvt &op1,
     bool subtract,
     representationt rep);
+  bvt saturating_add_sub(
+    const bvt &op0,
+    const bvt &op1,
+    bool subtract,
+    representationt rep);
 
   bvt add(const bvt &op0, const bvt &op1) { return add_sub(op0, op1, false); }
   bvt sub(const bvt &op0, const bvt &op1) { return add_sub(op0, op1, true); }