diff options
Diffstat (limited to 'test')
151 files changed, 3180 insertions, 0 deletions
diff --git a/test/typecheck/fail/assignment_simple1.sail b/test/typecheck/fail/assignment_simple1.sail new file mode 100644 index 00000000..1ad9f8bf --- /dev/null +++ b/test/typecheck/fail/assignment_simple1.sail @@ -0,0 +1,16 @@ + +val ([:10:], unit) -> [:10:] effect pure f + +function [:10:] f (x, y) = x + +val unit -> [:10:] effect pure test + +function [:10:] test () = +{ + z := 9; + z +} + +val unit -> unit effect pure test2 + +function unit test2 () = x := 10 diff --git a/test/typecheck/fail/assignment_simple2.sail b/test/typecheck/fail/assignment_simple2.sail new file mode 100644 index 00000000..db45bbcf --- /dev/null +++ b/test/typecheck/fail/assignment_simple2.sail @@ -0,0 +1,15 @@ + +val ([:10:], unit) -> [:10:] effect pure f + +function [:10:] f (x, y) = x + +val unit -> [:10:] effect pure test + +function [:10:] test () = +{ + f(z, z := 10) +} + +val unit -> unit effect pure test2 + +function unit test2 () = x := 10 diff --git a/test/typecheck/fail/assignment_simple3.sail b/test/typecheck/fail/assignment_simple3.sail new file mode 100644 index 00000000..2a596c29 --- /dev/null +++ b/test/typecheck/fail/assignment_simple3.sail @@ -0,0 +1,15 @@ + +val (unit, [:10:]) -> [:10:] effect pure f + +function [:10:] f (x, y) = y + +val unit -> [:10:] effect pure test + +function [:10:] test () = +{ + f(z := 10, z) +} + +val unit -> unit effect pure test2 + +function unit test2 () = x := 10 diff --git a/test/typecheck/fail/bitwise_not_gen1.sail b/test/typecheck/fail/bitwise_not_gen1.sail new file mode 100644 index 00000000..272b1a65 --- /dev/null +++ b/test/typecheck/fail/bitwise_not_gen1.sail @@ -0,0 +1,8 @@ + +val forall Nat 'n, Nat 'm, Order 'o. vector<'n,'m,'o,bit> -> vector<'n,'m,'o,bit> effect pure bitwise_not + +default Order dec + +val forall 'n. bit['n] -> bit['n - 1] effect pure test + +function forall 'n. bit['n - 1] test ((bit['n]) x) = bitwise_not(bitwise_not(x))
\ No newline at end of file diff --git a/test/typecheck/fail/bitwise_not_gen2.sail b/test/typecheck/fail/bitwise_not_gen2.sail new file mode 100644 index 00000000..fdf17244 --- /dev/null +++ b/test/typecheck/fail/bitwise_not_gen2.sail @@ -0,0 +1,8 @@ + +val forall Nat 'n, Nat 'm, Order 'o. vector<'n,'m,'o,bit> -> vector<'n,'m,'o,bit> effect pure bitwise_not + +default Order dec + +val forall 'n. bit['n] -> bit['n + 1] effect pure test + +function forall 'n. bit['n + 1] test ((bit['n]) x) = bitwise_not(bitwise_not(x))
\ No newline at end of file diff --git a/test/typecheck/fail/bv_simple_index_no_cast.sail b/test/typecheck/fail/bv_simple_index_no_cast.sail new file mode 100644 index 00000000..74f46ab7 --- /dev/null +++ b/test/typecheck/fail/bv_simple_index_no_cast.sail @@ -0,0 +1,9 @@ +val forall Nat 'n, Nat 'l, Type 'a, 'l >= 0. (vector<'n,'l,dec,'a>, [|'n - 'l + 1:'n|]) -> 'a effect pure vector_access_dec +val forall Nat 'n, Nat 'l, Type 'a, 'l >= 0. (vector<'n,'l,inc,'a>, [|'n:'n + 'l - 1|]) -> 'a effect pure vector_access_inc + +overload vector_access [vector_access_inc; vector_access_dec] + +function bool bv ((bit[64]) x) = +{ + x[32] +} diff --git a/test/typecheck/fail/case_simple1.sail b/test/typecheck/fail/case_simple1.sail new file mode 100644 index 00000000..471c3565 --- /dev/null +++ b/test/typecheck/fail/case_simple1.sail @@ -0,0 +1,9 @@ + +val forall Nat 'N. ([:10:], [|10:'N|]) -> [|10:'N|] effect pure case_test + +function forall Nat 'N. [|10:'N|] case_test (x, y) = +{ + switch (x, y) { + case _ -> x + } +} diff --git a/test/typecheck/fail/cast_lexp1.sail b/test/typecheck/fail/cast_lexp1.sail new file mode 100644 index 00000000..dad4c84c --- /dev/null +++ b/test/typecheck/fail/cast_lexp1.sail @@ -0,0 +1,7 @@ + +val unit -> nat effect pure test + +function nat test () = { + (int) y := 10; + y +} diff --git a/test/typecheck/fail/cast_simple.sail b/test/typecheck/fail/cast_simple.sail new file mode 100644 index 00000000..19768fbe --- /dev/null +++ b/test/typecheck/fail/cast_simple.sail @@ -0,0 +1,7 @@ + +val unit -> nat effect pure test + +function nat test () = { + (int) y := ([|0:10|]) 10; + (nat) y +} diff --git a/test/typecheck/fail/default_order.sail b/test/typecheck/fail/default_order.sail new file mode 100644 index 00000000..8de5cc46 --- /dev/null +++ b/test/typecheck/fail/default_order.sail @@ -0,0 +1,6 @@ +(* Could make an argument for why this should be ok, but allowing +default order to change could have unintended consequences if we arn't +careful, so it seems safer to just forbid it *) + +default Order dec +default Order inc diff --git a/test/typecheck/fail/eff_escape.sail b/test/typecheck/fail/eff_escape.sail new file mode 100644 index 00000000..698cf0b1 --- /dev/null +++ b/test/typecheck/fail/eff_escape.sail @@ -0,0 +1,7 @@ + +val unit -> unit effect pure test + +function unit test () = +{ + exit () +} diff --git a/test/typecheck/fail/eff_undef.sail b/test/typecheck/fail/eff_undef.sail new file mode 100644 index 00000000..d5d98a3f --- /dev/null +++ b/test/typecheck/fail/eff_undef.sail @@ -0,0 +1,7 @@ + +val unit -> unit effect pure test + +function unit test () = +{ + undefined +} diff --git a/test/typecheck/fail/flow_gt1.sail b/test/typecheck/fail/flow_gt1.sail new file mode 100644 index 00000000..917793cd --- /dev/null +++ b/test/typecheck/fail/flow_gt1.sail @@ -0,0 +1,28 @@ +default Order inc + +val forall Num 'n, Num 'm, Num 'o, Num 'p. ([|'n:'m|], [|'o:'p|]) -> [|'n+'o:'m+'p|] effect pure add_range + +val forall Num 'n, Num 'm, Num 'o, Num 'p. ([|'n:'m|], [|'o:'p|]) -> [|'n-'p:'m-'o|] effect pure sub_range + +val forall Num 'n, Num 'm, Num 'o. ([|'n:'m|], [:'o:]) -> bool effect pure lt_range_atom +val forall Num 'n, Num 'm, Num 'o. ([|'n:'m|], [:'o:]) -> bool effect pure lteq_range_atom +val forall Num 'n, Num 'm, Num 'o. ([|'n:'m|], [:'o:]) -> bool effect pure gt_range_atom +val forall Num 'n, Num 'm, Num 'o. ([|'n:'m|], [:'o:]) -> bool effect pure gteq_range_atom +val forall Num 'n, Num 'm, Num 'o. ([:'n:], [|'m:'o|]) -> bool effect pure lt_atom_range +val forall Num 'n, Num 'm, Num 'o. ([:'n:], [|'m:'o|]) -> bool effect pure lteq_atom_range +val forall Num 'n, Num 'm, Num 'o. ([:'n:], [|'m:'o|]) -> bool effect pure gt_atom_range +val forall Num 'n, Num 'm, Num 'o. ([:'n:], [|'m:'o|]) -> bool effect pure gteq_atom_range + +overload (deinfix +) [add_range] +overload (deinfix -) [sub_range] +overload (deinfix <) [lt_atom_range; lt_range_atom] +overload (deinfix <=) [lteq_atom_range; lteq_range_atom] +overload (deinfix >) [gt_atom_range; gt_range_atom] +overload (deinfix >=) [gteq_atom_range; gteq_range_atom] + +function ([|63|]) branch (([|63|]) x) = +{ + if (x > 31) + then x - 33 + else x + 32 +} diff --git a/test/typecheck/fail/flow_gt2.sail b/test/typecheck/fail/flow_gt2.sail new file mode 100644 index 00000000..f5ea4978 --- /dev/null +++ b/test/typecheck/fail/flow_gt2.sail @@ -0,0 +1,28 @@ +default Order inc + +val forall Num 'n, Num 'm, Num 'o, Num 'p. ([|'n:'m|], [|'o:'p|]) -> [|'n+'o:'m+'p|] effect pure add_range + +val forall Num 'n, Num 'm, Num 'o, Num 'p. ([|'n:'m|], [|'o:'p|]) -> [|'n-'p:'m-'o|] effect pure sub_range + +val forall Num 'n, Num 'm, Num 'o. ([|'n:'m|], [:'o:]) -> bool effect pure lt_range_atom +val forall Num 'n, Num 'm, Num 'o. ([|'n:'m|], [:'o:]) -> bool effect pure lteq_range_atom +val forall Num 'n, Num 'm, Num 'o. ([|'n:'m|], [:'o:]) -> bool effect pure gt_range_atom +val forall Num 'n, Num 'm, Num 'o. ([|'n:'m|], [:'o:]) -> bool effect pure gteq_range_atom +val forall Num 'n, Num 'm, Num 'o. ([:'n:], [|'m:'o|]) -> bool effect pure lt_atom_range +val forall Num 'n, Num 'm, Num 'o. ([:'n:], [|'m:'o|]) -> bool effect pure lteq_atom_range +val forall Num 'n, Num 'm, Num 'o. ([:'n:], [|'m:'o|]) -> bool effect pure gt_atom_range +val forall Num 'n, Num 'm, Num 'o. ([:'n:], [|'m:'o|]) -> bool effect pure gteq_atom_range + +overload (deinfix +) [add_range] +overload (deinfix -) [sub_range] +overload (deinfix <) [lt_atom_range; lt_range_atom] +overload (deinfix <=) [lteq_atom_range; lteq_range_atom] +overload (deinfix >) [gt_atom_range; gt_range_atom] +overload (deinfix >=) [gteq_atom_range; gteq_range_atom] + +function ([|63|]) branch (([|63|]) x) = +{ + if (x > 31) + then x - 32 + else x + 33 +} diff --git a/test/typecheck/fail/flow_gteq1.sail b/test/typecheck/fail/flow_gteq1.sail new file mode 100644 index 00000000..b55647d3 --- /dev/null +++ b/test/typecheck/fail/flow_gteq1.sail @@ -0,0 +1,28 @@ +default Order inc + +val forall Num 'n, Num 'm, Num 'o, Num 'p. ([|'n:'m|], [|'o:'p|]) -> [|'n+'o:'m+'p|] effect pure add_range + +val forall Num 'n, Num 'm, Num 'o, Num 'p. ([|'n:'m|], [|'o:'p|]) -> [|'n-'p:'m-'o|] effect pure sub_range + +val forall Num 'n, Num 'm, Num 'o. ([|'n:'m|], [:'o:]) -> bool effect pure lt_range_atom +val forall Num 'n, Num 'm, Num 'o. ([|'n:'m|], [:'o:]) -> bool effect pure lteq_range_atom +val forall Num 'n, Num 'm, Num 'o. ([|'n:'m|], [:'o:]) -> bool effect pure gt_range_atom +val forall Num 'n, Num 'm, Num 'o. ([|'n:'m|], [:'o:]) -> bool effect pure gteq_range_atom +val forall Num 'n, Num 'm, Num 'o. ([:'n:], [|'m:'o|]) -> bool effect pure lt_atom_range +val forall Num 'n, Num 'm, Num 'o. ([:'n:], [|'m:'o|]) -> bool effect pure lteq_atom_range +val forall Num 'n, Num 'm, Num 'o. ([:'n:], [|'m:'o|]) -> bool effect pure gt_atom_range +val forall Num 'n, Num 'm, Num 'o. ([:'n:], [|'m:'o|]) -> bool effect pure gteq_atom_range + +overload (deinfix +) [add_range] +overload (deinfix -) [sub_range] +overload (deinfix <) [lt_atom_range; lt_range_atom] +overload (deinfix <=) [lteq_atom_range; lteq_range_atom] +overload (deinfix >) [gt_atom_range; gt_range_atom] +overload (deinfix >=) [gteq_atom_range; gteq_range_atom] + +function ([|63|]) branch (([|63|]) x) = +{ + if (x >= 32) + then x - 33 + else x + 32 +} diff --git a/test/typecheck/fail/flow_gteq2.sail b/test/typecheck/fail/flow_gteq2.sail new file mode 100644 index 00000000..9d0a6201 --- /dev/null +++ b/test/typecheck/fail/flow_gteq2.sail @@ -0,0 +1,28 @@ +default Order inc + +val forall Num 'n, Num 'm, Num 'o, Num 'p. ([|'n:'m|], [|'o:'p|]) -> [|'n+'o:'m+'p|] effect pure add_range + +val forall Num 'n, Num 'm, Num 'o, Num 'p. ([|'n:'m|], [|'o:'p|]) -> [|'n-'p:'m-'o|] effect pure sub_range + +val forall Num 'n, Num 'm, Num 'o. ([|'n:'m|], [:'o:]) -> bool effect pure lt_range_atom +val forall Num 'n, Num 'm, Num 'o. ([|'n:'m|], [:'o:]) -> bool effect pure lteq_range_atom +val forall Num 'n, Num 'm, Num 'o. ([|'n:'m|], [:'o:]) -> bool effect pure gt_range_atom +val forall Num 'n, Num 'm, Num 'o. ([|'n:'m|], [:'o:]) -> bool effect pure gteq_range_atom +val forall Num 'n, Num 'm, Num 'o. ([:'n:], [|'m:'o|]) -> bool effect pure lt_atom_range +val forall Num 'n, Num 'm, Num 'o. ([:'n:], [|'m:'o|]) -> bool effect pure lteq_atom_range +val forall Num 'n, Num 'm, Num 'o. ([:'n:], [|'m:'o|]) -> bool effect pure gt_atom_range +val forall Num 'n, Num 'm, Num 'o. ([:'n:], [|'m:'o|]) -> bool effect pure gteq_atom_range + +overload (deinfix +) [add_range] +overload (deinfix -) [sub_range] +overload (deinfix <) [lt_atom_range; lt_range_atom] +overload (deinfix <=) [lteq_atom_range; lteq_range_atom] +overload (deinfix >) [gt_atom_range; gt_range_atom] +overload (deinfix >=) [gteq_atom_range; gteq_range_atom] + +function ([|63|]) branch (([|63|]) x) = +{ + if (x >= 32) + then x - 32 + else x + 33 +} diff --git a/test/typecheck/fail/flow_lt1.sail b/test/typecheck/fail/flow_lt1.sail new file mode 100644 index 00000000..a127ccb0 --- /dev/null +++ b/test/typecheck/fail/flow_lt1.sail @@ -0,0 +1,19 @@ +default Order inc + +val forall Num 'n, Num 'm, Num 'o, Num 'p. ([|'n:'m|], [|'o:'p|]) -> [|'n+'o:'m+'p|] effect pure add_range + +val forall Num 'n, Num 'm, Num 'o, Num 'p. ([|'n:'m|], [|'o:'p|]) -> [|'n-'p:'m-'o|] effect pure sub_range + +val forall Num 'n, Num 'm, Num 'o. ([|'n:'m|], [:'o:]) -> bool effect pure lt_range_atom +val forall Num 'n, Num 'm, Num 'o. ([:'n:], [|'m:'o|]) -> bool effect pure lt_atom_range + +overload (deinfix +) [add_range] +overload (deinfix -) [sub_range] +overload (deinfix <) [lt_atom_range; lt_range_atom] + +function ([|63|]) branch (([|63|]) x) = +{ + if (x < 32) + then x + 33 + else x - 32 +} diff --git a/test/typecheck/fail/flow_lt2.sail b/test/typecheck/fail/flow_lt2.sail new file mode 100644 index 00000000..a537a084 --- /dev/null +++ b/test/typecheck/fail/flow_lt2.sail @@ -0,0 +1,19 @@ +default Order inc + +val forall Num 'n, Num 'm, Num 'o, Num 'p. ([|'n:'m|], [|'o:'p|]) -> [|'n+'o:'m+'p|] effect pure add_range + +val forall Num 'n, Num 'm, Num 'o, Num 'p. ([|'n:'m|], [|'o:'p|]) -> [|'n-'p:'m-'o|] effect pure sub_range + +val forall Num 'n, Num 'm, Num 'o. ([|'n:'m|], [:'o:]) -> bool effect pure lt_range_atom +val forall Num 'n, Num 'm, Num 'o. ([:'n:], [|'m:'o|]) -> bool effect pure lt_atom_range + +overload (deinfix +) [add_range] +overload (deinfix -) [sub_range] +overload (deinfix <) [lt_atom_range; lt_range_atom] + +function ([|63|]) branch (([|63|]) x) = +{ + if (x < 32) + then x + 32 + else x - 33 +} diff --git a/test/typecheck/fail/flow_lteq1.sail b/test/typecheck/fail/flow_lteq1.sail new file mode 100644 index 00000000..3bebcc97 --- /dev/null +++ b/test/typecheck/fail/flow_lteq1.sail @@ -0,0 +1,28 @@ +default Order inc + +val forall Num 'n, Num 'm, Num 'o, Num 'p. ([|'n:'m|], [|'o:'p|]) -> [|'n+'o:'m+'p|] effect pure add_range + +val forall Num 'n, Num 'm, Num 'o, Num 'p. ([|'n:'m|], [|'o:'p|]) -> [|'n-'p:'m-'o|] effect pure sub_range + +val forall Num 'n, Num 'm, Num 'o. ([|'n:'m|], [:'o:]) -> bool effect pure lt_range_atom +val forall Num 'n, Num 'm, Num 'o. ([|'n:'m|], [:'o:]) -> bool effect pure lteq_range_atom +val forall Num 'n, Num 'm, Num 'o. ([|'n:'m|], [:'o:]) -> bool effect pure gt_range_atom +val forall Num 'n, Num 'm, Num 'o. ([|'n:'m|], [:'o:]) -> bool effect pure gteq_range_atom +val forall Num 'n, Num 'm, Num 'o. ([:'n:], [|'m:'o|]) -> bool effect pure lt_atom_range +val forall Num 'n, Num 'm, Num 'o. ([:'n:], [|'m:'o|]) -> bool effect pure lteq_atom_range +val forall Num 'n, Num 'm, Num 'o. ([:'n:], [|'m:'o|]) -> bool effect pure gt_atom_range +val forall Num 'n, Num 'm, Num 'o. ([:'n:], [|'m:'o|]) -> bool effect pure gteq_atom_range + +overload (deinfix +) [add_range] +overload (deinfix -) [sub_range] +overload (deinfix <) [lt_atom_range; lt_range_atom] +overload (deinfix <=) [lteq_atom_range; lteq_range_atom] +overload (deinfix >) [gt_atom_range; gt_range_atom] +overload (deinfix >=) [gteq_atom_range; gteq_range_atom] + +function ([|63|]) branch (([|63|]) x) = +{ + if (x <= 32) + then x + 32 + else x - 33 +} diff --git a/test/typecheck/fail/flow_lteq2.sail b/test/typecheck/fail/flow_lteq2.sail new file mode 100644 index 00000000..c3ee9c0a --- /dev/null +++ b/test/typecheck/fail/flow_lteq2.sail @@ -0,0 +1,28 @@ +default Order inc + +val forall Num 'n, Num 'm, Num 'o, Num 'p. ([|'n:'m|], [|'o:'p|]) -> [|'n+'o:'m+'p|] effect pure add_range + +val forall Num 'n, Num 'm, Num 'o, Num 'p. ([|'n:'m|], [|'o:'p|]) -> [|'n-'p:'m-'o|] effect pure sub_range + +val forall Num 'n, Num 'm, Num 'o. ([|'n:'m|], [:'o:]) -> bool effect pure lt_range_atom +val forall Num 'n, Num 'm, Num 'o. ([|'n:'m|], [:'o:]) -> bool effect pure lteq_range_atom +val forall Num 'n, Num 'm, Num 'o. ([|'n:'m|], [:'o:]) -> bool effect pure gt_range_atom +val forall Num 'n, Num 'm, Num 'o. ([|'n:'m|], [:'o:]) -> bool effect pure gteq_range_atom +val forall Num 'n, Num 'm, Num 'o. ([:'n:], [|'m:'o|]) -> bool effect pure lt_atom_range +val forall Num 'n, Num 'm, Num 'o. ([:'n:], [|'m:'o|]) -> bool effect pure lteq_atom_range +val forall Num 'n, Num 'm, Num 'o. ([:'n:], [|'m:'o|]) -> bool effect pure gt_atom_range +val forall Num 'n, Num 'm, Num 'o. ([:'n:], [|'m:'o|]) -> bool effect pure gteq_atom_range + +overload (deinfix +) [add_range] +overload (deinfix -) [sub_range] +overload (deinfix <) [lt_atom_range; lt_range_atom] +overload (deinfix <=) [lteq_atom_range; lteq_range_atom] +overload (deinfix >) [gt_atom_range; gt_range_atom] +overload (deinfix >=) [gteq_atom_range; gteq_range_atom] + +function ([|63|]) branch (([|63|]) x) = +{ + if (x <= 32) + then x + 31 + else x - 34 +} diff --git a/test/typecheck/fail/fun_simple_constraints1.sail b/test/typecheck/fail/fun_simple_constraints1.sail new file mode 100644 index 00000000..979e0cdf --- /dev/null +++ b/test/typecheck/fail/fun_simple_constraints1.sail @@ -0,0 +1,18 @@ + +val forall Nat 'n, Nat 'm. ([:'n + 20:], [:'m:]) -> [:'n + 20 + 'm:] effect pure plus + +val forall Nat 'n, 'n <= -10. [:'n:] -> [:'n:] effect pure minus_ten_id + +val forall Nat 'n, 'n >= 10. [:'n:] -> [:'n:] effect pure ten_id + +val forall Nat 'N, 'N >= 63. [|10:'N|] -> [|10:'N|] effect pure branch + +function forall Nat 'N, 'N >= 63. [|10:'N|] branch x = +{ + x +} +and branch (([|10:30|]) y) = y +and branch (([:31:]) _) = sizeof 'N +and branch (([|31:40|]) _) = plus(60,3) +and branch (([|41:50|]) _) = plus(sizeof 'N, minus_ten_id(-53)) +and branch (([|51:64|]) _) = ten_id(sizeof 'N) diff --git a/test/typecheck/fail/fun_simple_constraints2.sail b/test/typecheck/fail/fun_simple_constraints2.sail new file mode 100644 index 00000000..43a0b6d7 --- /dev/null +++ b/test/typecheck/fail/fun_simple_constraints2.sail @@ -0,0 +1,18 @@ + +val forall Nat 'n, Nat 'm. ([:'n + 20:], [:'m:]) -> [:'n + 20 + 'm:] effect pure plus + +val forall Nat 'n, 'n <= -10. [:'n:] -> [:'n:] effect pure minus_ten_id + +val forall Nat 'n, 'n >= 10. [:'n:] -> [:'n:] effect pure ten_id + +val forall Nat 'N, 'N >= 63. [|10:'N|] -> [|10:'N|] effect pure branch + +function forall Nat 'N, 'N >= 63. [|10:'N|] branch x = +{ + x +} +and branch (([|10:30|]) y) = y +and branch (([:31:]) _) = sizeof 'N +and branch (([|31:40|]) _) = plus(60,3) +and branch (([|41:50|]) _) = plus(sizeof 'N, minus_ten_id(-53)) +and branch (([|51:63|]) _) = ten_id(9) diff --git a/test/typecheck/fail/fun_simple_constraints3.sail b/test/typecheck/fail/fun_simple_constraints3.sail new file mode 100644 index 00000000..098054e4 --- /dev/null +++ b/test/typecheck/fail/fun_simple_constraints3.sail @@ -0,0 +1,18 @@ + +val forall Nat 'n, Nat 'm. ([:'n + 20:], [:'m:]) -> [:'n + 20 + 'm:] effect pure plus + +val forall Nat 'n, 'n <= -10. [:'n:] -> [:'n:] effect pure minus_ten_id + +val forall Nat 'n, 'n >= 10. [:'n:] -> [:'n:] effect pure ten_id + +val forall Nat 'N, 'N >= 63. [|10:'N|] -> [|10:'N|] effect pure branch + +function forall Nat 'N, 'N >= 63. [|10:'N|] branch x = +{ + x +} +and branch (([|10:30|]) y) = y +and branch (([:31:]) _) = sizeof 'N +and branch (([|31:40|]) _) = plus(60,3) +and branch (([|41:50|]) _) = plus(sizeof 'N, minus_ten_id(-53)) +and branch (([|51:63|]) _) = ten_id(plus(sizeof 'N, 1)) diff --git a/test/typecheck/fail/fun_simple_constraints4.sail b/test/typecheck/fail/fun_simple_constraints4.sail new file mode 100644 index 00000000..07b8c596 --- /dev/null +++ b/test/typecheck/fail/fun_simple_constraints4.sail @@ -0,0 +1,18 @@ + +val forall Nat 'n, Nat 'm. ([:'n + 20:], [:'m:]) -> [:'n + 20 + 'm:] effect pure plus + +val forall Nat 'n, 'n <= -10. [:'n:] -> [:'n:] effect pure minus_ten_id + +val forall Nat 'n, 'n >= 10. [:'n:] -> [:'n:] effect pure ten_id + +val forall Nat 'N, 'N >= 63. [|10:'N|] -> [|10:'N|] effect pure branch + +function forall Nat 'N, 'N >= 63. [|10:'N|] branch x = +{ + x +} +and branch (([|10:30|]) y) = y +and branch (([:31:]) _) = sizeof 'N +and branch (([|31:40|]) _) = plus(60,3) +and branch (([|41:50|]) _) = plus(sizeof 'N, minus_ten_id(-54)) +and branch (([|51:63|]) _) = ten_id(sizeof 'N) diff --git a/test/typecheck/fail/fun_simple_constraints5.sail b/test/typecheck/fail/fun_simple_constraints5.sail new file mode 100644 index 00000000..7e28db85 --- /dev/null +++ b/test/typecheck/fail/fun_simple_constraints5.sail @@ -0,0 +1,18 @@ + +val forall Nat 'n, Nat 'm. ([:'n + 20:], [:'m:]) -> [:'n + 20 + 'm:] effect pure plus + +val forall Nat 'n, 'n <= -10. [:'n:] -> [:'n:] effect pure minus_ten_id + +val forall Nat 'n, 'n >= 10. [:'n:] -> [:'n:] effect pure ten_id + +val forall Nat 'N, 'N >= 63. [|10:'N|] -> [|10:'N|] effect pure branch + +function forall Nat 'N, 'N >= 63. [|10:'N|] branch x = +{ + x +} +and branch (([|10:30|]) y) = y +and branch (([:31:]) _) = sizeof 'N +and branch (([|31:40|]) _) = plus(60,3) +and branch (([|41:50|]) _) = plus(sizeof 'N, minus_ten_id(-9)) +and branch (([|51:63|]) _) = ten_id(sizeof 'N) diff --git a/test/typecheck/fail/fun_simple_constraints6.sail b/test/typecheck/fail/fun_simple_constraints6.sail new file mode 100644 index 00000000..6dc5e0e6 --- /dev/null +++ b/test/typecheck/fail/fun_simple_constraints6.sail @@ -0,0 +1,18 @@ + +val forall Nat 'n, Nat 'k, Nat 'm. ([:'n + 'k:], [:'m:]) -> [:'n + 'k + 'm:] effect pure plus + +val forall Nat 'n, 'n <= -10. [:'n:] -> [:'n:] effect pure minus_ten_id + +val forall Nat 'n, 'n >= 10. [:'n:] -> [:'n:] effect pure ten_id + +val forall Nat 'N, 'N >= 63. [|10:'N|] -> [|10:'N|] effect pure branch + +function forall Nat 'N, 'N >= 63. [|10:'N|] branch x = +{ + x +} +and branch (([|10:30|]) y) = y +and branch (([:31:]) _) = sizeof 'N +and branch (([|31:40|]) _) = plus(60,3) +and branch (([|41:50|]) _) = plus(sizeof 'N, minus_ten_id(-53)) +and branch (([|51:63|]) _) = ten_id(sizeof 'N) diff --git a/test/typecheck/fail/fun_simple_constraints7.sail b/test/typecheck/fail/fun_simple_constraints7.sail new file mode 100644 index 00000000..00d2a172 --- /dev/null +++ b/test/typecheck/fail/fun_simple_constraints7.sail @@ -0,0 +1,18 @@ + +val forall Nat 'n, Nat 'm. ([:'n + 20:], [:'m:]) -> [:'n + 20 + 'm:] effect pure plus + +val forall Nat 'n, 'n <= -10. [:'n:] -> [:'n:] effect pure minus_ten_id + +val forall Nat 'n, 'n >= 10. [:'n:] -> [:'n:] effect pure ten_id + +val forall Nat 'N, 'N >= 63. [|11:'N|] -> [|10:'N|] effect pure branch + +function forall Nat 'N, 'N >= 63. [|10:'N|] branch x = +{ + x +} +and branch (([|10:30|]) y) = y +and branch (([:31:]) _) = sizeof 'N +and branch (([|31:40|]) _) = plus(60,3) +and branch (([|41:50|]) _) = plus(sizeof 'N, minus_ten_id(-53)) +and branch (([|51:63|]) _) = ten_id(sizeof 'N) diff --git a/test/typecheck/fail/fun_simple_constraints8.sail b/test/typecheck/fail/fun_simple_constraints8.sail new file mode 100644 index 00000000..e4c02da0 --- /dev/null +++ b/test/typecheck/fail/fun_simple_constraints8.sail @@ -0,0 +1,18 @@ + +val forall Nat 'n, Nat 'm. ([:'n + 20:], [:'m:]) -> [:'n + 20 + 'm:] effect pure plus + +val forall Nat 'n, 'n <= -10. [:'n:] -> [:'n:] effect pure minus_ten_id + +val forall Nat 'n, 'n >= 10. [:'n:] -> [:'n:] effect pure ten_id + +val forall Nat 'N, 'N >= 63. [|10:'N|] -> [|11:'N|] effect pure branch + +function forall Nat 'N, 'N >= 63. [|10:'N|] branch x = +{ + x +} +and branch (([|10:30|]) y) = y +and branch (([:31:]) _) = sizeof 'N +and branch (([|31:40|]) _) = plus(60,3) +and branch (([|41:50|]) _) = plus(sizeof 'N, minus_ten_id(-53)) +and branch (([|51:63|]) _) = ten_id(sizeof 'N) diff --git a/test/typecheck/fail/fun_simple_constraints9.sail b/test/typecheck/fail/fun_simple_constraints9.sail new file mode 100644 index 00000000..3563ae2d --- /dev/null +++ b/test/typecheck/fail/fun_simple_constraints9.sail @@ -0,0 +1,8 @@ + +val forall Nat 'n, Nat 'm. ([:'n + 20:], [:'m:]) -> [:'n + 20 + 'm:] effect pure plus + +val forall Nat 'n, 'n >= 10. [:'n:] -> [:'n:] effect pure ten_id + +val forall Nat 'N, 'N >= 63. [|10:'N|] -> [|10:'N|] effect pure branch + +function forall Nat 'N, 'N >= 63. [|10:'N|] branch x = ten_id(plus(sizeof 'N, 1)) diff --git a/test/typecheck/fail/funret1.sail b/test/typecheck/fail/funret1.sail new file mode 100644 index 00000000..09a4fd54 --- /dev/null +++ b/test/typecheck/fail/funret1.sail @@ -0,0 +1,16 @@ + +default Order inc + +typedef option = const union forall Type 'a. { + None; + 'a Some + } + +typedef Test = const union { + A; + B; + C +} + +let (option<int>) x = C + diff --git a/test/typecheck/fail/funret2.sail b/test/typecheck/fail/funret2.sail new file mode 100644 index 00000000..19536599 --- /dev/null +++ b/test/typecheck/fail/funret2.sail @@ -0,0 +1,16 @@ + +default Order inc + +typedef option = const union forall Type 'a. { + None; + 'a Some + } + +typedef Test = const union { + A; + B; + C +} + + +function option<int> test2 () = C diff --git a/test/typecheck/fail/funret3.sail b/test/typecheck/fail/funret3.sail new file mode 100644 index 00000000..d178f2ad --- /dev/null +++ b/test/typecheck/fail/funret3.sail @@ -0,0 +1,16 @@ + +default Order inc + +typedef option = const union forall Type 'a. { + None; + 'a Some + } + +typedef Test = const union { + A; + B; + C +} + + +function option<(option<int>)> test () = Some(C) diff --git a/test/typecheck/fail/mips_CP0Cause_BD_assign1.sail b/test/typecheck/fail/mips_CP0Cause_BD_assign1.sail new file mode 100644 index 00000000..2f599aa9 --- /dev/null +++ b/test/typecheck/fail/mips_CP0Cause_BD_assign1.sail @@ -0,0 +1,27 @@ +val forall Nat 'n, Order 'ord. [:1:] -> vector<'n,1,'ord,bit> effect pure cast_one_bv +val forall Nat 'n, Order 'ord. [:0:] -> vector<'n,1,'ord,bit> effect pure cast_zero_bv + +default Order dec + +typedef CauseReg = register bits [ 31 : 0 ] { + 31 : BD; (* branch delay *) + (*30 : Z0;*) + 29 .. 28 : CE; (* for coprocessor enable exception *) + (*27 .. 24 : Z1;*) + 23 : IV; (* special interrupt vector not supported *) + 22 : WP; (* watchpoint exception occurred *) + (*21 .. 16 : Z2; *) + 15 .. 8 : IP; (* interrupt pending bits *) + (*7 : Z3;*) + 6 .. 2 : ExcCode; (* code of last exception *) + (*1 .. 0 : Z4;*) +} + +register (CauseReg) CP0Cause + +val unit -> unit effect {wreg} test + +function unit test () = +{ + CP0Cause.BD := 2 +} diff --git a/test/typecheck/fail/mips_CauseReg1.sail b/test/typecheck/fail/mips_CauseReg1.sail new file mode 100644 index 00000000..ae99e625 --- /dev/null +++ b/test/typecheck/fail/mips_CauseReg1.sail @@ -0,0 +1,14 @@ + +typedef CauseReg = register bits [ 30 : 0 ] { + 31 : BD; (* branch delay *) + (*30 : Z0;*) + 29 .. 28 : CE; (* for coprocessor enable exception *) + (*27 .. 24 : Z1;*) + 23 : IV; (* special interrupt vector not supported *) + 22 : WP; (* watchpoint exception occurred *) + (*21 .. 16 : Z2; *) + 15 .. 8 : IP; (* interrupt pending bits *) + (*7 : Z3;*) + 6 .. 2 : ExcCode; (* code of last exception *) + (*1 .. 0 : Z4;*) +} diff --git a/test/typecheck/fail/mips_CauseReg2.sail b/test/typecheck/fail/mips_CauseReg2.sail new file mode 100644 index 00000000..683f5a2a --- /dev/null +++ b/test/typecheck/fail/mips_CauseReg2.sail @@ -0,0 +1,14 @@ + +typedef CauseReg = register bits [ 31 : 3 ] { + 31 : BD; (* branch delay *) + (*30 : Z0;*) + 29 .. 28 : CE; (* for coprocessor enable exception *) + (*27 .. 24 : Z1;*) + 23 : IV; (* special interrupt vector not supported *) + 22 : WP; (* watchpoint exception occurred *) + (*21 .. 16 : Z2; *) + 15 .. 8 : IP; (* interrupt pending bits *) + (*7 : Z3;*) + 6 .. 2 : ExcCode; (* code of last exception *) + (*1 .. 0 : Z4;*) +} diff --git a/test/typecheck/fail/mips_CauseReg3.sail b/test/typecheck/fail/mips_CauseReg3.sail new file mode 100644 index 00000000..09e27e27 --- /dev/null +++ b/test/typecheck/fail/mips_CauseReg3.sail @@ -0,0 +1,14 @@ + +typedef CauseReg = register bits [ 31 : 0 ] { + 31 : BD; (* branch delay *) + (*30 : Z0;*) + 32 .. 28 : CE; (* for coprocessor enable exception *) + (*27 .. 24 : Z1;*) + 23 : IV; (* special interrupt vector not supported *) + 22 : WP; (* watchpoint exception occurred *) + (*21 .. 16 : Z2; *) + 15 .. 8 : IP; (* interrupt pending bits *) + (*7 : Z3;*) + 6 .. 2 : ExcCode; (* code of last exception *) + (*1 .. 0 : Z4;*) +} diff --git a/test/typecheck/fail/mips_CauseReg4.sail b/test/typecheck/fail/mips_CauseReg4.sail new file mode 100644 index 00000000..1f14981f --- /dev/null +++ b/test/typecheck/fail/mips_CauseReg4.sail @@ -0,0 +1,14 @@ + +typedef CauseReg = register bits [ 31 : 0 ] { + 31 : BD; (* branch delay *) + (*30 : Z0;*) + 29 .. 28 : CE; (* for coprocessor enable exception *) + (*27 .. 24 : Z1;*) + 23 : IV; (* special interrupt vector not supported *) + 22 : WP; (* watchpoint exception occurred *) + (*21 .. 16 : Z2; *) + 8 .. 15 : IP; (* interrupt pending bits *) + (*7 : Z3;*) + 6 .. 2 : ExcCode; (* code of last exception *) + (*1 .. 0 : Z4;*) +} diff --git a/test/typecheck/fail/mips_CauseReg5.sail b/test/typecheck/fail/mips_CauseReg5.sail new file mode 100644 index 00000000..98fc614a --- /dev/null +++ b/test/typecheck/fail/mips_CauseReg5.sail @@ -0,0 +1,14 @@ + +typedef CauseReg = register bits [ 31 : 0 ] { + 31 : BD; (* branch delay *) + (*30 : Z0;*) + 29 .. 28 : CE; (* for coprocessor enable exception *) + (*27 .. 24 : Z1;*) + 22 : IV; (* special interrupt vector not supported *) + 23 : WP; (* watchpoint exception occurred *) + (*21 .. 16 : Z2; *) + 15 .. 8 : IP; (* interrupt pending bits *) + (*7 : Z3;*) + 6 .. 2 : ExcCode; (* code of last exception *) + (*1 .. 0 : Z4;*) +} diff --git a/test/typecheck/fail/mips_CauseReg6.sail b/test/typecheck/fail/mips_CauseReg6.sail new file mode 100644 index 00000000..ecb8322e --- /dev/null +++ b/test/typecheck/fail/mips_CauseReg6.sail @@ -0,0 +1,14 @@ + +typedef CauseReg = register bits [ 31 : 0 ] { + 31 : BD; (* branch delay *) + (*30 : Z0;*) + 29 .. 28 : BD; (* for coprocessor enable exception *) + (*27 .. 24 : Z1;*) + 23 : IV; (* special interrupt vector not supported *) + 22 : WP; (* watchpoint exception occurred *) + (*21 .. 16 : Z2; *) + 15 .. 8 : IP; (* interrupt pending bits *) + (*7 : Z3;*) + 6 .. 2 : ExcCode; (* code of last exception *) + (*1 .. 0 : Z4;*) +} diff --git a/test/typecheck/fail/mips_CauseReg7.sail b/test/typecheck/fail/mips_CauseReg7.sail new file mode 100644 index 00000000..48acd4f5 --- /dev/null +++ b/test/typecheck/fail/mips_CauseReg7.sail @@ -0,0 +1,15 @@ +default Order dec + +typedef CauseReg = register bits [ 31 : 0 ] { + 31 : BD; (* branch delay *) + (*30 : Z0;*) + 29 .. 28 : CE; (* for coprocessor enable exception *) + (*27 .. 24 : Z1;*) + 23 : IV; (* special interrupt vector not supported *) + 23 : WP; (* watchpoint exception occurred *) + (*21 .. 16 : Z2; *) + 15 .. 8 : IP; (* interrupt pending bits *) + (*7 : Z3;*) + 6 .. 2 : ExcCode; (* code of last exception *) + (*1 .. 0 : Z4;*) +} diff --git a/test/typecheck/fail/modify_assignment1.sail b/test/typecheck/fail/modify_assignment1.sail new file mode 100644 index 00000000..99adc95c --- /dev/null +++ b/test/typecheck/fail/modify_assignment1.sail @@ -0,0 +1,8 @@ + +val unit -> unit effect pure test + +function unit test () = +{ + z := 9; + z := 10 +}
\ No newline at end of file diff --git a/test/typecheck/fail/modify_assignment2.sail b/test/typecheck/fail/modify_assignment2.sail new file mode 100644 index 00000000..6551afff --- /dev/null +++ b/test/typecheck/fail/modify_assignment2.sail @@ -0,0 +1,8 @@ + +val unit -> unit effect pure test + +function unit test () = +{ + ([|0:9|]) z := 9; + z := ([|0:10|]) 10 +}
\ No newline at end of file diff --git a/test/typecheck/fail/modify_let_bound.sail b/test/typecheck/fail/modify_let_bound.sail new file mode 100644 index 00000000..a2ad1b98 --- /dev/null +++ b/test/typecheck/fail/modify_let_bound.sail @@ -0,0 +1,16 @@ + +default Order dec + +register bit[3] test + +val unit -> unit effect pure test + +function unit test () = +{ + let i = 10 in { + i := 20 + }; + z := 9; + z := 10; + test := 3 +}
\ No newline at end of file diff --git a/test/typecheck/fail/modify_type_chain1.sail b/test/typecheck/fail/modify_type_chain1.sail new file mode 100644 index 00000000..3fff3b59 --- /dev/null +++ b/test/typecheck/fail/modify_type_chain1.sail @@ -0,0 +1,8 @@ + +val unit -> unit effect pure test + +function unit test () = +{ + ([|0:10|]) z := 9; + ([|0:9|]) z := ([|0:10|]) 8 +}
\ No newline at end of file diff --git a/test/typecheck/fail/modify_type_chain2.sail b/test/typecheck/fail/modify_type_chain2.sail new file mode 100644 index 00000000..085e7db5 --- /dev/null +++ b/test/typecheck/fail/modify_type_chain2.sail @@ -0,0 +1,8 @@ + +val unit -> unit effect pure test + +function unit test () = +{ + ([|0:10|]) z := 9; + ([|0:7|]) z := ([|0:8|]) 8 +}
\ No newline at end of file diff --git a/test/typecheck/fail/modify_type_chain3.sail b/test/typecheck/fail/modify_type_chain3.sail new file mode 100644 index 00000000..cfe532aa --- /dev/null +++ b/test/typecheck/fail/modify_type_chain3.sail @@ -0,0 +1,8 @@ + +val unit -> unit effect pure test + +function unit test () = +{ + ([|0:6|]) z := 9; + ([|0:7|]) z := ([|0:8|]) 8 +}
\ No newline at end of file diff --git a/test/typecheck/fail/modify_type_chain4.sail b/test/typecheck/fail/modify_type_chain4.sail new file mode 100644 index 00000000..c36a9086 --- /dev/null +++ b/test/typecheck/fail/modify_type_chain4.sail @@ -0,0 +1,8 @@ + +val unit -> unit effect pure test + +function unit test () = +{ + ([|0:10|]) z := 9; + ([|0:11|]) z := ([|0:13|]) 8 +}
\ No newline at end of file diff --git a/test/typecheck/fail/modify_type_chain5.sail b/test/typecheck/fail/modify_type_chain5.sail new file mode 100644 index 00000000..3c3076a4 --- /dev/null +++ b/test/typecheck/fail/modify_type_chain5.sail @@ -0,0 +1,8 @@ + +val unit -> unit effect pure test + +function unit test () = +{ + ([|0:10|]) z := 9; + ([|0:9|]) z := ([|0:13|]) 8 +}
\ No newline at end of file diff --git a/test/typecheck/fail/my_unsigned1.sail b/test/typecheck/fail/my_unsigned1.sail new file mode 100644 index 00000000..958340ff --- /dev/null +++ b/test/typecheck/fail/my_unsigned1.sail @@ -0,0 +1,8 @@ + +default Order inc + +val forall Nat 'n, Nat 'm, Nat 'o, Order 'ord, 'o >= 0, 'o + 1 <= 2**'m. vector<'n,'m,'ord,bit> -> [:'o:] effect pure my_unsigned + +let MAX = my_unsigned(0xff) + +let ([:0:]) MIN = MAX
\ No newline at end of file diff --git a/test/typecheck/fail/nat_set.sail b/test/typecheck/fail/nat_set.sail new file mode 100644 index 00000000..036183c5 --- /dev/null +++ b/test/typecheck/fail/nat_set.sail @@ -0,0 +1,9 @@ + +function forall Nat 'n, 'n IN {1,2,3}. bool test (([:'n:]) x) = +{ + true +} + +let x = test(1) +let y = test(3) +let z = test(4)
\ No newline at end of file diff --git a/test/typecheck/fail/nondet.sail b/test/typecheck/fail/nondet.sail new file mode 100644 index 00000000..bce110c6 --- /dev/null +++ b/test/typecheck/fail/nondet.sail @@ -0,0 +1,10 @@ + +register int z + +function int test () = { + nondet { + z := 0; + z := 1; + z + } +} diff --git a/test/typecheck/fail/option_either1.sail b/test/typecheck/fail/option_either1.sail new file mode 100644 index 00000000..569ba212 --- /dev/null +++ b/test/typecheck/fail/option_either1.sail @@ -0,0 +1,35 @@ +default Order inc + +typedef option = const union forall Type 'a. { + None; + 'a Some +} + +function forall Type 'a. option<'a> none () = None + +function forall Type 'a. option<'a> some (('a) x) = Some(x) + +function forall Type 'a. int test ((option<'a>) x) = +{ + switch x { + case None -> 0 + case (Some(y)) -> 1 + } +} + +typedef either = const union forall Type 'a, Type 'b. { + 'a Left; + 'b Right +} + +val forall Nat 'n, 'n >= 0. bit['n] -> int effect pure signed + +function forall Type 'a, Type 'b. either<'a,'b> right (('b) x) = Right(x) + +function int test2 ((either<int,bit[1]>) x) = +{ + switch x { + case (Left(l)) -> l + case (right(r)) -> signed(r) + } +} diff --git a/test/typecheck/fail/procstate1.sail b/test/typecheck/fail/procstate1.sail new file mode 100644 index 00000000..00dc1ab1 --- /dev/null +++ b/test/typecheck/fail/procstate1.sail @@ -0,0 +1,16 @@ +default Order dec + +typedef ProcState = const struct forall Num 'n. +{ + bit['n] N; + bit[1] Z; + bit[1] C; + bit[1] V +} + +register ProcState<2> PSTATE + +function unit test () = +{ + PSTATE.N := 0b1 +} diff --git a/test/typecheck/fail/reg_mod.sail b/test/typecheck/fail/reg_mod.sail new file mode 100644 index 00000000..24b318b4 --- /dev/null +++ b/test/typecheck/fail/reg_mod.sail @@ -0,0 +1,11 @@ + +register [|0:10|] reg + +val unit -> unit effect pure test + +function unit test () = +{ + reg := 9; + reg := 10; + reg := 8 +}
\ No newline at end of file diff --git a/test/typecheck/fail/return_simple1.sail b/test/typecheck/fail/return_simple1.sail new file mode 100644 index 00000000..1bbc0e73 --- /dev/null +++ b/test/typecheck/fail/return_simple1.sail @@ -0,0 +1,7 @@ + +val forall Nat 'N. [|10:'N|] -> [|10:'N|] effect pure return_test + +function forall Nat 'N. [|10:'N|] return_test x = +{ + return x +} diff --git a/test/typecheck/fail/return_simple2.sail b/test/typecheck/fail/return_simple2.sail new file mode 100644 index 00000000..f212a945 --- /dev/null +++ b/test/typecheck/fail/return_simple2.sail @@ -0,0 +1,9 @@ + +val forall Nat 'N. [|10:'N|] -> [|10:'N|] effect pure return_test + +function forall Nat 'N. [|10:'N|] return_test x = +{ + x; + return x; + x +} diff --git a/test/typecheck/fail/return_simple3.sail b/test/typecheck/fail/return_simple3.sail new file mode 100644 index 00000000..df75c5bd --- /dev/null +++ b/test/typecheck/fail/return_simple3.sail @@ -0,0 +1,8 @@ + +val forall Nat 'N. [|10:'N|] -> [|10:'N|] effect pure return_test + +function forall Nat 'N. [|10:'N|] return_test x = +{ + return 9; + x +} diff --git a/test/typecheck/fail/return_simple4.sail b/test/typecheck/fail/return_simple4.sail new file mode 100644 index 00000000..aa7c3010 --- /dev/null +++ b/test/typecheck/fail/return_simple4.sail @@ -0,0 +1,8 @@ + +val forall Nat 'N. [|10:'N|] -> [|10:'N|] effect pure return_test + +function forall Nat 'N. [|10:'N|] return_test x = +{ + return x; + 9 +} diff --git a/test/typecheck/fail/return_simple5.sail b/test/typecheck/fail/return_simple5.sail new file mode 100644 index 00000000..d6947d91 --- /dev/null +++ b/test/typecheck/fail/return_simple5.sail @@ -0,0 +1,8 @@ + +val forall Nat 'N. [|10:'N - 1|] -> [|10:'N - 1|] effect pure return_test + +function forall Nat 'N. [|10:'N - 1|] return_test x = +{ + return x; + sizeof 'N +} diff --git a/test/typecheck/fail/return_simple6.sail b/test/typecheck/fail/return_simple6.sail new file mode 100644 index 00000000..0e118632 --- /dev/null +++ b/test/typecheck/fail/return_simple6.sail @@ -0,0 +1,8 @@ + +val forall Nat 'N. [|10:'N|] -> [|10:'N|] effect pure return_test + +function forall Nat 'N. [|10:'N|] return_test x = +{ + return x; + sizeof 'N +} diff --git a/test/typecheck/fail/set_spsr1.sail b/test/typecheck/fail/set_spsr1.sail new file mode 100644 index 00000000..27c343b2 --- /dev/null +++ b/test/typecheck/fail/set_spsr1.sail @@ -0,0 +1,17 @@ +default Order dec + +val forall Nat 'n, Nat 'l, Nat 'm, Nat 'o, Type 'a, 'l >= 0, 'm <= 'o, 'o <= 'l. + (vector<'n,'l,inc,'a>, [:'m:], [:'o:]) -> vector<'m,'o - 'm,inc,'a> effect pure vector_subrange_inc + +val forall Nat 'n, Nat 'l, Nat 'm, Nat 'o, Type 'a, 'n >= 'm, 'm >= 'o, 'o >= 'n - 'l + 1. + (vector<'n,'l,dec,'a>, [:'m:], [:'o:]) -> vector<'m,'m - 'o - 1,dec,'a> effect pure vector_subrange_dec + +overload vector_subrange [vector_subrange_inc; vector_subrange_dec] + +register bit[32] SPSR_EL2 + +function unit set_SPSR_hyp (bit[32]) val_name = +{ + (bit[32]) r := val_name; + SPSR_EL2[30..0] := r +} diff --git a/test/typecheck/fail/set_spsr2.sail b/test/typecheck/fail/set_spsr2.sail new file mode 100644 index 00000000..00493444 --- /dev/null +++ b/test/typecheck/fail/set_spsr2.sail @@ -0,0 +1,17 @@ +default Order dec + +val forall Nat 'n, Nat 'l, Nat 'm, Nat 'o, Type 'a, 'l >= 0, 'm <= 'o, 'o <= 'l. + (vector<'n,'l,inc,'a>, [:'m:], [:'o:]) -> vector<'m,'o - 'm,inc,'a> effect pure vector_subrange_inc + +val forall Nat 'n, Nat 'l, Nat 'm, Nat 'o, Type 'a, 'n >= 'm, 'm >= 'o, 'o >= 'n - 'l + 1. + (vector<'n,'l,dec,'a>, [:'m:], [:'o:]) -> vector<'m,'m - 'o - 1,dec,'a> effect pure vector_subrange_dec + +overload vector_subrange [vector_subrange_inc; vector_subrange_dec] + +register bit[32] SPSR_EL2 + +function unit set_SPSR_hyp (bit[32]) val_name = +{ + (bit[32]) r := val_name; + SPSR_EL2[0..31] := r +} diff --git a/test/typecheck/fail/set_spsr3.sail b/test/typecheck/fail/set_spsr3.sail new file mode 100644 index 00000000..c3a6208e --- /dev/null +++ b/test/typecheck/fail/set_spsr3.sail @@ -0,0 +1,17 @@ +default Order dec + +val forall Nat 'n, Nat 'l, Nat 'm, Nat 'o, Type 'a, 'l >= 0, 'm <= 'o, 'o <= 'l. + (vector<'n,'l,inc,'a>, [:'m:], [:'o:]) -> vector<'m,'o - 'm,inc,'a> effect pure vector_subrange_inc + +val forall Nat 'n, Nat 'l, Nat 'm, Nat 'o, Type 'a, 'n >= 'm, 'm >= 'o, 'o >= 'n - 'l + 1. + (vector<'n,'l,dec,'a>, [:'m:], [:'o:]) -> vector<'m,'m - 'o - 1,dec,'a> effect pure vector_subrange_dec + +overload vector_subrange [vector_subrange_inc; vector_subrange_dec] + +register bit[32] SPSR_EL2 + +function unit set_SPSR_hyp (bit[32]) val_name = +{ + (bit[32]) r := val_name; + SPSR_EL2[32..1] := r +} diff --git a/test/typecheck/fail/set_spsr4.sail b/test/typecheck/fail/set_spsr4.sail new file mode 100644 index 00000000..65596b59 --- /dev/null +++ b/test/typecheck/fail/set_spsr4.sail @@ -0,0 +1,17 @@ +default Order dec + +val forall Nat 'n, Nat 'l, Nat 'm, Nat 'o, Type 'a, 'l >= 0, 'm <= 'o, 'o <= 'l. + (vector<'n,'l,inc,'a>, [:'m:], [:'o:]) -> vector<'m,'o - 'm,inc,'a> effect pure vector_subrange_inc + +val forall Nat 'n, Nat 'l, Nat 'm, Nat 'o, Type 'a, 'n >= 'm, 'm >= 'o, 'o >= 'n - 'l + 1. + (vector<'n,'l,dec,'a>, [:'m:], [:'o:]) -> vector<'m,'m - 'o - 1,dec,'a> effect pure vector_subrange_dec + +overload vector_subrange [vector_subrange_inc; vector_subrange_dec] + +register bit[31] SPSR_EL2 + +function unit set_SPSR_hyp (bit[32]) val_name = +{ + (bit[32]) r := val_name; + SPSR_EL2[31..0] := r +} diff --git a/test/typecheck/fail/set_spsr5.sail b/test/typecheck/fail/set_spsr5.sail new file mode 100644 index 00000000..d8a6588c --- /dev/null +++ b/test/typecheck/fail/set_spsr5.sail @@ -0,0 +1,17 @@ +default Order dec + +val forall Nat 'n, Nat 'l, Nat 'm, Nat 'o, Type 'a, 'l >= 0, 'm <= 'o, 'o <= 'l. + (vector<'n,'l,inc,'a>, [:'m:], [:'o:]) -> vector<'m,'o - 'm,inc,'a> effect pure vector_subrange_inc + +val forall Nat 'n, Nat 'l, Nat 'm, Nat 'o, Type 'a, 'n >= 'm, 'm >= 'o, 'o >= 'n - 'l + 1. + (vector<'n,'l,dec,'a>, [:'m:], [:'o:]) -> vector<'m,'m - 'o - 1,dec,'a> effect pure vector_subrange_dec + +overload vector_subrange [vector_subrange_inc; vector_subrange_dec] + +register bit[32] SPSR_EL2 + +function unit set_SPSR_hyp (bit[16]) val_name = +{ + (bit[32]) r := val_name; + SPSR_EL2[31..0] := r +} diff --git a/test/typecheck/fail/vec_pat1.sail b/test/typecheck/fail/vec_pat1.sail new file mode 100644 index 00000000..e10838f6 --- /dev/null +++ b/test/typecheck/fail/vec_pat1.sail @@ -0,0 +1,17 @@ +default Order inc + +val extern forall Num 'n. (bit['n], bit['n]) -> bit['n] effect pure bv_add = "bv_add_inc" + +val forall Num 'n, Num 'm, Num 'o, Num 'p, Type 'a. + (vector<'n,'m,inc,'a>, vector<'o,'p,inc,'a>) -> vector<'n,'m + 'p,inc,'a> + effect pure vector_append_inc + +overload (deinfix +) [bv_add] +overload vector_append [vector_append_inc] + +val (bit[3], bit[3]) -> bit[3] effect pure test + +function bit[3] test (((bit[0]) x : 0b11 : 0b0), z) = +{ + (x : 0b11) + z +} diff --git a/test/typecheck/fail/vector_access1.sail b/test/typecheck/fail/vector_access1.sail new file mode 100644 index 00000000..1eef5250 --- /dev/null +++ b/test/typecheck/fail/vector_access1.sail @@ -0,0 +1,12 @@ + +val forall Nat 'n, Nat 'l, Order 'o, Type 'a, 'l >= 0. (vector<'n,'l,'o,'a>, [|'n:'n + 'l - 1|]) -> 'a effect pure vector_access + +default Order inc + +val bit[4] -> unit effect pure test + +function unit test v = +{ + z := vector_access(v,0); + z := v[4] +}
\ No newline at end of file diff --git a/test/typecheck/fail/vector_access2.sail b/test/typecheck/fail/vector_access2.sail new file mode 100644 index 00000000..0b4ba7c2 --- /dev/null +++ b/test/typecheck/fail/vector_access2.sail @@ -0,0 +1,12 @@ + +val forall Nat 'n, Nat 'l, Order 'o, Type 'a, 'l >= 0. (vector<'n,'l,'o,'a>, [|'n:'n + 'l - 1|]) -> 'a effect pure vector_access + +default Order inc + +val bit[4] -> unit effect pure test + +function unit test v = +{ + z := vector_access(v,-1); + z := v[3] +}
\ No newline at end of file diff --git a/test/typecheck/fail/vector_access3.sail b/test/typecheck/fail/vector_access3.sail new file mode 100644 index 00000000..dd43cfea --- /dev/null +++ b/test/typecheck/fail/vector_access3.sail @@ -0,0 +1,12 @@ + +val forall Nat 'n, Nat 'l, Order 'o, Type 'a, 'l >= 0. (vector<'n,'l,'o,'a>, [|'n:'n + 'l - 1|]) -> 'a effect pure vector_access + +default Order inc + +val bit[0] -> unit effect pure test + +function unit test v = +{ + z := vector_access(v,0); + z := v[0] +}
\ No newline at end of file diff --git a/test/typecheck/fail/vector_access4.sail b/test/typecheck/fail/vector_access4.sail new file mode 100644 index 00000000..31d34eae --- /dev/null +++ b/test/typecheck/fail/vector_access4.sail @@ -0,0 +1,12 @@ + +val forall Nat 'n, Nat 'l, Order 'o, Type 'a, 'l >= 0. (vector<'n,'l,'o,'a>, [|'n:'n + 'l - 1|]) -> 'a effect pure vector_access + +default Order inc + +val bit[-5] -> unit effect pure test + +function unit test v = +{ + z := vector_access(v,([|0:-5|]) -1); + z := v[-1] +}
\ No newline at end of file diff --git a/test/typecheck/fail/vector_append1.sail b/test/typecheck/fail/vector_append1.sail new file mode 100644 index 00000000..e2429380 --- /dev/null +++ b/test/typecheck/fail/vector_append1.sail @@ -0,0 +1,18 @@ + +val forall Nat 'n, Nat 'l, Order 'o, Type 'a, 'l >= 0. (vector<'n,'l,'o,'a>, [|'n:'n + 'l - 1|]) -> 'a effect pure vector_access + +val forall Nat 'n1, Nat 'l1, Nat 'n2, Nat 'l2, Order 'o, Type 'a, 'l1 >= 0, 'l2 >= 0. + (vector<'n1,'l1,'o,'a>, vector<'n2,'l2,'o,'a>) -> vector<'n1,'l1 + 'l2,'o,'a> effect pure vector_append + +default Order inc + +val (bit[4], bit[4]) -> bit[7] effect pure test + +function bit[7] test (v1, v2) = +{ + z := vector_access(v1, 3); + z := v1[0]; + zv := vector_append(v1, v2); + zv := v1 : v2; + zv +}
\ No newline at end of file diff --git a/test/typecheck/fail/vector_append2.sail b/test/typecheck/fail/vector_append2.sail new file mode 100644 index 00000000..acaeb0b0 --- /dev/null +++ b/test/typecheck/fail/vector_append2.sail @@ -0,0 +1,18 @@ + +val forall Nat 'n, Nat 'l, Order 'o, Type 'a, 'l >= 0. (vector<'n,'l,'o,'a>, [|'n:'n + 'l - 1|]) -> 'a effect pure vector_access + +val forall Nat 'n1, Nat 'l1, Nat 'n2, Nat 'l2, Order 'o, Type 'a, 'l1 >= 0, 'l2 >= 0. + (vector<'n1,'l1,'o,'a>, vector<'n2,'l2,'o,'a>) -> vector<'n1,'l1 + 'l2,'o,'a> effect pure vector_append + +default Order inc + +val (bit[4], bit[4]) -> bit[9] effect pure test + +function bit[9] test (v1, v2) = +{ + z := vector_access(v1, 3); + z := v1[0]; + zv := vector_append(v1, v2); + zv := v1 : v2; + zv +}
\ No newline at end of file diff --git a/test/typecheck/fail/vector_append3.sail b/test/typecheck/fail/vector_append3.sail new file mode 100644 index 00000000..82f0a861 --- /dev/null +++ b/test/typecheck/fail/vector_append3.sail @@ -0,0 +1,18 @@ +val forall Nat 'n, Nat 'l, Type 'a, 'l >= 0. (vector<'n,'l,dec,'a>, [|'n - 'l + 1:'n|]) -> 'a effect pure vector_access_dec +val forall Nat 'n, Nat 'l, Type 'a, 'l >= 0. (vector<'n,'l,inc,'a>, [|'n:'n + 'l - 1|]) -> 'a effect pure vector_access_inc + +val forall Nat 'n1, Nat 'l1, Nat 'n2, Nat 'l2, Order 'o, Type 'a, 'l1 >= 0, 'l2 >= 0. + (vector<'n1,'l1,'o,'a>, vector<'n2,'l2,'o,'a>) -> vector<'n1,'l1 + 'l2,'o,'a> effect pure vector_append + +default Order inc + +val (bit[4], bit[4]) -> bit[7] effect pure test + +function bit[7] test (v1, v2) = +{ + z := vector_access(v1, 3); + z := v1[0]; + zv := vector_append(v1, v2); + zv := v1 : v2; + zv +}
\ No newline at end of file diff --git a/test/typecheck/fail/vector_append_gen1.sail b/test/typecheck/fail/vector_append_gen1.sail new file mode 100644 index 00000000..727d5c14 --- /dev/null +++ b/test/typecheck/fail/vector_append_gen1.sail @@ -0,0 +1,14 @@ + +val forall Nat 'n, Nat 'l, Order 'o, Type 'a, 'l >= 0. (vector<'n,'l,'o,'a>, [|'n:'n + 'l - 1|]) -> 'a effect pure vector_access + +val forall Nat 'n1, Nat 'l1, Nat 'n2, Nat 'l2, Order 'o, Type 'a, 'l1 >= 0, 'l2 >= 0. + (vector<'n1,'l1,'o,'a>, vector<'n2,'l2,'o,'a>) -> vector<'n1,'l1 + 'l2,'o,'a> effect pure vector_append + +default Order inc + +val forall 'n, 'm. (bit['n], bit['m]) -> bit['n + 'm] effect pure test + +function forall 'n, 'm. bit['n + 'm] test (v1, v2) = +{ + v1 : v2; +}
\ No newline at end of file diff --git a/test/typecheck/fail/vector_append_gen2.sail b/test/typecheck/fail/vector_append_gen2.sail new file mode 100644 index 00000000..8e534253 --- /dev/null +++ b/test/typecheck/fail/vector_append_gen2.sail @@ -0,0 +1,14 @@ + +val forall Nat 'n, Nat 'l, Order 'o, Type 'a, 'l >= 0. (vector<'n,'l,'o,'a>, [|'n:'n + 'l - 1|]) -> 'a effect pure vector_access + +val forall Nat 'n1, Nat 'l1, Nat 'n2, Nat 'l2, Order 'o, Type 'a, 'l1 >= 0, 'l2 >= 0. + (vector<'n1,'l1,'o,'a>, vector<'n2,'l2,'o,'a>) -> vector<'n1,'l1 + 'l2,'o,'a> effect pure vector_append + +default Order inc + +val forall 'n, 'm. (bit['n], bit['m]) -> bit['n + 'm] effect pure test + +function forall 'n, 'm. bit['n + 'm] test (v1, v2) = +{ + vector_append(v1, v2); +}
\ No newline at end of file diff --git a/test/typecheck/fail/vector_arity.sail b/test/typecheck/fail/vector_arity.sail new file mode 100644 index 00000000..6ecc9565 --- /dev/null +++ b/test/typecheck/fail/vector_arity.sail @@ -0,0 +1,4 @@ + +val vector<0,5,inc,bit,bit> -> vector<0,5,inc,bit,bit> effect pure test + +function vector<0,5,inc,bit,bit> test x = x
\ No newline at end of file diff --git a/test/typecheck/fail/vector_subrange_gen1.sail b/test/typecheck/fail/vector_subrange_gen1.sail new file mode 100644 index 00000000..0ae6f9f9 --- /dev/null +++ b/test/typecheck/fail/vector_subrange_gen1.sail @@ -0,0 +1,20 @@ + +val forall Nat 'n, Nat 'l, Order 'o, Type 'a, 'l >= 0. (vector<'n,'l,'o,'a>, [|'n:'n + 'l - 1|]) -> 'a effect pure vector_access + +val forall Nat 'n1, Nat 'l1, Nat 'n2, Nat 'l2, Order 'o, Type 'a, 'l1 >= 0, 'l2 >= 0. + (vector<'n1,'l1,'o,'a>, vector<'n2,'l2,'o,'a>) -> vector<'n1,'l1 + 'l2,'o,'a> effect pure vector_append + +val forall Nat 'n, Nat 'l, Nat 'm, Nat 'u, Order 'o, Type 'a, 'l >= 0, 'm <= 'u, 'u <= 'l. (vector<'n,'l,'o,'a>, [:'m:], [:'u:]) -> vector<'m,'u - 'm,'o,'a> effect pure vector_subrange + +val forall Nat 'n, Nat 'm. ([:'n:], [:'m:]) -> [:'n - 'm:] effect pure minus + +default Order inc + +val forall 'n, 'm, 'n >= 5. bit['n] -> bit['n - 2] effect pure test + +function forall 'n, 'n >= 5. bit['n - 3] test v = +{ + z := vector_subrange(v, 0, minus(sizeof 'n, 3)); + z := v[0 .. minus(sizeof 'n, 2)]; + z +}
\ No newline at end of file diff --git a/test/typecheck/fail/word_width_bytes_mips.sail b/test/typecheck/fail/word_width_bytes_mips.sail new file mode 100644 index 00000000..91f3e787 --- /dev/null +++ b/test/typecheck/fail/word_width_bytes_mips.sail @@ -0,0 +1,11 @@ +typedef WordType = enumerate {B; H; W; D} + +(* This fails because it's not true for all combinations of 'r and WordType *) +(* Needs existential types, i.e. return type should be exists Nat 'r, 'r in {1,2,4,8}. [:'r:] *) +function forall Nat 'r, 'r IN {1,2,4,8}. wordWidthBytes((WordType) w) = + switch(w) { + case B -> 1 + case H -> 2 + case W -> 4 + case D -> 8 + } diff --git a/test/typecheck/pass/add_vec_lit.sail b/test/typecheck/pass/add_vec_lit.sail new file mode 100644 index 00000000..be897021 --- /dev/null +++ b/test/typecheck/pass/add_vec_lit.sail @@ -0,0 +1,10 @@ +default Order inc + +val extern forall Num 'n. (bit['n], bit['n]) -> bit['n] effect pure add_vec = "add_vec" +val extern forall Num 'n, Num 'm, Num 'o, Num 'p. ([|'n:'m|], [|'o:'p|]) -> [|'n+'o:'m+'p|] effect pure add_range = "add_range" + +val cast forall Num 'n. bit['n] -> [|0: 2** 'n - 1|] effect pure cast_vec_range + +overload (deinfix +) [add_vec; add_range] + +let (range<0,30>) x = 0xF + 0x2 diff --git a/test/typecheck/pass/arm_FPEXC1.sail b/test/typecheck/pass/arm_FPEXC1.sail new file mode 100644 index 00000000..cfae86a1 --- /dev/null +++ b/test/typecheck/pass/arm_FPEXC1.sail @@ -0,0 +1,53 @@ +default Order dec + +val forall Num 'n. (bit['n], int) -> bit effect pure vector_access + +val forall Num 'n, Num 'm, Num 'o, 'm >= 'o, 'o >= 0, 'n >= 'm + 1. + (bit['n], [:'m:], [:'o:]) -> bit['m - ('o - 1)] effect pure vector_subrange + +register vector<32 - 1, 32, dec, bit> _FPEXC32_EL2 + +val vector<32 - 1, 32, dec, bit> -> unit effect {wreg} set_FPEXC32_EL2 + +function set_FPEXC32_EL2 value_name = + { + _FPEXC32_EL2[0..0] := [value_name[0]]; + _FPEXC32_EL2[1..1] := [value_name[1]]; + _FPEXC32_EL2[2..2] := [value_name[2]]; + _FPEXC32_EL2[3..3] := [value_name[3]]; + _FPEXC32_EL2[4..4] := [value_name[4]]; + _FPEXC32_EL2[6..5] := value_name[6 .. 5]; + _FPEXC32_EL2[7..7] := [value_name[7]]; + _FPEXC32_EL2[20..11] := value_name[20 .. 11]; + _FPEXC32_EL2[29..29] := [value_name[29]]; + _FPEXC32_EL2[30..30] := [value_name[30]] + } + +val unit -> vector<32 - 1, 32, dec, bit> effect {rreg} get_FPEXC32_EL2 + +function get_FPEXC32_EL2 () = + { + (vector<32 - 1, 32, dec, bit> ) value_name := 0x04000700; + value_name[0..0] := [_FPEXC32_EL2[0]]; + value_name[1..1] := [_FPEXC32_EL2[1]]; + value_name[2..2] := [_FPEXC32_EL2[2]]; + value_name[3..3] := [_FPEXC32_EL2[3]]; + value_name[4..4] := [_FPEXC32_EL2[4]]; + value_name[6..5] := _FPEXC32_EL2[6 .. 5]; + value_name[7..7] := [_FPEXC32_EL2[7]]; + value_name[20..11] := _FPEXC32_EL2[20 .. 11]; + value_name[26..26] := [_FPEXC32_EL2[26]]; + value_name[29..29] := [_FPEXC32_EL2[29]]; + value_name[30..30] := [_FPEXC32_EL2[30]]; + value_name + } + +val vector<32 - 1, 32, dec, bit> -> unit effect {rreg, wreg} set_FPEXC + +function set_FPEXC val_name = + { + (vector<32 - 1, 32, dec, bit> ) r := val_name; + (vector<32 - 1, 32, dec, bit> ) __tmp_45 := get_FPEXC32_EL2(); + __tmp_45[31..0] := r; + set_FPEXC32_EL2(__tmp_45) + } diff --git a/test/typecheck/pass/arm_types.sail b/test/typecheck/pass/arm_types.sail new file mode 100644 index 00000000..d7244beb --- /dev/null +++ b/test/typecheck/pass/arm_types.sail @@ -0,0 +1,140 @@ + +typedef boolean = enumerate {FALSE; TRUE} + +typedef signal = enumerate {LOW; HIGH} + +typedef __RetCode = + enumerate {__RC_OK; + __RC_UNDEFINED; + __RC_UNPREDICTABLE; + __RC_SEE; + __RC_IMPLEMENTATION_DEFINED; + __RC_SUBARCHITECTURE_DEFINED; + __RC_EXCEPTION_TAKEN; + __RC_ASSERT_FAILED; + __RC_UNMATCHED_CASE} + +typedef TUBE_Type = bit[32] + +typedef ScheduleIRQ_Type = bit[32] + +typedef ClearIRQ_Type = bit[32] + +typedef ScheduleFIQ_Type = bit[32] + +typedef ClearFIQ_Type = bit[32] + +typedef TargetCPU_Type = bit[32] + +typedef AbortRgn64Lo1_Type = bit[32] + +typedef AbortRgn64Lo1_Hi_Type = bit[32] + +typedef AbortRgn64Hi1_Type = bit[32] + +typedef AbortRgn64Hi1_Hi_Type = bit[32] + +typedef AbortRgn64Lo2_Type = bit[32] + +typedef AbortRgn64Lo2_Hi_Type = bit[32] + +typedef AbortRgn64Hi2_Type = bit[32] + +typedef AbortRgn64Hi2_Hi_Type = bit[32] + +typedef AXIAbortCtl_Type = bit[32] + +typedef GTE_API_Type = bit[32] + +typedef GTE_API_PARAM_Type = bit[32] + +typedef GTE_API_STATUS_Type = bit[32] + +typedef PPURBAR_Type = bit[32] + +typedef PPURSER_Type = bit[32] + +typedef PPURACR_Type = bit[32] + +typedef GTE_API_STATUS_64_Type = bit[32] + +typedef GTE_API_STATUS_64_HI_Type = bit[32] + +typedef GTE_API_PARAM_64_Type = bit[32] + +typedef GTE_API_PARAM_64_HI_Type = bit[32] + +typedef MemAtomicOp = + enumerate {MemAtomicOp_ADD; + MemAtomicOp_BIC; + MemAtomicOp_EOR; + MemAtomicOp_ORR; + MemAtomicOp_SMAX; + MemAtomicOp_SMIN; + MemAtomicOp_UMAX; + MemAtomicOp_UMIN; + MemAtomicOp_SWP} + +typedef SCRType = bit[32] + +typedef SCTLRType = bit[32] + +typedef MAIRType = bit[64] + +typedef ESRType = bit[32] + +typedef FPCRType = bit[32] + +typedef FPSRType = bit[32] + +typedef FPSCRType = bit[32] + +typedef CPSRType = bit[32] + +typedef APSRType = bit[32] + +typedef ITSTATEType = bit[8] + +typedef CPACRType = bit[32] + +typedef CNTKCTLType = bit[32] + +typedef GTEParamType = enumerate {GTEParam_WORD; GTEParam_LIST; GTEParam_EOACCESS} + +typedef GTE_PPU_SizeEn_Type = bit[32] + +typedef GTEExtObsAccess_Type = bit[16] + +typedef GTEASAccess_Type = bit[32] + +typedef GTEASRecordedAccess_Type = bit[32] + +typedef AccType = + enumerate {AccType_NORMAL; + AccType_VEC; + AccType_STREAM; + AccType_VECSTREAM; + AccType_ATOMIC; + AccType_ORDERED; + AccType_UNPRIV; + AccType_IFETCH; + AccType_PTW; + AccType_DC; + AccType_IC; + AccType_DCZVA; + AccType_AT} + +typedef MemType = enumerate {MemType_Normal; MemType_Device} + +typedef DeviceType = + enumerate {DeviceType_GRE; DeviceType_nGRE; DeviceType_nGnRE; DeviceType_nGnRnE} + +typedef MemAttrHints = const struct {bit[2] attrs; bit[2] hints; bool transient;} + +typedef MemoryAttributes = + const struct {MemType type; + DeviceType device; + MemAttrHints inner; + MemAttrHints outer; + bool shareable; + bool outershareable;} diff --git a/test/typecheck/pass/assignment_simple.sail b/test/typecheck/pass/assignment_simple.sail new file mode 100644 index 00000000..dc0c78d8 --- /dev/null +++ b/test/typecheck/pass/assignment_simple.sail @@ -0,0 +1,16 @@ + +val ([:10:], unit) -> [:10:] effect pure f + +function [:10:] f (x, y) = x + +val unit -> [:10:] effect pure test + +function [:10:] test () = +{ + z := 10; + z +} + +val unit -> unit effect pure test2 + +function unit test2 () = x := 10
\ No newline at end of file diff --git a/test/typecheck/pass/bitwise_not.sail b/test/typecheck/pass/bitwise_not.sail new file mode 100644 index 00000000..1c4f8d3b --- /dev/null +++ b/test/typecheck/pass/bitwise_not.sail @@ -0,0 +1,7 @@ +val forall Nat 'n, Nat 'm, Order 'o. vector<'n,'m,'o,bit> -> vector<'n,'m,'o,bit> effect pure bitwise_not + +default Order dec + +val bit[5] -> bit[5] effect pure test + +function bit[5] test ((bit[5]) x) = bitwise_not(x)
\ No newline at end of file diff --git a/test/typecheck/pass/bitwise_not_gen.sail b/test/typecheck/pass/bitwise_not_gen.sail new file mode 100644 index 00000000..6d36c566 --- /dev/null +++ b/test/typecheck/pass/bitwise_not_gen.sail @@ -0,0 +1,8 @@ + +val forall Nat 'n, Nat 'm, Order 'o. vector<'n,'m,'o,bit> -> vector<'n,'m,'o,bit> effect pure bitwise_not + +default Order dec + +val forall 'n. bit['n] -> bit['n] effect pure test + +function forall 'n. bit['n] test ((bit['n]) x) = bitwise_not(bitwise_not(x)) diff --git a/test/typecheck/pass/bitwise_not_x3.sail b/test/typecheck/pass/bitwise_not_x3.sail new file mode 100644 index 00000000..49d962a6 --- /dev/null +++ b/test/typecheck/pass/bitwise_not_x3.sail @@ -0,0 +1,7 @@ +val forall Nat 'n, Nat 'm, Order 'o. vector<'n,'m,'o,bit> -> vector<'n,'m,'o,bit> effect pure bitwise_not + +default Order dec + +val bit[5] -> bit[5] effect pure test + +function bit[5] test ((bit[5]) x) = bitwise_not(bitwise_not(bitwise_not(x)))
\ No newline at end of file diff --git a/test/typecheck/pass/bv_simple_index.sail b/test/typecheck/pass/bv_simple_index.sail new file mode 100644 index 00000000..72e1b094 --- /dev/null +++ b/test/typecheck/pass/bv_simple_index.sail @@ -0,0 +1,11 @@ +val forall Nat 'n, Nat 'l, Type 'a, 'l >= 0. (vector<'n,'l,dec,'a>, [|'n - 'l + 1:'n|]) -> 'a effect pure vector_access_dec +val forall Nat 'n, Nat 'l, Type 'a, 'l >= 0. (vector<'n,'l,inc,'a>, [|'n:'n + 'l - 1|]) -> 'a effect pure vector_access_inc + +overload vector_access [vector_access_inc; vector_access_dec] + +val cast bit -> bool effect pure cast_bit_bool + +function bool bv ((bit[64]) x) = +{ + x[32] +} diff --git a/test/typecheck/pass/bv_simple_index_bit.sail b/test/typecheck/pass/bv_simple_index_bit.sail new file mode 100644 index 00000000..2ba5b928 --- /dev/null +++ b/test/typecheck/pass/bv_simple_index_bit.sail @@ -0,0 +1,9 @@ +val forall Nat 'n, Nat 'l, Type 'a, 'l >= 0. (vector<'n,'l,dec,'a>, [|'n - 'l + 1:'n|]) -> 'a effect pure vector_access_dec +val forall Nat 'n, Nat 'l, Type 'a, 'l >= 0. (vector<'n,'l,inc,'a>, [|'n:'n + 'l - 1|]) -> 'a effect pure vector_access_inc + +overload vector_access [vector_access_inc; vector_access_dec] + +function bit bv ((bit[64]) x) = +{ + x[32] +} diff --git a/test/typecheck/pass/case_simple1.sail b/test/typecheck/pass/case_simple1.sail new file mode 100644 index 00000000..e4a81a36 --- /dev/null +++ b/test/typecheck/pass/case_simple1.sail @@ -0,0 +1,9 @@ + +val forall Nat 'N. ([:10:], [|10:'N|]) -> [|10:'N|] effect pure case_test + +function forall Nat 'N. [|10:'N|] case_test (x, y) = +{ + switch (x, y) { + case _ -> y + } +} diff --git a/test/typecheck/pass/case_simple2.sail b/test/typecheck/pass/case_simple2.sail new file mode 100644 index 00000000..0ffba780 --- /dev/null +++ b/test/typecheck/pass/case_simple2.sail @@ -0,0 +1,9 @@ + +val forall Nat 'N, 'N >= 10. ([:10:], [|10:'N|]) -> [|10:'N|] effect pure case_test + +function forall Nat 'N. [|10:'N|] case_test (x, y) = +{ + switch (x, y) { + case _ -> x + } +} diff --git a/test/typecheck/pass/case_simple_constraints.sail b/test/typecheck/pass/case_simple_constraints.sail new file mode 100644 index 00000000..f1b87235 --- /dev/null +++ b/test/typecheck/pass/case_simple_constraints.sail @@ -0,0 +1,18 @@ + +val forall Nat 'n, Nat 'm. ([:'n + 20:], [:'m:]) -> [:'n + 20 + 'm:] effect pure plus + +val forall Nat 'n, 'n <= -10. [:'n:] -> [:'n:] effect pure minus_ten_id + +val forall Nat 'n, 'n >= 10. [:'n:] -> [:'n:] effect pure ten_id + +val forall Nat 'N, 'N >= 63. [|10:'N|] -> [|10:'N|] effect pure branch + +function forall Nat 'N, 'N >= 63. [|10:'N|] branch x = +{ + switch x { + case ([|10:30|]) y -> y + case ([:31:]) _ -> sizeof 'N + case ([|31:40|]) _ -> plus(60,3) + } +} +and branch (([|51:63|]) _) = ten_id(sizeof 'N) diff --git a/test/typecheck/pass/cast_lexp1.sail b/test/typecheck/pass/cast_lexp1.sail new file mode 100644 index 00000000..b8b29b87 --- /dev/null +++ b/test/typecheck/pass/cast_lexp1.sail @@ -0,0 +1,7 @@ + +val unit -> int effect pure test + +function int test () = { + (int) y := 10; + y +} diff --git a/test/typecheck/pass/cast_lexp2.sail b/test/typecheck/pass/cast_lexp2.sail new file mode 100644 index 00000000..a6f6d299 --- /dev/null +++ b/test/typecheck/pass/cast_lexp2.sail @@ -0,0 +1,7 @@ + +val unit -> int effect pure test + +function int test () = { + (nat) y := 10; + y +} diff --git a/test/typecheck/pass/cast_simple.sail b/test/typecheck/pass/cast_simple.sail new file mode 100644 index 00000000..c1507f26 --- /dev/null +++ b/test/typecheck/pass/cast_simple.sail @@ -0,0 +1,7 @@ + +val unit -> int effect pure test + +function int test () = { + (nat) y := ([|0:10|]) 10; + (int) y +} diff --git a/test/typecheck/pass/cons_pattern.sail b/test/typecheck/pass/cons_pattern.sail new file mode 100644 index 00000000..107bd6d5 --- /dev/null +++ b/test/typecheck/pass/cons_pattern.sail @@ -0,0 +1,8 @@ + +function unit test ((list<bit>) xs) = +{ + switch xs { + case x :: xs -> () + case [||||] -> () + } +} diff --git a/test/typecheck/pass/default_order.sail b/test/typecheck/pass/default_order.sail new file mode 100644 index 00000000..a283b221 --- /dev/null +++ b/test/typecheck/pass/default_order.sail @@ -0,0 +1 @@ +default Order dec diff --git a/test/typecheck/pass/deinfix_plus.sail b/test/typecheck/pass/deinfix_plus.sail new file mode 100644 index 00000000..c5a0f1ee --- /dev/null +++ b/test/typecheck/pass/deinfix_plus.sail @@ -0,0 +1,12 @@ +default Order inc + +val extern forall Num 'n. (bit['n], bit['n]) -> bit['n] effect pure bv_add = "bv_add_inc" + +overload (deinfix +) [bv_add] + +val (bit[3], bit[3]) -> bit[3] effect pure test + +function bit[3] test (x, y) = +{ + x + y +} diff --git a/test/typecheck/pass/exit1.sail b/test/typecheck/pass/exit1.sail new file mode 100644 index 00000000..92515c5a --- /dev/null +++ b/test/typecheck/pass/exit1.sail @@ -0,0 +1,8 @@ + +val unit -> [:6:] effect {escape} test + +function [:6:] test () = +{ + exit (); + 6 +} diff --git a/test/typecheck/pass/exit2.sail b/test/typecheck/pass/exit2.sail new file mode 100644 index 00000000..574302cc --- /dev/null +++ b/test/typecheck/pass/exit2.sail @@ -0,0 +1,7 @@ + +val unit -> [:6:] effect {escape} test + +function [:6:] test () = +{ + exit (); +} diff --git a/test/typecheck/pass/exit3.sail b/test/typecheck/pass/exit3.sail new file mode 100644 index 00000000..e26ff95c --- /dev/null +++ b/test/typecheck/pass/exit3.sail @@ -0,0 +1,7 @@ + +val forall Type 'a. unit -> 'a effect {escape} test + +function forall Type 'a. 'a test () = +{ + exit (); +} diff --git a/test/typecheck/pass/flow_gt1.sail b/test/typecheck/pass/flow_gt1.sail new file mode 100644 index 00000000..acfbab68 --- /dev/null +++ b/test/typecheck/pass/flow_gt1.sail @@ -0,0 +1,28 @@ +default Order inc + +val forall Num 'n, Num 'm, Num 'o, Num 'p. ([|'n:'m|], [|'o:'p|]) -> [|'n+'o:'m+'p|] effect pure add_range + +val forall Num 'n, Num 'm, Num 'o, Num 'p. ([|'n:'m|], [|'o:'p|]) -> [|'n-'p:'m-'o|] effect pure sub_range + +val forall Num 'n, Num 'm, Num 'o. ([|'n:'m|], [:'o:]) -> bool effect pure lt_range_atom +val forall Num 'n, Num 'm, Num 'o. ([|'n:'m|], [:'o:]) -> bool effect pure lteq_range_atom +val forall Num 'n, Num 'm, Num 'o. ([|'n:'m|], [:'o:]) -> bool effect pure gt_range_atom +val forall Num 'n, Num 'm, Num 'o. ([|'n:'m|], [:'o:]) -> bool effect pure gteq_range_atom +val forall Num 'n, Num 'm, Num 'o. ([:'n:], [|'m:'o|]) -> bool effect pure lt_atom_range +val forall Num 'n, Num 'm, Num 'o. ([:'n:], [|'m:'o|]) -> bool effect pure lteq_atom_range +val forall Num 'n, Num 'm, Num 'o. ([:'n:], [|'m:'o|]) -> bool effect pure gt_atom_range +val forall Num 'n, Num 'm, Num 'o. ([:'n:], [|'m:'o|]) -> bool effect pure gteq_atom_range + +overload (deinfix +) [add_range] +overload (deinfix -) [sub_range] +overload (deinfix <) [lt_atom_range; lt_range_atom] +overload (deinfix <=) [lteq_atom_range; lteq_range_atom] +overload (deinfix >) [gt_atom_range; gt_range_atom] +overload (deinfix >=) [gteq_atom_range; gteq_range_atom] + +function ([|63|]) branch (([|63|]) x) = +{ + if (x > 31) + then x - 32 + else x + 32 +} diff --git a/test/typecheck/pass/flow_gteq1.sail b/test/typecheck/pass/flow_gteq1.sail new file mode 100644 index 00000000..8918438c --- /dev/null +++ b/test/typecheck/pass/flow_gteq1.sail @@ -0,0 +1,28 @@ +default Order inc + +val forall Num 'n, Num 'm, Num 'o, Num 'p. ([|'n:'m|], [|'o:'p|]) -> [|'n+'o:'m+'p|] effect pure add_range + +val forall Num 'n, Num 'm, Num 'o, Num 'p. ([|'n:'m|], [|'o:'p|]) -> [|'n-'p:'m-'o|] effect pure sub_range + +val forall Num 'n, Num 'm, Num 'o. ([|'n:'m|], [:'o:]) -> bool effect pure lt_range_atom +val forall Num 'n, Num 'm, Num 'o. ([|'n:'m|], [:'o:]) -> bool effect pure lteq_range_atom +val forall Num 'n, Num 'm, Num 'o. ([|'n:'m|], [:'o:]) -> bool effect pure gt_range_atom +val forall Num 'n, Num 'm, Num 'o. ([|'n:'m|], [:'o:]) -> bool effect pure gteq_range_atom +val forall Num 'n, Num 'm, Num 'o. ([:'n:], [|'m:'o|]) -> bool effect pure lt_atom_range +val forall Num 'n, Num 'm, Num 'o. ([:'n:], [|'m:'o|]) -> bool effect pure lteq_atom_range +val forall Num 'n, Num 'm, Num 'o. ([:'n:], [|'m:'o|]) -> bool effect pure gt_atom_range +val forall Num 'n, Num 'm, Num 'o. ([:'n:], [|'m:'o|]) -> bool effect pure gteq_atom_range + +overload (deinfix +) [add_range] +overload (deinfix -) [sub_range] +overload (deinfix <) [lt_atom_range; lt_range_atom] +overload (deinfix <=) [lteq_atom_range; lteq_range_atom] +overload (deinfix >) [gt_atom_range; gt_range_atom] +overload (deinfix >=) [gteq_atom_range; gteq_range_atom] + +function ([|63|]) branch (([|63|]) x) = +{ + if (x >= 32) + then x - 32 + else x + 32 +} diff --git a/test/typecheck/pass/flow_lt1.sail b/test/typecheck/pass/flow_lt1.sail new file mode 100644 index 00000000..0f3c1bbc --- /dev/null +++ b/test/typecheck/pass/flow_lt1.sail @@ -0,0 +1,19 @@ +default Order inc + +val forall Num 'n, Num 'm, Num 'o, Num 'p. ([|'n:'m|], [|'o:'p|]) -> [|'n+'o:'m+'p|] effect pure add_range + +val forall Num 'n, Num 'm, Num 'o, Num 'p. ([|'n:'m|], [|'o:'p|]) -> [|'n-'p:'m-'o|] effect pure sub_range + +val forall Num 'n, Num 'm, Num 'o. ([|'n:'m|], [:'o:]) -> bool effect pure lt_range_atom +val forall Num 'n, Num 'm, Num 'o. ([:'n:], [|'m:'o|]) -> bool effect pure lt_atom_range + +overload (deinfix +) [add_range] +overload (deinfix -) [sub_range] +overload (deinfix <) [lt_atom_range; lt_range_atom] + +function ([|63|]) branch (([|63|]) x) = +{ + if (x < 32) + then x + 32 + else x - 32 +} diff --git a/test/typecheck/pass/flow_lt2.sail b/test/typecheck/pass/flow_lt2.sail new file mode 100644 index 00000000..effe0bc4 --- /dev/null +++ b/test/typecheck/pass/flow_lt2.sail @@ -0,0 +1,19 @@ +default Order inc + +val forall Num 'n, Num 'm, Num 'o, Num 'p. ([|'n:'m|], [|'o:'p|]) -> [|'n+'o:'m+'p|] effect pure add_range + +val forall Num 'n, Num 'm, Num 'o, Num 'p. ([|'n:'m|], [|'o:'p|]) -> [|'n-'p:'m-'o|] effect pure sub_range + +val forall Num 'n, Num 'm, Num 'o. ([|'n:'m|], [:'o:]) -> bool effect pure lt_range_atom +val forall Num 'n, Num 'm, Num 'o. ([:'n:], [|'m:'o|]) -> bool effect pure lt_atom_range + +overload (deinfix +) [add_range] +overload (deinfix -) [sub_range] +overload (deinfix <) [lt_atom_range; lt_range_atom] + +function ([|63|]) branch (([|63|]) x) = +{ + if (x < 32) + then x + 2 + else x - 2 +} diff --git a/test/typecheck/pass/flow_lt_assign.sail b/test/typecheck/pass/flow_lt_assign.sail new file mode 100644 index 00000000..4e787741 --- /dev/null +++ b/test/typecheck/pass/flow_lt_assign.sail @@ -0,0 +1,23 @@ +default Order inc + +val forall Num 'n, Num 'm, Num 'o, Num 'p. ([|'n:'m|], [|'o:'p|]) -> [|'n+'o:'m+'p|] effect pure add_range + +val forall Num 'n, Num 'm, Num 'o, Num 'p. ([|'n:'m|], [|'o:'p|]) -> [|'n-'p:'m-'o|] effect pure sub_range + +val forall Num 'n, Num 'm, Num 'o. ([|'n:'m|], [:'o:]) -> bool effect pure lt_range_atom +val forall Num 'n, Num 'm, Num 'o. ([:'n:], [|'m:'o|]) -> bool effect pure lt_atom_range + +overload (deinfix +) [add_range] +overload (deinfix -) [sub_range] +overload (deinfix <) [lt_atom_range; lt_range_atom] + +function ([|63|]) branch (([|63|]) x) = +{ + y := x; + if (y < 32) + then { + y := 31; + y + 32 + } + else y - 32 +} diff --git a/test/typecheck/pass/flow_lteq1.sail b/test/typecheck/pass/flow_lteq1.sail new file mode 100644 index 00000000..d32831a2 --- /dev/null +++ b/test/typecheck/pass/flow_lteq1.sail @@ -0,0 +1,28 @@ +default Order inc + +val forall Num 'n, Num 'm, Num 'o, Num 'p. ([|'n:'m|], [|'o:'p|]) -> [|'n+'o:'m+'p|] effect pure add_range + +val forall Num 'n, Num 'm, Num 'o, Num 'p. ([|'n:'m|], [|'o:'p|]) -> [|'n-'p:'m-'o|] effect pure sub_range + +val forall Num 'n, Num 'm, Num 'o. ([|'n:'m|], [:'o:]) -> bool effect pure lt_range_atom +val forall Num 'n, Num 'm, Num 'o. ([|'n:'m|], [:'o:]) -> bool effect pure lteq_range_atom +val forall Num 'n, Num 'm, Num 'o. ([|'n:'m|], [:'o:]) -> bool effect pure gt_range_atom +val forall Num 'n, Num 'm, Num 'o. ([|'n:'m|], [:'o:]) -> bool effect pure gteq_range_atom +val forall Num 'n, Num 'm, Num 'o. ([:'n:], [|'m:'o|]) -> bool effect pure lt_atom_range +val forall Num 'n, Num 'm, Num 'o. ([:'n:], [|'m:'o|]) -> bool effect pure lteq_atom_range +val forall Num 'n, Num 'm, Num 'o. ([:'n:], [|'m:'o|]) -> bool effect pure gt_atom_range +val forall Num 'n, Num 'm, Num 'o. ([:'n:], [|'m:'o|]) -> bool effect pure gteq_atom_range + +overload (deinfix +) [add_range] +overload (deinfix -) [sub_range] +overload (deinfix <) [lt_atom_range; lt_range_atom] +overload (deinfix <=) [lteq_atom_range; lteq_range_atom] +overload (deinfix >) [gt_atom_range; gt_range_atom] +overload (deinfix >=) [gteq_atom_range; gteq_range_atom] + +function ([|63|]) branch (([|63|]) x) = +{ + if (x <= 32) + then x + 31 + else x - 33 +} diff --git a/test/typecheck/pass/fun_simple_constraints1.sail b/test/typecheck/pass/fun_simple_constraints1.sail new file mode 100644 index 00000000..7fd502b0 --- /dev/null +++ b/test/typecheck/pass/fun_simple_constraints1.sail @@ -0,0 +1,18 @@ + +val forall Nat 'n, Nat 'm. ([:'n + 20:], [:'m:]) -> [:'n + 20 + 'm:] effect pure plus + +val forall Nat 'n, 'n <= -10. [:'n:] -> [:'n:] effect pure minus_ten_id + +val forall Nat 'n, 'n >= 10. [:'n:] -> [:'n:] effect pure ten_id + +val forall Nat 'N, 'N >= 63. [|10:'N|] -> [|10:'N|] effect pure branch + +function forall Nat 'N, 'N >= 63. [|10:'N|] branch x = +{ + x +} +and branch (([|10:30|]) y) = y +and branch (([:31:]) _) = sizeof 'N +and branch (([|31:40|]) _) = plus(60,3) +and branch (([|41:50|]) _) = plus(sizeof 'N, minus_ten_id(-53)) +and branch (([|51:63|]) _) = ten_id(sizeof 'N)
\ No newline at end of file diff --git a/test/typecheck/pass/fun_simple_constraints2.sail b/test/typecheck/pass/fun_simple_constraints2.sail new file mode 100644 index 00000000..338ef8e8 --- /dev/null +++ b/test/typecheck/pass/fun_simple_constraints2.sail @@ -0,0 +1,18 @@ + +val forall Nat 'n, Nat 'm. ([:'n + 20:], [:'m:]) -> [:'n + 20 + 'm:] effect pure plus + +val forall Nat 'n, 'n <= -10. [|'n:'n|] -> [:'n:] effect pure minus_ten_id + +val forall Nat 'n, 'n >= 10. [:'n:] -> [:'n:] effect pure ten_id + +val forall Nat 'N, 'N >= 63. [|10:'N|] -> [|10:'N|] effect pure branch + +function forall Nat 'N, 'N >= 63. [|10:'N|] branch x = +{ + x +} +and branch (([|10:30|]) y) = y +and branch (([:31:]) _) = sizeof 'N +and branch (([|31:40|]) _) = plus(60,3) +and branch (([|41:50|]) _) = plus(sizeof 'N, minus_ten_id(-53)) +and branch (([|51:63|]) _) = ten_id(sizeof 'N) diff --git a/test/typecheck/pass/guards.sail b/test/typecheck/pass/guards.sail new file mode 100644 index 00000000..2811c428 --- /dev/null +++ b/test/typecheck/pass/guards.sail @@ -0,0 +1,22 @@ + +val (int, int) -> int effect pure add_int +overload (deinfix +) [add_int] + +val forall Type 'a. ('a, 'a) -> bool effect pure eq +val forall Type 'a. ('a, 'a) -> bool effect pure neq + +overload (deinfix ==) [eq] +overload (deinfix !=) [neq] + +val (int, int) -> int effect pure quotient + +overload (deinfix quot) [quotient] + +typedef T = const union { int C1; int C2 } + +function int test ((int) x, (T) y) = + switch y { + case (C1(z)) when z == 0 -> 0 + case (C1(z)) when z != 0 -> x quot z + case (C2(z)) -> z + } diff --git a/test/typecheck/pass/lexp_memory.sail b/test/typecheck/pass/lexp_memory.sail new file mode 100644 index 00000000..83313ac7 --- /dev/null +++ b/test/typecheck/pass/lexp_memory.sail @@ -0,0 +1,65 @@ +default Order dec + +register (bit[64]) GPR00 (* should never be read or written *) +register (bit[64]) GPR01 +register (bit[64]) GPR02 +register (bit[64]) GPR03 +register (bit[64]) GPR04 +register (bit[64]) GPR05 +register (bit[64]) GPR06 +register (bit[64]) GPR07 +register (bit[64]) GPR08 +register (bit[64]) GPR09 +register (bit[64]) GPR10 +register (bit[64]) GPR11 +register (bit[64]) GPR12 +register (bit[64]) GPR13 +register (bit[64]) GPR14 +register (bit[64]) GPR15 +register (bit[64]) GPR16 +register (bit[64]) GPR17 +register (bit[64]) GPR18 +register (bit[64]) GPR19 +register (bit[64]) GPR20 +register (bit[64]) GPR21 +register (bit[64]) GPR22 +register (bit[64]) GPR23 +register (bit[64]) GPR24 +register (bit[64]) GPR25 +register (bit[64]) GPR26 +register (bit[64]) GPR27 +register (bit[64]) GPR28 +register (bit[64]) GPR29 +register (bit[64]) GPR30 +register (bit[64]) GPR31 + +let (vector <0, 32, inc, (register<(bit[64])>) >) GPR = + [ GPR00, GPR01, GPR02, GPR03, GPR04, GPR05, GPR06, GPR07, GPR08, GPR09, GPR10, + GPR11, GPR12, GPR13, GPR14, GPR15, GPR16, GPR17, GPR18, GPR19, GPR20, + GPR21, GPR22, GPR23, GPR24, GPR25, GPR26, GPR27, GPR28, GPR29, GPR30, GPR31 + ] + +val forall Nat 'n, Nat 'l, Type 'a, 'l >= 0. (vector<'n,'l,dec,'a>, [|'n - 'l + 1:'n|]) -> 'a effect pure vector_access_dec +val forall Nat 'n, Nat 'l, Type 'a, 'l >= 0. (vector<'n,'l,inc,'a>, [|'n:'n + 'l - 1|]) -> 'a effect pure vector_access_inc + +overload vector_access [vector_access_inc; vector_access_dec] + +val forall Num 'n, Num 'm, Order 'ord. (vector<'n,'m,'ord,bit>, vector<'n,'m,'ord,bit>) -> bool effect pure eq_vec + +overload (deinfix ==) [eq_vec] + +val cast forall Nat 'n, Nat 'l, Order 'ord. [|0:1|] -> vector<'n,'l,'ord,bit> effect pure cast_01_vec +val cast forall Nat 'n, Nat 'm, Order 'ord. vector<'n,'m,'ord,bit> -> [|0:2**'m - 1|] effect pure unsigned +val cast forall Type 'a. register<'a> -> 'a effect {rreg} reg_deref + +val (bit[5], bit[64]) -> unit effect {wreg} wGPR + +function unit wGPR (idx, v) = +{ + if idx == 0 then () else GPR[idx] := v +} + +function unit test () = +{ + wGPR(0b00001) := 0 +} diff --git a/test/typecheck/pass/mips400.sail b/test/typecheck/pass/mips400.sail new file mode 100644 index 00000000..1e8691d9 --- /dev/null +++ b/test/typecheck/pass/mips400.sail @@ -0,0 +1,631 @@ +(* New typechecker prelude *) + +val cast forall Nat 'n, Nat 'm, Order 'ord. vector<'n,'m,'ord,bit> -> [|0:2**'m - 1|] effect pure unsigned + +(* Vector access can't actually be properly polymorphic on vector + direction because of the ranges being different for each type, so + we overload it instead *) +val forall Nat 'n, Nat 'l, Type 'a, 'l >= 0. (vector<'n,'l,dec,'a>, [|'n - 'l + 1:'n|]) -> 'a effect pure vector_access_dec +val forall Nat 'n, Nat 'l, Type 'a, 'l >= 0. (vector<'n,'l,inc,'a>, [|'n:'n + 'l - 1|]) -> 'a effect pure vector_access_inc + +(* Type safe vector subrange *) +val forall Nat 'n, Nat 'l, Nat 'm, Nat 'o, Type 'a, 'l >= 0, 'm <= 'o, 'o <= 'l. + (vector<'n,'l,inc,'a>, [:'m:], [:'o:]) -> vector<'m,'o - 'm,inc,'a> effect pure vector_subrange_inc + +val forall Nat 'n, Nat 'l, Nat 'm, Nat 'o, Type 'a, 'n >= 'm, 'm >= 'o, 'o >= 'n - 'l + 1. + (vector<'n,'l,dec,'a>, [:'m:], [:'o:]) -> vector<'m,'m - ('o - 1),dec,'a> effect pure vector_subrange_dec + +overload vector_subrange [vector_subrange_inc; vector_subrange_dec] + +(* Type safe vector append *) +val forall Nat 'n1, Nat 'l1, Nat 'n2, Nat 'l2, Order 'o, Type 'a, 'l1 >= 0, 'l2 >= 0. + (vector<'n1,'l1,'o,'a>, vector<'n2,'l2,'o,'a>) -> vector<'n1,'l1 + 'l2,'o,'a> effect pure vector_append + +(* Implicit register dereferencing *) +val cast forall Type 'a. register<'a> -> 'a effect {rreg} reg_deref + +overload vector_access [vector_access_inc; vector_access_dec] + +(* Bitvector duplication *) +val forall Nat 'n. (bit, [:'n:]) -> vector<'n - 1,'n,dec,bit> effect pure duplicate + +val forall Nat 'n, Nat 'm, Nat 'o, Order 'ord. + (vector<'o,'n,'ord,bit>, [:'m:]) -> vector<'o,'m*'n,'ord,bit> effect pure duplicate_bits + +overload (deinfix ^^) [duplicate; duplicate_bits] + +(* Bitvector extension *) +val forall Nat 'n, Nat 'm, Nat 'o, Nat 'p, Order 'ord. + vector<'o, 'n, 'ord, bit> -> vector<'p, 'm, 'ord, bit> effect pure extz + +val forall Nat 'n, Nat 'm, Nat 'o, Nat 'p, Order 'ord. + vector<'o, 'n, 'ord, bit> -> vector<'p, 'm, 'ord, bit> effect pure exts + +overload EXTZ [extz] +overload EXTS [exts] + +val forall Type 'a, Nat 'n, Nat 'm, Nat 'o, Nat 'p, Order 'ord, 'm >= 'o. + vector<'n, 'm, 'ord, 'a> -> vector<'p, 'o, 'ord, 'a> effect pure mask + +(* Adjust the start index of a decreasing bitvector *) +val cast forall Nat 'n, Nat 'm, Nat 'o, 'n >= 'm - 1, 'o >= 'm - 1. + vector<'n,'m,dec,bit> -> vector<'o,'m,dec,bit> + effect pure adjust_dec + +(* Various casts from 0 and 1 to bitvectors *) +val cast forall Nat 'n, Nat 'l, Order 'ord. [:0:] -> vector<'n,'l,'ord,bit> effect pure cast_0_vec +val cast forall Nat 'n, Nat 'l, Order 'ord. [:1:] -> vector<'n,'l,'ord,bit> effect pure cast_1_vec +val cast forall Nat 'n, Nat 'l, Order 'ord. [|0:1|] -> vector<'n,'l,'ord,bit> effect pure cast_01_vec + +val cast forall Nat 'n, Order 'ord. vector<'n,1,'ord,bit> -> bool effect pure cast_vec_bool +val cast bit -> bool effect pure cast_bit_bool + +(* MSB *) +val forall Nat 'n, Nat 'm, Order 'ord. vector<'n, 'm, 'ord, bit> -> bit effect pure most_significant + +(* Arithmetic *) + +val forall Nat 'n, Nat 'm. + (atom<'n>, atom<'m>) -> atom<'n+'m> effect pure add + +val forall Nat 'n, Nat 'o, Nat 'p, Order 'ord. + (vector<'o, 'n, 'ord, bit>, vector<'p, 'n, 'ord, bit>) -> vector<'o, 'n, 'ord, bit> effect pure add_vec + +val forall Nat 'n, Nat 'o, Nat 'p, Nat 'q, Order 'ord. + (vector<'o, 'n, 'ord, bit>, vector<'p, 'n, 'ord, bit>) -> range<'q, 2**'n> effect pure add_vec_vec_range + +(* FIXME: the parser is broken for 2**... it's just been hacked to work for this common case *) +val forall Nat 'n, Nat 'm, Nat 'o, Order 'ord, 'o <= 2** 'm - 1. + (vector<'n, 'm, 'ord, bit>, atom<'o>) -> vector<'n, 'm, 'ord, bit> effect pure add_vec_range + +val forall Nat 'n, Nat 'o, Nat 'p, Order 'ord. + (vector<'o, 'n, 'ord, bit>, vector<'p, 'n, 'ord, bit>) -> (vector<'o, 'n, 'ord, bit>, bit, bit) effect pure add_overflow_vec + +(* but it doesn't parse this +val forall Nat 'n, Nat 'm, Nat 'o, Order 'ord, 'o <= 2** 'm - 1. + (vector<'n, 'm, 'ord, bit>, atom<'o>) -> range<'o, 'o+2** 'm> effect pure add_vec_range_range + *) + +val forall Nat 'n, Nat 'm, Nat 'o, Order 'ord, 'o <= 2** 'm - 1. + (atom<'o>, vector<'n, 'm, 'ord, bit>) -> vector<'n, 'm, 'ord, bit> effect pure add_range_vec + +(* or this +val forall Nat 'n, Nat 'm, Nat 'o, Order 'ord, 'o <= 2** 'm - 1. + (atom<'o>, vector<'n, 'm, 'ord, bit>) -> range<'o, 'o+2**'m-1> effect pure add_range_vec_range +*) + +val forall Nat 'o, Nat 'p, Order 'ord. + (vector<'o, 'p, 'ord, bit>, bit) -> vector<'o, 'p, 'ord, bit> effect pure add_vec_bit + +val forall Nat 'o, Nat 'p, Order 'ord. + (bit, vector<'o, 'p, 'ord, bit>) -> vector<'o, 'p, 'ord, bit> effect pure add_bit_vec + +val forall Nat 'n, Nat 'm. ([:'n:], [:'m:]) -> [:'n - 'm:] effect pure sub_exact +val forall Nat 'n, Nat 'm, Nat 'o, 'o <= 'm - 'n. ([|'n:'m|], [:'o:]) -> [|'n:'m - 'o|] effect pure sub_range +val forall Nat 'n, Nat 'm, Order 'ord. (vector<'n,'m,'ord,bit>, int) -> vector<'n,'m,'ord,bit> effect pure sub_bv + +overload (deinfix +) [ + add; + add_vec; + add_vec_vec_range; + add_vec_range; + add_overflow_vec; + add_vec_range_range; + add_range_vec; + add_range_vec_range; + add_vec_bit; + add_bit_vec; +] + +overload (deinfix -) [ + sub_exact; + sub_bv; + sub_range; +] + +(* Equality *) + +(* Sail gives a bunch of overloads for equality, but apparantly also +gives an equality and inequality for any type 'a, so why bother +overloading? *) + +val forall Type 'a. ('a, 'a) -> bool effect pure eq +val forall Type 'a. ('a, 'a) -> bool effect pure neq + +overload (deinfix ==) [eq] +overload (deinfix !=) [neq] + +(* Boolean operators *) +val bool -> bool effect pure bool_not +val (bool, bool) -> bool effect pure bool_or +val (bool, bool) -> bool effect pure bool_and + +overload ~ [bool_not] +overload (deinfix &) [bool_and] +overload (deinfix |) [bool_or] + +(* Mips spec starts here *) + +(*========================================================================*) +(* *) +(* Copyright (c) 2015-2017 Robert M. Norton *) +(* Copyright (c) 2015-2017 Kathyrn Gray *) +(* All rights reserved. *) +(* *) +(* This software was developed by the University of Cambridge Computer *) +(* Laboratory as part of the Rigorous Engineering of Mainstream Systems *) +(* (REMS) project, funded by EPSRC grant EP/K008528/1. *) +(* *) +(* Redistribution and use in source and binary forms, with or without *) +(* modification, are permitted provided that the following conditions *) +(* are met: *) +(* 1. Redistributions of source code must retain the above copyright *) +(* notice, this list of conditions and the following disclaimer. *) +(* 2. Redistributions in binary form must reproduce the above copyright *) +(* notice, this list of conditions and the following disclaimer in *) +(* the documentation and/or other materials provided with the *) +(* distribution. *) +(* *) +(* THIS SOFTWARE IS PROVIDED BY THE AUTHOR AND CONTRIBUTORS ``AS IS'' *) +(* AND ANY EXPRESS OR IMPLIED WARRANTIES, INCLUDING, BUT NOT LIMITED *) +(* TO, THE IMPLIED WARRANTIES OF MERCHANTABILITY AND FITNESS FOR A *) +(* PARTICULAR PURPOSE ARE DISCLAIMED. IN NO EVENT SHALL THE AUTHOR OR *) +(* CONTRIBUTORS BE LIABLE FOR ANY DIRECT, INDIRECT, INCIDENTAL, *) +(* SPECIAL, EXEMPLARY, OR CONSEQUENTIAL DAMAGES (INCLUDING, BUT NOT *) +(* LIMITED TO, PROCUREMENT OF SUBSTITUTE GOODS OR SERVICES; LOSS OF *) +(* USE, DATA, OR PROFITS; OR BUSINESS INTERRUPTION) HOWEVER CAUSED AND *) +(* ON ANY THEORY OF LIABILITY, WHETHER IN CONTRACT, STRICT LIABILITY, *) +(* OR TORT (INCLUDING NEGLIGENCE OR OTHERWISE) ARISING IN ANY WAY OUT *) +(* OF THE USE OF THIS SOFTWARE, EVEN IF ADVISED OF THE POSSIBILITY OF *) +(* SUCH DAMAGE. *) +(*========================================================================*) + +(* mips_prelude.sail: declarations of mips registers, and functions common + to mips instructions (e.g. address translation) *) + +(* bit vectors have indices decreasing from left i.e. msb is highest index *) +default Order dec + +register (bit[64]) PC +register (bit[64]) nextPC + +(* CP0 Registers *) + +typedef CauseReg = register bits [ 31 : 0 ] { + 31 : BD; (* branch delay *) + (*30 : Z0;*) + 29 .. 28 : CE; (* for coprocessor enable exception *) + (*27 .. 24 : Z1;*) + 23 : IV; (* special interrupt vector not supported *) + 22 : WP; (* watchpoint exception occurred *) + (*21 .. 16 : Z2; *) + 15 .. 8 : IP; (* interrupt pending bits *) + (*7 : Z3;*) + 6 .. 2 : ExcCode; (* code of last exception *) + (*1 .. 0 : Z4;*) +} + +typedef TLBEntryLoReg = register bits [63 : 0] { + 63 : CapS; + 62 : CapL; + 29 .. 6 : PFN; + 5 .. 3 : C; + 2 : D; + 1 : V; + 0 : G; +} + +typedef TLBEntryHiReg = register bits [63 : 0] { + 63 .. 62 : R; + 39 .. 13 : VPN2; + 7 .. 0 : ASID; +} + +typedef ContextReg = register bits [63 : 0] { + 63 .. 23 : PTEBase; + 22 .. 4 : BadVPN2; + (*3 .. 0 : ZR;*) +} + +typedef XContextReg = register bits [63 : 0] { + 63 .. 33: PTEBase; + 32 .. 31: R; + 30 .. 4: BadVPN2; +} + +let ([:64:]) TLBNumEntries = 64 +typedef TLBIndexT = (bit[6]) +let (TLBIndexT) TLBIndexMax = 0b111111 + +let MAX_U64 = unsigned(0xffffffffffffffff) +let MAX_VA = unsigned(0xffffffffff) +let MAX_PA = unsigned(0xfffffffff) + +typedef TLBEntry = register bits [116 : 0] { + 116 .. 101: pagemask; + 100 .. 99 : r ; + 98 .. 72 : vpn2 ; + 71 .. 64 : asid ; + 63 : g ; + 62 : valid ; + 61 : caps1 ; + 60 : capl1 ; + 59 .. 36 : pfn1 ; + 35 .. 33 : c1 ; + 32 : d1 ; + 31 : v1 ; + 30 : caps0 ; + 29 : capl0 ; + 28 .. 5 : pfn0 ; + 4 .. 2 : c0 ; + 1 : d0 ; + 0 : v0 ; +} + +register (bit[1]) TLBProbe +register (TLBIndexT) TLBIndex +register (TLBIndexT) TLBRandom +register (TLBEntryLoReg) TLBEntryLo0 +register (TLBEntryLoReg) TLBEntryLo1 +register (ContextReg) TLBContext +register (bit[16]) TLBPageMask +register (TLBIndexT) TLBWired +register (TLBEntryHiReg) TLBEntryHi +register (XContextReg) TLBXContext + +register (TLBEntry) TLBEntry00 +register (TLBEntry) TLBEntry01 +register (TLBEntry) TLBEntry02 +register (TLBEntry) TLBEntry03 +register (TLBEntry) TLBEntry04 +register (TLBEntry) TLBEntry05 +register (TLBEntry) TLBEntry06 +register (TLBEntry) TLBEntry07 +register (TLBEntry) TLBEntry08 +register (TLBEntry) TLBEntry09 +register (TLBEntry) TLBEntry10 +register (TLBEntry) TLBEntry11 +register (TLBEntry) TLBEntry12 +register (TLBEntry) TLBEntry13 +register (TLBEntry) TLBEntry14 +register (TLBEntry) TLBEntry15 +register (TLBEntry) TLBEntry16 +register (TLBEntry) TLBEntry17 +register (TLBEntry) TLBEntry18 +register (TLBEntry) TLBEntry19 +register (TLBEntry) TLBEntry20 +register (TLBEntry) TLBEntry21 +register (TLBEntry) TLBEntry22 +register (TLBEntry) TLBEntry23 +register (TLBEntry) TLBEntry24 +register (TLBEntry) TLBEntry25 +register (TLBEntry) TLBEntry26 +register (TLBEntry) TLBEntry27 +register (TLBEntry) TLBEntry28 +register (TLBEntry) TLBEntry29 +register (TLBEntry) TLBEntry30 +register (TLBEntry) TLBEntry31 +register (TLBEntry) TLBEntry32 +register (TLBEntry) TLBEntry33 +register (TLBEntry) TLBEntry34 +register (TLBEntry) TLBEntry35 +register (TLBEntry) TLBEntry36 +register (TLBEntry) TLBEntry37 +register (TLBEntry) TLBEntry38 +register (TLBEntry) TLBEntry39 +register (TLBEntry) TLBEntry40 +register (TLBEntry) TLBEntry41 +register (TLBEntry) TLBEntry42 +register (TLBEntry) TLBEntry43 +register (TLBEntry) TLBEntry44 +register (TLBEntry) TLBEntry45 +register (TLBEntry) TLBEntry46 +register (TLBEntry) TLBEntry47 +register (TLBEntry) TLBEntry48 +register (TLBEntry) TLBEntry49 +register (TLBEntry) TLBEntry50 +register (TLBEntry) TLBEntry51 +register (TLBEntry) TLBEntry52 +register (TLBEntry) TLBEntry53 +register (TLBEntry) TLBEntry54 +register (TLBEntry) TLBEntry55 +register (TLBEntry) TLBEntry56 +register (TLBEntry) TLBEntry57 +register (TLBEntry) TLBEntry58 +register (TLBEntry) TLBEntry59 +register (TLBEntry) TLBEntry60 +register (TLBEntry) TLBEntry61 +register (TLBEntry) TLBEntry62 +register (TLBEntry) TLBEntry63 + +let (vector <0, 64, inc, (TLBEntry)>) TLBEntries = [ +TLBEntry00, +TLBEntry01, +TLBEntry02, +TLBEntry03, +TLBEntry04, +TLBEntry05, +TLBEntry06, +TLBEntry07, +TLBEntry08, +TLBEntry09, +TLBEntry10, +TLBEntry11, +TLBEntry12, +TLBEntry13, +TLBEntry14, +TLBEntry15, +TLBEntry16, +TLBEntry17, +TLBEntry18, +TLBEntry19, +TLBEntry20, +TLBEntry21, +TLBEntry22, +TLBEntry23, +TLBEntry24, +TLBEntry25, +TLBEntry26, +TLBEntry27, +TLBEntry28, +TLBEntry29, +TLBEntry30, +TLBEntry31, +TLBEntry32, +TLBEntry33, +TLBEntry34, +TLBEntry35, +TLBEntry36, +TLBEntry37, +TLBEntry38, +TLBEntry39, +TLBEntry40, +TLBEntry41, +TLBEntry42, +TLBEntry43, +TLBEntry44, +TLBEntry45, +TLBEntry46, +TLBEntry47, +TLBEntry48, +TLBEntry49, +TLBEntry50, +TLBEntry51, +TLBEntry52, +TLBEntry53, +TLBEntry54, +TLBEntry55, +TLBEntry56, +TLBEntry57, +TLBEntry58, +TLBEntry59, +TLBEntry60, +TLBEntry61, +TLBEntry62, +TLBEntry63 +] + +register (bit[32]) CP0Compare +register (CauseReg) CP0Cause +register (bit[64]) CP0EPC +register (bit[64]) CP0ErrorEPC +register (bit[1]) CP0LLBit +register (bit[64]) CP0LLAddr +register (bit[64]) CP0BadVAddr +register (bit[32]) CP0Count +register (bit[32]) CP0HWREna +register (bit[64]) CP0UserLocal + +typedef StatusReg = register bits [31:0] { + 31 .. 28 : CU; (* co-processor enable bits *) + (* RP/FR/RE/MX/PX not implemented *) + 22 : BEV; (* use boot exception vectors (initialised to one) *) + (* TS/SR/NMI not implemented *) + 15 .. 8 : IM; (* Interrupt mask *) + 7 : KX; (* kernel 64-bit enable *) + 6 : SX; (* supervisor 64-bit enable *) + 5 : UX; (* user 64-bit enable *) + 4 .. 3 : KSU; (* Processor mode *) + 2 : ERL; (* error level (should be initialised to one, but BERI is different) *) + 1 : EXL; (* exception level *) + 0 : IE; (* interrupt enable *) +} +register (StatusReg) CP0Status + +(* Implementation registers -- not ISA defined *) +register (bit[1]) branchPending (* Set by branch instructions to implement branch delay *) +register (bit[1]) inBranchDelay (* Needs to be set by outside world when in branch delay slot *) +register (bit[64]) delayedPC (* Set by branch instructions to implement branch delay *) + +(* General purpose registers *) + +register (bit[64]) GPR00 (* should never be read or written *) +register (bit[64]) GPR01 +register (bit[64]) GPR02 +register (bit[64]) GPR03 +register (bit[64]) GPR04 +register (bit[64]) GPR05 +register (bit[64]) GPR06 +register (bit[64]) GPR07 +register (bit[64]) GPR08 +register (bit[64]) GPR09 +register (bit[64]) GPR10 +register (bit[64]) GPR11 +register (bit[64]) GPR12 +register (bit[64]) GPR13 +register (bit[64]) GPR14 +register (bit[64]) GPR15 +register (bit[64]) GPR16 +register (bit[64]) GPR17 +register (bit[64]) GPR18 +register (bit[64]) GPR19 +register (bit[64]) GPR20 +register (bit[64]) GPR21 +register (bit[64]) GPR22 +register (bit[64]) GPR23 +register (bit[64]) GPR24 +register (bit[64]) GPR25 +register (bit[64]) GPR26 +register (bit[64]) GPR27 +register (bit[64]) GPR28 +register (bit[64]) GPR29 +register (bit[64]) GPR30 +register (bit[64]) GPR31 + +(* Special registers For MUL/DIV *) +register (bit[64]) HI +register (bit[64]) LO + +let (vector <0, 32, inc, (register<(bit[64])>) >) GPR = + [ GPR00, GPR01, GPR02, GPR03, GPR04, GPR05, GPR06, GPR07, GPR08, GPR09, GPR10, + GPR11, GPR12, GPR13, GPR14, GPR15, GPR16, GPR17, GPR18, GPR19, GPR20, + GPR21, GPR22, GPR23, GPR24, GPR25, GPR26, GPR27, GPR28, GPR29, GPR30, GPR31 + ] + +(* JTAG Uart registers *) + +register (bit[8]) UART_WDATA +register (bit[1]) UART_WRITTEN +register (bit[8]) UART_RDATA +register (bit[1]) UART_RVALID + +(* Check whether a given 64-bit vector is a properly sign extended 32-bit word *) +val bit[64] -> bool effect pure NotWordVal +function bool NotWordVal (word) = + (word[31] ^^ 32) != word[63..32] + +(* Read numbered GP reg. (r0 is always zero) *) +val bit[5] -> bit[64] effect {rreg} rGPR +function bit[64] rGPR idx = { + if idx == 0 then 0 else GPR[idx] +} + +(* Write numbered GP reg. (writes to r0 ignored) *) +val (bit[5], bit[64]) -> unit effect {wreg} wGPR +function unit wGPR (idx, v) = { + if idx == 0 then () else GPR[idx] := v +} + +val extern forall Nat 'n. ( bit[64] , [|'n|] ) -> (bit[8 * 'n]) effect { rmem } MEMr +val extern forall Nat 'n. ( bit[64] , [|'n|] ) -> (bit[8 * 'n]) effect { rmem } MEMr_reserve +val extern unit -> unit effect { barr } MEM_sync + +val extern forall Nat 'n. ( bit[64] , [|'n|]) -> unit effect { eamem } MEMea +val extern forall Nat 'n. ( bit[64] , [|'n|]) -> unit effect { eamem } MEMea_conditional +val extern forall Nat 'n. ( bit[64] , [|'n|] , bit[8*'n]) -> unit effect { wmv } MEMval +val extern forall Nat 'n. ( bit[64] , [|'n|] , bit[8*'n]) -> bool effect { wmv } MEMval_conditional + +typedef Exception = enumerate +{ + Int; TLBMod; TLBL; TLBS; AdEL; AdES; Sys; Bp; ResI; CpU; Ov; Tr; C2E; C2Trap; + XTLBRefillL; XTLBRefillS; XTLBInvL; XTLBInvS; MCheck +} + +(* Return the ISA defined code for an exception condition *) +function (bit[5]) ExceptionCode ((Exception) ex) = + switch (ex) + { + case Int -> mask(0x00) (* Interrupt *) + case TLBMod -> mask(0x01) (* TLB modification exception *) + case TLBL -> mask(0x02) (* TLB exception (load or fetch) *) + case TLBS -> mask(0x03) (* TLB exception (store) *) + case AdEL -> mask(0x04) (* Address error (load or fetch) *) + case AdES -> mask(0x05) (* Address error (store) *) + case Sys -> mask(0x08) (* Syscall *) + case Bp -> mask(0x09) (* Breakpoint *) + case ResI -> mask(0x0a) (* Reserved instruction *) + case CpU -> mask(0x0b) (* Coprocessor Unusable *) + case Ov -> mask(0x0c) (* Arithmetic overflow *) + case Tr -> mask(0x0d) (* Trap *) + case C2E -> mask(0x12) (* C2E coprocessor 2 exception *) + case C2Trap -> mask(0x12) (* C2Trap maps to same exception code, different vector *) + case XTLBRefillL -> mask(0x02) + case XTLBRefillS -> mask(0x03) + case XTLBInvL -> mask(0x02) + case XTLBInvS -> mask(0x03) + case MCheck -> mask(0x18) + } + + + +function forall Type 'o. 'o SignalExceptionMIPS ((Exception) ex, (bit[64]) kccBase) = + { + (* Only update EPC and BD if not already in EXL mode *) + if (~ (CP0Status.EXL)) then + { + if (inBranchDelay[0]) then + { + CP0EPC := PC - 4; + CP0Cause.BD := 1; + } + else + { + CP0EPC := PC; + CP0Cause.BD := 0; + } + }; + + (* choose an exception vector to branch to. Some are not supported + e.g. Reset *) + vectorOffset := + if (CP0Status.EXL) then + 0x180 (* Always use common vector if in exception mode already *) + else if ((ex == XTLBRefillL) | (ex == XTLBRefillS)) then + 0x080 + else if (ex == C2Trap) then + 0x280 (* Special vector for CHERI traps *) + else + 0x180; (* Common vector *) + (bit[64]) vectorBase := if CP0Status.BEV then + 0xFFFFFFFFBFC00200 + else + 0xFFFFFFFF80000000; + (* On CHERI we have to subtract KCC.base so that we end up at the + right absolute vector address after indirecting via new PCC *) + nextPC := ((bit[64])(vectorBase + (bit[64])(EXTS(vectorOffset)))) - kccBase; + CP0Cause.ExcCode := ExceptionCode(ex); + CP0Status.EXL := 1; + exit (); + } + +val forall Type 'o . Exception -> 'o effect {escape, rreg, wreg} SignalException + +function forall Type 'o. 'o SignalExceptionBadAddr((Exception) ex, (bit[64]) badAddr) = + { + CP0BadVAddr := badAddr; + SignalException(ex); + } + +function forall Type 'o. 'o SignalExceptionTLB((Exception) ex, (bit[64]) badAddr) = { + CP0BadVAddr := badAddr; + (TLBContext.BadVPN2) := (badAddr[31..13]); + (TLBXContext.BadVPN2):= (badAddr[39..13]); + (TLBXContext.R) := (badAddr[63..62]); + (TLBEntryHi.R) := (badAddr[63..62]); + (TLBEntryHi.VPN2) := (badAddr[39..13]); + SignalException(ex); +} + +typedef MemAccessType = enumerate {Instruction; LoadData; StoreData} +typedef AccessLevel = enumerate {User; Supervisor; Kernel} + +function AccessLevel getAccessLevel() = + if ((CP0Status.EXL) | (CP0Status.ERL)) then + Kernel + else switch (bit[2]) (CP0Status.KSU) + { + case 0b00 -> Kernel + case 0b01 -> Supervisor + case 0b10 -> User + case _ -> User (* behaviour undefined, assume user *) + } + +function unit checkCP0Access () = + { + let accessLevel = getAccessLevel() in + if ((accessLevel != Kernel) & (~(CP0Status[28] (*CU0*)))) then + { + (CP0Cause.CE) := 0b00; + SignalException(CpU); + } + } diff --git a/test/typecheck/pass/mips_CP0Cause_BD_assign1.sail b/test/typecheck/pass/mips_CP0Cause_BD_assign1.sail new file mode 100644 index 00000000..4dc63e71 --- /dev/null +++ b/test/typecheck/pass/mips_CP0Cause_BD_assign1.sail @@ -0,0 +1,27 @@ +val cast forall Nat 'n, Order 'ord. [:1:] -> vector<'n,1,'ord,bit> effect pure cast_one_bv +val cast forall Nat 'n, Order 'ord. [:0:] -> vector<'n,1,'ord,bit> effect pure cast_zero_bv + +default Order dec + +typedef CauseReg = register bits [ 31 : 0 ] { + 31 : BD; (* branch delay *) + (*30 : Z0;*) + 29 .. 28 : CE; (* for coprocessor enable exception *) + (*27 .. 24 : Z1;*) + 23 : IV; (* special interrupt vector not supported *) + 22 : WP; (* watchpoint exception occurred *) + (*21 .. 16 : Z2; *) + 15 .. 8 : IP; (* interrupt pending bits *) + (*7 : Z3;*) + 6 .. 2 : ExcCode; (* code of last exception *) + (*1 .. 0 : Z4;*) +} + +register (CauseReg) CP0Cause + +val unit -> unit effect {wreg} test + +function unit test () = +{ + CP0Cause.BD := 1 +} diff --git a/test/typecheck/pass/mips_CP0Cause_BD_assign2.sail b/test/typecheck/pass/mips_CP0Cause_BD_assign2.sail new file mode 100644 index 00000000..b35a0767 --- /dev/null +++ b/test/typecheck/pass/mips_CP0Cause_BD_assign2.sail @@ -0,0 +1,27 @@ +val cast forall Nat 'n, Order 'ord. [:1:] -> vector<'n,1,'ord,bit> effect pure cast_one_bv +val cast forall Nat 'n, Order 'ord. [:0:] -> vector<'n,1,'ord,bit> effect pure cast_zero_bv + +default Order dec + +typedef CauseReg = register bits [ 31 : 0 ] { + 31 : BD; (* branch delay *) + (*30 : Z0;*) + 29 .. 28 : CE; (* for coprocessor enable exception *) + (*27 .. 24 : Z1;*) + 23 : IV; (* special interrupt vector not supported *) + 22 : WP; (* watchpoint exception occurred *) + (*21 .. 16 : Z2; *) + 15 .. 8 : IP; (* interrupt pending bits *) + (*7 : Z3;*) + 6 .. 2 : ExcCode; (* code of last exception *) + (*1 .. 0 : Z4;*) +} + +register (CauseReg) CP0Cause + +val unit -> unit effect {wreg} test + +function unit test () = +{ + CP0Cause.BD := 0 +} diff --git a/test/typecheck/pass/mips_CP0Cause_access.sail b/test/typecheck/pass/mips_CP0Cause_access.sail new file mode 100644 index 00000000..c0e318c4 --- /dev/null +++ b/test/typecheck/pass/mips_CP0Cause_access.sail @@ -0,0 +1,34 @@ +(* val forall Nat 'n, Nat 'm, Nat 'o, 'o >= 'm - 1. + vector<'n,'m,dec,bit> -> vector<'o,'m,dec,bit> + effect pure ADJUST +*) + +val forall Num 'n, Num 'l, Type 'a, 'l >= 0. (vector<'n,'l,dec,'a>, [|'n - 'l + 1:'n|]) -> 'a effect pure vector_access_dec +val forall Nat 'n, Nat 'l, Type 'a, 'l >= 0. (vector<'n,'l,inc,'a>, [|'n:'n + 'l - 1|]) -> 'a effect pure vector_access_inc + +overload vector_access [vector_access_inc; vector_access_dec] + +default Order dec + +typedef CauseReg = register bits [ 31 : 0 ] { + 31 : BD; (* branch delay *) + (*30 : Z0;*) + 29 .. 28 : CE; (* for coprocessor enable exception *) + (*27 .. 24 : Z1;*) + 23 : IV; (* special interrupt vector not supported *) + 22 : WP; (* watchpoint exception occurred *) + (*21 .. 16 : Z2; *) + 15 .. 8 : IP; (* interrupt pending bits *) + (*7 : Z3;*) + 6 .. 2 : ExcCode; (* code of last exception *) + (*1 .. 0 : Z4;*) +} + +register (CauseReg) CP0Cause + +val unit -> bit effect {rreg} test + +function bit test () = +{ + CP0Cause[30] +} diff --git a/test/typecheck/pass/mips_CauseReg1.sail b/test/typecheck/pass/mips_CauseReg1.sail new file mode 100644 index 00000000..b9503efa --- /dev/null +++ b/test/typecheck/pass/mips_CauseReg1.sail @@ -0,0 +1,15 @@ +default Order dec + +typedef CauseReg = register bits [ 31 : 0 ] { + 31 : BD; (* branch delay *) + (*30 : Z0;*) + 29 .. 28 : CE; (* for coprocessor enable exception *) + (*27 .. 24 : Z1;*) + 23 : IV; (* special interrupt vector not supported *) + 22 : WP; (* watchpoint exception occurred *) + (*21 .. 16 : Z2; *) + 15 .. 8 : IP; (* interrupt pending bits *) + (*7 : Z3;*) + 6 .. 2 : ExcCode; (* code of last exception *) + (*1 .. 0 : Z4;*) +} diff --git a/test/typecheck/pass/mips_CauseReg2.sail b/test/typecheck/pass/mips_CauseReg2.sail new file mode 100644 index 00000000..7600c9f1 --- /dev/null +++ b/test/typecheck/pass/mips_CauseReg2.sail @@ -0,0 +1,15 @@ +default Order dec + +typedef CauseReg = register bits [ 31 : 1 ] { + 31 : BD; (* branch delay *) + (*30 : Z0;*) + 29 .. 28 : CE; (* for coprocessor enable exception *) + (*27 .. 24 : Z1;*) + 23 : IV; (* special interrupt vector not supported *) + 22 : WP; (* watchpoint exception occurred *) + (*21 .. 16 : Z2; *) + 15 .. 8 : IP; (* interrupt pending bits *) + (*7 : Z3;*) + 6 .. 2 : ExcCode; (* code of last exception *) + (*1 .. 0 : Z4;*) +} diff --git a/test/typecheck/pass/mips_reg_field_bit.sail b/test/typecheck/pass/mips_reg_field_bit.sail new file mode 100644 index 00000000..33560bde --- /dev/null +++ b/test/typecheck/pass/mips_reg_field_bit.sail @@ -0,0 +1,28 @@ +val cast forall Nat 'n, Nat 'm, Nat 'o, 'o >= 'm - 1. + vector<'n,'m,dec,bit> -> vector<'o,'m,dec,bit> + effect pure ADJUST + +default Order dec + +typedef CauseReg = register bits [ 31 : 0 ] { + 31 : BD; (* branch delay *) + (*30 : Z0;*) + 29 .. 28 : CE; (* for coprocessor enable exception *) + (*27 .. 24 : Z1;*) + 23 : IV; (* special interrupt vector not supported *) + 22 : WP; (* watchpoint exception occurred *) + (*21 .. 16 : Z2; *) + 15 .. 8 : IP; (* interrupt pending bits *) + (*7 : Z3;*) + 6 .. 2 : ExcCode; (* code of last exception *) + (*1 .. 0 : Z4;*) +} + +register (CauseReg) CP0Cause + +val unit -> unit effect {wreg} test + +function unit test () = +{ + (CP0Cause.CE)[28] := bitone +} diff --git a/test/typecheck/pass/mips_reg_field_bv.sail b/test/typecheck/pass/mips_reg_field_bv.sail new file mode 100644 index 00000000..4b82d4de --- /dev/null +++ b/test/typecheck/pass/mips_reg_field_bv.sail @@ -0,0 +1,28 @@ +val cast forall Nat 'n, Nat 'm, Nat 'o, 'o >= 'm - 1. + vector<'n,'m,dec,bit> -> vector<'o,'m,dec,bit> + effect pure ADJUST + +default Order dec + +typedef CauseReg = register bits [ 31 : 0 ] { + 31 : BD; (* branch delay *) + (*30 : Z0;*) + 29 .. 28 : CE; (* for coprocessor enable exception *) + (*27 .. 24 : Z1;*) + 23 : IV; (* special interrupt vector not supported *) + 22 : WP; (* watchpoint exception occurred *) + (*21 .. 16 : Z2; *) + 15 .. 8 : IP; (* interrupt pending bits *) + (*7 : Z3;*) + 6 .. 2 : ExcCode; (* code of last exception *) + (*1 .. 0 : Z4;*) +} + +register (CauseReg) CP0Cause + +val unit -> unit effect {wreg} test + +function unit test () = +{ + CP0Cause.CE := 0b11 +} diff --git a/test/typecheck/pass/mips_regtyps.sail b/test/typecheck/pass/mips_regtyps.sail new file mode 100644 index 00000000..f7a3ce91 --- /dev/null +++ b/test/typecheck/pass/mips_regtyps.sail @@ -0,0 +1,53 @@ + +(* mips_prelude.sail: declarations of mips registers, and functions common + to mips instructions (e.g. address translation) *) + +(* bit vectors have indices decreasing from left i.e. msb is highest index *) +default Order dec + +register (bit[64]) PC +register (bit[64]) nextPC + +(* CP0 Registers *) + +typedef CauseReg = register bits [ 31 : 0 ] { + 31 : BD; (* branch delay *) + (*30 : Z0;*) + 29 .. 28 : CE; (* for coprocessor enable exception *) + (*27 .. 24 : Z1;*) + 23 : IV; (* special interrupt vector not supported *) + 22 : WP; (* watchpoint exception occurred *) + (*21 .. 16 : Z2; *) + 15 .. 8 : IP; (* interrupt pending bits *) + (*7 : Z3;*) + 6 .. 2 : ExcCode; (* code of last exception *) + (*1 .. 0 : Z4;*) +} + +typedef TLBEntryLoReg = register bits [63 : 0] { + 63 : CapS; + 62 : CapL; + 29 .. 6 : PFN; + 5 .. 3 : C; + 2 : D; + 1 : V; + 0 : G; +} + +typedef TLBEntryHiReg = register bits [63 : 0] { + 63 .. 62 : R; + 39 .. 13 : VPN2; + 7 .. 0 : ASID; +} + +typedef ContextReg = register bits [63 : 0] { + 63 .. 23 : PTEBase; + 22 .. 4 : BadVPN2; + (*3 .. 0 : ZR;*) +} + +typedef XContextReg = register bits [63 : 0] { + 63 .. 33: PTEBase; + 32 .. 31: R; + 30 .. 4: BadVPN2; +} diff --git a/test/typecheck/pass/mips_tlbindext_dec.sail b/test/typecheck/pass/mips_tlbindext_dec.sail new file mode 100644 index 00000000..af98cd85 --- /dev/null +++ b/test/typecheck/pass/mips_tlbindext_dec.sail @@ -0,0 +1,5 @@ + +default Order dec + +typedef TLBIndexT = (bit[6]) +let (TLBIndexT) TLBIndexMax = 0b111111 diff --git a/test/typecheck/pass/mips_tlbindext_inc.sail b/test/typecheck/pass/mips_tlbindext_inc.sail new file mode 100644 index 00000000..d64ffd68 --- /dev/null +++ b/test/typecheck/pass/mips_tlbindext_inc.sail @@ -0,0 +1,5 @@ + +default Order inc + +typedef TLBIndexT = (bit[6]) +let (TLBIndexT) TLBIndexMax = 0b111111 diff --git a/test/typecheck/pass/modify_assignment1.sail b/test/typecheck/pass/modify_assignment1.sail new file mode 100644 index 00000000..1c7ab614 --- /dev/null +++ b/test/typecheck/pass/modify_assignment1.sail @@ -0,0 +1,8 @@ + +val unit -> unit effect pure test + +function unit test () = +{ + ([|0:10|]) z := 9; + z := ([|0:9|]) 8 +}
\ No newline at end of file diff --git a/test/typecheck/pass/modify_type_chain.sail b/test/typecheck/pass/modify_type_chain.sail new file mode 100644 index 00000000..14651787 --- /dev/null +++ b/test/typecheck/pass/modify_type_chain.sail @@ -0,0 +1,8 @@ + +val unit -> unit effect pure test + +function unit test () = +{ + ([|0:10|]) z := 9; + ([|0:9|]) z := ([|0:8|]) 8 +}
\ No newline at end of file diff --git a/test/typecheck/pass/nat_set.sail b/test/typecheck/pass/nat_set.sail new file mode 100644 index 00000000..46338353 --- /dev/null +++ b/test/typecheck/pass/nat_set.sail @@ -0,0 +1,8 @@ + +function forall Nat 'n, 'n IN {1,2,3}. bool test (([:'n:]) x) = +{ + true +} + +let x = test(1) +let y = test(3)
\ No newline at end of file diff --git a/test/typecheck/pass/nondet.sail b/test/typecheck/pass/nondet.sail new file mode 100644 index 00000000..8a353c66 --- /dev/null +++ b/test/typecheck/pass/nondet.sail @@ -0,0 +1,12 @@ + +register int z + +val unit -> unit effect {wreg} test + +function unit test () = { + nondet { + z := 0; + z := 1; + z := 2; + } +} diff --git a/test/typecheck/pass/nondet_assert.sail b/test/typecheck/pass/nondet_assert.sail new file mode 100644 index 00000000..e90bb6f2 --- /dev/null +++ b/test/typecheck/pass/nondet_assert.sail @@ -0,0 +1,14 @@ + +register int z + +val unit -> int effect {wreg, rreg} test + +function int test () = { + nondet { + z := 0; + assert(false, "Nondeterministic assert"); + return z; + z := 1; + }; + z +} diff --git a/test/typecheck/pass/nondet_return.sail b/test/typecheck/pass/nondet_return.sail new file mode 100644 index 00000000..56fcfd5a --- /dev/null +++ b/test/typecheck/pass/nondet_return.sail @@ -0,0 +1,13 @@ + +register int z + +val unit -> int effect {wreg, rreg} test + +function int test () = { + nondet { + z := 0; + return z; + z := 1; + }; + z +} diff --git a/test/typecheck/pass/option_either.sail b/test/typecheck/pass/option_either.sail new file mode 100644 index 00000000..c466daf4 --- /dev/null +++ b/test/typecheck/pass/option_either.sail @@ -0,0 +1,33 @@ +default Order inc + +typedef option = const union forall Type 'a. { + None; + 'a Some +} + +function forall Type 'a. option<'a> none () = None + +function forall Type 'a. option<'a> some (('a) x) = Some(x) + +function forall Type 'a. int test ((option<'a>) x) = +{ + switch x { + case None -> 0 + case (Some(y)) -> 1 + } +} + +typedef either = const union forall Type 'a, Type 'b. { + 'a Left; + 'b Right +} + +val forall Nat 'n, 'n >= 0. bit['n] -> int effect pure signed + +function int test2 ((either<int,bit[1]>) x) = +{ + switch x { + case (Left(l)) -> l + case (Right(r)) -> signed(r) + } +} diff --git a/test/typecheck/pass/overload_plus.sail b/test/typecheck/pass/overload_plus.sail new file mode 100644 index 00000000..5390a5a4 --- /dev/null +++ b/test/typecheck/pass/overload_plus.sail @@ -0,0 +1,12 @@ +default Order inc + +val extern forall Nat 'n. (bit['n], bit['n]) -> bit['n] effect pure bv_add = "bv_add_inc" + +overload (deinfix +) [bv_add] + +val (bit[3], bit[3]) -> bit[3] effect pure test + +function bit[3] test (x, y) = +{ + x + y +} diff --git a/test/typecheck/pass/phantom_num.sail b/test/typecheck/pass/phantom_num.sail new file mode 100644 index 00000000..c4ff8b13 --- /dev/null +++ b/test/typecheck/pass/phantom_num.sail @@ -0,0 +1,17 @@ + +val extern (int, int) -> bool effect pure gt_int + +(* val cast forall Num 'n, Num 'm. [|'n:'m|] -> int effect pure cast_range_int *) + +overload (deinfix >) [gt_int] + +register int z + +val forall Nat 'n. unit -> unit effect {wreg} test + +function forall Nat 'n. unit test () = +{ + if sizeof 'n > 3 + then z := 0 + else z := 1 +} diff --git a/test/typecheck/pass/procstate1.sail b/test/typecheck/pass/procstate1.sail new file mode 100644 index 00000000..95ba97db --- /dev/null +++ b/test/typecheck/pass/procstate1.sail @@ -0,0 +1,16 @@ +default Order dec + +typedef ProcState = const struct forall Num 'n. +{ + bit['n] N; + bit[1] Z; + bit[1] C; + bit[1] V +} + +register ProcState<1> PSTATE + +function unit test () = +{ + PSTATE.N := 0b1 +} diff --git a/test/typecheck/pass/real.sail b/test/typecheck/pass/real.sail new file mode 100644 index 00000000..5ae1456b --- /dev/null +++ b/test/typecheck/pass/real.sail @@ -0,0 +1,2 @@ + +let (real) r = 2.2 diff --git a/test/typecheck/pass/reg_mod.sail b/test/typecheck/pass/reg_mod.sail new file mode 100644 index 00000000..37c8d890 --- /dev/null +++ b/test/typecheck/pass/reg_mod.sail @@ -0,0 +1,11 @@ + +register [|0:10|] reg + +val unit -> unit effect {wreg} test + +function unit test () = +{ + reg := 9; + reg := 10; + reg := 8 +}
\ No newline at end of file diff --git a/test/typecheck/pass/regtyp_vec.sail b/test/typecheck/pass/regtyp_vec.sail new file mode 100644 index 00000000..c939cce8 --- /dev/null +++ b/test/typecheck/pass/regtyp_vec.sail @@ -0,0 +1,36 @@ +(* val forall Nat 'n, Nat 'm, Nat 'o, 'o >= 'm - 1. + vector<'n,'m,dec,bit> -> vector<'o,'m,dec,bit> + effect pure ADJUST +*) + +val forall Nat 'n, Nat 'l, Type 'a, 'l >= 0. (vector<'n,'l,dec,'a>, [|'n - 'l + 1:'n|]) -> 'a effect pure vector_access_dec +(* +val forall Nat 'n, Nat 'l, Type 'a, 'l >= 0. (vector<'n,'l,inc,'a>, [|'n:'n + 'l - 1|]) -> 'a effect pure vector_access_inc +*) + +overload vector_access [vector_access_dec] + +default Order dec + +typedef CauseReg = register bits [ 31 : 0 ] { + 31 : BD; (* branch delay *) + (*30 : Z0;*) + 29 .. 28 : CE; (* for coprocessor enable exception *) + (*27 .. 24 : Z1;*) + 23 : IV; (* special interrupt vector not supported *) + 22 : WP; (* watchpoint exception occurred *) + (*21 .. 16 : Z2; *) + 15 .. 8 : IP; (* interrupt pending bits *) + (*7 : Z3;*) + 6 .. 2 : ExcCode; (* code of last exception *) + (*1 .. 0 : Z4;*) +} + +register (CauseReg) CP0Cause + +val unit -> bit effect {rreg} test + +function bit test () = +{ + CP0Cause[30] +} diff --git a/test/typecheck/pass/return_simple1.sail b/test/typecheck/pass/return_simple1.sail new file mode 100644 index 00000000..26e6fc1d --- /dev/null +++ b/test/typecheck/pass/return_simple1.sail @@ -0,0 +1,8 @@ + +val forall Nat 'N. [|10:'N|] -> [|10:'N|] effect pure return_test + +function forall Nat 'N. [|10:'N|] return_test x = +{ + return x; + x +} diff --git a/test/typecheck/pass/return_simple2.sail b/test/typecheck/pass/return_simple2.sail new file mode 100644 index 00000000..06ce9757 --- /dev/null +++ b/test/typecheck/pass/return_simple2.sail @@ -0,0 +1,11 @@ + +val forall Nat 'N. [|10:'N|] -> [|10:'N|] effect pure return_test + +function forall Nat 'N. [|10:'N|] return_test x = +{ + return x; + return x; + return x; + return x; + x +} diff --git a/test/typecheck/pass/return_simple3.sail b/test/typecheck/pass/return_simple3.sail new file mode 100644 index 00000000..7e81b5b2 --- /dev/null +++ b/test/typecheck/pass/return_simple3.sail @@ -0,0 +1,8 @@ + +val forall Nat 'N, 'N >= 10. [|10:'N|] -> [|10:'N|] effect pure return_test + +function forall Nat 'N, 'N >= 10. [|10:'N|] return_test x = +{ + return x; + sizeof 'N +} diff --git a/test/typecheck/pass/set_mark.sail b/test/typecheck/pass/set_mark.sail new file mode 100644 index 00000000..59710c46 --- /dev/null +++ b/test/typecheck/pass/set_mark.sail @@ -0,0 +1,6 @@ + +val cast forall Num 'n, Num 'm, Order 'ord. [:0:] -> vector<'n,'m,'ord,bit> effect pure cast_zero_bv + +function forall Num 'N, 'N IN {32}. bit['N] Foo32( (bit['N]) x) = x + +let x = Foo32( (bit[32]) 0) diff --git a/test/typecheck/pass/set_mark2.sail b/test/typecheck/pass/set_mark2.sail new file mode 100644 index 00000000..c1433058 --- /dev/null +++ b/test/typecheck/pass/set_mark2.sail @@ -0,0 +1,5 @@ +val cast forall Num 'n, Num 'm, Order 'ord. [:0:] -> vector<'n,'m,'ord,bit> effect pure cast_zero_bv + +function forall Nat 'N, 'N IN {32, 64}. bit['N] Foo32( (bit['N]) x) = x + +let x = Foo32( (bit[64]) 0) diff --git a/test/typecheck/pass/set_spsr.sail b/test/typecheck/pass/set_spsr.sail new file mode 100644 index 00000000..7fac206c --- /dev/null +++ b/test/typecheck/pass/set_spsr.sail @@ -0,0 +1,17 @@ +default Order dec + +val forall Nat 'n, Nat 'l, Nat 'm, Nat 'o, Type 'a, 'l >= 0, 'm <= 'o, 'o <= 'l. + (vector<'n,'l,inc,'a>, [:'m:], [:'o:]) -> vector<'m,'o - 'm,inc,'a> effect pure vector_subrange_inc + +val forall Nat 'n, Nat 'l, Nat 'm, Nat 'o, Type 'a, 'n >= 'm, 'm >= 'o, 'o >= 'n - 'l + 1. + (vector<'n,'l,dec,'a>, [:'m:], [:'o:]) -> vector<'m,'m - ('o - 1),dec,'a> effect pure vector_subrange_dec + +overload vector_subrange [vector_subrange_inc; vector_subrange_dec] + +register bit[32] SPSR_EL2 + +function unit set_SPSR_hyp (bit[32]) val_name = +{ + (bit[32]) r := val_name; + SPSR_EL2[31..0] := r +} diff --git a/test/typecheck/pass/simple_record_access.sail b/test/typecheck/pass/simple_record_access.sail new file mode 100644 index 00000000..d4f4d61f --- /dev/null +++ b/test/typecheck/pass/simple_record_access.sail @@ -0,0 +1,16 @@ +typedef signal = enumerate {LOW; HIGH} + +typedef Bit32 = bit[32] + +typedef Record = + const struct {signal rsig; + Bit32 bitfield;} + +register bit[32] R0 + +val Record -> unit effect {wreg} test + +function unit test ((Record) r) = +{ + R0 := r.bitfield; +} diff --git a/test/typecheck/pass/simple_scattered.sail b/test/typecheck/pass/simple_scattered.sail new file mode 100644 index 00000000..a500cd1f --- /dev/null +++ b/test/typecheck/pass/simple_scattered.sail @@ -0,0 +1,22 @@ + +default Order dec + +scattered typedef ast = const union forall Num 'datasize, Num 'destsize, Num 'regsize. + +val forall Num 'datasize, Num 'destsize, Num 'regsize. + ast<'datasize,'destsize,'regsize> -> unit effect pure execute + +scattered function forall Num 'datasize, Num 'destsize, Num 'regsize. unit execute + +union ast member (bit[8], bit['regsize]) test + +union ast member int test2 + +function clause execute (test (x, y)) = +{ + return () +} + +end ast + +end execute diff --git a/test/typecheck/pass/simple_scattered2.sail b/test/typecheck/pass/simple_scattered2.sail new file mode 100644 index 00000000..8cd26e95 --- /dev/null +++ b/test/typecheck/pass/simple_scattered2.sail @@ -0,0 +1,27 @@ + +default Order dec + +scattered typedef ast = const union forall Num 'datasize, Num 'destsize, Num 'regsize. + +val forall Num 'datasize, Num 'destsize, Num 'regsize. + ast<'datasize,'destsize,'regsize> -> unit effect pure execute + +scattered function forall Num 'datasize, Num 'destsize, Num 'regsize. unit execute + +union ast member (bit[8], bit['regsize]) test + +function clause execute (test (x, y)) = +{ + return () +} + +union ast member int test2 + +function clause execute (test2(x)) = +{ + return () +} + +end ast + +end execute diff --git a/test/typecheck/pass/sizeof_vector_start_index.sail b/test/typecheck/pass/sizeof_vector_start_index.sail new file mode 100644 index 00000000..6ad8ef06 --- /dev/null +++ b/test/typecheck/pass/sizeof_vector_start_index.sail @@ -0,0 +1,12 @@ +val forall Num 'n, Num 'm, Order 'ord, Type 'a. vector<'n,'m,'ord,'a> -> [:'n:] effect pure vector_start_index + +function forall Num 'n, Num 'm, Order 'ord, Type 'a. [:'n:] vector_start_index ((vector<'n,'m,'ord,'a>) vec) = +{ + sizeof 'n +} + +function int test ((vector<47,11,dec,bit>) vec) = +{ + vector_start_index(vec) +} + diff --git a/test/typecheck/pass/union_infer.sail b/test/typecheck/pass/union_infer.sail new file mode 100644 index 00000000..397525e0 --- /dev/null +++ b/test/typecheck/pass/union_infer.sail @@ -0,0 +1,16 @@ + +default Order inc + +typedef option = const union forall Type 'a. { + None; + 'a Some + } + +typedef Test = const union { + A; + B; + C +} + + +function option<Test> test () = Some(C) diff --git a/test/typecheck/pass/vec_pat1.sail b/test/typecheck/pass/vec_pat1.sail new file mode 100644 index 00000000..0a79d701 --- /dev/null +++ b/test/typecheck/pass/vec_pat1.sail @@ -0,0 +1,17 @@ +default Order inc + +val extern forall Num 'n. (bit['n], bit['n]) -> bit['n] effect pure bv_add = "bv_add_inc" + +val forall Num 'n, Num 'm, Num 'o, Num 'p, Type 'a. + (vector<'n,'m,inc,'a>, vector<'o,'p,inc,'a>) -> vector<'n,'m + 'p,inc,'a> + effect pure vector_append_inc + +overload (deinfix +) [bv_add] +overload vector_append [vector_append_inc] + +val (bit[3], bit[3]) -> bit[3] effect pure test + +function bit[3] test (((bit[1]) x : 0b1 : 0b0), z) = +{ + (x : 0b11) + z +} diff --git a/test/typecheck/pass/vector_access.sail b/test/typecheck/pass/vector_access.sail new file mode 100644 index 00000000..4228a62e --- /dev/null +++ b/test/typecheck/pass/vector_access.sail @@ -0,0 +1,15 @@ + +val forall Nat 'n, Nat 'l, Type 'a, 'l >= 0. (vector<'n,'l,dec,'a>, [|'n - 'l + 1:'n|]) -> 'a effect pure vector_access_dec +val forall Nat 'n, Nat 'l, Type 'a, 'l >= 0. (vector<'n,'l,inc,'a>, [|'n:'n + 'l - 1|]) -> 'a effect pure vector_access_inc + +default Order inc + +overload vector_access [vector_access_inc; vector_access_dec] + +val bit[4] -> unit effect pure test + +function unit test v = +{ + z := vector_access(v,3); + z := v[3] +}
\ No newline at end of file diff --git a/test/typecheck/pass/vector_access_dec.sail b/test/typecheck/pass/vector_access_dec.sail new file mode 100644 index 00000000..c59100f0 --- /dev/null +++ b/test/typecheck/pass/vector_access_dec.sail @@ -0,0 +1,15 @@ + +val forall Nat 'n, Nat 'l, Type 'a, 'l >= 0. (vector<'n,'l,dec,'a>, [|'n - 'l + 1:'n|]) -> 'a effect pure vector_access_dec +val forall Nat 'n, Nat 'l, Type 'a, 'l >= 0. (vector<'n,'l,inc,'a>, [|'n:'n + 'l - 1|]) -> 'a effect pure vector_access_inc + +overload vector_access [vector_access_inc; vector_access_dec] + +default Order dec + +val bit[4] -> unit effect pure test + +function unit test v = +{ + z := vector_access(v,3); + z := v[3] +}
\ No newline at end of file diff --git a/test/typecheck/pass/vector_append.sail b/test/typecheck/pass/vector_append.sail new file mode 100644 index 00000000..af83c44d --- /dev/null +++ b/test/typecheck/pass/vector_append.sail @@ -0,0 +1,15 @@ + + +val forall Nat 'n1, Nat 'l1, Nat 'n2, Nat 'l2, Order 'o, Type 'a, 'l1 >= 0, 'l2 >= 0. + (vector<'n1,'l1,'o,'a>, vector<'n2,'l2,'o,'a>) -> vector<'n1,'l1 + 'l2,'o,'a> effect pure vector_append + +default Order inc + +val (bit[4], bit[4]) -> bit[8] effect pure test + +function bit[8] test (v1, v2) = +{ + zv := vector_append(v1, v2); + zv := v1 : v2; + zv +}
\ No newline at end of file diff --git a/test/typecheck/pass/vector_append_gen.sail b/test/typecheck/pass/vector_append_gen.sail new file mode 100644 index 00000000..ddb027ee --- /dev/null +++ b/test/typecheck/pass/vector_append_gen.sail @@ -0,0 +1,14 @@ + +val forall Nat 'n, Nat 'l, Order 'o, Type 'a, 'l >= 0. (vector<'n,'l,'o,'a>, [|'n:'n + 'l - 1|]) -> 'a effect pure vector_access + +val forall Nat 'n1, Nat 'l1, Nat 'n2, Nat 'l2, Order 'o, Type 'a, 'l1 >= 0, 'l2 >= 0. + (vector<'n1,'l1,'o,'a>, vector<'n2,'l2,'o,'a>) -> vector<'n1,'l1 + 'l2,'o,'a> effect pure vector_append + +default Order inc + +val forall 'n, 'm, 'n >= 0, 'm >= 0. (bit['n], bit['m]) -> bit['n + 'm] effect pure test + +function forall 'n, 'm. bit['n + 'm] test (v1, v2) = +{ + vector_append(v1, v2); +}
\ No newline at end of file diff --git a/test/typecheck/pass/vector_subrange_gen.sail b/test/typecheck/pass/vector_subrange_gen.sail new file mode 100644 index 00000000..8857bd18 --- /dev/null +++ b/test/typecheck/pass/vector_subrange_gen.sail @@ -0,0 +1,20 @@ + +val forall Nat 'n, Nat 'l, Order 'o, Type 'a, 'l >= 0. (vector<'n,'l,'o,'a>, [|'n:'n + 'l - 1|]) -> 'a effect pure vector_access + +val forall Nat 'n1, Nat 'l1, Nat 'n2, Nat 'l2, Order 'o, Type 'a, 'l1 >= 0, 'l2 >= 0. + (vector<'n1,'l1,'o,'a>, vector<'n2,'l2,'o,'a>) -> vector<'n1,'l1 + 'l2,'o,'a> effect pure vector_append + +val forall Nat 'n, Nat 'l, Nat 'm, Nat 'u, Order 'o, Type 'a, 'l >= 0, 'm <= 'u, 'u <= 'l. (vector<'n,'l,'o,'a>, [:'m:], [:'u:]) -> vector<'m,'u - 'm,'o,'a> effect pure vector_subrange + +val forall Nat 'n, Nat 'm. ([:'n:], [:'m:]) -> [:'n - 'm:] effect pure minus + +default Order inc + +val forall 'n, 'm, 'n >= 5. bit['n] -> bit['n - 2] effect pure test + +function forall 'n, 'n >= 5. bit['n - 2] test v = +{ + z := vector_subrange(v, 0, minus(sizeof 'n, 2)); + z := v[0 .. minus(sizeof 'n, 2)]; + z +}
\ No newline at end of file diff --git a/test/typecheck/run_tests.sh b/test/typecheck/run_tests.sh new file mode 100755 index 00000000..c4faad7e --- /dev/null +++ b/test/typecheck/run_tests.sh @@ -0,0 +1,127 @@ +#!/usr/bin/env bash +set -e + +DIR="$( cd "$( dirname "${BASH_SOURCE[0]}" )" && pwd )" +SAILDIR="$DIR/../.." + +RED='\033[0;31m' +GREEN='\033[0;32m' +YELLOW='\033[0;33m' +NC='\033[0m' + +mkdir -p $DIR/rtpass +mkdir -p $DIR/rtpass2 +mkdir -p $DIR/lem +mkdir -p $DIR/rtfail + +rm -f $DIR/tests.xml + +MIPS="$SAILDIR/mips_new_tc" + +cat $SAILDIR/lib/prelude.sail $MIPS/mips_prelude.sail > $DIR/pass/mips_prelude.sail +cat $SAILDIR/lib/prelude.sail $MIPS/mips_prelude.sail $MIPS/mips_tlb.sail > $DIR/pass/mips_tlb.sail +cat $SAILDIR/lib/prelude.sail $MIPS/mips_prelude.sail $MIPS/mips_tlb.sail $MIPS/mips_wrappers.sail > $DIR/pass/mips_wrappers.sail +cat $SAILDIR/lib/prelude.sail $MIPS/mips_prelude.sail $MIPS/mips_tlb.sail $MIPS/mips_wrappers.sail $MIPS/mips_insts.sail $MIPS/mips_epilogue.sail > $DIR/pass/mips_insts.sail + +pass=0 +fail=0 + +XML="" + +function green { + (( pass += 1 )) + printf "$1: ${GREEN}$2${NC}\n" + XML+=" <testcase name=\"$1\"/>\n" +} + +function yellow { + (( fail += 1 )) + printf "$1: ${YELLOW}$2${NC}\n" + XML+=" <testcase name=\"$1\">\n <error message=\"$2\">$2</error>\n </testcase>\n" +} + +function red { + (( fail += 1 )) + printf "$1: ${RED}$2${NC}\n" + XML+=" <testcase name=\"$1\">\n <error message=\"$2\">$2</error>\n </testcase>\n" +} + +function finish_suite { + printf "$1: Passed ${pass} out of $(( pass + fail ))\n" + XML=" <testsuite name=\"$1\" tests=\"$(( pass + fail ))\" failures=\"${fail}\" timestamp=\"$(date)\">\n$XML </testsuite>\n" + printf "$XML" >> $DIR/tests.xml + XML="" + pass=0 + fail=0 +} + +printf "<testsuites>\n" >> $DIR/tests.xml + +for i in `ls $DIR/pass/`; +do + if $SAILDIR/sail -ddump_tc_ast -just_check $DIR/pass/$i 2> /dev/null 1> $DIR/rtpass/$i; + then + if $SAILDIR/sail -dno_cast -ddump_tc_ast -just_check $DIR/rtpass/$i 2> /dev/null 1> $DIR/rtpass2/$i; + then + if diff $DIR/rtpass/$i $DIR/rtpass2/$i; + then + green "tested $i expecting pass" "pass" + else + yellow "tested $i expecting pass" "re-check AST was different" + fi + else + yellow "tested $i expecting pass" "failed re-check" + fi + else + red "tested $i expecting pass" "fail" + fi +done + +finish_suite "Expecting pass" + +for i in `ls $DIR/fail/`; +do + if $SAILDIR/sail -ddump_tc_ast -just_check $DIR/fail/$i 2> /dev/null 1> $DIR/rtfail/$i; + then + red "tested $i expecting fail" "pass" + else + if $SAILDIR/sail -dno_cast -just_check $DIR/rtfail/$i 2> /dev/null; + then + yellow "tested $i expecting fail" "passed re-check" + else + green "tested $i expecting fail" "fail" + fi + fi +done + +finish_suite "Expecting fail" + +function test_lem { + for i in `ls $DIR/pass/`; + do + if $SAILDIR/sail -lem $DIR/$1/$i 2> /dev/null + then + mv $SAILDIR/${i%%.*}_embed_types.lem $DIR/lem/ + mv $SAILDIR/${i%%.*}_embed.lem $DIR/lem/ + mv $SAILDIR/${i%%.*}_embed_sequential.lem $DIR/lem/ + if lem -lib $SAILDIR/src/lem_interp -lib $SAILDIR/src/gen_lib/ $DIR/lem/${i%%.*}_embed_types.lem $DIR/lem/${i%%.*}_embed.lem 2> /dev/null + then + green "generated lem for $1/$i" "pass" + else + red "generated lem for $1/$i" "failed to typecheck lem" + fi + else + red "generated lem for $1/$i" "failed to generate lem" + fi + done +} + +test_lem pass + +finish_suite "Lem generation 1" + +test_lem rtpass + +finish_suite "Lem generation 2" + +printf "</testsuites>\n" >> $DIR/tests.xml |