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

Lean: add support for register definitions #894

Merged
merged 24 commits into from
Jan 27, 2025
Merged
Changes from 1 commit
Commits
File filter

Filter by extension

Filter by extension

Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
Prev Previous commit
Next Next commit
Cleaner PreSailM and RegisterState
lfrenot committed Jan 23, 2025
commit bf43b0a3aa6af4ff36220ef57d8e0d11d15fdd7f
13 changes: 7 additions & 6 deletions src/sail_lean_backend/Sail/Sail.lean
Original file line number Diff line number Diff line change
@@ -8,28 +8,29 @@ variable {Register : Type} {RegisterType : Register → Type} [DecidableEq Regis
/- The Units are placeholders for a future implementation of the state monad some Sail functions use. -/
abbrev Error := Unit

structure SequentialSate where
structure SequentialState (RegisterType : Register → Type) where
regs : Std.DHashMap Register RegisterType
mem : Unit
tags : Unit

inductive RegisterRef : Type → Type where
| Reg (r: Register) : RegisterRef (RegisterType r)

abbrev PreSailM := EStateM Error (@SequentialSate Register RegisterType _ _)
abbrev PreSailM (RegisterType : Register → Type) :=
EStateM Error (SequentialState RegisterType)

def writeReg (r : Register) (v : RegisterType r) : @PreSailM Register RegisterType _ _ Unit :=
def writeReg (r : Register) (v : RegisterType r) : PreSailM RegisterType Unit :=
modify fun s => { s with regs := s.regs.insert r v }

def readReg (r : Register) : @PreSailM Register RegisterType _ _ (RegisterType r) := do
def readReg (r : Register) : PreSailM RegisterType (RegisterType r) := do
let .some s := (← get).regs.get? r
| throw ()
pure s

def readRegRef (reg_ref : @RegisterRef Register RegisterType α) : @PreSailM Register RegisterType _ _ α := do
def readRegRef (reg_ref : @RegisterRef Register RegisterType α) : PreSailM RegisterType α := do
match reg_ref with | .Reg r => readReg r

def writeRegRef (reg_ref : @RegisterRef Register RegisterType α) (a : α) : @PreSailM Register RegisterType _ _ Unit := do
def writeRegRef (reg_ref : @RegisterRef Register RegisterType α) (a : α) : PreSailM RegisterType Unit := do
match reg_ref with | .Reg r => writeReg r a

def reg_deref (reg_ref : @RegisterRef Register RegisterType α) := readRegRef reg_ref
2 changes: 1 addition & 1 deletion src/sail_lean_backend/pretty_print_lean.ml
Original file line number Diff line number Diff line change
@@ -591,7 +591,7 @@ let doc_reg_info env registers =
[
register_enums registers;
type_enum bare_ctx registers;
string "abbrev SailM := @PreSailM Register RegisterType _ _";
string "abbrev SailM := PreSailM RegisterType";
empty;
empty;
]
2 changes: 1 addition & 1 deletion test/lean/bitfield.expected.lean
Original file line number Diff line number Diff line change
@@ -12,7 +12,7 @@ open Register
abbrev RegisterType : Register → Type
| .R => (BitVec 8)

abbrev SailM := @PreSailM Register RegisterType _ _
abbrev SailM := PreSailM RegisterType

def undefined_cr_type (lit : Unit) : SailM (BitVec 8) := do
sorry
2 changes: 1 addition & 1 deletion test/lean/registers.expected.lean
Original file line number Diff line number Diff line change
@@ -20,7 +20,7 @@ abbrev RegisterType : Register → Type
| .R1 => (BitVec 64)
| .R0 => (BitVec 64)

abbrev SailM := @PreSailM Register RegisterType _ _
abbrev SailM := PreSailM RegisterType

def test : SailM Int := do
writeReg INT (HAdd.hAdd (← readReg INT) 1)