Preliminary support for small data area in PowerPC port.

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

9 files changed, 201 insertions, 96 deletions

diff --git a/cfrontend/Cil2Csyntax.ml b/cfrontend/Cil2Csyntax.ml
index b8a88de..20a5b7a 100644
--- a/cfrontend/Cil2Csyntax.ml
+++ b/cfrontend/Cil2Csyntax.ml
@@ -1252,3 +1252,18 @@ let atom_is_readonly a =
   with Not_found ->
     false
 
+let atom_is_small_data a ofs =
+  match Configuration.system with
+  | "linux" ->
+      if !Clflags.option_fsda then begin
+        try
+          let v = Hashtbl.find varinfo_atom a in
+          let sz = Cil.bitsSizeOf v.vtype / 8 in
+          let ofs = camlint_of_coqint ofs in
+          sz <= 8 && ofs >= 0l && ofs < Int32.of_int sz
+        with Not_found ->
+          false
+      end else
+        false
+  | _ ->
+      false
diff --git a/driver/Clflags.ml b/driver/Clflags.ml
index 08e4a53..81d4af3 100644
--- a/driver/Clflags.ml
+++ b/driver/Clflags.ml
@@ -17,6 +17,7 @@ let linker_options = ref ([]: string list)
 let exe_name = ref "a.out"
 let option_flonglong = ref false
 let option_fmadd = ref false
+let option_fsda = ref false
 let option_dclight = ref false
 let option_dasm = ref false
 let option_E = ref false
diff --git a/driver/Driver.ml b/driver/Driver.ml
index 30d4a6c..77f8b82 100644
--- a/driver/Driver.ml
+++ b/driver/Driver.ml
@@ -264,6 +264,7 @@ Preprocessing options:
 Compilation options:
   -flonglong     Treat 'long long' as 'long' and 'long double' as 'double'
   -fmadd         Use fused multiply-add and multiply-sub instructions
+  -fsda          Use small data area
   -dclight       Save generated Clight in <file>.light.c
   -dasm          Save generated assembly in <file>.s
 Linking options:
@@ -303,6 +304,10 @@ let rec parse_cmdline i =
       option_fmadd := true;
       parse_cmdline (i + 1)
     end else
+    if s = "-fsda" then begin
+      option_fsda := true;
+      parse_cmdline (i + 1)
+    end else
     if s = "-dclight" then begin
       option_dclight := true;
       parse_cmdline (i + 1)
diff --git a/extraction/extraction.v b/extraction/extraction.v
index 4eb107b..f8a159b 100644
--- a/extraction/extraction.v
+++ b/extraction/extraction.v
@@ -72,6 +72,9 @@ Extract Constant Linearize.enumerate_aux => "Linearizeaux.enumerate_aux".
 (* Asm *)
 Extract Constant Asm.low_half => "fun _ -> assert false".
 Extract Constant Asm.high_half => "fun _ -> assert false".
+Extract Constant Asm.symbol_is_small_data => "Cil2Csyntax.atom_is_small_data".
+Extract Constant Asm.small_data_area_base => "fun _ -> assert false".
+Extract Constant Asm.small_data_area_offset => "fun _ _ _ -> assert false".
 
 (* Suppression of stupidly big equality functions *)
 Extract Constant Op.eq_operation => "fun (x: operation) (y: operation) -> x = y".
diff --git a/powerpc/Asm.v b/powerpc/Asm.v
index ab70072..bea5f5c 100644
--- a/powerpc/Asm.v
+++ b/powerpc/Asm.v
@@ -57,16 +57,18 @@ Lemma freg_eq: forall (x y: freg), {x=y} + {x<>y}.
 Proof. decide equality. Defined.
 
 (** Symbolic constants.  Immediate operands to an arithmetic instruction
-  or an indexed memory access can be either integer literals
+  or an indexed memory access can be either integer literals,
   or the low or high 16 bits of a symbolic reference (the address
-  of a symbol plus a displacement).  These symbolic references are
+  of a symbol plus a displacement), or a 16-bit offset from the
+  small data area register.  These symbolic references are
   resolved later by the linker.
 *)
 
 Inductive constant: Type :=
   | Cint: int -> constant
   | Csymbol_low: ident -> int -> constant
-  | Csymbol_high: ident -> int -> constant.
+  | Csymbol_high: ident -> int -> constant
+  | Csymbol_sda: ident -> int -> constant.
 
 (** A note on constants: while immediate operands to PowerPC
   instructions must be representable in 16 bits (with
@@ -413,6 +415,19 @@ Axiom low_half_type:
 Axiom high_half_type: 
   forall v, Val.has_type (high_half v) Tint.
  
+(** The function below axiomatizes how the linker builds the
+  small data area. *)
+
+Parameter symbol_is_small_data: ident -> int -> bool.
+Parameter small_data_area_base: genv -> val.
+Parameter small_data_area_offset: genv -> ident -> int -> val.
+
+Axiom small_data_area_addressing:
+  forall id ofs,
+  symbol_is_small_data id ofs = true ->
+  Val.add (small_data_area_base ge) (small_data_area_offset ge id ofs) =
+  symbol_offset id ofs.
+
 (** Armed with the [low_half] and [high_half] functions,
   we can define the evaluation of a symbolic constant.
   Note that for [const_high], integer constants
@@ -426,6 +441,7 @@ Definition const_low (c: constant) :=
   | Cint n => Vint n
   | Csymbol_low id ofs => low_half (symbol_offset id ofs)
   | Csymbol_high id ofs => Vundef
+  | Csymbol_sda id ofs => small_data_area_offset ge id ofs
   end.
 
 Definition const_high (c: constant) :=
@@ -433,6 +449,7 @@ Definition const_high (c: constant) :=
   | Cint n => Vint (Int.shl n (Int.repr 16))
   | Csymbol_low id ofs => Vundef
   | Csymbol_high id ofs => high_half (symbol_offset id ofs)
+  | Csymbol_sda id ofs => Vundef
   end.
 
 (** The semantics is purely small-step and defined as a function
@@ -852,7 +869,8 @@ Inductive initial_state (p: program): state -> Prop :=
         (Pregmap.init Vundef)
         # PC <- (symbol_offset ge p.(prog_main) Int.zero)
         # LR <- Vzero
-        # GPR1 <- (Vptr Mem.nullptr Int.zero) in
+        # GPR1 <- (Vptr Mem.nullptr Int.zero)
+        # GPR13 <- (small_data_area_base ge) in
       initial_state p (State rs0 m0).
 
 Inductive final_state: state -> int -> Prop :=
diff --git a/powerpc/Asmgen.v b/powerpc/Asmgen.v
index 5c37a57..05381ea 100644
--- a/powerpc/Asmgen.v
+++ b/powerpc/Asmgen.v
@@ -395,8 +395,11 @@ Definition transl_load_store
   | Aindexed2, a1 :: a2 :: nil =>
       mk2 (ireg_of a1) (ireg_of a2) :: k
   | Aglobal symb ofs, nil =>
-      Paddis GPR12 GPR0 (Csymbol_high symb ofs) ::
-      mk1 (Csymbol_low symb ofs) GPR12 :: k
+      if symbol_is_small_data symb ofs then
+        mk1 (Csymbol_sda symb ofs) GPR13 :: k
+      else
+        Paddis GPR12 GPR0 (Csymbol_high symb ofs) ::
+        mk1 (Csymbol_low symb ofs) GPR12 :: k
   | Abased symb ofs, a1 :: nil =>
       if ireg_eq (ireg_of a1) GPR0 then
         Pmr GPR12 (ireg_of a1) ::
diff --git a/powerpc/Asmgenproof.v b/powerpc/Asmgenproof.v
index b4176f2..19e1782 100644
--- a/powerpc/Asmgenproof.v
+++ b/powerpc/Asmgenproof.v
@@ -483,7 +483,7 @@ Proof.
   case (Int.eq (high_s i) Int.zero). simpl; rewrite H; auto.
   simpl; rewrite H; auto.
   simpl; rewrite H0; auto.
-  simpl; rewrite H; auto.
+  destruct (symbol_is_small_data i i0); simpl; rewrite H; auto.
   case (ireg_eq (ireg_of m) GPR0); intro; simpl; rewrite H; auto. 
   case (Int.eq (high_s i) Int.zero); simpl; rewrite H; auto.
 Qed.
@@ -593,13 +593,13 @@ Inductive match_states: Machconcr.state -> Asm.state -> Prop :=
         (WTF: wt_function f)
         (INCL: incl c f.(fn_code))
         (AT: transl_code_at_pc (rs PC) fb f c)
-        (AG: agree ms sp rs),
+        (AG: agree tge ms sp rs),
       match_states (Machconcr.State s fb sp c ms m)
                    (Asm.State rs m)
   | match_states_call:
       forall s fb ms m rs
         (STACKS: match_stack s)
-        (AG: agree ms (parent_sp s) rs)
+        (AG: agree tge ms (parent_sp s) rs)
         (ATPC: rs PC = Vptr fb Int.zero)
         (ATLR: rs LR = parent_ra s),
       match_states (Machconcr.Callstate s fb ms m)
@@ -607,7 +607,7 @@ Inductive match_states: Machconcr.state -> Asm.state -> Prop :=
   | match_states_return:
       forall s ms m rs
         (STACKS: match_stack s)
-        (AG: agree ms (parent_sp s) rs)
+        (AG: agree tge ms (parent_sp s) rs)
         (ATPC: rs PC = parent_ra s),
       match_states (Machconcr.Returnstate s ms m)
                    (Asm.State rs m).
@@ -621,7 +621,7 @@ Lemma exec_straight_steps:
   transl_code_at_pc (rs1 PC) fb f c1 ->
   (exists rs2,
      exec_straight tge (transl_function f) (transl_code f c1) rs1 m1 (transl_code f c2) rs2 m2
-     /\ agree ms2 sp rs2) ->
+     /\ agree tge ms2 sp rs2) ->
   exists st',
   plus step tge (State rs1 m1) E0 st' /\
   match_states (Machconcr.State s fb sp c2 ms2 m2) st'.
@@ -683,7 +683,7 @@ Proof.
   unfold load_stack in H. 
   generalize (wt_function_instrs _ WTF _ (INCL _ (in_eq _ _))).
   intro WTI. inversion WTI.
-  rewrite (sp_val _ _ _ AG) in H.
+  rewrite (sp_val _ _ _ _ AG) in H.
   assert (NOTE: GPR1 <> GPR0). congruence.
   generalize (loadind_correct tge (transl_function f) GPR1 ofs ty
                 dst (transl_code f c) rs m v H H1 NOTE).
@@ -691,7 +691,7 @@ Proof.
   left; eapply exec_straight_steps; eauto with coqlib.
   simpl. exists rs2; split. auto. 
   apply agree_exten_2 with (rs#(preg_of dst) <- v).
-  auto with ppcgen. 
+  apply agree_set_mreg. auto. 
   intros. case (preg_eq r0 (preg_of dst)); intro.
   subst r0. rewrite Pregmap.gss. auto. 
   rewrite Pregmap.gso; auto.
@@ -709,8 +709,8 @@ Proof.
   unfold store_stack in H. 
   generalize (wt_function_instrs _ WTF _ (INCL _ (in_eq _ _))).
   intro WTI. inversion WTI.
-  rewrite (sp_val _ _ _ AG) in H.
-  rewrite (preg_val ms sp rs) in H; auto.
+  rewrite (sp_val _ _ _ _ AG) in H.
+  rewrite (preg_val tge ms sp rs) in H; auto.
   assert (NOTE: GPR1 <> GPR0). congruence.
   generalize (storeind_correct tge (transl_function f) GPR1 ofs ty
                 src (transl_code f c) rs m m' H H1 NOTE).
@@ -738,7 +738,7 @@ Proof.
                  (loadind GPR12 ofs ty dst (transl_code f c)) rs2 m).
   simpl. apply exec_straight_one.
   simpl. unfold load1. rewrite gpr_or_zero_not_zero; auto with ppcgen.
-  unfold const_low. rewrite <- (sp_val ms sp rs); auto.
+  unfold const_low. rewrite <- (sp_val tge ms sp rs); auto.
   unfold load_stack in H0. simpl chunk_of_type in H0. 
   rewrite H0. reflexivity. reflexivity.
   generalize (wt_function_instrs _ WTF _ (INCL _ (in_eq _ _))).
@@ -818,7 +818,7 @@ Proof.
   exists (nextinstr (rs2#(ireg_of dst) <- v)).
   split. eapply exec_straight_trans. eexact EX1.
   apply exec_straight_one. simpl. 
-  rewrite <- (ireg_val _ _ _ dst AG1);auto. rewrite Regmap.gss. 
+  rewrite <- (ireg_val _ _ _ _ dst AG1);auto. rewrite Regmap.gss. 
   rewrite EQ1. reflexivity. reflexivity. 
   eauto with ppcgen.
 Qed.
@@ -881,13 +881,13 @@ Proof.
     rewrite RA_EQ.
     change (rs3 LR) with (Val.add (Val.add (rs PC) Vone) Vone).
     rewrite <- H5. reflexivity. 
-  assert (AG3: agree ms sp rs3). 
+  assert (AG3: agree tge ms sp rs3). 
     unfold rs3, rs2; auto 8 with ppcgen.
   left; exists (State rs3 m); split.
   apply plus_left with E0 (State rs2 m) E0. 
     econstructor. eauto. apply functions_transl. eexact H0. 
     eapply find_instr_tail. eauto.
-    simpl. rewrite <- (ireg_val ms sp rs); auto. 
+    simpl. rewrite <- (ireg_val tge ms sp rs); auto. 
   apply star_one. econstructor.
     change (rs2 PC) with (Val.add (rs PC) Vone). rewrite <- H5.
     simpl. auto.
@@ -910,7 +910,7 @@ Proof.
     rewrite RA_EQ.
     change (rs2 LR) with (Val.add (rs PC) Vone).
     rewrite <- H5. reflexivity. 
-  assert (AG2: agree ms sp rs2). 
+  assert (AG2: agree tge ms sp rs2). 
     unfold rs2; auto 8 with ppcgen.
   left; exists (State rs2 m); split.
   apply plus_one. econstructor. 
@@ -953,16 +953,16 @@ Proof.
             (transl_code f (Mtailcall sig (inl ident m0) :: c)) rs m 
             (Pbctr :: transl_code f c) rs5 (free m stk)).
   simpl. apply exec_straight_step with rs2 m. 
-  simpl. rewrite <- (ireg_val _ _ _ _ AG H6). reflexivity. reflexivity.
+  simpl. rewrite <- (ireg_val _ _ _ _ _ AG H6). reflexivity. reflexivity.
   apply exec_straight_step with rs3 m.
   simpl. unfold load1. rewrite gpr_or_zero_not_zero. unfold const_low.
-  change (rs2 GPR1) with (rs GPR1). rewrite <- (sp_val _ _ _ AG). 
+  change (rs2 GPR1) with (rs GPR1). rewrite <- (sp_val _ _ _ _ AG). 
   simpl. unfold load_stack in H2. simpl in H2. rewrite H2.
   reflexivity. discriminate. reflexivity.
   apply exec_straight_step with rs4 m.
   simpl. reflexivity. reflexivity.
   apply exec_straight_one. 
-  simpl. change (rs4 GPR1) with (rs GPR1). rewrite <- (sp_val _ _ _ AG).
+  simpl. change (rs4 GPR1) with (rs GPR1). rewrite <- (sp_val _ _ _ _ AG).
   unfold load_stack in H1; simpl in H1. 
   simpl. rewrite H1. reflexivity. reflexivity.
   left; exists (State rs6 (free m stk)); split.
@@ -977,12 +977,12 @@ Proof.
   simpl. reflexivity. traceEq.
   (* match states *)
   econstructor; eauto.
-  assert (AG4: agree ms (Vptr stk soff) rs4).
+  assert (AG4: agree tge ms (Vptr stk soff) rs4).
     unfold rs4, rs3, rs2; auto 10 with ppcgen.
-  assert (AG5: agree ms (parent_sp s) rs5).
-    unfold rs5. apply agree_nextinstr.
-    split. reflexivity. intros. inv AG4. rewrite H12. 
-    rewrite Pregmap.gso; auto with ppcgen.
+  assert (AG5: agree tge ms (parent_sp s) rs5).
+    unfold rs5. apply agree_nextinstr. destruct AG4 as [X [Y Z]].
+    split. reflexivity. split. rewrite <- Y. reflexivity.
+    intros. rewrite Z. rewrite Pregmap.gso; auto with ppcgen.
   unfold rs6; auto with ppcgen.
   change (rs6 PC) with (ms m0). 
   generalize H. destruct (ms m0); try congruence.
@@ -997,13 +997,13 @@ Proof.
             (Pbs i :: transl_code f c) rs4 (free m stk)).
   simpl. apply exec_straight_step with rs2 m. 
   simpl. unfold load1. rewrite gpr_or_zero_not_zero. unfold const_low.
-  rewrite <- (sp_val _ _ _ AG). 
+  rewrite <- (sp_val _ _ _ _ AG). 
   simpl. unfold load_stack in H2. simpl in H2. rewrite H2.
   reflexivity. discriminate. reflexivity.
   apply exec_straight_step with rs3 m.
   simpl. reflexivity. reflexivity.
   apply exec_straight_one. 
-  simpl. change (rs3 GPR1) with (rs GPR1). rewrite <- (sp_val _ _ _ AG).
+  simpl. change (rs3 GPR1) with (rs GPR1). rewrite <- (sp_val _ _ _ _ AG).
   unfold load_stack in H1; simpl in H1.
   simpl. rewrite H1. reflexivity. reflexivity.
   left; exists (State rs5 (free m stk)); split.
@@ -1019,12 +1019,12 @@ Proof.
   reflexivity. traceEq.
   (* match states *)
   econstructor; eauto.
-  assert (AG3: agree ms (Vptr stk soff) rs3).
+  assert (AG3: agree tge ms (Vptr stk soff) rs3).
     unfold rs3, rs2; auto 10 with ppcgen.
-  assert (AG4: agree ms (parent_sp s) rs4).
-    unfold rs4. apply agree_nextinstr.
-    split. reflexivity. intros. inv AG3. rewrite H12. 
-    rewrite Pregmap.gso; auto with ppcgen.
+  assert (AG4: agree tge ms (parent_sp s) rs4).
+    unfold rs4. apply agree_nextinstr. destruct AG3 as [X [Y Z]].
+    split. reflexivity. split. rewrite <- Y. reflexivity.
+    intros. rewrite Z. rewrite Pregmap.gso; auto with ppcgen.
   unfold rs5; auto with ppcgen.
 Qed.
 
@@ -1148,10 +1148,10 @@ Proof.
   simpl. apply exec_straight_three with rs2 m rs3 m.
   simpl. unfold load1. rewrite gpr_or_zero_not_zero. unfold const_low.
   unfold load_stack in H1. simpl in H1. 
-  rewrite <- (sp_val _ _ _ AG). simpl. rewrite H1.
+  rewrite <- (sp_val _ _ _ _ AG). simpl. rewrite H1.
   reflexivity. discriminate.
   unfold rs3. change (parent_ra s) with rs2#GPR12. reflexivity.
-  simpl. change (rs3 GPR1) with (rs GPR1). rewrite <- (sp_val _ _ _ AG).
+  simpl. change (rs3 GPR1) with (rs GPR1). rewrite <- (sp_val _ _ _ _ AG).
   simpl. 
   unfold load_stack in H0. simpl in H0.
   rewrite H0. reflexivity.
@@ -1172,12 +1172,13 @@ Proof.
   reflexivity. traceEq.
   (* match states *)
   econstructor; eauto. 
-  assert (AG3: agree ms (Vptr stk soff) rs3). 
+  assert (AG3: agree tge ms (Vptr stk soff) rs3). 
     unfold rs3, rs2; auto 10 with ppcgen.
-  assert (AG4: agree ms (parent_sp s) rs4).
-    split. reflexivity. intros. unfold rs4. 
-    rewrite nextinstr_inv. rewrite Pregmap.gso.
-    elim AG3; auto. auto with ppcgen. auto with ppcgen.
+  assert (AG4: agree tge ms (parent_sp s) rs4).
+    destruct AG3 as [X [Y Z]].
+    split. reflexivity. split. rewrite <- Y; reflexivity.
+    intros. unfold rs4. rewrite nextinstr_inv. rewrite Pregmap.gso. auto. 
+    auto with ppcgen. auto with ppcgen.
   unfold rs5; auto with ppcgen.
 Qed.
 
@@ -1212,7 +1213,7 @@ Proof.
   apply exec_straight_three with rs2 m2 rs3 m2.
   unfold exec_instr. rewrite H0. fold sp.
   unfold store_stack in H1. simpl chunk_of_type in H1. 
-  rewrite <- (sp_val _ _ _ AG). rewrite H1. reflexivity.
+  rewrite <- (sp_val _ _ _ _ AG). rewrite H1. reflexivity.
   simpl. change (rs2 LR) with (rs LR). rewrite ATLR. reflexivity.
   simpl. unfold store1. rewrite gpr_or_zero_not_zero. 
   unfold const_low. change (rs3 GPR1) with sp. change (rs3 GPR12) with (parent_ra s).
@@ -1227,12 +1228,13 @@ Proof.
     eapply code_tail_next_int; auto.
     change (Int.unsigned Int.zero) with 0. 
     unfold transl_function. constructor.
-  assert (AG2: agree ms sp rs2).
-    split. reflexivity. 
+  assert (AG2: agree tge ms sp rs2).
+    destruct AG as [X [Y Z]].
+    split. reflexivity. split. rewrite <- Y; reflexivity. 
     intros. unfold rs2. rewrite nextinstr_inv. 
-    repeat (rewrite Pregmap.gso). elim AG; auto.
+    repeat (rewrite Pregmap.gso). auto. 
     auto with ppcgen. auto with ppcgen. auto with ppcgen.
-  assert (AG4: agree ms sp rs4).
+  assert (AG4: agree tge ms sp rs4).
     unfold rs4, rs3; auto with ppcgen.
   left; exists (State rs4 m3); split.
   (* execution *)
@@ -1308,7 +1310,8 @@ Proof.
      with (Vptr fb Int.zero).
   rewrite (Genv.init_mem_transf_partial _ _ TRANSF).
   econstructor; eauto. constructor.
-  split. auto. intros. repeat rewrite Pregmap.gso; auto with ppcgen.
+  split. auto. split. auto. 
+  intros. repeat rewrite Pregmap.gso; auto with ppcgen.
   unfold symbol_offset. 
   rewrite (transform_partial_program_main _ _ TRANSF). 
   rewrite symbols_preserved. unfold ge; rewrite H0. auto.
@@ -1320,7 +1323,7 @@ Lemma transf_final_states:
 Proof.
   intros. inv H0. inv H. constructor. auto. 
   compute in H1. 
-  rewrite (ireg_val _ _ _ R3 AG) in H1. auto. auto.
+  rewrite (ireg_val _ _ _ _ R3 AG) in H1. auto. auto.
 Qed.
 
 Theorem transf_program_correct:
diff --git a/powerpc/Asmgenproof1.v b/powerpc/Asmgenproof1.v
index 38525c9..226c175 100644
--- a/powerpc/Asmgenproof1.v
+++ b/powerpc/Asmgenproof1.v
@@ -188,18 +188,30 @@ Lemma preg_of_not_GPR1:
 Proof.
   intro. case r; discriminate.
 Qed.
-Hint Resolve preg_of_not_GPR1: ppcgen.
+Lemma preg_of_not_GPR13:
+  forall r, preg_of r <> GPR13.
+Proof.
+  intro. case r; discriminate.
+Qed.
+
+Hint Resolve preg_of_not_GPR1 preg_of_not_GPR13: ppcgen.
 
 (** Agreement between Mach register sets and PPC register sets. *)
 
+Section AGREEMENT.
+
+Variable ge: genv.
+
 Definition agree (ms: Mach.regset) (sp: val) (rs: Asm.regset) :=
-  rs#GPR1 = sp /\ forall r: mreg, ms r = rs#(preg_of r).
+  rs#GPR1 = sp /\
+  rs#GPR13 = small_data_area_base ge /\ 
+  forall r: mreg, ms r = rs#(preg_of r).
 
 Lemma preg_val:
   forall ms sp rs r,
   agree ms sp rs -> ms r = rs#(preg_of r).
 Proof.
-  intros. elim H. auto.
+  intros. destruct H as [A [B C]]. auto.
 Qed.
   
 Lemma ireg_val:
@@ -208,8 +220,8 @@ Lemma ireg_val:
   mreg_type r = Tint ->
   ms r = rs#(ireg_of r).
 Proof.
-  intros. elim H; intros.
-  generalize (H2 r). unfold preg_of. rewrite H0. auto.
+  intros. rewrite (preg_val ms sp rs); auto. 
+  unfold preg_of. rewrite H0. auto.
 Qed.
 
 Lemma freg_val:
@@ -218,8 +230,8 @@ Lemma freg_val:
   mreg_type r = Tfloat ->
   ms r = rs#(freg_of r).
 Proof.
-  intros. elim H; intros.
-  generalize (H2 r). unfold preg_of. rewrite H0. auto.
+  intros. rewrite (preg_val ms sp rs); auto. 
+  unfold preg_of. rewrite H0. auto.
 Qed.
 
 Lemma sp_val:
@@ -227,7 +239,15 @@ Lemma sp_val:
   agree ms sp rs ->
   sp = rs#GPR1.
 Proof.
-  intros. elim H; auto.
+  intros. destruct H as [A [B C]]. auto.
+Qed.
+
+Lemma gpr13_val:
+  forall ms sp rs,
+  agree ms sp rs ->
+  small_data_area_base ge = rs#GPR13.
+Proof.
+  intros. destruct H as [A [B C]]. auto.
 Qed.
 
 Lemma agree_exten_1:
@@ -236,8 +256,9 @@ Lemma agree_exten_1:
   (forall r, is_data_reg r -> rs'#r = rs#r) ->
   agree ms sp rs'.
 Proof.
-  unfold agree; intros. elim H; intros.
-  split. rewrite H0. auto. exact I. 
+  unfold agree; intros. destruct H as [A [B C]]. 
+  split. rewrite H0. auto. exact I.
+  split. rewrite H0. auto. exact I.
   intros. rewrite H0. auto. apply preg_of_is_data_reg.
 Qed.
 
@@ -263,8 +284,9 @@ Lemma agree_set_mreg:
   agree ms sp rs ->
   agree (Regmap.set r v ms) sp (rs#(preg_of r) <- v).
 Proof.
-  unfold agree; intros. elim H; intros; clear H.
+  unfold agree; intros. destruct H as [A [B C]]. 
   split. rewrite Pregmap.gso. auto. apply sym_not_eq. apply preg_of_not_GPR1.
+  split. rewrite Pregmap.gso. auto. apply sym_not_eq. apply preg_of_not_GPR13.
   intros. unfold Regmap.set. case (RegEq.eq r0 r); intro.
   subst r0. rewrite Pregmap.gss. auto.
   rewrite Pregmap.gso. auto. red; intro. 
@@ -317,15 +339,9 @@ Lemma agree_set_mireg_twice:
   mreg_type r = Tint ->
   agree (Regmap.set r v ms) sp (rs #(ireg_of r) <- v' #(ireg_of r) <- v).
 Proof.
-  intros. replace (IR (ireg_of r)) with (preg_of r). elim H; intros.
-  split. repeat (rewrite Pregmap.gso; auto with ppcgen).
-  intros. case (mreg_eq r r0); intro.
-  subst r0. rewrite Regmap.gss. rewrite Pregmap.gss. auto.
-  assert (preg_of r <> preg_of r0). 
-    red; intro. elim n. apply preg_of_injective. auto.
-  rewrite Regmap.gso; auto.
-  repeat (rewrite Pregmap.gso; auto).
-  unfold preg_of. rewrite H0. auto.
+  intros. apply agree_exten_1 with (rs#(ireg_of r) <- v).
+  apply agree_set_mireg. apply agree_set_mreg. auto. auto. 
+  intros. unfold Pregmap.set. destruct (PregEq.eq r0 (ireg_of r)); auto.
 Qed.
 Hint Resolve agree_set_mireg_twice: ppcgen.
 
@@ -335,10 +351,12 @@ Lemma agree_set_twice_mireg:
   mreg_type r = Tint ->
   agree (Regmap.set r v ms) sp (rs#(ireg_of r) <- v).
 Proof.
-  intros. elim H; intros.
-  split. rewrite Pregmap.gso. auto. 
-  generalize (ireg_of_not_GPR1 r); congruence.
-  intros. generalize (H2 r0). 
+  intros. destruct H as [A [B C]].
+  split. rewrite Pregmap.gso; auto.
+  generalize (preg_of_not_GPR1 r). unfold preg_of. rewrite H0. congruence.
+  split. rewrite Pregmap.gso; auto.
+  generalize (preg_of_not_GPR13 r). unfold preg_of. rewrite H0. congruence.
+  intros. generalize (C r0). 
   case (mreg_eq r0 r); intro.
   subst r0. repeat rewrite Regmap.gss. unfold preg_of; rewrite H0.
   rewrite Pregmap.gss. auto.
@@ -466,11 +484,6 @@ Qed.
 
 (** * Execution of straight-line code *)
 
-Section STRAIGHTLINE.
-
-Variable ge: genv.
-Variable fn: code.
-
 (** Straight-line code is composed of PPC instructions that execute
   in sequence (no branches, no function calls and returns).
   The following inductive predicate relates the machine states
@@ -478,6 +491,8 @@ Variable fn: code.
   Instructions are taken from the first list instead of being fetched
   from memory. *)
 
+Variable fn: code.
+
 Inductive exec_straight: code -> regset -> mem -> 
                          code -> regset -> mem -> Prop :=
   | exec_straight_one:
@@ -1474,6 +1489,11 @@ Proof.
   apply H0. 
   simpl. repeat (rewrite (ireg_val ms sp rs); auto). auto.
   (* Aglobal *)
+  case_eq (symbol_is_small_data i i0); intro SISD.
+  eapply H; eauto.
+  simpl. rewrite <- (gpr13_val _ _ _ H1). 
+  rewrite small_data_area_addressing; auto.
+  discriminate.
   set (rs1 := nextinstr (rs#GPR12 <- (const_high ge (Csymbol_high i i0)))).
   assert (ADDR: eval_addressing_total ge sp (Aglobal i i0) ms##nil =
                 Val.add rs1#GPR12 (const_low ge (Csymbol_low i i0))).
@@ -1619,7 +1639,7 @@ Proof.
   unfold store1. rewrite gpr_or_zero_not_zero; auto.
   repeat rewrite B. 
   rewrite <- (eval_addressing_weaken _ _ _ _ H3) in H4.
-  rewrite H5 in H4. elim H6; intros. rewrite H9 in H4.
+  rewrite H5 in H4. rewrite (preg_val _ _ _ src H6) in H4. 
   rewrite H4. auto.
   apply preg_of_not. simpl. tauto.
   discriminate.
@@ -1631,7 +1651,7 @@ Proof.
   split. apply exec_straight_one. rewrite A. 
   unfold store2. repeat rewrite B. 
   rewrite <- (eval_addressing_weaken _ _ _ _ H3) in H4.
-  rewrite H5 in H4. elim H6; intros. rewrite H8 in H4.
+  rewrite H5 in H4. rewrite (preg_val _ _ _ src H6) in H4. 
   rewrite H4. auto.
   apply preg_of_not. simpl. tauto.
   discriminate. discriminate.
@@ -1641,6 +1661,18 @@ Proof.
   auto. auto.
 Qed.
 
+End AGREEMENT.
 
-End STRAIGHTLINE.
-
+(* Re-export hints. *)
+Hint Resolve agree_set_mreg: ppcgen.
+Hint Resolve agree_set_mireg: ppcgen.
+Hint Resolve agree_set_mfreg: ppcgen.
+Hint Resolve agree_set_other: ppcgen.
+Hint Resolve agree_nextinstr: ppcgen.
+Hint Resolve agree_set_mireg_twice: ppcgen.
+Hint Resolve agree_set_twice_mireg: ppcgen.
+Hint Resolve agree_set_commut: ppcgen.
+Hint Resolve agree_nextinstr_commut: ppcgen.
+Hint Resolve nextinstr_inv: ppcgen.
+Hint Resolve nextinstr_set_preg: ppcgen.
+Hint Resolve gpr_or_zero_not_zero gpr_or_zero_zero: ppcgen.
diff --git a/powerpc/PrintAsm.ml b/powerpc/PrintAsm.ml
index 3c8d82b..a5415f8 100644
--- a/powerpc/PrintAsm.ml
+++ b/powerpc/PrintAsm.ml
@@ -110,6 +110,8 @@ let constant oc cst =
       | Linux|Diab ->
           fprintf oc "(%a)@ha" symbol_offset (s, camlint_of_coqint n)
       end
+  | Csymbol_sda(s, n) ->
+      assert false  (* treated specially in ireg_with_offset below *)
 
 let num_crbit = function
   | CRbit_0 -> 0
@@ -162,27 +164,44 @@ let creg oc r =
   | MacOS|Diab -> fprintf oc "cr%d" r
   | Linux      -> fprintf oc "%d" r
 
+let ireg_with_offset oc (r, cst) =
+  match cst with
+  | Csymbol_sda(s, n) ->
+      begin match target with
+      | MacOS ->
+          assert false
+      | Linux ->
+          fprintf oc "(%a)@sdarel(%a)" symbol_offset (s, camlint_of_coqint n) ireg r
+      | Diab ->
+          fprintf oc "(%a)@sdarx(r0)" symbol_offset (s, camlint_of_coqint n)
+      end
+  | _ ->
+      fprintf oc "%a(%a)" constant cst ireg r
+
 let section oc name =
   fprintf oc "	%s\n" name
 
 (* Names of sections *)
 
-let (text, data, const_data, float_literal) =
+let (text, data, const_data, sdata, float_literal) =
   match target with
   | MacOS ->
       (".text",
        ".data",
        ".const",
+       ".data",  (* unused *)
        ".const_data")
   | Linux ->
       (".text",
        ".data",
        ".rodata",
+       ".section	.sdata,\"aw\",@progbits",
        ".section	.rodata.cst8,\"aM\",@progbits,8")
   | Diab ->
       (".text",
        ".data",
        ".data",  (* to check *)
+       ".sdata", (* to check *)
        ".data")  (* to check *)
 
 (* Encoding masks for rlwinm instructions *)
@@ -349,11 +368,11 @@ let print_instruction oc labels = function
       fprintf oc "%a:	.long	0x43300000, 0x00000000\n" label lbl;
       section oc text
   | Plbz(r1, c, r2) ->
-      fprintf oc "	lbz	%a, %a(%a)\n" ireg r1 constant c ireg r2
+      fprintf oc "	lbz	%a, %a\n" ireg r1 ireg_with_offset (r2, c)
   | Plbzx(r1, r2, r3) ->
       fprintf oc "	lbzx	%a, %a, %a\n" ireg r1 ireg r2 ireg r3
   | Plfd(r1, c, r2) ->
-      fprintf oc "	lfd	%a, %a(%a)\n" freg r1 constant c ireg r2
+      fprintf oc "	lfd	%a, %a\n" freg r1 ireg_with_offset (r2, c)
   | Plfdx(r1, r2, r3) ->
       fprintf oc "	lfdx	%a, %a, %a\n" freg r1 ireg r2 ireg r3
   | Plfi(r1, c) ->
@@ -367,19 +386,19 @@ let print_instruction oc labels = function
       fprintf oc "%a:	.long	0x%lx, 0x%lx\n" label lbl nhi nlo;
       section oc text
   | Plfs(r1, c, r2) ->
-      fprintf oc "	lfs	%a, %a(%a)\n" freg r1 constant c ireg r2
+      fprintf oc "	lfs	%a, %a\n" freg r1 ireg_with_offset (r2, c)
   | Plfsx(r1, r2, r3) ->
       fprintf oc "	lfsx	%a, %a, %a\n" freg r1 ireg r2 ireg r3
   | Plha(r1, c, r2) ->
-      fprintf oc "	lha	%a, %a(%a)\n" ireg r1 constant c ireg r2
+      fprintf oc "	lha	%a, %a\n" ireg r1 ireg_with_offset (r2, c)
   | Plhax(r1, r2, r3) ->
       fprintf oc "	lhax	%a, %a, %a\n" ireg r1 ireg r2 ireg r3
   | Plhz(r1, c, r2) ->
-      fprintf oc "	lhz	%a, %a(%a)\n" ireg r1 constant c ireg r2
+      fprintf oc "	lhz	%a, %a\n" ireg r1 ireg_with_offset (r2, c)
   | Plhzx(r1, r2, r3) ->
       fprintf oc "	lhzx	%a, %a, %a\n" ireg r1 ireg r2 ireg r3
   | Plwz(r1, c, r2) ->
-      fprintf oc "	lwz	%a, %a(%a)\n" ireg r1 constant c ireg r2
+      fprintf oc "	lwz	%a, %a\n" ireg r1 ireg_with_offset (r2, c)
   | Plwzx(r1, r2, r3) ->
       fprintf oc "	lwzx	%a, %a, %a\n" ireg r1 ireg r2 ireg r3
   | Pmfcrbit(r1, bit) ->
@@ -426,25 +445,25 @@ let print_instruction oc labels = function
   | Psrw(r1, r2, r3) ->
       fprintf oc "	srw	%a, %a, %a\n" ireg r1 ireg r2 ireg r3
   | Pstb(r1, c, r2) ->
-      fprintf oc "	stb	%a, %a(%a)\n" ireg r1 constant c ireg r2
+      fprintf oc "	stb	%a, %a\n" ireg r1 ireg_with_offset (r2, c)
   | Pstbx(r1, r2, r3) ->
       fprintf oc "	stbx	%a, %a, %a\n" ireg r1 ireg r2 ireg r3
   | Pstfd(r1, c, r2) ->
-      fprintf oc "	stfd	%a, %a(%a)\n" freg r1 constant c ireg r2
+      fprintf oc "	stfd	%a, %a\n" freg r1 ireg_with_offset (r2, c)
   | Pstfdx(r1, r2, r3) ->
       fprintf oc "	stfdx	%a, %a, %a\n" freg r1 ireg r2 ireg r3
   | Pstfs(r1, c, r2) ->
       fprintf oc "	frsp	%a, %a\n" freg FPR13 freg r1;
-      fprintf oc "	stfs	%a, %a(%a)\n" freg FPR13 constant c ireg r2
+      fprintf oc "	stfs	%a, %a\n" freg FPR13 ireg_with_offset (r2, c)
   | Pstfsx(r1, r2, r3) ->
       fprintf oc "	frsp	%a, %a\n" freg FPR13 freg r1;
       fprintf oc "	stfsx	%a, %a, %a\n" freg FPR13 ireg r2 ireg r3
   | Psth(r1, c, r2) ->
-      fprintf oc "	sth	%a, %a(%a)\n" ireg r1 constant c ireg r2
+      fprintf oc "	sth	%a, %a\n" ireg r1 ireg_with_offset (r2, c)
   | Psthx(r1, r2, r3) ->
       fprintf oc "	sthx	%a, %a, %a\n" ireg r1 ireg r2 ireg r3
   | Pstw(r1, c, r2) ->
-      fprintf oc "	stw	%a, %a(%a)\n" ireg r1 constant c ireg r2
+      fprintf oc "	stw	%a, %a\n" ireg r1 ireg_with_offset (r2, c)
   | Pstwx(r1, r2, r3) ->
       fprintf oc "	stwx	%a, %a, %a\n" ireg r1 ireg r2 ireg r3
   | Psubfc(r1, r2, r3) ->
@@ -681,8 +700,14 @@ let print_var oc (Coq_pair(Coq_pair(name, init_data), _)) =
   match init_data with
   | [] -> ()
   | _  ->
-      section oc 
-        (if Cil2Csyntax.atom_is_readonly name then const_data else data);
+      let sec =
+        if Cil2Csyntax.atom_is_small_data name (coqint_of_camlint 0l) then
+          sdata
+        else if Cil2Csyntax.atom_is_readonly name then
+          const_data
+        else
+          data in
+      section oc sec;
       fprintf oc "	.align	3\n";
       if not (Cil2Csyntax.atom_is_static name) then
         fprintf oc "	.globl	%a\n" symbol name;