Results for fold 1 Results for lemma transl_program_correct: : forward_simulation (Clight.semantics2 prog) (Csharpminor.semantics tprog) FAILURE! Tactics applied: 10000 Original Proof: [eapply forward_simulation_plus. eexact symbols_preserved. eexact transl_initial_states. eexact transl_final_states. eexact transl_step.] Proof search time: 2 min, 27 sec Number of successful tactic applications: 1640 Number of failed tactic applications: 8361 Results for lemma make_floatofint_correct: : forall a n sg e le m, eval_expr ge e le m a (Vint n) -> eval_expr ge e le m (make_floatofint a sg) (Vfloat(cast_int_float sg n)) FAILURE! Tactics applied: 10000 Original Proof: [intros. unfold make_floatofint, cast_int_float. destruct sg; econstructor; eauto.] Proof search time: 1 min, 34 sec Number of successful tactic applications: 1221 Number of failed tactic applications: 8780 Results for lemma transl_fundef_sig2: : forall f tf args res cc, transl_fundef f = OK tf -> type_of_fundef f = Tfunction args res cc -> funsig tf = signature_of_type args res cc FAILURE! Tactics applied: 10000 Original Proof: [intros. eapply transl_fundef_sig1; eauto. rewrite H0; reflexivity.] Proof search time: 1 min, 23 sec Number of successful tactic applications: 1257 Number of failed tactic applications: 8744 Results for lemma var_info_translated: : forall b v, Genv.find_var_info ge b = Some v -> exists tv, Genv.find_var_info tge b = Some tv /\ transf_globvar transl_globvar v = OK tv FAILURE! Tactics applied: 10000 Original Proof: [Proof (Genv.find_var_info_transf_partial2 transl_fundef transl_globvar _ TRANSL).] Proof search time: 1 min, 32 sec Number of successful tactic applications: 1490 Number of failed tactic applications: 8511 Results for lemma make_or_correct: : binary_constructor_correct make_or sem_or SUCCESS! Proof Found in EFSM: apply make_binarith_int_correct; econstructor. Tactics applied: 670 Original Proof: [apply make_binarith_int_correct; intros; auto.] Shorter Proof Found? yes This is a novel proof proof search time: 1 min, 6 sec Number of successful tactic applications: 167 Number of failed tactic applications: 503 Results for lemma bind_parameter_temps_match: : forall vars vals le1 le2, Clight.bind_parameter_temps vars vals le1 = Some le2 -> bind_parameters (map fst vars) vals le1 = Some le2 FAILURE! Tactics applied: 10000 Original Proof: [induction vars; simpl; intros. destruct vals; inv H. auto. destruct a as [id ty]. destruct vals; try discriminate. auto.] Proof search time: 1 min, 28 sec Number of successful tactic applications: 1116 Number of failed tactic applications: 8885 Results for lemma match_env_alloc_variables: : forall e1 m1 vars e2 m2, Clight.alloc_variables e1 m1 vars e2 m2 -> forall te1, match_env e1 te1 -> exists te2, Csharpminor.alloc_variables te1 m1 (map transl_var vars) te2 m2 /\ match_env e2 te2 FAILURE! Tactics applied: 10000 Original Proof: [induction 1; intros; simpl. exists te1; split. constructor. auto. exploit (IHalloc_variables (PTree.set id (b1, sizeof ty) te1)). constructor. intros until ty0. repeat rewrite PTree.gsspec. destruct (peq id0 id); intros. congruence. eapply me_local; eauto. intros until sz. repeat rewrite PTree.gsspec. destruct (peq id0 id); intros. exists ty; congruence. eapply me_local_inv; eauto. intros [te2 [ALLOC MENV]]. exists te2; split. econstructor; eauto. auto.] Proof search time: 1 min, 43 sec Number of successful tactic applications: 1963 Number of failed tactic applications: 8038 Results for lemma match_cont_call_cont: : forall tyret' nbrk' ncnt' tyret nbrk ncnt k tk, match_cont tyret nbrk ncnt k tk -> match_cont tyret' nbrk' ncnt' (Clight.call_cont k) (call_cont tk) FAILURE! Tactics applied: 10000 Original Proof: [induction 1; simpl; auto. constructor. econstructor; eauto.] Proof search time: 1 min, 50 sec Number of successful tactic applications: 1503 Number of failed tactic applications: 8498 Results for lemma match_env_same_blocks: : forall e te, match_env e te -> blocks_of_env te = Clight.blocks_of_env e FAILURE! Tactics applied: 10000 Original Proof: [intros. set (R := fun (x: (block * type)) (y: (block * Z)) => match x, y with | (b1, ty), (b2, sz) => b2 = b1 /\ sz = sizeof ty end). assert (list_forall2 (fun i_x i_y => fst i_x = fst i_y /\ R (snd i_x) (snd i_y)) (PTree.elements e) (PTree.elements te)). apply PTree.elements_canonical_order. intros id [b ty] GET. exists (b, sizeof ty); split. eapply me_local; eauto. red; auto. intros id [b sz] GET. exploit me_local_inv; eauto. intros [ty EQ]. exploit me_local; eauto. intros EQ1. exists (b, ty); split. auto. red; split; congruence. unfold blocks_of_env, Clight.blocks_of_env. generalize H0. induction 1. auto. simpl. f_equal; auto. unfold block_of_binding, Clight.block_of_binding. destruct a1 as [id1 [blk1 ty1]]. destruct b1 as [id2 [blk2 sz2]]. simpl in *. destruct H1 as [A [B C]]. congruence.] Proof search time: 1 min, 27 sec Number of successful tactic applications: 1016 Number of failed tactic applications: 8985 Results for lemma make_singleconst_correct: : forall n e le m, eval_expr ge e le m (make_singleconst n) (Vsingle n) SUCCESS! Proof Found in EFSM: econstructor. reflexivity. Tactics applied: 476 Original Proof: [intros. unfold make_singleconst. econstructor. reflexivity.] Shorter Proof Found? yes This is a novel proof proof search time: 1 min, 5 sec Number of successful tactic applications: 53 Number of failed tactic applications: 423 Results for lemma make_shr_correct: : binary_constructor_correct make_shr sem_shr FAILURE! Tactics applied: 10000 Original Proof: [red; unfold make_shr, sem_shr, sem_shift; intros until m; intros SEM MAKE EV1 EV2; destruct (classify_shift tya tyb); inv MAKE; destruct va; try discriminate; destruct vb; try discriminate. - destruct (Int.ltu i0 Int.iwordsize) eqn:E; inv SEM. destruct s; inv H0; econstructor; eauto; simpl; rewrite E; auto. - destruct (Int64.ltu i0 Int64.iwordsize) eqn:E; inv SEM. exploit small_shift_amount_1; eauto. intros [A B]. destruct s; inv H0; econstructor; eauto with cshm; simpl; rewrite A; f_equal; f_equal. unfold Int64.shr', Int64.shr; rewrite B; auto. unfold Int64.shru', Int64.shru; rewrite B; auto. - destruct (Int64.ltu i0 (Int64.repr 32)) eqn:E; inv SEM. destruct s; inv H0; econstructor; eauto with cshm; simpl; rewrite small_shift_amount_2; auto. - destruct (Int.ltu i0 Int64.iwordsize') eqn:E; inv SEM. destruct s; inv H0; econstructor; eauto with cshm; simpl; rewrite E. unfold Int64.shr', Int64.shr; rewrite small_shift_amount_3; auto. unfold Int64.shru', Int64.shru; rewrite small_shift_amount_3; auto.] Proof search time: 1 min, 40 sec Number of successful tactic applications: 2137 Number of failed tactic applications: 7864 Results for lemma transl_initial_states: : forall S, Clight.initial_state prog S -> exists R, initial_state tprog R /\ match_states S R FAILURE! Tactics applied: 10000 Original Proof: [intros. inv H. exploit function_ptr_translated; eauto. intros [tf [A B]]. assert (C: Genv.find_symbol tge (prog_main tprog) = Some b). rewrite symbols_preserved. replace (prog_main tprog) with (prog_main prog). auto. symmetry. unfold transl_program in TRANSL. eapply transform_partial_program2_main; eauto. assert (funsig tf = signature_of_type Tnil type_int32s cc_default). eapply transl_fundef_sig2; eauto. econstructor; split. econstructor; eauto. eapply Genv.init_mem_transf_partial2; eauto. econstructor; eauto. constructor; auto. exact I.] Proof search time: 1 min, 34 sec Number of successful tactic applications: 1679 Number of failed tactic applications: 8322 Results for lemma make_load_correct: : forall addr ty code b ofs v e le m, make_load addr ty = OK code -> eval_expr ge e le m addr (Vptr b ofs) -> deref_loc ty m b ofs v -> eval_expr ge e le m code v FAILURE! Tactics applied: 10000 Original Proof: [unfold make_load; intros until m; intros MKLOAD EVEXP DEREF. inv DEREF. rewrite H in MKLOAD. inv MKLOAD. apply eval_Eload with (Vptr b ofs); auto. rewrite H in MKLOAD. inv MKLOAD. auto. rewrite H in MKLOAD. inv MKLOAD. auto.] Proof search time: 1 min, 37 sec Number of successful tactic applications: 2001 Number of failed tactic applications: 8000 Results for fold 2 Results for lemma match_transl_step: : forall ts tk ts' tk' f te le m, match_transl (Sblock ts) tk ts' tk' -> star step tge (State f ts' tk' te le m) E0 (State f ts (Kblock tk) te le m) FAILURE! Tactics applied: 10000 Original Proof: [intros. inv H. apply star_one. constructor. apply star_refl.] Proof search time: 1 min, 21 sec Number of successful tactic applications: 1654 Number of failed tactic applications: 8347 Results for lemma transl_expr_correct: : forall a v, Clight.eval_expr ge e le m a v -> forall ta, transl_expr a = OK ta -> Csharpminor.eval_expr tge te le m ta v FAILURE! Tactics applied: 10000 Original Proof: [Proof (proj1 transl_expr_lvalue_correct).] Proof search time: 1 min, 49 sec Number of successful tactic applications: 1768 Number of failed tactic applications: 8233 Results for lemma match_env_free_blocks: : forall e te m m', match_env e te -> Mem.free_list m (Clight.blocks_of_env e) = Some m' -> Mem.free_list m (blocks_of_env te) = Some m' FAILURE! Tactics applied: 10000 Original Proof: [intros. rewrite (match_env_same_blocks _ _ H). auto.] Proof search time: 1 min, 17 sec Number of successful tactic applications: 1521 Number of failed tactic applications: 8480 Results for lemma create_undef_temps_match: : forall temps, create_undef_temps (map fst temps) = Clight.create_undef_temps temps FAILURE! Tactics applied: 10000 Original Proof: [induction temps; simpl. auto. destruct a as [id ty]. simpl. decEq. auto.] Proof search time: 1 min, 18 sec Number of successful tactic applications: 968 Number of failed tactic applications: 9033 Results for lemma transl_final_states: : forall S R r, match_states S R -> Clight.final_state S r -> final_state R r FAILURE! Tactics applied: 10000 Original Proof: [intros. inv H0. inv H. inv MK. constructor.] Proof search time: 1 min, 30 sec Number of successful tactic applications: 1539 Number of failed tactic applications: 8462 Results for lemma transl_unop_correct: : forall op a tya c va v e le m, transl_unop op a tya = OK c -> sem_unary_operation op va tya = Some v -> eval_expr ge e le m a va -> eval_expr ge e le m c v FAILURE! Tactics applied: 10000 Original Proof: [intros. destruct op; simpl in *. eapply make_notbool_correct; eauto. eapply make_notint_correct; eauto. eapply make_neg_correct; eauto. eapply make_absfloat_correct; eauto.] Proof search time: 1 min, 13 sec Number of successful tactic applications: 1692 Number of failed tactic applications: 8309 Results for lemma transl_lvalue_correct: : forall a b ofs, Clight.eval_lvalue ge e le m a b ofs -> forall ta, transl_lvalue a = OK ta -> Csharpminor.eval_expr tge te le m ta (Vptr b ofs) FAILURE! Tactics applied: 10000 Original Proof: [Proof (proj2 transl_expr_lvalue_correct).] Proof search time: 1 min, 27 sec Number of successful tactic applications: 1786 Number of failed tactic applications: 8215 Results for lemma make_cast_correct: : forall e le m a b v ty1 ty2 v', make_cast ty1 ty2 a = OK b -> eval_expr ge e le m a v -> sem_cast v ty1 ty2 = Some v' -> eval_expr ge e le m b v' FAILURE! Tactics applied: 10000 Original Proof: [intros. unfold make_cast, sem_cast in *; destruct (classify_cast ty1 ty2); inv H; destruct v; inv H1; eauto with cshm. unfold make_singleofint, cast_int_float. destruct si1; eauto with cshm. destruct (cast_float_int si2 f) as [i|] eqn:E; inv H2. apply make_cast_int_correct. unfold cast_float_int in E. unfold make_intoffloat. destruct si2; econstructor; eauto; simpl; rewrite E; auto. destruct (cast_single_int si2 f) as [i|] eqn:E; inv H2. apply make_cast_int_correct. unfold cast_single_int in E. unfold make_intofsingle. destruct si2; econstructor; eauto with cshm; simpl; rewrite E; auto. unfold make_longofint, cast_int_long. destruct si1; eauto with cshm. unfold make_floatoflong, cast_long_float. destruct si1; eauto with cshm. unfold make_singleoflong, cast_long_single. destruct si1; eauto with cshm. destruct (cast_float_long si2 f) as [i|] eqn:E; inv H2. unfold cast_float_long in E. unfold make_longoffloat. destruct si2; econstructor; eauto; simpl; rewrite E; auto. destruct (cast_single_long si2 f) as [i|] eqn:E; inv H2. unfold cast_single_long in E. unfold make_longofsingle. destruct si2; econstructor; eauto with cshm; simpl; rewrite E; auto. econstructor; eauto with cshm. simpl. unfold Val.cmpf, Val.cmpf_bool. rewrite Float.cmp_ne_eq. destruct (Float.cmp Ceq f Float.zero); auto. econstructor; eauto with cshm. simpl. unfold Val.cmpfs, Val.cmpfs_bool. rewrite Float32.cmp_ne_eq. destruct (Float32.cmp Ceq f Float32.zero); auto. econstructor; eauto with cshm. simpl. unfold Val.cmpl, Val.cmpl_bool, Int64.cmp. destruct (Int64.eq i Int64.zero); auto. econstructor; eauto with cshm. simpl. unfold Val.cmpu, Val.cmpu_bool, Int.cmpu. destruct (Int.eq i Int.zero); auto. destruct (ident_eq id1 id2 && fieldlist_eq fld1 fld2); inv H2; auto. destruct (ident_eq id1 id2 && fieldlist_eq fld1 fld2); inv H2; auto.] Proof search time: 1 min, 10 sec Number of successful tactic applications: 1374 Number of failed tactic applications: 8627 Results for lemma make_binarith_int_correct: : binary_constructor_correct (make_binarith_int iop iopu lop lopu) (sem_binarith sem_int sem_long (fun x y => None) (fun x y => None)) FAILURE! Tactics applied: 10000 Original Proof: [red; unfold make_binarith_int, sem_binarith; intros until m; intros SEM MAKE EV1 EV2. set (cls := classify_binarith tya tyb) in *. set (ty := binarith_type cls) in *. monadInv MAKE. destruct (sem_cast va tya ty) as [va'|] eqn:Ca; try discriminate. destruct (sem_cast vb tyb ty) as [vb'|] eqn:Cb; try discriminate. exploit make_cast_correct. eexact EQ. eauto. eauto. intros EV1'. exploit make_cast_correct. eexact EQ1. eauto. eauto. intros EV2'. destruct cls; inv EQ2; destruct va'; try discriminate; destruct vb'; try discriminate. - destruct s; inv H0; econstructor; eauto with cshm. rewrite iop_ok; auto. rewrite iopu_ok; auto. - destruct s; inv H0; econstructor; eauto with cshm. rewrite lop_ok; auto. rewrite lopu_ok; auto.] Proof search time: 1 min, 48 sec Number of successful tactic applications: 2097 Number of failed tactic applications: 7904 Results for lemma transl_fundef_sig1: : forall f tf args res cc, transl_fundef f = OK tf -> classify_fun (type_of_fundef f) = fun_case_f args res cc -> funsig tf = signature_of_type args res cc FAILURE! Tactics applied: 10000 Original Proof: [intros. destruct f; simpl in *. monadInv H. monadInv EQ. simpl. inversion H0. unfold signature_of_function, signature_of_type. f_equal. apply transl_params_types. destruct (signature_eq (ef_sig e) (signature_of_type t t0 c)); inv H. simpl. congruence.] Proof search time: 1 min, 3 sec Number of successful tactic applications: 943 Number of failed tactic applications: 9058 Results for lemma make_boolean_correct: : forall e le m a v ty b, eval_expr ge e le m a v -> bool_val v ty = Some b -> exists vb, eval_expr ge e le m (make_boolean a ty) vb /\ Val.bool_of_val vb b FAILURE! Tactics applied: 10000 Original Proof: [intros. unfold make_boolean. unfold bool_val in H0. destruct (classify_bool ty); destruct v; inv H0. econstructor; split. apply make_cmp_ne_zero_correct with (n := i); auto. destruct (Int.eq i Int.zero); simpl; constructor. econstructor; split. econstructor; eauto with cshm. simpl. eauto. unfold Val.cmpf, Val.cmpf_bool. simpl. rewrite <- Float.cmp_ne_eq. destruct (Float.cmp Cne f Float.zero); constructor. econstructor; split. econstructor; eauto with cshm. simpl. eauto. unfold Val.cmpfs, Val.cmpfs_bool. simpl. rewrite <- Float32.cmp_ne_eq. destruct (Float32.cmp Cne f Float32.zero); constructor. econstructor; split. econstructor; eauto with cshm. simpl. eauto. unfold Val.cmpu, Val.cmpu_bool. simpl. destruct (Int.eq i Int.zero); simpl; constructor. exists Vtrue; split. econstructor; eauto with cshm. constructor. econstructor; split. econstructor; eauto with cshm. simpl. unfold Val.cmpl. simpl. eauto. destruct (Int64.eq i Int64.zero); simpl; constructor.] Proof search time: 1 min, 23 sec Number of successful tactic applications: 1575 Number of failed tactic applications: 8426 Results for lemma make_store_correct: : forall addr ty rhs code e le m b ofs v m' f k, make_store addr ty rhs = OK code -> eval_expr ge e le m addr (Vptr b ofs) -> eval_expr ge e le m rhs v -> assign_loc ty m b ofs v m' -> step ge (State f code k e le m) E0 (State f Sskip k e le m') FAILURE! Tactics applied: 10000 Original Proof: [unfold make_store. intros until k; intros MKSTORE EV1 EV2 ASSIGN. inversion ASSIGN; subst. rewrite H in MKSTORE; inv MKSTORE. econstructor; eauto. rewrite H in MKSTORE; inv MKSTORE. eapply make_memcpy_correct; eauto.] Proof search time: 1 min, 20 sec Number of successful tactic applications: 1574 Number of failed tactic applications: 8427 Results for lemma make_neg_correct: : forall a tya c va v e le m, sem_neg va tya = Some v -> make_neg a tya = OK c -> eval_expr ge e le m a va -> eval_expr ge e le m c v FAILURE! Tactics applied: 10000 Original Proof: [unfold sem_neg, make_neg; intros until m; intros SEM MAKE EV1; destruct (classify_neg tya); inv MAKE; destruct va; inv SEM; eauto with cshm.] Proof search time: 1 min, 11 sec Number of successful tactic applications: 1562 Number of failed tactic applications: 8439 Results for fold 3 Results for lemma transl_binop_correct: : forall op a tya b tyb c va vb v e le m, transl_binop op a tya b tyb = OK c -> sem_binary_operation op va tya vb tyb m = Some v -> eval_expr ge e le m a va -> eval_expr ge e le m b vb -> eval_expr ge e le m c v FAILURE! Tactics applied: 10000 Original Proof: [intros. destruct op; simpl in *. eapply make_add_correct; eauto. eapply make_sub_correct; eauto. eapply make_mul_correct; eauto. eapply make_div_correct; eauto. eapply make_mod_correct; eauto. eapply make_and_correct; eauto. eapply make_or_correct; eauto. eapply make_xor_correct; eauto. eapply make_shl_correct; eauto. eapply make_shr_correct; eauto. eapply make_cmp_correct; eauto. eapply make_cmp_correct; eauto. eapply make_cmp_correct; eauto. eapply make_cmp_correct; eauto. eapply make_cmp_correct; eauto. eapply make_cmp_correct; eauto.] Proof search time: 1 min, 10 sec Number of successful tactic applications: 1804 Number of failed tactic applications: 8197 Results for lemma make_xor_correct: : binary_constructor_correct make_xor sem_xor SUCCESS! Proof Found in EFSM: apply make_binarith_int_correct; econstructor ; Tactics applied: 310 Original Proof: [apply make_binarith_int_correct; intros; auto.] Shorter Proof Found? yes This is a novel proof proof search time: 0 min, 21 sec Number of successful tactic applications: 47 Number of failed tactic applications: 263 Results for lemma block_is_volatile_preserved: : forall b, block_is_volatile tge b = block_is_volatile ge b FAILURE! Tactics applied: 10000 Original Proof: [intros. unfold block_is_volatile. destruct (Genv.find_var_info ge b) eqn:?. exploit var_info_translated; eauto. intros [tv [A B]]. rewrite A. unfold transf_globvar in B. monadInv B. auto. destruct (Genv.find_var_info tge b) eqn:?. exploit var_info_rev_translated; eauto. intros [tv [A B]]. congruence. auto.] Proof search time: 3 min, 5 sec Number of successful tactic applications: 730 Number of failed tactic applications: 9271 Results for lemma make_div_correct: : binary_constructor_correct make_div sem_div SUCCESS! Proof Found in EFSM: apply make_binarith_correct; econstructor ; Tactics applied: 310 Original Proof: [apply make_binarith_correct; intros; auto.] Shorter Proof Found? yes This is a novel proof proof search time: 0 min, 22 sec Number of successful tactic applications: 47 Number of failed tactic applications: 263 Results for lemma typlist_of_arglist_eq: : forall al tyl vl, Clight.eval_exprlist ge e le m al tyl vl -> typlist_of_arglist al tyl = typlist_of_typelist tyl SUCCESS! Proof Found in EFSM: induction 1; simpl ; congruence. Tactics applied: 7154 Original Proof: [induction 1; simpl. auto. f_equal; auto.] Shorter Proof Found? yes This is a novel proof This proof contained a loop around a state proof search time: 0 min, 54 sec Number of successful tactic applications: 1392 Number of failed tactic applications: 5762 Results for lemma transl_step: : forall S1 t S2, Clight.step2 ge S1 t S2 -> forall T1, match_states S1 T1 -> exists T2, plus step tge T1 t T2 /\ match_states S2 T2 FAILURE! Tactics applied: 10000 Original Proof: [induction 1; intros T1 MST; inv MST. monadInv TR. assert (SAME: ts' = ts /\ tk' = tk). inversion MTR. auto. subst ts. unfold make_store, make_memcpy in EQ3. destruct (access_mode (typeof a1)); congruence. destruct SAME; subst ts' tk'. econstructor; split. apply plus_one. eapply make_store_correct; eauto. eapply transl_lvalue_correct; eauto. eapply make_cast_correct; eauto. eapply transl_expr_correct; eauto. eapply match_states_skip; eauto. monadInv TR. inv MTR. econstructor; split. apply plus_one. econstructor. eapply transl_expr_correct; eauto. eapply match_states_skip; eauto. revert TR. simpl. case_eq (classify_fun (typeof a)); try congruence. intros targs tres cc CF TR. monadInv TR. inv MTR. exploit functions_translated; eauto. intros [tfd [FIND TFD]]. rewrite H in CF. simpl in CF. inv CF. econstructor; split. apply plus_one. econstructor; eauto. exploit transl_expr_correct; eauto. exploit transl_arglist_correct; eauto. erewrite typlist_of_arglist_eq by eauto. eapply transl_fundef_sig1; eauto. rewrite H3. auto. econstructor; eauto. econstructor; eauto. simpl. auto. monadInv TR. inv MTR. econstructor; split. apply plus_one. econstructor. eapply transl_arglist_correct; eauto. eapply external_call_symbols_preserved_2; eauto. exact symbols_preserved. eexact (Genv.find_var_info_transf_partial2 transl_fundef transl_globvar _ TRANSL). eexact (Genv.find_var_info_rev_transf_partial2 transl_fundef transl_globvar _ TRANSL). eapply match_states_skip; eauto. monadInv TR. inv MTR. econstructor; split. apply plus_one. constructor. econstructor; eauto. constructor. econstructor; eauto. monadInv TR. inv MTR. inv MK. econstructor; split. apply plus_one. apply step_skip_seq. econstructor; eauto. constructor. monadInv TR. inv MTR. inv MK. econstructor; split. apply plus_one. constructor. econstructor; eauto. simpl. reflexivity. constructor. monadInv TR. inv MTR. inv MK. econstructor; split. apply plus_one. constructor. econstructor; eauto. simpl. reflexivity. constructor. monadInv TR. inv MTR. exploit make_boolean_correct; eauto. exploit transl_expr_correct; eauto. intros [v [A B]]. econstructor; split. apply plus_one. apply step_ifthenelse with (v := v) (b := b); auto. destruct b; econstructor; eauto; constructor. monadInv TR. econstructor; split. eapply star_plus_trans. eapply match_transl_step; eauto. eapply plus_left. constructor. eapply star_left. constructor. apply star_one. constructor. reflexivity. reflexivity. traceEq. econstructor; eauto. constructor. econstructor; eauto. assert ((ts' = Sskip \/ ts' = Sexit ncnt) /\ tk' = tk). destruct H; subst x; monadInv TR; inv MTR; auto. destruct H0. inv MK. econstructor; split. eapply plus_left. destruct H0; subst ts'. 2:constructor. constructor. apply star_one. constructor. traceEq. econstructor; eauto. constructor. econstructor; eauto. monadInv TR. inv MTR. inv MK. econstructor; split. eapply plus_left. constructor. eapply star_left. constructor. eapply star_left. constructor. apply star_one. constructor. reflexivity. reflexivity. traceEq. eapply match_states_skip; eauto. monadInv TR. inv MTR. inv MK. econstructor; split. apply plus_one. constructor. econstructor; eauto. simpl. rewrite H5; simpl. rewrite H7; simpl. eauto. constructor. monadInv TR. inv MTR. inv MK. econstructor; split. eapply plus_left. constructor. apply star_one. constructor. traceEq. eapply match_states_skip; eauto. monadInv TR. inv MTR. econstructor; split. apply plus_one. constructor. eapply match_env_free_blocks; eauto. econstructor; eauto. eapply match_cont_call_cont. eauto. monadInv TR. inv MTR. econstructor; split. apply plus_one. constructor. eapply make_cast_correct; eauto. eapply transl_expr_correct; eauto. eapply match_env_free_blocks; eauto. econstructor; eauto. eapply match_cont_call_cont. eauto. monadInv TR. inv MTR. exploit match_cont_is_call_cont; eauto. intros [A B]. econstructor; split. apply plus_one. apply step_skip_call. auto. eapply match_env_free_blocks; eauto. constructor. eauto. monadInv TR. assert (E: exists b, ts = Sblock (Sswitch b x x0) /\ Switch.switch_argument b v n). { unfold sem_switch_arg in H0. destruct (classify_switch (typeof a)); inv EQ2; econstructor; split; eauto; destruct v; inv H0; constructor. } destruct E as (b & A & B). subst ts. exploit transl_expr_correct; eauto. intro EV. econstructor; split. eapply star_plus_trans. eapply match_transl_step; eauto. apply plus_one. econstructor; eauto. traceEq. econstructor; eauto. apply transl_lbl_stmt_2. apply transl_lbl_stmt_1. eauto. constructor. econstructor. eauto. assert ((ts' = Sskip \/ ts' = Sexit nbrk) /\ tk' = tk). destruct H; subst x; monadInv TR; inv MTR; auto. destruct H0. inv MK. econstructor; split. apply plus_one. destruct H0; subst ts'. 2:constructor. constructor. eapply match_states_skip; eauto. monadInv TR. inv MTR. inv MK. econstructor; split. apply plus_one. constructor. econstructor; eauto. simpl. reflexivity. constructor. monadInv TR. inv MTR. econstructor; split. apply plus_one. constructor. econstructor; eauto. constructor. monadInv TR. inv MTR. generalize TRF. unfold transl_function. intro TRF'. monadInv TRF'. exploit (transl_find_label lbl). eexact EQ. eapply match_cont_call_cont. eauto. rewrite H. intros [ts' [tk'' [nbrk' [ncnt' [A [B C]]]]]]. econstructor; split. apply plus_one. constructor. simpl. eexact A. econstructor; eauto. constructor. inv H. monadInv TR. monadInv EQ. exploit match_cont_is_call_cont; eauto. intros [A B]. exploit match_env_alloc_variables; eauto. apply match_env_empty. intros [te1 [C D]]. econstructor; split. apply plus_one. eapply step_internal_function. simpl. rewrite list_map_compose. simpl. assumption. simpl. auto. simpl. auto. simpl. eauto. simpl. rewrite create_undef_temps_match. eapply bind_parameter_temps_match; eauto. simpl. econstructor; eauto. unfold transl_function. rewrite EQ0; simpl. auto. constructor. simpl in TR. destruct (signature_eq (ef_sig ef) (signature_of_type targs tres cconv)); inv TR. exploit match_cont_is_call_cont; eauto. intros [A B]. econstructor; split. apply plus_one. constructor. eauto. eapply external_call_symbols_preserved_2; eauto. exact symbols_preserved. eexact (Genv.find_var_info_transf_partial2 transl_fundef transl_globvar _ TRANSL). eexact (Genv.find_var_info_rev_transf_partial2 transl_fundef transl_globvar _ TRANSL). econstructor; eauto. inv MK. econstructor; split. apply plus_one. constructor. econstructor; eauto. simpl; reflexivity. constructor.] Proof search time: 2 min, 21 sec Number of successful tactic applications: 1584 Number of failed tactic applications: 8417 Results for lemma symbols_preserved: : forall s, Genv.find_symbol tge s = Genv.find_symbol ge s FAILURE! Tactics applied: 10000 Original Proof: [Proof (Genv.find_symbol_transf_partial2 transl_fundef transl_globvar _ TRANSL).] Proof search time: 1 min, 0 sec Number of successful tactic applications: 887 Number of failed tactic applications: 9114 Results for lemma make_cmp_correct: : forall cmp a tya b tyb c va vb v e le m, sem_cmp cmp va tya vb tyb m = Some v -> make_cmp cmp a tya b tyb = OK c -> eval_expr ge e le m a va -> eval_expr ge e le m b vb -> eval_expr ge e le m c v FAILURE! Tactics applied: 10000 Original Proof: [unfold sem_cmp, make_cmp; intros until m; intros SEM MAKE EV1 EV2; destruct (classify_cmp tya tyb). - inv MAKE. destruct (Val.cmpu_bool (Mem.valid_pointer m) cmp va vb) as [bv|] eqn:E; simpl in SEM; inv SEM. econstructor; eauto. simpl. unfold Val.cmpu. rewrite E. auto. - inv MAKE. destruct vb; try discriminate. set (vb := Vint (Int.repr (Int64.unsigned i))) in *. destruct (Val.cmpu_bool (Mem.valid_pointer m) cmp va vb) as [bv|] eqn:E; simpl in SEM; inv SEM. econstructor; eauto with cshm. simpl. change (Vint (Int64.loword i)) with vb. unfold Val.cmpu. rewrite E. auto. - inv MAKE. destruct va; try discriminate. set (va := Vint (Int.repr (Int64.unsigned i))) in *. destruct (Val.cmpu_bool (Mem.valid_pointer m) cmp va vb) as [bv|] eqn:E; simpl in SEM; inv SEM. econstructor; eauto with cshm. simpl. change (Vint (Int64.loword i)) with va. unfold Val.cmpu. rewrite E. auto. - eapply make_binarith_correct; eauto; intros; auto.] Proof search time: 1 min, 9 sec Number of successful tactic applications: 1728 Number of failed tactic applications: 8273 Results for lemma function_ptr_translated: : forall b f, Genv.find_funct_ptr ge b = Some f -> exists tf, Genv.find_funct_ptr tge b = Some tf /\ transl_fundef f = OK tf FAILURE! Tactics applied: 10000 Original Proof: [Proof (Genv.find_funct_ptr_transf_partial2 transl_fundef transl_globvar _ TRANSL).] Proof search time: 0 min, 56 sec Number of successful tactic applications: 1087 Number of failed tactic applications: 8914 Results for lemma transl_find_label: : forall s nbrk ncnt k ts tk (TR: transl_statement tyret nbrk ncnt s = OK ts) (MC: match_cont tyret nbrk ncnt k tk), match Clight.find_label lbl s k with | None => find_label lbl ts tk = None | Some (s', k') => exists ts', exists tk', exists nbrk', exists ncnt', find_label lbl ts tk = Some (ts', tk') /\ transl_statement tyret nbrk' ncnt' s' = OK ts' /\ match_cont tyret nbrk' ncnt' k' tk' end with transl_find_label_ls: forall ls nbrk ncnt k tls tk (TR: transl_lbl_stmt tyret nbrk ncnt ls = OK tls) (MC: match_cont tyret nbrk ncnt k tk), match Clight.find_label_ls lbl ls k with | None => find_label_ls lbl tls tk = None | Some (s', k') => exists ts', exists tk', exists nbrk', exists ncnt', find_label_ls lbl tls tk = Some (ts', tk') /\ transl_statement tyret nbrk' ncnt' s' = OK ts' /\ match_cont tyret nbrk' ncnt' k' tk' end SUCCESS! Proof Found in EFSM: auto. auto. Tactics applied: 317 Original Proof: [intro s; case s; intros; try (monadInv TR); simpl. auto. unfold make_store, make_memcpy in EQ3. destruct (access_mode (typeof e)); inv EQ3; auto. auto. simpl in TR. destruct (classify_fun (typeof e)); monadInv TR. auto. auto. exploit (transl_find_label s0 nbrk ncnt (Clight.Kseq s1 k)); eauto. constructor; eauto. destruct (Clight.find_label lbl s0 (Clight.Kseq s1 k)) as [[s' k'] | ]. intros [ts' [tk' [nbrk' [ncnt' [A [B C]]]]]]. rewrite A. exists ts'; exists tk'; exists nbrk'; exists ncnt'; auto. intro. rewrite H. eapply transl_find_label; eauto. exploit (transl_find_label s0); eauto. destruct (Clight.find_label lbl s0 k) as [[s' k'] | ]. intros [ts' [tk' [nbrk' [ncnt' [A [B C]]]]]]. rewrite A. exists ts'; exists tk'; exists nbrk'; exists ncnt'; auto. intro. rewrite H. eapply transl_find_label; eauto. exploit (transl_find_label s0 1%nat 0%nat (Kloop1 s0 s1 k)); eauto. econstructor; eauto. destruct (Clight.find_label lbl s0 (Kloop1 s0 s1 k)) as [[s' k'] | ]. intros [ts' [tk' [nbrk' [ncnt' [A [B C]]]]]]. rewrite A. exists ts'; exists tk'; exists nbrk'; exists ncnt'; auto. intro. rewrite H. eapply transl_find_label; eauto. econstructor; eauto. auto. auto. simpl in TR. destruct o; monadInv TR. auto. auto. assert (exists b, ts = Sblock (Sswitch b x x0)). { destruct (classify_switch (typeof e)); inv EQ2; econstructor; eauto. } destruct H as [b EQ3]; rewrite EQ3; simpl. eapply transl_find_label_ls with (k := Clight.Kswitch k); eauto. econstructor; eauto. destruct (ident_eq lbl l). exists x; exists tk; exists nbrk; exists ncnt; auto. eapply transl_find_label; eauto. auto. intro ls; case ls; intros; monadInv TR; simpl. auto. exploit (transl_find_label s nbrk ncnt (Clight.Kseq (seq_of_labeled_statement l) k)); eauto. econstructor; eauto. apply transl_lbl_stmt_2; eauto. destruct (Clight.find_label lbl s (Clight.Kseq (seq_of_labeled_statement l) k)) as [[s' k'] | ]. intros [ts' [tk' [nbrk' [ncnt' [A [B C]]]]]]. rewrite A. exists ts'; exists tk'; exists nbrk'; exists ncnt'; auto. intro. rewrite H. eapply transl_find_label_ls; eauto.] Shorter Proof Found? yes This is a novel proof This proof contained a loop around a state This proof contained a sequence of repeated tactics proof search time: 0 min, 22 sec Number of successful tactic applications: 52 Number of failed tactic applications: 265 Results for lemma make_cmp_ne_zero_correct: : forall e le m a n, eval_expr ge e le m a (Vint n) -> eval_expr ge e le m (make_cmp_ne_zero a) (Vint (if Int.eq n Int.zero then Int.zero else Int.one)) FAILURE! Tactics applied: 10000 Original Proof: [intros. assert (DEFAULT: eval_expr ge e le m (Ebinop (Ocmp Cne) a (make_intconst Int.zero)) (Vint (if Int.eq n Int.zero then Int.zero else Int.one))). econstructor; eauto with cshm. simpl. unfold Val.cmp, Val.cmp_bool. unfold Int.cmp. destruct (Int.eq n Int.zero); auto. assert (CMP: forall ob, Val.of_optbool ob = Vint n -> n = (if Int.eq n Int.zero then Int.zero else Int.one)). intros. destruct ob; simpl in H0; inv H0. destruct b; inv H2. rewrite Int.eq_false. auto. apply Int.one_not_zero. rewrite Int.eq_true. auto. destruct a; simpl; auto. destruct b; auto. inv H. econstructor; eauto. rewrite H6. decEq. decEq. simpl in H6. inv H6. unfold Val.cmp in H0. eauto. inv H. econstructor; eauto. rewrite H6. decEq. decEq. simpl in H6. inv H6. unfold Val.cmp in H0. eauto. inv H. econstructor; eauto. rewrite H6. decEq. decEq. simpl in H6. inv H6. unfold Val.cmp in H0. eauto. inv H. econstructor; eauto. rewrite H6. decEq. decEq. simpl in H6. unfold Val.cmpfs in H6. destruct (Val.cmpfs_bool c v1 v2) as [[]|]; inv H6; reflexivity. inv H. econstructor; eauto. rewrite H6. decEq. decEq. simpl in H6. unfold Val.cmpl in H6. destruct (Val.cmpl_bool c v1 v2) as [[]|]; inv H6; reflexivity. inv H. econstructor; eauto. rewrite H6. decEq. decEq. simpl in H6. unfold Val.cmplu in H6. destruct (Val.cmplu_bool c v1 v2) as [[]|]; inv H6; reflexivity.] Proof search time: 0 min, 57 sec Number of successful tactic applications: 1293 Number of failed tactic applications: 8708 Results for lemma make_intconst_correct: : forall n e le m, eval_expr ge e le m (make_intconst n) (Vint n) SUCCESS! Proof Found in EFSM: econstructor ; split. Tactics applied: 259 Original Proof: [intros. unfold make_intconst. econstructor. reflexivity.] Shorter Proof Found? yes This is a novel proof proof search time: 0 min, 21 sec Number of successful tactic applications: 25 Number of failed tactic applications: 234 Results for lemma make_sub_correct: : binary_constructor_correct make_sub sem_sub FAILURE! Tactics applied: 10000 Original Proof: [red; unfold make_sub, sem_sub; intros until m; intros SEM MAKE EV1 EV2; destruct (classify_sub tya tyb); inv MAKE. - destruct va; try discriminate; destruct vb; inv SEM; eauto with cshm. - destruct va; try discriminate; destruct vb; inv SEM. destruct (eq_block b0 b1); try discriminate. destruct (Int.eq (Int.repr (sizeof ty)) Int.zero) eqn:E; inv H0. econstructor; eauto with cshm. rewrite dec_eq_true. simpl. rewrite E; auto. - destruct va; try discriminate; destruct vb; inv SEM; eauto with cshm. - eapply make_binarith_correct; eauto; intros; auto.] Proof search time: 0 min, 50 sec Number of successful tactic applications: 1596 Number of failed tactic applications: 8405 Results for fold 4 Results for lemma small_shift_amount_3: : forall i, Int.ltu i Int64.iwordsize' = true -> Int64.unsigned (Int64.repr (Int.unsigned i)) = Int.unsigned i FAILURE! Tactics applied: 10000 Original Proof: [intros. apply Int.ltu_inv in H. comput (Int.unsigned Int64.iwordsize'). apply Int64.unsigned_repr. comput Int64.max_unsigned; omega.] Proof search time: 1 min, 26 sec Number of successful tactic applications: 576 Number of failed tactic applications: 9425 Results for lemma make_floatofsingle_correct: : forall a n e le m, eval_expr ge e le m a (Vsingle n) -> eval_expr ge e le m (make_floatofsingle a) (Vfloat (Float.of_single n)) SUCCESS! Proof Found in EFSM: econstructor ; eauto. Tactics applied: 1675 Original Proof: [intros. econstructor. eauto. auto.] Shorter Proof Found? yes This is a novel proof proof search time: 1 min, 16 sec Number of successful tactic applications: 268 Number of failed tactic applications: 1407 Results for lemma transl_expr_lvalue: : forall ge e le m a loc ofs ta, Clight.eval_lvalue ge e le m a loc ofs -> transl_expr a = OK ta -> (exists tb, transl_lvalue a = OK tb /\ make_load tb (typeof a) = OK ta) FAILURE! Tactics applied: 10000 Original Proof: [intros until ta; intros EVAL TR. inv EVAL; simpl in TR. exists (Eaddrof id); auto. exists (Eaddrof id); auto. monadInv TR. exists x; auto. rewrite H0 in TR. monadInv TR. econstructor; split. simpl. rewrite H0. rewrite EQ; rewrite EQ1; simpl; eauto. auto. rewrite H0 in TR. monadInv TR. econstructor; split. simpl. rewrite H0. rewrite EQ; simpl; eauto. auto.] Proof search time: 2 min, 20 sec Number of successful tactic applications: 1327 Number of failed tactic applications: 8674 Results for lemma make_longconst_correct: : forall n e le m, eval_expr ge e le m (make_longconst n) (Vlong n) SUCCESS! Proof Found in EFSM: econstructor ; eauto. Tactics applied: 1569 Original Proof: [intros. unfold make_floatconst. econstructor. reflexivity.] Shorter Proof Found? yes This is a novel proof proof search time: 1 min, 14 sec Number of successful tactic applications: 219 Number of failed tactic applications: 1350 Results for lemma match_env_empty: : match_env Clight.empty_env Csharpminor.empty_env FAILURE! Tactics applied: 10000 Original Proof: [unfold Clight.empty_env, Csharpminor.empty_env. constructor. intros until ty. repeat rewrite PTree.gempty. congruence. intros until sz. rewrite PTree.gempty. congruence.] Proof search time: 1 min, 39 sec Number of successful tactic applications: 947 Number of failed tactic applications: 9054 Results for lemma transl_lbl_stmt_1: : forall tyret nbrk ncnt n sl tsl, transl_lbl_stmt tyret nbrk ncnt sl = OK tsl -> transl_lbl_stmt tyret nbrk ncnt (Clight.select_switch n sl) = OK (select_switch n tsl) FAILURE! Tactics applied: 10000 Original Proof: [intros until n. assert (DFL: forall sl tsl, transl_lbl_stmt tyret nbrk ncnt sl = OK tsl -> transl_lbl_stmt tyret nbrk ncnt (Clight.select_switch_default sl) = OK (select_switch_default tsl)). { induction sl; simpl; intros. inv H; auto. monadInv H. simpl. destruct o; eauto. simpl; rewrite EQ; simpl; rewrite EQ1; auto. } assert (CASE: forall sl tsl, transl_lbl_stmt tyret nbrk ncnt sl = OK tsl -> match Clight.select_switch_case n sl with | None => select_switch_case n tsl = None | Some sl' => exists tsl', select_switch_case n tsl = Some tsl' /\ transl_lbl_stmt tyret nbrk ncnt sl' = OK tsl' end). { induction sl; simpl; intros. inv H; auto. monadInv H; simpl. destruct o. destruct (zeq z n). econstructor; split; eauto. simpl; rewrite EQ; simpl; rewrite EQ1; auto. apply IHsl; auto. apply IHsl; auto. } intros. specialize (CASE _ _ H). unfold Clight.select_switch, select_switch. destruct (Clight.select_switch_case n sl) as [sl'|]. destruct CASE as [tsl' [P Q]]. rewrite P, Q. auto. rewrite CASE. auto.] Proof search time: 1 min, 28 sec Number of successful tactic applications: 611 Number of failed tactic applications: 9390 Results for lemma transl_lbl_stmt_2: : forall tyret nbrk ncnt sl tsl, transl_lbl_stmt tyret nbrk ncnt sl = OK tsl -> transl_statement tyret nbrk ncnt (seq_of_labeled_statement sl) = OK (seq_of_lbl_stmt tsl) FAILURE! Tactics applied: 10000 Original Proof: [induction sl; intros. monadInv H. auto. monadInv H. simpl. rewrite EQ; simpl. rewrite (IHsl _ EQ1). simpl. auto.] Proof search time: 1 min, 27 sec Number of successful tactic applications: 611 Number of failed tactic applications: 9390 Results for lemma make_mod_correct: : binary_constructor_correct make_mod sem_mod SUCCESS! Proof Found in EFSM: apply make_binarith_int_correct; traceEq. Tactics applied: 818 Original Proof: [apply make_binarith_int_correct; intros; auto.] Shorter Proof Found? yes This is a novel proof proof search time: 1 min, 15 sec Number of successful tactic applications: 178 Number of failed tactic applications: 640 Results for lemma transl_arglist_correct: : forall al tyl vl, Clight.eval_exprlist ge e le m al tyl vl -> forall tal, transl_arglist al tyl = OK tal -> Csharpminor.eval_exprlist tge te le m tal vl FAILURE! Tactics applied: 10000 Original Proof: [induction 1; intros. monadInv H. constructor. monadInv H2. constructor. eapply make_cast_correct; eauto. eapply transl_expr_correct; eauto. auto.] Proof search time: 1 min, 49 sec Number of successful tactic applications: 1709 Number of failed tactic applications: 8292 Results for lemma make_absfloat_correct: : forall a tya c va v e le m, sem_absfloat va tya = Some v -> make_absfloat a tya = OK c -> eval_expr ge e le m a va -> eval_expr ge e le m c v FAILURE! Tactics applied: 10000 Original Proof: [unfold sem_absfloat, make_absfloat; intros until m; intros SEM MAKE EV1; destruct (classify_neg tya); inv MAKE; destruct va; inv SEM; eauto with cshm. unfold make_floatoflong, cast_long_float. destruct s. econstructor. econstructor; simpl; eauto. simpl; eauto. simpl; eauto. econstructor. econstructor; simpl; eauto. simpl; eauto. simpl; eauto.] Proof search time: 1 min, 38 sec Number of successful tactic applications: 1489 Number of failed tactic applications: 8512 Results for lemma match_cont_is_call_cont: : forall tyret nbrk ncnt k tk tyret' nbrk' ncnt', match_cont tyret nbrk ncnt k tk -> Clight.is_call_cont k -> match_cont tyret' nbrk' ncnt' k tk /\ is_call_cont tk FAILURE! Tactics applied: 10000 Original Proof: [intros. inv H; simpl in H0; try contradiction; simpl. split; auto; constructor. split; auto; econstructor; eauto.] Proof search time: 2 min, 16 sec Number of successful tactic applications: 1922 Number of failed tactic applications: 8079 Results for lemma make_notbool_correct: : forall a tya c va v e le m, sem_notbool va tya = Some v -> make_notbool a tya = OK c -> eval_expr ge e le m a va -> eval_expr ge e le m c v FAILURE! Tactics applied: 10000 Original Proof: [unfold sem_notbool, make_notbool; intros until m; intros SEM MAKE EV1; destruct (classify_bool tya); inv MAKE; destruct va; inv SEM; eauto with cshm.] Proof search time: 1 min, 38 sec Number of successful tactic applications: 1493 Number of failed tactic applications: 8508 Results for lemma make_and_correct: : binary_constructor_correct make_and sem_and SUCCESS! Proof Found in EFSM: apply make_binarith_int_correct; traceEq. Tactics applied: 818 Original Proof: [apply make_binarith_int_correct; intros; auto.] Shorter Proof Found? yes This is a novel proof proof search time: 1 min, 14 sec Number of successful tactic applications: 178 Number of failed tactic applications: 640 Results for fold 5 Results for lemma make_floatconst_correct: : forall n e le m, eval_expr ge e le m (make_floatconst n) (Vfloat n) SUCCESS! Proof Found in EFSM: econstructor ; reflexivity. Tactics applied: 2461 Original Proof: [intros. unfold make_floatconst. econstructor. reflexivity.] Shorter Proof Found? yes This is a novel proof proof search time: 1 min, 15 sec Number of successful tactic applications: 272 Number of failed tactic applications: 2189 Results for lemma match_env_globals: : forall e te id, match_env e te -> e!id = None -> te!id = None FAILURE! Tactics applied: 10000 Original Proof: [intros. destruct (te!id) as [[b sz] | ] eqn:?; auto. exploit me_local_inv; eauto. intros [ty EQ]. congruence.] Proof search time: 1 min, 35 sec Number of successful tactic applications: 1259 Number of failed tactic applications: 8742 Results for lemma var_info_rev_translated: : forall b tv, Genv.find_var_info tge b = Some tv -> exists v, Genv.find_var_info ge b = Some v /\ transf_globvar transl_globvar v = OK tv FAILURE! Tactics applied: 10000 Original Proof: [Proof (Genv.find_var_info_rev_transf_partial2 transl_fundef transl_globvar _ TRANSL).] Proof search time: 1 min, 35 sec Number of successful tactic applications: 1073 Number of failed tactic applications: 8928 Results for lemma make_mul_correct: : binary_constructor_correct make_mul sem_mul SUCCESS! Proof Found in EFSM: apply make_binarith_correct; auto. Tactics applied: 694 Original Proof: [apply make_binarith_correct; intros; auto.] Shorter Proof Found? yes This is a novel proof proof search time: 1 min, 14 sec Number of successful tactic applications: 151 Number of failed tactic applications: 543 Results for lemma functions_translated: : forall v f, Genv.find_funct ge v = Some f -> exists tf, Genv.find_funct tge v = Some tf /\ transl_fundef f = OK tf FAILURE! Tactics applied: 10000 Original Proof: [Proof (Genv.find_funct_transf_partial2 transl_fundef transl_globvar _ TRANSL).] Proof search time: 1 min, 33 sec Number of successful tactic applications: 1053 Number of failed tactic applications: 8948 Results for lemma make_memcpy_correct: : forall f dst src ty k e le m b ofs v m', eval_expr ge e le m dst (Vptr b ofs) -> eval_expr ge e le m src v -> assign_loc ty m b ofs v m' -> access_mode ty = By_copy -> step ge (State f (make_memcpy dst src ty) k e le m) E0 (State f Sskip k e le m') FAILURE! Tactics applied: 10000 Original Proof: [intros. inv H1; try congruence. unfold make_memcpy. change le with (set_optvar None Vundef le) at 2. econstructor. econstructor. eauto. econstructor. eauto. constructor. econstructor; eauto. apply alignof_blockcopy_1248. apply sizeof_pos. apply sizeof_alignof_blockcopy_compat.] Proof search time: 1 min, 45 sec Number of successful tactic applications: 1624 Number of failed tactic applications: 8377 Results for lemma transl_expr_lvalue_correct: : (forall a v, Clight.eval_expr ge e le m a v -> forall ta (TR: transl_expr a = OK ta) , Csharpminor.eval_expr tge te le m ta v) /\(forall a b ofs, Clight.eval_lvalue ge e le m a b ofs -> forall ta (TR: transl_lvalue a = OK ta), Csharpminor.eval_expr tge te le m ta (Vptr b ofs)) FAILURE! Tactics applied: 10000 Original Proof: [apply eval_expr_lvalue_ind; intros; try (monadInv TR). apply make_intconst_correct. apply make_floatconst_correct. apply make_singleconst_correct. apply make_longconst_correct. constructor; auto. simpl in TR. auto. eapply transl_unop_correct; eauto. eapply transl_binop_correct; eauto. eapply make_cast_correct; eauto. exploit transl_expr_lvalue; eauto. intros [tb [TRLVAL MKLOAD]]. eapply make_load_correct; eauto. exploit (me_local _ _ MENV); eauto. intros EQ. econstructor. eapply eval_var_addr_local. eauto. econstructor. eapply eval_var_addr_global. eapply match_env_globals; eauto. rewrite symbols_preserved. auto. simpl in TR. eauto. simpl in TR. rewrite H1 in TR. monadInv TR. eapply eval_Ebinop; eauto. apply make_intconst_correct. simpl. congruence. simpl in TR. rewrite H1 in TR. eauto.] Proof search time: 1 min, 59 sec Number of successful tactic applications: 1546 Number of failed tactic applications: 8455 Results for lemma make_binarith_correct: : binary_constructor_correct (make_binarith iop iopu fop sop lop lopu) (sem_binarith sem_int sem_long sem_float sem_single) FAILURE! Tactics applied: 10000 Original Proof: [red; unfold make_binarith, sem_binarith; intros until m; intros SEM MAKE EV1 EV2. set (cls := classify_binarith tya tyb) in *. set (ty := binarith_type cls) in *. monadInv MAKE. destruct (sem_cast va tya ty) as [va'|] eqn:Ca; try discriminate. destruct (sem_cast vb tyb ty) as [vb'|] eqn:Cb; try discriminate. exploit make_cast_correct. eexact EQ. eauto. eauto. intros EV1'. exploit make_cast_correct. eexact EQ1. eauto. eauto. intros EV2'. destruct cls; inv EQ2; destruct va'; try discriminate; destruct vb'; try discriminate. - destruct s; inv H0; econstructor; eauto with cshm. rewrite iop_ok; auto. rewrite iopu_ok; auto. - destruct s; inv H0; econstructor; eauto with cshm. rewrite lop_ok; auto. rewrite lopu_ok; auto. - erewrite <- fop_ok in SEM; eauto with cshm. - erewrite <- sop_ok in SEM; eauto with cshm.] Proof search time: 2 min, 5 sec Number of successful tactic applications: 1910 Number of failed tactic applications: 8091 Results for lemma make_add_correct: : binary_constructor_correct make_add sem_add FAILURE! Tactics applied: 10000 Original Proof: [red; unfold make_add, sem_add; intros until m; intros SEM MAKE EV1 EV2; destruct (classify_add tya tyb); inv MAKE. - destruct va; try discriminate; destruct vb; inv SEM; eauto with cshm. - destruct va; try discriminate; destruct vb; inv SEM; eauto with cshm. - destruct va; try discriminate; destruct vb; inv SEM; eauto with cshm. - destruct va; try discriminate; destruct vb; inv SEM; eauto with cshm. - eapply make_binarith_correct; eauto; intros; auto.] Proof search time: 1 min, 44 sec Number of successful tactic applications: 1908 Number of failed tactic applications: 8093 Results for lemma make_notint_correct: : forall a tya c va v e le m, sem_notint va tya = Some v -> make_notint a tya = OK c -> eval_expr ge e le m a va -> eval_expr ge e le m c v FAILURE! Tactics applied: 10000 Original Proof: [unfold sem_notint, make_notint; intros until m; intros SEM MAKE EV1; destruct (classify_notint tya); inv MAKE; destruct va; inv SEM; eauto with cshm.] Proof search time: 1 min, 37 sec Number of successful tactic applications: 1554 Number of failed tactic applications: 8447 Results for lemma make_shl_correct: : binary_constructor_correct make_shl sem_shl FAILURE! Tactics applied: 10000 Original Proof: [red; unfold make_shl, sem_shl, sem_shift; intros until m; intros SEM MAKE EV1 EV2; destruct (classify_shift tya tyb); inv MAKE; destruct va; try discriminate; destruct vb; try discriminate. - destruct (Int.ltu i0 Int.iwordsize) eqn:E; inv SEM. econstructor; eauto. simpl; rewrite E; auto. - destruct (Int64.ltu i0 Int64.iwordsize) eqn:E; inv SEM. exploit small_shift_amount_1; eauto. intros [A B]. econstructor; eauto with cshm. simpl. rewrite A. f_equal; f_equal. unfold Int64.shl', Int64.shl. rewrite B; auto. - destruct (Int64.ltu i0 (Int64.repr 32)) eqn:E; inv SEM. econstructor; eauto with cshm. simpl. rewrite small_shift_amount_2; auto. - destruct (Int.ltu i0 Int64.iwordsize') eqn:E; inv SEM. econstructor; eauto with cshm. simpl. rewrite E. unfold Int64.shl', Int64.shl. rewrite small_shift_amount_3; auto.] Proof search time: 1 min, 45 sec Number of successful tactic applications: 1936 Number of failed tactic applications: 8065 Results for lemma make_cast_int_correct: : forall e le m a n sz si, eval_expr ge e le m a (Vint n) -> eval_expr ge e le m (make_cast_int a sz si) (Vint (cast_int_int sz si n)) FAILURE! Tactics applied: 10000 Original Proof: [intros. unfold make_cast_int, cast_int_int. destruct sz. destruct si; eauto with cshm. destruct si; eauto with cshm. auto. apply make_cmp_ne_zero_correct; auto.] Proof search time: 1 min, 32 sec Number of successful tactic applications: 1324 Number of failed tactic applications: 8677 Results for lemma make_singleoffloat_correct: : forall a n e le m, eval_expr ge e le m a (Vfloat n) -> eval_expr ge e le m (make_singleoffloat a) (Vsingle (Float.to_single n)) SUCCESS! Proof Found in EFSM: econstructor ; eauto. Tactics applied: 2489 Original Proof: [intros. econstructor. eauto. auto.] Shorter Proof Found? yes This is a novel proof proof search time: 1 min, 16 sec Number of successful tactic applications: 366 Number of failed tactic applications: 2123 OVERALL RESULTS SUMMARY EFSMProver proved 14 out of 65 lemmas. Success rate of 21.53846153846154% There were 0 errors. 51 proof attempts exhausted the automaton On average, a proof was found after applying 1430 tactics The longest proof consisted of 3 tactics There were 14 shorter proofs found Of the 51 failures, 51 of them used all 10000 tactics There were 0 reused proofs found There were 14 novel proofs found Of the 51 failures, the average number of tactics used was 10000 On average, a proof was found after 0 min, 57 sec On average, a failed proof attempt took 1 min, 35 sec On average, any (success or failure) proof attempt took 1 min, 26 sec The longest time to find a proof was 1 min, 16 sec The shortest time to find a proof was 0 min, 10 sec There were 1 proofs containing repeated tactics There were 2 proofs that repeated states