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