1(* ------------------------------------------------------------------------ *) 2(* Support running ARM model with a Patricia tree program memory *) 3(* ------------------------------------------------------------------------ *) 4 5(* interactive use: 6 app load ["arm_decoderTheory", "armTheory", "wordsLib", 7 "patriciaTheory", "parmonadsyntax"]; 8*) 9 10open HolKernel boolLib bossLib Parse; 11 12open patriciaTheory arm_coretypesTheory arm_astTheory arm_seq_monadTheory 13 arm_decoderTheory arm_opsemTheory armTheory; 14 15val _ = new_theory "arm_eval"; 16 17(* ------------------------------------------------------------------------ *) 18 19val _ = numLib.prefer_num(); 20val _ = wordsLib.prefer_word(); 21 22infix \\ << >> 23 24val op \\ = op THEN; 25val op << = op THENL; 26val op >> = op THEN1; 27 28val _ = temp_overload_on (parmonadsyntax.monad_bind, ``seqT``); 29val _ = temp_overload_on (parmonadsyntax.monad_par, ``parT``); 30val _ = temp_overload_on ("return", ``constT``); 31 32(* ------------------------------------------------------------------------ *) 33 34val ptree_read_word_def = Define` 35 ptree_read_word (prog:word8 ptree) (a:word32) : word32 M = 36 let pc = w2n a in 37 (case prog ' pc 38 of SOME b1 => 39 (case prog ' (pc + 1) 40 of SOME b2 => 41 (case prog ' (pc + 2) 42 of SOME b3 => 43 (case prog ' (pc + 3) 44 of SOME b4 => constT (word32 [b1; b2; b3; b4]) 45 | NONE => errorT "couldn't fetch an instruction") 46 | NONE => errorT "couldn't fetch an instruction") 47 | NONE => errorT "couldn't fetch an instruction") 48 | NONE => errorT "couldn't fetch an instruction")`; 49 50val ptree_read_halfword_def = Define` 51 ptree_read_halfword (prog:word8 ptree) (a:word32) : word16 M = 52 let pc = w2n a in 53 case prog ' pc 54 of SOME b1 => 55 (case prog ' (pc + 1) 56 of SOME b2 => constT (word16 [b1; b2]) 57 | NONE => errorT "couldn't fetch an instruction") 58 | NONE => errorT "couldn't fetch an instruction"`; 59 60val ptree_arm_next_def = zDefine 61 `ptree_arm_next ii (x:string # Encoding # word4 # ARMinstruction) 62 (pc:word32) (cycle:num) : unit M = 63 arm_instr ii (SND x)`; 64 65val attempt_def = Define` 66 attempt c f g = 67 \s:arm_state. 68 case f s 69 of Error e => ValueState (c, e) s 70 | ValueState v s' => g v s'`; 71 72val ptree_arm_loop_def = Define` 73 ptree_arm_loop ii cycle prog t : (num # string) M = 74 if t = 0 then 75 constT (cycle, "finished") 76 else 77 attempt cycle 78 (fetch_instruction ii (ptree_read_word prog) (ptree_read_halfword prog)) 79 (\x. 80 read_pc ii >>= 81 (\pc:word32. 82 ptree_arm_next ii x pc cycle >>= 83 (\u:unit. 84 ptree_arm_loop ii (cycle + 1) prog (t - 1))))`; 85 86val ptree_arm_run_def = Define` 87 ptree_arm_run prog state t = 88 case ptree_arm_loop <| proc := 0 |> 0 prog t state 89 of Error e => (e, NONE) 90 | ValueState (c,v) s => 91 ("at cycle " ++ num_to_dec_string c ++ ": " ++ v, SOME s)`; 92 93(* ------------------------------------------------------------------------ *) 94 95val proc_def = zDefine `proc (n:num) f = \(i,x). if i = n then f x else ARB`; 96 97val mk_arm_state_def = Define` 98 mk_arm_state arch regs psrs md mem = 99 <| registers := proc 0 regs; 100 psrs := proc 0 psrs; 101 event_register := (K T); 102 interrupt_wait := (K F); 103 memory := (\a. case patricia$PEEK mem (w2n a) 104 of SOME d => d 105 | NONE => md); 106 accesses := []; 107 information := <| arch := arch; 108 unaligned_support := T; 109 extensions := {} |>; 110 coprocessors updated_by 111 (Coprocessors_state_fupd 112 (cp15_fupd (CP15reg_SCTLR_fupd 113 (\sctlr. sctlr with <| V := F; A := T; U := F; 114 IE := T; TE := F; NMFI := T; 115 EE := T; VE := F |>)) o 116 cp14_fupd (CP14reg_TEEHBR_fupd (K 0xF0000000w)))); 117 monitors := <| ClearExclusiveByAddress := (K (constE ())) |> |>`; 118 119(* ------------------------------------------------------------------------ *) 120 121val registers_def = Define` 122 registers r0 r1 r2 r3 r4 r5 r6 r7 r8 r9 r10 r11 r12 r13 123 r14 r15 r16 r17 r18 r19 r20 r21 r22 r23 r24 r25 124 r26 r27 r28 r29 r30 r31 (r32:word32) = 125 \name. 126 RName_CASE 127 name r0 r1 r2 r3 r4 r5 r6 r7 r8 r9 r10 r11 r12 r13 128 r14 r15 r16 r17 r18 r19 r20 r21 r22 r23 r24 r25 129 r26 r27 r28 r29 r30 r31 r32` 130 131val psrs_def = Define` 132 psrs r0 r1 r2 r3 r4 r5 (r6:ARMpsr) = 133 \name. PSRName_CASE name r0 r1 r2 r3 r4 r5 r6` 134 135(* ------------------------------------------------------------------------ *) 136 137local 138 val tm1 = ``((n:num,r:RName) =+ d:word32)`` 139 140 val tm2 = 141 ``proc n 142 (registers r0 r1 r2 r3 r4 r5 r6 r7 r8 r9 r10 r11 r12 r13 143 r14 r15 r16 r17 r18 r19 r20 r21 r22 r23 r24 r25 144 r26 r27 r28 r29 r30 r31 r32)`` 145 146 fun reg n = mk_var ("r" ^ Int.toString n, ``:word32``) 147 148 fun reg_update (n,name) = 149 mk_eq (mk_comb (Term.subst [``r:RName`` |-> name] tm1, tm2), 150 Term.subst [reg n |-> ``d:word32``] tm2) 151 152 val thm = list_mk_conj (map reg_update (Lib.zip (List.tabulate(33,I)) 153 [``RName_0usr ``, ``RName_1usr ``, ``RName_2usr ``, ``RName_3usr``, 154 ``RName_4usr ``, ``RName_5usr ``, ``RName_6usr ``, ``RName_7usr``, 155 ``RName_8usr ``, ``RName_8fiq ``, ``RName_9usr ``, ``RName_9fiq``, 156 ``RName_10usr``, ``RName_10fiq``, ``RName_11usr``, ``RName_11fiq``, 157 ``RName_12usr``, ``RName_12fiq``, 158 ``RName_SPusr``, ``RName_SPfiq``, ``RName_SPirq``, ``RName_SPsvc``, 159 ``RName_SPabt``, ``RName_SPund``, ``RName_SPmon``, 160 ``RName_LRusr``, ``RName_LRfiq``, ``RName_LRirq``, ``RName_LRsvc``, 161 ``RName_LRabt``, ``RName_LRund``, ``RName_LRmon``, ``RName_PC``])) 162 163 val register_update = Tactical.prove(thm, 164 SRW_TAC [] [combinTheory.UPDATE_def, FUN_EQ_THM, registers_def, proc_def] 165 \\ Cases_on `x` \\ SRW_TAC [] [] \\ FULL_SIMP_TAC (srw_ss()) [] 166 \\ Cases_on `r` \\ FULL_SIMP_TAC (srw_ss()) []) 167in 168 val register_update = save_thm("register_update", GEN_ALL register_update) 169end 170 171local 172 val tm1 = ``((n:num,p:PSRName) =+ d:ARMpsr)`` 173 val tm2 = ``proc n (psrs r0 r1 r2 r3 r4 r5 r6)``; 174 175 fun psr n = mk_var ("r" ^ Int.toString n, ``:ARMpsr``) 176 177 fun psr_update (n,name) = 178 mk_eq (mk_comb (Term.subst [``p:PSRName`` |-> name] tm1, tm2), 179 Term.subst [psr n |-> ``d:ARMpsr``] tm2) 180 181 val thm = list_mk_conj (map psr_update (Lib.zip (List.tabulate(7,I)) 182 [``CPSR ``, ``SPSR_fiq ``, ``SPSR_irq ``, ``SPSR_svc``, 183 ``SPSR_mon``, ``SPSR_abt``, ``SPSR_und``])) 184 185 val psr_update = Tactical.prove(thm, 186 SRW_TAC [] [combinTheory.UPDATE_def, FUN_EQ_THM, psrs_def, proc_def] 187 \\ Cases_on `x` \\ SRW_TAC [] [] \\ FULL_SIMP_TAC (srw_ss()) [] 188 \\ Cases_on `r` \\ FULL_SIMP_TAC (srw_ss()) []) 189in 190 val psr_update = save_thm("psr_update", GEN_ALL psr_update) 191end 192 193val proc = Q.store_thm("proc", `proc n f (n,x) = f x`, SRW_TAC [] [proc_def]) 194 195val _ = computeLib.add_persistent_funs 196 ["combin.o_THM", "proc", "register_update", "psr_update"] 197 198(* ------------------------------------------------------------------------ *) 199 200val _ = export_theory () 201