Skip to content

Commit 56a7a49

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 (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
1 parent 57c59fc commit 56a7a49

File tree

16 files changed

+389
-3
lines changed

16 files changed

+389
-3
lines changed

‎regression/cbmc/saturating_arithmetric/main.c

Lines changed: 17 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,17 @@
1+
#include <limits.h>
2+
3+
int main()
4+
{
5+
__CPROVER_assert(
6+
__CPROVER_saturating_minus(INT_MIN, 1) == INT_MIN,
7+
"subtracting from INT_MIN");
8+
__CPROVER_assert(
9+
__CPROVER_saturating_plus(LONG_MAX, 1l) == LONG_MAX, "adding to LONG_MAX");
10+
__CPROVER_assert(
11+
__CPROVER_saturating_minus(-1, INT_MIN) == INT_MAX, "no overflow");
12+
__CPROVER_assert(
13+
__CPROVER_saturating_plus(ULONG_MAX, 1ul) == ULONG_MAX,
14+
"adding to ULONG_MAX");
15+
__CPROVER_assert(
16+
__CPROVER_saturating_minus(10ul, ULONG_MAX) == 0, "subtracting ULONG_MAX");
17+
}

‎regression/cbmc/saturating_arithmetric/output-formula.desc

Lines changed: 9 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,9 @@
1+
CORE
2+
main.c
3+
--program-only
4+
ASSERT\(__CPROVER_saturating_minus\(.*\)
5+
ASSERT\(__CPROVER_saturating_plus\(.*\)
6+
^EXIT=0$
7+
^SIGNAL=0$
8+
--
9+
^warning: ignoring

‎regression/cbmc/saturating_arithmetric/output-goto.desc

Lines changed: 9 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,9 @@
1+
CORE
2+
main.c
3+
--show-goto-functions
4+
ASSERT saturating-\(.*\)
5+
ASSERT saturating\+\(.*\)
6+
^EXIT=0$
7+
^SIGNAL=0$
8+
--
9+
^warning: ignoring

‎regression/cbmc/saturating_arithmetric/test.desc

Lines changed: 8 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,8 @@
1+
CORE broken-smt-backend
2+
main.c
3+
4+
^EXIT=0$
5+
^SIGNAL=0$
6+
^VERIFICATION SUCCESSFUL$
7+
--
8+
^warning: ignoring

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

Lines changed: 2 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -29,13 +29,15 @@
2929
['enum_is_in_range', 'format.desc'],
3030
['r_w_ok9', 'simplify.desc'],
3131
['reachability-slice-interproc2', 'test.desc'],
32+
['saturating_arithmetric', 'output-goto.desc'],
3233
# this one wants show-properties instead producing a trace
3334
['show_properties1', 'test.desc'],
3435
# program-only instead of trace
3536
['vla1', 'program-only.desc'],
3637
['Pointer_Arithmetic19', 'test.desc'],
3738
['Quantifiers-simplify', 'simplify_not_forall.desc'],
3839
['array-cell-sensitivity15', 'test.desc'],
40+
['saturating_arithmetric', 'output-formula.desc'],
3941
# these test for invalid command line handling
4042
['bad_option', 'test_multiple.desc'],
4143
['bad_option', 'test.desc'],

‎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: 57 additions & 3 deletions
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(
@@ -3499,9 +3537,15 @@ void c_typecheck_baset::typecheck_expr_binary_arithmetic(exprt &expr)
34993537
return;
35003538
}
35013539

3502-
// promote!
3503-
3504-
implicit_typecast_arithmetic(op0, op1);
3540+
if(expr.id() == ID_saturating_minus || expr.id() == ID_saturating_plus)
3541+
{
3542+
implicit_typecast(op1, o_type0);
3543+
}
3544+
else
3545+
{
3546+
// promote!
3547+
implicit_typecast_arithmetic(op0, op1);
3548+
}
35053549

35063550
const typet &type0 = op0.type();
35073551
const typet &type1 = op1.type();
@@ -3562,6 +3606,16 @@ void c_typecheck_baset::typecheck_expr_binary_arithmetic(exprt &expr)
35623606
}
35633607
}
35643608
}
3609+
else if(expr.id() == ID_saturating_minus || expr.id() == ID_saturating_plus)
3610+
{
3611+
if(
3612+
type0 == type1 &&
3613+
(type0.id() == ID_signedbv || type0.id() == ID_unsignedbv))
3614+
{
3615+
expr.type() = type0;
3616+
return;
3617+
}
3618+
}
35653619

35663620
error().source_location = expr.source_location();
35673621
error() << "operator '" << expr.id() << "' not defined for types '"

‎src/ansi-c/expr2c.cpp

Lines changed: 2 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -3977,6 +3977,8 @@ optionalt<std::string> expr2ct::convert_function(const exprt &src)
39773977
{ID_object_size, "OBJECT_SIZE"},
39783978
{ID_pointer_object, "POINTER_OBJECT"},
39793979
{ID_pointer_offset, "POINTER_OFFSET"},
3980+
{ID_saturating_minus, CPROVER_PREFIX "saturating_minus"},
3981+
{ID_saturating_plus, CPROVER_PREFIX "saturating_plus"},
39803982
{ID_r_ok, "R_OK"},
39813983
{ID_w_ok, "W_OK"},
39823984
{ID_rw_ok, "RW_OK"},

‎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)