search

rems-project / isla

Symbolic execution tool for Sail ISA specifications
Other
62 stars 10 forks source link

riscv64.toml and riscv64_ubuntu.toml configs #83

Open westtide opened 1 month ago

westtide commented 1 month ago

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 commented 4 weeks ago

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.