Module ZIntervalAnalysis

Require Import Coqlib ZArith.
Require Import AnalysisDomain.
Require Import ZIntervalDomain ZIntervalAOp.
Require Import Linking AST Op Registers Builtins.
Require Import Values Memory Integers Globalenvs Events.
Require List.


Definition areg (ae: aenv) (r: reg) : ival := AE.get r ae.
Definition aregs (ae: aenv) (rl: list reg) : list ival := List.map (areg ae) rl.

Lemma areg_sound:
  forall e ae r, ematch e ae -> vmatch (e#r) (areg ae r).

Lemma aregs_sound:
  forall e ae rl, ematch e ae -> list_forall2 vmatch (e##rl) (aregs ae rl).

Fixpoint ae_set_multiple (regs : list reg) (avals : list ival) (ae : aenv): aenv :=
  match regs, avals with
  | (r::regs0), (av::avals0) =>
      ae_set_multiple regs0 avals0 (AE.set r av ae)
  | nil, _ | _, nil => ae
  end.

Lemma ematch_restrict:
  forall e ae (av : ival) r
         (VMATCH : vmatch (e # r) av)
         (EMATCH : ematch e ae),
    ematch e (AE.set r av ae).

Lemma ematch_restrict_multiple:
  forall regs avals e ae
         (ARG_MATCH : list_forall2 vmatch (e ## regs) avals)
         (EMATCH : ematch e ae),
    (ematch e (ae_set_multiple regs avals ae)).


Module ZIntervalAADomain(IR : IRspec) <: AADomain IR.
  Module VA := Interval_Analysis.
  
  Definition astate : Type := AE.t.
  Definition Astate : astate -> VA.t := Some.
  Definition filter_astate (s : VA.t) : option astate := s.
  Lemma filter_astate_bot: filter_astate VA.bot = None.
  Lemma filter_iff_Astate s s': filter_astate s = Some s' <-> s = Astate s'.
  Lemma filter_ge s s' (GE : VA.ge s s') (BOT : filter_astate s = None): filter_astate s' = None.

  Definition default_top : VA.t := Some AE.top.
  Lemma ge_default_top s': VA.ge default_top s'.

  Definition entry_state (f : IR.function) : VA.t :=
    Some (einit_regs (IR.fn_params f)).

  Definition prog_info := unit.
  Definition get_prog_info (p : program (fundef IR.function) unit): prog_info := tt.
  
  Local Hint Resolve areg_sound aregs_sound : ival.
  

  Definition transfer_op (_ : prog_info) (op : operation) (args : list reg) (res : reg)
                         (ae : astate): VA.t :=
    let a := eval_static_operation op (aregs ae args) in
    Some (AE.set res a ae).

  Program Definition uint32_full_range := Int_Modulus_Interval.mkmod_interval (Interval.mkinterval 0 4294967295 _) _ _.
  Program Definition uint16_full_range := Int_Modulus_Interval.mkmod_interval (Interval.mkinterval 0 65535 _) _ _.
  Program Definition uint8_full_range := Int_Modulus_Interval.mkmod_interval (Interval.mkinterval 0 255 _) _ _.

  Definition transfer_load (_ : prog_info) (trap : trapping_mode) (chk : memory_chunk) (addr : addressing)
             (args : list reg) (res : reg) (ae : astate): VA.t :=
    let itv :=
      match chk with
      | Mint32 => if Archi.ptr64 then Iint true uint32_full_range else Itop
      | Mint16unsigned => Iint true uint16_full_range
      | Mint8unsigned => Iint true uint8_full_range
      | _ => Itop
      end in
    Some (AE.set res itv ae).

  Definition transfer_store (_ : prog_info) (chk : memory_chunk) (addr : addressing) (args : list reg)
                            (src : reg) (ae : astate): VA.t :=
    Some ae.

  Definition filter_condition (cond: condition) (regs: list reg) (ae : aenv) : aenv :=
    ae_set_multiple regs (filter_static_condition cond (aregs ae regs)) ae.

  Definition transfer_condition (_ : prog_info) (cond : condition) (args : list reg) (ae : astate): VA.t * VA.t :=
    match eval_static_condition cond (aregs ae args) with
    | Bnone => (None, None)
    | Just true => (Some ae, None)
    | Just false => (None, Some ae)
    | Btop | Any_bool =>
        (Some (filter_condition cond args ae),
         Some (filter_condition (negate_condition cond) args ae))
    end.

  Definition transfer_call (_ : prog_info) (args : list reg) (res : reg) (ae : astate): VA.t :=
      Some (AE.set res Itop ae).

  Fixpoint abuiltin_arg (ae: aenv) (ba: builtin_arg reg) : ival :=
    match ba with
    | BA r => areg ae r
    | BA_int n => intconst n
    | BA_long n => longconst n
    | BA_float _
    | BA_single _
    | BA_loadstack _ _
    | BA_addrstack _
    | BA_loadglobal _ _ _
    | BA_addrglobal _ _ => Itop
    | BA_splitlong hi lo => longofwords (abuiltin_arg ae hi) (abuiltin_arg ae lo)
    | BA_addptr ba1 ba2 =>
        let v1 := abuiltin_arg ae ba1 in
        let v2 := abuiltin_arg ae ba2 in
        if Archi.ptr64 then addl v1 v2 else add v1 v2
    end.

  Definition set_builtin_res (br: builtin_res reg) (av: ival) (ae: aenv) : aenv :=
    match br with
    | BR r => AE.set r av ae
    | _ => ae
    end.

  Definition transfer_builtin_default
                (ae: aenv)
                (args: list (builtin_arg reg)) (res: builtin_res reg) :=
    Some (set_builtin_res res Itop ae).

  Definition eval_static_builtin_function
                (ae: aenv)
                (bf: builtin_function) (args: list (builtin_arg reg)) :=
    match builtin_function_sem bf
                   (map val_of_ival (map (abuiltin_arg ae) args)) with
    | Some v => ival_of_val v
    | None => None
    end.

  Definition transfer_builtin (_ : prog_info) (ef : external_function)
                (args: list (builtin_arg reg)) (res: builtin_res reg) (ae : aenv): VA.t :=
    match ef, args with
    | EF_vload chunk, addr :: nil =>
        Some (set_builtin_res res Itop ae)
    | EF_vstore chunk, addr :: v :: nil =>
        Some (set_builtin_res res Itop ae)
    | EF_memcpy sz al, dst :: src :: nil =>
        Some (set_builtin_res res Itop ae)
    | (EF_annot _ _ _ | EF_debug _ _ _), _ =>
        Some (set_builtin_res res Itop ae)
    | EF_annot_val _ _ _, v :: nil =>
        let av := abuiltin_arg ae v in
        Some (set_builtin_res res av ae)
    | EF_builtin name sg, _ =>
        match lookup_builtin_function name sg with
        | Some bf =>
            match eval_static_builtin_function ae bf args with
            | Some av => Some (set_builtin_res res av ae)
            | None => transfer_builtin_default ae args res
            end
        | None => transfer_builtin_default ae args res
        end
    | _, _ =>
        transfer_builtin_default ae args res
    end.

  Definition transfer_jumpi (_ : prog_info) (arg : reg) (i : int) (ae : aenv) : VA.t :=
    Some (AE.set arg (intconst i) ae).

  Definition widen_node (_ : IR.function) (_ : IR.node) := true.

  Local Notation genv := (Genv.t (fundef IR.function) unit).
  
  Definition asmatch (_ : prog_info) (_ : genv) (_ : ghost_env) (_ : block) (rs : RTL.regset) (_ : mem)
                     (ae : astate): Prop :=
    ematch rs ae.

  Definition valid_callstate (_ : prog_info) (_ : genv) (_ : ghost_env) (_ : mem) (_ : list val): Prop :=
    True.
  Definition valid_returnstate (_ : prog_info) (_ : genv) (_ : ghost_env) (_ : mem) (_ : val) : Prop :=
    True.
  Definition succ_state (_ : prog_info) (_ : genv) (_ : block)
                        (_ : ghost_env) (_ : mem) (_ : ghost_env) (_ : mem) : Prop :=
    True.

  Lemma asmatch_ge: forall pi ge gh sp rs m s0 s1,
    VA.ge (Astate s1) (Astate s0) ->
    asmatch pi ge gh sp rs m s0 ->
    asmatch pi ge gh sp rs m s1.
  
  Lemma succ_state_refl pi ge bd gh m:
    succ_state pi ge bd gh m gh m.

  Lemma succ_state_trans pi ge bd gh0 m0 gh1 m1 gh2 m2:
    succ_state pi ge bd gh0 m0 gh1 m1 ->
    succ_state pi ge bd gh1 m1 gh2 m2 ->
    succ_state pi ge bd gh0 m0 gh2 m2.

  Lemma initial_valid_callstate prog b f m cu:
    let ge := Genv.globalenv prog in
    Genv.init_mem prog = Some m ->
    Genv.find_symbol ge prog.(prog_main) = Some b ->
    Genv.find_funct_ptr ge b = Some f ->
    IR.funsig f = signature_main ->
    forall (LINK : linkorder cu prog),
    exists gh, valid_callstate (get_prog_info cu) (Genv.globalenv prog) gh m nil.

  Lemma sound_tailcall pi ge gh sp m lo hi m' rs aa args
    (MATCH : asmatch pi ge gh sp rs m aa)
    (MEM : Mem.free m sp lo hi = Some m'):
    exists gh',
      valid_callstate pi ge gh' m' (rs ## args) /\
      (forall gh1 m1, succ_state pi ge (Mem.nextblock m') gh' m' gh1 m1 ->
                      succ_state pi ge sp gh m gh1 m1).
  
  Lemma sound_return pi ge gh sp m lo hi m' rs aa or
    (MATCH : asmatch pi ge gh sp rs m aa)
    (MEM : Mem.free m sp lo hi = Some m'):
    exists gh',
      valid_returnstate pi ge gh' m' (regmap_optget or Vundef rs) /\
      succ_state pi ge sp gh m gh' m'.

  Lemma sound_external_call pi ge gh m args ef t res m'
    (VCS : valid_callstate pi ge gh m args)
    (EXTCALL : external_call ef ge args m t res m'):
    exists gh',
      valid_returnstate pi ge gh' m' res /\
      succ_state pi ge (Mem.nextblock m) gh m gh' m'.

  Lemma function_init pi ge gh m args f m' sp
    (VCS : valid_callstate pi ge gh m args)
    (ARGTYPE: Val.has_argtype_list args (IR.fn_sig f).(sig_args))
    (ALLOC: Mem.alloc m 0 (IR.fn_stacksize f) = (m', sp)):
    exists aa gh',
      entry_state f = Astate aa /\
      asmatch pi ge gh' sp (RTL.init_regs args (IR.fn_params f)) m' aa /\
      succ_state pi ge sp gh m gh' m'.

  Section BUILTIN_SOUNDNESS.
  Lemma abuiltin_arg_sound:
    forall {F V : Type} (ge : Genv.t F V) rs m ae sp
    (EMATCH : ematch rs ae)
    a v
    (EVAL : eval_builtin_arg ge (fun r => rs#r) (Vptr sp Ptrofs.zero) m a v),
    vmatch v (abuiltin_arg ae a).

  Lemma abuiltin_args_sound:
    forall {F V : Type} (ge : Genv.t F V) rs sp m ae
    (EMATCH : ematch rs ae)
    al vl
    (EVAL : eval_builtin_args ge (fun r => rs#r) (Vptr sp Ptrofs.zero) m al vl),
    list_forall2 vmatch vl (map (abuiltin_arg ae) al).

  Lemma set_builtin_res_sound:
    forall rs ae v av res,
    ematch rs ae ->
    vmatch v av ->
    ematch (regmap_setres res v rs) (set_builtin_res res av ae).

  Lemma eval_static_builtin_function_sound:
    forall {F V : Type} (ge : Genv.t F V)
           rs sp m ae (bf: builtin_function) al vl v va,
    ematch rs ae ->
    eval_builtin_args ge (fun r => rs#r) (Vptr sp Ptrofs.zero) m al vl ->
    eval_static_builtin_function ae bf al = Some va ->
    builtin_function_sem bf vl = Some v ->
    vmatch v va.
  End BUILTIN_SOUNDNESS.

  Section TRANSFER_SOUNDNDESS.

    Variables (pi : prog_info) (ge : genv) (gh : ghost_env) (sp : block) (rs : RTL.regset) (m : mem)
              (s0 : astate).

  Lemma transfer_op_correct op args res v
    (MATCH : asmatch pi ge gh sp rs m s0)
    (EVAL : eval_operation ge (Vptr sp Ptrofs.zero) op rs ## args m = Some v):
    exists s1,
      transfer_op pi op args res s0 = Astate s1 /\
      asmatch pi ge gh sp (rs#res <- v) m s1.

  Lemma transfer_load_correct trap chunk addr args res v
    (MATCH : asmatch pi ge gh sp rs m s0)
    (LOAD : RTL.has_loaded ge (Vptr sp Ptrofs.zero) rs m chunk addr args v trap):
    exists s1,
      transfer_load pi trap chunk addr args res s0 = Astate s1 /\
      asmatch pi ge gh sp (rs#res <- v) m s1.

  Lemma transfer_store_correct chunk addr args a src m'
    (MATCH : asmatch pi ge gh sp rs m s0)
    (EVAL : eval_addressing ge (Vptr sp Ptrofs.zero) addr rs##args = Some a)
    (STORE : Mem.storev chunk m a rs # src = Some m'):
    exists s1,
      transfer_store pi chunk addr args src s0 = Astate s1 /\
      asmatch pi ge gh sp rs m' s1 /\
      succ_state pi ge sp gh m gh m'.

  Lemma filter_condition_sound cond regs
    (EMATCH : ematch rs s0)
    (COND : eval_condition cond (rs ## regs) m = Some true):
    ematch rs (filter_condition cond regs s0).

  Lemma transfer_condition_correct cond args b
    (MATCH : asmatch pi ge gh sp rs m s0)
    (EVAL : eval_condition cond rs ## args m = Some b):
    exists s1,
      (let (sso, snot) := transfer_condition pi cond args s0 in
       if b then sso else snot) = Astate s1 /\
      asmatch pi ge gh sp rs m s1.

  Lemma transfer_call_correct args res
    (MATCH : asmatch pi ge gh sp rs m s0):
    exists gh_ce0,
      valid_callstate pi ge gh_ce0 m (rs ## args) /\
    forall gh_ce1 m' vres,
      valid_returnstate pi ge gh_ce1 m' vres ->
      succ_state pi ge (Mem.nextblock m) gh_ce0 m gh_ce1 m' ->
    exists s1 gh_cr1,
      transfer_call pi args res s0 = Astate s1 /\
      asmatch pi ge gh_cr1 sp (rs # res <- vres) m' s1 /\
      succ_state pi ge sp gh m gh_cr1 m'.

  Lemma transfer_builtin_correct args vargs ef t vres m' res
    (MATCH : asmatch pi ge gh sp rs m s0)
    (EVAL : eval_builtin_args ge (fun r : positive => rs # r) (Vptr sp Ptrofs.zero) m args vargs)
    (CALL : external_call ef ge vargs m t vres m'):
    exists s1 gh',
      transfer_builtin pi ef args res s0 = Astate s1 /\
      asmatch pi ge gh' sp (regmap_setres res vres rs) m' s1 /\
      succ_state pi ge sp gh m gh' m'.

  Lemma transfer_jumpi_correct arg i
    (MATCH : asmatch pi ge gh sp rs m s0)
    (R_EQ : rs # arg = Vint i):
    exists s1,
      transfer_jumpi pi arg i s0 = Astate s1 /\
      asmatch pi ge gh sp rs m s1.

    Definition eforget := ZIntervalDomain.eforget.
    Definition eforget_ge := ZIntervalDomain.eforget_ge.
  End TRANSFER_SOUNDNDESS.
End ZIntervalAADomain.