diff options
| author | Alasdair Armstrong | 2019-05-13 18:03:35 +0100 |
|---|---|---|
| committer | Alasdair Armstrong | 2019-05-14 15:13:29 +0100 |
| commit | 41e6fe10e7d28193fa62711fcdad797b1f0103a0 (patch) | |
| tree | 0113597f0c1b5ba909028f576a6a51c8dbead6ac /lib | |
| parent | 7257b23239a3f8d6a45f973b9d953b31772abe06 (diff) | |
Add feature that allows functions to require type variables are constant
can now write e.g.
forall (constant 'n : Int) rather than forall ('n: Int)
which requires 'n to be a constant integer value whenever the function
is called. I added this to the 'addrsize variable on memory
reads/writes to absolutely guarantee in the SMT generation that we
don't have to worry about the address being a variable length
bitvector.
Diffstat (limited to 'lib')
| -rw-r--r-- | lib/regfp.sail | 9 |
1 files changed, 5 insertions, 4 deletions
diff --git a/lib/regfp.sail b/lib/regfp.sail index de2430ce..ebbf1655 100644 --- a/lib/regfp.sail +++ b/lib/regfp.sail @@ -4,7 +4,7 @@ $define _REGFP /* iR : input registers, * oR : output registers, * aR : registers feeding into the memory address */ - + /* branch instructions currently are not writing to NIA */ union regfp = { @@ -116,13 +116,14 @@ union instruction_kind = { val __read_mem = { ocaml: "Platform.read_mem", c: "platform_read_mem", _: "read_mem" } - : forall 'n 'addrsize, 'n > 0 & 'addrsize in {32, 64}. (read_kind, int('addrsize), bits('addrsize), int('n)) -> bits(8 * 'n) effect {rmem} + : forall 'n (constant 'addrsize : Int), 'n > 0 & 'addrsize in {32, 64}. + (read_kind, int('addrsize), bits('addrsize), int('n)) -> bits(8 * 'n) effect {rmem} val __write_mem_ea = { ocaml: "Platform.write_mem_ea", c: "platform_write_mem_ea", _: "write_mem_ea" } - : forall 'n 'addrsize, 'n > 0 & 'addrsize in {32, 64}. (write_kind, int('addrsize), bits('addrsize), int('n)) -> unit effect {eamem} + : forall 'n (constant 'addrsize : Int), 'n > 0 & 'addrsize in {32, 64}. (write_kind, int('addrsize), bits('addrsize), int('n)) -> unit effect {eamem} val __write_mem = { ocaml: "Platform.write_mem", c: "platform_write_mem", _: "write_mem" } - : forall 'n 'addrsize, 'n > 0 & 'addrsize in {32, 64}. (write_kind, int('addrsize), bits('addrsize), int('n), bits(8 * 'n)) -> bool effect {wmv} + : forall 'n (constant 'addrsize : Int), 'n > 0 & 'addrsize in {32, 64}. (write_kind, int('addrsize), bits('addrsize), int('n), bits(8 * 'n)) -> bool effect {wmv} val __excl_res = { ocaml: "Platform.excl_res", c: "platform_excl_res", _: "excl_result" } : unit -> bool effect {exmem} |