diff --git a/regression/cbmc/SIMD1/main.c b/regression/cbmc/SIMD1/main.c index 3bd22ded54a..e65431c7156 100644 --- a/regression/cbmc/SIMD1/main.c +++ b/regression/cbmc/SIMD1/main.c @@ -1,6 +1,11 @@ #include +#include + #ifdef _MSC_VER # include +# ifdef _WIN64 +# define _mm_extract_pi16(a, b) _mm_extract_epi16(a, b) +# endif #else # include #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; } diff --git a/regression/cbmc/saturating_arithmetric/main.c b/regression/cbmc/saturating_arithmetric/main.c new file mode 100644 index 00000000000..5e568f95372 --- /dev/null +++ b/regression/cbmc/saturating_arithmetric/main.c @@ -0,0 +1,17 @@ +#include + +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"); +} diff --git a/regression/cbmc/saturating_arithmetric/output-formula.desc b/regression/cbmc/saturating_arithmetric/output-formula.desc new file mode 100644 index 00000000000..11d26aada17 --- /dev/null +++ b/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 diff --git a/regression/cbmc/saturating_arithmetric/output-goto.desc b/regression/cbmc/saturating_arithmetric/output-goto.desc new file mode 100644 index 00000000000..fc144ed0a24 --- /dev/null +++ b/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 diff --git a/regression/cbmc/saturating_arithmetric/test.desc b/regression/cbmc/saturating_arithmetric/test.desc new file mode 100644 index 00000000000..39d9265e8a7 --- /dev/null +++ b/regression/cbmc/saturating_arithmetric/test.desc @@ -0,0 +1,8 @@ +CORE broken-smt-backend +main.c + +^EXIT=0$ +^SIGNAL=0$ +^VERIFICATION SUCCESSFUL$ +-- +^warning: ignoring diff --git a/regression/validate-trace-xml-schema/check.py b/regression/validate-trace-xml-schema/check.py index af5d919dc12..8a5cc9261be 100644 --- a/regression/validate-trace-xml-schema/check.py +++ b/regression/validate-trace-xml-schema/check.py @@ -29,6 +29,7 @@ ['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 @@ -36,6 +37,7 @@ ['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'], diff --git a/src/ansi-c/c_typecheck_base.h b/src/ansi-c/c_typecheck_base.h index b8f83f74d5c..4ee55c2cde9 100644 --- a/src/ansi-c/c_typecheck_base.h +++ b/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 typecheck_gcc_polymorphic_builtin( const irep_idt &identifier, const exprt::operandst &arguments, diff --git a/src/ansi-c/c_typecheck_expr.cpp b/src/ansi-c/c_typecheck_expr.cpp index bc712fe964b..e40c3b7a878 100644 --- a/src/ansi-c/c_typecheck_expr.cpp +++ b/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 '" diff --git a/src/ansi-c/expr2c.cpp b/src/ansi-c/expr2c.cpp index 2d66c2ea9cb..c5ee73d76bd 100644 --- a/src/ansi-c/expr2c.cpp +++ b/src/ansi-c/expr2c.cpp @@ -3977,6 +3977,8 @@ optionalt 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"}, diff --git a/src/ansi-c/library/gcc.c b/src/ansi-c/library/gcc.c index e3c6fab0deb..ee5f8b17d93 100644 --- a/src/ansi-c/library/gcc.c +++ b/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}; +} diff --git a/src/ansi-c/library/intrin.c b/src/ansi-c/library/intrin.c index 3f4ea7d0ed8..fed5b57ed2c 100644 --- a/src/ansi-c/library/intrin.c +++ b/src/ansi-c/library/intrin.c @@ -371,6 +371,78 @@ inline __m128i _mm_setr_epi32(int e3, int e2, int e1, int e0) } #endif +/* FUNCTION: _mm_set_epi16 */ + +#ifdef _MSC_VER +# ifndef __CPROVER_INTRIN_H_INCLUDED +# include +# define __CPROVER_INTRIN_H_INCLUDED +# endif + +inline __m128i _mm_set_epi16( + short e7, + short e6, + short e5, + short e4, + short e3, + short e2, + short e1, + short e0) +{ + return (__m128i){.m128i_i16 = {e0, e1, e2, e3, e4, e5, e6, e7}}; +} +#endif + +/* FUNCTION: _mm_setr_epi16 */ + +#ifdef _MSC_VER +# ifndef __CPROVER_INTRIN_H_INCLUDED +# include +# define __CPROVER_INTRIN_H_INCLUDED +# endif + +inline __m128i _mm_setr_epi16( + short e7, + short e6, + short e5, + short e4, + short e3, + short e2, + short e1, + short e0) +{ + return (__m128i){.m128i_i16 = {e7, e6, e5, e4, e3, e2, e1, e0}}; +} +#endif + +/* FUNCTION: _mm_set_pi16 */ + +#ifdef _MSC_VER +# ifndef __CPROVER_INTRIN_H_INCLUDED +# include +# define __CPROVER_INTRIN_H_INCLUDED +# endif + +inline __m64 _mm_set_pi16(short e3, short e2, short e1, short e0) +{ + return (__m64){.m64_i16 = {e0, e1, e2, e3}}; +} +#endif + +/* FUNCTION: _mm_setr_pi16 */ + +#ifdef _MSC_VER +# ifndef __CPROVER_INTRIN_H_INCLUDED +# include +# define __CPROVER_INTRIN_H_INCLUDED +# endif + +inline __m64 _mm_setr_pi16(short e3, short e2, short e1, short e0) +{ + return (__m64){.m64_i16 = {e3, e2, e1, e0}}; +} +#endif + /* FUNCTION: _mm_extract_epi32 */ #ifdef _MSC_VER @@ -384,3 +456,127 @@ inline int _mm_extract_epi32(__m128i a, const int imm8) return a.m128i_i32[imm8]; } #endif + +/* FUNCTION: _mm_extract_epi16 */ + +#ifdef _MSC_VER +# ifndef __CPROVER_INTRIN_H_INCLUDED +# include +# define __CPROVER_INTRIN_H_INCLUDED +# endif + +inline int _mm_extract_epi16(__m128i a, const int imm8) +{ + return a.m128i_i16[imm8]; +} +#endif + +/* FUNCTION: _mm_extract_pi16 */ + +#ifdef _MSC_VER +# ifndef __CPROVER_INTRIN_H_INCLUDED +# include +# define __CPROVER_INTRIN_H_INCLUDED +# endif + +inline int _mm_extract_pi16(__m64 a, const int imm8) +{ + return a.m64_i16[imm8]; +} +#endif + +/* FUNCTION: _mm_adds_epi16 */ + +#ifdef _MSC_VER +# ifndef __CPROVER_INTRIN_H_INCLUDED +# include +# define __CPROVER_INTRIN_H_INCLUDED +# endif + +inline __m128i _mm_adds_epi16(__m128i a, __m128i b) +{ + return (__m128i){ + .m128i_i16 = { + __CPROVER_saturating_plus(a.m128i_i16[0], b.m128i_i16[0]), + __CPROVER_saturating_plus(a.m128i_i16[1], b.m128i_i16[1]), + __CPROVER_saturating_plus(a.m128i_i16[2], b.m128i_i16[2]), + __CPROVER_saturating_plus(a.m128i_i16[3], b.m128i_i16[3]), + __CPROVER_saturating_plus(a.m128i_i16[4], b.m128i_i16[4]), + __CPROVER_saturating_plus(a.m128i_i16[5], b.m128i_i16[5]), + __CPROVER_saturating_plus(a.m128i_i16[6], b.m128i_i16[6]), + __CPROVER_saturating_plus(a.m128i_i16[7], b.m128i_i16[7]), + }}; +} +#endif + +/* FUNCTION: _mm_subs_epi16 */ + +#ifdef _MSC_VER +# ifndef __CPROVER_INTRIN_H_INCLUDED +# include +# define __CPROVER_INTRIN_H_INCLUDED +# endif + +inline __m128i _mm_subs_epi16(__m128i a, __m128i b) +{ + return (__m128i){ + .m128i_i16 = { + __CPROVER_saturating_minus(a.m128i_i16[0], b.m128i_i16[0]), + __CPROVER_saturating_minus(a.m128i_i16[1], b.m128i_i16[1]), + __CPROVER_saturating_minus(a.m128i_i16[2], b.m128i_i16[2]), + __CPROVER_saturating_minus(a.m128i_i16[3], b.m128i_i16[3]), + __CPROVER_saturating_minus(a.m128i_i16[4], b.m128i_i16[4]), + __CPROVER_saturating_minus(a.m128i_i16[5], b.m128i_i16[5]), + __CPROVER_saturating_minus(a.m128i_i16[6], b.m128i_i16[6]), + __CPROVER_saturating_minus(a.m128i_i16[7], b.m128i_i16[7]), + }}; +} +#endif + +/* FUNCTION: _mm_subs_epi16 */ + +#ifdef _MSC_VER +# ifndef __CPROVER_INTRIN_H_INCLUDED +# include +# define __CPROVER_INTRIN_H_INCLUDED +# endif + +inline __m128i _mm_subs_epi16(__m128i a, __m128i b) +{ + return (__m128i){ + .m128i_i16 = { + __CPROVER_saturating_minus(a.m128i_i16[0], b.m128i_i16[0]), + __CPROVER_saturating_minus(a.m128i_i16[1], b.m128i_i16[1]), + __CPROVER_saturating_minus(a.m128i_i16[2], b.m128i_i16[2]), + __CPROVER_saturating_minus(a.m128i_i16[3], b.m128i_i16[3]), + __CPROVER_saturating_minus(a.m128i_i16[4], b.m128i_i16[4]), + __CPROVER_saturating_minus(a.m128i_i16[5], b.m128i_i16[5]), + __CPROVER_saturating_minus(a.m128i_i16[6], b.m128i_i16[6]), + __CPROVER_saturating_minus(a.m128i_i16[7], b.m128i_i16[7]), + }}; +} +#endif + +/* FUNCTION: _mm_subs_epu16 */ + +#ifdef _MSC_VER +# ifndef __CPROVER_INTRIN_H_INCLUDED +# include +# define __CPROVER_INTRIN_H_INCLUDED +# endif + +inline __m128i _mm_subs_epu16(__m128i a, __m128i b) +{ + return (__m128i){ + .m128i_u16 = { + __CPROVER_saturating_minus(a.m128i_u16[0], b.m128i_u16[0]), + __CPROVER_saturating_minus(a.m128i_u16[1], b.m128i_u16[1]), + __CPROVER_saturating_minus(a.m128i_u16[2], b.m128i_u16[2]), + __CPROVER_saturating_minus(a.m128i_u16[3], b.m128i_u16[3]), + __CPROVER_saturating_minus(a.m128i_u16[4], b.m128i_u16[4]), + __CPROVER_saturating_minus(a.m128i_u16[5], b.m128i_u16[5]), + __CPROVER_saturating_minus(a.m128i_u16[6], b.m128i_u16[6]), + __CPROVER_saturating_minus(a.m128i_u16[7], b.m128i_u16[7]), + }}; +} +#endif diff --git a/src/goto-programs/remove_vector.cpp b/src/goto-programs/remove_vector.cpp index 7b0bcfd6c03..76f29108272 100644 --- a/src/goto-programs/remove_vector.cpp +++ b/src/goto-programs/remove_vector.cpp @@ -30,7 +30,8 @@ static bool have_to_remove_vector(const exprt &expr) expr.id() == ID_plus || expr.id() == ID_minus || expr.id() == ID_mult || expr.id() == ID_div || expr.id() == ID_mod || expr.id() == ID_bitxor || expr.id() == ID_bitand || expr.id() == ID_bitor || expr.id() == ID_shl || - expr.id() == ID_lshr || expr.id() == ID_ashr) + expr.id() == ID_lshr || expr.id() == ID_ashr || + expr.id() == ID_saturating_minus || expr.id() == ID_saturating_plus) { return true; } @@ -114,7 +115,8 @@ static void remove_vector(exprt &expr) expr.id() == ID_plus || expr.id() == ID_minus || expr.id() == ID_mult || expr.id() == ID_div || expr.id() == ID_mod || expr.id() == ID_bitxor || expr.id() == ID_bitand || expr.id() == ID_bitor || expr.id() == ID_shl || - expr.id() == ID_lshr || expr.id() == ID_ashr) + expr.id() == ID_lshr || expr.id() == ID_ashr || + expr.id() == ID_saturating_minus || expr.id() == ID_saturating_plus) { // FIXME plus, mult, bitxor, bitand and bitor are defined as n-ary // operations rather than binary. This code assumes that they @@ -255,6 +257,32 @@ static void remove_vector(exprt &expr) expr = array_exprt(exprt::operandst(dimension, casted_op), array_type); expr.add_source_location() = std::move(source_location); } + else if( + expr.type().id() == ID_vector && + to_vector_type(expr.type()).size() == to_array_type(op.type()).size()) + { + // do component-wise typecast: + // (vector-type) x -> array((vector-sub-type)x[0], ...) + remove_vector(expr.type()); + const array_typet &array_type = to_array_type(expr.type()); + const std::size_t dimension = + numeric_cast_v(to_constant_expr(array_type.size())); + const typet subtype = array_type.element_type(); + + exprt::operandst elements; + elements.reserve(dimension); + + for(std::size_t i = 0; i < dimension; i++) + { + exprt index = from_integer(i, array_type.size().type()); + elements.push_back( + typecast_exprt{index_exprt{op, std::move(index)}, subtype}); + } + + array_exprt array_expr(std::move(elements), array_type); + array_expr.add_source_location() = expr.source_location(); + expr.swap(array_expr); + } } } diff --git a/src/solvers/flattening/boolbv.cpp b/src/solvers/flattening/boolbv.cpp index f2d38ff051b..a7fca60feed 100644 --- a/src/solvers/flattening/boolbv.cpp +++ b/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); } diff --git a/src/solvers/flattening/boolbv.h b/src/solvers/flattening/boolbv.h index d7e31f59fbd..3670171fe8b 100644 --- a/src/solvers/flattening/boolbv.h +++ b/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); diff --git a/src/solvers/flattening/boolbv_add_sub.cpp b/src/solvers/flattening/boolbv_add_sub.cpp index c97d847036d..6727115cba6 100644 --- a/src/solvers/flattening/boolbv_add_sub.cpp +++ b/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; +} diff --git a/src/solvers/flattening/bv_utils.cpp b/src/solvers/flattening/bv_utils.cpp index a3216ef3224..8108bcf56cf 100644 --- a/src/solvers/flattening/bv_utils.cpp +++ b/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) { diff --git a/src/solvers/flattening/bv_utils.h b/src/solvers/flattening/bv_utils.h index a3e2942fe40..35a64eec59b 100644 --- a/src/solvers/flattening/bv_utils.h +++ b/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); } diff --git a/src/util/bitvector_expr.h b/src/util/bitvector_expr.h index 1034d25f187..220a9e5cae7 100644 --- a/src/util/bitvector_expr.h +++ b/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(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(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(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(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(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(expr); + validate_expr(ret); + return ret; +} + #endif // CPROVER_UTIL_BITVECTOR_EXPR_H diff --git a/src/util/format_expr.cpp b/src/util/format_expr.cpp index 7853dcfe856..e6d789ee5c9 100644 --- a/src/util/format_expr.cpp +++ b/src/util/format_expr.cpp @@ -12,6 +12,7 @@ Author: Daniel Kroening, kroening@kroening.com #include "format_expr.h" #include "arith_tools.h" +#include "bitvector_expr.h" #include "byte_operators.h" #include "format_type.h" #include "ieee_float.h" @@ -493,6 +494,20 @@ void format_expr_configt::setup() return os; }; + expr_map[ID_saturating_minus] = + [](std::ostream &os, const exprt &expr) -> std::ostream & { + const auto &saturating_minus = to_saturating_minus_expr(expr); + return os << "saturating-(" << format(saturating_minus.lhs()) << ", " + << format(saturating_minus.rhs()) << ')'; + }; + + expr_map[ID_saturating_plus] = + [](std::ostream &os, const exprt &expr) -> std::ostream & { + const auto &saturating_plus = to_saturating_plus_expr(expr); + return os << "saturating+(" << format(saturating_plus.lhs()) << ", " + << format(saturating_plus.rhs()) << ')'; + }; + fallback = [](std::ostream &os, const exprt &expr) -> std::ostream & { return fallback_format_rec(os, expr); }; diff --git a/src/util/irep_ids.def b/src/util/irep_ids.def index ae3cb358d04..cbde0869598 100644 --- a/src/util/irep_ids.def +++ b/src/util/irep_ids.def @@ -865,6 +865,8 @@ IREP_ID_ONE(shuffle_vector) IREP_ID_ONE(count_trailing_zeros) IREP_ID_ONE(empty_union) IREP_ID_ONE(bitreverse) +IREP_ID_ONE(saturating_minus) +IREP_ID_ONE(saturating_plus) // Projects depending on this code base that wish to extend the list of // available ids should provide a file local_irep_ids.def in their source tree