include "ncos.cat"
let roots(r) = domain(r) \ range(r)
let succs (e,r) = range ([e];r)
let mapset2rel f =
let rec map_rec xs =
match xs
with
|| {} ->
0
|| x ++ xs ->
f x | map_rec xs
end in
map_rec
let mapset2set f =
let rec map_rec xs =
match xs
with
|| {} -> {}
|| x ++ xs ->
f x | map_rec xs
end in
map_rec
let poDorW = [PoD|W];po;[PoD|W]
let nextDorW = poDorW \ (poDorW;poDorW)
let DpoDorW = [PoD];poDorW
let addD d =
let rec do_rec ws =
match ws
with
|| {} ->
fun k -> k
|| w ++ ws ->
let kws = do_rec ws
in
fun k -> (d,w) ++ kws k
end in do_rec
let addifequiv (equiv,ws0) = mapset2set (
fun w -> succs (w,equiv) & ws0)
let combine (equiv,ws1,ws2) =
addifequiv (equiv,ws1) ws2 | addifequiv (equiv,ws2) ws1
let rec case_disjunction (equiv,e) =
match { e } & PoD
with
|| {} ->
let (ws,dw) = write_acc (equiv, (succs (e,nextDorW)))
in
(e ++ ws,dw)
|| d ++ es ->
let (ws,dw) = keep_equiv_writes (equiv, (succs (d,nextDorW)))
in
(ws,addD d ws dw)
end
and write_acc (equiv,es) =
match es
with
|| {} -> ({},
0)
|| e ++ es ->
let (ws_e,dw_e) = case_disjunction (equiv, e)
and (ws_es,dw_es) = write_acc (equiv, es)
in
(ws_e|ws_es, dw_e|dw_es)
end
and keep_equiv_writes (equiv,es) =
match es
with
|| {} -> ({},
0)
|| e ++ es ->
match es
with
|| {} -> case_disjunction(equiv,e)
|| f ++ fs ->
let (ws_e,dw_e) = case_disjunction(equiv,e)
and (ws_es,dw_es) = keep_equiv_writes(equiv,es)
in
(combine (equiv,ws_e,ws_es), dw_e|dw_es)
end
end
let zyva equiv =
mapset2rel
(
fun r ->
let (ws,dw) = case_disjunction(equiv,r)
in dw)
let intrinsic = (iico_data | iico_ctrl)+
let udr r = domain r | range r
let generated-by-stxr = udr(same-instr;[range(rmw)])
let rf-reg-restrict =
let NW = ~generated-by-stxr
in
[NW];rf-reg
let dd = (rf-reg | intrinsic)+
let to-PoD = [R]; dd; [PoD]
let pre-ctrl = to-PoD; po; [W]
let Dmins = roots(DpoDorW)
let Dm=Dmins*Dmins
let always-exec equiv =
let DW = zyva equiv Dmins
in
to-PoD; DW
let ctrlequiv equiv = pre-ctrl \ (always-exec equiv)