Open RyanGlScott opened 8 months ago
For a first cut at this, we can keep it simple:
mir_vec_value
, without any integration which mir_elem
, the latter of which doesn't exist yet.Vec
values. All we'd need is the ability to create concrete ones via mir_vec_value
.Vec
values. All we'd need is the ability to pass or return raw Vec
values that were created via mir_vec_value
.Note that non-empty Vec
values need to be allocated, so perhaps we should call this mir_alloc_vec
to make this more explicit.
An array and a length works reasonably well for vectors, FWIW. You can run into problems with values in the array outside the intended valid region (so e.g. if you shrink the vector you need to explicitly clear the entries that are dropped) but as long as one remembers the hazard it isn't a big problem.
Rust's
Vec
type is very common, and we'd like to make it simpler to write specifications that useVec
values. At a first approximation, we'd like to offer amir_vec_value : [MIRType] -> MIRType
function that constructs aVec
value from a list of element values.Note that
Vec
is not a primitive MIR type, but it is instead a struct defined in terms ofRawVec
(which is in turn defined in terms ofNonNull
). As such,mir_vec_value
could be thought of as a convenient shorthand for building a particular type of struct. We might also consider offering some kind of indexing operator à lamir_elem
, as indexing into aRawVec
manually would be tedious.Some unresolved questions:
Vec
values? Presumably not, since we'd need theVec
to have a symbolic length, and Crucible isn't good at handling symbolic lengths. On the other hand, it would be convenient to be able to create aVec
of a specific length where each element is a symbolic value. We might want to add a dedicated SAWScript function for doing this.Vec
s? If so, how shouldVec
s be modeled on the Cryptol side? Cryptol has sequence types, but they are of a fixed length, unlikeVec
. We might need to introduce a primitive Cryptol type specifically for this purpose (similarly to how Cryptol has a primitiveArray
type for modeling SMT arrays).