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

Local Open Scope cminorsel_scope.
Local Open Scope string_scope.

Properties of the helper functions

Correctness of the instruction selection functions for 64-bit operators

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.

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

Lemma eval_helper:
  forall bf le id name sg args vargs vres,
  eval_exprlist ge sp e m le args vargs ->
  helper_declared prog id name sg ->
  lookup_builtin_function name sg = Some bf ->
  builtin_function_sem bf vargs = Some vres ->
  eval_expr ge sp e m le (Eexternal (QualIdent.root id) sg args) vres.

Corollary eval_helper_1:
  forall bf le id name sg arg1 varg1 vres,
  eval_expr ge sp e m le arg1 varg1 ->
  helper_declared prog id name sg ->
  lookup_builtin_function name sg = Some bf ->
  builtin_function_sem bf (varg1 :: nil) = Some vres ->
  eval_expr ge sp e m le (Eexternal (QualIdent.root id) sg (arg1 ::: Enil)) vres.

Corollary eval_helper_2:
  forall bf le id name sg arg1 arg2 varg1 varg2 vres,
  eval_expr ge sp e m le arg1 varg1 ->
  eval_expr ge sp e m le arg2 varg2 ->
  helper_declared prog id name sg ->
  lookup_builtin_function name sg = Some bf ->
  builtin_function_sem bf (varg1 :: varg2 :: nil) = Some vres ->
  eval_expr ge sp e m le (Eexternal (QualIdent.root id) sg (arg1 ::: arg2 ::: Enil)) vres.

Remark eval_builtin_1:
  forall bf le id sg arg1 varg1 vres,
  eval_expr ge sp e m le arg1 varg1 ->
  lookup_builtin_function id sg = Some bf ->
  builtin_function_sem bf (varg1 :: nil) = Some vres ->
  eval_expr ge sp e m le (Ebuiltin (EF_builtin id sg) (arg1 ::: Enil)) vres.

Remark eval_builtin_2:
  forall bf le id sg arg1 arg2 varg1 varg2 vres,
  eval_expr ge sp e m le arg1 varg1 ->
  eval_expr ge sp e m le arg2 varg2 ->
  lookup_builtin_function id sg = Some bf ->
  builtin_function_sem bf (varg1 :: varg2 :: nil) = Some vres ->
  eval_expr ge sp e m le (Ebuiltin (EF_builtin id sg) (arg1 ::: arg2 ::: Enil)) vres.

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

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.

Ltac EvalOp :=
  eauto;
  match goal with
  | [ |- eval_exprlist _ _ _ _ _ Enil _ ] => constructor
  | [ |- eval_exprlist _ _ _ _ _ (_:::_) _ ] => econstructor; EvalOp
  | [ |- eval_expr _ _ _ _ _ (Eletvar _) _ ] => constructor; simpl; eauto
  | [ |- eval_expr _ _ _ _ _ (Elet _ _) _ ] => econstructor; EvalOp
  | [ |- eval_expr _ _ _ _ _ (lift _) _ ] => apply eval_lift; EvalOp
  | [ |- eval_expr _ _ _ _ _ _ _ ] => eapply eval_Eop; [EvalOp | simpl; eauto]
  | _ => idtac
  end.

Lemma eval_splitlong:
  forall le a f v sem,
  (forall le a b x 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 (f a b) v /\
             (forall p q, x = Vint p -> y = Vint q -> v = sem (Vlong (Int64.ofwords p q)))) ->
  match v with Vlong _ => True | _ => sem v = Vundef end ->
  eval_expr ge sp e m le a v ->
  exists v', eval_expr ge sp e m le (splitlong a f) v' /\ Val.lessdef (sem v) v'.

Lemma eval_splitlong_strict:
  forall le a f va v,
  eval_expr ge sp e m le a (Vlong va) ->
  (forall le a1 a2,
     eval_expr ge sp e m le a1 (Vint (Int64.hiword va)) ->
     eval_expr ge sp e m le a2 (Vint (Int64.loword va)) ->
     eval_expr ge sp e m le (f a1 a2) v) ->
  eval_expr ge sp e m le (splitlong a f) v.

Lemma eval_splitlong2:
  forall le a b f va vb sem,
  (forall le a1 a2 b1 b2 x1 x2 y1 y2,
   eval_expr ge sp e m le a1 x1 ->
   eval_expr ge sp e m le a2 x2 ->
   eval_expr ge sp e m le b1 y1 ->
   eval_expr ge sp e m le b2 y2 ->
   exists v,
     eval_expr ge sp e m le (f a1 a2 b1 b2) v /\
     (forall p1 p2 q1 q2,
       x1 = Vint p1 -> x2 = Vint p2 -> y1 = Vint q1 -> y2 = Vint q2 ->
       v = sem (Vlong (Int64.ofwords p1 p2)) (Vlong (Int64.ofwords q1 q2)))) ->
  match va, vb with Vlong _, Vlong _ => True | _, _ => sem va vb = Vundef end ->
  eval_expr ge sp e m le a va ->
  eval_expr ge sp e m le b vb ->
  exists v, eval_expr ge sp e m le (splitlong2 a b f) v /\ Val.lessdef (sem va vb) v.

Lemma eval_splitlong2_strict:
  forall le a b f va vb v,
  eval_expr ge sp e m le a (Vlong va) ->
  eval_expr ge sp e m le b (Vlong vb) ->
  (forall le a1 a2 b1 b2,
     eval_expr ge sp e m le a1 (Vint (Int64.hiword va)) ->
     eval_expr ge sp e m le a2 (Vint (Int64.loword va)) ->
     eval_expr ge sp e m le b1 (Vint (Int64.hiword vb)) ->
     eval_expr ge sp e m le b2 (Vint (Int64.loword vb)) ->
     eval_expr ge sp e m le (f a1 a2 b1 b2) v) ->
  eval_expr ge sp e m le (splitlong2 a b f) v.

Lemma is_longconst_sound:
  forall le a x n,
  is_longconst a = Some n ->
  eval_expr ge sp e m le a x ->
  x = Vlong n.

Lemma is_longconst_zero_sound:
  forall le a x,
  is_longconst_zero a = true ->
  eval_expr ge sp e m le a x ->
  x = Vlong Int64.zero.

Lemma eval_lowlong: unary_constructor_sound lowlong Val.loword.

Lemma eval_highlong: unary_constructor_sound highlong Val.hiword.

Lemma eval_longconst:
  forall le n, eval_expr ge sp e m le (longconst n) (Vlong n).

Theorem eval_intoflong: unary_constructor_sound intoflong Val.loword.
Proof eval_lowlong.

Theorem eval_longofintu: unary_constructor_sound longofintu Val.longofintu.

Theorem eval_longofint: unary_constructor_sound longofint Val.longofint.

Theorem eval_negl: unary_constructor_sound negl Val.negl.

Theorem eval_notl: unary_constructor_sound notl Val.notl.

Theorem eval_longoffloat:
  forall le a x y,
  eval_expr ge sp e m le a x ->
  Val.longoffloat x = Some y ->
  exists v, eval_expr ge sp e m le (longoffloat a) v /\ Val.lessdef y v.

Theorem eval_longuoffloat:
  forall le a x y,
  eval_expr ge sp e m le a x ->
  Val.longuoffloat x = Some y ->
  exists v, eval_expr ge sp e m le (longuoffloat a) v /\ Val.lessdef y v.

Theorem eval_floatoflong:
  forall le a x y,
  eval_expr ge sp e m le a x ->
  Val.floatoflong x = Some y ->
  exists v, eval_expr ge sp e m le (floatoflong a) v /\ Val.lessdef y v.

Theorem eval_floatoflongu:
  forall le a x y,
  eval_expr ge sp e m le a x ->
  Val.floatoflongu x = Some y ->
  exists v, eval_expr ge sp e m le (floatoflongu a) v /\ Val.lessdef y v.

Theorem eval_longofsingle:
  forall le a x y,
  eval_expr ge sp e m le a x ->
  Val.longofsingle x = Some y ->
  exists v, eval_expr ge sp e m le (longofsingle a) v /\ Val.lessdef y v.

Theorem eval_longuofsingle:
  forall le a x y,
  eval_expr ge sp e m le a x ->
  Val.longuofsingle x = Some y ->
  exists v, eval_expr ge sp e m le (longuofsingle a) v /\ Val.lessdef y v.

Theorem eval_singleoflong:
  forall le a x y,
  eval_expr ge sp e m le a x ->
  Val.singleoflong x = Some y ->
  exists v, eval_expr ge sp e m le (singleoflong a) v /\ Val.lessdef y v.

Theorem eval_singleoflongu:
  forall le a x y,
  eval_expr ge sp e m le a x ->
  Val.singleoflongu x = Some y ->
  exists v, eval_expr ge sp e m le (singleoflongu a) v /\ Val.lessdef y v.

Theorem eval_andl: binary_constructor_sound andl Val.andl.

Theorem eval_orl: binary_constructor_sound orl Val.orl.

Theorem eval_xorl: binary_constructor_sound xorl Val.xorl.

Lemma is_intconst_sound:
  forall le a x n,
  is_intconst a = Some n ->
  eval_expr ge sp e m le a x ->
  x = Vint n.

Remark eval_shift_imm:
  forall (P: expr -> Prop) n a0 a1 a2 a3,
  (n = Int.zero -> P a0) ->
  (0 <= Int.unsigned n < Int.zwordsize ->
   Int.ltu n Int.iwordsize = true ->
   Int.ltu (Int.sub Int.iwordsize n) Int.iwordsize = true ->
   Int.ltu n Int64.iwordsize' = true ->
   P a1) ->
  (Int.zwordsize <= Int.unsigned n < Int64.zwordsize ->
   Int.ltu (Int.sub n Int.iwordsize) Int.iwordsize = true ->
   P a2) ->
  P a3 ->
  P (if Int.eq n Int.zero then a0
     else if Int.ltu n Int.iwordsize then a1
     else if Int.ltu n Int64.iwordsize' then a2
     else a3).

Lemma eval_shllimm:
  forall n,
  unary_constructor_sound (fun e => shllimm e n) (fun v => Val.shll v (Vint n)).

Theorem eval_shll: binary_constructor_sound shll Val.shll.

Lemma eval_shrluimm:
  forall n,
  unary_constructor_sound (fun e => shrluimm e n) (fun v => Val.shrlu v (Vint n)).

Theorem eval_shrlu: binary_constructor_sound shrlu Val.shrlu.

Lemma eval_shrlimm:
  forall n,
  unary_constructor_sound (fun e => shrlimm e n) (fun v => Val.shrl v (Vint n)).

Theorem eval_shrl: binary_constructor_sound shrl Val.shrl.

Theorem eval_addl: Archi.ptr64 = false -> binary_constructor_sound addl Val.addl.

Theorem eval_subl: Archi.ptr64 = false -> binary_constructor_sound subl Val.subl.

Lemma eval_mull_base: binary_constructor_sound mull_base Val.mull.

Lemma eval_mullimm:
  forall n, unary_constructor_sound (mullimm n) (fun v => Val.mull v (Vlong n)).

Theorem eval_mull: binary_constructor_sound mull Val.mull.

Theorem eval_mullhu:
  forall n, unary_constructor_sound (fun a => mullhu a n) (fun v => Val.mullhu v (Vlong n)).

Theorem eval_mullhs:
  forall n, unary_constructor_sound (fun a => mullhs a n) (fun v => Val.mullhs v (Vlong n)).

Theorem eval_shrxlimm:
  forall le a n x z,
  Archi.ptr64 = false ->
  eval_expr ge sp e m le a x ->
  Val.shrxl x (Vint n) = Some z ->
  exists v, eval_expr ge sp e m le (shrxlimm a n) v /\ Val.lessdef z v.

Theorem eval_divlu_base:
  forall le a b x y z,
  eval_expr ge sp e m le a x ->
  eval_expr ge sp e m le b y ->
  Val.divlu x y = Some z ->
  exists v, eval_expr ge sp e m le (divlu_base a b) v /\ Val.lessdef z v.

Theorem eval_modlu_base:
  forall le a b x y z,
  eval_expr ge sp e m le a x ->
  eval_expr ge sp e m le b y ->
  Val.modlu x y = Some z ->
  exists v, eval_expr ge sp e m le (modlu_base a b) v /\ Val.lessdef z v.

Theorem eval_divls_base:
  forall le a b x y z,
  eval_expr ge sp e m le a x ->
  eval_expr ge sp e m le b y ->
  Val.divls x y = Some z ->
  exists v, eval_expr ge sp e m le (divls_base a b) v /\ Val.lessdef z v.

Theorem eval_modls_base:
  forall le a b x y z,
  eval_expr ge sp e m le a x ->
  eval_expr ge sp e m le b y ->
  Val.modls x y = Some z ->
  exists v, eval_expr ge sp e m le (modls_base a b) v /\ Val.lessdef z v.

Remark decompose_cmpl_eq_zero:
  forall h l,
  Int64.eq (Int64.ofwords h l) Int64.zero = Int.eq (Int.or h l) Int.zero.

Lemma eval_cmpl_eq_zero:
  forall le a x,
  eval_expr ge sp e m le a (Vlong x) ->
  eval_expr ge sp e m le (cmpl_eq_zero a) (Val.of_bool (Int64.eq x Int64.zero)).

Lemma eval_cmpl_ne_zero:
  forall le a x,
  eval_expr ge sp e m le a (Vlong x) ->
  eval_expr ge sp e m le (cmpl_ne_zero a) (Val.of_bool (negb (Int64.eq x Int64.zero))).

Lemma eval_cmplu_gen:
  forall ch cl a b le x y,
  eval_expr ge sp e m le a (Vlong x) ->
  eval_expr ge sp e m le b (Vlong y) ->
  eval_expr ge sp e m le (cmplu_gen ch cl a b)
    (Val.of_bool (if Int.eq (Int64.hiword x) (Int64.hiword y)
                  then Int.cmpu cl (Int64.loword x) (Int64.loword y)
                  else Int.cmpu ch (Int64.hiword x) (Int64.hiword y))).

Remark int64_eq_xor:
  forall p q, Int64.eq p q = Int64.eq (Int64.xor p q) Int64.zero.

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.

Lemma eval_cmpl_gen:
  forall ch cl a b le x y,
  eval_expr ge sp e m le a (Vlong x) ->
  eval_expr ge sp e m le b (Vlong y) ->
  eval_expr ge sp e m le (cmpl_gen ch cl a b)
    (Val.of_bool (if Int.eq (Int64.hiword x) (Int64.hiword y)
                  then Int.cmpu cl (Int64.loword x) (Int64.loword y)
                  else Int.cmp ch (Int64.hiword x) (Int64.hiword y))).

Remark decompose_cmpl_lt_zero:
  forall h l,
  Int64.lt (Int64.ofwords h l) Int64.zero = Int.lt h Int.zero.

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.

End CMCONSTR.