diff options
Diffstat (limited to 'test')
95 files changed, 1085 insertions, 289 deletions
diff --git a/test/c/bool_bits_mapping.expect b/test/c/bool_bits_mapping.expect new file mode 100644 index 00000000..79ebd086 --- /dev/null +++ b/test/c/bool_bits_mapping.expect @@ -0,0 +1,2 @@ +ok +ok diff --git a/test/c/bool_bits_mapping.sail b/test/c/bool_bits_mapping.sail new file mode 100644 index 00000000..1a104186 --- /dev/null +++ b/test/c/bool_bits_mapping.sail @@ -0,0 +1,23 @@ +default Order dec + +$include <prelude.sail> + +mapping bool_bits : bool <-> bits(1) = { + true <-> 0b1, + false <-> 0b0 +} + +val "print_endline" : string -> unit + +function main((): unit) -> unit = { + if bool_bits(0b1) then { + print_endline("ok") + } else { + print_endline("fail") + }; + if bool_bits(true) == 0b1 then { + print_endline("ok") + } else { + print_endline("fail") + } +}
\ No newline at end of file diff --git a/test/c/cfold_reg.sail b/test/c/cfold_reg.sail index a5090e91..53066bf5 100644 --- a/test/c/cfold_reg.sail +++ b/test/c/cfold_reg.sail @@ -2,7 +2,7 @@ default Order dec $include <prelude.sail> -val "eq_string" : (string, string) -> bool +val eq_string = { lem: "eq", _: "eq_string" } : (string, string) -> bool overload operator == = {eq_string} diff --git a/test/c/cheri_capreg.sail b/test/c/cheri_capreg.sail index e8890a4a..a9480ab6 100644 --- a/test/c/cheri_capreg.sail +++ b/test/c/cheri_capreg.sail @@ -13,11 +13,11 @@ val _reg_deref = "reg_deref" : forall ('a : Type). register('a) -> 'a val zeros_0 = "zeros" : forall 'n. int('n) -> bits('n) -val zeros : forall 'n. unit -> bits('n) -function zeros() = zeros_0('n) +val zeros : forall 'n. (implicit('n), unit) -> bits('n) +function zeros(n, _) = zeros_0(n) -val ones : forall 'n, 'n >= 0 . unit -> bits('n) -function ones() = replicate_bits (0b1,'n) +val ones : forall 'n, 'n >= 0. (implicit('n), unit) -> bits('n) +function ones(n, _) = replicate_bits(0b1, n) val xor_vec = {c: "xor_bits" , _: "xor_vec"} : forall 'n. (bits('n), bits('n)) -> bits('n) diff --git a/test/c/config_register.sail b/test/c/config_register.sail index f4831ca5..8b41a3f4 100644 --- a/test/c/config_register.sail +++ b/test/c/config_register.sail @@ -2,8 +2,9 @@ default Order dec $include <prelude.sail> -function zeros forall 'n. (() : unit) -> bits('n) = { - sail_zeros('n) +val zeros : forall 'n, 'n >= 0. (implicit('n), unit) -> bits('n) +function zeros(n, _) = { + sail_zeros(n) } register configuration R : bits(32) = zeros() diff --git a/test/c/eq_struct.sail b/test/c/eq_struct.sail index b4258569..9da12aae 100644 --- a/test/c/eq_struct.sail +++ b/test/c/eq_struct.sail @@ -3,7 +3,7 @@ default Order dec $include <flow.sail> $include <exception_basic.sail> -val eq = "eq_anything" : forall ('a : Type). ('a, 'a) -> bool +val eq = { lem: "eq", _: "eq_anything" } : forall ('a : Type). ('a, 'a) -> bool overload operator == = {eq} diff --git a/test/c/fallthrough_exception.expect b/test/c/fallthrough_exception.expect new file mode 100644 index 00000000..6d9de85e --- /dev/null +++ b/test/c/fallthrough_exception.expect @@ -0,0 +1 @@ +E2 diff --git a/test/c/fallthrough_exception.sail b/test/c/fallthrough_exception.sail new file mode 100644 index 00000000..6260a603 --- /dev/null +++ b/test/c/fallthrough_exception.sail @@ -0,0 +1,20 @@ +default Order dec + +$include <prelude.sail> + +val print = "print_endline" : string -> unit + +union exception = { + E1 : unit, + E2 : unit +} + +function main((): unit) -> unit = { + try { + try throw(E2()) catch { + E1() => print("E1") + } + } catch { + E2() => print("E2") + } +}
\ No newline at end of file diff --git a/test/c/implicits.expect b/test/c/implicits.expect new file mode 100644 index 00000000..3d770e7d --- /dev/null +++ b/test/c/implicits.expect @@ -0,0 +1,11 @@ +a = 0x00000000000000FF +b = 0xFFFFFFFFFFFFFFFF +c = 0xFFFFFFFFFFFFFFFF +d = 0x0000000000000000 +e = 0x0000000000000000 +f = 0x0000000000000000 +g = 0x00000000 +h = 0x0000 +i = 0x00 +j = 0x0 +k = 0b00 diff --git a/test/c/implicits.sail b/test/c/implicits.sail new file mode 100644 index 00000000..2923fab4 --- /dev/null +++ b/test/c/implicits.sail @@ -0,0 +1,45 @@ +default Order dec + +$include <prelude.sail> + +val EXTZ : forall 'n 'm, 0 <= 'n <= 'm. (implicit('m), bits('n)) -> bits('m) + +function EXTZ(m, x) = sail_zero_extend(x, m) + +val EXTS : forall 'n 'm, 0 <= 'n <= 'm. (implicit('m), bits('n)) -> bits('m) + +function EXTS(m, x) = sail_sign_extend(x, m) + +val zeros : forall 'n, 'n >= 0. implicit('n) -> bits('n) + +function zeros(n) = replicate_bits(0b0, n) + +val dzeros : forall 'n 'm, 'n >= 0 & 'm >= 0. (implicit('n), implicit('m)) -> (bits('n), bits('m)) + +function dzeros(n, m) = (zeros(n), zeros(m)) + +val dzeros2 : forall 'n 'm, 'n >= 0 & 'm >= 0. (implicit('n), implicit('m), unit) -> (bits('n), bits('m)) + +function dzeros2(n, m, _) = (zeros(n), zeros(m)) + +function main((): unit) -> unit = { + let a: bits(64) = EXTZ(0xFF); + let b: bits(64) = EXTS(0xFF); + let c: bits(64) = EXTS(64, 0xFF); + let d: bits(64) = zeros(); + let e: bits(64) = zeros(64); + let (f, g): (bits(64), bits(32)) = dzeros(); + let (h, i) = dzeros(16, 8); + let (j, k): (bits(4), bits(2)) = dzeros2(); + print_bits("a = ", a); + print_bits("b = ", b); + print_bits("c = ", c); + print_bits("d = ", d); + print_bits("e = ", e); + print_bits("f = ", f); + print_bits("g = ", g); + print_bits("h = ", h); + print_bits("i = ", i); + print_bits("j = ", j); + print_bits("k = ", k) +}
\ No newline at end of file diff --git a/test/c/lbuild/_tags b/test/c/lbuild/_tags new file mode 100644 index 00000000..ced67350 --- /dev/null +++ b/test/c/lbuild/_tags @@ -0,0 +1,3 @@ +true: debug +<*.m{l,li}>: package(lem), package(linksem), package(zarith) +<main.native>: package(lem), package(linksem), package(zarith) diff --git a/test/c/lbuild/myocamlbuild.ml b/test/c/lbuild/myocamlbuild.ml new file mode 100644 index 00000000..cc65b03a --- /dev/null +++ b/test/c/lbuild/myocamlbuild.ml @@ -0,0 +1,77 @@ +(**************************************************************************) +(* Sail *) +(* *) +(* Copyright (c) 2013-2017 *) +(* Kathyrn Gray *) +(* Shaked Flur *) +(* Stephen Kell *) +(* Gabriel Kerneis *) +(* Robert Norton-Wright *) +(* Christopher Pulte *) +(* Peter Sewell *) +(* Alasdair Armstrong *) +(* Brian Campbell *) +(* Thomas Bauereiss *) +(* Anthony Fox *) +(* Jon French *) +(* Dominic Mulligan *) +(* Stephen Kell *) +(* Mark Wassell *) +(* *) +(* 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. *) +(**************************************************************************) + +open Ocamlbuild_plugin ;; +open Command ;; +open Pathname ;; +open Outcome ;; + +(* paths relative to _build *) +let lem = "lem" ;; + +(* All -wl ignores should be removed if you want to see the pattern compilation, exhaustive, and unused var warnings *) +let lem_opts = [A "-lib"; P ".."; + A "-wl_pat_comp"; P "ign"; + A "-wl_pat_exh"; P "ign"; + A "-wl_pat_fail"; P "ign"; + A "-wl_unused_vars"; P "ign"; + ] ;; + +dispatch begin function +| After_rules -> + rule "lem -> ml" + ~prod: "%.ml" + ~dep: "%.lem" + (fun env builder -> Seq [ + Cmd (S ([ P lem] @ lem_opts @ [ A "-ocaml"; P (env "%.lem") ])); + ]); + +| _ -> () +end ;; diff --git a/test/c/nexp_synonym.expect b/test/c/nexp_synonym.expect new file mode 100644 index 00000000..880c3ee3 --- /dev/null +++ b/test/c/nexp_synonym.expect @@ -0,0 +1 @@ +v = 0xFFFFFFFF diff --git a/test/c/nexp_synonym.sail b/test/c/nexp_synonym.sail new file mode 100644 index 00000000..b908b265 --- /dev/null +++ b/test/c/nexp_synonym.sail @@ -0,0 +1,11 @@ +default Order dec + +$include <prelude.sail> + +type LEN : Int = 32 + +let v : bits(LEN) = 0xFFFF_FFFF + +function main((): unit) -> unit = { + print_bits("v = ", v) +}
\ No newline at end of file diff --git a/test/c/poly_pair.sail b/test/c/poly_pair.sail index c4989829..7c86062d 100644 --- a/test/c/poly_pair.sail +++ b/test/c/poly_pair.sail @@ -2,7 +2,7 @@ default Order dec val print = "print_endline" : string -> unit -val "eq_int" : (int, int) -> bool +val eq_int = { lem: "eq", _: "eq_int" } : (int, int) -> bool union test('a : Type, 'b : Type) = { Ctor1 : ('a, 'b), diff --git a/test/c/reg_32_64.expect b/test/c/reg_32_64.expect new file mode 100644 index 00000000..c381486c --- /dev/null +++ b/test/c/reg_32_64.expect @@ -0,0 +1,2 @@ +R = 0xCAFECAFEFFFFFFFF +R = 0xFFFFFFFF diff --git a/test/c/reg_32_64.sail b/test/c/reg_32_64.sail new file mode 100644 index 00000000..79dfc862 --- /dev/null +++ b/test/c/reg_32_64.sail @@ -0,0 +1,39 @@ +default Order dec + +$include <prelude.sail> + +val "reg_deref" : forall ('a : Type). register('a) -> 'a effect {rreg} + +register R0 : bits(64) +register R1 : bits(64) +register R2 : bits(64) +register R3 : bits(64) + +let GPRs : vector(4, dec, register(bits(64))) = [ref R3, ref R2, ref R1, ref R0] + +type regno('r: Int) -> Bool = 0 <= 'r <= 3 + +val set_R : forall 'r 'd, regno('r) & 'd in {32, 64}. + (int('r), bits('d)) -> unit effect {wreg} + +function set_R(r, data) = { + let R = GPRs[r]; + (*R)['d - 1 .. 0] = data +} + +val get_R : forall 'r 'd, regno('r) & 'd in {32, 64}. + (implicit('d), int('r)) -> bits('d) effect {rreg} + +function get_R(datasize, r) = { + let R = GPRs[r]; + reg_deref(R)[datasize - 1 .. 0] +} + +overload R = {set_R, get_R} + +function main() -> unit = { + R(0) = 0xCAFE_CAFE_0000_0000; + R(0) = 0xFFFF_FFFF; + print_bits("R = ", R(0) : bits(64)); + print_bits("R = ", R(0) : bits(32)) +} diff --git a/test/c/run_tests.py b/test/c/run_tests.py index 4f221636..4927e281 100755 --- a/test/c/run_tests.py +++ b/test/c/run_tests.py @@ -64,6 +64,30 @@ def test_ocaml(name): results.collect(tests) return results.finish() +def test_lem(name): + banner('Testing {}'.format(name)) + results = Results(name) + for filenames in chunks(os.listdir('.'), parallel()): + tests = {} + for filename in filenames: + basename = os.path.splitext(os.path.basename(filename))[0] + tests[filename] = os.fork() + if tests[filename] == 0: + step('sail -lem {}'.format(filename)) + step('mkdir -p _lbuild_{}'.format(basename)) + step('cp {}*.lem _lbuild_{}'.format(basename, basename)) + step('cp lbuild/* _lbuild_{}'.format(basename)) + step('cp ../../src/gen_lib/*.lem _lbuild_{}'.format(basename)) + os.chdir('_lbuild_{}'.format(basename)) + step('echo "let _ = {}.main ()" > main.ml'.format(basename.capitalize())) + step('ocamlbuild -use-ocamlfind main.native'.format(basename, basename)) + step('./main.native 1> {}.lresult'.format(basename)) + step('diff ../{}.expect {}.lresult'.format(basename, basename)) + print '{} {}{}{}'.format(filename, color.PASS, 'ok', color.END) + sys.exit() + results.collect(tests) + return results.finish() + xml = '<testsuites>\n' xml += test_c('unoptimized C', '', '', True) @@ -76,6 +100,8 @@ xml += test_interpreter('interpreter') xml += test_ocaml('OCaml') +#xml += test_lem('lem') + xml += '</testsuites>\n' output = open('tests.xml', 'w') diff --git a/test/mono/assert.sail b/test/mono/assert.sail index 46892956..9d941467 100644 --- a/test/mono/assert.sail +++ b/test/mono/assert.sail @@ -1,5 +1,6 @@ $include <smt.sail> $include <flow.sail> +$include <arith.sail> default Order dec type bits ('n : Int) = vector('n, dec, bit) val operator & = "and_bool" : (bool, bool) -> bool diff --git a/test/mono/builtins.sail b/test/mono/builtins.sail index 99447d42..770259be 100644 --- a/test/mono/builtins.sail +++ b/test/mono/builtins.sail @@ -43,7 +43,7 @@ function test(b) = { assert(x != y, "!= by propagation"); assert(slice(x, 0, 4) == slice(x',0,4), "propagated slice == runtime slice"); assert(0x3 == slice(y, 4, 4), "literal vs propagated middle slice"); - assert(UInt(x) == (match n { 8 => 18, 16 => 4660 }), "UInt propagation vs literal"); + assert(UInt(x) == (match n { 8 => 18, 16 => 4660 }) : int, "UInt propagation vs literal"); assert(shl_int(5,2) == shl_int(launder_int(5),2), "shl_int"); } diff --git a/test/mono/castreq.sail b/test/mono/castreq.sail index 586aa54b..bb1bc952 100644 --- a/test/mono/castreq.sail +++ b/test/mono/castreq.sail @@ -1,5 +1,6 @@ $include <smt.sail> $include <flow.sail> +$include <arith.sail> default Order dec type bits ('n : Int) = vector('n, dec, bit) val operator & = "and_bool" : (bool, bool) -> bool @@ -10,8 +11,8 @@ overload operator * = {mult_range, mult_int, mult_real} val replicate_bits = "replicate_bits" : forall 'n 'm. (bits('n), atom('m)) -> bits('n * 'm) overload operator < = {lt_atom, lt_int} val "extz_vec" : forall 'n 'm. (atom('m),vector('n, dec, bit)) -> vector('m, dec, bit) effect pure -val extzv : forall 'n 'm. vector('n, dec, bit) -> vector('m, dec, bit) effect pure -function extzv(v) = extz_vec(sizeof('m),v) +val extzv : forall 'n 'm. (implicit('m), vector('n, dec, bit)) -> vector('m, dec, bit) effect pure +function extzv(m, v) = extz_vec(m,v) val bitvector_concat = {ocaml: "append", lem: "concat_vec", c: "append"} : forall ('n : Int) ('m : Int). (bits('n), bits('m)) -> bits('n + 'm) overload append = {bitvector_concat} @@ -19,12 +20,13 @@ val bitvector_cast_in = "zeroExtend" : forall 'n. bits('n) -> bits('n) effect pu val bitvector_cast_out = "zeroExtend" : forall 'n. bits('n) -> bits('n) effect pure val bitvector_length = "length" : forall 'n. bits('n) -> atom('n) overload length = {bitvector_length} +overload __size = {length} /* Test generation of casts across case splits (e.g., going from bits('m) to bits(32)) */ -val foo : forall 'm 'n, 'm in {8,16} & 'n in {32,64}. bits('m) -> bits('n) effect pure +val foo : forall 'm 'n, 'm in {8,16} & 'n in {32,64}. (implicit('n), bits('m)) -> bits('n) effect pure -function foo(x) = +function foo(n, x) = let y : bits(16) = extzv(x) in match 'n { 32 => y@y, @@ -43,9 +45,9 @@ function bar(x) = 16 => use(x) } -val ret : forall 'm 'n, 'm in {8,16} & 'n in {32,64}. bits('m) -> bits('n) effect {undef} +val ret : forall 'm 'n, 'm in {8,16} & 'n in {32,64}. (implicit('n), bits('m)) -> bits('n) effect {undef} -function ret(x) = +function ret(n, x) = let y : bits(16) = extzv(x) in match 'n { 32 => return y@y, diff --git a/test/mono/castrequnion.sail b/test/mono/castrequnion.sail index 4729fb11..1eefb2ad 100644 --- a/test/mono/castrequnion.sail +++ b/test/mono/castrequnion.sail @@ -4,9 +4,9 @@ $include <prelude.sail> val bitvector_cast_in = "zeroExtend" : forall 'n. bits('n) -> bits('n) effect pure val bitvector_cast_out = "zeroExtend" : forall 'n. bits('n) -> bits('n) effect pure -val foo : forall 'm 'n, 'm in {8,16} & 'n in {16,32,64}. bits('m) -> option(bits('n)) effect pure +val foo : forall 'm 'n, 'm in {8,16} & 'n in {16,32,64}. (implicit('n), bits('m)) -> option(bits('n)) effect pure -function foo(x) = +function foo(n, x) = let y : bits(16) = sail_zero_extend(x,16) in match 'n { 16 => None(), diff --git a/test/mono/control_deps.sail b/test/mono/control_deps.sail index dd3bba65..e97dc0fa 100644 --- a/test/mono/control_deps.sail +++ b/test/mono/control_deps.sail @@ -10,8 +10,8 @@ overload operator * = {mult_range, mult_int, mult_real} val replicate_bits = "replicate_bits" : forall 'n 'm. (bits('n), atom('m)) -> bits('n * 'm) overload operator < = {lt_atom, lt_int} val "extz_vec" : forall 'n 'm. (atom('m),vector('n, dec, bit)) -> vector('m, dec, bit) effect pure -val extz : forall 'n 'm. vector('n, dec, bit) -> vector('m, dec, bit) effect pure -function extz(v) = extz_vec(sizeof('m),v) +val extz : forall 'n 'm. (implicit('m), vector('n, dec, bit)) -> vector('m, dec, bit) effect pure +function extz(m, v) = extz_vec(m,v) val bitvector_concat = {ocaml: "append", lem: "concat_vec", c: "append"} : forall ('n : Int) ('m : Int). (bits('n), bits('m)) -> bits('n + 'm) overload append = {bitvector_concat} diff --git a/test/mono/exint.sail b/test/mono/exint.sail index 65589fb8..639e7d45 100644 --- a/test/mono/exint.sail +++ b/test/mono/exint.sail @@ -10,8 +10,8 @@ overload operator * = {mult_range, mult_int, mult_real} val replicate_bits = "replicate_bits" : forall 'n 'm. (bits('n), atom('m)) -> bits('n * 'm) overload operator < = {lt_atom, lt_int} val "extz_vec" : forall 'n 'm. (atom('m),vector('n, dec, bit)) -> vector('m, dec, bit) effect pure -val extzv : forall 'n 'm. vector('n, dec, bit) -> vector('m, dec, bit) effect pure -function extzv(v) = extz_vec(sizeof('m),v) +val extzv : forall 'n 'm. (implicit('m), vector('n, dec, bit)) -> vector('m, dec, bit) effect pure +function extzv(m, v) = extz_vec(m,v) val bitvector_concat = {ocaml: "append", lem: "concat_vec", c: "append"} : forall ('n : Int) ('m : Int). (bits('n), bits('m)) -> bits('n + 'm) overload append = {bitvector_concat} diff --git a/test/mono/feature.sail b/test/mono/feature.sail index c7e13e11..c12f79e8 100644 --- a/test/mono/feature.sail +++ b/test/mono/feature.sail @@ -10,8 +10,8 @@ overload operator * = {mult_range, mult_int, mult_real} val replicate_bits = "replicate_bits" : forall 'n 'm. (bits('n), atom('m)) -> bits('n * 'm) overload operator < = {lt_atom, lt_int} val "extz_vec" : forall 'n 'm. (atom('m),vector('n, dec, bit)) -> vector('m, dec, bit) effect pure -val extzv : forall 'n 'm. vector('n, dec, bit) -> vector('m, dec, bit) effect pure -function extzv(v) = extz_vec(sizeof('m),v) +val extzv : forall 'n 'm. (implicit('m), vector('n, dec, bit)) -> vector('m, dec, bit) effect pure +function extzv(m, v) = extz_vec(m,v) val bitvector_concat = {ocaml: "append", lem: "concat_vec", c: "append"} : forall ('n : Int) ('m : Int). (bits('n), bits('m)) -> bits('n + 'm) overload append = {bitvector_concat} diff --git a/test/mono/mutrecmono.sail b/test/mono/mutrecmono.sail index c5ed1c0d..557a8748 100644 --- a/test/mono/mutrecmono.sail +++ b/test/mono/mutrecmono.sail @@ -5,8 +5,8 @@ type bits ('n : Int) = vector('n, dec, bit) val eq_vec = {ocaml: "eq_list", lem: "eq_vec"} : forall 'n. (bits('n), bits('n)) -> bool overload operator == = {eq_int, eq_vec} val "extz_vec" : forall 'n 'm. (atom('m),vector('n, dec, bit)) -> vector('m, dec, bit) effect pure -val extz : forall 'n 'm. vector('n, dec, bit) -> vector('m, dec, bit) effect pure -function extz(v) = extz_vec(sizeof('m),v) +val extz : forall 'n 'm. (implicit('m), vector('n, dec, bit)) -> vector('m, dec, bit) effect pure +function extz(m,v) = extz_vec(m,v) val UInt = { ocaml: "uint", lem: "uint", diff --git a/test/mono/run_tests.sh b/test/mono/run_tests.sh index 6a9dedd6..08926aaa 100755 --- a/test/mono/run_tests.sh +++ b/test/mono/run_tests.sh @@ -6,9 +6,9 @@ SAILDIR="$DIR/../.." TESTSDIR="$DIR" OUTPUTDIR="$DIR/test-output" -RED='\033[0;31m' -GREEN='\033[0;32m' -YELLOW='\033[0;33m' +RED='\033[0;91m' +GREEN='\033[0;92m' +YELLOW='\033[0;93m' NC='\033[0m' rm -f $DIR/tests.xml diff --git a/test/mono/set.sail b/test/mono/set.sail index b7cf4862..74d4693e 100644 --- a/test/mono/set.sail +++ b/test/mono/set.sail @@ -1,4 +1,5 @@ default Order dec +$include <flow.sail> type bits ('n : Int) = vector('n, dec, bit) val operator & = "and_bool" : (bool, bool) -> bool val eq_vec = {ocaml: "eq_list", lem: "eq_vec"} : forall 'n. (bits('n), bits('n)) -> bool @@ -9,11 +10,11 @@ val vector_subrange = {ocaml: "subrange", lem: "subrange_vec_dec"} : forall ('n val mult_int = {ocaml: "mult", lem: "integerMult"} : (int, int) -> int overload operator * = {mult_range, mult_int, mult_real} val "extz_vec" : forall 'n 'm. (atom('m),vector('n, dec, bit)) -> vector('m, dec, bit) effect pure -val extz : forall 'n 'm. vector('n, dec, bit) -> vector('m, dec, bit) effect pure -function extz(v) = extz_vec(sizeof('m),v) +val extz : forall 'n 'm. (implicit('m), vector('n, dec, bit)) -> vector('m, dec, bit) effect pure +function extz(m,v) = extz_vec(m,v) val "exts_vec" : forall 'n 'm. (atom('m),vector('n, dec, bit)) -> vector('m, dec, bit) effect pure -val exts : forall 'n 'm. vector('n, dec, bit) -> vector('m, dec, bit) effect pure -function exts(v) = exts_vec(sizeof('m),v) +val exts : forall 'n 'm. (implicit('m), vector('n, dec, bit)) -> vector('m, dec, bit) effect pure +function exts(m,v) = exts_vec(m,v) /* A function which is merely parametrised by a size does not need to be monomorphised */ diff --git a/test/mono/times8.sail b/test/mono/times8.sail index 56b1d209..be672446 100644 --- a/test/mono/times8.sail +++ b/test/mono/times8.sail @@ -10,8 +10,8 @@ overload operator * = {mult_range, mult_int, mult_real} val replicate_bits = "replicate_bits" : forall 'n 'm. (bits('n), atom('m)) -> bits('n * 'm) overload operator < = {lt_atom, lt_int} val "extz_vec" : forall 'n 'm. (atom('m),vector('n, dec, bit)) -> vector('m, dec, bit) effect pure -val extzv : forall 'n 'm. vector('n, dec, bit) -> vector('m, dec, bit) effect pure -function extzv(v) = extz_vec(sizeof('m),v) +val extzv : forall 'n 'm. (implicit('m), vector('n, dec, bit)) -> vector('m, dec, bit) effect pure +function extzv(m,v) = extz_vec(m,v) val bitvector_concat = {ocaml: "append", lem: "concat_vec", c: "append"} : forall ('n : Int) ('m : Int). (bits('n), bits('m)) -> bits('n + 'm) overload append = {bitvector_concat} diff --git a/test/mono/times8div8.sail b/test/mono/times8div8.sail index 31f63fda..a5fd1c37 100644 --- a/test/mono/times8div8.sail +++ b/test/mono/times8div8.sail @@ -1,5 +1,6 @@ $include <smt.sail> $include <flow.sail> +$include <arith.sail> default Order dec type bits ('n : Int) = vector('n, dec, bit) val operator & = "and_bool" : (bool, bool) -> bool @@ -10,8 +11,8 @@ overload operator * = {mult_range, mult_int, mult_real} val replicate_bits = "replicate_bits" : forall 'n 'm. (bits('n), atom('m)) -> bits('n * 'm) overload operator < = {lt_atom, lt_int} val "extz_vec" : forall 'n 'm. (atom('m),vector('n, dec, bit)) -> vector('m, dec, bit) effect pure -val extzv : forall 'n 'm. vector('n, dec, bit) -> vector('m, dec, bit) effect pure -function extzv(v) = extz_vec(sizeof('m),v) +val extzv : forall 'n 'm. (implicit('m), vector('n, dec, bit)) -> vector('m, dec, bit) effect pure +function extzv(m,v) = extz_vec(m,v) val bitvector_concat = {ocaml: "append", lem: "concat_vec", c: "append"} : forall ('n : Int) ('m : Int). (bits('n), bits('m)) -> bits('n + 'm) overload append = {bitvector_concat} diff --git a/test/mono/varpatterns.sail b/test/mono/varpatterns.sail index 9de412ac..b2c9e7ee 100644 --- a/test/mono/varpatterns.sail +++ b/test/mono/varpatterns.sail @@ -35,7 +35,7 @@ val test : bool -> unit effect {escape} function test(b) = { let 'n : {|8,16|} = if b then 8 else 16; let x : bits('n) = match 'n { 8 => 0x12, 16 => 0x1234 }; - assert(UInt(x) == (match n { 8 => 18, 16 => 4660 }), "UInt"); + assert(UInt(x) == (match n { 8 => 18, 16 => 4660 }) : int, "UInt"); } val test2 : bool -> unit effect {escape} @@ -43,7 +43,7 @@ val test2 : bool -> unit effect {escape} function test2(b) = { let 'n = (if b then 8 else 16) : {|8,16|}; let x : bits('n) = match 'n { 8 => 0x12, 16 => 0x1234 }; - assert(UInt(x) == (match n { 8 => 18, 16 => 4660 }), "UInt"); + assert(UInt(x) == (match n { 8 => 18, 16 => 4660 }) : int, "UInt"); } val test_mult : {|4,8|} -> unit effect {escape} @@ -51,7 +51,7 @@ val test_mult : {|4,8|} -> unit effect {escape} function test_mult('m) = { let 'n = 2 * 'm; let x : bits('n) = match 'n { 8 => 0x12, 16 => 0x1234 }; - assert(UInt(x) == (match n { 8 => 18, 16 => 4660 }), "UInt"); + assert(UInt(x) == (match n { 8 => 18, 16 => 4660 }) : int, "UInt"); } val run : unit -> unit effect {escape} diff --git a/test/run_tests.sh b/test/run_tests.sh index 71c3eea1..09e99ff2 100755 --- a/test/run_tests.sh +++ b/test/run_tests.sh @@ -18,6 +18,12 @@ printf "==========================================\n" ./lem/run_tests.sh printf "\n==========================================\n" +printf "Monomorphisation tests\n" +printf "==========================================\n" + +./mono/run_tests.sh + +printf "\n==========================================\n" printf "Ocaml tests\n" printf "==========================================\n" diff --git a/test/typecheck/pass/Replicate.sail b/test/typecheck/pass/Replicate.sail new file mode 100644 index 00000000..03954a9f --- /dev/null +++ b/test/typecheck/pass/Replicate.sail @@ -0,0 +1,12 @@ +default Order dec + +$include <smt.sail> +$include <prelude.sail> + +val Replicate : forall ('M : Int) ('N : Int), 'M >= 1. + (implicit('N), bits('M)) -> bits('N) effect {escape} + +function Replicate (N, x) = { + assert('N % 'M == 0); + replicate_bits(x, 'N / 'M) +}
\ No newline at end of file diff --git a/test/typecheck/pass/Replicate/v1.expect b/test/typecheck/pass/Replicate/v1.expect new file mode 100644 index 00000000..92c6d7cd --- /dev/null +++ b/test/typecheck/pass/Replicate/v1.expect @@ -0,0 +1,8 @@ +Type error: +[[96mReplicate/v1.sail[0m]:11:4-30 +11[96m |[0m replicate_bits(x, 'N / 'M) + [91m |[0m [91m^------------------------^[0m + [91m |[0m Tried performing type coercion from vector(('M * div('N, 'M)), dec, bit) to vector('N, dec, bit) on replicate_bits(x, div(__id(N), bitvector_length(x))) + [91m |[0m Coercion failed because: + [91m |[0m Mismatched argument types in subtype check + [91m |[0m diff --git a/test/typecheck/pass/Replicate/v1.sail b/test/typecheck/pass/Replicate/v1.sail new file mode 100644 index 00000000..69f2bb6f --- /dev/null +++ b/test/typecheck/pass/Replicate/v1.sail @@ -0,0 +1,12 @@ +default Order dec + +$include <smt.sail> +$include <prelude.sail> + +val Replicate : forall ('M : Int) ('N : Int), 'M >= 0. + (implicit('N), bits('M)) -> bits('N) effect {escape} + +function Replicate (N, x) = { + assert('N % 'M == 0); + replicate_bits(x, 'N / 'M) +}
\ No newline at end of file diff --git a/test/typecheck/pass/Replicate/v2.expect b/test/typecheck/pass/Replicate/v2.expect new file mode 100644 index 00000000..0dec309f --- /dev/null +++ b/test/typecheck/pass/Replicate/v2.expect @@ -0,0 +1,8 @@ +Type error: +[[96mReplicate/v2.sail[0m]:10:4-30 +10[96m |[0m replicate_bits(x, 'N / 'M) + [91m |[0m [91m^------------------------^[0m + [91m |[0m Tried performing type coercion from {('ex42# : Int), true. vector(('M * 'ex42#), dec, bit)} to vector('N, dec, bit) on replicate_bits(x, div_int(__id(N), bitvector_length(x))) + [91m |[0m Coercion failed because: + [91m |[0m Mismatched argument types in subtype check + [91m |[0m diff --git a/test/typecheck/pass/Replicate/v2.sail b/test/typecheck/pass/Replicate/v2.sail new file mode 100644 index 00000000..e54b0af4 --- /dev/null +++ b/test/typecheck/pass/Replicate/v2.sail @@ -0,0 +1,11 @@ +default Order dec + +$include <prelude.sail> + +val Replicate : forall ('M : Int) ('N : Int), 'M >= 1. + (implicit('N), bits('M)) -> bits('N) effect {escape} + +function Replicate (N, x) = { + assert('N % 'M == 0); + replicate_bits(x, 'N / 'M) +}
\ No newline at end of file diff --git a/test/typecheck/pass/bitvector_param.sail b/test/typecheck/pass/bitvector_param.sail new file mode 100644 index 00000000..ffebeb6e --- /dev/null +++ b/test/typecheck/pass/bitvector_param.sail @@ -0,0 +1,42 @@ +/* from prelude */ +default Order dec +type bits ('n : Int) = vector('n, dec, bit) + +val vector_subrange = { + ocaml: "subrange", + lem: "subrange_vec_dec", + c: "vector_subrange", + coq: "subrange_vec_dec" +} : forall ('n : Int) ('m : Int) ('o : Int), 0 <= 'o <= 'm < 'n. + (bits('n), atom('m), atom('o)) -> bits('m - 'o + 1) + +val vector_update_subrange_dec = {ocaml: "update_subrange", c: "vector_update_subrange", lem: "update_subrange_vec_dec", coq: "update_subrange_vec_dec"} : forall 'n 'm 'o. + (bits('n), atom('m), atom('o), bits('m - ('o - 1))) -> bits('n) + +val vector_update_subrange_inc = {ocaml: "update_subrange", lem: "update_subrange_vec_inc"} : forall 'n 'm 'o. + (vector('n, inc, bit), atom('m), atom('o), vector('o - ('m - 1), inc, bit)) -> vector('n, inc, bit) + +overload vector_update_subrange = {vector_update_subrange_dec, vector_update_subrange_inc} + +val bitvector_concat = {c: "append", ocaml: "append", lem: "concat_vec", coq: "concat_vec"} : forall ('n : Int) ('m : Int). + (bits('n), bits('m)) -> bits('n + 'm) + +val vector_concat = {ocaml: "append", lem: "append_list"} : forall ('n : Int) ('m : Int) ('a : Type). + (vector('n, dec, 'a), vector('m, dec, 'a)) -> vector('n + 'm, dec, 'a) + +overload append = {bitvector_concat, vector_concat} + +val "reg_deref" : forall ('a : Type). register('a) -> 'a effect {rreg} +/* sneaky deref with no effect necessary for bitfield writes */ +val _reg_deref = "reg_deref" : forall ('a : Type). register('a) -> 'a + +type xlen : Int = 64 +type ylen : Int = 1 + +type xlenbits = bits(xlen) + +bitfield Mstatus : xlenbits = { + SD : xlen - ylen, + SXL : xlen - ylen - 1 .. xlen - ylen - 3 +} +register mstatus : Mstatus diff --git a/test/typecheck/pass/bool_bits_mapping.sail b/test/typecheck/pass/bool_bits_mapping.sail new file mode 100644 index 00000000..7fd2bae3 --- /dev/null +++ b/test/typecheck/pass/bool_bits_mapping.sail @@ -0,0 +1,8 @@ +default Order dec + +$include <prelude.sail> + +mapping bool_bits : bool <-> bits(1) = { + true <-> 0b1, + false <-> 0b0 +} diff --git a/test/typecheck/pass/bool_constraint/v1.expect b/test/typecheck/pass/bool_constraint/v1.expect index 3e2c7bde..b1597759 100644 --- a/test/typecheck/pass/bool_constraint/v1.expect +++ b/test/typecheck/pass/bool_constraint/v1.expect @@ -1,27 +1,20 @@ -Type error at file "bool_constraint/v1.sail", line 12, character 20 to line 12, character 20 - - if b then n else [41m4[0m - -Tried performing type coercion from int(4) to {'m, ('b & 'm == 'n | not('b) & 'm == 3). int('m)} on 4 -Coercion failed because: - int(4) is not a subtype of {('m : Int), (('b & 'm == 'n) | (not('b) & 'm == 3)). int('m)} - in context - * 4 == 'ex41#m - * not('b) - where - * 'b bound at file "bool_constraint/v1.sail", line 11, character 1 to line 13, character 1 - -[41mfunction foo(b, n) = {[0m -[41m if b then n else 4[0m -[41m}[0m - - * 'ex41#m bound at file "bool_constraint/v1.sail", line 12, character 20 to line 12, character 20 - - if b then n else [41m4[0m - - * 'n bound at file "bool_constraint/v1.sail", line 11, character 1 to line 13, character 1 - -[41mfunction foo(b, n) = {[0m -[41m if b then n else 4[0m -[41m}[0m - +Type error: +[[96mbool_constraint/v1.sail[0m]:12:19-20 +12[96m |[0m if b then n else 4 + [91m |[0m [91m^[0m + [91m |[0m Tried performing type coercion from int(4) to {('m : Int), (('b & 'm == 'n) | (not('b) & 'm == 3)). int('m)} on 4 + [91m |[0m Coercion failed because: + [91m |[0m int(4) is not a subtype of {('m : Int), (('b & 'm == 'n) | (not('b) & 'm == 3)). int('m)} + [91m |[0m [[96mbool_constraint/v1.sail[0m]:11:0-13:1 + [91m |[0m 11[96m |[0mfunction foo(b, n) = { + [91m |[0m [93m |[0m[93m^---------------------[0m + [91m |[0m 13[96m |[0m} + [91m |[0m [93m |[0m[93m^[0m + [91m |[0m [93m |[0m 'b bound here + [91m |[0m [[96mbool_constraint/v1.sail[0m]:11:0-13:1 + [91m |[0m 11[96m |[0mfunction foo(b, n) = { + [91m |[0m [93m |[0m[93m^---------------------[0m + [91m |[0m 13[96m |[0m} + [91m |[0m [93m |[0m[93m^[0m + [91m |[0m [93m |[0m 'n bound here + [91m |[0m diff --git a/test/typecheck/pass/bool_constraint/v2.expect b/test/typecheck/pass/bool_constraint/v2.expect index 847ef329..c7a355e1 100644 --- a/test/typecheck/pass/bool_constraint/v2.expect +++ b/test/typecheck/pass/bool_constraint/v2.expect @@ -1,5 +1,6 @@ -Type error at file "bool_constraint/v2.sail", line 38, character 5 to line 38, character 32 - - [41m_prove(constraint('n <= 14))[0m - -Cannot prove 'n <= 14 +Type error: +[[96mbool_constraint/v2.sail[0m]:38:4-32 +38[96m |[0m _prove(constraint('n <= 14)) + [91m |[0m [91m^--------------------------^[0m + [91m |[0m Cannot prove 'n <= 14 + [91m |[0m diff --git a/test/typecheck/pass/bool_constraint/v3.expect b/test/typecheck/pass/bool_constraint/v3.expect index ca87fac1..63791a70 100644 --- a/test/typecheck/pass/bool_constraint/v3.expect +++ b/test/typecheck/pass/bool_constraint/v3.expect @@ -1,5 +1,6 @@ -Type error at file "bool_constraint/v3.sail", line 46, character 5 to line 46, character 32 - - [41m_prove(constraint('n <= 14))[0m - -Cannot prove 'n <= 14 +Type error: +[[96mbool_constraint/v3.sail[0m]:46:4-32 +46[96m |[0m _prove(constraint('n <= 14)) + [91m |[0m [91m^--------------------------^[0m + [91m |[0m Cannot prove 'n <= 14 + [91m |[0m diff --git a/test/typecheck/pass/bool_constraint/v4.expect b/test/typecheck/pass/bool_constraint/v4.expect index 07363175..420909bf 100644 --- a/test/typecheck/pass/bool_constraint/v4.expect +++ b/test/typecheck/pass/bool_constraint/v4.expect @@ -1,5 +1,6 @@ -Type error at file "bool_constraint/v4.sail", line 46, character 5 to line 46, character 32 - - [41m_prove(constraint('n <= 13))[0m - -Cannot prove 'n <= 13 +Type error: +[[96mbool_constraint/v4.sail[0m]:46:4-32 +46[96m |[0m _prove(constraint('n <= 13)) + [91m |[0m [91m^--------------------------^[0m + [91m |[0m Cannot prove 'n <= 13 + [91m |[0m diff --git a/test/typecheck/pass/constrained_struct/v1.expect b/test/typecheck/pass/constrained_struct/v1.expect index ab25cbc4..8c95193d 100644 --- a/test/typecheck/pass/constrained_struct/v1.expect +++ b/test/typecheck/pass/constrained_struct/v1.expect @@ -1,5 +1,6 @@ -Type error at file "constrained_struct/v1.sail", line 10, character 19 to line 10, character 26 - -type MyStruct64 = [41mMyStruct[0m(65) - -Could not prove (65 == 32 | 65 == 64) for type constructor MyStruct +Type error: +[[96mconstrained_struct/v1.sail[0m]:10:18-26 +10[96m |[0mtype MyStruct64 = MyStruct(65) + [91m |[0m [91m^------^[0m + [91m |[0m Could not prove (65 == 32 | 65 == 64) for type constructor MyStruct + [91m |[0m diff --git a/test/typecheck/pass/constraint_ctor/v1.expect b/test/typecheck/pass/constraint_ctor/v1.expect index c3886af8..cf3b9399 100644 --- a/test/typecheck/pass/constraint_ctor/v1.expect +++ b/test/typecheck/pass/constraint_ctor/v1.expect @@ -1,5 +1,6 @@ -Type error at file "constraint_ctor/v1.sail", line 10, character 3 to line 10, character 29 - - [41m_prove(constraint('x >= 4))[0m; - -Cannot prove 'x >= 4 +Type error: +[[96mconstraint_ctor/v1.sail[0m]:10:2-29 +10[96m |[0m _prove(constraint('x >= 4)); + [91m |[0m [91m^-------------------------^[0m + [91m |[0m Cannot prove 'x >= 4 + [91m |[0m diff --git a/test/typecheck/pass/constraint_ctor/v2.expect b/test/typecheck/pass/constraint_ctor/v2.expect index a315b3b7..0e56f0a4 100644 --- a/test/typecheck/pass/constraint_ctor/v2.expect +++ b/test/typecheck/pass/constraint_ctor/v2.expect @@ -1,5 +1,6 @@ -Type error at file "constraint_ctor/v2.sail", line 18, character 3 to line 18, character 30 - - [41m_prove(constraint('x >= 24))[0m; - -Cannot prove 'x >= 24 +Type error: +[[96mconstraint_ctor/v2.sail[0m]:18:2-30 +18[96m |[0m _prove(constraint('x >= 24)); + [91m |[0m [91m^--------------------------^[0m + [91m |[0m Cannot prove 'x >= 24 + [91m |[0m diff --git a/test/typecheck/pass/constraint_ctor/v3.expect b/test/typecheck/pass/constraint_ctor/v3.expect index e0edd01a..37d1dff2 100644 --- a/test/typecheck/pass/constraint_ctor/v3.expect +++ b/test/typecheck/pass/constraint_ctor/v3.expect @@ -1,5 +1,6 @@ -Type error at file "constraint_ctor/v3.sail", line 18, character 3 to line 18, character 30 - - [41m_prove(constraint('x >= 23))[0m; - -Cannot prove 'x >= 23 +Type error: +[[96mconstraint_ctor/v3.sail[0m]:18:2-30 +18[96m |[0m _prove(constraint('x >= 23)); + [91m |[0m [91m^--------------------------^[0m + [91m |[0m Cannot prove 'x >= 23 + [91m |[0m diff --git a/test/typecheck/pass/constraint_ctor/v4.expect b/test/typecheck/pass/constraint_ctor/v4.expect index 06eb9d22..64893e4d 100644 --- a/test/typecheck/pass/constraint_ctor/v4.expect +++ b/test/typecheck/pass/constraint_ctor/v4.expect @@ -1,5 +1,6 @@ -Type error at file "constraint_ctor/v4.sail", line 17, character 34 to line 17, character 36 - -function bar(Bar(x as int('x)) : [41mBar[0m(23)) -> unit = { - -Could not prove 23 <= 22 for type constructor Bar +Type error: +[[96mconstraint_ctor/v4.sail[0m]:17:33-36 +17[96m |[0mfunction bar(Bar(x as int('x)) : Bar(23)) -> unit = { + [91m |[0m [91m^-^[0m + [91m |[0m Could not prove 23 <= 22 for type constructor Bar + [91m |[0m diff --git a/test/typecheck/pass/constraint_ctor/v5.expect b/test/typecheck/pass/constraint_ctor/v5.expect index b6df0222..fc2ef615 100644 --- a/test/typecheck/pass/constraint_ctor/v5.expect +++ b/test/typecheck/pass/constraint_ctor/v5.expect @@ -1,5 +1,6 @@ -Type error at file "constraint_ctor/v5.sail", line 27, character 3 to line 27, character 29 - - [41m_prove(constraint('x >= 4))[0m; - -Cannot prove 'x >= 4 +Type error: +[[96mconstraint_ctor/v5.sail[0m]:27:2-29 +27[96m |[0m _prove(constraint('x >= 4)); + [91m |[0m [91m^-------------------------^[0m + [91m |[0m Cannot prove 'x >= 4 + [91m |[0m diff --git a/test/typecheck/pass/exist_synonym/v1.expect b/test/typecheck/pass/exist_synonym/v1.expect index fb1b2619..cc8b874f 100644 --- a/test/typecheck/pass/exist_synonym/v1.expect +++ b/test/typecheck/pass/exist_synonym/v1.expect @@ -1,6 +1,8 @@ -Type error at file "exist_synonym/v1.sail", line 6, character 42 to line 6, character 42 - -let x : {'n, 0 <= 'n <= 33. regno('n)} = [41m4[0m - -Tried performing type coercion from int(4) to {'n, (0 <= 'n & 'n <= 33). regno('n)} on 4 -Coercion failed because: Could not prove constraints (0 <= 'n & ('n + 1) <= 32) in type synonym int('n) with (0 <= 'n & 'n <= 33) +Type error: +[[96mexist_synonym/v1.sail[0m]:6:41-42 +6[96m |[0mlet x : {'n, 0 <= 'n <= 33. regno('n)} = 4 + [91m |[0m [91m^[0m + [91m |[0m Tried performing type coercion from int(4) to {('n : Int), (0 <= 'n & 'n <= 33). regno('n)} on 4 + [91m |[0m Coercion failed because: + [91m |[0m Could not prove constraints (0 <= 'n & ('n + 1) <= 32) in type synonym int('n) with (0 <= 'n & 'n <= 33) + [91m |[0m diff --git a/test/typecheck/pass/exist_synonym/v2.expect b/test/typecheck/pass/exist_synonym/v2.expect index 5bde04ba..c01d8359 100644 --- a/test/typecheck/pass/exist_synonym/v2.expect +++ b/test/typecheck/pass/exist_synonym/v2.expect @@ -1,6 +1,8 @@ -Type error at file "exist_synonym/v2.sail", line 6, character 41 to line 6, character 41 - -let x : {'n, 0 <= 'n <= 8. regno('n)} = [41m4[0m - -Tried performing type coercion from int(4) to {'n, (0 <= 'n & 'n <= 8). regno('n)} on 4 -Coercion failed because: Could not prove constraints (0 <= 'n & ('n + 1) <= 2) in type synonym int('n) with (0 <= 'n & 'n <= 8) +Type error: +[[96mexist_synonym/v2.sail[0m]:6:40-41 +6[96m |[0mlet x : {'n, 0 <= 'n <= 8. regno('n)} = 4 + [91m |[0m [91m^[0m + [91m |[0m Tried performing type coercion from int(4) to {('n : Int), (0 <= 'n & 'n <= 8). regno('n)} on 4 + [91m |[0m Coercion failed because: + [91m |[0m Could not prove constraints (0 <= 'n & ('n + 1) <= 2) in type synonym int('n) with (0 <= 'n & 'n <= 8) + [91m |[0m diff --git a/test/typecheck/pass/exist_synonym/v3.expect b/test/typecheck/pass/exist_synonym/v3.expect index a647ef00..c237ae2d 100644 --- a/test/typecheck/pass/exist_synonym/v3.expect +++ b/test/typecheck/pass/exist_synonym/v3.expect @@ -1,3 +1,3 @@ -Type error at no location information available +Type error: +Could not prove constraints (0 <= 'n & ('n + 1) <= 32) in type synonym int('n) with (0 <= 'n & 'n <= 100), (0 <= '_x & '_x <= 8), (0 <= '_x#0 & '_x#0 <= 8) -Could not prove constraints (0 <= 'n & ('n + 1) <= 32) in type synonym int('n) with (0 <= 'n & 'n <= 100), (0 <= 'ex3#n & 'ex3#n <= 8), (0 <= 'ex2#n & 'ex2#n <= 8) diff --git a/test/typecheck/pass/exist_synonym/v4.expect b/test/typecheck/pass/exist_synonym/v4.expect index d8bad777..abb232cb 100644 --- a/test/typecheck/pass/exist_synonym/v4.expect +++ b/test/typecheck/pass/exist_synonym/v4.expect @@ -1,3 +1,3 @@ -Type error at no location information available +Type error: +Could not prove constraints (0 <= 'n & ('n + 1) <= 32) in type synonym int('n) with (0 <= '_x & '_x <= 8), (0 <= '_x#0 & '_x#0 <= 8) -Could not prove constraints (0 <= 'n & ('n + 1) <= 32) in type synonym int('n) with (0 <= 2 & 2 <= 4), (0 <= 'ex3#n & 'ex3#n <= 8), (0 <= 'ex2#n & 'ex2#n <= 8) diff --git a/test/typecheck/pass/foreach_var_updates.sail b/test/typecheck/pass/foreach_var_updates.sail index 7813cb16..347a9b3a 100644 --- a/test/typecheck/pass/foreach_var_updates.sail +++ b/test/typecheck/pass/foreach_var_updates.sail @@ -1,3 +1,5 @@ +$include <flow.sail> + val add_int = {ocaml: "add", lem: "integerAdd"}: (int, int) -> int overload operator + = {add_int} diff --git a/test/typecheck/pass/function_namespace/v1.expect b/test/typecheck/pass/function_namespace/v1.expect index 6e40adc0..2bb734aa 100644 --- a/test/typecheck/pass/function_namespace/v1.expect +++ b/test/typecheck/pass/function_namespace/v1.expect @@ -1,5 +1,6 @@ -Type error at file "function_namespace/v1.sail", line 9, character 7 to line 9, character 10 - - let [41mtest[0m = true; - -Local variable test is already bound as a function name +Type error: +[[96mfunction_namespace/v1.sail[0m]:9:6-10 +9[96m |[0m let test = true; + [91m |[0m [91m^--^[0m + [91m |[0m Local variable test is already bound as a function name + [91m |[0m diff --git a/test/typecheck/pass/global_type_var/v1.expect b/test/typecheck/pass/global_type_var/v1.expect index e81c467e..ac4428c6 100644 --- a/test/typecheck/pass/global_type_var/v1.expect +++ b/test/typecheck/pass/global_type_var/v1.expect @@ -1,24 +1,12 @@ -Type error at file "global_type_var/v1.sail", line 23, character 14 to line 23, character 15 - -let _ = test([41m32[0m) - -Tried performing type coercion from int(32) to int('size) on 32 -Coercion failed because: - int(32) is not a subtype of int('size) - in context - * 'size == 'ex14# - * ('ex14# == 32 | 'ex14# == 64) - * ('ex13# == 32 | 'ex13# == 64) - where - * 'ex13# bound at file "global_type_var/v1.sail", line 5, character 5 to line 5, character 32 - -let [41m(size as 'size) : {|32, 64|}[0m = 32 - - * 'ex14# bound at file "global_type_var/v1.sail", line 5, character 6 to line 5, character 18 - -let ([41msize as 'size[0m) : {|32, 64|} = 32 - - * 'size bound at file "global_type_var/v1.sail", line 5, character 14 to line 5, character 18 - -let (size as [41m'size[0m) : {|32, 64|} = 32 - +Type error: +[[96mglobal_type_var/v1.sail[0m]:23:13-15 +23[96m |[0mlet _ = test(32) + [91m |[0m [91m^^[0m + [91m |[0m Tried performing type coercion from int(32) to int('size) on 32 + [91m |[0m Coercion failed because: + [91m |[0m int(32) is not a subtype of int('size) + [91m |[0m [[96mglobal_type_var/v1.sail[0m]:5:13-18 + [91m |[0m 5[96m |[0mlet (size as 'size) : {|32, 64|} = 32 + [91m |[0m [93m |[0m [93m^---^[0m + [91m |[0m [93m |[0m 'size bound here + [91m |[0m diff --git a/test/typecheck/pass/global_type_var/v2.expect b/test/typecheck/pass/global_type_var/v2.expect index 21c4b348..93eb628b 100644 --- a/test/typecheck/pass/global_type_var/v2.expect +++ b/test/typecheck/pass/global_type_var/v2.expect @@ -1,24 +1,12 @@ -Type error at file "global_type_var/v2.sail", line 23, character 14 to line 23, character 15 - -let _ = test([41m64[0m) - -Tried performing type coercion from int(64) to int('size) on 64 -Coercion failed because: - int(64) is not a subtype of int('size) - in context - * 'size == 'ex14# - * ('ex14# == 32 | 'ex14# == 64) - * ('ex13# == 32 | 'ex13# == 64) - where - * 'ex13# bound at file "global_type_var/v2.sail", line 5, character 5 to line 5, character 32 - -let [41m(size as 'size) : {|32, 64|}[0m = 32 - - * 'ex14# bound at file "global_type_var/v2.sail", line 5, character 6 to line 5, character 18 - -let ([41msize as 'size[0m) : {|32, 64|} = 32 - - * 'size bound at file "global_type_var/v2.sail", line 5, character 14 to line 5, character 18 - -let (size as [41m'size[0m) : {|32, 64|} = 32 - +Type error: +[[96mglobal_type_var/v2.sail[0m]:23:13-15 +23[96m |[0mlet _ = test(64) + [91m |[0m [91m^^[0m + [91m |[0m Tried performing type coercion from int(64) to int('size) on 64 + [91m |[0m Coercion failed because: + [91m |[0m int(64) is not a subtype of int('size) + [91m |[0m [[96mglobal_type_var/v2.sail[0m]:5:13-18 + [91m |[0m 5[96m |[0mlet (size as 'size) : {|32, 64|} = 32 + [91m |[0m [93m |[0m [93m^---^[0m + [91m |[0m [93m |[0m 'size bound here + [91m |[0m diff --git a/test/typecheck/pass/global_type_var/v3.expect b/test/typecheck/pass/global_type_var/v3.expect index 43096686..6def5172 100644 --- a/test/typecheck/pass/global_type_var/v3.expect +++ b/test/typecheck/pass/global_type_var/v3.expect @@ -1,5 +1,12 @@ -Type error at file "global_type_var/v3.sail", line 9, character 19 to line 9, character 23 - -val test : forall [41m'size[0m. atom('size) -> unit - -type variable ('size : Int) is already bound +Type error: +[[96mglobal_type_var/v3.sail[0m]:15:23-27 +15[96m |[0m let y : atom(64) = size in + [91m |[0m [91m^--^[0m + [91m |[0m Tried performing type coercion from int('_size) to int(64) on size + [91m |[0m Coercion failed because: + [91m |[0m int('_size) is not a subtype of int(64) + [91m |[0m [[96mglobal_type_var/v3.sail[0m]:5:5-18 + [91m |[0m 5[96m |[0mlet (size as 'size) : {|32, 64|} = 32 + [91m |[0m [93m |[0m [93m^-----------^[0m + [91m |[0m [93m |[0m '_size bound here + [91m |[0m diff --git a/test/typecheck/pass/if_infer/v1.expect b/test/typecheck/pass/if_infer/v1.expect index 95073799..c8217478 100644 --- a/test/typecheck/pass/if_infer/v1.expect +++ b/test/typecheck/pass/if_infer/v1.expect @@ -1,17 +1,12 @@ -Type error at file "if_infer/v1.sail", line 10, character 11 to line 10, character 37 - - let _ = [41m0b100[if R then 0 else f()][0m; - -No overloadings for vector_access, tried: - bitvector_access: - Could not resolve quantifiers for bitvector_access (0 <= 'ex42#ex41# & ('ex42#ex41# + 1) <= 3) - - Try adding named type variables for - - - plain_vector_access: - Could not resolve quantifiers for plain_vector_access (0 <= 'ex45#ex44# & ('ex45#ex44# + 1) <= 3) - - Try adding named type variables for - - +Type error: +[[96mif_infer/v1.sail[0m]:10:10-37 +10[96m |[0m let _ = 0b100[if R then 0 else f()]; + [91m |[0m [91m^-------------------------^[0m + [91m |[0m No overloading for vector_access, tried: + [91m |[0m [94m*[0m bitvector_access + [91m |[0m Could not resolve quantifiers for bitvector_access + [91m |[0m [94m*[0m (0 <= 'ex40# & ('ex40# + 1) <= 3) + [91m |[0m [94m*[0m plain_vector_access + [91m |[0m Could not resolve quantifiers for plain_vector_access + [91m |[0m [94m*[0m (0 <= 'ex43# & ('ex43# + 1) <= 3) + [91m |[0m diff --git a/test/typecheck/pass/if_infer/v2.expect b/test/typecheck/pass/if_infer/v2.expect index afa04343..f0c2fab3 100644 --- a/test/typecheck/pass/if_infer/v2.expect +++ b/test/typecheck/pass/if_infer/v2.expect @@ -1,17 +1,12 @@ -Type error at file "if_infer/v2.sail", line 10, character 11 to line 10, character 38 - - let _ = [41m0b1001[if R then 0 else f()][0m; - -No overloadings for vector_access, tried: - bitvector_access: - Could not resolve quantifiers for bitvector_access (0 <= 'ex42#ex41# & ('ex42#ex41# + 1) <= 4) - - Try adding named type variables for - - - plain_vector_access: - Could not resolve quantifiers for plain_vector_access (0 <= 'ex45#ex44# & ('ex45#ex44# + 1) <= 4) - - Try adding named type variables for - - +Type error: +[[96mif_infer/v2.sail[0m]:10:10-38 +10[96m |[0m let _ = 0b1001[if R then 0 else f()]; + [91m |[0m [91m^--------------------------^[0m + [91m |[0m No overloading for vector_access, tried: + [91m |[0m [94m*[0m bitvector_access + [91m |[0m Could not resolve quantifiers for bitvector_access + [91m |[0m [94m*[0m (0 <= 'ex40# & ('ex40# + 1) <= 4) + [91m |[0m [94m*[0m plain_vector_access + [91m |[0m Could not resolve quantifiers for plain_vector_access + [91m |[0m [94m*[0m (0 <= 'ex43# & ('ex43# + 1) <= 4) + [91m |[0m diff --git a/test/typecheck/pass/if_infer/v3.expect b/test/typecheck/pass/if_infer/v3.expect index 8b149bc8..7e0e74bb 100644 --- a/test/typecheck/pass/if_infer/v3.expect +++ b/test/typecheck/pass/if_infer/v3.expect @@ -1,7 +1,10 @@ -Type error at file "if_infer/v3.sail", line 10, character 11 to line 10, character 38 - - let _ = [41m0b1001[if R then 0 else f()][0m; - -No overloadings for vector_access, tried: - bitvector_access: Numeric type is non-simple - plain_vector_access: Numeric type is non-simple +Type error: +[[96mif_infer/v3.sail[0m]:10:10-38 +10[96m |[0m let _ = 0b1001[if R then 0 else f()]; + [91m |[0m [91m^--------------------------^[0m + [91m |[0m No overloading for vector_access, tried: + [91m |[0m [94m*[0m bitvector_access + [91m |[0m Numeric type is non-simple + [91m |[0m [94m*[0m plain_vector_access + [91m |[0m Numeric type is non-simple + [91m |[0m diff --git a/test/typecheck/pass/implicits.sail b/test/typecheck/pass/implicits.sail new file mode 100644 index 00000000..2923fab4 --- /dev/null +++ b/test/typecheck/pass/implicits.sail @@ -0,0 +1,45 @@ +default Order dec + +$include <prelude.sail> + +val EXTZ : forall 'n 'm, 0 <= 'n <= 'm. (implicit('m), bits('n)) -> bits('m) + +function EXTZ(m, x) = sail_zero_extend(x, m) + +val EXTS : forall 'n 'm, 0 <= 'n <= 'm. (implicit('m), bits('n)) -> bits('m) + +function EXTS(m, x) = sail_sign_extend(x, m) + +val zeros : forall 'n, 'n >= 0. implicit('n) -> bits('n) + +function zeros(n) = replicate_bits(0b0, n) + +val dzeros : forall 'n 'm, 'n >= 0 & 'm >= 0. (implicit('n), implicit('m)) -> (bits('n), bits('m)) + +function dzeros(n, m) = (zeros(n), zeros(m)) + +val dzeros2 : forall 'n 'm, 'n >= 0 & 'm >= 0. (implicit('n), implicit('m), unit) -> (bits('n), bits('m)) + +function dzeros2(n, m, _) = (zeros(n), zeros(m)) + +function main((): unit) -> unit = { + let a: bits(64) = EXTZ(0xFF); + let b: bits(64) = EXTS(0xFF); + let c: bits(64) = EXTS(64, 0xFF); + let d: bits(64) = zeros(); + let e: bits(64) = zeros(64); + let (f, g): (bits(64), bits(32)) = dzeros(); + let (h, i) = dzeros(16, 8); + let (j, k): (bits(4), bits(2)) = dzeros2(); + print_bits("a = ", a); + print_bits("b = ", b); + print_bits("c = ", c); + print_bits("d = ", d); + print_bits("e = ", e); + print_bits("f = ", f); + print_bits("g = ", g); + print_bits("h = ", h); + print_bits("i = ", i); + print_bits("j = ", j); + print_bits("k = ", k) +}
\ No newline at end of file diff --git a/test/typecheck/pass/implicits/v1.expect b/test/typecheck/pass/implicits/v1.expect new file mode 100644 index 00000000..f1711d54 --- /dev/null +++ b/test/typecheck/pass/implicits/v1.expect @@ -0,0 +1,6 @@ +Type error: +[[96mimplicits/v1.sail[0m]:9:51-63 +9[96m |[0mval EXTS : forall 'n 'm, 0 <= 'n <= 'm. (bits('n), implicit('m)) -> bits('m) + [91m |[0m [91m^----------^[0m + [91m |[0m Arguments are invalid, implicit arguments must come before all other arguments + [91m |[0m diff --git a/test/typecheck/pass/implicits/v1.sail b/test/typecheck/pass/implicits/v1.sail new file mode 100644 index 00000000..661ff309 --- /dev/null +++ b/test/typecheck/pass/implicits/v1.sail @@ -0,0 +1,29 @@ +default Order dec + +$include <prelude.sail> + +val EXTZ : forall 'n 'm, 0 <= 'n <= 'm. (implicit('m), bits('n)) -> bits('m) + +function EXTZ(m, x) = sail_zero_extend(x, m) + +val EXTS : forall 'n 'm, 0 <= 'n <= 'm. (bits('n), implicit('m)) -> bits('m) + +function EXTS(x, m) = sail_sign_extend(x, m) + +val zeros : forall 'n, 'n >= 0. implicit('n) -> bits('n) + +function zeros(n) = replicate_bits(0b0, n) + +function main((): unit) -> unit = { + let a: bits(64) = EXTZ(0xFF); + let b: bits(64) = EXTS(0xFF); + let c: bits(64) = EXTS(0xFF, 64); + let d: bits(64) = zeros(); + let e: bits(64) = zeros(64); + print_bits("a = ", a); + print_bits("b = ", b); + print_bits("c = ", c); + print_bits("d = ", d); + print_bits("e = ", e); + () +}
\ No newline at end of file diff --git a/test/typecheck/pass/implicits/v2.expect b/test/typecheck/pass/implicits/v2.expect new file mode 100644 index 00000000..11ffeace --- /dev/null +++ b/test/typecheck/pass/implicits/v2.expect @@ -0,0 +1,6 @@ +Type error: +[[96mimplicits/v2.sail[0m]:5:50-56 +5[96m |[0mval EXTZ : forall 'n 'm, 0 <= 'n <= 'm. (implicit('m - 1), bits('n)) -> bits('m) + [91m |[0m [91m^----^[0m + [91m |[0m Implicit argument must contain a single type variable + [91m |[0m diff --git a/test/typecheck/pass/implicits/v2.sail b/test/typecheck/pass/implicits/v2.sail new file mode 100644 index 00000000..4040aa0c --- /dev/null +++ b/test/typecheck/pass/implicits/v2.sail @@ -0,0 +1,18 @@ +default Order dec + +$include <prelude.sail> + +val EXTZ : forall 'n 'm, 0 <= 'n <= 'm. (implicit('m - 1), bits('n)) -> bits('m) + +function EXTZ(m, x) = sail_zero_extend(x, m) + +val EXTS : forall 'n 'm, 0 <= 'n <= 'm. (implicit('m), bits('n)) -> bits('m) + +function EXTS(m, x) = sail_sign_extend(x, m) + +function main((): unit) -> unit = { + let a: bits(64) = EXTZ(0xFF); + let b: bits(64) = EXTS(0xFF); + print_bits("a = ", a); + print_bits("b = ", b) +}
\ No newline at end of file diff --git a/test/typecheck/pass/lt_flow.sail b/test/typecheck/pass/lt_flow.sail new file mode 100644 index 00000000..4e7572da --- /dev/null +++ b/test/typecheck/pass/lt_flow.sail @@ -0,0 +1,5 @@ +val lt_flow : forall 'n 'm. (int('n), int('m)) -> bool('n <= 'm) + +val test : unit -> bool(true) + +function test() = lt_flow(1,10) diff --git a/test/typecheck/pass/mutrec.sail b/test/typecheck/pass/mutrec.sail new file mode 100644 index 00000000..26dbf729 --- /dev/null +++ b/test/typecheck/pass/mutrec.sail @@ -0,0 +1,12 @@ +$include <prelude.sail> + +val f : list(int) -> int +val g : list(int) -> int + +function f([| |]) = 0 +and f(h::t) = h + g(t) +function g([||]) = 0 +and g(h::t) = f(t) - h + +val test : unit -> int +function test() = f([|1,2,3|]) diff --git a/test/typecheck/pass/nexp_synonym.sail b/test/typecheck/pass/nexp_synonym.sail new file mode 100644 index 00000000..b908b265 --- /dev/null +++ b/test/typecheck/pass/nexp_synonym.sail @@ -0,0 +1,11 @@ +default Order dec + +$include <prelude.sail> + +type LEN : Int = 32 + +let v : bits(LEN) = 0xFFFF_FFFF + +function main((): unit) -> unit = { + print_bits("v = ", v) +}
\ No newline at end of file diff --git a/test/typecheck/pass/nexp_synonym/v1.expect b/test/typecheck/pass/nexp_synonym/v1.expect new file mode 100644 index 00000000..9ba21c2c --- /dev/null +++ b/test/typecheck/pass/nexp_synonym/v1.expect @@ -0,0 +1,8 @@ +Type error: +[[96mnexp_synonym/v1.sail[0m]:7:20-31 +7[96m |[0mlet v : bits(LEN) = 0xFFFF_FFFF + [91m |[0m [91m^---------^[0m + [91m |[0m Tried performing type coercion from vector(32, dec, bit) to bits(LEN) on 0xFFFFFFFF + [91m |[0m Coercion failed because: + [91m |[0m Mismatched argument types in subtype check + [91m |[0m diff --git a/test/typecheck/pass/nexp_synonym/v1.sail b/test/typecheck/pass/nexp_synonym/v1.sail new file mode 100644 index 00000000..96690e00 --- /dev/null +++ b/test/typecheck/pass/nexp_synonym/v1.sail @@ -0,0 +1,11 @@ +default Order dec + +$include <prelude.sail> + +type LEN : Int = 33 + +let v : bits(LEN) = 0xFFFF_FFFF + +function main((): unit) -> unit = { + print_bits("v = ", v) +} diff --git a/test/typecheck/pass/nexp_synonym/v2.expect b/test/typecheck/pass/nexp_synonym/v2.expect new file mode 100644 index 00000000..68d664f7 --- /dev/null +++ b/test/typecheck/pass/nexp_synonym/v2.expect @@ -0,0 +1,8 @@ +Type error: +[[96mnexp_synonym/v2.sail[0m]:7:20-32 +7[96m |[0mlet v : bits(LEN) = 0xFFFF_FFFFF + [91m |[0m [91m^----------^[0m + [91m |[0m Tried performing type coercion from vector(36, dec, bit) to bits(LEN) on 0xFFFFFFFFF + [91m |[0m Coercion failed because: + [91m |[0m Mismatched argument types in subtype check + [91m |[0m diff --git a/test/typecheck/pass/nexp_synonym/v2.sail b/test/typecheck/pass/nexp_synonym/v2.sail new file mode 100644 index 00000000..0c1b5b5b --- /dev/null +++ b/test/typecheck/pass/nexp_synonym/v2.sail @@ -0,0 +1,11 @@ +default Order dec + +$include <prelude.sail> + +type LEN : Int = 32 + +let v : bits(LEN) = 0xFFFF_FFFFF + +function main((): unit) -> unit = { + print_bits("v = ", v) +} diff --git a/test/typecheck/pass/nexp_synonym2.sail b/test/typecheck/pass/nexp_synonym2.sail new file mode 100644 index 00000000..9e9bd7b8 --- /dev/null +++ b/test/typecheck/pass/nexp_synonym2.sail @@ -0,0 +1,15 @@ +default Order dec + +$include <prelude.sail> + +type LEN : Int = 30 + 2 + +type V : Type = bits(LEN) + +type V2('n: Int) -> Type = bits('n) + +let v : V = 0xFFFF_FFFF + +function main((): unit) -> unit = { + print_bits("v = ", v : V2(LEN)) +} diff --git a/test/typecheck/pass/not_pattern/v1.expect b/test/typecheck/pass/not_pattern/v1.expect index 9de82d1f..aeefb901 100644 --- a/test/typecheck/pass/not_pattern/v1.expect +++ b/test/typecheck/pass/not_pattern/v1.expect @@ -1,5 +1,6 @@ -Type error at file "not_pattern/v1.sail", line 12, character 7 to line 12, character 7 - - ~([41my[0m) => (), - -Bindings are not allowed in this context +Type error: +[[96mnot_pattern/v1.sail[0m]:12:6-7 +12[96m |[0m ~(y) => (), + [91m |[0m [91m^[0m + [91m |[0m Bindings are not allowed in this context + [91m |[0m diff --git a/test/typecheck/pass/patternrefinement.sail b/test/typecheck/pass/patternrefinement.sail index 86294543..4433a2c3 100644 --- a/test/typecheck/pass/patternrefinement.sail +++ b/test/typecheck/pass/patternrefinement.sail @@ -12,7 +12,7 @@ val eq_vec = {ocaml: "eq_vec", lem: "eq_vec"}: forall ('m : Int) ('ord : Order). (vector('m, 'ord, bit), vector('m, 'ord, bit)) -> bool val eq_int = {ocaml: "eq_atom", lem: "eq"}: forall ('n : Int) ('m : Int). - (int('n), int('m)) -> bool + (int('n), int('m)) -> bool('n == 'm) val eq = {ocaml: "eq", lem: "eq"}: forall ('a : Type). ('a, 'a) -> bool diff --git a/test/typecheck/pass/phantom_num.sail b/test/typecheck/pass/phantom_num.sail index 96663073..6be3533f 100644 --- a/test/typecheck/pass/phantom_num.sail +++ b/test/typecheck/pass/phantom_num.sail @@ -1,9 +1,13 @@ +function __id forall 'n. (x: int('n)) -> int('n) = x + +overload __size = {__id} + val gt_int = {ocaml: "gt", lem: "gt"}: (int, int) -> bool overload operator > = {gt_int} register z : int -val test : forall ('n : Int). unit -> unit effect {wreg} +val test : forall ('n : Int). (implicit('n), unit) -> unit effect {wreg} -function test () = if 'n > 3 then z = 0 else z = 1 +function test(n, _) = if 'n > 3 then z = 0 else z = 1 diff --git a/test/typecheck/pass/reg_32_64.sail b/test/typecheck/pass/reg_32_64.sail new file mode 100644 index 00000000..79dfc862 --- /dev/null +++ b/test/typecheck/pass/reg_32_64.sail @@ -0,0 +1,39 @@ +default Order dec + +$include <prelude.sail> + +val "reg_deref" : forall ('a : Type). register('a) -> 'a effect {rreg} + +register R0 : bits(64) +register R1 : bits(64) +register R2 : bits(64) +register R3 : bits(64) + +let GPRs : vector(4, dec, register(bits(64))) = [ref R3, ref R2, ref R1, ref R0] + +type regno('r: Int) -> Bool = 0 <= 'r <= 3 + +val set_R : forall 'r 'd, regno('r) & 'd in {32, 64}. + (int('r), bits('d)) -> unit effect {wreg} + +function set_R(r, data) = { + let R = GPRs[r]; + (*R)['d - 1 .. 0] = data +} + +val get_R : forall 'r 'd, regno('r) & 'd in {32, 64}. + (implicit('d), int('r)) -> bits('d) effect {rreg} + +function get_R(datasize, r) = { + let R = GPRs[r]; + reg_deref(R)[datasize - 1 .. 0] +} + +overload R = {set_R, get_R} + +function main() -> unit = { + R(0) = 0xCAFE_CAFE_0000_0000; + R(0) = 0xFFFF_FFFF; + print_bits("R = ", R(0) : bits(64)); + print_bits("R = ", R(0) : bits(32)) +} diff --git a/test/typecheck/pass/reg_32_64/v1.expect b/test/typecheck/pass/reg_32_64/v1.expect new file mode 100644 index 00000000..eb398991 --- /dev/null +++ b/test/typecheck/pass/reg_32_64/v1.expect @@ -0,0 +1,11 @@ +Type error: +[[96mreg_32_64/v1.sail[0m]:35:9-28 +35[96m |[0m R(0) = 0xCAFE_CAFE_0000_00; + [91m |[0m [91m^-----------------^[0m + [91m |[0m No overloading for R, tried: + [91m |[0m [94m*[0m set_R + [91m |[0m Could not resolve quantifiers for set_R + [91m |[0m [94m*[0m (regno(0) & (56 == 32 | 56 == 64)) + [91m |[0m [94m*[0m get_R + [91m |[0m No valid casts resulted in unification + [91m |[0m diff --git a/test/typecheck/pass/reg_32_64/v1.sail b/test/typecheck/pass/reg_32_64/v1.sail new file mode 100644 index 00000000..8c0e980b --- /dev/null +++ b/test/typecheck/pass/reg_32_64/v1.sail @@ -0,0 +1,39 @@ +default Order dec + +$include <prelude.sail> + +val "reg_deref" : forall ('a : Type). register('a) -> 'a effect {rreg} + +register R0 : bits(64) +register R1 : bits(64) +register R2 : bits(64) +register R3 : bits(64) + +let GPRs : vector(4, dec, register(bits(64))) = [ref R3, ref R2, ref R1, ref R0] + +type regno('r: Int) -> Bool = 0 <= 'r <= 3 + +val set_R : forall 'r 'd, regno('r) & 'd in {32, 64}. + (int('r), bits('d)) -> unit effect {wreg} + +function set_R(r, data) = { + let R = GPRs[r]; + (*R)['d - 1 .. 0] = data +} + +val get_R : forall 'r 'd, regno('r) & 'd in {32, 64}. + (implicit('d), int('r)) -> bits('d) effect {rreg} + +function get_R(datasize, r) = { + let R = GPRs[r]; + reg_deref(R)[datasize - 1 .. 0] +} + +overload R = {set_R, get_R} + +function main() -> unit = { + R(0) = 0xCAFE_CAFE_0000_00; + R(0) = 0xFFFF_FFFF; + print_bits("R = ", R(0) : bits(64)); + print_bits("R = ", R(0) : bits(32)) +} diff --git a/test/typecheck/pass/reg_32_64/v2.expect b/test/typecheck/pass/reg_32_64/v2.expect new file mode 100644 index 00000000..f007c917 --- /dev/null +++ b/test/typecheck/pass/reg_32_64/v2.expect @@ -0,0 +1,13 @@ +Type error: +[[96mreg_32_64/v2.sail[0m]:21:18-22 +21[96m |[0m (*R)['d .. 0] = data + [91m |[0m [91m^--^[0m + [91m |[0m Tried performing type coercion from vector('d, dec, bit) to vector((('d - 0) + 1), dec, bit) on data + [91m |[0m Coercion failed because: + [91m |[0m Mismatched argument types in subtype check + [91m |[0m This error occured because of a previous error: + [91m |[0m [[96mreg_32_64/v2.sail[0m]:21:2-15 + [91m |[0m 21[96m |[0m (*R)['d .. 0] = data + [91m |[0m [91m |[0m [91m^-----------^[0m + [91m |[0m [91m |[0m Mismatched argument types in subtype check + [91m |[0m diff --git a/test/typecheck/pass/reg_32_64/v2.sail b/test/typecheck/pass/reg_32_64/v2.sail new file mode 100644 index 00000000..64daea4a --- /dev/null +++ b/test/typecheck/pass/reg_32_64/v2.sail @@ -0,0 +1,39 @@ +default Order dec + +$include <prelude.sail> + +val "reg_deref" : forall ('a : Type). register('a) -> 'a effect {rreg} + +register R0 : bits(64) +register R1 : bits(64) +register R2 : bits(64) +register R3 : bits(64) + +let GPRs : vector(4, dec, register(bits(64))) = [ref R3, ref R2, ref R1, ref R0] + +type regno('r: Int) -> Bool = 0 <= 'r <= 3 + +val set_R : forall 'r 'd, regno('r) & 'd in {32, 64}. + (int('r), bits('d)) -> unit effect {wreg} + +function set_R(r, data) = { + let R = GPRs[r]; + (*R)['d .. 0] = data +} + +val get_R : forall 'r 'd, regno('r) & 'd in {32, 64}. + (implicit('d), int('r)) -> bits('d) effect {rreg} + +function get_R(datasize, r) = { + let R = GPRs[r]; + reg_deref(R)[datasize - 1 .. 0] +} + +overload R = {set_R, get_R} + +function main() -> unit = { + R(0) = 0xCAFE_CAFE_0000_0000; + R(0) = 0xFFFF_FFFF; + print_bits("R = ", R(0) : bits(64)); + print_bits("R = ", R(0) : bits(32)) +} diff --git a/test/typecheck/pass/reg_32_64/v3.expect b/test/typecheck/pass/reg_32_64/v3.expect new file mode 100644 index 00000000..cea45127 --- /dev/null +++ b/test/typecheck/pass/reg_32_64/v3.expect @@ -0,0 +1,10 @@ +Type error: +[[96mreg_32_64/v3.sail[0m]:29:15-21 +29[96m |[0m reg_deref(R)['d - 1 .. 0] + [91m |[0m [91m^----^[0m + [91m |[0m No overloading for (operator -), tried: + [91m |[0m [94m*[0m sub_atom + [91m |[0m Cannot re-write sizeof('d) + [91m |[0m [94m*[0m sub_int + [91m |[0m Cannot re-write sizeof('d) + [91m |[0m diff --git a/test/typecheck/pass/reg_32_64/v3.sail b/test/typecheck/pass/reg_32_64/v3.sail new file mode 100644 index 00000000..dda787ab --- /dev/null +++ b/test/typecheck/pass/reg_32_64/v3.sail @@ -0,0 +1,39 @@ +default Order dec + +$include <prelude.sail> + +val "reg_deref" : forall ('a : Type). register('a) -> 'a effect {rreg} + +register R0 : bits(64) +register R1 : bits(64) +register R2 : bits(64) +register R3 : bits(64) + +let GPRs : vector(4, dec, register(bits(64))) = [ref R3, ref R2, ref R1, ref R0] + +type regno('r: Int) -> Bool = 0 <= 'r <= 3 + +val set_R : forall 'r 'd, regno('r) & 'd in {32, 64}. + (int('r), bits('d)) -> unit effect {wreg} + +function set_R(r, data) = { + let R = GPRs[r]; + (*R)['d - 1 .. 0] = data +} + +val get_R : forall 'r 'd, regno('r) & 'd in {32, 64}. + (implicit('d), int('r)) -> bits('d) effect {rreg} + +function get_R(_, r) = { + let R = GPRs[r]; + reg_deref(R)['d - 1 .. 0] +} + +overload R = {set_R, get_R} + +function main() -> unit = { + R(0) = 0xCAFE_CAFE_0000_0000; + R(0) = 0xFFFF_FFFF; + print_bits("R = ", R(0) : bits(64)); + print_bits("R = ", R(0) : bits(32)) +} diff --git a/test/typecheck/pass/return_simple3.sail b/test/typecheck/pass/return_simple3.sail index fdda96dc..5653cb51 100644 --- a/test/typecheck/pass/return_simple3.sail +++ b/test/typecheck/pass/return_simple3.sail @@ -1,6 +1,10 @@ -val return_test : forall ('N : Int), 'N >= 10. range(10, 'N) -> range(10, 'N) +function __id forall 'n. (x: int('n)) -> int('n) = x -function return_test x = { +overload __size = {__id} + +val return_test : forall ('N : Int), 'N >= 10. (implicit('N), range(10, 'N)) -> range(10, 'N) + +function return_test(N, x) = { return(x); 'N } diff --git a/test/typecheck/pass/tautology.sail b/test/typecheck/pass/tautology.sail index f1c8bade..43c7ddc9 100644 --- a/test/typecheck/pass/tautology.sail +++ b/test/typecheck/pass/tautology.sail @@ -1,3 +1,4 @@ +$include <flow.sail> type implies('p: Bool, 'q: Bool) -> Bool = not('p) | 'q diff --git a/test/typecheck/pass/true_false.sail b/test/typecheck/pass/true_false.sail new file mode 100644 index 00000000..42b175d8 --- /dev/null +++ b/test/typecheck/pass/true_false.sail @@ -0,0 +1,11 @@ +default Order dec + +$include <prelude.sail> + +function main((): unit) -> unit = { + let x: bool(false) = false; + let y: bool(true) = true; + _check(x : bool); + _check(x : bool(false)); + _not_check(x : bool(true)) +} diff --git a/test/typecheck/pass/tyvar_shadow.sail b/test/typecheck/pass/tyvar_shadow.sail new file mode 100644 index 00000000..973aa916 --- /dev/null +++ b/test/typecheck/pass/tyvar_shadow.sail @@ -0,0 +1,14 @@ +default Order dec + +$include <prelude.sail> + +function main((): unit) -> unit = { + let x as int('x) = 3; + let x as int('x) = 4; + _prove(constraint('x + 'x == 8)); + _not_prove(constraint('x + 'x == 6 | 'x + 'x == 7)); + + let y : {'n, 'n == 3. int('n)} = 3; + _prove(constraint('_y == 3)) +} + diff --git a/test/typecheck/pass/vec_length/v1.expect b/test/typecheck/pass/vec_length/v1.expect index 68a4ca70..ce61cf2a 100644 --- a/test/typecheck/pass/vec_length/v1.expect +++ b/test/typecheck/pass/vec_length/v1.expect @@ -1,13 +1,12 @@ -Type error at file "vec_length/v1.sail", line 6, character 11 to line 6, character 15 - - let y = [41mx[10][0m; - -No overloadings for vector_access, tried: - bitvector_access: - Could not resolve quantifiers for bitvector_access (0 <= 10 & (10 + 1) <= 8) - - Try adding the constraint: (0 <= 10 & (10 + 1) <= 8) - plain_vector_access: - Could not resolve quantifiers for plain_vector_access (0 <= 10 & (10 + 1) <= 8) - - Try adding the constraint: (0 <= 10 & (10 + 1) <= 8) +Type error: +[[96mvec_length/v1.sail[0m]:6:10-15 +6[96m |[0m let y = x[10]; + [91m |[0m [91m^---^[0m + [91m |[0m No overloading for vector_access, tried: + [91m |[0m [94m*[0m bitvector_access + [91m |[0m Could not resolve quantifiers for bitvector_access + [91m |[0m [94m*[0m (0 <= 10 & (10 + 1) <= 8) + [91m |[0m [94m*[0m plain_vector_access + [91m |[0m Could not resolve quantifiers for plain_vector_access + [91m |[0m [94m*[0m (0 <= 10 & (10 + 1) <= 8) + [91m |[0m diff --git a/test/typecheck/pass/vec_length/v1_inc.expect b/test/typecheck/pass/vec_length/v1_inc.expect index 7ce8fd99..3d40cdb0 100644 --- a/test/typecheck/pass/vec_length/v1_inc.expect +++ b/test/typecheck/pass/vec_length/v1_inc.expect @@ -1,13 +1,12 @@ -Type error at file "vec_length/v1_inc.sail", line 6, character 11 to line 6, character 15 - - let y = [41mx[10][0m; - -No overloadings for vector_access, tried: - bitvector_access: - Could not resolve quantifiers for bitvector_access (0 <= 10 & (10 + 1) <= 8) - - Try adding the constraint: (0 <= 10 & (10 + 1) <= 8) - plain_vector_access: - Could not resolve quantifiers for plain_vector_access (0 <= 10 & (10 + 1) <= 8) - - Try adding the constraint: (0 <= 10 & (10 + 1) <= 8) +Type error: +[[96mvec_length/v1_inc.sail[0m]:6:10-15 +6[96m |[0m let y = x[10]; + [91m |[0m [91m^---^[0m + [91m |[0m No overloading for vector_access, tried: + [91m |[0m [94m*[0m bitvector_access + [91m |[0m Could not resolve quantifiers for bitvector_access + [91m |[0m [94m*[0m (0 <= 10 & (10 + 1) <= 8) + [91m |[0m [94m*[0m plain_vector_access + [91m |[0m Could not resolve quantifiers for plain_vector_access + [91m |[0m [94m*[0m (0 <= 10 & (10 + 1) <= 8) + [91m |[0m diff --git a/test/typecheck/pass/vec_length/v2.expect b/test/typecheck/pass/vec_length/v2.expect index d123cabd..c77ecaa7 100644 --- a/test/typecheck/pass/vec_length/v2.expect +++ b/test/typecheck/pass/vec_length/v2.expect @@ -1,13 +1,12 @@ -Type error at file "vec_length/v2.sail", line 7, character 11 to line 7, character 25 - - let z = [41m[x with 10 = y][0m; - -No overloadings for vector_update, tried: - bitvector_update: - Could not resolve quantifiers for bitvector_update (0 <= 10 & (10 + 1) <= 8) - - Try adding the constraint: (0 <= 10 & (10 + 1) <= 8) - plain_vector_update: - Could not resolve quantifiers for plain_vector_update (0 <= 10 & (10 + 1) <= 8) - - Try adding the constraint: (0 <= 10 & (10 + 1) <= 8) +Type error: +[[96mvec_length/v2.sail[0m]:7:10-25 +7[96m |[0m let z = [x with 10 = y]; + [91m |[0m [91m^-------------^[0m + [91m |[0m No overloading for vector_update, tried: + [91m |[0m [94m*[0m bitvector_update + [91m |[0m Could not resolve quantifiers for bitvector_update + [91m |[0m [94m*[0m (0 <= 10 & (10 + 1) <= 8) + [91m |[0m [94m*[0m plain_vector_update + [91m |[0m Could not resolve quantifiers for plain_vector_update + [91m |[0m [94m*[0m (0 <= 10 & (10 + 1) <= 8) + [91m |[0m diff --git a/test/typecheck/pass/vec_length/v2_inc.expect b/test/typecheck/pass/vec_length/v2_inc.expect index e7d2b52f..cff65f62 100644 --- a/test/typecheck/pass/vec_length/v2_inc.expect +++ b/test/typecheck/pass/vec_length/v2_inc.expect @@ -1,13 +1,12 @@ -Type error at file "vec_length/v2_inc.sail", line 7, character 11 to line 7, character 25 - - let z = [41m[x with 10 = y][0m; - -No overloadings for vector_update, tried: - bitvector_update: - Could not resolve quantifiers for bitvector_update (0 <= 10 & (10 + 1) <= 8) - - Try adding the constraint: (0 <= 10 & (10 + 1) <= 8) - plain_vector_update: - Could not resolve quantifiers for plain_vector_update (0 <= 10 & (10 + 1) <= 8) - - Try adding the constraint: (0 <= 10 & (10 + 1) <= 8) +Type error: +[[96mvec_length/v2_inc.sail[0m]:7:10-25 +7[96m |[0m let z = [x with 10 = y]; + [91m |[0m [91m^-------------^[0m + [91m |[0m No overloading for vector_update, tried: + [91m |[0m [94m*[0m bitvector_update + [91m |[0m Could not resolve quantifiers for bitvector_update + [91m |[0m [94m*[0m (0 <= 10 & (10 + 1) <= 8) + [91m |[0m [94m*[0m plain_vector_update + [91m |[0m Could not resolve quantifiers for plain_vector_update + [91m |[0m [94m*[0m (0 <= 10 & (10 + 1) <= 8) + [91m |[0m diff --git a/test/typecheck/pass/vec_length/v3.expect b/test/typecheck/pass/vec_length/v3.expect new file mode 100644 index 00000000..e3afecee --- /dev/null +++ b/test/typecheck/pass/vec_length/v3.expect @@ -0,0 +1,14 @@ +Type error: +[[96mvec_length/v3.sail[0m]:6:10-12:3 +6 [96m |[0m let y = x[ + [91m |[0m [91m^-[0m +12[96m |[0m ]; + [91m |[0m[91m--^[0m + [91m |[0m No overloading for vector_access, tried: + [91m |[0m [94m*[0m bitvector_access + [91m |[0m Could not resolve quantifiers for bitvector_access + [91m |[0m [94m*[0m (0 <= 10 & (10 + 1) <= 8) + [91m |[0m [94m*[0m plain_vector_access + [91m |[0m Could not resolve quantifiers for plain_vector_access + [91m |[0m [94m*[0m (0 <= 10 & (10 + 1) <= 8) + [91m |[0m diff --git a/test/typecheck/pass/vec_length/v3.sail b/test/typecheck/pass/vec_length/v3.sail new file mode 100644 index 00000000..8736278e --- /dev/null +++ b/test/typecheck/pass/vec_length/v3.sail @@ -0,0 +1,14 @@ +default Order dec +$include <vector_dec.sail> + +function main () : unit -> unit = { + let x : bits(8) = 0xff; + let y = x[ + + + + + 10 + ]; + () +} diff --git a/test/typecheck/pass/vector_subrange_gen.sail b/test/typecheck/pass/vector_subrange_gen.sail index 50a93cff..b82d6c8c 100644 --- a/test/typecheck/pass/vector_subrange_gen.sail +++ b/test/typecheck/pass/vector_subrange_gen.sail @@ -1,3 +1,4 @@ + val vector_access : forall ('l : Int) ('o : Order) ('a : Type), 'l >= 0. (vector('l, 'o, 'a), range(0, 'l - 1)) -> 'a @@ -11,6 +12,8 @@ val sub : forall ('n : Int) ('m : Int). (atom('n), atom('m)) -> atom('n - 'm) val "length" : forall ('n : Int). vector('n, inc, bit) -> atom('n) +overload __size = {length} + default Order inc val test : forall 'n 'm, 'n >= 5. |