-
Notifications
You must be signed in to change notification settings - Fork 9
Commit
This commit does not belong to any branch on this repository, and may belong to a fork outside of the repository.
check in gen files into rmem, now no more copying around files from t…
…he ISA packages in the build process
- Loading branch information
Showing
99 changed files
with
16,155 additions
and
195 deletions.
There are no files selected for viewing
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Original file line number | Diff line number | Diff line change |
---|---|---|
@@ -0,0 +1,70 @@ | ||
## import ISA models ################################################# | ||
|
||
get_all_deps: get_all_isa_models | ||
.PHONY: get_all_isa_models | ||
|
||
get_isa_model_%: ISABUILDDIR ?= build_isa_models/$* | ||
get_isa_model_%: BUILDISA ?= true | ||
get_isa_model_%: BUILDISATARGET ?= all | ||
get_isa_model_%: ISASAILFILES ?= $(ISADIR)/*.sail | ||
get_isa_model_%: ISALEMFILES ?= $(ISADIR)/*.lem | ||
get_isa_model_%: ISAGENFILES ?= $(ISADIR)/gen/* | ||
get_isa_model_%: FORCE | ||
rm -rf $(ISABUILDDIR) | ||
mkdir -p $(ISABUILDDIR) | ||
mkdir -p $(ISABUILDDIR)/gen | ||
cp -a $(ISAGENFILES) $(ISABUILDDIR)/gen/ | ||
CLEANDIRS += build_isa_models | ||
|
||
|
||
get_isa_model_power: ISANAME=power | ||
get_isa_model_power: ISADIR=$(saildir)/arch/power | ||
ifeq ($(filter PPCGEN,$(ISA_LIST)),) | ||
get_isa_model_power: BUILDISA=false | ||
RMEMSTUBS += src_top/PPCGenTransSail.ml | ||
endif | ||
get_all_isa_models: get_isa_model_power | ||
|
||
|
||
get_isa_model_aarch64: ISANAME=armV8 | ||
get_isa_model_aarch64: ISADIR=$(saildir)/arch/arm | ||
ifeq ($(filter AArch64,$(ISA_LIST)),) | ||
get_isa_model_aarch64: BUILDISA=false | ||
RMEMSTUBS += src_top/AArch64HGenTransSail.ml | ||
endif | ||
get_all_isa_models: get_isa_model_aarch64 | ||
|
||
# TODO: Currently AArch64Gen is always stubbed out | ||
RMEMSTUBS += src_top/AArch64GenTransSail.ml | ||
|
||
get_isa_model_mips: ISANAME=mips | ||
get_isa_model_mips: ISADIR=$(saildir)/arch/mips | ||
ifeq ($(filter MIPS,$(ISA_LIST)),) | ||
get_isa_model_mips: BUILDISA=false | ||
RMEMSTUBS += src_top/MIPSHGenTransSail.ml | ||
endif | ||
get_all_isa_models: get_isa_model_mips | ||
|
||
get_isa_model_riscv: ISANAME=riscv | ||
get_isa_model_riscv: ISADIR=$(riscvdir) | ||
get_isa_model_riscv: ISASAILFILES=$(ISADIR)/model/*.sail | ||
get_isa_model_riscv: ISALEMFILES=$(ISADIR)/generated_definitions/for-rmem/*.lem | ||
get_isa_model_riscv: ISALEMFILES+=$(ISADIR)/handwritten_support/0.11/*.lem | ||
get_isa_model_riscv: ISAGENFILES=$(ISADIR)/handwritten_support/hgen/*.hgen | ||
|
||
# By assigning a value to SAIL_DIR we force riscv to build with the | ||
# checked-out Sail2 instead of Sail2 from opam: | ||
get_isa_model_riscv: BUILDISATARGET=SAIL_DIR="$(realpath $(sail2dir))" riscv_rmem | ||
ifeq ($(filter RISCV,$(ISA_LIST)),) | ||
get_isa_model_riscv: BUILDISA=false | ||
RMEMSTUBS += src_top/RISCVHGenTransSail.ml | ||
endif | ||
get_all_isa_models: get_isa_model_riscv | ||
|
||
get_isa_model_x86: ISANAME=x86 | ||
get_isa_model_x86: ISADIR=$(saildir)/arch/x86 | ||
ifeq ($(filter X86,$(ISA_LIST)),) | ||
get_isa_model_x86: BUILDISA=false | ||
RMEMSTUBS += src_top/X86HGenTransSail.ml | ||
endif | ||
get_all_isa_models: get_isa_model_x86 |
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Original file line number | Diff line number | Diff line change |
---|---|---|
@@ -0,0 +1,47 @@ | ||
| `AArch64Unallocated | ||
| `AArch64TMStart of inst_reg (* t *) | ||
| `AArch64TMCommit | ||
| `AArch64TMAbort of boolean*bit5 (* retry,reason *) | ||
| `AArch64TMTest | ||
|
||
| `AArch64ImplementationDefinedTestBeginEnd of boolean (* isEnd *) | ||
| `AArch64ImplementationDefinedStopFetching | ||
| `AArch64ImplementationDefinedThreadStart | ||
| `AArch64AddSubCarry of inst_reg*inst_reg*inst_reg*reg_size*boolean*boolean (* d,n,m,datasize,sub_op,setflags *) | ||
| `AArch64AddSubExtendRegister of inst_reg*inst_reg*inst_reg*reg_size*boolean*boolean*extendType*range0_7 (* d,n,m,datasize,sub_op,setflags,extend_type,shift *) | ||
| `AArch64AddSubShiftedRegister of inst_reg*inst_reg*inst_reg*reg_size*boolean*boolean*shiftType*range0_63 (* d,n,m,datasize,sub_op,setflags,shift_type,shift_amount *) | ||
| `AArch64AddSubImmediate of inst_reg*inst_reg*reg_size*boolean*boolean*reg_size_bits (* d,n,datasize,sub_op,setflags,imm *) | ||
| `AArch64Address of inst_reg*boolean*bit64 (* d,page,imm *) | ||
| `AArch64LogicalImmediate of inst_reg*inst_reg*reg_size*boolean*logicalOp*reg_size_bits (* d,n,datasize,setflags,op,imm *) | ||
| `AArch64LogicalShiftedRegister of inst_reg*inst_reg*inst_reg*reg_size*boolean*logicalOp*shiftType*range0_63*boolean (* d,n,m,datasize,setflags,op,shift_type,shift_amount,invert *) | ||
| `AArch64Shift of inst_reg*inst_reg*inst_reg*reg_size*shiftType (* d,n,m,datasize,shift_type *) | ||
| `AArch64BranchConditional of bit64*bit4 (* offset,condition *) | ||
| `AArch64BranchImmediate of branchType*bit64 (* branch_type,offset *) | ||
| `AArch64BitfieldMove of inst_reg*inst_reg*reg_size*boolean*boolean*uinteger*uinteger*reg_size_bits*reg_size_bits (* d,n,datasize,inzero,extend,R,S,wmask,tmask *) | ||
| `AArch64BranchRegister of inst_reg*branchType (* n,branch_type *) | ||
| `AArch64CompareAndBranch of inst_reg*reg_size*boolean*bit64 (* t,datasize,iszero,offset *) | ||
| `AArch64ConditionalCompareImmediate of inst_reg*reg_size*boolean*bit4*bit4*reg_size_bits (* n,datasize,sub_op,condition,flags,imm *) | ||
| `AArch64ConditionalCompareRegister of inst_reg*inst_reg*reg_size*boolean*bit4*bit4 (* n,m,datasize,sub_op,condition,flags *) | ||
| `AArch64ClearExclusiveMonitor of uinteger (* imm *) | ||
| `AArch64CountLeading of inst_reg*inst_reg*reg_size*countOp (* d,n,datasize,opcode *) | ||
| `AArch64CRC of inst_reg*inst_reg*inst_reg*data_size*boolean (* d,n,m,size,crc32c *) | ||
| `AArch64ConditionalSelect of inst_reg*inst_reg*inst_reg*reg_size*bit4*boolean*boolean (* d,n,m,datasize,condition,else_inv,else_inc *) | ||
| `AArch64Barrier of memBarrierOp*mBReqDomain*mBReqTypes (* op,domain,types *) | ||
| `AArch64ExtractRegister of inst_reg*inst_reg*inst_reg*reg_size*uinteger (* d,n,m,datasize,lsb *) | ||
| `AArch64Hint of systemHintOp (* op *) | ||
| `AArch64LoadStoreAcqExc of inst_reg*inst_reg*inst_reg*inst_reg*accType*boolean*boolean*memOp*uinteger*reg_size*data_size (* n,t,t2,s,acctype,excl,pair,memop,elsize,regsize,datasize *) | ||
| `AArch64LoadStorePair of boolean*boolean*inst_reg*inst_reg*inst_reg*accType*memOp*boolean*data_size*bit64 (* wback,postindex,n,t,t2,acctype,memop,signed,datasize,offset *) | ||
| `AArch64LoadImmediate of inst_reg*inst_reg*accType*memOp*boolean*boolean*boolean*bit64*reg_size*data_size (* n,t,acctype,memop,signed,wback,postindex,offset,regsize,datasize *) | ||
| `AArch64LoadLiteral of inst_reg*memOp*boolean*uinteger*bit64*data_size (* t,memop,signed,size,offset,datasize *) | ||
| `AArch64LoadRegister of inst_reg*inst_reg*inst_reg*accType*memOp*boolean*boolean*boolean*extendType*uinteger*reg_size*data_size (* n,t,m,acctype,memop,signed,wback,postindex,extend_type,shift,regsize,datasize *) | ||
| `AArch64MultiplyAddSub of inst_reg*inst_reg*inst_reg*inst_reg*reg_size*data_size*boolean (* d,n,m,a,destsize,datasize,sub_op *) | ||
| `AArch64MoveWide of inst_reg*reg_size*bit16*uinteger*moveWideOp (* d,datasize,imm,pos,opcode *) | ||
| `AArch64Reverse of inst_reg*inst_reg*reg_size*revOp (* d,n,datasize,op *) | ||
| `AArch64Division of inst_reg*inst_reg*inst_reg*reg_size*boolean (* d,n,m,datasize,unsigned *) | ||
| `AArch64MultiplyAddSubLong of inst_reg*inst_reg*inst_reg*inst_reg*reg_size*data_size*boolean*boolean (* d,n,m,a,destsize,datasize,sub_op,unsigned *) | ||
| `AArch64MultiplyHigh of inst_reg*inst_reg*inst_reg*inst_reg*reg_size*data_size*boolean (* d,n,m,a,destsize,datasize,unsigned *) | ||
| `AArch64TestBitAndBranch of inst_reg*reg_size*uinteger*bit*bit64 (* t,datasize,bit_pos,bit_val,offset *) | ||
| `AArch64MoveSystemRegister of inst_reg*uinteger*uinteger*uinteger*uinteger*uinteger*boolean (* t,sys_op0,sys_op1,sys_op2,sys_crn,sys_crm,read *) | ||
| `AArch64MoveSystemImmediate of bit4*pSTATEField (* operand,field *) | ||
| `AArch64DataCache of inst_reg*dCOp | ||
| `AArch64InstructionCache of inst_reg*iCOp |
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Original file line number | Diff line number | Diff line change |
---|---|---|
@@ -0,0 +1,47 @@ | ||
| `AArch64Unallocated -> (y_reg, y_sreg) | ||
| `AArch64TMStart t -> fold_reg t (y_reg, y_sreg) | ||
| `AArch64TMCommit -> (y_reg, y_sreg) | ||
| `AArch64TMAbort (retry,reason) -> (y_reg, y_sreg) | ||
| `AArch64TMTest -> (y_reg, y_sreg) | ||
|
||
| `AArch64ImplementationDefinedStopFetching -> (y_reg, y_sreg) | ||
| `AArch64ImplementationDefinedThreadStart -> (y_reg, y_sreg) | ||
| `AArch64ImplementationDefinedTestBeginEnd (isEnd) -> (y_reg, y_sreg) | ||
| `AArch64AddSubCarry (d,n,m,datasize,sub_op,setflags) -> fold_reg m (fold_reg n (fold_reg d (y_reg, y_sreg))) | ||
| `AArch64AddSubExtendRegister (d,n,m,datasize,sub_op,setflags,extend_type,shift) -> fold_reg m (fold_reg n (fold_reg d (y_reg, y_sreg))) | ||
| `AArch64AddSubShiftedRegister (d,n,m,datasize,sub_op,setflags,shift_type,shift_amount) -> fold_reg m (fold_reg n (fold_reg d (y_reg, y_sreg))) | ||
| `AArch64AddSubImmediate (d,n,datasize,sub_op,setflags,imm) -> fold_reg n (fold_reg d (y_reg, y_sreg)) | ||
| `AArch64Address (d,page,imm) -> fold_reg d (y_reg, y_sreg) | ||
| `AArch64LogicalImmediate (d,n,datasize,setflags,op,imm) -> fold_reg n (fold_reg d (y_reg, y_sreg)) | ||
| `AArch64LogicalShiftedRegister (d,n,m,datasize,setflags,op,shift_type,shift_amount,invert) -> fold_reg m (fold_reg n (fold_reg d (y_reg, y_sreg))) | ||
| `AArch64Shift (d,n,m,datasize,shift_type) -> fold_reg m (fold_reg n (fold_reg d (y_reg, y_sreg))) | ||
| `AArch64BranchConditional (offset,condition) -> (y_reg, y_sreg) | ||
| `AArch64BranchImmediate (branch_type,offset) -> (y_reg, y_sreg) | ||
| `AArch64BitfieldMove (d,n,datasize,inzero,extend,_R,_S,wmask,tmask) -> fold_reg n (fold_reg d (y_reg, y_sreg)) | ||
| `AArch64BranchRegister (n,branch_type) -> fold_reg n (y_reg, y_sreg) | ||
| `AArch64CompareAndBranch (t,datasize,iszero,offset) -> fold_reg t (y_reg, y_sreg) | ||
| `AArch64ConditionalCompareImmediate (n,datasize,sub_op,condition,flags,imm) -> fold_reg n (y_reg, y_sreg) | ||
| `AArch64ConditionalCompareRegister (n,m,datasize,sub_op,condition,flags) -> fold_reg m (fold_reg n (y_reg, y_sreg)) | ||
| `AArch64ClearExclusiveMonitor (imm) -> (y_reg, y_sreg) | ||
| `AArch64CountLeading (d,n,datasize,opcode) -> fold_reg n (fold_reg d (y_reg, y_sreg)) | ||
| `AArch64CRC (d,n,m,size,crc32c) -> fold_reg m (fold_reg n (fold_reg d (y_reg, y_sreg))) | ||
| `AArch64ConditionalSelect (d,n,m,datasize,condition,else_inv,else_inc) -> fold_reg m (fold_reg n (fold_reg d (y_reg, y_sreg))) | ||
| `AArch64Barrier (op,domain,types) -> (y_reg, y_sreg) | ||
| `AArch64ExtractRegister (d,n,m,datasize,lsb) -> fold_reg m (fold_reg n (fold_reg d (y_reg, y_sreg))) | ||
| `AArch64Hint (op) -> (y_reg, y_sreg) | ||
| `AArch64LoadStoreAcqExc (n,t,t2,s,acctype,excl,pair,memop,elsize,regsize,datasize) -> fold_reg s (fold_reg t2 (fold_reg t (fold_reg n (y_reg, y_sreg)))) | ||
| `AArch64LoadStorePair (wback,postindex,n,t,t2,acctype,memop,signed,datasize,offset) -> fold_reg t2 (fold_reg t (fold_reg n (y_reg, y_sreg))) | ||
| `AArch64LoadImmediate (n,t,acctype,memop,signed,wback,postindex,offset,regsize,datasize) -> fold_reg t (fold_reg n (y_reg, y_sreg)) | ||
| `AArch64LoadLiteral (t,memop,signed,size,offset,datasize) -> fold_reg t (y_reg, y_sreg) | ||
| `AArch64LoadRegister (n,t,m,acctype,memop,signed,wback,postindex,extend_type,shift,regsize,datasize) -> fold_reg m (fold_reg t (fold_reg n (y_reg, y_sreg))) | ||
| `AArch64MultiplyAddSub (d,n,m,a,destsize,datasize,sub_op) -> fold_reg a (fold_reg m (fold_reg n (fold_reg d (y_reg, y_sreg)))) | ||
| `AArch64MoveWide (d,datasize,imm,pos,opcode) -> fold_reg d (y_reg, y_sreg) | ||
| `AArch64Reverse (d,n,datasize,op) -> fold_reg n (fold_reg d (y_reg, y_sreg)) | ||
| `AArch64Division (d,n,m,datasize,unsigned) -> fold_reg m (fold_reg n (fold_reg d (y_reg, y_sreg))) | ||
| `AArch64MultiplyAddSubLong (d,n,m,a,destsize,datasize,sub_op,unsigned) -> fold_reg a (fold_reg m (fold_reg n (fold_reg d (y_reg, y_sreg)))) | ||
| `AArch64MultiplyHigh (d,n,m,a,destsize,datasize,unsigned) -> fold_reg a (fold_reg m (fold_reg n (fold_reg d (y_reg, y_sreg)))) | ||
| `AArch64TestBitAndBranch (t,datasize,bit_pos,bit_val,offset) -> fold_reg t (y_reg, y_sreg) | ||
| `AArch64MoveSystemRegister (t,sys_op0,sys_op1,sys_op2,sys_crn,sys_crm,read) -> fold_reg t (y_reg, y_sreg) | ||
| `AArch64MoveSystemImmediate (operand,field) -> (y_reg, y_sreg) | ||
| `AArch64DataCache (t, dc_op) -> fold_reg t (y_reg, y_sreg) | ||
| `AArch64InstructionCache (t, ic_op) -> fold_reg t (y_reg, y_sreg) |
Oops, something went wrong.