From f88f3c71812cee94301243079ad3a42db9180671 Mon Sep 17 00:00:00 2001 From: David Malcolm Date: Mon, 15 Jun 2020 11:57:22 -0400 Subject: [PATCH 229/315] FIXME: more on widening_svalue2::eval_condition_without_cm --- gcc/analyzer/region-model2.cc | 129 +++++++++++++++++++++++++++++++--- 1 file changed, 120 insertions(+), 9 deletions(-) diff --git a/gcc/analyzer/region-model2.cc b/gcc/analyzer/region-model2.cc index 621fced83b8..0a622b4a881 100644 --- a/gcc/analyzer/region-model2.cc +++ b/gcc/analyzer/region-model2.cc @@ -864,32 +864,61 @@ widening_svalue2::eval_condition_without_cm (enum tree_code op, /* LHS is in [base_cst, +ve infinity), assuming no overflow. */ switch (op) { + case LE_EXPR: case LT_EXPR: { - /* [BASE, +INF) < RHS: - This is false at +ve ininity. It can be true for points - X where X < RHS, so we have either "false", or "unknown". */ - tree base_lt_rhs = fold_binary (op, boolean_type_node, + /* [BASE, +INF) OP RHS: + This is either true or false at +ve ininity, + It can be true for points X where X OP RHS, so we have either + "false", or "unknown". */ + tree base_op_rhs = fold_binary (op, boolean_type_node, base_cst, rhs_cst); - if (base_lt_rhs == boolean_true_node) + if (base_op_rhs == boolean_true_node) return tristate::TS_UNKNOWN; else return tristate::TS_FALSE; } case GE_EXPR: + case GT_EXPR: { - /* [BASE, +INF) >= RHS: + /* [BASE, +INF) OP RHS: This is true at +ve infinity. It will be true everywhere in the range if BASE >= RHS. */ - tree base_ge_rhs = fold_binary (op, boolean_type_node, + tree base_op_rhs = fold_binary (op, boolean_type_node, base_cst, rhs_cst); - if (base_ge_rhs == boolean_true_node) + if (base_op_rhs == boolean_true_node) return tristate::TS_TRUE; else return tristate::TS_UNKNOWN; } + case EQ_EXPR: + { + /* [BASE, +INF) == RHS: + Could this be true at any point in the range? If so we + have "unknown", otherwise we have "false". */ + tree base_le_rhs = fold_binary (LE_EXPR, boolean_type_node, + base_cst, rhs_cst); + if (base_le_rhs == boolean_true_node) + return tristate::TS_UNKNOWN; + else + return tristate::TS_FALSE; + } + + case NE_EXPR: + { + /* [BASE, +INF) != RHS: + Could we have equality at any point in the range? If so we + have "unknown", otherwise we have "true". */ + tree base_le_rhs = fold_binary (LE_EXPR, boolean_type_node, + base_cst, rhs_cst); + if (base_le_rhs == boolean_true_node) + return tristate::TS_UNKNOWN; + else + return tristate::TS_TRUE; + } + default: return tristate::TS_UNKNOWN; } @@ -10024,6 +10053,84 @@ test_constraint_merging () tristate (tristate::TS_UNKNOWN)); } +/* FIXME. */ + +static void +test_widening_constraints () +{ + program_point point (program_point::origin ()); + tree int_0 = build_int_cst (integer_type_node, 0); + tree int_m1 = build_int_cst (integer_type_node, -1); + tree int_1 = build_int_cst (integer_type_node, 1); + tree int_256 = build_int_cst (integer_type_node, 256); + region_model2_manager mgr; + test_region_model2_context ctxt; + const svalue2 *int_0_sval = mgr.get_or_create_constant_svalue2 (int_0); + const svalue2 *int_1_sval = mgr.get_or_create_constant_svalue2 (int_1); + const svalue2 *w_zero_then_one_sval + = mgr.get_or_create_widening_svalue2 (integer_type_node, point, + int_0_sval, int_1_sval); + const widening_svalue2 *w_zero_then_one + = w_zero_then_one_sval->dyn_cast_widening_svalue2 (); + ASSERT_EQ (w_zero_then_one->get_direction (), + widening_svalue2::DIR_ASCENDING); + ASSERT_EQ (w_zero_then_one->eval_condition_without_cm (LT_EXPR, int_m1), + tristate::TS_FALSE); + ASSERT_EQ (w_zero_then_one->eval_condition_without_cm (LT_EXPR, int_0), + tristate::TS_FALSE); + ASSERT_EQ (w_zero_then_one->eval_condition_without_cm (LT_EXPR, int_1), + tristate::TS_UNKNOWN); + ASSERT_EQ (w_zero_then_one->eval_condition_without_cm (LT_EXPR, int_256), + tristate::TS_UNKNOWN); + + ASSERT_EQ (w_zero_then_one->eval_condition_without_cm (LE_EXPR, int_m1), + tristate::TS_FALSE); + ASSERT_EQ (w_zero_then_one->eval_condition_without_cm (LE_EXPR, int_0), + tristate::TS_UNKNOWN); + ASSERT_EQ (w_zero_then_one->eval_condition_without_cm (LE_EXPR, int_1), + tristate::TS_UNKNOWN); + ASSERT_EQ (w_zero_then_one->eval_condition_without_cm (LE_EXPR, int_256), + tristate::TS_UNKNOWN); + + ASSERT_EQ (w_zero_then_one->eval_condition_without_cm (GT_EXPR, int_m1), + tristate::TS_TRUE); + ASSERT_EQ (w_zero_then_one->eval_condition_without_cm (GT_EXPR, int_0), + tristate::TS_UNKNOWN); + ASSERT_EQ (w_zero_then_one->eval_condition_without_cm (GT_EXPR, int_1), + tristate::TS_UNKNOWN); + ASSERT_EQ (w_zero_then_one->eval_condition_without_cm (GT_EXPR, int_256), + tristate::TS_UNKNOWN); + + ASSERT_EQ (w_zero_then_one->eval_condition_without_cm (GE_EXPR, int_m1), + tristate::TS_TRUE); + ASSERT_EQ (w_zero_then_one->eval_condition_without_cm (GE_EXPR, int_0), + tristate::TS_TRUE); + ASSERT_EQ (w_zero_then_one->eval_condition_without_cm (GE_EXPR, int_1), + tristate::TS_UNKNOWN); + ASSERT_EQ (w_zero_then_one->eval_condition_without_cm (GE_EXPR, int_256), + tristate::TS_UNKNOWN); + + ASSERT_EQ (w_zero_then_one->eval_condition_without_cm (EQ_EXPR, int_m1), + tristate::TS_FALSE); + ASSERT_EQ (w_zero_then_one->eval_condition_without_cm (EQ_EXPR, int_0), + tristate::TS_UNKNOWN); + ASSERT_EQ (w_zero_then_one->eval_condition_without_cm (EQ_EXPR, int_1), + tristate::TS_UNKNOWN); + ASSERT_EQ (w_zero_then_one->eval_condition_without_cm (EQ_EXPR, int_256), + tristate::TS_UNKNOWN); + + ASSERT_EQ (w_zero_then_one->eval_condition_without_cm (NE_EXPR, int_m1), + tristate::TS_TRUE); + ASSERT_EQ (w_zero_then_one->eval_condition_without_cm (NE_EXPR, int_0), + tristate::TS_UNKNOWN); + ASSERT_EQ (w_zero_then_one->eval_condition_without_cm (NE_EXPR, int_1), + tristate::TS_UNKNOWN); + ASSERT_EQ (w_zero_then_one->eval_condition_without_cm (NE_EXPR, int_256), + tristate::TS_UNKNOWN); + + // TODO: a descending value +} + /* Verify merging constraints for states simulating successive iterations of a loop. Simulate: @@ -10143,8 +10250,11 @@ test_iteration_1 () ASSERT_TRUE (model5.can_merge_with_p (model2, point, &model6)); const svalue2 *merged_widening = model6.get_rvalue (i, &ctxt); ASSERT_EQ (merged_widening->get_kind (), svalue2::SK_WIDENING); + // FIXME: what constraints should we have here? - // TODO + // TODO: constraints at end of loop (with i >= 256; should get i == 256) + /* TODO: unittests for widening_svalue2::eval_condition_without_cm + (separately). */ #endif } @@ -10517,6 +10627,7 @@ analyzer_region_model2_cc_tests () #endif test_state_merging (); test_constraint_merging (); + test_widening_constraints (); test_iteration_1 (); test_iteration_2 (); #if 0 -- 2.26.2