avanhatt / wasmtime

Standalone JIT-style runtime for WebAssembly, using Cranelift
https://wasmtime.dev/
Apache License 2.0
0 stars 1 forks source link

veri: verify some x64 amode rules #76

Closed mmcloughlin closed 11 months ago

mmcloughlin commented 11 months ago

Adds specs to verify some of the Amode ISLE rules.

Tests:

mbm@m1p ~/D/v/v/c/i/v/veri_engine (mbm/x64-veri-amode-init)> cargo test -- named_x64_
...

running 13 tests
test test_named_x64_amode_imm_reg_base ... ok
test test_named_x64_to_amode_add_base_case ... ok
test test_named_x64_amode_imm_reg_reg_shift_no_shift ... ok
test test_named_x64_iadd_base_case_32_or_64_lea ... ok
test test_named_x64_amode_imm_reg_iadd ... ok
test test_named_x64_to_amode_add_const_rhs ... ok
test test_named_x64_to_amode_add_const_lhs ... ok
test test_named_x64_amode_imm_reg_reg_shift_shl_rhs ... ok
test test_named_x64_amode_imm_reg_reg_shift_shl_lhs ... ok
test test_named_x64_to_amode_add_const_fold_iadd_rhs_lhs ... ok
test test_named_x64_to_amode_add_const_fold_iadd_lhs_lhs ... ok
test test_named_x64_to_amode_add_const_fold_iadd_lhs_rhs ... ok
test test_named_x64_to_amode_add_const_fold_iadd_rhs_rhs ... ok

test result: ok. 13 passed; 0 failed; 0 ignored; 0 measured; 169 filtered out; finished in 8.23s

   Doc-tests veri_engine_lib

running 0 tests

test result: ok. 0 passed; 0 failed; 0 ignored; 0 measured; 0 filtered out; finished in 0.00s