From eb339de72a530275bb9d427fa6d09234c87b4c02 Mon Sep 17 00:00:00 2001 From: David Malcolm Date: Thu, 11 Jun 2020 08:19:24 -0400 Subject: [PATCH 226/315] FIXME: WIP on widening --- gcc/analyzer/constraint-manager2.cc | 22 +++++- gcc/analyzer/region-model2.cc | 117 +++++++++++++++++++++++++++- gcc/analyzer/region-model2.h | 4 + 3 files changed, 137 insertions(+), 6 deletions(-) diff --git a/gcc/analyzer/constraint-manager2.cc b/gcc/analyzer/constraint-manager2.cc index a8779f35e71..d6708c191ba 100644 --- a/gcc/analyzer/constraint-manager2.cc +++ b/gcc/analyzer/constraint-manager2.cc @@ -919,7 +919,8 @@ constraint_manager2::add_constraint_internal (equiv_class2_id lhs_id, } /* Look for SVAL within the equivalence classes of this constraint_manager2; - if found, write the id to *OUT and return true, otherwise return false. */ + if found, return true, writing the id to *OUT if OUT is non-NULL, + otherwise return false. */ bool constraint_manager2::get_equiv_class2_by_svalue2 (const svalue2 *sval, @@ -935,7 +936,8 @@ constraint_manager2::get_equiv_class2_by_svalue2 (const svalue2 *sval, FOR_EACH_VEC_ELT (ec->m_vars, j, iv) if (iv == sval) { - *out = equiv_class2_id (i); + if (out) + *out = equiv_class2_id (i); return true; } } @@ -1362,6 +1364,19 @@ public: void on_fact (const svalue2 *lhs, enum tree_code code, const svalue2 *rhs) FINAL OVERRIDE { + /* Special-case for widening. */ + /* FIXME: should only do this if LHS isn't mentioned anywhere in + m_cm_b's model, rather than just in m_cb_b? */ + if (lhs->get_kind () == svalue2::SK_WIDENING) + if (!m_cm_b->get_equiv_class2_by_svalue2 (lhs, NULL)) + { + /* LHS isn't constrained within m_cm_b. */ + /* FIXME: for now, treat it as "unmentioned". */ + bool sat = m_out->add_constraint (lhs, code, rhs); + gcc_assert (sat); + return; + } + if (m_cm_b->eval_condition (lhs, code, rhs).is_true ()) { bool sat = m_out->add_constraint (lhs, code, rhs); @@ -1397,6 +1412,9 @@ constraint_manager2::merge (const constraint_manager2 &cm_a, and add those to *OUT. */ merger2_fact_visitor v (©_cm_b, out); copy_cm_a.for_each_fact (&v); + + /* FIXME and the other way around, since things could be implicit in one + and explicit in the other? */ } /* A subroutine of constraint_manager2::merge. diff --git a/gcc/analyzer/region-model2.cc b/gcc/analyzer/region-model2.cc index 75189c7be2e..3882334d7de 100644 --- a/gcc/analyzer/region-model2.cc +++ b/gcc/analyzer/region-model2.cc @@ -261,8 +261,6 @@ svalue2::can_merge_p (const svalue2 *other, if (tree cst0 = maybe_get_constant ()) if (tree cst1 = other->maybe_get_constant ()) { - /* FIXME: we also need to distinguish these via the stmt (or - program_point?) so we can handle nested loops. */ return mgr->get_or_create_widening_svalue2 (other->get_type (), point, other, this); } @@ -785,8 +783,9 @@ widening_svalue2::dump_to_pp (pretty_printer *pp, bool simple) const if (simple) { pp_string (pp, "WIDENING("); + pp_character (pp, '{'); m_point.print (pp, format (false)); - pp_string (pp, ", "); + pp_string (pp, "}, "); m_base_sval->dump_to_pp (pp, simple); pp_string (pp, ", "); m_iter_sval->dump_to_pp (pp, simple); @@ -797,8 +796,9 @@ widening_svalue2::dump_to_pp (pretty_printer *pp, bool simple) const pp_string (pp, "widening_svalue2 ("); // TODO: type? pp_string (pp, ", "); + pp_character (pp, '{'); m_point.print (pp, format (false)); - pp_string (pp, ", "); + pp_string (pp, "}, "); m_base_sval->dump_to_pp (pp, simple); pp_string (pp, ", "); m_iter_sval->dump_to_pp (pp, simple); @@ -9605,7 +9605,12 @@ test_state_merging () assert_region_model2s_merge (x, int_42, int_113, &merged, &merged_x_sval); /* In particular, there should be an unknown value for "x". */ + // FIXME +#if WIDENING + ASSERT_EQ (merged_x_sval->get_kind (), svalue2::SK_WIDENING); +#else ASSERT_EQ (merged_x_sval->get_kind (), svalue2::SK_UNKNOWN); +#endif } /* Uninit and constant. */ @@ -9884,6 +9889,108 @@ test_constraint_merging () tristate (tristate::TS_UNKNOWN)); } +/* Verify merging constraints for states simulating successive iterations + of a loop. + Simulate: + for (i = 0; i < 256; i++) + [...body...] + i.e. this gimple:. + i_15 = 0; + goto ; + + : + i_11 = PHI + if (i_11 <= 255) + goto ; + else + goto [AFTER LOOP] + + : + [LOOP BODY] + i_23 = i_11 + 1; + + and thus these ops (and resultant states): + i_11 = PHI() + {i_11: 0} + add_constraint (i_11 <= 255) [for the true edge] + {i_11: 0} [constraint was a no-op] + i_23 = i_11 + 1; + {i_22: 1} + i_11 = PHI() + {i_11: WIDENED (at phi, 0, 1)} + add_constraint (i_11 <= 255) [for the true edge] + {i_11: WIDENED (at phi, 0, 1); WIDENED <= 255} + i_23 = i_11 + 1; + {i_23: (WIDENED (at phi, 0, 1) + 1); WIDENED <= 255} + i_11 = PHI() + {i_11: WIDENED (at phi, 0, 1); WIDENED <= 256} + [changing meaning of "WIDENED" here] + if (i_11 <= 255) + T: {i_11: WIDENED (at phi, 0, 1); WIDENED <= 255}; cache hit + F: {i_11: 256} + + FIXME. + TODO: rename? + */ + +static void +test_iteration_1 () +{ +#if WIDENING + program_point point (program_point::origin ()); + + tree int_0 = build_int_cst (integer_type_node, 0); + tree int_1 = build_int_cst (integer_type_node, 1); + tree int_256 = build_int_cst (integer_type_node, 256); + tree i = build_global_decl ("i", integer_type_node); + + region_model2_manager mgr; + test_region_model2_context ctxt; + + /* model0: i: 0. */ + region_model2 model0 (&mgr); + model0.set_value (i, int_0, &ctxt); + + /* model1: i: 1. */ + region_model2 model1 (&mgr); + model1.set_value (i, int_1, &ctxt); + + /* FIXME: should merge to a widened value. */ + region_model2 model2 (&mgr); + ASSERT_TRUE (model1.can_merge_with_p (model0, point, &model2)); + const svalue2 *merged_i = model2.get_rvalue (i, &ctxt); + ASSERT_EQ (merged_i->get_kind (), svalue2::SK_WIDENING); + /* Add constraint: i < 256 */ + model2.add_constraint (i, LT_EXPR, int_256, &ctxt); + ASSERT_EQ (model2.eval_condition (i, LT_EXPR, int_256, &ctxt), + tristate (tristate::TS_TRUE)); + + /* Try merging with the initial state. */ + region_model2 model3 (&mgr); + ASSERT_TRUE (model2.can_merge_with_p (model0, point, &model3)); + /* Merging the merged value with the initial value should be idempotent, + so that the analysis converges. */ + ASSERT_EQ (model3.get_rvalue (i, &ctxt), merged_i); + /* Merger of 0 and a widening value with constraint < CST + should retain the constraint, even though it was implicit + for the 0 case. */ + ASSERT_EQ (model3.eval_condition (i, LT_EXPR, int_256, &ctxt), + tristate (tristate::TS_TRUE)); + /* ...and we should have equality: the analysis should have converged. */ + ASSERT_EQ (model3, model2); + + // TODO +#endif +} + +// TODO: as above, but with comparison against "n", rather than a constant + +static void +test_iteration_2 () +{ + // TODO +} + #if 0 /* Verify that if we mark a pointer to a malloc-ed region2 as non-NULL, @@ -10245,6 +10352,8 @@ analyzer_region_model2_cc_tests () #endif test_state_merging (); test_constraint_merging (); + test_iteration_1 (); + test_iteration_2 (); #if 0 test_malloc_constraints (); #endif diff --git a/gcc/analyzer/region-model2.h b/gcc/analyzer/region-model2.h index 43ffe6e78b0..10c7d646db2 100644 --- a/gcc/analyzer/region-model2.h +++ b/gcc/analyzer/region-model2.h @@ -892,6 +892,10 @@ namespace ana { representing a possible fixed point in an iteration from the base to +ve infinity, or -ve infinity, and thus useful for representing a value within a loop. + We also need to capture the program_point at which the merger happens, + so that distinguish between different iterators, and thus handle + nested loops. + FIXME: firm this up; clarify the above. */ class widening_svalue2 : public svalue2 -- 2.26.2