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
103
104
105
106
107
108
109
110
111
112
113
114
115
116
117
|
(****************************************************************************)
(* the diy toolsuite *)
(* *)
(* Jade Alglave, University College London, UK. *)
(* Luc Maranget, INRIA Paris-Rocquencourt, France. *)
(* *)
(* Copyright 2010-present Institut National de Recherche en Informatique et *)
(* en Automatique 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 Config = sig
val eieio : bool
val naturalsize : MachSize.sz
val moreedges : bool
end
(* Default: know about eieio and word size *)
module Config =
struct
let eieio = true
let naturalsize = MachSize.Word
let moreedges = false
end
module Make(C:Config) =
struct
include PPCBase
let tr_endian x = MachSize.tr_endian C.naturalsize x
module ScopeGen = ScopeGen.NoGen
include MachAtom.Make
(struct
let naturalsize = Some C.naturalsize
let endian = endian
let fullmixed = C.moreedges
end)
module PteVal = PteVal_gen.No(struct type arch_atom = atom end)
(**********)
(* Fences *)
(**********)
type fence = Sync | LwSync | ISync | Eieio
let is_isync = function
| ISync -> true
| _ -> false
let compare_fence = compare
let default = Sync
let strong = default
let pp_fence = function
| Sync -> "Sync"
| LwSync -> "LwSync"
| ISync -> "ISync"
| Eieio -> "Eieio"
let fold_cumul_fences =
if C.eieio then fun f r -> f Sync (f LwSync (f Eieio r))
else fun f r -> f Sync (f LwSync r)
let fold_all_fences f r = f ISync (fold_cumul_fences f r)
let fold_some_fences = fold_cumul_fences
open Code
let orders f d1 d2 = match f,d1,d2 with
| Sync,_,_ -> true
| LwSync,W,R -> false
| LwSync,_,_ -> true
| ISync,_,_ -> false
| Eieio,W,W -> true
| Eieio,_,_ -> false
let var_fence f r = f default r
(********)
(* Deps *)
(********)
include Dep
let pp_dp = function
| ADDR -> "Addr"
| DATA -> "Data"
| CTRL -> "Ctrl"
| CTRLISYNC -> "CtrlIsync"
(*******)
(* RWM *)
(*******)
include Exch.LxSx(struct type arch_atom = atom end)
include NoEdge
include
ArchExtra_gen.Make
(struct
type arch_reg = reg
let is_symbolic = function
| Symbolic_reg _ -> true
| _ -> false
let pp_reg = pp_reg
let pp_i _ = assert false
let free_registers = allowed_for_symb
include NoSpecial
end)
end
|
