Remove old test directory in src/test

58 files changed, 0 insertions, 6107 deletions

diff --git a/src/test/hello3 b/src/test/hello3
deleted file mode 100644
index bb0df93e..00000000
--- a/src/test/hello3
+++ /dev/null
diff --git a/src/test/hello4 b/src/test/hello4
deleted file mode 100755
index 962527fa..00000000
--- a/src/test/hello4
+++ /dev/null
diff --git a/src/test/hello4.c b/src/test/hello4.c
deleted file mode 100644
index 849e7a8d..00000000
--- a/src/test/hello4.c
+++ /dev/null
@@ -1,11 +0,0 @@
-int main() {
-  int x = 6;
-  int y = 7;
-  int z = 0;
-  if ((x * y) > (x - y)) {
-    z = x * y;
-  } else {
-    z = x - y;
-  }
-  return z;
-}
diff --git a/src/test/hello4.objdump-D b/src/test/hello4.objdump-D
deleted file mode 100644
index 9b2f6c70..00000000
--- a/src/test/hello4.objdump-D
+++ /dev/null
@@ -1,79 +0,0 @@
-hello4:     file format elf64-powerpc
-
-
-Disassembly of section .note.gnu.build-id:
-
-0000000010000120 <.note.gnu.build-id>:
-    10000120:	00 00 00 04 	.long 0x4
-    10000124:	00 00 00 14 	.long 0x14
-    10000128:	00 00 00 03 	.long 0x3
-    1000012c:	47 4e 55 00 	.long 0x474e5500
-    10000130:	9a e3 14 bb 	stb     r23,5307(r3)
-    10000134:	f9 dc 7d 0e 	.long 0xf9dc7d0e
-    10000138:	69 0d 2a a8 	xori    r13,r8,10920
-    1000013c:	15 68 80 6a 	.long 0x1568806a
-    10000140:	64 36 a4 e2 	oris    r22,r1,42210
-
-Disassembly of section .text:
-
-0000000010000148 <.main>:
-    10000148:	fb e1 ff f8 	std     r31,-8(r1)
-    1000014c:	f8 21 ff b1 	stdu    r1,-80(r1)
-    10000150:	7c 3f 0b 78 	mr      r31,r1
-    10000154:	38 00 00 06 	li      r0,6
-    10000158:	90 1f 00 38 	stw     r0,56(r31)
-    1000015c:	38 00 00 07 	li      r0,7
-    10000160:	90 1f 00 34 	stw     r0,52(r31)
-    10000164:	38 00 00 00 	li      r0,0
-    10000168:	90 1f 00 30 	stw     r0,48(r31)
-    1000016c:	81 3f 00 38 	lwz     r9,56(r31)
-    10000170:	80 1f 00 34 	lwz     r0,52(r31)
-    10000174:	7c 09 01 d6 	mullw   r0,r9,r0
-    10000178:	7c 09 07 b4 	extsw   r9,r0
-    1000017c:	81 7f 00 38 	lwz     r11,56(r31)
-    10000180:	80 1f 00 34 	lwz     r0,52(r31)
-    10000184:	7c 00 58 50 	subf    r0,r0,r11
-    10000188:	7c 00 07 b4 	extsw   r0,r0
-    1000018c:	7f 89 00 00 	cmpw    cr7,r9,r0
-    10000190:	40 9d 00 18 	ble-    cr7,100001a8 <.main+0x60>
-    10000194:	81 3f 00 38 	lwz     r9,56(r31)
-    10000198:	80 1f 00 34 	lwz     r0,52(r31)
-    1000019c:	7c 09 01 d6 	mullw   r0,r9,r0
-    100001a0:	90 1f 00 30 	stw     r0,48(r31)
-    100001a4:	48 00 00 14 	b       100001b8 <.main+0x70>
-    100001a8:	81 3f 00 38 	lwz     r9,56(r31)
-    100001ac:	80 1f 00 34 	lwz     r0,52(r31)
-    100001b0:	7c 00 48 50 	subf    r0,r0,r9
-    100001b4:	90 1f 00 30 	stw     r0,48(r31)
-    100001b8:	80 1f 00 30 	lwz     r0,48(r31)
-    100001bc:	7c 00 07 b4 	extsw   r0,r0
-    100001c0:	7c 03 03 78 	mr      r3,r0
-    100001c4:	38 3f 00 50 	addi    r1,r31,80
-    100001c8:	eb e1 ff f8 	ld      r31,-8(r1)
-    100001cc:	4e 80 00 20 	blr
-	...
-    100001d8:	80 01 00 01 	lwz     r0,1(r1)
-
-Disassembly of section .opd:
-
-00000000100101e0 <main>:
-    100101e0:	00 00 00 00 	.long 0x0
-    100101e4:	10 00 01 48 	vmulosh v0,v0,v0
-    100101e8:	00 00 00 00 	.long 0x0
-    100101ec:	10 01 81 e0 	vmhaddshs v0,v1,v16,v7
-	...
-
-Disassembly of section .comment:
-
-0000000000000000 <.comment>:
-   0:	47 43 43 3a 	.long 0x4743433a
-   4:	20 28 47 4e 	subfic  r1,r8,18254
-   8:	55 29 20 34 	rlwinm  r9,r9,4,0,26
-   c:	2e 34 2e 37 	cmpdi   cr4,r20,11831
-  10:	20 32 30 31 	subfic  r1,r18,12337
-  14:	32 30 33 31 	addic   r17,r16,13105
-  18:	33 20 28 52 	addic   r25,r0,10322
-  1c:	65 64 20 48 	oris    r4,r11,8264
-  20:	61 74 20 34 	ori     r20,r11,8244
-  24:	2e 34 2e 37 	cmpdi   cr4,r20,11831
-  28:	2d 33 29 00 	cmpdi   cr2,r19,10496
diff --git a/src/test/hello4.s b/src/test/hello4.s
deleted file mode 100644
index 4c7100d6..00000000
--- a/src/test/hello4.s
+++ /dev/null
@@ -1,53 +0,0 @@
-	.file	"hello4.c"
-	.section	".toc","aw"
-	.section	".text"
-	.align 2
-	.globl main
-	.section	".opd","aw"
-	.align 3
-main:
-	.quad	.L.main,.TOC.@tocbase
-	.previous
-	.type	main, @function
-.L.main:
-	std 31,-8(1)
-	stdu 1,-80(1)
-	mr 31,1
-	li 0,6
-	stw 0,56(31)
-	li 0,7
-	stw 0,52(31)
-	li 0,0
-	stw 0,48(31)
-	lwz 9,56(31)
-	lwz 0,52(31)
-	mullw 0,9,0
-	extsw 9,0
-	lwz 11,56(31)
-	lwz 0,52(31)
-	subf 0,0,11
-	extsw 0,0
-	cmpw 7,9,0
-	ble 7,.L2
-	lwz 9,56(31)
-	lwz 0,52(31)
-	mullw 0,9,0
-	stw 0,48(31)
-	b .L3
-.L2:
-	lwz 9,56(31)
-	lwz 0,52(31)
-	subf 0,0,9
-	stw 0,48(31)
-.L3:
-	lwz 0,48(31)
-	extsw 0,0
-	mr 3,0
-	addi 1,31,80
-	ld 31,-8(1)
-	blr
-	.long 0
-	.byte 0,0,0,0,128,1,0,1
-	.size	main,.-.L.main
-	.ident	"GCC: (GNU) 4.4.7 20120313 (Red Hat 4.4.7-3)"
-	.section	.note.GNU-stack,"",@progbits
diff --git a/src/test/hello6 b/src/test/hello6
deleted file mode 100755
index 4eb7db0a..00000000
--- a/src/test/hello6
+++ /dev/null
diff --git a/src/test/idempotence.sh b/src/test/idempotence.sh
deleted file mode 100755
index 5527680d..00000000
--- a/src/test/idempotence.sh
+++ /dev/null
@@ -1,14 +0,0 @@
-#!/bin/sh -e
-input=$1
-sail=../sail.native
-
-output1=`mktemp  --suffix=.sail`
-echo Pretty-printing $input
-$sail -verbose $input > $output1
-
-output2=`mktemp  --suffix=.sail`
-echo Pretty-printing pretty-printed
-$sail -verbose $output1 > $output2
-
-diff -u $output1 $output2 && \
-  (rm -f $output1 $output2; echo Idempotence: ok)
diff --git a/src/test/lib/Makefile b/src/test/lib/Makefile
deleted file mode 100644
index fbd5a332..00000000
--- a/src/test/lib/Makefile
+++ /dev/null
@@ -1,52 +0,0 @@
-
-# Disable built-in make madness
-MAKEFLAGS=-r
-.SUFFIXES:
-
-TESTS=div.sail
-
-BITBUCKET_DIR:=$(realpath ../../../../)
-LEM_DIR:=$(BITBUCKET_DIR)/lem
-LEM:=$(LEM_DIR)/lem
-SAIL_DIR:=$(BITBUCKET_DIR)/sail/src
-SAIL:=$(SAIL_DIR)/sail.native
-SAIL_VALUES:=$(SAIL_DIR)/gen_lib/sail_values.ml
-
-BUILD_DIR:=_build
-
-TESTS:=$(wildcard tests/*.sail)
-OCAML_RESULTS:=$(addsuffix _embed.out,$(addprefix $(BUILD_DIR)/,$(notdir $(basename $(TESTS)))))
-INTERP_RESULTS:=$(addsuffix _interp.out,$(addprefix $(BUILD_DIR)/,$(notdir $(basename $(TESTS)))))
-
-all: tests.xml
-
-clean:
-	rm -rf $(BUILD_DIR) tests.xml
-
-$(BUILD_DIR):
-	mkdir -p $@
-
-$(BUILD_DIR)/run_test_embed.ml: | $(BUILD_DIR)
-	cp run_test_embed.ml $(BUILD_DIR)
-
-$(BUILD_DIR)/run_test_interp.ml: | $(BUILD_DIR)
-	cp run_test_interp.ml $(BUILD_DIR)
-
-$(BUILD_DIR)/sail_values.ml: | $(BUILD_DIR)
-	cp $(SAIL_VALUES) $(BUILD_DIR)
-
-$(BUILD_DIR)/%_embed.out : tests/%.sail $(BUILD_DIR)/run_test_embed.ml $(BUILD_DIR)/sail_values.ml
-	cd $(BUILD_DIR) && \
-	$(SAIL) -ocaml ../test_prelude.sail ../$< ../test_epilogue.sail -o test && \
-	ocamlfind ocamlopt -package zarith -linkpkg sail_values.ml test.ml run_test_embed.ml -o test_embed.native && \
-	./test_embed.native > $(notdir $@)
-
-$(BUILD_DIR)/%_interp.out : tests/%.sail $(BUILD_DIR)/run_test_interp.ml
-	cd $(BUILD_DIR) && \
-	$(SAIL) -lem_ast ../test_prelude.sail ../$< ../test_epilogue.sail -o test_lem_ast && \
-	$(LEM) -ocaml test_lem_ast.lem -lib $(SAIL_DIR)/lem_interp && \
-	ocamlfind ocamlopt -g -package num -package zarith -package lem -linkpkg -I $(SAIL_DIR)/_build/lem_interp $(SAIL_DIR)/_build/lem_interp/extract.cmxa test_lem_ast.ml run_test_interp.ml -o test_interp.native && \
-	./test_interp.native >$(notdir $@) 2>&1
-
-tests.xml: $(OCAML_RESULTS) $(INTERP_RESULTS)
-	./test_to_junit.sh $^
diff --git a/src/test/lib/run_test_embed.ml b/src/test/lib/run_test_embed.ml
deleted file mode 100644
index f7b45316..00000000
--- a/src/test/lib/run_test_embed.ml
+++ /dev/null
@@ -1,2 +0,0 @@
-Test._run()
-  
diff --git a/src/test/lib/test_epilogue.sail b/src/test/lib/test_epilogue.sail
deleted file mode 100644
index 434b8a95..00000000
--- a/src/test/lib/test_epilogue.sail
+++ /dev/null
@@ -1,5 +0,0 @@
-(* TranslateAddress compatible "main" function *)
-function (bit[64]) run ((bit[64]) x) = {
-  test();
-  return 0;
-}
diff --git a/src/test/lib/test_prelude.sail b/src/test/lib/test_prelude.sail
deleted file mode 100644
index 3525af8e..00000000
--- a/src/test/lib/test_prelude.sail
+++ /dev/null
@@ -1,19 +0,0 @@
-default Order inc
-
-scattered typedef ast = const union
-val ast -> unit effect pure execute
-scattered function unit execute
-
-union ast member (unit) DUMMY
-function clause execute (DUMMY) = ()
-
-end ast
-end execute
-
-function unit test_assert (name, pred) = {
-  print (name);
-  if pred then
-    print (": pass\n")
-  else
-    print(": fail\n")
-}
diff --git a/src/test/lib/test_to_junit.sh b/src/test/lib/test_to_junit.sh
deleted file mode 100755
index 71e908bd..00000000
--- a/src/test/lib/test_to_junit.sh
+++ /dev/null
@@ -1,62 +0,0 @@
-#!/usr/bin/env bash
-set -e
-
-RED='\033[0;31m'
-GREEN='\033[0;32m'
-YELLOW='\033[0;33m'
-NC='\033[0m'
-
-
-pass=0
-fail=0
-
-XML=""
-
-XML_FILE=tests.xml
-
-function green {
-    (( pass += 1 ))
-    printf "$1: ${GREEN}$2${NC}\n"
-    XML+="    <testcase name=\"$1\"/>\n"
-}
-
-function yellow {
-    (( fail += 1 ))
-    printf "$1: ${YELLOW}$2${NC}\n"
-    XML+="    <testcase name=\"$1\">\n      <error message=\"$2\">$2</error>\n    </testcase>\n"
-}
-
-function red {
-    (( fail += 1 ))
-    printf "$1: ${RED}$2${NC}\n"
-    XML+="    <testcase name=\"$1\">\n      <error message=\"$2\">$2</error>\n    </testcase>\n"
-}
-
-function finish_suite {
-    printf "$1: Passed ${pass} out of $(( pass + fail ))\n"
-    XML="  <testsuite name=\"$1\" tests=\"$(( pass + fail ))\" failures=\"${fail}\" timestamp=\"$(date)\">\n$XML  </testsuite>\n"
-    printf "$XML" >> $XML_FILE
-    XML=""
-    pass=0
-    fail=0
-}
-
-test_regex="^\"*([^\"]*)\"*: (pass|fail)$"
-echo "<testsuites>" > $XML_FILE
-for result_file in $@; do
-    while read line; do
-        if [[ $line =~ $test_regex ]] ; then
-            test_name=${BASH_REMATCH[1]}
-            test_status=${BASH_REMATCH[2]}
-            if [[ $test_status == pass ]] ; then
-                green $test_name $test_status
-            else
-                red $test_name $test_status
-            fi
-        else
-            echo $line
-        fi
-    done < "$result_file"
-    finish_suite $result_file
-done
-echo "</testsuites>" >> $XML_FILE
diff --git a/src/test/lib/tests/test_add.sail b/src/test/lib/tests/test_add.sail
deleted file mode 100644
index ce0a19f0..00000000
--- a/src/test/lib/tests/test_add.sail
+++ /dev/null
@@ -1,19 +0,0 @@
-function unit test () = {
-  test_assert ("add", 1 + 1 == 2);
-  test_assert ("add_vec", ((bit[4])(0x1 + 0x1)) == 0x2);
-  test_assert ("add_vec_ov", ((bit[4])(0xf + 0x1)) == 0x0);
-  test_assert ("add_vec_vec_range", ((range<0,30>)(0x1 + 0x1)) == 2);
-  test_assert ("add_vec_vec_range_ov", ((range<0,15>)(0xf + 0x1)) == 0); (* XXX broken... *)
-  test_assert ("add_vec_range", ((bit[4])(0x1 + 1)) == 0x2);
-  test_assert ("add_vec_range_range", ((range<0,15>)(0xe + 1)) == 15);
-  test_assert ("add_overflow_vec", (((bit[4], bit, bit))(0x1 + 0x1)) == (0x2, false, false));
-  test_assert ("add_overflow_vec_ov", (((bit[4], bit, bit))(0xf + 0x1)) == (0x0, true, true)); (* XXX overflow flag makes no sense for unsigned... *)
-  test_assert ("add_overflow_vec_ovs", (((bit[4], bit, bit))(0x4 + 0x4)) == (0x8, false, false));
-  test_assert ("add_vec_range_range", ((range<0,16>)(0xe + 1)) == 15);
-  test_assert ("add_range_vec", ((bit[4])(1 + 0xe)) == 0xf);
-  test_assert ("add_range_vec_range", ((range<0,3>)(1 + 0xe)) == 15);
-  test_assert ("add_vec_bit", ((bit[4])(0xe + bitone)) == 0xf);
-  (* not defined on either model...
-  test_assert ("add_bit_vec", ((bit[4])(bitone + 0x1)) == 0x2); *)
-}
-
diff --git a/src/test/lib/tests/test_add_signed.sail b/src/test/lib/tests/test_add_signed.sail
deleted file mode 100644
index a723389e..00000000
--- a/src/test/lib/tests/test_add_signed.sail
+++ /dev/null
@@ -1,27 +0,0 @@
-function unit test() = {
-  test_assert ("adds", 1 +_s 1 == 2); (* same as unsigned *)
-  test_assert ("adds_vec", ((bit[4])(0x1 +_s 0x1)) == 0x2);  (* same as unsigned *)
-  test_assert ("adds_vec_ov", ((bit[4])(0xf +_s 0x1)) == 0x0);  (* same as unsigned *)
-
-  (* XXX would be good to restrict range type *)
-  test_assert ("adds_vec_vec_range_pp", ((int)(0x1 +_s 0x1)) == 2);
-  test_assert ("adds_vec_vec_range_np", ((int)(0xa +_s 0x1)) == (-5));
-  test_assert ("adds_vec_vec_range_pn", ((int)(0x3 +_s 0xe)) == 1);
-  test_assert ("adds_vec_vec_range_nn", ((int)(0x8 +_s 0x8)) == (-16));
-
-  test_assert ("adds_vec_range", ((bit[4])(0xe +_s 1)) == 0xf);
-  test_assert ("adds_vec_range_range", ((int)(0xe +_s 1)) == (-1));
-  (* returns (result, signed overflow, carry out)*)
-  test_assert ("adds_overflow_vec0", (((bit[4], bit, bit))(0x1 +_s 0x1)) == (0x2, false, false));
-  test_assert ("adds_overflow_vec1", (((bit[4], bit, bit))(0xf +_s 0x1)) == (0x0, false, true));
-  test_assert ("adds_overflow_vec2", (((bit[4], bit, bit))(0x7 +_s 0x1)) == (0x8, true, false));
-  test_assert ("adds_overflow_vec3", (((bit[4], bit, bit))(0x8 +_s 0x8)) == (0x0, true, true));
-
-  test_assert ("adds_vec_range_range", ((int)(0xe +_s 1)) == (-1));
-  test_assert ("adds_range_vec", ((bit[4])(1 +_s 0xe)) == 0xf);
-  test_assert ("adds_range_vec_range", ((int)(1 +_s 0xe)) == -1);
-  test_assert ("adds_vec_bit", ((bit[4])(0xe +_s bitone)) == 0xf);
-  (* not defined on either model... 
-  test_assert ("adds_bit_vec", ((bit[4])(bitone +_s 0xe)) == 0xf);*)
-}
-
diff --git a/src/test/lib/tests/test_and.sail b/src/test/lib/tests/test_and.sail
deleted file mode 100644
index 7c9cd800..00000000
--- a/src/test/lib/tests/test_and.sail
+++ /dev/null
@@ -1,7 +0,0 @@
-function unit test () = {
-  test_assert ("bitwise_and", (0b0101 & 0b0011) == 0b0001);
-  test_assert ("bitwise_and_00", (bitzero & bitzero) == bitzero);
-  test_assert ("bitwise_and_01", (bitzero & bitone)  == bitzero);
-  test_assert ("bitwise_and_10", (bitone  & bitzero) == bitzero);
-  test_assert ("bitwise_and_11", (bitone  & bitone)  == bitone);
-}
diff --git a/src/test/lib/tests/test_div.sail b/src/test/lib/tests/test_div.sail
deleted file mode 100644
index 1af58d20..00000000
--- a/src/test/lib/tests/test_div.sail
+++ /dev/null
@@ -1,39 +0,0 @@
-function unit test () = {
-  test_assert ("divpospos_exact", (21 div 7) == 3);
-  test_assert ("divposneg_exact", (21 div -7) == -3);
-  test_assert ("divnegpos_exact", (-21 div 7) == -3);
-  test_assert ("divnegneg_exact", (-21 div -7) == 3);
-
-  test_assert ("divpospos_approx", (21 div 8) == 2);
-  test_assert ("divposneg_approx", (21 div -8) == -2);
-  test_assert ("divnegpos_approx", (-21 div 8) == -2);
-  test_assert ("divnegneg_approx", (-21 div -8) == 2);
-
-  (* quot and div are synonyms but let's check...  *)
-  test_assert ("quotpospos_exact", (21 quot 7) == 3);
-  test_assert ("quotposneg_exact", (21 quot -7) == -3);
-  test_assert ("quotnegpos_exact", (-21 quot 7) == -3);
-  test_assert ("quotnegneg_exact", (-21 quot -7) == 3);
-
-  test_assert ("quotpospos_approx", (21 quot 8) == 2);
-  test_assert ("quotposneg_approx", (21 quot -8) == -2);
-  test_assert ("quotnegpos_approx", (-21 quot 8) == -2);
-  test_assert ("quotnegneg_approx", (-21 quot -8) == 2);
-
-  (* XXX currently crashes on shallow embedding
-  test_assert ("div_overflow", ((bit[8])(0x80 quot_s 0xff)) == 0x80);
-  *)
-  test_assert ("quot_vec_pospos_exact", ((bit[8])(0x15 quot 0x07)) == 0x03);
-  test_assert ("quot_vec_posneg_exact", ((bit[8])(0x15 quot 0xf9)) == 0x00);
-  test_assert ("quot_vec_negpos_exact", ((bit[8])(0xeb quot 0x07)) == 0x21);
-  test_assert ("quot_vec_negneg_exact", ((bit[8])(0xeb quot 0xf9)) == 0x00);
-
-  test_assert ("quot_vec_pospos_approx", ((bit[8])(0x15 quot 0x08)) == 0x02);
-  test_assert ("quot_vec_posneg_approx", ((bit[8])(0x15 quot 0xf8)) == 0x00);
-  test_assert ("quot_vec_negpos_approx", ((bit[8])(0xeb quot 0x08)) == 0x1d);
-  test_assert ("quot_vec_negneg_approx", ((bit[8])(0xeb quot 0xf8)) == 0x00);
-
-  test_assert ("quot_overflow_vec", (((bit[8], bit, bit))(0x15 quot 0x08)) == (0x02, false, false));
-  test_assert ("quot_overflow_vec", (((bit[8], bit, bit))(0x80 quot 0xff)) == (0x00, false, false));
-}
-
diff --git a/src/test/lib/tests/test_duplicate.sail b/src/test/lib/tests/test_duplicate.sail
deleted file mode 100644
index 99ffbe6c..00000000
--- a/src/test/lib/tests/test_duplicate.sail
+++ /dev/null
@@ -1,14 +0,0 @@
-function unit test () = {
-  (* XXX crashes on shallow embedding
-  should type have a constraint n>0?
-  test_assert ("duplicate_empty", (bitzero ^^ 0) == []); *)
-  test_assert ("duplicate0", (bitzero ^^ 8) == 0x00);
-  test_assert ("duplicate1", (bitone ^^ 8) == 0xff);
-
-  (* XXX crashes on shallow embedding 
-  test_assert ("duplicate_bits0", (0x21 ^^ 0) == []);*)
-  test_assert ("duplicate_bits1", (0xce ^^ 1) == 0xce);
-  test_assert ("duplicate_bits9", (0xce ^^ 9) == 0xcecececececececece);
-  test_assert ("duplicate_covfefe", (0xc0 : (0xfe ^^ 2)) == 0xc0fefe);
-}
-
diff --git a/src/test/lib/tests/test_eq.sail b/src/test/lib/tests/test_eq.sail
deleted file mode 100644
index 3000b7c5..00000000
--- a/src/test/lib/tests/test_eq.sail
+++ /dev/null
@@ -1,18 +0,0 @@
-function unit test () = {
-  test_assert("eq_bit00", false == bitzero);
-  test_assert("eq_bit01", not(false == bitone));
-  test_assert("eq_bit10", not(true == bitzero));
-  test_assert("eq_bit11", true == bitone);
-
-  test_assert("eq_vec0", not (0x1 == 0x2));
-  test_assert("eq_vec1", 0x2 == 0x2);
-  test_assert("eq_vec_range0", not (0xf == 16));
-  test_assert("eq_vec_range1", 0xf == 15);
-  test_assert("eq_range_vec0", not (16 == 0xf));
-  test_assert("eq_range_vec1", 15 == 0xf);
-  test_assert("eq_range0", not(12 == 13));
-  test_assert("eq_range1", 13 == 13);
-  test_assert("eq_tup0", not ((true, false) == (bitzero, bitzero)));
-  test_assert("eq_tup1", (true, false) == (bitone, bitzero));
-}
-
diff --git a/src/test/lib/tests/test_ext.sail b/src/test/lib/tests/test_ext.sail
deleted file mode 100644
index 1cbc2855..00000000
--- a/src/test/lib/tests/test_ext.sail
+++ /dev/null
@@ -1,15 +0,0 @@
-function unit test () = {
-  test_assert ("extz0", EXTZ(0b00) == 0x00);
-  test_assert ("extz1", EXTZ(0b10) == 0x02);
-  test_assert ("extz2", EXTZ(0b10) == 0b10);
-  test_assert ("extz3", EXTZ(0b10) == 0b0);
-  
-  test_assert ("exts0", EXTS(0b00) == 0x00);
-  test_assert ("exts1", EXTS(0b10) == 0xfe);
-  test_assert ("exts2", EXTS(0b10) == 0b10);
-  test_assert ("exts3", EXTS(0b10) == 0b0);
-
-  test_assert ("most_significant0", most_significant(0b011) == bitzero);
-  test_assert ("most_significant1", most_significant(0b100) == bitone);
-  }
-
diff --git a/src/test/lib/tests/test_gt.sail b/src/test/lib/tests/test_gt.sail
deleted file mode 100644
index 8576a8cd..00000000
--- a/src/test/lib/tests/test_gt.sail
+++ /dev/null
@@ -1,36 +0,0 @@
-function unit test() = {
-  test_assert("gt0",    ( 1 > -1));
-  test_assert("gt1", not(-1 > -1));
-  test_assert("gt2", not(-1 >  1));
-
-  (* XXX default is signed -- document this! *)
-  test_assert("gt_vec0",    (0x1 > 0xf));
-  test_assert("gt_vec1", not(0xf > 0xf));
-  test_assert("gt_vec2", not(0xf > 0x1));
-
-  test_assert("gt_vec_range0",    (0x1 > -1));
-  test_assert("gt_vec_range1", not(0xf > -1));
-  test_assert("gt_vec_range2", not(0xf > 1));
-  (* NB missing range_vec version *)
-
-  (* XXX missing implementations
-  test_assert("gt_unsigned0",    ( 1 >_u -1));
-  test_assert("gt_unsigned1", not(-1 >_u -1));
-  test_assert("gt_unsigned2", not(-1 >_u  1)); *)
-
-  test_assert("gt_vec_unsigned0", not(0x1 >_u 0xf));
-  test_assert("gt_vec_unsigned1", not(0xf >_u 0xf));
-  test_assert("gt_vec_unsigned2",    (0xf >_u 0x1));
-
-  (* NB there is no gt_vec_range unsigned or signed *)
-
-  (* XXX missing implementations 
-  test_assert("gt_signed0",    ( 1 >_s -1));
-  test_assert("gt_signed1", not(-1 >_s -1));
-  test_assert("gt_signed2", not(-1 >_s  1)); *)
-
-  test_assert("gt_vec_signed0",    (0x1 >_s 0xf));
-  test_assert("gt_vec_signed1", not(0xf >_s 0xf));
-  test_assert("gt_vec_signed2", not(0xf >_s 0x1));
-}
-
diff --git a/src/test/lib/tests/test_gteq.sail b/src/test/lib/tests/test_gteq.sail
deleted file mode 100644
index 79d4d378..00000000
--- a/src/test/lib/tests/test_gteq.sail
+++ /dev/null
@@ -1,41 +0,0 @@
-function unit test() = {
-  test_assert("gteq0",    ( 1 >= -1));
-  test_assert("gteq1",    (-1 >= -1));
-  test_assert("gteq2", not(-1 >=  1));
-
-  (* XXX default is signed -- document this! *)
-  test_assert("gteq_vec0",    (0x1 >= 0xf));
-  test_assert("gteq_vec1",    (0xf >= 0xf));
-  test_assert("gteq_vec2", not(0xf >= 0x1));
-
-  (* XXX odd type error here -- sail seems to prefer gteq_vec...
-  test_assert("gteq_vec_range0",    (0x1 >= -1)); 
-  test_assert("gteq_vec_range1",    (0xf >= -1));
-  test_assert("gteq_vec_range2", not(0xf >= 1));
-
-  test_assert("gteq_range_vec0",    ( 1 >= 0xf));
-  test_assert("gteq_range_vec1",    (-1 >= 0xf));
-  test_assert("gteq_range_vec2", not(-1 >= 0x1));*)
-
-  (* XXX missing implementations
-  test_assert("gteq_unsigned0",    ( 1 >=_u -1));
-  test_assert("gteq_unsigned1", not(-1 >=_u -1));
-  test_assert("gteq_unsigned2", not(-1 >=_u  1)); *)
-
-  (* XXX missing
-  test_assert("gteq_unsigned_vec0", not(0x1 >=_u 0xf));
-  test_assert("gteq_unsigned_vec1", not(0xf >=_u 0xf));
-  test_assert("gteq_unsigned_vec2",    (0xf >=_u 0x1)); *)
-
-  (* NB there is no gteq_vec_range unsigned or signed *)
-
-  (* XXX missing implementations 
-  test_assert("gteq_signed0",    ( 1 >=_s -1));
-  test_assert("gteq_signed1", not(-1 >=_s -1));
-  test_assert("gteq_signed2", not(-1 >=_s  1)); *)
-
-  test_assert("gteq_vec_signed0",    (0x1 >=_s 0xf));
-  test_assert("gteq_vec_signed1",    (0xf >=_s 0xf));
-  test_assert("gteq_vec_signed2", not(0xf >=_s 0x1));
-}
-
diff --git a/src/test/lib/tests/test_leftshift.sail b/src/test/lib/tests/test_leftshift.sail
deleted file mode 100644
index 15c308bc..00000000
--- a/src/test/lib/tests/test_leftshift.sail
+++ /dev/null
@@ -1,11 +0,0 @@
-function unit test () = {
-  test_assert ("leftshift_small0", (0x99 << 0) == 0x99);
-  test_assert ("leftshift_small3", (0x99 << 3) == 0xc8);
-  test_assert ("leftshift_small7", (0x99 << 7) == 0x80);
-  test_assert ("leftshift_small8", (0x99 << 8) == 0x00);
-  test_assert ("leftshift_big0", (0x99999999999999999 << 0) == 0x99999999999999999);
-  test_assert ("leftshift_big3", (0x99999999999999999 << 3) == 0xcccccccccccccccc8);
-  test_assert ("leftshift_big7", (0x99999999999999999 << 7) == 0xccccccccccccccc80);
-  test_assert ("leftshift_big68", (0x99999999999999999 << 68) == 0x00000000000000000);
-}
-
diff --git a/src/test/lib/tests/test_lt.sail b/src/test/lib/tests/test_lt.sail
deleted file mode 100644
index 6ae7a3c3..00000000
--- a/src/test/lib/tests/test_lt.sail
+++ /dev/null
@@ -1,36 +0,0 @@
-function unit test() = {
-  test_assert("lt0", not( 1 < -1));
-  test_assert("lt1", not(-1 < -1));
-  test_assert("lt2",    (-1 <  1));
-
-  (* XXX default is signed -- document this! *)
-  test_assert("lt_vec0", not(0x1 < 0xf));
-  test_assert("lt_vec1", not(0xf < 0xf));
-  test_assert("lt_vec2",    (0xf < 0x1));
-
-  test_assert("lt_vec_range0", not(0x1 < -1));
-  test_assert("lt_vec_range1", not(0xf < -1));
-  test_assert("lt_vec_range2",    (0xf < 1));
-  (* NB missing range_vec version *)
-
-  (* XXX missing implementations
-  test_assert("lt_unsigned0", not( 1 <_u -1));
-  test_assert("lt_unsigned1", not(-1 <_u -1));
-  test_assert("lt_unsigned2",    (-1 <_u  1)); *)
-
-  test_assert("lt_vec_unsigned0",    (0x1 <_u 0xf));
-  test_assert("lt_vec_unsigned1", not(0xf <_u 0xf));
-  test_assert("lt_vec_unsigned2", not(0xf <_u 0x1));
-
-  (* NB there is no lt_vec_range unsigned or signed *)
-
-  (* XXX missing implementations 
-  test_assert("lt_signed0", not( 1 <_s -1));
-  test_assert("lt_signed1", not(-1 <_s -1));
-  test_assert("lt_signed2",    (-1 <_s  1)); *)
-
-  test_assert("lt_vec_signed0", not(0x1 <_s 0xf));
-  test_assert("lt_vec_signed1", not(0xf <_s 0xf));
-  test_assert("lt_vec_signed2",    (0xf <_s 0x1));
-}
-
diff --git a/src/test/lib/tests/test_lteq.sail b/src/test/lib/tests/test_lteq.sail
deleted file mode 100644
index 612023e9..00000000
--- a/src/test/lib/tests/test_lteq.sail
+++ /dev/null
@@ -1,40 +0,0 @@
-function unit test() = {
-  test_assert("lteq0", not( 1 <= -1));
-  test_assert("lteq1",    (-1 <= -1));
-  test_assert("lteq2",    (-1 <=  1));
-
-  (* XXX default is signed -- document this! *)
-  test_assert("lteq_vec0", not(0x1 <= 0xf));
-  test_assert("lteq_vec1",    (0xf <= 0xf));
-  test_assert("lteq_vec2",    (0xf <= 0x1));
-
-  test_assert("lteq_vec_range0", not(0x1 <= -1));
-  test_assert("lteq_vec_range1",    (0xf <= -1));
-  test_assert("lteq_vec_range2",    (0xf <= 1));
-
-  test_assert("lteq_range_vec0", not( 1 <= 0xf));
-  test_assert("lteq_range_vec1",    (-1 <= 0xf));
-  test_assert("lteq_range_vec2",    (-1 <= 0x1));
-
-  (* XXX missing implementations
-  test_assert("lteq_unsigned0", not( 1 <=_u -1));
-  test_assert("lteq_unsigned1",    (-1 <=_u -1));
-  test_assert("lteq_unsigned2",    (-1 <=_u  1)); *)
-
-  (* XXX missing type / parser
-  test_assert("lteq_unsigned_vec0",    (0x1 <=_u 0xf));
-  test_assert("lteq_unsigned_vec1",    (0xf <=_u 0xf));
-  test_assert("lteq_unsigned_vec2", not(0xf <=_u 0x1));*)
-
-  (* NB there is no lteq_vec_range unsigned or signed *)
-
-  (* XXX missing implementations 
-  test_assert("lteq_signed0", not( 1 <=_s -1));
-  test_assert("lteq_signed1",    (-1 <=_s -1));
-  test_assert("lteq_signed2",    (-1 <=_s  1)); *)
-
-  test_assert("lteq_vec_signed0", not(0x1 <=_s 0xf));
-  test_assert("lteq_vec_signed1",    (0xf <=_s 0xf));
-  test_assert("lteq_vec_signed2",    (0xf <=_s 0x1));
-}
-
diff --git a/src/test/lib/tests/test_minus.sail b/src/test/lib/tests/test_minus.sail
deleted file mode 100644
index 455f3954..00000000
--- a/src/test/lib/tests/test_minus.sail
+++ /dev/null
@@ -1,25 +0,0 @@
-function unit test() = {
-  test_assert("minus", 1 - 1 == 0);
-  test_assert("minus_vec", ((bit[4])(0x2 - 0x1)) == 0x1);
-  test_assert("minus_vec_ov", ((bit[4])(0x1 - 0xf)) == 0x2);
-  (* XXX minus_vec_vec_range not implemented 
-  test_assert("minus_vec_vec_range_pp", ((int)(0x1 - 0x1)) == 0);
-  test_assert("minus_vec_vec_range_np", ((int)(0xa - 0x1)) == 9);
-  test_assert("minus_vec_vec_range_pn", ((int)(0x3 - 0xe)) == 5);
-  test_assert("minus_vec_vec_range_nn", ((int)(0x8 - 0x8)) == 0);*)
-  test_assert("minus_vec_range", ((bit[4])(0xe - 1)) == 0xd);
-  test_assert("minus_vec_range_range", ((int)(0xe - 1)) == 13);
-  test_assert("minus_range_vec", ((bit[4])(1 - 0xe)) == 0x3);
-  test_assert("minus_range_vec_range", ((int)(1 - 0xe)) == -13);
-  (* returns (result, signed overflow, borrow in)*)
-  test_assert ("minus_overflow_vec0", (((bit[4], bit, bit))(0x1 - 0x1)) == (0x0, false, false));
-  test_assert ("minus_overflow_vec1", (((bit[4], bit, bit))(0x0 - 0x1)) == (0xf, true, true));
-  test_assert ("minus_overflow_vec2", (((bit[4], bit, bit))(0x8 - 0x1)) == (0x7, false, false));
-  test_assert ("minus_overflow_vec3", (((bit[4], bit, bit))(0x0 - 0x8)) == (0x8, true, true));
-
-  test_assert ("minus_overflow_vec_bit0", (((bit[4], bit, bit))(0x1 - bitone)) == (0x0, false, false));
-  test_assert ("minus_overflow_vec_bit1", (((bit[4], bit, bit))(0x0 - bitone)) == (0xf, true, true));
-  test_assert ("minus_overflow_vec_bit2", (((bit[4], bit, bit))(0x8 - bitone)) == (0x7, false, false));
-  test_assert ("minus_overflow_vec_bit3", (((bit[4], bit, bit))(0x8 - bitzero)) == (0x8, false, false)); (* XXX shallow embedding returns true, false... *)
-}
-
diff --git a/src/test/lib/tests/test_minus_signed.sail b/src/test/lib/tests/test_minus_signed.sail
deleted file mode 100644
index 7268f340..00000000
--- a/src/test/lib/tests/test_minus_signed.sail
+++ /dev/null
@@ -1,27 +0,0 @@
-function unit test() = {
-  test_assert("minus_signed", 1 -_s 1 == 0);
-  (* XXX minus_vec_signed not implemented
-  test_assert("minus_vec_signed", ((bit[4])(0x2 -_s 0x1)) == 0x1); 
-  test_assert("minus_vec_ov_signed", ((bit[4])(0x1 -_s 0xf)) == 0x2); *)
-  (* XXX minus_vec_vec_range_signed not implemented 
-  test_assert("minus_vec_vec_range_signed_pp", ((int)(0x1 -_s 0x1)) == 0);
-  test_assert("minus_vec_vec_range_signed_np", ((int)(0xa -_s 0x1)) == 9);
-  test_assert("minus_vec_vec_range_signed_pn", ((int)(0x3 -_s 0xe)) == 5);
-  test_assert("minus_vec_vec_range_signed_nn", ((int)(0x8 -_s 0x8)) == 0);*)
-  (* XXX not implemented 
-  test_assert("minus_vec_range_signed", ((bit[4])(0xe -_s 1)) == 0xd);
-  test_assert("minus_vec_range_range_signed", ((int)(0xe -_s 1)) == -3);
-  test_assert("minus_range_vec_signed", ((bit[4])(1 -_s 0xe)) == 0x3);
-  test_assert("minus_range_vec_range_signed", ((int)(1 -_s 0xe)) == 3);*)
-  (* returns (result, signed overflow, borrow in)*)
-  test_assert ("minus_overflow_vec_signed0", (((bit[4], bit, bit))(0x1 -_s 0x1)) == (0x0, false, false));
-  test_assert ("minus_overflow_vec_signed1", (((bit[4], bit, bit))(0x0 -_s 0x1)) == (0xf, true, true));
-  test_assert ("minus_overflow_vec_signed2", (((bit[4], bit, bit))(0x8 -_s 0x1)) == (0x7, false, false));
-  test_assert ("minus_overflow_vec_signed3", (((bit[4], bit, bit))(0x0 -_s 0x8)) == (0x8, true, true));
-
-  test_assert ("minus_overflow_vec_bit_signed0", (((bit[4], bit, bit))(0x1 -_s bitone)) == (0x0, false, false));
-  test_assert ("minus_overflow_vec_bit_signed1", (((bit[4], bit, bit))(0x0 -_s bitone)) == (0xf, true, true));
-  test_assert ("minus_overflow_vec_bit_signed2", (((bit[4], bit, bit))(0x8 -_s bitone)) == (0x7, false, false));
-  test_assert ("minus_overflow_vec_bit_signed3", (((bit[4], bit, bit))(0x8 -_s bitzero)) == (0x8, false, false));
-}
-
diff --git a/src/test/lib/tests/test_misc.sail b/src/test/lib/tests/test_misc.sail
deleted file mode 100644
index 5b4b6fd4..00000000
--- a/src/test/lib/tests/test_misc.sail
+++ /dev/null
@@ -1,19 +0,0 @@
-function unit test () = {
-  test_assert ("power0", (0 ** 3) == 0);
-  test_assert ("power1", (3 ** 0) == 1);
-  test_assert ("power2", (11 ** 17) == 505447028499293771);
-  (* XXX should be type error but isn't 
-  test_assert ("power-1", (1 ** -1) == 0); *)
-
-  test_assert ("abs_neg", (abs (-42)) == 42);
-  test_assert ("abs_zero", (abs (0)) == 0);
-  test_assert ("abs_pos", (abs (143)) == 143);
-
-  test_assert ("max", max(-1, 1) == 1);
-  test_assert ("min", min(-1, 1) == -1);
-
-  test_assert ("length0", length([]) == 0);
-  test_assert ("length1", length([bitzero]) == 1);
-  test_assert ("length2", length(0x1234) == 16);
-}
-
diff --git a/src/test/lib/tests/test_mod.sail b/src/test/lib/tests/test_mod.sail
deleted file mode 100644
index 7f078bae..00000000
--- a/src/test/lib/tests/test_mod.sail
+++ /dev/null
@@ -1,23 +0,0 @@
-function unit test () = {
-  test_assert ("modpospos_exact", (21 mod 7) == 0);
-  test_assert ("modposneg_exact", (21 mod -7) == 0);
-  test_assert ("modnegpos_exact", (-21 mod 7) == 0);
-  test_assert ("modnegneg_exact", (-21 mod -7) == 0);
-
-  test_assert ("modpospos_approx", (21 mod 8) == 5);
-  test_assert ("modposneg_approx", (21 mod -8) == 5);
-  test_assert ("modnegpos_approx", (-21 mod 8) == -5);
-  test_assert ("modnegneg_approx", (-21 mod -8) == -5);
- 
-  (* XXX how to test this? Type checker should catch?
-  test_assert ("mod_zero", (21 mod 0) == undefined); *)
-
-  test_assert("mod_vec_range_pos", (0x7 mod 5) == 2);
-  test_assert("mod_vec_range_neg", (0xf mod 5) == 0);
-
-  test_assert("mod_vec_pos", (0x7 mod 0x5) == 0x2);
-  test_assert("mod_vec_neg", (0xf mod 0x5) == 0x0);
-  test_assert("mod_vec_pos_neg", (0x7 mod 0x8) == 0x7);
-  test_assert("mod_vec_neg_neg", (0xf mod 0x8) == 0x7);
-}
-
diff --git a/src/test/lib/tests/test_mod_signed.sail b/src/test/lib/tests/test_mod_signed.sail
deleted file mode 100644
index 61acec17..00000000
--- a/src/test/lib/tests/test_mod_signed.sail
+++ /dev/null
@@ -1,26 +0,0 @@
-function unit test () = {
-  ();
-  (* XXX mod_signed does exist on ocaml shallow embedding...
-  test_assert ("mod_signed_pospos_exact", (21 mod_s 7) == 0);
-  test_assert ("mod_signed_posneg_exact", (21 mod_s -7) == 0);
-  test_assert ("mod_signed_negpos_exact", (-21 mod_s 7) == 0);
-  test_assert ("mod_signed_negneg_exact", (-21 mod_s -7) == 0);
-
-  test_assert ("mod_signed_pospos_approx", (21 mod_s 8) == 5);
-  test_assert ("mod_signed_posneg_approx", (21 mod_s -8) == 5);
-  test_assert ("mod_signed_negpos_approx", (-21 mod_s 8) == -5);
-  test_assert ("mod_signed_negneg_approx", (-21 mod_s -8) == -5);
- 
-  (* XXX how to test this? Type checker should catch?
-  test_assert ("mod_signed_zero", (21 mod_s 0) == undefined); *)
-
-  test_assert("mod_vec_range_signed_pos", (0x7 mod_s 5) == 2);
-  test_assert("mod_vec_range_signed_neg", (0xf mod_s 5) == -1);
-
-  test_assert("mod_vec_signed_pos", (0x7 mod_s 0x5) == 0x2);
-  test_assert("mod_vec_signed_neg", (0xf mod_s 0x5) == 0xf);
-  test_assert("mod_vec_signed_pos_neg", (0x7 mod_s 0x8) == 0x7);
-  test_assert("mod_vec_signed_neg_neg", (0xf mod_s 0x8) == 0x7);
-  *)
-}
-
diff --git a/src/test/lib/tests/test_multiply.sail b/src/test/lib/tests/test_multiply.sail
deleted file mode 100644
index 03adfa27..00000000
--- a/src/test/lib/tests/test_multiply.sail
+++ /dev/null
@@ -1,21 +0,0 @@
-function unit test () = {
-  test_assert ("multiply", 6 * 9 == 54);
-  test_assert ("multiply_vec", ((bit[8])(0x6 * 0xb)) == 0x42);
-  test_assert ("mult_range_vec", ((bit[8])(6 * 0xb)) == 0x42);
-  test_assert ("mult_vec_range", ((bit[8])(0x6 * 11)) == 0x42);
-  (* XXX mult_oveflow_vec missing *)
-
-  (* XXX not implmented
-  test_assert ("multiply_signed", 6 *_s 9 == 54); *)
-  test_assert ("multiply_vec_signed", ((bit[8])(0x6 *_s 0xb)) == 0xe2);
-  test_assert ("mult_range_vec_signed", ((bit[8])(6 *_s 0xb)) == 0xe2);
-  test_assert ("mult_vec_range_signed", ((bit[8])(0x6 *_s 11)) == 0xe2);
-
-  (* XXX don't think it's possible to set carryout out bit *)
-  test_assert ("mult_overflow_vec_signed0", (((bit[8], bit, bit)) (0xf *_s 0x2)) == (0xfe, false, false));
-  test_assert ("mult_overflow_vec_signed1", (((bit[8], bit, bit)) (0xf *_s 0xf)) == (0x01, false, false));
-  test_assert ("mult_overflow_vec_signed2", (((bit[8], bit, bit)) (0x8 *_s 0x8)) == (0x40, true, false));
-  test_assert ("mult_overflow_vec_signed3", (((bit[8], bit, bit)) (0x7 *_s 0x7)) == (0x31, true, false));
-  test_assert ("mult_overflow_vec_signed4", (((bit[8], bit, bit)) (0x8 *_s 0x7)) == (0xc8, true, false));
-}
-
diff --git a/src/test/lib/tests/test_neq.sail b/src/test/lib/tests/test_neq.sail
deleted file mode 100644
index e3ad50cf..00000000
--- a/src/test/lib/tests/test_neq.sail
+++ /dev/null
@@ -1,20 +0,0 @@
-function unit test () = {
-  test_assert("neq_bit00", not(false != bitzero));
-  test_assert("neq_bit01", false != bitone);
-  test_assert("neq_bit10", true != bitzero);
-  test_assert("neq_bit11", not(true != bitone));
-
-  test_assert("neq_vec0", 0x1 != 0x2);
-  test_assert("neq_vec1", not(0x2 != 0x2));
-  test_assert("neq_vec_range0", 0xf != 16);
-  test_assert("neq_vec_range0", 0x7 != 8);
-  test_assert("neq_vec_range1", not(0xf != 15));
-  (* XXX not implemented for ocaml
-  test_assert("neq_range_vec0", 16 != 0xf);
-  test_assert("neq_range_vec1", not(15 != 0xf)); *)
-  test_assert("neq_range0", 12 != 13);
-  test_assert("neq_range1", not(13 != 13));
-  test_assert("neq_tup0", (true, false) != (bitzero, bitzero));
-  test_assert("neq_tup1", not((true, false) != (bitone, bitzero)));
-}
-
diff --git a/src/test/lib/tests/test_not.sail b/src/test/lib/tests/test_not.sail
deleted file mode 100644
index 8ae2514f..00000000
--- a/src/test/lib/tests/test_not.sail
+++ /dev/null
@@ -1,8 +0,0 @@
-function unit test () = {
-  test_assert ("not_bit0", (not (bitzero)) == bitone);
-  test_assert ("not_bit1", (not (bitone)) == bitzero);
-
-  test_assert ("bitwise_not", (~ (0b01) == 0b10));
-  test_assert ("bitwise_not_bit0", ((~ (bitzero)) == bitone));
-  test_assert ("bitwise_not_bit1", ((~ (bitone)) == bitzero));
-}
diff --git a/src/test/lib/tests/test_oddments.sail b/src/test/lib/tests/test_oddments.sail
deleted file mode 100644
index 4c8fd086..00000000
--- a/src/test/lib/tests/test_oddments.sail
+++ /dev/null
@@ -1,14 +0,0 @@
-function unit test () = {
-  (* XXX this is weird, wrong type?
-  test_assert("is_one0", not(is_one(bitzero)));
-  test_assert("is_one1", is_one(bitone)); *)
-
-  test_assert("signed-1", signed(0xf) == -1);
-  test_assert("signed0",  signed(0x0) == 0);
-  test_assert("signed1",  signed(0x1) == 1);
-
-  test_assert("unsigned-1", unsigned(0xf) == 15);
-  test_assert("unsigned0",  unsigned(0x0) == 0);
-  test_assert("unsigned1",  unsigned(0x1) == 1);
-}
-
diff --git a/src/test/lib/tests/test_or.sail b/src/test/lib/tests/test_or.sail
deleted file mode 100644
index c48caedc..00000000
--- a/src/test/lib/tests/test_or.sail
+++ /dev/null
@@ -1,7 +0,0 @@
-function unit test () = {
-  test_assert ("bitwise_or", (0b0101 | 0b0011) == 0b0111);
-  test_assert ("bitwise_or_00", (bitzero | bitzero) == bitzero);
-  test_assert ("bitwise_or_01", (bitzero | bitone)  == bitone);
-  test_assert ("bitwise_or_10", (bitone  | bitzero) == bitone);
-  test_assert ("bitwise_or_11", (bitone  | bitone)  == bitone);
-}
diff --git a/src/test/lib/tests/test_quot_signed.sail b/src/test/lib/tests/test_quot_signed.sail
deleted file mode 100644
index 39259204..00000000
--- a/src/test/lib/tests/test_quot_signed.sail
+++ /dev/null
@@ -1,18 +0,0 @@
-function unit test () = {
-  test_assert ("quot_vec_signed_pospos_exact", ((bit[8])(0x15 quot_s 0x07)) == 0x03);
-  test_assert ("quot_vec_signed_posneg_exact", ((bit[8])(0x15 quot_s 0xf9)) == 0xfd);
-  test_assert ("quot_vec_signed_negpos_exact", ((bit[8])(0xeb quot_s 0x07)) == 0xfd);
-  test_assert ("quot_vec_signed_negneg_exact", ((bit[8])(0xeb quot_s 0xf9)) == 0x03);
-
-  test_assert ("quot_vec_signed_pospos_approx", ((bit[8])(0x15 quot_s 0x08)) == 0x02);
-  test_assert ("quot_vec_signed_posneg_approx", ((bit[8])(0x15 quot_s 0xf8)) == 0xfe);
-  test_assert ("quot_vec_signed_negpos_approx", ((bit[8])(0xeb quot_s 0x08)) == 0xfe);
-  test_assert ("quot_vec_signed_negneg_approx", ((bit[8])(0xeb quot_s 0xf8)) == 0x02);
-
-  test_assert ("quot_signed_overflow_vec", (((bit[8], bit, bit))(0x15 quot_s 0x08)) == (0x02, false, false));
-  (* XXX crashes shallow embedding due to undefined result
-  let (result, overflow, carry) = ((bit[8], bit, bit))(0x80 quot_s 0xff) in {
-    test_assert ("quot_signed_overflow_vec_ov", overflow);
-    test_assert ("quot_signed_overflow_vec_ca", carry);
-  };*)
-}
diff --git a/src/test/lib/tests/test_rightshift.sail b/src/test/lib/tests/test_rightshift.sail
deleted file mode 100644
index 7879a33e..00000000
--- a/src/test/lib/tests/test_rightshift.sail
+++ /dev/null
@@ -1,10 +0,0 @@
-function unit test () = {
-  test_assert ("rightshift_small0", (0x99 >> 0) == 0x99);
-  test_assert ("rightshift_small3", (0x99 >> 3) == 0x13);
-  test_assert ("rightshift_small7", (0x99 >> 7) == 0x01);
-  test_assert ("rightshift_small8", (0x99 >> 8) == 0x00); (* XXX fails on interp *)
-  test_assert ("rightshift_big0", (0x99999999999999999 >> 0) == 0x99999999999999999);
-  test_assert ("rightshift_big3", (0x99999999999999999 >> 3) == 0x13333333333333333);
-  test_assert ("rightshift_big7", (0x99999999999999999 >> 7) == 0x01333333333333333);
-  test_assert ("rightshift_big68", (0x99999999999999999 >> 68) == 0x00000000000000000); (* XXX fails on interp *)
-}
diff --git a/src/test/lib/tests/test_rotate.sail b/src/test/lib/tests/test_rotate.sail
deleted file mode 100644
index f0f8e45c..00000000
--- a/src/test/lib/tests/test_rotate.sail
+++ /dev/null
@@ -1,7 +0,0 @@
-function unit test () = { 
-  test_assert ("rotate0", (0x99 <<< 0) == 0x99); (* XXX fails on interp *)
-  test_assert ("rotate3", (0x99 <<< 3) == 0xcc);
-  test_assert ("rotate7", (0x99 <<< 7) == 0xcc);
-  test_assert ("rotate8", (0x99 <<< 8) == 0x99);
-}
-
diff --git a/src/test/lib/tests/test_xor.sail b/src/test/lib/tests/test_xor.sail
deleted file mode 100644
index 125b2f10..00000000
--- a/src/test/lib/tests/test_xor.sail
+++ /dev/null
@@ -1,7 +0,0 @@
-function unit test () = {
-  test_assert ("bitwise_xor", (0b0101 ^ 0b0011) == 0b0110);
-  test_assert ("bitwise_xor_00", (bitzero ^ bitzero) == bitzero);
-  test_assert ("bitwise_xor_01", (bitzero ^ bitone)  == bitone);
-  test_assert ("bitwise_xor_10", (bitone  ^ bitzero) == bitone);
-  test_assert ("bitwise_xor_11", (bitone  ^ bitone)  == bitzero);
-}
diff --git a/src/test/main.bin b/src/test/main.bin
deleted file mode 100755
index 3c9a56ed..00000000
--- a/src/test/main.bin
+++ /dev/null
diff --git a/src/test/mips/test_cp2_csetbounds_cases.elf b/src/test/mips/test_cp2_csetbounds_cases.elf
deleted file mode 100755
index 9ba8ab94..00000000
--- a/src/test/mips/test_cp2_csetbounds_cases.elf
+++ /dev/null
diff --git a/src/test/mips/test_cp2_x_jr_imprecise.elf b/src/test/mips/test_cp2_x_jr_imprecise.elf
deleted file mode 100755
index 23de20b4..00000000
--- a/src/test/mips/test_cp2_x_jr_imprecise.elf
+++ /dev/null
diff --git a/src/test/mips/test_raw_capinstructions.elf b/src/test/mips/test_raw_capinstructions.elf
deleted file mode 100755
index 120996bd..00000000
--- a/src/test/mips/test_raw_capinstructions.elf
+++ /dev/null
diff --git a/src/test/mips/test_slti.elf b/src/test/mips/test_slti.elf
deleted file mode 100755
index 7013930e..00000000
--- a/src/test/mips/test_slti.elf
+++ /dev/null
diff --git a/src/test/mips/test_tlb_load_0.elf b/src/test/mips/test_tlb_load_0.elf
deleted file mode 100755
index 107d5cda..00000000
--- a/src/test/mips/test_tlb_load_0.elf
+++ /dev/null
diff --git a/src/test/mips/test_tlb_probe.elf b/src/test/mips/test_tlb_probe.elf
deleted file mode 100755
index c827a9f4..00000000
--- a/src/test/mips/test_tlb_probe.elf
+++ /dev/null
diff --git a/src/test/mips/test_tlb_user_mode.elf b/src/test/mips/test_tlb_user_mode.elf
deleted file mode 100755
index adf06a85..00000000
--- a/src/test/mips/test_tlb_user_mode.elf
+++ /dev/null
diff --git a/src/test/pattern.sail b/src/test/pattern.sail
deleted file mode 100644
index 97e5a0ef..00000000
--- a/src/test/pattern.sail
+++ /dev/null
@@ -1,37 +0,0 @@
-
-register nat n 
-register nat x
-register nat y
-
-typedef wordsize = forall Nat 'n, 'n IN {8,16,32}. [|'n|]
-(* let forall Nat 'n. (wordsize<'n>) word = 8 *)
-
-function nat main () = {
-
-  (* works - x and y are set to 42 *)
-  n := 1;
-  y :=
-  (switch n {
-    case 0 -> { x := 21; x }
-    case 1 -> { x := 42; x } 
-    case z -> { x := 99; x }
-  }); 
-
-  switch word {
-    case 8 -> { x:= 32; }
-    case 16 -> { x:= 64; }
-    case 32 -> { x:= 128; }
-  };
-
-  switch 0b010101 {
-    case (0b01:(bit[1]) _:0b101) -> n:= 42
-    case _ -> n:=0
-  };
-
-  n := 3;
-  switch n {
-    case 0 -> { 21 }
-    case 1 -> { 42 } 
-    case x -> { 99 }
-  };
-}
diff --git a/src/test/power.sail b/src/test/power.sail
deleted file mode 100644
index 87a81ab9..00000000
--- a/src/test/power.sail
+++ /dev/null
@@ -1,4543 +0,0 @@
-
-(* XXX binary coded decimal *)
-(*function bit[12] DEC_TO_BCD ( (bit[10]) declet ) = {
-  (bit[4]) hundreds := 0;
-  (bit[4]) tens := 0;
-  (bit[4]) ones := 0;
-  foreach (i from 0 to 9) {
-    if hundreds >= 5 then hundreds := hundreds + 3;
-    if tens >= 5 then tens := tens + 3;
-    if ones >= 5 then ones := ones + 3;
-    hundreds := hundreds << 1;
-    hundreds[3] := tens[0];
-    tens := tens << 1;
-    tens[3] := ones[0];
-    ones := ones << 1;
-    ones[3] := declet[i] };
-  hundreds:tens:ones }*)
-
-function bit[12] DEC_TO_BCD ( (bit[10]) [p,q,r,s,t,u,v,w,x,y]) = {
-  a := ((~(s) & v & w) | (t & v & w & s) | (v & w & ~(x)));
-  b := ((p & s & x & ~(t)) | (p & ~(w)) | (p & ~(v)));
-  c := ((q & s & x & ~(t)) | (q & ~(w)) | (q & ~(v)));
-  d := r;
-
-  e := ((v & ~(w) & x) | (s & v & w & x) | (~(t) & v & x & w));
-  f := ((p & t & v & w & x & ~(s)) | (s & ~(x) & v) | (s & ~(v)));
-  g := ((q & t & w & v & x & ~(s)) | (t & ~(x) & v) | (t & ~(v)));
-  h := u;
-
-  i := ((t & v & w & x) | (s & v & w & x) | (v & ~(w) & ~(x)));
-  j := ((p & ~(s) & ~(t) & w & v) | (s & v & ~(w) & x) | (p & w & ~(x) & v) | (w & ~(v)));
-  k := ((q & ~(s) & ~(t) & v & w) | (t & v & ~(w) & x) | (q & v & w & ~(x)) | (x & ~(v)));
-  m := y;
-  [a,b,c,d,e,f,g,h,i,j,k,m]
-}
-
-(*function bit[10] BCD_TO_DEC ( (bit[12]) bcd ) = 
-   (bit[10]) (([|2** 10|]) (bcd[0..3] * 100)) + ([|2** 7|]) ((([|2** 7|]) (bcd[4..7] * 10)) + bcd[8..11])
-*)
-
-function bit[10] BCD_TO_DEC ( (bit[12]) [a,b,c,d,e,f,g,h,i,j,k,m] ) = {
-   p := ((f & a & i & ~(e)) | (j & a & ~(i)) | (b & ~(a)));
-   q := ((g & a & i & ~(e)) | (k & a & ~(i)) | (c & ~(a)));
-   r := d;
-   s := ((j & ~(a) & e & ~(i)) | (f & ~(i) & ~(e)) | (f & ~(a) & ~(e)) | (e & i));
-   t := ((k & ~(a) & e & ~(i)) | (g & ~(i) & ~(e)) | (g & ~(a) & ~(e)) | (a & i));
-   u := h;
-   v := (a | e | i);
-   w := ((~(e) & j & ~(i)) | (e & i) | a);
-   x := ((~(a) & k & ~(i)) | (a & i) | e);
-   y := m;
-   [p,q,r,s,t,u,v,w,x,y]
-}
-
-(* XXX carry out *)
-function forall Nat 'a . bit carry_out ( (bit['a]) _,carry ) = carry
-(* XXX Storage control *)
-function forall Type 'a . 'a real_addr ( x ) = x
-(* XXX For stvxl and lvxl - what does that do? *)
-function forall Type 'a . unit mark_as_not_likely_to_be_needed_again_anytime_soon ( x ) = ()
-
-(* XXX *)
-val extern forall Nat 'k, Nat 'r,
-  0 <= 'k, 'k <= 64, 'r + 'k = 64.
-  (bit[64], [|'k|]) -> [|0:'r|] effect pure countLeadingZeroes
-
-function forall Nat 'n, Nat 'm .
-  bit['m] EXTS_EXPLICIT((bit['n]) v, ([:'m:]) m) =
-  (v[0] ^^ (m - length(v))) : v
-
-val forall Nat 'n, Nat 'm, 0 <= 'n, 'n <= 'm, 'm <= 63 .
-  ([|'n|],[|'m|]) -> bit[64]
-  effect pure
-  MASK
-
-function (bit[64]) MASK(start, stop) = {
-  (bit[64]) mask_temp := 0;
-  if(start > stop) then {
-    mask_temp[start .. 63] := bitone ^^ (64 - start);
-    mask_temp[0 .. stop] := bitone ^^ (stop + 1);
-  } else {
-    mask_temp[start .. stop ] := bitone ^^ (stop - start + 1);
-  };
-  mask_temp;
-}
-
-val forall Nat 'n, 0 <= 'n, 'n <= 63 .
-  (bit[64], [|'n|]) -> bit[64] effect pure ROTL
-
-function (bit[64]) ROTL(v, n) = v[n .. 63] : v[0 .. (n - 1)]
-
-(* Branch facility registers *)
-
-typedef cr = register bits [ 32 : 63 ] {
-  32 .. 35 : CR0;
-    32 : LT; 33 : GT; 34 : EQ; 35 : SO;
-  36 .. 39 : CR1;
-    36 : FX; 37 : FEX; 38 : VX; 39 : OX;
-  40 .. 43 : CR2;
-  44 .. 47 : CR3;
-  48 .. 51 : CR4;
-  52 .. 55 : CR5;
-  56 .. 59 : CR6;
-    (* name clashing - do we need hierarchical naming for fields, or do
-    we just don't care? LT, GT, etc. are not used in the code anyway.
-    56 : LT; 57 : GT; 58 : EQ; 59 : SO;
-    *)
-  60 .. 63 : CR7;
-}
-register (cr) CR
-
-register (bit[64]) CTR
-register (bit[64]) LR
-
-typedef xer = register bits [ 0 : 63 ] {
-  32 : SO;
-  33 : OV;
-  34 : CA;
-}
-register (xer) XER
-
-register alias CA = XER.CA
-
-(* Fixed-point registers *)
-
-register (bit[64]) GPR0
-register (bit[64]) GPR1
-register (bit[64]) GPR2
-register (bit[64]) GPR3
-register (bit[64]) GPR4
-register (bit[64]) GPR5
-register (bit[64]) GPR6
-register (bit[64]) GPR7
-register (bit[64]) GPR8
-register (bit[64]) GPR9
-register (bit[64]) GPR10
-register (bit[64]) GPR11
-register (bit[64]) GPR12
-register (bit[64]) GPR13
-register (bit[64]) GPR14
-register (bit[64]) GPR15
-register (bit[64]) GPR16
-register (bit[64]) GPR17
-register (bit[64]) GPR18
-register (bit[64]) GPR19
-register (bit[64]) GPR20
-register (bit[64]) GPR21
-register (bit[64]) GPR22
-register (bit[64]) GPR23
-register (bit[64]) GPR24
-register (bit[64]) GPR25
-register (bit[64]) GPR26
-register (bit[64]) GPR27
-register (bit[64]) GPR28
-register (bit[64]) GPR29
-register (bit[64]) GPR30
-register (bit[64]) GPR31
-
-let (vector <0, 32, inc, (register<(bit[64])>) >) GPR =
-  [ GPR0, GPR1, GPR2, GPR3, GPR4, GPR5, GPR6, GPR7, GPR8, GPR9, GPR10,
-  GPR11, GPR12, GPR13, GPR14, GPR15, GPR16, GPR17, GPR18, GPR19, GPR20,
-  GPR21, GPR22, GPR23, GPR24, GPR25, GPR26, GPR27, GPR28, GPR29, GPR30, GPR31
-  ]
-
-register (bit[32:63]) VRSAVE
-
-register (bit[64]) SPRG3
-register (bit[64]) SPRG4
-register (bit[64]) SPRG5
-register (bit[64]) SPRG6
-register (bit[64]) SPRG7
-
-let (vector <0, 1024, inc, (register<(bit[64])>) >) SPR =
-  [ 1=XER, 8=LR, 9=CTR(*, 256=VRSAVE (*32 bit, so not 64, caught by type checker at last*)*), 259=SPRG3, 260=SPRG4, 261=SPRG5, 262=SPRG6, 263=SPRG7
-  ]
-
-(* XXX DCR is implementation-dependent; also, some DCR are only 32 bits
- instead of 64, and mtdcrux/mfdcrux do special tricks in that case, not
- shown in pseudo-code. We just define two dummy DCR here, using sparse
- vector definition. *)
-register (vector <0, 64, inc, bit>) DCR0
-register (vector <0, 64, inc, bit>) DCR1
-let (vector <0, 1024, inc, (register<(vector<0, 64, inc, bit>)>) >) DCR =
-  [ 0=DCR0, 1=DCR1 ; default=undefined]
-
-(* Floating-point registers *)
-
-register (bit[64]) FPR0
-register (bit[64]) FPR1
-register (bit[64]) FPR2
-register (bit[64]) FPR3
-register (bit[64]) FPR4
-register (bit[64]) FPR5
-register (bit[64]) FPR6
-register (bit[64]) FPR7
-register (bit[64]) FPR8
-register (bit[64]) FPR9
-register (bit[64]) FPR10
-register (bit[64]) FPR11
-register (bit[64]) FPR12
-register (bit[64]) FPR13
-register (bit[64]) FPR14
-register (bit[64]) FPR15
-register (bit[64]) FPR16
-register (bit[64]) FPR17
-register (bit[64]) FPR18
-register (bit[64]) FPR19
-register (bit[64]) FPR20
-register (bit[64]) FPR21
-register (bit[64]) FPR22
-register (bit[64]) FPR23
-register (bit[64]) FPR24
-register (bit[64]) FPR25
-register (bit[64]) FPR26
-register (bit[64]) FPR27
-register (bit[64]) FPR28
-register (bit[64]) FPR29
-register (bit[64]) FPR30
-register (bit[64]) FPR31
-
-let (vector <0, 32, inc, (register<(bit[64])>) >) FPR =
-  [ FPR0, FPR1, FPR2, FPR3, FPR4, FPR5, FPR6, FPR7, FPR8, FPR9, FPR10,
-  FPR11, FPR12, FPR13, FPR14, FPR15, FPR16, FPR17, FPR18, FPR19, FPR20,
-  FPR21, FPR22, FPR23, FPR24, FPR25, FPR26, FPR27, FPR28, FPR29, FPR30, FPR31
-  ]
-
-typedef fpscr = register bits [ 0 : 63 ] {
-  32 : FX;
-  33 : FEX;
-  34 : VX;
-  35 : OX;
-  36 : UX;
-  37 : ZX;
-  38 : XX;
-  39 : VXSNAN;
-  40 : VXISI;
-  41 : VXIDI;
-  42 : VXZDZ;
-  43 : VXIMZ;
-  44 : VXVC;
-  45 : FR;
-  46 : FI;
-  47 .. 51 : FPRF;
-  47 : C;
-  48 .. 51 : FPCC;
-    48 : FL; 49 : FG; 50 : FE; 51 : FU;
-  53 : VXSOFT;
-  54 : VXSQRT;
-  55 : VXCVI;
-  56 : VE;
-  57 : OE;
-  58 : UE;
-  59 : ZE;
-  60 : XE;
-  61 : NI;
-  62 .. 63 : RN;
-}
-register (fpscr) FPSCR
-
-(* Pair-wise access to FPR registers *)
-
-register alias FPRp0 = FPR0 : FPR1
-register alias FPRp2 = FPR2 : FPR3
-register alias FPRp4 = FPR4 : FPR5
-register alias FPRp6 = FPR6 : FPR7
-register alias FPRp8 = FPR8 : FPR9
-register alias FPRp10 = FPR10 : FPR11
-register alias FPRp12 = FPR12 : FPR13
-register alias FPRp14 = FPR14 : FPR15
-register alias FPRp16 = FPR16 : FPR17
-register alias FPRp18 = FPR18 : FPR19
-register alias FPRp20 = FPR20 : FPR21
-register alias FPRp22 = FPR22 : FPR23
-register alias FPRp24 = FPR24 : FPR25
-register alias FPRp26 = FPR26 : FPR27
-register alias FPRp28 = FPR28 : FPR29
-register alias FPRp30 = FPR30 : FPR31
-
-let (vector <0, 32, inc, (register<(bit[128])>)>) FPRp =
-  [ 0 = FPRp0, 2 = FPRp2, 4 = FPRp4, 6 = FPRp6, 8 = FPRp8, 10 = FPRp10,
-  12 = FPRp12, 14 = FPRp14, 16 = FPRp16, 18 = FPRp18, 20 = FPRp20, 22 =
-  FPRp22, 24 = FPRp24, 26 = FPRp26, 28 = FPRp28, 30 = FPRp30 ]
-
-
-val bit[32] -> bit[64] effect pure DOUBLE
-val bit[64] -> bit[32] effect { undef } SINGLE
-
-function  bit[64] DOUBLE word = {
-  (bit[64]) temp := 0;
-  if word[1..8] > 0 & word[1..8] < 255
-  then {
-    temp[0..1] := word[0..1];
-    temp[2] := ~(word[1]);
-    temp[3] := ~(word[1]);
-    temp[4] := ~(word[1]);
-    temp[5..63] := word[2..31] : 0b00000000000000000000000000000;
-  } else if word[1..8] == 0 & word[9..31] != 0 
-  then {
-    sign := word[0];
-    exp := 0 - 126;
-    (bit[53]) frac := 0b0 : word[9..31] : 0b00000000000000000000000000000;
-    foreach (i from 0 to 52) {
-      if frac[0] == 0 
-      then { frac[0..52] := frac[1..52] : 0b0;
-             exp := exp - 1; }
-      else ()
-     };
-     temp[0] := sign;
-     temp[1..11] := (bit[1:11]) exp + 1023;
-     temp[12..63] := frac[1..52];
-   } else {
-     temp[0..1] := word[0..1];
-     temp[2] := word[1];
-     temp[3] := word[1];
-     temp[4] := word[1];
-     temp[5..63] := word[2..31] : 0b00000000000000000000000000000;
-   };
-   temp
-}
-
-function bit[32] SINGLE ((bit[64]) frs) = {
-  (bit[32]) word := 0;
-  if (frs[1..11] > 896) | (frs[1..63] == 0) 
-  then { word[0..1] := frs[0..1];
-         word[2..31] := frs[5..34]; }
-  else if (874 <= frs[1..11]) & (frs[1..11] <= 896)
-  then { 
-   sign := frs[0];
-   (bit[11]) exp := frs[1..11] - 1023;
-   (bit[53]) frac := 0b1 : frs[12..63];
-   foreach (i from 0 to 53) {
-     if exp < (0 - 126) 
-     then { frac[0..52] := 0b0 : frac[0..51];
-            exp := exp + 1; }
-     else ()};
-   } else word := undefined;
-   word   
-}
-
-(* Vector registers *)
-
-register (bit[128]) VR0
-register (bit[128]) VR1
-register (bit[128]) VR2
-register (bit[128]) VR3
-register (bit[128]) VR4
-register (bit[128]) VR5
-register (bit[128]) VR6
-register (bit[128]) VR7
-register (bit[128]) VR8
-register (bit[128]) VR9
-register (bit[128]) VR10
-register (bit[128]) VR11
-register (bit[128]) VR12
-register (bit[128]) VR13
-register (bit[128]) VR14
-register (bit[128]) VR15
-register (bit[128]) VR16
-register (bit[128]) VR17
-register (bit[128]) VR18
-register (bit[128]) VR19
-register (bit[128]) VR20
-register (bit[128]) VR21
-register (bit[128]) VR22
-register (bit[128]) VR23
-register (bit[128]) VR24
-register (bit[128]) VR25
-register (bit[128]) VR26
-register (bit[128]) VR27
-register (bit[128]) VR28
-register (bit[128]) VR29
-register (bit[128]) VR30
-register (bit[128]) VR31
-
-let (vector <0, 32, inc, (register<(bit[128])>) >) VR =
-  [ VR0, VR1, VR2, VR3, VR4, VR5, VR6, VR7, VR8, VR9, VR10,
-  VR11, VR12, VR13, VR14, VR15, VR16, VR17, VR18, VR19, VR20,
-  VR21, VR22, VR23, VR24, VR25, VR26, VR27, VR28, VR29, VR30, VR31
-  ]
-
-typedef vscr = register bits [ 96 : 127 ] {
-  111 : NJ;
-  127 : SAT;
-}
-register (vscr) VSCR
-
-(*(* XXX extend with zeroes -- the resulting size in completely unknown and depends of context *)
-val extern forall Nat 'n, Nat 'm. (implicit<'m>,bit['n]) -> bit['m] effect pure EXTZ*)
-
-(* Chop has a very weird definition where the resulting size depends of
-   context, but in practice it is used with the following definition everywhere,
-   except in vaddcuw which probably needs to be patched accordingly. *)
-val forall Nat 'n, Nat 'm, 'm <= 'n. (bit['n], [:'m:]) -> bit['m] effect pure Chop
-function forall Nat 'n, Nat 'm. (bit['m]) Chop(x, y) = x[0..y]
-
-val forall Nat 'o, Nat 'n, Nat 'm, Nat 'k, 'n <= 0.
-  (implicit<'k>, [:'o:], [:'n:], [|'m|]) -> bit['k] effect { wreg } Clamp
-
-function forall Nat 'o,Nat 'n, Nat 'm, Nat 'k, 'n <= 0. (bit['k])
-Clamp(([:'o:]) x, ([:'n:]) y, ([|'m|]) z) = {
-  ([|'n:'m|]) result := 0;
-  if (x<y) then {
-    result := y;
-    VSCR.SAT := 1;
-  } else if (x > z) then {
-    result := z;
-    VSCR.SAT := 1;
-  } else {
-    result := x;
-  };
-  (bit['k]) result;
-}
-
-(* XXX *)
-val extern bit[32] -> bit[32] effect pure RoundToSPIntCeil
-val extern bit[32] -> bit[32] effect pure RoundToSPIntFloor
-val extern bit[32] -> bit[32] effect pure RoundToSPIntNear
-val extern bit[32] -> bit[32] effect pure RoundToSPIntTrunc
-val extern bit[32] -> bit[32] effect pure RoundToNearSP
-val extern bit[32] -> bit[32] effect pure ReciprocalEstimateSP
-val extern bit[32] -> bit[32] effect pure ReciprocalSquareRootEstimateSP
-val extern bit[32] -> bit[32] effect pure LogBase2EstimateSP
-val extern bit[32] -> bit[32] effect pure Power2EstimateSP
-val extern (bit[32], bit[5]) -> bit[32] effect pure ConvertSPtoSXWsaturate
-val extern (bit[32], bit[5]) -> bit[32] effect pure ConvertSPtoUXWsaturate
-
-
-register (bit[64]) NIA (* next instruction address *)
-register (bit[64]) CIA (* current instruction address *)
-
-
-val extern forall Nat 'n. ( bit[64] , [|'n|] , bit[8*'n]) -> unit effect { wmv } MEMw
-val extern forall Nat 'n. ( bit[64] , [|'n|] ) -> (bit[8 * 'n]) effect { rmem } MEMr
-val extern forall Nat 'n. ( bit[64] , [|'n|] ) -> (bit[8 * 'n]) effect { rmem } MEMr_reserve
-val extern forall Nat 'n. ( bit[64] , [|'n|] , bit[8*'n]) -> bool effect { wmv } MEMw_conditional
-
-(* announce write address for plain write *)
-val extern forall Nat 'N, 'N IN {1,2,4,8,16}. (bit[64] (*address*), [:'N:] (*size*)) -> unit effect {eamem} MEMw_EA
-
-(* announce write address for write conditional *)
-val extern forall Nat 'N, 'N IN {1,2,4,8,16}. (bit[64] (*address*), [:'N:] (*size*)) -> unit effect {eamem} MEMw_EA_cond
-
-val extern unit -> unit effect { barr } I_Sync
-val extern unit -> unit effect { barr } H_Sync (*corresponds to Sync in barrier kinds*)
-val extern unit -> unit effect { barr } LW_Sync
-val extern unit -> unit effect { barr } EIEIO_Sync
-
-val extern unit -> unit effect { depend } recalculate_dependency
-
-val forall Nat 'n, Nat 'm, 'n *8 = 'm. (implicit<'m>,(bit['m])) -> (bit['m]) effect pure byte_reverse
-function forall Nat 'n, Nat 'm, 'n*8 = 'm. (bit['m]) effect pure byte_reverse((bit['m]) input) = {
-  (bit['m]) output := 0;
-  j := length(input);
-  foreach (i from 0 to (length(input)) by 8) {
-   output[i..i+7] := input[j - 7 ..j];
-   j := j - 8; };
-  output
-}  
-
-(* XXX effect for trap? *)
-val extern unit -> unit effect {escape} trap
-
-register (bit[1]) mode64bit
-register (bit[1]) bigendianmode
-
-val (bit[64],bit) -> unit effect {rreg,wreg} set_overflow_cr0 
-function (unit) set_overflow_cr0(target_register,new_xer_so) = {
-  m:= 0;
-  (bit[3]) c:= 0;
-  (bit[64]) zero := 0;
-  (if mode64bit
-   then m := 0
-   else m := 32);
-  (if target_register[m..63] <_s zero[m..63]
-  then c := 0b100
-  else if target_register[m..63] >_s zero[m..63] 
-  then c := 0b010
-  else c := 0b001);
-  CR.CR0 := c:[new_xer_so]
-}
-
-function (unit) set_SO_OV(overflow) =  {
-  XER.OV := overflow;
-  XER.SO := (XER.SO | overflow);
-}
-
-function forall Nat 'n. (bit['n]) zero_or_undef ((bit['n]) x) = {
-  (bit['n]) out := 0;
-  foreach (i from 0 to ((length(x)) - 1)) {
-   out[i] := if x[i] then undefined else 0
-  };
-  out
-}
-
-scattered function unit execute
-scattered typedef ast = const union
-
-val bit[32] -> option<ast> effect pure decode
-
-scattered function option<ast> decode
-
-union ast member (bit[24], bit, bit) B
-
-function clause decode (0b010010 : (bit[24]) LI : [AA] : [LK] as instr) = Some(B(LI,AA,LK))
-
-function clause execute (B (LI, AA, LK)) =
-  {
-    if AA then NIA := EXTS(LI : 0b00) else NIA := CIA + EXTS(LI : 0b00);
-    if LK then LR := CIA + 4 else ()
-  }
-
-union ast member (bit[5], bit[5], bit[14], bit, bit) Bc
-
-function clause decode (0b010000 :
-(bit[5]) BO :
-(bit[5]) BI :
-(bit[14]) BD :
-[AA] :
-[LK] as instr) =
-  Some(Bc(BO,BI,BD,AA,LK))
-
-function clause execute (Bc (BO, BI, BD, AA, LK)) =
-  {
-    if mode64bit then M := 0 else M := 32;
-    (bit[64]) ctr_temp := CTR;
-    if ~(BO[2])
-    then {
-      ctr_temp := ctr_temp - 1;
-      CTR := ctr_temp
-    }
-    else ();
-    ctr_ok := (BO[2] | ~(ctr_temp[M .. 63] == 0) ^ BO[3]);
-    cond_ok := (BO[0] | CR[BI + 32] ^ ~(BO[1]));
-    if ctr_ok & cond_ok
-    then if AA then NIA := EXTS(BD : 0b00) else NIA := CIA + EXTS(BD : 0b00)
-    else ();
-    if LK then LR := CIA + 4 else ()
-  }
-
-union ast member (bit[5], bit[5], bit[2], bit) Bclr
-
-function clause decode (0b010011 :
-(bit[5]) BO :
-(bit[5]) BI :
-(bit[3]) _ :
-(bit[2]) BH :
-0b0000010000 :
-[LK] as instr) =
-  Some(Bclr(BO,BI,BH,LK))
-
-function clause execute (Bclr (BO, BI, BH, LK)) =
-  {
-    if mode64bit then M := 0 else M := 32;
-    (bit[64]) ctr_temp := CTR;
-    if ~(BO[2])
-    then {
-      ctr_temp := ctr_temp - 1;
-      CTR := ctr_temp
-    }
-    else ();
-    ctr_ok := (BO[2] | ~(ctr_temp[M .. 63] == 0) ^ BO[3]);
-    cond_ok := (BO[0] | CR[BI + 32] ^ ~(BO[1]));
-    if ctr_ok & cond_ok then NIA := LR[0 .. 61] : 0b00 else ();
-    if LK then LR := CIA + 4 else ()
-  }
-
-union ast member (bit[5], bit[5], bit[2], bit) Bcctr
-
-function clause decode (0b010011 :
-(bit[5]) BO :
-(bit[5]) BI :
-(bit[3]) _ :
-(bit[2]) BH :
-0b1000010000 :
-[LK] as instr) =
-  Some(Bcctr(BO,BI,BH,LK))
-
-function clause execute (Bcctr (BO, BI, BH, LK)) =
-  {
-    cond_ok := (BO[0] | CR[BI + 32] ^ ~(BO[1]));
-    if cond_ok then NIA := CTR[0 .. 61] : 0b00 else ();
-    if LK then LR := CIA + 4 else ()
-  }
-
-union ast member (bit[5], bit[5], bit[5]) Crand
-
-function clause decode (0b010011 :
-(bit[5]) BT :
-(bit[5]) BA :
-(bit[5]) BB :
-0b0100000001 :
-(bit[1]) _ as instr) =
-  Some(Crand(BT,BA,BB))
-
-function clause execute (Crand (BT, BA, BB)) = CR[BT + 32] := (CR[BA + 32] & CR[BB + 32])
-
-union ast member (bit[5], bit[5], bit[5]) Crnand
-
-function clause decode (0b010011 :
-(bit[5]) BT :
-(bit[5]) BA :
-(bit[5]) BB :
-0b0011100001 :
-(bit[1]) _ as instr) =
-  Some(Crnand(BT,BA,BB))
-
-function clause execute (Crnand (BT, BA, BB)) = CR[BT + 32] := ~(CR[BA + 32] & CR[BB + 32])
-
-union ast member (bit[5], bit[5], bit[5]) Cror
-
-function clause decode (0b010011 :
-(bit[5]) BT :
-(bit[5]) BA :
-(bit[5]) BB :
-0b0111000001 :
-(bit[1]) _ as instr) =
-  Some(Cror(BT,BA,BB))
-
-function clause execute (Cror (BT, BA, BB)) = CR[BT + 32] := (CR[BA + 32] | CR[BB + 32])
-
-union ast member (bit[5], bit[5], bit[5]) Crxor
-
-function clause decode (0b010011 :
-(bit[5]) BT :
-(bit[5]) BA :
-(bit[5]) BB :
-0b0011000001 :
-(bit[1]) _ as instr) =
-  Some(Crxor(BT,BA,BB))
-
-function clause execute (Crxor (BT, BA, BB)) = CR[BT + 32] := CR[BA + 32] ^ CR[BB + 32]
-
-union ast member (bit[5], bit[5], bit[5]) Crnor
-
-function clause decode (0b010011 :
-(bit[5]) BT :
-(bit[5]) BA :
-(bit[5]) BB :
-0b0000100001 :
-(bit[1]) _ as instr) =
-  Some(Crnor(BT,BA,BB))
-
-function clause execute (Crnor (BT, BA, BB)) = CR[BT + 32] := ~(CR[BA + 32] | CR[BB + 32])
-
-union ast member (bit[5], bit[5], bit[5]) Creqv
-
-function clause decode (0b010011 :
-(bit[5]) BT :
-(bit[5]) BA :
-(bit[5]) BB :
-0b0100100001 :
-(bit[1]) _ as instr) =
-  Some(Creqv(BT,BA,BB))
-
-function clause execute (Creqv (BT, BA, BB)) = CR[BT + 32] := CR[BA + 32] ^ ~(CR[BB + 32])
-
-union ast member (bit[5], bit[5], bit[5]) Crandc
-
-function clause decode (0b010011 :
-(bit[5]) BT :
-(bit[5]) BA :
-(bit[5]) BB :
-0b0010000001 :
-(bit[1]) _ as instr) =
-  Some(Crandc(BT,BA,BB))
-
-function clause execute (Crandc (BT, BA, BB)) = CR[BT + 32] := (CR[BA + 32] & ~(CR[BB + 32]))
-
-union ast member (bit[5], bit[5], bit[5]) Crorc
-
-function clause decode (0b010011 :
-(bit[5]) BT :
-(bit[5]) BA :
-(bit[5]) BB :
-0b0110100001 :
-(bit[1]) _ as instr) =
-  Some(Crorc(BT,BA,BB))
-
-function clause execute (Crorc (BT, BA, BB)) = CR[BT + 32] := (CR[BA + 32] | ~(CR[BB + 32]))
-
-union ast member (bit[3], bit[3]) Mcrf
-
-function clause decode (0b010011 :
-(bit[3]) BF :
-(bit[2]) _ :
-(bit[3]) BFA :
-(bit[2]) _ :
-(bit[5]) _ :
-0b0000000000 :
-(bit[1]) _ as instr) =
-  Some(Mcrf(BF,BFA))
-
-function clause execute (Mcrf (BF, BFA)) =
-  CR[4 * BF + 32..4 * BF + 35] := CR[4 * BFA + 32 .. 4 * BFA + 35]
-
-union ast member (bit[7]) Sc
-
-function clause decode (0b010001 :
-(bit[5]) _ :
-(bit[5]) _ :
-(bit[4]) _ :
-(bit[7]) LEV :
-(bit[3]) _ :
-0b1 :
-(bit[1]) _ as instr) =
-  Some(Sc(LEV))
-
-function clause execute (Sc (LEV)) = ()
-
-union ast member (bit[7]) Scv
-
-function clause decode (0b010001 :
-(bit[5]) _ :
-(bit[5]) _ :
-(bit[4]) _ :
-(bit[7]) LEV :
-(bit[3]) _ :
-0b0 :
-0b1 as instr) =
-  Some(Scv(LEV))
-
-function clause execute (Scv (LEV)) = ()
-
-union ast member (bit[5], bit[5], bit[16]) Lbz
-
-function clause decode (0b100010 :
-(bit[5]) RT :
-(bit[5]) RA :
-(bit[16]) D as instr) =
-  Some(Lbz(RT,RA,D))
-
-function clause execute (Lbz (RT, RA, D)) =
-  {
-    (bit[64]) b := 0;
-    (bit[64]) EA := 0;
-    if RA == 0 then b := 0 else b := GPR[RA];
-    EA := b + EXTS(D);
-    GPR[RT] := 0b00000000000000000000000000000000000000000000000000000000 : MEMr(EA,1)
-  }
-
-union ast member (bit[5], bit[5], bit[5]) Lbzx
-
-function clause decode (0b011111 :
-(bit[5]) RT :
-(bit[5]) RA :
-(bit[5]) RB :
-0b0001010111 :
-(bit[1]) _ as instr) =
-  Some(Lbzx(RT,RA,RB))
-
-function clause execute (Lbzx (RT, RA, RB)) =
-  {
-    (bit[64]) b := 0;
-    (bit[64]) EA := 0;
-    if RA == 0 then b := 0 else b := GPR[RA];
-    EA := b + GPR[RB];
-    GPR[RT] := 0b00000000000000000000000000000000000000000000000000000000 : MEMr(EA,1)
-  }
-
-union ast member (bit[5], bit[5], bit[16]) Lbzu
-
-function clause decode (0b100011 :
-(bit[5]) RT :
-(bit[5]) RA :
-(bit[16]) D as instr) =
-  Some(Lbzu(RT,RA,D))
-
-function clause execute (Lbzu (RT, RA, D)) =
-  {
-    (bit[64]) EA := 0;
-    EA := GPR[RA] + EXTS(D);
-    GPR[RA] := EA;
-    GPR[RT] := 0b00000000000000000000000000000000000000000000000000000000 : MEMr(EA,1)
-  }
-
-union ast member (bit[5], bit[5], bit[5]) Lbzux
-
-function clause decode (0b011111 :
-(bit[5]) RT :
-(bit[5]) RA :
-(bit[5]) RB :
-0b0001110111 :
-(bit[1]) _ as instr) =
-  Some(Lbzux(RT,RA,RB))
-
-function clause execute (Lbzux (RT, RA, RB)) =
-  {
-    (bit[64]) EA := 0;
-    EA := GPR[RA] + GPR[RB];
-    GPR[RA] := EA;
-    GPR[RT] := 0b00000000000000000000000000000000000000000000000000000000 : MEMr(EA,1)
-  }
-
-union ast member (bit[5], bit[5], bit[16]) Lhz
-
-function clause decode (0b101000 :
-(bit[5]) RT :
-(bit[5]) RA :
-(bit[16]) D as instr) =
-  Some(Lhz(RT,RA,D))
-
-function clause execute (Lhz (RT, RA, D)) =
-  {
-    (bit[64]) b := 0;
-    (bit[64]) EA := 0;
-    if RA == 0 then b := 0 else b := GPR[RA];
-    EA := b + EXTS(D);
-    GPR[RT] := 0b000000000000000000000000000000000000000000000000 : MEMr(EA,2)
-  }
-
-union ast member (bit[5], bit[5], bit[5]) Lhzx
-
-function clause decode (0b011111 :
-(bit[5]) RT :
-(bit[5]) RA :
-(bit[5]) RB :
-0b0100010111 :
-(bit[1]) _ as instr) =
-  Some(Lhzx(RT,RA,RB))
-
-function clause execute (Lhzx (RT, RA, RB)) =
-  {
-    (bit[64]) b := 0;
-    (bit[64]) EA := 0;
-    if RA == 0 then b := 0 else b := GPR[RA];
-    EA := b + GPR[RB];
-    GPR[RT] := 0b000000000000000000000000000000000000000000000000 : MEMr(EA,2)
-  }
-
-union ast member (bit[5], bit[5], bit[16]) Lhzu
-
-function clause decode (0b101001 :
-(bit[5]) RT :
-(bit[5]) RA :
-(bit[16]) D as instr) =
-  Some(Lhzu(RT,RA,D))
-
-function clause execute (Lhzu (RT, RA, D)) =
-  {
-    (bit[64]) EA := 0;
-    EA := GPR[RA] + EXTS(D);
-    GPR[RA] := EA;
-    GPR[RT] := 0b000000000000000000000000000000000000000000000000 : MEMr(EA,2)
-  }
-
-union ast member (bit[5], bit[5], bit[5]) Lhzux
-
-function clause decode (0b011111 :
-(bit[5]) RT :
-(bit[5]) RA :
-(bit[5]) RB :
-0b0100110111 :
-(bit[1]) _ as instr) =
-  Some(Lhzux(RT,RA,RB))
-
-function clause execute (Lhzux (RT, RA, RB)) =
-  {
-    (bit[64]) EA := 0;
-    EA := GPR[RA] + GPR[RB];
-    GPR[RA] := EA;
-    GPR[RT] := 0b000000000000000000000000000000000000000000000000 : MEMr(EA,2)
-  }
-
-union ast member (bit[5], bit[5], bit[16]) Lha
-
-function clause decode (0b101010 :
-(bit[5]) RT :
-(bit[5]) RA :
-(bit[16]) D as instr) =
-  Some(Lha(RT,RA,D))
-
-function clause execute (Lha (RT, RA, D)) =
-  {
-    (bit[64]) b := 0;
-    (bit[64]) EA := 0;
-    if RA == 0 then b := 0 else b := GPR[RA];
-    EA := b + EXTS(D);
-    GPR[RT] := EXTS(MEMr(EA,2))
-  }
-
-union ast member (bit[5], bit[5], bit[5]) Lhax
-
-function clause decode (0b011111 :
-(bit[5]) RT :
-(bit[5]) RA :
-(bit[5]) RB :
-0b0101010111 :
-(bit[1]) _ as instr) =
-  Some(Lhax(RT,RA,RB))
-
-function clause execute (Lhax (RT, RA, RB)) =
-  {
-    (bit[64]) b := 0;
-    (bit[64]) EA := 0;
-    if RA == 0 then b := 0 else b := GPR[RA];
-    EA := b + GPR[RB];
-    GPR[RT] := EXTS(MEMr(EA,2))
-  }
-
-union ast member (bit[5], bit[5], bit[16]) Lhau
-
-function clause decode (0b101011 :
-(bit[5]) RT :
-(bit[5]) RA :
-(bit[16]) D as instr) =
-  Some(Lhau(RT,RA,D))
-
-function clause execute (Lhau (RT, RA, D)) =
-  {
-    (bit[64]) EA := 0;
-    EA := GPR[RA] + EXTS(D);
-    GPR[RA] := EA;
-    GPR[RT] := EXTS(MEMr(EA,2))
-  }
-
-union ast member (bit[5], bit[5], bit[5]) Lhaux
-
-function clause decode (0b011111 :
-(bit[5]) RT :
-(bit[5]) RA :
-(bit[5]) RB :
-0b0101110111 :
-(bit[1]) _ as instr) =
-  Some(Lhaux(RT,RA,RB))
-
-function clause execute (Lhaux (RT, RA, RB)) =
-  {
-    (bit[64]) EA := 0;
-    EA := GPR[RA] + GPR[RB];
-    GPR[RA] := EA;
-    GPR[RT] := EXTS(MEMr(EA,2))
-  }
-
-union ast member (bit[5], bit[5], bit[16]) Lwz
-
-function clause decode (0b100000 :
-(bit[5]) RT :
-(bit[5]) RA :
-(bit[16]) D as instr) =
-  Some(Lwz(RT,RA,D))
-
-function clause execute (Lwz (RT, RA, D)) =
-  {
-    (bit[64]) b := 0;
-    (bit[64]) EA := 0;
-    if RA == 0 then b := 0 else b := GPR[RA];
-    EA := b + EXTS(D);
-    GPR[RT] := 0b00000000000000000000000000000000 : MEMr(EA,4)
-  }
-
-union ast member (bit[5], bit[5], bit[5]) Lwzx
-
-function clause decode (0b011111 :
-(bit[5]) RT :
-(bit[5]) RA :
-(bit[5]) RB :
-0b0000010111 :
-(bit[1]) _ as instr) =
-  Some(Lwzx(RT,RA,RB))
-
-function clause execute (Lwzx (RT, RA, RB)) =
-  {
-    (bit[64]) b := 0;
-    (bit[64]) EA := 0;
-    if RA == 0 then b := 0 else b := GPR[RA];
-    EA := b + GPR[RB];
-    GPR[RT] := 0b00000000000000000000000000000000 : MEMr(EA,4)
-  }
-
-union ast member (bit[5], bit[5], bit[16]) Lwzu
-
-function clause decode (0b100001 :
-(bit[5]) RT :
-(bit[5]) RA :
-(bit[16]) D as instr) =
-  Some(Lwzu(RT,RA,D))
-
-function clause execute (Lwzu (RT, RA, D)) =
-  {
-    (bit[64]) EA := 0;
-    EA := GPR[RA] + EXTS(D);
-    GPR[RA] := EA;
-    GPR[RT] := 0b00000000000000000000000000000000 : MEMr(EA,4)
-  }
-
-union ast member (bit[5], bit[5], bit[5]) Lwzux
-
-function clause decode (0b011111 :
-(bit[5]) RT :
-(bit[5]) RA :
-(bit[5]) RB :
-0b0000110111 :
-(bit[1]) _ as instr) =
-  Some(Lwzux(RT,RA,RB))
-
-function clause execute (Lwzux (RT, RA, RB)) =
-  {
-    (bit[64]) EA := 0;
-    EA := GPR[RA] + GPR[RB];
-    GPR[RA] := EA;
-    GPR[RT] := 0b00000000000000000000000000000000 : MEMr(EA,4)
-  }
-
-union ast member (bit[5], bit[5], bit[14]) Lwa
-
-function clause decode (0b111010 :
-(bit[5]) RT :
-(bit[5]) RA :
-(bit[14]) DS :
-0b10 as instr) =
-  Some(Lwa(RT,RA,DS))
-
-function clause execute (Lwa (RT, RA, DS)) =
-  {
-    (bit[64]) b := 0;
-    (bit[64]) EA := 0;
-    if RA == 0 then b := 0 else b := GPR[RA];
-    EA := b + EXTS(DS : 0b00);
-    GPR[RT] := EXTS(MEMr(EA,4))
-  }
-
-union ast member (bit[5], bit[5], bit[5]) Lwax
-
-function clause decode (0b011111 :
-(bit[5]) RT :
-(bit[5]) RA :
-(bit[5]) RB :
-0b0101010101 :
-(bit[1]) _ as instr) =
-  Some(Lwax(RT,RA,RB))
-
-function clause execute (Lwax (RT, RA, RB)) =
-  {
-    (bit[64]) b := 0;
-    (bit[64]) EA := 0;
-    if RA == 0 then b := 0 else b := GPR[RA];
-    EA := b + GPR[RB];
-    GPR[RT] := EXTS(MEMr(EA,4))
-  }
-
-union ast member (bit[5], bit[5], bit[5]) Lwaux
-
-function clause decode (0b011111 :
-(bit[5]) RT :
-(bit[5]) RA :
-(bit[5]) RB :
-0b0101110101 :
-(bit[1]) _ as instr) =
-  Some(Lwaux(RT,RA,RB))
-
-function clause execute (Lwaux (RT, RA, RB)) =
-  {
-    (bit[64]) EA := 0;
-    EA := GPR[RA] + GPR[RB];
-    GPR[RA] := EA;
-    GPR[RT] := EXTS(MEMr(EA,4))
-  }
-
-union ast member (bit[5], bit[5], bit[14]) Ld
-
-function clause decode (0b111010 :
-(bit[5]) RT :
-(bit[5]) RA :
-(bit[14]) DS :
-0b00 as instr) =
-  Some(Ld(RT,RA,DS))
-
-function clause execute (Ld (RT, RA, DS)) =
-  {
-    (bit[64]) b := 0;
-    (bit[64]) EA := 0;
-    if RA == 0 then b := 0 else b := GPR[RA];
-    EA := b + EXTS(DS : 0b00);
-    GPR[RT] := MEMr(EA,8)
-  }
-
-union ast member (bit[5], bit[5], bit[5]) Ldx
-
-function clause decode (0b011111 :
-(bit[5]) RT :
-(bit[5]) RA :
-(bit[5]) RB :
-0b0000010101 :
-(bit[1]) _ as instr) =
-  Some(Ldx(RT,RA,RB))
-
-function clause execute (Ldx (RT, RA, RB)) =
-  {
-    (bit[64]) b := 0;
-    (bit[64]) EA := 0;
-    if RA == 0 then b := 0 else b := GPR[RA];
-    EA := b + GPR[RB];
-    GPR[RT] := MEMr(EA,8)
-  }
-
-union ast member (bit[5], bit[5], bit[14]) Ldu
-
-function clause decode (0b111010 :
-(bit[5]) RT :
-(bit[5]) RA :
-(bit[14]) DS :
-0b01 as instr) =
-  Some(Ldu(RT,RA,DS))
-
-function clause execute (Ldu (RT, RA, DS)) =
-  {
-    (bit[64]) EA := 0;
-    EA := GPR[RA] + EXTS(DS : 0b00);
-    GPR[RA] := EA;
-    GPR[RT] := MEMr(EA,8)
-  }
-
-union ast member (bit[5], bit[5], bit[5]) Ldux
-
-function clause decode (0b011111 :
-(bit[5]) RT :
-(bit[5]) RA :
-(bit[5]) RB :
-0b0000110101 :
-(bit[1]) _ as instr) =
-  Some(Ldux(RT,RA,RB))
-
-function clause execute (Ldux (RT, RA, RB)) =
-  {
-    (bit[64]) EA := 0;
-    EA := GPR[RA] + GPR[RB];
-    GPR[RA] := EA;
-    GPR[RT] := MEMr(EA,8)
-  }
-
-union ast member (bit[5], bit[5], bit[16]) Stb
-
-function clause decode (0b100110 :
-(bit[5]) RS :
-(bit[5]) RA :
-(bit[16]) D as instr) =
-  Some(Stb(RS,RA,D))
-
-function clause execute (Stb (RS, RA, D)) =
-  {
-    (bit[64]) b := 0;
-    (bit[64]) EA := 0;
-    if RA == 0 then b := 0 else b := GPR[RA];
-    EA := b + EXTS(D);
-    MEMw_EA(EA,1);
-    MEMw(EA,1) := (GPR[RS])[56 .. 63]
-  }
-
-union ast member (bit[5], bit[5], bit[5]) Stbx
-
-function clause decode (0b011111 :
-(bit[5]) RS :
-(bit[5]) RA :
-(bit[5]) RB :
-0b0011010111 :
-(bit[1]) _ as instr) =
-  Some(Stbx(RS,RA,RB))
-
-function clause execute (Stbx (RS, RA, RB)) =
-  {
-    (bit[64]) b := 0;
-    (bit[64]) EA := 0;
-    if RA == 0 then b := 0 else b := GPR[RA];
-    EA := b + GPR[RB];
-    MEMw_EA(EA,1);
-    MEMw(EA,1) := (GPR[RS])[56 .. 63]
-  }
-
-union ast member (bit[5], bit[5], bit[16]) Stbu
-
-function clause decode (0b100111 :
-(bit[5]) RS :
-(bit[5]) RA :
-(bit[16]) D as instr) =
-  Some(Stbu(RS,RA,D))
-
-function clause execute (Stbu (RS, RA, D)) =
-  {
-    (bit[64]) EA := 0;
-    EA := GPR[RA] + EXTS(D);
-    MEMw_EA(EA,1);
-    GPR[RA] := EA;
-    MEMw(EA,1) := (GPR[RS])[56 .. 63]
-  }
-
-union ast member (bit[5], bit[5], bit[5]) Stbux
-
-function clause decode (0b011111 :
-(bit[5]) RS :
-(bit[5]) RA :
-(bit[5]) RB :
-0b0011110111 :
-(bit[1]) _ as instr) =
-  Some(Stbux(RS,RA,RB))
-
-function clause execute (Stbux (RS, RA, RB)) =
-  {
-    (bit[64]) EA := 0;
-    EA := GPR[RA] + GPR[RB];
-    MEMw_EA(EA,1);
-    GPR[RA] := EA;
-    MEMw(EA,1) := (GPR[RS])[56 .. 63]
-  }
-
-union ast member (bit[5], bit[5], bit[16]) Sth
-
-function clause decode (0b101100 :
-(bit[5]) RS :
-(bit[5]) RA :
-(bit[16]) D as instr) =
-  Some(Sth(RS,RA,D))
-
-function clause execute (Sth (RS, RA, D)) =
-  {
-    (bit[64]) b := 0;
-    (bit[64]) EA := 0;
-    if RA == 0 then b := 0 else b := GPR[RA];
-    EA := b + EXTS(D);
-    MEMw_EA(EA,2);
-    MEMw(EA,2) := (GPR[RS])[48 .. 63]
-  }
-
-union ast member (bit[5], bit[5], bit[5]) Sthx
-
-function clause decode (0b011111 :
-(bit[5]) RS :
-(bit[5]) RA :
-(bit[5]) RB :
-0b0110010111 :
-(bit[1]) _ as instr) =
-  Some(Sthx(RS,RA,RB))
-
-function clause execute (Sthx (RS, RA, RB)) =
-  {
-    (bit[64]) b := 0;
-    (bit[64]) EA := 0;
-    if RA == 0 then b := 0 else b := GPR[RA];
-    EA := b + GPR[RB];
-    MEMw_EA(EA,2);
-    MEMw(EA,2) := (GPR[RS])[48 .. 63]
-  }
-
-union ast member (bit[5], bit[5], bit[16]) Sthu
-
-function clause decode (0b101101 :
-(bit[5]) RS :
-(bit[5]) RA :
-(bit[16]) D as instr) =
-  Some(Sthu(RS,RA,D))
-
-function clause execute (Sthu (RS, RA, D)) =
-  {
-    (bit[64]) EA := 0;
-    EA := GPR[RA] + EXTS(D);
-    MEMw_EA(EA,2);
-    GPR[RA] := EA;
-    MEMw(EA,2) := (GPR[RS])[48 .. 63]
-  }
-
-union ast member (bit[5], bit[5], bit[5]) Sthux
-
-function clause decode (0b011111 :
-(bit[5]) RS :
-(bit[5]) RA :
-(bit[5]) RB :
-0b0110110111 :
-(bit[1]) _ as instr) =
-  Some(Sthux(RS,RA,RB))
-
-function clause execute (Sthux (RS, RA, RB)) =
-  {
-    (bit[64]) EA := 0;
-    EA := GPR[RA] + GPR[RB];
-    MEMw_EA(EA,2);
-    GPR[RA] := EA;
-    MEMw(EA,2) := (GPR[RS])[48 .. 63]
-  }
-
-union ast member (bit[5], bit[5], bit[16]) Stw
-
-function clause decode (0b100100 :
-(bit[5]) RS :
-(bit[5]) RA :
-(bit[16]) D as instr) =
-  Some(Stw(RS,RA,D))
-
-function clause execute (Stw (RS, RA, D)) =
-  {
-    (bit[64]) b := 0;
-    (bit[64]) EA := 0;
-    if RA == 0 then b := 0 else b := GPR[RA];
-    EA := b + EXTS(D);
-    MEMw_EA(EA,4);
-    MEMw(EA,4) := (GPR[RS])[32 .. 63]
-  }
-
-union ast member (bit[5], bit[5], bit[5]) Stwx
-
-function clause decode (0b011111 :
-(bit[5]) RS :
-(bit[5]) RA :
-(bit[5]) RB :
-0b0010010111 :
-(bit[1]) _ as instr) =
-  Some(Stwx(RS,RA,RB))
-
-function clause execute (Stwx (RS, RA, RB)) =
-  {
-    (bit[64]) b := 0;
-    (bit[64]) EA := 0;
-    if RA == 0 then b := 0 else b := GPR[RA];
-    EA := b + GPR[RB];
-    MEMw_EA(EA,4);
-    MEMw(EA,4) := (GPR[RS])[32 .. 63]
-  }
-
-union ast member (bit[5], bit[5], bit[16]) Stwu
-
-function clause decode (0b100101 :
-(bit[5]) RS :
-(bit[5]) RA :
-(bit[16]) D as instr) =
-  Some(Stwu(RS,RA,D))
-
-function clause execute (Stwu (RS, RA, D)) =
-  {
-    (bit[64]) EA := 0;
-    EA := GPR[RA] + EXTS(D);
-    MEMw_EA(EA,4);
-    GPR[RA] := EA;
-    MEMw(EA,4) := (GPR[RS])[32 .. 63]
-  }
-
-union ast member (bit[5], bit[5], bit[5]) Stwux
-
-function clause decode (0b011111 :
-(bit[5]) RS :
-(bit[5]) RA :
-(bit[5]) RB :
-0b0010110111 :
-(bit[1]) _ as instr) =
-  Some(Stwux(RS,RA,RB))
-
-function clause execute (Stwux (RS, RA, RB)) =
-  {
-    (bit[64]) EA := 0;
-    EA := GPR[RA] + GPR[RB];
-    MEMw_EA(EA,4);
-    GPR[RA] := EA;
-    MEMw(EA,4) := (GPR[RS])[32 .. 63]
-  }
-
-union ast member (bit[5], bit[5], bit[14]) Std
-
-function clause decode (0b111110 :
-(bit[5]) RS :
-(bit[5]) RA :
-(bit[14]) DS :
-0b00 as instr) =
-  Some(Std(RS,RA,DS))
-
-function clause execute (Std (RS, RA, DS)) =
-  {
-    (bit[64]) b := 0;
-    (bit[64]) EA := 0;
-    if RA == 0 then b := 0 else b := GPR[RA];
-    EA := b + EXTS(DS : 0b00);
-    MEMw_EA(EA,8);
-    MEMw(EA,8) := GPR[RS]
-  }
-
-union ast member (bit[5], bit[5], bit[5]) Stdx
-
-function clause decode (0b011111 :
-(bit[5]) RS :
-(bit[5]) RA :
-(bit[5]) RB :
-0b0010010101 :
-(bit[1]) _ as instr) =
-  Some(Stdx(RS,RA,RB))
-
-function clause execute (Stdx (RS, RA, RB)) =
-  {
-    (bit[64]) b := 0;
-    (bit[64]) EA := 0;
-    if RA == 0 then b := 0 else b := GPR[RA];
-    EA := b + GPR[RB];
-    MEMw_EA(EA,8);
-    MEMw(EA,8) := GPR[RS]
-  }
-
-union ast member (bit[5], bit[5], bit[14]) Stdu
-
-function clause decode (0b111110 :
-(bit[5]) RS :
-(bit[5]) RA :
-(bit[14]) DS :
-0b01 as instr) =
-  Some(Stdu(RS,RA,DS))
-
-function clause execute (Stdu (RS, RA, DS)) =
-  {
-    (bit[64]) EA := 0;
-    EA := GPR[RA] + EXTS(DS : 0b00);
-    MEMw_EA(EA,8);
-    GPR[RA] := EA;
-    MEMw(EA,8) := GPR[RS]
-  }
-
-union ast member (bit[5], bit[5], bit[5]) Stdux
-
-function clause decode (0b011111 :
-(bit[5]) RS :
-(bit[5]) RA :
-(bit[5]) RB :
-0b0010110101 :
-(bit[1]) _ as instr) =
-  Some(Stdux(RS,RA,RB))
-
-function clause execute (Stdux (RS, RA, RB)) =
-  {
-    (bit[64]) EA := 0;
-    EA := GPR[RA] + GPR[RB];
-    MEMw_EA(EA,8);
-    GPR[RA] := EA;
-    MEMw(EA,8) := GPR[RS]
-  }
-
-union ast member (bit[5], bit[5], bit[12], bit[4]) Lq
-
-function clause decode (0b111000 :
-(bit[5]) RTp :
-(bit[5]) RA :
-(bit[12]) DQ :
-(bit[4]) PT as instr) =
-  Some(Lq(RTp,RA,DQ,PT))
-
-function clause execute (Lq (RTp, RA, DQ, PT)) =
-  {
-    (bit[64]) EA := 0;
-    (bit[64]) b := 0;
-    if RA == 0 then b := 0 else b := GPR[RA];
-    EA := b + EXTS(DQ : 0b0000);
-    (bit[128]) mem := MEMr(EA,16);
-    if bigendianmode
-    then {
-      GPR[RTp] := mem[0 .. 63];
-      GPR[RTp + 1] := mem[64 .. 127]
-    }
-    else {
-      (bit[128]) bytereverse := byte_reverse(mem);
-      GPR[RTp] := bytereverse[0 .. 63];
-      GPR[RTp + 1] := bytereverse[64 .. 127]
-    }
-  }
-
-union ast member (bit[5], bit[5], bit[14]) Stq
-
-function clause decode (0b111110 :
-(bit[5]) RSp :
-(bit[5]) RA :
-(bit[14]) DS :
-0b10 as instr) =
-  Some(Stq(RSp,RA,DS))
-
-function clause execute (Stq (RSp, RA, DS)) =
-  {
-    (bit[64]) b := 0;
-    (bit[64]) EA := 0;
-    if RA == 0 then b := 0 else b := GPR[RA];
-    EA := b + EXTS(DS : 0b00);
-    MEMw_EA(EA,16);
-    (bit[128]) mem := 0;
-    mem[0..63] := GPR[RSp];
-    mem[64..127] := GPR[RSp + 1];
-    if ~(bigendianmode) then mem := byte_reverse(mem) else ();
-    MEMw(EA,16) := mem
-  }
-
-union ast member (bit[5], bit[5], bit[5]) Lhbrx
-
-function clause decode (0b011111 :
-(bit[5]) RT :
-(bit[5]) RA :
-(bit[5]) RB :
-0b1100010110 :
-(bit[1]) _ as instr) =
-  Some(Lhbrx(RT,RA,RB))
-
-function clause execute (Lhbrx (RT, RA, RB)) =
-  {
-    (bit[64]) b := 0;
-    (bit[64]) EA := 0;
-    if RA == 0 then b := 0 else b := GPR[RA];
-    EA := b + GPR[RB];
-    load_data := MEMr(EA,2);
-    GPR[RT] :=
-      0b000000000000000000000000000000000000000000000000 : load_data[8 .. 15] : load_data[0 .. 7]
-  }
-
-union ast member (bit[5], bit[5], bit[5]) Sthbrx
-
-function clause decode (0b011111 :
-(bit[5]) RS :
-(bit[5]) RA :
-(bit[5]) RB :
-0b1110010110 :
-(bit[1]) _ as instr) =
-  Some(Sthbrx(RS,RA,RB))
-
-function clause execute (Sthbrx (RS, RA, RB)) =
-  {
-    (bit[64]) b := 0;
-    (bit[64]) EA := 0;
-    if RA == 0 then b := 0 else b := GPR[RA];
-    EA := b + GPR[RB];
-    MEMw_EA(EA,2);
-    MEMw(EA,2) := (GPR[RS])[56 .. 63] : (GPR[RS])[48 .. 55]
-  }
-
-union ast member (bit[5], bit[5], bit[5]) Lwbrx
-
-function clause decode (0b011111 :
-(bit[5]) RT :
-(bit[5]) RA :
-(bit[5]) RB :
-0b1000010110 :
-(bit[1]) _ as instr) =
-  Some(Lwbrx(RT,RA,RB))
-
-function clause execute (Lwbrx (RT, RA, RB)) =
-  {
-    (bit[64]) b := 0;
-    (bit[64]) EA := 0;
-    if RA == 0 then b := 0 else b := GPR[RA];
-    EA := b + GPR[RB];
-    load_data := MEMr(EA,4);
-    GPR[RT] :=
-      0b00000000000000000000000000000000 :
-        load_data[24 .. 31] : load_data[16 .. 23] : load_data[8 .. 15] : load_data[0 .. 7]
-  }
-
-union ast member (bit[5], bit[5], bit[5]) Stwbrx
-
-function clause decode (0b011111 :
-(bit[5]) RS :
-(bit[5]) RA :
-(bit[5]) RB :
-0b1010010110 :
-(bit[1]) _ as instr) =
-  Some(Stwbrx(RS,RA,RB))
-
-function clause execute (Stwbrx (RS, RA, RB)) =
-  {
-    (bit[64]) b := 0;
-    (bit[64]) EA := 0;
-    if RA == 0 then b := 0 else b := GPR[RA];
-    EA := b + GPR[RB];
-    MEMw_EA(EA,4);
-    MEMw(EA,4) :=
-      (GPR[RS])[56 .. 63] : (GPR[RS])[48 .. 55] : (GPR[RS])[40 .. 47] : (GPR[RS])[32 .. 39]
-  }
-
-union ast member (bit[5], bit[5], bit[5]) Ldbrx
-
-function clause decode (0b011111 :
-(bit[5]) RT :
-(bit[5]) RA :
-(bit[5]) RB :
-0b1000010100 :
-(bit[1]) _ as instr) =
-  Some(Ldbrx(RT,RA,RB))
-
-function clause execute (Ldbrx (RT, RA, RB)) =
-  {
-    (bit[64]) b := 0;
-    (bit[64]) EA := 0;
-    if RA == 0 then b := 0 else b := GPR[RA];
-    EA := b + GPR[RB];
-    load_data := MEMr(EA,8);
-    GPR[RT] :=
-      load_data[56 .. 63] :
-        load_data[48 .. 55] :
-          load_data[40 .. 47] :
-            load_data[32 .. 39] :
-              load_data[24 .. 31] : load_data[16 .. 23] : load_data[8 .. 15] : load_data[0 .. 7]
-  }
-
-union ast member (bit[5], bit[5], bit[5]) Stdbrx
-
-function clause decode (0b011111 :
-(bit[5]) RS :
-(bit[5]) RA :
-(bit[5]) RB :
-0b1010010100 :
-(bit[1]) _ as instr) =
-  Some(Stdbrx(RS,RA,RB))
-
-function clause execute (Stdbrx (RS, RA, RB)) =
-  {
-    (bit[64]) b := 0;
-    (bit[64]) EA := 0;
-    if RA == 0 then b := 0 else b := GPR[RA];
-    EA := b + GPR[RB];
-    MEMw_EA(EA,8);
-    MEMw(EA,8) :=
-      (GPR[RS])[56 .. 63] :
-        (GPR[RS])[48 .. 55] :
-          (GPR[RS])[40 .. 47] :
-            (GPR[RS])[32 .. 39] :
-              (GPR[RS])[24 .. 31] : (GPR[RS])[16 .. 23] : (GPR[RS])[8 .. 15] : (GPR[RS])[0 .. 7]
-  }
-
-union ast member (bit[5], bit[5], bit[16]) Lmw
-
-function clause decode (0b101110 :
-(bit[5]) RT :
-(bit[5]) RA :
-(bit[16]) D as instr) =
-  Some(Lmw(RT,RA,D))
-
-function clause execute (Lmw (RT, RA, D)) =
-  {
-    (bit[64]) b := 0;
-    (bit[64]) EA := 0;
-    if RA == 0 then b := 0 else b := GPR[RA];
-    EA := b + EXTS(D);
-    size := ([|32|]) (32 - RT) * 4;
-    buffer := MEMr(EA,size);
-    i := 0;
-    foreach (r from RT to 31 by 1 in inc)
-    {
-      GPR[r] := 0b00000000000000000000000000000000 : buffer[i .. i + 31];
-      i := i + 32
-    }
-  }
-
-union ast member (bit[5], bit[5], bit[16]) Stmw
-
-function clause decode (0b101111 :
-(bit[5]) RS :
-(bit[5]) RA :
-(bit[16]) D as instr) =
-  Some(Stmw(RS,RA,D))
-
-function clause execute (Stmw (RS, RA, D)) =
-  {
-    (bit[64]) b := 0;
-    (bit[64]) EA := 0;
-    if RA == 0 then b := 0 else b := GPR[RA];
-    EA := b + EXTS(D);
-    size := ([|32|]) (32 - RS) * 4;
-    MEMw_EA(EA,size);
-    (bit[994]) buffer := [0 = 0,993 = 0; default=0];
-    i := 0;
-    foreach (r from RS to 31 by 1 in inc)
-    {
-      buffer[i..i + 31] := (GPR[r])[32 .. 63];
-      i := i + 32
-    };
-    MEMw(EA,size) := buffer[0 .. size * 8]
-  }
-
-union ast member (bit[5], bit[5], bit[5]) Lswi
-
-function clause decode (0b011111 :
-(bit[5]) RT :
-(bit[5]) RA :
-(bit[5]) NB :
-0b1001010101 :
-(bit[1]) _ as instr) =
-  Some(Lswi(RT,RA,NB))
-
-function clause execute (Lswi (RT, RA, NB)) =
-  {
-    (bit[64]) EA := 0;
-    if RA == 0 then EA := 0 else EA := GPR[RA];
-    ([|31|]) r := 0;
-    r := RT - 1;
-    ([|32|]) size := if NB == 0 then 32 else NB;
-    (bit[256]) membuffer := MEMr(EA,size);
-    j := 0;
-    i := 32;
-    foreach (n from (if NB == 0 then 32 else NB) to 1 by 1 in dec)
-    {
-      if i == 32
-      then {
-        r := ([|31|]) (r + 1) mod 32;
-        GPR[r] := 0
-      }
-      else ();
-      (GPR[r])[i..i + 7] := membuffer[j .. j + 7];
-      j := j + 8;
-      i := i + 8;
-      if i == 64 then i := 32 else ();
-      EA := EA + 1
-    }
-  }
-
-union ast member (bit[5], bit[5], bit[5]) Lswx
-
-function clause decode (0b011111 :
-(bit[5]) RT :
-(bit[5]) RA :
-(bit[5]) RB :
-0b1000010101 :
-(bit[1]) _ as instr) =
-  Some(Lswx(RT,RA,RB))
-
-function clause execute (Lswx (RT, RA, RB)) =
-  {
-    (bit[64]) b := 0;
-    (bit[64]) EA := 0;
-    if RA == 0 then b := 0 else b := GPR[RA];
-    ([|31|]) r := 0;
-    EA := b + GPR[RB];
-    r := RT - 1;
-    i := 32;
-    ([|128|]) n_top := XER[57 .. 63];
-    recalculate_dependency(());
-    if n_top == 0
-    then GPR[RT] := undefined
-    else {
-      (bit[512]) membuffer := MEMr(EA,n_top);
-      j := 0;
-      n_r := n_top quot 4;
-      n_mod := n_top mod 4;
-      n_r := if n_mod == 0 then n_r else n_r + 1;
-      foreach (n from n_r to 1 by 1 in dec)
-      {
-        r := ([|32|]) (r + 1) mod 32;
-        (bit[64]) temp := 0;
-        if n == 1
-        then switch n_mod {
-          case 0 -> temp[32..63] := membuffer[j .. j + 31]
-          case 1 -> temp[32..39] := membuffer[j .. j + 7]
-          case 2 -> temp[32..47] := membuffer[j .. j + 15]
-          case 3 -> temp[32..55] := membuffer[j .. j + 23]
-        }
-        else temp[32..63] := membuffer[j .. j + 31];
-        j := j + 32;
-        GPR[r] := temp
-      }
-    }
-  }
-
-union ast member (bit[5], bit[5], bit[5]) Stswi
-
-function clause decode (0b011111 :
-(bit[5]) RS :
-(bit[5]) RA :
-(bit[5]) NB :
-0b1011010101 :
-(bit[1]) _ as instr) =
-  Some(Stswi(RS,RA,NB))
-
-function clause execute (Stswi (RS, RA, NB)) =
-  {
-    (bit[64]) EA := 0;
-    if RA == 0 then EA := 0 else EA := GPR[RA];
-    ([|31|]) r := 0;
-    r := RS - 1;
-    ([|32|]) size := if NB == 0 then 32 else NB;
-    MEMw_EA(EA,size);
-    (bit[256]) membuffer := [0 = 0,255 = 0; default=0];
-    j := 0;
-    i := 32;
-    foreach (n from (if NB == 0 then 32 else NB) to 1 by 1 in dec)
-    {
-      if i == 32 then r := ([|32|]) (r + 1) mod 32 else ();
-      membuffer[j..j + 7] := (GPR[r])[i .. i + 7];
-      j := j + 8;
-      i := i + 8;
-      if i == 64 then i := 32 else ()
-    };
-    MEMw(EA,size) := membuffer[0 .. size * 8]
-  }
-
-union ast member (bit[5], bit[5], bit[5]) Stswx
-
-function clause decode (0b011111 :
-(bit[5]) RS :
-(bit[5]) RA :
-(bit[5]) RB :
-0b1010010101 :
-(bit[1]) _ as instr) =
-  Some(Stswx(RS,RA,RB))
-
-function clause execute (Stswx (RS, RA, RB)) =
-  {
-    (bit[64]) b := 0;
-    (bit[64]) EA := 0;
-    if RA == 0 then b := 0 else b := GPR[RA];
-    ([|31|]) r := 0;
-    EA := b + GPR[RB];
-    r := RS - 1;
-    i := 32;
-    ([|128|]) n_top := XER[57 .. 63];
-    recalculate_dependency(());
-    MEMw_EA(EA,n_top);
-    (bit[512]) membuffer := [0 = 0,511 = 0; default=0];
-    j := 0;
-    foreach (n from n_top to 1 by 1 in dec)
-    {
-      if i == 32 then r := ([|32|]) (r + 1) mod 32 else ();
-      membuffer[j..j + 7] := (GPR[r])[i .. i + 7];
-      i := i + 8;
-      j := j + 8;
-      if i == 64 then i := 32 else ()
-    };
-    if ~(n_top == 0) then MEMw(EA,n_top) := membuffer[0 .. n_top * 8] else ()
-  }
-
-union ast member (bit[5], bit[5], bit[16]) Addi
-
-function clause decode (0b001110 :
-(bit[5]) RT :
-(bit[5]) RA :
-(bit[16]) SI as instr) =
-  Some(Addi(RT,RA,SI))
-
-function clause execute (Addi (RT, RA, SI)) =
-  if RA == 0 then GPR[RT] := EXTS(SI) else GPR[RT] := GPR[RA] + EXTS(SI)
-
-union ast member (bit[5], bit[5], bit[16]) Addis
-
-function clause decode (0b001111 :
-(bit[5]) RT :
-(bit[5]) RA :
-(bit[16]) SI as instr) =
-  Some(Addis(RT,RA,SI))
-
-function clause execute (Addis (RT, RA, SI)) =
-  if RA == 0
-  then GPR[RT] := EXTS(SI : 0b0000000000000000)
-  else GPR[RT] := GPR[RA] + EXTS(SI : 0b0000000000000000)
-
-union ast member (bit[5], bit[5], bit[5], bit, bit) Add
-
-function clause decode (0b011111 :
-(bit[5]) RT :
-(bit[5]) RA :
-(bit[5]) RB :
-[OE] :
-0b100001010 :
-[Rc] as instr) =
-  Some(Add(RT,RA,RB,OE,Rc))
-
-function clause execute (Add (RT, RA, RB, OE, Rc)) =
-  let (temp, overflow, _) = (GPR[RA] +_s GPR[RB]) in
-    {
-      GPR[RT] := temp;
-      if Rc
-      then {
-        (bit) xer_so := XER.SO;
-        if OE & overflow then xer_so := overflow else ();
-        set_overflow_cr0(temp,xer_so)
-      }
-      else ();
-      if OE then set_SO_OV(overflow) else ()
-    }
-
-union ast member (bit[5], bit[5], bit[5], bit, bit) Subf
-
-function clause decode (0b011111 :
-(bit[5]) RT :
-(bit[5]) RA :
-(bit[5]) RB :
-[OE] :
-0b000101000 :
-[Rc] as instr) =
-  Some(Subf(RT,RA,RB,OE,Rc))
-
-function clause execute (Subf (RT, RA, RB, OE, Rc)) =
-  let (t1, o1, _) = (~(GPR[RA]) +_s GPR[RB]) in
-    let (t2, o2, _) = (t1 +_s (bit) 1) in
-      {
-        (bit[64]) temp := t2;
-        overflow := (o1 | o2);
-        GPR[RT] := temp;
-        if Rc
-        then {
-          (bit) xer_so := XER.SO;
-          if OE & overflow then xer_so := overflow else ();
-          set_overflow_cr0(temp,xer_so)
-        }
-        else ();
-        if OE then set_SO_OV(overflow) else ()
-      }
-
-union ast member (bit[5], bit[5], bit[16]) Addic
-
-function clause decode (0b001100 :
-(bit[5]) RT :
-(bit[5]) RA :
-(bit[16]) SI as instr) =
-  Some(Addic(RT,RA,SI))
-
-function clause execute (Addic (RT, RA, SI)) =
-  let (temp, _, carry) = (GPR[RA] +_s EXTS(SI)) in
-    {
-      GPR[RT] := temp;
-      CA := carry
-    }
-
-union ast member (bit[5], bit[5], bit[16]) AddicDot
-
-function clause decode (0b001101 :
-(bit[5]) RT :
-(bit[5]) RA :
-(bit[16]) SI as instr) =
-  Some(AddicDot(RT,RA,SI))
-
-function clause execute (AddicDot (RT, RA, SI)) =
-  let (temp, overflow, carry) = (GPR[RA] +_s EXTS(SI)) in
-    {
-      GPR[RT] := temp;
-      CA := carry;
-      set_overflow_cr0(temp,overflow | XER.SO)
-    }
-
-union ast member (bit[5], bit[5], bit[16]) Subfic
-
-function clause decode (0b001000 :
-(bit[5]) RT :
-(bit[5]) RA :
-(bit[16]) SI as instr) =
-  Some(Subfic(RT,RA,SI))
-
-function clause execute (Subfic (RT, RA, SI)) =
-  let (t1, o1, c1) = (~(GPR[RA]) +_s EXTS(SI)) in
-    let (t2, o2, c2) = (t1 +_s (bit) 1) in
-      {
-        (bit[64]) temp := t2;
-        GPR[RT] := temp;
-        CA := (c1 | c2)
-      }
-
-union ast member (bit[5], bit[5], bit[5], bit, bit) Addc
-
-function clause decode (0b011111 :
-(bit[5]) RT :
-(bit[5]) RA :
-(bit[5]) RB :
-[OE] :
-0b000001010 :
-[Rc] as instr) =
-  Some(Addc(RT,RA,RB,OE,Rc))
-
-function clause execute (Addc (RT, RA, RB, OE, Rc)) =
-  let (temp, overflow, carry) = (GPR[RA] +_s GPR[RB]) in
-    {
-      GPR[RT] := temp;
-      if Rc
-      then {
-        (bit) xer_so := XER.SO;
-        if OE & overflow then xer_so := overflow else ();
-        set_overflow_cr0(temp,xer_so)
-      }
-      else ();
-      CA := carry;
-      if OE then set_SO_OV(overflow) else ()
-    }
-
-union ast member (bit[5], bit[5], bit[5], bit, bit) Subfc
-
-function clause decode (0b011111 :
-(bit[5]) RT :
-(bit[5]) RA :
-(bit[5]) RB :
-[OE] :
-0b000001000 :
-[Rc] as instr) =
-  Some(Subfc(RT,RA,RB,OE,Rc))
-
-function clause execute (Subfc (RT, RA, RB, OE, Rc)) =
-  let (t1, o1, c1) = (~(GPR[RA]) +_s GPR[RB]) in
-    let (t2, o2, c2) = (t1 +_s (bit) 1) in
-      {
-        (bit[64]) temp := t2;
-        overflow := (o1 | o2);
-        carry := (c1 | c2);
-        GPR[RT] := temp;
-        if Rc
-        then {
-          (bit) xer_so := XER.SO;
-          if OE & overflow then xer_so := overflow else ();
-          set_overflow_cr0(temp,xer_so)
-        }
-        else ();
-        CA := carry;
-        if OE then set_SO_OV(overflow) else ()
-      }
-
-union ast member (bit[5], bit[5], bit[5], bit, bit) Adde
-
-function clause decode (0b011111 :
-(bit[5]) RT :
-(bit[5]) RA :
-(bit[5]) RB :
-[OE] :
-0b010001010 :
-[Rc] as instr) =
-  Some(Adde(RT,RA,RB,OE,Rc))
-
-function clause execute (Adde (RT, RA, RB, OE, Rc)) =
-  let (t1, o1, c1) = (GPR[RA] +_s GPR[RB]) in
-    let (t2, o2, c2) = (t1 +_s (bit) CA) in
-      {
-        (bit[64]) temp := t2;
-        overflow := (o1 | o2);
-        carry := (c1 | c2);
-        GPR[RT] := temp;
-        if Rc
-        then {
-          (bit) xer_so := XER.SO;
-          if OE & overflow then xer_so := overflow else ();
-          set_overflow_cr0(temp,xer_so)
-        }
-        else ();
-        CA := carry;
-        if OE then set_SO_OV(overflow) else ()
-      }
-
-union ast member (bit[5], bit[5], bit[5], bit, bit) Subfe
-
-function clause decode (0b011111 :
-(bit[5]) RT :
-(bit[5]) RA :
-(bit[5]) RB :
-[OE] :
-0b010001000 :
-[Rc] as instr) =
-  Some(Subfe(RT,RA,RB,OE,Rc))
-
-function clause execute (Subfe (RT, RA, RB, OE, Rc)) =
-  let (t1, o1, c1) = (~(GPR[RA]) +_s GPR[RB]) in
-    let (t2, o2, c2) = (t1 +_s (bit) CA) in
-      {
-        (bit[64]) temp := t2;
-        overflow := (o1 | o2);
-        carry := (c1 | c2);
-        GPR[RT] := temp;
-        if Rc
-        then {
-          (bit) xer_so := XER.SO;
-          if OE & overflow then xer_so := overflow else ();
-          set_overflow_cr0(temp,xer_so)
-        }
-        else ();
-        CA := carry;
-        if OE then set_SO_OV(overflow) else ()
-      }
-
-union ast member (bit[5], bit[5], bit, bit) Addme
-
-function clause decode (0b011111 :
-(bit[5]) RT :
-(bit[5]) RA :
-(bit[5]) _ :
-[OE] :
-0b011101010 :
-[Rc] as instr) =
-  Some(Addme(RT,RA,OE,Rc))
-
-function clause execute (Addme (RT, RA, OE, Rc)) =
-  let (t1, o1, c1) = (GPR[RA] +_s CA) in
-    let (t2, o2, c2) = (t1 +_s 0b1111111111111111111111111111111111111111111111111111111111111111) in
-      {
-        (bit[64]) temp := t2;
-        overflow := (o1 | o2);
-        carry := (c1 | c2);
-        GPR[RT] := temp;
-        if Rc
-        then {
-          (bit) xer_so := XER.SO;
-          if OE & overflow then xer_so := overflow else ();
-          set_overflow_cr0(temp,xer_so)
-        }
-        else ();
-        CA := carry;
-        if OE then set_SO_OV(overflow) else ()
-      }
-
-union ast member (bit[5], bit[5], bit, bit) Subfme
-
-function clause decode (0b011111 :
-(bit[5]) RT :
-(bit[5]) RA :
-(bit[5]) _ :
-[OE] :
-0b011101000 :
-[Rc] as instr) =
-  Some(Subfme(RT,RA,OE,Rc))
-
-function clause execute (Subfme (RT, RA, OE, Rc)) =
-  let (t1, o1, c1) = (~(GPR[RA]) +_s CA) in
-    let (t2, o2, c2) = (t1 +_s 0b1111111111111111111111111111111111111111111111111111111111111111) in
-      {
-        (bit[64]) temp := t2;
-        overflow := (o1 | o2);
-        carry := (c1 | c2);
-        GPR[RT] := temp;
-        if Rc
-        then {
-          (bit) xer_so := XER.SO;
-          if OE & overflow then xer_so := overflow else ();
-          set_overflow_cr0(temp,xer_so)
-        }
-        else ();
-        CA := carry;
-        if OE then set_SO_OV(overflow) else ()
-      }
-
-union ast member (bit[5], bit[5], bit, bit) Addze
-
-function clause decode (0b011111 :
-(bit[5]) RT :
-(bit[5]) RA :
-(bit[5]) _ :
-[OE] :
-0b011001010 :
-[Rc] as instr) =
-  Some(Addze(RT,RA,OE,Rc))
-
-function clause execute (Addze (RT, RA, OE, Rc)) =
-  let (temp, overflow, carry) = (GPR[RA] +_s CA) in
-    {
-      GPR[RT] := temp;
-      if Rc
-      then {
-        (bit) xer_so := XER.SO;
-        if OE & overflow then xer_so := overflow else ();
-        set_overflow_cr0(temp,xer_so)
-      }
-      else ();
-      CA := carry;
-      if OE then set_SO_OV(overflow) else ()
-    }
-
-union ast member (bit[5], bit[5], bit, bit) Subfze
-
-function clause decode (0b011111 :
-(bit[5]) RT :
-(bit[5]) RA :
-(bit[5]) _ :
-[OE] :
-0b011001000 :
-[Rc] as instr) =
-  Some(Subfze(RT,RA,OE,Rc))
-
-function clause execute (Subfze (RT, RA, OE, Rc)) =
-  let (temp, overflow, carry) = (~(GPR[RA]) +_s CA) in
-    {
-      GPR[RT] := temp;
-      if Rc
-      then {
-        (bit) xer_so := XER.SO;
-        if OE & overflow then xer_so := overflow else ();
-        set_overflow_cr0(temp,xer_so)
-      }
-      else ();
-      CA := carry;
-      if OE then set_SO_OV(overflow) else ()
-    }
-
-union ast member (bit[5], bit[5], bit, bit) Neg
-
-function clause decode (0b011111 :
-(bit[5]) RT :
-(bit[5]) RA :
-(bit[5]) _ :
-[OE] :
-0b001101000 :
-[Rc] as instr) =
-  Some(Neg(RT,RA,OE,Rc))
-
-function clause execute (Neg (RT, RA, OE, Rc)) =
-  let (temp, overflow, _) = (~(GPR[RA]) +_s (bit) 1) in
-    {
-      GPR[RT] := temp;
-      if Rc then set_overflow_cr0(temp,XER.SO) else ();
-      if OE then set_SO_OV(overflow) else ()
-    }
-
-union ast member (bit[5], bit[5], bit[16]) Mulli
-
-function clause decode (0b000111 :
-(bit[5]) RT :
-(bit[5]) RA :
-(bit[16]) SI as instr) =
-  Some(Mulli(RT,RA,SI))
-
-function clause execute (Mulli (RT, RA, SI)) =
-  {
-    (bit[128]) prod := GPR[RA] *_s EXTS(SI);
-    GPR[RT] := prod[64 .. 127]
-  }
-
-union ast member (bit[5], bit[5], bit[5], bit, bit) Mullw
-
-function clause decode (0b011111 :
-(bit[5]) RT :
-(bit[5]) RA :
-(bit[5]) RB :
-[OE] :
-0b011101011 :
-[Rc] as instr) =
-  Some(Mullw(RT,RA,RB,OE,Rc))
-
-function clause execute (Mullw (RT, RA, RB, OE, Rc)) =
-  let (prod, overflow, _) = ((GPR[RA])[32 .. 63] *_s (GPR[RB])[32 .. 63]) in
-    {
-      GPR[RT] := prod;
-      if Rc
-      then {
-        (bit) xer_so := XER.SO;
-        if OE & overflow then xer_so := overflow else ();
-        set_overflow_cr0(prod,xer_so)
-      }
-      else ();
-      if OE then set_SO_OV(overflow) else ()
-    }
-
-union ast member (bit[5], bit[5], bit[5], bit) Mulhw
-
-function clause decode (0b011111 :
-(bit[5]) RT :
-(bit[5]) RA :
-(bit[5]) RB :
-(bit[1]) _ :
-0b001001011 :
-[Rc] as instr) =
-  Some(Mulhw(RT,RA,RB,Rc))
-
-function clause execute (Mulhw (RT, RA, RB, Rc)) =
-  {
-    (bit[64]) prod := 0;
-    (bit) overflow := 0;
-    let (p, o, _) = ((GPR[RA])[32 .. 63] *_s (GPR[RB])[32 .. 63]) in
-      {
-        prod := p;
-        overflow := o
-      };
-    (GPR[RT])[32..63] := prod[0 .. 31];
-    (GPR[RT])[0..31] := undefined;
-    if Rc
-    then {
-      (bit) xer_so := XER.SO;
-      if mode64bit
-      then CR.CR0 := [undefined,undefined,undefined,xer_so]
-      else set_overflow_cr0(prod,xer_so)
-    }
-    else ()
-  }
-
-union ast member (bit[5], bit[5], bit[5], bit) Mulhwu
-
-function clause decode (0b011111 :
-(bit[5]) RT :
-(bit[5]) RA :
-(bit[5]) RB :
-(bit[1]) _ :
-0b000001011 :
-[Rc] as instr) =
-  Some(Mulhwu(RT,RA,RB,Rc))
-
-function clause execute (Mulhwu (RT, RA, RB, Rc)) =
-  {
-    (bit[64]) prod := (GPR[RA])[32 .. 63] * (GPR[RB])[32 .. 63];
-    (GPR[RT])[32..63] := prod[0 .. 31];
-    (GPR[RT])[0..31] := undefined;
-    if Rc
-    then {
-      (bit) xer_so := XER.SO;
-      if mode64bit
-      then CR.CR0 := [undefined,undefined,undefined,xer_so]
-      else set_overflow_cr0(prod,xer_so)
-    }
-    else ()
-  }
-
-union ast member (bit[5], bit[5], bit[5], bit, bit) Divw
-
-function clause decode (0b011111 :
-(bit[5]) RT :
-(bit[5]) RA :
-(bit[5]) RB :
-[OE] :
-0b111101011 :
-[Rc] as instr) =
-  Some(Divw(RT,RA,RB,OE,Rc))
-
-function clause execute (Divw (RT, RA, RB, OE, Rc)) =
-  {
-    (bit[32]) dividend := (GPR[RA])[32 .. 63];
-    (bit[32]) divisor := (GPR[RB])[32 .. 63];
-    (bit[64]) divided := 0b0000000000000000000000000000000000000000000000000000000000000000;
-    (bit) overflow := 0;
-    let (d, o, _) = (dividend quot_s divisor) in
-      {
-        divided[32..63] := d;
-        overflow := o
-      };
-    (GPR[RT])[32..63] := divided[32 .. 63];
-    (GPR[RT])[0..31] := undefined;
-    if Rc
-    then {
-      (bit) xer_so := XER.SO;
-      if OE & overflow then xer_so := overflow else ();
-      if mode64bit | overflow
-      then CR.CR0 := [undefined,undefined,undefined,xer_so]
-      else set_overflow_cr0(divided,xer_so)
-    }
-    else ();
-    if OE then set_SO_OV(overflow) else ()
-  }
-
-union ast member (bit[5], bit[5], bit[5], bit, bit) Divwu
-
-function clause decode (0b011111 :
-(bit[5]) RT :
-(bit[5]) RA :
-(bit[5]) RB :
-[OE] :
-0b111001011 :
-[Rc] as instr) =
-  Some(Divwu(RT,RA,RB,OE,Rc))
-
-function clause execute (Divwu (RT, RA, RB, OE, Rc)) =
-  {
-    (bit[32]) dividend := (GPR[RA])[32 .. 63];
-    (bit[32]) divisor := (GPR[RB])[32 .. 63];
-    (bit[64]) divided := 0b0000000000000000000000000000000000000000000000000000000000000000;
-    (bit) overflow := 0;
-    let (d, o, _) = (dividend quot divisor) in
-      {
-        divided[32..63] := d;
-        overflow := o
-      };
-    (GPR[RT])[32..63] := divided[32 .. 63];
-    (GPR[RT])[0..31] := undefined;
-    if Rc
-    then {
-      (bit) xer_so := XER.SO;
-      if OE & overflow then xer_so := overflow else ();
-      if mode64bit | overflow
-      then CR.CR0 := [undefined,undefined,undefined,xer_so]
-      else set_overflow_cr0(divided,xer_so)
-    }
-    else ();
-    if OE then set_SO_OV(overflow) else ()
-  }
-
-union ast member (bit[5], bit[5], bit[5], bit, bit) Divwe
-
-function clause decode (0b011111 :
-(bit[5]) RT :
-(bit[5]) RA :
-(bit[5]) RB :
-[OE] :
-0b110101011 :
-[Rc] as instr) =
-  Some(Divwe(RT,RA,RB,OE,Rc))
-
-function clause execute (Divwe (RT, RA, RB, OE, Rc)) =
-  {
-    (bit[64]) dividend := (GPR[RA])[32 .. 63] : 0b00000000000000000000000000000000;
-    (bit[32]) divisor := (GPR[RB])[32 .. 63];
-    (bit[64]) divided := 0b0000000000000000000000000000000000000000000000000000000000000000;
-    (bit) overflow := 0;
-    let (d, o, _) = (dividend quot_s divisor) in
-      {
-        divided[32..63] := d[32 .. 63];
-        overflow := o
-      };
-    (GPR[RT])[32..63] := divided[32 .. 63];
-    (GPR[RT])[0..31] := undefined;
-    if Rc
-    then {
-      (bit) xer_so := XER.SO;
-      if OE & overflow then xer_so := overflow else ();
-      if mode64bit | overflow
-      then CR.CR0 := [undefined,undefined,undefined,xer_so]
-      else set_overflow_cr0(divided,xer_so)
-    }
-    else ();
-    if OE then set_SO_OV(overflow) else ()
-  }
-
-union ast member (bit[5], bit[5], bit[5], bit, bit) Divweu
-
-function clause decode (0b011111 :
-(bit[5]) RT :
-(bit[5]) RA :
-(bit[5]) RB :
-[OE] :
-0b110001011 :
-[Rc] as instr) =
-  Some(Divweu(RT,RA,RB,OE,Rc))
-
-function clause execute (Divweu (RT, RA, RB, OE, Rc)) =
-  {
-    (bit[64]) dividend := (GPR[RA])[32 .. 63] : 0b00000000000000000000000000000000;
-    (bit[32]) divisor := (GPR[RB])[32 .. 63];
-    (bit[64]) divided := 0b0000000000000000000000000000000000000000000000000000000000000000;
-    (bit) overflow := 0;
-    let (d, o, _) = (dividend quot divisor) in
-      {
-        divided[32..63] := d[32 .. 63];
-        overflow := o
-      };
-    (GPR[RT])[32..63] := divided[32 .. 63];
-    (GPR[RT])[0..31] := undefined;
-    if Rc
-    then {
-      (bit) xer_so := XER.SO;
-      if OE & overflow then xer_so := overflow else ();
-      if mode64bit | overflow
-      then CR.CR0 := [undefined,undefined,undefined,xer_so]
-      else set_overflow_cr0(divided,xer_so)
-    }
-    else ();
-    if OE then set_SO_OV(overflow) else ()
-  }
-
-union ast member (bit[5], bit[5], bit[5], bit, bit) Mulld
-
-function clause decode (0b011111 :
-(bit[5]) RT :
-(bit[5]) RA :
-(bit[5]) RB :
-[OE] :
-0b011101001 :
-[Rc] as instr) =
-  Some(Mulld(RT,RA,RB,OE,Rc))
-
-function clause execute (Mulld (RT, RA, RB, OE, Rc)) =
-  {
-    (bit[128]) prod := 0;
-    (bit) overflow := 0;
-    let (p, o, _) = (GPR[RA] *_s GPR[RB]) in
-      {
-        prod := p;
-        overflow := o
-      };
-    GPR[RT] := prod[64 .. 127];
-    if Rc
-    then {
-      (bit) xer_so := XER.SO;
-      if OE & overflow then xer_so := overflow else ();
-      set_overflow_cr0(prod[64 .. 127],xer_so)
-    }
-    else ();
-    if OE then set_SO_OV(overflow) else ()
-  }
-
-union ast member (bit[5], bit[5], bit[5], bit) Mulhd
-
-function clause decode (0b011111 :
-(bit[5]) RT :
-(bit[5]) RA :
-(bit[5]) RB :
-(bit[1]) _ :
-0b001001001 :
-[Rc] as instr) =
-  Some(Mulhd(RT,RA,RB,Rc))
-
-function clause execute (Mulhd (RT, RA, RB, Rc)) =
-  {
-    (bit[128]) prod := GPR[RA] *_s GPR[RB];
-    GPR[RT] := prod[0 .. 63];
-    if Rc then set_overflow_cr0(prod[0 .. 63],XER.SO) else ()
-  }
-
-union ast member (bit[5], bit[5], bit[5], bit) Mulhdu
-
-function clause decode (0b011111 :
-(bit[5]) RT :
-(bit[5]) RA :
-(bit[5]) RB :
-(bit[1]) _ :
-0b000001001 :
-[Rc] as instr) =
-  Some(Mulhdu(RT,RA,RB,Rc))
-
-function clause execute (Mulhdu (RT, RA, RB, Rc)) =
-  {
-    (bit[128]) prod := GPR[RA] * GPR[RB];
-    GPR[RT] := prod[0 .. 63];
-    if Rc then set_overflow_cr0(prod[0 .. 63],XER.SO) else ()
-  }
-
-union ast member (bit[5], bit[5], bit[5], bit, bit) Divd
-
-function clause decode (0b011111 :
-(bit[5]) RT :
-(bit[5]) RA :
-(bit[5]) RB :
-[OE] :
-0b111101001 :
-[Rc] as instr) =
-  Some(Divd(RT,RA,RB,OE,Rc))
-
-function clause execute (Divd (RT, RA, RB, OE, Rc)) =
-  {
-    (bit[64]) dividend := GPR[RA];
-    (bit[64]) divisor := GPR[RB];
-    (bit[64]) divided := 0b0000000000000000000000000000000000000000000000000000000000000000;
-    (bit) overflow := 0;
-    let (d, o, _) = (dividend quot_s divisor) in
-      {
-        divided := d;
-        overflow := o
-      };
-    GPR[RT] := divided;
-    if OE then set_SO_OV(overflow) else ();
-    if Rc then set_overflow_cr0(divided,overflow | XER.SO) else ()
-  }
-
-union ast member (bit[5], bit[5], bit[5], bit, bit) Divdu
-
-function clause decode (0b011111 :
-(bit[5]) RT :
-(bit[5]) RA :
-(bit[5]) RB :
-[OE] :
-0b111001001 :
-[Rc] as instr) =
-  Some(Divdu(RT,RA,RB,OE,Rc))
-
-function clause execute (Divdu (RT, RA, RB, OE, Rc)) =
-  {
-    (bit[64]) dividend := GPR[RA];
-    (bit[64]) divisor := GPR[RB];
-    (bit[64]) divided := 0b0000000000000000000000000000000000000000000000000000000000000000;
-    (bit) overflow := 0;
-    let (d, o, _) = (dividend quot divisor) in
-      {
-        divided := d;
-        overflow := o
-      };
-    GPR[RT] := divided;
-    if OE then set_SO_OV(overflow) else ();
-    if Rc then set_overflow_cr0(divided,overflow | XER.SO) else ()
-  }
-
-union ast member (bit[5], bit[5], bit[5], bit, bit) Divde
-
-function clause decode (0b011111 :
-(bit[5]) RT :
-(bit[5]) RA :
-(bit[5]) RB :
-[OE] :
-0b110101001 :
-[Rc] as instr) =
-  Some(Divde(RT,RA,RB,OE,Rc))
-
-function clause execute (Divde (RT, RA, RB, OE, Rc)) =
-  {
-    (bit[128]) dividend :=
-      GPR[RA] : 0b0000000000000000000000000000000000000000000000000000000000000000;
-    (bit[64]) divisor := GPR[RB];
-    (bit[128]) divided := 0;
-    (bit) overflow := 0;
-    let (d, o, _) = (dividend quot_s divisor) in
-      {
-        divided := d;
-        overflow := o
-      };
-    GPR[RT] := divided[64 .. 127];
-    if OE then set_SO_OV(overflow) else ();
-    if Rc
-    then {
-      (bit) xer_so := XER.SO;
-      if OE & overflow then xer_so := overflow else ();
-      if overflow
-      then CR.CR0 := [undefined,undefined,undefined,xer_so]
-      else set_overflow_cr0(divided[64 .. 127],xer_so)
-    }
-    else ()
-  }
-
-union ast member (bit[5], bit[5], bit[5], bit, bit) Divdeu
-
-function clause decode (0b011111 :
-(bit[5]) RT :
-(bit[5]) RA :
-(bit[5]) RB :
-[OE] :
-0b110001001 :
-[Rc] as instr) =
-  Some(Divdeu(RT,RA,RB,OE,Rc))
-
-function clause execute (Divdeu (RT, RA, RB, OE, Rc)) =
-  {
-    (bit[128]) dividend :=
-      GPR[RA] : 0b0000000000000000000000000000000000000000000000000000000000000000;
-    (bit[64]) divisor := GPR[RB];
-    (bit[128]) divided := 0;
-    (bit) overflow := 0;
-    let (d, o, _) = (dividend quot divisor) in
-      {
-        divided := d;
-        overflow := o
-      };
-    GPR[RT] := divided[64 .. 127];
-    if OE then set_SO_OV(overflow) else ();
-    if Rc
-    then {
-      (bit) xer_so := XER.SO;
-      if OE & overflow then xer_so := overflow else ();
-      if overflow
-      then CR.CR0 := [undefined,undefined,undefined,xer_so]
-      else set_overflow_cr0(divided[64 .. 127],xer_so)
-    }
-    else ()
-  }
-
-union ast member (bit[3], bit, bit[5], bit[16]) Cmpi
-
-function clause decode (0b001011 :
-(bit[3]) BF :
-(bit[1]) _ :
-[L] :
-(bit[5]) RA :
-(bit[16]) SI as instr) =
-  Some(Cmpi(BF,L,RA,SI))
-
-function clause execute (Cmpi (BF, L, RA, SI)) =
-  {
-    (bit[64]) a := 0;
-    if L == 0 then a := EXTS((GPR[RA])[32 .. 63]) else a := GPR[RA];
-    if a < EXTS(SI) then c := 0b100 else if a > EXTS(SI) then c := 0b010 else c := 0b001;
-    CR[4 * BF + 32..4 * BF + 35] := c : [XER.SO]
-  }
-
-union ast member (bit[3], bit, bit[5], bit[5]) Cmp
-
-function clause decode (0b011111 :
-(bit[3]) BF :
-(bit[1]) _ :
-[L] :
-(bit[5]) RA :
-(bit[5]) RB :
-0b0000000000 :
-(bit[1]) _ as instr) =
-  Some(Cmp(BF,L,RA,RB))
-
-function clause execute (Cmp (BF, L, RA, RB)) =
-  {
-    (bit[64]) a := 0;
-    (bit[64]) b := 0;
-    if L == 0
-    then {
-      a := EXTS((GPR[RA])[32 .. 63]);
-      b := EXTS((GPR[RB])[32 .. 63])
-    }
-    else {
-      a := GPR[RA];
-      b := GPR[RB]
-    };
-    if a < b then c := 0b100 else if a > b then c := 0b010 else c := 0b001;
-    CR[4 * BF + 32..4 * BF + 35] := c : [XER.SO]
-  }
-
-union ast member (bit[3], bit, bit[5], bit[16]) Cmpli
-
-function clause decode (0b001010 :
-(bit[3]) BF :
-(bit[1]) _ :
-[L] :
-(bit[5]) RA :
-(bit[16]) UI as instr) =
-  Some(Cmpli(BF,L,RA,UI))
-
-function clause execute (Cmpli (BF, L, RA, UI)) =
-  {
-    (bit[64]) a := 0;
-    (bit[3]) c := 0;
-    if L == 0 then a := 0b00000000000000000000000000000000 : (GPR[RA])[32 .. 63] else a := GPR[RA];
-    if a <_u 0b000000000000000000000000000000000000000000000000 : UI
-    then c := 0b100
-    else if a >_u 0b000000000000000000000000000000000000000000000000 : UI
-    then c := 0b010
-    else c := 0b001;
-    CR[4 * BF + 32..4 * BF + 35] := c : [XER.SO]
-  }
-
-union ast member (bit[3], bit, bit[5], bit[5]) Cmpl
-
-function clause decode (0b011111 :
-(bit[3]) BF :
-(bit[1]) _ :
-[L] :
-(bit[5]) RA :
-(bit[5]) RB :
-0b0000100000 :
-(bit[1]) _ as instr) =
-  Some(Cmpl(BF,L,RA,RB))
-
-function clause execute (Cmpl (BF, L, RA, RB)) =
-  {
-    (bit[64]) a := 0;
-    (bit[64]) b := 0;
-    (bit[3]) c := 0;
-    if L == 0
-    then {
-      a := 0b00000000000000000000000000000000 : (GPR[RA])[32 .. 63];
-      b := 0b00000000000000000000000000000000 : (GPR[RB])[32 .. 63]
-    }
-    else {
-      a := GPR[RA];
-      b := GPR[RB]
-    };
-    if a <_u b then c := 0b100 else if a >_u b then c := 0b010 else c := 0b001;
-    CR[4 * BF + 32..4 * BF + 35] := c : [XER.SO]
-  }
-
-union ast member (bit[5], bit[5], bit[5], bit[5]) Isel
-
-function clause decode (0b011111 :
-(bit[5]) RT :
-(bit[5]) RA :
-(bit[5]) RB :
-(bit[5]) BC :
-0b01111 :
-(bit[1]) _ as instr) =
-  Some(Isel(RT,RA,RB,BC))
-
-function clause execute (Isel (RT, RA, RB, BC)) =
-  {
-    (bit[64]) a := 0;
-    if RA == 0 then a := 0 else a := GPR[RA];
-    if CR[BC + 32] == 1
-    then {
-      GPR[RT] := a;
-      discard := GPR[RB]
-    }
-    else GPR[RT] := GPR[RB]
-  }
-
-union ast member (bit[5], bit[5], bit[16]) Andi
-
-function clause decode (0b011100 :
-(bit[5]) RS :
-(bit[5]) RA :
-(bit[16]) UI as instr) =
-  Some(Andi(RS,RA,UI))
-
-function clause execute (Andi (RS, RA, UI)) =
-  {
-    (bit[64]) temp := (GPR[RS] & 0b000000000000000000000000000000000000000000000000 : UI);
-    GPR[RA] := temp;
-    set_overflow_cr0(temp,XER.SO)
-  }
-
-union ast member (bit[5], bit[5], bit[16]) Andis
-
-function clause decode (0b011101 :
-(bit[5]) RS :
-(bit[5]) RA :
-(bit[16]) UI as instr) =
-  Some(Andis(RS,RA,UI))
-
-function clause execute (Andis (RS, RA, UI)) =
-  {
-    (bit[64]) temp := (GPR[RS] & 0b00000000000000000000000000000000 : UI : 0b0000000000000000);
-    GPR[RA] := temp;
-    set_overflow_cr0(temp,XER.SO)
-  }
-
-union ast member (bit[5], bit[5], bit[16]) Ori
-
-function clause decode (0b011000 :
-(bit[5]) RS :
-(bit[5]) RA :
-(bit[16]) UI as instr) =
-  Some(Ori(RS,RA,UI))
-
-function clause execute (Ori (RS, RA, UI)) =
-  GPR[RA] := (GPR[RS] | 0b000000000000000000000000000000000000000000000000 : UI)
-
-union ast member (bit[5], bit[5], bit[16]) Oris
-
-function clause decode (0b011001 :
-(bit[5]) RS :
-(bit[5]) RA :
-(bit[16]) UI as instr) =
-  Some(Oris(RS,RA,UI))
-
-function clause execute (Oris (RS, RA, UI)) =
-  GPR[RA] := (GPR[RS] | 0b00000000000000000000000000000000 : UI : 0b0000000000000000)
-
-union ast member (bit[5], bit[5], bit[16]) Xori
-
-function clause decode (0b011010 :
-(bit[5]) RS :
-(bit[5]) RA :
-(bit[16]) UI as instr) =
-  Some(Xori(RS,RA,UI))
-
-function clause execute (Xori (RS, RA, UI)) =
-  GPR[RA] := GPR[RS] ^ 0b000000000000000000000000000000000000000000000000 : UI
-
-union ast member (bit[5], bit[5], bit[16]) Xoris
-
-function clause decode (0b011011 :
-(bit[5]) RS :
-(bit[5]) RA :
-(bit[16]) UI as instr) =
-  Some(Xoris(RS,RA,UI))
-
-function clause execute (Xoris (RS, RA, UI)) =
-  GPR[RA] := GPR[RS] ^ 0b00000000000000000000000000000000 : UI : 0b0000000000000000
-
-union ast member (bit[5], bit[5], bit[5], bit) And
-
-function clause decode (0b011111 :
-(bit[5]) RS :
-(bit[5]) RA :
-(bit[5]) RB :
-0b0000011100 :
-[Rc] as instr) =
-  Some(And(RS,RA,RB,Rc))
-
-function clause execute (And (RS, RA, RB, Rc)) =
-  {
-    (bit[64]) temp := (GPR[RS] & GPR[RB]);
-    GPR[RA] := temp;
-    if Rc then set_overflow_cr0(temp,XER.SO) else ()
-  }
-
-union ast member (bit[5], bit[5], bit[5], bit) Xor
-
-function clause decode (0b011111 :
-(bit[5]) RS :
-(bit[5]) RA :
-(bit[5]) RB :
-0b0100111100 :
-[Rc] as instr) =
-  Some(Xor(RS,RA,RB,Rc))
-
-function clause execute (Xor (RS, RA, RB, Rc)) =
-  {
-    (bit[64]) temp := 0;
-    if RS == RB
-    then {
-      temp := GPR[RS];
-      temp := 0;
-      GPR[RA] := 0
-    }
-    else {
-      temp := GPR[RS] ^ GPR[RB];
-      GPR[RA] := temp
-    };
-    if Rc then set_overflow_cr0(temp,XER.SO) else ()
-  }
-
-union ast member (bit[5], bit[5], bit[5], bit) Nand
-
-function clause decode (0b011111 :
-(bit[5]) RS :
-(bit[5]) RA :
-(bit[5]) RB :
-0b0111011100 :
-[Rc] as instr) =
-  Some(Nand(RS,RA,RB,Rc))
-
-function clause execute (Nand (RS, RA, RB, Rc)) =
-  {
-    (bit[64]) temp := ~(GPR[RS] & GPR[RB]);
-    GPR[RA] := temp;
-    if Rc then set_overflow_cr0(temp,XER.SO) else ()
-  }
-
-union ast member (bit[5], bit[5], bit[5], bit) Or
-
-function clause decode (0b011111 :
-(bit[5]) RS :
-(bit[5]) RA :
-(bit[5]) RB :
-0b0110111100 :
-[Rc] as instr) =
-  Some(Or(RS,RA,RB,Rc))
-
-function clause execute (Or (RS, RA, RB, Rc)) =
-  {
-    (bit[64]) temp := (GPR[RS] | GPR[RB]);
-    GPR[RA] := temp;
-    if Rc then set_overflow_cr0(temp,XER.SO) else ()
-  }
-
-union ast member (bit[5], bit[5], bit[5], bit) Nor
-
-function clause decode (0b011111 :
-(bit[5]) RS :
-(bit[5]) RA :
-(bit[5]) RB :
-0b0001111100 :
-[Rc] as instr) =
-  Some(Nor(RS,RA,RB,Rc))
-
-function clause execute (Nor (RS, RA, RB, Rc)) =
-  {
-    (bit[64]) temp := ~(GPR[RS] | GPR[RB]);
-    GPR[RA] := temp;
-    if Rc then set_overflow_cr0(temp,XER.SO) else ()
-  }
-
-union ast member (bit[5], bit[5], bit[5], bit) Eqv
-
-function clause decode (0b011111 :
-(bit[5]) RS :
-(bit[5]) RA :
-(bit[5]) RB :
-0b0100011100 :
-[Rc] as instr) =
-  Some(Eqv(RS,RA,RB,Rc))
-
-function clause execute (Eqv (RS, RA, RB, Rc)) =
-  {
-    (bit[64]) temp := GPR[RS] ^ ~(GPR[RB]);
-    GPR[RA] := temp;
-    if Rc then set_overflow_cr0(temp,XER.SO) else ()
-  }
-
-union ast member (bit[5], bit[5], bit[5], bit) Andc
-
-function clause decode (0b011111 :
-(bit[5]) RS :
-(bit[5]) RA :
-(bit[5]) RB :
-0b0000111100 :
-[Rc] as instr) =
-  Some(Andc(RS,RA,RB,Rc))
-
-function clause execute (Andc (RS, RA, RB, Rc)) =
-  {
-    (bit[64]) temp := (GPR[RS] & ~(GPR[RB]));
-    GPR[RA] := temp;
-    if Rc then set_overflow_cr0(temp,XER.SO) else ()
-  }
-
-union ast member (bit[5], bit[5], bit[5], bit) Orc
-
-function clause decode (0b011111 :
-(bit[5]) RS :
-(bit[5]) RA :
-(bit[5]) RB :
-0b0110011100 :
-[Rc] as instr) =
-  Some(Orc(RS,RA,RB,Rc))
-
-function clause execute (Orc (RS, RA, RB, Rc)) =
-  {
-    (bit[64]) temp := (GPR[RS] | ~(GPR[RB]));
-    GPR[RA] := temp;
-    if Rc then set_overflow_cr0(temp,XER.SO) else ()
-  }
-
-union ast member (bit[5], bit[5], bit) Extsb
-
-function clause decode (0b011111 :
-(bit[5]) RS :
-(bit[5]) RA :
-(bit[5]) _ :
-0b1110111010 :
-[Rc] as instr) =
-  Some(Extsb(RS,RA,Rc))
-
-function clause execute (Extsb (RS, RA, Rc)) =
-  {
-    (bit[64]) temp := 0;
-    s := (GPR[RS])[56];
-    temp[56..63] := (GPR[RS])[56 .. 63];
-    (GPR[RA])[56..63] := temp[56 .. 63];
-    temp[0..55] := s ^^ 56;
-    (GPR[RA])[0..55] := temp[0 .. 55];
-    if Rc then set_overflow_cr0(temp,XER.SO) else ()
-  }
-
-union ast member (bit[5], bit[5], bit) Extsh
-
-function clause decode (0b011111 :
-(bit[5]) RS :
-(bit[5]) RA :
-(bit[5]) _ :
-0b1110011010 :
-[Rc] as instr) =
-  Some(Extsh(RS,RA,Rc))
-
-function clause execute (Extsh (RS, RA, Rc)) =
-  {
-    (bit[64]) temp := 0;
-    s := (GPR[RS])[48];
-    temp[48..63] := (GPR[RS])[48 .. 63];
-    (GPR[RA])[48..63] := temp[48 .. 63];
-    temp[0..47] := s ^^ 48;
-    (GPR[RA])[0..47] := temp[0 .. 47];
-    if Rc then set_overflow_cr0(temp,XER.SO) else ()
-  }
-
-union ast member (bit[5], bit[5], bit) Cntlzw
-
-function clause decode (0b011111 :
-(bit[5]) RS :
-(bit[5]) RA :
-(bit[5]) _ :
-0b0000011010 :
-[Rc] as instr) =
-  Some(Cntlzw(RS,RA,Rc))
-
-function clause execute (Cntlzw (RS, RA, Rc)) =
-  {
-    temp := (bit[64]) (countLeadingZeroes(GPR[RS],32));
-    GPR[RA] := temp;
-    if Rc then set_overflow_cr0(temp,XER.SO) else ()
-  }
-
-union ast member (bit[5], bit[5], bit[5]) Cmpb
-
-function clause decode (0b011111 :
-(bit[5]) RS :
-(bit[5]) RA :
-(bit[5]) RB :
-0b0111111100 :
-(bit[1]) _ as instr) =
-  Some(Cmpb(RS,RA,RB))
-
-function clause execute (Cmpb (RS, RA, RB)) =
-  foreach (n from 0 to 7 by 1 in inc)
-  if (GPR[RS])[8 * n .. 8 * n + 7] == (GPR[RB])[8 * n .. 8 * n + 7]
-  then (GPR[RA])[8 * n..8 * n + 7] := 0b11111111
-  else (GPR[RA])[8 * n..8 * n + 7] := (bit[8]) 0
-
-union ast member (bit[5], bit[5]) Popcntb
-
-function clause decode (0b011111 :
-(bit[5]) RS :
-(bit[5]) RA :
-(bit[5]) _ :
-0b0001111010 :
-(bit[1]) _ as instr) =
-  Some(Popcntb(RS,RA))
-
-function clause execute (Popcntb (RS, RA)) =
-  foreach (i from 0 to 7 by 1 in inc)
-  {
-    ([|64|]) n := 0;
-    foreach (j from 0 to 7 by 1 in inc) if (GPR[RS])[i * 8 + j] == 1 then n := n + 1 else ();
-    (GPR[RA])[i * 8..i * 8 + 7] := (bit[8]) n
-  }
-
-union ast member (bit[5], bit[5]) Popcntw
-
-function clause decode (0b011111 :
-(bit[5]) RS :
-(bit[5]) RA :
-(bit[5]) _ :
-0b0101111010 :
-(bit[1]) _ as instr) =
-  Some(Popcntw(RS,RA))
-
-function clause execute (Popcntw (RS, RA)) =
-  foreach (i from 0 to 1 by 1 in inc)
-  {
-    ([|64|]) n := 0;
-    foreach (j from 0 to 31 by 1 in inc) if (GPR[RS])[i * 32 + j] == 1 then n := n + 1 else ();
-    (GPR[RA])[i * 32..i * 32 + 31] := (bit[32]) n
-  }
-
-union ast member (bit[5], bit[5]) Prtyd
-
-function clause decode (0b011111 :
-(bit[5]) RS :
-(bit[5]) RA :
-(bit[5]) _ :
-0b0010111010 :
-(bit[1]) _ as instr) =
-  Some(Prtyd(RS,RA))
-
-function clause execute (Prtyd (RS, RA)) =
-  {
-    s := 0;
-    foreach (i from 0 to 7 by 1 in inc) s := s ^ (GPR[RS])[i * 8 + 7];
-    GPR[RA] := 0b000000000000000000000000000000000000000000000000000000000000000 : [s]
-  }
-
-union ast member (bit[5], bit[5]) Prtyw
-
-function clause decode (0b011111 :
-(bit[5]) RS :
-(bit[5]) RA :
-(bit[5]) _ :
-0b0010011010 :
-(bit[1]) _ as instr) =
-  Some(Prtyw(RS,RA))
-
-function clause execute (Prtyw (RS, RA)) =
-  {
-    s := 0;
-    t := 0;
-    foreach (i from 0 to 3 by 1 in inc) s := s ^ (GPR[RS])[i * 8 + 7];
-    foreach (i from 4 to 7 by 1 in inc) t := t ^ (GPR[RS])[i * 8 + 7];
-    (GPR[RA])[0..31] := 0b0000000000000000000000000000000 : [s];
-    (GPR[RA])[32..63] := 0b0000000000000000000000000000000 : [t]
-  }
-
-union ast member (bit[5], bit[5], bit) Extsw
-
-function clause decode (0b011111 :
-(bit[5]) RS :
-(bit[5]) RA :
-(bit[5]) _ :
-0b1111011010 :
-[Rc] as instr) =
-  Some(Extsw(RS,RA,Rc))
-
-function clause execute (Extsw (RS, RA, Rc)) =
-  {
-    s := (GPR[RS])[32];
-    (bit[64]) temp := 0;
-    temp[32..63] := (GPR[RS])[32 .. 63];
-    temp[0..31] := s ^^ 32;
-    if Rc then set_overflow_cr0(temp,XER.SO) else ();
-    GPR[RA] := temp
-  }
-
-union ast member (bit[5], bit[5], bit) Cntlzd
-
-function clause decode (0b011111 :
-(bit[5]) RS :
-(bit[5]) RA :
-(bit[5]) _ :
-0b0000111010 :
-[Rc] as instr) =
-  Some(Cntlzd(RS,RA,Rc))
-
-function clause execute (Cntlzd (RS, RA, Rc)) =
-  {
-    temp := (bit[64]) (countLeadingZeroes(GPR[RS],0));
-    GPR[RA] := temp;
-    if Rc then set_overflow_cr0(temp,XER.SO) else ()
-  }
-
-union ast member (bit[5], bit[5]) Popcntd
-
-function clause decode (0b011111 :
-(bit[5]) RS :
-(bit[5]) RA :
-(bit[5]) _ :
-0b0111111010 :
-(bit[1]) _ as instr) =
-  Some(Popcntd(RS,RA))
-
-function clause execute (Popcntd (RS, RA)) =
-  {
-    ([|64|]) n := 0;
-    foreach (i from 0 to 63 by 1 in inc) if (GPR[RS])[i] == 1 then n := n + 1 else ();
-    GPR[RA] := (bit[64]) n
-  }
-
-union ast member (bit[5], bit[5], bit[5]) Bpermd
-
-function clause decode (0b011111 :
-(bit[5]) RS :
-(bit[5]) RA :
-(bit[5]) RB :
-0b0011111100 :
-(bit[1]) _ as instr) =
-  Some(Bpermd(RS,RA,RB))
-
-function clause execute (Bpermd (RS, RA, RB)) =
-  {
-    (bit[8]) perm := 0;
-    foreach (i from 0 to 7 by 1 in inc)
-    {
-      index := (GPR[RS])[8 * i .. 8 * i + 7];
-      if index <_u (bit[8]) 64
-      then perm[i] := (GPR[RB])[index]
-      else {
-        perm[i] := 0;
-        discard := GPR[RB]
-      }
-    };
-    GPR[RA] := 0b00000000000000000000000000000000000000000000000000000000 : perm[0 .. 7]
-  }
-
-union ast member (bit[5], bit[5], bit[5], bit[5], bit[5], bit) Rlwinm
-
-function clause decode (0b010101 :
-(bit[5]) RS :
-(bit[5]) RA :
-(bit[5]) SH :
-(bit[5]) MB :
-(bit[5]) ME :
-[Rc] as instr) =
-  Some(Rlwinm(RS,RA,SH,MB,ME,Rc))
-
-function clause execute (Rlwinm (RS, RA, SH, MB, ME, Rc)) =
-  {
-    n := SH;
-    r := ROTL((GPR[RS])[32 .. 63] : (GPR[RS])[32 .. 63],n);
-    m := MASK(MB + 32,ME + 32);
-    (bit[64]) temp := (r & m);
-    GPR[RA] := temp;
-    if Rc then set_overflow_cr0(temp,XER.SO) else ()
-  }
-
-union ast member (bit[5], bit[5], bit[5], bit[5], bit[5], bit) Rlwnm
-
-function clause decode (0b010111 :
-(bit[5]) RS :
-(bit[5]) RA :
-(bit[5]) RB :
-(bit[5]) MB :
-(bit[5]) ME :
-[Rc] as instr) =
-  Some(Rlwnm(RS,RA,RB,MB,ME,Rc))
-
-function clause execute (Rlwnm (RS, RA, RB, MB, ME, Rc)) =
-  {
-    n := (GPR[RB])[59 .. 63];
-    r := ROTL((GPR[RS])[32 .. 63] : (GPR[RS])[32 .. 63],n);
-    m := MASK(MB + 32,ME + 32);
-    (bit[64]) temp := (r & m);
-    GPR[RA] := temp;
-    if Rc then set_overflow_cr0(temp,XER.SO) else ()
-  }
-
-union ast member (bit[5], bit[5], bit[5], bit[5], bit[5], bit) Rlwimi
-
-function clause decode (0b010100 :
-(bit[5]) RS :
-(bit[5]) RA :
-(bit[5]) SH :
-(bit[5]) MB :
-(bit[5]) ME :
-[Rc] as instr) =
-  Some(Rlwimi(RS,RA,SH,MB,ME,Rc))
-
-function clause execute (Rlwimi (RS, RA, SH, MB, ME, Rc)) =
-  {
-    n := SH;
-    r := ROTL((GPR[RS])[32 .. 63] : (GPR[RS])[32 .. 63],n);
-    m := MASK(MB + 32,ME + 32);
-    (bit[64]) temp := (r & m | GPR[RA] & ~(m));
-    GPR[RA] := temp;
-    if Rc then set_overflow_cr0(temp,XER.SO) else ()
-  }
-
-union ast member (bit[5], bit[5], bit[6], bit[6], bit) Rldicl
-
-function clause decode (0b011110 :
-(bit[5]) RS :
-(bit[5]) RA :
-(bit[5]) _ :
-(bit[6]) mb :
-0b000 :
-(bit[1]) _ :
-[Rc] as instr) =
-  Some(Rldicl(RS,RA,instr[16 .. 20] : instr[30 .. 30],mb,Rc))
-
-function clause execute (Rldicl (RS, RA, sh, mb, Rc)) =
-  {
-    n := [sh[5]] : sh[0 .. 4];
-    r := ROTL(GPR[RS],n);
-    b := [mb[5]] : mb[0 .. 4];
-    m := MASK(b,63);
-    (bit[64]) temp := (r & m);
-    GPR[RA] := temp;
-    if Rc then set_overflow_cr0(temp,XER.SO) else ()
-  }
-
-union ast member (bit[5], bit[5], bit[6], bit[6], bit) Rldicr
-
-function clause decode (0b011110 :
-(bit[5]) RS :
-(bit[5]) RA :
-(bit[5]) _ :
-(bit[6]) me :
-0b001 :
-(bit[1]) _ :
-[Rc] as instr) =
-  Some(Rldicr(RS,RA,instr[16 .. 20] : instr[30 .. 30],me,Rc))
-
-function clause execute (Rldicr (RS, RA, sh, me, Rc)) =
-  {
-    n := [sh[5]] : sh[0 .. 4];
-    r := ROTL(GPR[RS],n);
-    e := [me[5]] : me[0 .. 4];
-    m := MASK(0,e);
-    (bit[64]) temp := (r & m);
-    GPR[RA] := temp;
-    if Rc then set_overflow_cr0(temp,XER.SO) else ()
-  }
-
-union ast member (bit[5], bit[5], bit[6], bit[6], bit) Rldic
-
-function clause decode (0b011110 :
-(bit[5]) RS :
-(bit[5]) RA :
-(bit[5]) _ :
-(bit[6]) mb :
-0b010 :
-(bit[1]) _ :
-[Rc] as instr) =
-  Some(Rldic(RS,RA,instr[16 .. 20] : instr[30 .. 30],mb,Rc))
-
-function clause execute (Rldic (RS, RA, sh, mb, Rc)) =
-  {
-    n := [sh[5]] : sh[0 .. 4];
-    r := ROTL(GPR[RS],n);
-    b := [mb[5]] : mb[0 .. 4];
-    m := MASK(b,(bit[6]) (~(n)));
-    (bit[64]) temp := (r & m);
-    GPR[RA] := temp;
-    if Rc then set_overflow_cr0(temp,XER.SO) else ()
-  }
-
-union ast member (bit[5], bit[5], bit[5], bit[6], bit) Rldcl
-
-function clause decode (0b011110 :
-(bit[5]) RS :
-(bit[5]) RA :
-(bit[5]) RB :
-(bit[6]) mb :
-0b1000 :
-[Rc] as instr) =
-  Some(Rldcl(RS,RA,RB,mb,Rc))
-
-function clause execute (Rldcl (RS, RA, RB, mb, Rc)) =
-  {
-    n := (GPR[RB])[58 .. 63];
-    r := ROTL(GPR[RS],n);
-    b := [mb[5]] : mb[0 .. 4];
-    m := MASK(b,63);
-    (bit[64]) temp := (r & m);
-    GPR[RA] := temp;
-    if Rc then set_overflow_cr0(temp,XER.SO) else ()
-  }
-
-union ast member (bit[5], bit[5], bit[5], bit[6], bit) Rldcr
-
-function clause decode (0b011110 :
-(bit[5]) RS :
-(bit[5]) RA :
-(bit[5]) RB :
-(bit[6]) me :
-0b1001 :
-[Rc] as instr) =
-  Some(Rldcr(RS,RA,RB,me,Rc))
-
-function clause execute (Rldcr (RS, RA, RB, me, Rc)) =
-  {
-    n := (GPR[RB])[58 .. 63];
-    r := ROTL(GPR[RS],n);
-    e := [me[5]] : me[0 .. 4];
-    m := MASK(0,e);
-    (bit[64]) temp := (r & m);
-    GPR[RA] := temp;
-    if Rc then set_overflow_cr0(temp,XER.SO) else ()
-  }
-
-union ast member (bit[5], bit[5], bit[6], bit[6], bit) Rldimi
-
-function clause decode (0b011110 :
-(bit[5]) RS :
-(bit[5]) RA :
-(bit[5]) _ :
-(bit[6]) mb :
-0b011 :
-(bit[1]) _ :
-[Rc] as instr) =
-  Some(Rldimi(RS,RA,instr[16 .. 20] : instr[30 .. 30],mb,Rc))
-
-function clause execute (Rldimi (RS, RA, sh, mb, Rc)) =
-  {
-    n := [sh[5]] : sh[0 .. 4];
-    r := ROTL(GPR[RS],n);
-    b := [mb[5]] : mb[0 .. 4];
-    m := MASK(b,(bit[6]) (~(n)));
-    (bit[64]) temp := (r & m | GPR[RA] & ~(m));
-    GPR[RA] := temp;
-    if Rc then set_overflow_cr0(temp,XER.SO) else ()
-  }
-
-union ast member (bit[5], bit[5], bit[5], bit) Slw
-
-function clause decode (0b011111 :
-(bit[5]) RS :
-(bit[5]) RA :
-(bit[5]) RB :
-0b0000011000 :
-[Rc] as instr) =
-  Some(Slw(RS,RA,RB,Rc))
-
-function clause execute (Slw (RS, RA, RB, Rc)) =
-  {
-    n := (GPR[RB])[59 .. 63];
-    r := ROTL((GPR[RS])[32 .. 63] : (GPR[RS])[32 .. 63],n);
-    if (GPR[RB])[58] == 0
-    then m := MASK(32,63 - n)
-    else m := 0b0000000000000000000000000000000000000000000000000000000000000000;
-    (bit[64]) temp := (r & m);
-    GPR[RA] := temp;
-    if Rc then set_overflow_cr0(temp,XER.SO) else ()
-  }
-
-union ast member (bit[5], bit[5], bit[5], bit) Srw
-
-function clause decode (0b011111 :
-(bit[5]) RS :
-(bit[5]) RA :
-(bit[5]) RB :
-0b1000011000 :
-[Rc] as instr) =
-  Some(Srw(RS,RA,RB,Rc))
-
-function clause execute (Srw (RS, RA, RB, Rc)) =
-  {
-    n := (GPR[RB])[59 .. 63];
-    r := ROTL((GPR[RS])[32 .. 63] : (GPR[RS])[32 .. 63],64 - n);
-    if (GPR[RB])[58] == 0
-    then m := MASK(n + 32,63)
-    else m := 0b0000000000000000000000000000000000000000000000000000000000000000;
-    (bit[64]) temp := (r & m);
-    GPR[RA] := temp;
-    if Rc then set_overflow_cr0(temp,XER.SO) else ()
-  }
-
-union ast member (bit[5], bit[5], bit[5], bit) Srawi
-
-function clause decode (0b011111 :
-(bit[5]) RS :
-(bit[5]) RA :
-(bit[5]) SH :
-0b1100111000 :
-[Rc] as instr) =
-  Some(Srawi(RS,RA,SH,Rc))
-
-function clause execute (Srawi (RS, RA, SH, Rc)) =
-  {
-    n := SH;
-    r := ROTL((GPR[RS])[32 .. 63] : (GPR[RS])[32 .. 63],64 - n);
-    m := MASK(n + 32,63);
-    s := (GPR[RS])[32];
-    (bit[64]) temp := (r & m | s ^^ 64 & ~(m));
-    GPR[RA] := temp;
-    if Rc then set_overflow_cr0(temp,XER.SO) else ();
-    XER.CA := if n >_u (bit[5]) 0 then s & ~((r & ~(m)) == 0) else 0
-  }
-
-union ast member (bit[5], bit[5], bit[5], bit) Sraw
-
-function clause decode (0b011111 :
-(bit[5]) RS :
-(bit[5]) RA :
-(bit[5]) RB :
-0b1100011000 :
-[Rc] as instr) =
-  Some(Sraw(RS,RA,RB,Rc))
-
-function clause execute (Sraw (RS, RA, RB, Rc)) =
-  {
-    n := (GPR[RB])[59 .. 63];
-    r := ROTL((GPR[RS])[32 .. 63] : (GPR[RS])[32 .. 63],64 - n);
-    if (GPR[RB])[58] == 0
-    then m := MASK(n + 32,63)
-    else m := 0b0000000000000000000000000000000000000000000000000000000000000000;
-    s := (GPR[RS])[32];
-    (bit[64]) temp := (r & m | s ^^ 64 & ~(m));
-    GPR[RA] := temp;
-    if Rc then set_overflow_cr0(temp,XER.SO) else ();
-    XER.CA := if n >_u (bit[5]) 0 then s & ~((r & ~(m)) == 0) else 0
-  }
-
-union ast member (bit[5], bit[5], bit[5], bit) Sld
-
-function clause decode (0b011111 :
-(bit[5]) RS :
-(bit[5]) RA :
-(bit[5]) RB :
-0b0000011011 :
-[Rc] as instr) =
-  Some(Sld(RS,RA,RB,Rc))
-
-function clause execute (Sld (RS, RA, RB, Rc)) =
-  {
-    n := (GPR[RB])[58 .. 63];
-    r := ROTL(GPR[RS],n);
-    if (GPR[RB])[57] == 0
-    then m := MASK(0,63 - n)
-    else m := 0b0000000000000000000000000000000000000000000000000000000000000000;
-    (bit[64]) temp := (r & m);
-    GPR[RA] := temp;
-    if Rc then set_overflow_cr0(temp,XER.SO) else ()
-  }
-
-union ast member (bit[5], bit[5], bit[5], bit) Srd
-
-function clause decode (0b011111 :
-(bit[5]) RS :
-(bit[5]) RA :
-(bit[5]) RB :
-0b1000011011 :
-[Rc] as instr) =
-  Some(Srd(RS,RA,RB,Rc))
-
-function clause execute (Srd (RS, RA, RB, Rc)) =
-  {
-    n := (GPR[RB])[58 .. 63];
-    r := ROTL(GPR[RS],64 - n);
-    if (GPR[RB])[57] == 0
-    then m := MASK(n,63)
-    else m := 0b0000000000000000000000000000000000000000000000000000000000000000;
-    (bit[64]) temp := (r & m);
-    GPR[RA] := temp;
-    if Rc then set_overflow_cr0(temp,XER.SO) else ()
-  }
-
-union ast member (bit[5], bit[5], bit[6], bit) Sradi
-
-function clause decode (0b011111 :
-(bit[5]) RS :
-(bit[5]) RA :
-(bit[5]) _ :
-0b110011101 :
-(bit[1]) _ :
-[Rc] as instr) =
-  Some(Sradi(RS,RA,instr[16 .. 20] : instr[30 .. 30],Rc))
-
-function clause execute (Sradi (RS, RA, sh, Rc)) =
-  {
-    n := [sh[5]] : sh[0 .. 4];
-    r := ROTL(GPR[RS],64 - n);
-    m := MASK(n,63);
-    s := (GPR[RS])[0];
-    (bit[64]) temp := (r & m | s ^^ 64 & ~(m));
-    GPR[RA] := temp;
-    if Rc then set_overflow_cr0(temp,XER.SO) else ();
-    XER.CA := if n >_u (bit[6]) 0 then s & ~((r & ~(m)) == 0) else 0
-  }
-
-union ast member (bit[5], bit[5], bit[5], bit) Srad
-
-function clause decode (0b011111 :
-(bit[5]) RS :
-(bit[5]) RA :
-(bit[5]) RB :
-0b1100011010 :
-[Rc] as instr) =
-  Some(Srad(RS,RA,RB,Rc))
-
-function clause execute (Srad (RS, RA, RB, Rc)) =
-  {
-    n := (GPR[RB])[58 .. 63];
-    r := ROTL(GPR[RS],64 - n);
-    if (GPR[RB])[57] == 0
-    then m := MASK(n,63)
-    else m := 0b0000000000000000000000000000000000000000000000000000000000000000;
-    s := (GPR[RS])[0];
-    (bit[64]) temp := (r & m | s ^^ 64 & ~(m));
-    GPR[RA] := temp;
-    if Rc then set_overflow_cr0(temp,XER.SO) else ();
-    XER.CA := if n >_u (bit[6]) 0 then s & ~((r & ~(m)) == 0) else 0
-  }
-
-union ast member (bit[5], bit[5]) Cdtbcd
-
-function clause decode (0b011111 :
-(bit[5]) RS :
-(bit[5]) RA :
-(bit[5]) _ :
-0b0100011010 :
-(bit[1]) _ as instr) =
-  Some(Cdtbcd(RS,RA))
-
-function clause execute (Cdtbcd (RS, RA)) =
-  foreach (i from 0 to 1 by 1 in inc)
-  {
-    n := i * 32;
-    (GPR[RA])[n + 0..n + 7] := (bit[8]) 0;
-    (GPR[RA])[n + 8..n + 19] := DEC_TO_BCD((GPR[RS])[n + 12 .. n + 21]);
-    (GPR[RA])[n + 20..n + 31] := DEC_TO_BCD((GPR[RS])[n + 22 .. n + 31])
-  }
-
-union ast member (bit[5], bit[5]) Cbcdtd
-
-function clause decode (0b011111 :
-(bit[5]) RS :
-(bit[5]) RA :
-(bit[5]) _ :
-0b0100111010 :
-(bit[1]) _ as instr) =
-  Some(Cbcdtd(RS,RA))
-
-function clause execute (Cbcdtd (RS, RA)) =
-  foreach (i from 0 to 1 by 1 in inc)
-  {
-    n := i * 32;
-    (GPR[RA])[n + 0..n + 11] := (bit[12]) 0;
-    (GPR[RA])[n + 12..n + 21] := BCD_TO_DEC((GPR[RS])[n + 8 .. n + 19]);
-    (GPR[RA])[n + 22..n + 31] := BCD_TO_DEC((GPR[RS])[n + 20 .. n + 31])
-  }
-
-union ast member (bit[5], bit[5], bit[5]) Addg6s
-
-function clause decode (0b011111 :
-(bit[5]) RT :
-(bit[5]) RA :
-(bit[5]) RB :
-(bit[1]) _ :
-0b001001010 :
-(bit[1]) _ as instr) =
-  Some(Addg6s(RT,RA,RB))
-
-function clause execute (Addg6s (RT, RA, RB)) =
-  {
-    (bit[16]) dc := 0;
-    foreach (i from 0 to 15 by 1 in inc)
-    let (v, _, co) = ((GPR[RA])[4 * i .. 63] + (GPR[RB])[4 * i .. 63]) in dc[i] := carry_out(v,co);
-    c :=
-      (dc[0] ^^ 4) :
-        (dc[1] ^^ 4) :
-          (dc[2] ^^ 4) :
-            (dc[3] ^^ 4) :
-              (dc[4] ^^ 4) :
-                (dc[5] ^^ 4) :
-                  (dc[6] ^^ 4) :
-                    (dc[7] ^^ 4) :
-                      (dc[8] ^^ 4) :
-                        (dc[9] ^^ 4) :
-                          (dc[10] ^^ 4) :
-                            (dc[11] ^^ 4) :
-                              (dc[12] ^^ 4) : (dc[13] ^^ 4) : (dc[14] ^^ 4) : (dc[15] ^^ 4);
-    GPR[RT] := (~(c) & 0b0110011001100110011001100110011001100110011001100110011001100110)
-  }
-
-union ast member (bit[5], bit[10]) Mtspr
-
-function clause decode (0b011111 :
-(bit[5]) RS :
-(bit[10]) spr :
-0b0111010011 :
-(bit[1]) _ as instr) =
-  Some(Mtspr(RS,spr))
-
-function clause execute (Mtspr (RS, spr)) =
-  {
-    n := spr[5 .. 9] : spr[0 .. 4];
-    if n == 13
-    then trap(())
-    else if n == 1
-    then {
-      (bit[64]) reg := GPR[RS];
-      (bit[32]) front := zero_or_undef(reg[0 .. 31]);
-      (bit) xer_so := reg[32];
-      (bit) xer_ov := reg[33];
-      (bit) xer_ca := reg[34];
-      (bit[22]) mid := zero_or_undef(reg[35 .. 56]);
-      (bit[7]) bot := reg[57 .. 63];
-      XER := front : [xer_so] : [xer_ov] : [xer_ca] : mid : bot
-    }
-    else if length(SPR[n]) == 64
-    then SPR[n] := GPR[RS]
-    else if n == 152 then CTRL := (GPR[RS])[32 .. 63] else ()
-  }
-
-union ast member (bit[5], bit[10]) Mfspr
-
-function clause decode (0b011111 :
-(bit[5]) RT :
-(bit[10]) spr :
-0b0101010011 :
-(bit[1]) _ as instr) =
-  Some(Mfspr(RT,spr))
-
-function clause execute (Mfspr (RT, spr)) =
-  {
-    n := spr[5 .. 9] : spr[0 .. 4];
-    if length(SPR[n]) == 64
-    then GPR[RT] := SPR[n]
-    else GPR[RT] := 0b00000000000000000000000000000000 : SPR[n]
-  }
-
-union ast member (bit[5], bit[8]) Mtcrf
-
-function clause decode (0b011111 :
-(bit[5]) RS :
-0b0 :
-(bit[8]) FXM :
-(bit[1]) _ :
-0b0010010000 :
-(bit[1]) _ as instr) =
-  Some(Mtcrf(RS,FXM))
-
-function clause execute (Mtcrf (RS, FXM)) =
-  {
-    mask :=
-      (FXM[0] ^^ 4) :
-        (FXM[1] ^^ 4) :
-          (FXM[2] ^^ 4) :
-            (FXM[3] ^^ 4) : (FXM[4] ^^ 4) : (FXM[5] ^^ 4) : (FXM[6] ^^ 4) : (FXM[7] ^^ 4);
-    CR := ((bit[32]) ((GPR[RS])[32 .. 63] & mask) | (bit[32]) (CR & ~((bit[32]) mask)))
-  }
-
-union ast member (bit[5]) Mfcr
-
-function clause decode (0b011111 :
-(bit[5]) RT :
-0b0 :
-(bit[9]) _ :
-0b0000010011 :
-(bit[1]) _ as instr) =
-  Some(Mfcr(RT))
-
-function clause execute (Mfcr (RT)) = GPR[RT] := 0b00000000000000000000000000000000 : CR
-
-union ast member (bit[5], bit[8]) Mtocrf
-
-function clause decode (0b011111 :
-(bit[5]) RS :
-0b1 :
-(bit[8]) FXM :
-(bit[1]) _ :
-0b0010010000 :
-(bit[1]) _ as instr) =
-  Some(Mtocrf(RS,FXM))
-
-function clause execute (Mtocrf (RS, FXM)) =
-  {
-    ([|7|]) n := 0;
-    count := 0;
-    foreach (i from 0 to 7 by 1 in inc)
-    if FXM[i] == 1
-    then {
-      n := i;
-      count := count + 1
-    }
-    else ();
-    if count == 1
-    then CR[4 * n + 32..4 * n + 35] := (GPR[RS])[4 * n + 32 .. 4 * n + 35]
-    else CR := undefined
-  }
-
-union ast member (bit[5], bit[8]) Mfocrf
-
-function clause decode (0b011111 :
-(bit[5]) RT :
-0b1 :
-(bit[8]) FXM :
-(bit[1]) _ :
-0b0000010011 :
-(bit[1]) _ as instr) =
-  Some(Mfocrf(RT,FXM))
-
-function clause execute (Mfocrf (RT, FXM)) =
-  {
-    ([|7|]) n := 0;
-    count := 0;
-    foreach (i from 0 to 7 by 1 in inc)
-    if FXM[i] == 1
-    then {
-      n := i;
-      count := count + 1
-    }
-    else ();
-    if count == 1
-    then {
-      (bit[64]) temp := undefined;
-      temp[4 * n + 32..4 * n + 35] := CR[4 * n + 32 .. 4 * n + 35];
-      GPR[RT] := temp
-    }
-    else GPR[RT] := undefined
-  }
-
-union ast member (bit[3]) Mcrxr
-
-function clause decode (0b011111 :
-(bit[3]) BF :
-(bit[2]) _ :
-(bit[5]) _ :
-(bit[5]) _ :
-0b1000000000 :
-(bit[1]) _ as instr) =
-  Some(Mcrxr(BF))
-
-function clause execute (Mcrxr (BF)) =
-  {
-    CR[4 * BF + 32..4 * BF + 35] := XER[32 .. 35];
-    XER[32..35] := 0b0000
-  }
-
-union ast member (bit[5], bit[5], bit[5], bit) Dlmzb
-
-function clause decode (0b011111 :
-(bit[5]) RS :
-(bit[5]) RA :
-(bit[5]) RB :
-0b0001001110 :
-[Rc] as instr) =
-  Some(Dlmzb(RS,RA,RB,Rc))
-
-function clause execute (Dlmzb (RS, RA, RB, Rc)) = ()
-
-union ast member (bit[5], bit[5], bit[5], bit, bit) Macchw
-
-function clause decode (0b000100 :
-(bit[5]) RT :
-(bit[5]) RA :
-(bit[5]) RB :
-[OE] :
-0b010101100 :
-[Rc] as instr) =
-  Some(Macchw(RT,RA,RB,OE,Rc))
-
-function clause execute (Macchw (RT, RA, RB, OE, Rc)) = ()
-
-union ast member (bit[5], bit[5], bit[5], bit, bit) Macchws
-
-function clause decode (0b000100 :
-(bit[5]) RT :
-(bit[5]) RA :
-(bit[5]) RB :
-[OE] :
-0b011101100 :
-[Rc] as instr) =
-  Some(Macchws(RT,RA,RB,OE,Rc))
-
-function clause execute (Macchws (RT, RA, RB, OE, Rc)) = ()
-
-union ast member (bit[5], bit[5], bit[5], bit, bit) Macchwu
-
-function clause decode (0b000100 :
-(bit[5]) RT :
-(bit[5]) RA :
-(bit[5]) RB :
-[OE] :
-0b010001100 :
-[Rc] as instr) =
-  Some(Macchwu(RT,RA,RB,OE,Rc))
-
-function clause execute (Macchwu (RT, RA, RB, OE, Rc)) = ()
-
-union ast member (bit[5], bit[5], bit[5], bit, bit) Macchwsu
-
-function clause decode (0b000100 :
-(bit[5]) RT :
-(bit[5]) RA :
-(bit[5]) RB :
-[OE] :
-0b011001100 :
-[Rc] as instr) =
-  Some(Macchwsu(RT,RA,RB,OE,Rc))
-
-function clause execute (Macchwsu (RT, RA, RB, OE, Rc)) = ()
-
-union ast member (bit[5], bit[5], bit[5], bit, bit) Machhw
-
-function clause decode (0b000100 :
-(bit[5]) RT :
-(bit[5]) RA :
-(bit[5]) RB :
-[OE] :
-0b000101100 :
-[Rc] as instr) =
-  Some(Machhw(RT,RA,RB,OE,Rc))
-
-function clause execute (Machhw (RT, RA, RB, OE, Rc)) = ()
-
-union ast member (bit[5], bit[5], bit[5], bit, bit) Machhws
-
-function clause decode (0b000100 :
-(bit[5]) RT :
-(bit[5]) RA :
-(bit[5]) RB :
-[OE] :
-0b001101100 :
-[Rc] as instr) =
-  Some(Machhws(RT,RA,RB,OE,Rc))
-
-function clause execute (Machhws (RT, RA, RB, OE, Rc)) = ()
-
-union ast member (bit[5], bit[5], bit[5], bit, bit) Machhwu
-
-function clause decode (0b000100 :
-(bit[5]) RT :
-(bit[5]) RA :
-(bit[5]) RB :
-[OE] :
-0b000001100 :
-[Rc] as instr) =
-  Some(Machhwu(RT,RA,RB,OE,Rc))
-
-function clause execute (Machhwu (RT, RA, RB, OE, Rc)) = ()
-
-union ast member (bit[5], bit[5], bit[5], bit, bit) Machhwsu
-
-function clause decode (0b000100 :
-(bit[5]) RT :
-(bit[5]) RA :
-(bit[5]) RB :
-[OE] :
-0b001001100 :
-[Rc] as instr) =
-  Some(Machhwsu(RT,RA,RB,OE,Rc))
-
-function clause execute (Machhwsu (RT, RA, RB, OE, Rc)) = ()
-
-union ast member (bit[5], bit[5], bit[5], bit, bit) Maclhw
-
-function clause decode (0b000100 :
-(bit[5]) RT :
-(bit[5]) RA :
-(bit[5]) RB :
-[OE] :
-0b110101100 :
-[Rc] as instr) =
-  Some(Maclhw(RT,RA,RB,OE,Rc))
-
-function clause execute (Maclhw (RT, RA, RB, OE, Rc)) = ()
-
-union ast member (bit[5], bit[5], bit[5], bit, bit) Maclhws
-
-function clause decode (0b000100 :
-(bit[5]) RT :
-(bit[5]) RA :
-(bit[5]) RB :
-[OE] :
-0b111101100 :
-[Rc] as instr) =
-  Some(Maclhws(RT,RA,RB,OE,Rc))
-
-function clause execute (Maclhws (RT, RA, RB, OE, Rc)) = ()
-
-union ast member (bit[5], bit[5], bit[5], bit, bit) Maclhwu
-
-function clause decode (0b000100 :
-(bit[5]) RT :
-(bit[5]) RA :
-(bit[5]) RB :
-[OE] :
-0b110001100 :
-[Rc] as instr) =
-  Some(Maclhwu(RT,RA,RB,OE,Rc))
-
-function clause execute (Maclhwu (RT, RA, RB, OE, Rc)) = ()
-
-union ast member (bit[5], bit[5], bit[5], bit, bit) Maclhwsu
-
-function clause decode (0b000100 :
-(bit[5]) RT :
-(bit[5]) RA :
-(bit[5]) RB :
-[OE] :
-0b111001100 :
-[Rc] as instr) =
-  Some(Maclhwsu(RT,RA,RB,OE,Rc))
-
-function clause execute (Maclhwsu (RT, RA, RB, OE, Rc)) = ()
-
-union ast member (bit[5], bit[5], bit[5], bit) Mulchw
-
-function clause decode (0b000100 :
-(bit[5]) RT :
-(bit[5]) RA :
-(bit[5]) RB :
-0b0010101000 :
-[Rc] as instr) =
-  Some(Mulchw(RT,RA,RB,Rc))
-
-function clause execute (Mulchw (RT, RA, RB, Rc)) = ()
-
-union ast member (bit[5], bit[5], bit[5], bit) Mulchwu
-
-function clause decode (0b000100 :
-(bit[5]) RT :
-(bit[5]) RA :
-(bit[5]) RB :
-0b0010001000 :
-[Rc] as instr) =
-  Some(Mulchwu(RT,RA,RB,Rc))
-
-function clause execute (Mulchwu (RT, RA, RB, Rc)) = ()
-
-union ast member (bit[5], bit[5], bit[5], bit) Mulhhw
-
-function clause decode (0b000100 :
-(bit[5]) RT :
-(bit[5]) RA :
-(bit[5]) RB :
-0b0000101000 :
-[Rc] as instr) =
-  Some(Mulhhw(RT,RA,RB,Rc))
-
-function clause execute (Mulhhw (RT, RA, RB, Rc)) = ()
-
-union ast member (bit[5], bit[5], bit[5], bit) Mulhhwu
-
-function clause decode (0b000100 :
-(bit[5]) RT :
-(bit[5]) RA :
-(bit[5]) RB :
-0b0000001000 :
-[Rc] as instr) =
-  Some(Mulhhwu(RT,RA,RB,Rc))
-
-function clause execute (Mulhhwu (RT, RA, RB, Rc)) = ()
-
-union ast member (bit[5], bit[5], bit[5], bit) Mullhw
-
-function clause decode (0b000100 :
-(bit[5]) RT :
-(bit[5]) RA :
-(bit[5]) RB :
-0b0110101000 :
-[Rc] as instr) =
-  Some(Mullhw(RT,RA,RB,Rc))
-
-function clause execute (Mullhw (RT, RA, RB, Rc)) = ()
-
-union ast member (bit[5], bit[5], bit[5], bit) Mullhwu
-
-function clause decode (0b000100 :
-(bit[5]) RT :
-(bit[5]) RA :
-(bit[5]) RB :
-0b0110001000 :
-[Rc] as instr) =
-  Some(Mullhwu(RT,RA,RB,Rc))
-
-function clause execute (Mullhwu (RT, RA, RB, Rc)) = ()
-
-union ast member (bit[5], bit[5], bit[5], bit, bit) Nmacchw
-
-function clause decode (0b000100 :
-(bit[5]) RT :
-(bit[5]) RA :
-(bit[5]) RB :
-[OE] :
-0b010101110 :
-[Rc] as instr) =
-  Some(Nmacchw(RT,RA,RB,OE,Rc))
-
-function clause execute (Nmacchw (RT, RA, RB, OE, Rc)) = ()
-
-union ast member (bit[5], bit[5], bit[5], bit, bit) Nmacchws
-
-function clause decode (0b000100 :
-(bit[5]) RT :
-(bit[5]) RA :
-(bit[5]) RB :
-[OE] :
-0b011101110 :
-[Rc] as instr) =
-  Some(Nmacchws(RT,RA,RB,OE,Rc))
-
-function clause execute (Nmacchws (RT, RA, RB, OE, Rc)) = ()
-
-union ast member (bit[5], bit[5], bit[5], bit, bit) Nmachhw
-
-function clause decode (0b000100 :
-(bit[5]) RT :
-(bit[5]) RA :
-(bit[5]) RB :
-[OE] :
-0b000101110 :
-[Rc] as instr) =
-  Some(Nmachhw(RT,RA,RB,OE,Rc))
-
-function clause execute (Nmachhw (RT, RA, RB, OE, Rc)) = ()
-
-union ast member (bit[5], bit[5], bit[5], bit, bit) Nmachhws
-
-function clause decode (0b000100 :
-(bit[5]) RT :
-(bit[5]) RA :
-(bit[5]) RB :
-[OE] :
-0b001101110 :
-[Rc] as instr) =
-  Some(Nmachhws(RT,RA,RB,OE,Rc))
-
-function clause execute (Nmachhws (RT, RA, RB, OE, Rc)) = ()
-
-union ast member (bit[5], bit[5], bit[5], bit, bit) Nmaclhw
-
-function clause decode (0b000100 :
-(bit[5]) RT :
-(bit[5]) RA :
-(bit[5]) RB :
-[OE] :
-0b110101110 :
-[Rc] as instr) =
-  Some(Nmaclhw(RT,RA,RB,OE,Rc))
-
-function clause execute (Nmaclhw (RT, RA, RB, OE, Rc)) = ()
-
-union ast member (bit[5], bit[5], bit[5], bit, bit) Nmaclhws
-
-function clause decode (0b000100 :
-(bit[5]) RT :
-(bit[5]) RA :
-(bit[5]) RB :
-[OE] :
-0b111101110 :
-[Rc] as instr) =
-  Some(Nmaclhws(RT,RA,RB,OE,Rc))
-
-function clause execute (Nmaclhws (RT, RA, RB, OE, Rc)) = ()
-
-union ast member (bit[5], bit[5]) Icbi
-
-function clause decode (0b011111 :
-(bit[5]) _ :
-(bit[5]) RA :
-(bit[5]) RB :
-0b1111010110 :
-(bit[1]) _ as instr) =
-  Some(Icbi(RA,RB))
-
-function clause execute (Icbi (RA, RB)) = ()
-
-union ast member (bit[4], bit[5], bit[5]) Icbt
-
-function clause decode (0b011111 :
-(bit[1]) _ :
-(bit[4]) CT :
-(bit[5]) RA :
-(bit[5]) RB :
-0b0000010110 :
-(bit[1]) _ as instr) =
-  Some(Icbt(CT,RA,RB))
-
-function clause execute (Icbt (CT, RA, RB)) = ()
-
-union ast member (bit[5], bit[5]) Dcba
-
-function clause decode (0b011111 :
-(bit[5]) _ :
-(bit[5]) RA :
-(bit[5]) RB :
-0b1011110110 :
-(bit[1]) _ as instr) =
-  Some(Dcba(RA,RB))
-
-function clause execute (Dcba (RA, RB)) = ()
-
-union ast member (bit[5], bit[5], bit[5]) Dcbt
-
-function clause decode (0b011111 :
-(bit[5]) TH :
-(bit[5]) RA :
-(bit[5]) RB :
-0b0100010110 :
-(bit[1]) _ as instr) =
-  Some(Dcbt(TH,RA,RB))
-
-function clause execute (Dcbt (TH, RA, RB)) = ()
-
-union ast member (bit[5], bit[5], bit[5]) Dcbtst
-
-function clause decode (0b011111 :
-(bit[5]) TH :
-(bit[5]) RA :
-(bit[5]) RB :
-0b0011110110 :
-(bit[1]) _ as instr) =
-  Some(Dcbtst(TH,RA,RB))
-
-function clause execute (Dcbtst (TH, RA, RB)) = ()
-
-union ast member (bit[5], bit[5]) Dcbz
-
-function clause decode (0b011111 :
-(bit[5]) _ :
-(bit[5]) RA :
-(bit[5]) RB :
-0b1111110110 :
-(bit[1]) _ as instr) =
-  Some(Dcbz(RA,RB))
-
-function clause execute (Dcbz (RA, RB)) = ()
-
-union ast member (bit[5], bit[5]) Dcbst
-
-function clause decode (0b011111 :
-(bit[5]) _ :
-(bit[5]) RA :
-(bit[5]) RB :
-0b0000110110 :
-(bit[1]) _ as instr) =
-  Some(Dcbst(RA,RB))
-
-function clause execute (Dcbst (RA, RB)) = ()
-
-union ast member (bit[2], bit[5], bit[5]) Dcbf
-
-function clause decode (0b011111 :
-(bit[3]) _ :
-(bit[2]) L :
-(bit[5]) RA :
-(bit[5]) RB :
-0b0001010110 :
-(bit[1]) _ as instr) =
-  Some(Dcbf(L,RA,RB))
-
-function clause execute (Dcbf (L, RA, RB)) = ()
-
-union ast member Isync
-
-function clause decode (0b010011 :
-(bit[5]) _ :
-(bit[5]) _ :
-(bit[5]) _ :
-0b0010010110 :
-(bit[1]) _ as instr) =
-  Some(Isync())
-
-function clause execute Isync = I_Sync(())
-
-union ast member (bit[5], bit[5], bit[5], bit) Lbarx
-
-function clause decode (0b011111 :
-(bit[5]) RT :
-(bit[5]) RA :
-(bit[5]) RB :
-0b0000110100 :
-[EH] as instr) =
-  Some(Lbarx(RT,RA,RB,EH))
-
-function clause execute (Lbarx (RT, RA, RB, EH)) =
-  {
-    (bit[64]) b := 0;
-    (bit[64]) EA := 0;
-    if RA == 0 then b := 0 else b := GPR[RA];
-    EA := b + GPR[RB];
-    GPR[RT] := 0b00000000000000000000000000000000000000000000000000000000 : MEMr_reserve(EA,1)
-  }
-
-union ast member (bit[5], bit[5], bit[5], bit) Lharx
-
-function clause decode (0b011111 :
-(bit[5]) RT :
-(bit[5]) RA :
-(bit[5]) RB :
-0b0001110100 :
-[EH] as instr) =
-  Some(Lharx(RT,RA,RB,EH))
-
-function clause execute (Lharx (RT, RA, RB, EH)) =
-  {
-    (bit[64]) b := 0;
-    (bit[64]) EA := 0;
-    if RA == 0 then b := 0 else b := GPR[RA];
-    EA := b + GPR[RB];
-    GPR[RT] := 0b000000000000000000000000000000000000000000000000 : MEMr_reserve(EA,2)
-  }
-
-union ast member (bit[5], bit[5], bit[5], bit) Lwarx
-
-function clause decode (0b011111 :
-(bit[5]) RT :
-(bit[5]) RA :
-(bit[5]) RB :
-0b0000010100 :
-[EH] as instr) =
-  Some(Lwarx(RT,RA,RB,EH))
-
-function clause execute (Lwarx (RT, RA, RB, EH)) =
-  {
-    (bit[64]) b := 0;
-    (bit[64]) EA := 0;
-    if RA == 0 then b := 0 else b := GPR[RA];
-    EA := b + GPR[RB];
-    GPR[RT] := 0b00000000000000000000000000000000 : MEMr_reserve(EA,4)
-  }
-
-union ast member (bit[5], bit[5], bit[5]) Stbcx
-
-function clause decode (0b011111 :
-(bit[5]) RS :
-(bit[5]) RA :
-(bit[5]) RB :
-0b1010110110 :
-0b1 as instr) =
-  Some(Stbcx(RS,RA,RB))
-
-function clause execute (Stbcx (RS, RA, RB)) =
-  {
-    (bit[64]) b := 0;
-    (bit[64]) EA := 0;
-    if RA == 0 then b := 0 else b := GPR[RA];
-    EA := b + GPR[RB];
-    MEMw_EA_cond(EA,1);
-    status := MEMw_conditional(EA,1,(GPR[RS])[56 .. 63]);
-    CR0 := 0b00 : [status] : [XER.SO]
-  }
-
-union ast member (bit[5], bit[5], bit[5]) Sthcx
-
-function clause decode (0b011111 :
-(bit[5]) RS :
-(bit[5]) RA :
-(bit[5]) RB :
-0b1011010110 :
-0b1 as instr) =
-  Some(Sthcx(RS,RA,RB))
-
-function clause execute (Sthcx (RS, RA, RB)) =
-  {
-    (bit[64]) b := 0;
-    (bit[64]) EA := 0;
-    if RA == 0 then b := 0 else b := GPR[RA];
-    EA := b + GPR[RB];
-    MEMw_EA_cond(EA,2);
-    status := MEMw_conditional(EA,2,(GPR[RS])[48 .. 63]);
-    CR0 := 0b00 : [status] : [XER.SO]
-  }
-
-union ast member (bit[5], bit[5], bit[5]) Stwcx
-
-function clause decode (0b011111 :
-(bit[5]) RS :
-(bit[5]) RA :
-(bit[5]) RB :
-0b0010010110 :
-0b1 as instr) =
-  Some(Stwcx(RS,RA,RB))
-
-function clause execute (Stwcx (RS, RA, RB)) =
-  {
-    (bit[64]) b := 0;
-    (bit[64]) EA := 0;
-    if RA == 0 then b := 0 else b := GPR[RA];
-    EA := b + GPR[RB];
-    MEMw_EA_cond(EA,4);
-    status := MEMw_conditional(EA,4,(GPR[RS])[32 .. 63]);
-    CR0 := 0b00 : [status] : [XER.SO]
-  }
-
-union ast member (bit[5], bit[5], bit[5], bit) Ldarx
-
-function clause decode (0b011111 :
-(bit[5]) RT :
-(bit[5]) RA :
-(bit[5]) RB :
-0b0001010100 :
-[EH] as instr) =
-  Some(Ldarx(RT,RA,RB,EH))
-
-function clause execute (Ldarx (RT, RA, RB, EH)) =
-  {
-    (bit[64]) b := 0;
-    (bit[64]) EA := 0;
-    if RA == 0 then b := 0 else b := GPR[RA];
-    EA := b + GPR[RB];
-    GPR[RT] := MEMr_reserve(EA,8)
-  }
-
-union ast member (bit[5], bit[5], bit[5]) Stdcx
-
-function clause decode (0b011111 :
-(bit[5]) RS :
-(bit[5]) RA :
-(bit[5]) RB :
-0b0011010110 :
-0b1 as instr) =
-  Some(Stdcx(RS,RA,RB))
-
-function clause execute (Stdcx (RS, RA, RB)) =
-  {
-    (bit[64]) b := 0;
-    (bit[64]) EA := 0;
-    if RA == 0 then b := 0 else b := GPR[RA];
-    EA := b + GPR[RB];
-    MEMw_EA_cond(EA,8);
-    status := MEMw_conditional(EA,8,GPR[RS]);
-    CR0 := 0b00 : [status] : [XER.SO]
-  }
-
-union ast member (bit[2]) Sync
-
-function clause decode (0b011111 :
-(bit[3]) _ :
-(bit[2]) L :
-(bit[5]) _ :
-(bit[5]) _ :
-0b1001010110 :
-(bit[1]) _ as instr) =
-  Some(Sync(L))
-
-function clause execute (Sync (L)) =
-  switch L { case 0b00 -> { H_Sync(()) } case 0b01 -> { LW_Sync(()) } }
-
-union ast member Eieio
-
-function clause decode (0b011111 :
-(bit[5]) _ :
-(bit[5]) _ :
-(bit[5]) _ :
-0b1101010110 :
-(bit[1]) _ as instr) =
-  Some(Eieio())
-
-function clause execute Eieio = EIEIO_Sync(())
-
-union ast member (bit[5]) Mbar
-
-function clause decode (0b011111 :
-(bit[5]) MO :
-(bit[5]) _ :
-(bit[5]) _ :
-0b1101010110 :
-(bit[1]) _ as instr) =
-  Some(Mbar(MO))
-
-function clause execute (Mbar (MO)) = ()
-
-union ast member (bit[2]) Wait
-
-function clause decode (0b011111 :
-(bit[3]) _ :
-(bit[2]) WC :
-(bit[5]) _ :
-(bit[5]) _ :
-0b0000111110 :
-(bit[1]) _ as instr) =
-  Some(Wait(WC))
-
-function clause execute (Wait (WC)) = ()
-
-
-typedef decode_failure = enumerate { no_matching_pattern; unsupported_instruction; illegal_instruction } 
-
-function clause decode _ = None
-
-end decode
-end execute
-end ast
-
-val ast -> option<ast> effect pure supported_instructions
-function option<ast> supported_instructions ((ast) instr) = {
-  switch instr {
-    case (Mbar(_)) -> None
-    case (Sync(0b10)) -> None
-    case (Sync(0b11)) -> None
-    case _ -> Some(instr)
-   }
-}
-
-val ast -> bit effect pure illegal_instructions_pred
-function bit illegal_instructions_pred ((ast) instr) = {
-     switch instr {
-        case (Bcctr(BO,BI,BH,LK)) -> ~(BO[2])
-        case (Lbzu(RT,RA,D)) -> (RA == 0) | (RA == RT) 
-        case (Lbzux(RT,RA,_)) ->(RA == 0) | (RA == RT) 
-        case (Lhzu(RT,RA,D)) -> (RA == 0) | (RA == RT)
-        case (Lhzux(RT,RA,RB)) -> (RA == 0) | (RA == RT)
-        case (Lhau(RT,RA,D)) -> (RA == 0) | (RA == RT)
-        case (Lhaux(RT,RA,RB)) -> (RA == 0) | (RA == RT)
-        case (Lwzu(RA,RT,D)) -> (RA == 0) | (RA == RT)
-        case (Lwzux(RT,RA,RB)) -> (RA == 0) | (RA == RT)
-        case (Lwaux(RA,RT,RB)) -> (RA == 0) | (RA == RT)
-        case (Ldu(RT,RA,DS)) -> (RA == 0) | (RA == RT)
-        case (Ldux(RT,RA,RB)) -> (RA == 0) | (RA == RT)
-        case (Stbu(RS,RA,D)) -> (RA == 0)
-        case (Stbux(RS,RA,RB)) -> (RA == 0)
-        case (Sthu(RS,RA,RB)) -> (RA == 0)
-        case (Sthux(RS,RA,RB)) -> (RA == 0)
-        case (Stwu(RS,RA,D)) -> (RA == 0)
-        case (Stwux(RS,RA,RB)) -> (RA == 0)
-        case (Stdu(RS,RA,DS)) -> (RA == 0)
-        case (Stdux(RS,RA,RB)) -> (RA == 0)
-        case (Lmw(RT,RA,D)) -> (RA == 0) | ((RT <= RA) & (RA <= 31))
-        case (Lswi(RT,RA,NB)) ->
-           let (([|32|]) n) = (if ~(NB == 0) then NB else 32) in
-           let ceil =
-             (if (n mod 4) == 0
-             then n quot 4 else (n quot 4) + 1) in
-           (RT <= RA) & (RA <= ((bit[5]) (((bit[5]) (RT + ceil)) - 1)))
-        (* Can't read XER at the time meant, so will need to rethink *)
-       (* case (Lswx(RT,RA,RB)) ->
-           let (([|32|]) n) = (XER[57..63]) in
-           let ceil =
-             (if (n mod 4 == 0)
-             then n quot 4 else (n quot 4) + 1) in
-           let ((bit[5]) upper_bound) = (RT + ceil) in
-           (RT <= RA & RA <= upper_bound) |
-           (RT <= RB & RB <= upper_bound) |
-          (RT == RA) | (RT == RB)*)
-(*Floating point instructions*)
-(*        case (Lfsu(FRT,RA,D)) -> (RA == 0)
-        case (Lfsux(FRT,RA,RB)) -> (RA == 0)
-        case (Lfdu(FRT,RA,D)) -> (RA == 0)
-        case (Lfdux(FRT,RA,RB)) -> (RA == 0)
-        case (Stfsu(FRS,RA,D)) -> (RA == 0)
-        case (Stfsux(FRS,RA,RB)) -> (RA == 0)
-        case (Stfdu(FRS,D,RA)) -> (RA == 0)
-        case (Stfdux(FRS,RA,RB)) -> (RA == 0)
-        case (Lfdp(FRTp,RA,DS)) -> (FRTp mod 2 == 1)
-        case (Stfdp(FRSp,RA,DS)) -> (FRSp mod 2 == 1)
-        case (Lfdpx(FRTp,RA,RB)) -> (FRTp mod 2 == 1)
-        case (Stfdpx(FRSp,RA,RB)) -> (FRSp mod 2 == 1)*)
-        case (Lq(RTp,RA,DQ,Pt)) -> ((RTp mod 2 ==1) | RTp == RA)
-        case (Stq(RSp,RA,RS)) -> (RSp mod 2 == 1)
-        case (Mtspr(RS, spr)) ->
-          ~ ((spr == 1) | (spr == 8) | (spr == 9) | (spr == 256) |
-            (spr == 512) | (spr == 896) | (spr == 898))
-(*One of these causes a stack overflow error, don't want to debug why now*)
-        (*case (Mfspr(RT, spr)) ->
-           ~ ((spr == 1) | (spr == 8) | (spr == 9) | (spr == 136) |
-           (spr == 256) | (spr == 259) | (spr == 260) | (spr == 261) |
-           (spr == 262) | (spr == 263) | (spr == 268) | (spr == 268) |
-           (spr == 269) | (spr == 512) | (spr == 526) | (spr == 526) |
-           (spr == 527) | (spr == 896) | (spr == 898))
-        case (Se_illegal) -> true
-        case (E_lhau(RT,RA,D8)) -> (RA == 0 | RA == RT)
-        case (E_Lhzu(RT,RA,D8)) -> (RA == 0 | RA == RT)
-        case (E_lwzu(RT,RA,D8)) -> (RA == 0 | RA == RT)
-        case (E_stbu(RS,RA,D8)) -> (RA == 0)
-        case (E_sthu(RS,RA,D8)) -> (RA == 0)
-        case (E_stwu(RS,RA,D8)) -> (RA == 0)
-        case (E_lmw(RT,RA,D8)) -> (RT <= RA & RA <= 31)*)
-        case _ -> false
-     }
-}
-
-val ast -> option<ast> effect pure illegal_instructions
-function option<ast> illegal_instructions instr =
-  if (illegal_instructions_pred (instr))
-  then None else Some(instr)
-
-(* old fetch-decode-execute *)
-(*function unit fde () = {
-  NIA := CIA + 4;
-  instr := decode(MEMr(CIA, 4));
-  instr := supported_instructions(instr);
-  execute(instr);
-  CIA := NIA;
-}*)
diff --git a/src/test/regbits.sail b/src/test/regbits.sail
deleted file mode 100644
index 469f0f79..00000000
--- a/src/test/regbits.sail
+++ /dev/null
@@ -1,30 +0,0 @@
- typedef xer = register bits [ 0 : 63 ] {
-  32 : SO;
-  33 : OV;
-  34 : CA;
-  35..36: FOOBAR;
- }
-
-register (xer) XER
-register (bit) query
-
-register alias CA = XER.CA
-register alias Fo = XER[35]
-register alias foobar = XER[35..36]
-register alias doub = XER:XER
-
-function (bit[64]) main _ = {
-  XER := 0b0101010101010101010101010101010101010101010101010101010101010010;
-  f := XER;
-  (bit[7]) foo := XER[57..63];
-  query := XER.SO;
-  XER.SO := 0;
-  query := CA;
-  query := Fo;
-  CA := query;
-  XER.FOOBAR := 0b11;
-  XER.FOOBAR := foobar;
-  query := doub[13];
-  doub := XER:XER;
-  XER }
-
diff --git a/src/test/run_power.ml b/src/test/run_power.ml
deleted file mode 100644
index 2ba7ee2b..00000000
--- a/src/test/run_power.ml
+++ /dev/null
@@ -1,333 +0,0 @@
-open Printf ;;
-open Big_int ;;
-open Interp_ast ;;
-open Interp_interface ;;
-open Interp_inter_imp ;;
-open Run_interp_model ;;
-
-open Sail_interface ;;
-
-let startaddr = ref [] ;;
-let mainaddr  = ref "0" ;;
-let sections = ref [] ;;
-let file = ref "" ;;
-let print_bytes = ref false ;;
-let bytes_file = ref "bytes_out.lem";;
-let test_format = ref false ;;
-let test_file = ref "test.txt";;
-let test_memory_addr = ref (0,[]) ;;
-
-let rec foldli f acc ?(i=0) = function
-  | [] -> acc
-  | x::xs -> foldli f (f i acc x) ~i:(i+1) xs
-;;
-
-let big_endian = true ;;
-
-let hex_to_big_int s = big_int_of_int64 (Int64.of_string s) ;;
-
-let big_int_to_vec for_mem b size =
-  fst (extern_value
-	 (make_mode true false)
-	 for_mem
-	 None
-	 ((if big_endian then Interp_lib.to_vec_inc else Interp_lib.to_vec_dec)
-	     (Interp.V_tuple [(Interp.V_lit (L_aux (L_num size, Unknown))); 
-			      (Interp.V_lit (L_aux (L_num b, Unknown)))])))
-;;
-
-let mem = ref Mem.empty ;;
-let reg = ref (Reg.add "dummy" Unknown0 Reg.empty) ;;
-
-let add_mem byte addr =
-  assert(byte >= 0 && byte < 256);
-  (*Printf.printf "adder is %s, byte is %s\n" (string_of_big_int addr) (string_of_int byte);*)
-  let addr = big_int_to_vec true addr (big_int_of_int 64) in
-  (*Printf.printf "adder is %s byte is %s\n" (Printing_functions.val_to_string addr) (string_of_int byte);*)
-  match addr with
-    | Bytevector addr -> (*List.iter (fun i -> Printf.printf "%i " i) addr; Printf.printf "\n";*)
-      mem := Mem.add addr byte !mem
-;;
-
-let add_section s =
-  match Str.split (Str.regexp ",") s with
-  | [name;offset;size;addr] ->
-      begin try
-        sections := (
-          int_of_string offset,
-          int_of_string size,
-          hex_to_big_int addr) ::
-            !sections
-      with Failure msg -> raise (Arg.Bad (msg ^ ": " ^ s))
-      end
-  | _ -> raise (Arg.Bad ("Wrong section format: "^s))
-;;
-
-let load_section ic (offset,size,addr) =
-  seek_in ic offset;
-  for i = 0 to size - 1 do
-    add_mem (input_byte ic) (add_int_big_int i addr);
-  done
-;;
-
-let load_memory (bits,addr) =
-  let rec loop bits addr = 
-    if (Bitstring.bitstring_length bits = 0)
-    then ()
-    else let (Error.Success(bitsnum,rest)) = Ml_bindings.read_unsigned_char Endianness.default_endianness bits in
-	 add_mem (Uint32.to_int bitsnum) (big_int_of_int addr);
-	 loop rest (1 + addr)
-  in loop bits addr
-
-let rec read_mem mem loc length = 
-  if length = 0  
-  then []
-  else 
-    let location = big_int_to_vec true loc (big_int_of_int 64) in
-    match location with
-      | Bytevector location ->
-	(Mem.find location mem)::(read_mem mem (add_big_int loc unit_big_int) (length - 1))
-
-let get_reg reg name =
-  let reg_content = Reg.find name reg in reg_content
-
-(* use zero as a sentinel --- it might prevent a minimal loop from
- * working in principle, but won't happen in practice *)
-let lr_init_value = zero_big_int
-
-let init_reg () =
-  let init name value size =
-    (* fix index - this is necessary for CR, indexed from 32 *)
-    let offset = function
-      | Bitvector(bits,inc,fst) ->
-        Bitvector(bits,inc,big_int_of_int (64 - size))
-     | _ -> assert false in
-    name, offset (big_int_to_vec false value (big_int_of_int size)) in
-  List.fold_left (fun r (k,v) -> Reg.add k v r) Reg.empty (
-    (* Special registers *)
-    [
-      init "CR" zero_big_int 32;
-      init "CTR" zero_big_int 64;
-      init "LR" lr_init_value 64;
-      init "XER" zero_big_int 64;
-      init "VRSAVE" zero_big_int 32;
-      init "FPSCR" zero_big_int 64;
-      init "VSCR" zero_big_int 32;
-      init "SPRG4" zero_big_int 64;
-      init "SPRG5" zero_big_int 64;
-      init "SPRG6" zero_big_int 64;
-      init "SPRG7" zero_big_int 64;
-    ] @
-    (* Commonly read before written general purpose register *)
-      [init "GPR0" zero_big_int 64;
-       init "GPR1" zero_big_int 64;
-       init "GPR2" zero_big_int 64;
-       init "GPR3" zero_big_int 64;
-       init "GPR31" zero_big_int 64;]
-      (*Conditionally include all general purpose registers *)
-    @ (if !test_format
-      then [ 
-	init "GPR4" zero_big_int 64;
-	init "GPR5" zero_big_int 64;
-	init "GPR6" zero_big_int 64;
-	init "GPR7" zero_big_int 64;
-	init "GPR8" zero_big_int 64;
-	init "GPR9" zero_big_int 64;
-	init "GPR10" zero_big_int 64;
-	init "GPR11" zero_big_int 64;
-	init "GPR12" zero_big_int 64;
-	init "GPR13" zero_big_int 64;
-	init "GPR14" zero_big_int 64;
-	init "GPR15" zero_big_int 64;
-	init "GPR16" zero_big_int 64;
-	init "GPR17" zero_big_int 64;
-	init "GPR18" zero_big_int 64;
-	init "GPR19" zero_big_int 64;
-	init "GPR20" zero_big_int 64;
-	init "GPR21" zero_big_int 64;
-	init "GPR22" zero_big_int 64;
-	init "GPR23" zero_big_int 64;
-	init "GPR24" zero_big_int 64;
-	init "GPR25" zero_big_int 64;
-	init "GPR26" zero_big_int 64;
-	init "GPR27" zero_big_int 64;
-	init "GPR28" zero_big_int 64;
-	init "GPR29" zero_big_int 64;
-	init "GPR30" zero_big_int 64;]
-      else [])
-      @
-      (if !test_format
-       then [
-	 init "VR0" zero_big_int 128;
-	 init "VR1" zero_big_int 128;
-	 init "VR2" zero_big_int 128;
-	 init "VR3" zero_big_int 128;
-	 init "VR4" zero_big_int 128;
-	 init "VR5" zero_big_int 128;
-	 init "VR6" zero_big_int 128;
-	 init "VR7" zero_big_int 128;
-	 init "VR8" zero_big_int 128;
-	 init "VR9" zero_big_int 128;
-	 init "VR10" zero_big_int 128;
-	 init "VR11" zero_big_int 128;
-	 init "VR12" zero_big_int 128;
-	 init "VR13" zero_big_int 128;
-	 init "VR14" zero_big_int 128;
-	 init "VR15" zero_big_int 128;
-	 init "VR16" zero_big_int 128;
-	 init "VR17" zero_big_int 128;
-	 init "VR18" zero_big_int 128;
-	 init "VR19" zero_big_int 128;
-	 init "VR20" zero_big_int 128;
-	 init "VR21" zero_big_int 128;
-	 init "VR22" zero_big_int 128;
-	 init "VR23" zero_big_int 128;
-	 init "VR24" zero_big_int 128;
-	 init "VR25" zero_big_int 128;
-	 init "VR26" zero_big_int 128;
-	 init "VR27" zero_big_int 128;
-	 init "VR28" zero_big_int 128;
-	 init "VR29" zero_big_int 128;
-	 init "VR30" zero_big_int 128;
-    	 init "VR31" zero_big_int 128;]
-       else [])
-      @
-      (*Not really registers*)
-     [(* Currint Instruciton Address, manually set *)
-       init "CIA" (hex_to_big_int !mainaddr) 64;
-       init "NIA" zero_big_int 64;
-       "mode64bit", Bitvector([true],true,zero_big_int);
-     ])
-;;
-
-let lem_print_memory m =
-  let format_addr a = "[" ^ (List.fold_right (fun i r -> "(" ^ (string_of_int i) ^ ": word8);" ^ r) a "") ^ "]" in
-  let preamble = "open import Pervasives\ntype word8 = nat\n" in
-  let start_addr = "let start_adder_address = " ^ format_addr !startaddr ^ ";;\n" in
-  let start_list_def = "let instruction_byte_list = [" in
-  let list_elements = 
-    Mem.fold (fun key byte rest -> 
-      rest ^ "(" ^ (format_addr key) ^ ", (" ^ (string_of_int byte) ^ ":word8) );\n") m "" in
-  let close_list_def = "];;" in
-  let (temp_file_name, o) = Filename.open_temp_file "ll_temp" "" in
-  let o' = Format.formatter_of_out_channel o in
-  Format.fprintf o' "%s" (preamble ^ start_addr ^ start_list_def ^ list_elements ^ close_list_def);
-  let _ = close_out o in
-  Sys.rename temp_file_name !bytes_file 
-
-let print_test_results final_reg final_mem = 
-  let tilde = String.make 90 '~' in
-  let preamble = "\t\t"^"Value before test" ^ "\t\t\t" ^ "Value after test\n" ^ tilde ^ "\n" in
-  let format_register reg_name = 
-    let original_reg = get_reg !reg reg_name in
-    let final_reg = get_reg final_reg reg_name in
-    reg_name ^ ";\t\t" ^ Printing_functions.val_to_hex_string original_reg ^ ";\t\t\t" ^ Printing_functions.val_to_hex_string final_reg ^ "\n"
-  in
-  let rec numbered_reg base_name curr_index stop_index =
-    if curr_index > stop_index
-    then ""
-    else (format_register (base_name ^ (string_of_int curr_index))) ^ (numbered_reg base_name (curr_index +1) stop_index)
-  in
-  let special_reg = List.fold_right (fun r rs -> (format_register r) ^ rs) ["CR";"CTR";"LR";"XER"] "" in
-  let gpr_reg = numbered_reg "GPR" 0 31 in
-  let vr_reg = numbered_reg "VR" 0 31 in
-  let reg_contents = special_reg ^ gpr_reg ^ (format_register "VRSAVE") ^ vr_reg ^ (format_register "VSCR") in
-  let rec memory_crawl curr_index curr_address = 
-    if curr_index >= 100
-    then ""
-    else let mem_orig = Bytevector(read_mem !mem curr_address 8) in
-	 let mem_end = Bytevector(read_mem final_mem curr_address 8) in
-	"MEM_" ^ (string_of_int curr_index) ^ ";\t\t" ^ Printing_functions.val_to_hex_string mem_orig ^ 
-	  ";\t\t\t" ^ Printing_functions.val_to_hex_string mem_end ^ "\n" ^ 
-	  (memory_crawl (curr_index + 1) (add_big_int curr_address unit_big_int))
-  in
-  let mem_contents = memory_crawl 0 (big_int_of_int (fst (!test_memory_addr))) in
-  let footer = tilde ^ "\n" in
-  let (temp_file_name, o) = Filename.open_temp_file "tt_temp" "" in
-  let o' = Format.formatter_of_out_channel o in
-  Format.fprintf o' "%s" (preamble ^ reg_contents ^footer ^ mem_contents);
-  let _ = close_out o in
-  Sys.rename temp_file_name !test_file
-
-let eager_eval = ref true
-
-let args = [
-  ("--file", Arg.Set_string file, "filename binary code to load in memory");
-  ("--data", Arg.String add_section, "name,offset,size,addr add a data section");
-  ("--code", Arg.String add_section, "name,offset,size,addr add a code section");
-  ("--mainaddr", Arg.Set_string mainaddr, "addr address of the main section (entry point; default: 0)");
-  ("--quiet", Arg.Clear Run_interp_model.debug, "do not display interpreter actions");
-  ("--interactive", Arg.Clear eager_eval , "interactive execution");
-  ("--test", Arg.Set test_format , "format output for single instruction tests, save in file");
-  ("--test_file", Arg.Set_string test_file , "specify the name for a file generated by --test");
-  ("--dump", Arg.Set print_bytes , "do not run, just generate a lem file of a list of bytes");
-  ("--dump_file", Arg.Set_string bytes_file, "specify the name for a file generated by --dump");
-] ;;
-
-let time_it action arg =
-  let start_time = Sys.time () in
-  ignore (action arg);
-  let finish_time = Sys.time () in
-  finish_time -. start_time
-;;
-
-let eq_zero = function
-  | Bitvector(bools,_,_) -> List.for_all (not) bools
-;;
-
-let rec fde_loop count main_func parameters mem reg ?mode track_dependencies prog =
-  debugf "\n**** instruction %d  ****\n" count;
-  match Run_interp_model.run ~main_func ~parameters ~mem ~reg ~eager_eval:!eager_eval ~track_dependencies:(ref track_dependencies) ?mode prog with
-  | false, _,_, _ -> eprintf "FAILURE\n"; exit 1
-  | true, mode, track_dependencies, (my_reg, my_mem) ->
-      if eq_zero (get_reg my_reg "CIA") then
-        (if not(!test_format) 
-	 then eprintf "\nSUCCESS: returned with value %s\n"
-          (Printing_functions.val_to_string (get_reg my_reg "GPR3"))
-	 else print_test_results my_reg my_mem)	    
-      else
-        fde_loop (count+1) main_func parameters my_mem my_reg ~mode:mode track_dependencies prog
-;;
-
-let run () =
-  Arg.parse args (fun _ -> raise (Arg.Bad "anonymous parameter")) "" ;
-  if !file = "" then begin
-    Arg.usage args "";
-    exit 1;
-  end;
-  if !eager_eval then Run_interp_model.debug := true;
-  if !test_format then Run_interp_model.debug := false;
-  let (((locations,start_address),_),(symbol_map)) = populate_and_obtain_symbol_to_address_mapping !file in
-  let total_size = (List.length locations) in
-  if not(!test_format)
-  then eprintf "Loading binary into memory (%d sections)... %!" total_size;
-  let t = time_it (List.iter load_memory) locations in
-  if not(!test_format)
-  then eprintf "done. (%f seconds)\n%!" t;
-  let addr = read_mem !mem (big_int_of_int start_address) 8 in
-  let _ = begin
-    startaddr := addr;
-    mainaddr := "0x" ^ (List.fold_left (^) "" (List.map (Printf.sprintf "%02x") addr));
-  end in
-  if not(!test_format) then
-    Printf.printf "start address: %s\n" !mainaddr;
-  let my_reg = init_reg () in
-  reg := my_reg;
-  if !test_format 
-  then if List.mem_assoc "TEST_MEM" symbol_map
-    then test_memory_addr := 
-      let num = (List.assoc "TEST_MEM" symbol_map) in
-      match big_int_to_vec true (big_int_of_int num) (big_int_of_int 64) with
-	| Bytevector location -> (num,location);
-    else ();
-  (* entry point: unit -> unit fde *)
-  let funk_name = "fde" in
-  let parms = [] in
-  let name = Filename.basename !file in
-  if !print_bytes 
-  then lem_print_memory !mem
-  else let t =time_it (fun () -> fde_loop 0 funk_name parms !mem !reg false (name, Power.defs)) () in
-       if not(!test_format) then eprintf "Execution time: %f seconds\n" t
-;;
-
-run () ;;
diff --git a/src/test/run_tests.ml b/src/test/run_tests.ml
deleted file mode 100644
index 770ed426..00000000
--- a/src/test/run_tests.ml
+++ /dev/null
@@ -1,29 +0,0 @@
-open Printf
-
-let tests = [
-  "test1", Test1.defs;
-  "test2", Test2.defs;
-  "test3", Test3.defs;
-  "test4", Test4.defs;
-  "pattern", Pattern.defs;
-  "vectors", Vectors.defs;
-  "regbits", Regbits.defs;
-  (*"power", Power.defs;*)
-] ;;
-
-let fst3 (x,_,_) = x
-
-let run_one ((name, _) as t) = (name, fst3(Run_interp.run t))
-
-let run_all () =
-  let results = List.map run_one tests in
-  if List.for_all (fun (_, r) -> r) results then
-    eprintf "\nSUCCESS: all tests passed!\n"
-  else begin
-    eprintf "\nFAILURE: the following tests failed:\n";
-    List.iter (fun (name, r) -> if not r then eprintf "- %s\n" name) results;
-    exit 1
-  end
-;;
-
-run_all () ;;
diff --git a/src/test/test1.sail b/src/test/test1.sail
deleted file mode 100644
index 0c08324c..00000000
--- a/src/test/test1.sail
+++ /dev/null
@@ -1,51 +0,0 @@
-default Order inc
-default Nat 'i
-default Order 'o
-default bool b
-default forall 'a. list<'a> b
-val forall 'a, 'b . ('a, 'b) -> 'b effect pure snd
-val forall Type 'i, 'b. ('i, 'b) -> 'i effect pure fst
-typedef int_list [name = "il"] = list<nat>
-typedef reco = const struct forall 'i, 'a, 'b. { 'a['i] v; 'b w; }
-typedef maybe = const union forall 'a. { Nne; 'a Sme; }
-typedef creg = register bits [5:10] { 5 : h ; 6..7 : j}
-let (bool) e = true
-val forall Nat 'a, Nat 'b. bit['a:'b] sliced
-let (bit) v = bitzero
-let ( bit [ 3 ] ) v1 = 0b101
-
-let ( bit [32] ) v2 = 0xABCDEF01
-
-val forall Type 'a. 'a -> 'a effect pure identity
-function forall Type 'a. 'a identity i = i
-
-(*function unit ignore(x) = ()*)
-
-(* scattered function definition and union definition *)
-scattered typedef ast = const union
-scattered function ast f
-
-union ast member  (bit, bit, bit) A
-function clause f (  A (a,b,c) ) = C(a)
-
-union ast member  (bit, bit) B
-function clause f (  B (a,b) ) = C(a)
-
-union ast member  bit C
-function clause f (  C (a) ) = C(a)
-
-end ast
-end f
-
-function unit a (bit) b = if identity(b) then (identity()) else ()
-
-function bit sw s = switch s { case 0 -> bitzero }
-
-typedef colors = enumerate { red; green; blue }
-
-let (colors) rgb = red
-
-function bit enu ((colors) red) = let (one, two) = (1,2) in 0
-
-function bit main _ = {ignore(sw(0)); ignore((nat) v2); ignore(enu(0)); v1[0] }
-
diff --git a/src/test/test2.sail b/src/test/test2.sail
deleted file mode 100644
index 6cc876c8..00000000
--- a/src/test/test2.sail
+++ /dev/null
@@ -1,15 +0,0 @@
-
-function unit f() = {
- (if( true ) then 
-   a := (nat) (3 + 0b01) mod 4
-  else 
-   a := 4
- );
- a:= (nat) 0b010101;
- a:= (nat) (0b0101010 + 0b0101000);
- c := (bit[5]) (3 + 0b00101) mod 3;
- if c[1] then c:= 31 else c:= 0;
- b := a;
-}
-
-
diff --git a/src/test/test3.sail b/src/test/test3.sail
deleted file mode 100644
index 5e9ba2df..00000000
--- a/src/test/test3.sail
+++ /dev/null
@@ -1,57 +0,0 @@
-(* a register containing nat numbers *)
-register [|0:256|] dummy_reg
-(* and one containing a byte *)
-register (bit[8]) dummy_reg2
-(* a function to read from memory; wmem serves no purpose currently,
-   memory-writing functions are figured out syntactically. *)
-val extern (nat,nat) -> unit effect { wmem }  MEMw
-val extern nat -> nat effect { rmem } MEMr
-val extern (nat,nat) -> unit effect { wmem }  MEM_GPUw
-val extern nat -> nat effect { rmem} MEM_GPUr
-val extern forall Nat 'n . ( nat, [|'n|], bit['n*8]) -> unit effect { wmem }  MEM_SIZEw
-val extern forall Nat 'n . ( nat, [|'n|]) -> bit['n*8] effect { rmem } MEM_SIZEr
-val extern (nat,bit[8]) -> unit effect { wmem }  MEM_WORDw
-val extern nat -> bit[8] effect { rmem } MEM_WORDr
-
-function nat (deinfix * ) ( (nat) x, (nat) y ) = 42
-
-function nat main _ = {
-  (* left-hand side function call = memory write *)
-  MEMw(0) := 0;
-  ignore(MEMr(0));
-  (* register write, idem *)
-  dummy_reg := 1;
-  (* register read, thanks to register declaration *)
-  ignore(dummy_reg);
-
-
-  MEM_WORDw(0) := 0b10101010;
-  (MEM_WORDw(0))[3..4] := 0b10;
-  (* XXX this one is broken - I don't what it should do,
-  or even if we should accept it, but the current result
-  is to eat up one bit, ending up with a 7-bit word. *)
-  (*(MEM_WORD(0))[4..3] := 0b10;*) (*We reject this as 4 > 3 not <= *)
-  ignore(MEM_WORDr(0));
-
-  (* infix call *)
-  ignore(7 * 9);
-
-  (* Some more checks *)
-  MEMw(1) := 2;
-  ignore(MEMr(1));
-  MEM_GPUw(0) := 3;
-  ignore(MEM_GPUr(0));
-  MEM_SIZEw(0,1) := 0b11110000;
-  ignore(MEM_SIZEr(0,1));
-  MEM_SIZEw(0,2) := 0b1111000010100000;
-  ignore(MEM_SIZEr(0,2));
-
-  (* extern calls *)
-  dummy_reg := 3 + 39;
-  (*dummy_reg := (deinfix +)(5, 37);*)
-  (* casts and external calls *)
-  dummy_reg := 0b01 + 0b01;
-  dummy_reg2 := 0b00000001;
-  dummy_reg2 := dummy_reg2 + dummy_reg2; (* cast to nat for add call *)
-  dummy_reg2;                            (* cast again and return 4 *)
-}
diff --git a/src/test/test4.sail b/src/test/test4.sail
deleted file mode 100644
index fa0133ca..00000000
--- a/src/test/test4.sail
+++ /dev/null
@@ -1,67 +0,0 @@
-(* hack to display log messages. Syntax: LOG(0) := "log message"; *)
-val extern forall Type 'a . (nat, 'a) -> unit effect { wmem }  LOG
-
-register (bit[1]) GPR0
-register (bit[1]) GPR1
-
-let (vector <0, 2, inc, (register<bit[1] >)>) GPR = [ GPR0, GPR1 ]
-
-(* if we access GPR with a bit or a nat - doing the conversion in the
-   caller, works as expected *)
-function unit good ((bit)  RA ) =
-{
-  LOG(0) := "good";
-  (nat) x := GPR[RA];
-}
-
-function unit good2 ((nat)  RA ) =
-{
-  LOG(0) := "good2";
-  (nat) x := GPR[RA];
-}
-
-(* but here, the first to_num_inc(RA) somehow inhibits the cast,
-   yielding to_num_inc(GPR0) instead of to_num_inc(0b0) *)
-function unit bad ((bit[1])  RA ) =
-{
-  LOG(0) := "oldbad";
-  (nat) x := GPR[RA];
-}
-
-(* and now, another bug - when DCR contains registers of bits instead of bit[0] *)
-
-register (bit) DCR0
-register (bit) DCR1
-
-let (vector <0, 2, inc, (register<bit >)>) DCR = [ DCR0, DCR1 ]
-
-(* also fails only when passing RA as a vector, nat and bit work fine as
-   above;
-   error message is different though, and very disturbing:
-   "error: No matching patterns in case", corresponding to the DCR[RA]
-   expression *)
-function unit bad2 ((bit[1])  RA ) =
-{
-  LOG(0) := "oldbad2";
-  (nat) x := DCR[RA];
-}
-
-
-function unit main () = {
-  LOG(0) := "init";
-
-  GPR[0] := 0b0;
-  GPR[1] := 0b1;
-
-  DCR[0] := bitzero;
-  DCR[1] := bitone;
-
-  good(bitzero);
-  good2(0);
-
-  (* a first bug *)
-  bad(0b0);
-
-  (* another bug :-) comment out first one to see it *)
-  bad2(0b0);
-}
diff --git a/src/test/test5.sail b/src/test/test5.sail
deleted file mode 100644
index bcc108c4..00000000
--- a/src/test/test5.sail
+++ /dev/null
@@ -1,21 +0,0 @@
-register (bit) SAT
-
-val forall Nat 'n, Nat 'm, 'n <= 0, 0 <= 'm.
-  (nat, [|'n|], [|'m|]) -> [|'n:'m|] effect { wreg } Clamp
-
-function
-  forall Nat 'n, Nat 'm, 'n <= 0, 0 <= 'm. ([|'n:'m|])
-  Clamp((nat) x, ([|'n|]) y, ([|'m|]) z) = {
-    ([|'n:'m|]) result := 0;
-    if (x<y) then {
-      result := y;
-      SAT := bitone;
-    } else if (x > z) then {
-      result := z;
-      SAT := bitone;
-    } else {
-      result := x;
-    };
-    result;
-  }
-
diff --git a/src/test/test_cp2_tagmem.elf b/src/test/test_cp2_tagmem.elf
deleted file mode 100755
index cad51d2a..00000000
--- a/src/test/test_cp2_tagmem.elf
+++ /dev/null
diff --git a/src/test/vectors.sail b/src/test/vectors.sail
deleted file mode 100644
index a861b65c..00000000
--- a/src/test/vectors.sail
+++ /dev/null
@@ -1,92 +0,0 @@
-let (bit[3]) v = 0b101
-let (bit[4]) v2 = [0,1,0,0]
-register (bit[4]) i
-
-let (bit[10]) v3 = 0b0101010111
-register (bit[10]) slice_check
-register (bit[10]) slice_check_copy
-register nat result
-
-function forall Type 'a . 'a id ( x ) = x
-
-register nat match_success
-register nat add_check
-register bit partial_check
-
-let (vector<0,3,inc,(register<(bit[10])>)>) gpr_small = [slice_check,slice_check,slice_check]
-
-let (bit[3]) indexed = [0=1,1=1,2=0]
-let (bit[50]) partial = [0 = 0, 5=1, 32=0; default = 0]
-let (bit[50]) partial_unspec = [0=0, 4=0, 7=1, 49=1]
-
-function unit decode ([bitzero, bitzero, bitone, bitzero]) = match_success := 1
-and decode x = match_success := x
-
-register (bit[32 : 63]) CR
-register (bit[5]) BA
-
-function bit main _ = {
-
-  slice_check := v3;
-  slice_check := v3[1..10];
-  slice_check := v3[5..10];
-
-  gpr_small[1] := v3; (*Writes to slice_check*)
-  slice_check_copy := gpr_small[1];
-  (* check that cast are inserted inside function calls (here +), and that the
-  previous assignment (to slice_check_copy) got the correct cast *)
-  result := gpr_small[1] + slice_check_copy;
-  (* idem with type inference for return type *)
-  fresh_var := gpr_small[1] + gpr_small[1];
-  (* id function call - prevents the correct cast currently *)
-  result := gpr_small[1] + id(gpr_small[1]);
- 
-  add_check := gpr_small[2] + 3;
-  partial_check := partial[5];
-  partial_check := partial[49];
-
-  i := [bitzero, bitzero, bitone, bitzero];
-
-  (* literal match *)
-  switch v {
-    case 0b101 -> match_success := 1
-    case _ -> match_success := v
-  };
-
-  switch i {
-    case [bitzero, bitzero, bitone, bitzero] -> match_success := 1
-    case _ -> match_success := i
-  };
-
-  decode(i);
-
-  (* concatenation *)
-  switch i {
-    case ([bitzero] : [bitzero, bitone] : [bitzero]) -> match_success := 1
-    case _ -> match_success := i
-  };
-  switch i {
-    (* check order of concatenation *)
-    case ([bitzero] : [bitone] : [bitzero] : [bitzero]) -> match_success := 99
-    case ([bitzero] : [bitzero] : [bitone] : [bitzero]) -> match_success := 1
-    case _ -> match_success := i
-  };
-
-  (* indexed match *)
-  switch i {
-    case [0=bitzero, 1=bitzero, 2=bitone, 3=bitzero] -> match_success := 1
-    case _ -> match_success := i
-  };
-
-  (* slice update *)
-  i[0] := bitzero;
-  i[2 .. 3] := [bitone, bitone];
-
-  (* constraints checking *)
-  BA := 12;
-  CR := 0b00000000000000000000000000000000;
-  CR[32 + BA] := CR[32 + BA];
-
-  (* slice access of literal *)
-  v[0];
-}