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.
Section SLICE_ALGORITHM.
Definition icond_true (
reg_vint :
reg) (
ifso ifnot :
node):
instruction :=
Icond (
Cmaskzero Integers.Int.zero) (
reg_vint ::
nil)
ifso ifnot.
Definition icond_false (
reg_vint :
reg) (
ifso ifnot :
node):
instruction :=
Icond (
Cmasknotzero Integers.Int.zero) (
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
end
|
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
end
end.
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
end.
Definition compute_bs_code (
reg_vint :
reg) (
f :
function) (
bs_nodes :
list node) (
s_dobs :
dobsT) (
dexit :
PTree.t N) :
PTree.t instruction :=
PTree.map (
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
end
end
)
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).
End SLICE_ALGORITHM.
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 :
Scope.family 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)
else
Error ((
MSG "
scope_exits_checker failed") ::
nil)
else
Error ((
MSG "
rvs_checker failed") ::
nil)
else
Error ((
MSG "
s_dobs_checker failed") ::
nil).
Definition slice_function (
f:
function) (
nc :
t_criterion) (
fsc :
Scope.family 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 :
Scope.family f) :
res function :=
do (
sliced_f,
_) <-
slice_function f nc fsc exit_n reg_vint;
OK sliced_f.
Definition local_sliced_bound (
f :
function) (
fsc:
Scope.family f) (
nc :
t_criterion) :
res Z :=
if positive_eq_dec nc f.(
fn_entrypoint)
then OK 1%
Z
else
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).