rems-project / sail

Sail architecture definition language
Other
624 stars 116 forks source link

Sail dislikes the arm-v8.5-a spec ("pow2 cannot be defined as an overload, as it is already bound") #735

Open Trolldemorted opened 1 month ago

Trolldemorted commented 1 month ago

I tried to use the armv8 spec, but unfortunately sail complains:

root@3e8154d285c6:/input/arm-v8.5-a# make
[WARNING] Running as root is not recommended
Makefile:7: SAIL_DIR is /root/.opam/4.10.0/share/sail
sail -just_check -verbose 1 -non_lexical_flow -no_lexp_bounds_check -memo_z3 -no_warn -dno_cast  model/prelude.sail model/no_devices.sail model/aarch_types.sail model/aarch_mem.sail model/aarch64.sail model/aarch64_float.sail model/aarch64_vector.sail model/aarch32.sail model/aarch_decode.sail model/elfmain.sail
Type check [==================================================] 100% (12/12)
Type error:[=============================================     ] 91% (212/231)
/root/.opam/4.10.0/share/sail/lib/arith.sail:103.4-8:
103 |val pow2 = pure "pow2" : forall 'n. int('n) -> int(2 ^ 'n)
    |    ^--^ Previous binding
model/prelude.sail:412.0-37:
412 |overload pow2 = {pow2_atom, pow2_int}
    |^-----------------------------------^
    | pow2 cannot be defined as an overload, as it is already bound
make: *** [Makefile:21: check] Error 1

Steps to reproduce:

Am I doing something wrong?