diff options
Diffstat (limited to 'risc-v/riscv_extras.lem')
| -rw-r--r-- | risc-v/riscv_extras.lem | 83 |
1 files changed, 0 insertions, 83 deletions
diff --git a/risc-v/riscv_extras.lem b/risc-v/riscv_extras.lem deleted file mode 100644 index 4ca5f9b7..00000000 --- a/risc-v/riscv_extras.lem +++ /dev/null @@ -1,83 +0,0 @@ -open import Pervasives -open import Interp_ast -open import Interp_interface -open import Sail_impl_base -open import Interp_inter_imp -import Set_extra - -let memory_parameter_transformer mode v = - match v with - | Interp_ast.V_tuple [location;length] -> - let (v,loc_regs) = extern_with_track mode extern_vector_value location in - - match length with - | Interp_ast.V_lit (L_aux (L_num len) _) -> - (v,(natFromInteger len),loc_regs) - | Interp_ast.V_track (Interp_ast.V_lit (L_aux (L_num len) _)) size_regs -> - 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)))) - end - | _ -> Assert_extra.failwith "expected 'V_lit (L_aux (L_num _) _)' or 'V_track (V_lit (L_aux (L_num len) _)) _'" - end - | _ -> Assert_extra.failwith ("memory_parameter_transformer: expected 'V_tuple [_;_]' given " ^ (Interp.string_of_value v)) - end - -let memory_parameter_transformer_option_address _mode v = - match v with - | Interp_ast.V_tuple [location;_] -> - Just (extern_vector_value location) - | _ -> Assert_extra.failwith ("memory_parameter_transformer_option_address: expected 'V_tuple [_;_]' given " ^ (Interp.string_of_value v)) - end - - -let riscv_read_memory_functions : memory_reads = - [ ("MEMr", (MR Read_plain memory_parameter_transformer)); - ("MEMr_acquire", (MR Read_RISCV_acquire memory_parameter_transformer)); - ("MEMr_strong_acquire", (MR Read_RISCV_strong_acquire memory_parameter_transformer)); - ("MEMr_reserved", (MR Read_RISCV_reserved memory_parameter_transformer)); - ("MEMr_reserved_acquire", (MR Read_RISCV_reserved_acquire memory_parameter_transformer)); - ("MEMr_reserved_strong_acquire", - (MR Read_RISCV_reserved_acquire memory_parameter_transformer)); - ] - -let riscv_memory_writes : memory_writes = - [] - -let riscv_memory_eas : memory_write_eas = - [ ("MEMea", (MEA Write_plain memory_parameter_transformer)); - ("MEMea_release", (MEA Write_RISCV_release memory_parameter_transformer)); - ("MEMea_strong_release", (MEA Write_RISCV_strong_release memory_parameter_transformer)); - ("MEMea_conditional", (MEA Write_RISCV_conditional memory_parameter_transformer)); - ("MEMea_conditional_release", (MEA Write_RISCV_conditional_release memory_parameter_transformer)); - ("MEMea_conditional_strong_release", - (MEA Write_RISCV_conditional_strong_release - memory_parameter_transformer)); - ] - -let riscv_memory_vals : memory_write_vals = - [ ("MEMval", (MV memory_parameter_transformer_option_address Nothing)); - ("MEMval_release", (MV memory_parameter_transformer_option_address Nothing)); - ("MEMval_strong_release", (MV memory_parameter_transformer_option_address Nothing)); - ("MEMval_conditional", (MV memory_parameter_transformer_option_address Nothing)); - ("MEMval_conditional_release",(MV memory_parameter_transformer_option_address Nothing)); - ("MEMval_conditional_strong_release", - (MV memory_parameter_transformer_option_address Nothing)); - - ] - -let riscv_speculate_conditional_success : excl_res = - let f = fun (IState interp context) b -> - let bool_res = Interp_ast.V_lit (L_aux (if b then L_one else L_zero) Interp_ast.Unknown) in - IState (Interp.add_answer_to_stack interp bool_res) context - in - Just ("speculate_conditional_success", (ER (Just f))) - -let riscv_barrier_functions = - [ ("MEM_fence_rw_rw", Barrier_RISCV_rw_rw); - ("MEM_fence_r_rw", Barrier_RISCV_r_rw); - ("MEM_fence_r_r", Barrier_RISCV_r_r); - ("MEM_fence_rw_w", Barrier_RISCV_rw_w); - ("MEM_fence_w_w", Barrier_RISCV_w_w); - ("MEM_fence_i", Barrier_RISCV_i); - ] |