Merge branch 'master' of https://bitbucket.org/Peter_Sewell/sail

6 files changed, 76 insertions, 64 deletions

diff --git a/arm/armV8.h.sail b/arm/armV8.h.sail
index d9232a5b..01927fbe 100644
--- a/arm/armV8.h.sail
+++ b/arm/armV8.h.sail
@@ -136,6 +136,14 @@ function unit effect { escape } not_implemented((string) message) =
   exit message;
 }
 
+(* not_implemented_extern is used to indicate something ARM did not define
+   and we did not define yet either. Those functions used to be declared as
+   external but undefined there. *)
+function forall 'a. 'a effect { escape } not_implemented_extern((string) message) =
+{
+  exit message;
+}
+
 (* info is used to convey information to the user *)
 function unit effect pure info((string) message) = ()
 
diff --git a/arm/armV8.sail b/arm/armV8.sail
index 385c40d1..298a6a8c 100644
--- a/arm/armV8.sail
+++ b/arm/armV8.sail
@@ -238,7 +238,7 @@ scattered function forall Nat 'R, 'R IN {32,64}, Nat 'D, 'D IN {8,16,32,64}.
         option<(ast<'R,'D>)> decodeSystem
 
 (* MSR (immediate) *)
-function clause decodeSystem (0b1101010100:[0]:0b00:op1:0b0100:CRm:op2:0b11111) = {
+function clause decodeSystem (0b1101010100:[0]:0b00:(bit[3]) op1:0b0100:CRm:(bit[3]) op2:0b11111) = {
   (* FIXME: we don't allow register reads in the decoding *)
   (* ARM: CheckSystemAccess(0b00, op1, 0b0100, CRm, op2, 0b11111, 0); *)
 
@@ -398,7 +398,7 @@ function clause execute ( Barrier(op,domain,types) ) = {
 
 (* SYS L=0b0 *)
 (* SYSL L=0b1 *)
-function clause decodeSystem (0b1101010100:[L]:0b01:op1:CRn:CRm:op2:Rt) = {
+function clause decodeSystem (0b1101010100:[L]:0b01:(bit[3]) op1:(bit[4]) CRn:(bit[4]) CRm:(bit[3]) op2:Rt) = {
   (* FIXME: we don't allow register reads in the decoding *)
   (* ARM: CheckSystemAccess(0b01, op1, CRn, CRm, op2, Rt, L);*)
 
@@ -650,7 +650,7 @@ function forall Nat 'R, 'R IN {32,64}, Nat 'D, 'D IN {8,16,32,64}.
   Some(LoadLiteral(t,memop,_signed,size,offset,datasize));
 }
 
-function clause execute ( LoadLiteral(t,memop,_signed,size,offset,datasize) ) = {
+function clause execute ( LoadLiteral(t,memop,_signed,size,offset,([:'D:]) datasize) ) = {
   (bit[64]) address := rPC() + offset;
   (bit['D]) data := 0; (* ARM: uninitialized *)
 
diff --git a/arm/armV8_A64_lib.sail b/arm/armV8_A64_lib.sail
index b3104255..bb049344 100644
--- a/arm/armV8_A64_lib.sail
+++ b/arm/armV8_A64_lib.sail
@@ -145,11 +145,12 @@ function unit effect {rreg} AArch64_CheckForWFxTrap((bit[2]) target_el, (boolean
     assert((HaveEL(target_el)), None);
 
     (boolean) trap := false; (* ARM: uninitialized *)
-    switch target_el {
-        case EL1 -> trap := ((if is_wfe then SCTLR_EL1.nTWE else SCTLR_EL1.nTWI) == 0)
-        case EL2 -> trap := ((if is_wfe then HCR_EL2.TWE else HCR_EL2.TWI) == 1)
-        case EL3 -> trap := ((if is_wfe then SCR_EL3.TWE else SCR_EL3.TWI) == 1)
-    };
+
+    if      target_el == EL1 then trap := ((if is_wfe then SCTLR_EL1.nTWE else SCTLR_EL1.nTWI) == 0)
+    else if target_el == EL2 then trap := ((if is_wfe then HCR_EL2.TWE else HCR_EL2.TWI) == 1)
+    else if target_el == EL3 then trap := ((if is_wfe then SCR_EL3.TWE else SCR_EL3.TWI) == 1)
+    else {assert(false,None); ()};
+
 
     if trap then
         AArch64_WFxTrap(target_el, is_wfe);
@@ -514,11 +515,12 @@ function forall Nat 'N, 'N IN {32,64}. unit effect {rreg,wreg} wSP ((),(bit['N])
   if PSTATE_SP == 0 then
     SP_EL0 := ZeroExtend(value)
   else
-    switch PSTATE_EL {
-      case EL0 -> SP_EL0 := ZeroExtend(value)
-      case EL1 -> SP_EL1 := ZeroExtend(value)
-      case EL2 -> SP_EL2 := ZeroExtend(value)
-      case EL3 -> SP_EL3 := ZeroExtend(value)
+    let pstate_el = PSTATE_EL in {
+      if      pstate_el == EL0 then SP_EL0 := ZeroExtend(value)
+      else if pstate_el == EL1 then SP_EL1 := ZeroExtend(value)
+      else if pstate_el == EL2 then SP_EL2 := ZeroExtend(value)
+      else if pstate_el == EL3 then SP_EL3 := ZeroExtend(value)
+      else assert(false,None); ();
     }
 }
 
@@ -530,11 +532,12 @@ function bit['N] effect {rreg} rSP () =
   if PSTATE_SP == 0 then
     mask(SP_EL0)
   else
-    switch PSTATE_EL {
-      case EL0 -> mask(SP_EL0)
-      case EL1 -> mask(SP_EL1)
-      case EL2 -> mask(SP_EL2)
-      case EL3 -> mask(SP_EL3)
+    let pstate_el = PSTATE_EL in {
+      if      pstate_el == EL0 then mask(SP_EL0)
+      else if pstate_el == EL1 then mask(SP_EL1)
+      else if pstate_el == EL2 then mask(SP_EL2)
+      else if pstate_el == EL3 then mask(SP_EL3)
+      else {assert(false,None); mask(SP_EL3)}
     }
 }
 
@@ -600,12 +603,10 @@ function forall Nat 'N, 'N IN {8,16,32,64}. bit['N] effect {rreg} rX((reg_index)
 function bit[64] rELR((bit[2]) el) =
 {
   (bit[64]) r := 0; (* ARM: uninitialized *)
-  switch el {
-      case EL1 -> r := ELR_EL1
-      case EL2 -> r := ELR_EL2
-      case EL3 -> r := ELR_EL3
-      case _   -> Unreachable()
-  };
+  if      el == EL1 then r := ELR_EL1
+  else if el == EL2 then r := ELR_EL2
+  else if el == EL3 then r := ELR_EL3
+  else Unreachable();
   r;
 }
 
@@ -620,12 +621,10 @@ function bit[64] rELR'() =
 (** FUNCTION:SCTLRType SCTLR[bits(2) regime] *)
 
 function SCTLR_type effect {rreg} SCTLR ((bit[2]) regime) = {
-   switch regime {
-      case EL1 -> SCTLR_EL1
-      case EL2 -> SCTLR_EL2
-      case EL3 -> SCTLR_EL3
-      case _ -> {assert(false,Some("SCTLR_type unreachable")); SCTLR_EL1} (* ARM: Unreachabe() *)
-   }
+   if      regime == EL1 then SCTLR_EL1
+   else if regime == EL2 then SCTLR_EL2
+   else if regime == EL3 then SCTLR_EL3
+   else {assert(false,Some("SCTLR_type unreachable")); SCTLR_EL1} (* ARM: Unreachabe() *)
 }
 
 (** FUNCTION:SCTLRType SCTLR[] *)
@@ -798,7 +797,10 @@ function forall Nat 'M, Nat 'E, 'E IN {2,4,8,16,32,64}. (bit['M],bit['M]) Decode
 
   (* Compute log2 of element size *)
   (* 2^len must be in range [2, 'M] *)
-  ([|6|]) len := switch HighestSetBit([immN]:(NOT(imms))) { case -1 -> { assert (false,None); 0; } case ([|6|]) c -> c };
+  ([|6|]) len := switch HighestSetBit([immN]:(NOT(imms))) {
+    case None -> { assert (false,Some("DecodeBitMasks: HighestSetBit returned None")); 0; }
+    case (Some(c)) -> c
+  };
   if len < 1 then ReservedValue();
   assert((M >= lsl(1, len)),None);
 
diff --git a/arm/armV8_common_lib.sail b/arm/armV8_common_lib.sail
index 84332c71..1aa55992 100644
--- a/arm/armV8_common_lib.sail
+++ b/arm/armV8_common_lib.sail
@@ -49,10 +49,10 @@ function boolean DoubleLockStatus() =
 typedef signalValue =
   enumerate {LOw; HIGH}
 
-val extern unit -> signalValue effect pure signalDBGEN
-val extern unit -> signalValue effect pure signalNIDEN
-val extern unit -> signalValue effect pure signalSPIDEN
-val extern unit -> signalValue effect pure signalSPNIDEN
+function signalValue signalDBGEN () = not_implemented_extern("signalDBGEN")
+function signalValue signelNIDEN () = not_implemented_extern("signalNIDEN")
+function signalValue signalSPIDEN () = not_implemented_extern("signalSPIDEN")
+function signalValue signalDPNIDEN () = not_implemented_extern("signalSPNIDEN")
 
 (** FUNCTION:shared/debug/authentication/ExternalInvasiveDebugEnabled *)
 
@@ -202,8 +202,10 @@ function forall Nat 'N. [|'N|] CountLeadingSignBits((bit['N]) x) =
 (** FUNCTION:integer CountLeadingZeroBits(bits(N) x) *)
 
 function forall Nat 'N. [|'N|] CountLeadingZeroBits((bit['N]) x) =
-  length(x) - 1 - HighestSetBit(x)
-
+  switch HighestSetBit(x) {
+    case None -> length(x)
+    case (Some(n)) -> length(x) - 1 - n
+  }
 (** FUNCTION:bits(N) Extend(bits(M) x, integer N, boolean unsigned) *)
 
 val forall Nat 'N, Nat 'M, 'M <= 'N. (implicit<'N>,bit['M],bit) -> bit['N] effect pure Extend
@@ -212,7 +214,7 @@ function forall Nat 'N, Nat 'M. bit['N] Extend (x, unsigned) =
 
 (** FUNCTION:integer HighestSetBit(bits(N) x) *)
 
-function forall Nat 'N. [|-1:('N + -1)|] HighestSetBit((bit['N]) x) = {
+function forall Nat 'N. option<[|0:('N + -1)|]> HighestSetBit((bit['N]) x) = {
   let N = (length(x)) in {
   ([|('N + -1)|]) result := 0;
   (bool) break := false;
@@ -222,7 +224,7 @@ function forall Nat 'N. [|-1:('N + -1)|] HighestSetBit((bit['N]) x) = {
       break := true;
     };
 
-  if break then result else -1;
+  if break then Some(result) else None;
 }}
 
 (** FUNCTION:integer Int(bits(N) x, boolean unsigned) *)
@@ -733,27 +735,28 @@ function forall Nat 'N, 'N IN {32,64}. unit effect {rreg,wreg} BranchTo((bit['N]
   } else {
     assert(( length(target) == 64 & ~(UsingAArch32()) ), None);
     (* Remove the tag bits from tagged target *)
-    switch PSTATE_EL {
-      case EL0 -> {
+    let pstate_el = PSTATE_EL in {
+      if pstate_el == EL0 then {
         if target'[55] == 1 & TCR_EL1.TBI1 == 1 then
           target'[63..56] := 0b11111111;
         if target'[55] == 0 & TCR_EL1.TBI0 == 1 then
           target'[63..56] := 0b00000000;
       }
-      case EL1 -> {
+      else if pstate_el == EL1 then {
         if target'[55] == 1 & TCR_EL1.TBI1 == 1 then
           target'[63..56] := 0b11111111;
         if target'[55] == 0 & TCR_EL1.TBI0 == 1 then
           target'[63..56] := 0b00000000;
       }
-      case EL2 -> {
+      else if pstate_el == EL2 then {
         if TCR_EL2.TBI == 1 then
           target'[63..56] := 0b00000000;
       }
-      case EL3 -> {
+      else if pstate_el == EL3 then {
         if TCR_EL3.TBI == 1 then
           target'[63..56] := 0b00000000;
       }
+      else assert(false,None)
     };
     _PC := target';
   };
@@ -768,7 +771,7 @@ function unit effect pure Hint_Branch((BranchType) hint) =
 }
 
 (** FUNCTION:shared/functions/registers/ResetExternalDebugRegisters *)
-val extern boolean -> unit effect pure ResetExternalDebugRegisters
+function unit ResetExternalDebugRegisters ((boolean) b) = not_implemented_extern("ResetExternalDebugRegisters")
 (** FUNCTION:shared/functions/registers/ThisInstrAddr *)
 
 val forall Nat 'N. implicit<'N> -> bit['N] effect {rreg} ThisInstrAddr
@@ -798,11 +801,11 @@ function bit[32] rSPSR() =
       otherwise          Unreachable();
     *)
   } else {
-    switch PSTATE_EL {
-      case EL1 -> result := SPSR_EL1
-      case EL2 -> result := SPSR_EL2
-      case EL3 -> result := SPSR_EL3
-      case _   -> Unreachable()
+    let pstate_el = PSTATE_EL in {
+      if      pstate_el == EL1 then result := SPSR_EL1
+      else if pstate_el == EL2 then result := SPSR_EL2
+      else if pstate_el == EL3 then result := SPSR_EL3
+      else Unreachable()
     };
   };
 
@@ -810,7 +813,7 @@ function bit[32] rSPSR() =
 }
 
 (** FUNCTION:shared/functions/system/ClearEventRegister *)
-val extern unit -> unit effect pure ClearEventRegister
+function unit ClearEventRegister () = not_implemented_extern("ClearEventRegister")
 (** FUNCTION:boolean ConditionHolds(bits(4) cond) *)
 
 function boolean effect {rreg} ConditionHolds((bit[4]) _cond) =
@@ -843,9 +846,9 @@ function boolean ELUsingAArch32((bit[2]) el) =
     false (* ARM: ELStateUsingAArch32(el, IsSecureBelowEL3()) *) (* FIXME: implement *)
 
 (** FUNCTION:shared/functions/system/EventRegisterSet *)
-val extern unit -> unit effect pure EventRegisterSet
+function unit EventRegisterSet () = not_implemented_extern("EventRegisterSet")
 (** FUNCTION:shared/functions/system/EventRegistered *)
-val extern unit -> boolean effect pure EventRegistered
+function boolean EventRegistered () = not_implemented_extern("EventRegistered")
 (** FUNCTION:shared/functions/system/HaveAArch32EL *)
 
 function boolean HaveAArch32EL((bit[2]) el) =
@@ -879,12 +882,11 @@ function boolean HaveEL((bit[2]) el) =
     true (*EL1 and EL0 must exist*)
   else {
 
-  switch el {
-    case EL2 -> IMPLEMENTATION_DEFINED.HaveEL2
-    case EL3 -> IMPLEMENTATION_DEFINED.HaveEL3
-    case _ -> {assert (false,None); false;}
+  if      el == EL2 then IMPLEMENTATION_DEFINED.HaveEL2
+  else if el == EL3 then IMPLEMENTATION_DEFINED.HaveEL3
+  else {assert (false,None); false};
   };
-}}
+}
 
 (** FUNCTION:boolean HighestELUsingAArch32() *)
 
@@ -902,7 +904,7 @@ function unit Hint_Yield() = ()
 val extern unit -> unit effect {barr} InstructionSynchronizationBarrier
 (** FUNCTION:shared/functions/system/InterruptPending *)
 
-val extern unit -> boolean effect pure InterruptPending
+function boolean InterruptPending () = not_implemented_extern("InterruptPending")
 
 (** FUNCTION:boolean IsSecure() *)
 
@@ -970,9 +972,9 @@ function boolean UsingAArch32() =
 }
 
 (** FUNCTION:shared/functions/system/WaitForEvent *)
-val extern unit -> unit effect pure WaitForEvent
+function unit WaitForEvent () = not_implemented_extern("WaitForEvent")
 (** FUNCTION:shared/functions/system/WaitForInterrupt *)
-val extern unit -> unit effect pure WaitForInterrupt
+function unit WaitForInterrupt () = not_implemented_extern("WaitForInterrupt")
 (** FUNCTION:shared/translation/translation/PAMax *)
 
 function uinteger PAMax() =
diff --git a/arm/armV8_lib.h.sail b/arm/armV8_lib.h.sail
index e8e979c8..6c8f9aaa 100644
--- a/arm/armV8_lib.h.sail
+++ b/arm/armV8_lib.h.sail
@@ -166,7 +166,7 @@ val forall Nat 'N. implicit<'N> -> bit['N] effect pure Ones
 val forall Nat 'N, Nat 'M. bit['N] -> [:'M:] effect pure UInt
 (* val forall Nat 'N, Nat 'M, Nat 'K, 'M = 'N + -1, 'K = 2**'M. bit['N] -> [|'K * -1:'K + -1|] effect pure SInt *)
 val forall Nat 'N, Nat 'M. bit['N] -> [:'M:] effect pure SInt
-val forall Nat 'N. bit['N+1] -> [|-1:'N|] effect pure HighestSetBit
+val forall Nat 'N. bit['N+1] -> option<[|0:'N + -1|]> effect pure HighestSetBit
 val forall Nat 'N. bit['N] -> [|'N|] effect pure CountLeadingZeroBits
 val unit -> boolean effect {rreg} IsSecure
 val unit -> boolean effect {rreg} IsSecureBelowEL3
diff --git a/arm/armV8_pstate.sail b/arm/armV8_pstate.sail
index 5be50b19..da707b44 100644
--- a/arm/armV8_pstate.sail
+++ b/arm/armV8_pstate.sail
@@ -43,14 +43,14 @@ register alias PSTATE_F   = DAIF.F  (* FIQ mask bit *)
 (* register alias PSTATE_SS  =         (* Software step bit *) *)
 (* register alias PSTATE_IL  =         (* Illegal execution state bit *) *)
 register alias PSTATE_EL  = CurrentEL.EL (* Exception Level *)
-register (bit) PSTATE_nRW           (* not Register Width: 0=64, 1=32 *)
+register (bit[1]) PSTATE_nRW           (* not Register Width: 0=64, 1=32 *)
 register alias PSTATE_SP = SPSel.SP (* Stack pointer select: 0=SP0, 1=SPx [AArch64 only] *) (* TODO: confirm this *)
 (* register alias PSTATE_Q   =         (* Cumulative saturation flag         [AArch32 only] *) *)
 (* register alias PSTATE_GE  =         (* Greater than or Equal flags        [AArch32 only] *) *)
 (* register alias PSTATE_IT  =         (* If-then bits, RES0 in CPSR         [AArch32 only] *) *)
 (* register alias PSTATE_J   =         (* J bit, RES0 in CPSR                [AArch32 only, RES0 in ARMv8] *) *)
 (* register alias PSTATE_T   =         (* T32 bit, RES0 in CPSR              [AArch32 only] *) *)
-register (bit) PSTATE_E             (* Endianness bit                     [AArch32 only] *)
+register (bit[1]) PSTATE_E             (* Endianness bit                     [AArch32 only] *)
 register (bit[5]) PSTATE_M          (* Mode field                         [AArch32 only] *)