Merge master branch into sail2 for OCaml 4.06 compatibility

35 files changed, 304 insertions, 507 deletions

diff --git a/arm/Makefile b/arm/Makefile
index d7124df6..c597f714 100644
--- a/arm/Makefile
+++ b/arm/Makefile
@@ -38,7 +38,7 @@ apply_header:
 .PHONY: apply_header
 
 ######################################################################
-IDLARM=../../../rsem/idlarm
+IDLARM=../../rsem/idlarm
 
 pull_from_idlarm:
 	$(MAKE) -C $(IDLARM) clean
diff --git a/arm/aarch64_regfp.sail b/arm/aarch64_regfp.sail
index 148f9646..60aa48d1 100644
--- a/arm/aarch64_regfp.sail
+++ b/arm/aarch64_regfp.sail
@@ -168,7 +168,7 @@ function (regfps,regfps,regfps,niafps,diafp,instruction_kind) effect pure initia
       let (i,o) = BranchToFP(iR,oR) in {iR := i; oR := o};
       (bit[64]) nia' := rPC() + offset;
       Nias := [|| NIAFP_successor, NIAFP_concrete_address(nia') ||];
-      ik := IK_cond_branch;
+      ik := IK_branch;
     }
     case (BranchConditional(offset,condition)) -> {
       iR := append(iR,ConditionHoldsIFP(condition));
@@ -176,7 +176,7 @@ function (regfps,regfps,regfps,niafps,diafp,instruction_kind) effect pure initia
          ConditionHolds(condition) *)
       let (i,o) = BranchToFP(iR,oR) in {iR := i; oR := o};
       Nias := [|| NIAFP_successor, NIAFP_concrete_address(rPC() + offset) ||];
-      ik := IK_cond_branch;
+      ik := IK_branch;
     }
     case (GenerateExceptionEL1(imm)) -> not_implemented("GenerateExceptionEL1")
     case (GenerateExceptionEL2(imm)) -> not_implemented("GenerateExceptionEL2")
@@ -271,14 +271,14 @@ function (regfps,regfps,regfps,niafps,diafp,instruction_kind) effect pure initia
          operand[bit_pos] == bit_val *)
       let (i,o) = BranchToFP(iR,oR) in {iR := i; oR := o}; 
       Nias := [|| NIAFP_successor, NIAFP_concrete_address(rPC() + offset) ||];
-      ik := IK_cond_branch;
+      ik := IK_branch;
     }
     case (BranchImmediate(branch_type,offset)) -> {
       if branch_type == BranchType_CALL
         then {iR := _PCfp :: iR; oR := append(xFP(30),oR)};
       let (i,o) = BranchToFP(iR,oR) in {iR := i; oR := o}; 
       Nias := [|| NIAFP_concrete_address(rPC() + offset) ||];
-      ik := IK_simple (* IK_uncond_branch *)
+      ik := IK_branch
     }
     case (BranchRegister(n,branch_type)) -> {
       iR := append(iR,xFP(n));
@@ -287,8 +287,8 @@ function (regfps,regfps,regfps,niafps,diafp,instruction_kind) effect pure initia
       let (i,o) = BranchToFP(iR,oR) in {iR := i; oR := o};
       Nias := if n ==31
               then [|| NIAFP_concrete_address(0) ||]
-              else [|| NIAFP_register(RFull(_Rs[n]))||];
-      ik := IK_simple (* IK_uncond_branch *)
+              else [|| NIAFP_indirect_address ||];
+      ik := IK_branch
     }
     case (ExceptionReturn) -> not_implemented("ExceptionReturn")
     case (DebugRestorePState) -> not_implemented("DebugRestorePState")
diff --git a/arm/armV8.sail b/arm/armV8.sail
index 2614c7a5..4a62bda6 100644
--- a/arm/armV8.sail
+++ b/arm/armV8.sail
@@ -40,7 +40,7 @@ typedef ast = const union forall Nat 'R, 'R IN {32, 64},     (* register size *)
   ImplementationDefinedStopFetching;
   ImplementationDefinedThreadStart;
 
-  (* transactional memory, from the pre-alpha document *)
+  (* transactional memory, not part of the official spec *)
   (reg_index) TMStart;
   TMCommit;
   (boolean,bit[5]) TMAbort;
@@ -106,7 +106,7 @@ function forall Nat 'R, 'R IN {32,64}, Nat 'D, 'D IN {8,16,32,64}.
   Some(TMStart(t));
 }
 
-(* transactional memory, from the pre-alpha document *)
+(* transactional memory, not part of the official spec *)
 function clause execute (TMStart(t)) = {
   (bit[8]) nesting := TxNestingLevel;
 
@@ -132,7 +132,7 @@ function forall Nat 'R, 'R IN {32,64}, Nat 'D, 'D IN {8,16,32,64}.
   Some(TMCommit);
 }
 
-(* transactional memory, from the pre-alpha document *)
+(* transactional memory, not part of the official spec *)
 function clause execute (TMCommit) = {
   (bit[8]) nesting := TxNestingLevel;
 
@@ -151,7 +151,7 @@ function forall Nat 'R, 'R IN {32,64}, Nat 'D, 'D IN {8,16,32,64}.
   Some(TMTest);
 }
 
-(* transactional memory, from the pre-alpha document *)
+(* transactional memory, not part of the official spec *)
 function clause execute (TMTest) = {
   if TxNestingLevel > 0 then
     wPSTATE_NZCV() := 0b0000
@@ -166,7 +166,7 @@ function forall Nat 'R, 'R IN {32,64}, Nat 'D, 'D IN {8,16,32,64}.
   Some(TMAbort(R,imm5));
 }
 
-(* transactional memory, from the pre-alpha document *)
+(* transactional memory, not part of the official spec *)
 function clause execute (TMAbort(retry,reason)) = {
   if TxNestingLevel > 0 then {
     (bit[64]) status := 0;
@@ -642,7 +642,7 @@ function clause execute (BranchRegister(n,branch_type)) =
   (bit[64]) target := rX(n);
 
   if branch_type == BranchType_CALL then wX(30) := rPC() + 4;
-    BranchTo(target, branch_type);
+  BranchTo(target, branch_type);
 }
 
 (* ERET *)
diff --git a/arm/armV8_A64_sys_regs.sail b/arm/armV8_A64_sys_regs.sail
index 95b5c710..3a5f85fa 100644
--- a/arm/armV8_A64_sys_regs.sail
+++ b/arm/armV8_A64_sys_regs.sail
@@ -278,7 +278,7 @@ typedef EDSCR_type = register bits [31:0]
 }
 register (EDSCR_type) EDSCR (* External Debug Status and Control Register *)
 
-(* transactional memory, from the pre-alpha document *)
+(* transactional memory, not part of the official spec *)
 typedef TXIDR_EL0_type = register bits [63:0]
 {
   (*63..8 : RES0;*)
diff --git a/arm/gen/sail_trans_out.hgen b/arm/gen/sail_trans_out.hgen
index 9595f00c..84826c18 100644
--- a/arm/gen/sail_trans_out.hgen
+++ b/arm/gen/sail_trans_out.hgen
@@ -64,7 +64,7 @@
 | "Address", [d; page; imm] ->
   `AArch64Address ( translate_out_regzr Set64 d,
                     translate_out_bool page,
-                    translate_out_big_bit imm)
+                    translate_out_signed_big_bit imm)
 
 | "LogicalImmediate", [d; n; datasize; setflags; op; imm] ->
   let setflags' = translate_out_bool setflags in
diff --git a/arm/gen/shallow_ast_to_herdtools_ast.hgen b/arm/gen/shallow_ast_to_herdtools_ast.hgen
index aa989e95..6927767e 100644
--- a/arm/gen/shallow_ast_to_herdtools_ast.hgen
+++ b/arm/gen/shallow_ast_to_herdtools_ast.hgen
@@ -64,7 +64,7 @@
 | Address0 (d, page, imm) ->
   `AArch64Address ( translate_out_regzr Set64 d,
                     translate_out_bool page,
-                    translate_out_big_bit imm)
+                    translate_out_signed_big_bit imm)
 
 | LogicalImmediate (d, n, datasize, setflags, op, imm) ->
   let setflags' = translate_out_bool setflags in
diff --git a/etc/regfp.sail b/etc/regfp.sail
index cc057f2e..9a6172a9 100644
--- a/etc/regfp.sail
+++ b/etc/regfp.sail
@@ -16,9 +16,7 @@ typedef regfps = list <regfp>
 typedef niafp = const union {
   NIAFP_successor;
   (bit[64]) NIAFP_concrete_address;
-  NIAFP_LR;
-  NIAFP_CTR;
-  (regfp) NIAFP_register;
+  NIAFP_indirect_address;
 }
 
 typedef niafps = list <niafp>
@@ -90,7 +88,7 @@ typedef instruction_kind = const union {
   (read_kind) IK_mem_read;
   (write_kind) IK_mem_write;
   (read_kind, write_kind) IK_mem_rmw;
-  IK_cond_branch;
+  IK_branch;
   (trans_kind) IK_trans;
   IK_simple
 }
diff --git a/language/Makefile b/language/Makefile
index 081d90a7..759523b7 100644
--- a/language/Makefile
+++ b/language/Makefile
@@ -1,6 +1,6 @@
 #OTT=../../../rsem/ott/bin/ott
 # this is the binary that gets rebuilt by make in ott/src:
-OTT=../../../github/ott/src/ott
+OTT=../../ott/src/ott
 OTTLIB=$(dir $(shell which ott))../hol
 
 .PHONY: all
diff --git a/mips/mips_regfp.sail b/mips/mips_regfp.sail
index 36750583..13165f67 100644
--- a/mips/mips_regfp.sail
+++ b/mips/mips_regfp.sail
@@ -322,38 +322,34 @@ function (regfps,regfps,regfps,niafps,diafp,instruction_kind) initial_analysis (
       oR := RFull("HI") :: RFull ("LO") :: oR;
     }
     case (J(offset)) -> {
-      (* XXX actually unconditional jump *)
-      (*ik := IK_cond_branch;*)
+      ik := IK_branch;
       Dia := DIAFP_concrete((PC + 4)[63..28] : offset : 0b00);
     }
     case (JAL(offset)) -> {
-      (* XXX actually unconditional jump *)
-      (*ik := IK_cond_branch;*)
+      ik := IK_branch;
       oR := RFull("GPR31") :: oR;
       Dia := DIAFP_concrete((PC + 4)[63..28] : offset : 0b00);
     }
     case (JR(rs)) -> {
-      (* XXX actually unconditional jump *)
-      (*ik := IK_cond_branch;*)
+      ik := IK_branch;
       iR := RFull(GPRs[rs]) :: iR;
       Dia := DIAFP_reg(RFull(GPRs[rs]));
     }
     case (JALR(rs, rd)) -> {
-      (* XXX actually unconditional jump *)
-      (*ik := IK_cond_branch;*)
+      ik := IK_branch;
       iR := RFull(GPRs[rs]) :: iR;
       oR := RFull("GPR31") :: oR;
       Dia := DIAFP_reg(RFull(GPRs[rs]));
     }
     case (BEQ(rs, rd, imm, ne, likely)) -> {
-      ik := IK_cond_branch;
+      ik := IK_branch;
       if rs == 0 then () else iR := RFull(GPRs[rs]) :: iR;
       if rd == 0 then () else iR := RFull(GPRs[rd]) :: iR;
       let (bit[64]) offset = (EXTS(imm : 0b00) + 4) in
       Dia := DIAFP_concrete (PC + offset);
     }
     case (BCMPZ(rs, imm, cmp, link, likely)) -> {
-      ik := IK_cond_branch;
+      ik := IK_branch;
       if rs == 0 then () else iR := RFull(GPRs[rs]) :: iR;
       if link then
         oR := RFull("GPR31") :: oR;
diff --git a/power/power_regfp.sail b/power/power_regfp.sail
index 35ecb37b..1f421186 100644
--- a/power/power_regfp.sail
+++ b/power/power_regfp.sail
@@ -76,7 +76,7 @@ function (regfps,regfps,regfps,niafps,diafp,instruction_kind) initial_analysis (
       if LK then oR := RFull("LR") :: oR;
       (bit[64]) nia' := if AA then EXTS(LI : 0b00) else CIA + EXTS(LI : 0b00);
       Nias := [|| NIAFP_concrete_address(nia') ||];
-      ik := IK_simple (* IK_uncond_branch *);
+      ik := IK_branch
     }
     case (Bc (BO, BI, BD, AA, LK)) -> {
       iR := mode64bit_fp :: iR;
@@ -89,7 +89,7 @@ function (regfps,regfps,regfps,niafps,diafp,instruction_kind) initial_analysis (
       if AA then iR := CIA_fp :: iR; 
       Nias := [|| NIAFP_successor, NIAFP_concrete_address(if AA then EXTS(BD : 0b00) else CIA + EXTS(BD : 0b00)) ||];
       if LK then {oR := RFull("LR") :: oR; iR := CIA_fp :: iR};
-      ik := IK_cond_branch
+      ik := IK_branch
     }
     case (Bclr (BO, BI, BH, LK)) -> {
       iR := mode64bit_fp :: iR;
@@ -99,18 +99,18 @@ function (regfps,regfps,regfps,niafps,diafp,instruction_kind) initial_analysis (
       (* TODO: actually whether LR is read, NIA written depends on runtime data *)
       (* if ctr_ok .. *) iR := RSlice("LR",0,61) :: iR;
       oR := NIA_fp :: oR;
-      Nias := [|| NIAFP_successor, NIAFP_LR ||];
+      Nias := [|| NIAFP_successor, NIAFP_indirect_address ||];
       if LK then {oR := RFull("LR") :: oR; iR := CIA_fp :: iR;};
-      ik := IK_cond_branch;
+      ik := IK_branch;
     }
     case (Bcctr (BO, BI, BH, LK)) -> {
       iR := RSliceBit("CR",BI + 32) :: iR;
       (* TODO: actually whether CTR is read and NIA written depends on runtime data *)
       (* if cond_ok *) iR := RSlice("CTR",0,61) :: iR;
       oR := NIA_fp :: oR;
-      Nias := [|| NIAFP_successor, NIAFP_CTR ||];
+      Nias := [|| NIAFP_successor, NIAFP_indirect_address ||];
       if LK then {oR := RFull("LR") :: oR; iR := CIA_fp :: iR;};
-      ik := IK_cond_branch;
+      ik := IK_branch;
     }
     case (Crand (BT, BA, BB)) -> {
       iR := RSliceBit("CR",BA + 32) :: RSliceBit("CR",BB + 32) :: iR;
@@ -150,7 +150,7 @@ function (regfps,regfps,regfps,niafps,diafp,instruction_kind) initial_analysis (
     }
     case (Sc (LEV)) -> {
       (* fake test end instruction *)
-      Nias := if LEV==63 then [|| ||] else [|| NIAFP_successor ||]; 
+      ();
     }
     case (Scv (LEV)) -> ()
     case (Lbz (RT, RA, D)) -> {
@@ -1480,4 +1480,4 @@ function (regfps,regfps,regfps,niafps,diafp,instruction_kind) recalculate_stswx_
   };
   ik := IK_mem_write(Write_plain);
   (iR,oR,aR,Nias,Dia,ik)}
-}
\ No newline at end of file
+}
diff --git a/src/Makefile b/src/Makefile
index 924cfb1c..e44f13fb 100644
--- a/src/Makefile
+++ b/src/Makefile
@@ -48,6 +48,20 @@
 #  SUCH DAMAGE.                                                          #
 ##########################################################################
 
+$(warning MAKECMDGOALS is $(MAKECMDGOALS))
+ifneq ($(MAKECMDGOALS),clean)
+# Lem optionally vendors the zarith dependency, but currently
+# we don't use that -- just assume the host system has zarith.
+ifeq ($(shell ocamlfind query zarith),)
+$(error No zarith installed [anywhere ocamlfind can find it]; install it (opam install zarith || apt-get install libzarith-ocaml{,-dev} || yum install ocaml-zarith), or use make install_dependencies in lem/ocaml-lib.)
+endif
+# assume the host system has lem
+ifeq ($(shell ocamlfind query lem),)
+$(error No lem installed [anywhere ocamlfind can find it]; please install it ('make install' from lem/ocaml-lib || 'make local-install' from lem/ocaml-lib and add lem/ocaml-lib/local to OCAMLPATH))
+endif
+endif
+
+
 .PHONY: all sail sail.native sail.byte test clean doc lib power test_power test_idempotence
 
 # set to -p on command line to enable gprof profiling
@@ -75,7 +89,7 @@ lem_interp/interp_ast.lem: ../language/l2.ott
 	ott -sort false -generate_aux_rules true -o lem_interp/interp_ast.lem -picky_multiple_parses true ../language/l2.ott
 
 sail: ast.ml bytecode.ml
-	ocamlbuild -use-ocamlfind sail.native
+	ocamlbuild -use-ocamlfind sail.native sail_lib.cma sail_lib.cmxa
 
 isail: ast.ml bytecode.ml
 	ocamlbuild -use-ocamlfind isail.native
@@ -86,23 +100,19 @@ sail.byte:
 	ocamlbuild -use-ocamlfind -cflag -g sail.byte
 
 interpreter: lem_interp/interp_ast.lem
-	ocamlbuild lem_interp/extract.cmxa
-	ocamlbuild lem_interp/extract.cma
+	ocamlbuild -use-ocamlfind lem_interp/extract.cmxa
+	ocamlbuild -use-ocamlfind lem_interp/extract.cma
 
 test: sail interpreter
-	ocamlbuild test/run_tests.native
+	ocamlbuild -use-ocamlfind test/run_tests.native
 	./run_tests.native
 
 THIS_MAKEFILE := $(realpath $(lastword $(MAKEFILE_LIST)))
 SAIL_DIR:=$(realpath $(dir $(THIS_MAKEFILE))..)
-BITBUCKET_ROOT=$(realpath $(dir $(THIS_MAKEFILE))../..)
+PROJECT_ROOT=$(realpath $(dir $(THIS_MAKEFILE))../..)
 
-LEM = $(BITBUCKET_ROOT)/lem/lem
-LEMLIBOCAML = $(BITBUCKET_ROOT)/lem/ocaml-lib/_build_zarith
-ELFDIR= $(BITBUCKET_ROOT)/linksem
-ZARITH_DIR=$(LEMLIBOCAML)/dependencies/zarith
-ZARITH_LIB=$(ZARITH_DIR)/zarith.cma
-# ZARITH_LIB=$(ZARITH_DIR)/zarith.cmxa
+LEM = $(PROJECT_ROOT)/lem/lem
+ELFDIR= $(PROJECT_ROOT)/linksem
 
 SAIL_LIB_DIR:=$(SAIL_DIR)/lib
 MIPS_SAIL_DIR:=$(SAIL_DIR)/mips_new_tc
@@ -154,39 +164,39 @@ _build/mips.lem: $(MIPS_SAILS) ./sail.native
 	cd _build ;\
 	../sail.native -lem_ast -o mips $(MIPS_SAILS)
 
-_build/mips_embed_types.lem: $(MIPS_NOTLB_SAILS) ./sail.native
+_build/mips_types.lem: $(MIPS_NOTLB_SAILS) ./sail.native
 	mkdir -p _build
 	cd _build ;\
-	../sail.native -lem_lib "Mips_extras_embed" -lem -lem_mwords -o mips $(MIPS_NOTLB_SAILS)
+	../sail.native -lem_lib "Mips_extras" -lem -lem_mwords -o mips $(MIPS_NOTLB_SAILS)
 
-_build/Mips_embed.thy: _build/mips_embed_types.lem
+_build/Mips.thy: _build/mips_types.lem
 	cd _build ;\
-	lem -isa -outdir . -lib ../lem_interp -lib ../gen_lib $(MIPS_SAIL_DIR)/mips_extras_embed.lem mips_embed_types.lem mips_embed.lem
+	lem -isa -outdir . -lib ../lem_interp -lib ../gen_lib $(MIPS_SAIL_DIR)/mips_extras.lem mips_types.lem mips.lem
 
 _build/mips_notlb.lem: $(MIPS_NOTLB_SAILS) ./sail.native
 	mkdir -p _build
 	cd _build ; \
 	../sail.native -lem_ast -o mips_notlb $(MIPS_NOTLB_SAILS)
 
-_build/mips_notlb_embed.ml: $(MIPS_NOTLB_SAILS_PRE) ./sail.native
+_build/mips_notlb.ml: $(MIPS_NOTLB_SAILS_PRE) ./sail.native
 	mkdir -p _build
 	cd _build ; \
-	../sail.native -ocaml -lem -lem_ast -ocaml_lib Mips_extras_ml -o mips_notlb_embed $(MIPS_NOTLB_SAILS_PRE)
+	../sail.native -ocaml -lem -lem_ast -ocaml_lib Mips_extras_ml -o mips_notlb $(MIPS_NOTLB_SAILS_PRE)
 
-_build/mips_embed.ml: $(MIPS_SAILS_PRE) ./sail.native
+_build/mips.ml: $(MIPS_SAILS_PRE) ./sail.native
 	mkdir -p _build
 	cd _build ; \
-	../sail.native -ocaml -lem -lem_ast -ocaml_lib Mips_extras_ml -o mips_embed $(MIPS_SAILS_PRE)
+	../sail.native -ocaml -lem -lem_ast -ocaml_lib Mips_extras_ml -o mips $(MIPS_SAILS_PRE)
 
-_build/cheri_embed.ml: $(CHERI_SAILS) ./sail.native
+_build/cheri.ml: $(CHERI_SAILS) ./sail.native
 	mkdir -p _build
 	cd _build ; \
-	../sail.native -ocaml -lem -lem_ast -ocaml_lib Mips_extras_ml -o cheri_embed $(CHERI_SAILS)
+	../sail.native -ocaml -lem -lem_ast -ocaml_lib Mips_extras_ml -o cheri $(CHERI_SAILS)
 
-_build/cheri128_embed.ml: $(CHERI128_SAILS) ./sail.native
+_build/cheri128.ml: $(CHERI128_SAILS) ./sail.native
 	mkdir -p _build
 	cd _build ; \
-	../sail.native -ocaml -lem -lem_ast -ocaml_lib Mips_extras_ml -o cheri128_embed $(CHERI128_SAILS)
+	../sail.native -ocaml -lem -lem_ast -ocaml_lib Mips_extras_ml -o cheri128 $(CHERI128_SAILS)
 
 _build/cheri.lem: $(CHERI_SAILS) ./sail.native
 	mkdir -p _build
@@ -203,14 +213,14 @@ _build/cheri_notlb.lem: $(CHERI_NOTLB_SAILS) ./sail.native
 	cd _build ;\
 	../sail.native -lem_ast -o cheri_notlb $(CHERI_NOTLB_SAILS)
 
-_build/cheri_embed_types_sequential.lem: $(CHERI_SAILS) ./sail.native
+_build/cheri_types.lem: $(CHERI_SAILS) ./sail.native
 	mkdir -p _build
 	cd _build ;\
-	../sail.native -lem_lib "Mips_extras_embed" -lem -lem_sequential -lem_mwords -o cheri $(CHERI_SAILS)
+	../sail.native -lem_lib "Mips_extras" -lem -lem_mwords -o cheri $(CHERI_SAILS)
 
-_build/Cheri_embed_sequential.thy: _build/cheri_embed_types_sequential.lem
+_build/Cheri.thy: _build/cheri_types.lem
 	cd _build ;\
-	lem -isa -outdir . -lib ../lem_interp -lib ../gen_lib $(MIPS_SAIL_DIR)/mips_extras_embed_sequential.lem cheri_embed_types_sequential.lem cheri_embed_sequential.lem
+	lem -isa -outdir . -lib ../lem_interp -lib ../gen_lib $(MIPS_SAIL_DIR)/mips_extras.lem cheri_types.lem cheri.lem
 
 _build/mips_all.sail: $(MIPS_SAILS)
 	cat $(MIPS_SAILS) > $@
@@ -231,32 +241,32 @@ count: _build/cheri_trimmed.sail _build/mips_trimmed.sail
 #	env OCAMLRUNPARAM=l=100M ocamlfind ocamlopt $(OCAML_OPTS) -g -package num -package str -package unix -I $(ELFDIR)/contrib/ocaml-uint/_build/lib -I $(LEMLIBOCAML) -I $(ZARITH_DIR) -I _build/lem_interp/ -I $(ELFDIR)/src  -I $(ELFDIR)/src/adaptors -I $(ELFDIR)/src/abis/mips64 -I _build -linkpkg $(ZARITH_LIB) $(LEMLIBOCAML)/extract.cmxa $(ELFDIR)/contrib/ocaml-uint/_build/lib/uint.cmxa $(ELFDIR)/src/linksem.cmxa  _build/pprint/src/PPrintLib.cmxa _build/lem_interp/extract.cmxa _build/mips.ml _build/mips_extras.ml _build/run_with_elf.ml  -o run_mips.native
 
 run_mips.native: _build/mips.ml _build/mips_extras.ml _build/run_with_elf.ml interpreter
-	env OCAMLRUNPARAM=l=100M ocamlfind ocamlc $(OCAML_OPTS) -g -package num -package str -package unix -I $(ELFDIR)/contrib/ocaml-uint/_build/lib -I $(LEMLIBOCAML) -I $(ZARITH_DIR) -I _build/lem_interp/ -I $(ELFDIR)/src  -I $(ELFDIR)/src/adaptors -I $(ELFDIR)/src/abis/mips64 -I _build -linkpkg $(ZARITH_LIB) $(LEMLIBOCAML)/extract.cma $(ELFDIR)/contrib/ocaml-uint/_build/lib/uint.cma $(ELFDIR)/src/linksem.cma  _build/pprint/src/PPrintLib.cma _build/lem_interp/extract.cma _build/mips.ml _build/mips_extras.ml _build/run_with_elf.ml  -o run_mips.native
+	env OCAMLRUNPARAM=l=100M ocamlfind ocamlopt $(OCAML_OPTS) -g -package num -package str -package unix -package zarith -package lem -package linksem -linkpkg -I _build/lem_interp/ -I _build _build/pprint/src/PPrintLib.cmxa _build/lem_interp/extract.cmxa _build/mips.ml _build/mips_extras.ml _build/run_with_elf.ml -o run_mips.native
 
 run_cheri.native:  _build/cheri.ml _build/mips_extras.ml _build/run_with_elf_cheri.ml interpreter
-	env OCAMLRUNPARAM=l=100M ocamlfind ocamlopt $(OCAML_OPTS) -g -package num -package str -package unix -I $(ELFDIR)/contrib/ocaml-uint/_build/lib -I $(LEMLIBOCAML) -I $(ZARITH_DIR) -I _build/lem_interp/ -I $(ELFDIR)/src  -I $(ELFDIR)/src/adaptors -I $(ELFDIR)/src/abis/mips64 -I _build -linkpkg $(ZARITH_LIB) $(LEMLIBOCAML)/extract.cmxa $(ELFDIR)/contrib/ocaml-uint/_build/lib/uint.cmxa $(ELFDIR)/src/linksem.cmxa  _build/pprint/src/PPrintLib.cmxa _build/lem_interp/extract.cmxa _build/cheri.ml _build/mips_extras.ml _build/run_with_elf_cheri.ml  -o run_cheri.native
+	env OCAMLRUNPARAM=l=100M ocamlfind ocamlopt $(OCAML_OPTS) -g -package num -package str -package unix -package zarith -package lem -package linksem -linkpkg -I _build/lem_interp/ -I _build _build/pprint/src/PPrintLib.cmxa _build/lem_interp/extract.cmxa _build/cheri.ml _build/mips_extras.ml _build/run_with_elf_cheri.ml  -o run_cheri.native
 
 run_cheri128.native:  _build/cheri128.ml _build/mips_extras.ml _build/run_with_elf_cheri128.ml interpreter
-	env OCAMLRUNPARAM=l=100M ocamlfind ocamlopt $(OCAML_OPTS) -g -package num -package str -package unix -I $(ELFDIR)/contrib/ocaml-uint/_build/lib -I $(LEMLIBOCAML) -I $(ZARITH_DIR) -I _build/lem_interp/ -I $(ELFDIR)/src  -I $(ELFDIR)/src/adaptors -I $(ELFDIR)/src/abis/mips64 -I _build -linkpkg $(ZARITH_LIB) $(LEMLIBOCAML)/extract.cmxa $(ELFDIR)/contrib/ocaml-uint/_build/lib/uint.cmxa $(ELFDIR)/src/linksem.cmxa  _build/pprint/src/PPrintLib.cmxa _build/lem_interp/extract.cmxa _build/cheri128.ml _build/mips_extras.ml _build/run_with_elf_cheri128.ml  -o run_cheri128.native
+	env OCAMLRUNPARAM=l=100M ocamlfind ocamlopt $(OCAML_OPTS) -g -package num -package str -package unix -package zarith -package lem -package linksem -linkpkg -I _build/lem_interp/ -I _build _build/pprint/src/PPrintLib.cmxa _build/lem_interp/extract.cmxa _build/cheri128.ml _build/mips_extras.ml _build/run_with_elf_cheri128.ml  -o run_cheri128.native
 
-run_embed.native: _build/sail_values.ml _build/mips_extras_ml.ml _build/mips_embed.ml _build/cheri_embed.ml _build/cheri128_embed.ml _build/run_embed.ml
-	env OCAMLRUNPARAM=l=100M ocamlfind ocamlopt $(OCAML_OPTS) -g -package unix -I $(ZARITH_DIR) -I _build -linkpkg $(ZARITH_LIB) $^ -o $@
+run_embed.native: _build/sail_values.ml _build/mips_extras_ml.ml _build/mips.ml _build/cheri.ml _build/cheri128.ml _build/run_embed.ml
+	env OCAMLRUNPARAM=l=100M ocamlfind ocamlopt $(OCAML_OPTS) -g -package zarith -package unix -I _build -linkpkg $^ -o $@
 
 _build/power.ml: $(SAIL_DIR)/src/test/power.sail sail.native
 	cd _build; \
 	./sail.native -lem_ast -ocaml $< -o $(basename $(@))
 
 _build/power.native: _build/sail_values.ml _build/power.ml
-	env OCAMLRUNPARAM=l=100M ocamlfind ocamlopt $(OCAML_OPTS) -g -package unix -I $(ZARITH_DIR) -I _build -linkpkg $(ZARITH_LIB) $^ -o $@
+	env OCAMLRUNPARAM=l=100M ocamlfind ocamlopt $(OCAML_OPTS) -g -package zarith -package unix -I _build -linkpkg $^ -o $@
 
 _build/armv8_embed.ml: sail.native
 	make -C ../arm ocaml
 	cp ../arm/build/armv8_embed.ml $@
 
 _build/arm.native: _build/sail_values.ml _build/armv8_embed.ml
-	env OCAMLRUNPARAM=l=100M ocamlfind ocamlopt $(OCAML_OPTS) -g -package unix -I $(ZARITH_DIR) -I _build -linkpkg $(ZARITH_LIB) $^ -o $@
+	env OCAMLRUNPARAM=l=100M ocamlfind ocamlopt $(OCAML_OPTS) -g -package zarith -package unix -I _build -linkpkg $^ -o $@
 
-mips_notlb: _build/mips_notlb.ml  _build/mips_embed_types.lem _build/mips_extras.ml
+mips_notlb: _build/mips_notlb.ml  _build/mips_types.lem _build/mips_extras.ml
 	true
 
 mips: elf run_mips.native
diff --git a/src/_tags b/src/_tags
index bb9b9c04..1b9be030 100644
--- a/src/_tags
+++ b/src/_tags
@@ -9,8 +9,8 @@ true: -traverse, debug, use_menhir
 <*.m{l,li}>: package(lem)
 
 # see http://caml.inria.fr/mantis/view.php?id=4943
-<lem_interp/*> and not <lem_interp/*.cmxa>: use_nums, package(lem)
-<test/*> and not <test/*.cmxa>: use_nums, package(lem), use_str
+<lem_interp/*> and not <lem_interp/*.cmxa>: package(num), package(lem)
+<test/*> and not <test/*.cmxa>: package(num), package(lem), package(str)
 
 # disable partial match and unused variable warnings
 <**/*.ml>: warn_y
diff --git a/src/gen_lib/deep_shallow_convert.lem b/src/gen_lib/deep_shallow_convert.lem
index 76880dbd..7fea0409 100644
--- a/src/gen_lib/deep_shallow_convert.lem
+++ b/src/gen_lib/deep_shallow_convert.lem
@@ -532,7 +532,7 @@ let instruction_kindToInterpValue = function
   | IK_mem_read v -> V_ctor (Id_aux (Id "IK_mem_read") Unknown) (T_id "instruction_kind") C_Union (toInterpValue v)
   | IK_mem_write v -> V_ctor (Id_aux (Id "IK_mem_write") Unknown) (T_id "instruction_kind") C_Union (toInterpValue v)
   | IK_mem_rmw v -> V_ctor (Id_aux (Id "IK_mem_rmw") Unknown) (T_id "instruction_kind") C_Union (toInterpValue v)
-  | IK_cond_branch -> V_ctor (Id_aux (Id "IK_cond_branch") Unknown) (T_id "instruction_kind") C_Union (toInterpValue ())
+  | IK_branch -> V_ctor (Id_aux (Id "IK_branch") Unknown) (T_id "instruction_kind") C_Union (toInterpValue ())
   | IK_trans v -> V_ctor (Id_aux (Id "IK_trans") Unknown) (T_id "instruction_kind") C_Union (toInterpValue v)
   | IK_simple -> V_ctor (Id_aux (Id "IK_simple") Unknown) (T_id "instruction_kind") C_Union (toInterpValue ())
   end
@@ -541,7 +541,7 @@ let rec instruction_kindFromInterpValue v = match v with
   | V_ctor (Id_aux (Id "IK_mem_read") _) _ _ v -> IK_mem_read (fromInterpValue v)
   | V_ctor (Id_aux (Id "IK_mem_write") _) _ _ v -> IK_mem_write (fromInterpValue v)
   | V_ctor (Id_aux (Id "IK_mem_rmw") _) _ _ v -> IK_mem_rmw (fromInterpValue v)
-  | V_ctor (Id_aux (Id "IK_cond_branch") _) _ _ v -> IK_cond_branch
+  | V_ctor (Id_aux (Id "IK_branch") _) _ _ v -> IK_branch
   | V_ctor (Id_aux (Id "IK_trans") _) _ _ v -> IK_trans (fromInterpValue v)
   | V_ctor (Id_aux (Id "IK_simple") _) _ _ v -> IK_simple
   | V_tuple [v] -> instruction_kindFromInterpValue v
diff --git a/src/gen_lib/sail_values.lem b/src/gen_lib/sail_values.lem
index 3d55843e..33caac37 100644
--- a/src/gen_lib/sail_values.lem
+++ b/src/gen_lib/sail_values.lem
@@ -801,9 +801,7 @@ let toNaturalFiveTup (n1,n2,n3,n4,n5) =
 type niafp =
   | NIAFP_successor
   | NIAFP_concrete_address of vector bitU
-  | NIAFP_LR
-  | NIAFP_CTR
-  | NIAFP_register of regfp
+  | NIAFP_indirect_address
 
 (* only for MIPS *)
 type diafp =
@@ -834,15 +832,13 @@ end
 
 let niafp_to_nia reginfo = function
   | NIAFP_successor -> NIA_successor
-  | NIAFP_concrete_address v -> NIA_concrete_address (address_of_bitv (bits_of v))
-  | NIAFP_LR -> NIA_LR
-  | NIAFP_CTR -> NIA_CTR
-  | NIAFP_register r -> NIA_register (regfp_to_reg reginfo r)
+  | NIAFP_concrete_address v -> NIA_concrete_address (address_of_bitv v)
+  | NIAFP_indirect_address -> NIA_indirect_address
 end
 
 let diafp_to_dia reginfo = function
   | DIAFP_none -> DIA_none
-  | DIAFP_concrete v -> DIA_concrete_address (address_of_bitv (bits_of v))
+  | DIAFP_concrete v -> DIA_concrete_address (address_of_bitv v)
   | DIAFP_reg r -> DIA_register (regfp_to_reg reginfo r)
 end
 *)
diff --git a/src/lem_interp/interp_inter_imp.lem b/src/lem_interp/interp_inter_imp.lem
index 563da2e5..74e43a8f 100644
--- a/src/lem_interp/interp_inter_imp.lem
+++ b/src/lem_interp/interp_inter_imp.lem
@@ -573,13 +573,11 @@ let instruction_analysis top_level end_flag thunk_name regn_to_reg_details regis
          | Interp_ast.V_ctor (Id_aux (Id "DIAFP_reg") _) _ _ reg -> DIA_register (reg_to_reg_name reg) 
          | _ -> failwith "Register footprint analysis did not return dia of expected type" end in
        let nia_to_nia = function
-         | Interp_ast.V_ctor (Id_aux (Id "NIAFP_successor") _) _ _ _-> NIA_successor
+         | Interp_ast.V_ctor (Id_aux (Id "NIAFP_successor") _) _ _ _ -> NIA_successor
          | Interp_ast.V_ctor (Id_aux (Id "NIAFP_concrete_address") _) _ _ address ->
             NIA_concrete_address (get_addr address)
-         | Interp_ast.V_ctor (Id_aux (Id "NIAFP_LR") _) _ _ _ -> NIA_LR
-         | Interp_ast.V_ctor (Id_aux (Id "NIAFP_CTR") _) _ _ _ -> NIA_CTR
-         | Interp_ast.V_ctor (Id_aux (Id "NIAFP_register") _) _ _ reg ->
-            NIA_register (reg_to_reg_name reg)
+         | Interp_ast.V_ctor (Id_aux (Id "NIAFP_indirect_address") _) _ _ _ ->
+            NIA_indirect_address
          | _ -> failwith "Register footprint analysis did not return nia of expected type" end in
        let readk_to_readk = function
                          | "Read_plain" ->             Read_plain
@@ -636,8 +634,8 @@ let instruction_analysis top_level end_flag thunk_name regn_to_reg_details regis
            (Interp_ast.V_tuple [(Interp_ast.V_ctor (Id_aux (Id readk) _) _ _ _) ;
                                 (Interp_ast.V_ctor (Id_aux (Id writek) _) _ _ _)]) ->
             IK_mem_rmw(readk_to_readk readk, writek_to_writek writek)
-         | Interp_ast.V_ctor (Id_aux (Id "IK_cond_branch") _) _ _ _ ->
-            IK_cond_branch
+         | Interp_ast.V_ctor (Id_aux (Id "IK_branch") _) _ _ _ ->
+            IK_branch
          | Interp_ast.V_ctor (Id_aux (Id "IK_simple") _) _ _ _ ->
             IK_simple
          | _ -> failwith "Analysis returned unexpected instruction kind"
@@ -1159,7 +1157,7 @@ let rr_interp_exhaustive mode i_state events =
 *)
 
 
-let instruction_kind_of_event : event -> maybe instruction_kind = function
+let instruction_kind_of_event nia_reg : event -> maybe instruction_kind = function
   (* this is a hack to avoid adding special events for AArch64 transactional-memory *)
   | E_read_reg (Reg "TMStartEffect" 63 64 D_decreasing) -> Just (IK_trans Transaction_start)
   | E_write_reg (Reg "TMAbortEffect" 63 64 D_decreasing) _ -> Just (IK_trans Transaction_abort)
@@ -1175,7 +1173,9 @@ let instruction_kind_of_event : event -> maybe instruction_kind = function
   | E_barrier bk -> Just (IK_barrier bk)
   | E_footprint -> Nothing
   | E_read_reg _ -> Nothing
-  | E_write_reg _ _ -> Nothing
+  | E_write_reg reg _ ->
+      if register_base_name reg = register_base_name nia_reg then Just IK_branch
+      else Nothing
   | E_error s -> failwith ("instruction_kind_of_event error: "^s)
   | E_escape -> Nothing (*failwith ("instruction_kind_of_event escape")*)
  end
@@ -1254,8 +1254,8 @@ let interp_instruction_analysis
       (interp_exhaustive : ((list (reg_name * register_value)) -> list event))
       instruction 
       nia_reg 
-      (nias_function : (list (maybe address) -> list reg_name -> list nia))
-      ism environment = 
+      (nias_function : (list (maybe address) -> list nia))
+      ism environment =
     
     let es = interp_exhaustive environment in
 
@@ -1265,19 +1265,15 @@ let interp_instruction_analysis
     let regs_feeding_address = List.concatMap regs_feeding_memory_access_address_of_event es in
 
     let nia_address = List.mapMaybe (nia_address_of_event nia_reg) es in
-
-    let nias = nias_function nia_address regs_in in
+    let nias = nias_function nia_address in
 
     let dia = DIA_none in (* FIX THIS! *)
 
-
     let inst_kind =
-      match List.mapMaybe instruction_kind_of_event es with
-      | [] -> if List.length nias > 1 then IK_cond_branch else IK_simple
+      match List.mapMaybe (instruction_kind_of_event nia_reg) es with
+      | [] -> IK_simple
+      | inst_kind :: [] -> inst_kind
       | inst_kind :: inst_kinds ->
-          let () = ensure (List.length nias > 1 --> inst_kind = IK_cond_branch)
-                      "multiple NIAs must be IK_cond_branch" in
-
           if forall (inst_kind' MEM inst_kinds). inst_kind' = inst_kind then
             inst_kind
 
@@ -1288,19 +1284,9 @@ let interp_instruction_analysis
                 | IK_mem_write _ -> true
                 | IK_mem_rmw _   -> false
                 | IK_barrier _   -> false
-                | IK_cond_branch -> false
+                | IK_branch      -> false
                 | IK_trans _     -> false
                 | IK_simple      -> false
-                end) &&
-            (exists (inst_kind' MEM (inst_kind :: inst_kinds)).
-                match inst_kind' with
-                | IK_mem_read _  -> true
-                | _              -> false
-                end) &&
-            (exists (inst_kind' MEM (inst_kind :: inst_kinds)).
-                match inst_kind' with
-                | IK_mem_write _ -> true
-                | _              -> false
                 end)
           then
             match
@@ -1357,7 +1343,7 @@ let interp_compare_analyses
       interp_exhaustive
       (instruction : Interp_ast.value)
       nia_reg
-      (nias_function : (list (maybe address) -> list reg_name -> list nia))
+      (nias_function : (list (maybe address) -> list nia))
       ism
       environment
       analysis_function
diff --git a/src/lem_interp/run_with_elf.ml b/src/lem_interp/run_with_elf.ml
index bb56c8a9..0dadc007 100644
--- a/src/lem_interp/run_with_elf.ml
+++ b/src/lem_interp/run_with_elf.ml
@@ -736,11 +736,11 @@ let initial_system_state_of_elf_file name =
             initial_stack_and_reg_data_of_MIPS_elf_file e_entry !data_mem in
           
           (Mips.defs,
-           (Mips_extras.read_memory_functions,
-            Mips_extras.memory_writes,
-            Mips_extras.memory_eas,
-            Mips_extras.memory_vals,
-            Mips_extras.barrier_functions),
+           (Mips_extras.mips_read_memory_functions,
+            Mips_extras.mips_memory_writes,
+            Mips_extras.mips_memory_eas,
+            Mips_extras.mips_memory_vals,
+            Mips_extras.mips_barrier_functions),
            [],
            MIPS,
            D_decreasing,
diff --git a/src/lem_interp/run_with_elf_cheri.ml b/src/lem_interp/run_with_elf_cheri.ml
index 3d187aa9..2bf84e2d 100644
--- a/src/lem_interp/run_with_elf_cheri.ml
+++ b/src/lem_interp/run_with_elf_cheri.ml
@@ -405,13 +405,13 @@ let initial_system_state_of_elf_file name =
             initial_stack_and_reg_data_of_MIPS_elf_file e_entry !data_mem in
           
           (Cheri.defs,
-           (Mips_extras.read_memory_functions,
-            Mips_extras.read_memory_tagged_functions,
-            Mips_extras.memory_writes,
-            Mips_extras.memory_eas,
-            Mips_extras.memory_vals,
-            Mips_extras.memory_vals_tagged,
-            Mips_extras.barrier_functions),
+           (Mips_extras.mips_read_memory_functions,
+            Mips_extras.mips_read_memory_tagged_functions,
+            Mips_extras.mips_memory_writes,
+            Mips_extras.mips_memory_eas,
+            Mips_extras.mips_memory_vals,
+            Mips_extras.mips_memory_vals_tagged,
+            Mips_extras.mips_barrier_functions),
            [],
            MIPS,
            D_decreasing,
diff --git a/src/lem_interp/run_with_elf_cheri128.ml b/src/lem_interp/run_with_elf_cheri128.ml
index 6b12ebbb..e4d91c41 100644
--- a/src/lem_interp/run_with_elf_cheri128.ml
+++ b/src/lem_interp/run_with_elf_cheri128.ml
@@ -405,13 +405,13 @@ let initial_system_state_of_elf_file name =
             initial_stack_and_reg_data_of_MIPS_elf_file e_entry !data_mem in
           
           (Cheri128.defs,
-           (Mips_extras.read_memory_functions,
-            Mips_extras.read_memory_tagged_functions,
-            Mips_extras.memory_writes,
-            Mips_extras.memory_eas,
-            Mips_extras.memory_vals,
-            Mips_extras.memory_vals_tagged,
-            Mips_extras.barrier_functions),
+           (Mips_extras.mips_read_memory_functions,
+            Mips_extras.mips_read_memory_tagged_functions,
+            Mips_extras.mips_memory_writes,
+            Mips_extras.mips_memory_eas,
+            Mips_extras.mips_memory_vals,
+            Mips_extras.mips_memory_vals_tagged,
+            Mips_extras.mips_barrier_functions),
            [],
            MIPS,
            D_decreasing,
diff --git a/src/lem_interp/sail_impl_base.lem b/src/lem_interp/sail_impl_base.lem
index f029b952..39ba0b5c 100644
--- a/src/lem_interp/sail_impl_base.lem
+++ b/src/lem_interp/sail_impl_base.lem
@@ -148,65 +148,20 @@ type opcode = Opcode of list byte (* of length 4 *)
 
 (** typeclass instantiations *)
 
-let ~{ocaml} bitCompare (b1:bit) (b2:bit) =
-  match (b1,b2) with
-  | (Bitc_zero, Bitc_zero) -> EQ
-  | (Bitc_one, Bitc_one) -> EQ
-  | (Bitc_zero, _) -> LT
-  | (_,_) -> GT
+instance (EnumerationType bit)
+  let toNat = function
+    | Bitc_zero -> 0
+    | Bitc_one -> 1
   end
-let inline {ocaml} bitCompare = defaultCompare
-
-let ~{ocaml} bitLess b1 b2      = bitCompare b1 b2 =  LT
-let ~{ocaml} bitLessEq b1 b2    = bitCompare b1 b2 <> GT
-let ~{ocaml} bitGreater b1 b2   = bitCompare b1 b2 =  GT
-let ~{ocaml} bitGreaterEq b1 b2 = bitCompare b1 b2 <> LT
-
-let inline {ocaml} bitLess      = defaultLess
-let inline {ocaml} bitLessEq    = defaultLessEq
-let inline {ocaml} bitGreater   = defaultGreater
-let inline {ocaml} bitGreaterEq = defaultGreaterEq
-
-instance (Ord bit)
-  let compare = bitCompare
-  let (<)  = bitLess
-  let (<=) = bitLessEq
-  let (>)  = bitGreater
-  let (>=) = bitGreaterEq
 end
 
-let ~{ocaml} bit_liftedCompare (bl1:bit_lifted) (bl2:bit_lifted) =
-  match (bl1,bl2) with
-  | (Bitl_zero, Bitl_zero) -> EQ
-  | (Bitl_zero,_) -> LT
-  | (Bitl_one, Bitl_zero) -> GT
-  | (Bitl_one, Bitl_one) -> EQ
-  | (Bitl_one, _) -> LT
-  | (Bitl_undef,Bitl_zero) -> GT
-  | (Bitl_undef,Bitl_one) -> GT
-  | (Bitl_undef,Bitl_undef) -> EQ
-  | (Bitl_undef,_) -> LT
-  | (Bitl_unknown,Bitl_unknown) -> EQ
-  | (Bitl_unknown,_) -> GT
+instance (EnumerationType bit_lifted)
+  let toNat = function
+    | Bitl_zero -> 0
+    | Bitl_one -> 1
+    | Bitl_undef -> 2
+    | Bitl_unknown -> 3
   end
-let inline {ocaml} bit_liftedCompare = defaultCompare
-
-let ~{ocaml} bit_liftedLess b1 b2      = bit_liftedCompare b1 b2 =  LT
-let ~{ocaml} bit_liftedLessEq b1 b2    = bit_liftedCompare b1 b2 <> GT
-let ~{ocaml} bit_liftedGreater b1 b2   = bit_liftedCompare b1 b2 =  GT
-let ~{ocaml} bit_liftedGreaterEq b1 b2 = bit_liftedCompare b1 b2 <> LT
-
-let inline {ocaml} bit_liftedLess      = defaultLess
-let inline {ocaml} bit_liftedLessEq    = defaultLessEq
-let inline {ocaml} bit_liftedGreater   = defaultGreater
-let inline {ocaml} bit_liftedGreaterEq = defaultGreaterEq
-
-instance (Ord bit_lifted)
-  let compare = bit_liftedCompare
-  let (<)  = bit_liftedLess
-  let (<=) = bit_liftedLessEq
-  let (>)  = bit_liftedGreater
-  let (>=) = bit_liftedGreaterEq
 end
 
 let ~{ocaml} byte_liftedCompare (Byte_lifted b1) (Byte_lifted b2) = compare b1 b2
@@ -251,6 +206,10 @@ instance (Ord byte)
   let (>=) = byteGreaterEq
 end
 
+
+
+
+
 let ~{ocaml} opcodeCompare (Opcode o1) (Opcode o2) =
   compare o1 o2
 let {ocaml} opcodeCompare = defaultCompare
@@ -1078,32 +1037,18 @@ end
 type nia = 
   | NIA_successor
   | NIA_concrete_address of address
-  | NIA_LR   (* "LR0:61 || 0b00" in Power pseudocode *)
-  | NIA_CTR  (* "CTR0:61 || 0b00" in Power pseudocode *)
-  | NIA_register of reg_name (* the address will be in a register,
-                                corresponds to AArch64 BLR, BR, RET
-                                instructions *)
+  | NIA_indirect_address
 
 let niaCompare n1 n2 = match (n1,n2) with
   | (NIA_successor, NIA_successor) -> EQ
   | (NIA_successor, _) -> LT
-  | (NIA_concrete_address _, NIA_successor) -> GT
+  | (_, NIA_successor) -> GT
   | (NIA_concrete_address a1, NIA_concrete_address a2) -> compare a1 a2
   | (NIA_concrete_address _, _) -> LT
-  | (NIA_LR, NIA_successor) -> GT
-  | (NIA_LR, NIA_concrete_address _) -> GT
-  | (NIA_LR, NIA_LR) -> EQ
-  | (NIA_LR, _) -> LT
-  | (NIA_CTR, NIA_successor) -> GT
-  | (NIA_CTR, NIA_concrete_address _) -> GT
-  | (NIA_CTR, NIA_LR) -> GT
-  | (NIA_CTR, NIA_CTR) -> EQ
-  | (NIA_CTR, NIA_register _) -> LT
-  | (NIA_register _, NIA_successor) -> GT
-  | (NIA_register _, NIA_concrete_address _) -> GT
-  | (NIA_register _, NIA_LR) -> GT
-  | (NIA_register _, NIA_CTR) -> GT
-  | (NIA_register r1, NIA_register r2) -> compare r1 r2
+  | (_, NIA_concrete_address _) -> GT
+  | (NIA_indirect_address, NIA_indirect_address) -> EQ
+  (* | (NIA_indirect_address, _) -> LT
+  | (_, NIA_indirect_address) -> GT *)
   end
 
 instance (Ord nia)
@@ -1115,11 +1060,9 @@ instance (Ord nia)
 end
 
 let stringFromNia = function
-  | NIA_successor -> "NIA_successor"
+  | NIA_successor          -> "NIA_successor"
   | NIA_concrete_address a -> "NIA_concrete_address " ^ show a
-  | NIA_LR -> "NIA_LR"
-  | NIA_CTR -> "NIA_CTR"
-  | NIA_register r -> "NIA_register " ^ show r
+  | NIA_indirect_address   -> "NIA_indirect_address"
 end
 
 instance (Show nia)
diff --git a/src/lem_interp/sail_instr_kinds.lem b/src/lem_interp/sail_instr_kinds.lem
index 89ff67b2..d8a2c0c0 100644
--- a/src/lem_interp/sail_instr_kinds.lem
+++ b/src/lem_interp/sail_instr_kinds.lem
@@ -50,6 +50,27 @@
 
 open import Pervasives_extra
 
+
+class ( EnumerationType 'a )
+  val toNat : 'a -> nat
+end
+
+
+val enumeration_typeCompare : forall 'a. EnumerationType 'a => 'a -> 'a -> ordering
+let ~{ocaml} enumeration_typeCompare e1 e2 =
+  compare (toNat e1) (toNat e2)
+let inline {ocaml} enumeration_typeCompare = defaultCompare
+
+
+default_instance forall 'a. EnumerationType 'a => (Ord 'a)
+  let compare = enumeration_typeCompare
+  let (<)  r1 r2 = (enumeration_typeCompare r1 r2) = LT
+  let (<=) r1 r2 = (enumeration_typeCompare r1 r2) <> GT
+  let (>)  r1 r2 = (enumeration_typeCompare r1 r2) = GT
+  let (>=) r1 r2 = (enumeration_typeCompare r1 r2) <> LT
+end
+
+
 (* Data structures for building up instructions *)
 
 (* careful: changes in the read/write/barrier kinds have to be
@@ -177,10 +198,9 @@ type instruction_kind =
   | IK_mem_read  of read_kind
   | IK_mem_write of write_kind
   | IK_mem_rmw   of (read_kind * write_kind)
-  | IK_cond_branch
-  (* unconditional branches are not distinguished in the instruction_kind;
-  they just have particular nias (and will be IK_simple *)
-  (* | IK_uncond_branch *)
+  | IK_branch (* this includes conditional-branch (multiple nias, none of which is NIA_indirect_address),
+  indirect/computed-branch (single nia of kind NIA_indirect_address)
+  and branch/jump (single nia of kind NIA_concrete_address) *)
   | IK_trans     of trans_kind
   | IK_simple
 
@@ -188,80 +208,16 @@ type instruction_kind =
 instance (Show instruction_kind)
   let show = function
     | IK_barrier barrier_kind -> "IK_barrier " ^ (show barrier_kind)
-    | IK_mem_read read_kind -> "IK_mem_read " ^ (show read_kind)
+    | IK_mem_read read_kind   -> "IK_mem_read " ^ (show read_kind)
     | IK_mem_write write_kind -> "IK_mem_write " ^ (show write_kind)
-    | IK_cond_branch -> "IK_cond_branch"
-    | IK_trans trans_kind -> "IK_trans " ^ (show trans_kind)
-    | IK_simple -> "IK_simple"
+    | IK_mem_rmw (r, w)       -> "IK_mem_rmw " ^ (show r) ^ " " ^ (show w)
+    | IK_branch               -> "IK_branch"
+    | IK_trans trans_kind     -> "IK_trans " ^ (show trans_kind)
+    | IK_simple               -> "IK_simple"
   end
 end
 
 
-
-let ~{ocaml} read_kindCompare rk1 rk2 =
-  match (rk1, rk2) with
-  | (Read_plain, Read_plain)             -> EQ
-  | (Read_plain, Read_reserve)           -> LT
-  | (Read_plain, Read_acquire)           -> LT
-  | (Read_plain, Read_exclusive)         -> LT
-  | (Read_plain, Read_exclusive_acquire) -> LT
-  | (Read_plain, Read_stream)            -> LT
-
-  | (Read_reserve, Read_plain)             -> GT
-  | (Read_reserve, Read_reserve)           -> EQ
-  | (Read_reserve, Read_acquire)           -> LT
-  | (Read_reserve, Read_exclusive)         -> LT
-  | (Read_reserve, Read_exclusive_acquire) -> LT
-  | (Read_reserve, Read_stream)            -> LT
-
-  | (Read_acquire, Read_plain)             -> GT
-  | (Read_acquire, Read_reserve)           -> GT
-  | (Read_acquire, Read_acquire)           -> EQ
-  | (Read_acquire, Read_exclusive)         -> LT
-  | (Read_acquire, Read_exclusive_acquire) -> LT
-  | (Read_acquire, Read_stream)            -> LT
-
-  | (Read_exclusive, Read_plain)             -> GT
-  | (Read_exclusive, Read_reserve)           -> GT
-  | (Read_exclusive, Read_acquire)           -> GT
-  | (Read_exclusive, Read_exclusive)         -> EQ
-  | (Read_exclusive, Read_exclusive_acquire) -> LT
-  | (Read_exclusive, Read_stream)            -> LT
-
-  | (Read_exclusive_acquire, Read_plain)             -> GT
-  | (Read_exclusive_acquire, Read_reserve)           -> GT
-  | (Read_exclusive_acquire, Read_acquire)           -> GT
-  | (Read_exclusive_acquire, Read_exclusive)         -> GT
-  | (Read_exclusive_acquire, Read_exclusive_acquire) -> EQ
-  | (Read_exclusive_acquire, Read_stream)            -> GT
-
-  | (Read_stream, Read_plain)             -> GT
-  | (Read_stream, Read_reserve)           -> GT
-  | (Read_stream, Read_acquire)           -> GT
-  | (Read_stream, Read_exclusive)         -> GT
-  | (Read_stream, Read_exclusive_acquire) -> GT
-  | (Read_stream, Read_stream)            -> EQ
-end
-let inline {ocaml} read_kindCompare = defaultCompare
-
-let ~{ocaml} read_kindLess b1 b2      = read_kindCompare b1 b2 =  LT
-let ~{ocaml} read_kindLessEq b1 b2    = read_kindCompare b1 b2 <> GT
-let ~{ocaml} read_kindGreater b1 b2   = read_kindCompare b1 b2 =  GT
-let ~{ocaml} read_kindGreaterEq b1 b2 = read_kindCompare b1 b2 <> LT
-
-let inline {ocaml} read_kindLess      = defaultLess
-let inline {ocaml} read_kindLessEq    = defaultLessEq
-let inline {ocaml} read_kindGreater   = defaultGreater
-let inline {ocaml} read_kindGreaterEq = defaultGreaterEq
-
-instance (Ord read_kind)
-  let compare = read_kindCompare
-  let (<)  = read_kindLess
-  let (<=) = read_kindLessEq
-  let (>)  = read_kindGreater
-  let (>=) = read_kindGreaterEq
-end
-
 let read_is_exclusive = function
   | Read_plain -> false
   | Read_reserve -> true
@@ -277,63 +233,46 @@ let read_is_exclusive = function
   | Read_X86_locked -> true
 end
 
-let ~{ocaml} write_kindCompare wk1 wk2 =
-  match (wk1, wk2) with
-  | (Write_plain, Write_plain)             -> EQ
-  | (Write_plain, Write_conditional)       -> LT
-  | (Write_plain, Write_release)           -> LT
-  | (Write_plain, Write_exclusive)         -> LT
-  | (Write_plain, Write_exclusive_release) -> LT
-
-  | (Write_conditional, Write_plain)             -> GT
-  | (Write_conditional, Write_conditional)       -> EQ
-  | (Write_conditional, Write_release)           -> LT
-  | (Write_conditional, Write_exclusive)         -> LT
-  | (Write_conditional, Write_exclusive_release) -> LT
-
-  | (Write_release, Write_plain)             -> GT
-  | (Write_release, Write_conditional)       -> GT
-  | (Write_release, Write_release)           -> EQ
-  | (Write_release, Write_exclusive)         -> LT
-  | (Write_release, Write_exclusive_release) -> LT
 
-  | (Write_exclusive, Write_plain)             -> GT
-  | (Write_exclusive, Write_conditional)       -> GT
-  | (Write_exclusive, Write_release)           -> GT
-  | (Write_exclusive, Write_exclusive)         -> EQ
-  | (Write_exclusive, Write_exclusive_release) -> LT
 
-  | (Write_exclusive_release, Write_plain)             -> GT
-  | (Write_exclusive_release, Write_conditional)       -> GT
-  | (Write_exclusive_release, Write_release)           -> GT
-  | (Write_exclusive_release, Write_exclusive)         -> GT
-  | (Write_exclusive_release, Write_exclusive_release) -> EQ
+instance (EnumerationType read_kind)
+  let toNat = function
+    | Read_plain -> 0
+    | Read_reserve -> 1
+    | Read_acquire -> 2
+    | Read_exclusive -> 3
+    | Read_exclusive_acquire -> 4
+    | Read_stream -> 5
+    | Read_RISCV_acquire -> 6
+    | Read_RISCV_strong_acquire -> 7
+    | Read_RISCV_reserved -> 8
+    | Read_RISCV_reserved_acquire -> 9
+    | Read_RISCV_reserved_strong_acquire -> 10
+    | Read_X86_locked -> 11
+  end
 end
-let inline {ocaml} write_kindCompare = defaultCompare
-
-let ~{ocaml} write_kindLess b1 b2      = write_kindCompare b1 b2 =  LT
-let ~{ocaml} write_kindLessEq b1 b2    = write_kindCompare b1 b2 <> GT
-let ~{ocaml} write_kindGreater b1 b2   = write_kindCompare b1 b2 =  GT
-let ~{ocaml} write_kindGreaterEq b1 b2 = write_kindCompare b1 b2 <> LT
-
-let inline {ocaml} write_kindLess      = defaultLess
-let inline {ocaml} write_kindLessEq    = defaultLessEq
-let inline {ocaml} write_kindGreater   = defaultGreater
-let inline {ocaml} write_kindGreaterEq = defaultGreaterEq
 
-instance (Ord write_kind)
-  let compare = write_kindCompare
-  let (<)  = write_kindLess
-  let (<=) = write_kindLessEq
-  let (>)  = write_kindGreater
-  let (>=) = write_kindGreaterEq
+instance (EnumerationType write_kind)
+  let toNat = function
+    | Write_plain -> 0
+    | Write_conditional -> 1
+    | Write_release -> 2
+    | Write_exclusive -> 3
+    | Write_exclusive_release -> 4
+    | Write_RISCV_release -> 5
+    | Write_RISCV_strong_release -> 6
+    | Write_RISCV_conditional -> 7
+    | Write_RISCV_conditional_release -> 8
+    | Write_RISCV_conditional_strong_release -> 9
+    | Write_X86_locked -> 10
+  end
 end
 
-(* Barrier comparison that uses less memory in Isabelle/HOL *)
-let ~{ocaml} barrier_number = function
-    | Barrier_Sync -> (0 : natural)
+instance (EnumerationType barrier_kind)
+  let toNat = function
+    | Barrier_Sync -> 0
     | Barrier_LwSync -> 1
-    | Barrier_Eieio -> 2
+    | Barrier_Eieio ->2
     | Barrier_Isync -> 3
     | Barrier_DMB -> 4
     | Barrier_DMB_ST -> 5
@@ -352,85 +291,4 @@ let ~{ocaml} barrier_number = function
     | Barrier_RISCV_i -> 18
     | Barrier_x86_MFENCE -> 19
   end
-
-let ~{ocaml} barrier_kindCompare bk1 bk2 =
-  let n1 = barrier_number bk1 in
-  let n2 = barrier_number bk2 in
-  if n1 < n2 then LT
-  else if n1 = n2 then EQ
-  else GT
-let inline {ocaml} barrier_kindCompare = defaultCompare
-
-(*let ~{ocaml} barrier_kindCompare bk1 bk2 =
-  match (bk1, bk2) with
-  | (Barrier_Sync, Barrier_Sync) -> EQ
-  | (Barrier_Sync, _) -> LT
-  | (_, Barrier_Sync) -> GT
-
-  | (Barrier_LwSync, Barrier_LwSync) -> EQ
-  | (Barrier_LwSync, _) -> LT
-  | (_, Barrier_LwSync) -> GT
-
-  | (Barrier_Eieio, Barrier_Eieio) -> EQ
-  | (Barrier_Eieio, _) -> LT
-  | (_, Barrier_Eieio) -> GT
-
-  | (Barrier_Isync, Barrier_Isync) -> EQ
-  | (Barrier_Isync, _) -> LT
-  | (_, Barrier_Isync) -> GT
-
-  | (Barrier_DMB, Barrier_DMB) -> EQ
-  | (Barrier_DMB, _) -> LT
-  | (_, Barrier_DMB) -> GT
-
-  | (Barrier_DMB_ST, Barrier_DMB_ST) -> EQ
-  | (Barrier_DMB_ST, _) -> LT
-  | (_, Barrier_DMB_ST) -> GT
-
-  | (Barrier_DMB_LD, Barrier_DMB_LD) -> EQ
-  | (Barrier_DMB_LD, _) -> LT
-  | (_, Barrier_DMB_LD) -> GT
-
-  | (Barrier_DSB, Barrier_DSB) -> EQ
-  | (Barrier_DSB, _) -> LT
-  | (_, Barrier_DSB) -> GT
-
-  | (Barrier_DSB_ST, Barrier_DSB_ST) -> EQ
-  | (Barrier_DSB_ST, _) -> LT
-  | (_, Barrier_DSB_ST) -> GT
-
-  | (Barrier_DSB_LD, Barrier_DSB_LD) -> EQ
-  | (Barrier_DSB_LD, _) -> LT
-  | (_, Barrier_DSB_LD) -> GT
-
-  | (Barrier_ISB, Barrier_ISB) -> EQ
-  | (Barrier_ISB, _) -> LT
-  | (_, Barrier_ISB) -> GT
-
-  | (Barrier_TM_COMMIT, Barrier_TM_COMMIT) -> EQ
-  | (Barrier_TM_COMMIT, _) -> LT
-  | (_, Barrier_TM_COMMIT) -> GT
-
-  | (Barrier_MIPS_SYNC, Barrier_MIPS_SYNC) -> EQ
-  (* | (Barrier_MIPS_SYNC, _) -> LT
-  | (_, Barrier_MIPS_SYNC) -> GT *)
-
-  end*)
-
-let ~{ocaml} barrier_kindLess b1 b2      = barrier_kindCompare b1 b2 =  LT
-let ~{ocaml} barrier_kindLessEq b1 b2    = barrier_kindCompare b1 b2 <> GT
-let ~{ocaml} barrier_kindGreater b1 b2   = barrier_kindCompare b1 b2 =  GT
-let ~{ocaml} barrier_kindGreaterEq b1 b2 = barrier_kindCompare b1 b2 <> LT
-
-let inline {ocaml} barrier_kindLess      = defaultLess
-let inline {ocaml} barrier_kindLessEq    = defaultLessEq
-let inline {ocaml} barrier_kindGreater   = defaultGreater
-let inline {ocaml} barrier_kindGreaterEq = defaultGreaterEq
-
-instance (Ord barrier_kind)
-  let compare = barrier_kindCompare
-  let (<)  = barrier_kindLess
-  let (<=) = barrier_kindLessEq
-  let (>)  = barrier_kindGreater
-  let (>=) = barrier_kindGreaterEq
 end
diff --git a/src/pprint/src/META b/src/pprint/src/META
index b7d43d40..4a966166 100755
--- a/src/pprint/src/META
+++ b/src/pprint/src/META
@@ -2,4 +2,4 @@ requires = ""
 description = "The PPrint pretty-printing library"
 archive(byte) = "PPrintLib.cma"
 archive(native) = "PPrintLib.cmxa"
-version = "20140424"
+version = "20171003"
diff --git a/src/pprint/src/Makefile b/src/pprint/src/Makefile
index f56f4d88..3bfa12df 100644
--- a/src/pprint/src/Makefile
+++ b/src/pprint/src/Makefile
@@ -1,6 +1,6 @@
-.PHONY: all install clean doc test
+.PHONY: all install uninstall reinstall clean doc test bench
 
-OCAMLBUILD := ocamlbuild -use-ocamlfind -cflags "-g" -lflags "-g" -classic-display
+OCAMLBUILD := ocamlbuild -use-ocamlfind -classic-display
 OCAMLFIND  := ocamlfind
 DOCDIR     := doc
 MAIN       := PPrintTest
@@ -14,6 +14,14 @@ install: all
 		$(patsubst %,_build/%,$(TO_BUILD)) \
 		_build/PPrintLib.a _build/*.cmx _build/*.cmi
 
+# [make uninstall] attempts to uninstall, but succeeds even if uninstallation
+# fails (probably because the package was not installed in the first place).
+uninstall:
+	ocamlfind remove pprint || true
+
+reinstall: uninstall
+	@ $(MAKE) install
+
 clean:
 	rm -f *~
 	rm -rf doc
@@ -33,3 +41,6 @@ test: all
 	$(OCAMLBUILD) $(MAIN).native
 	./$(MAIN).native
 
+bench: all
+	$(OCAMLBUILD) -tag use_unix PPrintBench.native
+	time ./PPrintBench.native
diff --git a/src/pprint/src/PPrint.ml b/src/pprint/src/PPrint.ml
index ae1ff709..46d732b1 100644
--- a/src/pprint/src/PPrint.ml
+++ b/src/pprint/src/PPrint.ml
@@ -2,12 +2,12 @@
 (*                                                                        *)
 (*  PPrint                                                                *)
 (*                                                                        *)
-(*  Francois Pottier, INRIA Paris-Rocquencourt                            *)
-(*  Nicolas Pouillard, IT University of Copenhagen                        *)
+(*  François Pottier, Inria Paris                                         *)
+(*  Nicolas Pouillard                                                     *)
 (*                                                                        *)
-(*  Copyright 2007-2014 INRIA. All rights reserved. This file is          *)
-(*  distributed under the terms of the CeCILL-C license, as described     *)
-(*  in the file LICENSE.                                                  *)
+(*  Copyright 2007-2017 Inria. All rights reserved. This file is          *)
+(*  distributed under the terms of the GNU Library General Public         *)
+(*  License, with an exception, as described in the file LICENSE.         *)
 (*                                                                        *)
 (**************************************************************************)
 
diff --git a/src/pprint/src/PPrintCombinators.ml b/src/pprint/src/PPrintCombinators.ml
index 39b99b9c..70499878 100644
--- a/src/pprint/src/PPrintCombinators.ml
+++ b/src/pprint/src/PPrintCombinators.ml
@@ -2,12 +2,12 @@
 (*                                                                        *)
 (*  PPrint                                                                *)
 (*                                                                        *)
-(*  Francois Pottier, INRIA Paris-Rocquencourt                            *)
-(*  Nicolas Pouillard, IT University of Copenhagen                        *)
+(*  François Pottier, Inria Paris                                         *)
+(*  Nicolas Pouillard                                                     *)
 (*                                                                        *)
-(*  Copyright 2007-2014 INRIA. All rights reserved. This file is          *)
-(*  distributed under the terms of the CeCILL-C license, as described     *)
-(*  in the file LICENSE.                                                  *)
+(*  Copyright 2007-2017 Inria. All rights reserved. This file is          *)
+(*  distributed under the terms of the GNU Library General Public         *)
+(*  License, with an exception, as described in the file LICENSE.         *)
 (*                                                                        *)
 (**************************************************************************)
 
diff --git a/src/pprint/src/PPrintCombinators.mli b/src/pprint/src/PPrintCombinators.mli
index ef2b44ea..c538cb35 100644
--- a/src/pprint/src/PPrintCombinators.mli
+++ b/src/pprint/src/PPrintCombinators.mli
@@ -2,12 +2,12 @@
 (*                                                                        *)
 (*  PPrint                                                                *)
 (*                                                                        *)
-(*  Francois Pottier, INRIA Paris-Rocquencourt                            *)
-(*  Nicolas Pouillard, IT University of Copenhagen                        *)
+(*  François Pottier, Inria Paris                                         *)
+(*  Nicolas Pouillard                                                     *)
 (*                                                                        *)
-(*  Copyright 2007-2014 INRIA. All rights reserved. This file is          *)
-(*  distributed under the terms of the CeCILL-C license, as described     *)
-(*  in the file LICENSE.                                                  *)
+(*  Copyright 2007-2017 Inria. All rights reserved. This file is          *)
+(*  distributed under the terms of the GNU Library General Public         *)
+(*  License, with an exception, as described in the file LICENSE.         *)
 (*                                                                        *)
 (**************************************************************************)
 
@@ -133,7 +133,7 @@ val words: string -> document list
     character that satisfies the predicate [ok]. The substrings thus obtained
     are turned into documents, and a list of documents is returned. No
     information is lost: the concatenation of the documents yields the
-    original string.  This code is not UTF-8 aware. *)
+    original string. This code is not UTF-8 aware. *)
 val split: (char -> bool) -> string -> document list
 
 (** [flow sep docs] separates the documents in the list [docs] with the
diff --git a/src/pprint/src/PPrintEngine.ml b/src/pprint/src/PPrintEngine.ml
index cfa8474a..2a78363d 100644
--- a/src/pprint/src/PPrintEngine.ml
+++ b/src/pprint/src/PPrintEngine.ml
@@ -2,12 +2,12 @@
 (*                                                                        *)
 (*  PPrint                                                                *)
 (*                                                                        *)
-(*  Francois Pottier, INRIA Paris-Rocquencourt                            *)
-(*  Nicolas Pouillard, IT University of Copenhagen                        *)
+(*  François Pottier, Inria Paris                                         *)
+(*  Nicolas Pouillard                                                     *)
 (*                                                                        *)
-(*  Copyright 2007-2014 INRIA. All rights reserved. This file is          *)
-(*  distributed under the terms of the CeCILL-C license, as described     *)
-(*  in the file LICENSE.                                                  *)
+(*  Copyright 2007-2017 Inria. All rights reserved. This file is          *)
+(*  distributed under the terms of the GNU Library General Public         *)
+(*  License, with an exception, as described in the file LICENSE.         *)
 (*                                                                        *)
 (**************************************************************************)
 
@@ -57,7 +57,13 @@ end
 
 class channel_output channel = object
   method char = output_char channel
-  method substring = output channel
+  method substring = output_substring channel
+    (* We used to use [output], but, as of OCaml 4.02 and with -safe-string
+       enabled, the type of [output] has changed: this function now expects
+       an argument of type [bytes]. The new function [output_substring] must
+       be used instead. Furthermore, as of OCaml 4.06, -safe-string is enabled
+       by default. In summary, we require OCaml 4.02, use [output_substring],
+       and enable -safe-string. *)
 end
 
 class buffer_output buffer = object
@@ -152,21 +158,21 @@ end
 
 type document =
 
-    (* [Empty] is the empty document. *)
+  (* [Empty] is the empty document. *)
 
   | Empty
 
-    (* [Char c] is a document that consists of the single character [c]. We
-       enforce the invariant that [c] is not a newline character. *)
+  (* [Char c] is a document that consists of the single character [c]. We
+     enforce the invariant that [c] is not a newline character. *)
 
   | Char of char
 
-    (* [String (s, ofs, len)] is a document that consists of the portion of
-       the string [s] delimited by the offset [ofs] and the length [len]. We
-       assume, but do not check, that this portion does not contain a newline
-       character. *)
+  (* [String s] is a document that consists of just the string [s]. We
+     assume, but do not check, that this string does not contain a newline
+     character. [String] is a special case of [FancyString], which takes up
+     less space in memory. *)
 
-  | String of string * int * int
+  | String of string
 
   (* [FancyString (s, ofs, len, apparent_length)] is a (portion of a) string
      that may contain fancy characters: color escape characters, UTF-8 or
@@ -252,7 +258,8 @@ let rec requirement = function
       0
   | Char _ ->
       1
-  | String (_, _, len)
+  | String s ->
+      String.length s
   | FancyString (_, _, _, len)
   | Blank len ->
       len
@@ -268,7 +275,7 @@ let rec requirement = function
       infinity
   | Cat (req, _, _)
   | Nest (req, _, _)
-  | Group (req, _) 
+  | Group (req, _)
   | Align (req, _) ->
       (* These nodes store their requirement -- which is computed when the
          node is constructed -- so as to allow us to answer in constant time
@@ -293,14 +300,8 @@ let char c =
 let space =
   char ' '
 
-let substring s ofs len =
-  if len = 0 then
-    empty
-  else
-    String (s, ofs, len)
-
 let string s =
-  substring s 0 (String.length s)
+  String s
 
 let fancysubstring s ofs len apparent_length =
   if len = 0 then
@@ -308,6 +309,9 @@ let fancysubstring s ofs len apparent_length =
   else
     FancyString (s, ofs, len, apparent_length)
 
+let substring s ofs len =
+  fancysubstring s ofs len len
+
 let fancystring s apparent_length =
   fancysubstring s 0 (String.length s) apparent_length
 
@@ -467,8 +471,9 @@ let rec pretty
       (* assert (ok state flatten); *)
       continue output state cont
 
-  | String (s, ofs, len) ->
-      output#substring s ofs len;
+  | String s ->
+      let len = String.length s in
+      output#substring s 0 len;
       state.column <- state.column + len;
       (* assert (ok state flatten); *)
       continue output state cont
@@ -566,8 +571,9 @@ let rec compact output doc cont =
   | Char c ->
       output#char c;
       continue output cont
-  | String (s, ofs, len) ->
-      output#substring s ofs len;
+  | String s ->
+      let len = String.length s in
+      output#substring s 0 len;
       continue output cont
   | FancyString (s, ofs, len, apparent_length) ->
       output#substring s ofs len;
@@ -634,4 +640,3 @@ module ToFormatter =
     type channel = Format.formatter
     let output = new formatter_output
   end)
-
diff --git a/src/pprint/src/PPrintEngine.mli b/src/pprint/src/PPrintEngine.mli
index 7f6fcf35..eda61a6c 100644
--- a/src/pprint/src/PPrintEngine.mli
+++ b/src/pprint/src/PPrintEngine.mli
@@ -2,12 +2,12 @@
 (*                                                                        *)
 (*  PPrint                                                                *)
 (*                                                                        *)
-(*  Francois Pottier, INRIA Paris-Rocquencourt                            *)
-(*  Nicolas Pouillard, IT University of Copenhagen                        *)
+(*  François Pottier, Inria Paris                                         *)
+(*  Nicolas Pouillard                                                     *)
 (*                                                                        *)
-(*  Copyright 2007-2014 INRIA. All rights reserved. This file is          *)
-(*  distributed under the terms of the CeCILL-C license, as described     *)
-(*  in the file LICENSE.                                                  *)
+(*  Copyright 2007-2017 Inria. All rights reserved. This file is          *)
+(*  distributed under the terms of the GNU Library General Public         *)
+(*  License, with an exception, as described in the file LICENSE.         *)
 (*                                                                        *)
 (**************************************************************************)
 
diff --git a/src/pprint/src/PPrintOCaml.ml b/src/pprint/src/PPrintOCaml.ml
index 88e039ce..bee5f2a3 100644
--- a/src/pprint/src/PPrintOCaml.ml
+++ b/src/pprint/src/PPrintOCaml.ml
@@ -2,12 +2,12 @@
 (*                                                                        *)
 (*  PPrint                                                                *)
 (*                                                                        *)
-(*  Francois Pottier, INRIA Paris-Rocquencourt                            *)
-(*  Nicolas Pouillard, IT University of Copenhagen                        *)
+(*  François Pottier, Inria Paris                                         *)
+(*  Nicolas Pouillard                                                     *)
 (*                                                                        *)
-(*  Copyright 2007-2014 INRIA. All rights reserved. This file is          *)
-(*  distributed under the terms of the CeCILL-C license, as described     *)
-(*  in the file LICENSE.                                                  *)
+(*  Copyright 2007-2017 Inria. All rights reserved. This file is          *)
+(*  distributed under the terms of the GNU Library General Public         *)
+(*  License, with an exception, as described in the file LICENSE.         *)
 (*                                                                        *)
 (**************************************************************************)
 
diff --git a/src/pprint/src/PPrintOCaml.mli b/src/pprint/src/PPrintOCaml.mli
index e1395203..119bca23 100644
--- a/src/pprint/src/PPrintOCaml.mli
+++ b/src/pprint/src/PPrintOCaml.mli
@@ -2,12 +2,12 @@
 (*                                                                        *)
 (*  PPrint                                                                *)
 (*                                                                        *)
-(*  Francois Pottier, INRIA Paris-Rocquencourt                            *)
-(*  Nicolas Pouillard, IT University of Copenhagen                        *)
+(*  François Pottier, Inria Paris                                         *)
+(*  Nicolas Pouillard                                                     *)
 (*                                                                        *)
-(*  Copyright 2007-2014 INRIA. All rights reserved. This file is          *)
-(*  distributed under the terms of the CeCILL-C license, as described     *)
-(*  in the file LICENSE.                                                  *)
+(*  Copyright 2007-2017 Inria. All rights reserved. This file is          *)
+(*  distributed under the terms of the GNU Library General Public         *)
+(*  License, with an exception, as described in the file LICENSE.         *)
 (*                                                                        *)
 (**************************************************************************)
 
diff --git a/src/pprint/src/PPrintRenderer.ml b/src/pprint/src/PPrintRenderer.ml
index 9096eada..3449d6c3 100644
--- a/src/pprint/src/PPrintRenderer.ml
+++ b/src/pprint/src/PPrintRenderer.ml
@@ -2,12 +2,12 @@
 (*                                                                        *)
 (*  PPrint                                                                *)
 (*                                                                        *)
-(*  Francois Pottier, INRIA Paris-Rocquencourt                            *)
-(*  Nicolas Pouillard, IT University of Copenhagen                        *)
+(*  François Pottier, Inria Paris                                         *)
+(*  Nicolas Pouillard                                                     *)
 (*                                                                        *)
-(*  Copyright 2007-2014 INRIA. All rights reserved. This file is          *)
-(*  distributed under the terms of the CeCILL-C license, as described     *)
-(*  in the file LICENSE.                                                  *)
+(*  Copyright 2007-2017 Inria. All rights reserved. This file is          *)
+(*  distributed under the terms of the GNU Library General Public         *)
+(*  License, with an exception, as described in the file LICENSE.         *)
 (*                                                                        *)
 (**************************************************************************)
 
diff --git a/src/pprint/src/PPrintTest.ml b/src/pprint/src/PPrintTest.ml
index 3e4fb2c9..37444127 100644
--- a/src/pprint/src/PPrintTest.ml
+++ b/src/pprint/src/PPrintTest.ml
@@ -2,12 +2,12 @@
 (*                                                                        *)
 (*  PPrint                                                                *)
 (*                                                                        *)
-(*  Francois Pottier, INRIA Paris-Rocquencourt                            *)
-(*  Nicolas Pouillard, IT University of Copenhagen                        *)
+(*  François Pottier, Inria Paris                                         *)
+(*  Nicolas Pouillard                                                     *)
 (*                                                                        *)
-(*  Copyright 2007-2014 INRIA. All rights reserved. This file is          *)
-(*  distributed under the terms of the CeCILL-C license, as described     *)
-(*  in the file LICENSE.                                                  *)
+(*  Copyright 2007-2017 Inria. All rights reserved. This file is          *)
+(*  distributed under the terms of the GNU Library General Public         *)
+(*  License, with an exception, as described in the file LICENSE.         *)
 (*                                                                        *)
 (**************************************************************************)
 
diff --git a/src/reporting_basic.ml b/src/reporting_basic.ml
index fce7137d..1fc4fc6c 100644
--- a/src/reporting_basic.ml
+++ b/src/reporting_basic.ml
@@ -217,9 +217,9 @@ let format_loc_source ff l =
     begin
       let (s, multi_line) = read_from_file_pos2 p1 p2 in
       if multi_line then 
-        Format.fprintf ff "  original input:\n%s\n" s
+        Format.fprintf ff "  original input:\n%s\n" (Bytes.to_string s)
       else
-        Format.fprintf ff "  original input: \"%s\"\n" s
+        Format.fprintf ff "  original input: \"%s\"\n" (Bytes.to_string s)
     end
   | _ -> ()
 
diff --git a/src/test/lib/Makefile b/src/test/lib/Makefile
index d2185866..fbd5a332 100644
--- a/src/test/lib/Makefile
+++ b/src/test/lib/Makefile
@@ -8,11 +8,8 @@ TESTS=div.sail
 BITBUCKET_DIR:=$(realpath ../../../../)
 LEM_DIR:=$(BITBUCKET_DIR)/lem
 LEM:=$(LEM_DIR)/lem
-LEMLIB = $(LEM_DIR)/ocaml-lib
 SAIL_DIR:=$(BITBUCKET_DIR)/sail/src
 SAIL:=$(SAIL_DIR)/sail.native
-ZARITH_DIR:=$(LEM_DIR)/ocaml-lib/dependencies/zarith
-ZARITH_LIB:=$(ZARITH_DIR)/zarith.cmxa
 SAIL_VALUES:=$(SAIL_DIR)/gen_lib/sail_values.ml
 
 BUILD_DIR:=_build
@@ -41,14 +38,14 @@ $(BUILD_DIR)/sail_values.ml: | $(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 && \
-	ocamlopt -I $(ZARITH_DIR) $(ZARITH_LIB) sail_values.ml test.ml run_test_embed.ml -o test_embed.native && \
+	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 -I $(ZARITH_DIR)  -I $(SAIL_DIR)/_build/lem_interp -I $(LEMLIB) -linkpkg $(ZARITH_LIB) $(LEMLIB)/extract.cmxa  $(SAIL_DIR)/_build/lem_interp/extract.cmxa test_lem_ast.ml run_test_interp.ml -o test_interp.native && \
+	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)
diff --git a/src/util.ml b/src/util.ml
index a627fd58..b44c5dfb 100644
--- a/src/util.ml
+++ b/src/util.ml
@@ -327,7 +327,7 @@ module ExtraSet = functor (S : Set.S) ->
 
 let copy_file src dst = 
   let len = 5096 in
-  let b = String.make len ' ' in
+  let b = Bytes.make len ' ' in
   let read_len = ref 0 in
   let i = open_in_bin src in
   let o = open_out_bin dst  in
diff --git a/x86/x64.sail b/x86/x64.sail
index 9fa0b838..3549b123 100644
--- a/x86/x64.sail
+++ b/x86/x64.sail
@@ -1457,8 +1457,7 @@ function (regfps,regfps,regfps,niafps,diafp,instruction_kind) initial_analysis (
           oR := RFull("RSP") :: oR;
           aR := ars;
           Nias := switch irm {
-          (* XXX register name is not important here -- just indicates we don't know the destination yet. *)
-            case (Rm (v))  -> NIAFP_register(RFull("RAX"))
+            case (Rm (v))  -> NIAFP_indirect_address
             case (Imm (v)) -> NIAFP_concrete_address(RIP + v)
           } :: Nias;
       }
@@ -1486,7 +1485,7 @@ function (regfps,regfps,regfps,niafps,diafp,instruction_kind) initial_analysis (
     case(HLT                          ) -> ()
     case(Jcc     (c, imm64)           ) -> 
       let flags = regfp_cond(c) in {
-        ik := IK_cond_branch;
+        ik := IK_branch;
         iR := RFull("RIP") :: flags;
         Nias :=  NIAFP_concrete_address(RIP + imm64) :: Nias;
       }
@@ -1495,8 +1494,7 @@ function (regfps,regfps,regfps,niafps,diafp,instruction_kind) initial_analysis (
         ik := if m then IK_mem_read(Read_plain) else IK_simple;
         iR := RFull("RIP")::append(rs, ars);
         aR := ars;
-        (* XXX register name is not important here -- just indicates we don't know the destination yet. *)
-        Nias := NIAFP_register(RFull("RAX")) :: Nias;
+        Nias := NIAFP_indirect_address :: Nias;
       }
     case(LEA     (sz, ds)             ) ->
       let (_, irs, ors, ars) = regfp_dest_src (ds) in {
@@ -1512,7 +1510,7 @@ function (regfps,regfps,regfps,niafps,diafp,instruction_kind) initial_analysis (
     }
     case(LOOP    (c, imm64)           ) -> 
       let flags = regfp_cond(c) in {
-          ik := IK_cond_branch;
+          ik := IK_branch;
           iR := RFull("RCX") :: flags;
           oR := RFull("RCX") :: oR;
           Nias := NIAFP_concrete_address(RIP + imm64) :: Nias;
@@ -1578,8 +1576,7 @@ function (regfps,regfps,regfps,niafps,diafp,instruction_kind) initial_analysis (
       iR := RFull("RSP") :: iR;
       oR := RFull("RSP") :: oR;
       aR := RFull("RSP") :: aR;
-      (* XXX register name is not important here -- just indicates we don't know the destination yet. *)
-      Nias := NIAFP_register(RFull("RAX")) :: Nias;
+      Nias := NIAFP_indirect_address :: Nias;
     }
     case(SET     (c, b, r_m)          ) -> 
       let flags = regfp_cond(c) in