1(* ========================================================================= *) 2(* FILE : arm_rulesLib.sml *) 3(* DESCRIPTION : Tools for symbolic evaluation of the ARM Instruction Set *) 4(* *) 5(* AUTHORS : (c) Anthony Fox, University of Cambridge *) 6(* DATE : 2006 *) 7(* ========================================================================= *) 8 9structure arm_rulesLib :> arm_rulesLib = 10struct 11 12(* interactive use: 13 app load ["instructionSyntax", "arm_rulesTheory"]; 14*) 15 16open HolKernel boolLib Parse bossLib; 17open Q wordsTheory arm_evalTheory arm_rulesTheory; 18 19(* ------------------------------------------------------------------------- *) 20 21val SIMP_USR = SIMP_RULE bool_ss [armTheory.USER_def]; 22 23val PSR_CONV = 24 SIMP_CONV pure_ss 25 [SIMP_USR SPSR_READ_THM2,SIMP_USR SPSR_WRITE_THM,SIMP_USR SPSR_WRITE_READ, 26 SPSR_WRITE_WRITE,CPSR_WRITE_READ,CONJUNCT1 CPSR_READ_WRITE,CPSR_WRITE_WRITE, 27 PSR_WRITE_COMM,SPSR_READ_WRITE,armTheory.mode_distinct,SET_NZCV_ID, 28 DECODE_IFMODE_SET_NZCV,DECODE_NZCV_SET_NZCV, 29 DECODE_IFMODE_SET_IFMODE,DECODE_NZCV_SET_IFMODE, 30 SET_NZCV_IDEM,SET_IFMODE_IDEM,SET_IFMODE_NZCV_SWP]; 31 32(* ------------------------------------------------------------------------- *) 33 34val DIMINDEX4 = 35 SIMP_RULE std_ss [dimindex_4,dimword_4] o 36 INST_TYPE [`:'a` |-> `:4`]; 37 38val wrd_ss = std_ss ++ rewrites [DIMINDEX4 word_ls_n2w,DIMINDEX4 n2w_11]; 39 40val REG_WRITE_WRITE_PC = (GEN_ALL o GSYM o SIMP_RULE std_ss [] o 41 INST [`m1` |-> `usr`,`m2` |-> `m`] o DISCH `~(n = 15w)` o 42 SPEC_ALL) REG_WRITE_WRITE_PC; 43 44val REG_WRITE_WRITE_PC2 = (GEN_ALL o SIMP_RULE std_ss [] o 45 INST [`n` |-> `15w`] o SPEC_ALL) REG_WRITE_WRITE_PC; 46 47val REG_WRITEL_PC = GEN_ALL 48 ((SIMP_CONV std_ss [REG_WRITEL_def,TO_WRITE_READ6] THENC 49 REWRITE_CONV [REG_WRITE_WRITEL]) ``REG_WRITEL r m [(15w,d)]``); 50 51val REG_WRITEL_WRITEL_PC = (GEN_ALL o ONCE_REWRITE_RULE [REG_WRITEL_PC] o 52 INST [`l1` |-> `[(15w,d)]`] o SPEC_ALL) REG_WRITEL_WRITEL; 53 54val SORT_REG_WRITEL_CONV = 55 SIMP_CONV wrd_ss [INC_PC,REG_READ_WRITEL_PC2] THENC 56 SIMP_CONV wrd_ss [REG_WRITEL_def,REG_WRITE_WRITE_THM, 57 REG_WRITE_WRITE_PC,REG_WRITE_WRITE_PC2] THENC 58 REWRITE_CONV [listTheory.APPEND,REG_WRITE_WRITEL, 59 REG_WRITEL_WRITEL,REG_WRITEL_WRITEL_PC]; 60 61val REG_READ_WRITEL_CONV = SIMP_CONV std_ss 62 [CONJUNCT1 REG_WRITEL_def,REG_READ_WRITEL,REG_READ_WRITEL_PC, 63 REG_READ_WRITEL_PC2,DIMINDEX4 n2w_11]; 64 65val REG_WRITEL_CONV = SORT_REG_WRITEL_CONV THENC REG_READ_WRITEL_CONV; 66 67(* ------------------------------------------------------------------------- *) 68 69fun mk_abbrev v = mk_comb(``Abbrev``,mk_eq(v,genvar (type_of v))); 70 71val dest_abbrev = dest_eq o snd o dest_comb; 72 73fun is_abbrev_match m t = 74let val v = fst (dest_abbrev m) 75 val rrl = match_term m t 76in 77 null (snd rrl) andalso 78 not (isSome (List.find (fn x => term_eq (#redex x) v) (fst rrl))) 79end; 80 81fun total_is_abbrev_match m t = 82 case total (is_abbrev_match m) t of 83 SOME b => b 84 | _ => false; 85 86fun get_abbrev_match m t = find_term (total_is_abbrev_match m) t; 87 88fun UNABBREV_RULE q thm = 89let val t = concl thm 90 val m = mk_abbrev (parse_in_context (free_vars t) q) 91 val mt = get_abbrev_match m t 92 val (l,r) = dest_abbrev mt 93in 94 SIMP_RULE bool_ss [SPEC `T` markerTheory.Abbrev_def] (Thm.INST [l |-> r] thm) 95end; 96 97fun UNABBREVL_RULE l t = 98 GEN_ALL (foldl (fn (x,t) => UNABBREV_RULE x t) (SPEC_ALL t) l); 99 100(* ------------------------------------------------------------------------- *) 101 102val dest_enc_term = snd o dest_comb o snd o dest_eq; 103 104fun is_enc_term t = type_of (dest_enc_term t) = ``:arm_instruction`` 105 handle HOL_ERR _ => false; 106 107fun MATCH_ARM_RULE m r = GEN_ALL (PART_MATCH 108 (fn t => (dest_enc_term o valOf) 109 (List.find is_enc_term ((strip_conj o fst o dest_imp) t))) r m); 110 111val arm_rules = 112 filter (fn x => substring(fst x, 0, 3) = "ARM") (theorems "arm_rules"); 113 114fun RULE_FIND m l = filter (can (MATCH_ARM_RULE m)) l; 115 116fun RULE_GET m l = filter (fn x => not (term_eq (concl x) T)) 117 (map (SIMP_RULE wrd_ss [] o MATCH_ARM_RULE m) (RULE_FIND m l)); 118 119fun RULE_GET_ARM m = hd (RULE_GET m (map snd arm_rules)); 120 121val GET_ARM = RULE_GET_ARM o instructionSyntax.mk_instruction; 122 123(* ------------------------------------------------------------------------- *) 124 125end 126