Skip to content

Commit a504bb9

Browse files
maturvomaturvo
authored
Merge pull request #1 from maturvo/extract-relocations2
Symbolic relocation-aware DWARF
2 parents 238f803 + 6d307ef commit a504bb9

File tree

9 files changed

+1261
-566
lines changed

9 files changed

+1261
-566
lines changed

‎.gitignore‎

Lines changed: 2 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -30,3 +30,5 @@ src/build_num
3030
src/build_zarith
3131
src/_build
3232
src/byte_sequence_impl.lem
33+
34+
_opam

‎src/abis/aarch64/abi_aarch64_symbolic_relocation.lem‎

Lines changed: 145 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,145 @@
1+
open import Missing_pervasives
2+
open import Error
3+
open import Maybe
4+
5+
open import Num
6+
open import Basic_classes
7+
8+
open import Elf_types_native_uint
9+
open import Elf_file
10+
open import Elf_header
11+
open import Elf_relocation
12+
open import Elf_symbolic
13+
14+
open import Abi_aarch64_relocation
15+
open import Abi_utilities
16+
open import Abi_symbolic_relocation
17+
18+
type aarch64_relocation_target
19+
= Data64
20+
| Data32
21+
| ADRP
22+
| ADD
23+
| LDST
24+
| CALL
25+
26+
(* TODO fix sizes and stuff *)
27+
val abi_aarch64_apply_relocation_symbolic :
28+
elf64_relocation_a -> symbolic_expression -> symbolic_expression -> elf64_file ->
29+
error (Map.map elf64_addr (relocation_description symbolic_expression aarch64_relocation_target))
30+
let abi_aarch64_apply_relocation_symbolic rel s_val p_val ef =
31+
if is_elf64_relocatable_file ef.elf64_file_header then
32+
let (rel_type, _) = parse_elf64_relocation_info rel.elf64_ra_info in
33+
let a_val = Const (integer_of_elf64_sxword rel.elf64_ra_addend) in
34+
(** No width, no calculation *)
35+
if rel_type = r_aarch64_none then
36+
return Map.empty
37+
(** No width, no calculation *)
38+
else if rel_type = r_aarch64_withdrawn then
39+
return Map.empty
40+
(** Signed 64 bit width, calculation: S + A *)
41+
else if rel_type = r_aarch64_abs64 then
42+
let result = Plus(Lift s_val, Lift a_val) in
43+
let addr = rel.elf64_ra_offset in
44+
return (Map.singleton addr
45+
<| rel_desc_operation = (result, I64, CannotFail)
46+
; rel_desc_mask = (63, 0)
47+
; rel_desc_target = Data64
48+
|>
49+
)
50+
(** Signed 32 bit width, calculation: S + A *)
51+
else if rel_type = r_aarch64_abs32 then
52+
let result = Plus(Lift s_val, Lift a_val) in
53+
let addr = rel.elf64_ra_offset in
54+
return (Map.singleton addr
55+
<| rel_desc_operation = (result, I32, CanFail)
56+
; rel_desc_mask = (31, 0)
57+
; rel_desc_target = Data32
58+
|>
59+
)
60+
(** Signed 64 bit width, calculation: S + A - P *)
61+
else if rel_type = r_aarch64_prel64 then
62+
let result = Minus(Plus(Lift s_val, Lift a_val), Lift p_val) in
63+
let addr = rel.elf64_ra_offset in
64+
return (Map.singleton addr
65+
<| rel_desc_operation = (result, I64, CannotFail)
66+
; rel_desc_mask = (63, 0)
67+
; rel_desc_target = Data64
68+
|>
69+
)
70+
(** Signed 32 bit width, calculation: S + A - P *)
71+
else if rel_type = r_aarch64_prel32 then
72+
let result = Minus(Plus(Lift s_val, Lift a_val), Lift p_val) in
73+
let addr = rel.elf64_ra_offset in
74+
return (Map.singleton addr
75+
<| rel_desc_operation = (result, I32, CanFail)
76+
; rel_desc_mask = (31, 0)
77+
; rel_desc_target = Data32
78+
|>
79+
)
80+
else if rel_type = r_aarch64_adr_prel_pg_hi21 then
81+
let result = Minus(Apply(Page, Plus(Lift s_val, Lift a_val)), Apply(Page, Lift p_val)) in
82+
let addr = rel.elf64_ra_offset in
83+
return (Map.singleton addr
84+
<| rel_desc_operation = (result, I32, CanFail)
85+
; rel_desc_mask = (32, 12)
86+
; rel_desc_target = ADRP
87+
|>
88+
)
89+
else if rel_type = r_aarch64_add_abs_lo12_nc then
90+
let result = Plus(Lift s_val, Lift a_val) in
91+
let addr = rel.elf64_ra_offset in
92+
return (Map.singleton addr
93+
<| rel_desc_operation = (result, I32, CannotFail)
94+
; rel_desc_mask = (11, 0)
95+
; rel_desc_target = ADD
96+
|>
97+
)
98+
else if rel_type = r_aarch64_ldst32_abs_lo12_nc then
99+
let result = Plus(Lift s_val, Lift a_val) in
100+
let addr = rel.elf64_ra_offset in
101+
return (Map.singleton addr
102+
<| rel_desc_operation = (result, I32, CannotFail)
103+
; rel_desc_mask = (11, 2)
104+
; rel_desc_target = LDST
105+
|>
106+
)
107+
else if rel_type = r_aarch64_ldst64_abs_lo12_nc then
108+
let result = Plus(Lift s_val, Lift a_val) in
109+
let addr = rel.elf64_ra_offset in
110+
return (Map.singleton addr
111+
<| rel_desc_operation = (result, I32, CannotFail)
112+
; rel_desc_mask = (11, 3)
113+
; rel_desc_target = LDST
114+
|>
115+
)
116+
else if rel_type = r_aarch64_call26 then
117+
let result = Minus(Plus(Lift s_val, Lift a_val), Lift p_val) in
118+
let addr = rel.elf64_ra_offset in
119+
return (Map.singleton addr
120+
<| rel_desc_operation = (result, I27, CanFail)
121+
; rel_desc_mask = (27, 2)
122+
; rel_desc_target = CALL
123+
|>
124+
)
125+
else
126+
fail "Invalid AARCH64 relocation type"
127+
else
128+
fail "abi_aarch64_apply_relocation: not a relocatable file"
129+
130+
val abi_aarch64_relocation_to_abstract : relocation_interpreter aarch64_relocation_target
131+
let abi_aarch64_relocation_to_abstract ef symtab_map sidx rel =
132+
section_with_offset ef sidx rel.elf64_ra_offset >>= fun p_val ->
133+
let (_, sym) = parse_elf64_relocation_info rel.elf64_ra_info in
134+
match Map.lookup sym symtab_map with
135+
| Just ste -> symbolic_address_from_elf64_symbol_table_entry ef ste
136+
| Nothing -> fail "Invalid symbol table index"
137+
end >>= fun s_val ->
138+
abi_aarch64_apply_relocation_symbolic rel s_val p_val ef >>= fun rel_desc_map ->
139+
map_mapM eval_relocation rel_desc_map
140+
141+
let aarch64_relocation_target_to_data_target = function
142+
| Data32 -> return Elf_symbolic.Data32
143+
| Data64 -> return Elf_symbolic.Data64
144+
| _ -> fail "Not a data relocation"
145+
end

‎src/abis/abi_symbolic_relocation.lem‎

Lines changed: 47 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,47 @@
1+
open import Num
2+
3+
open import Error
4+
5+
open import Abi_utilities
6+
7+
open import Elf_types_native_uint
8+
open import Elf_symbol_table
9+
open import Elf_symbolic
10+
11+
12+
type relocation_description 'res 'tar =
13+
<| rel_desc_operation : (relocation_operator_expression 'res * integer_bit_width * can_fail 'res)
14+
; rel_desc_mask : (natural * natural)
15+
; rel_desc_target : 'tar
16+
|>
17+
18+
19+
20+
let rec eval_op_exp op: error symbolic_expression =
21+
match op with
22+
| Lift x -> return x
23+
| Plus (x, y) ->
24+
eval_op_exp x >>= fun a ->
25+
eval_op_exp y >>= fun b ->
26+
return (BinOp (a, Add, b))
27+
| Minus (x, y) ->
28+
eval_op_exp x >>= fun a ->
29+
eval_op_exp y >>= fun b ->
30+
return (BinOp (a, Sub, b))
31+
| _ -> fail "Not supported"
32+
end
33+
34+
35+
let eval_relocation desc =
36+
let (exp, bit_width, can_fail) = desc.rel_desc_operation in
37+
let (lo, hi) = desc.rel_desc_mask in
38+
39+
eval_op_exp exp >>= fun value ->
40+
match can_fail with
41+
| CanFail -> return (AssertRange(value, 0, 0)) (*todo*)
42+
| CannotFail -> return value
43+
| CanFailOnTest -> fail "Not supported"
44+
end
45+
>>= fun value ->
46+
return <| arel_value = Mask(value, lo, hi) ; arel_target = desc.rel_desc_target |>
47+

‎src/adaptors/harness_interface.lem‎

Lines changed: 4 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -16,6 +16,7 @@ open import Default_printing
1616
open import Endianness
1717
open import String_table
1818

19+
open import Abi_utilities
1920
open import Elf_dynamic
2021
open import Elf_file
2122
open import Elf_header
@@ -514,12 +515,13 @@ let {ocaml} harness_string_of_elf64_reloc_a_entry os symtab sht stbl sechdr_stbl
514515
let off = natural_of_elf64_addr rel.elf64_ra_offset in
515516
let inf = natural_of_elf64_xword rel.elf64_ra_info in
516517
let add = integer_of_elf64_sxword rel.elf64_ra_addend in
517-
let typ = Missing_pervasives.unsafe_string_take 22 (os 0) in (*FIXME *)
518+
let (typ, sym) = parse_elf64_relocation_info rel.elf64_ra_info in
519+
let typ = Missing_pervasives.unsafe_string_take 22 (os typ) in
518520
let typs =
519521
let len = naturalFromNat (22 - String.stringLength typ) in
520522
concatS (replicate len " ")
521523
in
522-
let idx = 0 in (* FIXME *)
524+
let idx = sym in
523525
let (nm, value, symtyp, secthdr) =
524526
match List.index symtab (unsafe_nat_of_natural idx) with
525527
| Nothing -> (stn_undef, 0, 0, 0)

0 commit comments

Comments
 (0)