Skip to content

Commit

Permalink
More RISC-V store tests using the zero register, fix to SB
Browse files Browse the repository at this point in the history
  • Loading branch information
@didriklundberg
didriklundberg committed Sep 19, 2024
1 parent 1affe48 commit 441c8fc
Show file tree
Hide file tree
Showing 3 changed files with 119 additions and 1 deletion.
51 changes: 51 additions & 0 deletions src/theory/tools/lifter/bir_riscv_extrasScript.sml
View file
Original file line number Diff line number Diff line change
Expand Up @@ -478,6 +478,28 @@ subgoal `((w2w vr):word8) = (7 >< 0) vr` >- (
FULL_SIMP_TAC std_ss []
QED

Theorem riscv_is_lifted_mem_exp_STORE_ENDIAN_BYTE_8LSB_alt:
(!env em ea va er vr mem_f.
bir_is_lifted_mem_exp env em mem_f ==>
bir_is_lifted_imm_exp env ea (Imm64 va) ==>
bir_is_lifted_imm_exp env er (Imm8 vr) ==>
bir_is_lifted_mem_exp env (BExp_Store em ea BEnd_LittleEndian er)
mem_f(| va |-> vr |))
Proof
SIMP_TAC (std_ss++holBACore_ss++wordsLib.WORD_ss) [bir_is_lifted_imm_exp_def,
bir_is_lifted_mem_exp_def, PULL_EXISTS,
bir_env_oldTheory.bir_env_vars_are_initialised_UNION, bir_eval_store_BASIC_REWR] >>
rpt strip_tac >>
`sa = Bit64` by metis_tac[size_of_bir_immtype_INJ, size_of_bir_immtype_def] >>
`sb = Bit8` by metis_tac[size_of_bir_immtype_INJ, size_of_bir_immtype_def] >>
gs[bir_store_in_mem_def] >>
FULL_SIMP_TAC (std_ss++holBACore_ss) [bir_load_mmap_w_bir_mmap_n2w_thm, FUN_EQ_THM] >>
subgoal `size_of_bir_immtype Bit64 = dimindex (:64)` >- (
FULL_SIMP_TAC (std_ss++holBACore_ss) [dimindex_64]
) >>
gs[bir_update_mmap_words_INTRO_w2n, bitstring_split_SINGLE, bir_update_mmap_words_def]
QED

Theorem riscv_is_lifted_mem_exp_STORE_ENDIAN_BYTE_16LSB:
(!env em ea va er vr mem_f.
bir_is_lifted_mem_exp env em mem_f ==>
Expand Down Expand Up @@ -568,6 +590,18 @@ Q.SUBGOAL_THEN `(7 >< 0) (vv:word64) = ((w2w vv):word8)` (fn thm => FULL_SIMP_TA
FULL_SIMP_TAC std_ss [mem_store_byte_def]
QED

Theorem riscv_LIFT_STORE_BYTE_alt:
!env em ea va ev vv ms mem_f.
bir_is_lifted_mem_exp env em mem_f ==>
bir_is_lifted_imm_exp env ea (Imm64 va) ==>
bir_is_lifted_imm_exp env ev (Imm8 vv) ==>
bir_is_lifted_mem_exp env (BExp_Store em ea BEnd_LittleEndian ev)
(mem_store_byte va vv mem_f)
Proof
SIMP_TAC std_ss [mem_store_byte_def, elim_zero_for_def_thm,
riscv_is_lifted_mem_exp_STORE_ENDIAN_BYTE_8LSB_alt]
QED

Theorem riscv_LIFT_STORE_DWORD_CHANGE_INTERVAL:
!va vv mem_f.
FUNS_EQ_OUTSIDE_WI_size va 8 (riscv_mem_store_dword va vv mem_f)
Expand Down Expand Up @@ -658,6 +692,21 @@ SIMP_TAC (std_ss++holBACore_ss) [bir_is_lifted_imm_exp_def,
blastLib.BBLAST_TAC
QED

(*************************************************)
(* 8 LSBs (8-bit) - for SB *)
(*************************************************)

Theorem riscv_is_lifted_imm_exp_8LSBs[local]:
!env w e.
bir_is_lifted_imm_exp env e (Imm64 w) ==>
bir_is_lifted_imm_exp env (BExp_Cast BIExp_LowCast e Bit8)
(Imm8 ((7 >< 0) w))
Proof
SIMP_TAC (std_ss++holBACore_ss++wordsLib.WORD_ss) [bir_is_lifted_imm_exp_def,
bir_env_oldTheory.bir_env_vars_are_initialised_UNION] >>
blastLib.BBLAST_TAC
QED

(********************************************************************)
(* 32 LSBs - for 32-bit instructions (ending in "W") of RV64I *)
(********************************************************************)
Expand Down Expand Up @@ -800,12 +849,14 @@ Theorem riscv_extra_LIFTS = LIST_CONJ [
riscv_LIFT_LOAD_HALF,
riscv_LIFT_LOAD_BYTE,
riscv_LIFT_STORE_BYTE,
riscv_LIFT_STORE_BYTE_alt,
riscv_LIFT_STORE_HALF,
riscv_LIFT_STORE_WORD,
riscv_LIFT_STORE_DWORD,
riscv_is_lifted_imm_exp_BIN_PRED,
riscv_is_lifted_imm_exp_6LSBs,
riscv_is_lifted_imm_exp_5LSBs,
riscv_is_lifted_imm_exp_8LSBs,
riscv_is_lifted_imm_exp_32LSBsLC,
riscv_is_lifted_imm_exp_64MSBs,
riscv_is_lifted_imm_exp_GE,
Expand Down
60 changes: 59 additions & 1 deletion src/tools/lifter/selftest_riscv.log
View file
Original file line number Diff line number Diff line change
Expand Up @@ -330,6 +330,26 @@ SW x14, 8(x2): 00E12423 @ 0x10030 - OK
bb_last_statement :=
BStmt_Jmp (BLE_Label (BL_Address (Imm64 0x10034w)))|>])

SD x0, 0(x7): 0003B023 @ 0x10030 - OK
[]
|- bir_is_lifted_inst_prog riscv_bmr (Imm64 0x10030w) (WI_end 0w 0x1000000w)
(0x10030w,[35w; 176w; 3w; 0w])
(BirProgram
[<|bb_label := BL_Address_HC (Imm64 0x10030w) "0003B023";
bb_statements :=
[BStmt_Assert
(BExp_Aligned Bit64 3
(BExp_Den (BVar "x7" (BType_Imm Bit64))));
BStmt_Assert
(BExp_unchanged_mem_interval_distinct Bit64 0 16777216
(BExp_Den (BVar "x7" (BType_Imm Bit64))) 8);
BStmt_Assign (BVar "MEM8" (BType_Mem Bit64 Bit8))
(BExp_Store (BExp_Den (BVar "MEM8" (BType_Mem Bit64 Bit8)))
(BExp_Den (BVar "x7" (BType_Imm Bit64))) BEnd_LittleEndian
(BExp_Const (Imm64 0w)))];
bb_last_statement :=
BStmt_Jmp (BLE_Label (BL_Address (Imm64 0x10034w)))|>])

SW x0, 0(x7): 0003A023 @ 0x10030 - OK
[]
|- bir_is_lifted_inst_prog riscv_bmr (Imm64 0x10030w) (WI_end 0w 0x1000000w)
Expand All @@ -350,6 +370,44 @@ SW x0, 0(x7): 0003A023 @ 0x10030 - OK
bb_last_statement :=
BStmt_Jmp (BLE_Label (BL_Address (Imm64 0x10034w)))|>])

SH x0, 0(x15): 00079023 @ 0x10030 - OK
[]
|- bir_is_lifted_inst_prog riscv_bmr (Imm64 0x10030w) (WI_end 0w 0x1000000w)
(0x10030w,[35w; 144w; 7w; 0w])
(BirProgram
[<|bb_label := BL_Address_HC (Imm64 0x10030w) "00079023";
bb_statements :=
[BStmt_Assert
(BExp_Aligned Bit64 1
(BExp_Den (BVar "x15" (BType_Imm Bit64))));
BStmt_Assert
(BExp_unchanged_mem_interval_distinct Bit64 0 16777216
(BExp_Den (BVar "x15" (BType_Imm Bit64))) 2);
BStmt_Assign (BVar "MEM8" (BType_Mem Bit64 Bit8))
(BExp_Store (BExp_Den (BVar "MEM8" (BType_Mem Bit64 Bit8)))
(BExp_Den (BVar "x15" (BType_Imm Bit64)))
BEnd_LittleEndian
(BExp_Cast BIExp_LowCast (BExp_Const (Imm64 0w)) Bit16))];
bb_last_statement :=
BStmt_Jmp (BLE_Label (BL_Address (Imm64 0x10034w)))|>])

SB x0, 0(x15): 00078023 @ 0x10030 - OK
[]
|- bir_is_lifted_inst_prog riscv_bmr (Imm64 0x10030w) (WI_end 0w 0x1000000w)
(0x10030w,[35w; 128w; 7w; 0w])
(BirProgram
[<|bb_label := BL_Address_HC (Imm64 0x10030w) "00078023";
bb_statements :=
[BStmt_Assert
(BExp_unchanged_mem_interval_distinct Bit64 0 16777216
(BExp_Den (BVar "x15" (BType_Imm Bit64))) 1);
BStmt_Assign (BVar "MEM8" (BType_Mem Bit64 Bit8))
(BExp_Store (BExp_Den (BVar "MEM8" (BType_Mem Bit64 Bit8)))
(BExp_Den (BVar "x15" (BType_Imm Bit64)))
BEnd_LittleEndian (BExp_Const (Imm8 0w)))];
bb_last_statement :=
BStmt_Jmp (BLE_Label (BL_Address (Imm64 0x10034w)))|>])

ADDI x15,x1,-50: FCE08793 @ 0x10030 - OK
[]
|- bir_is_lifted_inst_prog riscv_bmr (Imm64 0x10030w) (WI_end 0w 0x1000000w)
Expand Down Expand Up @@ -1234,7 +1292,7 @@ REMUW x5, x6, x7: 027372BB @ 0x10030 - OK
SUMMARY FAILING HEXCODES RISC-V


Instructions FAILED: 10/74
Instructions FAILED: 10/77

"3400F0F3" (* bmr_step_hex failed *),
"3400E0F3" (* bmr_step_hex failed *),
Expand Down
9 changes: 9 additions & 0 deletions src/tools/lifter/selftest_riscv.sml
View file
Original file line number Diff line number Diff line change
Expand Up @@ -156,9 +156,18 @@ val _ = print_msg "\n";
* memory address in x2 with offset 8 *)
val _ = riscv_test_hex_print_asm "SW x14, 8(x2)" "00E12423";

(* Usage of the zero register: ("SD x0, 0(x7)") *)
val _ = riscv_test_hex_print_asm "SD x0, 0(x7)" "0003B023";

(* Usage of the zero register: ("SW x0, 0(x7)") *)
val _ = riscv_test_hex_print_asm "SW x0, 0(x7)" "0003A023";

(* Usage of the zero register: ("SH x0, 0(x15)") *)
val _ = riscv_test_hex_print_asm "SH x0, 0(x15)" "00079023";

(* Usage of the zero register: ("SB x0, 0(x15)") *)
val _ = riscv_test_hex_print_asm "SB x0, 0(x15)" "00078023";

(* I-format (opcode OP-IMM) *)
val _ = riscv_test_asms [
(* Addition by constant *)
Expand Down

0 comments on commit 441c8fc

Please sign in to comment.