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