Open martinberger opened 3 years ago
jrtc27
commented
3 years ago The RISC-V model already has (dis)assembly support, e.g.:
mapping clause assembly = ITYPE(imm, rs1, rd, op)
<-> itype_mnemonic(op) ^ spc() ^ reg_name(rd) ^ sep() ^ reg_name(rs1) ^ sep() ^ hex_bits_12(imm)It's unclear to me how you'd improve on that without inventing a whole new DSL.
PeterSewell
commented
3 years ago On Fri, 10 Sept 2021 at 11:17, Martin Berger @.***> wrote:
Sail currently lacks first-class support for the assembly syntax of instructions. The manual (Page 3) states that "this is something we plan to add". While technically maybe not so challenging, it is vital for a coherent description of the ISA level to captures the information required to auto-generate tools like linkers, assembler, disassemblers, machine readable documentation etc. This will be important for anyone who's doing RISCV.
As Jess says, for RISC-V there is already the assembly/disassembly mapping description in Sail, which might suffice for some purposes - though I should note that the Sail implementation for such mappings is not very mature.
I can see two core issues:
-
From a programming language point-of-view that should be straightforward, except that, in principle, assembly syntax could be arbitrarily crazy. I imagine that a language like Sail should only support 'sane' assembly languages.
The point is more that, in practice, assembly syntax is pretty crazy, with different ad hoc things in different architectures, and Sail should support at least all those of our major ISA models. Doing that well would certainly be worthwhile, but we don't internally currently need it (as we're focussed on semantics of binaries) or have spare effort for it, so we have no active plan.
There's a fair bit of previous work in the area to learn from, if someone was going to try to do it properly - for example the cgen tooling, and the work Alasdair Reid did for Armv8-A. Note also that there's quite a difference between the plain assembly syntax of instructions and the languages actually accepted by assemblers (with labels, directives, etc.).
-
I'm also not sure how to adapt a formal description of assembly syntax and associated concepts to the HOL, Isabelle/HOL, Coq and SMT-LIB backends.
There are lots of options, depending what one wanted to do - ranging from nothing at all, up to some deep embedding of the grammar and mappings that one might want to specify and prove a verified assembler.
-
I wonder what the Sail team's plans and suggestions are in this direction.
— You are receiving this because you are subscribed to this thread. Reply to this email directly, view it on GitHub https://github.com/rems-project/sail/issues/145, or unsubscribe https://github.com/notifications/unsubscribe-auth/ABFMZZRUP6UTVJK7P2AIIILUBHLLDANCNFSM5DZAW4LA . Triage notifications on the go with GitHub Mobile for iOS https://apps.apple.com/app/apple-store/id1477376905?ct=notification-email&mt=8&pt=524675 or Android https://play.google.com/store/apps/details?id=com.github.android&referrer=utm_campaign%3Dnotification-email%26utm_medium%3Demail%26utm_source%3Dgithub.
Sail currently lacks first-class support for the assembly syntax of instructions. The manual (Page 3) states that "this is something we plan to add". While technically maybe not so challenging, it is vital for a coherent description of the ISA level to captures the information required to auto-generate tools like linkers, assembler, disassemblers, machine readable documentation etc. This will be important for anyone who's doing RISCV.
I can see two core issues:
From a programming language point-of-view that should be straightforward, except that, in principle, assembly syntax could be arbitrarily crazy. I imagine that a language like Sail should only support 'sane' assembly languages.
I'm also not sure how to adapt a formal description of assembly syntax and associated concepts to the HOL, Isabelle/HOL, Coq and SMT-LIB backends.
I wonder what the Sail team's plans and suggestions are in this direction.