Module BTL_AnalysisLib

Require Import ZArith List Maps Coqlib Lattice Smallstep.
Require Import AST BTL Registers Op.
Require Import Linking IPass Values Integers Memory Events Globalenvs.
Require Import AnalysisDomain.
Require RTL ValueDomain.
Require Kildall MultiFixpoint.

Section BINARY_TREE.

Inductive binary_tree (A : Type) :=
| binary_tree_leaf : A -> binary_tree A
| binary_tree_split : binary_tree A -> binary_tree A -> binary_tree A.
Global Arguments binary_tree_leaf {A}.
Global Arguments binary_tree_split {A}.

Fixpoint binary_tree_fold {A B : Type} (f : A -> B -> B)
         (tr : binary_tree A) (b0 : B) :=
  match tr with
  | binary_tree_leaf a => f a b0
  | binary_tree_split l r =>
      binary_tree_fold f l (binary_tree_fold f r b0)
  end.

Fixpoint apply_at_leaves {A B : Type} (f : A -> binary_tree B)
         (tree : binary_tree A) :=
  match tree with
  | binary_tree_leaf a => f a
  | binary_tree_split l r =>
    binary_tree_split (apply_at_leaves f l) (apply_at_leaves f r)
  end.

Fixpoint match_tree {A : Type} (P : A -> Prop) (tr : binary_tree A) :=
  match tr with
  | binary_tree_leaf l => P l
  | binary_tree_split l r =>
      match_tree P l \/ match_tree P r
  end.

Fixpoint flatten_outcomes_rec
           { T : Type} (t : binary_tree (list T)) (already : list T) : list T :=
  match t with
  | binary_tree_leaf l => List.rev_append l already
  | binary_tree_split l r =>
      flatten_outcomes_rec l (flatten_outcomes_rec r already)
  end.

Lemma In_rev_append:
  forall {T} l1 l2 x, In (x : T) (List.rev_append l1 l2) <-> In x l1 \/ In x l2.

Lemma apply_match_tree:
  forall {A B : Type} (P : A -> Prop) (Q : B -> Prop) (f : A -> binary_tree B)
         (MAP : forall x, P x -> match_tree Q (f x))
         tr
         (EX : match_tree P tr),
    match_tree Q (apply_at_leaves f tr).
    
Lemma In_binary_tree_flatten_outcomes_rec :
  forall { T : Type }
         (t : binary_tree (list T))
         (already : list T)
         (x : T),
      In x (flatten_outcomes_rec t already) <->
         match_tree (In x) t \/ In x already.

Definition flatten_outcomes
           { T : Type} (t : binary_tree (list T)) :=
  flatten_outcomes_rec t nil.

Lemma In_binary_tree_flatten_outcomes :
  forall { T : Type }
         (t : binary_tree (list T))
         (x : T),
      In x (flatten_outcomes t) <->
         match_tree (In x) t.

Definition In_tree {T : Type} (l0 : T) : binary_tree T -> Prop :=
  match_tree (fun l => l = l0).

End BINARY_TREE.


Module BTL_IRspec <: IRspec.
  Definition function := BTL.function.
  Definition node := RTL.node.
  Definition fn_stacksize := BTL.fn_stacksize.
  Definition fn_params := BTL.fn_params.
  Definition funsig := BTL.funsig.
End BTL_IRspec.

Module BTL_AbstractAnalysis (D : AADomain BTL_IRspec).
  Include D.

  Module DS := MultiFixpoint.Solver(Kildall.NodeSetForward)(D.VA).

Definition outcome := (VA.t * (option final))%type.
Definition outcomes := binary_tree outcome.

Definition apply_on_outcomes (f : astate -> outcomes):=
  apply_at_leaves
  (fun (oc : outcome) =>
     let (s, final) := oc in
     match filter_astate s with
     | None => binary_tree_leaf oc
     | Some s =>
         match final with
         | Some _ => binary_tree_leaf oc
         | None => f s
         end
     end).

Fixpoint transfer_iblock (pi: prog_info) (ib : iblock) (s : astate) : outcomes :=
  match ib with
  | BF fi _ => binary_tree_leaf (Astate s, Some fi)
  | Bnop _ => binary_tree_leaf (Astate s, None)
  | Bop op args res _ =>
      binary_tree_leaf (transfer_op pi op args res s, None)
  | Bload trap chunk addr args dst _ =>
      binary_tree_leaf (transfer_load pi trap chunk addr args dst s, None)
  | Bstore chunk addr args src _ =>
      binary_tree_leaf (transfer_store pi chunk addr args src s, None)
  | Bseq b1 b2 =>
      apply_on_outcomes (transfer_iblock pi b2)
                        (transfer_iblock pi b1 s)
  | Bcond cond args ifso ifnot _ =>
      let (sso, snot) := transfer_condition pi cond args s in
      match filter_astate sso, filter_astate snot with
      | None, None => binary_tree_leaf (VA.bot, None)
      | Some sso, None => transfer_iblock pi ifso sso
      | None, Some snot => transfer_iblock pi ifnot snot
      | Some sso, Some snot =>
          binary_tree_split (transfer_iblock pi ifso sso)
                            (transfer_iblock pi ifnot snot)
      end
  end.

Definition final_outcome := (exit * VA.t)%type.
Definition final_outcomes := binary_tree (list final_outcome).

Definition transfer_final (pi: prog_info) (fi : final) (s : astate): list final_outcome :=
  match fi with
  | Bgoto exit => (exit, Astate s) :: nil
  | Breturn arg => nil
  | Bcall sig reg_ident args res exit =>
      (exit, transfer_call pi args res s) :: nil
  | Btailcall sig reg_ident args => nil
  | Bbuiltin ef args res exit =>
      (exit, transfer_builtin pi ef args res s) :: nil
  | Bjumptable arg exits =>
      mapi (fun i exit => (exit, transfer_jumpi pi arg (Int.repr i) s)) exits
  end.

Definition transfer_block (pi: prog_info) (ib : iblock) (s : astate): final_outcomes :=
  apply_at_leaves
    (fun (oc : outcome) =>
       let (s, ofi) := oc in
       binary_tree_leaf
         (match ofi with
          | Some fi =>
              match filter_astate s with
              | None => nil
              | Some s => transfer_final pi fi s
              end
          | None => nil
          end))
    (transfer_iblock pi ib s).

Definition flat_transfer_block (pi: prog_info) (ibi : iblock_info) (s : astate) : list final_outcome :=
   flatten_outcomes (transfer_block pi ibi.(entry) s).

Definition transfer (pi: prog_info) (co : code) (n : positive) (va : VA.t) : list final_outcome :=
  match filter_astate va with
  | None => nil
  | Some s =>
      match PTree.get n co with
      | Some ibi => flat_transfer_block pi ibi s
      | None => nil
      end
  end.

Definition analyze (pi : prog_info) (f : function) : PMap.t D.VA.t :=
  match
    DS.solution_opt (widen_node f)
                    (transfer pi f.(fn_code))
                    ((f.(fn_entrypoint), entry_state f)::nil)
  with
  | Some solution => solution
  | None => PMap.init default_top
  end.

Section SOUNDNESS.


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'.

Section ANALYSIS.

Lemma transfer_strict pi co n:
  transfer pi co n VA.bot = nil.

Lemma analyze_successor [pi f n s ibi n' s']
  (ANALYZE : (analyze pi f)!!n = Astate s)
  (AT : f.(fn_code)!n = Some ibi)
  (IN : In (n', s') (flat_transfer_block pi ibi s)):
  VA.ge (analyze pi f)!!n' s'.

Lemma analyze_entrypoint [pi ge gh sp e m f s0]
  (ENTRY: entry_state f = Astate s0)
  (MATCH: asmatch pi ge gh sp e m s0):
  exists s1,
    (analyze pi f)!!(fn_entrypoint f) = Astate s1 /\
    asmatch pi ge gh sp e m s1.

Lemma analyze_succ [pi ge gh sp e m f n s0 ibi n' s1]
  (ANALYZE : (analyze pi f)!!n = Astate s0)
  (AT : f.(fn_code)!n = Some ibi)
  (IN : In (n', Astate s1) (flat_transfer_block pi ibi s0))
  (MATCH : asmatch pi ge gh sp e m s1):
  exists s2,
     (analyze pi f)!!n' = Astate s2 /\
     asmatch pi ge gh sp e m s2.

End ANALYSIS.

Section ISTEP.
Variable pi: prog_info.
Variable ge: genv.
Variable gh: ghost_env.
Variable sp: block.

Local Notation amatch := (asmatch pi ge gh sp).

Definition match_outcomes e m (ofi : option final) : outcomes -> Prop :=
  match_tree
    (fun l : outcome =>
       let (s, ofi') := l in
       match filter_astate s with
       | Some s => amatch e m s /\ ofi = ofi'
       | None => False
       end).

Lemma match_outcomes_iff_exists e m ofi tr:
  match_outcomes e m ofi tr <->
  exists s,
    In_tree (Astate s, ofi) tr /\ amatch e m s.

Lemma match_apply_on_outcomes1 oc1 f2 e1 m1 fi1
    (MATCH1 : match_outcomes e1 m1 (Some fi1) oc1):
    match_outcomes e1 m1 (Some fi1) (apply_on_outcomes f2 oc1).

Lemma match_apply_on_outcomes2 oc1 f2 e1 m1 e2 m2 ofi2
    (MATCH1 : match_outcomes e1 m1 None oc1)
    (MATCH2 : forall s1, amatch e1 m1 s1 ->
                match_outcomes e2 m2 ofi2 (f2 s1)):
    match_outcomes e2 m2 ofi2 (apply_on_outcomes f2 oc1).

Lemma transfer_iblock_correct gh0 ib e m e' m' ofi
  (STEP : iblock_istep AnnotTrap ge (Vptr sp Ptrofs.zero) gh0 e m ib e' m' ofi):
  forall s (MATCH : amatch e m s),
    match_outcomes e' m' ofi (transfer_iblock pi ib s) /\
    succ_state pi ge sp gh m gh m'.

End ISTEP.

Section STEP.
Variable pi: prog_info.
Variable ge: genv.

Local Notation amatch := (asmatch pi ge).

Inductive sound_stack : ghost_env -> list stackframe -> mem -> block -> Prop :=
  | sound_stack_nil
        gh m bound:
        sound_stack gh nil m bound
  | sound_stack_call
        gh res f sp pc e stk m bound
        (MATCH : forall gh_ce1 m' vres
                   (VRS : valid_returnstate pi ge gh_ce1 m' vres)
                   (SUCC : succ_state pi ge bound gh m gh_ce1 m'),
                 exists aa gh1,
                   (analyze pi f) !! pc = Astate aa /\
                   amatch gh1 sp (e#res <- vres) m' aa /\
                   sound_stack gh1 stk m' sp):
        sound_stack gh (Stackframe res f (Vptr sp Ptrofs.zero) pc e :: stk) m bound.

Inductive sound_state_base (gh : ghost_env) : state -> Prop :=
  | sound_regular_state
        stk f sp pc e m _bc aa
        (STK : sound_stack gh stk m sp)
        (AN : (analyze pi f)!!pc = Astate aa)
        (MATCH : amatch gh sp e m aa):
      sound_state_base gh (State stk f (Vptr sp Ptrofs.zero) pc e m _bc)
  | sound_call_state
        stk fd args m _bc
        (STK : sound_stack gh stk m (Mem.nextblock m))
        (VCS : valid_callstate pi ge gh m args):
      sound_state_base gh (Callstate stk fd args m _bc)
  | sound_return_state
        stk v m bound _bc
        (STK : sound_stack gh stk m bound)
        (VRS : valid_returnstate pi ge gh m v):
      sound_state_base gh (Returnstate stk v m _bc).

Lemma sound_stack_succ_imp [gh gh' stk m m' bound bound']
  (STACK : sound_stack gh stk m bound)
  (IMP : forall gh1 m1, succ_state pi ge bound' gh' m' gh1 m1 -> succ_state pi ge bound gh m gh1 m1):
  sound_stack gh' stk m' bound'.

Lemma sound_stack_succ [gh gh' stk m m' bound]
  (SUCC : succ_state pi ge bound gh m gh' m')
  (STACK : sound_stack gh stk m bound):
  sound_stack gh' stk m' bound.


Lemma sound_succ_state gh pc s0 ibi s1 stk f sp pc' e' m' _bc
  (ANALYZE : (analyze pi f)!!pc = Astate s0)
  (AT : f.(fn_code)!pc = Some ibi)
  (IN : In (pc', Astate s1) (flat_transfer_block pi ibi s0))
  (MATCH : amatch gh sp e' m' s1)
  (STACK : sound_stack gh stk m' sp):
  sound_state_base gh (State stk f (Vptr sp Ptrofs.zero) pc' e' m' _bc).

Lemma propagate_to_final ib fin s0 s1 x
    (MID : match_tree (fun l : outcome => l = (Astate s1, Some fin))
                      (transfer_iblock pi (entry ib) s0))
    (END : In x (transfer_final pi fin s1)):
    In x (flat_transfer_block pi ib s0).


Definition final_preserv_gh (f : final) : bool :=
  match f with
  | Bgoto _ | Bjumptable _ _ => true
  | _ => false
  end.

Lemma sound_step_base_exec_iblock gh0 stack f sp pc rs m _bc0 _bc2 trace gh ib rs' m' fin st'
  (SOUND: sound_state_base gh (State stack f sp pc rs m _bc0))
  (PC: (fn_code f) ! pc = Some ib)
  (ISTEP: iblock_istep AnnotTrap ge sp gh0 rs m (entry ib) rs' m' (Some fin))
  (FINAL: final_step ge stack f sp rs' m' _bc2 fin trace st'):
  if final_preserv_gh fin
  then sound_state_base gh st'
  else exists gh', sound_state_base gh' st'.

Theorem sound_step_base st t st' gh
  (STEP: BTL.step AnnotTrap ge st t st')
  (SOUND: sound_state_base gh st):
  exists gh', sound_state_base gh' st'.

End STEP.

Section PROGRAM.
Variable prog: program.
Let ge := Genv.globalenv prog.

Inductive sound_state (st : state) : Prop :=
  | sound_state_intro
      (SOUND: forall cunit, linkorder cunit prog -> exists gh, sound_state_base (get_prog_info cunit) ge gh st).

Remark sound_state_inv st cunit:
  sound_state st -> linkorder cunit prog -> exists bc, sound_state_base (get_prog_info cunit) ge bc st.

Theorem sound_initial st
  (INIT : initial_state prog st):
  sound_state st.

Theorem sound_step st t st'
  (STEP : BTL.step AnnotTrap ge st t st')
  (SOUND : sound_state st):
  sound_state st'.

End PROGRAM.

End SOUNDNESS.

End BTL_AbstractAnalysis.



Module Type BTL_AADomain_Annotate.
  Include AADomain BTL_IRspec.


  Parameter unreachable_inst_promotable : operation + condition -> list reg -> inst_promotion_info.
  Parameter unreachable_addr_aval : option ValueDomain.aval.

  Parameter op_inst_promotable : prog_info -> astate -> operation -> list reg -> inst_promotion_info.
  Parameter cond_inst_promotable : prog_info -> astate -> condition -> list reg -> inst_promotion_info.
  Parameter get_addr_aval : prog_info -> astate -> addressing -> list reg -> option ValueDomain.aval.

  Axiom op_inst_promotable_correct : forall pi ge gh sp rs m aa op prom args
    (MATCH : asmatch pi ge gh sp rs m aa)
    (PROM : op_inst_promotable pi aa op args = IPromotableOp prom)
    (ALIVE : eval_operation ge (Vptr sp Ptrofs.zero) op rs##args m <> None),
    adp_op_promotable ge (Vptr sp Ptrofs.zero) m op prom rs##args.
  
  Axiom cond_inst_promotable_correct : forall pi ge gh sp rs m aa cond prom args
    (MATCH : asmatch pi ge gh sp rs m aa)
    (PROM : cond_inst_promotable pi aa cond args = IPromotableCond prom)
    (ALIVE : eval_condition cond rs##args m <> None),
    adp_cond_promotable m cond prom rs##args.

  Axiom get_addr_aval_correct : forall pi ge gh sp rs m aa addr args aaddr a
    (MATCH : asmatch pi ge gh sp rs m aa)
    (AADDR : get_addr_aval pi aa addr args = Some aaddr)
    (EVAL : eval_addressing ge (Vptr sp Ptrofs.zero) addr rs##args = Some a),
    ValueDomain.vmatch gh a aaddr.

End BTL_AADomain_Annotate.

Module BTL_AnnotateAnalysis (D : BTL_AADomain_Annotate).
  Include D.
  Module AA := BTL_AbstractAnalysis D.
  Import IntPromotionCommon.

Definition combine_inst_promotion_info (iprom0 iprom1 : inst_promotion_info) : inst_promotion_info :=
  if match iprom1 with
     | IPromotableOp (mk_op_prom_ceq (mk_op_prom None None _ _) _ _)
     | IPromotableCond (mk_cond_prom_ceq (mk_cond_prom None None) _)
     | IPromNone
          => false
     | _ => true
     end
  then iprom1 else iprom0.

Lemma combine_inst_promotion_info_either iprom0 iprom1:
  let iprom := combine_inst_promotion_info iprom0 iprom1 in
  iprom = iprom0 \/ iprom = iprom1.
Global Opaque combine_inst_promotion_info.

Definition set_inst_promotion (iprom : inst_promotion_info) (ii : inst_info) : inst_info :=
  BTL.set_inst_promotion (combine_inst_promotion_info ii.(inst_promotion) iprom) ii.

Fixpoint transf_iblock_bot (ib : iblock) :=
  match ib with
  | BF _ _ | Bnop _ => ib
  | Bop op args dst iinfo =>
      Bop op args dst (set_inst_promotion (unreachable_inst_promotable (inl op) args) iinfo)
  | Bload trap chunk addr args dst iinfo =>
      Bload trap chunk addr args dst (set_addr_aval unreachable_addr_aval iinfo)
  | Bstore chunk addr args src iinfo =>
      Bstore chunk addr args src (set_addr_aval unreachable_addr_aval iinfo)
  | Bseq b1 b2 =>
      Bseq (transf_iblock_bot b1) (transf_iblock_bot b2)
  | Bcond cond args ifso ifnot iinfo =>
      Bcond cond args (transf_iblock_bot ifso) (transf_iblock_bot ifnot)
        (set_inst_promotion (unreachable_inst_promotable (inr cond) args) iinfo)
  end.

Fixpoint transf_iblock (pi: prog_info) (ib : iblock) (s : VA.t) {struct ib}:
  iblock * VA.t :=
  match filter_astate s with
  | None => (transf_iblock_bot ib, VA.bot)
  | Some aa =>
  match ib with
  | BF fi iinfo =>
      (ib, VA.bot)
  | Bnop iinfo =>
      (ib, Astate aa)
  | Bop op args res iinfo =>
      (Bop op args res (set_inst_promotion (op_inst_promotable pi aa op args) iinfo),
       transfer_op pi op args res aa)
  | Bload trap chunk addr args dst iinfo =>
      (Bload trap chunk addr args dst (set_addr_aval (get_addr_aval pi aa addr args) iinfo),
       transfer_load pi trap chunk addr args dst aa)
  | Bstore chunk addr args src iinfo =>
      (Bstore chunk addr args src (set_addr_aval (get_addr_aval pi aa addr args) iinfo),
       transfer_store pi chunk addr args src aa)
  | Bseq b1 b2 =>
      let (b1', s1) := transf_iblock pi b1 (Astate aa) in
      let (b2', s2) := transf_iblock pi b2 s1 in
      (Bseq b1' b2', s2)
  | Bcond cond args ifso ifnot iinfo =>
      let (s_ifso, s_ifnot) := transfer_condition pi cond args aa in
      let (ifso', s1) := transf_iblock pi ifso s_ifso in
      let (ifnot', s2) := transf_iblock pi ifnot s_ifnot in
      (Bcond cond args ifso' ifnot' (set_inst_promotion (cond_inst_promotable pi aa cond args) iinfo),
       VA.lub s1 s2)
  end end.

Definition transf_function (pi : prog_info) (f : function) : BTL.function :=
  let an := AA.analyze pi f in
  let code' := PTree.map (fun i ib =>
                    let ib' := fst (transf_iblock pi (entry ib) (an !! i)) in
                    mk_ibinfo ib' (binfo ib))
                  (fn_code f) in
  BTL.mkfunction (fn_sig f) (fn_params f) (fn_stacksize f) code' (fn_entrypoint f) (fn_gm f) (fn_info f).

Definition transf_fundef (pi : prog_info) (f : fundef) : fundef :=
  AST.transf_fundef (transf_function pi) f.

Definition transf_program (p : program) : BTL.program :=
  AST.transform_program (transf_fundef (get_prog_info p)) p.


Definition match_prog (p tp: program) :=
  match_program (fun cu f tf => tf = transf_fundef (get_prog_info cu) f) eq p tp.

Definition pass := mkpass match_prog.

Lemma transf_program_match p:
  match_prog p (transf_program p).

Section SOUNDNESS.

Section ISTEP.
Variable pi: prog_info.
Variable ge0 ge1 : genv.
Variable gh: ghost_env.
Variable sp: block.
Hypothesis PRESERVED: forall s : ident, Genv.find_symbol ge1 s = Genv.find_symbol ge0 s.

Local Notation amatch := (asmatch pi ge0 gh sp).

Lemma transf_iblock_correct gh0 ib aa e m e' m' ofi
  (MATCH : amatch e m aa)
  (STEP : iblock_istep AnnotTrap ge0 (Vptr sp Ptrofs.zero) gh0 e m ib e' m' ofi):
  let (ib', aa1) := transf_iblock pi ib (Astate aa) in
  (ofi = None -> exists aa1', aa1 = Astate aa1' /\ amatch e' m' aa1') /\
  iblock_istep AnnotTrap ge1 (Vptr sp Ptrofs.zero) gh e m ib' e' m' ofi.

End ISTEP.

Section PROGRAM.

Variable prog tprog: program.
Hypothesis TRANSL: match_prog prog tprog.

Let ge0 := Genv.globalenv prog.
Let ge1 := Genv.globalenv tprog.

Lemma ge_find_symbol (s : ident):
  Genv.find_symbol ge1 s = Genv.find_symbol ge0 s.
Local Hint Resolve ge_find_symbol : core.

Lemma ge_find_function (fp : reg + ident) rs f:
  find_function ge0 fp rs = Some f ->
  exists cunit,
    find_function ge1 fp rs = Some (transf_fundef (get_prog_info cunit) f) /\
    linkorder cunit prog.


Inductive match_stackframe: stackframe -> stackframe -> Prop :=
  | match_stackframe_intro
      sp res f pc rs cu
      (LINK: linkorder cu prog)
      : match_stackframe (BTL.Stackframe res f sp pc rs)
                         (BTL.Stackframe res (transf_function (get_prog_info cu) f) sp pc rs).

Definition match_stackframes : list stackframe -> list stackframe -> Prop :=
  list_forall2 match_stackframe.

Inductive match_states0 rm : state -> state -> Prop :=
  | match_states_norm stk stk' f pc sp rs m _bc bc
      (STACK: match_stackframes stk stk')
      : match_states0 rm (State stk f sp pc rs m _bc)
                         (State stk' (transf_function rm f) sp pc rs m bc)
  | match_states_call stk stk' f args m _bc bc
      (STACK: match_stackframes stk stk')
      : match_states0 rm (Callstate stk f args m _bc)
                         (Callstate stk' (transf_fundef rm f) args m bc)
  | match_states_return stk stk' v m _bc bc
      (STACK: match_stackframes stk stk')
      : match_states0 rm (Returnstate stk v m _bc)
                         (Returnstate stk' v m bc)
   .

Definition state_gh (s : state) : ghost_env :=
  match s with
  | State _ _ _ _ _ _ gh
  | Callstate _ _ _ _ gh
  | Returnstate _ _ _ gh
      => gh
  end.

Inductive match_states (st st' : state) : Prop :=
  match_states_intro
    (cu : program) (LINK: linkorder cu prog)
    (SOUND: AA.sound_state_base (get_prog_info cu) ge0 (state_gh st') st)
    (MATCH: match_states0 (get_prog_info cu) st st').

Lemma transfer_step st0 t st1 st0'
  (STEP : step AnnotTrap ge0 st0 t st1)
  (MATCH : match_states st0 st0')
  (OSOUND: AA.sound_state prog st0):
  exists st1',
    step AnnotTrap ge1 st0' t st1' /\ match_states st1 st1'.


Theorem transf_program_correct:
  forward_simulation (sem AnnotTrap prog) (sem AnnotTrap tprog).

End PROGRAM.

End SOUNDNESS.

Program Definition ipass : IPass (BTL.sem AnnotTrap) (BTL.sem AnnotTrap) :=
  {|
    ipass_spec := pass;
    ipass_impl := fun p => Errors.OK (transf_program p);
  |}.

End BTL_AnnotateAnalysis.