summaryrefslogtreecommitdiff
path: root/checklink
diff options
context:
space:
mode:
Diffstat (limited to 'checklink')
-rw-r--r--checklink/Check.ml165
-rw-r--r--checklink/Frameworks.ml8
2 files changed, 33 insertions, 140 deletions
diff --git a/checklink/Check.ml b/checklink/Check.ml
index c51e090..8e8afd1 100644
--- a/checklink/Check.ml
+++ b/checklink/Check.ml
@@ -195,13 +195,10 @@ let mark_covered_fun_sym_ndx (ndx: int) ffw: f_framework =
)
>>> (ff_sf ^%= check_fun_symtab ffw.this_ident ndx)
-(** Taken from CompCert *)
-let re_variadic_stub: Str.regexp = Str.regexp "\\(.*\\)\\$[if]*$"
-
(** Tries to refine the mapping for key [k] in [ident_to_sym_ndx] so that it is
mapped to [vaddr]. Fails if no symbol in [k]'s mapping has that virtual
- address, unless the symbol is a stub from CompCert. Otherwise, it filters
- out all symbols whose virtual address does not match [vaddr].
+ address. Otherwise, it filters out all symbols whose virtual
+ address does not match [vaddr].
*)
let idmap_unify (k: P.t) (vaddr: int32) (sfw: s_framework)
: s_framework or_err =
@@ -215,39 +212,16 @@ let idmap_unify (k: P.t) (vaddr: int32) (sfw: s_framework)
with
| [] ->
(* no symbol has that virtual address *)
- let ident_name = Hashtbl.find sfw.ident_to_name k in
- if Str.string_match re_variadic_stub ident_name 0
- then (* this ident needs a stub, whose address is [vaddr] *)
- try (
- (* fetch the registered virtual address for this stub *)
- let v = PosMap.find k sfw.stub_ident_to_vaddr in
- (* if there is one, we're good if it's the same as [vaddr] *)
- if vaddr = v
- then OK(sfw)
- else ERR(
- Printf.sprintf
- "Incoherent constraints for stub: %s"
- (Hashtbl.find sfw.ident_to_name k)
- )
- )
- with Not_found ->
- (* if the stub has no previously registered virtual address,
- register [vaddr] *)
- OK(
- sfw
- >>> (stub_ident_to_vaddr ^%= PosMap.add k vaddr)
+ ERR(
+ Printf.sprintf
+ "Incoherent constraints for ident %s with value %s and candidates [%s]"
+ (Hashtbl.find sfw.ident_to_name k)
+ (string_of_int32 vaddr)
+ (string_of_list
+ (fun ndx -> string_of_int32 sfw.ef.elf.e_symtab.(ndx).st_value)
+ ", " id_ndxes
)
- else (* not a stub, so this is a real error *)
- ERR(
- Printf.sprintf
- "Incoherent constraints for ident %s with value %s and candidates [%s]"
- (Hashtbl.find sfw.ident_to_name k)
- (string_of_int32 vaddr)
- (string_of_list
- (fun ndx -> string_of_int32 sfw.ef.elf.e_symtab.(ndx).st_value)
- ", " id_ndxes
- )
- )
+ )
| ndxes ->
if id_ndxes = ndxes
then OK(sfw)
@@ -595,6 +569,20 @@ let rec match_jmptbl lbllist vaddr size ffw =
end
end
+(** Matches [ecode] against the expected CR6 magic before a function call.
+*)
+let match_set_cr6 sg ecode =
+ if sg.sig_cc.cc_vararg then
+ if List.mem Tfloat sg.sig_args then
+ match ecode with
+ | CREQV(6, 6, 6) :: ecode' -> Some ecode'
+ | _ -> None
+ else
+ match ecode with
+ | CRXOR(6, 6, 6) :: ecode' -> Some ecode'
+ | _ -> None
+ else Some ecode
+
(** Matches [ecode] agains the expected code for a small memory copy
pseudo-instruction. Returns a triple containing the updated framework,
the remaining ELF code, and the updated program counter.
@@ -1022,8 +1010,8 @@ let rec compare_code ccode ecode pc: checker = fun fw ->
| _ -> error
end
| Pbctr sg ->
- begin match ecode with
- | BCCTRx(bo, bi, lk) :: es ->
+ begin match match_set_cr6 sg ecode with
+ | Some(BCCTRx(bo, bi, lk) :: es) ->
OK(fw)
>>= match_bo_ctr bo
>>= match_ints 0 bi
@@ -1032,8 +1020,8 @@ let rec compare_code ccode ecode pc: checker = fun fw ->
| _ -> error
end
| Pbctrl sg ->
- begin match ecode with
- | BCCTRx(bo, bi, lk) :: es ->
+ begin match match_set_cr6 sg ecode with
+ | Some(BCCTRx(bo, bi, lk) :: es) ->
OK(fw)
>>= match_bo_ctr bo
>>= match_ints 0 bi
@@ -1070,8 +1058,8 @@ let rec compare_code ccode ecode pc: checker = fun fw ->
| _ -> error
end
| Pbl(ident, sg) ->
- begin match ecode with
- | Bx(li, aa, lk) :: es ->
+ begin match match_set_cr6 sg ecode with
+ | Some(Bx(li, aa, lk) :: es) ->
let dest = Int32.(add pc (mul 4l (exts li))) in
OK(fw)
>>= (ff_sf ^%=? idmap_unify ident dest)
@@ -1091,8 +1079,8 @@ let rec compare_code ccode ecode pc: checker = fun fw ->
| _ -> error
end
| Pbs(ident, sg) ->
- begin match ecode with
- | Bx(li, aa, lk) :: es ->
+ begin match match_set_cr6 sg ecode with
+ | Some(Bx(li, aa, lk) :: es) ->
let dest = Int32.(add pc (mul 4l (exts li))) in
OK(fw)
>>= match_bools false aa
@@ -2911,87 +2899,6 @@ let check_data (pv: (ident * unit globvar) list) (sfw: s_framework)
(* Empty lists mean the symbol is external, no need for check *)
(List.filter (fun (_, gv) -> gv.gvar_init <> []) pv)
-(** Checks that everything that has been assimiled as a stub during checks
- indeed looks like a stub.
-*)
-let check_stubs sfw =
- let check cond msg sfw =
- sfw
- >>> (if cond then id else (sf_ef ^%= add_log (ERROR(msg))))
- in
- let check_eq msg a b = check (a = b) msg in
- let match_bools = check_eq "match_bools" in
- let match_ints = check_eq "match_ints" in
- let check_stub ident vaddr sfw =
- let fundef = List.find (fun (i, _) -> i = ident) sfw.program.prog_defs in
- let elf = sfw.ef.elf in
- let stub_ecode = from_some (code_at_vaddr elf vaddr 2) in
- let stub_offset = from_some (physical_offset_of_vaddr elf vaddr) in
- begin match fundef with
- | (_, Gfun(External(EF_external(dest_ident, _) as ef))) ->
- let args = (ef_sig ef).sig_args in
- if List.mem Tfloat args
- then
- begin match stub_ecode with
- | CREQV(crbD, crbA, crbB) :: (* vaddr *)
- Bx(li, aa, lk) :: (* vaddr + 4 *)
- [] ->
- let dest_vaddr = Int32.(add (add vaddr 4l) (mul 4l (exts li))) in
- begin match idmap_unify dest_ident dest_vaddr sfw with
- | ERR(s) ->
- sfw
- >>> (sf_ef ^%= add_log (ERROR(
- "Couldn't match stub, " ^ s
- )))
- | OK(sfw) ->
- sfw
- >>> match_ints 6 crbD
- >>> match_ints 6 crbA
- >>> match_ints 6 crbB
- >>> match_bools false aa
- >>> match_bools false lk
- >>> (sf_ef ^%=
- add_range stub_offset 8l 4
- (Stub(Hashtbl.find sfw.ident_to_name ident))
- )
- end
- | _ ->
- sfw
- >>> (sf_ef ^%= add_log (ERROR("Couldn't match stub")))
- end
- else
- begin match stub_ecode with
- | CRXOR(crbD, crbA, crbB) :: (* vaddr *)
- Bx(li, aa, lk) :: (* vaddr + 4 *)
- [] ->
- let dest_vaddr = Int32.(add (add vaddr 4l) (mul 4l (exts li))) in
- begin match idmap_unify dest_ident dest_vaddr sfw with
- | ERR(s) ->
- sfw
- >>> (sf_ef ^%= add_log (ERROR(
- "Couldn't match stub, " ^ s
- )))
- | OK(sfw) ->
- sfw
- >>> match_ints 6 crbD
- >>> match_ints 6 crbA
- >>> match_ints 6 crbB
- >>> match_bools false aa
- >>> match_bools false lk
- >>> (sf_ef ^%=
- add_range stub_offset 8l 4
- (Stub(Hashtbl.find sfw.ident_to_name ident))
- )
- end
- | _ ->
- sfw
- >>> (sf_ef ^%= add_log (ERROR("Couldn't match stub")))
- end
- | _ -> fatal "Unexpected fundef in check_stubs, please report."
- end
- in
- PosMap.fold check_stub sfw.stub_ident_to_vaddr sfw
-
(** Read a .sdump file *)
let sdump_magic_number = "CompCertSDUMP" ^ Configuration.version
@@ -3065,17 +2972,11 @@ let process_sdump efw sdump: e_framework =
; program = prog
; ident_to_name = names
; ident_to_sym_ndx = ident_to_sym_ndx
- ; stub_ident_to_vaddr = PosMap.empty
; atoms = atoms
}
)
>>> worklist_process wl
>>> (fun sfw ->
- print_debug "Checking stubs";
- sfw
- )
- >>> check_stubs
- >>> (fun sfw ->
print_debug "Checking data";
sfw
)
diff --git a/checklink/Frameworks.ml b/checklink/Frameworks.ml
index 35144dc..ec11412 100644
--- a/checklink/Frameworks.ml
+++ b/checklink/Frameworks.ml
@@ -84,9 +84,6 @@ type s_framework = {
as we learn more about the contents of the symbol.
*)
ident_to_sym_ndx: (int list) PosMap.t;
- (** CompCert generates stubs for some functions, which we will aggregate as we
- discover them. *)
- stub_ident_to_vaddr: int32 PosMap.t;
(** This structure is imported from CompCert's .sdump, and describes each
atom. *)
atoms: (ident, C2C.atom_info) Hashtbl.t;
@@ -140,11 +137,6 @@ let ident_to_sym_ndx = {
set = (fun i sf -> { sf with ident_to_sym_ndx = i });
}
-let stub_ident_to_vaddr = {
- get = (fun sf -> sf.stub_ident_to_vaddr);
- set = (fun i sf -> { sf with stub_ident_to_vaddr = i });
-}
-
(** Adds a range to the checked bytes list.
*)
let add_range (start: int32) (length: int32) (align: int) (bcd: byte_chunk_desc)