Algoritmo de la División Entera

Queremos transformar el código escrito en Dgcl - el lenguaje de los comandos guardados de Dijkstra - obtenido en la página 134 del apunte ``Cálculo de Programas'', que implementa el algoritmo de la división entera, en un código ensamlador para la ISA de ARC.

[ var x,y,q,r: Int
$\{R: x\geq 0 \wedge y\geq 0\}$ 
q,r := 0,x
$\{Q: x=q\times y+r \wedge 0\leq r\}$ 
 do
	r$\geq$y $\rightarrow$ q,r := q+1,r-y 
 od
$\{Q: x=q\times y+r \wedge 0\leq r \wedge r<y\}$ 
]

La primera línea de código declara 4 variables de tipo entero.

  [ var x,y,q,r: Int 

Utilizamos 4 registros para almacenar el valor de cada variable. También indicamos al ensamblador el inicio de nuestro código, asi como la dirección de memoria que elejimos para que comience a ensamblar.

 		 ! x <-> %r1 

		 ! y <-> %r2 

		 ! q <-> %r3 

		 ! r <-> %r4 

		 .begin 

		 .org 		 2048 

La siguiente sentencia es una multiasignación que hace verdadero el invariante en el inicio.

 		 q,r := 0,x 

		 $\{Q: x=q\times y+r \wedge 0\leq r\}$

La multiasignación puede ser desacoplada sin problemas, pues los rhs no dependen de los lhs. Para hacer 0 a $q$ y copiar $x$ en $r$, podemos usar sethi y add de la siguiente forma: como sethi copia su operando inmediato de 22 bits en la parte superior del registro destino y pone a 0 los 10 bits bajos, con asignar 0 a la parte alta alcanza para asignar 0 a %r3 ($q$)¹. Para la segunda asignación efectuamos una suma entre %r1 ($x$) y %r0 y ponemos el resultado en %r4 ($r$).

 	sethi	0, %r3		! q := 0
	add	%r1, %r0, %r4	! r := x

El inicio de la repetición nos induce a introducir una etiqueta loop, para poder saltar aquí cuando el lazo deba repetirse.

 do
	r$\geq$y $\rightarrow \cdots$

La comparación de la guarda la obtenemos con un subcc que modifica el registro de estado y descarta el resultado. En el caso que la guarda no sea verdadera saltamos a endloop, etiqueta de la primera instrucción fuera del ciclo.

loop:	subcc	%r4, %r2, %r0
	bneg	endloop		! do r>=y

La multiasignación que le sigue a la guarda del do... od

 	$\cdots \rightarrow$ q,r := q+1,r-y 

se logra fácilmente con instrucciones de suma y resta.

	add	%r3, 1, %r3	! q := q+1
	sub	%r4, %r2, %r4	! r := r-y

El final de la repetición la logramos con un salto incondicional al inicio del lazo, marcado por la etiqueta loop

	ba	loop		! od

Finalmente ponemos la etiqueta de salida del lazo junto con la instrucción halt que detiene la ejecución de la máquina, e indicamos al ensamblador que terminamos el programa.

endloop:halt
	.end

El código ARC completo se muestra a continuación, con el agregado de un par de instrucciones que sirven para cargar %r1 y %r2 a fin de probar el programa.

 	 ! x <-> %r1
	 ! y <-> %r2
	 ! q <-> %r3
	 ! r <-> %r4
	 .begin
	.org	2048
	ld 	[x], %r1	! cargo x
	ld	[y], %r2	! cargo y
	sethi	0, %r3		! q := 0
	add	%r1, %r0, %r4	! r := x
loop:	subcc	%r4, %r2, %r0
	bneg	endloop		! do r>= y
	add	%r3, 1, %r3	! q := q+1
	sub 	%r4, %r2, %r4	! r := r-y
	ba	loop		! od
endloop:halt
x:	25
y:	6
	.end