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/Check.ml | 66 +++++++++++++------------- checklink/ELF_parsers.ml | 117 ++++++++++++++++++++++++----------------------- checklink/ELF_utils.ml | 30 ++++++------ checklink/Exc.ml | 2 + checklink/Frameworks.ml | 8 ++-- checklink/Fuzz.ml | 10 ++-- checklink/Library.ml | 63 +++++++++++-------------- checklink/PPC_utils.ml | 2 +- checklink/Safe.ml | 25 ++++++++++ checklink/Safe32.ml | 34 ++++++++++++++ 10 files changed, 206 insertions(+), 151 deletions(-) create mode 100644 checklink/Exc.ml create mode 100644 checklink/Safe.ml create mode 100644 checklink/Safe32.ml (limited to 'checklink') diff --git a/checklink/Check.ml b/checklink/Check.ml index 33914f2..be56fe0 100644 --- a/checklink/Check.ml +++ b/checklink/Check.ml @@ -129,7 +129,7 @@ let check_fun_symtab let symtab_ent_start = Int32.(add elf.e_shdra.(symtab_sndx).sh_offset - (int_int32 (16 * sym_ndx))) in + (Safe32.of_int (16 * sym_ndx))) in let sym = sfw.ef.elf.e_symtab.(sym_ndx) in let atom = Hashtbl.find sfw.atoms ident in let section = @@ -160,7 +160,7 @@ let check_fun_symtab (** Checks that the offset [ofs] is well aligned with regards to [al], expressed in bytes. *) let is_well_aligned (ofs: int32) (al: int): bool = - al = 0 || Int32.rem ofs (int_int32 al) = 0l + al = 0 || Int32.rem ofs (Safe32.of_int al) = 0l (** Adds a function symbol to the set of covered symbols. *) let mark_covered_fun_sym_ndx (ndx: int) ffw: f_framework = @@ -201,7 +201,7 @@ let re_variadic_stub: Str.regexp = Str.regexp "\\(.*\\)\\$[if]*$" out all symbols whose virtual address does not match [vaddr]. *) let idmap_unify - (k: positive) (vaddr: int32) (sfw: s_framework): s_framework on_success = + (k: positive) (vaddr: int32) (sfw: s_framework): s_framework or_err = try ( let id_ndxes = PosMap.find k sfw.ident_to_sym_ndx in match List.filter @@ -260,7 +260,7 @@ let idmap_unify Subsequent references to the label will have to conform. *) let lblmap_unify (k: label) (v: int32) (ffw: f_framework) - : f_framework on_success = + : f_framework or_err = try ( let v' = PosMap.find k ffw.label_to_vaddr in if v = v' @@ -408,7 +408,7 @@ let match_z_int32 (cz: coq_Z) (ei: int32) = check_eq "match_z_int32" (z_int32 cz) ei let match_z_int (cz: coq_Z) (ei: int) = - check_eq "match_z_int" (z_int32 cz) (int_int32 ei) + check_eq "match_z_int" (z_int32 cz) (Safe32.of_int ei) (* [m] is interpreted as a bitmask, and checked against [ei]. *) let match_mask (m: coq_Z) (ei: int32) = @@ -544,7 +544,7 @@ let rec match_jmptbl lbllist vaddr size ffw = ) >>> match_jmptbl_aux lbllist bs >>? (ff_ef ^%= - add_range ofs (int_int32 (size / 8)) 0 Jumptable) + add_range ofs (Safe32.of_int (size / 8)) 0 Jumptable) (** Matches [ecode] agains the expected code for a small memory copy pseudo-instruction. Returns a triple containing the updated framework, @@ -553,7 +553,7 @@ let rec match_jmptbl lbllist vaddr size ffw = let match_memcpy_small ecode pc sz al src dst (fw: f_framework) : (f_framework * ecode * int32) option = let rec match_memcpy_small_aux ofs sz ecode pc (fw: f_framework) = - let ofs32 = int_int32 ofs in + let ofs32 = Safe32.of_int ofs in if sz >= 8 && al >= 4 then ( match ecode with @@ -632,7 +632,7 @@ let match_memcpy_big ecode pc sz al src dst fw STWU (rS5, rA5, d5) :: (* | *) BCx (bo6, bi6, bd6, aa6, lk6) :: (* pc + 24 -- *) es -> - let sz' = int_int32 (sz / 4) in + let sz' = Safe32.of_int (sz / 4) in let (s, d) = if dst <> GPR11 then (GPR11, GPR12) else (GPR12, GPR11) in let target_vaddr = Int32.(add 16l pc) in let dest_vaddr = Int32.(add (add 24l pc) (mul 4l (exts bd6))) in @@ -723,7 +723,7 @@ let match_memcpy_big ecode pc sz al src dst fw (** Compares a whole CompCert function code against an ELF code, starting at program counter [pc]. *) -let rec compare_code ccode ecode pc fw: f_framework on_success = +let rec compare_code ccode ecode pc fw: f_framework or_err = let error = ERR("Non-matching instructions") in match ccode, ecode with | [], [] -> OK(fw) @@ -790,7 +790,7 @@ let rec compare_code ccode ecode pc fw: f_framework on_success = fw >>> match_iregs rd rD >>> match_iregs r1 rA - >>> match_csts cst (int_int32 simm) + >>> match_csts cst (Safe32.of_int simm) >>> recur_simpl | _ -> error end @@ -851,7 +851,7 @@ let rec compare_code ccode ecode pc fw: f_framework on_success = fw >>> match_iregs rd rA >>> match_iregs r1 rS - >>> match_csts cst (int_int32 uimm) + >>> match_csts cst (Safe32.of_int uimm) >>> recur_simpl | _ -> error end @@ -861,7 +861,7 @@ let rec compare_code ccode ecode pc fw: f_framework on_success = fw >>> match_iregs rd rA >>> match_iregs r1 rS - >>> match_csts cst (int_int32 uimm) + >>> match_csts cst (Safe32.of_int uimm) >>> recur_simpl | _ -> error end @@ -984,7 +984,7 @@ let rec compare_code ccode ecode pc fw: f_framework on_success = MTSPR (rS2, spr2) :: BCCTRx(bo3, bi3, rc3) :: es -> let tblvaddr = Int32.( - add (shift_left (int_int32 simm0) 16) (exts d1) + add (shift_left (Safe32.of_int simm0) 16) (exts d1) ) in let tblsize = (32 * List.length table) in fw @@ -1260,7 +1260,7 @@ let rec compare_code ccode ecode pc fw: f_framework on_success = fw >>> match_iregs GPR11 rD >>> match_iregs GPR0 rA - >>> match_csts high (int_int32 simm) + >>> match_csts high (Safe32.of_int simm) >>> check_builtin_vload_common cs es (Int32.add pc 4l) chunk GPR11 (Csymbol_low(ident, ofs)) res @@ -1280,7 +1280,7 @@ let rec compare_code ccode ecode pc fw: f_framework on_success = fw >>> match_iregs tmp rD >>> match_iregs GPR0 rA - >>> match_csts high (int_int32 simm) + >>> match_csts high (Safe32.of_int simm) >>> check_builtin_vstore_common cs es (Int32.add pc 4l) chunk tmp (Csymbol_low(ident, ofs)) src @@ -1358,7 +1358,7 @@ let rec compare_code ccode ecode pc fw: f_framework on_success = | CMPLI(crfD, l, rA, uimm) :: es -> fw >>> match_iregs r1 rA - >>> match_csts cst (int_int32 uimm) + >>> match_csts cst (Safe32.of_int uimm) >>> match_crbits CRbit_0 crfD >>> match_bools false l >>> recur_simpl @@ -1699,7 +1699,7 @@ let rec compare_code ccode ecode pc fw: f_framework on_success = | ADDIS(rD0, rA0, simm0) :: LFD (frD1, rA1, d1) :: es -> let vaddr = Int32.( - add (shift_left (int_int32 simm0) 16) (exts d1) + add (shift_left (Safe32.of_int simm0) 16) (exts d1) ) in if Int32.rem vaddr 8l <> 0l then ERR("Float constants should be 8-byte aligned") @@ -1892,7 +1892,7 @@ let rec compare_code ccode ecode pc fw: f_framework on_success = fw >>> match_iregs rd rA >>> match_iregs r1 rS - >>> match_csts cst (int_int32 uimm) + >>> match_csts cst (Safe32.of_int uimm) >>> recur_simpl | _ -> error end @@ -1902,7 +1902,7 @@ let rec compare_code ccode ecode pc fw: f_framework on_success = fw >>> match_iregs rd rA >>> match_iregs r1 rS - >>> match_csts cst (int_int32 uimm) + >>> match_csts cst (Safe32.of_int uimm) >>> recur_simpl | _ -> error end @@ -2133,7 +2133,7 @@ let rec compare_code ccode ecode pc fw: f_framework on_success = fw >>> match_iregs rd rA >>> match_iregs r1 rS - >>> match_csts cst (int_int32 uimm) + >>> match_csts cst (Safe32.of_int uimm) >>> recur_simpl | _ -> error end @@ -2143,7 +2143,7 @@ let rec compare_code ccode ecode pc fw: f_framework on_success = fw >>> match_iregs rd rA >>> match_iregs r1 rS - >>> match_csts cst (int_int32 uimm) + >>> match_csts cst (Safe32.of_int uimm) >>> recur_simpl | _ -> error end @@ -2406,10 +2406,10 @@ type maybe_bitstring = framework as well as the size of the data matched. **) let compare_data (l: init_data list) (maybebs: maybe_bitstring) (sfw: s_framework) - : (s_framework * int) on_success = + : (s_framework * int) or_err = let error = ERR("Reached end of data bitstring too soon") in let rec compare_data_aux l bs s (sfw: s_framework): - (s_framework * int) on_success = + (s_framework * int) or_err = match l with | [] -> OK(sfw, s) | d::l -> @@ -2476,7 +2476,7 @@ let compare_data (l: init_data list) (maybebs: maybe_bitstring) (sfw: s_framewor end in let rec compare_data_empty l s (sfw: s_framework): - (s_framework * int) on_success = + (s_framework * int) or_err = match l with | [] -> OK(sfw, s) | d::l -> @@ -2496,7 +2496,7 @@ let check_data_symtab ident sym_ndx size sfw = let symtab_ent_start = Int32.( add elf.e_shdra.(elf.e_symtab_sndx).sh_offset - (int_int32 (16 * sym_ndx)) + (Safe32.of_int (16 * sym_ndx)) ) in let sym = sfw.ef.elf.e_symtab.(sym_ndx) in let atom = Hashtbl.find sfw.atoms ident in @@ -2507,7 +2507,7 @@ let check_data_symtab ident sym_ndx size sfw = in sfw >>> ( - if sym.st_size = int_int32 size + if sym.st_size = Safe32.of_int size then id else ( sf_ef ^%= @@ -2554,7 +2554,7 @@ let check_data (pv: (ident * unit globvar) list) (sfw: s_framework) let sym_bs = match elf.e_shdra.(sym_sndx).sh_type with | SHT_NOBITS -> - Empty(int32_int sym.st_size * 8) + Empty(Safe.(of_int32 sym.st_size * 8)) | SHT_PROGBITS -> NonEmpty(bitstring_at_vaddr_nosize elf sym_sndx sym_vaddr) | _ -> assert false @@ -2872,7 +2872,7 @@ let check_padding efw = the end. *) | [(_, e, _, _) as h] -> let elf_size = - int_int32 ((Bitstring.bitstring_length efw.elf.e_bitstring) / 8) in + Safe32.of_int ((Bitstring.bitstring_length efw.elf.e_bitstring) / 8) in let elf_end = Int32.sub elf_size 1l in if e = elf_end then { efw with @@ -2890,9 +2890,9 @@ let check_padding efw = let pad_stop = Int32.sub b2 1l in if pad_start = b2 (* if they are directly consecutive *) - || int32_int (Int32.sub b2 e1) > a2 (* or if they are too far away *) + || Safe.(of_int32 b2 - of_int32 e1) > a2 (* or if they are too far away *) || not (is_padding efw.elf.e_bitstring - (int32_int pad_start) (int32_int pad_stop)) + (Safe32.to_int pad_start) (Safe32.to_int pad_stop)) then (* not padding *) if pad_start <= pad_stop then check_padding_aux efw @@ -2984,7 +2984,7 @@ let check_elf_nodump elf sdumps = let nb_syms = Array.length elf.e_symtab in let section_strtab = elf.e_shdra.(eh.e_shstrndx) in let symtab_shdr = elf.e_shdra.(elf.e_symtab_sndx) in - let symbol_strtab = elf.e_shdra.(int32_int symtab_shdr.sh_link) in + let symbol_strtab = elf.e_shdra.(Safe32.to_int symtab_shdr.sh_link) in let efw = { elf = elf; @@ -2996,12 +2996,12 @@ let check_elf_nodump elf sdumps = >>> check_elf_header >>> add_range eh.e_phoff - (int_int32 (eh.e_phnum * eh.e_phentsize)) + Safe.(to_int32 (eh.e_phnum * eh.e_phentsize)) 4 ELF_progtab >>> add_range eh.e_shoff - (int_int32 (eh.e_shnum * eh.e_shentsize)) + Safe.(to_int32 (eh.e_shnum * eh.e_shentsize)) 4 ELF_shtab >>> add_range diff --git a/checklink/ELF_parsers.ml b/checklink/ELF_parsers.ml index c71ff00..ba04c68 100644 --- a/checklink/ELF_parsers.ml +++ b/checklink/ELF_parsers.ml @@ -17,24 +17,24 @@ let elfdata_to_endian (e: elfdata): Bitstring.endian = (** Parses an elf32 header *) let read_elf32_ehdr (bs: bitstring): elf32_ehdr = bitmatch bs with - | { e_ident : 16*8 : bitstring ; - rest : -1 : bitstring } -> + | { e_ident : 16*8 : bitstring ; + rest : -1 : bitstring } -> ( bitmatch e_ident with - | { 0x7F : 8 ; - "ELF" : 24 : string ; - ei_class : 8 : int ; - ei_data : 8 : int ; - ei_version : 8 : int ; - padding : 72 : bitstring } -> + | { 0x7F : 8 ; + "ELF" : 24 : string ; + ei_class : 8 : int ; + ei_data : 8 : int ; + ei_version : 8 : int ; + padding : 72 : bitstring } -> assert (is_zeros padding 72); - let ei_data = ( - match ei_data with + let ei_data = + begin match ei_data with | 0 -> ELFDATANONE | 1 -> ELFDATA2LSB | 2 -> ELFDATA2MSB | _ -> ELFDATAUNKNOWN - ) + end in let e = elfdata_to_endian ei_data in ( @@ -59,32 +59,32 @@ let read_elf32_ehdr (bs: bitstring): elf32_ehdr = { e_ident = { - ei_class = ( - match ei_class with + ei_class = + begin match ei_class with | 0 -> ELFCLASSNONE | 1 -> ELFCLASS32 | 2 -> ELFCLASS64 | _ -> ELFCLASSUNKNOWN - ); + end; ei_data = ei_data; - ei_version = ( - match ei_version with + ei_version = + begin match ei_version with | 0 -> EV_NONE | 1 -> EV_CURRENT | _ -> EV_UNKNOWN - ); + end; }; - e_type = ( - match e_type with + e_type = + begin match e_type with | 0 -> ET_NONE | 1 -> ET_REL | 2 -> ET_EXEC | 3 -> ET_DYN | 4 -> ET_CORE | _ -> ET_UNKNOWN - ); - e_machine = ( - match e_machine with + end; + e_machine = + begin match e_machine with | 0 -> EM_NONE | 1 -> EM_M32 | 2 -> EM_SPARC @@ -96,13 +96,13 @@ let read_elf32_ehdr (bs: bitstring): elf32_ehdr = | 10 -> EM_MIPS_RS4_BE | 20 -> EM_PPC | _ -> EM_UNKNOWN - ); - e_version = ( - match e_version with + end; + e_version = + begin match e_version with | 0l -> EV_NONE | 1l -> EV_CURRENT | _ -> EV_UNKNOWN - ); + end; e_entry = e_entry; e_phoff = e_phoff; e_shoff = e_shoff; @@ -119,22 +119,24 @@ let read_elf32_ehdr (bs: bitstring): elf32_ehdr = (** Returns the file offset of the section header indexed *) let section_header_offset (e_hdr: elf32_ehdr) (sndx: int): int = - int32_int e_hdr.e_shoff + sndx * e_hdr.e_shentsize + Safe.(of_int32 e_hdr.e_shoff + (sndx * e_hdr.e_shentsize)) (** Returns the ndx-th string in the provided bitstring, according to null characters *) let strtab_string (bs: bitstring) (ndx: int): string = let (str, ofs, _) = bs in - let start = (ofs/8 + ndx) in + let start = (ofs / 8 + ndx) in String.sub str start (String.index_from str start '\000' - start) (** Reads an ELF section header *) let read_elf32_shdr (e_hdr: elf32_ehdr) (bs: bitstring) (strtab: bitstring) (num: int): elf32_shdr = let e = elfdata_to_endian e_hdr.e_ident.ei_data in - let byte_ofs = section_header_offset e_hdr num in + let bit_ofs = Safe.( + (section_header_offset e_hdr num) * 8 + ) in bitmatch bs with - | { sh_name : 32 : endian(e), offset(byte_ofs*8) ; + | { sh_name : 32 : endian(e), offset(bit_ofs) ; sh_type : 32 : endian(e) ; sh_flags : 32 : endian(e) ; sh_addr : 32 : endian(e) ; @@ -145,9 +147,9 @@ let read_elf32_shdr (e_hdr: elf32_ehdr) (bs: bitstring) (strtab: bitstring) sh_addralign : 32 : endian(e) ; sh_entsize : 32 : endian(e) } -> { - sh_name = strtab_string strtab (int32_int sh_name); - sh_type = ( - match sh_type with + sh_name = strtab_string strtab (Safe32.to_int sh_name); + sh_type = + begin match sh_type with | 0l -> SHT_NULL | 1l -> SHT_PROGBITS | 2l -> SHT_SYMTAB @@ -161,7 +163,7 @@ let read_elf32_shdr (e_hdr: elf32_ehdr) (bs: bitstring) (strtab: bitstring) | 10l -> SHT_SHLIB | 11l -> SHT_DYNSYM | _ -> SHT_UNKNOWN - ); + end; sh_flags = sh_flags ; sh_addr = sh_addr ; sh_offset = sh_offset ; @@ -173,12 +175,13 @@ let read_elf32_shdr (e_hdr: elf32_ehdr) (bs: bitstring) (strtab: bitstring) } (** Reads an elf program header *) -let read_elf32_phdr (e_hdr: elf32_ehdr) (bs: bitstring) (ndx: int) - : elf32_phdr = +let read_elf32_phdr (e_hdr: elf32_ehdr) (bs: bitstring) (ndx: int): elf32_phdr = let e = elfdata_to_endian e_hdr.e_ident.ei_data in - let phdr_ofs = int32_int e_hdr.e_phoff + ndx * e_hdr.e_phentsize in + let bit_ofs = Safe.( + ((of_int32 e_hdr.e_phoff) + (ndx * e_hdr.e_phentsize)) * 8 + ) in bitmatch bs with - | { p_type : 32 : endian(e), offset(phdr_ofs*8) ; + | { p_type : 32 : endian(e), offset(bit_ofs) ; p_offset : 32 : endian(e) ; p_vaddr : 32 : endian(e) ; p_paddr : 32 : endian(e) ; @@ -187,8 +190,8 @@ let read_elf32_phdr (e_hdr: elf32_ehdr) (bs: bitstring) (ndx: int) p_flags : 32 : bitstring ; p_align : 32 : endian(e) } -> { - p_type = ( - match p_type with + p_type = + begin match p_type with | 0l -> PT_NULL | 1l -> PT_LOAD | 2l -> PT_DYNAMIC @@ -197,7 +200,7 @@ let read_elf32_phdr (e_hdr: elf32_ehdr) (bs: bitstring) (ndx: int) | 5l -> PT_SHLIB | 6l -> PT_PHDR | _ -> PT_UNKNOWN - ); + end; p_offset = p_offset ; p_vaddr = p_vaddr ; p_paddr = p_paddr ; @@ -211,8 +214,9 @@ let read_elf32_phdr (e_hdr: elf32_ehdr) (bs: bitstring) (ndx: int) let read_elf32_sym (e_hdr: elf32_ehdr) (symtab: bitstring) (strtab: bitstring) (num: int): elf32_sym = let e = elfdata_to_endian e_hdr.e_ident.ei_data in + let bit_ofs = Safe.(num * 128) in (* each symbol takes 16 bytes = 128 bits *) bitmatch symtab with - | { st_name : 32 : endian(e), offset(num*16*8) ; + | { st_name : 32 : endian(e), offset(bit_ofs) ; st_value : 32 : endian(e) ; st_size : 32 : endian(e) ; st_bind : 4 ; @@ -220,30 +224,30 @@ let read_elf32_sym (e_hdr: elf32_ehdr) (symtab: bitstring) (strtab: bitstring) st_other : 8 ; st_shndx : 16 : endian(e) } -> { - st_name = strtab_string strtab (int32_int st_name) ; + st_name = strtab_string strtab (Safe32.to_int st_name) ; st_value = st_value ; st_size = st_size ; - st_bind = ( - match st_bind with + st_bind = + begin match st_bind with | 0 -> STB_LOCAL | 1 -> STB_GLOBAL | 2 -> STB_WEAK | _ -> STB_UNKNOWN - ); - st_type = ( - match st_type with + end; + st_type = + begin match st_type with | 0 -> STT_NOTYPE | 1 -> STT_OBJECT | 2 -> STT_FUNC | 3 -> STT_SECTION | 4 -> STT_FILE | _ -> STT_UNKNOWN - ); + end; st_other = st_other ; st_shndx = st_shndx ; } -(** Aborts if two sections overlap *) +(** Abort if two sections overlap *) let check_overlaps (shdra: elf32_shdr array) (ehdr: elf32_ehdr): unit = let intersect a asize b bsize = asize <> 0l && bsize <> 0l && @@ -263,9 +267,9 @@ let check_overlaps (shdra: elf32_shdr array) (ehdr: elf32_ehdr): unit = if ai_intersects 0l 52l (* ELF header *) || ai_intersects ehdr.e_phoff - (int_int32 (ehdr.e_phnum * ehdr.e_phentsize)) + (Int32.of_int (ehdr.e_phnum * ehdr.e_phentsize)) || ai_intersects ehdr.e_shoff - (int_int32 (ehdr.e_shnum * ehdr.e_shentsize)) + (Int32.of_int (ehdr.e_shnum * ehdr.e_shentsize)) then assert false else Array.iteri @@ -288,10 +292,11 @@ let read_elf_bs (bs: bitstring): elf = let e = elfdata_to_endian e_hdr.e_ident.ei_data in let strtab_sndx = e_hdr.e_shstrndx in let strtab_shofs = section_header_offset e_hdr strtab_sndx in + let skipped_bits = Safe.(strtab_shofs * 8 + 128) in bitmatch bs with - | { ofs : 32 : endian(e), offset(strtab_shofs * 8 + 128) ; + | { ofs : 32 : endian(e), offset(skipped_bits) ; size : 32 : endian(e) } -> - Bitstring.subbitstring bs (int32_int ofs * 8) (int32_int size * 8) + Bitstring.subbitstring bs Safe.(of_int32 ofs * 8) Safe.(of_int32 size * 8) ) in let e_shdra = @@ -307,11 +312,11 @@ let read_elf_bs (bs: bitstring): elf = e_symtab = ( let symtab_shdr = e_shdra.(symtab_sndx) in let symtab_strtab_sndx = symtab_shdr.sh_link in - let symtab_nb_ent = (int32_int symtab_shdr.sh_size / 16) in + let symtab_nb_ent = (Safe32.to_int symtab_shdr.sh_size / 16) in Array.init symtab_nb_ent (read_elf32_sym e_hdr (section_bitstring_noelf bs e_shdra symtab_sndx) - (section_bitstring_noelf bs e_shdra (int32_int symtab_strtab_sndx))) + (section_bitstring_noelf bs e_shdra (Safe32.to_int symtab_strtab_sndx))) ); e_symtab_sndx = symtab_sndx; } 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. diff --git a/checklink/Exc.ml b/checklink/Exc.ml new file mode 100644 index 0000000..101087d --- /dev/null +++ b/checklink/Exc.ml @@ -0,0 +1,2 @@ +exception IntOverflow +exception Int32Overflow diff --git a/checklink/Frameworks.ml b/checklink/Frameworks.ml index fdd0769..f35672d 100644 --- a/checklink/Frameworks.ml +++ b/checklink/Frameworks.ml @@ -138,18 +138,18 @@ let add_range (start: int32) (length: int32) (align: int) (bcd: byte_chunk_desc) (* external ( >>> ) : 'a -> ('a -> 'b) -> 'b = "%revapply" *) let ( >>> ) (a: 'a) (f: 'a -> 'b): 'b = f a -let ( >>? ) (a: 'a on_success) (f: 'a -> 'b): 'b on_success = +let ( >>? ) (a: 'a or_err) (f: 'a -> 'b): 'b or_err = match a with | ERR(s) -> ERR(s) | OK(x) -> OK(f x) -let ( >>= ) (a: 'a on_success) (f: 'a -> 'b on_success): 'b on_success = +let ( >>= ) (a: 'a or_err) (f: 'a -> 'b or_err): 'b or_err = match a with | ERR(s) -> ERR(s) | OK(x) -> f x -let ( ^%=? ) (lens: ('a, 'b) Lens.t) (transf: 'b -> 'b on_success) - (arg: 'a): 'a on_success = +let ( ^%=? ) (lens: ('a, 'b) Lens.t) (transf: 'b -> 'b or_err) + (arg: 'a): 'a or_err = let focus = arg |. lens in match transf focus with | OK(res) -> OK((lens ^= res) arg) diff --git a/checklink/Fuzz.ml b/checklink/Fuzz.ml index c1f6780..fb7bee7 100644 --- a/checklink/Fuzz.ml +++ b/checklink/Fuzz.ml @@ -9,7 +9,7 @@ let fuzz_debug = ref false let string_of_byte = Printf.sprintf "0x%02x" let full_range_of_byte elfmap byte = - let byte = int_int32 byte in + let byte = Int32.of_int byte in List.find (fun (a, b, _, _) -> a <= byte && byte <= b) elfmap let range_of_byte elfmap byte = @@ -23,7 +23,7 @@ let fuzz_check elfmap bs byte old sdumps = let is_error = function ERROR(_) -> true | _ -> false in let (str, _, _) = bs in let fuzz_description = - string_of_int32 (int_int32 byte) ^ " <- " ^ + string_of_int32 (Int32.of_int byte) ^ " <- " ^ string_of_byte (Char.code str.[byte]) ^ " (was " ^ string_of_byte (Char.code old) ^ ") - " ^ string_of_byte_chunk_desc (range_of_byte elfmap byte) @@ -51,7 +51,7 @@ let fuzz_check elfmap bs byte old sdumps = | Assert_failure(s, l, c) -> if !fuzz_debug then Printf.printf "fuzz_check failed an assertion at %s (%d, %d)\n" s l c - | Library.Integer_overflow -> + | Exc.IntOverflow | Exc.Int32Overflow -> if !fuzz_debug then Printf.printf "fuzz_check raised an integer overflow exception\n" | Match_failure(s, l, c) -> @@ -74,8 +74,8 @@ let fuzz_check elfmap bs byte old sdumps = *) let ok_fuzz elfmap str byte fuzz = let (a, b, _, r) = full_range_of_byte elfmap byte in - let a = int32_int a in - let b = int32_int b in + let a = Safe32.to_int a in + let b = Safe32.to_int b in let old = Char.code str.[byte] in let fuz = Char.code fuzz in match r with diff --git a/checklink/Library.ml b/checklink/Library.ml index 0014025..67d8a45 100644 --- a/checklink/Library.ml +++ b/checklink/Library.ml @@ -3,29 +3,31 @@ open BinPos type bitstring = Bitstring.bitstring -let is_some = function +let is_some: 'a option -> bool = function | Some(_) -> true | None -> false -let from_some = function +let from_some: 'a option -> 'a = function | Some(x) -> x | None -> raise Not_found -let filter_some l = List.(map from_some (filter is_some l)) +let filter_some (l: 'a option list): 'a list = + List.(map from_some (filter is_some l)) -type 'a on_success = +type 'a or_err = | OK of 'a | ERR of string -let is_ok: 'a on_success -> bool = function +let is_ok: 'a or_err -> bool = function | OK(_) -> true | ERR(_) -> false -let from_ok = function +let from_ok: 'a or_err -> 'a = function | OK(x) -> x | ERR(_) -> raise Not_found -let filter_ok l = List.(map from_ok (filter is_ok l)) +let filter_ok (l: 'a or_err list): 'a list = + List.(map from_ok (filter is_ok l)) external id : 'a -> 'a = "%identity" @@ -41,17 +43,8 @@ let array_exists (cond: 'a -> bool) (arr: 'a array): int option = else array_exists_aux (ndx - 1) in array_exists_aux (Array.length arr - 1) -(* Functions for safely converting between numeric types *) - -exception Integer_overflow - -let int32_int (i32: int32): int = - let i = Int32.to_int i32 in - if i32 = Int32.of_int i - then i - else raise Integer_overflow - -let int_int32 = Int32.of_int +exception IntOverflow +exception Int32Overflow (* Can only return positive numbers 0 <= res < 2^31 *) let positive_int32 p = @@ -63,19 +56,19 @@ let positive_int32 p = let res = positive_int32_unsafe p in if res >= 0l then res - else raise Integer_overflow + else raise IntOverflow (* This allows for 1 bit of overflow, effectively returning a negative *) let rec positive_int32_lax = function | Coq_xI(p) -> let acc = positive_int32_lax p in if acc < 0l - then raise Integer_overflow + then raise Int32Overflow else Int32.(add (shift_left acc 1) 1l) | Coq_xO(p) -> let acc = positive_int32_lax p in if acc < 0l - then raise Integer_overflow + then raise Int32Overflow else Int32.shift_left acc 1 | Coq_xH -> 1l @@ -87,27 +80,27 @@ let z_int32 = function let z_int32_lax = function | Z0 -> 0l | Zpos(p) -> positive_int32_lax p -| Zneg(p) -> raise Integer_overflow +| Zneg(p) -> raise Int32Overflow -let z_int z = int32_int (z_int32 z) +let z_int z = Safe32.to_int (z_int32 z) -let z_int_lax z = int32_int (z_int32_lax z) +let z_int_lax z = Safe32.to_int (z_int32_lax z) (* Some more printers *) let string_of_array string_of_elt sep a = - "[\n" ^ - fst ( - Array.fold_left - ( - fun accu elt -> + let contents = + (fst + (Array.fold_left + (fun accu elt -> let (str, ndx) = accu in (str ^ (if ndx > 0 then sep else "") ^ string_of_int ndx ^ ": " ^ string_of_elt elt, ndx + 1) - ) - ("", 0) a - ) ^ - "\n]" + ) + ("", 0) a + ) + ) + in "[\n" ^ contents ^ "\n]" let string_of_list string_of_elt sep l = String.concat sep (List.map string_of_elt l) @@ -117,9 +110,7 @@ let string_of_bitstring bs = bitmatch bs with | { bit : 1 : int ; rest : -1 : bitstring } -> - (if bit - then "1" - else "0") ^ (string_of_bitset_aux rest) + (if bit then "1" else "0") ^ (string_of_bitset_aux rest) | { _ } -> "" in string_of_bitset_aux bs diff --git a/checklink/PPC_utils.ml b/checklink/PPC_utils.ml index 086d1c2..d027649 100644 --- a/checklink/PPC_utils.ml +++ b/checklink/PPC_utils.ml @@ -17,7 +17,7 @@ let code_of_sym_ndx (e: elf) (ndx: int): ecode option = match sym.st_type with | STT_FUNC -> let sym_vaddr = sym.st_value in - let sym_size = 8 * (int32_int sym.st_size) in + let sym_size = Safe.(of_int32 sym.st_size * 8) in let sym_sndx = sym.st_shndx in let code_bs = bitstring_at_vaddr e sym_sndx sym_vaddr sym_size in diff --git a/checklink/Safe.ml b/checklink/Safe.ml new file mode 100644 index 0000000..efcd3bd --- /dev/null +++ b/checklink/Safe.ml @@ -0,0 +1,25 @@ +(* "Hacker's Delight", section 2.12 *) + +let ( + ) x y = + let z = x + y in + (* Overflow occurs iff x and y have same sign and z's sign is different *) + if (z lxor x) land (z lxor y) < 0 + then raise Exc.IntOverflow + else z + +let ( - ) x y = + let z = x - y in + (* Overflow occurs iff x and y have opposite signs and z and x have + opposite signs *) + if (x lxor y) land (z lxor x) < 0 + then raise Exc.IntOverflow + else z + +let ( * ) x y = + let z = x * y in + if (x = min_int && y < 0) || (y <> 0 && z / y <> x) + then raise Exc.IntOverflow + else z + +let of_int32 = Safe32.to_int +let to_int32 = Safe32.of_int diff --git a/checklink/Safe32.ml b/checklink/Safe32.ml new file mode 100644 index 0000000..e72563d --- /dev/null +++ b/checklink/Safe32.ml @@ -0,0 +1,34 @@ +(* "Hacker's Delight", section 2.12 *) + +let ( + ) x y = Int32.( + let z = add x y in + (* Overflow occurs iff x and y have same sign and z's sign is different *) + if logand (logxor z x) (logxor z y) < 0l + then raise Exc.Int32Overflow + else z +) + +let ( - ) x y = Int32.( + let z = sub x y in + (* Overflow occurs iff x and y have opposite signs and z and x have + opposite signs *) + if logand (logxor x y) (logxor z x) < 0l + then raise Exc.Int32Overflow + else z +) + +let ( * ) x y = Int32.( + let z = mul x y in + if (x = min_int && y < 0l) || (y <> 0l && div z y <> x) + then raise Exc.Int32Overflow + else z +) + +let to_int i32 = Int32.( + let i = to_int i32 in + if i32 = of_int i + then i + else raise Exc.IntOverflow +) + +let of_int = Int32.of_int -- cgit v1.2.3