diff options
| -rw-r--r-- | lib/flow.sail | 3 | ||||
| -rw-r--r-- | lib/sail.c | 5 | ||||
| -rw-r--r-- | lib/sail.h | 1 | ||||
| -rw-r--r-- | src/bitfield.ml | 2 | ||||
| -rw-r--r-- | src/jib/jib_smt.ml | 1 | ||||
| -rw-r--r-- | src/sail.ml | 2 | ||||
| -rw-r--r-- | test/c/undefined_nat.expect | 1 | ||||
| -rw-r--r-- | test/c/undefined_nat.sail | 13 | ||||
| -rw-r--r-- | test/typecheck/pass/bitfield_pc.sail | 6 |
9 files changed, 31 insertions, 3 deletions
diff --git a/lib/flow.sail b/lib/flow.sail index dd917b55..a2f6ed55 100644 --- a/lib/flow.sail +++ b/lib/flow.sail @@ -63,4 +63,7 @@ overload __size = {__id} val __deref = "reg_deref" : forall ('a : Type). register('a) -> 'a effect {rreg} +/* Used to implement bitfield desugaring */ +val __bitfield_deref = "reg_deref" : forall ('a : Type). register('a) -> 'a effect pure + $endif @@ -323,6 +323,11 @@ void undefined_int(sail_int *rop, const int n) mpz_set_ui(*rop, (uint64_t) n); } +void undefined_nat(sail_int *rop, const unit u) +{ + mpz_set_ui(*rop, 0); +} + inline void undefined_range(sail_int *rop, const sail_int l, const sail_int u) { @@ -129,6 +129,7 @@ SAIL_INT_FUNCTION(shr_int, sail_int, const sail_int, const sail_int); * constraints. */ SAIL_INT_FUNCTION(undefined_int, sail_int, const int); +SAIL_INT_FUNCTION(undefined_nat, sail_int, const unit); SAIL_INT_FUNCTION(undefined_range, sail_int, const sail_int, const sail_int); /* diff --git a/src/bitfield.ml b/src/bitfield.ml index 1f64adbd..feda4602 100644 --- a/src/bitfield.ml +++ b/src/bitfield.ml @@ -121,7 +121,7 @@ let index_range_setter name field order start stop = in let irs_function = String.concat "\n" [ Printf.sprintf "function _set_%s_%s (r_ref, v) = {" name field; - " r = _reg_deref(r_ref);"; + " r = __bitfield_deref(r_ref);"; Printf.sprintf " %s;" (Util.string_of_list ";\n " body indices); " (*r_ref) = r"; "}" diff --git a/src/jib/jib_smt.ml b/src/jib/jib_smt.ml index 7f622f85..5847c99c 100644 --- a/src/jib/jib_smt.ml +++ b/src/jib/jib_smt.ml @@ -1456,7 +1456,6 @@ let smt_instr ctx = | [rk; addr_size; addr; data_size] -> let mem_event, var = builtin_read_mem ctx rk addr_size addr data_size ret_ctyp in mem_event @ [define_const ctx id ret_ctyp var] - | _ -> Reporting.unreachable l __POS__ "Bad arguments for __read_mem" end diff --git a/src/sail.ml b/src/sail.ml index eff90fa3..65be5474 100644 --- a/src/sail.ml +++ b/src/sail.ml @@ -260,7 +260,7 @@ let options = Arg.align ([ "<filename>:<line>:<variable> to case split for monomorphisation"); ( "-memo_z3", Arg.Set opt_memo_z3, - " memoize calls to z3, improving performance when typechecking repeatedly (default)"); + " memoize calls to z3, improving performance when typechecking repeatedly"); ( "-no_memo_z3", Arg.Clear opt_memo_z3, " do not memoize calls to z3 (default)"); diff --git a/test/c/undefined_nat.expect b/test/c/undefined_nat.expect new file mode 100644 index 00000000..9766475a --- /dev/null +++ b/test/c/undefined_nat.expect @@ -0,0 +1 @@ +ok diff --git a/test/c/undefined_nat.sail b/test/c/undefined_nat.sail new file mode 100644 index 00000000..35dead66 --- /dev/null +++ b/test/c/undefined_nat.sail @@ -0,0 +1,13 @@ +default Order dec + +$include <prelude.sail> + +val "print_endline" : string -> unit + +register R : nat + +register T : int + +function main() -> unit = { + print_endline("ok"); +}
\ No newline at end of file diff --git a/test/typecheck/pass/bitfield_pc.sail b/test/typecheck/pass/bitfield_pc.sail new file mode 100644 index 00000000..9764289a --- /dev/null +++ b/test/typecheck/pass/bitfield_pc.sail @@ -0,0 +1,6 @@ +$include <vector_dec.sail> + +bitfield PC_t : vector(16, dec, bit) = { + H : 15 .. 8, + L : 7 .. 0 +} |