Skip to content

Commit

Permalink
Lean: Run more tests (#1008)
Browse files Browse the repository at this point in the history
  • Loading branch information
@Alasdair
Alasdair authored Feb 14, 2025
1 parent fb75c8d commit 8797890
Showing 1 changed file with 175 additions and 13 deletions.
188 changes: 175 additions & 13 deletions test/lean/run_tests.py
View file
Original file line number Diff line number Diff line change
Expand Up @@ -21,14 +21,173 @@
# that you can run to exercise the language and the extracted output.
# Not all self-tests are supported.
# TODO: once we support many of those, we should make this a `skip_selftests`
include_selftests = {
'hello_world.sail',
skip_selftests = {
'struct_pattern_partial',
'issue202_1',
'list_rec_functions2',
'list_mut',
'eq_struct',
'either_rvbug',
'bv_literal',
'issue362',
'return_register_ref',
'prelude',
'tuple_fun',
'pow2_var',
'large_bitvector',
'exn_hello_world',
'struct',
'poly_union_rev',
'match_bind',
'sv_dpi',
'rev_bits_in_byte',
'list_let',
'foreach_none',
'letbind',
'enum_map',
'all_even_vector_length',
'outcome_impl',
'lib_valid_hex_bits',
'string_of_bits2',
'list_cons_cons',
'tuple_conversion',
'pow2',
'primop',
'reg_ref',
'zero_length_bv',
'reg_ref_nb',
'poly_pair',
'fast_signed',
'issue37',
'assign_rename_bug',
'warl',
'config',
'if_opt_typ',
'spc_mappings_small',
'cheri128_hsb',
'instruction',
'overload_mapping',
'encdec_subrange',
'gvector',
'small_slice',
'union_variant_names',
'lib_hex_bits',
'lib_hex_bits_signed',
'fail_assert_mono_bug',
'constructor247',
'config_bit',
'varswap',
'empty_list',
'struct_fn_arg',
'rv_format2',
'let_option_shadow',
'try_return',
'bitvector_update2',
'poly_mapping2',
'real',
'inc_tests',
'poly_outcome',
'string_of_bits',
'nexp_synonym',
'config_register',
'return_leak',
'custom_flow',
'pointer_assign',
'either',
'two_mapping',
'ctz',
'spc_mappings',
'concurrency_interface',
'vector_example',
'reg_init_let',
'list_scope',
'for_shadow',
'list_torture',
'rv_format',
'list_scope3',
'option_nest',
'vector_subrange_pattern',
'string_literal_type',
'hex_str_negative',
'single_arg',
'shadow_let',
'tuple_union',
'bitvector',
'xlen32',
'rv_duopod_bug',
'warl2',
'mapping',
'list_scope2',
'issue232_2',
'poly_int_record',
'cheri_capreg',
'loop_exception',
'issue429',
'list_list_eq',
'list_test',
'struct_mapping',
'pc_no_wildcard',
'type_if_bits',
'poly_union',
'dec_str_fixed',
'unused_poly_ctor',
'bitvector_update',
'nested_fields',
'nexp_simp_euclidian',
'tl_let',
'config_register_ones',
'toplevel_tyvar',
'pattern_concat_nest',
'option',
'abstract_type',
'poly_tup',
'ediv',
'ediv_from_tdiv',
'int_struct',
'dead_branch',
'int64_vector_literal',
'concurrency_interface_write',
'read_write_ram',
'enum_vector',
'list_rec_functions1',
'issue136',
'reg_32_64',
'issue232',
'issue243_fixed',
'enum_functions',
'int_struct_constrained',
'get_slice_int',
'fail_exception',
'zeros_mapping',
'extend_simple',
'natural_sort_reg',
'option_option',
'pr194',
'tl_pat',
'anf_as_pattern',
'implicits',
'simple_bitmanip',
'poly_mapping',
'xlen_val',
'nested_mapping',
'gvectorlit',
'encdec',
'infix_include',
'fvector_update',
'split',
'struct_pattern',
'stack_struct',
'new_bitfields',
'real_prop',
'vector_init',
'partial_mapping',
'fail_issue203'
}

print("Sail is {}".format(sail))
print("Sail dir is {}".format(sail_dir))

def test_lean(subdir: str, allowed_list = None, runnable: bool = False):
def test_lean(subdir: str, skip_list = None, runnable: bool = False):
"""
Run all Sail files available in the `subdir`.
If `runnable` is set to `True`, it will do `lake run`
Expand All @@ -39,10 +198,12 @@ def test_lean(subdir: str, allowed_list = None, runnable: bool = False):
for filenames in chunks(os.listdir(f'../{subdir}'), parallel()):
tests = {}
for filename in filenames:
if allowed_list is not None and filename not in allowed_list:
basename = os.path.splitext(os.path.basename(filename))[0]

if skip_list is not None and basename in skip_list:
print_skip(filename)
continue

basename = os.path.splitext(os.path.basename(filename))[0]
tests[filename] = os.fork()
if tests[filename] == 0:
os.chdir(f'../{subdir}')
Expand All @@ -60,13 +221,14 @@ def test_lean(subdir: str, allowed_list = None, runnable: bool = False):
# NOTE: lake --dir does not behave the same as cd $dir && lake build...
step('lake build', cwd=f'{basename}/out', name=filename)

status = step_with_status(f'diff {basename}/out/Out.lean {basename}.expected.lean', name=filename)
if status != 0:
if update_expected:
print(f'Overriding file {basename}.expected.lean')
step(f'cp {basename}/out/Out.lean {basename}.expected.lean')
else:
sys.exit(1)
if not runnable:
status = step_with_status(f'diff {basename}/out/Out.lean {basename}.expected.lean', name=filename)
if status != 0:
if update_expected:
print(f'Overriding file {basename}.expected.lean')
step(f'cp {basename}/out/Out.lean {basename}.expected.lean')
else:
sys.exit(1)

if runnable:
status = step_with_status(f'diff {basename}/out/expected {basename}.expect', name=filename)
Expand All @@ -81,7 +243,7 @@ def test_lean(subdir: str, allowed_list = None, runnable: bool = False):
xml = '<testsuites>\n'

xml += test_lean('lean')
xml += test_lean('c', allowed_list=include_selftests, runnable=True)
xml += test_lean('c', skip_list=skip_selftests, runnable=True)

xml += '</testsuites>\n'

Expand Down

0 comments on commit 8797890

Please sign in to comment.