From dd1615cd663fe28d0a7ee7c589ee6f7ca16b7560 Mon Sep 17 00:00:00 2001 From: Christopher Pulte Date: Mon, 7 Nov 2016 11:44:00 +0000 Subject: factor out regfp analysis types into etc/regfp.sail --- etc/regfp.sail | 72 +++++++++++++++++++++++++++++++++ mips/mips_regfp.sail | 81 ++++--------------------------------- src/Makefile | 4 +- src/gen_lib/prompt.lem | 9 +++-- src/gen_lib/sail_values.lem | 57 +++++++++++++++++++++----- src/lem_interp/interp_inter_imp.lem | 16 ++++---- src/lem_interp/sail_impl_base.lem | 7 ---- src/pretty_print.ml | 4 +- 8 files changed, 143 insertions(+), 107 deletions(-) create mode 100644 etc/regfp.sail 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 + +typedef niafp = const union { + NIAFP_successor; + (bit[64]) NIAFP_concrete_address; + NIAFP_LR; + NIAFP_CTR; + (regfp) NIAFP_register; +} + +typedef niafps = list + +(* 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 - -typedef nia = bit[64] -typedef nias = list - -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 = -- cgit v1.2.3