diff options
67 files changed, 1749 insertions, 1214 deletions
diff --git a/aarch64/Builtins1.v b/aarch64/Builtins1.v index f6e643d2..53c83d7e 100644 --- a/aarch64/Builtins1.v +++ b/aarch64/Builtins1.v @@ -29,5 +29,5 @@ Definition platform_builtin_table : list (string * platform_builtin) := Definition platform_builtin_sig (b: platform_builtin) : signature := match b with end. -Definition platform_builtin_sem (b: platform_builtin) : builtin_sem (proj_sig_res (platform_builtin_sig b)) := +Definition platform_builtin_sem (b: platform_builtin) : builtin_sem (sig_res (platform_builtin_sig b)) := match b with end. diff --git a/aarch64/Conventions1.v b/aarch64/Conventions1.v index 5914e8f2..efda835d 100644 --- a/aarch64/Conventions1.v +++ b/aarch64/Conventions1.v @@ -102,10 +102,9 @@ Definition is_float_reg (r: mreg): bool := with one integer result. *) Definition loc_result (s: signature) : rpair mreg := - match s.(sig_res) with - | None => One R0 - | Some (Tint | Tlong | Tany32 | Tany64) => One R0 - | Some (Tfloat | Tsingle) => One F0 + match proj_sig_res s with + | Tint | Tlong | Tany32 | Tany64 => One R0 + | Tfloat | Tsingle => One F0 end. (** The result registers have types compatible with that given in the signature. *) @@ -114,7 +113,7 @@ Lemma loc_result_type: forall sig, subtype (proj_sig_res sig) (typ_rpair mreg_type (loc_result sig)) = true. Proof. - intros. unfold proj_sig_res, loc_result. destruct (sig_res sig) as [[]|]; auto. + intros. unfold loc_result. destruct (proj_sig_res sig); auto. Qed. (** The result locations are caller-save registers *) @@ -124,7 +123,7 @@ Lemma loc_result_caller_save: forall_rpair (fun r => is_callee_save r = false) (loc_result s). Proof. intros. - unfold loc_result. destruct (sig_res s) as [[]|]; simpl; auto. + unfold loc_result. destruct (proj_sig_res s); simpl; auto. Qed. (** If the result is in a pair of registers, those registers are distinct and have type [Tint] at least. *) @@ -134,12 +133,12 @@ Lemma loc_result_pair: match loc_result sg with | One _ => True | Twolong r1 r2 => - r1 <> r2 /\ sg.(sig_res) = Some Tlong + r1 <> r2 /\ proj_sig_res sg = Tlong /\ subtype Tint (mreg_type r1) = true /\ subtype Tint (mreg_type r2) = true /\ Archi.ptr64 = false end. Proof. - intros; unfold loc_result; destruct (sig_res sg) as [[]|]; exact I. + intros; unfold loc_result; destruct (proj_sig_res sg); exact I. Qed. (** The location of the result depends only on the result part of the signature *) @@ -147,7 +146,7 @@ Qed. Lemma loc_result_exten: forall s1 s2, s1.(sig_res) = s2.(sig_res) -> loc_result s1 = loc_result s2. Proof. - intros. unfold loc_result. rewrite H; auto. + intros. unfold loc_result, proj_sig_res. rewrite H; auto. Qed. (** ** Location of function arguments *) @@ -191,27 +190,6 @@ Fixpoint loc_arguments_rec Definition loc_arguments (s: signature) : list (rpair loc) := loc_arguments_rec s.(sig_args) 0 0 0. -(** [size_arguments s] returns the number of [Outgoing] slots used - to call a function with signature [s]. *) - -Fixpoint size_arguments_rec (tyl: list typ) (ir fr ofs: Z) {struct tyl} : Z := - match tyl with - | nil => ofs - | (Tint | Tlong | Tany32 | Tany64) :: tys => - match list_nth_z int_param_regs ir with - | None => size_arguments_rec tys ir fr (ofs + 2) - | Some ireg => size_arguments_rec tys (ir + 1) fr ofs - end - | (Tfloat | Tsingle) :: tys => - match list_nth_z float_param_regs fr with - | None => size_arguments_rec tys ir fr (ofs + 2) - | Some freg => size_arguments_rec tys ir (fr + 1) ofs - end - end. - -Definition size_arguments (s: signature) : Z := - size_arguments_rec s.(sig_args) 0 0 0. - (** Argument locations are either caller-save registers or [Outgoing] stack slots at nonnegative offsets. *) @@ -286,95 +264,22 @@ Qed. Hint Resolve loc_arguments_acceptable: locs. -(** The offsets of [Outgoing] arguments are below [size_arguments s]. *) - -Remark size_arguments_rec_above: - forall tyl ir fr ofs0, - ofs0 <= size_arguments_rec tyl ir fr ofs0. -Proof. - induction tyl; simpl; intros. - omega. - assert (A: ofs0 <= - match list_nth_z int_param_regs ir with - | Some _ => size_arguments_rec tyl (ir + 1) fr ofs0 - | None => size_arguments_rec tyl ir fr (ofs0 + 2) - end). - { destruct (list_nth_z int_param_regs ir); eauto. - apply Z.le_trans with (ofs0 + 2); auto. omega. } - assert (B: ofs0 <= - match list_nth_z float_param_regs fr with - | Some _ => size_arguments_rec tyl ir (fr + 1) ofs0 - | None => size_arguments_rec tyl ir fr (ofs0 + 2) - end). - { destruct (list_nth_z float_param_regs fr); eauto. - apply Z.le_trans with (ofs0 + 2); auto. omega. } - destruct a; auto. -Qed. - -Lemma size_arguments_above: - forall s, size_arguments s >= 0. -Proof. - intros; unfold size_arguments. apply Z.le_ge. apply size_arguments_rec_above. -Qed. - -Lemma loc_arguments_rec_bounded: - forall ofs ty tyl ir fr ofs0, - In (S Outgoing ofs ty) (regs_of_rpairs (loc_arguments_rec tyl ir fr ofs0)) -> - ofs + typesize ty <= size_arguments_rec tyl ir fr ofs0. -Proof. - induction tyl; simpl; intros. -- contradiction. -- assert (T: forall ty0, typesize ty0 <= 2). - { destruct ty0; simpl; omega. } - assert (A: forall ty0, - In (S Outgoing ofs ty) (regs_of_rpairs - match list_nth_z int_param_regs ir with - | Some ireg => - One (R ireg) :: loc_arguments_rec tyl (ir + 1) fr ofs0 - | None => One (S Outgoing ofs0 ty0) :: loc_arguments_rec tyl ir fr (ofs0 + 2) - end) -> - ofs + typesize ty <= - match list_nth_z int_param_regs ir with - | Some _ => size_arguments_rec tyl (ir + 1) fr ofs0 - | None => size_arguments_rec tyl ir fr (ofs0 + 2) - end). - { intros. destruct (list_nth_z int_param_regs ir); simpl in H0; destruct H0. - - discriminate. - - eapply IHtyl; eauto. - - inv H0. apply Z.le_trans with (ofs + 2). specialize (T ty). omega. apply size_arguments_rec_above. - - eapply IHtyl; eauto. } - assert (B: forall ty0, - In (S Outgoing ofs ty) (regs_of_rpairs - match list_nth_z float_param_regs fr with - | Some ireg => - One (R ireg) :: loc_arguments_rec tyl ir (fr + 1) ofs0 - | None => One (S Outgoing ofs0 ty0) :: loc_arguments_rec tyl ir fr (ofs0 + 2) - end) -> - ofs + typesize ty <= - match list_nth_z float_param_regs fr with - | Some _ => size_arguments_rec tyl ir (fr + 1) ofs0 - | None => size_arguments_rec tyl ir fr (ofs0 + 2) - end). - { intros. destruct (list_nth_z float_param_regs fr); simpl in H0; destruct H0. - - discriminate. - - eapply IHtyl; eauto. - - inv H0. apply Z.le_trans with (ofs + 2). specialize (T ty). omega. apply size_arguments_rec_above. - - eapply IHtyl; eauto. } - destruct a; eauto. -Qed. - -Lemma loc_arguments_bounded: - forall (s: signature) (ofs: Z) (ty: typ), - In (S Outgoing ofs ty) (regs_of_rpairs (loc_arguments s)) -> - ofs + typesize ty <= size_arguments s. -Proof. - unfold loc_arguments, size_arguments; intros. - eauto using loc_arguments_rec_bounded. -Qed. - Lemma loc_arguments_main: loc_arguments signature_main = nil. Proof. unfold loc_arguments; reflexivity. Qed. +(** ** Normalization of function results *) + +(** According to the AAPCS64 ABI specification, "padding bits" in the return + value of a function have unpredictable values and must be ignored. + Consequently, we force normalization of return values of small integer + types (8- and 16-bit integers), so that the top bits (the "padding bits") + are proper sign- or zero-extensions of the small integer value. *) + +Definition return_value_needs_normalization (t: rettype) : bool := + match t with + | Tint8signed | Tint8unsigned | Tint16signed | Tint16unsigned => true + | _ => false + end. diff --git a/arm/Builtins1.v b/arm/Builtins1.v index f6e643d2..53c83d7e 100644 --- a/arm/Builtins1.v +++ b/arm/Builtins1.v @@ -29,5 +29,5 @@ Definition platform_builtin_table : list (string * platform_builtin) := Definition platform_builtin_sig (b: platform_builtin) : signature := match b with end. -Definition platform_builtin_sem (b: platform_builtin) : builtin_sem (proj_sig_res (platform_builtin_sig b)) := +Definition platform_builtin_sem (b: platform_builtin) : builtin_sem (sig_res (platform_builtin_sig b)) := match b with end. diff --git a/arm/Conventions1.v b/arm/Conventions1.v index c5277e8d..fe49a781 100644 --- a/arm/Conventions1.v +++ b/arm/Conventions1.v @@ -104,13 +104,12 @@ Definition is_float_reg (r: mreg): bool := representation with a single LDM instruction. *) Definition loc_result (s: signature) : rpair mreg := - match s.(sig_res) with - | None => One R0 - | Some (Tint | Tany32) => One R0 - | Some (Tfloat | Tsingle | Tany64) => One F0 - | Some Tlong => if Archi.big_endian - then Twolong R0 R1 - else Twolong R1 R0 + match proj_sig_res s with + | Tint | Tany32 => One R0 + | Tfloat | Tsingle | Tany64 => One F0 + | Tlong => if Archi.big_endian + then Twolong R0 R1 + else Twolong R1 R0 end. (** The result registers have types compatible with that given in the signature. *) @@ -119,7 +118,7 @@ Lemma loc_result_type: forall sig, subtype (proj_sig_res sig) (typ_rpair mreg_type (loc_result sig)) = true. Proof. - intros. unfold proj_sig_res, loc_result. destruct (sig_res sig) as [[]|]; destruct Archi.big_endian; auto. + intros. unfold loc_result. destruct (proj_sig_res sig); destruct Archi.big_endian; auto. Qed. (** The result locations are caller-save registers *) @@ -129,7 +128,7 @@ Lemma loc_result_caller_save: forall_rpair (fun r => is_callee_save r = false) (loc_result s). Proof. intros. - unfold loc_result. destruct (sig_res s) as [[]|]; destruct Archi.big_endian; simpl; auto. + unfold loc_result. destruct (proj_sig_res s); destruct Archi.big_endian; simpl; auto. Qed. (** If the result is in a pair of registers, those registers are distinct and have type [Tint] at least. *) @@ -139,14 +138,13 @@ Lemma loc_result_pair: match loc_result sg with | One _ => True | Twolong r1 r2 => - r1 <> r2 /\ sg.(sig_res) = Some Tlong + r1 <> r2 /\ proj_sig_res sg = Tlong /\ subtype Tint (mreg_type r1) = true /\ subtype Tint (mreg_type r2) = true /\ Archi.ptr64 = false end. Proof. - intros; unfold loc_result; destruct (sig_res sg) as [[]|]; destruct Archi.big_endian; auto. - intuition congruence. - intuition congruence. + intros; unfold loc_result; destruct (proj_sig_res sg); auto. + destruct Archi.big_endian; intuition congruence. Qed. (** The location of the result depends only on the result part of the signature *) @@ -154,7 +152,7 @@ Qed. Lemma loc_result_exten: forall s1 s2, s1.(sig_res) = s2.(sig_res) -> loc_result s1 = loc_result s2. Proof. - intros. unfold loc_result. rewrite H; auto. + intros. unfold loc_result, proj_sig_res. rewrite H; auto. Qed. (** ** Location of function arguments *) @@ -271,48 +269,6 @@ Definition loc_arguments (s: signature) : list (rpair loc) := else loc_arguments_hf s.(sig_args) 0 0 0 end. -(** [size_arguments s] returns the number of [Outgoing] slots used - to call a function with signature [s]. *) - -Fixpoint size_arguments_hf (tyl: list typ) (ir fr ofs: Z) {struct tyl} : Z := - match tyl with - | nil => ofs - | (Tint|Tany32) :: tys => - if zlt ir 4 - then size_arguments_hf tys (ir + 1) fr ofs - else size_arguments_hf tys ir fr (ofs + 1) - | (Tfloat|Tany64) :: tys => - if zlt fr 8 - then size_arguments_hf tys ir (fr + 1) ofs - else size_arguments_hf tys ir fr (align ofs 2 + 2) - | Tsingle :: tys => - if zlt fr 8 - then size_arguments_hf tys ir (fr + 1) ofs - else size_arguments_hf tys ir fr (ofs + 1) - | Tlong :: tys => - let ir := align ir 2 in - if zlt ir 4 - then size_arguments_hf tys (ir + 2) fr ofs - else size_arguments_hf tys ir fr (align ofs 2 + 2) - end. - -Fixpoint size_arguments_sf (tyl: list typ) (ofs: Z) {struct tyl} : Z := - match tyl with - | nil => Z.max 0 ofs - | (Tint | Tsingle | Tany32) :: tys => size_arguments_sf tys (ofs + 1) - | (Tfloat | Tlong | Tany64) :: tys => size_arguments_sf tys (align ofs 2 + 2) - end. - -Definition size_arguments (s: signature) : Z := - match Archi.abi with - | Archi.Softfloat => - size_arguments_sf s.(sig_args) (-4) - | Archi.Hardfloat => - if s.(sig_cc).(cc_vararg) - then size_arguments_sf s.(sig_args) (-4) - else size_arguments_hf s.(sig_args) 0 0 0 - end. - (** Argument locations are either non-temporary registers or [Outgoing] stack slots at nonnegative offsets. *) @@ -473,173 +429,15 @@ Qed. Hint Resolve loc_arguments_acceptable: locs. -(** The offsets of [Outgoing] arguments are below [size_arguments s]. *) - -Remark size_arguments_hf_above: - forall tyl ir fr ofs0, - ofs0 <= size_arguments_hf tyl ir fr ofs0. -Proof. - induction tyl; simpl; intros. - omega. - destruct a. - destruct (zlt ir 4); eauto. apply Z.le_trans with (ofs0 + 1); auto; omega. - destruct (zlt fr 8); eauto. - apply Z.le_trans with (align ofs0 2). apply align_le; omega. - apply Z.le_trans with (align ofs0 2 + 2); auto; omega. - set (ir' := align ir 2). - destruct (zlt ir' 4); eauto. - apply Z.le_trans with (align ofs0 2). apply align_le; omega. - apply Z.le_trans with (align ofs0 2 + 2); auto; omega. - destruct (zlt fr 8); eauto. - apply Z.le_trans with (ofs0 + 1); eauto. omega. - destruct (zlt ir 4); eauto. apply Z.le_trans with (ofs0 + 1); auto; omega. - destruct (zlt fr 8); eauto. - apply Z.le_trans with (align ofs0 2). apply align_le; omega. - apply Z.le_trans with (align ofs0 2 + 2); auto; omega. -Qed. - -Remark size_arguments_sf_above: - forall tyl ofs0, - Z.max 0 ofs0 <= size_arguments_sf tyl ofs0. -Proof. - induction tyl; simpl; intros. - omega. - destruct a; (eapply Z.le_trans; [idtac|eauto]). - xomega. - assert (ofs0 <= align ofs0 2) by (apply align_le; omega). xomega. - assert (ofs0 <= align ofs0 2) by (apply align_le; omega). xomega. - xomega. - xomega. - assert (ofs0 <= align ofs0 2) by (apply align_le; omega). xomega. -Qed. - -Lemma size_arguments_above: - forall s, size_arguments s >= 0. -Proof. - intros; unfold size_arguments. apply Z.le_ge. - assert (0 <= size_arguments_sf (sig_args s) (-4)). - { change 0 with (Z.max 0 (-4)). apply size_arguments_sf_above. } - assert (0 <= size_arguments_hf (sig_args s) 0 0 0). - { apply size_arguments_hf_above. } - destruct Archi.abi; [ | destruct (cc_vararg (sig_cc s)) ]; auto. -Qed. - -Lemma loc_arguments_hf_bounded: - forall ofs ty tyl ir fr ofs0, - In (S Outgoing ofs ty) (regs_of_rpairs (loc_arguments_hf tyl ir fr ofs0)) -> - ofs + typesize ty <= size_arguments_hf tyl ir fr ofs0. -Proof. - induction tyl; simpl; intros. - elim H. - destruct a. -- (* int *) - destruct (zlt ir 4); destruct H. - discriminate. - eauto. - inv H. apply size_arguments_hf_above. - eauto. -- (* float *) - destruct (zlt fr 8); destruct H. - discriminate. - eauto. - inv H. apply size_arguments_hf_above. - eauto. -- (* long *) - destruct (zlt (align ir 2) 4). - destruct H. discriminate. destruct H. discriminate. eauto. - destruct Archi.big_endian. - destruct H. inv H. - eapply Z.le_trans. 2: apply size_arguments_hf_above. simpl; omega. - destruct H. inv H. - rewrite <- Z.add_assoc. simpl. apply size_arguments_hf_above. - eauto. - destruct H. inv H. - rewrite <- Z.add_assoc. simpl. apply size_arguments_hf_above. - destruct H. inv H. - eapply Z.le_trans. 2: apply size_arguments_hf_above. simpl; omega. - eauto. -- (* float *) - destruct (zlt fr 8); destruct H. - discriminate. - eauto. - inv H. apply size_arguments_hf_above. - eauto. -- (* any32 *) - destruct (zlt ir 4); destruct H. - discriminate. - eauto. - inv H. apply size_arguments_hf_above. - eauto. -- (* any64 *) - destruct (zlt fr 8); destruct H. - discriminate. - eauto. - inv H. apply size_arguments_hf_above. - eauto. -Qed. - -Lemma loc_arguments_sf_bounded: - forall ofs ty tyl ofs0, - In (S Outgoing ofs ty) (regs_of_rpairs (loc_arguments_sf tyl ofs0)) -> - Z.max 0 (ofs + typesize ty) <= size_arguments_sf tyl ofs0. -Proof. - induction tyl; simpl; intros. - elim H. - destruct a. -- (* int *) - destruct H. - destruct (zlt ofs0 0); inv H. apply size_arguments_sf_above. - eauto. -- (* float *) - destruct H. - destruct (zlt (align ofs0 2) 0); inv H. apply size_arguments_sf_above. - eauto. -- (* long *) - destruct H. - destruct Archi.big_endian. - destruct (zlt (align ofs0 2) 0); inv H. - eapply Z.le_trans. 2: apply size_arguments_sf_above. simpl; xomega. - destruct (zlt (align ofs0 2) 0); inv H. - rewrite <- Z.add_assoc. simpl. apply size_arguments_sf_above. - destruct H. - destruct Archi.big_endian. - destruct (zlt (align ofs0 2) 0); inv H. - rewrite <- Z.add_assoc. simpl. apply size_arguments_sf_above. - destruct (zlt (align ofs0 2) 0); inv H. - eapply Z.le_trans. 2: apply size_arguments_sf_above. simpl; xomega. - eauto. -- (* float *) - destruct H. - destruct (zlt ofs0 0); inv H. apply size_arguments_sf_above. - eauto. -- (* any32 *) - destruct H. - destruct (zlt ofs0 0); inv H. apply size_arguments_sf_above. - eauto. -- (* any64 *) - destruct H. - destruct (zlt (align ofs0 2) 0); inv H. apply size_arguments_sf_above. - eauto. -Qed. - -Lemma loc_arguments_bounded: - forall (s: signature) (ofs: Z) (ty: typ), - In (S Outgoing ofs ty) (regs_of_rpairs (loc_arguments s)) -> - ofs + typesize ty <= size_arguments s. -Proof. - unfold loc_arguments, size_arguments; intros. - assert (In (S Outgoing ofs ty) (regs_of_rpairs (loc_arguments_sf (sig_args s) (-4))) -> - ofs + typesize ty <= size_arguments_sf (sig_args s) (-4)). - { intros. eapply Z.le_trans. 2: eapply loc_arguments_sf_bounded; eauto. xomega. } - assert (In (S Outgoing ofs ty) (regs_of_rpairs (loc_arguments_hf (sig_args s) 0 0 0)) -> - ofs + typesize ty <= size_arguments_hf (sig_args s) 0 0 0). - { intros. eapply loc_arguments_hf_bounded; eauto. } - destruct Archi.abi; [ | destruct (cc_vararg (sig_cc s)) ]; eauto. -Qed. - Lemma loc_arguments_main: loc_arguments signature_main = nil. Proof. unfold loc_arguments. destruct Archi.abi; reflexivity. Qed. + +(** ** Normalization of function results *) + +(** No normalization needed. *) + +Definition return_value_needs_normalization (t: rettype) := false. diff --git a/backend/Allocation.v b/backend/Allocation.v index 6e4fcc82..d18b07a9 100644 --- a/backend/Allocation.v +++ b/backend/Allocation.v @@ -738,11 +738,11 @@ Function add_equations_args (rl: list reg) (tyl: list typ) (ll: list (rpair loc) (** [add_equations_res] is similar but is specialized to the case where there is only one pseudo-register. *) -Function add_equations_res (r: reg) (oty: option typ) (p: rpair mreg) (e: eqs) : option eqs := - match p, oty with +Function add_equations_res (r: reg) (ty: typ) (p: rpair mreg) (e: eqs) : option eqs := + match p, ty with | One mr, _ => Some (add_equation (Eq Full r (R mr)) e) - | Twolong mr1 mr2, Some Tlong => + | Twolong mr1 mr2, Tlong => if Archi.ptr64 then None else Some (add_equation (Eq Low r (R mr2)) (add_equation (Eq High r (R mr1)) e)) | _, _ => @@ -1088,7 +1088,7 @@ Definition transfer_aux (f: RTL.function) (env: regenv) | BStailcall sg ros args mv1 ros' => let args' := loc_arguments sg in assertion (tailcall_is_possible sg); - assertion (opt_typ_eq sg.(sig_res) f.(RTL.fn_sig).(sig_res)); + assertion (rettype_eq sg.(sig_res) f.(RTL.fn_sig).(sig_res)); assertion (ros_compatible_tailcall ros'); do e1 <- add_equation_ros ros ros' empty_eqs; do e2 <- add_equations_args args (sig_args sg) args' e1; @@ -1118,7 +1118,7 @@ Definition transfer_aux (f: RTL.function) (env: regenv) track_moves env mv empty_eqs | BSreturn (Some arg) mv => let arg' := loc_result (RTL.fn_sig f) in - do e1 <- add_equations_res arg (sig_res (RTL.fn_sig f)) arg' empty_eqs; + do e1 <- add_equations_res arg (proj_sig_res (RTL.fn_sig f)) arg' empty_eqs; track_moves env mv e1 end. diff --git a/backend/Allocproof.v b/backend/Allocproof.v index 3d8fb451..b6880860 100644 --- a/backend/Allocproof.v +++ b/backend/Allocproof.v @@ -1301,10 +1301,10 @@ Proof. Qed. Lemma add_equations_res_lessdef: - forall r oty l e e' rs ls, - add_equations_res r oty l e = Some e' -> + forall r ty l e e' rs ls, + add_equations_res r ty l e = Some e' -> satisf rs ls e' -> - Val.has_type rs#r (match oty with Some ty => ty | None => Tint end) -> + Val.has_type rs#r ty -> Val.lessdef rs#r (Locmap.getpair (map_rpair R l) ls). Proof. intros. functional inversion H; simpl. @@ -1892,7 +1892,7 @@ Qed. Inductive match_stackframes: list RTL.stackframe -> list LTL.stackframe -> signature -> Prop := | match_stackframes_nil: forall sg, - sg.(sig_res) = Some Tint -> + sg.(sig_res) = Tint -> match_stackframes nil nil sg | match_stackframes_cons: forall res f sp pc rs s tf bb ls ts sg an e env @@ -2498,13 +2498,13 @@ Proof. (return_regs (parent_locset ts) ls1)) with (Locmap.getpair (map_rpair R (loc_result (RTL.fn_sig f))) ls1). eapply add_equations_res_lessdef; eauto. - rewrite H13. apply WTRS. + rewrite <- H14. apply WTRS. generalize (loc_result_caller_save (RTL.fn_sig f)). destruct (loc_result (RTL.fn_sig f)); simpl. intros A; rewrite A; auto. intros [A B]; rewrite A, B; auto. apply return_regs_agree_callee_save. - unfold proj_sig_res. rewrite <- H11; rewrite H13. apply WTRS. + rewrite <- H11, <- H14. apply WTRS. (* internal function *) - monadInv FUN. simpl in *. @@ -2536,7 +2536,8 @@ Proof. simpl. destruct (loc_result (ef_sig ef)) eqn:RES; simpl. rewrite Locmap.gss; auto. generalize (loc_result_pair (ef_sig ef)); rewrite RES; intros (A & B & C & D & E). - exploit external_call_well_typed; eauto. unfold proj_sig_res; rewrite B. intros WTRES'. + assert (WTRES': Val.has_type v' Tlong). + { rewrite <- B. eapply external_call_well_typed; eauto. } rewrite Locmap.gss. rewrite Locmap.gso by (red; auto). rewrite Locmap.gss. rewrite val_longofwords_eq_1 by auto. auto. red; intros. rewrite (AG l H0). diff --git a/backend/Asmexpandaux.ml b/backend/Asmexpandaux.ml index b1d822db..cc171cae 100644 --- a/backend/Asmexpandaux.ml +++ b/backend/Asmexpandaux.ml @@ -100,7 +100,7 @@ let translate_annot sp preg_to_dwarf annot = | a::_ -> aux a) let builtin_nop = - let signature ={sig_args = []; sig_res = None; sig_cc = cc_default} in + let signature ={sig_args = []; sig_res = Tvoid; sig_cc = cc_default} in let name = coqstring_of_camlstring "__builtin_nop" in Pbuiltin(EF_builtin(name,signature),[],BR_none) diff --git a/backend/CSE2.v b/backend/CSE2.v index 38a46c1b..41adba7b 100644 --- a/backend/CSE2.v +++ b/backend/CSE2.v @@ -29,13 +29,30 @@ Proof. decide equality. Defined. +Definition pset := PTree.t unit. + +Definition pset_inter : pset -> pset -> pset := + PTree.combine_null + (fun ov1 ov2 => Some tt). + +Definition pset_empty : pset := PTree.empty unit. +Definition pset_add (i : positive) (s : pset) := PTree.set i tt s. +Definition pset_remove (i : positive) (s : pset) := PTree.remove i s. + +Record relmap := mkrel { + var_to_sym : PTree.t sym_val ; + mem_used : pset ; + reg_used : PTree.t pset + }. + Module RELATION. - -Definition t := (PTree.t sym_val). + +Definition t := relmap. + Definition eq (r1 r2 : t) := - forall x, (PTree.get x r1) = (PTree.get x r2). + forall x, (PTree.get x (var_to_sym r1)) = (PTree.get x (var_to_sym r2)). -Definition top : t := PTree.empty sym_val. +Definition top : t := mkrel (PTree.empty sym_val) pset_empty (PTree.empty pset). Lemma eq_refl: forall x, eq x x. Proof. @@ -58,27 +75,27 @@ Qed. Definition sym_val_beq (x y : sym_val) := if eq_sym_val x y then true else false. -Definition beq (r1 r2 : t) := PTree.beq sym_val_beq r1 r2. +Definition beq (r1 r2 : t) := PTree.beq sym_val_beq (var_to_sym r1) (var_to_sym r2). Lemma beq_correct: forall r1 r2, beq r1 r2 = true -> eq r1 r2. Proof. unfold beq, eq. intros r1 r2 EQ x. - pose proof (PTree.beq_correct sym_val_beq r1 r2) as CORRECT. + pose proof (PTree.beq_correct sym_val_beq (var_to_sym r1) (var_to_sym r2)) as CORRECT. destruct CORRECT as [CORRECTF CORRECTB]. pose proof (CORRECTF EQ x) as EQx. clear CORRECTF CORRECTB EQ. unfold sym_val_beq in *. - destruct (r1 ! x) as [R1x | ] in *; - destruct (r2 ! x) as [R2x | ] in *; + destruct ((var_to_sym r1) ! x) as [R1x | ] in *; + destruct ((var_to_sym r2) ! x) as [R2x | ] in *; trivial; try contradiction. destruct (eq_sym_val R1x R2x) in *; congruence. Qed. Definition ge (r1 r2 : t) := forall x, - match PTree.get x r1 with + match PTree.get x (var_to_sym r1) with | None => True - | Some v => (PTree.get x r2) = Some v + | Some v => (PTree.get x (var_to_sym r2)) = Some v end. Lemma ge_refl: forall r1 r2, eq r1 r2 -> ge r1 r2. @@ -87,7 +104,7 @@ Proof. intros r1 r2 EQ x. pose proof (EQ x) as EQx. clear EQ. - destruct (r1 ! x). + destruct ((var_to_sym r1) ! x). - congruence. - trivial. Qed. @@ -98,12 +115,13 @@ Proof. intros r1 r2 r3 GE12 GE23 x. pose proof (GE12 x) as GE12x; clear GE12. pose proof (GE23 x) as GE23x; clear GE23. - destruct (r1 ! x); trivial. - destruct (r2 ! x); congruence. + destruct ((var_to_sym r1) ! x); trivial. + destruct ((var_to_sym r2) ! x); congruence. Qed. Definition lub (r1 r2 : t) := - PTree.combine + mkrel + (PTree.combine (fun ov1 ov2 => match ov1, ov2 with | (Some v1), (Some v2) => @@ -113,12 +131,19 @@ Definition lub (r1 r2 : t) := | None, _ | _, None => None end) - r1 r2. + (var_to_sym r1) (var_to_sym r2)) + (pset_inter (mem_used r1) (mem_used r2)) + (PTree.combine_null + (fun x y => let r := pset_inter x y in + if PTree.bempty_canon r + then None + else Some r) + (reg_used r1) (reg_used r2)). Lemma ge_lub_left: forall x y, ge (lub x y) x. Proof. unfold ge, lub. - intros r1 r2 x. + intros r1 r2 x. simpl. rewrite PTree.gcombine by reflexivity. destruct (_ ! _); trivial. destruct (_ ! _); trivial. @@ -128,7 +153,7 @@ Qed. Lemma ge_lub_right: forall x y, ge (lub x y) y. Proof. unfold ge, lub. - intros r1 r2 x. + intros r1 r2 x. simpl. rewrite PTree.gcombine by reflexivity. destruct (_ ! _); trivial. destruct (_ ! _); trivial. @@ -250,21 +275,53 @@ Module ADD_BOTTOM(L : SEMILATTICE_WITHOUT_BOTTOM). - apply L.ge_refl. apply L.eq_refl. Qed. + + Definition top := Some RELATION.top. End ADD_BOTTOM. Module RB := ADD_BOTTOM(RELATION). Module DS := Dataflow_Solver(RB)(NodeSetForward). -Definition kill_sym_val (dst : reg) (sv : sym_val) := +Definition kill_sym_val (dst : reg) (sv : sym_val) : bool := match sv with | SMove src => if peq dst src then true else false | SOp op args => List.existsb (peq dst) args | SLoad chunk addr args => List.existsb (peq dst) args end. - -Definition kill_reg (dst : reg) (rel : RELATION.t) := - PTree.filter1 (fun x => negb (kill_sym_val dst x)) - (PTree.remove dst rel). + +Definition referenced_by sv := + match sv with + | SMove src => src :: nil + | SOp op args => args + | SLoad chunk addr args => args + end. + +Definition referenced_by' osv := + match osv with + | None => nil + | Some sv => referenced_by sv + end. + +Definition remove_from_sets + (to_remove : reg) : + list reg -> PTree.t pset -> PTree.t pset := + List.fold_left + (fun sets reg => + match PTree.get reg sets with + | None => sets + | Some xset => + let xset' := PTree.remove to_remove xset in + if PTree.bempty_canon xset' + then PTree.remove reg sets + else PTree.set reg xset' sets + end). + +Definition kill_reg (dst : reg) (rel : RELATION.t) : RELATION.t := + let rel' := PTree.remove dst (var_to_sym rel) in + mkrel (PTree.filter1 (fun x => negb (kill_sym_val dst x)) rel') + (pset_remove dst (mem_used rel)) + (remove_from_sets dst (referenced_by' (PTree.get dst (var_to_sym rel))) + (PTree.remove dst (reg_used rel))). Definition kill_sym_val_mem (sv: sym_val) := match sv with @@ -274,17 +331,23 @@ Definition kill_sym_val_mem (sv: sym_val) := end. Definition kill_mem (rel : RELATION.t) := - PTree.filter1 (fun x => negb (kill_sym_val_mem x)) rel. + mkrel + (PTree.remove_t (var_to_sym rel) (mem_used rel)) + pset_empty + (reg_used rel). (* FIXME *) Definition forward_move (rel : RELATION.t) (x : reg) : reg := - match rel ! x with + match (var_to_sym rel) ! x with | Some (SMove org) => org | _ => x end. Definition move (src dst : reg) (rel : RELATION.t) := - PTree.set dst (SMove (forward_move rel src)) (kill_reg dst rel). + let rel0 := kill_reg dst rel in + mkrel (PTree.set dst (SMove (forward_move rel src)) (var_to_sym rel0)) + (mem_used rel0) + (reg_used rel0). (* FIXME *) Definition find_op_fold op args (already : option reg) x sv := match already with @@ -300,7 +363,7 @@ Definition find_op_fold op args (already : option reg) x sv := end. Definition find_op (rel : RELATION.t) (op : operation) (args : list reg) := - PTree.fold (find_op_fold op args) rel None. + PTree.fold (find_op_fold op args) (var_to_sym rel) None. Definition find_load_fold chunk addr args (already : option reg) x sv := match already with @@ -318,37 +381,42 @@ Definition find_load_fold chunk addr args (already : option reg) x sv := end. Definition find_load (rel : RELATION.t) (chunk : memory_chunk) (addr : addressing) (args : list reg) := - PTree.fold (find_load_fold chunk addr args) rel None. + PTree.fold (find_load_fold chunk addr args) (var_to_sym rel) None. Definition oper2 (op: operation) (dst : reg) (args : list reg) - (rel : RELATION.t) := + (rel : RELATION.t) : RELATION.t := let rel' := kill_reg dst rel in - PTree.set dst (SOp op (List.map (forward_move rel') args)) rel'. + mkrel (PTree.set dst (SOp op (List.map (forward_move rel') args)) (var_to_sym rel')) + (if op_depends_on_memory op then (pset_add dst (mem_used rel')) + else mem_used rel') + (reg_used rel'). (* FIXME *) Definition oper1 (op: operation) (dst : reg) (args : list reg) - (rel : RELATION.t) := + (rel : RELATION.t) : RELATION.t := if List.in_dec peq dst args then kill_reg dst rel else oper2 op dst args rel. Definition oper (op: operation) (dst : reg) (args : list reg) - (rel : RELATION.t) := + (rel : RELATION.t) : RELATION.t := match find_op rel op (List.map (forward_move rel) args) with | Some r => move r dst rel | None => oper1 op dst args rel end. Definition gen_oper (op: operation) (dst : reg) (args : list reg) - (rel : RELATION.t) := + (rel : RELATION.t) : RELATION.t := match op, args with | Omove, src::nil => move src dst rel | _, _ => oper op dst args rel end. Definition load2 (chunk: memory_chunk) (addr : addressing) - (dst : reg) (args : list reg) (rel : RELATION.t) := + (dst : reg) (args : list reg) (rel : RELATION.t) : RELATION.t := let rel' := kill_reg dst rel in - PTree.set dst (SLoad chunk addr (List.map (forward_move rel') args)) rel'. + mkrel (PTree.set dst (SLoad chunk addr (List.map (forward_move rel') args)) (var_to_sym rel')) + (pset_add dst (mem_used rel')) + (reg_used rel'). (* FIXME *) Definition load1 (chunk: memory_chunk) (addr : addressing) (dst : reg) (args : list reg) (rel : RELATION.t) := @@ -415,7 +483,7 @@ Definition apply_instr' code (pc : node) (ro : RB.t) : RB.t := Definition forward_map (f : RTL.function) := DS.fixpoint (RTL.fn_code f) RTL.successors_instr - (apply_instr' (RTL.fn_code f)) (RTL.fn_entrypoint f) (Some RELATION.top). + (apply_instr' (RTL.fn_code f)) (RTL.fn_entrypoint f) RB.top. Definition forward_move_b (rb : RB.t) (x : reg) := match rb with @@ -457,7 +525,7 @@ Definition transf_instr (fmap : option (PMap.t RB.t)) match instr with | Iop op args dst s => let args' := subst_args fmap pc args in - match find_op_in_fmap fmap pc op args' with + match (if is_trivial_op op then None else find_op_in_fmap fmap pc op args') with | None => Iop op args' dst s | Some src => Iop Omove (src::nil) dst s end diff --git a/backend/CSE2proof.v b/backend/CSE2proof.v index 254cc4ce..577b1e69 100644 --- a/backend/CSE2proof.v +++ b/backend/CSE2proof.v @@ -37,6 +37,515 @@ Proof. assumption. Qed. +Lemma gpset_inter_none: forall a b i, + (pset_inter a b) ! i = None <-> + (a ! i = None) \/ (b ! i = None). +Proof. + intros. unfold pset_inter. + rewrite PTree.gcombine_null. + destruct (a ! i); destruct (b ! i); intuition discriminate. +Qed. + +Lemma some_some: + forall x : option unit, + x <> None <-> x = Some tt. +Proof. + destruct x as [[] | ]; split; congruence. +Qed. + +Lemma gpset_inter_some: forall a b i, + (pset_inter a b) ! i = Some tt <-> + (a ! i = Some tt) /\ (b ! i = Some tt). +Proof. + intros. unfold pset_inter. + rewrite PTree.gcombine_null. + destruct (a ! i) as [[] | ]; destruct (b ! i) as [[] | ]; intuition congruence. +Qed. + +Definition wellformed_mem (rel : RELATION.t) : Prop := + forall i sv, + (var_to_sym rel) ! i = Some sv -> + kill_sym_val_mem sv = true -> + (mem_used rel) ! i = Some tt. + +Definition wellformed_reg (rel : RELATION.t) : Prop := + forall i j sv, + (var_to_sym rel) ! i = Some sv -> + kill_sym_val j sv = true -> + match (reg_used rel) ! j with + | Some uses => uses ! i = Some tt + | None => False + end. + +Lemma wellformed_mem_top : wellformed_mem RELATION.top. +Proof. + unfold wellformed_mem, RELATION.top, pset_empty. + simpl. + intros. + rewrite PTree.gempty in *. + discriminate. +Qed. +Local Hint Resolve wellformed_mem_top : wellformed. + +Lemma wellformed_reg_top : wellformed_reg RELATION.top. +Proof. + unfold wellformed_reg, RELATION.top, pset_empty. + simpl. + intros. + rewrite PTree.gempty in *. + discriminate. +Qed. +Local Hint Resolve wellformed_reg_top : wellformed. + +Lemma wellformed_mem_lub : forall a b, + (wellformed_mem a) -> (wellformed_mem b) -> (wellformed_mem (RELATION.lub a b)). +Proof. + unfold wellformed_mem, RELATION.lub. + simpl. + intros a b Ha Hb. + intros i sv COMBINE KILLABLE. + rewrite PTree.gcombine in *. + 2: reflexivity. + destruct (var_to_sym a) ! i as [syma | ] eqn:SYMA; + destruct (var_to_sym b) ! i as [symb | ] eqn:SYMB; + try discriminate. + destruct (eq_sym_val syma symb); try discriminate. + subst syma. + inv COMBINE. + apply gpset_inter_some. + split; eauto. +Qed. +Local Hint Resolve wellformed_mem_lub : wellformed. + +Lemma wellformed_reg_lub : forall a b, + (wellformed_reg a) -> (wellformed_reg b) -> (wellformed_reg (RELATION.lub a b)). +Proof. + unfold wellformed_reg, RELATION.lub. + simpl. + intros a b Ha Hb. + intros i j sv COMBINE KILLABLE. + specialize Ha with (i := i) (j := j). + specialize Hb with (i := i) (j := j). + rewrite PTree.gcombine in *. + 2: reflexivity. + destruct (var_to_sym a) ! i as [syma | ] eqn:SYMA; + destruct (var_to_sym b) ! i as [symb | ] eqn:SYMB; + try discriminate. + specialize Ha with (sv := syma). + specialize Hb with (sv := symb). + destruct (eq_sym_val syma symb); try discriminate. + subst syma. + inv COMBINE. + rewrite PTree.gcombine_null. + destruct ((reg_used a) ! j) as [uA| ]; destruct ((reg_used b) ! j) as [uB | ]; auto. + { pose proof (PTree.bempty_canon_correct (pset_inter uA uB) i) as EMPTY. + destruct PTree.bempty_canon. + - rewrite gpset_inter_none in EMPTY. + intuition congruence. + - rewrite gpset_inter_some. + auto. + } +Qed. +Local Hint Resolve wellformed_reg_lub : wellformed. + +Lemma wellformed_mem_kill_reg: + forall dst rel, + (wellformed_mem rel) -> (wellformed_mem (kill_reg dst rel)). +Proof. + unfold wellformed_mem, kill_reg, pset_remove. + simpl. + intros dst rel Hrel. + intros i sv KILLREG KILLABLE. + rewrite PTree.gfilter1 in KILLREG. + destruct (peq dst i). + { subst i. + rewrite PTree.grs in *. + discriminate. + } + rewrite PTree.gro in * by congruence. + specialize Hrel with (i := i). + eapply Hrel. + 2: eassumption. + destruct (_ ! i); try discriminate. + destruct negb; congruence. +Qed. +Local Hint Resolve wellformed_mem_kill_reg : wellformed. + +Lemma kill_sym_val_referenced: + forall dst, + forall sv, + (kill_sym_val dst sv)=true <-> In dst (referenced_by sv). +Proof. + intros. + destruct sv; simpl. + - destruct peq; intuition congruence. + - rewrite existsb_exists. + split. + + intros [x [IN EQ]]. + destruct peq. + * subst x; trivial. + * discriminate. + + intro. + exists dst. + split; trivial. + destruct peq; trivial. + congruence. + - rewrite existsb_exists. + split. + + intros [x [IN EQ]]. + destruct peq. + * subst x; trivial. + * discriminate. + + intro. + exists dst. + split; trivial. + destruct peq; trivial. + congruence. +Qed. +Local Hint Resolve kill_sym_val_referenced : wellformed. + +Lemma remove_from_sets_notin: + forall dst l sets j, + not (In j l) -> + (remove_from_sets dst l sets) ! j = sets ! j. +Proof. + induction l; simpl; trivial. + intros. + rewrite IHl by tauto. + destruct (@PTree.get (PTree.t unit) a sets) eqn:SETSA; trivial. + pose proof (PTree.bempty_canon_correct (PTree.remove dst t)) as CORRECT. + destruct (PTree.bempty_canon (PTree.remove dst t)). + - apply PTree.gro. + intuition. + - rewrite PTree.gso by intuition. + trivial. +Qed. + +Lemma remove_from_sets_pass: + forall dst l sets i j, + i <> dst -> + match sets ! j with + | Some uses => uses ! i = Some tt + | None => False + end -> + match (remove_from_sets dst l sets) ! j with + | Some uses => uses ! i = Some tt + | None => False + end. +Proof. + induction l; simpl; trivial. + intros. + apply IHl; trivial. + destruct (@PTree.get (PTree.t unit) a sets) eqn:SETSA; trivial. + pose proof (PTree.bempty_canon_correct (PTree.remove dst t)) as CORRECT. + specialize CORRECT with (i := i). + destruct (PTree.bempty_canon (PTree.remove dst t)). + - rewrite PTree.gro in CORRECT by congruence. + destruct (peq a j). + + subst a. + rewrite SETSA in *. + intuition congruence. + + rewrite PTree.gro by congruence. + assumption. + - destruct (peq a j). + + subst a. + rewrite SETSA in *. + rewrite PTree.gss. + rewrite PTree.gro by congruence. + assumption. + + rewrite PTree.gso by congruence. + assumption. +Qed. +Local Hint Resolve remove_from_sets_pass : wellformed. + +Lemma rem_comes_from: + forall A x y (tr: PTree.t A) v, + (PTree.remove x tr) ! y = Some v -> tr ! y = Some v. +Proof. + intros. + destruct (peq x y). + - subst y. + rewrite PTree.grs in *. + discriminate. + - rewrite PTree.gro in * by congruence. + assumption. +Qed. +Local Hint Resolve rem_comes_from : wellformed. + +Lemma rem_ineq: + forall A x y (tr: PTree.t A) v, + (PTree.remove x tr) ! y = Some v -> x<>y. +Proof. + intros. + intro. + subst y. + rewrite PTree.grs in *. + discriminate. +Qed. +Local Hint Resolve rem_ineq : wellformed. + +Lemma wellformed_reg_kill_reg: + forall dst rel, + (wellformed_reg rel) -> (wellformed_reg (kill_reg dst rel)). +Proof. + unfold wellformed_reg, kill_reg. + simpl. + intros dst rel Hrel. + intros i j sv KILLREG KILLABLE. + + rewrite PTree.gfilter1 in KILLREG. + destruct PTree.get eqn:REMi in KILLREG. + 2: discriminate. + destruct negb eqn:NEGB in KILLREG. + 2: discriminate. + inv KILLREG. + + assert ((var_to_sym rel) ! i = Some sv) as RELi by eauto with wellformed. + + destruct (peq dst j). + { (* absurd case *) + subst j. + rewrite KILLABLE in NEGB. + simpl in NEGB. + discriminate. + } + specialize Hrel with (i := i) (j := j) (sv := sv). + destruct ((var_to_sym rel) ! dst) eqn:DST; simpl. + { + assert (dst <> i) by eauto with wellformed. + apply remove_from_sets_pass. + congruence. + rewrite PTree.gro by congruence. + apply Hrel; trivial. + } + rewrite PTree.gro by congruence. + apply Hrel; trivial. +Qed. +Local Hint Resolve wellformed_reg_kill_reg : wellformed. + +Lemma wellformed_mem_kill_mem: + forall rel, + (wellformed_mem rel) -> (wellformed_mem (kill_mem rel)). +Proof. + unfold wellformed_mem, kill_mem. + simpl. + intros rel Hrel. + intros i sv KILLMEM KILLABLE. + rewrite PTree.gremove_t in KILLMEM. + exfalso. + specialize Hrel with (i := i). + destruct ((var_to_sym rel) ! i) eqn:RELi. + - specialize Hrel with (sv := s). + destruct ((mem_used rel) ! i) eqn:USEDi. + discriminate. + inv KILLMEM. + intuition congruence. + - destruct ((mem_used rel) ! i); discriminate. +Qed. +Local Hint Resolve wellformed_mem_kill_mem : wellformed. + +Lemma wellformed_reg_kill_mem: + forall rel, + (wellformed_reg rel) -> (wellformed_reg (kill_mem rel)). +Proof. + unfold wellformed_reg, kill_mem. + simpl. + intros rel Hrel. + intros i j sv KILLMEM KILLABLE. + apply Hrel with (sv := sv); trivial. + rewrite PTree.gremove_t in KILLMEM. + destruct ((mem_used rel) ! i) in KILLMEM. + discriminate. + assumption. +Qed. +Local Hint Resolve wellformed_reg_kill_mem : wellformed. + +Lemma wellformed_mem_move: + forall r dst rel, + (wellformed_mem rel) -> (wellformed_mem (move r dst rel)). +Proof. + Local Opaque kill_reg. + intros; unfold move, wellformed_mem; simpl. + intros i sv MOVE KILL. + destruct (peq i dst). + { subst i. + rewrite PTree.gss in MOVE. + inv MOVE. + simpl in KILL. + discriminate. + } + rewrite PTree.gso in MOVE by congruence. + eapply wellformed_mem_kill_reg; eauto. +Qed. +Local Hint Resolve wellformed_mem_move : wellformed. + +Lemma wellformed_mem_oper2: + forall op dst args rel, + (wellformed_mem rel) -> + (wellformed_mem (oper2 op dst args rel)). +Proof. + intros until rel. intro WELLFORMED. + unfold oper2. + intros i sv MOVE OPER. + simpl in *. + destruct (peq i dst). + { subst i. + rewrite PTree.gss in MOVE. + inv MOVE. + simpl in OPER. + rewrite OPER. + apply PTree.gss. + } + unfold pset_add. + rewrite PTree.gso in MOVE by congruence. + destruct op_depends_on_memory. + - rewrite PTree.gso by congruence. + eapply wellformed_mem_kill_reg; eauto. + - eapply wellformed_mem_kill_reg; eauto. +Qed. +Local Hint Resolve wellformed_mem_oper2 : wellformed. + +Lemma wellformed_mem_oper1: + forall op dst args rel, + (wellformed_mem rel) -> + (wellformed_mem (oper1 op dst args rel)). +Proof. + unfold oper1. intros. + destruct in_dec ; auto with wellformed. +Qed. +Local Hint Resolve wellformed_mem_oper1 : wellformed. + +Lemma wellformed_mem_oper: + forall op dst args rel, + (wellformed_mem rel) -> + (wellformed_mem (oper op dst args rel)). +Proof. + unfold oper. intros. + destruct find_op ; auto with wellformed. +Qed. +Local Hint Resolve wellformed_mem_oper : wellformed. + +Lemma wellformed_mem_gen_oper: + forall op dst args rel, + (wellformed_mem rel) -> + (wellformed_mem (gen_oper op dst args rel)). +Proof. + intros. + unfold gen_oper. + destruct op; auto with wellformed. + destruct args; auto with wellformed. + destruct args; auto with wellformed. +Qed. +Local Hint Resolve wellformed_mem_gen_oper : wellformed. + +Lemma wellformed_mem_load2 : + forall chunk addr dst args rel, + (wellformed_mem rel) -> + (wellformed_mem (load2 chunk addr dst args rel)). +Proof. + intros. + unfold load2, wellformed_mem. + simpl. + intros i sv LOAD KILL. + destruct (peq i dst). + { subst i. + apply PTree.gss. + } + unfold pset_add. + rewrite PTree.gso in * by congruence. + eapply wellformed_mem_kill_reg; eauto. +Qed. +Local Hint Resolve wellformed_mem_load2 : wellformed. + +Lemma wellformed_mem_load1 : + forall chunk addr dst args rel, + (wellformed_mem rel) -> + (wellformed_mem (load1 chunk addr dst args rel)). +Proof. + intros. + unfold load1. + destruct in_dec; eauto with wellformed. +Qed. +Local Hint Resolve wellformed_mem_load1 : wellformed. + +Lemma wellformed_mem_load : + forall chunk addr dst args rel, + (wellformed_mem rel) -> + (wellformed_mem (load chunk addr dst args rel)). +Proof. + intros. + unfold load. + destruct find_load; eauto with wellformed. +Qed. +Local Hint Resolve wellformed_mem_load : wellformed. + +Definition wellformed_mem_rb (rb : RB.t) := + match rb with + | None => True + | Some r => wellformed_mem r + end. + +Lemma wellformed_mem_apply_instr: + forall instr rel, + (wellformed_mem rel) -> + (wellformed_mem_rb (apply_instr instr rel)). +Proof. + destruct instr; simpl; auto with wellformed. +Qed. +Local Hint Resolve wellformed_mem_apply_instr : wellformed. + +Lemma wellformed_mem_rb_bot : + wellformed_mem_rb RB.bot. +Proof. + simpl. + trivial. +Qed. +Local Hint Resolve wellformed_mem_rb_bot: wellformed. + +Lemma wellformed_mem_rb_top : + wellformed_mem_rb RB.top. +Proof. + simpl. + auto with wellformed. +Qed. +Local Hint Resolve wellformed_mem_rb_top: wellformed. + +Lemma wellformed_mem_rb_apply_instr': + forall code pc rel, + (wellformed_mem_rb rel) -> + (wellformed_mem_rb (apply_instr' code pc rel)). +Proof. + destruct rel; simpl; trivial. + intro. + destruct (code ! pc); + eauto with wellformed. +Qed. +Local Hint Resolve wellformed_mem_rb_apply_instr' : wellformed. + +Lemma wellformed_mem_rb_lub : forall a b, + (wellformed_mem_rb a) -> (wellformed_mem_rb b) -> (wellformed_mem_rb (RB.lub a b)). +Proof. + destruct a; destruct b; simpl; auto with wellformed. +Qed. +Local Hint Resolve wellformed_mem_rb_lub: wellformed. + +Definition wellformed_mem_fmap fmap := + forall i, wellformed_mem_rb (fmap !! i). + +Theorem wellformed_mem_forward_map : forall f, + forall fmap, (forward_map f) = Some fmap -> + wellformed_mem_fmap fmap. +Proof. + intros. + unfold forward_map in *. + unfold wellformed_mem_fmap. + intro. + eapply DS.fixpoint_invariant with (ev := Some RELATION.top); eauto with wellformed. +Qed. +Local Hint Resolve wellformed_mem_forward_map: wellformed. + +Local Transparent kill_reg. + Section SOUNDNESS. Variable F V : Type. Variable genv: Genv.t F V. @@ -61,7 +570,7 @@ Definition sem_sym_val sym rs (v : option val) : Prop := end. Definition sem_reg (rel : RELATION.t) (x : reg) (rs : regset) (v : val) : Prop := - match rel ! x with + match (var_to_sym rel) ! x with | None => True | Some sym => sem_sym_val sym rs (Some (rs # x)) end. @@ -101,7 +610,7 @@ Proof. pose proof (SEM arg) as SEMarg. simpl. unfold forward_move. unfold sem_sym_val in *. - destruct (t ! arg); trivial. + destruct (_ ! arg); trivial. destruct s; congruence. Qed. @@ -130,7 +639,7 @@ Lemma kill_reg_sound : Proof. unfold sem_rel, kill_reg, sem_reg, sem_sym_val. intros until v. - intros REL x. + intros REL x. simpl. rewrite PTree.gfilter1. destruct (Pos.eq_dec dst x). { @@ -140,7 +649,7 @@ Proof. } rewrite PTree.gro by congruence. rewrite Regmap.gso by congruence. - destruct (rel ! x) as [relx | ] eqn:RELx; trivial. + destruct (_ ! x) as [relx | ] eqn:RELx; trivial. unfold kill_sym_val. pose proof (REL x) as RELinstx. rewrite RELx in RELinstx. @@ -193,12 +702,13 @@ Proof. { subst x. unfold sem_reg. + simpl. rewrite PTree.gss. rewrite Regmap.gss. unfold sem_reg in *. simpl. unfold forward_move. - destruct (rel ! src) as [ sv |]; simpl. + destruct (_ ! src) as [ sv |]; simpl. destruct sv eqn:SV; simpl in *. { destruct (peq dst src0). @@ -214,6 +724,7 @@ Proof. } rewrite Regmap.gso by congruence. unfold sem_reg. + simpl. rewrite PTree.gso by congruence. rewrite Regmap.gso in KILL by congruence. exact KILL. @@ -226,9 +737,10 @@ Lemma move_cases_neq: Proof. intros until a. intro NEQ. unfold kill_reg, forward_move. + simpl. rewrite PTree.gfilter1. rewrite PTree.gro by congruence. - destruct (rel ! a); simpl. + destruct (_ ! a); simpl. 2: congruence. destruct s. { @@ -262,9 +774,10 @@ Proof. unfold kill_reg. unfold sem_reg in RELa. unfold forward_move. + simpl. rewrite PTree.gfilter1. rewrite PTree.gro by auto. - destruct (rel ! a); simpl; trivial. + destruct (_ ! a); simpl; trivial. destruct s; simpl in *; destruct negb; simpl; congruence. Qed. @@ -288,6 +801,7 @@ Proof. { subst x. unfold sem_reg. + simpl. rewrite PTree.gss. rewrite Regmap.gss. simpl. @@ -297,6 +811,7 @@ Proof. } rewrite Regmap.gso by congruence. unfold sem_reg. + simpl. rewrite PTree.gso by congruence. rewrite Regmap.gso in KILL by congruence. exact KILL. @@ -344,13 +859,13 @@ Proof. | Some src => eval_operation genv sp op rs ## args m = Some rs # src end -> fold_left (fun (a : option reg) (p : positive * sym_val) => - find_op_fold op args a (fst p) (snd p)) (PTree.elements rel) start = + find_op_fold op args a (fst p) (snd p)) (PTree.elements (var_to_sym rel)) start = Some src -> eval_operation genv sp op rs ## args m = Some rs # src) as REC. { unfold sem_rel, sem_reg in REL. - generalize (PTree.elements_complete rel). - generalize (PTree.elements rel). + generalize (PTree.elements_complete (var_to_sym rel)). + generalize (PTree.elements (var_to_sym rel)). induction l; simpl. { intros. @@ -375,7 +890,7 @@ Proof. destruct eq_args; trivial. subst args0. simpl. - assert ((rel ! r) = Some (SOp op args)) as RELatr. + assert (((var_to_sym rel) ! r) = Some (SOp op args)) as RELatr. { apply COMPLETE. left. @@ -426,7 +941,7 @@ Proof. end -> fold_left (fun (a : option reg) (p : positive * sym_val) => - find_load_fold chunk addr args a (fst p) (snd p)) (PTree.elements rel) start = + find_load_fold chunk addr args a (fst p) (snd p)) (PTree.elements (var_to_sym rel)) start = Some src -> match eval_addressing genv sp addr rs##args with | Some a => match Mem.loadv chunk m a with @@ -438,8 +953,8 @@ Proof. { unfold sem_rel, sem_reg in REL. - generalize (PTree.elements_complete rel). - generalize (PTree.elements rel). + generalize (PTree.elements_complete (var_to_sym rel)). + generalize (PTree.elements (var_to_sym rel)). induction l; simpl. { intros. @@ -466,7 +981,7 @@ Proof. destruct eq_args; trivial. subst args0. simpl. - assert ((rel ! r) = Some (SLoad chunk addr args)) as RELatr. + assert (((var_to_sym rel) ! r) = Some (SLoad chunk addr args)) as RELatr. { apply COMPLETE. left. @@ -562,7 +1077,7 @@ Proof. 2: (apply IHargs; assumption). unfold forward_move, sem_rel, sem_reg, sem_sym_val in *. pose proof (REL a) as RELa. - destruct (rel ! a); trivial. + destruct (_ ! a); trivial. destruct s; congruence. Qed. @@ -645,6 +1160,7 @@ Proof. { subst x. unfold sem_reg. + simpl. rewrite PTree.gss. rewrite Regmap.gss. simpl. @@ -657,7 +1173,7 @@ Proof. discriminate. } rewrite Regmap.gso by congruence. - unfold sem_reg. + unfold sem_reg. simpl. rewrite PTree.gso by congruence. rewrite Regmap.gso in KILL by congruence. exact KILL. @@ -682,7 +1198,7 @@ Proof. destruct (peq x dst). { subst x. - unfold sem_reg. + unfold sem_reg. simpl. rewrite PTree.gss. rewrite Regmap.gss. simpl. @@ -692,7 +1208,7 @@ Proof. trivial. } rewrite Regmap.gso by congruence. - unfold sem_reg. + unfold sem_reg. simpl. rewrite PTree.gso by congruence. rewrite Regmap.gso in KILL by congruence. exact KILL. @@ -719,7 +1235,7 @@ Proof. destruct (peq x dst). { subst x. - unfold sem_reg. + unfold sem_reg. simpl. rewrite PTree.gss. rewrite Regmap.gss. simpl. @@ -729,7 +1245,8 @@ Proof. right; trivial. } rewrite Regmap.gso by congruence. - unfold sem_reg. + unfold sem_reg. simpl. + simpl. rewrite PTree.gso by congruence. rewrite Regmap.gso in KILL by congruence. exact KILL. @@ -926,6 +1443,7 @@ Proof. intros REL x. pose proof (REL x) as RELx. unfold kill_reg, sem_reg in *. + simpl. rewrite PTree.gfilter1. destruct (peq res x). { subst x. @@ -933,7 +1451,7 @@ Proof. reflexivity. } rewrite PTree.gro by congruence. - destruct (mpc ! x) as [sv | ]; trivial. + destruct (_ ! x) as [sv | ]; trivial. destruct negb; trivial. Qed. @@ -956,8 +1474,8 @@ Proof. pose proof (RE x) as REx. pose proof (GE x) as GEx. unfold sem_reg in *. - destruct (r1 ! x) as [r1x | ] in *; - destruct (r2 ! x) as [r2x | ] in *; + destruct ((var_to_sym r1) ! x) as [r1x | ] in *; + destruct ((var_to_sym r2) ! x) as [r2x | ] in *; congruence. Qed. End SAME_MEMORY. @@ -966,23 +1484,33 @@ Lemma kill_mem_sound : forall m m' : mem, forall rel : RELATION.t, forall rs, + wellformed_mem rel -> sem_rel m rel rs -> sem_rel m' (kill_mem rel) rs. Proof. unfold sem_rel, sem_reg. intros until rs. - intros SEM x. - pose proof (SEM x) as SEMx. + intros WELLFORMED SEM x. + unfold wellformed_mem in *. + specialize SEM with (x := x). + specialize WELLFORMED with (i := x). unfold kill_mem. - rewrite PTree.gfilter1. + simpl. + rewrite PTree.gremove_t. unfold kill_sym_val_mem. - destruct (rel ! x) as [ sv | ]. - 2: reflexivity. - destruct sv; simpl in *; trivial. - { - destruct op_depends_on_memory eqn:DEPENDS; simpl; trivial. - rewrite SEMx. - apply op_depends_on_memory_correct; auto. - } + destruct ((var_to_sym rel) ! x) as [ sv | ] eqn:VAR. + - specialize WELLFORMED with (sv0 := sv). + destruct ((mem_used rel) ! x) eqn:USED; trivial. + unfold sem_sym_val in *. + destruct sv; simpl in *; trivial. + + rewrite op_depends_on_memory_correct with (m2 := m). + assumption. + destruct op_depends_on_memory; intuition congruence. + + intuition discriminate. + - replace (match (mem_used rel) ! x with + | Some _ | _ => None + end) with (@None sym_val) by + (destruct ((mem_used rel) ! x); trivial). + trivial. Qed. End SOUNDNESS. @@ -1123,6 +1651,39 @@ Ltac TR_AT := generalize (transf_function_at _ _ _ A); intros end. +Lemma wellformed_mem_mpc: + forall f map pc mpc, + (forward_map f) = Some map -> + map # pc = Some mpc -> + wellformed_mem mpc. +Proof. + intros. + assert (wellformed_mem_fmap map) by eauto with wellformed. + unfold wellformed_mem_fmap, wellformed_mem_rb in *. + specialize H1 with (i := pc). + rewrite H0 in H1. + assumption. +Qed. +Hint Resolve wellformed_mem_mpc : wellformed. + +Lemma match_same_option : + forall { A B : Type}, + forall x : option A, + forall y : B, + (match x with Some _ => y | None => y end) = y. +Proof. + destruct x; trivial. +Qed. + +Lemma match_same_bool : + forall { B : Type}, + forall x : bool, + forall y : B, + (if x then y else y) = y. +Proof. + destruct x; trivial. +Qed. + Lemma step_simulation: forall S1 t S2, RTL.step ge S1 t S2 -> forall S1', match_states S1 S1' -> @@ -1150,8 +1711,9 @@ Proof. reflexivity. - (* op *) unfold transf_instr in *. - destruct find_op_in_fmap eqn:FIND_OP. + destruct (if is_trivial_op op then None else find_op_in_fmap (forward_map f) pc op (subst_args (forward_map f) pc args)) eqn:FIND_OP. { + destruct is_trivial_op. discriminate. unfold find_op_in_fmap, fmap_sem', fmap_sem in *. destruct (forward_map f) as [map |] eqn:MAP. 2: discriminate. @@ -1468,8 +2030,7 @@ Proof. rewrite H. reflexivity. } - apply (kill_mem_sound' sp m). - assumption. + apply (kill_mem_sound' sp m); eauto with wellformed. (* call *) - econstructor; split. @@ -1499,8 +2060,7 @@ Proof. reflexivity. } apply kill_reg_sound. - apply (kill_mem_sound' sp m). - assumption. + apply (kill_mem_sound' sp m); eauto with wellformed. } (* tailcall *) @@ -1657,4 +2217,4 @@ Proof. exact step_simulation. Qed. -End PRESERVATION.
\ No newline at end of file +End PRESERVATION. diff --git a/backend/Cminor.v b/backend/Cminor.v index ca01ad50..91a4c104 100644 --- a/backend/Cminor.v +++ b/backend/Cminor.v @@ -676,12 +676,24 @@ Definition outcome_block (out: outcome) : outcome := | out => out end. +(* Definition outcome_result_value - (out: outcome) (retsig: option typ) (vres: val) : Prop := + (out: outcome) (retsig: rettype) (vres: val) : Prop := match out with | Out_normal => vres = Vundef | Out_return None => vres = Vundef - | Out_return (Some v) => retsig <> None /\ vres = v + | Out_return (Some v) => retsig <> Tvoid /\ vres = v + | Out_tailcall_return v => vres = v + | _ => False + end. +*) + +Definition outcome_result_value + (out: outcome) (vres: val) : Prop := + match out with + | Out_normal => vres = Vundef + | Out_return None => vres = Vundef + | Out_return (Some v) => vres = v | Out_tailcall_return v => vres = v | _ => False end. @@ -711,7 +723,7 @@ Inductive eval_funcall: Mem.alloc m 0 f.(fn_stackspace) = (m1, sp) -> set_locals f.(fn_vars) (set_params vargs f.(fn_params)) = e -> exec_stmt f (Vptr sp Ptrofs.zero) e m1 f.(fn_body) t e2 m2 out -> - outcome_result_value out f.(fn_sig).(sig_res) vres -> + outcome_result_value out vres -> outcome_free_mem out m2 sp f.(fn_stackspace) m3 -> eval_funcall m (Internal f) vargs t m3 vres | eval_funcall_external: @@ -995,7 +1007,7 @@ Proof. subst vres. replace k with (call_cont k') by congruence. apply star_one. apply step_return_0; auto. (* Out_return Some *) - destruct H3. subst vres. + subst vres. replace k with (call_cont k') by congruence. apply star_one. eapply step_return_1; eauto. (* Out_tailcall_return *) diff --git a/backend/Cminortyping.v b/backend/Cminortyping.v index fccbda27..92ec45f2 100644 --- a/backend/Cminortyping.v +++ b/backend/Cminortyping.v @@ -130,7 +130,7 @@ Definition opt_set (e: S.typenv) (optid: option ident) (ty: typ) : res S.typenv | Some id => S.set e id ty end. -Fixpoint type_stmt (tret: option typ) (e: S.typenv) (s: stmt) : res S.typenv := +Fixpoint type_stmt (tret: rettype) (e: S.typenv) (s: stmt) : res S.typenv := match s with | Sskip => OK e | Sassign id a => type_assign e id a @@ -141,7 +141,7 @@ Fixpoint type_stmt (tret: option typ) (e: S.typenv) (s: stmt) : res S.typenv := do e2 <- type_exprlist e1 args sg.(sig_args); opt_set e2 optid (proj_sig_res sg) | Stailcall sg fn args => - assertion (opt_typ_eq sg.(sig_res) tret); + assertion (rettype_eq sg.(sig_res) tret); do e1 <- type_expr e fn Tptr; type_exprlist e1 args sg.(sig_args) | Sbuiltin optid ef args => @@ -163,10 +163,14 @@ Fixpoint type_stmt (tret: option typ) (e: S.typenv) (s: stmt) : res S.typenv := | Sswitch sz a tbl dfl => type_expr e a (if sz then Tlong else Tint) | Sreturn opta => - match opta, tret with - | None, _ => OK e - | Some a, Some t => type_expr e a t - | _, _ => Error (msg "inconsistent return") + match opta with + | None => OK e + | Some a => type_expr e a (proj_rettype tret) +(* + if rettype_eq tret Tvoid + then Error (msg "inconsistent return") + else type_expr e a (proj_rettype tret) +*) end | Slabel lbl s1 => type_stmt tret e s1 @@ -186,7 +190,7 @@ Definition type_function (f: function) : res typenv := Section SPEC. Variable env: ident -> typ. -Variable tret: option typ. +Variable tret: rettype. Inductive wt_expr: expr -> typ -> Prop := | wt_Evar: forall id, @@ -205,9 +209,9 @@ Inductive wt_expr: expr -> typ -> Prop := wt_expr a1 Tptr -> wt_expr (Eload chunk a1) (type_of_chunk chunk). -Definition wt_opt_assign (optid: option ident) (optty: option typ) : Prop := +Definition wt_opt_assign (optid: option ident) (ty: rettype) : Prop := match optid with - | Some id => match optty with Some ty => ty | None => Tint end = env id + | Some id => proj_rettype ty = env id | _ => True end. @@ -251,8 +255,8 @@ Inductive wt_stmt: stmt -> Prop := wt_stmt (Sswitch sz a tbl dfl) | wt_Sreturn_none: wt_stmt (Sreturn None) - | wt_Sreturn_some: forall a t, - tret = Some t -> wt_expr a t -> + | wt_Sreturn_some: forall a, + wt_expr a (proj_rettype tret) -> wt_stmt (Sreturn (Some a)) | wt_Slabel: forall lbl s1, wt_stmt s1 -> @@ -393,7 +397,7 @@ Proof. - constructor; eauto. - constructor. - constructor; eauto using type_expr_sound with ty. -- destruct tret, o; try (monadInv T); econstructor; eauto using type_expr_sound with ty. +- destruct o; try (monadInv T); econstructor; eauto using type_expr_sound with ty. - constructor; eauto. - constructor. Qed. @@ -414,9 +418,9 @@ Definition wt_env (env: typenv) (e: Cminor.env) : Prop := Definition def_env (f: function) (e: Cminor.env) : Prop := forall id, In id f.(fn_params) \/ In id f.(fn_vars) -> exists v, e!id = Some v. -Inductive wt_cont_call: cont -> option typ -> Prop := +Inductive wt_cont_call: cont -> rettype -> Prop := | wt_cont_Kstop: - wt_cont_call Kstop (Some Tint) + wt_cont_call Kstop Tint | wt_cont_Kcall: forall optid f sp e k tret env (WT_FN: wt_function env f) (WT_CONT: wt_cont env f.(fn_sig).(sig_res) k) @@ -425,7 +429,7 @@ Inductive wt_cont_call: cont -> option typ -> Prop := (WT_DEST: wt_opt_assign env optid tret), wt_cont_call (Kcall optid f sp e k) tret -with wt_cont: typenv -> option typ -> cont -> Prop := +with wt_cont: typenv -> rettype -> cont -> Prop := | wt_cont_Kseq: forall env tret s k, wt_stmt env tret s -> wt_cont env tret k -> @@ -451,7 +455,7 @@ Inductive wt_state: state -> Prop := (WT_CONT: wt_cont_call k (funsig f).(sig_res)), wt_state (Callstate f args k m) | wt_return_state: forall v k m tret - (WT_RES: Val.has_type v (match tret with None => Tint | Some t => t end)) + (WT_RES: Val.has_type v (proj_rettype tret)) (WT_CONT: wt_cont_call k tret), wt_state (Returnstate v k m). @@ -651,9 +655,8 @@ Proof. rewrite H8; eapply call_cont_wt; eauto. - inv WT_STMT. exploit external_call_well_typed; eauto. intros TRES. econstructor; eauto using wt_Sskip. - unfold proj_sig_res in TRES; red in H5. - destruct optid. rewrite H5 in TRES. apply wt_env_assign; auto. assumption. - destruct optid. apply def_env_assign; auto. assumption. + destruct optid; auto. apply wt_env_assign; auto. rewrite <- H5; auto. + destruct optid; auto. apply def_env_assign; auto. - inv WT_STMT. econstructor; eauto. econstructor; eauto. - inv WT_STMT. destruct b; econstructor; eauto. - inv WT_STMT. econstructor; eauto. econstructor; eauto. constructor; auto. @@ -664,7 +667,7 @@ Proof. - econstructor; eauto using wt_Sexit. - inv WT_STMT. econstructor; eauto using call_cont_wt. exact I. - inv WT_STMT. econstructor; eauto using call_cont_wt. - rewrite H2. eapply wt_eval_expr; eauto. + eapply wt_eval_expr; eauto. - inv WT_STMT. econstructor; eauto. - inversion WT_FN; subst. assert (WT_CK: wt_cont env (sig_res (fn_sig f)) (call_cont k)). @@ -675,7 +678,7 @@ Proof. constructor; auto. apply wt_env_set_locals. apply wt_env_set_params. rewrite H2; auto. red; intros. apply def_set_locals. destruct H4; auto. left; apply def_set_params; auto. -- exploit external_call_well_typed; eauto. unfold proj_sig_res. simpl in *. intros. +- exploit external_call_well_typed; eauto. intros. econstructor; eauto. - inv WT_CONT. econstructor; eauto using wt_Sskip. red in WT_DEST. diff --git a/backend/Conventions.v b/backend/Conventions.v index 6025c6b4..14ffb587 100644 --- a/backend/Conventions.v +++ b/backend/Conventions.v @@ -34,6 +34,73 @@ Proof. apply IHpl; auto. Qed. +(** ** Stack size of function arguments *) + +(** [size_arguments s] returns the number of [Outgoing] slots used + to call a function with signature [s]. *) + +Definition max_outgoing_1 (accu: Z) (l: loc) : Z := + match l with + | S Outgoing ofs ty => Z.max accu (ofs + typesize ty) + | _ => accu + end. + +Definition max_outgoing_2 (accu: Z) (rl: rpair loc) : Z := + match rl with + | One l => max_outgoing_1 accu l + | Twolong l1 l2 => max_outgoing_1 (max_outgoing_1 accu l1) l2 + end. + +Definition size_arguments (s: signature) : Z := + List.fold_left max_outgoing_2 (loc_arguments s) 0. + +(** The offsets of [Outgoing] arguments are below [size_arguments s]. *) + +Remark fold_max_outgoing_above: + forall l n, fold_left max_outgoing_2 l n >= n. +Proof. + assert (A: forall n l, max_outgoing_1 n l >= n). + { intros; unfold max_outgoing_1. destruct l as [_ | []]; xomega. } + induction l; simpl; intros. + - omega. + - eapply Zge_trans. eauto. + destruct a; simpl. apply A. eapply Zge_trans; eauto. +Qed. + +Lemma size_arguments_above: + forall s, size_arguments s >= 0. +Proof. + intros. apply fold_max_outgoing_above. +Qed. + +Lemma loc_arguments_bounded: + forall (s: signature) (ofs: Z) (ty: typ), + In (S Outgoing ofs ty) (regs_of_rpairs (loc_arguments s)) -> + ofs + typesize ty <= size_arguments s. +Proof. + intros until ty. + assert (A: forall n l, n <= max_outgoing_1 n l). + { intros; unfold max_outgoing_1. destruct l as [_ | []]; xomega. } + assert (B: forall p n, + In (S Outgoing ofs ty) (regs_of_rpair p) -> + ofs + typesize ty <= max_outgoing_2 n p). + { intros. destruct p; simpl in H; intuition; subst; simpl. + - xomega. + - eapply Z.le_trans. 2: apply A. xomega. + - xomega. } + assert (C: forall l n, + In (S Outgoing ofs ty) (regs_of_rpairs l) -> + ofs + typesize ty <= fold_left max_outgoing_2 l n). + { induction l; simpl; intros. + - contradiction. + - rewrite in_app_iff in H. destruct H. + + eapply Z.le_trans. eapply B; eauto. + apply Z.ge_le. apply fold_max_outgoing_above. + + apply IHl; auto. + } + apply C. +Qed. + (** ** Location of function parameters *) (** A function finds the values of its parameter in the same locations diff --git a/backend/Inliningaux.ml b/backend/Inliningaux.ml index 609b2637..d58704ca 100644 --- a/backend/Inliningaux.ml +++ b/backend/Inliningaux.ml @@ -16,7 +16,7 @@ open FSetAVL open Maps open Op open Ordered -open !RTL +open! RTL module PSet = Make(OrderedPositive) diff --git a/backend/OpHelpers.v b/backend/OpHelpers.v index 53414dab..b9b97903 100644 --- a/backend/OpHelpers.v +++ b/backend/OpHelpers.v @@ -6,16 +6,16 @@ Require Import Op CminorSel. runtime library functions. The following type class collects the names of these functions. *) -Definition sig_l_l := mksignature (Tlong :: nil) (Some Tlong) cc_default. -Definition sig_l_f := mksignature (Tlong :: nil) (Some Tfloat) cc_default. -Definition sig_l_s := mksignature (Tlong :: nil) (Some Tsingle) cc_default. -Definition sig_f_l := mksignature (Tfloat :: nil) (Some Tlong) cc_default. -Definition sig_ll_l := mksignature (Tlong :: Tlong :: nil) (Some Tlong) cc_default. -Definition sig_li_l := mksignature (Tlong :: Tint :: nil) (Some Tlong) cc_default. -Definition sig_ii_l := mksignature (Tint :: Tint :: nil) (Some Tlong) cc_default. -Definition sig_ii_i := mksignature (Tint :: Tint :: nil) (Some Tint) cc_default. -Definition sig_ff_f := mksignature (Tfloat :: Tfloat :: nil) (Some Tfloat) cc_default. -Definition sig_ss_s := mksignature (Tsingle :: Tsingle :: nil) (Some Tsingle) cc_default. +Definition sig_l_l := mksignature (Tlong :: nil) Tlong cc_default. +Definition sig_l_f := mksignature (Tlong :: nil) Tfloat cc_default. +Definition sig_l_s := mksignature (Tlong :: nil) Tsingle cc_default. +Definition sig_f_l := mksignature (Tfloat :: nil) Tlong cc_default. +Definition sig_ll_l := mksignature (Tlong :: Tlong :: nil) Tlong cc_default. +Definition sig_li_l := mksignature (Tlong :: Tint :: nil) Tlong cc_default. +Definition sig_ii_l := mksignature (Tint :: Tint :: nil) Tlong cc_default. +Definition sig_ii_i := mksignature (Tint :: Tint :: nil) Tint cc_default. +Definition sig_ff_f := mksignature (Tfloat :: Tfloat :: nil) Tfloat cc_default. +Definition sig_ss_s := mksignature (Tsingle :: Tsingle :: nil) Tsingle cc_default. Class helper_functions := mk_helper_functions { i64_dtos: ident; (**r float64 -> signed long *) diff --git a/backend/PrintAsmaux.ml b/backend/PrintAsmaux.ml index 8652b2c5..d82e6f84 100644 --- a/backend/PrintAsmaux.ml +++ b/backend/PrintAsmaux.ml @@ -99,7 +99,7 @@ let exists_constants () = let current_function_stacksize = ref 0l let current_function_sig = - ref { sig_args = []; sig_res = None; sig_cc = cc_default } + ref { sig_args = []; sig_res = Tvoid; sig_cc = cc_default } (* Functions for printing of symbol names *) let elf_symbol oc symb = @@ -268,8 +268,8 @@ let re_asm_param_2 = Str.regexp "%\\([QR]?\\)\\([0-9]+\\)" let print_inline_asm print_preg oc txt sg args res = let (operands, ty_operands) = match sg.sig_res with - | None -> (args, sg.sig_args) - | Some tres -> (builtin_arg_of_res res :: args, tres :: sg.sig_args) in + | Tvoid -> (args, sg.sig_args) + | tres -> (builtin_arg_of_res res :: args, proj_rettype tres :: sg.sig_args) in let print_fragment = function | Str.Text s -> output_string oc s diff --git a/backend/PrintCminor.ml b/backend/PrintCminor.ml index 8c255a65..c9a6d399 100644 --- a/backend/PrintCminor.ml +++ b/backend/PrintCminor.ml @@ -16,7 +16,7 @@ (** Pretty-printer for Cminor *) open Format -open !Camlcoq +open! Camlcoq open Integers open AST open PrintAST @@ -193,9 +193,7 @@ let print_sig p sg = List.iter (fun t -> fprintf p "%s ->@ " (name_of_type t)) sg.sig_args; - match sg.sig_res with - | None -> fprintf p "void" - | Some ty -> fprintf p "%s" (name_of_type ty) + fprintf p "%s" (name_of_rettype sg.sig_res) let rec just_skips s = match s with diff --git a/backend/RTLgen.v b/backend/RTLgen.v index a0ca0f17..2c27944a 100644 --- a/backend/RTLgen.v +++ b/backend/RTLgen.v @@ -410,12 +410,11 @@ Fixpoint convert_builtin_args {A: Type} (al: list (builtin_arg expr)) (rl: list a1' :: convert_builtin_args al rl1 end. -Definition convert_builtin_res (map: mapping) (oty: option typ) (r: builtin_res ident) : mon (builtin_res reg) := - match r, oty with - | BR id, _ => do r <- find_var map id; ret (BR r) - | BR_none, None => ret BR_none - | BR_none, Some _ => do r <- new_reg; ret (BR r) - | _, _ => error (Errors.msg "RTLgen: bad builtin_res") +Definition convert_builtin_res (map: mapping) (ty: rettype) (r: builtin_res ident) : mon (builtin_res reg) := + match r with + | BR id => do r <- find_var map id; ret (BR r) + | BR_none => if rettype_eq ty Tvoid then ret BR_none else (do r <- new_reg; ret (BR r)) + | _ => error (Errors.msg "RTLgen: bad builtin_res") end. (** Translation of an expression. [transl_expr map a rd nd] @@ -667,10 +666,7 @@ Fixpoint reserve_labels (s: stmt) (ms: labelmap * state) (** Translation of a CminorSel function. *) Definition ret_reg (sig: signature) (rd: reg) : option reg := - match sig.(sig_res) with - | None => None - | Some ty => Some rd - end. + if rettype_eq sig.(sig_res) Tvoid then None else Some rd. Definition transl_fun (f: CminorSel.function) (ngoto: labelmap): mon (node * list reg) := do (rparams, map1) <- add_vars init_mapping f.(CminorSel.fn_params); diff --git a/backend/RTLgenspec.v b/backend/RTLgenspec.v index aa83da6d..92b48e2b 100644 --- a/backend/RTLgenspec.v +++ b/backend/RTLgenspec.v @@ -639,8 +639,8 @@ Lemma new_reg_return_ok: map_valid map s1 -> return_reg_ok s2 map (ret_reg sig r). Proof. - intros. unfold ret_reg. destruct (sig_res sig); constructor. - eauto with rtlg. eauto with rtlg. + intros. unfold ret_reg. + destruct (rettype_eq (sig_res sig) Tvoid); constructor; eauto with rtlg. Qed. (** * Relational specification of the translation *) @@ -1224,9 +1224,9 @@ Lemma convert_builtin_res_charact: Proof. destruct res; simpl; intros. - monadInv TR. constructor. unfold find_var in EQ. destruct (map_vars map)!x; inv EQ; auto. -- destruct oty; monadInv TR. -+ constructor. eauto with rtlg. +- destruct (rettype_eq oty Tvoid); monadInv TR. + constructor. ++ constructor. eauto with rtlg. - monadInv TR. Qed. @@ -1350,7 +1350,7 @@ Proof. intros [C D]. eapply tr_function_intro; eauto with rtlg. eapply transl_stmt_charact; eauto with rtlg. - unfold ret_reg. destruct (sig_res (CminorSel.fn_sig f)). - constructor. eauto with rtlg. eauto with rtlg. + unfold ret_reg. destruct (rettype_eq (sig_res (CminorSel.fn_sig f)) Tvoid). constructor. + constructor; eauto with rtlg. Qed. diff --git a/backend/RTLtyping.v b/backend/RTLtyping.v index 74bfa582..857f2211 100644 --- a/backend/RTLtyping.v +++ b/backend/RTLtyping.v @@ -151,11 +151,12 @@ Inductive wt_instr : instruction -> Prop := list_length_z tbl * 4 <= Int.max_unsigned -> wt_instr (Ijumptable arg tbl) | wt_Ireturn_none: - funct.(fn_sig).(sig_res) = None -> + funct.(fn_sig).(sig_res) = Tvoid -> wt_instr (Ireturn None) | wt_Ireturn_some: forall arg ty, - funct.(fn_sig).(sig_res) = Some ty -> + funct.(fn_sig).(sig_res) <> Tvoid -> + env arg = proj_sig_res funct.(fn_sig) -> env arg = ty -> wt_instr (Ireturn (Some arg)). @@ -298,7 +299,7 @@ Definition type_instr (e: S.typenv) (i: instruction) : res S.typenv := | Itailcall sig ros args => do e1 <- type_ros e ros; do e2 <- S.set_list e1 args sig.(sig_args); - if opt_typ_eq sig.(sig_res) f.(fn_sig).(sig_res) then + if rettype_eq sig.(sig_res) f.(fn_sig).(sig_res) then if tailcall_is_possible sig then OK e2 else Error(msg "tailcall not possible") @@ -323,9 +324,9 @@ Definition type_instr (e: S.typenv) (i: instruction) : res S.typenv := then OK e1 else Error(msg "jumptable too big") | Ireturn optres => - match optres, f.(fn_sig).(sig_res) with - | None, None => OK e - | Some r, Some t => S.set e r t + match optres, rettype_eq f.(fn_sig).(sig_res) Tvoid with + | None, left _ => OK e + | Some r, right _ => S.set e r (proj_sig_res f.(fn_sig)) | _, _ => Error(msg "bad return") end end. @@ -468,7 +469,7 @@ Proof. destruct l; try discriminate. destruct l; monadInv EQ0. eauto with ty. destruct (type_of_operation o) as [targs tres] eqn:TYOP. monadInv EQ0. eauto with ty. - (* tailcall *) - destruct (opt_typ_eq (sig_res s) (sig_res (fn_sig f))); try discriminate. + destruct (rettype_eq (sig_res s) (sig_res (fn_sig f))); try discriminate. destruct (tailcall_is_possible s) eqn:TCIP; inv EQ2. eauto with ty. - (* builtin *) @@ -477,7 +478,8 @@ Proof. destruct (zle (list_length_z l * 4) Int.max_unsigned); inv EQ2. eauto with ty. - (* return *) - simpl in H. destruct o as [r|] eqn: RET; destruct (sig_res (fn_sig f)) as [t|] eqn: RES; try discriminate. + simpl in H. + destruct o as [r|] eqn: RET; destruct (rettype_eq (sig_res (fn_sig f)) Tvoid); try discriminate. eauto with ty. inv H; auto with ty. Qed. @@ -519,7 +521,7 @@ Proof. eapply S.set_sound; eauto with ty. eauto with ty. - (* tailcall *) - destruct (opt_typ_eq (sig_res s) (sig_res (fn_sig f))); try discriminate. + destruct (rettype_eq (sig_res s) (sig_res (fn_sig f))); try discriminate. destruct (tailcall_is_possible s) eqn:TCIP; inv EQ2. constructor. eapply type_ros_sound; eauto with ty. @@ -543,8 +545,9 @@ Proof. eapply check_successors_sound; eauto. auto. - (* return *) - simpl in H. destruct o as [r|] eqn: RET; destruct (sig_res (fn_sig f)) as [t|] eqn: RES; try discriminate. - econstructor. eauto. eapply S.set_sound; eauto with ty. + simpl in H. + destruct o as [r|] eqn: RET; destruct (rettype_eq (sig_res (fn_sig f)) Tvoid); try discriminate. + econstructor. auto. eapply S.set_sound; eauto with ty. eauto. inv H. constructor. auto. Qed. @@ -721,9 +724,9 @@ Proof. rewrite check_successor_complete by auto; simpl. apply IHtbl0; intros; auto. - (* return none *) - rewrite H0. exists e; auto. + rewrite H0, dec_eq_true. exists e; auto. - (* return some *) - rewrite H0. apply S.set_complete; auto. + rewrite dec_eq_false by auto. apply S.set_complete; auto. Qed. Lemma type_code_complete: @@ -882,7 +885,7 @@ Qed. Inductive wt_stackframes: list stackframe -> signature -> Prop := | wt_stackframes_nil: forall sg, - sg.(sig_res) = Some Tint -> + sg.(sig_res) = Tint -> wt_stackframes nil sg | wt_stackframes_cons: forall s res f sp pc rs env sg, @@ -978,13 +981,13 @@ Proof. econstructor; eauto. (* Ireturn *) econstructor; eauto. - inv WTI; simpl. auto. unfold proj_sig_res; rewrite H2. auto. + inv WTI; simpl. auto. rewrite <- H3. auto. (* internal function *) simpl in *. inv H5. econstructor; eauto. inv H1. apply wt_init_regs; auto. rewrite wt_params0. auto. (* external function *) - econstructor; eauto. simpl. + econstructor; eauto. eapply external_call_well_typed; eauto. (* return *) inv H1. econstructor; eauto. diff --git a/backend/Tailcall.v b/backend/Tailcall.v index 939abeea..b7a62d74 100644 --- a/backend/Tailcall.v +++ b/backend/Tailcall.v @@ -82,7 +82,7 @@ Definition transf_instr (f: function) (pc: node) (instr: instruction) := | Icall sig ros args res s => if is_return niter f s res && tailcall_is_possible sig - && opt_typ_eq sig.(sig_res) f.(fn_sig).(sig_res) + && rettype_eq sig.(sig_res) f.(fn_sig).(sig_res) then Itailcall sig ros args else instr | _ => instr diff --git a/backend/Tailcallproof.v b/backend/Tailcallproof.v index 5cb1b980..79a5c1cf 100644 --- a/backend/Tailcallproof.v +++ b/backend/Tailcallproof.v @@ -157,12 +157,10 @@ Lemma transf_instr_charact: transf_instr_spec f instr (transf_instr f pc instr). Proof. intros. unfold transf_instr. destruct instr; try constructor. - caseEq (is_return niter f n r && tailcall_is_possible s && - opt_typ_eq (sig_res s) (sig_res (fn_sig f))); intros. - destruct (andb_prop _ _ H0). destruct (andb_prop _ _ H1). - eapply transf_instr_tailcall; eauto. - eapply is_return_charact; eauto. - constructor. + destruct (is_return niter f n r && tailcall_is_possible s && + rettype_eq (sig_res s) (sig_res (fn_sig f))) eqn:B. +- InvBooleans. eapply transf_instr_tailcall; eauto. eapply is_return_charact; eauto. +- constructor. Qed. Lemma transf_instr_lookup: diff --git a/cfrontend/C2C.ml b/cfrontend/C2C.ml index 24e3cacf..ec5fb4dc 100644 --- a/cfrontend/C2C.ml +++ b/cfrontend/C2C.ml @@ -33,6 +33,7 @@ type inline_status = type atom_info = { a_storage: C.storage; (* storage class *) + a_size: int64 option; (* size in bytes *) a_alignment: int option; (* alignment *) a_sections: Sections.section_name list; (* in which section to put it *) (* 1 section for data, 3 sections (code/lit/jumptbl) for functions *) @@ -72,9 +73,14 @@ let atom_sections a = with Not_found -> [] -let atom_is_small_data a ofs = +let atom_is_small_data a ofs = try - (Hashtbl.find decl_atom a).a_access = Sections.Access_near + let info = Hashtbl.find decl_atom a in + info.a_access = Sections.Access_near + && (match info.a_size with + | None -> false + | Some sz -> + let ofs = camlint64_of_ptrofs ofs in 0L <= ofs && ofs < sz) with Not_found -> false @@ -376,6 +382,7 @@ let name_for_string_literal s = Hashtbl.add decl_atom id { a_storage = C.Storage_static; a_alignment = Some 1; + a_size = Some (Int64.of_int (String.length s + 1)); a_sections = [Sections.for_stringlit()]; a_access = Sections.Access_default; a_inline = No_specifier; @@ -403,9 +410,12 @@ let name_for_wide_string_literal s = incr stringNum; let name = Printf.sprintf "__stringlit_%d" !stringNum in let id = intern_string name in + let wchar_size = Machine.((!config).sizeof_wchar) in Hashtbl.add decl_atom id { a_storage = C.Storage_static; - a_alignment = Some Machine.((!config).sizeof_wchar); + a_alignment = Some wchar_size; + a_size = Some (Int64.(mul (of_int (List.length s + 1)) + (of_int wchar_size))); a_sections = [Sections.for_stringlit()]; a_access = Sections.Access_default; a_inline = No_specifier; @@ -1247,6 +1257,7 @@ let convertFundef loc env fd = Hashtbl.add decl_atom id' { a_storage = fd.fd_storage; a_alignment = None; + a_size = None; a_sections = Sections.for_function env id' fd.fd_attrib; a_access = Sections.Access_default; a_inline = inline; @@ -1341,6 +1352,7 @@ let convertGlobvar loc env (sto, id, ty, optinit) = Hashtbl.add decl_atom id' { a_storage = sto; a_alignment = Some (Z.to_int al); + a_size = Some (Z.to_int64 sz); a_sections = [section]; a_access = access; a_inline = No_specifier; diff --git a/cfrontend/Cop.v b/cfrontend/Cop.v index aa73abb0..143e87a3 100644 --- a/cfrontend/Cop.v +++ b/cfrontend/Cop.v @@ -140,8 +140,8 @@ Definition classify_cast (tfrom tto: type) : classify_cast_cases := | Tfloat F64 _, Tfloat F32 _ => cast_case_s2f | Tfloat F32 _, Tfloat F64 _ => cast_case_f2s (* To pointer types *) - | Tpointer _ _, Tint _ _ _ => - if Archi.ptr64 then cast_case_i2l Unsigned else cast_case_pointer + | Tpointer _ _, Tint _ si _ => + if Archi.ptr64 then cast_case_i2l si else cast_case_pointer | Tpointer _ _, Tlong _ _ => if Archi.ptr64 then cast_case_pointer else cast_case_l2i I32 Unsigned | Tpointer _ _, (Tpointer _ _ | Tarray _ _ _ | Tfunction _ _ _) => cast_case_pointer diff --git a/cfrontend/Csem.v b/cfrontend/Csem.v index a76a14ba..6d2b470f 100644 --- a/cfrontend/Csem.v +++ b/cfrontend/Csem.v @@ -444,7 +444,7 @@ Lemma red_selection: Proof. intros. unfold Eselection. set (t := typ_of_type ty). - set (sg := mksignature (AST.Tint :: t :: t :: nil) (Some t) cc_default). + set (sg := mksignature (AST.Tint :: t :: t :: nil) t cc_default). assert (LK: lookup_builtin_function "__builtin_sel"%string sg = Some (BI_standard (BI_select t))). { unfold sg, t; destruct ty as [ | ? ? ? | ? | [] ? | ? ? | ? ? ? | ? ? ? | ? ? | ? ? ]; simpl; unfold Tptr; destruct Archi.ptr64; reflexivity. } diff --git a/cfrontend/Cshmgen.v b/cfrontend/Cshmgen.v index 792a73f9..5bd12d00 100644 --- a/cfrontend/Cshmgen.v +++ b/cfrontend/Cshmgen.v @@ -23,6 +23,7 @@ Require Import Coqlib Maps Errors Integers Floats. Require Import AST Linking. Require Import Ctypes Cop Clight Cminor Csharpminor. +Require Import Conventions1. Local Open Scope string_scope. Local Open Scope error_monad_scope. @@ -558,6 +559,34 @@ Fixpoint typlist_of_arglist (al: list Clight.expr) (tyl: typelist) typ_of_type (default_argument_conversion (typeof a1)) :: typlist_of_arglist a2 Tnil end. +(** Translate a function call. + Depending on the ABI, it may be necessary to normalize the value + returned by casting it to the return type of the function. + For example, in the x86 ABI, a return value of type "char" is + returned in register AL, leaving the top 24 bits of EAX + unspecified. Hence, a cast to type "char" is needed to sign- or + zero-extend the returned integer before using it. *) + +Definition make_normalization (t: type) (a: expr) := + match t with + | Tint IBool _ _ => Eunop Ocast8unsigned a + | Tint I8 Signed _ => Eunop Ocast8signed a + | Tint I8 Unsigned _ => Eunop Ocast8unsigned a + | Tint I16 Signed _ => Eunop Ocast16signed a + | Tint I16 Unsigned _ => Eunop Ocast16unsigned a + | _ => a + end. + +Definition make_funcall (x: option ident) (tres: type) (sg: signature) + (fn: expr) (args: list expr): stmt := + match x, return_value_needs_normalization sg.(sig_res) with + | Some id, true => + Sseq (Scall x sg fn args) + (Sset id (make_normalization tres (Evar id))) + | _, _ => + Scall x sg fn args + end. + (** * Translation of statements *) (** [transl_statement nbrk ncnt s] returns a Csharpminor statement @@ -601,10 +630,10 @@ Fixpoint transl_statement (ce: composite_env) (tyret: type) (nbrk ncnt: nat) | fun_case_f args res cconv => do tb <- transl_expr ce b; do tcl <- transl_arglist ce cl args; - OK(Scall x {| sig_args := typlist_of_arglist cl args; - sig_res := opttyp_of_type res; - sig_cc := cconv |} - tb tcl) + let sg := {| sig_args := typlist_of_arglist cl args; + sig_res := rettype_of_type res; + sig_cc := cconv |} in + OK (make_funcall x res sg tb tcl) | _ => Error(msg "Cshmgen.transl_stmt(call)") end | Clight.Sbuiltin x ef tyargs bl => @@ -667,7 +696,7 @@ Definition transl_var (ce: composite_env) (v: ident * type) := Definition signature_of_function (f: Clight.function) := {| sig_args := map typ_of_type (map snd (Clight.fn_params f)); - sig_res := opttyp_of_type (Clight.fn_return f); + sig_res := rettype_of_type (Clight.fn_return f); sig_cc := Clight.fn_callconv f |}. Definition transl_function (ce: composite_env) (f: Clight.function) : res function := diff --git a/cfrontend/Cshmgenproof.v b/cfrontend/Cshmgenproof.v index 09e31cb2..1ceb8e4d 100644 --- a/cfrontend/Cshmgenproof.v +++ b/cfrontend/Cshmgenproof.v @@ -15,7 +15,7 @@ Require Import Coqlib Errors Maps Integers Floats. Require Import AST Linking. Require Import Values Events Memory Globalenvs Smallstep. -Require Import Ctypes Cop Clight Cminor Csharpminor. +Require Import Ctypes Ctyping Cop Clight Cminor Csharpminor. Require Import Cshmgen. (** * Relational specification of the transformation *) @@ -996,6 +996,26 @@ Proof. eapply make_memcpy_correct with (b := b) (v := Vptr b' ofs'); eauto. Qed. +Lemma make_normalization_correct: + forall e le m a v t, + eval_expr ge e le m a v -> + wt_val v t -> + eval_expr ge e le m (make_normalization t a) v. +Proof. + intros. destruct t; simpl; auto. inv H0. +- destruct i; simpl in H3. + + destruct s; econstructor; eauto; simpl; congruence. + + destruct s; econstructor; eauto; simpl; congruence. + + auto. + + econstructor; eauto; simpl; congruence. +- auto. +- destruct i. + + destruct s; econstructor; eauto. + + destruct s; econstructor; eauto. + + auto. + + econstructor; eauto. +Qed. + End CONSTRUCTORS. (** * Basic preservation invariants *) @@ -1360,7 +1380,16 @@ Inductive match_cont: composite_env -> type -> nat -> nat -> Clight.cont -> Csha match_cont cu.(prog_comp_env) (Clight.fn_return f) nbrk' ncnt' k tk -> match_cont ce tyret nbrk ncnt (Clight.Kcall id f e le k) - (Kcall id tf te le tk). + (Kcall id tf te le tk) + | match_Kcall_normalize: forall ce tyret nbrk ncnt nbrk' ncnt' f e k id a tf te le tk cu, + linkorder cu prog -> + transl_function cu.(prog_comp_env) f = OK tf -> + match_env e te -> + match_cont cu.(prog_comp_env) (Clight.fn_return f) nbrk' ncnt' k tk -> + (forall v e le m, wt_val v tyret -> le!id = Some v -> eval_expr tge e le m a v) -> + match_cont ce tyret nbrk ncnt + (Clight.Kcall (Some id) f e le k) + (Kcall (Some id) tf te le (Kseq (Sset id a) tk)). Inductive match_states: Clight.state -> Csharpminor.state -> Prop := | match_state: @@ -1377,14 +1406,15 @@ Inductive match_states: Clight.state -> Csharpminor.state -> Prop := forall fd args k m tfd tk targs tres cconv cu ce (LINK: linkorder cu prog) (TR: match_fundef cu fd tfd) - (MK: match_cont ce Tvoid 0%nat 0%nat k tk) + (MK: match_cont ce tres 0%nat 0%nat k tk) (ISCC: Clight.is_call_cont k) (TY: type_of_fundef fd = Tfunction targs tres cconv), match_states (Clight.Callstate fd args k m) (Callstate tfd args tk m) | match_returnstate: - forall res k m tk ce - (MK: match_cont ce Tvoid 0%nat 0%nat k tk), + forall res tres k m tk ce + (MK: match_cont ce tres 0%nat 0%nat k tk) + (WT: wt_val res tres), match_states (Clight.Returnstate res k m) (Returnstate res tk m). @@ -1442,7 +1472,9 @@ Proof. - (* set *) auto. - (* call *) - simpl in TR. destruct (classify_fun (typeof e)); monadInv TR. auto. + simpl in TR. destruct (classify_fun (typeof e)); monadInv TR. + unfold make_funcall. + destruct o; auto; destruct Conventions1.return_value_needs_normalization; auto. - (* builtin *) auto. - (* seq *) @@ -1500,24 +1532,26 @@ End FIND_LABEL. (** Properties of call continuations *) Lemma match_cont_call_cont: - forall ce' tyret' nbrk' ncnt' ce tyret nbrk ncnt k tk, + forall ce' nbrk' ncnt' ce tyret nbrk ncnt k tk, match_cont ce tyret nbrk ncnt k tk -> - match_cont ce' tyret' nbrk' ncnt' (Clight.call_cont k) (call_cont tk). + match_cont ce' tyret nbrk' ncnt' (Clight.call_cont k) (call_cont tk). Proof. induction 1; simpl; auto. - constructor. - econstructor; eauto. +- apply match_Kstop. +- eapply match_Kcall; eauto. +- eapply match_Kcall_normalize; eauto. Qed. Lemma match_cont_is_call_cont: - forall ce tyret nbrk ncnt k tk ce' tyret' nbrk' ncnt', + forall ce tyret nbrk ncnt k tk ce' nbrk' ncnt', match_cont ce tyret nbrk ncnt k tk -> Clight.is_call_cont k -> - match_cont ce' tyret' nbrk' ncnt' k tk /\ is_call_cont tk. + match_cont ce' tyret nbrk' ncnt' k tk /\ is_call_cont tk. Proof. intros. inv H; simpl in H0; try contradiction; simpl. - split; auto; constructor. - split; auto; econstructor; eauto. + split; auto; apply match_Kstop. + split; auto; eapply match_Kcall; eauto. + split; auto; eapply match_Kcall_normalize; eauto. Qed. (** The simulation proof *) @@ -1549,19 +1583,44 @@ Proof. - (* call *) revert TR. simpl. case_eq (classify_fun (typeof a)); try congruence. - intros targs tres cc CF TR. monadInv TR. inv MTR. + intros targs tres cc CF TR. monadInv TR. exploit functions_translated; eauto. intros (cu' & tfd & FIND & TFD & LINK'). rewrite H in CF. simpl in CF. inv CF. - econstructor; split. - apply plus_one. econstructor; eauto. - eapply transl_expr_correct with (cunit := cu); eauto. - eapply transl_arglist_correct with (cunit := cu); eauto. - erewrite typlist_of_arglist_eq by eauto. - eapply transl_fundef_sig1; eauto. - rewrite H3. auto. - econstructor; eauto. - eapply match_Kcall with (ce := prog_comp_env cu') (cu := cu); eauto. - simpl. auto. + set (sg := {| sig_args := typlist_of_arglist al targs; + sig_res := rettype_of_type tres; + sig_cc := cc |}) in *. + assert (SIG: funsig tfd = sg). + { unfold sg; erewrite typlist_of_arglist_eq by eauto. + eapply transl_fundef_sig1; eauto. rewrite H3; auto. } + assert (EITHER: tk' = tk /\ ts' = Scall optid sg x x0 + \/ exists id, optid = Some id /\ + tk' = tk /\ ts' = Sseq (Scall optid sg x x0) + (Sset id (make_normalization tres (Evar id)))). + { unfold make_funcall in MTR. + destruct optid. destruct Conventions1.return_value_needs_normalization. + inv MTR. right; exists i; auto. + inv MTR; auto. + inv MTR; auto. } + destruct EITHER as [(EK & ES) | (id & EI & EK & ES)]; rewrite EK, ES. + + (* without normalization of return value *) + econstructor; split. + apply plus_one. eapply step_call; eauto. + eapply transl_expr_correct with (cunit := cu); eauto. + eapply transl_arglist_correct with (cunit := cu); eauto. + econstructor; eauto. + eapply match_Kcall with (ce := prog_comp_env cu') (cu := cu); eauto. + exact I. + + (* with normalization of return value *) + subst optid. + econstructor; split. + eapply plus_two. apply step_seq. eapply step_call; eauto. + eapply transl_expr_correct with (cunit := cu); eauto. + eapply transl_arglist_correct with (cunit := cu); eauto. + traceEq. + econstructor; eauto. + eapply match_Kcall_normalize with (ce := prog_comp_env cu') (cu := cu); eauto. + intros. eapply make_normalization_correct; eauto. constructor; eauto. + exact I. - (* builtin *) monadInv TR. inv MTR. @@ -1658,6 +1717,7 @@ Proof. eapply match_env_free_blocks; eauto. eapply match_returnstate with (ce := prog_comp_env cu); eauto. eapply match_cont_call_cont. eauto. + constructor. - (* return some *) monadInv TR. inv MTR. @@ -1667,6 +1727,7 @@ Proof. eapply match_env_free_blocks; eauto. eapply match_returnstate with (ce := prog_comp_env cu); eauto. eapply match_cont_call_cont. eauto. + apply wt_val_casted. eapply cast_val_is_casted; eauto. - (* skip call *) monadInv TR. inv MTR. @@ -1675,6 +1736,7 @@ Proof. apply plus_one. apply step_skip_call. auto. eapply match_env_free_blocks; eauto. eapply match_returnstate with (ce := prog_comp_env cu); eauto. + constructor. - (* switch *) monadInv TR. @@ -1738,20 +1800,33 @@ Proof. simpl. econstructor; eauto. unfold transl_function. rewrite EQ; simpl. rewrite EQ1; simpl. auto. constructor. + replace (fn_return f) with tres. eassumption. + simpl in TY. unfold type_of_function in TY. congruence. - (* external function *) inv TR. exploit match_cont_is_call_cont; eauto. intros [A B]. econstructor; split. - apply plus_one. constructor. eauto. + apply plus_one. constructor. eapply external_call_symbols_preserved; eauto. apply senv_preserved. eapply match_returnstate with (ce := ce); eauto. + apply has_rettype_wt_val. + replace (rettype_of_type tres0) with (sig_res (ef_sig ef)). + eapply external_call_well_typed_gen; eauto. + rewrite H5. simpl. simpl in TY. congruence. - (* returnstate *) inv MK. - econstructor; split. - apply plus_one. constructor. - econstructor; eauto. simpl; reflexivity. constructor. + + (* without normalization *) + econstructor; split. + apply plus_one. constructor. + econstructor; eauto. simpl; reflexivity. constructor. + + (* with normalization *) + econstructor; split. + eapply plus_three. econstructor. econstructor. constructor. + simpl. apply H13. eauto. apply PTree.gss. + traceEq. + simpl. rewrite PTree.set2. econstructor; eauto. simpl; reflexivity. constructor. Qed. Lemma transl_initial_states: diff --git a/cfrontend/Csyntax.v b/cfrontend/Csyntax.v index c34a5e13..e3e2c1e9 100644 --- a/cfrontend/Csyntax.v +++ b/cfrontend/Csyntax.v @@ -106,7 +106,7 @@ Definition Epreincr (id: incr_or_decr) (l: expr) (ty: type) := Definition Eselection (r1 r2 r3: expr) (ty: type) := let t := typ_of_type ty in - let sg := mksignature (AST.Tint :: t :: t :: nil) (Some t) cc_default in + let sg := mksignature (AST.Tint :: t :: t :: nil) t cc_default in Ebuiltin (EF_builtin "__builtin_sel"%string sg) (Tcons type_bool (Tcons ty (Tcons ty Tnil))) (Econs r1 (Econs r2 (Econs r3 Enil))) diff --git a/cfrontend/Ctypes.v b/cfrontend/Ctypes.v index bfc5daa9..664a60c5 100644 --- a/cfrontend/Ctypes.v +++ b/cfrontend/Ctypes.v @@ -732,8 +732,21 @@ Definition typ_of_type (t: type) : AST.typ := | Tpointer _ _ | Tarray _ _ _ | Tfunction _ _ _ | Tstruct _ _ | Tunion _ _ => AST.Tptr end. -Definition opttyp_of_type (t: type) : option AST.typ := - if type_eq t Tvoid then None else Some (typ_of_type t). +Definition rettype_of_type (t: type) : AST.rettype := + match t with + | Tvoid => AST.Tvoid + | Tint I32 _ _ => AST.Tint + | Tint I8 Signed _ => AST.Tint8signed + | Tint I8 Unsigned _ => AST.Tint8unsigned + | Tint I16 Signed _ => AST.Tint16signed + | Tint I16 Unsigned _ => AST.Tint16unsigned + | Tint IBool _ _ => AST.Tint8unsigned + | Tlong _ _ => AST.Tlong + | Tfloat F32 _ => AST.Tsingle + | Tfloat F64 _ => AST.Tfloat + | Tpointer _ _ => AST.Tptr + | Tarray _ _ _ | Tfunction _ _ _ | Tstruct _ _ | Tunion _ _ => AST.Tvoid + end. Fixpoint typlist_of_typelist (tl: typelist) : list AST.typ := match tl with @@ -742,7 +755,7 @@ Fixpoint typlist_of_typelist (tl: typelist) : list AST.typ := end. Definition signature_of_type (args: typelist) (res: type) (cc: calling_convention): signature := - mksignature (typlist_of_typelist args) (opttyp_of_type res) cc. + mksignature (typlist_of_typelist args) (rettype_of_type res) cc. (** * Construction of the composite environment *) diff --git a/cfrontend/Ctyping.v b/cfrontend/Ctyping.v index b92a9bac..00fcf8ab 100644 --- a/cfrontend/Ctyping.v +++ b/cfrontend/Ctyping.v @@ -397,10 +397,10 @@ Inductive wt_rvalue : expr -> Prop := wt_arguments rargs tyargs -> (* This typing rule is specialized to the builtin invocations generated by C2C, which are either __builtin_sel or builtins returning void. *) - (ty = Tvoid /\ sig_res (ef_sig ef) = None) + (ty = Tvoid /\ sig_res (ef_sig ef) = AST.Tvoid) \/ (tyargs = Tcons type_bool (Tcons ty (Tcons ty Tnil)) /\ let t := typ_of_type ty in - let sg := mksignature (AST.Tint :: t :: t :: nil) (Some t) cc_default in + let sg := mksignature (AST.Tint :: t :: t :: nil) t cc_default in ef = EF_builtin "__builtin_sel"%string sg) -> wt_rvalue (Ebuiltin ef tyargs rargs ty) | wt_Eparen: forall r tycast ty, @@ -521,11 +521,20 @@ Fixpoint bind_globdef (e: typenv) (l: list (ident * globdef fundef type)) : type | (id, Gvar v) :: l => bind_globdef (PTree.set id v.(gvar_info) e) l end. +Inductive wt_fundef (ce: composite_env) (e: typenv) : fundef -> Prop := + | wt_fundef_internal: forall f, + wt_function ce e f -> + wt_fundef ce e (Internal f) + | wt_fundef_external: forall ef targs tres cc, + (ef_sig ef).(sig_res) = rettype_of_type tres -> + wt_fundef ce e (External ef targs tres cc). + Inductive wt_program : program -> Prop := | wt_program_intro: forall p, let e := bind_globdef (PTree.empty _) p.(prog_defs) in - (forall id f, In (id, Gfun (Internal f)) p.(prog_defs) -> - wt_function p.(prog_comp_env) e f) -> + (forall id fd, + In (id, Gfun fd) p.(prog_defs) -> + wt_fundef p.(prog_comp_env) e fd) -> wt_program p. Hint Constructors wt_val wt_rvalue wt_lvalue wt_stmt wt_lblstmts: ty. @@ -745,7 +754,7 @@ Definition ebuiltin (ef: external_function) (tyargs: typelist) (args: exprlist) do x1 <- check_rvals args; do x2 <- check_arguments args tyargs; if type_eq tyres Tvoid - && opt_typ_eq (sig_res (ef_sig ef)) None + && AST.rettype_eq (sig_res (ef_sig ef)) AST.Tvoid then OK (Ebuiltin ef tyargs args tyres) else Error (msg "builtin: wrong type decoration"). @@ -915,7 +924,8 @@ Definition retype_function (ce: composite_env) (e: typenv) (f: function) : res f Definition retype_fundef (ce: composite_env) (e: typenv) (fd: fundef) : res fundef := match fd with | Internal f => do f' <- retype_function ce e f; OK (Internal f') - | External id args res cc => OK fd + | External ef args res cc => + assertion (rettype_eq (ef_sig ef).(sig_res) (rettype_of_type res)); OK fd end. Definition typecheck_program (p: program) : res program := @@ -987,6 +997,7 @@ Proof. classify_cast (Tint i s a) t2 <> cast_case_default). { unfold classify_cast. destruct t2; try congruence. destruct f; congruence. + destruct Archi.ptr64; congruence. } destruct i; auto. Qed. @@ -1240,7 +1251,7 @@ Lemma ebuiltin_sound: Proof. intros. monadInv H. destruct (type_eq tyres Tvoid); simpl in EQ2; try discriminate. - destruct (opt_typ_eq (sig_res (ef_sig ef)) None); inv EQ2. + destruct (rettype_eq (sig_res (ef_sig ef)) AST.Tvoid); inv EQ2. econstructor; eauto. eapply check_arguments_sound; eauto. Qed. @@ -1372,6 +1383,14 @@ Proof. intros. monadInv H. constructor; simpl. eapply retype_stmt_sound; eauto. Qed. +Lemma retype_fundef_sound: + forall ce e fd fd', retype_fundef ce e fd = OK fd' -> wt_fundef ce e fd'. +Proof. + intros. destruct fd; monadInv H. +- constructor; eapply retype_function_sound; eauto. +- constructor; auto. +Qed. + Theorem typecheck_program_sound: forall p p', typecheck_program p = OK p' -> wt_program p'. Proof. @@ -1394,11 +1413,11 @@ Proof. inv H1. simpl. auto. } rewrite ENVS. - intros id f. revert MATCH; generalize (prog_defs p) (AST.prog_defs tp). + intros id fd. revert MATCH; generalize (prog_defs p) (AST.prog_defs tp). induction 1; simpl; intros. contradiction. destruct H0; auto. subst b1; inv H. simpl in H1. inv H1. - destruct f1; monadInv H4. eapply retype_function_sound; eauto. + eapply retype_fundef_sound; eauto. Qed. (** * Subject reduction *) @@ -1710,6 +1729,26 @@ Proof. inv H; auto. Qed. +Lemma has_rettype_wt_val: + forall v ty, + Val.has_rettype v (rettype_of_type ty) -> wt_val v ty. +Proof. + unfold rettype_of_type, Val.has_rettype, Val.has_type; destruct ty; intros. +- destruct v; contradiction || constructor. +- destruct i. + + destruct s; destruct v; try contradiction; constructor; red; auto. + + destruct s; destruct v; try contradiction; constructor; red; auto. + + destruct v; try contradiction; constructor; auto. + + destruct v; try contradiction; constructor; red; auto. +- destruct v; try contradiction; constructor; auto. +- destruct f; destruct v; try contradiction; constructor. +- unfold Tptr in *; destruct v; destruct Archi.ptr64 eqn:P64; try contradiction; constructor; auto. +- destruct v; contradiction || constructor. +- destruct v; contradiction || constructor. +- destruct v; contradiction || constructor. +- destruct v; contradiction || constructor. +Qed. + Lemma wt_rred: forall ge tenv a m t a' m', rred ge a m t a' m' -> wt_rvalue ge tenv a -> wt_rvalue ge tenv a'. @@ -1749,7 +1788,7 @@ Proof. - (* builtin *) subst. destruct H7 as [(A & B) | (A & B)]. + subst ty. auto with ty. + simpl in B. set (T := typ_of_type ty) in *. - set (sg := mksignature (AST.Tint :: T :: T :: nil) (Some T) cc_default) in *. + set (sg := mksignature (AST.Tint :: T :: T :: nil) T cc_default) in *. assert (LK: lookup_builtin_function "__builtin_sel"%string sg = Some (BI_standard (BI_select T))). { unfold sg, T; destruct ty as [ | ? ? ? | ? | [] ? | ? ? | ? ? ? | ? ? ? | ? ? | ? ? ]; simpl; unfold Tptr; destruct Archi.ptr64; reflexivity. } @@ -1895,12 +1934,6 @@ Hypothesis WTPROG: wt_program prog. Let ge := globalenv prog. Let gtenv := bind_globdef (PTree.empty _) prog.(prog_defs). -Hypothesis WT_EXTERNAL: - forall id ef args res cc vargs m t vres m', - In (id, Gfun (External ef args res cc)) prog.(prog_defs) -> - external_call ef ge vargs m t vres m' -> - wt_val vres res. - Inductive wt_expr_cont: typenv -> function -> cont -> Prop := | wt_Kdo: forall te f k, wt_stmt_cont te f k -> @@ -1999,12 +2032,6 @@ Proof. induction 1; simpl; auto; econstructor; eauto. Qed. -Definition wt_fundef (fd: fundef) := - match fd with - | Internal f => wt_function ge gtenv f - | External ef targs tres cc => True - end. - Definition fundef_return (fd: fundef) : type := match fd with | Internal f => f.(fn_return) @@ -2012,10 +2039,10 @@ Definition fundef_return (fd: fundef) : type := end. Lemma wt_find_funct: - forall v fd, Genv.find_funct ge v = Some fd -> wt_fundef fd. + forall v fd, Genv.find_funct ge v = Some fd -> wt_fundef ge gtenv fd. Proof. intros. apply Genv.find_funct_prop with (p := prog) (v := v); auto. - intros. inv WTPROG. destruct f; simpl; auto. apply H1 with id; auto. + intros. inv WTPROG. apply H1 with id; auto. Qed. Inductive wt_state: state -> Prop := @@ -2031,7 +2058,7 @@ Inductive wt_state: state -> Prop := wt_state (ExprState f r k e m) | wt_call_state: forall b fd vargs k m (WTK: wt_call_cont k (fundef_return fd)) - (WTFD: wt_fundef fd) + (WTFD: wt_fundef ge gtenv fd) (FIND: Genv.find_funct ge b = Some fd), wt_state (Callstate fd vargs k m) | wt_return_state: forall v k m ty @@ -2088,7 +2115,6 @@ Qed. End WT_FIND_LABEL. - Lemma preservation_estep: forall S t S', estep ge S t S' -> wt_state S -> wt_state S'. Proof. @@ -2163,9 +2189,10 @@ Proof. - inv WTS; eauto with ty. - exploit wt_find_label. eexact WTB. eauto. eapply call_cont_wt'; eauto. intros [A B]. eauto with ty. -- simpl in WTFD; inv WTFD. econstructor; eauto. apply wt_call_cont_stmt_cont; auto. -- exploit (Genv.find_funct_inversion prog); eauto. intros (id & A). - econstructor; eauto. +- inv WTFD. inv H3. econstructor; eauto. apply wt_call_cont_stmt_cont; auto. +- inv WTFD. econstructor; eauto. + apply has_rettype_wt_val. simpl; rewrite <- H1. + eapply external_call_well_typed_gen; eauto. - inv WTK. eauto with ty. Qed. @@ -2180,7 +2207,7 @@ Theorem wt_initial_state: Proof. intros. inv H. econstructor. constructor. apply Genv.find_funct_ptr_prop with (p := prog) (b := b); auto. - intros. inv WTPROG. destruct f0; simpl; auto. apply H4 with id; auto. + intros. inv WTPROG. apply H4 with id; auto. instantiate (1 := (Vptr b Ptrofs.zero)). rewrite Genv.find_funct_find_funct_ptr. auto. Qed. diff --git a/cfrontend/PrintCsyntax.ml b/cfrontend/PrintCsyntax.ml index 1c9729c5..03dc5837 100644 --- a/cfrontend/PrintCsyntax.ml +++ b/cfrontend/PrintCsyntax.ml @@ -19,7 +19,7 @@ open Format open Camlcoq open Values open AST -open Ctypes +open! Ctypes open Cop open Csyntax @@ -85,7 +85,7 @@ let name_optid id = let rec name_cdecl id ty = match ty with - | Tvoid -> + | Ctypes.Tvoid -> "void" ^ name_optid id | Ctypes.Tint(sz, sg, a) -> name_inttype sz sg ^ attributes a ^ name_optid id diff --git a/common/AST.v b/common/AST.v index 86cab287..eb34d675 100644 --- a/common/AST.v +++ b/common/AST.v @@ -45,9 +45,6 @@ Lemma typ_eq: forall (t1 t2: typ), {t1=t2} + {t1<>t2}. Proof. decide equality. Defined. Global Opaque typ_eq. -Definition opt_typ_eq: forall (t1 t2: option typ), {t1=t2} + {t1<>t2} - := option_eq typ_eq. - Definition list_typ_eq: forall (l1 l2: list typ), {l1=l2} + {l1<>l2} := list_eq_dec typ_eq. @@ -91,10 +88,34 @@ Fixpoint subtype_list (tyl1 tyl2: list typ) : bool := | _, _ => false end. +(** To describe the values returned by functions, we use the more precise + types below. *) + +Inductive rettype : Type := + | Tret (t: typ) (**r like type [t] *) + | Tint8signed (**r 8-bit signed integer *) + | Tint8unsigned (**r 8-bit unsigned integer *) + | Tint16signed (**r 16-bit signed integer *) + | Tint16unsigned (**r 16-bit unsigned integer *) + | Tvoid. (**r no value returned *) + +Coercion Tret: typ >-> rettype. + +Lemma rettype_eq: forall (t1 t2: rettype), {t1=t2} + {t1<>t2}. +Proof. generalize typ_eq; decide equality. Defined. +Global Opaque rettype_eq. + +Fixpoint proj_rettype (r: rettype) : typ := + match r with + | Tret t => t + | Tint8signed | Tint8unsigned | Tint16signed | Tint16unsigned => Tint + | Tvoid => Tint + end. + (** Additionally, function definitions and function calls are annotated by function signatures indicating: - the number and types of arguments; -- the type of the returned value, if any; +- the type of the returned value; - additional information on which calling convention to use. These signatures are used in particular to determine appropriate @@ -117,24 +138,20 @@ Global Opaque calling_convention_eq. Record signature : Type := mksignature { sig_args: list typ; - sig_res: option typ; + sig_res: rettype; sig_cc: calling_convention }. -Definition proj_sig_res (s: signature) : typ := - match s.(sig_res) with - | None => Tint - | Some t => t - end. +Definition proj_sig_res (s: signature) : typ := proj_rettype s.(sig_res). Definition signature_eq: forall (s1 s2: signature), {s1=s2} + {s1<>s2}. Proof. - generalize opt_typ_eq, list_typ_eq, calling_convention_eq; decide equality. + generalize rettype_eq, list_typ_eq, calling_convention_eq; decide equality. Defined. Global Opaque signature_eq. Definition signature_main := - {| sig_args := nil; sig_res := Some Tint; sig_cc := cc_default |}. + {| sig_args := nil; sig_res := Tint; sig_cc := cc_default |}. (** Memory accesses (load and store instructions) are annotated by a ``memory chunk'' indicating the type, size and signedness of the @@ -177,6 +194,28 @@ Definition type_of_chunk (c: memory_chunk) : typ := Lemma type_of_Mptr: type_of_chunk Mptr = Tptr. Proof. unfold Mptr, Tptr; destruct Archi.ptr64; auto. Qed. +(** Same, as a return type. *) + +Definition rettype_of_chunk (c: memory_chunk) : rettype := + match c with + | Mint8signed => Tint8signed + | Mint8unsigned => Tint8unsigned + | Mint16signed => Tint16signed + | Mint16unsigned => Tint16unsigned + | Mint32 => Tint + | Mint64 => Tlong + | Mfloat32 => Tsingle + | Mfloat64 => Tfloat + | Many32 => Tany32 + | Many64 => Tany64 + end. + +Lemma proj_rettype_of_chunk: + forall chunk, proj_rettype (rettype_of_chunk chunk) = type_of_chunk chunk. +Proof. + destruct chunk; auto. +Qed. + (** The chunk that is appropriate to store and reload a value of the given type, without losing information. *) @@ -487,15 +526,15 @@ Definition ef_sig (ef: external_function): signature := | EF_external name sg => sg | EF_builtin name sg => sg | EF_runtime name sg => sg - | EF_vload chunk => mksignature (Tptr :: nil) (Some (type_of_chunk chunk)) cc_default - | EF_vstore chunk => mksignature (Tptr :: type_of_chunk chunk :: nil) None cc_default - | EF_malloc => mksignature (Tptr :: nil) (Some Tptr) cc_default - | EF_free => mksignature (Tptr :: nil) None cc_default - | EF_memcpy sz al => mksignature (Tptr :: Tptr :: nil) None cc_default - | EF_annot kind text targs => mksignature targs None cc_default - | EF_annot_val kind text targ => mksignature (targ :: nil) (Some targ) cc_default + | EF_vload chunk => mksignature (Tptr :: nil) (rettype_of_chunk chunk) cc_default + | EF_vstore chunk => mksignature (Tptr :: type_of_chunk chunk :: nil) Tvoid cc_default + | EF_malloc => mksignature (Tptr :: nil) Tptr cc_default + | EF_free => mksignature (Tptr :: nil) Tvoid cc_default + | EF_memcpy sz al => mksignature (Tptr :: Tptr :: nil) Tvoid cc_default + | EF_annot kind text targs => mksignature targs Tvoid cc_default + | EF_annot_val kind text targ => mksignature (targ :: nil) targ cc_default | EF_inline_asm text sg clob => sg - | EF_debug kind text targs => mksignature targs None cc_default + | EF_debug kind text targs => mksignature targs Tvoid cc_default end. (** Whether an external function should be inlined by the compiler. *) diff --git a/common/Builtins.v b/common/Builtins.v index c9097e86..476b541e 100644 --- a/common/Builtins.v +++ b/common/Builtins.v @@ -29,7 +29,7 @@ Definition builtin_function_sig (b: builtin_function) : signature := | BI_platform b => platform_builtin_sig b end. -Definition builtin_function_sem (b: builtin_function) : builtin_sem (proj_sig_res (builtin_function_sig b)) := +Definition builtin_function_sem (b: builtin_function) : builtin_sem (sig_res (builtin_function_sig b)) := match b with | BI_standard b => standard_builtin_sem b | BI_platform b => platform_builtin_sem b diff --git a/common/Builtins0.v b/common/Builtins0.v index b78006dd..8da98314 100644 --- a/common/Builtins0.v +++ b/common/Builtins0.v @@ -26,8 +26,8 @@ Require Import AST Integers Floats Values Memdata. appropriate for the target. *) -Definition val_opt_has_type (ov: option val) (t: typ) : Prop := - match ov with Some v => Val.has_type v t | None => True end. +Definition val_opt_has_rettype (ov: option val) (t: rettype) : Prop := + match ov with Some v => Val.has_rettype v t | None => True end. Definition val_opt_inject (j: meminj) (ov ov': option val) : Prop := match ov, ov' with @@ -42,10 +42,10 @@ Definition val_opt_inject (j: meminj) (ov ov': option val) : Prop := and be compatible with value injections. *) -Record builtin_sem (tret: typ) : Type := mkbuiltin { +Record builtin_sem (tret: rettype) : Type := mkbuiltin { bs_sem :> list val -> option val; bs_well_typed: forall vl, - val_opt_has_type (bs_sem vl) tret; + val_opt_has_rettype (bs_sem vl) tret; bs_inject: forall j vl vl', Val.inject_list j vl vl' -> val_opt_inject j (bs_sem vl) (bs_sem vl') }. @@ -60,8 +60,8 @@ Record builtin_sem (tret: typ) : Type := mkbuiltin { Local Unset Program Cases. Program Definition mkbuiltin_v1t - (tret: typ) (f: val -> val) - (WT: forall v1, Val.has_type (f v1) tret) + (tret: rettype) (f: val -> val) + (WT: forall v1, Val.has_rettype (f v1) tret) (INJ: forall j v1 v1', Val.inject j v1 v1' -> Val.inject j (f v1) (f v1')) := mkbuiltin tret (fun vl => match vl with v1 :: nil => Some (f v1) | _ => None end) _ _. Next Obligation. @@ -72,8 +72,8 @@ Next Obligation. Qed. Program Definition mkbuiltin_v2t - (tret: typ) (f: val -> val -> val) - (WT: forall v1 v2, Val.has_type (f v1 v2) tret) + (tret: rettype) (f: val -> val -> val) + (WT: forall v1 v2, Val.has_rettype (f v1 v2) tret) (INJ: forall j v1 v1' v2 v2', Val.inject j v1 v1' -> Val.inject j v2 v2' -> Val.inject j (f v1 v2) (f v1' v2')) := @@ -86,8 +86,8 @@ Next Obligation. Qed. Program Definition mkbuiltin_v3t - (tret: typ) (f: val -> val -> val -> val) - (WT: forall v1 v2 v3, Val.has_type (f v1 v2 v3) tret) + (tret: rettype) (f: val -> val -> val -> val) + (WT: forall v1 v2 v3, Val.has_rettype (f v1 v2 v3) tret) (INJ: forall j v1 v1' v2 v2' v3 v3', Val.inject j v1 v1' -> Val.inject j v2 v2' -> Val.inject j v3 v3' -> Val.inject j (f v1 v2 v3) (f v1' v2' v3')) := @@ -100,8 +100,8 @@ Next Obligation. Qed. Program Definition mkbuiltin_v1p - (tret: typ) (f: val -> option val) - (WT: forall v1, val_opt_has_type (f v1) tret) + (tret: rettype) (f: val -> option val) + (WT: forall v1, val_opt_has_rettype (f v1) tret) (INJ: forall j v1 v1', Val.inject j v1 v1' -> val_opt_inject j (f v1) (f v1')) := mkbuiltin tret (fun vl => match vl with v1 :: nil => f v1 | _ => None end) _ _. @@ -113,8 +113,8 @@ Next Obligation. Qed. Program Definition mkbuiltin_v2p - (tret: typ) (f: val -> val -> option val) - (WT: forall v1 v2, val_opt_has_type (f v1 v2) tret) + (tret: rettype) (f: val -> val -> option val) + (WT: forall v1 v2, val_opt_has_rettype (f v1 v2) tret) (INJ: forall j v1 v1' v2 v2', Val.inject j v1 v1' -> Val.inject j v2 v2' -> val_opt_inject j (f v1 v2) (f v1' v2')) := @@ -171,7 +171,7 @@ Proof. destruct t; intros; constructor. Qed. -Lemma inj_num_opt_wt: forall t x, val_opt_has_type (option_map (inj_num t) x) t. +Lemma inj_num_opt_wt: forall t x, val_opt_has_rettype (option_map (inj_num t) x) t. Proof. intros. destruct x; simpl. apply inj_num_wt. auto. Qed. @@ -200,13 +200,13 @@ Proof. Qed. Lemma proj_num_opt_wt: - forall tres t k0 k1 v, + forall (tres: typ) t k0 k1 v, k0 = None \/ k0 = Some Vundef -> - (forall x, val_opt_has_type (k1 x) tres) -> - val_opt_has_type (proj_num t k0 v k1) tres. + (forall x, val_opt_has_rettype (k1 x) tres) -> + val_opt_has_rettype (proj_num t k0 v k1) tres. Proof. intros. - assert (val_opt_has_type k0 tres). { destruct H; subst k0; exact I. } + assert (val_opt_has_rettype k0 tres). { destruct H; subst k0; exact I. } destruct t; simpl; destruct v; auto. Qed. @@ -393,33 +393,33 @@ Definition standard_builtin_table : list (string * standard_builtin) := Definition standard_builtin_sig (b: standard_builtin) : signature := match b with | BI_select t => - mksignature (Tint :: t :: t :: nil) (Some t) cc_default + mksignature (Tint :: t :: t :: nil) t cc_default | BI_fabs | BI_fsqrt => - mksignature (Tfloat :: nil) (Some Tfloat) cc_default + mksignature (Tfloat :: nil) Tfloat cc_default | BI_negl => - mksignature (Tlong :: nil) (Some Tlong) cc_default + mksignature (Tlong :: nil) Tlong cc_default | BI_addl | BI_subl | BI_i64_umulh| BI_i64_smulh | BI_i64_sdiv | BI_i64_udiv | BI_i64_smod | BI_i64_umod => - mksignature (Tlong :: Tlong :: nil) (Some Tlong) cc_default + mksignature (Tlong :: Tlong :: nil) Tlong cc_default | BI_mull => - mksignature (Tint :: Tint :: nil) (Some Tlong) cc_default + mksignature (Tint :: Tint :: nil) Tlong cc_default | BI_i32_bswap => - mksignature (Tint :: nil) (Some Tint) cc_default + mksignature (Tint :: nil) Tint cc_default | BI_i64_bswap => - mksignature (Tlong :: nil) (Some Tlong) cc_default + mksignature (Tlong :: nil) Tlong cc_default | BI_i16_bswap => - mksignature (Tint :: nil) (Some Tint) cc_default + mksignature (Tint :: nil) Tint cc_default | BI_i64_shl | BI_i64_shr | BI_i64_sar => - mksignature (Tlong :: Tint :: nil) (Some Tlong) cc_default + mksignature (Tlong :: Tint :: nil) Tlong cc_default | BI_i64_dtos | BI_i64_dtou => - mksignature (Tfloat :: nil) (Some Tlong) cc_default + mksignature (Tfloat :: nil) Tlong cc_default | BI_i64_stod | BI_i64_utod => - mksignature (Tlong :: nil) (Some Tfloat) cc_default + mksignature (Tlong :: nil) Tfloat cc_default | BI_i64_stof | BI_i64_utof => - mksignature (Tlong :: nil) (Some Tsingle) cc_default + mksignature (Tlong :: nil) Tsingle cc_default end. -Program Definition standard_builtin_sem (b: standard_builtin) : builtin_sem (proj_sig_res (standard_builtin_sig b)) := +Program Definition standard_builtin_sem (b: standard_builtin) : builtin_sem (sig_res (standard_builtin_sig b)) := match b with | BI_select t => mkbuiltin t diff --git a/common/Events.v b/common/Events.v index 3fb84f49..10e0c232 100644 --- a/common/Events.v +++ b/common/Events.v @@ -623,7 +623,7 @@ Record extcall_properties (sem: extcall_sem) (sg: signature) : Prop := ec_well_typed: forall ge vargs m1 t vres m2, sem ge vargs m1 t vres m2 -> - Val.has_type vres (proj_sig_res sg); + Val.has_rettype vres sg.(sig_res); (** The semantics is invariant under change of global environment that preserves symbols. *) ec_symbols_preserved: @@ -771,12 +771,12 @@ Qed. Lemma volatile_load_ok: forall chunk, extcall_properties (volatile_load_sem chunk) - (mksignature (Tptr :: nil) (Some (type_of_chunk chunk)) cc_default). + (mksignature (Tptr :: nil) (rettype_of_chunk chunk) cc_default). Proof. intros; constructor; intros. (* well typed *) -- unfold proj_sig_res; simpl. inv H. inv H0. apply Val.load_result_type. - eapply Mem.load_type; eauto. +- inv H. inv H0. apply Val.load_result_rettype. + eapply Mem.load_rettype; eauto. (* symbols *) - inv H0. constructor. eapply volatile_load_preserved; eauto. (* valid blocks *) @@ -922,7 +922,7 @@ Qed. Lemma volatile_store_ok: forall chunk, extcall_properties (volatile_store_sem chunk) - (mksignature (Tptr :: type_of_chunk chunk :: nil) None cc_default). + (mksignature (Tptr :: type_of_chunk chunk :: nil) Tvoid cc_default). Proof. intros; constructor; intros. (* well typed *) @@ -967,7 +967,7 @@ Inductive extcall_malloc_sem (ge: Senv.t): Lemma extcall_malloc_ok: extcall_properties extcall_malloc_sem - (mksignature (Tptr :: nil) (Some Tptr) cc_default). + (mksignature (Tptr :: nil) Tptr cc_default). Proof. assert (UNCHANGED: forall (P: block -> Z -> Prop) m lo hi v m' b m'', @@ -984,7 +984,7 @@ Proof. } constructor; intros. (* well typed *) -- inv H. unfold proj_sig_res, Tptr; simpl. destruct Archi.ptr64; auto. +- inv H. simpl. unfold Tptr; destruct Archi.ptr64; auto. (* symbols preserved *) - inv H0; econstructor; eauto. (* valid block *) @@ -1053,11 +1053,11 @@ Inductive extcall_free_sem (ge: Senv.t): Lemma extcall_free_ok: extcall_properties extcall_free_sem - (mksignature (Tptr :: nil) None cc_default). + (mksignature (Tptr :: nil) Tvoid cc_default). Proof. constructor; intros. (* well typed *) -- inv H. unfold proj_sig_res. simpl. auto. +- inv H. simpl. auto. (* symbols preserved *) - inv H0; econstructor; eauto. (* valid block *) @@ -1147,11 +1147,11 @@ Inductive extcall_memcpy_sem (sz al: Z) (ge: Senv.t): Lemma extcall_memcpy_ok: forall sz al, extcall_properties (extcall_memcpy_sem sz al) - (mksignature (Tptr :: Tptr :: nil) None cc_default). + (mksignature (Tptr :: Tptr :: nil) Tvoid cc_default). Proof. intros. constructor. - (* return type *) - intros. inv H. constructor. + intros. inv H. exact I. - (* change of globalenv *) intros. inv H0. econstructor; eauto. - (* valid blocks *) @@ -1258,7 +1258,7 @@ Inductive extcall_annot_sem (text: string) (targs: list typ) (ge: Senv.t): Lemma extcall_annot_ok: forall text targs, extcall_properties (extcall_annot_sem text targs) - (mksignature targs None cc_default). + (mksignature targs Tvoid cc_default). Proof. intros; constructor; intros. (* well typed *) @@ -1303,11 +1303,11 @@ Inductive extcall_annot_val_sem (text: string) (targ: typ) (ge: Senv.t): Lemma extcall_annot_val_ok: forall text targ, extcall_properties (extcall_annot_val_sem text targ) - (mksignature (targ :: nil) (Some targ) cc_default). + (mksignature (targ :: nil) targ cc_default). Proof. intros; constructor; intros. (* well typed *) -- inv H. unfold proj_sig_res; simpl. eapply eventval_match_type; eauto. +- inv H. eapply eventval_match_type; eauto. (* symbols *) - destruct H as (A & B & C). inv H0. econstructor; eauto. eapply eventval_match_preserved; eauto. @@ -1347,7 +1347,7 @@ Inductive extcall_debug_sem (ge: Senv.t): Lemma extcall_debug_ok: forall targs, extcall_properties extcall_debug_sem - (mksignature targs None cc_default). + (mksignature targs Tvoid cc_default). Proof. intros; constructor; intros. (* well typed *) @@ -1396,7 +1396,8 @@ Proof. intros. set (bsem := builtin_function_sem bf). constructor; intros. (* well typed *) - inv H. - specialize (bs_well_typed _ bsem vargs). unfold val_opt_has_type, bsem; rewrite H0. + specialize (bs_well_typed _ bsem vargs). + unfold val_opt_has_rettype, bsem; rewrite H0. auto. (* symbols *) - inv H0. econstructor; eauto. @@ -1516,7 +1517,7 @@ Proof. apply extcall_debug_ok. Qed. -Definition external_call_well_typed ef := ec_well_typed (external_call_spec ef). +Definition external_call_well_typed_gen ef := ec_well_typed (external_call_spec ef). Definition external_call_symbols_preserved ef := ec_symbols_preserved (external_call_spec ef). Definition external_call_valid_block ef := ec_valid_block (external_call_spec ef). Definition external_call_max_perm ef := ec_max_perm (external_call_spec ef). @@ -1527,6 +1528,16 @@ Definition external_call_trace_length ef := ec_trace_length (external_call_spec Definition external_call_receptive ef := ec_receptive (external_call_spec ef). Definition external_call_determ ef := ec_determ (external_call_spec ef). +(** Corollary of [external_call_well_typed_gen]. *) + +Lemma external_call_well_typed: + forall ef ge vargs m1 t vres m2, + external_call ef ge vargs m1 t vres m2 -> + Val.has_type vres (proj_sig_res (ef_sig ef)). +Proof. + intros. apply Val.has_proj_rettype. eapply external_call_well_typed_gen; eauto. +Qed. + (** Corollary of [external_call_valid_block]. *) Lemma external_call_nextblock: diff --git a/common/Memdata.v b/common/Memdata.v index 7144d72c..f3016efe 100644 --- a/common/Memdata.v +++ b/common/Memdata.v @@ -547,18 +547,26 @@ Proof. destruct v1; auto. Qed. -Lemma decode_val_type: +Lemma decode_val_rettype: forall chunk cl, - Val.has_type (decode_val chunk cl) (type_of_chunk chunk). + Val.has_rettype (decode_val chunk cl) (rettype_of_chunk chunk). Proof. intros. unfold decode_val. destruct (proj_bytes cl). - destruct chunk; simpl; auto. -Local Opaque Val.load_result. +- destruct chunk; simpl; rewrite ? Int.sign_ext_idem, ? Int.zero_ext_idem by omega; auto. +- Local Opaque Val.load_result. destruct chunk; simpl; (exact I || apply Val.load_result_type || destruct Archi.ptr64; (exact I || apply Val.load_result_type)). Qed. +Lemma decode_val_type: + forall chunk cl, + Val.has_type (decode_val chunk cl) (type_of_chunk chunk). +Proof. + intros. rewrite <- proj_rettype_of_chunk. + apply Val.has_proj_rettype. apply decode_val_rettype. +Qed. + Lemma encode_val_int8_signed_unsigned: forall v, encode_val Mint8signed v = encode_val Mint8unsigned v. Proof. @@ -607,11 +615,9 @@ Lemma decode_val_cast: | _ => True end. Proof. - unfold decode_val; intros; destruct chunk; auto; destruct (proj_bytes l); auto. - unfold Val.sign_ext. rewrite Int.sign_ext_idem; auto. omega. - unfold Val.zero_ext. rewrite Int.zero_ext_idem; auto. omega. - unfold Val.sign_ext. rewrite Int.sign_ext_idem; auto. omega. - unfold Val.zero_ext. rewrite Int.zero_ext_idem; auto. omega. + intros. + assert (A: Val.has_rettype v (rettype_of_chunk chunk)) by apply decode_val_rettype. + destruct chunk; auto; simpl in A; destruct v; try contradiction; simpl; congruence. Qed. (** Pointers cannot be forged. *) diff --git a/common/Memory.v b/common/Memory.v index 50e339e1..f21d99af 100644 --- a/common/Memory.v +++ b/common/Memory.v @@ -728,6 +728,15 @@ Proof. apply decode_val_type. Qed. +Theorem load_rettype: + forall m chunk b ofs v, + load chunk m b ofs = Some v -> + Val.has_rettype v (rettype_of_chunk chunk). +Proof. + intros. exploit load_result; eauto; intros. rewrite H0. + apply decode_val_rettype. +Qed. + Theorem load_cast: forall m chunk b ofs v, load chunk m b ofs = Some v -> diff --git a/common/Memtype.v b/common/Memtype.v index 53775d8b..ca9c6f1f 100644 --- a/common/Memtype.v +++ b/common/Memtype.v @@ -300,6 +300,11 @@ Axiom load_type: load chunk m b ofs = Some v -> Val.has_type v (type_of_chunk chunk). +Axiom load_rettype: + forall m chunk b ofs v, + load chunk m b ofs = Some v -> + Val.has_rettype v (rettype_of_chunk chunk). + (** For a small integer or float type, the value returned by [load] is invariant under the corresponding cast. *) Axiom load_cast: diff --git a/common/PrintAST.ml b/common/PrintAST.ml index baddb722..3f718428 100644 --- a/common/PrintAST.ml +++ b/common/PrintAST.ml @@ -27,6 +27,14 @@ let name_of_type = function | Tany32 -> "any32" | Tany64 -> "any64" +let name_of_rettype = function + | Tret t -> name_of_type t + | Tvoid -> "void" + | Tint8signed -> "int8s" + | Tint8unsigned -> "int8u" + | Tint16signed -> "int16s" + | Tint16unsigned -> "int16u" + let name_of_chunk = function | Mint8signed -> "int8s" | Mint8unsigned -> "int8u" diff --git a/common/Values.v b/common/Values.v index 84030123..6401ba52 100644 --- a/common/Values.v +++ b/common/Values.v @@ -149,6 +149,23 @@ Proof. auto. Defined. +Definition has_rettype (v: val) (r: rettype) : Prop := + match r, v with + | Tret t, _ => has_type v t + | Tint8signed, Vint n => n = Int.sign_ext 8 n + | Tint8unsigned, Vint n => n = Int.zero_ext 8 n + | Tint16signed, Vint n => n = Int.sign_ext 16 n + | Tint16unsigned, Vint n => n = Int.zero_ext 16 n + | _, Vundef => True + | _, _ => False + end. + +Lemma has_proj_rettype: forall v r, + has_rettype v r -> has_type v (proj_rettype r). +Proof. + destruct r; simpl; intros; auto; destruct v; try contradiction; exact I. +Qed. + (** Truth values. Non-zero integers are treated as [True]. The integer 0 (also used to represent the null pointer) is [False]. Other values are neither true nor false. *) @@ -1003,10 +1020,24 @@ Definition load_result (chunk: memory_chunk) (v: val) := | _, _ => Vundef end. +Lemma load_result_rettype: + forall chunk v, has_rettype (load_result chunk v) (rettype_of_chunk chunk). +Proof. + intros. unfold has_rettype; destruct chunk; destruct v; simpl; auto. +- rewrite Int.sign_ext_idem by omega; auto. +- rewrite Int.zero_ext_idem by omega; auto. +- rewrite Int.sign_ext_idem by omega; auto. +- rewrite Int.zero_ext_idem by omega; auto. +- destruct Archi.ptr64 eqn:SF; simpl; auto. +- destruct Archi.ptr64 eqn:SF; simpl; auto. +- destruct Archi.ptr64 eqn:SF; simpl; auto. +Qed. + Lemma load_result_type: forall chunk v, has_type (load_result chunk v) (type_of_chunk chunk). Proof. - intros. unfold has_type; destruct chunk; destruct v; simpl; auto; destruct Archi.ptr64 eqn:SF; simpl; auto. + intros. rewrite <- proj_rettype_of_chunk. apply has_proj_rettype. + apply load_result_rettype. Qed. Lemma load_result_same: diff --git a/config_aarch64.sh b/config_aarch64.sh new file mode 100755 index 00000000..ded267bf --- /dev/null +++ b/config_aarch64.sh @@ -0,0 +1 @@ +exec ./config_simple.sh aarch64-linux --toolprefix aarch64-linux-gnu- "$@" diff --git a/config_arm.sh b/config_arm.sh new file mode 100755 index 00000000..eed55fab --- /dev/null +++ b/config_arm.sh @@ -0,0 +1 @@ +exec ./config_simple.sh arm-linux --toolprefix arm-linux-gnueabihf- "$@" diff --git a/config_ia32.sh b/config_ia32.sh new file mode 100755 index 00000000..b40f2b39 --- /dev/null +++ b/config_ia32.sh @@ -0,0 +1 @@ +exec ./config_simple.sh ia32-linux "$@" diff --git a/config_k1c.sh b/config_k1c.sh new file mode 100755 index 00000000..20408397 --- /dev/null +++ b/config_k1c.sh @@ -0,0 +1 @@ +exec ./config_simple.sh k1c-cos "$@" diff --git a/config_ppc.sh b/config_ppc.sh new file mode 100755 index 00000000..d597cda5 --- /dev/null +++ b/config_ppc.sh @@ -0,0 +1 @@ +exec ./config_simple.sh ppc-linux --toolprefix powerpc-linux-gnu- "$@" diff --git a/config_rv32.sh b/config_rv32.sh new file mode 100755 index 00000000..654cacfa --- /dev/null +++ b/config_rv32.sh @@ -0,0 +1 @@ +exec ./config_simple.sh rv32-linux --toolprefix riscv64-unknown-elf- "$@" diff --git a/config_rv64.sh b/config_rv64.sh new file mode 100755 index 00000000..e95f8a70 --- /dev/null +++ b/config_rv64.sh @@ -0,0 +1 @@ +exec ./config_simple.sh rv64-linux --toolprefix riscv64-unknown-elf- "$@" diff --git a/config_simple.sh b/config_simple.sh new file mode 100755 index 00000000..f02680c4 --- /dev/null +++ b/config_simple.sh @@ -0,0 +1,6 @@ +arch=$1 +shift +version=`git rev-parse --short HEAD` +branch=`git rev-parse --abbrev-ref HEAD` +date=`date -I` +./configure --prefix /opt/CompCert/${branch}/${date}_${version}/$arch "$@" $arch diff --git a/config_x86_64.sh b/config_x86_64.sh new file mode 100755 index 00000000..b18ec95b --- /dev/null +++ b/config_x86_64.sh @@ -0,0 +1 @@ +exec ./config_simple.sh x86_64-linux "$@" @@ -12,4 +12,4 @@ make -q ${1}o || { done) } -"${COQBIN}coqide" $INCLUDES $1 && make ${1}o +"${COQBIN}coqide" -async-proofs off $INCLUDES $1 && make ${1}o diff --git a/cparser/Elab.ml b/cparser/Elab.ml index 3dbb9d45..f60e15a3 100644 --- a/cparser/Elab.ml +++ b/cparser/Elab.ml @@ -21,7 +21,7 @@ open Machine open Cabs open C open Diagnostics -open !Cutil +open! Cutil (** * Utility functions *) @@ -452,7 +452,8 @@ let elab_constant loc = function let (v, fk) = elab_float_constant f in CFloat(v, fk) | CONST_CHAR(wide, s) -> - CInt(elab_char_constant loc wide s, IInt, "") + let ikind = if wide then wchar_ikind () else IInt in + CInt(elab_char_constant loc wide s, ikind, "") | CONST_STRING(wide, s) -> elab_string_literal loc wide s diff --git a/cparser/Lexer.mll b/cparser/Lexer.mll index 346477b5..e44a330f 100644 --- a/cparser/Lexer.mll +++ b/cparser/Lexer.mll @@ -177,7 +177,7 @@ let identifier_nondigit = let identifier = identifier_nondigit (identifier_nondigit|digit)* (* Whitespaces *) -let whitespace_char_no_newline = [' ' '\t' '\012' '\r'] +let whitespace_char_no_newline = [' ' '\t' '\011' '\012' '\r'] (* Integer constants *) let nonzero_digit = ['1'-'9'] diff --git a/driver/Interp.ml b/driver/Interp.ml index a6841460..d4286779 100644 --- a/driver/Interp.ml +++ b/driver/Interp.ml @@ -15,12 +15,12 @@ open Format open Camlcoq open AST -open !Integers +open! Integers open Values open Memory open Globalenvs open Events -open Ctypes +open! Ctypes open Csyntax open Csem diff --git a/exportclight/ExportClight.ml b/exportclight/ExportClight.ml index d86e137a..c9d6fced 100644 --- a/exportclight/ExportClight.ml +++ b/exportclight/ExportClight.ml @@ -18,7 +18,7 @@ open Format open Camlcoq open AST -open Ctypes +open! Ctypes open Cop open Clight @@ -221,6 +221,14 @@ let asttype p t = | AST.Tany32 -> "AST.Tany32" | AST.Tany64 -> "AST.Tany64") +let astrettype p = function + | AST.Tret t -> asttype p t + | AST.Tvoid -> fprintf p "AST.Tvoid" + | AST.Tint8signed -> fprintf p "AST.Tint8signed" + | AST.Tint8unsigned -> fprintf p "AST.Tint8unsigned" + | AST.Tint16signed -> fprintf p "AST.Tint16signed" + | AST.Tint16unsigned -> fprintf p "AST.Tint16unsigned" + let name_of_chunk = function | Mint8signed -> "Mint8signed" | Mint8unsigned -> "Mint8unsigned" @@ -236,7 +244,7 @@ let name_of_chunk = function let signatur p sg = fprintf p "@[<hov 2>(mksignature@ %a@ %a@ %a)@]" (print_list asttype) sg.sig_args - (print_option asttype) sg.sig_res + astrettype sg.sig_res callconv sg.sig_cc let assertions = ref ([]: (string * typ list) list) @@ -116,6 +116,19 @@ Module Type TREE. forall (m1: t A) (m2: t B) (i: elt), get i (combine f m1 m2) = f (get i m1) (get i m2). + Parameter combine_null : + forall (A B C: Type) (f: A -> B -> option C), + t A -> t B -> t C. + + Axiom gcombine_null: + forall (A B C: Type) (f: A -> B -> option C), + forall (m1: t A) (m2: t B) (i: elt), + get i (combine_null f m1 m2) = + match (get i m1), (get i m2) with + | (Some x1), (Some x2) => f x1 x2 + | _, _ => None + end. + (** Enumerating the bindings of a tree. *) Parameter elements: forall (A: Type), t A -> list (elt * A). @@ -151,6 +164,12 @@ Module Type TREE. forall (A B: Type) (f: B -> A -> B) (v: B) (m: t A), fold1 f m v = List.fold_left (fun a p => f a (snd p)) (elements m) v. + + Parameter bempty_canon : + forall (A : Type), t A -> bool. + Axiom bempty_canon_correct: + forall (A : Type) (tr : t A) (i : elt), + bempty_canon tr = true -> get i tr = None. End TREE. (** * The abstract signatures of maps *) @@ -261,6 +280,12 @@ Module PTree <: TREE. induction i; simpl; auto. Qed. + Definition bempty_canon (A : Type) (tr : t A) : bool := + match tr with + | Leaf => true + | _ => false + end. + Theorem gss: forall (A: Type) (i: positive) (x: A) (m: t A), get i (set i x m) = Some x. Proof. @@ -269,7 +294,16 @@ Module PTree <: TREE. Lemma gleaf : forall (A : Type) (i : positive), get i (Leaf : t A) = None. Proof. exact gempty. Qed. - + + Lemma bempty_canon_correct: + forall (A : Type) (tr : t A) (i : elt), + bempty_canon tr = true -> get i tr = None. + Proof. + destruct tr; intros. + - rewrite gleaf; trivial. + - discriminate. + Qed. + Theorem gso: forall (A: Type) (i j: positive) (x: A) (m: t A), i <> j -> get i (set j x m) = get i m. @@ -625,7 +659,81 @@ Module PTree <: TREE. auto. Qed. - Fixpoint xelements (A : Type) (m : t A) (i : positive) + Section COMBINE_NULL. + + Variables A B C: Type. + Variable f: A -> B -> option C. + + + Fixpoint combine_null (m1: t A) (m2: t B) {struct m1} : t C := + match m1, m2 with + | (Node l1 o1 r1), (Node l2 o2 r2) => + Node' (combine_null l1 l2) + (match o1, o2 with + | (Some x1), (Some x2) => f x1 x2 + | _, _ => None + end) + (combine_null r1 r2) + | _, _ => Leaf + end. + + Theorem gcombine_null: + forall (m1: t A) (m2: t B) (i: positive), + get i (combine_null m1 m2) = + match (get i m1), (get i m2) with + | (Some x1), (Some x2) => f x1 x2 + | _, _ => None + end. + Proof. + induction m1; intros; simpl. + - rewrite gleaf. rewrite gleaf. + reflexivity. + - destruct m2; simpl. + + rewrite gleaf. rewrite gleaf. + destruct get; reflexivity. + + rewrite gnode'. + destruct i; simpl; try rewrite IHm1_1; try rewrite IHm1; trivial. + Qed. + + End COMBINE_NULL. + + Section REMOVE_TREE. + + Variables A B: Type. + + Fixpoint remove_t (m1: t A) (m2: t B) {struct m1} : t A := + match m1, m2 with + | Leaf, _ | _, Leaf => m1 + | (Node l1 o1 r1), (Node l2 o2 r2) => + Node' (remove_t l1 l2) + (match o2 with + | Some _ => None + | None => o1 + end) + (remove_t r1 r2) + end. + + Theorem gremove_t: + forall m1 : t A, + forall m2 : t B, + forall i : positive, + get i (remove_t m1 m2) = match get i m2 with + | None => get i m1 + | Some _ => None + end. + Proof. + induction m1; intros; simpl. + - rewrite gleaf. + destruct get; reflexivity. + - destruct m2; simpl. + + rewrite gleaf. + reflexivity. + + rewrite gnode'. + destruct i; simpl; try rewrite IHm1_1; try rewrite IHm1; trivial. + Qed. + End REMOVE_TREE. + + Fixpoint xelements (A : Type) (m : t A) (i : positive) (k: list (positive * A)) {struct m} : list (positive * A) := match m with diff --git a/mppa_k1c/Builtins1.v b/mppa_k1c/Builtins1.v index 6186961f..3b5cd419 100644 --- a/mppa_k1c/Builtins1.v +++ b/mppa_k1c/Builtins1.v @@ -43,18 +43,18 @@ Definition platform_builtin_table : list (string * platform_builtin) := Definition platform_builtin_sig (b: platform_builtin) : signature := match b with | BI_fmin | BI_fmax => - mksignature (Tfloat :: Tfloat :: nil) (Some Tfloat) cc_default + mksignature (Tfloat :: Tfloat :: nil) Tfloat cc_default | BI_fminf | BI_fmaxf => - mksignature (Tsingle :: Tsingle :: nil) (Some Tsingle) cc_default + mksignature (Tsingle :: Tsingle :: nil) Tsingle cc_default | BI_fabsf => - mksignature (Tsingle :: nil) (Some Tsingle) cc_default + mksignature (Tsingle :: nil) Tsingle cc_default | BI_fma => - mksignature (Tfloat :: Tfloat :: Tfloat :: nil) (Some Tfloat) cc_default + mksignature (Tfloat :: Tfloat :: Tfloat :: nil) Tfloat cc_default | BI_fmaf => - mksignature (Tsingle :: Tsingle :: Tsingle :: nil) (Some Tsingle) cc_default + mksignature (Tsingle :: Tsingle :: Tsingle :: nil) Tsingle cc_default end. -Definition platform_builtin_sem (b: platform_builtin) : builtin_sem (proj_sig_res (platform_builtin_sig b)) := +Definition platform_builtin_sem (b: platform_builtin) : builtin_sem (sig_res (platform_builtin_sig b)) := match b with | BI_fmin => mkbuiltin_n2t Tfloat Tfloat Tfloat ExtFloat.min | BI_fmax => mkbuiltin_n2t Tfloat Tfloat Tfloat ExtFloat.max diff --git a/mppa_k1c/Conventions1.v b/mppa_k1c/Conventions1.v index d41f1095..48346a6d 100644 --- a/mppa_k1c/Conventions1.v +++ b/mppa_k1c/Conventions1.v @@ -90,12 +90,17 @@ Definition is_float_reg (r: mreg) := false. returned value. We treat a function without result as a function with one integer result. *) + Definition loc_result (s: signature) : rpair mreg := - match s.(sig_res) with - | None => One R0 - | Some (Tint | Tany32) => One R0 - | Some (Tfloat | Tsingle | Tany64) => One R0 - | Some Tlong => if Archi.ptr64 then One R0 else One R0 + match s.(sig_res) with + | Tvoid => One R0 + | Tint8signed => One R0 + | Tint8unsigned => One R0 + | Tint16signed => One R0 + | Tint16unsigned => One R0 + | Tint | Tany32 => One R0 + | Tfloat | Tsingle | Tany64 => One R0 + | Tlong => if Archi.ptr64 then One R0 else One R0 end. (** The result registers have types compatible with that given in the signature. *) @@ -104,8 +109,8 @@ Lemma loc_result_type: forall sig, subtype (proj_sig_res sig) (typ_rpair mreg_type (loc_result sig)) = true. Proof. - intros. unfold proj_sig_res, loc_result, mreg_type; - destruct (sig_res sig) as [[]|]; auto; destruct Archi.ptr64; auto. + intros. unfold proj_sig_res, loc_result, mreg_type. + destruct (sig_res sig); try destruct Archi.ptr64; simpl; trivial; destruct t; trivial. Qed. (** The result locations are caller-save registers *) @@ -115,7 +120,7 @@ Lemma loc_result_caller_save: forall_rpair (fun r => is_callee_save r = false) (loc_result s). Proof. intros. unfold loc_result, is_callee_save; - destruct (sig_res s) as [[]|]; simpl; auto; destruct Archi.ptr64; simpl; auto. + destruct (sig_res s); simpl; auto; try destruct Archi.ptr64; simpl; auto; try destruct t; simpl; auto. Qed. (** If the result is in a pair of registers, those registers are distinct and have type [Tint] at least. *) @@ -125,14 +130,15 @@ Lemma loc_result_pair: match loc_result sg with | One _ => True | Twolong r1 r2 => - r1 <> r2 /\ sg.(sig_res) = Some Tlong + r1 <> r2 /\ proj_sig_res sg = Tlong /\ subtype Tint (mreg_type r1) = true /\ subtype Tint (mreg_type r2) = true /\ Archi.ptr64 = false end. Proof. intros. - unfold loc_result; destruct (sig_res sg) as [[]|]; auto. - unfold mreg_type; destruct Archi.ptr64; auto. + unfold loc_result; destruct (sig_res sg); auto; + unfold mreg_type; try destruct Archi.ptr64; auto; + destruct t; auto. Qed. (** The location of the result depends only on the result part of the signature *) @@ -409,3 +415,6 @@ Lemma loc_arguments_main: Proof. reflexivity. Qed. + + +Definition return_value_needs_normalization (t: rettype) : bool := false. diff --git a/powerpc/Asmexpand.ml b/powerpc/Asmexpand.ml index 704b0aba..ce88778c 100644 --- a/powerpc/Asmexpand.ml +++ b/powerpc/Asmexpand.ml @@ -852,7 +852,7 @@ let expand_instruction instr = if variadic then begin emit (Pmflr GPR0); emit (Pbl(intern_string "__compcert_va_saveregs", - {sig_args = []; sig_res = None; sig_cc = cc_default})); + {sig_args = []; sig_res = Tvoid; sig_cc = cc_default})); emit (Pmtlr GPR0) end; current_function_stacksize := sz; diff --git a/powerpc/Builtins1.v b/powerpc/Builtins1.v index f6e643d2..53c83d7e 100644 --- a/powerpc/Builtins1.v +++ b/powerpc/Builtins1.v @@ -29,5 +29,5 @@ Definition platform_builtin_table : list (string * platform_builtin) := Definition platform_builtin_sig (b: platform_builtin) : signature := match b with end. -Definition platform_builtin_sem (b: platform_builtin) : builtin_sem (proj_sig_res (platform_builtin_sig b)) := +Definition platform_builtin_sem (b: platform_builtin) : builtin_sem (sig_res (platform_builtin_sig b)) := match b with end. diff --git a/powerpc/Conventions1.v b/powerpc/Conventions1.v index 1de55c1a..1f048694 100644 --- a/powerpc/Conventions1.v +++ b/powerpc/Conventions1.v @@ -117,18 +117,16 @@ Definition dummy_float_reg := F0. (**r Used in [Coloring]. *) We treat a function without result as a function with one integer result. *) Definition loc_result_32 (s: signature) : rpair mreg := - match s.(sig_res) with - | None => One R3 - | Some (Tint | Tany32) => One R3 - | Some (Tfloat | Tsingle | Tany64) => One F1 - | Some Tlong => Twolong R3 R4 + match proj_sig_res s with + | Tint | Tany32 => One R3 + | Tfloat | Tsingle | Tany64 => One F1 + | Tlong => Twolong R3 R4 end. Definition loc_result_64 (s: signature) : rpair mreg := - match s.(sig_res) with - | None => One R3 - | Some (Tint | Tlong | Tany32 | Tany64) => One R3 - | Some (Tfloat | Tsingle) => One F1 + match proj_sig_res s with + | Tint | Tlong | Tany32 | Tany64 => One R3 + | Tfloat | Tsingle => One F1 end. Definition loc_result := @@ -140,8 +138,8 @@ Lemma loc_result_type: forall sig, subtype (proj_sig_res sig) (typ_rpair mreg_type (loc_result sig)) = true. Proof. - intros. unfold proj_sig_res, loc_result, loc_result_32, loc_result_64, mreg_type. - destruct Archi.ptr64 eqn:?; destruct (sig_res sig) as [[]|]; destruct Archi.ppc64; simpl; auto. + intros. unfold loc_result, loc_result_32, loc_result_64, mreg_type. + destruct Archi.ptr64 eqn:?; destruct (proj_sig_res sig); destruct Archi.ppc64; simpl; auto. Qed. (** The result locations are caller-save registers *) @@ -151,7 +149,7 @@ Lemma loc_result_caller_save: forall_rpair (fun r => is_callee_save r = false) (loc_result s). Proof. intros. unfold loc_result, loc_result_32, loc_result_64, is_callee_save; - destruct Archi.ptr64; destruct (sig_res s) as [[]|]; simpl; auto. + destruct Archi.ptr64; destruct (proj_sig_res s); simpl; auto. Qed. (** If the result is in a pair of registers, those registers are distinct and have type [Tint] at least. *) @@ -161,13 +159,13 @@ Lemma loc_result_pair: match loc_result sg with | One _ => True | Twolong r1 r2 => - r1 <> r2 /\ sg.(sig_res) = Some Tlong + r1 <> r2 /\ proj_sig_res sg = Tlong /\ subtype Tint (mreg_type r1) = true /\ subtype Tint (mreg_type r2) = true /\ Archi.ptr64 = false end. Proof. intros; unfold loc_result, loc_result_32, loc_result_64, mreg_type; - destruct Archi.ptr64; destruct (sig_res sg) as [[]|]; destruct Archi.ppc64; simpl; auto. + destruct Archi.ptr64; destruct (proj_sig_res sg); destruct Archi.ppc64; simpl; auto. split; auto. congruence. split; auto. congruence. Qed. @@ -177,7 +175,7 @@ Qed. Lemma loc_result_exten: forall s1 s2, s1.(sig_res) = s2.(sig_res) -> loc_result s1 = loc_result s2. Proof. - intros. unfold loc_result, loc_result_32, loc_result_64. + intros. unfold loc_result, loc_result_32, loc_result_64, proj_sig_res. destruct Archi.ptr64; rewrite H; auto. Qed. @@ -238,33 +236,6 @@ Fixpoint loc_arguments_rec Definition loc_arguments (s: signature) : list (rpair loc) := loc_arguments_rec s.(sig_args) 0 0 0. -(** [size_arguments s] returns the number of [Outgoing] slots used - to call a function with signature [s]. *) - -Fixpoint size_arguments_rec (tyl: list typ) (ir fr ofs: Z) {struct tyl} : Z := - match tyl with - | nil => ofs - | (Tint | Tany32) :: tys => - match list_nth_z int_param_regs ir with - | None => size_arguments_rec tys ir fr (ofs + 1) - | Some ireg => size_arguments_rec tys (ir + 1) fr ofs - end - | (Tfloat | Tsingle | Tany64) :: tys => - match list_nth_z float_param_regs fr with - | None => size_arguments_rec tys ir fr (align ofs 2 + 2) - | Some freg => size_arguments_rec tys ir (fr + 1) ofs - end - | Tlong :: tys => - let ir := align ir 2 in - match list_nth_z int_param_regs ir, list_nth_z int_param_regs (ir + 1) with - | Some r1, Some r2 => size_arguments_rec tys (ir + 2) fr ofs - | _, _ => size_arguments_rec tys ir fr (align ofs 2 + 2) - end - end. - -Definition size_arguments (s: signature) : Z := - size_arguments_rec s.(sig_args) 0 0 0. - (** Argument locations are either caller-save registers or [Outgoing] stack slots at nonnegative offsets. *) @@ -361,107 +332,14 @@ Qed. Hint Resolve loc_arguments_acceptable: locs. -(** The offsets of [Outgoing] arguments are below [size_arguments s]. *) - -Remark size_arguments_rec_above: - forall tyl ir fr ofs0, - ofs0 <= size_arguments_rec tyl ir fr ofs0. -Proof. - induction tyl; simpl; intros. - omega. - destruct a. - destruct (list_nth_z int_param_regs ir); eauto. apply Z.le_trans with (ofs0 + 1); auto; omega. - destruct (list_nth_z float_param_regs fr); eauto. - apply Z.le_trans with (align ofs0 2). apply align_le; omega. - apply Z.le_trans with (align ofs0 2 + 2); auto; omega. - set (ir' := align ir 2). - destruct (list_nth_z int_param_regs ir'); eauto. - destruct (list_nth_z int_param_regs (ir' + 1)); eauto. - apply Z.le_trans with (align ofs0 2). apply align_le; omega. - apply Z.le_trans with (align ofs0 2 + 2); auto; omega. - apply Z.le_trans with (align ofs0 2). apply align_le; omega. - apply Z.le_trans with (align ofs0 2 + 2); auto; omega. - destruct (list_nth_z float_param_regs fr); eauto. - apply Z.le_trans with (align ofs0 2). apply align_le; omega. - apply Z.le_trans with (align ofs0 2 + 2); auto; omega. - destruct (list_nth_z int_param_regs ir); eauto. apply Z.le_trans with (ofs0 + 1); auto; omega. - destruct (list_nth_z float_param_regs fr); eauto. - apply Z.le_trans with (align ofs0 2). apply align_le; omega. - apply Z.le_trans with (align ofs0 2 + 2); auto; omega. -Qed. - -Lemma size_arguments_above: - forall s, size_arguments s >= 0. -Proof. - intros; unfold size_arguments. apply Z.le_ge. - apply size_arguments_rec_above. -Qed. - -Lemma loc_arguments_bounded: - forall (s: signature) (ofs: Z) (ty: typ), - In (S Outgoing ofs ty) (regs_of_rpairs (loc_arguments s)) -> - ofs + typesize ty <= size_arguments s. -Proof. - intros. - assert (forall tyl ir fr ofs0, - In (S Outgoing ofs ty) (regs_of_rpairs (loc_arguments_rec tyl ir fr ofs0)) -> - ofs + typesize ty <= size_arguments_rec tyl ir fr ofs0). -{ - induction tyl; simpl; intros. - elim H0. - destruct a. -- (* int *) - destruct (list_nth_z int_param_regs ir); destruct H0. - congruence. - eauto. - inv H0. apply size_arguments_rec_above. - eauto. -- (* float *) - destruct (list_nth_z float_param_regs fr); destruct H0. - congruence. - eauto. - inv H0. apply size_arguments_rec_above. eauto. -- (* long *) - set (ir' := align ir 2) in *. - assert (DFL: - In (S Outgoing ofs ty) (regs_of_rpairs - ((if Archi.ptr64 - then One (S Outgoing (align ofs0 2) Tlong) - else Twolong (S Outgoing (align ofs0 2) Tint) - (S Outgoing (align ofs0 2 + 1) Tint)) - :: loc_arguments_rec tyl ir' fr (align ofs0 2 + 2))) -> - ofs + typesize ty <= size_arguments_rec tyl ir' fr (align ofs0 2 + 2)). - { destruct Archi.ptr64; intros IN. - - destruct IN. inv H1. apply size_arguments_rec_above. auto. - - destruct IN. inv H1. transitivity (align ofs0 2 + 2). simpl; omega. apply size_arguments_rec_above. - destruct H1. inv H1. transitivity (align ofs0 2 + 2). simpl; omega. apply size_arguments_rec_above. - auto. } - destruct (list_nth_z int_param_regs ir'); auto. - destruct (list_nth_z int_param_regs (ir' + 1)); auto. - destruct H0. congruence. destruct H0. congruence. eauto. -- (* single *) - destruct (list_nth_z float_param_regs fr); destruct H0. - congruence. - eauto. - inv H0. transitivity (align ofs0 2 + 2). simpl; omega. apply size_arguments_rec_above. - eauto. -- (* any32 *) - destruct (list_nth_z int_param_regs ir); destruct H0. - congruence. - eauto. - inv H0. apply size_arguments_rec_above. - eauto. -- (* any64 *) - destruct (list_nth_z float_param_regs fr); destruct H0. - congruence. - eauto. - inv H0. apply size_arguments_rec_above. eauto. - } - eauto. -Qed. - Lemma loc_arguments_main: loc_arguments signature_main = nil. Proof. reflexivity. Qed. + +(** ** Normalization of function results *) + +(** No normalization needed. *) + +Definition return_value_needs_normalization (t: rettype) := false. diff --git a/riscV/Asmexpand.ml b/riscV/Asmexpand.ml index 1df63308..7e36abf8 100644 --- a/riscV/Asmexpand.ml +++ b/riscV/Asmexpand.ml @@ -23,7 +23,7 @@ open Asm open Asmexpandaux open AST open Camlcoq -open !Integers +open! Integers exception Error of string @@ -63,44 +63,44 @@ let expand_storeind_ptr src base ofs = let int_param_regs = [| X10; X11; X12; X13; X14; X15; X16; X17 |] let float_param_regs = [| F10; F11; F12; F13; F14; F15; F16; F17 |] -let rec fixup_variadic_call pos tyl = - if pos < 8 then +let rec fixup_variadic_call ri rf tyl = + if ri < 8 then match tyl with | [] -> () | (Tint | Tany32) :: tyl -> - fixup_variadic_call (pos + 1) tyl + fixup_variadic_call (ri + 1) rf tyl | Tsingle :: tyl -> - let rs =float_param_regs.(pos) - and rd = int_param_regs.(pos) in + let rs = float_param_regs.(rf) + and rd = int_param_regs.(ri) in emit (Pfmvxs(rd, rs)); - fixup_variadic_call (pos + 1) tyl + fixup_variadic_call (ri + 1) (rf + 1) tyl | Tlong :: tyl -> - let pos' = if Archi.ptr64 then pos + 1 else align pos 2 + 2 in - fixup_variadic_call pos' tyl + let ri' = if Archi.ptr64 then ri + 1 else align ri 2 + 2 in + fixup_variadic_call ri' rf tyl | (Tfloat | Tany64) :: tyl -> if Archi.ptr64 then begin - let rs = float_param_regs.(pos) - and rd = int_param_regs.(pos) in + let rs = float_param_regs.(rf) + and rd = int_param_regs.(ri) in emit (Pfmvxd(rd, rs)); - fixup_variadic_call (pos + 1) tyl + fixup_variadic_call (ri + 1) (rf + 1) tyl end else begin - let pos = align pos 2 in - if pos < 8 then begin - let rs = float_param_regs.(pos) - and rd1 = int_param_regs.(pos) - and rd2 = int_param_regs.(pos + 1) in + let ri = align ri 2 in + if ri < 8 then begin + let rs = float_param_regs.(rf) + and rd1 = int_param_regs.(ri) + and rd2 = int_param_regs.(ri + 1) in emit (Paddiw(X2, X X2, Integers.Int.neg _16)); emit (Pfsd(rs, X2, Ofsimm _0)); emit (Plw(rd1, X2, Ofsimm _0)); emit (Plw(rd2, X2, Ofsimm _4)); emit (Paddiw(X2, X X2, _16)); - fixup_variadic_call (pos + 2) tyl + fixup_variadic_call (ri + 2) (rf + 1) tyl end end let fixup_call sg = - if sg.sig_cc.cc_vararg then fixup_variadic_call 0 sg.sig_args + if sg.sig_cc.cc_vararg then fixup_variadic_call 0 0 sg.sig_args (* Handling of annotations *) diff --git a/riscV/Builtins1.v b/riscV/Builtins1.v index f6e643d2..53c83d7e 100644 --- a/riscV/Builtins1.v +++ b/riscV/Builtins1.v @@ -29,5 +29,5 @@ Definition platform_builtin_table : list (string * platform_builtin) := Definition platform_builtin_sig (b: platform_builtin) : signature := match b with end. -Definition platform_builtin_sem (b: platform_builtin) : builtin_sem (proj_sig_res (platform_builtin_sig b)) := +Definition platform_builtin_sem (b: platform_builtin) : builtin_sem (sig_res (platform_builtin_sig b)) := match b with end. diff --git a/riscV/Conventions1.v b/riscV/Conventions1.v index df7ddfd2..7f8048f6 100644 --- a/riscV/Conventions1.v +++ b/riscV/Conventions1.v @@ -105,7 +105,9 @@ Definition is_float_reg (r: mreg) := of function arguments), but this leaves much liberty in choosing actual locations. To ensure binary interoperability of code generated by our compiler with libraries compiled by another compiler, we - implement the standard RISC-V conventions. *) + implement the standard RISC-V conventions as found here: + https://github.com/riscv/riscv-elf-psabi-doc/blob/master/riscv-elf.md +*) (** ** Location of function result *) @@ -115,11 +117,10 @@ Definition is_float_reg (r: mreg) := with one integer result. *) Definition loc_result (s: signature) : rpair mreg := - match s.(sig_res) with - | None => One R10 - | Some (Tint | Tany32) => One R10 - | Some (Tfloat | Tsingle | Tany64) => One F10 - | Some Tlong => if Archi.ptr64 then One R10 else Twolong R11 R10 + match proj_sig_res s with + | Tint | Tany32 => One R10 + | Tfloat | Tsingle | Tany64 => One F10 + | Tlong => if Archi.ptr64 then One R10 else Twolong R11 R10 end. (** The result registers have types compatible with that given in the signature. *) @@ -128,8 +129,8 @@ Lemma loc_result_type: forall sig, subtype (proj_sig_res sig) (typ_rpair mreg_type (loc_result sig)) = true. Proof. - intros. unfold proj_sig_res, loc_result, mreg_type; - destruct (sig_res sig) as [[]|]; auto; destruct Archi.ptr64; auto. + intros. unfold loc_result, mreg_type; + destruct (proj_sig_res sig); auto; destruct Archi.ptr64; auto. Qed. (** The result locations are caller-save registers *) @@ -139,7 +140,7 @@ Lemma loc_result_caller_save: forall_rpair (fun r => is_callee_save r = false) (loc_result s). Proof. intros. unfold loc_result, is_callee_save; - destruct (sig_res s) as [[]|]; simpl; auto; destruct Archi.ptr64; simpl; auto. + destruct (proj_sig_res s); simpl; auto; destruct Archi.ptr64; simpl; auto. Qed. (** If the result is in a pair of registers, those registers are distinct and have type [Tint] at least. *) @@ -149,13 +150,13 @@ Lemma loc_result_pair: match loc_result sg with | One _ => True | Twolong r1 r2 => - r1 <> r2 /\ sg.(sig_res) = Some Tlong + r1 <> r2 /\ proj_sig_res sg = Tlong /\ subtype Tint (mreg_type r1) = true /\ subtype Tint (mreg_type r2) = true /\ Archi.ptr64 = false end. Proof. intros. - unfold loc_result; destruct (sig_res sg) as [[]|]; auto. + unfold loc_result; destruct (proj_sig_res sg); auto. unfold mreg_type; destruct Archi.ptr64; auto. split; auto. congruence. Qed. @@ -165,43 +166,37 @@ Qed. Lemma loc_result_exten: forall s1 s2, s1.(sig_res) = s2.(sig_res) -> loc_result s1 = loc_result s2. Proof. - intros. unfold loc_result. rewrite H; auto. + intros. unfold loc_result, proj_sig_res. rewrite H; auto. Qed. (** ** Location of function arguments *) -(** The RISC-V ABI states the following convention for passing arguments +(** The RISC-V ABI states the following conventions for passing arguments to a function: -- Arguments are passed in registers when possible. - -- Up to eight integer registers (ai: int_param_regs) and up to eight - floating-point registers (fai: float_param_regs) are used for this - purpose. - -- If the arguments to a function are conceptualized as fields of a C - struct, each with pointer alignment, the argument registers are a - shadow of the first eight pointer-words of that struct. If argument - i < 8 is a floating-point type, it is passed in floating-point - register fa_i; otherwise, it is passed in integer register a_i. - -- When primitive arguments twice the size of a pointer-word are passed - on the stack, they are naturally aligned. When they are passed in the - integer registers, they reside in an aligned even-odd register pair, - with the even register holding the least-significant bits. - -- Floating-point arguments to variadic functions (except those that - are explicitly named in the parameter list) are passed in integer - registers. - -- The portion of the conceptual struct that is not passed in argument - registers is passed on the stack. The stack pointer sp points to the - first argument not passed in a register. - -The bit about variadic functions doesn't quite fit CompCert's model. -We do our best by passing the FP arguments in registers, as usual, -and reserving the corresponding integer registers, so that fixup -code can be introduced in the Asmexpand pass. +- RV64, not variadic: pass the first 8 integer arguments in + integer registers (a1...a8: int_param_regs), the first 8 FP arguments + in FP registers (fa1...fa8: float_param_regs), and the remaining + arguments on the stack, in 8-byte slots. + +- RV32, not variadic: same, but arguments of 64-bit integer type + are passed in two consecutive integer registers (a(i), a(i+1)) + or in a(8) and on a 32-bit word on the stack. Stack-allocated + arguments are aligned to their natural alignment. + +- RV64, variadic: pass the first 8 arguments in integer registers + (a1...a8), including FP arguments; pass the remaining arguments on + the stack, in 8-byte slots. + +- RV32, variadic: same, but arguments of 64-bit types (integers as well + as floats) are passed in two consecutive aligned integer registers + (a(2i), a(2i+1)). + +The passing of FP arguments to variadic functions in integer registers +doesn't quite fit CompCert's model. We do our best by passing the FP +arguments in registers, as usual, and reserving the corresponding +integer registers, so that fixup code can be introduced in the +Asmexpand pass. *) Definition int_param_regs := @@ -209,80 +204,84 @@ Definition int_param_regs := Definition float_param_regs := F10 :: F11 :: F12 :: F13 :: F14 :: F15 :: F16 :: F17 :: nil. -Definition one_arg (regs: list mreg) (rn: Z) (ofs: Z) (ty: typ) - (rec: Z -> Z -> list (rpair loc)) := - match list_nth_z regs rn with +Definition int_arg (ri rf ofs: Z) (ty: typ) + (rec: Z -> Z -> Z -> list (rpair loc)) := + match list_nth_z int_param_regs ri with | Some r => - One(R r) :: rec (rn + 1) ofs + One(R r) :: rec (ri + 1) rf ofs | None => let ofs := align ofs (typealign ty) in - One(S Outgoing ofs ty) :: rec rn (ofs + (if Archi.ptr64 then 2 else typesize ty)) + One(S Outgoing ofs ty) + :: rec ri rf (ofs + (if Archi.ptr64 then 2 else typesize ty)) end. -Definition two_args (regs: list mreg) (rn: Z) (ofs: Z) - (rec: Z -> Z -> list (rpair loc)) := - let rn := align rn 2 in - match list_nth_z regs rn, list_nth_z regs (rn + 1) with - | Some r1, Some r2 => - Twolong (R r2) (R r1) :: rec (rn + 2) ofs - | _, _ => - let ofs := align ofs 2 in - Twolong (S Outgoing (ofs + 1) Tint) (S Outgoing ofs Tint) :: - rec rn (ofs + 2) +Definition float_arg (va: bool) (ri rf ofs: Z) (ty: typ) + (rec: Z -> Z -> Z -> list (rpair loc)) := + match list_nth_z float_param_regs rf with + | Some r => + if va then + (let ri' := (* reserve 1 or 2 aligned integer registers *) + if Archi.ptr64 || zeq (typesize ty) 1 then ri + 1 else align ri 2 + 2 in + if zle ri' 8 then + (* we have enough integer registers, put argument in FP reg + and fixup code will put it in one or two integer regs *) + One (R r) :: rec ri' (rf + 1) ofs + else + (* we are out of integer registers, pass argument on stack *) + let ofs := align ofs (typealign ty) in + One(S Outgoing ofs ty) + :: rec ri' rf (ofs + (if Archi.ptr64 then 2 else typesize ty))) + else + One (R r) :: rec ri (rf + 1) ofs + | None => + let ofs := align ofs (typealign ty) in + One(S Outgoing ofs ty) + :: rec ri rf (ofs + (if Archi.ptr64 then 2 else typesize ty)) end. -Definition hybrid_arg (regs: list mreg) (rn: Z) (ofs: Z) (ty: typ) - (rec: Z -> Z -> list (rpair loc)) := - let rn := align rn 2 in - match list_nth_z regs rn with - | Some r => - One (R r) :: rec (rn + 2) ofs - | None => +Definition split_long_arg (va: bool) (ri rf ofs: Z) + (rec: Z -> Z -> Z -> list (rpair loc)) := + let ri := if va then align ri 2 else ri in + match list_nth_z int_param_regs ri, list_nth_z int_param_regs (ri + 1) with + | Some r1, Some r2 => + Twolong (R r2) (R r1) :: rec (ri + 2) rf ofs + | Some r1, None => + Twolong (S Outgoing ofs Tint) (R r1) :: rec (ri + 1) rf (ofs + 1) + | None, _ => let ofs := align ofs 2 in - One (S Outgoing ofs ty) :: rec rn (ofs + 2) + Twolong (S Outgoing (ofs + 1) Tint) (S Outgoing ofs Tint) :: + rec ri rf (ofs + 2) end. Fixpoint loc_arguments_rec (va: bool) - (tyl: list typ) (r ofs: Z) {struct tyl} : list (rpair loc) := + (tyl: list typ) (ri rf ofs: Z) {struct tyl} : list (rpair loc) := match tyl with | nil => nil | (Tint | Tany32) as ty :: tys => - one_arg int_param_regs r ofs ty (loc_arguments_rec va tys) + (* pass in one integer register or on stack *) + int_arg ri rf ofs ty (loc_arguments_rec va tys) | Tsingle as ty :: tys => - one_arg float_param_regs r ofs ty (loc_arguments_rec va tys) + (* pass in one FP register or on stack. + If vararg, reserve 1 integer register. *) + float_arg va ri rf ofs ty (loc_arguments_rec va tys) | Tlong as ty :: tys => - if Archi.ptr64 - then one_arg int_param_regs r ofs ty (loc_arguments_rec va tys) - else two_args int_param_regs r ofs (loc_arguments_rec va tys) + if Archi.ptr64 then + (* pass in one integer register or on stack *) + int_arg ri rf ofs ty (loc_arguments_rec va tys) + else + (* pass in register pair or on stack; align register pair if vararg *) + split_long_arg va ri rf ofs(loc_arguments_rec va tys) | (Tfloat | Tany64) as ty :: tys => - if va && negb Archi.ptr64 - then hybrid_arg float_param_regs r ofs ty (loc_arguments_rec va tys) - else one_arg float_param_regs r ofs ty (loc_arguments_rec va tys) + (* pass in one FP register or on stack. + If vararg, reserve 1 or 2 integer registers. *) + float_arg va ri rf ofs ty (loc_arguments_rec va tys) end. (** [loc_arguments s] returns the list of locations where to store arguments when calling a function with signature [s]. *) Definition loc_arguments (s: signature) : list (rpair loc) := - loc_arguments_rec s.(sig_cc).(cc_vararg) s.(sig_args) 0 0. - -(** [size_arguments s] returns the number of [Outgoing] slots used - to call a function with signature [s]. *) - -Definition max_outgoing_1 (accu: Z) (l: loc) : Z := - match l with - | S Outgoing ofs ty => Z.max accu (ofs + typesize ty) - | _ => accu - end. - -Definition max_outgoing_2 (accu: Z) (rl: rpair loc) : Z := - match rl with - | One l => max_outgoing_1 accu l - | Twolong l1 l2 => max_outgoing_1 (max_outgoing_1 accu l1) l2 - end. - -Definition size_arguments (s: signature) : Z := - List.fold_left max_outgoing_2 (loc_arguments s) 0. + loc_arguments_rec s.(sig_cc).(cc_vararg) s.(sig_args) 0 0 0. (** Argument locations are either non-temporary registers or [Outgoing] stack slots at nonnegative offsets. *) @@ -295,15 +294,18 @@ Definition loc_argument_acceptable (l: loc) : Prop := end. Lemma loc_arguments_rec_charact: - forall va tyl rn ofs p, + forall va tyl ri rf ofs p, ofs >= 0 -> - In p (loc_arguments_rec va tyl rn ofs) -> forall_rpair loc_argument_acceptable p. + In p (loc_arguments_rec va tyl ri rf ofs) -> forall_rpair loc_argument_acceptable p. Proof. set (OK := fun (l: list (rpair loc)) => forall p, In p l -> forall_rpair loc_argument_acceptable p). - set (OKF := fun (f: Z -> Z -> list (rpair loc)) => - forall rn ofs, ofs >= 0 -> OK (f rn ofs)). - set (OKREGS := fun (l: list mreg) => forall r, In r l -> is_callee_save r = false). + set (OKF := fun (f: Z -> Z -> Z -> list (rpair loc)) => + forall ri rf ofs, ofs >= 0 -> OK (f ri rf ofs)). + assert (CSI: forall r, In r int_param_regs -> is_callee_save r = false). + { decide_goal. } + assert (CSF: forall r, In r float_param_regs -> is_callee_save r = false). + { decide_goal. } assert (AL: forall ofs ty, ofs >= 0 -> align ofs (typealign ty) >= 0). { intros. assert (ofs <= align ofs (typealign ty)) by (apply align_le; apply typealign_pos). @@ -312,73 +314,64 @@ Proof. { destruct Archi.ptr64; omega. } assert (SKK: forall ty, (if Archi.ptr64 then 2 else typesize ty) > 0). { intros. destruct Archi.ptr64. omega. apply typesize_pos. } - assert (A: forall regs rn ofs ty f, - OKREGS regs -> OKF f -> ofs >= 0 -> OK (one_arg regs rn ofs ty f)). - { intros until f; intros OR OF OO; red; unfold one_arg; intros. - destruct (list_nth_z regs rn) as [r|] eqn:NTH; destruct H. - - subst p; simpl. apply OR. eapply list_nth_z_in; eauto. + assert (A: forall ri rf ofs ty f, + OKF f -> ofs >= 0 -> OK (int_arg ri rf ofs ty f)). + { intros until f; intros OF OO; red; unfold int_arg; intros. + destruct (list_nth_z int_param_regs ri) as [r|] eqn:NTH; destruct H. + - subst p; simpl. apply CSI. eapply list_nth_z_in; eauto. - eapply OF; eauto. - subst p; simpl. auto using align_divides, typealign_pos. - eapply OF; [idtac|eauto]. generalize (AL ofs ty OO) (SKK ty); omega. } - assert (B: forall regs rn ofs f, - OKREGS regs -> OKF f -> ofs >= 0 -> OK (two_args regs rn ofs f)). - { intros until f; intros OR OF OO; unfold two_args. - set (rn' := align rn 2). + assert (B: forall va ri rf ofs ty f, + OKF f -> ofs >= 0 -> OK (float_arg va ri rf ofs ty f)). + { intros until f; intros OF OO; red; unfold float_arg; intros. + destruct (list_nth_z float_param_regs rf) as [r|] eqn:NTH. + - set (ri' := if Archi.ptr64 || zeq (typesize ty) 1 then ri + 1 else align ri 2 + 2) in *. + destruct va; [destruct (zle ri' 8)|idtac]; destruct H. + + subst p; simpl. apply CSF. eapply list_nth_z_in; eauto. + + eapply OF; eauto. + + subst p; repeat split; auto using align_divides, typealign_pos. + + eapply OF; [idtac|eauto]. generalize (AL ofs ty OO) (SKK ty); omega. + + subst p; simpl. apply CSF. eapply list_nth_z_in; eauto. + + eapply OF; eauto. + - destruct H. + + subst p; repeat split; auto using align_divides, typealign_pos. + + eapply OF; [idtac|eauto]. generalize (AL ofs ty OO) (SKK ty); omega. + } + assert (C: forall va ri rf ofs f, + OKF f -> ofs >= 0 -> OK (split_long_arg va ri rf ofs f)). + { intros until f; intros OF OO; unfold split_long_arg. + set (ri' := if va then align ri 2 else ri). set (ofs' := align ofs 2). assert (OO': ofs' >= 0) by (apply (AL ofs Tlong); auto). - assert (DFL: OK (Twolong (S Outgoing (ofs' + 1) Tint) (S Outgoing ofs' Tint) - :: f rn' (ofs' + 2))). - { red; simpl; intros. destruct H. - - subst p; simpl. - repeat split; auto using Z.divide_1_l. omega. - - eapply OF; [idtac|eauto]. omega. - } - destruct (list_nth_z regs rn') as [r1|] eqn:NTH1; - destruct (list_nth_z regs (rn' + 1)) as [r2|] eqn:NTH2; - try apply DFL. - red; simpl; intros; destruct H. - - subst p; simpl. split; apply OR; eauto using list_nth_z_in. - - eapply OF; [idtac|eauto]. auto. - } - assert (C: forall regs rn ofs ty f, - OKREGS regs -> OKF f -> ofs >= 0 -> typealign ty = 1 -> OK (hybrid_arg regs rn ofs ty f)). - { intros until f; intros OR OF OO OTY; unfold hybrid_arg; red; intros. - set (rn' := align rn 2) in *. - destruct (list_nth_z regs rn') as [r|] eqn:NTH; destruct H. - - subst p; simpl. apply OR. eapply list_nth_z_in; eauto. - - eapply OF; eauto. - - subst p; simpl. rewrite OTY. split. apply (AL ofs Tlong OO). apply Z.divide_1_l. - - eapply OF; [idtac|eauto]. generalize (AL ofs Tlong OO); simpl; omega. + destruct (list_nth_z int_param_regs ri') as [r1|] eqn:NTH1; + [destruct (list_nth_z int_param_regs (ri'+1)) as [r2|] eqn:NTH2 | idtac]. + - red; simpl; intros; destruct H. + + subst p; split; apply CSI; eauto using list_nth_z_in. + + eapply OF; [idtac|eauto]. omega. + - red; simpl; intros; destruct H. + + subst p; split. split; auto using Z.divide_1_l. apply CSI; eauto using list_nth_z_in. + + eapply OF; [idtac|eauto]. omega. + - red; simpl; intros; destruct H. + + subst p; repeat split; auto using Z.divide_1_l. omega. + + eapply OF; [idtac|eauto]. omega. } - assert (D: OKREGS int_param_regs). - { red. decide_goal. } - assert (E: OKREGS float_param_regs). - { red. decide_goal. } - - cut (forall va tyl rn ofs, ofs >= 0 -> OK (loc_arguments_rec va tyl rn ofs)). + cut (forall va tyl ri rf ofs, ofs >= 0 -> OK (loc_arguments_rec va tyl ri rf ofs)). unfold OK. eauto. induction tyl as [ | ty1 tyl]; intros until ofs; intros OO; simpl. - red; simpl; tauto. - destruct ty1. + (* int *) apply A; auto. -+ (* float *) - destruct (va && negb Archi.ptr64). - apply C; auto. - apply A; auto. ++ (* float *) apply B; auto. + (* long *) destruct Archi.ptr64. apply A; auto. - apply B; auto. -+ (* single *) - apply A; auto. -+ (* any32 *) - apply A; auto. -+ (* any64 *) - destruct (va && negb Archi.ptr64). apply C; auto. - apply A; auto. ++ (* single *) apply B; auto. ++ (* any32 *) apply A; auto. ++ (* any64 *) apply B; auto. Qed. Lemma loc_arguments_acceptable: @@ -388,54 +381,14 @@ Proof. unfold loc_arguments; intros. eapply loc_arguments_rec_charact; eauto. omega. Qed. -(** The offsets of [Outgoing] arguments are below [size_arguments s]. *) - -Remark fold_max_outgoing_above: - forall l n, fold_left max_outgoing_2 l n >= n. -Proof. - assert (A: forall n l, max_outgoing_1 n l >= n). - { intros; unfold max_outgoing_1. destruct l as [_ | []]; xomega. } - induction l; simpl; intros. - - omega. - - eapply Zge_trans. eauto. - destruct a; simpl. apply A. eapply Zge_trans; eauto. -Qed. - -Lemma size_arguments_above: - forall s, size_arguments s >= 0. -Proof. - intros. apply fold_max_outgoing_above. -Qed. - -Lemma loc_arguments_bounded: - forall (s: signature) (ofs: Z) (ty: typ), - In (S Outgoing ofs ty) (regs_of_rpairs (loc_arguments s)) -> - ofs + typesize ty <= size_arguments s. -Proof. - intros until ty. - assert (A: forall n l, n <= max_outgoing_1 n l). - { intros; unfold max_outgoing_1. destruct l as [_ | []]; xomega. } - assert (B: forall p n, - In (S Outgoing ofs ty) (regs_of_rpair p) -> - ofs + typesize ty <= max_outgoing_2 n p). - { intros. destruct p; simpl in H; intuition; subst; simpl. - - xomega. - - eapply Z.le_trans. 2: apply A. xomega. - - xomega. } - assert (C: forall l n, - In (S Outgoing ofs ty) (regs_of_rpairs l) -> - ofs + typesize ty <= fold_left max_outgoing_2 l n). - { induction l; simpl; intros. - - contradiction. - - rewrite in_app_iff in H. destruct H. - + eapply Z.le_trans. eapply B; eauto. apply Z.ge_le. apply fold_max_outgoing_above. - + apply IHl; auto. - } - apply C. -Qed. - Lemma loc_arguments_main: loc_arguments signature_main = nil. Proof. reflexivity. Qed. + +(** ** Normalization of function results *) + +(** No normalization needed. *) + +Definition return_value_needs_normalization (t: rettype) := false. diff --git a/test/regression/Results/interop1 b/test/regression/Results/interop1 index 990dfe9d..6e32c1cb 100644 --- a/test/regression/Results/interop1 +++ b/test/regression/Results/interop1 @@ -1,4 +1,8 @@ --- CompCert calling native: +si8u: 177 +si8s: -79 +si16u: 64305 +si16s: -1231 s1: { a = 'a' } s2: { a = 'a', b = 'b' } s3: { a = 'a', b = 'b', c = ' c' } @@ -44,6 +48,10 @@ ru6: { a = 55555, b = 666 } ru7: { a = -10001, b = -789, c = 'z' } ru8: { a = 'x', b = 12345 } --- native calling CompCert: +si8u: 177 +si8s: -79 +si16u: 64305 +si16s: -1231 s1: { a = 'a' } s2: { a = 'a', b = 'b' } s3: { a = 'a', b = 'b', c = ' c' } diff --git a/test/regression/interop1.c b/test/regression/interop1.c index a39f449c..6836b89e 100644 --- a/test/regression/interop1.c +++ b/test/regression/interop1.c @@ -195,6 +195,17 @@ RETURN(ru6,U6,init_U6) RETURN(ru7,U7,init_U7) RETURN(ru8,U8,init_U8) +/* Returning small integers */ + +#define SMALLINT(name,ty) \ +extern ty THEM(name)(int); \ +ty US(name)(int x) { return x * x; } + +SMALLINT(si8u, unsigned char) +SMALLINT(si8s, signed char) +SMALLINT(si16u, unsigned short) +SMALLINT(si16s, signed short) + /* Test function, calling the functions compiled by the other compiler */ #define CALLPRINT(name,ty,init) \ @@ -207,6 +218,10 @@ RETURN(ru8,U8,init_U8) extern void THEM(test) (void); void US(test) (void) { + printf("si8u: %d\n", THEM(si8u)(12345)); + printf("si8s: %d\n", THEM(si8s)(12345)); + printf("si16u: %d\n", THEM(si16u)(1234567)); + printf("si16s: %d\n", THEM(si16s)(1234567)); CALLPRINT(s1,S1,init_S1) CALLPRINT(s2,S2,init_S2) CALLPRINT(s3,S3,init_S3) diff --git a/x86/Asmexpand.ml b/x86/Asmexpand.ml index 16426ce3..b8353046 100644 --- a/x86/Asmexpand.ml +++ b/x86/Asmexpand.ml @@ -251,7 +251,7 @@ let expand_builtin_va_start_32 r = invalid_arg "Fatal error: va_start used in non-vararg function"; let ofs = Int32.(add (add !PrintAsmaux.current_function_stacksize 4l) - (mul 4l (Z.to_int32 (Conventions1.size_arguments + (mul 4l (Z.to_int32 (Conventions.size_arguments (get_current_function_sig ()))))) in emit (Pleal (RAX, linear_addr RSP (Z.of_uint32 ofs))); emit (Pmovl_mr (linear_addr r _0z, RAX)) @@ -506,7 +506,7 @@ let expand_instruction instr = (* Save the registers *) emit (Pleaq (R10, linear_addr RSP (Z.of_uint save_regs))); emit (Pcall_s (intern_string "__compcert_va_saveregs", - {sig_args = []; sig_res = None; sig_cc = cc_default})) + {sig_args = []; sig_res = Tvoid; sig_cc = cc_default})) end; (* Stack chaining *) let fullsz = sz + 8 in diff --git a/x86/Builtins1.v b/x86/Builtins1.v index 6103cc4c..f1d60961 100644 --- a/x86/Builtins1.v +++ b/x86/Builtins1.v @@ -33,10 +33,10 @@ Definition platform_builtin_table : list (string * platform_builtin) := Definition platform_builtin_sig (b: platform_builtin) : signature := match b with | BI_fmin | BI_fmax => - mksignature (Tfloat :: Tfloat :: nil) (Some Tfloat) cc_default + mksignature (Tfloat :: Tfloat :: nil) Tfloat cc_default end. -Definition platform_builtin_sem (b: platform_builtin) : builtin_sem (proj_sig_res (platform_builtin_sig b)) := +Definition platform_builtin_sem (b: platform_builtin) : builtin_sem (sig_res (platform_builtin_sig b)) := match b with | BI_fmin => mkbuiltin_n2t Tfloat Tfloat Tfloat diff --git a/x86/Conventions1.v b/x86/Conventions1.v index 35d555f9..d9f5b8fa 100644 --- a/x86/Conventions1.v +++ b/x86/Conventions1.v @@ -100,22 +100,20 @@ Definition is_float_reg (r: mreg) := function with one integer result. *) Definition loc_result_32 (s: signature) : rpair mreg := - match s.(sig_res) with - | None => One AX - | Some (Tint | Tany32) => One AX - | Some (Tfloat | Tsingle) => One FP0 - | Some Tany64 => One X0 - | Some Tlong => Twolong DX AX + match proj_sig_res s with + | Tint | Tany32 => One AX + | Tfloat | Tsingle => One FP0 + | Tany64 => One X0 + | Tlong => Twolong DX AX end. (** In 64 bit mode, he result value of a function is passed back to the caller in registers [AX] or [X0]. *) Definition loc_result_64 (s: signature) : rpair mreg := - match s.(sig_res) with - | None => One AX - | Some (Tint | Tlong | Tany32 | Tany64) => One AX - | Some (Tfloat | Tsingle) => One X0 + match proj_sig_res s with + | Tint | Tlong | Tany32 | Tany64 => One AX + | Tfloat | Tsingle => One X0 end. Definition loc_result := @@ -127,8 +125,8 @@ Lemma loc_result_type: forall sig, subtype (proj_sig_res sig) (typ_rpair mreg_type (loc_result sig)) = true. Proof. - intros. unfold proj_sig_res, loc_result, loc_result_32, loc_result_64, mreg_type; - destruct Archi.ptr64; destruct (sig_res sig) as [[]|]; auto. + intros. unfold loc_result, loc_result_32, loc_result_64, mreg_type; + destruct Archi.ptr64; destruct (proj_sig_res sig); auto. Qed. (** The result locations are caller-save registers *) @@ -138,7 +136,7 @@ Lemma loc_result_caller_save: forall_rpair (fun r => is_callee_save r = false) (loc_result s). Proof. intros. unfold loc_result, loc_result_32, loc_result_64, is_callee_save; - destruct Archi.ptr64; destruct (sig_res s) as [[]|]; simpl; auto. + destruct Archi.ptr64; destruct (proj_sig_res s); simpl; auto. Qed. (** If the result is in a pair of registers, those registers are distinct and have type [Tint] at least. *) @@ -148,14 +146,14 @@ Lemma loc_result_pair: match loc_result sg with | One _ => True | Twolong r1 r2 => - r1 <> r2 /\ sg.(sig_res) = Some Tlong + r1 <> r2 /\ proj_sig_res sg = Tlong /\ subtype Tint (mreg_type r1) = true /\ subtype Tint (mreg_type r2) = true /\ Archi.ptr64 = false end. Proof. intros. unfold loc_result, loc_result_32, loc_result_64, mreg_type; - destruct Archi.ptr64; destruct (sig_res sg) as [[]|]; auto. + destruct Archi.ptr64; destruct (proj_sig_res sg); auto. split; auto. congruence. Qed. @@ -164,7 +162,7 @@ Qed. Lemma loc_result_exten: forall s1 s2, s1.(sig_res) = s2.(sig_res) -> loc_result s1 = loc_result s2. Proof. - intros. unfold loc_result, loc_result_32, loc_result_64. + intros. unfold loc_result, loc_result_32, loc_result_64, proj_sig_res. destruct Archi.ptr64; rewrite H; auto. Qed. @@ -223,36 +221,6 @@ Definition loc_arguments (s: signature) : list (rpair loc) := then loc_arguments_64 s.(sig_args) 0 0 0 else loc_arguments_32 s.(sig_args) 0. -(** [size_arguments s] returns the number of [Outgoing] slots used - to call a function with signature [s]. *) - -Fixpoint size_arguments_32 - (tyl: list typ) (ofs: Z) {struct tyl} : Z := - match tyl with - | nil => ofs - | ty :: tys => size_arguments_32 tys (ofs + typesize ty) - end. - -Fixpoint size_arguments_64 (tyl: list typ) (ir fr ofs: Z) {struct tyl} : Z := - match tyl with - | nil => ofs - | (Tint | Tlong | Tany32 | Tany64) :: tys => - match list_nth_z int_param_regs ir with - | None => size_arguments_64 tys ir fr (ofs + 2) - | Some ireg => size_arguments_64 tys (ir + 1) fr ofs - end - | (Tfloat | Tsingle) :: tys => - match list_nth_z float_param_regs fr with - | None => size_arguments_64 tys ir fr (ofs + 2) - | Some freg => size_arguments_64 tys ir (fr + 1) ofs - end - end. - -Definition size_arguments (s: signature) : Z := - if Archi.ptr64 - then size_arguments_64 s.(sig_args) 0 0 0 - else size_arguments_32 s.(sig_args) 0. - (** Argument locations are either caller-save registers or [Outgoing] stack slots at nonnegative offsets. *) @@ -354,123 +322,22 @@ Qed. Hint Resolve loc_arguments_acceptable: locs. -(** The offsets of [Outgoing] arguments are below [size_arguments s]. *) - -Remark size_arguments_32_above: - forall tyl ofs0, ofs0 <= size_arguments_32 tyl ofs0. +Lemma loc_arguments_main: + loc_arguments signature_main = nil. Proof. - induction tyl; simpl; intros. - omega. - apply Z.le_trans with (ofs0 + typesize a); auto. - generalize (typesize_pos a); omega. + unfold loc_arguments; destruct Archi.ptr64; reflexivity. Qed. -Remark size_arguments_64_above: - forall tyl ir fr ofs0, - ofs0 <= size_arguments_64 tyl ir fr ofs0. -Proof. - induction tyl; simpl; intros. - omega. - assert (A: ofs0 <= - match list_nth_z int_param_regs ir with - | Some _ => size_arguments_64 tyl (ir + 1) fr ofs0 - | None => size_arguments_64 tyl ir fr (ofs0 + 2) - end). - { destruct (list_nth_z int_param_regs ir); eauto. - apply Z.le_trans with (ofs0 + 2); auto. omega. } - assert (B: ofs0 <= - match list_nth_z float_param_regs fr with - | Some _ => size_arguments_64 tyl ir (fr + 1) ofs0 - | None => size_arguments_64 tyl ir fr (ofs0 + 2) - end). - { destruct (list_nth_z float_param_regs fr); eauto. - apply Z.le_trans with (ofs0 + 2); auto. omega. } - destruct a; auto. -Qed. +(** ** Normalization of function results *) -Lemma size_arguments_above: - forall s, size_arguments s >= 0. -Proof. - intros; unfold size_arguments. apply Z.le_ge. - destruct Archi.ptr64; [apply size_arguments_64_above|apply size_arguments_32_above]. -Qed. +(** In the x86 ABI, a return value of type "char" is returned in + register AL, leaving the top 24 bits of EAX unspecified. + Likewise, a return value of type "short" is returned in register + AH, leaving the top 16 bits of EAX unspecified. Hence, return + values of small integer types need re-normalization after calls. *) -Lemma loc_arguments_32_bounded: - forall ofs ty tyl ofs0, - In (S Outgoing ofs ty) (regs_of_rpairs (loc_arguments_32 tyl ofs0)) -> - ofs + typesize ty <= size_arguments_32 tyl ofs0. -Proof. - induction tyl as [ | t l]; simpl; intros x IN. -- contradiction. -- rewrite in_app_iff in IN; destruct IN as [IN|IN]. -+ apply Z.le_trans with (x + typesize t); [|apply size_arguments_32_above]. - Ltac decomp := - match goal with - | [ H: _ \/ _ |- _ ] => destruct H; decomp - | [ H: S _ _ _ = S _ _ _ |- _ ] => inv H - | [ H: False |- _ ] => contradiction +Definition return_value_needs_normalization (t: rettype) : bool := + match t with + | Tint8signed | Tint8unsigned | Tint16signed | Tint16unsigned => true + | _ => false end. - destruct t; simpl in IN; decomp; simpl; omega. -+ apply IHl; auto. -Qed. - -Lemma loc_arguments_64_bounded: - forall ofs ty tyl ir fr ofs0, - In (S Outgoing ofs ty) (regs_of_rpairs (loc_arguments_64 tyl ir fr ofs0)) -> - ofs + typesize ty <= size_arguments_64 tyl ir fr ofs0. -Proof. - induction tyl; simpl; intros. - contradiction. - assert (T: forall ty0, typesize ty0 <= 2). - { destruct ty0; simpl; omega. } - assert (A: forall ty0, - In (S Outgoing ofs ty) (regs_of_rpairs - match list_nth_z int_param_regs ir with - | Some ireg => - One (R ireg) :: loc_arguments_64 tyl (ir + 1) fr ofs0 - | None => One (S Outgoing ofs0 ty0) :: loc_arguments_64 tyl ir fr (ofs0 + 2) - end) -> - ofs + typesize ty <= - match list_nth_z int_param_regs ir with - | Some _ => size_arguments_64 tyl (ir + 1) fr ofs0 - | None => size_arguments_64 tyl ir fr (ofs0 + 2) - end). - { intros. destruct (list_nth_z int_param_regs ir); simpl in H0; destruct H0. - - discriminate. - - eapply IHtyl; eauto. - - inv H0. apply Z.le_trans with (ofs + 2). specialize (T ty). omega. apply size_arguments_64_above. - - eapply IHtyl; eauto. } - assert (B: forall ty0, - In (S Outgoing ofs ty) (regs_of_rpairs - match list_nth_z float_param_regs fr with - | Some ireg => - One (R ireg) :: loc_arguments_64 tyl ir (fr + 1) ofs0 - | None => One (S Outgoing ofs0 ty0) :: loc_arguments_64 tyl ir fr (ofs0 + 2) - end) -> - ofs + typesize ty <= - match list_nth_z float_param_regs fr with - | Some _ => size_arguments_64 tyl ir (fr + 1) ofs0 - | None => size_arguments_64 tyl ir fr (ofs0 + 2) - end). - { intros. destruct (list_nth_z float_param_regs fr); simpl in H0; destruct H0. - - discriminate. - - eapply IHtyl; eauto. - - inv H0. apply Z.le_trans with (ofs + 2). specialize (T ty). omega. apply size_arguments_64_above. - - eapply IHtyl; eauto. } - destruct a; eauto. -Qed. - -Lemma loc_arguments_bounded: - forall (s: signature) (ofs: Z) (ty: typ), - In (S Outgoing ofs ty) (regs_of_rpairs (loc_arguments s)) -> - ofs + typesize ty <= size_arguments s. -Proof. - unfold loc_arguments, size_arguments; intros. - destruct Archi.ptr64; eauto using loc_arguments_32_bounded, loc_arguments_64_bounded. -Qed. - -Lemma loc_arguments_main: - loc_arguments signature_main = nil. -Proof. - unfold loc_arguments; destruct Archi.ptr64; reflexivity. -Qed. |