1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
|
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_NonShReads", Barrier_DMB (A64_NonShare, A64_barrier_LD));
("DataMemoryBarrier_NonShWrites", Barrier_DMB (A64_NonShare, A64_barrier_ST));
("DataMemoryBarrier_NonShAll", Barrier_DMB (A64_NonShare, A64_barrier_all));
("DataMemoryBarrier_InnerShReads", Barrier_DMB (A64_InnerShare, A64_barrier_LD));
("DataMemoryBarrier_InnerShWrites", Barrier_DMB (A64_InnerShare, A64_barrier_ST));
("DataMemoryBarrier_InnerShAll", Barrier_DMB (A64_InnerShare, A64_barrier_all));
("DataMemoryBarrier_OuterShReads", Barrier_DMB (A64_OuterShare, A64_barrier_LD));
("DataMemoryBarrier_OuterShWrites", Barrier_DMB (A64_OuterShare, A64_barrier_ST));
("DataMemoryBarrier_OuterShAll", Barrier_DMB (A64_OuterShare, A64_barrier_all));
("DataMemoryBarrier_FullShReads", Barrier_DMB (A64_FullShare, A64_barrier_LD));
("DataMemoryBarrier_FullShWrites", Barrier_DMB (A64_FullShare, A64_barrier_ST));
("DataMemoryBarrier_FullShAll", Barrier_DMB (A64_FullShare, A64_barrier_all));
("DataSynchronizationBarrier_NonShReads", Barrier_DSB (A64_NonShare, A64_barrier_LD));
("DataSynchronizationBarrier_NonShWrites", Barrier_DSB (A64_NonShare, A64_barrier_ST));
("DataSynchronizationBarrier_NonShAll", Barrier_DSB (A64_NonShare, A64_barrier_all));
("DataSynchronizationBarrier_InnerShReads", Barrier_DSB (A64_InnerShare, A64_barrier_LD));
("DataSynchronizationBarrier_InnerShWrites", Barrier_DSB (A64_InnerShare, A64_barrier_ST));
("DataSynchronizationBarrier_InnerShAll", Barrier_DSB (A64_InnerShare, A64_barrier_all));
("DataSynchronizationBarrier_OuterShReads", Barrier_DSB (A64_OuterShare, A64_barrier_LD));
("DataSynchronizationBarrier_OuterShWrites", Barrier_DSB (A64_OuterShare, A64_barrier_ST));
("DataSynchronizationBarrier_OuterShAll", Barrier_DSB (A64_OuterShare, A64_barrier_all));
("DataSynchronizationBarrier_FullShReads", Barrier_DSB (A64_FullShare, A64_barrier_LD));
("DataSynchronizationBarrier_FullShWrites", Barrier_DSB (A64_FullShare, A64_barrier_ST));
("DataSynchronizationBarrier_FullShAll", Barrier_DSB (A64_FullShare, A64_barrier_all));
("InstructionSynchronizationBarrier", Barrier_ISB ());
("TMCommitEffect", Barrier_TM_COMMIT ());
]
|
