Require Import String Coqlib Maps Integers Floats Errors.
Require Archi.
Require Import AST Values Memory Globalenvs Events.
Require Import Cminor Op CminorSel.
Require Import SelectOp SelectOpproof SplitLong SplitLongproof.
Require Import SelectLong SelectLongproof.


Require Import Blockset Footprint Op_fp CUAST helpers Cminor_local CminorSel_local
        selectop_proof splitlong_proof.

Local Open Scope cminorsel_scope.
Local Open Scope string_scope.

Correctness of the instruction selection functions for 64-bit operators

Section CMCONSTR.

Variable cu: cminorsel_comp_unit.
Variable hf: helper_functions.
Hypothesis HELPERS: helper_functions_declared cu hf.
Variable ge: genv.
Hypothesis GEINIT: globalenv_generic cu ge.

Variable sp: val.
Variable e: env.
Variable m: mem.

Definition unary_constructor_fp_sound (cstr: expr -> expr) : Prop :=
  forall le a x fpx v,
    eval_expr ge sp e m le a x ->
    eval_expr_fp ge sp e m le a fpx ->
    eval_expr ge sp e m le (cstr a) v ->
    exists fp, eval_expr_fp ge sp e m le (cstr a) fp /\ FP.subset fp fpx.

Definition binary_constructor_fp_sound (cstr: expr -> expr -> expr) : Prop :=
  forall le a x fpx b y fpy z,
  eval_expr ge sp e m le a x ->
  eval_expr_fp ge sp e m le a fpx ->
  eval_expr ge sp e m le b y ->
  eval_expr_fp ge sp e m le b fpy ->
  eval_expr ge sp e m le (cstr a b) z ->
  exists fp, eval_expr_fp ge sp e m le (cstr a b) fp /\ FP.subset fp (FP.union fpx fpy).

Theorem eval_longconst_fp:
  forall le n, eval_expr_fp ge sp e m le (longconst n) FP.emp.

Theorem eval_intoflong_fp: unary_constructor_fp_sound intoflong.

Theorem eval_longofintu_fp: unary_constructor_fp_sound longofintu.

Theorem eval_longofint_fp: unary_constructor_fp_sound longofint.

Theorem eval_notl_fp: unary_constructor_fp_sound notl.

Theorem eval_andlimm_fp: forall n, unary_constructor_fp_sound (andlimm n).

Theorem eval_andl_fp: binary_constructor_fp_sound andl.

Theorem eval_orlimm_fp: forall n, unary_constructor_fp_sound (orlimm n).

Theorem eval_orl_fp: binary_constructor_fp_sound orl.

Theorem eval_xorlimm_fp: forall n, unary_constructor_fp_sound (xorlimm n).

Theorem eval_xorl_fp: binary_constructor_fp_sound xorl.

Ltac trivcases:=
  repeat match goal with [ |- context[match ?x with _ => _ end] ] => destruct x end; InvEvalFP; Triv.

Theorem eval_shllimm_fp: forall n, unary_constructor_fp_sound (fun e => shllimm e n).

Theorem eval_shrluimm_fp: forall n, unary_constructor_fp_sound (fun e => shrluimm e n).

Theorem eval_shrlimm_fp: forall n, unary_constructor_fp_sound (fun e => shrlimm e n).

Theorem eval_shll_fp: binary_constructor_fp_sound shll.

Theorem eval_shrlu_fp: binary_constructor_fp_sound shrlu.

Theorem eval_shrl_fp: binary_constructor_fp_sound shrl.

Theorem eval_negl_fp: unary_constructor_fp_sound negl.

Theorem eval_addlimm_fp: forall n, unary_constructor_fp_sound (addlimm n).

Theorem eval_addl_fp: binary_constructor_fp_sound addl.

Theorem eval_subl_fp: binary_constructor_fp_sound subl.

Theorem eval_mullimm_base_fp: forall n, unary_constructor_fp_sound (mullimm_base n).

Theorem eval_mullimm_fp: forall n, unary_constructor_fp_sound (mullimm n).

Theorem eval_mull_fp: binary_constructor_fp_sound mull.

Theorem eval_mullhu_fp: forall n, unary_constructor_fp_sound (fun a => mullhu a n).

Theorem eval_mullhs_fp: forall n, unary_constructor_fp_sound (fun a => mullhs a n).

Theorem eval_shrxlimm_fp:
  forall le a n x fpx z,
  eval_expr ge sp e m le a x ->
  eval_expr_fp ge sp e m le a fpx ->
  Val.shrxl x (Vint n) = Some z ->
  exists fp, eval_expr_fp ge sp e m le (shrxlimm a n) fp /\ FP.subset fp fpx.

Ltac UseHelper := decompose [Logic.and] i64_helpers_correct; eauto.
Ltac DeclHelper := red in HELPERS; decompose [Logic.and] HELPERS; eauto.

Theorem eval_divls_base_fp: binary_constructor_fp_sound divls_base.

Theorem eval_modls_base_fp: binary_constructor_fp_sound modls_base.

Theorem eval_divlu_base_fp: binary_constructor_fp_sound divlu_base.

Theorem eval_modlu_base_fp: binary_constructor_fp_sound modlu_base.

Theorem eval_cmplu_fp:
  forall c le a x fpx b y fpy v fp,
  eval_expr ge sp e m le a x ->
  eval_expr_fp ge sp e m le a fpx ->
  eval_expr ge sp e m le b y ->
  eval_expr_fp ge sp e m le b fpy ->
  Val.cmplu (Mem.valid_pointer m) c x y = Some v ->
  ValFP.cmplu_bool_fp m c x y = Some fp ->
  exists fp', eval_expr_fp ge sp e m le (cmplu c a b) fp' /\ FP.subset fp' (FP.union (FP.union fpx fpy) fp).

Theorem eval_cmpl_fp:
  forall c le a x fpx b y fpy v,
  eval_expr ge sp e m le a x ->
  eval_expr_fp ge sp e m le a fpx ->
  eval_expr ge sp e m le b y ->
  eval_expr_fp ge sp e m le b fpy ->
  Val.cmpl c x y = Some v ->
  exists fp', eval_expr_fp ge sp e m le (cmpl c a b) fp' /\ FP.subset fp' (FP.union fpx fpy).

Ltac findhelper:= DeclHelper;
                  match goal with
                  | [H: context[Genv.find_symbol _ ?id],
                        H1: (helper_declared _ ?id _ _ ),
                            H2: context[Genv.find_funct_ptr _ _] |- _ ] =>
                    let b := fresh in
                    let A := fresh in
                    let B := fresh in
                    eapply find_def_symbol in H1; eauto; destruct H1 as [b [A B]];
                    unfold fundef, Genv.find_funct_ptr in *; simpl in *;
                    rewrite H in A; inv A; rewrite B in H2; inv H2
                  end.

Theorem eval_longoffloat_fp: unary_constructor_fp_sound longoffloat.

Theorem eval_floatoflong_fp: unary_constructor_fp_sound floatoflong.

Theorem eval_longofsingle_fp: unary_constructor_fp_sound longofsingle.

Theorem eval_singleoflong_fp: unary_constructor_fp_sound singleoflong.

End CMCONSTR.