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