Module SliceGen

Validates a set of slice nodes and produces an executable sliced function.

Require Import Bool.
Require Import BinPos.
Require Import List.
Require Import TheoryList.
Require Import Arith.
Require Import Ndec.

Require Import Errors.
Require Import AST.
Require Import Globalenvs.
Require Import RTL.
Require Import Maps.
Require Import Registers.
Require Import Op.
Require Import Coqlib.

Require Import UtilTacs.
Require Import UtilBase.
Require Import UtilLemmas.
Require Import VarsUseDef.
Require Import RTLWfFunction.
Require Import RTLPaths.
Require Import SliceObs.
Require Import SliceRelVar.
Require Import SliceScopeExits.
Require Import Scope.
Require Import ValueAnalysis.
Require Import LocalBounds.

Local Open Scope positive_scope.
Open Scope error_monad_scope.


Definition icond_true (reg_vint : reg) (ifso ifnot : node): instruction :=
  Icond (Cmaskzero (reg_vint :: nil) ifso ifnot.

Definition icond_false (reg_vint : reg) (ifso ifnot : node): instruction :=
  Icond (Cmasknotzero (reg_vint :: nil) ifso ifnot.

Definition update_succs_icond (reg_vint : reg) (n : node) (ifso: node) (ifnot: node) (s_dobs: dobsT) (dexit : PTree.t N) : instruction :=
  let true_branch := icond_true reg_vint ifso ifnot in
  let false_branch := icond_false reg_vint ifso ifnot in
  match s_dobs ! n with
    | None =>
      match (dexit ! ifso, dexit ! ifnot) with
        | (Some dx1, Some dx2) =>
          if nle dx1 dx2 then true_branch
          else false_branch
        | _ => true_branch
    | Some (d, n') =>
      match (s_dobs ! ifso, s_dobs ! ifnot) with
        | (Some _, None) => true_branch
        | (None, Some _) => false_branch
        | (Some (d1, _, n1), Some (d2, _, n2)) =>
          if nle d1 d2 then true_branch
          else false_branch
        | (None, None) => true_branch

Returns the only successor of a instruction (if it only has one), None otherwise.
Definition successor_instr (i : instruction) : option node :=
  match i with
    | Inop s => Some s
    | Iop op args res s => Some s
    | Iload chunk addr args dst s => Some s
    | Istore chunk addr args sr s => Some s
    | Icall si ros args res s => Some s
    | Ibuiltin ef args res s => Some s
    | _ => None

Definition compute_bs_code (reg_vint : reg) (f : function) (bs_nodes : list node) (s_dobs : dobsT) (dexit : PTree.t N) : PTree.t instruction := (fun p i =>
    if mem positive_eq_dec p bs_nodes then i
      else match i with
             | Icond cond args ifso ifnot => update_succs_icond reg_vint p ifso ifnot s_dobs dexit
             | Ireturn o => Ireturn o
             | Itailcall sg fn args => Ireturn None
             | Ijumptable arg tbl => i
             | _ => match successor_instr i with
                      | Some s => Inop s
                      | None => i
  ) f.(fn_code).

Computes an executable slice from the list of slice nodes and auxiliary functions.
Definition compute_bs (reg_vint : reg) (f : function) (bs_nodes : list node) (s_dobs : dobsT) (dexit : PTree.t N) : function :=
  let bs_code := compute_bs_code reg_vint f bs_nodes s_dobs dexit in
    mkfunction f.(fn_sig) f.(fn_params) f.(fn_stacksize) bs_code f.(fn_entrypoint).


The external slicer function that produces the list of nodes which must be kept in the slice.
Parameter ext_slicer : function -> t_criterion -> res (list node).

Record obs_function : Type := mk_of {
  _slice_nodes : list node;
  _s_dobs : dobsT;
  _exit : node;
  _dexit : PTree.t N;
  _rvs : node -> varset;
  _reg_vint : reg

compute_slice computes a obs_function record containing the information necessary for an executable slice to be built.
Definition compute_slice (slicer_f : function -> t_criterion -> res (list node)) (f : function) (nc : t_criterion) (fsc : f) (exit_n : node) (reg_vint : reg) : res obs_function :=
  do slice_nodes <- slicer_f f nc;
  let s_dobs := f_dobs f nc slice_nodes in
    let dexit := f_dexit f exit_n in
    if s_dobs_checker f nc exit_n slice_nodes s_dobs dexit then
      let rvs := f_rvs f slice_nodes in
      if rvs_checker f slice_nodes rvs then
        if scope_exits_checker f fsc nc slice_nodes then
          OK (mk_of slice_nodes s_dobs exit_n dexit rvs reg_vint)
          Error ((MSG "scope_exits_checker failed") :: nil)
        Error ((MSG "rvs_checker failed") :: nil)
      Error ((MSG "s_dobs_checker failed") :: nil).

Definition slice_function (f: function) (nc : t_criterion) (fsc : f) (exit_n : node) (reg_vint : reg) : res (function * obs_function) :=
  do of <- compute_slice ext_slicer f nc fsc exit_n reg_vint;
    OK (compute_bs of.(_reg_vint) f of.(_slice_nodes) of.(_s_dobs) of.(_dexit), of).

The program transformation that produces an executable slice from an RTL function. It may fail if the function is not well-formed.
Definition transf_function (nc : t_criterion) (exit_n : node) (reg_vint : reg) (f: function) (fsc : f) : res function :=
  do (sliced_f, _) <- slice_function f nc fsc exit_n reg_vint;
  OK sliced_f.

Definition local_sliced_bound (f : function) ( f) (nc : t_criterion) : res Z :=
  if positive_eq_dec nc f.(fn_entrypoint) then OK 1%Z
      do (exit_n, reg_vint) <- check_wf f;
      do sliced_f <- transf_function nc exit_n reg_vint f fsc;
      let dom_reg := value sliced_f in
      let scope_nc := Scope.scope fsc nc in
      let nodes_nc := Scope.nodes scope_nc in
      do vars <- build_all_use_and_def sliced_f nc nodes_nc;
        if check_may_not_update_mem sliced_f nodes_nc then
          fold_left (fun rprod0 x =>
            do prod0 <- rprod0;
              do itv <- value sliced_f nc x;
                let res := ((itv_length itv) * prod0)%Z in
                  OK res
          ) vars (OK 1%Z)
          else Error (MSG ("local_bound failed: memory updates in function") :: nil).