From 32a6fcb12814550633261960b540ffeb8a0fcab5 Mon Sep 17 00:00:00 2001 From: varobert Date: Wed, 4 Apr 2012 11:59:40 +0000 Subject: Added safety to potentially overflowing arithmetics git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@1872 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e --- checklink/ELF_utils.ml | 30 ++++++++++++++---------------- 1 file changed, 14 insertions(+), 16 deletions(-) (limited to 'checklink/ELF_utils.ml') diff --git a/checklink/ELF_utils.ml b/checklink/ELF_utils.ml index f860e3f..d5c205a 100644 --- a/checklink/ELF_utils.ml +++ b/checklink/ELF_utils.ml @@ -11,9 +11,9 @@ let section_ndx_by_name (e: elf)(name: string): int option = let section_bitstring_noelf (bs: bitstring)(eshdra: elf32_shdr array)(sndx: int): bitstring = - let sofs = int32_int eshdra.(sndx).sh_offset in - let size = int32_int eshdra.(sndx).sh_size in - Bitstring.subbitstring bs (sofs * 8) (size * 8) + let sofs = Safe32.to_int eshdra.(sndx).sh_offset in + let size = Safe32.to_int eshdra.(sndx).sh_size in + Bitstring.subbitstring bs Safe.(sofs * 8) Safe.(size * 8) let section_bitstring (e: elf): int -> bitstring = section_bitstring_noelf e.e_bitstring e.e_shdra @@ -30,27 +30,25 @@ let section_at_vaddr (e: elf)(vaddr: int32): int option = e.e_shdra (** - Returns the entire bitstring that begins at the specified virtual address - within the specified section and ends at the end of the file. This is useful - when you don't know the sections size yet. + Returns the bitstring of the specified size beginning at the specified + virtual address within the specified section. *) -let bitstring_at_vaddr_nosize (e: elf)(sndx: int)(vaddr: int32): bitstring = +let bitstring_at_vaddr e sndx vaddr size = let shdr = e.e_shdra.(sndx) in let bs = section_bitstring e sndx in - let ofs = int32_int (Int32.sub vaddr shdr.sh_addr) in - bitmatch bs with - | { subbs : -1 : bitstring, offset(8*ofs) } -> subbs + let bit_ofs = Safe.(8 * Safe32.(to_int (vaddr - shdr.sh_addr))) in + Bitstring.subbitstring bs bit_ofs size (** - Returns the bitstring of the specified size beginning at the specified - virtual address within the specified section. + Returns the entire bitstring that begins at the specified virtual address + within the specified section and ends at the end of the file. This is useful + when you don't know the sections size yet. *) -let bitstring_at_vaddr e sndx vaddr size = +let bitstring_at_vaddr_nosize (e: elf)(sndx: int)(vaddr: int32): bitstring = let shdr = e.e_shdra.(sndx) in let bs = section_bitstring e sndx in - let ofs = int32_int (Int32.sub vaddr shdr.sh_addr) in - bitmatch bs with - | { subbs : size : bitstring, offset(8*ofs) } -> subbs + let bit_ofs = Safe.(8 * Safe32.(to_int (vaddr - shdr.sh_addr))) in + Bitstring.dropbits bit_ofs bs (** Removes symbol version for GCC's symbols. -- cgit v1.2.3