diff options
Diffstat (limited to 'test')
226 files changed, 5225 insertions, 0 deletions
diff --git a/test/mono/.gitignore b/test/mono/.gitignore new file mode 100644 index 00000000..2dd3daa3 --- /dev/null +++ b/test/mono/.gitignore @@ -0,0 +1 @@ +test-out
\ No newline at end of file diff --git a/test/mono/addsubexist.sail b/test/mono/addsubexist.sail new file mode 100644 index 00000000..f59f596e --- /dev/null +++ b/test/mono/addsubexist.sail @@ -0,0 +1,75 @@ +(* Adapted from hand-written ARM model *) + +default Order dec +typedef boolean = bit +typedef reg_size = bit[5] +typedef reg_index = [|31|] + +val reg_size -> reg_index effect pure UInt_reg +val unit -> unit effect pure (* probably not pure *) ReservedValue +function forall Nat 'N. bit['N] NOT((bit['N]) x) = ~(x) +val forall Nat 'M, Nat 'N. bit['M] -> bit['N] effect pure ZeroExtend +val forall Nat 'N. (bit['N], bit['N], bit) -> (bit['N],bit[4]) effect pure AddWithCarry +val forall Nat 'N, 'N IN {8,16,32,64}. (*broken? implicit<'N>*)unit -> bit['N] effect {rreg} rSP +val forall Nat 'N, 'N IN {8,16,32,64}. ((*ditto implicit<'N>,*)reg_index) -> bit['N] effect {rreg}rX +val (unit, bit[4]) -> unit effect {wreg} wPSTATE_NZCV +val forall Nat 'N, 'N IN {32,64}. (unit, bit['N]) -> unit effect {rreg,wreg} wSP +val forall Nat 'N, 'N IN {32,64}. (reg_index,bit['N]) -> unit effect {wreg} wX + +typedef ast = const union +{ + (exist 'R, 'R in {32,64}. (reg_index,reg_index,[:'R:],boolean,boolean,bit['R])) AddSubImmediate; +} + +val ast -> unit effect {rreg,wreg(*,rmem,barr,eamem,wmv,escape*)} execute +scattered function unit execute + +val bit[32] -> option<(ast)> effect pure decodeAddSubtractImmediate + +(* ADD/ADDS (immediate) *) +(* SUB/SUBS (immediate) *) +function option<(ast)> effect pure decodeAddSubtractImmediate ([sf]:[op]:[S]:0b10001:(bit[2]) shift:(bit[12]) imm12:(reg_size) Rn:(reg_size) Rd) = +{ + (reg_index) d := UInt_reg(Rd); + (reg_index) n := UInt_reg(Rn); + let (exist 'R, 'R in {32,64}. [:'R:]) 'datasize = if sf then 64 else 32 in { + (boolean) sub_op := op; + (boolean) setflags := S; + (bit['datasize]) imm := 0; (* ARM: uninitialized *) + + switch shift { + case 0b00 -> imm := ZeroExtend(imm12) + case 0b01 -> imm := ZeroExtend(imm12 : (0b0 ^^ 12)) + case [bitone,_] -> ReservedValue() + }; + + Some(AddSubImmediate( (d,n,datasize,sub_op,setflags,imm) )); +}} + +function clause execute (AddSubImmediate('datasize)) = { +switch datasize { +case (d,n,datasize,sub_op,setflags,imm) -> +{ + (bit['datasize]) operand1 := if n == 31 then rSP() else rX(n); + (bit['datasize]) operand2 := imm; + (bit) carry_in := bitzero; (* ARM: uninitialized *) + + if sub_op then { + operand2 := NOT(operand2); + carry_in := bitone; + } + else + carry_in := bitzero; + + let (result,nzcv) = (AddWithCarry(operand1, operand2, carry_in)) in { + + if setflags then + wPSTATE_NZCV() := nzcv; + + if (d == 31 & ~(setflags)) then + wSP() := result + else + wX(d) := result; + } +}}} +end execute diff --git a/test/mono/fnreduce.sail b/test/mono/fnreduce.sail new file mode 100644 index 00000000..f39fb87d --- /dev/null +++ b/test/mono/fnreduce.sail @@ -0,0 +1,69 @@ +(* Test constant propagation part of monomorphisation involving + functions. We should reduce a function application when the + arguments are suitable values, the function is pure and the result + is a value. + *) + +typedef AnEnum = enumerate { One; Two; Three } + +typedef EnumlikeUnion = const union { First; Second } + +typedef ProperUnion = const union { + (AnEnum) Stuff; + (EnumlikeUnion) Nonsense; +} + +function AnEnum canReduce ((AnEnum) x) = { + switch (x) { + case One -> Two + case x -> x + } +} + +function nat cannotReduce ((AnEnum) x) = { + let (nat) y = switch (x) { case One -> 1 case _ -> 5 } in + 2 + y +} + +function AnEnum effect {rreg} fakeUnpure ((AnEnum) x) = { + switch (x) { + case One -> Two + case x -> x + } +} + +function EnumlikeUnion canReduceUnion ((AnEnum) x) = { + switch (x) { + case One -> First + case _ -> Second + } +} + +function ProperUnion canReduceUnion2 ((AnEnum) x) = { + switch (x) { + case One -> Nonsense(First) + case y -> Stuff(y) + } +} + +(* FIXME LATER: once effect handling is in place we should get an error + because this isn't pure *) + +val AnEnum -> (AnEnum,nat,AnEnum,EnumlikeUnion,ProperUnion) effect pure test + +function test (x) = { + let a = canReduce(x) in + let b = cannotReduce(x) in + let c = fakeUnpure(x) in + let d = canReduceUnion(x) in + let e = canReduceUnion2(x) in + (a,b,c,d,e) +} + +val unit -> bool effect pure run + +function run () = { + test(One) == (Two,3,Two,First,Nonsense(First)) & + test(Two) == (Two,7,Two,Second,Stuff(Two)) & + test(Three) == (Three,7,Three,Second,Stuff(Three)) +} diff --git a/test/mono/set.sail b/test/mono/set.sail new file mode 100644 index 00000000..ecc06137 --- /dev/null +++ b/test/mono/set.sail @@ -0,0 +1,29 @@ +default Order dec + +(* A function which is merely parametrised by a size does not need to be + monomorphised *) + +val forall 'n, 'n in {32,64}. [:'n:] -> bit[64] effect pure parametric + +function parametric(n) = { + let (bit['n]) x = exts(0x80000000) in + extz(x) +} + +(* But if we do a calculation on the size then we'll need to case split *) + +val forall 'n, 'n in {16,32}. [:'n:] -> bit[64] effect pure depends + +function depends(n) = { + let 'm = 2 * n in + let (bit['m]) x = exts(0x80000000) in + extz(x) +} + +val unit -> bool effect pure run + +function run () = + parametric(32) == 0x0000000080000000 & + parametric(64) == 0xffffffff80000000 & + depends(16) == 0x0000000080000000 & + depends(32) == 0xffffffff80000000 diff --git a/test/mono/test.ml b/test/mono/test.ml new file mode 100644 index 00000000..f99abfb8 --- /dev/null +++ b/test/mono/test.ml @@ -0,0 +1 @@ +if Testout_embed_sequential.run() then print_endline "OK" else print_endline "Failed";; diff --git a/test/mono/test.sh b/test/mono/test.sh new file mode 100755 index 00000000..2a5aa80b --- /dev/null +++ b/test/mono/test.sh @@ -0,0 +1,44 @@ +#!/bin/bash + +set -e + +DIR="$( cd "$( dirname "${BASH_SOURCE[0]}" )" && pwd )" +SAILDIR="$DIR/../.." +LEMDIR="$DIR/../../../lem" +OUTDIR="$DIR/test-out" +ZARITH="$LEMDIR/ocaml-lib/dependencies/zarith" + +if [ ! -d "$OUTDIR" ]; then + mkdir -- "$OUTDIR" +fi +cd "$OUTDIR" + +TESTONLY="$1" +if [ -n "$TESTONLY" ]; then shift; fi + +LOG="$DIR/log" +date > "$LOG" + +exec 3< "$DIR/tests" +set +e + +while read -u 3 TEST ARGS; do + if [ -z "$TESTONLY" -o "$TEST" = "$TESTONLY" ]; then +# echo "$TEST ocaml" +# rm -f -- "$OUTDIR"/* +# "$SAILDIR/sail" -ocaml "$SAILDIR/lib/prelude.sail" "$SAILDIR/lib/prelude_wrappers.sail" "$DIR/$TEST" -o "$OUTDIR/testout" $ARGS +# cp -- "$SAILDIR"/src/gen_lib/sail_values.ml . +# cp -- "$DIR"/test.ml . +# ocamlc -I "$ZARITH" "$ZARITH/zarith.cma" -dllpath "$ZARITH" -I "$LEMDIR/ocaml-lib" "$LEMDIR/ocaml-lib/extract.cma" -I "$SAILDIR/src/_build/lem_interp" "$SAILDIR/src/_build/lem_interp/extract.cma" sail_values.ml testout.ml test.ml -o test +# ./test + + echo "$TEST lem - ocaml" | tee -a -- "$LOG" + rm -f -- "$OUTDIR"/* + "$SAILDIR/sail" -lem -lem_sequential -lem_mwords "$SAILDIR/lib/prelude.sail" "$SAILDIR/lib/prelude_wrappers.sail" "$DIR/$TEST".sail -o "$OUTDIR/testout" $ARGS $@ &>> "$LOG" && \ + "$LEMDIR/bin/lem" -ocaml -lib "$SAILDIR/src/lem_interp" "$SAILDIR/src/gen_lib/sail_values.lem" "$SAILDIR/src/gen_lib/sail_operators_mwords.lem" "$SAILDIR/src/gen_lib/state.lem" testout_embed_types_sequential.lem testout_embed_sequential.lem -outdir "$OUTDIR" &>> "$LOG" && \ + cp -- "$DIR"/test.ml "$OUTDIR" && \ + ocamlc -I "$ZARITH" "$ZARITH/zarith.cma" -dllpath "$ZARITH" -I "$LEMDIR/ocaml-lib" "$LEMDIR/ocaml-lib/extract.cma" -I "$SAILDIR/src/_build/lem_interp" "$SAILDIR/src/_build/lem_interp/extract.cma" sail_values.ml sail_operators_mwords.ml state.ml testout_embed_types_sequential.ml testout_embed_sequential.ml test.ml -o test &>> "$LOG" && \ + ./test |& tee -a -- "$LOG" || \ + (echo "Failed:"; echo; tail -- "$LOG"; echo; echo) + fi +done diff --git a/test/mono/tests b/test/mono/tests new file mode 100644 index 00000000..27e161cf --- /dev/null +++ b/test/mono/tests @@ -0,0 +1,9 @@ +fnreduce -mono-split fnreduce.sail:43:x +varmatch -mono-split varmatch.sail:7:x +vector -mono-split vector.sail:7:sel +union-exist -mono-split union-exist.sail:9:v +fnreduce -auto_mono +varmatch -auto_mono +vector -auto_mono +union-exist -auto_mono +set -auto_mono diff --git a/test/mono/union-exist.sail b/test/mono/union-exist.sail new file mode 100644 index 00000000..74ab429a --- /dev/null +++ b/test/mono/union-exist.sail @@ -0,0 +1,33 @@ +default Order dec + +typedef myunion = const union { + (exist 'n, 'n in {8,16}. ([:'n:],bit['n])) MyConstr; +} + +val bit[2] -> myunion effect pure make + +function make(v) = + (* Can't mention these below without running into exp/nexp parsing conflict! *) + let eight = 8 in let sixteen = 16 in + switch v { + case 0b00 -> MyConstr( ( eight, 0x12) ) + case 0b01 -> MyConstr( (sixteen,0x1234) ) + case 0b10 -> MyConstr( ( eight, 0x56) ) + case 0b11 -> MyConstr( (sixteen,0x5678) ) + } + +val myunion -> bit[32] effect pure use + +function use(MyConstr('n)) = { + switch n { + case (n,v) -> extz(v) + } +} +val unit -> bool effect pure run + +function run () = { + use(make(0b00)) == 0x00000012 & + use(make(0b01)) == 0x00001234 & + use(make(0b10)) == 0x00000056 & + use(make(0b11)) == 0x00005678 +} diff --git a/test/mono/varmatch.sail b/test/mono/varmatch.sail new file mode 100644 index 00000000..7d2b9b73 --- /dev/null +++ b/test/mono/varmatch.sail @@ -0,0 +1,19 @@ +(* Check that when we case split on a variable that the constant propagation + handles the default case correctly. *) + +typedef AnEnum = enumerate { One; Two; Three } + +function AnEnum foo((AnEnum) x) = { + switch (x) { + case One -> Two + case y -> y + } +} + +val unit -> bool effect pure run + +function run () = { + foo(One) == Two & + foo(Two) == Two & + foo(Three) == Three +} diff --git a/test/mono/vector.sail b/test/mono/vector.sail new file mode 100644 index 00000000..03f36da5 --- /dev/null +++ b/test/mono/vector.sail @@ -0,0 +1,21 @@ +(* Check case splitting on a vector *) + +default Order dec + +val bit[32] -> nat effect pure test + +function nat test((bit[2]) sel : (bit[30]) _) = { + switch (sel) { + case 0b00 -> 5 + case 0b10 -> 1 + case _ -> 0 + } +} + +val unit -> bool effect pure run + +function run () = { + test(0x0f353533) == 5 & + test(0x84534656) == 1 & + test(0xf3463903) == 0 +} diff --git a/test/ocaml/hello_world/expect b/test/ocaml/hello_world/expect new file mode 100644 index 00000000..3df47a31 --- /dev/null +++ b/test/ocaml/hello_world/expect @@ -0,0 +1,2 @@ +Hello, Sail! +Hello, World! diff --git a/test/ocaml/hello_world/hello_world.sail b/test/ocaml/hello_world/hello_world.sail new file mode 100644 index 00000000..bafea2de --- /dev/null +++ b/test/ocaml/hello_world/hello_world.sail @@ -0,0 +1,18 @@ +val hello_world : unit -> string + +function hello_world () = { + return("Hello, World!"); + "Unreachable" +} + +val main : unit -> unit effect {wreg, rreg} + +register REG : string + +function main () = { + REG = "Hello, Sail!"; + print(REG); + REG = hello_world(); + print(REG); + return(()) +} diff --git a/test/ocaml/loop/expect b/test/ocaml/loop/expect new file mode 100644 index 00000000..190423f8 --- /dev/null +++ b/test/ocaml/loop/expect @@ -0,0 +1,100 @@ +1 +2 +3 +4 +5 +6 +7 +8 +9 +10 +11 +12 +13 +14 +15 +16 +17 +18 +19 +20 +21 +22 +23 +24 +25 +26 +27 +28 +29 +30 +31 +32 +33 +34 +35 +36 +37 +38 +39 +40 +41 +42 +43 +44 +45 +46 +47 +48 +49 +50 +51 +52 +53 +54 +55 +56 +57 +58 +59 +60 +61 +62 +63 +64 +65 +66 +67 +68 +69 +70 +71 +72 +73 +74 +75 +76 +77 +78 +79 +80 +81 +82 +83 +84 +85 +86 +87 +88 +89 +90 +91 +92 +93 +94 +95 +96 +97 +98 +99 +100 diff --git a/test/ocaml/loop/loop.sail b/test/ocaml/loop/loop.sail new file mode 100644 index 00000000..3808c19a --- /dev/null +++ b/test/ocaml/loop/loop.sail @@ -0,0 +1,19 @@ +val string_of_int = "string_of_big_int" : int -> string + +val add = "add" : (int, int) -> int + +val lt = "lt_int" : (int, int) -> bool + +overload operator + = {add} + +overload operator < = {lt} + +val main : unit -> unit + +function main () = { + x : int = 0; + while x < 100 do { + x = x + 1; + print(string_of_int(x)) + } +} diff --git a/test/ocaml/lsl/expect b/test/ocaml/lsl/expect new file mode 100644 index 00000000..c72d1eb8 --- /dev/null +++ b/test/ocaml/lsl/expect @@ -0,0 +1,4 @@ +pass +pass +pass +pass diff --git a/test/ocaml/lsl/lsl.sail b/test/ocaml/lsl/lsl.sail new file mode 100644 index 00000000..8c3e9700 --- /dev/null +++ b/test/ocaml/lsl/lsl.sail @@ -0,0 +1,28 @@ +val zeros : forall ('n : Int), 'n >= 0. atom('n) -> bits('n) + +function zeros n = replicate_bits(0b0, 'n) + +val lslc : forall ('n : Int) ('shift : Int), 'n >= 0. + (bits('n), atom('shift)) -> (bits('n), bit) effect {escape} + +function lslc (vec, shift) = { + assert(constraint('shift >= 1), "shift must be positive"); + extended : bits('shift + 'n) = vec @ zeros(shift); + result : bits('n) = extended[sizeof('n - 1) .. 0]; + c : bit = extended['n]; + return((result, c)) +} + +val lsl : forall ('n : Int) ('shift : Int), 'n >= 0. + (bits('n), atom('shift)) -> bits('n) effect {escape} + +function lsl (vec, shift) = if shift == 0 then vec else let (result, _) = lslc(vec, shift) in result + +val main : unit -> unit effect {escape} + +function main () = { + print(if lsl(0b0110, 1) == 0b1100 then "pass" else "fail"); + print(if lsl(0b1111, 2) == 0b1100 then "pass" else "fail"); + print(if lsl(0x0F, 4) == 0xF0 then "pass" else "fail"); + let (result, c) = lslc(0xF000, 2) in print(if (result == 0xC000) & (c == bitone) then "pass" else "fail") +} diff --git a/test/ocaml/pattern1/expect b/test/ocaml/pattern1/expect new file mode 100644 index 00000000..2ae28399 --- /dev/null +++ b/test/ocaml/pattern1/expect @@ -0,0 +1 @@ +pass diff --git a/test/ocaml/pattern1/pattern.sail b/test/ocaml/pattern1/pattern.sail new file mode 100644 index 00000000..3c28d46e --- /dev/null +++ b/test/ocaml/pattern1/pattern.sail @@ -0,0 +1,9 @@ +val main : unit -> unit + +function main () = { + vec = 0x4F; + match vec { + 0b01 @ x : bits(2) @ 0xF => if x == 0b00 then print("pass") else print("x is incorrect"), + _ => print("pattern fail") + } +} diff --git a/test/ocaml/prelude.sail b/test/ocaml/prelude.sail new file mode 100644 index 00000000..b56ce7e2 --- /dev/null +++ b/test/ocaml/prelude.sail @@ -0,0 +1,288 @@ +default Order dec + +type bits ('n : Int) = vector('n - 1, 'n, dec, bit) + +infix 4 == + +val eq_atom = "eq_int" : forall 'n 'm. (atom('n), atom('m)) -> bool +val lteq_atom = "lteq" : forall 'n 'm. (atom('n), atom('m)) -> bool +val gteq_atom = "gteq" : forall 'n 'm. (atom('n), atom('m)) -> bool +val lt_atom = "lt" : forall 'n 'm. (atom('n), atom('m)) -> bool +val gt_atom = "gt" : forall 'n 'm. (atom('n), atom('m)) -> bool + +val eq_int = "eq_int" : (int, int) -> bool + +val eq_vec = "eq_list" : forall 'n. (bits('n), bits('n)) -> bool + +val eq_string = "eq_string" : (string, string) -> bool + +val eq_real = "eq_real" : (real, real) -> bool + +val eq_anything = "(fun (x, y) -> x = y)" : forall ('a : Type). ('a, 'a) -> bool + +val length = "length" : forall 'n ('a : Type). vector('n - 1, 'n, dec, 'a) -> atom('n) + +overload operator == = {eq_atom, eq_int, eq_vec, eq_string, eq_real, eq_anything} + +val vector_subrange_A = "subrange" : forall ('n : Int) ('m : Int) ('o : Int), 'o <= 'm <= 'n. + (bits('n), atom('m), atom('o)) -> bits('m - ('o - 1)) + +val vector_subrange_B = "subrange" : forall ('n : Int) ('m : Int) ('o : Int). + (bits('n), atom('m), atom('o)) -> bits('m - ('o - 1)) + +overload vector_subrange = {vector_subrange_A, vector_subrange_B} + +val vector_access_A = "access" : forall ('n : Int) ('m : Int) ('a : Type), 0 <= 'm < 'n. + (vector('n - 1, 'n, dec, 'a), atom('m)) -> 'a + +val vector_access_B = "access" : forall ('n : Int) ('a : Type). + (vector('n - 1, 'n, dec, 'a), int) -> 'a + +overload vector_access = {vector_access_A, vector_access_B} + +val vector_update = "update" : forall 'n ('a : Type). + (vector('n - 1, 'n, dec, 'a), int, 'a) -> vector('n - 1, 'n, dec, 'a) + +val vector_update_subrange = "update_subrange" : forall 'n 'm 'o. + (bits('n), atom('m), atom('o), bits('m - ('o - 1))) -> bits('n) + +val vcons : forall ('n : Int) ('a : Type). + ('a, vector('n - 1, 'n, dec, 'a)) -> vector('n, 'n + 1, dec, 'a) + +val append = "append" : forall ('n : Int) ('m : Int) ('a : Type). + (vector('n - 1, 'n, dec, 'a), vector('m - 1, 'm, dec, 'a)) -> vector('n + 'm - 1, 'n + 'm, dec, 'a) + +val not_bool = "not" : bool -> bool + +val not_vec = "not_vec" : forall 'n. bits('n) -> bits('n) + +overload ~ = {not_bool, not_vec} + +val neq_atom : forall 'n 'm. (atom('n), atom('m)) -> bool + +function neq_atom (x, y) = not_bool(eq_atom(x, y)) + +val neq_int : (int, int) -> bool + +function neq_int (x, y) = not_bool(eq_int(x, y)) + +val neq_vec : forall 'n. (bits('n), bits('n)) -> bool + +function neq_vec (x, y) = not_bool(eq_vec(x, y)) + +val neq_anything : forall ('a : Type). ('a, 'a) -> bool + +function neq_anything (x, y) = not_bool(x == y) + +overload operator != = {neq_atom, neq_int, neq_vec, neq_anything} + +val and_bool = "and_bool" : (bool, bool) -> bool + +val builtin_and_vec = "and_vec" : forall 'n. (bits('n), bits('n)) -> bits('n) + +val and_vec : forall 'n. (bits('n), bits('n)) -> bits('n) + +function and_vec (xs, ys) = builtin_and_vec(xs, ys) + +overload operator & = {and_bool, and_vec} + +val or_bool = "or_bool" : (bool, bool) -> bool + +val builtin_or_vec = "or_vec" : forall 'n. (bits('n), bits('n)) -> bits('n) + +val or_vec : forall 'n. (bits('n), bits('n)) -> bits('n) + +function or_vec (xs, ys) = builtin_or_vec(xs, ys) + +overload operator | = {or_bool, or_vec} + +val UInt = "uint" : forall 'n. bits('n) -> range(0, 2 ^ 'n - 1) + +val SInt = "sint" : forall 'n. bits('n) -> range(- (2 ^ ('n - 1)), 2 ^ ('n - 1) - 1) + +val hex_slice = "hex_slice" : forall 'n 'm. (string, atom('n), atom('m)) -> bits('n - 'm) + +val __SetSlice_bits = "set_slice" : forall 'n 'm. + (atom('n), atom('m), bits('n), int, bits('m)) -> bits('n) + +val __SetSlice_int = "set_slice_int" : forall 'w. (atom('w), int, int, bits('w)) -> int + +val __raw_SetSlice_int : forall 'w. (atom('w), int, int, bits('w)) -> int + +val __raw_GetSlice_int = "get_slice_int" : forall 'w. (atom('w), int, int) -> bits('w) + +val __GetSlice_int : forall 'n. (atom('n), int, int) -> bits('n) + +function __GetSlice_int (n, m, o) = __raw_GetSlice_int(n, m, o) + +val __raw_SetSlice_bits : forall 'n 'w. + (atom('n), atom('w), bits('n), int, bits('w)) -> bits('n) + +val __raw_GetSlice_bits : forall 'n 'w. + (atom('n), atom('w), bits('n), int) -> bits('w) + +val __ShiftLeft : forall 'm. (bits('m), int) -> bits('m) + +val __SignExtendSlice : forall 'm. (bits('m), int, int) -> bits('m) + +val __ZeroExtendSlice : forall 'm. (bits('m), int, int) -> bits('m) + +val cast cast_unit_vec : bit -> bits(1) + +val print = "print_endline" : string -> unit + +val putchar = "putchar" : forall ('a : Type). 'a -> unit + +val concat_str = "concat_str" : (string, string) -> string + +val DecStr : int -> string + +val HexStr : int -> string + +val BitStr = "string_of_bits" : forall 'n. bits('n) -> string + +val xor_vec = "xor_vec" : forall 'n. (bits('n), bits('n)) -> bits('n) + +val int_power : (int, int) -> int + +val real_power = "real_power" : (real, int) -> real + +overload operator ^ = {xor_vec, int_power, real_power} + +val add_range = "add" : forall 'n 'm 'o 'p. + (range('n, 'm), range('o, 'p)) -> range('n + 'o, 'm + 'p) + +val add_int = "add" : (int, int) -> int + +val add_vec = "add_vec" : forall 'n. (bits('n), bits('n)) -> bits('n) + +val add_vec_int = "add_vec_int" : forall 'n. (bits('n), int) -> bits('n) + +val add_real = "add_real" : (real, real) -> real + +overload operator + = {add_range, add_int, add_vec, add_vec_int, add_real} + +val sub_range = "sub" : forall 'n 'm 'o 'p. + (range('n, 'm), range('o, 'p)) -> range('n - 'p, 'm - 'o) + +val sub_int = "sub" : (int, int) -> int + +val sub_vec : forall 'n. (bits('n), bits('n)) -> bits('n) + +val sub_vec_int = "sub_vec_int" : forall 'n. (bits('n), int) -> bits('n) + +val sub_real = "sub_real" : (real, real) -> real + +val negate_range = "minus_big_int" : forall 'n 'm. range('n, 'm) -> range(- 'm, - 'n) + +val negate_int = "minus_big_int" : int -> int + +val negate_real = "Num.minus_num" : real -> real + +overload operator - = {sub_range, sub_int, sub_vec, sub_vec_int, sub_real} + +overload negate = {negate_range, negate_int, negate_real} + +val mult_range = "mult" : forall 'n 'm 'o 'p. + (range('n, 'm), range('o, 'p)) -> range('n * 'o, 'm * 'p) + +val mult_int = "mult" : (int, int) -> int + +val mult_real = "mult_real" : (real, real) -> real + +overload operator * = {mult_range, mult_int, mult_real} + +val Sqrt = "sqrt_real" : real -> real + +val gteq_int = "gteq" : (int, int) -> bool + +val gteq_real = "gteq_real" : (real, real) -> bool + +overload operator >= = {gteq_atom, gteq_int, gteq_real} + +val lteq_int = "lteq" : (int, int) -> bool + +val lteq_real = "lteq_real" : (real, real) -> bool + +overload operator <= = {lteq_atom, lteq_int, lteq_real} + +val gt_int = "gt" : (int, int) -> bool + +val gt_real = "gt_real" : (real, real) -> bool + +overload operator > = {gt_atom, gt_int, gt_real} + +val lt_int = "lt" : (int, int) -> bool + +val lt_real = "lt_real" : (real, real) -> bool + +overload operator < = {lt_atom, lt_int, lt_real} + +val RoundDown = "round_down" : real -> int + +val RoundUp = "round_up" : real -> int + +val abs = "abs_num" : real -> real + +val quotient_nat = "quotient" : (nat, nat) -> nat + +val quotient_real = "quotient_real" : (real, real) -> real + +val quotient = "quotient" : (int, int) -> int + +infixl 7 / + +overload operator / = {quotient_nat, quotient, quotient_real} + +val modulus = "modulus" : (int, int) -> int + +infixl 7 % + +overload operator % = {modulus} + +val Real = "Num.num_of_big_int" : int -> real + +val shl_int = "shl_int" : (int, int) -> int + +val shr_int = "shr_int" : (int, int) -> int + +val min_nat = "min_int" : (nat, nat) -> nat + +val min_int = "min_int" : (int, int) -> int + +val max_nat = "max_int" : (nat, nat) -> nat + +val max_int = "max_int" : (int, int) -> int + +overload min = {min_nat, min_int} + +overload max = {max_nat, max_int} + +val replicate_bits = "replicate_bits" : forall 'n 'm. (bits('n), atom('m)) -> bits('n * 'm) + +val cast ex_nat : nat -> {'n, 'n >= 0. atom('n)} + +function ex_nat 'n = n + +val cast ex_int : int -> {'n, true. atom('n)} + +function ex_int 'n = n + +val ex_range : forall 'n 'm. + range('n, 'm) -> {'o, 'n <= 'o & 'o <= 'm. atom('o)} + +val coerce_int_nat : int -> nat effect {escape} + +function coerce_int_nat 'x = { + assert(constraint('x >= 0)); + x +} + +val slice = "slice" : forall ('n : Int) ('m : Int), 'm >= 0 & 'n >= 0. + (bits('m), int, atom('n)) -> bits('n) + +val pow2 = "pow2" : forall 'n. atom('n) -> atom(2 ^ 'n) + +val "print_int" : (string, int) -> unit + +val "print_bits" : forall 'n. (string, bits('n)) -> unit
\ No newline at end of file diff --git a/test/ocaml/reg_passing/expect b/test/ocaml/reg_passing/expect new file mode 100644 index 00000000..e64f92f2 --- /dev/null +++ b/test/ocaml/reg_passing/expect @@ -0,0 +1,3 @@ +R1 = 10 +R2 = 20 +R3 = 10 diff --git a/test/ocaml/reg_passing/reg_passing.sail b/test/ocaml/reg_passing/reg_passing.sail new file mode 100644 index 00000000..94acdf7e --- /dev/null +++ b/test/ocaml/reg_passing/reg_passing.sail @@ -0,0 +1,36 @@ + +register R1 : int +register R2 : int +register R3 : int + +val cast "reg_deref" : forall ('a : Type). register('a) -> 'a effect {rreg} +val output = { + ocaml: "(fun (str, n) -> print_endline (str ^ string_of_big_int n))" + } : (string, int) -> unit + +val f : register(int) -> unit effect {rreg, wreg} + +function f R = { + R1 = R; +} + +val g : unit -> unit effect {rreg, wreg} + +function g () = { + f(R1); + f(R2); +} + +val main : unit -> unit effect {rreg, wreg} + +function main () = { + R1 = 4; + R2 = 5; + g (); + R3 = 10; + f(R3); + R2 = 20; + output("R1 = ", R1); + output("R2 = ", R2); + output("R3 = ", R3) +}
\ No newline at end of file diff --git a/test/ocaml/run_tests.sh b/test/ocaml/run_tests.sh new file mode 100755 index 00000000..9ed00494 --- /dev/null +++ b/test/ocaml/run_tests.sh @@ -0,0 +1,96 @@ +#!/usr/bin/env bash +set -e + +DIR="$( cd "$( dirname "${BASH_SOURCE[0]}" )" && pwd )" +cd $DIR +SAILDIR="$DIR/../.." + +RED='\033[0;31m' +GREEN='\033[0;32m' +YELLOW='\033[0;33m' +NC='\033[0m' + +rm -f $DIR/tests.xml + +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 +} + +SAILLIBDIR="$DIR/../../lib/" + +printf "<testsuites>\n" >> $DIR/tests.xml + +for i in `ls -d */`; +do + cd $DIR/$i; + if $SAILDIR/sail -new_parser -o out -ocaml ../prelude.sail `ls *.sail` 1> /dev/null; + then + ./out > result; + if diff expect result; + then + green "built $i" "ok" + else + yellow "bad output $i" "fail" + fi; + rm out; + rm result; + rm -r _sbuild + else + red "building $i" "fail" + fi +done + +finish_suite "Ocaml testing" + +cd $DIR + +for i in `ls -d */`; +do + cd $DIR/$i; + if $SAILDIR/sail -new_parser -o out -ocaml_trace ../prelude.sail `ls *.sail` 1> /dev/null; + then + ./out > result 2> /dev/null; + if diff expect result; + then + green "built $i" "ok" + else + yellow "bad output $i" "fail" + fi; + rm out; + rm result; + rm -r _sbuild + else + red "building $i" "fail" + fi +done + +finish_suite "Ocaml trace testing" + +printf "</testsuites>\n" >> $DIR/tests.xml diff --git a/test/ocaml/short_circuit/expect b/test/ocaml/short_circuit/expect new file mode 100644 index 00000000..9766475a --- /dev/null +++ b/test/ocaml/short_circuit/expect @@ -0,0 +1 @@ +ok diff --git a/test/ocaml/short_circuit/sc.sail b/test/ocaml/short_circuit/sc.sail new file mode 100644 index 00000000..a0f4941d --- /dev/null +++ b/test/ocaml/short_circuit/sc.sail @@ -0,0 +1,15 @@ + +val fail : unit -> bool effect {escape} + +function fail () = { + assert(false); + true +} + +val main : unit -> unit effect {escape} + +function main () = { + assert(~(false & fail())); + assert(true | fail()); + print("ok") +}
\ No newline at end of file diff --git a/test/ocaml/string_equality/expect b/test/ocaml/string_equality/expect new file mode 100644 index 00000000..27ba77dd --- /dev/null +++ b/test/ocaml/string_equality/expect @@ -0,0 +1 @@ +true diff --git a/test/ocaml/string_equality/string_equality.sail b/test/ocaml/string_equality/string_equality.sail new file mode 100644 index 00000000..568052cd --- /dev/null +++ b/test/ocaml/string_equality/string_equality.sail @@ -0,0 +1,3 @@ +val main : unit -> unit + +function main () = if "test" == "test" then print("true") else print("false") diff --git a/test/ocaml/trycatch/expect b/test/ocaml/trycatch/expect new file mode 100644 index 00000000..0aab34df --- /dev/null +++ b/test/ocaml/trycatch/expect @@ -0,0 +1,2 @@ +Before throw +Caught! diff --git a/test/ocaml/trycatch/tc.sail b/test/ocaml/trycatch/tc.sail new file mode 100644 index 00000000..b805f3fa --- /dev/null +++ b/test/ocaml/trycatch/tc.sail @@ -0,0 +1,23 @@ + +scattered union exception + +union clause exception = Test_int : int + +union clause exception = Test_failure : string + +val main : unit -> unit effect {escape} + +function main () = { + try { + print("Before throw"); + throw(Test_failure("Caught!")); + print("Not printed") + } catch { + Test_failure(msg) => print(msg), + _ => print("Unknown exception") + } +} + +union clause exception = Test_other + +end exception
\ No newline at end of file diff --git a/test/ocaml/types/expect b/test/ocaml/types/expect new file mode 100644 index 00000000..747ef4c9 --- /dev/null +++ b/test/ocaml/types/expect @@ -0,0 +1,5 @@ +pass +pass +pass +pass +pass diff --git a/test/ocaml/types/types.sail b/test/ocaml/types/types.sail new file mode 100644 index 00000000..a710eb25 --- /dev/null +++ b/test/ocaml/types/types.sail @@ -0,0 +1,44 @@ +enum signal = {Low, High} + +enum enum_single = {SingleConstructor} + +type byte = bits(8) + +type b32 = bits(32) + +type b64 = bits(64) + +register R64 : b64 + +register R32 : b32 + +register R8 : byte + +register SIGNALREG : signal + +struct TestStruct = { + field1 : bits(2), + field2 : byte, + field3 : bool +} + +register SREG : TestStruct + +union option ('a : Type) = {None, Some : 'a} + +register OREG : option(byte) + +val main : unit -> unit effect {rreg, wreg} + +function main () = { + R8 = 0xFF; + SIGNALREG = Low; + print(if SIGNALREG == Low then "pass" else "fail"); + SIGNALREG = High; + print(if SIGNALREG == High then "pass" else "fail"); + SREG.field1 = 0b00; + print(if SREG.field1 == 0b00 then "pass" else "faiL"); + SREG.field1 = 0b11; + print(if SREG.field1 == 0b11 then "pass" else "faiL"); + print("pass") +} diff --git a/test/ocaml/vec_32_64/expect b/test/ocaml/vec_32_64/expect new file mode 100644 index 00000000..4d4fce36 --- /dev/null +++ b/test/ocaml/vec_32_64/expect @@ -0,0 +1,2 @@ +xs = 0x00000000 +zeros(64) = 0x0000000000000000 diff --git a/test/ocaml/vec_32_64/vec_32_64.sail b/test/ocaml/vec_32_64/vec_32_64.sail new file mode 100644 index 00000000..eb518515 --- /dev/null +++ b/test/ocaml/vec_32_64/vec_32_64.sail @@ -0,0 +1,28 @@ +(* This example is more testing the typechecker flow typing rather +than the ocaml backend, but it does test that recursive functions work +correctly *) + +val get_size : unit -> {|32, 64|} + +function get_size () = 32 + +val only64 = { ocaml: "(fun _ -> ())" } : bits(64) -> unit + +val zeros : forall 'n. atom('n) -> vector('n - 1, 'n, dec, bit) + +function zeros n = + if (n == 1 + 0) then 0b0 else 0b0 @ zeros('n - 1) + +val main : unit -> unit + +function main () = { + let 'length = get_size (); + let xs = zeros(length); + if (length == 32) then { + () + } else { + only64(xs) + }; + print_bits("xs = ", xs); + print_bits("zeros(64) = ", zeros(64)) +}
\ No newline at end of file diff --git a/test/ocaml/void/expect b/test/ocaml/void/expect new file mode 100644 index 00000000..559bf40a --- /dev/null +++ b/test/ocaml/void/expect @@ -0,0 +1 @@ +Before diff --git a/test/ocaml/void/void.sail b/test/ocaml/void/void.sail new file mode 100644 index 00000000..485ac019 --- /dev/null +++ b/test/ocaml/void/void.sail @@ -0,0 +1,14 @@ + +val void : forall 'n, 'n = 'n + 1. atom('n) -> unit + +function void _ = () + +val main : unit -> unit + +function main () = { + print("Before"); + if false then { + print("After"); + void(0); + } +}
\ No newline at end of file diff --git a/test/run_tests.sh b/test/run_tests.sh new file mode 100755 index 00000000..73f622c7 --- /dev/null +++ b/test/run_tests.sh @@ -0,0 +1,8 @@ +#!/usr/bin/env bash +set -e + +DIR="$( cd "$( dirname "${BASH_SOURCE[0]}" )" && pwd )" + +cd $DIR/.. +./test/typecheck/run_tests.sh +./test/ocaml/run_tests.sh 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/ex_cast.sail b/test/typecheck/fail/ex_cast.sail new file mode 100644 index 00000000..5ea22d14 --- /dev/null +++ b/test/typecheck/fail/ex_cast.sail @@ -0,0 +1,12 @@ + +default Order dec + +val cast int -> exist 'n. [:'n:] effect pure ex_int + +val [:'n:] -> bit['n] effect pure zeros + +val int -> unit effect pure test + +function test n = { + x := zeros(n) +} diff --git a/test/typecheck/fail/exist1.sail b/test/typecheck/fail/exist1.sail new file mode 100644 index 00000000..3fab1366 --- /dev/null +++ b/test/typecheck/fail/exist1.sail @@ -0,0 +1,30 @@ + +let (exist 'n, 'n in {0, 1}. [:'n:]) v1 = 0 + +val bool -> exist 'n, 'n in {0, 1}. [:'n:] effect pure test + +function test flag = +{ + if flag then 0 else 1 +} + +let ([|0:1|]) v2 = test(true) + +val forall 'a, 'b. ([:'a:], [:'b:]) -> [:'a + 'b:] effect pure add + +let (exist 'k, 'k in {3, 4}. [:'k:]) v3 = 3 + +let (exist 'q, 'q in {0, 1}. [:'q + 3:]) v4 = v3 + +let v5 = add(test(true), 4) + +let ([:4:]) v6 = 4 + +function unit unit_fn (([:4:]) x) = () + +val forall 'a. ([:'a:], [:'a:]) -> [:'a + 'a:] effect pure s_add + +let (exist 'k, 'k = 4. [:'k:]) v7 = 4 + +let v8 = s_add(test(true), 4) + 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/mismatch_return.sail b/test/typecheck/fail/mismatch_return.sail new file mode 100644 index 00000000..85b8b636 --- /dev/null +++ b/test/typecheck/fail/mismatch_return.sail @@ -0,0 +1,7 @@ + +val unit -> unit effect pure test + +function int test () = +{ + () +} 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/overlap_field_wreg.sail b/test/typecheck/fail/overlap_field_wreg.sail new file mode 100644 index 00000000..4c4d858d --- /dev/null +++ b/test/typecheck/fail/overlap_field_wreg.sail @@ -0,0 +1,13 @@ + +typedef A = const struct {bool field_A; int shared} +typedef B = const struct {bool field_B; int shared} + +val (bool, int) -> A effect {undef, wreg} makeA + +function makeA (x, y) = +{ + (A) record := undefined; + record.field_A := x; + record.shared := y; + record +} 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/pure_record_arity.sail b/test/typecheck/fail/pure_record_arity.sail new file mode 100644 index 00000000..846df2c3 --- /dev/null +++ b/test/typecheck/fail/pure_record_arity.sail @@ -0,0 +1,25 @@ +default Order dec + +typedef State = const struct forall Type 'a, Nat 'n. { + vector<0, 'n, dec, 'a> N; + vector<0, 1, dec, bit> Z; +} + +register State procState + +let (State<bit,1>) myStateM = { + (State<bit,1>) r := undefined; + r.N := 0b1; + r.Z := 0b1; + r +} + +let (State<bit,1>) myState = { N = 0b1; Z = 0b1 } + +val unit -> unit effect {undef} test + +function test () = { + (State<bit,1>) myState1 := undefined; + (State<bit,1>) myState2 := { N = undefined; Z = 0b1 }; + (State<bit,1>) myState3 := { myState2 with N = 0b0 } +} diff --git a/test/typecheck/fail/pure_record_arity2.sail b/test/typecheck/fail/pure_record_arity2.sail new file mode 100644 index 00000000..a9566da8 --- /dev/null +++ b/test/typecheck/fail/pure_record_arity2.sail @@ -0,0 +1,25 @@ +default Order dec + +typedef State = const struct forall Type 'a, Nat 'n. { + vector<0, 'n, dec, 'a> N; + vector<0, 1, dec, bit> Z; +} + +register State<bit,inc> procState + +let (State<bit,1>) myStateM = { + (State<bit,1>) r := undefined; + r.N := 0b1; + r.Z := 0b1; + r +} + +let (State<bit,1>) myState = { N = 0b1; Z = 0b1 } + +val unit -> unit effect {undef} test + +function test () = { + (State<bit,1>) myState1 := undefined; + (State<bit,1>) myState2 := { N = undefined; Z = 0b1 }; + (State<bit,1>) myState3 := { myState2 with N = 0b0 } +} 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_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_append_old.sail b/test/typecheck/fail/vector_append_old.sail new file mode 100644 index 00000000..fb6018b9 --- /dev/null +++ b/test/typecheck/fail/vector_append_old.sail @@ -0,0 +1,14 @@ + +val extern forall Nat 'n1, Nat 'l1, Nat 'n2, Nat 'l2, Order 'o, 'l1 >= 0, 'l2 >= 0. + (vector<'n1,'l1,'o,bit>, vector<'n2,'l2,'o,bit>) -> vector<'n1,'l1 + 'l2,'o,bit> effect pure vector_append = "bitvector_concat" + +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 +} 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_real.sail b/test/typecheck/pass/add_real.sail new file mode 100644 index 00000000..38a9cff3 --- /dev/null +++ b/test/typecheck/pass/add_real.sail @@ -0,0 +1,5 @@ +val (real, real) -> real effect pure add_real + +overload (deinfix +) [add_real] + +let (real) r = 2.2 + 0.2 diff --git a/test/typecheck/pass/add_vec_exts_no_annot.sail b/test/typecheck/pass/add_vec_exts_no_annot.sail new file mode 100644 index 00000000..54aa2d40 --- /dev/null +++ b/test/typecheck/pass/add_vec_exts_no_annot.sail @@ -0,0 +1,19 @@ +default Order dec + +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 EXTS [exts] + +val forall Nat 'n, Nat 'o, Order 'ord. + (vector<'o, 'n, 'ord, bit>, vector<'o, 'n, 'ord, bit>) -> vector<'o, 'n, 'ord, bit> effect pure add_vec + +overload (deinfix +) [add_vec] + +val (bit[32], bit[32]) -> unit effect pure test + +function test (x, y) = +{ + let (bit[64]) z = add_vec(exts(x), exts(y)) in + () +} diff --git a/test/typecheck/pass/add_vec_exts_no_annot_overload.sail b/test/typecheck/pass/add_vec_exts_no_annot_overload.sail new file mode 100644 index 00000000..01e3bf7c --- /dev/null +++ b/test/typecheck/pass/add_vec_exts_no_annot_overload.sail @@ -0,0 +1,19 @@ +default Order dec + +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 EXTS [exts] + +val forall Nat 'n, Nat 'o, Order 'ord. + (vector<'o, 'n, 'ord, bit>, vector<'o, 'n, 'ord, bit>) -> vector<'o, 'n, 'ord, bit> effect pure add_vec + +overload (deinfix +) [add_vec] + +val (bit[32], bit[32]) -> unit effect pure test + +function test (x, y) = +{ + let (bit[64]) z = EXTS(x) + EXTS(y) in + () +} diff --git a/test/typecheck/pass/add_vec_lit.sail b/test/typecheck/pass/add_vec_lit.sail new file mode 100644 index 00000000..4d662a8d --- /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 unsigned + +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..f711a5ad --- /dev/null +++ b/test/typecheck/pass/arm_FPEXC1.sail @@ -0,0 +1,53 @@ +default Order dec + +val extern forall Num 'n. (bit['n], int) -> bit effect pure vector_access = "bitvector_access_dec" + +val extern 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 = "bitvector_subrange_dec" + +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/as_pattern.sail b/test/typecheck/pass/as_pattern.sail new file mode 100644 index 00000000..a1cd9461 --- /dev/null +++ b/test/typecheck/pass/as_pattern.sail @@ -0,0 +1,7 @@ + +val int -> int effect pure test + +function test ((int) _ as x) = +{ + x +} 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/atomcase.sail b/test/typecheck/pass/atomcase.sail new file mode 100644 index 00000000..18840867 --- /dev/null +++ b/test/typecheck/pass/atomcase.sail @@ -0,0 +1,18 @@ +default Order dec + +val extern forall Num 'n, Num 'm. (atom<'n>, atom<'m>) -> bool effect pure eq_atom +overload (deinfix ==) [eq_atom] + +val forall 'n, 'n in {8,16}. [:'n:] -> int effect pure test_fn +val forall 'n, 'n in {8,16}. [:'n:] -> int effect pure test_switch + +function test_fn 8 = 8 +and test_fn 16 = 16 + + +function test_switch n = + switch(n) { + case 8 -> 8 + case 16 -> 16 + } + 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..811b3a5b --- /dev/null +++ b/test/typecheck/pass/bv_simple_index.sail @@ -0,0 +1,11 @@ +val forall Nat 'n, Nat 'l, 'l >= 0. (vector<'n,'l,dec,bit>, [|'n - 'l + 1:'n|]) -> bit effect pure bitvector_access_dec +val forall Nat 'n, Nat 'l, 'l >= 0. (vector<'n,'l,inc,bit>, [|'n:'n + 'l - 1|]) -> bit effect pure bitvector_access_inc + +overload vector_access [bitvector_access_inc; bitvector_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..46bc19d6 --- /dev/null +++ b/test/typecheck/pass/bv_simple_index_bit.sail @@ -0,0 +1,9 @@ +val forall Nat 'n, Nat 'l, 'l >= 0. (vector<'n,'l,dec,bit>, [|'n - 'l + 1:'n|]) -> bit effect pure bitvector_access_dec +val forall Nat 'n, Nat 'l, 'l >= 0. (vector<'n,'l,inc,bit>, [|'n:'n + 'l - 1|]) -> bit effect pure bitvector_access_inc + +overload vector_access [bitvector_access_inc; bitvector_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..335e10ee --- /dev/null +++ b/test/typecheck/pass/case_simple_constraints.sail @@ -0,0 +1,18 @@ + +val extern forall Nat 'n, Nat 'm. ([:'n + 20:], [:'m:]) -> [:'n + 20 + 'm:] effect pure plus = "add" + +val extern forall Nat 'n, 'n <= -10. [:'n:] -> [:'n:] effect pure minus_ten_id = "id" + +val extern forall Nat 'n, 'n >= 10. [:'n:] -> [:'n:] effect pure ten_id = "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/cons_pattern_synonym.sail b/test/typecheck/pass/cons_pattern_synonym.sail new file mode 100644 index 00000000..f5b26294 --- /dev/null +++ b/test/typecheck/pass/cons_pattern_synonym.sail @@ -0,0 +1,7 @@ +typedef ty = list<(bit[8])> + +function bool foo ((ty) l) = + switch l { + case _ :: _ -> false + case _ -> true + }
\ No newline at end of file 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..8fc7c00e --- /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 = "add_vec" + +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/ex_cast.sail b/test/typecheck/pass/ex_cast.sail new file mode 100644 index 00000000..964bfa72 --- /dev/null +++ b/test/typecheck/pass/ex_cast.sail @@ -0,0 +1,12 @@ + +default Order dec + +val cast int -> exist 'n. [:'n:] effect pure ex_int + +val forall 'n. [:'n:] -> bit['n] effect pure zeros + +val int -> unit effect pure test + +function test n = { + x := zeros(n) +} diff --git a/test/typecheck/pass/exint.sail b/test/typecheck/pass/exint.sail new file mode 100644 index 00000000..1239fa44 --- /dev/null +++ b/test/typecheck/pass/exint.sail @@ -0,0 +1,22 @@ + +typedef Int = exist 'n. [:'n:] + +val forall 'n, 'm. ([:'n:], [:'m:]) -> exist 'o, 'o = 'n + 'm. [:'o:] effect pure add + +val forall 'n, 'm. ([:'n:], [:'m:]) -> exist 'o, 'o = 'n * 'm. [:'o:] effect pure mult + +overload (deinfix +) [add] + +overload (deinfix * ) [mult] + +let x = 3 + 4 + +let y = x + x * x + +let ([:7 * 8:]) z = y + +typedef Range = forall Num 'n, Num 'm, 'n <= 'm. exist 'o, 'n <= 'o & 'o <= 'm. [:'o:] + +let (Range<3,4>) a = 3 + +let (Range<2,5>) b = a + 1
\ No newline at end of file diff --git a/test/typecheck/pass/exist1.sail b/test/typecheck/pass/exist1.sail new file mode 100644 index 00000000..31968f36 --- /dev/null +++ b/test/typecheck/pass/exist1.sail @@ -0,0 +1,30 @@ + +let (exist 'n, 'n in {0, 1}. [:'n:]) v1 = 0 + +val bool -> exist 'n, 'n in {0, 1}. [:'n:] effect pure test + +function test flag = +{ + if flag then 0 else 1 +} + +let ([|0:1|]) v2 = test(true) + +val forall 'a, 'b. ([:'a:], [:'b:]) -> [:'a + 'b:] effect pure add + +let (exist 'k, 'k in {3, 4}. [:'k:]) v3 = 3 + +let (exist 'q, 'q in {0, 1}. [:'q + 3:]) v4 = v3 + +let v5 = add(test(true), 4) + +let ([:4:]) v6 = 4 + +function unit unit_fn (([:4:]) x) = () + +val forall 'a. ([:'a:], [:'a:]) -> [:'a + 'a:] effect pure s_add + +let (exist 'k, 'k = 4. [:'k:]) v7 = 4 + +let v8 = s_add(v7, 4) + diff --git a/test/typecheck/pass/exist2.sail b/test/typecheck/pass/exist2.sail new file mode 100644 index 00000000..04ccb57b --- /dev/null +++ b/test/typecheck/pass/exist2.sail @@ -0,0 +1,46 @@ + +let (exist 'n, 'n in {0, 1}. [:'n:]) v1 = 0 + +val bool -> exist 'n, 'n in {0, 1}. [:'n:] effect pure test + +function test flag = +{ + if flag then 0 else 1 +} + +let ([|0:1|]) v2 = test(true) + +val forall 'a, 'b. ([:'a:], [:'b:]) -> [:'a + 'b:] effect pure add + +let (exist 'k, 'k in {3, 4}. [:'k:]) v3 = 3 + +let (exist 'q, 'q in {0, 1}. [:'q + 3:]) v4 = v3 + +let v5 = add(test(true), 4) + +let ([:4:]) v6 = 4 + +function unit unit_fn (([:4:]) x) = () + +val forall 'a. ([:'a:], [:'a:]) -> [:'a + 'a:] effect pure s_add + +let (exist 'k, 'k = 4. [:'k:]) v7 = 4 + +(* let v8 = s_add(test(true), 4) *) + +let (exist 'n, 0 = 0. [:'n:]) v9 = 100 + +let (int) v10 = v9 + +typedef Int = exist 'n, 0 = 0. [:'n:] + +val int -> Int effect pure existential_int +val forall 'n, 'm. range<'n,'m> -> exist 'e, 'n <= 'e & 'e <= 'm. [:'e:] effect pure existential_range + +overload existential [existential_int; existential_range] + +let (exist 'n, 0 = 0. [:'n:]) v11 = existential(v10) + +let (exist 'e, 0 <= 'e & 'e <= 3. [:'e:]) v12 = existential(([|0:3|]) 2) + +let (Int) v13 = existential(v10) diff --git a/test/typecheck/pass/exist_pattern.sail b/test/typecheck/pass/exist_pattern.sail new file mode 100644 index 00000000..4561074a --- /dev/null +++ b/test/typecheck/pass/exist_pattern.sail @@ -0,0 +1,42 @@ +default Order inc + +register nat n +register nat x +register nat y + +val (int, int) -> bool effect pure eq_int + +overload (deinfix ==) [eq_int] + +typedef wordsize = exist 'n, 'n IN {8,16,32}. [|'n|] +let (wordsize) word = ([|8|]) 8 + +function nat main () = { + + (* works - x and y are set to 42 *) + n := 1; + y := + (switch n { + case 0 -> { x := 21; x } + case 1 -> { x := 42; x } + case z -> { x := 99; x } + }); + + switch word { + case ([|8|]) 8 -> { x:= 32; } + case ([|16|]) 16 -> { x:= 64; } + case ([|32|]) 32 -> { x:= 128; } + }; + + switch 0b010101 { + case (0b01:(bit[1]) _:0b101) -> n:= 42 + case _ -> n:=0 + }; + + n := 3; + switch n { + case 0 -> { 21 } + case 1 -> { 42 } + case u -> { 99 } + }; +} diff --git a/test/typecheck/pass/exist_simple.sail b/test/typecheck/pass/exist_simple.sail new file mode 100644 index 00000000..87e62b13 --- /dev/null +++ b/test/typecheck/pass/exist_simple.sail @@ -0,0 +1,15 @@ + +register bool reg + +let (exist 'n, 0 <= 'n & 'n <= 4. [:'n:]) A = 4 + +let ([|0:4|]) B = A + +val unit -> exist 'n, 'n in {0, 1}. [:'n:] effect {rreg} test + +function test () = +{ + if reg + then 0 + else 1 +} diff --git a/test/typecheck/pass/exist_subrange.sail b/test/typecheck/pass/exist_subrange.sail new file mode 100644 index 00000000..de867b75 --- /dev/null +++ b/test/typecheck/pass/exist_subrange.sail @@ -0,0 +1,12 @@ +default Order dec + +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 + +function unit test ((bit[6]) xs) = +{ + (int) len := 4; + (exist 'n. [:'n:]) len := 5; + ys := xs[len .. 0]; + () +} diff --git a/test/typecheck/pass/exist_tlb.sail b/test/typecheck/pass/exist_tlb.sail new file mode 100644 index 00000000..525d29c6 --- /dev/null +++ b/test/typecheck/pass/exist_tlb.sail @@ -0,0 +1,94 @@ + +(* Minimal prelude *) + +val forall Num 'n, Num 'm, Num 'o, Num 'p, Order 'ord. + vector<'o, 'n, 'ord, bit> -> vector<'p, 'm, 'ord, bit> effect pure extz + +val forall Num 'n, Num 'm, Num 'o, Num 'p, Order 'ord. + vector<'o, 'n, 'ord, bit> -> vector<'p, 'm, 'ord, bit> effect pure exts + +overload EXTZ [extz] +overload EXTS [exts] + +val forall Num 'n, Num 'o, Order 'ord. + (vector<'o, 'n, 'ord, bit>, vector<'o, 'n, 'ord, bit>) -> vector<'o, 'n, 'ord, bit> effect pure add_vec + +overload (deinfix +) [add_vec] + +val bool -> bool effect pure bool_not +overload ~ [bool_not] + +(* MIPS spec subset *) + +default Order dec + +register (bit[1]) CP0LLBit +register (bit[64]) CP0LLAddr + +typedef MemAccessType = enumerate {Instruction; LoadData; StoreData} + +typedef regno = bit[5] (* a register number *) +typedef imm16 = bit[16] (* 16-bit immediate *) + +typedef Exception = enumerate +{ + Int; TLBMod; TLBL; TLBS; AdEL; AdES; Sys; Bp; ResI; CpU; Ov; Tr; C2E; C2Trap; + XTLBRefillL; XTLBRefillS; XTLBInvL; XTLBInvS; MCheck +} + +typedef WordType = enumerate {B; H; W; D} + +val bit[5] -> bit[64] effect {rreg} rGPR +val (bit[64], WordType) -> bool effect pure isAddressAligned +val forall Type 'o. (Exception, bit[64]) -> 'o effect pure SignalExceptionBadAddr + +val WordType -> exist 'r, 'r in {1,2,4,8}. [:'r:] effect pure wordWidthBytes + +function wordWidthBytes w = switch w { + case B -> 1 + case H -> 2 + case W -> 4 + case D -> 8 +} + +val forall Nat 'n. (bit[64], [:'n:]) -> bit[8 * 'n] effect {rmem} MEMr_reserve_wrapper +val forall Nat 'n. (bit[64], [:'n:]) -> bit[8 * 'n] effect {rmem} MEMr_wrapper +val (bit[5], bit[64]) -> unit effect {wreg} wGPR + +function bit[64] addrWrapper((bit[64]) addr, (MemAccessType) accessType, (WordType) width) = addr + +function (bit[64]) TLBTranslate ((bit[64]) vAddr, (MemAccessType) accessType) = vAddr + +scattered typedef ast = const union + +val ast -> unit effect {rmem, rreg, wreg} execute + +scattered function unit execute + +union ast member (WordType, bool, bool, regno, regno, imm16) Load + +function clause execute (Load(width, signed, linked, base, rt, offset)) = + { + (bit[64]) vAddr := addrWrapper(EXTS(offset) + rGPR(base), LoadData, width); + if ~ (isAddressAligned(vAddr, width)) then + (SignalExceptionBadAddr(AdEL, vAddr)) (* unaligned access *) + else + let pAddr = (TLBTranslate(vAddr, LoadData)) in + { + (exist 't, 't in {1,2,4,8}. bit[8 * 't]) memResult := if linked then + { + CP0LLBit := 0b1; + CP0LLAddr := pAddr; + MEMr_reserve_wrapper(pAddr, wordWidthBytes(width)); + } + else + MEMr_wrapper(pAddr, wordWidthBytes(width)); + if (signed) then + wGPR(rt) := EXTS(memResult) + else + wGPR(rt) := EXTZ(memResult) + } + } + +end ast +end execute diff --git a/test/typecheck/pass/exist_true.sail b/test/typecheck/pass/exist_true.sail new file mode 100644 index 00000000..a30fb87b --- /dev/null +++ b/test/typecheck/pass/exist_true.sail @@ -0,0 +1,7 @@ + +function unit test () = +{ + (exist 'n. [:'n:]) x := 4; + (exist 'n, true. [:'n:]) y := 5; + () +} 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..ddeefd53 --- /dev/null +++ b/test/typecheck/pass/flow_gt1.sail @@ -0,0 +1,28 @@ +default Order inc + +val extern forall Num 'n, Num 'm, Num 'o, Num 'p. ([|'n:'m|], [|'o:'p|]) -> [|'n+'o:'m+'p|] effect pure add_range = "add" + +val extern forall Num 'n, Num 'm, Num 'o, Num 'p. ([|'n:'m|], [|'o:'p|]) -> [|'n-'p:'m-'o|] effect pure sub_range = "sub" + +val extern forall Num 'n, Num 'm, Num 'o. ([|'n:'m|], [:'o:]) -> bool effect pure lt_range_atom = "lt" +val extern forall Num 'n, Num 'm, Num 'o. ([|'n:'m|], [:'o:]) -> bool effect pure lteq_range_atom = "lteq" +val extern forall Num 'n, Num 'm, Num 'o. ([|'n:'m|], [:'o:]) -> bool effect pure gt_range_atom = "gt" +val extern forall Num 'n, Num 'm, Num 'o. ([|'n:'m|], [:'o:]) -> bool effect pure gteq_range_atom = "gteq" +val extern forall Num 'n, Num 'm, Num 'o. ([:'n:], [|'m:'o|]) -> bool effect pure lt_atom_range = "lt" +val extern forall Num 'n, Num 'm, Num 'o. ([:'n:], [|'m:'o|]) -> bool effect pure lteq_atom_range = "lteq" +val extern forall Num 'n, Num 'm, Num 'o. ([:'n:], [|'m:'o|]) -> bool effect pure gt_atom_range = "gt" +val extern forall Num 'n, Num 'm, Num 'o. ([:'n:], [|'m:'o|]) -> bool effect pure gteq_atom_range = "gteq" + +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..47f7aa0f --- /dev/null +++ b/test/typecheck/pass/flow_gteq1.sail @@ -0,0 +1,28 @@ +default Order inc + +val extern forall Num 'n, Num 'm, Num 'o, Num 'p. ([|'n:'m|], [|'o:'p|]) -> [|'n+'o:'m+'p|] effect pure add_range = "add" + +val extern forall Num 'n, Num 'm, Num 'o, Num 'p. ([|'n:'m|], [|'o:'p|]) -> [|'n-'p:'m-'o|] effect pure sub_range = "sub" + +val extern forall Num 'n, Num 'm, Num 'o. ([|'n:'m|], [:'o:]) -> bool effect pure lt_range_atom = "lt" +val extern forall Num 'n, Num 'm, Num 'o. ([|'n:'m|], [:'o:]) -> bool effect pure lteq_range_atom = "lteq" +val extern forall Num 'n, Num 'm, Num 'o. ([|'n:'m|], [:'o:]) -> bool effect pure gt_range_atom = "gt" +val extern forall Num 'n, Num 'm, Num 'o. ([|'n:'m|], [:'o:]) -> bool effect pure gteq_range_atom = "gteq" +val extern forall Num 'n, Num 'm, Num 'o. ([:'n:], [|'m:'o|]) -> bool effect pure lt_atom_range = "lt" +val extern forall Num 'n, Num 'm, Num 'o. ([:'n:], [|'m:'o|]) -> bool effect pure lteq_atom_range = "lteq" +val extern forall Num 'n, Num 'm, Num 'o. ([:'n:], [|'m:'o|]) -> bool effect pure gt_atom_range = "gt" +val extern forall Num 'n, Num 'm, Num 'o. ([:'n:], [|'m:'o|]) -> bool effect pure gteq_atom_range = "gteq" + +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..c210ed7a --- /dev/null +++ b/test/typecheck/pass/flow_lt1.sail @@ -0,0 +1,25 @@ +default Order inc + +val extern forall Num 'n, Num 'm, Num 'o, Num 'p. ([|'n:'m|], [|'o:'p|]) -> [|'n+'o:'m+'p|] effect pure add_range = "add" + +val extern forall Num 'n, Num 'm, Num 'o, Num 'p. ([|'n:'m|], [|'o:'p|]) -> [|'n-'p:'m-'o|] effect pure sub_range = "sub" + +val extern forall Num 'n, Num 'm, Num 'o. ([|'n:'m|], [:'o:]) -> bool effect pure lt_range_atom = "lt" +val extern forall Num 'n, Num 'm, Num 'o. ([|'n:'m|], [:'o:]) -> bool effect pure lteq_range_atom = "lteq" +val extern forall Num 'n, Num 'm, Num 'o. ([|'n:'m|], [:'o:]) -> bool effect pure gt_range_atom = "gt" +val extern forall Num 'n, Num 'm, Num 'o. ([|'n:'m|], [:'o:]) -> bool effect pure gteq_range_atom = "gteq" +val extern forall Num 'n, Num 'm, Num 'o. ([:'n:], [|'m:'o|]) -> bool effect pure lt_atom_range = "lt" +val extern forall Num 'n, Num 'm, Num 'o. ([:'n:], [|'m:'o|]) -> bool effect pure lteq_atom_range = "lteq" +val extern forall Num 'n, Num 'm, Num 'o. ([:'n:], [|'m:'o|]) -> bool effect pure gt_atom_range = "gt" +val extern forall Num 'n, Num 'm, Num 'o. ([:'n:], [|'m:'o|]) -> bool effect pure gteq_atom_range = "gteq" + +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..cccebaa3 --- /dev/null +++ b/test/typecheck/pass/flow_lt2.sail @@ -0,0 +1,25 @@ +default Order inc + +val extern forall Num 'n, Num 'm, Num 'o, Num 'p. ([|'n:'m|], [|'o:'p|]) -> [|'n+'o:'m+'p|] effect pure add_range = "add" + +val extern forall Num 'n, Num 'm, Num 'o, Num 'p. ([|'n:'m|], [|'o:'p|]) -> [|'n-'p:'m-'o|] effect pure sub_range = "sub" + +val extern forall Num 'n, Num 'm, Num 'o. ([|'n:'m|], [:'o:]) -> bool effect pure lt_range_atom = "lt" +val extern forall Num 'n, Num 'm, Num 'o. ([|'n:'m|], [:'o:]) -> bool effect pure lteq_range_atom = "lteq" +val extern forall Num 'n, Num 'm, Num 'o. ([|'n:'m|], [:'o:]) -> bool effect pure gt_range_atom = "gt" +val extern forall Num 'n, Num 'm, Num 'o. ([|'n:'m|], [:'o:]) -> bool effect pure gteq_range_atom = "gteq" +val extern forall Num 'n, Num 'm, Num 'o. ([:'n:], [|'m:'o|]) -> bool effect pure lt_atom_range = "lt" +val extern forall Num 'n, Num 'm, Num 'o. ([:'n:], [|'m:'o|]) -> bool effect pure lteq_atom_range = "lteq" +val extern forall Num 'n, Num 'm, Num 'o. ([:'n:], [|'m:'o|]) -> bool effect pure gt_atom_range = "gt" +val extern forall Num 'n, Num 'm, Num 'o. ([:'n:], [|'m:'o|]) -> bool effect pure gteq_atom_range = "gteq" + +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..9601f48f --- /dev/null +++ b/test/typecheck/pass/flow_lt_assign.sail @@ -0,0 +1,29 @@ +default Order inc + +val extern forall Num 'n, Num 'm, Num 'o, Num 'p. ([|'n:'m|], [|'o:'p|]) -> [|'n+'o:'m+'p|] effect pure add_range = "add" + +val extern forall Num 'n, Num 'm, Num 'o, Num 'p. ([|'n:'m|], [|'o:'p|]) -> [|'n-'p:'m-'o|] effect pure sub_range = "sub" + +val extern forall Num 'n, Num 'm, Num 'o. ([|'n:'m|], [:'o:]) -> bool effect pure lt_range_atom = "lt" +val extern forall Num 'n, Num 'm, Num 'o. ([|'n:'m|], [:'o:]) -> bool effect pure lteq_range_atom = "lteq" +val extern forall Num 'n, Num 'm, Num 'o. ([|'n:'m|], [:'o:]) -> bool effect pure gt_range_atom = "gt" +val extern forall Num 'n, Num 'm, Num 'o. ([|'n:'m|], [:'o:]) -> bool effect pure gteq_range_atom = "gteq" +val extern forall Num 'n, Num 'm, Num 'o. ([:'n:], [|'m:'o|]) -> bool effect pure lt_atom_range = "lt" +val extern forall Num 'n, Num 'm, Num 'o. ([:'n:], [|'m:'o|]) -> bool effect pure lteq_atom_range = "lteq" +val extern forall Num 'n, Num 'm, Num 'o. ([:'n:], [|'m:'o|]) -> bool effect pure gt_atom_range = "gt" +val extern forall Num 'n, Num 'm, Num 'o. ([:'n:], [|'m:'o|]) -> bool effect pure gteq_atom_range = "gteq" + +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..ffa4dd8b --- /dev/null +++ b/test/typecheck/pass/flow_lteq1.sail @@ -0,0 +1,28 @@ +default Order inc + +val extern forall Num 'n, Num 'm, Num 'o, Num 'p. ([|'n:'m|], [|'o:'p|]) -> [|'n+'o:'m+'p|] effect pure add_range = "add" + +val extern forall Num 'n, Num 'm, Num 'o, Num 'p. ([|'n:'m|], [|'o:'p|]) -> [|'n-'p:'m-'o|] effect pure sub_range = "sub" + +val extern forall Num 'n, Num 'm, Num 'o. ([|'n:'m|], [:'o:]) -> bool effect pure lt_range_atom = "lt" +val extern forall Num 'n, Num 'm, Num 'o. ([|'n:'m|], [:'o:]) -> bool effect pure lteq_range_atom = "lteq" +val extern forall Num 'n, Num 'm, Num 'o. ([|'n:'m|], [:'o:]) -> bool effect pure gt_range_atom = "gt" +val extern forall Num 'n, Num 'm, Num 'o. ([|'n:'m|], [:'o:]) -> bool effect pure gteq_range_atom = "gteq" +val extern forall Num 'n, Num 'm, Num 'o. ([:'n:], [|'m:'o|]) -> bool effect pure lt_atom_range = "lt" +val extern forall Num 'n, Num 'm, Num 'o. ([:'n:], [|'m:'o|]) -> bool effect pure lteq_atom_range = "lteq" +val extern forall Num 'n, Num 'm, Num 'o. ([:'n:], [|'m:'o|]) -> bool effect pure gt_atom_range = "gt" +val extern forall Num 'n, Num 'm, Num 'o. ([:'n:], [|'m:'o|]) -> bool effect pure gteq_atom_range = "gteq" + +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/foreach_var_updates.sail b/test/typecheck/pass/foreach_var_updates.sail new file mode 100644 index 00000000..e3e30ce6 --- /dev/null +++ b/test/typecheck/pass/foreach_var_updates.sail @@ -0,0 +1,15 @@ +val extern (int, int) -> int effect pure add_int = "add" +overload (deinfix +) [ add_int ] + +val extern (int, int) -> int effect pure sub_int = "sub" +overload (deinfix -) [ sub_int ] + +function (int) foo ((int) w) = { + (int) x := w; + (int) y := w; + foreach (z from 0 to 10) { + x := x + z; + y := y - z; + }; + x + y; +} 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/let_subtyp_bug.sail b/test/typecheck/pass/let_subtyp_bug.sail new file mode 100644 index 00000000..e2abde2d --- /dev/null +++ b/test/typecheck/pass/let_subtyp_bug.sail @@ -0,0 +1,9 @@ +let ([|5|]) y = 2 + +val unit -> nat effect pure test + +function test() = { + let ([|5|]) x = 2 in + x +} +
\ No newline at end of file diff --git a/test/typecheck/pass/lexp_memory.sail b/test/typecheck/pass/lexp_memory.sail new file mode 100644 index 00000000..321fb315 --- /dev/null +++ b/test/typecheck/pass/lexp_memory.sail @@ -0,0 +1,68 @@ +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 extern forall Num 'l, Num 'm. ([:'l:], [:'m:], int) -> vector<'l,'m,dec,bit> effect pure to_vec_dec + +val cast forall Nat 'n, Nat 'l. [|0:1|] -> vector<'n,'l,dec,bit> effect pure cast_01_vec +function forall Num 'n, Num 'l. (vector<'n,'l,dec,bit>) cast_01_vec i = to_vec_dec (sizeof 'n, sizeof 'l, i) +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/list_cons.sail b/test/typecheck/pass/list_cons.sail new file mode 100644 index 00000000..6f103bf6 --- /dev/null +++ b/test/typecheck/pass/list_cons.sail @@ -0,0 +1 @@ +function list<int> foo ((int) i, (list<int>) l) = i :: l diff --git a/test/typecheck/pass/list_cons2.sail b/test/typecheck/pass/list_cons2.sail new file mode 100644 index 00000000..8c34282b --- /dev/null +++ b/test/typecheck/pass/list_cons2.sail @@ -0,0 +1,7 @@ +function list<int> foo ((int) i, (list<int>) l) = i :: l + +function list<int> bar () = [||||] + +function list<int> baz ((list<int>) l) = l + +function list<int> quux () = baz ([||||]) diff --git a/test/typecheck/pass/list_lit.sail b/test/typecheck/pass/list_lit.sail new file mode 100644 index 00000000..d4febadf --- /dev/null +++ b/test/typecheck/pass/list_lit.sail @@ -0,0 +1,2 @@ + +let (list<int>) xs = [||1,2,3,4,5,6||] diff --git a/test/typecheck/pass/mips400.sail b/test/typecheck/pass/mips400.sail new file mode 100644 index 00000000..951f5126 --- /dev/null +++ b/test/typecheck/pass/mips400.sail @@ -0,0 +1,785 @@ +(* New typechecker prelude *) + +val cast forall Num 'n, Num 'm, Order 'ord. vector<'n,'m,'ord,bit> -> [|0:2**'m - 1|] effect pure unsigned + +val forall Num 'n, Num 'm, Order 'ord. vector<'n,'m,'ord,bit> -> [|0 - (2**('m - 1)):2**('m - 1) - 1|] effect pure signed + +val extern forall Num 'n, Num 'm. [|0:'n|] -> vector<'m - 1,'m,dec,bit> effect pure to_vec = "to_vec_dec" + +val extern forall Num 'm. int -> vector<'m - 1,'m,dec,bit> effect pure to_svec = "to_vec_dec" + +(* 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 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 Num 'n, Num 'l, Type 'a, 'l >= 0. (vector<'n,'l,inc,'a>, [|'n:'n + 'l - 1|]) -> 'a effect pure vector_access_inc +val forall Num 'n, Num 'l, 'l >= 0. (vector<'n,'l,dec,bit>, [|'n - 'l + 1:'n|]) -> bit effect pure bitvector_access_dec +val forall Num 'n, Num 'l, 'l >= 0. (vector<'n,'l,inc,bit>, [|'n:'n + 'l - 1|]) -> bit effect pure bitvector_access_inc + +overload vector_access [bitvector_access_inc; bitvector_access_dec; vector_access_inc; vector_access_dec] + +(* Type safe vector subrange *) +(* vector_subrange(v, m, o) returns the subvector of v with elements with + indices from m up to and *including* o. *) +val forall Num 'n, Num 'l, Num 'm, Num 'o, Type 'a, 'l >= 0, 'm <= 'o, 'o <= 'l. + (vector<'n,'l,inc,'a>, [:'m:], [:'o:]) -> vector<'m,('o - 'm) + 1,inc,'a> effect pure vector_subrange_inc + +val forall Num 'n, Num 'l, Num 'm, Num '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 + +val forall Num 'n, Num 'l, Order 'ord. + (vector<'n,'l,'ord,bit>, int, int) -> list<bit> effect pure vector_subrange_bl + +val forall Num 'n, Num 'l, Num 'm, Num 'o, 'l >= 0, 'm <= 'o, 'o <= 'l. + (vector<'n,'l,inc,bit>, [:'m:], [:'o:]) -> vector<'m,('o - 'm) + 1,inc,bit> effect pure bitvector_subrange_inc + +val forall Num 'n, Num 'l, Num 'm, Num 'o, 'n >= 'm, 'm >= 'o, 'o >= 'n - 'l + 1. + (vector<'n,'l,dec,bit>, [:'m:], [:'o:]) -> vector<'m,('m - 'o) + 1,dec,bit> effect pure bitvector_subrange_dec + +overload vector_subrange [bitvector_subrange_inc; bitvector_subrange_dec; vector_subrange_inc; vector_subrange_dec; vector_subrange_bl] + +(* Type safe vector append *) +val extern forall Num 'n1, Num 'l1, Num 'n2, Num 'l2, Order 'o, Type 'a, 'l1 >= 0, 'l2 >= 0. + (vector<'n1,'l1,'o,'a>, vector<'n2,'l2,'o,'a>) -> vector<'l1 + 'l2 - 1,'l1 + 'l2,'o,'a> effect pure vec_append = "vector_concat" + +val (list<bit>, list<bit>) -> list<bit> effect pure list_append + +val extern forall Num 'n1, Num 'l1, Num 'n2, Num 'l2, Order 'o, 'l1 >= 0, 'l2 >= 0. + (vector<'n1,'l1,'o,bit>, vector<'n2,'l2,'o,bit>) -> vector<'l1 + 'l2 - 1,'l1 + 'l2,'o,bit> effect pure bitvec_append = "bitvector_concat" + +overload vector_append [bitvec_append; vec_append; list_append] + +(* Implicit register dereferencing *) +val cast forall Type 'a. register<'a> -> 'a effect {rreg} reg_deref + +(* Bitvector duplication *) +val forall Num 'n. (bit, [:'n:]) -> vector<'n - 1,'n,dec,bit> effect pure duplicate + +val (bit, int) -> list<bit> effect pure duplicate_to_list + +val forall Num 'n, Num 'm, Num 'o, Order 'ord. + (vector<'o,'n,'ord,bit>, [:'m:]) -> vector<'o,'m*'n,'ord,bit> effect pure duplicate_bits + +val forall Num 'n, Num 'o, Order 'ord. + (vector<'o,'n,'ord,bit>, int) -> list<bit> effect pure duplicate_bits_to_list + +overload (deinfix ^^) [duplicate; duplicate_bits; duplicate_to_list; duplicate_bits_to_list] + +(* Bitvector extension *) +val forall Num 'n, Num 'm, Num 'o, Num 'p, Order 'ord. + vector<'o, 'n, 'ord, bit> -> vector<'p, 'm, 'ord, bit> effect pure extz + +val forall Num 'm, Num 'p, Order 'ord. + list<bit> -> vector<'p, 'm, 'ord, bit> effect pure extz_bl + +val forall Num 'n, Num 'm, Num 'o, Num 'p, Order 'ord. + vector<'o, 'n, 'ord, bit> -> vector<'p, 'm, 'ord, bit> effect pure exts + +val forall Num 'm, Num 'p, Order 'ord. + list<bit> -> vector<'p, 'm, 'ord, bit> effect pure exts_bl + +(* If we want an automatic bitvector extension, then this is the function to + use, but I've disabled the cast because it hides signedness bugs. *) +val (*cast*) forall Num 'n, Num 'm, Num 'o, Num 'p, Order 'ord, 'm >= 'n. + vector<'o, 'n, 'ord, bit> -> vector<'p, 'm, 'ord, bit> effect pure extzi + +overload EXTZ [extz; extz_bl] +overload EXTS [exts; exts_bl] + +val forall Type 'a, Num 'n, Num 'm, Num 'o, Num '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 Num 'n, Num 'm, 'n >= 'm - 1. + vector<'n,'m,dec,bit> -> vector<'m - 1,'m,dec,bit> + effect pure norm_dec + +val cast forall Num 'n, Num 'm, Num '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 Num 'n, Num 'l, Order 'ord. [:0:] -> vector<'n,'l,'ord,bit> effect pure cast_0_vec +val cast forall Num 'n, Num 'l, Order 'ord. [:1:] -> vector<'n,'l,'ord,bit> effect pure cast_1_vec +val cast forall Num 'n, Num 'l, Order 'ord. [|0:1|] -> vector<'n,'l,'ord,bit> effect pure cast_01_vec + +val cast forall Num 'n, Order 'ord. vector<'n,1,'ord,bit> -> bool effect pure cast_vec_bool +val cast bit -> bool effect pure cast_bit_bool + +val cast forall Num 'n, Num 'm, 'n >= 'm - 1, 'm >= 1. bit -> vector<'n,'m,dec,bit> effect pure cast_bit_vec + +(* MSB *) +val forall Num 'n, Num 'm, Order 'ord. vector<'n, 'm, 'ord, bit> -> bit effect pure most_significant + +(* Arithmetic *) + +val extern forall Num 'n, Num 'm, Num 'o, Num 'p. + ([|'n:'m|], [|'o:'p|]) -> [|'n + 'o:'m + 'p|] effect pure add + +val extern (nat, nat) -> nat effect pure add_nat = "add" + +val extern (int, int) -> int effect pure add_int = "add" + +val forall Num 'n, Num 'o, Order 'ord. + (vector<'o, 'n, 'ord, bit>, vector<'o, 'n, 'ord, bit>) -> vector<'o, 'n, 'ord, bit> effect pure add_vec + +val forall Num 'n, Num 'o, Order 'ord. + (vector<'o, 'n, 'ord, bit>, int) -> vector<'o, 'n, 'ord, bit> effect pure add_vec_int + +val forall Num 'n, Num 'o, Order 'ord. + (vector<'o, 'n, 'ord, bit>, vector<'o, 'n, 'ord, bit>) -> (vector<'o, 'n, 'ord, bit>, bit, bit) effect pure add_overflow_vec + +val extern forall Num 'n, Num 'm, Num 'o, Num 'p. + ([|'n:'m|], [|'o:'p|]) -> [|'n - 'p:'m - 'o|] effect pure sub + +val extern (int, int) -> int effect pure sub_int = "sub" + +val forall Num 'n, Num 'm, Order 'ord. + (vector<'n,'m,'ord,bit>, int) -> vector<'n,'m,'ord,bit> effect pure sub_vec_int + +val forall Num 'n, Num 'o, Order 'ord. + (vector<'o, 'n, 'ord, bit>, vector<'o, 'n, 'ord, bit>) -> vector<'o, 'n, 'ord, bit> effect pure sub_vec + +val forall Num 'n, Num 'o, Order 'ord. + (vector<'o, 'n, 'ord, bit>, vector<'o, 'n, 'ord, bit>) -> (vector<'o, 'n, 'ord, bit>, bit, bit) effect pure sub_underflow_vec + +overload (deinfix +) [ + add_vec; + add_overflow_vec; + add_vec_int; + add; + add_nat; + add_int +] + +overload (deinfix -) [ + sub_vec_int; + sub_vec; + sub_underflow_vec; + sub; + sub_int +] + +val extern bool -> bit effect pure bool_to_bit = "bool_to_bitU" + +val (int, int) -> int effect pure mul_int +val forall Num 'n, Num 'o, Order 'ord. + (vector<'o, 'n, 'ord, bit>, vector<'o, 'n, 'ord, bit>) -> vector<2 * 'n - 1, 2 * 'n, 'ord, bit> effect pure mul_vec + +overload (deinfix * ) [ + mul_vec; + mul_int +] + +val forall Num 'n, Num 'o, Order 'ord. + (vector<'o, 'n, 'ord, bit>, vector<'o, 'n, 'ord, bit>) -> vector<2 * 'n - 1, 2 * 'n, 'ord, bit> effect pure mul_svec + +overload (deinfix *_s) [ + mul_svec +] + +val extern (bool, bool) -> bool effect pure bool_xor + +val extern forall Num 'n, Num 'o, Order 'ord. + (vector<'o, 'n, 'ord, bit>, vector<'o, 'n, 'ord, bit>) -> vector<'o, 'n, 'ord, bit> effect pure xor_vec = "bitwise_xor" + +overload (deinfix ^) [ + bool_xor; + xor_vec +] + +val forall Num 'n, Num 'o, Order 'ord. + (vector<'o, 'n, 'ord, bit>, int) -> vector<'o, 'n, 'ord, bit> effect pure shiftl + +overload (deinfix <<) [ + shiftl +] + +val forall Num 'n, Num 'o, Order 'ord. + (vector<'o, 'n, 'ord, bit>, int) -> vector<'o, 'n, 'ord, bit> effect pure shiftr + +overload (deinfix >>) [ + shiftr +] + +(* Boolean operators *) +val extern bool -> bool effect pure bool_not = "not" +val (bool, bool) -> bool effect pure bool_or +val (bool, bool) -> bool effect pure bool_and + +val forall Num 'n, Num 'm, Order 'ord. + vector<'n,'m,'ord,bit> -> vector<'n,'m,'ord,bit> effect pure bitwise_not + +val forall Num 'n, Num 'm, Order 'ord. + (vector<'n,'m,'ord,bit>, vector<'n,'m,'ord,bit>) -> vector<'n,'m,'ord,bit> effect pure bitwise_and + +val forall Num 'n, Num 'm, Order 'ord. + (vector<'n,'m,'ord,bit>, vector<'n,'m,'ord,bit>) -> vector<'n,'m,'ord,bit> effect pure bitwise_or + +overload ~ [bool_not; bitwise_not] +overload (deinfix &) [bool_and; bitwise_and] +overload (deinfix |) [bool_or; bitwise_or] + +(* Equality *) + +val forall Num 'n, Num 'm, Order 'ord. (vector<'n,'m,'ord,bit>, vector<'n,'m,'ord,bit>) -> bool effect pure eq_vec + +val forall Type 'a. ('a, 'a) -> bool effect pure eq + +val forall Num 'n, Num 'm, Order 'ord. (vector<'n,'m,'ord,bit>, vector<'n,'m,'ord,bit>) -> bool effect pure neq_vec + +val forall Type 'a. ('a, 'a) -> bool effect pure neq + +function forall Num 'n, Num 'm, Order 'ord. bool neq_vec (v1, v2) = bool_not(eq_vec(v1, v2)) + +overload (deinfix ==) [eq_vec; eq] +overload (deinfix !=) [neq_vec; neq] + +val forall Num 'n, Num 'm, Order 'ord. (vector<'n,'m,'ord,bit>, vector<'n,'m,'ord,bit>) -> bool effect pure gteq_vec +val forall Num 'n, Num 'm, Order 'ord. (vector<'n,'m,'ord,bit>, vector<'n,'m,'ord,bit>) -> bool effect pure gt_vec +val forall Num 'n, Num 'm, Order 'ord. (vector<'n,'m,'ord,bit>, vector<'n,'m,'ord,bit>) -> bool effect pure lteq_vec +val forall Num 'n, Num 'm, Order 'ord. (vector<'n,'m,'ord,bit>, vector<'n,'m,'ord,bit>) -> bool effect pure lt_vec + +val extern (int, int) -> bool effect pure gteq_int = "gteq" +val extern (int, int) -> bool effect pure gt_int = "gt" +val extern (int, int) -> bool effect pure lteq_int = "lteq" +val extern (int, int) -> bool effect pure lt_int = "lt" + +val extern forall Num 'n, Num 'm, Num 'o. ([|'n:'m|], [:'o:]) -> bool effect pure lt_range_atom = "lt" +val extern forall Num 'n, Num 'm, Num 'o. ([|'n:'m|], [:'o:]) -> bool effect pure lteq_range_atom = "lteq" +val extern forall Num 'n, Num 'm, Num 'o. ([|'n:'m|], [:'o:]) -> bool effect pure gt_range_atom = "gt" +val extern forall Num 'n, Num 'm, Num 'o. ([|'n:'m|], [:'o:]) -> bool effect pure gteq_range_atom = "gteq" +val extern forall Num 'n, Num 'm, Num 'o. ([:'n:], [|'m:'o|]) -> bool effect pure lt_atom_range = "lt" +val extern forall Num 'n, Num 'm, Num 'o. ([:'n:], [|'m:'o|]) -> bool effect pure lteq_atom_range = "lteq" +val extern forall Num 'n, Num 'm, Num 'o. ([:'n:], [|'m:'o|]) -> bool effect pure gt_atom_range = "gt" +val extern forall Num 'n, Num 'm, Num 'o. ([:'n:], [|'m:'o|]) -> bool effect pure gteq_atom_range = "gteq" + +val extern forall Num 'n, Num 'm. ([:'n:], [:'m:]) -> bool effect pure lteq_atom_atom = "lteq" +val extern forall Num 'n, Num 'm. ([:'n:], [:'m:]) -> bool effect pure gteq_atom_atom = "gteq" +val extern forall Num 'n, Num 'm. ([:'n:], [:'m:]) -> bool effect pure lt_atom_atom = "lt" +val extern forall Num 'n, Num 'm. ([:'n:], [:'m:]) -> bool effect pure gt_atom_atom = "gt" + +overload (deinfix >=) [gteq_atom_atom; gteq_range_atom; gteq_atom_range; gteq_vec; gteq_int] +overload (deinfix >) [gt_atom_atom; gt_vec; gt_int] +overload (deinfix <=) [lteq_atom_atom; lteq_range_atom; lteq_atom_range; lteq_vec; lteq_int] +overload (deinfix <) [lt_atom_atom; lt_vec; lt_int] + +val forall Num 'n, Num 'm, Order 'ord. (vector<'n,'m,'ord,bit>, vector<'n,'m,'ord,bit>) -> bool effect pure gteq_svec +val forall Num 'n, Num 'm, Order 'ord. (vector<'n,'m,'ord,bit>, vector<'n,'m,'ord,bit>) -> bool effect pure gt_svec +val forall Num 'n, Num 'm, Order 'ord. (vector<'n,'m,'ord,bit>, vector<'n,'m,'ord,bit>) -> bool effect pure lteq_svec +val forall Num 'n, Num 'm, Order 'ord. (vector<'n,'m,'ord,bit>, vector<'n,'m,'ord,bit>) -> bool effect pure lt_svec + +overload (deinfix <_s) [lt_svec] +overload (deinfix <=_s) [lteq_svec] +overload (deinfix >_s) [gt_svec] +overload (deinfix >=_s) [gteq_svec] + +val (int, int) -> int effect pure quotient + +overload (deinfix quot) [quotient] + +val (int, int) -> int effect pure modulo + +overload (deinfix mod) [modulo] + +val extern forall Num 'n, Num 'm, Order 'ord, Type 'a. vector<'n,'m,'ord,'a> -> [:'m:] effect pure vec_length = "length" +val forall Type 'a. list<'a> -> nat effect pure list_length + +val extern forall Num 'n, Num 'm, Order 'ord. vector<'n,'m,'ord,bit> -> [:'m:] effect pure bitvector_length = "bvlength" + +overload length [bitvector_length; vector_length; list_length] + +val cast forall Num 'n. [:'n:] -> [|'n|] effect pure upper + +typedef option = const union forall Type 'a. { + None; + 'a Some +} + +(* 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, (register<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); + } + } + +function forall Type 'o. 'o SignalException ((Exception) ex) = SignalExceptionMIPS(ex, 0x0000000000000000) 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..54ae354f --- /dev/null +++ b/test/typecheck/pass/mips_CP0Cause_BD_assign1.sail @@ -0,0 +1,32 @@ +val cast forall Num 'n. [:1:] -> vector<'n,1,dec,bit> effect pure cast_1_vec +val cast forall Num 'n. [:0:] -> vector<'n,1,dec,bit> effect pure cast_0_vec + +val extern forall Num 'l, Num 'm. ([:'l:], [:'m:], int) -> vector<'l,'m,dec,bit> effect pure to_vec_dec + +function forall Num 'n. (vector<'n,1,dec,bit>) cast_1_vec i = to_vec_dec (sizeof 'n, 1, i) +function forall Num 'n. (vector<'n,1,dec,bit>) cast_0_vec i = to_vec_dec (sizeof 'n, 1, i) + +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..2e80f538 --- /dev/null +++ b/test/typecheck/pass/mips_CP0Cause_BD_assign2.sail @@ -0,0 +1,32 @@ +val cast forall Num 'n. [:1:] -> vector<'n,1,dec,bit> effect pure cast_1_vec +val cast forall Num 'n. [:0:] -> vector<'n,1,dec,bit> effect pure cast_0_vec + +val extern forall Num 'l, Num 'm. ([:'l:], [:'m:], int) -> vector<'l,'m,dec,bit> effect pure to_vec_dec + +function forall Num 'n. (vector<'n,1,dec,bit>) cast_1_vec i = to_vec_dec (sizeof 'n, 1, i) +function forall Num 'n. (vector<'n,1,dec,bit>) cast_0_vec i = to_vec_dec (sizeof 'n, 1, i) + +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..eb3b9389 --- /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 extern forall Num 'n, Num 'l, 'l >= 0. (vector<'n,'l,dec,bit>, [|'n - 'l + 1:'n|]) -> bit effect pure bitvector_access_dec +val extern forall Nat 'n, Nat 'l, 'l >= 0. (vector<'n,'l,inc,bit>, [|'n:'n + 'l - 1|]) -> bit effect pure bitvector_access_inc + +overload vector_access [bitvector_access_inc; bitvector_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..4c37a6e9 --- /dev/null +++ b/test/typecheck/pass/mips_reg_field_bit.sail @@ -0,0 +1,28 @@ +default Order dec + +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_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..0ce19b4f --- /dev/null +++ b/test/typecheck/pass/mips_reg_field_bv.sail @@ -0,0 +1,28 @@ +default Order dec + +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_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..501432d3 --- /dev/null +++ b/test/typecheck/pass/nondet_assert.sail @@ -0,0 +1,14 @@ + +register int z + +val unit -> int effect {wreg, rreg, escape} 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/nzcv.sail b/test/typecheck/pass/nzcv.sail new file mode 100644 index 00000000..3e23e529 --- /dev/null +++ b/test/typecheck/pass/nzcv.sail @@ -0,0 +1,13 @@ +default Order dec + +val bit[4] -> unit effect pure test + +function test nzcv = +{ + N := 0b0; + Z := 0b0; + C := 0b0; + V := 0b0; + (N,Z,C,V) := nzcv; + () +} 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/overlap_field.sail b/test/typecheck/pass/overlap_field.sail new file mode 100644 index 00000000..82e685ee --- /dev/null +++ b/test/typecheck/pass/overlap_field.sail @@ -0,0 +1,13 @@ + +typedef A = const struct {bool field_A; int shared} +typedef B = const struct {bool field_B; int shared} + +val (bool, int) -> A effect {undef} makeA + +function makeA (x, y) = +{ + (A) record := undefined; + record.field_A := x; + record.shared := y; + record +} diff --git a/test/typecheck/pass/overload_plus.sail b/test/typecheck/pass/overload_plus.sail new file mode 100644 index 00000000..2aa8ecc5 --- /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 = "add_vec" + +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/patternrefinement.sail b/test/typecheck/pass/patternrefinement.sail new file mode 100644 index 00000000..5a89372a --- /dev/null +++ b/test/typecheck/pass/patternrefinement.sail @@ -0,0 +1,19 @@ +default Order dec + +val extern forall Num 'n, Num 'm, Num 'o, Num 'p, Order 'ord. + vector<'o, 'n, 'ord, bit> -> vector<'p, 'm, 'ord, bit> effect pure extz +val extern forall Num 'n, Num 'm, Order 'ord, Type 'a. vector<'n,'m,'ord,'a> -> [:'m:] effect pure length +val extern forall Num 'n, Num 'm, Order 'ord. (vector<'n,'m,'ord,bit>, vector<'n,'m,'ord,bit>) -> bool effect pure eq_vec +val extern forall Num 'n, Num 'm. ([:'n:],[:'m:]) -> bool effect pure eq_atom +val extern forall Type 'a. ('a, 'a) -> bool effect pure eq +overload (deinfix ==) [eq_vec; eq_atom; eq] + + +val forall 'n, 'n in {32,64}. bit['n] -> bit[64] effect pure test + +function test(v) = { + switch (length(v)) { + case 32 -> extz(v) + case 64 -> v + } +} diff --git a/test/typecheck/pass/phantom_num.sail b/test/typecheck/pass/phantom_num.sail new file mode 100644 index 00000000..c676807d --- /dev/null +++ b/test/typecheck/pass/phantom_num.sail @@ -0,0 +1,17 @@ + +val extern (int, int) -> bool effect pure gt_int = "gt" + +(* 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/pure_record.sail b/test/typecheck/pass/pure_record.sail new file mode 100644 index 00000000..c7bc373a --- /dev/null +++ b/test/typecheck/pass/pure_record.sail @@ -0,0 +1,22 @@ +default Order dec + +typedef State = const struct forall Type 'a. { + vector<0, 1, dec, 'a> N; + vector<0, 1, dec, bit> Z; +} + +let (State<bit>) myStateM = { + (State<bit>) r := undefined; + r.N := 0b1; + r.Z := 0b1; + r +} + +let (State<bit>) myState = { N = 0b1; Z = 0b1 } + +val unit -> unit effect {undef} test + +function test () = { + (State<bit>) myState2 := { N = undefined; Z = 0b1 }; + (State<bit>) myState3 := { myState2 with N = 0b0 } +} diff --git a/test/typecheck/pass/pure_record2.sail b/test/typecheck/pass/pure_record2.sail new file mode 100644 index 00000000..a0a85313 --- /dev/null +++ b/test/typecheck/pass/pure_record2.sail @@ -0,0 +1,22 @@ +default Order dec + +typedef State = const struct forall Type 'a, Nat 'n. { + vector<0, 'n, dec, 'a> N; + vector<0, 1, dec, bit> Z; +} + +let (State<bit,1>) myStateM = { + (State<bit,1>) r := undefined; + r.N := 0b1; + r.Z := 0b1; + r +} + +let (State<bit,1>) myState = { N = 0b1; Z = 0b1 } + +val unit -> unit effect {undef} test + +function test () = { + (State<bit,1>) myState2 := { N = undefined; Z = 0b1 }; + (State<bit,1>) myState3 := { myState2 with N = 0b0 } +} diff --git a/test/typecheck/pass/pure_record3.sail b/test/typecheck/pass/pure_record3.sail new file mode 100644 index 00000000..61d74ebf --- /dev/null +++ b/test/typecheck/pass/pure_record3.sail @@ -0,0 +1,25 @@ +default Order dec + +typedef State = const struct forall Type 'a, Nat 'n. { + vector<0, 'n, dec, 'a> N; + vector<0, 1, dec, bit> Z; +} + +register State<bit,1> procState + +let (State<bit,1>) myStateM = { + (State<bit,1>) r := undefined; + r.N := 0b1; + r.Z := 0b1; + r +} + +let (State<bit,1>) myState = { N = 0b1; Z = 0b1 } + +val unit -> unit effect {undef} test + +function test () = { + (State<bit,1>) myState1 := undefined; + (State<bit,1>) myState2 := { N = undefined; Z = 0b1 }; + (State<bit,1>) myState3 := { myState2 with N = 0b0 } +} 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..28978882 --- /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, 'l >= 0. (vector<'n,'l,dec,bit>, [|'n - 'l + 1:'n|]) -> bit effect pure bitvector_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 [bitvector_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/return_simple4.sail b/test/typecheck/pass/return_simple4.sail new file mode 100644 index 00000000..1bbc0e73 --- /dev/null +++ b/test/typecheck/pass/return_simple4.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/pass/set_mark.sail b/test/typecheck/pass/set_mark.sail new file mode 100644 index 00000000..af0b5ba2 --- /dev/null +++ b/test/typecheck/pass/set_mark.sail @@ -0,0 +1,11 @@ + +val extern forall Num 'l, Num 'm. ([:'l:], [:'m:], int) -> vector<'l,'m,dec,bit> effect pure to_vec_dec + +val cast forall Num 'n, Num 'm. [:0:] -> vector<'n,'m,dec,bit> effect pure cast_0_vec +function forall Num 'n, Num 'm. (vector<'n,'m,dec,bit>) cast_0_vec i = to_vec_dec (sizeof 'n, sizeof 'm, i) + +default Order dec + +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..591c17ad --- /dev/null +++ b/test/typecheck/pass/set_mark2.sail @@ -0,0 +1,11 @@ + +val extern forall Num 'l, Num 'm. ([:'l:], [:'m:], int) -> vector<'l,'m,dec,bit> effect pure to_vec_dec + +val cast forall Num 'n, Num 'm. [:0:] -> vector<'n,'m,dec,bit> effect pure cast_0_vec +function forall Num 'n, Num 'm. (vector<'n,'m,dec,bit>) cast_0_vec i = to_vec_dec (sizeof 'n, sizeof 'm, i) + +default Order dec + +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/trycatch.sail b/test/typecheck/pass/trycatch.sail new file mode 100644 index 00000000..b7f97dd0 --- /dev/null +++ b/test/typecheck/pass/trycatch.sail @@ -0,0 +1,20 @@ + +scattered typedef exception = const union + +union exception member int IntEx + +val unit -> unit effect {escape} test2 + +function test2 () = throw (IntEx(3)) + +val unit -> unit effect {escape} test + +function test () = + try { + test2(); + () + } catch { + case (IntEx(_)) -> () + } + +end exception 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/varity.sail b/test/typecheck/pass/varity.sail new file mode 100644 index 00000000..750d70eb --- /dev/null +++ b/test/typecheck/pass/varity.sail @@ -0,0 +1,19 @@ + +val int -> unit effect pure f1 +val (int, int) -> unit effect pure f2 +val (int, int, int) -> unit effect pure f3 + +function f1 (i1) = () +function f2 (i1, i2) = () +function f3 (i1, i2, i3) = () + +overload f [f1; f2; f3] + +val unit -> unit effect pure test + +function test () = +{ + f(1); + f(2, 3); + f(4, 5, 6); +} diff --git a/test/typecheck/pass/vec_pat1.sail b/test/typecheck/pass/vec_pat1.sail new file mode 100644 index 00000000..b22f0029 --- /dev/null +++ b/test/typecheck/pass/vec_pat1.sail @@ -0,0 +1,20 @@ +default Order inc + +val extern forall Num 'n. (bit['n], bit['n]) -> bit['n] effect pure bv_add = "add_vec" + +val extern forall Num 'n, Num 'l, Num 'm, Num 'o, 'l >= 0, 'm <= 'o, 'o <= 'l. + (vector<'n,'l,inc,bit>, [:'m:], [:'o:]) -> vector<'m,'o + 1 - 'm,inc,bit> effect pure vector_subrange = "bitvector_subrange_inc" + +val forall Num 'n, Num 'm, Num 'o, Num 'p. + (vector<'n,'m,inc,bit>, vector<'o,'p,inc,bit>) -> vector<'n,'m + 'p,inc,bit> + effect pure bitvector_concat + +overload (deinfix +) [bv_add] +overload append [bitvector_concat] + +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..df610fb1 --- /dev/null +++ b/test/typecheck/pass/vector_append.sail @@ -0,0 +1,14 @@ + +val extern forall Nat 'n1, Nat 'l1, Nat 'n2, Nat 'l2, Order 'o, 'l1 >= 0, 'l2 >= 0. + (vector<'n1,'l1,'o,bit>, vector<'n2,'l2,'o,bit>) -> vector<'n1,'l1 + 'l2,'o,bit> effect pure append = "bitvector_concat" + +default Order inc + +val (bit[4], bit[4]) -> bit[8] effect pure test + +function bit[8] test (v1, v2) = +{ + zv := append(v1, v2); + zv := v1 : v2; + zv +} diff --git a/test/typecheck/pass/vector_append_gen.sail b/test/typecheck/pass/vector_append_gen.sail new file mode 100644 index 00000000..ce63ed87 --- /dev/null +++ b/test/typecheck/pass/vector_append_gen.sail @@ -0,0 +1,12 @@ + +val extern forall Nat 'n1, Nat 'l1, Nat 'n2, Nat 'l2, Order 'o, 'l1 >= 0, 'l2 >= 0. + (vector<'n1,'l1,'o,bit>, vector<'n2,'l2,'o,bit>) -> vector<'n1,'l1 + 'l2,'o,bit> effect pure vector_append = "bitvector_concat" + +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); +} diff --git a/test/typecheck/pass/vector_subrange_gen.sail b/test/typecheck/pass/vector_subrange_gen.sail new file mode 100644 index 00000000..4ec067de --- /dev/null +++ b/test/typecheck/pass/vector_subrange_gen.sail @@ -0,0 +1,21 @@ + +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 extern forall Num 'n, Num 'l, Num 'm, Num 'o, 'l >= 0, 'm <= 'o, 'o <= 'l. + (vector<'n,'l,inc,bit>, [:'m:], [:'o:]) -> vector<'m,('o - 'm) + 1,inc,bit> effect pure vector_subrange = "bitvector_subrange_inc" + +val forall Nat 'n, Nat 'm. ([:'n:], [:'m:]) -> [:'n - 'm:] effect pure sub + +default Order inc + +val forall 'n, 'm, 'n >= 5. bit['n] -> bit['n - 1] effect pure test + +function forall 'n, 'n >= 5. bit['n - 1] test v = +{ + z := vector_subrange(v, 0, sub(sizeof 'n, 2)); + z := v[0 .. sub(sizeof 'n, 2)]; + z +} diff --git a/test/typecheck/pass/vector_synonym_cast.sail b/test/typecheck/pass/vector_synonym_cast.sail new file mode 100644 index 00000000..bd0acaa6 --- /dev/null +++ b/test/typecheck/pass/vector_synonym_cast.sail @@ -0,0 +1,8 @@ + +typedef vecsyn = vector<0,1,dec,bit> + +val cast vector<1,1,dec,bit> -> vector<0,1,dec,bit> effect pure norm_dec + +val vector<1,1,dec,bit> -> vecsyn effect pure test + +function test x = x diff --git a/test/typecheck/pass/while_MM.sail b/test/typecheck/pass/while_MM.sail new file mode 100644 index 00000000..e6916edd --- /dev/null +++ b/test/typecheck/pass/while_MM.sail @@ -0,0 +1,23 @@ +default Order dec + +val extern forall Num 'n, Num 'm, Num 'o, Num 'p. + ([|'n:'m|], [|'o:'p|]) -> [|'n + 'o:'m + 'p|] effect pure add_range = "add" +val extern (int, int) -> int effect pure add_int = "add" +val forall Num 'n, Num 'o, Order 'ord. + (vector<'o, 'n, 'ord, bit>, int) -> vector<'o, 'n, 'ord, bit> effect pure add_vec_int +overload (deinfix +) [add_vec_int; add_range; add_int] + +val extern bool -> bool effect pure bool_not = "not" + +val cast forall Num 'n, Num 'l. [:0:] -> vector<'n,'l,dec,bit> effect pure cast_0_vec_dec + +register (bit[64]) COUNT +register (bool) INT + +function (unit) test () = { + COUNT := 0; + while (bool_not(INT)) do { + COUNT := COUNT + 1; + } +} + diff --git a/test/typecheck/pass/while_MP.sail b/test/typecheck/pass/while_MP.sail new file mode 100644 index 00000000..05d396e2 --- /dev/null +++ b/test/typecheck/pass/while_MP.sail @@ -0,0 +1,17 @@ +default Order dec + +val extern (int, int) -> int effect pure add_int = "add" +overload (deinfix +) [add_vec_int; add_range; add_int] + +val extern bool -> bool effect pure bool_not = "not" + +register (bool) INT + +function (int) test () = { + (int) count := 0; + while (bool_not(INT)) do { + count := count + 1; + }; + return count; +} + diff --git a/test/typecheck/pass/while_PM.sail b/test/typecheck/pass/while_PM.sail new file mode 100644 index 00000000..b03a87dc --- /dev/null +++ b/test/typecheck/pass/while_PM.sail @@ -0,0 +1,23 @@ +default Order dec + +val extern forall Num 'n, Num 'm, Num 'o. ([|'n:'m|], [:'o:]) -> bool effect pure lt_range_atom = "lt" +val extern (int, int) -> bool effect pure lt_int = "lt" +overload (deinfix <) [lt_range_atom; lt_int] + +val extern forall Num 'n, Num 'm, Num 'o, Num 'p. + ([|'n:'m|], [|'o:'p|]) -> [|'n + 'o:'m + 'p|] effect pure add_range = "add" +val extern (int, int) -> int effect pure add_int = "add" +overload (deinfix +) [add_range; add_int] + +val extern forall Num 'n, Num 'l, 'l >= 0. (vector<'n,'l,dec,bit>, int) -> bit effect pure vector_access = "bitvector_access_dec" + +register (bit[64]) GPR00 + +function (unit) test ((bit) b) = { + (int) i := 0; + while (i < 64) do { + GPR00[i] := b; + i := i + 1; + } +} + diff --git a/test/typecheck/pass/while_PP.sail b/test/typecheck/pass/while_PP.sail new file mode 100644 index 00000000..454cc9ac --- /dev/null +++ b/test/typecheck/pass/while_PP.sail @@ -0,0 +1,24 @@ +default Order dec + +val extern forall Num 'n, Num 'm, Num 'o. ([|'n:'m|], [:'o:]) -> bool effect pure lt_range_atom = "lt" +val extern (int, int) -> bool effect pure lt_int = "lt" +overload (deinfix <) [lt_range_atom; lt_int] + +val (int, int) -> int effect pure mult_int +overload (deinfix * ) [mult_int] + +val extern forall Num 'n, Num 'm, Num 'o, Num 'p. + ([|'n:'m|], [|'o:'p|]) -> [|'n + 'o:'m + 'p|] effect pure add_range = "add" +val extern (int, int) -> int effect pure add_int = "add" +overload (deinfix +) [add_range; add_int] + +function (int) test ((int) n) = { + (int) i := 1; + (int) j := 1; + while (i < n) do { + j := i * j; + i := i + 1; + }; + j +} + diff --git a/test/typecheck/run_tests.sh b/test/typecheck/run_tests.sh new file mode 100755 index 00000000..a2567d21 --- /dev/null +++ b/test/typecheck/run_tests.sh @@ -0,0 +1,160 @@ +#!/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 $SAILDIR/lib/prelude_wrappers.sail $MIPS/mips_prelude.sail > $DIR/pass/mips_prelude.sail +cat $SAILDIR/lib/prelude.sail $SAILDIR/lib/prelude_wrappers.sail $MIPS/mips_prelude.sail $MIPS/mips_tlb.sail > $DIR/pass/mips_tlb.sail +cat $SAILDIR/lib/prelude.sail $SAILDIR/lib/prelude_wrappers.sail $MIPS/mips_prelude.sail $MIPS/mips_tlb.sail $MIPS/mips_wrappers.sail > $DIR/pass/mips_wrappers.sail +cat $SAILDIR/lib/prelude.sail $SAILDIR/lib/prelude_wrappers.sail $MIPS/mips_prelude.sail $MIPS/mips_tlb.sail $MIPS/mips_wrappers.sail $MIPS/mips_ast_decl.sail $MIPS/mips_insts.sail $MIPS/mips_epilogue.sail > $DIR/pass/mips_insts.sail +cat $SAILDIR/lib/prelude.sail $SAILDIR/lib/prelude_wrappers.sail $MIPS/mips_prelude.sail $MIPS/mips_tlb_stub.sail $MIPS/mips_wrappers.sail $MIPS/mips_ast_decl.sail $MIPS/mips_insts.sail $MIPS/mips_epilogue.sail > $DIR/pass/mips_notlb.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 -dsanity $DIR/pass/$i 2> /dev/null 1> $DIR/rtpass/$i; + then + if $SAILDIR/sail -ddump_tc_ast -dmagic_hash -dno_cast -dsanity $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 -dmagic_hash -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 + # MIPS requires an additional library, Mips_extras_embed. + # It might be useful to allow adding options for specific test cases. + # For now, include the library for all test cases, which doesn't seem to hurt. + if $SAILDIR/sail -lem -lem_lib Mips_extras_embed -lem_sequential -lem_mwords $DIR/$1/$i 2> /dev/null + then + green "generated lem for $1/$i" "pass" + + cp $MIPS/mips_extras_embed_sequential.lem $DIR/lem/ + # mv $SAILDIR/${i%%.*}_embed_types.lem $DIR/lem/ + mv $SAILDIR/${i%%.*}_embed_types_sequential.lem $DIR/lem/ + # mv $SAILDIR/${i%%.*}_embed.lem $DIR/lem/ + mv $SAILDIR/${i%%.*}_embed_sequential.lem $DIR/lem/ + # Test sequential embedding for now + # TODO: Add tests for the free monad + if lem -lib $SAILDIR/src/lem_interp -lib $SAILDIR/src/gen_lib/ $DIR/lem/mips_extras_embed_sequential.lem $DIR/lem/${i%%.*}_embed_types_sequential.lem $DIR/lem/${i%%.*}_embed_sequential.lem 2> /dev/null + then + green "typechecking lem for $1/$i" "pass" + else + red "typechecking lem for $1/$i" "fail" + fi + else + red "generated lem for $1/$i" "fail" + red "typechecking lem for $1/$i" "fail" + fi + done +} + +test_lem pass + +finish_suite "Lem generation 1" + +test_lem rtpass + +finish_suite "Lem generation 2" + +# function test_ocaml { +# for i in `ls $DIR/pass/`; +# do +# if $SAILDIR/sail -ocaml $DIR/$1/$i 2> /dev/null +# then +# green "generated ocaml for $1/$i" "pass" + +# rm $SAILDIR/${i%%.*}.ml +# else +# red "generated ocaml for $1/$i" "fail" +# fi +# done +# } + +# test_ocaml pass + +# finish_suite "Ocaml generation 1" + +# test_ocaml rtpass + +# finish_suite "Ocaml generation 2" + +printf "</testsuites>\n" >> $DIR/tests.xml |