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