Skip to content
GitLab
Projects
Groups
Snippets
Help
Loading...
Help
What's new
10
Help
Support
Community forum
Keyboard shortcuts
?
Submit feedback
Contribute to GitLab
Sign in / Register
Toggle navigation
Open sidebar
AVA
FloVer
Commits
89142369
Commit
89142369
authored
Feb 20, 2019
by
Joachim Bard
Browse files
Options
Browse Files
Download
Email Patches
Plain Diff
removing conditionals in some more files
parent
2369fb36
Changes
4
Hide whitespace changes
Inline
Side-by-side
Showing
4 changed files
with
34 additions
and
6 deletions
+34
-6
coq/ErrorAnalysis.v
coq/ErrorAnalysis.v
+2
-0
coq/RealRangeArith.v
coq/RealRangeArith.v
+7
-1
coq/TypeValidator.v
coq/TypeValidator.v
+11
-2
coq/ssaPrgs.v
coq/ssaPrgs.v
+14
-3
No files found.
coq/ErrorAnalysis.v
View file @
89142369
...
...
@@ -21,10 +21,12 @@ Fixpoint validErrorBounds (e:expr Q) E1 E2 A Gamma DeltaMap :Prop :=
eval_expr
E1
(
toRTMap
(
toRExpMap
Gamma
))
DeltaMapR
(
toREval
(
toRExp
e1
))
v__R
REAL
->
eval_expr
E2
(
toRExpMap
Gamma
)
DeltaMap
(
toRExp
e1
)
v__FP
m
->
validErrorBounds
e2
(
updEnv
x
v__R
E1
)
(
updEnv
x
v__FP
E2
)
A
Gamma
DeltaMap
)
(
*
|
Cond
e1
e2
e3
=>
validErrorBounds
e1
E1
E2
A
Gamma
DeltaMap
/
\
validErrorBounds
e2
E1
E2
A
Gamma
DeltaMap
/
\
validErrorBounds
e3
E1
E2
A
Gamma
DeltaMap
*
)
|
_
=>
True
end
)
/
\
forall
v__R
(
iv
:
intv
)
(
err
:
error
),
...
...
coq/RealRangeArith.v
View file @
89142369
...
...
@@ -84,9 +84,11 @@ Fixpoint validRanges e (A:analysisResult) E Gamma :Prop :=
validRanges
e1
A
E
Gamma
/
\
(
forall
vR
,
eval_expr
E
Gamma
DeltaMapR
(
toREval
(
toRExp
e1
))
vR
REAL
->
validRanges
e2
A
(
updEnv
x
vR
E
)
Gamma
)
(
*
|
Cond
e1
e2
e3
=>
validRanges
e1
A
E
Gamma
/
\
validRanges
e2
A
E
Gamma
/
\
validRanges
e3
A
E
Gamma
*
)
end
/
\
exists
iv
err
vR
,
FloverMap
.
find
e
A
=
Some
(
iv
,
err
)
/
\
...
...
@@ -123,7 +125,7 @@ Proof.
-
destruct
valid1
as
[[
H1
H2
]
_
];
auto
.
split
;
auto
.
intros
.
eauto
using
swap_Gamma_eval_expr
.
-
destruct
valid1
as
[[
?
[
?
?
]]
?
];
auto
.
(
*
-
destruct
valid1
as
[[
?
[
?
?
]]
?
];
auto
.
*
)
Qed
.
(
*
...
...
@@ -361,6 +363,7 @@ Proof.
rewrite
N
.
eqb_compare
in
e3
.
rewrite
Heq
,
e7
in
e3
.
discriminate
.
(
*
-
intros
valid1
;
destruct
valid1
as
[[
validsub1
[
validsub1
'
validsub1
''
]]
validr1
].
specialize
(
IHc
e3
E
validsub1
).
specialize
(
IHc0
e4
E
validsub1
'
).
...
...
@@ -378,6 +381,7 @@ Proof.
rewrite
Q_orderedExps
.
exprCompare_eq_sym
.
simpl
.
rewrite
Heq
,
e3
,
e4
;
auto
.
*
)
Qed
.
Lemma
validRanges_ssa_extension
(
e
:
expr
Q
)
A
E
Gamma
...
...
@@ -473,6 +477,7 @@ Proof.
eapply
eval_expr_ssa_extension
;
eauto
.
cbn
.
rewrite
!
freeVars_toREval_toRExp_compat
;
auto
.
(
*
-
simpl
in
Hsub
.
assert
(
NatSet
.
Subset
(
freeVars
e1
)
fVars
)
as
Hsub1
by
set_tac
.
assert
(
NatSet
.
Subset
(
freeVars
e2
)
fVars
)
as
Hsub2
by
(
clear
Hsub1
;
set_tac
).
...
...
@@ -491,4 +496,5 @@ Proof.
eapply
eval_expr_ssa_extension
;
try
eassumption
.
*
)
simpl
.
rewrite
!
freeVars_toREval_toRExp_compat
;
auto
.
*
)
Admitted
.
coq/TypeValidator.v
View file @
89142369
...
...
@@ -55,6 +55,7 @@ Fixpoint validTypes e (Gamma:FloverMap.t mType): Prop :=
exists
me
,
FloverMap
.
find
e1
Gamma
=
Some
m
/
\
FloverMap
.
find
(
Var
Q
x
)
Gamma
=
Some
m
/
\
FloverMap
.
find
e2
Gamma
=
Some
me
/
\
isCompat
me
mG
=
true
(
*
|
Cond
e1
e2
e3
=>
validTypes
e1
Gamma
/
\
validTypes
e2
Gamma
/
\
...
...
@@ -64,6 +65,7 @@ Fixpoint validTypes e (Gamma:FloverMap.t mType): Prop :=
FloverMap
.
find
e2
Gamma
=
Some
m2
/
\
FloverMap
.
find
e3
Gamma
=
Some
m3
/
\
isJoin
m2
m3
mG
=
true
*
)
end
/
\
(
forall
E
Gamma2
DeltaMap
v
m
,
(
forall
e
m
,
FloverMap
.
find
e
Gamma
=
Some
m
->
...
...
@@ -300,6 +302,7 @@ Fixpoint getValidMap (Gamma:FloverMap.t mType) (e:expr Q)
else
Fail
_
"Incorrect type for let-bound variable"
end
(
*
|
Cond
e1
e2
e3
=>
rlet
akk1_map
:=
getValidMap
Gamma
e1
akk
in
rlet
akk2_map
:=
getValidMap
Gamma
e2
akk1_map
in
...
...
@@ -328,6 +331,7 @@ Fixpoint getValidMap (Gamma:FloverMap.t mType) (e:expr Q)
end
|
_
,
_
,
_
=>
Fail
_
"Could not infer type for argument of Cond"
end
*
)
end
.
Lemma
tMap_def
:
...
...
@@ -544,6 +548,7 @@ Proof.
-
destruct
(
mTypeEq
m
m1
)
eqn
:?
;
congruence
.
-
destruct
(
mTypeEq
m
m1
)
eqn
:?
;
congruence
.
-
destruct
(
mTypeEq
m
m1
)
eqn
:?
;
congruence
.
(
*
-
destruct
(
isFixedPointB
m1
&&
isFixedPointB
m2
)
eqn
:?
;
try
congruence
;
destruct
(
morePrecise
m1
m3
&&
morePrecise
m2
m3
)
eqn
:?
;
...
...
@@ -561,6 +566,7 @@ Proof.
unfold_addMono
;
try
eauto
;
by_monotonicity
find_akk
Hmem
.
-
destruct
(
isFixedPointB
m1
&&
isFixedPointB
m2
)
eqn
:?
;
congruence
.
*
)
Qed
.
Lemma
validTypes_mono
e
:
...
...
@@ -598,6 +604,7 @@ Proof.
pose
proof
(
maps_mono
(
Var
Q
n
)
m
find_n
)
as
find_mx_map2
;
pose
proof
(
maps_mono
e2
m2
find_m2
)
as
find_m2_map2
.
eauto
.
(
*
-
destruct
check_top
as
[
valid_e1
[
valid_e2
[
valid_e3
validJoin
]]];
repeat
split
;
try
eauto
.
destruct
validJoin
as
[
m1
[
m2
[
m3
[
find_m1
[
find_m2
[
find_m3
join_true
]]]]]].
...
...
@@ -605,6 +612,7 @@ Proof.
pose
proof
(
maps_mono
e2
m2
find_m2
)
as
find_m2_map2
;
pose
proof
(
maps_mono
e3
m3
find_m3
)
as
find_m3_map2
.
repeat
eexists
;
eauto
.
*
)
Qed
.
Lemma
validTypes_eq_compat
e1
:
...
...
@@ -780,6 +788,7 @@ Proof.
rewrite
mTypeEq_refl
in
*
.
rewrite
Nat
.
compare_refl
in
*
.
rewrite
eq_rec1
in
*
.
rewrite
eq_rec2
in
*
.
rewrite
<-
H2
in
H1
;
eauto
.
(
*
-
assert
(
Q_orderedExps
.
exprCompare
e1_1
e2_1
=
Eq
)
as
eq_rec1
by
(
destruct
(
Q_orderedExps
.
exprCompare
e1_1
e2_1
)
eqn
:?
;
try
congruence
).
...
...
@@ -805,6 +814,7 @@ Proof.
+
intros
.
pose
proof
(
expr_compare_eq_eval_compat
(
Cond
e1_1
e1_2
e1_3
)
(
Cond
e2_1
e2_2
e2_3
)).
simpl
in
*
;
rewrite
<-
H1
in
H0
;
eauto
.
*
)
Qed
.
Lemma
map_find_mono
e1
e2
m1
m2
Gamma
:
...
...
@@ -1409,8 +1419,7 @@ Proof.
-
rewrite
FloverMapFacts
.
P
.
F
.
mem_find_b
in
*
.
erewrite
<-
FloverMapFacts
.
P
.
F
.
find_o
in
in_t
;
eauto
.
congruence
.
}
-
(
*
Conditional
case
*
)
admit
.
Admitted
.
Qed
.
Corollary
getValidMap_top_correct
e
:
forall
akk
Gamma
res
,
...
...
coq/ssaPrgs.v
View file @
89142369
...
...
@@ -124,11 +124,14 @@ Inductive ssa (V:Type): (expr V) -> NatSet.t -> NatSet.t -> Prop :=
ssa
e
inVars
outVars
->
ssa
s
(
NatSet
.
add
x
inVars
)
outVars
->
ssa
(
Let
m
x
e
s
)
inVars
outVars
(
*
|
ssaCond
e1
e2
e3
inVars
outVars
:
ssa
e1
inVars
outVars
->
ssa
e2
inVars
outVars
->
ssa
e3
inVars
outVars
->
ssa
(
Cond
e1
e2
e3
)
inVars
outVars
.
ssa
(
Cond
e1
e2
e3
)
inVars
outVars
*
)
.
Lemma
ssa_subset_freeVars
V
(
f
:
expr
V
)
inVars
outVars
:
ssa
f
inVars
outVars
->
...
...
@@ -140,7 +143,7 @@ Proof.
-
intros
n
.
set_tac
.
intros
[
?|
[
?|?
]];
auto
.
-
intros
n
.
set_tac
.
intros
[
?|
[
?
?
]];
auto
.
eapply
NatSetProps
.
Dec
.
F
.
add_3
;
eauto
.
-
intros
n
.
set_tac
.
intros
[
?|
[
?|?
]];
auto
.
(
*
-
intros
n
.
set_tac
.
intros
[
?|
[
?|?
]];
auto
.
*
)
Qed
.
Lemma
ssa_equal_set
V
(
f
:
expr
V
)
inVars
inVars
'
outVars
:
...
...
@@ -175,7 +178,7 @@ Fixpoint validSSA (f:expr Q) (inVars:NatSet.t) :=
|
Downcast
_
e
=>
validSSA
e
inVars
|
Let
m
x
e
g
=>
(
negb
(
NatSet
.
mem
x
inVars
))
&&
validSSA
e
inVars
&&
validSSA
g
(
NatSet
.
add
x
inVars
)
|
Cond
e1
e2
e3
=>
validSSA
e1
inVars
&&
validSSA
e2
inVars
&&
validSSA
e3
inVars
(
*
|
Cond
e1
e2
e3
=>
validSSA
e1
inVars
&&
validSSA
e2
inVars
&&
validSSA
e3
inVars
*
)
end
.
Lemma
validSSA_sound
f
inVars
:
...
...
@@ -206,12 +209,14 @@ Proof.
edestruct
IHf2
as
[
O2
?
];
eauto
.
exists
(
O1
∪
O2
).
constructor
;
eauto
using
ssa_open_out
.
(
*
-
andb_to_prop
H
.
edestruct
IHf1
as
[
O1
?
];
eauto
.
edestruct
IHf2
as
[
O2
?
];
eauto
.
edestruct
IHf3
as
[
O3
?
];
eauto
.
exists
(
O1
∪
O2
∪
O3
).
constructor
;
eauto
using
ssa_open_out
.
*
)
Qed
.
Lemma
validSSA_checks_freeVars
f
S
:
...
...
@@ -233,8 +238,10 @@ Proof.
intros
[
?
?
].
pose
proof
(
H0
_
H
).
set_tac
.
firstorder
.
(
*
-
andb_to_prop
validSSA_true
.
destruct
H
;
set_tac
;
[
apply
IHf1
|
destruct
H
;
[
apply
IHf2
|
apply
IHf3
]];
auto
.
*
)
Qed
.
Lemma
validSSA_eq_set
s
s
'
f
:
...
...
@@ -269,8 +276,10 @@ Proof.
apply
NatSetProps
.
equal_sym
in
sub
.
apply
NatSetProps
.
subset_equal
in
sub
.
split
;
set_tac
;
intuition
.
(
*
-
andb_to_prop
H
.
erewrite
IHf1
,
IHf2
,
IHf3
;
eauto
.
*
)
Qed
.
Lemma
validSSA_downward_closed
S
S
'
f
:
...
...
@@ -304,8 +313,10 @@ Proof.
*
set_tac
.
destruct
(
dec_eq_nat
a
n
);
[
now
left
|
right
;
set_tac
].
*
set_tac
.
intuition
.
(
*
-
andb_to_prop
H1
.
erewrite
IHf1
,
IHf2
,
IHf3
;
eauto
;
set_tac
.
*
)
Qed
.
Lemma
ssa_shadowing_free
m
x
y
v
v
'
e
f
inVars
outVars
E
Gamma
DeltaMap
:
...
...
Write
Preview
Markdown
is supported
0%
Try again
or
attach a new file
.
Attach a file
Cancel
You are about to add
0
people
to the discussion. Proceed with caution.
Finish editing this message first!
Cancel
Please
register
or
sign in
to comment