isl_tab_basic_map_partial_lexopt: disable use of shifted tableau on equalities

If the input context already involves equalities then the shfited tableau
is not used as it would be empty.  However, if equalities are added at
a later stage (e.g., transferred for the input map), then we would fail
to disable the use of the shifted tableau, possibly resulting in invalid
sample values being computing from this shifted tableau.

Reported-by: Tobias Grosser <tobias@grosser.es>
Signed-off-by: Sven Verdoolaege <skimo@kotnet.org>

diff --git a/isl_tab_pip.c b/isl_tab_pip.c
index 16bae5a..d5ed654 100644 (file)
--- a/isl_tab_pip.c
+++ b/isl_tab_pip.c
@@ -2610,6 +2610,14 @@ error:
        return NULL;
 }
 
+/* Representation of the context when using generalized basis reduction.
+ *
+ * "shifted" contains the offsets of the unit hypercubes that lie inside the
+ * context.  Any rational point in "shifted" can therefore be rounded
+ * up to an integer point in the context.
+ * If the context is constrained by any equality, then "shifted" is not used
+ * as it would be empty.
+ */
 struct isl_context_gbr {
        struct isl_context context;
        struct isl_tab *tab;
@@ -2833,6 +2841,15 @@ error:
        return NULL;
 }
 
+/* Add the equality described by "eq" to the context.
+ * If "check" is set, then we check if the context is empty after
+ * adding the equality.
+ * If "update" is set, then we check if the samples are still valid.
+ *
+ * We do not explicitly add shifted copies of the equality to
+ * cgbr->shifted since they would conflict with each other.
+ * Instead, we directly mark cgbr->shifted empty.
+ */
 static void context_gbr_add_eq(struct isl_context *context, isl_int *eq,
                int check, int update)
 {
@@ -2840,6 +2857,11 @@ static void context_gbr_add_eq(struct isl_context *context, isl_int *eq,
 
        cgbr->tab = add_gbr_eq(cgbr->tab, eq);
 
+       if (cgbr->shifted && !cgbr->shifted->empty && use_shifted(cgbr)) {
+               if (isl_tab_mark_empty(cgbr->shifted) < 0)
+                       goto error;
+       }
+
        if (cgbr->cone && cgbr->cone->n_col != cgbr->cone->n_dead) {
                if (isl_tab_extend_cons(cgbr->cone, 2) < 0)
                        goto error;

diff --git a/isl_test.c b/isl_test.c
index 745c4ed..9bd3b58 100644 (file)
--- a/isl_test.c
+++ b/isl_test.c
@@ -3867,10 +3867,36 @@ static int test_simplify(isl_ctx *ctx)
        return 0;
 }
 
+/* This is a regression test for a bug where isl_tab_basic_map_partial_lexopt
+ * with gbr context would fail to disable the use of the shifted tableau
+ * when transferring equalities for the input to the context, resulting
+ * in invalid sample values.
+ */
+static int test_partial_lexmin(isl_ctx *ctx)
+{
+       const char *str;
+       isl_basic_set *bset;
+       isl_basic_map *bmap;
+       isl_map *map;
+
+       str = "{ [1, b, c, 1 - c] -> [e] : 2e <= -c and 2e >= -3 + c }";
+       bmap = isl_basic_map_read_from_str(ctx, str);
+       str = "{ [a, b, c, d] : c <= 1 and 2d >= 6 - 4b - c }";
+       bset = isl_basic_set_read_from_str(ctx, str);
+       map = isl_basic_map_partial_lexmin(bmap, bset, NULL);
+       isl_map_free(map);
+
+       if (!map)
+               return -1;
+
+       return 0;
+}
+
 struct {
        const char *name;
        int (*fn)(isl_ctx *ctx);
 } tests [] = {
+       { "partial lexmin", &test_partial_lexmin },
        { "simplify", &test_simplify },
        { "curry", &test_curry },
        { "piecewise multi affine expressions", &test_pw_multi_aff },