eqv_cmp.c

   1 #include <assert.h>
   2 #include <stdio.h>
   3 #include <yaml.h>
   4 #include <isl/arg.h>
   5 #include <isl/union_set.h>
   6
   7 struct options {
   8         char *eqv1;
   9         char *eqv2;
  10 };
  11
  12 ISL_ARGS_START(struct options, options_args)
  13 ISL_ARG_ARG(struct options, eqv1, "eqv1", NULL)
  14 ISL_ARG_ARG(struct options, eqv2, "eqv2", NULL)
  15 ISL_ARGS_END
  16
  17 ISL_ARG_DEF(options, struct options, options_args)
  18
  19 struct eqv {
  20         isl_union_set *only1;
  21         isl_union_set *only2;
  22         isl_union_set *proved;
  23         isl_union_set *not_proved;
  24 };
  25
  26 static void *eqv_free(struct eqv *eqv)
  27 {
  28         if (!eqv)
  29                 return NULL;
  30
  31         isl_union_set_free(eqv->only1);
  32         isl_union_set_free(eqv->only2);
  33         isl_union_set_free(eqv->proved);
  34         isl_union_set_free(eqv->not_proved);
  35
  36         free(eqv);
  37         return NULL;
  38 }
  39
  40 static __isl_give isl_union_set *extract_set(isl_ctx *ctx,
  41         yaml_document_t *document, yaml_node_t *node)
  42 {
  43         if (node->type != YAML_SCALAR_NODE)
  44                 isl_die(ctx, isl_error_invalid, "expecting scalar node",
  45                         return NULL);
  46
  47         return isl_union_set_read_from_str(ctx,
  48                                             (char *) node->data.scalar.value);
  49 }
  50
  51 static struct eqv *extract_eqv(isl_ctx *ctx, yaml_document_t *document,
  52         yaml_node_t *node)
  53 {
  54         struct eqv *eqv;
  55         yaml_node_pair_t * pair;
  56
  57         if (!node)
  58                 return NULL;
  59
  60         if (node->type != YAML_MAPPING_NODE)
  61                 isl_die(ctx, isl_error_invalid, "expecting mapping",
  62                         return NULL);
  63
  64         eqv = isl_calloc_type(ctx, struct eqv);
  65         if (!eqv)
  66                 return NULL;
  67
  68         for (pair = node->data.mapping.pairs.start;
  69              pair < node->data.mapping.pairs.top; ++pair) {
  70                 yaml_node_t *key, *value;
  71
  72                 key = yaml_document_get_node(document, pair->key);
  73                 value = yaml_document_get_node(document, pair->value);
  74
  75                 if (key->type != YAML_SCALAR_NODE)
  76                         isl_die(ctx, isl_error_invalid, "expecting scalar key",
  77                                 return eqv_free(eqv));
  78                 if (!strcmp((char *) key->data.scalar.value,
  79                                 "Equivalence proved"))
  80                         eqv->proved = extract_set(ctx, document, value);
  81                 if (!strcmp((char *) key->data.scalar.value,
  82                                 "Equivalence NOT proved"))
  83                         eqv->not_proved = extract_set(ctx, document, value);
  84                 if (!strcmp((char *) key->data.scalar.value,
  85                                 "Only in program 1"))
  86                         eqv->only1 = extract_set(ctx, document, value);
  87                 if (!strcmp((char *) key->data.scalar.value,
  88                                 "Only in program 2"))
  89                         eqv->only2 = extract_set(ctx, document, value);
  90         }
  91
  92         return eqv;
  93 }
  94
  95 static struct eqv *eqv_parse(isl_ctx *ctx, FILE *in)
  96 {
  97         struct eqv *eqv = NULL;
  98         yaml_parser_t parser;
  99         yaml_node_t *root;
 100         yaml_document_t document = { 0 };
 101
 102         yaml_parser_initialize(&parser);
 103
 104         yaml_parser_set_input_file(&parser, in);
 105
 106         if (!yaml_parser_load(&parser, &document))
 107                 goto error;
 108
 109         root = yaml_document_get_root_node(&document);
 110
 111         eqv = extract_eqv(ctx, &document, root);
 112
 113         yaml_document_delete(&document);
 114
 115         yaml_parser_delete(&parser);
 116
 117         return eqv;
 118 error:
 119         yaml_parser_delete(&parser);
 120         eqv_free(eqv);
 121         return NULL;
 122 }
 123
 124 static int eqv_is_equal(struct eqv *eqv1, struct eqv *eqv2)
 125 {
 126         if (!eqv1 || !eqv2)
 127                 return 0;
 128
 129         if (!eqv1->only1 != !eqv2->only1)
 130                 return 0;
 131         if (!isl_union_set_is_equal(eqv1->only1, eqv2->only1)) {
 132                 isl_union_set_dump(eqv1->only1);
 133                 isl_union_set_dump(eqv2->only1);
 134                 return 0;
 135         }
 136
 137         if (!eqv1->only2 != !eqv2->only2)
 138                 return 0;
 139         if (!isl_union_set_is_equal(eqv1->only2, eqv2->only2)) {
 140                 isl_union_set_dump(eqv1->only2);
 141                 isl_union_set_dump(eqv2->only2);
 142                 return 0;
 143         }
 144
 145         if (!eqv1->proved != !eqv2->proved)
 146                 return 0;
 147         if (!isl_union_set_is_equal(eqv1->proved, eqv2->proved)) {
 148                 isl_union_set_dump(eqv1->proved);
 149                 isl_union_set_dump(eqv2->proved);
 150                 return 0;
 151         }
 152
 153         if (!eqv1->not_proved != !eqv2->not_proved)
 154                 return 0;
 155         if (!isl_union_set_is_equal(eqv1->not_proved, eqv2->not_proved)) {
 156                 isl_union_set_dump(eqv1->not_proved);
 157                 isl_union_set_dump(eqv2->not_proved);
 158                 return 0;
 159         }
 160
 161         return 1;
 162 }
 163
 164 int main(int argc, char **argv)
 165 {
 166         isl_ctx *ctx;
 167         struct options *options;
 168         struct eqv *eqv1, *eqv2;
 169         FILE *file1, *file2;
 170         int equal;
 171
 172         options = options_new_with_defaults();
 173         assert(options);
 174         argc = options_parse(options, argc, argv, ISL_ARG_ALL);
 175         ctx = isl_ctx_alloc_with_options(&options_args, options);
 176
 177         file1 = fopen(options->eqv1, "r");
 178         assert(file1);
 179         file2 = fopen(options->eqv2, "r");
 180         assert(file2);
 181
 182         eqv1 = eqv_parse(ctx, file1);
 183         eqv2 = eqv_parse(ctx, file2);
 184
 185         equal = eqv_is_equal(eqv1, eqv2);
 186
 187         eqv_free(eqv1);
 188         eqv_free(eqv2);
 189
 190         fclose(file2);
 191         fclose(file1);
 192         isl_ctx_free(ctx);
 193
 194         return equal ? 0 : 1;
 195 }