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
|
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);
]
|
