added transactional memory support

4 files changed, 126 insertions, 110 deletions

diff --git a/etc/regfp.sail b/etc/regfp.sail
index 3c90c269..fb15310a 100644
--- a/etc/regfp.sail
+++ b/etc/regfp.sail
@@ -64,10 +64,15 @@ typedef barrier_kind = enumerate {
   Barrier_MIPS_SYNC;
 }
 
+typedef trans_kind = enumerate {
+  Transaction_start; Transaction_commit; Transaction_abort;
+}
+
 typedef instruction_kind = const union {
   (barrier_kind) IK_barrier;
   (read_kind) IK_mem_read;
   (write_kind) IK_mem_write;
   IK_cond_branch;
+  (trans_kind) IK_trans;
   IK_simple
 }
diff --git a/src/lem_interp/interp_inter_imp.lem b/src/lem_interp/interp_inter_imp.lem
index 63dd0d76..72bf0bcc 100644
--- a/src/lem_interp/interp_inter_imp.lem
+++ b/src/lem_interp/interp_inter_imp.lem
@@ -171,8 +171,8 @@ let intern_ifield_value direction v =
 let extern_slice (d:direction) (start:nat) ((i,j):(nat*nat)) =
   match d with
     | D_increasing -> (i,j) (*This is the case the thread/concurrecny model expects, so no change needed*)
-    | D_decreasing -> 
-      let slice_i = start - i in 
+    | D_decreasing ->
+      let slice_i = start - i in
       let slice_j = (i - j) + slice_i in
       (slice_i,slice_j)
    end 
@@ -211,7 +211,7 @@ let rec extern_reg_value reg_name v =
       extern_reg_value reg_name (Interp_lib.fill_in_sparse v)
     | _ ->
       let (internal_start, external_start, direction) =
-        (match reg_name with 
+        (match reg_name with
           | Reg _ start size dir ->
             (start, (if dir = D_increasing then start else (start - (size +1))), dir)
           | Reg_slice _ reg_start dir (slice_start, slice_end) ->
@@ -1070,6 +1070,11 @@ let rr_interp_exhaustive mode i_state events =
 
 
 let instruction_kind_of_event : event -> maybe instruction_kind = function
+  (* this is a hack to avoid adding special events for AArch64 transactional-memory *)
+  | E_read_reg (Reg "TMStartEffect" 63 64 D_decreasing) -> Just (IK_trans Transaction_start)
+  | E_write_reg (Reg "TMAbortEffect" 63 64 D_decreasing) _ -> Just (IK_trans Transaction_abort)
+  | E_barrier Barrier_TM_COMMIT -> Just (IK_trans Transaction_commit)
+
   | E_read_mem rk _ _ _ -> Just (IK_mem_read rk)
   | E_write_mem wk _ _ _ _ _  -> Just (IK_mem_write wk)
   | E_write_ea wk _ _ _ -> Just (IK_mem_write wk)
@@ -1290,11 +1295,20 @@ let interp_instruction_analysis
       match List.mapMaybe instruction_kind_of_event es with
       | [] -> if List.length nias > 1 then IK_cond_branch else IK_simple
       | inst_kind :: inst_kinds ->
-          let () = ensure (forall (inst_kind' MEM inst_kinds). inst_kind' = inst_kind)
-                          "multiple instruction kinds" in
           let () = ensure (List.length nias > 1 --> inst_kind = IK_cond_branch)
-                          "multiple NIAs must be IK_cond_branch" in
-          inst_kind
+                      "multiple NIAs must be IK_cond_branch" in
+
+          if forall (inst_kind' MEM inst_kinds). inst_kind' = inst_kind then
+            inst_kind
+          (* the TSTART instruction can also be aborted so it will have two kinds of events *)
+          else if (exists (inst_kind' MEM (inst_kind :: inst_kinds)).
+                        inst_kind' = IK_trans Transaction_start) &&
+                  (forall (inst_kind' MEM (inst_kind :: inst_kinds)).
+                        inst_kind' = IK_trans Transaction_start
+                        || inst_kind' = IK_trans Transaction_abort)
+          then
+            IK_trans Transaction_start
+          else failwith "multiple instruction kinds"
     end in
 
   (regs_in, regs_out, regs_feeding_address, nias, dia, inst_kind)
diff --git a/src/lem_interp/sail_impl_base.lem b/src/lem_interp/sail_impl_base.lem
index 9ee0d011..616c0b0d 100644
--- a/src/lem_interp/sail_impl_base.lem
+++ b/src/lem_interp/sail_impl_base.lem
@@ -271,6 +271,10 @@ instance (Ord direction)
   let (>=) = directionGreaterEq
 end
 
+instance (Show direction)
+  let show = function D_increasing -> "D_increasing" | D_decreasing  -> "D_decreasing" end
+end
+
 let ~{ocaml} register_valueCompare rv1 rv2 =
   compare (rv1.rv_bits, rv1.rv_dir, rv1.rv_start, rv1.rv_start_internal)
           (rv2.rv_bits, rv2.rv_dir, rv2.rv_start, rv2.rv_start_internal)
@@ -349,6 +353,19 @@ let slice_of_reg_name : reg_name -> slice = function
   | Reg_f_slice _ _ _ _ _ sl       -> sl
   end
 
+let width_of_reg_name (r: reg_name) : nat =
+  let width_of_slice (i, j) = (* j - i + 1 in *)
+
+    (integerFromNat j) - (integerFromNat i) + 1
+    $> abs $> natFromInteger
+  in
+  match r with
+  | Reg _ _ width _          -> width
+  | Reg_slice _ _ _ sl       -> width_of_slice sl
+  | Reg_field _ _ _ _ sl     -> width_of_slice sl
+  | Reg_f_slice _ _ _ _ _ sl -> width_of_slice sl
+  end
+
 let reg_name_non_empty_intersection (r: reg_name) (r': reg_name) : bool = 
   register_base_name r = register_base_name r' &&
   let (i1,  i2)  = slice_of_reg_name r in
@@ -450,7 +467,8 @@ type barrier_kind =
   Barrier_Sync | Barrier_LwSync | Barrier_Eieio | Barrier_Isync
   (* AArch64 barriers *)
   | Barrier_DMB | Barrier_DMB_ST | Barrier_DMB_LD | Barrier_DSB
-  | Barrier_DSB_ST | Barrier_DSB_LD | Barrier_ISB 
+  | Barrier_DSB_ST | Barrier_DSB_LD | Barrier_ISB
+  | Barrier_TM_COMMIT
   (* MIPS barriers *)
   | Barrier_MIPS_SYNC
 
@@ -467,10 +485,23 @@ instance (Show barrier_kind)
     | Barrier_DSB_ST -> "Barrier_DSB_ST"
     | Barrier_DSB_LD -> "Barrier_DSB_LD"
     | Barrier_ISB -> "Barrier_ISB"
+    | Barrier_TM_COMMIT -> "Barrier_TM_COMMIT"
     | Barrier_MIPS_SYNC -> "Barrier_MIPS_SYNC"
   end
 end
 
+type trans_kind =
+  (* AArch64 *)
+  | Transaction_start | Transaction_commit | Transaction_abort
+
+instance (Show trans_kind)
+  let show = function
+  | Transaction_start  -> "Transaction_start"
+  | Transaction_commit -> "Transaction_commit"
+  | Transaction_abort  -> "Transaction_abort"
+  end
+end
+
 type instruction_kind = 
   | IK_barrier of barrier_kind 
   | IK_mem_read of read_kind 
@@ -480,6 +511,7 @@ 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_trans of trans_kind
   | IK_simple
 
 
@@ -489,6 +521,7 @@ instance (Show instruction_kind)
     | IK_mem_read read_kind -> "IK_mem_read " ^ (show read_kind)
     | IK_mem_write write_kind -> "IK_mem_write " ^ (show write_kind)
     | IK_cond_branch -> "IK_cond_branch"
+    | IK_trans trans_kind -> "IK_trans " ^ (show trans_kind)
     | IK_simple -> "IK_simple"
   end
 end
@@ -669,107 +702,58 @@ end
 
 let ~{ocaml} barrier_kindCompare bk1 bk2 =
   match (bk1, bk2) with
-  | (Barrier_Sync, Barrier_Sync)   -> EQ
+  | (Barrier_Sync, Barrier_Sync) -> EQ
   | (Barrier_Sync, _) -> LT
+  | (_, Barrier_Sync) -> GT
 
-  | (Barrier_LwSync, Barrier_Sync)   -> GT
   | (Barrier_LwSync, Barrier_LwSync) -> EQ
-  | (Barrier_LwSync, _)  -> LT
-
-  | (Barrier_Eieio, Barrier_Sync)   -> GT
-  | (Barrier_Eieio, Barrier_LwSync) -> GT
-  | (Barrier_Eieio, Barrier_Eieio)  -> EQ
-  | (Barrier_Eieio, _)  -> LT
-
-  | (Barrier_Isync, Barrier_Sync)   -> GT
-  | (Barrier_Isync, Barrier_LwSync) -> GT
-  | (Barrier_Isync, Barrier_Eieio)  -> GT
-  | (Barrier_Isync, Barrier_Isync)  -> EQ
-  | (Barrier_Isync, _)    -> LT
-
-  | (Barrier_DMB, Barrier_Sync)   -> GT
-  | (Barrier_DMB, Barrier_LwSync) -> GT
-  | (Barrier_DMB, Barrier_Eieio)  -> GT
-  | (Barrier_DMB, Barrier_Isync)  -> GT
-  | (Barrier_DMB, Barrier_DMB)    -> EQ
-  | (Barrier_DMB, Barrier_DMB_ST) -> LT
+  | (Barrier_LwSync, _) -> LT
+  | (_, Barrier_LwSync) -> GT
+
+  | (Barrier_Eieio, Barrier_Eieio) -> EQ
+  | (Barrier_Eieio, _) -> LT
+  | (_, Barrier_Eieio) -> GT
+
+  | (Barrier_Isync, Barrier_Isync) -> EQ
+  | (Barrier_Isync, _) -> LT
+  | (_, Barrier_Isync) -> GT
+
+  | (Barrier_DMB, Barrier_DMB) -> EQ
   | (Barrier_DMB, _) -> LT
+  | (_, Barrier_DMB) -> GT
 
-  | (Barrier_DMB_ST, Barrier_Sync)   -> GT
-  | (Barrier_DMB_ST, Barrier_LwSync) -> GT
-  | (Barrier_DMB_ST, Barrier_Eieio)  -> GT
-  | (Barrier_DMB_ST, Barrier_Isync)  -> GT
-  | (Barrier_DMB_ST, Barrier_DMB)    -> GT
   | (Barrier_DMB_ST, Barrier_DMB_ST) -> EQ
   | (Barrier_DMB_ST, _) -> LT
+  | (_, Barrier_DMB_ST) -> GT
 
-  | (Barrier_DMB_LD, Barrier_Sync)   -> GT
-  | (Barrier_DMB_LD, Barrier_LwSync) -> GT
-  | (Barrier_DMB_LD, Barrier_Eieio)  -> GT
-  | (Barrier_DMB_LD, Barrier_Isync)  -> GT
-  | (Barrier_DMB_LD, Barrier_DMB)    -> GT
-  | (Barrier_DMB_LD, Barrier_DMB_ST) -> GT
   | (Barrier_DMB_LD, Barrier_DMB_LD) -> EQ
-  | (Barrier_DMB_LD, _)    -> LT
-
-  | (Barrier_DSB, Barrier_Sync)   -> GT
-  | (Barrier_DSB, Barrier_LwSync) -> GT
-  | (Barrier_DSB, Barrier_Eieio)  -> GT
-  | (Barrier_DSB, Barrier_Isync)  -> GT
-  | (Barrier_DSB, Barrier_DMB)    -> GT
-  | (Barrier_DSB, Barrier_DMB_ST) -> GT
-  | (Barrier_DSB, Barrier_DMB_LD) -> GT
-  | (Barrier_DSB, Barrier_DSB)    -> EQ
+  | (Barrier_DMB_LD, _) -> LT
+  | (_, Barrier_DMB_LD) -> GT
+
+  | (Barrier_DSB, Barrier_DSB) -> EQ
   | (Barrier_DSB, _) -> LT
+  | (_, Barrier_DSB) -> GT
 
-  | (Barrier_DSB_ST, Barrier_Sync)   -> GT
-  | (Barrier_DSB_ST, Barrier_LwSync) -> GT
-  | (Barrier_DSB_ST, Barrier_Eieio)  -> GT
-  | (Barrier_DSB_ST, Barrier_Isync)  -> GT
-  | (Barrier_DSB_ST, Barrier_DMB)    -> GT
-  | (Barrier_DSB_ST, Barrier_DMB_ST) -> GT
-  | (Barrier_DSB_ST, Barrier_DMB_LD) -> GT
-  | (Barrier_DSB_ST, Barrier_DSB)    -> GT
   | (Barrier_DSB_ST, Barrier_DSB_ST) -> EQ
   | (Barrier_DSB_ST, _) -> LT
+  | (_, Barrier_DSB_ST) -> GT
 
-  | (Barrier_DSB_LD, Barrier_Sync)   -> GT
-  | (Barrier_DSB_LD, Barrier_LwSync) -> GT
-  | (Barrier_DSB_LD, Barrier_Eieio)  -> GT
-  | (Barrier_DSB_LD, Barrier_Isync)  -> GT
-  | (Barrier_DSB_LD, Barrier_DMB)    -> GT
-  | (Barrier_DSB_LD, Barrier_DMB_ST) -> GT
-  | (Barrier_DSB_LD, Barrier_DMB_LD) -> GT
-  | (Barrier_DSB_LD, Barrier_DSB)    -> GT
-  | (Barrier_DSB_LD, Barrier_DSB_ST) -> GT
   | (Barrier_DSB_LD, Barrier_DSB_LD) -> EQ
-  | (Barrier_DSB_LD, _)    -> LT
+  | (Barrier_DSB_LD, _) -> LT
+  | (_, Barrier_DSB_LD) -> GT
                           
-  | (Barrier_ISB, Barrier_Sync)   -> GT
-  | (Barrier_ISB, Barrier_LwSync) -> GT
-  | (Barrier_ISB, Barrier_Eieio)  -> GT
-  | (Barrier_ISB, Barrier_Isync)  -> GT
-  | (Barrier_ISB, Barrier_DMB)    -> GT
-  | (Barrier_ISB, Barrier_DMB_ST) -> GT
-  | (Barrier_ISB, Barrier_DMB_LD) -> GT
-  | (Barrier_ISB, Barrier_DSB)    -> GT
-  | (Barrier_ISB, Barrier_DSB_ST) -> GT
-  | (Barrier_ISB, Barrier_DSB_LD) -> GT
-  | (Barrier_ISB, Barrier_ISB)    -> EQ
-  | (Barrier_ISB, Barrier_MIPS_SYNC) -> LT
-
-  | (Barrier_MIPS_SYNC, Barrier_Sync)   -> GT
-  | (Barrier_MIPS_SYNC, Barrier_LwSync) -> GT
-  | (Barrier_MIPS_SYNC, Barrier_Eieio)  -> GT
-  | (Barrier_MIPS_SYNC, Barrier_Isync)  -> GT
-  | (Barrier_MIPS_SYNC, Barrier_DMB)    -> GT
-  | (Barrier_MIPS_SYNC, Barrier_DMB_ST) -> GT
-  | (Barrier_MIPS_SYNC, Barrier_DMB_LD) -> GT
-  | (Barrier_MIPS_SYNC, Barrier_DSB)    -> GT
-  | (Barrier_MIPS_SYNC, Barrier_DSB_ST) -> GT
-  | (Barrier_MIPS_SYNC, Barrier_DSB_LD) -> GT
-  | (Barrier_MIPS_SYNC, Barrier_ISB)    -> GT
+  | (Barrier_ISB, Barrier_ISB) -> EQ
+  | (Barrier_ISB, _) -> LT
+  | (_, Barrier_ISB) -> GT
+
+  | (Barrier_TM_COMMIT, Barrier_TM_COMMIT) -> EQ
+  | (Barrier_TM_COMMIT, _) -> LT
+  | (_, Barrier_TM_COMMIT) -> GT
+
   | (Barrier_MIPS_SYNC, Barrier_MIPS_SYNC) -> EQ
+  (* | (Barrier_MIPS_SYNC, _) -> LT
+  | (_, Barrier_MIPS_SYNC) -> GT *)
+
   end
 let inline {ocaml} barrier_kindCompare = defaultCompare
 
@@ -1167,6 +1151,10 @@ let register_value_of_integer (len:nat) (start:nat) (dir:direction) (i:integer):
   let bs = bit_list_of_integer len i in
   build_register_value (List.map bit_lifted_of_bit bs) dir len start
 
+val register_value_for_reg_of_integer : reg_name -> integer -> register_value
+let register_value_for_reg_of_integer (r: reg_name) (i:integer) : register_value =
+  register_value_of_integer (width_of_reg_name r) (start_of_reg_name r) (direction_of_reg_name r) i
+
 (* *)
 
 val opcode_of_bytes : byte -> byte -> byte -> byte -> opcode
@@ -1276,25 +1264,29 @@ let byte_list_of_opcode (Opcode bs) : list byte = bs
 
 (* matching printing_functions.ml *)
 val stringFromReg_name : reg_name -> string
-let stringFromReg_name r = match r with
-| Reg s start size dir -> s
-| Reg_slice s start dir (first,second) ->
-    let (first,second) = 
-      match dir with
-      | D_increasing -> (first,second) 
-      | D_decreasing -> (start - first, start - second)
-      end in
-    s ^ "[" ^ show first ^ (if (first = second) then "" else ".." ^ (show second)) ^ "]"
-| Reg_field s size dir f (first, second) ->
-    s ^ "." ^ f
-| Reg_f_slice s start dir f (first1,second1) (first,second) ->
-    let (first,second) = 
-      match dir with
-      | D_increasing -> (first,second) 
+let stringFromReg_name r =
+  let norm_sl start dir (first,second) = (first,second)
+    (* match dir with
+      | D_increasing -> (first,second)
       | D_decreasing -> (start - first, start - second)
-      end in
-    s ^ "." ^ f ^ "]" ^ show first ^ (if (first = second) then "" else ".." ^ (show second)) ^ "]"
-end
+    end *)
+  in
+  match r with
+  | Reg s start size dir -> s
+  | Reg_slice s start dir sl ->
+      let (first,second) = norm_sl start dir sl in
+      s ^ "[" ^ show first ^ (if (first = second) then "" else ".." ^ (show second)) ^ "]"
+  | Reg_field s start dir f sl ->
+      let (first,second) = norm_sl start dir sl in
+      s ^ "." ^ f ^ " (" ^ (show start) ^ ", " ^ (show dir) ^ ", " ^ (show first) ^ ", " ^ (show second) ^ ")"
+  | Reg_f_slice s start dir f (first1,second1) (first,second) ->
+      let (first,second) =
+        match dir with
+        | D_increasing -> (first,second)
+        | D_decreasing -> (start - first, start - second)
+        end in
+      s ^ "." ^ f ^ "]" ^ show first ^ (if (first = second) then "" else ".." ^ (show second)) ^ "]"
+  end
 
 instance (Show reg_name)
   let show = stringFromReg_name
diff --git a/src/pretty_print_lem.ml b/src/pretty_print_lem.ml
index 969bc5ba..b55685f4 100644
--- a/src/pretty_print_lem.ml
+++ b/src/pretty_print_lem.ml
@@ -821,6 +821,7 @@ let doc_typdef_lem regtypes (TD_aux(td,_)) = match td with
       | Id_aux ((Id "read_kind"),_) -> empty
       | Id_aux ((Id "write_kind"),_) -> empty
       | Id_aux ((Id "barrier_kind"),_) -> empty
+      | Id_aux ((Id "trans_kind"),_) -> empty
       | Id_aux ((Id "instruction_kind"),_) -> empty
       | Id_aux ((Id "regfp"),_) -> empty
       | Id_aux ((Id "niafp"),_) -> empty
@@ -909,7 +910,11 @@ let doc_typdef_lem regtypes (TD_aux(td,_)) = match td with
       | Id_aux ((Id "read_kind"),_) -> empty
       | Id_aux ((Id "write_kind"),_) -> empty
       | Id_aux ((Id "barrier_kind"),_) -> empty
+      | Id_aux ((Id "trans_kind"),_) -> empty
       | Id_aux ((Id "instruction_kind"),_) -> empty
+      | Id_aux ((Id "regfp"),_) -> empty
+      | Id_aux ((Id "niafp"),_) -> empty
+      | Id_aux ((Id "diafp"),_) -> empty
       | _ ->
          let rec range i j = if i > j then [] else i :: (range (i+1) j) in
          let nats = range 0 in