From Coq Require Import Program.Equality.
Require Import Coqlib Maps List Integers Errors.
Import ListNotations.
Require Import AST.
Require Import Op Registers.
Require Import RTL RTLtyping RTLpast.

Open Scope positive.

Toolkit for writing and specifying counter-measure transformations

Some tactics

Ltac destruct_conjs :=
  repeat
    match goal with
    | H: _ /\ _ |- _ => destruct H
    | H: exists _, _ |- _ => destruct H
    end.

Ltac cases :=
  repeat
    match goal with
    | H: context [ match ?x with _ => _ end ] |- _ => destruct x
    end.

Ltac cases_eq :=
  repeat
    match goal with
    | H: context [ match ?x with _ => _ end ] |- _ => destruct x eqn:?EQ
    end.

State monad

Record state : Type := mkstate {
  st_nextnode: positive; (* last used CFG node *)
  st_code: code; (* current CFG *)
}.


Inductive sincr (s1 s2: state) : Prop :=
  Sincr (NEXTNODE: Ple s1.(st_nextnode) s2.(st_nextnode)).

Remark sincr_refl: forall s, sincr s s.

Lemma sincr_trans: forall s1 s2 s3, sincr s1 s2 -> sincr s2 s3 -> sincr s1 s3.


Inductive res {A: Type} {s: state}: Type := R (x: A) (s': state) (I: sincr s s').

Definition proj_val {A: Type} {st: state} (r: @res A st) :=
  let '(R v _ _) := r in v.

Definition proj_st {A: Type} {st: state} (r: @res A st) :=
  let '(R _ st' _) := r in st'.

Definition mon (A: Type) : Type := forall (s: state), @res A s.


Definition ret {A: Type} (x: A): mon A :=
  fun s => R x s (sincr_refl s).

Definition bind {A B: Type} (x: mon A) (f: A -> mon B): mon B :=
  fun s1 => match x s1 with R vx s2 I1 =>
              match f vx s2 with R vy s3 I2 =>
                R vy s3 (sincr_trans s1 s2 s3 I1 I2)
              end
            end.

Notation "'doM' X <- A ; B" := (bind A (fun X => B))
   (at level 200, X ident, A at level 100, B at level 200).

Lemma bind_inversion {A B: Type} : forall (x: mon A) (f: A -> mon B) v st st' sincr,
    bind x f st = R v st' sincr ->
    exists vx st1 sincr1 sincr2, x st = R vx st1 sincr1 /\ f vx st1 = R v st' sincr2.

Program Definition fresh_pc : mon node :=
  fun s =>
    let pc := s.(st_nextnode) in
    R pc (mkstate (Pos.succ pc) s.(st_code)) _.

Program Definition set_instr (pc: node) (i: instruction): mon unit :=
  fun s =>
    R tt (mkstate s.(st_nextnode) (PTree.set pc i s.(st_code))) _.

Ltac monadInv :=
  match goal with
  | H: bind _ _ _ = R _ _ _ |- _ =>
      apply bind_inversion in H as (?&?&?INCR&?INCR&?MON&?MON)
  | H: ret _ _ = R _ _ _ |- _ => inv H
  | H:fresh_pc _ = R _ _ _ |- _ => inv H
  | H:set_instr _ _ _ = R _ _ _ |- _ => inv H
  | x: res |- _ => destruct x
  | H:sincr _ _ |- _ => inv H
  end; simpl in *.

Partial state monad

Definition pmon (A: Type) : Type := forall (s: state), Errors.res (@res A s).

Definition pret {A: Type} (x: A): pmon A :=
  fun s => OK (R x s (sincr_refl s)).

Definition pbind {A B: Type} (x: pmon A) (f: A -> pmon B): pmon B :=
  fun s1 => match x s1 with
         | OK (R vx s2 I1) =>
             match f vx s2 with
             | OK (R vy s3 I2) => OK (R vy s3 (sincr_trans s1 s2 s3 I1 I2))
             | Error e => Error e
             end
         | Error e => Error e
         end.

Lemma pbind_inversion {A B: Type} : forall (x: pmon A) (f: A -> pmon B) v st st' sincr,
    pbind x f st = OK (R v st' sincr) ->
    exists vx st1 sincr1 sincr2, x st = OK (R vx st1 sincr1) /\ f vx st1 = OK (R v st' sincr2).

Ltac pMonadInv :=
  match goal with
  | H: pbind _ _ _ = OK (R _ _ _) |- _ =>
      apply pbind_inversion in H as (?&?&?INCR&?INCR&?MON&?MON)
  | H: OK _ = OK _ |- _ => inv H
  | H: Error _ = OK _ |- _ => inv H
  | H: Errors.bind _ _ = OK _ |- _ =>
      apply Errors.bind_inversion in H as (?&?MON&?MON)
  | x: unit |- _ => destruct x
  | H: _ |- _ => monadInv
  end; simpl in *.

Definition ptree_pmfold {A: Type} (f: positive -> A -> pmon unit) (t: PTree.t A): pmon unit :=
  PTree.fold (fun s1 k v => pbind s1 (fun _ => f k v)) t (pret tt).

Lemma ptree_pmfold_rec {A} f m_final st st' (P : PTree.t A -> state -> Prop) :
  (forall m m' a, (forall x, m ! x = m' ! x) -> P m a -> P m' a) ->
  P (PTree.empty _) st ->
  (forall m pc i st1 st2,
      sincr st st1 ->
      m!pc = None ->
      m_final!pc = Some i ->
      P m st1 ->
      f pc i st1 = Errors.OK st2 ->
      P (PTree.set pc i m) (proj_st st2)) ->
  @ptree_pmfold A f m_final st = Errors.OK st' ->
  P m_final (proj_st st').

Ltac extlia :=
  repeat match goal with H: _ = R _ _ _ |- _ => clear H end;
  repeat match goal with H: _ = OK (R _ _ _) |- _ => clear H end;
  repeat monadInv;
  Coqlib.extlia.

Sequence builder. This applies to passes that translate each instruction individually into a sequence of instructions.

Inductive exits : Type :=
| OneExit
| NoExit
| TwoExits
| NExits
.

Fact exits_eq_dec : forall e1 e2 : exits, {e1 = e2} + {e1 <> e2}.

Global Ltac inv_existT_eq :=
  match goal with
  | H: existT _ _ _ = existT _ _ _ |- _ =>
      apply Eqdep_dec.inj_pair2_eq_dec in H; subst; auto using exits_eq_dec
  end.

Inductive seqinstr : exits -> Type :=
| Seinstr : (node -> instruction) -> seqinstr OneExit
| Sereturn : instruction -> seqinstr NoExit
| Second : condition -> list reg -> seqinstr OneExit -> seqinstr OneExit -> option bool -> seqinstr TwoExits
| Sejumptable : reg -> seqinstr NExits
| Secatch : seqinstr NoExit
| Ssinstr {e} : (node -> instruction) -> seqinstr e -> seqinstr e
| Ssmerge2 {e} : condition -> list reg -> seqinstr OneExit -> seqinstr OneExit -> option bool -> seqinstr e -> seqinstr e
| Ssmerge1 {e} : condition -> list reg -> seqinstr NoExit -> option bool -> seqinstr e -> seqinstr e
.

Good formation of seqinstr wrt the successors_instr fun

Inductive wf_seq : forall {e}, seqinstr e -> Prop :=
| wfs_einstr : forall i,
    (forall pc, successors_instr (i pc) = [pc]) ->
    wf_seq (Seinstr i)
| wfs_ereturn : forall i,
    successors_instr i = [] ->
    wf_seq (Sereturn i)
| wfs_econd : forall c rs seq1 seq2 pred,
    wf_seq seq1 -> wf_seq seq2 ->
    wf_seq (Second c rs seq1 seq2 pred)
| wfs_ejumptable : forall r, wf_seq (Sejumptable r)
| wfs_ecatch : wf_seq Secatch
| wfs_sinstr {e} : forall i (seq: seqinstr e),
    (forall pc, successors_instr (i pc) = [pc]) ->
    wf_seq seq ->
    wf_seq (Ssinstr i seq)
| wfs_smerge2 {e} : forall c rs seq1 seq2 pred (seq: seqinstr e),
    wf_seq seq1 -> wf_seq seq2 ->
    wf_seq seq ->
    wf_seq (Ssmerge2 c rs seq1 seq2 pred seq)
| wfs_smerge1 {e} : forall c rs seq1 pred (seq: seqinstr e),
    wf_seq seq1 ->
    wf_seq seq ->
    wf_seq (Ssmerge1 c rs seq1 pred seq).
Global Hint Constructors wf_seq : rtlcm.

Ltac inv_wf_seq :=
  match goal with
  | H: wf_seq (Seinstr _) |- _ => inv H
  | H: wf_seq (Sereturn _) |- _ => inv H
  | H: wf_seq (Second _ _ _ _ _) |- _ => inv H
  | H: wf_seq (Sejumptable _) |- _ => inv H
  | H: wf_seq Secatch |- _ => inv H
  | H: wf_seq (Ssinstr _ _) |- _ => inv H
  | H: wf_seq (Ssmerge2 _ _ _ _ _ _) |- _ => inv H
  | H: wf_seq (Ssmerge1 _ _ _ _ _) |- _ => inv H
  end.

Inductive cont : exits -> Type :=
| COneExit : node -> cont OneExit
| CNoExit : cont NoExit
| CTwoExits : node -> node -> cont TwoExits
| CNExits : list node -> cont NExits.

Inductive is_cont : forall {e}, cont e -> node -> Prop :=
| isContOne : forall pc, is_cont (COneExit pc) pc
| isContTwo : forall pc1 pc2 pc,
    pc = pc1 \/ pc = pc2 ->
    is_cont (CTwoExits pc1 pc2) pc
| isContN : forall pcs pc,
    In pc pcs ->
    is_cont (CNExits pcs) pc.
Global Hint Constructors is_cont : rtlcm.

Ltac inv_is_cont :=
  match goal with
  | H:is_cont CNoExit _ |- _ => inv H
  | H:is_cont (COneExit _) _ |- _ => inv H
  | H:is_cont (CTwoExits _ _) _ |- _ => inv H
  | H:is_cont (CNExits _) _ |- _ => inv H
  end.

Ltac is_cont_specialize :=
  match goal with
  | I: (forall _, is_cont _ _ -> _), H:is_cont _ _ |- _ => specialize (I _ H)
  | H: forall _, is_cont (COneExit ?pc) _ -> _ |- _ =>
      specialize (H pc (isContOne _)) as ?PC; clear H
  | H: forall _, is_cont (CTwoExits ?pc1 ?pc2) _ -> _ |- _ =>
      specialize (H pc1 (isContTwo _ _ _ (or_introl eq_refl))) as ?PC;
      specialize (H pc2 (isContTwo _ _ _ (or_intror eq_refl))) as ?PC; clear H
  end.

Section cseq.

  Inductive cseqinstr : exits -> Type :=
  | Ceinstr : instruction -> cseqinstr OneExit
  | Cereturn : instruction -> cseqinstr NoExit
  | Cecond : condition -> list reg -> cseq OneExit -> cseq OneExit -> option bool -> cseqinstr TwoExits
  | Cejumptable : reg -> list node -> cseqinstr NExits
  | Cecatch : cseqinstr NoExit
  | Csinstr {e} : instruction -> cseq e -> cseqinstr e
  | Csmerge2 {e} : condition -> list reg -> cseq OneExit -> cseq OneExit -> option bool -> cseq e -> cseqinstr e
  | Csmerge1 {e} : condition -> list reg -> cseq NoExit -> option bool -> cseq e -> cseqinstr e

  with cseq : exits -> Type :=
  | Cseq {e} : node -> cseqinstr e -> node -> cseq e.

  Section cseq_ind2.
    Variable P : forall {e}, cseq e -> Prop.

    Hypothesis Heinstr : forall pc i pcl, P (Cseq pc (Ceinstr i) pcl).
    Hypothesis Hereturn : forall pc i pcl, P (Cseq pc (Cereturn i) pcl).
    Hypothesis Hecond : forall pc c rs s1 s2 pred pcl,
        P s1 -> P s2 -> P (Cseq pc (Cecond c rs s1 s2 pred) pcl).
    Hypothesis Hejumptable : forall pc r pcs pcl, P (Cseq pc (Cejumptable r pcs) pcl).
    Hypothesis Hecatch : forall pc pcl, P (Cseq pc Cecatch pcl).
    Hypothesis Hsinstr : forall {e} pc i (s: cseq e) pcl,
        P s -> P (Cseq pc (Csinstr i s) pcl).
    Hypothesis Hsmerge2 : forall {e} pc c rs s1 s2 pred (s3: cseq e) pcl,
        P s1 -> P s2 -> P s3 -> P (Cseq pc (Csmerge2 c rs s1 s2 pred s3) pcl).
    Hypothesis Hsmerge1 : forall {e} pc c rs s1 pred (s3: cseq e) pcl,
        P s1 -> P s3 -> P (Cseq pc (Csmerge1 c rs s1 pred s3) pcl).

    Lemma cseq_ind2 : forall {e} (s: cseq e), P s.
  End cseq_ind2.

  Definition cseq_pc {e} (cs : cseq e) :=
    let '(Cseq pc _ _) := cs in pc.

  Definition cseq_last {e} (cs : cseq e) :=
    let '(Cseq _ _ pc) := cs in pc.

  Variable abort : node.

Backward specification

  Inductive in_cseq : forall {e}, node -> instruction -> cseq e -> Prop :=
  | in_einstr : forall pc i pcl, in_cseq pc i (Cseq pc (Ceinstr i) pcl)
  | in_ereturn : forall pc i pcl, in_cseq pc i (Cseq pc (Cereturn i) pcl)
  | in_econd_1 : forall pc c rs pred s1 s2 pcl,
      in_cseq pc (Icond c rs (cseq_pc s1) (cseq_pc s2) pred) (Cseq pc (Cecond c rs s1 s2 pred) pcl)
  | in_econd_2 : forall pc i c rs pred s1 s2 pcf pcl,
      in_cseq pc i s1 -> in_cseq pc i (Cseq pcf (Cecond c rs s1 s2 pred) pcl)
  | in_econd_3 : forall pc i c rs pred s1 s2 pcf pcl,
      in_cseq pc i s2 -> in_cseq pc i (Cseq pcf (Cecond c rs s1 s2 pred) pcl)
  | in_ejumptable : forall pc r pcs pcl, in_cseq pc (Ijumptable r pcs) (Cseq pc (Cejumptable r pcs) pcl)
  | in_ecatch : forall pc pcl, in_cseq pc (Inop abort) (Cseq pc Cecatch pcl)
  | in_sinstr_1 {e} : forall pc i (s: cseq e) pcl,
      in_cseq pc i (Cseq pc (Csinstr i s) pcl)
  | in_sinstr_2 {e} : forall pc i i' (s: cseq e) pcf pcl,
      in_cseq pc i s -> in_cseq pc i (Cseq pcf (Csinstr i' s) pcl)
  | in_smerge2_1 {e} : forall pc c rs pred s1 s2 (s: cseq e) pcl,
      in_cseq pc (Icond c rs (cseq_pc s1) (cseq_pc s2) pred) (Cseq pc (Csmerge2 c rs s1 s2 pred s) pcl)
  | in_smerge2_2 {e} : forall pc i c rs pred s1 s2 (s: cseq e) pcf pcl,
      in_cseq pc i s1 -> in_cseq pc i (Cseq pcf (Csmerge2 c rs s1 s2 pred s) pcl)
  | in_smerge2_3 {e} : forall pc i c rs pred s1 s2 (s: cseq e) pcf pcl,
      in_cseq pc i s2 -> in_cseq pc i (Cseq pcf (Csmerge2 c rs s1 s2 pred s) pcl)
  | in_smerge2_4 {e} : forall pc i c rs pred s1 s2 (s: cseq e) pcf pcl,
      in_cseq pc i s -> in_cseq pc i (Cseq pcf (Csmerge2 c rs s1 s2 pred s) pcl)
  | in_smerge1_1 {e} : forall pc c rs pred s1 (s: cseq e) pcl,
      in_cseq pc (Icond c rs (cseq_pc s1) (cseq_pc s) pred) (Cseq pc (Csmerge1 c rs s1 pred s) pcl)
  | in_smerge1_2 {e} : forall pc i c rs pred s1 (s: cseq e) pcf pcl,
      in_cseq pc i s1 -> in_cseq pc i (Cseq pcf (Csmerge1 c rs s1 pred s) pcl)
  | in_smerge1_4 {e} : forall pc i c rs pred s1 (s: cseq e) pcf pcl,
      in_cseq pc i s -> in_cseq pc i (Cseq pcf (Csmerge1 c rs s1 pred s) pcl).

  Local Hint Constructors in_cseq : rtlcm.

  Lemma cseq_pc_in : forall {e} (s : cseq e),
      exists i, in_cseq (cseq_pc s) i s.

  Inductive spec_mode :=
  | NoPred
  | Pred.

  Inductive wf_cseq m : forall {e}, cseq e -> Prop :=
  | wf_einstr : forall pcf i pcl, wf_cseq m (Cseq pcf (Ceinstr i) pcl)
  | wf_ereturn : forall pcf i pcl, wf_cseq m (Cseq pcf (Cereturn i) pcl)
  | wf_econd : forall pcf c rs seq1 seq2 pred pcl,
      (forall i, ~in_cseq pcf i seq1) ->
      (forall i, ~in_cseq pcf i seq2) ->
      (forall pc i1 i2, in_cseq pc i1 seq1 -> in_cseq pc i2 seq2 -> False) ->
      (m = Pred -> forall pc1 i1, in_cseq pc1 i1 seq1 -> ~In (cseq_pc seq1) (successors_instr i1)) ->
      (m = Pred -> forall pc1 i1, in_cseq pc1 i1 seq2 -> ~In (cseq_pc seq2) (successors_instr i1)) ->
      (m = Pred -> forall pc1 i1, in_cseq pc1 i1 seq1 -> forall pc2 i2, In pc2 (successors_instr i1) -> ~in_cseq pc2 i2 seq2) ->
      (m = Pred -> forall pc1 i1, in_cseq pc1 i1 seq2 -> forall pc2 i2, In pc2 (successors_instr i1) -> ~in_cseq pc2 i2 seq1) ->
      wf_cseq m seq1 -> wf_cseq m seq2 ->
      wf_cseq m (Cseq pcf (Cecond c rs seq1 seq2 pred) pcl)
  | wf_ejumptable : forall pcf r pcs pcl,
      wf_cseq m (Cseq pcf (Cejumptable r pcs) pcl)
  | wf_ecatch : forall pcf pcl,
      wf_cseq m (Cseq pcf Cecatch pcl)
  | wf_sinstr {e} : forall pcf i (seq: cseq e) pcl,
      (m = Pred -> successors_instr i = [cseq_pc seq]) ->
      (forall i, ~in_cseq pcf i seq) ->
      (m = Pred -> forall pc1 i1, in_cseq pc1 i1 seq -> ~In (cseq_pc seq) (successors_instr i1)) ->
      wf_cseq m seq ->
      wf_cseq m (Cseq pcf (Csinstr i seq) pcl)
  | wf_smerge2 {e} : forall pcf c rs seq1 seq2 pred (seq: cseq e) pcl,
      (forall i, ~in_cseq pcf i seq1) ->
      (forall i, ~in_cseq pcf i seq2) ->
      (forall i, ~in_cseq pcf i seq) ->
      (forall pc i1 i2, in_cseq pc i1 seq1 -> in_cseq pc i2 seq2 -> False) ->
      (forall pc i1 i2, in_cseq pc i1 seq1 -> in_cseq pc i2 seq -> False) ->
      (forall pc i1 i2, in_cseq pc i1 seq2 -> in_cseq pc i2 seq -> False) ->
      (m = Pred -> forall pc1 i1, in_cseq pc1 i1 seq1 -> ~In (cseq_pc seq1) (successors_instr i1)) ->
      (m = Pred -> forall pc1 i1, in_cseq pc1 i1 seq2 -> ~In (cseq_pc seq2) (successors_instr i1)) ->
      (m = Pred -> forall pc1 i1, in_cseq pc1 i1 seq -> ~In (cseq_pc seq) (successors_instr i1)) ->
      (m = Pred -> forall pc1 i1, in_cseq pc1 i1 seq1 -> forall pc2 i2, In pc2 (successors_instr i1) -> ~in_cseq pc2 i2 seq2) ->
      (m = Pred -> forall pc1 i1, in_cseq pc1 i1 seq2 -> forall pc2 i2, In pc2 (successors_instr i1) -> ~in_cseq pc2 i2 seq1) ->
      (m = Pred -> forall pc1 i1, in_cseq pc1 i1 seq -> forall pc2 i2, In pc2 (successors_instr i1) -> ~in_cseq pc2 i2 seq1) ->
      (m = Pred -> forall pc1 i1, in_cseq pc1 i1 seq -> forall pc2 i2, In pc2 (successors_instr i1) -> ~in_cseq pc2 i2 seq2) ->
      (m = Pred -> forall pc1 i1, in_cseq pc1 i1 seq1 -> forall pc2 i2, In pc2 (successors_instr i1) -> in_cseq pc2 i2 seq -> pc2 = cseq_pc seq) ->
      (m = Pred -> forall pc1 i1, in_cseq pc1 i1 seq2 -> forall pc2 i2, In pc2 (successors_instr i1) -> in_cseq pc2 i2 seq -> pc2 = cseq_pc seq) ->
      (m = Pred -> forall pc1 i1, in_cseq pc1 i1 seq1 -> In (cseq_pc seq) (successors_instr i1) -> pc1 = cseq_last seq1) ->
      (m = Pred -> forall pc1 i1, in_cseq pc1 i1 seq2 -> In (cseq_pc seq) (successors_instr i1) -> pc1 = cseq_last seq2) ->
      wf_cseq m seq1 -> wf_cseq m seq2 -> wf_cseq m seq ->
      wf_cseq m (Cseq pcf (Csmerge2 c rs seq1 seq2 pred seq) pcl)
  | wf_smerge1 {e} : forall pcf c rs seq1 pred (seq: cseq e) pcl,
      (forall i, ~in_cseq pcf i seq1) ->
      (forall i, ~in_cseq pcf i seq) ->
      (forall pc i1 i2, in_cseq pc i1 seq1 -> in_cseq pc i2 seq -> False) ->
      (m = Pred -> forall pc1 i1, in_cseq pc1 i1 seq1 -> ~In (cseq_pc seq1) (successors_instr i1)) ->
      (m = Pred -> forall pc1 i1, in_cseq pc1 i1 seq -> ~In (cseq_pc seq) (successors_instr i1)) ->
      (m = Pred -> forall pc1 i1, in_cseq pc1 i1 seq -> forall pc2 i2, In pc2 (successors_instr i1) -> ~in_cseq pc2 i2 seq1) ->
      (m = Pred -> forall pc1 i1, in_cseq pc1 i1 seq1 -> forall pc2 i2, In pc2 (successors_instr i1) -> in_cseq pc2 i2 seq -> pc2 = cseq_pc seq) ->
      (m = Pred -> forall pc1 i1, in_cseq pc1 i1 seq1 -> In (cseq_pc seq) (successors_instr i1) -> False) ->
      wf_cseq m seq1 -> wf_cseq m seq ->
      wf_cseq m (Cseq pcf (Csmerge1 c rs seq1 pred seq) pcl).

End cseq.

Ltac inv_in_cseq :=
  match goal with
  | H: in_cseq _ _ _ (Cseq _ (Ceinstr _) _) |- _ => inv H
  | H: in_cseq _ _ _ (Cseq _ (Cereturn _) _) |- _ => inv H
  | H: in_cseq _ _ _ (Cseq _ (Cecond _ _ _ _ _) _) |- _ => inv H
  | H: in_cseq _ _ _ (Cseq _ (Cejumptable _ _) _) |- _ => inv H
  | H: in_cseq _ _ _ (Cseq _ Cecatch _) |- _ => inv H
  | H: in_cseq _ _ _ (Cseq _ (Csinstr _ _) _) |- _ => inv H
  | H: in_cseq _ _ _ (Cseq _ (Csmerge2 _ _ _ _ _ _) _) |- _ => inv H
  | H: in_cseq _ _ _ (Cseq _ (Csmerge1 _ _ _ _ _) _) |- _ => inv H
  end; try inv_existT_eq.

Concretize a sequence of instructions

Section conc_seq.
  Variable abort : node.

Concretization function

  Fixpoint concretize_seq {e} (pc : node) (s : seqinstr e) : cont e -> mon (cseq e) :=
    match s in seqinstr e return cont e -> mon (cseq e) with
    | Seinstr i =>
        fun k => match k with
              | COneExit next => ret (Cseq pc (Ceinstr (i next)) pc)
              end
    | Sereturn i => fun k => ret (Cseq pc (Cereturn i) pc)
    | Second c rs seq1 seq2 pred =>
        fun k => match k with
              | CTwoExits next1 next2 =>
                  doM pc1 <- fresh_pc;
                  doM pc2 <- fresh_pc;
                  doM cseq1 <- concretize_seq pc1 seq1 (COneExit next1);
                  doM cseq2 <- concretize_seq pc2 seq2 (COneExit next2);
                  ret (Cseq pc (Cecond c rs cseq1 cseq2 pred) pc)
              end
    | Sejumptable r =>
        fun k => match k with CNExits pcs => ret (Cseq pc (Cejumptable r pcs) pc) end
    | Secatch => fun k => ret (Cseq pc Cecatch pc)
    | Ssinstr i seq1 =>
        fun k =>
          doM pc1 <- fresh_pc;
          doM cseq1 <- concretize_seq pc1 seq1 k;
          ret (Cseq pc (Csinstr (i pc1) cseq1) (cseq_last cseq1))
    | Ssmerge2 c rs seq1 seq2 pred seq3 =>
        fun k =>
          doM pc1 <- fresh_pc;
          doM pc2 <- fresh_pc;
          doM pc3 <- fresh_pc;
          doM cseq1 <- concretize_seq pc1 seq1 (COneExit pc3);
          doM cseq2 <- concretize_seq pc2 seq2 (COneExit pc3);
          doM cseq3 <- concretize_seq pc3 seq3 k;
          ret (Cseq pc (Csmerge2 c rs cseq1 cseq2 pred cseq3) (cseq_last cseq3))
    | Ssmerge1 c rs seq1 pred seq3 =>
        fun k =>
          doM pc1 <- fresh_pc;
          doM pc2 <- fresh_pc;
          doM pc3 <- fresh_pc;
          doM cseq1 <- concretize_seq pc1 seq1 CNoExit;
          doM cseq3 <- concretize_seq pc3 seq3 k;
          ret (Cseq pc (Csmerge1 c rs cseq1 pred cseq3) (cseq_last cseq3))
    end.

Concretization relation

  Inductive concretized : forall {e}, node -> seqinstr e -> cont e -> cseq e -> Prop :=
  | conc_einstr : forall pc i next,
      concretized pc (Seinstr i) (COneExit next) (Cseq pc (Ceinstr (i next)) pc)
  | conc_ereturn : forall pc i,
      concretized pc (Sereturn i) CNoExit (Cseq pc (Cereturn i) pc)
  | conc_econd : forall pc c rs seq1 seq2 pred pc1 pc2 next1 next2 cseq1 cseq2,
      concretized pc1 seq1 (COneExit next1) cseq1 ->
      concretized pc2 seq2 (COneExit next2) cseq2 ->
      concretized pc (Second c rs seq1 seq2 pred) (CTwoExits next1 next2)
        (Cseq pc (Cecond c rs cseq1 cseq2 pred) pc)
  | conc_ejumptable : forall pc r pcs,
      concretized pc (Sejumptable r) (CNExits pcs) (Cseq pc (Cejumptable r pcs) pc)
  | conc_ecatch : forall pc,
      concretized pc Secatch CNoExit (Cseq pc Cecatch pc)
  | conc_sinstr {e} : forall pc i seq (k: cont e) pc1 cseq,
      concretized pc1 seq k cseq ->
      concretized pc (Ssinstr i seq) k (Cseq pc (Csinstr (i pc1) cseq) (cseq_last cseq))
  | conc_smerge2 {e} : forall pc c rs seq1 seq2 pred seq3 (k: cont e) pc1 pc2 next cseq1 cseq2 cseq3,
      concretized pc1 seq1 (COneExit next) cseq1 ->
      concretized pc2 seq2 (COneExit next) cseq2 ->
      concretized next seq3 k cseq3 ->
      concretized pc (Ssmerge2 c rs seq1 seq2 pred seq3) k
        (Cseq pc (Csmerge2 c rs cseq1 cseq2 pred cseq3) (cseq_last cseq3))
  | conc_smerge1 {e} : forall pc c rs seq1 pred seq3 (k: cont e) pc1 next cseq1 cseq3,
      concretized pc1 seq1 CNoExit cseq1 ->
      concretized next seq3 k cseq3 ->
      concretized pc (Ssmerge1 c rs seq1 pred seq3) k
        (Cseq pc (Csmerge1 c rs cseq1 pred cseq3) (cseq_last cseq3)).

Correctness

  Lemma concretize_seq_correct : forall {e} (s: seqinstr e) pc k cs st st' sincr,
      concretize_seq pc s k st = R cs st' sincr ->
      concretized pc s k cs.

  Ltac concretize_seq_specialize :=
    match goal with
    | IHs: (forall _, _ -> _ -> _) |- _ =>
        specialize (IHs _ eq_refl JMeq_refl)
    | IHs: (forall _ _ _ _ _ _, concretize_seq _ _ _ _ = R _ _ _ -> _),
        H:concretize_seq _ _ _ _ = R _ _ _ |- _ => specialize (IHs _ _ _ _ _ _ H)
    end.

  Lemma concretize_seq_preserves : forall {e} (s: seqinstr e) pc k cs st st' sincr,
      concretize_seq pc s k st = R cs st' sincr ->
      forall pc i, (st_code st)!pc = Some i <-> (st_code st')!pc = Some i.

  Lemma concretize_seq_in_inv : forall {e} (s: seqinstr e) pcf k cs st st' sincr,
      concretize_seq pcf s k st = R cs st' sincr ->
      forall pc i, in_cseq abort pc i cs -> pc = pcf \/ st_nextnode st <= pc < st_nextnode st'.

  Fact concretize_seq_cseq_pc : forall {e} (s: seqinstr e) pcf k cs st st' sincr,
      concretize_seq pcf s k st = R cs st' sincr ->
      cseq_pc cs = pcf.

  Ltac concretize_seq_successors_inv :=
    repeat
      match goal with
      | _ => concretize_seq_specialize
      | k: cont _ |- _ => dependent destruction k; [idtac]
      | _ => monadInv
      | H: successors_instr _ = _ |- _ => rewrite H in *
      | H: forall _, successors_instr _ = _ |- _ => rewrite H in *
      | H: _ \/ _ |- _ => destruct H; subst
      | H: _ /\ _ |- _ => destruct H; subst
      | H: False |- _ => inv H
      | I: wf_seq _ -> _, H:wf_seq _ |- _ => specialize (I H)
      | I: (forall _ _, in_cseq _ _ _ _ -> _), H: in_cseq _ _ _ _ |- _ => specialize (I _ _ H)
      | I: (forall _, In _ _ -> _), H: In _ _ |- _ => specialize (I _ H)
      | _ => extlia
      | _ => inv_wf_seq
      | _ => inv_in_cseq
      | _ => inv_existT_eq
      | _ => inv_is_cont
      | _ => erewrite concretize_seq_cseq_pc; [|eauto]
      | _ => simpl in *; eauto with rtlcm
      end.

  Lemma concretize_seq_successors_inv : forall {e} (s: seqinstr e) pcf k cs st st' sincr,
      concretize_seq pcf s k st = R cs st' sincr ->
      wf_seq s ->
      forall pc i, in_cseq abort pc i cs ->
              forall pc1,
                In pc1 (successors_instr i) ->
                ((e = OneExit -> pc = cseq_last cs) /\ is_cont k pc1) \/ st_nextnode st <= pc1 < st_nextnode st' \/ pc1 = abort.

  Lemma concretize_seq_wf {m} : forall {e} (s: seqinstr e) pcf k cs st st' sincr,
      concretize_seq pcf s k st = R cs st' sincr ->
      pcf < st_nextnode st ->
      abort < st_nextnode st ->
      (m = Pred -> forall pc, is_cont k pc -> pc < st_nextnode st) ->
      (m = Pred -> wf_seq s) ->
      wf_cseq abort m cs.

End conc_seq.

Global Hint Constructors in_cseq : rtlcm.
Global Hint Resolve cseq_pc_in : rtlcm.

Add a sequence of instructions into the CFG

Section add_seq.

  Variable abort : node.

  Fixpoint add_seq {e} (s : cseq e) : mon unit :=
    match s with
    | Cseq pc (Ceinstr i) _ => set_instr pc i
    | Cseq pc (Cereturn i) _ => set_instr pc i
    | Cseq pc (Cecond c rs seq1 seq2 pred) _ =>
        doM tt <- set_instr pc (Icond c rs (cseq_pc seq1) (cseq_pc seq2) pred);
        doM tt <- add_seq seq1;
        doM tt <- add_seq seq2;
        ret tt
    | Cseq pc (Cejumptable r pcs) _ =>
        set_instr pc (Ijumptable r pcs)
    | Cseq pc Cecatch _ => set_instr pc (Inop abort)
    | Cseq pc (Csinstr i seq) _ =>
        doM tt <- set_instr pc i;
        add_seq seq
    | Cseq pc (Csmerge2 c rs seq1 seq2 pred seq) _ =>
        doM tt <- set_instr pc (Icond c rs (cseq_pc seq1) (cseq_pc seq2) pred);
        doM tt <- add_seq seq1;
        doM tt <- add_seq seq2;
        add_seq seq
    | Cseq pc (Csmerge1 c rs seq1 pred seq) _ =>
        doM tt <- set_instr pc (Icond c rs (cseq_pc seq1) (cseq_pc seq) pred);
        doM tt <- add_seq seq1;
        add_seq seq
    end.

Specification generator

  Fixpoint spec_cseq {e} (Pnode : node -> Prop) (m : spec_mode) (code : code) (s : cseq e) : Prop :=
    match s with
    | Cseq pc (Ceinstr i) _ =>
        code!pc = Some i
    | Cseq pc (Cereturn i) _ => code!pc = Some i
    | Cseq pc (Cecond c rs seq1 seq2 pred) _ =>
        code!pc = Some (Icond c rs (cseq_pc seq1) (cseq_pc seq2) pred)
        /\ (m = Pred -> one_predecessor code (cseq_pc seq1) pc)
        /\ (m = Pred -> one_predecessor code (cseq_pc seq2) pc)
        /\ spec_cseq Pnode m code seq1
        /\ spec_cseq Pnode m code seq2
        /\ Pnode (cseq_pc seq1) /\ Pnode (cseq_pc seq2)
    | Cseq pc (Cejumptable r pcs) _ =>
        code!pc = Some (Ijumptable r pcs)
    | Cseq pc Cecatch _ => code!pc = Some (Inop abort)
    | Cseq pc (Csinstr i seq) _ =>
        code!pc = Some i
        /\ (m = Pred -> one_predecessor code (cseq_pc seq) pc)
        /\ spec_cseq Pnode m code seq
        /\ Pnode (cseq_pc seq)
    | Cseq pc (Csmerge2 c rs seq1 seq2 pred seq) _ =>
        code!pc = Some (Icond c rs (cseq_pc seq1) (cseq_pc seq2) pred)
        /\ (m = Pred -> one_predecessor code (cseq_pc seq1) pc)
        /\ (m = Pred -> one_predecessor code (cseq_pc seq2) pc)
        /\ spec_cseq Pnode m code seq1
        /\ spec_cseq Pnode m code seq2
        /\ (m = Pred -> two_predecessors code (cseq_pc seq) (cseq_last seq1) (cseq_last seq2))
        /\ spec_cseq Pnode m code seq
        /\ Pnode (cseq_pc seq1) /\ Pnode (cseq_pc seq2) /\ Pnode (cseq_pc seq)
    | Cseq pc (Csmerge1 c rs seq1 pred seq) _ =>
        code!pc = Some (Icond c rs (cseq_pc seq1) (cseq_pc seq) pred)
        /\ (m = Pred -> one_predecessor code (cseq_pc seq1) pc)
        /\ (m = Pred -> one_predecessor code (cseq_pc seq) pc)
        /\ spec_cseq Pnode m code seq1
        /\ spec_cseq Pnode m code seq
        /\ Pnode (cseq_pc seq1) /\ Pnode (cseq_pc seq)
    end.

  Definition spec_seq {e} code pc (seq: seqinstr e) cont :=
    exists cseq, concretized pc seq cont cseq /\ spec_cseq (fun _ => True) NoPred code cseq.

Properties

  Inductive nodup_cont : forall {e}, cont e -> Prop :=
  | ndContNo : nodup_cont CNoExit
  | ndContOne : forall pc, nodup_cont (COneExit pc)
  | ndContTwo : forall pc1 pc2, pc1 <> pc2 -> nodup_cont (CTwoExits pc1 pc2)
  | ndContN : forall pcs, list_norepet pcs -> nodup_cont (CNExits pcs).

  Ltac inv_nodup_cont :=
    match goal with
    | H:nodup_cont CNoExit |- _ => inv H
    | H:nodup_cont (COneExit _) |- _ => inv H
    | H:nodup_cont (CTwoExits _ _) |- _ => inv H
    | H:nodup_cont (CNExits _) |- _ => inv H
    end.

  Lemma is_predecessor_code : forall code1 code2 pc1 pc2,
      is_predecessor code1 pc1 pc2 ->
      (forall i, In pc2 (successors_instr i) -> code1!pc1 = Some i -> code2!pc1 = Some i) ->
      is_predecessor code2 pc1 pc2.

  Corollary one_predecessor_code : forall code1 code2 pc1 pc2,
      one_predecessor code1 pc1 pc2 ->
      (forall i, In pc1 (successors_instr i) -> forall pc, code2!pc = Some i -> code1!pc = Some i) ->
      one_predecessor code2 pc1 pc2.

  Corollary two_predecessors_code : forall code1 code2 pc1 pc2 pc3,
      two_predecessors code1 pc1 pc2 pc3 ->
      (forall i, In pc1 (successors_instr i) -> forall pc, code2!pc = Some i -> code1!pc = Some i) ->
      two_predecessors code2 pc1 pc2 pc3.

  Lemma spec_cseq_code {e} : forall (P: node -> Prop) m code1 code2 (s: cseq e),
      spec_cseq P m code1 s ->
      (forall pc i, in_cseq abort pc i s -> code1!pc = Some i -> code2!pc = Some i) ->
      (m = Pred -> forall pc1 i, In pc1 (successors_instr i) -> P pc1 -> (exists i, in_cseq abort pc1 i s) -> forall pc, code2!pc = Some i -> code1!pc = Some i) ->
      spec_cseq P m code2 s.

  Lemma spec_cseq_implies {e} : forall (P1 P2: node -> Prop) m code (s: cseq e),
      spec_cseq P1 m code s ->
      (forall x, P1 x -> P2 x) ->
      spec_cseq P2 m code s.

Correctness

  Lemma add_seq_preserves {e} : forall (s : cseq e) tt st st' sincr,
      add_seq s st = R tt st' sincr ->
      forall pc i,
        (forall pc' i', in_cseq abort pc' i' s -> pc <> pc') ->
        (st_code st)!pc = Some i <->
        (st_code st')!pc = Some i.

  Local Ltac my_split :=
    repeat
      match goal with
      | |- exists _, _ => esplit
      | |- _ <= _ < _ => idtac
      | |- _ /\ _ => split
      end.

  Lemma add_seq_inv {e} : forall (s: cseq e) tt st st' sincr,
      add_seq s st = R tt st' sincr ->
      forall pc i, (st_code st')!pc = Some i ->
              in_cseq abort pc i s
              \/ ((st_code st)!pc = Some i /\ (forall i, ~in_cseq abort pc i s)).

  Lemma add_seq_correct Pnode {e} : forall (s : cseq e) m tt st st' sincr,
      add_seq s st = R tt st' sincr ->
      wf_cseq abort m s ->
      (m = Pred -> forall pc i, (st_code st)!pc = Some i -> forall pc2 i2, In pc2 (successors_instr i) -> in_cseq abort pc2 i2 s -> pc2 = cseq_pc s) ->
      (forall pc i, in_cseq abort pc i s -> pc = cseq_pc s \/ Pnode pc) ->
      spec_cseq Pnode m (st_code st') s.

End add_seq.

Backward spec

Definition spec_seq_inv {e} Pnode abort code pc i pcf (seq : seqinstr e) (k : cont e) :=
  exists cseq,
    concretized pcf seq k cseq
    /\ in_cseq abort pc i cseq
    /\ spec_cseq abort Pnode Pred code cseq.

Full node transformation

Definition add_abort_blk :=
  doM pc <- fresh_pc;
  doM di <- set_instr pc (Ibuiltin EF_cm_catch [] BR_none pc);
  ret pc.

Definition add_prologue abort (s : seqinstr OneExit) entry :=
  doM pc <- fresh_pc;
  doM cs <- concretize_seq pc s (COneExit entry);
  doM tt <- add_seq abort cs;
  ret pc.

Total transformation

Section total.
  Variable prologue : seqinstr OneExit.

  Variable transf_nop : node -> node -> seqinstr OneExit.
  Variable transf_op : node -> operation -> list reg -> reg -> node -> seqinstr OneExit.
  Variable transf_load : node -> trapping_mode -> memory_chunk -> addressing -> list reg -> reg -> node -> seqinstr OneExit.
  Variable transf_store : node -> memory_chunk -> addressing -> list reg -> reg -> node -> seqinstr OneExit.
  Variable transf_call : node -> signature -> reg + qualident -> list reg -> reg -> node -> seqinstr OneExit.
  Variable transf_tailcall : node -> signature -> reg + qualident -> list reg -> seqinstr NoExit.
  Variable transf_builtin : node -> external_function -> list (builtin_arg reg) -> builtin_res reg -> node -> seqinstr OneExit.
  Variable transf_cond : node -> condition -> list reg -> node -> node -> option bool -> seqinstr TwoExits.
  Variable transf_jumptable : node -> reg -> list node -> seqinstr NExits.
  Variable transf_return : node -> option reg -> seqinstr NoExit.

Rewrite a single instruction

  Definition transf_instr pc i : (sigT (fun e => (seqinstr e * cont e)%type)) :=
    match i with
    | Inop pc1 | Iassert _ _ pc1 => (existT _ _ (transf_nop pc pc1, COneExit pc1))
    | Iop op rs r pc1 => (existT _ _ (transf_op pc op rs r pc1, COneExit pc1))
    | Iload trap chk addr rs r pc1 => (existT _ _ (transf_load pc trap chk addr rs r pc1, COneExit pc1))
    | Istore chk addr rs r pc1 => (existT _ _ (transf_store pc chk addr rs r pc1, COneExit pc1))
    | Icall sig ros rs r pc1 => (existT _ _ (transf_call pc sig ros rs r pc1, COneExit pc1))
    | Itailcall sig ros rs => (existT _ _ (transf_tailcall pc sig ros rs, CNoExit))
    | Ibuiltin ef rs r pc1 => (existT _ _ (transf_builtin pc ef rs r pc1, COneExit pc1))
    | Icond c rs pc1 pc2 o => (existT _ _ (transf_cond pc c rs pc1 pc2 o, CTwoExits pc1 pc2))
    | Ijumptable r pcs => (existT _ _ (transf_jumptable pc r pcs, CNExits pcs))
    | Ireturn r => (existT _ _ (transf_return pc r, CNoExit))
    end.

Rewrite the whole code

  Definition ptree_mfold {A: Type} (f: positive -> A -> mon unit) (t: PTree.t A): mon unit :=
    PTree.fold (fun s1 k v => bind s1 (fun _ => f k v)) t (ret tt).

  Lemma ptree_mfold_rec {A} f m_final st (P : PTree.t A -> state -> Prop) :
    (forall m m' a, (forall x, m ! x = m' ! x) -> P m a -> P m' a) ->
    P (PTree.empty _) st ->
    (forall m pc i st1,
        sincr st st1 ->
        m!pc = None ->
        m_final!pc = Some i ->
        P m st1 ->
        P (PTree.set pc i m) (proj_st (f pc i st1))) ->
    P m_final (proj_st (@ptree_mfold A f m_final st)).

  Definition transf_code abort :=
    ptree_mfold
      (fun pc i =>
         let '(existT _ _ (seq, cont)) := transf_instr pc i in
         doM cs <- concretize_seq pc seq cont;
         add_seq abort cs).

  Definition transf_function (f : function) :=
    let initstate := mkstate (Pos.succ (max_pc_function f)) (PTree.empty _) in
    let res := (doM abort <- add_abort_blk;
                doM dummy <- transf_code abort (fn_code f);
                add_prologue abort prologue (fn_entrypoint f)) initstate in
    ((proj_st res).(st_code), proj_val res).


  Lemma transf_code_preserves abort : forall code tt st st' sincr,
      transf_code abort code st = R tt st' sincr ->
      forall pcl i,
        (forall pc i, code!pc = Some i -> pc < pcl) ->
        pcl < (st_nextnode st) ->
        (st_code st)!pcl = Some i ->
        (st_code st')!pcl = Some i.

  Lemma transf_code_correct abort : forall code tt st st' sincr,
      transf_code abort code st = R tt st' sincr ->
      (forall pc i, code!pc = Some i -> pc < st_nextnode st) ->
      (forall pc i, (st_code st)!pc = Some i -> pc < st_nextnode st) ->
      (abort < st_nextnode st) ->
      (forall pc i,
        code!pc = Some i ->
        forall x seq cont,
          transf_instr pc i = existT _ x (seq, cont) ->
          exists cseq,
            concretized pc seq cont cseq
            /\ (forall pc' i, in_cseq abort pc' i cseq -> pc' = pc \/ st_nextnode st <= pc')
            /\ spec_cseq abort (fun _ : node => True) NoPred (st_code st') cseq)
      /\ (forall pc i, (st_code st')!pc = Some i -> pc < st_nextnode st').

  Lemma transf_function_entry : forall f code entry,
      transf_function f = (code, entry) ->
      exists abort, spec_seq abort code entry prologue (COneExit (fn_entrypoint f)).

  Lemma transf_function_correct : forall f code entry,
      transf_function f = (code, entry) ->
      forall pc i,
        (fn_code f)!pc = Some i ->
        let '(existT _ _ (seq, cont)) := transf_instr pc i in
        exists abort,
          spec_seq abort code pc seq cont
          /\ code!abort = Some (Ibuiltin EF_cm_catch [] BR_none abort).

Backward spec

  Hypothesis WF_PROLOGUE : wf_seq prologue.
  Hypothesis WF_NOP : forall pc pc1, wf_seq (transf_nop pc pc1).
  Hypothesis WF_OP : forall pc op rs r pc1, wf_seq (transf_op pc op rs r pc1).
  Hypothesis WF_LOAD : forall pc trp chk addr rs r pc1, wf_seq (transf_load pc trp chk addr rs r pc1).
  Hypothesis WF_STORE : forall pc chk addr rs r pc1, wf_seq (transf_store pc chk addr rs r pc1).
  Hypothesis WF_CALL : forall pc sig ros rs r pc1, wf_seq (transf_call pc sig ros rs r pc1).
  Hypothesis WF_TAILCALL : forall pc sig ros rs, wf_seq (transf_tailcall pc sig ros rs).
  Hypothesis WF_BUILTIN : forall pc ef rs r pc1, wf_seq (transf_builtin pc ef rs r pc1).
  Hypothesis WF_COND : forall pc c rs pc1 pc2 pred, wf_seq (transf_cond pc c rs pc1 pc2 pred).
  Hypothesis WF_JUMPTABLE : forall pc r pcs, wf_seq (transf_jumptable pc r pcs).
  Hypothesis WF_RETURN : forall pc r, wf_seq (transf_return pc r).

  Lemma transf_instr_wf_seq : forall pc i e s c,
      transf_instr pc i = existT _ e (s, c) ->
      wf_seq s.

  Lemma transf_instr_cont_succ : forall pc i e s c,
      transf_instr pc i = existT _ e (s, c) ->
      forall pc, is_cont c pc -> In pc (successors_instr i).

  Fact transf_code_successors_ge : forall abort f env tt st st' sincr,
      transf_code abort (fn_code f) st = R tt st' sincr ->
      wt_function f env ->
      max_pc_function f < st_nextnode st ->
      abort < st_nextnode st ->
      (forall pc i, (st_code st)!pc = Some i -> forall pc2, In pc2 (successors_instr i) -> pc2 < st_nextnode st) ->
      (forall pc1 i, (st_code st')!pc1 = Some i -> forall pc2, In pc2 (successors_instr i) -> pc2 < st_nextnode st').

  Lemma transf_code_inv : forall abort f env tt st st' sincr,
      transf_code abort (fn_code f) st = R tt st' sincr ->
      wt_function f env ->
      (max_pc_function f < st_nextnode st) ->
      (forall pc i, (fn_code f)!pc = Some i -> pc < st_nextnode st) ->
      (forall pc i, (st_code st)!pc = Some i -> pc < st_nextnode st) ->
      (forall pc i, (st_code st)!pc = Some i -> forall pc2, In pc2 (successors_instr i) -> pc2 < st_nextnode st) ->
      (max_pc_function f < abort < st_nextnode st) ->
      (forall pc i,
          (st_code st')!pc = Some i ->
          (exists pcf i' e (s: seqinstr e) k cseq,
              (fn_code f)!pcf = Some i'
              /\ transf_instr pcf i' = existT _ e (s, k)
              /\ pcf <= max_pc_function f
              /\ concretized pcf s k cseq
              /\ (forall pc' i, in_cseq abort pc' i cseq -> pc' = pcf \/ st_nextnode st <= pc' < st_nextnode st')
              /\ in_cseq abort pc i cseq
              /\ spec_cseq abort (fun pc => st_nextnode st <= pc < st_nextnode st') Pred (st_code st') cseq)
          \/ (st_code st)!pc = Some i)
      /\ (forall pc i, (st_code st')!pc = Some i -> pc < st_nextnode st')
      /\ (forall pc1 i, (st_code st')!pc1 = Some i -> forall pc2, In pc2 (successors_instr i) -> pc2 < st_nextnode st').

  Lemma transf_function_inv env : forall f code entry,
      transf_function f = (code, entry) ->
      wt_function f env ->
      forall pc i,
        code!pc = Some i ->
        exists abort,
          code!abort = Some (Ibuiltin EF_cm_catch [] BR_none abort)
          /\ let spec_seq_inv {e} := @spec_seq_inv e (fun pc => pc <> entry) abort code in
            spec_seq_inv pc i entry prologue (COneExit (fn_entrypoint f))
            \/ (exists pcf pcl, ((fn_code f)!pcf = Some (Inop pcl) \/ exists cond args, (fn_code f)!pcf = Some (Iassert cond args pcl)) /\ spec_seq_inv pc i pcf (transf_nop pcf pcl) (COneExit pcl))
            \/ (exists op rs r pcf pcl, (fn_code f)!pcf = Some (Iop op rs r pcl) /\ spec_seq_inv pc i pcf (transf_op pcf op rs r pcl) (COneExit pcl))
            \/ (exists trp chk addr rs r pcf pcl, (fn_code f)!pcf = Some (Iload trp chk addr rs r pcl) /\ spec_seq_inv pc i pcf (transf_load pcf trp chk addr rs r pcl) (COneExit pcl))
            \/ (exists chk addr rs r pcf pcl, (fn_code f)!pcf = Some (Istore chk addr rs r pcl) /\ spec_seq_inv pc i pcf (transf_store pcf chk addr rs r pcl) (COneExit pcl))
            \/ (exists sig ros rs r pcf pcl, (fn_code f)!pcf = Some (Icall sig ros rs r pcl) /\ spec_seq_inv pc i pcf (transf_call pcf sig ros rs r pcl) (COneExit pcl))
            \/ (exists sig ros rs pcf, (fn_code f)!pcf = Some (Itailcall sig ros rs) /\ spec_seq_inv pc i pcf (transf_tailcall pcf sig ros rs) CNoExit)
            \/ (exists ef rs r pcf pcl, (fn_code f)!pcf = Some (Ibuiltin ef rs r pcl) /\ spec_seq_inv pc i pcf (transf_builtin pcf ef rs r pcl) (COneExit pcl))
            \/ (exists c rs pc1 pc2 pred pcf, (fn_code f)!pcf = Some (Icond c rs pc1 pc2 pred) /\ spec_seq_inv pc i pcf (transf_cond pcf c rs pc1 pc2 pred) (CTwoExits pc1 pc2))
            \/ (exists r pcs pcf, (fn_code f)!pcf = Some (Ijumptable r pcs) /\ spec_seq_inv pc i pcf (transf_jumptable pcf r pcs) (CNExits pcs))
            \/ (exists r pcf, (fn_code f)!pcf = Some (Ireturn r) /\ spec_seq_inv pc i pcf (transf_return pcf r) CNoExit)
            \/ (i = Ibuiltin EF_cm_catch [] BR_none abort).
End total.

Global Hint Unfold spec_seq in_seq spec_seq_inv : rtlcm.

Default total transfer functions

Definition transf_nop_default (_ : node) (_ : node) := Seinstr Inop.
Definition transf_op_default (_ : node) op rs r (_ : node) := Seinstr (Iop op rs r).
Definition transf_load_default (_ : node) trp chk addr rs r (_ : node) := Seinstr (Iload trp chk addr rs r).
Definition transf_store_default (_ : node) chk addr rs r (_ : node) := Seinstr (Istore chk addr rs r).
Definition transf_call_default (_ : node) sig ros rs r (_ : node) := Seinstr (Icall sig ros rs r).
Definition transf_tailcall_default (_ : node) sig ros rs := Sereturn (Itailcall sig ros rs).
Definition transf_builtin_default (_ : node) ef rs r (_ : node) := Seinstr (Ibuiltin ef rs r).
Definition transf_cond_default (_ : node) c rs (_ _ : node) pred := Second c rs (Seinstr Inop) (Seinstr Inop) pred.
Definition transf_jumptable_default (_ : node) r (_ : list node) := Sejumptable r.
Definition transf_return_default (_ : node) r := Sereturn (Ireturn r).

Global Hint Unfold
  transf_nop_default transf_op_default transf_load_default transf_store_default
  transf_call_default transf_tailcall_default transf_builtin_default
  transf_cond_default transf_jumptable_default transf_return_default : rtlcm.

Transformation that completely replace the body of the function

Section replace.
  Variable body : seqinstr NoExit.

  Definition transf_replace_function (f : function) :=
    let initstate := mkstate (Pos.succ (fn_entrypoint f)) (PTree.empty _) in
    let res := (doM abort <- add_abort_blk;
                doM cs <- concretize_seq (fn_entrypoint f) body CNoExit;
                add_seq abort cs) initstate in
    (proj_st res).(st_code).

  Lemma transf_replace_function_entry : forall f,
      exists abort, spec_seq abort (transf_replace_function f) (fn_entrypoint f) body CNoExit.

Backward spec

  Hypothesis WF_BODY : wf_seq body.

  Lemma transf_replace_function_inv env : forall f code,
      transf_replace_function f = code ->
      wt_function f env ->
      forall pc i,
        code!pc = Some i ->
        exists abort,
          code!abort = Some (Ibuiltin EF_cm_catch [] BR_none abort)
          /\ (spec_seq_inv (fun pc => pc <> fn_entrypoint f) abort code pc i (fn_entrypoint f) body CNoExit
             \/ (i = Ibuiltin EF_cm_catch [] BR_none abort)).
End replace.

Partial transformation

Section partial.
  Variable prologue : seqinstr OneExit.

  Variable transf_nop : node -> Errors.res (seqinstr OneExit).
  Variable transf_op : operation -> list reg -> reg -> node -> Errors.res (seqinstr OneExit).
  Variable transf_load : trapping_mode -> memory_chunk -> addressing -> list reg -> reg -> node -> Errors.res (seqinstr OneExit).
  Variable transf_store : memory_chunk -> addressing -> list reg -> reg -> node -> Errors.res (seqinstr OneExit).
  Variable transf_call : signature -> reg + qualident -> list reg -> reg -> node -> Errors.res (seqinstr OneExit).
  Variable transf_tailcall : signature -> reg + qualident -> list reg -> Errors.res (seqinstr NoExit).
  Variable transf_builtin : external_function -> list (builtin_arg reg) -> builtin_res reg -> node -> Errors.res (seqinstr OneExit).
  Variable transf_cond : condition -> list reg -> node -> node -> option bool -> Errors.res (seqinstr TwoExits).
  Variable transf_jumptable : reg -> list node -> Errors.res (seqinstr NExits).
  Variable transf_return : option reg -> Errors.res (seqinstr NoExit).

  Open Scope error_monad_scope.

Rewrite a single instruction

  Definition transf_partial_instr i : Errors.res (sigT (fun e => (seqinstr e * cont e)%type)) :=
    match i with
    | Inop pc | Iassert _ _ pc =>
        do seq <- transf_nop pc; OK (existT _ _ (seq, COneExit pc))
    | Iop op rs r pc =>
        do seq <- transf_op op rs r pc; OK (existT _ _ (seq, COneExit pc))
    | Iload trap chk addr rs r pc =>
        do seq <- transf_load trap chk addr rs r pc; OK (existT _ _ (seq, COneExit pc))
    | Istore chk addr rs r pc =>
        do seq <- transf_store chk addr rs r pc; OK (existT _ _ (seq, COneExit pc))
    | Icall sig ros rs r pc =>
        do seq <- transf_call sig ros rs r pc; OK (existT _ _ (seq, COneExit pc))
    | Itailcall sig ros rs =>
        do seq <- transf_tailcall sig ros rs; OK (existT _ _ (seq, CNoExit))
    | Ibuiltin ef rs r pc =>
        do seq <- transf_builtin ef rs r pc; OK (existT _ _ (seq, COneExit pc))
    | Icond c rs pc1 pc2 o =>
        do seq <- transf_cond c rs pc1 pc2 o; OK (existT _ _ (seq, CTwoExits pc1 pc2))
    | Ijumptable r pcs =>
        do seq <- transf_jumptable r pcs; OK (existT _ _ (seq, CNExits pcs))
    | Ireturn r =>
        do seq <- transf_return r; OK (existT _ _ (seq, CNoExit))
    end.

Rewrite the whole code

  Definition transf_partial_code abort :=
    ptree_pmfold
      (fun pc i st =>
         match transf_partial_instr i with
         | OK (existT _ _ (seq, cont)) =>
             OK (bind (concretize_seq pc seq cont) (add_seq abort) st)
         | Error e => Error e
         end).

  Close Scope error_monad_scope.

  Definition transf_partial_function (f : function) :=
    let initstate := mkstate (Pos.succ (max_pc_function f)) (PTree.empty _) in
    Errors.bind
      (pbind
         (fun st => Errors.OK (add_abort_blk st))
         (fun abort =>
            pbind (transf_partial_code abort (fn_code f))
              (fun _ st => Errors.OK (add_prologue abort prologue (fn_entrypoint f) st))
         ) initstate)
      (fun '(R val st _) => OK (st.(st_code), val)).


  Lemma transf_partial_code_preserves abort : forall code tt st st' sincr,
      transf_partial_code abort code st = OK (R tt st' sincr) ->
      forall pcl i,
        (forall pc i, code!pc = Some i -> pc < pcl) ->
        pcl < (st_nextnode st) ->
        (st_code st)!pcl = Some i ->
        (st_code st')!pcl = Some i.

  Lemma transf_partial_code_correct abort : forall code tt st st' sincr,
      (forall pc i, code!pc = Some i -> pc < st_nextnode st) ->
      (forall pc i, (st_code st)!pc = Some i -> pc < st_nextnode st) ->
      (abort < st_nextnode st) ->
      transf_partial_code abort code st = OK (R tt st' sincr) ->
      (forall pc i,
        code!pc = Some i ->
        exists e (seq: seqinstr e) cont cseq,
          transf_partial_instr i = OK (existT _ e (seq, cont))
          /\ concretized pc seq cont cseq
          /\ (forall pc' i, in_cseq abort pc' i cseq -> pc' = pc \/ st_nextnode st <= pc')
          /\ spec_cseq abort (fun _ : node => True) NoPred (st_code st') cseq)
      /\ (forall pc i, (st_code st')!pc = Some i -> pc < st_nextnode st').

  Lemma transf_partial_function_entry : forall f code entry,
      transf_partial_function f = OK (code, entry) ->
      exists abort,
        spec_seq abort code entry prologue (COneExit (fn_entrypoint f))
        /\ code!abort = Some (Ibuiltin EF_cm_catch [] BR_none abort).

  Lemma transf_partial_function_correct : forall f code entry,
      transf_partial_function f = OK (code, entry) ->
      forall pc i,
        (fn_code f)!pc = Some i ->
        exists e seq cont abort,
          transf_partial_instr i = OK (existT _ e (seq, cont))
          /\ spec_seq abort code pc seq cont
          /\ code!abort = Some (Ibuiltin EF_cm_catch [] BR_none abort).


  Hypothesis WF_PROLOGUE : wf_seq prologue.
  Hypothesis WF_NOP : forall pc s, transf_nop pc = OK s -> wf_seq s.
  Hypothesis WF_OP : forall op rs r pc s, transf_op op rs r pc = OK s -> wf_seq s.
  Hypothesis WF_LOAD : forall trp chk addr rs r pc s, transf_load trp chk addr rs r pc = OK s -> wf_seq s.
  Hypothesis WF_STORE : forall chk addr rs r pc s, transf_store chk addr rs r pc = OK s -> wf_seq s.
  Hypothesis WF_CALL : forall sig ros rs r pc s, transf_call sig ros rs r pc = OK s -> wf_seq s.
  Hypothesis WF_TAILCALL : forall sig ros rs s, transf_tailcall sig ros rs = OK s -> wf_seq s.
  Hypothesis WF_BUILTIN : forall ef rs r pc s, transf_builtin ef rs r pc = OK s -> wf_seq s.
  Hypothesis WF_COND : forall c rs pc1 pc2 pred s, transf_cond c rs pc1 pc2 pred = OK s -> wf_seq s.
  Hypothesis WF_JUMPTABLE : forall r pcs s, transf_jumptable r pcs = OK s -> wf_seq s.
  Hypothesis WF_RETURN : forall r s, transf_return r = OK s -> wf_seq s.

  Lemma transf_partial_instr_wf_seq : forall i e s c,
      transf_partial_instr i = OK (existT _ e (s, c)) ->
      wf_seq s.

  Lemma transf_partial_instr_cont_succ : forall i e s c,
      transf_partial_instr i = OK (existT _ e (s, c)) ->
      forall pc, is_cont c pc -> In pc (successors_instr i).

  Fact transf_partial_code_successors_ge : forall abort f env tt st st' sincr,
      transf_partial_code abort (fn_code f) st = OK (R tt st' sincr) ->
      wt_function f env ->
      max_pc_function f < st_nextnode st ->
      abort < st_nextnode st ->
      (forall pc i, (st_code st)!pc = Some i -> forall pc2, In pc2 (successors_instr i) -> pc2 < st_nextnode st) ->
      (forall pc1 i, (st_code st')!pc1 = Some i -> forall pc2, In pc2 (successors_instr i) -> pc2 < st_nextnode st').

  Lemma transf_partial_code_inv : forall abort f env tt st st' sincr,
      transf_partial_code abort (fn_code f) st = OK (R tt st' sincr) ->
      wt_function f env ->
      (max_pc_function f < st_nextnode st) ->
      (forall pc i, (fn_code f)!pc = Some i -> pc < st_nextnode st) ->
      (forall pc i, (st_code st)!pc = Some i -> pc < st_nextnode st) ->
      (forall pc i, (st_code st)!pc = Some i -> forall pc2, In pc2 (successors_instr i) -> pc2 < st_nextnode st) ->
      (max_pc_function f < abort < st_nextnode st) ->
      (forall pc i,
          (st_code st')!pc = Some i ->
          (exists pcf i' e (s: seqinstr e) k cseq,
              (fn_code f)!pcf = Some i'
              /\ transf_partial_instr i' = OK (existT _ e (s, k))
              /\ pcf <= max_pc_function f
              /\ concretized pcf s k cseq
              /\ (forall pc' i, in_cseq abort pc' i cseq -> pc' = pcf \/ st_nextnode st <= pc' < st_nextnode st')
              /\ in_cseq abort pc i cseq
              /\ spec_cseq abort (fun pc => st_nextnode st <= pc < st_nextnode st') Pred (st_code st') cseq)
          \/ (st_code st)!pc = Some i)
      /\ (forall pc i, (st_code st')!pc = Some i -> pc < st_nextnode st')
      /\ (forall pc1 i, (st_code st')!pc1 = Some i -> forall pc2, In pc2 (successors_instr i) -> pc2 < st_nextnode st').

  Lemma transf_partial_function_inv env : forall f code entry,
      transf_partial_function f = OK (code, entry) ->
      wt_function f env ->
      forall pc i,
        code!pc = Some i ->
        exists abort,
          code!abort = Some (Ibuiltin EF_cm_catch [] BR_none abort)
          /\ let spec_seq_inv {e} := @spec_seq_inv e (fun pc => pc <> entry) abort code in
            spec_seq_inv pc i entry prologue (COneExit (fn_entrypoint f))
            \/ (exists pcf pcl s, ((fn_code f)!pcf = Some (Inop pcl) \/ exists cond args, (fn_code f)!pcf = Some (Iassert cond args pcl)) /\ transf_nop pcl = OK s /\ spec_seq_inv pc i pcf s (COneExit pcl))
            \/ (exists op rs r pcf pcl s, (fn_code f)!pcf = Some (Iop op rs r pcl) /\ transf_op op rs r pcl = OK s /\ spec_seq_inv pc i pcf s (COneExit pcl))
            \/ (exists trp chk addr rs r pcf pcl s, (fn_code f)!pcf = Some (Iload trp chk addr rs r pcl) /\ transf_load trp chk addr rs r pcl = OK s /\ spec_seq_inv pc i pcf s (COneExit pcl))
            \/ (exists chk addr rs r pcf pcl s, (fn_code f)!pcf = Some (Istore chk addr rs r pcl) /\ transf_store chk addr rs r pcl = OK s /\ spec_seq_inv pc i pcf s (COneExit pcl))
            \/ (exists sig ros rs r pcf pcl s, (fn_code f)!pcf = Some (Icall sig ros rs r pcl) /\ transf_call sig ros rs r pcl = OK s /\ spec_seq_inv pc i pcf s (COneExit pcl))
            \/ (exists sig ros rs pcf s, (fn_code f)!pcf = Some (Itailcall sig ros rs) /\ transf_tailcall sig ros rs = OK s /\ spec_seq_inv pc i pcf s CNoExit)
            \/ (exists ef rs r pcf pcl s, (fn_code f)!pcf = Some (Ibuiltin ef rs r pcl) /\ transf_builtin ef rs r pcl = OK s /\ spec_seq_inv pc i pcf s (COneExit pcl))
            \/ (exists c rs pc1 pc2 pred pcf s, (fn_code f)!pcf = Some (Icond c rs pc1 pc2 pred) /\ transf_cond c rs pc1 pc2 pred = OK s /\ spec_seq_inv pc i pcf s (CTwoExits pc1 pc2))
            \/ (exists r pcs pcf s, (fn_code f)!pcf = Some (Ijumptable r pcs) /\ transf_jumptable r pcs = OK s /\ spec_seq_inv pc i pcf s (CNExits pcs))
            \/ (exists r pcf s, (fn_code f)!pcf = Some (Ireturn r) /\ transf_return r = OK s /\ spec_seq_inv pc i pcf s CNoExit)
            \/ (i = Ibuiltin EF_cm_catch [] BR_none abort).
End partial.

Default partial transfer functions

Definition transf_partial_nop_default (_ : node) := Errors.OK (Seinstr Inop).
Definition transf_partial_op_default op rs r (_ : node) := Errors.OK (Seinstr (Iop op rs r)).
Definition transf_partial_load_default trp chk addr rs r (_ : node) := Errors.OK (Seinstr (Iload trp chk addr rs r)).
Definition transf_partial_store_default chk addr rs r (_ : node) := Errors.OK (Seinstr (Istore chk addr rs r)).
Definition transf_partial_call_default sig ros rs r (_ : node) := Errors.OK (Seinstr (Icall sig ros rs r)).
Definition transf_partial_tailcall_default sig ros rs := Errors.OK (Sereturn (Itailcall sig ros rs)).
Definition transf_partial_builtin_default ef rs r (_ : node) := Errors.OK (Seinstr (Ibuiltin ef rs r)).
Definition transf_partial_cond_default c rs (_ _ : node) pred := Errors.OK (Second c rs (Seinstr Inop) (Seinstr Inop) pred).
Definition transf_partial_jumptable_default r (_ : list node) := Errors.OK (Sejumptable r).
Definition transf_partial_return_default r := Errors.OK (Sereturn (Ireturn r)).

Global Hint Unfold
  transf_partial_nop_default transf_partial_op_default transf_partial_load_default transf_partial_store_default
  transf_partial_call_default transf_partial_tailcall_default transf_partial_builtin_default
  transf_partial_cond_default transf_partial_jumptable_default transf_partial_return_default : rtlcm.

Tactics and notations

Opaque transf_function.

Ltac inv_seq :=
  repeat
    match goal with
    | H: exists (pc : node), _ |- _ => destruct H as (?pc&?)
    | H: exists _, _ |- _ => destruct H as (?&?)
    | H: _ /\ _ |- _ => destruct H
    | H: (_, _) = (_, _) |- _ => inv H
    | H: existT _ ?e _ = existT _ ?e _ |- _ =>
        apply Eqdep.EqdepTheory.inj_pair2 in H; subst; simpl in *
    | H: existT _ _ _ = existT _ _ _ |- _ =>
        apply EqdepFacts.eq_sigT_fst in H as ?; subst
    | H: concretized _ _ _ _ |- _ => inv H; [idtac]
    | _ => autounfold with rtlcm in *
    end.

Ltac inv_transf_function :=
  repeat
    match goal with
    | H: _ \/ _ |- _ => destruct H
    | H: ?p = ?p -> _ |- _ => specialize (H eq_refl)
    | _ => congruence
    | _ => now (eauto 12)
    | _ => pMonadInv
    | _ => inv_in_cseq
    | _ => inv_seq
    end.

Tactic Notation "plus_step" int_or_var(n) :=
  do n (try (eapply Smallstep.plus_left'; [| |eauto using Events.E0_left])).

Notation "i ;; seq" := ((i : seqinstr _ -> seqinstr _) seq) (at level 15, right associativity).

Helpers for proof of security

Require Import Globalenvs Events.
Require Import Smallstep RTL RTLfault.

Section protected_multi_step.

Variable tprog : program.
Let tge := Genv.globalenv tprog.
Variable f : fault.

Hypothesis protected_fault_step : forall st0 t0 st1 st2,
  RTL.initial_state tprog st0 ->
  star step tge st0 t0 st1 ->
  fstep tge (Valid st1) [Event_fault f] st2 ->
  gets_caught tprog st2
  \/ (exists (st' : RTL.state) (t' : trace),
        star fstep tge st2 t' (Valid st') /\ nofault t' /\ star step tge st1 t' st').

Lemma protected_multi_step: forall st0 st1 st2 t1 t2,
    RTL.initial_state tprog st0 ->
    star step tge st0 t1 st1 ->
    star fstep tge (Valid st1) t2 st2 ->
    last_event_is_fault f t2 ->
    gets_caught tprog st2
    \/ (exists st' t',
          star fstep tge st2 t' (Valid st')
          /\ nofault t'
          /\ star step tge st1 (ignore_faults t2 ** t') st').

End protected_multi_step.