From 5bd5dff99c934dccae8b96d36d4aaa5dead097e9 Mon Sep 17 00:00:00 2001 From: Jon French Date: Wed, 2 Aug 2017 06:11:27 +0100 Subject: fix run_with_elf*.ml with changed lem_interp api --- src/lem_interp/run_with_elf.ml | 2 +- src/lem_interp/run_with_elf_cheri.ml | 2 +- src/lem_interp/run_with_elf_cheri128.ml | 2 +- 3 files changed, 3 insertions(+), 3 deletions(-) (limited to 'src') diff --git a/src/lem_interp/run_with_elf.ml b/src/lem_interp/run_with_elf.ml index d48b7e7b..2a1783db 100644 --- a/src/lem_interp/run_with_elf.ml +++ b/src/lem_interp/run_with_elf.ml @@ -1292,7 +1292,7 @@ let run () = startaddr, startaddr_internal), pp_symbol_map) = initial_system_state_of_elf_file !file in - let context = build_context isa_defs isa_m0 [] isa_m1 isa_m2 isa_m3 [] isa_m4 None isa_externs in + let context = build_context false isa_defs isa_m0 [] isa_m1 isa_m2 isa_m3 [] isa_m4 None isa_externs in (*NOTE: this is likely MIPS specific, so should probably pull from initial_system_state info on to translate or not, endian mode, and translate function name *) diff --git a/src/lem_interp/run_with_elf_cheri.ml b/src/lem_interp/run_with_elf_cheri.ml index eaf8ddfa..e773bf5b 100644 --- a/src/lem_interp/run_with_elf_cheri.ml +++ b/src/lem_interp/run_with_elf_cheri.ml @@ -1386,7 +1386,7 @@ let run () = startaddr, startaddr_internal), pp_symbol_map) = initial_system_state_of_elf_file !file in - let context = build_context isa_defs isa_m0 isa_m1 isa_m2 isa_m3 isa_m4 isa_m5 isa_m6 None isa_externs in + let context = build_context false isa_defs isa_m0 isa_m1 isa_m2 isa_m3 isa_m4 isa_m5 isa_m6 None isa_externs in (*NOTE: this is likely MIPS specific, so should probably pull from initial_system_state info on to translate or not, endian mode, and translate function name *) diff --git a/src/lem_interp/run_with_elf_cheri128.ml b/src/lem_interp/run_with_elf_cheri128.ml index eca6d342..cd2e7312 100644 --- a/src/lem_interp/run_with_elf_cheri128.ml +++ b/src/lem_interp/run_with_elf_cheri128.ml @@ -1386,7 +1386,7 @@ let run () = startaddr, startaddr_internal), pp_symbol_map) = initial_system_state_of_elf_file !file in - let context = build_context isa_defs isa_m0 isa_m1 isa_m2 isa_m3 isa_m4 isa_m5 isa_m6 None isa_externs in + let context = build_context false isa_defs isa_m0 isa_m1 isa_m2 isa_m3 isa_m4 isa_m5 isa_m6 None isa_externs in (*NOTE: this is likely MIPS specific, so should probably pull from initial_system_state info on to translate or not, endian mode, and translate function name *) -- cgit v1.2.3 From 3ee583761a8b7801d0870c0b47e050ac5c8851cd Mon Sep 17 00:00:00 2001 From: Robert Norton Date: Wed, 2 Aug 2017 14:24:52 +0100 Subject: fix sail library test interpreter glue for API change. Also fix build_context val spec which was out of dated although lem did not complain for some reason... --- src/lem_interp/interp_interface.lem | 2 +- src/test/lib/run_test_interp.ml | 2 +- 2 files changed, 2 insertions(+), 2 deletions(-) (limited to 'src') diff --git a/src/lem_interp/interp_interface.lem b/src/lem_interp/interp_interface.lem index 937db466..dcc9f537 100644 --- a/src/lem_interp/interp_interface.lem +++ b/src/lem_interp/interp_interface.lem @@ -259,7 +259,7 @@ type outcome = (* Functions to build up the initial state for interpretation *) -val build_context : specification -> memory_reads -> memory_read_taggeds-> memory_writes -> memory_write_eas -> memory_write_vals -> memory_write_vals_tagged -> barriers -> excl_res -> external_functions -> context +val build_context : bool -> specification -> memory_reads -> memory_read_taggeds-> memory_writes -> memory_write_eas -> memory_write_vals -> memory_write_vals_tagged -> barriers -> excl_res -> external_functions -> context val initial_instruction_state : context -> string -> list register_value -> instruction_state (* string is a function name, list of value are the parameters to that function *) diff --git a/src/test/lib/run_test_interp.ml b/src/test/lib/run_test_interp.ml index 3446ef9f..5f2ace1b 100644 --- a/src/test/lib/run_test_interp.ml +++ b/src/test/lib/run_test_interp.ml @@ -45,7 +45,7 @@ open Interp_inter_imp ;; open Sail_impl_base ;; let doit () = - let context = build_context Test_lem_ast.defs [] [] [] [] [] [] [] None [] in + let context = build_context false Test_lem_ast.defs [] [] [] [] [] [] [] None [] in translate_address context E_little_endian "run" None (address_of_integer (Nat_big_num.of_int 0));; doit () ;; -- cgit v1.2.3 From 73965da84487d06066eae4b9b5fa49da8d123d7b Mon Sep 17 00:00:00 2001 From: Thomas Bauereiss Date: Sat, 12 Aug 2017 19:04:58 +0100 Subject: Fix compilation issue for 32-bit systems --- src/type_internal.ml | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) (limited to 'src') diff --git a/src/type_internal.ml b/src/type_internal.ml index 155e78f4..ddf0b692 100644 --- a/src/type_internal.ml +++ b/src/type_internal.ml @@ -1901,8 +1901,8 @@ let int8_t = {t = Tapp("range", [TA_nexp (mk_neg (mk_2nc (mk_c_int 7) (big_int_o TA_nexp (mk_c_int 127)])} let int16_t = {t = Tapp("range", [TA_nexp (mk_neg (mk_2nc (mk_c_int 15) (big_int_of_int 32768))); TA_nexp (mk_c_int 32767)])} -let int32_t = {t = Tapp("range", [TA_nexp (mk_neg (mk_2nc (mk_c_int 31) (big_int_of_int 2147483648))) ; - TA_nexp (mk_c_int 2147483647)])} +let int32_t = {t = Tapp("range", [TA_nexp (mk_neg (mk_2nc (mk_c_int 31) (big_int_of_string "2147483648"))) ; + TA_nexp (mk_c (big_int_of_string "2147483647"))])} let int64_t = {t = Tapp("range", [TA_nexp (mk_neg (mk_2nc (mk_c_int 63) (big_int_of_string "9223372036854775808"))); TA_nexp (mk_c (big_int_of_string "9223372036854775807"))])} -- cgit v1.2.3 From 44850d32e227647813b44a8c97c4de57cd7a9978 Mon Sep 17 00:00:00 2001 From: Thomas Bauereiss Date: Sat, 12 Aug 2017 19:05:32 +0100 Subject: Resolve ambiguity between negation of integers and bools --- src/gen_lib/sail_values.lem | 3 +-- 1 file changed, 1 insertion(+), 2 deletions(-) (limited to 'src') diff --git a/src/gen_lib/sail_values.lem b/src/gen_lib/sail_values.lem index 38f7d512..49f37381 100644 --- a/src/gen_lib/sail_values.lem +++ b/src/gen_lib/sail_values.lem @@ -266,7 +266,7 @@ let hardware_quot (a:integer) (b:integer) : integer = if ((a<0) = (b<0)) then q (* same sign -- result positive *) else - ~q (* different sign -- result negative *) + integerNegate q (* different sign -- result negative *) let quot_signed = hardware_quot @@ -956,4 +956,3 @@ let diafp_to_dia reginfo = function | DIAFP_concrete v -> DIA_concrete_address (address_of_bitv v) | DIAFP_reg r -> DIA_register (regfp_to_reg reginfo r) end - -- cgit v1.2.3