1structure preARMSyntax =
2struct
3
4local
5  open HolKernel Parse boolLib preARMTheory pairLib
6       numSyntax optionSyntax listSyntax
7in
8
9(*----------------------------------------------------------------------------*)
10(* Create ARM progroms to be used in HOL                                      *)
11(* From ML programs to HOL programs                                           *)
12(*----------------------------------------------------------------------------*)
13
14fun to_exp (Assem.MEM {reg = regNo, offset = offset, wback = flag}) =
15      mk_comb(Term`MEM:(num # OFFSET) -> EXP`,
16                mk_pair(term_of_int regNo,
17                  mk_comb(if offset >= 0 then Term`POS` else Term`NEG`,
18                          term_of_int (abs offset))))
19 |  to_exp (Assem.NCONST e) =
20      mk_comb(Term`NCONST`, mk_numeral (Arbint.toNat e))
21 |  to_exp (Assem.WCONST e) =
22      mk_comb(Term`WCONST`, mk_comb (Term`n2w:num->word32`, mk_numeral (Arbint.toNat e)))
23 |  to_exp (Assem.REG e) =
24      mk_comb(Term`REG`, term_of_int e)
25 |  to_exp (Assem.WREG e) =
26      mk_comb(Term`WREG`, term_of_int e)
27 |  to_exp (Assem.PAIR(e1,e2)) =
28      mk_pair(to_exp e1, to_exp e2)
29 |  to_exp _ =
30      raise ERR "ARM" ("invalid expression")
31
32fun mk_arm (ins,stms,outs) =
33  let
34
35    fun mk_stm (Assem.OPER {oper = (op1, cond1, flag), dst = dlist, src = slist, jump = jumps}) =
36        let
37            val ops = list_mk_pair [ mk_thy_const {Name = Assem.print_op op1, Thy = "preARM", Ty = Type `:OPERATOR`},
38
39                                     (* For instruction BL, jump is always effective; and, when the pc appears in the destination list, then
40                                        a jump occurs                                                                                           *)
41                                     if op1 = Assem.BL orelse not (List.find (fn r => r = Assem.REG 15 orelse r = Assem.WREG 15) dlist = NONE)  then
42                                                Term(`SOME AL:COND option`)         (* always jumps *)
43
44                                     else if cond1 = NONE then mk_none (Type `:COND`)
45                                     else mk_comb(Term`SOME:COND->COND option`,
46                                                   mk_const(Assem.print_cond cond1, Type `:COND`)),
47                                     Term`F`]
48
49            val j1 = case (List.find (fn e => e = Assem.REG 15 orelse e = Assem.WREG 15) dlist) of
50                                (* check whether the pc is in the destination list *)
51                        NONE => (case jumps of
52                                       NONE => mk_none (Type `:OFFSET`)
53                                    |  SOME l =>
54                                                if Symbol.name (hd l) = "+" then
55                                                        mk_some (mk_comb(Term`POS`, term_of_int (Symbol.index (hd l))))
56                                                else mk_some (mk_comb(Term`NEG`, term_of_int (Symbol.index (hd l))))
57                                ) |
58                        SOME l => mk_some (Term`INR`)     (* the pc is modified to be the value in a register *)
59
60            val (slist,dlist) = if op1 = Assem.LDMFD orelse op1 = Assem.STR then (dlist,slist)
61                                else if op1 = Assem.CMP then (slist, [])
62                                else (slist,dlist)
63            val d1 = if length dlist = 0 then
64                        mk_none (Type `:EXP`)
65                     else mk_some (to_exp (hd dlist));
66            val s1 = mk_list (List.map to_exp slist, Type `:EXP`);
67
68        in
69            list_mk_pair [ops,d1,s1,j1]
70        end
71
72   |  mk_stm (Assem.MOVE inst) =
73        list_mk_pair [list_mk_pair [Term`MOV`, Term`NONE : COND option`, Term`F`],
74                      mk_some (to_exp (#dst inst)),
75                      mk_list ([to_exp (#src inst)], Type `:EXP`),
76                      mk_none (Type `:OFFSET`)
77                     ]
78
79    |  mk_stm (Assem.LABEL _) =
80        ( print "Please use link2 to remove the labels first \n";
81          raise ERR "ARM" ("invalid ARM program")
82        )
83
84    fun one_fun (args, stms, outs) =
85        (to_exp args,
86         mk_list(List.map mk_stm stms, Type `:INST`),
87         to_exp outs
88        )
89
90  in
91      one_fun (ins,stms,outs)
92  end
93
94(*----------------------------------------------------------------------------*)
95(* Convert from HOL programs to ML programs                                   *)
96(*----------------------------------------------------------------------------*)
97
98fun from_op operator =
99  if operator = Term `ADD` then Assem.ADD
100  else if operator = Term `SUB:OPERATOR` then Assem.SUB
101  else if operator = Term `RSB:OPERATOR` then Assem.RSB
102  else if operator = Term `MUL:OPERATOR` then Assem.MUL
103  else if operator = Term `MLA:OPERATOR` then Assem.MLA
104  else if operator = Term `AND:OPERATOR` then Assem.AND
105  else if operator = Term `ORR:OPERATOR` then Assem.ORR
106  else if operator = Term `EOR:OPERATOR` then Assem.EOR
107  else if operator = Term `CMP:OPERATOR` then Assem.CMP
108  else if operator = Term `TST:OPERATOR` then Assem.TST
109  else if operator = Term `LSL:OPERATOR` then Assem.LSL
110  else if operator = Term `LSR:OPERATOR` then Assem.LSR
111  else if operator = Term `ASR:OPERATOR` then Assem.ASR
112  else if operator = Term `ROR:OPERATOR` then Assem.ROR
113  else if operator = Term `LDR:OPERATOR` then Assem.LDR
114  else if operator = Term `LDMFD:OPERATOR` then Assem.LDMFD
115  else if operator = Term `STR:OPERATOR` then Assem.STR
116  else if operator = Term `STMFD:OPERATOR` then Assem.STMFD
117  else if operator = Term `MRS:OPERATOR` then Assem.MRS
118  else if operator = Term `MSR:OPERATOR` then Assem.MSR
119  else if operator = Term `BL:OPERATOR` then Assem.BL
120  else if operator = Term `B:OPERATOR` then Assem.B
121  else if operator = Term `SWI:OPERATOR` then Assem.SWI
122  else if operator = Term `NOP:OPERATOR` then Assem.NOP
123  else raise Fail "from_op: invalid ARM operator!"
124
125fun from_cond cond =
126  if cond = Term `SOME EQ` then SOME (Assem.EQ)
127  else if cond = Term `SOME NE` then SOME (Assem.NE)
128  else if cond = Term `SOME GE` then SOME (Assem.GE)
129  else if cond = Term `SOME LT` then SOME (Assem.LT)
130  else if cond = Term `SOME GT` then SOME (Assem.GT)
131  else if cond = Term `SOME LE` then SOME (Assem.LE)
132  else if cond = Term `SOME AL` then SOME (Assem.AL)
133  else if cond = Term `SOME NV` then SOME (Assem.NV)
134  else NONE;
135
136
137fun from_exp t =
138    if is_comb t then
139       let val (c,v) = dest_comb t
140       in
141           if same_const c (Term`REG`) then Assem.REG (int_of_term v)
142           else if same_const c (Term`WREG`) then Assem.WREG (int_of_term v)
143           else if same_const c (Term`NCONST`) then Assem.NCONST ((Arbint.fromNat o dest_numeral) v)
144           else if same_const c (Term`WCONST`) then Assem.WCONST ((Arbint.fromNat o dest_numeral) (#2(dest_comb v)))
145           else (* MEM *)
146               let val (regNo,offset) = dest_pair v
147                   val (p,q) = dest_comb offset
148               in  Assem.MEM {reg = int_of_term regNo,
149                              offset = if same_const p (Term `POS`) then int_of_term q
150                                       else (~1 * int_of_term q),
151                              wback = false
152                             }
153               end
154        end
155    else
156        let val (t1,t2) = dest_pair t in
157            Assem.PAIR (from_exp t1, from_exp t2)
158        end
159
160
161fun dest_arm stms =
162  let
163
164    fun dest_stm stm =
165        let
166          val [operator0, op_cond0, flag0, dst0, srcL0, jump0] = strip_pair stm;
167        in
168          if operator0 = Term`MOV` then
169             Assem.MOVE {dst = from_exp (dest_some dst0),
170                         src = from_exp (hd (#1 (dest_list srcL0)))
171                        }
172          else
173            let
174              val operator1 = from_op operator0;
175              val op_cond1 = if operator1 = Assem.BL then NONE
176                           else from_cond op_cond0;
177              val flag1 = false;
178
179              val dst1 = if dst0 = mk_none (Type `:EXP`) then []
180                       else [from_exp (dest_some dst0)];
181              val srcL1 = List.map from_exp (#1 (dest_list srcL0));
182              val (dst2,srcL2) = if operator1 = Assem.LDMFD orelse operator1 = Assem.STR then (srcL1,dst1)
183                                else if operator1 = Assem.CMP then ([], srcL1)
184                                else (dst1,srcL1);
185
186              val jump1 = if jump0 = mk_none (Type `:OFFSET`) then NONE
187                        else let val l = dest_some jump0
188                                 val (sign, v) = dest_comb l;
189                                 val sign' = if sign = Term`POS` then "+" else "-"
190                                 val v' = int_of_term v;
191                             in
192                                 SOME [Symbol.mkSymbol sign' v']
193                             end
194            in
195              Assem.OPER {oper = (operator1, op_cond1, flag1), dst = dst2, src = srcL2, jump = jump1}
196            end
197       end
198  in
199      List.map dest_stm (#1 (dest_list stms))
200  end
201
202end (* local open *)
203end (* structure *)
204