1(* 2 3loadPath := 4 (concat Globals.HOLDIR "/examples/dev/sw") :: 5 (concat Globals.HOLDIR "/examples/elliptic/arm") :: 6 (concat Globals.HOLDIR "/examples/temporal_deep/src/tools") :: 7 (concat Globals.HOLDIR "/examples/sep") :: 8 !loadPath; 9 10app load ["relationTheory", "pred_setSimps","pred_setTheory","whileTheory","finite_mapTheory","rich_listTheory", "listSyntax", 11 "ILTheory", "rulesTheory", "preARMSyntax", "annotatedIR", "funCall", "preARMTheory", "wordsLib"]; 12 13quietdec := true; 14open HolKernel Parse boolLib bossLib numLib pairLib relationTheory pairTheory arithmeticTheory listSyntax preARMTheory 15 preARMSyntax Assem pred_setSimps pred_setTheory listTheory rich_listTheory whileTheory finite_mapTheory 16 annotatedIR ILTheory rulesTheory wordsLib wordsTheory 17 preARMTheory; 18quietdec := false; 19*) 20 21structure mechReasoning = struct 22 local 23 open HolKernel Parse boolLib bossLib numLib pairLib relationTheory pairTheory arithmeticTheory listSyntax preARMTheory 24 preARMSyntax Assem pred_setSimps pred_setTheory listTheory rich_listTheory whileTheory finite_mapTheory declFuncs 25 annotatedIR ILTheory rulesTheory wordsLib wordsTheory IRSyntax 26 in 27 28infix ++ THENC ORELSEC THEN THENL ORELSE |-> ##; 29 30(*---------------------------------------------------------------------------------*) 31(* Simplifier on finite maps *) 32(*---------------------------------------------------------------------------------*) 33 34 35val fupdate_normalizer = 36 let val thm = SPEC_ALL FUPDATE_LT_COMMUTES 37 val pat = lhs(snd(dest_imp(concl thm))) 38 in 39 {name = "Finite map normalization", 40 trace = 2, 41 key = SOME([],pat), 42 conv = let fun reducer tm = 43 let val (theta,ty_theta) = match_term pat tm 44 val thm' = INST theta (INST_TYPE ty_theta thm) 45 val constraint = fst(dest_imp(concl thm')) 46 val cthm = EQT_ELIM(reduceLib.REDUCE_CONV constraint) 47 in MP thm' cthm 48 end 49 in 50 K (K reducer) 51 end} 52 end; 53 54val finmap_conv_frag = 55 simpLib.SSFRAG 56 {convs = [fupdate_normalizer], 57 rewrs = [], ac=[],filter=NONE,dprocs=[],congs=[]}; 58 59val finmap_ss = std_ss ++ finmap_conv_frag ++ rewrites [FUPDATE_EQ, FAPPLY_FUPDATE_THM]; 60 61val set_ss = std_ss ++ SET_SPEC_ss ++ PRED_SET_ss; 62 63(*---------------------------------------------------------------------------------*) 64(* Assistant Functions *) 65(*---------------------------------------------------------------------------------*) 66 67(* make variable tuple, e.g. ((v0,v1),v2,...) *) 68 69fun mk_vars exp = 70 let 71 val i = ref (~1); 72 fun set_vars (IRSyntax.PAIR (e1,e2)) = 73 mk_pair(set_vars e1, set_vars e2) 74 | set_vars exp = 75 mk_var ("v" ^ (i := !i + 1; Int.toString (!i)) , Type `:DATA`) 76 in 77 set_vars exp 78 end 79 80(* make mread tuple, e.g. ((st<v0>,st<v1>),st<v2>,...) *) 81 82fun mk_mreads st (IRSyntax.PAIR (e1,e2)) = 83 mk_pair(mk_mreads st e1, mk_mreads st e2) 84 | mk_mreads st (IRSyntax.REG e) = 85 list_mk_comb (Term`mread`, [st, mk_comb (Term`RR`, IRSyntax.convert_reg (IRSyntax.REG e))]) 86 | mk_mreads st (IRSyntax.MEM m) = 87 list_mk_comb (Term`mread`, [st, mk_comb (Term`RM`, IRSyntax.convert_mem (IRSyntax.MEM m))]) 88 | mk_mreads st _ = 89 (print "mk_mreads: invalid incoming expression"; 90 raise ERR "" ("mk_mreads: invalid incoming expression")); 91 92 93fun ADDR30_CONV t = 94 let 95 val (f, args) = dest_comb t; 96 val _ = if same_const (Term `ADDR30`) f then () else Raise (ERR "" "Syntax"); 97 val num_term = rand (rand args); 98 val num = dest_numeral num_term; 99 val (c, r) = Arbnum.divmod(num, Arbnum.fromInt 4); 100 val _ = if (r = Arbnum.zero) then () else Raise (ERR "" "Syntax"); 101 val mult_term = mk_mult(mk_numeral c, term_of_int 4); 102 val mult_thm = GSYM (EVAL mult_term); 103 val thm = RAND_CONV (RAND_CONV (REWRITE_CONV [mult_thm])) t 104 in 105 thm 106 end; 107 108val word_extract_thm = GSYM ((SIMP_RULE std_ss [w2w_def, combinTheory.o_DEF, FUN_EQ_THM]) word_extract_def); 109 110 111val SIM_REWRITE_CONV = 112 REWRITE_CONV ([mdecode_def, write_thm, read_thm, toMEM_def, toEXP_def, toREG_def, index_of_reg_def, WORD_ADD_0, FAPPLY_FUPDATE_THM, word4_distinct, 113 GSYM WORD_ADD_ASSOC, FUPDATE_EQ, fupdate_lt_commutes_word4, word_sub_def]); 114 115 116val SIM_CONV = 117 SIM_REWRITE_CONV THENC 118 WORDS_CONV THENC 119 REWRITE_CONV [word_extract_thm, WORD_ADD_0] 120 121val SIM_MEM_CONV = 122 SIM_REWRITE_CONV THENC 123 SIMP_CONV arith_ss [word4_distinct, ADDR30_ADD_CONST_MOD, GSYM WORD_ADD_ASSOC, 124 WORD_EQ_ADD_LCANCEL] THENC 125 WORDS_CONV THENC 126 REWRITE_CONV [word_extract_thm, WORD_ADD_0] 127 128val SIM_PUSH_CONV = 129 REWRITE_CONV [mdecode_def, pushL_def, GSYM MAP_REVERSE, REVERSE_DEF, APPEND, MAP, LENGTH, FOLDL] THENC 130 DEPTH_CONV GEN_BETA_CONV THENC 131 SIM_REWRITE_CONV THENC 132 SIMP_CONV arith_ss [ADDR30_ADD_CONST_MOD] THENC 133 SIM_CONV; 134 135val SIM_POP_CONV = 136 REWRITE_CONV [mdecode_def, popL_def, GSYM MAP_REVERSE, REVERSE_DEF, APPEND, MAP, LENGTH, FOLDL] THENC 137 DEPTH_CONV GEN_BETA_CONV THENC 138 SIM_REWRITE_CONV THENC 139 SIMP_CONV arith_ss [word4_distinct, ADDR30_ADD_CONST_MOD, GSYM WORD_ADD_ASSOC, 140 WORD_EQ_ADD_LCANCEL] THENC 141 SIM_CONV; 142 143(* make a list of rules [exp0 <- v0, exp1 <- v1, ...] *) 144 145fun mk_subst_rules expL = 146 let 147 val i = ref (~1); 148 in 149 List.map (fn exp => (i := !i + 1; {redex = exp, residue = mk_var ("v" ^ (Int.toString (!i)), Type `:DATA`)})) expL 150 end 151 152fun read_one_var s exp = 153 let 154 val v0 = IRSyntax.read_exp s exp; 155 fun conv (IRSyntax.MEM (b, off)) = SIM_MEM_CONV | 156 conv _ = SIM_CONV 157 val v1 = rhs (concl ((conv exp) v0)) 158 in 159 v1 160 end 161 162 163(*---------------------------------------------------------------------------------*) 164(* Symbolic Simulation of Instructions *) 165(*---------------------------------------------------------------------------------*) 166 167val ACCESS_CONV = SIMP_CONV finmap_ss [mread_def, write_thm, read_thm, toMEM_def, toEXP_def, toREG_def, index_of_reg_def]; 168val ACCESS_RULE = SIMP_RULE finmap_ss [mread_def, write_thm, read_thm, toMEM_def, toEXP_def, toREG_def, index_of_reg_def]; 169 170(* Basic RULE for instructions execpt for PUSH and POP *) 171 172 173 174(* Find the first instruction to be simulated next *) 175 176fun locate_first_inst t = 177 if type_of t = Type `:DOPER` then true 178 else false; 179 180 181fun is_mdecode_exp t = 182 (let 183 val const = #1 (strip_comb t) 184 in 185 (same_const const (Term `mdecode`)) 186 end) handle _ => false; 187 188 189fun find_innermost_mdecode t = 190 (let 191 val state = (rand (rator t)); 192 in 193 if is_mdecode_exp state then find_innermost_mdecode state else t 194 end) 195 handle e => (print "find_innermost_mdecode:syntax error"; Raise e); 196 197(* eliminate all "decode"s and get the new state *) 198(* 199fun step th = 200 let 201 val t1 = concl th 202 val st = if is_imp t1 then rhs (#2 (dest_imp t1)) else rhs t1 203 val t1 = find_term locate_first_inst st; 204 val operator = #1 (strip_comb t1); 205 val t2 = find_innermost_mdecode st; 206 val conv = if same_const operator (Term `MPUSH`) then SIM_PUSH_CONV 207 else if same_const operator (Term `MPOP`) then SIM_POP_CONV 208 else if same_const operator (Term `MLDR`) then SIM_MEM_CONV 209 else if same_const operator (Term `MSTR`) then SIM_MEM_CONV 210 else SIM_CONV 211 val t2_thm = conv t2; 212 in 213 REWRITE_RULE [t2_thm] th 214 end; 215 216val th = th1 217 218val th = step th 219*) 220fun elim_decode th = 221 let val t1 = concl th 222 val st = if is_imp t1 then rhs (#2 (dest_imp t1)) else rhs t1 223 in 224 if is_pair st then th 225 else 226 let val t1 = find_term locate_first_inst st; 227 val operator = #1 (strip_comb t1); 228 val _ = print ("Simulating a " ^ (#1 (dest_const operator)) ^ " instruction\n"); 229 val t2 = find_innermost_mdecode st; 230 val conv = if same_const operator (Term `MPUSH`) then SIM_PUSH_CONV 231 else if same_const operator (Term `MPOP`) then SIM_POP_CONV 232 else if same_const operator (Term `MLDR`) then SIM_MEM_CONV 233 else if same_const operator (Term `MSTR`) then SIM_MEM_CONV 234 else SIM_CONV 235 val t2_thm = conv t2; 236 val th' = REWRITE_RULE [t2_thm] th 237 in elim_decode th' 238 end 239 end 240 handle e => (print "get_blk_spec: errors occur while symbolically simulating a block! "; Raise e); 241 242 243(* Given a list of IR statements, return a theorem indicating the state after symolic simulation *) 244(* pre_spec specifies the pre-conditions before the simulation *) 245fun sim_stms stms = 246 let 247 val blk = mk_comb (Term`BLK`, mk_list (List.map IRSyntax.convert_stm stms, Type`:DOPER`)); 248 val st = mk_pair (mk_var ("regs", Type `:REGISTER |-> DATA`), mk_var ("mem", Type `:ADDR |-> DATA`)); 249 val instance = list_mk_comb (Term`run_ir:CTL_STRUCTURE -> DSTATE -> DSTATE`, [blk, st]); 250 val th0 = REWRITE_CONV [IR_SEMANTICS_BLK] instance; 251 val th1 = SIMP_RULE std_ss [mread_def, toMEM_def, toREG_def, index_of_reg_def, read_thm] th0; 252 val th2 = elim_decode th1 (* symbolically simulate the block *) 253 in 254 th2 255 end; 256 257(*---------------------------------------------------------------------------------*) 258(* PSPEC specification and Mechanized Reasoning *) 259(*---------------------------------------------------------------------------------*) 260 261(* Make a PSPEC specification *) 262 263val basic_outL = [IRSyntax.REG 11, IRSyntax.REG 13]; (* fp and sp *) 264 265 266val PSPEC_term = 267 Term `PSPEC:CTL_STRUCTURE -> 268 ((bool ** i4 |-> bool ** i32) # (bool ** i30 |-> bool ** i32) -> 269 bool) # 270 ((bool ** i4 |-> bool ** i32) # (bool ** i30 |-> bool ** i32) -> 271 bool) -> 272 ((bool ** i4 |-> bool ** i32) # (bool ** i30 |-> bool ** i32) -> 'a) 273 -> 274 ((bool ** i4 |-> bool ** i32) # (bool ** i30 |-> bool ** i32) -> 'b) 275 # 276 ('b -> 'c) # 277 ((bool ** i4 |-> bool ** i32) # (bool ** i30 |-> bool ** i32) -> 'c) 278 -> bool`; 279 280 281fun mk_PSPEC ir (pre_st,post_st) (ins,outs) = 282 let 283 284 fun calculate_outs st (IRSyntax.PAIR (a,b)) = 285 mk_pair (calculate_outs st a, calculate_outs st b) 286 | calculate_outs st exp = 287 read_one_var st exp 288 289 290 (* the characteristic function *) 291 val rules = mk_subst_rules (List.map (read_one_var pre_st) (IRSyntax.pair2list ins)); 292 val (initV,out_vars) = (mk_vars ins, mk_vars outs); 293 val f_c = mk_pabs (initV, subst rules (calculate_outs post_st outs)); (* the charateristic function *) 294 295 (* the pre-condition and the post-condition *) 296 297 val st' = mk_var ("st", Type `:DSTATE`); 298 299 (* the stack function *) 300 val stk_f = mk_pabs (st', Term `T`); 301 val stk_tp = hd (tl (#2 (dest_type (type_of stk_f)))); 302 303 (* the projective specification *) 304 val (in_f,out_f) = (mk_pabs (st', mk_mreads st' ins), mk_pabs (st', mk_mreads st' outs)); 305 val pspec = list_mk_comb (inst [{redex = alpha, residue = stk_tp}, 306 {redex = beta, residue = type_of initV}, 307 {redex = gamma, residue = type_of out_vars}] (PSPEC_term), 308 [ir, mk_pair(stk_f, stk_f), stk_f, list_mk_pair[in_f,f_c,out_f]]); 309 in 310 pspec 311 end; 312 313(*---------------------------------------------------------------------------------*) 314(* Symbolic Simulation of Basic Blocks *) 315(*---------------------------------------------------------------------------------*) 316 317(* Given an basic block, the charateristic function on inputs and outputs are derived by symbolic simulation *) 318(* and the context about unchanged variables is maintained *) 319(* Finally well_formed information is given *) 320(* 321fun extract (annotatedIR.BLK (instL,{ins = ins, outs = outs, context = context, ...})) = 322(instL, ins, outs, context); 323val (instL, ins, outs, context) = extract f_ir; 324val (unchanged_list, _) = unchanged_lists_weak 325val unchanged_list = #2 unchanged_lists 326mk_blk_spec pre_ir unchanged_lists_weak 327 328*) 329 330 331 332fun mk_blk_spec (annotatedIR.BLK (instL,{ins = ins, outs = outs, context = context, ...})) (unchanged_list, _) = 333 let 334 val th = sim_stms instL; 335 val t1 = concl th; 336 val spec_terms = (#2 (strip_comb (lhs t1)), rhs t1); 337 val blk_ir = el 1 (#1 spec_terms); 338 val pre_st = el 2 (#1 spec_terms); 339 val post_st = #2 spec_terms; 340 val ir_abbr = mk_var ("ir", Type `:CTL_STRUCTURE`); 341 342 val f_spec = mk_PSPEC blk_ir (pre_st,post_st) (ins,outs); 343 val f_spec' = subst [{redex = blk_ir, residue = ir_abbr}] f_spec; 344 345 val unchanged_spec = list_mk_comb (Term`UNCHANGED`, [unchanged_list, ir_abbr]); 346 val unchanged_term = list_mk_comb (Term`UNCHANGED`, [unchanged_list, blk_ir]); 347 348 val unchanged_thm = prove (unchanged_term, (* set_goal ([],unchanged_term) *) 349 REWRITE_TAC[UNCHANGED_THM, th, EVERY_DEF] THEN 350 BETA_TAC THEN 351 REWRITE_TAC[read_thm, toREG_def, index_of_reg_def, FAPPLY_FUPDATE_THM, word4_distinct]); 352 353 (* well_formedness *) 354 val wf_spec = mk_comb (Term`WELL_FORMED`, ir_abbr); 355 356 (* specifiction of functional correctness *) 357 val fspec = mk_let (mk_abs (ir_abbr, list_mk_conj [f_spec', wf_spec, unchanged_spec]), blk_ir); 358 359 val spec = prove (fspec, (* set_goal ([],fspec) *) 360 SIMP_TAC std_ss [LET_THM, PSPEC_def, HSPEC_def, FORALL_DSTATE, BLOCK_IS_WELL_FORMED, read_thm, unchanged_thm] THEN 361 SIMP_TAC list_ss [mread_def, toMEM_def, toREG_def, index_of_reg_def, read_thm, th] THEN 362 CONV_TAC SIM_MEM_CONV THEN 363 SIMP_TAC std_ss [pair_induction] 364 ) 365 366 in 367 (spec, th) 368 end 369 | mk_blk_spec _ _ = 370 raise Fail "mk_blk_spec: BLK is expected!"; 371 372 373 374(* Obtain the specification associated with pointers *) 375fun get_p_spec spec = 376 let 377 val th0 = CONJUNCT1 (SIMP_RULE std_ss [LET_THM] spec); 378 val (t0,t1) = strip_comb (concl th0) 379 in 380 List.nth (t1,1) 381 end 382 383 384(*---------------------------------------------------------------------------------*) 385(* Specification for Sequential Composition *) 386(*---------------------------------------------------------------------------------*) 387 388(* retrieve information from a PSPEC specification *) 389fun get_spec_info spec = 390 let val f_spec = hd (strip_conj spec); 391 val (_, [ir, ps, stk_f, fs]) = strip_comb f_spec; 392 val (ps1,ps2) = dest_pair ps; 393 val list0 = strip_pair fs; 394 val (in_f, f_c, out_f) = (#2 (dest_abs (hd list0)), List.nth(list0,1), #2 (dest_abs (List.nth(list0,2)))) 395 in 396 (ir, (ps1, ps2), stk_f, (in_f, f_c, out_f)) 397 end 398 handle e => (print "get_spec_info: the input is not valid PSPEC and UNCHANGED"; Raise e); 399 400 401 402fun mk_sc_spec ir1_spec ir2_spec = 403 let 404 val (specL1,specL2) = (strip_conj (concl (SIMP_RULE std_ss [LET_THM] ir1_spec)),strip_conj (concl (SIMP_RULE std_ss [LET_THM] ir2_spec))); 405 val (ir1,(pre_p1,post_p1),stk_f,(ins1,f1,outs1)) = get_spec_info (hd specL1); 406 val (ir2,(pre_p2,post_p2),stk_f,(ins2,f2,outs2)) = get_spec_info (hd specL2); 407 val (spec1_thm, spec2_thm) = (SIMP_RULE std_ss [LET_THM] ir1_spec, SIMP_RULE std_ss [LET_THM] ir2_spec); 408 409 (* SC (ir1, ir2) *) 410 val sc_ir = list_mk_comb (Term`IL$SC`, [ir1, ir2]); 411 val ir_abbr = mk_var ("ir", Type `:CTL_STRUCTURE`); 412 val st = mk_var ("st", Type `:DSTATE`); 413 val instance = list_mk_comb (Term`run_ir:CTL_STRUCTURE -> DSTATE -> DSTATE`, [sc_ir, st]); 414 415 (* the characteristic function of SC *) 416 val sc_f = combinSyntax.mk_o (f2,f1); 417 val (in_f,out_f) = (mk_pabs (st,ins1), mk_abs (st,outs2)); 418 val out_f1 = mk_pabs (st, outs1); 419 val stk_tp = hd (tl (#2 (dest_type (type_of stk_f)))); 420 421 (* the SC specification *) 422 val f_spec = list_mk_comb (inst [alpha |-> stk_tp, beta |-> type_of ins1, gamma |-> type_of outs2] (PSPEC_term), 423 [sc_ir, mk_pair(pre_p1, post_p2), stk_f, list_mk_pair[in_f,sc_f,out_f]]); 424 425 val f_th = prove (f_spec, (* set_goal ([],f_spec) *) 426 MATCH_MP_TAC PRJ_SC_RULE THEN 427 EXISTS_TAC post_p1 THEN EXISTS_TAC out_f1 THEN 428 SIMP_TAC std_ss [spec1_thm, spec2_thm] 429 ) 430 431 val well_formed_spec = mk_comb (Term`WELL_FORMED`, sc_ir); 432 val well_formed_th = prove (well_formed_spec, (* set_goal ([],well_formed_spec) *) 433 ONCE_REWRITE_TAC [GSYM IR_SC_IS_WELL_FORMED] THEN 434 SIMP_TAC std_ss [spec1_thm, spec2_thm] 435 ); 436 437 438 val unchanged_spec = mk_comb(rator (el 3 specL1), sc_ir); 439 val unchanged_th = prove (unchanged_spec, (* set_goal ([],unchanged_spec) *) 440 MATCH_MP_TAC IR_SC_UNCHANGED THEN 441 REWRITE_TAC [well_formed_th, spec1_thm, spec2_thm] 442 ); 443 444 val spec = subst [sc_ir |-> ir_abbr] (list_mk_conj [f_spec, well_formed_spec, unchanged_spec]); 445 val spec' = mk_let (mk_abs (ir_abbr, spec), sc_ir); 446 447 val th = prove (spec', (* set_goal ([],spec') *) 448 SIMP_TAC std_ss [LET_THM, f_th, well_formed_th, unchanged_th] 449 ) 450 in 451 th 452 end; 453 454(*---------------------------------------------------------------------------------*) 455(* Specification for Function Calls *) 456(*---------------------------------------------------------------------------------*) 457 458fun compute_outL modifiedRegL = 459 let val i = ref 0 460 in 461 List.map (fn e => (i := !i - 1; IRSyntax.MEM (11, !i))) ([12, 11] @ (List.rev modifiedRegL)) (* neglect pc and lr *) 462 end 463 464fun mk_fc_spec (pre_spec, body_spec, post_spec, pre_th, body_th, post_th, unchanged_list) = 465 let 466 val sc1_spec = (mk_sc_spec pre_spec body_spec); 467 val sc2_spec = (mk_sc_spec sc1_spec post_spec); 468 469(* 470 val specL = CONJ_LIST 3 (SIMP_RULE std_ss [LET_THM] sc2_spec); 471 472 val fc_ir = rand (concl sc2_spec); 473 val unchanged_spec = mk_comb(mk_comb (Term`UNCHANGED`, unchanged_list), fc_ir); 474 val unchanged_th = prove (unchanged_spec, set_goal ([],unchanged_spec) 475 SIMP_TAC std_ss [UNCHANGED_def] THEN 476 Cases_on `st` THEN 477 SIMP_TAC std_ss [Once IR_SEMANTICS_SC, Once IR_SEMANTICS_SC, el 2 specL, WELL_FORMED_thm, pre_th, body_th, post_th] THEN 478 CONV_TAC SIM_REWRITE_CONV THEN 479 SIMP_TAC arith_ss [word4_distinct, ADDR30_ADD_CONST_MOD, GSYM WORD_ADD_ASSOC, WORD_EQ_ADD_LCANCEL] THEN 480 WORDS_TAC THEN 481 SIMP_TAC std_ss [word_extract_thm, WORD_ADD_0, IN_INSERT, NOT_IN_EMPTY, DISJ_IMP_THM, index_of_reg_def] 482 );*) 483 in 484 sc2_spec 485 end; 486 487(*---------------------------------------------------------------------------------*) 488(* Specification for input/output matching *) 489(*---------------------------------------------------------------------------------*) 490 491(* 492PROJ_POST_RULE 493 |- !ir in_f out_f convert_f. 494 PSPEC ir (pre_p,post_p) (in_f,f,out_f) ==> 495 PSPEC ir (pre_p,post_p) (in_f,convert_f o f,convert_f o out_f) : thm 496 497 498fun mk_match_spec spec in_f2 = 499 let 500 501 val (_, (pre_p1, post_p1), (in_f1, f_c, out_f1), _) = get_spec_info spec; 502 503 504 in 505 th 506 end; 507*) 508 509 510 511(*---------------------------------------------------------------------------------*) 512(* Specification for Tail Recursion *) 513(*---------------------------------------------------------------------------------*) 514 515(* Given a TR, the charateristic function on inputs and outputs are derived by the TR_RULE *) 516(* and the context about unchanged variables is maintained *) 517 518fun convert_cond (exp1, rop, exp2) = 519 let 520 val cond_t0 = list_mk_pair [IRSyntax.convert_reg exp1, 521 IRSyntax.convert_rop rop, 522 IRSyntax.convert_exp exp2]; 523 in 524 cond_t0 525 end 526 handle e => (print "mk_cond: errors occur while converting the condition"; Raise e); 527 528fun strip_pair2 t = 529 if is_pair t then List.foldl (fn (t0,L0) => L0 @ (strip_pair2 t0)) [] (strip_pair t) 530 else [t]; 531 532fun mk_cj_cond cond_t ins = 533 let 534 val st = mk_var ("st", Type `:DSTATE`); 535 val instance = list_mk_comb (Term`eval_il_cond`, [cond_t, st]); 536 537 val read_const_th = prove (Term`!st v. read st (WCONST v) = v`, SIMP_TAC std_ss [FORALL_DSTATE, read_thm]); 538 539 val th0 = REWRITE_CONV [ARMCompositionTheory.eval_cond_def, 540 ILTheory.eval_il_cond_def, 541 ILTheory.translate_condition_def, 542 ILTheory.toREG_def, 543 ILTheory.toEXP_def, 544 ILTheory.index_of_reg_def] instance; 545 val th1 = REWRITE_RULE [read_const_th] th0; 546 val th1 = WORDS_RULE th1; 547 val instance1 = rhs (concl th1); 548 549 val rules = mk_subst_rules (List.map (fn t0 => rhs (concl (REWRITE_CONV [mread_def, toMEM_def, toREG_def, index_of_reg_def] t0))) (strip_pair2 ins)); 550 val cj_cond = subst rules instance1 (* the condition function *) 551 in 552 cj_cond 553 end 554 555fun mk_cond_f cond_t ins = (* the condition function *) 556 let 557 val rules = mk_subst_rules (strip_pair2 ins) 558 in 559 mk_pabs (subst rules ins, mk_cj_cond cond_t ins) 560 end 561 562fun guessR2 tp = 563 let val tp1 = List.nth(#2 (dest_type tp),1) 564 in 565 (Term`(measure (w2n o FST)):(word32#word32)->(word32#word32)->bool`) 566 end 567 568fun cheat_tac (asl,g) = ACCEPT_TAC(ASSUME g) (asl,g); 569 570fun mk_tr_spec cond body_spec = 571 let 572 val specL = strip_conj (concl (SIMP_RULE std_ss [LET_THM] body_spec)); 573 val (body_ir,(pre_p,post_p),stk_f,(ins,f,outs)) = get_spec_info (hd specL); 574 575 val t_cond = convert_cond cond; 576 val tr_ir = list_mk_comb (Term`TR`, [t_cond, body_ir]); 577 val ir_abbr = mk_var ("ir", Type `:CTL_STRUCTURE`); 578 val st = mk_var ("st", Type `:DSTATE`); 579 val instance = list_mk_comb (Term`run_ir:CTL_STRUCTURE -> DSTATE -> DSTATE`, [tr_ir, st]); 580 581 val initV = #1 (dest_pabs f); 582 583 val cond_f_0 = mk_cond_f t_cond ins; 584 val cond_f = combinSyntax.mk_o (Term `$~:bool->bool`, cond_f_0); 585 586 val tr_f = list_mk_comb (inst [alpha |-> type_of initV] (Term`WHILE:('a -> bool) -> ('a -> 'a) -> 'a -> 'a`), [cond_f, f]); 587 val prj_f = mk_pabs (st,ins); 588 val stk_tp = hd (tl (#2 (dest_type (type_of stk_f)))); 589 590 (* well_founded relation: WF (\st1 st0. ~eval_cond cond st0 /\ (st1 = run_ir ir st0)) *) 591 592 val (st0,st1) = (mk_var ("st0", Type `:DSTATE`), mk_var ("st1", Type `:DSTATE`)); 593 val wf_t0 = mk_neg (list_mk_comb (Term`eval_il_cond`, [t_cond, st0])); 594 val wf_t1 = mk_eq (st1, list_mk_comb (Term`run_ir`, [body_ir, st0])); 595 val wf_t2 = list_mk_abs ([st1,st0],mk_conj(wf_t0,wf_t1)); 596 val wf_t3 = mk_comb (Term`WF:(DSTATE->DSTATE->bool)->bool`, wf_t2); 597 val wf_th = prove (wf_t3, (* set_goal ([],wf_t3) *) 598 MATCH_MP_TAC (INST_TYPE [alpha |-> type_of initV] WF_TR_LEM_2) THEN 599 EXISTS_TAC prj_f THEN EXISTS_TAC f THEN EXISTS_TAC cond_f_0 THEN 600 SIMP_TAC std_ss [SIMP_RULE std_ss [PSPEC_def, HSPEC_def, LET_THM] body_spec] THEN 601 SIMP_TAC std_ss [ARMCompositionTheory.eval_cond_def, FORALL_DSTATE, mread_def, 602 eval_il_cond_def, translate_condition_def, toEXP_def, 603 index_of_reg_def,toREG_def, toMEM_def, read_thm] THEN 604 WORDS_TAC THEN 605 SIMP_TAC std_ss [] THEN 606 MATCH_MP_TAC (INST_TYPE [alpha |-> type_of initV] WF_TR_LEM_3) THEN 607 (let val r = guessR2 (type_of initV) in 608 WF_REL_TAC `^r` THEN 609 WORDS_TAC THEN 610 RW_TAC std_ss [WORDS_RULE 611 (INST_TYPE [alpha |-> Type `:i32`] WORD_PRED_THM)] 612 end 613 handle e => (print "fail to prove totalness, add statement into assumption list"; cheat_tac) 614 ) 615 ); 616 (* the characteristic function *) 617 val f_spec = list_mk_comb (inst [alpha |-> stk_tp, beta |-> type_of initV, gamma |-> type_of initV] (PSPEC_term), 618 [tr_ir, mk_pair(pre_p, post_p), stk_f, list_mk_pair[prj_f,tr_f, prj_f]]); 619 620 val f_th = prove (f_spec, (* set_goal ([],f_spec) *) 621 ASSUME_TAC wf_th THEN 622 MATCH_MP_TAC PRJ_TR_RULE THEN 623 SIMP_TAC std_ss [SIMP_RULE std_ss [LET_THM] body_spec] THEN 624 STRIP_TAC THENL [ 625 RW_TAC std_ss [], 626 SIMP_TAC std_ss [ARMCompositionTheory.eval_cond_def, FORALL_DSTATE, mread_def, eval_il_cond_def, translate_condition_def, 627 index_of_reg_def, toREG_def, toEXP_def, toMEM_def, read_thm] THEN 628 WORDS_TAC THEN 629 SIMP_TAC std_ss [] 630 ] 631 ) 632 633 (* Well-formedness *) 634 635 val well_formed_spec = mk_comb (Term`WELL_FORMED`, tr_ir); 636 val well_formed_th = prove (well_formed_spec, (* set_goal ([],well_formed_spec) *) 637 ASSUME_TAC wf_th THEN 638 MATCH_MP_TAC WELL_FORMED_TR_RULE THEN 639 SIMP_TAC std_ss [SIMP_RULE std_ss [LET_THM] body_spec] THEN 640 RW_TAC std_ss [] 641 ); 642 643 (* unchanged *) 644 val unchanged_spec = mk_comb (rator (el 3 specL), tr_ir); 645 val unchanged_th = prove (unchanged_spec, (* set_goal ([],unchanged_spec) *) 646 MATCH_MP_TAC UNCHANGED_TR_RULE THEN 647 SIMP_TAC std_ss [well_formed_th, SIMP_RULE std_ss [LET_THM] body_spec] 648 ); 649 650 651 val spec = subst [tr_ir |-> ir_abbr] (list_mk_conj [f_spec, well_formed_spec, unchanged_spec]); 652 val spec' = mk_let (mk_abs (ir_abbr, spec), tr_ir); 653 654 val th = prove (spec', (* set_goal ([],spec') *) 655 SIMP_TAC std_ss [f_th, well_formed_th, unchanged_th, LET_THM] 656 ) 657 in 658 th 659 end; 660 661 662(*---------------------------------------------------------------------------------*) 663(* Specification for Conditional Jumps *) 664(*---------------------------------------------------------------------------------*) 665fun mk_cj_spec cond ir1_spec ir2_spec = 666 let 667 val (specL1,specL2) = (strip_conj (concl (SIMP_RULE std_ss [LET_THM] ir1_spec)),strip_conj (concl (SIMP_RULE std_ss [LET_THM] ir2_spec))); 668 val (ir1,(pre_p1,post_p1),stk_f,(ins1,f1,outs1)) = get_spec_info (hd specL1); 669 val (ir2,(pre_p2,post_p2),stk_f,(ins2,f2,outs2)) = get_spec_info (hd specL2); 670 val (spec1_thm, spec2_thm) = (SIMP_RULE std_ss [LET_THM] ir1_spec, SIMP_RULE std_ss [LET_THM] ir2_spec); 671 672 val t_cond = convert_cond cond; 673 val cj_ir = list_mk_comb (Term`CJ`, [t_cond, ir1, ir2]); 674 val ir_abbr = mk_var ("ir", Type `:CTL_STRUCTURE`); 675 val st = mk_var ("st", Type `:DSTATE`); 676 val instance = list_mk_comb (Term`run_ir:CTL_STRUCTURE -> DSTATE -> DSTATE`, [cj_ir, st]); 677 678 val initV = #1 (dest_pabs f1); 679 val cj_cond = mk_pabs(initV, mk_cj_cond t_cond ins1); 680 val cj_f = mk_pabs(initV, list_mk_comb (inst [alpha |-> type_of outs1] (Term`COND:bool->'a->'a->'a`), 681 [mk_comb(cj_cond,initV), mk_comb(f1,initV), mk_comb(f2,initV)])); 682 683 val (in_f,out_f) = (mk_pabs (st,ins1), mk_abs (st,outs2)); 684 val stk_tp = hd (tl (#2 (dest_type (type_of stk_f)))); 685 686 (* the characteristic function *) 687 val f_spec = list_mk_comb (inst [alpha |-> stk_tp, beta |-> type_of ins1, gamma |-> type_of outs2] (PSPEC_term), 688 [cj_ir, mk_pair(pre_p1,post_p1), stk_f, list_mk_pair[in_f,cj_f,out_f]]); 689 690 val f_th = prove (f_spec, (* set_goal ([],f_spec) *) 691 MATCH_MP_TAC (GEN_ALL (SIMP_RULE std_ss [LAMBDA_PROD] (INST_TYPE [beta |-> type_of initV] 692 (SPEC_ALL PRJ_CJ_RULE)))) THEN 693 SIMP_TAC std_ss [spec1_thm, spec2_thm] THEN 694 SIMP_TAC std_ss [ARMCompositionTheory.eval_cond_def, 695 ILTheory.eval_il_cond_def, 696 ILTheory.translate_condition_def, 697 FORALL_DSTATE, mread_def, 698 index_of_reg_def, toREG_def, 699 toEXP_def, read_thm, GSYM PFORALL_THM] THEN 700 WORDS_TAC THEN 701 SIMP_TAC std_ss [] 702 ) 703 704 (* well-formedness *) 705 706 val well_formed_spec = mk_comb (Term`WELL_FORMED`, cj_ir); 707 val well_formed_th = prove (well_formed_spec, (* set_goal ([],well_formed_spec) *) 708 REWRITE_TAC [GSYM IR_CJ_IS_WELL_FORMED] THEN 709 SIMP_TAC std_ss [spec1_thm, spec2_thm] 710 ); 711 712 (* unchanged *) 713 val unchanged_spec = mk_comb (rator (el 3 specL1), cj_ir); 714 val unchanged_th = prove (unchanged_spec, (* set_goal ([],unchanged_spec) *) 715 MATCH_MP_TAC IR_CJ_UNCHANGED THEN 716 SIMP_TAC std_ss [spec1_thm, spec2_thm] 717 ); 718 719 720 val spec = list_mk_conj [f_spec, well_formed_spec, unchanged_spec]; 721 722 val th = prove (spec, (* set_goal ([],spec) *) 723 SIMP_TAC std_ss [f_th, well_formed_th, unchanged_th, LET_THM] 724 ) 725 in 726 th 727 end; 728 729 730(*---------------------------------------------------------------------------------*) 731(* Application of the SHUFFLE rule *) 732(*---------------------------------------------------------------------------------*) 733 734fun mk_shuffle_spec spec (in_f', g) = 735 let 736 val spec_thm = SIMP_RULE std_ss [LET_THM] spec; 737 val (ir,(pre_p,post_p),stk_f,(ins,f,outs)) = get_spec_info (hd (strip_conj (concl spec_thm))); 738 val st = mk_var ("st", Type `:DSTATE`); 739 val (in_f,out_f) = (mk_pabs(st,ins), mk_pabs(st,outs)); 740 741 (* (g o in_f' = f o in_f) *) 742 val (g_tp,f_tp) = (#2 (dest_type (type_of g)), #2 (dest_type (type_of f))); 743 val g_com = list_mk_comb (inst [alpha |-> hd g_tp, beta |-> hd (tl g_tp), gamma |-> Type`:DSTATE`] (Term`$o`), [g,in_f']); 744 val f_com = list_mk_comb (inst [alpha |-> hd f_tp, beta |-> hd (tl f_tp), gamma |-> Type`:DSTATE`] (Term`$o`), [f,in_f]); 745 val shuffle_th = prove (mk_eq(g_com,f_com), (* set_goal ([],(mk_eq(g_com,f_com))) *) 746 SIMP_TAC std_ss [FUN_EQ_THM, FORALL_DSTATE, LET_THM, read_thm] THEN 747 SIMP_TAC list_ss [mread_def, toMEM_def, toREG_def, index_of_reg_def, read_thm] THEN 748 WORDS_TAC THEN 749 SIMP_TAC std_ss [pair_induction] 750 ); 751 752 val fspec = subst [f |-> g, in_f |-> in_f'] (concl spec_thm); 753 754 val spec = prove (fspec, (* set_goal ([],fspec) *) 755 SIMP_TAC std_ss [spec_thm] THEN 756 MATCH_MP_TAC PRJ_SHUFFLE_RULE2 THEN 757 EXISTS_TAC in_f' THEN EXISTS_TAC g THEN 758 RW_TAC std_ss [spec_thm, shuffle_th] 759 ) 760 in 761 spec 762 end; 763 764(*---------------------------------------------------------------------------------*) 765(* Application of the PUSH rule *) 766(*---------------------------------------------------------------------------------*) 767 768fun mk_push_spec spec = 769 let 770 val spec_thm = SIMP_RULE std_ss [LET_THM] spec; 771 val (ir,(pre_p,post_p),stk_f,(ins,f,outs)) = get_spec_info (hd (strip_conj (concl spec_thm))); 772 val st = mk_var ("st", Type `:DSTATE`); 773 val (in_f,out_f) = (mk_pabs(st,ins), mk_pabs(st,outs)); 774 val (g,in_f') = (f,in_f); 775 776 (* (g o in_f' = f o in_f) *) 777 val (g_tp,f_tp) = (#2 (dest_type (type_of g)), #2 (dest_type (type_of f))); 778 val g_com = list_mk_comb (inst [alpha |-> hd g_tp, beta |-> hd (tl g_tp), gamma |-> Type`:DSTATE`] (Term`$o`), [g,in_f']); 779 val f_com = list_mk_comb (inst [alpha |-> hd f_tp, beta |-> hd (tl f_tp), gamma |-> Type`:DSTATE`] (Term`$o`), [f,in_f]); 780 val push_th = prove (mk_eq(g_com,f_com), (* set_goal ([],(mk_eq(g_com,f_com))) *) 781 SIMP_TAC std_ss [FUN_EQ_THM, FORALL_DSTATE, LET_THM, read_thm] THEN 782 SIMP_TAC list_ss [mread_def, toMEM_def, toREG_def, index_of_reg_def, read_thm] THEN 783 WORDS_TAC THEN 784 SIMP_TAC std_ss [pair_induction] 785 ); 786 787 val fspec = subst [f |-> g, in_f |-> in_f'] (concl spec_thm); 788 789 val spec = prove (fspec, (* set_goal ([],fspec) *) 790 SIMP_TAC std_ss [spec_thm] THEN 791 MATCH_MP_TAC PRJ_PUSH_RULE THEN 792 EXISTS_TAC in_f' THEN EXISTS_TAC g THEN 793 RW_TAC std_ss [spec_thm, push_th] 794 ) 795 in 796 spec 797 end; 798 799(*---------------------------------------------------------------------------------*) 800(* Application of the POP rule *) 801(*---------------------------------------------------------------------------------*) 802 803fun mk_pop_spec spec = 804 let 805 val spec_thm = SIMP_RULE std_ss [LET_THM] spec; 806 val (ir,(pre_p,post_p),stk_f,(ins,f,outs)) = get_spec_info (hd (strip_conj (concl spec_thm))); 807 val st = mk_var ("st", Type `:DSTATE`); 808 val (in_f,out_f) = (mk_pabs(st,ins), mk_pabs(st,outs)); 809 val (g,in_f') = (f,in_f); 810 811 (* (g o in_f' = f o in_f) *) 812 val (g_tp,f_tp) = (#2 (dest_type (type_of g)), #2 (dest_type (type_of f))); 813 val g_com = list_mk_comb (inst [alpha |-> hd g_tp, beta |-> hd (tl g_tp), gamma |-> Type`:DSTATE`] (Term`$o`), [g,in_f']); 814 val f_com = list_mk_comb (inst [alpha |-> hd f_tp, beta |-> hd (tl f_tp), gamma |-> Type`:DSTATE`] (Term`$o`), [f,in_f]); 815 val pop_th = prove (mk_eq(g_com,f_com), (* set_goal ([],(mk_eq(g_com,f_com))) *) 816 SIMP_TAC std_ss [FUN_EQ_THM, FORALL_DSTATE, LET_THM, read_thm] THEN 817 SIMP_TAC list_ss [mread_def, toMEM_def, toREG_def, index_of_reg_def, read_thm] THEN 818 WORDS_TAC THEN 819 SIMP_TAC std_ss [pair_induction] 820 ); 821 822 val fspec = subst [f |-> g, in_f |-> in_f'] (concl spec_thm); 823 824 val spec = prove (fspec, (* set_goal ([],fspec) *) 825 SIMP_TAC std_ss [spec_thm] THEN 826 MATCH_MP_TAC PRJ_POP_RULE THEN 827 EXISTS_TAC in_f' THEN EXISTS_TAC g THEN 828 RW_TAC std_ss [spec_thm, pop_th] 829 ) 830 in 831 spec 832 end; 833 834 835(*---------------------------------------------------------------------------------*) 836(* Forward Reasoning *) 837(*---------------------------------------------------------------------------------*) 838 839(* 840fun extract (annotatedIR.SC (ir1, ir2, info)) = (ir1, ir2, info); 841val (ir1, ir2, info) = extract f_ir; 842 843fun extract (annotatedIR.CALL (fname, pre_ir, body_ir, post_ir, info)) = (fname, pre_ir, body_ir, post_ir, info); 844val (fname, pre_ir, body_ir, post_ir, info) = extract ir1; 845 846fun extract (annotatedIR.SC (ir1, ir2, info)) = (ir1, ir2, info); 847 848fun extract (annotatedIR.TR (cond, body, {fspec = fspec1, ins = ins1, outs = outs1, context = contextL, ...})) = (cond, body) 849val (cond, body) = extract ir2 850 851fun extract (annotatedIR.CJ (cond, ir1, ir2, {fspec = fspec1, ins = ins1, outs = outs1, context = contextL, ...})) = (cond, ir1, ir2) 852val (cond, ir1, ir2) = extract f_ir 853*) 854 855 856fun fwd_reason (annotatedIR.BLK blk_ir) unchanged_lists = 857 #1 (mk_blk_spec (annotatedIR.BLK blk_ir) unchanged_lists) 858 859 | fwd_reason (annotatedIR.SC (ir1, ir2, info)) unchanged_lists = 860 let val spec1 = fwd_reason ir1 unchanged_lists; 861 val spec2 = fwd_reason ir2 unchanged_lists; 862 in 863 mk_sc_spec spec1 spec2 864 end 865 866 | fwd_reason (annotatedIR.TR (cond, body, {fspec = fspec1, ins = ins1, outs = outs1, context = contextL, ...})) unchanged_lists = 867 let val body_spec = fwd_reason body unchanged_lists 868 in 869 mk_tr_spec cond body_spec 870 end 871 872 | fwd_reason (annotatedIR.CJ (cond, ir1, ir2, {fspec = fspec1, ins = ins1, outs = outs1, context = contextL, ...})) unchanged_lists = 873 mk_cj_spec cond (fwd_reason ir1 unchanged_lists) (fwd_reason ir2 unchanged_lists) 874 875 | fwd_reason (annotatedIR.CALL (fname, pre_ir, body_ir, post_ir, info)) unchanged_lists = 876 let 877 val unchanged_lists_weak = (#2 unchanged_lists, #2 unchanged_lists); 878 val (pre_spec, pre_th) = mk_blk_spec pre_ir unchanged_lists_weak; 879 val (body_spec, body_th) = mk_blk_spec body_ir unchanged_lists_weak; 880 val (post_spec, post_th) = mk_blk_spec post_ir unchanged_lists_weak; 881 in 882 mk_fc_spec (pre_spec, body_spec, post_spec, pre_th, body_th, post_th, (#1 unchanged_lists)) 883 end 884 885 | fwd_reason _ _ = 886 raise Fail "fwd_reason: unsupported IR strcuture" 887 ; 888 889(*---------------------------------------------------------------------------------*) 890(* Equivalence between the original function and the spec function *) 891(*---------------------------------------------------------------------------------*) 892fun restore_f_TAC defs = 893 SIMP_TAC std_ss [FUN_EQ_THM, FORALL_PROD] THEN 894 REPEAT GEN_TAC THEN 895 896 SIMP_TAC std_ss defs THEN 897 REPEAT (CHANGED_TAC (FIRST [CHANGED_TAC (SIMP_TAC std_ss ([LET_THM, WORD_ADD_ASSOC] @ defs)), WORDS_TAC])) THEN 898 REPEAT (CHANGED_TAC (FIRST [CHANGED_TAC (SIMP_TAC std_ss ([LET_THM, GSYM WORD_ADD_ASSOC] @ defs)), WORDS_TAC])) THEN 899 METIS_TAC[WORD_ADD_COMM, WORD_AND_COMM, WORD_OR_COMM, WORD_XOR_COMM]; 900 901 902fun restore_f spec defs prove_equiv = 903 let 904 val th0 = CONJUNCT1 (SIMP_RULE std_ss [LET_THM] spec); 905 val [in_f,spec_f,out_f] = strip_pair (List.nth (#2 (strip_comb (concl th0)),3)); 906 val sfl_f_const = #1 (strip_comb (lhs ((concl o SPEC_ALL) (hd defs)))); 907 val eq_stat = mk_eq (spec_f, sfl_f_const); 908 val eq_th = if (prove_equiv) then 909 (print "Proving equivalence with input function\n"; 910 prove(eq_stat, restore_f_TAC defs) handle _ => 911 let 912 val _ = print "! Equivalence proof between original function and\n"; 913 val _ = print "! derived program semantics failed!\n\n"; 914 in 915 ASSUME eq_stat 916 end) 917 else ASSUME eq_stat; 918 in 919 eq_th 920 end; 921 922 923(*---------------------------------------------------------------------------------*) 924(* Display the theorem at the level of ARM flat code *) 925(*---------------------------------------------------------------------------------*) 926 927fun f_correct spec = 928 let 929 val th0 = CONJUNCT1 (SIMP_RULE std_ss [LET_THM] spec); 930 val th1 = SIMP_RULE std_ss [PSPEC_def, HSPEC_def, run_ir_def] th0; 931 val f = let val t0 = concl (SPEC_ALL th1) 932 val (assm,f_spec) = 933 let val (assm, t1) = dest_imp t0 934 in (assm,#2 (dest_conj t1)) 935 end handle e => (Term`T`,t0) 936 in 937 mk_imp (assm, f_spec) 938 end 939 val th2 = GEN_ALL (prove (f, SIMP_TAC std_ss [th1])); 940 val th3 = SIMP_RULE std_ss [translate_def, translate_assignment_def, toEXP_def, toREG_def, toMEM_def, index_of_reg_def, translate_condition_def] th2; 941 val th4 = SIMP_RULE list_ss [ARMCompositionTheory.mk_SC_def, ARMCompositionTheory.mk_CJ_def, ARMCompositionTheory.mk_TR_def] th3 942 val th5 = SIMP_RULE std_ss [GSYM proper_def] th4 943 val th6 = WORDS_RULE th5 944 in 945 th6 946 end; 947 948 949fun f_correct_ir spec = 950 let 951 val th0 = CONJUNCT1 (SIMP_RULE std_ss [LET_THM] spec); 952 val th1 = SIMP_RULE std_ss [PSPEC_def, HSPEC_def] th0; 953 val f = let val t0 = concl (SPEC_ALL th1) 954 val (assm,f_spec) = 955 let val (assm, t1) = dest_imp t0 956 in (assm,#2 (dest_conj t1)) 957 end handle e => (Term`T`,t0) 958 in 959 mk_imp (assm, f_spec) 960 end 961 val th2 = GEN_ALL (prove (f, SIMP_TAC std_ss [th1])); 962 val th3 = SIMP_RULE std_ss [toEXP_def, toREG_def, toMEM_def, index_of_reg_def] th2; 963 val th4 = SIMP_RULE list_ss [] th3 964 val th5 = SIMP_RULE std_ss [GSYM proper_def] th4 965 val th6 = WORDS_RULE th5 966 in 967 th6 968 end; 969 970 971(*---------------------------------------------------------------------------------*) 972(* Print out *) 973(*---------------------------------------------------------------------------------*) 974 975(* Extract the IR tree from the specification and print it out *) 976 977fun extract_ir spec = 978 let 979 val (f_name, _, (f_args,f_ir,f_outs), _, _, _) = spec; 980 in 981 (print (" Name : " ^ f_name ^ "\n"); 982 print (" Arguments : " ^ (IRSyntax.format_exp f_args) ^ "\n"); 983 print (" Returns : " ^ (IRSyntax.format_exp f_outs) ^ "\n"); 984 print " Body: \n"; 985 annotatedIR.printIR (annotatedIR.merge_ir f_ir) 986 ) 987 end 988 989(* Extract the ARM instruction list from the specification and print it out *) 990 991fun extract_arm spec = 992 let 993 val (f_name, _, (f_args,_,f_outs), _, stat0, _) = spec; 994 val stat1 = let val t0 = concl (SPEC_ALL stat0) 995 in if is_imp t0 then #2 (dest_imp t0) else t0 996 end 997 val stms = find_term (fn t => type_of t = Type `:INST list`) stat1; 998 val stms1 = preARMSyntax.dest_arm stms 999 in 1000 (print (" Name : " ^ f_name ^ "\n"); 1001 print (" Arguments : " ^ (IRSyntax.format_exp f_args) ^ "\n"); 1002 print (" Returns : " ^ (IRSyntax.format_exp f_outs) ^ "\n"); 1003 print " Body: \n"; 1004 Assem.printInsts stms1 1005 ) 1006 end 1007 1008(*---------------------------------------------------------------------------------*) 1009(* Interface *) 1010(*---------------------------------------------------------------------------------*) 1011 1012(* To make the initial value of fp or sp unspecified, assign it a negative integer *) 1013(* For example, init_fp = ~1 will lead to st<MR R11> = ARB *) 1014 1015(*val init_fp = ref (100);*) 1016val init_sp = ref (~1); 1017 1018fun mk_pre_p sp_v = 1019 if (!init_sp < 0) then mk_pabs (mk_var ("st", Type `:DSTATE`), Term`T`) 1020 else 1021 let val st = mk_pair (mk_var ("regs", Type `:num |-> DATA`), mk_var ("mem", Type `:num |-> DATA`)); 1022 val (fp',sp') = (read_one_var st (IRSyntax.REG 11), read_one_var st (IRSyntax.REG 13)); 1023 fun convert_pt v = if v < 0 then inst [alpha |-> Type `:DATA`] (Term `ARB`) else mk_comb (Term `n2w:num->word32`, term_of_int v) 1024 in mk_pabs (st, mk_conj ( mk_eq(fp', convert_pt (!init_sp)), mk_eq(sp', convert_pt (!init_sp)))) (* Initially fp = sp *) 1025 end; 1026 1027(*---------------------------------------------------------------------------------*) 1028(*Preprocess definition to eliminate ugly constants *) 1029(*---------------------------------------------------------------------------------*) 1030 1031fun wordsplit t = 1032 let 1033 fun term2Arbnum t = 1034 let 1035 val t = mk_comb (Term `w2n:word32->num`, t) 1036 val t = rhs (concl (EVAL t)); 1037 val n = numLib.dest_numeral t; 1038 in 1039 n 1040 end; 1041 1042 fun arbnum2term n = 1043 let 1044 val t = numLib.mk_numeral n; 1045 val t = mk_comb (Term `n2w:num->word32`, t) 1046 val t = rhs (concl (EVAL t)); 1047 in 1048 t 1049 end; 1050 1051 1052 fun remove_zero n c = 1053 let 1054 val (n1, n2) = (Arbnum.divmod (n, Arbnum.fromInt 4)) 1055 in 1056 if (n2 = Arbnum.zero) then 1057 remove_zero n1 (Arbnum.plus1 c) 1058 else 1059 (n, c) 1060 end; 1061 1062 1063 fun wordsplit_internal (n:num) l = 1064 if (n = Arbnum.zero) then 1065 if (l = []) then [n] else l 1066 else 1067 let 1068 val (n_div, n_mod) = remove_zero n Arbnum.zero; 1069 val n' = Arbnum.mod (n_div, Arbnum.fromInt 256); 1070 val n' = Arbnum.* (n', Arbnum.pow (Arbnum.fromInt 4, n_mod)); 1071 val m = Arbnum.- (n, n'); 1072 in 1073 wordsplit_internal m (n'::l) 1074 end; 1075 1076 val l = wordsplit_internal (term2Arbnum t) []; 1077 val l = map arbnum2term l; 1078 in 1079 l 1080 end; 1081 1082fun needs_split t = not (length(wordsplit t) = 1) 1083 1084fun WORD_EVAL_CONV t = 1085 if ((wordsSyntax.is_word_type(type_of t)) andalso (free_vars t = [])) then 1086 (CHANGED_CONV EVAL t) else raise ERR "WORD_EVAL_CONV" "" 1087 1088 1089fun DATA_RESTRICT_CONV t = 1090 if (wordsSyntax.is_n2w t andalso needs_split t) then 1091 let 1092 val l = wordsplit t; 1093 val (h, l) = (hd l, tl l); 1094 val new_t = foldl (fn (x, y) => mk_comb (mk_comb (Term `($!!):word32->word32->word32`, x), y)) h l; 1095 in 1096 GSYM (WORDS_CONV new_t) 1097 end 1098 else raise ERR "DATA_RESTRICT_CONV" "" 1099 1100 1101 1102val extra_defs = ref [DECIDE (Term `T`)]; 1103 1104fun preprocess_def def = 1105 CONV_RULE ((DEPTH_CONV WORD_EVAL_CONV) THENC (DEPTH_CONV DATA_RESTRICT_CONV)) def 1106 1107 1108fun mk_unchanged_term f_name = 1109 let 1110 val {regs=regs,...} = declFuncs.getFunc f_name; 1111 val univ_set = Binaryset.addList (Binaryset.empty Int.compare, [0,1,2,3,4,5,6,7,8,9,10,14]) 1112 val neg_regs = Binaryset.difference(univ_set,regs) 1113 val int_list = Binaryset.listItems neg_regs; 1114 val mreg_list = map (fn n => 1115 let 1116 val n_term = term_of_int n 1117 in 1118 rhs (concl (EVAL (mk_comb (Term `from_reg_index`, n_term)))) 1119 end) int_list; 1120 val changed_list = mk_list (mreg_list, Type `:MREG`); 1121 in 1122 changed_list 1123 end; 1124 1125(*val prog = def2;*) 1126fun pp_compile prog prove_equiv = 1127 let 1128 val def = preprocess_def prog; 1129 val (f_name, f_type, (f_args,f_ir,f_outs), defs) = funCall.link_ir def; 1130 val unchanged_list = mk_unchanged_term f_name; 1131 val unchanged_list_fp_sp = Term `R11 :: R12 :: R13 :: ^unchanged_list`; 1132(* val unchanged_lists = (unchanged_list_fp_sp, unchanged_list);*) 1133 val unchanged_lists = (unchanged_list_fp_sp, unchanged_list); 1134 val f_spec0 = fwd_reason f_ir unchanged_lists; 1135 val f_spec1 = (SIMP_RULE std_ss [restore_f f_spec0 defs prove_equiv] f_spec0) 1136 val thm_list = CONJ_LIST 3 (SIMP_RULE std_ss [LET_THM] f_spec1); 1137 val stat = f_correct f_spec1 1138 val stat_ir = f_correct_ir f_spec1 1139 in 1140 (f_name, f_type, (f_args,f_ir,f_outs), defs, stat, stat_ir, el 1 thm_list, el 2 thm_list, el 3 thm_list) 1141 end 1142 1143 1144 1145end 1146end 1147