diff options
| author | Shaked Flur | 2017-05-24 16:45:22 +0100 |
|---|---|---|
| committer | Shaked Flur | 2017-05-24 16:45:22 +0100 |
| commit | b400be4ea3917ace2237149e11dd5e1ab4e35078 (patch) | |
| tree | 2baa7860e625b180c26f61acbc44db347fccfb6b /mips/mips_extras.lem | |
| parent | 9cffd54c6170f8a5cdcc6e54cb9077b62bf6a284 (diff) | |
| parent | e9b40edcc325bfe5a0e3566c61ee12a236c5ddf8 (diff) | |
Merge branch 'master' of bitbucket.org:Peter_Sewell/sail
# Conflicts:
# src/lem_interp/interp.lem
# src/lem_interp/interp_inter_imp.lem
# src/lem_interp/interp_interface.lem
# src/parser.mly
# src/pretty_print_lem.ml
Diffstat (limited to 'mips/mips_extras.lem')
| -rw-r--r-- | mips/mips_extras.lem | 25 |
1 files changed, 12 insertions, 13 deletions
diff --git a/mips/mips_extras.lem b/mips/mips_extras.lem index bdaa08e6..99487f49 100644 --- a/mips/mips_extras.lem +++ b/mips/mips_extras.lem @@ -34,23 +34,19 @@ let memory_parameter_transformer_option_address _mode v = let read_memory_functions : memory_reads = [ ("MEMr", (MR Read_plain memory_parameter_transformer)); ("MEMr_reserve", (MR Read_reserve memory_parameter_transformer)); - ("MEMr_tag", (MR Read_tag memory_parameter_transformer)); - ("MEMr_tag_reserve", (MR Read_tag_reserve memory_parameter_transformer)); + ] + +let read_memory_tagged_functions : memory_read_taggeds = + [ ("MEMr_tag", (MRT Read_plain memory_parameter_transformer)); + ("MEMr_tag_reserve", (MRT Read_reserve memory_parameter_transformer)); ] let memory_writes : memory_writes = - [ ("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 - IState (Interp.add_answer_to_stack interp_state v) c)) - )); ] + [] let memory_eas : memory_write_eas = [ ("MEMea", (MEA Write_plain memory_parameter_transformer)); ("MEMea_conditional", (MEA Write_conditional memory_parameter_transformer)); - ("MEMea_tag", (MEA Write_tag memory_parameter_transformer)); - ("MEMea_tag_conditional", (MEA Write_tag_conditional memory_parameter_transformer)); ] let memory_vals : memory_write_vals = @@ -60,15 +56,18 @@ let memory_vals : memory_write_vals = (fun (IState interp context) b -> let bit = Interp.V_lit (L_aux (if b then L_one else L_zero) Interp_ast.Unknown) in (IState (Interp.add_answer_to_stack interp bit) context))))); - ("MEMval_tag", (MV memory_parameter_transformer_option_address Nothing)); - ("MEMval_tag_conditional", (MV memory_parameter_transformer_option_address + ] + +let memory_vals_tagged : memory_write_vals_tagged = + [ + ("MEMval_tag", (MVT memory_parameter_transformer_option_address Nothing)); + ("MEMval_tag_conditional", (MVT memory_parameter_transformer_option_address (Just (fun (IState interp context) b -> let bit = Interp.V_lit (L_aux (if b then L_one else L_zero) Interp_ast.Unknown) in (IState (Interp.add_answer_to_stack interp bit) context))))); ] - let barrier_functions = [ ("MEM_sync", Barrier_MIPS_SYNC); ] |