#!/bin/awk -f
function hex(h){
	v=0
	h=tolower(h)
	for(i=1; i<=length(h); ++i){
		x=index("0123456789abcdef", substr(h, i, 1))
		if(!x)
			return -1
		v=(16*v)+x-1
	}
	return v
}
/PCI INT [A-D] \-\> GSI/{
	# remove [ timestamp ]
	sub(/^[^\:]+/, "")
	#print
	split($1, a, ":")
	bd[1]=hex(a[2])
	split(a[3], b, ".")
	bd[2]=hex(b[1])
	intp=index("ABCD", $4)
	gsi=$7
	busno=bd[1]
	# devno<<2 | (intp-1)
	irq=(4*bd[2])+(intp-1)
	apicno=2
	intin=gsi
	printf("03 00 00 00 %.2X %.2X %.2X %.2X\n", busno, irq, apicno, intin);
	# print "PCI."bd[1]"."bd[2]" #"intp" gsi"gsi" irq"irq
}