mir_array_value
#1925
Merged
mir_array_value
#1925
Conversation
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
RyanGlScott
commented
Aug 30, 2023
Comment on lines
+311
to
+325
| -- match arrays point-wise | ||
| (MIRVal (ArrayShape _ _ elemShp) xs, Mir.TyArray y _len, MS.SetupArray _elemTy zs) | ||
| | Mir.MirVector_Vector xs' <- xs | ||
| , V.length xs' == length zs -> | ||
| sequence_ | ||
| [ matchArg opts sc cc cs prepost md (MIRVal elemShp x) y z | ||
| | (x, z) <- zip (V.toList xs') zs ] | ||
|
|
||
| | Mir.MirVector_PartialVector xs' <- xs | ||
| , V.length xs' == length zs -> | ||
| do xs'' <- liftIO $ | ||
| traverse (readMaybeType sym "vector element" (shapeType elemShp)) xs' | ||
| sequence_ | ||
| [ matchArg opts sc cc cs prepost md (MIRVal elemShp x) y z | ||
| | (x, z) <- zip (V.toList xs'') zs ] |
There was a problem hiding this comment.
Here is how SAW matches array arguments in specifications. Note that MirVector_Array (for symbolic, SMT-based arrays) aren't supported.
Comment on lines
+123
to
+124
| MS.SetupArray elemTy vs -> | ||
| pure $ Mir.TyArray elemTy (length vs) |
There was a problem hiding this comment.
Here is where the type of mir_array_values are computed.
Comment on lines
+2618
to
+2629
| In the experimental MIR verification implementation, the following functions | ||
| construct compound values: | ||
|
|
||
| * `mir_array_value : MIRType -> [SetupValue] -> SetupValue` constructs an array | ||
| of the given type whose elements consist of the given values. Supplying the | ||
| element type is necessary to support length-0 arrays. |
RyanGlScott
force-pushed
the
T1859-mir_array_value
branch
from
7761c9b to
f12cdf4
Compare
29 tasks
RyanGlScott
force-pushed
the
T1859-mir_array_value
branch
from
f12cdf4 to
9d74cbd
Compare
RyanGlScott
added
the
PR: ready to merge
This adds support for a `mir_array_value` function in the MIR backend, which allows constructing array `SetupValue`s. This largely behaves like `llvm_array_value`s in the LLVM backend, but with the following differences: * Unlike in the LLVM backend, MIR arrays can have length 0. To account for this possibility, `mir_array_value` has a `MIRType` argument to ensure that SAW can always infer the type of the array, even if there are no element values from which to infer the type. Similarly, the SAW remote API's `array()` function now has an optional `element_type` kwarg that can be used to specify the element type in the event that there are no element values. * Because only the MIR backend makes use of the element type, this is encoded in the `XSetupArray` extension field. This checks off one box in #1859.
RyanGlScott
force-pushed
the
T1859-mir_array_value
branch
from
9d74cbd to
ca34dbe
Compare
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment
Add this suggestion to a batch that can be applied as a single commit.
This suggestion is invalid because no changes were made to the code.
Suggestions cannot be applied while the pull request is closed.
Suggestions cannot be applied while viewing a subset of changes.
Only one suggestion per line can be applied in a batch.
Add this suggestion to a batch that can be applied as a single commit.
Applying suggestions on deleted lines is not supported.
You must change the existing code in this line in order to create a valid suggestion.
Outdated suggestions cannot be applied.
This suggestion has been applied or marked resolved.
Suggestions cannot be applied from pending reviews.
Suggestions cannot be applied on multi-line comments.
Suggestions cannot be applied while the pull request is queued to merge.
Suggestion cannot be applied right now. Please check back later.
This adds support for a
mir_array_valuefunction in the MIR backend, which allows constructing arraySetupValues. This largely behaves likellvm_array_values in the LLVM backend, but with the following differences:Unlike in the LLVM backend, MIR arrays can have length 0. To account for this possibility,
mir_array_valuehas aMIRTypeargument to ensure that SAW can always infer the type of the array, even if there are no element values from which to infer the type.Similarly, the SAW remote API's
array()function now has an optionalelement_typekwarg that can be used to specify the element type in the event that there are no element values.Because only the MIR backend makes use of the element type, this is encoded in the
XSetupArrayextension field.This checks off one box in #1859.