scheck.c

   1 // SPDX-License-Identifier: MIT
   2 // Copyright (C) 2021 Luc Van Oostenryck
   3
   4 ///
   5 // Symbolic checker for Sparse's IR
   6 // --------------------------------
   7 //
   8 // This is an example client program with a dual purpose:
   9 //      # It shows how to translate Sparse's IR into the language
  10 //        of SMT solvers (only the part concerning integers,
  11 //        floating-point and memory is ignored).
  12 //      # It's used as a simple symbolic checker for the IR.
  13 //        The idea is to create a mini-language that allows to
  14 //        express some assertions with some pre-conditions.
  15
  16 #include <stdarg.h>
  17 #include <stdlib.h>
  18 #include <stdio.h>
  19 #include <string.h>
  20 #include <ctype.h>
  21 #include <unistd.h>
  22 #include <fcntl.h>
  23
  24 #include <boolector.h>
  25 #include "lib.h"
  26 #include "expression.h"
  27 #include "linearize.h"
  28 #include "symbol.h"
  29 #include "builtin.h"
  30
  31
  32 #define dyntype incomplete_ctype
  33 static const struct builtin_fn builtins_scheck[] = {
  34         { "__assume", &void_ctype, 0, { &dyntype }, .op = &generic_int_op },
  35         { "__assert", &void_ctype, 0, { &bool_ctype }, .op = &generic_int_op },
  36         { "__assert_eq", &void_ctype, 0, { &dyntype, &dyntype }, .op = &generic_int_op },
  37         { "__assert_const", &void_ctype, 0, { &dyntype, &dyntype }, .op = &generic_int_op },
  38         {}
  39 };
  40
  41
  42 static BoolectorSort get_sort(Btor *btor, struct symbol *type, struct position pos)
  43 {
  44         if (!is_int_type(type)) {
  45                 sparse_error(pos, "invalid type");
  46                 return NULL;
  47         }
  48         return boolector_bitvec_sort(btor, type->bit_size);
  49 }
  50
  51 static BoolectorNode *mkvar(Btor *btor, BoolectorSort s, pseudo_t pseudo)
  52 {
  53         static char buff[33];
  54         BoolectorNode *n;
  55
  56         if (pseudo->priv)
  57                 return pseudo->priv;
  58
  59         switch (pseudo->type) {
  60         case PSEUDO_VAL:
  61                 sprintf(buff, "%llx", pseudo->value);
  62                 return boolector_consth(btor, s, buff);
  63         case PSEUDO_ARG:
  64         case PSEUDO_REG:
  65                 n = boolector_var(btor, s, show_pseudo(pseudo));
  66                 break;
  67         default:
  68                 fprintf(stderr, "invalid pseudo: %s\n", show_pseudo(pseudo));
  69                 return NULL;
  70         }
  71         return pseudo->priv = n;
  72 }
  73
  74 static BoolectorNode *get_arg(Btor *btor, struct instruction *insn, int idx)
  75 {
  76         pseudo_t arg = ptr_list_nth(insn->arguments, idx);
  77         struct symbol *type = ptr_list_nth(insn->fntypes, idx + 1);
  78         BoolectorSort s = get_sort(btor, type, insn->pos);
  79
  80         return mkvar(btor, s, arg);
  81 }
  82
  83 static BoolectorNode *zext(Btor *btor, struct instruction *insn, BoolectorNode *s)
  84 {
  85         int old = boolector_get_width(btor, s);
  86         int new = insn->type->bit_size;
  87         return boolector_uext(btor, s, new - old);
  88 }
  89
  90 static BoolectorNode *sext(Btor *btor, struct instruction *insn, BoolectorNode *s)
  91 {
  92         int old = boolector_get_width(btor, s);
  93         int new = insn->type->bit_size;
  94         return boolector_sext(btor, s, new - old);
  95 }
  96
  97 static BoolectorNode *slice(Btor *btor, struct instruction *insn, BoolectorNode *s)
  98 {
  99         int old = boolector_get_width(btor, s);
 100         int new = insn->type->bit_size;
 101         return boolector_slice(btor, s, old - new - 1, 0);
 102 }
 103
 104 static void binary(Btor *btor, BoolectorSort s, struct instruction *insn)
 105 {
 106         BoolectorNode *t, *a, *b;
 107
 108         a = mkvar(btor, s, insn->src1);
 109         b = mkvar(btor, s, insn->src2);
 110         if (!a || !b)
 111                 return;
 112         switch (insn->opcode) {
 113         case OP_ADD:    t = boolector_add(btor, a, b); break;
 114         case OP_SUB:    t = boolector_sub(btor, a, b); break;
 115         case OP_MUL:    t = boolector_mul(btor, a, b); break;
 116         case OP_AND:    t = boolector_and(btor, a, b); break;
 117         case OP_OR:     t = boolector_or (btor, a, b); break;
 118         case OP_XOR:    t = boolector_xor(btor, a, b); break;
 119         case OP_SHL:    t = boolector_sll(btor, a, b); break;
 120         case OP_LSR:    t = boolector_srl(btor, a, b); break;
 121         case OP_ASR:    t = boolector_sra(btor, a, b); break;
 122         case OP_DIVS:   t = boolector_sdiv(btor, a, b); break;
 123         case OP_DIVU:   t = boolector_udiv(btor, a, b); break;
 124         case OP_MODS:   t = boolector_srem(btor, a, b); break;
 125         case OP_MODU:   t = boolector_urem(btor, a, b); break;
 126         case OP_SET_EQ: t = zext(btor, insn, boolector_eq(btor, a, b)); break;
 127         case OP_SET_NE: t = zext(btor, insn, boolector_ne(btor, a, b)); break;
 128         case OP_SET_LT: t = zext(btor, insn, boolector_slt(btor, a, b)); break;
 129         case OP_SET_LE: t = zext(btor, insn, boolector_slte(btor, a, b)); break;
 130         case OP_SET_GE: t = zext(btor, insn, boolector_sgte(btor, a, b)); break;
 131         case OP_SET_GT: t = zext(btor, insn, boolector_sgt(btor, a, b)); break;
 132         case OP_SET_B:  t = zext(btor, insn, boolector_ult(btor, a, b)); break;
 133         case OP_SET_BE: t = zext(btor, insn, boolector_ulte(btor, a, b)); break;
 134         case OP_SET_AE: t = zext(btor, insn, boolector_ugte(btor, a, b)); break;
 135         case OP_SET_A:  t = zext(btor, insn, boolector_ugt(btor, a, b)); break;
 136         default:
 137                 fprintf(stderr, "unsupported insn\n");
 138                 return;
 139         }
 140         insn->target->priv = t;
 141 }
 142
 143 static void binop(Btor *btor, struct instruction *insn)
 144 {
 145         BoolectorSort s = get_sort(btor, insn->type, insn->pos);
 146         binary(btor, s, insn);
 147 }
 148
 149 static void icmp(Btor *btor, struct instruction *insn)
 150 {
 151         BoolectorSort s = get_sort(btor, insn->itype, insn->pos);
 152         binary(btor, s, insn);
 153 }
 154
 155 static void unop(Btor *btor, struct instruction *insn)
 156 {
 157         BoolectorSort s = get_sort(btor, insn->type, insn->pos);
 158         BoolectorNode *t, *a;
 159
 160         a = mkvar(btor, s, insn->src1);
 161         if (!a)
 162                 return;
 163         switch (insn->opcode) {
 164         case OP_NEG:    t = boolector_neg(btor, a); break;
 165         case OP_NOT:    t = boolector_not(btor, a); break;
 166         case OP_SEXT:   t = sext(btor, insn, a); break;
 167         case OP_ZEXT:   t = zext(btor, insn, a); break;
 168         case OP_TRUNC:  t = slice(btor, insn, a); break;
 169         default:
 170                 fprintf(stderr, "unsupported insn\n");
 171                 return;
 172         }
 173         insn->target->priv = t;
 174 }
 175
 176 static void ternop(Btor *btor, struct instruction *insn)
 177 {
 178         BoolectorSort s = get_sort(btor, insn->type, insn->pos);
 179         BoolectorNode *t, *a, *b, *c, *z, *d;
 180
 181         a = mkvar(btor, s, insn->src1);
 182         b = mkvar(btor, s, insn->src2);
 183         c = mkvar(btor, s, insn->src3);
 184         if (!a || !b || !c)
 185                 return;
 186         switch (insn->opcode) {
 187         case OP_SEL:
 188                 z = boolector_zero(btor, s);
 189                 d = boolector_ne(btor, a, z);
 190                 t = boolector_cond(btor, d, b, c);
 191                 break;
 192         default:
 193                 fprintf(stderr, "unsupported insn\n");
 194                 return;
 195         }
 196         insn->target->priv = t;
 197 }
 198
 199 static bool add_precondition(Btor *btor, BoolectorNode **pre, struct instruction *insn)
 200 {
 201         BoolectorNode *a = get_arg(btor, insn, 0);
 202         BoolectorNode *z = boolector_zero(btor, boolector_get_sort(btor, a));
 203         BoolectorNode *n = boolector_ne(btor, a, z);
 204         BoolectorNode *p = boolector_and(btor, *pre, n);
 205         *pre = p;
 206         return true;
 207 }
 208
 209 static bool check_btor(Btor *btor, BoolectorNode *p, BoolectorNode *n, struct instruction *insn)
 210 {
 211         char model_format[] = "btor";
 212         int res;
 213
 214         n = boolector_implies(btor, p, n);
 215         boolector_assert(btor, boolector_not(btor, n));
 216         res = boolector_sat(btor);
 217         switch (res) {
 218         case BOOLECTOR_UNSAT:
 219                 return 1;
 220         case BOOLECTOR_SAT:
 221                 sparse_error(insn->pos, "assertion failed");
 222                 show_entry(insn->bb->ep);
 223                 boolector_dump_btor(btor, stdout);
 224                 boolector_print_model(btor, model_format, stdout);
 225                 break;
 226         default:
 227                 sparse_error(insn->pos, "SMT failure");
 228                 break;
 229         }
 230         return 0;
 231 }
 232
 233 static bool check_assert(Btor *btor, BoolectorNode *pre, struct instruction *insn)
 234 {
 235         BoolectorNode *a = get_arg(btor, insn, 0);
 236         BoolectorNode *z = boolector_zero(btor, boolector_get_sort(btor, a));
 237         BoolectorNode *n = boolector_ne(btor, a, z);
 238         return check_btor(btor, pre, n, insn);
 239 }
 240
 241 static bool check_equal(Btor *btor, BoolectorNode *pre, struct instruction *insn)
 242 {
 243         BoolectorNode *a = get_arg(btor, insn, 0);
 244         BoolectorNode *b = get_arg(btor, insn, 1);
 245         BoolectorNode *n = boolector_eq(btor, a, b);
 246         return check_btor(btor, pre, n, insn);
 247 }
 248
 249 static bool check_const(Btor *ctxt, struct instruction *insn)
 250 {
 251         pseudo_t src1 = ptr_list_nth(insn->arguments, 0);
 252         pseudo_t src2 = ptr_list_nth(insn->arguments, 1);
 253
 254         if (src2->type != PSEUDO_VAL)
 255                 sparse_error(insn->pos, "should be a constant: %s", show_pseudo(src2));
 256         if (src1 == src2)
 257                 return 1;
 258         if (src1->type != PSEUDO_VAL)
 259                 sparse_error(insn->pos, "not a constant: %s", show_pseudo(src1));
 260         else
 261                 sparse_error(insn->pos, "invalid value: %s != %s", show_pseudo(src1), show_pseudo(src2));
 262         return 0;
 263 }
 264
 265 static bool check_call(Btor *btor, BoolectorNode **pre, struct instruction *insn)
 266 {
 267         pseudo_t func = insn->func;
 268         struct ident *ident = func->ident;
 269
 270         if (ident == &__assume_ident)
 271                 return add_precondition(btor, pre, insn);
 272         if (ident == &__assert_ident)
 273                 return check_assert(btor, *pre, insn);
 274         if (ident == &__assert_eq_ident)
 275                 return check_equal(btor, *pre, insn);
 276         if (ident == &__assert_const_ident)
 277                 return check_const(btor, insn);
 278         return 0;
 279 }
 280
 281 static bool check_function(struct entrypoint *ep)
 282 {
 283         Btor *btor = boolector_new();
 284         BoolectorNode *pre = boolector_true(btor);
 285         struct basic_block *bb;
 286         int rc = 0;
 287
 288         boolector_set_opt(btor, BTOR_OPT_MODEL_GEN, 1);
 289         boolector_set_opt(btor, BTOR_OPT_INCREMENTAL, 1);
 290
 291         FOR_EACH_PTR(ep->bbs, bb) {
 292                 struct instruction *insn;
 293                 FOR_EACH_PTR(bb->insns, insn) {
 294                         if (!insn->bb)
 295                                 continue;
 296                         switch (insn->opcode) {
 297                         case OP_ENTRY:
 298                                 continue;
 299                         case OP_BINARY ... OP_BINARY_END:
 300                                 binop(btor, insn);
 301                                 break;
 302                         case OP_BINCMP ... OP_BINCMP_END:
 303                                 icmp(btor, insn);
 304                                 break;
 305                         case OP_UNOP ... OP_UNOP_END:
 306                                 unop(btor, insn);
 307                                 break;
 308                         case OP_SEL:
 309                                 ternop(btor, insn);
 310                                 break;
 311                         case OP_CALL:
 312                                 rc &= check_call(btor, &pre, insn);
 313                                 break;
 314                         case OP_RET:
 315                                 goto out;
 316                         default:
 317                                 fprintf(stderr, "unsupported insn\n");
 318                                 goto out;
 319                         }
 320                 } END_FOR_EACH_PTR(insn);
 321         } END_FOR_EACH_PTR(bb);
 322         fprintf(stderr, "unterminated function\n");
 323
 324 out:
 325         boolector_release_all(btor);
 326         boolector_delete(btor);
 327         return rc;
 328 }
 329
 330 static void check_functions(struct symbol_list *list)
 331 {
 332         struct symbol *sym;
 333
 334         FOR_EACH_PTR(list, sym) {
 335                 struct entrypoint *ep;
 336
 337                 expand_symbol(sym);
 338                 ep = linearize_symbol(sym);
 339                 if (!ep || !ep->entry)
 340                         continue;
 341                 check_function(ep);
 342         } END_FOR_EACH_PTR(sym);
 343 }
 344
 345 int main(int argc, char **argv)
 346 {
 347         struct string_list *filelist = NULL;
 348         char *file;
 349
 350         Wdecl = 0;
 351
 352         sparse_initialize(argc, argv, &filelist);
 353
 354         declare_builtins(0, builtins_scheck);
 355         predefine_strong("__SYMBOLIC_CHECKER__");
 356
 357         // Expand, linearize and check.
 358         FOR_EACH_PTR(filelist, file) {
 359                 check_functions(sparse(file));
 360         } END_FOR_EACH_PTR(file);
 361         return 0;
 362 }