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
|
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 riscv_read_memory_functions : memory_reads =
[ ("MEMr", (MR Read_plain memory_parameter_transformer));
("MEMr_acquire", (MR Read_RISCV_acquire memory_parameter_transformer));
("MEMr_strong_acquire", (MR Read_RISCV_strong_acquire memory_parameter_transformer));
("MEMr_reserved", (MR Read_RISCV_reserved memory_parameter_transformer));
("MEMr_reserved_acquire", (MR Read_RISCV_reserved_acquire memory_parameter_transformer));
("MEMr_reserved_strong_acquire",
(MR Read_RISCV_reserved_acquire memory_parameter_transformer));
]
let riscv_memory_writes : memory_writes =
[]
let riscv_memory_eas : memory_write_eas =
[ ("MEMea", (MEA Write_plain memory_parameter_transformer));
("MEMea_release", (MEA Write_RISCV_release memory_parameter_transformer));
("MEMea_strong_release", (MEA Write_RISCV_strong_release memory_parameter_transformer));
("MEMea_conditional", (MEA Write_RISCV_conditional memory_parameter_transformer));
("MEMea_conditional_release", (MEA Write_RISCV_conditional_release memory_parameter_transformer));
("MEMea_conditional_strong_release",
(MEA Write_RISCV_conditional_strong_release
memory_parameter_transformer));
]
let riscv_memory_vals : memory_write_vals =
[ ("MEMval", (MV memory_parameter_transformer_option_address Nothing));
("MEMval_release", (MV memory_parameter_transformer_option_address Nothing));
("MEMval_strong_release", (MV memory_parameter_transformer_option_address Nothing));
("MEMval_conditional", (MV memory_parameter_transformer_option_address Nothing));
("MEMval_conditional_release",(MV memory_parameter_transformer_option_address Nothing));
("MEMval_conditional_strong_release",
(MV memory_parameter_transformer_option_address Nothing));
]
let riscv_speculate_conditional_success : 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_conditional_success", (ER (Just f)))
let riscv_barrier_functions =
[ ("MEM_fence_rw_rw", Barrier_RISCV_rw_rw);
("MEM_fence_r_rw", Barrier_RISCV_r_rw);
("MEM_fence_r_r", Barrier_RISCV_r_r);
("MEM_fence_rw_w", Barrier_RISCV_rw_w);
("MEM_fence_w_w", Barrier_RISCV_w_w);
("MEM_fence_i", Barrier_RISCV_i);
]
|
