From 71a8a9586078c0132aa326a8c7968d38fe25a78d Mon Sep 17 00:00:00 2001 From: xleroy Date: Mon, 18 Aug 2014 12:34:43 +0000 Subject: powerpc/Asm: simplify the modeling of Csymbol_low and Csymbol_high. powerpc/Asmgen*: simplify the code generated for far-data relative accesses, so that the only occurrences of Csymbol_rel_{low,high} are in the pattern Paddis(r, GPR0, Csymbol_rel_high...); Paddi(r, r, Csymbol_rel_low...) checklink/Check.ml: check the pattern above. git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@2569 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e --- checklink/Check.ml | 28 ++++++++++++++++++++++------ 1 file changed, 22 insertions(+), 6 deletions(-) (limited to 'checklink') diff --git a/checklink/Check.ml b/checklink/Check.ml index 7eb3ea3..cc53f4e 100644 --- a/checklink/Check.ml +++ b/checklink/Check.ml @@ -415,13 +415,12 @@ let match_csts (cc: constant) (ec: int32): checker = fun ffw -> end | Csymbol_sda (ident, i) -> (* sda should be handled separately in places it occurs *) - fatal "Unhandled Csymbol_sda, please report." + ERR("Incorrect reference to near-data symbol " + ^ Hashtbl.find ffw.sf.ident_to_name ident) | Csymbol_rel_low (ident, i) | Csymbol_rel_high (ident, i) -> - (* not checked yet *) - OK((ff_ef ^%= - (add_log (WARNING("Cannot check access to far-data symbol " ^ - Hashtbl.find ffw.sf.ident_to_name ident)))) - ffw) + (* should be handled separately in places it occurs *) + ERR("Incorrect reference to far-data symbol " + ^ Hashtbl.find ffw.sf.ident_to_name ident) let match_z_int32 (cz: Z.t) (ei: int32) = let cz = z_int32 cz in @@ -738,6 +737,23 @@ let rec compare_code ccode ecode pc: checker = fun fw -> >>= recur_simpl | _ -> error end + | Paddis(rd, r1, Csymbol_rel_high(id, ofs)) -> + begin match cs with + | Paddi(rd', r1', Csymbol_rel_low(id', ofs')) :: cs + when id' = id && ofs' = ofs -> + begin match ecode with + | ADDIS(rD, rA, simm) :: ADDI(rD', rA', simm') :: es -> + OK(fw) + >>= match_iregs rd rD + >>= match_iregs r1' rA' + >>= match_iregs rd' rD' + >>= check_sda id ofs rA + Int32.(add (shift_left (of_int simm) 16) (exts simm')) + >>= compare_code cs es (Int32.add 8l pc) + | _ -> error + end + | _ -> error + end | Paddis(rd, r1, cst) -> begin match ecode with | ADDIS(rD, rA, simm) :: es -> -- cgit v1.2.3