diff --git a/Makefile b/Makefile index 982c2ae874..c15b871462 100644 --- a/Makefile +++ b/Makefile @@ -241,9 +241,9 @@ endif # ########## Flags ########## ifeq ($(ZLIST),platform) - VSTDIRS= msl sepcomp veric floyd $(PROGSDIR) concurrency ccc26x86 atomics + VSTDIRS= msl sepcomp veric floyd elpi ltac2 $(PROGSDIR) concurrency ccc26x86 atomics else - VSTDIRS= msl sepcomp veric zlist floyd $(PROGSDIR) concurrency ccc26x86 atomics + VSTDIRS= msl sepcomp veric zlist floyd elpi ltac2 $(PROGSDIR) concurrency ccc26x86 atomics endif OTHERDIRS= wand_demo sha hmacfcf tweetnacl20140427 hmacdrbg aes mailbox boringssl_fips_20180730 DIRS = $(VSTDIRS) $(OTHERDIRS) @@ -478,6 +478,11 @@ FLOYD_FILES= \ data_at_list_solver.v step.v fastforward.v finish.v #real_forward.v +ELPI_FILES= \ + simpl_by_cbv.v cbv_symbol_lists_generated_definitions.v cbv_symbol_lists_generated.v + +LTAC2_FILES= \ + simpl_by_cbv.v cbv_symbol_lists_generated.v constr_ex.v list_ex.v control_ex.v message_ex.v print_ex.v PROGS32_FILES= \ incr.v verif_incr.v \ @@ -606,6 +611,8 @@ FILES = \ $(SEPCOMP_FILES:%=sepcomp/%) \ $(VERIC_FILES:%=veric/%) \ $(FLOYD_FILES:%=floyd/%) \ + $(ELPI_FILES:%=elpi/%) \ + $(LTAC2_FILES:%=ltac2/%) \ $(PROGS_FILES:%=$(PROGSDIR)/%) \ $(WAND_DEMO_FILES:%=wand_demo/%) \ $(SHA_FILES:%=sha/%) \ @@ -730,7 +737,7 @@ concurrency: _CoqProject $(CC_TARGET) $(SEPCOMP_FILES:%.v=sepcomp/%.vo) $(CONCUR linking: _CoqProject $(LINKING_FILES:%.v=linking/%.vo) veric: _CoqProject $(VERIC_FILES:%.v=veric/%.vo) veric/version.vo zlist: _CoqProject $(ZLIST_FILES:%.v=zlist/%.vo) -floyd: _CoqProject $(FLOYD_FILES:%.v=floyd/%.vo) +floyd: _CoqProject $(FLOYD_FILES:%.v=floyd/%.vo) $(ELPI_FILES:%.v=elpi/%.vo) $(LTAC2_FILES:%.v=ltac2/%.vo) progs: _CoqProject $(PROGS_FILES:%.v=$(PROGSDIR)/%.vo) progsdir: $(PROGSDIR) wand_demo: _CoqProject $(WAND_DEMO_FILES:%.v=wand_demo/%.vo) @@ -926,4 +933,3 @@ assumptions.txt: veric/tcb.vo # such problem, not sure exactly. -- Andrew) include .depend -include .depend-concur - diff --git a/elpi/ReadMe.md b/elpi/ReadMe.md new file mode 100644 index 0000000000..f3c72035c5 --- /dev/null +++ b/elpi/ReadMe.md @@ -0,0 +1,31 @@ +# Elpi code for VST + +Elpi is a (relatively) new tactic language for Coq based on Prolog. + +Currently we use it only for one purpose: + +## Simplification by "Call By Value" computation with specially crafted delta symbol lists + +VST needs in many places to do e.g. computations on PTress with symbol lists. These can contain user provided terms (values assigned to variables). +Using simpl for this task usually works but has two drawbacks: + +- it is quite slow because simpl employs rather involved heuristics to decide if a term will get simpler if reductions are done +- running simpl on unknown user terms can explode in case the terms contain variables + +This problem is solved by using the `cbv` tactic with a specially crafted delta symbol list, which only contains those symbols required e.g. +for the PTree reduction. As long as the user terms don't contain PTree logic, they are unmodified by this. + +The issue with this is that the symbol lists are long (many 100) and it might be a lot of work to maintain them. For this reason we use Elpi +to create symbol lists from high level descriptions like "all transparent definitions in module X.Y". + +This works, but requires a version of Elpi which has not yet been released (at least not in Coq Platform), so we do this in a two step process: + +- a symbol list generator which creates .v files which are checked into git - only this requires the edge version of Elpi +- a tactic which uses the generated symbol list .v files - this is (currently) written in Ltac2 + +Adding make rules for the generator leads to circular make dependencies. So no explicit rules are provided. +The symbol lists can be regenerated with a usual call to make (with whatever parameters you usually use) and the target + +`elpi/cbv_symbol_lists_generator.vo` + +This regenerates `elpi/cbv_symbol_lists_generated.v` and `ltac2/cbv_symbol_lists_generated.v` diff --git a/elpi/cbv_symbol_lists_generated.v b/elpi/cbv_symbol_lists_generated.v new file mode 100644 index 0000000000..ae2c677a0d --- /dev/null +++ b/elpi/cbv_symbol_lists_generated.v @@ -0,0 +1,1129 @@ +(* This file has been auto-generated by elpi/cbv_symbol_lists_generator.v - DO NOT MODIFY! *) +Require Import elpi.elpi. +Require Import VST.elpi.cbv_symbol_lists_generated_definitions. + +Require Import VST.veric.val_lemmas. +Require Import VST.veric.SeparationLogic. +Require Import VST.veric.mpred. +Require Import VST.veric.lift. +Require Import VST.veric.expr. +Require Import VST.veric.Clight_Cop2. +Require Import VST.floyd.local2ptree_typecheck. +Require Import VST.floyd.local2ptree_eval. +Require Import compcert.aarch64.Archi. +Require Import compcert.lib.Maps. +Require Import compcert.export.Ctypesdefs. +Require Import compcert.cfrontend.Ctypes. +Require Import compcert.cfrontend.Cop. +Require Import compcert.cfrontend.Clight. +Require Import PArith.BinPos. +Require Import ZArith.BinInt. + +Elpi cbv_expanded_reduction_definition "msubst_denote_tc_assert" + VST.veric.val_lemmas.is_true + VST.veric.val_lemmas.force_val + VST.veric.val_lemmas.force_val1 + VST.veric.val_lemmas.force_val2 + VST.veric.val_lemmas.force_int + VST.veric.val_lemmas.force_signed_int + VST.veric.val_lemmas.force_ptr + VST.veric.val_lemmas.always + VST.veric.val_lemmas.offset_val + VST.veric.val_lemmas.range_s32 + VST.veric.val_lemmas.range_s64 + VST.veric.val_lemmas.is_long + VST.veric.val_lemmas.is_float + VST.veric.val_lemmas.is_single + VST.veric.val_lemmas.is_pointer_or_null + VST.veric.val_lemmas.is_pointer_or_integer + VST.veric.val_lemmas.isptr + VST.veric.SeparationLogic.Nveric + VST.veric.SeparationLogic.Sveric + VST.veric.SeparationLogic.Cveric + VST.veric.SeparationLogic.Iveric + VST.veric.SeparationLogic.Rveric + VST.veric.SeparationLogic.SIveric + VST.veric.SeparationLogic.CSLveric + VST.veric.SeparationLogic.CIveric + VST.veric.SeparationLogic.SRveric + VST.veric.SeparationLogic.Bveric + VST.veric.SeparationLogic.Fveric + VST.veric.SeparationLogic.LiftNatDed' + VST.veric.SeparationLogic.LiftSepLog' + VST.veric.SeparationLogic.LiftClassicalSep' + VST.veric.SeparationLogic.LiftIndir' + VST.veric.SeparationLogic.LiftSepIndir' + VST.veric.SeparationLogic.LiftCorableSepLog' + VST.veric.SeparationLogic.LiftCorableIndir' + VST.veric.SeparationLogic.local + VST.veric.SeparationLogic.argsHaveTyps + VST.veric.SeparationLogic.funspec_sub_si + VST.veric.SeparationLogic.funspec_sub + VST.veric.SeparationLogic.close_precondition + VST.veric.SeparationLogic.argsassert2assert + VST.veric.SeparationLogic.denote_tc_iszero + VST.veric.SeparationLogic.denote_tc_nonzero + VST.veric.SeparationLogic.denote_tc_igt + VST.veric.SeparationLogic.denote_tc_lgt + VST.veric.SeparationLogic.Zoffloat + VST.veric.SeparationLogic.Zofsingle + VST.veric.SeparationLogic.denote_tc_Zge + VST.veric.SeparationLogic.denote_tc_Zle + VST.veric.SeparationLogic.sameblock + VST.veric.SeparationLogic.denote_tc_samebase + VST.veric.SeparationLogic.denote_tc_nodivover + VST.veric.SeparationLogic.denote_tc_nosignedover + VST.veric.SeparationLogic.denote_tc_initialized + VST.veric.SeparationLogic.denote_tc_isptr + VST.veric.SeparationLogic.denote_tc_isint + VST.veric.SeparationLogic.denote_tc_islong + VST.veric.SeparationLogic.test_eq_ptrs + VST.veric.SeparationLogic.test_order_ptrs + VST.veric.SeparationLogic.denote_tc_test_eq + VST.veric.SeparationLogic.denote_tc_test_order + VST.veric.SeparationLogic.typecheck_error + VST.veric.SeparationLogic.fool + VST.veric.SeparationLogic.denote_tc_assert + VST.veric.SeparationLogic.fool' + VST.veric.SeparationLogic.cast_pointer_to_bool + VST.veric.SeparationLogic.ext_link_prog' + VST.veric.SeparationLogic.ext_link_prog + VST.veric.SeparationLogic.closed_wrt_vars + VST.veric.SeparationLogic.closed_wrt_lvars + VST.veric.SeparationLogic.not_a_param + VST.veric.SeparationLogic.precondition_closed + VST.veric.SeparationLogic.typed_true + VST.veric.SeparationLogic.typed_false + VST.veric.SeparationLogic.substopt + VST.veric.SeparationLogic.cast_expropt + VST.veric.SeparationLogic.typecheck_tid_ptr_compare + VST.veric.SeparationLogic.mapsto + VST.veric.SeparationLogic.mapsto_ + VST.veric.SeparationLogic.mapsto_zeros + VST.veric.SeparationLogic.globals + VST.veric.SeparationLogic.init_data2pred + VST.veric.SeparationLogic.init_data_size + VST.veric.SeparationLogic.init_data_list_size + VST.veric.SeparationLogic.init_data_list2pred + VST.veric.SeparationLogic.readonly2share + VST.veric.SeparationLogic.globvar2pred + VST.veric.SeparationLogic.globals_of_env + VST.veric.SeparationLogic.globals_of_genv + VST.veric.SeparationLogic.globvars2pred + VST.veric.SeparationLogic.initializer_aligned + VST.veric.SeparationLogic.initializers_aligned + VST.veric.SeparationLogic.funsig + VST.veric.SeparationLogic.memory_block + VST.veric.SeparationLogic.align_compatible + VST.veric.SeparationLogic.size_compatible + VST.veric.SeparationLogic.is_int32_noattr_type + VST.veric.SeparationLogic.eval_lvar + VST.veric.SeparationLogic.var_block + VST.veric.SeparationLogic.stackframe_of + VST.veric.SeparationLogic.func_ptr + VST.veric.SeparationLogic.NDmk_funspec + VST.veric.SeparationLogic.allp_fun_id + VST.veric.SeparationLogic.type_of_funsig + VST.veric.SeparationLogic.fn_funsig + VST.veric.SeparationLogic.tc_fn_return + VST.veric.SeparationLogic.globals_only + VST.veric.SeparationLogic.make_args + VST.veric.SeparationLogic.make_args' + VST.veric.SeparationLogic.ret_temp + VST.veric.SeparationLogic.get_result1 + VST.veric.SeparationLogic.get_result + VST.veric.SeparationLogic.maybe_retval + VST.veric.SeparationLogic.bind_ret + VST.veric.SeparationLogic.overridePost + VST.veric.SeparationLogic.existential_ret_assert + VST.veric.SeparationLogic.normal_ret_assert + VST.veric.SeparationLogic.frame_ret_assert + VST.veric.SeparationLogic.switch_ret_assert + VST.veric.SeparationLogic.with_ge + VST.veric.SeparationLogic.prog_funct' + VST.veric.SeparationLogic.prog_funct + VST.veric.SeparationLogic.prog_vars' + VST.veric.SeparationLogic.prog_vars + VST.veric.SeparationLogic.all_initializers_aligned + VST.veric.SeparationLogic.loop1_ret_assert + VST.veric.SeparationLogic.loop2_ret_assert + VST.veric.SeparationLogic.function_body_ret_assert + VST.veric.SeparationLogic.loop_nocontinue_ret_assert + VST.veric.SeparationLogic.tc_environ + VST.veric.SeparationLogic.tc_temp_id + VST.veric.SeparationLogic.typeof_temp + VST.veric.SeparationLogic.tc_expr + VST.veric.SeparationLogic.tc_exprlist + VST.veric.SeparationLogic.tc_lvalue + VST.veric.SeparationLogic.tc_expropt + VST.veric.SeparationLogic.is_comparison + VST.veric.SeparationLogic.blocks_match + VST.veric.SeparationLogic.cmp_ptr_no_mem + VST.veric.SeparationLogic.op_to_cmp + VST.veric.SeparationLogic.arglist + VST.veric.SeparationLogic.closed_wrt_modvars + VST.veric.SeparationLogic.initblocksize + VST.veric.SeparationLogic.main_pre + VST.veric.SeparationLogic.main_post + VST.veric.SeparationLogic.main_spec_ext' + VST.veric.SeparationLogic.main_spec_ext + VST.veric.SeparationLogic.match_globvars + VST.veric.SeparationLogic.int_range + VST.veric.SeparationLogic.semax_body_params_ok + VST.veric.SeparationLogic.var_sizes_ok + VST.veric.SeparationLogic.make_ext_rval + VST.veric.SeparationLogic.tc_option_val + VST.veric.SeparationLogic.zip_with_tl + VST.veric.SeparationLogic.funspecs_norepeat + VST.veric.SeparationLogic.add_funspecs + VST.veric.SeparationLogic.funsig2signature + VST.veric.SeparationLogic.decode_encode_val_ok + VST.veric.SeparationLogic.numeric_type + VST.veric.SeparationLogic.subp_sepcon_mpred + VST.veric.SeparationLogic.unfold_Ssequence + VST.veric.SeparationLogic.nocontinue + VST.veric.SeparationLogic.nocontinue_ls + VST.veric.SeparationLogic.withtype_empty + VST.veric.SeparationLogic.prop_Proper + VST.veric.mpred.Map.t + VST.veric.mpred.Map.get + VST.veric.mpred.Map.set + VST.veric.mpred.Map.remove + VST.veric.mpred.Map.empty + VST.veric.mpred.strict_bool_val + VST.veric.mpred.type_is_by_value + VST.veric.mpred.type_is_by_reference + VST.veric.mpred.genviron + VST.veric.mpred.venviron + VST.veric.mpred.tenviron + VST.veric.mpred.environ_rect + VST.veric.mpred.environ_ind + VST.veric.mpred.environ_rec + VST.veric.mpred.environ_sind + VST.veric.mpred.ge_of + VST.veric.mpred.ve_of + VST.veric.mpred.te_of + VST.veric.mpred.any_environ + VST.veric.mpred.argsEnviron + VST.veric.mpred.AssertTT + VST.veric.mpred.ArgsTT + VST.veric.mpred.SpecTT + VST.veric.mpred.SpecArgsTT + VST.veric.mpred.super_non_expansive + VST.veric.mpred.args_super_non_expansive + VST.veric.mpred.const_super_non_expansive + VST.veric.mpred.AssertListTT + VST.veric.mpred.super_non_expansive_list + VST.veric.mpred.args_const_super_non_expansive + VST.veric.mpred.funspec_rect + VST.veric.mpred.funspec_ind + VST.veric.mpred.funspec_rec + VST.veric.mpred.funspec_sind + VST.veric.mpred.varspecs + VST.veric.mpred.funspecs + VST.veric.mpred.assert + VST.veric.mpred.argsassert + VST.veric.mpred.packPQ + VST.veric.mpred.int_range + VST.veric.mpred.typelist_of_type_list + VST.veric.mpred.type_of_funspec + VST.veric.mpred.typelist2list + VST.veric.mpred.idset + VST.veric.mpred.idset0 + VST.veric.mpred.idset1 + VST.veric.mpred.insert_idset + VST.veric.mpred.eval_id + VST.veric.mpred.env_set + VST.veric.mpred.make_tycontext_s + VST.veric.mpred.lift0 + VST.veric.mpred.lift1 + VST.veric.mpred.lift2 + VST.veric.mpred.lift3 + VST.veric.mpred.lift4 + VST.veric.mpred.alift0 + VST.veric.mpred.alift1 + VST.veric.mpred.alift2 + VST.veric.mpred.alift3 + VST.veric.mpred.alift4 + VST.veric.mpred.LiftEnviron + VST.veric.mpred.LiftAEnviron + VST.veric.lift.lift_S + VST.veric.lift.lift_T + VST.veric.lift.lift_prod + VST.veric.lift.lift_last + VST.veric.lift.lifted + VST.veric.lift.lift_curry + VST.veric.lift.lift_uncurry_open + VST.veric.lift.Tend + VST.veric.lift.Tarrow + VST.veric.lift.lift + VST.veric.lift.liftx + VST.veric.expr.sizeof + VST.veric.expr.alignof + VST.veric.expr.eval_unop + VST.veric.expr.op_to_cmp + VST.veric.expr.is_comparison + VST.veric.expr.eval_binop + VST.veric.expr.eval_cast + VST.veric.expr.eval_field + VST.veric.expr.eval_var + VST.veric.expr.deref_noload + VST.veric.expr.eval_expr + VST.veric.expr.eval_lvalue + VST.veric.expr.eval_exprlist + VST.veric.expr.eval_expropt + VST.veric.expr.bool_type + VST.veric.expr.is_scalar_type + VST.veric.expr.is_int_type + VST.veric.expr.is_int32_type + VST.veric.expr.is_long_type + VST.veric.expr.is_ptrofs_type + VST.veric.expr.is_float_type + VST.veric.expr.is_single_type + VST.veric.expr.is_anyfloat_type + VST.veric.expr.is_pointer_type + VST.veric.expr.tc_error_rect + VST.veric.expr.tc_error_ind + VST.veric.expr.tc_error_rec + VST.veric.expr.tc_error_sind + VST.veric.expr.tc_assert_rect + VST.veric.expr.tc_assert_ind + VST.veric.expr.tc_assert_rec + VST.veric.expr.tc_assert_sind + VST.veric.expr.tc_noproof + VST.veric.expr.tc_iszero + VST.veric.expr.tc_nonzero + VST.veric.expr.tc_test_eq + VST.veric.expr.tc_test_order + VST.veric.expr.tc_nodivover + VST.veric.expr.if_expr_signed + VST.veric.expr.tc_nobinover + VST.veric.expr.tc_andp + VST.veric.expr.tc_orp + VST.veric.expr.tc_bool + VST.veric.expr.check_pp_int + VST.veric.expr.binarithType + VST.veric.expr.is_numeric_type + VST.veric.expr.tc_ilt + VST.veric.expr.tc_llt + VST.veric.expr.tc_int_or_ptr_type + VST.veric.expr.isUnOpResultType + VST.veric.expr.isBinOpResultType + VST.veric.expr.isCastResultType + VST.veric.expr.is_neutral_cast + VST.veric.expr.get_var_type + VST.veric.expr.same_base_type + VST.veric.expr.typecheck_expr + VST.veric.expr.typecheck_lvalue + VST.veric.expr.implicit_deref + VST.veric.expr.typecheck_temp_id + VST.veric.expr.tc_might_be_true + VST.veric.expr.tc_always_true + VST.veric.expr.typecheck_b + VST.veric.expr.typecheck_pure_b + VST.veric.expr.typecheck_exprlist + VST.veric.expr.match_fsig_aux + VST.veric.expr.match_fsig + VST.veric.expr.expr_closed_wrt_vars + VST.veric.expr.lvalue_closed_wrt_vars + VST.veric.expr.typecheck_store + VST.veric.expr.valid_pointer' + VST.veric.expr.valid_pointer + VST.veric.expr.weak_valid_pointer + VST.veric.expr.funsig_of_function + VST.veric.expr.subsumespec + VST.veric.expr.tycontext_sub + VST.veric.expr.cenv_sub + VST.veric.expr.ha_env_cs_sub + VST.veric.expr.la_env_cs_sub + VST.veric.expr.cspecs_sub + VST.veric.Clight_Cop2.sem_cast_pointer + VST.veric.Clight_Cop2.sem_cast_i2i + VST.veric.Clight_Cop2.sem_cast_i2bool + VST.veric.Clight_Cop2.sem_cast_l2bool + VST.veric.Clight_Cop2.sem_cast_l2l + VST.veric.Clight_Cop2.sem_cast_i2l + VST.veric.Clight_Cop2.sem_cast_l2i + VST.veric.Clight_Cop2.sem_cast_struct + VST.veric.Clight_Cop2.sem_cast_union + VST.veric.Clight_Cop2.sem_cast_f2f + VST.veric.Clight_Cop2.sem_cast_s2s + VST.veric.Clight_Cop2.sem_cast_s2f + VST.veric.Clight_Cop2.sem_cast_f2s + VST.veric.Clight_Cop2.sem_cast_i2f + VST.veric.Clight_Cop2.sem_cast_i2s + VST.veric.Clight_Cop2.sem_cast_f2i + VST.veric.Clight_Cop2.sem_cast_s2i + VST.veric.Clight_Cop2.sem_cast_f2bool + VST.veric.Clight_Cop2.sem_cast_s2bool + VST.veric.Clight_Cop2.sem_cast_l2f + VST.veric.Clight_Cop2.sem_cast_l2s + VST.veric.Clight_Cop2.sem_cast_f2l + VST.veric.Clight_Cop2.sem_cast_s2l + VST.veric.Clight_Cop2.classify_cast + VST.veric.Clight_Cop2.sem_cast + VST.veric.Clight_Cop2.sem_notbool + VST.veric.Clight_Cop2.sem_neg_i + VST.veric.Clight_Cop2.sem_neg_f + VST.veric.Clight_Cop2.sem_neg_s + VST.veric.Clight_Cop2.sem_neg_l + VST.veric.Clight_Cop2.sem_neg + VST.veric.Clight_Cop2.sem_absfloat_i + VST.veric.Clight_Cop2.sem_absfloat_f + VST.veric.Clight_Cop2.sem_absfloat_s + VST.veric.Clight_Cop2.sem_absfloat_l + VST.veric.Clight_Cop2.sem_absfloat + VST.veric.Clight_Cop2.sem_notint_i + VST.veric.Clight_Cop2.sem_notint_l + VST.veric.Clight_Cop2.sem_notint + VST.veric.Clight_Cop2.both_int + VST.veric.Clight_Cop2.both_long + VST.veric.Clight_Cop2.both_float + VST.veric.Clight_Cop2.both_single + VST.veric.Clight_Cop2.sem_binarith + VST.veric.Clight_Cop2.sem_add_ptr_int + VST.veric.Clight_Cop2.sem_add_int_ptr + VST.veric.Clight_Cop2.sem_add_ptr_long + VST.veric.Clight_Cop2.sem_add_long_ptr + VST.veric.Clight_Cop2.sem_add + VST.veric.Clight_Cop2.sem_sub_pi + VST.veric.Clight_Cop2.sem_sub_pl + VST.veric.Clight_Cop2.sem_sub_pp + VST.veric.Clight_Cop2.sem_sub_default + VST.veric.Clight_Cop2.sem_sub + VST.veric.Clight_Cop2.sem_mul + VST.veric.Clight_Cop2.sem_div + VST.veric.Clight_Cop2.sem_mod + VST.veric.Clight_Cop2.sem_and + VST.veric.Clight_Cop2.sem_or + VST.veric.Clight_Cop2.sem_xor + VST.veric.Clight_Cop2.sem_shift_ii + VST.veric.Clight_Cop2.sem_shift_il + VST.veric.Clight_Cop2.sem_shift_li + VST.veric.Clight_Cop2.sem_shift_ll + VST.veric.Clight_Cop2.sem_shift + VST.veric.Clight_Cop2.sem_shl + VST.veric.Clight_Cop2.sem_shr + VST.veric.Clight_Cop2.true2 + VST.veric.Clight_Cop2.sem_cmp_pp + VST.veric.Clight_Cop2.sem_cmp_pi + VST.veric.Clight_Cop2.sem_cmp_ip + VST.veric.Clight_Cop2.sem_cmp_pl + VST.veric.Clight_Cop2.sem_cmp_lp + VST.veric.Clight_Cop2.sem_cmp_default + VST.veric.Clight_Cop2.sem_cmp + VST.veric.Clight_Cop2.sem_unary_operation + VST.veric.Clight_Cop2.sem_binary_operation' + VST.veric.Clight_Cop2.sem_incrdecr + VST.floyd.local2ptree_typecheck.msubst_simpl_tc_assert + VST.floyd.local2ptree_typecheck.msubst_denote_tc_assert + VST.floyd.local2ptree_typecheck.msubst_tc_lvalue + VST.floyd.local2ptree_typecheck.msubst_tc_expr + VST.floyd.local2ptree_typecheck.msubst_tc_LR + VST.floyd.local2ptree_typecheck.msubst_tc_efield + VST.floyd.local2ptree_typecheck.msubst_tc_exprlist + VST.floyd.local2ptree_typecheck.msubst_tc_expropt + VST.floyd.local2ptree_typecheck.legal_tc_init + VST.floyd.local2ptree_eval.eval_vardesc + VST.floyd.local2ptree_eval.eval_lvardesc + VST.floyd.local2ptree_eval.msubst_eval_expr + VST.floyd.local2ptree_eval.msubst_eval_lvalue + VST.floyd.local2ptree_eval.msubst_eval_LR + VST.floyd.local2ptree_eval.msubst_eval_lvar + compcert.aarch64.Archi.ptr64 + compcert.aarch64.Archi.big_endian + compcert.aarch64.Archi.align_int64 + compcert.aarch64.Archi.align_float64 + compcert.aarch64.Archi.splitlong + compcert.aarch64.Archi.default_nan_64 + compcert.aarch64.Archi.default_nan_32 + compcert.aarch64.Archi.choose_nan + compcert.aarch64.Archi.choose_nan_64 + compcert.aarch64.Archi.choose_nan_32 + compcert.aarch64.Archi.fma_order + compcert.aarch64.Archi.fma_invalid_mul_is_nan + compcert.aarch64.Archi.float_of_single_preserves_sNaN + compcert.aarch64.Archi.float_conversion_default_nan + compcert.aarch64.Archi.abi_kind_rect + compcert.aarch64.Archi.abi_kind_ind + compcert.aarch64.Archi.abi_kind_rec + compcert.aarch64.Archi.abi_kind_sind + compcert.lib.Maps.PTree.elt + compcert.lib.Maps.PTree.elt_eq + compcert.lib.Maps.PTree.tree'_ind + compcert.lib.Maps.PTree.t + compcert.lib.Maps.PTree.Node + compcert.lib.Maps.PTree.empty + compcert.lib.Maps.PTree.get' + compcert.lib.Maps.PTree.get + compcert.lib.Maps.PTree.set0 + compcert.lib.Maps.PTree.set' + compcert.lib.Maps.PTree.set + compcert.lib.Maps.PTree.rem' + compcert.lib.Maps.PTree.remove' + compcert.lib.Maps.PTree.remove + compcert.lib.Maps.PTree.not_trivially_empty + compcert.lib.Maps.PTree.tree_case + compcert.lib.Maps.PTree.tree_rec' + compcert.lib.Maps.PTree.tree_rec + compcert.lib.Maps.PTree.tree_rec2' + compcert.lib.Maps.PTree.tree_rec2 + compcert.lib.Maps.PTree.tree_ind'_obligation_1 + compcert.lib.Maps.PTree.tree_ind'_obligation_2 + compcert.lib.Maps.PTree.tree_ind'_obligation_3 + compcert.lib.Maps.PTree.tree_ind'_obligation_4 + compcert.lib.Maps.PTree.tree_ind'_obligation_5 + compcert.lib.Maps.PTree.tree_ind'_obligation_6 + compcert.lib.Maps.PTree.tree_ind'_obligation_7 + compcert.lib.Maps.PTree.tree_ind' + compcert.lib.Maps.PTree.tree_ind + compcert.lib.Maps.PTree.beq' + compcert.lib.Maps.PTree.beq + compcert.lib.Maps.PTree.prev_append + compcert.lib.Maps.PTree.prev + compcert.lib.Maps.PTree.map' + compcert.lib.Maps.PTree.map + compcert.lib.Maps.PTree.map1' + compcert.lib.Maps.PTree.map1 + compcert.lib.Maps.PTree.map_filter1_nonopt + compcert.lib.Maps.PTree.map_filter1 + compcert.lib.Maps.PTree.filter1 + compcert.lib.Maps.PTree.combine + compcert.lib.Maps.PTree.xelements' + compcert.lib.Maps.PTree.elements + compcert.lib.Maps.PTree.xelements + compcert.lib.Maps.PTree.xkeys + compcert.lib.Maps.PTree.fold' + compcert.lib.Maps.PTree.fold + compcert.lib.Maps.PTree.fold1' + compcert.lib.Maps.PTree.fold1 + compcert.export.Ctypesdefs.tvoid + compcert.export.Ctypesdefs.tschar + compcert.export.Ctypesdefs.tuchar + compcert.export.Ctypesdefs.tshort + compcert.export.Ctypesdefs.tushort + compcert.export.Ctypesdefs.tint + compcert.export.Ctypesdefs.tuint + compcert.export.Ctypesdefs.tbool + compcert.export.Ctypesdefs.tlong + compcert.export.Ctypesdefs.tulong + compcert.export.Ctypesdefs.tfloat + compcert.export.Ctypesdefs.tdouble + compcert.export.Ctypesdefs.tptr + compcert.export.Ctypesdefs.tarray + compcert.export.Ctypesdefs.volatile_attr + compcert.export.Ctypesdefs.tattr + compcert.export.Ctypesdefs.tvolatile + compcert.export.Ctypesdefs.talignas + compcert.export.Ctypesdefs.tvolatile_alignas + compcert.export.Ctypesdefs.append_bit_pos + compcert.export.Ctypesdefs.append_char_pos_default + compcert.export.Ctypesdefs.append_char_pos + compcert.export.Ctypesdefs.ident_of_string + compcert.export.Ctypesdefs.decode_n_bits + compcert.export.Ctypesdefs.decode_8_bits + compcert.export.Ctypesdefs.string_of_ident + compcert.cfrontend.Ctypes.signedness_rect + compcert.cfrontend.Ctypes.signedness_ind + compcert.cfrontend.Ctypes.signedness_rec + compcert.cfrontend.Ctypes.signedness_sind + compcert.cfrontend.Ctypes.intsize_rect + compcert.cfrontend.Ctypes.intsize_ind + compcert.cfrontend.Ctypes.intsize_rec + compcert.cfrontend.Ctypes.intsize_sind + compcert.cfrontend.Ctypes.floatsize_rect + compcert.cfrontend.Ctypes.floatsize_ind + compcert.cfrontend.Ctypes.floatsize_rec + compcert.cfrontend.Ctypes.floatsize_sind + compcert.cfrontend.Ctypes.attr_volatile + compcert.cfrontend.Ctypes.attr_alignas + compcert.cfrontend.Ctypes.noattr + compcert.cfrontend.Ctypes.type_rect + compcert.cfrontend.Ctypes.type_ind + compcert.cfrontend.Ctypes.type_rec + compcert.cfrontend.Ctypes.type_sind + compcert.cfrontend.Ctypes.typelist_rect + compcert.cfrontend.Ctypes.typelist_ind + compcert.cfrontend.Ctypes.typelist_rec + compcert.cfrontend.Ctypes.typelist_sind + compcert.cfrontend.Ctypes.intsize_eq + compcert.cfrontend.Ctypes.signedness_eq + compcert.cfrontend.Ctypes.attr_eq + compcert.cfrontend.Ctypes.type_eq + compcert.cfrontend.Ctypes.typelist_eq + compcert.cfrontend.Ctypes.attr_of_type + compcert.cfrontend.Ctypes.change_attributes + compcert.cfrontend.Ctypes.remove_attributes + compcert.cfrontend.Ctypes.attr_union + compcert.cfrontend.Ctypes.merge_attributes + compcert.cfrontend.Ctypes.bitsize_intsize + compcert.cfrontend.Ctypes.struct_or_union_rect + compcert.cfrontend.Ctypes.struct_or_union_ind + compcert.cfrontend.Ctypes.struct_or_union_rec + compcert.cfrontend.Ctypes.struct_or_union_sind + compcert.cfrontend.Ctypes.member_rect + compcert.cfrontend.Ctypes.member_ind + compcert.cfrontend.Ctypes.member_rec + compcert.cfrontend.Ctypes.member_sind + compcert.cfrontend.Ctypes.members + compcert.cfrontend.Ctypes.composite_definition_rect + compcert.cfrontend.Ctypes.composite_definition_ind + compcert.cfrontend.Ctypes.composite_definition_rec + compcert.cfrontend.Ctypes.composite_definition_sind + compcert.cfrontend.Ctypes.name_member + compcert.cfrontend.Ctypes.type_member + compcert.cfrontend.Ctypes.member_is_padding + compcert.cfrontend.Ctypes.name_composite_def + compcert.cfrontend.Ctypes.composite_def_eq + compcert.cfrontend.Ctypes.co_su + compcert.cfrontend.Ctypes.co_members + compcert.cfrontend.Ctypes.co_attr + compcert.cfrontend.Ctypes.co_sizeof + compcert.cfrontend.Ctypes.co_alignof + compcert.cfrontend.Ctypes.co_rank + compcert.cfrontend.Ctypes.co_sizeof_pos + compcert.cfrontend.Ctypes.co_alignof_two_p + compcert.cfrontend.Ctypes.co_sizeof_alignof + compcert.cfrontend.Ctypes.composite_env + compcert.cfrontend.Ctypes.bitfield_rect + compcert.cfrontend.Ctypes.bitfield_ind + compcert.cfrontend.Ctypes.bitfield_rec + compcert.cfrontend.Ctypes.bitfield_sind + compcert.cfrontend.Ctypes.type_int32s + compcert.cfrontend.Ctypes.type_bool + compcert.cfrontend.Ctypes.typeconv + compcert.cfrontend.Ctypes.default_argument_conversion + compcert.cfrontend.Ctypes.complete_type + compcert.cfrontend.Ctypes.complete_or_function_type + compcert.cfrontend.Ctypes.align_attr + compcert.cfrontend.Ctypes.alignof + compcert.cfrontend.Ctypes.sizeof + compcert.cfrontend.Ctypes.naturally_aligned + compcert.cfrontend.Ctypes.bitalignof + compcert.cfrontend.Ctypes.bitsizeof + compcert.cfrontend.Ctypes.bitalignof_intsize + compcert.cfrontend.Ctypes.next_field + compcert.cfrontend.Ctypes.layout_field + compcert.cfrontend.Ctypes.layout_start + compcert.cfrontend.Ctypes.layout_width + compcert.cfrontend.Ctypes.layout_alignment + compcert.cfrontend.Ctypes.alignof_composite + compcert.cfrontend.Ctypes.bitsizeof_struct + compcert.cfrontend.Ctypes.bytes_of_bits + compcert.cfrontend.Ctypes.sizeof_struct + compcert.cfrontend.Ctypes.sizeof_union + compcert.cfrontend.Ctypes.field_type + compcert.cfrontend.Ctypes.field_offset_rec + compcert.cfrontend.Ctypes.field_offset + compcert.cfrontend.Ctypes.union_field_offset + compcert.cfrontend.Ctypes.mode_rect + compcert.cfrontend.Ctypes.mode_ind + compcert.cfrontend.Ctypes.mode_rec + compcert.cfrontend.Ctypes.mode_sind + compcert.cfrontend.Ctypes.access_mode + compcert.cfrontend.Ctypes.type_is_volatile + compcert.cfrontend.Ctypes.alignof_blockcopy + compcert.cfrontend.Ctypes.rank_type + compcert.cfrontend.Ctypes.rank_members + compcert.cfrontend.Ctypes.type_of_params + compcert.cfrontend.Ctypes.typ_of_type + compcert.cfrontend.Ctypes.rettype_of_type + compcert.cfrontend.Ctypes.typlist_of_typelist + compcert.cfrontend.Ctypes.signature_of_type + compcert.cfrontend.Ctypes.sizeof_composite + compcert.cfrontend.Ctypes.complete_members + compcert.cfrontend.Ctypes.composite_of_def_obligation_1 + compcert.cfrontend.Ctypes.composite_of_def_obligation_2 + compcert.cfrontend.Ctypes.composite_of_def_obligation_3 + compcert.cfrontend.Ctypes.composite_of_def + compcert.cfrontend.Ctypes.add_composite_definitions + compcert.cfrontend.Ctypes.build_composite_env + compcert.cfrontend.Ctypes.co_consistent_complete + compcert.cfrontend.Ctypes.co_consistent_alignof + compcert.cfrontend.Ctypes.co_consistent_sizeof + compcert.cfrontend.Ctypes.co_consistent_rank + compcert.cfrontend.Ctypes.composite_env_consistent + compcert.cfrontend.Ctypes.fundef_rect + compcert.cfrontend.Ctypes.fundef_ind + compcert.cfrontend.Ctypes.fundef_rec + compcert.cfrontend.Ctypes.fundef_sind + compcert.cfrontend.Ctypes.prog_defs + compcert.cfrontend.Ctypes.prog_public + compcert.cfrontend.Ctypes.prog_main + compcert.cfrontend.Ctypes.prog_types + compcert.cfrontend.Ctypes.prog_comp_env + compcert.cfrontend.Ctypes.prog_comp_env_eq + compcert.cfrontend.Ctypes.program_of_program + compcert.cfrontend.Ctypes.make_program_obligation_1 + compcert.cfrontend.Ctypes.make_program + compcert.cfrontend.Ctypes.Linker_types_obligation_1 + compcert.cfrontend.Ctypes.Linker_types_obligation_2 + compcert.cfrontend.Ctypes.Linker_types_obligation_3 + compcert.cfrontend.Ctypes.Linker_types + compcert.cfrontend.Ctypes.check_compat_composite + compcert.cfrontend.Ctypes.filter_redefs + compcert.cfrontend.Ctypes.link_composite_defs + compcert.cfrontend.Ctypes.Linker_composite_defs_obligation_1 + compcert.cfrontend.Ctypes.Linker_composite_defs_obligation_2 + compcert.cfrontend.Ctypes.Linker_composite_defs_obligation_3 + compcert.cfrontend.Ctypes.Linker_composite_defs + compcert.cfrontend.Ctypes.link_fundef + compcert.cfrontend.Ctypes.linkorder_fundef_ind + compcert.cfrontend.Ctypes.linkorder_fundef_sind + compcert.cfrontend.Ctypes.Linker_fundef_obligation_1 + compcert.cfrontend.Ctypes.Linker_fundef_obligation_2 + compcert.cfrontend.Ctypes.Linker_fundef_obligation_3 + compcert.cfrontend.Ctypes.Linker_fundef + compcert.cfrontend.Ctypes.lift_option + compcert.cfrontend.Ctypes.link_program + compcert.cfrontend.Ctypes.linkorder_program + compcert.cfrontend.Ctypes.Linker_program_obligation_1 + compcert.cfrontend.Ctypes.Linker_program_obligation_2 + compcert.cfrontend.Ctypes.Linker_program_obligation_3 + compcert.cfrontend.Ctypes.Linker_program + compcert.cfrontend.Cop.unary_operation_rect + compcert.cfrontend.Cop.unary_operation_ind + compcert.cfrontend.Cop.unary_operation_rec + compcert.cfrontend.Cop.unary_operation_sind + compcert.cfrontend.Cop.binary_operation_rect + compcert.cfrontend.Cop.binary_operation_ind + compcert.cfrontend.Cop.binary_operation_rec + compcert.cfrontend.Cop.binary_operation_sind + compcert.cfrontend.Cop.incr_or_decr_rect + compcert.cfrontend.Cop.incr_or_decr_ind + compcert.cfrontend.Cop.incr_or_decr_rec + compcert.cfrontend.Cop.incr_or_decr_sind + compcert.cfrontend.Cop.classify_cast_cases_rect + compcert.cfrontend.Cop.classify_cast_cases_ind + compcert.cfrontend.Cop.classify_cast_cases_rec + compcert.cfrontend.Cop.classify_cast_cases_sind + compcert.cfrontend.Cop.classify_cast + compcert.cfrontend.Cop.cast_int_int + compcert.cfrontend.Cop.cast_int_float + compcert.cfrontend.Cop.cast_float_int + compcert.cfrontend.Cop.cast_int_single + compcert.cfrontend.Cop.cast_single_int + compcert.cfrontend.Cop.cast_int_long + compcert.cfrontend.Cop.cast_long_float + compcert.cfrontend.Cop.cast_long_single + compcert.cfrontend.Cop.cast_float_long + compcert.cfrontend.Cop.cast_single_long + compcert.cfrontend.Cop.sem_cast + compcert.cfrontend.Cop.classify_bool_cases_rect + compcert.cfrontend.Cop.classify_bool_cases_ind + compcert.cfrontend.Cop.classify_bool_cases_rec + compcert.cfrontend.Cop.classify_bool_cases_sind + compcert.cfrontend.Cop.classify_bool + compcert.cfrontend.Cop.bool_val + compcert.cfrontend.Cop.sem_notbool + compcert.cfrontend.Cop.classify_neg_cases_rect + compcert.cfrontend.Cop.classify_neg_cases_ind + compcert.cfrontend.Cop.classify_neg_cases_rec + compcert.cfrontend.Cop.classify_neg_cases_sind + compcert.cfrontend.Cop.classify_neg + compcert.cfrontend.Cop.sem_neg + compcert.cfrontend.Cop.sem_absfloat + compcert.cfrontend.Cop.classify_notint_cases_rect + compcert.cfrontend.Cop.classify_notint_cases_ind + compcert.cfrontend.Cop.classify_notint_cases_rec + compcert.cfrontend.Cop.classify_notint_cases_sind + compcert.cfrontend.Cop.classify_notint + compcert.cfrontend.Cop.sem_notint + compcert.cfrontend.Cop.binarith_cases_rect + compcert.cfrontend.Cop.binarith_cases_ind + compcert.cfrontend.Cop.binarith_cases_rec + compcert.cfrontend.Cop.binarith_cases_sind + compcert.cfrontend.Cop.classify_binarith + compcert.cfrontend.Cop.binarith_type + compcert.cfrontend.Cop.sem_binarith + compcert.cfrontend.Cop.classify_add_cases_rect + compcert.cfrontend.Cop.classify_add_cases_ind + compcert.cfrontend.Cop.classify_add_cases_rec + compcert.cfrontend.Cop.classify_add_cases_sind + compcert.cfrontend.Cop.classify_add + compcert.cfrontend.Cop.ptrofs_of_int + compcert.cfrontend.Cop.sem_add_ptr_int + compcert.cfrontend.Cop.sem_add_ptr_long + compcert.cfrontend.Cop.sem_add + compcert.cfrontend.Cop.classify_sub_cases_rect + compcert.cfrontend.Cop.classify_sub_cases_ind + compcert.cfrontend.Cop.classify_sub_cases_rec + compcert.cfrontend.Cop.classify_sub_cases_sind + compcert.cfrontend.Cop.classify_sub + compcert.cfrontend.Cop.sem_sub + compcert.cfrontend.Cop.sem_mul + compcert.cfrontend.Cop.sem_div + compcert.cfrontend.Cop.sem_mod + compcert.cfrontend.Cop.sem_and + compcert.cfrontend.Cop.sem_or + compcert.cfrontend.Cop.sem_xor + compcert.cfrontend.Cop.classify_shift_cases_rect + compcert.cfrontend.Cop.classify_shift_cases_ind + compcert.cfrontend.Cop.classify_shift_cases_rec + compcert.cfrontend.Cop.classify_shift_cases_sind + compcert.cfrontend.Cop.classify_shift + compcert.cfrontend.Cop.sem_shift + compcert.cfrontend.Cop.sem_shl + compcert.cfrontend.Cop.sem_shr + compcert.cfrontend.Cop.classify_cmp_cases_rect + compcert.cfrontend.Cop.classify_cmp_cases_ind + compcert.cfrontend.Cop.classify_cmp_cases_rec + compcert.cfrontend.Cop.classify_cmp_cases_sind + compcert.cfrontend.Cop.classify_cmp + compcert.cfrontend.Cop.cmp_ptr + compcert.cfrontend.Cop.sem_cmp + compcert.cfrontend.Cop.classify_fun_cases_rect + compcert.cfrontend.Cop.classify_fun_cases_ind + compcert.cfrontend.Cop.classify_fun_cases_rec + compcert.cfrontend.Cop.classify_fun_cases_sind + compcert.cfrontend.Cop.classify_fun + compcert.cfrontend.Cop.classify_switch_cases_rect + compcert.cfrontend.Cop.classify_switch_cases_ind + compcert.cfrontend.Cop.classify_switch_cases_rec + compcert.cfrontend.Cop.classify_switch_cases_sind + compcert.cfrontend.Cop.classify_switch + compcert.cfrontend.Cop.sem_switch_arg + compcert.cfrontend.Cop.sem_unary_operation + compcert.cfrontend.Cop.sem_binary_operation + compcert.cfrontend.Cop.sem_incrdecr + compcert.cfrontend.Cop.incrdecr_type + compcert.cfrontend.Cop.chunk_for_carrier + compcert.cfrontend.Cop.bitsize_carrier + compcert.cfrontend.Cop.first_bit + compcert.cfrontend.Cop.bitfield_extract + compcert.cfrontend.Cop.bitfield_normalize + compcert.cfrontend.Cop.load_bitfield_ind + compcert.cfrontend.Cop.load_bitfield_sind + compcert.cfrontend.Cop.store_bitfield_ind + compcert.cfrontend.Cop.store_bitfield_sind + compcert.cfrontend.Cop.optval_self_injects + compcert.cfrontend.Cop.val_casted_ind + compcert.cfrontend.Cop.val_casted_sind + compcert.cfrontend.Clight.expr_rect + compcert.cfrontend.Clight.expr_ind + compcert.cfrontend.Clight.expr_rec + compcert.cfrontend.Clight.expr_sind + compcert.cfrontend.Clight.typeof + compcert.cfrontend.Clight.label + compcert.cfrontend.Clight.statement_rect + compcert.cfrontend.Clight.statement_ind + compcert.cfrontend.Clight.statement_rec + compcert.cfrontend.Clight.statement_sind + compcert.cfrontend.Clight.labeled_statements_rect + compcert.cfrontend.Clight.labeled_statements_ind + compcert.cfrontend.Clight.labeled_statements_rec + compcert.cfrontend.Clight.labeled_statements_sind + compcert.cfrontend.Clight.Swhile + compcert.cfrontend.Clight.Sdowhile + compcert.cfrontend.Clight.Sfor + compcert.cfrontend.Clight.fn_return + compcert.cfrontend.Clight.fn_callconv + compcert.cfrontend.Clight.fn_params + compcert.cfrontend.Clight.fn_vars + compcert.cfrontend.Clight.fn_temps + compcert.cfrontend.Clight.fn_body + compcert.cfrontend.Clight.var_names + compcert.cfrontend.Clight.fundef + compcert.cfrontend.Clight.type_of_function + compcert.cfrontend.Clight.type_of_fundef + compcert.cfrontend.Clight.program + compcert.cfrontend.Clight.genv_genv + compcert.cfrontend.Clight.genv_cenv + compcert.cfrontend.Clight.globalenv + compcert.cfrontend.Clight.env + compcert.cfrontend.Clight.empty_env + compcert.cfrontend.Clight.temp_env + compcert.cfrontend.Clight.deref_loc_ind + compcert.cfrontend.Clight.deref_loc_sind + compcert.cfrontend.Clight.assign_loc_ind + compcert.cfrontend.Clight.assign_loc_sind + compcert.cfrontend.Clight.alloc_variables_ind + compcert.cfrontend.Clight.alloc_variables_sind + compcert.cfrontend.Clight.bind_parameters_ind + compcert.cfrontend.Clight.bind_parameters_sind + compcert.cfrontend.Clight.create_undef_temps + compcert.cfrontend.Clight.bind_parameter_temps + compcert.cfrontend.Clight.block_of_binding + compcert.cfrontend.Clight.blocks_of_env + compcert.cfrontend.Clight.set_opttemp + compcert.cfrontend.Clight.select_switch_default + compcert.cfrontend.Clight.select_switch_case + compcert.cfrontend.Clight.select_switch + compcert.cfrontend.Clight.seq_of_labeled_statement + compcert.cfrontend.Clight.eval_expr_ind + compcert.cfrontend.Clight.eval_expr_sind + compcert.cfrontend.Clight.eval_lvalue_ind + compcert.cfrontend.Clight.eval_lvalue_sind + compcert.cfrontend.Clight.eval_lvalue_ind2 + compcert.cfrontend.Clight.eval_expr_ind2 + compcert.cfrontend.Clight.eval_expr_lvalue_ind + compcert.cfrontend.Clight.eval_exprlist_ind + compcert.cfrontend.Clight.eval_exprlist_sind + compcert.cfrontend.Clight.cont_rect + compcert.cfrontend.Clight.cont_ind + compcert.cfrontend.Clight.cont_rec + compcert.cfrontend.Clight.cont_sind + compcert.cfrontend.Clight.call_cont + compcert.cfrontend.Clight.is_call_cont + compcert.cfrontend.Clight.state_rect + compcert.cfrontend.Clight.state_ind + compcert.cfrontend.Clight.state_rec + compcert.cfrontend.Clight.state_sind + compcert.cfrontend.Clight.find_label + compcert.cfrontend.Clight.find_label_ls + compcert.cfrontend.Clight.step_ind + compcert.cfrontend.Clight.step_sind + compcert.cfrontend.Clight.initial_state_ind + compcert.cfrontend.Clight.initial_state_sind + compcert.cfrontend.Clight.final_state_ind + compcert.cfrontend.Clight.final_state_sind + compcert.cfrontend.Clight.function_entry1_ind + compcert.cfrontend.Clight.function_entry1_sind + compcert.cfrontend.Clight.step1 + compcert.cfrontend.Clight.function_entry2_rect + compcert.cfrontend.Clight.function_entry2_ind + compcert.cfrontend.Clight.function_entry2_rec + compcert.cfrontend.Clight.function_entry2_sind + compcert.cfrontend.Clight.step2 + compcert.cfrontend.Clight.semantics1 + compcert.cfrontend.Clight.semantics2 +. + +Elpi cbv_expanded_reduction_definition "zarith" + Coq.PArith.BinPos.Pos.t + Coq.PArith.BinPos.Pos.succ + Coq.PArith.BinPos.Pos.add + Coq.PArith.BinPos.Pos.add_carry + Coq.PArith.BinPos.Pos.pred_double + Coq.PArith.BinPos.Pos.pred + Coq.PArith.BinPos.Pos.pred_N + Coq.PArith.BinPos.Pos.mask_rect + Coq.PArith.BinPos.Pos.mask_ind + Coq.PArith.BinPos.Pos.mask_rec + Coq.PArith.BinPos.Pos.mask_sind + Coq.PArith.BinPos.Pos.succ_double_mask + Coq.PArith.BinPos.Pos.double_mask + Coq.PArith.BinPos.Pos.double_pred_mask + Coq.PArith.BinPos.Pos.pred_mask + Coq.PArith.BinPos.Pos.sub_mask + Coq.PArith.BinPos.Pos.sub_mask_carry + Coq.PArith.BinPos.Pos.sub + Coq.PArith.BinPos.Pos.mul + Coq.PArith.BinPos.Pos.iter + Coq.PArith.BinPos.Pos.pow + Coq.PArith.BinPos.Pos.square + Coq.PArith.BinPos.Pos.div2 + Coq.PArith.BinPos.Pos.div2_up + Coq.PArith.BinPos.Pos.size_nat + Coq.PArith.BinPos.Pos.size + Coq.PArith.BinPos.Pos.compare_cont + Coq.PArith.BinPos.Pos.compare + Coq.PArith.BinPos.Pos.min + Coq.PArith.BinPos.Pos.max + Coq.PArith.BinPos.Pos.eqb + Coq.PArith.BinPos.Pos.leb + Coq.PArith.BinPos.Pos.ltb + Coq.PArith.BinPos.Pos.sqrtrem_step + Coq.PArith.BinPos.Pos.sqrtrem + Coq.PArith.BinPos.Pos.sqrt + Coq.PArith.BinPos.Pos.divide + Coq.PArith.BinPos.Pos.gcdn + Coq.PArith.BinPos.Pos.gcd + Coq.PArith.BinPos.Pos.ggcdn + Coq.PArith.BinPos.Pos.ggcd + Coq.PArith.BinPos.Pos.Nsucc_double + Coq.PArith.BinPos.Pos.Ndouble + Coq.PArith.BinPos.Pos.lor + Coq.PArith.BinPos.Pos.land + Coq.PArith.BinPos.Pos.ldiff + Coq.PArith.BinPos.Pos.lxor + Coq.PArith.BinPos.Pos.shiftl_nat + Coq.PArith.BinPos.Pos.shiftr_nat + Coq.PArith.BinPos.Pos.shiftl + Coq.PArith.BinPos.Pos.shiftr + Coq.PArith.BinPos.Pos.testbit_nat + Coq.PArith.BinPos.Pos.testbit + Coq.PArith.BinPos.Pos.iter_op + Coq.PArith.BinPos.Pos.to_nat + Coq.PArith.BinPos.Pos.of_nat + Coq.PArith.BinPos.Pos.of_succ_nat + Coq.PArith.BinPos.Pos.of_uint_acc + Coq.PArith.BinPos.Pos.of_uint + Coq.PArith.BinPos.Pos.of_hex_uint_acc + Coq.PArith.BinPos.Pos.of_hex_uint + Coq.PArith.BinPos.Pos.of_num_uint + Coq.PArith.BinPos.Pos.of_int + Coq.PArith.BinPos.Pos.of_hex_int + Coq.PArith.BinPos.Pos.of_num_int + Coq.PArith.BinPos.Pos.to_little_uint + Coq.PArith.BinPos.Pos.to_uint + Coq.PArith.BinPos.Pos.to_little_hex_uint + Coq.PArith.BinPos.Pos.to_hex_uint + Coq.PArith.BinPos.Pos.to_num_uint + Coq.PArith.BinPos.Pos.to_num_hex_uint + Coq.PArith.BinPos.Pos.to_int + Coq.PArith.BinPos.Pos.to_hex_int + Coq.PArith.BinPos.Pos.to_num_int + Coq.PArith.BinPos.Pos.to_num_hex_int + Coq.PArith.BinPos.Pos.eq + Coq.PArith.BinPos.Pos.eq_equiv + Coq.PArith.BinPos.Pos.eq_refl + Coq.PArith.BinPos.Pos.eq_sym + Coq.PArith.BinPos.Pos.eq_trans + Coq.PArith.BinPos.Pos.lt + Coq.PArith.BinPos.Pos.gt + Coq.PArith.BinPos.Pos.le + Coq.PArith.BinPos.Pos.ge + Coq.PArith.BinPos.Pos.eq_dec + Coq.PArith.BinPos.Pos.peano_rect + Coq.PArith.BinPos.Pos.peano_rec + Coq.PArith.BinPos.Pos.peano_ind + Coq.PArith.BinPos.Pos.PeanoView_rect + Coq.PArith.BinPos.Pos.PeanoView_ind + Coq.PArith.BinPos.Pos.PeanoView_rec + Coq.PArith.BinPos.Pos.PeanoView_sind + Coq.PArith.BinPos.Pos.peanoView_xO + Coq.PArith.BinPos.Pos.peanoView_xI + Coq.PArith.BinPos.Pos.peanoView + Coq.PArith.BinPos.Pos.PeanoView_iter + Coq.PArith.BinPos.Pos.SubMaskSpec_ind + Coq.PArith.BinPos.Pos.SubMaskSpec_sind + Coq.PArith.BinPos.Pos.eqb_spec + Coq.PArith.BinPos.Pos.switch_Eq + Coq.PArith.BinPos.Pos.mask2cmp + Coq.PArith.BinPos.Pos.leb_spec0 + Coq.PArith.BinPos.Pos.ltb_spec0 + Coq.PArith.BinPos.Pos.le_lteq + Coq.PArith.BinPos.Pos.max_case_strong + Coq.PArith.BinPos.Pos.max_case + Coq.PArith.BinPos.Pos.max_dec + Coq.PArith.BinPos.Pos.min_case_strong + Coq.PArith.BinPos.Pos.min_case + Coq.PArith.BinPos.Pos.min_dec + Coq.PArith.BinPos.Pos.SqrtSpec_ind + Coq.PArith.BinPos.Pos.SqrtSpec_sind + Coq.ZArith.BinInt.Z.t + Coq.ZArith.BinInt.Z.zero + Coq.ZArith.BinInt.Z.one + Coq.ZArith.BinInt.Z.two + Coq.ZArith.BinInt.Z.double + Coq.ZArith.BinInt.Z.succ_double + Coq.ZArith.BinInt.Z.pred_double + Coq.ZArith.BinInt.Z.pos_sub + Coq.ZArith.BinInt.Z.add + Coq.ZArith.BinInt.Z.opp + Coq.ZArith.BinInt.Z.succ + Coq.ZArith.BinInt.Z.pred + Coq.ZArith.BinInt.Z.sub + Coq.ZArith.BinInt.Z.mul + Coq.ZArith.BinInt.Z.pow_pos + Coq.ZArith.BinInt.Z.pow + Coq.ZArith.BinInt.Z.square + Coq.ZArith.BinInt.Z.compare + Coq.ZArith.BinInt.Z.sgn + Coq.ZArith.BinInt.Z.leb + Coq.ZArith.BinInt.Z.ltb + Coq.ZArith.BinInt.Z.geb + Coq.ZArith.BinInt.Z.gtb + Coq.ZArith.BinInt.Z.eqb + Coq.ZArith.BinInt.Z.max + Coq.ZArith.BinInt.Z.min + Coq.ZArith.BinInt.Z.abs + Coq.ZArith.BinInt.Z.abs_nat + Coq.ZArith.BinInt.Z.abs_N + Coq.ZArith.BinInt.Z.to_nat + Coq.ZArith.BinInt.Z.to_N + Coq.ZArith.BinInt.Z.of_nat + Coq.ZArith.BinInt.Z.of_N + Coq.ZArith.BinInt.Z.to_pos + Coq.ZArith.BinInt.Z.of_uint + Coq.ZArith.BinInt.Z.of_hex_uint + Coq.ZArith.BinInt.Z.of_num_uint + Coq.ZArith.BinInt.Z.of_int + Coq.ZArith.BinInt.Z.of_hex_int + Coq.ZArith.BinInt.Z.of_num_int + Coq.ZArith.BinInt.Z.to_int + Coq.ZArith.BinInt.Z.to_hex_int + Coq.ZArith.BinInt.Z.to_num_int + Coq.ZArith.BinInt.Z.to_num_hex_int + Coq.ZArith.BinInt.Z.iter + Coq.ZArith.BinInt.Z.pos_div_eucl + Coq.ZArith.BinInt.Z.div_eucl + Coq.ZArith.BinInt.Z.div + Coq.ZArith.BinInt.Z.modulo + Coq.ZArith.BinInt.Z.quotrem + Coq.ZArith.BinInt.Z.quot + Coq.ZArith.BinInt.Z.rem + Coq.ZArith.BinInt.Z.even + Coq.ZArith.BinInt.Z.odd + Coq.ZArith.BinInt.Z.div2 + Coq.ZArith.BinInt.Z.quot2 + Coq.ZArith.BinInt.Z.log2 + Coq.ZArith.BinInt.Z.sqrtrem + Coq.ZArith.BinInt.Z.sqrt + Coq.ZArith.BinInt.Z.gcd + Coq.ZArith.BinInt.Z.ggcd + Coq.ZArith.BinInt.Z.testbit + Coq.ZArith.BinInt.Z.shiftl + Coq.ZArith.BinInt.Z.shiftr + Coq.ZArith.BinInt.Z.lor + Coq.ZArith.BinInt.Z.land + Coq.ZArith.BinInt.Z.ldiff + Coq.ZArith.BinInt.Z.lxor + Coq.ZArith.BinInt.Z.eq + Coq.ZArith.BinInt.Z.eq_equiv + Coq.ZArith.BinInt.Z.lt + Coq.ZArith.BinInt.Z.gt + Coq.ZArith.BinInt.Z.le + Coq.ZArith.BinInt.Z.ge + Coq.ZArith.BinInt.Z.divide + Coq.ZArith.BinInt.Z.Even + Coq.ZArith.BinInt.Z.Odd + Coq.ZArith.BinInt.Z.eq_dec + Coq.ZArith.BinInt.Z.succ_wd + Coq.ZArith.BinInt.Z.pred_wd + Coq.ZArith.BinInt.Z.opp_wd + Coq.ZArith.BinInt.Z.add_wd + Coq.ZArith.BinInt.Z.sub_wd + Coq.ZArith.BinInt.Z.mul_wd + Coq.ZArith.BinInt.Z.lt_wd + Coq.ZArith.BinInt.Z.div_wd + Coq.ZArith.BinInt.Z.mod_wd + Coq.ZArith.BinInt.Z.quot_wd + Coq.ZArith.BinInt.Z.rem_wd + Coq.ZArith.BinInt.Z.pow_wd + Coq.ZArith.BinInt.Z.testbit_wd + Coq.ZArith.BinInt.Z.leb_spec0 + Coq.ZArith.BinInt.Z.ltb_spec0 + Coq.ZArith.BinInt.Z.eq_refl + Coq.ZArith.BinInt.Z.eq_sym + Coq.ZArith.BinInt.Z.eq_trans + Coq.ZArith.BinInt.Z.lt_compat + Coq.ZArith.BinInt.Z.lt_total + Coq.ZArith.BinInt.Z.le_lteq + Coq.ZArith.BinInt.Z.mul_eq_0 + Coq.ZArith.BinInt.Z.mul_eq_0_l + Coq.ZArith.BinInt.Z.mul_eq_0_r + Coq.ZArith.BinInt.Z.mul_eq_1 + Coq.ZArith.BinInt.Z.max_case_strong + Coq.ZArith.BinInt.Z.max_case + Coq.ZArith.BinInt.Z.max_dec + Coq.ZArith.BinInt.Z.min_case_strong + Coq.ZArith.BinInt.Z.min_case + Coq.ZArith.BinInt.Z.min_dec + Coq.ZArith.BinInt.Z.mod_bound_pos + Coq.ZArith.BinInt.Z.sqrt_up + Coq.ZArith.BinInt.Z.log2_up + Coq.ZArith.BinInt.Z.divide_reflexive + Coq.ZArith.BinInt.Z.divide_transitive + Coq.ZArith.BinInt.Z.Bezout + Coq.ZArith.BinInt.Z.lcm + Coq.ZArith.BinInt.Z.eqb_spec + Coq.ZArith.BinInt.Z.b2z + Coq.ZArith.BinInt.Z.b2z_wd + Coq.ZArith.BinInt.Z.eqf + Coq.ZArith.BinInt.Z.setbit + Coq.ZArith.BinInt.Z.clearbit + Coq.ZArith.BinInt.Z.lnot + Coq.ZArith.BinInt.Z.ones +. diff --git a/elpi/cbv_symbol_lists_generated_definitions.v b/elpi/cbv_symbol_lists_generated_definitions.v new file mode 100644 index 0000000000..47e96e7b5b --- /dev/null +++ b/elpi/cbv_symbol_lists_generated_definitions.v @@ -0,0 +1,29 @@ +Require Import elpi.elpi. + +(** * ELPI based cbv reduction in parts of terms with hand crafted delta symbol lists: Common definitions *) + +(** ** Elpi Database containing some helper databases for CBV symbol list generation + helper predicates *) + +Elpi Db cbv_symbol_generated.db lp:{{ + % A database mapping reduction names (ids) to reduction flags (usually with lengthy delta expansion lists) + pred cbv-reduction i:string o:coq.redflags. + :name "cbv-reduction.fail" + cbv-reduction N _ :- coq.error "cbv-reduction: entry with name" N "not found!". +}}. + +Elpi Command cbv_expanded_reduction_definition. +Elpi Accumulate Db cbv_symbol_generated.db. +Elpi Accumulate lp:{{ + % Convert a symbol name to a redflag + pred argument->redflag i:argument, o:coq.redflag. + argument->redflag (str N) (coq.redflags.const C) :- coq.locate N (const C), !. + argument->redflag (str N) _ :- coq.error "cbv_expanded_reduction_definition: the given name" N "is not a constant!". + argument->redflag A _ :- coq.error "cbv_expanded_reduction_definition: the given argument" A "is not a string". + + main [str NAME|ARGUMENTS] :- + std.map ARGUMENTS argument->redflag LR, + coq.redflags.add coq.redflags.betaiotazeta LR RF, + coq.elpi.accumulate _ "cbv_symbol_generated.db" (clause _ (before "cbv-reduction.fail") (cbv-reduction NAME RF)) + . +}}. +Elpi Typecheck. diff --git a/elpi/cbv_symbol_lists_generator.v b/elpi/cbv_symbol_lists_generator.v new file mode 100644 index 0000000000..5f7e8330c6 --- /dev/null +++ b/elpi/cbv_symbol_lists_generator.v @@ -0,0 +1,61 @@ +(** * Create file with hand craftes symbol lists *) + +(** ATTENTION: running the generator require coq-elpi >= 1.16.0. *) +(** For this reason we currently generate a checked in file with symbol lists. *) + +Require Import elpi.elpi. +Require Import VST.elpi.cbv_symbol_lists_generator_definitions. + +(** ** Require all modules, for which we want to create symbol lists below *) + +From VST Require floyd.proofauto floyd.library. +From compcert Require Import Coqlib Integers Floats AST Ctypes Cop Clight Clightdefs. + +(** ** Map modules which are not file level modules to the corresponding file level module *) + +Elpi cbv_add_module_mapping compcert.lib.Maps.PTree compcert.lib.Maps. +Elpi cbv_add_module_mapping VST.veric.mpred.Map VST.veric.mpred. +Elpi cbv_add_module_mapping Coq.ZArith.BinInt.Z ZArith.BinInt. +Elpi cbv_add_module_mapping Coq.PArith.BinPos.Pos PArith.BinPos. + +(** ** Add definitions of reduction symbol lists *) + +(** +The first entry in the list is the name of the generated delta reduction symbol list (used with "cbv_nr" tactic). +Further entries are intepreted as follows: +- if prefixed with "ADD." the entry adds a single (preferably fully ualified) symbol to the delta reduction symbol list +- if prefixed with "REMOVE." the entry removes a single (preferably fully ualified) symbol from the (so far constructed) delta reduction symbol listt +- otherwise the entry is intepreted as module path and all transparanet definitions from the module (not recursive) are added to the delta reduction symbol list +- if the module path of a module or an individual symbol is not a file level module (one which can be loaded with "Require") a name mapping must be given with cbv_add_module_mapping (see above). +*) + +Elpi cbv_add_reduction_definition + "msubst_denote_tc_assert" + compcert.cfrontend.Clight + compcert.cfrontend.Cop + compcert.cfrontend.Ctypes + compcert.export.Ctypesdefs + compcert.lib.Maps.PTree + compcert.aarch64.Archi + VST.floyd.local2ptree_eval + VST.floyd.local2ptree_typecheck + VST.veric.Clight_Cop2 + VST.veric.expr + VST.veric.lift + VST.veric.mpred + REMOVE.VST.veric.mpred.mpred + VST.veric.mpred.Map + VST.veric.SeparationLogic + VST.veric.val_lemmas + . + +Elpi cbv_add_reduction_definition + "zarith" + ZArith.BinInt.Z + PArith.BinPos.Pos + . + +(** ** Generate file with expaned reduction definitions *) + +Elpi cbv_write_reduction_definitions "elpi/cbv_symbol_lists_generated.v". +Elpi cbv_write_reduction_definitions_ltac2 "ltac2/cbv_symbol_lists_generated.v". diff --git a/elpi/cbv_symbol_lists_generator_definitions.v b/elpi/cbv_symbol_lists_generator_definitions.v new file mode 100644 index 0000000000..804f92dd4b --- /dev/null +++ b/elpi/cbv_symbol_lists_generator_definitions.v @@ -0,0 +1,209 @@ +Require Import elpi.elpi. + +(** * ELPI based cbv reduction in parts of terms with hand crafted delta symbol lists: Common definitions *) + +(** ** Elpi Database containing some helper databases for CBV symbol list generation + helper predicates *) + +Elpi Db cbv_symbol_generator.db lp:{{ + % A database mapping reduction names (ids) to a list of constants. + % Note: all parameters are "output" because this predicate is enumerated with "forall". + pred cbv-reduction-definition o:string, o:list constant. + :name "cbv-reduction-definition.fail" + cbv-reduction-definition _ _ :- fail. + + % A database mapping module paths to file level module paths which can be used for Require. + % That is path components refering to modules defined with Module are stripped away. + % The default is that both are the same. + pred module-path->require-path i:string, o:string. + :name "module-path->require-path.default" + module-path->require-path MP MP. + + % Remove duplicates from a list + pred remove-duplicates i:list A, o:list A. + remove-duplicates [] []. + remove-duplicates [H|T] L :- std.mem! T H, remove-duplicates T L, !. + remove-duplicates [H|T] [H|L] :- remove-duplicates T L. + + % Convert a contant to a fully qualified name + pred constant->name i:constant, o:string. + constant->name C N :- + coq.gref->string (const C) N. + + % Extract the module part of the fully qualified name of a constant + pred constant->module-path i:constant o:string. + constant->module-path C MP :- + coq.gref->string (const C) CS, + rex.replace "\.[^.]+$" "" CS MP. + + % Get the list of require modules from a cbv-reduction-definition entry + pred cbv-reduction-definition->require-list i:prop, o:list string. + cbv-reduction-definition->require-list (cbv-reduction-definition _NAME CONSTANTS) REQUIRES :- + std.map CONSTANTS constant->module-path LM, + std.map LM module-path->require-path LR, + remove-duplicates LR REQUIRES. + + % output a "Require Import" command + pred output-require i:out_stream, i:string. + output-require OS RP :- + output OS "Require Import ", + output OS RP, + output OS ".\n". +}}. + +(** ** Elpi Command to add an entry into the module path -> require path database *) + +Elpi Command cbv_add_module_mapping. +Elpi Accumulate Db cbv_symbol_generator.db. +Elpi Accumulate lp:{{ + main [str MP, str RP] :- + coq.elpi.accumulate _ "cbv_symbol_generator.db" (clause _ (before "module-path->require-path.default") (module-path->require-path MP RP)), + coq.say "Added module path mapping" MP "->" RP. +}}. +Elpi Typecheck. + +(** ** Elpi Command to add a new reduction definition *) + +Elpi Command cbv_add_reduction_definition. +Elpi Accumulate Db cbv_symbol_generator.db. +Elpi Accumulate lp:{{ + % Filter transparnt constants from module-items + pred module-item-filter-transparent-const-gref i:module-item, o:constant. + module-item-filter-transparent-const-gref (gref (const X)) X :- not (coq.env.opaque? X). + + % Get a list of transparent definitions from a module + pred module-get-transparent-definitions i:string, o:list constant. + module-get-transparent-definitions MN LR :- + coq.locate-module MN MP, + coq.env.module MP L, + std.map-filter L module-item-filter-transparent-const-gref LR. + + % Convert a - preferably fully qualified - name to a constant + pred name->constant i:string, o:constant. + name->constant N C :- coq.locate N (const C). + name->constant N _ :- coq.error "name->constant: the given name" N "is not a constant!". + + % Append symbols from an argument string (either module or individual symbol prefixed with "ADD.") to a list of constants + pred filter-items i:argument, i:list constant, o:list constant. + % Individual symbols are prefixed with "ADD." + filter-items (str NAME) LCI LCO :- + rex.match "^ADD\\." NAME, + rex.replace "^ADD\\." "" NAME NAMES, + name->constant NAMES C, + LCO = [C|LCI], !. + % Removals (exclusions on the already constructed list) are prefixed with "REMOVE." + filter-items (str NAME) LCI LCO :- + rex.match "^REMOVE\\." NAME, + rex.replace "^REMOVE\\." "" NAME NAMES, + name->constant NAMES C, + std.filter LCI (x\ not (x = C)) LCO, !. + % Otherwise we habe a module + filter-items (str NAME) LCI LCO :- + module-get-transparent-definitions NAME LC, + std.append LC LCI LCO. + % In case this is not a string -> fail + filter-items I _ _ :- coq.error "cbv_add_reduction_definition: illegal command line item (should all be strings)" I. + + main [str NAME|ENTRIES] :- + std.fold ENTRIES [] filter-items CONSTANTS, + coq.elpi.accumulate _ "cbv_symbol_generator.db" (clause _ (before "cbv-reduction-definition.fail") (cbv-reduction-definition NAME CONSTANTS)), + coq.say "Added reduction definition" NAME "containing" {std.length CONSTANTS} "definitions." + . +}}. +Elpi Typecheck. + +(** ** Elpi Command to add write *all* defined reductions to a file in Elpi format *) + +Elpi Command cbv_write_reduction_definitions. +Elpi Accumulate Db cbv_symbol_generator.db. +Elpi Accumulate lp:{{ + % output a constant + pred output-constant i:out_stream, i:constant. + output-constant OS C :- + constant->name C N, + output OS " ", + output OS N, + output OS "\n". + + % Output a cbv-reduction-definition as cbv_expanded_reduction_definition + pred output-cbv-reduction-definition i:out_stream, i:prop. + output-cbv-reduction-definition OS (cbv-reduction-definition NAME CONSTANTS) :- + output OS "\n", + output OS "Elpi cbv_expanded_reduction_definition \"", + output OS NAME, + output OS "\"\n", + std.forall CONSTANTS (output-constant OS), + output OS ".\n". + + % Main function of command + main [str FILEPATH] :- + % Get list of reduction definitions + std.findall (cbv-reduction-definition _ _) LRD, + + % Get list of Require commands from reduction definitions + std.map LRD cbv-reduction-definition->require-list LLRP, + std.flatten LLRP LRPD, + remove-duplicates LRPD LRP, + + % Write Coq file + open_out FILEPATH OSTREAM, + output OSTREAM "(* This file has been auto-generated by elpi/cbv_symbol_lists_generator.v - DO NOT MODIFY! *)\n", + output OSTREAM "Require Import elpi.elpi.\n", + output OSTREAM "Require Import VST.elpi.cbv_symbol_lists_generated_definitions.\n", + output OSTREAM "\n", + std.forall LRP (output-require OSTREAM), + std.forall LRD (output-cbv-reduction-definition OSTREAM), + close_out OSTREAM + . +}}. +Elpi Typecheck. + +(** ** Elpi Command to add write *all* defined reductions to a file in Ltac2 format *) + +Elpi Command cbv_write_reduction_definitions_ltac2. +Elpi Accumulate Db cbv_symbol_generator.db. +Elpi Accumulate lp:{{ + % output a constant + pred output-constant i:out_stream, i:constant. + output-constant OS C :- + constant->name C N, + output OS " reference:(", + output OS N, + output OS ")". + + % Like std.forall but calls a second function without arguments between any two list elements + pred forall-sep i:list A, i:(A -> prop), i:prop. + forall-sep [] _ _. + forall-sep [X] P _ :- P X, !. + forall-sep [X|L] P S :- P X, S, forall-sep L P S. + + % Output a cbv-reduction-definition as cbv_expanded_reduction_definition + pred output-cbv-reduction-definition i:out_stream, i:prop. + output-cbv-reduction-definition OS (cbv-reduction-definition NAME CONSTANTS) :- + output OS "\n", + output OS "Ltac2 reduction_symbol_list_", + output OS NAME, + output OS "() : Std.reference list := [\n", + forall-sep CONSTANTS (output-constant OS) (output OS ";\n"), + output OS "\n].\n". + + % Main function of command + main [str FILEPATH] :- + % Get list of reduction definitions + std.findall (cbv-reduction-definition _ _) LRD, + + % Get list of Require commands from reduction definitions + std.map LRD cbv-reduction-definition->require-list LLRP, + std.flatten LLRP LRPD, + remove-duplicates LRPD LRP, + + % Write Coq file + open_out FILEPATH OSTREAM, + output OSTREAM "(* This file has been auto-generated by elpi/cbv_symbol_lists_generator.v - DO NOT MODIFY! *)\n", + output OSTREAM "Require Import Ltac2.Ltac2.\n", + output OSTREAM "\n", + std.forall LRP (output-require OSTREAM), + std.forall LRD (output-cbv-reduction-definition OSTREAM), + close_out OSTREAM + . +}}. +Elpi Typecheck. diff --git a/elpi/simpl_by_cbv.v b/elpi/simpl_by_cbv.v new file mode 100644 index 0000000000..350f63330c --- /dev/null +++ b/elpi/simpl_by_cbv.v @@ -0,0 +1,118 @@ +(** * Define tactics which do a cbv reduction restricted to a tailored delta list and optionally to certain parts of a term *) + +Require Import elpi.elpi. +(* This file contains symbol lists for delta reductions tailored for specific applications *) +Require Export VST.elpi.cbv_symbol_lists_generated. + +(* This defines Evar Etempvar *) +Require Import compcert.cfrontend.Clight. + +(** Elpi database with common definitions for advanced CBV style computation functions *) + +Elpi Db restricted_cbv.db lp:{{ + %%% Simple utility predicates + + % Convert a constant to a reduction flag + pred constant->redflag i:constant, o:coq.redflag. + constant->redflag C (coq.redflags.const C). + + %%% VST specifi tactic: find local symbols - more specifically arguments to Evar or Etempvar - in a term + %%% vst-extract-local-symbols input-term input-symbol-list extended-output-symbol-list + + pred vst-extract-local-symbols i:term, i:list constant, o:list constant. + % type prod name -> term -> (term -> term) -> term. % forall x : t, + vst-extract-local-symbols (prod N S B) I O :- pi x\ decl x N S => vst-extract-local-symbols (B x) I O. + % type let name -> term -> term -> (term -> term) -> term. % let x : T := v in + vst-extract-local-symbols (let N S _V B) I O :- pi x\ decl x N S => vst-extract-local-symbols (B x) I O. + % type app list term -> term. % app [hd|args] + vst-extract-local-symbols {{Evar lp:{{global (const VN)}} lp:{{_VT}} }} I [VN|I]. + vst-extract-local-symbols {{Etempvar lp:{{global (const VN)}} lp:{{_VT}} }} I [VN|I]. + vst-extract-local-symbols (app L) I O :- std.fold L I vst-extract-local-symbols O. + % Everything else we don't recurse into + vst-extract-local-symbols _T I I. + + %%% VST specifi tactic: extend reduction flags by local symbol found in term, + %%% vst-extend-reduction-by-local-symbols input-reduction input-term extended-reduction + pred vst-extend-reduction-by-local-symbols i: coq.redflags, i:term, o:coq.redflags. + vst-extend-reduction-by-local-symbols RF T RFX :- + vst-extract-local-symbols T [] LLS, + std.map LLS constant->redflag LLR, + coq.redflags.add RF LLR RFX. + + %%% CBV under applications of a given term + %%% cbv-under-application-of head-term reduction-flag-generation-function input-term output-term + %%% Note: the reduction flags used in general depend on the term. E.g. one might want to search for additional local symbols in the term. + + pred cbv-under-application-of i:term, i:(term -> coq.redflags -> prop), i:term, o:term. + % forall X : T, B + cbv-under-application-of HT FRF (prod X T BI) (prod X T BO) :- pi x\ decl x X T => cbv-under-application-of HT FRF (BI x) (BO x). + % let x : T := v in B + cbv-under-application-of HT FRF (let X T V BI) (let X T V BO) :- pi x\ def x X T V => cbv-under-application-of HT FRF (BI x) (BO x). + % application of HT + cbv-under-application-of HT FRF ((app [ HT | _ ]) as TI) TO :- + !, + FRF TI RFX, + @redflags! RFX => coq.reduction.cbv.norm TI TO. + % any other application + cbv-under-application-of HT FRF (app LI) (app LO) :- std.map LI (cbv-under-application-of HT FRF) LO. + % Everything else we just copy + cbv-under-application-of _ _ T T. + +}}. + +(** Tactic for cbv reduction of the goal with + - nr: named reduction from the reduction database (=delta symbol list) + Usage: cbv_nr + *) +Elpi Tactic cbv_nr. +Elpi Accumulate Db cbv_symbol_generated.db. +Elpi Accumulate Db restricted_cbv.db. +Elpi Accumulate lp:{{ + solve (goal _ _ GoalType _ [str ReductionId] as Goal) GoalReduced :- + cbv-reduction ReductionId RF, + @redflags! RF => coq.reduction.cbv.norm GoalType GoalTypeReduced, + refine {{ _ : lp:{{GoalTypeReduced}} }} Goal GoalReduced % to leave a vmcast one needs to call ltac1 + . +}}. +Elpi Typecheck. + +(** Tactic for cbv reduction of the goal with + - nr: named reduction from the reduction database (=delta symbol list) + - vstl: extend the delta reduction list with VST local symbols + Usage: cbv_nr_vstl + *) +Elpi Tactic cbv_nr_vstl. +Elpi Accumulate Db cbv_symbol_generated.db. +Elpi Accumulate Db restricted_cbv.db. +Elpi Accumulate lp:{{ + solve (goal _ _ GoalType _ [str ReductionId] as Goal) GoalReduced :- + cbv-reduction ReductionId RF, + vst-extend-reduction-by-local-symbols RF GoalType RFX, + @redflags! RFX => coq.reduction.cbv.norm GoalType GoalTypeReduced, + refine {{ _ : lp:{{GoalTypeReduced}} }} Goal GoalReduced % to leave a vmcast one needs to call ltac1 + . +}}. +Elpi Typecheck. + +(** Tactic for cbv reduction of the goal with + - nr: named reduction from the reduction database (=delta symbol list) + - uao: reduction only under applications of the given head symbol + - vstl: extend the delta reduction list with VST local symbols + Usage: cbv_nr_uao_vstl + *) +Elpi Tactic cbv_nr_uao_vstl. +Elpi Accumulate Db cbv_symbol_generated.db. +Elpi Accumulate Db restricted_cbv.db. +Elpi Accumulate lp:{{ + solve (goal _ _ GoalType _ [str ReductionId, trm HeadTerm] as Goal) GoalReduced :- + cbv-reduction ReductionId RF, + cbv-under-application-of HeadTerm (vst-extend-reduction-by-local-symbols RF) GoalType GoalTypeReduced, + refine {{ _ : lp:{{GoalTypeReduced}} }} Goal GoalReduced % to leave a vmcast one needs to call ltac1 + . +}}. +Elpi Typecheck. + +(** Ltac wrappers for the elpi tactics for specific cases *) + +(* Ltac simpl_msubst_denote_tc_assert := simpl VST.floyd.local2ptree_typecheck.msubst_denote_tc_assert. *) +Ltac simpl_msubst_denote_tc_assert := elpi cbv_nr_uao_vstl "msubst_denote_tc_assert" (@VST.floyd.local2ptree_typecheck.msubst_denote_tc_assert). diff --git a/floyd/go_lower.v b/floyd/go_lower.v index 1166bb18e8..7b3da3e54d 100644 --- a/floyd/go_lower.v +++ b/floyd/go_lower.v @@ -5,6 +5,7 @@ Require Import VST.floyd.local2ptree_denote. Require Import VST.floyd.local2ptree_eval. Require Import VST.floyd.local2ptree_typecheck. Require Import VST.floyd.semax_tactics. +Require Export VST.ltac2.simpl_by_cbv. Import LiftNotation. Import compcert.lib.Maps. @@ -912,7 +913,7 @@ unfold fold_right_sepcon; fold fold_right_sepcon; rewrite ?sepcon_emp; (* for th unfold_for_go_lower; simpl tc_val; cbv [typecheck_exprlist typecheck_expr]; simpl tc_andp; -simpl msubst_denote_tc_assert; +simpl_msubst_denote_tc_assert; (* HERE *) try clear dependent rho; clear_Delta ]. diff --git a/ltac2/cbv_symbol_lists_generated.v b/ltac2/cbv_symbol_lists_generated.v new file mode 100644 index 0000000000..b4b42b2363 --- /dev/null +++ b/ltac2/cbv_symbol_lists_generated.v @@ -0,0 +1,1128 @@ +(* This file has been auto-generated by elpi/cbv_symbol_lists_generator.v - DO NOT MODIFY! *) +Require Import Ltac2.Ltac2. + +Require Import VST.veric.val_lemmas. +Require Import VST.veric.SeparationLogic. +Require Import VST.veric.mpred. +Require Import VST.veric.lift. +Require Import VST.veric.expr. +Require Import VST.veric.Clight_Cop2. +Require Import VST.floyd.local2ptree_typecheck. +Require Import VST.floyd.local2ptree_eval. +Require Import compcert.aarch64.Archi. +Require Import compcert.lib.Maps. +Require Import compcert.export.Ctypesdefs. +Require Import compcert.cfrontend.Ctypes. +Require Import compcert.cfrontend.Cop. +Require Import compcert.cfrontend.Clight. +Require Import PArith.BinPos. +Require Import ZArith.BinInt. + +Ltac2 reduction_symbol_list_msubst_denote_tc_assert() : Std.reference list := [ + reference:(VST.veric.val_lemmas.is_true); + reference:(VST.veric.val_lemmas.force_val); + reference:(VST.veric.val_lemmas.force_val1); + reference:(VST.veric.val_lemmas.force_val2); + reference:(VST.veric.val_lemmas.force_int); + reference:(VST.veric.val_lemmas.force_signed_int); + reference:(VST.veric.val_lemmas.force_ptr); + reference:(VST.veric.val_lemmas.always); + reference:(VST.veric.val_lemmas.offset_val); + reference:(VST.veric.val_lemmas.range_s32); + reference:(VST.veric.val_lemmas.range_s64); + reference:(VST.veric.val_lemmas.is_long); + reference:(VST.veric.val_lemmas.is_float); + reference:(VST.veric.val_lemmas.is_single); + reference:(VST.veric.val_lemmas.is_pointer_or_null); + reference:(VST.veric.val_lemmas.is_pointer_or_integer); + reference:(VST.veric.val_lemmas.isptr); + reference:(VST.veric.SeparationLogic.Nveric); + reference:(VST.veric.SeparationLogic.Sveric); + reference:(VST.veric.SeparationLogic.Cveric); + reference:(VST.veric.SeparationLogic.Iveric); + reference:(VST.veric.SeparationLogic.Rveric); + reference:(VST.veric.SeparationLogic.SIveric); + reference:(VST.veric.SeparationLogic.CSLveric); + reference:(VST.veric.SeparationLogic.CIveric); + reference:(VST.veric.SeparationLogic.SRveric); + reference:(VST.veric.SeparationLogic.Bveric); + reference:(VST.veric.SeparationLogic.Fveric); + reference:(VST.veric.SeparationLogic.LiftNatDed'); + reference:(VST.veric.SeparationLogic.LiftSepLog'); + reference:(VST.veric.SeparationLogic.LiftClassicalSep'); + reference:(VST.veric.SeparationLogic.LiftIndir'); + reference:(VST.veric.SeparationLogic.LiftSepIndir'); + reference:(VST.veric.SeparationLogic.LiftCorableSepLog'); + reference:(VST.veric.SeparationLogic.LiftCorableIndir'); + reference:(VST.veric.SeparationLogic.local); + reference:(VST.veric.SeparationLogic.argsHaveTyps); + reference:(VST.veric.SeparationLogic.funspec_sub_si); + reference:(VST.veric.SeparationLogic.funspec_sub); + reference:(VST.veric.SeparationLogic.close_precondition); + reference:(VST.veric.SeparationLogic.argsassert2assert); + reference:(VST.veric.SeparationLogic.denote_tc_iszero); + reference:(VST.veric.SeparationLogic.denote_tc_nonzero); + reference:(VST.veric.SeparationLogic.denote_tc_igt); + reference:(VST.veric.SeparationLogic.denote_tc_lgt); + reference:(VST.veric.SeparationLogic.Zoffloat); + reference:(VST.veric.SeparationLogic.Zofsingle); + reference:(VST.veric.SeparationLogic.denote_tc_Zge); + reference:(VST.veric.SeparationLogic.denote_tc_Zle); + reference:(VST.veric.SeparationLogic.sameblock); + reference:(VST.veric.SeparationLogic.denote_tc_samebase); + reference:(VST.veric.SeparationLogic.denote_tc_nodivover); + reference:(VST.veric.SeparationLogic.denote_tc_nosignedover); + reference:(VST.veric.SeparationLogic.denote_tc_initialized); + reference:(VST.veric.SeparationLogic.denote_tc_isptr); + reference:(VST.veric.SeparationLogic.denote_tc_isint); + reference:(VST.veric.SeparationLogic.denote_tc_islong); + reference:(VST.veric.SeparationLogic.test_eq_ptrs); + reference:(VST.veric.SeparationLogic.test_order_ptrs); + reference:(VST.veric.SeparationLogic.denote_tc_test_eq); + reference:(VST.veric.SeparationLogic.denote_tc_test_order); + reference:(VST.veric.SeparationLogic.typecheck_error); + reference:(VST.veric.SeparationLogic.fool); + reference:(VST.veric.SeparationLogic.denote_tc_assert); + reference:(VST.veric.SeparationLogic.fool'); + reference:(VST.veric.SeparationLogic.cast_pointer_to_bool); + reference:(VST.veric.SeparationLogic.ext_link_prog'); + reference:(VST.veric.SeparationLogic.ext_link_prog); + reference:(VST.veric.SeparationLogic.closed_wrt_vars); + reference:(VST.veric.SeparationLogic.closed_wrt_lvars); + reference:(VST.veric.SeparationLogic.not_a_param); + reference:(VST.veric.SeparationLogic.precondition_closed); + reference:(VST.veric.SeparationLogic.typed_true); + reference:(VST.veric.SeparationLogic.typed_false); + reference:(VST.veric.SeparationLogic.substopt); + reference:(VST.veric.SeparationLogic.cast_expropt); + reference:(VST.veric.SeparationLogic.typecheck_tid_ptr_compare); + reference:(VST.veric.SeparationLogic.mapsto); + reference:(VST.veric.SeparationLogic.mapsto_); + reference:(VST.veric.SeparationLogic.mapsto_zeros); + reference:(VST.veric.SeparationLogic.globals); + reference:(VST.veric.SeparationLogic.init_data2pred); + reference:(VST.veric.SeparationLogic.init_data_size); + reference:(VST.veric.SeparationLogic.init_data_list_size); + reference:(VST.veric.SeparationLogic.init_data_list2pred); + reference:(VST.veric.SeparationLogic.readonly2share); + reference:(VST.veric.SeparationLogic.globvar2pred); + reference:(VST.veric.SeparationLogic.globals_of_env); + reference:(VST.veric.SeparationLogic.globals_of_genv); + reference:(VST.veric.SeparationLogic.globvars2pred); + reference:(VST.veric.SeparationLogic.initializer_aligned); + reference:(VST.veric.SeparationLogic.initializers_aligned); + reference:(VST.veric.SeparationLogic.funsig); + reference:(VST.veric.SeparationLogic.memory_block); + reference:(VST.veric.SeparationLogic.align_compatible); + reference:(VST.veric.SeparationLogic.size_compatible); + reference:(VST.veric.SeparationLogic.is_int32_noattr_type); + reference:(VST.veric.SeparationLogic.eval_lvar); + reference:(VST.veric.SeparationLogic.var_block); + reference:(VST.veric.SeparationLogic.stackframe_of); + reference:(VST.veric.SeparationLogic.func_ptr); + reference:(VST.veric.SeparationLogic.NDmk_funspec); + reference:(VST.veric.SeparationLogic.allp_fun_id); + reference:(VST.veric.SeparationLogic.type_of_funsig); + reference:(VST.veric.SeparationLogic.fn_funsig); + reference:(VST.veric.SeparationLogic.tc_fn_return); + reference:(VST.veric.SeparationLogic.globals_only); + reference:(VST.veric.SeparationLogic.make_args); + reference:(VST.veric.SeparationLogic.make_args'); + reference:(VST.veric.SeparationLogic.ret_temp); + reference:(VST.veric.SeparationLogic.get_result1); + reference:(VST.veric.SeparationLogic.get_result); + reference:(VST.veric.SeparationLogic.maybe_retval); + reference:(VST.veric.SeparationLogic.bind_ret); + reference:(VST.veric.SeparationLogic.overridePost); + reference:(VST.veric.SeparationLogic.existential_ret_assert); + reference:(VST.veric.SeparationLogic.normal_ret_assert); + reference:(VST.veric.SeparationLogic.frame_ret_assert); + reference:(VST.veric.SeparationLogic.switch_ret_assert); + reference:(VST.veric.SeparationLogic.with_ge); + reference:(VST.veric.SeparationLogic.prog_funct'); + reference:(VST.veric.SeparationLogic.prog_funct); + reference:(VST.veric.SeparationLogic.prog_vars'); + reference:(VST.veric.SeparationLogic.prog_vars); + reference:(VST.veric.SeparationLogic.all_initializers_aligned); + reference:(VST.veric.SeparationLogic.loop1_ret_assert); + reference:(VST.veric.SeparationLogic.loop2_ret_assert); + reference:(VST.veric.SeparationLogic.function_body_ret_assert); + reference:(VST.veric.SeparationLogic.loop_nocontinue_ret_assert); + reference:(VST.veric.SeparationLogic.tc_environ); + reference:(VST.veric.SeparationLogic.tc_temp_id); + reference:(VST.veric.SeparationLogic.typeof_temp); + reference:(VST.veric.SeparationLogic.tc_expr); + reference:(VST.veric.SeparationLogic.tc_exprlist); + reference:(VST.veric.SeparationLogic.tc_lvalue); + reference:(VST.veric.SeparationLogic.tc_expropt); + reference:(VST.veric.SeparationLogic.is_comparison); + reference:(VST.veric.SeparationLogic.blocks_match); + reference:(VST.veric.SeparationLogic.cmp_ptr_no_mem); + reference:(VST.veric.SeparationLogic.op_to_cmp); + reference:(VST.veric.SeparationLogic.arglist); + reference:(VST.veric.SeparationLogic.closed_wrt_modvars); + reference:(VST.veric.SeparationLogic.initblocksize); + reference:(VST.veric.SeparationLogic.main_pre); + reference:(VST.veric.SeparationLogic.main_post); + reference:(VST.veric.SeparationLogic.main_spec_ext'); + reference:(VST.veric.SeparationLogic.main_spec_ext); + reference:(VST.veric.SeparationLogic.match_globvars); + reference:(VST.veric.SeparationLogic.int_range); + reference:(VST.veric.SeparationLogic.semax_body_params_ok); + reference:(VST.veric.SeparationLogic.var_sizes_ok); + reference:(VST.veric.SeparationLogic.make_ext_rval); + reference:(VST.veric.SeparationLogic.tc_option_val); + reference:(VST.veric.SeparationLogic.zip_with_tl); + reference:(VST.veric.SeparationLogic.funspecs_norepeat); + reference:(VST.veric.SeparationLogic.add_funspecs); + reference:(VST.veric.SeparationLogic.funsig2signature); + reference:(VST.veric.SeparationLogic.decode_encode_val_ok); + reference:(VST.veric.SeparationLogic.numeric_type); + reference:(VST.veric.SeparationLogic.subp_sepcon_mpred); + reference:(VST.veric.SeparationLogic.unfold_Ssequence); + reference:(VST.veric.SeparationLogic.nocontinue); + reference:(VST.veric.SeparationLogic.nocontinue_ls); + reference:(VST.veric.SeparationLogic.withtype_empty); + reference:(VST.veric.SeparationLogic.prop_Proper); + reference:(VST.veric.mpred.Map.t); + reference:(VST.veric.mpred.Map.get); + reference:(VST.veric.mpred.Map.set); + reference:(VST.veric.mpred.Map.remove); + reference:(VST.veric.mpred.Map.empty); + reference:(VST.veric.mpred.strict_bool_val); + reference:(VST.veric.mpred.type_is_by_value); + reference:(VST.veric.mpred.type_is_by_reference); + reference:(VST.veric.mpred.genviron); + reference:(VST.veric.mpred.venviron); + reference:(VST.veric.mpred.tenviron); + reference:(VST.veric.mpred.environ_rect); + reference:(VST.veric.mpred.environ_ind); + reference:(VST.veric.mpred.environ_rec); + reference:(VST.veric.mpred.environ_sind); + reference:(VST.veric.mpred.ge_of); + reference:(VST.veric.mpred.ve_of); + reference:(VST.veric.mpred.te_of); + reference:(VST.veric.mpred.any_environ); + reference:(VST.veric.mpred.argsEnviron); + reference:(VST.veric.mpred.AssertTT); + reference:(VST.veric.mpred.ArgsTT); + reference:(VST.veric.mpred.SpecTT); + reference:(VST.veric.mpred.SpecArgsTT); + reference:(VST.veric.mpred.super_non_expansive); + reference:(VST.veric.mpred.args_super_non_expansive); + reference:(VST.veric.mpred.const_super_non_expansive); + reference:(VST.veric.mpred.AssertListTT); + reference:(VST.veric.mpred.super_non_expansive_list); + reference:(VST.veric.mpred.args_const_super_non_expansive); + reference:(VST.veric.mpred.funspec_rect); + reference:(VST.veric.mpred.funspec_ind); + reference:(VST.veric.mpred.funspec_rec); + reference:(VST.veric.mpred.funspec_sind); + reference:(VST.veric.mpred.varspecs); + reference:(VST.veric.mpred.funspecs); + reference:(VST.veric.mpred.assert); + reference:(VST.veric.mpred.argsassert); + reference:(VST.veric.mpred.packPQ); + reference:(VST.veric.mpred.int_range); + reference:(VST.veric.mpred.typelist_of_type_list); + reference:(VST.veric.mpred.type_of_funspec); + reference:(VST.veric.mpred.typelist2list); + reference:(VST.veric.mpred.idset); + reference:(VST.veric.mpred.idset0); + reference:(VST.veric.mpred.idset1); + reference:(VST.veric.mpred.insert_idset); + reference:(VST.veric.mpred.eval_id); + reference:(VST.veric.mpred.env_set); + reference:(VST.veric.mpred.make_tycontext_s); + reference:(VST.veric.mpred.lift0); + reference:(VST.veric.mpred.lift1); + reference:(VST.veric.mpred.lift2); + reference:(VST.veric.mpred.lift3); + reference:(VST.veric.mpred.lift4); + reference:(VST.veric.mpred.alift0); + reference:(VST.veric.mpred.alift1); + reference:(VST.veric.mpred.alift2); + reference:(VST.veric.mpred.alift3); + reference:(VST.veric.mpred.alift4); + reference:(VST.veric.mpred.LiftEnviron); + reference:(VST.veric.mpred.LiftAEnviron); + reference:(VST.veric.lift.lift_S); + reference:(VST.veric.lift.lift_T); + reference:(VST.veric.lift.lift_prod); + reference:(VST.veric.lift.lift_last); + reference:(VST.veric.lift.lifted); + reference:(VST.veric.lift.lift_curry); + reference:(VST.veric.lift.lift_uncurry_open); + reference:(VST.veric.lift.Tend); + reference:(VST.veric.lift.Tarrow); + reference:(VST.veric.lift.lift); + reference:(VST.veric.lift.liftx); + reference:(VST.veric.expr.sizeof); + reference:(VST.veric.expr.alignof); + reference:(VST.veric.expr.eval_unop); + reference:(VST.veric.expr.op_to_cmp); + reference:(VST.veric.expr.is_comparison); + reference:(VST.veric.expr.eval_binop); + reference:(VST.veric.expr.eval_cast); + reference:(VST.veric.expr.eval_field); + reference:(VST.veric.expr.eval_var); + reference:(VST.veric.expr.deref_noload); + reference:(VST.veric.expr.eval_expr); + reference:(VST.veric.expr.eval_lvalue); + reference:(VST.veric.expr.eval_exprlist); + reference:(VST.veric.expr.eval_expropt); + reference:(VST.veric.expr.bool_type); + reference:(VST.veric.expr.is_scalar_type); + reference:(VST.veric.expr.is_int_type); + reference:(VST.veric.expr.is_int32_type); + reference:(VST.veric.expr.is_long_type); + reference:(VST.veric.expr.is_ptrofs_type); + reference:(VST.veric.expr.is_float_type); + reference:(VST.veric.expr.is_single_type); + reference:(VST.veric.expr.is_anyfloat_type); + reference:(VST.veric.expr.is_pointer_type); + reference:(VST.veric.expr.tc_error_rect); + reference:(VST.veric.expr.tc_error_ind); + reference:(VST.veric.expr.tc_error_rec); + reference:(VST.veric.expr.tc_error_sind); + reference:(VST.veric.expr.tc_assert_rect); + reference:(VST.veric.expr.tc_assert_ind); + reference:(VST.veric.expr.tc_assert_rec); + reference:(VST.veric.expr.tc_assert_sind); + reference:(VST.veric.expr.tc_noproof); + reference:(VST.veric.expr.tc_iszero); + reference:(VST.veric.expr.tc_nonzero); + reference:(VST.veric.expr.tc_test_eq); + reference:(VST.veric.expr.tc_test_order); + reference:(VST.veric.expr.tc_nodivover); + reference:(VST.veric.expr.if_expr_signed); + reference:(VST.veric.expr.tc_nobinover); + reference:(VST.veric.expr.tc_andp); + reference:(VST.veric.expr.tc_orp); + reference:(VST.veric.expr.tc_bool); + reference:(VST.veric.expr.check_pp_int); + reference:(VST.veric.expr.binarithType); + reference:(VST.veric.expr.is_numeric_type); + reference:(VST.veric.expr.tc_ilt); + reference:(VST.veric.expr.tc_llt); + reference:(VST.veric.expr.tc_int_or_ptr_type); + reference:(VST.veric.expr.isUnOpResultType); + reference:(VST.veric.expr.isBinOpResultType); + reference:(VST.veric.expr.isCastResultType); + reference:(VST.veric.expr.is_neutral_cast); + reference:(VST.veric.expr.get_var_type); + reference:(VST.veric.expr.same_base_type); + reference:(VST.veric.expr.typecheck_expr); + reference:(VST.veric.expr.typecheck_lvalue); + reference:(VST.veric.expr.implicit_deref); + reference:(VST.veric.expr.typecheck_temp_id); + reference:(VST.veric.expr.tc_might_be_true); + reference:(VST.veric.expr.tc_always_true); + reference:(VST.veric.expr.typecheck_b); + reference:(VST.veric.expr.typecheck_pure_b); + reference:(VST.veric.expr.typecheck_exprlist); + reference:(VST.veric.expr.match_fsig_aux); + reference:(VST.veric.expr.match_fsig); + reference:(VST.veric.expr.expr_closed_wrt_vars); + reference:(VST.veric.expr.lvalue_closed_wrt_vars); + reference:(VST.veric.expr.typecheck_store); + reference:(VST.veric.expr.valid_pointer'); + reference:(VST.veric.expr.valid_pointer); + reference:(VST.veric.expr.weak_valid_pointer); + reference:(VST.veric.expr.funsig_of_function); + reference:(VST.veric.expr.subsumespec); + reference:(VST.veric.expr.tycontext_sub); + reference:(VST.veric.expr.cenv_sub); + reference:(VST.veric.expr.ha_env_cs_sub); + reference:(VST.veric.expr.la_env_cs_sub); + reference:(VST.veric.expr.cspecs_sub); + reference:(VST.veric.Clight_Cop2.sem_cast_pointer); + reference:(VST.veric.Clight_Cop2.sem_cast_i2i); + reference:(VST.veric.Clight_Cop2.sem_cast_i2bool); + reference:(VST.veric.Clight_Cop2.sem_cast_l2bool); + reference:(VST.veric.Clight_Cop2.sem_cast_l2l); + reference:(VST.veric.Clight_Cop2.sem_cast_i2l); + reference:(VST.veric.Clight_Cop2.sem_cast_l2i); + reference:(VST.veric.Clight_Cop2.sem_cast_struct); + reference:(VST.veric.Clight_Cop2.sem_cast_union); + reference:(VST.veric.Clight_Cop2.sem_cast_f2f); + reference:(VST.veric.Clight_Cop2.sem_cast_s2s); + reference:(VST.veric.Clight_Cop2.sem_cast_s2f); + reference:(VST.veric.Clight_Cop2.sem_cast_f2s); + reference:(VST.veric.Clight_Cop2.sem_cast_i2f); + reference:(VST.veric.Clight_Cop2.sem_cast_i2s); + reference:(VST.veric.Clight_Cop2.sem_cast_f2i); + reference:(VST.veric.Clight_Cop2.sem_cast_s2i); + reference:(VST.veric.Clight_Cop2.sem_cast_f2bool); + reference:(VST.veric.Clight_Cop2.sem_cast_s2bool); + reference:(VST.veric.Clight_Cop2.sem_cast_l2f); + reference:(VST.veric.Clight_Cop2.sem_cast_l2s); + reference:(VST.veric.Clight_Cop2.sem_cast_f2l); + reference:(VST.veric.Clight_Cop2.sem_cast_s2l); + reference:(VST.veric.Clight_Cop2.classify_cast); + reference:(VST.veric.Clight_Cop2.sem_cast); + reference:(VST.veric.Clight_Cop2.sem_notbool); + reference:(VST.veric.Clight_Cop2.sem_neg_i); + reference:(VST.veric.Clight_Cop2.sem_neg_f); + reference:(VST.veric.Clight_Cop2.sem_neg_s); + reference:(VST.veric.Clight_Cop2.sem_neg_l); + reference:(VST.veric.Clight_Cop2.sem_neg); + reference:(VST.veric.Clight_Cop2.sem_absfloat_i); + reference:(VST.veric.Clight_Cop2.sem_absfloat_f); + reference:(VST.veric.Clight_Cop2.sem_absfloat_s); + reference:(VST.veric.Clight_Cop2.sem_absfloat_l); + reference:(VST.veric.Clight_Cop2.sem_absfloat); + reference:(VST.veric.Clight_Cop2.sem_notint_i); + reference:(VST.veric.Clight_Cop2.sem_notint_l); + reference:(VST.veric.Clight_Cop2.sem_notint); + reference:(VST.veric.Clight_Cop2.both_int); + reference:(VST.veric.Clight_Cop2.both_long); + reference:(VST.veric.Clight_Cop2.both_float); + reference:(VST.veric.Clight_Cop2.both_single); + reference:(VST.veric.Clight_Cop2.sem_binarith); + reference:(VST.veric.Clight_Cop2.sem_add_ptr_int); + reference:(VST.veric.Clight_Cop2.sem_add_int_ptr); + reference:(VST.veric.Clight_Cop2.sem_add_ptr_long); + reference:(VST.veric.Clight_Cop2.sem_add_long_ptr); + reference:(VST.veric.Clight_Cop2.sem_add); + reference:(VST.veric.Clight_Cop2.sem_sub_pi); + reference:(VST.veric.Clight_Cop2.sem_sub_pl); + reference:(VST.veric.Clight_Cop2.sem_sub_pp); + reference:(VST.veric.Clight_Cop2.sem_sub_default); + reference:(VST.veric.Clight_Cop2.sem_sub); + reference:(VST.veric.Clight_Cop2.sem_mul); + reference:(VST.veric.Clight_Cop2.sem_div); + reference:(VST.veric.Clight_Cop2.sem_mod); + reference:(VST.veric.Clight_Cop2.sem_and); + reference:(VST.veric.Clight_Cop2.sem_or); + reference:(VST.veric.Clight_Cop2.sem_xor); + reference:(VST.veric.Clight_Cop2.sem_shift_ii); + reference:(VST.veric.Clight_Cop2.sem_shift_il); + reference:(VST.veric.Clight_Cop2.sem_shift_li); + reference:(VST.veric.Clight_Cop2.sem_shift_ll); + reference:(VST.veric.Clight_Cop2.sem_shift); + reference:(VST.veric.Clight_Cop2.sem_shl); + reference:(VST.veric.Clight_Cop2.sem_shr); + reference:(VST.veric.Clight_Cop2.true2); + reference:(VST.veric.Clight_Cop2.sem_cmp_pp); + reference:(VST.veric.Clight_Cop2.sem_cmp_pi); + reference:(VST.veric.Clight_Cop2.sem_cmp_ip); + reference:(VST.veric.Clight_Cop2.sem_cmp_pl); + reference:(VST.veric.Clight_Cop2.sem_cmp_lp); + reference:(VST.veric.Clight_Cop2.sem_cmp_default); + reference:(VST.veric.Clight_Cop2.sem_cmp); + reference:(VST.veric.Clight_Cop2.sem_unary_operation); + reference:(VST.veric.Clight_Cop2.sem_binary_operation'); + reference:(VST.veric.Clight_Cop2.sem_incrdecr); + reference:(VST.floyd.local2ptree_typecheck.msubst_simpl_tc_assert); + reference:(VST.floyd.local2ptree_typecheck.msubst_denote_tc_assert); + reference:(VST.floyd.local2ptree_typecheck.msubst_tc_lvalue); + reference:(VST.floyd.local2ptree_typecheck.msubst_tc_expr); + reference:(VST.floyd.local2ptree_typecheck.msubst_tc_LR); + reference:(VST.floyd.local2ptree_typecheck.msubst_tc_efield); + reference:(VST.floyd.local2ptree_typecheck.msubst_tc_exprlist); + reference:(VST.floyd.local2ptree_typecheck.msubst_tc_expropt); + reference:(VST.floyd.local2ptree_typecheck.legal_tc_init); + reference:(VST.floyd.local2ptree_eval.eval_vardesc); + reference:(VST.floyd.local2ptree_eval.eval_lvardesc); + reference:(VST.floyd.local2ptree_eval.msubst_eval_expr); + reference:(VST.floyd.local2ptree_eval.msubst_eval_lvalue); + reference:(VST.floyd.local2ptree_eval.msubst_eval_LR); + reference:(VST.floyd.local2ptree_eval.msubst_eval_lvar); + reference:(compcert.aarch64.Archi.ptr64); + reference:(compcert.aarch64.Archi.big_endian); + reference:(compcert.aarch64.Archi.align_int64); + reference:(compcert.aarch64.Archi.align_float64); + reference:(compcert.aarch64.Archi.splitlong); + reference:(compcert.aarch64.Archi.default_nan_64); + reference:(compcert.aarch64.Archi.default_nan_32); + reference:(compcert.aarch64.Archi.choose_nan); + reference:(compcert.aarch64.Archi.choose_nan_64); + reference:(compcert.aarch64.Archi.choose_nan_32); + reference:(compcert.aarch64.Archi.fma_order); + reference:(compcert.aarch64.Archi.fma_invalid_mul_is_nan); + reference:(compcert.aarch64.Archi.float_of_single_preserves_sNaN); + reference:(compcert.aarch64.Archi.float_conversion_default_nan); + reference:(compcert.aarch64.Archi.abi_kind_rect); + reference:(compcert.aarch64.Archi.abi_kind_ind); + reference:(compcert.aarch64.Archi.abi_kind_rec); + reference:(compcert.aarch64.Archi.abi_kind_sind); + reference:(compcert.lib.Maps.PTree.elt); + reference:(compcert.lib.Maps.PTree.elt_eq); + reference:(compcert.lib.Maps.PTree.tree'_ind); + reference:(compcert.lib.Maps.PTree.t); + reference:(compcert.lib.Maps.PTree.Node); + reference:(compcert.lib.Maps.PTree.empty); + reference:(compcert.lib.Maps.PTree.get'); + reference:(compcert.lib.Maps.PTree.get); + reference:(compcert.lib.Maps.PTree.set0); + reference:(compcert.lib.Maps.PTree.set'); + reference:(compcert.lib.Maps.PTree.set); + reference:(compcert.lib.Maps.PTree.rem'); + reference:(compcert.lib.Maps.PTree.remove'); + reference:(compcert.lib.Maps.PTree.remove); + reference:(compcert.lib.Maps.PTree.not_trivially_empty); + reference:(compcert.lib.Maps.PTree.tree_case); + reference:(compcert.lib.Maps.PTree.tree_rec'); + reference:(compcert.lib.Maps.PTree.tree_rec); + reference:(compcert.lib.Maps.PTree.tree_rec2'); + reference:(compcert.lib.Maps.PTree.tree_rec2); + reference:(compcert.lib.Maps.PTree.tree_ind'_obligation_1); + reference:(compcert.lib.Maps.PTree.tree_ind'_obligation_2); + reference:(compcert.lib.Maps.PTree.tree_ind'_obligation_3); + reference:(compcert.lib.Maps.PTree.tree_ind'_obligation_4); + reference:(compcert.lib.Maps.PTree.tree_ind'_obligation_5); + reference:(compcert.lib.Maps.PTree.tree_ind'_obligation_6); + reference:(compcert.lib.Maps.PTree.tree_ind'_obligation_7); + reference:(compcert.lib.Maps.PTree.tree_ind'); + reference:(compcert.lib.Maps.PTree.tree_ind); + reference:(compcert.lib.Maps.PTree.beq'); + reference:(compcert.lib.Maps.PTree.beq); + reference:(compcert.lib.Maps.PTree.prev_append); + reference:(compcert.lib.Maps.PTree.prev); + reference:(compcert.lib.Maps.PTree.map'); + reference:(compcert.lib.Maps.PTree.map); + reference:(compcert.lib.Maps.PTree.map1'); + reference:(compcert.lib.Maps.PTree.map1); + reference:(compcert.lib.Maps.PTree.map_filter1_nonopt); + reference:(compcert.lib.Maps.PTree.map_filter1); + reference:(compcert.lib.Maps.PTree.filter1); + reference:(compcert.lib.Maps.PTree.combine); + reference:(compcert.lib.Maps.PTree.xelements'); + reference:(compcert.lib.Maps.PTree.elements); + reference:(compcert.lib.Maps.PTree.xelements); + reference:(compcert.lib.Maps.PTree.xkeys); + reference:(compcert.lib.Maps.PTree.fold'); + reference:(compcert.lib.Maps.PTree.fold); + reference:(compcert.lib.Maps.PTree.fold1'); + reference:(compcert.lib.Maps.PTree.fold1); + reference:(compcert.export.Ctypesdefs.tvoid); + reference:(compcert.export.Ctypesdefs.tschar); + reference:(compcert.export.Ctypesdefs.tuchar); + reference:(compcert.export.Ctypesdefs.tshort); + reference:(compcert.export.Ctypesdefs.tushort); + reference:(compcert.export.Ctypesdefs.tint); + reference:(compcert.export.Ctypesdefs.tuint); + reference:(compcert.export.Ctypesdefs.tbool); + reference:(compcert.export.Ctypesdefs.tlong); + reference:(compcert.export.Ctypesdefs.tulong); + reference:(compcert.export.Ctypesdefs.tfloat); + reference:(compcert.export.Ctypesdefs.tdouble); + reference:(compcert.export.Ctypesdefs.tptr); + reference:(compcert.export.Ctypesdefs.tarray); + reference:(compcert.export.Ctypesdefs.volatile_attr); + reference:(compcert.export.Ctypesdefs.tattr); + reference:(compcert.export.Ctypesdefs.tvolatile); + reference:(compcert.export.Ctypesdefs.talignas); + reference:(compcert.export.Ctypesdefs.tvolatile_alignas); + reference:(compcert.export.Ctypesdefs.append_bit_pos); + reference:(compcert.export.Ctypesdefs.append_char_pos_default); + reference:(compcert.export.Ctypesdefs.append_char_pos); + reference:(compcert.export.Ctypesdefs.ident_of_string); + reference:(compcert.export.Ctypesdefs.decode_n_bits); + reference:(compcert.export.Ctypesdefs.decode_8_bits); + reference:(compcert.export.Ctypesdefs.string_of_ident); + reference:(compcert.cfrontend.Ctypes.signedness_rect); + reference:(compcert.cfrontend.Ctypes.signedness_ind); + reference:(compcert.cfrontend.Ctypes.signedness_rec); + reference:(compcert.cfrontend.Ctypes.signedness_sind); + reference:(compcert.cfrontend.Ctypes.intsize_rect); + reference:(compcert.cfrontend.Ctypes.intsize_ind); + reference:(compcert.cfrontend.Ctypes.intsize_rec); + reference:(compcert.cfrontend.Ctypes.intsize_sind); + reference:(compcert.cfrontend.Ctypes.floatsize_rect); + reference:(compcert.cfrontend.Ctypes.floatsize_ind); + reference:(compcert.cfrontend.Ctypes.floatsize_rec); + reference:(compcert.cfrontend.Ctypes.floatsize_sind); + reference:(compcert.cfrontend.Ctypes.attr_volatile); + reference:(compcert.cfrontend.Ctypes.attr_alignas); + reference:(compcert.cfrontend.Ctypes.noattr); + reference:(compcert.cfrontend.Ctypes.type_rect); + reference:(compcert.cfrontend.Ctypes.type_ind); + reference:(compcert.cfrontend.Ctypes.type_rec); + reference:(compcert.cfrontend.Ctypes.type_sind); + reference:(compcert.cfrontend.Ctypes.typelist_rect); + reference:(compcert.cfrontend.Ctypes.typelist_ind); + reference:(compcert.cfrontend.Ctypes.typelist_rec); + reference:(compcert.cfrontend.Ctypes.typelist_sind); + reference:(compcert.cfrontend.Ctypes.intsize_eq); + reference:(compcert.cfrontend.Ctypes.signedness_eq); + reference:(compcert.cfrontend.Ctypes.attr_eq); + reference:(compcert.cfrontend.Ctypes.type_eq); + reference:(compcert.cfrontend.Ctypes.typelist_eq); + reference:(compcert.cfrontend.Ctypes.attr_of_type); + reference:(compcert.cfrontend.Ctypes.change_attributes); + reference:(compcert.cfrontend.Ctypes.remove_attributes); + reference:(compcert.cfrontend.Ctypes.attr_union); + reference:(compcert.cfrontend.Ctypes.merge_attributes); + reference:(compcert.cfrontend.Ctypes.bitsize_intsize); + reference:(compcert.cfrontend.Ctypes.struct_or_union_rect); + reference:(compcert.cfrontend.Ctypes.struct_or_union_ind); + reference:(compcert.cfrontend.Ctypes.struct_or_union_rec); + reference:(compcert.cfrontend.Ctypes.struct_or_union_sind); + reference:(compcert.cfrontend.Ctypes.member_rect); + reference:(compcert.cfrontend.Ctypes.member_ind); + reference:(compcert.cfrontend.Ctypes.member_rec); + reference:(compcert.cfrontend.Ctypes.member_sind); + reference:(compcert.cfrontend.Ctypes.members); + reference:(compcert.cfrontend.Ctypes.composite_definition_rect); + reference:(compcert.cfrontend.Ctypes.composite_definition_ind); + reference:(compcert.cfrontend.Ctypes.composite_definition_rec); + reference:(compcert.cfrontend.Ctypes.composite_definition_sind); + reference:(compcert.cfrontend.Ctypes.name_member); + reference:(compcert.cfrontend.Ctypes.type_member); + reference:(compcert.cfrontend.Ctypes.member_is_padding); + reference:(compcert.cfrontend.Ctypes.name_composite_def); + reference:(compcert.cfrontend.Ctypes.composite_def_eq); + reference:(compcert.cfrontend.Ctypes.co_su); + reference:(compcert.cfrontend.Ctypes.co_members); + reference:(compcert.cfrontend.Ctypes.co_attr); + reference:(compcert.cfrontend.Ctypes.co_sizeof); + reference:(compcert.cfrontend.Ctypes.co_alignof); + reference:(compcert.cfrontend.Ctypes.co_rank); + reference:(compcert.cfrontend.Ctypes.co_sizeof_pos); + reference:(compcert.cfrontend.Ctypes.co_alignof_two_p); + reference:(compcert.cfrontend.Ctypes.co_sizeof_alignof); + reference:(compcert.cfrontend.Ctypes.composite_env); + reference:(compcert.cfrontend.Ctypes.bitfield_rect); + reference:(compcert.cfrontend.Ctypes.bitfield_ind); + reference:(compcert.cfrontend.Ctypes.bitfield_rec); + reference:(compcert.cfrontend.Ctypes.bitfield_sind); + reference:(compcert.cfrontend.Ctypes.type_int32s); + reference:(compcert.cfrontend.Ctypes.type_bool); + reference:(compcert.cfrontend.Ctypes.typeconv); + reference:(compcert.cfrontend.Ctypes.default_argument_conversion); + reference:(compcert.cfrontend.Ctypes.complete_type); + reference:(compcert.cfrontend.Ctypes.complete_or_function_type); + reference:(compcert.cfrontend.Ctypes.align_attr); + reference:(compcert.cfrontend.Ctypes.alignof); + reference:(compcert.cfrontend.Ctypes.sizeof); + reference:(compcert.cfrontend.Ctypes.naturally_aligned); + reference:(compcert.cfrontend.Ctypes.bitalignof); + reference:(compcert.cfrontend.Ctypes.bitsizeof); + reference:(compcert.cfrontend.Ctypes.bitalignof_intsize); + reference:(compcert.cfrontend.Ctypes.next_field); + reference:(compcert.cfrontend.Ctypes.layout_field); + reference:(compcert.cfrontend.Ctypes.layout_start); + reference:(compcert.cfrontend.Ctypes.layout_width); + reference:(compcert.cfrontend.Ctypes.layout_alignment); + reference:(compcert.cfrontend.Ctypes.alignof_composite); + reference:(compcert.cfrontend.Ctypes.bitsizeof_struct); + reference:(compcert.cfrontend.Ctypes.bytes_of_bits); + reference:(compcert.cfrontend.Ctypes.sizeof_struct); + reference:(compcert.cfrontend.Ctypes.sizeof_union); + reference:(compcert.cfrontend.Ctypes.field_type); + reference:(compcert.cfrontend.Ctypes.field_offset_rec); + reference:(compcert.cfrontend.Ctypes.field_offset); + reference:(compcert.cfrontend.Ctypes.union_field_offset); + reference:(compcert.cfrontend.Ctypes.mode_rect); + reference:(compcert.cfrontend.Ctypes.mode_ind); + reference:(compcert.cfrontend.Ctypes.mode_rec); + reference:(compcert.cfrontend.Ctypes.mode_sind); + reference:(compcert.cfrontend.Ctypes.access_mode); + reference:(compcert.cfrontend.Ctypes.type_is_volatile); + reference:(compcert.cfrontend.Ctypes.alignof_blockcopy); + reference:(compcert.cfrontend.Ctypes.rank_type); + reference:(compcert.cfrontend.Ctypes.rank_members); + reference:(compcert.cfrontend.Ctypes.type_of_params); + reference:(compcert.cfrontend.Ctypes.typ_of_type); + reference:(compcert.cfrontend.Ctypes.rettype_of_type); + reference:(compcert.cfrontend.Ctypes.typlist_of_typelist); + reference:(compcert.cfrontend.Ctypes.signature_of_type); + reference:(compcert.cfrontend.Ctypes.sizeof_composite); + reference:(compcert.cfrontend.Ctypes.complete_members); + reference:(compcert.cfrontend.Ctypes.composite_of_def_obligation_1); + reference:(compcert.cfrontend.Ctypes.composite_of_def_obligation_2); + reference:(compcert.cfrontend.Ctypes.composite_of_def_obligation_3); + reference:(compcert.cfrontend.Ctypes.composite_of_def); + reference:(compcert.cfrontend.Ctypes.add_composite_definitions); + reference:(compcert.cfrontend.Ctypes.build_composite_env); + reference:(compcert.cfrontend.Ctypes.co_consistent_complete); + reference:(compcert.cfrontend.Ctypes.co_consistent_alignof); + reference:(compcert.cfrontend.Ctypes.co_consistent_sizeof); + reference:(compcert.cfrontend.Ctypes.co_consistent_rank); + reference:(compcert.cfrontend.Ctypes.composite_env_consistent); + reference:(compcert.cfrontend.Ctypes.fundef_rect); + reference:(compcert.cfrontend.Ctypes.fundef_ind); + reference:(compcert.cfrontend.Ctypes.fundef_rec); + reference:(compcert.cfrontend.Ctypes.fundef_sind); + reference:(compcert.cfrontend.Ctypes.prog_defs); + reference:(compcert.cfrontend.Ctypes.prog_public); + reference:(compcert.cfrontend.Ctypes.prog_main); + reference:(compcert.cfrontend.Ctypes.prog_types); + reference:(compcert.cfrontend.Ctypes.prog_comp_env); + reference:(compcert.cfrontend.Ctypes.prog_comp_env_eq); + reference:(compcert.cfrontend.Ctypes.program_of_program); + reference:(compcert.cfrontend.Ctypes.make_program_obligation_1); + reference:(compcert.cfrontend.Ctypes.make_program); + reference:(compcert.cfrontend.Ctypes.Linker_types_obligation_1); + reference:(compcert.cfrontend.Ctypes.Linker_types_obligation_2); + reference:(compcert.cfrontend.Ctypes.Linker_types_obligation_3); + reference:(compcert.cfrontend.Ctypes.Linker_types); + reference:(compcert.cfrontend.Ctypes.check_compat_composite); + reference:(compcert.cfrontend.Ctypes.filter_redefs); + reference:(compcert.cfrontend.Ctypes.link_composite_defs); + reference:(compcert.cfrontend.Ctypes.Linker_composite_defs_obligation_1); + reference:(compcert.cfrontend.Ctypes.Linker_composite_defs_obligation_2); + reference:(compcert.cfrontend.Ctypes.Linker_composite_defs_obligation_3); + reference:(compcert.cfrontend.Ctypes.Linker_composite_defs); + reference:(compcert.cfrontend.Ctypes.link_fundef); + reference:(compcert.cfrontend.Ctypes.linkorder_fundef_ind); + reference:(compcert.cfrontend.Ctypes.linkorder_fundef_sind); + reference:(compcert.cfrontend.Ctypes.Linker_fundef_obligation_1); + reference:(compcert.cfrontend.Ctypes.Linker_fundef_obligation_2); + reference:(compcert.cfrontend.Ctypes.Linker_fundef_obligation_3); + reference:(compcert.cfrontend.Ctypes.Linker_fundef); + reference:(compcert.cfrontend.Ctypes.lift_option); + reference:(compcert.cfrontend.Ctypes.link_program); + reference:(compcert.cfrontend.Ctypes.linkorder_program); + reference:(compcert.cfrontend.Ctypes.Linker_program_obligation_1); + reference:(compcert.cfrontend.Ctypes.Linker_program_obligation_2); + reference:(compcert.cfrontend.Ctypes.Linker_program_obligation_3); + reference:(compcert.cfrontend.Ctypes.Linker_program); + reference:(compcert.cfrontend.Cop.unary_operation_rect); + reference:(compcert.cfrontend.Cop.unary_operation_ind); + reference:(compcert.cfrontend.Cop.unary_operation_rec); + reference:(compcert.cfrontend.Cop.unary_operation_sind); + reference:(compcert.cfrontend.Cop.binary_operation_rect); + reference:(compcert.cfrontend.Cop.binary_operation_ind); + reference:(compcert.cfrontend.Cop.binary_operation_rec); + reference:(compcert.cfrontend.Cop.binary_operation_sind); + reference:(compcert.cfrontend.Cop.incr_or_decr_rect); + reference:(compcert.cfrontend.Cop.incr_or_decr_ind); + reference:(compcert.cfrontend.Cop.incr_or_decr_rec); + reference:(compcert.cfrontend.Cop.incr_or_decr_sind); + reference:(compcert.cfrontend.Cop.classify_cast_cases_rect); + reference:(compcert.cfrontend.Cop.classify_cast_cases_ind); + reference:(compcert.cfrontend.Cop.classify_cast_cases_rec); + reference:(compcert.cfrontend.Cop.classify_cast_cases_sind); + reference:(compcert.cfrontend.Cop.classify_cast); + reference:(compcert.cfrontend.Cop.cast_int_int); + reference:(compcert.cfrontend.Cop.cast_int_float); + reference:(compcert.cfrontend.Cop.cast_float_int); + reference:(compcert.cfrontend.Cop.cast_int_single); + reference:(compcert.cfrontend.Cop.cast_single_int); + reference:(compcert.cfrontend.Cop.cast_int_long); + reference:(compcert.cfrontend.Cop.cast_long_float); + reference:(compcert.cfrontend.Cop.cast_long_single); + reference:(compcert.cfrontend.Cop.cast_float_long); + reference:(compcert.cfrontend.Cop.cast_single_long); + reference:(compcert.cfrontend.Cop.sem_cast); + reference:(compcert.cfrontend.Cop.classify_bool_cases_rect); + reference:(compcert.cfrontend.Cop.classify_bool_cases_ind); + reference:(compcert.cfrontend.Cop.classify_bool_cases_rec); + reference:(compcert.cfrontend.Cop.classify_bool_cases_sind); + reference:(compcert.cfrontend.Cop.classify_bool); + reference:(compcert.cfrontend.Cop.bool_val); + reference:(compcert.cfrontend.Cop.sem_notbool); + reference:(compcert.cfrontend.Cop.classify_neg_cases_rect); + reference:(compcert.cfrontend.Cop.classify_neg_cases_ind); + reference:(compcert.cfrontend.Cop.classify_neg_cases_rec); + reference:(compcert.cfrontend.Cop.classify_neg_cases_sind); + reference:(compcert.cfrontend.Cop.classify_neg); + reference:(compcert.cfrontend.Cop.sem_neg); + reference:(compcert.cfrontend.Cop.sem_absfloat); + reference:(compcert.cfrontend.Cop.classify_notint_cases_rect); + reference:(compcert.cfrontend.Cop.classify_notint_cases_ind); + reference:(compcert.cfrontend.Cop.classify_notint_cases_rec); + reference:(compcert.cfrontend.Cop.classify_notint_cases_sind); + reference:(compcert.cfrontend.Cop.classify_notint); + reference:(compcert.cfrontend.Cop.sem_notint); + reference:(compcert.cfrontend.Cop.binarith_cases_rect); + reference:(compcert.cfrontend.Cop.binarith_cases_ind); + reference:(compcert.cfrontend.Cop.binarith_cases_rec); + reference:(compcert.cfrontend.Cop.binarith_cases_sind); + reference:(compcert.cfrontend.Cop.classify_binarith); + reference:(compcert.cfrontend.Cop.binarith_type); + reference:(compcert.cfrontend.Cop.sem_binarith); + reference:(compcert.cfrontend.Cop.classify_add_cases_rect); + reference:(compcert.cfrontend.Cop.classify_add_cases_ind); + reference:(compcert.cfrontend.Cop.classify_add_cases_rec); + reference:(compcert.cfrontend.Cop.classify_add_cases_sind); + reference:(compcert.cfrontend.Cop.classify_add); + reference:(compcert.cfrontend.Cop.ptrofs_of_int); + reference:(compcert.cfrontend.Cop.sem_add_ptr_int); + reference:(compcert.cfrontend.Cop.sem_add_ptr_long); + reference:(compcert.cfrontend.Cop.sem_add); + reference:(compcert.cfrontend.Cop.classify_sub_cases_rect); + reference:(compcert.cfrontend.Cop.classify_sub_cases_ind); + reference:(compcert.cfrontend.Cop.classify_sub_cases_rec); + reference:(compcert.cfrontend.Cop.classify_sub_cases_sind); + reference:(compcert.cfrontend.Cop.classify_sub); + reference:(compcert.cfrontend.Cop.sem_sub); + reference:(compcert.cfrontend.Cop.sem_mul); + reference:(compcert.cfrontend.Cop.sem_div); + reference:(compcert.cfrontend.Cop.sem_mod); + reference:(compcert.cfrontend.Cop.sem_and); + reference:(compcert.cfrontend.Cop.sem_or); + reference:(compcert.cfrontend.Cop.sem_xor); + reference:(compcert.cfrontend.Cop.classify_shift_cases_rect); + reference:(compcert.cfrontend.Cop.classify_shift_cases_ind); + reference:(compcert.cfrontend.Cop.classify_shift_cases_rec); + reference:(compcert.cfrontend.Cop.classify_shift_cases_sind); + reference:(compcert.cfrontend.Cop.classify_shift); + reference:(compcert.cfrontend.Cop.sem_shift); + reference:(compcert.cfrontend.Cop.sem_shl); + reference:(compcert.cfrontend.Cop.sem_shr); + reference:(compcert.cfrontend.Cop.classify_cmp_cases_rect); + reference:(compcert.cfrontend.Cop.classify_cmp_cases_ind); + reference:(compcert.cfrontend.Cop.classify_cmp_cases_rec); + reference:(compcert.cfrontend.Cop.classify_cmp_cases_sind); + reference:(compcert.cfrontend.Cop.classify_cmp); + reference:(compcert.cfrontend.Cop.cmp_ptr); + reference:(compcert.cfrontend.Cop.sem_cmp); + reference:(compcert.cfrontend.Cop.classify_fun_cases_rect); + reference:(compcert.cfrontend.Cop.classify_fun_cases_ind); + reference:(compcert.cfrontend.Cop.classify_fun_cases_rec); + reference:(compcert.cfrontend.Cop.classify_fun_cases_sind); + reference:(compcert.cfrontend.Cop.classify_fun); + reference:(compcert.cfrontend.Cop.classify_switch_cases_rect); + reference:(compcert.cfrontend.Cop.classify_switch_cases_ind); + reference:(compcert.cfrontend.Cop.classify_switch_cases_rec); + reference:(compcert.cfrontend.Cop.classify_switch_cases_sind); + reference:(compcert.cfrontend.Cop.classify_switch); + reference:(compcert.cfrontend.Cop.sem_switch_arg); + reference:(compcert.cfrontend.Cop.sem_unary_operation); + reference:(compcert.cfrontend.Cop.sem_binary_operation); + reference:(compcert.cfrontend.Cop.sem_incrdecr); + reference:(compcert.cfrontend.Cop.incrdecr_type); + reference:(compcert.cfrontend.Cop.chunk_for_carrier); + reference:(compcert.cfrontend.Cop.bitsize_carrier); + reference:(compcert.cfrontend.Cop.first_bit); + reference:(compcert.cfrontend.Cop.bitfield_extract); + reference:(compcert.cfrontend.Cop.bitfield_normalize); + reference:(compcert.cfrontend.Cop.load_bitfield_ind); + reference:(compcert.cfrontend.Cop.load_bitfield_sind); + reference:(compcert.cfrontend.Cop.store_bitfield_ind); + reference:(compcert.cfrontend.Cop.store_bitfield_sind); + reference:(compcert.cfrontend.Cop.optval_self_injects); + reference:(compcert.cfrontend.Cop.val_casted_ind); + reference:(compcert.cfrontend.Cop.val_casted_sind); + reference:(compcert.cfrontend.Clight.expr_rect); + reference:(compcert.cfrontend.Clight.expr_ind); + reference:(compcert.cfrontend.Clight.expr_rec); + reference:(compcert.cfrontend.Clight.expr_sind); + reference:(compcert.cfrontend.Clight.typeof); + reference:(compcert.cfrontend.Clight.label); + reference:(compcert.cfrontend.Clight.statement_rect); + reference:(compcert.cfrontend.Clight.statement_ind); + reference:(compcert.cfrontend.Clight.statement_rec); + reference:(compcert.cfrontend.Clight.statement_sind); + reference:(compcert.cfrontend.Clight.labeled_statements_rect); + reference:(compcert.cfrontend.Clight.labeled_statements_ind); + reference:(compcert.cfrontend.Clight.labeled_statements_rec); + reference:(compcert.cfrontend.Clight.labeled_statements_sind); + reference:(compcert.cfrontend.Clight.Swhile); + reference:(compcert.cfrontend.Clight.Sdowhile); + reference:(compcert.cfrontend.Clight.Sfor); + reference:(compcert.cfrontend.Clight.fn_return); + reference:(compcert.cfrontend.Clight.fn_callconv); + reference:(compcert.cfrontend.Clight.fn_params); + reference:(compcert.cfrontend.Clight.fn_vars); + reference:(compcert.cfrontend.Clight.fn_temps); + reference:(compcert.cfrontend.Clight.fn_body); + reference:(compcert.cfrontend.Clight.var_names); + reference:(compcert.cfrontend.Clight.fundef); + reference:(compcert.cfrontend.Clight.type_of_function); + reference:(compcert.cfrontend.Clight.type_of_fundef); + reference:(compcert.cfrontend.Clight.program); + reference:(compcert.cfrontend.Clight.genv_genv); + reference:(compcert.cfrontend.Clight.genv_cenv); + reference:(compcert.cfrontend.Clight.globalenv); + reference:(compcert.cfrontend.Clight.env); + reference:(compcert.cfrontend.Clight.empty_env); + reference:(compcert.cfrontend.Clight.temp_env); + reference:(compcert.cfrontend.Clight.deref_loc_ind); + reference:(compcert.cfrontend.Clight.deref_loc_sind); + reference:(compcert.cfrontend.Clight.assign_loc_ind); + reference:(compcert.cfrontend.Clight.assign_loc_sind); + reference:(compcert.cfrontend.Clight.alloc_variables_ind); + reference:(compcert.cfrontend.Clight.alloc_variables_sind); + reference:(compcert.cfrontend.Clight.bind_parameters_ind); + reference:(compcert.cfrontend.Clight.bind_parameters_sind); + reference:(compcert.cfrontend.Clight.create_undef_temps); + reference:(compcert.cfrontend.Clight.bind_parameter_temps); + reference:(compcert.cfrontend.Clight.block_of_binding); + reference:(compcert.cfrontend.Clight.blocks_of_env); + reference:(compcert.cfrontend.Clight.set_opttemp); + reference:(compcert.cfrontend.Clight.select_switch_default); + reference:(compcert.cfrontend.Clight.select_switch_case); + reference:(compcert.cfrontend.Clight.select_switch); + reference:(compcert.cfrontend.Clight.seq_of_labeled_statement); + reference:(compcert.cfrontend.Clight.eval_expr_ind); + reference:(compcert.cfrontend.Clight.eval_expr_sind); + reference:(compcert.cfrontend.Clight.eval_lvalue_ind); + reference:(compcert.cfrontend.Clight.eval_lvalue_sind); + reference:(compcert.cfrontend.Clight.eval_lvalue_ind2); + reference:(compcert.cfrontend.Clight.eval_expr_ind2); + reference:(compcert.cfrontend.Clight.eval_expr_lvalue_ind); + reference:(compcert.cfrontend.Clight.eval_exprlist_ind); + reference:(compcert.cfrontend.Clight.eval_exprlist_sind); + reference:(compcert.cfrontend.Clight.cont_rect); + reference:(compcert.cfrontend.Clight.cont_ind); + reference:(compcert.cfrontend.Clight.cont_rec); + reference:(compcert.cfrontend.Clight.cont_sind); + reference:(compcert.cfrontend.Clight.call_cont); + reference:(compcert.cfrontend.Clight.is_call_cont); + reference:(compcert.cfrontend.Clight.state_rect); + reference:(compcert.cfrontend.Clight.state_ind); + reference:(compcert.cfrontend.Clight.state_rec); + reference:(compcert.cfrontend.Clight.state_sind); + reference:(compcert.cfrontend.Clight.find_label); + reference:(compcert.cfrontend.Clight.find_label_ls); + reference:(compcert.cfrontend.Clight.step_ind); + reference:(compcert.cfrontend.Clight.step_sind); + reference:(compcert.cfrontend.Clight.initial_state_ind); + reference:(compcert.cfrontend.Clight.initial_state_sind); + reference:(compcert.cfrontend.Clight.final_state_ind); + reference:(compcert.cfrontend.Clight.final_state_sind); + reference:(compcert.cfrontend.Clight.function_entry1_ind); + reference:(compcert.cfrontend.Clight.function_entry1_sind); + reference:(compcert.cfrontend.Clight.step1); + reference:(compcert.cfrontend.Clight.function_entry2_rect); + reference:(compcert.cfrontend.Clight.function_entry2_ind); + reference:(compcert.cfrontend.Clight.function_entry2_rec); + reference:(compcert.cfrontend.Clight.function_entry2_sind); + reference:(compcert.cfrontend.Clight.step2); + reference:(compcert.cfrontend.Clight.semantics1); + reference:(compcert.cfrontend.Clight.semantics2) +]. + +Ltac2 reduction_symbol_list_zarith() : Std.reference list := [ + reference:(Coq.PArith.BinPos.Pos.t); + reference:(Coq.PArith.BinPos.Pos.succ); + reference:(Coq.PArith.BinPos.Pos.add); + reference:(Coq.PArith.BinPos.Pos.add_carry); + reference:(Coq.PArith.BinPos.Pos.pred_double); + reference:(Coq.PArith.BinPos.Pos.pred); + reference:(Coq.PArith.BinPos.Pos.pred_N); + reference:(Coq.PArith.BinPos.Pos.mask_rect); + reference:(Coq.PArith.BinPos.Pos.mask_ind); + reference:(Coq.PArith.BinPos.Pos.mask_rec); + reference:(Coq.PArith.BinPos.Pos.mask_sind); + reference:(Coq.PArith.BinPos.Pos.succ_double_mask); + reference:(Coq.PArith.BinPos.Pos.double_mask); + reference:(Coq.PArith.BinPos.Pos.double_pred_mask); + reference:(Coq.PArith.BinPos.Pos.pred_mask); + reference:(Coq.PArith.BinPos.Pos.sub_mask); + reference:(Coq.PArith.BinPos.Pos.sub_mask_carry); + reference:(Coq.PArith.BinPos.Pos.sub); + reference:(Coq.PArith.BinPos.Pos.mul); + reference:(Coq.PArith.BinPos.Pos.iter); + reference:(Coq.PArith.BinPos.Pos.pow); + reference:(Coq.PArith.BinPos.Pos.square); + reference:(Coq.PArith.BinPos.Pos.div2); + reference:(Coq.PArith.BinPos.Pos.div2_up); + reference:(Coq.PArith.BinPos.Pos.size_nat); + reference:(Coq.PArith.BinPos.Pos.size); + reference:(Coq.PArith.BinPos.Pos.compare_cont); + reference:(Coq.PArith.BinPos.Pos.compare); + reference:(Coq.PArith.BinPos.Pos.min); + reference:(Coq.PArith.BinPos.Pos.max); + reference:(Coq.PArith.BinPos.Pos.eqb); + reference:(Coq.PArith.BinPos.Pos.leb); + reference:(Coq.PArith.BinPos.Pos.ltb); + reference:(Coq.PArith.BinPos.Pos.sqrtrem_step); + reference:(Coq.PArith.BinPos.Pos.sqrtrem); + reference:(Coq.PArith.BinPos.Pos.sqrt); + reference:(Coq.PArith.BinPos.Pos.divide); + reference:(Coq.PArith.BinPos.Pos.gcdn); + reference:(Coq.PArith.BinPos.Pos.gcd); + reference:(Coq.PArith.BinPos.Pos.ggcdn); + reference:(Coq.PArith.BinPos.Pos.ggcd); + reference:(Coq.PArith.BinPos.Pos.Nsucc_double); + reference:(Coq.PArith.BinPos.Pos.Ndouble); + reference:(Coq.PArith.BinPos.Pos.lor); + reference:(Coq.PArith.BinPos.Pos.land); + reference:(Coq.PArith.BinPos.Pos.ldiff); + reference:(Coq.PArith.BinPos.Pos.lxor); + reference:(Coq.PArith.BinPos.Pos.shiftl_nat); + reference:(Coq.PArith.BinPos.Pos.shiftr_nat); + reference:(Coq.PArith.BinPos.Pos.shiftl); + reference:(Coq.PArith.BinPos.Pos.shiftr); + reference:(Coq.PArith.BinPos.Pos.testbit_nat); + reference:(Coq.PArith.BinPos.Pos.testbit); + reference:(Coq.PArith.BinPos.Pos.iter_op); + reference:(Coq.PArith.BinPos.Pos.to_nat); + reference:(Coq.PArith.BinPos.Pos.of_nat); + reference:(Coq.PArith.BinPos.Pos.of_succ_nat); + reference:(Coq.PArith.BinPos.Pos.of_uint_acc); + reference:(Coq.PArith.BinPos.Pos.of_uint); + reference:(Coq.PArith.BinPos.Pos.of_hex_uint_acc); + reference:(Coq.PArith.BinPos.Pos.of_hex_uint); + reference:(Coq.PArith.BinPos.Pos.of_num_uint); + reference:(Coq.PArith.BinPos.Pos.of_int); + reference:(Coq.PArith.BinPos.Pos.of_hex_int); + reference:(Coq.PArith.BinPos.Pos.of_num_int); + reference:(Coq.PArith.BinPos.Pos.to_little_uint); + reference:(Coq.PArith.BinPos.Pos.to_uint); + reference:(Coq.PArith.BinPos.Pos.to_little_hex_uint); + reference:(Coq.PArith.BinPos.Pos.to_hex_uint); + reference:(Coq.PArith.BinPos.Pos.to_num_uint); + reference:(Coq.PArith.BinPos.Pos.to_num_hex_uint); + reference:(Coq.PArith.BinPos.Pos.to_int); + reference:(Coq.PArith.BinPos.Pos.to_hex_int); + reference:(Coq.PArith.BinPos.Pos.to_num_int); + reference:(Coq.PArith.BinPos.Pos.to_num_hex_int); + reference:(Coq.PArith.BinPos.Pos.eq); + reference:(Coq.PArith.BinPos.Pos.eq_equiv); + reference:(Coq.PArith.BinPos.Pos.eq_refl); + reference:(Coq.PArith.BinPos.Pos.eq_sym); + reference:(Coq.PArith.BinPos.Pos.eq_trans); + reference:(Coq.PArith.BinPos.Pos.lt); + reference:(Coq.PArith.BinPos.Pos.gt); + reference:(Coq.PArith.BinPos.Pos.le); + reference:(Coq.PArith.BinPos.Pos.ge); + reference:(Coq.PArith.BinPos.Pos.eq_dec); + reference:(Coq.PArith.BinPos.Pos.peano_rect); + reference:(Coq.PArith.BinPos.Pos.peano_rec); + reference:(Coq.PArith.BinPos.Pos.peano_ind); + reference:(Coq.PArith.BinPos.Pos.PeanoView_rect); + reference:(Coq.PArith.BinPos.Pos.PeanoView_ind); + reference:(Coq.PArith.BinPos.Pos.PeanoView_rec); + reference:(Coq.PArith.BinPos.Pos.PeanoView_sind); + reference:(Coq.PArith.BinPos.Pos.peanoView_xO); + reference:(Coq.PArith.BinPos.Pos.peanoView_xI); + reference:(Coq.PArith.BinPos.Pos.peanoView); + reference:(Coq.PArith.BinPos.Pos.PeanoView_iter); + reference:(Coq.PArith.BinPos.Pos.SubMaskSpec_ind); + reference:(Coq.PArith.BinPos.Pos.SubMaskSpec_sind); + reference:(Coq.PArith.BinPos.Pos.eqb_spec); + reference:(Coq.PArith.BinPos.Pos.switch_Eq); + reference:(Coq.PArith.BinPos.Pos.mask2cmp); + reference:(Coq.PArith.BinPos.Pos.leb_spec0); + reference:(Coq.PArith.BinPos.Pos.ltb_spec0); + reference:(Coq.PArith.BinPos.Pos.le_lteq); + reference:(Coq.PArith.BinPos.Pos.max_case_strong); + reference:(Coq.PArith.BinPos.Pos.max_case); + reference:(Coq.PArith.BinPos.Pos.max_dec); + reference:(Coq.PArith.BinPos.Pos.min_case_strong); + reference:(Coq.PArith.BinPos.Pos.min_case); + reference:(Coq.PArith.BinPos.Pos.min_dec); + reference:(Coq.PArith.BinPos.Pos.SqrtSpec_ind); + reference:(Coq.PArith.BinPos.Pos.SqrtSpec_sind); + reference:(Coq.ZArith.BinInt.Z.t); + reference:(Coq.ZArith.BinInt.Z.zero); + reference:(Coq.ZArith.BinInt.Z.one); + reference:(Coq.ZArith.BinInt.Z.two); + reference:(Coq.ZArith.BinInt.Z.double); + reference:(Coq.ZArith.BinInt.Z.succ_double); + reference:(Coq.ZArith.BinInt.Z.pred_double); + reference:(Coq.ZArith.BinInt.Z.pos_sub); + reference:(Coq.ZArith.BinInt.Z.add); + reference:(Coq.ZArith.BinInt.Z.opp); + reference:(Coq.ZArith.BinInt.Z.succ); + reference:(Coq.ZArith.BinInt.Z.pred); + reference:(Coq.ZArith.BinInt.Z.sub); + reference:(Coq.ZArith.BinInt.Z.mul); + reference:(Coq.ZArith.BinInt.Z.pow_pos); + reference:(Coq.ZArith.BinInt.Z.pow); + reference:(Coq.ZArith.BinInt.Z.square); + reference:(Coq.ZArith.BinInt.Z.compare); + reference:(Coq.ZArith.BinInt.Z.sgn); + reference:(Coq.ZArith.BinInt.Z.leb); + reference:(Coq.ZArith.BinInt.Z.ltb); + reference:(Coq.ZArith.BinInt.Z.geb); + reference:(Coq.ZArith.BinInt.Z.gtb); + reference:(Coq.ZArith.BinInt.Z.eqb); + reference:(Coq.ZArith.BinInt.Z.max); + reference:(Coq.ZArith.BinInt.Z.min); + reference:(Coq.ZArith.BinInt.Z.abs); + reference:(Coq.ZArith.BinInt.Z.abs_nat); + reference:(Coq.ZArith.BinInt.Z.abs_N); + reference:(Coq.ZArith.BinInt.Z.to_nat); + reference:(Coq.ZArith.BinInt.Z.to_N); + reference:(Coq.ZArith.BinInt.Z.of_nat); + reference:(Coq.ZArith.BinInt.Z.of_N); + reference:(Coq.ZArith.BinInt.Z.to_pos); + reference:(Coq.ZArith.BinInt.Z.of_uint); + reference:(Coq.ZArith.BinInt.Z.of_hex_uint); + reference:(Coq.ZArith.BinInt.Z.of_num_uint); + reference:(Coq.ZArith.BinInt.Z.of_int); + reference:(Coq.ZArith.BinInt.Z.of_hex_int); + reference:(Coq.ZArith.BinInt.Z.of_num_int); + reference:(Coq.ZArith.BinInt.Z.to_int); + reference:(Coq.ZArith.BinInt.Z.to_hex_int); + reference:(Coq.ZArith.BinInt.Z.to_num_int); + reference:(Coq.ZArith.BinInt.Z.to_num_hex_int); + reference:(Coq.ZArith.BinInt.Z.iter); + reference:(Coq.ZArith.BinInt.Z.pos_div_eucl); + reference:(Coq.ZArith.BinInt.Z.div_eucl); + reference:(Coq.ZArith.BinInt.Z.div); + reference:(Coq.ZArith.BinInt.Z.modulo); + reference:(Coq.ZArith.BinInt.Z.quotrem); + reference:(Coq.ZArith.BinInt.Z.quot); + reference:(Coq.ZArith.BinInt.Z.rem); + reference:(Coq.ZArith.BinInt.Z.even); + reference:(Coq.ZArith.BinInt.Z.odd); + reference:(Coq.ZArith.BinInt.Z.div2); + reference:(Coq.ZArith.BinInt.Z.quot2); + reference:(Coq.ZArith.BinInt.Z.log2); + reference:(Coq.ZArith.BinInt.Z.sqrtrem); + reference:(Coq.ZArith.BinInt.Z.sqrt); + reference:(Coq.ZArith.BinInt.Z.gcd); + reference:(Coq.ZArith.BinInt.Z.ggcd); + reference:(Coq.ZArith.BinInt.Z.testbit); + reference:(Coq.ZArith.BinInt.Z.shiftl); + reference:(Coq.ZArith.BinInt.Z.shiftr); + reference:(Coq.ZArith.BinInt.Z.lor); + reference:(Coq.ZArith.BinInt.Z.land); + reference:(Coq.ZArith.BinInt.Z.ldiff); + reference:(Coq.ZArith.BinInt.Z.lxor); + reference:(Coq.ZArith.BinInt.Z.eq); + reference:(Coq.ZArith.BinInt.Z.eq_equiv); + reference:(Coq.ZArith.BinInt.Z.lt); + reference:(Coq.ZArith.BinInt.Z.gt); + reference:(Coq.ZArith.BinInt.Z.le); + reference:(Coq.ZArith.BinInt.Z.ge); + reference:(Coq.ZArith.BinInt.Z.divide); + reference:(Coq.ZArith.BinInt.Z.Even); + reference:(Coq.ZArith.BinInt.Z.Odd); + reference:(Coq.ZArith.BinInt.Z.eq_dec); + reference:(Coq.ZArith.BinInt.Z.succ_wd); + reference:(Coq.ZArith.BinInt.Z.pred_wd); + reference:(Coq.ZArith.BinInt.Z.opp_wd); + reference:(Coq.ZArith.BinInt.Z.add_wd); + reference:(Coq.ZArith.BinInt.Z.sub_wd); + reference:(Coq.ZArith.BinInt.Z.mul_wd); + reference:(Coq.ZArith.BinInt.Z.lt_wd); + reference:(Coq.ZArith.BinInt.Z.div_wd); + reference:(Coq.ZArith.BinInt.Z.mod_wd); + reference:(Coq.ZArith.BinInt.Z.quot_wd); + reference:(Coq.ZArith.BinInt.Z.rem_wd); + reference:(Coq.ZArith.BinInt.Z.pow_wd); + reference:(Coq.ZArith.BinInt.Z.testbit_wd); + reference:(Coq.ZArith.BinInt.Z.leb_spec0); + reference:(Coq.ZArith.BinInt.Z.ltb_spec0); + reference:(Coq.ZArith.BinInt.Z.eq_refl); + reference:(Coq.ZArith.BinInt.Z.eq_sym); + reference:(Coq.ZArith.BinInt.Z.eq_trans); + reference:(Coq.ZArith.BinInt.Z.lt_compat); + reference:(Coq.ZArith.BinInt.Z.lt_total); + reference:(Coq.ZArith.BinInt.Z.le_lteq); + reference:(Coq.ZArith.BinInt.Z.mul_eq_0); + reference:(Coq.ZArith.BinInt.Z.mul_eq_0_l); + reference:(Coq.ZArith.BinInt.Z.mul_eq_0_r); + reference:(Coq.ZArith.BinInt.Z.mul_eq_1); + reference:(Coq.ZArith.BinInt.Z.max_case_strong); + reference:(Coq.ZArith.BinInt.Z.max_case); + reference:(Coq.ZArith.BinInt.Z.max_dec); + reference:(Coq.ZArith.BinInt.Z.min_case_strong); + reference:(Coq.ZArith.BinInt.Z.min_case); + reference:(Coq.ZArith.BinInt.Z.min_dec); + reference:(Coq.ZArith.BinInt.Z.mod_bound_pos); + reference:(Coq.ZArith.BinInt.Z.sqrt_up); + reference:(Coq.ZArith.BinInt.Z.log2_up); + reference:(Coq.ZArith.BinInt.Z.divide_reflexive); + reference:(Coq.ZArith.BinInt.Z.divide_transitive); + reference:(Coq.ZArith.BinInt.Z.Bezout); + reference:(Coq.ZArith.BinInt.Z.lcm); + reference:(Coq.ZArith.BinInt.Z.eqb_spec); + reference:(Coq.ZArith.BinInt.Z.b2z); + reference:(Coq.ZArith.BinInt.Z.b2z_wd); + reference:(Coq.ZArith.BinInt.Z.eqf); + reference:(Coq.ZArith.BinInt.Z.setbit); + reference:(Coq.ZArith.BinInt.Z.clearbit); + reference:(Coq.ZArith.BinInt.Z.lnot); + reference:(Coq.ZArith.BinInt.Z.ones) +]. diff --git a/ltac2/constr_ex.v b/ltac2/constr_ex.v new file mode 100644 index 0000000000..a1c6ff11b1 --- /dev/null +++ b/ltac2/constr_ex.v @@ -0,0 +1,48 @@ +(** * Utilities / extensions for the Ltac2 "constr" type *) + +Require Import Ltac2.Ltac2. + +(* The coressponding functions in the Ltac2 library don't match the OCaml parameter order. + If we want to use the OCaml order for the constr fold functions we need to redefine it - otherwise we can't use (fold_right f) as function argument to the array *) + +Ltac2 rec array_fold_right_aux (f : 'b -> 'a -> 'a) (b : 'b array) (a : 'a) (pos : int) (len : int) : 'a := + (* Note: one could compare pos<0. + We keep an extra len parameter so that the function can be used for any sub array *) + match Int.equal len 0 with + | true => a + | false => array_fold_right_aux f b (f (Array.get b pos) a) (Int.sub pos 1) (Int.sub len 1) + end. + +Ltac2 array_fold_right (f : 'b -> 'a -> 'a) (b : 'b array) (a : 'a) := array_fold_right_aux f b a (Int.sub (Array.length b) 1) (Array.length b). + +(** This is a simple (and fast) function to call "f" on all applications. + It is intended to extract data from terms which are mostly applications of constructors on some terms. + It does not recurse into type terms, matches, lambdas, fixpoints. + In applications it does not recurse into function terms, but into arguments. + The function "f" is only called for terms which are applications. *) + +Ltac2 rec fold_right_app (f : constr -> 'a -> 'a ) (term : constr) (a : 'a ) : 'a := + match Constr.Unsafe.kind term with + | Constr.Unsafe.Cast constr1 cast constr2 + (* Don't recurse into type of cast - just the cast term *) + => fold_right_app f constr1 a + | Constr.Unsafe.Prod binder constr + (* Don't recurse into type of binder - just the bound term *) + => fold_right_app f constr a + | Constr.Unsafe.LetIn binder constr1 constr2 + (* Don't recurse into type of binder - just the assigned and bound term *) + => fold_right_app f constr1 (fold_right_app f constr2 a) + | Constr.Unsafe.App constr_func constr_arr_args + (* Call "f" for the complete "term" *) + (* Don't recurse into the function term - just into the array of arguments *) + => f term (array_fold_right (fold_right_app f) constr_arr_args a) + | _ => a + end. + +(** Examples *) + +(* +Ltac2 Eval fold_right_app (fun c l => c :: l) constr:(1+2+3) []. +*) + + diff --git a/ltac2/control_ex.v b/ltac2/control_ex.v new file mode 100644 index 0000000000..f848be8e23 --- /dev/null +++ b/ltac2/control_ex.v @@ -0,0 +1,8 @@ +Require Import Ltac2.Ltac2. + +(* Throw invalid argument function which takes a printf style format *) + +Ltac2 throw_invalid_argument fmt := + Message.Format.kfprintf (fun x => Control.throw (Invalid_argument (Some x))) fmt. + +Ltac2 Notation "throw_invalid_argument" fmt(format) := throw_invalid_argument fmt. diff --git a/ltac2/list_ex.v b/ltac2/list_ex.v new file mode 100644 index 0000000000..2914b16fe4 --- /dev/null +++ b/ltac2/list_ex.v @@ -0,0 +1,20 @@ +Require Import Ltac2.Ltac2. + +(** * Ltac2 list utilities / extensions *) + +(** ** Use list as unsorted sets of constr terms *) + +Ltac2 rec constr_bag_add (ls : constr list) (e : constr) := + match ls with + | [] => [e] + | h :: tl => if Constr.equal h e then ls else h::(constr_bag_add tl e) + end. + +Ltac2 constr_bag_contains (ls : constr list) (e : constr) := + List.exist (fun x => Constr.equal x e) ls. + +Ltac2 rec constr_bag_union (a : constr list) (b : constr list) := + match b with + | [] => a + | h :: tl => constr_bag_union (constr_bag_add a h) tl + end. \ No newline at end of file diff --git a/ltac2/message_ex.v b/ltac2/message_ex.v new file mode 100644 index 0000000000..176d16eebd --- /dev/null +++ b/ltac2/message_ex.v @@ -0,0 +1,26 @@ +Require Import Ltac2.Ltac2. + +(** * Ltac2 message utilities / extensions *) + +Ltac2 list_to_message_flex (element_to_message : 'a -> message) (prefix : string) (separator : string) (postfix : string) (l : 'a list) : message := + let rec aux(l : 'a list) : message := + match l with + | [] => Message.of_string postfix + | h :: t => + match t with + | [] => Message.concat (element_to_message h) (Message.of_string postfix) + | _ :: _ => Message.concat (element_to_message h) (Message.concat (Message.of_string separator) (aux t)) + end + end in + Message.concat (Message.of_string prefix) (aux l). + +Ltac2 list_to_message (element_to_message : 'a -> message) (l : 'a list) : message := list_to_message_flex element_to_message "[ " "; " " ]" l. + +Ltac2 reference_to_message (ref : Std.reference) : message := + let path := Env.path ref in + list_to_message_flex Message.of_ident "" "." "" path. + +(* Tests +Ltac2 Eval Message.print (list_to_message Message.of_string [ "A"; "B" ]). +Ltac2 Eval Message.print (reference_to_message reference:(S)). +*) diff --git a/ltac2/print_ex.v b/ltac2/print_ex.v new file mode 100644 index 0000000000..ed5aabba5c --- /dev/null +++ b/ltac2/print_ex.v @@ -0,0 +1,42 @@ +Require Import Ltac2.Ltac2. +Require Import Ltac2.Printf. + +(** * Ltac2 printing utilities / extensions *) + +Ltac2 print_hyps () := + let rec aux (hyps : (ident * constr option * constr) list) := + match hyps with + | [] => () + | h :: t => + let (id, value, type) := h in + match value with + | Some value => printf "let %I := %t : %t in " id value type + | None => printf "forall (%I : %t), " id type + end; + aux t + end in + aux (Control.hyps ()) + . + +Ltac2 print_goal () := + lazy_match! goal with + | [ |- ?g ] => printf "%t" g + end. + +(** With these options: + + Set Printing Depth 1000. + Set Printing Width 240. + Unset Printing Notations. + Set Printing Implicit. + +print_context should produce something which Coq can parse as Goal. +*) + +Ltac2 print_context () := + printf "Goal"; + print_hyps (); + print_goal (); + printf "." + . + \ No newline at end of file diff --git a/ltac2/simpl_by_cbv.v b/ltac2/simpl_by_cbv.v new file mode 100644 index 0000000000..16e0748dbb --- /dev/null +++ b/ltac2/simpl_by_cbv.v @@ -0,0 +1,320 @@ +(** * Define tactics which do a cbv reduction restricted to a tailored delta list and optionally to certain parts of a term *) + +Require Import Ltac2.Ltac2. +Require Import Ltac2.Bool. +Require Import Ltac2.Printf. +(* This file contains symbol lists for delta reductions tailored for specific applications *) +Require Export VST.ltac2.cbv_symbol_lists_generated. +(* Ltac helper files *) +Require Export VST.ltac2.list_ex. +Require Export VST.ltac2.constr_ex. +Require Export VST.ltac2.control_ex. +Require Export VST.ltac2.message_ex. +Require Export VST.ltac2.print_ex. +(* Definition of EVar ... *) +Require compcert.cfrontend.Clight. +Require VST.veric.expr. + +(** ** Ltac2 utilities *) + +(** Get first and second of a pair *) + +Ltac2 pair_first (x : 'a*'b) : 'a := let (a,b):=x in a. +Ltac2 pair_second (x : 'a*'b) : 'b := let (a,b):=x in b. + +(** ** Functions to construct Std.red_flags records for specific purposes *) + +Ltac2 redflags_full () := +{ + (* beta: expand the application of an unfolded functions by substitution *) + Std.rBeta := true; + (* delta: true = expand all but rConst; false = expand only rConst *) + Std.rDelta := true; + (* Note: iota in tactics like cbv is a shorthand for match, fix and cofix *) + (* iota-match: simplify matches by choosing a pattern *) + Std.rMatch := true; + (* iota-fix: simplify fixpoint expressions by expanding one level *) + Std.rFix := true; + (* iota-cofix: simplify cofixpoint expressions by expanding one level *) + Std.rCofix := true; + (* zeta: expand let expressions by substitution *) + Std.rZeta := true; + (* Symbols to expand or not to expand (depending on rDelta) *) + Std.rConst := [] +}. + +Ltac2 redflags_delta_only (delta_symbols : Std.reference list) := +{ + (* beta: expand the application of an unfolded functions by substitution *) + Std.rBeta := true; + (* delta: true = expand all but rConst; false = expand only rConst *) + Std.rDelta := false; + (* Note: iota in tactics like cbv is a shorthand for match, fix and cofix *) + (* iota-match: simplify matches by choosing a pattern *) + Std.rMatch := true; + (* iota-fix: simplify fixpoint expressions by expanding one level *) + Std.rFix := true; + (* iota-cofix: simplify cofixpoint expressions by expanding one level *) + Std.rCofix := true; + (* zeta: expand let expressions by substitution *) + Std.rZeta := true; + (* Symbols to expand or not to expand (depending on rDelta) *) + Std.rConst := delta_symbols +}. + +(** ** Functions to CBV compute only under applications of a given head symbol *) + +(** ** CBV under application of the given head term with limited recursion: + - arguments and function terms in applications + - bound terms of products and lambdas + - bound terms and values of let in bindings + - values of cast expressions + - values or primitive projections + - match expressions and match case functions in matches, but no match return types +fixpoints, types and native arrays are copied unchanged. +The function returns a pair with a bool, which indicates if the match term was found and cbv was called on a part of the term. +There is an extended recusion variant of the function below. +*) + +Ltac2 rec eval_cbv_uao_lr (head : constr) (frf : constr -> Std.red_flags) (term : constr) : constr * bool := + match Constr.Unsafe.kind term with + | Constr.Unsafe.App func args => + if Constr.equal head func + then + (Std.eval_cbv (frf term) term, true) + else + let (func_r, func_m) := eval_cbv_uao_lr head frf func in + let args_e := Array.map (eval_cbv_uao_lr head frf) args in + if func_m || (Array.exist pair_second args_e) + then (Constr.Unsafe.make (Constr.Unsafe.App func_r (Array.map pair_first args_e)), true) + else (term, false) + + | Constr.Unsafe.Prod binder bound => + let (bound_r, bound_m) := eval_cbv_uao_lr head frf bound in + if bound_m + then (Constr.Unsafe.make (Constr.Unsafe.Prod binder bound_r), true) + else (term, false) + + | Constr.Unsafe.Lambda binder bound => + let (bound_r, bound_m) := eval_cbv_uao_lr head frf bound in + if bound_m + then (Constr.Unsafe.make (Constr.Unsafe.Lambda binder bound_r), true) + else (term, false) + + | Constr.Unsafe.LetIn binder value bound => + let (value_r, value_m) := eval_cbv_uao_lr head frf value in + let (bound_r, bound_m) := eval_cbv_uao_lr head frf bound in + if value_m || bound_m + then (Constr.Unsafe.make (Constr.Unsafe.LetIn binder value_r bound_r), true) + else (term, false) + + | Constr.Unsafe.Cast value cast type => + let (value_r, value_m) := eval_cbv_uao_lr head frf value in + if value_m + then (Constr.Unsafe.make (Constr.Unsafe.Cast value_r cast type), true) + else (term, false) + + | Constr.Unsafe.Proj projection value => + let (value_r, value_m) := eval_cbv_uao_lr head frf value in + if value_m + then (Constr.Unsafe.make (Constr.Unsafe.Proj projection value_r), true) + else (term, false) + + | Constr.Unsafe.Case case_a constr_return case_b constr_match case_funcs => + let (match_r, match_m) := eval_cbv_uao_lr head frf constr_match in + let case_funcs_e := Array.map (eval_cbv_uao_lr head frf) case_funcs in + if match_m || (Array.exist pair_second case_funcs_e) + then (Constr.Unsafe.make (Constr.Unsafe.Case case_a constr_return case_b match_r (Array.map pair_first case_funcs_e)), true) + else (term, false) + + | _ => (term, false) + end. + +(** ** CBV under application of the given head term with almsot full recusion. + The search does not recurse into types in binders, because with Coq 8.16 Ltac2 one cannot safely reconstruct the term (fixed in 8.17) +*) + +Ltac2 rec eval_cbv_uao_afr (head : constr) (frf : constr -> Std.red_flags) (term : constr) : constr * bool := + match Constr.Unsafe.kind term with + | Constr.Unsafe.App func args => + if Constr.equal head func + then + (Std.eval_cbv (frf term) term, true) + else + let (func_r, func_m) := eval_cbv_uao_afr head frf func in + let args_e := Array.map (eval_cbv_uao_afr head frf) args in + if func_m || (Array.exist pair_second args_e) + then (Constr.Unsafe.make (Constr.Unsafe.App func_r (Array.map pair_first args_e)), true) + else (term, false) + + | Constr.Unsafe.Prod binder bound => + let (bound_r, bound_m) := eval_cbv_uao_afr head frf bound in + if bound_m + then (Constr.Unsafe.make (Constr.Unsafe.Prod binder bound_r), true) + else (term, false) + + | Constr.Unsafe.Lambda binder bound => + let (bound_r, bound_m) := eval_cbv_uao_afr head frf bound in + if bound_m + then (Constr.Unsafe.make (Constr.Unsafe.Lambda binder bound_r), true) + else (term, false) + + | Constr.Unsafe.LetIn binder value bound => + let (value_r, value_m) := eval_cbv_uao_afr head frf value in + let (bound_r, bound_m) := eval_cbv_uao_afr head frf bound in + if value_m || bound_m + then (Constr.Unsafe.make (Constr.Unsafe.LetIn binder value_r bound_r), true) + else (term, false) + + | Constr.Unsafe.Cast value cast type => + let (value_r, value_m) := eval_cbv_uao_afr head frf value in + let (type_r, type_m) := eval_cbv_uao_afr head frf type in + if value_m || type_m + then (Constr.Unsafe.make (Constr.Unsafe.Cast value_r cast type_r), true) + else (term, false) + + | Constr.Unsafe.Proj projection value => + let (value_r, value_m) := eval_cbv_uao_afr head frf value in + if value_m + then (Constr.Unsafe.make (Constr.Unsafe.Proj projection value_r), true) + else (term, false) + + | Constr.Unsafe.Case case_a constr_return case_b constr_match case_funcs => + let (return_r, return_m) := eval_cbv_uao_afr head frf constr_return in + let (match_r, match_m) := eval_cbv_uao_afr head frf constr_match in + let case_funcs_e := Array.map (eval_cbv_uao_afr head frf) case_funcs in + if return_m || match_m || (Array.exist pair_second case_funcs_e) + then (Constr.Unsafe.make (Constr.Unsafe.Case case_a return_r case_b match_r (Array.map pair_first case_funcs_e)), true) + else (term, false) + + | Constr.Unsafe.Fix int_arr int binder_arr constr_arr => + let constr_arr_e := Array.map (eval_cbv_uao_afr head frf) constr_arr in + if (Array.exist pair_second constr_arr_e) + then (Constr.Unsafe.make (Constr.Unsafe.Fix int_arr int binder_arr (Array.map pair_first constr_arr_e)), true) + else (term, false) + + | Constr.Unsafe.CoFix int binder_arr constr_arr => + let constr_arr_e := Array.map (eval_cbv_uao_afr head frf) constr_arr in + if (Array.exist pair_second constr_arr_e) + then (Constr.Unsafe.make (Constr.Unsafe.CoFix int binder_arr (Array.map pair_first constr_arr_e)), true) + else (term, false) + + | Constr.Unsafe.Array instance constr_arr constr_a constr_b => + let (constr_a_r, constr_a_m) := eval_cbv_uao_afr head frf constr_a in + let (constr_b_r, constr_b_m) := eval_cbv_uao_afr head frf constr_b in + let constr_arr_e := Array.map (eval_cbv_uao_afr head frf) constr_arr in + if constr_a_m || constr_b_m || (Array.exist pair_second constr_arr_e) + then (Constr.Unsafe.make (Constr.Unsafe.Array instance (Array.map pair_first constr_arr_e) constr_a_r constr_b_r), true) + else (term, false) + + | _ => (term, false) + end. + +(** ** Functions to collect local symbol definitions in VST *) + +Ltac2 reference_of_constr(ref : constr) : Std.reference := + match Constr.Unsafe.kind ref with + | Constr.Unsafe.Var ident + => Std.VarRef ident + | Constr.Unsafe.Constant constant instance + => Std.ConstRef constant + | Constr.Unsafe.Ind inductive instance + => Std.IndRef inductive + | Constr.Unsafe.Constructor constructor instance + => Std.ConstructRef constructor + | _ => throw_invalid_argument "reference_of_constr: not a reference: %t" ref + end. + +Ltac2 vst_collect_local_ident_one (c : constr) (l : constr list) : constr list := +match! c with +| compcert.cfrontend.Clight.Evar ?a ?b => constr_bag_add l a +| compcert.cfrontend.Clight.Etempvar ?a ?b => constr_bag_add l a +| VST.veric.expr.tc_initialized ?a ?b => constr_bag_add l a +| _ => l +end. + +Ltac2 vst_collect_local_idents (c : constr) : constr list := fold_right_app vst_collect_local_ident_one c []. + +Ltac2 vst_extend_delta_symbols (ds : Std.reference list) (c : constr) : Std.reference list := + let cl := vst_collect_local_idents c in + let rl := List.map reference_of_constr cl in + (* printf "vst_extend_delta_symbols: %a" (fun _ => list_to_message reference_to_message) rl; *) + List.append rl ds. + +(** ** Reduction tactics *) + +(** Tactic for cbv reduction of the goal with + - uao_lr: reduction only under applications of the given head symbol - with limited recursion into the term + Usage: cbv_uao_lr_tac '@ + *) + +Ltac2 cbv_uao_lr (head : constr) : unit := + let goal := Control.goal() in + let (goal_r, goal_m) := eval_cbv_uao_lr head (fun _ => redflags_full ()) goal in + change $goal_r. + +(** Tactic for cbv reduction of the goal with + - uao_afr: reduction only under applications of the given head symbol - with almost full recursion into the term + Usage: cbv_uao_fr '@ + *) + +Ltac2 cbv_uao_afr (head : constr) : unit := + let goal := Control.goal() in + let (goal_r, goal_m) := eval_cbv_uao_afr head (fun _ => redflags_full ()) goal in + change $goal_r. + +(** Tactic for cbv reduction of the goal with + - ds: delta expansion symbol list + Usage: cbv_ds < delta symbol definition> + *) + +Ltac2 cbv_ds (delta_symbols : Std.reference list) : unit := + let goal := Control.goal() in + let goal_r := Std.eval_cbv (redflags_delta_only delta_symbols) goal in + change $goal_r. + +(** Tactic for cbv reduction of the goal with + - ds: delta expansion symbol list + - uao_lr: reduction only under applications of the given head symbol - with limited recursion into the term + - vstl: extend the delta reduction list with VST local symbols + Usage: cbv_ds_uao_lr_vstl < delta symbol definition> '@ + *) + +Ltac2 cbv_ds_uao_lr_vstl (delta_symbols : Std.reference list) (head : constr) : unit := + let goal := Control.goal() in + (* printf "cbv_ds_uao_lr_vstl"; print_context (); *) + let (goal_r, goal_m) := eval_cbv_uao_lr head (fun term => redflags_delta_only (vst_extend_delta_symbols delta_symbols term)) goal in + change $goal_r. + +(** Tactic for cbv reduction of the goal with + - ds: delta expansion symbol list + - uao_afr: reduction only under applications of the given head symbol - with almost full recursion into the term + - vstl: extend the delta reduction list with VST local symbols + Usage: cbv_ds_uao_afr_vstl < delta symbol definition> '@ + *) + +Ltac2 cbv_ds_uao_afr_vstl (delta_symbols : Std.reference list) (head : constr) : unit := + let goal := Control.goal() in + (* printf "cbv_ds_uao_afr_vstl"; print_context (); *) + let (goal_r, goal_m) := eval_cbv_uao_afr head (fun term => redflags_delta_only (vst_extend_delta_symbols delta_symbols term)) goal in + change $goal_r. + +(** ** Special tactics for VST *) + +(** The whole essence of this file is currently disabled, because not all of VST compiles with it cause of entialer changes. + To enable it, comment the line below and uncomment the second line below *) +Ltac simpl_msubst_denote_tc_assert := simpl VST.floyd.local2ptree_typecheck.msubst_denote_tc_assert. +(* Ltac simpl_msubst_denote_tc_assert := ltac2:(cbv_ds_uao_lr_vstl (reduction_symbol_list_msubst_denote_tc_assert ()) '@VST.floyd.local2ptree_typecheck.msubst_denote_tc_assert). *) + +(** ** Tests *) + +(* Test limited rewrite *) +Goal forall x, let f := (fun x => x+2*3) in (x + (f (2*3)) + (2*3) + 2*3+4*5*6 + x = x + 144). +cbv_uao_lr 'Nat.mul. +Abort. + +(* Test compute intensive reduction *) +Require Import ZArith. +Goal (2^400 / 2^396 = 16)%Z. +Time cbv_ds (reduction_symbol_list_zarith ()). +Abort. diff --git a/ltac2/simpl_by_cbv_notes.md b/ltac2/simpl_by_cbv_notes.md new file mode 100644 index 0000000000..b31adc23f1 --- /dev/null +++ b/ltac2/simpl_by_cbv_notes.md @@ -0,0 +1,38 @@ +# Debugging simplification by cbv + +If symbols are missing in the delta list, the resulting terms can become very large and it can take minutes to run cbv. + +## Using `Set Debug "Cbv"` + +Coq has a command `Set Debug "Cbv".`. If enabled, it dumps all delta expansion decisions. A few hints: + +- This cannot be undone - one has to restart coqtop to disable this setting. +- Interesting are typically the `[Cbv] Not unfolding` lines - I usually grep the output for it and `sort | uniq` the result + +## Using Coqtop and batch debug + +Usually coqtop is faster in displaying terms than most IDEs - also it obeys `Set Printing Depth`. + +To use coqtop try the following: + +- put your current file until including the failing tactic call into a file `Debug.v` +- put the following commands in front of the failing tactic: + ``` + Set Printing Depth 1000. + Set Printing Width 240. + Unset Printing Notations. + Set Printing Implicit. + Set Ltac Debug. + Set Ltac Batch Debug. + ``` +- put a `Quit.` after the failing tactic. +- run `coqtop -lv Debug.v 2>&1 | ts -i "%.s" 1>Debug.log` +- the `ts` command adds run times in us at the begin of each line - you can search the log for longer times with a regexp + - if you don't want the time stamps, remove this from the pipe +- look into `Debug.log` and find the long running command +- assuming you waited long enough for it to finish, you will find teh resulting goal after it +- In this goal typically you have a longish half expanded function application, which is applied to a term containing variables +- Jump after the function term using "go to matched parenthesis" and see what it is applied on - this term is usually not that long and one can find out by inspection why it does not compute. +- The `Debug.log` can be long (a few 10 million lines is not unheard of) - if you have issues with modern editors, use vi + - search forward / backward is `/` and `?`` + - search matching parenthesis is `%` \ No newline at end of file diff --git a/util/make_version b/util/make_version index d068b7380d..94f7604276 100755 --- a/util/make_version +++ b/util/make_version @@ -12,7 +12,7 @@ printf >>$F 'Definition release := "' tr -d '[:cntrl:]' >$F printf >>$F '".\n' printf >>$F 'Definition date := "' -date --rfc-3339=date | tr -d '[:cntrl:]' >>$F +date -Idate | tr -d '[:cntrl:]' >>$F printf >>$F '".\n' printf >>$F 'Definition bitsize : Z := %d.\n' $1 printf >>$F 'Definition compcert_version := "%s".' $2