checklink/Check.ml: missing SDA addressing for store instructions.

powerpc/PrintAsm.ml: update Linux output (Csymbol_rel, SDA sections).
test/regression/sections.c: test for SDA and relative addressings.


git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@2571 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e

5 files changed, 217 insertions, 14 deletions

diff --git a/checklink/Check.ml b/checklink/Check.ml
index cc53f4e..a9a5f02 100644
--- a/checklink/Check.ml
+++ b/checklink/Check.ml
@@ -69,7 +69,7 @@ let check_st_bind atom (sym: elf32_sym): s_framework -> s_framework =
 let name_of_section_Linux: section_name -> string = function
 | Section_text -> ".text"
 | Section_data i -> if i then ".data" else "COMM"
-| Section_small_data i -> if i then ".sdata" else "COMM"
+| Section_small_data i -> if i then ".sdata" else ".sbss"
 | Section_const -> ".rodata"
 | Section_small_const -> ".sdata2"
 | Section_string -> ".rodata"
@@ -1936,6 +1936,15 @@ let rec compare_code ccode ecode pc: checker = fun fw ->
               >>= recur_simpl
           | _ -> error
           end
+      | Pstb(rd, Csymbol_sda(ident, ofs), r1) ->
+          begin match ecode with
+          | STB(rS, rA, d) :: es ->
+              OK(fw)
+              >>= match_iregs rd  rS
+              >>= check_sda ident ofs rA (exts d)
+              >>= recur_simpl
+          | _ -> error
+          end
       | Pstb(rd, cst, r1) ->
           begin match ecode with
           | STB(rS, rA, d) :: es ->
@@ -1956,6 +1965,15 @@ let rec compare_code ccode ecode pc: checker = fun fw ->
               >>= recur_simpl
           | _ -> error
           end
+      | Pstfd(rd, Csymbol_sda(ident, ofs), r1) ->
+          begin match ecode with
+          | STFD(frS, rA, d) :: es ->
+              OK(fw)
+              >>= match_fregs rd  frS
+              >>= check_sda ident ofs rA (exts d)
+              >>= recur_simpl
+          | _ -> error
+          end
       | Pstfd(rd, cst, r1) | Pstfd_a(rd, cst, r1) ->
           begin match ecode with
           | STFD(frS, rA, d) :: es ->
@@ -1986,6 +2004,15 @@ let rec compare_code ccode ecode pc: checker = fun fw ->
               >>= recur_simpl
           | _ -> error
           end
+      | Pstfs(rd, Csymbol_sda(ident, ofs), r1) ->
+          begin match ecode with
+          | STFS(frS, rA, d) :: es ->
+              OK(fw)
+              >>= match_fregs rd  frS
+              >>= check_sda ident ofs rA (exts d)
+              >>= recur_simpl
+          | _ -> error
+          end
       | Pstfs(rd, cst, r1) ->
           begin match ecode with
           | STFS(frS, rA, d) :: es ->
@@ -2006,6 +2033,15 @@ let rec compare_code ccode ecode pc: checker = fun fw ->
               >>= recur_simpl
           | _ -> error
           end
+      | Psth(rd, Csymbol_sda(ident, ofs),  r1) ->
+          begin match ecode with
+          | STH(rS, rA, d) :: es ->
+              OK(fw)
+              >>= match_iregs rd  rS
+              >>= check_sda ident ofs rA (exts d)
+              >>= recur_simpl
+          | _ -> error
+          end
       | Psth(rd, cst, r1) ->
           begin match ecode with
           | STH(rS, rA, d) :: es ->
@@ -2036,6 +2072,15 @@ let rec compare_code ccode ecode pc: checker = fun fw ->
               >>= recur_simpl
           | _ -> error
           end
+      | Pstw(rd, Csymbol_sda(ident, ofs), r1) ->
+          begin match ecode with
+          | STW(rS, rA, d) :: es ->
+              OK(fw)
+              >>= match_iregs rd  rS
+              >>= check_sda ident ofs rA (exts d)
+              >>= recur_simpl
+          | _ -> error
+          end
       | Pstw(rd, cst, r1) | Pstw_a(rd, cst, r1) ->
           begin match ecode with
           | STW(rS, rA, d) :: es ->
diff --git a/powerpc/PrintAsm.ml b/powerpc/PrintAsm.ml
index 691ecfb..0192747 100644
--- a/powerpc/PrintAsm.ml
+++ b/powerpc/PrintAsm.ml
@@ -77,25 +77,30 @@ let comment =
   | Linux -> "#"
   | Diab -> ";"
 
+let symbol_fragment oc s n op =
+      fprintf oc "(%a)%s" symbol_offset (s, camlint_of_coqint n) op
+
 let constant oc cst =
   match cst with
   | Cint n ->
       fprintf oc "%ld" (camlint_of_coqint n)
   | Csymbol_low(s, n) ->
-      fprintf oc "(%a)@l" symbol_offset (s, camlint_of_coqint n)
+      symbol_fragment oc s n "@l"
   | Csymbol_high(s, n) ->
-      fprintf oc "(%a)@ha" symbol_offset (s, camlint_of_coqint n)
+      symbol_fragment oc s n "@ha"
   | Csymbol_sda(s, n) ->
-      begin match target with
-      | Linux ->
-          fprintf oc "(%a)@sda21" symbol_offset (s, camlint_of_coqint n)
-      | Diab ->
-          fprintf oc "(%a)@sdarx" symbol_offset (s, camlint_of_coqint n)
-      end
+      symbol_fragment oc s n
+        (match target with Linux -> "@sda21" | Diab  -> "@sdarx")
+  (* 32-bit relative addressing is supported by the Diab tools but not by
+     GNU binutils.  In the latter case, for testing purposes, we treat
+     them as absolute addressings.  The default base register being GPR0,
+     this produces correct code, albeit with absolute addresses. *)
   | Csymbol_rel_low(s, n) ->
-      fprintf oc "(%a)@sdax@l" symbol_offset (s, camlint_of_coqint n)
+      symbol_fragment oc s n
+        (match target with Linux -> "@l" | Diab  -> "@sdax@l")
   | Csymbol_rel_high(s, n) ->
-      fprintf oc "(%a)@sdarx@ha" symbol_offset (s, camlint_of_coqint n)
+      symbol_fragment oc s n
+        (match target with Linux -> "@ha" | Diab -> "@sdarx@ha")
 
 let num_crbit = function
   | CRbit_0 -> 0
@@ -159,9 +164,12 @@ let preg oc = function
 let name_of_section_Linux = function
   | Section_text -> ".text"
   | Section_data i -> if i then ".data" else "COMM"
-  | Section_small_data i -> if i then ".sdata" else "COMM"
+  | Section_small_data i -> 
+      if i
+      then ".section	.sdata,\"aw\",@progbits"
+      else ".section	.sbss,\"aw\",@progbits"
   | Section_const -> ".rodata"
-  | Section_small_const -> ".sdata2"
+  | Section_small_const -> ".section	.sdata2,\"a\",@progbits"
   | Section_string -> ".rodata"
   | Section_literal -> ".section	.rodata.cst8,\"aM\",@progbits,8"
   | Section_jumptable -> ".text"
diff --git a/test/regression/Makefile b/test/regression/Makefile
index 4cf9470..bd99675 100644
--- a/test/regression/Makefile
+++ b/test/regression/Makefile
@@ -23,7 +23,7 @@ TESTS=int32 int64 floats floats-basics \
 TESTS_COMP=attribs1 bitfields1 bitfields2 bitfields3 bitfields4 \
   bitfields5 bitfields6 bitfields7 bitfields8 \
   builtins-$(ARCH) packedstruct1 packedstruct2 alignas \
-  varargs1 varargs2
+  varargs1 varargs2 sections
 
 # Can run, both in compiled mode and in interpreter mode,
 # but produce processor-dependent results, so no reference output in Results
diff --git a/test/regression/Results/sections b/test/regression/Results/sections
new file mode 100644
index 0000000..540a839
--- /dev/null
+++ b/test/regression/Results/sections
@@ -0,0 +1,75 @@
+---- Absolute addressing
+signed char 1: OK
+signed char 2: OK
+signed char 3: OK
+unsigned char 1: OK
+unsigned char 2: OK
+unsigned char 3: OK
+signed short 1: OK
+signed short 2: OK
+signed short 3: OK
+unsigned short 1: OK
+unsigned short 2: OK
+unsigned short 3: OK
+int 1: OK
+int 2: OK
+int 3: OK
+float 1: OK
+float 2: OK
+float 3: OK
+double 1: OK
+double 2: OK
+double 3: OK
+long long 1: OK
+long long 2: OK
+long long 3: OK
+---- Small data area
+signed char 1: OK
+signed char 2: OK
+signed char 3: OK
+unsigned char 1: OK
+unsigned char 2: OK
+unsigned char 3: OK
+signed short 1: OK
+signed short 2: OK
+signed short 3: OK
+unsigned short 1: OK
+unsigned short 2: OK
+unsigned short 3: OK
+int 1: OK
+int 2: OK
+int 3: OK
+float 1: OK
+float 2: OK
+float 3: OK
+double 1: OK
+double 2: OK
+double 3: OK
+long long 1: OK
+long long 2: OK
+long long 3: OK
+---- Relative addressing
+signed char 1: OK
+signed char 2: OK
+signed char 3: OK
+unsigned char 1: OK
+unsigned char 2: OK
+unsigned char 3: OK
+signed short 1: OK
+signed short 2: OK
+signed short 3: OK
+unsigned short 1: OK
+unsigned short 2: OK
+unsigned short 3: OK
+int 1: OK
+int 2: OK
+int 3: OK
+float 1: OK
+float 2: OK
+float 3: OK
+double 1: OK
+double 2: OK
+double 3: OK
+long long 1: OK
+long long 2: OK
+long long 3: OK
diff --git a/test/regression/sections.c b/test/regression/sections.c
new file mode 100644
index 0000000..2e0e4e7
--- /dev/null
+++ b/test/regression/sections.c
@@ -0,0 +1,75 @@
+#include <stdio.h>
+
+/* Testing accesses to small data area and relative addressing sections */
+
+struct s {
+  signed char sc;
+  unsigned char uc;
+  signed short ss;
+  unsigned short us;
+  int i;
+  float f;
+  double d;
+  long long ll;
+};
+
+struct s x;                     /* normal absolute addressing */
+
+#pragma use_section SDATA y
+struct s y;                     /* small data area */
+
+#pragma section MYDATA ".mydata" ".mydata" far-data RW
+#pragma use_section MYDATA z
+struct s z;                     /* far data area, relative addressing */
+
+#define TEST(msg,ty,x,v1,v2,v3)                                    \
+  x = v1;                                                          \
+  __builtin_membar();                                              \
+  printf("%s 1: %s\n", msg, x == v1 ? "OK" : "FAILED");            \
+  *((volatile ty *) &x) = v2;                                      \
+  printf("%s 2: %s\n", msg, x == v2 ? "OK" : "FAILED");            \
+  x = v3;                                                          \
+  printf("%s 3: %s\n", msg, *((volatile ty *) &x) == v3 ? "OK" : "FAILED");
+
+/* This function must be inlined so that global addressing modes are 
+   generated */
+
+static inline void test(struct s * p)
+{
+  TEST("signed char", signed char, p->sc, 12, 34, 56);
+  TEST("unsigned char", unsigned char, p->uc, 56, 78, 123);
+  TEST("signed short", signed short, p->ss, 1234, 5678, 9999);
+  TEST("unsigned short", unsigned short, p->us, 1357, 2468, 3939);
+  TEST("int", int, p->i, 0x123456, 0x7890AB, 0xDEADBEEF);
+  TEST("float", float, p->f, 0.5f, 256.0f, 16.0f);
+  TEST("double", double, p->d, 3.1415, 2.718, 0.747);
+  TEST("long long", long long, p->ll, 
+       0x123456789ABCDEFLL, 0x789ABCDEF1234567LL,
+       0x128934AB56CD70EFLL);
+}
+
+void absolute(void)
+{
+  printf("---- Absolute addressing\n");
+  test(&x);
+}
+
+void sda(void)
+{
+  printf("---- Small data area\n");
+  test(&y);
+}
+
+void relative(void)
+{
+  printf("---- Relative addressing\n");
+  test(&z);
+}
+
+int main(void)
+{
+  absolute();
+  sda();
+  relative();
+  return 0;
+}