1(* ========================================================================= *) 2(* FILE : iclass_compScript.sml *) 3(* DESCRIPTION : Provides theorems for evaluating the models during *) 4(* verification. *) 5(* AUTHOR : (c) Anthony Fox, University of Cambridge *) 6(* DATE : 2005 *) 7(* ========================================================================= *) 8 9(* interactive use: 10 app load ["armTheory", "coreTheory", "lemmasTheory"]; 11*) 12 13open HolKernel boolLib bossLib; 14open Q pairTheory; 15open armTheory coreTheory lemmasTheory; 16 17val _ = new_theory "iclass_comp"; 18 19(* ------------------------------------------------------------------------- *) 20 21val std_ss = std_ss ++ boolSimps.LET_ss; 22 23val classes = [`unexec`,`swp`,`mrs_msr`,`data_proc`,`reg_shift`,`ldr`,`str`, 24 `br`,`swi_ex`,`cdp_und`,`mrc`,`mcr`,`ldc`,`stc`]; 25 26val basic_rws = 27 [FST,SND,LET_THM,UNCURRY_DEF,io_onestepTheory.ADVANCE_def, 28 iseq_distinct,GSYM iseq_distinct]; 29 30val basic_rws2 = basic_rws @ [iclass_EQ_iclass,iclass2num_thm]; 31 32val the_rws = 33 [RP_def,PCWA_def,RWA_def,PIPEBLL_def,BUSA_def,BUSB_def,BORROW_def,COUNT1_def, 34 MUL1_def,MSHIFT,NOPC_def,NMREQ_def,NEWINST_def,NXTIS_def,DIN_def,AREG_def, 35 NBW_def,NRW_def,NBS_def,MASK_def,SCTRLREGWRITE_def,PSRFBWRITE_def, 36 ALUAWRITE_def,ALUBWRITE_def,PSRWA_def]; 37 38val the_rws2 = 39 [ALU6_def,FIELD_def,SHIFTER_def,RAA_def,RBA_def,PSRA_def,PSRDAT_def]; 40 41val SPEC_SIMP = 42 (GEN_ALL o 43 RIGHT_CONV_RULE (SIMP_CONV (std_ss++rewrites basic_rws2) []) o 44 SPEC_ALL); 45 46fun SIMP_SPEC tm = (SPEC_SIMP o SPEC tm); 47fun SIMP_SPECL tm = (SPEC_SIMP o SPECL tm); 48fun map_rws rws ic = map (SIMP_SPEC ic) rws; 49 50val constant_fold_ldm_stm = 51 let val l = map (map_rws ((tl the_rws) @ (tl the_rws2))) [`ldm`,`stm`] in 52 [[SIMP_SPEC `ldm` BASELATCH_def,SIMP_SPECL [`ldm`,`tn`] ALU6_def, 53 SIMP_SPECL [`ldm`,`tm`] ALU6_def] @ (hd l),hd (tl l)] 54 end; 55 56val constant_fold_mul = 57 [(SIMP_SPECL [`mla_mul`,`tn`] ALU6_def) :: map_rws (the_rws @ (tl the_rws2)) 58 `mla_mul`]; 59 60val constant_fold = 61 (map (map_rws the_rws) classes) @ 62 constant_fold_ldm_stm @ 63 constant_fold_mul; 64 65(* Used for ALU evaluation *) 66val constant_fold_alu = 67 [SIMP_SPEC `br` OFFSET_def,SIMP_SPEC `swi_ex` OFFSET_def] @ 68 List.concat (map (map_rws the_rws2) 69 [`swp`,`mrs_msr`,`data_proc`,`reg_shift`,`ldr`,`str`, 70 `br`,`swi_ex`,`mrc`,`ldc`,`stc`]); 71 72val thms = save_thm("iclass_comp_thms", 73 LIST_CONJ (map LIST_CONJ constant_fold)); 74 75val ldm_stm_thms = save_thm("ldm_stm_comp_thms", 76 LIST_CONJ (map LIST_CONJ constant_fold_ldm_stm)); 77 78val mul_thms = save_thm("mul_comp_thms",LIST_CONJ (hd constant_fold_mul)); 79val alu_thms = save_thm("alu_comp_thms",LIST_CONJ constant_fold_alu); 80 81(* ------------------------------------------------------------------------- *) 82 83val _ = export_theory(); 84