Should `--list-files riscv.sail_project` be empty?

[enathang]

Hello. New here, trying to wrap my head around the current state of sail and sail-riscv.

Issue
I'm following https://alasdair.github.io/#_modular_sail_specifications which has been a great tutorial so far. However, when I run sail --list-files model/riscv.sail_project I get a blank line. This is unexpected to me, because the riscv.sail_project file seems to contain a lot of files, ie

...
riscv {
  requires riscv_core, riscv_exceptions, pmp, V_core, Smcntrpmf

  files
    riscv_sys_reservation.sail,
    riscv_sys_control.sail,
    riscv_platform.sail,
    riscv_mem.sail,
    riscv_inst_retire.sail,
    riscv_vmem_pte.sail,
    riscv_vmem_ptw.sail,
    riscv_vmem_tlb.sail,
    riscv_vmem.sail,
    riscv_vmem_utils.sail,
    riscv_insts_begin.sail,
}
...

A couple hypotheses on what could be happening:

1. the guide mentions optional, default, and conditional modules, which might influence the inclusion or exclusion of files. However, I see none of those types of modules used in the sail_project file
2. The project still needs to be built (through make or cmake, not sure) to actually generate the full concatenated file. However, I've ran ./build_simulators.sh, which succeeds, but cannot find anything useful in the build/ directory.
3. I'm using sail installed through opam, which probably doesn't contain any bugfixes for the past couple weeks (I assume it lags behind source slightly). So if this was a known issue, it could already be resolved, but I don't see any closed tickets on it.

I suspect the solution is quite banal, such as "oh you just have to run x before this", but I've tried to do my due diligence on this and still have not found a solution/explanation. So any help is much appreciated!

Local details

$ sail -v
Sail 0.19.1 (sail @ opam-v2.4.1 0.19.1)

Latest commit of local riscv-sail repo: 28c80a32cda06bf25bcfc764b1e8e3797f70724a (Aug 13th).

Motivation for asking
Specifically, I'm asking this because I'm trying to get the AST output of the riscv model, but it's giving me a mostly empty AST, which I attribute (correctly or not) to the other sail files not being linked in.
Command and output:
sail --ddump-tc-ast model/riscv.sail_project

val internal_pick = monadic {_: "internal_pick"}: forall ('a : Type).
  list('a) -> 'a

val undefined_bool = monadic {_: "undefined_bool"}: unit -> bool

val undefined_bit = monadic {_: "undefined_bit"}: unit -> bit

val undefined_int = monadic {_: "undefined_int"}: unit -> int

val undefined_nat = monadic {_: "undefined_nat"}: unit -> nat

val undefined_real = monadic {_: "undefined_real"}: unit -> real

val undefined_string = monadic {_: "undefined_string"}: unit -> string

val undefined_list = monadic {_: "undefined_list"}: forall ('a : Type).
  'a -> list('a)

val undefined_range = monadic {_: "undefined_range"}: forall ('n : Int) ('m : Int).
  (int('n), int('m)) -> range('n, 'm)

val undefined_vector = monadic {_: "undefined_vector"}: forall ('n : Int) ('a : Type).
  (int('n), 'a) -> vector('n, 'a)

val undefined_bitvector = monadic {_: "undefined_bitvector"}: forall ('n : Int).
  int('n) -> bitvector('n)

val undefined_unit = monadic {_: "undefined_unit"}: unit -> unit

$[global]
val initialize_registers : unit -> unit

$[complete]
$[global]
function initialize_registers () = ()

[pmundkur]

Try sail --all-modules --list-files model/riscv.sail_project.

sail --list-files model/riscv.sail_project <module> <module> ... lists the files in the specified modules (including required dependencies). Since no <module> was specified, it gave an empty list.

[Timmmm]

Will it always print an empty list in that case? Maybe it should be an error not to supply any <module>.

[enathang]

Thanks, much appreciated! That worked. I'd close the thread now, but seems like there's a bit of ongoing discussion.

My own question: for the default/optional modules, are those declared in the sail_project file or somewhere else? I haven't found any reference to them in the code itself. I'd like to set the default module of the riscv model such that I don't need to pass in the module/--all-modules flag again, if possible. Or, maybe that's not how that works at all :)

[Timmmm]

I don't think there is a "default" - we just always use --all-modules. We've only just switched to this module system and it's very new so I wouldn't expect everything to work perfectly. I don't think anyone has actually even tried building a subset of --all-modules yet (e.g. building the model without float support for example).

[nadime15]

I think #1021 planned to only generate RV32IM. Would be nice to know if it worked or not :D

I don't think anyone has actually even tried building a subset of --all-modules yet (e.g. building the model without float support for example).

I had a discussion a few weeks ago with @pmundkur about whether it would make sense to add some sort of C/C++ style preprocessor conditionals (#ifdef, etc.) to exclude code thats hard to separate cleanly from the core files.

Extensions like Hypervisor or Debug code touch a lot of files, and I think it would be cool if people could still configure their own core and leave out everything they dont need. Right now, as far as I can tell, thats really not possible.

[Timmmm]

It is possible - Sail supports $ifdef. Currently the only use is $ifdef SYMBOLIC in main.sail. I have used it in the past to make vector optional. Worked pretty well.

It's not based on text processing (which is good!) so you can't use it in arbitrary positions, but it was flexible enough to ifdef out vector.

If we are going to do that though I think it would be good if the Sail compiler had native support for something like

$ifmodule extensions.FD
...

This would avoid:

1. Having to duplicate the list of modules into --defines.
2. Silently ignoring typos, which is a major issue with ifdef.

Also, a big danger with having a gazillion compile time configurations is that they're really difficult to test. I don't know if Sail currently enforces that any valid combination of modules will compile... but that definitely wouldn't be the case if we start adding ifdefs.