From 9ea00d39bb32c1f188f1af2745c3368da6a349c1 Mon Sep 17 00:00:00 2001 From: varobert Date: Thu, 24 May 2012 15:00:56 +0000 Subject: cchecklink continues when sections overlap cchecklink now reports overlapping sections but keeps analyzing. Error messages have also been made clearer. git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@1901 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e --- checklink/Check.ml | 89 +++++++++++++++++++++++++++++++++++------------- checklink/ELF_parsers.ml | 38 --------------------- checklink/Library.ml | 12 +++++++ 3 files changed, 77 insertions(+), 62 deletions(-) (limited to 'checklink') diff --git a/checklink/Check.ml b/checklink/Check.ml index 0483a89..54de487 100644 --- a/checklink/Check.ml +++ b/checklink/Check.ml @@ -91,10 +91,10 @@ let name_of_section: section_name -> string = begin match Configuration.system with - | "macosx" -> assert false + | "macosx" -> failwith "Unsupported CompCert configuration: macosx" | "linux" -> name_of_section_Linux | "diab" -> name_of_section_Diab - | _ -> assert false + | _ -> failwith "Unsupported CompCert configuration" end (** Compares a CompCert section name with an ELF section name. *) @@ -408,7 +408,8 @@ let match_csts (cc: constant) (ec: int32) (ffw: f_framework): f_framework = else ((ff_sf |-- ident_to_sym_ndx) ^%= (PosMap.add ident vaddrs)) ffw end | Csymbol_sda (ident, i) -> - assert false (* sda should be handled separately in places it occurs *) + (* sda should be handled separately in places it occurs *) + failwith "Unhandled Csymbol_sda, please report." let match_z_int32 (cz: coq_Z) (ei: int32) = check_eq "match_z_int32" (z_int32 cz) ei @@ -788,7 +789,7 @@ let check_sda ident ofs r addr ffw: f_framework or_err = | [] -> ERR("No satisfying SDA mapping, errors were: " ^ string_of_list id ", " (filter_err res)) | [ffw] -> OK(ffw) - | _ -> assert false (* This should not happen... *) + | _ -> failwith "Multiple possible SDA mappings, please report." (** Compares a whole CompCert function code against an ELF code, starting at program counter [pc]. @@ -1345,7 +1346,7 @@ let rec compare_code ccode ecode pc fw: f_framework or_err = fw >>> check_builtin_vload_common cs ecode pc chunk addr (Cint Integers.Int.zero) res - | _ -> assert false + | _ -> failwith "Unexpected args in EF_vload, please report." end | EF_vstore(chunk) -> begin match args with @@ -1353,7 +1354,7 @@ let rec compare_code ccode ecode pc fw: f_framework or_err = fw >>> check_builtin_vstore_common cs ecode pc chunk addr (Cint Integers.Int.zero) src - | _ -> assert false + | _ -> failwith "Unexpected args in EF_vstore, please report." end | EF_vload_global(chunk, ident, ofs) -> begin match ecode with @@ -1388,7 +1389,7 @@ let rec compare_code ccode ecode pc fw: f_framework or_err = (Csymbol_low(ident, ofs)) src | _ -> error end - | _ -> assert false + | _ -> failwith "Unexpected args in EF_vstore_global, please report." end | EF_memcpy(sz, al) -> let sz = z_int sz in @@ -1439,10 +1440,10 @@ let rec compare_code ccode ecode pc fw: f_framework or_err = else compare_code cs ecode pc fw | _ -> error end - | EF_annot(_, _) -> assert false - | EF_external(_, _) -> assert false - | EF_free -> assert false - | EF_malloc -> assert false + | EF_annot(_, _) -> failwith "Unexpected EF_annot, please report." + | EF_external(_, _) -> failwith "Unexpected EF_external, please report." + | EF_free -> failwith "Unexpected EF_free, please report." + | EF_malloc -> failwith "Unexpected EF_malloc, please report." end | Pcmplw(r1, r2) -> begin match ecode with @@ -1782,8 +1783,12 @@ let rec compare_code ccode ecode pc fw: f_framework or_err = | _ -> Section_literal end in + let continue = compare_code cs es (Int32.add 8l pc) in begin match bitstring_at_vaddr elf vaddr 64l with - | None -> assert false + | None -> + fw + >>> (ff_ef ^%= add_log (ERROR("Floating point constant address is wrong"))) + >>> continue | Some(bs, pofs, psize) -> let f = bitmatch bs with @@ -1805,7 +1810,7 @@ let rec compare_code ccode ecode pc fw: f_framework or_err = >>> match_floats c f >>> (ff_ef ^%= add_range pofs psize 8 (Float_literal(f))) >>> match_iregs GPR12 rA1 - >>> compare_code cs es (Int32.add 8l pc) + >>> continue end | _ -> error end @@ -2846,7 +2851,7 @@ let check_stubs sfw = sfw >>> (sf_ef ^%= add_log (ERROR("Couldn't match stub"))) end - | _ -> assert false + | _ -> failwith "Unexpected fundef in check_stubs, please report." end in PosMap.fold check_stub sfw.stub_ident_to_vaddr sfw @@ -2903,7 +2908,7 @@ let process_sdump efw sdump: e_framework = (fun f -> match f with | ident, Internal ccode -> (ident, Hashtbl.find names ident, ccode) - | _, External _ -> assert false + | _, External _ -> failwith "IMPOSSIBRU!" ) worklist_fundefs in @@ -2932,14 +2937,6 @@ let process_sdump efw sdump: e_framework = >>> check_data prog.prog_vars >>> (fun sfw -> sfw.ef) -(** Builds the list [0; 1; ...; n - 1]. *) -let list_n (n: int): int list = - let rec list_n_aux x l = - if x < 0 - then l - else list_n_aux (x - 1) (x :: l) - in list_n_aux (n - 1) [] - (** Returns true if [a, b] intersects [ofs, ofs + size - 1]. *) let intersect (a, b) ofs size: bool = let within (a, b) x = (a <= x) && (x <= b) in @@ -3011,7 +3008,7 @@ let check_padding efw = (* check_padding_aux assumes a sorted list *) let rec check_padding_aux efw accu l = match l with - | [] -> assert false + | [] -> efw (* if there is only one chunk left, we add an unknown space between it and the end. *) | [(_, e, _, _) as h] -> @@ -3156,6 +3153,48 @@ let warn_sda_mapping efw = efw ) +let (>>=) li f = List.flatten (List.map f li) + +(** Returns the list of all strictly-ordered pairs of [[0; len - 1]] that don't + satisfy f. *) +let forall_sym (len: int) (f: 'a -> 'a -> bool): ('a * 'a) list = + (list_n len) >>= fun x -> + (list_ab (x + 1) (len - 1)) >>= fun y -> + (if f x y then [] else [(x, y)]) + +let check_overlaps efw = + let shdra = efw.elf.e_shdra in + let intersect a asize b bsize = + asize <> 0l && bsize <> 0l && + ( + let last x xsize = Int32.(sub (add x xsize) 1l) in + let alast = last a asize in + let blast = last b bsize in + let within (a, b) x = (a <= x) && (x <= b) in + (within (a, alast) b) || (within (b, blast) a) + ) + in + match + forall_sym (Array.length shdra) + (fun i j -> + let ai = shdra.(i) in + let aj = shdra.(j) in + (ai.sh_type = SHT_NOBITS) + || (aj.sh_type = SHT_NOBITS) + || (not (intersect ai.sh_offset ai.sh_size aj.sh_offset aj.sh_size)) + ) + with + | [] -> efw + | l -> + List.fold_left + (fun efw (i, j) -> + let msg = + Printf.sprintf "Sections %s and %s overlap" shdra.(i).sh_name shdra.(j).sh_name + in + add_log (ERROR(msg)) efw + ) + efw l + (** Checks a whole ELF file according to a list of .sdump files. This never dumps anything, so it can be safely used when fuzz-testing even if the user accidentally enabled dumping options. *) @@ -3205,6 +3244,8 @@ let check_elf_nodump elf sdumps = >>> check_padding (* warn if some CompCert sections have been remapped by the linker script *) >>> warn_sections_remapping + (* warn if there exists non-empty overlapping sections *) + >>> check_overlaps >>> warn_sda_mapping (** Checks a whole ELF file according to .sdump files. diff --git a/checklink/ELF_parsers.ml b/checklink/ELF_parsers.ml index 776b7d9..8c2d486 100644 --- a/checklink/ELF_parsers.ml +++ b/checklink/ELF_parsers.ml @@ -257,43 +257,6 @@ let read_elf32_sym (e_hdr: elf32_ehdr) (symtab: bitstring) (strtab: bitstring) st_shndx = st_shndx ; } -(** 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 && - ( - let last x xsize = Int32.(sub (add x xsize) 1l) in - let alast = last a asize in - let blast = last b bsize in - let within (a, b) x = (a <= x) && (x <= b) in - (within (a, alast) b) || (within (b, blast) a) - ) - in - Array.iteri - (fun i ai -> - if ai.sh_type <> SHT_NOBITS - then - let ai_intersects = intersect ai.sh_offset ai.sh_size in - if - ai_intersects 0l 52l (* ELF header *) - || ai_intersects ehdr.e_phoff - (Int32.of_int (ehdr.e_phnum * ehdr.e_phentsize)) - || ai_intersects ehdr.e_shoff - (Int32.of_int (ehdr.e_shnum * ehdr.e_shentsize)) - then assert false - else - Array.iteri - (fun j aj -> - if - i <> j - && aj.sh_type <> SHT_NOBITS - && ai_intersects aj.sh_offset aj.sh_size - then assert false - ) - shdra - ) - shdra - (** Reads a whole ELF file from a bitstring *) let read_elf_bs (bs: bitstring): elf = let e_hdr = read_elf32_ehdr bs in @@ -312,7 +275,6 @@ let read_elf_bs (bs: bitstring): elf = let e_shdra = Array.init e_hdr.e_shnum (read_elf32_shdr e_hdr bs strtab) in - check_overlaps e_shdra e_hdr; let symtab_sndx = section_ndx_by_name_noelf e_shdra ".symtab" in let e_symtab = ( let symtab_shdr = e_shdra.(symtab_sndx) in diff --git a/checklink/Library.ml b/checklink/Library.ml index f55d9de..0ce3bcd 100644 --- a/checklink/Library.ml +++ b/checklink/Library.ml @@ -43,6 +43,18 @@ let filter_err (l: 'a or_err list): string list = external id : 'a -> 'a = "%identity" +(** [a; a + 1; ... ; b - 1; b] *) +let list_ab (a: int) (b: int): int list = + let rec list_ab_aux a b res = + if b < a + then res + else list_ab_aux a (b - 1) (b :: res) + in list_ab_aux a b [] + +(** [0; 1; ...; n - 1] *) +let list_n (n: int): int list = + list_ab 0 (n - 1) + (** Checks for existence of an array element satisfying a condition, and returns its index if it exists. *) -- cgit v1.2.3