riscv64.toml and riscv64_ubuntu.toml configs

[westtide]

Hi,
I’m using Isla on Ubuntu 20.04 LTS with gcc-riscv64-unknown-elf for RISC-V, and I cloned the isla-snapshots repository for the latest snapshots. However, I’ve encountered the following issues:
I tried

target/release/isla-footprint -A isla-snapshots/riscv64.ir -C configs/riscv64.toml --partial -i '0000000 00001 00010 000 00011 0110011' -s  

which corresponds to the RISC-V instruction add x3, x1, x2, received the following error:

configs/riscv64.toml: sail_barrier is not a known event name for in_program_order in configuration

The error seems related to the in_program_order = ["sail_barrier"] line in the configs/riscv64.toml.

Besieds, I tried running the same command with the riscv64_ubuntu.toml, following:

 target/release/isla-footprint -A isla-snapshots/riscv64.ir -C configs/riscv64_ubuntu.toml --partial -i '0000000 00001 00010 000 00011 0110011' -s  

This resulted in the error:

configs/riscv64_ubuntu.toml: Toolchain option nm must be specified

Therefore, I add nm = "riscv64-unknown-elf-nm" to configs/riscv64_ubuntu.toml, and it succeed finally, with an smt-lib2 formula

Warning: Could not find register rv_enable_pmp when parsing registers.defaults in configuration
No primop platform_write_mem_ea (Name { id: 2020 })
No primop plat_get_16_random_bits (Name { id: 2657 })
No primop softfloat_f16add (Name { id: 2914 })
No primop softfloat_f16sub (Name { id: 2922 })
No primop softfloat_f16mul (Name { id: 2924 })
No primop softfloat_f16div (Name { id: 2926 })
No primop softfloat_f32add (Name { id: 2928 })
No primop softfloat_f32sub (Name { id: 2933 })
No primop softfloat_f32mul (Name { id: 2935 })
No primop softfloat_f32div (Name { id: 2937 })
No primop softfloat_f64add (Name { id: 2939 })
No primop softfloat_f64sub (Name { id: 2944 })
No primop softfloat_f64mul (Name { id: 2946 })
No primop softfloat_f64div (Name { id: 2948 })
No primop softfloat_f16muladd (Name { id: 2950 })
No primop softfloat_f32muladd (Name { id: 2953 })
No primop softfloat_f64muladd (Name { id: 2955 })
No primop softfloat_f16sqrt (Name { id: 2957 })
No primop softfloat_f32sqrt (Name { id: 2959 })
No primop softfloat_f64sqrt (Name { id: 2961 })
No primop softfloat_f16toi32 (Name { id: 2963 })
No primop softfloat_f16toui32 (Name { id: 2965 })
No primop softfloat_i32tof16 (Name { id: 2967 })
No primop softfloat_ui32tof16 (Name { id: 2969 })
No primop softfloat_f16toi64 (Name { id: 2971 })
No primop softfloat_f16toui64 (Name { id: 2973 })
No primop softfloat_i64tof16 (Name { id: 2975 })
No primop softfloat_ui64tof16 (Name { id: 2977 })
No primop softfloat_f32toi32 (Name { id: 2979 })
No primop softfloat_f32toui32 (Name { id: 2981 })
No primop softfloat_i32tof32 (Name { id: 2983 })
No primop softfloat_ui32tof32 (Name { id: 2985 })
No primop softfloat_f32toi64 (Name { id: 2987 })
No primop softfloat_f32toui64 (Name { id: 2989 })
No primop softfloat_i64tof32 (Name { id: 2991 })
No primop softfloat_ui64tof32 (Name { id: 2993 })
No primop softfloat_f64toi32 (Name { id: 2995 })
No primop softfloat_f64toui32 (Name { id: 2997 })
No primop softfloat_i32tof64 (Name { id: 2999 })
No primop softfloat_ui32tof64 (Name { id: 3001 })
No primop softfloat_f64toi64 (Name { id: 3003 })
No primop softfloat_f64toui64 (Name { id: 3005 })
No primop softfloat_i64tof64 (Name { id: 3007 })
No primop softfloat_ui64tof64 (Name { id: 3009 })
No primop softfloat_f16tof32 (Name { id: 3011 })
No primop softfloat_f16tof64 (Name { id: 3013 })
No primop softfloat_f32tof64 (Name { id: 3015 })
No primop softfloat_f32tof16 (Name { id: 3017 })
No primop softfloat_f64tof16 (Name { id: 3019 })
No primop softfloat_f64tof32 (Name { id: 3021 })
No primop softfloat_f16lt (Name { id: 3023 })
No primop softfloat_f16lt_quiet (Name { id: 3028 })
No primop softfloat_f16le (Name { id: 3030 })
No primop softfloat_f16le_quiet (Name { id: 3032 })
No primop softfloat_f16eq (Name { id: 3034 })
No primop softfloat_f32lt (Name { id: 3036 })
No primop softfloat_f32lt_quiet (Name { id: 3038 })
No primop softfloat_f32le (Name { id: 3040 })
No primop softfloat_f32le_quiet (Name { id: 3042 })
No primop softfloat_f32eq (Name { id: 3044 })
No primop softfloat_f64lt (Name { id: 3046 })
No primop softfloat_f64lt_quiet (Name { id: 3048 })
No primop softfloat_f64le (Name { id: 3050 })
No primop softfloat_f64le_quiet (Name { id: 3052 })
No primop softfloat_f64eq (Name { id: 3054 })
No primop softfloat_f16roundToInt (Name { id: 3056 })
No primop softfloat_f32roundToInt (Name { id: 3059 })
No primop softfloat_f64roundToInt (Name { id: 3061 })
(segments)
(trace
  (assume-reg |rv_enable_writable_misa| nil true)
  (assume-reg |rv_enable_rvc| nil true)
  (assume-reg |rv_enable_fdext| nil false)
  (assume-reg |rv_enable_zfinx| nil false)
  (assume-reg |rv_enable_next| nil false)
  (assume-reg |rv_enable_zcb| nil false)
  (assume-reg |rv_enable_writable_fiom| nil false)
  (assume-reg |rv_pmp_count| nil (_ bv0 64))
  (assume-reg |rv_pmp_grain| nil (_ bv0 64))
  (assume-reg |rv_enable_vext| nil false)
  (assume-reg |rv_enable_dirty_update| nil false)
  (assume-reg |rv_enable_misaligned_access| nil false)
  (assume-reg |rv_mtval_has_illegal_inst_bits| nil false)
  (assume-reg |rv_ram_base| nil #x0000000080000000)
  (assume-reg |rv_ram_size| nil #x0000000004000000)
  (assume-reg |rv_rom_base| nil #x0000000000001000)
  (assume-reg |rv_rom_size| nil #x0000000000000100)
  (assume-reg |rv_clint_base| nil #x0000000002000000)
  (assume-reg |rv_clint_size| nil #x00000000000c0000)
  (assume-reg |rv_htif_tohost| nil #x0000000080001000)
  (assume-reg |rv_insns_per_tick| nil (_ bv10 128))
  (assume-reg |tlb| nil (|None| (_ unit)))
  (define-enum |Privilege| 3 (|User| |Supervisor| |Machine|)) ; 0:0 - 0:0
  (define-enum |Architecture| 3 (|RV32| |RV64| |RV128|)) ; 0:0 - 0:0
  (define-enum |PmpAddrMatchType| 4 (|OFF| |TOR| |NA4| |NAPOT|)) ; 0:0 - 0:0
  (cycle)
  (declare-const v244 (_ BitVec 64)) ; model/main.sail 47:15 - 47:21
  (read-reg |PC| nil v244)
  (define-const v245 (bvadd v244 #x0000000000000004)) ; 0:0 - 0:0
  (write-reg |nextPC| nil v245)
  (define-enum |rop| 10 (|RISCV_ADD| |RISCV_SUB| |RISCV_SLL| |RISCV_SLT| |RISCV_SLTU| |RISCV_XOR| |RISCV_SRL| |RISCV_SRA| |RISCV_OR| |RISCV_AND|)) ; 0:0 - 0:0
  (declare-const v257 (_ BitVec 64)) ; model/riscv_regs.sail 57:11 - 57:13
  (read-reg |x2| nil v257)
  (declare-const v258 (_ BitVec 64)) ; model/riscv_regs.sail 56:11 - 56:13
  (read-reg |x1| nil v258)
  (define-const v259 (bvadd v257 v258)) ; model/riscv_insts_base.sail 259:18 - 259:35
  (write-reg |x3| nil v259)
  (define-enum |Retired| 2 (|RETIRE_SUCCESS| |RETIRE_FAIL|)) ; 0:0 - 0:0
  (read-reg |nextPC| nil v245)
  (write-reg |PC| nil v245))

However, I noticed multiple warnings such as:

No primop softfloat_f16le_quiet (Name { id: 3032 })

I am not sure if they suggest a missing configuration for primitive operations, while these do not cause errors.

I am still familiarizing myself with the project and experimenting with modifying the config files to improve these outputs. Could you please confirm if my changes so far are appropriate? Thanks!

[bacam]

Those seem reasonable to me. The riscv64.toml file corresponds to a more recent version of the model than the one in snapshots (if you want to try an up-to-the-minute version you could try the Makefile addition for the riscv repository in #82), and I think the ubuntu one is older. You don't need to worry about the softfloat warnings - they're just observing that Isla doesn't have functions for floating point operations.