diff options
| author | Shaked Flur | 2017-03-23 14:43:55 +0000 |
|---|---|---|
| committer | Shaked Flur | 2017-03-23 14:43:55 +0000 |
| commit | 68f22b52e40a8e6ea8b99d514faf3310547e63e6 (patch) | |
| tree | d6e8f3ed9883b821d5d5b129fcf5b395bd614172 /mips/mips_extras_embed.lem | |
| parent | 3519cfe79e70c805185eeec3df508534c73b5579 (diff) | |
the interpreter/shallow expects little-endian memory-values
Diffstat (limited to 'mips/mips_extras_embed.lem')
| -rw-r--r-- | mips/mips_extras_embed.lem | 18 |
1 files changed, 8 insertions, 10 deletions
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 |