Module CFGAnalysis

Require Import Coqlib.
Require Import Maps.
Require Import AST.
Require Import Integers.
Require Import Floats.
Require Import Values.
Require Import Globalenvs.
Require Import Op.
Require Import Registers.
Require Import Cminor.
Require Import CFG.
Require Import LatticeSignatures.
Require Import CfgIterator.
Require Import AbMemSignature.
Require Import Intervals.

Section abmem.
  Variable abmem: Type.
  Variable abdom: mem_dom (abmem+⊥).

  Let forget := forget _ abdom.
  Let assign := assign _ abdom.
  Let store := store _ abdom.
  Let assume := assume _ abdom.

  Definition transfer (n : node) (ins: instruction) : list (node*(abmem+⊥->abmem+⊥)) :=
    match ins with
      | Iskip s => (s,fun ab => ab) :: nil
      | Iassign x e s => (s, assign x e) :: nil
      | Istore chunk e a s => (s, store chunk e a) :: nil
      | Itailcall _ _ _ => nil
      | Icall None _ _ _ s
      | Ibuiltin None _ _ s => (s,fun ab => ab) :: nil
      | Icall (Some x) _ _ _ s
      | Ibuiltin (Some x) _ _ s => (s, forget x) :: nil
      | Iifthenelse e ifso ifno =>
        (ifso, assume e) :: (ifno, assume (Eunop Onotbool e)) :: nil
      | Iswitch e cases default =>
        map (fun s => (s,fun ab => ab)) (default::map snd cases)
      | Ireturn _ => nil
    end.

  Definition solve_pfp (f:function) : node -> abmem+⊥ :=
    BourdoncleIterator.solve_pfp (mem_adom _ abdom) f.(fn_entrypoint) f.(fn_code) transfer (@top _ _ (mem_adom _ abdom)).

  Definition value_analysis (f:function) : node -> (ident -> sign_flag -> Interval.itv+⊥)+⊥ :=
    let a := solve_pfp f in
      fun pc => range _ abdom (a pc).
End abmem.

Require AbMem.
Require Import BoxDomain.

Inductive num_dom_kind :=
| SignedOnly
| UnsignedOnly
| SignedAndUnsignedReduced
.

Require Import AbNumDomain.

Definition vanalysis (nk:num_dom_kind) :
  function -> node -> (ident -> sign_flag -> Interval.itv+⊥)+⊥ :=
  match nk with
    | SignedOnly =>
      value_analysis _ (AbMem.make (Box.abdom _ itv_num_correct))
    | UnsignedOnly =>
      value_analysis _ (AbMem.make (Box.abdom _ UInterval.itvu_num_correct))
    | SignedAndUnsignedReduced =>
      value_analysis _ (AbMem.make (Box.abdom _ intervals_correct))
  end.