Module VarsUseDef

Specification of def/use sets for RTL instructions.

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

Require Import AST.
Require Import RTL.
Require Import Maps.
Require Import Integers.
Require Import Registers.
Require Import Op.

Require Import UtilTacs.
Require Import UtilLemmas.

Notation node := positive.

Local Open Scope positive_scope.

Variables are either memvar (special value indicating the memory) or a register. Variable indices are shifted by +1 with respect to register indices.

Definition var := positive.

Notation reg_to_var r := (Psucc r).
Notation var_to_reg r := (Ppred r).
Notation memvar := 1.
Notation varset := Regset.t.

Definition regs_to_vars (rs : list reg) : varset :=
  List.fold_left (fun rs0 r => Regset.add (reg_to_var r) rs0) rs Regset.empty.

Definition ros_to_var (ros : reg + ident) : varset :=
  match ros with
    | inl r => Regset.singleton (reg_to_var r)
    | inr id => Regset.empty
  end.

Definition optreg_to_var (o : option reg) : varset :=
  match o with
    | None => Regset.empty
    | Some arg => Regset.singleton (reg_to_var arg)
  end.

Definition def (f : function) (n : node) : varset :=
  match PTree.get n f.(fn_code) with
    | None => Regset.empty
    | Some i => match i with
                  | Inop s => Regset.empty
                  | Iop op args res s => Regset.singleton (reg_to_var res)
                  | Iload chunk addr args dst s => Regset.singleton (reg_to_var dst)
                  | Istore chunk addr args src s => Regset.singleton memvar
                  | Icall sig ros args res s => Regset.add memvar (Regset.singleton (reg_to_var res))
                  | Itailcall sig ros args => Regset.singleton memvar
                  | Ibuiltin ef args res s => match ef with
                                                  | EF_annot _ _
                                                  | EF_annot_val _ _ => Regset.singleton (reg_to_var res)
                                                  | _ => Regset.add memvar (Regset.singleton (reg_to_var res))
                                              end
                  | Icond cond args ifso ifnot => Regset.empty
                  | Ijumptable arg tbl => Regset.empty
                  | Ireturn optarg => Regset.empty
                end
  end.

Definition use (f : function) (n : node) : varset :=
  match PTree.get n f.(fn_code) with
    | None => Regset.empty
    | Some i => match i with
                  | Inop s => Regset.empty
                  | Iop op args res s =>
                    match op with
                      | Op.Ocmp c =>
                        match c with
                          | Op.Ccompu c' =>
                            Regset.add memvar (regs_to_vars args)
                          | _ => (regs_to_vars args)
                        end
                      | _ => (regs_to_vars args)
                    end
                  | Iload chunk addr args dst s => Regset.add memvar (regs_to_vars args)
                  | Istore chunk addr args src s => Regset.add memvar (regs_to_vars (src :: args))
                  | Icall sig ros args res s => Regset.union (Regset.add memvar (ros_to_var ros)) (regs_to_vars args)
                  | Itailcall sig ros args => Regset.union (Regset.add memvar (ros_to_var ros)) (regs_to_vars args)
                  | Ibuiltin ef args res s => match ef with
                                                  | EF_annot _ _
                                                  | EF_annot_val _ _ => regs_to_vars args
                                                  | _ => Regset.add memvar (regs_to_vars args)
                                              end
                  | Icond cond args ifso ifnot =>
                    match cond with
                      | Op.Ccompu c' =>
                        Regset.add memvar (regs_to_vars args)
                      | _ => (regs_to_vars args)
                    end
                  | Ijumptable arg tbl => Regset.singleton (reg_to_var arg)
                  | Ireturn optarg => optreg_to_var optarg
                end
  end.

Lemma In_fold_reg_to_var:
  forall rs rs' r,
    Regset.In (reg_to_var r) (fold_left (fun rs0 r' => Regset.add (reg_to_var r') rs0) rs rs') <->
    In r rs \/ Regset.In (reg_to_var r) rs'.

Proof.

  induction rs; simpl; intros; split; intros.
  right; asmp.
  nsolve.
  apply IHrs in H.
  destruct H.
  left. right. asmp.
  destruct (positive_eq_dec a r); subst.
  left. left. refl.
  apply Regset.add_3 in H.
  right. asmp.
  repeat rewrite <- Pplus_one_succ_r.
  intro.
  apply Psucc_inj in H0. contra.
  apply IHrs.
  destruct H.
  destruct H.
  subst.
  right. apply Regset.add_1. refl.
  left. asmp.
  right. apply Regset.add_2. asmp.
Qed.

Lemma In_regs_to_vars:
forall rs r,
Regset.In (reg_to_var r) (regs_to_vars rs) <-> In r rs.

Proof.

  unfold regs_to_vars.
  induction rs; simpl; intros.
  split; intro; nsolve.
  destruct (positive_eq_dec a r); subst.
  split; intro. left; refl.
  destruct H.
  rewrite In_fold_reg_to_var.
  right. apply Regset.add_1. refl.
  rewrite In_fold_reg_to_var.
  left. asmp.
  rewrite In_fold_reg_to_var.
  split; intros.
  destruct H. right. asmp.
  apply Regset.add_3 in H; auto. inv H.
  repeat rewrite <- Pplus_one_succ_r.
  intro.
  apply Psucc_inj in H0. contra.
  destruct H; nsolve.
Qed.

Lemma no_memvar_to_reg:
forall r, ~ reg_to_var r = memvar.

Proof.

intros. intro.
apply Psucc_not_one in H; auto.
Qed.

Hint Resolve no_memvar_to_reg.

Lemma var_to_var:
forall r,
var_to_reg (reg_to_var r) = r.

Proof.

  intros.
  rewrite Ppred_succ.
  refl.
Qed.

Lemma reg_to_reg:
forall x, x <> memvar -> (reg_to_var (var_to_reg x)) = x.

Proof.

  intros.
  destruct x; simpl; trim.
  rewrite <- Psucc_o_double_minus_one_eq_xO.
  lia2.
Qed.

Lemma def_Inop:
  forall f pc s,
    (fn_code f) ! pc = Some (Inop s) ->
    def f pc = Regset.empty.

Proof.