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