Skip to content

x86-syntax: Add syntax for flags registers #533

@langston-barrett

Description

@langston-barrett

It would be useful to have syntax for the following registers:

-- | Carry flag
cf :: Ctx.Index (MacawCrucibleRegTypes M.X86_64) C.BoolType
cf = Ctx.natIndex @CF
-- | Parity flag
pf :: Ctx.Index (MacawCrucibleRegTypes M.X86_64) C.BoolType
pf = Ctx.natIndex @PF
-- | Auxiliary carry flag
af :: Ctx.Index (MacawCrucibleRegTypes M.X86_64) C.BoolType
af = Ctx.natIndex @AF
-- | Zero flag
zf :: Ctx.Index (MacawCrucibleRegTypes M.X86_64) C.BoolType
zf = Ctx.natIndex @ZF
-- | Sign flag
sf :: Ctx.Index (MacawCrucibleRegTypes M.X86_64) C.BoolType
sf = Ctx.natIndex @SF
-- | Trap flag
tf :: Ctx.Index (MacawCrucibleRegTypes M.X86_64) C.BoolType
tf = Ctx.natIndex @TF
-- | Interrupt enable flag
if_ :: Ctx.Index (MacawCrucibleRegTypes M.X86_64) C.BoolType
if_ = Ctx.natIndex @IF
-- | Direction flag
df :: Ctx.Index (MacawCrucibleRegTypes M.X86_64) C.BoolType
df = Ctx.natIndex @DF
-- | Overflow flag
of_ :: Ctx.Index (MacawCrucibleRegTypes M.X86_64) C.BoolType
of_ = Ctx.natIndex @OF

This should be as simple as adding a few more cases here:

and some lines to this test-case:

(defun @id ((regs X86Regs)) X86Regs

We should be sure to update the documentation as well:

https://github.com/GaloisInc/macaw/blob/2560988c937eed393e22fdf14618657c8e8f60aa/macaw-x86-syntax/README.md

Checklist:

  • Add syntax
  • Modify test
  • Add docs

Metadata

Metadata

Assignees

Labels

Type

No type

Projects

No projects

Milestone

No milestone

Relationships

None yet

Development

No branches or pull requests

Issue actions