Module val_casted

Require Import Coqlib Integers Values AST Ctypes Cop FCop Locations.

Definition val_casted_func (v : val) (ty: type) : bool :=
  match v, ty with
  | Vint n, Tint sz si attr =>
    if Int.eq_dec (cast_int_int sz si n) n then true
    else false
  | Vfloat n, Tfloat F64 attr =>
    true
  | Vsingle n, Tfloat F32 attr =>
    true
  | Vlong n, Tlong si attr =>
    true
  | Vptr b ofs, Tpointer ty attr =>
    true
  | Vint n, Tpointer ty attr =>
    negb Archi.ptr64
  | Vptr b ofs, Tint I32 si attr =>
    negb Archi.ptr64
  | Vlong n, Tpointer ty attr =>
    Archi.ptr64
  | Vptr b ofs, Tlong si attr =>
    Archi.ptr64
  | Vptr b ofs, Tstruct id attr =>
    true
  | Vptr b ofs, Tunion id attr =>
    true
  | _, Tvoid =>
    true
  | _, _ => false
  end.

Lemma val_casted_funcP:
  forall v ty,
    val_casted v ty <-> val_casted_func v ty = true.

Inductive val_casted_list: list val -> typelist -> Prop :=
  | vcl_nil:
      val_casted_list nil Tnil
  | vcl_cons: forall v1 vl ty1 tyl,
      val_casted v1 ty1 -> val_casted_list vl tyl ->
      val_casted_list (v1 :: vl) (Tcons ty1 tyl).

Lemma val_casted_list_params:
  forall params vl,
  val_casted_list vl (type_of_params params) ->
  list_forall2 val_casted vl (List.map snd params).

Fixpoint val_casted_list_func (vs : list val) (ts : typelist) : bool :=
  match vs, ts with
    | nil, Tnil => true
    | v1 :: vl, Tcons ty1 tyl =>
      val_casted_func v1 ty1 && val_casted_list_func vl tyl
    | _, _ => false
  end.


Lemma val_casted_list_funcP vs ts :
  val_casted_list_func vs ts = true <-> val_casted_list vs ts.

Lemma val_casted_inj (j : meminj) v1 v2 tv :
  Val.inject j v1 v2 ->
  val_casted v1 tv ->
  val_casted v2 tv.

Lemma val_casted_list_inj (j : meminj) vs1 vs2 ts :
  Val.inject_list j vs1 vs2 ->
  val_casted_list vs1 ts ->
  val_casted_list vs2 ts.

Definition val_has_type_func (v : val) (t : typ) : bool :=
  match v with
    | Vundef => true
    | Vint _ => match t with
                | AST.Tint => true
                | AST.Tany32 => true
                | AST.Tany64 => true
                | _ => false
                end
    | Vlong _ => match t with
                 | AST.Tlong => true
                 | AST.Tany64 => true
                 | _ => false
               end
    | Vfloat _ => match t with
                  | AST.Tfloat => true
                  | AST.Tany64 => true
                  | _ => false
                  end
    | Vsingle _ => match t with
                   | AST.Tsingle => true
                   | AST.Tany32 => true
                   | AST.Tany64 => true
                   | _ => false
                   end
    | Vptr _ _ => match t with
                  | AST.Tint => negb Archi.ptr64
                  | AST.Tany32 => negb Archi.ptr64
                  | AST.Tlong => Archi.ptr64
                  | AST.Tany64 => true
                  | _ => false
                  end
  end.

Lemma val_has_type_funcP v t :
  Val.has_type v t <-> (val_has_type_func v t=true).

Fixpoint val_has_type_list_func (vl : list val) (tyl : list typ) : bool :=
  match vl, tyl with
    | nil, nil => true
    | v :: vl', ty :: tyl' => val_has_type_func v ty
                              && val_has_type_list_func vl' tyl'
    | nil, _ :: _ => false
    | _ :: _, nil => false
  end.

Lemma val_has_type_list_func_charact vl tyl :
  Val.has_type_list vl tyl <-> (val_has_type_list_func vl tyl=true).


Fixpoint tys_nonvoid (tyl : typelist) :=
  match tyl with
    | Tnil => true
    | Tcons Tvoid tyl' => false
    | Tcons _ tyl' => tys_nonvoid tyl'
  end.

Fixpoint vals_defined (vl : list val) :=
  match vl with
    | nil => true
    | Vundef :: _ => false
    | _ :: vl' => vals_defined vl'
  end.

Lemma vals_inject_defined (vl1 vl2 : list val) (j : meminj) :
  Val.inject_list j vl1 vl2 ->
  vals_defined vl1=true ->
  vals_defined vl2=true.

Lemma valinject_hastype':
  forall (j : meminj) (v v' : val),
    Val.inject j v v' ->
    v <> Vundef ->
    forall T : typ, Val.has_type v T -> Val.has_type v' T.

Lemma val_list_inject_hastype j vl1 vl2 tys :
  Val.inject_list j vl1 vl2 ->
  vals_defined vl1=true ->
  val_has_type_list_func vl1 tys=true ->
  val_has_type_list_func vl2 tys=true.

Lemma val_list_inject_defined j vl1 vl2 :
  Val.inject_list j vl1 vl2 ->
  vals_defined vl1=true ->
  vals_defined vl2=true.



Fixpoint encode_longs (tyl : list typ) (vl : list val) :=
  match tyl with
    | nil => nil
    | AST.Tlong :: tyl' =>
      match vl with
        | nil => nil
        | Vlong n :: vl' => Vint (Int64.hiword n) :: Vint (Int64.loword n)
                            :: encode_longs tyl' vl'
        | Vundef :: vl' => Vundef :: Vundef :: encode_longs tyl' vl'
        | _ :: vl' => Vundef :: Vundef :: encode_longs tyl' vl'
      end
    | t :: tyl' =>
      match vl with
        | nil => nil
        | v :: vl' => v :: encode_longs tyl' vl'
      end
  end.

Fixpoint encode_typs (tyl : list typ) : list typ :=
  match tyl with
    | nil => nil
    | AST.Tlong :: tyl' => AST.Tint :: AST.Tint :: encode_typs tyl'
    | t :: tyl' => t :: encode_typs tyl'
  end.

Fixpoint getBlocks' (vl : list val) (b0 : block) :=
  match vl with
    | nil => false
    | Vptr b _ :: vl' => eq_block b b0 || getBlocks' vl' b0
    | _ :: vl' => getBlocks' vl' b0
  end.















Definition wd_args (args: list val) (tyl: list typ) : bool :=
  val_has_type_list_func args tyl && vals_defined args && zlt (4 * (2 * (Zlength args))) Int.max_unsigned.

Fixpoint set_arguments (ll: list (rpair loc)) (vl: list val) (ls: Locmap.t) : Locmap.t :=
  match ll, vl with
  | lp :: ll' , v :: vl' =>
    match lp with
    | AST.One l => Locmap.set l v (set_arguments ll' vl' ls)
    | AST.Twolong hi lo => Locmap.set hi (Val.hiword v) (Locmap.set lo (Val.loword v) (set_arguments ll' vl' ls))
    end
  | _, _ => ls
  end.

Definition get_result (rp: rpair mreg) (lm: Locmap.t) : val :=
  match rp with
  | AST.One r => lm (R r)
  | AST.Twolong r1 r2 => Val.longofwords (lm (R r1)) (lm (R r2))
  end.








Lemma has_type_list_tail:
  forall vl vl' tyl tyl', Val.has_type_list (vl ++ vl') (tyl ++ tyl') ->
                     length vl = length tyl ->
                     Val.has_type_list vl' tyl'.

Lemma vals_defined_tail:
  forall vl vl', vals_defined (vl ++ vl') = true -> vals_defined vl' = true.

Lemma wd_args_inject:
  forall j args args' tyl,
    Val.inject_list j args args' ->
    wd_args args tyl = true ->
    wd_args args' tyl = true.


Require Import Conventions1.
Lemma wd_args_set_arguments_get_agree:
  forall sg args locs ls,
    wd_args args (sig_args sg) = true ->
    locs = loc_arguments sg ->
    set_arguments locs args (Locmap.init Vundef) = ls ->
    forall n l, nth_error locs n = Some l ->
           exists v, nth_error args n = Some v /\
                match l with
                | AST.One l0 => ls l0 = v
                | AST.Twolong lhi llo =>
                  ls lhi = Val.hiword v /\
                  ls llo = Val.loword v
                end.

Lemma wd_args_set_arguments_eq:
  forall args sg,
    wd_args args (sig_args sg) = true ->
    args = (map (fun p => Locmap.getpair p (set_arguments (loc_arguments sg) args (Locmap.init Vundef))) (loc_arguments sg)).

Lemma locmap_set_reorder:
  forall l1 l2 v1 v2 rs, Loc.diff l1 l2 ->
                    Locmap.set l1 v1 (Locmap.set l2 v2 rs) =
                    Locmap.set l2 v2 (Locmap.set l1 v1 rs).

Lemma set_arguments_reorder:
  forall t a tyl args z0 z rs,
    z0 <= z ->
    set_arguments (loc_arguments_32 (t::nil) z0) (a::nil)
                  (set_arguments (loc_arguments_32 tyl (z + typesize t)) args rs) =
    set_arguments (loc_arguments_32 tyl (z + typesize t)) args
                  (set_arguments (loc_arguments_32 (t::nil) z0) (a::nil) rs).