Reloc.lean🔗

Declarations on this page (35)

AArch64 ELF Relocations and Immediate Range Helpers

Static AArch64 ELF relocation classes (RelocKind), relocation entries (RelocEntry), link-independent code and data symbol records (SymCodeInfo, SymDataInfo), little-endian byte/word helpers, and instruction-word patchers with immediate range and alignment predicates.

@[expose] public section

namespace Arm64.Obj

Little-endian byte, page, and association-list helpers

def pageSizeL26–27 ↗#

Page size (4096 bytes on AArch64).

def pageSize : Nat := 4096

def bytesLEL29–31 ↗#

Little-endian bytes of a 64-bit value.

def bytesLE (n : Nat) (v : BitVec 64) : List (BitVec 8) :=
  (List.range n).map fun i => v.extractLsb' (8 * i) 8

def pageOfL33–34 ↗#

Page address (x & ~0xfff), clearing the low 12 bits.

def pageOf (x : BitVec 64) : BitVec 64 := x &&& 0xfffffffffffff000#64

1 declaration not shown (lines 36–37): theorems, which Lean checks, or definitions that no headline statement uses

Arm64.Obj.lo12Of

def wordOfBytesLEL39–45 ↗#

Read a 32-bit little-endian word from xs at byte offset off (0-padded if out of bounds).

def wordOfBytesLE (xs : List (BitVec 8)) (off : Nat) : BitVec 32 :=
  let b0 := (xs.getD off 0#8).zeroExtend 32
  let b1 := (xs.getD (off + 1) 0#8).zeroExtend 32 <<< 8
  let b2 := (xs.getD (off + 2) 0#8).zeroExtend 32 <<< 16
  let b3 := (xs.getD (off + 3) 0#8).zeroExtend 32 <<< 24
  b0 ||| b1 ||| b2 ||| b3

def bytesOfWordLEL47–49 ↗#

4-byte little-endian encoding of a 32-bit word w.

def bytesOfWordLE (w : BitVec 32) : List (BitVec 8) :=
  bytesLE 4 (w.zeroExtend 64)

def lookupL51–53 ↗#

Look up name in an association list (first occurrence).

def lookup {α} (name : String) (xs : List (String × α)) : Option α :=
  (xs.find? (·.1 == name)).map (·.2)

def lookupUniqueL55–59 ↗#

Unique-occurrence lookup (some v iff name appears in xs exactly once).

def lookupUnique {α} (name : String) (xs : List (String × α)) : Option α :=
  match xs.filter (·.1 == name) with
  | [(_, v)] => some v
  | _ => none

1 declaration not shown (lines 61–63): theorems, which Lean checks, or definitions that no headline statement uses

Arm64.Obj.bytesAt

Relocation classes and symbol records

inductive RelocKindL67–106 ↗#

AArch64 ELF static relocation classes supported by layout-generic objects.

inductive RelocKind where
  | call26
  | jump26
  | adrpHi21
  | adrpHi21Nc
  | addLo12
  | ldst8Lo12
  | ldst16Lo12
  | ldst32Lo12
  | ldst64Lo12
  | ldst128Lo12
  | condbr19
  | tstbr14
  | ldPrelLo19
  | adrPrelLo21
  | prel32
  | abs64
  | abs32
  | adrGotPage
  | ld64GotLo12Nc
  | tlsieAdrGottprelPage21
  | tlsieLd64GottprelLo12Nc
  | tlsdescAdrPage21
  | tlsdescLd64Lo12
  | tlsdescAddLo12
  | tlsdescCall
  | tlsleAddTprelHi12
  | tlsleAddTprelLo12
  | tlsleAddTprelLo12Nc
  | tlsleLdst8TprelLo12Nc
  | tlsleLdst16TprelLo12Nc
  | tlsleLdst32TprelLo12Nc
  | tlsleLdst64TprelLo12Nc
  | tlsleLdst128TprelLo12Nc
  | tlsleMovwTprelG1
  | tlsleMovwTprelG1Nc
  | tlsleMovwTprelG0
  | tlsleMovwTprelG0Nc
  deriving DecidableEq, Repr, Inhabited

def RelocKind.isGotOrTlsIeL108–112 ↗#

Whether kind is a GOT or initial-exec TLS relocation class.

def RelocKind.isGotOrTlsIe : RelocKind → Bool
  | .adrGotPage | .ld64GotLo12Nc
  | .tlsieAdrGottprelPage21 | .tlsieLd64GottprelLo12Nc => true
  | _ => false

structure RelocEntryL114–123 ↗#

One relocation at byte offset off within a function or data symbol, targeting sym + addend. When localSym = true, sym is resolved exclusively in the defining object's symbol table (STB_LOCAL).

structure RelocEntry where
  off : Nat
  kind : RelocKind
  sym : String
  addend : Int := 0
  localSym : Bool := false
  deriving DecidableEq, Repr, Inhabited

1 declaration not shown (lines 125–130): theorems, which Lean checks, or definitions that no headline statement uses

Arm64.Obj.SymCodeInfo.relocs, Arm64.Obj.SymCodeInfo, Arm64.Obj.SymCodeInfo.code, Arm64.Obj.SymCodeInfo.sym

structure SymDataInfoL132–140 ↗#

Link-independent facts about one .rodata, .data, .data.rel.ro, or .bss symbol (dataSyms).

structure SymDataInfo where
  sym : String
  align : Nat := 1
  readOnly : Bool := true
  bytes : List (BitVec 8) := []
  zeroTail : Nat := 0
  relocs : List RelocEntry := []
  deriving DecidableEq, Repr, Inhabited

2 declarations not shown (lines 144–156): theorems, which Lean checks, or definitions that no headline statement uses

Arm64.Obj.branchInRange, Arm64.Obj.patchBranchBytes

def branchWordL158–160 ↗#

Patch 32-bit instruction template w for a 26-bit branch (B/BL) from place to target.

def branchWord (w : BitVec 32) (place target : BitVec 64) : BitVec 32 :=
  (w &&& 0xfc000000#32) ||| (((target - place) >>> 2).setWidth 32 &&& 0x03ffffff#32)

def BranchInRangeL162–165 ↗#

Propositional range condition for a 26-bit PC-relative branch (B/BL).

def BranchInRange (place target : BitVec 64) : Prop :=
  (target - place).toNat % 4 = 0 ∧
  -(2 ^ 27 : Int) ≤ (target - place).toInt ∧ (target - place).toInt < (2 ^ 27 : Int)

def adrpWordOffL167–171 ↗#

Patch 32-bit ADRP template w with page displacement pgOff = pageOf target - pageOf place.

def adrpWordOff (w : BitVec 32) (pgOff : BitVec 64) : BitVec 32 :=
  (w &&& 0x9f00001f#32) |||
    ((((pgOff >>> 12).setWidth 32 &&& 0x3#32) <<< 29) |||
     (((pgOff >>> 14).setWidth 32 &&& 0x7ffff#32) <<< 5))

def adrpWordL173–175 ↗#

Patch 32-bit ADRP template w at place targeting target.

def adrpWord (w : BitVec 32) (place target : BitVec 64) : BitVec 32 :=
  adrpWordOff w (pageOf target - pageOf place)

def AdrpInRangeL177–180 ↗#

Propositional range condition ([-4 GiB, 4 GiB)) for R_AARCH64_ADR_PREL_PG_HI21 / R_AARCH64_ADR_GOT_PAGE.

def AdrpInRange (place target : BitVec 64) : Prop :=
  -(2 ^ 32 : Int) ≤ (pageOf target - pageOf place).toInt ∧
  (pageOf target - pageOf place).toInt < (2 ^ 32 : Int)

1 declaration not shown (lines 182–185): theorems, which Lean checks, or definitions that no headline statement uses

Arm64.Obj.adrpInRange

def adrWordOffL187–191 ↗#

Patch 32-bit ADR template w with byte displacement d = target - place.

def adrWordOff (w : BitVec 32) (d : BitVec 64) : BitVec 32 :=
  (w &&& 0x9f00001f#32) |||
    (((d.setWidth 32 &&& 0x3#32) <<< 29) |||
     (((d >>> 2).setWidth 32 &&& 0x7ffff#32) <<< 5))

def adrWordL193–195 ↗#

Patch 32-bit ADR template w at place targeting target.

def adrWord (w : BitVec 32) (place target : BitVec 64) : BitVec 32 :=
  adrWordOff w (target - place)

def AdrInRangeL197–199 ↗#

Propositional range condition ([-1 MiB, 1 MiB)) for R_AARCH64_ADR_PREL_LO21.

def AdrInRange (place target : BitVec 64) : Prop :=
  -(2 ^ 20 : Int) ≤ (target - place).toInt ∧ (target - place).toInt < (2 ^ 20 : Int)

1 declaration not shown (lines 201–204): theorems, which Lean checks, or definitions that no headline statement uses

Arm64.Obj.adrInRange

def lo12WordL206–209 ↗#

Patch 32-bit :lo12: instruction template w (ADD or scaled LDR/STR with shift scale).

def lo12Word (scale : Nat) (w : BitVec 32) (target : BitVec 64) : BitVec 32 :=
  (w &&& 0xffc003ff#32) |||
    ((((target &&& 0xfff#64) >>> scale).setWidth 32 &&& 0xfff#32) <<< 10)

def lo12AlignMaskL211–217 ↗#

Low-bit alignment mask (1 <<< scale) - 1 for scaled :lo12: load/store relocations.

def lo12AlignMask : Nat → BitVec 64
  | 0 => 0#64
  | 1 => 1#64
  | 2 => 3#64
  | 3 => 7#64
  | _ => 15#64

def Lo12AlignedL219–221 ↗#

Propositional alignment condition for a 2^scale-byte scaled :lo12: relocation.

def Lo12Aligned (scale : Nat) (target : BitVec 64) : Prop :=
  (target &&& lo12AlignMask scale) = 0#64

1 declaration not shown (lines 223–225): theorems, which Lean checks, or definitions that no headline statement uses

Arm64.Obj.lo12Aligned

def imm19WordOffL227–229 ↗#

Patch 32-bit 19-bit PC-relative instruction template w (B.cond, CBZ/CBNZ, LDR literal).

def imm19WordOff (w : BitVec 32) (d : BitVec 64) : BitVec 32 :=
  (w &&& 0xff00001f#32) ||| (((d >>> 2).setWidth 32 &&& 0x7ffff#32) <<< 5)

def imm19WordL231–233 ↗#

Patch 32-bit 19-bit PC-relative instruction template w at place targeting target.

def imm19Word (w : BitVec 32) (place target : BitVec 64) : BitVec 32 :=
  imm19WordOff w (target - place)

def Imm19InRangeL235–238 ↗#

Propositional range condition ([-1 MiB, 1 MiB), 4-byte aligned) for CONDBR19 / LD_PREL_LO19.

def Imm19InRange (place target : BitVec 64) : Prop :=
  (target - place).toNat % 4 = 0 ∧
  -(2 ^ 20 : Int) ≤ (target - place).toInt ∧ (target - place).toInt < (2 ^ 20 : Int)

1 declaration not shown (lines 240–243): theorems, which Lean checks, or definitions that no headline statement uses

Arm64.Obj.imm19InRange

def tstbr14WordOffL245–247 ↗#

Patch 32-bit 14-bit PC-relative test-and-branch template w (TBZ/TBNZ).

def tstbr14WordOff (w : BitVec 32) (d : BitVec 64) : BitVec 32 :=
  (w &&& 0xfff8001f#32) ||| (((d >>> 2).setWidth 32 &&& 0x3fff#32) <<< 5)

def tstbr14WordL249–251 ↗#

Patch 32-bit 14-bit PC-relative test-and-branch template w at place targeting target.

def tstbr14Word (w : BitVec 32) (place target : BitVec 64) : BitVec 32 :=
  tstbr14WordOff w (target - place)

def TstBr14InRangeL253–256 ↗#

Propositional range condition ([-32 KiB, 32 KiB), 4-byte aligned) for R_AARCH64_TSTBR14.

def TstBr14InRange (place target : BitVec 64) : Prop :=
  (target - place).toNat % 4 = 0 ∧
  -(2 ^ 15 : Int) ≤ (target - place).toInt ∧ (target - place).toInt < (2 ^ 15 : Int)

1 declaration not shown (lines 258–261): theorems, which Lean checks, or definitions that no headline statement uses

Arm64.Obj.tstbr14InRange

def Prel32InRangeL263–265 ↗#

Propositional range condition ([-2 GiB, 2 GiB)) for R_AARCH64_PREL32.

def Prel32InRange (place target : BitVec 64) : Prop :=
  -(2 ^ 31 : Int) ≤ (target - place).toInt ∧ (target - place).toInt < (2 ^ 31 : Int)

1 declaration not shown (lines 267–270): theorems, which Lean checks, or definitions that no headline statement uses

Arm64.Obj.prel32InRange

def Abs32InRangeL272–274 ↗#

Propositional range condition for R_AARCH64_ABS32.

def Abs32InRange (target : BitVec 64) : Prop :=
  -(2 ^ 31 : Int) ≤ target.toInt ∧ target.toInt < (2 ^ 32 : Int)

def isLdr64UnsignedWordL276–277 ↗#

w is a 64-bit unsigned-offset LDR Xt, [Xn, #pimm] (11 111 0 01 01 imm12 Rn Rt).

def isLdr64UnsignedWord (w : BitVec 32) : Bool := (w &&& 0xffc00000#32) == 0xf9400000#32

def ldrToAddWordL279–280 ↗#

Convert a 64-bit LDR Xt, [Xn, #0] template w into ADD Xd, Xn, #0 (preserving Rn and Rd).

def ldrToAddWord (w : BitVec 32) : BitVec 32 := 0x91000000#32 ||| (w &&& 0x3ff#32)

def tlsieMovzWordL282–285 ↗#

Relax R_AARCH64_TLSIE_ADR_GOTTPREL_PAGE21 (ADRP Xd, :gottprel:sym) to MOVZ Xd, #:tprel_g1:target, LSL #16 (0xd2a00000 | Rd | (((target >> 16) & 0xffff) << 5)).

def tlsieMovzWord (w : BitVec 32) (target : BitVec 64) : BitVec 32 :=
  0xd2a00000#32 ||| (w &&& 0x1f#32) ||| (((target >>> 16).setWidth 32 &&& 0xffff#32) <<< 5)

def tlsieMovkWordL287–290 ↗#

Relax R_AARCH64_TLSIE_LD64_GOTTPREL_LO12_NC (LDR Xd, [Xn, :gottprel_lo12:sym]) to MOVK Xd, #:tprel_g0_nc:target (0xf2800000 | Rd | ((target & 0xffff) << 5)).

def tlsieMovkWord (w : BitVec 32) (target : BitVec 64) : BitVec 32 :=
  0xf2800000#32 ||| (w &&& 0x1f#32) ||| ((target.setWidth 32 &&& 0xffff#32) <<< 5)

def TlsIeInRangeL292–294 ↗#

Propositional 32-bit unsigned TP-offset range ([0, 2^32)) for IE-to-LE TLS relaxation.

def TlsIeInRange (target : BitVec 64) : Prop :=
  target.toNat < 2 ^ 32

4 declarations not shown (lines 296–343): theorems, which Lean checks, or definitions that no headline statement uses

Arm64.Obj.tlsIeInRange, Arm64.Obj.addSignedOff, Arm64.Obj.codeRelocInRange, Arm64.Obj.patchCodeRelocWord

end Arm64.Obj