diff --git a/cfrontend/Cil2Csyntax.ml b/cfrontend/Cil2Csyntax.ml
index 20a5b7a64f5eef06530b10841c1aa40c19b4233f..16daa1418e193042cbaa2f475490b80597e99b8c 100644
--- a/cfrontend/Cil2Csyntax.ml
+++ b/cfrontend/Cil2Csyntax.ml
@@ -1254,16 +1254,14 @@ let atom_is_readonly a =
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
+ | "diab" ->
+ 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
| _ ->
false
diff --git a/driver/Clflags.ml b/driver/Clflags.ml
index 81d4af3abb39a965cb40a3301b744c0ac3741e68..08e4a5369f1309674844ee47c55ad4f551dddb86 100644
--- a/driver/Clflags.ml
+++ b/driver/Clflags.ml
@@ -17,7 +17,6 @@ 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 77f8b828ccc763477072e0bc45a497e680eaf310..30d4a6cc29aa1c19f023002858372dd50f686071 100644
--- a/driver/Driver.ml
+++ b/driver/Driver.ml
@@ -264,7 +264,6 @@ 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:
@@ -304,10 +303,6 @@ 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 f8a159b7b526842ef1ea703afbfcdaf30588f020..86b9b4c8756d642d0fd239f72fa448ba9465e100 100644
--- a/extraction/extraction.v
+++ b/extraction/extraction.v
@@ -73,7 +73,6 @@ Extract Constant Linearize.enumerate_aux => "Linearizeaux.enumerate_aux".
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 *)
diff --git a/powerpc/Asm.v b/powerpc/Asm.v
index bea5f5c06c4965c9c5b27ab2587a6ac070375d4e..0e6032fe7c09dceeac92356b583f46ff35c0db0e 100644
--- a/powerpc/Asm.v
+++ b/powerpc/Asm.v
@@ -415,18 +415,21 @@ 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. *)
+(** We also axiomatize the small data area. For simplicity, we
+ claim that small data symbols can be accessed by absolute 16-bit
+ offsets, that is, relative to [GPR0]. In reality, the linker
+ rewrites the object code, transforming [symb@sdarx(r0)] addressings
+ into [offset(rN)] addressings, where [rN] is the reserved
+ register pointing to the base of the small data area containing
+ symbol [symb]. We leave this transformation up to the linker. *)
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.
+ 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.
@@ -869,8 +872,7 @@ 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)
- # GPR13 <- (small_data_area_base ge) in
+ # GPR1 <- (Vptr Mem.nullptr Int.zero) in
initial_state p (State rs0 m0).
Inductive final_state: state -> int -> Prop :=
diff --git a/powerpc/Asmgen.v b/powerpc/Asmgen.v
index 05381ea1311b407c0d583113fd3bcf5f94b61ecb..aebb48346f20e0236a6537d51f9a7957fc8086eb 100644
--- a/powerpc/Asmgen.v
+++ b/powerpc/Asmgen.v
@@ -396,7 +396,7 @@ Definition transl_load_store
mk2 (ireg_of a1) (ireg_of a2) :: k
| Aglobal symb ofs, nil =>
if symbol_is_small_data symb ofs then
- mk1 (Csymbol_sda symb ofs) GPR13 :: k
+ mk1 (Csymbol_sda symb ofs) GPR0 :: k
else
Paddis GPR12 GPR0 (Csymbol_high symb ofs) ::
mk1 (Csymbol_low symb ofs) GPR12 :: k
diff --git a/powerpc/Asmgenproof.v b/powerpc/Asmgenproof.v
index 19e1782e2410ebd1bc934f83972038fed976e584..2710eddde6e957f83bff95c67ec045810c3295cf 100644
--- a/powerpc/Asmgenproof.v
+++ b/powerpc/Asmgenproof.v
@@ -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 tge ms sp rs),
+ (AG: agree 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 tge ms (parent_sp s) rs)
+ (AG: agree 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 tge ms (parent_sp s) rs)
+ (AG: agree 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 tge ms2 sp rs2) ->
+ /\ agree 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).
- apply agree_set_mreg. auto.
+ auto with ppcgen.
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 tge ms sp rs) in H; auto.
+ rewrite (sp_val _ _ _ AG) in H.
+ rewrite (preg_val 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 tge ms sp rs); auto.
+ unfold const_low. rewrite <- (sp_val 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 tge ms sp rs3).
+ assert (AG3: agree 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 tge ms sp rs); auto.
+ simpl. rewrite <- (ireg_val 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 tge ms sp rs2).
+ assert (AG2: agree 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 tge ms (Vptr stk soff) rs4).
+ assert (AG4: agree ms (Vptr stk soff) rs4).
unfold rs4, rs3, rs2; auto 10 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.
+ 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.
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 tge ms (Vptr stk soff) rs3).
+ assert (AG3: agree ms (Vptr stk soff) rs3).
unfold rs3, rs2; auto 10 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.
+ 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.
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,13 +1172,12 @@ Proof.
reflexivity. traceEq.
(* match states *)
econstructor; eauto.
- assert (AG3: agree tge ms (Vptr stk soff) rs3).
+ assert (AG3: agree ms (Vptr stk soff) rs3).
unfold rs3, rs2; auto 10 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.
+ 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.
unfold rs5; auto with ppcgen.
Qed.
@@ -1213,7 +1212,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).
@@ -1228,13 +1227,12 @@ Proof.
eapply code_tail_next_int; auto.
change (Int.unsigned Int.zero) with 0.
unfold transl_function. constructor.
- assert (AG2: agree tge ms sp rs2).
- destruct AG as [X [Y Z]].
- split. reflexivity. split. rewrite <- Y; reflexivity.
+ assert (AG2: agree ms sp rs2).
+ split. reflexivity.
intros. unfold rs2. rewrite nextinstr_inv.
- repeat (rewrite Pregmap.gso). auto.
+ repeat (rewrite Pregmap.gso). elim AG; auto.
auto with ppcgen. auto with ppcgen. auto with ppcgen.
- assert (AG4: agree tge ms sp rs4).
+ assert (AG4: agree ms sp rs4).
unfold rs4, rs3; auto with ppcgen.
left; exists (State rs4 m3); split.
(* execution *)
@@ -1310,8 +1308,7 @@ Proof.
with (Vptr fb Int.zero).
rewrite (Genv.init_mem_transf_partial _ _ TRANSF).
econstructor; eauto. constructor.
- split. auto. split. auto.
- intros. repeat rewrite Pregmap.gso; auto with ppcgen.
+ 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.
@@ -1323,7 +1320,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 226c175fb5b6a7c3db2fdb5645bfc35ab872dcc2..3baeb795650348d822bfa7dfee995cb7f4be2964 100644
--- a/powerpc/Asmgenproof1.v
+++ b/powerpc/Asmgenproof1.v
@@ -188,30 +188,18 @@ Lemma preg_of_not_GPR1:
Proof.
intro. case r; discriminate.
Qed.
-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.
+Hint Resolve preg_of_not_GPR1: 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 /\
- rs#GPR13 = small_data_area_base ge /\
- forall r: mreg, ms r = rs#(preg_of r).
+ rs#GPR1 = sp /\ 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. destruct H as [A [B C]]. auto.
+ intros. elim H. auto.
Qed.
Lemma ireg_val:
@@ -220,8 +208,8 @@ Lemma ireg_val:
mreg_type r = Tint ->
ms r = rs#(ireg_of r).
Proof.
- intros. rewrite (preg_val ms sp rs); auto.
- unfold preg_of. rewrite H0. auto.
+ intros. elim H; intros.
+ generalize (H2 r). unfold preg_of. rewrite H0. auto.
Qed.
Lemma freg_val:
@@ -230,8 +218,8 @@ Lemma freg_val:
mreg_type r = Tfloat ->
ms r = rs#(freg_of r).
Proof.
- intros. rewrite (preg_val ms sp rs); auto.
- unfold preg_of. rewrite H0. auto.
+ intros. elim H; intros.
+ generalize (H2 r). unfold preg_of. rewrite H0. auto.
Qed.
Lemma sp_val:
@@ -239,15 +227,7 @@ Lemma sp_val:
agree ms sp rs ->
sp = rs#GPR1.
Proof.
- 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.
+ intros. elim H; auto.
Qed.
Lemma agree_exten_1:
@@ -256,9 +236,8 @@ Lemma agree_exten_1:
(forall r, is_data_reg r -> rs'#r = rs#r) ->
agree ms sp rs'.
Proof.
- unfold agree; intros. destruct H as [A [B C]].
- split. rewrite H0. auto. exact I.
- split. rewrite H0. auto. exact I.
+ unfold agree; intros. elim H; intros.
+ split. rewrite H0. auto. exact I.
intros. rewrite H0. auto. apply preg_of_is_data_reg.
Qed.
@@ -284,9 +263,8 @@ Lemma agree_set_mreg:
agree ms sp rs ->
agree (Regmap.set r v ms) sp (rs#(preg_of r) <- v).
Proof.
- unfold agree; intros. destruct H as [A [B C]].
+ unfold agree; intros. elim H; intros; clear H.
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.
@@ -339,9 +317,15 @@ 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. 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.
+ 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.
Qed.
Hint Resolve agree_set_mireg_twice: ppcgen.
@@ -351,12 +335,10 @@ Lemma agree_set_twice_mireg:
mreg_type r = Tint ->
agree (Regmap.set r v ms) sp (rs#(ireg_of r) <- v).
Proof.
- 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).
+ intros. elim H; intros.
+ split. rewrite Pregmap.gso. auto.
+ generalize (ireg_of_not_GPR1 r); congruence.
+ intros. generalize (H2 r0).
case (mreg_eq r0 r); intro.
subst r0. repeat rewrite Regmap.gss. unfold preg_of; rewrite H0.
rewrite Pregmap.gss. auto.
@@ -484,6 +466,11 @@ 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
@@ -491,8 +478,6 @@ Qed.
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:
@@ -1422,9 +1407,9 @@ Lemma transl_load_store_correct:
forall (mk1: constant -> ireg -> instruction) (mk2: ireg -> ireg -> instruction)
addr args k ms sp rs m ms' m',
(forall cst (r1: ireg) (rs1: regset) k,
- eval_addressing_total ge sp addr (map ms args) = Val.add rs1#r1 (const_low ge cst) ->
+ eval_addressing_total ge sp addr (map ms args) =
+ Val.add (gpr_or_zero rs1 r1) (const_low ge cst) ->
agree ms sp rs1 ->
- r1 <> GPR0 ->
exists rs',
exec_straight (mk1 cst r1 :: k) rs1 m k rs' m' /\
agree ms' sp rs') ->
@@ -1448,14 +1433,13 @@ Proof.
set (rs1 := nextinstr (rs#GPR12 <- (ms t))).
set (rs2 := nextinstr (rs1#GPR12 <- (Val.add (ms t) (Vint (Int.shl (high_s i) (Int.repr 16)))))).
assert (ADDR: eval_addressing_total ge sp (Aindexed i) ms##(t :: nil) =
- Val.add rs2#GPR12 (const_low ge (Cint (low_s i)))).
- simpl. unfold rs2. rewrite nextinstr_inv. rewrite Pregmap.gss.
+ Val.add (gpr_or_zero rs2 GPR12) (const_low ge (Cint (low_s i)))).
+ simpl. rewrite gpr_or_zero_not_zero; auto with ppcgen.
+ unfold rs2. rewrite nextinstr_inv. rewrite Pregmap.gss.
rewrite Val.add_assoc. simpl. rewrite low_high_s. auto.
discriminate.
assert (AG: agree ms sp rs2). unfold rs2, rs1; auto 6 with ppcgen.
- assert (NOT0: GPR12 <> GPR0). discriminate.
- generalize (H _ _ _ k ADDR AG NOT0).
- intros [rs' [EX' AG']].
+ destruct (H _ _ _ k ADDR AG) as [rs' [EX' AG']].
exists rs'. split.
apply exec_straight_trans with (mk1 (Cint (low_s i)) GPR12 :: k) rs2 m.
apply exec_straight_two with rs1 m.
@@ -1467,20 +1451,21 @@ Proof.
(* Aindexed short *)
case (Int.eq (high_s i) Int.zero).
assert (ADDR: eval_addressing_total ge sp (Aindexed i) ms##(t :: nil) =
- Val.add rs#(ireg_of t) (const_low ge (Cint i))).
- simpl. rewrite (ireg_val ms sp rs); auto.
- generalize (H _ _ _ k ADDR H1 n). intros [rs' [EX' AG']].
+ Val.add (gpr_or_zero rs (ireg_of t)) (const_low ge (Cint i))).
+ simpl. rewrite gpr_or_zero_not_zero; auto with ppcgen.
+ rewrite (ireg_val ms sp rs); auto.
+ destruct (H _ _ _ k ADDR H1) as [rs' [EX' AG']].
exists rs'. split. auto. auto.
(* Aindexed long *)
set (rs1 := nextinstr (rs#GPR12 <- (Val.add (ms t) (Vint (Int.shl (high_s i) (Int.repr 16)))))).
assert (ADDR: eval_addressing_total ge sp (Aindexed i) ms##(t :: nil) =
- Val.add rs1#GPR12 (const_low ge (Cint (low_s i)))).
- simpl. unfold rs1. rewrite nextinstr_inv. rewrite Pregmap.gss.
+ Val.add (gpr_or_zero rs1 GPR12) (const_low ge (Cint (low_s i)))).
+ simpl. rewrite gpr_or_zero_not_zero; auto with ppcgen.
+ unfold rs1. rewrite nextinstr_inv. rewrite Pregmap.gss.
rewrite Val.add_assoc. simpl. rewrite low_high_s. auto.
discriminate.
assert (AG: agree ms sp rs1). unfold rs1; auto with ppcgen.
- assert (NOT0: GPR12 <> GPR0). discriminate.
- generalize (H _ _ _ k ADDR AG NOT0). intros [rs' [EX' AG']].
+ destruct (H _ _ _ k ADDR AG) as [rs' [EX' AG']].
exists rs'. split. apply exec_straight_step with rs1 m.
simpl. rewrite gpr_or_zero_not_zero; auto.
rewrite <- (ireg_val ms sp rs); auto. reflexivity.
@@ -1490,21 +1475,24 @@ Proof.
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.
+ (* Aglobal from small data *)
+ apply H. rewrite gpr_or_zero_zero. simpl const_low.
+ rewrite small_data_area_addressing; auto. simpl.
+ unfold find_symbol_offset, symbol_offset.
+ destruct (Genv.find_symbol ge i); auto. rewrite Int.add_zero. auto.
+ auto.
+ (* Aglobal general case *)
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))).
- simpl. unfold rs1. rewrite nextinstr_inv. rewrite Pregmap.gss.
+ Val.add (gpr_or_zero rs1 GPR12) (const_low ge (Csymbol_low i i0))).
+ simpl. rewrite gpr_or_zero_not_zero; auto.
+ unfold rs1. rewrite nextinstr_inv. rewrite Pregmap.gss.
unfold const_high, const_low.
set (v := symbol_offset ge i i0).
symmetry. rewrite Val.add_commut. unfold v. apply low_high_half.
- discriminate.
+ discriminate. discriminate.
assert (AG: agree ms sp rs1). unfold rs1; auto with ppcgen.
- assert (NOT0: GPR12 <> GPR0). discriminate.
- generalize (H _ _ _ k ADDR AG NOT0). intros [rs' [EX' AG']].
+ destruct (H _ _ _ k ADDR AG) as [rs' [EX' AG']].
exists rs'. split. apply exec_straight_step with rs1 m.
unfold exec_instr. rewrite gpr_or_zero_zero.
rewrite Val.add_commut. unfold const_high.
@@ -1525,8 +1513,9 @@ Proof.
intros.
set (rs2 := nextinstr (rs1#GPR12 <- (Val.add (ms t) (const_high ge (Csymbol_high i i0))))).
assert (ADDR: eval_addressing_total ge sp (Abased i i0) ms##(t::nil) =
- Val.add rs2#GPR12 (const_low ge (Csymbol_low i i0))).
- simpl. unfold rs2. rewrite nextinstr_inv. rewrite Pregmap.gss.
+ Val.add (gpr_or_zero rs2 GPR12) (const_low ge (Csymbol_low i i0))).
+ simpl. rewrite gpr_or_zero_not_zero; auto with ppcgen.
+ unfold rs2. rewrite nextinstr_inv. rewrite Pregmap.gss.
unfold const_high.
set (v := symbol_offset ge i i0).
rewrite Val.add_assoc.
@@ -1534,8 +1523,7 @@ Proof.
unfold v. rewrite low_high_half. apply Val.add_commut.
discriminate.
assert (AG: agree ms sp rs2). unfold rs2; auto with ppcgen.
- assert (NOT0: GPR12 <> GPR0). discriminate.
- generalize (H _ _ _ k ADDR AG NOT0). intros [rs' [EX' AG']].
+ destruct (H _ _ _ k ADDR AG) as [rs' [EX' AG']].
exists rs'. split. apply exec_straight_step with rs2 m.
unfold exec_instr. rewrite gpr_or_zero_not_zero; auto.
rewrite <- H3. reflexivity. reflexivity.
@@ -1555,17 +1543,17 @@ Proof.
apply COMMON; auto. eapply ireg_val; eauto.
(* Ainstack *)
case (Int.eq (high_s i) Int.zero).
- apply H. simpl. rewrite (sp_val ms sp rs); auto. auto.
- discriminate.
+ apply H. simpl. rewrite gpr_or_zero_not_zero; auto with ppcgen.
+ rewrite (sp_val ms sp rs); auto. auto.
set (rs1 := nextinstr (rs#GPR12 <- (Val.add sp (Vint (Int.shl (high_s i) (Int.repr 16)))))).
assert (ADDR: eval_addressing_total ge sp (Ainstack i) ms##nil =
- Val.add rs1#GPR12 (const_low ge (Cint (low_s i)))).
- simpl. unfold rs1. rewrite nextinstr_inv. rewrite Pregmap.gss.
+ Val.add (gpr_or_zero rs1 GPR12) (const_low ge (Cint (low_s i)))).
+ simpl. rewrite gpr_or_zero_not_zero; auto with ppcgen.
+ unfold rs1. rewrite nextinstr_inv. rewrite Pregmap.gss.
rewrite Val.add_assoc. decEq. simpl. rewrite low_high_s. auto.
discriminate.
assert (AG: agree ms sp rs1). unfold rs1; auto with ppcgen.
- assert (NOT0: GPR12 <> GPR0). discriminate.
- generalize (H _ _ _ k ADDR AG NOT0). intros [rs' [EX' AG']].
+ destruct (H _ _ _ k ADDR AG) as [rs' [EX' AG']].
exists rs'. split. apply exec_straight_step with rs1 m.
simpl. rewrite gpr_or_zero_not_zero.
unfold rs1. rewrite (sp_val ms sp rs). reflexivity.
@@ -1595,8 +1583,7 @@ Proof.
intros. apply transl_load_store_correct with ms.
intros. exists (nextinstr (rs1#(preg_of dst) <- v)).
split. apply exec_straight_one. rewrite H.
- unfold load1. rewrite gpr_or_zero_not_zero; auto.
- rewrite <- (eval_addressing_weaken _ _ _ _ H3) in H4.
+ unfold load1. rewrite <- (eval_addressing_weaken _ _ _ _ H3) in H4.
rewrite H5 in H4. rewrite H4. auto.
auto with ppcgen. auto with ppcgen.
intros. exists (nextinstr (rs1#(preg_of dst) <- v)).
@@ -1636,13 +1623,12 @@ Proof.
intros. destruct (H cst r1 rs1) as [rs2 [A B]].
exists (nextinstr rs2).
split. apply exec_straight_one. rewrite A.
- unfold store1. rewrite gpr_or_zero_not_zero; auto.
- repeat rewrite B.
+ unfold store1. rewrite B. replace (gpr_or_zero rs2 r1) with (gpr_or_zero rs1 r1).
rewrite <- (eval_addressing_weaken _ _ _ _ H3) in H4.
- rewrite H5 in H4. rewrite (preg_val _ _ _ src H6) in H4.
+ rewrite H5 in H4. elim H6; intros. rewrite H8 in H4.
rewrite H4. auto.
+ unfold gpr_or_zero. destruct (ireg_eq r1 GPR0); auto. symmetry. apply B. discriminate.
apply preg_of_not. simpl. tauto.
- discriminate.
rewrite <- B. auto. discriminate.
apply agree_nextinstr. eapply agree_exten_2; eauto.
@@ -1651,7 +1637,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. rewrite (preg_val _ _ _ src H6) in H4.
+ rewrite H5 in H4. elim H6; intros. rewrite H8 in H4.
rewrite H4. auto.
apply preg_of_not. simpl. tauto.
discriminate. discriminate.
@@ -1661,18 +1647,6 @@ Proof.
auto. auto.
Qed.
-End AGREEMENT.
-(* 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.
+End STRAIGHTLINE.
+
diff --git a/powerpc/PrintAsm.ml b/powerpc/PrintAsm.ml
index a5415f815d9c898f8f6865c4f4cd44a48553c98d..95074988aeb52ab345e55d059986fe8f47ff017f 100644
--- a/powerpc/PrintAsm.ml
+++ b/powerpc/PrintAsm.ml
@@ -111,7 +111,13 @@ let constant oc cst =
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 *)
+ begin match target with
+ | Diab ->
+ fprintf oc "(%a)@sdarx" symbol_offset (s, camlint_of_coqint n)
+ | _ ->
+ assert false
+ end
+
let num_crbit = function
| CRbit_0 -> 0
@@ -164,20 +170,6 @@ 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
@@ -195,7 +187,7 @@ let (text, data, const_data, sdata, float_literal) =
(".text",
".data",
".rodata",
- ".section .sdata,\"aw\",@progbits",
+ ".data", (* unused *)
".section .rodata.cst8,\"aM\",@progbits,8")
| Diab ->
(".text",
@@ -368,11 +360,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\n" ireg r1 ireg_with_offset (r2, c)
+ fprintf oc " lbz %a, %a(%a)\n" ireg r1 constant c ireg r2
| 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\n" freg r1 ireg_with_offset (r2, c)
+ fprintf oc " lfd %a, %a(%a)\n" freg r1 constant c ireg r2
| Plfdx(r1, r2, r3) ->
fprintf oc " lfdx %a, %a, %a\n" freg r1 ireg r2 ireg r3
| Plfi(r1, c) ->
@@ -386,19 +378,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\n" freg r1 ireg_with_offset (r2, c)
+ fprintf oc " lfs %a, %a(%a)\n" freg r1 constant c ireg r2
| 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\n" ireg r1 ireg_with_offset (r2, c)
+ fprintf oc " lha %a, %a(%a)\n" ireg r1 constant c ireg r2
| 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\n" ireg r1 ireg_with_offset (r2, c)
+ fprintf oc " lhz %a, %a(%a)\n" ireg r1 constant c ireg r2
| 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\n" ireg r1 ireg_with_offset (r2, c)
+ fprintf oc " lwz %a, %a(%a)\n" ireg r1 constant c ireg r2
| Plwzx(r1, r2, r3) ->
fprintf oc " lwzx %a, %a, %a\n" ireg r1 ireg r2 ireg r3
| Pmfcrbit(r1, bit) ->
@@ -445,25 +437,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\n" ireg r1 ireg_with_offset (r2, c)
+ fprintf oc " stb %a, %a(%a)\n" ireg r1 constant c ireg r2
| 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\n" freg r1 ireg_with_offset (r2, c)
+ fprintf oc " stfd %a, %a(%a)\n" freg r1 constant c ireg r2
| 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\n" freg FPR13 ireg_with_offset (r2, c)
+ fprintf oc " stfs %a, %a(%a)\n" freg FPR13 constant c ireg r2
| 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\n" ireg r1 ireg_with_offset (r2, c)
+ fprintf oc " sth %a, %a(%a)\n" ireg r1 constant c ireg r2
| 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\n" ireg r1 ireg_with_offset (r2, c)
+ fprintf oc " stw %a, %a(%a)\n" ireg r1 constant c ireg r2
| Pstwx(r1, r2, r3) ->
fprintf oc " stwx %a, %a, %a\n" ireg r1 ireg r2 ireg r3
| Psubfc(r1, r2, r3) ->