Skip to content

Commit 95f7c8d

Browse files
tautschnigtautschnig
committed
Add saturating addition/subtraction
Rust natively supports saturating arithmetic. For C code, it takes MMX instructions to have access to this, and even then it is limited to addition and subtraction. The implementation now is equally restricted to these two arithmetic operations.
1 parent ee2690d commit 95f7c8d

File tree

13 files changed

+502
-3
lines changed

13 files changed

+502
-3
lines changed

‎regression/cbmc/SIMD1/main.c

Lines changed: 31 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -1,4 +1,6 @@
11
#include <assert.h>
2+
#include <limits.h>
3+
24
#ifdef _MSC_VER
35
# include <intrin.h>
46
#else
@@ -10,5 +12,34 @@ int main()
1012
__m128i values = _mm_setr_epi32(0x1234, 0x2345, 0x3456, 0x4567);
1113
int val1 = _mm_extract_epi32(values, 0);
1214
assert(val1 == 0x1234);
15+
16+
__m64 a = _mm_setr_pi16(SHRT_MIN, 10, SHRT_MIN + 1, SHRT_MAX);
17+
__m64 b = _mm_set_pi16(1, 1, 10, 1);
18+
__m64 result = _mm_subs_pi16(a, b);
19+
short s1 = _mm_extract_pi16(result, 0);
20+
assert(s1 == SHRT_MIN);
21+
short s2 = _mm_extract_pi16(result, 1);
22+
assert(s2 == 0);
23+
short s3 = _mm_extract_pi16(result, 2);
24+
assert(s3 == SHRT_MIN);
25+
short s4 = _mm_extract_pi16(result, 3);
26+
assert(s4 == SHRT_MAX - 1);
27+
28+
result = _mm_adds_pi16(a, b);
29+
s1 = _mm_extract_pi16(result, 0);
30+
assert(s1 == SHRT_MIN + 1);
31+
s2 = _mm_extract_pi16(result, 1);
32+
assert(s2 == 20);
33+
s3 = _mm_extract_pi16(result, 2);
34+
assert(s3 == SHRT_MIN + 2);
35+
s4 = _mm_extract_pi16(result, 3);
36+
assert(s4 == SHRT_MAX);
37+
38+
__m128i x = _mm_set_epi16(0, 0, 0, 0, 0, 0, 0, 0);
39+
__m128i y = _mm_setr_epi16(1, 0, 0, 0, 0, 0, 0, 0);
40+
__m128i result128 = _mm_subs_epu16(x, y);
41+
short s = _mm_extract_epi16(result128, 0);
42+
assert(s == 0);
43+
1344
return 0;
1445
}

‎src/ansi-c/c_typecheck_base.h

Lines changed: 2 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -205,6 +205,8 @@ class c_typecheck_baset:
205205
exprt typecheck_builtin_overflow(
206206
side_effect_expr_function_callt &expr,
207207
const irep_idt &arith_op);
208+
exprt
209+
typecheck_saturating_arithmetic(const side_effect_expr_function_callt &expr);
208210
virtual optionalt<symbol_exprt> typecheck_gcc_polymorphic_builtin(
209211
const irep_idt &identifier,
210212
const exprt::operandst &arguments,

‎src/ansi-c/c_typecheck_expr.cpp

Lines changed: 41 additions & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -1967,6 +1967,15 @@ void c_typecheck_baset::typecheck_side_effect_function_call(
19671967

19681968
return;
19691969
}
1970+
else if(
1971+
identifier == CPROVER_PREFIX "saturating_minus" ||
1972+
identifier == CPROVER_PREFIX "saturating_plus")
1973+
{
1974+
exprt result = typecheck_saturating_arithmetic(expr);
1975+
expr.swap(result);
1976+
1977+
return;
1978+
}
19701979
else if(
19711980
auto gcc_polymorphic = typecheck_gcc_polymorphic_builtin(
19721981
identifier, expr.arguments(), f_op.source_location()))
@@ -3298,6 +3307,35 @@ exprt c_typecheck_baset::typecheck_builtin_overflow(
32983307
expr.source_location()};
32993308
}
33003309

3310+
exprt c_typecheck_baset::typecheck_saturating_arithmetic(
3311+
const side_effect_expr_function_callt &expr)
3312+
{
3313+
const irep_idt &identifier = to_symbol_expr(expr.function()).get_identifier();
3314+
3315+
// check function signature
3316+
if(expr.arguments().size() != 2)
3317+
{
3318+
std::ostringstream error_message;
3319+
error_message << expr.source_location().as_string() << ": " << identifier
3320+
<< " takes exactly two arguments, but "
3321+
<< expr.arguments().size() << " were provided";
3322+
throw invalid_source_file_exceptiont{error_message.str()};
3323+
}
3324+
3325+
exprt result;
3326+
if(identifier == CPROVER_PREFIX "saturating_minus")
3327+
result = saturating_minus_exprt{expr.arguments()[0], expr.arguments()[1]};
3328+
else if(identifier == CPROVER_PREFIX "saturating_plus")
3329+
result = saturating_plus_exprt{expr.arguments()[0], expr.arguments()[1]};
3330+
else
3331+
UNREACHABLE;
3332+
3333+
typecheck_expr_binary_arithmetic(result);
3334+
result.add_source_location() = expr.source_location();
3335+
3336+
return result;
3337+
}
3338+
33013339
/// Typecheck the parameters in a function call expression, and where
33023340
/// necessary, make implicit casts around parameters explicit.
33033341
void c_typecheck_baset::typecheck_function_call_arguments(
@@ -3523,7 +3561,9 @@ void c_typecheck_baset::typecheck_expr_binary_arithmetic(exprt &expr)
35233561
}
35243562
}
35253563
}
3526-
else if(expr.id()==ID_mod)
3564+
else if(
3565+
expr.id() == ID_mod || expr.id() == ID_saturating_minus ||
3566+
expr.id() == ID_saturating_plus)
35273567
{
35283568
if(type0==type1)
35293569
{

‎src/ansi-c/library/gcc.c

Lines changed: 85 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -192,6 +192,24 @@ __CPROVER_HIDE:;
192192
return size <= sizeof(__CPROVER_size_t);
193193
}
194194

195+
/* FUNCTION: __builtin_ia32_vec_ext_v4hi */
196+
197+
typedef short __gcc_v4hi __attribute__((__vector_size__(8)));
198+
199+
short __builtin_ia32_vec_ext_v4hi(__gcc_v4hi vec, int offset)
200+
{
201+
return *((short *)&vec + offset);
202+
}
203+
204+
/* FUNCTION: __builtin_ia32_vec_ext_v8hi */
205+
206+
typedef short __gcc_v8hi __attribute__((__vector_size__(16)));
207+
208+
short __builtin_ia32_vec_ext_v8hi(__gcc_v8hi vec, int offset)
209+
{
210+
return *((short *)&vec + offset);
211+
}
212+
195213
/* FUNCTION: __builtin_ia32_vec_ext_v4si */
196214

197215
typedef int __gcc_v4si __attribute__((__vector_size__(16)));
@@ -227,3 +245,70 @@ float __builtin_ia32_vec_ext_v4sf(__gcc_v4sf vec, int offset)
227245
{
228246
return *((float *)&vec + offset);
229247
}
248+
249+
/* FUNCTION: __builtin_ia32_psubsw128 */
250+
251+
#ifndef LIBRARY_CHECK
252+
typedef short __gcc_v8hi __attribute__((__vector_size__(16)));
253+
#else
254+
__gcc_v8hi __CPROVER_saturating_minus();
255+
#endif
256+
257+
__gcc_v8hi __builtin_ia32_psubsw128(__gcc_v8hi a, __gcc_v8hi b)
258+
{
259+
return __CPROVER_saturating_minus(a, b);
260+
}
261+
262+
/* FUNCTION: __builtin_ia32_psubusw128 */
263+
264+
#ifndef LIBRARY_CHECK
265+
typedef short __gcc_v8hi __attribute__((__vector_size__(16)));
266+
#endif
267+
268+
__gcc_v8hi __builtin_ia32_psubusw128(__gcc_v8hi a, __gcc_v8hi b)
269+
{
270+
typedef unsigned short v8hi_u __attribute__((__vector_size__(16)));
271+
return (__gcc_v8hi)__CPROVER_saturating_minus((v8hi_u)a, (v8hi_u)b);
272+
}
273+
274+
/* FUNCTION: __builtin_ia32_paddsw */
275+
276+
#ifndef LIBRARY_CHECK
277+
typedef short __gcc_v4hi __attribute__((__vector_size__(8)));
278+
#else
279+
__gcc_v4hi __CPROVER_saturating_plus();
280+
#endif
281+
282+
__gcc_v4hi __builtin_ia32_paddsw(__gcc_v4hi a, __gcc_v4hi b)
283+
{
284+
return __CPROVER_saturating_plus(a, b);
285+
}
286+
287+
/* FUNCTION: __builtin_ia32_psubsw */
288+
289+
#ifndef LIBRARY_CHECK
290+
typedef short __gcc_v4hi __attribute__((__vector_size__(8)));
291+
#else
292+
__gcc_v4hi __CPROVER_saturating_minus_v4hi(__gcc_v4hi, __gcc_v4hi);
293+
# define __CPROVER_saturating_minus __CPROVER_saturating_minus_v4hi
294+
#endif
295+
296+
__gcc_v4hi __builtin_ia32_psubsw(__gcc_v4hi a, __gcc_v4hi b)
297+
{
298+
return __CPROVER_saturating_minus(a, b);
299+
}
300+
301+
#ifdef LIBRARY_CHECK
302+
# undef __CPROVER_saturating_minus
303+
#endif
304+
305+
/* FUNCTION: __builtin_ia32_vec_init_v4hi */
306+
307+
#ifndef LIBRARY_CHECK
308+
typedef short __gcc_v4hi __attribute__((__vector_size__(8)));
309+
#endif
310+
311+
__gcc_v4hi __builtin_ia32_vec_init_v4hi(short e0, short e1, short e2, short e3)
312+
{
313+
return (__gcc_v4hi){e0, e1, e2, e3};
314+
}

‎src/ansi-c/library/intrin.c

Lines changed: 86 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -371,6 +371,78 @@ inline __m128i _mm_setr_epi32(int e3, int e2, int e1, int e0)
371371
}
372372
#endif
373373

374+
/* FUNCTION: _mm_set_epi16 */
375+
376+
#ifdef _MSC_VER
377+
# ifndef __CPROVER_shortRIN_H_INCLUDED
378+
# include <shortrin.h>
379+
# define __CPROVER_shortRIN_H_INCLUDED
380+
# endif
381+
382+
inline __m128i _mm_set_epi16(
383+
short e7,
384+
short e6,
385+
short e5,
386+
short e4,
387+
short e3,
388+
short e2,
389+
short e1,
390+
short e0)
391+
{
392+
return (__m128i){.m128i_i16 = {e0, e1, e2, e3, e4, e5, e6, e7}};
393+
}
394+
#endif
395+
396+
/* FUNCTION: _mm_setr_epi16 */
397+
398+
#ifdef _MSC_VER
399+
# ifndef __CPROVER_shortRIN_H_INCLUDED
400+
# include <shortrin.h>
401+
# define __CPROVER_shortRIN_H_INCLUDED
402+
# endif
403+
404+
inline __m128i _mm_setr_epi16(
405+
short e7,
406+
short e6,
407+
short e5,
408+
short e4,
409+
short e3,
410+
short e2,
411+
short e1,
412+
short e0)
413+
{
414+
return (__m128i){.m128i_i16 = {e7, e6, e5, e4, e3, e2, e1, e0}};
415+
}
416+
#endif
417+
418+
/* FUNCTION: _mm_set_pi16 */
419+
420+
#ifdef _MSC_VER
421+
# ifndef __CPROVER_INTRIN_H_INCLUDED
422+
# include <intrin.h>
423+
# define __CPROVER_INTRIN_H_INCLUDED
424+
# endif
425+
426+
inline __m64 _mm_set_pi16(short e3, short e2, short e1, short e0)
427+
{
428+
return (__m64){.m64_i16 = {e0, e1, e2, e3}};
429+
}
430+
#endif
431+
432+
/* FUNCTION: _mm_setr_pi16 */
433+
434+
#ifdef _MSC_VER
435+
# ifndef __CPROVER_shortRIN_H_INCLUDED
436+
# include <shortrin.h>
437+
# define __CPROVER_shortRIN_H_INCLUDED
438+
# endif
439+
440+
inline __m64 _mm_setr_pi16(short e3, short e2, short e1, short e0)
441+
{
442+
return (__m64){.m64_i16 = {e3, e2, e1, e0}};
443+
}
444+
#endif
445+
374446
/* FUNCTION: _mm_extract_epi32 */
375447

376448
#ifdef _MSC_VER
@@ -384,3 +456,17 @@ inline int _mm_extract_epi32(__m128i a, const int imm8)
384456
return a.m128i_i32[imm8];
385457
}
386458
#endif
459+
460+
/* FUNCTION: _mm_extract_pi16 */
461+
462+
#ifdef _MSC_VER
463+
# ifndef __CPROVER_INTRIN_H_INCLUDED
464+
# include <intrin.h>
465+
# define __CPROVER_INTRIN_H_INCLUDED
466+
# endif
467+
468+
inline int _mm_extract_pi16(__m64 a, const int imm8)
469+
{
470+
return a.m64_i16[imm8];
471+
}
472+
#endif

‎src/goto-programs/remove_vector.cpp

Lines changed: 4 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -28,7 +28,8 @@ static bool have_to_remove_vector(const exprt &expr)
2828
expr.id() == ID_plus || expr.id() == ID_minus || expr.id() == ID_mult ||
2929
expr.id() == ID_div || expr.id() == ID_mod || expr.id() == ID_bitxor ||
3030
expr.id() == ID_bitand || expr.id() == ID_bitor || expr.id() == ID_shl ||
31-
expr.id() == ID_lshr || expr.id() == ID_ashr)
31+
expr.id() == ID_lshr || expr.id() == ID_ashr ||
32+
expr.id() == ID_saturating_minus || expr.id() == ID_saturating_plus)
3233
{
3334
return true;
3435
}
@@ -102,7 +103,8 @@ static void remove_vector(exprt &expr)
102103
expr.id() == ID_plus || expr.id() == ID_minus || expr.id() == ID_mult ||
103104
expr.id() == ID_div || expr.id() == ID_mod || expr.id() == ID_bitxor ||
104105
expr.id() == ID_bitand || expr.id() == ID_bitor || expr.id() == ID_shl ||
105-
expr.id() == ID_lshr || expr.id() == ID_ashr)
106+
expr.id() == ID_lshr || expr.id() == ID_ashr ||
107+
expr.id() == ID_saturating_minus || expr.id() == ID_saturating_plus)
106108
{
107109
// FIXME plus, mult, bitxor, bitand and bitor are defined as n-ary
108110
// operations rather than binary. This code assumes that they

‎src/solvers/flattening/boolbv.cpp

Lines changed: 2 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -229,6 +229,8 @@ bvt boolbvt::convert_bitvector(const exprt &expr)
229229
}
230230
else if(expr.id() == ID_bitreverse)
231231
return convert_bitreverse(to_bitreverse_expr(expr));
232+
else if(expr.id() == ID_saturating_minus || expr.id() == ID_saturating_plus)
233+
return convert_saturating_add_sub(to_binary_expr(expr));
232234

233235
return conversion_failed(expr);
234236
}

‎src/solvers/flattening/boolbv.h

Lines changed: 1 addition & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -194,6 +194,7 @@ class boolbvt:public arrayst
194194
virtual bvt convert_function_application(
195195
const function_application_exprt &expr);
196196
virtual bvt convert_bitreverse(const bitreverse_exprt &expr);
197+
virtual bvt convert_saturating_add_sub(const binary_exprt &expr);
197198

198199
virtual exprt make_bv_expr(const typet &type, const bvt &bv);
199200
virtual exprt make_free_bv_expr(const typet &type);

0 commit comments

Comments
 (0)