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

Deduplicate AtomWrapper, Repeat, and SymFns code across macaw-*-symbolic packages #410

Open
RyanGlScott opened this issue Jul 26, 2024 · 0 comments
Labels
arch:aarch32 AArch32 (32 bit ARM) issues arch:ppc PowerPC issues arch:riscv RISC-V issues arch:x86 x86 issues 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

RyanGlScott commented Jul 26, 2024

The macaw-*-symbolic suite of packages all define various boilerplate code in order to translate Macaw into Crucible, and each package in the suite duplicates all of this boilerplate. I propose that we deduplicate this code and put it in a better home (perhaps in macaw-symbolic, parameterized-utils, or elsewhere).

AtomWrapper

This is defined separately in macaw-aarch32-symbolic, macaw-ppc-symbolic, macaw-riscv-symbolic, and macaw-x86-symbolic:

newtype AtomWrapper (f :: C.CrucibleType -> Type) (tp :: MT.Type)
= AtomWrapper (f (MS.ToCrucibleType tp))
liftAtomMap :: (forall s. f s -> g s) -> AtomWrapper f t -> AtomWrapper g t
liftAtomMap f (AtomWrapper x) = AtomWrapper (f x)
liftAtomTrav ::
Functor m =>
(forall s. f s -> m (g s)) -> (AtomWrapper f t -> m (AtomWrapper g t))
liftAtomTrav f (AtomWrapper x) = AtomWrapper <$> f x
liftAtomIn :: (forall s. f s -> a) -> AtomWrapper f t -> a
liftAtomIn f (AtomWrapper x) = f x

newtype AtomWrapper (f :: C.CrucibleType -> DK.Type) (tp :: MT.Type)
= AtomWrapper (f (MS.ToCrucibleType tp))
liftAtomMap :: (forall s. f s -> g s) -> AtomWrapper f t -> AtomWrapper g t
liftAtomMap f (AtomWrapper x) = AtomWrapper (f x)
liftAtomTrav ::
Functor m =>
(forall s. f s -> m (g s)) -> (AtomWrapper f t -> m (AtomWrapper g t))
liftAtomTrav f (AtomWrapper x) = AtomWrapper <$> f x
liftAtomIn :: (forall s. f s -> a) -> AtomWrapper f t -> a
liftAtomIn f (AtomWrapper x) = f x

newtype AtomWrapper (f :: C.CrucibleType -> Type) (tp :: MT.Type)
= AtomWrapper (f (MS.ToCrucibleType tp))
liftAtomMap :: (forall s. f s -> g s) -> AtomWrapper f t -> AtomWrapper g t
liftAtomMap f (AtomWrapper x) = AtomWrapper (f x)
liftAtomTrav ::
Functor m =>
(forall s. f s -> m (g s)) -> (AtomWrapper f t -> m (AtomWrapper g t))
liftAtomTrav f (AtomWrapper x) = AtomWrapper <$> f x
liftAtomIn :: (forall s. f s -> a) -> AtomWrapper f t -> a
liftAtomIn f (AtomWrapper x) = f x

newtype AtomWrapper (f :: CrucibleType -> Type) (tp :: M.Type)
= AtomWrapper (f (ToCrucibleType tp))
liftAtomMap :: (forall s. f s -> g s) -> AtomWrapper f t -> AtomWrapper g t
liftAtomMap f (AtomWrapper x) = AtomWrapper (f x)
liftAtomTrav ::
Functor m =>
(forall s. f s -> m (g s)) -> (AtomWrapper f t -> m (AtomWrapper g t))
liftAtomTrav f (AtomWrapper x) = AtomWrapper <$> f x
liftAtomIn :: (forall s. f s -> a) -> AtomWrapper f t -> a
liftAtomIn f (AtomWrapper x) = f x

Repeat

This is defined separately in macaw-ppc-symbolic, macaw-riscv-symbolic, and macaw-x86-symbolic:

type family CtxRepeat (n :: Nat) (c :: k) :: Ctx.Ctx k where
CtxRepeat 0 c = Ctx.EmptyCtx
CtxRepeat n c = CtxRepeat (n - 1) c Ctx.::> c
class RepeatAssign (tp :: k) (ctx :: Ctx.Ctx k) where
repeatAssign :: (Int -> f tp) -> Ctx.Assignment f ctx
instance RepeatAssign tp Ctx.EmptyCtx where
repeatAssign _ = Ctx.Empty
instance RepeatAssign tp ctx => RepeatAssign tp (ctx Ctx.::> tp) where
repeatAssign f =
let r = repeatAssign f
in r Ctx.:> f (Ctx.sizeInt (Ctx.size r))

type family CtxRepeat (n :: Nat) (c :: k) :: Ctx.Ctx k where
CtxRepeat 0 c = Ctx.EmptyCtx
CtxRepeat n c = CtxRepeat (n - 1) c Ctx.::> c
class RepeatAssign (tp :: k) (ctx :: Ctx.Ctx k) where
repeatAssign :: (Int -> f tp) -> Ctx.Assignment f ctx
instance RepeatAssign tp Ctx.EmptyCtx where
repeatAssign _ = Ctx.Empty
instance RepeatAssign tp ctx => RepeatAssign tp (ctx Ctx.::> tp) where
repeatAssign f =
let r = repeatAssign f
in r Ctx.:> f (Ctx.sizeInt (Ctx.size r))

type family CtxRepeat (n :: Nat) (c :: k) :: Ctx k where
CtxRepeat 0 c = EmptyCtx
CtxRepeat n c = CtxRepeat (n-1) c ::> c
class RepeatAssign (tp :: k) (ctx :: Ctx k) where
repeatAssign :: (Int -> f tp) -> Assignment f ctx
instance RepeatAssign tp EmptyCtx where
repeatAssign _ = Empty
instance RepeatAssign tp ctx => RepeatAssign tp (ctx ::> tp) where
repeatAssign f =
let r = repeatAssign f
in r :> f (sizeInt (Ctx.size r))

SymFns

This is defined separately in macaw-aarch32-symbolic and macaw-ppc-symbolic:

data SomeSymFun sym where
SomeSymFun :: Ctx.Assignment WT.BaseTypeRepr ps -> WT.BaseTypeRepr r -> WI.SymFn sym ps r -> SomeSymFun sym
data SymFuns sym =
SymFuns { symFuns :: IOR.IORef (Map.Map String (SomeSymFun sym))
}

data SomeSymFun sym where
SomeSymFun :: Ctx.Assignment C.BaseTypeRepr ps -> C.BaseTypeRepr r -> C.SymFn sym ps r -> SomeSymFun sym
data SymFuns sym =
SymFuns { symFuns :: IO.IORef (M.Map String (SomeSymFun sym))
}

@RyanGlScott RyanGlScott added arch:ppc PowerPC issues arch:aarch32 AArch32 (32 bit ARM) issues symbolic-execution Issues relating to macaw-symbolic and symbolic execution tech-debt Technical debt that would be nice to clean up arch:x86 x86 issues arch:riscv RISC-V issues labels Jul 26, 2024
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Labels
arch:aarch32 AArch32 (32 bit ARM) issues arch:ppc PowerPC issues arch:riscv RISC-V issues arch:x86 x86 issues 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