Module AnalysisDomain

Require Import ZArith List Maps Coqlib Lattice.
Require Import AST Registers Op.
Require Import Linking Values Integers Memory Events Globalenvs.
Require ValueDomain.

Definition ghost_env := ValueDomain.block_classification.

Definition dummy_ghost_env : ghost_env.

Module Type IRspec.
  Parameter function : Type.
  Parameter node : Type.
  Parameter fn_stacksize : function -> Z.
  Parameter fn_params : function -> list reg.
  Parameter fn_sig : function -> signature.
  Parameter funsig : fundef function -> signature.
End IRspec.

Module Type AADomain (IR : IRspec).
  Declare Module VA : SEMILATTICE_WITH_WIDENING.
 
  Parameter astate : Type.
  Parameter Astate : astate -> VA.t.
  Parameter filter_astate: VA.t -> option astate.
  Axiom filter_astate_bot: filter_astate VA.bot = None.
  Axiom filter_iff_Astate: forall s s', filter_astate s = Some s' <-> s = Astate s'.
  Axiom filter_ge: forall s s', VA.ge s s' -> filter_astate s = None -> filter_astate s' = None.

  Parameter eforget: list reg -> astate -> astate.
  Axiom eforget_ge : forall rl ae,
      VA.ge (Astate (eforget rl ae)) (Astate ae).
  
  Parameter default_top : VA.t.
  Axiom ge_default_top: forall s', VA.ge default_top s'.

  Parameter entry_state : IR.function -> VA.t.

  Parameter prog_info : Type.
  Parameter get_prog_info : program (fundef IR.function) unit -> prog_info.
 
  Parameter transfer_op : prog_info -> operation -> list reg -> reg ->
                                 astate -> VA.t.
  Parameter transfer_load : prog_info -> trapping_mode -> memory_chunk -> addressing -> list reg -> reg ->
                                 astate -> VA.t.
  Parameter transfer_store : prog_info -> memory_chunk -> addressing -> list reg -> reg ->
                                 astate -> VA.t.
  Parameter transfer_memcpy : prog_info -> cpychunk -> list (builtin_arg reg) ->
                                 astate -> VA.t.
  Parameter transfer_condition : prog_info -> condition -> list reg ->
                                 astate -> VA.t * VA.t.
  Parameter transfer_call : prog_info -> list reg -> reg ->
                                 astate -> VA.t.
  Parameter transfer_builtin : prog_info -> external_function -> list (builtin_arg reg) -> builtin_res reg ->
                                 astate -> VA.t.
  Parameter transfer_jumpi : prog_info -> reg -> int ->
                                 astate -> VA.t.

  Parameter widen_node : IR.function -> IR.node -> bool.


  Local Notation genv := (Genv.t (fundef IR.function) unit).

  Parameter asmatch : prog_info -> genv -> ghost_env -> block -> RTL.regset -> mem -> astate -> Prop.

  Parameter valid_callstate : prog_info -> genv -> ghost_env -> mem -> list val -> Prop.

  Parameter valid_returnstate : prog_info -> genv -> ghost_env -> mem -> val -> Prop.

  Parameter succ_state : prog_info -> genv -> block ->
                         ghost_env -> mem ->
                         ghost_env -> mem -> Prop.
 
  
  Axiom 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.

  Axiom succ_state_refl : forall pi ge bd gh m,
    succ_state pi ge bd gh m gh m.

  Axiom succ_state_trans : forall 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.

  Axiom initial_valid_callstate: forall 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.

  Axiom sound_tailcall: forall 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).

  Axiom sound_return: forall 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'.

  Axiom sound_external_call: forall 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'.

  Axiom function_init: forall 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) (Mem.size_alignment (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'.


  Axiom transfer_op_correct: forall pi ge gh sp rs m s0 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.

  Axiom transfer_load_correct: forall pi ge gh sp rs m s0 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.

  Axiom transfer_store_correct: forall pi ge gh sp rs m s0 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'.

  Axiom transfer_memcpy_correct: forall pi ge gh sp rs m s0 chk args m' vargs
    (MATCH : asmatch pi ge gh sp rs m s0)
    (EVAL : evalopt_builtin_args ge (fun r : positive => rs # r) (Vptr sp Ptrofs.zero) m args = Some vargs)
    (MEMCPY : memcpy_run chk vargs m = Some m'),
    exists s1,
      transfer_memcpy pi chk args s0 = Astate s1 /\
      asmatch pi ge gh sp rs m' s1 /\
      succ_state pi ge sp gh m gh m'.

  Axiom transfer_condition_correct: forall pi ge gh sp rs m s0 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.

  Axiom transfer_call_correct: forall pi ge gh sp rs m s0 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'.

  Axiom transfer_builtin_correct: forall pi ge gh sp rs m s0 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'.

  Axiom transfer_jumpi_correct: forall pi ge gh sp rs m s0 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.

End AADomain.

Module AADomainLemmas (IR : IRspec) (AA : AADomain IR).
  Import AA.
  Lemma filter_Astate [s s']:
    filter_astate s = Some s' ->
    s = Astate s'.

  Lemma Astate_filter s:
    filter_astate (Astate s) = Some s.

  Lemma Astate_inj s s'
    (H : Astate s = Astate s'):
    s = s'.
End AADomainLemmas.