Remove old specs that have more up to date version

Move outdated things into old subdirectory

1 files changed, 0 insertions, 77 deletions

diff --git a/arm/armV8_extras.lem b/arm/armV8_extras.lem
deleted file mode 100644
index 9a187ecb..00000000
--- a/arm/armV8_extras.lem
+++ /dev/null
@@ -1,77 +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 "expected 'V_tuple [_;_]'"
-  end
-
-let aArch64_read_memory_functions : memory_reads =
-  [ ("rMem_NORMAL",         (MR Read_plain             memory_parameter_transformer));
-    ("rMem_STREAM",         (MR Read_stream            memory_parameter_transformer));
-    ("rMem_ORDERED",        (MR Read_acquire           memory_parameter_transformer));
-    ("rMem_ATOMIC",         (MR Read_exclusive         memory_parameter_transformer));
-    ("rMem_ATOMIC_ORDERED", (MR Read_exclusive_acquire memory_parameter_transformer));
-  ]
-
-let aArch64_memory_writes : memory_writes = []
-  (* [ ("wMem_NORMAL",         (MW Write_plain             memory_parameter_transformer Nothing));
-    ("wMem_ORDERED",        (MW Write_release           memory_parameter_transformer Nothing));
-    ("wMem_ATOMIC",         (MW Write_exclusive         memory_parameter_transformer Nothing));
-    ("wMem_ATOMIC_ORDERED", (MW Write_exclusive_release memory_parameter_transformer Nothing));
-  ] *)
-
-let aArch64_memory_eas : memory_write_eas =
-  [ ("wMem_Addr_NORMAL",         (MEA Write_plain             memory_parameter_transformer));
-    ("wMem_Addr_ORDERED",        (MEA Write_release           memory_parameter_transformer));
-    ("wMem_Addr_ATOMIC",         (MEA Write_exclusive         memory_parameter_transformer));
-    ("wMem_Addr_ATOMIC_ORDERED", (MEA Write_exclusive_release memory_parameter_transformer));
-  ]
-
-let aArch64_memory_vals : memory_write_vals =
-  [ ("wMem_Val_NORMAL",      (MV (fun mode v -> Nothing) Nothing));
-    ("wMem_Val_ATOMIC", (MV (fun mode v -> Nothing)
-                           (Just 
-			   (fun (IState interp context) b -> 
-			     (*ppcmem2 provides true for success and false for failure; but the status for ARM is reversed*)
-			     let bit = Interp_ast.V_lit (L_aux (if b then L_zero else L_one) Interp_ast.Unknown)in
-			     (IState (Interp.add_answer_to_stack interp bit) context)))));
-  ]
-
-let aArch64_excl_res : 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_exclusive_success", (ER (Just f)))
-
-let aArch64_barrier_functions =
-  [ ("DataMemoryBarrier_Reads",           Barrier_DMB_LD);
-    ("DataMemoryBarrier_Writes",          Barrier_DMB_ST);
-    ("DataMemoryBarrier_All",             Barrier_DMB);
-    ("DataSynchronizationBarrier_Reads",  Barrier_DSB_LD);
-    ("DataSynchronizationBarrier_Writes", Barrier_DSB_ST);
-    ("DataSynchronizationBarrier_All",    Barrier_DSB);
-    ("InstructionSynchronizationBarrier", Barrier_ISB);
-
-    ("TMCommitEffect",                    Barrier_TM_COMMIT);
-  ]