From 4f638e8fc778109e92cee51f508852c2e22a5352 Mon Sep 17 00:00:00 2001 From: Xavier Leroy Date: Fri, 31 Jan 2025 10:55:45 +0100 Subject: [PATCH] More precise neededness analysis of 64-bit integer operations Especially the conversions between 32 and 64-bit integers, but also: - x86: the `leal` operation - aarch64: various combined operations (extend and shift, extend and shift and add, etc). --- aarch64/NeedOp.v | 66 +++++++++++++++++++++++++++++++++++++++--------- arm/NeedOp.v | 8 ++++-- powerpc/NeedOp.v | 24 ++++++++++++++---- riscV/NeedOp.v | 20 ++++++++++----- x86/NeedOp.v | 60 ++++++++++++++++++++----------------------- 5 files changed, 120 insertions(+), 58 deletions(-) diff --git a/aarch64/NeedOp.v b/aarch64/NeedOp.v index 133c344668..a3369c0a95 100644 --- a/aarch64/NeedOp.v +++ b/aarch64/NeedOp.v @@ -34,6 +34,12 @@ Definition needs_of_shiftl (s: shift) (a: amount64) (nv: nval) := | Sror => rorl nv a end. +Definition needs_of_extend (x: extension) (a: amount64) (nv: nval) := + match x with + | Xuns32 => longofintu (shllimm nv a) + | Xsgn32 => longofint (shllimm nv a) + end. + Definition zero_ext' (s: Z) (nv: nval) := if zle 0 s then zero_ext s nv else default nv. Definition sign_ext' (s: Z) (nv: nval) := @@ -49,6 +55,8 @@ Definition op2shift (s: shift) (a: amount32) (nv: nval) := nv :: needs_of_shift s a nv :: nil. Definition op2shiftl (s: shift) (a: amount64) (nv: nval) := nv :: needs_of_shiftl s a nv :: nil. +Definition op2extl (x: extension) (a: amount64) (nv: nval) := + nv :: needs_of_extend x a nv :: nil. Definition needs_of_condition (cond: condition): list nval := nil. @@ -90,22 +98,29 @@ Definition needs_of_operation (op: operation) (nv: nval): list nval := | Ozextshr a s => op1 (shruimm (zero_ext' s nv) a) | Osextshr a s => op1 (shrimm (sign_ext' s nv) a) - | Oshiftl _ _ | Oextend _ _ => op1 (default nv) - | Omakelong | Olowlong | Ohighlong => op1 (default nv) - | Oaddl | Osubl | Omull => op2 (default nv) - | Oaddlshift _ _ | Oaddlext _ _ | Osublshift _ _ | Osublext _ _ => op2 (default nv) - | Oaddlimm _ => op1 (default nv) + | Oshiftl s a => op1shiftl s a nv + | Oextend x a => op1 (needs_of_extend x a nv) + | Omakelong => makelong_hi nv :: makelong_lo nv :: nil + | Olowlong => op1 (loword nv) + | Ohighlong => op1 (hiword nv) + | Oaddl | Omull => op2 (modarith nv) + | Osubl => op2 (default nv) + | Oaddlshift s a => op2shiftl s a (modarith nv) + | Oaddlext x a => op2extl x a (modarith nv) + | Osublshift _ _ | Osublext _ _ => op2 (default nv) + | Oaddlimm _ => op1 (modarith nv) | Onegl => op1 (modarith nv) | Oneglshift s a => op1shiftl s a (modarith nv) - | Omulladd | Omullsub => let n := default nv in n :: n :: n :: nil - | Omullhs | Omullhu | Odivl | Odivlu => op2 (default nv) - | Oandl | Oorl | Oxorl | Obicl | Oornl | Oeqvl => op2 (default nv) + | Omulladd => let n := modarith nv in n :: n :: n :: nil + | Omullsub | Omullhs | Omullhu | Odivl | Odivlu => op2 (default nv) + | Oandl | Oorl | Oxorl | Obicl | Oornl | Oeqvl => op2 (bitwise nv) | Oandlshift s a | Oorlshift s a | Oxorlshift s a => op2shiftl s a (bitwise nv) | Obiclshift s a | Oornlshift s a | Oeqvlshift s a => let n := bitwise nv in n :: needs_of_shiftl s a (bitwise n) :: nil | Oandlimm n => op1 (andlimm nv n) | Oorlimm n => op1 (orlimm nv n) - | Oxorlimm n => op1 (default nv) + | Oxorlimm n => op1 (bitwise nv) + | Onotl => op1 (bitwise nv) | Onotlshift s a => needs_of_shiftl s a (bitwise nv) :: nil | Oshll | Oshrl | Oshrlu => op2 (default nv) @@ -173,6 +188,15 @@ Proof. - apply rorl_sound; auto. Qed. +Lemma extend_sound: + forall v w ext a x, + vagree v w (needs_of_extend ext a x) -> + vagree (eval_extend ext v a) (eval_extend ext w a) x. +Proof. + unfold needs_of_extend, eval_extend; intros. + destruct ext; auto using longofint_sound, longofintu_sound, shllimm_sound. +Qed. + Lemma zero_ext'_sound: forall v w x n, vagree v w (zero_ext' n x) -> @@ -257,18 +281,36 @@ Proof. - apply shlimm_sound; apply sign_ext'_sound; auto. - apply zero_ext'_sound; apply shruimm_sound; auto. - apply sign_ext'_sound; apply shrimm_sound; auto. +- apply shiftl_sound; auto. +- apply extend_sound; auto. +- apply makelong_sound; auto. +- apply loword_sound; auto. +- apply hiword_sound; auto. +- apply addl_sound; auto. +- apply addl_sound; auto using shiftl_sound. +- apply addl_sound; auto using extend_sound. +- apply addl_sound; auto with na. - apply negl_sound; auto. - apply negl_sound; auto using shiftl_sound. +- apply mull_sound; auto. +- apply addl_sound; auto. apply mull_sound; rewrite modarith_idem; auto. +- apply andl_sound; auto. - apply andl_sound; auto using shiftl_sound. - apply andlimm_sound; auto. +- apply orl_sound; auto. - apply orl_sound; auto using shiftl_sound. - apply orlimm_sound; auto. +- apply xorl_sound; auto. - apply xorl_sound; auto using shiftl_sound. +- apply xorl_sound; auto with na. - apply notl_sound; auto. - apply notl_sound; auto using shiftl_sound. -- apply andl_sound; auto. apply notl_sound; auto using shiftl_sound. -- apply orl_sound; auto. apply notl_sound; auto using shiftl_sound. -- apply xorl_sound; auto. apply notl_sound; auto using shiftl_sound. +- apply andl_sound; auto using notl_sound. +- apply andl_sound; auto using notl_sound, shiftl_sound. +- apply orl_sound; auto using notl_sound. +- apply orl_sound; auto using notl_sound, shiftl_sound. +- apply xorl_sound; auto using notl_sound. +- apply xorl_sound; auto using notl_sound, shiftl_sound. - destruct (eval_condition cond args m) as [b|] eqn:EC. erewrite needs_of_condition_sound by eauto. apply select_sound; auto. diff --git a/arm/NeedOp.v b/arm/NeedOp.v index 23e8f04738..ae5c51fe9c 100644 --- a/arm/NeedOp.v +++ b/arm/NeedOp.v @@ -80,8 +80,9 @@ Definition needs_of_operation (op: operation) (nv: nval): list nval := | Ofloatofsingle | Osingleoffloat => op1 (default nv) | Ointoffloat | Ointuoffloat | Ofloatofint | Ofloatofintu => op1 (default nv) | Ointofsingle | Ointuofsingle | Osingleofint | Osingleofintu => op1 (default nv) - | Omakelong => op2 (default nv) - | Olowlong | Ohighlong => op1 (default nv) + | Omakelong => makelong_hi nv :: makelong_lo nv :: nil + | Olowlong => op1 (loword nv) + | Ohighlong => op1 (hiword nv) | Ocmp c => needs_of_condition c | Osel c ty => nv :: nv :: needs_of_condition c end. @@ -184,6 +185,9 @@ Proof. - apply notint_sound; auto. - apply notint_sound. apply needs_of_shift_sound; auto. - apply needs_of_shift_sound; auto. +- apply makelong_sound; auto. +- apply loword_sound; auto. +- apply hiword_sound; auto. - destruct (eval_condition c args m) as [b|] eqn:EC. erewrite needs_of_condition_sound by eauto. apply select_sound; auto. diff --git a/powerpc/NeedOp.v b/powerpc/NeedOp.v index 0d2cb16bbf..a48f8af320 100644 --- a/powerpc/NeedOp.v +++ b/powerpc/NeedOp.v @@ -52,9 +52,12 @@ Definition needs_of_operation (op: operation) (nv: nval): list nval := | Orolm amount mask => op1 (rolm nv amount mask) | Oroli amount mask => op1 (default nv) | Olongconst n => nil - | Ocast32signed | Ocast32unsigned | Onegl | Onotl => op1 (default nv) - | Oaddl | Osubl| Omullhs | Omullhu | Odivl | Odivlu | Oshll | Oshrl | Oshrlu => op2 (default nv) - | Omull => op2 (modarith nv) + | Ocast32signed => op1 (longofint nv) + | Ocast32unsigned => op1 (longofintu nv) + | Onegl => op1 (modarith nv) + | Onotl => op1 (bitwise nv) + | Oaddl | Osubl| Omull => op2 (modarith nv) + | Omullhs | Omullhu | Odivl | Odivlu | Oshll | Oshrl | Oshrlu => op2 (default nv) | Oandl | Oorl | Oxorl => op2 (bitwise nv) | Oaddlimm n => op1 (modarith nv) | Oandlimm n => op1 (andlimm nv n) @@ -70,8 +73,10 @@ Definition needs_of_operation (op: operation) (nv: nval): list nval := | Oaddfs | Osubfs | Omulfs | Odivfs => op2 (default nv) | Osingleoffloat | Ofloatofsingle => op1 (default nv) | Ointoffloat => op1 (default nv) - | Ofloatofwords | Omakelong => op2 (default nv) - | Olowlong | Ohighlong => op1 (default nv) + | Ofloatofwords => op2 (default nv) + | Omakelong => makelong_hi nv :: makelong_lo nv :: nil + | Olowlong => op1 (loword nv) + | Ohighlong => op1 (hiword nv) | Ocmp c => needs_of_condition c | Osel c ty => nv :: nv :: needs_of_condition c end. @@ -155,7 +160,12 @@ Proof. - apply or_sound; auto. apply notint_sound; rewrite bitwise_idem; auto. - apply shrimm_sound; auto. - apply rolm_sound; auto. +- apply longofint_sound; auto. +- apply longofintu_sound; auto. +- apply addl_sound; auto. - apply addl_sound; auto with na. +- apply subl_sound; auto. +- apply negl_sound; auto. - apply mull_sound; auto. - apply andl_sound; auto. - apply andlimm_sound; auto. @@ -163,8 +173,12 @@ Proof. - apply orlimm_sound; auto. - apply xorl_sound; auto. - apply xorl_sound; auto with na. +- apply notl_sound; auto. - apply shrlimm_sound; auto. - apply rolml_sound; auto. +- apply makelong_sound; auto. +- apply loword_sound; auto. +- apply hiword_sound; auto. - destruct (eval_condition c args m) as [b|] eqn:EC; simpl in H2. erewrite needs_of_condition_sound by eauto. subst v; simpl. auto with na. diff --git a/riscV/NeedOp.v b/riscV/NeedOp.v index 6b7ee1fb60..38893f4ba0 100644 --- a/riscV/NeedOp.v +++ b/riscV/NeedOp.v @@ -56,12 +56,13 @@ Definition needs_of_operation (op: operation) (nv: nval): list nval := | Oshrimm n => op1 (shrimm nv n) | Oshruimm n => op1 (shruimm nv n) | Oshrximm n => op1 (default nv) - | Omakelong => op2 (default nv) - | Olowlong | Ohighlong => op1 (default nv) - | Ocast32signed => op1 (default nv) - | Ocast32unsigned => op1 (default nv) - | Oaddl => op2 (default nv) - | Oaddlimm n => op1 (default nv) + | Omakelong => makelong_hi nv :: makelong_lo nv :: nil + | Olowlong => op1 (loword nv) + | Ohighlong => op1 (hiword nv) + | Ocast32signed => op1 (longofint nv) + | Ocast32unsigned => op1 (longofintu nv) + | Oaddl => op2 (modarith nv) + | Oaddlimm n => op1 (modarith nv) | Onegl => op1 (modarith nv) | Osubl => op2 (default nv) | Omull => op2 (modarith nv) @@ -156,6 +157,13 @@ Proof. - apply shlimm_sound; auto. - apply shrimm_sound; auto. - apply shruimm_sound; auto. +- apply makelong_sound; auto. +- apply loword_sound; auto. +- apply hiword_sound; auto. +- apply longofint_sound; auto. +- apply longofintu_sound; auto. +- apply addl_sound; auto. +- apply addl_sound; auto with na. - apply negl_sound; auto. - apply mull_sound; auto. - apply andl_sound; auto. diff --git a/x86/NeedOp.v b/x86/NeedOp.v index 82091b6e26..fddc46e5aa 100644 --- a/x86/NeedOp.v +++ b/x86/NeedOp.v @@ -25,7 +25,7 @@ Definition needs_of_condition (cond: condition): list nval := | _ => nil end. -Definition needs_of_addressing_32 (addr: addressing) (nv: nval): list nval := +Definition needs_of_addressing (addr: addressing) (nv: nval): list nval := match addr with | Aindexed n => op1 (modarith nv) | Aindexed2 n => op2 (modarith nv) @@ -37,21 +37,6 @@ Definition needs_of_addressing_32 (addr: addressing) (nv: nval): list nval := | Ainstack ofs => nil end. -Definition needs_of_addressing_64 (addr: addressing) (nv: nval): list nval := - match addr with - | Aindexed n => op1 (default nv) - | Aindexed2 n => op2 (default nv) - | Ascaled sc ofs => op1 (default nv) - | Aindexed2scaled sc ofs => op2 (default nv) - | Aglobal s ofs => nil - | Abased s ofs => op1 (default nv) - | Abasedscaled sc s ofs => op1 (default nv) - | Ainstack ofs => nil - end. - -Definition needs_of_addressing (addr: addressing) (nv: nval): list nval := - if Archi.ptr64 then needs_of_addressing_64 addr nv else needs_of_addressing_32 addr nv. - Definition needs_of_operation (op: operation) (nv: nval): list nval := match op with | Omove => op1 nv @@ -85,11 +70,12 @@ Definition needs_of_operation (op: operation) (nv: nval): list nval := | Oshruimm n => op1 (shruimm nv n) | Ororimm n => op1 (ror nv n) | Oshldimm n => op1 (default nv) - | Olea addr => needs_of_addressing_32 addr nv - | Omakelong => op2 (default nv) - | Olowlong | Ohighlong => op1 (default nv) - | Ocast32signed => op1 (default nv) - | Ocast32unsigned => op1 (default nv) + | Olea addr => needs_of_addressing addr nv + | Omakelong => makelong_hi nv :: makelong_lo nv :: nil + | Olowlong => op1 (loword nv) + | Ohighlong => op1 (hiword nv) + | Ocast32signed => op1 (longofint nv) + | Ocast32unsigned => op1 (longofintu nv) | Onegl => op1 (modarith nv) | Oaddlimm _ => op1 (modarith nv) | Osubl => op2 (default nv) @@ -111,7 +97,7 @@ Definition needs_of_operation (op: operation) (nv: nval): list nval := | Oshrlu => op2 (default nv) | Oshrluimm n => op1 (shrluimm nv n) | Ororlimm n => op1 (rorl nv n) - | Oleal addr => needs_of_addressing_64 addr nv + | Oleal addr => needs_of_addressing addr nv | Onegf | Oabsf => op1 (default nv) | Oaddf | Osubf | Omulf | Odivf | Omaxf | Ominf => op2 (default nv) | Onegfs | Oabsfs => op1 (default nv) @@ -173,28 +159,34 @@ Qed. Lemma needs_of_addressing_32_sound: forall sp addr args v nv args', eval_addressing32 ge (Vptr sp Ptrofs.zero) addr args = Some v -> - vagree_list args args' (needs_of_addressing_32 addr nv) -> + vagree_list args args' (needs_of_addressing addr nv) -> exists v', eval_addressing32 ge (Vptr sp Ptrofs.zero) addr args' = Some v' /\ vagree v v' nv. Proof. - unfold needs_of_addressing_32; intros. + unfold needs_of_addressing; intros. destruct addr; simpl in *; FuncInv; InvAgree; TrivialExists; auto using add_sound, mul_sound with na. - apply add_sound; auto with na. apply add_sound; rewrite modarith_idem; auto. - apply add_sound; auto. apply add_sound; rewrite modarith_idem; auto with na. +- apply add_sound; auto with na. apply add_sound; rewrite modarith_idem; auto. +- apply add_sound; auto. apply add_sound; rewrite modarith_idem; auto with na. apply mul_sound; rewrite modarith_idem; auto with na. Qed. -(* Lemma needs_of_addressing_64_sound: forall sp addr args v nv args', eval_addressing64 ge (Vptr sp Ptrofs.zero) addr args = Some v -> - vagree_list args args' (needs_of_addressing_64 addr nv) -> + vagree_list args args' (needs_of_addressing addr nv) -> exists v', eval_addressing64 ge (Vptr sp Ptrofs.zero) addr args' = Some v' /\ vagree v v' nv. -*) +Proof. + unfold needs_of_addressing; intros. + destruct addr; simpl in *; FuncInv; InvAgree; TrivialExists; + auto using addl_sound, mull_sound with na. +- apply addl_sound; auto with na. apply addl_sound; rewrite modarith_idem; auto. +- apply addl_sound; auto with na. apply addl_sound; auto with na. + apply mull_sound; rewrite ! modarith_idem; auto with na. +Qed. Lemma needs_of_operation_sound: forall op args v nv args', @@ -226,6 +218,11 @@ Proof. - apply shruimm_sound; auto. - apply ror_sound; auto. - eapply needs_of_addressing_32_sound; eauto. +- apply makelong_sound; auto. +- apply loword_sound; auto. +- apply hiword_sound; auto. +- apply longofint_sound; auto. +- apply longofintu_sound; auto. - apply negl_sound; auto. - apply addl_sound; auto with na. - apply mull_sound; auto. @@ -241,10 +238,7 @@ Proof. - apply shrlimm_sound; auto. - apply shrluimm_sound; auto. - apply rorl_sound; auto. -- change (eval_addressing64 ge (Vptr sp Ptrofs.zero) a args') - with (eval_operation ge (Vptr sp Ptrofs.zero) (Oleal a) args' m'). - eapply default_needs_of_operation_sound; eauto. - destruct a; simpl in H0; auto. +- eapply needs_of_addressing_64_sound; eauto. - destruct (eval_condition cond args m) as [b|] eqn:EC; simpl in H2. erewrite needs_of_condition_sound by eauto. subst v; simpl. auto with na.