Subversion Repositories scarts

/* Scalar evolution detector.

   Copyright (C) 2003, 2004, 2005 Free Software Foundation, Inc.

   Contributed by Sebastian Pop <s.pop@laposte.net>

This file is part of GCC.

GCC is free software; you can redistribute it and/or modify it under

the terms of the GNU General Public License as published by the Free

Software Foundation; either version 2, or (at your option) any later

version.

GCC is distributed in the hope that it will be useful, but WITHOUT ANY

WARRANTY; without even the implied warranty of MERCHANTABILITY or

FITNESS FOR A PARTICULAR PURPOSE.  See the GNU General Public License

for more details.

You should have received a copy of the GNU General Public License

along with GCC; see the file COPYING.  If not, write to the Free

Software Foundation, 51 Franklin Street, Fifth Floor, Boston, MA

02110-1301, USA.  */

/*

   Description:

   This pass analyzes the evolution of scalar variables in loop

   structures.  The algorithm is based on the SSA representation,

   and on the loop hierarchy tree.  This algorithm is not based on

   the notion of versions of a variable, as it was the case for the

   previous implementations of the scalar evolution algorithm, but

   it assumes that each defined name is unique.

   The notation used in this file is called "chains of recurrences",

   and has been proposed by Eugene Zima, Robert Van Engelen, and

   others for describing induction variables in programs.  For example

   "b -> {0, +, 2}_1" means that the scalar variable "b" is equal to 0

   when entering in the loop_1 and has a step 2 in this loop, in other

   words "for (b = 0; b < N; b+=2);".  Note that the coefficients of

   this chain of recurrence (or chrec [shrek]) can contain the name of

   other variables, in which case they are called parametric chrecs.

   For example, "b -> {a, +, 2}_1" means that the initial value of "b"

   is the value of "a".  In most of the cases these parametric chrecs

   are fully instantiated before their use because symbolic names can

   hide some difficult cases such as self-references described later

   (see the Fibonacci example).

   A short sketch of the algorithm is:

   Given a scalar variable to be analyzed, follow the SSA edge to

   its definition:

   - When the definition is a MODIFY_EXPR: if the right hand side

   (RHS) of the definition cannot be statically analyzed, the answer

   of the analyzer is: "don't know".

   Otherwise, for all the variables that are not yet analyzed in the

   RHS, try to determine their evolution, and finally try to

   evaluate the operation of the RHS that gives the evolution

   function of the analyzed variable.

   - When the definition is a condition-phi-node: determine the

   evolution function for all the branches of the phi node, and

   finally merge these evolutions (see chrec_merge).

   - When the definition is a loop-phi-node: determine its initial

   condition, that is the SSA edge defined in an outer loop, and

   keep it symbolic.  Then determine the SSA edges that are defined

   in the body of the loop.  Follow the inner edges until ending on

   another loop-phi-node of the same analyzed loop.  If the reached

   loop-phi-node is not the starting loop-phi-node, then we keep

   this definition under a symbolic form.  If the reached

   loop-phi-node is the same as the starting one, then we compute a

   symbolic stride on the return path.  The result is then the

   symbolic chrec {initial_condition, +, symbolic_stride}_loop.

   Examples:

   Example 1: Illustration of the basic algorithm.

   | a = 3

   | loop_1

   |   b = phi (a, c)

   |   c = b + 1

   |   if (c > 10) exit_loop

   | endloop

   Suppose that we want to know the number of iterations of the

   loop_1.  The exit_loop is controlled by a COND_EXPR (c > 10).  We

   ask the scalar evolution analyzer two questions: what's the

   scalar evolution (scev) of "c", and what's the scev of "10".  For

   "10" the answer is "10" since it is a scalar constant.  For the

   scalar variable "c", it follows the SSA edge to its definition,

   "c = b + 1", and then asks again what's the scev of "b".

   Following the SSA edge, we end on a loop-phi-node "b = phi (a,

   c)", where the initial condition is "a", and the inner loop edge

   is "c".  The initial condition is kept under a symbolic form (it

   may be the case that the copy constant propagation has done its

   work and we end with the constant "3" as one of the edges of the

   loop-phi-node).  The update edge is followed to the end of the

   loop, and until reaching again the starting loop-phi-node: b -> c

   -> b.  At this point we have drawn a path from "b" to "b" from

   which we compute the stride in the loop: in this example it is

   "+1".  The resulting scev for "b" is "b -> {a, +, 1}_1".  Now

   that the scev for "b" is known, it is possible to compute the

   scev for "c", that is "c -> {a + 1, +, 1}_1".  In order to

   determine the number of iterations in the loop_1, we have to

   instantiate_parameters ({a + 1, +, 1}_1), that gives after some

   more analysis the scev {4, +, 1}_1, or in other words, this is

   the function "f (x) = x + 4", where x is the iteration count of

   the loop_1.  Now we have to solve the inequality "x + 4 > 10",

   and take the smallest iteration number for which the loop is

   exited: x = 7.  This loop runs from x = 0 to x = 7, and in total

   there are 8 iterations.  In terms of loop normalization, we have

   created a variable that is implicitly defined, "x" or just "_1",

   and all the other analyzed scalars of the loop are defined in

   function of this variable:

   a -> 3

   b -> {3, +, 1}_1

   c -> {4, +, 1}_1

   or in terms of a C program:

   | a = 3

   | for (x = 0; x <= 7; x++)

   |   {

   |     b = x + 3

   |     c = x + 4

   |   }

   Example 2: Illustration of the algorithm on nested loops.

   | loop_1

   |   a = phi (1, b)

   |   c = a + 2

   |   loop_2  10 times

   |     b = phi (c, d)

   |     d = b + 3

   |   endloop

   | endloop

   For analyzing the scalar evolution of "a", the algorithm follows

   the SSA edge into the loop's body: "a -> b".  "b" is an inner

   loop-phi-node, and its analysis as in Example 1, gives:

   b -> {c, +, 3}_2

   d -> {c + 3, +, 3}_2

   Following the SSA edge for the initial condition, we end on "c = a

   + 2", and then on the starting loop-phi-node "a".  From this point,

   the loop stride is computed: back on "c = a + 2" we get a "+2" in

   the loop_1, then on the loop-phi-node "b" we compute the overall

   effect of the inner loop that is "b = c + 30", and we get a "+30"

   in the loop_1.  That means that the overall stride in loop_1 is

   equal to "+32", and the result is:

   a -> {1, +, 32}_1

   c -> {3, +, 32}_1

   Example 3: Higher degree polynomials.

   | loop_1

   |   a = phi (2, b)

   |   c = phi (5, d)

   |   b = a + 1

   |   d = c + a

   | endloop

   a -> {2, +, 1}_1

   b -> {3, +, 1}_1

   c -> {5, +, a}_1

   d -> {5 + a, +, a}_1

   instantiate_parameters ({5, +, a}_1) -> {5, +, 2, +, 1}_1

   instantiate_parameters ({5 + a, +, a}_1) -> {7, +, 3, +, 1}_1

   Example 4: Lucas, Fibonacci, or mixers in general.

   | loop_1

   |   a = phi (1, b)

   |   c = phi (3, d)

   |   b = c

   |   d = c + a

   | endloop

   a -> (1, c)_1

   c -> {3, +, a}_1

   The syntax "(1, c)_1" stands for a PEELED_CHREC that has the

   following semantics: during the first iteration of the loop_1, the

   variable contains the value 1, and then it contains the value "c".

   Note that this syntax is close to the syntax of the loop-phi-node:

   "a -> (1, c)_1" vs. "a = phi (1, c)".

   The symbolic chrec representation contains all the semantics of the

   original code.  What is more difficult is to use this information.

   Example 5: Flip-flops, or exchangers.

   | loop_1

   |   a = phi (1, b)

   |   c = phi (3, d)

   |   b = c

   |   d = a

   | endloop

   a -> (1, c)_1

   c -> (3, a)_1

   Based on these symbolic chrecs, it is possible to refine this

   information into the more precise PERIODIC_CHRECs:

   a -> |1, 3|_1

   c -> |3, 1|_1

   This transformation is not yet implemented.

   Further readings:

   You can find a more detailed description of the algorithm in:

   http://icps.u-strasbg.fr/~pop/DEA_03_Pop.pdf

   http://icps.u-strasbg.fr/~pop/DEA_03_Pop.ps.gz.  But note that

   this is a preliminary report and some of the details of the

   algorithm have changed.  I'm working on a research report that

   updates the description of the algorithms to reflect the design

   choices used in this implementation.

   A set of slides show a high level overview of the algorithm and run

   an example through the scalar evolution analyzer:

   http://cri.ensmp.fr/~pop/gcc/mar04/slides.pdf

   The slides that I have presented at the GCC Summit'04 are available

   at: http://cri.ensmp.fr/~pop/gcc/20040604/gccsummit-lno-spop.pdf

*/

#include "config.h"

#include "system.h"

#include "coretypes.h"

#include "tm.h"

#include "ggc.h"

#include "tree.h"

#include "real.h"

/* These RTL headers are needed for basic-block.h.  */

#include "rtl.h"

#include "basic-block.h"

#include "diagnostic.h"

#include "tree-flow.h"

#include "tree-dump.h"

#include "timevar.h"

#include "cfgloop.h"

#include "tree-chrec.h"

#include "tree-scalar-evolution.h"

#include "tree-pass.h"

#include "flags.h"

#include "params.h"

static tree analyze_scalar_evolution_1 (struct loop *, tree, tree);

static tree resolve_mixers (struct loop *, tree);

/* The cached information about a ssa name VAR, claiming that inside LOOP,

   the value of VAR can be expressed as CHREC.  */

struct scev_info_str

{

  tree var;

  tree chrec;

};

/* Counters for the scev database.  */

static unsigned nb_set_scev = 0;

static unsigned nb_get_scev = 0;

/* The following trees are unique elements.  Thus the comparison of

   another element to these elements should be done on the pointer to

   these trees, and not on their value.  */

/* The SSA_NAMEs that are not yet analyzed are qualified with NULL_TREE.  */

tree chrec_not_analyzed_yet;

/* Reserved to the cases where the analyzer has detected an

   undecidable property at compile time.  */

tree chrec_dont_know;

/* When the analyzer has detected that a property will never

   happen, then it qualifies it with chrec_known.  */

tree chrec_known;

static bitmap already_instantiated;

static htab_t scalar_evolution_info;

/* Constructs a new SCEV_INFO_STR structure.  */

static inline struct scev_info_str *

new_scev_info_str (tree var)

{

  struct scev_info_str *res;

  res = xmalloc (sizeof (struct scev_info_str));

  res->var = var;

  res->chrec = chrec_not_analyzed_yet;

  return res;

}

/* Computes a hash function for database element ELT.  */

static hashval_t

hash_scev_info (const void *elt)

{

  return SSA_NAME_VERSION (((struct scev_info_str *) elt)->var);

}

/* Compares database elements E1 and E2.  */

static int

eq_scev_info (const void *e1, const void *e2)

{

  const struct scev_info_str *elt1 = e1;

  const struct scev_info_str *elt2 = e2;

  return elt1->var == elt2->var;

}

/* Deletes database element E.  */

static void

del_scev_info (void *e)

{

  free (e);

}

/* Get the index corresponding to VAR in the current LOOP.  If

   it's the first time we ask for this VAR, then we return

   chrec_not_analyzed_yet for this VAR and return its index.  */

static tree *

find_var_scev_info (tree var)

{

  struct scev_info_str *res;

  struct scev_info_str tmp;

  PTR *slot;

  tmp.var = var;

  slot = htab_find_slot (scalar_evolution_info, &tmp, INSERT);

  if (!*slot)

    *slot = new_scev_info_str (var);

  res = *slot;

  return &res->chrec;

}

/* Return true when CHREC contains symbolic names defined in

   LOOP_NB.  */

bool

chrec_contains_symbols_defined_in_loop (tree chrec, unsigned loop_nb)

{

  if (chrec == NULL_TREE)

    return false;

  if (TREE_INVARIANT (chrec))

    return false;

  if (TREE_CODE (chrec) == VAR_DECL

      || TREE_CODE (chrec) == PARM_DECL

      || TREE_CODE (chrec) == FUNCTION_DECL

      || TREE_CODE (chrec) == LABEL_DECL

      || TREE_CODE (chrec) == RESULT_DECL

      || TREE_CODE (chrec) == FIELD_DECL)

    return true;

  if (TREE_CODE (chrec) == SSA_NAME)

    {

      tree def = SSA_NAME_DEF_STMT (chrec);

      struct loop *def_loop = loop_containing_stmt (def);

      struct loop *loop = current_loops->parray[loop_nb];

      if (def_loop == NULL)

        return false;

      if (loop == def_loop || flow_loop_nested_p (loop, def_loop))

        return true;

      return false;

    }

  switch (TREE_CODE_LENGTH (TREE_CODE (chrec)))

    {

    case 3:

      if (chrec_contains_symbols_defined_in_loop (TREE_OPERAND (chrec, 2),

                                                  loop_nb))

        return true;

    case 2:

      if (chrec_contains_symbols_defined_in_loop (TREE_OPERAND (chrec, 1),

                                                  loop_nb))

        return true;

    case 1:

      if (chrec_contains_symbols_defined_in_loop (TREE_OPERAND (chrec, 0),

                                                  loop_nb))

        return true;

    default:

      return false;

    }

}

/* Return true when PHI is a loop-phi-node.  */

static bool

loop_phi_node_p (tree phi)

{

  /* The implementation of this function is based on the following

     property: "all the loop-phi-nodes of a loop are contained in the

     loop's header basic block".  */

  return loop_containing_stmt (phi)->header == bb_for_stmt (phi);

}

/* Compute the scalar evolution for EVOLUTION_FN after crossing LOOP.

   In general, in the case of multivariate evolutions we want to get

   the evolution in different loops.  LOOP specifies the level for

   which to get the evolution.

   Example:

   | for (j = 0; j < 100; j++)

   |   {

   |     for (k = 0; k < 100; k++)

   |       {

   |         i = k + j;   - Here the value of i is a function of j, k.

   |       }

   |      ... = i         - Here the value of i is a function of j.

   |   }

   | ... = i              - Here the value of i is a scalar.

   Example:

   | i_0 = ...

   | loop_1 10 times

   |   i_1 = phi (i_0, i_2)

   |   i_2 = i_1 + 2

   | endloop

   This loop has the same effect as:

   LOOP_1 has the same effect as:

   | i_1 = i_0 + 20

   The overall effect of the loop, "i_0 + 20" in the previous example,

   is obtained by passing in the parameters: LOOP = 1,

   EVOLUTION_FN = {i_0, +, 2}_1.

*/

static tree

compute_overall_effect_of_inner_loop (struct loop *loop, tree evolution_fn)

{

  bool val = false;

  if (evolution_fn == chrec_dont_know)

    return chrec_dont_know;

  else if (TREE_CODE (evolution_fn) == POLYNOMIAL_CHREC)

    {

      if (CHREC_VARIABLE (evolution_fn) >= (unsigned) loop->num)

        {

          struct loop *inner_loop =

            current_loops->parray[CHREC_VARIABLE (evolution_fn)];

          tree nb_iter = number_of_iterations_in_loop (inner_loop);

          if (nb_iter == chrec_dont_know)

            return chrec_dont_know;

          else

            {

              tree res;

              /* Number of iterations is off by one (the ssa name we

                 analyze must be defined before the exit).  */

              nb_iter = chrec_fold_minus (chrec_type (nb_iter),

                                nb_iter,

                                build_int_cst_type (chrec_type (nb_iter), 1));

              /* evolution_fn is the evolution function in LOOP.  Get

                 its value in the nb_iter-th iteration.  */

              res = chrec_apply (inner_loop->num, evolution_fn, nb_iter);

              /* Continue the computation until ending on a parent of LOOP.  */

              return compute_overall_effect_of_inner_loop (loop, res);

            }

        }

      else

        return evolution_fn;

     }

  /* If the evolution function is an invariant, there is nothing to do.  */

  else if (no_evolution_in_loop_p (evolution_fn, loop->num, &val) && val)

    return evolution_fn;

  else

    return chrec_dont_know;

}

/* Determine whether the CHREC is always positive/negative.  If the expression

   cannot be statically analyzed, return false, otherwise set the answer into

   VALUE.  */

bool

chrec_is_positive (tree chrec, bool *value)

{

  bool value0, value1;

  bool value2;

  tree end_value;

  tree nb_iter;

  switch (TREE_CODE (chrec))

    {

    case POLYNOMIAL_CHREC:

      if (!chrec_is_positive (CHREC_LEFT (chrec), &value0)

          || !chrec_is_positive (CHREC_RIGHT (chrec), &value1))

        return false;

      /* FIXME -- overflows.  */

      if (value0 == value1)

        {

          *value = value0;

          return true;

        }

      /* Otherwise the chrec is under the form: "{-197, +, 2}_1",

         and the proof consists in showing that the sign never

         changes during the execution of the loop, from 0 to

         loop->nb_iterations.  */

      if (!evolution_function_is_affine_p (chrec))

        return false;

      nb_iter = number_of_iterations_in_loop

        (current_loops->parray[CHREC_VARIABLE (chrec)]);

      if (chrec_contains_undetermined (nb_iter))

        return false;

      nb_iter = chrec_fold_minus

        (chrec_type (nb_iter), nb_iter,

         build_int_cst (chrec_type (nb_iter), 1));

#if 0

      /* TODO -- If the test is after the exit, we may decrease the number of

         iterations by one.  */

      if (after_exit)

        nb_iter = chrec_fold_minus

                (chrec_type (nb_iter), nb_iter,

                 build_int_cst (chrec_type (nb_iter), 1));

#endif

      end_value = chrec_apply (CHREC_VARIABLE (chrec), chrec, nb_iter);

      if (!chrec_is_positive (end_value, &value2))

        return false;

      *value = value0;

      return value0 == value1;

    case INTEGER_CST:

      *value = (tree_int_cst_sgn (chrec) == 1);

      return true;

    default:

      return false;

    }

}

/* Associate CHREC to SCALAR.  */

static void

set_scalar_evolution (tree scalar, tree chrec)

{

  tree *scalar_info;

  if (TREE_CODE (scalar) != SSA_NAME)

    return;

  scalar_info = find_var_scev_info (scalar);

  if (dump_file)

    {

      if (dump_flags & TDF_DETAILS)

        {

          fprintf (dump_file, "(set_scalar_evolution \n");

          fprintf (dump_file, "  (scalar = ");

          print_generic_expr (dump_file, scalar, 0);

          fprintf (dump_file, ")\n  (scalar_evolution = ");

          print_generic_expr (dump_file, chrec, 0);

          fprintf (dump_file, "))\n");

        }

      if (dump_flags & TDF_STATS)

        nb_set_scev++;

    }

  *scalar_info = chrec;

}

/* Retrieve the chrec associated to SCALAR in the LOOP.  */

static tree

get_scalar_evolution (tree scalar)

{

  tree res;

  if (dump_file)

    {

      if (dump_flags & TDF_DETAILS)

        {

          fprintf (dump_file, "(get_scalar_evolution \n");

          fprintf (dump_file, "  (scalar = ");

          print_generic_expr (dump_file, scalar, 0);

          fprintf (dump_file, ")\n");

        }

      if (dump_flags & TDF_STATS)

        nb_get_scev++;

    }

  switch (TREE_CODE (scalar))

    {

    case SSA_NAME:

      res = *find_var_scev_info (scalar);

      break;

    case REAL_CST:

    case INTEGER_CST:

      res = scalar;

      break;

    default:

      res = chrec_not_analyzed_yet;

      break;

    }

  if (dump_file && (dump_flags & TDF_DETAILS))

    {

      fprintf (dump_file, "  (scalar_evolution = ");

      print_generic_expr (dump_file, res, 0);

      fprintf (dump_file, "))\n");

    }

  return res;

}

/* Helper function for add_to_evolution.  Returns the evolution

   function for an assignment of the form "a = b + c", where "a" and

   "b" are on the strongly connected component.  CHREC_BEFORE is the

   information that we already have collected up to this point.

   TO_ADD is the evolution of "c".

   When CHREC_BEFORE has an evolution part in LOOP_NB, add to this

   evolution the expression TO_ADD, otherwise construct an evolution

   part for this loop.  */

static tree

add_to_evolution_1 (unsigned loop_nb,

                    tree chrec_before,

                    tree to_add)

{

  switch (TREE_CODE (chrec_before))

    {

    case POLYNOMIAL_CHREC:

      if (CHREC_VARIABLE (chrec_before) <= loop_nb)

        {

          unsigned var;

          tree left, right;

          tree type = chrec_type (chrec_before);

          /* When there is no evolution part in this loop, build it.  */

          if (CHREC_VARIABLE (chrec_before) < loop_nb)

            {

              var = loop_nb;

              left = chrec_before;

              right = SCALAR_FLOAT_TYPE_P (type)

                ? build_real (type, dconst0)

                : build_int_cst (type, 0);

            }

          else

            {

              var = CHREC_VARIABLE (chrec_before);

              left = CHREC_LEFT (chrec_before);

              right = CHREC_RIGHT (chrec_before);

            }

          return build_polynomial_chrec

            (var, left, chrec_fold_plus (type, right, to_add));

        }

      else

        /* Search the evolution in LOOP_NB.  */

        return build_polynomial_chrec

          (CHREC_VARIABLE (chrec_before),

           add_to_evolution_1 (loop_nb, CHREC_LEFT (chrec_before), to_add),

           CHREC_RIGHT (chrec_before));

    default:

      /* These nodes do not depend on a loop.  */

      if (chrec_before == chrec_dont_know)

        return chrec_dont_know;

      return build_polynomial_chrec (loop_nb, chrec_before, to_add);

    }

}

/* Add TO_ADD to the evolution part of CHREC_BEFORE in the dimension

   of LOOP_NB.

   Description (provided for completeness, for those who read code in

   a plane, and for my poor 62 bytes brain that would have forgotten

   all this in the next two or three months):

   The algorithm of translation of programs from the SSA representation

   into the chrecs syntax is based on a pattern matching.  After having

   reconstructed the overall tree expression for a loop, there are only

   two cases that can arise:

   1. a = loop-phi (init, a + expr)

   2. a = loop-phi (init, expr)

   where EXPR is either a scalar constant with respect to the analyzed

   loop (this is a degree 0 polynomial), or an expression containing

   other loop-phi definitions (these are higher degree polynomials).

   Examples:

   1.

   | init = ...

   | loop_1

   |   a = phi (init, a + 5)

   | endloop

   2.

   | inita = ...

   | initb = ...

   | loop_1

   |   a = phi (inita, 2 * b + 3)

   |   b = phi (initb, b + 1)

   | endloop

   For the first case, the semantics of the SSA representation is:

   | a (x) = init + \sum_{j = 0}^{x - 1} expr (j)

   that is, there is a loop index "x" that determines the scalar value

   of the variable during the loop execution.  During the first

   iteration, the value is that of the initial condition INIT, while

   during the subsequent iterations, it is the sum of the initial

   condition with the sum of all the values of EXPR from the initial

   iteration to the before last considered iteration.

   For the second case, the semantics of the SSA program is:

   | a (x) = init, if x = 0;

   |         expr (x - 1), otherwise.

   The second case corresponds to the PEELED_CHREC, whose syntax is

   close to the syntax of a loop-phi-node:

   | phi (init, expr)  vs.  (init, expr)_x

   The proof of the translation algorithm for the first case is a

   proof by structural induction based on the degree of EXPR.

   Degree 0:

   When EXPR is a constant with respect to the analyzed loop, or in

   other words when EXPR is a polynomial of degree 0, the evolution of

   the variable A in the loop is an affine function with an initial

   condition INIT, and a step EXPR.  In order to show this, we start

   from the semantics of the SSA representation:

   f (x) = init + \sum_{j = 0}^{x - 1} expr (j)

   and since "expr (j)" is a constant with respect to "j",

   f (x) = init + x * expr

   Finally, based on the semantics of the pure sum chrecs, by

   identification we get the corresponding chrecs syntax:

   f (x) = init * \binom{x}{0} + expr * \binom{x}{1}

   f (x) -> {init, +, expr}_x

   Higher degree:

   Suppose that EXPR is a polynomial of degree N with respect to the

   analyzed loop_x for which we have already determined that it is

   written under the chrecs syntax:

   | expr (x)  ->  {b_0, +, b_1, +, ..., +, b_{n-1}} (x)

   We start from the semantics of the SSA program:

   | f (x) = init + \sum_{j = 0}^{x - 1} expr (j)

   |

   | f (x) = init + \sum_{j = 0}^{x - 1}

   |                (b_0 * \binom{j}{0} + ... + b_{n-1} * \binom{j}{n-1})

   |

   | f (x) = init + \sum_{j = 0}^{x - 1}

   |                \sum_{k = 0}^{n - 1} (b_k * \binom{j}{k})

   |

   | f (x) = init + \sum_{k = 0}^{n - 1}

   |                (b_k * \sum_{j = 0}^{x - 1} \binom{j}{k})