diff options
Diffstat (limited to 'test/c')
33 files changed, 274 insertions, 41 deletions
diff --git a/test/c/anon_rec.expect b/test/c/anon_rec.expect new file mode 100644 index 00000000..9766475a --- /dev/null +++ b/test/c/anon_rec.expect @@ -0,0 +1 @@ +ok diff --git a/test/c/anon_rec.sail b/test/c/anon_rec.sail new file mode 100644 index 00000000..17dd1e07 --- /dev/null +++ b/test/c/anon_rec.sail @@ -0,0 +1,12 @@ +default Order dec + +union Foo ('a : Type) = { + MkFoo : { field1 : 'a, field2 : int } +} + +val "print_endline" : string -> unit + +function main((): unit) -> unit = { + let _: Foo(unit) = MkFoo(struct { field1 = (), field2 = 22 }); + print_endline("ok") +} diff --git a/test/c/assign_rename_bug.sail b/test/c/assign_rename_bug.sail index 8b74df2a..f9650b85 100644 --- a/test/c/assign_rename_bug.sail +++ b/test/c/assign_rename_bug.sail @@ -7,9 +7,8 @@ $include <vector_dec.sail> $include <exception_basic.sail> val sub_vec_int = { - ocaml: "sub_vec_int", - lem: "sub_vec_int", - c: "sub_bits_int" + c: "sub_bits_int", + _: "sub_vec_int" } : forall 'n. (bits('n), int) -> bits('n) overload operator - = {sub_vec_int} diff --git a/test/c/bitvector.sail b/test/c/bitvector.sail index 8a80234e..ba23b2cc 100644 --- a/test/c/bitvector.sail +++ b/test/c/bitvector.sail @@ -2,7 +2,7 @@ default Order dec $include <vector_dec.sail> -val test : (vector(16, dec, bit), vector(200, dec, bit)) -> bool +val test : (bitvector(16, dec), bitvector(200, dec)) -> bool function test (x, y) = { print_bits("x = ", x); diff --git a/test/c/bv_literal.sail b/test/c/bv_literal.sail index 1955b5dd..73f1133c 100644 --- a/test/c/bv_literal.sail +++ b/test/c/bv_literal.sail @@ -1,12 +1,12 @@ default Order dec -val "print_bits" : forall 'n. (string, vector('n, dec, bit)) -> unit +val "print_bits" : forall 'n. (string, bitvector('n, dec)) -> unit val main : unit -> unit function main () = { let x : bit = bitone; - let y : vector(4, dec, bit) = [x, bitone, bitzero, x]; + let y : bitvector(4, dec) = [x, bitone, bitzero, x]; print_bits("y = ", y); }
\ No newline at end of file diff --git a/test/c/eq_struct.sail b/test/c/eq_struct.sail index 9da12aae..2f6d4453 100644 --- a/test/c/eq_struct.sail +++ b/test/c/eq_struct.sail @@ -17,7 +17,7 @@ function neq(x, y) = ~(eq(x, y)) struct S = { field1: int, - field2: vector(8, dec, bit) + field2: bitvector(8, dec) } val "print" : string -> unit diff --git a/test/c/execute.isail b/test/c/execute.isail index f4b5ea0f..018dd92c 100644 --- a/test/c/execute.isail +++ b/test/c/execute.isail @@ -1,3 +1,4 @@ +:rewrites interpreter initialize_registers() :run main() diff --git a/test/c/gvector.sail b/test/c/gvector.sail index 3e452985..3d6e2bef 100644 --- a/test/c/gvector.sail +++ b/test/c/gvector.sail @@ -5,7 +5,7 @@ $include <vector_dec.sail> val "print_int" : (string, int) -> unit -register R : vector(32, dec, vector(32, dec, bit)) +register R : vector(32, dec, bitvector(32, dec)) register T : vector(32, dec, int) diff --git a/test/c/option.sail b/test/c/option.sail index aedde8ef..8041e8aa 100644 --- a/test/c/option.sail +++ b/test/c/option.sail @@ -5,7 +5,7 @@ $include <flow.sail> val print = "print_endline" : string -> unit val "print_int" : (string, int) -> unit -val "print_bits" : forall 'n. (string, vector('n, dec, bit)) -> unit +val "print_bits" : forall 'n. (string, bitvector('n, dec)) -> unit union option ('a : Type) = { None : unit, @@ -22,7 +22,7 @@ val main : unit -> unit function main () = { let x : option(int) = Some(5); let y : option(int) = None(); - let z : option(vector(4, dec, bit)) = Some(0xF); + let z : option(bitvector(4, dec)) = Some(0xF); match x { Some(a) => print_int("a = ", 5), @@ -34,7 +34,7 @@ function main () = { None() => print("None") }; - let q : soption(vector(4, dec, bit)) = sSome(0xA); + let q : soption(bitvector(4, dec)) = sSome(0xA); match q { sSome(c) => print_bits("c = ", c) diff --git a/test/c/pattern_concat_nest.sail b/test/c/pattern_concat_nest.sail index 92150e66..398e814f 100644 --- a/test/c/pattern_concat_nest.sail +++ b/test/c/pattern_concat_nest.sail @@ -1,26 +1,6 @@ default Order dec -type bits ('n : Int) = vector('n, dec, bit) - -union option ('a : Type) = {None : unit, Some : 'a} - -val vector_subrange = {ocaml: "subrange", lem: "subrange_vec_dec", c: "vector_subrange"} - : forall ('n : Int) ('m : Int) ('o : Int), 'o <= 'm & 'm <= 'n. - (bits('n), atom('m), atom('o)) -> bits('m - ('o - 1)) - -val bitvector_access = {ocaml: "access", lem: "access_vec_dec", c: "vector_access"} - : forall ('n : Int) ('m : Int), 0 <= 'm & 'm + 1 <= 'n. - (bits('n), atom('m)) -> bit - -overload vector_access = {bitvector_access} - -val eq_bit = {ocaml: "eq_bit", lem: "eq", interpreter: "eq_anything", c: "eq_bit"}: (bit, bit) -> bool - -overload operator == = { - eq_bit -} - -val and_bool = {ocaml: "and_bool", lem: "and_bool", smt: "and_bool", interpreter: "and_bool", c: "and_bool"}: (bool, bool) -> bool +$include <prelude.sail> //////////////////////////////////////////////////////////// diff --git a/test/c/poly_int_record.expect b/test/c/poly_int_record.expect new file mode 100644 index 00000000..a8a10253 --- /dev/null +++ b/test/c/poly_int_record.expect @@ -0,0 +1,3 @@ +x = 1 +y = 2 +ok diff --git a/test/c/poly_int_record.sail b/test/c/poly_int_record.sail new file mode 100644 index 00000000..ebb18713 --- /dev/null +++ b/test/c/poly_int_record.sail @@ -0,0 +1,21 @@ +default Order dec + +val "print_endline" : string -> unit +val "print_int" : (string, int) -> unit + +struct S('a: Type) = { + field1 : ('a, 'a), + field2 : unit +} + +function main((): unit) -> unit = { + var s : S(range(0, 3)) = struct { field1 = (0, 3), field2 = () }; + s.field1 = (1, 2); + match s.field1 { + (x, y) => { + print_int("x = ", x); + print_int("y = ", y); + } + }; + print_endline("ok"); +} diff --git a/test/c/poly_record.expect b/test/c/poly_record.expect new file mode 100644 index 00000000..9766475a --- /dev/null +++ b/test/c/poly_record.expect @@ -0,0 +1 @@ +ok diff --git a/test/c/poly_record.sail b/test/c/poly_record.sail new file mode 100644 index 00000000..afe1f144 --- /dev/null +++ b/test/c/poly_record.sail @@ -0,0 +1,18 @@ +default Order dec + +val "print_endline" : string -> unit + +struct S('a: Type) = { + field1 : 'a, + field2 : unit +} + +function f forall ('a :Type). (s: S('a)) -> unit = { + s.field2 +} + +function main((): unit) -> unit = { + let s : S(unit) = struct { field1 = (), field2 = () }; + f(s); + print_endline("ok"); +} diff --git a/test/c/run_tests.py b/test/c/run_tests.py index 2ee44fca..64c3ae42 100755 --- a/test/c/run_tests.py +++ b/test/c/run_tests.py @@ -22,10 +22,10 @@ def test_c(name, c_opts, sail_opts, valgrind): if tests[filename] == 0: step('sail -no_warn -c {} {} 1> {}.c'.format(sail_opts, filename, basename)) step('gcc {} {}.c {}/lib/*.c -lgmp -lz -I {}/lib -o {}'.format(c_opts, basename, sail_dir, sail_dir, basename)) - step('./{} 1> {}.result'.format(basename, basename)) + step('./{} 1> {}.result'.format(basename, basename), expected_status = 1 if basename == "exception" else 0) step('diff {}.result {}.expect'.format(basename, basename)) if valgrind: - step("valgrind --leak-check=full --track-origins=yes --errors-for-leak-kinds=all --error-exitcode=1 ./{}".format(basename)) + step("valgrind --leak-check=full --track-origins=yes --errors-for-leak-kinds=all --error-exitcode=2 ./{}".format(basename), expected_status = 1 if basename == "exception" else 0) print '{} {}{}{}'.format(filename, color.PASS, 'ok', color.END) sys.exit() results.collect(tests) @@ -40,7 +40,7 @@ def test_interpreter(name): basename = os.path.splitext(os.path.basename(filename))[0] tests[filename] = os.fork() if tests[filename] == 0: - step('sail -is execute.isail -iout {}.iresult {}'.format(basename, filename)) + step('sail -undefined_gen -is execute.isail -iout {}.iresult {}'.format(basename, filename)) step('diff {}.iresult {}.expect'.format(basename, basename)) print '{} {}{}{}'.format(filename, color.PASS, 'ok', color.END) sys.exit() @@ -57,7 +57,7 @@ def test_ocaml(name): tests[filename] = os.fork() if tests[filename] == 0: step('sail -ocaml -ocaml_build_dir _sbuild_{} -o {} {}'.format(basename, basename, filename)) - step('./{} 1> {}.oresult'.format(basename, basename)) + step('./{} 1> {}.oresult'.format(basename, basename), expected_status = 1 if basename == "exception" else 0) step('diff {}.oresult {}.expect'.format(basename, basename)) print '{} {}{}{}'.format(filename, color.PASS, 'ok', color.END) sys.exit() @@ -94,7 +94,6 @@ xml += test_c('unoptimized C', '', '', True) xml += test_c('optimized C', '-O2', '-O', True) xml += test_c('constant folding', '', '-Oconstant_fold', True) xml += test_c('monomorphised C', '-O2', '-O -Oconstant_fold -auto_mono', True) -xml += test_c('full optimizations', '-O2 -mbmi2 -DINTRINSICS', '-O -Oconstant_fold', True) xml += test_c('specialization', '-O1', '-O -c_specialize', True) xml += test_c('undefined behavior sanitised', '-O2 -fsanitize=undefined', '-O', False) diff --git a/test/c/rv_duopod_bug.expect b/test/c/rv_duopod_bug.expect new file mode 100644 index 00000000..681c7c43 --- /dev/null +++ b/test/c/rv_duopod_bug.expect @@ -0,0 +1,2 @@ +0 0x0000000000000000 +1 0xFFFFFFFFFFFFFFFF diff --git a/test/c/rv_duopod_bug.sail b/test/c/rv_duopod_bug.sail new file mode 100644 index 00000000..9a11996c --- /dev/null +++ b/test/c/rv_duopod_bug.sail @@ -0,0 +1,13 @@ +default Order dec + +$include <prelude.sail> + +val rX : int -> bits(64) + +function rX 0 = sail_zeros(64) +and rX (r if r > 0) = sail_ones(64) + +function main() -> unit = { + print_bits("0 ", rX(0)); + print_bits("1 ", rX(1)) +} diff --git a/test/c/single_guard.expect b/test/c/single_guard.expect new file mode 100644 index 00000000..070cdc2c --- /dev/null +++ b/test/c/single_guard.expect @@ -0,0 +1,2 @@ +In main +In test diff --git a/test/c/single_guard.sail b/test/c/single_guard.sail new file mode 100644 index 00000000..017ed8a5 --- /dev/null +++ b/test/c/single_guard.sail @@ -0,0 +1,16 @@ +default Order dec + +$include <prelude.sail> + +val "print_endline" : string -> unit + +val test : unit -> unit + +function test(_ if true) = { + print_endline("In test") +} + +function main() -> unit = { + print_endline("In main"); + test() +}
\ No newline at end of file diff --git a/test/c/stack_struct.sail b/test/c/stack_struct.sail index c5c79a81..5dd0caeb 100644 --- a/test/c/stack_struct.sail +++ b/test/c/stack_struct.sail @@ -1,6 +1,6 @@ default Order dec -type bits ('n : Int) = vector('n, dec, bit) +type bits ('n : Int) = bitvector('n, dec) union option ('a : Type) = { Some : 'a, diff --git a/test/c/struct.sail b/test/c/struct.sail index f3f2b071..21484c6a 100644 --- a/test/c/struct.sail +++ b/test/c/struct.sail @@ -1,10 +1,10 @@ default Order dec -val "print_bits" : forall 'n. (string, vector('n, dec, bit)) -> unit +val "print_bits" : forall 'n. (string, bitvector('n, dec)) -> unit struct test = { - A : vector(4, dec, bit), - B : vector(2, dec, bit), + A : bitvector(4, dec), + B : bitvector(2, dec), } function main (() : unit) -> unit = { diff --git a/test/c/toplevel_tyvar.expect b/test/c/toplevel_tyvar.expect new file mode 100644 index 00000000..9766475a --- /dev/null +++ b/test/c/toplevel_tyvar.expect @@ -0,0 +1 @@ +ok diff --git a/test/c/toplevel_tyvar.sail b/test/c/toplevel_tyvar.sail new file mode 100644 index 00000000..af2f4d1e --- /dev/null +++ b/test/c/toplevel_tyvar.sail @@ -0,0 +1,14 @@ +default Order dec + +$include <prelude.sail> + +val "print_endline" : string -> unit + +let 'var = 32 + +function main() -> unit = { + let x: bits('var) = 0xFFFF_FFFF; + let y: bits(32) = 0xFFFF_FFFF; + assert(x == y); + print_endline("ok") +} diff --git a/test/c/tuple_union.expect b/test/c/tuple_union.expect new file mode 100644 index 00000000..d8ea9f4f --- /dev/null +++ b/test/c/tuple_union.expect @@ -0,0 +1,42 @@ +y = 1 +z = 2 +y = 1 +z = 2 +y = 1 +z = 2 + +y = 3 +z = 4 +y = 3 +z = 4 +y = 3 +z = 4 + +y = 5 +z = 6 +y = 5 +z = 6 +y = 5 +z = 6 + +y = 7 +z = 8 +y = 7 +z = 8 +y = 7 +z = 8 + +y = 9 +z = 10 +y = 9 +z = 10 +y = 9 +z = 10 + +y = 11 +z = 12 +y = 11 +z = 12 +y = 11 +z = 12 + diff --git a/test/c/tuple_union.sail b/test/c/tuple_union.sail new file mode 100644 index 00000000..1914038f --- /dev/null +++ b/test/c/tuple_union.sail @@ -0,0 +1,48 @@ +default Order dec + +$include <prelude.sail> + +val "print_endline" : string -> unit + +union U('a: Type) = { + Ctor : 'a +} + +type pair = (int, int) + +function foo(x: U(pair)) -> unit = { + match x { + Ctor(y, z) => { + print_int("y = ", y); + print_int("z = ", z) + } + }; + match x { + Ctor((y, z)) => { + print_int("y = ", y); + print_int("z = ", z) + } + }; + match x { + Ctor(x) => match x { + (y, z) => { + print_int("y = ", y); + print_int("z = ", z) + } + } + }; + print_endline("") +} + +function main((): unit) -> unit = { + foo(Ctor(1, 2)); + foo(Ctor((3, 4))); + let x = (5, 6); + foo(Ctor(x)); + let x = Ctor(7, 8); + foo(x); + let x = Ctor(((9, 10))); + foo(x); + let x = (11, 12); + foo(Ctor(x)); +} diff --git a/test/c/undefined_nat.expect b/test/c/undefined_nat.expect new file mode 100644 index 00000000..9766475a --- /dev/null +++ b/test/c/undefined_nat.expect @@ -0,0 +1 @@ +ok diff --git a/test/c/undefined_nat.sail b/test/c/undefined_nat.sail new file mode 100644 index 00000000..35dead66 --- /dev/null +++ b/test/c/undefined_nat.sail @@ -0,0 +1,13 @@ +default Order dec + +$include <prelude.sail> + +val "print_endline" : string -> unit + +register R : nat + +register T : int + +function main() -> unit = { + print_endline("ok"); +}
\ No newline at end of file diff --git a/test/c/undefined_union.expect b/test/c/undefined_union.expect new file mode 100644 index 00000000..9766475a --- /dev/null +++ b/test/c/undefined_union.expect @@ -0,0 +1 @@ +ok diff --git a/test/c/undefined_union.sail b/test/c/undefined_union.sail new file mode 100644 index 00000000..9b652b34 --- /dev/null +++ b/test/c/undefined_union.sail @@ -0,0 +1,11 @@ + +union Test = { + Ctor1 : int, + Ctor2 : (int, int) +} + +val "print_endline" : string -> unit + +function main() -> unit = { + print_endline("ok") +} diff --git a/test/c/unused_poly_ctor.expect b/test/c/unused_poly_ctor.expect new file mode 100644 index 00000000..e55551e8 --- /dev/null +++ b/test/c/unused_poly_ctor.expect @@ -0,0 +1 @@ +y = 0xFFFF diff --git a/test/c/unused_poly_ctor.sail b/test/c/unused_poly_ctor.sail new file mode 100644 index 00000000..c752cb33 --- /dev/null +++ b/test/c/unused_poly_ctor.sail @@ -0,0 +1,18 @@ +default Order dec + +$include <prelude.sail> + +val "print_endline" : string -> unit + +union U('a: Type) = { + Err : 'a, + Ok : bits(16) +} + +function main((): unit) -> unit = { + let x : U(unit) = Ok(0xFFFF); + match x { + Err() => print_endline("error"), + Ok(y) => print_bits("y = ", y) + } +} diff --git a/test/c/zero_length_bv.expect b/test/c/zero_length_bv.expect new file mode 100644 index 00000000..9766475a --- /dev/null +++ b/test/c/zero_length_bv.expect @@ -0,0 +1 @@ +ok diff --git a/test/c/zero_length_bv.sail b/test/c/zero_length_bv.sail new file mode 100644 index 00000000..332b8aae --- /dev/null +++ b/test/c/zero_length_bv.sail @@ -0,0 +1,14 @@ +default Order dec + +$include <prelude.sail> + +val "print_endline" : string -> unit + +function main((): unit) -> unit = { + let x: bits(0) = []; + if x == sail_zeros(0) then { + print_endline("ok") + }; + let x: vector(0, dec, string) = []; + () +}
\ No newline at end of file |