summaryrefslogtreecommitdiff
path: root/x86/x86_extras.lem
diff options
context:
space:
mode:
authorAlasdair2020-07-31 13:30:53 +0100
committerAlasdair2020-07-31 13:30:53 +0100
commitdd76fdfd819bb1a5423cea369df0e7f2ae449b62 (patch)
tree88d8d69e39b724902b280beaa8ce874e444f5dbc /x86/x86_extras.lem
parent71db59830383b7db5316b5c99ccebe776fc837dc (diff)
Remove old specs that have more up to date version
Move outdated things into old subdirectory
Diffstat (limited to 'x86/x86_extras.lem')
-rw-r--r--x86/x86_extras.lem53
1 files changed, 0 insertions, 53 deletions
diff --git a/x86/x86_extras.lem b/x86/x86_extras.lem
deleted file mode 100644
index d6498d87..00000000
--- a/x86/x86_extras.lem
+++ /dev/null
@@ -1,53 +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 x86_read_memory_functions : memory_reads =
- [ ("rMEM", (MR Read_plain memory_parameter_transformer));
- ("rMEM_locked", (MR Read_X86_locked memory_parameter_transformer));
- ]
-
-let x86_memory_writes : memory_writes =
- []
-
-let x86_memory_eas : memory_write_eas =
- [ ("MEMea", (MEA Write_plain memory_parameter_transformer));
- ("MEMea_locked", (MEA Write_X86_locked memory_parameter_transformer));
- ]
-
-let x86_memory_vals : memory_write_vals =
- [ ("MEMval", (MV memory_parameter_transformer_option_address Nothing));
- ]
-
-let x86_barrier_functions =
- [
- ("X86_MFENCE", Barrier_x86_MFENCE);
- ]