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.

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/test.desc

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

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(
@@ -3523,7 +3561,9 @@ void c_typecheck_baset::typecheck_expr_binary_arithmetic(exprt &expr)
       }
     }
   }
-  else if(expr.id()==ID_mod)
+  else if(
+    expr.id() == ID_mod || expr.id() == ID_saturating_minus ||
+    expr.id() == ID_saturating_plus)
   {
     if(type0==type1)
     {

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,61 @@ 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)
+  {
+    for(const auto &literal : add_sub_result)
+    {
+      result.push_back(
+        subtract ? prop.land(literal, carry_out)
+                 : prop.lor(literal, carry_out));
+    }
+  }
+  else
+  {
+    literalt overflow_to_max_int = prop.land(bvt{
+      !sign_bit(op0),
+      subtract ? sign_bit(op1) : !sign_bit(op1),
+      sign_bit(add_sub_result)});
+    literalt overflow_to_min_int = prop.land(bvt{
+      sign_bit(op0),
+      subtract ? !sign_bit(op1) : sign_bit(op1),
+      !sign_bit(add_sub_result)});
+
+    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));
+    }
+    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); }

src/util/bitvector_expr.h

@@ -1056,4 +1056,103 @@ inline bitreverse_exprt &to_bitreverse_expr(exprt &expr)
   return ret;
 }
 
+/// \brief The saturating plus expression
+class saturating_plus_exprt : public binary_exprt
+{
+public:
+  saturating_plus_exprt(exprt _lhs, exprt _rhs)
+    : binary_exprt(std::move(_lhs), ID_saturating_plus, std::move(_rhs))
+  {
+  }
+
+  saturating_plus_exprt(exprt _lhs, exprt _rhs, typet _type)
+    : binary_exprt(
+        std::move(_lhs),
+        ID_saturating_plus,
+        std::move(_rhs),
+        std::move(_type))
+  {
+  }
+};
+
+template <>
+inline bool can_cast_expr<saturating_plus_exprt>(const exprt &base)
+{
+  return base.id() == ID_saturating_plus;
+}
+
+inline void validate_expr(const saturating_plus_exprt &value)
+{
+  validate_operands(value, 2, "saturating plus must have two operands");
+}
+
+/// \brief Cast an exprt to a \ref saturating_plus_exprt
+///
+/// \a expr must be known to be \ref saturating_plus_exprt.
+///
+/// \param expr: Source expression
+/// \return Object of type \ref saturating_plus_exprt
+inline const saturating_plus_exprt &to_saturating_plus_expr(const exprt &expr)
+{
+  PRECONDITION(expr.id() == ID_saturating_plus);
+  const saturating_plus_exprt &ret =
+    static_cast<const saturating_plus_exprt &>(expr);
+  validate_expr(ret);
+  return ret;
+}
+
+/// \copydoc to_saturating_plus_expr(const exprt &)
+inline saturating_plus_exprt &to_saturating_plus_expr(exprt &expr)
+{
+  PRECONDITION(expr.id() == ID_saturating_plus);
+  saturating_plus_exprt &ret = static_cast<saturating_plus_exprt &>(expr);
+  validate_expr(ret);
+  return ret;
+}
+
+/// \brief Saturating subtraction expression.
+class saturating_minus_exprt : public binary_exprt
+{
+public:
+  saturating_minus_exprt(exprt _lhs, exprt _rhs)
+    : binary_exprt(std::move(_lhs), ID_saturating_minus, std::move(_rhs))
+  {
+  }
+};
+
+template <>
+inline bool can_cast_expr<saturating_minus_exprt>(const exprt &base)
+{
+  return base.id() == ID_saturating_minus;
+}
+
+inline void validate_expr(const saturating_minus_exprt &value)
+{
+  validate_operands(value, 2, "saturating minus must have two operands");
+}
+
+/// \brief Cast an exprt to a \ref saturating_minus_exprt
+///
+/// \a expr must be known to be \ref saturating_minus_exprt.
+///
+/// \param expr: Source expression
+/// \return Object of type \ref saturating_minus_exprt
+inline const saturating_minus_exprt &to_saturating_minus_expr(const exprt &expr)
+{
+  PRECONDITION(expr.id() == ID_saturating_minus);
+  const saturating_minus_exprt &ret =
+    static_cast<const saturating_minus_exprt &>(expr);
+  validate_expr(ret);
+  return ret;
+}
+
+/// \copydoc to_saturating_minus_expr(const exprt &)
+inline saturating_minus_exprt &to_saturating_minus_expr(exprt &expr)
+{
+  PRECONDITION(expr.id() == ID_saturating_minus);
+  saturating_minus_exprt &ret = static_cast<saturating_minus_exprt &>(expr);
+  validate_expr(ret);
+  return ret;
+}
+
 #endif // CPROVER_UTIL_BITVECTOR_EXPR_H