Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

SMT performance fixes and SV return type attribute #699

Merged
merged 2 commits into from
Sep 6, 2024

SMT: Various small improvements for match performance

1f05f3c
Select commit
Loading
Failed to load commit list.
Sign in for the full log view
Merged

SMT performance fixes and SV return type attribute #699

SMT: Various small improvements for match performance
1f05f3c
Select commit
Loading
Failed to load commit list.
GitHub Actions / Test Results succeeded Sep 6, 2024 in 0s

All 680 tests pass in 0s

    9 files     21 suites   0s ⏱️
  680 tests   680 ✅ 0 💤 0 ❌
2 142 runs  2 141 ✅ 1 💤 0 ❌

Results for commit 1f05f3c.

Annotations

Check notice on line 0 in .github

See this annotation in the file changed.

@github-actions github-actions / Test Results

680 tests found

There are 680 tests, see "Raw output" for the full list of tests.
Raw output
Replicate.sail
abstract_bool.sail
abstract_bool2.sail
abstract_bool_inconsistent.sail
add_overflow.sat.sail
add_overflow.unsat.sail
add_real.sail
add_vec_exts_no_annot.sail
add_vec_exts_no_annot_overload.sail
add_vec_lit.sail
add_vec_lit_old.sail
all_even_vector_length.sail
allpats.sail
and_block.sail
and_let_bool.sail
anf_as_pattern.sail
anf_block.sail
anon_rec.sail
arith_C128FL.unsat.sail
arith_C64C32CB.unsat.sail
arith_FFL_1.unsat.sail
arith_FFL_2.unsat.sail
arith_FFL_3.unsat.sail
arith_FFL_4.unsat.sail
arith_FFL_5.unsat.sail
arith_LC32L.unsat.sail
arith_LC32L_1.unsat.sail
arith_LC32L_2.unsat.sail
arith_LC32L_3.unsat.sail
arith_LC32L_4.unsat.sail
arith_LCBL.unsat.sail
arm_FPEXC1.sail
arm_types.sail
as_pattern.sail
assign_rename_bug.sail
assignment_simple.sail
atomcase.sail
bad_option_pragma.sail
bad_option_pragma2.sail
basic_1.sat.sail
basic_1.unsat.sail
basic_2.sat.sail
basic_2.unsat.sail
bind_typ_var.sail
bitfield_abs.sail
bitfield_bits_field.sail
bitfield_error.sail
bitfield_exponential.sail
bitfield_mod.sail
bitfield_pc.sail
bitfield_updates.sail
bitfield_updates0.sail
bits_concat_pattern.sail
bits_if.sail
bitvector.sail
bitvector_param.sail
bitvector_update.sail
bitvector_update2.sail
bitwise_not.sail
bitwise_not_gen.sail
bitwise_not_x3.sail
block.sail
bool_bits_mapping.sail
bool_constraint.sail
bool_mapping.sail
bool_mapping2.sail
bool_typ_pat.sail
built bitfield/
built for_bounds/
built hello_world/
built is_x_subrange/
built loop/
built lsl/
built new_bitfields/
built pattern1/
built pure_rebind/
built reg_alias/
built reg_passing/
built reg_ref/
built short_circuit/
built string_equality/
built string_of_struct/
built trycatch/
built types/
built vec_32_64/
built void/
bv_literal.sail
bv_simple_index_bit.sail
bv_update_error.sail
can_hang.sail
case_simple1.sail
case_simple2.sail
cast_lexp1.sail
cast_lexp2.sail
cast_simple.sail
ccheri_regression1.unsat.sail
cfold_reg.sail
cheri128_hsb.sail
cheri_capreg.sail
cheri_capstruct_order.sail
clear_overflow_regression.unsat.sail
commentfix.sail
comments.sail
complete_pattern_let.sail
complex_exist_sat.sail
concat_prop.unsat.sail
concat_prop128.unsat.sail
concurrency_interface.sail
concurrency_interface_dec.sail
concurrency_interface_inc.sail
cond_mod.sail
config.sail
config_register.sail
cons_pattern.sail
cons_pattern_synonym.sail
cons_wildcard_insert.sail
constrained_function.sail
constrained_function_scattered.sail
constrained_struct.sail
constraint_ctor.sail
constraint_syn.sail
constructor247.sail
cr_invisible.sail
crlf.sail
custom_flow.sail
dead_branch.sail
dec_prelude.sail
decode_patterns.sail
default_order.sail
deinfix_plus.sail
doc_comment.sail
doc_comment_eof.sail
double_option.sail
downcast_fn.sail
duplicate_binding.sail
duplicate_builtin.sail
duplicate_ctor.sail
duplicate_quant.sail
duplicate_toplevel_let.sail
duplicate_toplevel_let_mod.sail
duplicate_type_id.sail
duplicate_type_id2.sail
duplicate_type_id3.sail
duplicate_type_id4.sail
duplicate_type_id5.sail
duplicate_type_id6.sail
either.sail
either_rvbug.sail
empty_list.sail
empty_su.sail
empty_vector_infer.sail
encdec.sail
encdec.sat.sail
encdec_subrange.sail
encdec_unknown_and_error.sail
enum_cast.sail
enum_function_override.sail
enum_functions.sail
enum_functions_partial.sail
enum_map.sail
enum_match.sail
enum_shadow.sail
enum_shadow_let.sail
enum_shadow_reg.sail
enum_tup_match.sail
eq_struct.sail
eqn_inst.sail
equation_arguments.sail
equation_return.sail
ex_cast.sail
ex_list_infer.sail
ex_vector_infer.sail
exception.unsat.sail
exception_2.unsat.sail
exception_3.unsat.sail
execute_decode_hard.sail
exint.sail
exist1.sail
exist2.sail
exist_simple.sail
exist_subrange.sail
exist_synonym.sail
exist_tlb.sail
exist_true.sail
existential_ast.sail
existential_ast2.sail
existential_ast3.sail
existential_constraint_synonym.sail
exit1.sail
exit2.sail
exit3.sail
exn_hello_world.sail
extend_simple.sail
extended_ascii.sail
extension_constructor.sail
fail_assert_mono_bug.sail
fail_exception.sail
fail_issue203.sail
fail_simple.sail_project
fallthrough_exception.sail
fast_signed.sail
float_prelude.sail
floor_pow2.sail
flow_gt1.sail
flow_gteq1.sail
flow_lt1.sail
flow_lt2.sail
flow_lteq1.sail
flow_restrict.sail
fn_kind_infer.sail
fn_kind_infer_body.sail
for_shadow.sail
foreach_e.sail
foreach_none.sail
foreach_simple.unsat.sail
foreach_simple_2.unsat.sail
foreach_var_updates.sail
fpthreesimp.sail
funcl_guard.sail
function_namespace.sail
function_quant.sail
fvector_update.sail
get_slice_int.sail
global_false_constraint.sail
global_let_shadow.sail
global_type_var.sail
guards.sail
gvector.sail
gvector.unsat.sail
gvector_trivial.unsat.sail
gvectorlit.sail
hello_world.sail
help_option_pragma.sail
if_infer.sail
if_infer2.sail
if_opt_typ.sail
if_return.sail
if_type_if.sail
if_var_updates.sail
illegal_escape.sail
implicits.sail
import_reserved.sail
inc_prelude.sail
inc_tests.sail
infix_include.sail
inline_regression.unsat.sail
inline_test_1.unsat.sail
inline_typ.sail
int64_vector_literal.sail
int_pattern.sail
int_struct.sail
int_struct_constrained.sail
int_synonym.sail
invalid_function_val.sail
issue136.sail
issue202_1.sail
issue232.sail
issue232_2.sail
issue243.sail
issue243_fixed.sail
issue244_1.sail
issue244_2.sail
issue244_3.sail
issue244_4.sail
issue250.sail
issue277.sail
issue362.sail
issue37.sail
issue401.sail
issue429.sail
issue434.sail
issue573_1.sat.sail
issue573_2.sat.sail
large_bitvector.sail
let_intervene.unsat.sail
let_option.sail
let_option_shadow.sail
let_single_branch.sail
let_subtyp_bug.sail
letbind.sail
lexp_vec.sail
lib_hex_bits.sail
lib_hex_bits_signed.sail
lib_valid_hex_bits.sail
line_comment_eof.sail
linked_int.unsat.sail
linked_int2.unsat.sail
list_cons.sail
list_cons2.sail
list_cons_cons.sail
list_infer.sail
list_let.sail
list_lit.sail
list_mut.sail
list_rec_functions1.sail
list_rec_functions2.sail
list_scope.sail
list_scope2.sail
list_scope3.sail
list_test.sail
list_torture.sail
literal_complete.sail
literal_complete_alt.sail
literal_complete_single.sail
lookup.sail
loop_exception.sail
lt_flow.sail
lt_int_irrefl.unsat.sail
lt_int_trans.unsat.sail
lteq_int_antisym.unsat.sail
lteq_int_def.unsat.sail
lteq_int_refl.unsat.sail
lteq_int_trans.unsat.sail
lzcnt.unsat.sail
lzcnt_2.unsat.sail
lzcnt_3.unsat.sail
mapping.sail
mapping_body_private.sail
mapping_clause.sail
mapping_compose.sail
mapping_length_mismatch.sail
mapping_rreg.sail
mapping_two_type.sail
match_bind.sail
match_fail.sat.sail
match_fail_query_1.sat.sail
match_fail_query_2.sat.sail
minmax.unsat.sail
minmax_1.sat.sail
minmax_2.sat.sail
missing_tick.sail
mix_declaration_update.sail
mod_var.sail
modify_assignment1.sail
modify_enum.sail
modify_enum2.sail
modify_immutable.sail
modify_immutable2.sail
modify_type_chain.sail
module_reserved.sail
multiple_unifiers.sail
mutrec.sail
nat_set.sail
negative_bits_existential.sail
negative_bits_list.sail
negative_bits_struct.sail
negative_bits_struct2.sail
negative_bits_tuple.sail
negative_bits_union.sail
negative_bits_union2.sail
nested_fields.sail
nested_mapping.sail
new_bitfields.sail
nexp_simp_euclidian.sail
nexp_synonym.sail
nexp_synonym2.sail
nlflow.sail
no_function.sail
no_function2.sail
no_function3.sail
no_possible_overload.sail
no_val_recur.sail
non_synonym.sail
non_unique.sail
nonexistent_overload.sail
nonexistent_pragma.sail
not_pattern.sail
nzcv.sail
option.sail
option_either.sail
option_lit.unsat.sail
option_nest.sail
option_option.sail
option_tuple.sail
option_tuple_i683.unsat.sail
order.unsat.sail
outcome_impl.sail
outcome_impl_quant.sail
overlap_field.sail
overload_bound.sail
overload_int_nat.sail
overload_mapping.sail
overload_member_scope.sail
overload_overload.sail
overload_plus.sail
pat_completeness.sail
pattern_concat_nest.sail
patternrefinement.sail
patterns.sail
pc_no_wildcard.sail
phantom_bitlist_struct.sail
phantom_bitlist_union.sail
phantom_num.sail
phantom_option.sail
plus_one_unify.sail
pointer_assign.sail
poly_ab_mapping.sail
poly_int_record.sail
poly_list.sail
poly_mapping.sail
poly_mapping2.sail
poly_outcome.sail
poly_pair.sail
poly_record.sail
poly_simple.sail
poly_tup.sail
poly_union.sail
poly_union_rev.sail
poly_vector.sail
pow2.sail
pow2space.sail
pow_32_64.sail
pow_unify.sail
pr194.sail
pragma_block.sail
prelude.sail
prelude_no_order.sail
primop.sail
priv_fn_no_val.sail
private_clause.sail
private_ctor.sail
private_extension.sail
private_function.sail
private_scattered_enum.sail
private_scattered_fn.sail
private_scattered_map.sail
private_scattered_union.sail
private_union.sail
procstate1.sail
pub_val_priv_fn.sail
pure_let_var.sail
pure_let_var2.sail
pure_record.sail
pure_record2.sail
pure_record3.sail
range.sail
read_write_ram.sail
real.sail
real.unsat.sail
real_prop.sail
recursion.sail
reg_32_64.sail
reg_init_let.sail
reg_list.sail
reg_mod.sail
reg_option.sail
reg_ref.sail
reg_ref.unsat.sail
reg_ref_nb.sail
repeat_constraint.sail
return_leak.sail
return_register_ref.sail
return_simple1.sail
return_simple2.sail
return_simple3.sail
return_simple4.sail
revrev_endianness.unsat.sail
revrev_endianness2.unsat.sail
revrev_endianness3.unsat.sail
rmem_rmemt_same.sail
rv_add_0.sat.sail
rv_add_0.unsat.sail
rv_add_1.sat.sail
rv_add_1.unsat.sail
rv_add_decode.unsat.sail
rv_duopod_bug.sail
rv_format.sail
rv_format2.sail
rv_memop.sail
rv_reg_rw.unsat.sail
sail_mask.unsat.sail
sail_mask_2.unsat.sail
sail_mask_3.unsat.sail
sail_mask_4.unsat.sail
sail_mask_5.unsat.sail
scattered_enum.sail
scattered_enum_mod.sail
scattered_function_mod.sail
scattered_map_mod.sail
scattered_mapping.sail
scattered_mapping_doc.sail
scattered_union_doc.sail
scattered_union_mod.sail
scattered_union_rec.sail
set_constraint.sail
set_match.sail
set_struct.sail
set_struct2.sail
set_syntax.sail
shadow_cleanup.sail
shadow_leak_check.sail
shadow_leak_infer.sail
shadow_let.sail
shift_or_concat.unsat.sail
shift_or_concat128.unsat.sail
shift_or_concat4.unsat.sail
shift_or_concat4_2.unsat.sail
shift_or_concat_1.sat.sail
shift_or_concat_2.sat.sail
shiftr_zero_1.sat.sail
shiftr_zero_1.unsat.sail
short_circuit.sail
short_circuit_bool_ex.sail
sign_extend.unsat.sail
sign_extend_2.unsat.sail
simple.sail_project
simple_bitmanip.sail
simple_if.sail
simple_record_access.sail
simple_scattered.sail
single_arg.sail
single_assign_in_block.sail
single_enum.sail
single_guard.sail
single_union.sail
sizeof_fixed.sail
small_slice.sail
some_none.sail
some_none_int.sail
spc_mappings.sail
spc_mappings_small.sail
special_annot.sail
split.sail
sqrt.sat.sail
sqrt.unsat.sail
stack_struct.sail
strict_var.sail
string.sat.sail
string.unsat.sail
string_append_non_exec.sail
string_literal_type.sail
string_of_bits.sail
string_of_bits2.sail
string_take.sail
struct.sail
struct_field_constraint.sail
struct_field_copy.unsat.sail
struct_fn_arg.sail
struct_incomplete_literal.sail
struct_kind_infer.sail
struct_mapping.sail
struct_pattern.sail
struct_pattern_duplicate_field.sail
struct_pattern_partial.sail
struct_prop.unsat.sail
struct_rec.sail
struct_update.sail
struct_width.unsat.sail
submodules_include.sail_project
syn_kind_infer.sail
synonym_rec.sail
synth_ex_vs.sail
tautology.sail
test_if_comment_1.sail
tl_let.sail
tl_let_shadow.sat.sail
tl_pat.sail
tl_poly_match.sail
toplevel_let.unsat.sail
toplevel_let_trivial.unsat.sail
toplevel_tyvar.sail
trivial.sat.sail
trivial.unsat.sail
trivial_assert.sat.sail
trivial_assert_2.unsat.sail
trivial_funcall.sat.sail
trivial_return.sat.sail
trivial_return.unsat.sail
true_false.sail
try_return.sail
try_while_try.sail
tuple_assign.sail
tuple_bitvector_int_pat.sail
tuple_bitvector_int_pat2.sail
tuple_bitvector_int_pat3.sail
tuple_conversion.sail
tuple_fun.sail
tuple_lexp1.sail
tuple_lexp2.sail
tuple_type_cast.sail
tuple_union.sail
two_argument.sail
two_mapping.sail
type_div.sail
type_if_bits.sail
type_if_then_else.sail
type_if_then_else_alt.sail
type_pat_parens.sail
type_pow_zero.sail
tyvar_shadow.sail
unbalanced_comment.sail
unbalanced_comment2.sail
unbound_tyvar.sail
unbound_tyvar2.sail
unbounded_int_annot.sail
unconstructed_type_mono.sail
undeclared_field_assignment.sail
undeclared_vector_assignment.sail
undefined_infer.sail
undefined_nat.sail
undefined_union.sail
union_ctor_constraint.sail
union_infer.sail
union_infer_kind.sail
union_rec.sail
union_recf.sail
unknown_end.sail
unknown_operator.sail
unscope_enum.sail
unscope_let.sail
unscope_register.sail
unscope_type.sail
unscope_val.sail
unsigned_index.sail
unterminated_ifdef.sail
unterminated_string.sail
unused_poly_ctor.sail
update_access.unsat.sail
update_fbits_i667.unsat.sail
update_subrange.unsat.sail
val.sail
varity.sail
varswap.sail
vec_length.sail
vec_length_inc.sail
vec_pat1.sail
vector_access.sail
vector_access_dec.sail
vector_append.sail
vector_append_gen.sail
vector_concat_assign.sail
vector_example.sail
vector_init.sail
vector_pattern_split.sail
vector_subrange_gen.sail
vector_subrange_mapping.sail
vector_subrange_pattern.sail
vmatch.sail
warl.sail
warl2.sail
warn_cannot_wildcard.sail
warn_cons_incomplete.sail
warn_cons_wildcard_insert1.sail
warn_cons_wildcard_insert2.sail
warn_double_cons_incomplete.sail
warn_empty_list.sail
warn_int_pattern.sail
warn_literal_complete.sail
warn_missing_enum.sail
warn_partial_lookup.sail
warn_partial_scattered.sail
warn_range_redundant.sail
warn_struct_pattern_incomplete.sail
warn_tuple_bitvector_pat.sail
warn_unbounded_int.sail
warn_unbounded_nat.sail
wf_assign_type.sail
wf_register_type.sail
wf_specs.sail
while_MM.sail
while_MP.sail
while_PM.sail
while_PP.sail
wildcard_mapping.sail
wrap_into_oneline.sail
write_ref.sat.sail
write_ref.unsat.sail
xlen32.sail
xlen_val.sail
zero_length_bv.sail
zeros_1.sat.sail
zeros_1.unsat.sail
zeros_2.sat.sail
zeros_2.unsat.sail
zeros_3.sat.sail
zeros_3.unsat.sail
zeros_4.unsat.sail
zeros_implicit.sail
zeros_mapping.sail
zeros_ones.unsat.sail