Skip to content

Commit

Permalink
Merge branch 'main' into worklist-perf
Browse files Browse the repository at this point in the history
  • Loading branch information
ailrst committed Nov 6, 2023
2 parents c665824 + e63dcc1 commit 7a4c3a5
Show file tree
Hide file tree
Showing 34 changed files with 2,527 additions and 553 deletions.
5 changes: 1 addition & 4 deletions .gitignore
Original file line number Diff line number Diff line change
Expand Up @@ -8,18 +8,15 @@
gen/
out/
target/
boogie_out.txt
boogie_out.bpl
metals.sbt
password.txt
*.iml
*.out
samples/const_prop_tests/
src/main/antlr4/.antlr
*.bpl
*.dot
*.il
result.txt
*.txt
examplesold/
src/test/scala/dump/
src/test/analysis/dump/
518 changes: 518 additions & 0 deletions examples/basic_local_reassign/basic_local_reassign.adt

Large diffs are not rendered by default.

234 changes: 234 additions & 0 deletions examples/basic_local_reassign/basic_local_reassign.bir
Original file line number Diff line number Diff line change
@@ -0,0 +1,234 @@
000005d7: program
000005c1: sub __cxa_finalize(__cxa_finalize_result)
000005d8: __cxa_finalize_result :: out u32 = low:32[R0]

0000036d:
00000465: R16 := 0x1F000
0000046c: R17 := mem[R16 + 0xFB8, el]:u64
00000472: R16 := R16 + 0xFB8
00000477: call R17 with noreturn

000005c2: sub __do_global_dtors_aux(__do_global_dtors_aux_result)
000005d9: __do_global_dtors_aux_result :: out u32 = low:32[R0]

0000028e:
00000292: #3 := R31 - 0x20
00000298: mem := mem with [#3, el]:u64 <- R29
0000029e: mem := mem with [#3 + 8, el]:u64 <- R30
000002a2: R31 := #3
000002a8: R29 := R31
000002b0: mem := mem with [R31 + 0x10, el]:u64 <- R19
000002b5: R19 := 0x20000
000002bc: R0 := pad:64[mem[R19 + 0x10]]
000002c3: when 31:0[R0] <> 0 goto %000002c1
000005c3: goto %00000336

00000336:
00000339: R0 := 0x1F000
00000340: R0 := mem[R0 + 0xFE0, el]:u64
00000346: when R0 = 0 goto %00000344
000005c4: goto %0000035d

0000035d:
00000360: R0 := 0x20000
00000367: R0 := mem[R0 + 8, el]:u64
0000036c: R30 := 0x6F0
0000036f: call @__cxa_finalize with return %00000344

00000344:
0000034c: R30 := 0x6F4
0000034e: call @deregister_tm_clones with return %00000350

00000350:
00000353: R0 := 1
0000035b: mem := mem with [R19 + 0x10] <- 7:0[R0]
000005c5: goto %000002c1

000002c1:
000002cb: R19 := mem[R31 + 0x10, el]:u64
000002d2: R29 := mem[R31, el]:u64
000002d7: R30 := mem[R31 + 8, el]:u64
000002db: R31 := R31 + 0x20
000002e0: call R30 with noreturn

000005c6: sub __libc_start_main(__libc_start_main_main, __libc_start_main_arg2, __libc_start_main_arg3, __libc_start_main_auxv, __libc_start_main_result)
000005da: __libc_start_main_main :: in u64 = R0
000005db: __libc_start_main_arg2 :: in u32 = low:32[R1]
000005dc: __libc_start_main_arg3 :: in out u64 = R2
000005dd: __libc_start_main_auxv :: in out u64 = R3
000005de: __libc_start_main_result :: out u32 = low:32[R0]

000001e7:
0000044f: R16 := 0x1F000
00000456: R17 := mem[R16 + 0xFB0, el]:u64
0000045c: R16 := R16 + 0xFB0
00000461: call R17 with noreturn

000005c7: sub _fini(_fini_result)
000005df: _fini_result :: out u32 = low:32[R0]

0000002f:
00000035: #0 := R31 - 0x10
0000003b: mem := mem with [#0, el]:u64 <- R29
00000041: mem := mem with [#0 + 8, el]:u64 <- R30
00000045: R31 := #0
0000004b: R29 := R31
00000052: R29 := mem[R31, el]:u64
00000057: R30 := mem[R31 + 8, el]:u64
0000005b: R31 := R31 + 0x10
00000060: call R30 with noreturn

000005c8: sub _init(_init_result)
000005e0: _init_result :: out u32 = low:32[R0]

00000517:
0000051d: #5 := R31 - 0x10
00000523: mem := mem with [#5, el]:u64 <- R29
00000529: mem := mem with [#5 + 8, el]:u64 <- R30
0000052d: R31 := #5
00000533: R29 := R31
00000538: R30 := 0x598
0000053a: call @call_weak_fn with return %0000053c

0000053c:
00000541: R29 := mem[R31, el]:u64
00000546: R30 := mem[R31 + 8, el]:u64
0000054a: R31 := R31 + 0x10
0000054f: call R30 with noreturn

000005c9: sub _start(_start_result)
000005e1: _start_result :: out u32 = low:32[R0]

000001a8:
000001ad: R29 := 0
000001b2: R30 := 0
000001b8: R5 := R0
000001bf: R1 := mem[R31, el]:u64
000001c5: R2 := R31 + 8
000001cb: R6 := R31
000001d0: R0 := 0x1F000
000001d7: R0 := mem[R0 + 0xFF0, el]:u64
000001dc: R3 := 0
000001e1: R4 := 0
000001e6: R30 := 0x630
000001e9: call @__libc_start_main with return %000001eb

000001eb:
000001ee: R30 := 0x634
000001f1: call @abort with return %000005ca

000005ca:
000005cb: call @call_weak_fn with noreturn

000005cc: sub abort()


000001ef:
00000491: R16 := 0x1F000
00000498: R17 := mem[R16 + 0xFC8, el]:u64
0000049e: R16 := R16 + 0xFC8
000004a3: call R17 with noreturn

000005cd: sub call_weak_fn(call_weak_fn_result)
000005e2: call_weak_fn_result :: out u32 = low:32[R0]

000001f3:
000001f6: R0 := 0x1F000
000001fd: R0 := mem[R0 + 0xFE8, el]:u64
00000203: when R0 = 0 goto %00000201
000005ce: goto %000003ad

00000201:
00000209: call R30 with noreturn

000003ad:
000003b0: goto @__gmon_start__

000003ae:
0000047b: R16 := 0x1F000
00000482: R17 := mem[R16 + 0xFC0, el]:u64
00000488: R16 := R16 + 0xFC0
0000048d: call R17 with noreturn

000005cf: sub deregister_tm_clones(deregister_tm_clones_result)
000005e3: deregister_tm_clones_result :: out u32 = low:32[R0]

0000020f:
00000212: R0 := 0x20000
00000218: R0 := R0 + 0x10
0000021d: R1 := 0x20000
00000223: R1 := R1 + 0x10
00000229: #1 := ~R0
0000022e: #2 := R1 + ~R0
00000234: VF := extend:65[#2 + 1] <> extend:65[R1] + extend:65[#1] + 1
0000023a: CF := pad:65[#2 + 1] <> pad:65[R1] + pad:65[#1] + 1
0000023e: ZF := #2 + 1 = 0
00000242: NF := 63:63[#2 + 1]
00000248: when ZF goto %00000246
000005d0: goto %0000038f

0000038f:
00000392: R1 := 0x1F000
00000399: R1 := mem[R1 + 0xFD8, el]:u64
0000039e: when R1 = 0 goto %00000246
000005d1: goto %000003a2

00000246:
0000024e: call R30 with noreturn

000003a2:
000003a6: R16 := R1
000003ab: call R16 with noreturn

000005d2: sub frame_dummy(frame_dummy_result)
000005e4: frame_dummy_result :: out u32 = low:32[R0]

000002e6:
000002e8: call @register_tm_clones with noreturn

000005d3: sub main(main_argc, main_argv, main_result)
000005e5: main_argc :: in u32 = low:32[R0]
000005e6: main_argv :: in out u64 = R1
000005e7: main_result :: out u32 = low:32[R0]

000002ea:
000002ee: R31 := R31 - 0x10
000002f5: mem := mem with [R31 + 0xC, el]:u32 <- 0
000002fc: R0 := pad:64[mem[R31 + 0xC, el]:u32]
00000302: R0 := pad:64[31:0[R0] + 1]
0000030a: mem := mem with [R31 + 0xC, el]:u32 <- 31:0[R0]
0000030f: R0 := 3
00000317: mem := mem with [R31 + 0xC, el]:u32 <- 31:0[R0]
0000031c: R0 := 0xA
00000324: mem := mem with [R31 + 0xC, el]:u32 <- 31:0[R0]
00000329: R0 := 0
0000032f: R31 := R31 + 0x10
00000334: call R30 with noreturn

000005d4: sub register_tm_clones(register_tm_clones_result)
000005e8: register_tm_clones_result :: out u32 = low:32[R0]

00000250:
00000253: R0 := 0x20000
00000259: R0 := R0 + 0x10
0000025e: R1 := 0x20000
00000264: R1 := R1 + 0x10
0000026b: R1 := R1 + ~R0 + 1
00000271: R2 := 0.63:63[R1]
00000278: R1 := R2 + (R1 ~>> 3)
0000027e: R1 := extend:64[63:1[R1]]
00000284: when R1 = 0 goto %00000282
000005d5: goto %00000371

00000371:
00000374: R2 := 0x1F000
0000037b: R2 := mem[R2 + 0xFF8, el]:u64
00000380: when R2 = 0 goto %00000282
000005d6: goto %00000384

00000282:
0000028a: call R30 with noreturn

00000384:
00000388: R16 := R2
0000038d: call R16 with noreturn
6 changes: 6 additions & 0 deletions examples/basic_local_reassign/basic_local_reassign.c
Original file line number Diff line number Diff line change
@@ -0,0 +1,6 @@
int main() {
int z = 0;
z = z + 1;
z = 3;
z = 10;
}
125 changes: 125 additions & 0 deletions examples/basic_local_reassign/basic_local_reassign.relf
Original file line number Diff line number Diff line change
@@ -0,0 +1,125 @@

Relocation section '.rela.dyn' at offset 0x468 contains 8 entries:
Offset Info Type Symbol's Value Symbol's Name + Addend
000000000001fd88 0000000000000403 R_AARCH64_RELATIVE 710
000000000001fd90 0000000000000403 R_AARCH64_RELATIVE 6c0
000000000001fff0 0000000000000403 R_AARCH64_RELATIVE 714
0000000000020008 0000000000000403 R_AARCH64_RELATIVE 20008
000000000001ffd8 0000000400000401 R_AARCH64_GLOB_DAT 0000000000000000 _ITM_deregisterTMCloneTable + 0
000000000001ffe0 0000000500000401 R_AARCH64_GLOB_DAT 0000000000000000 __cxa_finalize@GLIBC_2.17 + 0
000000000001ffe8 0000000600000401 R_AARCH64_GLOB_DAT 0000000000000000 __gmon_start__ + 0
000000000001fff8 0000000800000401 R_AARCH64_GLOB_DAT 0000000000000000 _ITM_registerTMCloneTable + 0

Relocation section '.rela.plt' at offset 0x528 contains 4 entries:
Offset Info Type Symbol's Value Symbol's Name + Addend
000000000001ffb0 0000000300000402 R_AARCH64_JUMP_SLOT 0000000000000000 __libc_start_main@GLIBC_2.34 + 0
000000000001ffb8 0000000500000402 R_AARCH64_JUMP_SLOT 0000000000000000 __cxa_finalize@GLIBC_2.17 + 0
000000000001ffc0 0000000600000402 R_AARCH64_JUMP_SLOT 0000000000000000 __gmon_start__ + 0
000000000001ffc8 0000000700000402 R_AARCH64_JUMP_SLOT 0000000000000000 abort@GLIBC_2.17 + 0

Symbol table '.dynsym' contains 9 entries:
Num: Value Size Type Bind Vis Ndx Name
0: 0000000000000000 0 NOTYPE LOCAL DEFAULT UND
1: 0000000000000588 0 SECTION LOCAL DEFAULT 11 .init
2: 0000000000020000 0 SECTION LOCAL DEFAULT 22 .data
3: 0000000000000000 0 FUNC GLOBAL DEFAULT UND __libc_start_main@GLIBC_2.34 (2)
4: 0000000000000000 0 NOTYPE WEAK DEFAULT UND _ITM_deregisterTMCloneTable
5: 0000000000000000 0 FUNC WEAK DEFAULT UND __cxa_finalize@GLIBC_2.17 (3)
6: 0000000000000000 0 NOTYPE WEAK DEFAULT UND __gmon_start__
7: 0000000000000000 0 FUNC GLOBAL DEFAULT UND abort@GLIBC_2.17 (3)
8: 0000000000000000 0 NOTYPE WEAK DEFAULT UND _ITM_registerTMCloneTable

Symbol table '.symtab' contains 92 entries:
Num: Value Size Type Bind Vis Ndx Name
0: 0000000000000000 0 NOTYPE LOCAL DEFAULT UND
1: 0000000000000238 0 SECTION LOCAL DEFAULT 1 .interp
2: 0000000000000254 0 SECTION LOCAL DEFAULT 2 .note.gnu.build-id
3: 0000000000000278 0 SECTION LOCAL DEFAULT 3 .note.ABI-tag
4: 0000000000000298 0 SECTION LOCAL DEFAULT 4 .gnu.hash
5: 00000000000002b8 0 SECTION LOCAL DEFAULT 5 .dynsym
6: 0000000000000390 0 SECTION LOCAL DEFAULT 6 .dynstr
7: 0000000000000424 0 SECTION LOCAL DEFAULT 7 .gnu.version
8: 0000000000000438 0 SECTION LOCAL DEFAULT 8 .gnu.version_r
9: 0000000000000468 0 SECTION LOCAL DEFAULT 9 .rela.dyn
10: 0000000000000528 0 SECTION LOCAL DEFAULT 10 .rela.plt
11: 0000000000000588 0 SECTION LOCAL DEFAULT 11 .init
12: 00000000000005a0 0 SECTION LOCAL DEFAULT 12 .plt
13: 0000000000000600 0 SECTION LOCAL DEFAULT 13 .text
14: 0000000000000744 0 SECTION LOCAL DEFAULT 14 .fini
15: 0000000000000758 0 SECTION LOCAL DEFAULT 15 .rodata
16: 000000000000075c 0 SECTION LOCAL DEFAULT 16 .eh_frame_hdr
17: 0000000000000798 0 SECTION LOCAL DEFAULT 17 .eh_frame
18: 000000000001fd88 0 SECTION LOCAL DEFAULT 18 .init_array
19: 000000000001fd90 0 SECTION LOCAL DEFAULT 19 .fini_array
20: 000000000001fd98 0 SECTION LOCAL DEFAULT 20 .dynamic
21: 000000000001ff98 0 SECTION LOCAL DEFAULT 21 .got
22: 0000000000020000 0 SECTION LOCAL DEFAULT 22 .data
23: 0000000000020010 0 SECTION LOCAL DEFAULT 23 .bss
24: 0000000000000000 0 SECTION LOCAL DEFAULT 24 .comment
25: 0000000000000000 0 SECTION LOCAL DEFAULT 25 .debug_aranges
26: 0000000000000000 0 SECTION LOCAL DEFAULT 26 .debug_info
27: 0000000000000000 0 SECTION LOCAL DEFAULT 27 .debug_abbrev
28: 0000000000000000 0 SECTION LOCAL DEFAULT 28 .debug_line
29: 0000000000000000 0 SECTION LOCAL DEFAULT 29 .debug_str
30: 0000000000000000 0 SECTION LOCAL DEFAULT 30 .debug_line_str
31: 0000000000000000 0 FILE LOCAL DEFAULT ABS Scrt1.o
32: 0000000000000278 0 NOTYPE LOCAL DEFAULT 3 $d
33: 0000000000000278 32 OBJECT LOCAL DEFAULT 3 __abi_tag
34: 0000000000000600 0 NOTYPE LOCAL DEFAULT 13 $x
35: 00000000000007ac 0 NOTYPE LOCAL DEFAULT 17 $d
36: 0000000000000758 0 NOTYPE LOCAL DEFAULT 15 $d
37: 0000000000000000 0 FILE LOCAL DEFAULT ABS crti.o
38: 0000000000000634 0 NOTYPE LOCAL DEFAULT 13 $x
39: 0000000000000634 20 FUNC LOCAL DEFAULT 13 call_weak_fn
40: 0000000000000588 0 NOTYPE LOCAL DEFAULT 11 $x
41: 0000000000000744 0 NOTYPE LOCAL DEFAULT 14 $x
42: 0000000000000000 0 FILE LOCAL DEFAULT ABS crtn.o
43: 0000000000000598 0 NOTYPE LOCAL DEFAULT 11 $x
44: 0000000000000750 0 NOTYPE LOCAL DEFAULT 14 $x
45: 0000000000000000 0 FILE LOCAL DEFAULT ABS crtstuff.c
46: 0000000000000650 0 NOTYPE LOCAL DEFAULT 13 $x
47: 0000000000000650 0 FUNC LOCAL DEFAULT 13 deregister_tm_clones
48: 0000000000000680 0 FUNC LOCAL DEFAULT 13 register_tm_clones
49: 0000000000020008 0 NOTYPE LOCAL DEFAULT 22 $d
50: 00000000000006c0 0 FUNC LOCAL DEFAULT 13 __do_global_dtors_aux
51: 0000000000020010 1 OBJECT LOCAL DEFAULT 23 completed.0
52: 000000000001fd90 0 NOTYPE LOCAL DEFAULT 19 $d
53: 000000000001fd90 0 OBJECT LOCAL DEFAULT 19 __do_global_dtors_aux_fini_array_entry
54: 0000000000000710 0 FUNC LOCAL DEFAULT 13 frame_dummy
55: 000000000001fd88 0 NOTYPE LOCAL DEFAULT 18 $d
56: 000000000001fd88 0 OBJECT LOCAL DEFAULT 18 __frame_dummy_init_array_entry
57: 00000000000007c0 0 NOTYPE LOCAL DEFAULT 17 $d
58: 0000000000020010 0 NOTYPE LOCAL DEFAULT 23 $d
59: 0000000000000000 0 FILE LOCAL DEFAULT ABS example.c
60: 0000000000000714 0 NOTYPE LOCAL DEFAULT 13 $x
61: 0000000000000820 0 NOTYPE LOCAL DEFAULT 17 $d
62: 0000000000000000 0 FILE LOCAL DEFAULT ABS crtstuff.c
63: 0000000000000838 0 NOTYPE LOCAL DEFAULT 17 $d
64: 0000000000000838 0 OBJECT LOCAL DEFAULT 17 __FRAME_END__
65: 0000000000000000 0 FILE LOCAL DEFAULT ABS
66: 000000000001fd98 0 OBJECT LOCAL DEFAULT ABS _DYNAMIC
67: 000000000000075c 0 NOTYPE LOCAL DEFAULT 16 __GNU_EH_FRAME_HDR
68: 000000000001ffd0 0 OBJECT LOCAL DEFAULT ABS _GLOBAL_OFFSET_TABLE_
69: 00000000000005a0 0 NOTYPE LOCAL DEFAULT 12 $x
70: 0000000000000000 0 FUNC GLOBAL DEFAULT UND __libc_start_main@GLIBC_2.34
71: 0000000000000000 0 NOTYPE WEAK DEFAULT UND _ITM_deregisterTMCloneTable
72: 0000000000020000 0 NOTYPE WEAK DEFAULT 22 data_start
73: 0000000000020010 0 NOTYPE GLOBAL DEFAULT 23 __bss_start__
74: 0000000000000000 0 FUNC WEAK DEFAULT UND __cxa_finalize@GLIBC_2.17
75: 0000000000020018 0 NOTYPE GLOBAL DEFAULT 23 _bss_end__
76: 0000000000020010 0 NOTYPE GLOBAL DEFAULT 22 _edata
77: 0000000000000744 0 FUNC GLOBAL HIDDEN 14 _fini
78: 0000000000020018 0 NOTYPE GLOBAL DEFAULT 23 __bss_end__
79: 0000000000020000 0 NOTYPE GLOBAL DEFAULT 22 __data_start
80: 0000000000000000 0 NOTYPE WEAK DEFAULT UND __gmon_start__
81: 0000000000020008 0 OBJECT GLOBAL HIDDEN 22 __dso_handle
82: 0000000000000000 0 FUNC GLOBAL DEFAULT UND abort@GLIBC_2.17
83: 0000000000000758 4 OBJECT GLOBAL DEFAULT 15 _IO_stdin_used
84: 0000000000020018 0 NOTYPE GLOBAL DEFAULT 23 _end
85: 0000000000000600 52 FUNC GLOBAL DEFAULT 13 _start
86: 0000000000020018 0 NOTYPE GLOBAL DEFAULT 23 __end__
87: 0000000000020010 0 NOTYPE GLOBAL DEFAULT 23 __bss_start
88: 0000000000000714 48 FUNC GLOBAL DEFAULT 13 main
89: 0000000000020010 0 OBJECT GLOBAL HIDDEN 22 __TMC_END__
90: 0000000000000000 0 NOTYPE WEAK DEFAULT UND _ITM_registerTMCloneTable
91: 0000000000000588 0 FUNC GLOBAL HIDDEN 11 _init
Loading

0 comments on commit 7a4c3a5

Please sign in to comment.