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         switch (pseudo->type) {
  57         case PSEUDO_VAL:
  58                 sprintf(buff, "%llx", pseudo->value);
  59                 return boolector_consth(btor, s, buff);
  60         case PSEUDO_ARG:
  61         case PSEUDO_REG:
  62                 if (pseudo->priv)
  63                         return pseudo->priv;
  64                 n = boolector_var(btor, s, show_pseudo(pseudo));
  65                 break;
  66         default:
  67                 fprintf(stderr, "invalid pseudo: %s\n", show_pseudo(pseudo));
  68                 return NULL;
  69         }
  70         return pseudo->priv = n;
  71 }
  72
  73 static BoolectorNode *mktvar(Btor *btor, struct instruction *insn, pseudo_t src)
  74 {
  75         BoolectorSort s = get_sort(btor, insn->type, insn->pos);
  76         return mkvar(btor, s, src);
  77 }
  78
  79 static BoolectorNode *mkivar(Btor *btor, struct instruction *insn, pseudo_t src)
  80 {
  81         BoolectorSort s = get_sort(btor, insn->itype, insn->pos);
  82         return mkvar(btor, s, src);
  83 }
  84
  85 static BoolectorNode *get_arg(Btor *btor, struct instruction *insn, int idx)
  86 {
  87         pseudo_t arg = ptr_list_nth(insn->arguments, idx);
  88         struct symbol *type = ptr_list_nth(insn->fntypes, idx + 1);
  89         BoolectorSort s = get_sort(btor, type, insn->pos);
  90
  91         return mkvar(btor, s, arg);
  92 }
  93
  94 static BoolectorNode *zext(Btor *btor, struct instruction *insn, BoolectorNode *s)
  95 {
  96         int old = boolector_get_width(btor, s);
  97         int new = insn->type->bit_size;
  98         return boolector_uext(btor, s, new - old);
  99 }
 100
 101 static BoolectorNode *sext(Btor *btor, struct instruction *insn, BoolectorNode *s)
 102 {
 103         int old = boolector_get_width(btor, s);
 104         int new = insn->type->bit_size;
 105         return boolector_sext(btor, s, new - old);
 106 }
 107
 108 static BoolectorNode *slice(Btor *btor, struct instruction *insn, BoolectorNode *s)
 109 {
 110         int old = boolector_get_width(btor, s);
 111         int new = insn->type->bit_size;
 112         return boolector_slice(btor, s, old - new - 1, 0);
 113 }
 114
 115 static void binary(Btor *btor, BoolectorSort s, struct instruction *insn)
 116 {
 117         BoolectorNode *t, *a, *b;
 118
 119         a = mkvar(btor, s, insn->src1);
 120         b = mkvar(btor, s, insn->src2);
 121         if (!a || !b)
 122                 return;
 123         switch (insn->opcode) {
 124         case OP_ADD:    t = boolector_add(btor, a, b); break;
 125         case OP_SUB:    t = boolector_sub(btor, a, b); break;
 126         case OP_MUL:    t = boolector_mul(btor, a, b); break;
 127         case OP_AND:    t = boolector_and(btor, a, b); break;
 128         case OP_OR:     t = boolector_or (btor, a, b); break;
 129         case OP_XOR:    t = boolector_xor(btor, a, b); break;
 130         case OP_SHL:    t = boolector_sll(btor, a, b); break;
 131         case OP_LSR:    t = boolector_srl(btor, a, b); break;
 132         case OP_ASR:    t = boolector_sra(btor, a, b); break;
 133         case OP_DIVS:   t = boolector_sdiv(btor, a, b); break;
 134         case OP_DIVU:   t = boolector_udiv(btor, a, b); break;
 135         case OP_MODS:   t = boolector_srem(btor, a, b); break;
 136         case OP_MODU:   t = boolector_urem(btor, a, b); break;
 137         case OP_SET_EQ: t = zext(btor, insn, boolector_eq(btor, a, b)); break;
 138         case OP_SET_NE: t = zext(btor, insn, boolector_ne(btor, a, b)); break;
 139         case OP_SET_LT: t = zext(btor, insn, boolector_slt(btor, a, b)); break;
 140         case OP_SET_LE: t = zext(btor, insn, boolector_slte(btor, a, b)); break;
 141         case OP_SET_GE: t = zext(btor, insn, boolector_sgte(btor, a, b)); break;
 142         case OP_SET_GT: t = zext(btor, insn, boolector_sgt(btor, a, b)); break;
 143         case OP_SET_B:  t = zext(btor, insn, boolector_ult(btor, a, b)); break;
 144         case OP_SET_BE: t = zext(btor, insn, boolector_ulte(btor, a, b)); break;
 145         case OP_SET_AE: t = zext(btor, insn, boolector_ugte(btor, a, b)); break;
 146         case OP_SET_A:  t = zext(btor, insn, boolector_ugt(btor, a, b)); break;
 147         default:
 148                 fprintf(stderr, "unsupported insn: %s\n", show_instruction(insn));
 149                 return;
 150         }
 151         insn->target->priv = t;
 152 }
 153
 154 static void binop(Btor *btor, struct instruction *insn)
 155 {
 156         BoolectorSort s = get_sort(btor, insn->type, insn->pos);
 157         binary(btor, s, insn);
 158 }
 159
 160 static void icmp(Btor *btor, struct instruction *insn)
 161 {
 162         BoolectorSort s = get_sort(btor, insn->itype, insn->pos);
 163         binary(btor, s, insn);
 164 }
 165
 166 static void unop(Btor *btor, struct instruction *insn)
 167 {
 168         pseudo_t src = insn->src;
 169         BoolectorNode *t;
 170
 171         switch (insn->opcode) {
 172         case OP_SEXT:   t = sext(btor, insn, mkivar(btor, insn, src)); break;
 173         case OP_ZEXT:   t = zext(btor, insn, mkivar(btor, insn, src)); break;
 174         case OP_TRUNC:  t = slice(btor, insn, mkivar(btor, insn, src)); break;
 175
 176         case OP_NEG:    t = boolector_neg(btor, mktvar(btor, insn, src)); break;
 177         case OP_NOT:    t = boolector_not(btor, mktvar(btor, insn, src)); break;
 178         default:
 179                 fprintf(stderr, "unsupported insn: %s\n", show_instruction(insn));
 180                 return;
 181         }
 182         insn->target->priv = t;
 183 }
 184
 185 static void ternop(Btor *btor, struct instruction *insn)
 186 {
 187         BoolectorSort s = get_sort(btor, insn->type, insn->pos);
 188         BoolectorNode *t, *a, *b, *c, *z, *d;
 189
 190         a = mkvar(btor, s, insn->src1);
 191         b = mkvar(btor, s, insn->src2);
 192         c = mkvar(btor, s, insn->src3);
 193         if (!a || !b || !c)
 194                 return;
 195         switch (insn->opcode) {
 196         case OP_SEL:
 197                 z = boolector_zero(btor, s);
 198                 d = boolector_ne(btor, a, z);
 199                 t = boolector_cond(btor, d, b, c);
 200                 break;
 201         default:
 202                 fprintf(stderr, "unsupported insn: %s\n", show_instruction(insn));
 203                 return;
 204         }
 205         insn->target->priv = t;
 206 }
 207
 208 static bool add_precondition(Btor *btor, BoolectorNode **pre, struct instruction *insn)
 209 {
 210         BoolectorNode *a = get_arg(btor, insn, 0);
 211         BoolectorNode *z = boolector_zero(btor, boolector_get_sort(btor, a));
 212         BoolectorNode *n = boolector_ne(btor, a, z);
 213         BoolectorNode *p = boolector_and(btor, *pre, n);
 214         *pre = p;
 215         return true;
 216 }
 217
 218 static bool check_btor(Btor *btor, BoolectorNode *p, BoolectorNode *n, struct instruction *insn)
 219 {
 220         char model_format[] = "btor";
 221         int res;
 222
 223         n = boolector_implies(btor, p, n);
 224         boolector_assert(btor, boolector_not(btor, n));
 225         res = boolector_sat(btor);
 226         switch (res) {
 227         case BOOLECTOR_UNSAT:
 228                 return 1;
 229         case BOOLECTOR_SAT:
 230                 sparse_error(insn->pos, "assertion failed");
 231                 show_entry(insn->bb->ep);
 232                 boolector_dump_btor(btor, stdout);
 233                 boolector_print_model(btor, model_format, stdout);
 234                 break;
 235         default:
 236                 sparse_error(insn->pos, "SMT failure");
 237                 break;
 238         }
 239         return 0;
 240 }
 241
 242 static bool check_assert(Btor *btor, BoolectorNode *pre, struct instruction *insn)
 243 {
 244         BoolectorNode *a = get_arg(btor, insn, 0);
 245         BoolectorNode *z = boolector_zero(btor, boolector_get_sort(btor, a));
 246         BoolectorNode *n = boolector_ne(btor, a, z);
 247         return check_btor(btor, pre, n, insn);
 248 }
 249
 250 static bool check_equal(Btor *btor, BoolectorNode *pre, struct instruction *insn)
 251 {
 252         BoolectorNode *a = get_arg(btor, insn, 0);
 253         BoolectorNode *b = get_arg(btor, insn, 1);
 254         BoolectorNode *n = boolector_eq(btor, a, b);
 255         return check_btor(btor, pre, n, insn);
 256 }
 257
 258 static bool check_const(Btor *ctxt, struct instruction *insn)
 259 {
 260         pseudo_t src1 = ptr_list_nth(insn->arguments, 0);
 261         pseudo_t src2 = ptr_list_nth(insn->arguments, 1);
 262
 263         if (src2->type != PSEUDO_VAL)
 264                 sparse_error(insn->pos, "should be a constant: %s", show_pseudo(src2));
 265         if (src1 == src2)
 266                 return 1;
 267         if (src1->type != PSEUDO_VAL)
 268                 sparse_error(insn->pos, "not a constant: %s", show_pseudo(src1));
 269         else
 270                 sparse_error(insn->pos, "invalid value: %s != %s", show_pseudo(src1), show_pseudo(src2));
 271         return 0;
 272 }
 273
 274 static bool check_call(Btor *btor, BoolectorNode **pre, struct instruction *insn)
 275 {
 276         pseudo_t func = insn->func;
 277         struct ident *ident = func->ident;
 278
 279         if (ident == &__assume_ident)
 280                 return add_precondition(btor, pre, insn);
 281         if (ident == &__assert_ident)
 282                 return check_assert(btor, *pre, insn);
 283         if (ident == &__assert_eq_ident)
 284                 return check_equal(btor, *pre, insn);
 285         if (ident == &__assert_const_ident)
 286                 return check_const(btor, insn);
 287         return 0;
 288 }
 289
 290 static bool check_function(struct entrypoint *ep)
 291 {
 292         Btor *btor = boolector_new();
 293         BoolectorNode *pre = boolector_true(btor);
 294         struct basic_block *bb;
 295         int rc = 0;
 296
 297         boolector_set_opt(btor, BTOR_OPT_MODEL_GEN, 1);
 298         boolector_set_opt(btor, BTOR_OPT_INCREMENTAL, 1);
 299
 300         FOR_EACH_PTR(ep->bbs, bb) {
 301                 struct instruction *insn;
 302                 FOR_EACH_PTR(bb->insns, insn) {
 303                         if (!insn->bb)
 304                                 continue;
 305                         switch (insn->opcode) {
 306                         case OP_ENTRY:
 307                                 continue;
 308                         case OP_BINARY ... OP_BINARY_END:
 309                                 binop(btor, insn);
 310                                 break;
 311                         case OP_BINCMP ... OP_BINCMP_END:
 312                                 icmp(btor, insn);
 313                                 break;
 314                         case OP_UNOP ... OP_UNOP_END:
 315                                 unop(btor, insn);
 316                                 break;
 317                         case OP_SEL:
 318                                 ternop(btor, insn);
 319                                 break;
 320                         case OP_CALL:
 321                                 rc &= check_call(btor, &pre, insn);
 322                                 break;
 323                         case OP_RET:
 324                                 goto out;
 325                         case OP_INLINED_CALL:
 326                         case OP_DEATHNOTE:
 327                         case OP_NOP:
 328                         case OP_CONTEXT:
 329                                 continue;
 330                         default:
 331                                 fprintf(stderr, "unsupported insn: %s\n", show_instruction(insn));
 332                                 goto out;
 333                         }
 334                 } END_FOR_EACH_PTR(insn);
 335         } END_FOR_EACH_PTR(bb);
 336         fprintf(stderr, "unterminated function\n");
 337
 338 out:
 339         boolector_release_all(btor);
 340         boolector_delete(btor);
 341         return rc;
 342 }
 343
 344 static void check_functions(struct symbol_list *list)
 345 {
 346         struct symbol *sym;
 347
 348         FOR_EACH_PTR(list, sym) {
 349                 struct entrypoint *ep;
 350
 351                 expand_symbol(sym);
 352                 ep = linearize_symbol(sym);
 353                 if (!ep || !ep->entry)
 354                         continue;
 355                 check_function(ep);
 356         } END_FOR_EACH_PTR(sym);
 357 }
 358
 359 int main(int argc, char **argv)
 360 {
 361         struct string_list *filelist = NULL;
 362         char *file;
 363
 364         Wdecl = 0;
 365
 366         sparse_initialize(argc, argv, &filelist);
 367
 368         declare_builtins(0, builtins_scheck);
 369         predefine_strong("__SYMBOLIC_CHECKER__");
 370
 371         // Expand, linearize and check.
 372         FOR_EACH_PTR(filelist, file) {
 373                 check_functions(sparse(file));
 374         } END_FOR_EACH_PTR(file);
 375         return 0;
 376 }