Module MachIRTaintAnalysis

Require Import AssocList.
Import Util.
Require MachIR.
Require Import Registers.
Import String.
Import Coqlib.
Import AST.
Import Machregs.
Import Globalenvs.
Import Op.
Import Integers.
Import Values.
Import Memory.
Import Mach.
Import MachIR.
Import Maps.
Import Utf8.
Import RelationClasses.
Import Morphisms.
Import Annotations.
Import FSetAVL.
Require Import ToString.

Unset Elimination Schemes.

Module SetProp (A: FSetInterface.S).
  Lemma mem_In x s : reflect (A.In x s) (A.mem x s).

  Instance string_of_t `(ToString A.elt) : ToString A.t := λ s,
  "{ " ++ A.fold (λ x, String.append (to_string x ++ "; ")) s "}".

End SetProp.

Instance mreg_eq_dec : EqDec mreg := mreg_eq.

Definition register_names := Eval vm_compute in
      rev_map (λ x, let '(s, r) := x in (r, s)) register_names.

Instance string_of_mreg : ToString mreg := λ r,
  match assoc r register_names with
  | Some s => s
  | None => "?"
  end.

Inductive sec_level := Low | High.

Definition Low_not_High (P: Prop) (EQ: Low = High) : P :=
  let 'eq_refl := EQ in I.

Definition max_sec_level (l1 l2:sec_level) : sec_level :=
  match l1 with
    | High => l1
    | _ => l2
  end.

Notation "l1 ∪ l2" := (max_sec_level l1 l2) (at level 19).

Lemma max_sec_level_comm x y : x ∪ y = y ∪ x.

Module Type AB_REG_MAP.
  Axiom t : Type.
  Axiom eq : t → t → Prop.
  Declare Instance equiv : Equivalence eq.
  Axiom t_dec : ∀ x x', { eq x x' } + { ¬ eq x x' }.
  Axiom empty : t.
  Axiom get : t -> mreg -> sec_level.
  Axiom set : t -> mreg -> sec_level -> t.
  Axiom union : t → t → t.

  Declare Instance get_m : Proper (eq ==> Logic.eq ==> Logic.eq) get.
  Axiom gempty : ∀ r, get empty r = Low.
  Axiom gs : ∀ x r v r', get (set x r v) r' = if mreg_eq r r' then v else get x r'.
  Axiom gunion : ∀ x y r, get (union x y) r = get x r ∪ get y r.

  Declare Instance string_of_t : ToString t.
End AB_REG_MAP.

Module MREG_ordered <: OrderedType.OrderedType.
  Definition t := mreg.
  Definition eq := @eq mreg.
  Definition eq_refl := @eq_refl mreg.
  Definition eq_sym := @eq_sym mreg.
  Definition eq_trans := @eq_trans mreg.
  Definition lt x y := Plt (IndexedMreg.index x) (IndexedMreg.index y).
  Definition lt_trans := fun x y z => Plt_trans (IndexedMreg.index x) (IndexedMreg.index y) (IndexedMreg.index z).
  Definition lt_not_eq : forall x y, lt x y -> ~ eq x y.
  Definition eq_dec := mreg_eq.
  Definition compare : forall x y, OrderedType.Compare lt eq x y.
End MREG_ordered.
  
Module AbRegMap : AB_REG_MAP.
  Module A := FSetAVL.Make MREG_ordered.
  Module AP := SetProp A.
  Definition t := A.t.
  Definition eq := A.eq.
  Instance equiv : Equivalence eq.
  Definition t_dec := A.eq_dec.
  Definition empty := A.empty.
  Definition get (s: t) (r: mreg) : sec_level :=
    if A.mem r s then High else Low.
  Definition set (s: t) (r: mreg) (v: sec_level) : t :=
    match v with
    | Low => A.remove r s
    | High => A.add r s
    end.

  Definition union := A.union.

  Instance get_m : Proper (eq ==> Logic.eq ==> Logic.eq) get.

  Definition gempty r : get empty r = Low := eq_refl.

  Lemma gs x r v r' : get (set x r v) r' = if mreg_eq r r' then v else get x r'.

  Lemma gunion x y r : get (union x y) r = get x r ∪ get y r.

  Instance string_of_t : ToString t := _.
End AbRegMap.

Local Coercion AbRegMap.get : AbRegMap.t >-> Funclass.

Inductive ab_cell : Type :=
| Global `(ident) `(Z)
| Stack `(nat) `(Z)
.

Instance ab_cell_dec : EqDec ab_cell.

Module Type AB_MEM_MAP.
  Axiom t : Type.
  Axiom eq : t → t → Prop.
  Declare Instance equiv : Equivalence eq.
  Axiom t_dec : ∀ x x', { eq x x' } + { ¬ eq x x' }.
  Axiom empty : t.
  Axiom get : t -> ab_cell -> sec_level.
  Axiom set : t -> ab_cell -> sec_level -> t.
  Axiom union : t → t → t.
  Axiom push : t -> t.
  Axiom pop : t -> t.

  Declare Instance get_m : Proper (eq ==> Logic.eq ==> Logic.eq) get.
  Axiom gempty : ∀ r, get empty r = Low.
  Axiom gunion : ∀ x y r, get (union x y) r = get x r ∪ get y r.

  Axiom gpush : ∀ x r, get (push x) r = match r with Global _ _ => get x r |
                                                Stack (S n) ofs => get x (Stack n ofs) |
                                                Stack O _ => Low end.
  Axiom gpop : ∀ x r, get (pop x) r = match r with Global _ _ => get x r |
                                              Stack n ofs => get x (Stack (S n) ofs) end.

  Declare Instance string_of_t : ToString t.
End AB_MEM_MAP.

Module AbMemMap : AB_MEM_MAP.
  Module PZ_ordered := OrderedTypeEx.PairOrderedType (OrderedTypeEx.Positive_as_OT) (OrderedTypeEx.Z_as_OT).
  Module A := FSetAVL.Make PZ_ordered.
  Module B := FSetAVL.Make OrderedTypeEx.Z_as_OT.

  Definition t := (A.t * list B.t)%type.
  Definition eq := fun x y => A.eq (fst x) (fst y) /\ list_forall2 B.eq (snd x) (snd y).
  Lemma list_forall2_dec:
    forall A B (R: A -> B -> Prop ) (R_dec: forall x y, { R x y } + { ~ R x y }) l1 l2,
      { list_forall2 R l1 l2 } + { ~ list_forall2 R l1 l2 }.
  Lemma t_dec : forall x y, { eq x y } + { ~ eq x y }.
  Lemma list_forall2_sym:
    forall A (R: A -> A -> Prop) (R_sym: forall a b, R a b -> R b a) l1 l2,
      list_forall2 R l1 l2 ->
      list_forall2 R l2 l1.
  Lemma list_forall2_trans:
    forall A (R: A -> A -> Prop) (R_trans: forall a b c, R a b -> R b c -> R a c) l1 l2 l3,
      list_forall2 R l1 l2 ->
      list_forall2 R l2 l3 ->
      list_forall2 R l1 l3.
  Instance equiv: Equivalence eq.
  Definition empty := (A.empty, @nil B.t).
  Definition get (s: t) (r: ab_cell): sec_level :=
    match r with
    | Global id ofs => if A.mem (id, ofs) (fst s) then High else Low
    | Stack n ofs => match nth_error (snd s) n with
                    | None => Low
                    | Some s => if B.mem ofs s then High else Low
                    end
    end.
  Fixpoint change_stack (k: Z -> B.t -> B.t) (n: nat) (ofs: Z) (l: list B.t): list B.t :=
    match l with
    | nil => nil
    | s::l => match n with
             | O => (k ofs s)::l
             | S n => s::(change_stack k n ofs l)
             end
    end.
  Definition set (s: t) (r: ab_cell) (v: sec_level): t :=
    match v with
    | Low =>
      match r with
      | Global id ofs => (A.remove (id, ofs) (fst s), snd s)
      | Stack n ofs => (fst s, change_stack B.remove n ofs (snd s))
      end
    | High =>
      match r with
      | Global id ofs => (A.add (id, ofs) (fst s), snd s)
      | Stack n ofs => (fst s, change_stack B.add n ofs (snd s))
      end
    end.
  Fixpoint map2 { A } (f: A -> A -> A) (l1 l2: list A): list A :=
    match l1 with
    | nil => l2
    | a::l1 => match l2 with
              | nil => a::l1
              | b::l2 => (f a b)::(map2 f l1 l2)
              end
    end.
  Definition union (x y: t): t := (A.union (fst x) (fst y), map2 B.union (snd x) (snd y)).
  Definition push (x: t): t := (fst x, B.empty::(snd x)).
  Definition pop (x: t): t :=
    match snd x with
    | nil => x
    | a::l => (fst x, l)
    end.
  Lemma list_forall2_nth_error:
    forall A B (R: A -> B -> Prop) l1 n l2,
      list_forall2 R l1 l2 ->
      match nth_error l1 n with
      | Some x => exists y, nth_error l2 n = Some y /\ R x y
      | None => nth_error l2 n = None
      end.
  Instance get_m : Proper (eq ==> Logic.eq ==> Logic.eq) get.
  Definition gempty : ∀ r, get empty r = Low.
  Lemma nth_error_map2:
    forall A (f: A -> A -> A) l1 n l2,
      match nth_error (map2 f l1 l2) n with
      | Some x => (exists a b, nth_error l1 n = Some a /\ nth_error l2 n = Some b /\ f a b = x) \/
                 (nth_error l1 n = None /\ nth_error l2 n = Some x) \/
                 (nth_error l1 n = Some x /\ nth_error l2 n = None)
      | None => nth_error l1 n = None /\ nth_error l2 n = None
      end.
  Definition gunion : ∀ x y r, get (union x y) r = get x r ∪ get y r.
  Definition gpush : ∀ x r, get (push x) r = match r with Global _ _ => get x r |
                                                     Stack (S n) ofs => get x (Stack n ofs) |
                                                     Stack O _ => Low end.
  Definition gpop : ∀ x r, get (pop x) r = match r with Global _ _ => get x r |
                                                   Stack n ofs => get x (Stack (S n) ofs) end.

  Module BP := SetProp B.
  Instance string_of_t : ToString t :=
    λ x, to_string (snd x).

End AbMemMap.
      
Definition stealth_var := Regset.t.

Definition sec_le (s1 s2:sec_level) : Prop :=
  s1=Low \/ s2=High.

Definition get_args_level (rm: AbRegMap.t) (args: list mreg) : sec_level :=
  fold_left (λ v r, v ∪ rm r) args Low.

Notation "vl '##t' x " := (get_args_level vl x) (at level 1).

Definition max_levels (l:list sec_level) : sec_level :=
  fold_left max_sec_level l Low.

Module Inference.

Require Import Lattice.
Require Import Kildall.

Record state : Type := State {
    reg: AbRegMap.t;
    mem: AbMemMap.t;
    context: list ident;
    alarms: list Errors.errmsg
  }.

Definition alarms_eq {X} (a a': list X) : Prop :=
  match a, a' with
  | nil, nil | _ :: _, _ :: _ => True
  | _, _ => False
  end.

Instance alarms_equiv {X} : Equivalence (@alarms_eq X).

Definition alarms_eqb {X} (a a': list X) : bool :=
  if a then if a' then true else false else if a' then false else true.

Remark alarmsP {X} (a a': list X) : reflect (alarms_eq a a') (alarms_eqb a a').

Definition state_eq (s s': state) : Prop :=
  AbRegMap.eq (reg s) (reg s') ∧
  AbMemMap.eq (mem s) (mem s') ∧
  context s = context s' ∧
  alarms_eq (alarms s) (alarms s').

Instance state_equiv : Equivalence state_eq.

Definition state_eq_dec (s s': state) : { state_eq s s' } + { ¬ state_eq s s' }.

Definition state_ge (s s': state) : Prop :=
  (∀ r, reg s' r = High → reg s r = High) ∧
  (∀ c, AbMemMap.get (mem s') c = High → AbMemMap.get (mem s) c = High).

Definition empty_state : state :=
  {| reg := AbRegMap.empty;
     mem := AbMemMap.empty;
     context := nil;
     alarms := nil |}.

Definition upd_reg (s: state) (f: AbRegMap.t → AbRegMap.t) : state :=
  {| reg := f (reg s); mem := mem s; context := context s; alarms := alarms s |}.

Definition upd_mem (s: state) (f: AbMemMap.t → AbMemMap.t) : state :=
  {| reg := reg s; mem := f (mem s); context := context s; alarms := alarms s |}.

Definition upd_alarms (s: state) (f: list Errors.errmsg → list Errors.errmsg) : state :=
  {| reg := reg s; mem := mem s; context := context s; alarms := f (alarms s) |}.

Definition push (f: ident) (s: state) : state :=
  {| reg := reg s; mem := AbMemMap.push (mem s); context := f :: context s; alarms := alarms s |}.

Definition pop (s s': state) : state :=
  {| reg := reg s'; mem := AbMemMap.pop (mem s'); context := context s; alarms := alarms s' |}.

Module D0 : SEMILATTICE
                     with Definition t := state
.

  Definition t : Type := state.
  Definition eq := state_eq.

  Instance eq_refl : Reflexive eq := _.
  Instance eq_sym : Symmetric eq := _.
  Instance eq_trans : Transitive eq := _.

  Definition beq (s s': t) : bool := state_eq_dec s s'.

  Lemma beq_correct s s' : beq s s' = true → eq s s'.

  Definition ge := state_ge.

  Lemma ge_refl s s' : eq s s' → ge s s'.

  Instance ge_trans : Transitive ge.

  Definition bot : state := empty_state.

  Lemma ge_bot x : ge x bot.

  Definition lub (s s': t) : t :=
    {| reg := AbRegMap.union (reg s) (reg s');
       mem := AbMemMap.union (mem s) (mem s');
       context := context s;
       alarms := rev_append (alarms s) (alarms s')
    |}.

  Lemma ge_lub_left s s' : ge (lub s s') s.

  Lemma ge_lub_right s s' : ge (lub s s') s'.

End D0.

Module D : SEMILATTICE with Definition t := option state :=
  LOption D0.

Module DS := Dataflow_Solver(D)(NodeSetForward).

Definition annotation : Type := list Annotations.ablock.

Definition fold_annot (α: annotation) {X: Type} (cb: (Z → ab_cell) → Z → Z → X → X) : X → X :=
  fold_left
    (λ x ab,
     let '(ab, (lo, hi)) :=
         match ab with
         | Annotations.ABlocal δ _ r => (Stack δ, r)
         | Annotations.ABglobal g r => (Global g, r)
         end in
     cb ab (Int.unsigned lo) (Int.unsigned hi) x
    ) α.

Section FOR_LOOP.
  Context {X : Type}
          (body : Z → X → X)
          (hi : Z).

  Function for_loop (lo: Z) (x: X) {measure (λ lo, Z.to_nat (hi - lo)) lo} : X :=
    if lo <? hi
    then for_loop (Z.succ lo) (body lo x)
    else x.
  
End FOR_LOOP.

Definition load_cells (mm: AbMemMap.t) (ϰ: memory_chunk) (c: Z → ab_cell) (lo hi: Z) (v: sec_level) : sec_level :=
  for_loop
    (λ ofs v,
     v ∪ AbMemMap.get mm (c ofs)
    ) (hi + size_chunk ϰ) lo v.

Definition load_all (mm: AbMemMap.t) (α: annotation) (ϰ: memory_chunk) : sec_level :=
  fold_annot α (load_cells mm ϰ) Low.

Definition set_cells (v: sec_level) (ϰ: memory_chunk) (c: Z → ab_cell) (lo hi: Z) (mm: AbMemMap.t) : AbMemMap.t :=
  for_loop
    (λ ofs mm,
     AbMemMap.set mm (c ofs) v
    ) (hi + size_chunk ϰ) lo mm.

Definition is_strong_update (α: annotation) : option ((Z → ab_cell) * Z) :=
  match α with
  | ab :: nil =>
    let '(c, (lo, hi)) :=
        match ab with
        | ABlocal d _ r => (Stack d, r)
        | ABglobal g r => (Global g, r)
        end in
    if Int.eq lo hi then Some (c, Int.unsigned lo) else None
  | _ => None
  end.

Definition store_all (mm: AbMemMap.t) (α: annotation) (ϰ: memory_chunk) (v: sec_level) :
  AbMemMap.t :=
  match v with
  | Low =>
    match is_strong_update α with
    | None => mm
    | Some (c, lo) => set_cells Low ϰ c lo lo mm
    end
  | High => fold_annot α (set_cells High ϰ) mm
  end.

Definition resolve_function_symbol (ge: Genv.t _ unit) (f: ident) : option fundef :=
  match Genv.find_symbol ge f with
  | None => None
  | Some b => Genv.find_funct_ptr ge b
  end.

Fixpoint registers_of_builtin_res {R} (br: builtin_res R) (a: list R) : list R :=
  match br with
  | BR r => r :: a
  | BR_none => a
  | BR_splitlong x y => registers_of_builtin_res x (registers_of_builtin_res y a)
  end.

Definition set_builtin_res (s: state) (dst: builtin_res mreg) (v: sec_level) : state :=
  fold_left (λ s d, upd_reg s (λ rm, AbRegMap.set rm d v)) (registers_of_builtin_res dst nil) s.

Section BUILTIN_ARGS.
  Variable fn : function.
  Variable rm : AbRegMap.t.
  Variable mm: AbMemMap.t.
  
  Fixpoint level_of_builtin_arg (ba: builtin_arg mreg) : sec_level :=
    match ba with
    | BA r => rm r
    | BA_splitlong x y => level_of_builtin_arg x ∪ level_of_builtin_arg y
    | BA_int _
    | BA_long _
    | BA_float _
    | BA_single _
    | BA_addrstack _
    | BA_addrglobal _ _
      => Low
    | BA_loadstack ϰ ofs =>
      let ofs := Int.sub ofs (Int.repr (fn_stackdata fn)) in
      let α := Annotations.ABlocal 0 xH (ofs, ofs) :: nil in
      load_all mm α ϰ
    | BA_loadglobal ϰ g ofs =>
      let α := Annotations.ABglobal g (ofs, ofs) :: nil in
      load_all mm α ϰ
    end.

  Definition level_of_builtin_args (args: list (builtin_arg mreg)) : sec_level :=
    fold_left (λ v a, v ∪ level_of_builtin_arg a) args Low.

End BUILTIN_ARGS.

Definition builtin_white_list : list string :=
  ("__i64_dtos"
:: "__i64_dtou"
:: "__i64_stod"
:: "__i64_utod"
:: "__i64_stof"
:: "__i64_utof"
:: "__builtin_negl"
:: "__builtin_addl"
:: "__builtin_subl"
:: "__builtin_mull"
:: "__i64_sdiv"
:: "__i64_udiv"
:: "__i64_smod"
:: "__i64_umod"
:: "__i64_shl"
:: "__i64_shr"
:: "__i64_sar"
:: nil)%string.

Section GE.

Variable prog : MachIR.program.
Variable ge: Genv.t fundef unit.

Definition is_volatile (g: ident) : bool :=
  match assoc g (prog_defs prog) with
  | Some (Gvar gv) => gvar_volatile gv
  | _ => false
  end.

Variable level_of_global : ident → sec_level.

Section ANALYZE.
Variable analyze : function → D.t → D.t.

Definition transfer (f: function) (pc: node) (is: D.t) : D.t :=
  match is with None => is | Some s =>
  match (fn_code f)!pc with
  | None => is
  | Some i =>
    match i with
    | MIop op args dest _ => Some (upd_reg s (λ rm, AbRegMap.set rm dest (rm##t args)))
    | MIload (_, α) ϰ addr args dst _ =>
      let v := if α then High else load_all (mem s) α ϰ ∪ (reg s) ##t args in
      Some (upd_reg s (λ rm, AbRegMap.set rm dst v))
    | MIstore (_, α) ϰ addr args src _ =>
      match α with
      | nil => None
      | _ =>
        let rg := reg s in
        let v := rg src ∪ rg ##t args in
        Some (upd_mem s (λ mm, store_all mm α ϰ v))
      end
    | MIgetparam ofs ty dst _ =>
      match
        match context s with
        | _ :: caller :: _ => resolve_function_symbol ge caller
        | _ => None
        end
      with
      | Some (Internal caller) =>
      let ofs := Int.sub ofs (Int.repr (fn_stackdata caller)) in
      let α := (Annotations.ABlocal 1 xH (ofs, ofs) :: nil) in
      let ϰ := chunk_of_type ty in
      let v := load_all (mem s) α ϰ in
      Some (upd_reg s (λ rm, AbRegMap.set rm dst v))
      | _ => None
      end
    | MIcall sg callee_name _ =>
      match resolve_function_symbol ge callee_name with
      | None => is
      | Some (Internal callee) =>
        option_map (pop s) (analyze callee (Some (push callee_name s)))
      | Some (External ef) => None
      end
    | MIbuiltin (EF_external _ _ | EF_malloc | EF_free | EF_memcpy _ _ | EF_inline_asm _ _ _) _ _ _
      => None
    | MIbuiltin (EF_builtin b _) args dst _ =>
      if List.in_dec string_dec b builtin_white_list
      then
        let v := level_of_builtin_args f (reg s) (mem s) args in
        Some (set_builtin_res s dst v)
      else None
    | MIbuiltin (EF_annot _ _ | EF_debug _ _ _) _ _ _ => is
    | MIbuiltin (EF_vload _) (BA_addrglobal g _ :: nil) dst _ =>
      if is_volatile g
      then Some (set_builtin_res s dst (level_of_global g))
      else None
    | MIbuiltin (EF_vload _) _ _ _ => None
    | MIbuiltin (EF_vstore _) (BA_addrglobal g _ :: _) _ _ =>
      if is_volatile g then is else None
    | MIbuiltin (EF_vstore _) _ _ _ => None
    | MIbuiltin (EF_annot_val _ _) args dst _ =>
      let v := level_of_builtin_args f (reg s) (mem s) args in
      Some (set_builtin_res s dst v)
    | MIgoto _
    | MIcond _ _ _ _
    | MIreturn
      => is
    end
  end
  end.

End ANALYZE.

Definition collect_result (fn: function) (res: PMap.t D.t) : D.t :=
  PTree.fold
    (λ vl pc i,
     match i with
     | MIreturn => D.lub vl (PMap.get pc res)
     | _ => vl
     end
    )
    (fn_code fn)
    (Some empty_state).

Variable sv : stealth_var.

Require Pun.

Definition is_stealth (α: annotation) : bool :=
  if α then false else
  Pun.forallb (λ ab, match ab with
                 | Annotations.ABlocal _ _ _ => false
                 | Annotations.ABglobal g _ => Regset.mem g sv
                 end) α.

Definition error pc ctx a :=
  (Errors.MSG "Not constant-time" :: Errors.POS pc :: (Errors.CTX ## ctx)) :: a.

Definition assert_low (pc: node) (ctx: list ident) (a: list Errors.errmsg) (v: sec_level) : list Errors.errmsg :=
  match v with
  | Low => a
  | High => error pc ctx a
  end.

Definition policy_check_one (res: D.t) (a: list Errors.errmsg) (pc: node) (i: instruction) : list Errors.errmsg :=
  let assert_low args :=
      match res with
      | None => error pc nil a
      | Some s =>
        let v := get_args_level (reg s) args in
        assert_low pc (context s) a v
      end
  in
  match i with
  | MIop _ _ _ _
  | MIgoto _
  | MIcall _ _ _
  | MIgetparam _ _ _ _
  | MIreturn
    => a
  | MIload (_, α) _ _ args _ _
  | MIstore (_, α) _ _ args _ _
    =>
    if is_stealth α
    then a
    else assert_low args
  | MIcond _ args _ _ => assert_low args
  | MIbuiltin _ args _ _ =>
a
  end.

Definition policy_check (fn: function) (res: PMap.t D.t) : list Errors.errmsg :=
  PTree.fold (λ a pc i,
              let s := PMap.get pc res in
              policy_check_one s a pc i)
             (fn_code fn)
             nil.

Fixpoint iter (n: nat) {struct n} :
  function → D.t → D.t :=
  match n with
  | O => λ _ _, None
  | S n' =>
    λ fn init,
    match DS.fixpoint (fn_code fn) successors (transfer (iter n') fn) (fn_entrypoint fn) init with
    | None => None
    | Some flow_sensitive_result =>
      let a := policy_check fn flow_sensitive_result in
      let s := collect_result fn flow_sensitive_result in
      match a with
      | nil => s
      | _ => option_map (λ s, upd_alarms s (app a)) s
      end
    end
  end.

End GE.

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

Definition full_range p g :=
  (Int.zero, Int.repr (Z.max 0 (Z.min (sizeof p g - 1) Int.max_unsigned))).

Definition init_ab_mem (p: program) (secret: list ident) :=
  List.fold_left (λ mm g, store_all mm (Annotations.ABglobal g (full_range p g) :: nil) Mint8unsigned High)
                 secret AbMemMap.empty.

Definition init_state (p: program) (secret: list ident) : D.t :=
  Some
  {| reg := AbRegMap.empty;
     mem := AbMemMap.push (init_ab_mem p secret);
     context := prog_main p :: nil;
     alarms := nil |}.

Definition run (p: program) (sv: stealth_var) (secret: list ident) (fuel: nat) : D.t :=
  let ge := Genv.globalenv p in
  match resolve_function_symbol ge (prog_main p) with
  | Some (Internal main) =>
    let level_of_global g :=
        if In_dec eq_dec g secret then High else Low
    in
    iter p ge level_of_global sv fuel main (init_state p secret)
  | _ => None
  end.

End Inference.