diff --git a/catalogue/dependencies/cats/aarch64.cat b/catalogue/dependencies/cats/aarch64.cat new file mode 100644 index 000000000..cb2e23eb4 --- /dev/null +++ b/catalogue/dependencies/cats/aarch64.cat @@ -0,0 +1,123 @@ +AArch64 "ARMv8 AArch64" +catdep (* This option tells that the cat file computes dependencies *) + +(* + * Include the cos.cat file shipped with herd. + * This builds the co relation as a total order over writes to the same + * location and then consequently defines the fr relation using co and + * rf. + *) +include "cos.cat" + +(* + * Include aarch64fences.cat to define barriers. + *) +include "aarch64fences.cat" + +(* + * Include aarch64deps.cat to define dependencies. + *) +include "aarch64deps-pick.cat" + +(* Show relations in generated diagrams *) +include "aarch64show.cat" + +(* + * As a restriction of the model, all observers are limited to the same + * inner-shareable domain. Consequently, the ISH, OSH and SY barrier + * options are all equivalent to each other. + *) +let dsb.full = DSB.ISH | DSB.OSH | DSB.SY +let dsb.ld = DSB.ISHLD | DSB.OSHLD | DSB.LD +let dsb.st = DSB.ISHST | DSB.OSHST | DSB.ST + +(* + * A further restriction is that standard litmus tests are unable to + * distinguish between DMB and DSB instructions, so the model treats + * them as equivalent to each other. + *) +let dmb.full = DMB.ISH | DMB.OSH | DMB.SY | dsb.full +let dmb.ld = DMB.ISHLD | DMB.OSHLD | DMB.LD | dsb.ld +let dmb.st = DMB.ISHST | DMB.OSHST | DMB.ST | dsb.st + +(* Flag any use of shareability options, due to the restrictions above. *) +flag ~empty (dmb.full | dmb.ld | dmb.st) \ + (DMB.SY | DMB.LD | DMB.ST | DSB.SY | DSB.LD | DSB.ST) + as Assuming-common-inner-shareable-domain + +(* Intrinsic order *) +let intrinsic = (iico_data|iico_ctrl)+ + +(* Coherence-after *) +let ca = fr | co + +(* Local read successor *) +let lrs = [W]; (po-loc \ (po-loc;[W];po-loc)) ; [R] + +(* Local write successor *) +let lws = po-loc; [W] + +(* Observed-by *) +let obs = rfe | fre | coe + +(* Read-modify-write *) +let rmw = lxsx | amo + +(* Dependency-ordered-before *) +let dob = addr | data | ctrl; [W] + | (ctrl | (addr; po)); [ISB]; po; [M] + | addr; po; [W] + | (addr | data); lrs +show ctrl;[M] as ctrl + +(* Pick-ordered-before *) +let pob = pick-dep; [W] + | (pick-ctrl-dep | pick-addr-dep; po); [ISB]; po; [M] + | pick-addr-dep; [M]; po; [W] + +(* Atomic-ordered-before *) +let aob = rmw + | rmw; lrs; [A | Q] + +(* Barrier-ordered-before *) +let bob = po; [dmb.full]; po + | po; ([A];amo;[L]); po + | [L]; po; [A] + | [R\NoRet]; po; [dmb.ld]; po + | [A | Q]; po + | [W]; po; [dmb.st]; po; [W] + | po; [L] + +(* Tag-ordered-before *) +let tob = [R & T]; iico_data; [BR]; iico_ctrl; [M \ T] + +(* Locally-ordered-before *) +let rec lob = lws; si + | dob + | pob + | aob + | bob + | tob + | lob; lob +let pick-lob = pick-basic-dep; lob; [W] + +(* Ordered-before *) +let rec ob = obs; si + | lob + | pick-lob + | ob; ob + +(* Tag-location-ordered *) +let tlo = [R & T]; tob; loc; tob^-1; [R & T] + +(* Internal visibility requirement *) +let po-loc = + let Exp = M\domain(tob) in + (po-loc & Exp*Exp) | (po & tlo) +acyclic po-loc | ca | rf as internal + +(* External visibility requirement *) +irreflexive ob as external + +(* Atomic: Basic LDXR/STXR constraint to forbid intervening writes. *) +empty rmw & (fre; coe) as atomic diff --git a/catalogue/dependencies/cats/aarch64deps-down-one-leg.cat b/catalogue/dependencies/cats/aarch64deps-down-one-leg.cat new file mode 100644 index 000000000..786dd2cfc --- /dev/null +++ b/catalogue/dependencies/cats/aarch64deps-down-one-leg.cat @@ -0,0 +1,43 @@ +(* Intrinsic dependencies *) +let intrinsic = (iico_data|iico_ctrl)+ + +(* Dependency through register *) +let generated-by-stxr = udr(same-instr;[range(lxsx)]) +let rf-reg-no-stxr = + let NW = ~generated-by-stxr in + [NW];rf-reg +let dd = (rf-reg-no-stxr | intrinsic)+ + +(* The relation to-PoD is a dependency through register + to a point of divergence*) +let to-PoD = [R]; dd; [PoD] + +(** Data and Address dependencies *) +let data = [R]; dd; [DATA]; intrinsic; [W] +let addrW = [R]; dd; [NDATA]; intrinsic; [W] +let addrR = + let dd-no-interv-PoD = dd \ (to-PoD;dd) in + [R]; dd-no-interv-PoD; [NDATA]; intrinsic; [R] +let addr = addrW | addrR + +(** Control dependency *) +(* Pre-control dependency *) +let pre-ctrl = to-PoD; po + +(* Equivalent writes *) +let antecedent = + let immediate-lws = singlestep([W];po-loc;[W]) in + (intrinsic|rf-reg|lrs|immediate-lws)^-1 + +let pre-equiv-evts = + let rdw-ext = + let wwloc = ((W * W) & loc) \ id in + ((rfe^-1;wwloc;rf)|(rf^-1;wwloc;rfe)) + in same-static\rdw-ext +show pre-equiv-evts \ id as pre-equiv-evts + +let equivalent-writes = (W*W) & bisimulation(antecedent,pre-equiv-evts) +show equivalent-writes \ id as equivalent-writes + +(* Control dependency *) +let ctrl = pre-ctrl \ (always-executed(to-PoD,equivalent-writes)) diff --git a/catalogue/dependencies/cats/aarch64deps-down-two-legs.cat b/catalogue/dependencies/cats/aarch64deps-down-two-legs.cat new file mode 100644 index 000000000..401657d90 --- /dev/null +++ b/catalogue/dependencies/cats/aarch64deps-down-two-legs.cat @@ -0,0 +1,25 @@ +(* Intrinsic dependencies *) +let intrinsic = (iico_data|iico_ctrl)+ + +(* Dependency through register *) +let rf-reg-no-stxr = + rf-reg \ ([W & range(lxsx)];rf-reg) + +let dd = + let r = (rf-reg-no-stxr | intrinsic)* in + r;rf-reg-no-stxr;r + +(* The relation to-BR is a dependency through register + to a Branching effect *) +let to-BR = [R]; dd; [BR] + +(** Data and Address dependencies *) +let data = ([R]; dd; [DATA]; intrinsic; [W]) \ same-instance +let addrW = [R]; dd; [NDATA]; intrinsic; [W] +let addrR = + let dd-no-interv-BR = dd \ (to-BR;dd) in + [R]; dd-no-interv-BR; [NDATA]; intrinsic; [R] +let addr = (addrW | addrR) \ same-instance + +(** Control dependencies *) +let ctrl = to-BR; po diff --git a/catalogue/dependencies/cats/aarch64deps-pick.cat b/catalogue/dependencies/cats/aarch64deps-pick.cat new file mode 100644 index 000000000..c1108093a --- /dev/null +++ b/catalogue/dependencies/cats/aarch64deps-pick.cat @@ -0,0 +1,32 @@ +(* Dependency through registers and memory *) +let rec dtrm = + rf-reg \ ([W & range(lxsx)];rf-reg) + | rfi + | iico_data + | dtrm; dtrm + +let Reg=~M | ~BR +(** Data, Address and Control dependencies *) +let ADDR=NDATA +let basic-dep = + [R|Rreg]; dtrm? +let data = basic-dep; [DATA]; iico_data; [W] +let addr = basic-dep; [ADDR]; iico_data; [M] +let ctrl = basic-dep; [BR]; po + +(** Pick dependencies *) +let pick-basic-dep = + [R|Rreg]; dtrm?; [Reg]; iico_ctrl; [Reg]; dtrm? +let pick-addr-dep = + pick-basic-dep; [ADDR]; iico_data; [M] +let pick-data-dep = + pick-basic-dep; [DATA]; iico_data; [W] +let pick-ctrl-dep = + pick-basic-dep; [BR]; po +let pick-dep = +( + pick-basic-dep | + pick-addr-dep | + pick-data-dep | + pick-ctrl-dep +) diff --git a/catalogue/dependencies/cats/always-executed-writes.cat b/catalogue/dependencies/cats/always-executed-writes.cat new file mode 100644 index 000000000..eebc5b32a --- /dev/null +++ b/catalogue/dependencies/cats/always-executed-writes.cat @@ -0,0 +1,103 @@ +(* Cat file to compute always executed write effects *) + +(* Utilities *) + +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 + +(* Basic definitions *) +let poDorW = [PoD|W];po;[PoD|W] +let nextDorW = poDorW \ (poDorW;poDorW) + +let sibling = + let inv = nextDorW^-1 in + fun s -> ([s];inv;nextDorW;[s])\(id|inv|nextDorW) + +let DpoDorW = [PoD];poDorW + +(* Add pair dw for w in ws + More precisely: + addD d (ws,dw) = dw U {(d,w) | w in ws} +*) + +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 + +(* + Set combination: union of equiv-related sets +*) + +let addifequiv (equiv,ws0) = mapset2set (fun w -> succs (w,equiv) & ws0) + +let combine (equiv,ws1,ws2) = + addifequiv (equiv,ws1) ws2 | addifequiv (equiv,ws2) ws1 + +(* Tree scan: returns ws,dw, where ws is the set of writes always performed at +this level and dw is the relation from PoD to writes always performed *) + +let rec case_disjunction (equiv,e) = match { e } & PoD with +|| {} -> (* e is not a PoD, hence is a write *) + let (ws,dw) = write_acc (equiv, (succs (e,nextDorW))) in + (e ++ ws,dw) +|| d ++ es -> (* e is a PoD *) + let nexts = (succs (d,nextDorW)) in + match sibling(nexts) with + || {} -> (* Only one branch, nothing equivalent *) + ({},0) + || _e ++ _es -> + let (ws,dw) = keep_equiv_writes (equiv,nexts) in + (ws,addD d ws dw) + end +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 + +(* Warning, base case is on singleton *) +and keep_equiv_writes (equiv,es) = match es with + || {} -> ({},0) (* No successors, ie no W po-after, special case *) + || e ++ es -> + match es with + || {} -> case_disjunction(equiv,e) (* Singleton = base case *) + || 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 + +(* Final call *) +let zyva equiv = + mapset2rel + (fun r -> let (ws,dw) = case_disjunction(equiv,r) in dw) + +let Dmins = roots(DpoDorW) +let always-executed (to-PoD,equiv) = + let DW = zyva equiv Dmins in + to-PoD; DW diff --git a/catalogue/dependencies/tests/desired-kinds.txt b/catalogue/dependencies/tests/desired-kinds.txt new file mode 100644 index 000000000..0c4ee494a --- /dev/null +++ b/catalogue/dependencies/tests/desired-kinds.txt @@ -0,0 +1,54 @@ +MP+rel+CAS-addr Allow +MP+rel+CSEL-addr Allow +MP+rel+CSEL-addr2 Allow +LB+rel+CAS Forbid +LB+CSEL-rfi-data+DMB Forbid +S+rel+CSEL-data Forbid +S+rel+CSEL-data2 Forbid +MP+CSEL-rfi-addr-rfi-addr Allow +LB+CSEL-addr-po+DMB Forbid +LB+CSEL-data-po+DMB Allow +MP+rel+CSEL-rfi-data-rfi-addr Allow +S+rel+CSEL-rfi-data-rfi-addr Forbid +S+rel+CSEL-rfi-ctrl Forbid +T3 Forbid +T3-bis Forbid +S+DMB.ST+CSEL-ctrl Forbid +LB+rel+data Forbid +MP+rel+CSEL Allow +MP+rel+CSEL-rf-reg Forbid +WILL-7 Forbid +WILL-7dep Forbid +WILL-8 Allow +WILL-8+BIS Forbid +WILL-9 Allow +WILL-9B Forbid +WILL-9C Allow +WILL-10B Forbid +WILL-10C Forbid +WILL-11 Allow +WILL-12 Allow +WILL-12B Allow +WILL-13 Forbid +WILL-13B Allow +WILL-13-mod2 Allow +WILL-13-mod3 Forbid +WILL-13-mod4 Allow +WILL-14 Allow +WILL-14B Forbid +WILL-14B-corrected Forbid +WILL-14-controldep Allow +WILL-14B-controldep Forbid +WILL-LDAR Allow +WILL-newest Forbid +WILL-newest-mod Forbid +WILL-99 Forbid +WILL-99-excls Forbid +WILL-99-excls-RZR Forbid +WILL-99-STADD Forbid +WILL-21-01-29 Allow +2021-01-29-Richard Allow +2021-01-29-WILL-newest Forbid +2021-01-29-WILL-newest-noWZR Forbid +WILL-15-corrected Forbid +WILL-15-datadep-corrected Forbid diff --git a/catalogue/dependencies/tests/down-one-leg-kinds.txt b/catalogue/dependencies/tests/down-one-leg-kinds.txt new file mode 100644 index 000000000..aedc516e7 --- /dev/null +++ b/catalogue/dependencies/tests/down-one-leg-kinds.txt @@ -0,0 +1,67 @@ +2+2W+addr+dmb Allow +2+2W+xp+dmb Allow +H10X Allow +H10bX Allow +H11V Forbid +H11bQ Allow +H12CV Forbid +H12V Forbid +H13V Forbid +H14V Forbid +H15V Forbid +H16X Allow +H1CX Allow +H1X Allow +H2CV Forbid +H2V Forbid +H3CV Forbid +H3V Forbid +H3bCQ Allow +H3bQ Allow +H4CX Allow +H4X Allow +H5CV Forbid +H5V Forbid +H6CX Allow +H6X Allow +H7CX Allow +H7X Allow +H8CX Allow +H8X Allow +H8bCQ Allow +H8bQ Forbid +H8cQ Forbid +H9CV Forbid +H9V Forbid +LB6b Allow +LB6b2 Forbid +LB6b3 Forbid +MP-STXR Allow +MP-STXR-fail Allow +MP-STXR-success Allow +MP+DMB.ST+B Allow +MP+DMB.ST+B-EOR Forbid +MP+DMB.ST+CSEL Forbid +PPCOA4b Allow +PPOCA Allow +PPOCA5b Forbid +PPOCA6b Allow +S-STXR-success Forbid +STXR-ctrl Allow +STXR-ctrl1 Forbid +STXR-ctrl1a Forbid +STXR-ctrl1b Forbid +STXR-ctrl2 Forbid +STXR-ctrl3 Forbid +STXR-ctrla Allow +SpecCE-01 Forbid +SpecCE-02 Forbid +SpecCE-03 Allow +SpecCE-04 Allow +SpecCE-05 Allow +SpecCoiV Forbid +SpecCoiX Allow +SpecRfeX Allow +SpecRfiV Forbid +SpecRfiX Allow + diff --git a/catalogue/dependencies/tests/down-one-leg/2+2W+addr+dmb.litmus b/catalogue/dependencies/tests/down-one-leg/2+2W+addr+dmb.litmus new file mode 100644 index 000000000..881ed5a13 --- /dev/null +++ b/catalogue/dependencies/tests/down-one-leg/2+2W+addr+dmb.litmus @@ -0,0 +1,18 @@ +AArch64 2+2W+addr+dmb +"PodWWXP Wse DMB.SYdWW WsePX" +Generator=diyone7 (version 7.55+01(dev)) +Prefetch=0:x=F,0:y=W,1:y=F,1:x=W +Com=Ws Ws +Orig=PodWWXP Wse DMB.SYdWW WsePX +{ +0:X0=x; 0:X5=y; +1:X1=y; 1:X3=x; +} + P0 | P1 ; + MOV W1,#2 | MOV W0,#2 ; + LDXR W2,[X0] | STR W0,[X1] ; + STXR W3,W1,[X0] | DMB SY ; + AND W9,W3,#128 | MOV W2,#1 ; + MOV W4,#1 | STR W2,[X3] ; + STR W4,[X5,W9,SXTW] | ; +exists (x=2 /\ y=2 /\ 0:X3=0 /\ 0:X2=1) diff --git a/catalogue/dependencies/tests/down-one-leg/2+2W+xp+dmb.litmus b/catalogue/dependencies/tests/down-one-leg/2+2W+xp+dmb.litmus new file mode 100644 index 000000000..4241a578e --- /dev/null +++ b/catalogue/dependencies/tests/down-one-leg/2+2W+xp+dmb.litmus @@ -0,0 +1,15 @@ +AArch64 2+2W+xp+dmb +Prefetch=0:x=F,0:y=W,1:y=F,1:x=W +Com=Ws Ws +Orig=PodWWXP Wse DMB.SYdWW WsePX +{ +0:X0=x; 0:X5=y; +1:X1=y; 1:X3=x; +} + P0 | P1 ; + MOV W1,#2 | MOV W0,#2 ; + LDXR W2,[X0] | STR W0,[X1] ; + STXR W3,W1,[X0] | DMB SY ; + MOV W4,#1 | MOV W2,#1 ; + STR W4,[X5] | STR W2,[X3] ; +exists (x=2 /\ y=2 /\ 0:X3=0 /\ 0:X2=1) diff --git a/catalogue/dependencies/tests/down-one-leg/H10X.litmus b/catalogue/dependencies/tests/down-one-leg/H10X.litmus new file mode 100644 index 000000000..b5d3aa82e --- /dev/null +++ b/catalogue/dependencies/tests/down-one-leg/H10X.litmus @@ -0,0 +1,19 @@ +AArch64 H10X +{ +0:X1=x; 0:X3=y; +1:X1=y; 1:X3=x; 1:X5=z; 1:X7=a; +} +P0 | P1 ; +LDR W0,[X1] | LDR W0,[X1] ; + | CMP W0,#0 ; +MOV W2,#1 | MOV W2,#1 ; +STLR W2,[X3] | B.EQ over ; + | MOV W2,#2 ; + | over: ; + | LDR W4,[X5] ; + | EOR W9,W4,W4 ; + | ADD W6,W6,#1 ; + | STR W6,[X7] ; + | MOV W8,#7 ; + | STR W8,[X3] ; +exists (0:X0=7 /\ 1:X0=1) diff --git a/catalogue/dependencies/tests/down-one-leg/H10bX.litmus b/catalogue/dependencies/tests/down-one-leg/H10bX.litmus new file mode 100644 index 000000000..22da7f78b --- /dev/null +++ b/catalogue/dependencies/tests/down-one-leg/H10bX.litmus @@ -0,0 +1,19 @@ +AArch64 H10bX +{ +0:X1=x; 0:X3=y; +1:X1=y; 1:X3=x; 1:X5=z; +} +P0 | P1 ; +LDR W0,[X1] | LDR W0,[X1] ; + | CMP W0,#0 ; +MOV W2,#1 | MOV W2,#1 ; +STLR W2,[X3] | B.EQ over ; + | MOV W2,#2 ; + | over: ; + | LDR W4,[X1] ; + | EOR W9,W4,W4 ; + | ADD W6,W6,#1 ; + | STR W6,[X5] ; + | MOV W8,#7 ; + | STR W8,[X3] ; +exists (0:X0=7 /\ 1:X0=1) diff --git a/catalogue/dependencies/tests/down-one-leg/H11V.litmus b/catalogue/dependencies/tests/down-one-leg/H11V.litmus new file mode 100644 index 000000000..e5d273ea2 --- /dev/null +++ b/catalogue/dependencies/tests/down-one-leg/H11V.litmus @@ -0,0 +1,17 @@ +AArch64 H11V +{ +0:X1=x; 0:X3=y; +1:X1=y; 1:X3=x; 1:X5=z; +} +P0 | P1 ; +LDR W0,[X1] | LDR W0,[X1] ; + | CMP W0,#0 ; +MOV W2,#1 | MOV W2,#1 ; +STLR W2,[X3] | B.EQ over ; + | MOV W2,#2 ; + | STR W4,[X5] ; + | DMB ST ; + | over: ; + | MOV W8,#7 ; + | STR W8,[X3] ; +exists (0:X0=7 /\ 1:X0=1) diff --git a/catalogue/dependencies/tests/down-one-leg/H11bQ.litmus b/catalogue/dependencies/tests/down-one-leg/H11bQ.litmus new file mode 100644 index 000000000..4c84f58ab --- /dev/null +++ b/catalogue/dependencies/tests/down-one-leg/H11bQ.litmus @@ -0,0 +1,17 @@ +AArch64 H11bQ +{ +0:X1=x; 0:X3=y; +1:X1=y; 1:X3=x; 1:X5=z; +} +P0 | P1 ; +LDR W0,[X1] | LDR W0,[X1] ; + | CMP W0,#0 ; +MOV W2,#1 | MOV W2,#1 ; +STLR W2,[X3] | B.EQ over ; + | MOV W2,#2 ; + | over: ; + | STR W4,[X5] ; + | DMB ST ; + | MOV W8,#7 ; + | STR W8,[X3] ; +exists (0:X0=7 /\ 1:X0=1) diff --git a/catalogue/dependencies/tests/down-one-leg/H12CV.litmus b/catalogue/dependencies/tests/down-one-leg/H12CV.litmus new file mode 100644 index 000000000..856bd38f1 --- /dev/null +++ b/catalogue/dependencies/tests/down-one-leg/H12CV.litmus @@ -0,0 +1,15 @@ +AArch64 H12CV +{ +0:X1=x; 0:X3=y; +1:X1=y; 1:X3=x; +} +P0 | P1 ; +MOV W0,#1 | ; +STR W0,[X1] | LDR W0,[X1] ; + | CMP W0,#0 ; +MOV W2,#1 | MOV W5,#1 ; +STLR W2,[X3] | MOV W6,#2 ; + | CSEL W2,W5,W6,EQ ; + | ISB ; + | LDR W8,[X3] ; +exists (1:X0=1 /\ 1:X8=0) diff --git a/catalogue/dependencies/tests/down-one-leg/H12V.litmus b/catalogue/dependencies/tests/down-one-leg/H12V.litmus new file mode 100644 index 000000000..f197cdb5f --- /dev/null +++ b/catalogue/dependencies/tests/down-one-leg/H12V.litmus @@ -0,0 +1,16 @@ +AArch64 H12V +{ +0:X1=x; 0:X3=y; +1:X1=y; 1:X3=x; +} +P0 | P1 ; +MOV W0,#1 | ; +STR W0,[X1] | LDR W0,[X1] ; + | CMP W0,#0 ; +MOV W2,#1 | MOV W2,#1 ; +STLR W2,[X3] | B.EQ over ; + | MOV W2,#2 ; + | over: ; + | ISB ; + | LDR W8,[X3] ; +exists (1:X0=1 /\ 1:X8=0) diff --git a/catalogue/dependencies/tests/down-one-leg/H13V.litmus b/catalogue/dependencies/tests/down-one-leg/H13V.litmus new file mode 100644 index 000000000..8907aa7b8 --- /dev/null +++ b/catalogue/dependencies/tests/down-one-leg/H13V.litmus @@ -0,0 +1,17 @@ +AArch64 H13V +{ +0:X1=x; 0:X3=y; +1:X1=y; 1:X3=x; +} +P0 | P1 ; +LDR W0,[X1] | LDR W0,[X1] ; + | CMP W0,#0 ; +MOV W2,#1 | MOV W2,#1 ; +STLR W2,[X3] | B.EQ over ; + | MOV W2,#2 ; + | MOV W4,#1 ; + | STR W4,[X3] ; + | over: ; + | MOV W8,#7 ; + | STR W8,[X3] ; +exists (0:X0=7 /\ 1:X0=1) diff --git a/catalogue/dependencies/tests/down-one-leg/H14V.litmus b/catalogue/dependencies/tests/down-one-leg/H14V.litmus new file mode 100644 index 000000000..3dbee4042 --- /dev/null +++ b/catalogue/dependencies/tests/down-one-leg/H14V.litmus @@ -0,0 +1,17 @@ +AArch64 H14V +{ +0:X1=x; 0:X3=y; +1:X1=y; 1:X3=x; +} +P0 | P1 ; +LDR W0,[X1] | LDR W0,[X1] ; + | CMP W0,#0 ; +MOV W2,#1 | MOV W2,#1 ; +STLR W2,[X3] | B.NE over ; + | MOV W2,#2 ; + | MOV W4,#1 ; + | STR W4,[X3] ; + | over: ; + | MOV W8,#7 ; + | STR W8,[X3] ; +exists (0:X0=7 /\ 1:X0=1) diff --git a/catalogue/dependencies/tests/down-one-leg/H15V.litmus b/catalogue/dependencies/tests/down-one-leg/H15V.litmus new file mode 100644 index 000000000..957c2f762 --- /dev/null +++ b/catalogue/dependencies/tests/down-one-leg/H15V.litmus @@ -0,0 +1,17 @@ +AArch64 H15V +{ +0:X1=x; 0:X3=y; +1:X1=y; 1:X3=x; 1:X5=z; +} +P0 | P1 ; +LDR W0,[X1] | LDR W0,[X1] ; + | CMP W0,#0 ; +MOV W2,#1 | MOV W2,#1 ; +STLR W2,[X3] | B.EQ over ; + | MOV W2,#2 ; + | EOR W9,W0,W0 ; + | LDR W4,[X5,W9,SXTW] ; + | over: ; + | MOV W8,#7 ; + | STR W8,[X3] ; +exists (0:X0=7 /\ 1:X0=1) diff --git a/catalogue/dependencies/tests/down-one-leg/H16X.litmus b/catalogue/dependencies/tests/down-one-leg/H16X.litmus new file mode 100644 index 000000000..4f1929e90 --- /dev/null +++ b/catalogue/dependencies/tests/down-one-leg/H16X.litmus @@ -0,0 +1,17 @@ +AArch64 H16X +{ +0:X1=x; 0:X3=y; +1:X1=y; 1:X3=x; 1:X5=z; +} +P0 | P1 ; +LDR W0,[X1] | LDR W0,[X1] ; + | CMP W0,#0 ; +MOV W2,#1 | MOV W2,#1 ; +STLR W2,[X3] | B.NE over ; + | MOV W2,#2 ; + | EOR W9,W0,W0 ; + | LDR W4,[X5,W9,SXTW] ; + | over: ; + | MOV W8,#7 ; + | STR W8,[X3] ; +exists (0:X0=7 /\ 1:X0=1) diff --git a/catalogue/dependencies/tests/down-one-leg/H1CX.litmus b/catalogue/dependencies/tests/down-one-leg/H1CX.litmus new file mode 100644 index 000000000..977fa2f78 --- /dev/null +++ b/catalogue/dependencies/tests/down-one-leg/H1CX.litmus @@ -0,0 +1,14 @@ +AArch64 H1CX +{ +0:X1=x; 0:X3=y; +1:X1=y; 1:X3=x; +} +P0 | P1 ; +LDR W0,[X1] | LDR W0,[X1] ; + | CMP W0,#0 ; + | MOV W5,#1 ; + | MOV W6,#2 ; +MOV W2,#1 | CSEL W2,W5,W6,EQ ; +STLR W2,[X3] | MOV W8,#7 ; + | STR W8,[X3] ; +exists (0:X0=7 /\ 1:X0=1) diff --git a/catalogue/dependencies/tests/down-one-leg/H1X.litmus b/catalogue/dependencies/tests/down-one-leg/H1X.litmus new file mode 100644 index 000000000..66e1fbe47 --- /dev/null +++ b/catalogue/dependencies/tests/down-one-leg/H1X.litmus @@ -0,0 +1,15 @@ +AArch64 H1X +{ +0:X1=x; 0:X3=y; +1:X1=y; 1:X3=x; +} +P0 | P1 ; +LDR W0,[X1] | LDR W0,[X1] ; + | CMP W0,#0 ; +MOV W2,#1 | MOV W2,#1 ; +STLR W2,[X3] | B.EQ over ; + | MOV W2,#2 ; + | over: ; + | MOV W8,#7 ; + | STR W8,[X3] ; +exists (0:X0=7 /\ 1:X0=1) diff --git a/catalogue/dependencies/tests/down-one-leg/H2CV.litmus b/catalogue/dependencies/tests/down-one-leg/H2CV.litmus new file mode 100644 index 000000000..fc1f8489c --- /dev/null +++ b/catalogue/dependencies/tests/down-one-leg/H2CV.litmus @@ -0,0 +1,15 @@ +AArch64 H2CV +{ +0:X1=x; 0:X3=y; +1:X1=y; 1:X3=x; +} +P0 | P1 ; +LDR W0,[X1] | LDR W0,[X1] ; +MOV W2,#1 | CMP W0,#0 ; +STLR W2,[X3] | MOV W5,#1 ; + | MOV W6,#2 ; + | CSEL W2,W5,W6,EQ ; + | ISB ; + | MOV W8,#7 ; + | STR W8,[X3] ; +exists (0:X0=7 /\ 1:X0=1) diff --git a/catalogue/dependencies/tests/down-one-leg/H2V.litmus b/catalogue/dependencies/tests/down-one-leg/H2V.litmus new file mode 100644 index 000000000..36912701b --- /dev/null +++ b/catalogue/dependencies/tests/down-one-leg/H2V.litmus @@ -0,0 +1,16 @@ +AArch64 H2V +{ +0:X1=x; 0:X3=y; +1:X1=y; 1:X3=x; +} +P0 | P1 ; +LDR W0,[X1] | LDR W0,[X1] ; + | CMP W0,#0 ; +MOV W2,#1 | MOV W2,#1 ; +STLR W2,[X3] | B.EQ over ; + | MOV W2,#2 ; + | over: ; + | ISB ; + | MOV W8,#7 ; + | STR W8,[X3] ; +exists (0:X0=7 /\ 1:X0=1) diff --git a/catalogue/dependencies/tests/down-one-leg/H3CV.litmus b/catalogue/dependencies/tests/down-one-leg/H3CV.litmus new file mode 100644 index 000000000..b02bcfa72 --- /dev/null +++ b/catalogue/dependencies/tests/down-one-leg/H3CV.litmus @@ -0,0 +1,16 @@ +AArch64 H3CV +{ +0:X1=x; 0:X3=y; +1:X1=y; 1:X3=x; 1:X10=z; +} +P0 | P1 ; +LDR W0,[X1] | LDR W0,[X1] ; + | CMP W0,#0 ; +MOV W2,#1 | MOV W5,#1 ; +STLR W2,[X3] | MOV W6,#2 ; + | CSEL W2,W5,W6,EQ ; + | EOR W9,W0,W0 ; + | LDR W4,[X10,W9,SXTW] ; + | MOV W8,#7 ; + | STR W8,[X3] ; +exists (0:X0=7 /\ 1:X0=1) diff --git a/catalogue/dependencies/tests/down-one-leg/H3V.litmus b/catalogue/dependencies/tests/down-one-leg/H3V.litmus new file mode 100644 index 000000000..5b8f9d958 --- /dev/null +++ b/catalogue/dependencies/tests/down-one-leg/H3V.litmus @@ -0,0 +1,17 @@ +AArch64 H3V +{ +0:X1=x; 0:X3=y; +1:X1=y; 1:X3=x; 1:X5=z; +} +P0 | P1 ; +LDR W0,[X1] | LDR W0,[X1] ; + | CMP W0,#0 ; +MOV W2,#1 | MOV W2,#1 ; +STLR W2,[X3] | B.EQ over ; + | MOV W2,#2 ; + | over: ; + | EOR W9,W0,W0 ; + | LDR W4,[X5,W9,SXTW] ; + | MOV W8,#7 ; + | STR W8,[X3] ; +exists (0:X0=7 /\ 1:X0=1) diff --git a/catalogue/dependencies/tests/down-one-leg/H3bCQ.litmus b/catalogue/dependencies/tests/down-one-leg/H3bCQ.litmus new file mode 100644 index 000000000..2e7c09372 --- /dev/null +++ b/catalogue/dependencies/tests/down-one-leg/H3bCQ.litmus @@ -0,0 +1,15 @@ +AArch64 H3bCQ +{ +0:X1=x; 0:X3=y; +1:X1=y; 1:X3=x; 1:X5=z; +} +P0 | P1 ; +LDR W0,[X1] | LDR W0,[X1] ; +MOV W2,#1 | CMP W0,#0 ; +STLR W2,[X3] | MOV W5,#1 ; + | MOV W6,#2 ; + | CSEL W2,W5,W6,EQ ; + | LDR W4,[X1] ; + | MOV W8,#7 ; + | STR W8,[X3] ; +exists (0:X0=7 /\ 1:X0=1) diff --git a/catalogue/dependencies/tests/down-one-leg/H3bQ.litmus b/catalogue/dependencies/tests/down-one-leg/H3bQ.litmus new file mode 100644 index 000000000..de55ef567 --- /dev/null +++ b/catalogue/dependencies/tests/down-one-leg/H3bQ.litmus @@ -0,0 +1,16 @@ +AArch64 H3bQ +{ +0:X1=x; 0:X3=y; +1:X1=y; 1:X3=x; 1:X5=z; +} +P0 | P1 ; +LDR W0,[X1] | LDR W0,[X1] ; + | CMP W0,#0 ; +MOV W2,#1 | MOV W2,#1 ; +STLR W2,[X3] | B.EQ over ; + | MOV W2,#2 ; + | over: ; + | LDR W4,[X1] ; + | MOV W8,#7 ; + | STR W8,[X3] ; +exists (0:X0=7 /\ 1:X0=1) diff --git a/catalogue/dependencies/tests/down-one-leg/H4CX.litmus b/catalogue/dependencies/tests/down-one-leg/H4CX.litmus new file mode 100644 index 000000000..be2867fbe --- /dev/null +++ b/catalogue/dependencies/tests/down-one-leg/H4CX.litmus @@ -0,0 +1,17 @@ +AArch64 H4CX +{ +0:X1=x; 0:X3=y; +1:X1=y; 1:X3=x; 1:X10=z; 1:X7=a; +} +P0 | P1 ; +LDR W0,[X1] | LDR W0,[X1] ; + | CMP W0,#0 ; +MOV W2,#1 | MOV W5,#1 ; +STLR W2,[X3] | MOV W6,#2 ; + | CSEL W2,W5,W6,EQ ; + | LDR W4,[X10] ; + | EOR W9,W4,W4 ; + | LDR W6,[X7,W9,SXTW] ; + | MOV W8,#7 ; + | STR W8,[X3] ; +exists (0:X0=7 /\ 1:X0=1) diff --git a/catalogue/dependencies/tests/down-one-leg/H4X.litmus b/catalogue/dependencies/tests/down-one-leg/H4X.litmus new file mode 100644 index 000000000..438413a17 --- /dev/null +++ b/catalogue/dependencies/tests/down-one-leg/H4X.litmus @@ -0,0 +1,18 @@ +AArch64 H4X +{ +0:X1=x; 0:X3=y; +1:X1=y; 1:X3=x; 1:X10=z; 1:X7=a; +} +P0 | P1 ; +LDR W0,[X1] | LDR W0,[X1] ; + | CMP W0,#0 ; +MOV W2,#1 | MOV W2,#1 ; +STLR W2,[X3] | B.EQ over ; + | MOV W2,#2 ; + | over: ; + | LDR W4,[X10] ; + | EOR W9,W4,W4 ; + | LDR W6,[X7,W9,SXTW] ; + | MOV W8,#7 ; + | STR W8,[X3] ; +exists (0:X0=7 /\ 1:X0=1) diff --git a/catalogue/dependencies/tests/down-one-leg/H5CV.litmus b/catalogue/dependencies/tests/down-one-leg/H5CV.litmus new file mode 100644 index 000000000..6695041a2 --- /dev/null +++ b/catalogue/dependencies/tests/down-one-leg/H5CV.litmus @@ -0,0 +1,16 @@ +AArch64 H5CV +{ +0:X1=x; 0:X3=y; +1:X1=y; 1:X3=x; 1:X10=z; +} +P0 | P1 ; +LDR W0,[X1] | LDR W0,[X1] ; + | CMP W0,#0 ; +MOV W2,#1 | MOV W5,#1 ; +STLR W2,[X3] | MOV W6,#2 ; + | CSEL W2,W5,W6,EQ ; + | LDR W4,[X10] ; + | DMB LD ; + | MOV W8,#7 ; + | STR W8,[X3] ; +exists (0:X0=7 /\ 1:X0=1) diff --git a/catalogue/dependencies/tests/down-one-leg/H5V.litmus b/catalogue/dependencies/tests/down-one-leg/H5V.litmus new file mode 100644 index 000000000..e02116d03 --- /dev/null +++ b/catalogue/dependencies/tests/down-one-leg/H5V.litmus @@ -0,0 +1,17 @@ +AArch64 H5V +{ +0:X1=x; 0:X3=y; +1:X1=y; 1:X3=x; 1:X5=z; +} +P0 | P1 ; +LDR W0,[X1] | LDR W0,[X1] ; + | CMP W0,#0 ; +MOV W2,#1 | MOV W2,#1 ; +STLR W2,[X3] | B.EQ over ; + | MOV W2,#2 ; + | over: ; + | LDR W4,[X5] ; + | DMB LD ; + | MOV W8,#7 ; + | STR W8,[X3] ; +exists (0:X0=7 /\ 1:X0=1) diff --git a/catalogue/dependencies/tests/down-one-leg/H6CX.litmus b/catalogue/dependencies/tests/down-one-leg/H6CX.litmus new file mode 100644 index 000000000..87e4688ef --- /dev/null +++ b/catalogue/dependencies/tests/down-one-leg/H6CX.litmus @@ -0,0 +1,15 @@ +AArch64 H6CX +{ +0:X1=x; 0:X3=y; +1:X1=y; 1:X3=x; +} +P0 | P1 ; +LDR W0,[X1] | LDR W0,[X1] ; + | CMP W0,#0 ; +MOV W2,#1 | MOV W5,#1 ; +STLR W2,[X3] | MOV W6,#2 ; + | CSEL W2,W5,W6,EQ ; + | LDR W4,[X1] ; + | MOV W8,#7 ; + | STR W8,[X3] ; +exists (0:X0=7 /\ 1:X0=1) diff --git a/catalogue/dependencies/tests/down-one-leg/H6X.litmus b/catalogue/dependencies/tests/down-one-leg/H6X.litmus new file mode 100644 index 000000000..925e4b941 --- /dev/null +++ b/catalogue/dependencies/tests/down-one-leg/H6X.litmus @@ -0,0 +1,16 @@ +AArch64 H6X +{ +0:X1=x; 0:X3=y; +1:X1=y; 1:X3=x; +} +P0 | P1 ; +LDR W0,[X1] | LDR W0,[X1] ; + | CMP W0,#0 ; +MOV W2,#1 | MOV W2,#1 ; +STLR W2,[X3] | B.EQ over ; + | MOV W2,#2 ; + | over: ; + | LDR W4,[X1] ; + | MOV W8,#7 ; + | STR W8,[X3] ; +exists (0:X0=7 /\ 1:X0=1) diff --git a/catalogue/dependencies/tests/down-one-leg/H7CX.litmus b/catalogue/dependencies/tests/down-one-leg/H7CX.litmus new file mode 100644 index 000000000..c3b138aa3 --- /dev/null +++ b/catalogue/dependencies/tests/down-one-leg/H7CX.litmus @@ -0,0 +1,16 @@ +AArch64 H7CX +{ +0:X1=x; 0:X3=y; +1:X1=y; 1:X3=x; +} +P0 | P1 ; +LDR W0,[X1] | LDR W0,[X1] ; + | CMP W0,#0 ; +MOV W2,#1 | MOV W5,#1 ; +STLR W2,[X3] | MOV W6,#2 ; + | CSEL W2,W5,W6,EQ ; + | MOV W4,#1 ; + | STR W4,[X3] ; + | MOV W8,#7 ; + | STR W8,[X3] ; +exists (0:X0=7 /\ 1:X0=1) diff --git a/catalogue/dependencies/tests/down-one-leg/H7X.litmus b/catalogue/dependencies/tests/down-one-leg/H7X.litmus new file mode 100644 index 000000000..d4d53257a --- /dev/null +++ b/catalogue/dependencies/tests/down-one-leg/H7X.litmus @@ -0,0 +1,17 @@ +AArch64 H7X +{ +0:X1=x; 0:X3=y; +1:X1=y; 1:X3=x; +} +P0 | P1 ; +LDR W0,[X1] | LDR W0,[X1] ; + | CMP W0,#0 ; +MOV W2,#1 | MOV W2,#1 ; +STLR W2,[X3] | B.EQ over ; + | MOV W2,#2 ; + | over: ; + | MOV W4,#1 ; + | STR W4,[X3] ; + | MOV W8,#7 ; + | STR W8,[X3] ; +exists (0:X0=7 /\ 1:X0=1) diff --git a/catalogue/dependencies/tests/down-one-leg/H8CX.litmus b/catalogue/dependencies/tests/down-one-leg/H8CX.litmus new file mode 100644 index 000000000..945967fc2 --- /dev/null +++ b/catalogue/dependencies/tests/down-one-leg/H8CX.litmus @@ -0,0 +1,16 @@ +AArch64 H8CX +{ +0:X1=x; 0:X3=y; +1:X1=y; 1:X3=x; 1:X10=z; +} +P0 | P1 ; +LDR W0,[X1] | LDR W0,[X1] ; + | CMP W0,#0 ; +MOV W2,#1 | MOV W5,#1 ; +STLR W2,[X3] | MOV W6,#2 ; + | CSEL W2,W5,W6,EQ ; + | LDR W4,[X10] ; + | EOR W9,W4,W4 ; + | MOV W8,#7 ; + | STR W8,[X3,W9,SXTW] ; +exists (0:X0=7 /\ 1:X0=1) diff --git a/catalogue/dependencies/tests/down-one-leg/H8X.litmus b/catalogue/dependencies/tests/down-one-leg/H8X.litmus new file mode 100644 index 000000000..59904f9d9 --- /dev/null +++ b/catalogue/dependencies/tests/down-one-leg/H8X.litmus @@ -0,0 +1,17 @@ +AArch64 H8X +{ +0:X1=x; 0:X3=y; +1:X1=y; 1:X3=x; 1:X10=z; +} +P0 | P1 ; +LDR W0,[X1] | LDR W0,[X1] ; + | CMP W0,#0 ; +MOV W2,#1 | MOV W2,#1 ; +STLR W2,[X3] | B.EQ over ; + | MOV W2,#2 ; + | over: ; + | LDR W4,[X10] ; + | EOR W9,W4,W4 ; + | MOV W8,#7 ; + | STR W8,[X3,W9,SXTW] ; +exists (0:X0=7 /\ 1:X0=1) diff --git a/catalogue/dependencies/tests/down-one-leg/H8bCQ.litmus b/catalogue/dependencies/tests/down-one-leg/H8bCQ.litmus new file mode 100644 index 000000000..4a53cdb14 --- /dev/null +++ b/catalogue/dependencies/tests/down-one-leg/H8bCQ.litmus @@ -0,0 +1,16 @@ +AArch64 H8bCQ +{ +0:X1=x; 0:X3=y; +1:X1=y; 1:X3=x; 1:X10=z; +} +P0 | P1 ; +LDR W0,[X1] | LDR W0,[X1] ; + | CMP W0,#0 ; +MOV W2,#1 | MOV W5,#1 ; +STLR W2,[X3] | MOV W6,#2 ; + | CSEL W2,W5,W6,EQ ; + | LDR W4,[X10] ; + | EOR W9,W4,W4 ; + | MOV W8,#7 ; + | STR W8,[X3,W9,SXTW] ; +exists (0:X0=7 /\ 1:X0=1) diff --git a/catalogue/dependencies/tests/down-one-leg/H8bQ.litmus b/catalogue/dependencies/tests/down-one-leg/H8bQ.litmus new file mode 100644 index 000000000..3079dbaad --- /dev/null +++ b/catalogue/dependencies/tests/down-one-leg/H8bQ.litmus @@ -0,0 +1,17 @@ +AArch64 H8bQ +{ +0:X1=x; 0:X3=y; +1:X1=y; 1:X3=x; 1:X10=z; +} +P0 | P1 ; +LDR W0,[X1] | LDR W0,[X1] ; + | CMP W0,#0 ; +MOV W2,#1 | MOV W2,#1 ; +STLR W2,[X3] | B.EQ over ; + | MOV W2,#2 ; + | LDR W4,[X10] ; + | EOR W9,W4,W4 ; + | over: ; + | MOV W8,#7 ; + | STR W8,[X3,W9,SXTW] ; +exists (0:X0=7 /\ 1:X0=1) diff --git a/catalogue/dependencies/tests/down-one-leg/H8cQ.litmus b/catalogue/dependencies/tests/down-one-leg/H8cQ.litmus new file mode 100644 index 000000000..be526ee74 --- /dev/null +++ b/catalogue/dependencies/tests/down-one-leg/H8cQ.litmus @@ -0,0 +1,17 @@ +AArch64 H8cQ +{ +0:X1=x; 0:X3=y; +1:X1=y; 1:X3=x; 1:X10=z; +} +P0 | P1 ; +LDR W0,[X1] | LDR W0,[X1] ; + | CMP W0,#0 ; +MOV W2,#1 | MOV W2,#1 ; +STLR W2,[X3] | B.EQ over ; + | MOV W2,#2 ; + | over: ; + | LDR W4,[X10] ; + | EOR W9,W4,W4 ; + | MOV W8,#7 ; + | STR W8,[X3,W9,SXTW] ; +exists (0:X0=7 /\ 1:X0=1) diff --git a/catalogue/dependencies/tests/down-one-leg/H9CV.litmus b/catalogue/dependencies/tests/down-one-leg/H9CV.litmus new file mode 100644 index 000000000..dad7c7ed8 --- /dev/null +++ b/catalogue/dependencies/tests/down-one-leg/H9CV.litmus @@ -0,0 +1,14 @@ +AArch64 H9CV +{ +0:X1=x; 0:X3=y; +1:X1=y; 1:X3=x; +} +P0 | P1 ; +LDR W0,[X1] | LDR W0,[X1] ; + | CMP W0,#0 ; +MOV W2,#1 | MOV W5,#1 ; +STLR W2,[X3] | MOV W6,#2 ; + | CSEL W2,W5,W6,EQ ; + | MOV W8,#7 ; + | STLR W8,[X3] ; +exists (0:X0=7 /\ 1:X0=1) diff --git a/catalogue/dependencies/tests/down-one-leg/H9V.litmus b/catalogue/dependencies/tests/down-one-leg/H9V.litmus new file mode 100644 index 000000000..649228d4d --- /dev/null +++ b/catalogue/dependencies/tests/down-one-leg/H9V.litmus @@ -0,0 +1,15 @@ +AArch64 H9V +{ +0:X1=x; 0:X3=y; +1:X1=y; 1:X3=x; +} +P0 | P1 ; +LDR W0,[X1] | LDR W0,[X1] ; + | CMP W0,#0 ; +MOV W2,#1 | MOV W2,#1 ; +STLR W2,[X3] | B.EQ over ; + | MOV W2,#2 ; + | over: ; + | MOV W8,#7 ; + | STLR W8,[X3] ; +exists (0:X0=7 /\ 1:X0=1) diff --git a/catalogue/dependencies/tests/down-one-leg/LB6b.litmus b/catalogue/dependencies/tests/down-one-leg/LB6b.litmus new file mode 100644 index 000000000..78660bbc8 --- /dev/null +++ b/catalogue/dependencies/tests/down-one-leg/LB6b.litmus @@ -0,0 +1,15 @@ +AArch64 LB6b +{ +0:X1=x; 0:X3=y; +1:X1=y; 1:X3=x; +} +P0 | P1 ; +LDR W0,[X1] | LDR W0,[X1] ; + | CMP W0,#0 ; +MOV W2,#1 | MOV W2,#1 ; +STLR W2,[X3] | B.EQ over ; + | MOV W2,#2 ; + | over: ; + | MOV W8,#7 ; + | STR W8,[X3] ; +exists (0:X0=7 /\ 1:X0=1) diff --git a/catalogue/dependencies/tests/down-one-leg/LB6b2.litmus b/catalogue/dependencies/tests/down-one-leg/LB6b2.litmus new file mode 100644 index 000000000..4b29e6c6f --- /dev/null +++ b/catalogue/dependencies/tests/down-one-leg/LB6b2.litmus @@ -0,0 +1,14 @@ +AArch64 LB6b2 +{ +0:X1=x; 0:X3=y; +1:X1=y; 1:X3=x; +} +P0 | P1 ; +LDR W0,[X1] | LDR W0,[X1] ; + | CMP W0,#0 ; +MOV W2,#1 | MOV W2,#1 ; +STLR W2,[X3] | B.EQ over ; + | MOV W2,#2 ; + | over: ; + | STR W2,[X3] ; +exists (0:X0=2 /\ 1:X0=1) diff --git a/catalogue/dependencies/tests/down-one-leg/LB6b3.litmus b/catalogue/dependencies/tests/down-one-leg/LB6b3.litmus new file mode 100644 index 000000000..99ac68ad7 --- /dev/null +++ b/catalogue/dependencies/tests/down-one-leg/LB6b3.litmus @@ -0,0 +1,14 @@ +AArch64 LB6b3 +{ +0:X1=x; 0:X3=y; +1:X1=y; 1:X3=x; +} +P0 | P1 ; +LDR W0,[X1] | LDR W0,[X1] ; + | CMP W0,#0 ; +MOV W2,#1 | MOV W2,#1 ; +STLR W2,[X3] | B.NE over ; + | MOV W2,#2 ; + | over: ; + | STR W2,[X3] ; +exists (0:X0=1 /\ 1:X0=1) diff --git a/catalogue/dependencies/tests/down-one-leg/MP+DMB.ST+B-EOR.litmus b/catalogue/dependencies/tests/down-one-leg/MP+DMB.ST+B-EOR.litmus new file mode 100644 index 000000000..6170a3db9 --- /dev/null +++ b/catalogue/dependencies/tests/down-one-leg/MP+DMB.ST+B-EOR.litmus @@ -0,0 +1,16 @@ +AArch64 MP+DMB.ST+B-EOR +{ +0:X1=x; 0:X3=y; +1:X1=x; 1:X3=y; +} + P0 | P1 ; + MOV W0,#1 | LDR W0,[X3] ; + STR W0,[X1] | MOV W4,#4 ; + | CMP W0,W4 ; + | B.EQ LC00 ; + | EOR X2,X0,X0 ; + DMB ST | LDR W2,[X2,X1] ; + MOV W2,#1 | LC00: ; + STR W2,[X3] | ; +exists +(1:X0=1 /\ 1:X2=0) diff --git a/catalogue/dependencies/tests/down-one-leg/MP+DMB.ST+B.litmus b/catalogue/dependencies/tests/down-one-leg/MP+DMB.ST+B.litmus new file mode 100644 index 000000000..159171d9a --- /dev/null +++ b/catalogue/dependencies/tests/down-one-leg/MP+DMB.ST+B.litmus @@ -0,0 +1,15 @@ +AArch64 MP+DMB.ST+B +{ +0:X1=x; 0:X3=y; +1:X1=x; 1:X3=y; +} + P0 | P1 ; + MOV W0,#1 | LDR W0,[X3] ; + STR W0,[X1] | MOV W4,#4 ; + | CMP W0,W4 ; + | B.EQ LC00 ; + DMB ST | LDR W2,[X2,X1] ; + MOV W2,#1 | LC00: ; + STR W2,[X3] | ; +exists +(1:X0=1 /\ 1:X2=0) diff --git a/catalogue/dependencies/tests/down-one-leg/MP+DMB.ST+CSEL.litmus b/catalogue/dependencies/tests/down-one-leg/MP+DMB.ST+CSEL.litmus new file mode 100644 index 000000000..a8ee56db3 --- /dev/null +++ b/catalogue/dependencies/tests/down-one-leg/MP+DMB.ST+CSEL.litmus @@ -0,0 +1,15 @@ +AArch64 MP+DMB.ST+CSEL +{ +0:X1=x; 0:X3=y; +1:X1=x; 1:X3=y; +} +P0 | P1 ; +MOV W0,#1 | LDR W0,[X3] ; +STR W0,[X1] | MOV W4,#4 ; +DMB ST | CMP W4,W0 ; +MOV W2,#1 | MOV X5,#0 ; +STR W2,[X3] | CSEL X2, XZR, X5, NE ; + | LDR W2,[X2,X1] ; + | LC00: ; +exists +(1:X0=1 /\ 1:X2=0) diff --git a/catalogue/dependencies/tests/down-one-leg/PPOCA.litmus b/catalogue/dependencies/tests/down-one-leg/PPOCA.litmus new file mode 100644 index 000000000..d0db2b356 --- /dev/null +++ b/catalogue/dependencies/tests/down-one-leg/PPOCA.litmus @@ -0,0 +1,15 @@ +AArch64 PPOCA +{ +0:X1=x; 0:X3=y; +1:X1=y; 1:X3=z; 1:X7=x; +} +P0 | P1 ; +MOV W0,#1 | LDR W0,[X1] ; +STR W0,[X1] | CBZ W0,over ; +MOV W2,#1 | MOV W2,#1 ; +STLR W2,[X3] | STR W2,[X3] ; + | LDR W4,[X3] ; + | EOR W5,W4,W4 ; + | LDR W6,[X7,W5,SXTW] ; + | over: ; +exists (1:X0=1 /\ 1:X4=1 /\ 1:X6=0) diff --git a/catalogue/dependencies/tests/down-one-leg/PPOCA4b.litmus b/catalogue/dependencies/tests/down-one-leg/PPOCA4b.litmus new file mode 100644 index 000000000..20ad12ffc --- /dev/null +++ b/catalogue/dependencies/tests/down-one-leg/PPOCA4b.litmus @@ -0,0 +1,16 @@ +AArch64 PPCOA4b +{ +0:X1=x; 0:X3=y; +1:X1=y; 1:X3=z; 1:X7=x; +} +P0 | P1 ; +MOV W0,#1 | LDR W0,[X1] ; +STR W0,[X1] | MOV W2,#1 ; +MOV W2,#1 | CBZ W0,over ; +STLR W2,[X3] | MOV W2,#2 ; + | over: ; + | STR W2,[X3] ; + | LDR W4,[X3] ; + | EOR W5,W4,W4 ; + | LDR W6,[X7,W5,SXTW] ; +exists (1:X0=1 /\ 1:X4=2 /\ 1:X6=0) diff --git a/catalogue/dependencies/tests/down-one-leg/PPOCA5b.litmus b/catalogue/dependencies/tests/down-one-leg/PPOCA5b.litmus new file mode 100644 index 000000000..9bf19a722 --- /dev/null +++ b/catalogue/dependencies/tests/down-one-leg/PPOCA5b.litmus @@ -0,0 +1,14 @@ +AArch64 PPOCA5b +{ +0:X1=x; 0:X3=y; +1:X1=y; 1:X3=z; 1:X7=x; +} +P0 | P1 ; +MOV W0,#1 | LDR W0,[X1] ; +STR W0,[X1] | EOR W2,W0,W0 ; +MOV W2,#1 | ADD W2,W2,#1 ; +STLR W2,[X3] | STR W2,[X3] ; + | LDR W4,[X3] ; + | EOR W5,W4,W4 ; + | LDR W6,[X7,W5,SXTW] ; +exists (1:X0=1 /\ 1:X4=1 /\ 1:X6=0) diff --git a/catalogue/dependencies/tests/down-one-leg/PPOCA6b.litmus b/catalogue/dependencies/tests/down-one-leg/PPOCA6b.litmus new file mode 100644 index 000000000..922179290 --- /dev/null +++ b/catalogue/dependencies/tests/down-one-leg/PPOCA6b.litmus @@ -0,0 +1,17 @@ +AArch64 PPOCA6b +{ +0:X1=x; 0:X3=y; +1:X1=y; 1:X3=z; 1:X7=x; +} +P0 | P1 ; +MOV W0,#1 | LDR W0,[X1] ; +STR W0,[X1] | MOV W2,#1 ; +MOV W2,#1 | CBZ W0,over ; +STLR W2,[X3] | MOV W2,#2 ; + | over: ; + | MOV W8,#7 ; + | STR W8,[X3] ; + | LDR W4,[X3] ; + | EOR W5,W4,W4 ; + | LDR W6,[X7,W5,SXTW] ; +exists (1:X0=1 /\ 1:X4=7 /\ 1:X6=0) diff --git a/catalogue/dependencies/tests/down-one-leg/PPOCA6c.litmus b/catalogue/dependencies/tests/down-one-leg/PPOCA6c.litmus new file mode 100644 index 000000000..922179290 --- /dev/null +++ b/catalogue/dependencies/tests/down-one-leg/PPOCA6c.litmus @@ -0,0 +1,17 @@ +AArch64 PPOCA6b +{ +0:X1=x; 0:X3=y; +1:X1=y; 1:X3=z; 1:X7=x; +} +P0 | P1 ; +MOV W0,#1 | LDR W0,[X1] ; +STR W0,[X1] | MOV W2,#1 ; +MOV W2,#1 | CBZ W0,over ; +STLR W2,[X3] | MOV W2,#2 ; + | over: ; + | MOV W8,#7 ; + | STR W8,[X3] ; + | LDR W4,[X3] ; + | EOR W5,W4,W4 ; + | LDR W6,[X7,W5,SXTW] ; +exists (1:X0=1 /\ 1:X4=7 /\ 1:X6=0) diff --git a/catalogue/dependencies/tests/down-one-leg/S-stxr-success.litmus b/catalogue/dependencies/tests/down-one-leg/S-stxr-success.litmus new file mode 100644 index 000000000..a71b291cc --- /dev/null +++ b/catalogue/dependencies/tests/down-one-leg/S-stxr-success.litmus @@ -0,0 +1,18 @@ +AArch64 S-STXR-success +{ +0:X1=x0; 0:X4=x1; 0:X5=x2; +1:X2=x1; 1:X4=x0; +} + P0 | P1 ; + LDR W0,[X1] | MOV W0,#1 ; + EOR W2,W0,W0 | MOV W1,#2 ; + ADD X5,X2,X5 | MOV W3,#3 ; + STR WZR,[X5] | STR W0,[X2] ; + LDXR W9,[X5] | STR W1,[X2] ; + STXR W2,W9,[X5] | DMB SY ; + EOR W6,W2,W2 | STR W3,[X4] ; + ADD X4,X6,X4 | ; + MOV W3,#4 | ; + STR W3,[X4] | ; +exists +(0:X0=3 /\ x1=2 /\ 0:X2=0) diff --git a/catalogue/dependencies/tests/down-one-leg/STXR-ctrl.litmus b/catalogue/dependencies/tests/down-one-leg/STXR-ctrl.litmus new file mode 100644 index 000000000..15edaa324 --- /dev/null +++ b/catalogue/dependencies/tests/down-one-leg/STXR-ctrl.litmus @@ -0,0 +1,15 @@ +AArch64 STXR-ctrl +{ +0:X1=x; 0:X3=y; +1:X0=y; 1:X5=x; +} + P0 | P1 ; + MOV W0,#2 | MOV W2,#2 ; + STR W0,[X1] | ; + DMB ST | LDXR W1,[X0] ; + MOV W2,#1 | STXR W3,W2,[X0] ; + STR W2,[X3] | CBNZ W3,Fail ; + | MOV W4,#1 ; + | STR W4,[X5] ; + | Fail: ; +exists (x=2 /\ y=2 /\ 1:X1=1 /\ 1:X3=0) diff --git a/catalogue/dependencies/tests/down-one-leg/STXR-ctrl1.litmus b/catalogue/dependencies/tests/down-one-leg/STXR-ctrl1.litmus new file mode 100644 index 000000000..3c4da0dbc --- /dev/null +++ b/catalogue/dependencies/tests/down-one-leg/STXR-ctrl1.litmus @@ -0,0 +1,17 @@ +AArch64 STXR-ctrl1 +{ +0:X1=x; 0:X3=y; +1:X8=y; 1:X5=x; 1:X0=z; +} + P0 | P1 ; + MOV W0,#2 | MOV W2,#2 ; + STR W0,[X1] | LDR W7,[X8] ; + | EOR W6,W7,W7 ; + | ADD X0,X6,X0 ; + DMB ST | LDXR W1,[X0] ; + MOV W2,#1 | STXR W3,W2,[X0] ; + STR W2,[X3] | CBNZ W3,Fail ; + | MOV W4,#1 ; + | STR W4,[X5] ; + | Fail: ; +exists (x=2 /\ z=2 /\ 1:X7=1 /\ 1:X3=0) diff --git a/catalogue/dependencies/tests/down-one-leg/STXR-ctrl1a.litmus b/catalogue/dependencies/tests/down-one-leg/STXR-ctrl1a.litmus new file mode 100644 index 000000000..6d7a0b928 --- /dev/null +++ b/catalogue/dependencies/tests/down-one-leg/STXR-ctrl1a.litmus @@ -0,0 +1,18 @@ +AArch64 STXR-ctrl1a +{ +0:X1=x; 0:X3=y; +1:X8=y; 1:X5=x; 1:X0=z; +} + P0 | P1 ; + MOV W0,#2 | MOV W2,#2 ; + STR W0,[X1] | LDR W7,[X8] ; + | EOR W6,W7,W7 ; + | ADD X0,X6,X0 ; + DMB ST | LDXR W1,[X0] ; + MOV W2,#1 | ; + STR W2,[X3] | MOV W3,#1 ; + | CBNZ W3,Fail ; + | MOV W4,#1 ; + | STR W4,[X5] ; + | Fail: ; +exists (x=2 /\ z=2 /\ 1:X7=1) diff --git a/catalogue/dependencies/tests/down-one-leg/STXR-ctrl1b.litmus b/catalogue/dependencies/tests/down-one-leg/STXR-ctrl1b.litmus new file mode 100644 index 000000000..9953968e0 --- /dev/null +++ b/catalogue/dependencies/tests/down-one-leg/STXR-ctrl1b.litmus @@ -0,0 +1,18 @@ +AArch64 STXR-ctrl1b +{ +0:X1=x; 0:X3=y; +1:X8=y; 1:X5=x; 1:X0=z; +} + P0 | P1 ; + MOV W0,#2 | MOV W2,#2 ; + STR W0,[X1] | LDR W7,[X8] ; + | EOR W6,W7,W7 ; + | ADD X0,X6,X0 ; + DMB ST | LDXR W1,[X0] ; + MOV W2,#1 | STR W2,[X0] ; + | MOV W3,#0 ; + STR W2,[X3] | CBNZ W3,Fail ; + | MOV W4,#1 ; + | STR W4,[X5] ; + | Fail: ; +exists (x=2 /\ z=2 /\ 1:X7=1 /\ 1:X3=0) diff --git a/catalogue/dependencies/tests/down-one-leg/STXR-ctrl2.litmus b/catalogue/dependencies/tests/down-one-leg/STXR-ctrl2.litmus new file mode 100644 index 000000000..eea0d256c --- /dev/null +++ b/catalogue/dependencies/tests/down-one-leg/STXR-ctrl2.litmus @@ -0,0 +1,18 @@ +AArch64 STXR-ctrl2 +{ +0:X1=x; 0:X3=y; +1:X8=y; 1:X5=x; 1:X0=z; +} + P0 | P1 ; + MOV W0,#2 | MOV W2,#2 ; + STR W0,[X1] | LDR W7,[X8] ; + | EOR W6,W7,W7 ; + | ADD X0,X6,X0 ; + DMB ST | LDXR W1,[X0] ; + MOV W2,#1 | STXR W3,W2,[X0] ; + | MOV W9,W3 ; + STR W2,[X3] | CBNZ W9,Fail ; + | MOV W4,#1 ; + | STR W4,[X5] ; + | Fail: ; +exists (x=2 /\ z=2 /\ 1:X7=1 /\ 1:X3=0) diff --git a/catalogue/dependencies/tests/down-one-leg/STXR-ctrl3.litmus b/catalogue/dependencies/tests/down-one-leg/STXR-ctrl3.litmus new file mode 100644 index 000000000..3d1659ae6 --- /dev/null +++ b/catalogue/dependencies/tests/down-one-leg/STXR-ctrl3.litmus @@ -0,0 +1,19 @@ +AArch64 STXR-ctrl3 +{ +0:X1=x; 0:X3=y; +1:X8=y; 1:X5=x; 1:X0=z; 1:X9=t; +} + P0 | P1 ; + MOV W0,#2 | MOV W2,#2 ; + STR W0,[X1] | LDR W7,[X8] ; + | EOR W6,W7,W7 ; + | ADD X0,X6,X0 ; + DMB ST | LDXR W1,[X0] ; + MOV W2,#1 | STXR W3,W2,[X0] ; + | STR W3,[X9] ; + | LDR W10,[X9] ; + STR W2,[X3] | CBNZ W10,Fail ; + | MOV W4,#1 ; + | STR W4,[X5] ; + | Fail: ; +exists (x=2 /\ z=2 /\ 1:X7=1 /\ 1:X3=0) diff --git a/catalogue/dependencies/tests/down-one-leg/STXR-ctrla.litmus b/catalogue/dependencies/tests/down-one-leg/STXR-ctrla.litmus new file mode 100644 index 000000000..73b1ef881 --- /dev/null +++ b/catalogue/dependencies/tests/down-one-leg/STXR-ctrla.litmus @@ -0,0 +1,15 @@ +AArch64 STXR-ctrla +{ +0:X1=x; 0:X3=y; +1:X0=y; 1:X5=x; +} + P0 | P1 ; + MOV W0,#2 | MOV W2,#2 ; + STR W0,[X1] | ; + DMB ST | LDXR W1,[X0] ; + MOV W2,#1 | STXR W3,W2,[X0] ; + STR W2,[X3] | CBZ W3,Ok ; + | MOV W4,#1 ; + | STR W4,[X5] ; + | Ok: ; +exists (x=2 /\ y=2 /\ 1:X1=1 /\ 1:X3=0) diff --git a/catalogue/dependencies/tests/down-one-leg/SpecCE-01.litmus b/catalogue/dependencies/tests/down-one-leg/SpecCE-01.litmus new file mode 100644 index 000000000..c60233737 --- /dev/null +++ b/catalogue/dependencies/tests/down-one-leg/SpecCE-01.litmus @@ -0,0 +1,17 @@ +AArch64 SpecCE-01 +Prefetch=0:x=F,0:y=W,1:y=F,1:x=W +Com=Rf Rf + +(* This test is Forbid, as the two instances of the STR at the end of P0 + have different histories. Indeed the values stored are different *) +{ +0:X1=x; 0:X3=y; 0:X2=1; +1:X1=y; 1:X3=x; +} + P0 | P1 ; + LDR W0,[X1] | LDR W0,[X1] ; + CBNZ W0,LC00 | STR W0,[X3] ; + MOV W2,#2 | ; + LC00: | ; + STR W2,[X3] | ; +exists (0:X0=1 /\ 1:X0=1) diff --git a/catalogue/dependencies/tests/down-one-leg/SpecCE-02.litmus b/catalogue/dependencies/tests/down-one-leg/SpecCE-02.litmus new file mode 100644 index 000000000..ad1b5ae56 --- /dev/null +++ b/catalogue/dependencies/tests/down-one-leg/SpecCE-02.litmus @@ -0,0 +1,19 @@ +AArch64 SpecCE-02 +Com=Rf Rf +{ +1:X1=x; 1:X3=y; 0:X5=z; +0:X1=x; 0:X3=y; + +} + P0 | P1 ; + LDR W0,[X1] | LDR W0,[X3] ; + CBNZ W0,LC00 | STR W0,[X1] ; + MOV W2,#2 | ; + B LC01 | ; +LC00: | ; + MOV W2,#1 | ; +LC01: | ; + STR W2,[X5] | ; + LDR W4,[X5] | ; + STR W4,[X3] | ; +exists (0:X0=1 /\ 1:X0=1) diff --git a/catalogue/dependencies/tests/down-one-leg/SpecCE-03.litmus b/catalogue/dependencies/tests/down-one-leg/SpecCE-03.litmus new file mode 100644 index 000000000..ecbde67ef --- /dev/null +++ b/catalogue/dependencies/tests/down-one-leg/SpecCE-03.litmus @@ -0,0 +1,14 @@ +AArch64 SpecCE-03 +Com=Rf Rf +{ +1:X1=x; 1:X3=y; 0:X5=z; z=1; +0:X1=x; 0:X3=y; + +} + P0 | P1 ; + LDR W0,[X1] | LDR W0,[X3] ; + CBNZ W0,LC00 | STR W0,[X1] ; +LC00: | ; + LDR W2,[X5] | ; + STR W2,[X3] | ; +exists (0:X0=1 /\ 1:X0=1) diff --git a/catalogue/dependencies/tests/down-one-leg/SpecCE-04.litmus b/catalogue/dependencies/tests/down-one-leg/SpecCE-04.litmus new file mode 100644 index 000000000..20bfec369 --- /dev/null +++ b/catalogue/dependencies/tests/down-one-leg/SpecCE-04.litmus @@ -0,0 +1,14 @@ +AArch64 SpecCE-04 +Com=Rf Rf +{ +0:X1=x; 0:X3=y; 0:X5=z; z=0; +1:X1=x; 1:X3=y; +2:X5=z; 3:X5=z; +} + P0 | P1 | P2 | P3 ; + LDR W0,[X1] | LDR W0,[X3] | MOV W0,#1 | MOV W0,#2 ; + CBNZ W0,LC00 | STR W0,[X1] | STR W0,[X5] | STR W0,[X5] ; +LC00: | | | ; + LDR W2,[X5] | | | ; + STR W2,[X3] | | | ; +exists (0:X0=1 /\ 1:X0=1) diff --git a/catalogue/dependencies/tests/down-one-leg/SpecCE-05.litmus b/catalogue/dependencies/tests/down-one-leg/SpecCE-05.litmus new file mode 100644 index 000000000..758ea85d0 --- /dev/null +++ b/catalogue/dependencies/tests/down-one-leg/SpecCE-05.litmus @@ -0,0 +1,14 @@ +AArch64 SpecCE-05 +Com=Rf Rf +{ +0:X1=x; 0:X3=y; 0:X5=z; z=0; +1:X1=x; 1:X3=y; +2:X5=z; +} + P0 | P1 | P2 ; + LDR W0,[X1] | LDR W0,[X3] | MOV W0,#1 ; + CBNZ W0,LC00 | STR W0,[X1] | STR W0,[X5] ; +LC00: | | ; + LDR W2,[X5] | | ; + STR W2,[X3] | | ; +exists (0:X0=1 /\ 1:X0=1) diff --git a/catalogue/dependencies/tests/down-one-leg/SpecCoiV.litmus b/catalogue/dependencies/tests/down-one-leg/SpecCoiV.litmus new file mode 100644 index 000000000..08d41380f --- /dev/null +++ b/catalogue/dependencies/tests/down-one-leg/SpecCoiV.litmus @@ -0,0 +1,17 @@ +AArch64 SpecCoiV +Com=Rf Rf +{ +0:X1=x; 0:X3=y; +1:X1=y; 1:X3=x; +} + P0 | P1 ; + LDR W0,[X1] | LDR W0,[X1] ; + DMB SY | LDR W2,[X3] ; + MOV W2,#1 | STR W2,[X3] ; + | CBNZ W0,LC00 ; + | STR W2,[X3] ; + |LC00: ; + | MOV W4,#1 ; + STR W2,[X3] | STR W4,[X3] ; + +exists (0:X0=1 /\ 1:X0=1) diff --git a/catalogue/dependencies/tests/down-one-leg/SpecCoiX.litmus b/catalogue/dependencies/tests/down-one-leg/SpecCoiX.litmus new file mode 100644 index 000000000..2d4fd6ea5 --- /dev/null +++ b/catalogue/dependencies/tests/down-one-leg/SpecCoiX.litmus @@ -0,0 +1,17 @@ +AArch64 SpecCoiX +Com=Rf Rf +{ +0:X1=x; 0:X3=y; +1:X1=y; 1:X3=x; +} + P0 | P1 ; + LDR W0,[X1] | LDR W0,[X1] ; + DMB SY | MOV W2,#2 ; + MOV W2,#1 | STR W2,[X3] ; + | CBNZ W0,LC00 ; + | LDR W2,[X3] ; + |LC00: ; + | MOV W4,#1 ; + STR W2,[X3] | STR W4,[X3] ; + +exists (0:X0=1 /\ 1:X0=1) diff --git a/catalogue/dependencies/tests/down-one-leg/SpecRfeX.litmus b/catalogue/dependencies/tests/down-one-leg/SpecRfeX.litmus new file mode 100644 index 000000000..c138dbafd --- /dev/null +++ b/catalogue/dependencies/tests/down-one-leg/SpecRfeX.litmus @@ -0,0 +1,14 @@ +AArch64 SpecRfeX +Com=Rf Rf +{ +0:X1=x; 0:X3=y; 0:X5=z; z=0; +1:X1=x; 1:X3=y; +2:X5=z; 3:X5=z; +} + P0 | P1 | P2 | P3 ; + LDR W0,[X1] | LDR W0,[X3] | MOV W0,#1 | MOV W0,#2 ; + CBNZ W0,LC00 | STR W0,[X1] | STR W0,[X5] | STR W0,[X5] ; +LC00: | | | ; + LDR W2,[X5] | | | ; + STR W2,[X3] | | | ; +exists (0:X0=1 /\ 1:X0=1 /\ z=2) diff --git a/catalogue/dependencies/tests/down-one-leg/SpecRfiV.litmus b/catalogue/dependencies/tests/down-one-leg/SpecRfiV.litmus new file mode 100644 index 000000000..db7bdcfaa --- /dev/null +++ b/catalogue/dependencies/tests/down-one-leg/SpecRfiV.litmus @@ -0,0 +1,19 @@ +AArch64 SpecRfiV +Com=Rf Rf +{ +1:X1=x; 1:X3=y; 0:X5=z; +0:X1=x; 0:X3=y; + +} + P0 | P1 ; + LDR W0,[X1] | LDR W0,[X3] ; + CBNZ W0,LC00 | STR W0,[X1] ; + MOV W2,#2 | ; + B LC01 | ; +LC00: | ; + MOV W2,#1 | ; +LC01: | ; + STR W2,[X5] | ; + LDR W4,[X5] | ; + STR W4,[X3] | ; +exists (0:X0=1 /\ 1:X0=1) diff --git a/catalogue/dependencies/tests/down-one-leg/SpecRfiX.litmus b/catalogue/dependencies/tests/down-one-leg/SpecRfiX.litmus new file mode 100644 index 000000000..b15ee160f --- /dev/null +++ b/catalogue/dependencies/tests/down-one-leg/SpecRfiX.litmus @@ -0,0 +1,17 @@ +AArch64 SpecRfiX +Com=Rf Rf +{ +0:X1=x; 0:X3=y; +1:X1=y; 1:X3=x; 1:X9=z; +} + P0 | P1 ; + LDR W0,[X1] | LDR W0,[X1] ; + DMB SY | CBNZ W0,LC00 ; + | LDR W2,[X9] ; + MOV W2,#1 |LC00: ; + | MOV W2,#1 ; + | STR W2,[X9] ; + | LDR W4,[X9] ; + STR W2,[X3] | STR W4,[X3] ; + +exists (0:X0=1 /\ 1:X0=1) diff --git a/catalogue/dependencies/tests/down-one-leg/down-one-leg-kinds.txt b/catalogue/dependencies/tests/down-one-leg/down-one-leg-kinds.txt new file mode 100644 index 000000000..aedc516e7 --- /dev/null +++ b/catalogue/dependencies/tests/down-one-leg/down-one-leg-kinds.txt @@ -0,0 +1,67 @@ +2+2W+addr+dmb Allow +2+2W+xp+dmb Allow +H10X Allow +H10bX Allow +H11V Forbid +H11bQ Allow +H12CV Forbid +H12V Forbid +H13V Forbid +H14V Forbid +H15V Forbid +H16X Allow +H1CX Allow +H1X Allow +H2CV Forbid +H2V Forbid +H3CV Forbid +H3V Forbid +H3bCQ Allow +H3bQ Allow +H4CX Allow +H4X Allow +H5CV Forbid +H5V Forbid +H6CX Allow +H6X Allow +H7CX Allow +H7X Allow +H8CX Allow +H8X Allow +H8bCQ Allow +H8bQ Forbid +H8cQ Forbid +H9CV Forbid +H9V Forbid +LB6b Allow +LB6b2 Forbid +LB6b3 Forbid +MP-STXR Allow +MP-STXR-fail Allow +MP-STXR-success Allow +MP+DMB.ST+B Allow +MP+DMB.ST+B-EOR Forbid +MP+DMB.ST+CSEL Forbid +PPCOA4b Allow +PPOCA Allow +PPOCA5b Forbid +PPOCA6b Allow +S-STXR-success Forbid +STXR-ctrl Allow +STXR-ctrl1 Forbid +STXR-ctrl1a Forbid +STXR-ctrl1b Forbid +STXR-ctrl2 Forbid +STXR-ctrl3 Forbid +STXR-ctrla Allow +SpecCE-01 Forbid +SpecCE-02 Forbid +SpecCE-03 Allow +SpecCE-04 Allow +SpecCE-05 Allow +SpecCoiV Forbid +SpecCoiX Allow +SpecRfeX Allow +SpecRfiV Forbid +SpecRfiX Allow + diff --git a/catalogue/dependencies/tests/down-one-leg/mp-stxr-fail.litmus b/catalogue/dependencies/tests/down-one-leg/mp-stxr-fail.litmus new file mode 100644 index 000000000..46b863660 --- /dev/null +++ b/catalogue/dependencies/tests/down-one-leg/mp-stxr-fail.litmus @@ -0,0 +1,17 @@ +AArch64 MP-STXR-fail +{ +0:X1=x0; 0:X4=x1; 0:X5=x2; +1:X2=x1; 1:X4=x0; +} + P0 | P1 ; + LDR W0,[X1] | MOV W0,#1 ; + EOR W2,W0,W0 | MOV W1,#2 ; + ADD X5,X2,X5 | MOV W3,#3 ; + STR WZR,[X5] | STR W0,[X2] ; + LDXR W9,[X5] | STR W1,[X2] ; + STXR W2,W9,[X5] | DMB SY ; + EOR W6,W2,W2 | STR W3,[X4] ; + ADD X4,X6,X4 | ; + LDR W3,[X4] | ; +exists +(0:X0=3 /\ 0:X3=1 /\ 0:X2=1) diff --git a/catalogue/dependencies/tests/down-one-leg/mp-stxr-success.litmus b/catalogue/dependencies/tests/down-one-leg/mp-stxr-success.litmus new file mode 100644 index 000000000..1249aa004 --- /dev/null +++ b/catalogue/dependencies/tests/down-one-leg/mp-stxr-success.litmus @@ -0,0 +1,17 @@ +AArch64 MP-STXR-success +{ +0:X1=x0; 0:X4=x1; 0:X5=x2; +1:X2=x1; 1:X4=x0; +} + P0 | P1 ; + LDR W0,[X1] | MOV W0,#1 ; + EOR W2,W0,W0 | MOV W1,#2 ; + ADD X5,X2,X5 | MOV W3,#3 ; + STR WZR,[X5] | STR W0,[X2] ; + LDXR W9,[X5] | STR W1,[X2] ; + STXR W2,W9,[X5] | DMB SY ; + EOR W6,W2,W2 | STR W3,[X4] ; + ADD X4,X6,X4 | ; + LDR W3,[X4] | ; +exists +(0:X0=3 /\ 0:X3=1 /\ 0:X2=0) diff --git a/catalogue/dependencies/tests/down-one-leg/mp-stxr.litmus b/catalogue/dependencies/tests/down-one-leg/mp-stxr.litmus new file mode 100644 index 000000000..04539415a --- /dev/null +++ b/catalogue/dependencies/tests/down-one-leg/mp-stxr.litmus @@ -0,0 +1,17 @@ +AArch64 MP-STXR +{ +0:X1=x0; 0:X4=x1; 0:X5=x2; +1:X2=x1; 1:X4=x0; +} + P0 | P1 ; + LDR W0,[X1] | MOV W0,#1 ; + EOR W2,W0,W0 | MOV W1,#2 ; + ADD X5,X2,X5 | MOV W3,#3 ; + STR WZR,[X5] | STR W0,[X2] ; + LDXR W9,[X5] | STR W1,[X2] ; + STXR W2,W9,[X5] | DMB SY ; + EOR W2,W2,W2 | STR W3,[X4] ; + ADD X4,X2,X4 | ; + LDR W3,[X4] | ; +exists +(0:X0=3 /\ 0:X3=1) diff --git a/catalogue/dependencies/tests/pick-deps/LB+CSEL-addr-po+DMB.litmus b/catalogue/dependencies/tests/pick-deps/LB+CSEL-addr-po+DMB.litmus new file mode 100644 index 000000000..cce72748c --- /dev/null +++ b/catalogue/dependencies/tests/pick-deps/LB+CSEL-addr-po+DMB.litmus @@ -0,0 +1,15 @@ +AArch64 LB+CSEL-addr-po+DMB +{ +0:X1=x; 0:X4=a; 0:X5=b; 0:X8=y; +1:X1=x; 1:X8=y; +} +P0 | P1 ; +LDR X0,[X1] | LDR X0, [X8] ; +CMP X0, #1 | DMB SY ; +CSEL X3, X4, X5, EQ | MOV X2,#1 ; +STR X6, [X3] | STR X2,[X1] ; +MOV X7,#1 | ; +STR X7, [X8] | ; +exists + (0:X0=1 /\ 1:X0=1) + diff --git a/catalogue/dependencies/tests/pick-deps/LB+CSEL-data-po+DMB.litmus b/catalogue/dependencies/tests/pick-deps/LB+CSEL-data-po+DMB.litmus new file mode 100644 index 000000000..2755c2528 --- /dev/null +++ b/catalogue/dependencies/tests/pick-deps/LB+CSEL-data-po+DMB.litmus @@ -0,0 +1,14 @@ +AArch64 LB+CSEL-data-po+DMB +{ +0:X1=x; 0:X4=4; 0:X5=5; 0:X6=z; 0:X8=y; +1:X1=x; 1:X8=y; +} +P0 | P1 ; +LDR X0,[X1] | LDR X0, [X8] ; +CMP X0, #1 | DMB SY ; +CSEL X3, X4, X5, EQ | MOV X2,#1 ; +STR X3, [X6] | STR X2,[X1] ; +MOV X7,#1 | ; +STR X7, [X8] | ; +exists + (0:X0=1 /\ 1:X0=1) diff --git a/catalogue/dependencies/tests/pick-deps/LB+CSEL-rfi-data+DMB.litmus b/catalogue/dependencies/tests/pick-deps/LB+CSEL-rfi-data+DMB.litmus new file mode 100644 index 000000000..d54052e3d --- /dev/null +++ b/catalogue/dependencies/tests/pick-deps/LB+CSEL-rfi-data+DMB.litmus @@ -0,0 +1,16 @@ +AArch64 LB+CSEL-rfi-data+DMB +{ +0:X1=x; 0:X10=y; 0:X3=1; 0:X4=2; 0:X5=z; +1:X1=x; 1:X10=y ; 1:X2=1 ; +} +P0 | P1 ; +LDR W0,[X1] | LDR W0, [X10]; +CMP W0, #1 | DMB SY ; +CSEL W2, W3, W4, EQ | STR W2,[X1] ; +STR W2,[X5] | ; +LDR W6,[X5] | ; +EOR W8, W6, W6 | ; +ADD W9, W8, W3 | ; +STR W9, [X10] | ; +exists + (0:X0=1 /\ 1:X0=1) diff --git a/catalogue/dependencies/tests/pick-deps/LB+rel+CAS.litmus b/catalogue/dependencies/tests/pick-deps/LB+rel+CAS.litmus new file mode 100644 index 000000000..da2380b45 --- /dev/null +++ b/catalogue/dependencies/tests/pick-deps/LB+rel+CAS.litmus @@ -0,0 +1,11 @@ +AArch64 LB+rel+CAS +{ +0:X1=x; 0:X3=y; +1:X1=x; 1:X3=y; +} +P0 | P1 ; +MOV W9, #1 | MOV W4, #1 ; +LDR W0, [X3] | LDR W5, [X1] ; +STLR W9, [X1] | AND W10, W5, #2 ; + | CAS W10, W4, [X3] ; +exists (1:X5=1 /\ 0:X0=1) diff --git a/catalogue/dependencies/tests/pick-deps/LB+rel+data.litmus b/catalogue/dependencies/tests/pick-deps/LB+rel+data.litmus new file mode 100644 index 000000000..083c5da1b --- /dev/null +++ b/catalogue/dependencies/tests/pick-deps/LB+rel+data.litmus @@ -0,0 +1,16 @@ +AArch64 LB+rel+data +"PodRWPL RfeLP DpDatadW Rfe" +Generator=diyone7 (version 7.56+02~dev) +Prefetch=0:x=F,0:y=W,1:y=F,1:x=W +Com=Rf Rf +Orig=PodRWPL RfeLP DpDatadW Rfe +{ +0:X1=x; 0:X3=y; +1:X1=y; 1:X3=x; +} + P0 | P1 ; + LDR W0,[X1] | LDR W0,[X1] ; + MOV W2,#1 | EOR W2,W0,W0 ; + STLR W2,[X3] | ADD W2,W2,#1 ; + | STR W2,[X3] ; +exists (0:X0=1 /\ 1:X0=1) diff --git a/catalogue/dependencies/tests/pick-deps/MP+CSEL-rfi-addr-rfi-addr.litmus b/catalogue/dependencies/tests/pick-deps/MP+CSEL-rfi-addr-rfi-addr.litmus new file mode 100644 index 000000000..22328d84a --- /dev/null +++ b/catalogue/dependencies/tests/pick-deps/MP+CSEL-rfi-addr-rfi-addr.litmus @@ -0,0 +1,21 @@ +AArch64 MP+CSEL-rfi-addr-rfi-addr +{ +0:X10=x; 1:X10=x; +0:X2=y; 1:X2=y; +1:X6=z; 1:X12=v ; +1:X4=4; 1:X5=5; +} +P0 | P1 ; +MOV W9,#1 | LDR W1, [X2] ; +STR W9,[X10] | CMP W1, #1 ; +MOV W11,#1 | CSEL W3, W4, W5, EQ; +STLR W11,[X2] | STR W3, [X6] ; + | LDR W9, [X6] ; + | EOR W11, W9, W9 ; + | MOV W8,#2 ; + | STR W8,[X12, W11, SXTW] ; + | LDR W13, [X12]; + | EOR W14, W13, W13 ; + | LDR W16, [X10,W14,SXTW]; + +exists(1:X1=1 /\ 1:X16=0) diff --git a/catalogue/dependencies/tests/pick-deps/MP+rel+CAS-addr.litmus b/catalogue/dependencies/tests/pick-deps/MP+rel+CAS-addr.litmus new file mode 100644 index 000000000..7af7ddd05 --- /dev/null +++ b/catalogue/dependencies/tests/pick-deps/MP+rel+CAS-addr.litmus @@ -0,0 +1,15 @@ +AArch64 MP+rel+CAS-addr +{ +z=1; +0:X1=x; 0:X3=y; +1:X1=x; 1:X3=y; 1:X8=z; +} +P0 | P1 ; +MOV W0, #1 | LDR W0, [X1] ; +STR W0, [X3] | MOV W5, W0 ; +STLR W0, [X1] | CAS W0, W6, [X8] ; + | LDR W0, [X8] ; + | EOR X0, X0, X0 ; + | ADD X3, X3, X0 ; + | LDR W4, [X3] ; +exists (1:X5=1 /\ 1:X4=0) diff --git a/catalogue/dependencies/tests/pick-deps/MP+rel+CSEL-addr.litmus b/catalogue/dependencies/tests/pick-deps/MP+rel+CSEL-addr.litmus new file mode 100644 index 000000000..096ec1ef5 --- /dev/null +++ b/catalogue/dependencies/tests/pick-deps/MP+rel+CSEL-addr.litmus @@ -0,0 +1,15 @@ +AArch64 MP+rel+CSEL-addr +{ +0:X10=x; 1:X10=x; +0:X2=y; 1:X2=y; +1:X6=z; +} +P0 | P1 ; +MOV W9,#1 | LDR W1, [X2] ; +STR W9,[X10] | CMP W1, #1 ; +MOV W11,#1 | CSEL W3, W4, W5, EQ; +STLR W11,[X2] | STR W3, [X6] ; + | LDR W7, [X6] ; + | EOR X8, X7,X7 ; + | LDR W9,[X10,X8,SXTW] ; +exists(1:X1=1 /\ 1:X9=0) diff --git a/catalogue/dependencies/tests/pick-deps/MP+rel+CSEL-addr2.litmus b/catalogue/dependencies/tests/pick-deps/MP+rel+CSEL-addr2.litmus new file mode 100644 index 000000000..077589a65 --- /dev/null +++ b/catalogue/dependencies/tests/pick-deps/MP+rel+CSEL-addr2.litmus @@ -0,0 +1,16 @@ +AArch64 MP+rel+CSEL-addr2 +{ +0:X10=x; 1:X10=x; +0:X2=y; 1:X2=y; +1:X3=z; 1:X6=1; +1:X4=a; 1:X5=b; +} +P0 | P1 ; +MOV W9,#1 | LDR W1, [X2] ; +STR W9,[X10] | CMP W1, #1 ; +MOV W11,#1 | CSEL X3, X4, X5, EQ; +STLR W11,[X2] | STR W6, [X3] ; + | LDR W7, [X3] ; + | EOR X8, X7,X7 ; + | LDR W9,[X10,X8,SXTW] ; +exists(1:X1=1 /\ 1:X7=1 /\ 1:X9=0) diff --git a/catalogue/dependencies/tests/pick-deps/MP+rel+CSEL-rf-reg.litmus b/catalogue/dependencies/tests/pick-deps/MP+rel+CSEL-rf-reg.litmus new file mode 100644 index 000000000..aabcf520d --- /dev/null +++ b/catalogue/dependencies/tests/pick-deps/MP+rel+CSEL-rf-reg.litmus @@ -0,0 +1,11 @@ +AArch64 MP+rel+CSEL-rf-reg +{ +0:X10=x; 1:X10=x; +0:X2=y; 1:X2=y; +} +P0 | P1 ; +MOV X9,#1 | LDR X1, [X2] ; +STR X9,[X10] | CMP X1, #1 ; +MOV X11,#1 | CSEL X3, X4, X5, EQ; +STLR X11,[X2] | STR X3, [X10] ; +exists(1:X1=1 /\ x=1) diff --git a/catalogue/dependencies/tests/pick-deps/MP+rel+CSEL.litmus b/catalogue/dependencies/tests/pick-deps/MP+rel+CSEL.litmus new file mode 100644 index 000000000..a7da92612 --- /dev/null +++ b/catalogue/dependencies/tests/pick-deps/MP+rel+CSEL.litmus @@ -0,0 +1,12 @@ +AArch64 MP+rel+CSEL +{ +0:X10=x; 1:X10=x; +0:X2=y; 1:X2=y; +} +P0 | P1 ; +MOV X9,#1 | LDR X1, [X2] ; +STR X9,[X10] | CMP X1, #1 ; +MOV X11,#1 | CSEL X3, X4, X5, EQ; +STLR X11,[X2] | MOV X13,#2 ; + | STR X13, [X10] ; +exists(1:X1=1 /\ x=1) diff --git a/catalogue/dependencies/tests/pick-deps/Pick0.litmus b/catalogue/dependencies/tests/pick-deps/Pick0.litmus new file mode 100644 index 000000000..cab6bded5 --- /dev/null +++ b/catalogue/dependencies/tests/pick-deps/Pick0.litmus @@ -0,0 +1,15 @@ +AArch64 Pick0 +{ +0:X1=x; 0:X3=y; +1:X1=y; 1:X3=z; 1:X7=x; +} +P0 | P1 ; +MOV W0,#1 | LDR W0,[X1] ; +STR W0,[X1] | CBNZ W0,LC00 ; +MOV W2,#1 | LC00: ; +STLR W2,[X3] | MOV W2,#1 ; + | STR W2,[X3] ; + | SWP W4,W4,[X3] ; + | EOR W5,W4,W4 ; + | LDR W6,[X7,W5,SXTW] ; +exists (1:X0=1 /\ 1:X6=0) diff --git a/catalogue/dependencies/tests/pick-deps/Pick1.litmus b/catalogue/dependencies/tests/pick-deps/Pick1.litmus new file mode 100644 index 000000000..4a2ee3177 --- /dev/null +++ b/catalogue/dependencies/tests/pick-deps/Pick1.litmus @@ -0,0 +1,15 @@ +AArch64 Pick1 +{ +0:X1=x; 0:X3=y; +1:X1=y; 1:X3=z; 1:X7=x; +} +P0 | P1 ; +MOV W0,#1 | LDR W0,[X1] ; +STR W0,[X1] | CBNZ W0,LC00 ; +MOV W2,#1 | LC00: ; +STLR W2,[X3] | MOV W2,#1 ; + | STR W2,[X3] ; + | SWP W4,W4,[X3] ; + | EOR W5,W4,W4 ; + | LDR W6,[X7,W5,SXTW] ; +exists (1:X0=1 /\ 1:X6=0) diff --git a/catalogue/dependencies/tests/pick-deps/Pick2-noWZR.litmus b/catalogue/dependencies/tests/pick-deps/Pick2-noWZR.litmus new file mode 100644 index 000000000..41752f928 --- /dev/null +++ b/catalogue/dependencies/tests/pick-deps/Pick2-noWZR.litmus @@ -0,0 +1,14 @@ +AArch64 Pick2-noWZR +{ +0:X1=x; 0:X3=y; +1:X1=y; 1:X11=x; 1:X5=z; +} +P0 | P1 ; +MOV W0,#1 | LDR W0,[X1] ; +STR W0,[X1] | CMP W0,#1 ; +MOV W2,#1 | B.EQ L0 ; +STLR W2,[X3] | L0: ; + | SWP W22,W23,[X5] ; + | LDAPR W6,[X5] ; + | LDR W10,[X11] ; +exists (1:X0=1 /\ 1:X10=0) diff --git a/catalogue/dependencies/tests/pick-deps/Pick2.litmus b/catalogue/dependencies/tests/pick-deps/Pick2.litmus new file mode 100644 index 000000000..60b569ccf --- /dev/null +++ b/catalogue/dependencies/tests/pick-deps/Pick2.litmus @@ -0,0 +1,14 @@ +AArch64 Pick2 +{ +0:X1=x; 0:X3=y; +1:X1=y; 1:X11=x; 1:X5=z; +} +P0 | P1 ; +MOV W0,#1 | LDR W0,[X1] ; +STR W0,[X1] | CMP W0,#1 ; +MOV W2,#1 | B.EQ L0 ; +STLR W2,[X3] | L0: ; + | SWP WZR,WZR,[X5] ; + | LDAPR W6,[X5] ; + | LDR W10,[X11] ; +exists (1:X0=1 /\ 1:X10=0) diff --git a/catalogue/dependencies/tests/pick-deps/Pick3-mod.litmus b/catalogue/dependencies/tests/pick-deps/Pick3-mod.litmus new file mode 100644 index 000000000..f40285839 --- /dev/null +++ b/catalogue/dependencies/tests/pick-deps/Pick3-mod.litmus @@ -0,0 +1,15 @@ +AArch64 Pick3-mod +{ +0:X1=x; 0:X3=y; +1:X1=y; 1:X11=x; 1:X5=z; +} +P0 | P1 ; +MOV W0,#1 | LDR W0,[X1] ; +STR W0,[X1] | CMP W0,#1 ; +MOV W2,#1 | B.EQ L0 ; +STLR W2,[X3] | L0: ; + | STR W21, [X5]; + | SWP WZR,WZR,[X5] ; + | LDAPR W6,[X5] ; + | LDR W10,[X11] ; +exists (1:X0=1 /\ 1:X10=0) diff --git a/catalogue/dependencies/tests/pick-deps/Pick3.litmus b/catalogue/dependencies/tests/pick-deps/Pick3.litmus new file mode 100644 index 000000000..a2ea12742 --- /dev/null +++ b/catalogue/dependencies/tests/pick-deps/Pick3.litmus @@ -0,0 +1,14 @@ +AArch64 Pick3 +{ +0:X1=x; 0:X3=y; +1:X1=y; 1:X11=x; 1:X5=z; +} +P0 | P1 ; +MOV W0,#1 | LDR W0,[X1] ; +STR W0,[X1] | CMP W0,#1 ; +MOV W2,#1 | B.EQ L0 ; +STLR W2,[X3] | L0: ; + | SWP WZR,WZR,[X5] ; + | LDAPR W6,[X5] ; + | LDR W10,[X11] ; +exists (1:X0=1 /\ 1:X10=0) diff --git a/catalogue/dependencies/tests/pick-deps/Pick4.litmus b/catalogue/dependencies/tests/pick-deps/Pick4.litmus new file mode 100644 index 000000000..0e4123c46 --- /dev/null +++ b/catalogue/dependencies/tests/pick-deps/Pick4.litmus @@ -0,0 +1,12 @@ +AArch64 Pick4 +{ +0:X1=x; 0:X2=y; +1:X1=y; 1:X3=x; 1:X4=z; +} +P0 | P1 ; +MOV X0,#1 | LDR X0,[X1] ; +STR X0,[X1] | CMP X0,#1 ; +STLR X0,[X2] | CSEL X2,X3,X4,EQ ; + | LDR X5,[X2] ; +exists +(1:X0=1 /\ 1:X5=0) diff --git a/catalogue/dependencies/tests/pick-deps/S+rel+CSEL-data.litmus b/catalogue/dependencies/tests/pick-deps/S+rel+CSEL-data.litmus new file mode 100644 index 000000000..4544daea0 --- /dev/null +++ b/catalogue/dependencies/tests/pick-deps/S+rel+CSEL-data.litmus @@ -0,0 +1,16 @@ +AArch64 S+rel+CSEL-data +{ +0:X10=x; 1:X10=x; +0:X2=y; 1:X2=y; +1:X6=z; +} +P0 | P1 ; +MOV W9,#1 | LDR W1, [X2] ; +STR W9,[X10] | CMP W1, #1 ; +MOV W11,#1 | CSEL W3, W4, W5, EQ; +STLR W11,[X2] | STR W3, [X6] ; + | LDR W9, [X6] ; + | EOR X8, X9, X9 ; + | ADD W8,W8,#2 ; + | STR W8,[X10] ; +exists(1:X1=1 /\ x=1) diff --git a/catalogue/dependencies/tests/pick-deps/T10B.litmus b/catalogue/dependencies/tests/pick-deps/T10B.litmus new file mode 100644 index 000000000..1fc2f8d41 --- /dev/null +++ b/catalogue/dependencies/tests/pick-deps/T10B.litmus @@ -0,0 +1,19 @@ +AArch64 T10B +{ +0:X1=x; 0:X2=y; +1:X1=y; 1:X3=x; 1:X6=za; 1:X9=zb; +} +P0 | P1 ; +MOV X0,#1 | LDR X0,[X1] ; +LDR X3,[X1] | CMP X0,#0 ; +STLR X0,[X2] | CSEL X2,X4,X5,EQ ; + | STR X2,[X6] ; + | LDR X7,[X6] ; + | STR X7,[X9] ; + | LDR X8,[X9] ; + | EOR X10,X8,X8 ; + | ADD X10,X10,X3 ; + | MOV X11,#1 ; + | STR X11,[X10] ; +exists +(1:X0=1 /\ 0:X3=1) diff --git a/catalogue/dependencies/tests/pick-deps/T10C.litmus b/catalogue/dependencies/tests/pick-deps/T10C.litmus new file mode 100644 index 000000000..37cc3249f --- /dev/null +++ b/catalogue/dependencies/tests/pick-deps/T10C.litmus @@ -0,0 +1,17 @@ +AArch64 T10C +{ +0:X1=x; 0:X2=y; +1:X1=y; 1:X3=x; 1:X6=za; 1:X9=zb; +} +P0 | P1 ; +MOV X0,#1 | LDR X0,[X1] ; +LDR X3,[X1] | CMP X0,#0 ; +STLR X0,[X2] | CSEL X2,X4,X5,EQ ; + | STR X2,[X6] ; + | LDR X8,[X6] ; + | EOR X10,X8,X8 ; + | ADD X10,X10,X3 ; + | MOV X11,#1 ; + | STR X11,[X10] ; +exists +(1:X0=1 /\ 0:X3=1) diff --git a/catalogue/dependencies/tests/pick-deps/T11.litmus b/catalogue/dependencies/tests/pick-deps/T11.litmus new file mode 100644 index 000000000..a335d8116 --- /dev/null +++ b/catalogue/dependencies/tests/pick-deps/T11.litmus @@ -0,0 +1,17 @@ +AArch64 T11 +{ +0:X1=x; 0:X3=y; +1:X1=y; 1:X11=x; 1:X5=za; +} +P0 | P1 ; +MOV X0,#2 | LDR X0,[X1] ; +STR X0,[X1] | CMP X0,#1 ; +MOV X2,#1 | CSEL X2,X3,X4,EQ ; +STLR X2,[X3] | STR X2,[X5] ; + | LDXR X6,[X5] ; + | STXR W7,X8,[X5] ; + | LDR X9,[X5] ; + | EOR X10,X9,X9 ; + | ADD X10,X10,#1 ; + | STR X10,[X11] ; +exists (x=2 /\ 1:X0=1 /\ 1:X7=0) diff --git a/catalogue/dependencies/tests/pick-deps/T11bis.litmus b/catalogue/dependencies/tests/pick-deps/T11bis.litmus new file mode 100644 index 000000000..57760c161 --- /dev/null +++ b/catalogue/dependencies/tests/pick-deps/T11bis.litmus @@ -0,0 +1,17 @@ +AArch64 T11bis +{ +0:X1=x; 0:X3=y; +1:X1=y; 1:X11=x; 1:X5=za; +} +P0 | P1 ; +MOV X0,#2 | LDR X0,[X1] ; +STR X0,[X1] | CMP X0,#1 ; +MOV X2,#1 | MOV X2,X0 ; +STLR X2,[X3] | STR X2,[X5] ; + | LDXR X6,[X5] ; + | STXR W7,X8,[X5] ; + | LDR X9,[X5] ; + | EOR X10,X9,X9 ; + | ADD X10,X10,#1 ; + | STR X10,[X11] ; +exists (x=2 /\ 1:X0=1 /\ 1:X7=0) diff --git a/catalogue/dependencies/tests/pick-deps/T12.litmus b/catalogue/dependencies/tests/pick-deps/T12.litmus new file mode 100644 index 000000000..578b1dc62 --- /dev/null +++ b/catalogue/dependencies/tests/pick-deps/T12.litmus @@ -0,0 +1,17 @@ +AArch64 T12 +{ +0:X1=x; 0:X3=y; +1:X1=y; 1:X3=z; 1:X7=x; +} +P0 | P1 ; +MOV W0,#2 | LDR W0,[X1] ; +STR W0,[X1] | CMP W0,#0 ; +MOV W2,#1 | CSEL W2,W8,W9,EQ ; (* Allowed if non-pick data dep *) +STLR W2,[X3] | STR W2,[X3] ; + | MOV W4,#2 ; + | STR W4,[X3] ; + | LDR W5,[X3] ; + | EOR W6,W5,W5 ; + | ADD W6,W6,#1 ; + | STR W6,[X7] ; +exists (x=2 /\ z=2 /\ 1:X0=1 /\ 1:X5=2) diff --git a/catalogue/dependencies/tests/pick-deps/T12B.litmus b/catalogue/dependencies/tests/pick-deps/T12B.litmus new file mode 100644 index 000000000..4b7aec463 --- /dev/null +++ b/catalogue/dependencies/tests/pick-deps/T12B.litmus @@ -0,0 +1,17 @@ +AArch64 T12B +{ +0:X1=x; 0:X3=y; +1:X1=y; 1:X3=z; 1:X7=x; +} +P0 | P1 ; +MOV W0,#2 | LDR W0,[X1] ; +STR W0,[X1] | EOR W2,W0,W0 ; +MOV W2,#1 | ADD W2,W2,#1 ; +STLR W2,[X3] | STR W2,[X3] ; + | MOV W4,#2 ; + | STR W4,[X3] ; + | LDR W5,[X3] ; + | EOR W6,W5,W5 ; + | ADD W6,W6,#1 ; + | STR W6,[X7] ; +exists (x=2 /\ z=2 /\ 1:X0=1 /\ 1:X5=2) diff --git a/catalogue/dependencies/tests/pick-deps/T13-mod2.litmus b/catalogue/dependencies/tests/pick-deps/T13-mod2.litmus new file mode 100644 index 000000000..834d5a3c0 --- /dev/null +++ b/catalogue/dependencies/tests/pick-deps/T13-mod2.litmus @@ -0,0 +1,14 @@ +AArch64 T13-mod2 +{ +0:X1=x; 0:X3=y; +1:X1=y; 1:X11=x; 1:X5=z; +} +P0 | P1 ; +MOV X0,#1 | LDR X0,[X1] ; +STR X0,[X1] | CMP X0,#1 ; +MOV X2,#1 | B.NE L0 ; + | L0: ; +STLR X2,[X3] | STR X2,[X5] ; + | LDAR X9,[X5] ; + | LDR X10,[X11] ; +exists (1:X0=1 /\ 1:X10=0 /\ 1:X7=0) diff --git a/catalogue/dependencies/tests/pick-deps/T13-mod3.litmus b/catalogue/dependencies/tests/pick-deps/T13-mod3.litmus new file mode 100644 index 000000000..99ccb8d63 --- /dev/null +++ b/catalogue/dependencies/tests/pick-deps/T13-mod3.litmus @@ -0,0 +1,16 @@ +AArch64 T13-mod3 +{ +0:X1=x; 0:X3=y; +1:X1=y; 1:X11=x; 1:X5=z; +} +P0 | P1 ; +MOV X0,#1 | LDR X0,[X1] ; +STR X0,[X1] | CMP X0,#1 ; +MOV X2,#1 | B.NE L0 ; + | L0: ; +STLR X2,[X3] | STR X2,[X5] ; + | LDXR X6, [X5]; + | STXR W7, X8, [X5]; + | LDAR X9,[X5] ; + | LDR X10,[X11] ; +exists (1:X0=1 /\ 1:X10=0 /\ 1:X7=0) diff --git a/catalogue/dependencies/tests/pick-deps/T13-mod4.litmus b/catalogue/dependencies/tests/pick-deps/T13-mod4.litmus new file mode 100644 index 000000000..bc07faabf --- /dev/null +++ b/catalogue/dependencies/tests/pick-deps/T13-mod4.litmus @@ -0,0 +1,17 @@ +AArch64 T13-mod4 +{ +0:X1=x; 0:X3=y; +1:X1=y; 1:X11=x; 1:X5=z; +} +P0 | P1 ; +MOV X0,#1 | LDR X0,[X1] ; +STR X0,[X1] | CMP X0,#1 ; +MOV X2,#1 | B.NE L0 ; + | L0: ; +STLR X2,[X3] | STR X2,[X5] ; + | LDXR X6, [X5]; + | STXR W7, X8, [X5]; + | LDR X9,[X5] ; + | EOR X12, X9, X9; + | LDR X10,[X11, W12, SXTW] ; +exists (1:X0=1 /\ 1:X10=0 /\ 1:X7=0) diff --git a/catalogue/dependencies/tests/pick-deps/T13.litmus b/catalogue/dependencies/tests/pick-deps/T13.litmus new file mode 100644 index 000000000..fc287b3ef --- /dev/null +++ b/catalogue/dependencies/tests/pick-deps/T13.litmus @@ -0,0 +1,15 @@ +AArch64 T13 +{ +0:X1=x; 0:X3=y; +1:X1=y; 1:X11=x; 1:X5=z; +} +P0 | P1 ; +MOV X0,#1 | LDR X0,[X1] ; +STR X0,[X1] | CMP X0,#1 ; +MOV X2,#1 | CSEL X2,X3,X4,EQ ; +STLR X2,[X3] | STR X2,[X5] ; + | LDXR X6,[X5] ; (* Allowed if exclusives removed *) + | STXR W7,X8,[X5] ; + | LDAR X9,[X5] ; + | LDR X10,[X11] ; +exists (1:X0=1 /\ 1:X10=0 /\ 1:X7=0) diff --git a/catalogue/dependencies/tests/pick-deps/T13B.litmus b/catalogue/dependencies/tests/pick-deps/T13B.litmus new file mode 100644 index 000000000..8f966fb62 --- /dev/null +++ b/catalogue/dependencies/tests/pick-deps/T13B.litmus @@ -0,0 +1,15 @@ +AArch64 T13B +{ +0:X1=x; 0:X3=y; +1:X1=y; 1:X11=x; 1:X5=z; +} +P0 | P1 ; +MOV X0,#1 | LDR X0,[X1] ; +STR X0,[X1] | CMP X0,#1 ; +MOV X2,#1 | CSEL X2,X3,X4,EQ ; +STLR X2,[X3] | STR X2,[X5] ; + | LDR X6,[X5] ; (* Allowed if exclusives removed *) + | STR X8,[X5] ; + | LDAR X9,[X5] ; + | LDR X10,[X11] ; +exists (1:X0=1 /\ 1:X10=0) diff --git a/catalogue/dependencies/tests/pick-deps/T14-controldep.litmus b/catalogue/dependencies/tests/pick-deps/T14-controldep.litmus new file mode 100644 index 000000000..749488481 --- /dev/null +++ b/catalogue/dependencies/tests/pick-deps/T14-controldep.litmus @@ -0,0 +1,17 @@ +AArch64 T14-controldep +{ +0:X1=x; 0:X3=y; +1:X1=y; 1:X11=x; 1:X5=za; 1:X8=zb; +} +P0 | P1 ; +MOV X0,#1 | LDR X0,[X1] ; +STR X0,[X1] | CMP X0,#1 ; +MOV X2,#1 | B.NE L0 ; + | L0: ; +STLR X2,[X3] | STR X2,[X5] ; + | LDAR X6,[X5] ; + | LDR X7,[X8] ; + | STR X7,[X8] ; + | LDAR X9,[X8] ; + | LDR X10,[X11] ; +exists (1:X0=1 /\ 1:X10=0) diff --git a/catalogue/dependencies/tests/pick-deps/T14.litmus b/catalogue/dependencies/tests/pick-deps/T14.litmus new file mode 100644 index 000000000..790e52265 --- /dev/null +++ b/catalogue/dependencies/tests/pick-deps/T14.litmus @@ -0,0 +1,16 @@ +AArch64 T14 +{ +0:X1=x; 0:X3=y; +1:X1=y; 1:X11=x; 1:X5=za; 1:X8=zb; +} +P0 | P1 ; +MOV X0,#1 | LDR X0,[X1] ; +STR X0,[X1] | CMP X0,#1 ; +MOV X2,#1 | CSEL X2,X3,X4,EQ ; +STLR X2,[X3] | STR X2,[X5] ; + | LDAR X6,[X5] ; + | LDR X7,[X8] ; + | STR X7,[X8] ; + | LDAR X9,[X8] ; + | LDR X10,[X11] ; +exists (1:X0=1 /\ 1:X10=0) diff --git a/catalogue/dependencies/tests/pick-deps/T14B-controldep.litmus b/catalogue/dependencies/tests/pick-deps/T14B-controldep.litmus new file mode 100644 index 000000000..4cf531cd6 --- /dev/null +++ b/catalogue/dependencies/tests/pick-deps/T14B-controldep.litmus @@ -0,0 +1,17 @@ +AArch64 T14B-controldep +{ +0:X1=x; 0:X3=y; +1:X1=y; 1:X11=x; 1:X5=za; 1:X8=zb; +} +P0 | P1 ; +MOV X0,#1 | LDR X0,[X1] ; +STR X0,[X1] | CMP X0,#1 ; +MOV X2,#1 | B.EQ L0 ; +STLR X2,[X3] | L0: ; + | STR X2,[X5] ; + | LDAR X6,[X5] ; + | LDXR X7,[X8] ; + | STXR W12,X7,[X8] ; + | LDAR X9,[X8] ; + | LDR X10,[X11] ; +exists (1:X0=1 /\ 1:X10=0 /\ 1:X12=0) diff --git a/catalogue/dependencies/tests/pick-deps/T14B-corrected.litmus b/catalogue/dependencies/tests/pick-deps/T14B-corrected.litmus new file mode 100644 index 000000000..966145741 --- /dev/null +++ b/catalogue/dependencies/tests/pick-deps/T14B-corrected.litmus @@ -0,0 +1,16 @@ +AArch64 T14B-corrected +{ +0:X1=x; 0:X3=y; +1:X1=y; 1:X11=x; 1:X5=za; 1:X8=zb; +} +P0 | P1 ; +MOV X0,#1 | LDR X0,[X1] ; +STR X0,[X1] | CMP X0,#1 ; +MOV X2,#1 | CSEL X2,X3,X4,EQ ; +STLR X2,[X3] | STR X2,[X5] ; + | LDAR X6,[X5] ; + | LDXR X7,[X8] ; + | STXR W12,X17,[X8] ; + | LDAR X9,[X8] ; + | LDR X10,[X11] ; +exists (1:X0=1 /\ 1:X10=0 /\ 1:X12=0) diff --git a/catalogue/dependencies/tests/pick-deps/T14B.litmus b/catalogue/dependencies/tests/pick-deps/T14B.litmus new file mode 100644 index 000000000..a3ae7563e --- /dev/null +++ b/catalogue/dependencies/tests/pick-deps/T14B.litmus @@ -0,0 +1,16 @@ +AArch64 T14B +{ +0:X1=x; 0:X3=y; +1:X1=y; 1:X11=x; 1:X5=za; 1:X8=zb; +} +P0 | P1 ; +MOV X0,#1 | LDR X0,[X1] ; +STR X0,[X1] | CMP X0,#1 ; +MOV X2,#1 | CSEL X2,X3,X4,EQ ; +STLR X2,[X3] | STR X2,[X5] ; + | LDAR X6,[X5] ; + | LDXR X7,[X8] ; + | STXR W12,X7,[X8] ; + | LDAR X9,[X8] ; + | LDR X10,[X11] ; +exists (1:X0=1 /\ 1:X10=0 /\ 1:X12=0) diff --git a/catalogue/dependencies/tests/pick-deps/T14Bbis-corrected.litmus b/catalogue/dependencies/tests/pick-deps/T14Bbis-corrected.litmus new file mode 100644 index 000000000..a2b8b870c --- /dev/null +++ b/catalogue/dependencies/tests/pick-deps/T14Bbis-corrected.litmus @@ -0,0 +1,16 @@ +AArch64 T14Bbis-corrected +{ +0:X1=x; 0:X3=y; +1:X1=y; 1:X11=x; 1:X5=za; 1:X8=zb; +} +P0 | P1 ; +MOV X0,#1 | LDR X0,[X1] ; +STR X0,[X1] | CMP X0,#1 ; +MOV X2,#1 | CSEL X2,X3,X4,EQ ; +STLR X2,[X3] | STR X2,[X5] ; + | LDAR X6,[X5] ; + | LDR X7,[X8] ; + | STR X12,[X8] ; + | LDAR X9,[X8] ; + | LDR X10,[X11] ; +exists (1:X0=1 /\ 1:X10=0 /\ 1:X12=0) diff --git a/catalogue/dependencies/tests/pick-deps/T14Bbis.litmus b/catalogue/dependencies/tests/pick-deps/T14Bbis.litmus new file mode 100644 index 000000000..1413e4a9b --- /dev/null +++ b/catalogue/dependencies/tests/pick-deps/T14Bbis.litmus @@ -0,0 +1,16 @@ +AArch64 T14Bbis +{ +0:X1=x; 0:X3=y; +1:X1=y; 1:X11=x; 1:X5=za; 1:X8=zb; +} +P0 | P1 ; +MOV X0,#1 | LDR X0,[X1] ; +STR X0,[X1] | CMP X0,#1 ; +MOV X2,#1 | CSEL X2,X3,X4,EQ ; +STLR X2,[X3] | STR X2,[X5] ; + | LDAR X6,[X5] ; + | LDR X7,[X8] ; + | STR X12,[X8] ; + | LDAR X9,[X8] ; + | LDR X10,[X11] ; +exists (1:X0=1 /\ 1:X10=0 /\ 1:X12=0) diff --git a/catalogue/dependencies/tests/pick-deps/T15-corrected.litmus b/catalogue/dependencies/tests/pick-deps/T15-corrected.litmus new file mode 100644 index 000000000..4b56554f0 --- /dev/null +++ b/catalogue/dependencies/tests/pick-deps/T15-corrected.litmus @@ -0,0 +1,16 @@ +AArch64 T15-corrected +{ +0:X1=x; 0:X3=y; +1:X1=y; 1:X11=x; 1:X5=z; +} +P0 | P1 ; +MOV X0,#1 | LDR X0,[X1] ; +STR X0,[X1] | CMP X0,#1 ; +MOV X2,#1 | CSEL X2,X3,X4,EQ ; +STLR X2,[X3] | STR X2,[X5] ; + | LDR X6,[X5] ; + | CBNZ X6,L0 ; + | L0: ; + | ISB ; + | LDR X10,[X11] ; +exists (1:X0=1 /\ 1:X10=0) diff --git a/catalogue/dependencies/tests/pick-deps/T15-datadep-corrected.litmus b/catalogue/dependencies/tests/pick-deps/T15-datadep-corrected.litmus new file mode 100644 index 000000000..8296f843b --- /dev/null +++ b/catalogue/dependencies/tests/pick-deps/T15-datadep-corrected.litmus @@ -0,0 +1,16 @@ +AArch64 T15-datadep-corrected +{ +0:X1=x; 0:X3=y; +1:X1=y; 1:X11=x; 1:X5=z; +} +P0 | P1 ; +MOV X0,#1 | LDR X0,[X1] ; +STR X0,[X1] | ; +MOV X2,#1 | MOV X2, X0 ; +STLR X2,[X3] | STR X2,[X5] ; + | LDR X6,[X5] ; + | CBNZ X6,L0 ; + | L0: ; + | ISB ; + | LDR X10,[X11] ; +exists (1:X0=1 /\ 1:X10=0) diff --git a/catalogue/dependencies/tests/pick-deps/T3-bis.litmus b/catalogue/dependencies/tests/pick-deps/T3-bis.litmus new file mode 100644 index 000000000..0f39b3073 --- /dev/null +++ b/catalogue/dependencies/tests/pick-deps/T3-bis.litmus @@ -0,0 +1,14 @@ +AArch64 T3-bis +{ +0:X1=x; 0:X3=y; 0:X10=za; 0:X11=zb; +1:X1=y; 1:X3=x; +} +P0 | P1 ; +LDR W0,[X1] | LDAR W0,[X1] ; +CMP W0,#0 | MOV W2,#1 ; +CSEL X5,X10,X11,EQ | STR W2,[X3] ; +LDR X4,[X5] | ; +MOV W2,#1 | ; +STR W2,[X3] | ; +exists +(0:X0=1 /\ 1:X0=1) diff --git a/catalogue/dependencies/tests/pick-deps/T3.litmus b/catalogue/dependencies/tests/pick-deps/T3.litmus new file mode 100644 index 000000000..5a316e33a --- /dev/null +++ b/catalogue/dependencies/tests/pick-deps/T3.litmus @@ -0,0 +1,15 @@ +AArch64 T3 +{ +0:X1=x; 0:X3=y; 0:X10=za; 0:X11=zb; +1:X1=y; 1:X3=x; +} +P0 | P1 ; +LDR W0,[X1] | LDAR W0,[X1] ; +CMP W0,#0 | MOV W2,#1 ; +CSEL X5,X10,X11,EQ | STR W2,[X3] ; +STR X4,[X5] | ; +LDR X4,[X5] | ; +MOV W2,#1 | ; +STR W2,[X3] | ; +exists +(0:X0=1 /\ 1:X0=1) diff --git a/catalogue/dependencies/tests/pick-deps/T5.litmus b/catalogue/dependencies/tests/pick-deps/T5.litmus new file mode 100644 index 000000000..beef32dd7 --- /dev/null +++ b/catalogue/dependencies/tests/pick-deps/T5.litmus @@ -0,0 +1,20 @@ +AArch64 T5 +{ +0:X1=x; 0:X9=y; 0:X5=z; 0:X7=p; 0:X8=q; +1:X1=y; 1:X3=x; +} +P0 | P1 ; +LDR X0,[X1] | LDAR X0,[X1] ; +CMP X0,#1 | MOV X2,#1 ; +MOV X3,#0 | STR X2,[X3] ; +MOV X4,#1 | ; +CSEL X2,X3,X4,EQ | ; +STR X2,[X5] | ; +LDR X2,[X5] | ; +CMP X2,#0 | ; +CSEL X6,X7,X8,EQ | ; +LDR X10,[X6] | ; +MOV X2,#1 | ; +STR X2,[X9] | ; +exists +(0:X0=1 /\ 1:X0=1) diff --git a/catalogue/dependencies/tests/pick-deps/T6.litmus b/catalogue/dependencies/tests/pick-deps/T6.litmus new file mode 100644 index 000000000..b8560d627 --- /dev/null +++ b/catalogue/dependencies/tests/pick-deps/T6.litmus @@ -0,0 +1,19 @@ +AArch64 T6 +{ +0:X1=x; 0:X9=y; 0:X5=z; 0:X7=a; +1:X1=y; 1:X3=x; +} +P0 | P1 ; +LDR W0,[X1] | LDAR W0,[X1] ; +CMP W0,#1 | MOV W2,#1 ; +MOV X3,#0 | STR W2,[X3] ; +MOV X4,#1 | ; +CSEL X2,X3,X4,EQ | ; +STR X2,[X5] | ; +LDR X2,[X5] | ; +LDR X6,[X7] | ; +MOV W2,#1 | ; +STR W2,[X9] | ; +exists +(0:X0=1 /\ 1:X0=1) + diff --git a/catalogue/dependencies/tests/pick-deps/T7.litmus b/catalogue/dependencies/tests/pick-deps/T7.litmus new file mode 100644 index 000000000..35a05421f --- /dev/null +++ b/catalogue/dependencies/tests/pick-deps/T7.litmus @@ -0,0 +1,18 @@ +AArch64 T7 +{ +0:X1=x; 0:X9=y; 0:X5=z; 0:X7=a; +1:X1=y; 1:X3=x; +} +P0 | P1 ; +LDR W0,[X1] | LDAR W0,[X1] ; +CMP W0,#1 | MOV W2,#1 ; +MOV X3,#0 | STR W2,[X3] ; +MOV X4,#1 | ; +CSEL X2,X3,X4,EQ | ; +STR X2,[X5] | ; +LDAR X2,[X5] | ; (* Ordered if dep *) +LDR X8,[X7] | ; +MOV W2,#1 | ; +STR W2,[X9] | ; +exists +(0:X0=1 /\ 1:X0=1) diff --git a/catalogue/dependencies/tests/pick-deps/T7bis.litmus b/catalogue/dependencies/tests/pick-deps/T7bis.litmus new file mode 100644 index 000000000..45933fed6 --- /dev/null +++ b/catalogue/dependencies/tests/pick-deps/T7bis.litmus @@ -0,0 +1,18 @@ +AArch64 T7bis +{ +0:X1=x; 0:X9=y; 0:X5=z; 0:X7=a; +1:X1=y; 1:X3=x; +} +P0 | P1 ; +LDR W0,[X1] | LDAR W0,[X1] ; +CMP W0,#1 | MOV W2,#1 ; +MOV X3,#0 | STR W2,[X3] ; +MOV X4,#1 | ; +MOV X2,X0 | ; +STR X2,[X5] | ; +LDAR X2,[X5] | ; (* Ordered if dep *) +LDR X8,[X7] | ; +MOV W2,#1 | ; +STR W2,[X9] | ; +exists +(0:X0=1 /\ 1:X0=1) diff --git a/catalogue/dependencies/tests/pick-deps/T7dep.litmus b/catalogue/dependencies/tests/pick-deps/T7dep.litmus new file mode 100644 index 000000000..85439b570 --- /dev/null +++ b/catalogue/dependencies/tests/pick-deps/T7dep.litmus @@ -0,0 +1,19 @@ +AArch64 T7dep +{ +0:X1=x; 0:X9=y; 0:X5=z; 0:X7=a; +1:X1=y; 1:X3=x; +} +P0 | P1 ; +LDR W0,[X1] | LDAR W0,[X1] ; +CMP W0,#1 | MOV W2,#1 ; +MOV X3,#0 | STR W2,[X3] ; +MOV X4,#1 | ; +CSEL X2,X3,X4,EQ | ; +STR X2,[X5] | ; +LDR X2,[X5] | ; (* Ordered if dep *) +EOR X10, X2, X2 | ; +LDR X8,[X7, W10, SXTW] | ; +MOV W2,#1 | ; +STR W2,[X9] | ; +exists +(0:X0=1 /\ 1:X0=1) diff --git a/catalogue/dependencies/tests/pick-deps/T7ter.litmus b/catalogue/dependencies/tests/pick-deps/T7ter.litmus new file mode 100644 index 000000000..e0449381d --- /dev/null +++ b/catalogue/dependencies/tests/pick-deps/T7ter.litmus @@ -0,0 +1,18 @@ +AArch64 T7ter +{ +0:X1=x; 0:X9=y; 0:X5=z; +1:X1=y; 1:X3=x; +} +P0 | P1 ; +LDR W0,[X1] | LDAR W0,[X1] ; +CMP W0,#1 | MOV W2,#1 ; +MOV X3,#0 | STR W2,[X3] ; +MOV X4,#1 | ; +MOV X2,X0 | ; +STR X2,[X5] | ; +LDR X2,[X5] | ; (* Ordered if dep *) +EOR W7,W2,W2 | ; +MOV W2,#1 | ; +STR W2,[X9,W7,SXTW]| ; +exists +(0:X0=1 /\ 1:X0=1) diff --git a/catalogue/dependencies/tests/pick-deps/T8+BIS.litmus b/catalogue/dependencies/tests/pick-deps/T8+BIS.litmus new file mode 100644 index 000000000..7f53a7344 --- /dev/null +++ b/catalogue/dependencies/tests/pick-deps/T8+BIS.litmus @@ -0,0 +1,18 @@ +AArch64 T8+BIS +{ +0:X1=x; 0:X10=y; 0:X5=z; +1:X1=y; 1:X3=x; +} +P0 | P1 ; +LDR W0,[X1] | LDAR W0,[X1] ; +CMP W0,#1 | MOV W2,#1 ; +CSEL X2,X3,X4,EQ | STR W2,[X3] ; +STR X2,[X5] | ; +LDXR X3,[X5] | ; +LDR X8,[X5] | ; +EOR X9,X8,X8 | ; +ADD X9,X9,X10 | ; +MOV W11,#1 | ; +STR W11,[X9] | ; +exists +(0:X0=1 /\ 0:X7=0 /\ 1:X0=1) diff --git a/catalogue/dependencies/tests/pick-deps/T8.litmus b/catalogue/dependencies/tests/pick-deps/T8.litmus new file mode 100644 index 000000000..155f85e35 --- /dev/null +++ b/catalogue/dependencies/tests/pick-deps/T8.litmus @@ -0,0 +1,19 @@ +AArch64 T8 +{ +0:X1=x; 0:X10=y; 0:X5=z; +1:X1=y; 1:X3=x; +} +P0 | P1 ; +LDR W0,[X1] | LDAR W0,[X1] ; +CMP W0,#1 | MOV W2,#1 ; +CSEL X2,X3,X4,EQ | STR W2,[X3] ; +STR X2,[X5] | ; +LDXR X3,[X5] | ; +STXR W7,X4,[X5] | ; (* Remove me *) +LDR X8,[X5] | ; +EOR X9,X8,X8 | ; +ADD X9,X9,X10 | ; +MOV W11,#1 | ; +STR W11,[X9] | ; +exists +(0:X0=1 /\ 0:X7=0 /\ 1:X0=1) diff --git a/catalogue/dependencies/tests/pick-deps/T9.litmus b/catalogue/dependencies/tests/pick-deps/T9.litmus new file mode 100644 index 000000000..1d2fef09c --- /dev/null +++ b/catalogue/dependencies/tests/pick-deps/T9.litmus @@ -0,0 +1,12 @@ +AArch64 T9 +{ +0:X1=x; 0:X2=y; +1:X1=y; 1:X3=x; 1:X4=z; +} +P0 | P1 ; +MOV X0,#1 | LDR X0,[X1] ; +STR X0,[X1] | CMP X0,#1 ; +STLR X0,[X2] | CSEL X2,X3,X4,EQ ; + | LDR X5,[X2] ; (* What causes replay on misprediction? *) +exists +(1:X0=1 /\ 1:X5=0) diff --git a/catalogue/dependencies/tests/pick-deps/T99-STADD.litmus b/catalogue/dependencies/tests/pick-deps/T99-STADD.litmus new file mode 100644 index 000000000..d10da7164 --- /dev/null +++ b/catalogue/dependencies/tests/pick-deps/T99-STADD.litmus @@ -0,0 +1,15 @@ +AArch64 T99-STADD +{ +0:X1=x; 0:X3=y; +1:X1=y; 1:X11=x; 1:X5=z; +} +P0 | P1 ; +MOV W0,#1 | LDR W0,[X1] ; +STR W0,[X1] | CMP W0,#1 ; +MOV W2,#1 | B.EQ L0 ; +STLR W2,[X3] | L0: ; + | STR W21, [X5]; + | STADD W18, [X5]; + | LDAR W26, [X5]; + | LDR W10,[X11] ; +exists (1:X0=1 /\ 1:X10=0 /\ 1:X16=0) diff --git a/catalogue/dependencies/tests/pick-deps/T99-excls-RZR.litmus b/catalogue/dependencies/tests/pick-deps/T99-excls-RZR.litmus new file mode 100644 index 000000000..b47c468b5 --- /dev/null +++ b/catalogue/dependencies/tests/pick-deps/T99-excls-RZR.litmus @@ -0,0 +1,16 @@ +AArch64 T99-excls-RZR +{ +0:X1=x; 0:X3=y; +1:X1=y; 1:X11=x; 1:X5=z; +} +P0 | P1 ; +MOV W0,#1 | LDR W0,[X1] ; +STR W0,[X1] | CMP W0,#1 ; +MOV W2,#1 | B.EQ L0 ; +STLR W2,[X3] | L0: ; + | STR W21, [X5]; + | LDXR WZR, [X5]; + | STXR W16, W15, [X5]; + | LDAR W26, [X5]; + | LDR W10,[X11] ; +exists (1:X0=1 /\ 1:X10=0 /\ 1:X16=0) diff --git a/catalogue/dependencies/tests/pick-deps/T99-excls.litmus b/catalogue/dependencies/tests/pick-deps/T99-excls.litmus new file mode 100644 index 000000000..a4ecfaf19 --- /dev/null +++ b/catalogue/dependencies/tests/pick-deps/T99-excls.litmus @@ -0,0 +1,16 @@ +AArch64 T99-excls +{ +0:X1=x; 0:X3=y; +1:X1=y; 1:X11=x; 1:X5=z; +} +P0 | P1 ; +MOV W0,#1 | LDR W0,[X1] ; +STR W0,[X1] | CMP W0,#1 ; +MOV W2,#1 | B.EQ L0 ; +STLR W2,[X3] | L0: ; + | STR W21, [X5]; + | LDXR W14, [X5]; + | STXR W16, W15, [X5]; + | LDAR W26, [X5]; + | LDR W10,[X11] ; +exists (1:X0=1 /\ 1:X10=0 /\ 1:X16=0) diff --git a/catalogue/dependencies/tests/pick-deps/T99.litmus b/catalogue/dependencies/tests/pick-deps/T99.litmus new file mode 100644 index 000000000..e70d127c3 --- /dev/null +++ b/catalogue/dependencies/tests/pick-deps/T99.litmus @@ -0,0 +1,15 @@ +AArch64 T99 +{ +0:X1=x; 0:X3=y; +1:X1=y; 1:X11=x; 1:X5=z; +} +P0 | P1 ; +MOV W0,#1 | LDR W0,[X1] ; +STR W0,[X1] | CMP W0,#1 ; +MOV W2,#1 | B.EQ L0 ; +STLR W2,[X3] | L0: ; + | STR W21, [X5]; + | SWP W15, W14, [X5]; + | LDAR W26, [X5]; + | LDR W10,[X11] ; +exists (1:X0=1 /\ 1:X10=0) diff --git a/catalogue/dependencies/tests/pick-deps/T9B.litmus b/catalogue/dependencies/tests/pick-deps/T9B.litmus new file mode 100644 index 000000000..dfdfab980 --- /dev/null +++ b/catalogue/dependencies/tests/pick-deps/T9B.litmus @@ -0,0 +1,16 @@ +AArch64 T9B +{ +0:X1=x; 0:X2=y; +1:X1=y; 1:X3=x; +} +P0 | P1 ; +MOV X0,#1 | LDR X0,[X1] ; +STR X0,[X1] | CMP X0,#0 ; +STLR X0,[X2] | CSEL X2,X4,X5,EQ ; + | CBNZ X2,LC00 ; (* Change to X0 and becomes forbidden *) + | LC00: ; + | ISB ; + | LDR X6,[X3] ; +exists +(1:X0=1 /\ 1:X6=0) + diff --git a/catalogue/dependencies/tests/pick-deps/T9C.litmus b/catalogue/dependencies/tests/pick-deps/T9C.litmus new file mode 100644 index 000000000..509f756df --- /dev/null +++ b/catalogue/dependencies/tests/pick-deps/T9C.litmus @@ -0,0 +1,13 @@ +AArch64 T9C +{ +0:X1=x; 0:X2=y; +1:X1=y; 1:X3=x; 1:X4=za; 1:X5=zb; +} +P0 | P1 ; +MOV X0,#1 | LDR X0,[X1] ; +STR X0,[X1] | CMP X0,#0 ; +STLR X0,[X2] | CSEL X2,X4,X5,EQ ; + | LDAR X6,[X2] ; + | LDR X7,[X3] ; +exists +(1:X0=1 /\ 1:X7=0) diff --git a/catalogue/dependencies/tests/pick-deps/TLDAR.litmus b/catalogue/dependencies/tests/pick-deps/TLDAR.litmus new file mode 100644 index 000000000..f73bfa8ed --- /dev/null +++ b/catalogue/dependencies/tests/pick-deps/TLDAR.litmus @@ -0,0 +1,13 @@ +AArch64 TLDAR +{ +0:X1=x; 0:X3=y; +1:X1=y; 1:X11=x; 1:X5=z; +} +P0 | P1 ; +MOV X0,#1 | LDR X0,[X1] ; +STR X0,[X1] | CMP X0,#1 ; +MOV X2,#1 | CSEL X2,X3,X4,EQ ; +STLR X2,[X3] | STR X2,[X5] ; + | LDAR X9,[X5] ; + | LDR X10,[X11] ; +exists (1:X0=1 /\ 1:X10=0 /\ 1:X7=0) diff --git a/catalogue/dependencies/tests/pick-deps/TTOB.litmus b/catalogue/dependencies/tests/pick-deps/TTOB.litmus new file mode 100644 index 000000000..b2dd3181b --- /dev/null +++ b/catalogue/dependencies/tests/pick-deps/TTOB.litmus @@ -0,0 +1,15 @@ +AArch64 TTOB +{ +0:X1=x:green; 0:X3=y:green; +1:X1=y:green; 1:X11=x:green; 1:X5=za:green; +1:X3=za:blue; 1:X4=za:red; 1:X6=1; +} +P0 | P1 ; +MOV X0,#2 | LDR X0,[X1] ; +STR X0,[X1] | CMP X0,#1 ; +MOV X2,#1 | CSEL X2,X3,X4,EQ ; +STLR X2,[X3] | STG X2,[X5] ; (* Set allocation tag for za *) + | STR X6,[X2] ; (* Checked store to za using new tag *) + | MOV X10,#1 ; + | STR X10,[X11] ; +exists (x=2 /\ 1:X0=1 /\ za=1 /\ ~fault(P1,za)) diff --git a/catalogue/dependencies/tests/pick-deps/TTOB2.litmus b/catalogue/dependencies/tests/pick-deps/TTOB2.litmus new file mode 100644 index 000000000..8edb281f2 --- /dev/null +++ b/catalogue/dependencies/tests/pick-deps/TTOB2.litmus @@ -0,0 +1,15 @@ +AArch64 TTOB2 +{ +0:X1=x:indeed; 0:X3=y:indeed; +1:X1=y:indeed; 1:X11=x:indeed; 1:X5=za:indeed; +1:X3=za:ohyeah; 1:X4=za:yes; 1:X6=1; +} +P0 | P1 ; +MOV X0,#2 | LDR X0,[X1] ; +STR X0,[X1] | CMP X0,#1 ; +MOV X2,#1 | CSEL X2,X3,X4,EQ ; +STLR X2,[X3] | STG X2,[X5] ; (* Set allocation tag for za *) + | STR X6,[X2] ; (* Checked store to za using new tag *) + | MOV X10,#1 ; + | STR X10,[X11] ; +exists (x=2 /\ 1:X0=1 /\ za=1 /\ ~fault(P1,za)) diff --git a/catalogue/dependencies/tests/pick-deps/desired-kinds.txt b/catalogue/dependencies/tests/pick-deps/desired-kinds.txt new file mode 100644 index 000000000..721a226ea --- /dev/null +++ b/catalogue/dependencies/tests/pick-deps/desired-kinds.txt @@ -0,0 +1,54 @@ +MP+rel+CAS-addr Allow +MP+rel+CSEL-addr Allow +MP+rel+CSEL-addr2 Allow +LB+rel+CAS Forbid +LB+CSEL-rfi-data+DMB Forbid +S+rel+CSEL-data Forbid +S+rel+CSEL-data2 Forbid +MP+CSEL-rfi-addr-rfi-addr Allow +LB+CSEL-addr-po+DMB Forbid +LB+CSEL-data-po+DMB Allow +MP+rel+CSEL-rfi-data-rfi-addr Allow +S+rel+CSEL-rfi-data-rfi-addr Forbid +S+rel+CSEL-rfi-ctrl Forbid +T3 Forbid +T3-bis Forbid +S+DMB.ST+CSEL-ctrl Forbid +LB+rel+data Forbid +MP+rel+CSEL Allow +MP+rel+CSEL-rf-reg Forbid +T7 Forbid +T7dep Forbid +T8 Allow +T8+BIS Forbid +T9 Allow +T9B Forbid +T9C Allow +T10B Forbid +T10C Forbid +T11 Allow +T12 Allow +T12B Allow +T13 Forbid +T13B Allow +T13-mod2 Allow +T13-mod3 Forbid +T13-mod4 Allow +T14 Allow +T14B Forbid +T14B-corrected Forbid +T14-controldep Allow +T14B-controldep Forbid +TLDAR Allow +Pick3 Forbid +Pick3-mod Forbid +T99 Forbid +T99-excls Forbid +T99-excls-RZR Forbid +T99-STADD Forbid +Pick0 Allow +Pick1 Allow +Pick2 Forbid +Pick2-noWZR Forbid +T15-corrected Forbid +T15-datadep-corrected Forbid