Dependently Typed Assembly Language

bcopy.dtal.asm

(*
void bcopy(int src[], int dst[]) {

   int l = 0;
   int i = 0;

   if(length(src) > length(dst))
     l = length (dst);
   else
     l = length (src);

    for(i=0;i<l;i++;) {
       src[i] = dst[i];
    }
}
*)
bcopy:	{i:nat, j:nat}
	[r0: int(i), r1:int(j), r2: int array(i), r3: int array(j)]
	mov	r4, 0
	cmp	r0, r1
	ifltz
		mov	r1, r0
	endif
	jmp	loop

loop: 	{i:nat, j:nat, n:nat, k:nat| n <= i /\ n <= j}
	[r1: int(n), r2: int array(i), r3: int array(j), r4: int(k)]
	cmp	r4, r1
	ifltz
		load	r5, r2(r4)
		store	r3(r4),	r5
	else
		jmp	finish
	endif
	add	r4, r4, 1
	jmp	loop

finish: []
	halt

bsearch.dtal.asm

start:  {n: nat}
        [r0:int array(n), r1:int(n), r5:int] // r5 store the key value we are trying to find
        mov     r2, 0                        // r2 stores the lower bound
        sub     r3, r1, 1                    // r3 stores the upper bound   
        jmp     loop                         // jump to the lable 'loop'

loop:   {n:nat, i:nat, j:nat | 0 <= i <= n /\ 0 <= j+1 <= n} // this is the loop invariant
        [r0:int array(n), r2:int(i), r3:int(j), r5:int]
        cmp     r2, r3              //  compare r2 and r3
        ifgtz                       // if r2 >  r3
                mov     r31, ~1     // r31 stores the result of the search
                jmp     finish
        else                        // if r2 <= r3
                add     r4, r3, r2 
                div     r4, r4, 2          // now r4 = (r2 + r3)/2
                load    r1, r0(r4)         // fetch array[r4] into r1
                cmp     r5, r1             // compare r5 and r1
                ifz                        // if r5 = r1 then the key has been found
                        mov     r31, r4    // r31 stores the location of the key
                        jmp     finish     // return r4
                else
                        ifgtz                     // if r5 > r1
                                add     r4, r4, 1 
                                mov     r2, r4    // move the lower bound up
                        else
                                sub     r4, r4, 1 // if r5 < r1
                                mov     r3, r4    // move the upper bound down
                        endif
                endif   
        endif
        jmp     loop                       // loop again

finish: [r31: int] // r31 contains the location of the key or -1(if the key is not found)
        halt       // the program halts

checksum.dtal.asm

(*
/* This is a version of CRC checksum: table driven implementation: */

WORD updcrc(WORD icrc, BYTE *icp, size_t icnt) {

      register WORD crc = icrc;
      register BYTE *cp = icp;
      register size_t cnt = icnt;

      while( cnt-- ) crc = (crc<<B) ^ crctab[(crc>>(W-B)) ^ *cp++];

      return( crc );
}
*)

loop:	{i, n:nat | i < n}
	[r0: word(8) array(256), r1: word(32), r2: int(i), r5: word(8) array(n)]
	blte	r2, finish
	srl	r3, r1, 24  // r3: word(8)
	load	r4, r5(r2)  // r4: word(8): load in a byte
	sub	r2, r2, 1   // r2: nat: decrease the counter by one
	xor	r3, r3, r4  // r3: word(8)
	load	r3, r0(r3)  // load in the precomputed value from the table
	sll 	r1, r1, 8   // r1: word(32)
	xor	r1, r1, r3
	jmp	loop

finish:	[r1: word(32)]
	halt

dotprod.dtal.asm

dotprod:
	{n: nat}
	[r0: int array(n), r1: int array(n), r3: int(n)]
	mov	r31, 0
	mov	r2, 0
	jmp	loop

loop:	{n:nat, i:int | 0 <= i <= n}
	[r0: int array(n), r1: int array(n), r2:int(i), r3: int(n), r31: int]
	cmp	r2, r3
	ifnz
		load	r4, r0(r2)
		load	r5, r1(r2)
		mul	r4, r4, r5
		add	r31, r31, r4
		add	r2, r2, 1
		jmp	loop
	else
		jmp	finish
	endif

finish:	[r31: int]
	halt

fact.dtal.asm

(* an implementaion of the factorial function in which
 * the continuation stores in a stack. This is basically
 * an example taken from a paper by Morriset et al.
 *)
start:	[sp: stack(0)]
	mov	r1, 10
	mov	r2, finish
	jmp     fact

fact:	{n: nat} [r1: int, sp: stack(n), r2: state(r31: int, sp: stack(n))]
	bneq	r1, nzero
	mov	r31, 1
	jmp	r2

nzero:	{n: nat} [r1: int, sp: stack(n), r2: state(r31: int, sp: stack(n))]
	push	r2
	push	r1
	sub	r1, r1, 1
	mov	r2, cont
	jmp	fact

cont:	{n: nat} [r31: int, sp: int::state(r31: int, sp: stack(n))::stack(n)]
	pop	r1
	pop	r2
	mul	r31, r31, r1
	jmp	r2

finish:	[r31: int, sp: stack(0)]
	halt

fact_cont.dtal.asm

(* 
 * The factorial fuction in CPS style. This is basically
 * an example taken from a paper by Morrisett et al.
 *)
l_start: []
	malloc	r1, 0
	malloc	r2, 0
	malloc	r3, 2
	mov	r4, l_halt
	store	r3(0), r4
	store	r3(1), r2
	mov	r2, 6
	jmp	l_fact

l_fact:	('a) [r2: int, r3: state(r1: 'a, r2: int) * 'a]
	bneq	r2, l_nonzero
	load	r4, r3(0)
	load	r1, r3(1)
	mov	r2, 1
	jmp	r4

l_nonzero:
	('a) [r2: int, r3: state(r1: 'a, r2: int) * 'a]
	sub	r4, r2, 1
	malloc	r5, 2
	store	r5(0), r2
	store	r5(1), r3 // r5: int * (state(r1: 'a, r2: int) * 'a)
	malloc	r3, 2
	mov	r2, l_cont
	store	r3(0), r2
	store	r3(1), r5 // r3: state(r1: int * ([r1: 'a, r2: int] * 'a), r2: int) *
	                  //     (int * ([r1: 'a, r2: int] * 'a)
	mov	r2, r4
	jmp	l_fact

l_cont:	('a) [r1: int * (state(r1: 'a, r2: int) * 'a), r2: int]
	load	r3, r1(0)
	load	r4, r1(1)
	mul	r2, r3, r2
	load	r3, r4(0)
	load	r1, r4(1)
	jmp	r3

l_halt:	[r2: int]
	mov	r1, r2
	halt