Skip to content

Commit

Permalink
scalar-crypto: Initial commit of 1.0.0-rc2 spec work. (#99)
Browse files Browse the repository at this point in the history 
Merged scalar-crypto pull request #99  of 1.0.0-rc2 spec work from Ben Marshall. See #99.
  • Loading branch information
@ben-marshall
ben-marshall committed Oct 18, 2021
1 parent 9f71c75 commit 1c7584b
Show file tree
Hide file tree
Showing 16 changed files with 997 additions and 2 deletions.
5 changes: 4 additions & 1 deletion Makefile
View file
Expand Up @@ -25,6 +25,8 @@ SAIL_DEFAULT_INST += riscv_insts_fext.sail riscv_insts_cfext.sail
ifeq ($(ARCH),RV64)
SAIL_DEFAULT_INST += riscv_insts_dext.sail riscv_insts_cdext.sail
endif
SAIL_DEFAULT_INST += riscv_insts_zkn.sail
SAIL_DEFAULT_INST += riscv_insts_zks.sail

SAIL_SEQ_INST = $(SAIL_DEFAULT_INST) riscv_jalr_seq.sail
SAIL_RMEM_INST = $(SAIL_DEFAULT_INST) riscv_jalr_rmem.sail riscv_insts_rmem.sail
Expand Down Expand Up @@ -63,7 +65,8 @@ SAIL_ARCH_SRCS = $(PRELUDE)
SAIL_ARCH_SRCS += riscv_types_common.sail riscv_types_ext.sail riscv_types.sail
SAIL_ARCH_SRCS += riscv_vmem_types.sail $(SAIL_REGS_SRCS) $(SAIL_SYS_SRCS) riscv_platform.sail
SAIL_ARCH_SRCS += riscv_mem.sail $(SAIL_VM_SRCS)
SAIL_ARCH_RVFI_SRCS = $(PRELUDE) rvfi_dii.sail riscv_types_common.sail riscv_types_ext.sail riscv_types.sail riscv_vmem_types.sail $(SAIL_REGS_SRCS) $(SAIL_SYS_SRCS) riscv_platform.sail riscv_mem.sail $(SAIL_VM_SRCS)
SAIL_ARCH_RVFI_SRCS = $(PRELUDE) rvfi_dii.sail riscv_types_common.sail riscv_types_ext.sail riscv_types.sail riscv_vmem_types.sail $(SAIL_REGS_SRCS) $(SAIL_SYS_SRCS) riscv_platform.sail riscv_mem.sail $(SAIL_VM_SRCS) riscv_types_kext.sail
SAIL_ARCH_SRCS += riscv_types_kext.sail # Shared/common code for the cryptography extension.

SAIL_STEP_SRCS = riscv_step_common.sail riscv_step_ext.sail riscv_decode_ext.sail riscv_fetch.sail riscv_step.sail
RVFI_STEP_SRCS = riscv_step_common.sail riscv_step_rvfi.sail riscv_decode_ext.sail riscv_fetch_rvfi.sail riscv_step.sail
Expand Down
4 changes: 4 additions & 0 deletions c_emulator/riscv_platform.c
View file
Expand Up @@ -45,6 +45,10 @@ mach_bits plat_rom_base(unit u)
mach_bits plat_rom_size(unit u)
{ return rv_rom_size; }

// Provides entropy for the scalar cryptography extension.
mach_bits plat_get_16_random_bits()
{ return rv_16_random_bits(); }

mach_bits plat_clint_base(unit u)
{ return rv_clint_base; }

Expand Down
3 changes: 3 additions & 0 deletions c_emulator/riscv_platform.h
View file
Expand Up @@ -18,6 +18,9 @@ bool within_phys_mem(mach_bits, sail_int);
mach_bits plat_rom_base(unit);
mach_bits plat_rom_size(unit);

// Provides entropy for the scalar cryptography extension.
mach_bits plat_get_16_random_bits();

mach_bits plat_clint_base(unit);
mach_bits plat_clint_size(unit);

Expand Down
14 changes: 14 additions & 0 deletions c_emulator/riscv_platform_impl.c
View file
Expand Up @@ -19,6 +19,20 @@ uint64_t rv_ram_size = UINT64_C(0x4000000);
uint64_t rv_rom_base = UINT64_C(0x1000);
uint64_t rv_rom_size = UINT64_C(0x100);

// Provides entropy for the scalar cryptography extension.
uint64_t rv_16_random_bits(void) {
// This function can be changed to support deterministic sequences of
// pseudo-random bytes. This is useful for testing.
const char *name = "/dev/urandom";
FILE *f = fopen(name, "rb");
uint16_t val;
if (fread(&val, 2, 1, f) != 1) {
fprintf(stderr, "Unable to read 2 bytes from %s\n", name);
}
fclose(f);
return (uint64_t)val;
}

uint64_t rv_clint_base = UINT64_C(0x2000000);
uint64_t rv_clint_size = UINT64_C(0xc0000);

Expand Down
3 changes: 3 additions & 0 deletions c_emulator/riscv_platform_impl.h
View file
Expand Up @@ -22,6 +22,9 @@ extern uint64_t rv_ram_size;
extern uint64_t rv_rom_base;
extern uint64_t rv_rom_size;

// Provides entropy for the scalar cryptography extension.
extern uint64_t rv_16_random_bits(void);

extern uint64_t rv_clint_base;
extern uint64_t rv_clint_size;

Expand Down
4 changes: 4 additions & 0 deletions handwritten_support/0.11/riscv_extras.lem
View file
Expand Up @@ -143,6 +143,10 @@ val plat_term_read : forall 'a. Size 'a => unit -> bitvector 'a
let plat_term_read () = wordFromInteger 0
declare ocaml target_rep function plat_term_read = `Platform.term_read`

val plat_get_16_random_bits : forall 'a. Size 'a => unit -> bitvector 'a
let plat_get_16_random_bits () = wordFromInteger 0
declare ocaml target_rep function plat_get_16_random_bits = `Platform.get_16_random_bits`

val shift_bits_right : forall 'a 'b. Size 'a, Size 'b => bitvector 'a -> bitvector 'b -> bitvector 'a
let shift_bits_right v m = shiftr v (uint m)
val shift_bits_left : forall 'a 'b. Size 'a, Size 'b => bitvector 'a -> bitvector 'b -> bitvector 'a
Expand Down
4 changes: 4 additions & 0 deletions handwritten_support/riscv_extras.lem
View file
Expand Up @@ -211,6 +211,10 @@ val plat_term_read : forall 'a. Size 'a => unit -> bitvector 'a
let plat_term_read () = wordFromInteger 0
declare ocaml target_rep function plat_term_read = `Platform.term_read`

val plat_get_16_random_bits : forall 'a. Size 'a => unit -> bitvector 'a
let plat_get_16_random_bits () = wordFromInteger 0
declare ocaml target_rep function plat_get_16_random_bits = `Platform.get_16_random_bits`

val shift_bits_right : forall 'a 'b. Size 'a, Size 'b => bitvector 'a -> bitvector 'b -> bitvector 'a
let shift_bits_right v m = shiftr v (uint m)
val shift_bits_left : forall 'a 'b. Size 'a, Size 'b => bitvector 'a -> bitvector 'b -> bitvector 'a
Expand Down
22 changes: 22 additions & 0 deletions model/prelude.sail
View file
Expand Up @@ -248,6 +248,28 @@ function shift_right_arith32 (v : bits(32), shift : bits(5)) -> bits(32) =
let v64 : bits(64) = EXTS(v) in
(v64 >> shift)[31..0]

infix 7 >>>
infix 7 <<<

val rotate_bits_right : forall 'n 'm, 'm >= 0. (bits('n), bits('m)) -> bits('n)
function rotate_bits_right (v, n) =
(v >> n) | (v << (to_bits(length(n), length(v)) - n))

val rotate_bits_left : forall 'n 'm, 'm >= 0. (bits('n), bits('m)) -> bits('n)
function rotate_bits_left (v, n) =
(v << n) | (v >> (to_bits(length(n), length(v)) - n))

val rotater : forall 'm 'n, 'm >= 'n >= 0. (bits('m), atom('n)) -> bits('m)
function rotater (v, n) =
(v >> n) | (v << (length(v) - n))

val rotatel : forall 'm 'n, 'm >= 'n >= 0. (bits('m), atom('n)) -> bits('m)
function rotatel (v, n) =
(v << n) | (v >> (length(v) - n))

overload operator >>> = {rotate_bits_right, rotater}
overload operator <<< = {rotate_bits_left, rotatel}

/* helpers for mappings */

val spc : unit <-> string
Expand Down
4 changes: 3 additions & 1 deletion model/riscv_csr_map.sail
View file
Expand Up @@ -86,6 +86,8 @@ mapping clause csr_name_map = 0x044 <-> "uip"
mapping clause csr_name_map = 0x001 <-> "fflags"
mapping clause csr_name_map = 0x002 <-> "frm"
mapping clause csr_name_map = 0x003 <-> "fcsr"
/* user entropy source */
mapping clause csr_name_map = 0x015 <-> "seed"
/* counter/timers */
mapping clause csr_name_map = 0xC00 <-> "cycle"
mapping clause csr_name_map = 0xC01 <-> "time"
Expand Down Expand Up @@ -185,4 +187,4 @@ scattered function ext_read_CSR

/* returns new value (after legalisation) if the CSR is defined */
val ext_write_CSR : (csreg, xlenbits) -> option(xlenbits) effect {rreg, wreg}
scattered function ext_write_CSR
scattered function ext_write_CSR
6 changes: 6 additions & 0 deletions model/riscv_insts_zicsr.sail
View file
Expand Up @@ -158,6 +158,9 @@ function readCSR csr : csreg -> xlenbits = {
(0xC81, 32) => mtime[63 .. 32],
(0xC82, 32) => minstret[63 .. 32],

/* user mode: Zkr */
(0x015, _) => read_seed_csr(),

_ => /* check extensions */
match ext_read_CSR(csr) {
Some(res) => res,
Expand Down Expand Up @@ -235,6 +238,9 @@ function writeCSR (csr : csreg, value : xlenbits) -> unit = {
(0x144, _) => { mip = legalize_sip(mip, mideleg, value); Some(mip.bits()) },
(0x180, _) => { satp = legalize_satp(cur_Architecture(), satp, value); Some(satp) },

/* user mode: seed (entropy source). writes are ignored */
(0x015, _) => write_seed_csr(),

_ => ext_write_CSR(csr, value)
};
match res {
Expand Down

7 comments on commit 1c7584b

@marnovandermaas
Copy link

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

I'm getting the following error when compiling sail-riscv with this new commit and upstream sail2 (a6810cb5):

Internal error: Unreachable code (at "jib/jib_util.ml" line 672):
[model/riscv_insts_zkn.sail]:288:2-7
288 |  X(rd) = (post_sb ^ rc) @ (post_sb ^ rc);
    |  ^---^
    | Invalid ctyp unifiers %bv32 and %bv64
    |
    | Raised by primitive operation at Reporting.err_unreachable in file "reporting.ml", line 181, characters 18-43
    | Called from Reporting.unreachable in file "reporting.ml" (inlined), line 190, characters 8-35
    | Called from Jib_util.ctyp_unify in file "jib/jib_util.ml", line 672, characters 5-119
    | Called from Jib_compile.Make.compile_funcall.setup_arg in file "jib/jib_compile.ml", line 628, characters 52-88
    | Called from Stdlib__list.map2 in file "list.ml", line 131, characters 32-39
    | Called from Stdlib__list.map2 in file "list.ml", line 131, characters 48-60
    | Called from Jib_compile.Make.compile_funcall in file "jib/jib_compile.ml", line 634, characters 19-53
    | Called from Jib_compile.Make.compile_aexp in file "jib/jib_compile.ml", line 766, characters 32-53
    | Called from Jib_compile.Make.compile_block in file "jib/jib_compile.ml", line 1117, characters 32-52
    | Called from Jib_compile.Make.compile_aexp in file "jib/jib_compile.ml", line 963, characters 17-40
    | Called from Jib_compile.Make.compile_aexp in file "jib/jib_compile.ml", line 766, characters 32-53

@jrtc27
Copy link
Collaborator

@jrtc27 jrtc27 commented on 1c7584b Oct 21, 2021

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

That looks to be a Sail bug; it type-checked based on the assertion that xlen was 64 (and thus the code was dead for RV32 builds) but the backend is not remembering that.

@marnovandermaas
Copy link

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

I was getting this behavior with the head of sail, but not with the sail that is in the opam repository. I guess they might have broken this in between?

@jrtc27
Copy link
Collaborator

@jrtc27 jrtc27 commented on 1c7584b Oct 21, 2021

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Yeah, working on a reduced test case.

@jrtc27
Copy link
Collaborator

@jrtc27 jrtc27 commented on 1c7584b Oct 28, 2021

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Reduced, bisected and reported as rems-project/sail#156

@marnovandermaas
Copy link

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Thanks Jess!

@jrtc27
Copy link
Collaborator

@jrtc27 jrtc27 commented on 1c7584b Oct 29, 2021

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Now fixed

Please sign in to comment.