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
a959dd8c
Commit
a959dd8c
authored
Dec 20, 2018
by
Joachim Bard
Browse files
Options
Browse Files
Download
Email Patches
Plain Diff
fixing def of unsat_queries
queries are false for every environment
parent
954cb8ec
Changes
5
Hide whitespace changes
Inline
Side-by-side
Showing
5 changed files
with
11 additions
and
12 deletions
+11
-12
coq/CertificateChecker.v
coq/CertificateChecker.v
+2
-2
coq/IEEE_connection.v
coq/IEEE_connection.v
+2
-2
coq/RealRangeValidator.v
coq/RealRangeValidator.v
+2
-2
coq/SMTArith.v
coq/SMTArith.v
+2
-2
coq/SMTValidation.v
coq/SMTValidation.v
+3
-4
No files found.
coq/CertificateChecker.v
View file @
a959dd8c
...
...
@@ -33,7 +33,7 @@ Theorem Certificate_checking_is_sound (e:expr Q) (absenv:analysisResult) P Qmap
(
forall
(
e
'
:
expr
R
)
(
m
'
:
mType
),
exists
d
:
R
,
DeltaMap
e
'
m
'
=
Some
d
/
\
(
Rabs
d
<=
mTypeToR
m
'
)
%
R
)
->
eval_precond
E1
P
->
unsat_queries
E1
Qmap
->
unsat_queries
Qmap
->
CertificateChecker
e
absenv
P
Qmap
defVars
=
true
->
exists
Gamma
,
approxEnv
E1
(
toRExpMap
Gamma
)
absenv
(
usedVars
e
)
NatSet
.
empty
E2
->
...
...
@@ -108,7 +108,7 @@ Theorem Certificate_checking_cmds_is_sound (f:cmd Q) (absenv:analysisResult) P Q
(
forall
(
e
'
:
expr
R
)
(
m
'
:
mType
),
exists
d
:
R
,
DeltaMap
e
'
m
'
=
Some
d
/
\
(
Rabs
d
<=
mTypeToR
m
'
)
%
R
)
->
eval_precond
E1
P
->
unsat_queries
E1
Qmap
->
unsat_queries
Qmap
->
CertificateCheckerCmd
f
absenv
P
Qmap
defVars
=
true
->
exists
Gamma
,
approxEnv
E1
(
toRExpMap
Gamma
)
absenv
(
freeVars
f
)
NatSet
.
empty
E2
->
...
...
coq/IEEE_connection.v
View file @
a959dd8c
...
...
@@ -1139,7 +1139,7 @@ Theorem IEEE_connection_expr e A P qMap E1 E2 defVars DeltaMap:
is64BitEnv
defVars
->
noDowncast
(
B2Qexpr
e
)
->
eval_expr_valid
e
E2
->
unsat_queries
E1
qMap
->
unsat_queries
qMap
->
eval_precond
E1
P
->
CertificateChecker
(
B2Qexpr
e
)
A
P
qMap
defVars
=
true
->
exists
Gamma
,
(
*
m
,
currently
=
M64
*
)
...
...
@@ -1209,7 +1209,7 @@ Theorem IEEE_connection_cmd (f:cmd fl64) (A:analysisResult) P qMap
is64BitEnv
defVars
->
noDowncastFun
(
B2Qcmd
f
)
->
bstep_valid
f
E2
->
unsat_queries
E1
qMap
->
unsat_queries
qMap
->
eval_precond
E1
P
->
CertificateCheckerCmd
(
B2Qcmd
f
)
A
P
qMap
defVars
=
true
->
exists
Gamma
,
...
...
coq/RealRangeValidator.v
View file @
a959dd8c
...
...
@@ -27,7 +27,7 @@ Theorem RangeValidator_sound (e : expr Q) (A : analysisResult) (P : precond)
affine_dVars_range_valid
dVars
E
A
1
(
FloverMap
.
empty
(
affine_form
Q
))
(
fun
_
:
nat
=>
None
)
->
validTypes
e
Gamma
->
eval_precond
E
P
->
unsat_queries
E
Qmap
->
unsat_queries
Qmap
->
validRanges
e
A
E
(
toRTMap
(
toRExpMap
Gamma
)).
Proof
.
intros
.
...
...
@@ -80,7 +80,7 @@ Theorem RangeValidatorCmd_sound (f : cmd Q) (A : analysisResult) (P : precond)
NatSet
.
Subset
(
preVars
P
)
fVars
->
NatSet
.
Subset
(
freeVars
f
--
dVars
)
fVars
->
validTypesCmd
f
Gamma
->
unsat_queries
E
Qmap
->
unsat_queries
Qmap
->
validRangesCmd
f
A
E
(
toRTMap
(
toRExpMap
Gamma
)).
Proof
.
intros
ranges_valid
;
intros
.
...
...
coq/SMTArith.v
View file @
a959dd8c
...
...
@@ -290,8 +290,8 @@ Inductive eval_smt_logic (E: env) : SMTLogic -> Prop :=
|
OrQ_eval_r
q1
q2
:
eval_smt_logic
E
q2
->
eval_smt_logic
E
(
OrQ
q1
q2
).
*
)
Definition
unsat_queries
E
qMap
:=
forall
e
ql
qh
,
FloverMap
.
find
e
qMap
=
Some
(
ql
,
qh
)
->
~
eval_smt_logic
E
ql
/
\
~
eval_smt_logic
E
qh
.
Definition
unsat_queries
qMap
:=
forall
E
e
ql
qh
,
FloverMap
.
find
e
qMap
=
Some
(
ql
,
qh
)
->
~
eval_smt_logic
E
ql
/
\
~
eval_smt_logic
E
qh
.
(
*
Lemma
eval_precond_sound
fVars
E
P
:
...
...
coq/SMTValidation.v
View file @
a959dd8c
...
...
@@ -198,7 +198,7 @@ Fixpoint validSMTIntervalbounds (e: expr Q) (A: analysisResult) (P: precond)
Theorem
validSMTIntervalbounds_sound
(
f
:
expr
Q
)
(
A
:
analysisResult
)
(
P
:
precond
)
(
Q
:
usedQueries
)
fVars
dVars
(
E
:
env
)
Gamma
:
unsat_queries
E
Q
->
unsat_queries
Q
->
validSMTIntervalbounds
f
A
P
Q
dVars
=
true
->
dVars_range_valid
dVars
E
A
->
NatSet
.
Subset
((
Expressions
.
usedVars
f
)
--
dVars
)
fVars
->
...
...
@@ -443,7 +443,7 @@ Theorem validSMTIntervalboundsCmd_sound (f:cmd Q) (A:analysisResult)
eval_precond
E
P
->
NatSet
.
Subset
(
preVars
P
)
fVars
->
NatSet
.
Subset
(
Commands
.
freeVars
f
--
dVars
)
fVars
->
unsat_queries
E
Q
->
unsat_queries
Q
->
validSMTIntervalboundsCmd
f
A
P
Q
dVars
=
true
->
validTypesCmd
f
Gamma
->
validRangesCmd
f
A
E
(
toRTMap
(
toRExpMap
Gamma
)).
...
...
@@ -503,7 +503,6 @@ Proof.
repeat
split
;
try
auto
.
+
hnf
;
intros
;
subst
.
apply
H1
;
set_tac
.
+
hnf
;
intros
.
apply
H1
;
set_tac
.
-
admit
.
(
*
TODO
:
fix
def
of
unsat_queries
*
)
}
(
*
destruct
x_contained
as
[
x_free
|
x_def
].
...
...
@@ -554,4 +553,4 @@ Proof.
apply
validRanges_single
in
valid_e
.
destruct
valid_e
as
[
?
[
?
[
?
[
?
[
?
?
]]]]];
try
auto
.
simpl
in
*
.
repeat
eexists
;
repeat
split
;
try
eauto
;
[
econstructor
;
eauto
|
|
];
lra
.
Admitted
.
\ No newline at end of file
Qed
.
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