mirror of
https://github.com/GaloisInc/macaw.git
synced 2024-12-28 08:34:23 +03:00
Bump submodules
This commit is contained in:
Joe Hendrix
parent
230b318dcf
commit
64d71737af
@ -2,8 +2,8 @@
|
||||
Copyright : (c) Galois, Inc 2017
|
||||
Maintainer : Joe Hendrix <jhendrix@galois.com>
|
||||
|
||||
This exports the "simplifiable CFG" interface. A CFG designed for
|
||||
optimization.
|
||||
This exports the "simplifiable CFG" interface. This CFG is designed
|
||||
for simple optimizations including mem2reg
|
||||
-}
|
||||
{-# LANGUAGE DataKinds #-}
|
||||
{-# LANGUAGE GADTs #-}
|
||||
@ -22,6 +22,459 @@ module Data.Macaw.SCFG
|
||||
, module Data.Macaw.CFG.App
|
||||
) where
|
||||
|
||||
{-
|
||||
Concepts:
|
||||
|
||||
initial(r): This denotes the value in r when the function is called.
|
||||
|
||||
|
||||
How will the algorithm work?
|
||||
|
||||
Example, suppose we have the following program:
|
||||
|
||||
simple.c:
|
||||
int add(int x, int y) {
|
||||
return x+y;
|
||||
}
|
||||
|
||||
|
||||
gcc -c -o simple.o simple.c
|
||||
ubuntu64:~% gobjdump -d simple.c
|
||||
|
||||
|
||||
Then we run the following to get the disassembly:
|
||||
|
||||
> gcc -c -o simple.o simple.c && objdump -d simple.o
|
||||
|
||||
0000000000000000 <add>:
|
||||
0: 55 push %rbp
|
||||
1: 48 89 e5 mov %rsp,%rbp
|
||||
4: 89 7d fc mov %edi,-0x4(%rbp)
|
||||
7: 89 75 f8 mov %esi,-0x8(%rbp)
|
||||
a: 8b 55 fc mov -0x4(%rbp),%edx
|
||||
d: 8b 45 f8 mov -0x8(%rbp),%eax
|
||||
10: 01 d0 add %edx,%eax
|
||||
12: 5d pop %rbp
|
||||
13: c3 retq
|
||||
|
||||
// Reopt outputs the following:
|
||||
|
||||
function add @ segment1+0x0
|
||||
segment1+0x0:
|
||||
# segment1+0x0: push rbp
|
||||
r23 := (bv_add rsp_0 (0xfffffffffffffff8 :: [64]))
|
||||
write_mem r23 rbp_0
|
||||
# segment1+0x1: mov rbp,rsp
|
||||
# segment1+0x4: mov DWORD PTR [rbp-0x4],edi
|
||||
r24 := (trunc rdi_0 32)
|
||||
r25 := (bv_add rsp_0 (0xfffffffffffffff4 :: [64]))
|
||||
write_mem r25 r24
|
||||
# segment1+0x7: mov DWORD PTR [rbp-0x8],esi
|
||||
r26 := (trunc rsi_0 32)
|
||||
r27 := (bv_add rsp_0 (0xfffffffffffffff0 :: [64]))
|
||||
write_mem r27 r26
|
||||
# segment1+0xa: mov edx,DWORD PTR [rbp-0x4]
|
||||
r28 := read_mem r25 (bvle 4)
|
||||
r29 := (uext r28 64)
|
||||
# segment1+0xd: mov eax,DWORD PTR [rbp-0x8]
|
||||
r30 := read_mem r27 (bvle 4)
|
||||
# segment1+0x10: add eax,edx
|
||||
r32 := (sadc_overflows r30 r28 false)
|
||||
r33 := (trunc r30 4)
|
||||
r34 := (trunc r28 4)
|
||||
r35 := (uadc_overflows r33 r34 false)
|
||||
r36 := (uadc_overflows r30 r28 false)
|
||||
r37 := (bv_add r30 r28)
|
||||
r38 := (bv_slt r37 (0x0 :: [32]))
|
||||
r39 := (eq r37 (0x0 :: [32]))
|
||||
r40 := (trunc r37 8)
|
||||
r41 := (even_parity r40)
|
||||
r42 := (uext r37 64)
|
||||
# segment1+0x12: pop rbp
|
||||
r43 := read_mem r23 (bvle 8)
|
||||
# segment1+0x13: ret
|
||||
r44 := read_mem rsp_0 (bvle 8)
|
||||
r45 := (bv_add rsp_0 (0x8 :: [64]))
|
||||
return
|
||||
{ rip = r44
|
||||
, rax = r42
|
||||
, rdx = r29
|
||||
, rsp = r45
|
||||
, rbp = r43
|
||||
, cf = r36
|
||||
, pf = r41
|
||||
, af = r35
|
||||
, zf = r39
|
||||
, sf = r38
|
||||
, of = r32
|
||||
}
|
||||
|
||||
We would like the following:
|
||||
|
||||
````
|
||||
function add @ segment1+0x0
|
||||
|
||||
Calling convention:
|
||||
stack grows down
|
||||
top of stack: rsp;
|
||||
|
||||
dont care about writes in range [rsp-16..rsp].
|
||||
|
||||
return_addr: *rsp;
|
||||
final(ip) = read(initial_memory, rsp);
|
||||
final(rsp) = initial(rsp)+8;
|
||||
final(rbp) = initial(rbp);
|
||||
|
||||
segment1+0x0:
|
||||
r28 := (trunc rdi_0 32)
|
||||
r30 := (trunc rsi_0 32)
|
||||
r37 := (bv_add r30 r28)
|
||||
return
|
||||
{ rax = (uext r37 64)
|
||||
, rdx = (uext r28 64)
|
||||
, af = (uadc_overflows (trunc r30 4) (trunc r28 4) false)
|
||||
, cf = (uadc_overflows r30 r28 false)
|
||||
, of = (sadc_overflows r30 r28 false)
|
||||
, pf = (even_parity (trunc r37 8))
|
||||
, zf = (eq r37 (0x0 :: [32]))
|
||||
, sf = (bv_slt r37 (0x0 :: [32]))
|
||||
}
|
||||
|
||||
Mask example
|
||||
======
|
||||
|
||||
|
||||
long mask(long c, long* a, long v) {
|
||||
long r = 0;
|
||||
for (long i = 0; i != c; ++c) {
|
||||
if (a[i] == v) {
|
||||
r = 2*r + 1;
|
||||
} else {
|
||||
r = 2*r;
|
||||
}
|
||||
}
|
||||
return r;
|
||||
}
|
||||
|
||||
> gcc -c -o mask.o mask.c && objdump -d mask.o
|
||||
|
||||
|
||||
0000000000000014 <mask>:
|
||||
14: 55 push %rbp
|
||||
15: 48 89 e5 mov %rsp,%rbp
|
||||
18: 48 89 7d e8 mov %rdi,-0x18(%rbp)
|
||||
1c: 48 89 75 e0 mov %rsi,-0x20(%rbp)
|
||||
20: 48 89 55 d8 mov %rdx,-0x28(%rbp)
|
||||
24: 48 c7 45 f0 00 00 00 movq $0x0,-0x10(%rbp)
|
||||
2b: 00
|
||||
2c: 48 c7 45 f8 00 00 00 movq $0x0,-0x8(%rbp)
|
||||
33: 00
|
||||
34: eb 36 jmp 6c <mask+0x58>
|
||||
36: 48 8b 45 f8 mov -0x8(%rbp),%rax
|
||||
3a: 48 8d 14 c5 00 00 00 lea 0x0(,%rax,8),%rdx
|
||||
41: 00
|
||||
42: 48 8b 45 e0 mov -0x20(%rbp),%rax
|
||||
46: 48 01 d0 add %rdx,%rax
|
||||
49: 48 8b 00 mov (%rax),%rax
|
||||
4c: 48 3b 45 d8 cmp -0x28(%rbp),%rax
|
||||
50: 75 11 jne 63 <mask+0x4f>
|
||||
52: 48 8b 45 f0 mov -0x10(%rbp),%rax
|
||||
56: 48 01 c0 add %rax,%rax
|
||||
59: 48 83 c0 01 add $0x1,%rax
|
||||
5d: 48 89 45 f0 mov %rax,-0x10(%rbp)
|
||||
61: eb 04 jmp 67 <mask+0x53>
|
||||
63: 48 d1 65 f0 shlq -0x10(%rbp)
|
||||
67: 48 83 45 e8 01 addq $0x1,-0x18(%rbp)
|
||||
6c: 48 8b 45 f8 mov -0x8(%rbp),%rax
|
||||
70: 48 3b 45 e8 cmp -0x18(%rbp),%rax
|
||||
74: 75 c0 jne 36 <mask+0x22>
|
||||
76: 48 8b 45 f0 mov -0x10(%rbp),%rax
|
||||
7a: 5d pop %rbp
|
||||
7b: c3 retq
|
||||
|
||||
|
||||
function mask @ segment1+0x14
|
||||
segment1+0x14:
|
||||
# Predecessors = []
|
||||
r6 := (bv_add rsp_0 (0xfffffffffffffff8 :: [64]))
|
||||
r7 := (bv_add rsp_0 (0xffffffffffffffe0 :: [64]))
|
||||
r8 := (bv_add rsp_0 (0xffffffffffffffd8 :: [64]))
|
||||
r9 := (bv_add rsp_0 (0xffffffffffffffd0 :: [64]))
|
||||
r10 := (bv_add rsp_0 (0xffffffffffffffe8 :: [64]))
|
||||
r11 := (bv_add rsp_0 (0xfffffffffffffff0 :: [64]))
|
||||
write_mem r6 rbp_0
|
||||
write_mem r7 rdi_0
|
||||
write_mem r8 rsi_0
|
||||
write_mem r9 rdx_0
|
||||
write_mem r10 0x0 :: [64]
|
||||
write_mem r11 0x0 :: [64]
|
||||
jump segment1+0x6c
|
||||
{ rip = segment1+0x6c
|
||||
, rsp = r6
|
||||
, rbp = r6
|
||||
, df = false
|
||||
, x87top = 0x7 :: [3]
|
||||
}
|
||||
segment1+0x36:
|
||||
# Dominators: 0x6c
|
||||
|
||||
#Predecessors = [0x6c]
|
||||
rbp_0 = phi [(0x14, rbp_0)]
|
||||
rsp_0 = phi [(0x14, rsp_0)]
|
||||
|
||||
r662 := read_mem (rbp_0 - 8) (bvle 8)
|
||||
r665 := read_mem (rbp_0 - 0x20) (bvle 8)
|
||||
r678 := read_mem (rbp_0 - 0x28) (bvle 8)
|
||||
|
||||
r663 := (bv_mul (0x8 :: [64]) r662)
|
||||
r671 := (bv_add r665 r663)
|
||||
r676 := read_mem r671 (bvle 8)
|
||||
r679 := (ssbb_overflows r676 r678 false)
|
||||
r680 := (trunc r676 4)
|
||||
r681 := (trunc r678 4)
|
||||
r682 := (bv_ult r680 r681)
|
||||
r683 := (bv_ult r676 r678)
|
||||
r684 := (bv_sub r676 r678)
|
||||
r685 := (bv_slt r684 (0x0 :: [64]))
|
||||
r686 := (eq r676 r678)
|
||||
r687 := (trunc r684 8)
|
||||
r688 := (even_parity r687)
|
||||
# segment1+0x50: jne 50+11
|
||||
r689 := (mux r686 (segment1+0x52) (segment1+0x63))
|
||||
ite r686
|
||||
{
|
||||
|
||||
jump segment1+0x52
|
||||
{ rip = segment1+0x52
|
||||
, rax = r676
|
||||
, rdx = r663
|
||||
, cf = r683
|
||||
, pf = r688
|
||||
, af = r682
|
||||
, zf = r686
|
||||
, sf = r685
|
||||
, df = false
|
||||
, of = r679
|
||||
, x87top = 0x7 :: [3]
|
||||
}
|
||||
}
|
||||
{
|
||||
|
||||
jump segment1+0x63
|
||||
{ rip = segment1+0x63
|
||||
, rax = r676
|
||||
, rdx = r663
|
||||
, cf = r683
|
||||
, pf = r688
|
||||
, af = r682
|
||||
, zf = r686
|
||||
, sf = r685
|
||||
, df = false
|
||||
, of = r679
|
||||
, x87top = 0x7 :: [3]
|
||||
}
|
||||
}
|
||||
segment1+0x52:
|
||||
# Predecessors 0x36
|
||||
rbp_0 = phi [(0x36, rbp_0)]
|
||||
rsp_0 = phi [(0x36, rsp_0)]
|
||||
|
||||
# segment1+0x52: mov rax,QWORD PTR [rbp-0x10]
|
||||
r711 := read_mem (rbp_0 - 16) (bvle 8)
|
||||
# segment1+0x56: add rax,rax
|
||||
r716 := (bv_add r711 r711)
|
||||
# segment1+0x59: add rax,0x1
|
||||
r721 := (sadc_overflows r716 (0x1 :: [64]) false)
|
||||
r722 := (trunc r716 4)
|
||||
r723 := (uadc_overflows r722 (0x1 :: [4]) false)
|
||||
r724 := (uadc_overflows r716 (0x1 :: [64]) false)
|
||||
r725 := (bv_add r716 (0x1 :: [64]))
|
||||
r726 := (bv_slt r725 (0x0 :: [64]))
|
||||
r727 := (eq r716 (0xffffffffffffffff :: [64]))
|
||||
r728 := (trunc r725 8)
|
||||
r729 := (even_parity r728)
|
||||
# segment1+0x5d: mov QWORD PTR [rbp-0x10],rax
|
||||
write_mem (rbp_0 - 0x10) r725
|
||||
# segment1+0x61: jmp 61+4
|
||||
jump segment1+0x67
|
||||
{ rip = segment1+0x67
|
||||
, rax = r725
|
||||
, cf = r724
|
||||
, pf = r729
|
||||
, af = r723
|
||||
, zf = r727
|
||||
, sf = r726
|
||||
, df = false
|
||||
, of = r721
|
||||
, x87top = 0x7 :: [3]
|
||||
}
|
||||
segment1+0x63:
|
||||
# Predecessors 0x36
|
||||
rbp_0 = phi [(0x14, rbp_0)]
|
||||
rsp_0 = phi [(0x14, rsp_0)]
|
||||
|
||||
# segment1+0x63: shl QWORD PTR [rbp-0x10],1
|
||||
r743 := read_mem (rbp_0 - 0x10) (bvle 8)
|
||||
r744 := undef :: [bool]
|
||||
r746 := (bv_slt r743 (0x0 :: [64]))
|
||||
r747 := (bv_slt r743 (0x0 :: [64]))
|
||||
r748 := (bv_shl r743 (0x1 :: [64]))
|
||||
r749 := (bv_slt r748 (0x0 :: [64]))
|
||||
r750 := (eq r748 (0x0 :: [64]))
|
||||
r751 := (trunc r748 8)
|
||||
r752 := (even_parity r751)
|
||||
write_mem (rbp_0 - 0x10) r748
|
||||
jump segment1+0x67
|
||||
{ rip = segment1+0x67
|
||||
, cf = r747
|
||||
, pf = r752
|
||||
, af = r744
|
||||
, zf = r750
|
||||
, sf = r749
|
||||
, df = false
|
||||
, of = r746
|
||||
, x87top = 0x7 :: [3]
|
||||
}
|
||||
segment1+0x67:
|
||||
# Predecessors 0x52, 0x63
|
||||
rbp_0 = phi [(0x14, rbp_0)]
|
||||
rsp_0 = phi [(0x14, rsp_0)]
|
||||
|
||||
# segment1+0x67: add QWORD PTR [rbp-0x18],0x1
|
||||
r591 := (bv_add rbp_0 (0xffffffffffffffe8 :: [64]))
|
||||
r592 := read_mem r591 (bvle 8)
|
||||
r593 := (sadc_overflows r592 (0x1 :: [64]) false)
|
||||
r594 := (trunc r592 4)
|
||||
r595 := (uadc_overflows r594 (0x1 :: [4]) false)
|
||||
r596 := (uadc_overflows r592 (0x1 :: [64]) false)
|
||||
r597 := (bv_add r592 (0x1 :: [64]))
|
||||
r598 := (bv_slt r597 (0x0 :: [64]))
|
||||
r599 := (eq r592 (0xffffffffffffffff :: [64]))
|
||||
r600 := (trunc r597 8)
|
||||
r601 := (even_parity r600)
|
||||
write_mem r591 r597
|
||||
jump segment1+0x6c
|
||||
{ rip = segment1+0x6c
|
||||
, cf = r596
|
||||
, pf = r601
|
||||
, af = r595
|
||||
, zf = r599
|
||||
, sf = r598
|
||||
, df = false
|
||||
, of = r593
|
||||
, x87top = 0x7 :: [3]
|
||||
}
|
||||
segment1+0x6c:
|
||||
# Predecessors 0x14 0x67
|
||||
rbp_0 = phi [(0x14, (rsp_0 - 8))]
|
||||
rsp_0 = phi [(0x14, (rsp_0 - 8))]
|
||||
|
||||
|
||||
r618 := read_mem (rbp_0 - 8) (bvle 8)
|
||||
r620 := read_mem (rbp_0 - 0x18) (bvle 8)
|
||||
r621 := (ssbb_overflows r618 r620 false)
|
||||
r622 := (trunc r618 4)
|
||||
r623 := (trunc r620 4)
|
||||
r624 := (bv_ult r622 r623)
|
||||
r625 := (bv_ult r618 r620)
|
||||
r626 := (bv_sub r618 r620)
|
||||
r627 := (bv_slt r626 (0x0 :: [64]))
|
||||
r628 := (eq r618 r620)
|
||||
r629 := (trunc r626 8)
|
||||
r630 := (even_parity r629)
|
||||
# segment1+0x74: jne 74+-40
|
||||
r631 := (mux r628 (segment1+0x76) (segment1+0x36))
|
||||
ite r628
|
||||
{
|
||||
|
||||
jump segment1+0x76
|
||||
{ rip = segment1+0x76
|
||||
, rax = r618
|
||||
, cf = r625
|
||||
, pf = r630
|
||||
, af = r624
|
||||
, zf = r628
|
||||
, sf = r627
|
||||
, df = false
|
||||
, of = r621
|
||||
, x87top = 0x7 :: [3]
|
||||
}
|
||||
}
|
||||
{
|
||||
|
||||
jump segment1+0x36
|
||||
{ rip = segment1+0x36
|
||||
, rax = r618
|
||||
, cf = r625
|
||||
, pf = r630
|
||||
, af = r624
|
||||
, zf = r628
|
||||
, sf = r627
|
||||
, df = false
|
||||
, of = r621
|
||||
, x87top = 0x7 :: [3]
|
||||
}
|
||||
}
|
||||
segment1+0x76:
|
||||
# Predecessors 0x6c
|
||||
rbp_0 = phi [(0x14, (initial(rsp) - 8)]
|
||||
rsp_0 = phi [(0x14, (initial(rsp) - 8)]
|
||||
# Detect *(0x14, rsp_0) = return_addr
|
||||
|
||||
|
||||
r761 := read_mem (initial(rsp) - 0x18) (bvle 8)
|
||||
r762 := read_mem rsp_0 (bvle 8)
|
||||
r764 := read_mem (rsp_0 + 8) (bvle 8)
|
||||
return
|
||||
{ rip = r764
|
||||
, rax = r761
|
||||
, rsp = initial(rsp) + 0x8
|
||||
, rbp = r762
|
||||
, df = false
|
||||
, x87top = 0x7 :: [3]
|
||||
}
|
||||
|
||||
0x14 -> 0x6c
|
||||
0x6c -> 0x76 | 0x36
|
||||
0x76 -> return
|
||||
0x36 -> 0x52 | 0x63
|
||||
0x52 -> 0x67
|
||||
0x63 -> 0x67
|
||||
0x67 -> 0x6c
|
||||
|
||||
|
||||
0x14 -> 0x6c -> (0x36 -> (0x52|0x63|0x67))
|
||||
-> 0x76
|
||||
|
||||
|
||||
|
||||
|
||||
0x6c -> 0x36
|
||||
0x36 -> 0x52 | 0x63
|
||||
|
||||
========================================================================
|
||||
== Implementation
|
||||
|
||||
|
||||
First goal:
|
||||
- Generate a ordering over the functions:
|
||||
|
||||
- f <= g if call @g appears inside a block of f.
|
||||
- f <= g if there exists an h such that call g(f, ...)
|
||||
|
||||
|
||||
Stack:
|
||||
|
||||
Partial map from index to (BlockId,StmtIndex,Value) tuples.
|
||||
|
||||
Concepts
|
||||
|
||||
|
||||
Build a dominator tree
|
||||
|
||||
-}
|
||||
|
||||
|
||||
import Data.Macaw.CFG.AssignRhs
|
||||
import Data.Macaw.CFG.App
|
||||
import Data.Macaw.Memory (AddrWidthRepr(..))
|
||||
|
||||
2
deps/flexdis86
vendored
2
deps/flexdis86
vendored
@ -1 +1 @@
|
||||
Subproject commit 9304269acef1c82e9ae3676649574e371ac54c36
|
||||
Subproject commit 71c367e2269f84dcdfda21612288109312ba3fc6
|
||||
Loading…
Reference in New Issue
Block a user