Generating C code for Armv8 instructions

[jrprice]

I'm trying to get Sail to generate C code for an Armv8 model, but I can't seem to get it to work for any of the provided ones. I've tried installing v0.10 from the OPAM repository as well from the head of the sail2 branch.

The README indicates that the hand-written model that comes with the repository is out-of-sync with the latest Sail, and indeed I get an error when trying to use it:

$ sail -c arm/armV8.sail 
Syntax error:
[arm/armV8.sail]:1:0-0
1 |(*========================================================================*)
  |^
  | current token: (

So, I then tried the automatically generated Armv8.5 model that comes in a separate repository, but I get a different error this time:

$ sail models/arm/arm-v8.5-a/model/aarch64.sail 
Lexical error:
[models/arm/arm-v8.5-a/model/aarch64.sail]:3326:34-34
3326 |    let msg : string = "Prefetch" ++ " address=0x" ++ HexStr(UInt(address)) ++ " op=" ++ op ++ " target=" ++ target ++ " stream=" ++ stream;
     |                                  ^
     | Operator fixity undeclared ++

I have zero experience with OCaml so can't tell if there's a real issue here or if I'm just doing something wrong.

Can you give some guidance on how to get any version of Sail working with any Armv8 model? At this stage I just want to see the C code that it will generate for instruction decoding and execution, to see if I might be able to modify it to make use of for my own work.

[jrprice]

I managed to complete overlook the fact that there are Makefiles with the models, which work just fine. I was assuming there was just a single "master" .sail file needed to build a model, which clearly isn't the case. Apologies for the noise.

I'll repurpose this issue into a more useful question. Is it possible to get Sail to generate the code necessary to decode/execute just a single instruction, e.g. add wd, wn, wm, rather than the whole ISA in one huge file?

[Alasdair]

There isn't really an easy automatic way to do that for the large ARMv8 model right now, because of the way we translate it in one large blob from ARM ASL. Our other models like RISC-V have an intermediate execute function which can be split into separate clauses for each instruction, but we don't have that there. There's also a weird quirk we inherit from ARM's specification where you can get through the initial part of the decode before realizing you're executing the wrong instruction and then have to back-out to the initial decode to try-again, which makes the decode hard to split up in general. This only applies to some newer 8.4 and 8.5 instructions, but it's a major nuisance.

To explain the various models in this repository a bit more. The aarch64_small/ directory contains the updated version of the model in the arm/ directory. It's only used for concurrency semantics, so might not work for anything else. The aarch64/ directory is an older translation of (iirc) 8.2 which is missing few features compared with the separate sail-arm repository. We should probably just remove the arm/ directory.

[jrprice]

Thanks for the detailed response. Sounds like I need to have another think about how to achieve what I need.