Add support for arrayCopy, arraySet, and arrayRangeEqual primitives #1428
Conversation
andreistefanescu
force-pushed
the
array-copy-set
branch
from
9d89e1f to
858afd6
Compare
| @@ -2242,6 +2245,18 @@ scArrayUpdate sc a b f i e = scGlobalApply sc "Prelude.arrayUpdate" [a, b, f, i, | |||
| scArrayEq :: SharedContext -> Term -> Term -> Term -> Term -> IO Term | |||
| scArrayEq sc a b x y = scGlobalApply sc "Prelude.arrayEq" [a, b, x, y] | |||
|
|
|||
| -- > arrayCopy : (n : Nat) -> (a : sort 0) -> Array (Vec n Bool) a -> Vec n Bool -> Array (Vec n Bool) a -> Vec n Bool -> Vec n Bool -> Array (Vec n Bool) a; | |||
There was a problem hiding this comment.
Let's list the names of the arguments for these. There are a lot of them, and it's easy to swap around src/dest, etc.
| @@ -184,6 +185,9 @@ prims = | |||
| , Prims.bpArrayLookup = unsupportedSBVPrimitive "bpArrayLookup" | |||
| , Prims.bpArrayUpdate = unsupportedSBVPrimitive "bpArrayUpdate" | |||
| , Prims.bpArrayEq = unsupportedSBVPrimitive "bpArrayEq" | |||
| , Prims.bpArrayCopy = unsupportedSBVPrimitive "bpArrayCopy" | |||
| , Prims.bpArraySet = unsupportedSBVPrimitive "bpArraySet" | |||
| , Prims.bpArrayRangeEq = unsupportedSBVPrimitive "bpArrayRangeEq" | |||
There was a problem hiding this comment.
This PR wouldn't be the place to implement it, probably, but doesn't the SBV library have support for SMT arrays? Is there anything stopping us from supporting them?
There was a problem hiding this comment.
As I recall, the "dynamic" SBV interface we use doesn't expose that functionality. I should double check to be sure, but I think that's why we don't support arrays or uninterpreted functions via Cryptol or SAW. It's one of the reasons I want to find a way to use the standard interface instead.
There was a problem hiding this comment.
I don't remember exactly why I didn't implement array support in the SBV backend in the first place. I am not that familiar with SBV, if it's not that complicated we could add support in the future
| sc_elm_type <- baseSCType sym sc range | ||
| SAWExpr <$> SC.scArrayEq sc sc_idx_type sc_elm_type x' y' | ||
| | otherwise -> | ||
| unsupported sym ("SAW backend: equality comparison on unsupported multidimensional array type:" ++ show tp) |
There was a problem hiding this comment.
Is the reason not to support multi-dimensional arrays here that it would be extra work, in this function, that we don't need right now? Or are there limitations elsewhere in the codebase that would make it hard to support them?
There was a problem hiding this comment.
we don't support multi-dimensional arrays in cryptol or saw-core, and we don't need them at the moment. Adding representation for multi-dimensional arrays in cryptol and saw-core, and translations for all the round-tripping would add a lot of complexity, and I wanted to keep things simple
Depends on GaloisInc/what4#152 and GaloisInc/cryptol#1268