Module BTL_ZIntervalAnalysis

Require Import Coqlib.
Require Import BTL AnalysisDomain BTL_AnalysisLib ZIntervalAnalysis ZIntervalDomain ZIntervalAOp.
Require Import Op Registers Integers Values Memory IntPromotionCommon IntPromotion.

Module AAD := ZIntervalAADomain BTL_IRspec.
Module AA := BTL_AbstractAnalysis AAD.
Definition analyze : function -> Maps.PMap.t (option aenv) := AA.analyze tt.


Module BTL_ZIntervalAADomain_Annotate <: BTL_AnalysisLib.BTL_AADomain_Annotate.
  Include AAD.
 
  Definition unreachable_inst_promotable (op : operation + condition) (args : list reg) : inst_promotion_info :=
    let fake_args := map (fun _ => intconst Int.zero) args in
    let ceq_args := map (fun _ => true) args in
    match op with
    | inl op =>
        IPromotableOp (mk_op_prom_ceq (promote_operation op fake_args) ceq_args true)
    | inr cond =>
        IPromotableCond (mk_cond_prom_ceq (promote_condition cond fake_args) ceq_args)
    end.
  Definition unreachable_addr_aval : option ValueDomain.aval := None.

  Definition is_int_pos_ival (x : ival) : bool :=
    match x with
    | Iint _ x => is_int_pos x
    | _ => false
    end.

  Definition op_inst_promotable (_ : prog_info) (aa : astate) (op : operation) (args : list reg)
    : inst_promotion_info :=
    let ars := aregs aa args in
    IPromotableOp (mk_op_prom_ceq
      (promote_operation op (aregs aa args))
      (map is_int_pos_ival ars) (is_int_pos_ival (eval_static_operation op ars))).

  Definition cond_inst_promotable (_ : prog_info) (aa : astate) (cond : condition) (args : list reg)
    : inst_promotion_info :=
    IPromotableCond (mk_cond_prom_ceq
      (promote_condition cond (aregs aa args)) (map is_int_pos_ival (aregs aa args))).

  Definition get_addr_aval (_ : prog_info) (_ : astate) (_ : addressing) (_ : list reg) : option ValueDomain.aval :=
    None.

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

  Local Opaque eval_static_operation.

  Lemma is_int_pos_ival_correct (v : val) (a : ival)
    (MATCH : vmatch v a):
    is_int_pos_ival a = true -> val_promotes_eq v.

  Lemma is_int_pos_ival_list_correct (v : list val) (a : list ival)
    (MATCH : list_forall2 vmatch v a):
    list_val_promotes_eq (map is_int_pos_ival a) v.

  Lemma op_inst_promotable_correct op prom args
    (MATCH : asmatch pi ge gh sp rs m aa)
    (PROM : op_inst_promotable pi aa op args = IPromotableOp prom)
    (ALIVE : eval_operation ge (Vptr sp Ptrofs.zero) op rs##args m <> None):
    adp_op_promotable ge (Vptr sp Ptrofs.zero) m op prom rs##args.
  
  Lemma cond_inst_promotable_correct cond prom args
    (MATCH : asmatch pi ge gh sp rs m aa)
    (PROM : cond_inst_promotable pi aa cond args = IPromotableCond prom)
    (ALIVE : eval_condition cond rs##args m <> None):
    adp_cond_promotable m cond prom rs##args.

  Lemma get_addr_aval_correct addr args aaddr a
    (MATCH : asmatch pi ge gh sp rs m aa)
    (AADDR : get_addr_aval pi aa addr args = Some aaddr)
    (EVAL : eval_addressing ge (Vptr sp Ptrofs.zero) addr rs##args = Some a):
    ValueDomain.vmatch gh a aaddr.

  End SOUNDNESS.

End BTL_ZIntervalAADomain_Annotate.