Module CsharpminorIter


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

Open Scope string_scope.

Axiom fuel : nat.

Section abmem.

Context {abstate abstate_iter:Type} {abmem:mem_dom 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 (abstate+⊥)) : alarm_mon 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 outcome)
         (x:abstate+⊥) (y:abstate_iter): alarm_mon 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 outcome) (lb:abstate+⊥)
         (steps:nat) (cur:alarm_mon outcome) : alarm_mon outcome :=
  match steps with
  | S steps =>
    if is_bot (fst cur).(onormal) then cur
    else
      let next := f (lb ⊔ (fst cur).(onormal)) in
      match snd cur, 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 outcome) (lb:abstate+⊥) : alarm_mon 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 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 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 unit :=
  fold_left2
    (fun (q: alarm_mon 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 (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 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 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 al sz dst src state
          end
        | _ => do _ <- alarm_am "memcpy used without the right number of arguments";
               ret Bot
      end
    | EF_vload κ => ab_vload rettemp None κ args state
    | EF_vstore κ => ab_vstore rettemp None κ args state
    | EF_malloc =>
      match args with
        | sz::nil => ab_malloc 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 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 (abstate+⊥).

Variable rettemp: option ident.

Fixpoint default_abstate_switch
         (islong:bool)
         (st:abstate) (e:expr) (s:lbl_stmt) : alarm_mon (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
            (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 outcome :=
  match s with
  | Sskip => ret (ABS inormal Bot nil bot_goto)
  | Sstore chunk b c =>
    do_normal inormal <- inormal;
    store chunk b c inormal
  | Sset x b =>
    do_normal inormal <- inormal;
    assign x b inormal
  | Scall x sig b cl =>
    do_normal inormal <- inormal;
    do funcs <- deref_fun b inormal;
    List.fold_left (fun prev fn =>
        do onormal <- iter_function sig (fst fn) (snd fn) x cl inormal;
        do prevnormal <- prev;
        ret (onormalprevnormal))
      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 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 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 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
            (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 outcome :=
  match sl with
  | LSnil => ret (ABS (iprevidefault) 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
                  (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 (iprevicase) 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 ab then None else Some tt
    end)
    a b
  in
  PTree.bempty t.

Fixpoint pfp_narrow_goto (f:PTree.t abstate -> alarm_mon outcome)
         (steps:nat) (cur:alarm_mon outcome) : alarm_mon 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 snd cur, 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 outcome)
         (x:PTree.t abstate) (y:PTree.t abstate_iter): alarm_mon 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 outcome) : alarm_mon 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 (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 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 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 unit :=
  do mem <- init_mem 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.