summaryrefslogtreecommitdiff
path: root/src
diff options
context:
space:
mode:
Diffstat (limited to 'src')
-rw-r--r--src/Makefile6
-rw-r--r--src/lem_interp/run_with_elf.ml12
-rw-r--r--src/lem_interp/run_with_elf_cheri.ml16
-rw-r--r--src/lem_interp/run_with_elf_cheri128.ml16
4 files changed, 25 insertions, 25 deletions
diff --git a/src/Makefile b/src/Makefile
index 931d9a39..44d1b8b2 100644
--- a/src/Makefile
+++ b/src/Makefile
@@ -213,13 +213,13 @@ count: _build/cheri_trimmed.sail _build/mips_trimmed.sail
$(LEM) -only_changed_output -ocaml -lib lem_interp/ $<
run_mips.native: _build/mips.ml _build/mips_extras.ml _build/run_with_elf.ml interpreter
- env OCAMLRUNPARAM=l=100M ocamlfind ocamlopt $(OCAML_OPTS) -g -package num -package lem -package zarith -package str -package unix -I $(ELFDIR)/contrib/ocaml-uint/_build/lib -I _build/lem_interp/ -I $(ELFDIR)/src -I $(ELFDIR)/src/adaptors -I $(ELFDIR)/src/abis/mips64 -I _build -linkpkg $(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
+ 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 lem -package zarith -package str -package unix -I $(ELFDIR)/contrib/ocaml-uint/_build/lib -I _build/lem_interp/ -I $(ELFDIR)/src -I $(ELFDIR)/src/adaptors -I $(ELFDIR)/src/abis/mips64 -I _build -linkpkg $(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 lem -package zarith -package str -package unix -I $(ELFDIR)/contrib/ocaml-uint/_build/lib -I _build/lem_interp/ -I $(ELFDIR)/src -I $(ELFDIR)/src/adaptors -I $(ELFDIR)/src/abis/mips64 -I _build -linkpkg $(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 zarith -package unix -I _build -linkpkg $^ -o $@
diff --git a/src/lem_interp/run_with_elf.ml b/src/lem_interp/run_with_elf.ml
index 8533827b..0dadc007 100644
--- a/src/lem_interp/run_with_elf.ml
+++ b/src/lem_interp/run_with_elf.ml
@@ -727,7 +727,7 @@ let initial_system_state_of_elf_file name =
aarch64_register_data_all) *)
| 8 (* EM_MIPS *) ->
let startaddr =
- let e_entry = Uint64.of_string (Nat_big_num.to_string e_entry) in
+ let e_entry = Uint64_wrapper.of_bigint e_entry in
match Abi_mips64.abi_mips64_compute_program_entry_point segments e_entry with
| Error.Fail s -> failwith "Failed computing entry point"
| Error.Success s -> s
@@ -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 46bc92fb..2bf84e2d 100644
--- a/src/lem_interp/run_with_elf_cheri.ml
+++ b/src/lem_interp/run_with_elf_cheri.ml
@@ -396,7 +396,7 @@ let initial_system_state_of_elf_file name =
match Nat_big_num.to_int e_machine with
| 8 (* EM_MIPS *) ->
let startaddr =
- let e_entry = Uint64.of_string (Nat_big_num.to_string e_entry) in
+ let e_entry = Uint64_wrapper.of_bigint e_entry in
match Abi_mips64.abi_mips64_compute_program_entry_point segments e_entry with
| Error.Fail s -> failwith "Failed computing entry point"
| Error.Success s -> s
@@ -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 5e5bee21..e4d91c41 100644
--- a/src/lem_interp/run_with_elf_cheri128.ml
+++ b/src/lem_interp/run_with_elf_cheri128.ml
@@ -396,7 +396,7 @@ let initial_system_state_of_elf_file name =
match Nat_big_num.to_int e_machine with
| 8 (* EM_MIPS *) ->
let startaddr =
- let e_entry = Uint64.of_string (Nat_big_num.to_string e_entry) in
+ let e_entry = Uint64_wrapper.of_bigint e_entry in
match Abi_mips64.abi_mips64_compute_program_entry_point segments e_entry with
| Error.Fail s -> failwith "Failed computing entry point"
| Error.Success s -> s
@@ -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,
generated by cgit v1.2.3 (git 2.25.1) at 2026-03-10 00:33:46 +0000