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

1 files changed, 22 insertions, 6 deletions

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 ->