From 8bf2ac5f87c579917b12a505bd8642f8a4656ac0 Mon Sep 17 00:00:00 2001 From: Ben Marshall Date: Mon, 3 Aug 2020 11:56:08 +0100 Subject: [PATCH] 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 | 2 +- doc/tex/sec-scalar-sha2.tex | 6 +++--- doc/tex/sec-scalar-sm3.tex | 2 +- doc/tex/sec-scalar-sm4.tex | 2 +- sail/riscv_insts_crypto.sail | 12 ++++-------- sail/riscv_insts_crypto_rv32.sail | 9 ++------- sail/riscv_insts_crypto_rv64.sail | 16 +++++----------- 7 files changed, 17 insertions(+), 32 deletions(-) diff --git a/doc/tex/sec-scalar-aes.tex b/doc/tex/sec-scalar-aes.tex index f3a0c6cf..45a07e57 100644 --- a/doc/tex/sec-scalar-aes.tex +++ b/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. } diff --git a/doc/tex/sec-scalar-sha2.tex b/doc/tex/sec-scalar-sha2.tex index 0c36d603..3aaa72c4 100644 --- a/doc/tex/sec-scalar-sha2.tex +++ b/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} diff --git a/doc/tex/sec-scalar-sm3.tex b/doc/tex/sec-scalar-sm3.tex index 2a5b97d7..eb282b20 100644 --- a/doc/tex/sec-scalar-sm3.tex +++ b/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} diff --git a/doc/tex/sec-scalar-sm4.tex b/doc/tex/sec-scalar-sm4.tex index d5eacf0c..c16bb901 100644 --- a/doc/tex/sec-scalar-sm4.tex +++ b/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} diff --git a/sail/riscv_insts_crypto.sail b/sail/riscv_insts_crypto.sail index 68f58e0f..f5ba13ad 100644 --- a/sail/riscv_insts_crypto.sail +++ b/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,8 +101,8 @@ 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 { @@ -113,6 +110,7 @@ function crypto_sm3 (op , rd , rs1 ) = { P1 => r1 ^ rol32(r1 ,0x0E) ^ rol32(r1 ,0x17) }; X(rd) = EXTZ(result); + RETIRE_SUCCESS } /* --- specification snippet end --- */ @@ -120,13 +118,11 @@ function crypto_sm3 (op , rd , rs1 ) = { /* 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 } diff --git a/sail/riscv_insts_crypto_rv32.sail b/sail/riscv_insts_crypto_rv32.sail index ca3b97a0..cd3baf05 100644 --- a/sail/riscv_insts_crypto_rv32.sail +++ b/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 } diff --git a/sail/riscv_insts_crypto_rv64.sail b/sail/riscv_insts_crypto_rv64.sail index f4f5dc75..e618f228 100644 --- a/sail/riscv_insts_crypto_rv64.sail +++ b/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 }