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
98
99
100
101
102
|
(****************************************************************************)
(* the diy toolsuite *)
(* *)
(* Jade Alglave, University College London, UK. *)
(* Luc Maranget, INRIA Paris-Rocquencourt, France. *)
(* *)
(* Copyright 2021-present Institut National de Recherche en Informatique et *)
(* en Automatique, ARM Ltd and the authors. All rights reserved. *)
(* *)
(* This software is governed by the CeCILL-B license under French law and *)
(* abiding by the rules of distribution of free software. You can use, *)
(* modify and/ or redistribute the software under the terms of the CeCILL-B *)
(* license as circulated by CEA, CNRS and INRIA at the following URL *)
(* "http://www.cecill.info". We also give a copy in LICENSE.txt. *)
(****************************************************************************)
module type S = sig
type t
val sets : (string * t list) list
val pp : t -> string
val parse : MiscParser.fault_type -> t
val compare : t -> t -> int
end
module type AArch64Sig = sig
type mmu_t =
| Translation
| AccessFlag
| Permission
type t =
| MMU of mmu_t
| TagCheck
| UndefinedInstruction
| SupervisorCall
include S with type t := t
end
module AArch64 = struct
type mmu_t =
| Translation
| AccessFlag
| Permission
let pp_mmu_t = function
| Translation -> "Translation"
| AccessFlag -> "AccessFlag"
| Permission -> "Permission"
type t =
| MMU of mmu_t
| TagCheck
| UndefinedInstruction
| SupervisorCall
let sets = [
"MMU", [MMU Translation;
MMU AccessFlag;
MMU Permission];
"Translation", [MMU Translation];
"AccessFlag", [MMU AccessFlag];
"Permission", [MMU Permission];
"TagCheck", [TagCheck];
"UndefinedInstruction",[UndefinedInstruction];
"SupervisorCall", [SupervisorCall];
]
let pp = function
| MMU m -> Printf.sprintf "MMU:%s" (pp_mmu_t m)
| TagCheck -> "TagCheck"
| UndefinedInstruction -> "UndefinedInstruction"
| SupervisorCall -> "SupervisorCall"
let parse = function
| "MMU:Translation" -> MMU Translation
| "MMU:AccessFlag" -> MMU AccessFlag
| "MMU:Permission" -> MMU Permission
| "TagCheck" -> TagCheck
| "UndefinedInstruction" -> UndefinedInstruction
| "SupervisorCall" -> SupervisorCall
| _ as s -> Warn.user_error "%s not a valid fault type" s
let is s = try ignore (parse s); true with _ -> false
let compare ft1 ft2 = Misc.polymorphic_compare ft1 ft2
end
module No = struct
type t = unit
let sets = []
let pp () = "Default"
let parse _ = Warn.user_error "Fault types not supported"
let compare _ _ = Warn.user_error "Fault types not supported"
end
let is = AArch64.is
|
