Module SelectLongproof


Instruction selection for 64-bit integer operations

From Coq Require Import String.
Require Import Coqlib Maps Integers Floats Errors.
Require Archi.
Require Import AST Values Memory Globalenvs Builtins Events.
Require Import Cminor Op CminorSel.
Require Import OpHelpers OpHelpersproof.
Require Import SelectOp SelectOpproof SplitLong SplitLongproof.
Require Import SelectLong.

Local Open Scope cminorsel_scope.
Local Open Scope string_scope.

Section CMCONSTR.

Variable prog: program.
Variable hf: helper_functions.
Hypothesis HELPERS: helper_functions_declared prog hf.
Let ge := Genv.globalenv prog.
Variable sp: val.
Variable e: env.
Variable m: mem.

Definition binary_constructor_sound (cstr: expr -> expr -> expr) (sem: val -> val -> val) : Prop :=
  forall le a x b y,
  eval_expr ge sp e m le a x ->
  eval_expr ge sp e m le b y ->
  exists v, eval_expr ge sp e m le (cstr a b) v /\ Val.lessdef (sem x y) v.

Semantic equivalence between Val.longofwords (Val.shr v 31) v and Val.longofint v. Borrowed from SplitLongproof.eval_longofint.
Lemma val_longofwords_shr31_eq:
  forall v, Val.longofwords (Val.shr v (Vint (Int.repr 31))) v = Val.longofint v.
Proof.
  intros. destruct v; cbn; auto.
  change (Int.ltu (Int.repr 31) Int.iwordsize) with true. cbn.
  f_equal.
  apply Int64.same_bits_eq; intros.
  rewrite Int64.testbit_repr by auto.
  rewrite Int64.bits_ofwords by auto.
  rewrite Int.bits_signed by lia.
  destruct (zlt i0 Int.zwordsize); auto.
  assert (Int64.zwordsize = 2 * Int.zwordsize) by reflexivity.
  rewrite Int.bits_shr by lia.
  change (Int.unsigned (Int.repr 31)) with (Int.zwordsize - 1).
  f_equal. destruct (zlt (i0 - Int.zwordsize + (Int.zwordsize - 1)) Int.zwordsize); lia.
Qed.

If is_longofint_signed e = Some a and eval_expr e v, then v = Val.longofint va for some va which a evaluates to.
Lemma is_longofint_signed_correct:
  forall le e' a v,
  is_longofint_signed e' = Some a ->
  eval_expr ge sp e m le e' v ->
  exists va, eval_expr ge sp e m le a va /\ v = Val.longofint va.
Proof.
  intros le e' a v HS HE.
  unfold is_longofint_signed in HS.
  destruct e' as [i|op args|chk addr al|c b1 b2|a' body|n|ef al|id sg al]; try discriminate.
  destruct body as [i|op args|chk addr al|c b1 b2|a'' body'|n|ef al|id sg al]; try discriminate.
  destruct op; try discriminate.
  destruct args as [|h tl]; try discriminate.
  destruct h as [i|opH argsH|chk addr al|c b1 b2|a'' body'|n|ef al|id sg al]; try discriminate.
  destruct opH; try discriminate.
  destruct s as [s|s|s|s]; try discriminate.
  destruct argsH as [|hh ttl]; try discriminate.
  destruct hh as [i|op args|chk addr al|c b1 b2|a'' body'|n|ef al|id sg al]; try discriminate.
  destruct n; try discriminate.
  destruct ttl; try discriminate.
  destruct tl as [|ll lll]; try discriminate.
  destruct ll as [i|op args|chk addr al|c b1 b2|a'' body'|n|ef al|id sg al]; try discriminate.
  destruct n; try discriminate.
  destruct lll; try discriminate.
  destruct (Int.eq (s_amount s) (Int.repr 31)) eqn:HC; try discriminate.
  inv HS.
  inv HE.
  match goal with
  | [ H : eval_expr _ _ _ _ _ a ?v1 |- _ ] =>
      exists v1; split; [exact H|];
      match goal with
      | [ H' : eval_expr _ _ _ _ (v1 :: le) _ v |- _ ] => inv H'
      end
  end.
  repeat match goal with
  | [ H : eval_exprlist _ _ _ _ _ Enil _ |- _ ] => inv H
  | [ H : eval_exprlist _ _ _ _ _ (_ ::: _) _ |- _ ] => inv H
  | [ H : eval_expr _ _ _ _ _ (Eop _ _) _ |- _ ] => inv H
  | [ H : eval_expr _ _ _ _ _ (Eletvar _) _ |- _ ] => inv H
  end.
  cbn in *.
  repeat match goal with
  | [ H : Some _ = Some _ |- _ ] => inv H
  end.
  generalize (Int.eq_spec (s_amount s) (Int.repr 31)); rewrite HC; intros HEQ.
  destruct s as [sa pf]. cbn in HEQ. subst sa.
  rewrite <- val_longofwords_shr31_eq.
  cbn. reflexivity.
Qed.

Theorem eval_mull: binary_constructor_sound mull Val.mull.
Proof.
  red; intros le ea x eb y Ha Hb.
  unfold mull.
  destruct (is_longofint_signed ea) as [a|] eqn:WS1; cycle 1.
  { eapply SplitLongproof.eval_mull; eauto. }
  destruct (is_longofint_signed eb) as [b|] eqn:WS2; cycle 1.
  { eapply SplitLongproof.eval_mull; eauto. }
  exploit is_longofint_signed_correct. exact WS1. exact Ha.
  intros [va [Eva HXa]].
  exploit is_longofint_signed_correct. exact WS2. exact Hb.
  intros [vb [Evb HXb]].
  subst x. subst y.
  exists (Val.mull (Val.longofint va) (Val.longofint vb)); split.
  - eapply SplitLongproof.eval_builtin_2.
    + exact Eva.
    + exact Evb.
    + reflexivity.
    + reflexivity.
  - apply Val.lessdef_refl.
Qed.

End CMCONSTR.

Soundness of the cmplu/cmpl overrides for ordered comparisons. The override is a syntactic rewrite from SplitLong's Econdition-tree to a single Eop (Ocmpcarryu c)/Eop (Ocmpcarry c) node with the four split halves; the eval semantics of Ocmpcarryu/Ocmpcarry in arm/Op.v is defined to return the same value as SplitLong's tree. Stated in a separate section without the HELPERS hypothesis so that the proof terms do not silently generalize over helper_functions_declared — that would change their type signatures in a way that breaks Selectionproof's eapply eval_cmpl / eapply eval_cmplu.

Section CMPL_VIA_CARRY.

Variable prog: program.
Let ge := Genv.globalenv prog.
Variable sp: val.
Variable e: env.
Variable m: mem.

Theorem eval_cmplu_via_carry:
  forall c le a x b y v,
  eval_expr ge sp e m le a x ->
  eval_expr ge sp e m le b y ->
  Val.cmplu (Mem.valid_pointer m) c x y = Some v ->
  Archi.ptr64 = false ->
  eval_expr ge sp e m le (cmplu_via_carry c a b) v.
Proof.
  intros c le a x b y v Ha Hb HC HP.
  unfold Val.cmplu in HC.
  destruct (Val.cmplu_bool (Mem.valid_pointer m) c x y) as [bb|] eqn:CMP;
    cbn in HC; try discriminate.
  inv HC.
  (* From Archi.ptr64 = false and CMP = Some, the only possibility is x=Vlong, y=Vlong *)
  destruct x; cbn in CMP; try discriminate;
    destruct y; cbn in CMP; try discriminate;
    try (rewrite HP in CMP; cbn in CMP; discriminate).
  inv CMP.
  exploit (SplitLongproof.eval_highlong prog sp e m). eexact Ha. intros (vhi & Ahi & Bhi).
  exploit (SplitLongproof.eval_lowlong prog sp e m). eexact Ha. intros (vlo & Alo & Blo).
  exploit (SplitLongproof.eval_highlong prog sp e m). eexact Hb. intros (vhi' & Ahi' & Blo').
  exploit (SplitLongproof.eval_lowlong prog sp e m). eexact Hb. intros (vlo' & Alo' & Bhi').
  cbn in Bhi, Blo, Blo', Bhi'.
  unfold cmplu_via_carry.
  econstructor.
  - econstructor. exact Ahi. econstructor. exact Alo.
    econstructor. exact Ahi'. econstructor. exact Alo'.
    constructor.
  - cbn. inv Bhi. inv Blo. inv Bhi'. inv Blo'.
    cbn. rewrite Int64.ofwords_recompose. rewrite Int64.ofwords_recompose. reflexivity.
Qed.

Theorem eval_cmpl_via_carry:
  forall c le a x b y v,
  eval_expr ge sp e m le a x ->
  eval_expr ge sp e m le b y ->
  Val.cmpl c x y = Some v ->
  eval_expr ge sp e m le (cmpl_via_carry c a b) v.
Proof.
  intros c le a x b y v Ha Hb HC.
  unfold Val.cmpl in HC.
  destruct (Val.cmpl_bool c x y) as [bb|] eqn:CMP; cbn in HC; try discriminate.
  inv HC.
  destruct x; cbn in CMP; try discriminate;
    destruct y; cbn in CMP; try discriminate.
  inv CMP.
  exploit (SplitLongproof.eval_highlong prog sp e m). eexact Ha. intros (vhi & Ahi & Bhi).
  exploit (SplitLongproof.eval_lowlong prog sp e m). eexact Ha. intros (vlo & Alo & Blo).
  exploit (SplitLongproof.eval_highlong prog sp e m). eexact Hb. intros (vhi' & Ahi' & Blo').
  exploit (SplitLongproof.eval_lowlong prog sp e m). eexact Hb. intros (vlo' & Alo' & Bhi').
  cbn in Bhi, Blo, Blo', Bhi'.
  unfold cmpl_via_carry.
  econstructor.
  - econstructor. exact Ahi. econstructor. exact Alo.
    econstructor. exact Ahi'. econstructor. exact Alo'.
    constructor.
  - cbn. inv Bhi. inv Blo. inv Bhi'. inv Blo'.
    cbn. rewrite Int64.ofwords_recompose. rewrite Int64.ofwords_recompose. reflexivity.
Qed.

Top-level cmplu/cmpl correctness — dispatches according to c.
Theorem eval_cmplu:
  forall c le a x b y v,
  eval_expr ge sp e m le a x ->
  eval_expr ge sp e m le b y ->
  Val.cmplu (Mem.valid_pointer m) c x y = Some v ->
  Archi.ptr64 = false ->
  eval_expr ge sp e m le (cmplu c a b) v.
Proof.
  intros. unfold cmplu.
  destruct c;
    try (eapply SplitLongproof.eval_cmplu; eauto);
    eapply eval_cmplu_via_carry; eauto.
Qed.

Theorem eval_cmpl:
  forall c le a x b y v,
  eval_expr ge sp e m le a x ->
  eval_expr ge sp e m le b y ->
  Val.cmpl c x y = Some v ->
  eval_expr ge sp e m le (cmpl c a b) v.
Proof.
  intros. unfold cmpl.
  destruct c;
    try (eapply SplitLongproof.eval_cmpl; eauto);
    eapply eval_cmpl_via_carry; eauto.
Qed.

End CMPL_VIA_CARRY.
Generated by coq2html