diff options
Diffstat (limited to 'power/power_extras.lem')
| -rw-r--r-- | power/power_extras.lem | 96 |
1 files changed, 0 insertions, 96 deletions
diff --git a/power/power_extras.lem b/power/power_extras.lem deleted file mode 100644 index b126aced..00000000 --- a/power/power_extras.lem +++ /dev/null @@ -1,96 +0,0 @@ -open import Pervasives_extra -open import Interp_ast -open import Interp_interface -open import Sail_impl_base -open import Interp_inter_imp -import Set_extra - -let rec countLeadingZeros_helper bits = - match bits with - | (Interp_ast.V_lit (L_aux L_zero _))::bits -> - let (n,loc) = match countLeadingZeros_helper bits with - | (Interp_ast.V_lit (L_aux (L_num n) loc)) -> (n,loc) - | _ -> failwith "countLeadingZeros_helper: unexpected value" end in - Interp_ast.V_lit (L_aux (L_num (n+1)) loc) - | _ -> Interp_ast.V_lit (L_aux (L_num 0) Interp_ast.Unknown) -end -let rec countLeadingZeros e = - match e with - | Interp_ast.V_tuple v -> - match v with - | [Interp_ast.V_track v r;Interp_ast.V_track v2 r2] -> - Interp.taint (countLeadingZeros (Interp_ast.V_tuple [v;v2])) (r union r2) - | [Interp_ast.V_track v r;v2] -> Interp.taint (countLeadingZeros (Interp_ast.V_tuple [v;v2])) r - | [v;Interp_ast.V_track v2 r2] -> Interp.taint (countLeadingZeros (Interp_ast.V_tuple [v;v2])) r2 - | [Interp_ast.V_unknown;_] -> Interp_ast.V_unknown - | [_;Interp_ast.V_unknown] -> Interp_ast.V_unknown - | [Interp_ast.V_vector _ _ bits;Interp_ast.V_lit (L_aux (L_num n) _)] -> - countLeadingZeros_helper (snd (List.splitAt (natFromInteger n) bits)) - | _ -> failwith "countLeadingZeros: unexpected value" - end - | _ -> failwith "countLeadingZeros: unexpected value" -end - -(*Power specific external functions*) -let power_externs = [ - ("countLeadingZeroes", countLeadingZeros); -] - -(*All external functions*) -(*let external_functions = Interp_lib.function_map ++ power_externs*) - -(*List of memory functions; needs to be expanded with all of the memory functions needed for PPCMem. - Should probably be expanded into a parameter to mode as with above - *) - -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 - | _ -> failwith "memory_parameter_transformer: unexpected value" - end - | _ -> failwith "memory_parameter_transformer: unexpected value" - end - -let power_read_memory_functions : memory_reads = - [ ("MEMr'", (MR Read_plain memory_parameter_transformer)); - ("MEMr_reserve'", (MR Read_reserve memory_parameter_transformer)); - ] -let power_memory_writes : memory_writes = [] - (* [ ("MEMw", (MW Write_plain memory_parameter_transformer Nothing)); - ("MEMw_conditional", (MW Write_conditional memory_parameter_transformer - (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 power_memory_eas : memory_write_eas = - [ ("MEMw_EA", (MEA Write_plain memory_parameter_transformer)); - ("MEMw_EA_cond", (MEA Write_conditional memory_parameter_transformer)) - ] - -let power_memory_vals : memory_write_vals = - [ ("MEMw'", (MV (fun mode v -> Nothing) Nothing)); - ("MEMw_conditional'", (MV (fun mode v -> Nothing) - (Just (fun (IState interp_state c) success -> - let v = Interp_ast.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 power_barrier_functions = [ - ("I_Sync", Barrier_Isync); - ("H_Sync", Barrier_Sync); - ("LW_Sync", Barrier_LwSync); - ("EIEIO_Sync", Barrier_Eieio); -] |