Module CsharpminorAnalysis

Require Import ToString.
Require Import
  Behaviors
  AbIdealEnvProduct IdealEnvToMachineEnv
  CsharpminorIter
  MemCsharpminor DebugAbMemCsharpminor.
Require
  AbTyps
  AbVarExpEq
  ZCongruences
  IdealIntervalsNonrel
  AbLinearize
  Octagons
  PolAdomZ.
Import
  Utf8 Coqlib
  Globalenvs
  Csharpminorannot.
Import
  AdomLib Util
  DebugAbMachineEnv AbMachineEnv
  Cells AlarmMon
  CsharpminorIter
  AbMemSignatureCsharpminor
  PointsTo
  MemCsharpminor.

Section S.

  Context (max_concretize : N)
          (trace verbose: bool)
          (unroll: nat).

  Context {tnum tnum_iter: Type}
          `{ToString tnum} `{ToString tnum_iter}
          (M: @ab_machine_env cell tnum tnum_iter _).

   Definition doit (p: program) : alarm_mon _ unit :=
    let ge := Genv.globalenv p in
    let mem_dom := mem_cshm_dom M ge max_concretize in
    iter_program _ unroll p
      (abmem:=if trace then
         @debug_mem_dom _ _ _ mem_dom (TToString ge)
                        (@bot_lift_toString _ (IterTToString ge)) verbose
       else mem_dom).

End S.

Require Import DomKind.

Existing Instance ACTreeDom.toString.

Section VA.

  Context (kind: num_dom_kind)
          (max_concretize: N)
          (trace verbose: bool)
          (unroll: nat).

  Definition vanalysis (p: program) :=
    let CS : ToString _ := CellToString (Genv.globalenv p) in
    match kind return _ with
    | ZIntervals =>
      let t_dom := reduced_product
        (AbTyps.t * (AbVarExpEq.t * (ZCongruences.t * IdealIntervalsNonrel.t))) _
      in
      let dom := idealenv_to_machineenv t_dom _ in
      let dom := if trace then debug_ab_machine_env verbose dom else dom in
      doit max_concretize trace verbose unroll dom p
    | Octagons =>
      let t_dom := reduced_product
                     (AbTyps.t * (AbVarExpEq.t * (ZCongruences.t *
                     (IdealIntervalsNonrel.t * (AbLinearize.t * Octagons.t)))))%type
                     _
      in
      let dom := idealenv_to_machineenv t_dom _ in
      let dom := if trace then debug_ab_machine_env verbose dom else dom in
      doit max_concretize trace verbose unroll dom p
    | Poly =>
      let t_dom := reduced_product
        (AbTyps.t * (AbVarExpEq.t * (ZCongruences.t * (IdealIntervalsNonrel.t * PolAdomZ.A)))) _
      in
      let dom := idealenv_to_machineenv t_dom _ in
      let dom := if trace then debug_ab_machine_env verbose dom else dom in
      doit max_concretize trace verbose unroll dom p
    end.

End VA.