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
1045a1af
Commit
1045a1af
authored
Sep 06, 2016
by
Eva Darulova
Browse files
mapValues does not do what I thought it does, changing it to calls to map()
parent
fda0579d
Changes
3
Hide whitespace changes
Inline
Side-by-side
src/main/scala/daisy/analysis/SpecsProcessingPhase.scala
View file @
1045a1af
...
...
@@ -54,7 +54,7 @@ object SpecsProcessingPhase extends DaisyPhase {
// TODO: additional constraints
val
(
ranges
,
errors
)
=
extractPreCondition
(
pre
)
allRanges
+=
(
fnc
.
id
->
ranges
.
map
Values
(
x
=>
Interval
(
x
.
_1
,
x
.
_2
)
))
allRanges
+=
(
fnc
.
id
->
ranges
.
map
(
x
=>
(
x
.
_1
->
Interval
(
x
.
_
2
.
_
1
,
x
.
_2
.
_2
)
))
)
allErrors
+=
(
fnc
.
id
->
errors
)
// annotate the variables in the function body directly
...
...
@@ -82,7 +82,8 @@ object SpecsProcessingPhase extends DaisyPhase {
case
Some
(
post
)
=>
val
(
ranges
,
errors
)
=
extractPostCondition
(
post
)
requiredOutputRanges
+=
(
fnc
.
id
->
ranges
.
mapValues
(
x
=>
PartialInterval
(
x
.
_1
,
x
.
_2
)
))
requiredOutputRanges
+=
(
fnc
.
id
->
ranges
.
map
(
x
=>
(
x
.
_1
->
PartialInterval
(
x
.
_2
.
_1
,
x
.
_2
.
_2
)
)))
requiredOutputErrors
+=
(
fnc
.
id
->
errors
)
case
_
=>
...
...
src/main/scala/daisy/utils/ErrorFunctions.scala
View file @
1045a1af
...
...
@@ -47,7 +47,7 @@ trait ErrorFunctions {
val
(
_
,
error
)
=
evaluate
[
Interval
,
AffineForm
](
expr
,
inputValMap
,
inputErrorMap
.
map
Values
(
AffineForm
.
fromError
(
_
)),
inputErrorMap
.
map
(
x
=>
(
x
.
_1
->
AffineForm
.
fromError
(
x
.
_2
)
)),
Interval
.
apply
,
AffineForm
.
zero
,
AffineForm
.
fromError
,
...
...
@@ -73,8 +73,8 @@ trait ErrorFunctions {
inputErrorMap
:
Map
[
Identifier
,
Rational
])
:
Rational
=
{
val
(
_
,
error
)
=
evaluate
[
AffineForm
,
AffineForm
](
expr
,
inputValMap
.
map
Values
(
AffineForm
(
_
)),
inputErrorMap
.
map
Values
(
AffineForm
.
fromError
(
_
)),
inputValMap
.
map
(
x
=>
(
x
.
_1
->
AffineForm
(
x
.
_2
)
)),
inputErrorMap
.
map
(
x
=>
(
x
.
_1
->
AffineForm
.
fromError
(
x
.
_2
)
)),
AffineForm
.
apply
,
AffineForm
.
zero
,
AffineForm
.
fromError
,
...
...
@@ -101,7 +101,7 @@ trait ErrorFunctions {
val
(
_
,
error
)
=
evaluate
[
SMTRange
,
AffineForm
](
expr
,
inputValMap
.
map
({
case
(
id
,
int
)
=>
(
id
->
SMTRange
(
Variable
(
id
),
int
))
}),
inputErrorMap
.
map
Values
(
AffineForm
.
fromError
(
_
)),
inputErrorMap
.
map
(
x
=>
(
x
.
_1
->
AffineForm
.
fromError
(
x
.
_2
)
)),
SMTRange
.
apply
,
AffineForm
.
zero
,
AffineForm
.
fromError
,
...
...
@@ -480,7 +480,7 @@ trait ErrorFunctions {
val
(
resInterval
,
resError
)
=
evaluate
[
Interval
,
AffineForm
](
expr
,
inputsSubdiv
.
head
,
getInputErrors
(
inputsSubdiv
.
head
).
map
Values
(
AffineForm
.
fromError
(
_
)),
getInputErrors
(
inputsSubdiv
.
head
).
map
(
x
=>
(
x
.
_1
->
AffineForm
.
fromError
(
x
.
_2
)
)),
Interval
.
apply
,
AffineForm
.
zero
,
AffineForm
.
fromError
,
AffineForm
.
apply
,
false
,
trackRoundoffErrs
,
uniformPrecision
)
...
...
@@ -491,7 +491,7 @@ trait ErrorFunctions {
val
(
tmpRange
,
tmpError
)
=
evaluate
[
Interval
,
AffineForm
](
expr
,
m
,
getInputErrors
(
m
).
map
Values
(
AffineForm
.
fromError
(
_
)),
getInputErrors
(
m
).
map
(
x
=>
(
x
.
_1
->
AffineForm
.
fromError
(
x
.
_2
)
)),
Interval
.
apply
,
AffineForm
.
zero
,
AffineForm
.
fromError
,
AffineForm
.
apply
,
false
,
trackRoundoffErrs
,
uniformPrecision
)
...
...
@@ -729,7 +729,7 @@ trait ErrorFunctions {
attachInterval
(
expr
)
// Now that we have the ranges, we can compute the errors
val
resError
=
computeAndAttachError
(
expr
,
varErrorMap
.
map
Values
(
AffineForm
.
fromError
(
_
)))
val
resError
=
computeAndAttachError
(
expr
,
varErrorMap
.
map
(
x
=>
(
x
.
_1
->
AffineForm
.
fromError
(
x
.
_2
)
)))
(
currentRanges
(
expr
),
maxAbs
(
resError
.
toInterval
))
}
...
...
src/test/scala/regression/RangeRegression.scala
View file @
1045a1af
...
...
@@ -31,10 +31,10 @@ class RangeRegressionTest extends FunSuite {
for
(
fnc
<-
inputPrg
.
defs
)
if
(!
fnc
.
precondition
.
isEmpty
&&
!
fnc
.
body
.
isEmpty
)
{
val
(
ranges
,
errors
)
=
analysis
.
SpecsProcessingPhase
.
extractPreCondition
(
fnc
.
precondition
.
get
)
val
inputRanges
=
ranges
.
map
Values
(
x
=>
Interval
(
x
.
_1
,
x
.
_2
)
)
val
inputRanges
=
ranges
.
map
(
x
=>
(
x
.
_1
->
Interval
(
x
.
_
2
.
_
1
,
x
.
_2
.
_2
)
))
val
affineRange
=
utils
.
Evaluators
.
evalAffine
(
fnc
.
body
.
get
,
inputRanges
.
map
Values
(
AffineForm
(
_
)))
inputRanges
.
map
(
x
=>
(
x
.
_1
->
AffineForm
(
x
.
_2
)
)))
val
intervalRange
=
utils
.
Evaluators
.
evalInterval
(
fnc
.
body
.
get
,
inputRanges
)
val
smtRange
=
utils
.
Evaluators
.
evalSMT
(
fnc
.
body
.
get
,
...
...
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