Skip to content

Commit 536c1df

Browse files
author
Shale Xiong
committed
[gen] Make wildcard edges only in diy7 and diycross7.
1 parent 84a1a4d commit 536c1df

17 files changed

Lines changed: 55 additions & 36 deletions

gen/CArch_gen.ml

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -243,7 +243,7 @@ let pp_rmw compat = function
243243

244244
let is_one_instruction _ = true
245245

246-
let fold_rmw f r = let r = f Add r in f Exch r
246+
let fold_rmw _b f r = let r = f Add r in f Exch r
247247

248248
let fold_rmw_compat f r = f Exch r
249249

gen/CCompile_gen.ml

Lines changed: 2 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -30,6 +30,7 @@ module type Config = sig
3030
val typ : TypBase.t
3131
val cpp : bool
3232
val docheck : bool
33+
val wildcard : bool
3334
end
3435

3536
module Make(O:Config) : Builder.S
@@ -54,6 +55,7 @@ module Make(O:Config) : Builder.S
5455
(struct
5556
let variant = O.variant
5657
let naturalsize = TypBase.get_size O.typ
58+
let wildcard = O.wildcard
5759
end)
5860
(A)
5961

gen/RISCVArch_gen.ml

Lines changed: 2 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -104,15 +104,15 @@ module Make
104104
let k = f AcqRel k in
105105
k
106106

107-
let fold_rmw f k =
107+
let fold_rmw _b f k =
108108
let fold1 f k = fold_mo f (f Rlx k) in
109109
fold1
110110
(fun m1 k -> fold1 (fun m2 k -> f (Atomic (m1,m2)) k) k)
111111
k
112112

113113
let fold_non_mixed f k =
114114
let k = fold_mo (fun mo k -> f (MO mo) k) k in
115-
fold_rmw f k
115+
fold_rmw false f k
116116

117117
let fold_atom f k =
118118
let k = fold_mixed f k in

gen/alt.ml

Lines changed: 2 additions & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -31,6 +31,7 @@ module type AltConfig = sig
3131
val variant : Variant_gen.t -> bool
3232
type fence
3333
val cumul : fence list Config.cumul
34+
val wildcard : bool
3435
end
3536

3637
module Make(C:Builder.S)
@@ -737,7 +738,7 @@ module Make(C:Builder.S)
737738
let fold_ie f k = f (Int) (f (Ext) k)
738739
let fold_dir f k = f Irr k (* expand later ! *)
739740
let fold_dir2 f = fold_dir (fun i1 k -> fold_dir (f i1) k)
740-
let fold_sd = Code.fold_sd
741+
let fold_sd = Code.fold_sd O.wildcard
741742
let fold_sd_dir2 f =
742743
fold_sd
743744
(fun sd -> fold_dir2 (fun d1 d2 -> f sd d1 d2))

gen/common/AArch64Arch_gen.ml

Lines changed: 3 additions & 3 deletions
Original file line numberDiff line numberDiff line change
@@ -791,17 +791,17 @@ let fold_aop f r =
791791
let r = f A_CLR r in
792792
r
793793

794-
let fold_rmw f r =
794+
let fold_rmw wildcard f r =
795795
let r = f LrSc r in
796796
let r = f Swp r in
797797
let r = f Cas r in
798798
let r = fold_aop (fun op r -> f (LdOp op) r) r in
799799
let r = fold_aop (fun op r -> f (StOp op) r) r in
800-
let r = f AllAmo r in
800+
let r = if wildcard then f AllAmo r else r in
801801
r
802802

803803
let all_concrete_rmw =
804-
fold_rmw ( fun rmw acc ->
804+
fold_rmw false ( fun rmw acc ->
805805
if rmw <> AllAmo && rmw <> LrSc then rmw :: acc else acc
806806
) []
807807
let expand_rmw rmw = match rmw with

gen/common/code.ml

Lines changed: 5 additions & 5 deletions
Original file line numberDiff line numberDiff line change
@@ -129,11 +129,11 @@ let seq_sd sd1 sd2 =
129129
| Diff,_|_,Diff -> Diff
130130

131131
let fold_ie f r = f Ext (f Int r)
132-
let fold_sd f r = f UnspecLoc (f Diff (f Same r))
133-
let fold_extr f r = f (Dir W) (f (Dir R) (f Irr r))
134-
let fold_sd_extr f = fold_sd (fun sd -> fold_extr (fun e -> f sd e))
135-
let fold_sd_extr_extr f =
136-
fold_sd_extr (fun sd e1 -> fold_extr (fun e2 -> f sd e1 e2))
132+
let fold_sd wildcard f r = let r = if wildcard then (f UnspecLoc r) else r in f Diff (f Same r)
133+
let fold_extr wildcard f r = let r = if wildcard then (f Irr r) else r in f (Dir W) (f (Dir R) r)
134+
let fold_sd_extr wildcard f = fold_sd wildcard (fun sd -> fold_extr wildcard (fun e -> f sd e))
135+
let fold_sd_extr_extr wildcard f =
136+
fold_sd_extr wildcard (fun sd e1 -> fold_extr wildcard (fun e2 -> f sd e1 e2))
137137

138138
type check =
139139
| Default | Sc | Uni | Thin | Critical

gen/common/code.mli

Lines changed: 5 additions & 4 deletions
Original file line numberDiff line numberDiff line change
@@ -70,10 +70,11 @@ val seq_sd : sd -> sd -> sd
7070
val is_same_loc : sd -> bool
7171
val is_both_loc : sd -> bool
7272
val fold_ie : (ie -> 'a -> 'a) -> 'a -> 'a
73-
val fold_extr : (extr -> 'a -> 'a) -> 'a -> 'a
74-
val fold_sd : (sd -> 'a -> 'a) -> 'a -> 'a
75-
val fold_sd_extr : (sd -> extr -> 'a -> 'a) -> 'a -> 'a
76-
val fold_sd_extr_extr : (sd -> extr -> extr -> 'a -> 'a) -> 'a -> 'a
73+
(* The first boolean indicates on wildcard syntax *)
74+
val fold_extr : bool -> (extr -> 'a -> 'a) -> 'a -> 'a
75+
val fold_sd : bool -> (sd -> 'a -> 'a) -> 'a -> 'a
76+
val fold_sd_extr : bool -> (sd -> extr -> 'a -> 'a) -> 'a -> 'a
77+
val fold_sd_extr_extr : bool -> (sd -> extr -> extr -> 'a -> 'a) -> 'a -> 'a
7778

7879
type check =
7980
| Default | Sc | Uni | Thin | Critical | Free

gen/common/edge.ml

Lines changed: 16 additions & 10 deletions
Original file line numberDiff line numberDiff line change
@@ -20,6 +20,7 @@ module Config =
2020
struct
2121
let variant _ = false
2222
let naturalsize = TypBase.get_size TypBase.default
23+
let wildcard = false
2324
end
2425

2526
let dbg = 0
@@ -35,6 +36,7 @@ module type S = sig
3536
type atom
3637
module PteVal : PteVal_gen.S with type pte_atom = atom
3738
type rmw
39+
val wildcard : bool
3840

3941
val pp_atom : atom -> string
4042
val tr_value : atom option -> Code.v -> Code.v
@@ -160,6 +162,7 @@ module
160162
sig
161163
val variant : Variant_gen.t -> bool
162164
val naturalsize : MachSize.sz
165+
val wildcard : bool
163166
end)
164167
(F:Fence.S) : S
165168
with
@@ -175,6 +178,7 @@ and type rmw = F.rmw = struct
175178
let do_kvm = Variant_gen.is_kvm Cfg.variant
176179
let do_disjoint = Cfg.variant Variant_gen.MixedDisjoint
177180
let do_strict_overlap = Cfg.variant Variant_gen.MixedStrictOverlap
181+
let wildcard = Cfg.wildcard
178182

179183
let debug = false
180184
open Code
@@ -389,24 +393,25 @@ let fold_tedges f r =
389393
let r = fold_ie (fun ie -> f (Rf ie)) r in
390394
let r = fold_ie (fun ie -> f (Fr ie)) r in
391395
let r = fold_ie (fun ie -> f (Ws ie)) r in
392-
let r = F.fold_rmw (fun rmw -> f (Rmw rmw)) r in
393-
let r = fold_sd_extr_extr (fun sd e1 e2 r -> f (Po (sd,e1,e2)) r) r in
396+
let r = F.fold_rmw wildcard (fun rmw -> f (Rmw rmw)) r in
397+
let r = fold_sd_extr_extr wildcard (fun sd e1 e2 r -> f (Po (sd,e1,e2)) r) r in
394398
let r = F.fold_all_fences (fun fe -> f (Insert fe)) r in
395399
let r = f Store r in
396400
let r =
397401
F.fold_all_fences
398402
(fun fe ->
399-
fold_sd_extr_extr
403+
fold_sd_extr_extr wildcard
400404
(fun sd e1 e2 -> f (Fenced (fe,sd,e1,e2)))) r in
401405
let r =
402406
F.fold_dpr
403-
(fun dp -> fold_sd (fun sd -> f (Dp (dp,sd,Dir R)))) r in
407+
(fun dp -> fold_sd wildcard (fun sd -> f (Dp (dp,sd,Dir R)))) r in
404408
let r =
405409
F.fold_dpw
406-
(fun dp -> fold_sd (fun sd -> f (Dp (dp,sd,Dir W)))) r in
410+
(fun dp -> fold_sd wildcard (fun sd -> f (Dp (dp,sd,Dir W)))) r in
407411
let r =
408-
F.fold_dpw
409-
(fun dp -> fold_sd (fun sd -> f (Dp (dp,sd,Irr)))) r in
412+
if wildcard then F.fold_dpw
413+
(fun dp -> fold_sd wildcard (fun sd -> f (Dp (dp,sd,Irr)))) r
414+
else r in
410415
let r = f Id r in
411416
let r = f (Node R) (f (Node W) r) in
412417
let r = f Hat r in
@@ -586,7 +591,7 @@ let fold_tedges f r =
586591

587592
let () =
588593
four_times_iter_edges false iter_edges;
589-
fold_sd_extr_extr
594+
fold_sd_extr_extr wildcard
590595
(fun sd e1 e2 () ->
591596
add_lxm_edge
592597
(pp_strong sd e1 e2) (plain_edge (Fenced (F.strong,sd,e1,e2)))) () ;
@@ -596,9 +601,10 @@ let fold_tedges f r =
596601
add_lxm_edge
597602
(pp_dp_default tag sd e)
598603
(plain_edge (Dp (dp,sd,e))) in
599-
fold_sd
604+
fold_sd wildcard
600605
(fun sd () ->
601-
fill_opt "Dp" F.ddr_default sd Irr ;
606+
if wildcard then fill_opt "Dp" F.ddr_default sd Irr ;
607+
if wildcard then fill_opt "Ctrl" F.ctrlr_default sd Irr ;
602608
fill_opt "Dp" F.ddr_default sd (Dir R) ;
603609
fill_opt "Ctrl" F.ctrlr_default sd (Dir R) ;
604610
fill_opt "Dp" F.ddw_default sd (Dir W) ;

gen/common/rmw.mli

Lines changed: 2 additions & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -22,7 +22,8 @@ module type S = sig
2222

2323
val pp_rmw : bool (* backward compatibility *) -> rmw -> string
2424
val is_one_instruction : rmw -> bool
25-
val fold_rmw : (rmw -> 'a -> 'a) -> 'a -> 'a
25+
(* the first boolean indicates if including wildcard syntax *)
26+
val fold_rmw : bool -> (rmw -> 'a -> 'a) -> 'a -> 'a
2627
(* Second round of fold, for rmw with back compatible name *)
2728
val fold_rmw_compat : (rmw -> 'a -> 'a) -> 'a -> 'a
2829
val applies_atom_rmw : rmw -> rmw_atom option -> rmw_atom option -> bool

gen/compileCommon.ml

Lines changed: 2 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -24,6 +24,7 @@ module type Config = sig
2424
val hexa : bool
2525
val moreedges : bool
2626
val variant : Variant_gen.t -> bool
27+
val wildcard : bool
2728
end
2829

2930
module type S = sig
@@ -59,6 +60,7 @@ module Make(C:Config) (A:Arch_gen.S) = struct
5960
(struct
6061
let variant = C.variant
6162
let naturalsize = TypBase.get_size C.typ
63+
let wildcard = C.wildcard
6264
end)
6365
(A)
6466

0 commit comments

Comments
 (0)