Module SliceObs

Observable nodes validator.

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

Require Import Coqlib.
Require Import RTL.
Require Import Maps.
Require Import Errors.
Require Import Op.

Require Import UtilTacs.
Require Import UtilLemmas.
Require Import UtilBase.
Require Import RTLPaths.

Notation t_criterion := node.

Require Import Utils.

Local Open Scope positive_scope.

Definition dobsT := PTree.t (N * N * node).

A posteriori validation of observables

f_dobs f nc slice_nodes computes an association between each node and: its observable; the distance until its observable; the distance until the criterion.
Parameter f_dobs : function -> node -> list node -> dobsT.

f_dexit f exit_n computes an association between each node and its distance until the (unique and reachable) exit node.
Parameter f_dexit : function -> node -> PTree.t N.

Conversion dobs -> obs (distance erasure), useful for proofs and also for some OCaml code.
Definition obs (dobs : dobsT) : node -> option node :=
  fun n => match PTree.get n dobs with
             | None => None
             | Some (d, dc, n') => Some n'
           end.

First we define the conditions the checker will verify, then we define the function that uses them.

Definition checker_dist_exit (n exit_n : node) (succs : list node) (unchecked_dexit : PTree.t N) : bool :=
  match PTree.get n unchecked_dexit with
      | None => false
      | Some dx =>
        if positive_eq_dec n exit_n then Neqb dx 0%N
        else
          forallb (fun s =>
                     match PTree.get s unchecked_dexit with
                       | None => false
                       | Some dx' => nle dx (dx'+1)%N
                     end) succs
                  &&
                  existsb (fun s =>
                             match PTree.get s unchecked_dexit with
                               | None => false
                               | Some dx' => Neqb dx (dx'+1)
                             end) succs
  end.
  

Definition checker_cond_none (succs : list node) (n : node) (exit_n : node) (unchecked_s_dobs : dobsT) (unchecked_dexit : PTree.t N) : bool :=
  forallb (fun s => option_N_N_node_beq (PTree.get s unchecked_s_dobs) None) succs.

Definition checker_cond_some1 (succs : list node) (n : node) (d : N) (dc : N) (unchecked_s_dobs : dobsT) : bool :=
  forallb (fun s => match PTree.get s unchecked_s_dobs with
                      | None => true
                      | Some (d', dc', n') => Peqb n n' && nle (d-1)%N d' && nle (dc-1)%N dc'
                    end) succs.

Definition checker_cond_some2 (succs : list node) (d : N) (dc : N) (unchecked_s_dobs : dobsT) : bool :=
  existsb (fun s => match PTree.get s unchecked_s_dobs with
                      | None => false
                      | Some (d', dc', _) => Neqb d' (d-1) && Neqb dc' (dc-1)
                    end) succs.

Definition checker_cond_control (succs : list node) (unchecked_s_dobs : dobsT) : bool :=
  forallb (fun s => option_none_beq (unchecked_s_dobs ! s) None) succs ||
  forallb (fun s => negb (option_none_beq (unchecked_s_dobs ! s) None)) succs.

Definition checker_cond_not_jumptable (i : instruction) : bool :=
  match i with
    | Ijumptable _ _ => false
    | _ => true
  end.

Definition checker_cond_some2_in_slice (succs : list node) (dc : N) (unchecked_s_dobs : dobsT) : bool :=
  existsb (fun s => match unchecked_s_dobs ! s with
                      | None => false
                      | Some (_, dc', _) => Neqb dc' (dc-1)
                    end) succs.

Definition checker_cond_in_slice (p : node) (o : option (N * N * node)) (succs : list node) (unchecked_s_dobs : dobsT) :=
  match o with
      | None => false
      | Some (d, dc, o') => N_eq_dec d N0 && nlt 0%N dc && positive_eq_dec p o' && checker_cond_some2_in_slice succs dc unchecked_s_dobs
  end.

Definition s_dobs_checker (f : function) (nc : t_criterion) (exit_n : node) (slice_nodes : list node) (unchecked_s_dobs : dobsT) (unchecked_dexit : PTree.t N) : bool :=
  (List.forallb (fun n' => Pmem n' f.(fn_code)) slice_nodes) &&
  (forall_ptree (fun n' _ => Pmem n' f.(fn_code)) unchecked_s_dobs) &&
  (option_N_N_node_beq (PTree.get nc unchecked_s_dobs) (Some (N0, N0, nc))) &&
  mem positive_eq_dec (fn_entrypoint f) slice_nodes &&
  mem positive_eq_dec nc slice_nodes &&
  (Pmem exit_n f.(fn_code) && option_beq N N_eq_dec (unchecked_dexit ! exit_n) (Some 0%N)) &&
  PTree.fold (fun b0 p i =>
    b0 && (
      let pobs := PTree.get p unchecked_s_dobs in
      let succs := successors_instr i in
      checker_dist_exit p exit_n succs unchecked_dexit &&
      if mem positive_eq_dec p slice_nodes then
        if positive_eq_dec p nc then
          option_N_N_node_beq pobs (Some (N0, N0, p))
        else
          checker_cond_in_slice p pobs succs unchecked_s_dobs
      else
        checker_cond_not_jumptable i &&
        (if gt_dec (length succs) 1%nat then
           checker_cond_control succs unchecked_s_dobs else true) &&
           match pobs with
             | None => checker_cond_none succs p exit_n unchecked_s_dobs unchecked_dexit
             | Some (d, dc, n) => nlt 0%N d && nle d dc && negb (positive_eq_dec p n) && checker_cond_some1 succs n d dc unchecked_s_dobs && checker_cond_some2 succs d dc unchecked_s_dobs
           end)
  ) f.(fn_code) true.
Generated by coq2html