Generating C disassemblers and assemblers from Sail

[moste00]

Hello, I'm working with the Capstone project to generate a RISC-V disassembler module from the Sail description of RISC-V maintained here. Previously Capstone relied on LLVM descriptions and metadata for automatically generating C assemblers and disassemblers, but those were found to be outdated and containing subtle errors. Capstone thus decided to start relying on Sail descriptions of architectures, at least with RISC-V.

I wanted to ask a couple of questions that I can't find easy answers to in the documentation.

Am I reinventing the wheel ?

Sail already has a C backend. The Sail manual linked above seems to imply that all Sail is translatable to C, however, almost all discussions that I see about Sail here and elsewhere reference the C backend only in the context of generating an "execution model", namely the execute function clauses of an arch model.

For my part, I did a small experiment where I wrote a very trivial and toy arch model, a single decode rule that uses the @ operator to destructure a bitvector into fields. Although the model passes type-checking and OCaml generation, the C backend keeps failing on it with errors along the lines of No overloading for vector_subrange and No overloading for operator (==).

What I am asking for is: A clarification of the exact scope of the C backend. What is the subset of Sail that the C backend definitely 100% supports? Is there any known deviations or bugs in the backend within this subset? Is the generated code readable (unlikely given that it's generated from the low-level instructions in Sail IR form, but asking here just to make sure), and/or suitable in any way to be called from human-written code?

Essentially, what I am asking is: is it worth it to write yet another generator, specialized for generating disassemblers in particular? Or is the C backend adequate enough and need only minor bug fixes and/or documentation and tutorials?

This question may be somewhat "too late" since I have already written a first prototype of the specialized generator tool, it's nearly 1/2 of the C backend at about 1200 lines of code. I appreciate any feedback if this is necessary, or if what I want to achieve* could be achieved by clever usage of the C backend. If the answer to the last question is "yes", it could still be worth it to compare the 2 generators, and possibly rely on the C backend if possible when the RISC-V model uses features that isn't supported by my custom generator.

* : "What I want to achieve" is generating a bunch of C files that faithfully emulates the logic of RISC-V decoding, defined as a bunch of mapping rules in the RISCV arch models. Hopefully the generated C is readable, but that's not strictly necessary.

Am I reinventing half of a wheel

In the case of the C backend not suitable for my purposes, I have a feeling I'm still reinventing parts of Sail's implementation. For example, the type checker.

One of the things that my generator has to do is computing the bitvector lengths of all arguments in an AST union case. This is in order that a bitvector destructuring expression like rs @ rd, where rs and rd have no explicit type annotations, can still be accepted because rs and rd are used on the other side of the mapping rule where the type of the member list of the union case can provide info regarding their lengths. Sail have a fully-general type-inference algorithm, but my generator does this in ad-hoc sense as needed, possibly crashing on cases that the Sail type checker handles easily.

What I'm asking is: Can I use the output of Sail's type checker to do this? I'm using the function Frontend.load_files to load the Sail files of the RISCV model. This function returns the sail code as an AST, my generator does all further processing on this AST. The function also returns a "Type Env", does this "Type Env" encode all information about all types in the AST? Can this information be used efficiently?

Is Sail designed to use as a library

As a final question: Is our way of usage supported by Sail or does it work by sheer luck? By "Our way of use" I mean including Sail as an OCaml library and building a tool on top of it. Is Sail's implementation written with this in mind or will we encounter friction because Sail was never meant to be used like this?

Sorry for the wall of questions! Have a nice day.

[Alasdair]

Sail already has a C backend. The Sail manual linked above seems to imply that all Sail is translatable to C, however, almost all discussions that I see about Sail here and elsewhere reference the C backend only in the context of generating an "execution model", namely the execute function clauses of an arch model.

The only thing that is not currently translated is the string parsing part of the mappings. If we wanted to translate those we might need to generate something more like a yacc grammar. In particular the string append pattern x ^ y doesn't have a good translation, as you can't decide how to split the input string without a somewhat sophisticated parsing approach. Right now because there isn't an exact semantics for these string append patterns, they get marked as being not-executable and we ensure they aren't used in the executable part of the semantics.

Is the generated code readable (unlikely given that it's generated from the low-level instructions in Sail IR form, but asking here just to make sure), and/or suitable in any way to be called from human-written code?

The code within functions is not particularly readable. When we have to monomorphise function calls the generated names can become pretty gnarly, but in general the name-mangling scheme we use is predictable and doesn't mangle most names that much. I didn't intend for the generated C code to be called as a library originally (only that it would build an emulator). In practice people have done this a bunch, and it makes it tricky to improve the output as a library because there are now backwards-compatibility concerns. I think we could have an option that avoids any name-mangling where possible, and tries to produce a nicer library but would need a little bit of work.

Essentially, what I am asking is: is it worth it to write yet another generator, specialized for generating disassemblers in particular? Or is the C backend adequate enough and need only minor bug fixes and/or documentation and tutorials?

I think parts of the C backend might be what you want, but it might require a bit of refactoring to make what you are trying to do easier.

What I'm asking is: Can I use the output of Sail's type checker to do this? I'm using the function Frontend.load_files to load the Sail files of the RISCV model. This function returns the sail code as an AST, my generator does all further processing on this AST. The function also returns a "Type Env", does this "Type Env" encode all information about all types in the AST? Can this information be used efficiently?

Yes, I think the function you are looking for is Type_check.typ_of, or Type_check.typ_of_pat. There's also env_of_* functions in that module which returns the typing environment for that node.

As a final question: Is our way of usage supported by Sail or does it work by sheer luck? By "Our way of use" I mean including Sail as an OCaml library and building a tool on top of it. Is Sail's implementation written with this in mind or will we encounter friction because Sail was never meant to be used like this?

I think the answer to this is 'yes', but it's a rather qualified yes. The splitting into a main library and plugins for each backend is mostly for our own code organisation purposes - different backends can have varying levels of quality and maturity, and particularly experimental ones can in theory live out-of-tree until they are mature enough. Other people using it is not a problem, but we don't guarantee any kind of API compatibility between Sail versions. If people build something that is generally useful and wouldn't be a maintenance burden going forwards, then the ideal situation would be to upstream it.