Skip to content

Commit a7c77db

Browse files
l-kentl-kent
l-kent
and
l-kent
authored
Atomic instructions support (#337)
* handling atomic sections in CAS for GTIRB input * handling atomic sections in BAP input + expanded support for memory loads in unusual places in BAP * move secure update check to be inside atomic section * fix crash * fix issue where old spec gammas were not automatically generated for guarantees * add sync_read and sync_write examples * add sync_write_spinlock example with required invariant described * update expected files * scalafmt * update expected * fixes * fix typo + add check that atomic sections contain blocks within a single procedure --------- Co-authored-by: l-kent <[email protected]>
1 parent d1f386c commit a7c77db

File tree

421 files changed

+14951
-13919
lines changed

Some content is hidden

Large Commits have some content hidden by default. Use the searchbox below for content that may be hidden.

421 files changed

+14951
-13919
lines changed

‎examples/sync_read/Makefile

+14
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,14 @@
1+
NAME=sync_read
2+
3+
all: relf gts
4+
5+
binary:
6+
clang-15 -target aarch64-linux-gnu -march=armv8.1-a -std=c11 $(NAME).c -o $(NAME).out
7+
8+
relf: binary
9+
aarch64-linux-gnu-readelf -s -r -W $(NAME).out > $(NAME).relf
10+
11+
gts: binary
12+
ddisasm $(NAME).out --ir $(NAME).gtirb
13+
gtirb-semantics $(NAME).gtirb $(NAME).gts
14+
rm -rf $(NAME).gtirb

‎examples/sync_read/sync_read.c

+16
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,16 @@
1+
#include <stdatomic.h>
2+
3+
long x = 0;
4+
atomic_long z = 0;
5+
6+
int main() {
7+
8+
long y;
9+
long expected = 0;
10+
if (atomic_compare_exchange_weak(&z, &expected, 2)) {
11+
y = x;
12+
z = 0;
13+
return y;
14+
}
15+
return -1;
16+
}

‎examples/sync_read/sync_read.gts

69.7 KB
Binary file not shown.

‎examples/sync_read/sync_read.relf

+124
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,124 @@
1+
2+
Relocation section '.rela.dyn' at offset 0x460 contains 8 entries:
3+
Offset Info Type Symbol's Value Symbol's Name + Addend
4+
0000000000010dc8 0000000000000403 R_AARCH64_RELATIVE 710
5+
0000000000010dd0 0000000000000403 R_AARCH64_RELATIVE 6c0
6+
0000000000010fd8 0000000000000403 R_AARCH64_RELATIVE 714
7+
0000000000011028 0000000000000403 R_AARCH64_RELATIVE 11028
8+
0000000000010fc0 0000000400000401 R_AARCH64_GLOB_DAT 0000000000000000 _ITM_deregisterTMCloneTable + 0
9+
0000000000010fc8 0000000500000401 R_AARCH64_GLOB_DAT 0000000000000000 __cxa_finalize@GLIBC_2.17 + 0
10+
0000000000010fd0 0000000600000401 R_AARCH64_GLOB_DAT 0000000000000000 __gmon_start__ + 0
11+
0000000000010fe0 0000000800000401 R_AARCH64_GLOB_DAT 0000000000000000 _ITM_registerTMCloneTable + 0
12+
13+
Relocation section '.rela.plt' at offset 0x520 contains 4 entries:
14+
Offset Info Type Symbol's Value Symbol's Name + Addend
15+
0000000000011000 0000000300000402 R_AARCH64_JUMP_SLOT 0000000000000000 __libc_start_main@GLIBC_2.34 + 0
16+
0000000000011008 0000000500000402 R_AARCH64_JUMP_SLOT 0000000000000000 __cxa_finalize@GLIBC_2.17 + 0
17+
0000000000011010 0000000600000402 R_AARCH64_JUMP_SLOT 0000000000000000 __gmon_start__ + 0
18+
0000000000011018 0000000700000402 R_AARCH64_JUMP_SLOT 0000000000000000 abort@GLIBC_2.17 + 0
19+
20+
Symbol table '.dynsym' contains 9 entries:
21+
Num: Value Size Type Bind Vis Ndx Name
22+
0: 0000000000000000 0 NOTYPE LOCAL DEFAULT UND
23+
1: 0000000000000580 0 SECTION LOCAL DEFAULT 11 .init
24+
2: 0000000000011020 0 SECTION LOCAL DEFAULT 23 .data
25+
3: 0000000000000000 0 FUNC GLOBAL DEFAULT UND __libc_start_main@GLIBC_2.34 (2)
26+
4: 0000000000000000 0 NOTYPE WEAK DEFAULT UND _ITM_deregisterTMCloneTable
27+
5: 0000000000000000 0 FUNC WEAK DEFAULT UND __cxa_finalize@GLIBC_2.17 (3)
28+
6: 0000000000000000 0 NOTYPE WEAK DEFAULT UND __gmon_start__
29+
7: 0000000000000000 0 FUNC GLOBAL DEFAULT UND abort@GLIBC_2.17 (3)
30+
8: 0000000000000000 0 NOTYPE WEAK DEFAULT UND _ITM_registerTMCloneTable
31+
32+
Symbol table '.symtab' contains 91 entries:
33+
Num: Value Size Type Bind Vis Ndx Name
34+
0: 0000000000000000 0 NOTYPE LOCAL DEFAULT UND
35+
1: 0000000000000238 0 SECTION LOCAL DEFAULT 1 .interp
36+
2: 0000000000000254 0 SECTION LOCAL DEFAULT 2 .note.gnu.build-id
37+
3: 0000000000000278 0 SECTION LOCAL DEFAULT 3 .note.ABI-tag
38+
4: 0000000000000298 0 SECTION LOCAL DEFAULT 4 .gnu.hash
39+
5: 00000000000002b8 0 SECTION LOCAL DEFAULT 5 .dynsym
40+
6: 0000000000000390 0 SECTION LOCAL DEFAULT 6 .dynstr
41+
7: 000000000000041e 0 SECTION LOCAL DEFAULT 7 .gnu.version
42+
8: 0000000000000430 0 SECTION LOCAL DEFAULT 8 .gnu.version_r
43+
9: 0000000000000460 0 SECTION LOCAL DEFAULT 9 .rela.dyn
44+
10: 0000000000000520 0 SECTION LOCAL DEFAULT 10 .rela.plt
45+
11: 0000000000000580 0 SECTION LOCAL DEFAULT 11 .init
46+
12: 00000000000005a0 0 SECTION LOCAL DEFAULT 12 .plt
47+
13: 0000000000000600 0 SECTION LOCAL DEFAULT 13 .text
48+
14: 00000000000007c0 0 SECTION LOCAL DEFAULT 14 .fini
49+
15: 00000000000007d4 0 SECTION LOCAL DEFAULT 15 .rodata
50+
16: 00000000000007d8 0 SECTION LOCAL DEFAULT 16 .eh_frame_hdr
51+
17: 0000000000000818 0 SECTION LOCAL DEFAULT 17 .eh_frame
52+
18: 0000000000010dc8 0 SECTION LOCAL DEFAULT 18 .init_array
53+
19: 0000000000010dd0 0 SECTION LOCAL DEFAULT 19 .fini_array
54+
20: 0000000000010dd8 0 SECTION LOCAL DEFAULT 20 .dynamic
55+
21: 0000000000010fb8 0 SECTION LOCAL DEFAULT 21 .got
56+
22: 0000000000010fe8 0 SECTION LOCAL DEFAULT 22 .got.plt
57+
23: 0000000000011020 0 SECTION LOCAL DEFAULT 23 .data
58+
24: 0000000000011030 0 SECTION LOCAL DEFAULT 24 .bss
59+
25: 0000000000000000 0 SECTION LOCAL DEFAULT 25 .comment
60+
26: 0000000000000000 0 FILE LOCAL DEFAULT ABS Scrt1.o
61+
27: 0000000000000278 0 NOTYPE LOCAL DEFAULT 3 $d
62+
28: 0000000000000278 32 OBJECT LOCAL DEFAULT 3 __abi_tag
63+
29: 0000000000000600 0 NOTYPE LOCAL DEFAULT 13 $x
64+
30: 000000000000082c 0 NOTYPE LOCAL DEFAULT 17 $d
65+
31: 00000000000007d4 0 NOTYPE LOCAL DEFAULT 15 $d
66+
32: 0000000000000000 0 FILE LOCAL DEFAULT ABS crti.o
67+
33: 0000000000000634 0 NOTYPE LOCAL DEFAULT 13 $x
68+
34: 0000000000000634 20 FUNC LOCAL DEFAULT 13 call_weak_fn
69+
35: 0000000000000580 0 NOTYPE LOCAL DEFAULT 11 $x
70+
36: 00000000000007c0 0 NOTYPE LOCAL DEFAULT 14 $x
71+
37: 0000000000000000 0 FILE LOCAL DEFAULT ABS crtn.o
72+
38: 0000000000000590 0 NOTYPE LOCAL DEFAULT 11 $x
73+
39: 00000000000007cc 0 NOTYPE LOCAL DEFAULT 14 $x
74+
40: 0000000000000000 0 FILE LOCAL DEFAULT ABS crtstuff.c
75+
41: 0000000000000650 0 NOTYPE LOCAL DEFAULT 13 $x
76+
42: 0000000000000650 0 FUNC LOCAL DEFAULT 13 deregister_tm_clones
77+
43: 0000000000000680 0 FUNC LOCAL DEFAULT 13 register_tm_clones
78+
44: 0000000000011028 0 NOTYPE LOCAL DEFAULT 23 $d
79+
45: 00000000000006c0 0 FUNC LOCAL DEFAULT 13 __do_global_dtors_aux
80+
46: 0000000000011030 1 OBJECT LOCAL DEFAULT 24 completed.0
81+
47: 0000000000010dd0 0 NOTYPE LOCAL DEFAULT 19 $d
82+
48: 0000000000010dd0 0 OBJECT LOCAL DEFAULT 19 __do_global_dtors_aux_fini_array_entry
83+
49: 0000000000000710 0 FUNC LOCAL DEFAULT 13 frame_dummy
84+
50: 0000000000010dc8 0 NOTYPE LOCAL DEFAULT 18 $d
85+
51: 0000000000010dc8 0 OBJECT LOCAL DEFAULT 18 __frame_dummy_init_array_entry
86+
52: 0000000000000840 0 NOTYPE LOCAL DEFAULT 17 $d
87+
53: 0000000000011030 0 NOTYPE LOCAL DEFAULT 24 $d
88+
54: 0000000000000000 0 FILE LOCAL DEFAULT ABS sync_read.c
89+
55: 0000000000000714 0 NOTYPE LOCAL DEFAULT 13 $x.0
90+
56: 0000000000011038 0 NOTYPE LOCAL DEFAULT 24 $d.1
91+
57: 000000000000002a 0 NOTYPE LOCAL DEFAULT 25 $d.2
92+
58: 00000000000008a0 0 NOTYPE LOCAL DEFAULT 17 $d.3
93+
59: 0000000000000000 0 FILE LOCAL DEFAULT ABS crtstuff.c
94+
60: 00000000000008cc 0 NOTYPE LOCAL DEFAULT 17 $d
95+
61: 00000000000008cc 0 OBJECT LOCAL DEFAULT 17 __FRAME_END__
96+
62: 0000000000000000 0 FILE LOCAL DEFAULT ABS
97+
63: 0000000000010dd8 0 OBJECT LOCAL DEFAULT ABS _DYNAMIC
98+
64: 00000000000007d8 0 NOTYPE LOCAL DEFAULT 16 __GNU_EH_FRAME_HDR
99+
65: 0000000000010fb8 0 OBJECT LOCAL DEFAULT ABS _GLOBAL_OFFSET_TABLE_
100+
66: 00000000000005a0 0 NOTYPE LOCAL DEFAULT 12 $x
101+
67: 0000000000000000 0 FUNC GLOBAL DEFAULT UND __libc_start_main@GLIBC_2.34
102+
68: 0000000000000000 0 NOTYPE WEAK DEFAULT UND _ITM_deregisterTMCloneTable
103+
69: 0000000000011020 0 NOTYPE WEAK DEFAULT 23 data_start
104+
70: 0000000000011030 0 NOTYPE GLOBAL DEFAULT 24 __bss_start__
105+
71: 0000000000000000 0 FUNC WEAK DEFAULT UND __cxa_finalize@GLIBC_2.17
106+
72: 0000000000011048 0 NOTYPE GLOBAL DEFAULT 24 _bss_end__
107+
73: 0000000000011030 0 NOTYPE GLOBAL DEFAULT 23 _edata
108+
74: 0000000000011040 8 OBJECT GLOBAL DEFAULT 24 z
109+
75: 0000000000011038 8 OBJECT GLOBAL DEFAULT 24 x
110+
76: 00000000000007c0 0 FUNC GLOBAL HIDDEN 14 _fini
111+
77: 0000000000011048 0 NOTYPE GLOBAL DEFAULT 24 __bss_end__
112+
78: 0000000000011020 0 NOTYPE GLOBAL DEFAULT 23 __data_start
113+
79: 0000000000000000 0 NOTYPE WEAK DEFAULT UND __gmon_start__
114+
80: 0000000000011028 0 OBJECT GLOBAL HIDDEN 23 __dso_handle
115+
81: 0000000000000000 0 FUNC GLOBAL DEFAULT UND abort@GLIBC_2.17
116+
82: 00000000000007d4 4 OBJECT GLOBAL DEFAULT 15 _IO_stdin_used
117+
83: 0000000000011048 0 NOTYPE GLOBAL DEFAULT 24 _end
118+
84: 0000000000000600 52 FUNC GLOBAL DEFAULT 13 _start
119+
85: 0000000000011048 0 NOTYPE GLOBAL DEFAULT 24 __end__
120+
86: 0000000000011030 0 NOTYPE GLOBAL DEFAULT 24 __bss_start
121+
87: 0000000000000714 172 FUNC GLOBAL DEFAULT 13 main
122+
88: 0000000000011030 0 OBJECT GLOBAL HIDDEN 23 __TMC_END__
123+
89: 0000000000000000 0 NOTYPE WEAK DEFAULT UND _ITM_registerTMCloneTable
124+
90: 0000000000000580 0 FUNC GLOBAL HIDDEN 11 _init

‎examples/sync_read/sync_read.spec

+12
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,12 @@
1+
Globals:
2+
z: bv64
3+
x: bv64
4+
5+
L: z -> true, x -> z != 1bv64
6+
Rely: (old(z) == 2bv64) ==> (old(z) == z && (old(Gamma_x) ==> Gamma_x))
7+
Guarantee: old(x) == x, old(z) == 1bv64 ==> z == old(z)
8+
9+
Subroutine: main
10+
Requires: Gamma_x == true
11+
Requires: Gamma_z == true
12+
Requires: z == 0bv64

‎examples/sync_write/Makefile

+14
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,14 @@
1+
NAME=sync_write
2+
3+
all: relf gts
4+
5+
binary:
6+
clang-15 -target aarch64-linux-gnu -march=armv8.1-a -std=c11 $(NAME).c -o $(NAME).out
7+
8+
relf: binary
9+
aarch64-linux-gnu-readelf -s -r -W $(NAME).out > $(NAME).relf
10+
11+
gts: binary
12+
ddisasm $(NAME).out --ir $(NAME).gtirb
13+
gtirb-semantics $(NAME).gtirb $(NAME).gts
14+
rm -rf $(NAME).gtirb

‎examples/sync_write/sync_write.c

+17
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,17 @@
1+
#include <stdatomic.h>
2+
3+
int x = 0;
4+
atomic_int z;
5+
int secret;
6+
7+
int main() {
8+
int expected = 0;
9+
if (atomic_compare_exchange_weak(&z, &expected, 1)) {
10+
x = secret;
11+
x = 0;
12+
z = 0;
13+
return 1;
14+
}
15+
return -1;
16+
17+
}

‎examples/sync_write/sync_write.gts

70.9 KB
Binary file not shown.

‎examples/sync_write/sync_write.relf

+125
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,125 @@
1+
2+
Relocation section '.rela.dyn' at offset 0x460 contains 8 entries:
3+
Offset Info Type Symbol's Value Symbol's Name + Addend
4+
0000000000010dc8 0000000000000403 R_AARCH64_RELATIVE 710
5+
0000000000010dd0 0000000000000403 R_AARCH64_RELATIVE 6c0
6+
0000000000010fd8 0000000000000403 R_AARCH64_RELATIVE 714
7+
0000000000011028 0000000000000403 R_AARCH64_RELATIVE 11028
8+
0000000000010fc0 0000000400000401 R_AARCH64_GLOB_DAT 0000000000000000 _ITM_deregisterTMCloneTable + 0
9+
0000000000010fc8 0000000500000401 R_AARCH64_GLOB_DAT 0000000000000000 __cxa_finalize@GLIBC_2.17 + 0
10+
0000000000010fd0 0000000600000401 R_AARCH64_GLOB_DAT 0000000000000000 __gmon_start__ + 0
11+
0000000000010fe0 0000000800000401 R_AARCH64_GLOB_DAT 0000000000000000 _ITM_registerTMCloneTable + 0
12+
13+
Relocation section '.rela.plt' at offset 0x520 contains 4 entries:
14+
Offset Info Type Symbol's Value Symbol's Name + Addend
15+
0000000000011000 0000000300000402 R_AARCH64_JUMP_SLOT 0000000000000000 __libc_start_main@GLIBC_2.34 + 0
16+
0000000000011008 0000000500000402 R_AARCH64_JUMP_SLOT 0000000000000000 __cxa_finalize@GLIBC_2.17 + 0
17+
0000000000011010 0000000600000402 R_AARCH64_JUMP_SLOT 0000000000000000 __gmon_start__ + 0
18+
0000000000011018 0000000700000402 R_AARCH64_JUMP_SLOT 0000000000000000 abort@GLIBC_2.17 + 0
19+
20+
Symbol table '.dynsym' contains 9 entries:
21+
Num: Value Size Type Bind Vis Ndx Name
22+
0: 0000000000000000 0 NOTYPE LOCAL DEFAULT UND
23+
1: 0000000000000580 0 SECTION LOCAL DEFAULT 11 .init
24+
2: 0000000000011020 0 SECTION LOCAL DEFAULT 23 .data
25+
3: 0000000000000000 0 FUNC GLOBAL DEFAULT UND __libc_start_main@GLIBC_2.34 (2)
26+
4: 0000000000000000 0 NOTYPE WEAK DEFAULT UND _ITM_deregisterTMCloneTable
27+
5: 0000000000000000 0 FUNC WEAK DEFAULT UND __cxa_finalize@GLIBC_2.17 (3)
28+
6: 0000000000000000 0 NOTYPE WEAK DEFAULT UND __gmon_start__
29+
7: 0000000000000000 0 FUNC GLOBAL DEFAULT UND abort@GLIBC_2.17 (3)
30+
8: 0000000000000000 0 NOTYPE WEAK DEFAULT UND _ITM_registerTMCloneTable
31+
32+
Symbol table '.symtab' contains 92 entries:
33+
Num: Value Size Type Bind Vis Ndx Name
34+
0: 0000000000000000 0 NOTYPE LOCAL DEFAULT UND
35+
1: 0000000000000238 0 SECTION LOCAL DEFAULT 1 .interp
36+
2: 0000000000000254 0 SECTION LOCAL DEFAULT 2 .note.gnu.build-id
37+
3: 0000000000000278 0 SECTION LOCAL DEFAULT 3 .note.ABI-tag
38+
4: 0000000000000298 0 SECTION LOCAL DEFAULT 4 .gnu.hash
39+
5: 00000000000002b8 0 SECTION LOCAL DEFAULT 5 .dynsym
40+
6: 0000000000000390 0 SECTION LOCAL DEFAULT 6 .dynstr
41+
7: 000000000000041e 0 SECTION LOCAL DEFAULT 7 .gnu.version
42+
8: 0000000000000430 0 SECTION LOCAL DEFAULT 8 .gnu.version_r
43+
9: 0000000000000460 0 SECTION LOCAL DEFAULT 9 .rela.dyn
44+
10: 0000000000000520 0 SECTION LOCAL DEFAULT 10 .rela.plt
45+
11: 0000000000000580 0 SECTION LOCAL DEFAULT 11 .init
46+
12: 00000000000005a0 0 SECTION LOCAL DEFAULT 12 .plt
47+
13: 0000000000000600 0 SECTION LOCAL DEFAULT 13 .text
48+
14: 00000000000007c8 0 SECTION LOCAL DEFAULT 14 .fini
49+
15: 00000000000007dc 0 SECTION LOCAL DEFAULT 15 .rodata
50+
16: 00000000000007e0 0 SECTION LOCAL DEFAULT 16 .eh_frame_hdr
51+
17: 0000000000000820 0 SECTION LOCAL DEFAULT 17 .eh_frame
52+
18: 0000000000010dc8 0 SECTION LOCAL DEFAULT 18 .init_array
53+
19: 0000000000010dd0 0 SECTION LOCAL DEFAULT 19 .fini_array
54+
20: 0000000000010dd8 0 SECTION LOCAL DEFAULT 20 .dynamic
55+
21: 0000000000010fb8 0 SECTION LOCAL DEFAULT 21 .got
56+
22: 0000000000010fe8 0 SECTION LOCAL DEFAULT 22 .got.plt
57+
23: 0000000000011020 0 SECTION LOCAL DEFAULT 23 .data
58+
24: 0000000000011030 0 SECTION LOCAL DEFAULT 24 .bss
59+
25: 0000000000000000 0 SECTION LOCAL DEFAULT 25 .comment
60+
26: 0000000000000000 0 FILE LOCAL DEFAULT ABS Scrt1.o
61+
27: 0000000000000278 0 NOTYPE LOCAL DEFAULT 3 $d
62+
28: 0000000000000278 32 OBJECT LOCAL DEFAULT 3 __abi_tag
63+
29: 0000000000000600 0 NOTYPE LOCAL DEFAULT 13 $x
64+
30: 0000000000000834 0 NOTYPE LOCAL DEFAULT 17 $d
65+
31: 00000000000007dc 0 NOTYPE LOCAL DEFAULT 15 $d
66+
32: 0000000000000000 0 FILE LOCAL DEFAULT ABS crti.o
67+
33: 0000000000000634 0 NOTYPE LOCAL DEFAULT 13 $x
68+
34: 0000000000000634 20 FUNC LOCAL DEFAULT 13 call_weak_fn
69+
35: 0000000000000580 0 NOTYPE LOCAL DEFAULT 11 $x
70+
36: 00000000000007c8 0 NOTYPE LOCAL DEFAULT 14 $x
71+
37: 0000000000000000 0 FILE LOCAL DEFAULT ABS crtn.o
72+
38: 0000000000000590 0 NOTYPE LOCAL DEFAULT 11 $x
73+
39: 00000000000007d4 0 NOTYPE LOCAL DEFAULT 14 $x
74+
40: 0000000000000000 0 FILE LOCAL DEFAULT ABS crtstuff.c
75+
41: 0000000000000650 0 NOTYPE LOCAL DEFAULT 13 $x
76+
42: 0000000000000650 0 FUNC LOCAL DEFAULT 13 deregister_tm_clones
77+
43: 0000000000000680 0 FUNC LOCAL DEFAULT 13 register_tm_clones
78+
44: 0000000000011028 0 NOTYPE LOCAL DEFAULT 23 $d
79+
45: 00000000000006c0 0 FUNC LOCAL DEFAULT 13 __do_global_dtors_aux
80+
46: 0000000000011030 1 OBJECT LOCAL DEFAULT 24 completed.0
81+
47: 0000000000010dd0 0 NOTYPE LOCAL DEFAULT 19 $d
82+
48: 0000000000010dd0 0 OBJECT LOCAL DEFAULT 19 __do_global_dtors_aux_fini_array_entry
83+
49: 0000000000000710 0 FUNC LOCAL DEFAULT 13 frame_dummy
84+
50: 0000000000010dc8 0 NOTYPE LOCAL DEFAULT 18 $d
85+
51: 0000000000010dc8 0 OBJECT LOCAL DEFAULT 18 __frame_dummy_init_array_entry
86+
52: 0000000000000848 0 NOTYPE LOCAL DEFAULT 17 $d
87+
53: 0000000000011030 0 NOTYPE LOCAL DEFAULT 24 $d
88+
54: 0000000000000000 0 FILE LOCAL DEFAULT ABS sync_write.c
89+
55: 0000000000000714 0 NOTYPE LOCAL DEFAULT 13 $x.0
90+
56: 0000000000011034 0 NOTYPE LOCAL DEFAULT 24 $d.1
91+
57: 000000000000002a 0 NOTYPE LOCAL DEFAULT 25 $d.2
92+
58: 00000000000008a8 0 NOTYPE LOCAL DEFAULT 17 $d.3
93+
59: 0000000000000000 0 FILE LOCAL DEFAULT ABS crtstuff.c
94+
60: 00000000000008d4 0 NOTYPE LOCAL DEFAULT 17 $d
95+
61: 00000000000008d4 0 OBJECT LOCAL DEFAULT 17 __FRAME_END__
96+
62: 0000000000000000 0 FILE LOCAL DEFAULT ABS
97+
63: 0000000000010dd8 0 OBJECT LOCAL DEFAULT ABS _DYNAMIC
98+
64: 00000000000007e0 0 NOTYPE LOCAL DEFAULT 16 __GNU_EH_FRAME_HDR
99+
65: 0000000000010fb8 0 OBJECT LOCAL DEFAULT ABS _GLOBAL_OFFSET_TABLE_
100+
66: 00000000000005a0 0 NOTYPE LOCAL DEFAULT 12 $x
101+
67: 0000000000000000 0 FUNC GLOBAL DEFAULT UND __libc_start_main@GLIBC_2.34
102+
68: 0000000000000000 0 NOTYPE WEAK DEFAULT UND _ITM_deregisterTMCloneTable
103+
69: 0000000000011020 0 NOTYPE WEAK DEFAULT 23 data_start
104+
70: 0000000000011030 0 NOTYPE GLOBAL DEFAULT 24 __bss_start__
105+
71: 0000000000000000 0 FUNC WEAK DEFAULT UND __cxa_finalize@GLIBC_2.17
106+
72: 0000000000011040 0 NOTYPE GLOBAL DEFAULT 24 _bss_end__
107+
73: 0000000000011030 0 NOTYPE GLOBAL DEFAULT 23 _edata
108+
74: 0000000000011038 4 OBJECT GLOBAL DEFAULT 24 z
109+
75: 0000000000011034 4 OBJECT GLOBAL DEFAULT 24 x
110+
76: 00000000000007c8 0 FUNC GLOBAL HIDDEN 14 _fini
111+
77: 0000000000011040 0 NOTYPE GLOBAL DEFAULT 24 __bss_end__
112+
78: 0000000000011020 0 NOTYPE GLOBAL DEFAULT 23 __data_start
113+
79: 0000000000000000 0 NOTYPE WEAK DEFAULT UND __gmon_start__
114+
80: 0000000000011028 0 OBJECT GLOBAL HIDDEN 23 __dso_handle
115+
81: 0000000000000000 0 FUNC GLOBAL DEFAULT UND abort@GLIBC_2.17
116+
82: 00000000000007dc 4 OBJECT GLOBAL DEFAULT 15 _IO_stdin_used
117+
83: 000000000001103c 4 OBJECT GLOBAL DEFAULT 24 secret
118+
84: 0000000000011040 0 NOTYPE GLOBAL DEFAULT 24 _end
119+
85: 0000000000000600 52 FUNC GLOBAL DEFAULT 13 _start
120+
86: 0000000000011040 0 NOTYPE GLOBAL DEFAULT 24 __end__
121+
87: 0000000000011030 0 NOTYPE GLOBAL DEFAULT 24 __bss_start
122+
88: 0000000000000714 180 FUNC GLOBAL DEFAULT 13 main
123+
89: 0000000000011030 0 OBJECT GLOBAL HIDDEN 23 __TMC_END__
124+
90: 0000000000000000 0 NOTYPE WEAK DEFAULT UND _ITM_registerTMCloneTable
125+
91: 0000000000000580 0 FUNC GLOBAL HIDDEN 11 _init

‎examples/sync_write/sync_write.spec

+8
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,8 @@
1+
Globals:
2+
z: bv32
3+
x: bv32
4+
secret: bv32
5+
6+
L: z -> true, x -> z != 1bv32, secret -> false
7+
Rely: old(Gamma_x) ==> Gamma_x, old(z) == 1bv32 ==> z == old(z)
8+
Guarantee: old(z) == 2bv32 ==> old(z) == z && old(x) == x

‎examples/sync_write_spinlock/Makefile

+14
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,14 @@
1+
NAME=sync_write
2+
3+
all: relf gts
4+
5+
binary:
6+
clang-15 -target aarch64-linux-gnu -march=armv8.1-a -std=c11 $(NAME).c -o $(NAME).out
7+
8+
relf: binary
9+
aarch64-linux-gnu-readelf -s -r -W $(NAME).out > $(NAME).relf
10+
11+
gts: binary
12+
ddisasm $(NAME).out --ir $(NAME).gtirb
13+
gtirb-semantics $(NAME).gtirb $(NAME).gts
14+
rm -rf $(NAME).gtirb

‎examples/sync_write_spinlock/readme.md

+9
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,9 @@
1+
This verifies if the following loop invariant is added to the Boogie output:
2+
3+
```
4+
main_1812__1__rlVqjjqoR6uHwOYvPCS15g:
5+
assume memory_load32_le(stack, bvadd64(R31, 24bv64)) == 0bv32;
6+
assume gamma_load32(Gamma_stack, bvadd64(R31, 24bv64));
7+
```
8+
9+
This invariant simply saying that the local variable 'expected' from the source code is always 0 at the start of the loop and always has a low security level.

0 commit comments

Comments
 (0)