Merge master branch into sail2 for OCaml 4.06 compatibility

24 files changed, 266 insertions, 460 deletions

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