Module CountingSem

Require Import Coqlib.
Require Import Maps.
Require Import AST.
Require Import Integers.
Require Import Values.
Require Import Events.
Require Import Memory.
Require Import Globalenvs.
Require Import Smallstep.
Require Import Op.
Require Import Registers.
Require Import RTL.
Require Import Errors.
Require Import String.
Require Import DLib.
Require Import Scope.
Require Import Counter.

Open Scope error_monad_scope.

Definition check_one_single_func (prog:program) : res function :=
  let ge := Genv.globalenv prog in
  do b_main <- get_opt (Genv.find_symbol ge prog.(prog_main)) "main block not found";
  do main <- get_opt (Genv.find_funct_ptr ge b_main) "main func not found";
    match main with
      | External _ => Error (MSG "main is external"::nil)
      | Internal main =>
        do _ <- ptree_forall_error
          (fun pc ins =>
            match ins with
              | Itailcall _ _ _
              | Icall _ _ _ _ _ => Error (MSG "call after inlining ?"::nil)
              | _ => OK tt
            end)
          (fn_code main);
          OK main
    end.

Section ge.

Variable ge: genv.
Variable f: function.
Variable fsc:Scope.family f.
Variable sp: val.
Variable scopes: list Scope.t.


Inductive state : Type :=
| State (pc: node) (* current program point in c *)
           (rs: regset) (* register state *)
           (m: mem) (* memory state *)
.

Inductive step: state -> trace -> state -> Prop :=
  | exec_Inop:
      forall pc rs m pc',
      (fn_code f)!pc = Some(Inop pc') ->
      step (State pc rs m)
        E0 (State pc' rs m)
  | exec_Iop:
      forall pc rs m op args res pc' v,
      (fn_code f)!pc = Some(Iop op args res pc') ->
      eval_operation ge sp op rs##args m = Some v ->
      step (State pc rs m)
        E0 (State pc' (rs#res <- v) m)
  | exec_Iload:
      forall pc rs m chunk addr args dst pc' a v,
      (fn_code f)!pc = Some(Iload chunk addr args dst pc') ->
      eval_addressing ge sp addr rs##args = Some a ->
      Mem.loadv chunk m a = Some v ->
      step (State pc rs m)
        E0 (State pc' (rs#dst <- v) m)
  | exec_Istore:
      forall pc rs m chunk addr args src pc' a m',
      (fn_code f)!pc = Some(Istore chunk addr args src pc') ->
      eval_addressing ge sp addr rs##args = Some a ->
      Mem.storev chunk m a rs#src = Some m' ->
      step (State pc rs m)
        E0 (State pc' rs m')
  | exec_Ibuiltin:
      forall pc rs m ef args res pc' t v m',
      (fn_code f)!pc = Some(Ibuiltin ef args res pc') ->
      external_call ef ge rs##args m t v m' ->
      step (State pc rs m)
         t (State pc' (rs#res <- v) m')
  | exec_Icond:
      forall pc rs m cond args ifso ifnot b pc',
      (fn_code f)!pc = Some(Icond cond args ifso ifnot) ->
      eval_condition cond rs##args m = Some b ->
      pc' = (if b then ifso else ifnot) ->
      step (State pc rs m)
        E0 (State pc' rs m)
  | exec_Ijumptable:
      forall pc rs m arg tbl n pc',
      (fn_code f)!pc = Some(Ijumptable arg tbl) ->
      rs#arg = Vint n ->
      list_nth_z tbl (Int.unsigned n) = Some pc' ->
      step (State pc rs m)
        E0 (State pc' rs m)
.

Definition get_pc (s:state) : node :=
  match s with
    | State pc rs m => pc
  end.

Definition get_rs (s:state) : regset :=
  match s with
    | State pc rs m => rs
  end.

Definition get_mem (s:state) : mem :=
  match s with
    | State pc rs m => m
  end.

Definition inc_r_counter (n n' : node) (rcs : counter) : counter :=
  reset_counters (exited_scopes fsc n n') (inc_counter n rcs).

Definition inc_r'_counter (n n' : node) (rcs : counter) : counter :=
  inc_counter n' (reset_counters (exited_scopes fsc n n') rcs).

Record cstate : Type := CST {
  get_st :> state;
  get_cs : counter;
  get_rcs : counter
}.

Notation "a %pc" := (get_pc a) (at level 1).
Notation "a %rs" := (get_rs a) (at level 1).
Notation "a %m" := (get_mem a) (at level 1).
Notation "a %cs" := (get_cs a) (at level 1).
Notation "a %rcs" := (get_rcs a) (at level 1).

Inductive cstep: cstate -> cstate -> Prop :=
| cstep_def: forall s1 t s2 cs1 rcs1 cs2 rcs2,
  step s1 t s2 ->
  cs2 = inc_counter s1%pc cs1 ->
  rcs2 = inc_r_counter s1%pc s2%pc rcs1 ->
  cstep (CST s1 cs1 rcs1) (CST s2 cs2 rcs2).

Notation entry := f.(fn_entrypoint).

Definition init_st (rs : regset) (m : mem) :=
  CST (State entry rs m) init_counter init_counter.

Inductive Reach rs m : cstate -> Prop :=
| R_init : Reach rs m (init_st rs m)
| R_step : forall s s', Reach rs m s -> cstep s s' -> Reach rs m s'.

Inductive Trace rs m : list cstate -> Prop :=
| T_init : Trace rs m (init_st rs m :: nil)
| T_cons : forall s s' tr, Trace rs m (s :: tr) -> cstep s s' -> Trace rs m (s' :: s :: tr).

CoInductive State_diverge: cstate -> Prop :=
| State_diverge_intro: forall s1 s2,
  cstep s1 s2 ->
  State_diverge s2 ->
  State_diverge s1.

Definition Terminates rs m : Prop :=
  ~ State_diverge (init_st rs m).

Definition Reaches_final rs m : Prop :=
  exists s, exists o,
    Reach rs m s /\
    ((fn_code f) ! (get_pc s)) = Some (Ireturn o).


Lemma in_Trace_Reach:
  forall
    rs m tr
    (TR : Trace rs m tr),
    forall s,
      In s tr ->
      Reach rs m s.
Proof.
    induction tr; intuition.
    inv TR.
    simpl in H; intuition; subst.
    apply R_init.
    simpl in H; intuition; subst.
    apply R_step with (s := s0); auto.
    auto with datatypes.
  Qed.

Lemma Reach_ex_Trace:
  forall rs m s, Reach rs m s -> exists tr, Trace rs m (s::tr).
Proof.
  induction 1.
  econstructor; econstructor.
  destruct IHReach.
  econstructor; econstructor; eauto.
Qed.

End ge.