From 5b99eec6f36dbac9d59d519cc58ce37dd6251abe Mon Sep 17 00:00:00 2001 From: varobert Date: Thu, 12 Jul 2012 14:57:51 +0000 Subject: checklink: simplifications git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@1973 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e --- checklink/Check.ml | 119 ++++++++++++++++++++++++++---------------------- checklink/Frameworks.ml | 21 ++++----- 2 files changed, 73 insertions(+), 67 deletions(-) (limited to 'checklink') diff --git a/checklink/Check.ml b/checklink/Check.ml index dc9f153..dff9f8f 100644 --- a/checklink/Check.ml +++ b/checklink/Check.ml @@ -106,17 +106,19 @@ let match_sections_name = let c_name = name_of_section c_section in try - let res = StringMap.find c_name sfw.ef.section_map in - let expected = from_inferrable res in + let (value, conflicts) = StringMap.find c_name sfw.ef.section_map in + let expected = from_inferrable value in if e_name = expected then sfw else ( sfw - >>> (sf_ef |-- section_map) ^%= StringMap.add c_name (add_failure e_name res) + >>> (sf_ef |-- section_map) ^%= + StringMap.add c_name (value, StringSet.add e_name conflicts) ) with Not_found -> ( sfw - >>> (sf_ef |-- section_map) ^%= StringMap.add c_name (Inferred(e_name, [])) + >>> (sf_ef |-- section_map) ^%= + StringMap.add c_name (Inferred(e_name), StringSet.empty) ) (** Checks the symbol table entry of the function symbol number [sym_ndx], @@ -788,32 +790,47 @@ let match_bo_ctr bo: checker = fun ffw -> | { true:1; false:1; true:1; false:1; false:1 } -> OK(ffw) | { _ } -> ERR("match_bo_ctr") +(** Checks whether it is feasible that the position at offset [ofs] from the + CompCert symbol [ident] is situated at a relative address [addr] from + the SDA register [r]. This means that the following equation must hold: + [r] + addr = @ident + ofs + This allows us to determine what address [r] has to contain. If it is the + first such guess or if it matches previous expectations, it's fine. + Otherwise, there is a conflict that is reported in sda_map. +*) let check_sda ident ofs r addr ffw: f_framework or_err = let ofs = z_int32 ofs in - let check_sda_aux ndx: f_framework or_err = + let check_sda_aux ndx: (int * f_framework) or_err = let elf = ffw.sf.ef.elf in let sym = elf.e_symtab.(ndx) in let expected_addr = Safe32.(sym.st_value + ofs - addr) in try let r_addr = from_inferrable (IntMap.find r ffw.sf.ef.sda_map) in if r_addr = expected_addr - then OK(ffw) + then OK(ndx, ffw) else ERR( Printf.sprintf "SDA register %d is expected to point both at 0x%lx and 0x%lx" r r_addr expected_addr ) with Not_found -> - OK( - ffw >>> (ff_ef |-- sda_map) ^%= IntMap.add r (Inferred(expected_addr, [])) + OK(ndx, + ffw >>> (ff_ef |-- sda_map) ^%= IntMap.add r (Inferred(expected_addr)) ) in + (* We might not know yet what symbols is the one for that ident *) let sym_list = PosMap.find ident ffw.sf.ident_to_sym_ndx in + (* So we test all the candidates *) let res = List.map check_sda_aux sym_list in + (* For now, we hope at most one matches *) match filter_ok res with | [] -> ERR("No satisfying SDA mapping, errors were: " ^ string_of_list id ", " (filter_err res)) - | [ffw] -> OK(ffw) + | [(ndx, ffw)] -> OK( + ffw + (* We instantiate the relationship for that ident to the matching symbol *) + >>> (ff_sf |-- ident_to_sym_ndx) ^%= PosMap.add ident [ndx] + ) | _ -> fatal "Multiple possible SDA mappings, please report." (** Compares a whole CompCert function code against an ELF code, starting at @@ -3153,34 +3170,43 @@ let check_sym_tab_zero efw = let warn_sections_remapping efw = print_debug "Checking remapped sections"; StringMap.fold - (fun c_name e_name efw -> - match e_name with - | Provided(_, []) -> efw - | Provided(e_name, conflicts) -> - efw - >>> add_log (ERROR( - Printf.sprintf " + (fun c_name (e_name, conflicts) efw -> + if StringSet.is_empty conflicts + then + match e_name with + | Provided(e_name) -> + efw + | Inferred(e_name) -> + if c_name = e_name + then efw + else + begin + efw + >>> add_log (WARNING( + Printf.sprintf + "Detected linker script remapping: section %S -> %S" + c_name e_name + )) + end + else (* conflicts not empty *) + match e_name with + | Provided(e_name) -> + efw + >>> add_log (ERROR( + Printf.sprintf " Conflicting remappings for section %s: Specified: %s Expected: %s" - c_name e_name (string_of_list id ", " conflicts) - )) - | Inferred(e_name, []) when c_name = e_name -> efw - | Inferred(e_name, []) -> - efw - >>> add_log (WARNING( - Printf.sprintf - "Detected linker script remapping: section %S -> %S" - c_name e_name - )) - | Inferred(e_name, conflicts) -> - efw - >>> add_log (ERROR( - Printf.sprintf " + c_name e_name (string_of_list id ", " (StringSet.elements conflicts)) + )) + | Inferred(e_name) -> + efw + >>> add_log (ERROR( + Printf.sprintf " Conflicting remappings for section %s: %s" - c_name (string_of_list id ", " (e_name :: conflicts)) - )) + c_name (string_of_list id ", " (e_name :: (StringSet.elements conflicts))) + )) ) efw.section_map efw @@ -3193,30 +3219,13 @@ let warn_sda_mapping efw = IntMap.fold (fun r vaddr efw -> match vaddr with - | Provided(_, []) -> efw - | Provided(vaddr, conflicts) -> - efw - >>> add_log (ERROR( - Printf.sprintf " - Conflicting SDA mappings for register r%u: - Specified: 0x%lX - Expected: %s" - r vaddr (string_of_list (Printf.sprintf "0x%lX") ", " conflicts) - )) - | Inferred(vaddr, []) -> + | Provided(_) -> efw + | Inferred(vaddr) -> efw >>> add_log (WARNING( Printf.sprintf - "SDA register mapping: register r%u = 0x%lX" + "This SDA register mapping was inferred: register r%u = 0x%lX" r vaddr )) - | Inferred(vaddr, conflicts) -> - efw - >>> add_log (ERROR( - Printf.sprintf " - Conflicting SDA mappings for register r%u: - %s" - r (string_of_list (Printf.sprintf "0x%lX") ", " (vaddr :: conflicts)) - )) ) efw.sda_map efw @@ -3404,7 +3413,9 @@ let parse_conf filename = sfrom ) else - section_map := StringMap.add sfrom (Provided(sto, [])) !section_map) + section_map := + StringMap.add sfrom (Provided(sto), StringSet.empty) !section_map + ) ) (* a SDA mapping *) ; (fun () -> @@ -3418,7 +3429,7 @@ let parse_conf filename = r ) else - sda_map := IntMap.add r (Provided(addr, [])) !sda_map) + sda_map := IntMap.add r (Provided(addr)) !sda_map) ) (* a list of symbols supposed to be missing from the .sdump files *) ; (fun () -> diff --git a/checklink/Frameworks.ml b/checklink/Frameworks.ml index c448734..92f110c 100644 --- a/checklink/Frameworks.ml +++ b/checklink/Frameworks.ml @@ -31,20 +31,14 @@ type byte_chunk_desc = let add_uniq x l = if List.mem x l then l else x :: l (* This type specifies whether its argument was inferred by the tool or provided - via a config file, and lists the conflicts that were detected by the tool in - the right component of the pair. This allows us to report every conflict once - rather than at every occurence of a conflict. *) + via a config file. *) type 'a inferrable = - | Inferred of 'a * 'a list - | Provided of 'a * 'a list - -let add_failure failure = function -| Inferred(x, failures) -> Inferred(x, add_uniq failure failures) -| Provided(x, failures) -> Provided(x, add_uniq failure failures) + | Inferred of 'a + | Provided of 'a let from_inferrable = function -| Inferred(x, _) -> x -| Provided(x, _) -> x +| Inferred(x) -> x +| Provided(x) -> x (** This framework is carried along while analyzing the whole ELF file. *) @@ -59,8 +53,9 @@ type e_framework = { chkd_data_syms: bool array; (** The mapping from CompCert sections to ELF sections will be inferred along the way. This way, we can check things without prior knowledge of the - linker script. *) - section_map: (string inferrable) StringMap.t; + linker script. The set holds conflicts for the mapping, if more than one + mapping is inferred. These are reported once, at the end. *) + section_map: (string inferrable * StringSet.t) StringMap.t; (** We will assign a virtual address to each register that can act as an SDA base register. *) sda_map: (int32 inferrable) IntMap.t; -- cgit v1.2.3