1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
|
#ifndef AWS_COMMON_MATH_CBMC_INL
#define AWS_COMMON_MATH_CBMC_INL
/**
* Copyright Amazon.com, Inc. or its affiliates. All Rights Reserved.
* SPDX-License-Identifier: Apache-2.0.
*/
/*
* This header is already included, but include it again to make editor
* highlighting happier.
*/
#include <aws/common/common.h>
AWS_EXTERN_C_BEGIN
/* This header does safe operations. Supressing the checks within these functions
* avoids unnecessary CBMC assertions
*/
#pragma CPROVER check push
#pragma CPROVER check disable "unsigned-overflow"
/**
* Multiplies a * b. If the result overflows, returns 2^64 - 1.
*/
AWS_STATIC_IMPL uint64_t aws_mul_u64_saturating(uint64_t a, uint64_t b) {
if (__CPROVER_overflow_mult(a, b))
return UINT64_MAX;
return a * b;
}
/**
* If a * b overflows, returns AWS_OP_ERR; otherwise multiplies
* a * b, returns the result in *r, and returns AWS_OP_SUCCESS.
*/
AWS_STATIC_IMPL int aws_mul_u64_checked(uint64_t a, uint64_t b, uint64_t *r) {
if (__CPROVER_overflow_mult(a, b))
return aws_raise_error(AWS_ERROR_OVERFLOW_DETECTED);
*r = a * b;
return AWS_OP_SUCCESS;
}
/**
* Multiplies a * b. If the result overflows, returns 2^32 - 1.
*/
AWS_STATIC_IMPL uint32_t aws_mul_u32_saturating(uint32_t a, uint32_t b) {
if (__CPROVER_overflow_mult(a, b))
return UINT32_MAX;
return a * b;
}
/**
* If a * b overflows, returns AWS_OP_ERR; otherwise multiplies
* a * b, returns the result in *r, and returns AWS_OP_SUCCESS.
*/
AWS_STATIC_IMPL int aws_mul_u32_checked(uint32_t a, uint32_t b, uint32_t *r) {
if (__CPROVER_overflow_mult(a, b))
return aws_raise_error(AWS_ERROR_OVERFLOW_DETECTED);
*r = a * b;
return AWS_OP_SUCCESS;
}
/**
* Adds a + b. If the result overflows returns 2^64 - 1.
*/
AWS_STATIC_IMPL uint64_t aws_add_u64_saturating(uint64_t a, uint64_t b) {
if (__CPROVER_overflow_plus(a, b))
return UINT64_MAX;
return a + b;
}
/**
* If a + b overflows, returns AWS_OP_ERR; otherwise adds
* a + b, returns the result in *r, and returns AWS_OP_SUCCESS.
*/
AWS_STATIC_IMPL int aws_add_u64_checked(uint64_t a, uint64_t b, uint64_t *r) {
if (__CPROVER_overflow_plus(a, b))
return aws_raise_error(AWS_ERROR_OVERFLOW_DETECTED);
*r = a + b;
return AWS_OP_SUCCESS;
}
/**
* Adds a + b. If the result overflows returns 2^32 - 1.
*/
AWS_STATIC_IMPL uint32_t aws_add_u32_saturating(uint32_t a, uint32_t b) {
if (__CPROVER_overflow_plus(a, b))
return UINT32_MAX;
return a + b;
}
/**
* If a + b overflows, returns AWS_OP_ERR; otherwise adds
* a + b, returns the result in *r, and returns AWS_OP_SUCCESS.
*/
AWS_STATIC_IMPL int aws_add_u32_checked(uint32_t a, uint32_t b, uint32_t *r) {
if (__CPROVER_overflow_plus(a, b))
return aws_raise_error(AWS_ERROR_OVERFLOW_DETECTED);
*r = a + b;
return AWS_OP_SUCCESS;
}
#pragma CPROVER check pop
AWS_EXTERN_C_END
#endif /* AWS_COMMON_MATH_CBMC_INL */
|
