diff options
Diffstat (limited to 'test/hol/test_raw_addScript.sml')
| -rw-r--r-- | test/hol/test_raw_addScript.sml | 248 |
1 files changed, 248 insertions, 0 deletions
diff --git a/test/hol/test_raw_addScript.sml b/test/hol/test_raw_addScript.sml new file mode 100644 index 00000000..eca6def7 --- /dev/null +++ b/test/hol/test_raw_addScript.sml @@ -0,0 +1,248 @@ +open HolKernel boolLib bossLib Parse +open intLib bitLib wordsLib +open sail_valuesAuxiliaryTheory state_monad_lemmasTheory +open cheriTheory hoareTheory + +val _ = new_theory "test_raw_add"; + +val _ = Globals.max_print_depth := 20; + +(* MIPS register names + ftp://www.linux-mips.org/pub/linux/mips/doc/ABI/MIPS-N32-ABI-Handbook.pdf + *) +val gpr_names_def = Define` + gpr_names = [ + "zero"; + "at"; + "v0"; "v1"; + "a0"; "a1"; "a2"; "a3"; "a4"; "a5"; "a6"; "a7"; + "t4"; "t5"; "t6"; "t7"; + "s0"; "s1"; "s2"; "s3"; "s4"; "s5"; "s6"; "s7"; + "t8"; "t9"; + "kt0"; "kt1"; + "gp"; + "sp"; + "s8"; + "ra"]`; + +val install_code_def = Define` + install_code initialPC (code:word32 list) = + iteriS (λi c. MEMw_wrapper (initialPC + 4w*(i2w i)) 4 c) code`; + +val clocked_whileS_def = Define` + clocked_whileS clock vars cond body s = + if 0n < clock then + bindS (cond vars) + (λcond_val s'. + if cond_val then + bindS (body vars) (λvars' s''. clocked_whileS (clock-1) vars' cond body s'') s' + else returnS vars s') s + else + failS "timeout" s`; + +val install_and_run_def = Define` + install_and_run code clock = + seqS + (seqS (install_code 0x9000000040000000w code) (init_registers 0x9000000040000000w)) + (clocked_whileS clock () (λunit_var. fetch_and_execute ()) (λunit_var. returnS ()))`; + +(* obtained from + objdump -d test_raw_add.elf + (with the cheri mips binutils version of objdump) + +test_raw_add.elf: file format elf64-bigmips + +Disassembly of section .text: + +9000000040000000 <start>: +9000000040000000: 24130001 li s3,1 +9000000040000004: 24140002 li s4,2 +9000000040000008: 02742020 add a0,s3,s4 +900000004000000c: 240c0001 li t0,1 +9000000040000010: 24050002 li a1,2 +9000000040000014: 00ac2820 add a1,a1,t0 +9000000040000018: 240c0001 li t0,1 +900000004000001c: 24060002 li a2,2 +9000000040000020: 01863020 add a2,t0,a2 +9000000040000024: 24070001 li a3,1 +9000000040000028: 00e73820 add a3,a3,a3 +900000004000002c: 240c0001 li t0,1 +9000000040000030: 240d0002 li t1,2 +9000000040000034: 240e0003 li t2,3 +9000000040000038: 018d7820 add t3,t0,t1 +900000004000003c: 01ee4020 add a4,t3,t2 +9000000040000040: 240c0001 li t0,1 +9000000040000044: 240dffff li t1,-1 +9000000040000048: 018d4820 add a5,t0,t1 +900000004000004c: 240cffff li t0,-1 +9000000040000050: 240dffff li t1,-1 +9000000040000054: 018d5020 add a6,t0,t1 +9000000040000058: 240cffff li t0,-1 +900000004000005c: 240d0002 li t1,2 +9000000040000060: 018d5820 add a7,t0,t1 +9000000040000064: 240c0001 li t0,1 +9000000040000068: 240dfffe li t1,-2 +900000004000006c: 018d8020 add s0,t0,t1 +9000000040000070: 4082d000 mtc0 v0,$26 + ... +900000004000007c: 4082b800 mtc0 v0,$23 + +9000000040000080 <end>: +9000000040000080: 1000ffff b 9000000040000080 <end> +9000000040000084: 00000000 nop +*) + + +val test_raw_add_insts_def = Define`test_raw_add_insts = + [0x24130001w:word32 + ;0x24140002w + ;0x02742020w + ;0x240c0001w + ;0x24050002w + ;0x00ac2820w + ;0x240c0001w + ;0x24060002w + ;0x01863020w + ;0x24070001w + ;0x00e73820w + ;0x240c0001w + ;0x240d0002w + ;0x240e0003w + ;0x018d7820w + ;0x01ee4020w + ;0x240c0001w + ;0x240dffffw + ;0x018d4820w + ;0x240cffffw + ;0x240dffffw + ;0x018d5020w + ;0x240cffffw + ;0x240d0002w + ;0x018d5820w + ;0x240c0001w + ;0x240dfffew + ;0x018d8020w + ;0x4082d000w]`; + +fun check_name n = + EVAL ``EL ^(numSyntax.term_of_int n) gpr_names``; + +val test_raw_add_post_def = Define` + test_raw_add_post s = ( + bindS (rGPR 19w) (λs3. (* check_name 19 *) + seqS (assert_expS (s3 = 1w) "add modified first input") ( + bindS (rGPR 20w) (λs4. (* check_name 20 *) + seqS (assert_expS (s4 = 2w) "add modified second input") ( + bindS (rGPR 04w) (λa0. (* check_name 04 *) + seqS (assert_expS (a0 = 3w) "add failed") ( + bindS (rGPR 05w) (λa1. (* check_name 05 *) + seqS (assert_expS (a1 = 3w) "add into first input failed") ( + bindS (rGPR 06w) (λa2. (* check_name 06 *) + seqS (assert_expS (a2 = 3w) "add into second input failed") ( + bindS (rGPR 07w) (λa3. (* check_name 07 *) + seqS (assert_expS (a3 = 2w) "add into both inputs failed") ( + bindS (rGPR 08w) (λa4. (* check_name 08 *) + seqS (assert_expS (a4 = 6w) "add-to-add pipeline failed") ( + bindS (rGPR 09w) (λa5. (* check_name 09 *) + seqS (assert_expS (a5 = 0w) "positive plus negative to zero failed") ( + bindS (rGPR 10w) (λa6. (* check_name 10 *) + seqS (assert_expS (a6 = 0xfffffffffffffffew) "negative plus negative to negative failed") ( + bindS (rGPR 11w) (λa7. (* check_name 11 *) + seqS (assert_expS (a7 = 1w) "negative plus positive to positive failed") ( + bindS (rGPR 16w) (λs0. (* check_name 16 *) + (assert_expS (s0 = 0xffffffffffffffffw) "positive plus negative to negative failed")))))))))))))))))))))) s + = {(Value (),s)})`; + +(* + +val decoded_insts1 = + listLib.MAP_CONV EVAL ``MAP decode ^(rhs(concl test_raw_add_insts_def))`` + +val (SOME_is, oty) = decoded_insts1 |> concl |> rhs |> listSyntax.dest_list +val asts = map rand SOME_is +val ls2 = listLib.MAP_CONV EVAL ``MAP SOME ^(listSyntax.mk_list(asts,optionSyntax.dest_option oty))``; +val test_raw_add_asts_def = Define` + test_raw_add_asts = ^(rand(lhs(concl ls2)))`; + +val decoded_insts = TRANS decoded_insts1 (SYM ls2) + |> ONCE_REWRITE_RULE[GSYM test_raw_add_insts_def, GSYM test_raw_add_asts_def] +*) + +val test_raw_add_thm = Q.store_thm("test_raw_add_thm", + `PrePost + (λ_. T) + (install_and_run test_raw_add_insts 100000) + (λ_ s. test_raw_add_post s)`, +(* + rw[install_and_run_def] + \\ match_mp_tac PrePost_seqS + \\ simp[] + \\ qmatch_goalsub_abbrev_tac`install_code initPC` + \\ qexists_tac`λs. code_installed initPC test_raw_add_insts s ∧ + init_registers_post s` + \\ conj_tac + >- ( + match_mp_tac PrePost_seqS \\ simp[] + \\ qexists_tac`code_installed initPC test_raw_add_insts` + \\ conj_tac + >- cheat + \\ cheat ) + fetch_and_execute_def +*) +cheat); + +(* +val cs = wordsLib.words_compset(); +val () = computeLib.extend_compset [ + computeLib.Extenders [ + intReduce.add_int_compset + ], + (* sail stuff *) + computeLib.Defs [ + sail_valuesTheory.nat_of_int_def, + sail_operators_mwordsTheory.subrange_vec_dec_def + ], + (* cheri/mips model *) + computeLib.Defs [ + decode_def + ], + (* addition test *) + computeLib.Defs [ + test_raw_add_insts_def + ] +] cs; + +computeLib.CBV_CONV cs ``decode (EL 1 test_raw_add_insts)`` + +val th1 = EVAL ``THE (decode (EL 1 test_raw_add_insts))`` + +val s1 = EVAL ``init_cp0_state () (init_state (regs:regstate) o1 seed)`` + +val th2 = ``execute ^(rhs(concl th1)) ^s1`` + |> SIMP_CONV(srw_ss())[execute_def] + |> SIMP_RULE(srw_ss())[execute_ADDIU_def] + +f"bindS" +type_of ``execute ast `` +f"init_state" +execute_ADDIU_def +type_of``OPTION_BIND`` +tyabbrev_info"M" +val (_, execute_rng) = dom_rng (type_of``execute``) +val (mdom, mrng) = dom_rng execute_rng +val state_ty = ``:regstate sequential_state`` +dest_thy_type state_ty +TypeBase.fields_of state_ty +disable_tyabbrev_printing"rel" +dest_type``:unit M`` + +f"vec_of_bits" +f"of_bits_fail" +f"maybe_failw" +f"nat_of_int" +f"just_list" +f"sfunpow" +show_assums := true +*) + +val _ = export_theory (); |