factor out regfp analysis types into etc/regfp.sail

8 files changed, 143 insertions, 107 deletions

diff --git a/etc/regfp.sail b/etc/regfp.sail
new file mode 100644
index 00000000..dcd38f76
--- /dev/null
+++ b/etc/regfp.sail
@@ -0,0 +1,72 @@
+(* iR : input registers,
+ * oR : output registers,
+ * aR : registers feeding into the memory address *)
+
+(* branch instructions currently are not writing to NIA *)
+
+typedef regfp = const union {
+   (string) RFull;
+   (string,nat,nat) RSlice;
+   (string,nat) RSliceBit;
+   (string,string) RField;
+}
+
+typedef regfps = list <regfp>
+
+typedef niafp = const union {
+  NIAFP_successor;
+  (bit[64]) NIAFP_concrete_address;
+  NIAFP_LR;
+  NIAFP_CTR;
+  (regfp) NIAFP_register;
+}
+
+typedef niafps = list <niafp>
+
+(* only for MIPS *)
+typedef diafp = const union {
+  DIAFP_none;
+  (bit[64]) DIAFP_concrete;
+  (regfp) DIAFP_reg;
+}
+
+typedef read_kind = enumerate {
+  Read_plain;
+  Read_tag;
+  Read_reserve;
+  Read_acquire;
+  Read_exclusive;
+  Read_exclusive_acquire;
+  Read_stream
+}
+
+typedef write_kind = enumerate {
+  Write_plain;
+  Write_tag;
+  Write_conditional;
+  Write_release;
+  Write_exclusive;
+  Write_exclusive_release;
+}
+
+typedef barrier_kind = enumerate {
+  Barrier_Sync;
+  Barrier_LwSync;
+  Barrier_Eieio;
+  Barrier_Isync;
+  Barrier_DMB;
+  Barrier_DMB_ST;
+  Barrier_DMB_LD;
+  Barrier_DSB;
+  Barrier_DSB_ST;
+  Barrier_DSB_LD;
+  Barrier_ISB;
+}
+
+typedef instruction_kind = const union {
+  (barrier_kind) IK_barrier;
+  (read_kind) IK_mem_read;
+  (write_kind) IK_mem_write;
+  IK_cond_branch;
+  IK_simple
+}
\ No newline at end of file
diff --git a/mips/mips_regfp.sail b/mips/mips_regfp.sail
index 714ad9fb..390aa82b 100644
--- a/mips/mips_regfp.sail
+++ b/mips/mips_regfp.sail
@@ -1,68 +1,3 @@
-(* iR : input registers,
- * oR : output registers,
- * aR : registers feeding into the memory address *)
-
-(* branch instructions currently are not writing to NIA *)
-
-typedef regfp = const union {
-   (string) RFull;
-   (string,nat,nat) RSlice;
-   (string,nat) RSliceBit;
-   (string,string) RField;
-}
-
-typedef regfps = list <regfp>
-
-typedef nia = bit[64]
-typedef nias = list <nia>
-
-typedef dia = const union {
-            DIA_none;
-  (bit[64]) DIA_concrete;
-  (regfp)   DIA_reg;
-}
-
-typedef read_kind = enumerate {
-  Read_plain;
-  Read_tag;
-  Read_reserve;
-  Read_acquire;
-  Read_exclusive;
-  Read_exclusive_acquire;
-  Read_stream
-}
-
-typedef write_kind = enumerate {
-  Write_plain;
-  Write_tag;
-  Write_conditional;
-  Write_release;
-  Write_exclusive;
-  Write_exclusive_release;
-}
-
-typedef barrier_kind = enumerate {
-  Barrier_Sync;
-  Barrier_LwSync;
-  Barrier_Eieio;
-  Barrier_Isync;
-  Barrier_DMB;
-  Barrier_DMB_ST;
-  Barrier_DMB_LD;
-  Barrier_DSB;
-  Barrier_DSB_ST;
-  Barrier_DSB_LD;
-  Barrier_ISB;
-}
-
-typedef instruction_kind = const union {
-  (barrier_kind) IK_barrier;
-  (read_kind) IK_mem_read;
-  (write_kind) IK_mem_write;
-  IK_cond_branch;
-  IK_simple
-}
-
 let (vector <0, 32, inc, string >) GPRs =
   [ "GPR00", "GPR01", "GPR02", "GPR03", "GPR04", "GPR05", "GPR06", "GPR07", "GPR08", "GPR09", "GPR10",
   "GPR11", "GPR12", "GPR13", "GPR14", "GPR15", "GPR16", "GPR17", "GPR18", "GPR19", "GPR20",
@@ -72,13 +7,13 @@ let (vector <0, 32, inc, string >) GPRs =
 let CIA_fp = RFull("CIA")
 let NIA_fp = RFull("NIA")
 
-function (regfps,regfps,regfps,nias,dia,instruction_kind) initial_analysis (instr) = {
+function (regfps,regfps,regfps,niafps,diafp,instruction_kind) initial_analysis (instr) = {
   iR := [|| ||];
   oR := [|| ||];
   aR := [|| ||];
   ik := IK_simple;
   Nias := [|| ||];
-  Dia := DIA_none;
+  Dia := DIAFP_none;
 
   switch instr {
     case (DADDIU (rs, rt, imm)) -> {
@@ -355,33 +290,33 @@ function (regfps,regfps,regfps,nias,dia,instruction_kind) initial_analysis (inst
     case (J(offset)) -> {
       (* XXX actually unconditional jump *)
       (*ik := IK_cond_branch;*)
-      Dia := DIA_concrete((PC + 4)[63..28] : offset : 0b00);
+      Dia := DIAFP_concrete((PC + 4)[63..28] : offset : 0b00);
     }
     case (JAL(offset)) -> {
       (* XXX actually unconditional jump *)
       (*ik := IK_cond_branch;*)
       oR := RFull("GPR31") :: oR;
-      Dia := DIA_concrete((PC + 4)[63..28] : offset : 0b00);
+      Dia := DIAFP_concrete((PC + 4)[63..28] : offset : 0b00);
     }
     case (JR(rs)) -> {
       (* XXX actually unconditional jump *)
       (*ik := IK_cond_branch;*)
       iR := RFull(GPRs[rs]) :: iR;
-      Dia := DIA_reg(RFull(GPRs[rs]));
+      Dia := DIAFP_reg(RFull(GPRs[rs]));
     }
     case (JALR(rs, rd)) -> {
       (* XXX actually unconditional jump *)
       (*ik := IK_cond_branch;*)
       iR := RFull(GPRs[rs]) :: iR;
       oR := RFull("GPR31") :: oR;
-      Dia := DIA_reg(RFull(GPRs[rs]));
+      Dia := DIAFP_reg(RFull(GPRs[rs]));
     }
     case (BEQ(rs, rd, imm, ne, likely)) -> {
       ik := IK_cond_branch;
       if rs == 0 then () else iR := RFull(GPRs[rs]) :: iR;
       if rd == 0 then () else iR := RFull(GPRs[rd]) :: iR;
       let (bit[64]) offset = (EXTS(imm : 0b00) + 4) in
-      Dia := DIA_concrete (PC + offset);
+      Dia := DIAFP_concrete (PC + offset);
     }
     case (BCMPZ(rs, imm, cmp, link, likely)) -> {
       ik := IK_cond_branch;
@@ -389,7 +324,7 @@ function (regfps,regfps,regfps,nias,dia,instruction_kind) initial_analysis (inst
       if link then
         oR := RFull("GPR31") :: oR;
       let (bit[64]) offset = (EXTS(imm : 0b00) + 4) in
-      Dia := DIA_concrete (PC + offset);
+      Dia := DIAFP_concrete (PC + offset);
     }
 (*
 
diff --git a/src/Makefile b/src/Makefile
index 5d501931..30ff9254 100644
--- a/src/Makefile
+++ b/src/Makefile
@@ -25,8 +25,8 @@ LEMLIBOCAML = $(BITBUCKET_ROOT)/lem/ocaml-lib
 ELFDIR= $(BITBUCKET_ROOT)/linksem
 
 MIPS_SAIL_DIR:=$(BITBUCKET_ROOT)/sail/mips
-MIPS_SAILS:=$(MIPS_SAIL_DIR)/mips_prelude.sail $(MIPS_SAIL_DIR)/mips_tlb.sail $(MIPS_SAIL_DIR)/mips_wrappers.sail $(MIPS_SAIL_DIR)/mips_insts.sail $(MIPS_SAIL_DIR)/mips_ri.sail $(MIPS_SAIL_DIR)/mips_epilogue.sail $(MIPS_SAIL_DIR)/mips_regfp.sail
-MIPS_NOTLB_SAILS:=$(MIPS_SAIL_DIR)/mips_prelude.sail $(MIPS_SAIL_DIR)/mips_tlb_stub.sail $(MIPS_SAIL_DIR)/mips_wrappers.sail $(MIPS_SAIL_DIR)/mips_insts.sail $(MIPS_SAIL_DIR)/mips_epilogue.sail $(MIPS_SAIL_DIR)/mips_regfp.sail
+MIPS_SAILS:=$(MIPS_SAIL_DIR)/mips_prelude.sail $(MIPS_SAIL_DIR)/mips_tlb.sail $(MIPS_SAIL_DIR)/mips_wrappers.sail $(MIPS_SAIL_DIR)/mips_insts.sail $(MIPS_SAIL_DIR)/mips_ri.sail $(MIPS_SAIL_DIR)/mips_epilogue.sail $(BITBUCKET_ROOT)/sail/etc/regfp.sail $(MIPS_SAIL_DIR)/mips_regfp.sail
+MIPS_NOTLB_SAILS:=$(MIPS_SAIL_DIR)/mips_prelude.sail $(MIPS_SAIL_DIR)/mips_tlb_stub.sail $(MIPS_SAIL_DIR)/mips_wrappers.sail $(MIPS_SAIL_DIR)/mips_insts.sail $(MIPS_SAIL_DIR)/mips_epilogue.sail $(BITBUCKET_ROOT)/sail/etc/regfp.sail $(MIPS_SAIL_DIR)/mips_regfp.sail
 CHERI_SAIL_DIR:=$(BITBUCKET_ROOT)/sail/cheri
 CHERI_SAILS:=$(MIPS_SAIL_DIR)/mips_prelude.sail $(MIPS_SAIL_DIR)/mips_tlb.sail $(CHERI_SAIL_DIR)/cheri_prelude.sail $(MIPS_SAIL_DIR)/mips_insts.sail $(CHERI_SAIL_DIR)/cheri_insts.sail $(MIPS_SAIL_DIR)/mips_ri.sail $(MIPS_SAIL_DIR)/mips_epilogue.sail
 
diff --git a/src/gen_lib/prompt.lem b/src/gen_lib/prompt.lem
index 18868b4a..6d895a87 100644
--- a/src/gen_lib/prompt.lem
+++ b/src/gen_lib/prompt.lem
@@ -66,9 +66,9 @@ let read_reg_aux reg =
 let read_reg reg =
   read_reg_aux (extern_reg_whole reg)
 let read_reg_range reg i j =
-  read_reg_aux (extern_reg_slice reg (i,j))
+  read_reg_aux (extern_reg_slice reg (natFromInteger i,natFromInteger j))
 let read_reg_bit reg i =
-  read_reg_aux (extern_reg_slice reg (i,i)) >>= fun v ->
+  read_reg_aux (extern_reg_slice reg (natFromInteger i,natFromInteger i)) >>= fun v ->
   return (extract_only_bit v)
 let read_reg_field reg regfield =
   read_reg_aux (extern_reg_field_whole reg regfield)
@@ -84,9 +84,10 @@ let write_reg_aux reg_name v =
 let write_reg reg v =
   write_reg_aux (extern_reg_whole reg) v
 let write_reg_range reg i j v =
-  write_reg_aux (extern_reg_slice reg (i,j)) v
+  write_reg_aux (extern_reg_slice reg (natFromInteger i,natFromInteger j)) v
 let write_reg_bit reg i bit =
-  write_reg_aux (extern_reg_slice reg (i,i)) (Vector [bit] i (is_inc_of_reg reg))
+  let iN = natFromInteger i in
+  write_reg_aux (extern_reg_slice reg (iN,iN)) (Vector [bit] i (is_inc_of_reg reg))
 let write_reg_field reg regfield v =
   write_reg_aux (extern_reg_field_whole reg regfield) v
 let write_reg_bitfield reg regfield bit =
diff --git a/src/gen_lib/sail_values.lem b/src/gen_lib/sail_values.lem
index 975c7a5e..399cc218 100644
--- a/src/gen_lib/sail_values.lem
+++ b/src/gen_lib/sail_values.lem
@@ -814,8 +814,7 @@ let intern_reg_value v =
          (v.rv_dir = D_increasing)
 
 
-let extern_slice (d:direction) (start:nat) ((i,j):(integer*integer)) =
-  let (i,j) = (natFromInteger i,natFromInteger j) in
+let extern_slice (d:direction) (start:nat) ((i,j):(nat*nat)) =
   match d with
   (*This is the case the thread/concurrecny model expects, so no change needed*)
   | D_increasing -> (i,j)
@@ -833,13 +832,13 @@ let extern_reg_slice reg (i,j) =
   Reg_slice (name_of_reg reg) start dir (extern_slice dir start (i,j))
 
 let extern_reg_field_whole reg rfield = 
-  let (m,n) = register_field_indices reg rfield in
+  let (m,n) = register_field_indices_nat reg rfield in
   let start = start_of_reg_nat reg in
   let dir = dir_of_reg reg in
   Reg_field (name_of_reg reg) start dir rfield (extern_slice dir start (m,n))
             
 let extern_reg_field_slice reg rfield (i,j) = 
-  let (m,n) = register_field_indices reg rfield in
+  let (m,n) = register_field_indices_nat reg rfield in
   let start = start_of_reg_nat reg in
   let dir = dir_of_reg reg in
   Reg_f_slice (name_of_reg reg) start dir rfield
@@ -1399,6 +1398,12 @@ instance (ToFromInterpValue instruction_kind)
 end
 
 
+type regfp =
+  | RFull of (string)
+  | RSlice of (string * integer * integer)
+  | RSliceBit of (string * integer)
+  | RField of (string * string)
+
 let regfpToInterpValue = function
   | RFull v -> SI.V_ctor (SIA.Id_aux (SIA.Id "RFull") SIA.Unknown) (SIA.T_id "regfp") SI.C_Union (toInterpValue v)
   | RSlice v -> SI.V_ctor (SIA.Id_aux (SIA.Id "RSlice") SIA.Unknown) (SIA.T_id "regfp") SI.C_Union (toInterpValue v)
@@ -1420,23 +1425,53 @@ instance (ToFromInterpValue regfp)
   let fromInterpValue = regfpFromInterpValue
 end
 
-(*
-let rfp_to_reg reg_info direction = function
+
+let regfp_to_reg (reg_info : string -> maybe string -> (nat * nat * direction * (nat * nat))) = function
   | RFull name -> 
      let (start,length,direction,_) = reg_info name Nothing in
      Reg name start length direction
   | RSlice (name,i,j) ->
+     let i = natFromInteger i in
+     let j = natFromInteger j in
      let (start,length,direction,_) = reg_info name Nothing in
-     let slice = extern_slice direction (natFromInteger start) (i,j) in
+     let slice = extern_slice direction start (i,j) in
      Reg_slice name start direction slice
   | RSliceBit (name,i) ->
+     let i = natFromInteger i in
      let (start,length,direction,_) = reg_info name Nothing in
-     let slice = extern_slice direction (natFromInteger start) (i,i) in
+     let slice = extern_slice direction start (i,i) in
      Reg_slice name start direction slice
   | RField (name,field_name) ->
      let (start,length,direction,span) = reg_info name (Just field_name) in
-     let start = natFromInteger start in
-     let slice = extern_slice direction start (start,span) in
+     let slice = extern_slice direction start span in
      Reg_field name start direction field_name slice
 end
- *)
+
+
+type niafp = 
+  | NIAFP_successor
+  | NIAFP_concrete_address of vector bitU
+  | NIAFP_LR
+  | NIAFP_CTR
+  | NIAFP_register of regfp
+
+(* only for MIPS *)
+type diafp = 
+  | DIAFP_none
+  | DIAFP_concrete of vector bitU
+  | DIAFP_reg of regfp
+
+let niafp_to_nia reginfo = function
+  | NIAFP_successor -> NIA_successor
+  | NIAFP_concrete_address v -> NIA_concrete_address (address_of_bitv v)
+  | NIAFP_LR -> NIA_LR
+  | NIAFP_CTR -> NIA_CTR
+  | NIAFP_register r -> NIA_register (regfp_to_reg reginfo r)
+end
+
+let diafp_to_dia reginfo = function
+  | DIAFP_none -> DIA_none
+  | DIAFP_concrete v -> DIA_concrete_address (address_of_bitv v)
+  | DIAFP_reg r -> DIA_register (regfp_to_reg reginfo r)
+end
+
diff --git a/src/lem_interp/interp_inter_imp.lem b/src/lem_interp/interp_inter_imp.lem
index cb5868ea..76dc01a1 100644
--- a/src/lem_interp/interp_inter_imp.lem
+++ b/src/lem_interp/interp_inter_imp.lem
@@ -506,18 +506,18 @@ let instruction_analysis top_level end_flag thunk_name regn_to_reg_details regis
          | Just addr -> addr
          | Nothing -> failwith "get_nia encountered invalid address" end in
        let dia_to_dia = function
-         | Interp.V_ctor (Id_aux (Id "DIA_none") _) _ _ _ -> DIA_none
-         | Interp.V_ctor (Id_aux (Id "DIA_concrete") _) _ _ address ->
+         | Interp.V_ctor (Id_aux (Id "DIAFP_none") _) _ _ _ -> DIA_none
+         | Interp.V_ctor (Id_aux (Id "DIAFP_concrete") _) _ _ address ->
             DIA_concrete_address (get_addr address)
-         | Interp.V_ctor (Id_aux (Id "DIA_reg") _) _ _ reg -> DIA_register (reg_to_reg_name reg) 
+         | Interp.V_ctor (Id_aux (Id "DIAFP_reg") _) _ _ reg -> DIA_register (reg_to_reg_name reg) 
          | _ -> failwith "Register footprint analysis did not return dia of expected type" end in
        let nia_to_nia = function
-         | Interp.V_ctor (Id_aux (Id "NIA_successor") _) _ _ _-> NIA_successor
-         | Interp.V_ctor (Id_aux (Id "NIA_concrete_address") _) _ _ address ->
+         | Interp.V_ctor (Id_aux (Id "NIAFP_successor") _) _ _ _-> NIA_successor
+         | Interp.V_ctor (Id_aux (Id "NIAFP_concrete_address") _) _ _ address ->
             NIA_concrete_address (get_addr address)
-         | Interp.V_ctor (Id_aux (Id "NIA_LR") _) _ _ _ -> NIA_LR
-         | Interp.V_ctor (Id_aux (Id "NIA_CTR") _) _ _ _ -> NIA_CTR
-         | Interp.V_ctor (Id_aux (Id "NIA_register") _) _ _ reg ->
+         | Interp.V_ctor (Id_aux (Id "NIAFP_LR") _) _ _ _ -> NIA_LR
+         | Interp.V_ctor (Id_aux (Id "NIAFP_CTR") _) _ _ _ -> NIA_CTR
+         | Interp.V_ctor (Id_aux (Id "NIAFP_register") _) _ _ reg ->
             NIA_register (reg_to_reg_name reg)
          | _ -> failwith "Register footprint analysis did not return nia of expected type" end in
        let ik_to_ik = function
diff --git a/src/lem_interp/sail_impl_base.lem b/src/lem_interp/sail_impl_base.lem
index 86778bee..63040ebf 100644
--- a/src/lem_interp/sail_impl_base.lem
+++ b/src/lem_interp/sail_impl_base.lem
@@ -1399,10 +1399,3 @@ instance  (Eq decode_error)
   let (=)  = decode_error_equal
   let (<>) = decode_error_inequal
 end
-
-type regfp =
-  | RFull of (string)
-  | RSlice of (string * integer * integer)
-  | RSliceBit of (string * integer)
-  | RField of (string * string)
-
diff --git a/src/pretty_print.ml b/src/pretty_print.ml
index 1ad4c632..68a3859c 100644
--- a/src/pretty_print.ml
+++ b/src/pretty_print.ml
@@ -2791,8 +2791,8 @@ let doc_typdef_lem regtypes (TD_aux(td,_)) = match td with
       | Id_aux ((Id "barrier_kind"),_) -> empty
       | Id_aux ((Id "instruction_kind"),_) -> empty
       | Id_aux ((Id "regfp"),_) -> empty
-      (* | Id_aux ((Id "nia"),_) -> empty
-      | Id_aux ((Id "dia"),_) -> empty *)
+      | Id_aux ((Id "niafp"),_) -> empty
+      | Id_aux ((Id "diafp"),_) -> empty
       | _ ->
          let ar_doc = group (separate_map (break 1) (doc_type_union_lem regtypes) ar) in
          let typ_pp =