spec,sail: pacify sail type checker some more.

- Fix the line numbers used to get source code into spec.

- See #20

 On branch dev/next-release
 Your branch is up-to-date with 'origin/dev/next-release'.

 Changes to be committed:
	modified:   doc/tex/sec-scalar-aes.tex
	modified:   doc/tex/sec-scalar-sha2.tex
	modified:   doc/tex/sec-scalar-sm3.tex
	modified:   doc/tex/sec-scalar-sm4.tex
	modified:   sail/riscv_insts_crypto.sail
	modified:   sail/riscv_insts_crypto_rv32.sail
	modified:   sail/riscv_insts_crypto_rv64.sail

 Changes not staged for commit:
	modified:   extern/riscv-gnu-toolchain (modified content)
	modified:   extern/riscv-isa-sim (modified content)

doc/tex/sec-scalar-aes.tex

@@ -158,7 +158,7 @@ \subsubsection{RV64 Instructions}
 \end{figure}
 
 \begin{figure}[h!]
-\lstinputlisting[language=sail,firstline=71,lastline=109]{../sail/riscv_insts_crypto_rv64.sail}
+\lstinputlisting[language=sail,firstline=72,lastline=110]{../sail/riscv_insts_crypto_rv64.sail}
 \caption{
 SAIL specification for the RV64 AES instructions.
 }

doc/tex/sec-scalar-sha2.tex

@@ -26,7 +26,7 @@ \subsubsection{SHA-256 Instructions}
 \ref{fig:sail:ssha256}.
 
 \begin{figure}[h]
-\lstinputlisting[language=sail,firstline=45,lastline=55]{../sail/riscv_insts_crypto.sail}
+\lstinputlisting[language=sail,firstline=46,lastline=56]{../sail/riscv_insts_crypto.sail}
 \caption{SAIL specification for the scalar RV32/RV64 SHA256 instructions.}
 \label{fig:sail:ssha256}
 \end{figure}
@@ -86,13 +86,13 @@ \subsubsection{SHA-512 Instructions}
 }
 
 \begin{figure}[h]
-\lstinputlisting[language=sail,firstline=142,lastline=155]{../sail/riscv_insts_crypto_rv32.sail}
+\lstinputlisting[language=sail,firstline=143,lastline=156]{../sail/riscv_insts_crypto_rv32.sail}
 \caption{SAIL specification for the scalar RV32 SHA512 instructions.}
 \label{fig:sail:ssha512:rv32}
 \end{figure}
 
 \begin{figure}[h]
-\lstinputlisting[language=sail,firstline=121,lastline=131]{../sail/riscv_insts_crypto_rv64.sail}
+\lstinputlisting[language=sail,firstline=152,lastline=162]{../sail/riscv_insts_crypto_rv64.sail}
 \caption{SAIL specification for the scalar RV64 SHA512 instructions.}
 \label{fig:sail:ssha512:rv64}
 \end{figure}

doc/tex/sec-scalar-sm3.tex

@@ -21,7 +21,7 @@ \subsection{Scalar SM3 Acceleration}
 \ref{fig:sail:sm3}.
 
 \begin{figure}[h]
-\lstinputlisting[language=sail,firstline=108,lastline=116]{../sail/riscv_insts_crypto.sail}
+\lstinputlisting[language=sail,firstline=106,lastline=114]{../sail/riscv_insts_crypto.sail}
 \caption{SAIL specification for the scalar RV32/RV64 SM3 instructions.}
 \label{fig:sail:sm3}
 \end{figure}

doc/tex/sec-scalar-sm4.tex

@@ -60,7 +60,7 @@ \subsection{Scalar SM4 Acceleration}
 }
 
 \begin{figure}[h]
-\lstinputlisting[language=sail,firstline=168,lastline=191]{../sail/riscv_insts_crypto.sail}
+\lstinputlisting[language=sail,firstline=164,lastline=187]{../sail/riscv_insts_crypto.sail}
 \caption{SAIL specification for the SM4 instructions.}
 \label{fig:sail:sm4}
 \end{figure}

sail/riscv_insts_crypto.sail

@@ -41,8 +41,8 @@ mapping clause assembly = SSHA256_SIG1 (rs1,rd) <-> "ssha256.sig1" ^ spc() ^ reg
 mapping clause assembly = SSHA256_SUM0 (rs1,rd) <-> "ssha256.sum0" ^ spc() ^ reg_name(rd) ^ sep() ^ reg_name(rs1)
 mapping clause assembly = SSHA256_SUM1 (rs1,rd) <-> "ssha256.sum1" ^ spc() ^ reg_name(rd) ^ sep() ^ reg_name(rs1)
 
+val      crypto_ssha256 : (ssha256_op, regidx, regidx) -> Retired effect {escape,rreg,wreg}
 /* --- specification snippet begin --- */
-val      crypto_ssha256 : (ssha256_op, regidx, regidx) -> unit
 function crypto_ssha256   (op        , rd    , rs1   ) =  {
   let inb    : bits(32) = X(rs1)[31..0];
   let result : bits(32) = match op {
@@ -52,28 +52,25 @@ function crypto_ssha256   (op        , rd    , rs1   ) =  {
     SHA256_SUM1 => ror32(inb ,0x06) ^ ror32(inb, 0x0B) ^ ror32(inb,0x19)
   };
   X(rd) = EXTZ(result);
+  RETIRE_SUCCESS
 }
 /* --- specification snippet end --- */
 
 /* Execution clauses for the SHA256 instructions. */
 function clause execute (SSHA256_SIG0 (rs1,rd)) = {
     crypto_ssha256(SHA256_SIG0, rd, rs1);
-    RETIRE_SUCCESS
 }
 
 function clause execute (SSHA256_SIG1 (rs1,rd)) = {
     crypto_ssha256(SHA256_SIG1, rd, rs1);
-    RETIRE_SUCCESS
 }
 
 function clause execute (SSHA256_SUM0 (rs1,rd)) = {
     crypto_ssha256(SHA256_SUM0, rd, rs1);
-    RETIRE_SUCCESS
 }
 
 function clause execute (SSHA256_SUM1 (rs1,rd)) = {
     crypto_ssha256(SHA256_SUM1, rd, rs1);
-    RETIRE_SUCCESS
 }
 
 /*
@@ -104,29 +101,28 @@ mapping clause assembly =  SSM3_P1 (rs1,rd) <->
     "ssm3.p1" ^ spc() ^ reg_name(rd) ^ sep() ^ reg_name(rs1)
 
 
+val      crypto_sm3 : (ssm3_op, regidx, regidx) -> Retired effect {escape,rreg,wreg}
 /* --- specification snippet begin --- */
-val      crypto_sm3 : (ssm3_op, regidx, regidx) -> unit
 function crypto_sm3   (op     , rd    , rs1   ) =  {
   let r1    : bits(32) = X(rs1)[31..0];
   let result  : bits(32) = match op {
     P0  => r1 ^ rol32(r1 ,0x09) ^ rol32(r1 ,0x11),
     P1  => r1 ^ rol32(r1 ,0x0E) ^ rol32(r1 ,0x17)
   };
   X(rd)       = EXTZ(result);
+  RETIRE_SUCCESS
 }
 /* --- specification snippet end --- */
 
 
 /* Execute clause for ssm3.p0 */
 function clause execute ( SSM3_P0 (rs1,rd)) = {
   crypto_sm3(P0, rd, rs1);
-  RETIRE_SUCCESS
 }
 
 /* Execute clause for ssm3.p1 */
 function clause execute ( SSM3_P1 (rs1,rd)) = {
   crypto_sm3(P1, rd, rs1);
-  RETIRE_SUCCESS
 }
 
 

sail/riscv_insts_crypto_rv32.sail

@@ -138,8 +138,8 @@ mapping clause assembly = SSHA512_SUM1R (rs2,rs1,rd) <->
     "ssha512.sum1r" ^ spc() ^ reg_name(rd) ^ sep() ^ reg_name(rs1) ^ sep() ^ reg_name(rs2)
 
 
+val      crypto_ssha512_rv32 :(ssha512_rv32_op, regidx, regidx, regidx) -> Retired effect {escape, rreg, wreg}
 /* --- specification snippet begin --- */
-val      crypto_ssha512_rv32 :(ssha512_rv32_op, regidx, regidx, regidx) -> unit
 function crypto_ssha512_rv32  (op             , rd    , rs1   , rs2   ) = {
   let r1     : bits(32) = X(rs1)[31..0];
   let r2     : bits(32) = X(rs2)[31..0];
@@ -152,6 +152,7 @@ function crypto_ssha512_rv32  (op             , rd    , rs1   , rs2   ) = {
     SHA512_SUM1R => (r1<<23) ^ (r1<<14) ^ (r1>>18) ^ (r2<< 9) ^(r2<<18) ^(r2<<14)
   };
   X(rd) = EXTZ(result);
+  RETIRE_SUCCESS
 }
 /* --- specification snippet end --- */
 
@@ -162,32 +163,26 @@ function crypto_ssha512_rv32  (op             , rd    , rs1   , rs2   ) = {
 
 function clause execute (  SSHA512_SIG0L (rs2,rs1,rd)) = {
   crypto_ssha512_rv32(SHA512_SIG0L, rd, rs1, rs2);
-  RETIRE_SUCCESS
 }
 
 function clause execute (  SSHA512_SIG0H (rs2,rs1,rd)) = {
   crypto_ssha512_rv32(SHA512_SIG0H, rd, rs1, rs2);
-  RETIRE_SUCCESS
 }
 
 function clause execute (  SSHA512_SIG1L (rs2,rs1,rd)) = {
   crypto_ssha512_rv32(SHA512_SIG1L, rd, rs1, rs2);
-  RETIRE_SUCCESS
 }
 
 function clause execute (  SSHA512_SIG1H (rs2,rs1,rd)) = {
   crypto_ssha512_rv32(SHA512_SIG1H, rd, rs1, rs2);
-  RETIRE_SUCCESS
 }
 
 function clause execute (  SSHA512_SUM0R (rs2,rs1,rd)) = {
   crypto_ssha512_rv32(SHA512_SUM0R, rd, rs1, rs2);
-  RETIRE_SUCCESS
 }
 
 function clause execute (  SSHA512_SUM1R (rs2,rs1,rd)) = {
   crypto_ssha512_rv32(SHA512_SUM1R, rd, rs1, rs2);
-  RETIRE_SUCCESS
 }
 
 

sail/riscv_insts_crypto_rv64.sail

@@ -67,8 +67,8 @@ mapping clause assembly =  SAES64_DECS (rs2,rs1,rd) <->
     "saes64.decs" ^ spc() ^ reg_name(rd) ^ sep() ^ reg_name(rs1) ^ sep() ^ reg_name(rs2)
 
 
+val      crypto_saes64 : (regidx, regidx, regidx, bool, bool) -> Retired effect {escape, rreg, wreg}
 /* --- specification snippet begin --- */
-val      crypto_saes64 : (regidx, regidx, regidx, bool, bool) -> unit
 function crypto_saes64   (rd    , rs1   , rs2   , enc , mix )  = {
   let sr : bits(128) = match enc {
     true  => aes_shift_rows_fwd(X(rs2)[63..0] @ X(rs1)[63..0]), /* Encrypt */
@@ -83,7 +83,8 @@ function crypto_saes64   (rd    , rs1   , rs2   , enc , mix )  = {
     (true,true ) => aes_mixcolumn_fwd(sb[63..32]) @ aes_mixcolumn_fwd(sb[31..0]),
     (true,false) => aes_mixcolumn_inv(sb[63..32]) @ aes_mixcolumn_inv(sb[31..0]),
     (false, _  ) => sb
-  }
+  };
+  RETIRE_SUCCESS
 }
 
 function clause execute (SAES64_KS1 (rcon,rs1,rd)) = {
@@ -111,22 +112,18 @@ function clause execute (SAES64_IMIX (rs1,rd)) = {
 
 function clause execute (SAES64_ENCSM (rs2,rs1,rd)) = {
     crypto_saes64(rd, rs1, rs2, true, true);
-    RETIRE_SUCCESS
 }
 
 function clause execute (SAES64_ENCS (rs2,rs1,rd)) = {
     crypto_saes64(rd, rs1, rs2, true, false);
-    RETIRE_SUCCESS
 }
 
 function clause execute (SAES64_DECSM (rs2,rs1,rd)) = {
     crypto_saes64(rd, rs1, rs2, false, true);
-    RETIRE_SUCCESS
 }
 
 function clause execute (SAES64_DECS (rs2,rs1,rd)) = {
     crypto_saes64(rd, rs1, rs2, false, false);
-    RETIRE_SUCCESS
 }
 
 /*
@@ -150,8 +147,8 @@ mapping clause assembly =    SSHA512_SUM0 (rs1,rd) <-> "ssha512.sum0" ^ spc() ^
 mapping clause assembly =    SSHA512_SUM1 (rs1,rd) <-> "ssha512.sum1" ^ spc() ^ reg_name(rd) ^ sep() ^ reg_name(rs1)
 
 
+val      crypto_ssha512_rv64 : (ssha512_rv64_op, regidx, regidx) -> Retired effect {escape, rreg, wreg}
 /* --- specification snippet begin --- */
-val      crypto_ssha512_rv64 : (ssha512_rv64_op, regidx, regidx) -> unit
 function crypto_ssha512_rv64   (op             , rd    , rs1   ) =  {
   let inb    : bits(64) = X(rs1)[63..0];
   let result : bits(64) = match op {
@@ -161,27 +158,24 @@ function crypto_ssha512_rv64   (op             , rd    , rs1   ) =  {
     SHA512_SUM1 => ror64(inb, 0x0E) ^ ror64(inb, 0x12) ^ ror64(inb ,0x29)
   };
   X(rd) = EXTZ(result);
+  RETIRE_SUCCESS
 }
 /* --- specification snippet end --- */
 
 
 function clause execute (   SSHA512_SIG0 (rs1,rd)) = {
     crypto_ssha512_rv64(SHA512_SIG0, rd, rs1);
-    RETIRE_SUCCESS
 }
 
 function clause execute (   SSHA512_SIG1 (rs1,rd)) = {
     crypto_ssha512_rv64(SHA512_SIG1, rd, rs1);
-    RETIRE_SUCCESS
 }
 
 function clause execute (   SSHA512_SUM0 (rs1,rd)) = {
     crypto_ssha512_rv64(SHA512_SUM0, rd, rs1);
-    RETIRE_SUCCESS
 }
 
 function clause execute (   SSHA512_SUM1 (rs1,rd)) = {
     crypto_ssha512_rv64(SHA512_SUM1, rd, rs1);
-    RETIRE_SUCCESS
 }