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

@@ -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.

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.

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.

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.

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.