encoder_smtlib.cc 26.6 KB
Newer Older
1 2
#include "encoder.hh"

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 15 16 17 18
//==============================================================================

//------------------------------------------------------------------------------
// static members
//------------------------------------------------------------------------------

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

phlo's avatar
phlo committed
20
const std::string Encoder::bv_sort = bitvector(word_size);
21

phlo's avatar
phlo committed
22 23
// exit code variable ----------------------------------------------------------

phlo's avatar
phlo committed
24
const std::string & Encoder::exit_code_var = exit_code_sym;
phlo's avatar
phlo committed
25 26 27

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

phlo's avatar
phlo committed
28 29
const std::string Encoder::accu_comment =
  comment(
phlo's avatar
phlo committed
30 31 32 33 34
    ConcuBinE::Encoder::accu_comment
    + " - "
    + accu_sym
    + "_<step>_<thread>"
    + eol);
35

phlo's avatar
phlo committed
36
const std::string Encoder::mem_comment =
phlo's avatar
phlo committed
37 38 39 40 41 42
  comment(
    ConcuBinE::Encoder::mem_comment
    + " - "
    + mem_sym
    + "_<step>_<thread>"
    + eol);
43

phlo's avatar
phlo committed
44 45
const std::string Encoder::sb_adr_comment =
  comment(
phlo's avatar
phlo committed
46 47 48 49 50
    ConcuBinE::Encoder::sb_adr_comment
    + " - "
    + sb_adr_sym
    + "_<step>_<thread>"
    + eol);
51

phlo's avatar
phlo committed
52 53
const std::string Encoder::sb_val_comment =
  comment(
phlo's avatar
phlo committed
54 55 56 57 58
    ConcuBinE::Encoder::sb_val_comment
    + " - "
    + sb_val_sym
    + "_<step>_<thread>"
    + eol);
59

phlo's avatar
phlo committed
60 61
const std::string Encoder::sb_full_comment =
  comment(
phlo's avatar
phlo committed
62 63 64 65 66
    ConcuBinE::Encoder::sb_full_comment
    + " - "
    + sb_full_sym
    + "_<step>_<thread>"
    + eol);
67

phlo's avatar
phlo committed
68 69
const std::string Encoder::stmt_comment =
  comment(
phlo's avatar
phlo committed
70 71 72 73 74
    ConcuBinE::Encoder::stmt_comment
    + " - "
    + stmt_sym
    + "_<step>_<thread>_<pc>"
    + eol);
75

phlo's avatar
phlo committed
76 77
const std::string Encoder::block_comment =
  comment(
phlo's avatar
phlo committed
78 79 80 81 82
    ConcuBinE::Encoder::block_comment
    + " - "
    + block_sym
    + "_<step>_<id>_<thread>"
    + eol);
83

84 85
const std::string Encoder::halt_comment =
  comment(
phlo's avatar
phlo committed
86 87 88 89 90
    ConcuBinE::Encoder::halt_comment
    + " - "
    + halt_sym
    + "_<step>_<thread>"
    + eol);
91

phlo's avatar
phlo committed
92 93
const std::string Encoder::heap_comment =
  comment(
phlo's avatar
phlo committed
94 95 96 97 98
    ConcuBinE::Encoder::heap_comment
    + " - "
    + heap_sym
    + "_<step>"
    + eol);
99

phlo's avatar
phlo committed
100 101
const std::string Encoder::exit_flag_comment =
  comment(
phlo's avatar
phlo committed
102 103 104 105 106
    ConcuBinE::Encoder::exit_flag_comment
    + " - "
    + exit_flag_sym
    + "_<step>"
    + eol);
phlo's avatar
phlo committed
107

phlo's avatar
phlo committed
108
const std::string Encoder::exit_code_comment =
phlo's avatar
phlo committed
109
  comment(ConcuBinE::Encoder::exit_code_comment + eol);
110

phlo's avatar
phlo committed
111 112
const std::string Encoder::thread_comment =
  comment(
phlo's avatar
phlo committed
113 114 115 116 117
    ConcuBinE::Encoder::thread_comment
    + " - "
    + thread_sym
    + "_<step>_<thread>"
    + eol);
118

phlo's avatar
phlo committed
119 120
const std::string Encoder::exec_comment =
  comment(
phlo's avatar
phlo committed
121 122 123 124 125
    ConcuBinE::Encoder::exec_comment
    + " - "
    + exec_sym
    + "_<step>_<thread>_<pc>"
    + eol);
phlo's avatar
phlo committed
126

phlo's avatar
phlo committed
127 128
const std::string Encoder::flush_comment =
  comment(
phlo's avatar
phlo committed
129 130 131 132 133
    ConcuBinE::Encoder::flush_comment
    + " - "
    + flush_sym
    + "_<step>_<thread>"
    + eol);
134

phlo's avatar
phlo committed
135 136
const std::string Encoder::check_comment =
  comment(
phlo's avatar
phlo committed
137 138 139 140 141
    ConcuBinE::Encoder::check_comment
    + " - "
    + check_sym
    + "_<step>_<id>"
    + eol);
142

phlo's avatar
phlo committed
143 144 145
//------------------------------------------------------------------------------
// constructors
//------------------------------------------------------------------------------
146

147 148 149 150
Encoder::Encoder (const Program::List::ptr & p,
                  const std::shared_ptr<MMap> & m,
                  const size_t b) :
  ConcuBinE::Encoder(p, m, b),
151 152 153
  step(0)
{}

phlo's avatar
phlo committed
154 155 156 157
//------------------------------------------------------------------------------
// private member functions
//------------------------------------------------------------------------------

phlo's avatar
phlo committed
158
// smtlib::Encoder::accu_var ---------------------------------------------------
phlo's avatar
phlo committed
159

phlo's avatar
phlo committed
160
std::string Encoder::accu_var (const word_t k, const word_t t)
161
{
phlo's avatar
phlo committed
162
  return accu_sym + '_' + std::to_string(k) + '_' + std::to_string(t);
163 164
}

phlo's avatar
phlo committed
165
std::string Encoder::accu_var () const
166 167 168 169
{
  return accu_var(step, thread);
}

phlo's avatar
phlo committed
170
// smtlib::Encoder::mem_var ----------------------------------------------------
phlo's avatar
phlo committed
171

phlo's avatar
phlo committed
172
std::string Encoder::mem_var (const word_t k, const word_t t)
173
{
phlo's avatar
phlo committed
174
  return mem_sym + '_' + std::to_string(k) + '_' + std::to_string(t);
175 176
}

phlo's avatar
phlo committed
177
std::string Encoder::mem_var () const
178 179 180 181
{
  return mem_var(step, thread);
}

phlo's avatar
phlo committed
182
// smtlib::Encoder::sb_adr_var -------------------------------------------------
phlo's avatar
phlo committed
183

phlo's avatar
phlo committed
184
std::string Encoder::sb_adr_var (const word_t k, const word_t t)
185
{
phlo's avatar
phlo committed
186
  return sb_adr_sym + '_' + std::to_string(k) + '_' + std::to_string(t);
187 188
}

phlo's avatar
phlo committed
189
std::string Encoder::sb_adr_var () const
190 191 192 193
{
  return sb_adr_var(step, thread);
}

phlo's avatar
phlo committed
194
// smtlib::Encoder::sb_val_var -------------------------------------------------
phlo's avatar
phlo committed
195

phlo's avatar
phlo committed
196
std::string Encoder::sb_val_var (const word_t k, const word_t t)
197
{
phlo's avatar
phlo committed
198
  return sb_val_sym + '_' + std::to_string(k) + '_' + std::to_string(t);
199 200
}

phlo's avatar
phlo committed
201
std::string Encoder::sb_val_var () const
202 203 204 205
{
  return sb_val_var(step, thread);
}

phlo's avatar
phlo committed
206
// smtlib::Encoder::sb_full_var ------------------------------------------------
phlo's avatar
phlo committed
207

phlo's avatar
phlo committed
208
std::string Encoder::sb_full_var (const word_t k, const word_t t)
209
{
phlo's avatar
phlo committed
210
  return sb_full_sym + '_' + std::to_string(k) + '_' + std::to_string(t);
211 212
}

phlo's avatar
phlo committed
213
std::string Encoder::sb_full_var () const
214 215 216 217
{
  return sb_full_var(step, thread);
}

phlo's avatar
phlo committed
218
// smtlib::Encoder::stmt_var ---------------------------------------------------
phlo's avatar
phlo committed
219

phlo's avatar
phlo committed
220
std::string Encoder::stmt_var (const word_t k, const word_t t, const word_t p)
221 222 223
{
  return
    stmt_sym + '_' +
phlo's avatar
phlo committed
224 225 226
    std::to_string(k) + '_' +
    std::to_string(t) + '_' +
    std::to_string(p);
227 228
}

phlo's avatar
phlo committed
229
std::string Encoder::stmt_var () const
230 231 232 233
{
  return stmt_var(step, thread, pc);
}

phlo's avatar
phlo committed
234
// smtlib::Encoder::block_var --------------------------------------------------
phlo's avatar
phlo committed
235

phlo's avatar
phlo committed
236 237 238
std::string Encoder::block_var (const word_t k,
                                const word_t id,
                                const word_t tid)
239 240 241
{
  return
    block_sym + '_' +
phlo's avatar
phlo committed
242 243 244
    std::to_string(k) + '_' +
    std::to_string(id) + '_' +
    std::to_string(tid);
245 246
}

247 248 249 250 251 252 253 254 255 256 257 258
// 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);
}

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

phlo's avatar
phlo committed
259
// smtlib::Encoder::heap_var ---------------------------------------------------
phlo's avatar
phlo committed
260

phlo's avatar
phlo committed
261
std::string Encoder::heap_var (const word_t k)
262
{
phlo's avatar
phlo committed
263
  return heap_sym + '_' + std::to_string(k);
264 265
}

phlo's avatar
phlo committed
266
std::string Encoder::heap_var () const
267 268 269 270
{
  return heap_var(step);
}

phlo's avatar
phlo committed
271
// smtlib::Encoder::exit_flag_var ----------------------------------------------
phlo's avatar
phlo committed
272

phlo's avatar
phlo committed
273
std::string Encoder::exit_flag_var (const word_t k)
274
{
phlo's avatar
phlo committed
275
  return exit_flag_sym + '_' + std::to_string(k);
276 277
}

phlo's avatar
phlo committed
278
std::string Encoder::exit_flag_var () const
279
{
phlo's avatar
phlo committed
280
  return exit_flag_var(step);
281 282
}

phlo's avatar
phlo committed
283
// smtlib::Encoder::thread_var -------------------------------------------------
phlo's avatar
phlo committed
284

phlo's avatar
phlo committed
285
std::string Encoder::thread_var (const word_t k, const word_t t)
286
{
phlo's avatar
phlo committed
287
  return thread_sym + '_' + std::to_string(k) + '_' + std::to_string(t);
288 289
}

phlo's avatar
phlo committed
290
std::string Encoder::thread_var () const
291 292 293 294
{
  return thread_var(step, thread);
}

phlo's avatar
phlo committed
295
// smtlib::Encoder::exec_var ---------------------------------------------------
phlo's avatar
phlo committed
296

phlo's avatar
phlo committed
297
std::string Encoder::exec_var (const word_t k, const word_t t, const word_t p)
298
{
phlo's avatar
phlo committed
299 300
  return
    exec_sym + '_' +
phlo's avatar
phlo committed
301 302 303
    std::to_string(k) + '_' +
    std::to_string(t) + '_' +
    std::to_string(p);
304 305
}

phlo's avatar
phlo committed
306
std::string Encoder::exec_var () const
307
{
phlo's avatar
phlo committed
308
  return exec_var(step, thread, pc);
309 310
}

phlo's avatar
phlo committed
311
// smtlib::Encoder::flush_var --------------------------------------------------
phlo's avatar
phlo committed
312

phlo's avatar
phlo committed
313
std::string Encoder::flush_var (const word_t k, const word_t t)
314
{
phlo's avatar
phlo committed
315
  return flush_sym + '_' + std::to_string(k) + '_' + std::to_string(t);
316 317
}

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

phlo's avatar
phlo committed
323
// smtlib::Encoder::check_var --------------------------------------------------
phlo's avatar
phlo committed
324

phlo's avatar
phlo committed
325
std::string Encoder::check_var (const word_t k, const word_t id)
326
{
phlo's avatar
phlo committed
327
  return check_sym + '_' + std::to_string(k) + '_' + std::to_string(id);
328 329
}

phlo's avatar
phlo committed
330
// smtlib::Encoder::assign -----------------------------------------------------
331

phlo's avatar
phlo committed
332 333
std::string Encoder::assign (const std::string & var,
                             const std::string & expr) const
334
{
phlo's avatar
phlo committed
335
  return assertion(equality({var, expr}));
336 337
}

phlo's avatar
phlo committed
338
// smtlib::Encoder::load -------------------------------------------------------
phlo's avatar
phlo committed
339

phlo's avatar
phlo committed
340
std::string Encoder::load (const word_t adr, const bool indirect)
341
{
342 343 344 345 346 347 348 349 350 351 352 353 354 355 356 357 358 359 360 361 362
  /*
  (ite sb-full
    (ite (= sb-adr #....)
      sb-val
      (select heap #....))
    (select heap #....))
  */
  /*
  (ite sb-full
    (ite (= sb-adr #....)                   ; sb-full
      (ite (= sb-val #....)                   ; (= sb-adr #....)
        #.... | sb-val                          ; (= sb-val #....)
        (ite (= sb-adr (select heap sb-val))    ; (not (= sb-val #....))
          sb-val                                  ; (= sb-adr (select heap sb-val))
          (select heap (select heap sb-val))))    ; (not (= sb-adr (select heap sb-val)))
      (ite (= sb-adr (select heap #....))     ; (not (= sb-adr #....))
        sb-val                                  ; (= sb-adr (select heap #....))
        (select (select heap #....))))          ; (not (= sb-adr (select heap #....)))
    (select (select heap #x....)))          ; (not sb-full)
  */

phlo's avatar
phlo committed
363
  std::string address = word2hex(adr);
364

phlo's avatar
phlo committed
365 366 367 368
  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);
369

phlo's avatar
phlo committed
370
  std::string load = select(heap, address);
371 372 373

  if (indirect)
    {
phlo's avatar
phlo committed
374 375 376
      std::string load_sb = select(heap, sb_val);
      std::string load_sb_indirect = select(heap, load_sb);
      std::string load_indirect = select(heap, load);
377 378

      return
phlo's avatar
phlo committed
379
        ite(
380
          sb_full,
phlo's avatar
phlo committed
381 382 383 384
          ite(
            equality({sb_adr, address}),
            ite(
              equality({sb_val, address}),
385
              sb_val,
phlo's avatar
phlo committed
386 387
              ite(
                equality({sb_adr, load_sb}),
388
                sb_val,
phlo's avatar
phlo committed
389 390 391
                load_sb_indirect)),
            ite(
              equality({sb_adr, load}),
392
              sb_val,
phlo's avatar
phlo committed
393 394
              load_indirect)),
          load_indirect);
395 396 397 398
    }
  else
    {
      return
phlo's avatar
phlo committed
399 400
        ite(
          land({sb_full, equality({sb_adr, address})}),
401
          sb_val,
phlo's avatar
phlo committed
402
          load);
403
    }
404 405
}

phlo's avatar
phlo committed
406
// smtlib::Encoder::declare_accu -----------------------------------------------
phlo's avatar
phlo committed
407

phlo's avatar
phlo committed
408
void Encoder::declare_accu ()
409 410
{
  if (verbose)
phlo's avatar
phlo committed
411
    formula << accu_comment;
412 413

  iterate_threads([this] {
phlo's avatar
phlo committed
414
    formula << declare_bv_var(accu_var(), word_size) << eol;
415 416 417 418 419
  });

  formula << eol;
}

phlo's avatar
phlo committed
420
// smtlib::Encoder::declare_mem ------------------------------------------------
phlo's avatar
phlo committed
421

phlo's avatar
phlo committed
422
void Encoder::declare_mem ()
423 424
{
  if (verbose)
phlo's avatar
phlo committed
425
    formula << mem_comment;
426 427

  iterate_threads([this] {
phlo's avatar
phlo committed
428
    formula << declare_bv_var(mem_var(), word_size) << eol;
429 430 431 432 433
  });

  formula << eol;
}

phlo's avatar
phlo committed
434
// smtlib::Encoder::declare_sb_adr ---------------------------------------------
phlo's avatar
phlo committed
435

phlo's avatar
phlo committed
436
void Encoder::declare_sb_adr ()
437 438
{
  if (verbose)
phlo's avatar
phlo committed
439
    formula << sb_adr_comment;
440 441

  iterate_threads([this] {
phlo's avatar
phlo committed
442
    formula << declare_bv_var(sb_adr_var(), word_size) << eol;
443 444 445 446 447
  });

  formula << eol;
}

phlo's avatar
phlo committed
448
// smtlib::Encoder::declare_sb_val ---------------------------------------------
phlo's avatar
phlo committed
449

phlo's avatar
phlo committed
450
void Encoder::declare_sb_val ()
451 452
{
  if (verbose)
phlo's avatar
phlo committed
453
    formula << sb_val_comment;
454 455

  iterate_threads([this] {
phlo's avatar
phlo committed
456
    formula << declare_bv_var(sb_val_var(), word_size) << eol;
457 458 459 460 461
  });

  formula << eol;
}

phlo's avatar
phlo committed
462
// smtlib::Encoder::declare_sb_full --------------------------------------------
phlo's avatar
phlo committed
463

phlo's avatar
phlo committed
464
void Encoder::declare_sb_full ()
465 466
{
  if (verbose)
phlo's avatar
phlo committed
467
    formula << sb_full_comment;
468 469

  iterate_threads([this] {
phlo's avatar
phlo committed
470
    formula << declare_bool_var(sb_full_var()) << eol;
471 472 473 474 475
  });

  formula << eol;
}

phlo's avatar
phlo committed
476
// smtlib::Encoder::declare_stmt -----------------------------------------------
phlo's avatar
phlo committed
477

phlo's avatar
phlo committed
478
void Encoder::declare_stmt ()
479 480
{
  if (verbose)
phlo's avatar
phlo committed
481
    formula << stmt_comment;
482 483 484

  iterate_programs([this] (const Program & program) {
    for (pc = 0; pc < program.size(); pc++)
phlo's avatar
phlo committed
485
      formula << declare_bool_var(stmt_var()) << eol;
486 487 488 489 490

    formula << eol;
  });
}

phlo's avatar
phlo committed
491
// smtlib::Encoder::declare_block ----------------------------------------------
phlo's avatar
phlo committed
492

phlo's avatar
phlo committed
493
void Encoder::declare_block ()
494
{
495
  if (check_pcs.empty())
496 497 498
    return;

  if (verbose)
phlo's avatar
phlo committed
499
    formula << block_comment;
500 501 502 503

  for (const auto & [s, threads] : check_pcs)
    for (const auto & t : threads)
      formula
phlo's avatar
phlo committed
504
        << declare_bool_var(block_var(step, s, t.first))
505 506 507 508 509
        << eol;

  formula << eol;
}

510 511 512 513 514 515 516 517 518 519 520 521 522 523 524 525
// smtlib::Encoder::declare_halt -----------------------------------------------

void Encoder::declare_halt ()
{
  if (halt_pcs.empty())
    return;

  if (verbose)
    formula << halt_comment;

  for (const auto & it : halt_pcs)
    formula << declare_bool_var(halt_var(step, it.first)) << eol;

  formula << eol;
}

phlo's avatar
phlo committed
526
// smtlib::Encoder::declare_heap -----------------------------------------------
phlo's avatar
phlo committed
527

phlo's avatar
phlo committed
528
void Encoder::declare_heap ()
529 530
{
  if (verbose)
phlo's avatar
phlo committed
531
    formula << heap_comment;
532

533
  formula
phlo's avatar
phlo committed
534
    << declare_array_var(heap_var(), bv_sort, bv_sort)
535
    << eol << eol;
536 537
}

phlo's avatar
phlo committed
538
// smtlib::Encoder::declare_exit_flag ------------------------------------------
phlo's avatar
phlo committed
539

phlo's avatar
phlo committed
540
void Encoder::declare_exit_flag ()
541
{
542
  if (halt_pcs.empty() && exit_pcs.empty())
543 544
    return;

545
  if (verbose)
phlo's avatar
phlo committed
546
    formula << exit_flag_comment;
547

phlo's avatar
phlo committed
548
  formula << declare_bool_var(exit_flag_var()) << eol << eol;
549 550
}

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

phlo's avatar
phlo committed
553
void Encoder::declare_exit_code ()
554
{
555
  if (verbose)
phlo's avatar
phlo committed
556
    formula << exit_code_comment;
557

phlo's avatar
phlo committed
558
  formula << declare_bv_var(exit_code_var, word_size) << eol << eol;
559 560
}

phlo's avatar
phlo committed
561
// smtlib::Encoder::declare_states ---------------------------------------------
phlo's avatar
phlo committed
562

phlo's avatar
phlo committed
563
void Encoder::declare_states ()
564 565
{
  if (verbose)
phlo's avatar
phlo committed
566
    formula << comment_subsection("state variable declarations");
567

568 569 570 571 572 573 574
  declare_accu();
  declare_mem();
  declare_sb_adr();
  declare_sb_val();
  declare_sb_full();
  declare_stmt();
  declare_block();
575
  declare_halt();
576

577
  declare_heap();
phlo's avatar
phlo committed
578
  declare_exit_flag();
579

580 581 582
  if (!step)
    declare_exit_code();
}
583

phlo's avatar
phlo committed
584
// smtlib::Encoder::declare_thread ---------------------------------------------
phlo's avatar
phlo committed
585

phlo's avatar
phlo committed
586
void Encoder::declare_thread ()
587 588
{
  if (verbose)
phlo's avatar
phlo committed
589
    formula << thread_comment;
590 591

  iterate_threads([this] {
phlo's avatar
phlo committed
592
    formula << declare_bool_var(thread_var()) << eol;
593 594 595
  });

  formula << eol;
596
}
597

phlo's avatar
phlo committed
598
// smtlib::Encoder::declare_exec -----------------------------------------------
phlo's avatar
phlo committed
599

phlo's avatar
phlo committed
600
void Encoder::declare_exec ()
phlo's avatar
phlo committed
601 602
{
  if (verbose)
phlo's avatar
phlo committed
603
    formula << exec_comment;
phlo's avatar
phlo committed
604 605 606

  iterate_programs([this] (const Program & program) {
    for (pc = 0; pc < program.size(); pc++)
phlo's avatar
phlo committed
607
      formula << declare_bool_var(exec_var()) << eol;
phlo's avatar
phlo committed
608 609 610 611 612

    formula << eol;
  });
}

phlo's avatar
phlo committed
613
// smtlib::Encoder::declare_flush ----------------------------------------------
phlo's avatar
phlo committed
614

phlo's avatar
phlo committed
615
void Encoder::declare_flush ()
616 617
{
  if (verbose)
phlo's avatar
phlo committed
618
    formula << flush_comment;
619 620

  iterate_threads([this] {
phlo's avatar
phlo committed
621
    formula << declare_bool_var(flush_var()) << eol;
622 623 624
  });

  formula << eol;
625
}
626

phlo's avatar
phlo committed
627
// smtlib::Encoder::declare_check ----------------------------------------------
phlo's avatar
phlo committed
628

phlo's avatar
phlo committed
629
void Encoder::declare_check ()
630 631 632
{
  if (check_pcs.empty())
    return;
633

634
  if (verbose)
phlo's avatar
phlo committed
635
    formula << check_comment;
636

637
  for (const auto & s : check_pcs)
phlo's avatar
phlo committed
638
    formula << declare_bool_var(check_var(step, s.first)) << eol;
639 640 641 642

  formula << eol;
}

phlo's avatar
phlo committed
643
// smtlib::Encoder::declare_transitions ----------------------------------------
644

phlo's avatar
phlo committed
645
void Encoder::declare_transitions ()
646 647
{
  if (verbose)
phlo's avatar
phlo committed
648
    formula << comment_subsection("transition variable declarations");
649

650
  declare_thread();
phlo's avatar
phlo committed
651
  declare_exec();
652 653 654
  declare_flush();
  declare_check();
}
655

phlo's avatar
phlo committed
656
// smtlib::Encoder::init_accu --------------------------------------------------
phlo's avatar
phlo committed
657

658 659 660
#define INIT_STATE(_var) \
  do { \
    iterate_threads([this] { \
phlo's avatar
phlo committed
661
      formula << assign(_var(step, thread), word2hex(0)) << eol; \
662 663 664 665
    }); \
    formula << eol; \
  } while (0)

phlo's avatar
phlo committed
666
void Encoder::init_accu ()
667 668
{
  if (verbose)
phlo's avatar
phlo committed
669
    formula << accu_comment;
670 671 672 673

  INIT_STATE(accu_var);
}

phlo's avatar
phlo committed
674
// smtlib::Encoder::init_mem ---------------------------------------------------
phlo's avatar
phlo committed
675

phlo's avatar
phlo committed
676
void Encoder::init_mem ()
677 678
{
  if (verbose)
phlo's avatar
phlo committed
679
    formula << mem_comment;
680 681 682 683

  INIT_STATE(mem_var);
}

phlo's avatar
phlo committed
684
// smtlib::Encoder::init_sb_adr ------------------------------------------------
phlo's avatar
phlo committed
685

phlo's avatar
phlo committed
686
void Encoder::init_sb_adr ()
687 688
{
  if (verbose)
phlo's avatar
phlo committed
689
    formula << sb_adr_comment;
690 691 692 693

  INIT_STATE(sb_adr_var);
}

phlo's avatar
phlo committed
694
// smtlib::Encoder::init_sb_val ------------------------------------------------
phlo's avatar
phlo committed
695

phlo's avatar
phlo committed
696
void Encoder::init_sb_val ()
697 698
{
  if (verbose)
phlo's avatar
phlo committed
699
    formula << sb_val_comment;
700 701 702 703

  INIT_STATE(sb_val_var);
}

phlo's avatar
phlo committed
704
// smtlib::Encoder::init_sb_full -----------------------------------------------
phlo's avatar
phlo committed
705

phlo's avatar
phlo committed
706
void Encoder::init_sb_full ()
707 708
{
  if (verbose)
phlo's avatar
phlo committed
709
    formula << sb_full_comment;
710 711

  iterate_threads([this] {
phlo's avatar
phlo committed
712
    formula << assertion(lnot(sb_full_var())) << eol;
713 714 715 716 717
  });

  formula << eol;
}

phlo's avatar
phlo committed
718
// smtlib::Encoder::init_stmt --------------------------------------------------
phlo's avatar
phlo committed
719

phlo's avatar
phlo committed
720
void Encoder::init_stmt ()
721 722
{
  if (verbose)
phlo's avatar
phlo committed
723
    formula << stmt_comment;
724 725 726 727

  iterate_programs([this] (const Program & program) {
    for (pc = 0; pc < program.size(); pc++)
      formula
phlo's avatar
phlo committed
728
        << assertion(pc ? lnot(stmt_var()) : stmt_var())
729 730 731 732 733 734
        << eol;

    formula << eol;
  });
}

phlo's avatar
phlo committed
735
// smtlib::Encoder::init_block -------------------------------------------------
phlo's avatar
phlo committed
736

phlo's avatar
phlo committed
737
void Encoder::init_block ()
738 739 740 741 742
{
  if (check_pcs.empty())
    return;

  if (verbose)
phlo's avatar
phlo committed
743
    formula << block_comment;
744 745 746

  for (const auto & [c, threads] : check_pcs)
    for (const auto & [t, pcs] : threads)
phlo's avatar
phlo committed
747
      formula << assertion(lnot(block_var(step, c, t))) << eol;
748 749 750 751

  formula << eol;
}

752 753 754 755 756 757 758 759 760 761 762 763 764 765 766 767 768
// smtlib::Encoder::init_halt --------------------------------------------------

void Encoder::init_halt ()
{
  if (halt_pcs.empty())
    return;

  if (verbose)
    formula << halt_comment;

  iterate_threads([this] {
    formula << assertion(lnot(halt_var())) << eol;
  });

  formula << eol;
}

769 770 771 772 773 774 775 776 777 778 779 780 781 782 783 784
// 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
785
// smtlib::Encoder::init_exit_flag ---------------------------------------------
phlo's avatar
phlo committed
786

phlo's avatar
phlo committed
787
void Encoder::init_exit_flag ()
788
{
789
  if (halt_pcs.empty() && exit_pcs.empty())
790 791 792
    return;

  if (verbose)
phlo's avatar
phlo committed
793
    formula << exit_flag_comment;
794

phlo's avatar
phlo committed
795
  formula << assertion(lnot(exit_flag_var())) << eol << eol;
796 797
}

phlo's avatar
phlo committed
798
// smtlib::Encoder::init_states ------------------------------------------------
phlo's avatar
phlo committed
799

phlo's avatar
phlo committed
800
void Encoder::init_states ()
801 802 803 804
{
  assert(!step);

  if (verbose)
phlo's avatar
phlo committed
805
    formula << comment_subsection("state variable initializations");
806 807 808 809 810 811 812 813

  init_accu();
  init_mem();
  init_sb_adr();
  init_sb_val();
  init_sb_full();
  init_stmt();
  init_block();
814
  init_halt();
815 816

  init_heap();
phlo's avatar
phlo committed
817 818 819
  init_exit_flag();
}

phlo's avatar
phlo committed
820
// smtlib::Encoder::define_exec ------------------------------------------------
phlo's avatar
phlo committed
821

phlo's avatar
phlo committed
822
void Encoder::define_exec ()
phlo's avatar
phlo committed
823 824
{
  if (verbose)
phlo's avatar
phlo committed
825
    formula << exec_comment;
phlo's avatar
phlo committed
826 827 828 829

  iterate_programs([this] (const Program & program) {
    for (pc = 0; pc < program.size(); pc++)
      formula
phlo's avatar
phlo committed
830
        << assign(exec_var(), land({stmt_var(), thread_var()}))
phlo's avatar
phlo committed
831 832 833 834
        << eol;

    formula << eol;
  });
835 836
}

phlo's avatar
phlo committed
837
// smtlib::Encoder::define_check -----------------------------------------------
phlo's avatar
phlo committed
838

phlo's avatar
phlo committed
839
void Encoder::define_check ()
840 841 842
{
  if (check_pcs.empty())
    return;
843

844
  if (verbose)
phlo's avatar
phlo committed
845
    formula << check_comment;
846

847
  for (const auto & [c, threads] : check_pcs)
848
    {
849 850
      if (step)
        {
phlo's avatar
phlo committed
851
          std::vector<std::string> check_args;
852

853
          check_args.reserve(threads.size());
854

855 856
          for (const auto & t : threads)
            check_args.push_back(block_var(step, c, t.first));
857

phlo's avatar
phlo committed
858
          formula << assign(check_var(step, c), land(check_args));
859 860 861
        }
      else
        {
phlo's avatar
phlo committed
862
          formula << assertion(lnot(check_var(step, c)));
863
        }
864 865 866 867

      formula << eol;
    }

868 869
  formula << eol;
}
870

phlo's avatar
phlo committed
871
// smtlib::Encoder::define_transitions -----------------------------------------
phlo's avatar
phlo committed
872

phlo's avatar
phlo committed
873
void Encoder::define_transitions ()
874
{
875
  if (verbose)
phlo's avatar
phlo committed
876
    formula << comment_subsection("transition variable definitions");
877

phlo's avatar
phlo committed
878 879
  define_exec();
  define_check();
880 881
}

phlo's avatar
phlo committed
882
// smtlib::Encoder::define_scheduling_constraints ------------------------------
phlo's avatar
phlo committed
883

phlo's avatar
phlo committed
884
void Encoder::define_scheduling_constraints ()
885
{
886
  if (verbose)
phlo's avatar
phlo committed
887
    formula << comment_subsection("scheduling constraints");
888

phlo's avatar
phlo committed
889
  std::vector<std::string> variables;
phlo's avatar
phlo committed
890 891 892 893 894 895 896 897

  variables.reserve(num_threads * 2 + 1);

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

898
  if (!halt_pcs.empty() || !exit_pcs.empty())
phlo's avatar
phlo committed
899 900 901 902
    variables.push_back(exit_flag_var());

  formula
    << (use_sinz_constraint
phlo's avatar
phlo committed
903 904
      ? card_constraint_sinz(variables)
      : card_constraint_naive(variables))
phlo's avatar
phlo committed
905
    << eol;
906 907
}

phlo's avatar
phlo committed
908
// smtlib::Encoder::define_store_buffer_constraints ----------------------------
phlo's avatar
phlo committed
909

phlo's avatar
phlo committed
910
void Encoder::define_store_buffer_constraints ()
911
{
912
  if (verbose)
phlo's avatar
phlo committed
913
    formula << comment_subsection("store buffer constraints");
914

915 916
  iterate_threads([this] {
    if (flush_pcs.find(thread) != flush_pcs.end())
917
      {
918 919
        const auto & pcs = flush_pcs[thread];

phlo's avatar
phlo committed
920
        std::vector<std::string> stmts;
921

922
        stmts.reserve(pcs.size());
923 924

        for (const word_t p : pcs)
925 926 927
          stmts.push_back(stmt_var(step, thread, p));

        formula <<
phlo's avatar
phlo committed
928 929
          assertion(
            ite(
930
              sb_full_var(),
phlo's avatar
phlo committed
931 932 933 934
              implication(
                lor(stmts),
                lnot(thread_var())),
              lnot(flush_var()))) <<
935
          eol;
936
      }
937 938 939 940
    else
      {
        // TODO: (or sb-full (not flush)) directly?
        formula <<
phlo's avatar
phlo committed
941 942 943 944
          assertion(
            implication(
              lnot(sb_full_var()),
              lnot(flush_var()))) <<
945 946 947
          eol;
      }
  });
948 949

  formula << eol;
950
}
951

952
// smtlib::Encoder::define_checkpoint_constraints ------------------------------
phlo's avatar
phlo committed
953

954
void Encoder::define_checkpoint_constraints ()
955 956 957
{
  if (check_pcs.empty())
    return;
958 959

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

962
  for (const auto & [c, threads] : check_pcs)
963 964 965
    for (const auto & [t, pcs] : threads)
      {
        formula <<
phlo's avatar
phlo committed
966 967 968
          assertion(
            implication(
              land({
969
                block_var(step, c, t),
phlo's avatar
phlo committed
970 971
                lnot(check_var(step, c))}),
              lnot(thread_var(step, t))));
972 973

        if (verbose)
974
          formula << " ; checkpoint " << c << ": thread " << t;
975 976 977 978 979 980 981

        formula << eol;
      }

  formula << eol;
}

982 983 984 985 986 987 988 989 990 991 992 993 994 995 996 997 998 999 1000 1001 1002
// smtlib::Encoder::define_halt_constraints ------------------------------------

void Encoder::define_halt_constraints ()
{
  if (halt_pcs.empty())
    return;

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

  for (const auto & it : halt_pcs)
    formula <<
      assertion(
        implication(
            halt_var(step, it.first),
            lnot(thread_var(step, it.first)))) <<
      eol;

  formula << eol;
}

phlo's avatar
phlo committed
1003
// smtlib::Encoder::define_constraints -----------------------------------------
phlo's avatar
phlo committed
1004

phlo's avatar
phlo committed
1005
void Encoder::define_constraints ()
1006
{
phlo's avatar
phlo committed
1007
  define_scheduling_constraints();
1008
  define_store_buffer_constraints();
1009 1010
  define_checkpoint_constraints();
  define_halt_constraints();
1011 1012
}

phlo's avatar
phlo committed
1013
// smtlib::Encoder::encode -----------------------------------------------------
phlo's avatar
phlo committed
1014

phlo's avatar
phlo committed
1015
void Encoder::encode ()
1016
{
phlo's avatar
phlo committed
1017
  formula << set_logic() << eol << eol;
1018

phlo's avatar
phlo committed
1019
  for (step = 0, prev = static_cast<size_t>(-1); step <= bound; step++, prev++)
1020 1021
    {
      if (verbose)
phlo's avatar
phlo committed
1022
        formula << comment_section("step " + std::to_string(step));
1023 1024 1025

      declare_states();
      declare_transitions();
phlo's avatar
phlo committed
1026
      define_transitions();
1027

1028 1029 1030 1031 1032
      if (step)
        define_states();
      else
        init_states();

1033 1034
      define_constraints ();
    }
1035
}
1036

phlo's avatar
phlo committed
1037
std::string Encoder::encode (const Instruction::Load & l)
1038 1039 1040 1041
{
  return load(l.arg, l.indirect);
}

phlo's avatar
phlo committed
1042
std::string Encoder::encode (const Instruction::Store & s)
1043 1044 1045
{
  switch (update)
    {
phlo's avatar
phlo committed
1046
    case State::sb_adr:
phlo's avatar
phlo committed
1047
      return s.indirect ? load(s.arg) : word2hex(s.arg);
1048

phlo's avatar
phlo committed
1049
    case State::sb_val:
1050 1051
      return accu_var(prev, thread);

phlo's avatar
phlo committed
1052
    default: throw std::runtime_error("illegal state update");
1053 1054 1055
    }
}

phlo's avatar
phlo committed
1056
std::string Encoder::encode (const Instruction::Fence & f [[maybe_unused]])
1057 1058 1059 1060
{
  return "";
}

phlo's avatar
phlo committed
1061
std::string Encoder::encode (const Instruction::Add & a)
1062
{
phlo's avatar
phlo committed
1063
  return bvadd({accu_var(prev, thread), load(a.arg, a.indirect)});
1064 1065
}

phlo's avatar
phlo committed
1066
std::string Encoder::encode (const Instruction::Addi & a)
1067
{
phlo's avatar
phlo committed
1068
  return bvadd({accu_var(prev, thread), word2hex(a.arg)});
1069 1070
}

phlo's avatar
phlo committed
1071
std::string Encoder::encode (const Instruction::Sub & s)
1072
{
phlo's avatar
phlo committed
1073
  return bvsub({accu_var(prev, thread), load(s.arg, s.indirect)});
1074 1075
}

phlo's avatar
phlo committed
1076
std::string Encoder::encode (const Instruction::Subi & s)
1077
{
phlo's avatar
phlo committed
1078
  return bvsub({accu_var(prev, thread), word2hex(s.arg)});
1079 1080
}

phlo's avatar
phlo committed
1081
std::string Encoder::encode (const Instruction::Mul & m)
phlo's avatar
phlo committed
1082
{
phlo's avatar
phlo committed
1083
  return bvmul({accu_var(prev, thread), load(m.arg, m.indirect)});
phlo's avatar
phlo committed
1084 1085
}

phlo's avatar
phlo committed
1086
std::string Encoder::encode (const Instruction::Muli & m)
phlo's avatar
phlo committed
1087
{
phlo's avatar
phlo committed
1088
  return bvmul({accu_var(prev, thread), word2hex(m.arg)});
phlo's avatar
phlo committed
1089 1090
}

phlo's avatar
phlo committed
1091
std::string Encoder::encode (const Instruction::Cmp & c)
1092
{
phlo's avatar
phlo committed
1093
  return bvsub({accu_var(prev, thread), load(c.arg, c.indirect)});
1094 1095
}

phlo's avatar
phlo committed
1096
std::string Encoder::encode (const Instruction::Jmp & j [[maybe_unused]])
1097 1098 1099 1100
{
  return "";
}

phlo's avatar
phlo committed
1101
std::string Encoder::encode (const Instruction::Jz & j [[maybe_unused]])
1102
{
phlo's avatar
phlo committed
1103
  return equality({accu_var(prev, thread), word2hex(0)});
1104 1105
}

phlo's avatar
phlo committed
1106
std::string Encoder::encode (const Instruction::Jnz & j [[maybe_unused]])
1107 1108
{
  return
phlo's avatar
phlo committed
1109 1110
    lnot(
      equality({
1111
        accu_var(prev, thread),
phlo's avatar
phlo committed
1112
        word2hex(0)}));
1113 1114
}

phlo's avatar
phlo committed
1115
std::string Encoder::encode (const Instruction::Js & j [[maybe_unused]])
1116
{
phlo's avatar
phlo committed
1117
  static const std::string bw = std::to_string(word_size - 1);
1118 1119

  return
phlo's avatar
phlo committed
1120
      equality({
1121
        "#b1",
phlo's avatar
phlo committed
1122
        extract(bw, bw, accu_var(prev, thread))});
1123 1124
}

phlo's avatar
phlo committed
1125
std::string Encoder::encode (const Instruction::Jns & j [[maybe_unused]])
1126
{
phlo's avatar
phlo committed
1127
  static const std::string bw = std::to_string(word_size - 1);
1128 1129

  return
phlo's avatar
phlo committed
1130
      equality({
1131
        "#b0",
phlo's avatar
phlo committed
1132
        extract(bw, bw, accu_var(prev, thread))});
1133 1134
}

phlo's avatar
phlo committed
1135
std::string Encoder::encode (const Instruction::Jnzns & j [[maybe_unused]])
1136
{
phlo's avatar
phlo committed
1137
  static const std::string bw = std::to_string(word_size - 1);
1138 1139

  return
phlo's avatar
phlo committed
1140 1141 1142
    land({
      lnot(
        equality({
1143
          accu_var(prev, thread),
phlo's avatar
phlo committed
1144 1145
          word2hex(0)})),
      equality({
1146
        "#b0",
phlo's avatar
phlo committed
1147
        extract(bw, bw, accu_var(prev, thread))})});
1148 1149
}

phlo's avatar
phlo committed
1150
std::string Encoder::encode (const Instruction::Mem & m)
1151 1152 1153 1154
{
  return load(m.arg, m.indirect);
}

phlo's avatar
phlo committed
1155
std::string Encoder::encode (const Instruction::Cas & c)
1156
{
phlo's avatar
phlo committed
1157
  std::string heap = heap_var(prev);
1158

phlo's avatar
phlo committed
1159 1160 1161
  std::string address = c.indirect
    ? select(heap, word2hex(c.arg))
    : word2hex(c.arg);
1162

phlo's avatar
phlo committed
1163 1164
  std::string condition =
    equality({
1165
      mem_var(prev, thread),
phlo's avatar
phlo committed
1166
      select(heap, address)});
1167 1168 1169

  switch (update)
    {
phlo's avatar
phlo committed
1170
    case State::accu:
1171
      return
phlo's avatar
phlo committed
1172
        ite(