pull files from idlarm

10 files changed, 70 insertions, 24 deletions

diff --git a/arm/Makefile b/arm/Makefile
index 16ad6ab4..99c7998f 100644
--- a/arm/Makefile
+++ b/arm/Makefile
@@ -13,15 +13,15 @@ endif
 LEMINTERPDIR=../src/lem_interp/
 
 # the order of the files is important
-SOURCES=armv8.h.sail\
-  armv8_A64_sys_regs.sail\
-  armv8_A64_special_purpose_regs.sail\
-  armv8_A32_sys_regs.sail\
-  armv8_pstate.sail\
-  armv8_lib.h.sail\
-  armv8_common_lib.sail\
-  armv8_A64_lib.sail\
-  armv8.sail
+SOURCES=armV8.h.sail\
+  armV8_A64_sys_regs.sail\
+  armV8_A64_special_purpose_regs.sail\
+  armV8_A32_sys_regs.sail\
+  armV8_pstate.sail\
+  armV8_lib.h.sail\
+  armV8_common_lib.sail\
+  armV8_A64_lib.sail\
+  armV8.sail
 
 all: $(BUILDDIR)/armv8.ml
 
@@ -43,9 +43,22 @@ $(BUILDDIR)/armv8.ml: $(BUILDDIR)/armv8.lem
 
 ######################################################################
 ETCDIR=../etc
-SAIL_FILES=$(wildcard *.sail)
 
 apply_header:
-	headache -c $(ETCDIR)/headache_config -h $(ETCDIR)/arm_header $(SAIL_FILES)
+	-chmod u+w *.sail
+	headache -c $(ETCDIR)/headache_config -h $(ETCDIR)/arm_header *.sail
+	chmod a-w *.sail
 
 .PHONY: apply_header
+
+######################################################################
+IDLARM=../../../rsem/idlarm
+
+pull_from_idlarm:
+	svn up $(IDLARM)
+	$(MAKE) -C $(IDLARM)
+	-chmod u+w *.sail
+	rm -f *.sail
+	cp -a $(IDLARM)/build/*.sail ./
+	chmod a-w *.sail
+	$(MAKE) apply_header
diff --git a/arm/armv8.h.sail b/arm/armV8.h.sail
index 1d20c635..d9232a5b 100644
--- a/arm/armv8.h.sail
+++ b/arm/armV8.h.sail
@@ -160,5 +160,5 @@ let IMPLEMENTATION_DEFINED =
   IsSecureBelowEL3 = false;
 }
 
-(* FIXME:  *)
+(* FIXME: ask Kathy what should we do with this *)
 let UNKNOWN = 0
diff --git a/arm/armv8.sail b/arm/armV8.sail
index e7e27c17..385c40d1 100644
--- a/arm/armv8.sail
+++ b/arm/armV8.sail
@@ -38,6 +38,7 @@ typedef ast = const union forall Nat 'R, 'R IN {32, 64},     (* register size *)
   Unallocated;
   (boolean) ImplementationDefinedTestBeginEnd;
   ImplementationDefinedStopFetching;
+  ImplementationDefinedThreadStart;
 
   (reg_index,[:'R:],boolean,bit[64]) CompareAndBranch;
   (bit[64],bit[4]) BranchConditional;
@@ -170,7 +171,7 @@ function clause decodeExceptionGeneration (0b11010100:0b000:(bit[16]) imm16:0b00
   Some(GenerateExceptionEL3(imm))
 }
 
-function clause execute (GenerateExceptionEL2(imm)) =
+function clause execute (GenerateExceptionEL3(imm)) =
 {
   if ~(HaveEL(EL3)) | PSTATE_EL == EL0 then
     UnallocatedEncoding();
@@ -478,6 +479,17 @@ function clause execute ( ImplementationDefinedStopFetching ) =
   info("stop fetching instructions");
 }
 
+(* instructions to signal ppcmem to start a thread *)
+function clause decodeImplementationDefined (0b1101010100:[0]:0b01:0b011:[1]:[_]:0b11:0b0000:0b000:0b00011) =
+{
+  Some(ImplementationDefinedThreadStart)
+}
+
+function clause execute ( ImplementationDefinedThreadStart ) =
+{
+  info("thread start");
+}
+
 end decodeImplementationDefined
 
 (* TBNZ *)
@@ -877,7 +889,7 @@ function clause execute ( LoadStorePairNonTemp(wback,postindex,n,t,t2,acctype,me
   (bit[64]) address := 0; (* ARM: uninitialized *)
   (bit['D]) data1 := 0; (* ARM: uninitialized *)
   (bit['D]) data2 := 0; (* ARM: uninitialized *)
-  (*constant*) ([|1:8|]) dbytes := datasize quot 8;
+  (*constant*) (uinteger) dbytes := datasize quot 8;
   (boolean) rt_unknown := false;
 
   if memop == MemOp_LOAD & t == t2 then {
@@ -1359,7 +1371,7 @@ function clause execute ( LoadStorePair(wback,postindex,n,t,t2,acctype,memop,_si
   (bit[64]) address := 0; (* ARM: uninitialized *)
   (bit['D]) data1 := 0; (* ARM: uninitialized *)
   (bit['D]) data2 := 0; (* ARM: uninitialized *)
-  (*constant*) ([|1:8|]) dbytes := datasize quot 8;
+  (*constant*) (uinteger) dbytes := datasize quot 8;
   (boolean) rt_unknown := false;
   (boolean) wb_unknown := false;
 
@@ -1540,7 +1552,7 @@ function clause execute (AddSubImmediate(d,n,datasize,sub_op,setflags,imm)) = {
   }
 }
 
-(* BFM *)
+(* BFM *) 
 (* SBFM *)
 (* UBFM *)
 function forall Nat 'R, 'R IN {32,64}, Nat 'D, 'D IN {8,16,32,64}.
diff --git a/arm/armv8_A32_sys_regs.sail b/arm/armV8_A32_sys_regs.sail
index 8b4a8e00..8b4a8e00 100644
--- a/arm/armv8_A32_sys_regs.sail
+++ b/arm/armV8_A32_sys_regs.sail
diff --git a/arm/armv8_A64_lib.sail b/arm/armV8_A64_lib.sail
index 6489e3ba..b3104255 100644
--- a/arm/armv8_A64_lib.sail
+++ b/arm/armV8_A64_lib.sail
@@ -550,6 +550,7 @@ function forall Nat 'N, 'N IN {8,16,32,64,128}. unit effect {wreg} wV((SIMD_inde
 
 function forall Nat 'N, 'N IN {8,16,32,64,128}. bit['N] effect {rreg} rV((SIMD_index) n) = mask(_V[n])
 
+
 (** FUNCTION:// Vpart[] - non-assignment form *)
 
 function forall Nat 'N, 'N IN {8,16,32,64,128}. bit['N] effect {rreg} rVpart (n,part) = {
@@ -753,6 +754,7 @@ function unit AArch64_ExceptionReturn((bit[64]) new_pc, (bit[32]) spsr) =
   not_implemented("AArch64_ExceptionReturn");
 }
 
+(** ENUMERATE:aarch64/instrs/countop/CountOp *)
 (** FUNCTION:ExtendType DecodeRegExtend(bits(3) op) *)
 
 function ExtendType DecodeRegExtend ((bit[3]) op) = ([|8|]) op
@@ -783,6 +785,8 @@ function bit['N] ExtendReg ((reg_index) _reg, (ExtendType) type, ([:'S:]) shift)
   Extend((_val[(len - 1)..0]) : ((bit['S]) (Zeros())), _unsigned)
 }
 
+(** ENUMERATE:aarch64/instrs/extendreg/ExtendType *)
+(** ENUMERATE:aarch64/instrs/integer/arithmetic/rev/revop/RevOp *)
 (** FUNCTION:(bits(M), bits(M)) DecodeBitMasks (bit immN, bits(6) imms, bits(6) immr, boolean immediate) *)
 
 val forall Nat 'M, Nat 'E. (implicit<'M>,bit,bit[6],bit[6],boolean) -> (bit['M],bit['M]) effect {escape} DecodeBitMasks
@@ -819,6 +823,7 @@ function forall Nat 'M, Nat 'E, 'E IN {2,4,8,16,32,64}. (bit['M],bit['M]) Decode
   (wmask, tmask);
 }}
 
+(** ENUMERATE:aarch64/instrs/integer/ins-ext/insert/movewide/movewideop/MoveWideOp *)
 (** FUNCTION:ShiftType DecodeShift(bits(2) op) *)
 
 function ShiftType DecodeShift((bit[2]) op) = ([|4|]) op
@@ -837,6 +842,9 @@ function forall Nat 'N. bit['N] effect {rreg} ShiftReg((reg_index) _reg, (ShiftT
   result;
 }
 
+(** ENUMERATE:aarch64/instrs/integer/shiftreg/ShiftType *)
+(** ENUMERATE:aarch64/instrs/logicalop/LogicalOp *)
+(** ENUMERATE:aarch64/instrs/memory/memop/MemOp *)
 (** FUNCTION:aarch64/instrs/memory/prefetch/Prefetch *)
 
 function unit Prefetch((bit[64]) address, (bit[5]) prfop) =
@@ -858,6 +866,9 @@ function unit Prefetch((bit[64]) address, (bit[5]) prfop) =
   Hint_Prefetch(address, hint, target, stream);
 }}
 
+(** ENUMERATE:aarch64/instrs/system/barriers/barrierop/MemBarrierOp *)
+(** ENUMERATE:aarch64/instrs/system/hints/syshintop/SystemHintOp *)
+(** ENUMERATE:aarch64/instrs/system/register/cpsr/pstatefield/PSTATEField *)
 (** FUNCTION:aarch64/translation/faults/AArch64.AlignmentFault *)
 
 function FaultRecord AArch64_AlignmentFault((AccType) acctype, (boolean) iswrite, (boolean) secondstage) =
@@ -907,3 +918,4 @@ function AddressDescriptor AArch64_TranslateAddress((bit[64]) vaddress, (AccType
 
   result;
 }
+
diff --git a/arm/armv8_A64_special_purpose_regs.sail b/arm/armV8_A64_special_purpose_regs.sail
index c12f0eeb..47e910bd 100644
--- a/arm/armv8_A64_special_purpose_regs.sail
+++ b/arm/armV8_A64_special_purpose_regs.sail
@@ -99,3 +99,4 @@ register (SPSR_type) SPSR_EL3 (* Saved Program Status Register (EL3) *)
 register (bit[64]) ELR_EL1 (* Exception Link Register (EL1) *)
 register (bit[64]) ELR_EL2 (* Exception Link Register (EL2) *)
 register (bit[64]) ELR_EL3 (* Exception Link Register (EL3) *)
+
diff --git a/arm/armv8_A64_sys_regs.sail b/arm/armV8_A64_sys_regs.sail
index 918e2b53..90228da1 100644
--- a/arm/armv8_A64_sys_regs.sail
+++ b/arm/armV8_A64_sys_regs.sail
@@ -458,6 +458,7 @@ typedef EDSCR_type = register bits [31:0]
 }
 register (EDSCR_type) EDSCR (* External Debug Status and Control Register *)
 
+
 function unit effect pure AArch64_ResetControlRegisters((boolean) cold_reset) =
 {
   ()
diff --git a/arm/armv8_common_lib.sail b/arm/armV8_common_lib.sail
index b09f9b7c..84332c71 100644
--- a/arm/armv8_common_lib.sail
+++ b/arm/armV8_common_lib.sail
@@ -479,6 +479,7 @@ function forall Nat 'N. (bit['N],bit[4]) AddWithCarry ((bit['N]) x, (bit['N]) y,
   (result,[n]:[z]:[c]:[v])
 }
 
+(** TYPE:shared/functions/memory/AddressDescriptor *)
 (** FUNCTION:boolean BigEndian() *)
 
 function boolean effect {rreg} BigEndian() = {
@@ -538,10 +539,19 @@ function unit effect {barr} DataSynchronizationBarrier((MBReqDomain) domain, (MB
   };
 }
 
+(** ENUMERATE:shared/functions/memory/DeviceType *)
+(** ENUMERATE:shared/functions/memory/DeviceType *)
+(** TYPE:shared/functions/memory/FaultRecord *)
+(** TYPE:shared/functions/memory/FullAddress *)
 (** FUNCTION:shared/functions/memory/Hint_Prefetch *)
 val (bit[64],PrefetchHint,integer,boolean) -> unit effect pure Hint_Prefetch
 function unit effect pure Hint_Prefetch(addr,hint,target,stream) = ()
-
+(** ENUMERATE:shared/functions/memory/MBReqDomain *)
+(** ENUMERATE:shared/functions/memory/MBReqTypes *)
+(** TYPE:shared/functions/memory/MemAttrHints *)
+(** ENUMERATE:shared/functions/memory/MemType *)
+(** TYPE:shared/functions/memory/MemoryAttributes *)
+(** ENUMERATE:shared/functions/memory/PrefetchHint *)
 (** FUNCTION:shared/functions/memory/_Mem *)
 
 (* regular load *)
@@ -749,6 +759,7 @@ function forall Nat 'N, 'N IN {32,64}. unit effect {rreg,wreg} BranchTo((bit['N]
   };
 }
 
+(** ENUMERATE:shared/functions/registers/BranchType *)
 (** FUNCTION:shared/functions/registers/Hint_Branch *)
 
 function unit effect pure Hint_Branch((BranchType) hint) =
@@ -758,7 +769,6 @@ function unit effect pure Hint_Branch((BranchType) hint) =
 
 (** FUNCTION:shared/functions/registers/ResetExternalDebugRegisters *)
 val extern boolean -> unit effect pure ResetExternalDebugRegisters
-
 (** FUNCTION:shared/functions/registers/ThisInstrAddr *)
 
 val forall Nat 'N. implicit<'N> -> bit['N] effect {rreg} ThisInstrAddr
@@ -801,7 +811,6 @@ function bit[32] rSPSR() =
 
 (** FUNCTION:shared/functions/system/ClearEventRegister *)
 val extern unit -> unit effect pure ClearEventRegister
-
 (** FUNCTION:boolean ConditionHolds(bits(4) cond) *)
 
 function boolean effect {rreg} ConditionHolds((bit[4]) _cond) =
@@ -827,6 +836,7 @@ function boolean effect {rreg} ConditionHolds((bit[4]) _cond) =
   result;
 }
 
+(** ENUMERATE:shared/functions/system/EL0 *)
 (** FUNCTION:boolean ELUsingAArch32(bits(2) el) *)
 
 function boolean ELUsingAArch32((bit[2]) el) =
@@ -834,10 +844,8 @@ function boolean ELUsingAArch32((bit[2]) el) =
 
 (** FUNCTION:shared/functions/system/EventRegisterSet *)
 val extern unit -> unit effect pure EventRegisterSet
-
 (** FUNCTION:shared/functions/system/EventRegistered *)
 val extern unit -> boolean effect pure EventRegistered
-
 (** FUNCTION:shared/functions/system/HaveAArch32EL *)
 
 function boolean HaveAArch32EL((bit[2]) el) =
@@ -892,7 +900,6 @@ function unit Hint_Yield() = ()
 
 (** FUNCTION:shared/functions/system/InstructionSynchronizationBarrier *)
 val extern unit -> unit effect {barr} InstructionSynchronizationBarrier
-
 (** FUNCTION:shared/functions/system/InterruptPending *)
 
 val extern unit -> boolean effect pure InterruptPending
@@ -922,6 +929,7 @@ function boolean IsSecureBelowEL3() = {
     IMPLEMENTATION_DEFINED.IsSecureBelowEL3;
 }
 
+(** ENUMERATE:shared/functions/system/Mode_Bits *)
 (** FUNCTION:shared/functions/system/SCR_GEN *)
 
 function SCRType SCR_GEN() = {
@@ -963,10 +971,8 @@ function boolean UsingAArch32() =
 
 (** FUNCTION:shared/functions/system/WaitForEvent *)
 val extern unit -> unit effect pure WaitForEvent
-
 (** FUNCTION:shared/functions/system/WaitForInterrupt *)
 val extern unit -> unit effect pure WaitForInterrupt
-
 (** FUNCTION:shared/translation/translation/PAMax *)
 
 function uinteger PAMax() =
@@ -996,3 +1002,4 @@ function bit[2] effect {rreg} S1TranslationRegime () =
   else
     EL1
 }
+
diff --git a/arm/armv8_lib.h.sail b/arm/armV8_lib.h.sail
index e8e979c8..e8e979c8 100644
--- a/arm/armv8_lib.h.sail
+++ b/arm/armV8_lib.h.sail
diff --git a/arm/armv8_pstate.sail b/arm/armV8_pstate.sail
index 5be50b19..5be50b19 100644
--- a/arm/armv8_pstate.sail
+++ b/arm/armV8_pstate.sail