diff options
| author | Alasdair Armstrong | 2017-08-29 18:00:51 +0100 |
|---|---|---|
| committer | Alasdair Armstrong | 2017-08-29 18:00:51 +0100 |
| commit | 04c32956a50d2e0a2f62b02828e9b549854a2b8c (patch) | |
| tree | cbdaadcb1f11fa8c740378d7fa6a3e04b63f7802 /mips_new_tc/mips_extras_embed_sequential.lem | |
| parent | 9cc9b5afff769b9185c6e6e4afad496d58d1a38d (diff) | |
| parent | 2300d45d6645faae3c00a183e80547c1a6cb9165 (diff) | |
Merge branch 'experiments' of https://bitbucket.org/Peter_Sewell/sail into experiments
Diffstat (limited to 'mips_new_tc/mips_extras_embed_sequential.lem')
| -rw-r--r-- | mips_new_tc/mips_extras_embed_sequential.lem | 16 |
1 files changed, 8 insertions, 8 deletions
diff --git a/mips_new_tc/mips_extras_embed_sequential.lem b/mips_new_tc/mips_extras_embed_sequential.lem index f9c6c92c..8425c110 100644 --- a/mips_new_tc/mips_extras_embed_sequential.lem +++ b/mips_new_tc/mips_extras_embed_sequential.lem @@ -6,8 +6,8 @@ open import State val MEMr : forall 'regs 'a 'b. Size 'b => (bitvector 'a * integer) -> M 'regs (bitvector 'b) val MEMr_reserve : forall 'regs 'a 'b. Size 'b => (bitvector 'a * integer) -> M 'regs (bitvector 'b) -val MEMr_tag : forall 'regs 'a 'b. Size 'b => (bitvector 'a * integer) -> M 'regs (bitU * bitvector 'b) -val MEMr_tag_reserve : forall 'regs 'a 'b. Size 'b => (bitvector 'a * integer) -> M 'regs (bitU * bitvector 'b) +val MEMr_tag : forall 'regs 'a 'b. Size 'b => (bitvector 'a * integer) -> M 'regs (bool * bitvector 'b) +val MEMr_tag_reserve : forall 'regs 'a 'b. Size 'b => (bitvector 'a * integer) -> M 'regs (bool * bitvector 'b) let MEMr (addr,size) = read_mem false Read_plain addr size let MEMr_reserve (addr,size) = read_mem false Read_reserve addr size @@ -15,12 +15,12 @@ let MEMr_reserve (addr,size) = read_mem false Read_reserve addr size let MEMr_tag (addr,size) = read_mem false Read_plain addr size >>= fun v -> read_tag false Read_plain addr >>= fun t -> - return (t, v) + return (bitU_to_bool t, v) let MEMr_tag_reserve (addr,size) = read_mem false Read_plain addr size >>= fun v -> read_tag false Read_plain addr >>= fun t -> - return (t, v) + return (bitU_to_bool t, v) val MEMea : forall 'regs 'a. (bitvector 'a * integer) -> M 'regs unit @@ -37,13 +37,13 @@ let MEMea_tag_conditional (addr,size) = write_mem_ea Write_conditional addr size val MEMval : forall 'regs 'a 'b. (bitvector 'a * integer * bitvector 'b) -> M 'regs unit val MEMval_conditional : forall 'regs 'a 'b. (bitvector 'a * integer * bitvector 'b) -> M 'regs bool -val MEMval_tag : forall 'regs 'a 'b. (bitvector 'a * integer * bitU * bitvector 'b) -> M 'regs unit -val MEMval_tag_conditional : forall 'regs 'a 'b. (bitvector 'a * integer * bitU * bitvector 'b) -> M 'regs bool +val MEMval_tag : forall 'regs 'a 'b. (bitvector 'a * integer * bool * bitvector 'b) -> M 'regs unit +val MEMval_tag_conditional : forall 'regs 'a 'b. (bitvector 'a * integer * bool * bitvector 'b) -> M 'regs bool let MEMval (_,_,v) = write_mem_val v >>= fun _ -> return () let MEMval_conditional (_,_,v) = write_mem_val v >>= fun b -> return (if b then true else false) -let MEMval_tag (_,_,t,v) = write_mem_val v >>= fun _ -> write_tag t >>= fun _ -> return () -let MEMval_tag_conditional (_,_,t,v) = write_mem_val v >>= fun b -> write_tag t >>= fun _ -> return (if b then true else false) +let MEMval_tag (_,_,t,v) = write_mem_val v >>= fun _ -> write_tag (bool_to_bitU t) >>= fun _ -> return () +let MEMval_tag_conditional (_,_,t,v) = write_mem_val v >>= fun b -> write_tag (bool_to_bitU t) >>= fun _ -> return (if b then true else false) val MEM_sync : forall 'regs. unit -> M 'regs unit |