Fail to run 'make' for sail-riscv

[xiaomaaaaa]

I'm on sail -v = Sail 0.16 (sail @ opam-v2.1.5)
When trying to run 'make' for sail-riscv on Centos7 I get the following error:

Warning: Incomplete pattern match statement at model/riscv_insts_vext_fp.sail:722.77-82:
722 |                              let (fflags, elem) : (bits_fflags, bits('m)) = match 'm {
    |                                                                             ^---^
    | 
The following expression is unmatched: 64

Warning: Incomplete pattern match statement at model/riscv_insts_vext_fp.sail:731.77-82:
731 |                              let (fflags, elem) : (bits_fflags, bits('m)) = match 'm {
    |                                                                             ^---^
    | 
The following expression is unmatched: 64

Warning: Incomplete pattern match statement at model/riscv_insts_vext_red.sail:213.12-17:
213 |      sum = match funct6 {
    |            ^---^
    | 
The following expression is unmatched: FVV_VFWREDOSUM

echo "declare {isabelle} rename field sync_exception_ext = sync_exception_ext_exception" >> generated_definitions/lem/RV64/riscv_types.lem 
lem -isa -outdir generated_definitions/isabelle/RV64 -lib Sail=/home/mashixiong0318004377/.opam/5.1.0/share/sail/src/lem_interp -lib Sail=/home/mashixiong0318004377/.opam/5.1.0/share/sail/src/gen_lib \
	handwritten_support/0.11/riscv_extras.lem handwritten_support/0.11/mem_metadata.lem handwritten_support/0.11/riscv_extras_fdext.lem \
	generated_definitions/lem/RV64/riscv_types.lem \
	generated_definitions/lem/RV64/riscv.lem
File "generated_definitions/lem/RV64/riscv.lem", line 24483, character 7:
  Syntax error
make: *** [Makefile:330: generated_definitions/isabelle/RV64/Riscv.thy] Error 1

and the content of the ‘riscv.lem’ is as follows:

let riscv_f16Rsqrte7 rm v =
   let class = (fp_class v  : mword ty16) in      #line 24483
   let b__0 = class in
   if ((eq_vec b__0 (0x0001 : mword ty16))) then
     return ((nvFlag ()  : mword ty5), (0x7E00 : mword ty16))
   else if ((eq_vec b__0 (0x0002 : mword ty16))) then
     return ((nvFlag ()  : mword ty5), (0x7E00 : mword ty16))
   else if ((eq_vec b__0 (0x0004 : mword ty16))) then
     return ((nvFlag ()  : mword ty5), (0x7E00 : mword ty16))
   else if ((eq_vec b__0 (0x0100 : mword ty16))) then
     return ((nvFlag ()  : mword ty5), (0x7E00 : mword ty16))
   else if ((eq_vec b__0 (0x0200 : mword ty16))) then
     return ((zeros_implicit (5:ii)  : mword ty5), (0x7E00 : mword ty16))
   else if ((eq_vec b__0 (0x0008 : mword ty16))) then
     return ((dzFlag ()  : mword ty5), (0xFC00 : mword ty16))
   else if ((eq_vec b__0 (0x0010 : mword ty16))) then
     return ((dzFlag ()  : mword ty5), (0x7C00 : mword ty16))
   else if ((eq_vec b__0 (0x0080 : mword ty16))) then
     return ((zeros_implicit (5:ii)  : mword ty5), (0x0000 : mword ty16))
   else if ((eq_vec b__0 (0x0020 : mword ty16))) then
     (rsqrt7 v true  : M (mword ty64)) >>= fun (w__0 : mword ty64) ->
     return ((zeros_implicit (5:ii)  : mword ty5),
             (subrange_vec_dec w__0 (15:ii) (0:ii)  : mword ty16))
   else
     (rsqrt7 v false  : M (mword ty64)) >>= fun (w__1 : mword ty64) ->
     return ((zeros_implicit (5:ii)  : mword ty5),
                (subrange_vec_dec w__1 (15:ii) (0:ii)  : mword ty16))

Any advices would be very helpful for me.Thank you!

[Alasdair]

Can you do make csim or even just make check (maybe after doing make clean)?

I can't reproduce these issues with the Lem -> Isabelle path. I think in general just make is trying to build too much which isn't useful to most users. I'll see about making a PR to simplify what the Makefile is trying to do by default.

[xiaomaaaaa]

I can do make csim make osim make rvfi , but when I do make riscv_isa , The above problem arises。

[quswarabid]

@Alasdair I have tried doing make csim after doing make clean (reference for my issue #333)

I am still getting the same error:

quswarabid@quswarabid:~/RISCV/sail-riscv(master)$ make clean
[WARNING] var was deprecated in version 2.1 of the opam CLI. Use opam var instead or set OPAMCLI environment variable to 2.0.
[WARNING] var was deprecated in version 2.1 of the opam CLI. Use opam var instead or set OPAMCLI environment variable to 2.0.
[WARNING] var was deprecated in version 2.1 of the opam CLI. Use opam var instead or set OPAMCLI environment variable to 2.0.
rm -rf generated_definitions/ocaml/* generated_definitions/c/* generated_definitions/latex/*
[WARNING] var was deprecated in version 2.1 of the opam CLI. Use opam var instead or set OPAMCLI environment variable to 2.0.
rm -rf generated_definitions/lem/* generated_definitions/isabelle/* generated_definitions/hol4/* generated_definitions/coq/*
rm -rf generated_definitions/for-rmem/*
make -C c_emulator/SoftFloat-3e/build/Linux-RISCV-GCC clean
make[1]: Entering directory '/home/quswarabid/RISCV/sail-riscv/c_emulator/SoftFloat-3e/build/Linux-RISCV-GCC'
rm -f s_eq128.o s_le128.o s_lt128.o s_shortShiftLeft128.o s_shortShiftRight128.o s_shortShiftRightJam64.o s_shortShiftRightJam64Extra.o s_shortShiftRightJam128.o s_shortShiftRightJam128Extra.o s_shiftRightJam32.o s_shiftRightJam64.o s_shiftRightJam64Extra.o s_shiftRightJam128.o s_shiftRightJam128Extra.o s_shiftRightJam256M.o s_countLeadingZeros8.o s_countLeadingZeros16.o s_countLeadingZeros32.o s_countLeadingZeros64.o s_add128.o s_add256M.o s_sub128.o s_sub256M.o s_mul64ByShifted32To128.o s_mul64To128.o s_mul128By32.o s_mul128To256M.o s_approxRecip_1Ks.o s_approxRecip32_1.o s_approxRecipSqrt_1Ks.o s_approxRecipSqrt32_1.o  softfloat_raiseFlags.o s_propagateNaNF16UI.o s_f32UIToCommonNaN.o s_commonNaNToF32UI.o s_propagateNaNF32UI.o s_f64UIToCommonNaN.o s_commonNaNToF64UI.o s_propagateNaNF64UI.o s_propagateNaNF128UI.o s_roundToUI32.o s_roundToUI64.o s_roundToI32.o s_roundToI64.o s_normSubnormalF16Sig.o s_roundPackToF16.o s_normRoundPackToF16.o s_addMagsF16.o s_subMagsF16.o s_mulAddF16.o s_normSubnormalF32Sig.o s_roundPackToF32.o s_normRoundPackToF32.o s_addMagsF32.o s_subMagsF32.o s_mulAddF32.o s_normSubnormalF64Sig.o s_roundPackToF64.o s_normRoundPackToF64.o s_addMagsF64.o s_subMagsF64.o s_mulAddF64.o s_normSubnormalExtF80Sig.o s_roundPackToExtF80.o s_normRoundPackToExtF80.o s_addMagsExtF80.o s_subMagsExtF80.o s_normSubnormalF128Sig.o s_roundPackToF128.o s_normRoundPackToF128.o s_addMagsF128.o s_subMagsF128.o s_mulAddF128.o softfloat_state.o ui32_to_f16.o ui32_to_f32.o ui32_to_f64.o ui32_to_extF80.o ui32_to_extF80M.o ui32_to_f128.o ui32_to_f128M.o ui64_to_f16.o ui64_to_f32.o ui64_to_f64.o ui64_to_extF80.o ui64_to_extF80M.o ui64_to_f128.o ui64_to_f128M.o i32_to_f16.o i32_to_f32.o i32_to_f64.o i32_to_extF80.o i32_to_extF80M.o i32_to_f128.o i32_to_f128M.o i64_to_f16.o i64_to_f32.o i64_to_f64.o i64_to_extF80.o i64_to_extF80M.o i64_to_f128.o i64_to_f128M.o f16_to_ui32.o f16_to_ui64.o f16_to_i32.o f16_to_i64.o f16_to_ui32_r_minMag.o f16_to_ui64_r_minMag.o f16_to_i32_r_minMag.o f16_to_i64_r_minMag.o f16_to_f32.o f16_to_f64.o f16_to_extF80.o f16_to_extF80M.o f16_to_f128.o f16_to_f128M.o f16_roundToInt.o f16_add.o f16_sub.o f16_mul.o f16_mulAdd.o f16_div.o f16_rem.o f16_sqrt.o f16_eq.o f16_le.o f16_lt.o f16_eq_signaling.o f16_le_quiet.o f16_lt_quiet.o f16_isSignalingNaN.o f32_to_ui32.o f32_to_ui64.o f32_to_i32.o f32_to_i64.o f32_to_ui32_r_minMag.o f32_to_ui64_r_minMag.o f32_to_i32_r_minMag.o f32_to_i64_r_minMag.o f32_to_f16.o f32_to_f64.o f32_to_extF80.o f32_to_extF80M.o f32_to_f128.o f32_to_f128M.o f32_roundToInt.o f32_add.o f32_sub.o f32_mul.o f32_mulAdd.o f32_div.o f32_rem.o f32_sqrt.o f32_eq.o f32_le.o f32_lt.o f32_eq_signaling.o f32_le_quiet.o f32_lt_quiet.o f32_isSignalingNaN.o f64_to_ui32.o f64_to_ui64.o f64_to_i32.o f64_to_i64.o f64_to_ui32_r_minMag.o f64_to_ui64_r_minMag.o f64_to_i32_r_minMag.o f64_to_i64_r_minMag.o f64_to_f16.o f64_to_f32.o f64_to_extF80.o f64_to_extF80M.o f64_to_f128.o f64_to_f128M.o f64_roundToInt.o f64_add.o f64_sub.o f64_mul.o f64_mulAdd.o f64_div.o f64_rem.o f64_sqrt.o f64_eq.o f64_le.o f64_lt.o f64_eq_signaling.o f64_le_quiet.o f64_lt_quiet.o f64_isSignalingNaN.o extF80_to_ui32.o extF80_to_ui64.o extF80_to_i32.o extF80_to_i64.o extF80_to_ui32_r_minMag.o extF80_to_ui64_r_minMag.o extF80_to_i32_r_minMag.o extF80_to_i64_r_minMag.o extF80_to_f16.o extF80_to_f32.o extF80_to_f64.o extF80_to_f128.o extF80_roundToInt.o extF80_add.o extF80_sub.o extF80_mul.o extF80_div.o extF80_rem.o extF80_sqrt.o extF80_eq.o extF80_le.o extF80_lt.o extF80_eq_signaling.o extF80_le_quiet.o extF80_lt_quiet.o extF80_isSignalingNaN.o extF80M_to_ui32.o extF80M_to_ui64.o extF80M_to_i32.o extF80M_to_i64.o extF80M_to_ui32_r_minMag.o extF80M_to_ui64_r_minMag.o extF80M_to_i32_r_minMag.o extF80M_to_i64_r_minMag.o extF80M_to_f16.o extF80M_to_f32.o extF80M_to_f64.o extF80M_to_f128M.o extF80M_roundToInt.o extF80M_add.o extF80M_sub.o extF80M_mul.o extF80M_div.o extF80M_rem.o extF80M_sqrt.o extF80M_eq.o extF80M_le.o extF80M_lt.o extF80M_eq_signaling.o extF80M_le_quiet.o extF80M_lt_quiet.o f128_to_ui32.o f128_to_ui64.o f128_to_i32.o f128_to_i64.o f128_to_ui32_r_minMag.o f128_to_ui64_r_minMag.o f128_to_i32_r_minMag.o f128_to_i64_r_minMag.o f128_to_f16.o f128_to_f32.o f128_to_extF80.o f128_to_f64.o f128_roundToInt.o f128_add.o f128_sub.o f128_mul.o f128_mulAdd.o f128_div.o f128_rem.o f128_sqrt.o f128_eq.o f128_le.o f128_lt.o f128_eq_signaling.o f128_le_quiet.o f128_lt_quiet.o f128_isSignalingNaN.o f128M_to_ui32.o f128M_to_ui64.o f128M_to_i32.o f128M_to_i64.o f128M_to_ui32_r_minMag.o f128M_to_ui64_r_minMag.o f128M_to_i32_r_minMag.o f128M_to_i64_r_minMag.o f128M_to_f16.o f128M_to_f32.o f128M_to_extF80M.o f128M_to_f64.o f128M_roundToInt.o f128M_add.o f128M_sub.o f128M_mul.o f128M_mulAdd.o f128M_div.o f128M_rem.o f128M_sqrt.o f128M_eq.o f128M_le.o f128M_lt.o f128M_eq_signaling.o f128M_le_quiet.o f128M_lt_quiet.o  softfloat.a
make[1]: Leaving directory '/home/quswarabid/RISCV/sail-riscv/c_emulator/SoftFloat-3e/build/Linux-RISCV-GCC'
rm -f c_emulator/riscv_sim_RV32 c_emulator/riscv_sim_RV64  c_emulator/riscv_rvfi_RV32 c_emulator/riscv_rvfi_RV64
rm -rf ocaml_emulator/_sbuild ocaml_emulator/_build ocaml_emulator/riscv_ocaml_sim_RV32 ocaml_emulator/riscv_ocaml_sim_RV64 ocaml_emulator/tracecmp
rm -f *.gcno *.gcda
rm -f z3_problems
Holmake cleanAll
make: Holmake: No such file or directory
make: [Makefile:485: clean] Error 127 (ignored)
rm -f handwritten_support/riscv_extras.vo handwritten_support/riscv_extras.vos handwritten_support/riscv_extras.vok handwritten_support/riscv_extras.glob handwritten_support/.riscv_extras.aux
rm -f handwritten_support/mem_metadata.vo handwritten_support/mem_metadata.vos handwritten_support/mem_metadata.vok handwritten_support/mem_metadata.glob handwritten_support/.mem_metadata.aux
rm -f sail_doc/riscv_RV32.json
rm -f sail_doc/riscv_RV64.json
ocamlbuild -clean
Finished, 0 targets (0 cached) in 00:00:00.
00:00:00 0    (0   ) STARTING                                                                                                                                                                           -------- |quswarabid@quswarabid:~/RISCV/sail-riscv(master)$ make csim 
[WARNING] var was deprecated in version 2.1 of the opam CLI. Use opam var instead or set OPAMCLI environment variable to 2.0.
[WARNING] var was deprecated in version 2.1 of the opam CLI. Use opam var instead or set OPAMCLI environment variable to 2.0.
[WARNING] var was deprecated in version 2.1 of the opam CLI. Use opam var instead or set OPAMCLI environment variable to 2.0.
mkdir -p generated_definitions/c
[WARNING] var was deprecated in version 2.1 of the opam CLI. Use opam var instead or set OPAMCLI environment variable to 2.0.
sail -dno_cast -O -Oconstant_fold -memo_z3 -c -c_include riscv_prelude.h -c_include riscv_platform.h -c_no_main model/prelude.sail model/prelude_mapping.sail model/riscv_xlen64.sail model/riscv_flen_D.sail model/riscv_vlen.sail model/prelude_mem_metadata.sail model/prelude_mem.sail model/riscv_types_common.sail model/riscv_types_ext.sail model/riscv_types.sail model/riscv_vmem_types.sail model/riscv_reg_type.sail model/riscv_freg_type.sail model/riscv_regs.sail model/riscv_pc_access.sail model/riscv_sys_regs.sail model/riscv_pmp_regs.sail model/riscv_pmp_control.sail model/riscv_ext_regs.sail model/riscv_addr_checks_common.sail model/riscv_addr_checks.sail model/riscv_misa_ext.sail model/riscv_vreg_type.sail model/riscv_vext_regs.sail model/riscv_csr_map.sail model/riscv_vext_control.sail model/riscv_next_regs.sail model/riscv_sys_exceptions.sail model/riscv_sync_exception.sail model/riscv_next_control.sail model/riscv_softfloat_interface.sail model/riscv_fdext_regs.sail model/riscv_fdext_control.sail model/riscv_csr_ext.sail model/riscv_sys_control.sail model/riscv_platform.sail model/riscv_mem.sail model/riscv_pte.sail model/riscv_ptw.sail model/riscv_vmem_common.sail model/riscv_vmem_tlb.sail model/riscv_vmem_sv39.sail model/riscv_vmem_sv48.sail model/riscv_vmem_rv64.sail model/riscv_types_kext.sail model/riscv_insts_begin.sail model/riscv_insts_base.sail model/riscv_insts_aext.sail model/riscv_insts_cext.sail model/riscv_insts_mext.sail model/riscv_insts_zicsr.sail model/riscv_insts_next.sail model/riscv_insts_hints.sail model/riscv_insts_fext.sail model/riscv_insts_cfext.sail model/riscv_insts_dext.sail model/riscv_insts_cdext.sail model/riscv_insts_zba.sail model/riscv_insts_zbb.sail model/riscv_insts_zbc.sail model/riscv_insts_zbs.sail model/riscv_insts_zfh.sail model/riscv_insts_zfa.sail model/riscv_insts_zkn.sail model/riscv_insts_zks.sail model/riscv_insts_zbkb.sail model/riscv_insts_zbkx.sail model/riscv_insts_zicond.sail model/riscv_insts_vext_utils.sail model/riscv_insts_vext_vset.sail model/riscv_insts_vext_arith.sail model/riscv_insts_vext_fp.sail model/riscv_insts_vext_mem.sail model/riscv_insts_vext_mask.sail model/riscv_insts_vext_vm.sail model/riscv_insts_vext_red.sail model/riscv_jalr_seq.sail model/riscv_insts_end.sail model/riscv_step_common.sail model/riscv_step_ext.sail model/riscv_decode_ext.sail model/riscv_fetch.sail model/riscv_step.sail model/riscv_analysis.sail model/main.sail -o generated_definitions/c/riscv_model_RV64
Warning: Deprecated model/prelude.sail:80.22-43:
80 |val string_startswith = "string_startswith" : (string, string) -> bool
   |                      ^-------------------^
   | 
All external bindings should be marked as either monadic or pure

Warning: Deprecated model/riscv_vlen.sail:41.36-49:
41 |val get_elen_pow : unit -> {|5, 6|} effect {rreg}
   |                                    ^-----------^
   | 
Explicit effect annotations are deprecated. They are no longer used and can be removed.

Warning: Duplicate function type definition for spc_forwards
model/prelude.sail:306.4-16:
306 |val spc_forwards : unit -> string
    |    ^----------^
    | This duplicate definition is being ignored!
Warning: Incomplete pattern match statement at model/riscv_sys_regs.sail:918.2-7:
918 |  match get_sew_pow() {
    |  ^---^
    | 
The following expression is unmatched: 0

Warning: Incomplete pattern match statement at model/riscv_sys_regs.sail:928.2-7:
928 |  match get_sew_pow() {
    |  ^---^
    | 
The following expression is unmatched: 0

Warning: Incomplete pattern match statement at model/riscv_types_kext.sail:240.2-7:
240 |  match (x, table) {
    |  ^---^
    | 
The following expression is unmatched: (undefined, [||])

Warning: Incomplete pattern match statement at model/riscv_insts_vext_fp.sail:420.77-82:
420 |                              let (fflags, elem) : (bits_fflags, bits('m)) = match 'm {
    |                                                                             ^---^
    | 
The following expression is unmatched: 8

Warning: Incomplete pattern match statement at model/riscv_insts_vext_fp.sail:429.77-82:
429 |                              let (fflags, elem) : (bits_fflags, bits('m)) = match 'm {
    |                                                                             ^---^
    | 
The following expression is unmatched: 8

Warning: Incomplete pattern match statement at model/riscv_insts_vext_fp.sail:438.77-82:
438 |                              let (fflags, elem) : (bits_fflags, bits('m)) = match 'm {
    |                                                                             ^---^
    | 
The following expression is unmatched: 8

Warning: Incomplete pattern match statement at model/riscv_insts_vext_fp.sail:447.77-82:
447 |                              let (fflags, elem) : (bits_fflags, bits('m)) = match 'm {
    |                                                                             ^---^
    | 
The following expression is unmatched: 8

Warning: Incomplete pattern match statement at model/riscv_insts_vext_fp.sail:456.77-82:
456 |                              let (fflags, elem) : (bits_fflags, bits('m)) = match 'm {
    |                                                                             ^---^
    | 
The following expression is unmatched: 8

Warning: Incomplete pattern match statement at model/riscv_insts_vext_fp.sail:465.77-82:
465 |                              let (fflags, elem) : (bits_fflags, bits('m)) = match 'm {
    |                                                                             ^---^
    | 
The following expression is unmatched: 8

Warning: Incomplete pattern match statement at model/riscv_insts_vext_fp.sail:668.77-82:
668 |                              let (fflags, elem) : (bits_fflags, bits('m)) = match 'm {
    |                                                                             ^---^
    | 
The following expression is unmatched: 64

Warning: Incomplete pattern match statement at model/riscv_insts_vext_fp.sail:677.77-82:
677 |                              let (fflags, elem) : (bits_fflags, bits('m)) = match 'm {
    |                                                                             ^---^
    | 
The following expression is unmatched: 64

Warning: Incomplete pattern match statement at model/riscv_insts_vext_fp.sail:686.77-82:
686 |                              let (fflags, elem) : (bits_fflags, bits('m)) = match 'm {
    |                                                                             ^---^
    | 
The following expression is unmatched: 64

Warning: Incomplete pattern match statement at model/riscv_insts_vext_fp.sail:695.77-82:
695 |                              let (fflags, elem) : (bits_fflags, bits('m)) = match 'm {
    |                                                                             ^---^
    | 
The following expression is unmatched: 64

Warning: Incomplete pattern match statement at model/riscv_insts_vext_fp.sail:704.77-82:
704 |                              let (fflags, elem) : (bits_fflags, bits('m)) = match 'm {
    |                                                                             ^---^
    | 
The following expression is unmatched: 64

Warning: Incomplete pattern match statement at model/riscv_insts_vext_fp.sail:713.77-82:
713 |                              let (fflags, elem) : (bits_fflags, bits('m)) = match 'm {
    |                                                                             ^---^
    | 
The following expression is unmatched: 64

Warning: Incomplete pattern match statement at model/riscv_insts_vext_fp.sail:722.77-82:
722 |                              let (fflags, elem) : (bits_fflags, bits('m)) = match 'm {
    |                                                                             ^---^
    | 
The following expression is unmatched: 64

Warning: Incomplete pattern match statement at model/riscv_insts_vext_fp.sail:731.77-82:
731 |                              let (fflags, elem) : (bits_fflags, bits('m)) = match 'm {
    |                                                                             ^---^
    | 
The following expression is unmatched: 64

Warning: Incomplete pattern match statement at model/riscv_insts_vext_red.sail:213.12-17:
213 |      sum = match funct6 {
    |            ^---^
    | 
The following expression is unmatched: FVV_VFWREDOSUM

make: *** [Makefile:257: generated_definitions/c/riscv_model_RV64.c] Killed
make: *** Deleting file 'generated_definitions/c/riscv_model_RV64.c'
quswarabid@quswarabid:~/RISCV/sail-riscv(master)$ 

[ingmarfjolla]

adding to this one since my issue was a duplicate of this, changing the sail-riscv commit to the one mentioned in issue: #333 532714a ended up fixing the issue.

I tested on both ocaml version 4.13.1 (which I think the CI here uses) and ocaml 5.1.0 with sail version 0.17.1 and the make file ran. I also tested with the ocaml/opam:latest image that this repos dockerfile uses and the ubuntu:latest image and it works on that commit for now.

[Alasdair]

Should be fixed by #353

The very large bitvectors in the vector extension cause issues for the mapping into Isabelle and HOL4 machine word libraries, so while that commit fixes the build it might make the generated theorem prover definitions less useful in the short term until we can fix the underlying issues.