Add saturating addition/subtraction

regression/cbmc/SIMD1/main.c

@@ -1,6 +1,11 @@
 #include <assert.h>
+#include <limits.h>
+
 #ifdef _MSC_VER
 #  include <intrin.h>
+#  ifdef _WIN64
+#    define _mm_extract_pi16(a, b) _mm_extract_epi16(a, b)
+#  endif
 #else
 #  include <immintrin.h>
 #endif
@@ -10,5 +15,44 @@ int main()
   __m128i values = _mm_setr_epi32(0x1234, 0x2345, 0x3456, 0x4567);
   int val1 = _mm_extract_epi32(values, 0);
   assert(val1 == 0x1234);
+
+#ifndef _WIN64
+  __m64 a = _mm_setr_pi16(SHRT_MIN, 10, SHRT_MIN + 1, SHRT_MAX);
+  __m64 b = _mm_set_pi16(1, 1, 10, 1);
+  __m64 result = _mm_subs_pi16(a, b);
+#else
+  __m128i a = _mm_setr_epi16(SHRT_MIN, 10, SHRT_MIN + 1, SHRT_MAX, 0, 0, 0, 0);
+  __m128i b = _mm_set_epi16(0, 0, 0, 0, 1, 1, 10, 1);
+  __m128i result = _mm_subs_epi16(a, b);
+#endif
+  short s1 = _mm_extract_pi16(result, 0);
+  assert(s1 == SHRT_MIN);
+  short s2 = _mm_extract_pi16(result, 1);
+  assert(s2 == 0);
+  short s3 = _mm_extract_pi16(result, 2);
+  assert(s3 == SHRT_MIN);
+  short s4 = _mm_extract_pi16(result, 3);
+  assert(s4 == SHRT_MAX - 1);
+
+#ifndef _WIN64
+  result = _mm_adds_pi16(a, b);
+#else
+  result = _mm_adds_epi16(a, b);
+#endif
+  s1 = _mm_extract_pi16(result, 0);
+  assert(s1 == SHRT_MIN + 1);
+  s2 = _mm_extract_pi16(result, 1);
+  assert(s2 == 20);
+  s3 = _mm_extract_pi16(result, 2);
+  assert(s3 == SHRT_MIN + 2);
+  s4 = _mm_extract_pi16(result, 3);
+  assert(s4 == SHRT_MAX);
+
+  __m128i x = _mm_set_epi16(0, 0, 0, 0, 0, 0, 0, 0);
+  __m128i y = _mm_setr_epi16(1, 0, 0, 0, 0, 0, 0, 0);
+  __m128i result128 = _mm_subs_epu16(x, y);
+  short s = _mm_extract_epi16(result128, 0);
+  assert(s == 0);
+
   return 0;
 }

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/ansi-c/library/gcc.c

@@ -192,6 +192,24 @@ __CPROVER_HIDE:;
   return size <= sizeof(__CPROVER_size_t);
 }
 
+/* FUNCTION: __builtin_ia32_vec_ext_v4hi */
+
+typedef short __gcc_v4hi __attribute__((__vector_size__(8)));
+
+short __builtin_ia32_vec_ext_v4hi(__gcc_v4hi vec, int offset)
+{
+  return *((short *)&vec + offset);
+}
+
+/* FUNCTION: __builtin_ia32_vec_ext_v8hi */
+
+typedef short __gcc_v8hi __attribute__((__vector_size__(16)));
+
+short __builtin_ia32_vec_ext_v8hi(__gcc_v8hi vec, int offset)
+{
+  return *((short *)&vec + offset);
+}
+
 /* FUNCTION: __builtin_ia32_vec_ext_v4si */
 
 typedef int __gcc_v4si __attribute__((__vector_size__(16)));
@@ -227,3 +245,70 @@ float __builtin_ia32_vec_ext_v4sf(__gcc_v4sf vec, int offset)
 {
   return *((float *)&vec + offset);
 }
+
+/* FUNCTION: __builtin_ia32_psubsw128 */
+
+#ifndef LIBRARY_CHECK
+typedef short __gcc_v8hi __attribute__((__vector_size__(16)));
+#else
+__gcc_v8hi __CPROVER_saturating_minus();
+#endif
+
+__gcc_v8hi __builtin_ia32_psubsw128(__gcc_v8hi a, __gcc_v8hi b)
+{
+  return __CPROVER_saturating_minus(a, b);
+}
+
+/* FUNCTION: __builtin_ia32_psubusw128 */
+
+#ifndef LIBRARY_CHECK
+typedef short __gcc_v8hi __attribute__((__vector_size__(16)));
+#endif
+
+__gcc_v8hi __builtin_ia32_psubusw128(__gcc_v8hi a, __gcc_v8hi b)
+{
+  typedef unsigned short v8hi_u __attribute__((__vector_size__(16)));
+  return (__gcc_v8hi)__CPROVER_saturating_minus((v8hi_u)a, (v8hi_u)b);
+}
+
+/* FUNCTION: __builtin_ia32_paddsw */
+
+#ifndef LIBRARY_CHECK
+typedef short __gcc_v4hi __attribute__((__vector_size__(8)));
+#else
+__gcc_v4hi __CPROVER_saturating_plus();
+#endif
+
+__gcc_v4hi __builtin_ia32_paddsw(__gcc_v4hi a, __gcc_v4hi b)
+{
+  return __CPROVER_saturating_plus(a, b);
+}
+
+/* FUNCTION: __builtin_ia32_psubsw */
+
+#ifndef LIBRARY_CHECK
+typedef short __gcc_v4hi __attribute__((__vector_size__(8)));
+#else
+__gcc_v4hi __CPROVER_saturating_minus_v4hi(__gcc_v4hi, __gcc_v4hi);
+#  define __CPROVER_saturating_minus __CPROVER_saturating_minus_v4hi
+#endif
+
+__gcc_v4hi __builtin_ia32_psubsw(__gcc_v4hi a, __gcc_v4hi b)
+{
+  return __CPROVER_saturating_minus(a, b);
+}
+
+#ifdef LIBRARY_CHECK
+#  undef __CPROVER_saturating_minus
+#endif
+
+/* FUNCTION: __builtin_ia32_vec_init_v4hi */
+
+#ifndef LIBRARY_CHECK
+typedef short __gcc_v4hi __attribute__((__vector_size__(8)));
+#endif
+
+__gcc_v4hi __builtin_ia32_vec_init_v4hi(short e0, short e1, short e2, short e3)
+{
+  return (__gcc_v4hi){e0, e1, e2, e3};
+}