1# 2# Copyright 2020, Data61, CSIRO (ABN 41 687 119 230) 3# 4# SPDX-License-Identifier: BSD-2-Clause 5# 6 7import syntax 8import solver 9import problem 10import rep_graph 11import search 12import logic 13import check 14 15from syntax import mk_var 16 17from target_objects import functions, trace, pairings, pre_pairings, printout 18import target_objects 19 20import re 21 22reg_aliases = {'sb': 'r9', 'sl': 'r10', 'fp': 'r11', 'ip': 'r12', 23 'sp': 'r13', 'lr': 'r14', 'pc': 'r15'} 24 25reg_set = set (['r%d' % i for i in range (16)]) 26 27inst_split_re = re.compile('[_,]*') 28crn_re = re.compile('cr[0123456789][0123456789]*') 29pn_re = re.compile('p[0123456789][0123456789]*') 30def split_inst_name_regs (nm): 31 bits = inst_split_re.split (nm) 32 fin_bits = [] 33 regs = [] 34 if len (bits) > 1 and pn_re.match (bits[1]): 35 bits[1] = bits[1][1:] 36 for bit in bits: 37 bit2 = bit.lower () 38 bit2 = reg_aliases.get (bit, bit) 39 if crn_re.match (bit2): 40 assert bit2.startswith ('cr') 41 bit2 = 'c' + bit2[2:] 42 if bit2 in reg_set or bit2.startswith ('%'): 43 regs.append (bit2) 44 fin_bits.append ('argv%d' % (len (regs))) 45 else: 46 fin_bits.append (bit2) 47 return (regs, '_'.join (fin_bits)) 48 49bin_globs = [('mem', syntax.builtinTs['Mem'])] 50asm_globs = [('Mem', syntax.builtinTs['Mem'])] 51 52def mk_fun (nm, word_args, ex_args, word_rets, ex_rets, globs): 53 """wrapper for making a syntax.Function with standard args/rets.""" 54 return syntax.Function (nm, 55 [(nm, syntax.word32T) for nm in word_args] + ex_args + globs, 56 [(nm, syntax.word32T) for nm in word_rets] + ex_rets + globs) 57 58instruction_fun_specs = { 59 'mcr' : ("impl'mcr", ["I"]), 60 'mcr2' : ("impl'mcr", ["I"]), 61 'mcrr' : ("impl'mcrr", ["I", "I"]), 62 'mcrr2' : ("impl'mcrr", ["I", "I"]), 63 'mrc': ("impl'mrc", ["O"]), 64 'mrc2': ("impl'mrc", ["O"]), 65 'mrrc': ("impl'mrrc", ["O", "O"]), 66 'mrrc2': ("impl'mrrc", ["O", "O"]), 67 'dsb': ("impl'dsb", []), 68 'dmb': ("impl'dmb", []), 69 'isb': ("impl'isb", []), 70 'wfi': ("impl'wfi", []), 71} 72 73instruction_name_aliases = { 74 'isb_sy': 'isb', 75 'dmb_sy': 'dmb', 76 'dsb_sy': 'dsb', 77} 78 79def add_impl_fun (impl_fname, regspecs): 80 l_fname = 'l_' + impl_fname 81 r_fname = 'r_' + impl_fname 82 if l_fname in functions: 83 return 84 assert r_fname not in functions 85 86 ident_v = ("inst_ident", syntax.builtinTs['Token']) 87 88 inps = [s for s in regspecs if s == 'I'] 89 inps = ['reg_val%d' % (i + 1) for (i, s) in enumerate (inps)] 90 rets = [s for s in regspecs if s == 'O'] 91 rets = ['ret_val%d' % (i + 1) for (i, s) in enumerate (rets)] 92 l_fun = mk_fun (l_fname, inps, [ident_v], rets, [], bin_globs) 93 r_fun = mk_fun (r_fname, inps, [ident_v], rets, [], bin_globs) 94 inp_eqs = [((mk_var (nm, typ), 'ASM_IN'), (mk_var (nm, typ), 'C_IN')) 95 for (nm, typ) in l_fun.inputs] 96 inp_eqs += [((logic.mk_rodata (mk_var (nm, typ)), 'ASM_IN'), 97 (syntax.true_term, 'C_IN')) for (nm, typ) in bin_globs] 98 out_eqs = [((mk_var (nm, typ), 'ASM_OUT'), (mk_var (nm, typ), 'C_OUT')) 99 for (nm, typ) in l_fun.outputs] 100 out_eqs += [((logic.mk_rodata (mk_var (nm, typ)), 'ASM_OUT'), 101 (syntax.true_term, 'C_OUT')) for (nm, typ) in bin_globs] 102 pair = logic.Pairing (['ASM', 'C'], {'ASM': l_fname, 'C': r_fname}, 103 (inp_eqs, out_eqs)) 104 assert l_fname not in pairings 105 assert r_fname not in pairings 106 functions[l_fname] = l_fun 107 functions[r_fname] = r_fun 108 pairings[l_fname] = [pair] 109 pairings[r_fname] = [pair] 110 111inst_addr_re = re.compile('E[0123456789][0123456789]*') 112def split_inst_name_addr (instname): 113 bits = instname.split('_') 114 assert bits, instname 115 addr = bits[-1] 116 assert inst_addr_re.match (addr), instname 117 addr = int (addr[1:], 16) 118 return ('_'.join (bits[:-1]), addr) 119 120def mk_bin_inst_spec (fname): 121 if not fname.startswith ("instruction'"): 122 return 123 if functions[fname].entry: 124 return 125 (_, ident) = fname.split ("'", 1) 126 (ident, addr) = split_inst_name_addr (ident) 127 (regs, ident) = split_inst_name_regs (ident) 128 ident = instruction_name_aliases.get (ident, ident) 129 base_ident = ident.split ("_")[0] 130 if base_ident not in instruction_fun_specs: 131 return 132 (impl_fname, regspecs) = instruction_fun_specs[base_ident] 133 add_impl_fun (impl_fname, regspecs) 134 assert len (regspecs) == len (regs), (fname, regs, regspecs) 135 inp_regs = [reg for (reg, d) in zip (regs, regspecs) if d == 'I'] 136 out_regs = [reg for (reg, d) in zip (regs, regspecs) if d == 'O'] 137 call = syntax.Node ('Call', 'Ret', ('l_' + impl_fname, 138 [syntax.mk_var (reg, syntax.word32T) for reg in inp_regs] 139 + [syntax.mk_token (ident)] 140 + [syntax.mk_var (nm, typ) for (nm, typ) in bin_globs], 141 [(reg, syntax.word32T) for reg in out_regs] + bin_globs)) 142 assert not functions[fname].nodes 143 functions[fname].nodes[1] = call 144 functions[fname].entry = 1 145 146def mk_asm_inst_spec (fname): 147 if not fname.startswith ("asm_instruction'"): 148 return 149 if functions[fname].entry: 150 return 151 (_, ident) = fname.split ("'", 1) 152 (args, ident) = split_inst_name_regs (ident) 153 if not all ([arg.startswith ('%') for arg in args]): 154 printout ('Warning: asm instruction name: formatting: %r' 155 % fname) 156 return 157 base_ident = ident.split ("_")[0] 158 if base_ident not in instruction_fun_specs: 159 return 160 (impl_fname, regspecs) = instruction_fun_specs[base_ident] 161 add_impl_fun (impl_fname, regspecs) 162 (iscs, imems, _) = logic.split_scalar_pairs (functions[fname].inputs) 163 (oscs, omems, _) = logic.split_scalar_pairs (functions[fname].outputs) 164 call = syntax.Node ('Call', 'Ret', ('r_' + impl_fname, 165 iscs + [syntax.mk_token (ident)] + imems, 166 [(v.name, v.typ) for v in oscs + omems])) 167 assert not functions[fname].nodes 168 functions[fname].nodes[1] = call 169 functions[fname].entry = 1 170 171def add_inst_specs (report_problematic = True): 172 for f in functions.keys (): 173 mk_asm_inst_spec (f) 174 mk_bin_inst_spec (f) 175 if report_problematic: 176 problematic_instructions () 177 178def problematic_instructions (): 179 add_inst_specs (report_problematic = False) 180 unhandled = {} 181 for f in functions: 182 for f2 in functions[f].function_calls (): 183 if "instruction'" not in f2: 184 continue 185 if functions[f2].entry: 186 continue 187 unhandled.setdefault (f, []) 188 unhandled[f].append (f2) 189 for f in unhandled: 190 printout ('Function %r contains unhandled instructions:' % f) 191 printout (' %s' % unhandled[f]) 192 return unhandled 193 194 195