Module MoreRTL

Require Import RTL.
Require Import MoreSemantics.
Require Import AssocList.
Import Utf8.
Import Coqlib Maps.
Import Globalenvs.
Import Memory.
Import Integers.
Require Import Extra.
Import Annotations.

Lemma semantics_determinate:
  forall (p: program), Smallstep.determinate (semantics p).


Section BACK_EDGES.
  
  Definition node_set : Type := PTree.t unit.
  Definition empty : node_set := PTree.empty _.
  Definition mem (n: node) (s: node_set) : { s ! n = Some tt } + { s ! n = None } :=
    match s ! n as b return { b = Some tt } + { b = None } with
    | Some x => let 'tt as y := x return { Some y = Some tt } + { _ = None } in left eq_refl
    | None => right eq_refl
    end.

  Definition add (n: node) (s: node_set) : node_set :=
    if mem n s then s else PTree.set n tt s.

  Context (m: code).


  Definition back_edges : node_set :=
    PTree.fold (λ s pc i,
                let succ := successors_instr i in
                List.fold_left (λ s pc',
                                if (pc <=? pc')%positive
                                then add pc' s
                                else s
                               ) succ s
               ) m empty.

End BACK_EDGES.

Section COLLECT_ANNOT.

Variable p: RTL.program.


Definition sizeof (g: AST.ident) : Z :=
  match assoc g (AST.prog_defs p) with
  | Some (AST.Gvar gv) => Genv.init_data_list_size (AST.gvar_init gv)
  | _ => 1
  end.

Definition is_trivial_annotation (α: annotation) (κ: AST.memory_chunk) (addr: Op.addressing) : bool :=
  match snd α with
  | nil => true
  | bs :: nil =>
    match bs with
    | ABglobal g r =>
      match addr with
      | Op.Abased g' _
      | Op.Abasedscaled _ g' _ =>
        if AST.ident_eq g g'
        then range_leb (Int.zero, Int.repr (Z.max 0 (Z.min (sizeof g - size_chunk κ) Int.max_unsigned))) r
        else false
      | Op.Aglobal g' o =>
        if AST.ident_eq g g'
        then range_leb (o, o) r
        else false
      | _ => false
      end
    | ABlocal O _ r =>
      match addr with
      | Op.Ainstack o => range_leb (o, o) r
      | _ => false
      end
    | ABlocal (S _) _ _ => false
    end
  | _ => false
  end.


Definition collect_annot_in_fun (f: function) : node_set -> node_set :=
  PTree.fold
    (λ acc _ i,
     match i with
     | Inop _
     | Iop _ _ _ _
     | Icall _ _ _ _ _
     | Itailcall _ _ _
     | Ibuiltin _ _ _ _
     | Icond _ _ _ _
     | Ijumptable _ _
     | Ireturn _
       => acc
     | Iload ((n, _) as α) κ addr _ _ _
     | Istore ((n, _) as α) κ addr _ _ _
       =>
       if is_trivial_annotation α κ addr
       then acc
       else add n acc
     end)
    (fn_code f).

Definition collect_annot : node_set :=
  List.fold_left
    (λ acc def,
     match def with
     | (_, AST.Gfun (AST.Internal f)) => collect_annot_in_fun f acc
     | _ => acc
     end)
    (AST.prog_defs p) empty.

End COLLECT_ANNOT.


Section CALL_DECLARED.

Context (p: program).

Definition declared_fundef (fd: fundef) : Prop :=
  ∃ name, In (name, AST.Gfun fd) (AST.prog_defs p).
Arguments declared_fundef _ /.

Definition declared_in_frame (sf: stackframe) : Prop :=
  let 'Stackframe _ fn _ _ _ := sf in
  declared_fundef (AST.Internal fn).

Definition declared_in_stack (stk: list stackframe) : Prop :=
  Forall declared_in_frame stk.

Definition call_declared (s: state) : Prop :=
  match s with
  | Returnstate stk _ _ => declared_in_stack stk
  | State stk fn _ _ _ _ => declared_in_stack stk ∧ declared_fundef (AST.Internal fn)
  | Callstate stk fd _ _ => declared_in_stack stk ∧ declared_fundef fd
  end.

Theorem call_declared_invariant : invariant (semantics p) call_declared.

End CALL_DECLARED.

Section PERMISSION_IN_BOUNDS.


Context (p: program) (m₀: Mem.mem).
Let ge := Genv.globalenv p.

Hypothesis names_norepet : list_norepet (AST.prog_defs_names p).
Hypothesis initial_memory : Genv.init_mem p = Some m₀.

Lemma mem_perm_nonempty {m b o k pe} :
  Mem.perm m b o k pe →
  Mem.perm m b o k Nonempty.

Lemma permission_in_bounds :
  ∀ g b,
    Genv.find_symbol ge g = Some b →
    ∀ ofs,
      Mem.perm m₀ b ofs Max Nonempty →
      0 <= ofs ∧ ofs < sizeof p g.

Definition mem_has_initial_global_max_permission (m: Mem.mem) : Prop :=
  ∀ g b,
    Genv.find_symbol ge g = Some b →
    ∀ ofs,
      Mem.perm m b ofs Max ⊆ Mem.perm m₀ b ofs Max.

Definition initially_valid_blocks_are_still_valid (m: Mem.mem) : Prop :=
  Mem.valid_block m₀ ⊆ Mem.valid_block m.

Definition mem_of_state (s: state) : Mem.mem :=
  match s with
  | State _ _ _ _ _ m
  | Callstate _ _ _ m
  | Returnstate _ _ m
    => m
  end.

Arguments mem_of_state s /.

Definition state_has_initial_global_max_permission (s: state) : Prop :=
  mem_of_state s ∈ (mem_has_initial_global_max_permission ∩ initially_valid_blocks_are_still_valid).

Theorem permission_in_bounds_invariant : invariant (semantics p) state_has_initial_global_max_permission.

Definition valid_access_in_bounds (m: Mem.mem) : Prop :=
  ∀ g b,
  Genv.find_symbol ge g = Some b →
  ∀ κ ofs pe,
  Mem.valid_access m κ b ofs pe →
  0 <= ofs ∧ ofs <= sizeof p g - size_chunk κ.

Local Opaque mem_of_state.

Corollary valid_access_in_bounds_invariant : invariant (semantics p) (valid_access_in_bounds ∘ mem_of_state).

End PERMISSION_IN_BOUNDS.

Section STACKS.

  Import Values.

  Definition stack : Type := list val.

  Definition stack_of_frames (stk: list stackframe) : stack :=
    List.map (λ sf, let 'Stackframe _ _ sp _ _ := sf in sp) stk.

  Definition stack_of_state (s: state) : stack :=
    match s with
    | State stk _ sp _ _ _ => sp :: stack_of_frames stk
    | Callstate stk _ _ _
    | Returnstate stk _ _ => stack_of_frames stk
    end.

  Definition pointer_to_block (v: val) (b: block) : Prop :=
    v = Vptr b Int.zero.

  Arguments list_norepet {_} _.

  Definition wf_stack (m: Mem.mem) (stk: stack) : Prop :=
    ∃ ptrs,
      ptrs ∈ (Forall2 pointer_to_block stk ∩ list_norepet ∩ Forall (Mem.valid_block m)).

  Lemma wf_stack_pop m v stk :
    wf_stack m (v :: stk) → wf_stack m stk.

  Lemma wf_stack_m {m m'} :
    Mem.valid_block m ⊆ Mem.valid_block m' →
    wf_stack m ⊆ wf_stack m'.

  Theorem wf_stack_invariant (p: program) :
    invariant (RTL.semantics p) (λ s, wf_stack (mem_of_state s) (stack_of_state s)).
  
End STACKS.