rems-project / sail

Sail architecture definition language
Other
617 stars 112 forks source link

providing an out of the box tutorial example #56

Open farhanpapin opened 5 years ago

farhanpapin commented 5 years ago

While trying to test sail I tried the

A trutorial RISCV example : riscv_duopod.sail

as shown on the manual chapter 2. It does not work out of the box. for instance when I tried type checking riscv_duopod.sail, type regbits = bits(5) throws an error

could not find type constructor bits and option(ast) throws an error

could not find type constructor option

after manually adding ./lib/vector_dec.sail and ./lib/option.sail it throws an error

Type error. No default order has been set

It would be very helpful to provide an out of the box tutorial example

Alasdair commented 5 years ago

Sorry the manual and example was a little out of sync. I've updated it so it should be more self-contained now. It does depend on the riscv prelude.sail defined in sail-riscv, which is what sets the default order (some instruction set architectures differ on whether they consider the MSB of a byte bit 0 or the LSB to be bit 0 which is what that controls), but hopefully this is clearer now.

farhanpapin commented 5 years ago

Thank you. That solved the issue with type checking. Once I reach the C compilation there are other dependencies missing e.g, (in manual section 3.2: C compilation) gcc out.c $SAIL_DIR/lib/*.c -lgmp -lz -I $SAIL_DIR/lib/ -o out complains about

undefined reference to zmain

grep for zmain returns many files a lot of which are definition, making it a bit unclear which file to include.
Is there an end-end tutorial at-least for C compilation that someone new to SAIL could use to demonstrate / understand usage of sail?

ourspalois commented 2 years ago

HI, i am running into a similar issue with the compilation of the C code generated by sail

undefined reference to zmain

have you found a solution ? I tried searching but the only definition of zmain i found was in the ocaml backend, but since i dont know much about ocaml i am having difficulties understanding how to solve the problem

Alasdair commented 2 years ago

By default it'll generate a C main function that calls a main function written in Sail. The sail main function will be name-mangled in the C output as zmain (we use an encoding similar to GHC Haskell's to encode any ascii string as a C identifier https://gitlab.haskell.org/ghc/ghc/-/wikis/commentary/compiler/symbol-names). I'd guess you want the -c_no_main flag to suppress generating this main function.