christopher, kathy, peter: hacky experiment on nias_of_instruction

1 files changed, 41 insertions, 5 deletions

diff --git a/src/lem_interp/interp_inter_imp.lem b/src/lem_interp/interp_inter_imp.lem
index 75e695eb..19ba56b6 100644
--- a/src/lem_interp/interp_inter_imp.lem
+++ b/src/lem_interp/interp_inter_imp.lem
@@ -1120,17 +1120,17 @@ let nias_of_instruction
   match (thread_ism, instruction_name) with
     | ("PPCGEN_ism", "B") ->
        let () = ensure (not unknown_nia_address)
-                       "unexpected unknown/undefined address in nia_values" in
+                       "unexpected unknown/undefined address in nia_values 1" in
        nias
     | ("PPCGEN_ism", "Bc") ->
        let () = ensure (not unknown_nia_address)
-                       "unexpected unknown/undefined address in nia_values" in
+                       "unexpected unknown/undefined address in nia_values 2" in
        NIA_successor :: nias
     | ("PPCGEN_ism", "Bclr") -> [ NIA_successor; NIA_LR ]
     | ("PPCGEN_ism", "Bcctr") -> [ NIA_successor; NIA_CTR ]
     | ("PPCGEN_ism", "Sc") ->
        let () = ensure (not unknown_nia_address)
-                       "unexpected unknown/undefined address in nia_values" in
+                       "unexpected unknown/undefined address in nia_values 3" in
        match instruction_fields with
        | [(_, _, lev)] ->
           (* LEV field is 7 bits long, pad it with false at beginning *)
@@ -1175,13 +1175,49 @@ let nias_of_instruction
                             | _ -> false
                             end]
 
+
+    (** hacky cut-and-paste for AArch64Gen, duplicating code just to see if this suffices *)
+
+    | ("AArch64GenSail", "BranchImmediate")   -> nias
+    | ("AArch64GenSail", "BranchConditional") -> NIA_successor :: nias
+    | ("AArch64GenSail", "CompareAndBranch")  -> NIA_successor :: nias
+    | ("AArch64GenSail", "TestBitAndBranch")  -> NIA_successor :: nias
+
+    (* AArch64 calculated address branch *)
+    | ("AArch64GenSail", "branch_unconditional_register") ->
+        (* do some parsing of the ast fields to figure out which register holds
+           the branching address i.e. find n in "BR <Xn>". The ast constructor
+           from armV8.sail: (reg_index,BranchType) BranchRegister; *)
+        let n_integer =
+          match instruction_fields with
+          | [(_, _, n); _] -> integer_of_bit_list n
+          | _ -> fail
+          end
+        in
+        let () = ensure (0 <= n_integer && n_integer <= 31)
+                  "expected register number from 0 to 31"
+        in
+        if n_integer = 31 then
+          nias (* BR XZR *)
+        else
+          (* look for Xn (which we actually call Rn) in regs_in *)
+          let n_reg = "R" ^ (String_extra.stringFromInteger n_integer) in
+          [NIA_register r | forall (r MEM regs_in)
+                          | match r with
+                            | (Reg name _ _ _) -> name = n_reg
+                            | _ -> false
+                            end]
+
+    (** end of hacky *)
+
     | ("AArch64LitmusSail", "CtrlDep") -> NIA_successor :: nias
 
+
     | ("MIPS_ism", "B") -> fail
 
-    | _ ->
+    | (s1,s2) ->
        let () = ensure (not unknown_nia_address)
-                       "unexpected unknown/undefined address in nia_values" in
+                       ("unexpected unknown/undefined address in nia_values 4 (\""^s1^"\", \""^s2^"\")") in
         [ NIA_successor ]
     end