Relevant variables validator.
Require Import Bool.
Require Import BinPos.
Require Import List.
Require Import TheoryList.
Require Import Arith.
Require Import Coqlib.
Require Import RTL.
Require Import Maps.
Require Import Registers.
Require Import UtilTacs.
Require Import UtilLemmas.
Require Import UtilBase.
Require Import RTLPaths.
Require Import VarsUseDef.
Require Import Utils.
Part of the slicing checker that verifies properties about relevant variables.
Local Notation "
a '
IN'
b" := (
Regset.mem a b) (
at level 30,
no associativity).
f_rvs f slice_nodes builds function rvs : node -> varset
that maps l to RV(l).
Parameter f_rvs :
function ->
list node ->
node ->
varset.
First we define the checks to be performed, then the function that calls them.
Definition check_uses_in_rvs (
use_n rvs_n :
varset) :
bool :=
Regset.subset use_n rvs_n.
Definition check_not_mem_def (
def_n rvs_n :
varset) (
succs :
list node)
(
unchecked_rvs :
node ->
varset) :
bool :=
List.forallb
(
fun s =>
let rvs_s :=
unchecked_rvs s in
if memvar IN rvs_s &&
memvar IN def_n &&
memvar IN rvs_n then
false else true)
succs.
Definition check_not_in_def_in_rvs (
def_n rvs_n :
varset) (
succs :
list node)
(
unchecked_rvs :
node ->
varset) :
bool :=
List.forallb
(
fun s =>
let rvs_s :=
unchecked_rvs s in
Regset.for_all (
fun v =>
v IN def_n ||
v IN rvs_n)
rvs_s
)
succs.
Definition check_not_in_slice_succ_rvs (
rvs_n :
varset) (
succs :
list node)
(
unchecked_rvs :
node ->
varset) :
bool :=
List.forallb
(
fun s =>
let rvs_s :=
unchecked_rvs s in
Regset.for_all (
fun v =>
v IN rvs_n)
rvs_s
)
succs.
Definition check_not_in_slice_def_not_in_rvs (
def_n rvs_n :
varset) :
bool :=
Regset.for_all (
fun v =>
negb (
v IN rvs_n))
def_n.
Definition rvs_checker (
f :
function) (
slice_nodes :
list node)
(
unchecked_rvs :
node ->
varset) :
bool :=
PTree.fold (
fun b0 n i =>
b0 && (
let succs :=
successors_instr i in
let '(
def_n,
use_n,
rvs_n) := (
def f n,
use f n,
unchecked_rvs n)
in
check_not_in_def_in_rvs def_n rvs_n succs unchecked_rvs &&
if mem positive_eq_dec n slice_nodes then
check_uses_in_rvs use_n rvs_n
else
check_not_mem_def def_n rvs_n succs unchecked_rvs &&
check_not_in_slice_succ_rvs rvs_n succs unchecked_rvs &&
check_not_in_slice_def_not_in_rvs def_n rvs_n
)
)
f.(
fn_code)
true.
Properties verified by the checker.
Record checked_rvs (
f :
function) (
slice_nodes :
list node) (
rvs :
node ->
varset) :
Prop := {
checked_not_in_def_in_rvs :
forall n i s v,
(
fn_code f) !
n =
Some i ->
In s (
successors_instr i) ->
Regset.In v (
rvs s) -> ~
Regset.In v (
def f n) ->
Regset.In v (
rvs n);
checked_in_slice_use_in_rvs :
forall n v,
In n slice_nodes ->
Regset.In v (
use f n) ->
Regset.In v (
rvs n);
checked_in_slice_mem_def :
forall n i s,
(
fn_code f) !
n =
Some i ->
In s (
successors_instr i) ->
Regset.In memvar (
rvs s) ->
Regset.In memvar (
def f n) ->
Regset.In memvar (
rvs n) ->
In n slice_nodes;
checked_not_in_slice_succ_rvs :
forall n i s,
~
In n slice_nodes -> (
fn_code f) !
n =
Some i ->
In s (
successors_instr i) ->
forall x,
Regset.In x (
rvs s) ->
Regset.In x (
rvs n);
checked_not_in_slice_def_not_in_rvs :
forall n,
f_In n f -> ~
In n slice_nodes ->
forall x,
Regset.In x (
def f n) -> ~
Regset.In x (
rvs n)
}.
Proof that the validator enforces the required properties.
Lemma checked_rvs_wf:
forall f slice_nodes rvs,
(
forall n,
In n slice_nodes ->
f_In n f) ->
rvs_checker f slice_nodes rvs =
true ->
checked_rvs f slice_nodes rvs.
Proof.
introsv SLICE_WF CHECK.
unfold rvs_checker in CHECK.
constructor;
intros.
Case "
checked_not_in_def_in_rvs".
eapply forall_ptree_true with (
i :=
n)
in CHECK;
eauto.
rewrite andb_true_iff in CHECK.
destruct CHECK as [
NOT_IN_DEF_IN_RVS _].
unfolds in NOT_IN_DEF_IN_RVS.
rewrite forallb_forall in NOT_IN_DEF_IN_RVS.
apply NOT_IN_DEF_IN_RVS in H0.
apply Regset.for_all_2 in H0.
unfold Regset.For_all in H0.
apply H0 in H1.
rewrite orb_true_iff in H1.
destruct H1.
apply Regset.mem_2 in H1;
contra.
apply Regset.mem_2 in H1;
asmp.
do 3
unfolds;
intros;
subst;
auto.
Case "
checked_in_slice_use_in_rvs".
gen (
SLICE_WF _ H)
as N_IN.
case_eq ((
fn_code f) !
n);
intros;
trim.
eapply forall_ptree_true with (
i :=
n)
in CHECK;
eauto.
rewrite <-
mem_iff_In in H.
rewrite H in CHECK.
rewrite andb_true_iff in CHECK.
destruct CHECK as [
NOT_IN_DEF_IN_RVS USES_IN_RVS].
unfolds in USES_IN_RVS.
apply Regset.subset_2 in USES_IN_RVS.
unfolds in USES_IN_RVS.
apply USES_IN_RVS;
auto.
Case "
checked_in_slice_mem_def".
eapply forall_ptree_true with (
i :=
n)
in CHECK;
eauto.
optDecN CHECK INSL.
apply mem_iff_In in INSL;
auto.
boolrw.
destruct CHECK as [
NODEF [[
NOMEM NORVS]
NOTIN]].
unfolds in NOMEM.
rewrite forallb_forall in NOMEM.
apply NOMEM in H0.
optDecN H0 EQS;
trim.
boolrw.
apply Regset.mem_1 in H1.
apply Regset.mem_1 in H2.
apply Regset.mem_1 in H3.
destruct EQS;
trim.
destruct H4;
trim.
Case "
checked_not_in_slice_succ_rvs".
eapply forall_ptree_true with (
i :=
n)
in CHECK;
eauto.
rewrite <-
mem_iff_In_conv in H.
rewrite H in CHECK.
boolrw.
decs CHECK.
unfolds in H7.
rewrite forallb_forall in H7.
apply H7 in H1.
apply Regset.for_all_2 in H1.
unfold Regset.For_all in H1.
apply Regset.mem_2.
apply H1;
auto.
do 3
unfolds;
intros;
subst;
auto.
apply positive.
Case "
checked_not_in_slice_def_not_in_rvs".
apply f_In_ex in H.
decs H;
eauto.
eapply forall_ptree_true with (
i :=
n)
in CHECK;
eauto.
rewrite <-
mem_iff_In_conv in H0.
rewrite H0 in CHECK.
boolrw.
decs CHECK.
unfolds in H3.
apply Regset.for_all_2 in H5.
unfold Regset.For_all in H5.
intro.
apply Regset.mem_1 in H4.
apply H5 in H1.
rewrite negb_true_iff in H1.
trim.
do 3
unfolds;
intros;
subst;
auto.
apply positive.
Qed.