Module CsharpminorIter

Require Import Coqlib.
Require Import Maps.
Require Import Integers.
Require Import AST.
Require Import Globalenvs.
Require Import AdomLib.
Require Import AbMemSignatureCsharpminor.
Import Csharpminorannot.
Require Import String.
Require Import DebugLib.
Require Import AlarmMon.
Require Import Util.

Open Scope string_scope.

Axiom fuel : nat.

Section abmem.

Context (L: Type) {abstate abstate_iter:Type} {abmem:mem_dom L abstate abstate_iter}.

Variable (unroll: nat).
Variable (prog: program).
Let ge := Genv.globalenv prog.

Existing Instance abmem.

Record outcome := ABS {
  onormal: abstate+⊥;
  oreturn: abstate+⊥;
  oexit: list (abstate+⊥);
  ogoto: PTree.t abstate
}.

Definition bot_goto := PTree.empty abstate.

Instance join_goto : join_op (PTree.t abstate) (PTree.t abstate) :=
  PTree.combine (fun a b =>
    match a, b with
      | Some a, Some b => match join a b with NotBot x => Some x | Bot => None end
      | Some x, None | None, Some x => Some x
      | None, None => None
    end).

Instance join_exit : join_op (list (abstate+⊥)) (list (abstate+⊥)) := fix join_exit l1 l2 :=
  match l1 with
    | nil => l2
    | t1::q1 =>
      match l2 with
        | nil => l1
        | t2 :: q2 =>
          let t :=
              match t1, t2 with
                | NotBot t1, NotBot t2 => join t1 t2
                | Bot, x | x, Bot => x
              end
          in
          t :: join_exit q1 q2
      end
  end.

Definition bind_normal_outcome (inormal:abstate+⊥) (f:abstate -> alarm_mon L (abstate+⊥)) : alarm_mon L outcome :=
  match inormal with
    | Bot => ret (ABS Bot Bot nil bot_goto)
    | NotBot inormal =>
      do onormal <- f inormal;
      ret (ABS onormal Bot nil bot_goto)
  end.

Notation "'do_normal' X <- A ; B" := (bind_normal_outcome A (fun X => B))
 (at level 200, X ident, A at level 100, B at level 200).

Fixpoint pfp_widen (fuel:nat) (f:abstate+⊥ -> alarm_mon L outcome)
         (x:abstate+⊥) (y:abstate_iter): alarm_mon L outcome :=
  let fx := f x in
  match fuel with
  | S fuel =>
    if (fst fx).(onormal) ⊑ x then fx
    else
      let '(y, x) := y ▽ (fst fx).(onormal) in
      pfp_widen fuel f x y
  | O =>
    do _ <- alarm_am "Not enough fuel to reach a fixpoint";
    fx
  end.

Definition narrowing_steps := 1%nat.

Fixpoint pfp_narrow (f : abstate+⊥ -> alarm_mon L outcome) (lb:abstate+⊥)
         (steps:nat) (cur:alarm_mon L outcome) : alarm_mon L outcome :=
  match steps with
  | S steps =>
    if is_bot (fst cur).(onormal) then cur
    else
      let next := f (lb ⊔ (fst cur).(onormal)) in
      match fst (snd cur), fst (snd next) with
      | nil, nil | _ :: _, _ :: _ => pfp_narrow f lb steps next
      | nil, _ :: _ => cur
      | _ :: _, nil =>
        if (fst next).(onormal) ⊑ (fst cur).(onormal) then pfp_narrow f lb steps next
        else cur
      end
  | O => cur
  end.

Definition pfp (f : abstate+⊥ -> alarm_mon L outcome) (lb:abstate+⊥) : alarm_mon L outcome :=
  let fp := pfp_widen fuel f lb (init_iter lb) in
  pfp_narrow f lb narrowing_steps fp.

Section stmt_iterator.

Definition type_check_expr (ty: typ) (exp: expr) (state: abstate) : alarm_mon L unit :=
  match match ty with
        | Tint => Some Cminor.Onegint
        | Tfloat => Some Cminor.Onegf
        | Tlong => Some Cminor.Onegl
        | Tsingle => Some Cminor.Onegfs
        | _ => None
        end
  with
  | Some op =>
    let e := Eunop op exp in
    noerror L e state
  | None => do _ <- alarm_am "type_check_expr: unsupported type"; ret tt
  end.

Definition type_check_list (targs: list typ) (args: list expr) (state: abstate) : alarm_mon L unit :=
  fold_left2
    (fun (q: alarm_mon L unit) ty exp => do _ <- q; type_check_expr ty exp state)
    (fun _ _ => do _ <- alarm_am "type_check_list: too many types"; ret tt)
    (fun _ _ => do _ <- alarm_am "type_check_list: too many arguments"; ret tt)
    targs args (ret tt).

Definition ab_builtin (ef:external_function) (rettemp:option ident)
                      (args:list expr) (state:abstate) : alarm_mon L (abstate+⊥) :=
  match ef with
    | EF_external id sig =>
      do _ <- alarm_am ("Call to external function " ++ id); ret Bot
    | EF_builtin _ _ => do _ <- alarm_am "Builtin are not supported"; ret Bot
    | EF_inline_asm _ _ _ => do _ <- alarm_am "Inline ASM is not supported"; ret Bot
    | EF_annot text targs =>
      do _ <- match rettemp with
              | None => type_check_list targs args state
              | Some _ => alarm_am "Use of return value of annot"
              end;
      ret (NotBot state)
    | EF_annot_val text targ =>
      match args with
      | earg :: nil =>
        do _ <- type_check_expr targ earg state;
          match rettemp with
          | Some x => assign L x earg state
          | None => ret (NotBot state)
          end
      | _ => do _ <- alarm_am "Wrong number of arguments in annot_val";
          ret (NotBot state)
      end
    | EF_debug _ _ _ =>
      do _ <- match rettemp with
              | None => am_fold (fun _ e => noerror L e state) args tt
              | Some _ => alarm_am "Use of return value of debug"
              end;
      ret (NotBot state)
    | EF_memcpy al sz =>
      match args with
        | dst::src::nil =>
          match rettemp with
            | Some _ => do _ <- alarm_am "Use of return value of memcpy";
                        ret Bot
            | None => ab_memcpy L al sz dst src state
          end
        | _ => do _ <- alarm_am "memcpy used without the right number of arguments";
               ret Bot
      end
    | EF_vload κ => ab_vload L rettemp None κ args state
    | EF_vstore κ => ab_vstore L rettemp None κ args state
    | EF_malloc =>
      match args with
        | sz::nil => ab_malloc L sz rettemp state
        | _ => do _ <- alarm_am "malloc used without the right number of arguments";
               ret Bot
      end
    | EF_free =>
      match args with
        | ptr::nil =>
          match rettemp with
            | Some _ => do _ <- alarm_am "Use of return value of free";
                        ret Bot
            | None => ab_free L ptr state
          end
        | _ => do _ <- alarm_am "free used with at least one parameter";
               ret Bot
      end
  end.

Variable iter_function:
  forall (sig:signature)
         (name: ident) (function:fundef) (rettemp:option ident)
         (args:list expr) (state:abstate), alarm_mon L (abstate+⊥).

Variable rettemp: option ident.

Fixpoint default_abstate_switch
         (islong:bool)
         (st:abstate) (e:expr) (s:lbl_stmt) : alarm_mon L (abstate+⊥) :=
  match s with
    | LSnil => ret (NotBot st)
    | LScons None _ s => default_abstate_switch islong st e s
    | LScons (Some n) _ s =>
      if zlt n 0 ||
         zlt (if islong then Int64.max_unsigned else Int.max_unsigned) n then
        default_abstate_switch islong st e s
      else
        do sts <-
          assume L
            (if islong then Ebinop (Cminor.Ocmpl Ceq) e (Econst (Olongconst (Int64.repr n)))
             else Ebinop (Cminor.Ocmp Ceq) e (Econst (Ointconst (Int.repr n))))
            st;
        match sts with
          | (_, NotBot st) => default_abstate_switch islong st e s
          | _ => ret Bot
        end
  end.

Definition verasco_unroll_ident := "verasco_unroll"%string.

Fixpoint unroll_call_lookup_aux (s:stmt) : Z :=
  match s with
    | Sseq s1 s2 => Z.max (unroll_call_lookup_aux s1) (unroll_call_lookup_aux s2)
    | Sblock s => unroll_call_lookup_aux s
    | Sbuiltin _ (EF_annot id _) (Econst (Ointconst i)::nil) =>
      if string_dec id verasco_unroll_ident then Int.unsigned i
      else 0
    | _ => 0
  end.

Definition unroll_call_lookup (s:stmt) (unroll:nat) : nat :=
  Z.abs_nat (Z.max (unroll_call_lookup_aux s) (Z.of_nat unroll)).

Fixpoint iter (inormal:abstate+⊥) (igoto:PTree.t abstate) (s: stmt) : alarm_mon L outcome :=
  match s with
  | Sskip => ret (ABS inormal Bot nil bot_goto)
  | Sstore α chunk b c =>
    do_normal inormal <- inormal;
    store L α chunk b c inormal
  | Sset x b =>
    do_normal inormal <- inormal;
    assign L x b inormal
  | Scall x sig b cl =>
    do_normal inormal <- inormal;
    do funcs <- deref_fun L b inormal;
    List.fold_left (fun prev fn =>
        do onormal <- iter_function sig (fst fn) (snd fn) x cl inormal;
        do prevnormal <- prev;
        ret (onormal ⊔ prevnormal))
      funcs (ret Bot)
  | Sbuiltin x ef bl =>
    do_normal inormal <- inormal;
    ab_builtin ef x bl inormal
  | Sseq s1 s2 =>
    do o1 <- iter inormal igoto s1;
    do o2 <- iter o1.(onormal) igoto s2;
    ret (ABS o2.(onormal)
                (o1.(oreturn) ⊔ o2.(oreturn))
                (o1.(oexit) ⊔ o2.(oexit))
                (o1.(ogoto) ⊔ o2.(ogoto)))
  | Sifthenelse e s1 s2 =>
    do inormals <-
      match inormal with
        | Bot => ret (Bot, Bot)
        | NotBot inormal => assume L e inormal
      end;
    let (inormaltrue, inormalfalse) := inormals in
    do o1 <- iter inormaltrue igoto s1;
    do o2 <- iter inormalfalse igoto s2;
    ret (ABS (o1.(onormal) ⊔ o2.(onormal))
                (o1.(oreturn) ⊔ o2.(oreturn))
                (o1.(oexit) ⊔ o2.(oexit))
                (o1.(ogoto) ⊔ o2.(ogoto)))
  | Sloop s =>
    let unroll := unroll_call_lookup s unroll in
    let fix unroll_loop (n:nat) (inormal:abstate+⊥) (igoto:PTree.t abstate): alarm_mon L outcome :=
        match n with
          | O =>
            do fp <- pfp (fun loopnormal => iter loopnormal igoto s) inormal;
            ret (ABS Bot fp.(oreturn) fp.(oexit) fp.(ogoto))
          | S n =>
            do o1 <- iter inormal igoto s;
            match o1.(onormal) with
              | Bot =>
                ret (ABS Bot o1.(oreturn) o1.(oexit) o1.(ogoto))
              | _ =>
                do o2 <- unroll_loop n o1.(onormal) bot_goto;
                ret (ABS o2.(onormal)
                            (o1.(oreturn) ⊔ o2.(oreturn))
                            (o1.(oexit) ⊔ o2.(oexit))
                            (o1.(ogoto) ⊔ o2.(ogoto)))
            end
        end in
    unroll_loop unroll inormal igoto
  | Sblock s =>
    do o <- iter inormal igoto s;
    ret (ABS (o.(onormal) ⊔ List.hd Bot o.(oexit))
                o.(oreturn)
                (List.tl o.(oexit))
                o.(ogoto))
  | Sexit n =>
    ret (ABS Bot Bot (nat_iter n (cons Bot) (cons inormal nil)) bot_goto)
  | Sreturn r =>
    match inormal with
      | Bot => ret (ABS Bot Bot nil bot_goto)
      | NotBot inormal =>
        do oreturn <- pop_frame L r rettemp inormal;
        ret (ABS Bot oreturn nil bot_goto)
    end
  | Sswitch islong a sl =>
    do idefault <-
      match inormal with
        | Bot => ret Bot
        | NotBot inormal =>
          do _ <- noerror L
            (Eunop (if islong then Cminor.Onegl else Cminor.Onegint) a) inormal;
          default_abstate_switch islong inormal a sl
      end;
    iter_switch islong inormal idefault Bot igoto a sl
  | Slabel lbl s =>
    iter (inormal ⊔
            match PTree.get lbl igoto with
              | None => Bot
              | Some ab => NotBot ab
            end) igoto s
  | Sgoto lbl =>
    ret (ABS Bot Bot nil
                (match inormal with
                   | Bot => bot_goto
                   | NotBot inormal => PTree.set lbl inormal bot_goto
                 end))
  end

with iter_switch (islong:bool) (inormal:abstate+⊥) (idefault iprev:abstate+⊥)
                 (igoto:PTree.t abstate) (e:expr) (sl: lbl_stmt)
     : alarm_mon L outcome :=
  match sl with
  | LSnil => ret (ABS (iprev ⊔ idefault) Bot nil bot_goto)
  | LScons o s sl' =>
    do icaseidefault <-
      match o with
        | None => ret (idefault, Bot)
        | Some n =>
          do icase <-
            match inormal with
              | Bot => ret Bot
              | NotBot inormal =>
                do abs <- assume L
                  (if islong then Ebinop (Cminor.Ocmpl Ceq) e (Econst (Olongconst (Int64.repr n)))
                   else Ebinop (Cminor.Ocmp Ceq) e (Econst (Ointconst (Int.repr n))))
                  inormal;
                ret (fst abs)
            end;
          ret (icase, idefault)
      end;
    let '(icase, idefault) := icaseidefault in
    do o1 <- iter (iprev ⊔ icase) igoto s;
    do o2 <- iter_switch islong inormal idefault o1.(onormal) igoto e sl';
    ret (ABS o2.(onormal)
                (o1.(oreturn) ⊔ o2.(oreturn))
                (o1.(oexit) ⊔ o2.(oexit))
                (o1.(ogoto) ⊔ o2.(ogoto)))
  end.

End stmt_iterator.

Instance leb_goto : leb_op (PTree.t abstate) := fun a b =>
  let t := PTree.combine (fun na nb =>
    match na, nb with
      | None, _ => None
      | Some _, None => Some tt
      | Some a, Some b => if a ⊑ b then None else Some tt
    end)
    a b
  in
  PTree.bempty t.

Fixpoint pfp_narrow_goto (f:PTree.t abstate -> alarm_mon L outcome)
         (steps:nat) (cur:alarm_mon L outcome) : alarm_mon L outcome :=
  match steps with
  | S steps =>
    if leb_goto (fst cur).(ogoto) bot_goto then cur
    else
      let next := f (fst cur).(ogoto) in
      match fst (snd cur), fst (snd next) with
      | nil, nil | _::_, _::_ => pfp_narrow_goto f steps next
      | nil, _ :: _ => cur
      | _ :: _, nil =>
        if leb_goto (fst next).(ogoto) (fst cur).(ogoto) then pfp_narrow_goto f steps next
        else cur
      end
  | O => cur
  end.

Definition widen_goto (x:PTree.t abstate_iter) (y:PTree.t abstate)
  : PTree.t abstate_iter * PTree.t abstate :=
  let w :=
      PTree.combine
        (fun nx ny =>
           match nx, ny with
           | None, None => None
           | _, _ =>
             Some ((match nx with Some x => x | None => init_iter Bot end) ▽
                   (match ny with Some y => NotBot y | None => Bot end))
           end)
        x y
  in
  (PTree.map1 fst w,
   PTree.combine
     (fun a _ =>
        match a with
        | Some (_, NotBot a) => Some a
        | _ => None
        end)
     w (PTree.empty False)).

Fixpoint pfp_widen_goto (fuel:nat) (f:PTree.t abstate -> alarm_mon L outcome)
         (x:PTree.t abstate) (y:PTree.t abstate_iter): alarm_mon L outcome :=
  let fx := f x in
  match fuel with
  | S fuel =>
    if leb_goto (fst fx).(ogoto) x then fx
    else
      let '(y, x) := widen_goto y (fst fx).(ogoto) in
      pfp_widen_goto fuel f x y
  | O =>
    do _ <- alarm_am "Not enough fuel to reach a fixpoint for gotos";
    fx
  end.

Definition pfp_goto (f : PTree.t abstate -> alarm_mon L outcome) : alarm_mon L outcome :=
  let fp := pfp_widen_goto fuel f bot_goto (PTree.empty _) in
  pfp_narrow_goto f narrowing_steps fp.

Fixpoint labels_stmt (s:stmt) : PTree.t unit :=
  match s with
    | Sskip | Sstore _ _ _ _ | Sset _ _ | Scall _ _ _ _ | Sbuiltin _ _ _
    | Sexit _ | Sreturn _ | Sgoto _ => PTree.empty unit
    | Sseq s1 s2 | Sifthenelse _ s1 s2 =>
      PTree.combine (fun x y => match x, y with None, None => None | _, _ => Some tt end)
        (labels_stmt s1) (labels_stmt s2)
    | Sloop s | Sblock s => labels_stmt s
    | Sswitch _ _ s => labels_sl s
    | Slabel lbl s => PTree.set lbl tt (labels_stmt s)
  end
with labels_sl (s:lbl_stmt) : PTree.t unit :=
  match s with
    | LSnil => PTree.empty unit
    | LScons _ s1 s2 =>
      PTree.combine (fun x y => match x, y with None, None => None | _, _ => Some tt end)
        (labels_stmt s1) (labels_sl s2)
  end.

Fixpoint iter_function (fuel:nat) (sig:signature) (name: ident) (fn:fundef) (rettemp:option ident)
                       (params:list expr) (istate:abstate) : alarm_mon L (abstate+⊥) :=
  match fuel with
    | O => do _ <- alarm_am "Not enough fuel for call stack depth";
           ret Bot
    | S fuel =>
      if signature_eq sig (funsig fn) then
        match fn with
          | Internal fn =>
              do _ <-
                if list_norepet_dec Pos.eq_dec (List.map fst fn.(fn_vars)) then ret tt
                else alarm_am "Repeating fn_vars";
              do _ <-
                if list_norepet_dec Pos.eq_dec (fn.(fn_params)) then ret tt
                else alarm_am "Repeating fn_params";
              do _ <-
                if list_disjoint_dec Pos.eq_dec (fn.(fn_params)) (fn.(fn_temps)) then ret tt
                else alarm_am "Non disjoint fn_params and fn_temps";
              do inormal <- push_frame L fn params istate;
              do o <- pfp_goto
                (fun igoto => iter (iter_function fuel) rettemp inormal igoto fn.(fn_body));
              do _ <-
                match o.(oexit) with
                  | nil => ret tt
                  | _::_ => alarm_am "Non-scoped exit"
                end;
              do _ <-
                if PTree.bempty
                     (PTree.combine (fun x y => match x, y with Some _, None => Some tt | _, _ => None end)
                                    o.(ogoto) (labels_stmt fn.(fn_body)))
                then ret tt
                else alarm_am "goto with unbound label";
                  do end_return_state <-
                    match o.(onormal) with
                      | Bot => ret Bot
                      | NotBot onormal => pop_frame L None rettemp onormal
                    end;
                  ret (o.(oreturn) ⊔ end_return_state)
          | External ext => ab_builtin ext rettemp params istate
        end
      else
        do _ <- alarm_am ("Could not prove that the called function ("++ string_of_ident name ++ ") has the right signature.");
        ret Bot
  end.

Definition iter_program : alarm_mon L unit :=
  do mem <- init_mem L prog.(prog_defs);
  match mem with
    | Bot => ret tt
    | NotBot mem =>
      match Genv.find_symbol ge prog.(prog_main) with
        | None => alarm_am "Could not find main symbol"
        | Some b =>
          match Genv.find_funct_ptr ge b with
            | None => alarm_am "Could not find the code of the main function"
            | Some fn =>
              do _ <- am_assert
                    match fn with Internal _ | External (EF_external _ _) => true | _ => false end
                    "Main function is a builtin";
              do end_mem <- iter_function fuel
                (mksignature nil (Some AST.Tint) cc_default)
                prog.(prog_main) fn None nil mem;
              ret tt
          end
      end
  end.

End abmem.