Support for relocatable files

.gitignore

@@ -9,6 +9,7 @@ src/**/*.ml
 !src/utility.ml
 !src/uint32_wrapper.ml
 !src/uint64_wrapper.ml
+!src/sym_ocaml.ml
 !src/ml_bindings.ml
 !src/byte_sequence_wrapper.ml
 !src/filesystem_wrapper.ml
@@ -30,3 +31,7 @@ src/build_num
 src/build_zarith
 src/_build
 src/byte_sequence_impl.lem
+
+_opam
+
+.vscode

src/abis/aarch64/abi_aarch64_symbolic_relocation.lem

@@ -0,0 +1,182 @@
+open import Missing_pervasives
+open import Error
+open import Maybe
+
+open import Num
+open import Basic_classes
+open import String
+
+open import Elf_types_native_uint
+open import Elf_file
+open import Elf_header
+open import Elf_relocation
+open import Elf_symbolic
+
+open import Abi_aarch64_relocation
+open import Abi_utilities
+open import Abi_symbolic_relocation
+
+type aarch64_relocation_target
+  = Data64
+  | Data32
+  | ADRP
+  | ADD
+  | LDST of int
+  | CALL
+  | CONDBR
+  | B
+
+val abi_aarch64_apply_relocation_symbolic : relocation_spec aarch64_relocation_target
+let abi_aarch64_apply_relocation_symbolic rel_type =
+  (** No width, no calculation *)
+  if rel_type = r_aarch64_none then
+    return Nothing
+  (** No width, no calculation *)
+  else if rel_type = r_aarch64_withdrawn then
+    return Nothing
+  (** Signed 64 bit width, calculation: S + A *)
+  else if rel_type = r_aarch64_abs64 then
+    let result = Plus(Lift S, Lift A) in
+    return (Just
+      <| rel_desc_value = result
+        ; rel_desc_checks = []
+        ; rel_desc_mask = (63, 0)
+        ; rel_desc_target = Data64
+        |>
+    )
+  (** Signed 32 bit width, calculation: S + A *)
+  else if rel_type = r_aarch64_abs32 then
+    let result = Plus(Lift S, Lift A) in
+    return (Just
+      <| rel_desc_value = result
+        ; rel_desc_checks = [Overflow (~(2**31), 2**32)]
+        ; rel_desc_mask = (31, 0)
+        ; rel_desc_target = Data32
+        |>
+    )
+  (** Signed 64 bit width, calculation: S + A - P *)
+  else if rel_type = r_aarch64_prel64 then
+    let result = Minus(Plus(Lift S, Lift A), Lift P) in
+    return (Just
+      <| rel_desc_value = result
+        ; rel_desc_checks = []
+        ; rel_desc_mask = (63, 0)
+        ; rel_desc_target = Data64
+        |>
+    )
+  (** Signed 32 bit width, calculation: S + A - P *)
+  else if rel_type = r_aarch64_prel32 then
+    let result = Minus(Plus(Lift S, Lift A), Lift P) in
+    return (Just
+      <| rel_desc_value = result
+        ; rel_desc_checks = [Overflow (~(2**31), 2**32)]
+        ; rel_desc_mask = (31, 0)
+        ; rel_desc_target = Data32
+        |>
+    )
+  else if rel_type = r_aarch64_adr_prel_pg_hi21 then
+    let result = Minus(Apply(Page, Plus(Lift S, Lift A)), Apply(Page, Lift P)) in
+    return (Just
+      <| rel_desc_value = result
+        ; rel_desc_checks = [Overflow (~(2**32), 2**32)]
+        ; rel_desc_mask = (32, 12)
+        ; rel_desc_target = ADRP
+        |>
+    )
+  else if rel_type = r_aarch64_add_abs_lo12_nc then
+    let result = Plus(Lift S, Lift A) in
+    return (Just
+      <| rel_desc_value = result
+        ; rel_desc_checks = []
+        ; rel_desc_mask = (11, 0)
+        ; rel_desc_target = ADD
+        |>
+    )
+  else if rel_type = r_aarch64_ldst8_abs_lo12_nc then
+    let result = Plus(Lift S, Lift A) in
+    return (Just
+      <| rel_desc_value = result
+        ; rel_desc_checks = []
+        ; rel_desc_mask = (11, 0)
+        ; rel_desc_target = LDST 0
+        |>
+    )
+  else if rel_type = r_aarch64_ldst16_abs_lo12_nc then
+    let result = Plus(Lift S, Lift A) in
+    return (Just
+      <| rel_desc_value = result
+        ; rel_desc_checks = [Alignment 1]
+        ; rel_desc_mask = (11, 1)
+        ; rel_desc_target = LDST 1
+        |>
+    )
+  else if rel_type = r_aarch64_ldst32_abs_lo12_nc then
+    let result = Plus(Lift S, Lift A) in
+    return (Just
+      <| rel_desc_value = result
+        ; rel_desc_checks = [Alignment 2]
+        ; rel_desc_mask = (11, 2)
+        ; rel_desc_target = LDST 2
+        |>
+    )
+  else if rel_type = r_aarch64_ldst64_abs_lo12_nc then
+    let result = Plus(Lift S, Lift A) in
+    return (Just
+      <| rel_desc_value = result
+        ; rel_desc_checks = [Alignment 3]
+        ; rel_desc_mask = (11, 3)
+        ; rel_desc_target = LDST 3
+        |>
+    )
+  else if rel_type = r_aarch64_ldst128_abs_lo12_nc then
+    let result = Plus(Lift S, Lift A) in
+    return (Just
+      <| rel_desc_value = result
+        ; rel_desc_checks = [Alignment 4]
+        ; rel_desc_mask = (11, 4)
+        ; rel_desc_target = LDST 4
+        |>
+    )
+  else if rel_type = r_aarch64_call26 then
+    let result = Minus(Plus(Lift S, Lift A), Lift P) in
+    return (Just
+      <| rel_desc_value = result
+        ; rel_desc_checks = [Overflow (~(2**27), 2**27); Alignment 2]
+        ; rel_desc_mask = (27, 2)
+        ; rel_desc_target = CALL
+        |>
+        )
+  else if rel_type = r_aarch64_condbr19 then
+    let result = Minus(Plus(Lift S, Lift A), Lift P) in
+    return (Just
+      <| rel_desc_value = result
+        ; rel_desc_checks = [Overflow (~(2**20), 2**20); Alignment 2]
+        ; rel_desc_mask = (20, 2)
+        ; rel_desc_target = CONDBR
+        |>
+        )
+  else if rel_type = r_aarch64_jump26 then
+    let result = Minus(Plus(Lift S, Lift A), Lift P) in
+    return (Just
+      <| rel_desc_value = result
+        ; rel_desc_checks = [Overflow (~(2**27), 2**27); Alignment 2]
+        ; rel_desc_mask = (27, 2)
+        ; rel_desc_target = B
+        |>
+        )
+  else
+    fail ("Unsupported AARCH64 relocation type " ^ (string_of_aarch64_relocation_type rel_type))
+
+let aarch64_relocation_target_to_data_target = function
+  | Data32 -> return Elf_symbolic.Data32
+  | Data64 -> return Elf_symbolic.Data64
+  | _ -> fail "Not a data relocation"
+end
+
+let aarch64_relocation_interpreter =
+  abi_relocation_interpreter abi_aarch64_apply_relocation_symbolic
+
+let aarch64_data_relocation_interpreter =
+  relocation_interpreter_map_target
+    aarch64_relocation_interpreter
+    aarch64_relocation_target_to_data_target

src/abis/abi_symbolic_relocation.lem

@@ -0,0 +1,77 @@
+open import Num
+open import Maybe
+open import Bool
+open import Basic_classes
+open import String
+
+open import Error
+
+open import Abi_utilities
+
+open import Elf_types_native_uint
+open import Elf_symbol_table
+open import Elf_symbolic
+open import Elf_relocation
+open import Elf_file
+open import Elf_header
+open import Elf_section_header_table
+open import Elf_interpreted_section
+
+type relocation_param = S | A | P
+
+let rec eval_op_exp s_val a_val p_val op: error symbolic_expression =
+  let f = eval_op_exp s_val a_val p_val in
+  match op with
+    | Lift S -> return s_val
+    | Lift A -> return a_val
+    | Lift P -> return p_val
+    | Plus (x, y) ->
+        f x >>= fun a ->
+        f y >>= fun b ->
+        return (BinOp (a, Add, b))
+    | Minus (x, y) ->
+        f x >>= fun a ->
+        f y >>= fun b ->
+        return (BinOp (a, Sub, b))
+    | Apply(Page, x) ->
+        f x >>= fun a ->
+        return (BinOp (a, And, UnOp (Not, Const 4095 (*0xFFF*))))
+    | _ -> fail "Not supported"
+  end
+
+let eval_relocation s_val a_val p_val desc=
+  eval_op_exp s_val a_val p_val desc.rel_desc_value >>= fun value ->
+  return <| rel_desc_value = value
+          ; rel_desc_checks = desc.rel_desc_checks
+          ; rel_desc_mask = desc.rel_desc_mask
+          ; rel_desc_target = desc.rel_desc_target
+          |>
+
+type relocation_spec 'a = natural -> error (maybe (relocation_description (relocation_operator_expression relocation_param) 'a))
+
+let relocation_spec_map_target f spec rel_type =
+  spec rel_type >>= function
+  | Nothing -> return Nothing
+  | Just desc -> return (Just (relocation_map_target f desc))
+  end
+
+val abi_relocation_interpreter : forall 'a. relocation_spec 'a -> relocation_interpreter 'a
+let abi_relocation_interpreter spec ef symtab sidx rel =
+  if is_elf64_relocatable_file ef.elf64_file_header then
+    section_with_offset ef sidx rel.elf64_ra_offset >>= fun p_val ->
+    let (rel_type, sym) = parse_elf64_relocation_info rel.elf64_ra_info in
+    let a_val = Const (integer_of_elf64_sxword rel.elf64_ra_addend) in
+    let addr = rel.elf64_ra_offset in
+    match symbolic_address_of_symbol ef symtab (natFromNatural sym) with
+      | Just x -> x
+      | Nothing -> fail "Invalid symbol table index"
+    end >>= fun s_val ->
+      spec rel_type >>= function
+      | Nothing -> return Map.empty
+      | Just rel_desc ->
+          eval_relocation s_val a_val p_val rel_desc >>= fun x ->
+          return (Map.singleton addr x)
+      end
+  else
+    fail "abi_relocation_interpreter: not a relocatable file"
+

src/adaptors/harness_interface.lem

@@ -16,6 +16,7 @@ open import Default_printing
 open import Endianness
 open import String_table
 
+open import Abi_utilities
 open import Elf_dynamic
 open import Elf_file
 open import Elf_header
@@ -514,12 +515,13 @@ let {ocaml} harness_string_of_elf64_reloc_a_entry os symtab sht stbl sechdr_stbl
   let off    = natural_of_elf64_addr  rel.elf64_ra_offset in
   let inf    = natural_of_elf64_xword rel.elf64_ra_info in
   let add    = integer_of_elf64_sxword rel.elf64_ra_addend in
-  let typ    = Missing_pervasives.unsafe_string_take 22 (os 0) in (*FIXME *)
+  let (typ, sym) = parse_elf64_relocation_info rel.elf64_ra_info in
+  let typ    = Missing_pervasives.unsafe_string_take 22 (os typ) in
   let typs   =
     let len = naturalFromNat (22 - String.stringLength typ) in
       concatS (replicate len " ")
   in
-  let idx  = 0 in (* FIXME *)
+  let idx  = sym in
   let (nm, value, symtyp, secthdr)  =
     match List.index symtab (unsafe_nat_of_natural idx) with
       | Nothing  -> (stn_undef, 0, 0, 0)