More precise neededness analysis of 64-bit integer operations

Especially the conversions between 32 and 64-bit integers.
AbsInt · Jan 31, 2025 · 12dbb42 · 12dbb42
1 parent d8b6193
commit 12dbb42
Show file tree

Hide file tree

Showing 5 changed files with 103 additions and 29 deletions.
diff --git 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
@@ -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
@@ -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,16 +160,25 @@ 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.
 - apply orl_sound; auto.
 - 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
@@ -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
@@ -71,10 +71,11 @@ Definition needs_of_operation (op: operation) (nv: nval): list nval :=
   | Ororimm n => op1 (ror nv n)
   | Oshldimm n => op1 (default nv)
   | Olea addr => needs_of_addressing addr nv
-  | Omakelong => op2 (default nv)
-  | Olowlong | Ohighlong => op1 (default nv)
-  | Ocast32signed => op1 (default nv)
-  | Ocast32unsigned => 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)
   | Onegl => op1 (modarith nv)
   | Oaddlimm _ => op1 (modarith nv)
   | Osubl => op2 (default nv)
@@ -217,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.