Skip to content

Commit 28d478d

Browse files
peterschrammelpeterschrammel
committed
Tests for overflows in pointer arithmetic
One is detected with --pointer-check enabled, the other one is currently not detected.
1 parent d122cfb commit 28d478d

File tree

4 files changed

+162
-0
lines changed

4 files changed

+162
-0
lines changed

‎regression/cbmc/address_space_size_limit2/test.c

Lines changed: 10 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,10 @@
1+
#include <stdlib.h>
2+
#include <assert.h>
3+
4+
int main(int argc, char** argv)
5+
{
6+
char* c=(char*)malloc(10);
7+
char* d=c;
8+
for(char i=0; i<10; i++, d++);
9+
assert((size_t)d==(size_t)c+10);
10+
}

‎regression/cbmc/address_space_size_limit2/test.desc

Lines changed: 5 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,5 @@
1+
KNOWNBUG
2+
test.c
3+
--32 --object-bits 31 --unwind 11 --no-simplify
4+
dynamic object too large
5+
--

‎regression/cbmc/address_space_size_limit3/main.c

Lines changed: 136 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,136 @@
1+
// copy of Pointer_Arithmetic12
2+
3+
#include <stdint.h>
4+
5+
#include <assert.h>
6+
7+
uint32_t __stack[32];
8+
9+
uint32_t eax;
10+
uint32_t ebp;
11+
uint32_t ebx;
12+
uint32_t ecx;
13+
uint32_t edi;
14+
uint32_t edx;
15+
uint32_t esi;
16+
uint32_t esp=(uint32_t)&(__stack[31]);
17+
uint32_t var0;
18+
uint32_t var1;
19+
uint32_t var10;
20+
uint32_t var11;
21+
uint32_t var12;
22+
uint32_t var13;
23+
uint32_t var14;
24+
uint32_t var15;
25+
uint32_t var16;
26+
uint32_t var2;
27+
uint32_t var3;
28+
uint32_t var4;
29+
uint32_t var5;
30+
uint32_t var6;
31+
uint32_t var7;
32+
uint32_t var8;
33+
uint32_t var9;
34+
35+
void g__L_0x3b4_0()
36+
{
37+
L_0x3b4_0: esp-=0x4;
38+
L_0x3b4_1: *(uint32_t*)(esp)=ebp;
39+
L_0x3b5_0: ebp=esp;
40+
L_0x3b7_0: var4=ebp;
41+
L_0x3b7_1: var4+=0xc;
42+
L_0x3b7_2: eax=*(uint32_t*)(var4);
43+
L_0x3ba_0: edx=eax;
44+
L_0x3bc_0: edx&=0x3;
45+
L_0x3bf_0: var5=ebp;
46+
L_0x3bf_1: var5+=0x8;
47+
L_0x3bf_2: eax=*(uint32_t*)(var5);
48+
L_0x3c2_0: *(uint32_t*)(eax)=edx;
49+
L_0x3c4_0: ebp=*(uint32_t*)(esp);
50+
L_0x3c4_1: esp+=0x4;
51+
L_0x3c5_0: return;
52+
}
53+
54+
void f__L_0x3c6_0()
55+
{
56+
L_0x3c6_0: esp-=0x4;
57+
L_0x3c6_1: *(uint32_t*)(esp)=ebp;
58+
L_0x3c7_0: ebp=esp;
59+
L_0x3c9_0: esp-=0x18;
60+
L_0x3cc_0: var6=ebp;
61+
L_0x3cc_1: var6-=0x4;
62+
L_0x3cc_2: *(uint32_t*)(var6)=0x0;
63+
L_0x3d3_0: var7=ebp;
64+
L_0x3d3_1: var7-=0x8;
65+
L_0x3d3_2: *(uint32_t*)(var7)=0x0;
66+
L_0x3da_0: var8=ebp;
67+
L_0x3da_1: var8+=0x8;
68+
L_0x3da_2: eax=*(uint32_t*)(var8);
69+
L_0x3dd_0: var9=ebp;
70+
L_0x3dd_1: var9-=0x4;
71+
L_0x3dd_2: *(uint32_t*)(var9)=eax;
72+
L_0x3e0_0: var10=ebp;
73+
L_0x3e0_1: var10-=0x4;
74+
L_0x3e0_2: eax=*(uint32_t*)(var10);
75+
L_0x3e3_0: var11=esp;
76+
L_0x3e3_1: var11+=0x4;
77+
L_0x3e3_2: *(uint32_t*)(var11)=eax;
78+
L_0x3e7_0: var12=ebp;
79+
L_0x3e7_1: var12-=0x8;
80+
L_0x3e7_2: eax=(uint32_t)&*(uint32_t*)(var12);
81+
L_0x3ea_0: *(uint32_t*)(esp)=eax;
82+
L_0x3ed_0: esp-=4; g__L_0x3b4_0(); esp+=4;
83+
L_0x3f2_0: var13=ebp;
84+
L_0x3f2_1: var13-=0x4;
85+
L_0x3f2_2: *(uint32_t*)(var13)=0x5;
86+
L_0x3f9_0: var14=ebp;
87+
L_0x3f9_1: var14-=0x8;
88+
L_0x3f9_2: eax=*(uint32_t*)(var14);
89+
L_0x3fc_0: esp=ebp;
90+
L_0x3fc_1: ebp=*(uint32_t*)(esp);
91+
L_0x3fc_2: esp+=0x4;
92+
L_0x3fd_0: return;
93+
}
94+
95+
int main()
96+
{
97+
L_0x3fe_0: esp-=0x4;
98+
L_0x3fe_1: *(uint32_t*)(esp)=ebp;
99+
L_0x3ff_0: ebp=esp;
100+
L_0x401_0: esp-=0x14;
101+
L_0x404_0: var15=ebp;
102+
L_0x404_1: var15-=0x4;
103+
#ifdef NONDET
104+
L_0x404_2: *(uint32_t*)(var15)=nondet_uint();
105+
#else
106+
L_0x404_2: *(uint32_t*)(var15)=0xffffffff;
107+
#endif
108+
L_0x40b_0: var16=ebp;
109+
L_0x40b_1: var16-=0x4;
110+
L_0x40b_2: eax=*(uint32_t*)(var16);
111+
L_0x40e_0: *(uint32_t*)(esp)=eax;
112+
L_0x411_0: esp-=4; f__L_0x3c6_0(); esp+=4;
113+
#if 1
114+
uint32_t eax1=eax;
115+
C_0x3ff_0: ebp=esp;
116+
C_0x401_0: esp-=0x14;
117+
C_0x404_0: var15=ebp;
118+
C_0x404_1: var15-=0x4;
119+
#ifdef NONDET
120+
C_0x404_2: *(uint32_t*)(var15)=nondet_uint();
121+
#else
122+
C_0x404_2: *(uint32_t*)(var15)=0xffffffff;
123+
#endif
124+
C_0x40b_0: var16=ebp;
125+
C_0x40b_1: var16-=0x4;
126+
C_0x40b_2: eax=*(uint32_t*)(var16);
127+
C_0x40e_0: *(uint32_t*)(esp)=eax;
128+
C_0x411_0: esp-=4; f__L_0x3c6_0(); esp+=4;
129+
uint32_t eax2=eax;
130+
assert(eax2==eax1);
131+
#endif
132+
L_0x416_0: esp=ebp;
133+
L_0x416_1: ebp=*(uint32_t*)(esp);
134+
L_0x416_2: esp+=0x4;
135+
L_0x417_0: return 0;
136+
}

‎regression/cbmc/address_space_size_limit3/test.desc

Lines changed: 11 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,11 @@
1+
CORE
2+
main.c
3+
--32 --little-endian --object-bits 25 --pointer-check
4+
^EXIT=10$
5+
^SIGNAL=0$
6+
^VERIFICATION FAILED$
7+
^.* dereference failure: pointer outside object bounds in .*: FAILURE$
8+
--
9+
^warning: ignoring
10+
--
11+
requires at least 8 offset bits

0 commit comments

Comments
 (0)