Module RTLperm

Require Import MoreRTL.
Import Utf8.
Import Util.
Import Coqlib Maps.
Import Integers Values Registers Globalenvs Memory.
Import RTL.
Import MoreSemantics.

Unset Elimination Schemes.

Definition perm_t : Type := block → Z → perm_kind → option permission.

Definition mem_perm (m: mem) : perm_t :=
  λ b o k, (Mem.mem_access m) # b o k.

Definition eq3 {Α Β Γ Δ} (f g: Α → Β → Γ → Δ) : Prop :=
  ∀ x y z, f x y z = g x y z.

Notation "f =3 g" := (eq3 f g) (at level 70).

Lemma eq3_trans {Α Β Γ Δ} (f g h: Α → Β → Γ → Δ):
  f =3 g → g =3 h → f =3 h.

Record stackframe : Type := SF {
  perm : perm_t;
  sf: RTL.stackframe }.

Inductive state : Type :=
| State (stk: list stackframe) (perm: perm_t) (fn: function) (sp: val) (pc: node) (ε: regset) (m: mem)
| Callstate (stk: list stackframe) (fd: fundef) (args: list val) (m: mem)
| Returnstate (stk: list stackframe) (res: val) (m: mem).

Definition erase_stack :=
  List.map sf.

Definition erase (s: state) : RTL.state :=
  match s with
  | State stk _ fn sp pc ε m => RTL.State (erase_stack stk) fn sp pc ε m
  | Callstate stk fd args m => RTL.Callstate (erase_stack stk) fd args m
  | Returnstate stk res m => RTL.Returnstate (erase_stack stk) res m
  end.

Definition step (ge: genv) (s: state) (tr: Events.trace) (s': state) : Prop :=
  step ge (erase s) tr (erase s') ∧
  match s, s' with
  | State stk p _ _ _ _ _, State stk' p' _ _ _ _ _ => stk' = stk ∧ p' = p
  | State stk p _ _ _ _ _, Callstate stk' _ _ _ =>
    stk' = stk ∨
    match stk' with nil => False | s :: stk' => stk' = stk ∧ s.(perm) = p end
  | Callstate stk _ _ _, Returnstate stk' _ _ => stk' = stk
  | Callstate stk _ _ _, State stk' p' _ _ _ _ m' => stk' = stk ∧ p' =3 (mem_perm m')
  | State stk _ _ _ _ _ _, Returnstate stk' _ _ => stk' = stk
  | Returnstate (s :: stk) _ _, State stk' p _ _ _ _ _ => stk' = stk ∧ s.(perm) = p
  | _, _ => False
  end.

Definition initial_state (p: program) (s: state) : Prop :=
  RTL.initial_state p (erase s).
  
Definition final_state (s: state) (v: int) : Prop :=
  RTL.final_state (erase s) v.

Definition semantics (p: program) : Smallstep.semantics :=
  Smallstep.Semantics step (initial_state p) final_state (Genv.globalenv p).

Theorem erase_simulation p : Smallstep.forward_simulation (semantics p) (RTL.semantics p).

Theorem simulation p : Smallstep.forward_simulation (RTL.semantics p) (semantics p).

Fixpoint stack_invariant (stk: list stackframe) (fn: function) (sp: val) (m: mem) : Prop :=
  match stk with
  | nil => True
  | SF p' (Stackframe _ fn' sp' _ _) :: stk' =>
    match sp with
    | Vptr b i =>
      ∀ m', Mem.free m b (Int.unsigned i) (fn_stacksize fn) = Some m' →
            p' =3 mem_perm m' ∧ stack_invariant stk' fn' sp' m'
    | _ => True
    end
  end.

Definition invariant s : Prop :=
  match s with
  | State stk p fn sp _ _ m => p =3 mem_perm m ∧ stack_invariant stk fn sp m
  | Returnstate (SF p (Stackframe _ fn sp _ _) :: stk) _ m => p =3 mem_perm m ∧ stack_invariant stk fn sp m
  | Callstate (SF p (Stackframe _ fn sp _ _) :: stk) _ _ m => p =3 mem_perm m ∧ stack_invariant stk fn sp m
  | _ => True
  end.

Lemma invariant_init p : initial_state p ⊆ invariant.

Lemma mem_store_perm {κ m b o v m'} :
  Mem.store κ m b o v = Some m' →
  mem_perm m =3 mem_perm m'.

Lemma mem_free_perm {m b lo hi m'} :
  Mem.free m b lo hi = Some m' →
  ∀ q, mem_perm q =3 mem_perm m →
       ∃ q', Mem.free q b lo hi = Some q' ∧
             mem_perm q' =3 mem_perm m'.

Lemma stack_invariant_perm stk :
  ∀ (fn : function) (sp : val) (m : mem),
    stack_invariant stk fn sp m →
    ∀ m' : mem,
      mem_perm m =3 mem_perm m' →
      stack_invariant stk fn sp m'.

Lemma alloc_free_perm {m lo hi m' sp m''} :
  Mem.alloc m lo hi = (m', sp) →
  Mem.free m' sp lo hi = Some m'' →
  mem_perm m =3 mem_perm m''.

Lemma no_infinite_list {A: Type} {a: A} {m: list A} (P: Prop) :
  m = a :: m → P.

Definition allowed_builtin ef : bool :=
  match ef with
  | AST.EF_malloc
  | AST.EF_free
  | AST.EF_inline_asm _ _ _
    => false
  | _ => true
  end.

Definition no_fancy_builtin (p: program) : bool :=
  List.forallb
    (λ q,
     match q with
     | (_, AST.Gfun (AST.External ef)) => allowed_builtin ef
     | (_, AST.Gfun (AST.Internal fn)) =>
       PTree_Properties.for_all
         (fn_code fn)
         (λ pc i,
          match i with
          | Ibuiltin ef _ _ _ => allowed_builtin ef
          | _ => true
          end)
     | _ => true end)
    (AST.prog_defs p).

Section S.

Variable p : program.
Let ge := Genv.globalenv p.

Hypothesis external_calls_do_not_change_the_permissions :
  ∀ name sg args m tr vres m',
  Events.external_functions_sem name sg ge args m tr vres m' →
  mem_perm m =3 mem_perm m'.

Hypothesis no_external_call :
  no_fancy_builtin p = true.

Lemma invariant_step s : reachable (semantics p) s → invariant s → ∀ tr, step ge s tr ⊆ invariant.

Theorem consistent_permissions : MoreSemantics.invariant (semantics p) invariant.

End S.