实验1：从软件测试到形式化验证

任务1：测试整数中点计算函数#

程序运行输入输出：

1
❯ ./midpoint_test.out
2
0 0
3
0
4
❯ ./midpoint_test.out
5
0 1
6
0
7
❯ ./midpoint_test.out
8
1 2147483647
9
-1073741824
10
❯ ./midpoint_test.out
11
2147483647 2147483647
12
-1

已运行：

No.	low	high	midpoint	output
1	0	0	0	0
2	0	1	0	0
3	1	2147483647	1073741824	-1073741824
4	2147483647	2147483647	2147483647	-1

未运行：

No.	low	high	midpoint	output
5	29	47	38	/
6	350	7701	4025	/
7	1073741824	1073741824	1073741824	/

测试结论：当前测试结果能够支持 low + high 较小的情形；对于 low + high 较大的情况，程序会发生溢出，导致得到错误的结果。当前测试结果可以支持测试点 5 与测试点 6 ，无法支持测试点 7 。

当前测试结果可以说明程序在 low + high 较小的情形下大致运行良好，在 low + high 较大的情形下可能产生错误的输出不能说明对于所有的合法输入，程序都可以按照预期运行。

任务2：使用 CBMC 检查整数溢出#

程序运行输入输出：

1
❯ cbmc midpoint_cbmc.c --signed-overflow-check --all-properties --trace
2
CBMC version 6.11.0 (640889b) 64-bit x86_64 linux
3
Type-checking midpoint_cbmc
4
Generating GOTO Program
5
Adding CPROVER library (x86_64)
6
Removal of function pointers and virtual functions
7
Generic Property Instrumentation
108 collapsed lines
8
Starting Bounded Model Checking
9
Passing problem to propositional reduction
10
converting SSA
11
Running propositional reduction
12
SAT checker: instance is SATISFIABLE
13
Building error trace
14

15
** Results:
16
midpoint_cbmc.c function main
17
[main.assertion.1] line 10 midpoint is inside the interval: FAILURE
18

19
midpoint_cbmc.c function midpoint
20
[midpoint.overflow.1] line 3 arithmetic overflow on signed + in low + high: FAILURE
21

22
Trace for main.assertion.1:
23

24
State 13 file midpoint_cbmc.c function main line 6 thread 0
25
----------------------------------------------------
26
  return_value_nondet_int=177393664 (00001010 10010010 11010000 00000000)
27

28
State 14 file midpoint_cbmc.c function main line 6 thread 0
29
----------------------------------------------------
30
  low=177393664 (00001010 10010010 11010000 00000000)
31

32
State 17 file midpoint_cbmc.c function main line 7 thread 0
33
----------------------------------------------------
34
  return_value_nondet_int$0=1981235200 (01110110 00010111 01000000 00000000)
35

36
State 18 file midpoint_cbmc.c function main line 7 thread 0
37
----------------------------------------------------
38
  high=1981235200 (01110110 00010111 01000000 00000000)
39

40
Assumption:
41
  file midpoint_cbmc.c line 8 function main
42
  0 <= low && low <= high
43

44
State 24 file midpoint_cbmc.c function main line 9 thread 0
45
----------------------------------------------------
46
  low=177393664 (00001010 10010010 11010000 00000000)
47

48
State 25 file midpoint_cbmc.c function main line 9 thread 0
49
----------------------------------------------------
50
  high=1981235200 (01110110 00010111 01000000 00000000)
51

52
Violated property:
53
  file midpoint_cbmc.c function midpoint line 3 thread 0
54
  arithmetic overflow on signed + in low + high
55
  !overflow("+", signed int, low, high)
56

57

58
State 27 file midpoint_cbmc.c function midpoint line 3 thread 0
59
----------------------------------------------------
60
  goto_symex$$return_value$$midpoint=-1068169216 (11000000 01010101 00001000 00000000)
61
misskey
62
State 29 file midpoint_cbmc.c function main line 9 thread 0
63
----------------------------------------------------
64
  return_value_midpoint=-1068169216 (11000000 01010101 00001000 00000000)
65

66
State 30 file midpoint_cbmc.c function main line 9 thread 0
67
----------------------------------------------------
68
  mid=-1068169216 (11000000 01010101 00001000 00000000)
69

70
Violated property:
71
  file midpoint_cbmc.c function main line 10 thread 0
72
  midpoint is inside the interval
73
  low <= mid && mid <= high
74

75

76

77
Trace for midpoint.overflow.1:
78

79
State 13 file midpoint_cbmc.c function main line 6 thread 0
80
----------------------------------------------------
81
  return_value_nondet_int=177393664 (00001010 10010010 11010000 00000000)
82

83
State 14 file midpoint_cbmc.c function main line 6 thread 0
84
----------------------------------------------------
85
  low=177393664 (00001010 10010010 11010000 00000000)
86

87
State 17 file midpoint_cbmc.c function main line 7 thread 0
88
----------------------------------------------------
89
  return_value_nondet_int$0=1981235200 (01110110 00010111 01000000 00000000)
90

91
State 18 file midpoint_cbmc.c function main line 7 thread 0
92
----------------------------------------------------
93
  high=1981235200 (01110110 00010111 01000000 00000000)
94

95
Assumption:
96
  file midpoint_cbmc.c line 8 function main
97
  0 <= low && low <= high
98

99
State 24 file midpoint_cbmc.c function main line 9 thread 0
100
----------------------------------------------------
101
  low=177393664 (00001010 10010010 11010000 00000000)
102

103
State 25 file midpoint_cbmc.c function main line 9 thread 0
104
----------------------------------------------------
105
  high=1981235200 (01110110 00010111 01000000 00000000)
106

107
Violated property:
108
  file midpoint_cbmc.c function midpoint line 3 thread 0
109
  arithmetic overflow on signed + in low + high
110
  !overflow("+", signed int, low, high)
111

112

113

114
** 2 of 2 failed (2 iterations)
115
VERIFICATION FAILED

从下列代码片段中可知 low + high 的有符号整数溢出性质

1
Violated property:
2
  file midpoint_cbmc.c function midpoint line 3 thread 0
3
  arithmetic overflow on signed + in low + high
4
  !overflow("+", signed int, low, high)

反例为low = 177393664; high = 1981235200; mid = -1068169216，满足 $0 \leq low \leq high$ 的输入假设。由数学计算知其和较小中点为 1079314432 ，仍在 int 表示范围内。但根据函数 midpoint 的定义：

1
int midpoint(int low, int high) {
2
 return (low + high) / 2;
3
}

程序执行过程中会先计算 (low + high) ，该过程中发生有符号整数溢出。

将反例作为任务 1 程序的输入，实际运行结果如下：

1
❯ ./midpoint_test.out
2
177393664 1981235200
3
-1068169216

运行结果与 CBMC 运行输出相符

任务3：分别检查计算安全和功能要求#

midpoint_test 输入输出：

1
❯ g++ midpoint_test.c -o midpoint_test.out
2
❯ ./midpoint_test.out
3
0 0
4
0
5
❯ ./midpoint_test.out
6
0 1
7
0
8
❯ ./midpoint_test.out
9
1 2147483647
10
1073741824
11
❯ ./midpoint_test.out
12
2147483647 2147483647
13
2147483647
14
❯ ./midpoint_test.out
15
29 47
16
38
17
❯ ./midpoint_test.out
18
350 7701
19
4025
20
❯ ./midpoint_test.out
21
1073741824 1073741824
22
1073741824

测试用例：

No.	low	high	midpoint	output
1	0	0	0	0
2	0	1	0	0
3	1	2147483647	1073741824	1073741824
4	2147483647	2147483647	2147483647	2147483647
5	29	47	38	38
6	350	7701	4025	4025
7	1073741824	1073741824	1073741824	1073741824

midpoint_cbmc 输入输出：

1
❯ cbmc midpoint_cbmc.c --signed-overflow-check --all-properties --trace
2
CBMC version 6.11.0 (640889b) 64-bit x86_64 linux
3
Type-checking midpoint_cbmc
4
Generating GOTO Program
5
Adding CPROVER library (x86_64)
6
Removal of function pointers and virtual functions
7
Generic Property Instrumentation
19 collapsed lines
8
Starting Bounded Model Checking
9
Passing problem to propositional reduction
10
converting SSA
11
Running propositional reduction
12
SAT checker: instance is UNSATISFIABLE
13

14
** Results:
15
midpoint_cbmc.c function main
16
[main.assertion.1] line 13 midpoint is inside the interval: SUCCESS
17
[main.assertion.2] line 15 midpoint has the expected offset: SUCCESS
18
[main.overflow.1] line 15 arithmetic overflow on signed - in mid - low: SUCCESS
19
[main.overflow.2] line 15 arithmetic overflow on signed - in high - low: SUCCESS
20

21
midpoint_cbmc.c function midpoint
22
[midpoint.overflow.1] line 3 arithmetic overflow on signed - in high - low: SUCCESS
23
[midpoint.overflow.2] line 3 arithmetic overflow on signed + in low + (high - low) / 2: SUCCESS
24

25
** 0 of 6 failed (1 iterations)
26
VERIFICATION SUCCESSFUL

low 和 high 可以取任意 int 范围内整数，输入假设排除了 $0 > low \vee low > high$ 的情形。

第一个断言检查结果是否仍在原区间中；第二个断言检查结果与 low 的距离是否等于区间长度的一半：

实际覆盖的输入条件为 low 与 high 均为 int 范围内整数且满足 $0 \leq low \leq high$ ，具有避免有符号整数溢出的性质。

将 midpoint 修改为下面版本

1
int midpoint(int low, int high) {
2
  return low / 2 + high / 2;
3
}

CBMC 运行结果如下：

1
❯ cbmc midpoint_cbmc.c --signed-overflow-check --all-properties --trace
2
CBMC version 6.11.0 (640889b) 64-bit x86_64 linux
3
Type-checking midpoint_cbmc
4
Generating GOTO Program
5
Adding CPROVER library (x86_64)
6
Removal of function pointers and virtual functions
7
Generic Property Instrumentation
122 collapsed lines
8
Starting Bounded Model Checking
9
Passing problem to propositional reduction
10
converting SSA
11
Running propositional reduction
12
SAT checker: instance is SATISFIABLE
13
Building error trace
14
Running propositional reduction
15
SAT checker: instance is SATISFIABLE
16
Building error trace
17
Running propositional reduction
18
SAT checker: instance is UNSATISFIABLE
19

20
** Results:
21
midpoint_cbmc.c function main
22
[main.assertion.1] line 13 midpoint is inside the interval: FAILURE
23
[main.assertion.2] line 15 midpoint has the expected offset: FAILURE
24
[main.overflow.1] line 15 arithmetic overflow on signed - in mid - low: SUCCESS
25
[main.overflow.2] line 15 arithmetic overflow on signed - in high - low: SUCCESS
26

27
midpoint_cbmc.c function midpoint
28
[midpoint.overflow.1] line 3 arithmetic overflow on signed + in low / 2 + high / 2: SUCCESS
29

30
Trace for main.assertion.1:
31

32
State 13 file midpoint_cbmc.c function main line 6 thread 0
33
----------------------------------------------------
34
  return_value_nondet_int=1 (00000000 00000000 00000000 00000001)
35

36
State 14 file midpoint_cbmc.c function main line 6 thread 0
37
----------------------------------------------------
38
  low=1 (00000000 00000000 00000000 00000001)
39

40
State 17 file midpoint_cbmc.c function main line 7 thread 0
41
----------------------------------------------------
42
  return_value_nondet_int$0=1 (00000000 00000000 00000000 00000001)
43

44
State 18 file midpoint_cbmc.c function main line 7 thread 0
45
----------------------------------------------------
46
  high=1 (00000000 00000000 00000000 00000001)
47

48
Assumption:
49
  file midpoint_cbmc.c line 9 function main
50
  0 <= low && low <= high
51

52
State 24 file midpoint_cbmc.c function main line 11 thread 0
53
----------------------------------------------------
54
  low=1 (00000000 00000000 00000000 00000001)
55

56
State 25 file midpoint_cbmc.c function main line 11 thread 0
57
----------------------------------------------------
58
  high=1 (00000000 00000000 00000000 00000001)
59

60
State 27 file midpoint_cbmc.c function midpoint line 3 thread 0
61
----------------------------------------------------
62
  goto_symex$$return_value$$midpoint=0 (00000000 00000000 00000000 00000000)
63

64
State 29 file midpoint_cbmc.c function main line 11 thread 0
65
----------------------------------------------------
66
  return_value_midpoint=0 (00000000 00000000 00000000 00000000)
67

68
State 30 file midpoint_cbmc.c function main line 11 thread 0
69
----------------------------------------------------
70
  mid=0 (00000000 00000000 00000000 00000000)
71

72
Violated property:
73
  file midpoint_cbmc.c function main line 13 thread 0
74
  midpoint is inside the interval
75
  low <= mid && mid <= high
76

77

78

79
Trace for main.assertion.2:
80

81
State 13 file midpoint_cbmc.c function main line 6 thread 0
82
----------------------------------------------------
83
  return_value_nondet_int=1 (00000000 00000000 00000000 00000001)
84

85
State 14 file midpoint_cbmc.c function main line 6 thread 0
86
----------------------------------------------------
87
  low=1 (00000000 00000000 00000000 00000001)
88

89
State 17 file midpoint_cbmc.c function main line 7 thread 0
90
----------------------------------------------------
91
  return_value_nondet_int$0=3 (00000000 00000000 00000000 00000011)
92

93
State 18 file midpoint_cbmc.c function main line 7 thread 0
94
----------------------------------------------------
95
  high=3 (00000000 00000000 00000000 00000011)
96

97
Assumption:
98
  file midpoint_cbmc.c line 9 function main
99
  0 <= low && low <= high
100

101
State 24 file midpoint_cbmc.c function main line 11 thread 0
102
----------------------------------------------------
103
  low=1 (00000000 00000000 00000000 00000001)
104

105
State 25 file midpoint_cbmc.c function main line 11 thread 0
106
----------------------------------------------------
107
  high=3 (00000000 00000000 00000000 00000011)
108

109
State 27 file midpoint_cbmc.c function midpoint line 3 thread 0
110
----------------------------------------------------
111
  goto_symex$$return_value$$midpoint=1 (00000000 00000000 00000000 00000001)
112

113
State 29 file midpoint_cbmc.c function main line 11 thread 0
114
----------------------------------------------------
115
  return_value_midpoint=1 (00000000 00000000 00000000 00000001)
116

117
State 30 file midpoint_cbmc.c function main line 11 thread 0
118
----------------------------------------------------
119
  mid=1 (00000000 00000000 00000000 00000001)
120

121
Violated property:
122
  file midpoint_cbmc.c function main line 15 thread 0
123
  midpoint has the expected offset
124
  mid - low == (high - low) / 2
125

126

127

128
** 2 of 5 failed (3 iterations)
129
VERIFICATION FAILED

从断言中可知一组失败的值为 low = 1; high = 1; mid = 0，此时有 low / 2 = 0; high / 2 = 0，二者之和为 0 ，而正确的较小中点为 1 。产生该结果的原因是计算整数除法时产生舍入误差。

任务4：比较软件测试与形式化验证#

任务 1 中 low = 0; high = 0； mid = 0 通过测试，而任务 2 中 low = 177393664; high = 1981235200; mid = -1068169216 产生了溢出，两组数据都满足 $0 \leq low \leq high$ 的条件。前一组输入通过只能说明程序在该用例上的正确性，不能排除其他输入可能产生的错误。
修正后的结果：
Terminal window
```
1
❯ ./midpoint_test.out
2
177393664 1981235200
3
1079314432
```
该条测试可以防止 low + high 产生有符号整数溢出的错误出现。
验证结论:
- 适用的输入条件： $0 \leq low \leq high$
- 使用的整数类型： int
- 已经检查的溢出性质： low + high 产生有符号整数溢出
- 功能性质：结果仍在原区间中；结果与 low 的距离等于区间长度的一半
- 没有检查的输入与程序行为：没有检查整数类型为其他类型的行为；没有检查输入值超过 int 类型范围的情况
软件测试可以发现特定情形下的问题，软件验证覆盖更广泛，但相应实现难度更高。要根据具体场景选择使用。