Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Unify the representations of TupleTypeRepr and StructRepr #396

Open
RyanGlScott opened this issue Jul 15, 2024 · 0 comments
Open

Unify the representations of TupleTypeRepr and StructRepr #396

RyanGlScott opened this issue Jul 15, 2024 · 0 comments
Labels
enhancement symbolic-execution Issues relating to macaw-symbolic and symbolic execution tech-debt Technical debt that would be nice to clean up

Comments

@RyanGlScott
Copy link
Contributor

Currently, macaw-base defines TupleType as:

-- | A tuple of types
| TupleType [Type]

With a corresponding representation type, TupleTypeRepr, defined as:

TupleTypeRepr :: !(P.List TypeRepr ctx) -> TypeRepr (TupleType ctx)

This makes use of Data.Parameterized.List. When we convert Macaw tuples to Crucible values in macaw-symbolic, however, we convert the lists to Ctxs. For instance, here is how macaw-symbolic converts a list of Macaw Types to a struct of Crucible Types (which uses a Ctx under the hood):

type family ToCrucibleTypeList (l :: [M.Type]) :: Ctx C.CrucibleType where
ToCrucibleTypeList '[] = EmptyCtx
ToCrucibleTypeList (h ': l) = ToCrucibleTypeList l ::> ToCrucibleType h

Similarly, here is how the conversion looks at the representation type level:

-- | Convert a list over macaw types to a context over crucible types.
--
-- N.B. The order of elements is reversed.
macawListToCrucible :: (forall tp . a tp -> b (ToCrucibleType tp))
-> P.List a ctx
-> Assignment b (ToCrucibleTypeList ctx)
macawListToCrucible f x =
case x of
P.Nil -> Empty
h P.:< r -> macawListToCrucible f r :> f h

One peculiar thing about this conversion is that we reverse the order of fields when going from a list to a Ctx. This is rather surprising, and it has caused a handful of bugs in the past. See, for instance, #284 and #393. It would be nice if we can minimize the chances of similar bugs happening in the future.

In light of this, here is one proposal: why not change TupleType to use Ctx Type instead of [Type] as its field? If we did this, then we could to a Crucible struct without changing the order of fields at all, which would be much more straightforward. To be honest, I'm not sure why we don't do this already (aside from the breaking API changes it would introduce), given that macaw-base already depends on parameterized-utils.

@RyanGlScott RyanGlScott added enhancement symbolic-execution Issues relating to macaw-symbolic and symbolic execution tech-debt Technical debt that would be nice to clean up labels Jul 15, 2024
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Labels
enhancement symbolic-execution Issues relating to macaw-symbolic and symbolic execution tech-debt Technical debt that would be nice to clean up
Projects
None yet
Development

No branches or pull requests

1 participant