summaryrefslogtreecommitdiff
path: root/mips
diff options
context:
space:
mode:
Diffstat (limited to 'mips')
-rw-r--r--mips/mips_extras.lem15
-rw-r--r--mips/mips_extras_embed.lem18
-rw-r--r--mips/mips_extras_embed_sequential.lem18
3 files changed, 22 insertions, 29 deletions
diff --git a/mips/mips_extras.lem b/mips/mips_extras.lem
index 4bbf368b..bdaa08e6 100644
--- a/mips/mips_extras.lem
+++ b/mips/mips_extras.lem
@@ -6,15 +6,14 @@ open import Interp_inter_imp
import Set_extra
let memory_parameter_transformer mode v =
- let mode = <|mode with endian = E_big_endian|> in
match v with
| Interp.V_tuple [location;length] ->
+ let (v,loc_regs) = extern_with_track mode extern_vector_value location in
+
match length with
| Interp.V_lit (L_aux (L_num len) _) ->
- let (v,regs) = extern_mem_value mode location in
- (v,(natFromInteger len),regs)
+ (v,(natFromInteger len),loc_regs)
| Interp.V_track (Interp.V_lit (L_aux (L_num len) _)) size_regs ->
- let (v,loc_regs) = extern_mem_value mode location in
match loc_regs with
| Nothing -> (v,(natFromInteger len),Just (List.map (fun r -> extern_reg r Nothing) (Set_extra.toList size_regs)))
| Just loc_regs -> (v,(natFromInteger len),Just (loc_regs++(List.map (fun r -> extern_reg r Nothing) (Set_extra.toList size_regs))))
@@ -24,12 +23,10 @@ let memory_parameter_transformer mode v =
| _ -> Assert_extra.failwith ("memory_parameter_transformer: expected 'V_tuple [_;_]' given " ^ (Interp.string_of_value v))
end
-let memory_parameter_transformer_option_address mode v =
- let mode = <|mode with endian = E_big_endian|> in
+let memory_parameter_transformer_option_address _mode v =
match v with
| Interp.V_tuple [location;_] ->
- let (v,_) = extern_mem_value mode location in
- Just v
+ Just (extern_vector_value location)
| _ -> Assert_extra.failwith ("memory_parameter_transformer_option_address: expected 'V_tuple [_;_]' given " ^ (Interp.string_of_value v))
end
@@ -42,7 +39,7 @@ let read_memory_functions : memory_reads =
]
let memory_writes : memory_writes =
- [ ("TAGw", (MW Write_tag (fun mode v -> let (v, regs) = extern_mem_value mode v in
+ [ ("TAGw", (MW Write_tag (fun mode v -> let (v, regs) = extern_with_track mode extern_vector_value v in
(v, 1, regs))
(Just (fun (IState interp_state c) success ->
let v = Interp.V_lit (L_aux (if success then L_one else L_zero) Unknown) in
diff --git a/mips/mips_extras_embed.lem b/mips/mips_extras_embed.lem
index 41a6726f..12f2ca5a 100644
--- a/mips/mips_extras_embed.lem
+++ b/mips/mips_extras_embed.lem
@@ -3,17 +3,15 @@ open import Sail_impl_base
open import Sail_values
open import Prompt
-let endian = E_big_endian
-
val MEMr : (vector bitU * integer) -> M (vector bitU)
val MEMr_reserve : (vector bitU * integer) -> M (vector bitU)
val MEMr_tag : (vector bitU * integer) -> M (vector bitU)
val MEMr_tag_reserve : (vector bitU * integer) -> M (vector bitU)
-let MEMr (addr,size) = read_mem endian false Read_plain addr size
-let MEMr_reserve (addr,size) = read_mem endian false Read_reserve addr size
-let MEMr_tag (addr,size) = read_mem endian false Read_tag addr size
-let MEMr_tag_reserve (addr,size) = read_mem endian false Read_tag_reserve addr size
+let MEMr (addr,size) = read_mem false Read_plain addr size
+let MEMr_reserve (addr,size) = read_mem false Read_reserve addr size
+let MEMr_tag (addr,size) = read_mem false Read_tag addr size
+let MEMr_tag_reserve (addr,size) = read_mem false Read_tag_reserve addr size
val MEMea : (vector bitU * integer) -> M unit
@@ -32,10 +30,10 @@ val MEMval_conditional : (vector bitU * integer * vector bitU) -> M bitU
val MEMval_tag : (vector bitU * integer * vector bitU) -> M unit
val MEMval_tag_conditional : (vector bitU * integer * vector bitU) -> M bitU
-let MEMval (_,_,v) = write_mem_val endian v >>= fun _ -> return ()
-let MEMval_conditional (_,_,v) = write_mem_val endian v >>= fun b -> return (if b then B1 else B0)
-let MEMval_tag (_,_,v) = write_mem_val endian v >>= fun _ -> return ()
-let MEMval_tag_conditional (_,_,v) = write_mem_val endian v >>= fun b -> return (if b then B1 else B0)
+let MEMval (_,_,v) = write_mem_val v >>= fun _ -> return ()
+let MEMval_conditional (_,_,v) = write_mem_val v >>= fun b -> return (if b then B1 else B0)
+let MEMval_tag (_,_,v) = write_mem_val v >>= fun _ -> return ()
+let MEMval_tag_conditional (_,_,v) = write_mem_val v >>= fun b -> return (if b then B1 else B0)
val MEM_sync : unit -> M unit
diff --git a/mips/mips_extras_embed_sequential.lem b/mips/mips_extras_embed_sequential.lem
index 502fe102..9aeb9487 100644
--- a/mips/mips_extras_embed_sequential.lem
+++ b/mips/mips_extras_embed_sequential.lem
@@ -3,17 +3,15 @@ open import Sail_impl_base
open import Sail_values
open import State
-let endian = E_big_endian
-
val MEMr : (vector bitU * integer) -> M (vector bitU)
val MEMr_reserve : (vector bitU * integer) -> M (vector bitU)
val MEMr_tag : (vector bitU * integer) -> M (vector bitU)
val MEMr_tag_reserve : (vector bitU * integer) -> M (vector bitU)
-let MEMr (addr,size) = read_mem endian false Read_plain addr size
-let MEMr_reserve (addr,size) = read_mem endian false Read_reserve addr size
-let MEMr_tag (addr,size) = read_mem endian false Read_tag addr size
-let MEMr_tag_reserve (addr,size) = read_mem endian false Read_tag_reserve addr size
+let MEMr (addr,size) = read_mem false Read_plain addr size
+let MEMr_reserve (addr,size) = read_mem false Read_reserve addr size
+let MEMr_tag (addr,size) = read_mem false Read_tag addr size
+let MEMr_tag_reserve (addr,size) = read_mem false Read_tag_reserve addr size
val MEMea : (vector bitU * integer) -> M unit
@@ -32,10 +30,10 @@ val MEMval_conditional : (vector bitU * integer * vector bitU) -> M bitU
val MEMval_tag : (vector bitU * integer * vector bitU) -> M unit
val MEMval_tag_conditional : (vector bitU * integer * vector bitU) -> M bitU
-let MEMval (_,_,v) = write_mem_val endian v >>= fun _ -> return ()
-let MEMval_conditional (_,_,v) = write_mem_val endian v >>= fun b -> return (if b then B1 else B0)
-let MEMval_tag (_,_,v) = write_mem_val endian v >>= fun _ -> return ()
-let MEMval_tag_conditional (_,_,v) = write_mem_val endian v >>= fun b -> return (if b then B1 else B0)
+let MEMval (_,_,v) = write_mem_val v >>= fun _ -> return ()
+let MEMval_conditional (_,_,v) = write_mem_val v >>= fun b -> return (if b then B1 else B0)
+let MEMval_tag (_,_,v) = write_mem_val v >>= fun _ -> return ()
+let MEMval_tag_conditional (_,_,v) = write_mem_val v >>= fun b -> return (if b then B1 else B0)
val MEM_sync : unit -> M unit
generated by cgit v1.2.3 (git 2.25.1) at 2026-03-09 14:21:10 +0000