Definitions and Operations on Symbolic Values and Invariants
TODO: a few words on symbolic values ?
We add a "Gluing Invariant" (GI) to each entry block,
relating the source variables (variables of the source function)
to the target variables (variables of the target function).
A GI (empty by default) is a map associating to some target variable a symbolic value on the source variables.
The symbolic simulation verifies the preservation of GIs by the following comparison:
S;J => I;T
where
- S : symbolic execution of the source
- I : input invariant
- J : ouput invariant
- T : symbolic execution of the target
- => : is a relation on the target variables.
Liveness is checked from GIs preservation.
Example of valid liveness checking: {x} y := x+1 {y}
input GI: {x := x} output GI: { y := y }
SJ res: { y := x+1 }
IT res: { y := x+1 }
Example of invalid liveness checking: {} y := x+1 {y}
input GI: { } output GI: { y := y }
SJ res: { y := x+1 }
IT res: { y := dead+1 } REJECTED
Example of invalid liveness checking: {} y := x+1 {}
input GI: { } output GI: { }
SJ res: { }
IT res: { y := dead+1 } REJECTED
Example of valid renaming:
{ y := x }
y := x + 1 versus z := y + 1
{ z := y }
SJ res: { z := x+1 }
IT res: { z := x+1 }
Example of valid renaming (but with wrong liveness info):
{ }
y := x + 1 versus z := y + 1
{ z := y }
SJ res: { z := x + 1}
IT res: { z := dead+1 } REJECTED
Example of invalid renaming (but with good liveness info):
{ y := x }
y := x + 1 versus z := y
{ z := y }
SJ res: { z := x + 1}
IT res: { z := x }
Example of valid transformation:
{ x := x }
y := load x; versus z := loadx
{ z := y }
SJ res: { ok(loadx); z := x }
IT res: { ok(loadx); z := x }
Example of invalid transformation (with bad liveness info):
{ x := x }
y := load z1; versus y := load z2;
y := x ; versus y := x
{ y := y }
SJ res: { ok(loadz1); y := x }
IT res: { ok(loaddead); y := x } REJECTED
Example of valid transformation (dead code elimination):
{ x := x }
y := load z1; versus
y := x ; versus y := x
{ y := y }
SJ res: { ok(loadz1); y := x }
IT res: { y := x }
Example of weird but valid transformation:
{ x }
y := x versus y := x+1
{ y := x+1 }
SJ res: { y := x+1 }
IT res: { y := x+1 }
Rem: this transformation simply considers
that the "y" on the source code is dead
and use "y" as a precomputation on the target code.
REM: liveness check cannot use rewriting rules ??? (TODO: a verifier avec Léo).
{ }
y := x-x versus y := mayundef x 0
{ y := y }
with a rewriting rule: x-x -> mayundef x 0
SJ res: { y := mayundef x 0 }
IT res: { y := mayundef dead 0 } REJECTED
Require Import Coqlib Maps Floats.
Require Import Classes.RelationClasses.
Require Import AST.
Require Import Op Registers.
Require Import OptionMonad.
Require Export Impure.ImpHCons.
Require Import ValueDomain.
Import HConsing.
Syntax of symbolic values
Additional informations attached to the stores.
Used by the semantics (if strict) and the rewriting rules.
Record store_info :
Type :=
mk_store_info {
store_num:
positive;
store_aaddr:
aval;
}.
Definition dummy_store_info :
store_info :=
mk_store_info 1%
positive Vtop.
Definition store_info_set_num (
i :
store_info) (
n :
positive) :
store_info :=
mk_store_info n (
store_aaddr i).
Definition store_info_set_aaddr (
i :
store_info) (
av :
aval) :
store_info :=
mk_store_info (
store_num i)
av.
Definition store_info_eq_dec (
ai0 ai1 :
store_info): {
ai0 =
ai1}+{
ai0<>
ai1}.
Proof.
symbolic value
Inductive sval :=
|
Sinput (
r:
reg) (
hid:
hashcode)
|
Sop (
op:
operation) (
lsv:
list_sval) (
hid:
hashcode)
|
Sfoldr (
op:
operation) (
lsv:
list_sval) (
sv0:
sval) (
hid:
hashcode)
|
Sload (
sm:
smem) (
trap:
trapping_mode) (
chunk:
memory_chunk)
(
addr:
addressing) (
lsv:
list_sval) (
aaddr:
aval) (
hid:
hashcode)
list of symbolic values
with list_sval :=
|
Snil (
hid:
hashcode)
|
Scons (
sv:
sval) (
lsv:
list_sval) (
hid:
hashcode)
symbolic memory
with smem :=
|
Sinit (
hid:
hashcode)
|
Sstore (
sm:
smem) (
chunk:
memory_chunk)
(
addr:
addressing) (
lsv:
list_sval) (
sinfo:
store_info) (
srce:
sval) (
hid:
hashcode)
.
Definition fst_lsv lsv :=
match lsv with
|
Snil _ =>
None
|
Scons sv _ _ =>
Some sv
end.
"fake" smart-constructors using an unknown_hid instead of the one provided by hash-consing.
These smart-constructors are those used in the abstract model of symbolic execution.
They will also appear in the implementation of rewriting rules
(in order to avoid hash-consing handling in proofs of rewriting rules)
and in the invariants provided by oracles.
Definition fSinput (
r:
reg) :=
Sinput r unknown_hid.
Definition fSop (
op:
operation) (
lsv:
list_sval) :=
Sop op lsv unknown_hid.
Definition fSfoldr (
op:
operation) (
lsv:
list_sval) (
sv0:
sval) :=
Sfoldr op lsv sv0 unknown_hid.
Definition fSload (
sm:
smem) (
trap:
trapping_mode)
(
chunk:
memory_chunk) (
addr:
addressing) (
lsv:
list_sval) (
aaddr:
aval)
:=
Sload sm trap chunk addr lsv aaddr unknown_hid.
Definition fSnil :=
Snil unknown_hid.
Definition fScons (
sv:
sval) (
lsv:
list_sval) :=
Scons sv lsv unknown_hid.
Definition fSinit :=
Sinit unknown_hid.
Definition fSstore (
sm:
smem) (
chunk:
memory_chunk) (
addr:
addressing) (
lsv:
list_sval) (
sinfo:
store_info) (
srce:
sval)
:=
Sstore sm chunk addr lsv sinfo srce unknown_hid.
Scheme sval_mut :=
Induction for sval Sort Prop
with list_sval_mut :=
Induction for list_sval Sort Prop
with smem_mut :=
Induction for smem Sort Prop.
Lemma sveq_dec:
forall (
sv1 sv2:
sval), {
sv1=
sv2} + {
sv1<>
sv2}
with lsveq_dec:
forall (
lsv1 lsv2:
list_sval), {
lsv1=
lsv2} + {
lsv1<>
lsv2}
with smeq_dec:
forall (
sm1 sm2:
list_sval), {
sm1=
sm2} + {
sm1<>
sm2}.
Proof.
Representations and syntax of symbolic invariants
registers in invariant
Record ireg := {
force_input:
bool;
regof:>
reg }.
input r is the input value of r in the block;
last r is the last value of the variable in the invariant
Definition input (
r:
reg) := {|
force_input :=
true;
regof :=
r |}.
Definition last (
r:
reg) := {|
force_input :=
false;
regof :=
r |}.
Definition ir_subst (
subst:
reg ->
sval) (
ir:
ireg):
sval :=
if ir.(
force_input)
then fSinput ir else subst ir.
operations in invariant
Inductive root_op:
Type :=
|
Rop (
op:
operation)
|
Rload (
trap:
trapping_mode) (
chunk:
memory_chunk) (
addr:
addressing) (
aaddr:
aval)
.
Definition root_apply (
o :
root_op) (
args :
list_sval) (
sm :
smem):
sval :=
match o with
|
Rop op =>
fSop op args
|
Rload trap chunk addr aaddr =>
fSload sm trap chunk addr args aaddr
end.
values in invariant
Inductive ival:
Type :=
|
Ireg (
ir:
ireg)
|
Iop (
rop:
root_op) (
args:
list ireg)
.
Fixpoint lsvof subst (
l:
list ireg):
list_sval :=
match l with
|
nil =>
fSnil
|
ir::
l =>
fScons (
ir_subst subst ir) (
lsvof subst l)
end.
Definition ir_input_of :
list reg ->
list ireg :=
map input.
Definition ir_last_of :
list reg ->
list ireg :=
map last.
Definition ir_reg_of :
list ireg ->
list reg :=
map regof.
Definition rop_subst subst (
rop:
root_op) (
lr:
list ireg):
sval :=
let lsv :=
lsvof subst lr in
root_apply rop (
lsvof subst lr)
fSinit.
Definition iv_subst subst (
iv:
ival):
sval :=
match iv with
|
Ireg ir =>
ir_subst subst ir
|
Iop rop args =>
rop_subst subst rop args
end.
Definition svof iv :=
iv_subst fSinput iv.
Coercion svof:
ival >->
sval.
This is an "abstract" representation of symbolic invariants as finite "parallel assignments"
of invariant values (into registers).
In other words, such an invariants relates (a finite set) of "output" variables in function
of "input" variables and an "input" memory.
Such invariant also express an implicit precondition on the "inputs" that the symbolic values
do not trap.
Inductive is_input:
sval ->
Prop :=
|
is_input_intro r hid:
is_input (
Sinput r hid).
Local Hint Resolve is_input_intro:
core.
Lemma is_input_dec sv: {
is_input sv } + { ~
is_input sv }.
Proof.
destruct sv; eauto; right; intro H; inv H.
Qed.
FPASV stands for "Finite Parallel Assignment of Symbolic Values"
Record fpasv :=
{
fpa_ok:
list sval;
fpa_reg:>
PTree.tree sval;
fpa_wf:
forall r sv,
fpa_reg!
r =
Some sv -> ~(
is_input sv) ->
List.In sv fpa_ok }.
Definition fpa_eq (
si1 si2:
fpasv):
Prop :=
(
forall x,
List.In x (
fpa_ok si1) <->
List.In x (
fpa_ok si2)) /\ (
fpa_reg si1) = (
fpa_reg si2).
Lemma fpa_eq_refl:
forall si,
fpa_eq si si.
Proof.
intros; repeat constructor; auto.
Qed.
Global Instance fpasv_Equivalence :
Equivalence fpa_eq.
Proof.
constructor.
- intros ?; constructor; reflexivity.
- intros ? ? []; constructor; symmetry; auto.
- intros ? ? ? [] []; constructor; etransitivity; eauto.
Qed.
Definition si_apply (
si:
fpasv)
r:
option sval := (
fpa_reg si)!
r.
Coercion si_apply:
fpasv >->
Funclass.
Lemma si_wf (
si:
fpasv):
forall r sv,
si r =
Some sv -> ~(
is_input sv) ->
List.In sv (
fpa_ok si).
Proof.
intros;
eapply fpa_wf;
eauto.
Qed.
Program Definition si_empty:
fpasv :=
{|
fpa_ok :=
nil;
fpa_reg := @
PTree.empty _
|}.
Lemma si_gempty r:
si_empty r =
None.
Proof.
Local Hint Resolve si_wf is_input_intro:
core.
Program Definition si_set (
r:
reg) (
sv:
sval) (
si:
fpasv):
fpasv :=
{|
fpa_ok :=
sv::(
fpa_ok si);
fpa_reg :=
PTree.set r sv (
fpa_reg si) |}.
Next Obligation.
Lemma si_gss r sv si:
si_set r sv si r =
Some sv.
Proof.
Lemma si_gso r1 r2 sv si:
r1 <>
r2 ->
si_set r2 sv si r1 =
si r1.
Proof.
Local Open Scope option_monad_scope.
A more "compact" (and "dynamic") representation of symbolic invariants as:
-
a sequence aseq of assignments of symbolic values
-
"exporting" a finite set of outputs.
This is the (abstract) syntax of invariants for oracles !
In the set of output registers, we distinguish those not defined in
aseq
(which thus satisfy
r=fSinput r).
Important remark: lazily, the simulation checker will consider that the set of register
r
such that
r = fSinput r is those not defined in
aseq !
This means that an oracle should not put in
aseq an assignment like
r := input r.
This may lead the simulation checker to reject the invariant while checking "only liveness"
constraints.
In the same spirit, at the return address of a "call/builtin" putting its result in
r,
the
aseq should not contain any reference to
r, even as an auxiliary variable when
r is
dead afterwards (i.e. not in
outputs). This would complicate a bit
test_seq_rclobberable to
support this feature (and this does not seem very useful).
Perhaps a good strategy for the oracle, is to use "fresh" names in the context for auxiliary
variables (it would be easier for debugging).
CSASV stands for "Compact Sequence Assignments of Symbolic Values"
Record csasv := {
aseq:
list (
reg *
ival);
outputs:
Regset.t;
}.
Definition ext (
si:
reg ->
option sval) (
r:
reg):
sval :=
match si r with
|
Some iv =>
iv
|
None =>
fSinput r
end.
Fixpoint exec_seq (
l:
list (
reg*
ival)) (
si:
fpasv):
fpasv :=
match l with
|
nil =>
si
| (
r,
iv)::
l =>
exec_seq l (
si_set r (
iv_subst (
ext si)
iv)
si)
end.
Fixpoint build_alive (
subst:
reg ->
sval) (
l:
list reg) :=
match l with
|
nil => @
PTree.empty _
|
r::
l =>
PTree.set r (
subst r) (
build_alive subst l)
end.
Lemma build_alive_In subst r l:
List.In r l -> (
build_alive subst l)!
r =
Some (
subst r).
Proof.
induction l as [|
r1 l];
simpl;
try tauto.
intros H.
destruct (
Pos.eq_dec r1 r).
-
subst;
rewrite PTree.gss;
auto.
-
rewrite PTree.gso;
auto.
intuition.
Qed.
Lemma build_alive_alive subst r l:
forall sv, (
build_alive subst l)!
r =
Some sv ->
List.In r l.
Proof.
Lemma build_alive_spec subst l r:
(
build_alive subst l) !
r = (
ASSERT (
in_dec Reg.eq r l)
IN Some (
subst r)).
Proof.
Semantics of csasv as "abstract" symbolic invariants
Program Definition siof (
csi:
csasv):
fpasv :=
let si :=
exec_seq csi.(
aseq)
si_empty in
{|
fpa_ok :=
fpa_ok si;
fpa_reg :=
build_alive (
ext si) (
Regset.elements csi.(
outputs))
|}.
Next Obligation.
intros;
exploit build_alive_alive;
eauto.
intro X;
rewrite build_alive_In in H;
eauto.
try_simplify_someHyps.
unfold ext in *.
autodestruct;
simpl;
eauto.
destruct H0.
econstructor.
Qed.
Coercion siof:
csasv >->
fpasv.
Some basic properties about sequential invariants
Lemma build_alive_nofail l subst1 subst2 r s:
(
build_alive subst1 l)!
r =
None ->
(
build_alive subst2 l)!
r =
Some s ->
False.
Proof.
Lemma build_alive_notIn_None l s1 s2 r:
(
build_alive s1 l)!
r =
None ->
(
build_alive s2 l)!
r =
None.
Proof.
Lemma build_alive_only_live l r sv:
(
build_alive (
ext si_empty)
l)!
r =
Some sv ->
sv =
fSinput r.
Proof.
Lemma build_alive_only_live_notin l r:
~
In r l ->
(
build_alive (
ext si_empty)
l)!
r =
None.
Proof.
Lemma csi_In (
csi:
csasv)
r:
Regset.In r csi.(
outputs) ->
csi r =
Some (
ext (
exec_seq csi.(
aseq)
si_empty)
r).
Proof.
Lemma csi_alive (
csi:
csasv)
r sv:
csi r =
Some sv ->
Regset.In r csi.(
outputs).
Proof.
Lemma csi_alive_get (
csi:
csasv)
r sv:
csi r =
Some sv ->
sv =
ext (
exec_seq csi.(
aseq)
si_empty)
r.
Proof.
intros;
exploit csi_alive;
eauto.
intros;
exploit csi_In;
eauto.
congruence.
Qed.
Lemma csi_notIn (
csi:
csasv)
r:
~(
Regset.In r csi.(
outputs)) ->
csi r =
None.
Proof.
intros.
destruct (
csi r)
eqn:
X;
auto.
destruct H.
exploit csi_alive;
eauto.
Qed.
Definition csi_empty:
csasv := {|
aseq:=
nil;
outputs :=
Regset.empty |}.
Lemma fpa_eq_csi_si_empty:
fpa_eq csi_empty si_empty.
Proof.
unfold fpa_eq;
simpl.
intuition.
Qed.
Lemma csi_gempty r:
csi_empty r =
None.
Proof.
Definition csi_remove r (
csi:
csasv) :
csasv :=
{|
aseq:=
csi.(
aseq);
outputs :=
Regset.remove r csi.(
outputs) |}.
Lemma csi_grs csi r:
csi_remove r csi r =
None.
Proof.
Lemma csi_gro csi r1 r2:
r1 <>
r2 ->
csi_remove r1 csi r2 =
csi r2.
Proof.
Record invariants := {
history:
csasv;
glue:>
csasv
}.
Definition csix_empty :
invariants := {|
history :=
csi_empty;
glue :=
csi_empty |}.
Definition gluemap :=
PTree.t invariants.
Definition gm_empty:
gluemap := (@
PTree.empty _).
Definition gm_apply (
gm:
gluemap) (
pc:
positive) :=
match gm!
pc with
|
Some csix =>
csix
|
_ =>
csix_empty
end.
Coercion gm_apply:
gluemap >->
Funclass.
Definition csix_remove r (
csix:
invariants) :
invariants :=
{|
history :=
csi_remove r (
history csix);
glue :=
csi_remove r (
glue csix)
|}.
A few syntactic properties on invariants that we need to check during the symbolic test
NOTE: some notions below are defined on abstract invariants (this may help for future generalizations ?)
Definition only_liveness (
si:
fpasv):
Prop :=
(
fpa_ok si) =
nil
/\ (
forall r sv,
si r =
Some sv ->
sv=
fSinput r).
Inductive only_live_input (
r:
reg):
sval ->
Prop :=
|
only_live_input_intro hid:
only_live_input r (
Sinput r hid).
Lemma only_live_input_dec r sv: {
only_live_input r sv } + { ~(
only_live_input r sv) }.
Proof.
destruct sv;
try (
right;
intro H;
inv H;
fail).
destruct (
Pos.eq_dec r r0);
try (
right;
intro H;
inv H;
congruence).
subst.
left;
constructor.
Qed.
Fixpoint svfree (
sv:
sval) (
r:
reg):
Prop :=
match sv with
|
Sinput r'
_ =>
r <>
r'
|
Sop _ l _ =>
lsvfree l r
|
Sfoldr _ lsv sv0 _ =>
lsvfree lsv r /\
svfree sv0 r
|
Sload sm _ _ _ lsv _ _ =>
smfree sm r /\
lsvfree lsv r
end
with lsvfree (
lsv:
list_sval) (
r:
reg):
Prop :=
match lsv with
|
Snil _ =>
True
|
Scons sv lsv'
_ =>
svfree sv r /\
lsvfree lsv'
r
end
with smfree (
sm:
smem) (
r:
reg):
Prop :=
match sm with
|
Sinit _ =>
True
|
Sstore sm _ _ lsv _ srce _ =>
smfree sm r /\
lsvfree lsv r /\
svfree srce r
end.
Fixpoint svfreem (
sv:
sval):
Prop :=
match sv with
|
Sop op l _ =>
op_depends_on_memory op =
false
/\
lsvfreem l
|
Sfoldr op l sv0 _ =>
op_depends_on_memory op =
false
/\
lsvfreem l
/\
svfreem sv0
|
Sload _ _ _ _ _ _ _ =>
False
|
_ =>
True
end
with lsvfreem (
lsv:
list_sval):
Prop :=
match lsv with
|
Snil _ =>
True
|
Scons sv lsv'
_ =>
svfreem sv /\
lsvfreem lsv'
end.
Definition sifree (
si:
fpasv) (
res:
reg):
Prop :=
(
forall sv,
List.In sv (
fpa_ok si) ->
svfree sv res)
/\ (
forall r sv,
si r =
Some sv -> ~(
only_live_input r sv) ->
svfree sv res).
Definition sifreem (
si:
fpasv):
Prop :=
forall sv,
List.In sv (
fpa_ok si) ->
svfreem sv.
Record clobbered_compat (
csi:
csasv) (
res:
reg):
Prop := {
res_is_free:
sifree csi res;
mem_is_free:
sifreem csi;
res_only_live:
forall sv,
csi res =
Some sv ->
sv =
fSinput res
}.
Local Open Scope lazy_bool_scope.
Lemma andb_rew (
a b:
bool): (
a &&&
b) =
true <-> (
a=
true /\
b=
true).
Proof.
destruct a; simpl; intuition congruence.
Qed.
Lemma negb_rew a:
negb a =
true <->
a =
false.
Proof.
destruct a; simpl; intuition congruence.
Qed.
Hint Rewrite andb_rew negb_rew Pos.eqb_neq Pos.eqb_eq:
bools.
Ltac simplify_ir_subst :=
simpl;
unfold ir_subst,
rop_subst,
root_apply in *;
repeat autodestruct;
simpl in *;
intros;
autorewrite with bools in *;
intuition (
congruence ||
eauto).
Lemma iv_subst_preserv_lsvfreem (
lr:
list ireg):
forall (
subst:
reg ->
sval),
(
forall r,
svfreem (
subst r)) ->
lsvfreem (
lsvof subst lr).
Proof.
induction lr; simplify_ir_subst.
Qed.
Local Hint Resolve iv_subst_preserv_lsvfreem:
core.
Lemma iv_subst_preserv_freem (
iv:
ival):
forall (
subst:
reg ->
sval),
svfreem iv ->
(
forall r,
svfreem (
subst r)) ->
svfreem (
iv_subst subst iv).
Proof.
destruct iv; simplify_ir_subst.
Qed.
Lemma ext_preserv_freem si r:
sifreem si ->
svfreem (
ext si r).
Proof.
unfold ext,
sifreem.
destruct (
si r)
as [
sv|]
eqn:
X;
simpl;
eauto.
intro H;
destruct (
is_input_dec sv)
as [
H0|
H0];
eauto.
inv H0;
simpl;
auto.
Qed.
Lemma sifreem_si_empty:
sifreem si_empty.
Proof.
intros sv. simpl. intuition.
Qed.
Functional checkers corresponding to the above properties.
Definition test_ivfreem (
iv:
ival):
bool :=
match iv with
|
Iop (
Rop op)
_ =>
negb (
op_depends_on_memory op)
|
Iop (
Rload _ _ _ _)
_ =>
false
|
_ =>
true
end.
Lemma lsvfreem_fSinput lr:
lsvfreem (
lsvof fSinput lr).
Proof.
induction lr; simplify_ir_subst.
Qed.
Local Hint Resolve lsvfreem_fSinput:
core.
Lemma test_ivfreem_correct iv:
test_ivfreem iv =
true ->
svfreem iv.
Proof.
destruct iv; simplify_ir_subst.
Qed.
Fixpoint test_seqfreem (
l:
list (
reg*
ival)):
bool :=
match l with
|
nil =>
true
| (
_,
iv)::
l =>
test_ivfreem iv &&&
test_seqfreem l
end.
Local Hint Resolve sifreem_si_empty iv_subst_preserv_freem ext_preserv_freem:
core.
Lemma test_seqfreem_correct (
l:
list (
reg*
ival)):
forall (
si:
fpasv),
sifreem si -> (
test_seqfreem l =
true ->
sifreem (
exec_seq l si)).
Proof.
induction l as [|(
r,
sv)
l];
simpl;
auto.
intros si FREEsi;
autorewrite with bools.
intros (
TESTSV &
TESTL).
apply test_ivfreem_correct in TESTSV.
intros r1 sv1.
eapply IHl in TESTL;
eauto.
clear r1 sv1.
intros sv1;
simpl.
intros [
H|
H];
subst;
eauto.
Qed.
NB: test_csifreem is linear in the size of csi
Definition test_csifreem (
csi:
csasv):
bool :=
test_seqfreem csi.(
aseq).
Theorem test_csifreem_correct csi:
test_csifreem csi =
true ->
sifreem csi.
Proof.
Fixpoint test_lirfree (
lir:
list ireg)
r:
bool :=
match lir with
|
nil =>
true
|
iv::
lir =>
negb (
Pos.eqb r (
regof iv))
&&&
test_lirfree lir r
end.
Lemma test_lirfree_correct lir r:
forall subst,
(
forall r',
r <>
r' ->
svfree (
subst r')
r) ->
test_lirfree lir r =
true ->
lsvfree (
lsvof subst lir)
r.
Proof.
induction lir; simplify_ir_subst.
Qed.
Local Hint Resolve test_lirfree_correct:
core.
Definition test_ivfree iv (
r:
reg):
bool :=
match iv with
|
Ireg ir =>
negb (
Pos.eqb r (
regof ir))
|
Iop _ lir =>
test_lirfree lir r
end.
Lemma test_ivfree_correct iv r:
forall subst,
(
forall r',
r <>
r' ->
svfree (
subst r')
r) ->
test_ivfree iv r =
true ->
svfree (
iv_subst subst iv)
r.
Proof.
destruct iv; simplify_ir_subst.
Qed.
Fixpoint test_seq_rclobberable (
l:
list (
reg*
ival))
r:
bool :=
match l with
|
nil =>
true
| (
r',
iv)::
l =>
negb (
Pos.eqb r r')
&&&
test_ivfree iv r
&&&
test_seq_rclobberable l r
end.
Lemma ext_preserv_free si r r':
r <>
r' ->
sifree si r ->
svfree (
ext si r')
r.
Proof.
unfold ext,
sifree.
intros DIFF H.
autodestruct.
intros EQ.
destruct (
only_live_input_dec r'
s)
as [
X|
X].
{
inv X.
simpl.
congruence. }
eapply H;
eauto.
Qed.
Local Hint Resolve test_ivfree_correct ext_preserv_free :
core.
Lemma test_seq_rclobberable_correct (
l:
list (
reg*
ival))
r:
forall (
si:
fpasv),
sifree si r ->
si r =
None ->
test_seq_rclobberable l r =
true ->
sifree (
exec_seq l si)
r /\
exec_seq l si r =
None.
Proof.
induction l as [|(
r',
sv)
l];
simpl;
auto.
intros si SVFREE EQNONE1;
autorewrite with bools.
intros ((
DIFF &
TESTsv) &
TESTl).
eapply IHl;
eauto.
-
generalize SVFREE.
intros [
SVF1 SVF2].
split;
simpl.
*
intros sv0 [
H|
H];
subst;
eauto.
*
intros r0 sv0;
destruct (
Pos.eq_dec r'
r0).
+
subst.
erewrite si_gss;
eauto.
intros;
try_simplify_someHyps.
+
rewrite si_gso;
eauto.
-
simpl.
rewrite si_gso;
eauto.
Qed.
NB: test_rclobberable is linear in the size of csi
Lemma sifree_si_empty r:
sifree si_empty r.
Proof.
split;
simpl;
intuition.
erewrite si_gempty in *.
congruence.
Qed.
Local Hint Resolve sifree_si_empty:
core.
Definition test_rclobberable (
csi:
csasv)
r:
bool :=
test_seq_rclobberable csi.(
aseq)
r.
Theorem test_rclobberable_only_liveness csi r sv:
test_rclobberable csi r =
true ->
csi r =
Some sv ->
sv =
fSinput r.
Proof.
Theorem test_rclobberable_sifree csi r:
test_rclobberable csi r =
true ->
sifree csi r.
Proof.
Definition test_only_liveness (
csi:
csasv):
bool :=
match csi.(
aseq)
with
|
nil =>
true
|
_ =>
false
end.
Theorem test_only_liveness_correct csi:
test_only_liveness csi =
true ->
only_liveness csi.
Proof.
unfold test_only_liveness.
case csi as [[|] ?];
simpl. 2:
congruence.
intros _.
split;
simpl.
-
reflexivity.
-
intros r sv X;
exploit csi_alive_get.
eapply X.
unfold ext.
simpl.
auto.
Qed.
Definition test_clobberable (
csi:
csasv) (
res:
reg):
bool
:=
test_rclobberable csi res &&&
test_csifreem csi.
Local Hint Resolve test_rclobberable_only_liveness test_rclobberable_sifree test_csifreem_correct:
core.
Theorem test_clobberable_correct res csi:
test_clobberable csi res =
true ->
clobbered_compat csi res.
Proof.
unfold test_clobberable;
autorewrite with bools.
intuition;
constructor;
eauto.
Qed.