Passing Elf Tests

[LiuTaowen-Tony]

Hi,

I am new to this sail-riscv project. I encountered some problems with compiling and running the elf tests.

Initially I used opam install sail to download sail. However, when running sh test/run_tests.sh, I failed all the tests except from the Building {32 | 64} bit RISCV {OCaml | C} emulator.

I thought probably I used an incompatible version of sail, so I tried to build sail manually. However, this time, I tried to run "sail tests" (the test for sail, not for riscv model), but I got several tests failed (e.g. type_pow_zero, castreq, exint, rewrites). I don't know how to fix them, so I proceeded this version of sail.

When running make at sail-riscv directory, I got an error that generated_definitions/Isabelle/RV64/Riscv.thy extra character at the end of g command. Despite I failed to generate definition for Isabelle, I still got Ocaml and C emulators. But when I run sh test/run_tests.sh I got the same result (no test passed).

The sail interactive worked fine. And the result of opam list is attached below.

I am not quite sure if this is a sail version problem. Any advices would be very helpful for me.

Sincerely, Tony

base-bigarray   base
base-bytes      base        Bytes library distributed with the OCaml compiler
base-threads    base
base-unix       base
base64          3.5.0       Base64 encoding for OCaml
biniou          1.2.1       Binary data format designed for speed, safety, ease 
conf-findutils  1           Virtual package relying on findutils
conf-gmp        4           Virtual package relying on a GMP lib system installa
conf-pkg-config 2           Check if pkg-config is installed and create an opam 
conf-zlib       1           Virtual package relying on zlib
cppo            1.6.8       Code preprocessor like cpp for OCaml
dune            2.9.3       Fast, portable, and opinionated build system
easy-format     1.3.2       High-level and functional interface to the Format mo
lem             2020-06-03  Lem is a tool for lightweight executable mathematics
linenoise       1.3.1       Lightweight readline alternative
linksem         0.7         A formalisation of the core ELF file format written 
menhir          20211128    An LR(1) parser generator
menhirLib       20211128    Runtime support library for parsers generated by Men
menhirSdk       20211128    Compile-time library for auxiliary tools related to 
num             1.4         The legacy Num library for arbitrary-precision integ
ocaml           4.12.0      The OCaml compiler (virtual package)
ocaml-config    2           OCaml Switch Configuration
ocaml-system    4.12.0      The OCaml compiler (system version, from outside of 
ocamlbuild      0.14.1      OCamlbuild is a build system with builtin rules to e
ocamlfind       1.9.3       A library manager for OCaml
omd             1.3.1       A Markdown frontend in pure OCaml.
ott             0.31        A tool for writing definitions of programming langua
pprint          20211129    A pretty-printing combinator library and rendering e
result          1.5         Compatibility Result module
sail            0.14        pinned to version 0.14 at git+file:///Users/anothert
yojson          1.7.0       Yojson is an optimized parsing and printing library 
zarith          1.12        Implements arithmetic and logical operations over ar

[jrtc27]

Hi,

I am new to this sail-riscv project. I encountered some problems with compiling and running the elf tests.

Initially I used opam install sail to download sail. However, when running sh test/run_tests.sh, I failed all the tests except from the Building {32 | 64} bit RISCV {OCaml | C} emulator.

That is supported. You should look at why the tests are failing, not just randomly try things with no real reason. Look at the .out and .cout files to see what the errors are, or run one of the tests by hand. Just saying it didn't work isn't really something we can help with.

I thought probably I used an incompatible version of sail, so I tried to build sail manually. However, this time, I tried to run "sail tests" (the test for sail, not for riscv model), but I got several tests failed (e.g. type_pow_zero, castreq, exint, rewrites). I don't know how to fix them, so I proceeded this version of sail.

Not a concern for sail-riscv; if you are following the correct build instructions and see failing tests then that's something to take up with the Sail compiler itself, not here.

When running make at sail-riscv directory, I got an error that generated_definitions/Isabelle/RV64/Riscv.thy extra character at the end of g command. Despite I failed to generate definition for Isabelle, I still got Ocaml and C emulators. But when I run sh test/run_tests.sh I got the same result (no test passed).

"g command"? If you get errors, please give the actual error, not some vague description thereof.

The sail interactive worked fine. And the result of opam list is attached below.

I am not quite sure if this is a sail version problem. Any advices would be very helpful for me.

0.14 is supported, and the latest released version.

[LiuTaowen-Tony]

Thank you so much for helping me!

I didn't know that there are .out and .cout files. And because I cloned an unchanged version of sail, and I still got the problem, so that I thought it was a sail compiler version problem.

With the help of error messages shown in .out and .cout files, I found the problems are caused by different paths in different systems.

Thank you again!

[LiuTaowen-Tony]

As for

I got an error that generated_definitions/Isabelle/RV64/Riscv.thy extra character at the end of g command.

The exact error message is attached below.

sed -i 's/datatype ast/datatype (plugins only: size) ast/' generated_definitions/isabelle/RV64/Riscv_types.thy
sed: 1: "generated_definitions/i ...": extra characters at the end of g command
make: *** [generated_definitions/isabelle/RV64/Riscv.thy] Error 1
make: *** Deleting file `generated_definitions/isabelle/RV64/Riscv.thy'

I am not familiar with Isabelle, so that I don't know what is the exact problem. It seems that I have a syntax error on the first line of generated_definitions/isabelle/RV64/Riscv_types.thy. I think showing the first few lines of this file might be helpful, so I attached them at the end.

I am sorry for the vague descriptions, and thank you for your help.

chapter \<open>Generated by Lem from \<open>generated_definitions/lem/RV64/riscv_types.lem\<close>.\<close>

theory "Riscv_types" 

imports
  Main
  "LEM.Lem_pervasives_extra"
  "Sail.Sail2_instr_kinds"
  "Sail.Sail2_values"
  "Sail.Sail2_operators_mwords"
  "Sail.Sail2_prompt_monad"
  "Sail.Sail2_prompt"
  "Sail.Sail2_string"

begin 

\<comment> \<open>\<open>Generated by Sail from riscv.\<close>\<close>
\<comment> \<open>\<open>open import Pervasives_extra\<close>\<close>
\<comment> \<open>\<open>open import Sail2_instr_kinds\<close>\<close>
\<comment> \<open>\<open>open import Sail2_values\<close>\<close>
\<comment> \<open>\<open>open import Sail2_string\<close>\<close>
\<comment> \<open>\<open>open import Sail2_operators_mwords\<close>\<close>
\<comment> \<open>\<open>open import Sail2_prompt_monad\<close>\<close>
\<comment> \<open>\<open>open import Sail2_prompt\<close>\<close>

[jrtc27]

The file contents or the fact it's Isabelle is irrelevant. All it's saying is that there's a problem with the sed command being run by the Makefile. I assume you're running on macOS; those sed commands are written for GNU sed, not BSD sed, and the two differ in terms of the syntax for the -i flag. If you edit the Makefile and change sed -i to sed -i '' it should work.

[LiuTaowen-Tony]

Thank you for your help. It is indeed a sed version problem. However, I got something like this, could you please help me to look at it?

[WARNING] var was deprecated in version 2.1 of the opam CLI. Use opam var instead or set OPAMCLI environment variable to 2.0.
File "handwritten_support/riscv_extras.lem", line 11, character 26 to line 11, character 52
  Type error: type mismatch: application expression
    unit -> Sail2_instr_kinds.barrier_kind
  and
    Sail2_instr_kinds.barrier_kind