From 61e6bc97a7d5efb58f9b91738f1dd64404091137 Mon Sep 17 00:00:00 2001 From: Alasdair Armstrong Date: Wed, 7 Nov 2018 18:40:57 +0000 Subject: Move inline forall in function definitions * Previously we allowed the following bizarre syntax for a forall quantifier on a function: val foo(arg1: int('n), arg2: typ2) -> forall 'n, 'n >= 0. unit this commit changes this to the more sane: val foo forall 'n, 'n >= 2. (arg1: int('n), arg2: typ2) -> unit Having talked about it today, we could consider adding the syntax val foo where 'n >= 2. (arg1: int('n), arg2: typ2) -> unit which would avoid the forall (by implicitly quantifying variables in the constraint), and be slightly more friendly especially for documentation purposes. Only RISC-V used this syntax, so all uses of it there have been switched to the new style. * Second, there is a new (somewhat experimental) syntax for existentials, that is hopefully more readable and closer to minisail: val foo(x: int, y: int) -> int('m) with 'm >= 2 "type('n) with constraint" is equivalent to minisail: {'n: type | constraint} the type variables in typ are implicitly quantified, so this is equivalent to {'n, constraint. typ('n)} In order to make this syntax non-ambiguous we have to use == in constraints rather than =, but this is a good thing anyway because the previous situation where = was type level equality and == term level equality was confusing. Now all the type type-level and term-level operators can be consistent. However, to avoid breaking anything = is still allowed in non-with constraints, and produces a deprecated warning when parsed. --- riscv/riscv_mem.sail | 10 +++++----- riscv/riscv_platform.sail | 16 ++++++++-------- 2 files changed, 13 insertions(+), 13 deletions(-) (limited to 'riscv') diff --git a/riscv/riscv_mem.sail b/riscv/riscv_mem.sail index 2bcc9797..434f79d5 100644 --- a/riscv/riscv_mem.sail +++ b/riscv/riscv_mem.sail @@ -4,11 +4,11 @@ * to MMIO regions can be dispatched. */ -function is_aligned_addr (addr : xlenbits, width : atom('n)) -> forall 'n. bool = +function is_aligned_addr forall 'n. (addr : xlenbits, width : atom('n)) -> bool = unsigned(addr) % width == 0 // only used for actual memory regions, to avoid MMIO effects -function phys_mem_read(t : ReadType, addr : xlenbits, width : atom('n), aq : bool, rl: bool, res : bool) -> forall 'n, 'n >= 0. MemoryOpResult(bits(8 * 'n)) = +function phys_mem_read forall 'n, 'n >= 0. (t : ReadType, addr : xlenbits, width : atom('n), aq : bool, rl: bool, res : bool) -> MemoryOpResult(bits(8 * 'n)) = match (t, __RISCV_read(addr, width, aq, rl, res)) { (Instruction, None()) => MemException(E_Fetch_Access_Fault), (Data, None()) => MemException(E_Load_Access_Fault), @@ -16,7 +16,7 @@ function phys_mem_read(t : ReadType, addr : xlenbits, width : atom('n), aq : boo MemValue(v) } } -function checked_mem_read(t : ReadType, addr : xlenbits, width : atom('n), aq : bool, rl : bool, res: bool) -> forall 'n, 'n > 0. MemoryOpResult(bits(8 * 'n)) = +function checked_mem_read forall 'n, 'n > 0. (t : ReadType, addr : xlenbits, width : atom('n), aq : bool, rl : bool, res: bool) -> MemoryOpResult(bits(8 * 'n)) = /* treat MMIO regions as not executable for now. TODO: this should actually come from PMP/PMA. */ if t == Data & within_mmio_readable(addr, width) then mmio_read(addr, width) @@ -89,13 +89,13 @@ function mem_write_ea (addr, width, aq, rl, con) = { } // only used for actual memory regions, to avoid MMIO effects -function phys_mem_write(addr : xlenbits, width : atom('n), data: bits(8 * 'n)) -> forall 'n. MemoryOpResult(bool) = { +function phys_mem_write forall 'n. (addr : xlenbits, width : atom('n), data: bits(8 * 'n)) -> MemoryOpResult(bool) = { print("mem[" ^ BitStr(addr) ^ "] <- " ^ BitStr(data)); MemValue(__RISCV_write(addr, width, data)) } // dispatches to MMIO regions or physical memory regions depending on physical memory map -function checked_mem_write(addr : xlenbits, width : atom('n), data: bits(8 * 'n)) -> forall 'n, 'n > 0. MemoryOpResult(bool) = +function checked_mem_write forall 'n, 'n > 0. (addr : xlenbits, width : atom('n), data: bits(8 * 'n)) -> MemoryOpResult(bool) = if within_mmio_writable(addr, width) then mmio_write(addr, width, data) else if within_phys_mem(addr, width) diff --git a/riscv/riscv_platform.sail b/riscv/riscv_platform.sail index 3020d23d..25b09bcd 100644 --- a/riscv/riscv_platform.sail +++ b/riscv/riscv_platform.sail @@ -47,7 +47,7 @@ function phys_mem_segments() = /* Physical memory map predicates */ -function within_phys_mem(addr : xlenbits, width : atom('n)) -> forall 'n. bool = { +function within_phys_mem forall 'n. (addr : xlenbits, width : atom('n)) -> bool = { let ram_base = plat_ram_base (); let rom_base = plat_rom_base (); let ram_size = plat_ram_size (); @@ -70,14 +70,14 @@ function within_phys_mem(addr : xlenbits, width : atom('n)) -> forall 'n. bool = } } -function within_clint(addr : xlenbits, width : atom('n)) -> forall 'n. bool = +function within_clint forall 'n. (addr : xlenbits, width : atom('n)) -> bool = plat_clint_base() <=_u addr & (addr + sizeof('n)) <=_u (plat_clint_base() + plat_clint_size()) -function within_htif_writable(addr : xlenbits, width : atom('n)) -> forall 'n. bool = +function within_htif_writable forall 'n. (addr : xlenbits, width : atom('n)) -> bool = plat_htif_tohost() == addr -function within_htif_readable(addr : xlenbits, width : atom('n)) -> forall 'n. bool = +function within_htif_readable forall 'n. (addr : xlenbits, width : atom('n)) -> bool = plat_htif_tohost() == addr /* CLINT (Core Local Interruptor), based on Spike. */ @@ -238,20 +238,20 @@ function htif_tick() = { /* Top-level MMIO dispatch */ -function within_mmio_readable(addr : xlenbits, width : atom('n)) -> forall 'n. bool = +function within_mmio_readable forall 'n. (addr : xlenbits, width : atom('n)) -> bool = within_clint(addr, width) | (within_htif_readable(addr, width) & 1 <= 'n) -function within_mmio_writable(addr : xlenbits, width : atom('n)) -> forall 'n. bool = +function within_mmio_writable forall 'n. (addr : xlenbits, width : atom('n)) -> bool = within_clint(addr, width) | (within_htif_writable(addr, width) & 'n <= 8) -function mmio_read(addr : xlenbits, width : atom('n)) -> forall 'n, 'n > 0. MemoryOpResult(bits(8 * 'n)) = +function mmio_read forall 'n, 'n > 0. (addr : xlenbits, width : atom('n)) -> MemoryOpResult(bits(8 * 'n)) = if within_clint(addr, width) then clint_load(addr, width) else if within_htif_readable(addr, width) & (1 <= 'n) then htif_load(addr, width) else MemException(E_Load_Access_Fault) -function mmio_write(addr : xlenbits, width : atom('n), data: bits(8 * 'n)) -> forall 'n, 'n > 0. MemoryOpResult(bool) = +function mmio_write forall 'n, 'n > 0. (addr : xlenbits, width : atom('n), data: bits(8 * 'n)) -> MemoryOpResult(bool) = if within_clint(addr, width) then clint_store(addr, width, data) else if within_htif_writable(addr, width) & 'n <= 8 -- cgit v1.2.3