From 87ffe603e44e9be6f4109f6a9dd475df6dcfc489 Mon Sep 17 00:00:00 2001 From: Shaked Flur Date: Fri, 8 Mar 2019 16:02:02 +0000 Subject: Adds the DC and IC instructions to AArch64_small; Also, removes etc/regfp.sail and etc/regfp2.sail in favour of lib/regfp.sail --- aarch64_small/Makefile | 2 +- aarch64_small/aarch64_regfp.sail | 26 +++++++++++ aarch64_small/armV8.h.sail | 4 ++ aarch64_small/armV8.sail | 80 +++++++++++++++++++++++++++++---- aarch64_small/armV8_A64_lib.sail | 64 ++++++++++++++++++++++++++ aarch64_small/armV8_lib.h.sail | 7 +++ etc/regfp.sail | 95 --------------------------------------- etc/regfp2.sail | 97 ---------------------------------------- lib/regfp.sail | 13 +++++- power/Makefile | 2 +- x86/Makefile | 2 +- 11 files changed, 187 insertions(+), 205 deletions(-) delete mode 100644 etc/regfp.sail delete mode 100644 etc/regfp2.sail diff --git a/aarch64_small/Makefile b/aarch64_small/Makefile index 3a5da685..b9abec80 100644 --- a/aarch64_small/Makefile +++ b/aarch64_small/Makefile @@ -24,7 +24,7 @@ armV8.ml: armV8.lem ../src/lem_interp/interp_ast.lem $(LEM) -ocaml -lib ../src/lem_interp/ $< -armV8_embed.lem: $(SOURCES) ../etc/regfp2.sail aarch64_regfp.sail +armV8_embed.lem: $(SOURCES) ../lib/regfp.sail aarch64_regfp.sail # also generates armV8_embed_sequential.lem, armV8_embed_types.lem, armV8_toFromInterp.lem $(SAIL) $(SAILFLAGS) -lem -lem_lib ArmV8_extras_embed -o armV8 $^ diff --git a/aarch64_small/aarch64_regfp.sail b/aarch64_small/aarch64_regfp.sail index 55f4a16b..ce155f0a 100644 --- a/aarch64_small/aarch64_regfp.sail +++ b/aarch64_small/aarch64_regfp.sail @@ -240,6 +240,32 @@ function initial_analysis (instr:ast) -> (regfps,regfps,regfps,niafps,diafp,inst IK_barrier(Barrier_ISB) }; }, + + (DataCache(t,dc_op)) => { + iR = appendL(iR,xFP(t)); + + ik = match dc_op { + IVAC => not_implemented("DC IVAC"), + ISW => not_implemented("DC ISW"), + CSW => not_implemented("DC CSW"), + CISW => not_implemented("DC CISW"), + ZVA => not_implemented("DC ZVA"), + CVAC => not_implemented("DC CVAC"), + CVAU => IK_cache_op(Cache_op_D_CVAU), + CIVAC => not_implemented("DC CIVAC") + }; + }, + + (InstructionCache(t,ic_op)) => { + iR = appendL(iR,xFP(t)); + + ik = match ic_op { + IALLUIS => not_implemented("IC IALLUIS"), + IALLU => not_implemented("IC IALLU"), + IVAU => IK_cache_op(Cache_op_I_IVAU) + }; + }, + (System(t,sys_op0,sys_op1,sys_op2,sys_crn,sys_crm,has_result)) => { oR = appendL(oR,xFP(t)); not_implemented("System"); /* because SysOp_R and SysOp_W */ diff --git a/aarch64_small/armV8.h.sail b/aarch64_small/armV8.h.sail index d0278d9d..b1eac1e7 100644 --- a/aarch64_small/armV8.h.sail +++ b/aarch64_small/armV8.h.sail @@ -64,6 +64,10 @@ bitfield TMSTATUS_type : bits(64) = register TMAbortEffect : TMSTATUS_type /* we abuse the register write to pass out the status value */ register TMStartEffect : TMSTATUS_type /* we abuse the register read to pass in the status value */ +/* abuse register write effect, instead of adding proper effects: */ +register data_cache_operation_CVAU : bits(64) +register instruction_cache_operation_IVAU : bits(64) + /* General purpose registers */ register R30 : bits(64) diff --git a/aarch64_small/armV8.sail b/aarch64_small/armV8.sail index 5e0b8cf9..d52099c0 100644 --- a/aarch64_small/armV8.sail +++ b/aarch64_small/armV8.sail @@ -61,6 +61,8 @@ union ast = { ClearExclusiveMonitor : (uinteger), Barrier : (MemBarrierOp,MBReqDomain,MBReqTypes), System : (reg_index,uinteger,uinteger,uinteger,uinteger,uinteger,boolean), + DataCache : (reg_index,DCOp), + InstructionCache : (reg_index,ICOp), MoveSystemRegister : (reg_index,uinteger,uinteger,uinteger,uinteger,uinteger,boolean), TestBitAndBranch : {'R 'bit_pos, RegisterSize('R) & 0 <= 'bit_pos < 'R. (reg_index,int('R),int('bit_pos),bit,bits(64))}, BranchImmediate : (BranchType,bits(64)), @@ -462,24 +464,84 @@ function clause execute ( Barrier(op,domain,types) ) = { /* SYS L=0b0 */ /* SYSL L=0b1 */ +/* The following are actually aliases of SYS: */ +/* DC L=0b0,SysOp(op1,CRn,CRm,op2) = Sys_DC */ +/* IC L=0b0,SysOp(op1,CRn,CRm,op2) = Sys_IC */ function clause decodeSystem (0b1101010100@[L]@0b01@(op1 : bits(3))@(CRn : bits(4))@(CRm : bits(4))@(op2 : bits(3))@(Rt:bits(5))) = { /* FIXME: we don't allow register reads in the decoding */ /* ARM: CheckSystemAccess(0b01, op1, CRn, CRm, op2, Rt, L);*/ t : reg_index = UInt_reg(Rt); - sys_op0 : uinteger = 1; - sys_op1 : uinteger = UInt(op1); - sys_op2 : uinteger = UInt(op2); - sys_crn : uinteger = UInt(CRn); - sys_crm : uinteger = UInt(CRm); - has_result : boolean = (L == b1); + sysop : SystemOp = Sys_SYS; + if L == b0 then + sysop = SysOp(op1,CRn,CRm,op2); + + match sysop { + Sys_AT => {not_implemented("AT"); None ();}, + + Sys_DC => + match (op1, CRm, op2) { + (0b000, 0b0110, 0b001) => Some(DataCache(t,IVAC)), + (0b000, 0b0110, 0b010) => Some(DataCache(t,ISW)), + (0b000, 0b1010, 0b010) => Some(DataCache(t,CSW)), + (0b000, 0b1110, 0b010) => Some(DataCache(t,CISW)), + (0b011, 0b0100, 0b001) => Some(DataCache(t,ZVA)), + (0b011, 0b1010, 0b001) => Some(DataCache(t,CVAC)), + (0b011, 0b1011, 0b001) => Some(DataCache(t,CVAU)), + (0b011, 0b1110, 0b001) => Some(DataCache(t,CIVAC)), + _ => {assert(false); None ();} + }, + + Sys_IC => + match (op1, CRm, op2) { + (0b000, 0b0001, 0b000) => Some(InstructionCache(t,IALLUIS)), + (0b000, 0b0101, 0b000) => Some(InstructionCache(t,IALLU)), + (0b011, 0b0101, 0b001) => Some(InstructionCache(t,IVAU)), + _ => {assert(false); None ();} + }, + + Sys_TLBI => {not_implemented("TLBI"); None ();}, + + Sys_SYS => { + sys_op0 : uinteger = 1; + sys_op1 : uinteger = UInt(op1); + sys_op2 : uinteger = UInt(op2); + sys_crn : uinteger = UInt(CRn); + sys_crm : uinteger = UInt(CRm); + has_result : boolean = (L == b1); + + Some(System(t,sys_op0,sys_op1,sys_op2,sys_crn,sys_crm,has_result)); + } + }; +} - Some(System(t,sys_op0,sys_op1,sys_op2,sys_crn,sys_crm,has_result)); +function clause execute ( DataCache(t,dc_op) ) = { + addr : bits(64) = rX(t); + + match dc_op { + IVAC => not_implemented("DC IVAC"), + ISW => not_implemented("DC ISW"), + CSW => not_implemented("DC CSW"), + CISW => not_implemented("DC CISW"), + ZVA => not_implemented("DC ZVA"), + CVAC => not_implemented("DC CVAC"), + CVAU => data_cache_operation_CVAU = addr, + CIVAC => not_implemented("DC CIVAC") + }; } -function clause execute ( System(t,sys_op0,sys_op1,sys_op2,sys_crn,sys_crm,has_result) ) = -{ +function clause execute ( InstructionCache(t,ic_op) ) = { + addr : bits(64) = rX(t); + + match ic_op { + IALLUIS => not_implemented("IC IALLUIS"), + IALLU => not_implemented("IC IALLU"), + IVAU => instruction_cache_operation_IVAU = addr + }; +} + +function clause execute ( System(t,sys_op0,sys_op1,sys_op2,sys_crn,sys_crm,has_result) ) = { if has_result then wX(t) = SysOp_R(sys_op0, sys_op1, sys_crn, sys_crm, sys_op2) else diff --git a/aarch64_small/armV8_A64_lib.sail b/aarch64_small/armV8_A64_lib.sail index ee9eabc9..cc65a03e 100644 --- a/aarch64_small/armV8_A64_lib.sail +++ b/aarch64_small/armV8_A64_lib.sail @@ -898,6 +898,70 @@ function Prefetch(address : bits(64), prfop : bits(5)) -> unit = { /** ENUMERATE:aarch64/instrs/system/barriers/barrierop/MemBarrierOp */ /** ENUMERATE:aarch64/instrs/system/hints/syshintop/SystemHintOp */ /** ENUMERATE:aarch64/instrs/system/register/cpsr/pstatefield/PSTATEField */ +/** FUNCTION:aarch64/instrs/system/sysops/sysop/SysOp */ + +function SysOp(op1 : bits(3), CRn : bits(4), CRm : bits(4), op2 : bits(3)) -> SystemOp = { + match (op1@CRn@CRm@op2) { + (0b000@0b0111@0b1000@0b000) => Sys_AT, /* S1E1R */ + (0b100@0b0111@0b1000@0b000) => Sys_AT, /* S1E2R */ + (0b110@0b0111@0b1000@0b000) => Sys_AT, /* S1E3R */ + (0b000@0b0111@0b1000@0b001) => Sys_AT, /* S1E1W */ + (0b100@0b0111@0b1000@0b001) => Sys_AT, /* S1E2W */ + (0b110@0b0111@0b1000@0b001) => Sys_AT, /* S1E3W */ + (0b000@0b0111@0b1000@0b010) => Sys_AT, /* S1E0R */ + (0b000@0b0111@0b1000@0b011) => Sys_AT, /* S1E0W */ + (0b100@0b0111@0b1000@0b100) => Sys_AT, /* S12E1R */ + (0b100@0b0111@0b1000@0b101) => Sys_AT, /* S12E1W */ + (0b100@0b0111@0b1000@0b110) => Sys_AT, /* S12E0R */ + (0b100@0b0111@0b1000@0b111) => Sys_AT, /* S12E0W */ + (0b011@0b0111@0b0100@0b001) => Sys_DC, /* ZVA */ + (0b000@0b0111@0b0110@0b001) => Sys_DC, /* IVAC */ + (0b000@0b0111@0b0110@0b010) => Sys_DC, /* ISW */ + (0b011@0b0111@0b1010@0b001) => Sys_DC, /* CVAC */ + (0b000@0b0111@0b1010@0b010) => Sys_DC, /* CSW */ + (0b011@0b0111@0b1011@0b001) => Sys_DC, /* CVAU */ + (0b011@0b0111@0b1110@0b001) => Sys_DC, /* CIVAC */ + (0b000@0b0111@0b1110@0b010) => Sys_DC, /* CISW */ + (0b000@0b0111@0b0001@0b000) => Sys_IC, /* IALLUIS */ + (0b000@0b0111@0b0101@0b000) => Sys_IC, /* IALLU */ + (0b011@0b0111@0b0101@0b001) => Sys_IC, /* IVAU */ + (0b100@0b1000@0b0000@0b001) => Sys_TLBI, /* IPAS2E1IS */ + (0b100@0b1000@0b0000@0b101) => Sys_TLBI, /* IPAS2LE1IS */ + (0b000@0b1000@0b0011@0b000) => Sys_TLBI, /* VMALLE1IS */ + (0b100@0b1000@0b0011@0b000) => Sys_TLBI, /* ALLE2IS */ + (0b110@0b1000@0b0011@0b000) => Sys_TLBI, /* ALLE3IS */ + (0b000@0b1000@0b0011@0b001) => Sys_TLBI, /* VAE1IS */ + (0b100@0b1000@0b0011@0b001) => Sys_TLBI, /* VAE2IS */ + (0b110@0b1000@0b0011@0b001) => Sys_TLBI, /* VAE3IS */ + (0b000@0b1000@0b0011@0b010) => Sys_TLBI, /* ASIDE1IS */ + (0b000@0b1000@0b0011@0b011) => Sys_TLBI, /* VAAE1IS */ + (0b100@0b1000@0b0011@0b100) => Sys_TLBI, /* ALLE1IS */ + (0b000@0b1000@0b0011@0b101) => Sys_TLBI, /* VALE1IS */ + (0b100@0b1000@0b0011@0b101) => Sys_TLBI, /* VALE2IS */ + (0b110@0b1000@0b0011@0b101) => Sys_TLBI, /* VALE3IS */ + (0b100@0b1000@0b0011@0b110) => Sys_TLBI, /* VMALLS12E1IS */ + (0b000@0b1000@0b0011@0b111) => Sys_TLBI, /* VAALE1IS */ + (0b100@0b1000@0b0100@0b001) => Sys_TLBI, /* IPAS2E1 */ + (0b100@0b1000@0b0100@0b101) => Sys_TLBI, /* IPAS2LE1 */ + (0b000@0b1000@0b0111@0b000) => Sys_TLBI, /* VMALLE1 */ + (0b100@0b1000@0b0111@0b000) => Sys_TLBI, /* ALLE2 */ + (0b110@0b1000@0b0111@0b000) => Sys_TLBI, /* ALLE3 */ + (0b000@0b1000@0b0111@0b001) => Sys_TLBI, /* VAE1 */ + (0b100@0b1000@0b0111@0b001) => Sys_TLBI, /* VAE2 */ + (0b110@0b1000@0b0111@0b001) => Sys_TLBI, /* VAE3 */ + (0b000@0b1000@0b0111@0b010) => Sys_TLBI, /* ASIDE1 */ + (0b000@0b1000@0b0111@0b011) => Sys_TLBI, /* VAAE1 */ + (0b100@0b1000@0b0111@0b100) => Sys_TLBI, /* ALLE1 */ + (0b000@0b1000@0b0111@0b101) => Sys_TLBI, /* VALE1 */ + (0b100@0b1000@0b0111@0b101) => Sys_TLBI, /* VALE2 */ + (0b110@0b1000@0b0111@0b101) => Sys_TLBI, /* VALE3 */ + (0b100@0b1000@0b0111@0b110) => Sys_TLBI, /* VMALLS12E1 */ + (0b000@0b1000@0b0111@0b111) => Sys_TLBI, /* VAALE1 */ + _ => Sys_SYS + }; +} + +/** ENUMERATE:aarch64/instrs/system/sysops/sysop/SystemOp */ /** FUNCTION:aarch64/translation/faults/AArch64.AlignmentFault */ function AArch64_AlignmentFault(acctype : AccType, iswrite : boolean, secondstage : boolean) -> FaultRecord = { diff --git a/aarch64_small/armV8_lib.h.sail b/aarch64_small/armV8_lib.h.sail index 66071b3a..332ad18c 100644 --- a/aarch64_small/armV8_lib.h.sail +++ b/aarch64_small/armV8_lib.h.sail @@ -210,6 +210,13 @@ enum SystemHintOp = enum PSTATEField = {PSTATEField_DAIFSet, PSTATEField_DAIFClr, PSTATEField_SP} +enum SystemOp = {Sys_AT, Sys_DC, Sys_IC, Sys_TLBI, Sys_SYS} + +enum DCOp = {IVAC, ISW, CSW, CISW, ZVA, CVAC, CVAU, CIVAC} + +enum ICOp = {IALLUIS, IALLU, IVAU} + + val rPC : unit -> bits(64) effect {rreg} val rSP : forall 'N, 'N in {8,16,32,64}. implicit('N) -> bits('N) effect {rreg,escape} val wX : forall 'N, 'N in {8,16,32,64}. (reg_index,bits('N)) -> unit effect {wreg} diff --git a/etc/regfp.sail b/etc/regfp.sail deleted file mode 100644 index de842c5c..00000000 --- a/etc/regfp.sail +++ /dev/null @@ -1,95 +0,0 @@ -(* 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_indirect_address; -} - -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_reserve; - Read_acquire; - Read_exclusive; - Read_exclusive_acquire; - Read_stream; - Read_RISCV_acquire; - Read_RISCV_strong_acquire; - Read_RISCV_reserved; - Read_RISCV_reserved_acquire; - Read_RISCV_reserved_strong_acquire; - Read_X86_locked; -} - -typedef write_kind = enumerate { - Write_plain; - Write_conditional; - Write_release; - Write_exclusive; - Write_exclusive_release; - Write_RISCV_release; - Write_RISCV_strong_release; - Write_RISCV_conditional; - Write_RISCV_conditional_release; - Write_RISCV_conditional_strong_release; - Write_X86_locked; -} - -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; - Barrier_MIPS_SYNC; - Barrier_RISCV_rw_rw; - Barrier_RISCV_r_rw; - Barrier_RISCV_r_r; - Barrier_RISCV_rw_w; - Barrier_RISCV_w_w; - Barrier_RISCV_tso; - Barrier_RISCV_i; - Barrier_x86_MFENCE; -} - -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; - (read_kind, write_kind) IK_mem_rmw; - IK_branch; - (trans_kind) IK_trans; - IK_simple -} diff --git a/etc/regfp2.sail b/etc/regfp2.sail deleted file mode 100644 index 85141853..00000000 --- a/etc/regfp2.sail +++ /dev/null @@ -1,97 +0,0 @@ -/* iR : input registers, - * oR : output registers, - * aR : registers feeding into the memory address */ - -/* branch instructions currently are not writing to NIA */ - -union regfp = { - RFull : string, - RSlice : (string,nat,nat), - RSliceBit : (string,nat), - RField : (string,string), -} - -type regfps = list(regfp) - -union niafp = { - NIAFP_successor : unit, - NIAFP_concrete_address : bits(64), - NIAFP_indirect_address : unit, -} - -type niafps = list(niafp) - -/* only for MIPS */ -union diafp = { - DIAFP_none : unit, - DIAFP_concrete : bits(64), - DIAFP_reg : regfp, -} - -enum read_kind = { - Read_plain, - Read_reserve, - Read_acquire, - Read_exclusive, - Read_exclusive_acquire, - Read_stream, - Read_RISCV_acquire, - Read_RISCV_strong_acquire, - Read_RISCV_reserved, - Read_RISCV_reserved_acquire, - Read_RISCV_reserved_strong_acquire, - Read_X86_locked -} - -enum write_kind = { - Write_plain, - Write_conditional, - Write_release, - Write_exclusive, - Write_exclusive_release, - Write_RISCV_release, - Write_RISCV_strong_release, - Write_RISCV_conditional, - Write_RISCV_conditional_release, - Write_RISCV_conditional_strong_release, - Write_X86_locked -} - -enum barrier_kind = { - 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, - Barrier_MIPS_SYNC, - Barrier_RISCV_rw_rw, - Barrier_RISCV_r_rw, - Barrier_RISCV_r_r, - Barrier_RISCV_rw_w, - Barrier_RISCV_w_w, - Barrier_RISCV_tso, - Barrier_RISCV_i, - Barrier_x86_MFENCE -} - -enum trans_kind = { - Transaction_start, - Transaction_commit, - Transaction_abort -} - -union instruction_kind = { - IK_barrier : barrier_kind, - IK_mem_read : read_kind, - IK_mem_write : write_kind, - IK_mem_rmw : (read_kind, write_kind), - IK_branch : unit, - IK_trans : trans_kind, - IK_simple : unit, -} diff --git a/lib/regfp.sail b/lib/regfp.sail index cc017585..6044e1cc 100644 --- a/lib/regfp.sail +++ b/lib/regfp.sail @@ -90,6 +90,16 @@ enum trans_kind = { Transaction_abort } +/* cache maintenance instructions */ +enum cache_op_kind = { + /* AArch64 DC */ + Cache_op_D_IVAC, Cache_op_D_ISW, Cache_op_D_CSW, Cache_op_D_CISW, + Cache_op_D_ZVA, Cache_op_D_CVAC, Cache_op_D_CVAU, Cache_op_D_CIVAC, + /* AArch64 IC */ + Cache_op_I_IALLUIS, Cache_op_I_IALLU, Cache_op_I_IVAU +} + + union instruction_kind = { IK_barrier : barrier_kind, IK_mem_read : read_kind, @@ -97,5 +107,6 @@ union instruction_kind = { IK_mem_rmw : (read_kind, write_kind), IK_branch : unit, IK_trans : trans_kind, - IK_simple : unit + IK_simple : unit, + IK_cache_op : cache_op_kind } diff --git a/power/Makefile b/power/Makefile index f7c49e00..be97aa0b 100644 --- a/power/Makefile +++ b/power/Makefile @@ -1,7 +1,7 @@ SAIL:=../src/sail.native LEM:=../../lem/lem -SOURCES:=power.sail ../etc/regfp.sail power_regfp.sail +SOURCES:=power.sail ../lib/regfp.sail power_regfp.sail all: power.lem power.ml power_embed.lem diff --git a/x86/Makefile b/x86/Makefile index 6863714d..0c6e830e 100644 --- a/x86/Makefile +++ b/x86/Makefile @@ -1,7 +1,7 @@ SAIL=../src/sail.native LEM:=../../lem/lem -SOURCES=../etc/regfp.sail x64.sail +SOURCES=../lib/regfp.sail x64.sail all: x86.lem x86.ml x86_embed.lem -- cgit v1.2.3