update instruction_analysis to support nias and instruction kind

2 files changed, 74 insertions, 11 deletions

diff --git a/src/lem_interp/interp_inter_imp.lem b/src/lem_interp/interp_inter_imp.lem
index 49d8cbfe..f36732fe 100644
--- a/src/lem_interp/interp_inter_imp.lem
+++ b/src/lem_interp/interp_inter_imp.lem
@@ -470,9 +470,13 @@ let instruction_analysis top_level end_flag thunk_name regn_to_reg_details regis
             (Interp_ast.Unknown, Nothing)) 
          top_env Interp.eenv (Interp.emem "instruction analysis top level") Interp.Top) Nothing) in
   match (analysis_or_error) with
-  | Ivh_value regs ->
-    (match regs with
-     | Interp.V_tuple [Interp.V_list regs1; Interp.V_list regs2; Interp.V_list regs3] ->
+  | Ivh_value analysis ->
+    (match analysis with
+     | Interp.V_tuple [Interp.V_list regs1;
+                       Interp.V_list regs2;
+                       Interp.V_list regs3;
+                       Interp.V_list nias;
+                       ik] ->
        let reg_to_reg_name v = match v with
          | Interp.V_ctor (Id_aux (Id "RFull") _) _ _ (Interp.V_lit (L_aux (L_string n) _)) ->
            let (start,length,direction,_) = regn_to_reg_details n Nothing in
@@ -494,14 +498,62 @@ let instruction_analysis top_level end_flag thunk_name regn_to_reg_details regis
                               Interp.V_lit (L_aux (L_string f) _);]) ->
            let (start,length,direction,span) = regn_to_reg_details n (Just f) in
            Reg_field n start direction f span             
-         | _ -> Assert_extra.failwith "Analysis did not return an element of the specified type" end
+         | _ -> Assert_extra.failwith "Register footprint analysis did not return an element of the specified type" end
        in
-       let (regs1,regs2,regs3) =
-         (List.map reg_to_reg_name regs1, List.map reg_to_reg_name regs2, List.map reg_to_reg_name regs3) in
-       (Just (regs1,regs2,regs3), events)
-     | _ -> Assert_extra.failwith "Analysis did not return a three-tuple of lists" end)
-  | Ivh_value_after_exn _ ->
-    (Nothing, events)
+       let get_nia v = address_of_memory_value end_flag (fst (extern_mem_value mode v)) in
+       let ik_to_ik = function
+         | Interp.V_ctor (Id_aux (Id "IK_barrier") _) _ _
+           (Interp.V_ctor (Id_aux (Id b) _) _ _ _) ->
+            IK_barrier (match b with
+                        | "Barrier_Sync" ->   Sync
+                        | "Barrier_Lwsync" -> LwSync
+                        | "Barrier_Eieio" ->  Eieio
+                        | "Barrier_Isync" ->  Isync
+                        | "Barrier_DMB" ->    DMB
+                        | "Barrier_DMB_ST" -> DMB_ST
+                        | "Barrier_DMB_LD" -> DMB_LD
+                        | "Barrier_DSB" ->    DSB
+                        | "Barrier_DSB_ST" -> DSB_ST
+                        | "Barrier_DSB_LD" -> DSB_LD
+                        | "Barrier_ISB" ->    ISB
+                        | "Barrier_Sync" ->   Sync
+                        end)
+         | Interp.V_ctor (Id_aux (Id "IK_mem_read") _) _ _
+           (Interp.V_ctor (Id_aux (Id r) _) _ _ _) ->
+            IK_mem_read (match r with
+                         | "Read_plain" ->             Read_plain
+                         | "Read_tag"   ->             Read_tag
+                         | "Read_reserve" ->           Read_reserve
+                         | "Read_acquire" ->           Read_acquire
+                         | "Read_exclusive" ->         Read_exclusive
+                         | "Read_exclusive_acquire" -> Read_exclusive_acquire
+                         | "Read_stream" ->            Read_stream
+                         end)
+         | Interp.V_ctor (Id_aux (Id "IK_mem_write") _) _ _
+           (Interp.V_ctor (Id_aux (Id w) _) _ _ _) ->
+            IK_mem_write (match w with
+                         | "Write_plain" ->             Write_plain
+                         | "Write_tag"   ->             Write_tag
+                         | "Write_conditional" ->       Write_conditional
+                         | "Write_release" ->           Write_release
+                         | "Write_exclusive" ->         Write_exclusive
+                         | "Write_exclusive_release" -> Write_exclusive_release
+                          end)
+         | Interp.V_ctor (Id_aux (Id "IK_cond_branch") _) _ _ _ ->
+            IK_cond_branch
+         | Interp.V_ctor (Id_aux (Id "IK_simple") _) _ _ _ ->
+            IK_simple
+         | _ -> failwith "Analysis returned unexpected instruction kind"
+       end in
+       let (regs1,regs2,regs3,nias,ik) =
+         (List.map reg_to_reg_name regs1,
+          List.map reg_to_reg_name regs2,
+          List.map reg_to_reg_name regs3,
+          List.map get_nia nias,
+          ik_to_ik ik) in
+       ((regs1,regs2,regs3,nias,ik), events)
+     | _ -> Assert_extra.failwith "Analysis did not return a four-tuple of lists" end)
+  | Ivh_value_after_exn _ -> Assert_extra.failwith "Instruction analysis failed"
   | Ivh_error err -> match err with
      | Internal_error msg -> Assert_extra.failwith msg
      | _ -> Assert_extra.failwith "Not an internal error either" end 
diff --git a/src/lem_interp/interp_interface.lem b/src/lem_interp/interp_interface.lem
index 2da9e060..5473e1a0 100644
--- a/src/lem_interp/interp_interface.lem
+++ b/src/lem_interp/interp_interface.lem
@@ -416,6 +416,17 @@ type barrier_kind =
   (* AArch64 barriers *)
   | DMB | DMB_ST | DMB_LD | DSB | DSB_ST | DSB_LD | ISB 
 
+type instruction_kind = 
+  | IK_barrier of barrier_kind 
+  | IK_mem_read of read_kind 
+  | IK_mem_write of write_kind
+(* SS reinstating cond_branches
+at present branches are not distinguished in the instruction_kind;
+they just have particular nias (and will be IK_simple *)
+  | IK_cond_branch 
+(*  | IK_uncond_branch *)
+  | IK_simple
+
 (*Map between external functions as preceived from a Sail spec and the actual implementation of the function *)
 type external_functions = list (string * (Interp.value -> Interp.value))
 
@@ -1156,7 +1167,7 @@ val translate_address :
 
 val instruction_analysis :
   context -> end_flag -> string -> (string -> (nat * nat * direction * (nat * nat)))
-  -> maybe (list (reg_name * register_value)) -> instruction -> (list reg_name * list reg_name * list reg_name)
+  -> maybe (list (reg_name * register_value)) -> instruction -> (list reg_name * list reg_name * list reg_name * list address)
 
 val byte_list_of_memory_value : end_flag -> memory_value -> maybe (list byte)
 let byte_list_of_memory_value endian mv =