Skip to content
GitLab
Menu
Projects
Groups
Snippets
Help
Help
Support
Community forum
Keyboard shortcuts
?
Submit feedback
Contribute to GitLab
Sign in / Register
Toggle navigation
Menu
Open sidebar
AVA
FloVer
Commits
5cf86e1f
Commit
5cf86e1f
authored
Feb 27, 2017
by
Heiko Becker
Browse files
Fix certificate generation to adhere to new structure of Daisy from ava daisy
parent
55696143
Changes
5
Hide whitespace changes
Inline
Side-by-side
src/main/scala/daisy/Context.scala
View file @
5cf86e1f
...
...
@@ -12,6 +12,8 @@ import scala.collection.immutable.Seq
import
scala.reflect.ClassTag
import
lang.Identifiers._
import
lang.Trees._
import
utils.
{
Interval
,
PartialInterval
,
Rational
}
case
class
Context
(
...
...
@@ -36,6 +38,9 @@ case class Context(
specResultRangeBounds
:
Map
[
Identifier
,
PartialInterval
]
=
Map
(),
specResultErrorBounds
:
Map
[
Identifier
,
Rational
]
=
Map
(),
analysisAbsoluteErrors
:
Map
[
Identifier
,
Map
[
Expr
,
Rational
]]
=
Map
(),
analysisRanges
:
Map
[
Identifier
,
Map
[
Expr
,
Interval
]]
=
Map
(),
// the analysed/computed roundoff errors for each function
resultAbsoluteErrors
:
Map
[
Identifier
,
Rational
]
=
Map
(),
resultRealRanges
:
Map
[
Identifier
,
Interval
]
=
Map
()
...
...
src/main/scala/daisy/analysis/RangeErrorPhase.scala
View file @
5cf86e1f
...
...
@@ -92,6 +92,9 @@ object RangeErrorPhase extends DaisyPhase with RoundoffEvaluators with IntervalS
val
fncsToConsider
:
Seq
[
String
]
=
functionsToConsider
(
ctx
,
prg
)
var
roundoffErrorMap
:
Map
[
Identifier
,
Map
[
Expr
,
Rational
]]
=
Map
()
var
rangeResMap
:
Map
[
Identifier
,
Map
[
Expr
,
Interval
]]
=
Map
()
val
res
:
Map
[
Identifier
,
(
Rational
,
Interval
)]
=
prg
.
defs
.
filter
(
fnc
=>
!
fnc
.
precondition
.
isEmpty
&&
!
fnc
.
body
.
isEmpty
&&
...
...
@@ -129,10 +132,8 @@ object RangeErrorPhase extends DaisyPhase with RoundoffEvaluators with IntervalS
allIDs
.
map
(
id
=>
(
id
->
zero
)).
toMap
}
// TODO: Interval-only based error estimation; should be a very quick fix
val
(
resError
:
Rational
,
resRange
:
Interval
)
=
(
rangeMethod
,
errorMethod
)
match
{
val
(
resError
:
Rational
,
resRange
:
Interval
,
rangeMap
:
Map
[
Expr
,
Interval
],
errorMap
:
Map
[
Expr
,
Interval
]
)
=
(
rangeMethod
,
errorMethod
)
match
{
case
(
"interval"
,
"interval"
)
=>
uniformRoundoff_IA_IA
(
fnc
.
body
.
get
,
inputValMap
,
inputErrorMap
,
uniformPrecision
,
trackRoundoffErrs
)
case
(
"interval"
,
"affine"
)
=>
...
...
@@ -159,13 +160,19 @@ object RangeErrorPhase extends DaisyPhase with RoundoffEvaluators with IntervalS
"for computing ranges and errors is not supported."
)
null
}
roundoffErrorMap
+=
(
fnc
.
id
->
(
errorMap
.
map
(
x
=>
x
.
_1
->
x
.
_2
.
xhi
)))
rangeResMap
+=
(
fnc
.
id
->
rangeMap
)
(
fnc
.
id
->
(
resError
,
resRange
))
}).
toMap
timer
.
stop
ctx
.
reporter
.
info
(
s
"Finished $name"
)
(
ctx
.
copy
(
resultAbsoluteErrors
=
res
.
map
(
x
=>
(
x
.
_1
->
x
.
_2
.
_1
)),
resultRealRanges
=
res
.
map
(
x
=>
(
x
.
_1
->
x
.
_2
.
_2
))),
prg
)
(
ctx
.
copy
(
resultAbsoluteErrors
=
res
.
map
(
x
=>
(
x
.
_1
->
x
.
_2
.
_1
)),
resultRealRanges
=
res
.
map
(
x
=>
(
x
.
_1
->
x
.
_2
.
_2
)),
analysisAbsoluteErrors
=
roundoffErrorMap
,
analysisRanges
=
rangeResMap
),
prg
)
}
...
...
src/main/scala/daisy/backend/CertificatePhase.scala
View file @
5cf86e1f
...
...
@@ -5,7 +5,7 @@ import daisy.lang.{ScalaPrinter, PrettyPrinter}
import
lang.Trees._
import
lang.Identifiers._
import
lang.NumAnnotation
import
utils.Interval
._
import
utils.Interval
import
utils.Rational
import
analysis.SpecsProcessingPhase
...
...
@@ -20,7 +20,9 @@ object CertificatePhase extends DaisyPhase {
def
run
(
ctx
:
Context
,
prg
:
Program
)
:
(
Context
,
Program
)
=
{
val
reporter
=
ctx
.
reporter
val
proverToUse
=
ctx
.
findOption
(
Main
.
optionValidators
)
val
prover
=
ctx
.
findOption
(
Main
.
optionValidators
)
val
errorMap
=
ctx
.
resultAbsoluteErrors
val
rangeMap
=
ctx
.
resultRealRanges
def
writeToFile
(
fileContent
:
String
,
prover
:
String
,
fname
:
String
){
import
java.io.FileWriter
...
...
@@ -30,9 +32,9 @@ object CertificatePhase extends DaisyPhase {
"./coq/output/certificate_"
+
prg
.
id
+
"_"
+
fname
+
".v"
else
if
(
prover
==
"hol4"
)
"./hol4/output/certificate_"
+
prg
.
id
+
"_"
+
fname
+
"Script.sml"
else
"./hol-light/output/certificate_"
+
prg
.
id
+
"_"
+
fname
+
".hl"
"./hol4/output/certificate_"
+
prg
.
id
+
"_"
+
fname
+
"Script.sml"
else
"./hol-light/output/certificate_"
+
prg
.
id
+
"_"
+
fname
+
".hl"
val
fstream
=
new
FileWriter
(
fileLocation
)
val
out
=
new
BufferedWriter
(
fstream
)
out
.
write
(
fileContent
)
...
...
@@ -43,8 +45,13 @@ object CertificatePhase extends DaisyPhase {
reporter
.
info
(
s
"Generating certificate for ${fnc.id}"
)
val
thePrecondition
=
fnc
.
precondition
val
theBody
=
fnc
.
body
//must be set
assert
(
ctx
.
analysisAbsoluteErrors
.
get
(
fnc
.
id
)
!=
None
)
val
errorMap
=
ctx
.
analysisAbsoluteErrors
.
get
(
fnc
.
id
).
get
assert
(
ctx
.
analysisRanges
.
get
(
fnc
.
id
)
!=
None
)
val
rangeMap
=
ctx
.
analysisRanges
.
get
(
fnc
.
id
).
get
prover
ToUse
match
{
prover
match
{
case
Some
(
prv
)
=>
thePrecondition
match
{
case
Some
(
pre
)
=>
...
...
@@ -55,7 +62,7 @@ object CertificatePhase extends DaisyPhase {
//generate the precondition
val
(
thePreconditionFunction
,
functionName
)
=
getPrecondFunction
(
pre
,
reporter
,
prv
)
//the analysis result function
val
(
analysisResultText
,
analysisResultName
)
=
getAbsEnvDef
(
theBody
.
get
,
prv
)
val
(
analysisResultText
,
analysisResultName
)
=
getAbsEnvDef
(
theBody
.
get
,
errorMap
,
rangeMap
,
prv
)
//generate the final evaluation statement
val
functionCall
=
getComputeExpr
(
lastGenName
,
analysisResultName
,
functionName
,
prv
)
//val functionCall = getAllComputeExps(theBody.get, analysisResultName, functionName, prv)
...
...
@@ -71,16 +78,11 @@ object CertificatePhase extends DaisyPhase {
//write to the output file
writeToFile
(
certificateText
,
prv
,
fnc
.
id
.
toString
)
case
None
=>
reporter
.
fatalError
(
"No Precondition specified"
)
case
None
=>
reporter
.
fatalError
(
"No Precondition specified
.
"
)
}
case
None
=>
reporter
.
fatalError
(
"
Failure
"
)
case
None
=>
reporter
.
fatalError
(
"
No theorem prover specified.
"
)
}
}
//generate definitions for "program"
//obtain analysis result from ctx?
//generate abstract environment for analysis result
(
ctx
,
prg
)
}
...
...
@@ -377,57 +379,59 @@ object CertificatePhase extends DaisyPhase {
}
}
private
def
coqAbsEnv
(
e
:
Expr
,
cont
:
String
)
:
String
=
private
def
coqAbsEnv
(
e
:
Expr
,
errorMap
:
Map
[
Expr
,
Rational
],
rangeMap
:
Map
[
Expr
,
Interval
],
cont
:
String
)
:
String
=
{
//must be set TODO:Assert?
//since we already generated the AST, we can be sure to have generated the name
assert
(
expressionNames
(
e
)
!=
None
)
val
nameE
=
expressionNames
(
e
)
e
match
{
case
x
@
Variable
(
id
)
=>
val
intvE
=
coqInterval
((
x
.
interval
.
xlo
,
x
.
interval
.
xhi
))
val
errE
=
x
.
absError
.
toFractionString
.
replace
(
"/"
,
"#"
)
val
intvE
=
coqInterval
((
rangeMap
(
x
).
xlo
,
rangeMap
(
x
)
.
xhi
))
val
errE
=
errorMap
(
x
)
.
toFractionString
.
replace
(
"/"
,
"#"
)
"if expEqBool e "
+
nameE
+
" then ("
+
intvE
+
","
+
errE
+
")\n"
+
" else "
+
cont
case
x
@
RealLiteral
(
r
)
=>
val
intvE
=
coqInterval
((
x
.
interval
.
xlo
,
x
.
interval
.
xhi
))
val
errE
=
x
.
absError
.
toFractionString
.
replace
(
"/"
,
"#"
)
val
intvE
=
coqInterval
((
rangeMap
(
x
).
xlo
,
rangeMap
(
x
)
.
xhi
))
val
errE
=
errorMap
(
x
)
.
toFractionString
.
replace
(
"/"
,
"#"
)
"if expEqBool e "
+
nameE
+
" then ("
+
intvE
+
","
+
errE
+
")\n"
+
" else "
+
cont
case
x
@
Plus
(
lhs
,
rhs
)
=>
val
lFun
=
coqAbsEnv
(
lhs
,
cont
)
val
rFun
=
coqAbsEnv
(
rhs
,
lFun
)
val
intvE
=
coqInterval
((
x
.
interval
.
xlo
,
x
.
interval
.
xhi
))
val
errE
=
x
.
absError
.
toFractionString
.
replace
(
"/"
,
"#"
)
val
lFun
=
coqAbsEnv
(
lhs
,
errorMap
,
rangeMap
,
cont
)
val
rFun
=
coqAbsEnv
(
rhs
,
errorMap
,
rangeMap
,
lFun
)
val
intvE
=
coqInterval
((
rangeMap
(
x
).
xlo
,
rangeMap
(
x
)
.
xhi
))
val
errE
=
errorMap
(
x
)
.
toFractionString
.
replace
(
"/"
,
"#"
)
"if expEqBool e "
+
nameE
+
" then ("
+
intvE
+
","
+
errE
+
")\n"
+
" else "
+
rFun
case
x
@
Minus
(
lhs
,
rhs
)
=>
val
lFun
=
coqAbsEnv
(
lhs
,
cont
)
val
rFun
=
coqAbsEnv
(
rhs
,
lFun
)
val
intvE
=
coqInterval
((
x
.
interval
.
xlo
,
x
.
interval
.
xhi
))
val
errE
=
x
.
absError
.
toFractionString
.
replace
(
"/"
,
"#"
)
val
lFun
=
coqAbsEnv
(
lhs
,
errorMap
,
rangeMap
,
cont
)
val
rFun
=
coqAbsEnv
(
rhs
,
errorMap
,
rangeMap
,
lFun
)
val
intvE
=
coqInterval
((
rangeMap
(
x
).
xlo
,
rangeMap
(
x
)
.
xhi
))
val
errE
=
errorMap
(
x
)
.
toFractionString
.
replace
(
"/"
,
"#"
)
"if expEqBool e "
+
nameE
+
" then ("
+
intvE
+
","
+
errE
+
")\n"
+
" else "
+
rFun
case
x
@
Times
(
lhs
,
rhs
)
=>
val
lFun
=
coqAbsEnv
(
lhs
,
cont
)
val
rFun
=
coqAbsEnv
(
rhs
,
lFun
)
val
intvE
=
coqInterval
((
x
.
interval
.
xlo
,
x
.
interval
.
xhi
))
val
errE
=
x
.
absError
.
toFractionString
.
replace
(
"/"
,
"#"
)
val
lFun
=
coqAbsEnv
(
lhs
,
errorMap
,
rangeMap
,
cont
)
val
rFun
=
coqAbsEnv
(
rhs
,
errorMap
,
rangeMap
,
lFun
)
val
intvE
=
coqInterval
((
rangeMap
(
x
).
xlo
,
rangeMap
(
x
)
.
xhi
))
val
errE
=
errorMap
(
x
)
.
toFractionString
.
replace
(
"/"
,
"#"
)
"if expEqBool e "
+
nameE
+
" then ("
+
intvE
+
","
+
errE
+
")\n"
+
" else "
+
rFun
case
x
@
Division
(
lhs
,
rhs
)
=>
val
lFun
=
coqAbsEnv
(
lhs
,
cont
)
val
rFun
=
coqAbsEnv
(
rhs
,
lFun
)
val
intvE
=
coqInterval
((
x
.
interval
.
xlo
,
x
.
interval
.
xhi
))
val
errE
=
x
.
absError
.
toFractionString
.
replace
(
"/"
,
"#"
)
val
lFun
=
coqAbsEnv
(
lhs
,
errorMap
,
rangeMap
,
cont
)
val
rFun
=
coqAbsEnv
(
rhs
,
errorMap
,
rangeMap
,
lFun
)
val
intvE
=
coqInterval
((
rangeMap
(
x
).
xlo
,
rangeMap
(
x
)
.
xhi
))
val
errE
=
errorMap
(
x
)
.
toFractionString
.
replace
(
"/"
,
"#"
)
"if expEqBool e "
+
nameE
+
" then ("
+
intvE
+
","
+
errE
+
")\n"
+
" else "
+
rFun
...
...
@@ -436,57 +440,57 @@ object CertificatePhase extends DaisyPhase {
}
}
private
def
hol4AbsEnv
(
e
:
Expr
,
cont
:
String
)
:
String
=
private
def
hol4AbsEnv
(
e
:
Expr
,
errorMap
:
Map
[
Expr
,
Rational
],
rangeMap
:
Map
[
Expr
,
Interval
],
cont
:
String
)
:
String
=
{
//must be set TODO:Assert?
val
nameE
=
expressionNames
(
e
)
e
match
{
case
x
@
Variable
(
id
)
=>
val
intvE
=
hol4Interval
((
x
.
interval
.
xlo
,
x
.
interval
.
xhi
))
val
errE
=
x
.
absError
.
toFractionString
val
intvE
=
hol4Interval
((
rangeMap
(
x
).
xlo
,
rangeMap
(
x
)
.
xhi
))
val
errE
=
errorMap
(
x
)
.
toFractionString
"if e = "
+
nameE
+
" then ("
+
intvE
+
","
+
errE
+
")\n"
+
" else "
+
cont
case
x
@
RealLiteral
(
r
)
=>
val
intvE
=
hol4Interval
((
x
.
interval
.
xlo
,
x
.
interval
.
xhi
))
val
errE
=
x
.
absError
.
toFractionString
val
intvE
=
hol4Interval
((
rangeMap
(
x
).
xlo
,
rangeMap
(
x
)
.
xhi
))
val
errE
=
errorMap
(
x
)
.
toFractionString
"if e = "
+
nameE
+
" then ("
+
intvE
+
","
+
errE
+
")\n"
+
" else "
+
cont
case
x
@
Plus
(
lhs
,
rhs
)
=>
val
lFun
=
hol4AbsEnv
(
lhs
,
cont
)
val
rFun
=
hol4AbsEnv
(
rhs
,
lFun
)
val
intvE
=
hol4Interval
((
x
.
interval
.
xlo
,
x
.
interval
.
xhi
))
val
errE
=
x
.
absError
.
toFractionString
val
lFun
=
hol4AbsEnv
(
lhs
,
errorMap
,
rangeMap
,
cont
)
val
rFun
=
hol4AbsEnv
(
rhs
,
errorMap
,
rangeMap
,
lFun
)
val
intvE
=
hol4Interval
((
rangeMap
(
x
).
xlo
,
rangeMap
(
x
)
.
xhi
))
val
errE
=
errorMap
(
x
)
.
toFractionString
"if e = "
+
nameE
+
" then ("
+
intvE
+
","
+
errE
+
")\n"
+
" else "
+
rFun
case
x
@
Minus
(
lhs
,
rhs
)
=>
val
lFun
=
hol4AbsEnv
(
lhs
,
cont
)
val
rFun
=
hol4AbsEnv
(
rhs
,
lFun
)
val
intvE
=
hol4Interval
((
x
.
interval
.
xlo
,
x
.
interval
.
xhi
))
val
errE
=
x
.
absError
.
toFractionString
val
lFun
=
hol4AbsEnv
(
lhs
,
errorMap
,
rangeMap
,
cont
)
val
rFun
=
hol4AbsEnv
(
rhs
,
errorMap
,
rangeMap
,
lFun
)
val
intvE
=
hol4Interval
((
rangeMap
(
x
).
xlo
,
rangeMap
(
x
)
.
xhi
))
val
errE
=
errorMap
(
x
)
.
toFractionString
"if e = "
+
nameE
+
" then ("
+
intvE
+
","
+
errE
+
")\n"
+
" else "
+
rFun
case
x
@
Times
(
lhs
,
rhs
)
=>
val
lFun
=
hol4AbsEnv
(
lhs
,
cont
)
val
rFun
=
hol4AbsEnv
(
rhs
,
lFun
)
val
intvE
=
hol4Interval
((
x
.
interval
.
xlo
,
x
.
interval
.
xhi
))
val
errE
=
x
.
absError
.
toFractionString
val
lFun
=
hol4AbsEnv
(
lhs
,
errorMap
,
rangeMap
,
cont
)
val
rFun
=
hol4AbsEnv
(
rhs
,
errorMap
,
rangeMap
,
lFun
)
val
intvE
=
hol4Interval
((
rangeMap
(
x
).
xlo
,
rangeMap
(
x
)
.
xhi
))
val
errE
=
errorMap
(
x
)
.
toFractionString
"if e = "
+
nameE
+
" then ("
+
intvE
+
","
+
errE
+
")\n"
+
" else "
+
rFun
case
x
@
Division
(
lhs
,
rhs
)
=>
val
lFun
=
hol4AbsEnv
(
lhs
,
cont
)
val
rFun
=
hol4AbsEnv
(
rhs
,
lFun
)
val
intvE
=
hol4Interval
((
x
.
interval
.
xlo
,
x
.
interval
.
xhi
))
val
errE
=
x
.
absError
.
toFractionString
val
lFun
=
hol4AbsEnv
(
lhs
,
errorMap
,
rangeMap
,
cont
)
val
rFun
=
hol4AbsEnv
(
rhs
,
errorMap
,
rangeMap
,
lFun
)
val
intvE
=
hol4Interval
((
rangeMap
(
x
).
xlo
,
rangeMap
(
x
)
.
xhi
))
val
errE
=
errorMap
(
x
)
.
toFractionString
"if e = "
+
nameE
+
" then ("
+
intvE
+
","
+
errE
+
")\n"
+
" else "
+
rFun
...
...
@@ -496,57 +500,57 @@ object CertificatePhase extends DaisyPhase {
}
}
private
def
holLightAbsEnv
(
e
:
Expr
,
cont
:
String
)
:
String
=
private
def
holLightAbsEnv
(
e
:
Expr
,
errorMap
:
Map
[
Expr
,
Rational
],
rangeMap
:
Map
[
Expr
,
Interval
],
cont
:
String
)
:
String
=
{
//must be set TODO:Assert?
val
nameE
=
expressionNames
(
e
)
e
match
{
case
x
@
Variable
(
id
)
=>
val
intvE
=
holLightInterval
((
x
.
interval
.
xlo
,
x
.
interval
.
xhi
))
val
errE
=
x
.
absError
.
toFractionString
.
replace
(
"("
,
"(&"
)
val
errE
=
errorMap
(
x
)
.
toFractionString
.
replace
(
"("
,
"(&"
)
"if e = "
+
nameE
+
" then ("
+
intvE
+
","
+
errE
+
")\n"
+
" else "
+
cont
case
x
@
RealLiteral
(
r
)
=>
val
intvE
=
holLightInterval
((
x
.
interval
.
xlo
,
x
.
interval
.
xhi
))
val
errE
=
x
.
absError
.
toFractionString
.
replace
(
"("
,
"(&"
)
val
errE
=
errorMap
(
x
)
.
toFractionString
.
replace
(
"("
,
"(&"
)
"if e = "
+
nameE
+
" then ("
+
intvE
+
","
+
errE
+
")\n"
+
" else "
+
cont
case
x
@
Plus
(
lhs
,
rhs
)
=>
val
lFun
=
holLightAbsEnv
(
lhs
,
cont
)
val
rFun
=
holLightAbsEnv
(
rhs
,
lFun
)
val
lFun
=
holLightAbsEnv
(
lhs
,
errorMap
,
rangeMap
,
cont
)
val
rFun
=
holLightAbsEnv
(
rhs
,
errorMap
,
rangeMap
,
lFun
)
val
intvE
=
holLightInterval
((
x
.
interval
.
xlo
,
x
.
interval
.
xhi
))
val
errE
=
x
.
absError
.
toFractionString
.
replace
(
"("
,
"(&"
)
val
errE
=
errorMap
(
x
)
.
toFractionString
.
replace
(
"("
,
"(&"
)
"if e = "
+
nameE
+
" then ("
+
intvE
+
","
+
errE
+
")\n"
+
" else "
+
rFun
case
x
@
Minus
(
lhs
,
rhs
)
=>
val
lFun
=
holLightAbsEnv
(
lhs
,
cont
)
val
rFun
=
holLightAbsEnv
(
rhs
,
lFun
)
val
lFun
=
holLightAbsEnv
(
lhs
,
errorMap
,
rangeMap
,
cont
)
val
rFun
=
holLightAbsEnv
(
rhs
,
errorMap
,
rangeMap
,
lFun
)
val
intvE
=
holLightInterval
((
x
.
interval
.
xlo
,
x
.
interval
.
xhi
))
val
errE
=
x
.
absError
.
toFractionString
.
replace
(
"("
,
"(&"
)
val
errE
=
errorMap
(
x
)
.
toFractionString
.
replace
(
"("
,
"(&"
)
"if e = "
+
nameE
+
" then ("
+
intvE
+
","
+
errE
+
")\n"
+
" else "
+
rFun
case
x
@
Times
(
lhs
,
rhs
)
=>
val
lFun
=
holLightAbsEnv
(
lhs
,
cont
)
val
rFun
=
holLightAbsEnv
(
rhs
,
lFun
)
val
lFun
=
holLightAbsEnv
(
lhs
,
errorMap
,
rangeMap
,
cont
)
val
rFun
=
holLightAbsEnv
(
rhs
,
errorMap
,
rangeMap
,
lFun
)
val
intvE
=
holLightInterval
((
x
.
interval
.
xlo
,
x
.
interval
.
xhi
))
val
errE
=
x
.
absError
.
toFractionString
.
replace
(
"("
,
"(&"
)
val
errE
=
errorMap
(
x
)
.
toFractionString
.
replace
(
"("
,
"(&"
)
"if e = "
+
nameE
+
" then ("
+
intvE
+
","
+
errE
+
")\n"
+
" else "
+
rFun
case
x
@
Division
(
lhs
,
rhs
)
=>
val
lFun
=
holLightAbsEnv
(
lhs
,
cont
)
val
rFun
=
holLightAbsEnv
(
rhs
,
lFun
)
val
lFun
=
holLightAbsEnv
(
lhs
,
errorMap
,
rangeMap
,
cont
)
val
rFun
=
holLightAbsEnv
(
rhs
,
errorMap
,
rangeMap
,
lFun
)
val
intvE
=
holLightInterval
((
x
.
interval
.
xlo
,
x
.
interval
.
xhi
))
val
errE
=
x
.
absError
.
toFractionString
.
replace
(
"("
,
"(&"
)
val
errE
=
errorMap
(
x
)
.
toFractionString
.
replace
(
"("
,
"(&"
)
"if e = "
+
nameE
+
" then ("
+
intvE
+
","
+
errE
+
")\n"
+
" else "
+
rFun
...
...
@@ -556,15 +560,18 @@ object CertificatePhase extends DaisyPhase {
}
}
private
def
getAbsEnvDef
(
e
:
Expr
,
prv
:
String
)
:
(
String
,
String
)
=
private
def
getAbsEnvDef
(
e
:
Expr
,
errorMap
:
Map
[
Expr
,
Rational
],
rangeMap
:
Map
[
Expr
,
Interval
],
prv
:
String
)
:
(
String
,
String
)
=
if
(
prv
==
"coq"
)
(
"Definition absenv :analysisResult := \nfun (e:exp Q) =>\n"
+
coqAbsEnv
(
e
,
"((0#1,0#1),0#1)"
)
+
"."
,
(
"Definition absenv :analysisResult := \nfun (e:exp Q) =>\n"
+
coqAbsEnv
(
e
,
errorMap
,
rangeMap
,
"((0#1,0#1),0#1)"
)
+
"."
,
"absenv"
)
else
if
(
prv
==
"hol4"
)
(
"val absenv_def = Define `absenv:analysisResult = \n\\e. \n"
+
hol4AbsEnv
(
e
,
"((0,1),1)"
)
+
"`;"
,
(
"val absenv_def = Define `absenv:analysisResult = \n\\e. \n"
+
hol4AbsEnv
(
e
,
errorMap
,
rangeMap
,
"((0,1),1)"
)
+
"`;"
,
"absenv"
)
else
(
"let absenv = define `absenv:analysisResult = \n\\e. \n"
+
holLightAbsEnv
(
e
,
"((&0,&1),&1)"
)
+
"`;;"
,
(
"let absenv = define `absenv:analysisResult = \n\\e. \n"
+
holLightAbsEnv
(
e
,
errorMap
,
rangeMap
,
"((&0,&1),&1)"
)
+
"`;;"
,
"absenv"
)
private
def
getComputeExpr
(
lastGenName
:
String
,
analysisResultName
:
String
,
precondName
:
String
,
prover
:
String
)
:
String
=
...
...
src/main/scala/daisy/utils/IntervalSubdivision.scala
View file @
5cf86e1f
...
...
@@ -75,7 +75,7 @@ trait IntervalSubdivision extends RoundoffEvaluators {
}
val
(
resError
,
resInterval
)
=
uniformRoundoff_IA_AA
(
expr
,
val
(
resError
,
resInterval
,
_
,
_
)
=
uniformRoundoff_IA_AA
(
expr
,
inputsSubdiv
.
head
,
getInputErrors
(
inputsSubdiv
.
head
),
uniformPrecision
)
// val (resInterval, resError) = evaluate[Interval, AffineForm](
// expr, inputsSubdiv.head,
...
...
@@ -88,7 +88,7 @@ trait IntervalSubdivision extends RoundoffEvaluators {
for
(
m
<-
inputsSubdiv
.
tail
)
{
val
(
tmpError
,
tmpRange
)
=
uniformRoundoff_IA_AA
(
expr
,
m
,
val
(
tmpError
,
tmpRange
,
_
,
_
)
=
uniformRoundoff_IA_AA
(
expr
,
m
,
getInputErrors
(
m
),
uniformPrecision
)
// evaluate[Interval, AffineForm](
...
...
src/main/scala/daisy/utils/RoundoffEvaluators.scala
View file @
5cf86e1f
...
...
@@ -12,6 +12,35 @@ import Rational.{min, abs, sqrtDown, one}
trait
RoundoffEvaluators
extends
RangeEvaluators
{
/**
* Calculate static error using interval ranges and interval errors
*
* @param expr Expression whose erros is to be calculated
* @param inputValMap Map from function identifier to its input value interval
* @param inputErrorMap Map from function
*/
def
uniformRoundoff_IA_IA
(
expr
:
Expr
,
inputValMap
:
Map
[
Identifier
,
Interval
],
inputErrorMap
:
Map
[
Identifier
,
Rational
],
uniformPrecision
:
Precision
,
trackRoundoffErrors
:
Boolean
=
true
)
:
(
Rational
,
Interval
,
Map
[
Expr
,
Interval
],
Map
[
Expr
,
Interval
])
=
{
val
(
resRange
,
intermediateRanges
)
=
evalRange
[
Interval
](
expr
,
inputValMap
.
map
(
x
=>
(
x
.
_1
->
Interval
(
x
.
_2
))),
Interval
.
apply
)
val
(
resRoundoff
,
allErrors
)
=
evalRoundoff
[
Interval
](
expr
,
intermediateRanges
,
allVariablesOf
(
expr
).
map
(
id
=>
(
id
->
uniformPrecision
)).
toMap
,
inputErrorMap
.
map
(
x
=>
(
x
.
_1
->
Interval
.
fromError
(
x
.
_2
))),
zeroError
=
Interval
.
zero
,
fromError
=
Interval
.
fromError
,
interval2T
=
Interval
.
apply
,
constantsPrecision
=
uniformPrecision
,
trackRoundoffErrors
)
(
Interval
.
maxAbs
(
resRoundoff
.
toInterval
),
resRange
,
intermediateRanges
,
allErrors
)
}
/**
* Calculates the roundoff error for a given uniform precision
* using interval arithmetic for ranges and affine arithmetic for errors.
...
...
@@ -28,10 +57,9 @@ trait RoundoffEvaluators extends RangeEvaluators {
inputValMap
:
Map
[
Identifier
,
Interval
],
inputErrorMap
:
Map
[
Identifier
,
Rational
],
uniformPrecision
:
Precision
,
trackRoundoffErrors
:
Boolean
=
true
)
:
(
Rational
,
Interval
)
=
{
trackRoundoffErrors
:
Boolean
=
true
)
:
(
Rational
,
Interval
,
Map
[
Expr
,
Interval
],
Map
[
Expr
,
Interval
]
)
=
{
val
(
resRange
,
intermediateRanges
)
=
evalRange
[
Interval
](
expr
,
inputValMap
,
Interval
.
apply
)
//println(intermediateRanges.mkString("\n"))
val
(
resRoundoff
,
allErrors
)
=
evalRoundoff
[
AffineForm
](
expr
,
intermediateRanges
,
...
...
@@ -43,37 +71,8 @@ trait RoundoffEvaluators extends RangeEvaluators {
constantsPrecision
=
uniformPrecision
,
trackRoundoffErrors
)
(
Interval
.
maxAbs
(
resRoundoff
.
toInterval
),
resRange
)
}
/**
* Calculate static error using interval ranges and interval errors
*
* @param expr Expression whose erros is to be calculated
* @param inputValMap Map from function identifier to its input value interval
* @param inputErrorMap Map from function
*/
def
uniformRoundoff_IA_IA
(
expr
:
Expr
,
inputValMap
:
Map
[
Identifier
,
Interval
],
inputErrorMap
:
Map
[
Identifier
,
Rational
],
uniformPrecision
:
Precision
,
trackRoundoffErrors
:
Boolean
=
true
)
:
(
Rational
,
Interval
)
=
{
val
(
resRange
,
intermediateRanges
)
=
evalRange
[
Interval
](
expr
,
inputValMap
.
map
(
x
=>
(
x
.
_1
->
Interval
(
x
.
_2
))),
Interval
.
apply
)
val
(
resRoundoff
,
allErrors
)
=
evalRoundoff
[
Interval
](
expr
,
intermediateRanges
.
map
(
x
=>
(
x
.
_1
->
x
.
_2
.
toInterval
)),
allVariablesOf
(
expr
).
map
(
id
=>
(
id
->
uniformPrecision
)).
toMap
,
inputErrorMap
.
map
(
x
=>
(
x
.
_1
->
Interval
.
fromError
(
x
.
_2
))),
zeroError
=
Interval
.
zero
,
fromError
=
Interval
.
fromError
,
interval2T
=
Interval
.
apply
,
constantsPrecision
=
uniformPrecision
,
trackRoundoffErrors
)
(
Interval
.
maxAbs
(
resRoundoff
.
toInterval
),
resRange
)
(
Interval
.
maxAbs
(
resRoundoff
.
toInterval
),
resRange
,
intermediateRanges
,
allErrors
.
map
(
x
=>
(
x
.
_1
->
x
.
_2
.
toInterval
)))
}
/**
...
...
@@ -90,7 +89,7 @@ trait RoundoffEvaluators extends RangeEvaluators {
inputValMap
:
Map
[
Identifier
,
Interval
],
inputErrorMap
:
Map
[
Identifier
,
Rational
],
uniformPrecision
:
Precision
,
trackRoundoffErrors
:
Boolean
=
true
)
:
(
Rational
,
Interval
)
=
{
trackRoundoffErrors
:
Boolean
=
true
)
:
(
Rational
,
Interval
,
Map
[
Expr
,
Interval
],
Map
[
Expr
,
Interval
]
)
=
{
val
(
resRange
,
intermediateRanges
)
=
evalRange
[
AffineForm
](
expr
,
inputValMap
.
map
(
x
=>
(
x
.
_1
->
AffineForm
(
x
.
_2
))),
AffineForm
.
apply
)
...
...
@@ -105,7 +104,9 @@ trait RoundoffEvaluators extends RangeEvaluators {
constantsPrecision
=
uniformPrecision
,
trackRoundoffErrors
)
(
Interval
.
maxAbs
(
resRoundoff
.
toInterval
),
resRange
.
toInterval
)
(
Interval
.
maxAbs
(
resRoundoff
.
toInterval
),
resRange
.
toInterval
,
intermediateRanges
.
map
(
x
=>
(
x
.
_1
->
x
.
_2
.
toInterval
)),
allErrors
.
map
(
x
=>
(
x
.
_1
->
x
.
_2
.
toInterval
)))
}
/**
...
...
@@ -122,7 +123,7 @@ trait RoundoffEvaluators extends RangeEvaluators {
inputValMap
:
Map
[
Identifier
,
Interval
],
inputErrorMap
:
Map
[
Identifier
,
Rational
],
uniformPrecision
:
Precision
,
trackRoundoffErrors
:
Boolean
=
true
)
:
(
Rational
,
Interval
)
=
{
trackRoundoffErrors
:
Boolean
=
true
)
:
(
Rational
,
Interval
,
Map
[
Expr
,
Interval
],
Map
[
Expr
,
Interval
]
)
=
{
val
(
resRange
,
intermediateRanges
)
=
evalRange
[
SMTRange
](
expr
,
inputValMap
.
map
({
case
(
id
,
int
)
=>
(
id
->
SMTRange
(
Variable
(
id
),
int
))
}),
...
...
@@ -138,7 +139,9 @@ trait RoundoffEvaluators extends RangeEvaluators {
constantsPrecision
=
uniformPrecision
,
trackRoundoffErrors
)
(
Interval
.
maxAbs
(
resRoundoff
.
toInterval
),
resRange
.
toInterval
)
(
Interval
.
maxAbs
(
resRoundoff
.
toInterval
),
resRange
.
toInterval
,
intermediateRanges
.
map
(
x
=>
(
x
.
_1
->
x
.
_2
.
toInterval
)),
allErrors
.
map
(
x
=>
(
x
.
_1
->
x
.
_2
.
toInterval
)))
}
/**
...
...
@@ -179,7 +182,8 @@ trait RoundoffEvaluators extends RangeEvaluators {
def
eval
(
e
:
Expr
,
errorMap
:
Map
[
Identifier
,
T
])
:
(
T
,
Precision
)
=
(
e
:
@unchecked
)
match
{
case
x
@
RealLiteral
(
r
)
=>
val
rndoff
=
if
(
isExactInFloats
(
r
,
constantsPrecision
)
||
!
trackRoundoffErrors
)
{
//val rndoff = if (isExactInFloats(r, constantsPrecision) || !trackRoundoffErrors) {
val
rndoff
=
if
(!
trackRoundoffErrors
)
{
zeroError
}
else
{
fromError
(
constantsPrecision
.
absRoundoff
(
r
))
...
...
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