Repository navigation
Operator precedence in updateNested causes incorrect nested map update #99
Description
In updateNested, the map update operator [<-] binds tighter than
orDefault, so this rule:
rule updateNested(MAP, INDEX1, INDEX2, VALUE) => MAP[ INDEX1 <- MAP[INDEX1] orDefault .Map [INDEX2 <- VALUE] ]is parsed as (_ [INDEX2 <- VALUE] is applied to empty map):
rule updateNested(MAP, INDEX1, INDEX2, VALUE) => MAP[ INDEX1 <- MAP[INDEX1] orDefault (.Map [INDEX2 <- VALUE]) ]
^^^ ^^^The parsing can also be seen in the kdist-******/kontrol-node/simbolik/compiled.txt file:
rule updateNested(MAP,INDEX1,INDEX2,VALUE)
=>`Map:update`(
MAP,
INDEX1,
`Map:lookupOrDefault`(
MAP,
INDEX1,
`Map:update`(
`.Map`(.KList),
INDEX2,
VALUE
)
)
)
requires #token("true","Bool")
ensures #token("true","Bool")Fix: wrap the orDefault expression and add a :>Map cast:
rule updateNested(MAP, INDEX1, INDEX2, VALUE) => MAP[ INDEX1 <- {MAP[INDEX1] orDefault .Map}:>Map [INDEX2 <- VALUE] ]The cast is needed because orDefault returns KItem, which [<-] won't accept without it.
Metadata
Metadata
Assignees
Labels
No labels
Activity