Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Non-deterministic GoTos for indirect call resolution #132

Merged
merged 25 commits into from
Nov 6, 2023
Merged

Non-deterministic GoTos for indirect call resolution #132

Show file tree
Hide file tree
Changes from 18 commits
Commits
Show all changes
25 commits
Select commit Hold shift + click to select a range
9cceafb
Added reassign and stack ptr examples
yousifpatti Sep 26, 2023
21948c4
Adding parent function to CFG statements
yousifpatti Sep 26, 2023
fedb667
Added Stack and Data renaming
yousifpatti Sep 26, 2023
3208cdd
Identifying constant regions
yousifpatti Oct 10, 2023
b1f3d15
Merge branch 'analysis-devel' into yousif-memory-region-analysis
yousifpatti Oct 10, 2023
1aad929
Fixes to merge comments
yousifpatti Oct 10, 2023
f48395a
Merge branch 'main' into yousif-memory-region-analysis
yousifpatti Oct 17, 2023
c9f37e3
Fixed merge issues
yousifpatti Oct 17, 2023
9610dea
add non-deterministic goto to IR, use it when indirect calls have mul…
Oct 30, 2023
3a6a93f
Merge branch 'main' into indirect-calls-nondet
Oct 30, 2023
42b2973
printer for analysis results that is ok and much more readable than t…
Oct 30, 2023
185ed71
clean up MRA/VSA a bit
Oct 30, 2023
d9c5e39
minor VSA improvement
Oct 31, 2023
d21425b
syntax cleanup
Oct 31, 2023
595c284
more type cleanup
Oct 31, 2023
d1de241
improve analysis printer
Oct 31, 2023
936596a
add *.txt and *.csv to gitignore
Oct 31, 2023
4e0ced0
Merge branch 'main' into indirect-calls-nondet
Nov 1, 2023
0f15ae5
add back dot output and wrap bubble labels
ailrst Nov 2, 2023
e1a5022
fix memory region equals/hashcode
Nov 2, 2023
cc08880
remove conditions from calls since they should not appear in the ARM6…
Nov 2, 2023
2a5fd77
Merge branch 'main' into indirect-calls-nondet
Nov 2, 2023
9be3c66
Merge remote-tracking branch 'origin/indirect-calls-nondet' into indi…
Nov 2, 2023
99b9bd8
add flags for printing analysis results, make it so separate results …
Nov 2, 2023
fb919aa
fix noted issues
Nov 6, 2023
File filter

Filter by extension

Filter by extension
Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
5 changes: 1 addition & 4 deletions .gitignore
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -8,17 +8,14 @@
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
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
View file
Open in desktop

Large diffs are not rendered by default.

234 changes: 234 additions & 0 deletions examples/basic_local_reassign/basic_local_reassign.bir
View file
Open in desktop
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
View file
Open in desktop
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
View file
Open in desktop
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