summaryrefslogtreecommitdiff
path: root/src
diff options
context:
space:
mode:
Diffstat (limited to 'src')
-rw-r--r--src/Makefile4
-rw-r--r--src/gen_lib/prompt.lem9
-rw-r--r--src/gen_lib/sail_values.lem57
-rw-r--r--src/lem_interp/interp_inter_imp.lem16
-rw-r--r--src/lem_interp/sail_impl_base.lem7
-rw-r--r--src/pretty_print.ml4
6 files changed, 63 insertions, 34 deletions
diff --git a/src/Makefile b/src/Makefile
index 5d501931..30ff9254 100644
--- a/src/Makefile
+++ b/src/Makefile
@@ -25,8 +25,8 @@ LEMLIBOCAML = $(BITBUCKET_ROOT)/lem/ocaml-lib
ELFDIR= $(BITBUCKET_ROOT)/linksem
MIPS_SAIL_DIR:=$(BITBUCKET_ROOT)/sail/mips
-MIPS_SAILS:=$(MIPS_SAIL_DIR)/mips_prelude.sail $(MIPS_SAIL_DIR)/mips_tlb.sail $(MIPS_SAIL_DIR)/mips_wrappers.sail $(MIPS_SAIL_DIR)/mips_insts.sail $(MIPS_SAIL_DIR)/mips_ri.sail $(MIPS_SAIL_DIR)/mips_epilogue.sail $(MIPS_SAIL_DIR)/mips_regfp.sail
-MIPS_NOTLB_SAILS:=$(MIPS_SAIL_DIR)/mips_prelude.sail $(MIPS_SAIL_DIR)/mips_tlb_stub.sail $(MIPS_SAIL_DIR)/mips_wrappers.sail $(MIPS_SAIL_DIR)/mips_insts.sail $(MIPS_SAIL_DIR)/mips_epilogue.sail $(MIPS_SAIL_DIR)/mips_regfp.sail
+MIPS_SAILS:=$(MIPS_SAIL_DIR)/mips_prelude.sail $(MIPS_SAIL_DIR)/mips_tlb.sail $(MIPS_SAIL_DIR)/mips_wrappers.sail $(MIPS_SAIL_DIR)/mips_insts.sail $(MIPS_SAIL_DIR)/mips_ri.sail $(MIPS_SAIL_DIR)/mips_epilogue.sail $(BITBUCKET_ROOT)/sail/etc/regfp.sail $(MIPS_SAIL_DIR)/mips_regfp.sail
+MIPS_NOTLB_SAILS:=$(MIPS_SAIL_DIR)/mips_prelude.sail $(MIPS_SAIL_DIR)/mips_tlb_stub.sail $(MIPS_SAIL_DIR)/mips_wrappers.sail $(MIPS_SAIL_DIR)/mips_insts.sail $(MIPS_SAIL_DIR)/mips_epilogue.sail $(BITBUCKET_ROOT)/sail/etc/regfp.sail $(MIPS_SAIL_DIR)/mips_regfp.sail
CHERI_SAIL_DIR:=$(BITBUCKET_ROOT)/sail/cheri
CHERI_SAILS:=$(MIPS_SAIL_DIR)/mips_prelude.sail $(MIPS_SAIL_DIR)/mips_tlb.sail $(CHERI_SAIL_DIR)/cheri_prelude.sail $(MIPS_SAIL_DIR)/mips_insts.sail $(CHERI_SAIL_DIR)/cheri_insts.sail $(MIPS_SAIL_DIR)/mips_ri.sail $(MIPS_SAIL_DIR)/mips_epilogue.sail
diff --git a/src/gen_lib/prompt.lem b/src/gen_lib/prompt.lem
index 18868b4a..6d895a87 100644
--- a/src/gen_lib/prompt.lem
+++ b/src/gen_lib/prompt.lem
@@ -66,9 +66,9 @@ let read_reg_aux reg =
let read_reg reg =
read_reg_aux (extern_reg_whole reg)
let read_reg_range reg i j =
- read_reg_aux (extern_reg_slice reg (i,j))
+ read_reg_aux (extern_reg_slice reg (natFromInteger i,natFromInteger j))
let read_reg_bit reg i =
- read_reg_aux (extern_reg_slice reg (i,i)) >>= fun v ->
+ read_reg_aux (extern_reg_slice reg (natFromInteger i,natFromInteger i)) >>= fun v ->
return (extract_only_bit v)
let read_reg_field reg regfield =
read_reg_aux (extern_reg_field_whole reg regfield)
@@ -84,9 +84,10 @@ let write_reg_aux reg_name v =
let write_reg reg v =
write_reg_aux (extern_reg_whole reg) v
let write_reg_range reg i j v =
- write_reg_aux (extern_reg_slice reg (i,j)) v
+ write_reg_aux (extern_reg_slice reg (natFromInteger i,natFromInteger j)) v
let write_reg_bit reg i bit =
- write_reg_aux (extern_reg_slice reg (i,i)) (Vector [bit] i (is_inc_of_reg reg))
+ let iN = natFromInteger i in
+ write_reg_aux (extern_reg_slice reg (iN,iN)) (Vector [bit] i (is_inc_of_reg reg))
let write_reg_field reg regfield v =
write_reg_aux (extern_reg_field_whole reg regfield) v
let write_reg_bitfield reg regfield bit =
diff --git a/src/gen_lib/sail_values.lem b/src/gen_lib/sail_values.lem
index 975c7a5e..399cc218 100644
--- a/src/gen_lib/sail_values.lem
+++ b/src/gen_lib/sail_values.lem
@@ -814,8 +814,7 @@ let intern_reg_value v =
(v.rv_dir = D_increasing)
-let extern_slice (d:direction) (start:nat) ((i,j):(integer*integer)) =
- let (i,j) = (natFromInteger i,natFromInteger j) in
+let extern_slice (d:direction) (start:nat) ((i,j):(nat*nat)) =
match d with
(*This is the case the thread/concurrecny model expects, so no change needed*)
| D_increasing -> (i,j)
@@ -833,13 +832,13 @@ let extern_reg_slice reg (i,j) =
Reg_slice (name_of_reg reg) start dir (extern_slice dir start (i,j))
let extern_reg_field_whole reg rfield =
- let (m,n) = register_field_indices reg rfield in
+ let (m,n) = register_field_indices_nat reg rfield in
let start = start_of_reg_nat reg in
let dir = dir_of_reg reg in
Reg_field (name_of_reg reg) start dir rfield (extern_slice dir start (m,n))
let extern_reg_field_slice reg rfield (i,j) =
- let (m,n) = register_field_indices reg rfield in
+ let (m,n) = register_field_indices_nat reg rfield in
let start = start_of_reg_nat reg in
let dir = dir_of_reg reg in
Reg_f_slice (name_of_reg reg) start dir rfield
@@ -1399,6 +1398,12 @@ instance (ToFromInterpValue instruction_kind)
end
+type regfp =
+ | RFull of (string)
+ | RSlice of (string * integer * integer)
+ | RSliceBit of (string * integer)
+ | RField of (string * string)
+
let regfpToInterpValue = function
| RFull v -> SI.V_ctor (SIA.Id_aux (SIA.Id "RFull") SIA.Unknown) (SIA.T_id "regfp") SI.C_Union (toInterpValue v)
| RSlice v -> SI.V_ctor (SIA.Id_aux (SIA.Id "RSlice") SIA.Unknown) (SIA.T_id "regfp") SI.C_Union (toInterpValue v)
@@ -1420,23 +1425,53 @@ instance (ToFromInterpValue regfp)
let fromInterpValue = regfpFromInterpValue
end
-(*
-let rfp_to_reg reg_info direction = function
+
+let regfp_to_reg (reg_info : string -> maybe string -> (nat * nat * direction * (nat * nat))) = function
| RFull name ->
let (start,length,direction,_) = reg_info name Nothing in
Reg name start length direction
| RSlice (name,i,j) ->
+ let i = natFromInteger i in
+ let j = natFromInteger j in
let (start,length,direction,_) = reg_info name Nothing in
- let slice = extern_slice direction (natFromInteger start) (i,j) in
+ let slice = extern_slice direction start (i,j) in
Reg_slice name start direction slice
| RSliceBit (name,i) ->
+ let i = natFromInteger i in
let (start,length,direction,_) = reg_info name Nothing in
- let slice = extern_slice direction (natFromInteger start) (i,i) in
+ let slice = extern_slice direction start (i,i) in
Reg_slice name start direction slice
| RField (name,field_name) ->
let (start,length,direction,span) = reg_info name (Just field_name) in
- let start = natFromInteger start in
- let slice = extern_slice direction start (start,span) in
+ let slice = extern_slice direction start span in
Reg_field name start direction field_name slice
end
- *)
+
+
+type niafp =
+ | NIAFP_successor
+ | NIAFP_concrete_address of vector bitU
+ | NIAFP_LR
+ | NIAFP_CTR
+ | NIAFP_register of regfp
+
+(* only for MIPS *)
+type diafp =
+ | DIAFP_none
+ | DIAFP_concrete of vector bitU
+ | DIAFP_reg of regfp
+
+let niafp_to_nia reginfo = function
+ | NIAFP_successor -> NIA_successor
+ | NIAFP_concrete_address v -> NIA_concrete_address (address_of_bitv v)
+ | NIAFP_LR -> NIA_LR
+ | NIAFP_CTR -> NIA_CTR
+ | NIAFP_register r -> NIA_register (regfp_to_reg reginfo r)
+end
+
+let diafp_to_dia reginfo = function
+ | DIAFP_none -> DIA_none
+ | 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 cb5868ea..76dc01a1 100644
--- a/src/lem_interp/interp_inter_imp.lem
+++ b/src/lem_interp/interp_inter_imp.lem
@@ -506,18 +506,18 @@ let instruction_analysis top_level end_flag thunk_name regn_to_reg_details regis
| Just addr -> addr
| Nothing -> failwith "get_nia encountered invalid address" end in
let dia_to_dia = function
- | Interp.V_ctor (Id_aux (Id "DIA_none") _) _ _ _ -> DIA_none
- | Interp.V_ctor (Id_aux (Id "DIA_concrete") _) _ _ address ->
+ | Interp.V_ctor (Id_aux (Id "DIAFP_none") _) _ _ _ -> DIA_none
+ | Interp.V_ctor (Id_aux (Id "DIAFP_concrete") _) _ _ address ->
DIA_concrete_address (get_addr address)
- | Interp.V_ctor (Id_aux (Id "DIA_reg") _) _ _ reg -> DIA_register (reg_to_reg_name reg)
+ | Interp.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.V_ctor (Id_aux (Id "NIA_successor") _) _ _ _-> NIA_successor
- | Interp.V_ctor (Id_aux (Id "NIA_concrete_address") _) _ _ address ->
+ | Interp.V_ctor (Id_aux (Id "NIAFP_successor") _) _ _ _-> NIA_successor
+ | Interp.V_ctor (Id_aux (Id "NIAFP_concrete_address") _) _ _ address ->
NIA_concrete_address (get_addr address)
- | Interp.V_ctor (Id_aux (Id "NIA_LR") _) _ _ _ -> NIA_LR
- | Interp.V_ctor (Id_aux (Id "NIA_CTR") _) _ _ _ -> NIA_CTR
- | Interp.V_ctor (Id_aux (Id "NIA_register") _) _ _ reg ->
+ | Interp.V_ctor (Id_aux (Id "NIAFP_LR") _) _ _ _ -> NIA_LR
+ | Interp.V_ctor (Id_aux (Id "NIAFP_CTR") _) _ _ _ -> NIA_CTR
+ | Interp.V_ctor (Id_aux (Id "NIAFP_register") _) _ _ reg ->
NIA_register (reg_to_reg_name reg)
| _ -> failwith "Register footprint analysis did not return nia of expected type" end in
let ik_to_ik = function
diff --git a/src/lem_interp/sail_impl_base.lem b/src/lem_interp/sail_impl_base.lem
index 86778bee..63040ebf 100644
--- a/src/lem_interp/sail_impl_base.lem
+++ b/src/lem_interp/sail_impl_base.lem
@@ -1399,10 +1399,3 @@ instance (Eq decode_error)
let (=) = decode_error_equal
let (<>) = decode_error_inequal
end
-
-type regfp =
- | RFull of (string)
- | RSlice of (string * integer * integer)
- | RSliceBit of (string * integer)
- | RField of (string * string)
-
diff --git a/src/pretty_print.ml b/src/pretty_print.ml
index 1ad4c632..68a3859c 100644
--- a/src/pretty_print.ml
+++ b/src/pretty_print.ml
@@ -2791,8 +2791,8 @@ let doc_typdef_lem regtypes (TD_aux(td,_)) = match td with
| Id_aux ((Id "barrier_kind"),_) -> empty
| Id_aux ((Id "instruction_kind"),_) -> empty
| Id_aux ((Id "regfp"),_) -> empty
- (* | Id_aux ((Id "nia"),_) -> empty
- | Id_aux ((Id "dia"),_) -> empty *)
+ | Id_aux ((Id "niafp"),_) -> empty
+ | Id_aux ((Id "diafp"),_) -> empty
| _ ->
let ar_doc = group (separate_map (break 1) (doc_type_union_lem regtypes) ar) in
let typ_pp =
generated by cgit v1.2.3 (git 2.25.1) at 2026-03-10 07:44:05 +0000