1structure stack_introLib :> stack_introLib = 2struct 3 4open HolKernel boolLib bossLib Parse; 5open helperLib backgroundLib file_readerLib writerLib; 6 7open GraphLangTheory 8 9fun STACK_MEMORY_INTRO_RULE th = let 10 val (_,p,_,_) = th |> concl |> dest_spec 11 val ps = list_dest dest_star p 12 val pat = case !arch_name of ARM => ``arm_MEMORY d m`` 13 | M0 => ``m0_MEMORY d m`` 14 val x = first (can (match_term pat)) ps 15 val d = x |> rator |> rand 16 val m = x |> rand 17 val th = th |> RW1 [GSYM arm_STACK_MEMORY_def, 18 GSYM m0_STACK_MEMORY_def] 19 val th = th |> INST [m |-> mk_var("stack" ,type_of m), 20 d |-> mk_var("dom_stack" ,type_of d)] 21 in th end handle HOL_ERR _ => th; 22 23(* 24 val () = arm_progLib.arm_config "vfpv3" "array" 25 val (f,_,_,_) = arm_decompLib.l3_arm_tools 26 val ((th,_,_),_) = f "e59d900c" (* ldr r9, [sp, #12] *) 27 val ((th,_,_),_) = f "e58d2010" (* str r2, [sp, #16] *) 28 val ((th,_,_),_) = f "e92d0030" (* push {r4, r5} *) 29 val ((th,_,_),_) = f "e92d0010" (* push {r4} *) 30 val ((th,_,_),_) = f "e24dd014" (* sub sp, sp, #20 *) 31 val ((th,_,_),_) = f "e1370006" (* teq r7, r6 *) 32*) 33 34val STACK_INTRO_RULE_input = ref ([]:int list,TRUTH); 35 36(* 37 val (stack_accesses,th) = !STACK_INTRO_RULE_input 38*) 39 40local 41 fun get_pc_pat () = let 42 val (_,_,_,pc) = get_tools () 43 in ``^pc w`` end 44 val r13 = mk_var("r13",``:word32``) 45 fun dest_r13 q = let 46 val r13_pat = case !arch_name of 47 ARM => ``arm_REG (R_mode mode 13w) r13`` 48 | M0 => ``m0_REG RName_SP_main r13`` 49 val tm = find_term (can (match_term r13_pat)) q |> rand 50 in let val (x,y) = wordsSyntax.dest_word_add tm 51 val _ = x = r13 orelse fail() 52 in y |> wordsSyntax.dest_n2w |> fst |> numSyntax.int_of_term end 53 handle HOL_ERR _ => 54 let val (x,y) = wordsSyntax.dest_word_sub tm 55 val _ = x = r13 orelse fail() 56 in 0-(y |> wordsSyntax.dest_n2w |> fst |> numSyntax.int_of_term) end 57 handle HOL_ERR _ => 58 if tm = r13 then 0 else failwith "unexpected value assigned to r13" end 59 fun get_pc_num th = let 60 val pc_pat = get_pc_pat () 61 val (_,p,_,_) = dest_spec (concl th) 62 in find_term (can (match_term pc_pat)) p 63 |> rand |> wordsSyntax.dest_n2w |> fst |> numSyntax.int_of_term end 64in 65 fun STACK_INTRO_RULE stack_accesses th = let 66 val (_,p,_,q) = dest_spec (concl th) 67 val (n,must_intro) = (dest_r13 q,true) 68 handle HOL_ERR _ => (0,mem (get_pc_num th) stack_accesses) 69 in if n <> 0 orelse must_intro then STACK_MEMORY_INTRO_RULE th else th end 70 handle HOL_ERR e => 71 (STACK_INTRO_RULE_input := (stack_accesses,th); 72 report_error "STACK_INTRO_RULE" (HOL_ERR e)) 73end 74 75end 76