Merge pull request #612 from artkhyzha/add-ctrl-to-br

[herd,aarch64] Adding ctrl to indirect branches

This is a draft PR aimed at making indirect branches create control dependencies.

The idea is to simply let the indirect branches to create a "commit" type of an event; then the `aarch64deps.cat` should automatically draw `ctrl` edges.

herd/AArch64Sem.ml

@@ -2009,9 +2009,11 @@ module Make
         | M.A.V.Val (Concrete i) -> Some (B.Addr (M.A.V.Cst.Scalar.to_int i))
         | _ -> None
 
-      let do_indirect_jump test bds i v =
+      let do_indirect_jump test bds i ii v =
         match  v2tgt v with
-        | Some tgt -> M.unitT (B.Jump (tgt,bds))
+        | Some tgt ->
+          commit_bcc ii
+          >>= fun () -> M.unitT (B.Jump (tgt,bds))
         | None ->
            match v with
            | M.A.V.Var(_) as v ->
@@ -2021,7 +2023,8 @@ module Make
                   "Could find no potential target for indirect branch %s \
                    (potential targets are statically known labels)" (AArch64.dump_instruction i)
               else
-                B.indirectBranchT v lbls bds
+                commit_bcc ii
+                >>= fun () -> B.indirectBranchT v lbls bds
         | _ -> Warn.fatal
             "illegal argument for the indirect branch instruction %s \
             (must be a label)" (AArch64.dump_instruction i)
@@ -2067,20 +2070,20 @@ module Make
            >>= fun () -> M.unitT (B.Jump (tgt2tgt ii l,[AArch64Base.linkreg,v_ret]))
 
         | I_BR r as i ->
-            read_reg_ord r ii >>= do_indirect_jump test [] i
+            read_reg_ord r ii >>= do_indirect_jump test [] i ii
 
         | I_BLR r as i ->
            let v_ret = V.intToV (ii.A.addr + 4) in
            write_reg AArch64Base.linkreg v_ret ii
            >>= fun () -> read_reg_ord r ii
-           >>= do_indirect_jump test [AArch64Base.linkreg,v_ret] i
+           >>= do_indirect_jump test [AArch64Base.linkreg,v_ret] i ii
 
         | I_RET ro as i ->
             let r = match ro with
             | None -> AArch64Base.linkreg
             | Some r -> r in
             read_reg_ord r ii
-            >>= do_indirect_jump test [] i
+            >>= do_indirect_jump test [] i ii
 
         | I_ERET ->
            let eret_to_addr = function

herd/tests/instructions/AArch64/AK001.litmus

@@ -0,0 +1,16 @@
+AArch64 AK001 (* LB+rel+br-ctrl *)
+{
+ins_t *y;
+0:X2=x; 0:X4=y; 0:X3=P1:L0;
+1:X2=x; 1:X4=y;
+}
+P0           |P1           ;
+LDR W1,[X2]  | ADR X5,L1   ;
+STLR X3,[X4] | STR X5,[X4] ;
+             | LDR X3,[X4] ;
+             | BR X3       ;
+             |L0:          ;
+             | MOV W0,#1   ;
+             | STR W0,[X2] ;
+             |L1:          ;
+exists (0:X1=1 /\ 1:X0=1)

herd/tests/instructions/AArch64/AK001.litmus.expected

@@ -0,0 +1,11 @@
+Test AK001 Allowed
+States 2
+0:X1=0; 1:X0=0;
+0:X1=0; 1:X0=1;
+No
+Witnesses
+Positive: 0 Negative: 3
+Condition exists (0:X1=1 /\ 1:X0=1)
+Observation AK001 Never 0 3
+Hash=7967e5120b4f97d2a96964ef4e3b026a
+

herd/tests/instructions/AArch64/AK002.litmus

@@ -0,0 +1,17 @@
+AArch64 AK002 (* MP+rel+br-ctrlisb-1 *)
+{
+ins_t *y;
+0:X2=x; 0:X4=y; 0:X3=P1:L0;
+1:X2=x; 1:X4=y;
+}
+P0           | P1          ;
+MOV W1,#1    | ADR X5,L1   ;
+STR W1,[X2]  | STR X5,[X4] ;
+STLR X3,[X4] | LDR X3,[X4] ;
+             | BR  X3      ;
+             |L0:          ; 
+             | ISB         ;
+             | MOV W0,#1   ;
+             | LDR W1,[X2] ;
+             |L1:          ;
+exists (1:X0=1 /\ 1:X1=0)

herd/tests/instructions/AArch64/AK002.litmus.expected

@@ -0,0 +1,11 @@
+Test AK002 Allowed
+States 2
+1:X0=0; 1:X1=0;
+1:X0=1; 1:X1=1;
+No
+Witnesses
+Positive: 0 Negative: 3
+Condition exists (1:X0=1 /\ 1:X1=0)
+Observation AK002 Never 0 3
+Hash=c4340862f7579b543222fa925b3531ea
+

herd/tests/instructions/AArch64/AK003.litmus

@@ -0,0 +1,17 @@
+AArch64 AK003 (* MP+rel+br-ctrlisb-2 *)
+{
+ins_t *y;
+0:X2=x; 0:X4=y; 0:X3=P1:L0;
+1:X2=x; 1:X4=y;
+}
+P0           | P1          ;
+MOV W1,#1    | ADR X5,L1   ;
+STR W1,[X2]  | STR X5,[X4] ;
+STLR X3,[X4] | LDR X3,[X4] ;
+             | BR  X3      ;
+             |L0:          ;
+             | ISB         ;
+             | MOV W0,#1   ;
+             |L1:          ;
+             | LDR W1,[X2] ;
+exists (1:X0=1 /\ 1:X1=0)

herd/tests/instructions/AArch64/AK003.litmus.expected

@@ -0,0 +1,12 @@
+Test AK003 Allowed
+States 3
+1:X0=0; 1:X1=0;
+1:X0=0; 1:X1=1;
+1:X0=1; 1:X1=1;
+No
+Witnesses
+Positive: 0 Negative: 5
+Condition exists (1:X0=1 /\ 1:X1=0)
+Observation AK003 Never 0 5
+Hash=f1ea3d37edb778d976084e71b2bbafc9
+