diff options
| author | Robert Norton | 2017-05-11 14:54:32 +0100 |
|---|---|---|
| committer | Robert Norton | 2017-05-24 10:56:59 +0100 |
| commit | e9b40edcc325bfe5a0e3566c61ee12a236c5ddf8 (patch) | |
| tree | f81ad5395520cc66a38d08d8ca1965f4e2bc30a3 /mips/run_embed.ml | |
| parent | a6c4b61f4ae06845663eb06b2a0efc98a42ccac3 (diff) | |
Change types of MEMr_tag, MEMval_tag and co. so that tag is separate from data and invent rmemt and wmvt effects for them. Extend the interpreter context to include lists of tagged memory read and write functions. The memory model must round down the address to the nearest capability aligned address when reading/writing tags. Remove TAGw which is no longer needed as a result.
Diffstat (limited to 'mips/run_embed.ml')
| -rw-r--r-- | mips/run_embed.ml | 2 |
1 files changed, 2 insertions, 0 deletions
diff --git a/mips/run_embed.ml b/mips/run_embed.ml index 70dee4b6..463caffd 100644 --- a/mips/run_embed.ml +++ b/mips/run_embed.ml @@ -197,6 +197,7 @@ module CHERI_model : ISA_model = struct set_register Cheri_embed._PCC initial_cap_vec; set_register Cheri_embed._nextPCC initial_cap_vec; set_register Cheri_embed._delayedPCC initial_cap_vec; + cap_size_shift := 5; (* configure memory model cap_size in mips_extras_ml *) for i = 0 to 31 do set_register (vector_access_int Cheri_embed._CapRegs i) initial_cap_vec done @@ -254,6 +255,7 @@ module CHERI128_model : ISA_model = struct set_register Cheri128_embed._PCC initial_cap_vec; set_register Cheri128_embed._nextPCC initial_cap_vec; set_register Cheri128_embed._delayedPCC initial_cap_vec; + cap_size_shift := 4; (* configure memory model cap_size in mips_extras_ml *) for i = 0 to 31 do set_register (vector_access_int Cheri128_embed._CapRegs i) initial_cap_vec done |