Lean: Memory model #965
Lean: Memory model #965
Conversation
lfrenot
force-pushed
the
lean/Arch-class
branch
from
e971e3e to
bb9d031
Compare
src/sail_lean_backend/Sail/Sail.lean
Outdated
| @@ -80,4 +148,5 @@ def addInt {w : Nat} (x : BitVec w) (i : Int) : BitVec w := | |||
| x + BitVec.ofInt w i | |||
|
|
|||
| end BitVec | |||
|
|
|||
There was a problem hiding this comment.
This is unrelated. Do we want to change this?
There was a problem hiding this comment.
No we don't, I've removed it
Need to figure out what `outcome` and `impl` are and what they should correspond to...
This backs out commit 84ad935.
lfrenot
force-pushed
the
lean/Arch-class
branch
from
2790e40 to
7058f9c
Compare
src/sail_lean_backend/Sail/Sail.lean
Outdated
| def write_byte (value : BitVec 8) (addr : Nat) : PreSailM RegisterType c PUnit := do | ||
| modify fun s => { s with mem := s.mem.insert addr value } | ||
| pure () | ||
|
|
||
| def write_bytes (addr : Nat) (value : BitVec (8 * n)) : PreSailM RegisterType c Bool := do |
There was a problem hiding this comment.
The two arguments are in the opposite order in the two functions
|
Should I add SailTinyArm as a CI test to this PR? |
Let's try! |
|
Not sure why it is failing, it works on my end |
|
I think I found it, needed to add the changes from removing the |
src/sail_lean_backend/Sail/Sail.lean
Outdated
| match size with | ||
| | 0 => pure (default, some true) | ||
| | n + 1 => do | ||
| let b ← read_byte addr |
There was a problem hiding this comment.
I don't think the do block should get an extra indentation here.
There was a problem hiding this comment.
Done
I've also renamed the internal functions to camelCase
| pure true | ||
|
|
||
| def sail_mem_write [Arch] (req : Mem_write_request n vasize (BitVec pa_size) ts arch) : PreSailM RegisterType c (Result (Option Bool) Arch.abort) := do | ||
| let addr := req.pa.toNat |
There was a problem hiding this comment.
Where does this toNat comes from?
There was a problem hiding this comment.
the type of req in the argument fixes req.pa to be a BitVec pa_size
So that toNat is BitVec.toNat
src/sail_lean_backend/Sail/Sail.lean
Outdated
|
|
||
| def readBytes (size : Nat) (addr : Nat) : PreSailM RegisterType c ((BitVec (8 * size)) × Option Bool) := | ||
| match size with | ||
| | 0 => pure (default, some true) |
There was a problem hiding this comment.
In theory, the Option Bool of a memory read is only used if you want to read a tag (the tag field of the request is true) otherwise it should be none, but it's not really important, and I don't think sail code that does not want a tag will crash if you return some true
This closes #959