Module SliceScopeExits

Complementary validation of program slicing and scopes.

Require Import Coqlib.
Require Import Integers.
Require Import Errors.
Require Import RTL.
Require Import Maps.

Require Import RTLPaths.
Require Import Scope.

Notation In_dec_node := (List.In_dec positive_eq_dec).

scope_exits_checker succs slice_nodes scope_list returns true if the desired property is verified on the scopes, which always happens for well-formed functions.

  Definition scope_exits_checker (f : function) (fsc : Scope.family f) (nc : node) (slice_nodes : list node) : bool :=
    PTree.fold (fun b0 n succs_n =>
      b0 &&
      (In_dec_node n slice_nodes ||
        List.forallb (fun s =>
          List.forallb (fun n' =>
            negb (In_dec_node n' slice_nodes)
          ) (exited_scopes fsc n s)
        ) succs_n)
    ) (successors f) true.