encoder_smtlib.cc 29.1 KB
Newer Older
phlo's avatar
phlo committed
1
#include "encoder_smtlib.hh"
2

3 4
#include <cassert>

5
#include "mmap.hh"
6 7
#include "smtlib.hh"

phlo's avatar
phlo committed
8
namespace ConcuBinE::smtlib {
phlo's avatar
phlo committed
9 10

//==============================================================================
phlo's avatar
phlo committed
11
// smtlib::Encoder
phlo's avatar
phlo committed
12 13 14
//==============================================================================

//------------------------------------------------------------------------------
phlo's avatar
phlo committed
15
// public constants
phlo's avatar
phlo committed
16 17
//------------------------------------------------------------------------------

phlo's avatar
phlo committed
18
const std::string & Encoder::exit_code_var = exit_code_sym;
19

phlo's avatar
phlo committed
20 21 22
//------------------------------------------------------------------------------
// public constructors
//------------------------------------------------------------------------------
23

phlo's avatar
phlo committed
24 25 26 27 28 29
Encoder::Encoder (const std::shared_ptr<Program::List> & p,
                  const std::shared_ptr<MMap> & m,
                  const size_t b) :
  ConcuBinE::Encoder(p, m, b),
  step(0)
{}
phlo's avatar
phlo committed
30

phlo's avatar
phlo committed
31 32 33 34 35 36 37 38 39 40 41 42 43 44 45 46 47 48 49 50 51 52 53 54 55 56 57 58 59 60 61 62 63 64 65 66 67 68 69 70 71 72 73 74 75 76 77 78 79 80 81 82 83 84 85 86 87 88 89 90 91 92 93 94 95 96 97 98 99 100 101 102 103 104 105 106 107 108 109 110 111 112 113 114 115 116 117 118 119 120 121 122 123 124 125 126 127 128 129 130 131 132 133 134 135 136 137 138 139 140 141 142 143 144 145 146 147 148 149 150 151 152 153 154 155 156 157 158 159 160 161 162 163 164 165 166 167 168 169 170 171 172 173 174 175 176 177 178 179 180 181
//------------------------------------------------------------------------------
// public member functions
//------------------------------------------------------------------------------

// smtlib::Encoder::accu_var ---------------------------------------------------

std::string Encoder::accu_var (const word_t k, const word_t t)
{
  return accu_sym + '_' + std::to_string(k) + '_' + std::to_string(t);
}

// smtlib::Encoder::mem_var ----------------------------------------------------

std::string Encoder::mem_var (const word_t k, const word_t t)
{
  return mem_sym + '_' + std::to_string(k) + '_' + std::to_string(t);
}

// smtlib::Encoder::sb_adr_var -------------------------------------------------

std::string Encoder::sb_adr_var (const word_t k, const word_t t)
{
  return sb_adr_sym + '_' + std::to_string(k) + '_' + std::to_string(t);
}

// smtlib::Encoder::sb_val_var -------------------------------------------------

std::string Encoder::sb_val_var (const word_t k, const word_t t)
{
  return sb_val_sym + '_' + std::to_string(k) + '_' + std::to_string(t);
}

// smtlib::Encoder::sb_full_var ------------------------------------------------

std::string Encoder::sb_full_var (const word_t k, const word_t t)
{
  return sb_full_sym + '_' + std::to_string(k) + '_' + std::to_string(t);
}

// smtlib::Encoder::stmt_var ---------------------------------------------------

std::string Encoder::stmt_var (const word_t k, const word_t t, const word_t p)
{
  return
    stmt_sym + '_' +
    std::to_string(k) + '_' +
    std::to_string(t) + '_' +
    std::to_string(p);
}

// smtlib::Encoder::block_var --------------------------------------------------

std::string Encoder::block_var (const word_t k,
                                const word_t id,
                                const word_t tid)
{
  return
    block_sym + '_' +
    std::to_string(k) + '_' +
    std::to_string(id) + '_' +
    std::to_string(tid);
}

// smtlib::Encoder::halt_var ---------------------------------------------------

std::string Encoder::halt_var (const word_t k, const word_t t)
{
  return halt_sym + '_' + std::to_string(k) + '_' + std::to_string(t);
}

// smtlib::Encoder::heap_var ---------------------------------------------------

std::string Encoder::heap_var (const word_t k)
{
  return heap_sym + '_' + std::to_string(k);
}

// smtlib::Encoder::exit_flag_var ----------------------------------------------

std::string Encoder::exit_flag_var (const word_t k)
{
  return exit_flag_sym + '_' + std::to_string(k);
}

// smtlib::Encoder::thread_var -------------------------------------------------

std::string Encoder::thread_var (const word_t k, const word_t t)
{
  return thread_sym + '_' + std::to_string(k) + '_' + std::to_string(t);
}

// smtlib::Encoder::exec_var ---------------------------------------------------

std::string Encoder::exec_var (const word_t k, const word_t t, const word_t p)
{
  return
    exec_sym + '_' +
    std::to_string(k) + '_' +
    std::to_string(t) + '_' +
    std::to_string(p);
}

// smtlib::Encoder::flush_var --------------------------------------------------

std::string Encoder::flush_var (const word_t k, const word_t t)
{
  return flush_sym + '_' + std::to_string(k) + '_' + std::to_string(t);
}

// smtlib::Encoder::check_var --------------------------------------------------

std::string Encoder::check_var (const word_t k, const word_t id)
{
  return check_sym + '_' + std::to_string(k) + '_' + std::to_string(id);
}

//------------------------------------------------------------------------------
// public member functions inherited from ConcuBinE::Encoder
//------------------------------------------------------------------------------

// smtlib::Encoder::encode -----------------------------------------------------

void Encoder::encode ()
{
  formula << set_logic() << eol << eol;

  for (step = 0, prev = static_cast<size_t>(-1); step <= bound; step++, prev++)
    {
      if (verbose)
        formula << comment_section("step " + std::to_string(step));

      declare_states();
      declare_transitions();
      define_transitions();

      if (step)
        define_states();
      else
        init_states();

      define_constraints ();
    }
}

// smtlib::Encoder::assert_exit ------------------------------------------------

void Encoder::assert_exit ()
{
  formula <<
    smtlib::assertion(
      smtlib::lnot(
182
        smtlib::equality(
phlo's avatar
phlo committed
183
          smtlib::Encoder::exit_code_var,
184
          smtlib::word2hex(0))));
phlo's avatar
phlo committed
185 186 187 188 189 190 191 192 193
}

//------------------------------------------------------------------------------
// protected constants
//------------------------------------------------------------------------------

// bitvector sort declaration --------------------------------------------------

const std::string Encoder::bv_sort = bitvector(word_size);
phlo's avatar
phlo committed
194 195 196

// variable comments -----------------------------------------------------------

phlo's avatar
phlo committed
197 198
const std::string Encoder::accu_comment =
  comment(
phlo's avatar
phlo committed
199 200 201 202 203
    ConcuBinE::Encoder::accu_comment
    + " - "
    + accu_sym
    + "_<step>_<thread>"
    + eol);
204

phlo's avatar
phlo committed
205
const std::string Encoder::mem_comment =
phlo's avatar
phlo committed
206 207 208 209 210 211
  comment(
    ConcuBinE::Encoder::mem_comment
    + " - "
    + mem_sym
    + "_<step>_<thread>"
    + eol);
212

phlo's avatar
phlo committed
213 214
const std::string Encoder::sb_adr_comment =
  comment(
phlo's avatar
phlo committed
215 216 217 218 219
    ConcuBinE::Encoder::sb_adr_comment
    + " - "
    + sb_adr_sym
    + "_<step>_<thread>"
    + eol);
220

phlo's avatar
phlo committed
221 222
const std::string Encoder::sb_val_comment =
  comment(
phlo's avatar
phlo committed
223 224 225 226 227
    ConcuBinE::Encoder::sb_val_comment
    + " - "
    + sb_val_sym
    + "_<step>_<thread>"
    + eol);
228

phlo's avatar
phlo committed
229 230
const std::string Encoder::sb_full_comment =
  comment(
phlo's avatar
phlo committed
231 232 233 234 235
    ConcuBinE::Encoder::sb_full_comment
    + " - "
    + sb_full_sym
    + "_<step>_<thread>"
    + eol);
236

phlo's avatar
phlo committed
237 238
const std::string Encoder::stmt_comment =
  comment(
phlo's avatar
phlo committed
239 240 241 242 243
    ConcuBinE::Encoder::stmt_comment
    + " - "
    + stmt_sym
    + "_<step>_<thread>_<pc>"
    + eol);
244

phlo's avatar
phlo committed
245 246
const std::string Encoder::block_comment =
  comment(
phlo's avatar
phlo committed
247 248 249 250 251
    ConcuBinE::Encoder::block_comment
    + " - "
    + block_sym
    + "_<step>_<id>_<thread>"
    + eol);
252

253 254
const std::string Encoder::halt_comment =
  comment(
phlo's avatar
phlo committed
255 256 257 258 259
    ConcuBinE::Encoder::halt_comment
    + " - "
    + halt_sym
    + "_<step>_<thread>"
    + eol);
260

phlo's avatar
phlo committed
261 262
const std::string Encoder::heap_comment =
  comment(
phlo's avatar
phlo committed
263 264 265 266 267
    ConcuBinE::Encoder::heap_comment
    + " - "
    + heap_sym
    + "_<step>"
    + eol);
268

phlo's avatar
phlo committed
269 270
const std::string Encoder::exit_flag_comment =
  comment(
phlo's avatar
phlo committed
271 272 273 274 275
    ConcuBinE::Encoder::exit_flag_comment
    + " - "
    + exit_flag_sym
    + "_<step>"
    + eol);
phlo's avatar
phlo committed
276

phlo's avatar
phlo committed
277
const std::string Encoder::exit_code_comment =
phlo's avatar
phlo committed
278
  comment(ConcuBinE::Encoder::exit_code_comment + eol);
279

phlo's avatar
phlo committed
280 281
const std::string Encoder::thread_comment =
  comment(
phlo's avatar
phlo committed
282 283 284 285 286
    ConcuBinE::Encoder::thread_comment
    + " - "
    + thread_sym
    + "_<step>_<thread>"
    + eol);
287

phlo's avatar
phlo committed
288 289
const std::string Encoder::exec_comment =
  comment(
phlo's avatar
phlo committed
290 291 292 293 294
    ConcuBinE::Encoder::exec_comment
    + " - "
    + exec_sym
    + "_<step>_<thread>_<pc>"
    + eol);
phlo's avatar
phlo committed
295

phlo's avatar
phlo committed
296 297
const std::string Encoder::flush_comment =
  comment(
phlo's avatar
phlo committed
298 299 300 301 302
    ConcuBinE::Encoder::flush_comment
    + " - "
    + flush_sym
    + "_<step>_<thread>"
    + eol);
303

phlo's avatar
phlo committed
304 305
const std::string Encoder::check_comment =
  comment(
phlo's avatar
phlo committed
306 307 308 309 310
    ConcuBinE::Encoder::check_comment
    + " - "
    + check_sym
    + "_<step>_<id>"
    + eol);
311

phlo's avatar
phlo committed
312
//------------------------------------------------------------------------------
phlo's avatar
phlo committed
313
// protected member functions
phlo's avatar
phlo committed
314
//------------------------------------------------------------------------------
315

phlo's avatar
phlo committed
316
// smtlib::Encoder::accu_var ---------------------------------------------------
317

phlo's avatar
phlo committed
318
std::string Encoder::accu_var () const { return accu_var(step, thread); }
phlo's avatar
phlo committed
319

phlo's avatar
phlo committed
320
// smtlib::Encoder::mem_var ----------------------------------------------------
phlo's avatar
phlo committed
321

phlo's avatar
phlo committed
322 323 324 325 326 327 328 329 330 331 332 333 334 335 336 337 338 339 340 341 342 343 344 345 346 347 348 349 350 351 352 353 354
std::string Encoder::mem_var () const { return mem_var(step, thread); }

// smtlib::Encoder::sb_adr_var -------------------------------------------------

std::string Encoder::sb_adr_var () const { return sb_adr_var(step, thread); }

// smtlib::Encoder::sb_val_var -------------------------------------------------

std::string Encoder::sb_val_var () const { return sb_val_var(step, thread); }

// smtlib::Encoder::sb_full_var ------------------------------------------------

std::string Encoder::sb_full_var () const { return sb_full_var(step, thread); }

// smtlib::Encoder::stmt_var ---------------------------------------------------

std::string Encoder::stmt_var () const { return stmt_var(step, thread, pc); }

// smtlib::Encoder::halt_var ---------------------------------------------------

std::string Encoder::halt_var () const { return halt_var(step, thread); }

// smtlib::Encoder::heap_var ---------------------------------------------------

std::string Encoder::heap_var () const { return heap_var(step); }

// smtlib::Encoder::exit_flag_var ----------------------------------------------

std::string Encoder::exit_flag_var () const { return exit_flag_var(step); }

// smtlib::Encoder::thread_var -------------------------------------------------

std::string Encoder::thread_var () const { return thread_var(step, thread); }
355

phlo's avatar
phlo committed
356 357 358 359 360 361 362 363 364 365 366 367
// smtlib::Encoder::exec_var ---------------------------------------------------

std::string Encoder::exec_var () const { return exec_var(step, thread, pc); }

// smtlib::Encoder::flush_var --------------------------------------------------

std::string Encoder::flush_var () const { return flush_var(step, thread); }

// smtlib::Encoder::assign -----------------------------------------------------

std::string Encoder::assign (const std::string & var,
                             const std::string & expr) const
368
{
369
  return assertion(equality(var, expr));
370 371
}

phlo's avatar
phlo committed
372 373 374
//------------------------------------------------------------------------------
// protected member functions inherited from ConcuBinE::Encoder
//------------------------------------------------------------------------------
phlo's avatar
phlo committed
375

phlo's avatar
phlo committed
376 377 378
// smtlib::Encoder::encode -----------------------------------------------------

std::string Encoder::encode (const Instruction::Load & l)
379
{
phlo's avatar
phlo committed
380
  return load(l.arg, l.indirect);
381 382
}

phlo's avatar
phlo committed
383
std::string Encoder::encode (const Instruction::Store & s)
384
{
phlo's avatar
phlo committed
385 386 387 388
  switch (update)
    {
    case Update::sb_adr:
      return s.indirect ? load(s.arg) : word2hex(s.arg);
389

phlo's avatar
phlo committed
390 391
    case Update::sb_val:
      return accu_var(prev, thread);
phlo's avatar
phlo committed
392

phlo's avatar
phlo committed
393 394
    default: throw std::runtime_error("illegal state update");
    }
395 396
}

phlo's avatar
phlo committed
397
std::string Encoder::encode (const Instruction::Fence & f [[maybe_unused]])
398
{
phlo's avatar
phlo committed
399
  return "";
400 401
}

phlo's avatar
phlo committed
402
std::string Encoder::encode (const Instruction::Add & a)
403
{
404
  return bvadd(accu_var(prev, thread), load(a.arg, a.indirect));
405 406
}

phlo's avatar
phlo committed
407
std::string Encoder::encode (const Instruction::Addi & a)
408
{
409
  return bvadd(accu_var(prev, thread), word2hex(a.arg));
410 411
}

phlo's avatar
phlo committed
412
std::string Encoder::encode (const Instruction::Sub & s)
413
{
414
  return bvsub(accu_var(prev, thread), load(s.arg, s.indirect));
415 416
}

phlo's avatar
phlo committed
417
std::string Encoder::encode (const Instruction::Subi & s)
418
{
419
  return bvsub(accu_var(prev, thread), word2hex(s.arg));
420 421
}

phlo's avatar
phlo committed
422
std::string Encoder::encode (const Instruction::Mul & m)
423
{
424
  return bvmul(accu_var(prev, thread), load(m.arg, m.indirect));
425 426
}

phlo's avatar
phlo committed
427
std::string Encoder::encode (const Instruction::Muli & m)
428
{
429
  return bvmul(accu_var(prev, thread), word2hex(m.arg));
430 431
}

phlo's avatar
phlo committed
432
std::string Encoder::encode (const Instruction::Cmp & c)
433
{
434
  return bvsub(accu_var(prev, thread), load(c.arg, c.indirect));
435 436
}

phlo's avatar
phlo committed
437
std::string Encoder::encode (const Instruction::Jmp & j [[maybe_unused]])
438
{
phlo's avatar
phlo committed
439
  return "";
440 441
}

phlo's avatar
phlo committed
442
std::string Encoder::encode (const Instruction::Jz & j [[maybe_unused]])
443
{
444
  return equality(accu_var(prev, thread), word2hex(0));
445 446
}

phlo's avatar
phlo committed
447
std::string Encoder::encode (const Instruction::Jnz & j [[maybe_unused]])
448
{
phlo's avatar
phlo committed
449 450
  return
    lnot(
451
      equality(
phlo's avatar
phlo committed
452
        accu_var(prev, thread),
453
        word2hex(0)));
454 455
}

phlo's avatar
phlo committed
456
std::string Encoder::encode (const Instruction::Js & j [[maybe_unused]])
457
{
phlo's avatar
phlo committed
458
  static const std::string bw = std::to_string(word_size - 1);
459

phlo's avatar
phlo committed
460
  return
461
      equality(
phlo's avatar
phlo committed
462
        "#b1",
463
        extract(bw, bw, accu_var(prev, thread)));
phlo's avatar
phlo committed
464
}
phlo's avatar
phlo committed
465

phlo's avatar
phlo committed
466
std::string Encoder::encode (const Instruction::Jns & j [[maybe_unused]])
467
{
phlo's avatar
phlo committed
468 469 470
  static const std::string bw = std::to_string(word_size - 1);

  return
471
      equality(
phlo's avatar
phlo committed
472
        "#b0",
473
        extract(bw, bw, accu_var(prev, thread)));
474 475
}

phlo's avatar
phlo committed
476
std::string Encoder::encode (const Instruction::Jnzns & j [[maybe_unused]])
477
{
phlo's avatar
phlo committed
478 479 480
  static const std::string bw = std::to_string(word_size - 1);

  return
481
    land(
phlo's avatar
phlo committed
482
      lnot(
483
        equality(
phlo's avatar
phlo committed
484
          accu_var(prev, thread),
485 486
          word2hex(0))),
      equality(
phlo's avatar
phlo committed
487
        "#b0",
488
        extract(bw, bw, accu_var(prev, thread))));
489 490
}

phlo's avatar
phlo committed
491
std::string Encoder::encode (const Instruction::Mem & m)
492
{
phlo's avatar
phlo committed
493
  return load(m.arg, m.indirect);
494 495
}

phlo's avatar
phlo committed
496
std::string Encoder::encode (const Instruction::Cas & c)
497
{
phlo's avatar
phlo committed
498
  std::string heap = heap_var(prev);
499

phlo's avatar
phlo committed
500 501 502
  std::string address = c.indirect
    ? select(heap, word2hex(c.arg))
    : word2hex(c.arg);
phlo's avatar
phlo committed
503

phlo's avatar
phlo committed
504
  std::string condition =
505
    equality(
phlo's avatar
phlo committed
506
      mem_var(prev, thread),
507
      select(heap, address));
508

phlo's avatar
phlo committed
509 510 511 512 513 514 515 516
  switch (update)
    {
    case Update::accu:
      return
        ite(
          condition,
          word2hex(1),
          word2hex(0));
517

phlo's avatar
phlo committed
518 519 520 521 522 523 524 525 526
    case Update::heap:
      return
        ite(
          condition,
          store(
            heap,
            address,
            accu_var(prev, thread)),
          heap);
phlo's avatar
phlo committed
527

phlo's avatar
phlo committed
528 529
    default: throw std::runtime_error("illegal state update");
    }
530 531
}

phlo's avatar
phlo committed
532
std::string Encoder::encode (const Instruction::Check & s [[maybe_unused]])
533
{
phlo's avatar
phlo committed
534
  return "";
535 536
}

phlo's avatar
phlo committed
537
std::string Encoder::encode (const Instruction::Halt & h [[maybe_unused]])
538
{
phlo's avatar
phlo committed
539
  return "";
540 541
}

phlo's avatar
phlo committed
542
std::string Encoder::encode (const Instruction::Exit & e)
543
{
phlo's avatar
phlo committed
544
  return word2hex(e.arg);
545 546
}

phlo's avatar
phlo committed
547 548 549 550
//------------------------------------------------------------------------------
// private member functions
//------------------------------------------------------------------------------

phlo's avatar
phlo committed
551
// smtlib::Encoder::load -------------------------------------------------------
phlo's avatar
phlo committed
552

phlo's avatar
phlo committed
553
std::string Encoder::load (const word_t adr, const bool indirect)
554
{
phlo's avatar
phlo committed
555 556 557 558 559 560 561 562 563 564 565 566 567 568 569 570 571 572 573 574 575 576 577 578 579 580 581 582 583 584 585
  // direct ////////////////////////////////////////////////////////////////////
  //
  // sb-adr == address ? sb-val : heap[address]
  //
  // indirect //////////////////////////////////////////////////////////////////
  //
  // * store buffer is full
  //   * store buffer contains address
  //     * store buffer value equals address
  //       * return store buffer value
  //     * store buffer value does not equal address
  //       * return heap[store buffer value]
  //   * store buffer does not contain address
  //     * store buffer address equals heap[address]
  //       * return return store buffer value
  //     * store buffer address does not equal heap[address]
  //       * return heap[heap[address]]
  // * store buffer is empty
  //   * return heap[heap[address]]
  //
  // sb-full
  // ? sb-adr == address
  //   ? sb-val == address
  //     ? sb-val (e.g. LOAD 0 | sb = {0, 0})
  //     : heap[sb-val] (e.g. LOAD 0 | sb = {0, 1}, heap = {{1, 1}})
  //   : sb-adr == heap[address]
  //     ? sb-val (e.g. LOAD 0 | sb = {1, 0}, heap = {{0, 1}})
  //     : heap[heap[address]] (e.g. LOAD 0 | sb = {1, x}, heap = {{0, 0}})
  // : heap[heap[address]] (e.g. LOAD 0 | sb = {}, heap = {{0, 0}})
  //
  //////////////////////////////////////////////////////////////////////////////
586

phlo's avatar
phlo committed
587
  std::string address = word2hex(adr);
588

phlo's avatar
phlo committed
589 590 591 592
  std::string sb_adr = sb_adr_var(prev, thread);
  std::string sb_val = sb_val_var(prev, thread);
  std::string sb_full = sb_full_var(prev, thread);
  std::string heap = heap_var(prev);
593

phlo's avatar
phlo committed
594
  std::string load = select(heap, address);
595 596 597

  if (indirect)
    {
phlo's avatar
phlo committed
598
      std::string load_indirect = select(heap, load);
599 600

      return
phlo's avatar
phlo committed
601
        ite(
602
          sb_full,
phlo's avatar
phlo committed
603
          ite(
604
            equality(sb_adr, address),
phlo's avatar
phlo committed
605
            ite(
606
              equality(sb_val, address),
607
              sb_val,
phlo's avatar
phlo committed
608
              select(heap, sb_val)),
phlo's avatar
phlo committed
609
            ite(
610
              equality(sb_adr, load),
611
              sb_val,
phlo's avatar
phlo committed
612 613
              load_indirect)),
          load_indirect);
614 615 616
    }
  else
    {
617
      return ite(land(sb_full, equality(sb_adr, address)), sb_val, load);
618
    }
619 620
}

phlo's avatar
phlo committed
621
// smtlib::Encoder::declare_accu -----------------------------------------------
phlo's avatar
phlo committed
622

phlo's avatar
phlo committed
623
void Encoder::declare_accu ()
624 625
{
  if (verbose)
phlo's avatar
phlo committed
626
    formula << accu_comment;
627 628

  iterate_threads([this] {
phlo's avatar
phlo committed
629
    formula << declare_bv_var(accu_var(), word_size) << eol;
630 631 632 633 634
  });

  formula << eol;
}

phlo's avatar
phlo committed
635
// smtlib::Encoder::declare_mem ------------------------------------------------
phlo's avatar
phlo committed
636

phlo's avatar
phlo committed
637
void Encoder::declare_mem ()
638 639
{
  if (verbose)
phlo's avatar
phlo committed
640
    formula << mem_comment;
641 642

  iterate_threads([this] {
phlo's avatar
phlo committed
643
    formula << declare_bv_var(mem_var(), word_size) << eol;
644 645 646 647 648
  });

  formula << eol;
}

phlo's avatar
phlo committed
649
// smtlib::Encoder::declare_sb_adr ---------------------------------------------
phlo's avatar
phlo committed
650

phlo's avatar
phlo committed
651
void Encoder::declare_sb_adr ()
652 653
{
  if (verbose)
phlo's avatar
phlo committed
654
    formula << sb_adr_comment;
655 656

  iterate_threads([this] {
phlo's avatar
phlo committed
657
    formula << declare_bv_var(sb_adr_var(), word_size) << eol;
658 659 660 661 662
  });

  formula << eol;
}

phlo's avatar
phlo committed
663
// smtlib::Encoder::declare_sb_val ---------------------------------------------
phlo's avatar
phlo committed
664

phlo's avatar
phlo committed
665
void Encoder::declare_sb_val ()
666 667
{
  if (verbose)
phlo's avatar
phlo committed
668
    formula << sb_val_comment;
669 670

  iterate_threads([this] {
phlo's avatar
phlo committed
671
    formula << declare_bv_var(sb_val_var(), word_size) << eol;
672 673 674 675 676
  });

  formula << eol;
}

phlo's avatar
phlo committed
677
// smtlib::Encoder::declare_sb_full --------------------------------------------
phlo's avatar
phlo committed
678

phlo's avatar
phlo committed
679
void Encoder::declare_sb_full ()
680 681
{
  if (verbose)
phlo's avatar
phlo committed
682
    formula << sb_full_comment;
683 684

  iterate_threads([this] {
phlo's avatar
phlo committed
685
    formula << declare_bool_var(sb_full_var()) << eol;
686 687 688 689 690
  });

  formula << eol;
}

phlo's avatar
phlo committed
691
// smtlib::Encoder::declare_stmt -----------------------------------------------
phlo's avatar
phlo committed
692

phlo's avatar
phlo committed
693
void Encoder::declare_stmt ()
694 695
{
  if (verbose)
phlo's avatar
phlo committed
696
    formula << stmt_comment;
697 698 699

  iterate_programs([this] (const Program & program) {
    for (pc = 0; pc < program.size(); pc++)
phlo's avatar
phlo committed
700
      formula << declare_bool_var(stmt_var()) << eol;
701 702 703 704 705

    formula << eol;
  });
}

phlo's avatar
phlo committed
706
// smtlib::Encoder::declare_block ----------------------------------------------
phlo's avatar
phlo committed
707

phlo's avatar
phlo committed
708
void Encoder::declare_block ()
709
{
710
  if (checkpoints.empty())
711 712 713
    return;

  if (verbose)
phlo's avatar
phlo committed
714
    formula << block_comment;
715

716 717 718
  for (const auto & [s, threads] : checkpoints)
    {
      assert(threads.size() > 1);
719

720 721 722 723 724 725 726
      for (const auto & t : threads)
        formula
          << declare_bool_var(block_var(step, s, t.first))
          << eol;

      formula << eol;
    }
727 728
}

729 730 731 732
// smtlib::Encoder::declare_halt -----------------------------------------------

void Encoder::declare_halt ()
{
733
  if (halts.empty())
734 735 736 737 738
    return;

  if (verbose)
    formula << halt_comment;

739
  for (const auto & it : halts)
740 741 742 743 744
    formula << declare_bool_var(halt_var(step, it.first)) << eol;

  formula << eol;
}

phlo's avatar
phlo committed
745
// smtlib::Encoder::declare_heap -----------------------------------------------
phlo's avatar
phlo committed
746

phlo's avatar
phlo committed
747
void Encoder::declare_heap ()
748 749
{
  if (verbose)
phlo's avatar
phlo committed
750
    formula << heap_comment;
751

752
  formula
phlo's avatar
phlo committed
753
    << declare_array_var(heap_var(), bv_sort, bv_sort)
754
    << eol << eol;
755 756
}

phlo's avatar
phlo committed
757
// smtlib::Encoder::declare_exit_flag ------------------------------------------
phlo's avatar
phlo committed
758

phlo's avatar
phlo committed
759
void Encoder::declare_exit_flag ()
760
{
761
  if (halts.empty() && exits.empty())
762 763
    return;

764
  if (verbose)
phlo's avatar
phlo committed
765
    formula << exit_flag_comment;
766

phlo's avatar
phlo committed
767
  formula << declare_bool_var(exit_flag_var()) << eol << eol;
768 769
}

phlo's avatar
phlo committed
770
// smtlib::Encoder::declare_exit_code ------------------------------------------
phlo's avatar
phlo committed
771

phlo's avatar
phlo committed
772
void Encoder::declare_exit_code ()
773
{
774
  if (verbose)
phlo's avatar
phlo committed
775
    formula << exit_code_comment;
776

phlo's avatar
phlo committed
777
  formula << declare_bv_var(exit_code_var, word_size) << eol << eol;
778 779
}

phlo's avatar
phlo committed
780
// smtlib::Encoder::declare_states ---------------------------------------------
phlo's avatar
phlo committed
781

phlo's avatar
phlo committed
782
void Encoder::declare_states ()
783 784
{
  if (verbose)
phlo's avatar
phlo committed
785
    formula << comment_subsection("state variable declarations");
786

787 788 789 790 791 792 793
  declare_accu();
  declare_mem();
  declare_sb_adr();
  declare_sb_val();
  declare_sb_full();
  declare_stmt();
  declare_block();
794
  declare_halt();
795

796
  declare_heap();
phlo's avatar
phlo committed
797
  declare_exit_flag();
798

799 800 801
  if (!step)
    declare_exit_code();
}
802

phlo's avatar
phlo committed
803
// smtlib::Encoder::declare_thread ---------------------------------------------
phlo's avatar
phlo committed
804

phlo's avatar
phlo committed
805
void Encoder::declare_thread ()
806 807
{
  if (verbose)
phlo's avatar
phlo committed
808
    formula << thread_comment;
809 810

  iterate_threads([this] {
phlo's avatar
phlo committed
811
    formula << declare_bool_var(thread_var()) << eol;
812 813 814
  });

  formula << eol;
815
}
816

phlo's avatar
phlo committed
817
// smtlib::Encoder::declare_exec -----------------------------------------------
phlo's avatar
phlo committed
818

phlo's avatar
phlo committed
819
void Encoder::declare_exec ()
phlo's avatar
phlo committed
820 821
{
  if (verbose)
phlo's avatar
phlo committed
822
    formula << exec_comment;
phlo's avatar
phlo committed
823 824 825

  iterate_programs([this] (const Program & program) {
    for (pc = 0; pc < program.size(); pc++)
phlo's avatar
phlo committed
826
      formula << declare_bool_var(exec_var()) << eol;
phlo's avatar
phlo committed
827 828 829 830 831

    formula << eol;
  });
}

phlo's avatar
phlo committed
832
// smtlib::Encoder::declare_flush ----------------------------------------------
phlo's avatar
phlo committed
833

phlo's avatar
phlo committed
834
void Encoder::declare_flush ()
835 836
{
  if (verbose)
phlo's avatar
phlo committed
837
    formula << flush_comment;
838 839

  iterate_threads([this] {
phlo's avatar
phlo committed
840
    formula << declare_bool_var(flush_var()) << eol;
841 842 843
  });

  formula << eol;
844
}
845

phlo's avatar
phlo committed
846
// smtlib::Encoder::declare_check ----------------------------------------------
phlo's avatar
phlo committed
847

phlo's avatar
phlo committed
848
void Encoder::declare_check ()
849
{
850
  if (checkpoints.empty())
851
    return;
852

853
  if (verbose)
phlo's avatar
phlo committed
854
    formula << check_comment;
855

856
  for (const auto & s : checkpoints)
phlo's avatar
phlo committed
857
    formula << declare_bool_var(check_var(step, s.first)) << eol;
858 859 860 861

  formula << eol;
}

phlo's avatar
phlo committed
862
// smtlib::Encoder::declare_transitions ----------------------------------------
863

phlo's avatar
phlo committed
864
void Encoder::declare_transitions ()
865 866
{
  if (verbose)
phlo's avatar
phlo committed
867
    formula << comment_subsection("transition variable declarations");
868

869
  declare_thread();
phlo's avatar
phlo committed
870
  declare_exec();
871 872 873
  declare_flush();
  declare_check();
}
874

phlo's avatar
phlo committed
875
// smtlib::Encoder::init_accu --------------------------------------------------
phlo's avatar
phlo committed
876

877 878 879
#define INIT_STATE(_var) \
  do { \
    iterate_threads([this] { \
phlo's avatar
phlo committed
880
      formula << assign(_var(step, thread), word2hex(0)) << eol; \
881 882 883 884
    }); \
    formula << eol; \
  } while (0)

phlo's avatar
phlo committed
885
void Encoder::init_accu ()
886 887
{
  if (verbose)
phlo's avatar
phlo committed
888
    formula << accu_comment;
889 890 891 892

  INIT_STATE(accu_var);
}

phlo's avatar
phlo committed
893
// smtlib::Encoder::init_mem ---------------------------------------------------
phlo's avatar
phlo committed
894

phlo's avatar
phlo committed
895
void Encoder::init_mem ()
896 897
{
  if (verbose)
phlo's avatar
phlo committed
898
    formula << mem_comment;
899 900 901 902

  INIT_STATE(mem_var);
}

phlo's avatar
phlo committed
903
// smtlib::Encoder::init_sb_adr ------------------------------------------------
phlo's avatar
phlo committed
904

phlo's avatar
phlo committed
905
void Encoder::init_sb_adr ()
906 907
{
  if (verbose)
phlo's avatar
phlo committed
908
    formula << sb_adr_comment;
909 910 911 912

  INIT_STATE(sb_adr_var);
}

phlo's avatar
phlo committed
913
// smtlib::Encoder::init_sb_val ------------------------------------------------
phlo's avatar
phlo committed
914

phlo's avatar
phlo committed
915
void Encoder::init_sb_val ()
916 917
{
  if (verbose)
phlo's avatar
phlo committed
918
    formula << sb_val_comment;
919 920 921 922

  INIT_STATE(sb_val_var);
}

phlo's avatar
phlo committed
923
// smtlib::Encoder::init_sb_full -----------------------------------------------
phlo's avatar
phlo committed
924

phlo's avatar
phlo committed
925
void Encoder::init_sb_full ()
926 927
{
  if (verbose)
phlo's avatar
phlo committed
928
    formula << sb_full_comment;
929 930

  iterate_threads([this] {
phlo's avatar
phlo committed
931
    formula << assertion(lnot(sb_full_var())) << eol;
932 933 934 935 936
  });

  formula << eol;
}

phlo's avatar
phlo committed
937
// smtlib::Encoder::init_stmt --------------------------------------------------
phlo's avatar
phlo committed
938

phlo's avatar
phlo committed
939
void Encoder::init_stmt ()
940 941
{
  if (verbose)
phlo's avatar
phlo committed
942
    formula << stmt_comment;
943 944 945 946

  iterate_programs([this] (const Program & program) {
    for (pc = 0; pc < program.size(); pc++)
      formula
phlo's avatar
phlo committed
947
        << assertion(pc ? lnot(stmt_var()) : stmt_var())
948 949 950 951 952 953
        << eol;

    formula << eol;
  });
}

phlo's avatar
phlo committed
954
// smtlib::Encoder::init_block -------------------------------------------------
phlo's avatar
phlo committed
955

phlo's avatar
phlo committed
956
void Encoder::init_block ()
957
{
958
  if (checkpoints.empty())
959 960 961
    return;

  if (verbose)
phlo's avatar
phlo committed
962
    formula << block_comment;
963

964 965 966
  for (const auto & [c, threads] : checkpoints)
    {
      assert(threads.size() > 1);
967

968 969 970 971 972
      for (const auto & [t, pcs] : threads)
        formula << assertion(lnot(block_var(step, c, t))) << eol;

      formula << eol;
    }
973 974
}

975 976 977 978
// smtlib::Encoder::init_halt --------------------------------------------------

void Encoder::init_halt ()
{
979
  if (halts.empty())
980 981 982 983 984
    return;

  if (verbose)
    formula << halt_comment;

985 986
  for (const auto & it : halts)
    formula << assertion(lnot(halt_var(step, it.first))) << eol;
987 988 989 990

  formula << eol;
}

991 992 993 994 995 996 997 998 999 1000 1001 1002 1003 1004 1005 1006
// smtlib::Encoder::init_heap --------------------------------------------------

void Encoder::init_heap ()
{
  if (!mmap || mmap->empty())
    return;

  if (verbose)
    formula << heap_comment;

  for (const auto & [adr, val] : *mmap)
    formula << assign(select(heap_var(), word2hex(adr)), word2hex(val)) << eol;

  formula << eol;
}

phlo's avatar
phlo committed
1007
// smtlib::Encoder::init_exit_flag ---------------------------------------------
phlo's avatar
phlo committed
1008

phlo's avatar
phlo committed
1009
void Encoder::init_exit_flag ()
1010
{
1011
  if (halts.empty() && exits.empty())
1012 1013 1014
    return;

  if (verbose)
phlo's avatar
phlo committed
1015
    formula << exit_flag_comment;
1016

phlo's avatar
phlo committed
1017
  formula << assertion(lnot(exit_flag_var())) << eol << eol;
1018 1019
}

phlo's avatar
phlo committed
1020
// smtlib::Encoder::init_states ------------------------------------------------
phlo's avatar
phlo committed
1021

phlo's avatar
phlo committed
1022
void Encoder::init_states ()
1023 1024 1025 1026
{
  assert(!step);

  if (verbose)
phlo's avatar
phlo committed
1027
    formula << comment_subsection("state variable initializations");
1028 1029 1030 1031 1032 1033 1034 1035

  init_accu();
  init_mem();
  init_sb_adr();
  init_sb_val();
  init_sb_full();
  init_stmt();
  init_block();
1036
  init_halt();
1037 1038

  init_heap();
phlo's avatar
phlo committed
1039 1040 1041
  init_exit_flag();
}

phlo's avatar
phlo committed
1042
// smtlib::Encoder::define_exec ------------------------------------------------
phlo's avatar
phlo committed
1043

phlo's avatar
phlo committed
1044
void Encoder::define_exec ()
phlo's avatar
phlo committed
1045 1046
{
  if (verbose)
phlo's avatar
phlo committed
1047
    formula << exec_comment;
phlo's avatar
phlo committed
1048 1049 1050 1051

  iterate_programs([this] (const Program & program) {
    for (pc = 0; pc < program.size(); pc++)
      formula
1052
        << assign(exec_var(), land(stmt_var(), thread_var()))
phlo's avatar
phlo committed
1053 1054 1055 1056
        << eol;

    formula << eol;
  });
1057 1058
}

phlo's avatar
phlo committed
1059
// smtlib::Encoder::define_check -----------------------------------------------
phlo's avatar
phlo committed
1060

phlo's avatar
phlo committed
1061
void Encoder::define_check ()
1062
{
1063
  if (checkpoints.empty())
1064
    return;
1065

1066
  if (verbose)
phlo's avatar
phlo committed
1067
    formula << check_comment;
1068

1069
  for (const auto & [c, threads] : checkpoints)
1070
    {
1071 1072
      assert(threads.size() > 1);

1073 1074
      if (step)
        {
phlo's avatar
phlo committed
1075
          std::vector<std::string> check_args;
1076

1077
          check_args.reserve(threads.size());
1078

1079 1080
          for (const auto & t : threads)
            check_args.push_back(block_var(step, c, t.first));
1081

phlo's avatar
phlo committed
1082
          formula << assign(check_var(step, c), land(check_args));
1083 1084 1085
        }
      else
        {
phlo's avatar
phlo committed
1086
          formula << assertion(lnot(check_var(step, c)));
1087
        }
1088 1089 1090 1091

      formula << eol;
    }

1092 1093
  formula << eol;
}
1094

phlo's avatar
phlo committed
1095
// smtlib::Encoder::define_transitions -----------------------------------------
phlo's avatar
phlo committed
1096

phlo's avatar
phlo committed
1097
void Encoder::define_transitions ()
1098
{
1099
  if (verbose)
phlo's avatar
phlo committed
1100
    formula << comment_subsection("transition variable definitions");
1101

phlo's avatar
phlo committed
1102 1103
  define_exec();
  define_check();
1104 1105
}

phlo's avatar
phlo committed
1106
// smtlib::Encoder::define_scheduling_constraints ------------------------------
phlo's avatar
phlo committed
1107

phlo's avatar
phlo committed
1108
void Encoder::define_scheduling_constraints ()
1109
{
1110
  if (verbose)
phlo's avatar
phlo committed
1111
    formula << comment_subsection("scheduling constraints");
1112

phlo's avatar
phlo committed
1113
  std::vector<std::string> variables;
phlo's avatar
phlo committed
1114 1115 1116 1117 1118 1119 1120 1121

  variables.reserve(num_threads * 2 + 1);

  iterate_threads([this, &variables] {
    variables.push_back(thread_var());
    variables.push_back(flush_var());
  });

1122
  if (!halts.empty() || !exits.empty())
phlo's avatar
phlo committed
1123 1124 1125 1126
    variables.push_back(exit_flag_var());

  formula
    << (use_sinz_constraint
phlo's avatar
phlo committed
1127 1128
      ? card_constraint_sinz(variables)
      : card_constraint_naive(variables))
phlo's avatar
phlo committed
1129
    << eol;
1130 1131
}

phlo's avatar
phlo committed
1132
// smtlib::Encoder::define_store_buffer_constraints ----------------------------
phlo's avatar
phlo committed
1133

phlo's avatar
phlo committed
1134
void Encoder::define_store_buffer_constraints ()
1135
{
1136
  if (verbose)
phlo's avatar
phlo committed
1137
    formula << comment_subsection("store buffer constraints");
1138

1139
  iterate_threads([this] {
1140
    if (flushes.find(thread) != flushes.end())
1141
      {
1142
        const auto & pcs = flushes[thread];
1143

phlo's avatar
phlo committed
1144
        std::vector<std::string> stmts;
1145

1146
        stmts.reserve(pcs.size());
1147 1148

        for (const word_t p : pcs)
1149 1150 1151
          stmts.push_back(stmt_var(step, thread, p));

        formula <<
phlo's avatar
phlo committed
1152 1153
          assertion(
            ite(
1154
              sb_full_var(),
phlo's avatar
phlo committed
1155 1156 1157 1158
              implication(
                lor(stmts),
                lnot(thread_var())),
              lnot(flush_var()))) <<
1159
          eol;
1160
      }
1161 1162 1163 1164
    else
      {
        // TODO: (or sb-full (not flush)) directly?
        formula <<
phlo's avatar
phlo committed
1165 1166 1167 1168
          assertion(
            implication(
              lnot(sb_full_var()),
              lnot(flush_var()))) <<
1169 1170 1171
          eol;
      }
  });
1172 1173

  formula << eol;
1174
}
1175

1176
// smtlib::Encoder::define_checkpoint_constraints ------------------------------
phlo's avatar
phlo committed
1177

1178
void Encoder::define_checkpoint_constraints ()
1179
{
1180
  if (checkpoints.empty())
1181
    return;
1182 1183

  if (verbose)
phlo's avatar
phlo committed
1184
    formula << comment_subsection("checkpoint constraints");
1185

1186 1187 1188
  for (const auto & [c, threads] : checkpoints)
    {
      assert(threads.size() > 1);
1189

1190 1191 1192 1193 1194
      for (const auto & [t, pcs] : threads)
        {
          formula <<
            assertion(
              implication(
1195
                land(
1196
                  block_var(step, c, t),
1197
                  lnot(check_var(step, c))),
1198
                lnot(thread_var(step, t))));
1199

1200 1201
          if (verbose)
            formula << " ; checkpoint " << c << ": thread " << t;
1202

1203 1204 1205 1206 1207
          formula << eol;
        }

      formula << eol;
    }
1208 1209
}

1210 1211 1212 1213
// smtlib::Encoder::define_halt_constraints ------------------------------------

void Encoder::define_halt_constraints ()
{
1214
  if (halts.empty())
1215 1216 1217 1218 1219
    return;

  if (verbose)
    formula << comment_subsection("halt constraints");

1220
  for (const auto & it : halts)
1221 1222 1223 1224 1225 1226 1227 1228 1229 1230
    formula <<
      assertion(
        implication(
            halt_var(step, it.first),
            lnot(thread_var(step, it.first)))) <<
      eol;

  formula << eol;
}

phlo's avatar
phlo committed
1231
// smtlib::Encoder::define_constraints -----------------------------------------
phlo's avatar
phlo committed
1232

phlo's avatar
phlo committed
1233
void Encoder::define_constraints ()
1234
{
phlo's avatar
phlo committed
1235
  define_scheduling_constraints();
1236
  define_store_buffer_constraints();
1237 1238
  define_checkpoint_constraints();
  define_halt_constraints();
1239 1240
}

phlo's avatar
phlo committed
1241
} // namespace ConcuBinE::smtlib