Module MemCsharpminor

Require ArithLib.
Require ListAdom.
Require Mconvert.
Require Pun.
Require AbMemSignatureCsharpminor.
Require DebugCshm DebugAbMachineEnv.

Import
  Utf8
  String
  Coqlib
  Maps
  Integers
  Floats
  Values
  Memory
  Globalenvs
  AST
  Cminor
  Csharpminorannot
  Util
  AssocList
  ToString
  Sets
  AdomLib
  AlarmMon
  ListAdom
  AbMemSignatureCsharpminor
  AbMachineEnv
  PExpr
  MemChunkTree
  Cells
  Pun
  NoError
  PointsTo
  Mconvert
  FastArith.

Require Import Annotagen.

Open Scope string.

Set Implicit Arguments.
Unset Elimination Schemes.


Definition injective_map {A B} (m: A → option B) : Prop :=
  ∀ x x' a,
    m(x) = Some a → m(x') = Some a →
    x = x'.

Definition stacks_tmp (stk stk': list (temp_env * env)) : Prop :=
  map snd stk =
  map snd stk'.

Lemma stacks_tmp_in : ∀ stk stk',
  stacks_tmp stk stk' →
  ∀ t e,
    In (t, e) stk' →
    ∃ t', In (t', e) stk.

Lemma get_stk_tmp : ∀ stk stk',
  stacks_tmp stk stk' →
  ∀ f,
  option_map snd (get_stk f stk) =
  option_map snd (get_stk f stk').

Remark block_of_ablock_tmp ge : ∀ stk stk',
  stacks_tmp stk stk' →
  ∀ ab, block_of_ablock ge stk ab = block_of_ablock ge stk' ab.

Module N := Nconvert ACTree.
Module PT := N.PT.
Export PT.

Definition lvarset : Type := PSet.t.
Definition tvarset : Type := PSet.t.
Definition stack : Type := list (lvarset * tvarset).

Instance fname_leb : leb_op fname := flat_leb_op Pos.eqb.
Instance fname_join : join_op fname (fname+⊤) := flat_join_op Pos.eqb.
Instance lvarset_leb : leb_op lvarset := flat_leb_op PSet.beq.
Instance lvarset_join : join_op lvarset (lvarset+⊤) := flat_join_op PSet.beq.

Definition sizes : Type := ABTreeDom.t (Z * (permission * bool)).
Definition sizes_gamma ge stk : gamma_op sizes mem :=
  λ sz m,
  ∀ b hi perm vol b',
    ABTreeDom.get b sz = Just (hi, (perm, vol)) →
    block_of_ablock ge stk b = Some b' →
    Mem.range_perm m b' 0 hi Cur perm
 ∧ Bool.leb vol (Senv.block_is_volatile ge b').

Instance BoolEqDec : EqDec bool := eq_dec_of_beq _ Bool.eqb_true_iff.
Definition permission_beq (x y: permission) : bool :=
  match x, y with
  | Freeable, Freeable
  | Writable, Writable
  | Readable, Readable
  | Nonempty, Nonempty
    => true
  | _, _ => false
  end.

Lemma permission_beq_iff x y : permission_beq x y = true ↔ x = y.
Instance PermissionEqDec : EqDec permission := eq_dec_of_beq _ permission_beq_iff.

Instance PermissionToString : ToString permission :=
  λ perm,
  match perm with
  | Freeable => "Freeable"
  | Writable => "Writable"
  | Readable => "Readable"
  | Nonempty => "Nonempty"
  end%string.

Instance sizes_leb : leb_op sizes :=
  leb (leb_op:=ABTreeDom.leb_tree (flat_leb_op eq_dec) _).

Instance sizes_join : join_op sizes sizes := ABTreeDom.join_tree (flat_join_op eq_dec) _.

Definition sizes_widen : sizes -> sizes -> sizes := join.

Instance sizes_top_correct ge stk : top_op_correct sizes mem (G:=sizes_gamma ge stk).

Instance sizes_leb_correct ge stk : leb_op_correct sizes mem (G:=sizes_gamma ge stk).

Instance sizes_join_correct ge stk : join_op_correct sizes sizes mem
                            (GA:=sizes_gamma ge stk) (GB:=sizes_gamma ge stk).

Lemma ptset_gamma_tmp ge : ∀ stk stk',
  stacks_tmp stk stk' →
  ∀ bs, ptset_gamma ge stk bs ⊆ ptset_gamma ge stk' bs.

Lemma type_gamma_covariant :
  ∀ (G G': gamma_op BlockSet.t block),
  (∀ bs, G bs ⊆ G' bs) →
  ∀ ty, type_gamma G ty ⊆ type_gamma G' ty.

Lemma points_to_gamma_tmp ge : ∀ stk stk',
  stacks_tmp stk stk' →
  ∀ ptr, points_to_gamma ge stk ptr ⊆ points_to_gamma ge stk' ptr.

Lemma sizes_gamma_tmp ge stk stk' :
  stacks_tmp stk stk' →
  ∀ sz, sizes_gamma ge stk sz ⊆ sizes_gamma ge stk' sz.

Section num.

  Context
    {num num_iter: Type}
    `{numToString: ToString num}
    `{numIterToString: ToString num_iter}
    (NumDom: ab_machine_env (var:=cell) num num_iter).

  Lemma gamma_num_ext :
   ∀ ρ ρ' : cell → mach_num,
   (∀ x : cell, ρ x = ρ' x) → ∀ m : num +⊥, γ m ρ → γ m ρ'.

  Definition compat := (λ ρ ρn, N.compat _ (λ x, x) ρ ρn).

  Variable ge : genv.
  Local Instance AblockToString : ToString ablock := AblockToString ge.
  Local Instance CellToString : ToString cell := CellToString ge.

  Record invariant (cs: concrete_state) : Prop :=
    { localFreeable :
        ∀ t e, In (t, e) (fst cs) →
          ∀ b hi, In (b, 0, hi) (blocks_of_env e) →
                  Mem.range_perm (snd cs) b 0 hi Cur Freeable
    ; localNotGlobal :
        ∀ t e, In (t, e) (fst cs) →
             ∀ x b y b' z,
               Genv.find_symbol ge x = Some b →
               e ! y = Some (b', z) →
               b ≠ b'
    ; localInj :
   injective_map (λ x_v,
                  do t_e <- get_stk (fst x_v) (fst cs);
                  fmap fst ((snd t_e) ! (snd x_v)))
   ; globalValid:
   ∀ x b, Genv.find_symbol ge x = Some b →
          b ∈ Mem.valid_block (snd cs)
   ; localValid:
       ∀ t e, In (t, e) (fst cs) →
                ∀ x b z,
               e ! x = Some (b, z) →
               b ∈ Mem.valid_block (snd cs)
   ; noIntFragment:
       ∀ ab b,
         block_of_ablock ge (fst cs) ab = Some b →
         ∀ o, match ZMap.get o (Mem.mem_contents (snd cs)) !! b with Fragment (Vint _) _ _ => False | _ => True end
   }.

  Lemma invariant_tmp : ∀ stk stk',
    stacks_tmp stk stk' →
    ∀ m, invariant (stk, m) → invariant (stk', m).

  Lemma invariant_block_of_ablock_inj stk m :
    (stk, m) ∈ invariant →
    ∀ ab₁ b₁ ab₂ b₂,
      block_of_ablock ge stk ab₁ = Some b₁ →
      block_of_ablock ge stk ab₂ = Some b₂ →
      ab₁ ≠ ab₂ →
      b₁ ≠ b₂.

  Lemma assign_const c i (nm : num) :
    ∀ ρ, ρ ∈ γ(nm) →
    match AbMachineEnv.assign c (me_const_i _ i) nm with
    | Bot => False
    | NotBot nm' => (upd ρ c (MNint i)) ∈ γ(nm')
    end.

  Definition tnum : Type := (points_to * num)%type.
  Definition tnum_iter : Type := (points_to * num_iter)%type.

  Section TNUM_GAMMA.

  Context (stk: list (temp_env * env)).

  Instance tnum_gamma : gamma_op tnum (cell → val) :=
    λ τ_ν ρ,
    let '(τ, ν) := τ_ν in
    ρ ∈ points_to_gamma ge stk (τ) ∧
    ∃ ρ',
      ρ' ∈ (compat ρ ∩ γ ν).

  Instance tnum_iter_gamma : gamma_op tnum_iter (cell → val) :=
    λ τ_ν ρ,
    let '(τ, ν) := τ_ν in
    ρ ∈ points_to_gamma ge stk (τ) ∧
    ∃ ρ',
      ρ' ∈ (compat ρ ∩ γ ν).

  Instance tnum_leb_correct : leb_op_correct (points_to * num) (cell → val).

  Instance tnum_top_correct : top_op_correct ((points_to * num)+⊥) (cell → val).

  Instance tnum_join_correct : join_op_correct (points_to * num) ((points_to * num)+⊥) (cell → val).

  Section REALIZATION.


    Definition is_int (tp: points_to) (c: cell) : bool :=
      ACTreeDom.get c tp ⊑ Just TyInt.

    Lemma is_int_intro (tp: points_to) (ρ: cell → val) (TP: ρ ∈ points_to_gamma ge stk tp) (c: cell) (P: bool → Prop):
      (P false) →
      ((∃ i, ρ c = Vint i) → P true) →
      P (is_int tp c).
    Global Opaque is_int.

    Definition realize_u8_from_κ (κ: typed_memory_chunk) (ab: ablock) (base: Z) (shift: Z) (tp: points_to) (nm: num) : tnum+⊥ :=
      let uc : cell := cell_from ab (base + shift, exist _ Mint8unsigned I) in
      let c : cell := cell_from ab (base, κ) in
      do nm' <- assign uc (MEbinop Oand (MEbinop Oshru (MEvar MNTint c) (MEconst _ (MNint (Int.repr (8 * shift))))) (MEconst _ (MNint (Int.repr 255)))) nm;
      NotBot (ACTreeDom.set tp uc (Just TyInt), nm').

    Definition tnum_mono (x y: tnum) : Prop :=
      ∀ ρ, Pun.pun_u8 ρ →
           ρ ∈ γ x →
           ρ ∈ points_to_gamma ge stk (fst y) ∧
           ∀ ρ',
             compat ρ ρ' →
             ρ' ∈ γ (snd x) → ρ' ∈ γ (snd y).

    Lemma tnum_m_stronger :
      ∀ x y, tnum_mono x y →
          Pun.pun_u8 ∩ γ (x) ⊆ γ (y).

    Lemma tnum_mono_refl x : tnum_mono x x.

    Lemma tnum_mono_trans y x z :
      tnum_mono x y → tnum_mono y z →
      tnum_mono x z.

    Definition tnum_mono' (x: tnum) (y': tnum+⊥) : Prop :=
      ∀ ρ, Pun.pun_u8 ρ →
           ρ ∈ γ x →
           match y' with
           | Bot => False
           | NotBot y =>
             ρ ∈ points_to_gamma ge stk (fst y) ∧
             ∀ ρ',
               compat ρ ρ' →
               ρ' ∈ γ (snd x) → ρ' ∈ γ (snd y)
           end.

    Lemma realize_u8_from_κ_sound (κ: typed_memory_chunk) ab base shift (tp: points_to) (nm: num) :
      (Archi.big_endian = false) →
      (align_chunk (proj1_sig κ) | base) →
      0 <= shift < size_chunk (proj1_sig κ) ∧ size_chunk (proj1_sig κ) <= 4 →
      let c : cell := cell_from ab (base, κ) in
      is_int tp c →
      tnum_mono' (tp, nm) (realize_u8_from_κ κ ab base shift tp nm).

    Definition cell_mem_rect {T: Type} :
      T →
      (ablock → Z → typed_memory_chunk → T) →
      cell → T :=
      λ b r c,
      match c with
      | AClocal f x ofs κ => r (ABlocal f x) ofs κ
      | ACglobal g ofs κ => r (ABglobal g) ofs κ
      | ACtemp _ _ => b
      end.

    Definition cell_mem_rect_intro {T: Type} (P: cell → T → Prop) :
      ∀ b r,
        (∀ f r, P (ACtemp f r) b) →
        (∀ ab ofs κ, P (cell_from ab (ofs, κ)) (r ab ofs κ)) →
        ∀ c, P c (cell_mem_rect b r c) :=
      λ b r B R c,
      match c with
      | AClocal f x ofs κ => R (ABlocal f x) ofs κ
      | ACglobal g ofs κ => R (ABglobal g) ofs κ
      | ACtemp f r => B f r
      end.
    Global Opaque cell_mem_rect.

    Definition optimistic_realization_one (c: cell) (tn: tnum) : tnum+⊥ :=
      let '(tp, nm) := tn in
      match ACTreeDom.get c tp with
      | Just _ => NotBot tn
      | All =>
        cell_mem_rect
          (NotBot tn)
          (λ ab ofs κ,
           match κ with
           | exist Mint8unsigned _ =>
             let (base, shift) := Z.div_eucl ofs 4 in
             let base := 4 * base in
             let c32 := cell_from ab (base, exist _ Mint32 I) in
             if is_int tp c32
             then realize_u8_from_κ (exist _ Mint32 I) ab base shift tp nm
             else
               let (base, shift) := Z.div_eucl ofs 2 in
               let base := 2 * base in
               let c16u := cell_from ab (base, exist _ Mint16unsigned I) in
               if is_int tp c16u
               then realize_u8_from_κ (exist _ Mint16unsigned I) ab base shift tp nm
               else
               let c16s := cell_from ab (base, exist _ Mint16signed I) in
               if is_int tp c16s
               then realize_u8_from_κ (exist _ Mint16signed I) ab base shift tp nm
               else
               let c8s := cell_from ab (ofs, exist _ Mint8signed I) in
               if is_int tp c8s
               then realize_u8_from_κ (exist _ Mint8signed I) ab ofs 0 tp nm
               else NotBot tn
           | exist Mint8signed _ =>
             let c := cell_from ab (ofs, κ) in
             let c8u := cell_from ab (ofs, exist _ Mint8unsigned I) in
             if is_int tp c8u then
               do nm' <- assign c (MEunop Ocast8signed (MEvar MNTint c8u)) nm;
               NotBot (ACTreeDom.set tp c (Just TyInt), nm')
             else NotBot tn
           | exist Mint16signed _ =>
             if ArithLib.divide ofs F2 then
             let c := cell_from ab (ofs, κ) in
             let c16u := cell_from ab (ofs, exist _ Mint16unsigned I) in
             if is_int tp c16u then
               do nm' <- assign c (MEunop Ocast16signed (MEvar MNTint c16u)) nm;
               NotBot (ACTreeDom.set tp c (Just TyInt), nm')
             else NotBot tn
             else NotBot tn
           | exist Mint32 _ =>
             if ArithLib.divide ofs F4 then
             let c := cell_from ab (ofs, κ) in
             let c8 shift := cell_from ab (ofs + shift, exist _ Mint8unsigned I) in
             if is_int tp (c8 0) then
             if is_int tp (c8 1) then
             if is_int tp (c8 2) then
             if is_int tp (c8 3) then
               do nm' <- assign c
                   (MEbinop Oadd (MEvar MNTint (c8 0))
                   (MEbinop Oadd (MEbinop Oshl (MEvar MNTint (c8 1)) (MEconst _ (MNint (Int.repr 8))))
                   (MEbinop Oadd (MEbinop Oshl (MEvar MNTint (c8 2)) (MEconst _ (MNint (Int.repr 16))))
                   (MEbinop Oshl (MEvar MNTint (c8 3)) (MEconst _ (MNint (Int.repr 24)))))))
                   nm;
               NotBot (ACTreeDom.set tp c (Just TyInt), nm')
             else NotBot tn
             else NotBot tn
             else NotBot tn
             else NotBot tn
             else NotBot tn
           | _ => NotBot tn
           end)
          c
      end.

    Lemma optimistic_realization_one_sound (c: cell) (tn: tnum) :
      tnum_mono' tn (optimistic_realization_one c tn).
    Global Opaque optimistic_realization_one.

    Definition optimistic_realization (cells: CellSet.t) (tn: tnum) : tnum+⊥ :=
      CellSet.fold (λ c tn, bind tn (optimistic_realization_one c)) cells (NotBot tn).

    Lemma optimistic_realization_sound cells tn:
      tnum_mono' tn (optimistic_realization cells tn).
    Global Opaque optimistic_realization.

  End REALIZATION.

  End TNUM_GAMMA.

  Variable max_concretize : N.

  Section CONVERT.

  Variable μ : fname.

  Variable ε : lvarset.

  Definition is_local (v: ident) : bool := PSet.mem v ε.

  Definition addr_of (v: ident) : BlockSet.t :=
    if is_local v
    then BSO.singleton (ABlocal μ v)
    else match Genv.find_symbol ge v with
         | Some b => BSO.singleton (ABglobal b)
         | None => BlockSet.empty
         end.

  Variable sz : sizes.

  Definition me_of_pe (tn: tnum) (pe: pexpr cell) : nconvert_t annotation_log (mexpr cell) :=
    let '(tp, nm) := tn in
    do me <- N.nconvert _ ge μ _ _ (λ x, x) _ _ NumDom sz nm tp pe;
    do _ <- assert _ (AbMachineEnv.noerror me nm)
       (λ _, "me_of_pe(" ++ to_string pe ++ "): error " ++ to_string me);
    ret me.

  Definition check_align (nm: num) (sz: Z) (me: mexpr cell) : bool :=
    match is_one sz with
    | false =>
           is_bot (AbMachineEnv.assume
              (MEbinop (Ocmp Cne)
                 (MEbinop Omodu me (me_const_i _ (Int.repr sz)))
                 (me_const_i _ Int.zero))
              true nm)
    | e => e
    end.

  Definition join_cellsets (cs: list (CellSet.t+⊤)) : CellSet.t+⊤ :=
    List.fold_left
      (λ acc cells,
       match acc with
       | All => All
       | Just acc => fmap (CellSet.union acc) cells
       end)
      cs
      (Just CellSet.empty).

  Lemma join_cellsets_correct cs :
    match join_cellsets cs with
    | All => In All cs
    | Just cells =>
      (∀ s, In s cs → ∃ s', s = Just s') ∧
      (∀ s, In (Just s) cs → ∀ c, CellSet.mem c s → CellSet.mem c cells) ∧
      (∀ c, CellSet.mem c cells → ∃ s, CellSet.mem c s ∧ In (Just s) cs)
    end.

  Definition has_type_VP (pe: pexpr cell) : bool :=
    match pexpr_get_ty pe with
    | VP => true
    | _ => false
    end.

  Definition itv_of_me (nm: num) (me: mexpr cell) : mach_num_itv+⊥ :=
    get_itv me nm.

  Definition int_pair_of_nvi (nvi: mach_num_itv+⊥) : (int * int)+⊤ :=
    match nvi with
    | Bot => All
    | (NotBot r) =>
      match r with
      | MNIint (Just (ZIntervals.ZITV lo hi)) => Just (Int.repr lo, Int.repr hi)
      | _ => All
      end
    end.

  Definition depth (f: ident) : nat :=
    (Pos.to_nat μ - Pos.to_nat f)%nat.

  Definition mk_log (α: Annotations.annotation) (nm: num) (ptr: BlockSet.t) (me: mexpr cell) : Annotations.annotation :=
    (fst α,
     match int_pair_of_nvi (itv_of_me nm me) with
     | All => nil
     | Just rng =>
       List.map
         (λ b,
          match b with
          | ABlocal f x => Annotations.ABlocal (depth f) x rng
          | ABglobal b => Annotations.ABglobal match Genv.invert_symbol ge b with Some g => g | None => xH end rng
          end
         )
         (BlockSet.elements ptr)
     end).

  Definition am_log (a: annotation_log) : nconvert_t annotation_log unit :=
    (tt :: nil, (nil, a :: nil)).

  Definition deref_pexpr (α: option _) (tn: tnum) (κ: typed_memory_chunk) (lpe: list (pexpr cell)) : alarm_mon annotation_log (CellSet.t+⊤) :=
    let al := align_chunk (proj1_sig κ) in
    do cells <- ((
    do pe <- (ret lpe : nconvert_t _ (pexpr cell));
    do _ <- assert _ (has_type_VP pe)
       (λ _, "deref_pexpr: maybe not a pointer (" ++ to_string pe ++ ")");
    let aptr := pt_eval_pexpr ge μ (fst tn) pe in
    do me <- me_of_pe tn pe;
    do _ <- assert _ (check_align (snd tn) al me)
       (λ _, "bad align (" ++ to_string (proj1_sig κ) ++ "): " ++ to_string me);
    let offs := concretize_int max_concretize me (snd tn) in
    match aptr with
    | Just (TyPtr (Just ptr) | TyZPtr (Just ptr)) =>
      do _ <- match α with None => ret tt | Some α' => am_log (mk_log α' (snd tn) ptr me) end;
      ret (set_product ptr κ offs)
    | _ => ret All
    end) : alarm_mon _ (list (CellSet.t+⊤)));
    ret (join_cellsets cells).

  Lemma deref_pexpr_inv α tn κ lpe cells :
    am_get (deref_pexpr α tn κ lpe) = Some cells →
    let al := align_chunk (proj1_sig κ) in
    ∀ pe, In pe lpe →
          pexpr_get_ty pe = VP ∧
          ∃ lme,
            am_get (me_of_pe tn pe) = Some lme ∧
            ∀ me, In me lme →
            check_align (snd tn) al me = true ∧
            let ofs := concretize_int max_concretize me (snd tn) in
            match cells with All => True | Just cells =>
            ofs ≠ NotBot All ∧
            ∃ ptr,
            (pt_eval_pexpr ge μ (fst tn) pe = Just (TyPtr (Just ptr)) ∨
             pt_eval_pexpr ge μ (fst tn) pe = Just (TyZPtr (Just ptr))) ∧
            ∀ b i,
              BlockSet.mem b ptr →
              i ∈ γ(ofs) →
              CellSet.mem (cell_from b (Int.unsigned i, κ)) cells
            end.

  Definition constant_of_constant (c: Csharpminor.constant) : constant :=
    match c with
    | Csharpminor.Ointconst i => Ointconst i
    | Csharpminor.Olongconst i => Olongconst i
    | Csharpminor.Ofloatconst f => Ofloatconst f
    | Csharpminor.Osingleconst f => Osingleconst f
    end.

  Definition convert_err (e:expr) msg :=
    ("convert(" ++ to_string e ++ "): " ++ msg ++ new_line ++
     "Function: " ++ to_string μ ++ new_line ++
     "Locals: " ++ to_string ε ++ new_line ).
  Opaque convert_err.

  Definition convert_t A := tnum -> alarm_mon annotation_log (tnum * A).
  Local Instance convert_monad : monad convert_t :=
    {
      ret A := λ a tn, ret (tn, a);
      bind A B := λ m f tn, do (tn', a) <- m tn; f a tn'
    }.

  Let get_tnum : convert_t tnum := λ tn, ret (tn, tn).
  Let lift {A} (m: alarm_mon annotation_log A) : convert_t A :=
    λ tn, fmap (λ x, (tn, x)) m.

  Local Notation "'alarm' e" := ((λ tn, (((tn, tt), ((λ _, e) :: nil, nil)))):(convert_t _)) (at level 100).

  Definition typ_of_type (ty: type) : typ :=
    match ty with
    | TyFloat => VF
    | TySingle => VS
    | TyLong => VL
    | TyZero | TyInt => VI
    | TyPtr _ => VP
    | TyZPtr _ | TyIntPtr => VIP
    end.

  Let convert_var (e: expr) (c: cell) : convert_t (list (pexpr cell)) :=
    λ tn,
    let '(tp, nm) := tn in
    match ACTreeDom.get c tp with
    | Just ty => ret (PEvar c (typ_of_type ty) :: nil) tn
    | All => (do _ <- alarm (convert_err e ("bad temp in " ++ to_string μ)); ret nil) tn
    end.

  Let realize (cells: CellSet.t) : convert_t (list cell) :=
    λ tn,
    match optimistic_realization cells tn with
    | Bot => ret nil tn
    | NotBot tn' => ret (CellSet.elements cells) tn'
    end.

  Definition typ_eval_constant (cst: constant) : typ :=
    match cst with
      | Ointconst n => VI
      | Ofloatconst n => VF
      | Osingleconst n => VS
      | Olongconst n => VL
      | Oaddrsymbol s ofs => VP
    end.

  Definition typ_eval_binop (op: binary_operation) (arg1 arg2: typ): typ :=
    match op with
    | Oadd =>
      match arg1, arg2 with
      | VP, VI
      | VI, VP => VP
      | VI, VI => VI
      | _, _ => VIP
      end
    | Osub =>
      match arg1, arg2 with
      | VP, VI => VP
      | VP, VP
      | VI, VI => VI
      | _, _ => VIP
      end
    | Omul | Odiv | Odivu | Omod | Omodu | Oand | Oor | Oxor | Oshl
    | Oshr | Oshru | Ocmp _ | Ocmpu _ | Ocmpf _ | Ocmpfs _ | Ocmpl _ | Ocmplu _ => VI
    | Oaddf | Osubf | Omulf | Odivf => VF
    | Oaddfs | Osubfs | Omulfs | Odivfs => VS
    | Oaddl | Osubl | Omull | Odivl | Odivlu | Omodl | Omodlu | Oandl
    | Oorl | Oxorl | Oshll | Oshrl | Oshrlu => VL
    end.

  Remark eval_constant_wt {c} :
    type_of_constant c (typ_eval_constant c).

  Remark eval_binop_wt {op ty ty'} :
    type_of_binop op (typ_eval_binop op ty ty').

  Fixpoint convert (e: expr) : convert_t (list (pexpr cell)) :=
    let err := convert_err e in
    match e with
    | Evar v => convert_var e (ACtemp μ v)
    | Eaddrof i =>
      if is_local i
      then ret (PElocal _ i :: nil)
      else match Genv.find_symbol ge i with
           | Some _ => ret (PEconst _ (Oaddrsymbol i Int.zero) VP eq_refl :: nil)
           | None => do _ <- alarm (err "bad global variable");
                     ret nil
           end
    | Econst cst =>
      let cst := constant_of_constant cst in
      ret (PEconst _ cst (typ_eval_constant cst) eval_constant_wt :: nil)
    | Eunop op e1 =>
      do e1' <- convert e1;
      ret (rev_map (λ e, PEunop op e (t := type_of_unop op) eq_refl) e1')
    | Ebinop op e1 e2 =>
      do e1' <- convert e1;
      do e2' <- convert e2;
      ret (map2 (λ e1 e2,
                 PEbinop op e1 e2
                         (typ_eval_binop op (pexpr_get_ty e1) (pexpr_get_ty e2))
                         eval_binop_wt
                ) e1' e2')

    | Eload α κ e1 =>
      do e1' <- convert e1;
      do κ <-
        match κ return convert_t (option typed_memory_chunk) with
          | Many32 | Many64 =>
            do _ <- alarm (err "Many32 or Many64"); ret None
          | κ => ret (Some (exist _ κ I:typed_memory_chunk))
        end;
      do tn <- get_tnum;
      do cells <- match κ with Some κ => lift (deref_pexpr (Some α) tn κ e1') | None => ret All end;
      match cells with
      | All => do _ <- alarm (err "too many cells"); ret nil
      | Just cells =>
        do cells <- realize cells;
        λ tn,
        let '(tp, nm) := tn in
        lift (
      am_map' annotation_log (λ c, match ACTreeDom.get c tp with
                    | All => Error None (err ("bad cell: " ++ to_string c))
                    | Just ty => Result (PEvar c (typ_of_type ty))
                    end)
              cells
          )
             tn
      end
    end.

  Definition me_of_pe_list (tn: tnum) (lpe: list (pexpr cell)) : alarm_mon annotation_log (list (mexpr cell)) :=
    flat_map_a annotation_log (me_of_pe tn) (ret lpe).

  Definition nconvert (e:expr) : convert_t (list (mexpr cell)) :=
    do lpe <- convert e;
    λ tn, lift (me_of_pe_list tn lpe) tn.

  Definition deref_expr_err (tn: tnum) (e: expr) (κ: typed_memory_chunk) (lpe: list (pexpr cell)) :=
    ("deref_expr(" ++ to_string e ++ ", " ++ to_string (proj1_sig κ) ++ ") " ++ to_string lpe )%string.
  Opaque deref_expr_err.

  Definition deref_expr α κ (e: expr) : convert_t (list cell) :=
    do lpe <- convert e;
    λ tn,
      lift (
      do cells <- deref_pexpr α tn κ lpe;
      match cells with
      | All => do _ <- alarm_am (deref_expr_err tn e κ lpe);
                ret nil
      | Just cell_set => ret (CellSet.elements cell_set)
      end
      ) tn.

  Section CONVERT_CORRECT.
    Context (e: env) (tmp: temp_env) (m: mem).
    Context (stk: list (temp_env * env)).
    Context (Hstk: μ = plength stk).
    Let ρ := mem_as_fun ge ((tmp, e) :: stk, m).
    Hypothesis E: ∀ i, is_local i = true ↔ e ! i ≠ None.
    Hypothesis INV : invariant ((tmp, e) :: stk, m).
    Hypothesis SZ: m ∈ sizes_gamma ge ((tmp, e) :: stk) sz.

    Lemma Tmp: ∀ i v, tmp ! i = Some v → ρ (ACtemp μ i) = v.
    Hint Resolve Tmp.

    Lemma me_of_pe_correct (tp: points_to) (nm: num) (ρn: cell → mach_num) (NM: ρn ∈ γ(nm)) pe lme :
      am_get (me_of_pe (tp, nm) pe) = Some lme →
      am_get (N.nconvert annotation_log ge μ _ _ (λ x, x) _ _ NumDom sz nm tp pe) = Some lme ∧
      ∀ me, In me lme → ¬ error_mexpr ρn me.

    Ltac with_me_of_pe q :=
      repeat match goal with
      | H : appcontext[ me_of_pe ?nm ?pe ] |- _ =>
        generalize (me_of_pe_correct pe);
        destruct (me_of_pe nm pe); q
      end.

    Lemma me_of_pe_list_correct nm lpe lme log :
      me_of_pe_list nm lpe = (lme, (nil, log)) →
      flat_map_a_spec _ (me_of_pe nm) lpe lme.

    Lemma pexpr_get_ty_ok (pe: pexpr cell) v :
      eval_pexpr ge m ρ e pe v → v ≠ Vundef → v ∈ γ(pexpr_get_ty pe).

    Lemma check_align_correct (nm: num) (ρn: cell → mach_num) (NM: ρn ∈ γ(nm)) al me :
      al = 1 ∨ al = 2 ∨ al = 4 ∨ al = 8 →
      check_align nm al me = true →
      ∀ n, eval_mexpr ρn me (MNint n) →
           Int.unsigned n = al * Int.unsigned (Int.divu n (Int.repr al)).

    Ltac subs := repeat match goal with H : ?a = ?b |- _ => subst a || subst b end.

    Let Hpun : ρ ∈ pun_u8 := mem_as_fun_pun_u8 _ _ INV.(noIntFragment).

    Lemma typ_of_type_gamma G ty :
      type_gamma G ty ⊆ gamma_typ (typ_of_type ty).

    Lemma convert_wf (q: expr):
      ∀ (tn: tnum) (TN: ρ ∈ tnum_gamma ((tmp, e) :: stk) tn),
      match am_get (convert q tn) with
      | Some (tn', lp) =>
        tnum_mono ((tmp, e) :: stk) tn tn'
        ∧
        ∀ pe, In pe lp → N.nconvert_def_pre ge e ρ pe
      | None => True
      end.

    Lemma convert_free_def (q: expr) :
      ∀ (tn: tnum) (TN: ρ ∈ tnum_gamma ((tmp, e) :: stk) tn),
      match am_get (convert q tn) with
      | Some (tn', lp) =>
          ∀ pe, In pe lp ->
          ∀ x, pe_free_var pe x -> ρ x ≠ Vundef
      | None => True
      end.

    Remark align_chunk_4_cases (κ: memory_chunk) :
      align_chunk κ = 1 ∨ align_chunk κ = 2 ∨ align_chunk κ = 4 ∨ align_chunk κ = 8.

  Lemma type_of_unop_correct op arg v :
    Cminor.eval_unop op arg = Some v →
    v ≠ Vundef →
    γ (type_of_unop op) v.

  Lemma typ_eval_binop_correct op arg1 arg2 p t1 t2 v :
    Cminor.eval_binop op arg1 arg2 p = Some v →
    v ≠ Vundef →
    γ t1 arg1 →
    γ t2 arg2 →
    γ (typ_eval_binop op t1 t2) v.

    Lemma convert_correct (q: expr) :
      ∀ (tn: tnum) (TN: ρ ∈ tnum_gamma ((tmp, e) :: stk) tn),
      match am_get (convert q tn) with
      | Some (tn', lp) =>
        ∀ v, eval_expr ge e tmp m (expr_erase q) v →
             ∃ a, In a lp ∧ eval_pexpr ge m ρ e a v
      | None => True
      end.

    Lemma SZ' :
      ∀ (b : ABTree.elt) (hi : Z) (md : permission * bool)
        (b' : block),
        ABTreeDom.get b sz = Just (hi, md)
        → block_of_ablock ge ((tmp, e) :: stk) b = Some b'
        → Mem.range_perm m b' 0 hi Cur Nonempty.

    Lemma convert_noerror (q: expr) :
      ∀ (tn: tnum) (TN: ρ ∈ tnum_gamma ((tmp, e) :: stk) tn),
      match am_get (convert q tn) with
      | Some (tn', lp) => (∀ pe, In pe lp → ¬ error_pexpr ge m ρ e pe) → ¬ error_expr ge e tmp m (expr_erase q)
      | None => True
      end.

    Lemma deref_expr_correct α (tn: tnum) (TN: ρ ∈ tnum_gamma ((tmp, e) :: stk) tn) κ q :
      match am_get (deref_expr α κ q tn) with
      | Some (tn', cells) =>
        tnum_mono ((tmp, e) :: stk) tn tn' ∧
        ¬ error_expr ge e tmp m (expr_erase q) ∧
        ∀ v, eval_expr ge e tmp m (expr_erase q) v →
        ∃ ab b i, v = Vptr b i ∧
                  In (cell_from ab (Int.unsigned i, κ)) cells ∧
                  block_of_ablock ge ((tmp, e) :: stk) ab = Some b ∧
                  (align_chunk (proj1_sig κ) | Int.unsigned i)
      | None => True
      end.

    Lemma nconvert_sound (tn: tnum) (TN: ρ ∈ tnum_gamma ((tmp, e) :: stk) tn) (q: expr) :
      match am_get (nconvert q tn) with
      | Some (tn', _) =>
        tnum_mono ((tmp, e) :: stk) tn tn' ∧
        ¬ error_expr ge e tmp m (expr_erase q)
      | None => True
      end.

    Lemma nconvert_ex (tn: tnum) (TN: ρ ∈ tnum_gamma ((tmp, e) :: stk) tn) (q: expr) :
      match am_get (nconvert q tn) with
      | Some ((tp', nm'), lme) =>
        tnum_mono ((tmp, e) :: stk) tn (tp', nm') ∧
        ∃ lpe, am_get (convert q tn) = Some ((tp', nm'), lpe) ∧
        ∀ v, eval_expr ge e tmp m (expr_erase q) v →
             v ≠ Vundef →
        ∀ (TP: ρ ∈ points_to_gamma ge ((tmp, e) :: stk) tp') (ρn: cell → mach_num) (Nc: compat ρ ρn) (NM: ρn ∈ γ nm'),
             ∃ pe lme' me n,
               In pe lpe ∧
               eval_pexpr ge m ρ e pe v ∧
               am_get (N.nconvert annotation_log ge μ _ _ (λ x, x) _ _ NumDom sz nm' tp' pe) = Some lme' ∧
               (∀ me', In me' lme' → In me' lme) ∧
               In me lme' ∧
               N.ncompat v n ∧
               N.wtype_num n (pexpr_get_ty pe) ∧
               eval_mexpr ρn me n
      | None => True
      end.

    Lemma convert_to_me (tn: tnum) (TN: ρ ∈ tnum_gamma ((tmp, e) :: stk) tn) (q: expr) :
      match am_get (convert q tn) with
      | Some ((tp', nm'), lpe) =>
        match am_get (me_of_pe_list (tp', nm') lpe) with
        | Some lme =>
          tnum_mono ((tmp, e) :: stk) tn (tp', nm') ∧
          ∃ v, eval_expr ge e tmp m (expr_erase q) v ∧ v ≠ Vundef
          ∧ ∀ (TP: ρ ∈ points_to_gamma ge ((tmp, e) :: stk) tp') (ρn: cell → mach_num) (Nc: compat ρ ρn) (NM: ρn ∈ γ nm'),
            ∃ pe lme' me n,
                 In pe lpe ∧
                 eval_pexpr ge m ρ e pe v ∧
                 am_get (N.nconvert annotation_log ge μ _ _ (λ x, x) _ _ NumDom sz nm' tp' pe) = Some lme' ∧
                 (∀ me', In me' lme' → In me' lme) ∧
                 In me lme' ∧
                 N.ncompat v n ∧
                 N.wtype_num n (pexpr_get_ty pe) ∧
                 eval_mexpr ρn me n
        | None => True
        end
      | None => True
      end.

  End CONVERT_CORRECT.

  End CONVERT.

  Definition t : Type := (stack+⊤ * (sizes * tnum))%type.
  Definition iter_t : Type := (stack+⊤ * (sizes * (points_to * num_iter)))%type.

  Definition AbMem stk sz tp nm : t := (stk, (sz, (tp, nm))).
  Definition ab_stk (ab: t) : stack+⊤ := fst ab.
  Definition ab_sz (ab: t) : sizes := fst (snd ab).
  Definition ab_nm (ab: t) : tnum := snd (snd ab).
  Definition ab_tp (ab: t) : points_to := fst (snd (snd ab)).
  Definition ab_num (ab: t) : num := snd (snd (snd ab)).

  Arguments ab_stk ab /.
  Arguments ab_sz ab /.
  Arguments ab_nm ab /.
  Arguments ab_tp ab /.
  Arguments ab_num ab /.

  Definition ab_stk_iter (ab: iter_t) : stack+⊤ := fst ab.
  Definition ab_sz_iter (ab: iter_t) : sizes := fst (snd ab).
  Definition ab_nm_iter (ab: iter_t) : tnum_iter := snd (snd ab).
  Definition ab_tp_iter (ab: iter_t) : points_to := fst (snd (snd ab)).
  Definition ab_num_iter (ab: iter_t) : num_iter := snd (snd (snd ab)).

  Definition with_stk (f: stack+⊤ → stack+⊤) (ab: t) : t :=
    AbMem (f (ab_stk ab)) (ab_sz ab) (ab_tp ab) (ab_num ab).

  Definition with_sz (f: sizes → sizes) (ab: t) : t :=
    AbMem (ab_stk ab) (f (ab_sz ab)) (ab_tp ab) (ab_num ab).

  Definition with_tp (f: points_to → points_to) (ab: t) : t :=
    AbMem (ab_stk ab) (ab_sz ab) (f (ab_tp ab)) (ab_num ab).

  Definition with_num (f: num → num) (ab: t) : t :=
    AbMem (ab_stk ab) (ab_sz ab) (ab_tp ab) (f (ab_num ab)).

  Definition with_tnum (f: tnum → tnum) (ab: t) : t :=
    (ab_stk ab, (ab_sz ab, f (ab_nm ab))).

  Definition dom {A} (x: positive) (m: PTree.t A) : bool :=
    match PTree.get x m with
    | Some _ => true
    | None => false
    end.

  Remark dom_set {A} x m y (a: A) : dom x (PTree.set y a m) = peq x y || dom x m.

  Instance stack_elt_gamma : gamma_op (lvarset * tvarset) (temp_env * env) :=
    λ ltv te_e,
    ∀ x, PSet.mem x (fst ltv) = dom x (snd te_e).

  Instance join_stack_elt_correct :
    join_op_correct (lvarset*tvarset) ((lvarset * tvarset)+⊤) (temp_env * env).

  Instance leb_stack_elt_correct :
    leb_op_correct (lvarset * tvarset) (temp_env * env).

  Record gamma (ab: t) (cs: concrete_state) : Prop :=
  { _ : fst cs ∈ γ(ab_stk ab)
  ; _ : ab_stk ab ≠ All → invariant cs
  ; _ : snd cs ∈ sizes_gamma ge (fst cs) (ab_sz ab)
  ; _ : mem_as_fun ge cs ∈ (tnum_gamma (fst cs) (ab_nm ab))
  }.
  Instance t_gamma : gamma_op t concrete_state := gamma.

  Record iter_gamma (ab: iter_t) (cs: concrete_state) : Prop :=
  { _ : fst cs ∈ γ(ab_stk_iter ab)
  ; _ : ab_stk_iter ab ≠ All → invariant cs
  ; _ : snd cs ∈ sizes_gamma ge (fst cs) (ab_sz_iter ab)
  ; _ : mem_as_fun ge cs ∈ (tnum_iter_gamma (fst cs) (ab_nm_iter ab))
  }.
  Instance iter_t_gamma : gamma_op iter_t concrete_state := iter_gamma.

  Definition split_t (ab:t) : option (ident * lvarset * tvarset * stack * sizes * tnum) :=
    match ab_stk ab with
    | All | Just nil => None
    | Just ((ε, τ) :: σ) =>
      let '(sz, tn) := (snd ab) in
      Some (plength σ, ε, τ, σ, sz, tn)
    end.

  Definition noerror (exp: expr) (ab: t) : alarm_mon _ unit :=
    match split_t ab with
    | Some (μ, ε, τ, σ, sz, tn) =>
      do _ <- nconvert μ ε sz exp tn;
      ret tt
    | None => do _ <- alarm_am "anomaly (noerror)"; ret tt
    end.

  Definition ab_eval_expr (ab: t) (a: expr)
  : alarm_mon _ ((tnum * type+⊤ * list (mexpr cell)) +⊥) :=
    match split_t ab with
    | Some (μ, ε, τ, σ, sz, tn) =>
      do (tn', lp) <- convert μ ε sz a tn;
      let '(tp', nm') := tn' in
      do ln <- me_of_pe_list μ sz tn' lp;
      match lp with nil => ret Bot | _ =>
      let ty := union_list_map (pt_eval_pexpr ge μ tp') All lp in
      ret (NotBot (tn', ty, ln))
      end
    | None => do _ <- alarm_am "ab_eval_expr failed"; ret Bot
    end.

  Fixpoint ab_eval_exprlist (ab: t) (e: list expr) : alarm_mon _ ((t * list (type+⊤ * list (mexpr cell)))+⊥) :=
    match e with
    | nil => ret (NotBot (ab, nil))
    | e :: e' =>
      do r <- ab_eval_expr ab e;
      match r with
      | Bot => ret Bot
      | NotBot (tn, ty, me) =>
        do m <- ab_eval_exprlist (with_tnum (λ _, tn) ab) e';
        match m with
        | Bot => ret Bot
        | NotBot (ab, y) => ret (NotBot (ab, (ty, me) :: y))
        end
      end
    end.

  Definition nm_forget_all :=
    fold_left (λ m c, bind m (AbMachineEnv.forget c)).

  Definition nm_upd (nm:num) (c:cell) (e:(mexpr cell)) : num+⊥ :=
    let nm' := AbMachineEnv.assign c e nm in
    nm_forget_all (overlap c) nm'.

  Definition nm_upd_cells (nm:num) (l:list cell) (e:(mexpr cell)) : num+⊥ :=
    union_list_map (λ c, nm_upd nm c e) (NotBot nm) l.

  Definition ct_forget_all {A: Type} := fold_left (λ (m: ACTreeDom.t A) c, ACTreeDom.set m c All).

  Definition ct_upd {A} (m:ACTreeDom.t A) (c:cell) (a:A+⊤) : ACTreeDom.t A :=
    ACTreeDom.set (ct_forget_all (overlap c) m) c a.

  Definition tp_upd_cells (tp: points_to) (l: list cell) (tt: type+⊤) : points_to :=
    union_list_map (λ c, ct_upd tp c tt) tp l.


  Definition chunk_type (κ: typed_memory_chunk) (ty: typ+⊤) : bool :=
    match ty with
    | All => false
    | Just ty' =>
      match κ, ty' with
      | exist (Mint8signed | Mint8unsigned | Mint16signed | Mint16unsigned) _, VI
      | exist Mint32 _, (VI | VP | VIP)
      | exist Mint64 _, VL
      | exist Mfloat64 _, VF
      | exist Mfloat32 _, VS
        => true
      | _, _ => false
      end
    end.

  Local Instance string_of_type : ToString type := string_of_type ge.

  Definition assign_cells (κ: option typed_memory_chunk) (c: list cell) (a:expr) (ab:t) : alarm_mon _ (t+⊥) :=
    do res <- ab_eval_expr ab a;
    match res with
    | NotBot ((tp, nm), ty, ln) =>
        do _ <- am_assert match κ with Some κ => chunk_type κ (fmap typ_of_type ty) | None => true end
                             ("bad type: " ++ to_string ty);
        ret (
            do nm' <- union_list_map (nm_upd_cells nm c) (NotBot nm) ln;
            let tp' := tp_upd_cells tp c ty in
            ret (AbMem (ab_stk ab) (ab_sz ab) tp' nm')
        )
    | Bot => ret Bot
    end.

  Definition assign_in (μ: fname) (x: ident) (a: expr) (ab: t) : alarm_mon _ (t+⊥) :=
    (assign_cells None (ACtemp μ x :: nil) a ab).

  Definition assign (x:ident) (a:expr) (ab:t) : alarm_mon _ (t+⊥) :=
    match ab_stk ab with
    | Just (_::σ) => assign_in (plength σ) x a ab
    | _ => do _ <- alarm_am "assign failed"; ret Bot
    end.

  Let type_of_typ (ty: typ) : type+⊤ :=
    match ty with
    | VI => Just TyInt
    | VF => Just TyFloat
    | VS => Just TySingle
    | VL => Just TyLong
    | _ => All
    end.

  Definition assign_any (x: ident) (ty: typ) (ab: t) : alarm_mon annotation_log (t+⊥) :=
    match split_t ab with
    | Some (μ, ε, τ, σ, sz, tn) =>
      let '(tp, nm) := tn in
      let c := ACtemp μ x in
      do nm' <-
            match ty with
            | VI | VL | VF | VS => ret (AbMachineEnv.forget c nm)
            | _ => do _ <- alarm_am ("assign_any: bad type " ++ to_string ty); ret Bot
            end;
        ret (
        do nm' <- nm';
        ret (with_num (λ _, nm')
                               (with_tp (λ tp, ACTreeDom.set tp c (type_of_typ ty)) ab)))
    | None => do _ <- alarm_am "assign_any failed"; ret Bot
    end.

  Definition permission_can_write (p: permission) : bool :=
    match p with
    | (Freeable | Writable) => true
    | (Readable | Nonempty) => false
    end.

  Definition cell_in_bounds (κ:typed_memory_chunk) (ab: t) (c: cell) : alarm_mon annotation_log unit :=
    let b := ablock_of_cell c in
    let '(ofs, _) := range_of_cell c in
    match ABTreeDom.get b (ab_sz ab) with
    | All => do _ <- alarm_am ("block of unknown size: " ++ to_string b); ret tt
    | Just (hi, (perm, vol)) =>
      if permission_can_write perm then
      if zle 0 ofs && zle (ofs + size_chunk (proj1_sig κ)) hi
      then ret tt
      else do _ <- alarm_am ("cell out of range("++ to_string hi ++"): " ++ to_string c); ret tt
      else do _ <- alarm_am ("read-only cell: " ++ to_string c); ret tt
    end.

  Definition expr_has_cast_for_chunk (e: expr) (κ: typed_memory_chunk) : bool :=
    match κ, e with
    | exist Mint8signed _, Eunop Ocast8signed _
    | exist Mint8unsigned _, Eunop Ocast8unsigned _
    | exist Mint16signed _, Eunop Ocast16signed _
    | exist Mint16unsigned _, Eunop Ocast16unsigned _
    | exist Mint32 _, _
    | exist Mint64 _, _
    | exist Mfloat32 _, _
    | exist Mfloat64 _, _
      => true
    | _, _ => false
    end.

  Definition store (α: Annotations.annotation) (κ: memory_chunk) (a e: expr) (ab: t) : alarm_mon _ (t+⊥) :=
    let κ : option typed_memory_chunk :=
        match κ with
          | Many32 | Many64 => None
          | κ => Some (exist _ κ I)
        end
    in
    match κ with
      | None =>
        do _ <- alarm_am "invalid store memory chunk"; ret Bot
      | Some κ =>
        match split_t ab with
          | Some (μ, ε, τ, σ, sz, tn) =>
            do _ <- am_assert (expr_has_cast_for_chunk e κ)
                  ("Uncasted expr for " ++ to_string (proj1_sig κ) ++ ": " ++ to_string e);
            do (tn', cells) <- deref_expr μ ε sz (Some α) κ a tn;
            let ab := with_tnum (λ _, tn') ab in
            match cells with nil => ret Bot | _ =>
              do _ <- am_rev_map (cell_in_bounds κ ab) cells;
              assign_cells (Some κ) cells e ab
            end
          | None => do _ <- alarm_am "store failed"; ret Bot
        end
    end.

  Definition nassume b nm (F: mexpr cell → mexpr cell) e : num+⊥ :=
    union_list_map (λ me, AbMachineEnv.assume (F me) b nm) (NotBot nm) e.

  Definition bool_expr (e: expr) : expr :=
    match e with
    | Ebinop (Ocmp _| Ocmpu _| Ocmpf _| Ocmpfs _| Ocmpl _| Ocmplu _) _ _ => e
    | _ => Ebinop (Ocmp Cne) e (Econst (Csharpminor.Ointconst Int.zero))
    end.

  Definition assume (b: expr) (ab: t) : alarm_mon _ (t+⊥ * t+⊥) :=
    match split_t ab with
    | Some (μ, ε, τ, σ, sz, tn) =>
      let b := bool_expr b in
      do (tn', b') <- nconvert μ ε sz b tn;
      let '(tp, nm) := tn' in
      ret
        (do nz <- nassume true nm id b'; ret (AbMem (Just ((ε,τ)::σ)) sz tp nz),
         do z <- nassume false nm id b'; ret (AbMem (Just ((ε,τ)::σ)) sz tp z))
    | None => do _ <- alarm_am "assume failed"; ret (Bot, Bot)
    end.

  Definition deref_fun (e: expr) (ab: t) : alarm_mon annotation_log (list (ident * fundef)) :=
    match split_t ab with
    | Some (μ, ε, τ, σ, sz, tn) =>
      do (tn, cells) <- deref_expr μ ε sz None (exist _ Mint32 I) e tn;
      am_map' _ (λ c,
              match c with
              | ACglobal b 0 (exist Mint32 _) =>
                match Genv.find_funct_ptr ge b with
                | Some f =>
                  match Genv.invert_symbol ge b with
                  | Some i => Result (i,f)
                  | None => Error None "unknown function"
                  end
                | None => Error None ("bad function pointer " ++ to_string b)
                end
              | _ => Error None ("bad function pointer (2)")
              end) cells
    | None => do _ <- alarm_am "anomaly: deref_fun";
              ret nil
    end.

  Definition ab_bind_parameters (μ: ident)
             (formals: list ident) (args: list (type+⊤ * list (mexpr cell)))
             : alarm_mon annotation_log (t+⊥) → alarm_mon _ (t+⊥) :=
    fold_left2
      (λ acc id v,
       do ab' <- acc;
       ret (
           do ab' <- ab';
           let c := ACtemp μ id in
           let '(ty, ln) := v in
           do nm' <- union_list_map (λ me, AbMachineEnv.assign c me (ab_num ab')) (NotBot (ab_num ab')) ln;
           ret (AbMem (ab_stk ab') (ab_sz ab')
                      (ct_upd (ab_tp ab') c ty)
                      nm'))
      )
      (λ _ _, do _ <- alarm_am "ab_bind_parameters: too many formals"; ret Bot)
      (λ _ _, do _ <- alarm_am "ab_bind_parameters: too many arguments"; ret Bot)
      formals args.

  Definition set_local_sizes μ vars : sizes → sizes :=
    fold_left (λ sz x_hi, ABTreeDom.set sz (ABlocal μ (fst x_hi)) (Just (snd x_hi, (Freeable, false))))
              vars.

  Definition push_frame (μ_def: function) (args: list expr) (ab:t) : alarm_mon _ (t+⊥) :=
    do σ' <- match ab_stk ab with
                | All => do _ <- alarm_am "no stack"; ret nil
                | Just σ' => ret σ'
                end;
      let μ := plength σ' in
      do res <- ab_eval_exprlist ab args;
      match res with
      | Bot => ret Bot
      | NotBot (ab, eargs) =>
      let ε := PSetOp.build (rev_map fst μ_def.(fn_vars)) in
      let τ := PSetOp.build (μ_def.(fn_temps) ++ μ_def.(fn_params)) in
      let σ := (ε, τ) :: σ' in
      let ab' := with_stk (λ _, Just σ) (with_sz (set_local_sizes μ μ_def.(fn_vars)) ab) in
      ab_bind_parameters μ μ_def.(fn_params) eargs (ret (NotBot ab'))
      end.

  Definition is_local_cell (μ: fname) (c: cell) : bool :=
    match c with
    | AClocal μ' _ _ _
    | ACtemp μ' _ => eq_dec μ μ'
    | ACglobal _ _ _ => false
    end.

  Definition is_local_block (μ: fname) (ab: ablock) : bool :=
    match ab with
    | ABlocal μ' _ => eq_dec μ μ'
    | ABglobal _ => false
    end.

  Definition pop_local_pt (μ: fname) : points_to → points_to :=
    ACTreeDom.SP.filter
      (λ c ty,
       if is_local_cell μ c
       then false
       else match ty with
            | (TyPtr (Just bs) | TyZPtr (Just bs)) =>
              negb (BSO.existsb (is_local_block μ) bs)
            | TyPtr All | TyZPtr All
            | TyFloat | TySingle | TyLong | TyInt | TyZero | TyIntPtr => true
            end).

  Definition clear_local_sizes μ ε : sizes → sizes :=
    PSet.fold (λ x, ABTree.remove (ABlocal μ x)) ε.

  Definition all_local_cells (μ: ident) (ε: lvarset) (sz: sizes) : list cell :=
    PSet.fold (λ x,
         let z := match ABTree.get (ABlocal μ x) sz with Some (z, _) => z | None => Z0 end in
         memory_chunk_fold (λ acc κ,
           let k := align_chunk (proj1_sig κ) in
           N.peano_rect _
             acc
             (λ n, cons (AClocal μ x (Z.of_N n * k) κ))
             (Z.to_N (z / k))
         )
    ) ε nil.

  Definition pop_local_num (μ: ident) (ε: lvarset) (τ: tvarset) (sz: sizes) : num+⊥ → num+⊥ :=
    (nm_forget_all (all_local_cells μ ε sz)) ∘ (nm_forget_all (List.map (ACtemp μ) (PSet.elements τ))).

  Definition pop_frame (res: option (expr)) (temp : option (ident)) (ab: t) : alarm_mon _ (t+⊥) :=
    match ab_stk ab, res, temp with
    | Just ((ε₀, τ₀)::(ε,τ)::σ), Some r, Some x =>
      let μ := plength σ in
      let μ₀ := Pos.succ μ in
(
      do ab' <- assign_in μ x r ab;
      match ab' with
      | NotBot ab'' =>
        ret (
            do nm' <- pop_local_num μ₀ ε₀ τ₀ (ab_sz ab'') (NotBot (ab_num ab''));
            ret (with_sz (clear_local_sizes μ₀ ε₀)
                (with_tp (pop_local_pt μ₀)
                (with_stk (λ _, Just ((ε,τ)::σ))
                (with_num (λ _, nm') ab'')))))
      | Bot => ret Bot
      end
      )
    | Just ((ε,τ)::nil), Some r, _ =>
      let μ := xH in
      do ret' <- ab_eval_expr ab r;
      match ret' with
      | Bot => ret Bot
      | NotBot (_, ty, _) =>
        do _ <- am_assert match ty with Just (TyInt | TyZero) => true | _ => false end "main ret not an int";
          ret (NotBot (with_sz (clear_local_sizes μ ε)
                           (with_tp (pop_local_pt μ)
                           (with_stk (λ _, Just nil) ab))))
      end
    | Just (_::nil), _, _ =>
      do _ <- alarm_am "pop_frame failed at main"; ret Bot
    | Just ((ε,τ)::σ), None, None =>
      let μ := plength σ in
        ret (
            do nm' <- pop_local_num μ ε τ (ab_sz ab) (NotBot (ab_num ab));
            ret (with_sz (clear_local_sizes μ ε)
                (with_tp (pop_local_pt μ)
                (with_stk (λ _, Just σ)
                (with_num (λ _, nm') ab)))))
    | Just ((ε,τ)::σ), Some r, None =>
      let μ := plength σ in
      do _ <- noerror r ab;
        ret (
            do nm' <- pop_local_num μ ε τ (ab_sz ab) (NotBot (ab_num ab));
            ret (with_sz (clear_local_sizes μ ε)
                (with_tp (pop_local_pt μ)
                (with_stk (λ _, Just σ)
                (with_num (λ _, nm') ab)))))
    | _, _, _ => do _ <- alarm_am ("pop_frame failed: " ++ to_string temp ++ " := " ++ to_string res ); ret Bot
    end.

  Let bad_align {T} (r: T) : alarm_mon annotation_log _ :=
    do _ <- alarm_am "misaligned init data"; ret r.
  Instance InitDataToString : ToString init_data :=
    λ id,
    match id with
    | Init_int8 i => "int8: " ++ to_string i
    | Init_int16 i => "int16: " ++ to_string i
    | Init_int32 i => "int32: " ++ to_string i
    | Init_int64 i => "int64: " ++ to_string i
    | Init_float32 f => "float32: " ++ to_string f
    | Init_float64 f => "float64: " ++ to_string f
    | Init_space n => "space: " ++ to_string n
    | Init_addrof i o => "&" ++ to_string i ++ " + " ++ to_string o
    end.

  Definition zero_type_of_chunk (κ: typed_memory_chunk) : type :=
    match κ with
    | exist (Mint8signed | Mint8unsigned |
             Mint16signed | Mint16unsigned |
             Mint32) _
      => TyZero
    | exist Mint64 _ => TyLong
    | exist Mfloat64 _ => TyFloat
    | exist Mfloat32 _ => TySingle
    | exist _ H => match H with end
    end.

  Definition permission_can_read (p: permission) : { perm_order p Readable } + { p = Nonempty } :=
    match p with
    | Freeable => left (perm_F_any Readable)
    | Writable => left perm_W_R
    | Readable => left (perm_refl Readable)
    | Nonempty => right eq_refl
    end.

  Definition zero_all_cells (b: block) (base: Z) (sz: Z) (ab: t): t+⊥ :=
    N.peano_rect
      (λ _, t+⊥)
      (NotBot ab)
      (λ ofs ab,
       memory_chunk_fold
         (λ ab κ,
          let ofs' := base + Z.of_N ofs in
          if Zdivide_dec (align_chunk (proj1_sig κ)) ofs' (align_chunk_pos (proj1_sig κ))
          && zle (Z.of_N ofs + size_chunk (proj1_sig κ)) sz then
            do ab <- ab;
              let c := ACglobal b ofs' κ in
              do nm <- AbMachineEnv.assign c
                (match κ with
                   | exist (Mint8signed | Mint8unsigned | Mint16signed | Mint16unsigned | Mint32) _
                     => me_const_i _ Int.zero
                   | exist Mint64 _ => me_const_l _ Int64.zero
                   | exist (Mfloat32) _ => me_const_s _ Float32.zero
                   | exist (Mfloat64) _ => me_const_f _ Float.zero
                   | exist _ H => match H with end
                 end)
                (ab_num ab);
              ret
                (with_tp (ACTree.set c (zero_type_of_chunk κ))
                (with_num (λ _, nm) ab))
          else ab
         ) ab)
      (Z.to_N sz).

  Definition ab_alloc_global perm vol b (gv: list init_data) ab : alarm_mon _ (t+⊥) :=
    do sz_ab' <- am_fold
      (λ (acc:_*(_+⊥)) id,
       let '(ofs, ab) := acc in
       let ofs' := ofs + Genv.init_data_size id in
       let c κ H := ACglobal b ofs (exist _ κ H) in
       if match id with
          | Init_space _
          | Init_int8 _ => true
          | Init_int16 _ => Zdivide_dec (align_chunk Mint16signed) ofs eq_refl
          | Init_int32 _
          | Init_addrof _ _ => Zdivide_dec (align_chunk Mint32) ofs eq_refl
          | Init_int64 _ => Zdivide_dec (align_chunk Mint64) ofs eq_refl
          | Init_float32 _ => Zdivide_dec (align_chunk Mfloat32) ofs eq_refl
          | Init_float64 _ => Zdivide_dec (align_chunk Mfloat64) ofs eq_refl
          end then
       match id return alarm_mon _ (Z*t+⊥) with
       | Init_int32 n =>
          ret (ofs',
                  if permission_can_read perm
                  then
                  do ab' <- ab;
                  do nm <- AbMachineEnv.assign (c Mint32 I) (me_const_i _ n) (ab_num ab');
                  ret (with_tp (ACTree.set (c Mint32 I) (type_of_int n))
                      (with_num (λ _, nm) ab'))
                  else ab)
       | Init_int64 n =>
          ret (ofs',
                  if permission_can_read perm
                  then
                  do ab' <- ab;
                  do nm <- AbMachineEnv.assign (c Mint64 I) (me_const_l _ n) (ab_num ab');
                  ret (with_tp (ACTree.set (c Mint64 I) TyLong)
                      (with_num (λ _, nm) ab'))
                  else ab)
       | Init_addrof s o =>
         match Genv.find_symbol ge s with
         | Some b' => ret (ofs',
                              if permission_can_read perm
                              then
                              do ab' <- ab;
                              do nm <- AbMachineEnv.assign (c Mint32 I) (me_const_i _ o) (ab_num ab');
                              ret (with_tp (ACTree.set (c Mint32 I) (TyPtr (Just (BSO.singleton (ABglobal b')))))
                                  (with_num (λ _, nm) ab'))
                              else ab)
         | None => do _ <- alarm_am ("ab_alloc_globals: not a symbol ("
                                        ++ to_string s ++ ")"); ret (ofs', ab)
         end
       | Init_space s =>
         ret (ofs',
                 if negb (permission_can_read perm)
                 then ab else do ab' <- ab; zero_all_cells b ofs s ab')
       | Init_float64 f =>
         ret (ofs',
           if negb (permission_can_read perm)
           then ab
           else
             do ab' <- ab;
             do nm <- AbMachineEnv.assign (c Mfloat64 I) (MEconst _ (MNfloat f)) (ab_num ab');
             ret (with_tp (ACTree.set (c Mfloat64 I) TyFloat)
                 (with_num (λ _, nm) ab')))
       | Init_float32 f =>
         ret (ofs',
           if negb (permission_can_read perm)
           then ab
           else
             do ab' <- ab;
             do nm <- AbMachineEnv.assign (c Mfloat32 I) (MEconst _ (MNsingle f)) (ab_num ab');
             ret (with_tp (ACTree.set (c Mfloat32 I) TySingle)
                 (with_num (λ _, nm) ab')))
       | Init_int8 i =>
         ret (ofs',
                 if permission_can_read perm
                 then
                 do ab' <- ab;
                 do nm <- AbMachineEnv.assign (c Mint8unsigned I) (MEunop Ocast8unsigned (me_const_i _ i)) (ab_num ab');
                 ret (with_tp (ACTree.set (c Mint8unsigned I) (type_of_int i))
                     (with_num (λ _, nm) ab'))
                 else ab)
       | Init_int16 i =>
         ret (ofs',
                 if permission_can_read perm
                 then
                 do ab' <- ab;
                 do nm <- AbMachineEnv.assign (c Mint16unsigned I) (MEunop Ocast16unsigned (me_const_i _ i)) (ab_num ab');
                 ret (with_tp (ACTree.set (c Mint16unsigned I) (type_of_int i))
                     (with_num (λ _, nm) ab'))
                 else ab)
       end
       else bad_align acc)
      gv
      (0, ab);
    let '(sz, ab') := sz_ab' in
    ret (do ab'' <- ab'; ret (with_sz (ABTree.set (ABglobal b) (sz, (perm, vol))) ab'')).

  Definition ab_alloc_globals (gl: list (ident * globdef fundef unit)) : alarm_mon _ (block * t+⊥) :=
    (am_fold
       (λ acc ig,
        let '(b, ab) := acc in
        let b' := Pos.succ b in
        match ig with
        | (_, Gfun _) => ret (b', fmap (with_sz (ABTree.set (ABglobal b) (1, (Nonempty, false)))) ab)
        | (_, Gvar gv) =>
            do ab' <- ab_alloc_global (Genv.perm_globvar gv) (gvar_volatile gv) b gv.(gvar_init) ab;
            ret (b', ab')
        end)
       gl
       (xH, do t <- ⊤; ret (Just nil, t))).

  Definition init_mem (defs:list (ident * globdef fundef unit)) : alarm_mon _ (t+⊥) :=
    do _ <- am_assert (norepet_map fst defs) ("duplicate name in globals");
    do ab <- ab_alloc_globals defs;
    ret (snd ab).

  Definition validate_volatile_ptr (sz: sizes) (ptr: BlockSet.t) (lne: list (mexpr cell)) : bool → bool :=
    BlockSet.fold
      (λ blk (acc: bool),
       if acc
       then
         match blk with
         | ABlocal _ _ => false
         | ABglobal b =>
           match Genv.invert_symbol ge b with
           | None => false
           | Some g =>
             match ABTreeDom.get blk sz with
             | Just (hi, (perm, vol)) =>
               vol
             | All => false
             end
           end
         end
       else acc)
      ptr.

  Definition check_volatile (tgt: (ident * int) + expr) (κ: memory_chunk) (ab: t) : alarm_mon _ ident :=
    do _ <-
    match tgt with
    | inl (g, ofs) =>
      match Genv.find_symbol ge g with
      | None => alarm_am "check_volatile: bad global"
      | Some b =>
        let b := ABglobal b in
        match ABTreeDom.get b (ab_sz ab) with
        | Just (hi, (perm, vol)) =>
          am_assert vol ("check_volatile: not volatile")
        | All => alarm_am "check_volatile: unknown size"
        end
      end
    | inr addr =>
      do z <- ab_eval_expr ab addr;
      match z with
      | NotBot (tn, Just (TyPtr (Just ptr)), ne) =>
        am_assert (validate_volatile_ptr (ab_sz ab) ptr ne true) ("check_volatile: bad pointer")
      | _ => alarm_am "check_volatile: unresolved expression"
      end
    end;
    match ab_stk ab with
    | Just ( _ :: σ ) => ret (plength σ)
    | _ => do _ <- alarm_am "check_volatile: no stack"; ret xH
    end.

  Definition forget_cell (ab: t) (c: cell) : t+⊥ :=
    do nm' <- AbMachineEnv.forget c (ab_num ab);
    NotBot (
           (with_tp (λ tp, ACTreeDom.set tp c (⊤))
           (with_num (λ _, nm') ab))).

  Definition vload (rettemp: option ident) (g_ofs: option (ident * int)) (κ: memory_chunk) (args: list expr) (ab: t) : alarm_mon _ (t+⊥) :=
    do _ <- am_assert match κ with Mint64 | Mint32 | Mfloat32 | Mfloat64 => true | _ => false end "vload: bad chunk";
    match
    match g_ofs, args with
    | Some q, nil => Some (inl q)
    | None, addr :: nil => Some (inr addr)
    | _, _ => None
    end
    with
    | None => do _ <- alarm_am "vload: bad arguments"; ret Bot
    | Some tgt =>
    do μ <- check_volatile tgt κ ab;
    match rettemp with
    | None => ret (NotBot ab)
    | Some r =>
      match κ with
      | Mint64 => assign_any r VL ab
      | Mfloat64 => assign_any r VF ab
      | Mfloat32 => assign_any r VS ab
      | _ => ret (forget_cell ab (ACtemp μ r))
      end
    end
    end.

  Definition only_global_pointer (aptr: BlockSet.t+⊤) : bool :=
    match aptr with
    | All => false
    | Just ptr =>
      negb (BSO.existsb (λ p,
                             match p with
                             | ABglobal b => match Genv.invert_symbol ge b with Some g => negb (Senv.public_symbol ge g) | None => true end
                             | ABlocal _ _ => true
                             end) ptr)
    end.

  Definition vstore (rettemp: option ident) (g_ofs: option (ident * int)) (κ: memory_chunk) (args: list expr) (ab: t) : alarm_mon _ (t+⊥) :=
    match
    match g_ofs, args with
    | Some q, arg :: nil => Some (inl q, arg)
    | None, addr :: arg :: nil => Some (inr addr, arg)
    | _, _ => None
    end
    with
    | None => do _ <- alarm_am "vstore: bad arguments"; ret Bot
    | Some (tgt, arg) =>
    do μ <- check_volatile tgt κ ab;
    do v <- ab_eval_expr ab arg;
    match v with
    | Bot => ret Bot
    | NotBot (tn, ptr, lne) =>
      do _ <- am_assert
            match ptr with
            | Just ty =>
              match ty, κ with
              | TyLong, Mint64
              | TySingle, Mfloat32
              | TyFloat, Mfloat64
              | (TyInt | TyZero), ( Mint32 | Mint8signed | Mint8unsigned | Mint16signed | Mint16unsigned )
                => true
              | (TyPtr bs | TyZPtr bs), Mint32 => only_global_pointer bs
              | _, _ => false
              end
            | All => false
            end
            ("vstore: cannot prove that the argument " ++ to_string arg ++ " is well-typed " ++ to_string ptr);
      let ab := with_tnum (λ _, tn) ab in
      match rettemp with
      | None => ret (NotBot ab)
      | Some r => ret (forget_cell ab (ACtemp μ r))
      end
    end
    end.

  Instance widen_mem : widen_op (iter_t+⊥) (t+⊥) :=
    {| widen A B :=
         let '(NUM_it_ret, NUM_ret) :=
           match A with
           | Bot => init_iter Bot
           | NotBot (_, (_, (_, NUM))) => NUM
           end ▽
           match B with
           | Bot => Bot
           | NotBot (_, (_, (_, NUM))) => NotBot NUM
           end
         in
         match B with
         | Bot =>
           match A with
           | Bot => (Bot, Bot)
           | NotBot (STK, (SZ, (PT, _))) =>
             (NotBot (STK, (SZ, (PT, NUM_it_ret))),
              do NUM_ret <- NUM_ret;
              ret (STK, (SZ, (PT, NUM_ret))))
           end
         | NotBot (STK', (SZ', (PT', _))) =>
           match A with
           | Bot =>
             (NotBot (STK', (SZ', (PT', NUM_it_ret))),
              do NUM_ret <- NUM_ret;
              ret (STK', (SZ', (PT', NUM_ret))))
           | NotBot (STK, (SZ, (PT, NUM))) =>
             let STK_ret :=
               match STK, STK' with
               | Just STK, Just STK' => list_widen join STK STK'
               | _, _ => All
               end
             in
             let SZ_ret := sizes_widen SZ SZ' in
             let PT_ret := points_to_widen PT PT' in
             (NotBot (STK_ret, (SZ_ret, (PT_ret, NUM_it_ret))),
              do NUM_ret <- NUM_ret;
              ret (STK_ret, (SZ_ret, (PT_ret, NUM_ret))))
           end
         end;
       init_iter x :=
         do x <- x;
         ret (ab_stk x, (ab_sz x, (ab_tp x, init_iter (NotBot (ab_num x)))))
    |}.

  Instance mem_cshm_dom : mem_dom annotation_log t (iter_t+⊥) :=
    {| assign := assign
     ; assign_any := assign_any
     ; store := store
     ; assume := assume

     ; noerror := noerror
     ; deref_fun := deref_fun

     ; ab_vload := vload
     ; ab_vstore := vstore

     ; push_frame := push_frame
     ; pop_frame := pop_frame

     ; ab_malloc sz dst ab := do _ <- alarm_am "malloc"; ret (⊤)
     ; ab_free e ab := do _ <- alarm_am "free"; ret (⊤)
     ; ab_memcpy sz al dst src ab :=
         do _ <- alarm_am ("memcpy(" ++ to_string sz ++ ", " ++ to_string al ++ ", " ++ to_string dst ++ ", " ++ to_string src ++ ")");
         ret (⊤)

     ; init_mem := init_mem
    |}.

  Instance t_join_correct : join_op_correct t (t+⊥) concrete_state.

  Instance t_leb_correct : leb_op_correct t concrete_state.

  Instance TToString : ToString t :=
    (λ x,
    "Mem { " ++ "stack : " ++ to_string (ab_stk x) ++ new_line
             ++ "blocks: " ++ to_string (ab_sz x) ++ new_line
             ++ "types : " ++ to_string (ab_tp x) ++ new_line
             ++ "num : " ++ to_string (ab_num x) ++ new_line
             ++ "}" ++ new_line ).

  Instance IterTToString : ToString iter_t :=
      (λ x,
       "Mem { " ++ "stack : " ++ to_string (ab_stk_iter x) ++ new_line
                ++ "blocks: " ++ to_string (ab_sz_iter x) ++ new_line
                ++ "types : " ++ to_string (ab_tp_iter x) ++ new_line
                ++ "num : " ++ to_string (ab_num_iter x) ++ new_line
                ++ "}" ++ new_line ).

End num.