1structure graph_specsLib :> graph_specsLib =
2struct
3
4open HolKernel boolLib bossLib Parse;
5open wordsTheory listTheory combinTheory progTheory;
6open helperLib backgroundLib file_readerLib derive_specsLib stack_introLib
7open writerLib;
8
9open GraphLangTheory
10
11val code_case_of = TRUTH (* TypeBase.case_def_of ``:code`` *);
12
13val emp_pat = ``emp:'a set set``
14fun s_var() = mk_var("s",``:^(tysize ()) state``)
15
16fun get_pc_pat () = let
17  val (_,_,_,pc) = get_tools ()
18  in ``^pc w`` end
19
20local
21  val var_bool_pat = ``var_bool n (s:string -> 'a variable)``
22  val var_nat_pat = ``var_nat n (s:string -> 'a variable)``
23  val var_word8_pat = ``var_word8 n (s:string -> 'a variable)``
24  val var_word_pat = ``var_word n (s:string -> 'a variable)``
25  val var_mem_pat = ``var_mem n (s:string -> 'a variable)``
26in
27  fun var_lookup tm =
28    can (match_term var_bool_pat) tm orelse
29    can (match_term var_nat_pat) tm orelse
30    can (match_term var_word8_pat) tm orelse
31    can (match_term var_word_pat) tm orelse
32    can (match_term var_mem_pat) tm
33  fun mk_update (x,y) = let
34    val ty = tysize ()
35    val var_bool = mk_const("VarBool",``: bool -> ^ty variable``)
36    val var_nat = mk_const("VarNat",``: num -> ^ty variable``)
37    val var_word8 = mk_const("VarWord8",``: word8 -> ^ty variable``)
38    val var_word = mk_const("VarWord",``: ^ty word -> ^ty variable``)
39    val var_mem = mk_const("VarMem",``: (^ty word -> word8) -> ^ty variable``)
40    in
41    if can (match_term var_bool_pat) x then
42      pairSyntax.mk_pair(x |> rator |> rand,
43      mk_abs(s_var(),mk_comb(var_bool,y)))
44    else if can (match_term var_nat_pat) x then
45      pairSyntax.mk_pair(x |> rator |> rand,
46      mk_abs(s_var(),mk_comb(var_nat,y)))
47    else if can (match_term var_word8_pat) x then
48      pairSyntax.mk_pair(x |> rator |> rand,
49      mk_abs(s_var(),mk_comb(var_word8,y)))
50    else if can (match_term var_word_pat) x then
51      pairSyntax.mk_pair(x |> rator |> rand,
52      mk_abs(s_var(),mk_comb(var_word,y)))
53    else if can (match_term var_mem_pat) x then
54      pairSyntax.mk_pair(x |> rator |> rand,
55      mk_abs(s_var(),mk_comb(var_mem,y)))
56    else failwith "should not happen (mk_update)" end
57end
58
59local
60  val s32 = mk_var("s",``:string -> 32 variable``)
61  val s64 = mk_var("s",``:string -> 64 variable``)
62  val arm_state_inst = arm_STATE_thm |> concl |> find_terms var_lookup
63          |> map (fn tm =>
64            let
65              val str = tm |> rator |> rand |> stringSyntax.fromHOLstring
66              val ty = type_of tm
67            in mk_var(str,ty) |-> tm end)
68          |> (fn x => (``dmem:word32 set`` |->
69                       ``(var_dom "dom" ^s32):word32 set``)::
70                      (``dom_stack:word32 set`` |->
71                       ``(var_dom "dom_stack" ^s32):word32 set``)::
72                      (``mode:word5`` |->
73                       ``w2w (var_word8 "mode" ^s32):word5``)::x) |> INST
74  val arm_state = arm_STATE_thm |> concl |> rator |> rand
75  val arm_state_parts = arm_STATE_thm |> concl |> rand |> list_dest dest_star
76  val arm_state_type = arm_state_parts |> hd |> type_of
77  val arm_state_combs = map (fn tm => (rator tm,rand tm)) arm_state_parts
78  val arm_state_thm = arm_STATE_thm
79  val m0_state_inst = m0_STATE_thm |> concl |> find_terms var_lookup
80          |> map (fn tm =>
81            let
82              val str = tm |> rator |> rand |> stringSyntax.fromHOLstring
83              val ty = type_of tm
84            in mk_var(str,ty) |-> tm end)
85          |> (fn x => (``dmem:word32 set`` |->
86                       ``(var_dom "dom" ^s32):word32 set``)::
87                      (``dom_stack:word32 set`` |->
88                       ``(var_dom "dom_stack" ^s32):word32 set``)::
89                      (mk_var("count",``:num``) |->
90                       ``(var_nat "clock" ^s32):num``)::
91                      (``mode:Mode`` |->
92                       ``Mode_Thread:Mode``)::x) |> INST
93  val m0_state = m0_STATE_thm |> concl |> rator |> rand
94  val m0_state_parts = m0_STATE_thm |> concl |> rand |> list_dest dest_star
95  val m0_state_type = m0_state_parts |> hd |> type_of
96  val m0_state_combs = map (fn tm => (rator tm,rand tm)) m0_state_parts
97  val m0_state_thm = m0_STATE_thm
98  val riscv_state_inst = riscv_STATE_thm |> concl |> find_terms var_lookup
99          |> map (fn tm =>
100            let
101              val str = tm |> rator |> rand |> stringSyntax.fromHOLstring
102              val ty = type_of tm
103            in mk_var(str,ty) |-> tm end)
104          |> (fn x => (``dmem:word64 set`` |->
105                       ``(var_dom "dom" ^s64):word64 set``)::
106                      (``dom_stack:word64 set`` |->
107                       ``(var_dom "dom_stack" ^s64):word64 set``)::x) |> INST
108  val riscv_state = riscv_STATE_thm |> concl |> rator |> rand
109  val riscv_state_parts = riscv_STATE_thm |> concl |> rand |> list_dest dest_star
110  val riscv_state_type = riscv_state_parts |> hd |> type_of
111  val riscv_state_combs = map (fn tm => (rator tm,rand tm)) riscv_state_parts
112  val riscv_state_thm = riscv_STATE_thm
113in
114  fun state_tools () =
115    case (!arch_name) of
116      ARM => (arm_state_inst, arm_state, arm_state_parts,
117              arm_state_type, arm_state_combs, arm_state_thm)
118    | M0 => (m0_state_inst, m0_state, m0_state_parts, m0_state_type,
119             m0_state_combs, m0_state_thm)
120    | RISCV => (riscv_state_inst, riscv_state, riscv_state_parts, riscv_state_type,
121                riscv_state_combs, riscv_state_thm)
122end
123
124val STATE_INTRO_RULE_input = ref TRUTH
125(*
126  val th = !STATE_INTRO_RULE_input
127*)
128fun STATE_INTRO_RULE th = let
129  val (state_inst, state, state_parts,
130       state_type, state_combs, state_thm) = state_tools ()
131  val pc_pat = get_pc_pat ()
132  val th = th |> SIMP_RULE (std_ss++sep_cond_ss) []
133              |> REWRITE_RULE [SPEC_MOVE_COND] |> UNDISCH_ALL
134              |> Q.INST [`curr`|->`stack`]
135  (* make pre into just ``STATE s`` *)
136  val th = state_inst th
137  val (_,pre,_,_) = dest_spec (concl th)
138  val ps = list_dest dest_star pre
139  val pc = first (can (match_term pc_pat)) ps
140  val missing_parts = term_diff state_parts ps
141  val frame = list_mk_star missing_parts state_type
142  val th = SPEC_FRAME_RULE th frame
143  val (_,pre,_,_) = dest_spec (concl th)
144  val goal = mk_eq(pre,mk_star(state,pc))
145  val conv = PURE_REWRITE_CONV [state_thm,emp_STAR] THENC
146             BINOP_CONV STAR_AC_CONV THENC REWRITE_CONV []
147  val lemma = auto_conv_prove "STATE_INTRO_RULE - 1" goal conv
148  val th = th |> CONV_RULE (PRE_CONV (REWR_CONV lemma))
149  (* make post into just state *)
150  val th = PURE_REWRITE_RULE [STAR_IF] th
151  val (_,_,_,post) = dest_spec (concl th)
152  fun term_term_all_distinct [] = []
153    | term_term_all_distinct ((x,y)::xs) =
154        (x,y) :: filter (fn (t1,t2) => not (aconv t1 x andalso aconv t2 y)) xs
155  fun fix_post_conv post = let
156    val ps = list_dest dest_star post
157    val pc = first (can (match_term pc_pat)) ps
158    val ps = filter (not o can (match_term pc_pat)) ps
159    val ps = filter (not o can (match_term emp_pat)) ps
160    fun find_match x [] = fail ()
161      | find_match x ((n,y)::xs) =
162          if aconv x n then y else find_match x xs
163    fun find_all_matches tm =
164      [(find_match (rator tm) state_combs,rand tm)]
165      handle HOL_ERR _ => let
166        val x = repeat rator tm
167        val y = first (fn tm => aconv x (repeat rator tm)) state_parts
168        fun dest_app tm = let
169          val (x,y) = dest_comb tm
170          val (f,xs) = dest_app x
171          in (f,xs @ [y]) end handle HOL_ERR _ => (tm,[])
172        val xs = zip (dest_app y |> snd) (dest_app tm |> snd)
173        in xs end
174    val qs = ps |> map find_all_matches |> flatten
175                |> filter (fn (x,y) => not (aconv x y))
176                |> term_term_all_distinct
177    val ty = tysize ()
178    val new_s = listSyntax.mk_list(
179                  foldl (fn ((x,y),s) => mk_update(x,y)::s) [] qs,
180                  ``:string # (^ty state -> ^ty variable)``)
181    val new_s = ``apply_update ^new_s ^(s_var())``
182    val goal = mk_eq(post,mk_star(mk_comb(rator state,new_s),pc))
183    val conv = (REWRITE_CONV [state_thm,var_update_thm,
184                  apply_update_def,
185                  CONS_11,NOT_CONS_NIL,GSYM NOT_CONS_NIL]
186                THENC (DEPTH_CONV stringLib.string_EQ_CONV)
187                THENC REWRITE_CONV [] THENC SIMP_CONV (srw_ss()) []
188                THENC PURE_REWRITE_CONV [state_thm,emp_STAR]
189                THENC BINOP_CONV STAR_AC_CONV THENC REWRITE_CONV [])
190    val lemma = auto_conv_prove "STATE_INTRO_RULE - 2" goal conv
191    in lemma end
192  fun fix_if_post_conv post =
193    if is_cond post then BINOP_CONV fix_if_post_conv post
194    else fix_post_conv post
195  val th = th |> CONV_RULE (POST_CONV fix_if_post_conv)
196  in th end
197  handle HOL_ERR e =>
198    (STATE_INTRO_RULE_input := th;
199     report_error "STATE_INTRO_RULE" (HOL_ERR e))
200
201fun write_transform th1 th2_opt th_res = let
202  val clean_th = REWRITE_RULE [] o DISCH_ALL
203  val _ = write_line "Proved:"
204  val _ = write_thm (clean_th th_res)
205  val _ = write_line "Using:"
206  val _ = write_thm (clean_th th1)
207  val _ = (case th2_opt of NONE => () | SOME th => write_thm (clean_th th))
208  in th_res end
209
210fun mk_code_term c =
211  case (!arch_name) of ARM => ``ARM ^c``
212                     | M0 => ``M0 ^c``
213                     | RISCV => ``RISCV ^c``;
214
215val make_ASM_input = ref TRUTH;
216val make_CALL_input = ref TRUTH;
217val make_SWITCH_input = ref TRUTH;
218
219(*
220val th = !make_ASM_input
221*)
222
223local
224  fun read_pc_assum hs = let
225    val h = first (can (match_term ``var_word "pc" s = w``)) hs
226    in (h |> rand,filter (fn tm => not (aconv tm h)) hs) end
227  fun read_pc_update th = let
228    val tm = find_term (can (match_term ``("pc" =+ VarWord (n2w n))``))
229               (concl th) |> rand |> rand
230    in (mk_comb(``Jump``,tm),th) end
231    handle HOL_ERR _ => let
232    val tm = find_term (can (match_term ``("pc" =+ pat)``)) (concl th)
233    val x = ``var_word "ret" s``
234    val assum = mk_eq(tm |> rand,``^(s_var()) "ret"``)
235    val rw = RAND_CONV (fn tm => ASSUME assum) tm
236    val th = RW1 [rw] th
237    in (``Return``,th) end
238  fun read_state_update th = let
239    val (_,_,_,q) = dest_spec (concl th)
240    in q |> rand end
241  val simp = SIMP_CONV std_ss [IMPL_INST_def,exec_next_def,CONS_11,NOT_CONS_NIL,
242        check_jump_def,get_assert_def,APPLY_UPDATE_THM,
243        stringTheory.CHR_11,code_case_of]
244  fun has_call_tag th =
245    can (find_term (can dest_call_tag)) (concl (DISCH_ALL th))
246  val ret_and_all_names =
247    ret_and_all_names_def |> concl |> rand
248                          |> REWRITE_CONV [all_names_def,APPEND] |> concl |> rand
249                          |> listSyntax.dest_list |> fst
250  fun dest_supdate tm =
251    listSyntax.dest_list tm |> fst |> map pairSyntax.dest_pair
252  fun prepare_supdate_for_call th = let
253    val (_,pre,_,post) = dest_spec (concl th)
254    val pc1 = pre |> rand |> rand
255    val tm = post |> rator |> rand |> rand |> rator |> rand
256    val supdate = dest_supdate tm
257    val r0 = ``"r0"``
258    val r1 = ``"r1"``
259    val r10 = ``"r10"``
260    val r14 = ``"r14"``
261    val ret_reg_name = (if !arch_name = RISCV then r1 else r14)
262    val ret_addr_reg_name = (if !arch_name = RISCV then r10 else r0)
263    val ret_str = ``"ret"``
264    val ret_addr_input_str = ``"ret_addr_input"``
265    val (is_tail_call,ret) = let
266      val u = first (fn (t,x) => aconv t ret_reg_name) supdate |> snd
267      val res = EVAL ``(^u s = VarWord (^pc1+4w)) \/ (^u s = VarWord (^pc1+2w))``
268        |> concl |> rand
269      in if aconv res T then
270           (false,mk_comb(mk_const("Jump",``:^(tysize()) word -> ^(tysize()) jump``),
271                          u |> dest_abs |> snd |> rand))
272         else (true,mk_const("Return",``:^(tysize()) jump``)) end
273         handle HOL_ERR _ => (true,mk_const("Return",``:^(tysize()) jump``))
274    val var_acc_ty = ``:string -> (string -> ^(tysize()) variable) -> ^(tysize()) variable``
275    val var_acc = mk_const ("var_acc",var_acc_ty)
276    fun get_assign tm =
277      if aconv tm ret_addr_input_str then let
278        val var_acc_ret = mk_comb(var_acc,ret_addr_reg_name)
279        in pairSyntax.mk_pair(ret_addr_input_str,var_acc_ret) end
280      else let
281        val tm2 = if is_tail_call then tm else
282                  if aconv tm ret_str then ret_reg_name else tm
283        val rhs = first (fn (t,x) => (aconv t tm2)) supdate |> snd
284                  handle HOL_ERR _ => mk_comb(var_acc,tm)
285        in pairSyntax.mk_pair(tm,rhs) end
286    val new_supdate = map get_assign ret_and_all_names
287    val new_supdate = listSyntax.mk_list(new_supdate,type_of (hd new_supdate))
288    val x = post |> rator |> rand |> rator
289    val goal = ``^x (apply_update ^tm s) = ^x (apply_update ^new_supdate s)``
290    val lemma = auto_prove "prepare_supdate_for_call" (goal,
291      TRY (MATCH_MP_TAC arm_STATE_all_names)
292      \\ TRY (MATCH_MP_TAC m0_STATE_all_names)
293      \\ TRY (MATCH_MP_TAC riscv_STATE_all_names)
294      \\ REWRITE_TAC [all_names_def,EVERY_DEF,apply_update_def,
295           combinTheory.APPLY_UPDATE_THM,var_acc_def]
296      \\ CONV_TAC (DEPTH_CONV BETA_CONV)
297      \\ CONV_TAC (DEPTH_CONV stringLib.string_EQ_CONV)
298      \\ REWRITE_TAC [all_names_def,EVERY_DEF,apply_update_def,
299           combinTheory.APPLY_UPDATE_THM,var_acc_def])
300    val th = CONV_RULE ((RAND_CONV o RATOR_CONV o RAND_CONV)
301               (REWR_CONV lemma)) th
302    in (th,ret) end
303(*
304  val th = !make_CALL_input
305*)
306  fun make_CALL th = let
307    val th = STATE_INTRO_RULE th
308    val hs = filter (fn tm => not (aconv tm T)) (hyp th)
309    val tag = first (can dest_call_tag) hs
310    val fname = fst (dest_call_tag tag)
311    val th = th |> DISCH_ALL |> PURE_REWRITE_RULE [CALL_TAG_def] |> UNDISCH_ALL
312    val (_,pre,_,post) = dest_spec (concl th)
313    val pc1 = pre |> rand |> rand
314    val pc2 = post |> rand |> rand
315    val supdate = post |> rator |> rand |> rand |> rator |> rand
316    val hs = filter (fn tm => not (aconv tm T)) (hyp th)
317    val side = if length hs = 0
318               then mk_const("NONE",``:(^(tysize())state->bool) option``)
319               else ``SOME ^(mk_abs(s_var(),list_mk_conj hs))``
320    val (th,ret) = prepare_supdate_for_call th
321    val (_,pre,_,post) = dest_spec (concl th)
322    val supdate = post |> rator |> rand |> rand |> rator |> rand
323    val name = stringSyntax.fromMLstring fname
324    val i = ``Inst ^pc1 (K T) (CALL ^side ^supdate ^name ^ret)``
325    val (m,_,c,_) = dest_spec (concl th)
326    val goal = ``(locs ^name = SOME ^pc2) ==> IMPL_INST ^(mk_code_term c) locs ^i``
327(*
328  set_goal([],goal)
329*)
330    val lemma = auto_prove "make_CALL" (goal,
331      CONV_TAC simp \\ REPEAT STRIP_TAC \\ IMP_RES_TAC ret_lemma
332      \\ ASM_SIMP_TAC std_ss [code_case_of]
333      \\ NTAC 20 (ONCE_REWRITE_TAC [var_word_apply_update])
334      \\ CONV_TAC (DEPTH_CONV stringLib.string_EQ_CONV)
335      \\ ASM_REWRITE_TAC [apply_update_NIL]
336      \\ SIMP_TAC std_ss [next_ok_def,check_ret_def,
337                          ARM_def,M0_def,RISCV_def,LET_THM]
338      \\ TRY (REWRITE_TAC [ret_and_all_names_def,all_names_def,MAP,APPEND]
339        \\ REWRITE_TAC [all_names_def,EVERY_DEF,apply_update_def,
340             combinTheory.APPLY_UPDATE_THM,var_acc_def,var_word_def]
341        \\ EVAL_TAC \\ NO_TAC)
342      \\ (DISCH_ALL th |> DISCH T
343            |> PURE_REWRITE_RULE [AND_IMP_INTRO] |> MATCH_MP_TAC)
344      \\ ASM_REWRITE_TAC [] \\ FULL_SIMP_TAC (srw_ss()) [])
345    val th = lemma |> UNDISCH_ALL |> SIMP_RULE std_ss [word_add_n2w]
346    in th end
347    handle HOL_ERR e =>
348      (make_CALL_input := th;
349       report_error "make_CALL" (HOL_ERR e))
350(*
351  val th = !make_ASM_input
352*)
353  fun make_ASM th =
354    if has_call_tag th then make_CALL th else let
355    val th = STATE_INTRO_RULE th
356    val (_,pre,_,post) = dest_spec (concl th)
357    val pc1 = pre |> rand |> rand
358    val pc2 = post |> rand |> rand
359    val supdate = post |> rator |> rand |> rand |> rator |> rand
360    val ty = tysize ()
361    val (jmp,th) = if wordsSyntax.is_n2w pc2 then (``Jump ^pc2``,th) else
362      (mk_const("Return",``: ^ty jump``),let
363         val lemma = ASSUME (mk_eq(pc2,``var_word "ret" ^(s_var())``))
364         in CONV_RULE (RAND_CONV (RAND_CONV (RAND_CONV (fn tm => lemma)))) th end)
365    val hs = filter (fn tm => not (aconv tm T)) (hyp th)
366    val side = if length hs = 0 then mk_const("NONE",``:(^ty state->bool) option``)
367               else ``SOME ^(mk_abs(s_var(),list_mk_conj hs))``
368    val i = ``Inst ^pc1 (K T) (ASM ^side ^supdate ^jmp)``
369    val th = RW [apply_update_NIL] th
370    val (m,_,c,_) = dest_spec (concl th)
371    val goal = ``IMPL_INST ^(mk_code_term c) locs ^i``
372(*
373  set_goal([],goal)
374*)
375    val lemma = auto_prove "make_ASM" (goal,
376      CONV_TAC simp \\ REPEAT STRIP_TAC \\ IMP_RES_TAC ret_lemma
377      \\ ASM_SIMP_TAC std_ss [code_case_of,ARM_def,M0_def,RISCV_def,LET_THM]
378      \\ NTAC 20 (ONCE_REWRITE_TAC [var_word_apply_update])
379      \\ CONV_TAC (DEPTH_CONV stringLib.string_EQ_CONV)
380      \\ ASM_REWRITE_TAC [apply_update_NIL] THEN1 EVAL_TAC THEN1 EVAL_TAC
381      \\ (DISCH_ALL th |> DISCH T
382            |> PURE_REWRITE_RULE [AND_IMP_INTRO] |> MATCH_MP_TAC)
383      \\ ASM_REWRITE_TAC [] \\ FULL_SIMP_TAC (srw_ss()) [])
384    in lemma end
385    handle HOL_ERR e =>
386      (make_ASM_input := th;
387       report_error "make_ASM" (HOL_ERR e))
388(*
389  val th = !make_SWITCH_input
390*)
391  fun make_SWITCH th = let
392    val th = STATE_INTRO_RULE th
393    (* val th = SIMP_RULE std_ss [Once EQ_SYM_EQ] th *)
394    val post = th |> concl |> rand
395    val pre =
396      th |> DISCH_ALL |> DISCH T |> PURE_REWRITE_RULE [AND_IMP_INTRO]
397         |> CONV_RULE ((RATOR_CONV o RAND_CONV) (REWRITE_CONV []))
398         |> concl |> dest_imp |> fst
399    val pre = mk_abs(s_var(),pre)
400    fun get_simp_asm x1 = let
401      val upd = x1 |> rator |> rand |> rand |> rator |> rand
402      val pc = x1 |> rand |> rand
403      in ``ASM (SOME ^pre) ^upd (Jump ^pc)`` end
404    fun dest_ifs post = let
405      val (g,x1,x2) = dest_cond post
406      val next1 = get_simp_asm x1
407      val next2 = dest_ifs x2
408      in ``IF (\s. ^g) ^next1 ^next2`` end
409      handle HOL_ERR _ => get_simp_asm post
410    val next = dest_ifs post
411    val pc1 = th |> concl |> rator |> rator |> rand |> rand |> rand
412    val i = ``Inst ^pc1 (K T) ^next``
413    val (m,_,c,_) = dest_spec (concl th)
414    val goal = ``IMPL_INST ^(mk_code_term c) locs ^i``
415    val lemma = auto_prove "make_SWITCH" (goal,
416      REWRITE_TAC [IMPL_INST_IF_SPLIT,ARM_def,RISCV_def,M0_def]
417      \\ CONV_TAC (DEPTH_CONV BETA_CONV)
418      \\ REPEAT STRIP_TAC
419      \\ CONV_TAC simp \\ REPEAT STRIP_TAC
420      \\ TRY (EVAL_TAC \\ NO_TAC)
421      \\ REWRITE_TAC [LET_THM]
422      \\ CONV_TAC (DEPTH_CONV PairRules.PBETA_CONV)
423      \\ MP_TAC (DISCH_ALL th)
424      \\ ASM_REWRITE_TAC []
425      \\ STRIP_TAC
426      \\ TRY (POP_ASSUM MATCH_MP_TAC)
427      \\ ASM_REWRITE_TAC [var_word_def,var_acc_def]
428      \\ EVAL_TAC)
429    in lemma end
430    handle HOL_ERR e =>
431      (make_SWITCH_input := th;
432       report_error "make_SWITCH" (HOL_ERR e))
433in
434  fun make_INST (i:int,(th,l:int,j:int option),NONE) =
435       write_transform th NONE
436        (if not (is_cond (rand (concl th)))
437         then make_ASM th else make_SWITCH th)
438    | make_INST (i,(th1',l',j'),SOME (th2',l:int,j:int option)) = let
439        val th1 = make_INST (i,(th1',l',j'),NONE)
440        val th2 = th2' |> DISCH_ALL
441                       |> REWRITE_RULE [CALL_TAG_def] |> UNDISCH_ALL |> make_ASM
442        val not_guard = th2 |> concl |> find_term (can (match_term ``ASM (SOME k)``))
443                            |> rand |> rand |> dest_abs |> snd
444                        handle HOL_ERR _ =>
445                        th2 |> concl |> find_term (can (match_term ``CALL (SOME k)``))
446                            |> rand |> rand |> dest_abs |> snd
447        val guard = dest_neg not_guard handle HOL_ERR _ => mk_neg not_guard
448        val c = (RAND_CONV o RATOR_CONV o RAND_CONV) (SIMP_CONV std_ss [])
449        val th = MATCH_MP IMPL_INST_IF (CONJ th1 th2)
450                 |> CONV_RULE (BINOP1_CONV (SIMP_CONV std_ss []))
451                 |> MATCH_MP T_IMP |> SPEC (mk_abs(s_var(),guard))
452        val th = RW1 [IMPL_INST_SIMP_IF] th
453                 |> SIMP_RULE std_ss [IMPL_INST_IF_RW]
454        in write_transform th1' (SOME th2') th end
455end
456
457(*
458val (i:int,(th,l:int,j:int option),NONE) =
459  first (fn (i,(th,_,_),_) => i = 52) thms
460
461val (i:int,(th,l:int,j:int option),NONE) = thms |> el 2
462
463val (_,(th1,_,_),SOME (th2,l:int,j:int option)) = first (not o can make_INST) thms
464
465*)
466
467fun try_map g f [] = []
468  | try_map g f (x::xs) = let
469      val y = f x
470      in y :: try_map g f xs end
471      handle HOL_ERR _ =>
472        (g x; try_map g f xs)
473
474val graph_spec_fails = ref ([] : (int * string) list);
475
476fun print_graph_spec_fail (pos,sec_name) = let
477  val str = ("Graph spec failed in " ^ sec_name ^ " for pos " ^
478              (int_to_hex pos) ^ ".")
479  in (write_line str; print (str ^ "\n")) end
480
481fun add_graph_spec_fail pos sec_name =
482  (print_graph_spec_fail (pos,sec_name);
483   graph_spec_fails := (pos, sec_name) :: (!graph_spec_fails));
484
485fun clear_graph_spec_fails () = (graph_spec_fails := []);
486
487fun print_graph_spec_report () =
488  (if length (!graph_spec_fails) = 0 then
489    (write_line "No graph spec failures."; [])
490   else (has_failures := true;
491         map print_graph_spec_fail (!graph_spec_fails)))
492
493fun get_pc_val th = let
494  val pc_pat = get_pc_pat ()
495  val (_,p,_,_) = dest_spec (concl th)
496  in find_term (can (match_term pc_pat)) p
497       |> rand |> rand |> numSyntax.int_of_term end
498
499local
500  val r = ref [""];
501  fun get_index_name name i = let
502    val str = name ^ "_" ^ int_to_string i
503    in if mem str (!r) then get_index_name name (i+1)
504       else(r := str::(!r); str) end
505in
506  fun get_name name =
507    if mem name (!r) then get_index_name name 0
508    else (r := name::(!r); name)
509end
510
511fun derive_insts_for sec_name = let
512  val thms = derive_specs_for sec_name
513  val _ = write_subsection "Proving inst theorems"
514  val _ = (writer_prints := false)
515  val insts = try_map (fn (_,(th,_,_),_) =>
516    add_graph_spec_fail (get_pc_val th) sec_name) make_INST thms
517  val _ = (writer_prints := true)
518  val all_ok_chars = explode
519   ("abcdefghijklmonpqrstuvwxyz" ^
520    "ABCDEFGHIJKLMNOPQRSTUVWXYZ" ^
521    "0123456789_")
522  fun remove_SKIP_TAG th = let
523    val code = th |> concl |> rator |> rator |> rand |> rand
524    val pos = th |> concl |> rand |> rator |> rator |> rand |> rand
525                 |> numSyntax.dest_numeral
526                 |> Arbnumcore.toHexString
527    val th = MATCH_MP SKIP_TAG_IMP_CALL_ARM th handle HOL_ERR _ =>
528             MATCH_MP SKIP_TAG_IMP_CALL_M0 th handle HOL_ERR _ =>
529             MATCH_MP SKIP_TAG_IMP_CALL_RISCV th
530    val cs = filter (fn v => fst (dest_var v) = "code") (free_vars (concl th))
531             |> map (fn c => c |-> code)
532    val th = (INST cs th handle HOL_ERR _ => th)
533    val name = find_term (can stringLib.dest_string) (concl th)
534    fun join [] = ""
535      | join [x] = x
536      | join (x::ys) = x ^ "_" ^ join ys
537    fun prefix_instr str = "instruction'" ^ str ^ "_" ^ pos
538    val new_name = stringLib.fromHOLstring name
539                   |> String.tokens (fn c => not (mem c all_ok_chars))
540                   |> join |> prefix_instr |> get_name
541    in th |> SIMP_RULE std_ss []
542          |> SPEC (stringLib.fromMLstring new_name)
543          |> UNDISCH end
544    handle HOL_ERR _ => th
545  val insts = map remove_SKIP_TAG insts
546  val inst_count = int_to_string (length insts)
547  val _ = write_line (inst_count ^ " inst theorems describe instructions.")
548  in insts end;
549
550(*
551
552  val base_name = "loop-riscv/example"
553  val base_name = "seL4-kernel/riscv/kernel-riscv"
554  val base_name = "seL4-kernel/arm/kernel"
555  val _ = read_files base_name []
556  val _ = open_current "test"
557  val sec_name = "lookupSlot"
558  val sec_name = "memzero"
559  val sec_name = "memcpy"
560  val sec_name = "isIRQPending"
561  val sec_name = "setMRs_syscall_error"
562
563  val thms = derive_insts_for sec_name
564
565  val base_name = "loop-riscv/example"
566  val _ = read_files base_name []
567  val _ = open_current "test"
568  val sec_name = "memcpy"
569  val sec_name = "memzero"
570  val sec_name = "lookupSlot"
571  val sec_name = "resolveAddressBits"
572
573  val base_name = "loop-m0/example"
574  val _ = read_files base_name []
575  val _ = open_current "test"
576  val sec_name = "f"
577
578*)
579
580end
581