diff options
Diffstat (limited to 'mips/mips_extras.lem')
| -rw-r--r-- | mips/mips_extras.lem | 93 |
1 files changed, 93 insertions, 0 deletions
diff --git a/mips/mips_extras.lem b/mips/mips_extras.lem new file mode 100644 index 00000000..49a618dc --- /dev/null +++ b/mips/mips_extras.lem @@ -0,0 +1,93 @@ +open import Pervasives +open import Interp_ast +open import Interp_interface +open import Interp_inter_imp +import Set_extra + + +(*MIPS specific external functions*) +let mips_externs = [ +] + +let read_memory_functions : memory_reads = + [ ("MEMr", (MR Read_plain + (fun mode v -> match v with + | Interp.V_tuple [location;length] -> + match length with + | Interp.V_lit (L_aux (L_num len) _) -> + let (v,regs) = extern_mem_value mode location in + (v,(natFromInteger len),regs) + | Interp.V_track (Interp.V_lit (L_aux (L_num len) _)) size_regs -> + let (v,loc_regs) = extern_mem_value mode location in + 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 end end))); + ("MEMr_reserve", (MR Read_reserve (*TODO Likely this isn't really best to be the same as Power*) + (fun mode v -> match v with + | Interp.V_tuple [location;length] -> + match length with + | Interp.V_lit (L_aux (L_num len) _) -> + let (v,regs) = extern_mem_value mode location in + (v,(natFromInteger len),regs) + | Interp.V_track (Interp.V_lit (L_aux (L_num len) _)) size_regs -> + let (v,loc_regs) = extern_mem_value mode location in + 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 end end))); +] +let memory_writes : memory_writes = [ + ("MEMw", (MW Write_plain + (fun mode v -> match v with + | Interp.V_tuple [location;length] -> + match length with + | Interp.V_lit (L_aux (L_num len) _) -> + let (v,regs) = extern_mem_value mode location in + (v,(natFromInteger len),regs) + | Interp.V_track (Interp.V_lit (L_aux (L_num len) _)) size_regs -> + let (v,loc_regs) = extern_mem_value mode location in + 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 end end) Nothing)); + (* As above, probably not best to be the same write kind as power *) + ("MEMw_conditional", (MW Write_conditional + (fun mode v -> match v with + | Interp.V_tuple [location;length] -> + match length with + | Interp.V_lit (L_aux (L_num len) _) -> + let (v,regs) = extern_mem_value mode location in + (v,(natFromInteger len),regs) + | Interp.V_track (Interp.V_lit (L_aux (L_num len) _)) size_regs -> + let (v,loc_regs) = extern_mem_value mode location in + 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 end end) + (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 barrier_functions = [ + (*Need to know what barrier kind to install*) + ("MEM_Sync", Isync); +] |