125
126 if (is_merged(sm) || sm->left || sm->right)
127 return 0;
128 if (!rl_to_sval(rl, &sval))
129 return 0;
130 if (!estate_rl(sm->state))
131 return 0;
132
133 orig_rl = cast_rl(rl_type(rl), estate_rl(sm->state));
134 split_comparison_rl(orig_rl, comparison, rl, &true_rl, &false_rl, NULL, NULL);
135
136 true_rl = rl_truncate_cast(estate_type(sm->state), true_rl);
137 false_rl = rl_truncate_cast(estate_type(sm->state), false_rl);
138 if (is_whole_rl(true_rl) || is_whole_rl(false_rl) ||
139 !true_rl || !false_rl ||
140 rl_equiv(orig_rl, true_rl) || rl_equiv(orig_rl, false_rl) ||
141 rl_equiv(estate_rl(sm->state), true_rl) || rl_equiv(estate_rl(sm->state), false_rl))
142 return 0;
143
144 if (rl_intersection(true_rl, false_rl)) {
145 sm_perror("parsing (%s (%s) %s %s)",
146 sm->name, sm->state->name, show_special(comparison), show_rl(rl));
147 sm_msg("true_rl = %s false_rl = %s intersection = %s",
148 show_rl(true_rl), show_rl(false_rl), show_rl(rl_intersection(true_rl, false_rl)));
149 return 0;
150 }
151
152 if (implied_debug)
153 sm_msg("fake_history: %s vs %s. %s %s %s. --> T: %s F: %s",
154 sm->name, show_rl(rl), sm->state->name, show_special(comparison), show_rl(rl),
155 show_rl(true_rl), show_rl(false_rl));
156
157 true_sm = clone_sm(sm);
158 false_sm = clone_sm(sm);
159
160 true_sm->state = clone_partial_estate(sm->state, true_rl);
161 free_slist(&true_sm->possible);
162 add_possible_sm(true_sm, true_sm);
163 false_sm->state = clone_partial_estate(sm->state, false_rl);
164 free_slist(&false_sm->possible);
165 add_possible_sm(false_sm, false_sm);
166
167 true_stree = clone_stree(sm->pool);
168 false_stree = clone_stree(sm->pool);
790
791 return 1;
792 }
793
794 static int handled_by_extra_states(struct expression *expr,
795 struct stree **implied_true,
796 struct stree **implied_false)
797 {
798 sval_t sval;
799
800 /* If the expression is known then it has no implications. */
801 if (get_implied_value(expr, &sval))
802 return true;
803
804 if (expr->type == EXPR_COMPARE)
805 return handle_comparison(expr, implied_true, implied_false);
806 else
807 return handle_zero_comparison(expr, implied_true, implied_false);
808 }
809
810 static int handled_by_stored_conditions(struct expression *expr,
811 struct stree **implied_true,
812 struct stree **implied_false)
813 {
814 struct state_list *true_stack = NULL;
815 struct state_list *false_stack = NULL;
816 struct stree *pre_stree;
817 struct sm_state *sm;
818
819 sm = stored_condition_implication_hook(expr, &true_stack, &false_stack);
820 if (!sm)
821 return 0;
822
823 pre_stree = clone_stree(__get_cur_stree());
824
825 *implied_true = filter_stack(sm, pre_stree, false_stack, true_stack);
826 *implied_false = filter_stack(sm, pre_stree, true_stack, false_stack);
827
828 free_stree(&pre_stree);
829 free_slist(&true_stack);
830 free_slist(&false_stack);
831
832 return 1;
833 }
834
835 static struct stree *saved_implied_true;
836 static struct stree *saved_implied_false;
837 static struct stree *extra_saved_implied_true;
838 static struct stree *extra_saved_implied_false;
839
840 static void separate_extra_states(struct stree **implied_true,
841 struct stree **implied_false)
842 {
843 struct sm_state *sm;
844
845 /* We process extra states later to preserve the implications. */
846 FOR_EACH_SM(*implied_true, sm) {
847 if (sm->owner == SMATCH_EXTRA)
848 overwrite_sm_state_stree(&extra_saved_implied_true, sm);
849 } END_FOR_EACH_SM(sm);
850 FOR_EACH_SM(extra_saved_implied_true, sm) {
851 delete_state_stree(implied_true, sm->owner, sm->name, sm->sym);
852 } END_FOR_EACH_SM(sm);
853
854 FOR_EACH_SM(*implied_false, sm) {
855 if (sm->owner == SMATCH_EXTRA)
856 overwrite_sm_state_stree(&extra_saved_implied_false, sm);
857 } END_FOR_EACH_SM(sm);
858 FOR_EACH_SM(extra_saved_implied_false, sm) {
859 delete_state_stree(implied_false, sm->owner, sm->name, sm->sym);
860 } END_FOR_EACH_SM(sm);
861 }
862
863 static void get_tf_states(struct expression *expr,
864 struct stree **implied_true,
865 struct stree **implied_false)
866 {
867 if (handled_by_comparison_hook(expr, implied_true, implied_false))
868 return;
869
870 if (handled_by_extra_states(expr, implied_true, implied_false)) {
871 separate_extra_states(implied_true, implied_false);
872 return;
873 }
874
875 if (handled_by_stored_conditions(expr, implied_true, implied_false))
876 return;
877 }
878
879 static void save_implications_hook(struct expression *expr)
880 {
881 if (going_too_slow())
882 return;
883 get_tf_states(expr, &saved_implied_true, &saved_implied_false);
884 }
885
886 static void set_implied_states(struct expression *expr)
887 {
888 struct sm_state *sm;
889
890 if (implied_debug &&
891 (expr || saved_implied_true || saved_implied_false)) {
1121
1122 value = value_expr(sval.value);
1123 comparison = compare_expression(left, op, value);
1124
1125 if (!assume(comparison))
1126 return 0;
1127 ret = is_impossible_path();
1128 end_assume();
1129
1130 return ret;
1131 }
1132
1133 void __extra_match_condition(struct expression *expr);
1134 void __comparison_match_condition(struct expression *expr);
1135 void __stored_condition(struct expression *expr);
1136 void register_implications(int id)
1137 {
1138 add_hook(&save_implications_hook, CONDITION_HOOK);
1139 add_hook(&set_implied_states, CONDITION_HOOK);
1140 add_hook(&__extra_match_condition, CONDITION_HOOK);
1141 add_hook(&set_extra_implied_states, CONDITION_HOOK);
1142 add_hook(&__comparison_match_condition, CONDITION_HOOK);
1143 add_hook(&__stored_condition, CONDITION_HOOK);
1144 add_hook(&match_end_func, END_FUNC_HOOK);
1145 }
|
125
126 if (is_merged(sm) || sm->left || sm->right)
127 return 0;
128 if (!rl_to_sval(rl, &sval))
129 return 0;
130 if (!estate_rl(sm->state))
131 return 0;
132
133 orig_rl = cast_rl(rl_type(rl), estate_rl(sm->state));
134 split_comparison_rl(orig_rl, comparison, rl, &true_rl, &false_rl, NULL, NULL);
135
136 true_rl = rl_truncate_cast(estate_type(sm->state), true_rl);
137 false_rl = rl_truncate_cast(estate_type(sm->state), false_rl);
138 if (is_whole_rl(true_rl) || is_whole_rl(false_rl) ||
139 !true_rl || !false_rl ||
140 rl_equiv(orig_rl, true_rl) || rl_equiv(orig_rl, false_rl) ||
141 rl_equiv(estate_rl(sm->state), true_rl) || rl_equiv(estate_rl(sm->state), false_rl))
142 return 0;
143
144 if (rl_intersection(true_rl, false_rl)) {
145 /*
146 * Normally these won't intersect, but one exception is when
147 * we're dealing with mtags. We have a long list of mtags and
148 * then negate the list. Now it's over the limit for mtag list
149 * length and we squash it down to 4096-ptr_max. So then it's
150 * possible for the true and false rl to overlap.
151 */
152 return 0;
153 }
154
155 if (implied_debug)
156 sm_msg("fake_history: %s vs %s. %s %s %s. --> T: %s F: %s",
157 sm->name, show_rl(rl), sm->state->name, show_special(comparison), show_rl(rl),
158 show_rl(true_rl), show_rl(false_rl));
159
160 true_sm = clone_sm(sm);
161 false_sm = clone_sm(sm);
162
163 true_sm->state = clone_partial_estate(sm->state, true_rl);
164 free_slist(&true_sm->possible);
165 add_possible_sm(true_sm, true_sm);
166 false_sm->state = clone_partial_estate(sm->state, false_rl);
167 free_slist(&false_sm->possible);
168 add_possible_sm(false_sm, false_sm);
169
170 true_stree = clone_stree(sm->pool);
171 false_stree = clone_stree(sm->pool);
793
794 return 1;
795 }
796
797 static int handled_by_extra_states(struct expression *expr,
798 struct stree **implied_true,
799 struct stree **implied_false)
800 {
801 sval_t sval;
802
803 /* If the expression is known then it has no implications. */
804 if (get_implied_value(expr, &sval))
805 return true;
806
807 if (expr->type == EXPR_COMPARE)
808 return handle_comparison(expr, implied_true, implied_false);
809 else
810 return handle_zero_comparison(expr, implied_true, implied_false);
811 }
812
813 static int handled_by_parsed_conditions(struct expression *expr,
814 struct stree **implied_true,
815 struct stree **implied_false)
816 {
817 struct state_list *true_stack = NULL;
818 struct state_list *false_stack = NULL;
819 struct stree *pre_stree;
820 struct sm_state *sm;
821
822 sm = parsed_condition_implication_hook(expr, &true_stack, &false_stack);
823 if (!sm)
824 return 0;
825
826 pre_stree = clone_stree(__get_cur_stree());
827
828 *implied_true = filter_stack(sm, pre_stree, false_stack, true_stack);
829 *implied_false = filter_stack(sm, pre_stree, true_stack, false_stack);
830
831 free_stree(&pre_stree);
832 free_slist(&true_stack);
833 free_slist(&false_stack);
834
835 return 1;
836 }
837
838 static int handled_by_stored_conditions(struct expression *expr,
839 struct stree **implied_true,
840 struct stree **implied_false)
841 {
842 struct state_list *true_stack = NULL;
843 struct state_list *false_stack = NULL;
844 struct stree *pre_stree;
845 struct sm_state *sm;
846
847 sm = stored_condition_implication_hook(expr, &true_stack, &false_stack);
848 if (!sm)
849 return 0;
850
851 pre_stree = clone_stree(__get_cur_stree());
852
853 *implied_true = filter_stack(sm, pre_stree, false_stack, true_stack);
854 *implied_false = filter_stack(sm, pre_stree, true_stack, false_stack);
855
856 free_stree(&pre_stree);
857 free_slist(&true_stack);
858 free_slist(&false_stack);
859
860 return 1;
861 }
862
863 static struct stree *saved_implied_true;
864 static struct stree *saved_implied_false;
865 static struct stree *extra_saved_implied_true;
866 static struct stree *extra_saved_implied_false;
867
868 static void separate_implication_states(struct stree **implied_true,
869 struct stree **implied_false,
870 int owner)
871 {
872 struct sm_state *sm;
873
874 /* We process these states later to preserve the implications. */
875 FOR_EACH_SM(*implied_true, sm) {
876 if (sm->owner == owner)
877 overwrite_sm_state_stree(&extra_saved_implied_true, sm);
878 } END_FOR_EACH_SM(sm);
879 FOR_EACH_SM(extra_saved_implied_true, sm) {
880 delete_state_stree(implied_true, sm->owner, sm->name, sm->sym);
881 } END_FOR_EACH_SM(sm);
882
883 FOR_EACH_SM(*implied_false, sm) {
884 if (sm->owner == owner)
885 overwrite_sm_state_stree(&extra_saved_implied_false, sm);
886 } END_FOR_EACH_SM(sm);
887 FOR_EACH_SM(extra_saved_implied_false, sm) {
888 delete_state_stree(implied_false, sm->owner, sm->name, sm->sym);
889 } END_FOR_EACH_SM(sm);
890 }
891
892 static void get_tf_states(struct expression *expr,
893 struct stree **implied_true,
894 struct stree **implied_false)
895 {
896 if (handled_by_parsed_conditions(expr, implied_true, implied_false))
897 return;
898
899 if (handled_by_comparison_hook(expr, implied_true, implied_false)) {
900 separate_implication_states(implied_true, implied_false, comparison_id);
901 return;
902 }
903
904 if (handled_by_extra_states(expr, implied_true, implied_false)) {
905 separate_implication_states(implied_true, implied_false, SMATCH_EXTRA);
906 return;
907 }
908
909 if (handled_by_stored_conditions(expr, implied_true, implied_false))
910 return;
911 }
912
913 static void save_implications_hook(struct expression *expr)
914 {
915 if (going_too_slow())
916 return;
917 get_tf_states(expr, &saved_implied_true, &saved_implied_false);
918 }
919
920 static void set_implied_states(struct expression *expr)
921 {
922 struct sm_state *sm;
923
924 if (implied_debug &&
925 (expr || saved_implied_true || saved_implied_false)) {
1155
1156 value = value_expr(sval.value);
1157 comparison = compare_expression(left, op, value);
1158
1159 if (!assume(comparison))
1160 return 0;
1161 ret = is_impossible_path();
1162 end_assume();
1163
1164 return ret;
1165 }
1166
1167 void __extra_match_condition(struct expression *expr);
1168 void __comparison_match_condition(struct expression *expr);
1169 void __stored_condition(struct expression *expr);
1170 void register_implications(int id)
1171 {
1172 add_hook(&save_implications_hook, CONDITION_HOOK);
1173 add_hook(&set_implied_states, CONDITION_HOOK);
1174 add_hook(&__extra_match_condition, CONDITION_HOOK);
1175 add_hook(&__comparison_match_condition, CONDITION_HOOK);
1176 add_hook(&set_extra_implied_states, CONDITION_HOOK);
1177 add_hook(&__stored_condition, CONDITION_HOOK);
1178 add_hook(&match_end_func, END_FUNC_HOOK);
1179 }
|