diff options
| -rw-r--r-- | cfrontend/Cil2Csyntax.ml | 18 | ||||
| -rw-r--r-- | driver/Clflags.ml | 1 | ||||
| -rw-r--r-- | driver/Driver.ml | 5 | ||||
| -rw-r--r-- | extraction/extraction.v | 1 | ||||
| -rw-r--r-- | powerpc/Asm.v | 16 | ||||
| -rw-r--r-- | powerpc/Asmgen.v | 2 | ||||
| -rw-r--r-- | powerpc/Asmgenproof.v | 87 | ||||
| -rw-r--r-- | powerpc/Asmgenproof1.v | 170 | ||||
| -rw-r--r-- | powerpc/PrintAsm.ml | 46 |
9 files changed, 151 insertions, 195 deletions
diff --git a/cfrontend/Cil2Csyntax.ml b/cfrontend/Cil2Csyntax.ml index 20a5b7a..16daa14 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 81d4af3..08e4a53 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 77f8b82..30d4a6c 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 f8a159b..86b9b4c 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 bea5f5c..0e6032f 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 05381ea..aebb483 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 19e1782..2710edd 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 226c175..3baeb79 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 a5415f8..9507498 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) -> |