mirror of
https://github.com/GaloisInc/cryptol.git
synced 2024-12-17 13:01:31 +03:00
Fix symbolic simulator implementations of (!!) and (@@)
Now these operations correctly set the is-bit flag on the VSeq constructor when the result type is a list of bits. Fixes #148.
This commit is contained in:
parent
88983488fc
commit
ccfbd1f2de
@ -206,7 +206,7 @@ evalECon econ =
|
|||||||
VFun $ \xs ->
|
VFun $ \xs ->
|
||||||
VFun $ \ys ->
|
VFun $ \ys ->
|
||||||
let err = zeroV a -- default for out-of-bounds accesses
|
let err = zeroV a -- default for out-of-bounds accesses
|
||||||
in mapV (selectV (\i -> nthV err xs i)) ys
|
in mapV (isTBit a) (selectV (\i -> nthV err xs i)) ys
|
||||||
|
|
||||||
ECAtBack -> -- {n,a,i} (fin n, fin i) => [n]a -> [i] -> a
|
ECAtBack -> -- {n,a,i} (fin n, fin i) => [n]a -> [i] -> a
|
||||||
tlam $ \(finTValue -> n) ->
|
tlam $ \(finTValue -> n) ->
|
||||||
@ -225,7 +225,7 @@ evalECon econ =
|
|||||||
VFun $ \xs ->
|
VFun $ \xs ->
|
||||||
VFun $ \ys ->
|
VFun $ \ys ->
|
||||||
let err = zeroV a -- default for out-of-bounds accesses
|
let err = zeroV a -- default for out-of-bounds accesses
|
||||||
in mapV (selectV (\i -> nthV err xs (n - 1 - i))) ys
|
in mapV (isTBit a) (selectV (\i -> nthV err xs (n - 1 - i))) ys
|
||||||
|
|
||||||
ECFromThen -> fromThenV
|
ECFromThen -> fromThenV
|
||||||
ECFromTo -> fromToV
|
ECFromTo -> fromToV
|
||||||
@ -315,10 +315,10 @@ nthV err v n =
|
|||||||
VBit (SBV.sbvTestBit x i)
|
VBit (SBV.sbvTestBit x i)
|
||||||
_ -> err
|
_ -> err
|
||||||
|
|
||||||
mapV :: (Value -> Value) -> Value -> Value
|
mapV :: Bool -> (Value -> Value) -> Value -> Value
|
||||||
mapV f v =
|
mapV isBit f v =
|
||||||
case v of
|
case v of
|
||||||
VSeq b xs -> VSeq b (map f xs)
|
VSeq _ xs -> VSeq isBit (map f xs)
|
||||||
VStream xs -> VStream (map f xs)
|
VStream xs -> VStream (map f xs)
|
||||||
_ -> panic "Cryptol.Symbolic.Prims.mapV" [ "non-mappable value" ]
|
_ -> panic "Cryptol.Symbolic.Prims.mapV" [ "non-mappable value" ]
|
||||||
|
|
||||||
|
Loading…
Reference in New Issue
Block a user