Module RTLWfFunction

Require Import Bool.
Require Import Arith.
Require Import List.
Require Import BinPos.

Require Import Coqlib.
Require Import Maps.
Require Import RTL.
Require Import Lattice.
Require Import Kildall.
Require Import Registers.
Require Import Errors.
Require Import Integers.

Require Import UtilBase.
Require Import UtilTacs.
Require Import Utils.
Require Import VarsUseDef.
Require Import RTLReaches.

Open Scope error_monad_scope.




Definition wf_cond_acc (f : function) : bool :=
  forall_ptree (fun p i => forallb (fun s => Pmem s f.(fn_code)) (successors_instr i)) f.(fn_code).

Definition wf_cond_entry (f : function) : bool :=
  forall_ptree (fun p i => forallb (fun s => negb (positive_eq_dec s f.(fn_entrypoint))) (successors_instr i)) f.(fn_code).

Definition wf_entry_acc (f : function) : bool :=
  match RTLReaches.transf_function f with
      | Error _ => false
      | OK (seen, tf) =>
        forall_ptree (fun p i => TheoryList.mem positive_eq_dec p seen) f.(fn_code)
  end.

Definition check_inst_entry (i : instruction) : res reg :=
  match i with
      | Iop op args res s =>
        match op with
          | Op.Ointconst i' =>
            if Int.eq_dec i' Int.zero then
              match args with
                | nil => OK res
                | _ => Error (MSG "inst_entry: args <> nil" :: nil)
              end
            else
              Error (MSG "inst_entry: val <> 0" :: nil)
          | _ => Error (MSG "inst_entry: op <> Ointconst" :: nil)
        end
      | _ => Error (MSG "inst_entry: not Iop" :: nil)
  end.

Definition f_exit (f : function) : res node :=
    let exits := List.filter (fun p_i => match snd p_i with
                                           | Itailcall _ _ _ => true
                                           | Ijumptable _ tbl => match tbl with
                                                                     | nil => true
                                                                     | _ => false
                                                                 end
                                           | Ireturn _ => true
                                           | _ => false
                                         end) (PTree.elements f.(fn_code)) in
    match exits with
      | nil => Error (MSG "f_exit: no exit" :: nil)
      | p_exit_n :: nil => match snd p_exit_n with
                               | Ireturn _ => OK (fst p_exit_n)
                               | _ => Error (MSG "f_exit: no tailcall/empty jumptable allowed" :: nil)
                           end
      | _ => Error (MSG "f_exit: too many exits" :: nil)
    end.

Definition check_valid_rs_function (f: function) : res reg :=
  match (fn_code f) ! (fn_entrypoint f) with
      | None => Error (MSG "check_valid_rs_function: entrypoint not in function" :: nil)
      | Some i =>
        do reg_vint <- check_inst_entry i;
          let vvint := reg_to_var reg_vint in
          if
          forall_ptree
            (fun n i =>
               if positive_eq_dec n f.(fn_entrypoint) then true
               else negb (Regset.mem vvint (def f n))
            ) f.(fn_code)
          then OK reg_vint
          else Error (MSG "check_valid_rs_function: reg_vint defd/used in function" :: nil)
  end.

Definition check_wf (f : function) : res (node * reg) :=
  if wf_cond_acc f && wf_cond_entry f && wf_entry_acc f then
    do exit <- f_exit f;
    do reg_vint <- check_valid_rs_function f;
    OK (exit, reg_vint)
else
  Error (MSG "check_wf: invalid function" :: nil).