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
118
119
120
121
122
123
124
125
126
127
128
|
(****************************************************************************)
(* 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. *)
(****************************************************************************)
(** Define PPC architecture *)
module Make (C:Arch_herd.Config) (V:Value.S)
=
struct
include PPCBase
let is_amo _ = false
let pp_barrier_short = pp_barrier
let reject_mixed = false
type lannot = bool (* atomicity *)
let get_machsize _ = V.Cst.Scalar.machsize
let empty_annot = false
let is_atomic annot = annot
let is_barrier b1 b2 = barrier_compare b1 b2 = 0
let ifetch_value_sets = []
let barrier_sets =
[
"SYNC",is_barrier Sync;
"ISYNC",is_barrier Isync;
"LWSYNC",is_barrier Lwsync;
"EIEIO",is_barrier Eieio;
]
let cmo_sets = []
let annot_sets = ["X",is_atomic]
let is_isync = is_barrier Isync
let pp_isync = "isync"
let pp_annot annot =
if annot then "*" else ""
include Explicit.No
include PteValSets.No
(* Now global locations, that include reservations *)
module V = V
let mem_access_size = function
| Pnop
| Padd _ | Psub _ | Psubf _ | Por _
| Pand _ | Pxor _ | Pmull _ | Pdiv _
| Paddi _ | Paddis _ | Pori _ | Pandi _ | Pxori _ | Pmulli _
| Prlwinm _ | Prlwimi _ | Pclrldi _
| Pli _ | Pb _ | Pbcc _ | Pcmpwi _ | Pcmpw _ | Plis _
| Pmr _ | Psync | Peieio | Pisync | Plwsync
| Pcmplwi _ | Pextsw _
| Pdcbf _ | Pblr | Pnor _ | Pneg _ | Pslw _
| Psrawi _| Psraw _ | Pbl _ | Pmtlr _ | Pmflr _ | Pmfcr _
| Plmw _ | Pstmw _ | Pcomment _
-> None
| Plwzu _ | Plwa _ | Pstwu _ | Plwarx _ | Pstwcx _
-> Some MachSize.Word
| Pload (sz,_,_,_) | Ploadx (sz,_,_,_) | Plwax (sz,_,_,_)
| Pstore (sz,_,_,_) | Pstorex (sz,_,_,_)
-> Some sz
include NoSemEnv
include NoLevelNorTLBI
include ArchExtra_herd.Make(C)
(struct
module V = V
let endian = endian
type arch_reg = reg
let pp_reg = pp_reg
let reg_compare = reg_compare
let fromto_of_instr _ = None
let get_val _ v = v
module FaultType=FaultType.No
end)
module MemType=MemoryType.No
module NoConf = struct
type v = V.v
type loc = location
type value_set = V.ValueSet.t
type solution = V.solution
type arch_lannot = lannot
type arch_explicit = explicit
end
module ArchAction = ArchAction.No(NoConf)
module Barrier = struct
type a = barrier
let a_to_b a =
let open AllBarrier in
match a with
| Sync -> SYNC
| Lwsync -> LWSYNC
| Isync -> ISYNC
| Eieio -> EIEIO
let pp_isync = "isync"
end
module CMO = Cmo.No
end
|
