Rangemap #3461
Rangemap #3461
Conversation
symbolic backends TODO.
…emove no longer used rangemap.
mariaKt
requested review from
radumereuta,
Baltoli and
dwightguth
and removed request for
dwightguth and
ehildenb
| implementation of range maps provided by the backend. | ||
| Although the underlying range map data structure supports any key sort, the | ||
| current implementation by the backend only supports `Int` keys due to | ||
| limitations of the underlying ordering function. |
There was a problem hiding this comment.
Is this supported by the haskell backend as well? If not, then I think it should be mentioned here that only the llvm backend implements this feature.
I think we also have some module attributes to protect against wrongful inclusion.
There was a problem hiding this comment.
In a follow-up PR, we can probably make an inefficient version of the RangeMap sort written entirely in K for use by the Haskell backend. I don't see the need to adjust the module attributes currently, although I agree about the documentation.
|
Hmmmm, what's the use case here? It seems to me that it's probably mostly useful for modelling byte-arrays, but I think the Or perhaps the idea here is a general notion of How is this datastructure being used? |
| implementation of range maps provided by the backend. | ||
| Although the underlying range map data structure supports any key sort, the | ||
| current implementation by the backend only supports `Int` keys due to | ||
| limitations of the underlying ordering function. |
There was a problem hiding this comment.
In a follow-up PR, we can probably make an inefficient version of the RangeMap sort written entirely in K for use by the Haskell backend. I don't see the need to adjust the module attributes currently, although I agree about the documentation.
|
The use case is fairly straightforward. You want to be able to map ranges of integers to values and then look up the value associated with a particular integer. Neither an array nor #buf does this in a fashion that would allow you to perform both operations in log time and linear space in the number of ranges. We're talking about cases where there might be hundreds of thousands of contiguous integers that all map to the exact same value spread out across an incredibly sparse larger range of integers... Neither an array nor any existing data type in K can do this without using vastly more memory than is practical. |
|
@ehildenb Specifically, we are dealing with this when using the C semantics with programs containing large static arrays. Currently, we are using the traditional K map to represent the memory cell, which is proving to be inefficient with such programs. |
|
|
||
| ### Implementation of range maps | ||
|
|
||
| TBD |
There was a problem hiding this comment.
If we're going to merge this into domains.md, we should have a more descriptive comment here explaining why the implementation is TBD.
…untimeverification#3134) * haskell-backend/src/main/native/haskell-backend: 8612bdfe4 - Remove redundant fields from RPC timeout response (runtimeverification#3474) * Sync flake inputs to submodules * haskell-backend/src/main/native/haskell-backend: 4e9b76ab1 - Update README section (runtimeverification#3473) * Sync flake inputs to submodules * haskell-backend/src/main/native/haskell-backend: fae73ac06 - Switch to GHC 9.2.5 (runtimeverification#3461) * Sync flake inputs to submodules * haskell-backend/src/main/native/haskell-backend: f3e87176a - [runtimeverification#2313] Remove bmc code (runtimeverification#3482) * Sync flake inputs to submodules * Remove kbmc tests --------- Co-authored-by: rv-jenkins <[email protected]> Co-authored-by: ana-pantilie <[email protected]>
This PR adds support for a new builtin type, range map, in K. Previous PRs have introduced the new type (here) and added hooks in the LLVM backend (here).
The bulk of the changes are in
domains.md, defining the relevant module.